Decidability of model checking with the temporal logic EF

DOI10.1016/S0304-3975(00)00101-8zbMath0973.68169MaRDI QIDQ5941100

Richard Mayr

Publication date: 20 August 2001

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

process algebramodel checkingtemporal logicEFinfinite-state systemsPA-processespushdown processes

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items

Characteristic invariants in Hennessy-Milner logic ⋮ An Automata-Theoretic Approach to the Reachability Analysis of RPPS Systems ⋮ Deciding bisimulation-like equivalences with finite-state processes ⋮ A general approach to comparing infinite-state systems with their finite-state specifications ⋮ Weak bisimilarity between finite-state systems and BPA or normed BPP is decidable in polynomial time ⋮ PDL with intersection and converse: satisfiability and infinite-state model checking ⋮ Refining the Process Rewrite Systems Hierarchy via Ground Tree Rewrite Systems ⋮ Refining the Process Rewrite Systems Hierarchy via Ground Tree Rewrite Systems ⋮ Model Checking FO(R) over One-Counter Processes and beyond ⋮ Decidable first-order transition logics for PA-processes

Cites Work

• Undecidability of bisimilarity for Petri nets and some related problems
• On the regular structure of prefix rewriting
• Algebra of communicating processes with abstraction
• Process rewrite systems.
• Pushdown processes: Games and model-checking
• Decidability of model checking for infinite-state concurrent systems
• Reachability analysis of pushdown automata: Application to model-checking
• Model checking PA-processes
• Infinite results
• Bisimulation collapse and the process taxonomy
• Constrained properties, semilinear systems, and Petri nets
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item