An implementation of an efficient algorithm for bisimulation equivalence (Q922711)

The standard bisimulation equivalence test is O(mn) for a labelled transition system with m transitions and n states. \textit{R. Paige} and \textit{R. Tarjan} [SIAM J. Comput. 16, 973-989 (1987; Zbl 0654.68072)] gives an O(m log n) algorithm for the relational coarsest partition problem. The author defines the bisimulation equivalent in terms of the relational coarsest partition problem and modifies the Paige-Tarjan algorithm to be used for bisimulation equivalence.