Jancar, Petr - Bisimilarity on Basic Process Algebra is in 2-ExpTime (an explicit proof)

lmcs:873 - Logical Methods in Computer Science, March 13, 2013, Volume 9, Issue 1
Bisimilarity on Basic Process Algebra is in 2-ExpTime (an explicit proof)

Authors: Jancar, Petr

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).

Source : oai:arXiv.org:1207.2479
DOI : 10.2168/LMCS-9(1:10)2013
Volume: Volume 9, Issue 1
Published on: March 13, 2013
Submitted on: July 9, 2012
Keywords: Computer Science - Logic in Computer Science,Computer Science - Formal Languages and Automata Theory,F.4.2,F.3.2


Consultation statistics

This page has been seen 50 times.
This article's PDF has been downloaded 11 times.