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

DOI10.2178/jsl/1231082313zbMath1181.03034MaRDI QIDQ3616354

Markus Lohrey, Carsten Lutz, Stefan Göller

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

automata; model checking; dynamic logic; satisfiability

Mathematics Subject Classification ID

68Q25: Analysis of algorithms and problem complexity

68Q45: Formal languages and automata

03B70: Logic in computer science

03D05: Automata and formal grammars in connection with logical questions

68Q60: Specification and verification (program logics, model checking, etc.)

68Q17: Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)

Related Items

Undecidability of representability as binary relations, Temporal logics for concurrent recursive programs: satisfiability and model checking

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