Filippo Bonchi
email: filippo.bonchi@ens-lyon.fr

Damien Pous
email: damien.pous@ens-lyon.fr

Checking NFA equivalence with bisimulations up to congruence

Keywords: Language Equivalence, Automata, Bisimulation, Coinduction, Up-to techniques, Congruence, Antichains

. We compare our approach to the recently introduced antichain algorithms, by analysing and relating the two underlying coinductive proof methods. We give concrete examples where we exponentially improve over antichains; experimental results moreover show non negligible improvements.

Introduction

Checking language equivalence of finite automata is a classical problem in computer science, which finds applications in many fields ranging from compiler construction to model checking.

Equivalence of deterministic finite automata (DFA) can be checked either via minimisation [START_REF] Brzozowski | Canonical regular expressions and minimal state graphs for definite events[END_REF][START_REF] Hopcroft | An n log n algorithm for minimizing in a finite automaton[END_REF] or through Hopcroft and Karp's algorithm [START_REF] Aho | The Design and Analysis of Computer Algorithms[END_REF][START_REF] Hopcroft | A linear algorithm for testing equivalence of finite automata[END_REF], which exploits an instance of what is nowadays called a coinduction proof principle [START_REF] Milner | Communication and Concurrency[END_REF][START_REF] Rutten | Automata and coinduction (an exercise in coalgebra)[END_REF][START_REF] Sangiorgi | Introduction to Bisimulation and Coinduction[END_REF]: two states recognise the same language if and only if there exists a bisimulation relating them. In order to check the equivalence of two given states, Hopcroft and Karp's algorithm creates a relation containing them and tries to build a bisimulation by adding pairs of states to this relation: if it succeeds then the two states are equivalent, otherwise they are different.

On the one hand, minimisation algorithms have the advantage of checking the equivalence of all the states at once (while Hopcroft and Karp's algorithm only check a given pair of states). On the other hand, they have the disadvantage of needing the whole automata from the beginning 1 1 , while Hopcroft and Karp's algorithm can be executed "on-the-fly" [START_REF] Fernandez | On-the-fly verification of finite transition systems[END_REF], on a lazy DFA whose transitions are computed on demand.

This difference is fundamental for our work and for other recently introduced algorithms based on antichains [START_REF] Abdulla | When simulation meets antichains[END_REF][START_REF] Wulf | Antichains: A new algorithm for checking universality of finite automata[END_REF]. Indeed, when starting from non-deterministic finite automata (NFA), the powerset construction used to get deterministic automata induces an exponential factor. In contrast, the algorithm we introduce in this work for checking equivalence of NFA (as well as those in [START_REF] Abdulla | When simulation meets antichains[END_REF][START_REF] Wulf | Antichains: A new algorithm for checking universality of finite automata[END_REF]) usually does not build the whole deterministic automaton, but just a small part of it. We write "usually" because in few bad cases, the algorithm still needs exponentially many states of the DFA.

Our algorithm is grounded on a simple observation on determinised NFA: for all sets X and Y of states of the original NFA, the union (written +) of the language recognised by X (written [[X]]) and the language recognised by Y ([[Y ]]) is equal to the language recognised by the union of X and Y ([[X + Y ]]). In symbols:

[[X + Y ]] = [[X]] + [[Y ]] (1)
This fact leads us to introduce a sound and complete proof technique for language equivalence, namely bisimulation up to context, that exploits both induction (on the operator +) and coinduction: if a bisimulation R equates both the (sets of) states X1, Y1 and X2, Y2, then

[[X1]] = [[Y1]] and [[X2]] = [[Y2]
] and, by [START_REF] Abdulla | When simulation meets antichains[END_REF], we can immediately conclude that also X1 + X2 and Y1 + Y2 are language equivalent. Intuitively, bisimulations up to context are bisimulations which do not need to relate X1 + X2 and Y1 + Y2 when X1 (resp. X2) and Y1 (resp. Y2) are already related.

To illustrate this idea, let us check the equivalence of states x and u in the following NFA. (Final states are overlined, labelled edges represent transitions.)

x a z a o o a ' ' y a f f u a ' ' a w a f f v a o o
The determinised automaton is depicted below. Actually, this is the relation that is built by Hopcroft and Karp's algorithm (the numbers express the order in which pairs are added).

{x} a /
The dashed lines (numbered by 1, 2, 3) form a smaller relation which is not a bisimulation, but a bisimulation up to context: the equivalence of states {x, y} and {u, v, w} could be immediately deduced from the fact that {x} is related to {u} and {y} to {v, w}, without the need of further exploring the determinised automaton.

Bisimulations up-to, and in particular bisimulations up to context, have been introduced in the setting of concurrency theory [START_REF] Milner | Communication and Concurrency[END_REF][START_REF] Milner | A calculus of mobile processes, I/II[END_REF][START_REF] Sangiorgi | On the bisimulation proof method[END_REF] as a proof technique for bisimilarity of CCS or π-calculus processes. As far as we know, they have never been used for proving language equivalence of NFA.

Among these techniques one should also mention bisimulation up to equivalence, which, as we show in this paper, is implicitly used in the original Hopcroft and Karp's algorithm. This technique can be briefly explained by noting that not all bisimulations are equivalence relations: it might be the case that a bisimulation relates (for instance) X and Y , Y and Z but not X and Z. However, since

[[X]] = [[Y ]] and [[Y ]] = [[Z]],
we can immediately conclude that X and Z recognise the same language. Analogously to bisimulations up to context, a bisimulation up to equivalence does not need to relate X and Z when they are both related to some Y .

The techniques of up-to equivalence and up-to context can be combined resulting in a powerful proof technique which we call bisimulation up to congruence. Our algorithm is in fact just an extension of Hopcroft and Karp's algorithm that attempts to build a bisimulation up to congruence instead of a bisimulation up to equivalence. An important consequence, when using up to congruence, is that we do not need to build the whole deterministic automata, but just those states that are needed for the bisimulation up-to. For instance, in the above NFA, the algorithm stops after equating z and u + v and does not build the remaining four states. Despite their use of the up to equivalence technique, this is not the case with Hopcroft and Karp's algorithm, where all accessible subsets of the deterministic automata have to be visited at least once.

The ability of visiting only a small portion of the determinised automaton is also the key feature of the antichain algorithm [START_REF] Wulf | Antichains: A new algorithm for checking universality of finite automata[END_REF] and its optimisation exploiting similarity [START_REF] Abdulla | When simulation meets antichains[END_REF]. The two algorithms are designed to check language inclusion rather than equivalence, but we can relate these approaches by observing that the two problems are equivalent ([

[X]] = [[Y ]] iff [[X]] ⊆ [[Y ]] and [[Y ]] ⊆ [[X]]; and [[X]] ⊆ [[Y ]] iff [[X]] + [[Y ]] = [[Y ]] iff [[X + Y ]] = [[Y ]]).
In order to compare with these algorithms, we make explicit the coinductive up-to technique underlying the antichain algorithm [START_REF] Wulf | Antichains: A new algorithm for checking universality of finite automata[END_REF]. We prove that this technique can be seen as a restriction of up to congruence, for which symmetry and transitivity are not allowed. As a consequence, the antichain algorithm usually needs to explore more states than our algorithm. Moreover, we show how to integrate the optimisation proposed in [START_REF] Abdulla | When simulation meets antichains[END_REF] in our setting, resulting in an even more efficient algorithm.

Summarising, the contributions of this work are (1) the observation that Hopcroft and Karp implicitly use bisimulations up to equivalence (Section 2),

(2) an efficient algorithm for checking language equivalence (and inclusion), based on a powerful up to technique (Section 3),

(3) a comparison with antichain algorithms, by recasting them into our coinductive framework (Sections 4 and 5).

Outline

Section 2 recalls Hopcroft and Karp's algorithm for DFA, showing that it implicitly exploits bisimulation up to equivalence. Section 3 describes the novel algorithm, based on bisimulations up to congruence. We compare this algorithm with the antichain one in Section 4, and we show how to exploit similarity in Section 5. Section 6 is devoted to benchmarks. Sections 7 and 8 discuss related and future works. Omitted proofs can be found in the Appendix.

Notation

We denote sets by capital letters X, Y, S, T . . . and functions by lower case letters f, g, . . . Given sets X and Y , X × Y is their Cartesian product, X Y is the disjoint union and X Y is the set of functions f : Y → X. Finite iterations of a function f : X → X are denoted by f n (formally,

f 0 (x) = x, f n+1 (x) = f (f n (x))).
The collection of subsets of X is denoted by P(X). The (omega) iteration of a function f : P(X) → P(X) is denoted by

f ω (formally, f ω (Y ) = n≥0 f n (Y )).
For a set of letters A, A denotes the set of all finite words over A; the empty word; and w1w2 the concatenation of words w1, w2 ∈ A . We use 2 for the set {0, 1} and 2 A for the set of all languages over A.

Hopcroft and Karp's algorithm for DFA

A deterministic finite automaton (DFA) over the alphabet A is a triple (S, o, t), where S is a finite set of states, o : S → 2 is the output function, which determines if a state x ∈ S is final (o(x) = 1) or not (o(x) = 0), and t : S → S A is the transition function which returns, for each state x and for each letter a ∈ A, the next state ta(x). For a ∈ A, we write x a → x to mean that ta(x) = x . For w ∈ A , we write x w → x for the least relation such that [START_REF] Abdulla | When simulation meets antichains[END_REF] x → x and (2)

x aw → x iff x a → x and x w → x .
For any DFA, there exists a function [[-]] : S → 2 A mapping states to languages, defined for all x ∈ S as follows:

[[x]]( ) = o(x) , [[x]](aw) = [[ta(x)]](w) .
The language [[x]] is called the language accepted by x. Given two automata (S1, o1, t1) and (S2, o2, t2), the states x1 ∈ S1 and x2 ∈ S2 are said to be language equivalent (written x1 ∼ x2) iff they accept they same language.

Remark 1. In the following, we will always consider the problem of checking the equivalence of states of one single and fixed automaton (S, o, t). We do not loose generality since for any two automata (S1, o1, t1) and (S2, o2, t2) it is always possible to build an automaton (S1 S2, o1 o2, t1 t2) such that the language accepted by every state x ∈ S1 S2 is the same as the language accepted by x in the original automaton (Si, oi, ti). For this reason, we also work with automata without explicit initial states: we focus on the equivalence of two arbitrary states of a fixed DFA.

Proving language equivalence via coinduction

We first define bisimulation. We make explicit the underlying notion of progression which we need in the sequel.

Definition 1 (Progression, Bisimulation). Given two relations R, R ⊆ S × S on states, R progresses to R , denoted R R , if whenever x R y then 1. o(x) = o(y) and 2. for all a ∈ A, ta(x) R ta(y). A bisimulation is a relation R such that R R.
As expected, bisimulation is a sound and complete proof technique for checking language equivalence of DFA: Proposition 1 (Coinduction). Two states are language equivalent iff there exists a bisimulation that relates them.

Naive algorithm

Figure 1 shows a naive version of Hopcroft and Karp's algorithm for checking language equivalence of the states x and y of a deterministic finite automaton (S, o, t). Starting from x and y, the algorithm builds a relation R that, in case of success, is a bisimulation. In order to do that, it employs the set (of pairs of states) todo which, intuitively, at any step of the execution, contains the pairs (x , y ) that must be checked: if (x , y ) already belongs to R, then it has already been checked and nothing else should be done. Otherwise, the algorithm checks if x and y have the same outputs (i.e., if both are final or not). If o(x ) = o(y ), then x and y are different.

Naive(x, y)

( 1 ) R i s e m p t y ; todo i s e m p t y ;

( 2 ) i n s e r t (x, y) i n todo; If o(x ) = o(y ), then the algorithm inserts (x , y ) in R and, for all a ∈ A, the pairs (ta(x ), ta(y )) in todo.

Proposition 2. For all x, y ∈ S, x ∼ y iff Naive(x, y).

Proof. We first observe that if Naive(x, y) returns true then the relation R that is built before arriving to step 4 is a bisimulation. Indeed, the following proposition is an invariant for the loop corresponding to step 3:

R R ∪ todo

This invariant is preserved since at any iteration of the algorithm, a pair (x , y ) is removed from todo and inserted in R after checking that o(x ) = o(y ) and adding (ta(x ), ta(y )) for all a ∈ A in todo. Since todo is empty at the end of the loop, we eventually have R R, i.e., R is a bisimulation. By Proposition 1, x ∼ y. We now prove that if Naive(x, y) returns false, then x ∼ y. Note that for all (x , y ) inserted in todo, there exists a word w ∈ A such that x w → x and y

w → y . Since o(x ) = o(y ), then [[x ]]( ) = [[y ]]( ) and thus [[x]](w) = [[x ]]( ) = [[y ]]( ) = [[y]](w), that is x ∼ y.
Since both Hopcroft and Karp's algorithm and the one we introduce in Section 3 are simple variations of this naive one, it is important to illustrate its execution with an example. Consider the DFA with input alphabet A = {a} in the left-hand side of Figure 2, and suppose we want to check that x and u are language equivalent.

During the initialisation, (x, u) is inserted in todo. At the first iteration, since o(x) = 0 = o(u), (x, u) is inserted in R and (y, v) in todo. At the second iteration, since o(y) = 1 = o(v), (y, v) is inserted in R and (z, w) in todo. At the third iteration, since o(z) = 0 = o(w), (z, w) is inserted in R and (y, v) in todo. At the fourth iteration, since (y, v) is already in R, the algorithm does nothing. Since there are no more pairs to check in todo, the relation R is a bisimulation and the algorithm terminates returning true. These iterations are concisely described by the numbered dashed lines in Figure 2. The line i means that the connected pair is inserted in R at iteration i. (In the sequel, when enumerating iterations, we ignore those where a pair from todo is already in R so that there is nothing to do.) Remark 2. Unless it finds a counter-example, Naive constructs the smallest bisimulation that relates the two starting states (see Proposition 8 in Appendix A). On the contrary, minimisation algorithms [START_REF] Brzozowski | Canonical regular expressions and minimal state graphs for definite events[END_REF][START_REF] Hopcroft | An n log n algorithm for minimizing in a finite automaton[END_REF] are designed to compute the largest bisimulation relation for a given automaton. For instance, taking automaton on the left of Figure 2, they would equate the states x and w which are language equivalent, while Naive(x, u) does not relate them.

Hopcroft and Karp's algorithm

The naive algorithm is quadratic: a new pair is added to R at each non-trivial iteration, and there are only n 2 such pairs, where n = |S| is the number of states of the DFA. To make this algorithm (almost) linear, Hopcroft and Karp actually record a set of equivalence classes rather than a set of visited pairs. As a consequence, their algorithm may stop earlier, when an encountered pair of states is not already in R but in its reflexive, symmetric, and transitive closure. For instance in the right-hand side example from Figure 2, we can stop when we encounter the dotted pair (y, w), since these two states already belong to the same equivalence class according to the four previous pairs. With this optimisation, the produced relation R contains at most n pairs (two equivalence classes are merged each time a pair is added). Formally, and ignoring the concrete data structure to store equivalence classes, Hopcroft and Karp's algorithm consists in simply replacing step 3.2 in Figure 1 with

( 3 . 2 ) i f (x , y ) ∈ e(R) t h e n s k i p ;
where e : P(S × S) → P(S × S) is the function mapping each relation R ⊆ S × S into its symmetric, reflexive, and transitive closure. We hereafter refer to this algorithm as HK.

Bisimulations up-to

We now show that the optimisation used by Hopcroft and Karp corresponds to exploiting an "up-to technique". Definition 2 (Bisimulation up-to). Let f : P(S × S) → P(S × S) be a function on relations on S. A relation R is a bisimulation up to f if R f (R), i.e., whenever x R y then 1. o(x) = o(y) and 2. for all a ∈ A, ta(x) f (R) ta(y).

With this definition, Hopcroft and Karp's algorithm just consists in trying to build a bisimulation up to e. To prove the correctness of the algorithm it suffices to show that any bisimulation up to e is contained in a bisimulation. We use for that the notion of compatible function [START_REF] Pous | Complete lattices and up-to techniques[END_REF][START_REF] Sangiorgi | On the bisimulation proof method[END_REF]:

Definition 3 (Compatible function). A function f : P(S × S) → P(S × S) is compatible if it is monotone and it preserves progres- sions: for all R, R ⊆ S × S, R R entails f (R) f (R ) .
Proposition 3. Let f be a compatible function. Any bisimulation up to f is contained in a bisimulation.

Proof. Suppose that R is a bisimulation up to f , i.e., that R f (R). Using compatibility of f and by a simple induction on n, we get ∀n, f n (R) f n+1 (R). Therefore, we have

n f n (R) n f n (R) , 3 2012/7/11
in other words, f ω (R) = n f n (R) is a bisimulation. This latter relation trivially contains R, by taking n = 0.

We could prove directly that e is a compatible function; we however take a detour to ease our correctness proof for the algorithm we propose in Section 3.

Lemma 1. The following functions are compatible: id: the identity function; f • g: the composition of compatible functions f and g; F : the pointwise union of an arbitrary family F of compatible functions: F (R) = f ∈F f (R); f ω : the (omega) iteration of a compatible function f . Lemma 2. The following functions are compatible:

• the constant reflexive function:

r(R) = {(x, x) | ∀x ∈ S}; • the converse function: s(R) = {(y, x) | x R y}; • the squaring function: t(R) = {(x, z) | ∃y, x R y R z}.
Intuitively, given a relation R, (s ∪ id)(R) is the symmetric closure of R, (r ∪ s ∪ id)(R) is its reflexive and symmetric closure, and (r ∪ s ∪ t ∪ id) ω (R) is its symmetric, reflexive and transitive closure: e = (r ∪ s ∪ t ∪ id) ω . Another way to understand this decomposition of e is to recall that for a given R, e(R) can be defined inductively by the following rules:

x e(R) x Proof. By Proposition 3, it suffices to show that e is compatible, which follows from Lemma 1 and Lemma 2.

Corollary 1. For all x, y ∈ S, x ∼ y iff HK(x, y).

Proof. Same proof as for Proposition 2, by using the invariant R e(R) ∪ todo. We deduce that R is a bisimulation up to e after the loop. We conclude with Theorem 1 and Proposition 1.

Returning to the right-hand side example from Figure 2, Hopcroft and Karp's algorithm constructs the relation

RHK = {(x, u), (y, v), (z, w), (z, v)}
which is not a bisimulation, but a bisimulation up to e: it contains the pair (x, u), whose b-transitions lead to (y, w), which is not in RHK but in its equivalence closure, e(RHK).

Optimised algorithm for NFA

We now move from DFA to non-deterministic automata (NFA). We start with standard definitions about semi-lattices, determinisation, and language equivalence for NFA.

A semi-lattice (X, +, 0) consists of a set X and a binary operation + : X × X → X which is associative, commutative, idempotent (ACI), and has 0 ∈ X as identity. Given two semilattices (X1, +1, 01) and (X2, +2, 02), an homomorphism of semilattices is a function f : X1 → X2 such that for all x, y ∈ X1, f (x +1 y) = f (x) +2 f (y) and f (01) = 02. The set 2 = {0, 1} is a semi-lattice when taking + to be the ordinary Boolean or. Also the set of all languages 2 A carries a semi-lattice where + is the union of languages and 0 is the empty language. More generally, for any set X, P(X) is a semi-lattice where + is the union of sets and 0 is the empty set. In the sequel, we indiscriminately use 0 to denote the element 0 ∈ 2, the empty language in 2 A , and the empty set in P(X). Similarly, we use + to denote the Boolean or in 2, the union of languages in 2 A , and the union of sets in P(X).

A non-deterministic finite automaton (NFA) over the input alphabet A is a triple (S, o, t), where S is a finite set of states, o : S → 2 is the output function (as for DFA), and t : S → P(S) A is the transition relation, which assigns to each state x ∈ S and input letter a ∈ A a set of possible successor states.

The powerset construction transforms any NFA (S, o, t) in the DFA (P(S), o , t ) where o : P(S) → 2 and t : P(S) → P(S) A are defined for all X ∈ P(S) and a ∈ A as follows:

o (X) =      o(x) if X = {x} with x ∈ S 0 if X = 0 o (X1) + o (X2) if X = X1 + X2 t a (X) =      ta(x) if X = {x} with x ∈ S 0 if X = 0 t a (X1) + t a (X2) if X = X1 + X2
Observe that in (P(S), o , t ), the states form a semi-lattice (P(S), +, 0), and o and t are, by definition, semi-lattices homomorphisms. These properties are fundamental for the up-to technique we are going to introduce; in order to highlight the difference with generic DFA (which usually do not carry this structure), we introduce the following definition. Definition 4. A determinised NFA is a DFA (P(S), o , t ) obtained via the powerset construction of some NFA (S, o, t).

Hereafter, we use a new notation for representing states of determinised NFA: in place of the singleton {x} we just write x and, in place of {x1, . . . , xn}, we write x1

+ • • • + xn.
For an example, consider the NFA (S, o, t) depicted below (left) and part of the determinised NFA (P(S), o , t ) (right).

x a B B a ' ' y a g g z a o o x a / / y + z a / / x + y a / / x + y + z a F F
In the determinised NFA, x makes one single a-transition going into y + z. This state is final:

o (y + z) = o (y) + o (z) = o(y) + o(z) = 1 + 0 = 1; it makes an a-transition into t a (y + z) = t a (y) + t a (z) = ta(y) + ta(z) = x + y.
The language accepted by the states of a NFA (S, o, t) can be conveniently defined via the powerset construction: the language accepted by x ∈ S is the language accepted by the singleton {x} in the DFA (P(S), o , t ), in symbols [[{x}]]. Therefore, in the following, instead of considering the problem of language equivalence of states of the NFA, we focus on language equivalence of sets of states of the NFA: given two sets of states X and Y in P(S), we say that X and Y are language equivalent (X

∼ Y ) iff [[X]] = [[Y ]].
This is exactly what happens in standard automata theory, where NFA are equipped with sets of initial states.

Extending coinduction to NFA

In order to check if two sets of states X and Y of an NFA (S, o, t) are language equivalent, we can simply employ the bisimulation proof method on (P(S), o , t ). More explicitly, a bisimulation for a NFA (S, o, t) is a relation R ⊆ P(S) × P(S) on sets of states, such that whenever X R Y then (1) o (X) = o (Y ), and (2) for all a ∈ A, t a (X) R t a (Y ). Since this is just the old definition of bisimulation (Definition 1) applied to (P(S), o , t ), we get that X ∼ Y iff there exists a bisimulation relating them.

Remark 3 (Linear time v.s. branching time). It is important not to confuse these bisimulation relations with the standard Milnerand-Park bisimulations [START_REF] Milner | Communication and Concurrency[END_REF] (which strictly imply language equivalence): in a standard bisimulation R, if the following states x and y of an NFA are in R,

x1

. . .

x a 5 5 a ) ) xn y1 . . . y a 5 5 a ) ) ym
then each xi should be in R with some yj (and vice-versa). Here, instead, we first transform the transition relation into

x a / / x1 + • • • + xn y a / / y1 + • • • + ym ,
using the powerset construction, and then we require that the sets

x1 + • • • + xn and y1 + • • • + ym are related by R.

Bisimulation up to congruence

The semi-lattice structure (P(S), +, 0) carried by determinised NFA makes it possible to introduce a new up-to technique, which is not available with plain DFA: up to congruence. This technique relies on the following function.

Definition 5 (Congruence closure). Let u : P(P(S) × P(S)) → P(P(S) × P(S)) be the function on relations on sets of states defined for all R ⊆ P(S) × P(S) as:

u(R) = {(X1 + X2, Y1 + Y2) | X1 R Y1 and X2 R Y2} . The function c = (r ∪ s ∪ t ∪ u ∪ id) ω is called the congruence closure function.
Intuitively, c(R) is the smallest equivalence relation which is closed with respect to + and which includes R. It could alternatively be defined inductively using the rules r, s, t, and id from the previous section, and the following one:

X1 c(R) Y1 X2 c(R) Y2 X1 + X2 c(R) Y1 + Y2 u
We call bisimulations up to congruence the bisimulations up to c. We report the explicit definition for the sake of clarity: Definition 6 (Bisimulation up to congruence). A bisimulation up to congruence for a NFA (S, o, t) is a relation R ⊆ P(S) × P(S) on sets of states, such that whenever X R Y then

1. o (X) = o (Y ) and 2. for all a ∈ A, t a (X) c(R) t a (Y ).
We then show that bisimulations up to congruence are sound, using the notion of compatibility:

Lemma 3. The function u is compatible.
Proof. We assume that R R , and we prove that u(R) u(R ). If X u(R) Y , then X = X1 + X2 and Y = Y1 + Y2 for some X1, X2, Y1, Y2 such that X1 R Y1 and X2 R Y2. By assumption, we have o (X1) = o (Y1), o (X2) = o (Y2), and for all a ∈ A, t a (X1) R t a (Y1) and t a (X2) R t a (Y2). Since o and t are homomorphisms, we deduce o (X1 + X2) = o (Y1 + Y2), and for all a ∈ A, t a (X1 + X2) u(R ) t a (Y1 + Y2).

Theorem 2. Any bisimulation up to congruence is contained in a bisimulation.

Proof. By Proposition 3, it suffices to show that c is compatible, which follows from Lemmas 1, 2 and 3. In the Introduction, we already gave an example of bisimulation up to context, which is a particular case of bisimulation up to congruence (up to context corresponds to use just the function (r ∪ u ∪ id) ω , without closing under s and t).

x a E E a & & y a g g z a o o u a D D x a / / 1 y + z a / / 2 x + y a / / 3 x + y + z a F F 4 u a D D
A more involved example illustrating the use of all ingredients of the congruence closure function (c) is given in Figure 3. The relation R expressed by the dashed numbered lines (formally R = {(x, u), (y + z, u)}) is neither a bisimulation, nor a bisimulation up to equivalence, since y + z a → x + y and u a → u, but (x+y, u) / ∈ e(R). However, R is a bisimulation up to congruence. Indeed, we have (x + y, u) ∈ c(R):

x + y c(R) u + y ((x, u) ∈ R) c(R) y + z + y ((y + z, u) ∈ R) = y + z c(R) u ((y + z, u) ∈ R)
In contrast, we need four pairs to get a bisimulation up to e containing (x, u): this is the relation depicted with both dashed and dotted lines in Figure 3. Note that we can deduce many other equations from R; in fact, c(R) defines the following partition of sets of states: {0}, {y}, {z}, {x, u, x+y, x+z, and the 9 remaining subsets}.

Optimised algorithm for NFA

Algorithms for NFA can be obtained by computing the determinised NFA on-the-fly [START_REF] Fernandez | On-the-fly verification of finite transition systems[END_REF]: starting from the algorithms for DFA (Figure 1), it suffices to work with sets of states, and to inline the powerset construction. The corresponding code is given in Figure 4. The naive algorithm (Naive) does not use any up to technique, Hopcroft and Karp's algorithm (HK) reasons up to equivalence in step 3.2, and the optimised algorithm, referred as HKC in the sequel, relies on up to congruence: step 3.2 becomes

( 3 . 2 ) i f (X , Y ) ∈ c(R ∪ todo) t h e n s k i p ;
Observe that we use c(R ∪ todo) rather than c(R): this allows us to skip more pairs, and this is safe since all pairs in todo will eventually be processed.

Corollary 2. For all X, Y ∈ P(S), X ∼ Y iff HKC(X, Y ).
Proof. Same proof as for Proposition 2, by using the invariant R c(R ∪ todo) for the loop. We deduce that R is a bisimulation up to congruence after the loop. We conclude with Theorem 2 and Proposition 1.

The most important point about these three algorithms is that they compute the states of the determinised NFA lazily. This means that only accessible states need to be computed, which is of practical importance since the determinised NFA can be exponentially large. In case of a negative answer, the three algorithms stop even before all accessible states have been explored; otherwise, if a bisimulation (possibly up-to) is found, it depends on the algorithm: • with Naive, all accessible states need to be visited, by definition of bisimulation; • with HK, the only case where some accessible states can be avoided is when a pair (X, X) is encountered: the algorithm skips this pair so that the successors of X are not necessarily computed (this situation rarely happens in practice-it actually never happens when starting with disjoint automata). In the other cases where a pair (X, Y ) is skipped, then X and Y are necessarily already related to some other states in R, so that their successors will eventually be explored; • with HKC, only a small portion of the accessible states is built (check the experiments in Section 6). To see a concrete example, let us execute HKC on the NFA from Figure 3. After two iterations, R = {(x, u), (y + z, u)}. Since x + y c(R) u, the algorithm stops without building the states x + y and x + y + z. Similarly, in the example from the Introduction, HKC does not construct the four states corresponding to pairs 4, 5, and 6.

Naive(X, Y ) ( 1 ) R i
This ability of HKC to ignore parts of the determinised NFA comes from the up to congruence technique, which allows one to infer properties about states that were not necessarily encountered before. As we shall see in Section 4 the efficiency of antichains algorithms [START_REF] Abdulla | When simulation meets antichains[END_REF][START_REF] Wulf | Antichains: A new algorithm for checking universality of finite automata[END_REF] also comes from their ability to skip large parts of the determinised NFA.

Computing the congruence closure

For the optimised algorithm to be effective, we need a way to check whether some pairs belong to the congruence closure of some relation (step 3.2). We present here a simple solution based on set rewriting; the key idea is to look at each pair (X, Y ) in a relation R as a pair of rewriting rules:

X → X + Y Y → X + Y ,
which can be used to compute normal forms for sets of states. Indeed, by idempotence, X R Y entails X c(R) X + Y .

Definition 7. Let R ⊆ P(S)×P(S) be a relation on sets of states.

We define R ⊆ P(S) × P(S) as the smallest irreflexive relation that satisfies the following rules:

X R Y X R X + Y X R Y Y R X + Y Z R Z U + Z R U + Z Lemma 4. For all relations R, the relation R is convergent.
In the sequel, we denote by X↓R the normal form of a set X w.r.t. R. Intuitively, the normal form of a set is the largest set of its equivalence class. Recalling the example from Figure 3, the common normal form of x + y and u can be computed as follows (R is the relation {(x, u), (y + z, u)}):

x + y * * u w w x + y + u + + x + u s s x + y + z + u
Theorem 3. For all relations R, and for all X, Y ∈ P(S), we have

X↓R = Y ↓R iff (X, Y ) ∈ c(R).
Thus, in order to check if (X, Y ) ∈ c(R ∪ todo) we only have to compute the normal form of X and Y with respect to R∪todo . Note that each pair of R∪todo may be used only once as a rewriting rule, but we do not know in advance in which order to apply these rules. Therefore, the time required to find one rule that applies is in the worst case rn where r = |R ∪ todo| is the size of the relation R∪todo, and n = |S| is the number of states of the NFA (assuming linear time complexity for set-theoretic union and containment of sets of states). Since we cannot apply more than r rules, the time for checking whether (X, Y ) ∈ c(R ∪ todo) is bounded by r 2 n.

We tried other solutions, notably by using binary decision diagrams [START_REF] Bryant | Graph-based algorithms for boolean function manipulation[END_REF]. We have chosen to keep the presented rewriting algorithm for its simplicity and because it behaves well in practice.

Complexity hints

The complexity of Naive, HK and HKC is closely related to the size of the relation that they build. Hereafter, we use v = |A| to denote the number of letters in A. Therefore, we can conveniently reason about |R|. Lemma 6. Let RNaive, RHK, and RHKC denote the relations produced by the three algorithms. We have

|RHKC|, |RHK| ≤ m |RNaive| ≤ m 2 , ( 2
)
where m ≤ 2 n is the number of accessible states in the determinised NFA and n is the number of states of the NFA. If the algorithms returned true, we moreover have

|RHKC| ≤ |RHK| ≤ |RNaive| . (3)
As shown below in Section 4.2.4, RHKC can be exponentially smaller than RHK. Notice however that the problem of deciding NFA language equivalence is PSPACE-complete [START_REF] Meyer | Word problems requiring exponential time[END_REF], and that none of the algorithms presented here is in PSPACE: all of them store a set of visited pairs, and in the worst case, this set can become exponentially large with all of them. (This also holds for the antichain algorithms [START_REF] Abdulla | When simulation meets antichains[END_REF][START_REF] Wulf | Antichains: A new algorithm for checking universality of finite automata[END_REF] which we describe in Section 4.) Instead, the standard PSPACE algorithm does not store any set of visited pairs: it checks all words of length smaller than 2 n . While this can be done in polynomial space, this systematically requires exponential time.

Using HKC for checking language inclusion

For NFA, language inclusion can be reduced to language equivalence in a rather simple way. Since the function [[-]] : P(S) → 2 A is a semi-lattice homomorphism (see Theorem 7 in Appendix A), for any given sets of states X and Y ,

[[X+Y ]] = [[Y ]] iff [[X]] + [[Y ]] = [[Y ]] iff [[X]] ⊆ [[Y ]]. Therefore, it suffices to run HKC(X+Y, Y ) to check the inclusion [[X]] ⊆ [[Y ]].
In such a situation, all pairs that are eventually manipulated by HKC have the shape (X +Y , Y ) for some sets X , Y . The step 3.2 of HKC, where it checks whether the current pair belongs to the congruence closure of the relation, can thus be simplified. First, the pairs in the current relation can only be used to rewrite from right to left. Second, the following lemma allows one to avoid unnecessary normal form computations: Lemma 7. For all sets X, Y and for all relations R, we have

X+Y c(R) Y iff X ⊆ Y ↓R.
Proof. We first prove that for all X, Y, X↓R = Y ↓R iff X ⊆ Y ↓R and Y ⊆ X↓R, using the fact that the normalisation function ↓R : X → X↓R is monotone and idempotent. The announced result follows by Theorem 3, since Y ⊆ (X + Y )↓R is always true and X+Y ⊆ Y ↓R iff X ⊆ Y ↓R.

However, as shown below, checking an equivalence by decomposing it into two inclusions cannot be more efficient than checking the equivalence directly.

Lemma 8. Let X, Y be two sets of states; let R ⊆ and R ⊇ be the relations computed by HKC(X+Y, Y ) and HKC(X+Y, X), respectively. If R ⊆ and R ⊇ are bisimulations up to congruence, then the following relation is a bisimulation up to congruence:

R= = {(X , Y ) | (X +Y , Y ) ∈ R ⊆ or (X +Y , X ) ∈ R ⊇ }.
On the contrary, checking the equivalence directly actually allows one to skip some pairs that cannot be skipped when reasoning by double inclusion. As an example, consider the DFA on the right of Figure 2. The relation computed by HKC(x, u) contains only four pairs (because the fifth one follows from transitivity). Instead, the relations built by HKC(x, x+u) and HKC(u+x, u) would both contain five pairs: transitivity cannot be used since our relations are now oriented (from y ≤ v, z ≤ v and z ≤ w, we cannot deduce y ≤ w). Another example, where we get an exponential factor by checking the equivalence directly rather than through the two inclusions, can be found in Section 4.2.4.

In a sense, the behaviour of the coinduction proof method here is similar to that of standard proofs by induction, where one often has to strengthen the induction predicate to get a (nicer) proof.

Antichain algorithm

In [START_REF] Wulf | Antichains: A new algorithm for checking universality of finite automata[END_REF], De Wulf et al. have proposed the antichain approach for checking language inclusion of NFA. We show that this approach can be explained in terms of simulations up to upward-closure that, in turn, can be seen as a special case of bisimulations up to congruence. Before doing so, we recall the standard notion of antichain and we describe the antichain algorithm (AC).

Given a partial order (X, ), an antichain is a subset Y ⊆ X containing only incomparable elements (that is, for all y1, y2 ∈ Y , y1 y2 and y2 y1). AC exploits antichains over the set S × P(S), where the ordering is given by (x1, Y1)

(x2, Y2) iff x1 = x2 and Y1 ⊆ Y2.
In order to check

[[X]] ⊆ [[Y ]
] for two sets of states X, Y of an NFA (S, o, t), AC maintains an antichain of pairs (x , Y ), where x is a state of the NFA and Y is a state of the determinised automaton. More precisely, the automaton is explored nondeterministically (via t) for obtaining the first component of the pair and deterministically (via t ) for the second one. If a pair such that x is accepting (o(x ) = 1) and Y is not (o (Y ) = 0) is encountered, then a counter-example has been found. Otherwise all derivatives of the pair along the automata transitions have to be inserted into the antichain, so that they will be explored. If one these pairs p is larger than a previously encountered pair p (p p) then the language inclusion corresponding to p is subsumed by p so that p can be skipped; otherwise, if p p1, . . . , pn for some pairs p1, . . . , pn that are already in the antichain, then one can safely remove these pairs: they are subsumed by p and, by doing so, the set of visited pairs remains an antichain. Remark 4. An important difference between HKC and AC consists in the fact that the former inserts pairs in todo without checking whether they are redundant (this check is performed when the pair is processed), while the latter removes all redundant pairs whenever a new one is inserted. Therefore, the cost of an iteration with HKC is merely the cost of the corresponding congruence check, while the cost of an iteration with AC is merely that of inserting all successors of the corresponding pair and simplifying the antichain.

Note that the above description corresponds to the "forward" antichain algorithm, as described in [START_REF] Abdulla | When simulation meets antichains[END_REF]. Instead, the original antichain algorithm, as first described in [START_REF] Wulf | Antichains: A new algorithm for checking universality of finite automata[END_REF], is "backward" in the sense that the automata are traversed in the reversed way, from accepting states to initial states. The two versions are dual [START_REF] Wulf | Antichains: A new algorithm for checking universality of finite automata[END_REF] and we could similarly define the backward counterpart of HKC and HK. We however stick to the forward versions for the sake of clarity.

Coinductive presentation

Leaving apart the concrete data structures used to manipulate antichains, we can rephrase this algorithm using a coinductive framework, like we did for Hopcroft and Karp's algorithm.

First define a notion of simulation, where the left-hand side automaton is executed non-deterministically: Definition 8 (Simulation). Given two relations T, T ⊆ S ×P(S), T s-progresses to T , denoted T s T , if whenever x T Y then 1. o(x) ≤ o (Y ) and 2. for all a ∈ A, x ∈ ta(x), x T t a (Y ).

A simulation is a relation T such that T s T . As expected, we obtain the following coinductive proof principle:

Proposition 4 (Coinduction). For all sets X, Y , we have [[X]] ⊆ [[Y ]

] iff there exists a simulation T such that for all x ∈ X, x T Y .

(Note that like for our notion of bisimulation, the above notion of simulation is weaker than the standard one from concurrency theory [START_REF] Milner | Communication and Concurrency[END_REF], which strictly entails language inclusion-Remark 3.)

To account for the antichain algorithm, where we can discard pairs using the preorder , it suffices to define the upward closure function : P(S × P(S)) → P(S × P(S)) as

T = {(x, Y ) | ∃(x , Y ) ∈ T s.t. (x , Y ) (x, Y )} .
A pair belongs to the upward closure T of a relation T ⊆ S × P(S), if and only if this pair is subsumed by some pair in T . In fact, rather than trying to construct a simulation, AC attempts to construct a simulation up to upward closure.

Like for HK and HKC, this method can be justified by defining the appropriate notion of s-compatible function, showing that any simulation up to an s-compatible function is contained in a simulation, and showing that the upward closure function ( ) is s-compatible.

Comparing HKC and AC

The efficiency of the two algorithms strongly depends on the number of pairs that they need to explore. In the following (Sections 4.2.3 and 4.2.4), we show that HKC can explore far fewer pairs than AC, when checking language inclusion of automata that share some states, or when checking language equivalence. We would also like to formally prove that (a) HKC never explores more than AC, and (b) when checking inclusion of disjoint automata, AC never explores more than HKC. Unfortunately, the validity of these statements highly depends on numerous assumptions about the two algorithms (e.g., on the exploration strategy) and their potential proofs seem complicated and not really informative. For these reasons, we preferred to investigate the formal correspondence at the level of the coinductive proof techniques, where it is much cleaner.

Language inclusion: HKC can mimic AC

As explained in Section 3.6, we can check the language inclusion of two sets X, Y by executing HKC(X+Y, Y ). We now show that for any simulation up to upward closure that proves the inclusion

[[X]] ⊆ [[Y ]],
there exists a bisimulation up to congruence of the same size which proves the same inclusion. For T ⊆ S × P(S), let T ⊆ P(S) × P(S) denote the relation

{(x + Y, Y ) | x T Y }. Lemma 9. We have T ⊆ c( T ). Proof. If (x + Y, Y ) ∈ T , then there exists Y ⊆ Y such that (x, Y ) ∈ T . By definition, (x + Y , Y ) ∈ T and (Y, Y ) ∈ c( T ). By the rule (u), (x + Y + Y, Y + Y ) ∈ c( T ) and since Y ⊆ Y , (x + Y, Y ) ∈ c( T ). Proposition 5. If T is a simulation up to , then T is a bisimulation up to c. Proof. First observe that if T s T , then T u ω ( T ). There- fore, if T s T , then T u ω ( T ). By Lemma 9, T u ω (c( T )) = c( T ).
(Note that transitivity and symmetry are not used in the above proofs: the constructed bisimulation up to congruence is actually a bisimulation up to context (r ∪ u ∪ id) ω .)

The relation T is not the one computed by HKC, since the former contains pairs of the shape (x + Y, Y ), while the latter has pairs of the shape (X + Y, Y ) with X possibly not a singleton. However, note that manipulating pairs of the two kinds does not change anything since by Lemma 7, (X + Y, Y ) ∈ c(R) iff for all x ∈ X, (x + Y, Y ) ∈ c(R).

Inclusion: AC can mimic HKC on disjoint automata

As shown in Section 4.2.3 below, HKC can be faster than AC, thanks to the up to transitivity technique. However, in the special case where the two automata are disjoint, transitivity cannot help, and the two algorithms actually match each other.

Suppose that the automaton (S, o, t) is built from two disjoint automata (S1, o1, t1) and (S2, o2, t2) as described in Remark Proof. Suppose that x c(R) Y , i.e., x ∈ X with X + Y c(R) Y . By Lemma 7, we have X ⊆ Y ↓R, and hence, x ∈ Y ↓R. By definition of R the pairs it contains can only be used to rewrite from right to left; moreover, since S1 and S2 are disjoint, such rewriting steps cannot enable new rewriting rules, so that all steps can be performed in parallel: we have Y ↓R = X +Y R Y ⊆Y X . Therefore, there exists some X , Y with x ∈ X , X +Y R Y , and Proof. First observe that for all relations R, R

Y ⊆ Y . It follows that (x, Y ) ∈ R, hence (x, Y ) ∈ (R).
, if R R , then R s R . Therefore, if R c(R), then R s c(R)
. We deduce R s (R) by Lemma 10.

Inclusion: AC cannot mimic HKC on merged automata

The containment of Lemma 10 does not hold when S1 and S2 are not disjoint, since c can exploit transitivity, while cannot. For a concrete grasp, take R = {(x + y, y), (y + z, z)} and observe that (x, z) ∈ c(R) but (x, z) / ∈ (R). This difference makes it possible to find bisimulations up to c that are much smaller than the corresponding simulations up to , and for HKC to be more efficient than AC. Such an example, where HKC is exponentially better than AC for checking language inclusion of automata sharing some states, is given in [START_REF] Bonchi | Web appendix for this paper[END_REF].

Language equivalence: AC cannot mimic HKC.

AC can be used to check language equivalence, by checking the two underlying inclusions. However, checking equivalence directly can be better, even in the disjoint case. To see this on a simple example, consider the DFA on the right-hand side of Figure 2. If we use AC twice to prove x ∼ u, we get the following antichains T1 = {(x, u), (y, v), (y, w), (z, v), (z, w)} , T2 = {(u, x), (v, y), (w, y), (v, z), (w, z)} , containing five pairs each. Instead, four pairs are sufficient with HK or HKC, thanks to up to symmetry and up to transitivity. For a more interesting example, consider the family of NFA given in Figure 5, where n is an arbitrary natural number. Taken together, the states x and y are equivalent to the state z: they recognise the language (a+b) (a+b) n+1 . Alone, the state x (resp. y) recognises the language (a+b) a(a+b) n (resp. (a+b) b(a+b) n ).

For i ≤ n, let Xi = x+x1+ . . . +xi, Yi = y+y1+ . . . +yi, and Zi = z+z1+ . . . +zi; for N ⊆ [1..i], furthermore set

X N i = x + j∈N xj , Y N i = y + j∈[1..n]\N yj .
In the determinised NFA, x + y can reach all the states of the shape X N i +Y The smallest bisimulation relating x + y and z is

R ={(X N i + Y N i , Zi) | i ≤ n, N ⊆ [1..i]},
which contains 2 n+1 -1 pairs. This is the relation computed by Naive(x, y) and HK(x, y)-the up to equivalence technique (alone) does not help in HK. With AC, we obtain the antichains Tx + Ty (for

8 2012/7/11 [[x + y]] ⊆ [[z]]) and Tz (for [[x + y]] ⊇ [[z]])
, where:

Tx = {(xi, Zi) | i ≤ n}, Ty = {(yi, Zi) | i ≤ n}, Tz = {(zi, X N i + Y N i ) | i ≤ n, N ⊆ [1.
.i]}. Note that Tx and Ty have size n + 1, and Tz has size 2 n+1 -1.

The language recognised by x or y are known for having a minimal DFA with 2 n states [START_REF] Hopcroft | Introduction to Automata Theory, Languages and Computation[END_REF]. So, checking x + y ∼ z via minimisation (e.g., [START_REF] Brzozowski | Canonical regular expressions and minimal state graphs for definite events[END_REF][START_REF] Hopcroft | An n log n algorithm for minimizing in a finite automaton[END_REF]) would also require exponential time. This is not the case with HKC, which requires only polynomial time in this case. Indeed, HKC(x+y, z) builds the relation

R = {(x + y, z)} ∪ {(x + Yi + yi+1, Zi+1) | i < n} ∪ {(x + Yi + xi+1, Zi+1) | i < n}
which is a bisimulation up to congruence and which only contains 2n + 1 pairs. To see that this is a bisimulation up to congruence, consider the pair (x+y+x1+y2, Z2) obtained from (x+y, z) after reading the word ba. This pair does not belong to R but to its congruence closure. Indeed, we have

x+y+x1+y2 c(R ) Z1+y2 (x+y+x1 R Z1) c(R ) x+y+y1+y2 (x+y+y1 R Z1) c(R ) Z2 (x+y+y1+y2 R Z2)
(Check Lemma 18 in Appendix D for a complete proof.)

Exploiting Similarity

Looking at the example in Figure 5, a natural idea would be to first quotient the automaton by graph isomorphism. By doing so, we would merge the states xi, yi, zi, and we would obtain the following automaton, for which checking x+y ∼ z is much easier. : :

m1 a,b / / • • • a,b / / mn z a,b 8 8 a,b
: :

As shown by Abdulla et al. [START_REF] Abdulla | When simulation meets antichains[END_REF], one can actually do better with the antichain algorithm, by exploiting any preorder contained in language inclusion (e.g., similarity [START_REF] Milner | Communication and Concurrency[END_REF]). In this section, we rephrase this technique for antichains in our coinductive framework, and we show how this idea can be embedded in HKC, resulting in an even stronger algorithm.

AC with similarity: AC'

For the sake of clarity, we fix the preorder to be similarity, which can be computed in quadratic time [START_REF] Henzinger | Computing simulations on finite and infinite graphs[END_REF]: Definition 9 (Similarity). Similarity is the largest relation on states ⊆ S × S such that x y entails:

1. o(x) ≤ o(y) and 2. for all a ∈ A, x ∈ S such that x a → x , there exists some y such that y a → y and x y .

One extends similarity to a preorder ∀∃ ⊆ P(S) × P(S) on sets of states, and to a preorder ⊆ (S × P(S)) × (S × P(S)) on antichain pairs, as:

X ∀∃ Y if ∀x ∈ X, ∃y ∈ Y, x y , (x , Y ) (x, Y ) if x x and Y ∀∃ Y .
The new antichain algorithm [START_REF] Abdulla | When simulation meets antichains[END_REF], which we call AC', is similar to AC, but the antichain is now taken w.r.t. the new preorder . Formally, let : P(S × P(S)) → P(S × P(S)) be the function defined for all relations T ⊆ S × P(S), as

T = {(x, Y ) | x ∀∃ Y , or ∃(x , Y ) ∈ T s.t. (x , Y ) (x, Y )}.
While AC consists in trying to build a simulation up to , AC' tries to build a simulation up to , i.e., it skips a pair (x, Y ) if either (a) it is subsumed by another pair of the antichain or (b) x ∀∃ Y .

Theorem 5. Any simulation up to is contained in a simulation.

Corollary 4. The antichain algorithm proposed in [START_REF] Abdulla | When simulation meets antichains[END_REF] is sound and complete: for all sets X, Y ,

[[X]] ⊆ [[Y ]] iff AC'(X, Y ).
Optimisation 1(a) and optimisation 1(b) in [START_REF] Abdulla | When simulation meets antichains[END_REF] are simply (a) and (b), as discussed above. Another optimisation, called Optimisation 2, is presented in [START_REF] Abdulla | When simulation meets antichains[END_REF]: if y1 y2 and y1, y2 ∈ Y for some pair (x, Y ), then y1 can be safely removed from Y . Note that while this is useful to store smaller sets, it does not allow one to explore less, since the pairs encountered with or without optimisation 2 are always equivalent w.r.t. the ordering : Y ∀∃ Y \ y1 and, for all a ∈ A, t a (Y ) ∀∃ t a (Y \ y1).

HKC with similarity: HKC'

Although HKC is primarily designed to check language equivalence, we can also extend it to exploit the similarity preorder. It suffices to notice that for any similarity pair x y, we have x+y ∼ y.

Let denote the relation {(x+y, y) | x y}, let r denote the constant to function, and let c = (r ∪s∪t∪u∪id) ω . Accordingly, we call HKC' the algorithm obtained from HKC (Figure 4) by replacing (X,

Y ) ∈ c(R ∪ todo) with (X, Y ) ∈ c (R ∪ todo) in step 3.2.
Notice that the latter test can be reduced to rewriting thanks to Theorem 3 and the following lemma.

Lemma 11. For all relations R, c (R) = c(R ∪ ).

In other words to check whether (X, Y ) ∈ c (R ∪ todo), it suffices to compute the normal forms of X and Y w.r.t. the rules from R ∪ todo plus the rules x + y ← y for all x y. Theorem 6. Any bisimulation up to c is contained in a bisimulation.

Proof. Consider the constant function r : P(P(S) × P(S)) → P(P(S)×P(S)) mapping all relations to ∼. Since language equivalence (∼) is a bisimulation, we immediately obtain that this function is compatible. Thus so is the function c = (r ∪s∪t∪u∪id) ω . We have that is contained in ∼, so that any bisimulation up to c is a bisimulation up to c . Since c is compatible, such a relation is contained in a bisimulation, by Proposition 3.

Note that in the above proof, we can replace by any other relation contained in ∼. Intuitively, bisimulations up to c correspond to classical bisimulations up to bisimilarity [START_REF] Milner | Communication and Concurrency[END_REF] from concurrency.

Corollary 5. For all sets X, Y , we have X ∼ Y iff HKC'(X, Y ).

Relationship between HKC' and AC'

Like in Section 4.2.1, we can show that for any simulation up to there exists a corresponding bisimulation up to c , of the same size.

Lemma 12. For all relations T ⊆ S × P(S), T ⊆ c ( T ). Proposition 7. If T is a simulation up to , then T is a bisimulation up to c . : : However, even for checking inclusion of disjoint automata, AC' cannot mimic HKC', because now the similarity relation allows one to exploit transitivity. To see this, consider the example given in Figure 6, where we want to check that

x1 a,b / / • • • a,b / / xn a k k y b / / a,b : : y1 a,b / / • • • a,b / / yn c k k z a,b / / a,b : : z1 a,b / / • • • a,b / / zn a,b k k x z x1 z1 . . .
[[z]] ⊆ [[x + y]],
and for which the similarity relation is shown on the right-hand side.

Since this is an inclusion of disjoint automata, HKC and AC, which do not exploit similarity, behave the same (cf. Sections 4.2.1 and 4.2.2). Actually, they also behave like HK and they require 2 n+1 -1 pairs. On the contrary, the use of similarity allows HKC' to prove the inclusion with only 2n + 1 pairs, by computing the following bisimulation up to c (Lemma 19 in Appendix E):

R = {(z+x+y, x+y)} ∪ {(Zi+1+Xi+y+yi+1, Xi+y+yi+1) | i < n} ∪ {(Zi+1+Xi+1+y, Xi+1+y) | i < n} ,
where Xi = x+x1+ . . . +xi and Zi = z+z1+ . . . +zi.

Like in Section 4.2.4, to see that this is a bisimulation up to c (where we do exploit similarity), consider the pair obtained after reading the word ab: (Z2+x+y+x2+y1, x+y+x2+y1). This pair does not belong to R or c(R ), but it does belong to c (R ). Indeed, by Lemmas 7 and 11, this pair belong to c (R ) iff Z2 ⊆ (x+y+x2+y1)↓ R ∪ , and we have

x+y+x2+y1 R ∪ Z1+x+y+y1+x2 (Z1+x+y+y1 R x+y+y1) R ∪ Z1+X1+y+y1+x2 = Z1+X2+y+y1 (x1 z1) R ∪ Z2+X2+y+y1+x2 (Z2+X2+y R X2+y)
On the contrary, AC' is not able to exploit similarity in this case, and it behaves like AC: both of them compute the same antichain Tz as in the example from Section 4.2.4, which has 2 n+1 -1 elements.

In fact, even when considering inclusion of disjoint automata, the use of similarity tends to virtually merge states, so that HKC' can use the up to transitivity technique which AC and AC' lack.

A short recap

Experimental assessment

To get an intuition of the average behaviour of HKC on various NFA, and to compare it with HK and AC, we provide some benchmarks on random automata and on automata obtained from model-checking problems. In both cases, we conduct the experiments on a MacBook pro 2.4GHz Intel Core i7, with 4GB of memory, running OS X Lion (10.7.4). We use our OCaml implementation for HK, HKC, and HKC' [START_REF] Bonchi | Web appendix for this paper[END_REF], and the libvata C++ library for AC and AC' [START_REF] Lengál | Vata: A library for efficient manipulation of non-deterministic tree automata[END_REF]. (To our knowledge, libvata is the most efficient implementation currently available for the antichain algorithms.)

Random automata

For a given size n, we generate a thousand random NFA with n states and two letters. According to [START_REF] Tabakov | Experimental evaluation of classical automata constructions[END_REF], we use a linear transition density of 1.25 (which means that the expected out-degree of each state and with respect to each letter is 1.25): Tabakov and Vardi empirically showed that one statistically gets more challenging NFA with this particular value. We generate NFA without accepting states: by doing so, we make sure that the algorithms never encounter a counter-example, so that they always continue until they find a (bi)simulation up to: these runs correspond to their worst cases for all possible choices of accepting states for the given NFA. 2We run all algorithms on these NFA, starting from two distinct singleton sets, to measure the required time and the number of processed pairs: for HK, HKC, and HKC', this is the number of pairs put into the bisimulation up to (R); for AC and AC', this is the number of pairs inserted into the antichain. The timings for HKC' and AC' do not include the time required to compute similarity.

We report the median values (50%), the last deciles (90%), the last percentiles (99%), and the maximum values (100%) in Table 1. For instance, for n = 70, 90% of the examples require less than 155ms with HK; equivalently, 10% of the examples require more than 155ms. (For a few tests, libvata ran out of memory, whence the ∞ symbols in the table.) We also plotted on Figure 8 the distribution of the number of processed pairs when n = 100.

HKC and AC are several orders of magnitude better than HK, and HKC is usually two to ten times faster than AC. Moreover, for the first four lines, HKC is much more predictable than AC, i.e., the last percentiles and maximal values are of the same order as the median value. (AC seems to become more predictable for larger values of n.) The same relative behaviour can be observed between HKC' and AC'; moreover, HKC alone is apparently faster than AC'.

Also recall that the size of the relations generated by HK is a lower bound for the number of accessible states of the determinised NFA (Lemma 6 (2)); one can thus see in Table 1 that HKC usually explores an extremely small portion of these DFA (e.g., less than one per thousand for n = 100). The last column reports the median size of the minimal DFA for the corresponding parameters, as given in [START_REF] Tabakov | Experimental evaluation of classical automata constructions[END_REF]. HK usually explores much many states than what would be necessary with a minimal DFA, while HKC and AC need much less.

Automata from model-checking

Checking language inclusion of NFA can be useful for modelchecking, where one sometimes has to compute a sequence of NFA 1.

by iteratively applying a transducer, until a fixpoint is reached [START_REF] Bouajjani | Abstract regular model checking[END_REF].

To know that the fixpoint is reached, one typically has to check whether an NFA is contained in another one. Abdulla et al. [START_REF] Abdulla | When simulation meets antichains[END_REF] use such benchmarks to test their algorithm (AC') against the plain antichain algorithm (AC [START_REF] Wulf | Antichains: A new algorithm for checking universality of finite automata[END_REF]). We reuse them to test HKC' against AC' in a concrete scenario. We take the sequences of automata kindly provided by L. Holik, which roughly corresponds to those used in [START_REF] Abdulla | When simulation meets antichains[END_REF] and which come from the model checking of various programs (the bakery algorithm, bubble sort, and a producer-consumer system). For all these sequences, we check the inclusions of consecutive pairs, in both directions. We separate the results into those for which a counter-example is found, and those for which the inclusion holds. We skip the trivial inclusions which hold by similarity ( ∀∃ ), and for which both HKC' and AC' stop immediately.

The results are given in Table 2. Even though these are inclusions of disjoint automata, HKC' is faster than AC' on these examples: up to transitivity can be exploited thanks to the similarity pairs, and larger parts of the determinised NFA can be skipped.

Related work

A similar notion of bisimulation up to congruence has already been used to obtain decidability and complexity results about contextfree processes, under the name of self-bisimulations. Caucal [START_REF]Graphes canoniques de graphes algébriques[END_REF] introduced this concept to give a shorter and nicer proof of the result by Baeten et al. [START_REF] Baeten | Decidability of bisimulation equivalence for processes generating context-free languages[END_REF]: bisimilarity is decidable for normed context-free processes. Christensen et al [START_REF] Christensen | Bisimulation equivalence is decidable for all context-free processes[END_REF] then generalised the result to all context-free processes, also by using self-bisimulations. Hirshfeld et al. [START_REF] Hirshfeld | A polynomial algorithm for deciding bisimilarity of normed context-free processes[END_REF] used a refinement of this notion to get a polynomial algorithm for bisimilarity in the normed case.

There are two main differences with the ideas we presented here. First, the above papers focus on bisimilarity rather than language equivalence (recall that although we use bisimulation relations, we check language equivalence since we work on the determinised NFA-Remark 3). Second, we consider a notion of bisimulation up to congruence where the congruence is taken with respect to non-determinism (union of sets of states). Selfbisimulations are also bisimulations up to congruence, but the congruence is taken with respect to word concatenation. We cannot consider this operation in our setting since we do not have the corresponding monoid structure in plain NFA.

Other approaches, that are independent from the algebraic structure (e.g., monoids or semi-lattices) and the behavioural equivalence (e.g., bisimilarity or language equivalence) are shown in [START_REF] Bartels | On generalized coinduction and probabilistic specification formats[END_REF][START_REF] Lenisa | From set-theoretic coinduction to coalgebraic coinduction: some results, some problems[END_REF][START_REF] Lucanu | Circular coinduction with special contexts[END_REF][START_REF] Pous | Complete lattices and up-to techniques[END_REF]. These propose very general frameworks into which our up to congruence technique fits as a very special case. To our knowledge, bisimulation up to congruence has never been proposed as a technique for proving language equivalence of NFA.

Conclusions and future work

We showed that the standard algorithm by Hopcroft and Karp for checking language equivalence of DFA relies on a bisimulation up to equivalence proof technique; this allowed us to design a new algorithm (HKC) for the non-deterministic case, where we exploit a novel technique called up to congruence.

We then compared HKC to the recently introduced antichain algorithms [START_REF] Wulf | Antichains: A new algorithm for checking universality of finite automata[END_REF] (AC): when checking the inclusion of disjoint automata, the two algorithms are equivalent, in all the other cases HKC is more efficient since it can use transitivity to prune a larger portion of the state-space.

The difference between these two approaches becomes even more striking when considering some optimisation exploiting similarity. Indeed, as nicely shown with AC' [START_REF] Abdulla | When simulation meets antichains[END_REF], the antichains approach can widely benefit from the knowledge one gets by first computing similarity. Inspired by this work, we showed that both our proof technique (bisimulation up to congruence) and our algorithm (HKC) can be easily modified to exploit similarity. The resulting algorithm (HKC') is now more efficient than AC' even for checking language inclusion of disjoint automata.

We provided concrete examples where HKC and HKC' are exponentially faster than AC and AC' (Sections 4.2.4 and 5.3) and we proved that the coinductive techniques underlying the formers are at least as powerful as those exploited by the latters (Propositions 5 and 7). We finally compared the algorithms experimentally, by running them on both randomly generated automata, and automata resulting from model checking problems. It appears that for these examples, HKC and HKC' perform better than AC and AC'.

Finally note that our implementation of the presented algorithms is available online [START_REF] Bonchi | Web appendix for this paper[END_REF], together with an applet making it possible to test them on user-provided examples.

As future work, we plan to extend our approach to tree automata. In particular, it seems promising to investigate if further up-to techniques can be defined for regular tree expressions. For instance, the algorithms proposed in [START_REF] Aiken | Implementing regular tree expressions[END_REF][START_REF] Hosoya | Regular expression types for XML[END_REF] exploit some optimisation which suggest us coinductive up-to techniques.

Proof. Let T [[

-]] be the relation {(x, Y ) | [[x]] ⊆ [[Y ]]}. We prove that T [[-]] is a simulation. If x T [[-]] Y , then o(x) = [[x]]( ) ≤ [[Y ]]( ) = o (Y ). Moreover, for all a ∈ A x ∈ ta(x) and w ∈ A * , [[x ]](w) ⊆ [[x]](a • w) ⊆ [[Y ]](a • w) = [[t a (Y )]](w) that means [[x ]] ⊆ [[t a (Y )]], that is ta(x) T [[-]] t a (Y ).
We now prove the other direction. Let T be a simulation. We want to prove that x T Y entails Proof. By Lemma 16, it suffices to show that is s-compatible. Suppose that T s T , we have to show that T s T . Assume that x T Y .

• if x ∀∃ Y then x y for some y ∈ Y . Therefore, we have o(x) ≤ o(y) ≤ o (Y ) and for all a ∈ A, x ∈ ta(x), we have some y ∈ ta(y) with x y . Since ta(y) ⊆ t a (Y ), we deduce x ∀∃ t a (Y ), and hence x T t a (Y ), as required.

• otherwise, we have some (x , Y ) ∈ T such that (x , Y ) (x, Y ), i.e., x x and Y ∀∃ Y . Since T s T , we have o(x) ≤ o(x ) ≤ o (Y ) ≤ o (Y ). Now take some x ∈ ta(x), we have some x ∈ ta(x ) with x

x , and since T s T , we know x T t a (Y ). It suffices to show that t a (Y ) ∀∃

X i + Y1 R ∪ X i + Y1 + Z1 R ∪ X i + Y1 + Z1 + x1
where the first reduction is given by (Z1 + X0 + y + y1, X0 + y + y1) ∈ R and the second by x1 z1. Since X i + x1 = Xi, then one can apply the third kind of pairs in R , so that X i + Y1 * R ∪ Xi + Y1 + Zi that is Zi ⊆ (X i + Y1)↓ R ∪ . By Lemmas 7 and 11, this means that Zi + X i + Y1 c (R ) X i + Y1

If we moreover have yi+1, we can apply the second kind of pair in R and obtain

X i + Y1 + yi+1 * R ∪ Xi + Y1 + Zi+1 + yi+1 that is Zi+1 + X i + Y1 + yi+1 c (R ) X i + Y1 + yi+1 (3)
With ( 2) and (3), it is easy to prove that R is a bisimulation up to c , by simply proceeding by cases:

( 3 )Figure 1 .

 31 Figure 1. Naive algorithm for checking the equivalence of states x and y of a DFA (S, o, t); R and todo are sets of pairs of states. The code of HK(x, y) is obtained by replacing step 3.2 with if (x , y ) ∈ e(R) then skip.

Figure 2 .

 2 Figure 2. Checking for DFA equivalence.

Theorem 1 .

 1 Any bisimulation up to e is contained in a bisimulation.

Figure 3 .

 3 Figure 3. Bisimulations up to congruence, on a single letter NFA.

Figure 4 .

 4 Figure 4. On-the-fly naive algorithm, for checking the equivalence of sets of states X and Y of a NFA (S, o, t). The code for onthe-fly HK(X, Y ) is obtained by replacing the test in step 3.2 with (X , Y ) ∈ e(R); the code for HKC(X, Y ) is obtained by replacing this test with (X , Y ) ∈ c(R ∪ todo).

Lemma 5 .

 5 The three algorithms require at most 1 + v•|R| iterations, where |R| is the size of the produced relation; moreover, this bound is reached whenever they return true.

Theorem 4 .Corollary 3 .

 43 Any simulation up to is contained in a simulation. For all X, Y ∈ P(S),[[X]] ⊆ [[Y ]] iff AC(X, Y ).

  1. Let R be the relation obtained by running HKC(X0+Y0, Y0) with X0 ⊆ S1 and Y0 ⊆ S2. All pairs in R are necessarily of the shape (X+Y, Y ) with X ⊆ S1 and Y ⊆ S2. Let R ⊆ S × P(S) denote the relation {(x, Y ) | ∃X, x ∈ X and X+Y R Y }. Lemma 10. If S1 and S2 are disjoint, then c(R) ⊆ (R).

Proposition 6 .

 6 If S1 and S2 are disjoint, and if R is a bisimulation up to congruence, then R is a simulation up to upward closure.

Figure 5 .

 5 Figure 5. Family of examples where HKC exponentially improves over AC and HK; we have x + y ∼ z.

Ni

  , for i ≤ n and N ⊆ [1..i]. For instance, for n=i=2, we have x+y aa → x+y+x1+x2, x+y ab → x+y+y1+x2, x+y ba → x+y+x1+y2, and x+y bb → x+y+y1+y2. Instead, z reaches only n+1 distinct states, those of the form Zi.

Figure 6 .

 6 Figure 6. Family of examples where HKC' exponentially improves over AC', for inclusion of disjoint automata: we have [[z]] ⊆ [[x+y]].

Figure 7

 7 Figure 7 summarises the relationship amongst the presented algorithms, in the general case and in the special case of language inclusion of disjoint automata. In this diagram, an arrow X→Y (from an algorithm X to Y) means that (a) Y can explore less states than X, and (b) Y can mimic X, i.e., the proof technique of Y is at least as powerful as the one of X. (The labels on the arrows point to the sections showing these relations; unlabelled arrows are not illustrated in this paper, they are easily inferred from what we have shown.)

Figure 7 .

 7 Figure 7. Relationship between the various algorithms.

  [[x]] ⊆ [[Y ]], i.e., for all w ∈ A * , [[x]](w) ≤ [[Y ]](w). We proceed by induction on w. For w = , we have [[x]]( ) = o(x) ≤ o (Y ) = [[Y ]]( ). For w = a • w , since T is a simulation, we have ta(x) T t a (Y ) and thus [[ta(x)]](w ) ≤ [[t a (Y )]](w ) by induction. This allows us to conclude since [[x]](a • w ) = [[ta(x)]](w ) and [[y]](a • w ) = [[t a (y)]](w ). Definition 10. A function f : P(S × P(S)) → P(S × P(S)) is scompatible if is monotone and for all relations T, T ⊆ S × P(S), T s T entails f (T ) s f (T ). Lemma 16. Any simulation T up to an s-compatible function f (T s f (T )) is contained in a simulation, namely f ω (T ).Proof. Same proof as for Proposition 3.Lemma 17. The upward closure function is s-compatible.Proof. We assume that T s T and we prove thatT s T . If x T Y , then ∃Y ⊆ Y such that x T Y . Since Y ⊆ Y , o (Y ) ≤ o (Y ) and t a (Y ) ⊆ t a (Y ) for all a ∈ A. SinceT s T and x T Y , then o(x) ≤ o (Y ) ≤ o (Y ) and ta(x) T t a (Y ) for all a ∈ A.

Theorem 4 . 5 Theorem 5 .

 455 Any simulation up to is contained in a simulation.Proof. By Lemmas 16 and 17.Lemma 18. The relationR = {(x + y, z)} + {(x + Yi + yi+1, Zi+1) | i < n} + {(x + Yi + xi+1, Zi+1) | i < n}is a bisimulation up to congruence for the NFA in Fig.5.Proof. First notice thatX1 + y c(R ) x + Y1 c(R ) Z1We then consider each kind of pair of R separately:• (x, y): we have o (x + y) = 0 = o (z) and t a (x + y) = X1 + y R Z1 = t a (z) and, similarly, t b (x + y) = x + Y1 R Z1 = t b (z). • (x + Yi + yi+1, Zi+1): both members are accepting iff i + 1 = n; setting j = min(i + 2, n), we have t a (x + Yi + yi+1) = X1 + y + y2 + • • • + yj c(R ) x + Y1 + y2 + • • • + yj = x + Yj R Zj = t a (Zi+1)andt b (x + Yi + yi+1) = x + Yj R Zj = t b (Zi+1)• (x + Yi + xi+1, Zi+1): both members are accepting iff i + 1 = n; if i + 1 < n then we have:t a (x + Yi + xi+1) = X1 + y + y2 + • • • + yi+1 + xi+2 c(R ) x + Y1 + y2 + • • • + yi+1 + xi+2 = x + Yi+1 + xi+2 R Zi+2 = t a (Zi+1)andt b (x + Yi + xi+1) = x + Yi+1 + xi+2 R Zi+2 = t b (Zi+1)otherwise, i.e., i + 1 = n, notice that:x + Yn + xn c(R ) Zn + yn c(R ) x + Yn + yn = x + Yn c(R ) Zn = t a (Zn) ,from which we deduce:t a (x + Yi + xn) = X1 + y + y2 + • • • + yn + xn c(R ) x + Y1 + y2 + • • • + yn + xn = x + Yn + xn c(R ) t a(Zn) and t b (x + Yi + xn) = x + Yn + xn c(R ) t a (Zn)E. Proofs of Section Any simulation up to is contained in a simulation.

Lemma 11 .

 11 t a (Y ) to conclude; this follows easily from Y ∀∃ Y and from the definition of similarity. For all relations R, c (R) = c(R ∪ ).Proof. The inclusion c(R ∪ ) ⊆ c (R) is trivial. For the other inclusion we take d = r ∪s∪t∪u∪id and we prove by induction that for all natural numbers n,d n (R) ⊆ c(R ∪ ). For n = 0, d 0 (R) = R ⊆ c(R ∪ ). For n + 1, d n+1 (R) = d(d n (R)). By induction hypothesis, d n (R) ⊆ c(R ∪ ) and, by monotonicity of d, d(d n (R)) ⊆ d(c(R ∪ )). By definition of d, the latter is equal to c(R ∪ ).Lemma 12. For all relations T ⊆ S × P(S), T ⊆ c ( T ).

15 2012/7/ 11 Proof.Proposition 7 .

 117 If (x + Y, Y ) ∈ T , then either (a) x ∀∃ Y or (b) there exists x x and Y ∀∃ Y such that (x , Y ) ∈ T . We have to show (x+Y, Y ) ∈ c ( T ), i.e., (x+Y, Y ) ∈ c( T + ) by Lemma 11, that is x ∈ Y ↓ T + by Lemma 7. For (b), we have:Y T + Y + Y (Y ∀∃ Y ) T + Y + Y + x ((x +Y , Y ) ∈ T ) T + Y + Y + x + x (x x )x ∈ Y ↓ T + follows by confluence (Lemma 4). For (a), we immediately have that Y T + Y + x. If T is a simulation up to , then T is a bisimulation up to c .Proof. First observe that if T s T , then T u ω ( T ). Therefore, if T s T , then T u ω ( T ). By Lemma 12, T u ω (c ( T )) = c ( T ). Lemma 19. The relation R = {(z+x+y, x+y)} ∪ {(Zi+1+Xi+y+yi+1, Xi+y+yi+1) | i < n} ∪ {(Zi+1+Xi+1+y, Xi+1+y) | i < n} ,is a bisimulation up to c for the NFA in Figure6.Proof. Let X i be the set Xi without x1 and note that Xi a → Xi+1 and Xi b → X i+1 . First we observe that for all i,

•

  (z+x+y, x+y): we have o (x+y+z) = 0 = o (x+y) and t a (x+y+z) = Z1+X1+y R X1 + y = t a (x+y) and, similarly, t b (x+y+z) = Z1+x+Y1 R x+Y1 = t b (z).• (Zi+1+Xi+y+yi+1, Xi+y+yi+1) and i < n -1: both members are not accepting;t a (Zi+1+Xi+y+yi+1) = Zi+2+Xi+1+y+yi+2 R Xi+1+y+yi+2 = t a (Xi+y+yi+1)andt b (Zi+1+Xi+y+yi+1) = Zi+2+X i+1 +Y1+yi+2 c (R ) X i+1 +Y1+yi+2 = t b (Xi+y+yi+1)• (Zn+Xn-1+y+yn, Xn-1+y+yn) and i = n -1: both members are accepting;t a (Zn+Xn-1+y+yn) = Zn+Xn+y R Xn+y = t a (Xn-1+y+yn)andt b (Zn+Xn-1+y+yn) = Zn+X n +Y1 c (R ) X n +Y1 = t b (Xn-1+y+yn)• (Zi+1+Xi+1+y, Xi+1+y) and i < n -1: both members are not accepting;t a (Zi+1+Xi+1+y) = Zi+2+Xi+2+y R Xi+2+y = t a (Xi+1+y)andt b (Zi+1+Xi+1+y) = Zi+2+X i+2 +Y1 c(R ) X i+2 +Y1 = t b(Xi+1+y)• (Zn+Xn+y, Xn+y): both members are accepting; Moreover, t a (Zn+Xn+y) = Zn+Xn+y R Xn+y = t a (Xn+y) and t b (Zn+Xn+y) = Zn+X n +Y1 c(R ) X n +Y1 = t b (Xn+y)The cases for the letter c are always trivial since Zi c

  Each state is a set of states of the NFA, final states are overlined: they contain at least one final state of the NFA. The numbered lines show a relation which is a bisimulation containing x and u.

/ 1 {y} a / / 2 {z} a / / 3 {x, y} a / / 4 {y, z} a / / 5 {x, y, z} a G G 6 {u} a / / {v, w} a / / {u, w} a / / {u, v, w} a } }

Table 1 .

 1 Running the five presented algorithms to check language equivalence on random NFA with two letters. Distributions of the number of processed pairs, for the 1000 NFA with 100 states and 2 letters from Table

				AC	0.009	0.010	0.028	0.750	562	622	2232	14655
				HKC AC'	0.001 0.012	0.002 0.013	0.003 0.022	0.009 0.970	86 433	104 484	118 920	132 14160	-
				HKC'	0.001	0.001	0.002	0.006	76	91	104	116
				AC	0.014	0.015	0.039	∞	918	986	2571	∞
			500	HKC AC'	0.002 0.025	0.005 0.028	0.008 0.042	0.018 ∞	130 710	154 772	176 1182	193 ∞	-
				HKC'	0.002	0.004	0.007	0.013	115	136	154	169
				AC	0.029	0.031	0.038	∞	1808	1878	2282	∞
			1000	HKC AC'	0.007 0.074	0.022 0.080	0.055 0.092	0.093 ∞	228 1409	271 1488	304 1647	337 ∞	-
				HKC'	0.008	0.019	0.041	0.077	202	238	265	299
		250
							HK
							AC
							AC'
		200					HKC
	number of checked NFA	100 150					HKC'
		50
		0
		10	100	1000	10000		100000	1e+06
				number of processed pairs
	Figure 8.

Table 2 .

 2 Running HKC' and AC' to test language inclusion of disjoint NFA generated from model-checking.

	number of processed pairs	number of tests

There are few exceptions, like[START_REF] Lee | Online minimization of transition systems (extended abstract)[END_REF] which minimises labelled transition systems w.r.t. bisimilarity rather than trace equivalence.[Copyright notice will appear here once 'preprint' option is removed.]

2012/7/11

2012/7/11

2012/7/11

2012/7/11

2012/7/11

2012/7/11

To get this behaviour for AC and AC', we actually had to trick libvata, which otherwise starts by removing non-coaccessible states, and thus reduces any of these NFA to the empty one. 10 2012/7/11

2012/7/11

2012/7/11

2012/7/11

A. Smallest bisimulation and compositionality

In this appendix, we show some (unrelated) properties that have been discussed through the paper, but never formally stated.

The first property concerns the relation computed by Naive(x, y). The following proposition shows that it is the smallest bisimulation relating x and y. Proposition 8. Let x and y be two states of a DFA. Let RNaive be the relation built by Naive(x, y). If Naive(x, y) = true, then RNaive is the smallest bisimulation relating x and y, i.e., RNaive ⊆ R, for all bisimulations R such that (x, y) ∈ R.

Proof. We have already shown in Proposition 2 that RNaive is a bisimulation. We need to prove that it is the smallest. Let R be a bisimulation such that (x, y) ∈ R. For all words w ∈ A * and pair of states (x , y ) such that x w → x and y w → y , it must hold that (x , y ) ∈ R (by definition of bisimulation).

By construction, for all (x , y ) ∈ RNaive there exists a word w ∈ A * , such that x w → x and y w → y . Therefore all the pairs in RNaive must be also in R, that is RNaive ⊆ R.

The second property is

which we have used in the Introduction to give an intuition of bisimulation up to context and to show that the problem of language inclusion can be reduced to language equivalence. We believe that this property is interesting, since it follows from the categorical observation made in [START_REF] Silva | Generalizing the powerset construction, coalgebraically[END_REF] that determinised NFA are bialgebras [START_REF] Turi | Towards a mathematical operational semantics[END_REF], like CCS processes. For this reason, we prove here that [[-]] : P(S) → 2 A * is a semi-lattice homomorphism.

Theorem 7. Let (S, o, t) be a non-deterministic automaton and (P(S), o , t ) be the corresponding deterministic automaton obtained through the powerset construction. The function [[-]] : P(S) → 2 A * is a semi-lattice homomorphism, that is, for all X1, X2 ∈ P(S),

Proof. We prove that for all words

, by induction on w.

• for , we have:

• for a • w, we have:

(by definition)

For the second part, we prove that for all words w ∈ A * , [[0]](w) = 0, again by induction on w. Base case:

that by induction hypothesis is 0.

B. Proofs of Section 2

Proposition 1. Two states are language equivalent iff there exists a bisimulation that relates them.

We now prove the other direction. Let R be a bisimulation. We want to prove that x R y entails

. We proceed by induction on w. For w = , we have

f ω : the (omega) iteration of a compatible function f .

Proof. The first two points are straightforward; For the third one, assume that F is a family of compatible functions. Suppose that R R ; for all f ∈ F , we have

For the last one, assume that f is compatible; for all n, f n is compatible because (a) f 0 = id is compatible (by the first point) and (b) f n+1 = f • f n is compatible (by the second point and induction hypothesis). By definition f ω = n f n and thus, by the third point, f ω is compatible.

Lemma 2. The following functions are compatible:

Proof. r: observe that the identity relation

S} is always a bisimulation, i.e., Id Id. Thus for all R, R r(R) = Id Id = r(R ). s: observe that the definition of progression is completely symmetric. Therefore, if R R , then s(R) s(R ). t: assume that R R . For each (x, z) ∈ t(R), there exists y such that (x, y) ∈ R and (y, z) ∈ R. By assumption, (1) o (x) = o (y) = o (z) and ( 2) for all a ∈ A, t a (x) R t a (y) R t a (z), that is t a (x) t(R ) t a (z).

C. Proofs of Section 3

Lemma 4. For all relations R, the relation R is convergent.

Proof. We have that Z R Z implies |Z | > |Z|, where |X| denotes the cardinality of the set X (note that R is irreflexive). Since |Z | is bounded by |S|, the number of states of the NFA, the relation R is strongly normalising. We can also check that whenever Z R Z1 and Z R Z2, either Z1 = Z2 or there is some Z such that Z1 R Z and Z2 R Z . Therefore, R is convergent.

Lemma 14. Let X, Y ∈ P(S), we have (X + Y )↓R = (X↓R + Y ↓R)↓R.

Proof. Follows from confluence (Lemma 4) and from the fact that for all Z, Z , U , Z R Z entails U + Z = R U + Z .

Theorem 3. For all relations R, and for all X, Y ∈ P(S), we have

Proof. From right to left. We proceed by induction on the derivation of (X, Y ) ∈ c(R). The cases for rules r, s, and t are straightforward. For rule id, suppose that X R Y , we have to show X↓R = Y ↓R:

R X + Y . (In the last three cases, we conclude by confluence-Lemma 4.) For rule u, suppose by induction that Xi↓R = Yi↓R for i ∈ 1, 2; we have to show that (X1 + Y1)↓R = (X2 + Y2)↓R. This follows by Lemma 14. From left to right. By Lemma 13, we have X c(R) X↓R for any set X, so that X c(R) X↓R = Y ↓R c(R) Y . Lemma 5. The three algorithms require at most 1+v•|R| iterations, where |R| is the size of the produced relation; moreover, this bound is reached whenever they return true.

Proof. At each iteration, one pair is extracted from todo. The latter contains one pair before entering the loop and v pairs are added to it every time that a pair is added to R. Lemma 15. Let x and y be two states of a DFA. Let RNaive and RHK be relations computed by Naive(x, y) and HK(x, y), respectively. If Naive(x, y) = HK(x, y) = true, then e(RNaive) = e(RHK).

Proof. By the proof of Proposition 3, e ω (RHK) is a bisimulation. Since e is idempotent, we have e ω = e and thus e(RHK) is a bisimulation; we can thus deduce by Proposition 8 that RNaive ⊆ e(RHK). Moreover, by definition of the algorithms, we have RHK ⊆ RNaive. Summarising,

It follows that e(RHK) = e(RNaive), e being monotonic and idempotent. Lemma 6. Let RNaive, RHK, and RHKC denote the relations produced by the three algorithms. We have

where m ≤ 2 n is the number of accessible states in the determinised NFA and n is the number of states of the NFA. If the algorithms returned true, we moreover have By construction, RHKC ⊆ RNaive and, since e is monotonic, e(RHKC) ⊆ e(RNaive) = e(RHK) (the latter equality is given by Proposition 15). In particular, there are more equivalence classes in e(RHKC) than in e(RHK); using the same argument as above, we deduce that |RHKC| ≤ |RHK|. Lemma 8. Let X, Y be two sets of states; let R ⊆ and R ⊇ be the relations computed by HKC(X+Y, Y ) and HKC(X+Y, X), respectively. If R ⊆ and R ⊇ are bisimulations up to congruence, then the following relation is a bisimulation up to congruence:

Proof. Let (X , Y ) ∈ R= and suppose that (X +Y , Y ) ∈ R ⊆ (the other case is symmetric).

First notice that all pairs in R ⊇ necessarily have the shape (t w (X+Y ), t w (X)), for some word w. Since R ⊇ is a bisimulation up to congruence, c(R ⊇ ) is a bisimulation. Since (X+Y, X) ∈ c(R ⊇ ) then, for all words w, (t w (X+Y ), t w (X)) ∈ c(R ⊇ ) and thus (X +Y , X ) ∈ c(R ⊇ ) (we have X = t w (X) and Y = t w (Y ) for some word w).

Since c(R ⊆ ) and c(R ⊇ ) are bisimulations containing (X +Y , Y ) and (X +Y , X ), it holds that:

2. for all a, t a (X + Y ) c(R ⊇ ) t a (X ) and t a (X + Y ) c(R ⊆ ) t a (Y ).

By Lemma 7, t a (Y ) ⊆ t a (X )↓R ⊇ and X ⊆ t a (Y )↓R ⊆ and since all the rewriting rules for R ⊆ and R ⊇ are also rewriting rules for R=, then t a (Y ) ⊆ t a (X )↓R = and t a (X ) ⊆ t a (Y )↓R = .

By the first observation in the proof of Lemma 7, this means that t a (X ) c(R=) t a (Y ).

D. Proofs of Section 4

Proposition 4. For all sets X, Y , we have

] iff there exists a simulation T such that for all x ∈ X, x T Y .