Model checking propositional dynamic logic with all extras

DOI10.1016/J.JAL.2005.08.002MaRDI QIDQ2494725zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• Infinite State Model-Checking of Propositional Dynamic Logics
• PDL with intersection and converse: satisfiability and infinite-state model checking
• scientific article; zbMATH DE number 1678389
• scientific article; zbMATH DE number 5599076
• The propositional dynamic logic of deterministic, well-structured programs

Cites work

• A characterization of exponential-time languages by alternating context- free grammars
• A dynamic logic for acting, sensing, and planning
• A lattice-theoretical fixpoint theorem and its applications
• A lower complexity bound for propositional dynamic logic with intersection
• A New Normal-Form Theorem for Context-Free Phrase Structure Grammars
• A Theorem on Boolean Matrices
• Alternation
• Automata-theoretic techniques for modal logics of programs
• Gaussian elimination is not optimal
• scientific article; zbMATH DE number 3974280 (Why is no real title available?)
• scientific article; zbMATH DE number 3983144 (Why is no real title available?)
• scientific article; zbMATH DE number 1032009 (Why is no real title available?)
• scientific article; zbMATH DE number 1142324 (Why is no real title available?)
• scientific article; zbMATH DE number 2064229 (Why is no real title available?)
• scientific article; zbMATH DE number 1556014 (Why is no real title available?)
• scientific article; zbMATH DE number 1747449 (Why is no real title available?)
• scientific article; zbMATH DE number 2149447 (Why is no real title available?)
• scientific article; zbMATH DE number 941396 (Why is no real title available?)
• scientific article; zbMATH DE number 2087624 (Why is no real title available?)
• Propositional dynamic logic of looping and converse is elementarily decidable
• Propositional dynamic logic of nonregular programs
• Propositional dynamic logic of regular programs
• Recurring Dominoes: Making the Highly Undecidable Highly Understandable
• The complexity of PDL with interleaving

Cited in

(35)

• Polyadic dynamic logics for HPSG parsing
• An automata-theoretic approach to the verification of distributed algorithms
• Combining deduction and model checking into tableaux and algorithms for converse-PDL.
• Communicating finite-state machines, first-order logic, and star-free propositional dynamic logic
• Temporal logics with language parameters
• On qualitative route descriptions. Representation, agent models, and computational complexity
• scientific article; zbMATH DE number 1678389 (Why is no real title available?)
• Extending propositional dynamic logic for Petri nets
• Complexity optimal decision procedure for a propositional dynamic logic with parallel composition
• Minimal Proof Search for Modal Logic K Model Checking
• scientific article; zbMATH DE number 2084327 (Why is no real title available?)
• Reasoning about joint action and coalitional ability in \(K _{n }\) with intersection
• Formal language constrained reachability and model checking propositional dynamic logics
• Checking interval properties of computations
• Infinite State Model-Checking of Propositional Dynamic Logics
• PDL with intersection and converse: satisfiability and infinite-state model checking
• Logical Foundations of XML and XQuery
• scientific article; zbMATH DE number 19783 (Why is no real title available?)
• scientific article; zbMATH DE number 218549 (Why is no real title available?)
• It is easy to be wise after the event: communicating finite-state machines capture first-order logic with ``happened before
• A dynamic epistemic framework for conformant planning
• Propositional Dynamic Logic for Hyperproperties
• \(\mathrm{FO}=\mathrm{FO}^3\) for linear orders with monotone binary relations
• Embedding coalition logic in the minimal normal multimodal logic with intersection
• Dynamic epistemic logics
• A calculus for automatic verification of Petri nets based on resolution and dynamic logics
• Propositional dynamic logic with converse and repeat for message-passing systems
• Propositional dynamic logic with converse and repeat for message-passing systems
• Axiomatization and computability of a variant of iteration-free PDL with fork
• Temporal logics with language parameters
• Model checking timed recursive CTL
• Separating the expressive power of propositional dynamic and modal fixpoint logics
• Knowing how to plan about planning: higher-order and meta-level epistemic planning
• Propositional dynamic logic formula synthesis and some applications
• Propositional dynamic logic of context-free programs and fixpoint logic with chop

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2494725)