An efficient algorithm for computing bisimulation equivalence

摘要

We propose an efficient algorithmic solution to the problem of determining a Bisimulation Relation on a finite structure working both on the explicit and on the implicit (symbolic) representation. As far as the explicit case is concerned, starting from a set-theoretic point of view we propose an algorithm that optimizes the solution to the Relational Coarsest Partition Problem given by Paige and Tarjan (SIAM J. Comput. 16(6) (1987) 973); its use in model-checking packages is also discussed and tested. For well-structured graphs our algorithm reaches a linear worst-case behaviour. The proposed algorithm is then re-elaborated to produce a symbolic version.