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

TL;DR

This paper presents the first polynomial-time algorithm for deciding branching bisimilarity on totally normed BPA systems, expanding the understanding of complexity differences between bisimilarity notions in infinite state systems.

Contribution

It introduces a novel polynomial-time algorithm for branching bisimilarity on totally normed BPA, with a unique correctness proof and a generalized partition refinement approach.

Findings

Decides branching bisimilarity in polynomial time for totally normed BPA.

First known polynomial-time algorithm for bisimilarity with silent transitions in infinite state systems.

Highlights the complexity distinction between branching and weak bisimilarity.

Abstract

Strong bisimilarity on normed BPA is polynomial-time decidable, while weak bisimilarity on totally normed BPA is NP-hard. It is natural to ask where the computational complexity of branching bisimilarity on totally normed BPA lies. This paper confirms that this problem is polynomial-time decidable. To our knowledge, in the presence of silent transitions, this is the first bisimilarity checking algorithm on infinite state systems which runs in polynomial time. This result spots an instance in which branching bisimilarity and weak bisimilarity are both decidable but lie in different complexity classes (unless NP=P), which is not known before. The algorithm takes the partition refinement approach and the final implementation can be thought of as a generalization of the previous algorithm of Czerwi\'{n}ski and Lasota. However, unexpectedly, the correctness of the algorithm cannot be directly generalized from previous works, and the correctness proof turns out to be subtle. The proof depends on the existence of a carefully defined refinement operation fitted for our algorithm and the proposal of elaborately developed techniques, which are quite different from previous works.