Branching Bisimilarity between Finite-State Systems and BPA or Normed BPP Is Polynomial-Time Decidable

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ˇcera 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ˇcera and Mayr, where similar results for weak bisimilarity are established.

• Type: Conference
• Year: 2009
• Where: APLAS
• Authors: Hongfei Fu
• Keywords: APLAS 2009, Normed Bpp, Polynomial Time Algorithms, Polynomial-time Decidability