Propositional dynamic logic of regular programs

1979/04/01 by Michael J. Fischer, Richard E. Ladner · 39 citations
Computer Science · #Logic, programming, and type systems #Logic, Reasoning, and Knowledge #Formal Methods in Verification

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

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\n 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\n 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\n Lattice
• Non-Sequential Theory of Distributed Systems
• Modelling and verification of reconfigurable multi-agent systems. [europepmc]
• NP Reasoning in the Monotone [europepmc]
• Towards Model Checking Real-World Software-Defined Networks [europepmc]