Branching Bisimilarity of Normed BPA Processes is in NEXPTIME

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.

arXiv commentThis is the same text as in July 2014, but only with some acknowledgment added due to administrative needs

Cited by in corpus (1)

• A Polynomial Time Algorithm for Deciding Branching Bisimilarity on Totally Normed BPA