An implementation of an efficient algorithm for bisimulation equivalence
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.
scientific article; zbMATH DE number 4170103