Lowerbounds for Bisimulation by Partition Refinement

TL;DR

This paper establishes fundamental time lower bounds for algorithms deciding bisimulation on labeled transition systems, highlighting the limitations of partition refinement methods in both sequential and parallel contexts.

Contribution

It provides tight lower bounds for the complexity of bisimulation algorithms and analyzes the limitations of existing techniques like partition refinement.

Findings

Sequential algorithms have a lower bound of Ω((m + n) log n).

Parallel algorithms have a lower bound of Ω(n).

Existing techniques cannot be improved to surpass these bounds.

Abstract

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 \mkern1mu {+} \mkern1mu n ) \mkern-1mu \log \mkern-1mu 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.