=Paper=
{{Paper
|id=Vol-3284/9606
|storemode=property
|title=Incremental NFA Minimization
|pdfUrl=https://ceur-ws.org/Vol-3284/9606.pdf
|volume=Vol-3284
|authors=Brian Riccardi,Riccardo Romanello,Alberto Policriti,Christian Bianchini
|dblpUrl=https://dblp.org/rec/conf/ictcs/RiccardiRPB22
}}
==Incremental NFA Minimization==
https://ceur-ws.org/Vol-3284/9606.pdf
Incremental NFA Minimization
Christian Bianchini1 , Alberto Policriti1,* , Brian Riccardi1 and Riccardo Romanello1
1
University of Udine, Italy
Abstract
Finite state automata are fundamental objects in Theoretical Computer Science and find their application
in Text Processing, Compilers Design, Artificial Intelligence and many other areas. The problem of
minimizing such objects can be traced back to the β50s and since then it has been the arena for developing
new algorithmic ideas. There are two main paradigms to tackle the problem: top down β which builds
a descending chain of equivalences by subsequent refinements β and bottom up β which builds an
ascending chain of equivalences by aggregation of classes. The former approach leads to a fast πͺ(π log π)
algorithm, whereas the latter is currently quadratic for any practical application. Nevertheless, the
bottom up algorithm enjoys the property of being incremental, i.e. the minimization process can be
stopped at any time obtaining a language-equivalent partially minimized automaton. In this work we
correct a small mistake in the algorithm given by Almeida et al. in 2014 and we propose a simple, DFS-like
and truly quadratic incremental algorithm for minimizing deterministic automata. Furthermore, we
adapt the idea to the nondeterministic case obtaining an incremental algorithm which computes the
maximum bisimulation relation in time πͺ(π2 π|Ξ£|), where π is the number of states, Ξ£ is the alphabet
and π is the degree of nondeterminism, improving by a factor of π the running time of the fastest known
aggregation based algorithm for this problem.
Keywords
Automata, Bisimulation, Minimization, Incremental
1. Introduction
Finite state automata are fundamental objects in Theoretical Computer Science and find their
application in Text Processing, Compilers Design, Artificial Intelligence and many other areas.
The minimization of an automaton is the process of constructing a new (language-equivalent)
automaton which is minimal in the number of states. This problem can be traced back to the
β50s by the work of Moore [1]. A fundamental result in Automata Theory is the Myhill-Nerode
Theorem [2], establishing that in the deterministic case this minimal automaton is in fact the
minimum, up to isomorphism. In the wider setting of nondeterministic automata there is no
analog result and finding any state-minimal automaton is PSPACE-complete [3]. For this reason,
a practical alternative is the minimization with respect to bisimulation. Bisimilarity is indeed
Proceedings of the 23rd Italian Conference on Theoretical Computer Science, Rome, Italy, September 7-9, 2022
*
Corresponding author.
" bianchini.christian@spes.uniud.it (C. Bianchini); alberto.policriti@uniud.it (A. Policriti);
riccardi.brian@spes.uniud.it (B. Riccardi); riccardo.romanello@uniud.it (R. Romanello)
~ http://users.dimi.uniud.it/~alberto.policriti/home (A. Policriti); https://riccardoromanello.github.io
(R. Romanello)
0000-0002-2855-1221 (R. Romanello)
Β© 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
CEUR
Workshop
Proceedings
http://ceur-ws.org
ISSN 1613-0073
CEUR Workshop Proceedings (CEUR-WS.org)
1
Christian Bianchini et al. CEUR Workshop Proceedings 1β13
a valid choice since in the deterministic case two states are bisimilar if and only if they are
Myhill-Nerode equivalent.
Thus, the problem of minimizing automata reduces to the problem of computing bisimilarity
between states, which in turn is equivalent to determining the coarsest partition of a set stable
with respect to some binary relation. The two main paradigms to compute the aforementioned
partition are top down and bottom up.
Top down algorithms start with the partition that separates states between final and non final
and subsequently refine the partition until it is stable. By a careful choice of which block of the
partition to split at each refining step, Paige and Tarjan [4] devised an algorithm that computes
the maximum bisimulation equivalence in time πͺ(π log π), where π is the number of states and
π is the number of transitions. The iconic Hopcroftβs Algorithm [5] (which Paige and Tarjanβs
solution is based on) deals with the special case of deterministic automata. Furthermore, it has
recently been proved that the bisimilarity computation requires β¦(π log π) time assuming top
down algorithms [6].
On the contrary, bottom up solutions start with the finest partition β the one where each
state constitutes a singleton β and proceed by subsequently merging two blocks found to be
equivalent. For this reason, the technique is also known in the literature as partition-aggregation.
The main advantage of this paradigm is that the algorithm is incremental, i.e. it proceeds in
subsequent stages where at the end of each merging step the resulting automaton is language-
equivalent to the input one. In this way, the minimization process can be stopped at any
time and can be resumed later. The first algorithm of this kind is due to Watson [7]. After a
series of improvements Watson and Daciuk [8] reduced the running time to πͺ(π2 |Ξ£|πΌ(π)) for
deterministic automata with π states, alphabet Ξ£ and where πΌ(π) is related to the inverse of
Ackermannβs function [9] which can be treated as a constant for any practical value of π1 . The
main idea is to propagate the definition of bisimilarity: if states π and π are equivalent, then
also their transitions by the same character must lead to equivalent states. This is done by a
recursive function Equiv which resembles an equivalence algorithm by Hopcroft and Karp [10].
A subsequent work by Almeida et al. [11] aimed at simplifying the algorithm by Watson and
Daciuk maintaining its running time. Unfortunately, there is a small mistake in their version of
Equiv which leads to a β¦(π3 ) algorithm in the worst case.
Above algorithms are focused on the minimization of deterministic automata. The nonde-
terministic case was tackled by BjΓΆrklund and Cleophas [12] adapting ideas from Watson and
Daciuk. They devised an incremental algorithm for computing bisimilarity in time πͺ(π2 π2 |Ξ£|),
where π is the degree of nondeterminism.
In this work we correct the algorithm by Almeida et al. providing a simplified version of
the one by Watson and Daciuk and maintaining the quadratic running time. The solution is
based on the concept of associated graph whose purpose is twofold: to distill the behaviour of
the aforementioned algorithms by interpreting them as graph colorings and to design our own
incremental procedure. Having established the clear connection between minimization and
graph coloring it is natural to generalize the algorithm for solving the bisimilarity problem on
nondeterministic automata. Furthermore, the proposed solution improves by a factor of π the
running time of BjΓΆrklund and Cleophas [13].
16
1
It holds πΌ(π) β€ 5 for π β€ 22 .
2
Christian Bianchini et al. CEUR Workshop Proceedings 1β13
The paper is organized as follows: in the next section we give the basics about partitions,
relations, and automata. In Section 3 we briefly describe the algorithm by Almeida et al. and
we point out the mistake. In Section 4 we introduce our procedure on the deterministic case.
Finally, in Section 5 we lift the algorithm to the nondeterministic case. Some conclusions are
drawn in Section 6.
2. Preliminaries
2.1. Relations and Partitions
A binary relation from set π΄ to set π΅ is a subset π β π΄ Γ π΅. Its size will be denoted by |π|. We
say that π β π΄ is in relation with π β π΅ whenever (π, π) β π, and we denote this by writing πππ.
If we consider binary relations over π΄ (i.e. subsets of π΄ Γ π΄), it remains defined the identity
relation ππ΄ = {(π, π) : π β π΄}.
An equivalence relation (or equivalence) is a relation which is reflexive, symmetric and
transitive. Given π β π΄, the equivalence class of π is the set [π] = {π : πππ}. The quotient set
π΄/π = {[π] : π β π΄} forms a partition of π΄.
2.2. Languages and Automata
An alphabet is a non-empty set Ξ£ of symbols. A string is a finite sequence π€ = π€1 . . . π€π of
symbols. Ξ£* is the set of all finite length strings of symbols in Ξ£ and we call a subset πΏ β Ξ£* a
language. β¨οΈ β©οΈ
A nondeterministic finite state automaton (NFA) is π© = π, Ξ£, π0 , πΏ, πΉ where π is a non-
empty finite set of states, Ξ£ is the alphabet, π0 is the initial state, πΏ : π Γ Ξ£ β 2π is the
transition function and πΉ β π is the set of final states. The degree of nondeterminism is
π = maxπ₯βΞ£,πβπ {|πΏ(π, π₯)|}. We say that π© is complete if |πΏ(π, π₯)| β₯ 1 for every state and
symbol. In what follows we will assume complete automata: this is not a loss of generalities
since it is always possible to complete an automaton by adding one state and suitable transitions.
As usual, the transition function can be recursively extended to strings, i.e. πΏ * : π Γ Ξ£* β 2π ,
still denoted by πΏ.
We say that state π β π accepts a string π€ β Ξ£* if πΏ(π, π€) β© πΉ ΜΈ= β
. The set of strings
accepted by π is denoted by πΏ(π). The language accepted by the automaton is πΏ(π© ) = πΏ(π0 ).
A minimal automaton accepting πΏ has the minimum number of states amongst all automata
accepting πΏ.
A deterministic finite state automaton (DFA) is a NFA π with the added condition that for
each symbol π₯ and each state π, |πΏ(π, π₯)| = 1.
For an automaton π© we define the equivalence relation βΌ β π Γ π as:
π βΌ π ββ πΏ(π) = πΏ(π)
If π ΜΈβΌ π we say they are distinguishable and if exactly one of the two is final we say they are
trivially distinguishable.
β¨οΈ Given a NFA π© and β©οΈ an equivalence π over its states, its quotient is defined as π© /π =
π/π, Ξ£, [π0 ], πΏπ , πΉ/π where πΏπ ([π], π₯) = {[π β² ] | π β² β πΏ(π, π₯)}. The Myhill-Nerode Theorem
3
Christian Bianchini et al. CEUR Workshop Proceedings 1β13
[2] estabilishes that the quotient automaton π/ βΌ is well defined and is the unique (up to
isomorphism) minimal automaton recognizing πΏ(π).
Definition 1. Given a NFA, a bisimulation is a binary relation over its states such that, for every
pair (π, π) β π΅:
B1. π β πΉ ββ π β πΉ ,
B2. βπ₯ β Ξ£ βπβ² β πΏ(π, π₯) βπ β² β πΏ(π, π₯) β§ (πβ² , π β² ) β π΅,
B3. βπ₯ β Ξ£ βπ β² β πΏ(π, π₯) βπβ² β πΏ(π, π₯) β§ (πβ² , π β² ) β π΅.
Two states π and π are said bisimilar if there exists a bisimulation which contains (π, π). The set of
all bisimulations over the states of π© is denoted by Bπ© .
The union of two bisimulation is also a bisimulation. In fact, the following generalization of
this observation is a well-known result.
Lemma 1. Bπ© is closed under union and has a unique largest bisimulation β¬, which will be called
bisimilarity, it is an equivalence relation, and it relates all and only bisimilar states. β¬ β βΌ and if
π© is deterministic, β¬ coincides with βΌ.
The above properties β combined with efficient algorithms to compute it β justify the use of
β¬ as an approximation of βΌ for nondeterministic automata.
2.3. Partition Aggregation
Given an automaton π© , our goal is to compute the bisimilarity relation β¬ over its set of states, so
that the resulting quotient π© /β¬ can be returned as the minimized version of π© . The partition-
aggregation strategy will compute an ascending chain π β π΅1 β . . . β π΅π = β¬ of
bisimulation-equivalences.
A partition-aggregation algorithm proceeds by a sequence of merging steps where at each
step π the bisimulation π΅π is computed. Since each π΅π is a bisimulation, the minimization process
can be stopped at any step obtaining a language-equivalent automaton with no more states than
the input one; the minimization process can be resumed later from this intermediate automaton.
In this sense, the algorithm is incremental. This property is not shared with top down algorithms
that proceed by partition-refinement β such as Hopcroftβs Algorithm and its many successors β
where only the final result is a bisimulation.
3. The Algorithm Proposed by Almeida et al.
This section is devoted to a brief description of the algorithm proposed by Almeida et al. It
uses the union-find [14, 9] data structure to manage the partition of states, so that finding and
merging classes with the Find and Union primitives can be done in πͺ(πΌ(π)).
Pairs of states are recursively considered until their equivalence is estabilished. Intermediate
results are cached, so that queries on pairs of states already found to be (non-)equivalent can be
answered in constant time.
4
Christian Bianchini et al. CEUR Workshop Proceedings 1β13
Algorithm 1 Aggregation-based minimization by Almeida et al.
1: function MinimizeAlmeida(π, πΏ, πΉ ) 21: function Equiv(π, π)
2: for all π β π do 22: if (π, π) β πΈ then
3: Make(π) 23: return β₯
4: πΈ β (πΉ Γ πΉ c ) βͺ (πΉ c Γ πΉ ) 24: if (π, π) β π» then
5: 25: return β€
6: for all (π, π) β π Γ π do 26:
7: π π β Find(π) 27: π» β π» βͺ {(π, π), (π, π)}
8: π π β Find(π) 28: for all π₯ β Ξ£ do
9: if π π ΜΈ= π π β§ (π, π) ΜΈβ πΈ then 29: (πβ² , π β² ) β (Find(πΏ(π, π₯)),Find(πΏ(π, π₯)))
10: πΈββ
30: if πβ² ΜΈ= π β² β§ (πβ² , π β² ) ΜΈβ πΈ then
11: π»ββ
31: πΈ β πΈ βͺ {(πβ² , π β² ), (π β² , πβ² )}
12: if Equiv(π, π) then 32: if Β¬Equiv(πβ² , π β² ) then
13: for all (πβ² , π β² ) β πΈ do 33: return β₯
14: Union(πβ² , π β² ) 34:
15: else 35: π» β π» β {(π, π), (π, π)}
16: πΈ βπΈβͺπ» 36: πΈ β πΈ βͺ {(π, π), (π, π)}
17: 37: return β€
18: π« β {ClassOf(π) : π β π} 38: end function
19: return π«
20: end function
At lines 2β3, the identity relation is constructed and pairs of trivially non-equivalent states
are added to the memoization table πΈ. In the main loop at lines 6β16, we iterate over all pairs
of states to check for equivalence. If a pair is either on the same class β i.e. is a pair of states
already found to be equivalent β or is in the memoization table β i.e. is a pair of distinguishable
states β the minimization continues to the next iteration. Otherwise, two empty collections πΈ
and π» are prepared, respectively the set of wondering pairs of states and the history pairs. πΈ
and π» are considered global variables and can be accessed from Equiv. The recursive function
Equiv is responsible for checking if states π, π are equivalent and, if so, pairs in πΈ are merged.
Otherwise, all visited pairs are set to be distinguishable and this information is used to update
πΈ. At the end the partition in equivalence classes is returned.
The underlying idea of Equiv(π, π) is to recursively check the transitions from π and π on all
symbols. If two states are found to be cached as distinguishable, the recursion stops returning
β₯. If they are found to be in visit, it is useless to continue the visit and nothing can be said (i.e.
Equiv returns β€ postponing the decision to the upper-level of the recursion). These preliminary
checks are at lines 22β25. Next, each π₯-transition is checked recursively in the loop at 28β33,
stopping when the states are found to be distinguishable. At the end, if π and π are not found to
be distinguishable, the pair is removed from the history π» and added to the βwonderingβ pairs
πΈ and β€ is returned.
Detailed proof of the algorithmβs correctness can be found in [11].
On the complexity analysis, the authors claim that the algorithm terminates in time
πͺ(π2 |Ξ£|πΌ(π)). This comes from the assumption that each pair visited during the recursion
of Equiv will be skipped on the subsequent iterations of MinimizeAlmeida (cf. [11, Lemma
4.9]). The assumption is wrong and a family of counterexamples can be constructed such that
MinimizeAlmeida terminates in time Ξ(π3 |Ξ£|πΌ(π)) (see Fig 1).
5
Christian Bianchini et al. CEUR Workshop Proceedings 1β13
start 1 Figure 1: A small counterexample of [11, Lemma 4.9]:
0 1
pair (6, 7) is visited twice. Consider Equiv(2, 3).
Pair (6, 7) is visited a first time by reading 0.
2 3 Symbol 1 leads to (4, 5) which stops the recur-
1 1
sion without inserting (6, 7) in πΈ. At some
0
4
0/1 0
5 subsequent iteration, (6, 7) is visited again via
Equiv(6, 7). By generalization of this automa-
0/1
6
1
7 ton (π΄1 ) automata π΄π of 8π β 1 states can be
1 provided such that π pairs are visited (roughly)
0 0 π2 times each.
4. Deterministic Case
In this Section we present our idea to correct the previously presented algorithm, discussing
its correctness and complexity. The main point is to run the recursive check on a richer data
structure, the associated graph introduced below, whereby the running time of the overall
algorithm is going to be πͺ(π2 |Ξ£|πΌ(π)).
4.1. The Associated Graph
The reason why Algorithm 1 is not quadratic on some automata is the fact that whenever a pair
of distinguishable states is found the recursion stops losing reusable information gathered on
elements of πΈ. A graph associated to the automaton clarifies how pairs of states evolve when
they are found to either be equivalent or distinguishable.
Definition 2. Given a DFA π its associated graph π’ = (π, π΄) is defined as:
π = π Γ π,
π΄ = {β¨π, πβ© β β¨πΏ(π, π₯), πΏ(π, π₯)β© | π, π β π, π₯ β Ξ£} .
β¨π, πβ© is distinguishable if π and π are distinguishable and equivalent otherwise.
Coloring π’ with distinguishable vertices black and equivalent vertices white, the problem of
computing βΌ can be seen as the problem of correctly coloring the associated graph.
The algorithm by Almeida et al. can be described as follows: starts by coloring trivially dis-
tinguishable and equivalent vertices in black and white, respectively, and in grey the remaining
vertices. At each iteration of the main loop, it considers a grey vertex β¨π, πβ© and starts a visit of
π’ from it. If the visit reaches a black vertex β¨πβ² , π β² β©, the recursion stops and all vertices in the
path from β¨π, πβ© to β¨πβ² , π β² β© (saved in π») are colored in black. Otherwise, if all paths lead either
to white or grey vertices all visited vertices are colored white. The main issue with Algorithm 1
is that when a black vertex is encountered all information of vertices in πΈ β π» gets lost.
4.2. The Algorithm for Deterministic Automata
We now present the minimization algorithm based on the observations above.
6
Christian Bianchini et al. CEUR Workshop Proceedings 1β13
Algorithm 2 Proposed algorithm for deterministic automata.
1: function MinimizeDfa(π, Ξ£, πΏ, πΉ ) 19: function Equiv(β¨π, πβ©) β β and β global
2: for all β¨π, πβ© β π Γ π do 20: if β¨π, πβ© β β then
3: if π, π are triv. distinguishable then 21: return β€
4: Color(β¨π, πβ©) β Black 22: else if Color(β¨π, πβ©) = Black then
5: else if π = π then 23: β β β¨π, πβ©
6: Color(β¨π, πβ©) β White 24: return β₯
7: else 25: else if Color(β¨π, πβ©) = White then
8: Color(β¨π, πβ©) β Grey 26: return β€
9: for all β¨π, πβ© β π Γ π do 27: else β here β¨π, πβ© is Grey and fresh
10: if Color(β¨π, πβ©) = Grey then 28: Color(β¨π, πβ©) β White
11: β β EmptyGraph 29:
12: ππ β Equiv(β¨π, πβ©) 30: for all π₯ β Ξ£ do β in lex. order
13: if Β¬ππ then 31: β¨ππ₯ , ππ₯ β© β β¨πΏ(π, π₯), πΏ(π, π₯)β©
14: β β Reverse(β) 32: AddArc(β, β¨π, πβ© , β¨ππ₯ , ππ₯ β©)
15: Visit(β, β) 33: ππ β Equiv(β¨ππ₯ , ππ₯ β©)
16: for all β¨πβ² , π β² β© β WhiteV(β) do 34: if Β¬ππ then return β₯
17: Union(πβ² , π β² ) 35:
36: return β€
18: end function
37: end function
The general structure of MinimizeDfa is the same as MinimizeAlmeida rewritten in terms of
colorings. The only difference is that instead of maintaining two sets πΈ and π» we maintain the
global variable β which represents the visited portion of π’. The idea is that when Equiv(β¨π, πβ©)
returns to the main loop, after line 15, vertices in β will be correctly colored, either in White
or Black. In Algorithm 1 this information was lost while in Algorithm 2 β is used to determine
extra black vertices. Helper procedures Reverse and Visit perform, respectively, arc-reverse of
a graph and the Black-coloring of β starting from the source vertex β.
Let us analyze the version of Equiv(β¨π, πβ©) in Algorithm 2. At lines 20β27 some base cases
are checked. In particular, if β¨π, πβ© is Black, then it is stored in the global variable β and β₯ is
returned. Otherwise, if β¨π, πβ© is White we return β€ to continue the downstream inspection.
Finally, in case β¨π, πβ© is Grey, it is colored White and at lines 30β34 the for loop tries to
continue the recursive visit by reading each symbol in lexicographic order. Before each recursive
call β is updated by adding arc β¨π, πβ© β β¨ππ₯ , ππ₯ β© β we assume vertex β¨ππ₯ , ππ₯ β© is added, if not
already present.
Even though we do not give detailed proofs for space reasons, below we outline the main
arguments for complexity and correctness.
As far as complexity is concerned it is clear that, summing over all the iterations of the main
loop, line 9, the associated graph is visited at most thrice: during the βforwardβ recursion pass
and, optionally, during Reverse and Visit. In fact, every vertex starts Grey and gets White
during the forward pass of an Equiv-call. Possibly, if the call returns β₯, some White vertices
become Black. Altogether, considering the cost of maintaining the union-find data-structure,
we have the following: (notice that |π’| = π2 + π2 |Ξ£|)
Theorem 1. MinimizeDfa algorithm terminates in time πͺ(π2 |Ξ£|πΌ(π)).
To prove correctness we will show the following invariant at line 16: all vertices in β are
correctly colored either Black or White β Lemma 2 below.
7
Christian Bianchini et al. CEUR Workshop Proceedings 1β13
We start by showing some properties of the coloring performed by Equiv and Visit. First of
all, notice that, since we are in the deterministic case, for every π’ = β¨π, πβ© β π and π€ β Ξ£* there
is a unique path in π’ starting from π’ and spelling π€: denote by πΏ(π’, π€) = β¨πΏ(π, π€), πΏ(π, π€)β©
the last vertex of this path.
Definition 3. Given π’ β π and π€ β Ξ£* , we say that π€ for π’ is:
1. simple if π’ β πΏ(π’, π€) in π’ is simple,
2. avalanche2 if it is simple and vertex πΏ(π’, π€) is Black.
If there exists π€ avalanche for π’, denote by av(π’) the lexicographically smallest such π€ and name
π’ β πΏ(π’, av(π’)) the avalanche path of π’.
If Equiv(π’0 ) is called in the main loop, line 12, the visit checks all simple words for π’0 in
lexicographic order, either until all words are explored or β if it exists β until av(π’0 ) is found.
Any vertex that can reach the avalanche path should be colored in Black.
Proposition 1. Consider β upon return of Equiv(π’0 ) at line 12. If there exists π’ β β distin-
guishable, then av(π’0 ) exists. Furthermore, if all White vertices in π’ β β are equivalent, then for
every π’ β β, if π’ is distinguishable we have that π’ β πΏ(π’0 , av(π’0 )) exists in β.
Proof. Suppose π’ β β is distinguishable. First of all, we prove that there exists π€ β Ξ£* such
that πΏ(π’0 , π€) is Black β recall av(π’0 ) is the lexicographically smallest such π€. Since π’ β β,
there exists π€0 such that π’ = πΏ(π’0 , π€0 ). Since π’ is distinguishable, there exists π€1 such that
πΏ(π’, π€1 ) is trivially distinguishable (i.e. Black from the start). Thus, πΏ(π’0 , π€0 π€1 ) is Black.
Let β = πΏ(π’0 , av(π’0 )), π’ β β distinguishable and π be the π’-path leading π’ to some trivially
distinguishable π£. We claim π must cross the avalanche path of π’0 (call it πΌ). Suppose not. Since
β is the only Black vertex in β, π£ β / β. Hence, π must traverse some arc π’β² β π’β²β² with π’β² β β
and π’ ββ²β² / β. By assumption on π and construction of Equiv it follows that π’β² β / πΌ and π’β²β² is
White. Since π leads π’β²β² to π£ it follows that π’β²β² is distinguishable contradicting the hypothesis
on White vertices in π’ β β.
Lemma 2. The following hold at the end of each iteration of loop 9β17:
D1. {β¨π, πβ© | Color(β¨π, πβ©) = Black} β© βΌ = β
,
D2. {β¨π, πβ© | Color(β¨π, πβ©) = White} β βΌ.
Proof. Before entering the the loop both properties hold by initialization.
D1. Assume (D1) and (D2) hold before Equiv(π’0 ). It is sufficient to prove that at the end of
the iteration for every β¨π, πβ© β β we have that β¨π, πβ© is Black if and only if β¨π, πβ© is
distinguishable.
(β) If π’ = β¨π, πβ© β β is Black, then it must have been colored by Visit. Therefore,
ππ = β₯ and before Reverse there was π’ β β in β. Since β was Black before the
Equiv-call, by (D1) it follows β distinguishable. Thus, β¨π, πβ© is distinguishable.
(β) If π’ = β¨π, πβ© β β is distinguishable, then by Prop. 1 it follows that after Reverse
and Visit pair β¨π, πβ© has been colored in Black.
2
The word βcatastrophically" leads to the Black vertex.
8
Christian Bianchini et al. CEUR Workshop Proceedings 1β13
D2. It follows from (D1) and the fact that all vertices in β are either Black or White.
Theorem 2. Algorithm 2 is correct and incremental.
Proof. Both correctness and incrementality follow from Lemma 2 and the fact that β upon
termination β all vertices of π’ are either Black or White. In particular, (D2) of Lemma 2
proves that Union is always correct.
5. Nondeterministic Case
Algorithm 2 is not directly applicable to the nondeterministic case, the reason being that reaching
a pair of non-bisimilar states β i.e. sufficient condition to color in Black a node by Algorithm 2
β is not a sufficient condition now to declare a pair of states distinguishable.
To tackle this issue we first turn the associated graph into a bipartite graph. In the definition
below, for each state π we introduce the shadow state π as a distinct copy of the real π.
Definition 4. Let π© be a complete NFA. The associated graph π’(π© ) is a bipartite directed graph
with vertices π0 βͺ π1 and arcs π΄0 βͺ π΄1 , defined as:
π0 = π Γ π,
π1 = {β¨π, π, π₯β© , β¨π, π, π₯β© | π, π β π, π₯ β Ξ£} ,
π΄0 = β¨π, πβ© β πβ² , π, π₯ , β¨π, πβ© β π, π β² , π₯ | πβ² β πΏ(π, π₯), π β² β πΏ(π, π₯) ,
{οΈ β¨οΈ β©οΈ β¨οΈ β©οΈ }οΈ
π΄1 = πβ² , π, π₯ β πβ² , π β² , π, π β² , π₯ β πβ² , π β² | πβ² β πΏ(π, π₯), π β² β πΏ(π, π₯) .
{οΈβ¨οΈ β©οΈ β¨οΈ β©οΈ β¨οΈ β©οΈ β¨οΈ β©οΈ }οΈ
β¨π, πβ© in βleft" π0 will be called equivalent or distinguishable as in Def. 2.
The bisimilarity between π and π (Def. 1) can be checked in two steps: 0) choose π₯ β Ξ£ and
πβ² β πΏ(π, π₯), and 1) respond with suitable π β² β πΏ(π, π₯). The idea is to mimic step 0) traversing
arcs of π΄0 and step 1) traversing arcs of π΄1 . The triplet β¨πβ² , π, π₯β© β π1 indicates that we have
chosen symbol π₯, state πβ² β πΏ(π, π₯), and we are expecting to respond with some π β² β πΏ(π, π₯) (π
provides the information on the state that must respond). π΄1 arcs do something similar.
Then we need to tune up nondeterminism and Black coloring of vertices in π’. Observe that
π’ β π0 needs only one Black child to be colored in Black, while it needs all children White to
be colored in White. Dually, π’ β π1 behaves the same but with reversed colors. A check will
be performed using the variable Doubts(π’) which, roughly speaking, counts how many Black
neighbours are needed to mark π’ as Black.
5.1. The Algorithm for Nondeterministic Automata
We present Algorithm 3 for the nondeterministic case, whose essential ingredients are those of
Algorithm 2. Details are left to the reader.
First of all, notice that we are actually dealing with four colors: β₯ (never been explored),
Grey (in visit), Black (distinguishable) and White (equivalent).
9
Christian Bianchini et al. CEUR Workshop Proceedings 1β13
Algorithm 3 Proposed algorithm for nondeterministic automata, adapted from DFA case.
1: {β₯, Black, White, Grey} β {β1, 0, 1, 2} 29: function Equiv(π’, π ) β β is global
2: 30: if Color(π’) ΜΈ= β₯ then
3: function MinimizeNfa(π, Ξ£, πΏ, πΉ ) 31: return Color(π’)
4: for all β¨π, πβ© β π Γ π do 32:
5: if π, π are triv. distinguishable then 33: Color(π’) β Grey
6: Color(β¨π, πβ©) β Black 34: Doubts(π’) β 0
7: else if π = π then 35:
8: Color(β¨π, πβ©) β White 36: for π£ β Adj(π’, π’) β§ Color(π’) ΜΈ= π do
9: else 37: πππ β Equiv(π£, 1 β π )
10: Color(β¨π, πβ©) β β₯ 38: if πππ = π then
11: for all β¨π, πβ© β π Γ π do 39: Color(π’) β πππ
12: β β EmptyGraph 40: Doubts(π’) β 0
13: Equiv(β¨π, πβ© , 0) 41: else if πππ = Grey then
14: for all π’ β π0 β© β do 42: AddArc(β, π£, π’)
15: β¨πβ² , π β² β© β π’ 43: Doubts(π’) β Doubts(π’) + 1
16: if Color(π’) ΜΈ= Black then 44:
17: β π’ is either Grey or White 45: if Color(π’) = Grey then
18: Color(π’) β White 46: if Doubts(π’) = 0 then
19: Union(πβ² , π β² ) 47: Color(π’) β 1 β π
20: end function 48: else if π = 0 then
21: 49: Doubts(π’) β 1
22: procedure Relax(π£) β β is global 50:
23: for π’ β Adj(β, π£) do 51: if Color(π’) = Black then
24: Doubts(π’) β Doubts(π’) β 1 52: Relax(π’)
25: if Doubts(π’) = 0 then 53: return Color(π’)
26: Color(π’) β Black
54: end function
27: Relax(π’)
28: end procedure
The procedure MinimizeNfa is structurally the same as MinimizeDfa, the twist being the
usage and maintenance of β. Function Equiv takes two inputs: the current vertex π’ and
the βside" π β {0, 1} of the bipartition. If π’ has already been encountered we return its color.
Otherwise, it is colored in Grey with zero Doubts. At lines 36β43 each successor π£ of π’ is
recursively visited. In case π = 0 (π’ β π0 ) if π£ is recursively found Black, then π’ can be safely
marked Black. Otherwise, there is not enough information to safely assign a Black/White
color to π’. In particular, if π£ is Grey we add arc π£ β π’ to β (notice that it is reversed w.r.t. the
transition) and we increment Doubts(π’) β Blackness of π’ depends on the (possible) future
Blackness of π£. Case π = 1 is dual.
Upon leaving the loop at lines 45β49, if π’ is still Grey we consider two cases: if there are no
doubts (i.e. Doubts(π’) = 0) each of its successors has the same color (either Black or White)
and this can be safely assigned to π’; otherwise, in case π’ β π0 we set Doubts(π’) = 1.
Proceeding at lines 51β53, if π’ is made Black this information is propagated (Relaxed) to its
neighbours in β. Notice that in this case we explicitly define the procedure Relax: in Algorithm
2 the corresponding procedure Visitβs purpose, was to color in Black all vertices reachable
from some distinguishable vertex. In Algorithm 3 we also need to consider the doubts of each
vertex π£ by coloring in Black only non-doubtful vertices.
The complexity is again easy to be determined. Observe that in case the automaton has π
states and π transitions, |π’| β€ 7ππ. Equiv performs the equivalent of a visit of π’ and Relax
visits every arc of β at most once. Hence, their cost over all the execution of Algorithm 3 is
10
Christian Bianchini et al. CEUR Workshop Proceedings 1β13
bounded by the size of π’. Considering the cost of maintaining the union-find data structures
and recalling that π is the degree of nondeterminism, we have the following:
Theorem 3. MinimizeNfa terminates in time πͺ(πππΌ(π)) β πͺ(π2 |Ξ£|ππΌ(π)).
Let us briefly discuss correctness.
Proposition 2. Let π ΜΈ= π and π’ = β¨π, πβ© be White. Then, for every arc π’ β π£ β π΄0 , vertex π£ is
either Grey or White.
Proof. Since π ΜΈ= π, there are only two places at which π’ = β¨π, πβ© changed from Grey to White:
Line 18. In this case, upon termination of Equiv(π’, 0) the pair is Grey and Doubts(π’) = 1
(line 49). In the loop of its Equiv-call every neighbour was recursively found to be either
Grey or White β or π’ would have been colored in Black. Finally, it cannot be the case
that some Grey neighbour π£ became Black afterward: Relax(π£) would have colored π’
in Black by setting Doubts(π’) = 0.
Line 47. In this case, inside the loop of Equiv(π’, 0) none of π’βs neighbours were found to be
either Black or Grey. Thus, they must all be White.
Therefore, every neighbour of π’ is either Grey or White.
Proposition 3. At line 19 (end of the main loop), for every π£ β π1 if π£ is either Grey or White,
then there exists π£ β π’β² β π΄1 such that π’β² is White.
Proof. If π£ is White, then it must have been colored at line 39 after finding a White neighbour.
If π£ is Grey, upon termination of Equiv at line 13 some of its neighbours must have been found
to be Grey. Since every Grey left node is colored in White before the end of the iteration, it
follows again that π£ has some White neighbour.
Lemma 3. The following hold at line 19 (end of the main loop):
N1. βπ = {β¨π, πβ© | Color(β¨π, πβ©) = White} β β¬,
N2. βπ΅ = {β¨π, πβ© | Color(β¨π, πβ©) = Black} β© β¬ = β
.
Proof.
N1. By Lemma 1 it is sufficient to prove that βπ is a bisimulation.
First, notice that pairs violating (B1) are colored in Black from the start. Consider
β¨π, πβ© β βπ . If π = π, (B2) and (B3) trivially hold. Otherwise, let π₯ β Ξ£ and πβ² β πΏ(π, π₯).
From Prop. 2 it follows that π£ = β¨πβ² , π, π₯β© is either Grey or White. From Prop. 3 it
follows that some neighbour π’β² of π£ is in βπ . By Def. 4 we have π’β² = β¨πβ² , π β² β© for some
π β² β πΏ(π, π₯). Thus, (B2) holds for β¨π, πβ©. The very same argument can be used to prove
that (B3) holds for β¨π, πβ©. Hence, βπ is a bisimulation.
N2. The result follows from (N1) and the fact that vertices in π0 β© β are either Black or White.
11
Christian Bianchini et al. CEUR Workshop Proceedings 1β13
Theorem 4. MinimizeNfa is correct and incremental.
Proof. The inclusion βπ β β¬ is (N1). For the converse inclusion notice that it can be easily
checked that, upon termination, every pair β¨π, πβ© β π0 is either Black or White. Therefore,
β¬ = π0 β© β¬ = (βπ΅ βͺ βπ ) β© β¬ = β
βͺ (βπ β© β¬) β βπ .
Incrementality follows again from (N1).
6. Conclusions
Bisimilarity is a fundamental (equivalence) relation among the states of finite automata, finding
applications and variants in a number of different areas. Algorithms for computing bisimilarity
are a classic and can be subdivided in two categories: top-down and a bottom-up. The former
(partition refinement) approach starts with a coarse partition and refines it until the result is
produced, while the latter (partition aggregation) starts from a singleton-classes equivalence
relation and merges classes until possible.
Although algorithms belonging to the bottom-up category are, to the best of our knowledge,
still currently asymptotically slower than their alternative ones, aggregation based techniques
enjoy the property of being incremental: automata resulting at intermediate stages of the
computation are partially minimized yet language-equivalent to the input one.
Moreover, partition aggregation algorithms, even though less celebrated than partition
refinement ones β introduced by Hopcroft and generalized by Paige and Tarjan β, are interesting
(at least) for two reasons. The first is theoretical: if two methods computes the same relation
(just one from βabove" and the other from βbelow"), why is there a complexity gap? Is there some
(hidden) cost involved in maintaining incrementality? The second is practical: some applicative
contexts can greatly benefit from having a partially minimized equivalent automaton, especially
when, as alternative, long sequences of refinement steps are involved.
In this work, while fixing a minor mistake in the algorithm by Almeida et al., we reduced
bisimilarity computation to a coloring problem on an associated graph. We then extended the
algorithm to nondeterministic case, obtaining a complexity improvement on the best known
bound for this case. The time complexity of both algorithms carry the πΌ(π) factor which we
aim to shave off as future work. As a further line of research, it will be interesting to investigate
the effect of applying the technique introduced here to the color refinement algorithm (a.k.a.
Weisfeiler-Leman-1 algorithm, see [15]), currently implemented using an algorithm by Cardon
and Crochemore (see [16]) belonging to the top-down/partition-refinement category.
References
[1] E. F. Moore, Gedanken-Experiments on Sequential Machines, Princeton University Press,
1956, pp. 129β154. doi:10.1515/9781400882618-006.
[2] J. E. Hopcroft, R. Motwani, J. D. Ullman, Pearson Education, 2014.
[3] A. R. Meyer, L. J. Stockmeyer, The equivalence problem for regular expressions with
squaring requires exponential space, in: SWAT, 1972.
12
Christian Bianchini et al. CEUR Workshop Proceedings 1β13
[4] R. Paige, R. E. Tarjan, Three partition refinement algorithms, SIAM J. Comput. 16 (1987)
973β989.
[5] J. E. Hopcroft, An n log n algorithm for minimizing states in a finite automaton, 1971.
[6] J. F. Groote, J. Martens, E. P. de Vink, Lowerbounds for bisimulation by partition refinement
(2022). URL: https://arxiv.org/abs/2203.07158.
[7] B. W. Watson, Taxonomies and toolkits of regular language algorithms, 1995.
[8] B. W. Watson, J. Daciuk, An efficient incremental dfa minimization algorithm, Natural
Language Engineering 9 (2003) 49 β 64.
[9] R. E. Tarjan, Efficiency of a good but not linear set union algorithm, J. ACM 22 (1975)
215β225. doi:10.1145/321879.321884.
[10] J. E. Hopcroft, A linear algorithm for testing equivalence of finite automata, volume 114,
Defense Technical Information Center, 1971.
[11] M. Almeida, N. Moreira, R. Reis, Incremental dfa minimisation, RAIRO - Theoretical
Informatics and Applications 48 (2014) 173β186. doi:10.1051/ita/2013045.
[12] J. BjΓΆrklund, L. G. Cleophas, Minimization of finite state automata through partition
aggregation, in: LATA, 2017.
[13] J. BjΓΆrklund, L. Cleophas, Aggregation-based minimization of finite state automata, 2020.
doi:10.1007/s00236-019-00363-5.
[14] T. H. Cormen, C. E. Leiserson, R. L. Rivest, C. Stein, Introduction to algorithms, 3rd edition,
2009, pp. 170β173.
[15] M. Grohe, K. Kersting, M. Mladenov, P. Schweitzer, Color refinement and its applications,
2021.
[16] A. Cardon, M. Crochemore, Partitioning a graph in o(|a| log2 |v|), Theor. Comput. Sci. 19
(1982) 85β98. doi:10.1016/0304-3975(82)90016-0.
13