An O(m log n) Algorithm for
Stuttering Equivalence and Branching Bisimulation
Jan Friso Groote and Anton Wijs
Department of Mathematics and Computer Science, Eindhoven University of Technology
P.O. Box 513, 5600 MB Eindhoven, The Netherlands

arXiv:1601.01478v1 [cs.LO] 7 Jan 2016

{J.F.Groote,A.J.Wijs}@tue.nl

Abstract
We provide a new algorithm to determine stuttering equivalence with time complexity O(m log n),
where n is the number of states and m is the number of transitions of a Kripke structure. This algorithm can also be used to determine branching bisimulation in O(m(log |Act| + log n)) time where Act
is the set of actions in a labelled transition system.
Theoretically, our algorithm substantially improves upon existing algorithms which all have time
complexity O(mn) at best [2, 3, 9]. Moreover, it has better or equal space complexity. Practical results
confirm these findings showing that our algorithm can outperform existing algorithms with orders of
magnitude, especially when the sizes of the Kripke structures are large.
The importance of our algorithm stretches far beyond stuttering equivalence and branching bisimulation. The known O(mn) algorithms were already far more efficient (both in space and time) than
most other algorithms to determine behavioural equivalences (including weak bisimulation) and therefore it was often used as an essential preprocessing step. This new algorithm makes this use of stuttering
equivalence and branching bisimulation even more attractive.

1

Introduction

Stuttering equivalence [4] and branching bisimulation [8] were proposed as alternatives to Milner’s weak
bisimulation [13]. They are very close to weak bisimulation, with as essential difference that all states
in the mimicking sequence τ ∗ a τ ∗ must be related to either the state before or directly after the a from
the first system. This means that branching bisimulation and stuttering equivalence are slightly stronger
notions than weak bisimulation.
In [9] an O(mn) time algorithm was proposed for stuttering equivalence and branching bisimulation,
where m is the number of transitions and n is the number of states in either a Kripke structure (for stuttering
equivalence) or a labelled transition system (for branching bisimulation). We refer to this algorithm as
GV. It is based upon the O(mn) algorithm for bisimulation equivalence in [11]. Both algorithms require
O(m+n) space. They calculate for each state whether it is bisimilar to another state.
The basic idea of the algorithms of [9, 11] is to partition the set of states into blocks. States that are
bisimilar always reside in the same block. Whenever there are some states in a block B 0 from which
a transition is possible to some block B and there are other states in B 0 from which such a step is not
possible, B 0 is split accordingly. Whenever no splitting is possible anymore, the partition is called stable,
and two states are in the same block iff they are bisimilar.
There have been some attempts to come up with improvements of GV. The authors of [2] observed that
GV only splits a block in two parts at a time. They proposed to split a block in as many parts as possible,
reducing moving states and transitions to new blocks. Their worst case time and space complexities are
worse than that of GV, especially the space complexity O(mn), but in practice this algorithm can outperform GV. In [3], the space complexity is brought back to O(m+n). A technique to be performed on
Graphics Processing Units based on both GV and [2, 3] is proposed in [19]. This improves the required runtime considerably by employing parallelism, but it does not imply any improvement to the single-threaded
algorithm.
1

2

PRELIMINARIES

2

In [15] an O(m log n) algorithm is proposed for strong bisimulation as an improvement upon the algorithm of [11]. The core idea for this improvement is described as “process the smaller half” [1]. Whenever
a block is split in two parts the amount of work must be contributed to the size of the smallest resulting
block. In such a case a state is only involved in the process of splitting if it resides in a block at most half
the size of the block it was previously in when involved in splitting. This means that a state can never be
involved in more than log2 n splittings. As the time used in each state is proportional to the number of
incoming or outgoing transitions in that state, the total required time is O(m log n).
In this paper we propose the first algorithm for stuttering equivalence and branching bisimulation in
which the “process the smaller half”-technique is used. By doing so, we can finally confirm the conjecture
in [9] that such an improvement of GV is conceivable. Moreover, we achieve an even lower complexity,
namely O(m log n), than conjectured in [9] by applying the technique twice, the second time for handling
the presence of inert transitions. First we establish whether a block can be split by combining the approach
regarding bottom states from GV with the detection approach in [15]. Subsequently, we use the “process
the smaller half”-technique again to split a block by only traversing transitions in a time proportional to
the size of the smallest subblock. As it is not known which of the two subblocks is smallest, the transitions
of the two subblocks are processed alternatingly, such that the total processing time can be contributed to
the smallest block. For checking behavioural equivalences, applying such a technique is entirely new. We
are only aware of a similar approach for an algorithm in which the smallest bottom strongly connected
component of a graph needs to be found [5].
The algorithm that we propose is complex. Although the basic sketch of the algorithm is relatively
straightforward, it heavily relies on auxiliary data structures. For instance, for each transition it is recalled
how many other transitions there are from the block where the transition starts to the constellation in which
the transition ends. Maintaining such auxiliary data structures is a tedious process. Therefore, we do not
only prove the major steps of the algorithm correct, we also provide a very detailed description of the
algorithm, and we ran the implemented algorithm on many thousands of randomly generated test cases,
comparing the reductions with the outcomes of existing algorithms. This not only convinced us that the
algorithm is correct and correctly implemented, it also allows others to easily reimplement the algorithm.
From a theoretical viewpoint our algorithm outperforms its predecessors substantially. But a fair question is whether this also translates into practice. The theoretical bounds are complexity upperbounds, and
depending on the transition system, the classical algorithms can be much faster than the upperbound suggests. Furthermore, the increased bookkeeping in the new algorithm may be such a burden that all gains
are lost. For this reason we compared the practical performance of our algorithm with that of the predecessors, and we found that for practical examples our algorithm can always match the best running times, but
especially when the Kripke structures and transition systems get large, our algorithm tends to outperform
existing algorithms with orders of magnitude.
Compared to checking other equivalences the existing algorithms for branching bisimulation/stuttering
equivalence were already known to be practically very efficient. This is the reason that they are being
used in multiple explicit-state model checkers, such as C ADP [7], the M CRL2 toolset [10] and TVT [18].
In particular they are being used as preprocessing steps for other equivalences (weak bisimulation, trace
based equivalences) that are much harder to compute. For weak bisimulation recently a O(mn) algorithm
has been devised [12, 16], but until that time an expensive transitive closure operation of at best O(n2.373 )
was required. Using our algorithm as a preprocessing step, the computation time of all other behavioural
‘weak’ equivalences can be made faster.

2

Preliminaries

We introduce Kripke structures and (divergence-blind) stuttering equivalence. Labelled transitions systems
and branching bisimulation will be addressed in section 6.
Definition 2.1 (Kripke structure). A Kripke structure is a four tuple K = (S, AP , →
− , L), where
1. S is a finite set of states.
2. AP is a finite set of atomic propositions.

3

PARTITIONS AND SPLITTERS: A SIMPLE ALGORITHM

3

3. →
− ⊆ S × S is a total transition relation, i.e., for each s ∈ S there is an s0 ∈ S s.t. s →
− s0 .
4. L : S → 2AP is a state labelling.
We use n=|S| for the number of states and m=| →
− | for the number of transitions. For a set of states B⊆S,
we write s →
− B s0 for s →
− s0 and s0 ∈ B, and s →
− B iff there is some s0 ∈ B such that s →
− s0 . We write
0
0
s 6→ s and s 6→ B iff it is not the case that s →
− s , resp., s →
− B.
Definition 2.2 (Divergence-blind stuttering equivalence). Let K = (S, AP , →
− , L) be a Kripke structure. A symmetric relation R ⊆ S × S is a divergence-blind stuttering equivalence iff for all s, t ∈ S such
that sRt:
1. L(s) = L(t).
2. for all s0 ∈ S if s →
− s0 , then there are t0 , . . . , tk ∈ S for some k ∈ N such that t = t0 , sRti ,
0
ti →
− ti+1 , and s Rtk for all i < k.
We say that two states s, t ∈ S are divergence-blind stuttering equivalent, notation s↔dbs t, iff there is a
divergence-blind stuttering equivalence relation R such that sRt.
An important property of divergence-blind stuttering equivalence is that if states on a loop all have the
same label then all these states are divergence-blind stuttering equivalent. We define stuttering equivalence
in terms of divergence-blind stuttering equivalence using the following Kripke structure.
Definition 2.3 (Stuttering equivalence). Let K = (S, AP , →
− , L) be a Kripke structure. Define the
Kripke structure Kd = (S ∪ {sd }, AP ∪ {d}, →
− d , Ld ) where d is an atomic proposition not occurring in
AP and sd is a fresh state not occurring in S. Furthermore,
1. →
−d = →
− ∪ {hs, sd i | s is on a cycle of states all labelled with L(s), or s = sd }.
2. For all s ∈ S we define Ld (s) = L(s) and Ld (sd ) = {d}.
States s, t ∈ S are stuttering equivalent, notation s↔s t iff there is a divergence-blind stuttering equivalence
relation R on Sd such that sRt.
Note that an algorithm for divergence-blind stuttering equivalence can also be used to determine stuttering
equivalence by employing only a linear time and space transformation. Therefore, we only concentrate on
an algorithm for divergence-blind stuttering equivalence.

3

Partitions and splitters: a simple algorithm

Our algorithms perform partition refinement of an initial partition containing the set of states S. A partition
π = {B
S i ⊆ S | 1 ≤ i ≤ k} is a set of non empty subsets such that Bi ∩ Bj = ∅ for all 1 ≤ i < j ≤ k and
S = 1≤i≤k Bi . Each Bi is called a block.
We call a transition s →
− s0 inert w.r.t. π iff s and s0 are in the same block B ∈ π. We say that a partition
π coincides with divergence-blind stuttering equivalence when s↔dbs t iff there is a block B ∈ π such
that s, t ∈ B. We say that a partition respects divergence-blind stuttering equivalence iff for all s, t ∈ S
if s↔dbs t then there is some block B ∈ π such that s, t ∈ B. The goal of the algorithm is to calculate a
partition that coincides with divergence-blind stuttering equivalence. This is done starting with the initial
partition π0 consisting of blocks B satisfying that if s, t ∈ B then L(s) = L(t). Note that this initial
partition respects divergence-blind stuttering equivalence.
We say that a partition π is cycle-free iff there is no state s ∈ B such that s →
− B s1 →
− B ··· →
− B sk →
− s
for some k ∈ N for each block B ∈ π. It is easy to make the initial partition π0 cycle-free by merging all
states on a cycle in each block into a single state. This preserves divergence-blind stuttering equivalence and
can be performed in linear time employing a standard algorithm to find strongly connected components [1].

3

PARTITIONS AND SPLITTERS: A SIMPLE ALGORITHM

4

The initial partition is refined until it coincides with divergence-blind stuttering equivalence. Given a
block B 0 of the current partition and the union B of some of the blocks in the partition, we define
split(B 0 , B) = {s0 ∈B 0 | ∃k∈N, s1 , .., sk ∈S.si →
− si+1 , si ∈B 0 for all i < k ∧ sk ∈B}
0
0
0
cosplit(B , B) = B \ split(B , B).
Note that if B 0 ⊆ B, then split(B 0 , B) = B 0 . The sets split(B 0 , B) and cosplit(B 0 , B) are intended as the
new blocks to replace B 0 . It is common to split blocks under single blocks, i.e., B corresponding with a
single block B ∈ π [9, 11]. However, as indicated in [15], it is required to split under the union of some of
the blocks in π to obtain an O(m log n) algorithm. We refer to such unions as constellations. In section 4,
we use constellations consisting of more than one block in the splitting.
We say that a block B 0 is unstable under B iff split(B 0 , B) 6= ∅ and cosplit(B 0 , B) 6= ∅. A partition π
is unstable under B iff there is at least one B 0 ∈ π which is unstable under B. If π is not unstable under
B then it is called stable under B. If π is stable under all B, then it is simply called stable.
A refinement of B 0 ∈ π under B consists of two new blocks split(B 0 , B) and cosplit(B 0 , B). A
partition π 0 is a refinement of π under B iff all unstable blocks B 0 ∈ π have been replaced by new blocks
split(B 0 , B) and cosplit(B 0 , B).
The following lemma expresses that if a partition is stable then it coincides with divergence-blind
stuttering equivalence. It also says that during refinement, the encountered partitions respect divergenceblind stuttering equivalence and remain cycle-free.
Lemma 3.1. Let K = (S, AP , →
− , L) be a Kripke structure and π a partition of S.
1. For all states s, t ∈ S, if s, t ∈ B with B a block of the partition π, π is stable, and a refinement of
the initial partition π0 , then s↔dbs t.
2. If π respects divergence-blind stuttering equivalence then any refinement of π under the union of
some of the blocks in π also respects it.
3. If π is a cycle-free partition, then any refinement of π is also cycle-free.
Proof.
1. We show that if π is a stable partition, the relation R = {hs, ti | s, t ∈ B, B ∈ π} is a divergenceblind stuttering equivalence. It is clear that R is symmetric. Assume sRt. Obviously, L(s) = L(t)
because s, t ∈ B and B refines the initial partition. For the second requirement of divergence-blind
stuttering equivalence, suppose s →
− s0 . There is a block B 0 such that s0 ∈ B 0 . As π is stable, it holds
for t that t = t0 →
− t1 →
− ··· →
− tk for some k ∈ N, t0 , . . . , tk−1 ∈ B and tk ∈ B 0 . This clearly
shows that for all i < k sRti , and s0 Rtk . So, R is a divergence-blind stuttering equivalence, and
therefore it holds for all states s, t ∈ S that reside in the same block of π that s↔dbs t.
2. The second part can be proven by reasoning towards a contradiction. Let us assume that a partition π 0
that is a refinement of π under B does not respect divergence-blind stuttering equivalence, although
π does. Hence, there are states s, t ∈ S with s↔dbs t and a block B 0 ∈ π with s, t ∈ B 0 and s and
t are in different blocks in π 0 . Given that π 0 is a refinement of π under B, s ∈ split(B 0 , B) and
t ∈ cosplit(B 0 , B) (or vice versa, which can be proven similarly). By definition of split, there are
s1 , . . . , sk−1 ∈ B 0 (k ∈ N) and sk ∈ B such that s →
− s1 →
− ··· →
− sk . Then, either k = 0 and
B 0 ⊆ B, but then t ∈
/ cosplit(B 0 , B). Or k > 0, and since s↔dbs t, there are t1 , . . . , tl−1 ∈ B 0
(l ∈ N) and tl ∈ B such that t →
− t1 →
− ··· →
− tl with si Rtj for all 1 ≤ i < k, 1 ≤ j < l and sk Rtl .
This means that we have t ∈ split(B 0 , B), again contradicting that t ∈ cosplit(B 0 , B).
3. If π is cycle-free, this property is straightforward, since splitting any block of π will not introduce
cycles.

This suggests the following simple algorithm which has time complexity O(mn) and space complexity
O(m+n), which essentially was presented in [9].

3

PARTITIONS AND SPLITTERS: A SIMPLE ALGORITHM

5

π := π0 , i.e., the initial partition;
while π is unstable under some B ∈ π
π := refinement of π under B;
It is an invariant of this algorithm that π respects divergence-blind stuttering equivalence and π is cyclefree. In particular, π = π0 satisfies this invariant initially. If π is not stable, a refinement under some
block B exists, splitting at least one block. Therefore, this algorithm finishes in at most n−1 steps as
during each iteration of the algorithm the number of blocks increases by one, and the number of blocks
can never exceed the number of states. When the algorithm terminates, π is stable and therefore, two states
are divergence-blind stuttering equivalent iff they are part of the same block in the final partition. This end
result is independent of the order in which splitting took place.
In order to see that the time complexity of this algorithm is O(mn), we must show that we can detect
that π is unstable and carry out splitting in time O(m). The crucial observation to efficiently determine
whether a partition is stable stems from [9] where it was shown that it is enough to look at the bottom states
of a block, which always exist for each block because the partition is cycle-free. The bottom states of a
block are those states that do not have an outgoing inert transition, i.e., a transition to a state in the same
block. They are defined by
bottom(B) = {s ∈ B | there is no state s0 ∈ B such that s →
− s0 }.
The following lemma presents the crucial observation concerning bottom states.
Lemma 3.2. Let K = (S, AP , →
− , L) be a Kripke structure and π be a cycle-free partition of its states.
Partition π is unstable under union B of some of the blocks in π iff there is a block B 0 ∈ π such that
∅ ⊂ split(B 0 , B) and bottom(B 0 ) ∩ split(B 0 , B) ⊂ bottom(B 0 ).
Here ⊂ is meant to be a strict subset.
Proof.
⇒ If π is unstable, then split(B 0 , B) 6= ∅ and split(B 0 , B) 6= B 0 . The first conjunct immediately
0
implies ∅ ⊂ split(B 0 , B). If split(B 0 , B) 6= B 0 , there are states s∈split(B
/
, B). As the blocks
0
0
B ∈π do not have cycles, consider such an s ∈
/ split(B , B) with a smallest distance to a state
sk ∈bottom(B 0 ), i.e., s →
− s1 →
− ··· →
− sk with all si ∈ B 0 . If s itself is an element of bottom(B 0 ),
0
the second part of the right hand side of the lemma follows. Assume s∈bottom(B
/
), there is some
0
0
0
0
0
0
state s ∈B closer to bottom(B ) such that s →
− s . Clearly, s ∈split(B
/
, B) either, as otherwise
s ∈ split(B 0 , B). But as s0 is closer to bottom(B 0 ), the state s was not a state with the smallest
distance to a state in bottom(B 0 ), which is a contradiction.
⇐ It follows from the right hand side that split(B 0 , B) 6= ∅, split(B 0 , B) 6= B 0 .

This lemma can be used as follows to find a block to be split. Consider each B ∈ π. Traverse its incoming
transitions and mark the states that can reach B in zero or one step. If a block B 0 has marked states, but
not all of its bottom states are marked, the condition of the lemma applies, and it needs to be split. It is at
most needed to traverse all transitions to carry this out, so its complexity is O(m).
If B is equal to B 0 , no splitting is possible. We implement it by marking all states in B as each state
in B can reach itself in zero steps. In this case condition bottom(B 0 ) ∩ split(B 0 , B) ⊂ bottom(B 0 ) is not
true. This is different from [9] where a block is never considered as a splitter of itself, but we require this
in the algorithm in the next sections.
If a block B 0 is unstable, and all states from which a state in B can be reached in one step are marked,
then a straightforward recursive procedure is required to extend the marking to all states in split(B 0 , B),
and those states need to be moved to a new block. This takes time proportional to the number of transitions
in B 0 , i.e., O(m).

4

CONSTELLATIONS: AN O(M LOG N ) ALGORITHM

B1
C

B

6

B2
0

B

Figure 1: After splitting B 0 under C, B1 is not stable under B.

4

Constellations: an O(m log n) algorithm

The crucial idea to transform the algorithm from the previous section into an O(m log n) algorithm stems
from [15]. By grouping the blocks in the current partition π into constellations such that π is stable
under the union of the blocks in such a constellation, we can determine whether a block exists under
which π is unstable by only looking at blocks that are at most half the size of the constellation, i.e.,
|B| ≤ 12 ΣB 0 ∈B |B 0 |, for a block B in a constellation B. If a block B 0 ∈ π is unstable under B, then we use
a remarkable technique consisting of two procedures running alternatingly to identify the smallest block
resulting from the split. The whole operation runs in time proportional to the smallest block resulting from
the split. We involve the blocks in B \ B 1 in the splitting without explicitly analysing the states contained
therein.
Working with constellations in this way ensures for each state that whenever it is involved in splitting,
i.e., if it is part of a block that is used to split or that is being split, this block is half the size of the previous
block in which the state resided when it was involved in splitting. That ensures that each state can at
most be log2 (n) times involved in splitting. When involving a state, we only analyse its incoming and
outgoing transitions, resulting in an algorithm with complexity O(m log n). Although we require quite a
number of auxiliary data structures, these are either proportional to the number of states or to the number
of transitions. So, the memory requirement is O(m+n).
In the following, the set of constellations also forms a partition, which we denote by C. A constellation is the union of one or more blocks from the current partition. If it corresponds with one block, the
constellation is called trivial. The current partition is stable with respect to each constellation in C.
If a constellation B contains more than one block, we select one block B∈B which is at most half the
size of B. We check whether the current partition is stable under B and B \ B according to lemma 3.2 by
traversing the incoming transitions of states in B and marking the encountered states that can reach B in
zero or one step. For all blocks B 0 that are unstable according to lemma 3.2, we calculate split(B 0 , B) and
cosplit(B 0 , B), as indicated below.
As noted in [15], cosplit(B 0 , B) is stable under B \ B. Therefore, only further splitting of split(B 0 , B)
under B \ B must be investigated. If B 0 is stable under B because all bottom states of B 0 are marked, it
can be that B 0 is not stable under B \ B, which we do not address here explicitly, as it proceeds along the
same line.
There is a special data structure to recall for any B 0 and B which transitions go from B 0 to B. When
investigating whether split(B 0 , B) is stable under B we adapt this list to determine the transitions from
split(B 0 , B) to B \ B and we simultaneously tag the states in B 0 that have a transition to B \ B. Therefore,
we know whether there are transitions from split(B 0 , B) to B \ B and we can traverse the bottom states of
split(B 0 , B) to inspect whether there is a bottom state without a transition to B. Following lemma 3.2, this
allows us to determine whether split(B 0 , B) must be split under B \ B in a time proportional to the size of
B. How splitting is carried out is indicated below.
When the current partition has become stable under B and B \ B, B is moved from constellation B
into a new trivial constellation B 0 , and the constellation B is reduced to contain the states in B \ B. Note
that the new B can have become trivial.
There is one aspect that complicates matters. If blocks are split, the new partition is not automatically
stable under all constellations. This is contrary to the situation in [15] and was already observed in [9].
Figure 1 indicates the situation. Block B 0 is stable under constellation B. But if B 0 is split under block C
into B1 and B2 , block B1 is not stable under B. The reason is, as exemplified by the following lemma,
1 For

convenience, we write B \ B instead of B \ {B}.

4

CONSTELLATIONS: AN O(M LOG N ) ALGORITHM

7

that some states that were non-bottom states in B 0 became bottom states in B1 .
Lemma 4.1. Let K = (S, AP , →
− , L) be a Kripke structure with cycle free partition π with refinement
π 0 . If π is stable under a constellation B, and B 0 ∈ π is refined into B10 , . . . , Bk0 ∈ π 0 , then for each Bi0
where the bottom states in Bi0 are also bottom states in B 0 , it holds that Bi0 is also stable under B.
Proof. Assume Bi0 is not stable under B. This means that Bi0 is not a subset of B. Hence, there is a state
s ∈ Bi0 such that s →
− s0 with s0 ∈ B and there is a bottom state t ∈ Bi0 with no outgoing transition to a
state in B. But as B 0 was stable under B, and s has an outgoing transition to a state in B, all bottom states
in B 0 must have at least one transition to a state in B. Therefore, t cannot be a bottom state of B 0 , and
must have become a bottom state after splitting B 0 .

This means that if a block B 0 is the result of a refinement, and some of its states became bottom states, it
must be made sure that B 0 is stable under the constellations. Typically, from the new bottom states a smaller
number of blocks in the constellation can be reached. For each block we maintain a list of constellations
that can be reached from states in this block. We match the outgoing transitions of the new bottom states
with this list, and if there is a difference, we know that B 0 must be split further.
The complexity of checking for additional splittings to regain stability when states become bottom
states is only O(m). Each state only becomes a bottom state once, and when that happens we perform
calculations proportional to the number of outgoing transitions of this state to determine whether a split
must be carried out.
It remains to show that splitting can be performed in a time proportional to the size of the smallest
block resulting from the splitting. Consider splitting B 0 under B∈B. While marking B 0 four lists of all
marked and non marked, bottom and non bottom states have been constructed. We simultaneously mark
states in B 0 either red or blue. Red means that there is a path from a state in B 0 to a state in B. Blue means
that there is no such path. Initially, marked states are red, and non marked bottom states are blue.
This colouring is simultaneously extended to all states in B 0 , spending equal time to both. The procedure is stopped when the colouring of one of the colours cannot be enlarged. We colour states red that
can reach other red states via inert transitions using a simple recursive procedure. We colour states blue
for which it is determined that all outgoing inert transitions go to a blue state (for this we need to recall
for each state the number of outgoing inert transitions) and there is no direct transition to B. The marking
procedure that terminates first, provided that its number of marked states does not exceed 21 |B 0 |, has the
smallest block that must be split. Now that we know the smallest block we move its states to a newly
created block.
Splitting regarding B \ B only has to be applied to split(B 0 , B), or to B 0 if all bottom states of B 0
were marked. As noted before cosplit(B 0 , B) is stable under B \ B. Define C := split(B 0 , B) or C := B 0
depending on the situation. We can traverse all bottom states of C and check whether they have outgoing
transitions to B \ B. This provides us with the blue states. The red states are obtained as we explicitly
maintained the list of all transitions from C to B \ B. By simultaneously extending this colouring the
smallest subblock of either red or blue states is obtained and splitting can commence.
The algorithm is concisely presented below. After that, it is presented in full detail in section 5. Since
it is not trivial how to achieve the O(m log n) complexity, we have decided to describe the algorithm as
detailed as possible.
π := initial partition; C := {π};
while C contains a non trivial constellation B ∈ C
choose some B ∈ π such that B ∈ B and |B| ≤ 12 |B|;
C :=partition C where B is replaced by B and B \ B;
if π is unstable for B or B \ B
π 0 := refinement of π under B and B \ B;
For each block C ∈ π 0 with bottom states that were not bottom in π
split C until it is stable for all constellations in C;
π := π 0

5

DETAILED ALGORITHM

5

8

Detailed algorithm

This section presents the data structures, the algorithm to detect which blocks must be split, and the algorithm to split blocks. It follows the outline presented in the previous section.

5.1

Data structures

As a basic data structure, we use (singly-linked) lists. For a list L of elements, we assume that for each
element e, a reference to the position in L preceding the position of e is maintained, such that checking
membership and removal can be done in constant time. In some cases we add some extra information to
the elements in the list. Moreover, for each list L, we maintain pointers to its first and last element, and the
size |L|.
1. The current partition π consists of a list of blocks. Initially, it corresponds with π0 . All blocks are
part of a single initial constellation C 0 .
2. For each block B, we maintain the following:
(a) A reference B.constln to the constellation containing B.
(b) A list of the bottom states in B called B.btm-sts.
(c) A list of the remaining states in B called B.non-btm-sts.
(d) A list B.to-constlns of structures associated with constellations reachable via a transition from
some s∈B. Initially, it contains one element associated with C 0 . Each element associated with
some constellation C in this list also contains the following:
• A reference trans-list to a list of all transitions from states in B to states in C \ B (note
that transitions between states in B, i.e., inert transitions, are not in this list).
• When splitting the block B into B and B 0 there is a reference in each list element to the
corresponding list element in B 0 .to-constlns (which in turn refers back to the element in
B.to-constlns).
• In order to check for stability when splitting produces new bottom states, each element
contains a list to keep track of which new bottom states can reach the associated constellation.
(e) A reference B.inconstln-ref is used to refer to the element in B.to-constlns associated with
constellation B.constln.
Furthermore, when splitting a block B 0 in constellation B 0 under a constellation B and block B∈B,
the following temporary structures are used, with C the new constellation to which B is moved:
(a) A list B 0 .mrkd-btm-sts (initially empty) contains states in B 0 with a transition to B.
(b) A list B 0 .mrkd-non-btm-sts (initially empty) contains states that are marked, but are not bottom
states, i.e., each of those states has at least one transition to B and at least one transition to B 0 .
(c) A reference B 0 .constln-ref is used to refer to the (new) element in B 0 .to-constlns associated
with constellation C, i.e., the new constellation of B.
(d) A reference B 0 .coconstln-ref is used to refer to the element in B 0 .to-constlns associated with
constellation B, i.e., the old constellation of B.
(e) A list B 0 .new-btm-sts to keep track of the states that have become bottom states when B 0 was
split. This is required to determine whether B 0 is stable under all constellations after a split.
3. The constellations are represented by two lists. The first one, non-trivial-constlns, contains the
constellations encompassing two or more blocks of the current partition. The second one, trivialconstlns, contains constellations that match a block of the current partition. Initially, if the initial
partition π0 consists of one block, the constellation C 0 = {π0 } is added to trivial-constlns and
nothing needs to be done, because the initial partition is already stable. Otherwise C 0 is added to
non-trivial-constlns.

5

DETAILED ALGORITHM

9

4. For each constellation B, the following is maintained:
(a) A list B.blocks of blocks contained in B. Initially, the only constellation is C 0 .
(b) Counter B.size is used to keep track of the number of states in B; it is equal to ΣB∈B.blocks |B|.
5. Each transition s →
− s0 contains its source and target state. Moreover, it refers with to-constln-cnt to
a variable containing the number of transitions from s to the constellation in which s0 resides. For
each state and constellation, there is one such variable, provided there is a transition from this state
to this constellation.
Each transition s →
− s0 has a reference to the element associated with B in the list B.to-constlns
where s∈B and s0 ∈B. This is denoted as (s →
− s0 ).to-constln-ref. Initially, it refers to the single
element in B.to-constlns, unless the transition is inert, i.e., both s∈B and s0 ∈B.
Furthermore, each transition s →
− s0 is stored in the list of transitions from B to B. Initially, there is
such a list for each block in the initial partition π0 . From a transition s →
− s0 , the list can be accessed
0
via (s →
− s ).to-constln-ref.trans-list.
6. For each state s∈B we maintain the following information:
(a) A reference s.block to the block containing s.
(b) A static, i.e., not changing during the course of the algorithm, list s.Ttgt of transitions of the
form s →
− s0 containing precisely all the transitions from s.
(c) A static list s.Tsrc of transitions s0 →
− s containing all the transitions to s. In the sequel we
write such transitions as s ← s0 , to stress that these move into s.
(d) A counter s.inert-cnt containing the number of outgoing transitions to a state in the same block
as s. For any bottom state s, we have s.inert-cnt = 0.
(e) Furthermore, when splitting a block B 0 under B and B∈B, there are references s.constln-cnt
and s.coconstln-cnt to the variables that are used to count how many transitions there are from
s to B and from s to B \ B.

− s01 , s1 →
− s001
B1 .to-constlns C, •, • B, •, • trans-list B1 →
− C s1 →
B1 →
− B
B1 s2s0
2
s1

1

B1 .inconstln-ref
to-constln-ref

to-constln-cnt
2

B
B1 .btm-sts

s1

B1 .non-btm-sts

s2

s02

s001
s01
C

Figure 2: An example showing some of the data structures used in the detailed algorithm.
Figure 2 illustrates some of the used structures. A block B1 in constellation B contains bottom states
s1 , s02 and non-bottom state s2 . State s1 has two outgoing transitions s1 →
− s01 , s1 →
− s001 to states s01 ,
00
s1 in constellation C. This means that for both transitions, we have the following references:
(a) to-constln-cnt to the number of outgoing transitions from s1 to C.
(b) to-constln-ref to the element (C, •, •) in B1 .to-constlns, where C is the constellation reached
by the transitions, and the •’s are the (now uninitialized) references that are used when splitting.
(c) Via element (C, •, •), a reference trans-list to the list of transitions from B1 to C.

5

DETAILED ALGORITHM

10

Note that for the inert transition s2 →
− s02 , we only have a reference to the number of outgoing transitions from s2 to B, and that B1 .inconstln-ref refers to the element (B, •, •) associated with the
constellation containing B1 .

5.2

Finding the blocks that must be split

While non-trivial-constlns is not empty, we perform the algorithm listed in the following sections. To
determine whether the current partition π is unstable, we select a constellation B in non-trivial-constlns,
and we select a block B from B.blocks such that |B| ≤ 21 B.size. We first check which blocks are unstable
for B and B \ B.
1. We update the list of constellations w.r.t. B and B \ B.
(a) Move B into a new constellation C (with C.blocks empty and C.size = 0), by removing B
from B.blocks, adding it to C.blocks.
(b) Add C to trivial-constlns. If |B.blocks|=1, move B to trivial-constlns.
2. Walk through the elements in B.btm-sts and B.non-btm-sts, i.e., the states in B. For each state
s∈B visit all transitions s ← s0 ∈ s.Tsrc , and do the steps (a) to (d) below for each transition where
B 6= B 0 , with B 0 the block in which s0 resides.
(a) If B 0 .mrkd-btm-sts and B 0 .mrkd-non-btm-sts are empty:
i. Put B 0 in a list splittable-blks.
ii. Let B 0 .coconstln-ref refer to (s ← s0 ).to-constln-ref. Let B 0 .constln-ref refer to a new
element in B 0 .to-constlns.
(b) If s0 .coconstln-cnt is uninitialized, let s0 .constln-cnt refer to a new counter (with initial value
0), and let s0 .coconstln-cnt refer to (s ← s0 ).to-constln-cnt.
(c) If s0 6∈ B 0 .mrkd-btm-sts and s0 6∈ B 0 .mrkd-non-btm-sts, then:
i. If s0 is a bottom state, move s0 from B 0 .btm-sts to B 0 .mrkd-btm-sts.
ii. Else move s0 from B 0 .non-btm-sts to B 0 .mrkd-non-btm-sts.
(d) Increment the variable to which s0 .constln-cnt refers, and let (s ← s0 ).to-constln-cnt refer to
this variable. Decrement the variable referred to by s0 .coconstln-cnt. Move s ← s0 from
B 0 .coconstln-ref.trans-list to B 0 .constln-ref.trans-list, and let (s ← s0 ).to-constln-ref refer to
B 0 .constln-ref.
3. Next, check whether B itself can be split. First, mark all states by moving the states in B.btm-sts
to B.mrkd-btm-sts and those in B.non-btm-sts to B.mrkd-non-btm-sts. Add B to splittable-blks
and reset references B.constln-ref and B.coconstln-ref. Next, for each s∈B visit all transitions
s→
− s0 ∈ s.Ttgt , and do the steps (a) to (c) below for each transition where either B 0 = B or
B 0 = C, with B 0 the constellation in which s0 resides.
(a) If B 0 =B and B.constln-ref is uninitialized, let B.coconstln-ref refer to (s →
− s0 ).to-constln-ref,
add a new element for C to B.to-constlns, and let B.constln-ref and B.inconstln-ref refer to
this element.
(b) If s.coconstln-cnt is uninitialized, let s.constln-cnt refer to a new counter, and s.coconstln-cnt
to (s →
− s0 ).to-constln-cnt.
(c) If B 0 = B, increment the variable to which s.constln-cnt refers, let (s →
− s0 ).to-constln-cnt
refer to this variable, and decrement the variable referred to by s.coconstln-cnt.
4. Do the steps below for each B 0 ∈splittable-blks.
(a) If |B 0 .btm-sts| > 0 (there is at least one unmarked bottom state in B 0 ), the block must be split.
We leave B 0 in the list of splittable-blks.

5

DETAILED ALGORITHM

11

(b) Else, if B 0 .coconstln-ref.trans-list is not empty, and there is a state s∈B 0 .mrkd-btm-sts with
s.coconstln-cnt uninitialized or 0, the block must be split.
(c) Else, no splitting is required. Remove B 0 from splittable-blks and remove the temporary
markings of B 0 by doing steps i to iii below.
i. Move each s∈B 0 .mrkd-btm-sts to B 0 .btm-sts and reset s.constln-cnt and s.coconstln-cnt.
ii. Move each s∈B 0 .mrkd-non-btm-sts to B 0 .non-btm-sts. Reset s.constln-cnt.
If s.coconstln-cnt = 0, delete the variable to which s.coconstln-cnt refers.
Reset s.coconstln-cnt.
iii. Do the following steps for ref = constln-ref and ref = coconstln-ref, if B 0 .ref is initialized.
A. If |B 0 .ref.trans-list| = 0, then first reset B 0 .inconstln-ref if the element to which B 0 .ref
refers is associated with B 0 .constln, and second remove the element to which B 0 .ref
refers from B 0 .to-constlns and delete it.
B. Reset B 0 .ref.
5. If splittable-blks is not empty, start splitting (section 5.3). Else, carry on with finding blocks to split,
by selecting another non trivial constellation B and block B∈B, and continuing with step 1. If there
are no non trivial constellations left, the current partition is stable, the algorithm terminates.

5.3

Splitting the blocks

Splitting the splittable blocks is performed using the following steps. We walk through the blocks B 0 in
splittable-blks, which must be split into two or three blocks under constellation B and block B. For each
splitting procedure, we use time proportional to the smallest of the two blocks into which B 0 is split, where
one of the two smallest blocks can have size 0, and we also allow ourselves to traverse the marked states,
which is proportional to the time we used to mark the states in the previous step. Create new lists XB 0 ,
XB 00 , XB 000 to keep track of new bottom states when splitting.
If |B 0 .btm-sts| = 0 (all bottom states are marked), then we have split(B 0 , B) = B 0 , and can start with
step 3 below.
1. We start to split block B 0 w.r.t. B. We must determine whether split(B 0 , B) or cosplit(B 0 , B) is
the smallest. This is done by performing the following two procedures in lockstep, alternatingly
processing a transition. The entire operation terminates when one of the procedures terminates. If
one procedure acquires more states than 21 |B 0 |, it is stopped, and the other is allowed to terminate.
(a) The first procedure attempts to collect the states in split(B 0 , B).
i. Initialise an empty stack Q and an empty list L. Let D1 refer to the list consisting of
B 0 .mrkd-btm-sts and B 0 .mrkd-non-btm-sts. In the next step, we walk through the states in
D1 .
ii. Perform detect1 as long as |L| ≤ 12 |B 0 |:
A. While Q is not empty or we have not walked through all states in D1 , do the following
steps.
• If Q is empty, push the next state in D1 on Q and add it to L.
• Pop s from Q. For all s ← s0 ∈ s.Tsrc if s0 ∈ B 0 and s0 6∈ L, add s0 to L and push
s0 on Q.
(b) The second procedure attempts to collect the states in cosplit(B 0 , B). It uses a priority queue P ,
in which the priority of a state s represents the number of outgoing inert transitions to a target
state for which it has not yet been determined whether it is in cosplit(B 0 , B). If the priority of
a state s becomes 0, it is obvious that s must be in cosplit(B 0 , B).
i. Create an empty priority queue P and an empty list L0 . Let D2 refer to the list B 0 .btm-sts.
ii. Perform detect2 as long as |L0 | ≤ 12 |B 0 |:
A. While P has states with priority 0 or we have not walked through all states in D2 , do
the following steps.

5

DETAILED ALGORITHM

12

• If we have not walked through all states in D2 , let s be the next state in D2 . Else,
get a state with priority 0 from P , and let s be that state. Add s to L0 .
• For all s ← s0 ∈ s.Tsrc , do the following steps.
– If s0 ∈B 0 , s0 6∈P ∪L0 , and s0 6∈B 0 .mrkd-non-btm-sts (or s0 does not have a transition
to B \ B; this last condition is required when detect2 is invoked in 5.3.4.b and
5.3.7.b.i.B, and can be checked for s0 ∈mrkd-non-btm-sts by determining whether
the variable to which s0 .coconstln-cnt refers, minus s0 .inert-cnt if B 0 = B, is
larger than 0. Else, it can be checked by walking over the transitions s0 →
− s00 ∈
0
0
s.Ttgt ), add s with priority s .inert-cnt to P .
– If s0 ∈P , decrement the priority of s0 in P .
2. The next step is to actually carry out the splitting of B 0 . Create a new block B 00 with empty lists,
and add it to the list of blocks. Set B 00 .constln to B 0 .constln, and add B 00 to the list of blocks of that
constellation.
Depending on whether detect1 or detect2 terminated in the previous step, one of the lists L or L0
contains the states to be moved to B 00 . Below we refer to this list as N . For each s∈N , do the
following:
(a) Set s.block to B 00 , and move s from the list in which it resides in B 0 to the corresponding list
in B 00 .
(b) For each s →
− s0 ∈Ttgt , do the following steps.
i. If (s →
− s0 ).to-constln-ref is initialized, i.e., s →
− s0 is not inert, consider the list element l
in B 0 .to-constlns retrievable by (s →
− s0 ).to-constln-ref. Check whether there is a corresponding new element in B 00 .to-constlns. If so, l refers to this new element, which we call
l0 . If not, create it, add it to B 00 .to-constlns and call it also l0 , set the constellation in this
new l0 to that of l, set B 00 .inconstln-ref to l0 in case this constellation is B 00 .constln, set
B 00 .constln-ref to l0 in case l refers to B 0 .constln-ref, set B 00 .coconstln-ref to l0 in case l
refers to B 0 .coconstln-ref, and let l and l0 refer to each other. Move s →
− s0 from l.trans-list
0
0
0
to l .trans-list and let (s →
− s ).to-constln-ref refer to l .
0
0
ii. Else, if s ∈B \ N (an inert transition becomes non-inert):
A. Decrement s.inert-cnt.
B. If s.inert-cnt=0, add s to XB 00 , move s from B 00 .non-btm-sts or B 00 .mrkd-non-btm-sts
to the corresponding bottom states list in B 00 . If B 00 .inconstln-ref is uninitialized,
create a new element for B 00 .constln, add it to B 00 .to-constlns, let B 00 .inconstln-ref
refer to that element, and if B 0 .inconstln-ref is initialized, let B 0 .inconstln-ref and
B 00 .inconstln-ref refer to each other. Add s →
− s0 to B 00 .inconstln-ref. trans-list and let
0
00
(s →
− s ).to-constln-ref refer to B .inconstln-ref.
(c) For each s ← s0 ∈ Tsrc , s0 ∈ B 0 \ N (an inert transition becomes non-inert):
i. Decrement s0 .inert-cnt.
ii. If s0 .inert-cnt=0, add s0 to XB 0 , and move s0 from B 0 .non-btm-sts or B 0 .mrkd-non-btm-sts
to the corresponding bottom states list in B 0 . If B 0 . inconstln-ref is uninitialized, create a
new element for constellation B 0 .constln and add it to B 0 .to-constlns, let B 0 .inconstln-ref
refer to that element, and if B 00 .inconstln-ref is initialized, let B 0 .inconstln-ref and B 00 .
inconstln-ref refer to each other. Add s ← s0 to B 0 .inconstln-ref. trans-list and let (s ← s0 ).
to-constln-ref refer to B 0 .inconstln-ref.
3. For each element l in B 00 .to-constlns referring to an element l0 in B 0 .to-constlns, do the following
steps.
(a) If l0 .trans-list is empty and l0 does not refer to B 0 .constln-ref and not to B 0 . coconstln-ref, reset
B 0 .inconstln-ref if l0 is associated with B 0 .constln, remove l0 from B 0 .to-constlns and delete it.
(b) Else, reset the reference from l0 to l.

5

DETAILED ALGORITHM

13

(c) Reset the reference from l to l0 .
4. Next, we must consider splitting split(B 0 , B) under B \B, or if B 0 was stable under B, we must split
B 0 under B \ B. Define C = split(B 0 , B). If B 0 was not split, then C = B 0 . C is stable under B \ B
if C.coconstln-ref is uninitialized or C.coconstln-ref.trans-list is empty or for all s∈C.mrkd-btm-sts
it holds that s.coconstln-cnt > 0. If this is not the case, then we must determine which of the blocks
split(C, B \ B) or cosplit(C, B \ B) is the smallest in a time proportional to the smallest of the two.
This is again done by simultaneously iterating over the transitions of states in both sets in lockstep.
The entire operation terminates when one of the two procedures terminates. If one of the procedures
acquires more than 21 |C| states, that procedure is stopped, and the other is allowed to terminate.
(a) The first procedure attempts to collect the states in split(C, B \ B).
i. Create an empty stack Q and an empty list L. Let D1 be the list of states s occurring in
some s →
− s0 in the list split(B 0 , B).coconstln-ref.trans-list (in practice we walk over D1
by walking over the latter list).
ii. Perform detect1 with B 0 = C.
(b) The second procedure attempts to collect the states in cosplit(C, B \ B).
i. Create an empty priority queue P and an empty list L0 . Let D2 be the list of states s with
s.coconstln-cnt = 0 in C.mrkd-btm-sts (in practice we walk over the latter list and check
the condition).
ii. Perform detect2 with B 0 = C.
Finally, we split C by moving either split(C, B \ B) or cosplit(C, B \ B) to a new block B 000 ,
depending on which of the two is the smallest. This can be done by using the procedure described
in steps 2 and 3, where in step 2.b.ii.B, we fill a state list XB 000 instead of XB 00 , and in 2.c.ii, we
possibly add states to XC instead of XB 0 (we define XC = XB 0 if C = B 0 , otherwise XC = XB 00 ).
We move all states in XC that are now in B 000 to XB 000 .
5. Remove the temporary markings of each block C resulting from the splitting of B 0 (see steps 5.2.4.c.i
to iii).
6. If the splitting of B 0 resulted in new bottom states (either XB 0 , XB 00 , or XB 000 is not empty), check
for those states whether further splitting is required. This is the case if from some new bottom states,
not all constellations can be reached which can be reached from the block. Perform the following for
B̂ = B 0 , B 00 , and B 000 , and all s ∈ XB̂ :
(a) For all s →
− s0 ∈ Ttgt (s0 ∈ B 0 ):
i. If it does not exist, create an empty list SB 0 and associate it with B 0 in B̂.to-constlns
(accessible via (s →
− s0 ).to-constln-ref), and move B 0 to the front of B̂.to-constlns.
ii. If s 6∈ SB 0 , add it.
(b) Move s from XB̂ to B̂.new-btm-sts.
7. Check if there are unstable blocks that require further splitting, and if so, split further. Repeat this
until no further splitting is required. A stack Q0 is used to keep track of the blocks that require
checking. For B̂ = B 0 , B 00 , and B 000 , push B̂ on Q0 if |B̂.new-btm-sts| > 0. While Q0 is not empty,
perform steps a to c below.
(a) Pop block B̂ from Q0 .
(b) Find a constellation under which B̂ is not stable by walking through the B ∈ B̂.to-constlns. If
|SB | < |B̂.new-btm-sts|, then further splitting is required under B:
i. Find the smallest subblock of B̂ by performing the following two procedures in lockstep.
A. The first procedure attempts to collect the states in split(B̂, B).

6

APPLICATION TO BRANCHING BISIMULATION

14

• Create an empty stack Q and an empty list L. Let D1 be the list of states s occurring
in some s →
− s0 with s0 ∈B in the list trans-list associated with B∈B̂.to-constlns (in
practice we walk over D1 by walking over trans-list).
• Perform detect1 with B 0 = B̂.
B. The second procedure attempts to collect the states in cosplit(B̂, B).
• Create an empty priority queue P and an empty list L0 . Let D2 be the list of states
s∈B̂.new-btm-sts \ SB .
• Perform detect2 with B 0 = B̂.
ii. Continue the splitting of B̂ by performing step 2 to produce a new block B̂ 0 and a list
of new bottom states XB̂ 0 . Move all states in B̂.new-btm-sts that have moved to B̂ 0 to
B̂ 0 .new-btm-sts. Update the SB lists by walking over the l∈B̂.to-constlns and doing the
following steps as long as an empty SB is not encountered. Note that the l still refer to
corresponding elements l0 in B̂ 0 .to-constlns.
A. For all s∈SB , if s∈B̂ 0 , then insert s in the SB associated with l0 (if this list does not
exist yet, create it, and move l0 to the front of B̂ 0 .to-constlns) and remove s from the
SB associated with l.
B. If the SB of l is now empty, remove it, and move l to the back of B̂.to-constlns.
iii. Perform step 3 for elements l0 in B̂ 0 .to-constlns referring to an element l in B̂.to-constlns.
Skip steps 4 and 5, and continue with step 6 for B̂, B̂ 0 , XB̂ and XB̂ 0 .
iv. Push B̂ on Q0 if |B̂.new-btm-sts| > 0 and B̂ 0 on Q0 if |B̂ 0 .new-btm-sts| > 0.
(c) If no further splitting was required for B̂, empty B̂.new-btm-sts and remove the remaining SB
associated with constellations B∈B̂.to-constlns.
8. If B 0 .constln∈trivial-constlns, move it to non-trivial-constlns.

6

Application to branching bisimulation

We show that the algorithm can also be used to determine branching bisimulation, using the transformation
from [14, 17], with complexity O(m(log |Act| + log n)). Branching bisimulation is typically applied to
labelled transition systems (LTSs).
Definition 6.1 (Labeled transition system). A labeled transition system (LTS) is a three tuple A =
(S, Act, →
− ) where
1. S is a finite set of states. The number of states is generally denoted by n.
2. Act is a finite set of actions including the internal action τ .
3. →
− ⊆ S × Act × S is a transition relation. The number of transitions is generally denoted as by m.
a

It is common to write t −
→ t0 for (t, a, t0 ) ∈ →
− .
There are various, but equivalent, ways to define branching bisimulation. We use the definition below.
Definition 6.2 (Branching bisimulation). Consider the labeled transition system A = (S, Act, →
− ). We
call a symmetric relation R ⊆ S × S a branching bisimulation relation iff for all s, t ∈ S such that s R t,
the following conditions hold for all actions a ∈ Act:
a

1. If s −
→ s0 , then
(a) Either a = τ and s0 R t, or
τ

τ

a

(b) There is a sequence t −
→ ··· −
→ t0 of (zero or more) τ -transitions such that s R t0 and t0 −
→ t00
with s0 R t00 .

7

EXPERIMENTS

15

Figure 3: Runtime results for (a·τ )size sequences (left) and trees of depth size (right)
Two states s and t are branching bisimilar iff there is a branching bisimulation relation R such that s R t.
Our new algorithm can be applied to an LTS by translating it to a Kripke structure.
Definition 6.3 (LTS embedding). Let A = (S, Act, →
− ) be an LTS. We construct the embedding of A to
be the Kripke structure KA = (SA , AP , →
− , L) as follows:
a

1. SA = S ∪ {ha, ti | s −
→ t for some t ∈ S}.
2. AP = Act ∪ {⊥}.
3. →
− is the least relation satisfying (s, t ∈ S, a ∈ Act \ τ ):
a

s−
→t
s→
− ha, ti

τ

ha, ti →
− t

s−
→t
s→
− t

4. L(s) = {⊥} for s ∈ S and L(ha, ti) = {a}.
The following theorem stems from [14].
Theorem 6.4. Let A be an LTS and KA its embedding. Then two states are branching bisimilar in A iff
they are divergence-blind stuttering equivalent in KA .
If we start out with an LTS with n states and m transitions then its embedding has at most m + n states and
2m transitions. Hence, the algorithm requires O(m log(n+m)) time. As m is at most |Act|n2 this is also
equal to O(m(log |Act|+ log n)).
A final note is that the algorithm can also easily be adapted to determine divergence-sensitive branching
bisimulation [8], by simply adding a self loop indicating divergence to those states on a τ -loop, similar to
the way stuttering equivalence is calculated using divergence-blind stuttering equivalence.

7

Experiments

The new algorithm has been implemented as part of the mCRL2 toolset [6], which offers implementations
of GV and the algorithm by Blom & Orzan [2] that distinguishes states by their connection to blocks via
their outgoing transitions. We refer to the latter as BO. The performance of GV and BO can be very
different on concrete examples. We have extensively tested the new algorithm by applying it to thousands
of randomly generated LTSs and comparing the results with those of the other algorithms.
We experimentally compared the performance of GV, BO, and the implementation of the new algorithm (GW). All experiments involve the analysis of LTSs, which for GW are first transformed to Kripke

7

EXPERIMENTS

16

structures using the translation of section 6. The reported runtimes do not include the time to read the input
LTS and write the output, but the time it takes to translate the LTS to a Kripke structure and to reduce
strongly connected components is included.
Practically all experiments have been performed on machines running C ENT OS L INUX, with an I NTEL
E5-2620 2.0 GHz CPU and 64 GB RAM. Exceptions to this are the final two entries in table 1, which were
obtained by using a machine running F EDORA 12, with an I NTEL X EON E5520 2.27 GHz CPU and 1 TB
RAM.
Figure 3 presents the runtime results for two sets of experiments designed to demonstrate that GW has
the expected scalability. At the left are the results of analysing single sequences of the shape (a·τ )n . As the
length 2n of such a sequence is increased, the results show that the runtimes of both BO and GV increase
at least quadratically, while the runtime of GW grows linearly. All algorithms require n iterations, in which
BO and GV walk over all the states in the sequence, but GW only moves two states into a new block. At
the right of figure 3, the results are displayed of analysing trees of depth n that up to level n−1 correspond
with a binary tree of τ -transitions. Each state at level n−1 has a uniquely labelled outgoing transition to a
state in level n. This example is particularly suitable for BO which only needs one iteration to obtain the
stable partition. Still GW beats BO by repeatedly splitting off small blocks of size 2(k − 1) if a state at
level k is the splitter.
Table 1 contains results for minimising LTSs from the VLTS benchmark set2 and the mCRL2 toolset3 .
For each case, the best runtime result has been highlighted in bold. Some characteristics of each case are
given on the left, in particular the number of states (n) and transitions (m) in the original LTS and the
number of states (min. n) and transitions (min. m) in the minimized LTS.
The final two cases stem from mCRL2 models distributed with the mCRL2 toolset as follows:
• dining 14 is an extension of the Dining Philosophers model to fourteen philosophers;
• 1394-fin3 extends the 1394-fin model to three processes and two data elements.
The experiments demonstrate that also when applied to actual state spaces of real models, GW generally
outperforms the best of the other algorithms, often with a factor 10 and sometimes with a factor 100. This
difference tends to grow as the LTSs get larger. GW’s memory usage is only sometimes substantially higher
than GV’s and BO’s, which surprised us given the amount of required bookkeeping.

2 http://cadp.inria.fr/resources/vlts.
3 http://www.mcrl2.org.

Model
vasy 40
vasy 65
vasy 66
vasy 69
vasy 116
vasy 157
vasy 164
vasy 166
cwi 214
cwi 371
cwi 566
vasy 574
cwi 2165
cwi 2416
vasy 2581
vasy 4220
vasy 4338
vasy 6020
vasy 6120
cwi 7838
vasy 8082
vasy 11026
vasy 12323
cwi 33949
dining 14
1394-fin3

n
40,006
65,537
66,929
69,754
116,456
157,604
164,865
166,464
214,202
371,804
566,640
574,057
2,165,446
2,416,632
2,581,374
4,220,790
4,338,672
6,020,550
6,120,718
7,838,608
8,082,905
11,026,932
12,323,703
33,949,609
18,378,370
126,713,623

min. n
20,003
65,536
51,128
69,753
22,398
3,038
992
42,195
478
2,134
198
3,577
4,256
730
704,737
1,186,266
704,737
256
2,505
62,031
290
775,618
876,944
12,463
228,486
160,258

min. m
40,004
2,621,440
1,018,692
520,632
87,674
12,095
3,456
197,200
1,612
5,634
791
16,168
20,880
2,899
3,972,600
6,863,329
3,972,600
510
5,358
470,230
680
2,454,834
2,780,022
71,466
2,067,856
538,936

time GV
142.77
239.67
7.42
3.98
3.84
6.98
3.89
21.60
0.87
42.70
1683.28
105.10
80.56
1,679.55
2,592.74
3,643.08
5,290.54
130.76
546.11
745.33
288.45
5,005.61
5,997.26
1,684.56
1,264.67
229,217.0

me. GV
65
437
208
155
95
97
251
153
140
179
454
1,766
1,403
1,932
1,690
2,054
2,258
2,045
1,893
6,319
6,098
3,642
4,068
21,951
20,155
26,000

time BO
762.69
47.88
16.16
12.65
15.73
6.80
20.20
6.20
29.92
17.37
26.24
487.01
387.93
59.29
463.52
863.74
587.87
95.76
291.30
11,667.98
677.28
2,555.30
2,068.52
11,635.09
3,010.17
15,319.00

me. BO
62
645
356
171
128
110
316
177
197
261
531
2,192
2,409
2,660
2,344
2,951
3,026
3,482
2,300
11,027
7,824
5,235
5,770
42,162
31,201
75,000

Table 1: Runtime (in sec.) and memory use (in MB) results for GV, BO, and GW

m
60,007
2,621,480
1,302,664
520,633
368,569
297,000
1,619,204
651,168
684,419
641,565
3,984,157
13,561,040
8,723,465
17,605,592
11,442,382
13,944,372
15,666,588
19,353,474
11,031,292
59,101,007
42,933,110
24,660,513
27,667,803
165,318,222
164,329,284
276,426,688

time GW
0.34
20.07
9.05
4.53
2.68
1.08
5.38
3.89
2.64
3.12
19.94
40.18
59.49
90.69
76.16
119.20
109.21
45.54
81.05
617.46
200.72
225.20
256.70
1,459.92
1,100.91
1,516.00

me. GW
93
2,481
853
493
142
129
246
376
140
168
454
1,495
1,948
1,932
5,098
7,287
6,927
2,045
3,392
14,456
6,108
10,394
11,575
37,437
20,155
45,000

7
EXPERIMENTS
17

REFERENCES

18

References
[1] A. Aho, J. Hopcroft and J. Ullman. The Design and Analysis of Computer Algorithms. AddisonWesley, 1974.
[2] S.C. Blom and S. Orzan. Distributed Branching Bisimulation Reduction of State Spaces. In
FMICS’03, ENTCS 80, pp. 109-123. Elsevier, 2003.
[3] S.C. Blom and J.C. van de Pol. Distributed Branching Bisimulation Minimization by Inductive Signatures. In PDMC’09, EPTCS 14, pp. 32-46. Open Publ. Association, 2009.
[4] M.C. Browne. E.M. Clarke and O. Grumberg. Characterizing finite Kripke structures in propositional
temporal logic. Theoretical Computer Science 59(1,2):115-131, 1988.
[5] K. Chatterjee and M. Henzinger. Faster and Dynamic Algorithms for Maximal End-Component Decomposition and Related Graph Problems in Probabilistic Verification. In SODA’11, pp. 1318-1336.
SIAM, 2011.
[6] S. Cranen, J.F. Groote, J.J.A. Keiren, F.P.M. Stappers, E.P. de Vink, J.W. Wesselink, and
T.A.C. Willemse. An overview of the mCRL2 toolset and its recent advances. TACAS’13, LNCS
7795, pp. 199-213, Springer, 2013. See also www.mcrl2.org.
[7] H. Garavel, F. Lang, R. Mateescu and W. Serwe. CADP 2011: A Toolbox for the Construction and
Analysis of Distributed Processes. Software Tools for Technology Transfer 15(2):98-107, 2013.
[8] R.J. van Glabbeek and W.P. Weijland. Branching time and abstraction in bisimulation semantics.
Journal of the ACM 43(3):555–600, 1996.
[9] J.F. Groote and F.W. Vaandrager. An efficient algorithm for branching bisimulation and stuttering
equivalence. In ICALP’90, LNCS 443, pp. 626-638. Springer, 1990.
[10] J.F. Groote and M.R. Mousavi. Modeling and Analysis of Communicating Systems. The MIT Press,
2014.
[11] P. Kannelakis, S. Smolka. CCS Expressions, Finite State Processes and Three Problems of Equivalence. Information and Computation 86:43-68, 1990.
[12] W. Li. Algorithms for Computing Weak Bisimulation Equivalence. In TASE’09, pp. 241-248. IEEE,
2009.
[13] R. Milner. Calculus of Communicating Systems. Lecture Notes in Computer Science 92. SpringerVerlag 1980.
[14] R. De Nicola and F.W. Vaandrager. Three logics for branching bisimulation. Journal of the ACM
42:458-487, 1995.
[15] R. Paige and R.E. Tarjan. Three partition refinement algorithms. SIAM Journal of Computation
16(6):973-989, 1987.
[16] F. Ranzato and F. Tapparo. Generalizing the Paige-Tarjan Algorithm by Abstract Interpretation. Information and Computation 206(5):620-651, 2008.
[17] M.A. Reniers, R. Schoren, and T.A.C. Willemse. Results on embeddings between state-based and
event-based systems. The Computer Journal 57(1):73-92, 2014.
[18] H. Virtanen, H. Hansen, A. Valmari, J. Nieminen and T. Erkkilä. Tampere Verification Tool. In
TACAS’04, LNCS 2988, pp. 153-157. Springer, 2004.
[19] A.J. Wijs. GPU Accelerated Strong and Branching Bisimilarity Checking. In TACAS’15, LNCS 9035,
pp. 368-383. Springer, 2015.

