Qiang Yin (SJTU)

Branching Bisimulation Regularity Checking on Normed BPA

Bisimulation regularity checking asks whether a system can reach
only finite many states up to a bisimulation equivalence. It has
been proved by Fu that branching bisimulation regularity checking
on normed BPA is decidable but no elementary complexity bound was
given. In this work we prove that this problem is PSPACE-hard and
EXPTIME solvable. The PSPACE-hard lower bound also holds for weak
bisimulation regularity checking. This improves previous NP-hard
lower bound.