An Implementation of an Efficient Algorithm for Bisimulation Equivalence

Jean-Claude Fernandez

Science of Computer Programming, volume 13, number 2-3, pages 219-236, May 1990

Abstract:

We 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 & Tarjan in O(mlogn) 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(mlogn) to minimize labeled transition systems modulo bisimulation equivalence. This algorithm has been implemented in C and is used in Aldebaran, a tool for the verification of concurrent systems.

17 pages

PDF

PostScript