Explaining Behavioural Inequivalence Generically
in Quasilinear Time

Universal coalgebra [40] provides a generic framework for the modelling and analysis of state-based systems. Its key abstraction is to parametrize notions and results over the transition type of systems, encapsulated as an endofunctor on a given base category. Instances cover, for example, deterministic automata, labelled (weighted) transition systems, and Markov chains.

We briefly review basic concepts of coalgebraic modal logic [38, 42]. Coalgebraic modal logics are parametric in a functor $F$ determining the type of systems underlying the semantics, and additionally in a choice of modalities interpreted in terms of predicate liftings. For now, we use $F=\mathcal{P}$ as a basic example, deferring further examples to section 5.

Before we turn to constructing certificates in coalgebraic generality, we informally recall and extend the Paige-Tarjan algorithm [36], which computes the partition modulo bisimilarity of a given transition system with $n$ states and $m$ transitions in time $\mathcal{O}((m+n)\log n)$. We fix a given finite transition system, viewed as a $\mathcal{P}$-coalgebra $c\colon C\to\mathcal{P}C$.

The algorithm computes two sequences $(C/P_{i})_{i\in\mathbb{N}}$ and $(C/Q_{i})_{i\in\mathbb{N}}$ of partitions of $C$ (with $Q_{i},P_{i}$ equivalence relations), where only the most recent partition is held in memory and $i$ indexes the iterations of the main loop. Throughout the execution, $C/P_{i}$ is finer than $C/Q_{i}$ (that is, $P_{i}\subseteq Q_{i}$ for all $i$), and the algorithm terminates when $P_{i}=Q_{i}$. Intuitively, $P_{i}$ is ‘one transition ahead’ of $Q_{i}$: if $Q_{i}$ distinguishes states $x$ and $y$, then $P_{i}$ is based on distinguishing transitions to $x$ from transitions to $y$.

Initially, $C/Q_{0}:=\{C\}$ consists of only one block and $C/P_{0}$ of two blocks: the live states and the deadlocks (i.e. states with no outgoing transitions). If $P_{i}\subsetneqq Q_{i}$, then there is a block $B\in C/Q_{i}$ that is the union of at least two blocks in $C/P_{i}$. In such a situation, the algorithm chooses $S\subseteq B$ in $C/P_{i}$ to have at most half the size of $B$ and then splits the block $B$ into $S$ and $B\setminus S$ in the partition $C/Q_{i}$:

This is correct because every state in $S$ is already known to be behaviourally inequivalent to every state in $B\setminus S$. By the definition of bisimilarity, this implies that every block $T\in C/P_{i}$ with some transition to $B$ may contain behaviourally inequivalent states as illustrated in Figure 3; that is, $T$ may need to be split into smaller blocks, as follows:

1. (C1)

   states in $T$ with successors in $S$ but not in $B\setminus S$ (e.g. $x_{1}$ in Figure 3),

2. (C2)

   states in $T$ with successors in $S$ and $B\setminus S$ (e.g. $x_{2}$), and

3. (C3)

   states in $T$ with successors $B\setminus S$ but not in $S$ (e.g. $x_{3}$).

The Paige-Tarjan algorithm has been adapted to other system types, e.g. weighted systems [44], and it has recently been generalized to coalgebras [46, 20]. A crucial step in this generalization is to rephrase the case distinction (C1)–(C3) in terms of the functor $\mathcal{P}$: Given a predecessor block $T$ in $C/P_{i}$ for $S\subsetneqq B\in C/Q_{i}$, the three cases distinguish between the equivalence classes $[x]_{\mathcal{P}\chi_{S}^{B}\cdot c}$ for $x\in T$, where the map $\chi_{S}^{B}\colon C\to 3$ in the composite $\mathcal{P}\chi_{S}^{B}\cdot c\colon C\to\mathcal{P}3$ is defined by

Every case is a possible value of $t:=\mathcal{P}\chi_{S}^{B}(c(x))\in\mathcal{P}3$: (C1) $2\in t\not\mkern 1.0mu\ni 1$, (C2) $2\in t\ni 1$, and (C3) $2\notin t\ni 1$. Since $T$ is a predecessor block of $B$, the ‘fourth case’ $2\not\in t\not\mkern 1.0mu\ni 1$ is not possible. There is a transition from $x$ to some state outside of $B$ iff $0\in t$. However, because of the previous refinement steps performed by the algorithm, either all or no states states of $T$ have an edge to $C\setminus B$ (a property called stability [36]), hence no distinction on $0\in t$ is necessary.

It is now easy to generalize from transition systems to coalgebras by simply replacing the functor $\mathcal{P}$ with $F$ in the refinement step. We recall the algorithm:

This algorithm formalizes the intuitive steps from subsection 3.1. Again, two sequences of partitions $P_{1}$, $Q_{i}$ are constructed, and $P_{i}=Q_{i}$ upon termination. Initially, $Q_{0}$ identifies all states and $P_{0}$ distinguishes states by only their output behaviour; e.g. for $F=\mathcal{P}$ and $x\in C$, the value $\mathcal{P}!(c(x))\in\mathcal{P}1$ is $\emptyset$ if $x$ is a deadlock, and $\{1\}$ if $x$ is a live state, and for $FX=2\times X^{A}$, the value $F1(c(x))\in F1=2\times 1^{A}\cong 2$ indicates whether $x$ is a final or non-final state.

In the main loop, blocks $S\in C/P_{i}$ and $B\in C/Q_{i}$ witnessing $P_{i}\subsetneqq Q_{i}$ are picked, and $B$ is split into $S$ and $B\setminus S$, like in the Paige-Tarjan algorithm. Note that step (A2) is equivalent to directly defining the equivalence relation $Q_{i+1}$ as

A similar intersection of equivalence relations is performed in step (A3). The intersection splits every block $T\in C/P_{i}$ into smaller blocks such that $x,x^{\prime}\in T$ end up in the same block iff $F\chi_{S}^{B}(c(x))=F\chi_{S}^{B}(c(x^{\prime}))$, i.e. $T$ is replaced by $\{[x]_{F\chi_{S}^{B}(c(x))}\mid x\in T\}$. Again, this corresponds to the distinction of the three cases (C1)–(C3). For example, for $FX=2\times X^{A}$, there are $|F3|=2\cdot 3^{|A|}$ cases to be distinguished, and so every $T\in C/P_{i}$ is split into at most that many blocks.

The following property of $F$ is needed for correctness [46, Ex. 5.11].

Intuitively, $t\in F(A+B)$ is a term in variables from $A$ and $B$. If $F$ is zippable, then $t$ is uniquely determined by the two elements in $F(A+1)$ and $F(1+B)$ obtained by identifying all $B$- and all $A$-variables with $0\in 1$, respectively. E.g. $FX=X^{2}$ is zippable: $t=(\mathsf{in}_{1}(a),\mathsf{in}_{2}(b))\in(A+B)^{2}$ is uniquely determined by $(\mathsf{in}_{1}(a),\mathsf{in}_{2}(0))\in(A+1)^{2}$ and $(\mathsf{in}_{1}(0),\mathsf{in}_{2}(b))\in(1+B)^{2}$, and similarly for the three other cases of $t$. In fact, all signature functors as well as $\mathcal{P}$ and all monoid-valued functors are zippable. Moreover, the class of zippable functors is closed under products, coproducts, and subfunctors but not under composition, e.g. $\mathcal{P}\mathcal{P}$ is not zippable [46].

The extended Paige-Tarjan algorithm (subsection 3.1) constructs a distinguishing formula according to the three cases (C1)–(C3). In the coalgebraic 3.1, these cases correspond to elements of $F3$, which determine in which block an element of a predecessor block $T$ ends up. Indeed, the elements of $F3$ will also serve as generic modalities in characteristic formulae for blocks of states, essentially by the known equivalence between $n$-ary predicate liftings and (in this case, singleton) subsets of $F(2^{n})$ [42] (termed tests by Klin [30]):

The intended use of ${\ulcorner t\urcorner}$ is as follows: Suppose a block $B$ is split into subblocks $S\subseteq B$ and $B\setminus S$ with certificates $\delta$ and $\beta$, respectively: $\llbracket\delta\rrbracket=S$ and $\llbracket\beta\rrbracket=B$. As in Figure 3, we then split every predecessor block $T$ of $B$ into smaller parts, each of which is uniquely characterized by the formula ${\ulcorner t\urcorner}(\delta,\beta)$ for some $t\in F3$.

In the initial partition $C/P_{0}$ on a transition system $(C,c)$, we used the formulae $\Diamond\top$ and $\neg\Diamond\top$ to distinguish live states and deadlocks. In general, we can similarly describe the initial partition using modalities induced by elements of $F1$:

The $F3$-modalities introduced above (4) induce an instance of coalgebraic modal logic (subsection 2.2). We refer to coalgebraic modal formulae employing the $F3$-modalities as $F3$-modal formulae, and write $\mathcal{M}$ for the set of $F3$-modal formulae. As in the extended Paige-Tarjan algorithm (subsection 3.1), we annotate every block arising during the execution of 3.1 with a certificate in the shape of an $F3$-modal formula. Annotating blocks with formulae means that we construct maps

As in 3.1, $i$ indexes the loop iterations. For blocks $B,S$ in the respective partition, $\beta_{i}(B)$, $\delta_{i}(S)$ denote corresponding certificates: we will have

We construct $\beta_{i}(B)$ and $\delta_{i}(S)$ iteratively, using certificates for the blocks $S\subsetneqq B$ at every iteration:

Like in subsection 3.1, the only block of $C/Q_{0}$ has $\beta_{0}(\{C\})=\top$ as a certificate. Since the partition $C/P_{0}$ distinguishes by the ‘output’ (e.g. final vs. non-final states), the certificate of $[x]_{P_{0}}$ specifies what $F!(c(x))\in F1$ is (3.6).

In the $i$-th iteration of the main loop, we have certificates $\delta_{i}(S)$ and $\beta_{i}(B)$ for $S\subsetneqq B$ in step (A1) satisfying (6) available from the previous iterations. In (A’2), the Boolean connectives describe how $B$ is split into $S$ and $B\setminus S$. In (A’3), new certificates are constructed for every predecessor block $T\in C/P_{i}$ that is refined. If $T$ does not change, then neither does its certificate. Otherwise, the block $T=[x]_{P_{i}}$ is split into the blocks $[x]_{F\chi_{S}^{B}(c(x))}$ for $x\in T$ in step (A3), which is reflected by the $F3$ modality ${\ulcorner F\chi_{S}^{B}(c(x))\urcorner}$ as per 3.4.

The operations introduced by 3.7 can be implemented with only constant run time overhead. To this end, one implements $\beta$ and $\delta$ as arrays of formulae of length $|C|$ (note that at any point, there are at most $|C|$-many blocks). In the refinable-partition data structure [45], every block has an index (a natural number) and there is an array of length $|C|$ mapping every state $x\in C$ to the block it is contained in. Hence, for both partitions $C/P$ and $C/Q$, one can look up a state’s block and a block’s certificate in constant time.

It is very likely that the certificates contain a particular subformula multiple times and that certificates of different blocks share common subformulae. For example, every certificate of a block refined in the $i$-th iteration using $S\subsetneqq B$ contains the subformulas $\delta_{i}(S)$ and $\beta_{i}(B)$. Therefore, it is advantageous to represent all certificates constructed as one directed acyclic graph (dag) with nodes labelled by modal operators and conjunction and having precisely two outgoing edges. Moreover, edges have a binary flag indicating whether they represent negation $\neg$. Initially, there is only one node representing $\top$, and the operations of 3.7 allocate new nodes and update the arrays for $\beta$ and $\delta$ to point to the right nodes. For example, if the predecessor block $T\in C/P_{i}$ is refined in step (A’3), yielding a new block $[x]_{P_{i+1}}$, then a new node labelled $\wedge$ is allocated with edges to the nodes $\delta_{i}(T)$ and to another new node labelled $F\chi_{S}^{B}(c(x))$ with edges to the nodes $\delta_{i}(S)$ and $\delta_{i}(B)$.

For purposes of estimating the size of formulae generated by the algorithm, we use a notion of transition in coalgebras, inspired by the notion of canonical graph [26].