Branching Bisimilarity on Normed BPA Is EXPTIME-complete

TL;DR

This paper establishes that deciding branching bisimilarity on normed BPA systems is an EXPTIME-complete problem, providing an exponential-time algorithm and confirming its computational complexity.

Contribution

The paper introduces an exponential-time algorithm for branching bisimilarity on normed BPA and proves its EXPTIME-completeness, resolving a long-standing open problem.

Findings

Decidability of branching bisimilarity on normed BPA is confirmed.

The problem is proven to be EXPTIME-complete.

An exponential-time decision algorithm is provided.

Abstract

We put forward an exponential-time algorithm for deciding branching bisimilarity on normed BPA (Bacis Process Algebra) systems. The decidability of branching (or weak) bisimilarity on normed BPA was once a long standing open problem which was closed by Yuxi Fu. The EXPTIME-hardness is an inference of a slight modification of the reduction presented by Richard Mayr. Our result claims that this problem is EXPTIME-complete.