Model checking propositional dynamic logic with all extras

DOI10.1016/j.jal.2005.08.002zbMath1095.68053OpenAlexW2117221156MaRDI QIDQ2494725

Martin Lange

Publication date: 30 June 2006

Published in: Journal of Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jal.2005.08.002

zbMATH Keywords

complexitymodel checkingpropositional dynamic logic

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (21)

Extending propositional dynamic logic for Petri nets ⋮ Propositional dynamic logic of context-free programs and fixpoint logic with chop ⋮ Checking interval properties of computations ⋮ Minimal Proof Search for Modal Logic K Model Checking ⋮ Unnamed Item ⋮ An automata-theoretic approach to the verification of distributed algorithms ⋮ Communicating finite-state machines, first-order logic, and star-free propositional dynamic logic ⋮ Unnamed Item ⋮ Temporal logics with language parameters ⋮ A calculus for automatic verification of Petri nets based on resolution and dynamic logics ⋮ Temporal logics with language parameters ⋮ Unnamed Item ⋮ Axiomatization and computability of a variant of iteration-free PDL with fork ⋮ Embedding Coalition Logic in the Minimal Normal Multimodal Logic with Intersection ⋮ Polyadic dynamic logics for HPSG parsing ⋮ Complexity Optimal Decision Procedure for a Propositional Dynamic Logic with Parallel Composition ⋮ Reasoning about Joint Action and Coalitional Ability in K n with Intersection ⋮ Logical Foundations of XML and XQuery ⋮ Propositional Dynamic Logic for Hyperproperties ⋮ Dynamic Epistemic Logics ⋮ On qualitative route descriptions. Representation, agent models, and computational complexity

Cites Work

• Propositional dynamic logic of nonregular programs
• Automata-theoretic techniques for modal logics of programs
• A characterization of exponential-time languages by alternating context- free grammars
• Propositional dynamic logic of regular programs
• The complexity of PDL with interleaving
• Gaussian elimination is not optimal
• A lattice-theoretical fixpoint theorem and its applications
• Recurring Dominoes: Making the Highly Undecidable Highly Understandable
• Propositional dynamic logic of looping and converse is elementarily decidable
• Alternation
• A dynamic logic for acting, sensing, and planning
• A New Normal-Form Theorem for Context-Free Phrase Structure Grammars
• A Theorem on Boolean Matrices
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Model checking propositional dynamic logic with all extras