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 algebra; model checking; temporal logic; EF; infinite-state systems; PA-processes; pushdown processes

Mathematics Subject Classification ID

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

Related Items

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

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