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

TL;DR

This paper provides a clear, self-contained proof that bisimilarity in Basic Process Algebra can be decided within double exponential time, using a Prover-Refuter game and explicit bounds, clarifying its computational complexity.

Contribution

It offers an explicit 2-ExpTime upper bound proof for BPA bisimilarity using a novel game-based approach with infinite regular strings included.

Findings

Bisimilarity in BPA is in 2-ExpTime complexity.

An explicit exponential upper bound on equivalence levels is established.

A Prover-Refuter game demonstrates the decision procedure within exponential space.

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