A question haunting me for a while is whether the O(m log n) algorithm for strong bisimulation is optimal. We found a family of graphs that shows that any  reasonable partition refinement algorithm is necessarily Omega(n log n), n being the number of states, steps to calculate strong bisimulation.  This appeared to answer the question. But some results from  the literature — digged up by Jan Martens — puts our finding in a strange light. There is a family of graphs for which branching bisimulation can be calculated linearly, but which still is Omega(n log n) when partition refinement is applied. These results need to be understood further, but in extremo this suggests that partition refinement is not such a good idea after all.