Bisimilarity on basic process algebra is in 2-ExpTime (an explicit proof)

DOI10.2168/LMCS-9(1:10)2013MaRDI QIDQ4913773zbMATH OpenOpenAlexFDO

Authors Petr Jančar

Publication date 9 April 2013

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1207.2479

zbMATH Keywords

basic process algebrabisimulation equivalencecomplexity

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: Burkart, Caucal, Steffen (1995) showed a procedure deciding bisimulation equivalence of processes in Basic Process Algebra (BPA), i.e. of sequential processes generated by context-free grammars. They improved the previous decidability result of Christensen, H"uttel, Stirling (1992), since their procedure has obviously an elementary time complexity and the authors claim that a close analysis would reveal a double exponential upper bound. Here a self-contained direct proof of the membership in 2-ExpTime is given. This is done via a Prover-Refuter game which shows that there is an alternating Turing machine deciding the problem in exponential space. The proof uses similar ingredients (size-measures, decompositions, bases) as the previous proofs, but one new simplifying factor is an explicit addition of infinite regular strings to the state space. An auxiliary claim also shows an explicit exponential upper bound on the equivalence level of nonbisimilar normed BPA processes. The importance of clarifying the 2-ExpTime upper bound for BPA bisimilarity has recently increased due to the shift of the known lower bound from PSpace (Srba, 2002) to ExpTime (Kiefer, 2012).

Recommendations

• Branching bisimilarity of normed BPA processes is in NExpTime
• Complexity of deciding bisimilarity between normed BPA and normed BPP
• Two lower bounds for BPA
• Normed BPA vs. Normed BPP Revisited
• Deciding bisimilarity of normed context-free processes is in \(\Sigma_ 2^ p\)

Cited in

(11)

• Strong bisimilarity of simple process algebras: Complexity lower bounds
• Bisimilarity on basic parallel processes
• Equivalence of pushdown automata via first-order grammars
• Nested session types
• Bisimulation equivalence and regularity for real-time one-counter automata
• Game characterization of probabilistic bisimilarity, and applications to pushdown automata
• Branching bisimilarity of normed BPA processes is in NExpTime
• Branching bisimilarity on normed BPA is EXPTIME-complete
• Two lower bounds for BPA
• Deciding the bisimilarity of context-free session types
• System \(F^\mu_\omega\) with context-free session types

This page was built for publication: Bisimilarity on basic process algebra is in 2-ExpTime (an explicit proof)

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