Decidability of model checking with the temporal logic EF
From MaRDI portal
Publication:5941100
DOI10.1016/S0304-3975(00)00101-8zbMath0973.68169MaRDI QIDQ5941100
Publication date: 20 August 2001
Published in: Theoretical Computer Science (Search for Journal in Brave)
process algebra; model checking; temporal logic; EF; infinite-state systems; PA-processes; pushdown processes
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