Deciding bisimulation-like equivalences with finite-state processes

DOI10.1016/S0304-3975(00)00027-XzbMath0974.68131WikidataQ127740450 ScholiaQ127740450MaRDI QIDQ5941202

Antonín Kučera, Petr Jančar, Richard Mayr

Publication date: 20 August 2001

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

zbMATH Keywords

bisimulationconcurrencyinfinite-state systemscharacteristic formulae

Mathematics Subject Classification ID

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

Related Items (17)

Regularity of normed PA processes ⋮ DP lower bounds for equivalence-checking and model-checking of one-counter automata ⋮ Characteristic invariants in Hennessy-Milner logic ⋮ The complexity of bisimilarity-checking for one-counter processes. ⋮ Petri nets and regular processes ⋮ Computable fixpoints in well-structured symbolic model checking ⋮ Complexity of Weak Bisimilarity and Regularity for BPA and BPP ⋮ Petri nets are less expressive than state-extended PA ⋮ Deciding probabilistic simulation between probabilistic pushdown automata and finite-state systems ⋮ On the complexity of checking semantic equivalences between pushdown processes and 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 ⋮ The regular viewpoint on PA-processes ⋮ Reachability is decidable for weakly extended process rewrite systems ⋮ Decidable first-order transition logics for PA-processes ⋮ Simulation preorder over simple process algebras ⋮ On Symbolic Verification of Weakly Extended PAD

Cites Work

• Undecidability of bisimilarity for Petri nets and some related problems
• On the regular structure of prefix rewriting
• Decidability of a temporal logic problem for Petri nets
• The theory of ends, pushdown automata, and second-order logic
• Decidability of bisimulation equivalence for normed pushdown processes
• Comparing expressibility of normed BPA and normed BPP processes
• Characteristic formulae for processes with divergence
• Effective decomposability of sequential behaviours
• Process rewrite systems.
• Bisimulation equivalence is decidable for all context-free processes
• Decidability of model checking for infinite-state concurrent systems
• Decidability of bisimulation equivalence for process generating context-free languages
• Process Algebra
• Branching time and abstraction in bisimulation semantics
• On the Ehrenfeucht-Fraïssé game in theoretical computer science
• Decidability of model checking with the temporal logic EF
• Reachability analysis of pushdown automata: Application to model-checking
• Model checking PA-processes
• Infinite results
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Deciding bisimulation-like equivalences with finite-state processes