The Complexity of Bisimilarity by Partition Refinement

In order to formally reason about systems and their actions, one can build a mathematical model that represents them. Many specification languages are developed in order to specify complex behaviour. The resulting objects are usually interpreted as Labelled Transition Systems (LTSs). These systems consist of a set of states and a set of (labelled) transitions. The states represent the current situation of a system and all the relevant information. The actions represent any event, that possibly alters the state.

One of the most fundamental notions is that of equality. When are two objects the same? In the case of IT systems a rich theory of behavioural equivalences has arisen. A corner stone in this theory is the notion of bisimilarity.

In this thesis we study theoretical aspects of these behavioural equivalences. We focus on strong bisimulation and branching bisimulation. Branching bisimulation differs from strong bisimulation in that it allows for abstractions in the form of so-called silent transitions. The thesis consists of three parts, `lowerbounds’, `distinguishing formulas’, and `parallel algorithms’.

The first part considers the computational complexity of deciding bisimilarity. We introduce families of LTSs for which we can show that it is impossible to compute strong bisimilarity with a run-time complexity that is smaller than that of the most efficient algorithm both sequentially and in parallel. This lower bound holds for all partition refinement algorithms.

The second part of the thesis studies the computation of witnesses for states that are not bisimulation equivalent. Hennessy-Milner logic contains formulas that express some behaviour. A formula in the Hennessy-Milner logic that is true in only one of two states explains behaviour that distinguishes them, thereby witnessing bisimulation inequivalence. In our contribution we show that it is NP-hard to compute a minimal distinguishing formula. Additionally, we introduce show that for different metrics, such as minimal depth and minimal negation-depth, this is not the case. We introduce polynomial-time algorithms to compute minimal distinguishing formulas with respect to these metrics that witness inequivalence with respect to branching and strong bisimilarity.

In the third part of this thesis we study parallel algorithms that decide bisimulation relations. For strong and branching bisimilarity we introduce a parallel algorithm that runs in linear parallel time on a theoretical parallel model. We also show a parallel implementation that computes strong bisimilarity using Graphical Processing Units (GPUs). These devices approach the theoretical parallel model. Lastly, we also study the implementations of parallel algorithms deciding bisimilarity on deterministic transition systems on GPUs. We show that the theoretically fastest parallel algorithm is not feasible in its current form. The generic partition refinement algorithm, that also works for non-deterministic structures, performs much better.