Weak bisimilarity between finite-state systems and BPA or normed BPP is decidable in polynomial time

DOI10.1016/S0304-3975(01)00094-9zbMath0988.68118MaRDI QIDQ5958326

Antonín Kučera, Richard Mayr

Publication date: 3 March 2002

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

zbMATH Keywords

verificationbisimulationconcurrencyprocess algebrasonfinite-state systems

Mathematics Subject Classification ID

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

Related Items

A generic framework for checking semantic equivalences between pushdown automata and finite-state automata, The complexity of bisimilarity-checking for one-counter processes., Complexity of deciding bisimilarity between normed BPA and normed BPP, Normed BPA vs. Normed BPP Revisited, Weak bisimilarity and regularity of context-free processes is EXPTIME-hard, On the complexity of checking semantic equivalences between pushdown processes and finite-state processes, Simulation preorder over simple process algebras

Cites Work

• A short proof of the decidability of bisimulation for normed BPA- processes
• Comparing expressibility of normed BPA and normed BPP processes
• A polynomial algorithm for deciding bisimilarity of normed context-free processes
• 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
• Graphes canoniques de graphes algébriques
• An elementary bisimulation decision procedure for arbitrary context-free processes
• Three Partition Refinement Algorithms
• Process Algebra
• Actions speak louder than words: proving bisimilarity for context-free processes
• A polynomial-time algorithm for deciding bisimulation equivalence of normed Basic Parallel Processes
• Complexity of Weak Bisimilarity and Regularity for BPA and BPP
• Petri nets, commutative context-free grammars, and basic parallel processes
• Decidability of model checking with the temporal logic EF
• Deciding bisimulation-like equivalences with finite-state processes
• Reachability analysis of pushdown automata: Application to model-checking
• Infinite results
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item