Branching Bisimilarity of Normed BPA Processes Is in NEXPTIME

Branching bisimilarity of nor med Basic Process Algebra (BPA) processes was 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. We also derive that semantic finiteness (the question if a given nor med BPA process is branching bisimilar with some finite-state process) belongs to NExpTime as well.