# Minimal History-Deterministic Co-Buchi Automata: Congruences and Passive Learning

Christof Löding, Igor Walukiewicz

<figure><img src="image_1.png" /></figure>

## To cite this version:

Christof Löding, Igor Walukiewicz. Minimal History-Deterministic Co-Buchi Automata: Congruences and Passive Learning. Logic in Computer Science, 2025, Singapore, Singapore. pp.431–443, 10.1109/LICS65433.2025.00039. hal-05399220

HAL Id: hal-05399220

https://hal.science/hal-05399220v1

Submitted on 4 Dec 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Minimal History-Deterministic Co-Büchi Automata: Congruences and Passive Learning

Christof Löding

RWTH Aachen University

Aachen, Germany

ORCID: 0000-0002-1529-2806

Igor Walukiewicz

CNRS, Bordeaux University

Talence, France

ORCID: 0000-0001-8952-7201

*Abstract*—Abu Radi and Kupferman (2019) demonstrated the efficient minimization of history-deterministic (transition-based) co-Büchi automata, building on the results of Kuperberg and Skrzypczak (2015). We give a congruence-based description of these minimal automata, and a self-contained proof of its correctness. We use this description based on congruences to create a passive learning algorithm that can learn minimal history-deterministic co-Büchi automata from a set of labeled example words. The algorithm runs in polynomial time on a given set of examples, and there is a characteristic set of examples of polynomial size for each minimal history-deterministic co-Büchi automaton.

*Index Terms*—history-deterministic automata, co-Büchi automata, minimization, congruences, passive learning

## I. INTRODUCTION

Automata on infinite words, called $\omega$-automata, have been studied since the early 1960s as a tool for solving decision problems in logic [9] (see also [29]). Algorithms in formal verification of systems use various types of automata; for example, nondeterministic $\omega$-automata are used in model-checking procedures [3] while deterministic $\omega$-automata find applications in the verification of probabilistic systems [3] or in the synthesis of reactive systems from specifications (see [20], [30] for a survey and some more recent work). Despite this considerable interest, we still do not know how to canonize $\omega$-automata or how to learn them.

Deterministic $\omega$-automata are not a particularly promising model for canonization or learning. For deterministic $\omega$-automata, no small canonical forms are known, and minimization is computationally hard for many classes of deterministic $\omega$-automata [10], [27]. The only exception are so-called deterministic weak Büchi automata (DWBA), for which canonical minimal automata exist, and minimization is possible efficiently [18], [28].

History-deterministic automata over $\omega$-words are non-deterministic automata where the non-determinism can be resolved by a strategy depending only on the prefix of the $\omega$-word read so far. This makes them suitable for use in game-based synthesis procedures [14], [11]; see also [8] for a recent survey. The class of co-Büchi history-deterministic automata is particularly attractive because:

* co-Büchi history-deterministic automata can be exponentially smaller than deterministic co-Büchi automata for the same language [17],

* there exist canonical, minimal history-deterministic co-Büchi automata, and minimization can be done in deterministic polynomial time [26].

This is remarkable because co-Büchi languages are a standard class of $\omega$-languages that appear in many contexts. They capture the persistence properties in the temporal hierarchy of [23], and every regular $\omega$-language can be written as a finite Boolean combination of co-Büchi languages [29].

The existence of such canonical automata naturally raises the question of better understanding their structure. For instance, we can aim to describe them using congruences, similarly to the well-known description of minimal deterministic finite automata using the right congruence (see standard textbooks on automata theory like [15]). We can then evaluate whether this new description offers any advantages. A quite obvious choice is to apply it to the passive learning problem, which heavily relies on congruences and remains largely unsolved for $\omega$-automata. Our contributions follow this plan.

**Contribution 1** We give a congruence-based description of minimal history-deterministic co-Büchi automata using a congruence relation on pairs of finite words (it is a congruence with respect to right concatenation of letters in the second component of the pairs).

Until now, we have had only an algorithmic description of the minimal history-deterministic co-Büchi automata. The method involves taking a history-deterministic automaton and applying a minimization algorithm [26]. This algorithm consists of a series of transformations, the most complex being safe determinization from [17]. This step requires solving a game on two copies of the automaton, the winning region of the game determining which states and transitions should be retained. Although this algorithmic approach provides polynomial-time minimization, it does not offer a straightforward description of the minimal automaton. This is the essence of our first contribution.

Our second contribution uses the congruence-based description to develop a passive learning algorithm for history-deterministic co-Büchi automata. This is the first efficient learning algorithm for a class of $\omega$-automata that does not become trivial when restricted to prefix-independent languages. Finite regular languages are determined by their right congruence. This is not the case for $\omega$-languages; in particular, prefix-
independent languages have only one right congruence class. We believe that developing an efficient learning algorithm for co-Büchi languages shows that we have gained a better understanding of the class and have made measurable progress in learning theory.

**Contribution 2** We develop a passive learning algorithm for history-deterministic co-Büchi automata that is polynomial in time and data (as explained below).

Passive learning is the task of constructing an automaton from a given set of labeled examples, where the label indicates whether the example word belongs to the language or not. Optimally, the algorithm solving the passive learning problem should be efficient in both time and data. Time efficiency means that the algorithm should be able to produce an automaton in polynomial time with respect to the size of the sample. Being efficient in data refers to the concept of learning every automaton in the limit. For every language $L$, there should be a characteristic sample such that the learner produces an automaton for $L$ with this characteristic sample as input, and it produces the same automaton for every extension of the characteristic sample that is consistent with $L$. Being polynomial in data means that for every language in the class, there should be a characteristic sample of size polynomial in the size of the minimal automaton for the language.

This problem has been studied for DFAs since the 1970s (see [4], [13], [31]). The first passive learning algorithm polynomial in time and in data was proposed in [13]. Since then, many variations of the basic algorithms have been developed (see [19] for a survey) and were implemented in recent years, e.g., in the library flexfringe [32].

For $\omega$-automata the progress has been much slower. There is a polynomial active learning algorithm for learning deterministic weak Büchi automata (DWBA) [21], which allows to construct a passive learner that is polynomial in time and data for DWBA. The minimal automata for this class have a simple congruence-based description analogous to DFAs [28]. There are some passive learning algorithms for $\omega$-automata [2], [5]–[7], but the language classes that can be learned from polynomial data by these learners are defined by semantic restrictions of the standard right-congruence of the underlying language and become trivial when restricted to prefix-independent languages (see also related work in Section I-A).

The primary difficulty in developing learning algorithms for $\omega$-automata lies in the absence of a canonical form and a manageable description of such a form, preferably based on congruences. Given our first contribution, one could expect that it would be quite easy to get a passive learning algorithm for history-deterministic co-Büchi automata just by following the same recipe as for the DFA case. However, we encounter important challenges because the congruence-based description of the minimal automaton does not use all equivalence classes, but only those we call pointed. So, unlike in the case of finite words, the learning algorithm cannot just enumerate all equivalence classes and then pick the pointed ones, because the overall number of classes might

be exponential in the number of pointed classes. And not only can the number of classes be exponential, but there can also be equivalence classes containing only representatives of exponential size in the size of the minimal automaton. Fortunately, for pointed classes, there are always polynomial-sized representatives. These observations indicate why the progress in learning algorithms for $\omega$-automata has been so slow. The part of the algorithm finding the pointed equivalence classes is the most complex part of our algorithm.

The paper is structured as follows. We finish the introduction with a discussion of related work. In Section II we introduce basic terminology and basic results. In Section III we give the congruence-based automaton description and prove its correctness. In Section IV we present the learning algorithm in two steps. First, we consider an idealized algorithm allowing us to point out difficulties outlined above and to describe how we solve them. The final algorithm is a refinement of every step of the idealized algorithm. In Section V we conclude. All the missing proofs are given in the appendix.

## A. Related Work

Clearly, the starting point of our work are results and insights from [26], where the existence of canonical minimal history-deterministic co-Büchi automata is shown, which itself builds on [17]. But our proofs do not rely on any of these prior results and thus provide a new and independent view on history-deterministic co-Büchi automata.

The congruences we use appear in related forms, either implicitly or explicitly, in the literature. We use the standard right congruence $\sim_L$ of a language, which is a standard tool in the theory of automata on finite and infinite words. The relation $\approx_L$ introduced in Section IV is a relation on pairs of words. It is a different representation of the syntactic family of right-congruences of a language introduced in [22]. The relation $\equiv_L$ that is introduced in Section III and which is the basis for the automaton definition is new in its exact definition, but it is closely related to a family of automata used in [6], where a passive learner for deterministic Büchi automata is developed. This family of automata, one for each $\sim_L$ class, induces an equivalence on pairs that corresponds to our relation $\equiv_L$ with an additional condition of $\sim_L$-equivalence on the first component of pairs. Omitting this additional condition, is crucial for minimality. The notion of pointed pairs and the selection of the corresponding equivalence classes is, to the best of our knowledge, new.

Concerning previous results on passive learning for $\omega$-automata, there is a polynomial time active learner for DWBAs [21], which induces a passive learner that is polynomial in time and data (see [5, Proposition 13]). The paper [2] gives an adaptation of Gold's passive learner for DFAs to $\omega$-automata. For this to work, the automaton class has to be restricted to automata that have only one state per $\sim_L$-class (referred to as IRC languages for informative right congruence). Then the transition system can be inferred as for DFAs, and it only remains to deal with the acceptance condition. The class of DWBA languages is contained in the IRC class [28]. The well-
known RPNI algorithm [25] that infers a DFA from examples by a state merging technique has been adapted to deterministic ω -automata in [5]. The algorithm requires only polynomial data for the IRC languages considered in [2], and it can also infer automata for some languages beyond this class, but there is no further characterization of the class of inferrable languages. The main lesson to learn from [2], [5] is that we know how to deal with acceptance conditions in learning algorithms when the transition system is easy to infer. There is some work beyond IRC languages, presenting polynomial- time passive learners for deterministic Büchi automata [6] and deterministic parity automata [7]. However, for obtaining classes that can be learned from polynomial data, again a restriction on the right-congruence is required: the number of states for each ~<sub>L</sub>-class needs to be at most *k* for some fixed *k*. Restricted to prefix-independent languages (a single ~<sub>L</sub>-class), this gives only finitely many languages for fixed *k*. Therefore, none of the aforementioned learners is capable of learning a nontrivial class of prefix-independent languages from polynomial data.

Finally, there is a polynomial-time active learner for the class of deterministic parity automata [24]. But this algorithm uses, in addition to membership and equivalence queries, so- called loop-index queries, which provide some information on the structure of the target automaton and not just on the target language.

II. PRELIMINARIES

An alphabet Σ is a non-empty, finite set of letters. We use
standard notation, Σ* for the set of finite words, Σω for the
set of infinite words. We write $\underline{\sqsubseteq}$ for the prefix relation on
words. In our learning algorithm we use *length-lexicographic*
*order* on finite words, that is we first compare the lengths
of words, and then compare them lexicographically, assuming
some fixed order on the alphabet. Whenever we say that a
word *v* is *smaller* than *w*, we refer to *length-lexicographic*
*order*.

A co-Büchi automaton is a tuple $\mathcal{A} = (Q, Q_{init}, \Sigma, \Delta \subseteq Q \times \Sigma \times \{1, 2\} \times Q)$ where $Q$ is a finite set of states, $Q_{init}$ a set of initial states, and $\Delta$ is a transition relation, each transition having a rank 1 or 2 (we say 1-transition or 2-transition). Without loss of generality we can assume that from every state there is an outgoing transition on every letter. A run of $\mathcal{A}$ from a state $q_0$ on an infinite word $a_0 a_1 \dots \in \Sigma^\omega$ is a sequence of transitions $q_0 \xrightarrow{a_0:t_0} q_1 \xrightarrow{a_1:t_1} q_2 \xrightarrow{a_2:t_2} \dots$ with $a_j \in \Sigma$ and $i_j \in \{1, 2\}$. It is accepting if $q_0 \in Q_{init}$, and there are only finitely many 1-transitions on the run; in other words we work with the min-parity condition. We write $L(\mathcal{A}, q)$ for the set of words accepted from $q$. We write $L(q)$ when $\mathcal{A}$ is clear from the context.

An automaton $\mathcal{A}$ is *history-deterministic* if Eve can resolve
nondeterminism in $\mathcal{A}$ while reading the input. More precisely,
Eve should have a winning *strategy* in the following game.
Eve starts by putting a token at some initial state. Then the
game proceeds in rounds: Adam chooses a letter, and Eve
moves the token along a transition of her choice (with the input

letter chosen by Adam). Eve wins if the run she constructs is
accepting or the infinite sequence chosen by Adam is not in
$L(\mathcal{A})$.

We will use arrow notation to denote runs on finite words.
For a finite word $w \in \Sigma^*$ we write $q \xrightarrow{w:2} q'$ when there
is a run of the automaton from $q$ to $q'$ on $w$ using only 2-
transitions; since the automaton is nondeterministic, there can
be more than one run. We write $q \xrightarrow{w:1} q'$ if there is a run from
$q$ to $q'$ on $w$ but not $q \xrightarrow{w:2} q'$. Sometimes we omit the state
$q'$ in the notation, with $q \xrightarrow{w:2} \text{ meaning that there is } q'$ \text{ with}
$q \xrightarrow{w:2} q'$, and $q \xrightarrow{w:1} \text{ meaning that there is } q'$ \text{ with}
$q \xrightarrow{w:1} q'$, and there is no } q'' \text{ with } q \xrightarrow{w:2} q''$. Note that } q \xrightarrow{w:1} \text{ implies that}
\text{ all runs from } q \text{ on } w \text{ have minimal rank 1. Finally, we simply}
\text{ write } q \xrightarrow{w} q' \text{ to say that there is a run without specifying the}
\text{ ranks on it. Most often } \mathcal{A} \text{ will be clear from the context, so}
\text{ we do not specify it in our notation.}
$$

This notation can be used to define an important concept of
a *safe language* of a state: $L^{\text{sf}}(\mathcal{A}, q) = \{w \in \Sigma^* : q \xrightarrow{w:2} w\}$.
Note that the safe language of a state is a set of finite words,
whereas $L(\mathcal{A}, q)$ is a set of infinite words. We write $L^{\text{sf}}(q)$
when $\mathcal{A}$ is clear from the context.

Finally, we introduce a few standard notions for history-
deterministic co-Büchi automata. A co-Büchi automaton $\mathcal{A}$ is

* normalized if for each 2-transition $q \xrightarrow{a:2} q'$ there is $x \in \Sigma^*$ such that $q' \xrightarrow{x:2} q$, so if restricted to 2-transitions the graph of the automaton consists of separated strongly connected components, called the *safe SCCs* of $\mathcal{A}$.

* semantically-deterministic if $p \xrightarrow{a} q$ implies $L(q) = a^{-1}L(p)$; clearly a history-deterministic automaton can take only such transitions.

* **unsafe-saturated** if for every *p*, letter *a* and state *q* such that $L(q) = a^{-1}L(p)$ we have $p \xrightarrow{a:1} q$; in the case of co-Büchi automata, adding such 1-transitions does not change the accepted language.

* *safe-deterministic* if for every state *p* and letter *a* there is at most one 2-transition on *a* from *p*, so the only non-determinism left is in choice of 1-transitions; this can happen only finitely many times in an accepting run.

For all the above properties but safe-determinism it is easy
to prove that they can be ensured on a history-deterministic
automaton $\mathcal{A}$ without increasing the number of its states [17].

**Lemma 1.** Every history-deterministic co-Büchi automaton can be made normalized, semantically-deterministic, and unsafe-saturated without changing the language, by respectively modifying the rank of some transitions, removing some states, and adding some 1-transitions.

Once an automaton is unsafe-saturated the whole complex-
ity of a co-Büchi automaton is hidden in understanding the
structure of safe SCCs. This indicates why safe-determinism
is such a central property as it ensures that inside a safe
SCC the automaton is deterministic. Making an automaton
safe-deterministic is slightly more involved. The only way we
know how to do this is to use a game-theoretic approach of Kuperberg and Skrzypczak [17]. We do not use this result in our approach. Assuming safe-determinism, the following result shows how the notions introduced above can be used together.

**Lemma 2.** Every semantically-deterministic, unsafe-saturated, and safe-deterministic co-Büchi automaton is history-deterministic.

*Proof.* Let $\mathcal{A}$ be such an automaton. We define a strategy to accept $L(\mathcal{A})$. The argument is a generalization of the argument in the proof of [17, Lemma 3], where a similar construction of a strategy is given for a specific language. For this we use some arbitrary linear ordering $p \le q$ on the states of $\mathcal{A}$.

We define a *support* of a sequence $u \in \Sigma^*$ to be a pair $(x, p')$ where $x$ is a prefix of $u$ and $p'$ is a state such that for some initial state $p$ there is a run $p \xrightarrow{x} p' \xrightarrow{z:2} z$ where $xz = u$. A *base* $(x_u, p_u)$ of $u$ is a support of $u$ with $x_u$ the shortest possible, and $p_u$ the $\le$-smallest once $x_u$ is fixed. Finally, the *top state* $q_u$ of $u$ is the state reached by the run $p \xrightarrow{x_u} p_u \xrightarrow{z_u:2} q_u$, where $x_u z_u = u$. State $q_u$ is determined by the base thanks to safe-determinism.

The strategy for the automaton is to be in the top state of $u$ after reading $u$. Let us look why this strategy is feasible. Suppose that we read a letter $a$ after $u$. If there is a 2-transition $q_u \xrightarrow{a:2} q'$, then the base does not change so $q' = q_{ua}$ is the top state of $ua$. If there is no rank 2-transition on $a$, then the base changes to some $(x_{ua}, p_{ua})$. By semantic-determinism for the top state $q_{ua}$ of $ua$ we get $L(q_{ua}) = (ua)^{-1}L$. Since $L(q_u) = u^{-1}L$ we have $L(q_{ua}) = a^{-1}L(q_u)$, so there is a transition $q_u \xrightarrow{a:1} q_{ua}$ as desired, because $\mathcal{A}$ is unsafe-saturated.

We show that this strategy guarantees accepting every word from $L(\mathcal{A})$. Take a word $w \in L(\mathcal{A})$. Since $\mathcal{A}$ is co-Büchi there is a prefix $u$ of $w$ such that the accepting run sees only 2-transitions after reading $u$. Let $v \in \Sigma^*$, $a \in \Sigma$ such that $uva$ is a prefix of $w$. Then $x_{uv} \sqsubseteq x_{uva} \sqsubseteq u$, and either $x_{uv} \neq x_{uva}$, or $q_{uv} \le q_{uva}$. This means that the base can change only finitely often, and in consequence, for all sufficiently long prefixes of $w$ the base is the same. As we have seen in the previous paragraph, the run following our strategy passes through a 1-transition only if the base changes. Hence, the run on $w$ following the strategy from the previous paragraph is accepting. $\square$

### III. CANONICAL AUTOMATON

The objective of this section is to give a direct construction of a minimal history-deterministic co-Büchi automaton for a given co-Büchi language $L$. This minimal automaton is defined from equivalence classes of some congruence relation determined by $L$ (cf. Definition 6).

For the whole section, fix a co-Büchi language $L \subseteq \Sigma^\omega$. For $u, v \in \Sigma^*$ we write $u \sim_L v$ for the standard right congruence:

$$u \sim_L v \quad \text{if for all } w \in \Sigma^\omega: uw \in L \text{ iff } vw \in L.$$

We work with pairs $(u, v)$ and for such a pair we are interested in all ultimately periodic words of the form $u(vx)^\omega$

such that $u \sim_L uvx$. Since there are only finitely many $\sim_L$-classes, each ultimately periodic word can be written in such a way that its periodic part loops on the class reached by the prefix. The restriction to such decompositions of ultimately periodic words is also used in the theory of families of right congruences [22] and families of DFAs [16].

The aim is to define an equivalence relation on pairs of words such that (a subset of) the classes of this equivalence relation can be used as states for a history-deterministic co-Büchi automaton for $L$. The transitions of the automaton that we define, extend the second component of the pair (on an $a$-transition, $a$ is appended to the second component). However, if appending the $a$ leads to a pair $(u, va)$ such that $u(vax)^\omega \notin L$ for all $x$ with $uvax \sim_L u$, then the automaton has to take a 1-transition. We capture this by defining for every $(u, v) \in \Sigma^* \times \Sigma^*$:

$$(u, v) \approx_L \perp \text{ if } v \neq \varepsilon \quad \text{and} \\ u(vx)^\omega \notin L \text{ for all } x \text{ with } uvx \sim_L u.$$

So we are interested in pairs $(u, v)$ such that $(u, v) \not\approx_L \perp$, and we have a 2-transition on $a$ from $(u, v)$ to $(u, va)$, unless $(u, va) \approx_L \perp$. Of course, we cannot take all $(u, v)$ as states, but rather need to define some equivalence relation of a finite index on these pairs. As we will see shortly, we cannot even take all the equivalence classes of the relation we define.

Each pair $(u, v) \in \Sigma^* \times \Sigma^*$ naturally defines the set of all extensions of the second component that do not lead to $\perp$:

$$sf_L(u, v) := \{x \in \Sigma^* : (u, vx) \not\approx_L \perp\}$$

Intuitively, this corresponds to the concept of a safe language $L^{sf}$ (cf. Proposition 8). The equivalence relation $\equiv_L$ merges $\sim_L$-equivalent pairs with same safe language:

$$(u, v) \equiv_L (u', v') \text{ if } uv \sim_L u'v' \text{ and } sf_L(u, v) = sf_L(u', v')$$

We write $[u, v]_{\equiv_L}$ for the $\equiv_L$ equivalence class of $(u, v)$.

**Example 1.** Consider the alphabet $\Sigma_k := \{a_1, \dots, a_k\}$ and the language of all $\omega$-words that do not contain all letters infinitely often. Then $\sim_L$ is trivial (all words are $\sim_L$-equivalent), and $(u, v) \approx_L \perp$ iff $v$ contains all letters. The language $sf_L(u, v)$ consists of all $x$ such that $vx$ does not contain all letters, and $(u, v) \equiv_L (u', v')$ if the same letters occur in $v$ and $v'$. The number of classes of $\equiv_L$ is thus $2^k$. The canonical history-deterministic co-Büchi automaton for $L$ has $k$ states, one for each $a_i$, that has loops with 2-transitions on all $a_j$ with $j \neq i$, and all possible 1-transitions.

The above example shows that, in general, $\equiv_L$ has too many equivalence classes to construct the minimal automaton from them. For our automaton construction, we use only $\equiv_L$-classes of pairs that we call *pointed*. Intuitively, $(u, v)$ is pointed if no pair that is $\sim_L$-similar to $(u, v)$ and whose looping part ends with $v$ has a smaller safe language than $(u, v)$.

**Definition 3.** We say that $(u, v)$ is *pointed* if $(u, v) \not\approx_L \perp$, and

$$\forall u_1, u_2 \in \Sigma^*. (u_1 u_2 \sim_L u \wedge (u_1, u_2 v) \not\approx_L \perp) \Rightarrow \\ sf_L(u, v) = sf_L(u_1, u_2 v).$$
<figure><img src="image_3.png" /><figcaption>Fig. 1: Relations ~L and ≡_L for the language of all words over {a, b, c} that start with a and have finitely many c or a finite and odd number of b, see Examples 3, 5.</figcaption></figure>

Note that $u_1u_2 \sim_L u$ and $sf_L(u,v) = sf_L(u_1, u_2v)$ imply $(u,v) \equiv_L (u_1, u_2v)$. We call a class of $\equiv_L$ pointed if it contains a pointed pair.

While the notion *pointed* is a central definition of the paper, it is not easy to motivate it at this stage. We try to give some intuition in the following example, and give some motivations later when we show technical properties of pointed elements and classes.

**Example 2.** Continuing Example 1, the *pointed* pairs are those of the form $(u, v)$ where $v$ contains all but one of the letters. Indeed, if $v$ does not contain $a_i$ and $a_j$ for $i \neq j$, then let $v_i$ be such that $v_iv$ contains all letters except $a_j$. Then $(u, v_iv) \not\leq_L \perp$ and $a_j \in sf_L(u, v)$ while $a_j \notin sf_L(u, v_iv)$ because $(u, v_iva_j) \approx_L \perp$. So out of the $2^k$ classes there are only $k$ classes that contain *pointed* elements. The rough intuition is as follows. There can be several reasons for a word to be in a language $L$: in the example, each $a_i$ not appearing infinitely often is such a reason. A history-deterministic automaton needs a component for each individual reason to check whether it is satisfied. The classes of $\equiv_L$ roughly correspond to subsets of reasons, and the classes of *pointed* pairs correspond to exactly one reason.

Here is a more complicated example when $\sim_L$ is not trivial.

**Example 3.** Figure 1 shows the relations $\sim_L$ and $\equiv_L$ for the language $L$ over the alphabet $\{a, b, c\}$ that contains all words that start with $a$ and that have finite number of $c$'s or a finite and odd number of $b$'s. The right congruence $\sim_L$ of $L$ has four classes: the initial class contains only $\varepsilon$, the class of $b$ contains all non-empty words that do not start with $a$, the classes of $a$ and $ab$ contain words starting with $a$: the first those with an even number of $b$'s and the second with an odd number of $b$'s. For $\equiv_L$, the 6 classes $\not\leq_L \perp$ are shown. The color indicates the $\sim_L$-class of the respective $\equiv_L$-class, namely, the $\sim_L$-class of the concatenation of the two words of the pair. The transitions in the diagram correspond to prolonging the second element of the pair with the letter on the transition. For example, we have a transition $(a, b) \xrightarrow{b:2} (a, bb) \equiv_L (a, \varepsilon)$. The classes containing *pointed* pairs have a solid frame (in this example, each class consists only of non-pointed pairs or only of *pointed* pairs, but in general this needs not to be the case). The only class that does not contain a *pointed* pair is the class of $(ab, \varepsilon)$,

which contains all pairs of the form $(ab, a^n)$ for $n \ge 0$. Since $b \in sf_L(ab, a^n)$ but $b \notin sf_L(ab, ca^n)$, we get that $(ab, a^n)$ is not pointed because $abc \sim_L ab$.

The next lemmas ensure that we can define the 2-transitions on the level of classes of *pointed* pairs.

**Lemma 4.** If $(u, v) \equiv_L (u', v')$ then for every letter $a$ we have $(u, va) \equiv_L (u', v'a)$.

*Proof.* Clearly $uva \sim_L u'v'a$, as $uv \sim_L u'v'$. Take some $x \in sf_L(u, va)$. Then $ax \in sf_L(u, v)$, and hence $ax \in sf_L(u', v')$ because $(u, v) \equiv_L (u', v')$. So $x \in sf_L(u', v'a)$. The symmetric argument yields $sf_L(u, va) = sf_L(u', v'a)$. $\square$

**Lemma 5.** If $(u, v)$ is *pointed* then for every letter $a$, either $(u, va) \approx_L \perp$ or $(u, va)$ is *pointed*.

*Proof.* Suppose $(u, va) \not\leq_L \perp$, we show that $(u, va)$ is *pointed*. Take $u_1, u_2$ such that $u_1u_2 \sim_L u$ and $(u_1, u_2va) \not\leq_L \perp$. We need to show that $sf_L(u, va) = sf_L(u_1, u_2va)$. Since $(u_1, u_2v) \not\leq_L \perp$, from $(u, v)$ being *pointed* it follows that $sf_L(u, v) = sf_L(u_1, u_2v)$. Hence, $sf_L(u, va) = sf_L(u_1, u_2va)$ from the definition of $sf_L$. $\square$

We are ready to define a canonical automaton for $L$.

**Definition 6.** The canonical automaton $A_{\equiv_L}$ is defined by:

* $Q^L = \{[u, v]_{\equiv_L} : (u, v)$ is *pointed*\},

* $Q_{init}^L = \{[u, v]_{\equiv_L} : (u, v)$ *pointed* $uv \sim_L \varepsilon\},

* $[u, v]_{\equiv_L} \xrightarrow{a:2} [u, va]_{\equiv_L}$ if $(u, va) \not\leq_L \perp,$

* $[u, v]_{\equiv_L} \xrightarrow{a:1} [u', v']_{\equiv_L}$ if $uva \sim_L u'v'$.

Note that the transitions are well-defined: for the first case by Lemma 4, and for the second case because $(u_1, v_1) \equiv_L (u_2, v_2)$ implies that $u_1v_1 \sim_L u_2v_2$, and $\sim_L$ is a right-congruence.

**Example 4.** For the language $L$ from Examples 1 and 2, the canonical automaton $A_{\equiv_L}$ has one state for each letter $a_i$, which corresponds to the class of *pointed* pairs $(\varepsilon, v)$, where $v$ contains all letters except $a_i$. There are loops of 2-transitions on this state for all letters except $a_i$. Since $\sim_L$ has only one class, all states are connected by 1-transitions for all letters (so the 1-transitions on every letter form a complete graph).

**Example 5.** For the language $L$ from Example 3, the canonical automaton $A_{\equiv_L}$ is obtained by taking the $\equiv_L$-classes with solid frame shown in Figure 1, and the 2-transitions connecting them. The 1-transitions are inherited from the transitions shown for $\sim_L$ in Figure 1, namely, a transition on letter $a$ connecting two $\sim_L$-classes induces 1-transitions connecting all states corresponding to the first class to all the states corresponding to the second class. For example, the transitions $(a, \varepsilon) \xrightarrow{b:1} (a, b)$ and $(a, \varepsilon) \xrightarrow{b:1} (ab, c)$ are induced by a transition from the yellow $\sim_L$-class to the green $\sim_L$-class. From the initial state $(\varepsilon, \varepsilon)$ we have $\xrightarrow{a:1}$ transition to $(a, \varepsilon)$.

**Theorem 7.** The automaton $A_{\equiv_L}$ is the minimal history-deterministic co-Büchi automaton for $L$.
The rest of this section is devoted to the sketch of the proof of this theorem. First, we need to verify that indeed $A_{\equiv_L}$ accepts $L$. The following proposition more precisely characterizes the languages and the safe languages accepted from the states of $A_{\equiv_L}$. It also justifies our notation $sf_L(u, v)$.

**Proposition 8.** For every state $[u, v]_{\equiv_L}$ of $A_{\equiv_L}$:

* $L([u, v]_{\equiv_L}) = (uv)^{-1}L$,

* $L^{sf}([u, v]_{\equiv_L}) = sf_L(u, v)$.

In particular, $A_{\equiv_L}$ accepts $L$.

Thanks to this proposition, and Lemma 2 it is quite easy to see that $A_{\equiv_L}$ is history-deterministic.

**Lemma 9.** $A_{\equiv_L}$ is semantically-deterministic, unsafe- saturated, and normalized. Hence, $A_{\equiv_L}$ is history- deterministic.

*Proof.* Semantic-determinism is implied by Proposition 8 and the fact that all the transitions of $A_{\equiv_L}$ respect the $\sim_L$-class. Since $A_{\equiv_L}$ contains all 1-transitions that respect the $\sim_L$-class, Proposition 8 implies that $A_{\equiv_L}$ is unsafe-saturated. As $A_{\equiv_L}$ is safe-deterministic by definition, Lemma 2 implies that $A_{\equiv_L}$ is history-deterministic.

It remains to show that $A_{\equiv_L}$ is normalized. Consider a state of $A_{\equiv_L}$ identified by a pointed pair $(u, v)$. Suppose $[u, v]_{\equiv_L} \xrightarrow{x:2} [u, vx]_{\equiv_L}$ with $x \neq \varepsilon$. By definitions of transitions in $A_{\equiv_L}$, pair $(u, vx)$ is pointed. Hence, $(u, vx) \not\asymp_L \bot$. This means that there is $y$ such that $uvxy \sim_L u$ and $u(vxy)^\omega \in L$. In particular, $(u, vxyv) \not\asymp_L \bot$, because $u(vxyvxy)^\omega \in L$. Now we observe that $uvxyv \sim_L uv$ so since $(u, v)$ is pointed we get $(u, v) \equiv_L (u, vxyv)$. Thus, $[u, vx]_{\equiv_L} \xrightarrow{vy:2} [u, v]_{\equiv_L}$. $\square$

It remains to show that $A_{\equiv_L}$ is minimal. This proof is slightly more involved. Similarly to [26] we show that there is an injection from $A_{\equiv_L}$ to every history-deterministic co-Büchi automaton for $L$ (Lemma 14). As a new tool, we use of the notion of central sequence (Definition 11 and Lemma 13). This allows us to directly give a proof for all history-deterministic co-Büchi automata for $L$, while [26] relies on [17] in order to restrict to safe-deterministic ones. We start with a small lemma that shows that $A_{\equiv_L}$ has the property called safe-minimal in [26].

**Lemma 10.** If $L([u, v]_{\equiv_L}) = L([u', v']_{\equiv_L})$ and $L^{sf}([u, v]_{\equiv_L}) = L^{sf}([u', v']_{\equiv_L})$ then $[u, v]_{\equiv_L} = [u', v']_{\equiv_L}$.

**Definition 11.** Let $\mathcal{B}$ be a safe-deterministic co-Büchi automaton. A central sequence for a state $q$ of $\mathcal{B}$ is $z_q \in \Sigma^*$ such that $q \xrightarrow{z_q:2} q$ and for every $p$ with $L(p) = L(q)$ we have $p \xrightarrow{z_q:2} q$ or $p \xrightarrow{z_q:1} p$.

*Remark 12.* Recall that $p \xrightarrow{z_q:1} q$ means that every run from $p$ on $z_q$ visits a 1 transition, and there is at least one such run. A central sequence of $q$ can be $\varepsilon$. In this case the definition degenerates to saying that there is no state $p \neq q$ with $L(p) = L(q)$.

**Lemma 13.** Each state $q$ of $A_{\equiv_L}$ has a central sequence $z_q$.

The following lemma when put together with Lemma 10 shows that $A_{\equiv_L}$ is a minimal history-deterministic co-Büchi automaton for $L$.

**Lemma 14.** Let $\mathcal{B}$ be a history-deterministic co-Büchi automaton for $L$. For each state $p$ of $A_{\equiv_L}$ there is a state $q_p$ of $\mathcal{B}$ with $L^{sf}(A_{\equiv_L}, p) = L^{sf}(\mathcal{B}, q_p)$ and $L(A_{\equiv_L}, p) = L(\mathcal{B}, q_p)$.

*Proof.* We can assume that $\mathcal{B}$ is normalized and semantically-deterministic by Lemma 1.

Let $p$ be a state of $A_{\equiv_L}$. By Lemma 13, there is a central sequence $z_p$ for $p$. Call a state $q$ of $\mathcal{B}$ a $z_p$-loop if $L(\mathcal{B}, q) = L(A_{\equiv_L}, p)$ and $q \xrightarrow{z_p:2} q$ for some $k \geq 1$.

We first show that $L^{sf}(\mathcal{B}, q) \subseteq L^{sf}(A_{\equiv_L}, p)$ for every $q$ that is a $z_p$-loop. Suppose for a contradiction that $x \in L^{sf}(\mathcal{B}, q) \setminus L^{sf}(A_{\equiv_L}, p)$. Then $x \neq \varepsilon$ because $\varepsilon$ is in $L^{sf}$ of every state. Let $y \in \Sigma^*$ with $q \xrightarrow{xy:2} q$. Such $y$ exists because $\mathcal{B}$ is normalized. Then $\mathcal{B}$ accepts $(z_p^kxy)^\omega$ from $q$. But since $z_p$ is central for $p$ and $x \notin L^{sf}(A_{\equiv_L}, p)$, we have that when starting from an arbitrary state, $z_p^kxy$ must see a 1-transition. So $(z_p^kxy)^\omega$ is not accepted from $p$, contradicting $L(\mathcal{B}, q) = L(A_{\equiv_L}, p)$.

Now assume that there is $x_q \in L^{sf}(A_{\equiv_L}, p) \setminus L^{sf}(\mathcal{B}, q)$ for every $z_p$-loop $q$ of $\mathcal{B}$. Let $y_q$ be such that $p \xrightarrow{x_qy_q:2} p$. Let $f$ be a strategy witnessing history-determinism of $\mathcal{B}$, let $u \in \Sigma^*$ such that $p$ is reachable via $u$ in $A_{\equiv_L}$, and consider the run of $\mathcal{B}$ constructed by $f$ of the following form:

$$ (\mathcal{B}, f) : q_0 \xrightarrow{uz_p^{n_0}} q_1 \xrightarrow{x_1y_1z_p^{n_1:1}} q_2 \xrightarrow{x_2y_2z_p^{n_2:1}} q_3 \dots $$

where each $n_i$ is chosen such that $q_{i+1}$ is a $z_p$-loop (just iterate $z_p$ until a state repeats), $x_i = x_{q_i}$, and $y_i = y_{q_i}$. Then this run visits 1-transitions on all $x_i$ and thus is not accepting. But in $A_{\equiv_L}$ there is an accepting run that moves to $p$ on $u$ and then loops on $p$ without visiting 1-transitions. This contradicts that $f$ constructs an accepting run for each word in $L$, so there must be a $z_p$ loop $q$ that has the same safe language as $p$. $\square$

## IV. PASSIVE LEARNING

A sample $S$ is a set of pairs $(u, v) \in \Sigma^* \times \Sigma^+$ partitioned into sets $S^+$ and $S^-$, we often write $S = (S^+, S^-)$. A pair $(u, v)$ represents the ultimately periodic word $uv^\omega$. An ultimately periodic word can be represented by different pairs (e.g., $(a, b)$ and $(ab, bbb)$ represent the same ultimately periodic word). When we say that $uv^\omega$ is in the sample, we mean that some pair representing $uv^\omega$ is in the sample. The size of a sample is the sum of the lengths $|uv|$ over all the $(u, v)$ in the sample. A sample $S$ is consistent with $L \subseteq \Sigma^\omega$ if $S^+ \subseteq L$ and $L \cap S^- = \emptyset$. We say that $S_2$ is an extension of $S_1$ if $S_1^+ \subseteq S_2^+$ and $S_1^- \subseteq S_2^-$, and we write $S_1 \subseteq S_2$ in this case.

A passive learner for history deterministic co-Büchi automata (just learner, for short) is a function $f$ that maps samples to history deterministic co-Büchi automata. Such a learner $f$ is called a polynomial-time learner if $f$ can be computed in polynomial time (as usual, measured in the size of the input, i.e., the sample), and $f$ is a consistent learner
if for each sample $S = (S^+, S^-)$, the constructed automaton is consistent with $S$, meaning the language of the automaton $f(S)$ is consistent with the sample $S$. Further, we say that $f$ can learn every co-Büchi language from polynomial data if for each co-Büchi language $L$ there is a characteristic sample $S_L$ of size polynomial in $A_{\equiv_L}$, where characteristic means that for $A := f(S_L)$ we have $L(A) = L$ and for every extension $S$ of $S_L$ that is consistent with $L$ we have $f(S) = A$.

## A. Overview and Challenges

Assuming that the sample contains the relevant information for the language $L$, our learner constructs the automaton $A_{\equiv_L}$ by inferring the classes of $\equiv_L$ for pointed pairs.

The first step is to find representatives $R_{\sim_L}$ for the classes of $\sim_L$, which is used in the definition of $\equiv_L$. This is straightforward and can be done as for finite words. We start with $\varepsilon \in R_{\sim_L}$. In a loop, having already $R_{\sim_L} = \{u_1, \dots, u_k\}$, we find the smallest $u$ such that for all $i$ there is a proof in $S$ of $u \not\sim_L u_i$. A proof consists of two witnesses $(uw, x) \in S^+$ and $(u_i w, x) \in S^-$ for some $w, x$ (or with $S^+$, $S^-$ interchanged). If the sample contains all the minimal representatives of $\sim_L$ classes, and contains proofs that they are pairwise not $\sim_L$-equivalent then this algorithm indeed finds the minimal representatives of the $\sim_L$-classes. The algorithm terminates, as the number of candidates for $u$ is bounded by the size of $S$.

For finding representatives of the pointed $\equiv_L$-classes, there are two main challenges. The first one is that non-equivalence for $\equiv_L$ can, in general, not be witnessed by finitely many examples: Spelling out the full definition of $\not\equiv_L$ shows that it contains a universal quantifier over finite words, so it is not sufficient to give finitely many examples for proving $(u, v) \not\equiv_L (u', v')$. The second challenge is that we need to extract the pointed classes. Since the definition of pointed contains a universal quantifier and uses the relation $\equiv_L$, it is not directly possible to prove that a pair is pointed just by adding finitely many examples to the sample. Note that constructing all classes of $\equiv_L$ is not an option since the total number of $\equiv_L$-classes can be exponential in the size of the minimal automaton (see Example 2). Furthermore, there are example languages showing that $\equiv_L$ can have classes whose shortest representatives have length exponential in the number of pointed classes (see Example 6).

Our plan for solving these challenges is as follows:

* In (Section IV-B) we introduce relation $\approx_L$, which is a refinement of $\equiv_L$, and we show that it can be used instead of $\equiv_L$ on pointed elements.

* We immediately put $\approx_L$ to work in Section IV-C by showing how to construct a safe SCC of $A_{\equiv_L}$ for a given pointed $(u, v)$. This turns out to be easy, essentially it is the same as for languages of finite words because non-equivalence $\not\approx_L$ can be witnessed as easily as $\not\sim_L$.

* In Section IV-D we present a complete but idealized learning algorithm assuming that we can query some properties of $L$. This idealized version is easier to understand, and its correctness proof serves as an intermediate

step for the correctness proof of the passive learning algorithm.

* The most complicated step in the idealized algorithm is to find a fresh pointed pair $(u, v)$. For this we need new theoretical developments in form of a few technical lemmas. This step is presented in a separate Section IV-E. There we also give an example illustrating the main steps of the algorithm (Example 7).

* Finally, in Section IV-F, we spell out the passive learning algorithm that is obtained by essentially replacing each line of the idealized algorithm by a passive learning procedure. We prove correctness of each of these procedures.

## B. Equivalence $\approx_L$

The first step in our plan is to introduce an equivalence relation $\approx_L$ that we can use instead of $\equiv_L$ in some contexts. It is central to our learning algorithm.

**Definition 15.** For $(u, v), (u', v') \in \Sigma^* \times \Sigma^+$ we define $(u, v) \approx_L (u', v')$ if $u \sim_L u'$, $uv \sim_L u'v'$, and for every $x \in \Sigma^*$ with $uvx \sim_L u$ we have $u(vx)^\omega \in L$ iff $u'(v'x)^\omega \notin L$.

Observe that we require that the second components of the pairs in the relation are not empty as otherwise a statement like $u(vx)^\omega \in L$ would not make sense when $vx = \varepsilon$. The $\approx_L$ relation is easy to work with in the context of learning because a proof for non-equivalence $(u, v) \not\approx_L (u', v')$ requires only two pairs $(u, vx), (u'v'x)$ with $u(vx)^\omega \in L$ iff $u'(v'x)^\omega \notin L$. This is in contrast to the $\equiv_L$ relation that is defined by a nested quantification. The following crucial lemma shows that once we have a pointed pair, we can work with $\approx_L$ instead of $\equiv_L$.

**Lemma 16.** For $(u, v)$ pointed with $v \neq \varepsilon$, and for arbitrary $x, y \in \Sigma^*$ we have: $(u, vx) \equiv_L (u, vy)$ iff $(u, vx) \approx_L (u, vy)$.

## C. Components $C(u, v)$ and automaton $A[C]$

Our next goal is to construct for a given pointed $(u, v)$ an automaton $C(u, v)$ isomorphic to the safe SCC of $A_{\equiv_L}$ containing $[u, v]_{\equiv_L}$. Here we profit from Lemma 16 allowing us to work with $\approx_L$ instead of $\equiv_L$. We call such an automaton a *component*. Then for a set of components $C$ we can define an automaton $A[C]$ as $A_{\equiv_L}$ restricted to these components.

The set of states of $C(u, v)$ consists of representatives of $\approx_L$-equivalence classes extending $(u, v)$, namely the set $R_{\approx_L}(u, v) = \{(u, vw_1), \dots, (u, vw_k)\}$ of pairs such that

* $w_1 = \varepsilon$,

* $w_i$ is the smallest such that $(u, vw_i) \not\approx_L \{\perp, (u, vw_1), \dots, (u, vw_{i-1})\}$, and

* for every pair $(u, vw)$ extending $(u, v)$ we have $(u, vw) \approx_L (u, vw_i)$ for some $i$.

The set $R_{\approx_L}(u, v)$ can be constructed using the same principle as for the construction of $R_{\sim_L}$ described at the beginning of Section IV-A.

The transitions of $C(u, v)$ are determined by:

* $(u, vw_i) \xrightarrow{a:2} (u, vw_j)$ if $(u, vw_i a) \approx_L (u, vw_j)$.

So a component has only rank 2 transitions.
Listing 1: An idealized learning algorithm constructing $\mathcal{A}_{\equiv_L}$

1 **find** the set $R_{\sim_L} = \{u_1, \dots, u_k\}$

2 **find** $NT_{\sim_L} \subseteq R_{\sim_L}$

3 $\mathcal{C} := \{C(u, \varepsilon) : u \in R_{\sim_L} - NT_{\sim_L}\}$

4 $\mathcal{A} := \mathcal{A}[\mathcal{C}]$

5 **while** $L \neq L(\mathcal{A})$ **do**

6 **find** the smallest $u_i$ such that there is $x$ with $u_i x^{\omega} \in L - L(\mathcal{A})$, and $u_i x \sim_L u_i$.

7 **find** the smallest $x$ such that

$$u_i x^{\omega} \in L - L(\mathcal{A}) \text{ and } u_i x \sim_L u_i$$

8 **find** a pointed $(u_i, x^d v)$ extending $(u_i, x^d)$ with $d = \max(\{|C| : C \in \mathcal{C}\} \cup \{1\})$

9 **find** $R_{\sim_L}(u_i, x^d v)$

10 **construct** the component $C(u_i, x^d v)$ using $R_{\sim_L}(u_i, x^d v)$

11 **add** $C(u_i, x^d v)$ to $\mathcal{C}$.

12 $\mathcal{A} := \mathcal{A}[\mathcal{C}]$

13 **return**($\mathcal{A}$)

**Lemma 17.** If $(u, v)$ is pointed then $C(u, v)$ is isomorphic to the safe SCC of $\mathcal{A}_{\equiv_L}$ containing $[u, v]_{\equiv_L}$.

**Definition 18.** Given some set of components $\mathcal{C} = \{C(u_1, v_1), \dots, C(u_k, v_k)\}$ we define automaton $\mathcal{A}[\mathcal{C}]$ whose states are the states of these components, whose rank 2 transitions are the transitions in these components, and whose rank 1 transitions are: $(u, v) \xrightarrow{a:1} (u', v')$ if $uv \sim_L u'v'$. The initial states are $(u, v)$ such that $uv \sim_L \varepsilon$.

**Lemma 19.** For every set of components $\mathcal{C}$, we have $L(\mathcal{A}[\mathcal{C}]) \subseteq L(\mathcal{A}_{\equiv_L})$. There is a set of components such that $L(\mathcal{A}[\mathcal{C}]) = L(\mathcal{A}_{\equiv_L})$.

*Proof.* Every component corresponds to a safe SCC of $\mathcal{A}_{\equiv_L}$. The rank 1 transitions in $\mathcal{A}[\mathcal{C}]$ are placed exactly as in $\mathcal{A}_{\equiv_L}$. So the graph of $\mathcal{A}[\mathcal{C}]$ is a subgraph of $\mathcal{A}_{\equiv_L}$, hence $L(\mathcal{A}[\mathcal{C}]) \subseteq L(\mathcal{A}_{\equiv_L})$. If $\mathcal{C}$ contains a component for every safe SCC of $\mathcal{A}_{\equiv_L}$ then we get the equality. $\square$

### D. Idealized learning algorithm

We are ready to present an idealized version of the learning algorithm in Listing 1 that assumes unrestricted access to the language $L$. In Section IV-F, we discuss how to implement each of these steps in a true passive learning algorithm that does not have access to $L$ but only to a sample of $L$.

Let us look closer how this idealized version of the algorithm works. The first step is to find representatives for the classes of $\sim_L$. For this the algorithm computes the set $R_{\sim_L} = \{u_1, \dots, u_k\}$ as explained at the beginning of Section IV-A.

Then the algorithm proceeds with constructing all the components of $\mathcal{A}_{\equiv_L}$. There are two types of components. We have trivial components corresponding to $[u, \varepsilon]_{\equiv_L}$ with $ux^{\omega} \notin L$ for all $x \in \Sigma^+$. Observe that such $(u, \varepsilon)$ is pointed, and there are

no rank 2 transitions going out of $[u, \varepsilon]_{\equiv_L}$. For the language from Examples 3, 5 and Figure 1, these are the components of the classes $[(\varepsilon, \varepsilon)]_{\equiv_L}$ and $[(b, \varepsilon)]_{\equiv_L}$. The algorithm computes the set $NT_{\sim_L} \subseteq R_{\sim_L}$ of those $u_i$ for which there is $x$ with $u_i \sim_L u_i x$ and $u_i x^{\omega} \in L$. These classes of $\sim_L$ give rise to non-trivial components in $\mathcal{A}_{\equiv_L}$. Again in the example from Figure 1, the set $NT_{\sim_L}$ is $\{a, ab\}$. If $u_i \notin NT_{\sim_L}$ then $C(u_i, \varepsilon)$ is a trivial component consisting of one state with no transitions: $(u_i, \varepsilon)$ is pointed and $sf_L(u_i, \varepsilon) = \{\varepsilon\}$. All such components are added to $\mathcal{C}$, and at this point $\mathcal{A}[\mathcal{C}]$ is the automaton accepting the empty language as it has no rank 2 transitions.

In the while-loop of the algorithm we keep the invariant that $L(\mathcal{A}[\mathcal{C}]) \subseteq L$. If the inclusion is strict, then we find the smallest example for this, namely we find the smallest $\sim_L$-class $u_i$ and the smallest $x$ for this class such that $u_i x^{\omega} \in L - L(\mathcal{A})$ and $u_i x \sim_L u_i$. Then we find a pointed pair $(u_i, x^d v)$ extending $(u_i, x^d)$, for sufficiently big $d$. The choice of $d$ is such that it guarantees that $(u_i, x^d v)$ is new, namely $(u_i, x^d v) \not\equiv_L (u', v')$ for all $(u', v') \in \bigcup \mathcal{C}$ (cf. Lemma 20). Hence, the component $C(u_i, x^d v)$ that we add to $\mathcal{C}$ strictly increases the size of $\mathcal{C}$. This guarantees termination in polynomial time as the number of equivalence classes of $\equiv_L$ with a pointed pair is exactly the size of $\mathcal{A}_{\equiv_L}$. In the example from Figure 1, after adding the trivial components, we would get $u_i = a$ and $x = a$ and $d = 1$. The pair $(a, a)$ is already pointed, so the algorithm proceeds with constructing the component containing the classes $[(a, a)]_{\equiv_L} = [(a, \varepsilon)]_{\equiv_L}$ and $[(a, b)]_{\equiv_L}$.

All the steps but that of finding a new pointed pair in line 8 are relatively easy to implement in a passive learning algorithm. We discuss line 8 in Section IV-E. At this point we can already prove correctness and the polynomial time complexity of the algorithm (Theorem 21) assuming every step is implemented correctly. The proof is based on the next lemma ensuring that the algorithm adds a new component in every iteration of the loop. More precisely, it says that once we have found $(u, x^d)$, we can be sure that all its extensions $(u, x^d v)$ are new, as long as they are pointed.

**Lemma 20.** With the notations from Listing 1, suppose $ux^{\omega} \in L - L(\mathcal{A}[\mathcal{C}])$ and $ux \sim_L u$. Suppose moreover that $d = \max(\{|C| : C \in \mathcal{C}\} \cup \{1\})$. If $(u, x^d v)$ is a pointed pair extending $(u, x^d)$ then $(u, x^d v) \not\equiv_L (u', v')$ for every $(u', v') \in \bigcup \mathcal{C}$.

**Theorem 21.** *The idealized algorithm from Listing 1 does at most $|\mathcal{A}_{\equiv_L}|$ iterations of the loop and returns $\mathcal{A}_{\equiv_L}$.*

*Proof.* The main point is to show that the invariant is that $\mathcal{C}$ is a subset of the components of $\mathcal{A}_{\equiv_L}$. Then by Lemma 19 we have $L(\mathcal{A}[\mathcal{C}]) \subseteq L(\mathcal{A}_{\equiv_L})$. This invariant implies correctness. As Lemma 20 shows, in every iteration of the loop we add a new component. Hence, the number of iterations of the loop is bounded by the size of $\mathcal{A}_{\equiv_L}$.

Let us look why the invariant holds. The invariant is preserved in the loop thanks to Lemma 17 as each time we add $C(u_i, x^d v)$ for a pointed $(u_i, x^d v)$. It remains to check
<table><caption>Listing 2: Finding a pointed $(u, w\bar{v})$ extending $(u, v)$</caption><tr><td>1</td><td>function FindPointed(u, v):</td></tr><tr><td>2</td><td>Assume u ~<sub>L</sub> uv.</td></tr><tr><td>3</td><td>Set v̄ = v.</td></tr><tr><td>4</td><td>while ∃x s.t. u ~<sub>L</sub> u&#773;vx, (u, v̄xv̄) ≁<sub>L</sub> ⊥ and<br/>u(v̄x)ω ∉ L</td></tr><tr><td>5</td><td>Find the smallest such x.</td></tr><tr><td>6</td><td>v̄ := v̄(xv̄)m, where m the biggest s.t.,<br/>(u, v̄(xv̄)m) ≁<sub>L</sub> ⊥.</td></tr><tr><td>7</td><td>Set w = ε.</td></tr><tr><td>8</td><td>while ∃x s.t. u ~<sub>L</sub> uwv̄x, (u, w&#773;v̄xv̄) ≁<sub>L</sub> {⊥, (u, w&#773;v̄)}</td></tr><tr><td>9</td><td>Find the smallest such x.</td></tr><tr><td>10</td><td>w := w&#773;vx.</td></tr><tr><td>11</td><td>return (u, w&#773;v̄)</td></tr></table>

that the invariant holds in the beginning when $C$ contains $C(u, \varepsilon)$ for all $u \in R_{\sim_L} - NT_{\sim_L}$. We need to verify that $(u, \varepsilon)$ is pointed. For this we show that for every $u_1u_2 \sim_L u$ with $u_2 \neq \varepsilon$ we have $(u_1, u_2) \approx_L \perp$. Indeed, if $(u_1, u_2) \not\approx_L \perp$, then there would be $x$ with $u_1 \sim_L u_1u_2x$ and $u_1(u_2x)^\omega \in L$. But then $u_1u_2(xu_2)^\omega \in L$, hence $u(xu_2)^\omega \in L$ meaning $u \in NT_{\sim_L}$. □

### E. Finding a new pointed element

The difficult part of the idealized learning algorithm from Listing 1 is hidden in line 8. The task is to extend (the second component of) a given pair $(u, v) \not\approx_L \perp$, satisfying $u \sim_L uv$, to a pointed pair. An idealized algorithm is presented in Listing 2. But to explain the idea behind it, we need a definition and some lemmas.

We heavily use the structure of $A_{\equiv_L}$ in this subsection. We use $p, q$ for states of $A_{\equiv_L}$. Whenever we talk about states or transitions, this refers to the automaton $A_{\equiv_L}$. We write $\xrightarrow{u} p$ to mean that in $A_{\equiv_L}$ there is a run on $u$ from an initial state to $p$.

**Definition 22.** For a pair $(u, v)$ we define:

$$ \theta(u, v) = \{q : \exists p. \xrightarrow{u} p \xrightarrow{v:2} q\} $$

The general idea is to use $\theta$ as a measure for how close a pair is to being pointed, since the pointed elements are those for which $\theta$ is a singleton, as shown in Lemma 25. Given a pair $(u, v)$ that is not yet pointed, the algorithm starts by finding an $x$ such that $\theta(u, vxv) \subseteq \theta(u, v)$. The following example illustrates that such an $x$ has to be chosen with care because the length of $vxv$ at least doubles w.r.t. the length of $v$.

**Example 6.** Let $k \ge 1$, let $\Sigma := \{a_0, \dots, a_{k+1}\}$ and for $i \in \{0, \dots, k\}$ let $\Sigma_{>i} := \{a_j \mid i < j \le k+1\}$ and $\Sigma_{<i} := \{a_j \mid 0 \le j < i\}$. Let $L$ be the set of all $\omega$-words that for some $i \in \{0, \dots, k\}$ only finitely often contain patterns of the form $a_i \Sigma_{<i}^* a_i$ and $\Sigma_{>i} \Sigma_{<i}^* \Sigma_{>i}$. That is, when removing all letters from $\Sigma_{<i}$, there are no two successive occurrences of $a_i$ and no two successive occurrences of $\Sigma_{>i}$. For example, $a_j^\omega \in L$

<figure><img src="image_4.png" /><figcaption>Fig. 2: The 2-transitions of the minimal history-deterministic co-Büchi automaton for the language from Example 6 with state set $Q_k$.</figcaption></figure>

for all $j \in \{0, \dots, k-1\}$ because there are no occurrences of the bad patterns for all $i \in \{j+1, \dots, k\}$. But $a_k^\omega \notin L$ because for $i \in \{0, \dots, k-1\}$ the pattern $\Sigma_{>i} \Sigma_{>i}$ occurs infinitely often, and for $i=k$, the pattern $a_ia_i$ occurs infinitely often. Similarly, $a_{k+1}^\omega \notin L$.

Figure 2 shows the 2-transitions of the minimal history-deterministic co-Büchi automaton for $L$. The language has only one $\sim_L$-class and thus the automaton contains all possible 1-transitions. Note that all the components have the same structure. The left-most component does not have self-loops because $\Sigma_{<0}$ is empty. And the edge label $a_{k+1}$ on the transition from $q_k^1$ to $q_k^0$ corresponds to the only letter from $\Sigma_{>k}$. In what follows, we will see that there are words making the automaton to behave as a counter counting up to $2^k$.

Assume that we want to construct a pointed pair that extends $(\varepsilon, v_0)$ with $v_0 = \varepsilon$. The least $x_0$ such that $\theta(\varepsilon, v_0x_0v_0) \subseteq \theta(\varepsilon, v_0)$ is $x_0 := a_0$. So we let $v_1 := v_0x_0v_0 = a_0$. Then $\theta(\varepsilon, v_1)$ contains all states except $q_0^0$. The smallest $x_1$ such that $\theta(\varepsilon, v_1x_1v_1) \subseteq \theta(\varepsilon, v_1)$ is $x_1 := a_1$. So we let $v_2 := v_1x_1v_1 = a_0a_1a_0$. If we continue like this, then we get $v_{j+1} := v_jx_jv_j$ with $x_j := a_j$, and $\theta(\varepsilon, v_{j+1})$ contains all states except $q_0^0, \dots, q_j^0$. This “greedy” way of making progress towards pointed pairs thus produces pairs of exponential length since $|v_j| = 2^{j+1} - 1$. Some further properties of this example are that $(\varepsilon, v_k)$ visits $2^k$ different SCCs of the $\equiv_L$-graph in the sense that for all prefixes $v \sqsubseteq v' \sqsubseteq v_k$ with $v \neq v'$, we have $(\varepsilon, v) \not\equiv_L (\varepsilon, v'w)$ for all $w$. Further, the pair $(\varepsilon, a_kv_k)$ is the shortest in its $\equiv_L$-class. This shows that there are not only exponentially many $\equiv_L$-classes but also classes in which the shortest representative has exponential length in the size of $A_{\equiv_L}$.

In order to avoid ending up with words of exponential length, we show that the words $x$ can be chosen such that the decrease from $\theta(u, v)$ to $\theta(u, vxv)$ is significant, or that we can switch to another method not doubling the second element of the pair in every step (the second while loop in Listing 2). For this we use the following definitions, which are illustrated in Example 7.

**Definition 23.** We say:

* $(u, v)$ is supported if $\theta(u, v) \neq \emptyset$.

* $(u, v)$ is double-supported if there are two elements from $\theta(u, v)$ in the same safe SCC of $A_{\equiv_L}$.

* $(u, v)$ is single-supported if it is supported but not double-supported.

Basically, the algorithm FindPointed in Listing 2 extends
the second component of the given pair $(u, v)$ by iteratively constructing words $\bar{v}$ and $w$, starting with $\bar{v} = v$ and $w = \varepsilon$, such that the size of $\theta(u, w\bar{v})$ decreases. The notions of double-supported and single-supported correspond to the two while loops in Listing 2. If $(u, \bar{v}) \not\le_L \perp$ is not pointed then $\theta(u, \bar{v})$ is supported but not a singleton (Lemma 25). If $(u, \bar{v})$ is double-supported, then by Lemma 26 there is $x$ satisfying the condition of the first while loop. When the condition of the first while loop is no longer true, then $(u, \bar{v})$ is single-supported. Either $(u, w\bar{v})$ is pointed, or by Lemma 29 there is $x$ satisfying the condition of the second while loop, and $\theta(u, w\bar{v})$ decreases. In each iteration of the first while loop, the length of the second component more than doubles, but Lemma 27 shows that at the same time $\theta(u, \bar{v})$ decreases quickly enough. In the iterations of the second while loop, the length of the second component increases only by a polynomial factor. Before going into details we explain this on our example.

**Example 7.** We continue Example 6 from Figure 2 to illustrate the concepts of single-supported and double-supported and the use of the different lemmas in the construction of pointed pairs. Note that for this example language $\sim_L$ is trivial, so $R_{\sim_L} = \{\varepsilon\}$ and we can ignore all conditions on $\sim_L$ in the algorithm.

Consider Listing 1, and assume that the component $C_0$ consisting of $\{q_0^0, q_0^1\}$ has already been constructed (it is indeed the first one that our algorithm constructs). Then $x = a_0$ in line 7 because $(a_0)^\omega \in L$ but it is not accepted by the component $C_0$. Then $d = 2$ in line 8, and FindPointed($\varepsilon, a_0a_0$) is called. We now enter the notation in this call of FindPointed. We index the different $\bar{v}$ for better readability.

We start with $\bar{v}_0 = a_0a_0$, for which $\theta(\varepsilon, \bar{v}_0) = Q_k\{q_0^0, q_0^1\}$, which are all states except the ones from $C_0$. So $(\varepsilon, \bar{v}_0)$ is double-supported, and Lemma 26 guarantees the condition of the while loop in line 4 is satisfied. Then $x = a_k$ in line 5 because $(\bar{v}_0a_k)^\omega \notin L$, $\bar{v}_0a_k\bar{v}_0 \not\le_L \perp$. We have $\bar{v}_0(a_k\bar{v}_0)^2 \approx_L \perp$ because the repetition of $a_0$ removes all states from $C_0$, and the repetition of $a_k$ with only $a_0$ in between removes the states of all other components. Hence, $m = 1$ in line 6 and we continue with $\bar{v}_1 := \bar{v}_0a_k\bar{v}_0$. Note that $|\bar{v}_1| = 2|\bar{v}_0| + |x|$. Lemma 28 guarantees that the length of $x$ is polynomial in the size of $A_{\approx_L}$, and Lemma 27 guarantees that $|\theta(\varepsilon, \bar{v}_1)| \le \frac{1}{2}|\theta(\varepsilon, \bar{v}_0)|$. And indeed we have $\theta(\varepsilon, \bar{v}_1) = \{q_1^0, \dots, q_{k-1}^0, q_k^1\}$. So these two lemmas ensure that the length of the $\bar{v}$ constructed in the first loop remains polynomial. For this, it is essential that $u(\bar{v}x)^\omega$ is not in $L$ in line 4, which ensures a quick decrease of $\theta$, and avoids the problems illustrated in Example 6.

At this point the condition of the while loop in line 4 is not satisfied anymore for $(\varepsilon, \bar{v}_1)$. Since $(\varepsilon, \bar{v}_1)$ is single-supported (but not yet pointed because $\theta(\varepsilon, \bar{v}_1)$ is not a singleton), Lemma 29 guarantees that the condition of the while loop in line 8 is satisfied (with $w = \varepsilon$) with an $x$ whose length is polynomial in $A_{\approx_L}$. Then $x = a_1$ in line 9 because $\theta(\varepsilon, \bar{v}_1a_1\bar{v}_1) = \{q_1^0\}$, so $(\varepsilon, \bar{v}_1a_1\bar{v}_1) \not\le_L \perp$ and $(\varepsilon, \bar{v}_1a_1\bar{v}_1) \not\le_L (\varepsilon, \bar{v}_1)$ because, for example, $(\varepsilon, \bar{v}_1a_1\bar{v}_1a_2) \approx_L \perp$ but $(\varepsilon, \bar{v}_1a_2) \not\le_L \perp$. Note that Lemma 29 only gives $\theta(\varepsilon, \bar{v}_1a_1\bar{v}_1) \subsetneq \theta(\varepsilon, \bar{v}_1)$, so it could

happen that the size of $\theta$ decreases by only 1. But every application of the second while loop only increases the length of $w$ by $x\bar{v}$ for the $x$ of the current execution of the while loop, and the fixed $\bar{v}$ resulting from the first loop, which is polynomial in $A_{\approx_L}$ as argued above (formal arguments are given in the proof of Proposition 30).

Now $(\varepsilon, \bar{v}_1a_1\bar{v}_1) = (\varepsilon, a_0a_0a_k a_0a_0a_1 a_0a_0a_k a_0a_0)$ is pointed and returned from the call FindPointed($\varepsilon, a_0a_0$). The main algorithm now proceeds by constructing the component of the returned pointed pair, which is $C_1$ in this case. This construction is based on Lemma 17. And Lemma 20 indeed guarantees that the returned pointed pair always belongs to a new component.

We proceed with the formal statements and arguments. The running time of the algorithm and the length of the computed words are expressed in terms of $\alpha := |A_{\approx_L}|$ that is the size of $A_{\approx_L}$. We start with two auxiliary lemmas, relating important notions on pairs of words to their $\theta$-sets.

**Lemma 24.** $\theta(u, v) = \emptyset$ iff $(u, v) \approx_L \perp$.

**Lemma 25.** $\theta(u, v)$ is a singleton iff $(u, v)$ is pointed.

The next two Lemmas 26 and 27 deal with the condition of the first while loop in line 4 of FindPointed, see Example 7 for an illustration.

**Lemma 26.** If $(u, v)$ is double-supported then there is $x \in \Sigma^+$ such that $u \sim_L uvx$, $(u, vxv) \not\le_L \perp$, and $u(vx)^\omega \notin L$.

**Lemma 27.** Suppose $(u, v) \not\le_L \perp$, $u \sim_L uv \sim_L uvx$, and $u(vx)^\omega \notin L$. Let $m$ maximal such that $(u, v(xv)^m) \not\le_L \perp$. Then $\theta(u, v(xv)^m) \subseteq \theta(u, v)$ and $|\theta(u, v(xv)^m)| \le \frac{1}{m+1}|\theta(u, v)|$.

The next Lemma 28 deals with the size of a witness for the first while loop in line 4 of FindPointed, whose existence is guaranteed by Lemma 26 for double supported pairs.

**Lemma 28.** If there is an $x$ such that $u \sim_L uvx$, $(u, vxv) \not\le_L \perp$ and $u(vx)^\omega \notin L$ then there is one of size $< 2\alpha^3$.

Lemma 29 below deals with the condition of the second while loop in line 8 of FindPointed, see explanation after Definition 23, and Example 7 for an illustration.

**Lemma 29.** Suppose $(u, v)$ is single-supported, $uw \sim_L u$, and $(u, wv) \not\le_L \perp$ is not pointed. There is $x \in \Sigma^+$ such that $u \sim_L uwvx$ and $\perp \not\le_L (u, wvxx) \not\le_L (u, wv)$. Moreover, for every such $x$, $\theta(u, wvxx) \subsetneq \theta(u, v)$. Additionally, there is such $x$ of size $< 2\alpha^2$.

We are ready to prove that the algorithm FindPointed in Listing 2 is correct, runs in polynomial time, and produces a pointed pair of polynomial size.

**Proposition 30.** Given $(u, v) \not\le_L \perp$ with $v \neq \varepsilon$ such that $u \sim_L uv$, FindPointed$(u, v)$ in Listing 2 returns a pointed element $(u, w\bar{v}) \not\le_L \perp$. Moreover, the algorithm runs in time
polynomial in $|A_{\equiv_L}|$, $|w\bar{v}| \le 2|A_{\equiv_L}|^2|v| + 4|A_{\equiv_L}|^6$ and the initial $v$ is a prefix of $w\bar{v}$.

*Proof.* Recall that we use $\alpha$ for the size of $A_{\equiv_L}$. If $(u, v)$ is not pointed then $\theta(u, v)$ is not a singleton, by Lemma 25.

The first case is when $(u, v)$ is double-supported. At the beginning we consider $\bar{v} = v$. By Lemma 26 there is $x$ satisfying the condition of the first while loop. In the loop $\bar{v}$ is changed to $\bar{v}(x\bar{v})^m$ for some $m$. Observe, that $u \sim_L w\bar{v}(x\bar{v})^m$, and $(u, \bar{v}(x\bar{v})^m) \not\asymp_L \perp$ by the choice of $m$, so we can repeat the reasoning for $(u, \bar{v})$ where $\bar{v}$ is changed to $\bar{v}(x\bar{v})^m$. Let us note that $m \ge 1$, so indeed $\bar{v}$ is prolonged in this step and $\theta(u, \bar{v})$ decreases.

When the condition of the first while loop is no longer true then $(u, \bar{v})$ is single-supported (Lemma 26). Either $(u, w\bar{v})$ is pointed, or by Lemma 29 there is $x$ satisfying the condition of the second while loop. In this case we change $w$ to $w\bar{v}x$, and Lemma 29 says that $\theta(u, w\bar{v}x\bar{v})$ is strictly included in $\theta(u, w\bar{v})$. So $(u, w\bar{v}x\bar{v})$ is single-supported, and we can repeat the reasoning after updating $w$ to $w\bar{v}x$. Thus, the algorithm terminates with a pointed pair $(u, w\bar{v})$. By examining how $\bar{v}$ and $w$ are constructed we can see that the initial $v$ is always a prefix of $w\bar{v}$. This shows the last property stated in the proposition.

It remains to check that the algorithm runs in polynomial time and that the size of $w\bar{v}$ is bounded as stated in the lemma. Let $v_i$ denote the value of $\bar{v}$ just after the $i$-th iteration of the first while loop in line 4. Let $m_i$ be the value of $m$ at the same moment. We use $v_0$ for the initial $\bar{v}$. By Lemma 27 we have

$$|\theta(u, v_i)| \le \frac{1}{m_i + 1} |\theta(u, v_{i-1})|. \quad (1)$$

As we have observed above, $m_i \ge 1$, so we have in particular $|\theta(u, v_{i+1})| < |\theta(u, v_i)|$, for all $i$. Thus, the number $k$ of iterations of the first while loop is at most $\alpha$. As $x$ used in this loop comes from Lemma 28, its size is at most $\beta := 2\alpha^3$ giving us $|v_i| \le (m_i + 1)|v_{i-1}| + m_i\beta$. We check that for all $i = 1, \dots, k$:

$$|v_i| \le \left( \prod_{j=1}^{i} (m_j + 1) \right) (|v_0| + i\beta) \quad (2)$$

This holds for $i = 1$ as $|v_1| \le (m_1 + 1)|v_0| + m_1\beta$. By induction for $i > 1$ we have

$$\begin{aligned} |v_i| &\le (m_i + 1)|v_{i-1}| + m_i\beta \\ &\le (m_i + 1) \left( \prod_{j=1}^{i-1} (m_j + 1) \right) (|v_0| + (i-1)\beta) + m_i\beta \\ &= \left( \prod_{j=1}^{i} (m_j + 1) \right) (|v_0| + (i-1)\beta) + m_i\beta \\ &\le \left( \prod_{j=1}^{i} (m_j + 1) \right) (|v_0| + i\beta) \end{aligned}$$

The last inequality holds as $m_i \le \prod_{j=1}^{i} (m_j + 1)$.

By iterated application of equation (1) we have $\theta(u, v_k) \le \frac{\theta(u, v_0)}{\prod_{i=1}^k (m_i+1)}$. Since $|\theta(u, v_k)| \ge 1$, we get $\prod_{i=1}^k (m_i + 1) \le \theta(u, v_0) \le \alpha$. Plugging this bound into (2) for $v_k$, we get $|v_k| \le \alpha(|v_0| + \alpha\beta)$. Finally, since $\beta = 2\alpha^3$ and $v_k$ is the result of the first while loop, we get $|\bar{v}| \le \alpha|v_0| + 2\alpha^5$ at the end of the first while loop.

Now let us turn to the second while loop. By Lemma 29, $|\theta(u, w\bar{v}x\bar{v})| < |\theta(u, w\bar{v})|$, hence the loop executes at most $\alpha$ times. Each time $x$ is found thanks to Lemma 29, so $|x| \le 2\alpha^2$. Hence, at each iteration of the loop we prolong $w$ by at most $|\bar{v}| + 2\alpha^2$. This gives us a bound on the final size of $w$ as $|w| \le \alpha(|\bar{v}| + 2\alpha^2)$. Plugging in our bound on $|\bar{v}|$ from the previous paragraph we obtain $|w| \le \alpha(\alpha|v_0| + 2\alpha^5 + 2\alpha^2)$. So finally, $|w\bar{v}| \le \alpha^2|v_0| + 2\alpha^6 + 2\alpha^3 + \alpha|v_0| + 2\alpha^5$ that we can bound by $2\alpha^2|v_0| + 4\alpha^6$. $\square$

## F. Passive learning algorithm

The true learning algorithm does not have access to the language $L$, but only to a sample $S$. In this section we show how to implement the idealized algorithm from Listing 1 in a passive learning algorithm *Learn(S)* presented in Listing 3. It is parameterized by a sample $S$ given on input. Each line of the idealized algorithm is implemented by a corresponding function depending on $S$. Compared to the idealized algorithm from Listing 1, the algorithm from Listing 3 has two additional tests in lines 8 and 15. These are needed in case a sample has some incomplete information about $L$ that make our algorithm return incoherent results. In this case the algorithm returns some default automaton that accepts precisely $S^+$. Such an automaton is easy to construct, so we do not detail it here. This choice of a default automaton, together with the termination condition of the algorithm, guarantees that the algorithm is a consistent learner.

The result we prove is:

**Theorem 31.** *Learn(S)* is a consistent polynomial time passive learner that learns the minimal history-deterministic co-Büchi automaton $A_{\equiv_L}$ for each co-Büchi language $L$ in the limit from polynomial data.*

Compared to the idealized algorithm, the passive learning algorithm has to deduce information about the language $L$ from a sample. So all the tests that refer to the language $L$ (like membership or equality) have to be relativized to the sample $S$, which is done by the following definitions.

* $(u, v) \in_S L$ if $(u, v) \in S^+$,

* $(u, v) \notin_S L$ if $(u, v) \in S^-$,

* $L \neq_S L(\mathcal{A})$ for some automaton $\mathcal{A}$ if there is $(u, v)$ with either $(u, v) \in_S L$ and $uv^\omega \notin L(\mathcal{A})$, or $(u, v) \notin_S L$ and $uv^\omega \in L(\mathcal{A})$.

* $x \nsim_S y$ if there is $(u, v)$ such that either $(xu, v) \in_S L$ and $(yu, v) \notin_S L$, or $(xu, v) \notin_S L$ and $(yu, v) \in_S L$.

The most important thing to notice, is that $(u, v) \notin_S L$ is not the negation of $(u, v) \in_S L$. Indeed, it may happen that neither $(u, v) \in_S L$ nor $(u, v) \notin_S L$ hold as there is no information about $(u, v)$ in the sample. For this reason the formulation of these definitions is so long, as all the tests should be used positively. This guarantees that these definitions are stable under extensions: if they hold for $S$ then they hold for every $S'$ extending $S$.

For each function in Listing 3 we show that there is $S$ which is polynomial in the size of $A_{\equiv_L}$, for which the function
<table><caption>Listing 3: Passive learning algorithm for L</caption><tr><td>1</td><td>function Learn(S):</td></tr><tr><td>2</td><td>R := Find-R(S)</td></tr><tr><td>3</td><td>NT := Find-NT(R, S)</td></tr><tr><td>4</td><td>forevery u ∈ R − NT add C(u, ε) to C.</td></tr><tr><td>5</td><td>A = Automaton(R, C, S)</td></tr><tr><td>6</td><td>while L ≠<sub>S</sub> L(A) do</td></tr><tr><td>7</td><td>u := Find-u(A, NT, R, S)</td></tr><tr><td>8</td><td>if u = ⊥ then return(Default(S))</td></tr><tr><td>9</td><td>x := Find-x(u, A, R, S)</td></tr><tr><td>10</td><td>d := max({|C| : C ∈ C} ∪ {1})</td></tr><tr><td>11</td><td>(u, v) := FindPointedInS(u, x<sup>d</sup>, R, S)</td></tr><tr><td>12</td><td>C := Construct(u, v, R, S)</td></tr><tr><td>13</td><td>add C to C</td></tr><tr><td>14</td><td>A' = Automaton(R, C, S);</td></tr><tr><td>15</td><td>if L(A) ⊊ L(A') ⊆ S<sup>+</sup> then A := A' else<br/>return(Default(S))</td></tr><tr><td>16</td><td>return(A)</td></tr></table>

<table><caption>Listing 4: Finding $R_{\sim_L}$</caption><tr><td>1</td><td>function Find-R(S):</td></tr><tr><td>2</td><td>R := {Ø}</td></tr><tr><td>3</td><td>repeat</td></tr><tr><td>4</td><td>D := {x : ∀y ∈ R. x ≁<sub>S</sub> y}</td></tr><tr><td>5</td><td>if D ≠ Ø then add min(D) to R</td></tr><tr><td>6</td><td>until D = Ø</td></tr><tr><td>7</td><td>return(R)</td></tr></table>

• $(u, v) \not\asymp_S (u', v')$ if either $u \not\asymp_S u'$, or $uv \not\asymp_S u'v'$, or there is $x \in \Sigma^*$ such that $uvx \sim_S u$ and either $(u, vx) \in_S L$ and $(u', v'x) \notin_S L$, or $(u, vx) \notin_S L$ and $(u', v'x) \in_S L$.

These definitions are also stable under extensions, namely if S is big enough for $R_{\sim_L}$ to be correct, and has the necessary distinguishing examples for witnessing $x \sim_S y$, $(u, v) \not\asymp_S \perp$, or $(u, v) \not\asymp_S (u', v')$, this will also hold for every $S'$ that is consistent with L and extends S.

Remark 34. We manage to have a stabilizing test $x \sim_S y$ thanks to the enumeration $R_{\sim_L}$ of all equivalence classes of $\sim_S$ relation. It is tempting to follow the same route and get a test for $(u, v) \approx_L (u', v')$ by enumerating all classes of $\approx_L$ relation. The problem is that there are exponentially many such classes with respect to the size of the minimal automaton, cf. Example 2, so we cannot afford to do this if we want polynomial size samples and algorithms.

The other functions from Listing 3 are implemented similarly. Even the most complicated step in the idealized algorithm, namely FindPointed(u, v) needs only minimal changes to be implemented in the passive setting. Here we use the arguments from Proposition 30 to show that there is a stabilizing S of polynomial size in $|A_{\equiv_L}|$ allowing the algorithm to find the new pointed elements. It is sufficient to always add to the sample the least witnesses that are used in the proof from Proposition 30, together with witnesses ensuring that the required tests for $\sim_L$ and $\not\asymp_L$ give the same results as $\sim_S$ and $\not\asymp_S$.

V. CONCLUSION

The main technical result of this paper is a passive learning algorithm for history-deterministic co-Büchi automata that is polynomial in both time and data. This is the first such algorithm for a class that remains non-trivial when restricted to prefix-independent $\omega$-languages. With Example 6, we have highlighted the challenges concerning polynomial learning of $\omega$-automata, that can in part explain the slow progress in this area in the past. The straightforward congruence-based approach encounters the problem of an exponential number of congruence classes, and there are classes that can only be identified with exponentially long examples.

The other foundational contribution is a congruence-based description of minimal history-deterministic co-Büchi automata. The main novelty here is the notion of a pointed pair. Another subtlety is the definition of the $\equiv_L$ relation, which is similar to those present in the literature but does not require the first components to be $\sim_L$ equivalent.

For future work, it would be interesting to go beyond the co-Büchi condition. A good starting point are the chains of co-Büchi automata (COCOA) from [12], a canonical representation of all $\omega$-regular languages as a Boolean combination of history-deterministic co-Büchi automata. Another goal is to develop an active, Angluin-style [1] learning algorithm for the co-Büchi class. Finally, it would be interesting to have faster minimization algorithms for history-deterministic co-Büchi automata. As in the case of finite words, understanding their structure in terms of congruences may be helpful.

computes the right answer, and moreover this S is stabilizing in the following sense.

**Definition 32.** A sample S that is consistent with L is L-stabilizing for a function Func if for every $S'$ consistent with L such that $S' \supseteq S$, we have $Func(S') = Func(S)$. We just say stabilizing in the following since L is clear from the context.

The notion of stabilizing S can be seen in action already in the first line of the algorithm from Listing 3. The goal of function Find-R(S) is to compute $R_{\sim_L}$, the set of minimal representatives of all $\sim_L$ classes. The algorithm successively adds to D the smallest word that is in the relation $\not\asymp_S$ to all the words already in D, as already explained on page 7.

**Lemma 33.** There is a stabilizing S of size polynomial in $|A_{\equiv_L}|$ such that $R_{\sim_L} = Find-R(S)$. Moreover, the algorithm runs in time polynomial in S.

Assuming we have $R_{\sim_L}$, we can define further tests on S:

• $x \sim_S y$ if there is $u \in R_{\sim_L}$ such that $x \not\asymp_S u'$ and $y \not\asymp_S u'$ for all $u' \in R_{\sim_L}$, $u' \neq u$.

• $(u, v) \not\asymp_S \perp$ if $v = \varepsilon$ or there is $x \in \Sigma^*$ such that $uvx \sim_S u$ and $(u, vx) \in_S L$.
REFERENCES

[1] Dana Angluin. Learning regular sets from queries and counterexamples. Inf. Comput., 75(2):87-106, 1987.

[2] Dana Angluin, Dana Fisman, and Yaara Shoval. Polynomial identification of $\omega$-automata. In *Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020*, volume 12079 of Lecture Notes in Computer Science, pages 325-343. Springer, 2020.

[3] Christel Baier and Joost-Pieter Katoen. *Principles of model checking*. MIT Press, 2008.

[4] Alan W. Biermann and Jerome A. Feldman. On the synthesis of finite-state machines from samples of their behavior. *IEEE Trans. Computers*, 21(6):592-597, 1972.

[5] León Bohn and Christof Löding. Constructing deterministic $\omega$-automata from examples by an extension of the RPNI algorithm. In *46th International Symposium on Mathematical Foundations of Computer Science, MFCS 2021*, volume 202 of LIPICS, pages 20:1-20:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021.

[6] León Bohn and Christof Löding. Passive learning of deterministic büchi automata by combinations of DFAs. In *49th International Colloquium on Automata, Languages, and Programming, ICALP 2022*, July 4-8, 2022, Paris, France, volume 229 of LIPICS, pages 114:1-114:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.

[7] León Bohn and Christof Löding. Constructing deterministic parity automata from positive and negative examples. *TheoretICS*, 3, 2024.

[8] Udi Boker and Karoliina Lehtinen. When a little nondeterminism goes a long way: An introduction to history-determinism. *ACM SIGLOG News*, 10(1):24-51, 2023.

[9] J. Richard Büchi. On a decision method in restricted second order arithmetic. In *International Congress on Logic, Methodology and Philosophy of Science*, pages 1-11. Stanford University Press, 1962.

[10] Antonio Casares. On the minimisation of transition-based rabin automata and the chromatic memory requirements of muller conditions. In *30th EACSL Annual Conference on Computer Science Logic, CSL 2022*, February 14-19, 2022, Göttingen, Germany (Virtual Conference), volume 216 of LIPICS, pages 12:1-12:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.

[11] Rüdiger Ehlers and Ayrat Khalimov. Fully Generalized Reactivity(1) Synthesis. In Bernd Finkbeiner and Laura Kovács, editors, *TACAS, Tools and Algorithms for the Construction and Analysis of Systems*, volume 14570, pages 83-102, 2024.

[12] Rüdiger Ehlers and Sven Schewe. Natural colors of infinite words. In *Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2022*, volume 250 of LIPICS, pages 36:1-36:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.

[13] E. Mark Gold. Complexity of automaton identification from given data. *Information and Control*, 37(3):302-320, 1978.

[14] Thomas A. Henzinger and Nir Piterman. Solving games without determination. In *Computer Science Logic, 20th International Workshop, CSL 2006, 15th Annual Conference of the EACSL, Szeged, Hungary, September 25-29, 2006, Proceedings*, volume 4207 of Lecture Notes in Computer Science, pages 395-410. Springer, 2006.

[15] John E. Hopcroft and Jeffrey D. Ullman. *Introduction to Automata Theory, Languages, and Computation*. Addison Wesley, 1979.

[16] Nils Klarlund. A homomorphism concepts for omega-regularity. In *Computer Science Logic, 8th International Workshop, CSL '94, Kazimierz, Poland, September 25-30, 1994, Selected Papers*, volume 933 of Lecture Notes in Computer Science, pages 471-485. Springer, 1994.

[17] Denis Kuperberg and Michal Skrzypczak. On Determinisation of Good-for-Games Automata. In Magnus M. Halldorsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann, editors, *Automata, Languages, and Programming*, volume 9135, pages 299-310. Springer Berlin Heidelberg, 2015.

[18] Christof Löding. Efficient minimization of deterministic weak $\omega$-automata. *Information Processing Letters*, 79(3):105-109, 2001.

[19] Damian López and Pedro García. On the inference of finite state automata from positive and negative data. In Sempere J. In: Heinz J., editor, *Topics in Grammatical Inference*. Springer, 2016.

[20] Michael Luttenberger, Philipp J. Meyer, and Salomon Sickert. Practical synthesis of reactive systems from LTL specifications via parity games. *Acta Informatica*, 57(1-2):3-36, 2020.

[21] Oded Maler and Amir Pnueli. On the learnability of infinitary regular sets. *Inf. Comput.*, 118(2):316-326, 1995.

[22] Oded Maler and Ludwig Staiger. On syntactic congruences for $\omega$-languages. *Theoretical Computer Science*, 183(1):93-112, 1997.

[23] Zohar Manna and Amir Pnueli. A hierarchy of temporal properties. In *Proceedings of the Ninth Annual ACM Symposium on Principles of Distributed Computing, Quebec City, Quebec, Canada, August 22-24, 1990*, pages 377-410. ACM, 1990.

[24] Jakub Michaliszyn and Jan Otop. Learning infinite-word automata with loop-index queries. *Artif. Intell.*, 307:103710, 2022.

[25] José Oncina and Pedro García. Identifying regular languages in polynomial time. In *Proceedings of the International Workshop on Structural and Syntactic Pattern Recognition*, volume 5 of Machine Perception and Artificial Intelligence, pages 99-108. World Scientific, 1992.

[26] Bader Abu Radi and Orna Kupferman. Minimization and Canonization of GFG Transition-Based Automata. *Logical Methods in Computer Science*, Volume 18, Issue 3:7587, 2022.

[27] Sven Schewe. Beyond Hyper-Minimisation—Minimising DBAs and DPAs is NP-Complete. In Kamal Lodaya and Meena Mahajan, editors, *IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)*, volume 8 of Leibniz International Proceedings in Informatics (LIPIcs), pages 400-411, Dagstuhl, Germany, 2010. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.

[28] Ludwig Staiger. Finite-state $\omega$-languages. *Journal of Computer and System Sciences*, 27:434-448, 1983.

[29] Wolfgang Thomas. Automata on infinite objects. In *Handbook of Theoretical Computer Science*, volume B: Formal Models and Semantics, pages 133-192. Elsevier Science Publishers, Amsterdam, 1990.

[30] Wolfgang Thomas. Facets of synthesis: Revisiting Church's problem. In *Proceedings of the 12th International Conference on Foundations of Software Science and Computational Structures, FOSSACS 2009*, volume 5504 of Lecture Notes in Computer Science, pages 1-14. Springer, 2009.

[31] Boris A. Trakhtenbrot and Y.M. Barzdin. *Finite Automata: Behavior and Synthesis*. North-Holland Publishing Company, Amsterdam, 1973.

[32] Sicco Verwer and Christian A. Hammerschmidt. Flexfringe: A Passive Automaton Learning Package. In *2017 IEEE International Conference on Software Maintenance and Evolution (ICSME)*, pages 638-642. IEEE, 2017.
# APPENDIX A
## DETAILS ON EXAMPLE 6

Consider the example language $L$ from Example 6. Figure 2 shows the minimal history-deterministic co-Büchi automaton. By component $i$ we refer to the component consisting of the states $q_i^0, q_i^1$. Note that a letter $a_i$ sets the $i$-th component to $q_i^1$, all components $i' < i$ to $q_i^0$, and leaves all other components (with larger index) unchanged. So we can view the automaton as a binary counter where letter $a_i$ is responsible for setting bit $i$ to 1, all bits for $j < i$ to 0, and leaves all other bits unchanged. The condition defining the language says that there is a bit $i$ such that from some point onwards the actions on this bit alternate (setting to 1 and to 0). The words $v_j$ defined by $v_0 = \varepsilon$ and $v_{j+1} := v_j a_j v_j$ in Example 6 correspond to the instruction sequence that counts up from 0 to $2^j - 1$.

We prove the claims from Example 6:

*Claim 1.* 1) $(\varepsilon, v_k)$ visits $2^k$ different SCCs of the $\equiv_L$-graph in the sense that for all prefixes $v \sqsubseteq v' \sqsubseteq v_k$ with $v \neq v'$, we have $(\varepsilon, v) \not\equiv_L (\varepsilon, v'w)$ for all $w$.

2) $(\varepsilon, a_k v_k)$ is the shortest in its $\equiv_L$-class.

*Proof.* Let us first note that $\sim_L$ is trivial, so we can always assume that the first component of pairs is $\varepsilon$. For this reason, we can consider $\equiv_L$ to be a relation on single words instead of pairs by omitting the first component. We first show that for our example language $L$, we have for all $v, v' \in \Sigma^*$:

$$v \equiv_L v' \text{ iff } \theta(v) = \theta(v'). \quad (*)$$

If $\theta(v) = \theta(v')$, then $sf_L(v) = \bigcup_{q \in \theta(v)} L^q(q) = \bigcup_{q \in \theta(v')} L^q(q) = sf_L(v')$, and hence $v \equiv_L v'$. (So this direction holds in general, it does not use any properties of $L$).

For the other direction, assume $\theta(v) \neq \theta(v')$, and wlog. let $q_i^h \in \theta(v) \setminus \theta(v')$ for $i \in \{0, \dots, k\}$ and $h \in \{0, 1\}$. The only state from which there is a rank 2 run on $a_i a_{k+1} a_i a_{k+1}$ is $q_i^0$, and the only state from which there is a rank 2 run on $a_{k+1} a_i a_{k+1}$ is $q_i^1$. Hence, if $h = 0$, then $a_i a_{k+1} a_i a_{k+1} \in sf_L(v) \setminus sf_L(v')$, and if $h = 1$, then $a_{k+1} a_i a_{k+1} \in sf_L(v) \setminus sf_L(v')$, and therefore $v \not\equiv_L v'$. This finishes the proof of (*).

We write $(q_0^0, \dots, q_i^0) \xrightarrow{x:2} (q_0^1, \dots, q_i^1)$ for expressing that $q_j^0 \xrightarrow{x:2} q_j^1$ for each $j \in \{0, \dots, i\}$, so $x$ maps the 0-state to the 1-state for each component $\le i$.

*Proof of second claim:* By induction on $i$, one easily shows that $v_{i+1}$ is the shortest $x$ with $(q_0^0, \dots, q_i^0) \xrightarrow{x:2} (q_0^1, \dots, q_i^1)$. For $i = 0$ we have $v_{i+1} = a_0$, so the claim holds. For $i > 0$, such a word $x$ needs to contain $a_i$. Since $a_i$ has no rank 2 transition on $q_j^0$ for $j < i$, and since $q_j^1 \xrightarrow{a_{i:2}} q_j^0$ for all $j < i$, we obtain that $x$ must be of the form $x_1 a_i x_2$ with $(q_0^0, \dots, q_{i-1}^0) \xrightarrow{x_{1,2:2}} (q_0^1, \dots, q_{i-1}^1)$. By induction, the shortest such word is $v_i a_i v_i = v_{i+1}$.

Now note that $\theta(a_k) = \{q_0^0, \dots, q_{k-1}^0, q_k^1\}$, and $\theta(a_k v_k) = \{q_0^1, \dots, q_{k-1}^1, q_k^1\}$ because $(q_0^0, \dots, q_{k-1}^0) \xrightarrow{v_k:2} (q_0^1, \dots, q_{k-1}^1)$ as explained above. Since every $v$ with $\theta(v) = \{q_0^1, \dots, q_{k-1}^1, q_k^1\}$ needs to contain $a_k$ followed by an $x$ with $(q_0^0, \dots, q_{k-1}^0) \xrightarrow{x:2} (q_0^1, \dots, q_{k-1}^1)$, and since $v_k$ is the

shortest such $x$, we obtain that $a_k v_k$ is indeed the shortest representative of its class.

*Proof of first claim:* We show that claim by showing that if a word $x \in \Sigma^*_{<i}$ for $i \in \{0, \dots, k+1\}$ is such that $\theta(x)$ contains at least one state from each component, then $|x| \le 2^i - 1$. Before proving this, let us first see how the first claim follows from this. We have $v_k \in \Sigma_{<k}$, and from the proof of the second claim we know that $(q_0^0, \dots, q_{k-1}^0) \xrightarrow{v_k:2} (q_1^0, \dots, q_{k-1}^1)$, and thus $\theta(v_k)$ contains a state from each component. Since $\theta(v_k)$ contains both states from component $k$ (because $v_k \in \Sigma_{<k}$), we obtain that for each prefix $v$ of $v_k$, the class $[v]_{\equiv_L}$ only contains words over $\Sigma_{<k}$, and hence only words of length at most $2^k - 1$. If there were $v \sqsubseteq v' \sqsubseteq v_k$ with $v \neq v'$ and $(\varepsilon, v) \equiv_L (\varepsilon, v'w)$ for some $w$, then there is a loop on the class $[v]_{\equiv_L}$, and it would contain words of arbitrary length. So the first claim follows.

For completing the proof, let $x \in \Sigma^*_{<i}$ for $i \in \{0, \dots, k+1\}$ such that $\theta(x)$ contains at least one state from each component. We use induction on $i$. If $i = 0$, then $\Sigma_{<i} = \emptyset$, so $x = \varepsilon$ and the claim holds. If $i > 1$, then $x$ contains the letter $a_{i-1}$ at most once because otherwise $\theta(x)$ would not contain a state from component $i-1$. If $x$ does not contain $a_{i-1}$, then by induction $|x| \le 2^{i-1} - 1$. Otherwise, $x = x_1 a_{i-1} x_2$ with $x_1, x_2 \in \Sigma^*_{<i-1}$, and by induction $|x_1 a_{i-1} x_2| \le 2(2^{i-1} - 1) + 1 = 2^i - 1$. $\square$

# APPENDIX B
## PROOFS FROM SECTION III

For showing that $A_{\equiv_L}$ accepts $L$, we need some auxiliary lemmas. At some moment we need to use the fact that $L$ is accepted by a finite history deterministic automaton. We do this straight away by giving a variant of the definition of $(u, v) \approx_L \perp$ based on a normalized deterministic co-Büchi automaton for $L$. The definition uses a concrete such automaton $D$, but Lemma 36 then shows that it is independent of the choice of $D$.

**Definition 35.** Let $D$ be a normalized deterministic co-Büchi automaton $D$ for $L$. For $(u, v) \in \Sigma^* \times \Sigma^*$, write $(u, v) \approx_D \perp$ if for all $u' \in \Sigma^*$ with $u' \sim_L u$, the run of $D$ on $u'v$ takes a 1-transition on the suffix $v$.

Observe that the definition implies $(u, \varepsilon) \not\approx_D \perp$, for every $u$, because there is no run taking a 1-transition on $\varepsilon$.

**Lemma 36.** $(u, v) \approx_L \perp$ iff $(u, v) \approx_D \perp$.

*Proof.* Assume $(u, v) \not\approx_L \perp$. If $v = \varepsilon$ then $(u, v) \not\approx_D \perp$. Otherwise, let $x \in \Sigma^*$ with $uvx \sim_L u$ and $u(vx)^\omega \in L$. Then $D$ accepts $u(vx)^\omega$ meaning there is a run not visiting 1-transitions after some prefix $u(vx)^i$. Choosing $u' = u(vx)^i$ we get $(u, v) \not\approx_D \perp$.

For the other direction, assume $(u, v) \not\approx_D \perp$. If $v = \varepsilon$ then $(u, v) \not\approx_L \perp$ by definition. Otherwise, let $u'$ be such that $u' \sim_L u$, and the run of $D$ on $u'v$ does not visit a 1-transition on the suffix $v$. So in $D$ there is a run $u' \xrightarrow{u'} q' \xrightarrow{v:2} q$ for some $q, q'$. Since $D$ is normalized, there is $x$ with $q \xrightarrow{x:2} q'$ in $D$. We get $u'(vx)^\omega \in L$ and hence $u(vx)^\omega \in L$ because $u' \sim_L u$.
Moreover, $u'vx \sim_L u'$ because they reach the same state in $\mathcal{D}$.
Hence, $uvx \sim_L u$ too, giving $(u,v) \not\sim_L \perp$.
□

**Lemma 37.** Relation $\equiv_L$ has finitely many equivalence classes.

*Proof.* By Lemma 36, the language $sf_L(u, v)$ only depends on the set of states that are reachable in $\mathcal{D}$ via $u' \sim_L u$ and the states reachable from them by the run on $v$ not using a 1-transition.
□

The following observation is an immediate consequence of the definition of $A_{\equiv_L}$, because the transitions always respect the $\sim_L$-class, and there are all 1-transitions that respect the $\sim_L$-class.

**Lemma 38.** For all pointed pairs $(u, v)$ and $(u', v')$ and all $x \in \Sigma^*$ we have $[u, v]_{\equiv_L} \xrightarrow{x} [u', v']_{\equiv_L}$ iff $uvx \sim_L u'v'$.

The next lemma is an important technical lemma showing that for every pair $(u, v) \not\sim_L \perp$ there is a pointed pair with $v$ as suffix starting in the $\sim_L$-class of $u$.

**Lemma 39.** For all $u, v \in \Sigma^*$ with $(u, v) \not\sim_L \perp$, there are $u_1, u_2 \in \Sigma^*$ with $u_1 u_2 \sim_L u$ and $(u_1, u_2 v)$ pointed.

*Proof.* We first show the following auxiliary claim:

$$sf_L(u_1, u_2 v) \subseteq sf_L(u, v) \text{ for all } u_1, u_2 \in \Sigma^* \text{ with } u_1 u_2 \sim_L u. \quad (3)$$

To see this, let $x \in sf_L(u_1, u_2 v)$, that is, $(u_1, u_2 vx) \not\sim_L \perp$. If $u_2 vx = \varepsilon$, then $x = \varepsilon$ and $\varepsilon \in sf_L(u, v)$ because $(u, v) \not\sim_L \perp$. Otherwise, there is $y$ such that $u_1(u_2 vxy)^\omega \in L$. Then also $u_1 u_2(vxyu_2)^\omega \in L$ and hence $u(vxyu_2)^\omega \in L$ because $u_1 u_2 \sim_L u$. This implies that $x \in sf_L(u, v)$, and thus shows (3).

Going back to the proof of the lemma. If $(u, v)$ is already pointed, then the claim holds by choosing $u_1 = u$ and $u_2 = \varepsilon$.

Otherwise, by definition of pointed, there are $u_{1,1}, u_{1,2}$ with $u_{1,1}u_{1,2} \sim_L u$, $(u_{1,1}, u_{1,2}v) \not\sim_L \perp$, and $sf_L(u_{1,1}, u_{1,2}v) \neq sf_L(u, v)$. By (3), this means that $sf_L(u_{1,1}, u_{1,2}v) \subseteq sf_L(u, v)$. Then $(u_{1,1}, u_{1,2}v) \not\equiv_L (u, v)$ by the definition of $\equiv_L$.

If $(u_{1,1}, u_{1,2}v)$ is not pointed, then we can repeat this argument, obtaining $u_{2,1}, u_{2,2}$ with $u_{2,1}u_{2,2} \sim_L u_{1,1}$, $(u_{2,1}, u_{2,2}u_{1,2}v) \not\sim_L \perp$ and $sf_L(u_{2,1}, u_{2,2}u_{1,2}v) \not\subseteq sf_L(u_{1,1}, u_{1,2}v)$. Since $\equiv_L$ has only finitely many classes (Lemma 37), this construction must terminate after $i$ steps for some $i$, yielding the desired pair $u_1 := u_{i,1}$ and $u_2 := u_{i,2} \cdots u_{1,2}$. □

We now turn to the proof of Proposition 8. We first show that $A_{\equiv_L}$ indeed accepts $L$ (Lemma 40), and then give the more precise characterizations of the languages and the safe languages accepted from the states of $A_{\equiv_L}$ (Lemma 41).

**Lemma 40.** $A_{\equiv_L}$ accepts $L$.

*Proof.* Let $\mathcal{D}$ be a normalized deterministic co-Büchi automaton for $L$, as in Definition 35.

We first show $L(A_{\equiv_L}) \subseteq L$: Let $w \in L(A_{\equiv_L})$. Then there is a pointed pair $(u, v)$ and an index $i$ such that $[u, v]_{\equiv_L}$ is

reachable via $w[0, i]$, and $(u, vw[i+1, k]) \not\sim_L \perp$ for all $k > i$ (here, $w[\cdot, \cdot]$ denotes the infix of $w$ between given positions). By Lemma 36, we have $(u, vw[i+1, k]) \not\sim_D \perp$ for all $k \ge i$. This means that $uvw[i+1, \infty)$ is accepted by $\mathcal{D}$. Since $[u, v]_{\equiv_L}$ is reachable via $w[0, i]$, we have $uv \sim_L w[0, i]$ by Lemma 38, and thus $w = w[0, i]w[i+1, \infty) \in L$.

For the inclusion $L \subseteq L(A_{\equiv_L})$ consider an ultimately periodic word $uv^\omega \in L$. Without loss of generality we can assume $u \sim_L uv$; if not we just prolong $u$ and $v$. We show that $uv^\omega$ is accepted by $L(A_{\equiv_L})$. Let $n$ be bigger than the size of $A_{\equiv_L}$. Clearly $(u, v^n) \not\sim_L \perp$, and by Lemma 39 there is pointed $(u_1, u_2 v^n)$ with $u_1 u_2 \sim_L u$. So there is $x \in \Sigma^*$ with $u_1 u_2 v^n x \sim_L u_1$ such that $u_1(u_2 v^n x)^\omega \in L$. Since $(u_1, u_2 v^n)$ is pointed and $u_1(u_2 v^n x)^\omega \in L$, we get that $(u_1, u_2 v^n y)$ is pointed for all prefixes $y$ of $(xu_2 v^n)^\omega$ by Lemma 5. Thus, by the definition of $A_{\equiv_L}$ we have $[u_1, u_2 v^n x u_2]_{\equiv_L} \xrightarrow{v^n:2} [u_1, u_2 v^n x u_2 v^n]_{\equiv_L}$. Since $n$ is bigger than the size of $A_{\equiv_L}$, there are $i \ge 0$ and $j > 0$ such that $[u_1, u_2 v^n x u_2 v^i]_{\equiv_L} \xrightarrow{j^2:2} [u_1, u_2 v^n x u_2 v^{i+j}]_{\equiv_L}$ with $(u_1, u_2 v^n x u_2 v^i)_{\equiv_L} = (u_1, u_2 v^n x u_2 v^{i+j})$. We have found an accepting run on $uv^\omega$ since $q_{init} \xrightarrow{u} [u_1, u_2 v^n x u_2 v^i]_{\equiv_L}$ by Lemma 38, as $u_1 u_2 v^n x u_2 v^i \sim_L u_1 u_2 v^i \sim_L uv^i \sim_L u$ □

**Lemma 41.** For every state $[u, v]_{\equiv_L}$ of $A_{\equiv_L}$:

$$\bullet L([u, v]_{\equiv_L}) = (uv)^{-1}L,$$

$$\bullet L^f([u, v]_{\equiv_L}) = sf_L(u, v).$$

*Proof.* Consider the first statement. Let $[u, v]_{\equiv_L}$ be a state of $A_{\equiv_L}$. By Lemma 38, $[u, v]_{\equiv_L}$ is reachable by $uv$, and hence $L([u, v]_{\equiv_L}) \subseteq (uv)^{-1}L$. For the other inclusion, let $w \in (uv)^{-1}L$. By Lemma 40, $uvw$ is accepted by $A_{\equiv_L}$. Let $\rho$ be an accepting run of $A_{\equiv_L}$ on $uvw$, and let $[u', v']_{\equiv_L}$ be the state in $\rho$ after $uva$, where $a$ is the first letter of $w$. Then $uva \sim_L u'v'$ by Lemma 38 and the definition of the initial states of $A_{\equiv_L}$. By definition of $A_{\equiv_L}$, there is an $a$-labeled 1-transition from $[u, v]_{\equiv_L}$ to $[u', v']_{\equiv_L}$, so we get an accepting run on $w$ starting in $[u, v]_{\equiv_L}$.

Now we proceed to the second statement. By definition of $A_{\equiv_L}$ we have $[u, v]_{\equiv_L} \xrightarrow{x:2} [u, vx]_{\equiv_L}$ iff $(u, vx) \not\sim_L \perp$. The latter is the definition of $x \in sf_L(u, v)$. □

This finishes the proof of Proposition 8. Below we provide the missing proofs from the part that shows minimality of $A_{\equiv_L}$.

**Lemma 10.** If $L([u, v]_{\equiv_L}) = L([u', v']_{\equiv_L})$ and $L^f([u, v]_{\equiv_L}) = L^f([u', v']_{\equiv_L})$ then $[u, v]_{\equiv_L} = [u', v']_{\equiv_L}$.

*Proof.* This is a direct consequence of Lemma 41, because first, $(uv)^{-1}L = L([u, v]_{\equiv_L}) = L([u', v']_{\equiv_L}) = (u'v')^{-1}L$, which shows $uv \sim_L u'v'$, and second $sf_L(u, v) = L^f([u, v]_{\equiv_L}) = L^f([u', v']_{\equiv_L}) = sf_L(u', v')$, which shows $(u, v) \equiv_L (u', v')$. □

**Lemma 13.** Each state $q$ of $A_{\equiv_L}$ has a central sequence $z_q$.

*Proof.* A state of $A_{\equiv_L}$ is an equivalence class $[u, v]_{\equiv_L}$ of a pointed pair $(u, v)$, in particular $(u, v) \not\sim_L \perp$.
When $v = \varepsilon$ then $(u, v)$ is the unique state recognizing $L([u, v]_{\equiv_L})$. Indeed, if $L([u, v]_{\equiv_L}) = L([u', v']_{\equiv_L})$ then we have $u'v' \sim_L uv$. This gives also $u'v' \sim_L u$, as $v = \varepsilon$. Since $(u, v)$ is pointed wet get $sf_L(u', v') = sf_L(u', v') = sf_L(u, v)$. So $(u, v) \equiv_L (u', v')$. Hence $\varepsilon$ is a central sequence for $[u, v]_{\equiv_L}$.

Now consider the case $v \neq \varepsilon$. Since $(u, v) \not\asymp_L \perp$, there exists $x$ such that $uvx \sim_L u$ and $u(vx)^\omega \in L$. We claim that $xv$ is central for $q = [u, v]_{\equiv_L}$.

Because $u(vx)^\omega \in L$, we have that $(u, vxv) \not\asymp_L \perp$. Thus, since $(u, v)$ is pointed, and $uvx \sim_L u$, we obtain that $(u, vxv) \equiv_L (u, v)$, which means that $[u, v]_{\equiv_L} \xrightarrow{\text{vx}:2} [u, v]_{\equiv_L}$. So the first condition in the definition of central sequence is satisfied.

It remains to show the second condition of the definition of central sequence. Let $[u', v']_{\equiv_L}$ be some state of $A_{\equiv_L}$ that is language equivalent to $[u, v]_{\equiv_L}$. By Lemma 41, this implies that $u'v' \sim_L uv$ and thus $u'v'x \sim_L u$. Hence, again because $(u, v)$ is pointed, we have that either $(u', v'xv) \asymp_L \perp$ or $(u', v'xv) \equiv_L (u, v)$. This shows that $xv$ is central for $q = [u, v]_{\equiv_L}$.

## APPENDIX C
PROOFS FROM SECTION IV

### A. Equivalence $\approx_L$

**Lemma 16.** For $(u, v)$ pointed with $v \neq \varepsilon$, and for arbitrary $x, y \in \Sigma^*$ we have: $(u, vx) \equiv_L (u, vy)$ iff $(u, vx) \approx_L (u, vy)$.

*Proof.* Consider the right-to-left direction. We have $uvx \sim_L uvy$. Take $z \in sf_L(u, vx)$. This means there is $z'$ such that $uvxzz' \sim_L u$ and $(vxzz')^\omega \in L$. By $(u, vx) \approx_L (u, vy)$ we get $u(vyzz')^\omega \in L$, so $z \in sf_L(u, vy)$, and we are done.

For the left-to-right direction, we once again have $uvx \sim_L uvy$. Take $z$ such that $u(vxz)^\omega \in L$ and $uvxz \sim_L u$. Since $(u, v)$ is pointed we have a run in $A_{\equiv_L}: [u, v]_{\equiv_L} \xrightarrow{\text{vx}:2} [u, vx]_{\equiv_L} \xrightarrow{\text{z}:2} [u, vxz]_{\equiv_L} \xrightarrow{\text{vy}:2} [u, vxzv]_{\equiv_L}$. Now from the definition of pointed applied to $(u, v)$ and $uvxz \sim_L u$ we get $sf_L(u, vxzv) = sf_L(u, v)$. This means $[u, vxzv]_{\equiv_L} = [u, v]_{\equiv_L}$, so we have found a loop in $A_{\equiv_L}$ on rank 2 transitions. But since $(u, vx) \equiv_L (u, vy)$ we get $[u, v]_{\equiv_L} \xrightarrow{\text{vy}:2} [u, vy]_{\equiv_L} \xrightarrow{\text{z}:2} [u, vxz]_{\equiv_L} \xrightarrow{\text{vy}:2} [u, vxzv]_{\equiv_L}$, so $u(vyz)^\omega \in L$ as desired.

### B. Components $C(u, v)$ and automaton $A[C]$

**Lemma 17.** If $(u, v)$ is pointed then $C(u, v)$ is isomorphic to the safe SCC of $A_{\equiv_L}$ containing $[u, v]_{\equiv_L}$.

*Proof.* Since $(u, v)$ is pointed, all $(u, vw_i)$ are pointed by Lemma 5. Due to the choice of $w_1, \dots, w_k$ and by Lemma 16, there is a bijection between the states of the safe SCC of $A_{\equiv_L}$ and states of the component. The transitions are defined in the same way for the two.

### C. Idealized learning algorithm

**Lemma 20.** With the notations from Listing 1, suppose $ux^\omega \in L - L(A[C])$ and $ux \sim_L u$. Suppose moreover that $d = \max(\{|C| : C \in C\} \cup \{1\})$. If $(u, x^d v)$ is a pointed

pair extending $(u, x^d)$ then $(u, x^d v) \not\asymp_L (u', v')$ for every $(u', v') \in \bigcup C$.

*Proof.* First we observe that $x^d \not\asymp_L sf_L(u', v')$ for every $(u', v') \in \bigcup C$ with $u \sim_L u'v'$. Indeed, otherwise $A[C]$ would have an accepting run on $ux^\omega$ by the choice of $d$.

Since $(u, x^d v)$ is pointed, $(u, x^d v) \not\asymp_L \perp$. So there is $y$ with $u(x^d vy)^\omega \in L$ and $u \sim_L ux^d vy$. In particular, $yx^d \in sf_L(u, x^d v)$. Suppose to the contrary that $(u, x^d v) \equiv_L (u', v')$ for some $(u', v') \in C$ and $C \in C$. Hence, $yx^d \in sf_L(u', v')$. But then, since $C$ is a component, we have some $(u'', v'') \in C$ with $(u'', v'') \equiv_L (u', v'y)$ in $C$. This means that $x^d \in sf_L(u'', v'')$. Moreover, $u''v'' \sim_L u$ because $u''v'' \sim_L u'v'y$, $u'v' \sim_L ux^d v$ and $ux^d vy \sim_L u$. A contradiction with our observation at the beginning of the proof. $\square$

### D. Finding a new pointed element

**Lemma 24.** $\theta(u, v) = \emptyset$ iff $(u, v) \approx_L \perp$.

*Proof.* Assume that $\theta(u, v) \neq \emptyset$. If $v = \varepsilon$, then $(u, v) \not\asymp_L \perp$ by definition. Otherwise, let $q \in \theta(u, v)$ and $p$ such that there is a run $u \xrightarrow{p} v \xrightarrow{p} q$, and let $x$ be such that $q \xrightarrow{x:2} p$, which exists since $A_{\equiv_L}$ is normalized (Lemma 9). Then $uvx \sim_L u$ and $u(vx)^\omega \in L(A_{\equiv_L}) = L$, and hence $(u, v) \not\asymp_L \perp$.

Now assume that $(u, v) \not\asymp_L \perp$. If $v = \varepsilon$, then $\theta(u, v) \neq \emptyset$ because $A_{\equiv_L}$ is unsafe-saturated (Lemma 9). Otherwise, let $x$ be such that $uvx \sim_L u$ and $u(vx)^\omega \in L$. Then there is a run of the form $u(vx)^i \xrightarrow{p} (vx)^{j:2} \xrightarrow{p} p$ for some $i \geq 0$ and $j \geq 1$. since $u(vx)^i \sim_L u$, we get $u \xrightarrow{p} v \xrightarrow{p} p'$ for some $p'$, and thus $\theta(u, v) \neq \emptyset$. $\square$

**Lemma 25.** $\theta(u, v)$ is a singleton iff $(u, v)$ is pointed.

*Proof.* For the left-to-right direction, if $\theta(u, v)$ is a singleton, then $(u, v) \not\asymp_L \perp$ by Lemma 24. For showing that $(u, v)$ is pointed, take some $u_1u_2 \sim_L u$ with $(u_1, u_2v) \not\asymp_L \perp$. We need to show that $sf_L(u_1, u_2v) = sf_L(u, v)$. Since $\varepsilon$ is in $sf_L$ of every pair that is $\not\asymp_L \perp$, we only need to consider non-empty words below.

First we observe that $sf_L(u_1, u_2v) \subseteq sf_L(u, v)$ without any assumption on $\theta(u, v)$. Indeed, if $x \in sf_L(u_1, u_2v)$ then there is $y$ such that $u_1(u_2vxy)^\omega \in L$ and $u_1u_2vxy \sim_L u_1$. But then $u_1u_2(vxyu_2)^\omega \in L$ and $u_1u_2vxyu_2 \sim_L u_1u_2$. This shows $x \in sf_L(u, v)$ as $u_1u_2 \sim_L u$.

For the other inclusion take $x \in sf_L(u, v)$. Then there is $y$ such that $u(vxy)^\omega \in L$ and $uvxy \sim_L u$. This implies that we have $u \xrightarrow{p} v \xrightarrow{p} q \xrightarrow{xy:2} \text{ for some } p \text{ and } q$. Since $(u_1, u_2v) \not\asymp_L \perp$ we have $u_1 \xrightarrow{p_1} p_1 \xrightarrow{u_2:2} p_2 \xrightarrow{v:2} q_1$ for some $p_1, p_2$ and $q_1$. But since $\theta(u, v)$ is a singleton, and $u_1u_2 \sim_L u$, we conclude that $q_1 = q$. Thus, $x \in sf_L(u_1, u_2v)$ because $u_1 \xrightarrow{p_1} p_1 \xrightarrow{u_2:2} p_2 \xrightarrow{v:2} q \xrightarrow{x:2}$, and $A_{\equiv_L}$ is normalized (Lemma 9).

For the right-to-left direction we suppose $\theta(u, v)$ is not a singleton, and show that $(u, v)$ is not pointed. As $\theta(u, v)$ is not a singleton, in $A_{\equiv_L}$ we have runs:

$$u \xrightarrow{p_1} v \xrightarrow{p_1} q_1 \quad \text{and} \quad u \xrightarrow{p_2} v \xrightarrow{p_2} q_2$$
with $q_1 \neq q_2$. Since $L(q_1) = L(q_2)$ we must have $L^f(q_1) \neq L^f(q_2)$ by Lemma 10. Suppose $z \in L^f(q_1) - L^f(q_2)$. Since $A_{\equiv_L}$ is normalized, there is $z'$ such that $q_1 \xrightarrow{zz':2} q_1$. Take $x = zz'$. We have $(u, vx) \not\asymp_L \perp$ because $p_1 \xrightarrow{vx:2} q_1$. Let $z_{p_2}$ be a central sequence for $p_2$, which exists by Lemma 13. Then $uz_{p_2} \sim_L u$, and $(u, z_{p_2}v) \not\asymp_L \perp$ because $p_2 \xrightarrow{z_{p_2}v:2} q_2$. On the other hand, $(u, z_{p_2}vx) \approx_L \perp$ because for every state $p'$ with $L(p) = u^{-1}L$ we have that either $p' \xrightarrow{z_{p_2}:1} p$ or $p' \xrightarrow{z_{p_2}:2} p_2 \xrightarrow{v:2} q_2 \xrightarrow{z:1} p$. So $sf_L(u, v) \neq sf_L(u, z_{p_2}v)$, hence $(u, v)$ is not pointed. $\square$

The next two Lemmas 26 and 27 deal with the condition of the first while loop in line 4 of FindPointed, see Example 7 for an illustration.

**Lemma 26.** If $(u, v)$ is double-supported then there is $x \in \Sigma^+$ such that $u \sim_L uvx$, $(u, vxv) \not\asymp_L \perp$, and $u(vx)^\omega \notin L$.

*Proof.* If $\theta(u, v)$ is double-supported then there are $p, p' \in \theta(u, v)$ and runs $u \xrightarrow{} p_u \xrightarrow{v:2} p$, $u \xrightarrow{} p'_u \xrightarrow{v:2} p'$, where $p_u, p'_u, p, p'$ are in the same safe SCC of $A_{\equiv_L}$. By Lemma 10 we can assume that there is $y \in \Sigma^+$ with $p \xrightarrow{y:2} q$, for some $q$, and $p' \xrightarrow{y:1} p$. Take any $w$ with $q \xrightarrow{w:2} p'_u$ (by Lemma 9). Consider:

$$ u \xrightarrow{} p_u \xrightarrow{v:2} p \xrightarrow{y:2} q \xrightarrow{z_q:2} q \xrightarrow{w:2} p'_u \xrightarrow{v:2} p' \xrightarrow{y:1} $$

where $z_q$ is a central sequence for $q$, which exists by Lemma 13. Take $x = yz_qw$. We have $u \sim_L uvx$ because there is a run on $uvx$ ending in $p'_u$. We also have $u(vx)^\omega \notin L$ because for every $p''_u$ with $u \xrightarrow{} p''_u$ we have either $p''_u \xrightarrow{vx:1} p''_u \xrightarrow{vx:2} p'_u \xrightarrow{v:2} p'_u \xrightarrow{x:1} p$. $\square$

**Lemma 27.** Suppose $(u, v) \not\asymp_L \perp$, $u \sim_L uv \sim_L uvx$, and $u(vx)^\omega \notin L$. Let $m$ maximal such that $(u, v(xv)^m) \not\asymp_L \perp$. Then $\theta(u, v(xv)^m) \subseteq \theta(u, v)$ and $|\theta(u, v(xv)^m)| \le \frac{1}{m+1}|\theta(u, v)|$.

*Proof.* First note that $m$ is well-defined because we have $(u, v(xv)^0) = (u, v) \not\asymp_L \perp$, and further if $(u, v(xv)^n) \not\asymp_L \perp$ for all $n$, then $A_{\equiv_L}$ would accept $u(vx)^\omega$. Consider:

$$ u \xrightarrow{} P_u \xrightarrow{v:2} Q_0 \xrightarrow{vx:2} Q_1 \xrightarrow{vx:2} \dots \xrightarrow{vx:2} Q_m \xrightarrow{vx:2} Q_{m+1} = \emptyset. $$

Here $P_u = \theta(u, \varepsilon)$ is the set of states $[u', v']_{\equiv_L}$ with $(u', v') \sim_L u$, and $Q_i = \theta(u, v(xv)^i)$ for $i \in \{0, \dots, m+1\}$. Thanks to $u \sim_L uv \sim_L uvx$, we have $Q_i \subseteq P_u$, for all $i$. Further, we get $Q_{i+1} \subseteq Q_i$ as follows. For $i=0$ we have $P_0 \xrightarrow{v:2} Q_0 \xrightarrow{x:2} Q'_0 \subseteq P_u$ because $u \sim_L uvx$, and $Q'_0 \xrightarrow{v:2} Q_1$. This implies $Q_0 \subseteq Q_1$. Then we can proceed by induction because $Q_{i-1} \xrightarrow{vx:2} Q_i \xrightarrow{vx:2} Q_{i+1}$. This shows that $\theta(u, v(xv)^m) = Q_m \subseteq Q_0 = \theta(u, v)$.

For the claim on the size of $\theta(u, v(xv)^m)$, let $R_i = Q_i - Q_{i+1}$, for $i=0, \dots, m$. Since $Q_{m+1} = \emptyset$, we have $Q_m = R_m$ and $R_m \xrightarrow{vx:2} \emptyset$. Then $Q_{m-1} = (Q_{m-1} - Q_m) \cup Q_m = R_{m-1} \cup R_m$ and $R_{m-1} \xrightarrow{vx:2} R_m$. By iterating this reasoning $Q_i = R_i \cup R_{i+1} \cup \dots \cup R_m$, and $R_i \xrightarrow{vx:2} R_{i+1}$.

By 2-determinism we have $|R_i| \ge |R_{i+1}|$. So $|R_m| < \frac{1}{m+1}|Q_0|$ as $Q_0 = R_0 \cup \dots \cup R_m$ and all the $R_i$ are pairwise disjoint. So the claim of the lemma follows from $R_m = \theta(u, v(vw)^m)$ and $Q_0 = \theta(u, v)$. $\square$

The next two Lemmas 42 and 28 deal with the size of a witness for the first while loop in line 4 of FindPointed, whose existence is guaranteed by Lemma 26 for double supported pairs.

**Lemma 42.** Every state of $A_{\equiv_L}$ has a central sequence of size $< \alpha^3$.

*Proof.* As first step, consider a state $q$ that is maximal in a sense that there is no $p$ such that $L(p) = L(q)$ and $L^f(q) \subseteq L^f(p)$. Let $p_1, \dots, p_k$ be an arbitrary enumeration of states such that $L(p_i) = L(q)$. By the choice of $q$, for every $p_i$ there is $y_i$ such that $q \xrightarrow{y_i:2} q'_i$ for some state $q'_i$, and $p_i \xrightarrow{y_i:1} p$. Since $A_{\equiv_L}$ is normalized (Lemma 9), $q$ and $q'_i$ are in the same safe SCC of $A$ so there is $q'_i \xrightarrow{y'_i:2} q$. Taking $z_i = y_iy'_i$ we have $q \xrightarrow{z_i:2} q$ and $p_i \xrightarrow{z_i:1} p$. The length of $y_i$ is at most $\alpha^2$ and the length of $y'_i$ is at most $\alpha - 1$. So the length of $z_i$ is bounded by $\alpha^2 + \alpha - 1$.

Now let us look at our fixed enumeration $p_1, \dots, p_k$. If $z_1$ is central for $q$ then we are done. Otherwise, consider the smallest $i_1$ such that $p_{i_1} \xrightarrow{z_1:2} p'$ for some state $p'$. Observe that by semantic-determinism (Lemma 9), $L(q) = L(p_{i_1}) = L(p')$. Hence, $p' = p_{j_1}$ for some $j_1$. Clearly $i_1 > 1$. If $z_1z_{j_1} \xrightarrow{z_1z_{j_1}:2} p_{j_2}$ is not central, we can find the smallest $i_2$ such that $p_{i_2} \xrightarrow{z_1z_{j_1}:2} p_{j_2}$ for some $j_2$. Clearly $i_2 > i_1$ as $p_{i_1} \xrightarrow{z_1z_{j_1}:1} p'$. Continuing like this we get the required $z_q$. Since we do at most $k$ steps in this construction and $k$ is bounded by $\alpha - 1$ we have that the size of $z_q$ is bounded by $(\alpha - 1)(\alpha^2 + \alpha - 1) = \alpha^3 - 2\alpha + 1$.

In the second step of the construction consider some $q'$ that is not maximal. Hence, there is some $q$ with $L(q') = L(q)$ and $L^f(q') \subseteq L^f(q)$. Choose $q$ such that $L^f(q)$ is maximal for inclusion. By Lemma 10, there is no other $p$ such that $L(p) = L(q)$ and $L^f(q) \subseteq L^f(p)$, hence $q$ is maximal in the sense of the first step, so there is a central sequence $z_q$ for $q$. By Lemma 13 we know that $q'$ has a central sequence $z_{q'}$. Since $L^f(q') \subseteq L^f(q)$ we have $q \xrightarrow{z_q:2} q'$. Since $A_{\equiv_L}$ is normalized (Lemma 9), $q$ and $q'$ are in the same safe SCC of $A$. So we have $q' \xrightarrow{x:2} q \xrightarrow{y:2} q'$ for some $x$ and $y$ with size of $xy$ at most $2\alpha - 2$. It is easy to check that $xz_qy$ is also central for $q'$. Given that the size of $z_q$ is at most $\alpha^3 - 2\alpha + 1$ we get the desired bound $\alpha^3$. $\square$

**Lemma 28.** If there is an $x$ such that $u \sim_L uvx$, $(u, vxv) \not\asymp_L \perp$ and $u(vx)^\omega \notin L$ then there is one of size $< 2\alpha^3$.

*Proof.* We claim that the assumptions of the lemma imply that in $A_{\equiv_L}$ there is the following run for some $i \ge 0$:

$$ u \xrightarrow{} p_u \xrightarrow{(vx)^{i:2}} p \xrightarrow{v:2} q \xrightarrow{x:2} p' \xrightarrow{v:2} q' \xrightarrow{vx:1} $$
The existence of such a run up to $q'$ follows from $(u, vxv) \not\approx_L \bot$. And $i$ can be chosen such that $q' \underset{\xrightarrow{\ xv:1 \to \ }}{\xrightarrow{\ xv:2 \to \ }}$ because $u(vx)^\omega \notin L$.

Since $q \xrightarrow{\ xv:2 \to \ } q'$ and $q' \xrightarrow{\ xv:1 \to \ }$, we can choose a shortest $y$ with this property $q \xrightarrow{y:2} q'$ and $q' \xrightarrow{y:1} p'$, which is of length at most $\alpha^2$. Let further $y'$ be shortest with $q' \xrightarrow{y':2} p'$, which exists since $A_{\equiv_L}$ is normalized (Lemma 9) and is of size $< \alpha$. Then $x' := yz_{q'}y'$ for a central sequence $z_{q'}$ of $q'$ satisfies the claim of the lemma, as argued in the following. Indeed, $u \sim_L uvx'$ because $u \xrightarrow{\ p \to \ } p \xrightarrow{\ v:2 \to \ } q \xrightarrow{\ x':2 \to \ } p'$. The fact $u \xrightarrow{\ p \to \ } p$ follows from $u \xrightarrow{\ p \to \ } p_u \xrightarrow{(vx)^i:2} p$ and $u(vx)^i \sim_L u$. Further, $u \xrightarrow{\ p \to \ } p \xrightarrow{vx:v:2} q'$, so $(u, vxv') \not\approx_L \bot$. Finally, $u(vx')^\omega \notin L$ because for every $p''$ with $u \xrightarrow{\ p'' \to \ } p''$ we have either $p'' \xrightarrow{vy:2} q'' \xrightarrow{z_{q'}:1} \to$, or $p'' \xrightarrow{vy:2} q'' \xrightarrow{y':2} q' \xrightarrow{v:2} p' \xrightarrow{y:1} q' \xrightarrow{\ y:1 \to \ }$.

The existence of $z_{q'}$ and an $\alpha^3$ bound on its size come from Lemma 42. Together with the bounds on $y$ and $y'$ we have $|x'| < 2\alpha^3$. $\square$

Lemma 29 below deals with the condition of the second while loop in line 8 of FindPointed, see explanation after Definition 23, and Example 7 for an illustration.

**Lemma 29.** Suppose $(u, v)$ is single-supported, $uw \sim_L u$, and $(u, wv) \not\approx_L \bot$ is not pointed. There is $x \in \Sigma^+$ such that $u \sim_L uwvx$ and $\bot \not\approx_L (u, wvxx)$ $\not\approx_L$ $(u, wv)$. Moreover, for every such $x$, $\theta(u, wvxx) \subseteq \theta(u, v)$. Additionally, there is such $x$ of size $< 2\alpha^2$.

*Proof.* We first show that $\theta(u, wvxx) \subseteq \theta(u, wv)$ for every $x$ such that $u \sim_L uwvx$. For $q \in \theta(u, wvxx)$ we get $u \xrightarrow{w:2} p \xrightarrow{w:2} q_1 \xrightarrow{v:2} q_2 \xrightarrow{x:2} q_3 \xrightarrow{v:2} q$. By $uw \sim_L u$ we get $q_2 \in \theta(u, v)$, and by $u \sim_L uwvx$ we get $q \in \theta(u, v)$. But since $(u, v)$ is single-supported, $q = q_2$. Since $q_2 \in \theta(u, wv)$ we get $q \in \theta(u, wv)$.

Now we turn to the second statement of the lemma and look for $x$ such that $(u, wvxx) \not\approx_L (u, wv)$. Since $(u, wv)$ is not pointed, $\theta(u, wv)$ is not a singleton, by Lemma 25. So there are two distinct $q, q' \in \theta(u, wv)$. By Lemma 10 we can assume that there is $y$ with $q \xrightarrow{y:2} \to$ and $q' \xrightarrow{y:1} \to$. By normality (Lemma 9) there is $y'$ such that $q \xrightarrow{yy':2} p$, where $p$ is from a run witnessing $q \in \theta(u, wv)$ as follows:

$$u:2 \xrightarrow{\ } p_u \xrightarrow{\ w:2 \to \ } p \xrightarrow{\ v:2 \to \ } q \xrightarrow{\ yy':2 \to \ } p$$

We take $x = yy'$. First, $q \in \theta(u, wvxx)$ so $(u, wvxx) \not\approx_L \bot$. Then $u \sim_L uwvx$ because the run ends in $p$ and $uw \sim_L u$. Finally, we show $\theta(u, wvxx) \neq \theta(u, wv)$ because $q' \in \theta(u, wv)$, but $q' \notin \theta(u, wvxx)$. Suppose $q' \in \theta(u, wvxx)$. Then there is a run $u:2 \xrightarrow{\ p'' \to \ } p_u \xrightarrow{\ w:2 \to \ } p'' \xrightarrow{\ v:2 \to \ } q'' \xrightarrow{\ yy':v:2 \to \ } q'$, for some $p''_u, p''$ and $q''$. This run gives us $q'' \in \theta(u, wv)$. But then $q'' \in \theta(u, v)$, because $uw \sim_L u$. Again using $uw \sim_L u$ and $q' \in \theta(u, wv)$ we also get $q' \in \theta(u, v)$. Since $q'$ and $q''$ are in the same safe SCC of $A_{\equiv_L}$, and $(u, v)$ is single-supported we have $q' = q''$. But then $q' \xrightarrow{yy':v:2} q'$, and this is a contradiction with the fact that $q' \xrightarrow{y:1} \to$.

<table><caption>Listing 5: Finding $NT_{\sim_L}$</caption><tr><td>1</td><td>function Find-NT(R, S):</td></tr><tr><td>2</td><td>NT = ∅</td></tr><tr><td>3</td><td>forevery u ∈ R</td></tr><tr><td>4</td><td>if there is x with ux<sup>ω</sup> ∈ S L and ux<sub>S</sub> u<br>then</td></tr><tr><td>5</td><td>NT := NT ∪ {u}</td></tr><tr><td>6</td><td>return(NT)</td></tr></table>

The size of $y$ is bounded by $\alpha^2$ and the size of $y'$ is bounded by $\alpha - 1$. So the size of $x$ is bounded by $\alpha^2 + \alpha - 1$ that is at most $2\alpha^2$. $\square$

### E. Passive learning algorithm

We provide the missing details for the proof of Theorem 31 by giving implementations for all functions in Listing 3 and showing that there is a stabilizing sample $S$ which is polynomial in the size of $A_{\equiv_L}$, and for which the function computes the right answer.

**Lemma 33.** There is a stabilizing $S$ of size polynomial in $|A_{\equiv_L}|$ such that $R_{\sim_L} = Find-R(S)$. Moreover, the algorithm runs in time polynomial in $S$.

*Proof.* Consider $R_{\sim_L} = \{x_1, \dots, x_k\}$. For every $x_i, x_j \in R_{\sim_L}$ with $i \neq j$ there is $(u_{i,j}, v_{i,j})$ such that $x_i u_{i,j} v_{i,j}^\omega \in L \Leftrightarrow x_j u_{i,j} v_{i,j}^\omega \notin L$. Let $S$ contain information about membership in $L$ of all the pairs in $\{(x_\ell u_{i,j}, v_{i,j}) : \ell \in \{i, j\}, i \neq j, i, j \in \{1, \dots, k\}\}$. This is a set of quadratic size in the number of equivalence classes of $\sim_L$ that in turn is not bigger than the number of states of $A_{\equiv_L}$. Moreover, the size of each word is bounded by the size of $A_{\equiv_L}$.

On the sample $S$, the algorithm returns $R_{\sim_L}$. On every bigger sample it must also return $R_{\sim_L}$ due to the minimality of elements in $R_{\sim_L}$. The algorithm runs in polynomial time because the set $D$ is bounded by the size of $S$. $\square$

Now we consider line 2 of Listing 1 and implement it as a function Find-NT($R, S$) given in Listing 5. The function when called with $R_{\sim_L}$ returns the set $NT_{\sim_L}$ of all $u \in R_{\sim_L}$ such that there is $x$ with $ux^\omega \in_S L$ and $ux \sim_S u$. Thanks to Find-R($S$) we can assume that Find-NT has access to $R_{\sim_L}$, simply because $S$ can be big enough for Find-R to return the correct $R_{\sim_L}$. Then in the rest of the algorithm, the $x \sim_S y$ test that uses $R_{\sim_L}$ is equivalent to the $x \sim_L y$ test.

**Lemma 43.** There is a stabilizing $S$ of size polynomial in $|A_{\equiv_L}|$ such that $NT_{\sim_L} = Find-NT(R_{\sim_L}, S)$. Moreover, the algorithm runs in time polynomial in $S$.

Next, in Listing 6 we construct an automaton for the given set of components. We can use $\sim_S$ tests because we can assume that $R = R_{\sim_L}$. Using this test, the function Automaton simply adds the rank 1 transitions to the components, and defines the initial states. It is clear that this works in polynomial time.
<table><caption>Listing 6: Constructing automaton for C</caption>
  <tr>
    <td>1</td>
    <td>function Automaton(R, C, S):</td>
  </tr>
  <tr>
    <td>2</td>
    <td>Q<sup>A</sup> = &cup;{Q : &lang;Q, &Delta;&rang; &isin; C}</td>
  </tr>
  <tr>
    <td>3</td>
    <td>&Delta;<sub>2</sub><sup>A</sup> = &cup;{&Delta; : &lang;Q, &Delta;&rang; &isin; C}</td>
  </tr>
  <tr>
    <td>4</td>
    <td>&Delta;<sub>1</sub><sup>A</sup> = {(u, v) <sup>a:1</sup> &rarr; (u', v') : a &isin; &Sigma;, (u, v),</td>
  </tr>
  <tr>
    <td>5</td>
    <td>(u', v') &isin; Q<sup>A</sup>, uva &sim;S u'v'</td>
  </tr>
  <tr>
    <td>6</td>
    <td>init = {(u, v) &isin; Q<sup>A</sup> : uv &sim;S &epsilon;}</td>
  </tr>
  <tr>
    <td>7</td>
    <td>return(&lang;Q<sup>A</sup>, &Delta;<sub>1</sub><sup>A</sup> &cup; &Delta;<sub>2</sub><sup>A</sup>, init&rang;)</td>
  </tr>
</table>

<table><caption>Listing 7: Finding $u_i$</caption>
  <tbody>
    <tr>
      <td>1</td>
      <td>function Find-u(A, R, S):</td>
    </tr>
    <tr>
      <td>2</td>
      <td>Let R = {u<sub>1</sub>, ..., u<sub>k</sub>}</td>
    </tr>
    <tr>
      <td>3</td>
      <td>i := 0</td>
    </tr>
    <tr>
      <td>4</td>
      <td>repeat</td>
    </tr>
    <tr>
      <td>5</td>
      <td>i = i + 1</td>
    </tr>
    <tr>
      <td>6</td>
      <td>found:=false</td>
    </tr>
    <tr>
      <td>7</td>
      <td>forevery (u<sub>i</sub>, x) &isin; S L do</td>
    </tr>
    <tr>
      <td>8</td>
      <td>if u<sub>i</sub> x ~S u<sub>i</sub> and u<sub>i</sub> x<sup>&omega;</sup> &notin; L(A) then</td>
    </tr>
    <tr>
      <td></td>
      <td>found:=true</td>
    </tr>
    <tr>
      <td>9</td>
      <td>until found or i = k</td>
    </tr>
    <tr>
      <td>10</td>
      <td>if found then return(u<sub>i</sub>) else return(&#x2213;)</td>
    </tr>
  </tbody>
</table>

The following step is the test in line 6. It is realized by direct inclusion test that is one of the operations that is defined for a given sample. It just requires to iterate over all elements from the sample and to check if the positive examples are accepted by A, and the negative ones are rejected by A, which can be done in polynomial time.

Then finding $u$ from line 7 is realized by the function in Listing 7. It is a simple search for $u_i$ such that there is $(u_i, x) \in_S L$ with $u_i x \sim_S u_i$ and $u_i x^\omega \notin L(A)$.

**Lemma 44.** For every $\mathcal{A}$ there is a stabilizing $S$ of size polynomial in $|\mathcal{A}| + |\mathcal{A}_{\approx_L}|$ such that $u_i = \text{Find}-u(\mathcal{A}, R_{\approx_L}, S)$ is the same as in line 6 of Listing 1. Moreover, $\text{Find}-u(\mathcal{A}, R_{\approx_L}, S)$ runs in time polynomial in the size of $\mathcal{A}$, $R_{\approx_L}$ and $S$.

*Proof.* The algorithm uses only operations that are stable under extension. The for-loop of the algorithm runs in polynomial time as the number of possible $x$ is bounded by the size of $S^+$, and the test $u_i x^\omega \notin L(\mathcal{A})$ is polynomial in $u_i, x$, and $\mathcal{A}$. A sample $S$ that is big enough to have correct $R_{\approx_L}$ and contains some $(u_i, x) \in S^+$ for the $u_i$ from line 6 of the idealized algorithm in Listing 1, gives the correct $u_i$. $\square$

The next step is finding $x$ from line 9. This is the smallest $x$ such that $u_i x \sim_S u_i$ and $u_i x^\omega \notin L(\mathcal{A})$. This is realized by the function in Listing 8.

**Lemma 45.** There is a stabilizing $S$ of polynomial size in $|\mathcal{A}| + |\mathcal{A}_{\approx_L}|$ such that $x = \text{Find}-x(u, \mathcal{A}, R_{\approx_L}, S)$ is as in line 7 of Listing 1, provided that $u$ equals $u_i$ as computed in line 6 of Listing 1. Moreover, $\text{Find}-x(u, \mathcal{A}, R_{\approx_L}, S)$ runs in time polynomial in the size of its arguments.

<table><caption>Listing 8: Finding $x$</caption>
  <tr>
    <td>1</td>
    <td>function Find-x(u, A, R, S):</td>
  </tr>
  <tr>
    <td>2</td>
    <td>D := {y : (u, y) &isin; S, uy &sim; S u}</td>
  </tr>
  <tr>
    <td>3</td>
    <td>x := min{y &isin; D : uy<sup>&omega;</sup> &notin; L(A)}</td>
  </tr>
  <tr>
    <td>4</td>
    <td>return(x)</td>
  </tr>
</table>

<table><caption>Listing 9: Constructing $C(u, v)$</caption>
  <tbody>
    <tr>
      <td>1</td>
      <td>function Construct(u, v, R, S):</td>
    </tr>
    <tr>
      <td>2</td>
      <td>K := {ε}</td>
    </tr>
    <tr>
      <td>3</td>
      <td>repeat</td>
    </tr>
    <tr>
      <td>4</td>
      <td>D := {x : ∀y ∈ K.(u, vx) ≁S (u, vy)}</td>
    </tr>
    <tr>
      <td>5</td>
      <td>if D ≠ ∅ then add min(D) to K</td>
    </tr>
    <tr>
      <td>6</td>
      <td>until D = ∅</td>
    </tr>
    <tr>
      <td>7</td>
      <td>T = {(x, a, y) ∈ K × Σ × K :</td>
    </tr>
    <tr>
      <td>8</td>
      <td>∀z ∈ K. z ≠ y ⇒ (u, vxa) ≁S (u, vz)}</td>
    </tr>
    <tr>
      <td>9</td>
      <td>Q = {(u, vx) : x ∈ K}</td>
    </tr>
    <tr>
      <td>10</td>
      <td>Δ = {(u, vx) <sup>a:2</sup> &rarr; (u, vy) : (x, a, y) ∈ T}</td>
    </tr>
    <tr>
      <td>11</td>
      <td>return(&lang;Q, &Delta;&rang;)</td>
    </tr>
  </tbody>
</table>

*Proof.* The size of $D$ is bounded by the size of $S$. For the algorithm to return the correct answer, it is enough that it has the pair $(u_i, x)$ in $S^+$. $\square$

The $d$ in line 10 of Listing 3 is defined in the same way as in line 8 of Listing 1. Constructing a component $C(u, v)$ from line 10 of Listing 1 is done in line 12 of Listing 3 by the function *Construct* in Listing 9. While its pseudo-code is longer than the others, it is a simple application of the definition using what we have already computed. If the *sample* contains enough distinguishing examples, then the set $K$ that is computed corresponds to $R_{\approx_L}(u, v)$. This is similar to the computation of $R_{\approx_L}$.

The last missing step is the implementation of the function *FindPointed*(*u*, *v*) from Listing 2. Actually it needs only minimal changes to be implemented in the passive setting. The implementation is called *FindPointedInS*(*u*, *v*, *R*, *S*) and is shown in Listing 10. Observe that the two loops run in polynomial time, as they are bounded by the size of *S*. The tests $\sim_S$, $\not\approx_S \perp$, and $\not\approx_S$ used in *FindPointedInS* are stable under extensions, provided that $R = R_{\approx_L}$. Then the arguments from Proposition 30 show that there is a stabilizing *S* of polynomial size in $|\mathcal{A}| + |\mathcal{A}_{\approx_L}|$ allowing to find the new pointed element. It is sufficient to always add the least witnesses to the *sample* that are used in the proof from Proposition 30, together with witnesses that ensure that the required tests for $\sim_L$ and $\not\approx_L$ give the same results as $\sim_S$ and $\not\approx_S$.

This finishes the proof of Theorem 31.
<table><caption>Listing 10: Finding a pointed $(u, w\bar{v})$ extending $(u, v)$</caption><tr><td>1</td><td><strong>function</strong> FindPointedInS(u, v, R, S):</td></tr><tr><td>2</td><td>Assume u ~ S uv.</td></tr><tr><td>3</td><td>Set v&#773; = v.</td></tr><tr><td>4</td><td><strong>while</strong> ∃x s.t. u ~ S u&#773;vx, (u, v&#773;vx) &ne; S ⊥ and<br/>u(v&#773;x)<sup>ω</sup> &notin; S L</td></tr><tr><td>5</td><td>Find the smallest such x.</td></tr><tr><td>6</td><td>v&#773; := v&#773;(x&#773;x)<sup>m</sup>, where m the biggest s.t.,<br/>(u, v&#773;(x&#773;x)<sup>m</sup>) &ne; S ⊥.</td></tr><tr><td>7</td><td>Set w = &epsilon;.</td></tr><tr><td>8</td><td><strong>while</strong> ∃x s.t. u ~ S uw&#773;vx,<br/>(u, w&#773;vx&#773;) &ne; S {⊥, (u, w&#773;})</td></tr><tr><td>9</td><td>Find the smallest such x.</td></tr><tr><td>10</td><td>w := w&#773;vx.</td></tr><tr><td>11</td><td><strong>return</strong> (u, w&#773;)</td></tr></table>