Angluin-Style Learning of NFA

1 Introduction

Learning automata has a wide field of applications ranging over robotics and control systems, pattern recognition, computational linguistics, computational biology, data compression, data mining, etc. (see [de la Higuera, 2005] for an excellent survey). Recently, learning techniques have also become popular in the area of automatic verification. They have been used [Leucker, 2007] for minimizing (partially) specified systems and for model checking black-box systems, proved helpful in compositional model checking and in regular model checking. To put it bluntly, automata learning is en vogue.

The general goal of learning algorithms employed in verification is to identify a machine, usually of minimal size, that conforms with an a priori fixed set of strings or a given machine. Nearly all algorithms learn deterministic finitestate automata (DFA) or deterministic finite-state machines (Mealy-/Moore machines), as the class of DFA has preferable properties in the setting of learning. For every regular language, there is a unique minimal DFA accepting it, which can be characterized thanks to Nerode's right congruence. This characterization is at the base of most learning algorithms.

In general, two types of learning algorithms for DFA can be distinguished, so-called online and offline algorithms. Of- Carsten Kern MOVES, RWTH Aachen kern@cs.rwth-aachen.de Martin Leucker Institut f¨ur Informatik, TU Munich leucker@in.tum.de fline algorithms get a fixed set of positive and negative examples, comprising strings that should be accepted and, respectively, strings that should be rejected by the automaton in question. The learning algorithm now has to provide a (minimal) automaton that accepts the positive examples and rejects the negative ones. For deriving minimal automata, major achievements are due to Biermann [Biermann and Feldman, 1972], Trakhtenbrot and Barzdin [Trakhtenbrot and Barzdin, 1973]. Efficient algorithms inferring a not necessarily minimal DFA are given in [Lang, 1992] and [Oncina and Garcia, 1992] under the name RPNI.

∗Work supported by DAAD/EGIDE (Procope 2008/2009).

Online algorithms have the possibility to ask further queries, i.e., whether some string is in the language of the automaton to learn or not. In this way, an online algorithm can enlarge the set of examples as needed.

A popular setup for an online approach is that of Angluin's L∗ algorithm [Angluin, 1987]: A minimal DFA is learned based on membership and equivalence queries. We have a learner whose job is to come up with the automaton to learn, a teacher who may answer if a given string is in the language as well as an oracle answering if the automaton hypothesis currently proposed by the learner is correct or not.

DFA have a serious drawback for applications in verification. In general, a DFA might be exponentially bigger than a non-deterministic finite-state automaton (NFA). For many applications, it would be a huge improvement to work with an exponentially more succinct NFA rather than the corresponding DFA. As such, learning algorithms for NFA are needed. However, the class of NFA lacks important properties that are essential for current learning algorithms: There is no unique minimal NFA for a given regular language and there is no characterization of NFA in terms of right-congruence classes.

In a seminal paper, Denis et al. [Denis et al., 2002] introduce the class of residual finite-state automata (RFSA). It is a subclass of NFA that shares important properties with the class of DFA: For every regular language, there is a unique minimal canonical RFSA accepting it. The states of this automaton correspond to right-congruence classes, or, equivalently, to residuals of the accepted language. At the same time, the RFSA can be exponentially more succinct than the corresponding DFA. As such, RFSA are the preferable class for learning regular languages. In [Denis et al., 2004], Denis et al. provided an offline algorithm, called DeLeTe2, which works in the spirit of RPNI. Alternatives and extensions to this algorithms have then been presented, most recently in [Garc´ıa et al., 2008], which also gives a nice overview on offline algorithms for learning NFA.

In this paper, we introduce NL∗ as an online learning algorithm for RFSA, patterned after L∗ . Using membership and equivalence queries, our algorithm infers a (minimal) canonical RFSA for the language in question, which is always smaller than or equal to the corresponding DFA. Note that [Yokomori, 1994] presents an online learning algorithm for NFA based on contradiction backtracking. According to [Denis et al., 2004], the resulting NFA are actually RFSA. They are, however, not canonical and can even be larger than the corresponding minimal DFA, as their size crucially depends on the size of counterexamples provided by the oracle.

We have implemented our algorithm and studied its efficiency on a collection of regular languages described by regular expressions. It turns out that, for most examples, the resulting RFSA is much smaller than the corresponding DFA. While our current upper bounds for NL∗ on the number of membership and equivalence queries are slightly worse than those for L∗ , our implementation shows that the resulting RFSA are typically obtained after far fewer queries. Summarizing, we provide a new learning algorithm for regular languages. Together with a practically efficient oracle realization based on anti-chains [De Wulf et al., 2006], we expect it to enhance, e.g., associated verification tasks considerably.

Full proofs can be found in [Bollig et al., 2008].

2 Preliminaries

We fix a finite set Σ of letters, called alphabet. Finite sequences of letters are elements of Σ∗ , called words. Subsets of Σ∗ are termed languages. For w ∈ Σ∗ , we denote by Pref (w) (resp. Suff (w)) the set of its prefixes (resp. suffixes) including w itself and the empty word ϵ. A non-deterministic finite-state automaton (NFA) A = (Q, Q0, F, δ) has a finite set of states Q, a set of initial states Q0 ⊆ Q, a set of final states F ⊆ Q, and a transition function δ : Q× Σ → 2Q. A is a deterministic finite-state automaton (DFA) if |Q0| = 1 and |δ(q, a)| = 1 for all q ∈ Q and a ∈ Σ. As usual, δ is extended to ¯ δ : Q × Σ∗ → 2Q by ¯ δ(q, ϵ) = {q} and ¯ δ(q, aw) = ⋃q′ ∈δ(q,a) ¯ δ(q′ ,w), and to sets Q′ ⊆ Q by ˆ δ(Q′ , w) = ⋃q∈Q′ ¯ δ(q, w). We use δ to denote both ¯ δ and ˆ δ. For q ∈ Q, let Lq = {w ∈ Σ∗ | δ(q, w) ∩ F ̸= ∅}. The language L(A) accepted by A is ⋃q∈Q0 Lq. Two automata are equivalent if they accept the same language. It is folklore that the languages of finite-state automata are the regular ones. We call a DFA minimal if there is no equivalent DFA with strictly fewer states. In contrast to NFA, a DFA has always a unique minimal representative, as shown by Myhill/Nerode.

Residual Finite-State Automata RFSA, introduced in the seminal work [Denis et al., 2002], are a subclass of NFA inheriting some desirable features of DFA. Important for learning, every regular language is accepted by a canonical RFSA with a minimal number of states. As this does not hold for arbitrary NFA, it seems difficult to come up with learning algorithms for the whole class of NFA. At the same time, like for NFA, RFSA can be exponentially more succinct than DFA.

Technically, RFSA and DFA have the property that the states of the automata correspond to so-called residual languages defined below. This is in general not true for NFA.

Definition 1 (Residual Language) For L ⊆ Σ∗ and u ∈ Σ∗ , we denote by u-1L the set {v ∈ Σ∗ | uv ∈ L}. A language L′ ⊆ Σ∗ is a residual language (or, simply, residual) of L if there is u ∈ Σ∗ with L′ = u-1L. We denote by Res(L) the set of residual languages of L.

The Myhill-Nerode theorem states that the number of residuals of a language is finite iff this language is regular [Nerode, 1958]. Moreover, for a minimal DFA A, there is a natural bijection between its states and the residual languages of L(A).

Definition 2 (Residual Finite-State Automaton) A residual finite-state automaton (RFSA) is an NFA R = (Q, Q0, F, δ) such that, for each q ∈ Q, Lq ∈ Res(L(R)).

In other words, each state accepts a residual language of L(R), but not every residual language must be accepted by a single state. Intuitively, the states of an RFSA form a class of states of the corresponding minimal DFA. Yet, using nondeterminism, certain states of a minimal DFA are not needed as they correspond to the union of languages of other states. To this end, we distinguish prime and composed residuals:

Definition 3 (Prime and Composed Residuals) Let L ⊆ Σ∗ . A residual L′ ∈ Res(L) is called composed if there are L1, . . . , Ln ∈ Res(L) \ {L′} such that L′ = L1 ∪ . . . ∪ Ln. Otherwise, it is called prime. The set of prime residuals of L is denoted by Primes(L).

We can now define the canonical RFSA of a regular language. The idea is that its set of states corresponds exactly to its prime residuals. Moreover, the transition function should be saturated in the sense that a transition to a state should exist if it does not change the accepted language.

Definition 4 (Canonical RFSA) Let L ⊆ Σ∗ be a regular language. The canonical RFSA of L, denoted by R(L), is the NFA (Q, Q0, F, δ) where Q = Primes(L), Q0 = {L′ ∈ Q | L′ ⊆ L}, F = {L′ ∈ Q | ϵ ∈ L′}, and δ(L1, a) = {L2 ∈ Q | L2 ⊆ a-1L1}.

Note that R(L) is indeed an RFSA and we actually have L(R(L)) = L. We say that an RFSA R is canonical if it is the canonical RFSA of L(R).

Angluin's Learning Algorithm L∗ The algorithm from [Angluin, 1987] learns or infers a minimal DFA for a given regular language L. A so-called Learner, who initially knows nothing about L, is trying to learn a DFA A such that L(A) = L. To this end, it repeatedly asks queries to a Teacher and an Oracle, who both know L. There are two kinds of queries: A membership query consists of asking the Teacher if a string w ∈ Σ∗ is in L, and an equivalence query consists of asking the Oracle whether a hypothesized DFA H is correct, i.e., whether L(H) = L. The Oracle answers yes if H is correct, or, otherwise, supplies a counterexample w, drawn from the symmetric difference of L and L(H).

The Learner maintains a prefix-closed set U ⊆ Σ∗ of words that are candidates for identifying states, and a suffixclosed set V ⊆ Σ∗ of words used to distinguish those states. Words of U are called access strings and words of V experiments. U and V are both initialized to {ϵ} and increased when needed. The Learner makes membership queries for all words in (U ∪ UΣ)V , and organizes the results into a table T = (T, U, V ) where function T maps each w ∈ (U ∪ UΣ)V to an element from {+, -}. Here, + means accepted and - not accepted. To u ∈ U ∪ UΣ, we assign a function row(u) : V → {+, -} given by row(u)(v) = T (uv). Any such function is called a row of T , and the set of all rows of a table is denoted by Rows(T ). We let Rowsupp(T ) = {row(u) | u ∈ U} denote the set of rows representing the "upper" part of the table. The rows from Rowslow(T ) = {row(u) | u ∈ UΣ} occur in its "lower" part. Table T is closed if, for all u ∈ U and a ∈ Σ, there is u′ ∈ U such that row(ua) = row(u′ ). It is consistent if, for all u, u′ ∈ U and a ∈ Σ, row(u) = row(u′ ) implies row(ua) = row(u′a).

If T is not closed, then we find u′ ∈ UΣ such that row(u) ̸= row(u′ ) for all u ∈ U. We move u′ to U and ask membership queries for every u′av where a ∈ Σ and v ∈ V . Likewise, if T is not consistent, then we find u, u′ ∈ U, a ∈ Σ, and v ∈ V such that row(u) = row(u′ ) and row(ua)(v) ̸= row(u′a)(v). In that case, we add av to V and ask membership queries for every u′′av with u′′ ∈ U ∪UΣ. When T is closed and consistent, the Learner constructs a hypothesized DFA H = (Q,Q0, δ, F) where Q = Rowsupp(T ) = {row(u) | u ∈ U}, Q0 = {row(ϵ)}, δ is defined by δ(row(u), a) = {row(ua)}, and F = {r ∈ Q | r(ϵ) = +}. Then, the Learner submits H to an equivalence query (asking whether L(H) = L). If the answer is yes, the learning procedure is completed. Otherwise, the returned counterexample u is processed by adding every prefix of u (including u) to U, extending UΣ accordingly, and performing membership queries to make the table closed and consistent, whereupon a new hypothesized DFA is constructed, etc.

Remark 1 L∗ can be modified by changing the treatment of counterexamples. Instead of adding the counterexample and its prefixes to U, one can add the counterexample and all its suffixes to V ensuring that the table is always consistent [Maler and Pnueli, 1995].

3 Learning of Residual Finite-State Automata

We will now modify Angluin's learning algorithm L∗ , which infers DFA, towards learning of NFA in terms of RFSA.

From Tables to RFSA To simplify our presentation, we follow Angluin's notions and notation. We use tables T = (T, U, V ) with a prefix-closed set of words U, a suffix-closed set V , and a mapping T : (U ∪ UΣ)V → {+, -}. We associate with a word u ∈ U ∪ UΣ a mapping row(u) : V → {+, -}. Members of U are used to reach states and members of V to distinguish states. We adopt notations introduced before such as Rows(T ), Rowsupp(T ), and Rows low(T ).

The main difference in the new approach is that not all rows of the table will correspond to states of the hypothesized automaton, but only certain prime rows. Essentially, we have to define for rows what corresponds to 'union', 'composed', 'prime', and 'subset' previously introduced for languages.

Definition 5 (Join Operator) Let T = (T, U, V ) be a table. The join (r1 ⊔ r2) : V → {+, -} of rows r1, r2 ∈ Rows(T ) is defined, for v ∈ V , by (r1 ⊔ r2)(v) = r1(v) ⊔ r2(v) where - ⊔ - = - and + ⊔ + = + ⊔ - = - ⊔ + = +.

Note that the join operator is associative, commutative, and idempotent, yet that the join of two rows is not necessarily a row of table T .

Definition 6 (Composed, Prime Rows) Let T = (T, U, V ) be a table. A row r ∈ Rows(T ) is called composed if there are rows r1, . . . , rn ∈ Rows(T ) \ {r} such that r = r1 ⊔ . . . ⊔ rn. Otherwise, r is called prime. The set of prime rows in T is denoted by Primes(T ). Moreover, we let Primes upp(T ) = Primes(T ) ∩ Rowsupp(T ).

Definition 7 (Covering Relation) Let T = (T, U, V ) be a table. A row r ∈ Rows(T ) is covered by row r′ ∈ Rows(T ), denoted by r ⊑ r′ , if, for all v ∈ V , r(v) = + implies r′ (v) = +. If, moreover, r′ ̸= r, then r is strictly covered by r′ , denoted by r ⊏ r′ .

As for L∗ , we now define concepts comparable to closedness and consistency called RFSA-closedness and RFSAconsistency. For DFA, closedness ensures that every row in the lower part also occurs in the upper part. For RFSA, this translates to the idea that each row of the lower part of the table is composed of (prime) rows from the upper part.

Definition 8 (RFSA-Closedness) A table T = (T, U, V ) is called RFSA-closed if, for each r ∈ Rowslow(T ), r = ⊔{r′ ∈ Primesupp(T ) | r′ ⊑ r}.

Note that a table is RFSA-closed iff any prime row of the lower part is a prime row of the upper part of the table.

The idea of consistency in the DFA case was as follows: Assume that two words u and u′ of the table have the same row. This suggests that both words lead to the same state of the automaton to learn as they cannot be distinguished by words v ∈ V . Hence, they induce the same residuals. Then, however, ua and u′a have to induce equal residuals as well, for any a ∈ Σ. In other words, if there is some a ∈ Σ and v ∈ V such that T(uav) ̸= T(u′av), then the residuals induced by u and u′ cannot be the same and must be distinguishable by the suffix av to be added to V .

For RFSA, if there are u and u′ with row(u) ⊑ row(u′ ), then this suggests that the residual induced by u is a subset of the residual induced by u′ . If indeed so, then the same relation must hold for the successors ua and u′a.

Definition 9 (RFSA-Consistency) A table T = (T, U, V ) is called RFSA-consistent if, for all u, u′ ∈ U and a ∈ Σ, row(u′ ) ⊑ row(u) implies row(u′ a) ⊑ row(ua).

One might expect that the previous simple definitions smoothly lead to a straightforward extension of L∗ towards learning RFSA. This is, however, not the case. We now list some major difficulties that arise. First, an RFSA-closed and RFSA-consistent table does generally not represent a canonical RFSA, not even an RFSA. To put things right, we come up with an algorithm that produces NFA as intermediate hypotheses and outputs a canonical RFSA only in the last step. Second, termination of our algorithm crucially depends on the treatment of counterexamples, which need to be added to the set of suffixes held in a table. A third subtle point is that the number of states may decrease during a run of the algorithm. Thus, the termination proof requires reasoning on a measure that relates four indicators of a table such as the number of distinct rows or the number of upper prime rows.

So let us first associate an NFA to an RFSA-closed and RFSA-consistent table. As above-mentioned, we show that this NFA corresponds to a canonical RFSA only after our learning algorithm has terminated (Theorems 1 and 2).

For the rest of this subsection, we fix an RFSA-closed and RFSA-consistent table T = (T, U, V ).

Definition 10 (NFA of a Table) We define RT to be the NFA (Q, Q0, F, δ) with Q = Primesupp(T ), Q0 = {r ∈ Q | r ⊑ row(ϵ)}, F = {r ∈ Q | r(ϵ) = +}, and δ(row(u), a) = {r ∈ Q | r ⊑ row(ua)} for u ∈ U with row(u) ∈ Q, a ∈ Σ.

Note that Primesupp(T ) = Primes(T ), as T is RFSAclosed. Also, δ is well-defined: Take u, u′ with row(u) = row(u′ ). Then, row(u) ⊑ row(u′ ) and row(u′ ) ⊑ row(u). Consistency implies row(ua) ⊑ row(u′a) and row(u′a) ⊑ row(ua) so that both resulting rows are the same.

Let us establish some elementary properties of RT . The proof of the first two lemmas is by simple inductions.

Lemma 1 Let RT = (Q,Q0, F, δ). For all u ∈ U and r ∈ δ(Q0, u), we have r ⊑ row(u).

Lemma 2 Let RT = (Q, Q0, F, δ). For each r ∈ Q and v ∈ V , we have (1) r(v) = - iff v ̸∈ Lr, and (2) row(ϵ)(v) = - iff v ̸∈ L(RT ).

Lemma 2 may be summarized by saying that each state of RT correctly classifies strings of V . This fact will enable us to prove that the covering relation precisely reflects language inclusion, as stated in the next lemma.

Lemma 3 Let RT = (Q,Q0, F, δ). For every r1, r2 ∈ Q, r1 ⊑ r2 iff Lr1 ⊆ Lr2 .

Proof: Let r1, r2 ∈ Q and assume u1, u2 ∈ U with row(u1) = r1 and row(u2) = r2. "only if": Suppose r1 ⊑ r2 and w ∈ Lr1 . We distinguish two cases. Assume first w = ϵ. Then, row(u1)(ϵ) = + and, due to r1 ⊑ r2, row(u2)(ϵ) = +. Thus, r2 ∈ F so that ϵ ∈ Lr2 . Now let w = aw′ with a ∈ Σ. We have δ(r1, aw′ ) ∩ F ̸= ∅. Thus, there is r ∈ δ(r1, a) such that δ(r,w′ ) ∩ F ̸= ∅. From r1 ⊑ r2, we obtain, by RFSA-consistency, row(u1a) ⊑ row(u2a). By definition of δ, r ⊑ row(u1a), which implies r ⊑ row(u2a). Thus, r ∈ δ(r2, a) and we have aw′ ∈ Lr2 . "if": Assume r1 ̸⊑ r2. We show that Lr1 ̸⊆ Lr2 . By definition of ⊑, there exists v ∈ V with row(u1)(v) = + but row(u2)(v) = -. By Lemma 2, v ∈ Lr1 and v ̸∈ Lr2 . Therefore, Lr1 ̸⊆ Lr2 . □

The automaton RT constructed from T is not necessarily an RFSA [Bollig et al., 2008]. However, we show that RT is a canonical RFSA if it is consistent with T , i.e., if it correctly classifies all words from T .

Definition 11 RT is consistent with T if, for all words w ∈ (U ∪ UΣ)V , we have T (w) = + iff w ∈ L(RT ).

The next lemma is a stronger version of Lemma 1, if we additionally have that RT is consistent with T .

Lemma 4 If RT = (Q,Q0, F, δ) is consistent with T , then, for all u ∈ U with row(u) ∈ Q, we have row(u) ∈ δ(Q0, u).

Proof: Suppose row(u) ̸∈ δ(Q0, u). With Lemma 1, we have ∀r ∈ δ(Q0, u).r ⊑ row(u). Then, Lemma 3 implies ∀r ∈ δ(Q0, u).Lr ⊆ Lrow(u). As row(u) ∈ Q and row(u) ̸∈ δ(Q0, u), there is v ∈ V such that row(u)(v) = + and, for all r ∈ δ(Q0, u), r(v) = -. This, with Lemma 2, implies ∀r ∈ δ(Q0, u).v /∈ Lr. But then, uv ̸∈ L(RT ), a contradiction to the fact that RT is consistent with T . □

Theorem 1 Let T be RFSA-closed and RFSA-consistent and let RT be consistent with T . Then, RT is a canonical RFSA.

Proof: Let T = (T, U, V ) and assume RT = (Q, q0, F, δ). Set L = L(RT ). We first prove that RT is an RFSA. Let u ∈ U with row(u) ∈ Q. Let us show Lrow(u) = u-1L. By Lemma 4, we have row(u) ∈ δ(Q0, u), which implies Lrow(u) ⊆ u-1L. By Lemma 1, ∀r ∈ δ(Q0, u).r ⊑ row(u). Thus, with Lemma 3, ∀r ∈ δ(Q0, u).Lr ⊆ Lrow(u). This gives u-1L ⊆ Lrow(u). With Lrow(u) ⊆ u-1L, we have Lrow(u) = u-1L. As, by Lemma 3, the relation ⊑ over rows corresponds to the subset relation over languages, Lrow(u) is prime and the transition function δ is saturated. □

The Algorithm We now describe NL∗ , which takes a regular language L ⊆ Σ∗ as input. Its pseudo code is given in Algorithm1. After initializing the table T , the it is repeatedly checked for RFSA-closedness and RFSA-consistency. If the algorithm detects a prime row row(ua) that is not contained in Primesupp(T ) (a violation of the RFSA-closedness condition from Def. 8), then ua is added to U. This involves additional membership queries. On the other hand, whenever the algorithm perceives an RFSA-consistency violation (Def. 9), then a suffix av can be determined that makes two existing rows distinct or incomparable. In this case, a column is added to V invoking supplemental queries. This procedure is repeated until T is RFSA-closed and RFSA-consistent. If both properties are fulfilled, a conjecture RT can be derived from T (cf. Def. 10), and either a counterexample u from the symmetric difference of L and L(RT ) is provided and Suff (u) added to V invoking NL∗ , or the learning procedure terminates successfully. Note that the algorithm ensures that V is always suffix-closed and U prefix-closed.

Remark 2 The counterexamples are handled as described in Remark 1, since treating them as in L∗ leads to a nonterminating algorithm [Bollig et al., 2008]. Our treatment of counterexamples ensures that each row can appear at most once in the upper part of the table.

Proving termination of L∗ is quite straightforward. In our setting, however, the termination proof is intricate as, after an equivalence query or a violation of RFSA-consistency, the number of states of the hypothesized automaton does not necessarily increase [Bollig et al., 2008].

The following theorem constitutes our main contribution.

Theorem 2 Let n be the number of states of the minimal DFA A∗ for a given regular language L ⊆ Σ∗ . Let m be the length of the biggest counterexample returned by the equivalence test (or 1 if the equivalence test always succeeds). Then,

initialize T := (T, U, V ) for U = V = {ϵ} by memb. queries REPEAT WHILE T is not (RFSA-closed and RFSA-consistent) DO IF T is not RFSA-closed THEN find u ∈ U and a ∈ Σ with row(ua) ∈ Primes(T ) \ Primesupp(T ) extend T to (T ′ , U ∪ {ua}, V ) by memb. queries IF T is not RFSA-consistent THEN find u, u′ ∈ U, a ∈ Σ, and v ∈ V with T (uav) = -, T (u′av) = +, and row(u′ ) ⊑ row(u) extend T to (T ′ , U, V ∪ {av}) by memb. queries from T construct hypothesized NFART / / cf. Def. 10 IF (L = L(RT )) THEN equivalence test succeeds ELSE get counterexample w ∈ (L \ L(RT )) ∪ (L(RT ) \ L) extend T to (T ′ , U, V ∪ Suff (w)) by memb. queries UNTIL equivalence test succeeds RETURN RT

NL∗ returns, after at most O(n2 ) equivalence queries and O(m|Σ|n3 ) membership queries, the canonical RFSA R(L).

Proof: First of all, if the algorithm terminates, then it outputs the canonical RFSA for L due to Theorem 1, because passing the equivalence test implies that the constructed automaton must be consistent with the table. To show that the algorithm terminates after at most O(n2 ) equivalence queries, we create a measure M that associates a tuple of positive natural numbers to a table T . We let M(T ) = (lup, l, p, i), where lup = |Rowsupp(T )|, l = |Rows(T )|, p = |Primes(T )|, and i = |{(r, r′ ) | r, r′ ∈ Rows(T ) and r ⊏ r′ }|. An analysis of the evolution of M during an execution of NL∗ reveals that, after each extension of the table, either (1) lup is increased or (2) l is increased by k > 0 and, simultaneously, i is increased by at most kl+k(k-1)/2 or (3) l stays the same and i decreases or p increases. However, lup, l, and p cannot increase beyond n. Hence, the algorithmmust (a) always reach an equivalence query and (b) terminate after at most O(n2 ) equivalence queries. Concerning the number of membership queries, we notice that their maximal number corresponds to the size of the table which has at most n + n|Σ| (n rows in the upper part + their successors) rows and O(mn2 ) columns since at each extension at most m suffixes are added to V . □

The theoretical complexity of NL∗ wrt. equivalence (resp. membership) queries is higher compared to L∗ where at most n equivalence (resp. roughly |Σ|mn2 membership) queries are needed. But we observe that, in practice, fewer equivalence and membership queries are needed (cf. Section 4).

NL* bymeans of an Example SupposeΣ = {a, b} and let Ln ⊆ Σ∗ be given by the regular expression Σ∗ aΣn. I.e., Ln contains the words having an a at the (n+1)-last position. Then, Ln is accepted by a minimal DFA A∗n with 2n+1 states. However, it is easy to see that the canonical RFSAR(Ln) has n + 2 states (see Fig. 1 for n = 2). In other words, R(Ln) is exponentiallymore succinct than A∗n.

Next, we show how R(L2) is inferred by NL∗ :

Rows with a preceding ∗ are prime. The table T1 is RFSAclosed and RFSA-consistent but does not represent the target language because aaa is not accepted. We add aaa and its suffixes to V , performmembership queries, and obtain table T2, which is not RFSA-closed. We add a to U and continue. Resolving two more closedness violations, we obtain table T5, which is RFSA-closed and RFSA-consistent. Its automaton RT5 given in Fig. 1, is the canonical RFSA for L2. Notice that table T5 is not closed in Angluin's sense so that L∗ would continue adding strings to the upper part of the table.

4 Experiments

To evaluate the performance of our learning algorithm NL∗ , we compare it with Angluin's L∗ and its modification wrt. to Remark 1, called L∗col . As NL∗ is similar in spirit to L∗col , a comparison with this algorithm seems fairer. All algorithms have been implemented in Java and tested on a wide range of examples. Following [Denis et al., 2004], we randomly generate large sets of regular expressions over different sizes of alphabets. A detailed description of this as well as a full description of the outcome can be found in [Bollig et al., 2008]. As in [Denis et al., 2004], we present a characteristic selection of the results for an alphabet of size two.

Results We generated a set of 3180 regular expressions, resulting in minimal DFA of sizes between 1 and 200 states. These DFA were given to the learning algorithms, i.e., membership and equivalence queries were answered according to these automata. To evaluate the algorithms' performance, we measured, for each algorithm and input regular expression, the number of states of the final automaton (RSFA or DFA) and the number of membership (resp. equivalence) queries that are needed to infer it. As Fig. 2 (top) shows, the automata learned by NL∗ are considerably smaller than those that are returned by L∗ and L∗col , confirming the results of [Denis et al., 2004]. More importantly, in practice, the actual sizes of RFSA compared to DFA seem to follow an exponential gap.

In Fig. 2 (middle), the number of membership queries is depicted. As in the first case, NL∗ behaves much better than the other learning algorithms. While the difference between

# membership queries

the curves is rather small for automata with less than 40 states, it increases significantly for larger automata. The same is the case for the number of equivalence queries depicted in Fig. 2 (bottom). This is in contrast with the theoretical result we obtained in Theorem 2. The experiments we performed point out the clear predominance of NL∗ over L∗ and L∗col as long as the user is not dependent on a deterministic model.

5 Future Work

There is room for further improvement by adapting the various recent variants of L∗ (see [Leucker, 2007] for references). In the future, we plan to show that using our NL∗ algorithm, the limits of learning-based verification techniques can be pushed ahead considerably, as most often non-deterministic automata should be sufficient for verification tasks.