Lowerbounds for Bisimulation by Partition Refinement
Jan Friso Groote, Jan Martens, Erik. P. de Vink

We provide time lower bounds for sequential and parallel algorithms
deciding bisimulation on labeled transition systems that use partition
refinement. For sequential algorithms this is Omega((m+n)log n) and
for parallel algorithms this is Omega(n), where n is the number of
states and m is the number of transitions. The lowerbounds are
obtained by analysing families of deterministic transition systems,
ultimately with two actions in the sequential case, and one action for
parallel algorithms. For deterministic transition systems with one
action, bisimilarity can be decided sequentially 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 this
approach is not of help to develop a faster generic algorithm for
deciding bisimilarity. For parallel algorithms there is a similar
situation where these techniques may be applied, too.