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.
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 [
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
languageequivalent 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 [
Above algorithms are focused on the minimization of deterministic automata. The
nondeterministic case was tackled by Björklund and Cleophas [
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 [
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.
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 .
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 nonempty 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
[
pair (, ) ∈ : B1. ∈ B2. ∀ ∈ Σ B3. ∀ ∈ Σ ⇐⇒ ∈ , ∀′ ∈ (, ) ∃′ ∈ (, ) ∧ (′, ′) ∈ , ∀′ ∈ (, ) ∃′ ∈ (, ) ∧ (′, ′) ∈ .
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 eficient algorithms to compute it — justify the use of ℬ as an approximation of ∼ for nondeterministic automata.
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 partitionaggregation 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.
This section is devoted to a brief description of the algorithm proposed by Almeida et al. It
uses the union-find [
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. Algorithm 1 Aggregation-based minimization by Almeida et al.
1: function MinimizeAlmeida(, , ) 2: for all ∈ do 3: Make() 4: ← ( × c) ∪ ( c × ) 5: 6: 7: 8: 9: 10: 11: 12: 13: 14: 15: else 16: ← ∪ 17: 18: ← { ClassOf() : ∈ } 19: return 20: end function for all (, ) ∈ × do ← Find() ← Find() if ̸= ∧ (, ) ̸∈ then ← ∅ ← ∅ if Equiv(, ) then for all (′, ′) ∈ do
Union(′, ′) 21: function Equiv(, ) 22: if (, ) ∈ then 23: return ⊥ 24: if (, ) ∈ then 25: return ⊤ 26: 27: 28: 29: 30: 31: 32: 33: 34: 35: ← ∖ {(, ), (, )} 36: ← ∪ {(, ), (, )} 37: return ⊤ 38: end function ← ∪ {(, ), (, )} for all ∈ Σ do (′, ′) ← (Find( (, )),Find( (, ))) if ′ ̸= ′ ∧ (′, ′) ̸∈ then ← ∪ {(′, ′), (′, ′)} if ¬Equiv(′, ′) then return ⊥
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 [
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). start 0 1 4 1 1 1
1 0/1 0 3 7 0 1 0/1
5
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|Σ | ()).
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 distinguishable 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.
We now present the minimization algorithm based on the observations above. Algorithm 2 Proposed algorithm for deterministic automata.
The general structure of MinimizeDfa is the same as MinimizeAlmeida rewritten in terms of colorings. The only diference 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.
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.
⇝ (, 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 ∈ ℋ distinguishable, 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, 01) 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 ∖ ℋ.
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 suficient 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. 2The word “catastrophically" leads to the Black vertex. D2. It follows from (D1) and the fact that all vertices in ℋ are either Black or White.
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.
Algorithm 2 is not directly applicable to the nondeterministic case, the reason being that reaching a pair of non-bisimilar states — i.e. suficient condition to color in Black a node by Algorithm 2 — is not a suficient 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.
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). Algorithm 3 Proposed algorithm for nondeterministic automata, adapted from DFA case.
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 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.
N1. ℛ = {⟨, ⟩ | Color(⟨, ⟩) = White} ⊆ ℬ , N2. ℛ = {⟨, ⟩ | Color(⟨, ⟩) = Black} ∩ ℬ = ∅.
N1. By Lemma 1 it is suficient 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.
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).
Bisimilarity is a fundamental (equivalence) relation among the states of finite automata, finding applications and variants in a number of diferent 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 of as future work. As a further line of research, it will be interesting to investigate
the efect of applying the technique introduced here to the color refinement algorithm (a.k.a.
Weisfeiler-Leman-1 algorithm, see [