Decidability of model checking with the temporal logic EF

DOI10.1016/S0304-3975(00)00101-8MaRDI QIDQ5941100zbMATH OpenFDO

Authors Richard M. Mayr

Publication date 20 August 2001

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

Full work available at URL https://doi.org/10.1016/S0304-3975(00)00101-8

zbMATH Keywords

EFinfinite-state systemsmodel checkingPA-processesprocess algebrapushdown processestemporal logic

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 2196601
• Model-checking timed temporal logics
• A model checker for linear time temporal logic
• scientific article; zbMATH DE number 1744956
• Model checking general linear temporal logic
• Decidability for a temporal logic used in discrete-event system analysis
• Symbolic model checking for temporal-epistemic logic
• From Model Checking to a Temporal Proof for Partial Models
• scientific article; zbMATH DE number 1696823

Cites work

• Algebra of communicating processes with abstraction
• Bisimulation collapse and the process taxonomy
• Constrained properties, semilinear systems, and Petri nets
• Decidability of model checking for infinite-state concurrent systems
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 52748 (Why is no real title available?)
• scientific article; zbMATH DE number 1231599 (Why is no real title available?)
• scientific article; zbMATH DE number 1263840 (Why is no real title available?)
• scientific article; zbMATH DE number 1304329 (Why is no real title available?)
• scientific article; zbMATH DE number 1304991 (Why is no real title available?)
• scientific article; zbMATH DE number 1064110 (Why is no real title available?)
• scientific article; zbMATH DE number 1088051 (Why is no real title available?)
• scientific article; zbMATH DE number 1414283 (Why is no real title available?)
• scientific article; zbMATH DE number 1456956 (Why is no real title available?)
• Infinite results
• Model checking PA-processes
• On the regular structure of prefix rewriting
• Process rewrite systems.
• Pushdown processes: Games and model-checking
• Reachability analysis of pushdown automata: Application to model-checking
• Undecidability of bisimilarity for Petri nets and some related problems

Cited in

(15)

• 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
• Model checking EGF on basic parallel processes
• PDL with intersection and converse: satisfiability and infinite-state model checking
• Model Checking FO(R) over One-Counter Processes and beyond
• scientific article; zbMATH DE number 177234 (Why is no real title available?)
• A decidability result for the model checking of infinite-state systems
• An automata-theoretic approach to the reachability analysis of RPPS systems
• From Model Checking to a Temporal Proof for Partial Models
• Refining the process rewrite systems hierarchy via ground tree rewrite systems
• Refining the process rewrite systems hierarchy via ground tree rewrite 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
• Model checking PA-processes

This page was built for publication: Decidability of model checking with the temporal logic EF

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5941100)