An implementation of an efficient algorithm for bisimulation equivalence

AbstractWe present an efficient algorithm for bisimulation equivalence. Generally, bisimulation equivalence can be tested in O(mn) for a labeled transition system with m transitions and n states. In order to come up with a more efficient algorithm, we establish a relationship between bisimulation equivalence and the relational coarsest partition problem, solved by Paige and Tarjan in O(m log n) time. Given an initial partition and a binary relation, the problem is to find the coarsest partition compatible with them. Computing bisimulation equivalence can be viewed both as an instance and as a generalization of this problem: an instance, because only the universal partition is considered as an initial partition and a generalization since we want to find a partition compatible with a family of binary relations instead of one single binary relation. We describe how we have adapted the Paige-Tarjan algorithm of complexity O(m log n) to minimize labeled transition systems modulo bisimulation equivalence. This algorithm has been implemented in C and is used in Aldébaran, a tool for the verification of concurrent systems