PDL with intersection and converse: satisfiability and infinite-state model checking

DOI10.2178/JSL/1231082313zbMath1181.03034OpenAlexW2019785612MaRDI QIDQ3616354

Markus Lohrey, Stefan Göller, Carsten Lutz

Publication date: 25 March 2009

Published in: The Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2178/jsl/1231082313

zbMATH Keywords

automatamodel checkingdynamic logicsatisfiability

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Formal languages and automata (68Q45) Logic in computer science (03B70) Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)

Related Items (9)

Unnamed Item ⋮ Querying the Unary Negation Fragment with Regular Path Expressions. ⋮ 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 ⋮ Temporal logics for concurrent recursive programs: satisfiability and model checking ⋮ Undecidability of representability as binary relations ⋮ Relative expressive power of navigational querying on graphs ⋮ Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• DAL -- a logic for data analysis
• Automata-theoretic techniques for modal logics of programs
• Alternating automata on infinite trees
• A near-optimal method for reasoning about action
• Propositional dynamic logic of regular programs
• Computer aided verification. 14th international conference, CAV 2002, Copenhagen, Denmark, July 27--31, 2002. Proceedings
• Guarded fixed point logics and the monadic theory of countable trees.
• Pushdown processes: Games and model-checking
• Model checking LTL with regular valuations for pushdown systems
• Infinite State Model-Checking of Propositional Dynamic Logics
• PDL for ordered trees
• PDL with negation of atomic programs
• Alternation
• A Modal Perspective on Path Constraints
• Decidability of model checking with the temporal logic EF
• The regular viewpoint on PA-processes

This page was built for publication: PDL with intersection and converse: satisfiability and infinite-state model checking