Branching Bisimilarity of Normed BPA Processes is in NEXPTIME

TL;DR

This paper introduces a simpler nondeterministic exponential-time algorithm for deciding branching bisimilarity on normed BPA processes, establishing its complexity bounds close to the theoretical lower limit.

Contribution

It provides a new, simpler approach using relative prime decompositions to determine the complexity of branching bisimilarity for normed BPA processes.

Findings

Decidability of branching bisimilarity with an NEXPTIME algorithm

Algorithm complexity is close to the exponential-time lower bound

Simplifies previous proofs of decidability

Abstract

Branching bisimilarity on normed BPA processes was recently shown to be decidable by Yuxi Fu (ICALP 2013) but his proof has not provided any upper complexity bound. We present a simpler approach based on relative prime decompositions that leads to a nondeterministic exponential-time algorithm; this is close to the known exponential-time lower bound.