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

This page has been seen 58 times.

This article's PDF has been downloaded 15 times.