Propositional dynamic logic of regular programs

1979/04/01 by Michael J. Fischer, Richard E. Ladner · 1,195 citations
Computer Science · Mathematics · #Algorithm #Autoepistemic logic #Computer science #Correctness #Description logic #Discrete mathematics #Dynamic logic (digital electronics) #Equivalence (formal languages) #Formal Methods in Verification #Intermediate logic #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Mathematics #Modal #Modal logic #Modal μ-calculus #Multimodal logic #Nondeterministic algorithm #Programming language #Propositional variable #Satisfiability #Well-formed formula #Zeroth-order logic

paper · doi:10.1016/0022-0000(79)90046-1

published in Journal of Computer and System Sciences 18(2), 194-211 (Elsevier BV)

openalex publication_date 1979/04/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/06

Cited by

• A probabilistic PDL
• The Complexity of the Constructive Master Modality
• The Equational Theory of Relational Kleene Algebra with Graph Loop is PSPACE-Complete
• Guarded Negation Transitive Closure Logic
• Dynamic Logic with Parallel Operator for Verifying Communication Protocols
• Alternating Pushdown and Stack Automata
• A Logical Framework for Trust-Related Emotions
• Many-valued coalgebraic dynamic logics: Safety and strong completeness via reducibility
• Tableaux for Dynamic Logic of Propositional Assignments
• Correctness of an Incremental and Worst-Case Optimal Decision Procedure for Modal Logic with Eventualities
• Comparing State-Representations for DEL Model Checking
• Complexity Results and Practical Algorithms for Logics in Knowledge Representation
• The Limit of Recursion in State-based Systems
• Modalities for model checking: branching time logic strikes back
• A theory of timed automata
• Logic programming for deliberative robotic task planning
• An Introduction to Logics of Knowledge and Belief
• Parametric Linear Dynamic Logic (full version)
• Robust Vacuity for Branching Temporal Logic
• Continuation Semantics for Fixpoint Modal Logic and Computation Tree Logics
• The Complexity of Defining and Separating Fixpoint Formulae in Modal Logic
• On Explicit Solutions to Fixed-Point Equations in Propositional Dynamic Logic
• An On-the-fly Tableau-based Decision Procedure for PDL-Satisfiability
• Automated Verification of Interactive Rule-Based Configuration Systems (Additional Material)
• Parallelized sequential composition, pipelines, and hardware weak memory models
• An Automaton-based Characterisation of First-Order Logic over Infinite Trees
• Interpolation for Converse PDL
• Model checking: the interval way
• Short proofs without interference
• Reasoning About Common Knowledge with Infinitely Many Agents
• A Note on the Complexity of Model-Checking Bounded Multi-Pushdown Systems
• Propositional dynamic logic with Belnapian truth values
• Models and temporal logical specifications for timed component connectors
• ExpTime Tableaux for Type PDL
• Model Checking for Modal Dependence Logic: An Approach Through Post's Lattice
• Non-Sequential Theory of Distributed Systems
• Partially Observable Markov Decision Processes with Behavioral Norms
• Timed Systems through the Lens of Logic
• SCULPT: A Schema Language for Tabular Data on the Web
• Semantics and Axiomatization for Stochastic Differential Dynamic Logic
• Kleene algebra with tests
• Predicative proof theory of PDL and basic applications
• CCS-Based Dynamic Logics for Communicating Concurrent Programs
• Algebras for Deterministic Computation Are Inherently Incomplete
• Automata for dynamic answer set solving: Preliminary report
• Inquisitive Team Semantics of LTL
• The model checking fingerprints of CTL operators
• Characterization theorems for PDL and FO(TC)
• Description Logics
• LTLf and LDLf Monitoring: A Technical Report
• Handling Conflicts in Depth-First Search for LTL Tableau to Debug Compliance Based Languages
• Alternation
• Undecidability of the Emptiness Problem of Deterministic Propositional While Programs with Graph Loop: Hypothesis Elimination Using Loops
• Modal Logics and mu-Calculi: An Introduction
• Efficient on-the-fly model-checking for regular alternation-free mu-calculus
• Unary negation
• A Canonical Model Construction for Iteration-Free PDL with Intersection
• The Complexity of Model Checking Higher-Order Fixpoint Logic
• Modelling and verification of reconfigurable multi-agent systems. [europepmc]
• NP Reasoning in the Monotone [europepmc]
• Towards Model Checking Real-World Software-Defined Networks [europepmc]