Decidability of model checking for infinite-state concurrent systems
From MaRDI portal
Publication:1920224
DOI10.1007/s002360050074zbMath0865.68046OpenAlexW1977601940MaRDI QIDQ1920224
Publication date: 5 June 1997
Published in: Acta Informatica (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s002360050074
Petri netsmodel checkingconcurrent computationmu-calculusparallel processesbranching logicslinear logics
Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Related Items (32)
Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker ⋮ Sequent calculi for process verification: Hennessy-Milner logic for an arbitrary GSOS ⋮ Forward analysis and model checking for trace bounded WSTS ⋮ Generalization strategies for the verification of infinite state systems ⋮ A generic framework for checking semantic equivalences between pushdown automata and finite-state automata ⋮ Proving properties of dynamic process networks ⋮ Model checking PA-processes ⋮ Undecidable problems in unreliable computations. ⋮ ON COUNTER MACHINES, REACHABILITY PROBLEMS, AND DIOPHANTINE EQUATIONS ⋮ REACHABILITY ANALYSIS IN VERIFICATION VIA SUPERCOMPILATION ⋮ Specification and encoding of transaction interaction properties ⋮ Linear temporal logic symbolic model checking ⋮ Program Specialization for Verifying Infinite State Systems: An Experimental Evaluation ⋮ Forward Analysis and Model Checking for Trace Bounded WSTS ⋮ Dynamical systems in categories ⋮ VERIFICATION IN QUEUE-CONNECTED MULTICOUNTER MACHINES ⋮ Decidability of Weak Bisimilarity for a Subset of BPA ⋮ Decidability of model checking with the temporal logic EF ⋮ Deciding bisimulation-like equivalences with finite-state processes ⋮ On the complexity of checking semantic equivalences between pushdown processes and finite-state processes ⋮ Characterizing EF and EX tree logics ⋮ Model checking for process rewrite systems and a class of action-based regular properties ⋮ Weak bisimilarity between finite-state systems and BPA or normed BPP is decidable in polynomial time ⋮ State space analysis of Petri nets with relation-algebraic methods ⋮ Distributed semantics for the \(\pi \)-calculus based on Petri nets with inhibitor ARCS ⋮ A theory of structural stationarity in the \(\pi\)-calculus ⋮ Stop-transitions of Petri Nets* ⋮ ON REACHABILITY AND SAFETY IN INFINITE-STATE SYSTEMS ⋮ Counter machines and verification problems. ⋮ Process rewrite systems. ⋮ On Symbolic Verification of Weakly Extended PAD ⋮ Analysis issues in Petri nets with inhibitor arcs
This page was built for publication: Decidability of model checking for infinite-state concurrent systems
