Bisimulation by Partioning is Omega((m+n)log n)
Jan Friso Groote, Jan Martens, and Erik de Vink

An asymptotic lowerbound of Omega((m+n)log n) is established for
partition refinement algorithms that decide bisimilarity on labeled
transition systems. The lowerbound is obtained by subsequently
analysing two families of deterministic transition systems - one
with a growing action set and another with a fixed action set.

For deterministic transition systems with a one-letter action set,
bisimilarity can be decided with fundamentally different techniques
than partition refinement. In particular, Paige, Tarjan, and Bonic
give a linear algorithm for this specific situation. We show,
exploiting the concept of an oracle, that the approach of Paige,
Tarjan, and Bonic is not of help to develop a generic algorithm for
deciding bisimilarity on labeled transition systems that is faster
than the established lowerbound of Omega((m+n)log n).