Angluin-Style Learning of Deterministic Büchi and Co-Büchi Automata

1 Introduction

In her seminal paper, Angluin [Angluin, 1987] proposed a learning framework that can learn an automaton representation of an unknown regular language R from an oracle. The learning algorithm or the learner can interact with the oracle by means of two types of queries, namely membership and equivalence queries. While membership queries ask whether a word u belongs to R, equivalence queries ask whether a given automaton correctly recognises the target language R. After asking a certain number of membership queries, the learner is able to propose a conjecture automaton and ask an equivalence query about the conjecture. When the oracle returns a positive answer to an equivalence query, the learner has completed his task and successfully learned R; otherwise, the learner will receive a counterexample from the oracle, which he will use to refine the current conjecture automaton. This learning procedure will continue until a correct automaton of R has been learned.

Since its introduction, Angluin-style learning frameworks have, for example, been applied in learning assumptions for compositional verification [Cobleigh et al., 2003], detecting bugs in network protocol implementations [de Ruiter and Poll, 2015], and extracting automata models for recurrent neural networks [Weiss et al., 2018].

Angluin-style learning has initially focused on learning automata that represent regular languages, especially deterministic finite automata (DFAs) [Angluin, 1987; Isberner et al., 2014; Vaandrager et al., 2022], but also nondeterministic finite automata [Bollig et al., 2009], and alternating automata [Angluin et al., 2015]. More recently, they have branched out into learning ω-regular languages represented by ω-automata, so far focusing on nondeterministic B¨uchi automata (NBAs) [Farzan et al., 2008; Li et al., 2021], where the current vehicle for learning them are families of DFAs (FDFAs) [Angluin and Fisman, 2016; Li et al., 2023a].

While NBAs are popular in verification, they are hard to reason about, because equivalence checking of NBAs is PSPACE-complete. For instance, the expensive resolution of equivalence queries is the reason why the learning-based complementation algorithm of NBAs [Li et al., 2018] cannot scale to large cases. While the operations of FDFAs are easy [Angluin et al., 2018], they have not yet found applications besides the learning.

For languages recognisable by deterministic B¨uchi automata (DBAs) or deterministic co-B¨uchi automata (DCAs), we may well encounter a situation, where the oracle is in effect in possession of a DBA or a DCA that recognises the target language. It will then be easy for her to answer equivalence queries. We can therefore turn to a run-of-the-mill oracle if our conjecture automata are also presented as DBAs or DCAs, respectively, whereas the answer to a PSPACE-hard question might require a trip to Delphi.

But can we make use of these cheap equivalence queries? Considering that FDFAs naturally translate to NBAs, the answer to this question is not straightforward. However, we observe that a translation from FDFAs in a particular normal form-limit FDFAs [Li et al., 2023a]-to a DBA that recognises a sub-language of the limit FDFAs, but will, for DBA recognisable languages, converge to the full language when the learning of the limit FDFA is complete. The tricky bit is to cover the case, where the counterexample is not in the language of the conjecture DBA, but is both in the language of the FDFA (or: the language of the NBA that represents it) and the target language.

The refinement of the FDFA for this case is slightly more involved than usual, but this complication is minor compared to the significant decrease in complexity-from PSPACE to NL-for the equivalence query itself. This balance of the expressiveness of learned languages and the complexity of equivalence queries provides the first Angluin-style learning algorithm for DBAs, the main contribution of this paper. Moreover, since DCAs are dual to DBAs, our algorithm can be easily adapted for learning DCAs by learning a DBA of the complement language of the target co-B¨uchi language.

Related work. Recent work has studied learning DBAs (and even deterministic parity automata) [Michaliszyn and Otop, 2022]; however, this work not only requires the oracle to answer membership and equivalence queries, but also needs to know the loop index of each queried infinite word in the target automaton. Such queries about the loop index of infinite words may not be feasible in some scenarios such as learning a representation of black-box systems where the inner structure of the system is unknown; it therefore does not fit into Angluin's learning framework. Angluin's learning framework can be classified as active learning, in contrast to passive learning, where automata are learned from a given set of labelled samples. We note that there is a passive learning algorithm for DBAs proposed in [Bohn and L¨oding, 2022], which is orthogonal to our work. An Angluin-style learning framework has been suggested for the smaller class of weak B¨uchi automata [Maler and Pnueli, 1995]. This work, however, only covers a strict subset of DBA languages, which behave like DFAs in that the states of weak B¨uchi automata simply represent the right congruence classes [Myhill, 1957; Nerode, 1958].

2 Preliminaries

In the whole paper, we fix a finite alphabet Σ. A word is a finite or infinite sequence of letters in Σ; ε denotes the empty word. Let Σ∗ and Σω denote the set of all finite and infinite words (or ω-words), respectively. In particular, we let Σ+ = Σ∗ \{ε}. A finitary language is a subset of Σ∗ ; an ω-language is a subset of Σω . Let ρ be a sequence; we denote by ρ[i] the i-th element of ρ and by ρ[i..k] the subsequence of ρ starting at the i-th element and ending at the (k-1)-th element when 0 ≤ i < k, and the empty sequence ε when i ≥ k. We denote by ρ[i . . .] the subsequence of ρ starting at the i-th element when i < |ρ|, and the empty sequence ε when i ≥ |ρ|. Given a finite word u and a word w, we denote by u · w (uw, for short) the concatenation of u and w.

Transition system. A (nondeterministic) transition system (TS) is a tuple T = (Q, q0, δ), where Q is a finite set of states, q0 ∈ Q is the initial state, and δ : Q×Σ → 2Q is a transition function. We also lift δ to sets as δ(S, σ) := ⋃q∈S δ(q, σ). We also extend δ to words in a usual way, by letting δ(S, ε) = S and δ(S, u · a) = δ(δ(S, u), a), where u ∈ Σ∗ and a ∈ Σ.

Automata. An automaton on finite words is called a nondeterministic finite automaton (NFA). An NFA A is formally defined as a tuple (T , F ), where T is a TS and F ⊆ Q is a set of final states. An automaton on ω-words is called a nondeterministic B¨uchi automaton (NBA). An NBA B is represented as a tuple (T , Γ) where T is a TS and Γ ⊆ {(q, a, q′ ) : q, q′ ∈ Q, a ∈ Σ, q′ ∈ δ(q, a)} is a set of accepting transitions. An NFA A is a deterministic finite automaton (DFA) if, for each q ∈ Q and a ∈ Σ, |δ(q, a)| ≤ 1. Deterministic B¨uchi automata (DBAs) are defined similarly and thus Γ is a subset of {(q, a) : q ∈ Q, a ∈ Σ}, since the successor q′ is determined by the source state and the input letter.

A run of an NFA A on a finite word u of length n ≥ 0 is a sequence of states ρ = q0q1 · · · qn ∈ Q+ such that, for every 0 ≤ i < n, qi+1 ∈ δ(qi, u[i]). We write q0 u-→qn if there is a run from q0 to qn over u. A finite word u ∈ Σ∗ is accepted by an NFA A if there is a run q0 · · · qn over u such that qn ∈ F . Similarly, an ω-run of A on an ω-word w is an infinite sequence of transitions ρ = (q0, w[0], q1)(q1, w[1], q2) · · · such that, for every i ≥ 0, qi+1 ∈ δ(qi,w[i]). Let inf(ρ) be the set of transitions that occur infinitely often in ρ. An ω-word w ∈ Σω is accepted by an NBA A if there is an ω-run ρ of A over w such that inf(ρ)∩Γ ̸= ∅. The finitary language recognised by an NFA A, denoted L∗(A), is defined as the set of finite words accepted by it. Similarly, we denote by L(A) the ω-language recognised by an NBA A, i.e. the set of ω-words accepted by A. NFAs/DFAs accept exactly regular languages while NBAs recognise exactly ω-regular languages.

Deterministic co-B¨uchi automata (DCA) are dual to DBAs and have the same structure as DBAs except that w is accepted by a DCA if its run satisfies that inf(ρ) ∩ Γ = ∅. For DCAs, Γ is called the set of rejecting transitions.

Right congruences. A right congruence (RC) relation is an equivalence relation ∽ over Σ∗ such that x ∽ y implies xv ∽ yv for all v ∈ Σ∗ . We denote by | ∽ | the index of ∽, i.e. the number of equivalence classes of ∽. A finite RC is an RC with a finite index. We denote by Σ∗ /∽ the set of equivalence classes of Σ∗ under ∽. Given x ∈ Σ∗ , we denote by [x]∽ the equivalence class of ∽ that x belongs to.

For a given regular language R, one can define the RC ∽R of R as x ∽R y if, and only if, ∀v ∈ Σ∗ . xv ∈ R ⇐⇒ yv ∈ R [Myhill, 1957; Nerode, 1958]. The RC ∽R also defines the minimal DFA D of R, in which each state of D corresponds to an equivalence class in Σ∗ /∽. Formally, the TS T [∽] of D is defined as follows.

Definition 1 ([Myhill, 1957; Nerode, 1958]). Let ∽ be an RC of finite index. The TS T [∽] induced by ∽ is a tuple (S, s0, δ) where S = Σ∗ /∽, s0 = [ε]∽, and for each u ∈ Σ∗ and a ∈ Σ, δ([u]∽, a) = [ua]∽.

The minimal DFA D of R is the DFA D = (T [∽R], F∽R ) where F∽R collects all classes [u]∽R such that u ∈ R.

Ultimately periodic words. For ω-regular languages, we only need to consider a type of ω-words called ultimately periodic (UP) words; a UP-word w is of the form uvω , where u ∈ Σ∗ and v ∈ Σ+. For an ω-language L, let UP(L) = {uvω ∈ L | u ∈ Σ∗ ∧ v ∈ Σ+ } denote the set of all UP-words in L. By [B¨uchi, 1962; Calbrix et al., 1993], two ω-regular languages L and L′ are equivalent if, and only if, UP(L) = UP(L′ ). That is, the set of UP-words of an ω-regular language L uniquely characterises L.

Output B[FB]

Figure 1: Overview of our DBA learning framework

As aforementioned, a UP-word w = uvω can be denoted as a pair of finite words such as (u, v), (uv, v) and other valid pairs; they are all called a decomposition of w.

Families of DFAs (FDFAs). FDFAs have been introduced to recognise an ω-regular language L by accepting the decompositions of UP(L) [Angluin et al., 2018].

Definition 2 ([Angluin et al., 2018]). An FDFA is a pair F = (M, {N q }) consisting of a leading DFA M and of a progress DFAN q for each state q inM.

Intuitively, for the FDFA F = (M, {N q }) to accept a UPword uvω ∈ UP(L), the leading DFAMfirst consumes the finite prefix u, reaching some state q and, for each state q of M, the progress DFAN q accepts the loop word v. Note that the leading DFAM of every FDFA is in fact only a TS since it does not make use of final states.

Let A be a deterministic automaton with TS T = (Q, q0, δ) and x ∈ Σ∗ . We denote by A(x) the state δ(q0, x). Each FDFA F accepts a set of UP-words UP(F) by using the following acceptance condition.

Definition 3 (Acceptance). Let F = (M, {N q }) be an FDFA and w be a UP-word. A decomposition (u, v) of w is normalised with respect to F if M(u) = M(uv). A decomposition (u, v) is accepted by F if (u, v) is normalised and v ∈ L∗(N q ) where q = M(u). Then, w is accepted by F if there exists a decomposition (u, v) of w accepted by F.

So, we can also see UP(F) as the set of words recognised by F. In the remainder of the paper, we fix a target DBAlanguage L unless stated otherwise.

3 Outline of Our Algorithm

We give an overview of our DBA learning algorithm in this section; the framework is depicted in Fig. 1. Assume that we have a DBA oracle who knows L and can answer membership queries about L and equivalence queries about whether a given DBA recognises L. We note that using equivalence queries that involve NBA operations would significantly increase the complexity for resolving equivalence queries and lose all the advantage we aim to reap.

Our DBA learner is comprised of three components: the limit FDFA learner (cf. Sect. 5), the component transforming an FDFA F to a DBA B[FB] (cf. Sect. 4), and a counterexample (CEX) analysis component (cf. Sect. 6). Limit FDFAs are a type of canonical FDFAs that have special structures for DBA-languages [Li et al., 2023a]; they are a natural choice of canonical FDFAs for our DBA learning algorithm. In a nutshell, our DBA learner, corresponding to the red dashed box on the left in Fig. 1, tries to use the limit FDFA learner to learn the canonical form of limit FDFAs F (and thus the sink FDFA FB in Sect. 4) [Li et al., 2023a] and then converts the sink FDFA FB to a language-equivalent DBA B[FB].

The DBA learner needs to first construct a DBA B[FB] from F, where FB is obtained from F by only allowing sink final states. Then the DBA learner poses an equivalence query EQ DBA(B[FB]) to the DBA oracle. If the DBA oracle returns "Yes", the DBA learner can just output the learned DBA B[FB]: it has completed the learning task. Otherwise, the DBA learner receives "NO" along with a CEX uvω ∈ L ⊖ L(B[FB]). Then the DBA learner has to utilise the CEX analysis component to extract a CEX (u′ , v′ ), which may not be a decomposition of uvω but should be good for refining F. Observe that there is a dashed line labelled with F and B[FB] from the DBA construction component to the CEX analysis component; this means that we will need F and B[FB] in the CEX analysis. The above procedure will continue until a correct DBA has been learned.

More precisely, the DBA learner uses the FDFA learner to learn the limit FDFA F (and thus B[FB]) by answering membership and equivalence queries posed by the limit FDFA learner, through interacting with the DBA oracle. We will use superscripts, FDFA and DBA, to distinguish the equivalence queries posed by the limit FDFA learner and the DBA learner respectively. To answer a membership query MQ(u, v), the DBA learner simply forwards the answer to the membership query MQ(uvω ) obtained from the DBA oracle. Answering an equivalence query EQ FDFA(F) can be more involved.

The main challenge here is that the DBA B[FB] is only guaranteed to be language-equivalent with F if F is in the canonical form of limit FDFAs; before that, it will accept a sub-language, i.e. UP(L(B[FB])) ⊆ UP(F). This is because B[FB] is obtained by making all final states, except for the sink final states, non-final; so, some words of F may not be accepted by FB and thus not by B[FB]. However, a standard CEX for the limit FDFA learner to refine F needs to be in the symmetric difference between F and L, i.e. u · vω ∈ UP(F) ⊖ UP(L), but we only have uvω ∈ L ⊖ L(B[FB]). As a consequence, the CEX returned for B[FB] from equivalence queries cannot always be directly used to refine the current conjecture FDFA F.

While the first two cases are standard (as they are in the

We overcome this challenge by carefully categorising a CEX and then extracting a CEX for F from uvω ∈ L ⊖ L(B[F]) accordingly, possibly with the help of a few membership queries. Since the intermediate FDFA F is not perfect, the CEX uvω from EQ DBA(B[FB]) can fall into three categories, shown in Fig. 2: it can be (1) in the language of the conjecture DBA B[FB] (and thus of the FDFA F), but not in the target language L, (2) in the target language L, but not in the language of the FDFA F (and thus not in the language of B[FB]), and (3) in the target language L and the language of the FDFA F, but not in the language of B[FB].

symmetric difference between UP(F) and UP(L)), the third case poses an additional challenge in FDFA learning. Our key technical innovation here is an CEX analysis algorithm that deals with the third case.

We will describe each component of the DBA learner separately with more details in subsequent sections.

4 FromLimit/Sink FDFAs to DBAs

We present our DBA construction component in this section. We will first recall the definitions of limit FDFAs as canonical FDFAs for ω-regular languages and then introduce the sink FDFAs we use to construct DBAs.

By Definition 1, the Myhill-Nerode theorem associates each equivalence class of ∽R with a state of the minimal DFA D of the regular language R. The situation in ω-regular languages is, however, more involved. An immediate extension of such RCs for an ω-regular language L is the following.

Definition 4 (Leading RC). For two u1, u2 ∈ Σ∗ , u1 ∽L u2 if, and only if, ∀w ∈ Σω . u1w ∈ L ⇐⇒ u2w ∈ L holds.

We then define the limit FDFAs for ω-regular languages.

Definition 5 (Limit FDFAs [Li et al., 2023a]). The leading RC ∽ is as defined in Definition 4.

Let [u]∽ be an equivalence class of ∽. For x, y ∈ Σ∗ , we

Intuitively, a word v is accepted by N u L if, whenMmakes a round trip from state [u]∽ over v, we must have uvω ∈ L. In the setting of DBAs, this means that v is a word making the DBA of L visit some accepting transition from [u]∽-states; so, if the DBA closes a loop over v, then uvω must be accepted by the DBA and thus belong to L. The limit RC ≈u is then naturally defined over the language {v ∈ Σ∗ : u · v ∽ u ⇒ uvω ∈ L}, similar to the RC ∽R defined over a regular language R as given in Sect. 2.

define limit RC as: x ≈u y if, and only if, ∀v ∈ Σ∗ , (u·x·v ∽ u =⇒ u·(x·v)ω ∈ L) ⇐⇒ (u·y·v ∽ u =⇒ u·(y·v)ω ∈ L). The limit FDFA FL = (M, {N u L }) of L uses the leading DFA M = (T [∽], ∅) as defined in Definition 1; and, for each state [u]∽ ∈ Σ∗ /∽, the progress DFA N u L is the tuple (T [≈u ], Fu), where [v]≈u ∈ Fu if u · v ∽ u =⇒ uvω ∈ L.

Limit FDFAs are the class of canonical FDFAs that have been proved useful for defining the sink FDFAs we use for learning DBAs.

Definition 6 (Sink FDFAs [Li et al., 2023a]). The sink FDFA FB = (M, {N u B }) of L is defined so that the leading DFA M is as in Definition 5, and the TS of each N u B is, for each [u]∽ ∈ Σ∗ /∽, exactly as that of N u L fromDefinition 5.

The set of final states Fu contains the equivalence classes [x]≈u such that, for all v ∈ Σ∗ , u·xv ∽ u =⇒ u·(xv)ω ∈ L.

While the definition says 'classes', Fu either contains a single state, which is a final sink in N u L (and N u B ), or is empty (if N u L does not have such a final sink) [Li et al., 2023a]. A final state is said to be a sink if it has a self-loop over Σ.

DBA construction. Upon receiving an FDFA F from EQ FDFA(F), which may not be in canonical form, we first obtain an FDFA F ′B by allowing only final sinks as final states and construct a DBA below. To make the DBA construction more general, we assume an FDFA F ′B = (M, {N q }q∈Q) where M = (Q,Σ, ι, δ) and, for each q ∈ Q, we have N q = (Qq, Σ, ιq, δq, Fq) where Fq only contains final sinks.

Definition 7 ([Bohn and L¨oding, 2022]). Let F ′B = (M, {N q }q∈Q) be the FDFA defined above. Let T [F ′B ] be the TS constructed from F ′B defined as the tuple T [F ′B ] = (QT , Σ, ιT , δT ) and Γ ⊆ {(q, σ) : q ∈ QT , σ ∈ Σ} be a set of transitions where

• QT := Q× ⋃q∈Q Qq;
• ιT := (ι, ιι);
• For a state (m, q) ∈ QT and σ ∈ Σ, let q′ = δ˜m(q, σ) where N ˜m is the progress DFA that q belongs to and let m′ = δ(m, σ). Then

• ((m, q), σ) ∈ Γ if q′ ∈ F˜m

An example DBA constructed from an FDFA is provided in Fig. 3. The sink FDFA FB of L, as constructed in Definition 6, can be translated to its equivalent DBA.

Lemma 1 ([Li et al., 2023a]). If F ′B is an FDFA with only sink final states. Let B[F ′B ] = (T [F ′B ], Γ) as given in Definition 7. Then, UP(L(B[F ′B ])) ⊆ UP(F ′B ).

Recall that we learn DBAs by learning the limit FDFA FL. By Lemma 1, our DBA learner eventually learns the correct DBA when the conjecture FDFA converges to FL in the worst case. Usually, an earlier conjecture DBA may already be correct-our algorithm will output the correct DBA.

Let FB be the sink FDFA of a DBA language L, as defined in Definition 6. Let B[FB] be the DBA constructed by Definition 7 from FB. Then UP(FB) = UP(L) = UP(L(B[FB])).

5 The Limit FDFA Learner

With the canonical form of limit FDFAs (cf. Definition 5), we can now describe the limit FDFA learner. In [Li et al., 2023b, Appendix E], the authors gave a learning algorithm for limit FDFAs. We follow their description of the limit FDFA learner but allow a more relaxed form of counterexamples. For instance, they require the CEX (u, v) to be normalised with respect to the current leading DFAM, while our requirements in Definition 8 does not ask for it. The importance of our definition of counterexamples is that it allows to learn the canonical form of limit FDFAs, while theirs only learns an abstract form, which cannot be used to construct DBAs.

As usual, a learner uses an observation table [Angluin, 1987] defined as a tuple T B = (S, ˜ S,E, T), where S is a prefix-closed set of finite words, E is a set of experiments trying to distinguish the words in S, and T : S ×E → D stores the element (membership query results) in entry T(s, e) an element in some domain D, where s ∈ S and e ∈ E. For the limit FDFA, D is the set of Boolean values {⊤,⊥} for the leading DFA and a pair of Boolean values for progress DFAs (see Fig. 4). We determine when two words s1, s2 ∈ S are not equivalent depending on the RC we are using. The component ˜ S ⊆ S is the subset considered as representatives of the equivalence classes, i.e. the state names of the constructed DFA. Take T Bε in Fig. 4 for example: S = {ε, a, aa, aaa, aab, ab, b} (all row names), ˜ S = {ε, a, aa} (upper row names), and E = {ε, b} (all column names).

A table is closed if S is prefix-closed and, for every s ∈ ˜ S and σ ∈ Σ, we have sσ ∈ S. The procedure CloseTable uses two sub-procedures ENT (read: entry) and DFR (read: difference) to make a given table closed. Here ENT(s, e) is used to fill the table entry T (s, e) by means of asking membership queries. The procedure DFR is used to determine which rows (words) of the table should be distinguished.

A learning procedure usually begins by creating an initial observation table by asking membership queries, closing the table with ENT and DFR procedures, and then constructing a conjecture automaton for asking an equivalence query. The learner should be able to use the CEX to the equivalence query to find new experiments (columns) for discovering new equivalence classes.

We let MQ(x, y) be the result of the membership query to the UP-word x·yω to the oracle. The procedures ENT1, DFR1 and Aut1 are used for learning the leading DFA. More precisely, for u, x, y ∈ Σ∗ , ENT1(u, (x, y)) = MQ(u · x, y); for two finite row words u1, u2 ∈ S, DFR1(u1, u2) = ⊤ iff there exists (x, y) ∈ E such that T(u1, (x, y)) ̸= T(u2, (x, y)). That is, we can use x · yω to distinguish the finite words u1

and u2 according to ∽.

The procedure Aut1 is simply to construct the leading DFA without final states from T B, by Definition 1. Note that, when a leading DFA is updated, this affects the RC ≈u , which in turn affects some of the progress DFAs that then need to be reconstructed. This is why in Algorithm 1 we reconstruct progress DFAs N ˜u for all ˜u ∈ ˜ S once M is updated.

The procedure Autu(T Bu) not only constructs the TS but also sets a state x as final if Tu(x, ε) = ⊤. Note that here Tu(x, v) is regarded as the result of whether or not (u =Mu(xv) =⇒ MQ(u, xv)) holds.

Let Mu denote the DFA obtained fromM by setting the initial state to u. In the table, if u ∈ ˜ S, we have u = M(u) = Mu(ε). When learning progress DFAs, for u, x, v ∈ Σ∗ , we define ENTu2 (x, v) = (Mu(x · v) ?= u,MQ(u, x · v)). We can also regard ENTu2 (x, v) (and thus Tu(x, v)) as ⊤ (Boolean implication of the pairs) in testing equivalence ifMu(x·v) ̸= u or MQ(u, x · v) = ⊤ holds, corresponding to whether ux · v ∽ u =⇒ u · (xv)ω ∈ L holds in Definition 5; for two finite row words, x1, x2 ∈ Su, DFRu2 (x1, x2) returns ⊤ if there exists v ∈ E such that Tu(x1, v) ̸= Tu(x2, v). An example table T Bε is depicted in Fig. 4.

We have described above how to fill the observation tables and construct DFAs. Now we show that, as long as the CEX returned for the limit FDFA learner satisfies Definition 8, it is good to refine the current conjecture F. By analysing the CEX, we can add a new column e to the corresponding table in order to distinguish two rows x · a and x′ that are currently classified as equivalent, where x, x′ ∈ ˜ S, x · a ∈ S and DFR(x · a, x′ ) = ⊤ with DFR ∈ {DFRu1 , DFR2}.

In the remainder of the paper, we will regularly make use of the duality of the states in the DFAs and the words in the observation table they represent.

Definition 8. Let (u, v) be a CEX to the conjecture FDFA F = (M, {N x }). We say (u, v) is good for refinement (GfR) of F if it has the prefix or loop property described below.

Prefix. There exist two indices 0 ≤ i < j ≤ |u| such that MQ(xi · u[i . . .], v) ̸= MQ(xj · u[j . . .], v), where xi = M(u[0 · · · i]) and xj =M(u[0 · · · j]).

Loop. There exist two indices 0 ≤ i < j ≤ |v| such that ˜u = M˜u(yi · v[i . . .]) =⇒ MQ(˜u, yi · v[i . . .]) and ˜u = M˜u(yj · v[j . . .]) =⇒ MQ(˜u, yj · v[j . . .]) are not equal, where ˜u = M(u), yi = N ˜u (v[0 · · · i]) and yj = N ˜u (v[0 · · · j]).

The refinement procedure of the conjecture FDFA F = (M, {N x }) has been formalised as Algorithm 1. First, we assume that the CEX (u, v) is GfR. Let ˜u =M(u). If (u, v) is a prefix CEX, the leading DFAMwill be refined. Otherwise, if (u, v) is a loop CEX, the progress DFA N ˜u will be refined. We use the function FindDistinguishingExperiment to find an experiment (non-empty finite word) to be added to the column of an observation table, so to distinguish a word and its current representative state. The implementation details of FindDistinguishingExperiment are formalised as the refinement procedures for M and N ˜u described below.

Input: An FDFA F = (M, {N x }). Let (u, v) be GfR for F and let ˜u =M(u); if (u, v) is a prefix CEX then E = E ∪ FindDistinguishingExperiment(u, v); CloseTable(T B, ENT1, DFR1) and let M = Aut1(T B); forall ˜u ∈ ˜ S do CloseTable(T B˜u, ENT˜u2 , DFR˜u2 ) and let N ˜u = Aut 2(T B˜u); else if (u, v) is a loop CEX then E˜u = E˜u ∪ FindDistinguishingExperiment(˜u, v); CloseTable(T B˜u, ENT˜u2 , DFR˜u2 ) and let N ˜u = Aut 2(T B˜u);

Refinement of M. Since MQ(xi · u[i . . .], v) ̸= MQ(xj · u[j . . .], v), we have xi · u[i . . .] ̸∽ xj · u[j . . .]. We can find an experiment as follows. Let xk = M(u[0 · · · k]) be the state or word representative that M arrives at after reading the first k letters of u. In particular, xi = M(u[0 · · · i]) and xj = M(u[0 · · · j]). We construct the sequence by asking membership queries: MQ(x0 · u[0 . . .], v), · · · ,MQ(xi · u[i . . .], v), · · · ,MQ(xj · u[j . . .], v), · · · . Since MQ(xi · u[i . . .], v) ̸= MQ(xj · u[j . . .], v) by prefix assumption, this sequence has different results at the indices i and j.

Therefore, there must exist the smallest k ∈ [i, j) such that MQ(xk · u[k] · u[k + 1 . . .], v) ̸= MQ(xk+1 · u[k + 1 . . .], v), Hence, since xk+1 =Mxk (u[k]), we can use the experiment e = (u[k + 1 . . .], v) to distinguish xk · u[k] and xk+1.

Since (u, v) is a loop CEX, only one of mi =⇒ ci and mj =⇒ cj holds. There must be a smallest integer k ∈ [i, j) such that mk =⇒ ck and mk+1 =⇒ ck+1 differ. Assume mk =⇒ ck holds (the other case is entirely similar). Thus, mk+1 =⇒ ck+1 does not hold. Analogously, we can add the experiment e = v[k +1 . . .] to distinguish yk · v[k] and yk+1 since we have ˜u = M˜u(yk · v[k . . .]) =⇒ ˜u · (yk · v[k . . .])ω ∈ L holds but ˜u = M˜u(yk+1 · v[k + 1 . . .]) =⇒ ˜u · (yk+1 · v[k + 1 . . .])ω ∈ L does not hold.

Refinement of N ˜u . Let yk = N ˜u (v[0 · · · k]). Similarly, we have a sequence (m0, c0), · · · , (mi, ci), · · · , (mj, cj) where mk = ⊤ iff ˜u = M˜u(yk · v[k . . .]) and ck = ⊤ iff ˜u · (yk · v[k . . .])ω ∈ L (i.e. ck = MQ(˜u, yk · v[k . . .])).

It immediately follows that the limit FDFA learner is guaranteed to make progress once receiving a GfR CEX.

Lemma 2. A CEX (u, v) satisfying Definition 8 refines the current leading DFA or a progress DFA in Algorithm 1.

6 CEXAnalysis Component

Now we describe the CEX analysis component. By assumption, the input here is a UP-word w = uvω ∈ L(B[FB]) ⊖L, represented by its decomposition (u, v) (cf. Fig. 1).

Recall that we have the following three cases about w in Fig. 2: (1) w ∈ L(B[FB]) \ L and w ∈ UP(F) since UP(L(B[FB])) ⊆ UP(F), (2) w ∈ L \ L(B[FB]) and w /∈ UP(F), and (3) w ∈ L \ L(B[FB]) and w ∈ UP(F).

We first analyse Case (1) and Case (2), which are already in the symmetric difference between UP(F) and UP(L). This means that the CEX is easy and we only need to extract a normalised decomposition (u′ , v′ ) from w as below.

1. w ∈ L(B[FB]) \ L and w ∈ UP(L(B[FB])) ⊆ UP(F). Hence, w ∈ UP(F) but w /∈ L. There must be a normalised decomposition (u′ , v′ ) of w such that (u′ , v′ ) is accepted by F. However, w is not in L, so (u′ , v′ ) should actually have been rejected. We can just return (u′ , v′ ) as a CEX to further refine F. We now prove that (u′ , v′ ) satisfies Definition 8.

First, let x =M(u′ ). We ask MQ(x, v′ ) ?= MQ(u′ , v′ ). If their results are not equal, we let i = 0 and j = |u′ |. We can then verify that (u′ , v′ ) satisfies the prefix requirement. Otherwise their membership results agree. We let i = 0 and j = |v′ |. Hence, yi = v′ [0 · · · 0] = ε and yj = N x (v′ ). Since (u′ , v′ ) is accepted by F, we have x = Mx(yj ·ε) =⇒ MQ(x, yj ·ε) since yj is a final state in N x . However, x = M(u′ ) = Mx(yi · v′ ) because (u′ , v′ ) is normalised. Together with MQ(x, v′ ) = MQ(u′ , v′ ) = ⊥, x = Mx(yi) =⇒ MQ(x, yi ·v′ [0 . . . ]) does not hold. Hence, (u′ , v′ ) satisfies the loop requirement. Therefore, (u′ , v′ ) is GfR.

1. w ∈ L \ L(B[FB]) and w /∈ UP(F). Consequently, w /∈ UP(F) and w ∈ L. There must be a normalised decomposition (u′ , v′ ) of w such that (u′ , v′ ) is not accepted by F. However, w is in L, so (u′ , v′ ) should have been accepted. Similarly, we can return (u′ , v′ ) as a CEX to refine F. Again, one can similarly prove that (u′ , v′ ) is GfR as Case (1).

We only proved the existence of such counterexamples. We refer to [Li et al., 2021] for details about how to extract them.

Note that the first two cases do not make any specific reference to the difference between UP(F) and L(B[FB])- they are a variation of vanilla FDFA learning. The third case, however, is quite different: the CEX (u, v) is such that w = uvω ∈ L \ L(B[FB]) and w ∈ UP(F)-and not in the symmetric difference of UP(F) and UP(L) (cf. Fig. 2).

Let ρ = (m0, ι0)(m1, ι1) · · · be the run of B[FB] over w. By assumption, w is not accepted by B[FB]. So, the sequence of progress DFA states in the run ρ will eventually get stuck in a progress DFA according to Definition 7. Assume that ρ eventually gets stuck in the progress DFA N m, where m is a state of the leading DFA, and thus also a word representative of that equivalence class. Let ˆ ρ be the projection on the first element of each pair in ρ. We can see that ˆ ρ is the run of the leading DFA M over w.

To tackle the CEX analysis in this case, the structure of the DBA B[FB] plays a crucial role. This seems unavoidable, because we have w ∈ L and w ∈ UP(F), so that the quest for a normalised decomposition (u′ , v′ ) of w such that (u′ , v′ ) is not accepted by F, as we did in case (2), cannot work. This makes case (3) significantly more involved. We will analyse the CEX w by looking carefully at the run of B[FB] over w = uvω ∈ L \ L(B[FB]).

Since B[FB] has a finite number of states and w is a UPword, we can decompose w into three finite words x, v1 ∈

Algorithm 2: Counterexample generation for

Case (3c): m =Mm(v1 · y) and m · (v1 · y)ω /∈ L Input: m, x, v1, y ∈ Σ∗ and v2 ∈ Σ+ Output: A GfR counterexample if MQ(m · v1, v2) = ⊥ then return (x · v1, v2) as a prefix CEX; k := 0; while true do h := 1; while h ≤ k do if MQ(m · (v1 · vk 2 · y)h · v1, v2) = ⊥ then return (x · (v1 · vk 2 · y)h · v1, v2) as a prefix CEX; h := h + 1; if MQ(m, v1 · vk 2 · y) = ⊤ then return (x, v1 · vk 2 · y) as a loop CEX; k := k + 1;

Σ∗ , v2 ∈ Σ+ such that w = x · v1 · (v2)ω ,m =M(x),m′ = M(xv1) = M(xv1 · v2), N m(v1) = N m(v1 · v2), where m′ is a leading state that might be different to m. Let ˜ v1 = N m(v1). Hence, ˜ v1 = N m(v1 · v2) holds as well. We can depict the run ρ as follows:

Next, we find a word y ∈ Σ∗ from the observation table for N m such that m = Mm(˜ v1 · y) and m· (˜ v1 · y)ω /∈ L. To see that such a word exists we assume for contradiction that there is no such word, and thus no entry (⊤, ⊥) in the row of the observation table for ˜ v1. But then ˜ v1 is the sink final state, which contradicts that B[FB] got stuck in N m.

With this word y, we can extract the CEX (u′ , v′ ) by analysing the following three cases.

1. m ̸= Mm(v1 · y). By Definition 5, this entails that y can be used to distinguish ˜ v1 and v1 but currently ˜ v1 and v1 are classified as equivalent since ˜ v1 = N m(v1). We can thus choose the loop CEX (u′ , v′ ) = (x, v1 · y) to refine N m. One can verify that (x, v1 · y) is a valid GfR loop CEX by setting the indices i = 0 and j = |v1| in Definition 8. Note that since m = M(x), so we use (u′ , v′ ) to refine N m.
2. The remaining casem=Mm(v1 ·y) andm·(v1 ·y)ω /∈ L (tested by MQ(m, v1 · y)) is quite involved, so we dedicate the remainder of this section to it. The analysis method is provided as Algorithm 2.
3. m = Mm(v1 · y) and m · (v1 · y)ω ∈ L (tested by MQ(m, v1 · y)). We can again choose the loop CEX (u′ , v′ ) = (x, v1 · y) to refine N m since ˜ v1 and v1 can be distinguished with y. One can verify that (x, v1 · y) is a valid GfR loop CEX by again setting i = 0 and j = |v1| in Definition 8.

We now describe how Algorithm 2 extracts a GfR CEX for Case (3c). First, if m · v1 · v2 ω /∈ L, then v1 · v2ω (tested by MQ(m, v1 · y)) distinguishes x from m, so that we can return the prefix CEX (x · v1, v2). One can verify (x · v1, v2) by setting i = 0 and j = |x| in Definition 8.

Now we prove that Algorithm 2 terminates. Let us assume that our algorithm does not terminate. For this, we argue towards contradiction that L is recognised by a DBA D with transition function δ and d states. Once we have completed the outer loop for k = d+1, we then know that, for all h ≤ k, we have that m · (v1 · vk 2 · y)h · v1 · v2 ω ∈ L. (Otherwise the inner loop will eventually return a prefix CEX, which leads to a contradiction.) Let us denote xh = δ(ι, m·(v1 ·vk 2 ·y)h ·v1), then the run of Dxh on vk 2 contains an accepting transition.

We also observe that the prefix CEX and loop CEX we return in the loop/s are GfR counterexamples, as they establish that: (1) m ̸∼ x · (v1 · vk 2 · y)h although m = M(x · (v1 · vk 2 · y)h ) = Mm((v1 · vk 2 · y)h ) (because m′ =M(x · v1) =Mm(v1) =Mm(v1 · vk 2 ) by decomposition of ρ); and (2) ˜ v1 ̸≈m v1 · vk 2 although ˜ v1 = N m(v1) = N m(v1 · vk 2 ). To prove (1), we first observe that Algorithm 2 did not return before while loop, hence m · v1 · vω 2 ∈ L. Moreover, by return condition of inner loop, we have that m·(v1·vk 2 ·y)h ·v1·vω 2 /∈ L. It follows thatmandm·(v1·vk 2 ·y)h can be distinguished by v1 · vω 2 . To obtain a valid GfR prefix CEX, we return (x · (v1 · vk 2 · y)h · v1, v2). One can verify the CEX by setting i = |x| and j = |x · (v1 · vk 2 · y)h | in Definition 8. To prove (2), we first have m · (v1 · y)ω /∈ L and m = Mm(v1 · y) by assumption. By return condition of the outer loop, we have m · (v1 · vk 2 · y)ω ∈ L. Therefore, it follows that ˜ v1 and v1 ·vk 2 can be distinguished with y by Definition 5. Again, to obtain a valid GfR loop CEX, we return (x, v1 · vk 2 · y) since m =M(x). One can verify the returned CEX by setting i = 0 and j = |v1 · vk 2 | in Definition 8.

We now consider the run of D on m · (v1 · vk 2 · y)ω . We have established that it passes an accepting transition while traversing each of the first k 'v2 k ' sequences. Moreover, it cannot be on k different states (as there are only d = k - 1 different ones) after the first k iterations of the loop-part 'v1 · vk 2 · y', so that the run ends in an accepting loop. This entails m· (v1 · vk 2 ·y)ω ∈ L, and we would return a loop CEX, which provides a contradiction and completes the proof.

Therefore, Lemma 3 follows immediately.

Lemma 3. Algorithm 2 terminates and returns a valid GfR counterexample.

7 Concluding Remarks

By putting all three components together, we have completed the design of our DBA learner. Theorem 1 follows directly from Lemmas 1, 2 and 3.

Theorem 1. Our DBA learner depicted in Fig. 1 terminates and learns a correct DBA of L.

We note that the target of the learning algorithm in [Angluin and Fisman, 2016] is the canonical FDFA itself. While our algorithm in the worst case learns a canonical limit FDFA, it can (and does) in practice terminate well before converging to the canonical FDFAs, as long as the constructed DBA is correct. Furthermore, as mentioned in Sect. 1, we can easily obtain a DCA learner by learning the complement language of a co-B¨uchi target language.

To establish a complexity bound of our learning algorithm, we need to assume that a membership query and an equivalence query are both resolved in constant time by the oracle. As proved in [Angluin and Fisman, 2016; Li et al., 2021], the FDFA learners run in polynomial time in the size of a type of canonical FDFAs called periodic FDFAs, rather than the target FDFAs. Since our DBA learning algorithm is based on FDFA learners, our algorithm also runs in polynomial time with respect to the size of the periodic FDFAs, rather than in the size of the minimal DBAs.

Corollary 1. Our DBA learning algorithm runs in time polynomial in the size of the periodic FDFA of L.

Let n be the number of states in the periodic FDFA of L and m = |u| + |v| be the maximal length of the prefix and loop, respectively, of all returned counterexamples by the DBA oracle. A rough complexity analysis of our algorithm leads to the upper bound O(n32 · m · |Σ|).

We dive into the detailed complexity analysis below. The worst-case complexity of our algorithm could only occur when we have learned the canonical FDFA, which rarely happens in practice. According to [Li et al., 2021, Theorem 4], the number of equivalence queries needed for learning canonical FDFAs is O(n4 ). Furthermore, the intermediate conjecture FDFA in each iteration has O(n3 ) states [Li et al., 2021]. We analyse each component of the algorithm separately for a learning iteration. Assume that the current FDFA has r states and the minimal DBA of L has d states.

The FDFA learner uses membership queries to fill the entries of the observation tables and to refine the leading or a progress DFA with GfR CEXes. First, the total number of columns in all tables is bounded by the number of equivalence queries, i.e. O(n4 ), since a column is only added after an equivalence query. The total number of rows in all tables is bounded by the number of states and their outgoing transitions, i.e. r+r · |Σ|. So, the number of entries in the tables is O(n4 · (r + r · |Σ|)). Recall that r ∈ O(n3 ). It follows that the number of entries in the tables is O(n4 · (n3 +n3 · |Σ|)) ∈ O(n7 · |Σ|). Further, the number of membership queries used in the refinement procedure of the leading and progress DFAs is linear in the length of the input GfR CEX, which is bounded by O(n10 ·d3 ·m), as explained later. Therefore, the complexity of the FDFA learner for each iteration is O(n10 ·d3 ·m·|Σ|).

Now we consider the CEX analysis component. Algorithm 2 dominates the complexity of the CEX analysis component, as other cases are easier. In Algorithm 2, the number of iterations in the outer while loop is O(k2 ). Since we already proved before that k ≤ d, the number of membership queries used here is O(d2 ). In the worst case, to obtain the decomposed words x, v1 and v2, we find a decomposition in the product of the automaton recognising the CEX uvω and the conjecture DBA B[FB]. It follows that |x| + |v1| + |v2| ∈ O(m · n6 ), as the product has O(m · n6 ) states and |u| + |v| ≤ m by assumption. Note that y comes from the progress tables that adds loop suffixes of the CEX (x, v1 · vk 2 · y). Hence, in the worst case, |y| in-

Recall that the DBA construction produces a DBA with O(r2 ) states. Then, the complexity of the DBA construction for each iteration is O(n6 ).

creases by |v1 · vk 2 | after each equivalence query. Hence, |y| ∈ O(n4 ) · k · (m · n6 ) ∈ O(n10 · m · d). In the worst case, Algorithm 2 returns (x · (v1 · vk 2 · y)h · v1, v2) as a prefix CEX. Recall that h ≤ k ≤ d. The length of this CEX is |x| + h · |v1| + k · h · |v2| + h · |y| + |v1| + |v2| ∈ O(2 · m · n6 + n10 · m · d) · k · h ∈ O(m · n10 · d3 ). So, we return a CEX with length of O(n10 · d3 ·m) to the limit FDFA learner and ask O(d2 ) membership queries. Hence, the complexity of the CEX analysis component for each iteration is O(n10 · d3 · m).

Observe that the operations in the FDFA learner component contributes most to the complexity in each iteration. Therefore, the complexity of the whole algorithm is in O(n14 · d3 · m · |Σ|) since the number of learning iterations is O(n4 ). Additionally, since the minimal DBA is not larger than the constructed DBA, we also have d ∈ O(n6 ). So, the complexity is O(n32 · m · |Σ|), if we do not depend on the size of the minimal DBA of L.

We note that, in theory, the canonical limit FDFA that represents a DBA language L could be exponentially larger than the minimal DBA of L. Such languages are easy to construct, and the standard example given in [Bohn and L¨oding, 2022] is the language that contains all letters of an alphabet of size n infinitely often, Ln = (Σ∗ · a1 · Σ∗ · a2 · · · Σ∗ · an)ω . The canonical periodic/limit FDFA has a leading DFA with one state and a progress DFA with 2n states, as it needs to immediately recognise when all letters have been seen. When learning, this is an upper bound on the size of the FDFA one has to learn, but we did not (in spite of trying hard) manage to feed the learner with inputs that would make it create a progress FDFA with more than 2 · n states. This is because many FDFAs recognise the language Ln, and the constructed DBA will be correct once the progress DFA has a run from the initial state that visits all letters, without requiring to accept all permutations of {a1, · · · , an}. In practice, we do not need the precise limit FDFA in order to obtain the correct DBA.

Our DBA learning algorithm has been implemented in the tool ROLL [Li et al., 2019], which is publicly available at https://github.com/iscas-tis/roll-library.

When integrating learning algorithms into applications like verification, we also need to consider the cost of resolving equivalence queries in the oracle. (Membership queries are normally cheap.) This is a key strength of our algorithm, because the operations involving DBAs are easy. In fact, the perhaps biggest advantage we reap with our DBA learner over other learning algorithms for ω-automata is that we not only obtain easy resolution of equivalence queries, but also maintain reasonable expressiveness for the learned languages. Our contribution will further advance the frontier of the applications of learning algorithms in various fields, including verification, testing, and modelling, as well as further applications mentioned in the introduction.

Acknowledgements

We thank the anonymous reviewers for their valuable feedback. This work has been supported in part by the NSFC grant 62102407 and the EPSRC through grants EP/X021513/1 and EP/X017796/1.