PDL with intersection and converse: satisfiability and infinite-state model checking
From MaRDI portal
Logic in computer science (03B70) Automata and formal grammars in connection with logical questions (03D05) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Analysis of algorithms and problem complexity (68Q25) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)
Recommendations
Cites work
- A Modal Perspective on Path Constraints
- A near-optimal method for reasoning about action
- Alternating automata on infinite trees
- Alternation
- Automata-theoretic techniques for modal logics of programs
- Computer aided verification. 14th international conference, CAV 2002, Copenhagen, Denmark, July 27--31, 2002. Proceedings
- DAL -- a logic for data analysis
- Decidability of model checking with the temporal logic EF
- Guarded fixed point logics and the monadic theory of countable trees.
- scientific article; zbMATH DE number 1936671 (Why is no real title available?)
- scientific article; zbMATH DE number 1556014 (Why is no real title available?)
- scientific article; zbMATH DE number 795590 (Why is no real title available?)
- Infinite State Model-Checking of Propositional Dynamic Logics
- Model checking LTL with regular valuations for pushdown systems
- PDL for ordered trees
- PDL with negation of atomic programs
- Propositional dynamic logic of regular programs
- Pushdown processes: Games and model-checking
- The regular viewpoint on PA-processes
Cited in
(19)- The complexity of PDL with interleaving
- An automata-theoretic approach to the verification of distributed algorithms
- Eliminating ``converse from converse PDL
- Communicating finite-state machines, first-order logic, and star-free propositional dynamic logic
- Model checking propositional dynamic logic with all extras
- Satisfiability for SCULPT-schemas for CSV-like data
- Querying the unary negation fragment with regular path expressions
- Infinite State Model-Checking of Propositional Dynamic Logics
- PDL with intersection of programs: a complete axiomatization
- scientific article; zbMATH DE number 3974280 (Why is no real title available?)
- Temporal logics for concurrent recursive programs: satisfiability and model checking
- Undecidability of representability as binary relations
- It is easy to be wise after the event: communicating finite-state machines capture first-order logic with ``happened before
- \(\mathrm{FO}=\mathrm{FO}^3\) for linear orders with monotone binary relations
- Relative expressive power of navigational querying on graphs
- Computer Science Logic
- 2-Exp Time lower bounds for propositional dynamic logics with intersection
- PDL with Intersection and Converse Is 2EXP-Complete
- Derivatives on graphs for the positive calculus of relations with transitive closure
This page was built for publication: PDL with intersection and converse: satisfiability and infinite-state model checking
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3616354)
