Bisimulation equivalence of a BPP and a finite-state system can be decided in polynomial time

In this paper we consider the problem of deciding bisimulation equivalence of a BPP and a finite-state system. We show that the problem can be solved in polynomial time and we present an algorithm deciding the problem in time O(n⁴). The algorithm also constructs for each state of the finite-state system a ‘symbolic’ semilinear representation of the set of all states of the BPP system which are bisimilar with this state.