A State-Based O(m log n) Partitioning Algorithm for Branching Bisimilarity

As the first step of the algorithm the LTS is preprocessed to contract each $\tau$-strongly connected component (SCC) into a single state. This step is valid since all states in a $\tau$-SCC are branching bisimilar. For divergence-preserving branching bisimilarity, the $\tau$-self-loops are replaced by a special non-internal action. In both cases, $\tau$-self-loops can be suppressed and therefore, from this point onwards, as the algorithm does not change the structure of the LTS further, all $\tau$-paths in the LTS are finite, formalised by the following lemma.

In every set of states $B\subseteq S$, the states without $\tau$-transition to another state in $B$ are called bottom states. The set of bottom states in $B$ is denoted by $\mathrm{𝐵𝑜𝑡𝑡𝑜𝑚}(B)$. Lemma 3.1 implies the following lemma:

The algorithm is a partition refinement algorithm of sets of states where two partitions of states are iteratively refined.

A partition induces an equivalence relation in the following way: $s{\equiv }_{𝒫}t$ iff there is some $B\in 𝒫$ containing both $s$ and $t$. We call a transition $𝒫$-inert iff it is ${\equiv }_{𝒫}$-inert, i.e., exactly if it is a transition $s\stackrel{𝜏}{\to }t$ with $s,t\in P$ for some $P\in 𝒫$.

Our algorithm uses two partitions $ℬ$ and $𝒞$ of states. The main partition $ℬ$ contains blocks, typically denoted with the letter $B$, recording the current knowledge about branching bisimilarity. Two states are in different blocks iff the algorithm has found a proof that they are not branching bisimilar, formulated contrapositionally by the following invariant:

We desire to make the partition $ℬ$ “stable” in the sense that blocks of $ℬ$ cannot be split further as all states in each block are branching bisimilar. This notion of stability is defined as follows. Consider two sets of states $B,B^{\prime }\subseteq S$. We say that two states $s,t\in B$ are stable under $B^{\prime }$ iff if $s\stackrel{𝑎}{\to }{s}^{\prime }$ for any $s^{\prime }\in B^{\prime }$ then

• $\mathrm{■}$

  either $B=B^{\prime }$ and $a=\tau$,

• $\mathrm{■}$

  or there are $t_1,\mathrm{\dots },t_k\in B$ and $t^{\prime }\in B^{\prime }$ such that $t=t_1$, $k\ge 1$ and $t_1\stackrel{𝜏}{\to }\mathrm{\cdots }\stackrel{𝜏}{\to }{t}_k\stackrel{𝑎}{\to }{t}^{\prime }$.

A partition $ℬ$ of $S$ is stable under a set of states $B^{\prime }\subseteq S$ iff for all $B\in ℬ$ and $s,t\in B$ it holds that $s$ and $t$ are stable under $B^{\prime }$. If $ℬ$ is stable under every $B\in ℬ$ we say that $ℬ$ is stable.

An important property is that if a partition $ℬ$ is stable, then the induced equivalence relation ${\equiv }_{ℬ}$ is a branching bisimulation.

In order to remember which instabilities have already been resolved we introduce a second partition $𝒞$ of the set of states $S$ of which $ℬ$ is a refinement. We call the blocks in $𝒞$ constellations and we typically denote constellations with the letter $C$.

The partition $𝒞$ records the current knowledge about stability by guaranteeing that $ℬ$ is always stable under each constellation $C\in 𝒞$. Using Lemma 3.2 this follows from the following invariant.

The goal of the algorithm is to let the partition of constellations $𝒞$ and the partition of blocks $ℬ$ coincide. If $ℬ=𝒞$, then $ℬ$ is stable, and, using Invariants 3.4 and 3.5, the partition $ℬ$ exactly characterises branching bisimulation. As this is the core purpose of our algorithm, we formulate it as a theorem, although the proof is straightforward.

The main idea of the algorithm is to refine $𝒞$ until it coincides with $ℬ$. After refining $𝒞$, one may have to refine $ℬ$ to reestablish Invariant 3.5. For this to work, we use two essential subroutines, namely $\text{four-way-split}ℬ$ (Algorithm 2) and $\mathrm{𝗌𝗍𝖺𝖻𝗂𝗅𝗂𝗌𝖾}ℬ$ (Algorithm 3). We first give a summary of what these functions do, after which we explain the overall algorithm. In Sections 4 and 5 their underlying algorithms are explained.

The function $\text{four-way-split}ℬ(B,\text{SmallSp},\text{LargeSp})$ splits a block $B$ in $ℬ$ in at most four sub-blocks based on two disjoint sets of transitions SmallSp and LargeSp that start in $B$. We require that at least one of these two sets is non-empty. If both are non-empty, every state in $B$ can $ℬ$-inertly reach a transition in at least one of the two. The four sub-blocks are the following:

$\mathrm{𝖠𝗏𝗈𝗂𝖽𝖫𝗋𝗀}$:

If $\mathrm{𝐿𝑎𝑟𝑔𝑒𝑆𝑝}\ne \mathrm{\varnothing }$, $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖫𝗋𝗀}$ contains the states in $B$ that cannot $ℬ$-inertly reach $\mathrm{𝐿𝑎𝑟𝑔𝑒𝑆𝑝}$. If $\mathrm{𝐿𝑎𝑟𝑔𝑒𝑆𝑝}=\mathrm{\varnothing }$, then $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖫𝗋𝗀}=\mathrm{\varnothing }$.

$\mathrm{𝖠𝗏𝗈𝗂𝖽𝖲𝗆𝗅}$:

If $\mathrm{𝑆𝑚𝑎𝑙𝑙𝑆𝑝}\ne \mathrm{\varnothing }$, $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖲𝗆𝗅}$ contains the states in $B$ that cannot $ℬ$-inertly reach $\mathrm{𝑆𝑚𝑎𝑙𝑙𝑆𝑝}$. If $\mathrm{𝑆𝑚𝑎𝑙𝑙𝑆𝑝}=\mathrm{\varnothing }$, then $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖲𝗆𝗅}=\mathrm{\varnothing }$.

$\mathrm{𝖱𝖾𝖺𝖼𝗁𝖠𝗅𝗐}$:

states in $B$ that can always $ℬ$-inertly reach both splitters $\mathrm{𝑆𝑚𝑎𝑙𝑙𝑆𝑝}$ and $\mathrm{𝐿𝑎𝑟𝑔𝑒𝑆𝑝}$ if both are non-empty. Otherwise, $\mathrm{𝖱𝖾𝖺𝖼𝗁𝖠𝗅𝗐}$ consists of states in $B$ that can always $ℬ$-inertly reach the non-empty splitter. “Always …reach” here also means: if a $ℬ$-inert transition starts in such a state, its target state, which is in $B$, must also be in $\mathrm{𝖱𝖾𝖺𝖼𝗁𝖠𝗅𝗐}$.

$\mathrm{𝖭𝖾𝗐𝖡𝗈𝗍𝖲𝗍}$:

states in $B$ that do not fit in any of the three sets above. Original bottom states cannot end up in $\mathrm{𝖭𝖾𝗐𝖡𝗈𝗍𝖲𝗍}$, and new bottom states will always end up in this sub-block.

Figure 1 contains two examples of how a block $B^{\prime }$ is split. Here unlabelled transitions are $ℬ$-inert transitions in $B^{\prime }$. The next lemma expresses that new bottom states end up in $\mathrm{𝖭𝖾𝗐𝖡𝗈𝗍𝖲𝗍}$ and Invariant 3.4 is preserved under the four-way-split.

1. 1.

   We use contraposition. Assume that $s\in \mathrm{𝐵𝑜𝑡𝑡𝑜𝑚}(B)$. Then $s$ does not have an outgoing $ℬ$-inert transition. By construction $s$ ends up in one of the sets $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖲𝗆𝗅}$, $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖫𝗋𝗀}$ and $\mathrm{𝖱𝖾𝖺𝖼𝗁𝖠𝗅𝗐}$. Hence, $s\notin \mathrm{𝖭𝖾𝗐𝖡𝗈𝗍𝖲𝗍}$.

2. 2.

   This follows by observing that if there is a bottom state $s\in B_s$ where $B_s$ is any of the blocks $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖫𝗋𝗀}$, $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖲𝗆𝗅}$ and $\mathrm{𝖱𝖾𝖺𝖼𝗁𝖠𝗅𝗐}$ which was not a bottom state in $B$, then there is transition $s\stackrel{𝜏}{\to }{s}^{\prime }$ with $s^{\prime }\in B$ but $s^{\prime }\notin B_s$. Going through the various cases, it follows that $s$ cannot be in any of the three sets $B_s$, and therefore must be part of $\mathrm{𝖭𝖾𝗐𝖡𝗈𝗍𝖲𝗍}$.

3. 3.

   Using that Invariant 3.4 is valid for $ℬ$, we only need to show that two states $s,t\in B$ that have been moved to different blocks in ${ℬ}^{\prime }$ are not branching bisimilar.

   Assume $s\in \mathrm{𝖱𝖾𝖺𝖼𝗁𝖠𝗅𝗐}$ and $t\in \mathrm{𝖠𝗏𝗈𝗂𝖽𝖲𝗆𝗅}$. Then $s$ can $ℬ$-inertly reach $\mathrm{𝑆𝑚𝑎𝑙𝑙𝑆𝑝}$. This means, using the invariant and the conditions of this lemma, it can reach a non-${\underset{¯}{\leftrightarrow }}_b$-inert transition in $\mathrm{𝑆𝑚𝑎𝑙𝑙𝑆𝑝}$. As $t\in \mathrm{𝖠𝗏𝗈𝗂𝖽𝖲𝗆𝗅}$, $t$ cannot mimic this transition, and hence $s{\mathrm{／}\underset{¯}{\leftrightarrow }}_{b}t$. More concretely, all states in $\mathrm{𝖱𝖾𝖺𝖼𝗁𝖠𝗅𝗐}$ and $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖲𝗆𝗅}$ are not branching bisimilar. Similarly, one proves that the states in $\mathrm{𝖱𝖾𝖺𝖼𝗁𝖠𝗅𝗐}$ and $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖫𝗋𝗀}$, respectively, the states in $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖲𝗆𝗅}$ and $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖫𝗋𝗀}$ are not branching bisimilar.

   Now assume $s\in \mathrm{𝖭𝖾𝗐𝖡𝗈𝗍𝖲𝗍}$. We claim that $s$ can $ℬ$-inertly reach both $\mathrm{𝑆𝑚𝑎𝑙𝑙𝑆𝑝}$ and $\mathrm{𝐿𝑎𝑟𝑔𝑒𝑆𝑝}$ unless they are empty, and $s$ can $ℬ$-inertly reach $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖲𝗆𝗅}$ or $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖫𝗋𝗀}$. This can be seen as follows. If $s\in B$ can $ℬ$-inertly reach $\mathrm{𝑆𝑚𝑎𝑙𝑙𝑆𝑝}$ but not $\mathrm{𝐿𝑎𝑟𝑔𝑒𝑆𝑝}$ (and $\mathrm{𝐿𝑎𝑟𝑔𝑒𝑆𝑝}\ne \mathrm{\varnothing }$), then $s\in \mathrm{𝖠𝗏𝗈𝗂𝖽𝖫𝗋𝗀}$. Similarly, if $s\in B$ can $ℬ$-inertly reach $\mathrm{𝐿𝑎𝑟𝑔𝑒𝑆𝑝}$ but not $\mathrm{𝑆𝑚𝑎𝑙𝑙𝑆𝑝}$ (and $\mathrm{𝑆𝑚𝑎𝑙𝑙𝑆𝑝}\ne \mathrm{\varnothing }$), then $s\in \mathrm{𝖠𝗏𝗈𝗂𝖽𝖲𝗆𝗅}$. So, $s$ can reach all non-empty splitters. As $s\notin \mathrm{𝖱𝖾𝖺𝖼𝗁𝖠𝗅𝗐}$, it can $ℬ$-inertly reach a bottom state $s^{\prime }\in \mathrm{𝐵𝑜𝑡𝑡𝑜𝑚}(B)\setminus \mathrm{𝖱𝖾𝖺𝖼𝗁𝖠𝗅𝗐}$. As $s^{\prime }\notin \mathrm{𝖭𝖾𝗐𝖡𝗈𝗍𝖲𝗍}$ (by dictum 1), we have $s^{\prime }\in \mathrm{𝖠𝗏𝗈𝗂𝖽𝖲𝗆𝗅}$ or $s^{\prime }\in \mathrm{𝖠𝗏𝗈𝗂𝖽𝖫𝗋𝗀}$.

   If $t\in \mathrm{𝖠𝗏𝗈𝗂𝖽𝖲𝗆𝗅}$ or $t\in \mathrm{𝖠𝗏𝗈𝗂𝖽𝖫𝗋𝗀}$, then $s$ can $ℬ$-inertly reach a non-${\underset{¯}{\leftrightarrow }}_b$-inert transition in $\mathrm{𝑆𝑚𝑎𝑙𝑙𝑆𝑝}$ or $\mathrm{𝐿𝑎𝑟𝑔𝑒𝑆𝑝}$, respectively, that $t$ cannot mimic.

   Now consider $t\in \mathrm{𝖱𝖾𝖺𝖼𝗁𝖠𝗅𝗐}$. We know that $s$ can $ℬ$-inertly reach a state $s^{\prime }\in \mathrm{𝖠𝗏𝗈𝗂𝖽𝖲𝗆𝗅}\cup \mathrm{𝖠𝗏𝗈𝗂𝖽𝖫𝗋𝗀}$, and as argued above $t{\mathrm{／}\underset{¯}{\leftrightarrow }}_b{s}^{\prime }$. Suppose we can find a state $t^{\prime }$ reachable with internal transitions from $t$ that mimics the path from $s$ to $s^{\prime }$ such that $t^{\prime }{\underset{¯}{\leftrightarrow }}_b{s}^{\prime }$. Using Invariant 3.4 for $ℬ$, $t^{\prime }$ must be $ℬ$-inertly reachable and $t^{\prime }\in B$. But then $t^{\prime }\in \mathrm{𝖱𝖾𝖺𝖼𝗁𝖠𝗅𝗐}$ and $s^{\prime }{\mathrm{／}\underset{¯}{\leftrightarrow }}_b{t}^{\prime }$. So, no such $t^{\prime }$ exists, and hence $s{\mathrm{／}\underset{¯}{\leftrightarrow }}_{b}t$.

$◀$ The following lemma explains which calls to $\text{four-way-split}ℬ$ are needed to reestablish Invariant 3.5 after splitting a constellation $C\in 𝒞\setminus ℬ$. For now we exclude blocks that contain new bottom states, i.e. sub-blocks of $\mathrm{𝖭𝖾𝗐𝖡𝗈𝗍𝖲𝗍}$, cf., Lemma 3.7.1 and 3.7.2.

Consider a state $s\in \widehat{B}$ for any block $\widehat{B}\in {ℬ}^{\prime }$ not refining any $\mathrm{𝖭𝖾𝗐𝖡𝗈𝗍𝖲𝗍}$. Assume that a non-${𝒞}^{\prime }$-inert transition $s\stackrel{𝑎}{\to }t$ exists with $t\in \widehat{C}$ for some constellation $\widehat{C}\in {𝒞}^{\prime }$. So, $a\ne \tau$ or $s\notin \widehat{C}$. We must prove that any $s^{\prime }\in \mathrm{𝐵𝑜𝑡𝑡𝑜𝑚}(\widehat{B})$ has a transition $s^{\prime }\stackrel{𝑎}{\to }{t}^{\prime }$ with $t^{\prime }\in \widehat{C}$.

Let ${\widehat{B}}^{\prime }$ be the block $\widehat{B}\subseteq {\widehat{B}}^{\prime }\in ℬ$. Note that $s^{\prime }\in \mathrm{𝐵𝑜𝑡𝑡𝑜𝑚}({\widehat{B}}^{\prime })$ by Lemma 3.7.2.

Case $\widehat{C}⊈C$:

That means that $\widehat{C}\in 𝒞$. Using Invariant 3.5 (for ${\widehat{B}}^{\prime }\in ℬ$ and $\widehat{C}\in 𝒞$), $s^{\prime }$ has a transition $s^{\prime }\stackrel{𝑎}{\to }{t}^{\prime }$ with $t^{\prime }\in \widehat{C}$.

Case $\widehat{B}\subseteq C$, $a=\tau$ and $\widehat{C}=B$:

If $\widehat{B}\subseteq B={\widehat{B}}^{\prime }$, then $s\stackrel{𝜏}{\to }t$ were ${𝒞}^{\prime }$-inert. So, we can assume $\widehat{B}\subseteq C\setminus B$. There is a block ${\widehat{B}}^{\prime \prime }$ with $\widehat{B}\subseteq {\widehat{B}}^{\prime \prime }\subseteq {\widehat{B}}^{\prime }$ such that a call

$$\text{four-way-split}ℬ({\widehat{B}}^{\prime \prime },{\widehat{B}}^{\prime \prime }\stackrel{𝜏}{\to }B,\mathrm{\varnothing })$$

must have taken place. In this case $\widehat{B}$ is a sub-block of $\mathrm{𝖱𝖾𝖺𝖼𝗁𝖠𝗅𝗐}$ or $\mathrm{𝖭𝖾𝗐𝖡𝗈𝗍𝖲𝗍}$. In the last case there is nothing to check. But $\widehat{B}\subseteq \mathrm{𝖱𝖾𝖺𝖼𝗁𝖠𝗅𝗐}$ implies that $s^{\prime }\in \mathrm{𝐵𝑜𝑡𝑡𝑜𝑚}(\widehat{B})$ has a transition $s^{\prime }\stackrel{𝜏}{\to }{t}^{\prime }$ with $t^{\prime }\in B$, as had to be shown.

Case ($\widehat{B}⊈C$ or $a\ne \tau$) and $\widehat{C}=B$:

If $(\widehat{B}\stackrel{𝑎}{\to }C\setminus B)=\mathrm{\varnothing }$, we know by Invariant 3.5 (for ${\widehat{B}}^{\prime }\in ℬ$ and $C\in 𝒞$) that $s^{\prime }\in \mathrm{𝐵𝑜𝑡𝑡𝑜𝑚}(\widehat{B})$ has a transition $s^{\prime }\stackrel{𝑎}{\to }{t}^{\prime }$ with $t^{\prime }\in C$, and as the transition cannot go to $C\setminus B$, it must go to $B$, which we had to prove.

Otherwise, $(\widehat{B}\stackrel{𝑎}{\to }C\setminus B)\ne \mathrm{\varnothing }$, and there is a block ${\widehat{B}}^{\prime \prime }$ with $\widehat{B}\subseteq {\widehat{B}}^{\prime \prime }\subseteq {\widehat{B}}^{\prime }$ for which a call

$$\text{four-way-split}ℬ({\widehat{B}}^{\prime \prime },{\widehat{B}}^{\prime \prime }\stackrel{𝑎}{\to }B,{\widehat{B}}^{\prime \prime }\stackrel{𝑎}{\to }C\setminus B)$$

took place with $\widehat{B}$ a sub-block of $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖫𝗋𝗀}$, $\mathrm{𝖱𝖾𝖺𝖼𝗁𝖠𝗅𝗐}$ or $\mathrm{𝖭𝖾𝗐𝖡𝗈𝗍𝖲𝗍}$. The last case does not lead to a proof obligation. But $\widehat{B}\subseteq \mathrm{𝖠𝗏𝗈𝗂𝖽𝖫𝗋𝗀}$ or $\widehat{B}\subseteq \mathrm{𝖱𝖾𝖺𝖼𝗁𝖠𝗅𝗐}$ implies that $s^{\prime }\in \mathrm{𝐵𝑜𝑡𝑡𝑜𝑚}(\widehat{B})$ has a transition $s^{\prime }\stackrel{𝑎}{\to }{t}^{\prime }$ with $t^{\prime }\in B$, as had to be shown.

Case $\widehat{B}\subseteq C$, $a=\tau$ and $\widehat{C}=C\setminus B$:

If $\widehat{B}\subseteq C\setminus B$, then $s\stackrel{𝜏}{\to }t$ were ${𝒞}^{\prime }$-inert. So we can assume $\widehat{B}\subseteq B={\widehat{B}}^{\prime }$. There is a block ${\widehat{B}}^{\prime \prime }$ with $\widehat{B}\subseteq {\widehat{B}}^{\prime \prime }\subseteq B$ such that a call

$$\text{four-way-split}ℬ({\widehat{B}}^{\prime \prime },{\widehat{B}}^{\prime \prime }\stackrel{𝜏}{\to }C\setminus B,\mathrm{\varnothing })$$

must have taken place, where $\widehat{B}$ is a sub-block of $\mathrm{𝖱𝖾𝖺𝖼𝗁𝖠𝗅𝗐}$ or $\mathrm{𝖭𝖾𝗐𝖡𝗈𝗍𝖲𝗍}$. The latter case is not interesting. Again, $\widehat{B}\subseteq \mathrm{𝖱𝖾𝖺𝖼𝗁𝖠𝗅𝗐}$ implies that $s^{\prime }\in \mathrm{𝐵𝑜𝑡𝑡𝑜𝑚}(\widehat{B})$ has a transition $s^{\prime }\stackrel{𝜏}{\to }{t}^{\prime }$ with $t^{\prime }\in C\setminus B$, as had to be shown.

Case ($\widehat{B}⊈C$ or $a=\tau$) and $\widehat{C}=C\setminus B$:

If $(\widehat{B}\stackrel{𝑎}{\to }B)=\mathrm{\varnothing }$, we know by Invariant 3.5 (for ${\widehat{B}}^{\prime }\in ℬ$ and $C\in 𝒞$) that $s^{\prime }\in \mathrm{𝐵𝑜𝑡𝑡𝑜𝑚}(\widehat{B})$ has a transition $s^{\prime }\stackrel{𝑎}{\to }{t}^{\prime }$ with $t^{\prime }\in C$, and as the transition cannot go to $B$, it must go to $C\setminus B$, which we had to prove.

Otherwise, $(\widehat{B}\stackrel{𝑎}{\to }B)\ne \mathrm{\varnothing }$, and there is a block ${\widehat{B}}^{\prime \prime }$ such that $\widehat{B}\subseteq {\widehat{B}}^{\prime \prime }\subseteq {\widehat{B}}^{\prime }$ and a call

$$\text{four-way-split}ℬ({\widehat{B}}^{\prime \prime },{\widehat{B}}^{\prime \prime }\stackrel{𝑎}{\to }B,{\widehat{B}}^{\prime \prime }\stackrel{𝑎}{\to }C\setminus B)$$

must have taken place, and $\widehat{B}$ is a subset of $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖲𝗆𝗅}$ or $\mathrm{𝖱𝖾𝖺𝖼𝗁𝖠𝗅𝗐}$ or $\mathrm{𝖭𝖾𝗐𝖡𝗈𝗍𝖲𝗍}$. We can ignore the latter case. But $\widehat{B}\subseteq \mathrm{𝖠𝗏𝗈𝗂𝖽𝖲𝗆𝗅}$ or $\widehat{B}\subseteq \mathrm{𝖱𝖾𝖺𝖼𝗁𝖠𝗅𝗐}$ implies that $s^{\prime }\in \mathrm{𝐵𝑜𝑡𝑡𝑜𝑚}(\widehat{B})$ has a transition $s^{\prime }\stackrel{𝑎}{\to }{t}^{\prime }$ with $t^{\prime }\in C\setminus B$, as had to be shown.

$◀$ Blocks with new bottom states, which were excluded by Lemma 3.8, are handled by the function $\mathrm{𝗌𝗍𝖺𝖻𝗂𝗅𝗂𝗌𝖾}ℬ$. It assumes that blocks without new bottom states are already stable and stabilises the blocks with new bottom states, which concretely means that it refines them under all their outgoing non-$𝒞$-inert transitions such that for the resulting partition Invariant 3.5 holds, while maintaining Invariant 3.4.

We are now in the situation to explain Algorithm 1. First we need to take care that the Invariants 3.4 and 3.5 become valid. Therefore, in line 1.2 we set the partition $ℬ$ and the set of constellations $𝒞$ to $\{S\}$. This makes Invariant 3.4 trivially true.

If a block $B$ has new bottom states, we use the predicate $has\mathrm{\_}new\mathrm{\_}bottom\mathrm{\_}states(B)$ to indicate so. This is not only the case when block $B$ is a refinement of some block $\mathrm{𝖭𝖾𝗐𝖡𝗈𝗍𝖲𝗍}$ but it also applies to the initial block, and this is explicitly indicated in line 1.2. Invariant 3.5 is now made valid by one call to $\mathrm{𝗌𝗍𝖺𝖻𝗂𝗅𝗂𝗌𝖾}ℬ$ in line 1.3. Concretely, this call splits $\{S\}$ into a partition $ℬ$ such that all bottom states in each block $B$ in $ℬ$ have exactly the same outgoing non-$ℬ$-inert actions, while keeping branching bisimilar states in the same block.

As stated above, the purpose of the main algorithm is to refine $𝒞$ such that it ultimately coincides with $ℬ$. This happens in the loop starting at line 1.4. If $ℬ$ and $𝒞$ do not coincide, there is at least one block $B\subseteq C$ with size smaller than or equal to $\frac{1}{2}\left|C\right|$. We replace the constellation $C$ in $𝒞$ by two new constellations $B$ and $C\setminus B$ (line 1.6).

Our main task is to make Invariant 3.5 valid again. This is done by taking care that all calls to $\text{four-way-split}ℬ$ as required by Lemma 3.8 are performed. This guarantees that Invariant 3.5 is valid except for blocks of the form $\mathrm{𝖭𝖾𝗐𝖡𝗈𝗍𝖲𝗍}$. Therefore, one extra call is needed to $\mathrm{𝗌𝗍𝖺𝖻𝗂𝗅𝗂𝗌𝖾}ℬ$ in line 1.19.

In order to effectively carry out the four-way-splits, transitions are organised in block-label-constellation sets (BLC sets). Every BLC set contains the transitions $B\stackrel{𝑎}{\to }C$ for a specific block $B\in ℬ$, action $a\in \mathrm{𝐴𝑐𝑡}$, and constellation $C\in 𝒞$. Whenever a constellation or a block is split (lines 1.6 and 2.45) these BLC sets are updated.

In line 1.8 there is a call to $\text{four-way-split}ℬ(B,B\stackrel{𝜏}{\to }(C\setminus B),\mathrm{\varnothing })$ that corresponds with the third case in Lemma 3.8. So, that case has been covered.

For the remainder we put all non-$𝒞$-inert transitions to block $B$ in a set $ℳ$. By traversing the BLC sets in $ℳ$ the other required calls to four-way split are done. In line 1.5 such a BLC set $\mathrm{𝑆𝑚𝑎𝑙𝑙𝑆𝑝}=B^{\prime }\stackrel{𝑎}{\to }B$ for some block $B^{\prime }$ is selected. For the complexity, it is important that as this implies that the selected BLC set is small, hence its name.

If $B^{\prime }$ has only one state or is a refinement of some block $\mathrm{𝖭𝖾𝗐𝖡𝗈𝗍𝖲𝗍}$ and hence has new bottom states, according to Lemma 3.8 it does not need to be considered to be split (line 1.12).

Otherwise, there are two situations. The first one is when $a=\tau$ and $B^{\prime }$ was part of the constellation $C$ (line 1.13). As $ℳ$ does not contain $\tau$-transitions from $B$ to $B$, this means $B^{\prime }\in C\setminus B$ and the required second call $\text{four-way-split}ℬ(B^{\prime },\mathrm{𝑆𝑚𝑎𝑙𝑙𝑆𝑝},\mathrm{\varnothing })$ in Lemma 3.8 is made. The other situation, i.e., the else part at lines 1.15–1.18, exactly satisfies the conditions of the first mentioned call to four-way-split in Lemma 3.8. As the algorithm traverses all BLC sets that are part of $ℳ$, the whole set $S$ is covered as required in Lemma 3.8.

From Lemma 3.8 it follows that at line 1.19 of the algorithm, Invariant 3.5 holds for all blocks, except for those that are of the shape $\mathrm{𝖭𝖾𝗐𝖡𝗈𝗍𝖲𝗍}$. As stated above one call to $\mathrm{𝗌𝗍𝖺𝖻𝗂𝗅𝗂𝗌𝖾}ℬ$ is sufficient to restore Invariant 3.5 for all blocks. Just for the record, Invariant 3.4 remains valid, as each call to $\text{four-way-split}ℬ$ preserves it (see Lemma 3.7.3), and, as explained in Section 5, $\mathrm{𝗌𝗍𝖺𝖻𝗂𝗅𝗂𝗌𝖾}ℬ$ refines $ℬ$ only using $\text{four-way-split}ℬ$ also.

This means that at line 1.4 of Algorithm 1 both invariants hold. If the condition of the while is not valid, the partitions $ℬ$ and $𝒞$ are equal, and as argued above, these resulting partitions coincide exactly with branching bisimulation. As the initial set of states $S$ is finite, the partition $𝒞$ can only be refined finitely often, which happens in the body of the while loop. This means that this algorithm always terminates with the required answer.

At least one splitter must be non-empty. If both splitters are given (as in line 1.18 of Algorithm 1), it is known that every bottom state of $B$ has a transition in at least one of the two splitters. We use data structures such that it is possible to quickly determine whether states with a transition in $\mathrm{𝑆𝑚𝑎𝑙𝑙𝑆𝑝}$ also have a transition in $\mathrm{𝐿𝑎𝑟𝑔𝑒𝑆𝑝}$.

We now go through the pseudocode shown as Algorithm 2.

In lines 2.2–2.11, the algorithm initialises a number of sets of states, mainly to decide for every bottom state to which part it belongs.

In lines 2.2–2.4 in case $\mathrm{𝑆𝑚𝑎𝑙𝑙𝑆𝑝}\ne \mathrm{\varnothing }$ every transition in $\mathrm{𝑆𝑚𝑎𝑙𝑙𝑆𝑝}$ is visited, and its source state is moved to $\mathrm{𝖱𝖾𝖺𝖼𝗁𝖠𝗅𝗐}$ or $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖫𝗋𝗀}$, depending on whether it has a transition in $\mathrm{𝐿𝑎𝑟𝑔𝑒𝑆𝑝}$ or not. Bottom states that have not been moved belong to $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖲𝗆𝗅}$. In case $\mathrm{𝑆𝑚𝑎𝑙𝑙𝑆𝑝}=\mathrm{\varnothing }$, the transitions in $\mathrm{𝐿𝑎𝑟𝑔𝑒𝑆𝑝}$ that start in a bottom state are traversed, to move these bottom states to $\mathrm{𝖱𝖾𝖺𝖼𝗁𝖠𝗅𝗐}$. The states that have not been moved belong to $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖫𝗋𝗀}$.

If some non-bottom state has a transition in $\mathrm{𝑆𝑚𝑎𝑙𝑙𝑆𝑝}$, it is not immediately known to which part it belongs; it might happen that it has a $ℬ$-inert transition to another part. If the non-bottom state has a transition in the small splitter but not in $\mathrm{𝐿𝑎𝑟𝑔𝑒𝑆𝑝}\ne \mathrm{\varnothing }$ (like $s_{15}$ in Figure 1 at the left), it may end up in any part except $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖲𝗆𝗅}$. To register this such a state is temporarily added to $\mathrm{𝖧𝗂𝗍𝖲𝗆𝖺𝗅𝗅}$ in line 2.8. It will be processed further in line 2.20 left.

If the non-bottom state has a transition in all (non-empty) splitters, it is potentially in $\mathrm{𝖱𝖾𝖺𝖼𝗁𝖠𝗅𝗐}$, unless it has a $ℬ$-inert transition to one of the other sub-blocks. In the latter case, it will be in $\mathrm{𝖭𝖾𝗐𝖡𝗈𝗍𝖲𝗍}$. We add it temporarily to pot-ReachAlw to register this in line 2.7.

If all bottom states belong to $\mathrm{𝖱𝖾𝖺𝖼𝗁𝖠𝗅𝗐}$, the split is trivial (lines 2.5–2.6). Even if all bottom states belong to one of $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖫𝗋𝗀}$ or $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖲𝗆𝗅}$, there still can be some non-bottom states with transitions causing a split. Such states will be moved to $\mathrm{𝖭𝖾𝗐𝖡𝗈𝗍𝖲𝗍}$.

After all bottom states have been distributed over the initial sets, we have to extend the distribution to the non-bottom states. To stay within the time bounds, we need to find all the states in the three smallest parts in time proportional to the number of their incoming and outgoing transitions.

Of the four coroutines, three (for $\mathrm{𝖱𝖾𝖺𝖼𝗁𝖠𝗅𝗐}$, $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖲𝗆𝗅}$ and $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖫𝗋𝗀}$) are almost the same. Their code is shown on the left of lines 2.12–2.41, where we use the keyword cor to indicate the three coroutines. The basic idea is the following. If all outgoing $ℬ$-inert transitions of some non-bottom state go to the same set, the state also belongs to this set. To avoid checking any transition more than once, we go through all incoming $ℬ$-inert transitions of the respective set and count how many outgoing $ℬ$-inert transitions of its source are not yet known to point to this set. If the $ℬ$-inert transitions point to different sets, the state belongs to $\mathrm{𝖭𝖾𝗐𝖡𝗈𝗍𝖲𝗍}$ (line 2.21 left).

If the number of unknown transitions is $0$, the source is added to the respective set, unless it has an incompatible transition in a splitter: states with a transition in both splitters can only be in $\mathrm{𝖱𝖾𝖺𝖼𝗁𝖠𝗅𝗐}$ or $\mathrm{𝖭𝖾𝗐𝖡𝗈𝗍𝖲𝗍}$ and were therefore already added to pot-ReachAlw; this ensures that they move to $\mathrm{𝖭𝖾𝗐𝖡𝗈𝗍𝖲𝗍}$ as soon as it is found out that they have a transition to $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖲𝗆𝗅}$ or $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖫𝗋𝗀}$. – States with a transition in $\mathrm{𝑆𝑚𝑎𝑙𝑙𝑆𝑝}$ but not in $\mathrm{𝐿𝑎𝑟𝑔𝑒𝑆𝑝}$ cannot be in $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖲𝗆𝗅}$. If they would be added to that set, the test in line 2.20 left ensures that they will be added to $\mathrm{𝖭𝖾𝗐𝖡𝗈𝗍𝖲𝗍}$ instead. – States with a transition in $\mathrm{𝐿𝑎𝑟𝑔𝑒𝑆𝑝}$ but not in $\mathrm{𝑆𝑚𝑎𝑙𝑙𝑆𝑝}$ cannot be in $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖫𝗋𝗀}$. But as the algorithm is not allowed to go through all transitions in $\mathrm{𝐿𝑎𝑟𝑔𝑒𝑆𝑝}$ a priori, they are more difficult to handle. Only if the number of unknown transitions is $0$ and the state is still a candidate for $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖫𝗋𝗀}$, we are allowed to spend the time to check whether it has a transition in $\mathrm{𝐿𝑎𝑟𝑔𝑒𝑆𝑝}$ by looking through its non-$𝒞$-inert outgoing transitions in lines 2.29–2.33 left. Section 6 explains why this fits the time bounds.

When all incoming $ℬ$-inert transitions of a set have been visited, no more states can be added, so that set is finished. The states that had some $ℬ$-inert transitions to the set but still have unknown transitions must have transitions to some other set as well, so they are added to $\mathrm{𝖭𝖾𝗐𝖡𝗈𝗍𝖲𝗍}$ in line 2.38 left. If $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖲𝗆𝗅}$ is the only coroutine that still runs on the left side, any unassigned states remaining in $\mathrm{𝖧𝗂𝗍𝖲𝗆𝖺𝗅𝗅}$ also belong to $\mathrm{𝖭𝖾𝗐𝖡𝗈𝗍𝖲𝗍}$, as they cannot be in $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖲𝗆𝗅}$ (see lines 2.39–2.40 left).

The fourth coroutine, the one for $\mathrm{𝖭𝖾𝗐𝖡𝗈𝗍𝖲𝗍}$, follows a slightly simpler principle. Every $ℬ$-inert predecessor of a $\mathrm{𝖭𝖾𝗐𝖡𝗈𝗍𝖲𝗍}$-state is also in $\mathrm{𝖭𝖾𝗐𝖡𝗈𝗍𝖲𝗍}$, independent of other transitions it might have. This happens in line 2.18 right. The other three coroutines may also occasionally add states to $\mathrm{𝖭𝖾𝗐𝖡𝗈𝗍𝖲𝗍}$ and therefore, different from the first three coroutines, we cannot end the coroutine as soon as all incoming $ℬ$-inert transitions of the current $\mathrm{𝖭𝖾𝗐𝖡𝗈𝗍𝖲𝗍}$ have been visited. Instead, we wait in an (outer) infinite loop. The outer loop can terminate when at least $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖫𝗋𝗀}$ and one other coroutine have finished.

If only the coroutines for $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖫𝗋𝗀}$ and $\mathrm{𝖭𝖾𝗐𝖡𝗈𝗍𝖲𝗍}$ are still running, the latter will go through $\mathrm{𝐿𝑎𝑟𝑔𝑒𝑆𝑝}$ to find states that cannot be in $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖫𝗋𝗀}$ in lines 2.24–2.27 right. If the source state of some transition in $\mathrm{𝐿𝑎𝑟𝑔𝑒𝑆𝑝}$ has not yet been inserted into a sub-block, it cannot be in $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖫𝗋𝗀}$, so it must be in $\mathrm{𝖭𝖾𝗐𝖡𝗈𝗍𝖲𝗍}$.

We can ignore the coroutine for the largest sub-block because it is aborted as soon as it is clearly the largest (line 2.13) or the three other coroutines are finished. The time it spends is at most proportional to the time attribution of the second-largest coroutine.

Initialisation (lines 2.2–2.11):

If the function is called from the main algorithm, $\mathrm{𝑆𝑚𝑎𝑙𝑙𝑆𝑝}$ either consists of outgoing transitions of $B$ (line 1.8) or of incoming transitions of $B$ (lines 1.14 and 1.18). Then the sets $\mathrm{𝖱𝖾𝖺𝖼𝗁𝖠𝗅𝗐}$, $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖫𝗋𝗀}$, $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖲𝗆𝗅}$, pot-ReachAlw and $\mathrm{𝖧𝗂𝗍𝖲𝗆𝖺𝗅𝗅}$ can be initialised by going through the transitions in $\mathrm{𝑆𝑚𝑎𝑙𝑙𝑆𝑝}$, which falls under timing item C. Note that we require that for states with a transition in $\mathrm{𝑆𝑚𝑎𝑙𝑙𝑆𝑝}$, one can determine in time $O\left(1\right)$ whether they have a transition in $\mathrm{𝐿𝑎𝑟𝑔𝑒𝑆𝑝}$. This allows to distinguish $\mathrm{𝖱𝖾𝖺𝖼𝗁𝖠𝗅𝗐}$ from $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖫𝗋𝗀}$ and pot-ReachAlw from $\mathrm{𝖧𝗂𝗍𝖲𝗆𝖺𝗅𝗅}$.

If the function is called from $\mathrm{𝗌𝗍𝖺𝖻𝗂𝗅𝗂𝗌𝖾}ℬ$ (line 3.12), $\mathrm{𝑆𝑚𝑎𝑙𝑙𝑆𝑝}=\mathrm{\varnothing }$, and $\mathrm{𝐿𝑎𝑟𝑔𝑒𝑆𝑝}$ consists of outgoing transitions of a block with new bottom states. Then the sets $\mathrm{𝖱𝖾𝖺𝖼𝗁𝖠𝗅𝗐}$ and $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖫𝗋𝗀}$ can be distinguished by going through those transitions in $\mathrm{𝐿𝑎𝑟𝑔𝑒𝑆𝑝}$ that start in (new) bottom states, which falls under timing item N. The other sets in the initialisation are empty. Note that we only spend time on transitions in $\mathrm{𝐿𝑎𝑟𝑔𝑒𝑆𝑝}$ starting in bottom states because we singled them out in lines 3.6 and 3.16.

All coroutines:

Every coroutine generally runs a loop over all states in the respective sub-block and its incoming transitions. This can immediately be attributed to timing item B.

Coroutine

for $\mathrm{𝗔𝘃𝗼𝗶𝗱𝗟𝗿𝗴}$ (lines 2.29–2.33 left):  The coroutine for $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖫𝗋𝗀}$, once it has found a state $t$ with $t.\mathrm{𝑐𝑜𝑢𝑛𝑡}=0$, still needs to check whether $t$ has a transition in $\mathrm{𝐿𝑎𝑟𝑔𝑒𝑆𝑝}$ that could not be handled during initialisation. Depending on the outcome of this check, we attribute the time spent on the loop in lines 2.29–2.33 left differently:

• $\mathrm{■}$

  If $t$ has no transition in $\mathrm{𝐿𝑎𝑟𝑔𝑒𝑆𝑝}$, we conclude that $t\in \mathrm{𝖠𝗏𝗈𝗂𝖽𝖫𝗋𝗀}$, and we can attribute the time to the outgoing transitions of $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖫𝗋𝗀}$, i.e. to timing item B.

• $\mathrm{■}$

  If, however, $t$ has a transition in $\mathrm{𝐿𝑎𝑟𝑔𝑒𝑆𝑝}$, it is added to $\mathrm{𝖭𝖾𝗐𝖡𝗈𝗍𝖲𝗍}$ in line 2.32 left, and it becomes a new bottom state: all its outgoing $ℬ$-inert transitions point to another sub-block (namely $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖫𝗋𝗀}$). Therefore we can attribute this to timing item N.

Finalising a sub-block $R=\mathrm{𝖱𝖾𝖺𝖼𝗁𝖠𝗅𝗐}$, $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖲𝗆𝗅}$ or $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖫𝗋𝗀}$:

In line 2.38 left, states in $\text{pot-}R\setminus R$ are moved to $\mathrm{𝖭𝖾𝗐𝖡𝗈𝗍𝖲𝗍}$. Every such state has a transition to $R$, so this is attributed to timing item B. In lines 2.39–2.40 left, the $\mathrm{𝖧𝗂𝗍𝖲𝗆𝖺𝗅𝗅}$-states are moved to $\mathrm{𝖭𝖾𝗐𝖡𝗈𝗍𝖲𝗍}$. Because $\left|\mathrm{𝖧𝗂𝗍𝖲𝗆𝖺𝗅𝗅}\right|\le \left|\mathrm{𝑆𝑚𝑎𝑙𝑙𝑆𝑝}\right|$, we can attribute this to timing item C.

Coroutine for $\mathrm{𝖭𝖾𝗐𝖡𝗈𝗍𝖲𝗍}$:

This coroutine has an outer infinite loop in line 2.14 right, when all states that are known to be in $\mathrm{𝖭𝖾𝗐𝖡𝗈𝗍𝖲𝗍}$ are already explored and the coroutine has to wait until a different coroutine adds another state to $\mathrm{𝖭𝖾𝗐𝖡𝗈𝗍𝖲𝗍}$. Note that this will only happen as long as at least two coroutines different from $\mathrm{𝖭𝖾𝗐𝖡𝗈𝗍𝖲𝗍}$ are running. So, we can attribute the waiting time to the smaller of the two sub-blocks. When only the coroutines for $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖫𝗋𝗀}$ and $\mathrm{𝖭𝖾𝗐𝖡𝗈𝗍𝖲𝗍}$ are unfinished, the latter goes through the transitions in $\mathrm{𝐿𝑎𝑟𝑔𝑒𝑆𝑝}$ in lines 2.24–2.27 right. Source states of these transitions cannot be in $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖫𝗋𝗀}$, so they either are in a finished sub-block (and then that sub-block is not the largest one, so we are allowed to spend time on its outgoing transitions under timing item B) or they are in $\mathrm{𝖭𝖾𝗐𝖡𝗈𝗍𝖲𝗍}$ (and then they also fall under timing item B).

Final administration (lines 2.42–2.46):

This can be organised in a way that only the states in the three smallest sub-blocks and their outgoing transitions are moved to new blocks and new BLC sets, respectively. So, we attribute it to timing item B.

$◀$

It can happen that we have to stabilise a block with new bottom states under BLC sets whose transitions all start in non-bottom states, but then after the respective call to $\text{four-way-split}ℬ$, this BLC set will contain a transition that starts in a new bottom state. We denote the set of the new bottom states together with these prospective new bottom states by “${\mathrm{𝐵𝑜𝑡𝑡𝑜𝑚}}^{+}(B)$”.

Initialisation (lines 3.3–3.7):

If one adds transitions to $\widehat{𝒬}$ in constant time per BLC set in line 3.4, then time $O\left(\left|{\mathrm{𝐵𝑜𝑡𝑡𝑜𝑚}}^{+}(B)\right|\right)$ is spent. Lines 3.5–3.7 access new bottom states and their outgoing transitions. All these steps can be attributed to timing item N.

Main loop (lines 3.8–3.12):

In every iteration one BLC set in $\widehat{𝒬}$ is handled, so there cannot be more iterations than transitions starting in ${\mathrm{𝐵𝑜𝑡𝑡𝑜𝑚}}^{+}(B)$ (summed over all blocks $B$ with new bottom states). The call to $\text{four-way-split}ℬ$ is attributed according to Lemma 6.1.

Adding another new bottom block (lines 3.13–3.17):

This is the same operation as the loop body for the initialisation (lines 3.4–3.7), so we can attribute the timing in the same way. When adding new transitions to $\widehat{𝒬}$, one only has to take care not to spend time on BLC sets that have been added already earlier.

$◀$

Splitting a constellation (lines 1.4–1.8):

This part of the algorithm handles the states and transitions of $B$ and is attributed to timing item C.

Stabilising under $B$ and $C\setminus B$ (lines 1.9–1.19):

Except for the calls to $\text{four-way-split}ℬ$ and $\mathrm{𝗌𝗍𝖺𝖻𝗂𝗅𝗂𝗌𝖾}ℬ$ (which fall under Lemmas 6.1 and 6.2), these lines use constant time per iteration. Because $ℳ\subseteq \mathrm{𝑖𝑛}(B)$, there are not too many iterations.

$◀$

We believe that many data structures are straightforward to implement, and we only describe the less obvious data structures here.

Transitions are stored in three orderings: incoming transitions per state (used e.g. in lines 1.6–1.7 and 2.16), outgoing transitions per state (used e.g. in lines 2.30 left and 3.6), and transitions per BLC set (used e.g. in lines 2.24 right and 3.4). The outgoing transitions are grouped per label and target constellation, and every block has a list of BLC sets with transitions that start in this block.

When splitting a constellation (line 1.6), the groups for outgoing transitions per state to $C$ are split into two, such that the groups for $\mathrm{𝑆𝑚𝑎𝑙𝑙𝑆𝑝}$ and $\mathrm{𝐿𝑎𝑟𝑔𝑒𝑆𝑝}$ are next to each other. This allows to find out quickly whether a state with an outgoing transition in one of them also has a transition in the other (used to distinguish $\mathrm{𝖱𝖾𝖺𝖼𝗁𝖠𝗅𝗐}$ from $\mathrm{𝖠𝗏𝗈𝗂𝖽𝖫𝗋𝗀}$ and pot-ReachAlw from $\mathrm{𝖧𝗂𝗍𝖲𝗆𝖺𝗅𝗅}$ in lines 2.2–2.8). Similarly, the list entries for BLC sets containing transitions to $C$ are split into two adjacent ones, and line 1.16 can find $\mathrm{𝐿𝑎𝑟𝑔𝑒𝑆𝑝}$ (given $\mathrm{𝑆𝑚𝑎𝑙𝑙𝑆𝑝}$) in time $O\left(1\right)$.

During $\mathrm{𝗌𝗍𝖺𝖻𝗂𝗅𝗂𝗌𝖾}ℬ$, we place BLC sets that are in $\widehat{𝒬}$ near the end of the list, so that line 3.14 only spends time on BLC sets that are currently not in $\widehat{𝒬}$.

To be absolutely sure that our correctness and timing analysis, as well as the implementation are correct we instrumented the implementation with both assertions and counters counting each operation on states and transitions and ran it on a large number of transition systems, most of which were randomly generated. Besides the invariants and the overall time bounds, it is checked that after the coroutines are finished, the counters for the largest sub-block have not been increased more often than the others, and also that the coroutine for $\mathrm{𝖭𝖾𝗐𝖡𝗈𝗍𝖲𝗍}$ did not wait too often without doing assignable work.