Branching bisimilarity between finite-state systems and BPA or normed BPP is polynomial-time decidable

Abstract

In this paper we present polynomial time algorithms deciding branching bisimilarity between finite-state systems and several classes of infinite-state systems: BPA and normed BPP. The algorithm for BPA improves a previous one given by Kučera and Mayr, while the one for normed BPP demonstrates the polynomial-time decidability of the problem, which is unknown previously. The proof style follows an early work of Kučera and Mayr, where similar results for weak bisimilarity are established. © 2009 Springer-Verlag.