RWTH Aachen University, Ahornstr. 55, 52074 Aachen<EMAIL_ADDRESS>aachen.dehttps://orcid.org/0000-0003-0881-3199 RWTH Aachen University,
Ahornstr. 55, 52074 Aachen<EMAIL_ADDRESS>León Bohn and
Christof Löding [100]Theory of computation—Formal languages and automata
theory—Automata over infinite objects Filippo Bonchi and Simon J. Puglisi 2
46th International Symposium on Mathematical Foundations of Computer Science
(MFCS 2021) MFCS 2021 MFCS 2021 August 23–27, 2021 Tallinn, Estonia 202 64

# Constructing deterministic $\omega$-automata from examples by an extension
of the RPNI algorithm

León Bohn  Christof Löding

###### Abstract

The RPNI algorithm (Oncina, Garcia 1992) constructs deterministic finite
automata from finite sets of negative and positive example words. We propose
and analyze an extension of this algorithm to deterministic $\omega$-automata
with different types of acceptance conditions. In order to obtain this
generalization of RPNI, we develop algorithms for the standard acceptance
conditions of $\omega$-automata that check for a given set of example words
and a deterministic transition system, whether these example words can be
accepted in the transition system with a corresponding acceptance condition.
Based on these algorithms, we can define the extension of RPNI to infinite
words. We prove that it can learn all deterministic $\omega$-automata with an
informative right congruence in the limit with polynomial time and data. We
also show that the algorithm, while it can learn some automata that do not
have an informative right congruence, cannot learn deterministic
$\omega$-automata for all regular $\omega$-languages in the limit. Finally, we
also prove that active learning with membership and equivalence queries is not
easier for automata with an informative right congruence than for general
deterministic $\omega$-automata.

###### keywords:

deterministic omega-automata, learning from examples, learning in the limit,
constructing acceptance conditions, active learning

###### category:

###### Acknowledgements.

##  1 Introduction

In this paper we consider learning problems for automata on infinite words,
also referred to as $\omega$-automata, which have been studied since the early
1960s as a tool for solving decision problems in logic [7] (see also [26]),
and are nowadays used in procedures for formal verification and synthesis of
reactive systems (see, e.g., [5, 27, 18] for surveys and recent work).
Syntactically $\omega$-automata are very similar to NFA resp. DFA (standard
nondeterministic resp. deterministic finite automata on finite words), and
they also share many closure and algorithmic properties. However, many
algorithms and constructions are much more involved for $\omega$-automata, one
prominent such example being determinization [23, 22, 24, 15], and another one
the minimization of deterministic $\omega$-automata [25], which is hard for
most of the acceptance conditions of $\omega$-automata. The underlying reason
is that regular languages of finite words have a simple characterization in
terms of the Myhill/Nerode congruence, and the unique minimal DFA for a
regular language can be constructed by merging language equivalent states (see
[13]). In contrast, deterministic $\omega$-automata need, in general,
different language equivalent states for accepting a given regular
$\omega$-language.

The characterization of minimal DFA in terms of the Myhill/Nerode congruence
is also an important property that is used by learning algorithms for DFA. In
automaton learning one usually distinguishes the two settings of passive and
active learning. We are mainly concerned with passive learning in this paper,
where the task is to construct an automaton from a sample, a given finite set
of words together with a classification if they are in the language or not.
The RPNI algorithm [21] is a passive learning algorithm that constructs a DFA
from a given sample of positive and negative examples (words that are in the
language and words that are not in the language, respectively). It starts with
the prefix tree acceptor, a tree shaped DFA that accepts precisely the
positive examples and subsequently it tries to merge pairs of states in the
canonical order of words (each state is associated with the word reaching it
in the prefix tree acceptor). If a merge results in a DFA that accepts a
negative example, the merge is discarded. Otherwise the merge is kept and the
algorithm continues with this DFA. RPNI can learn the minimal DFA for each
regular language in the limit with polynomial time and data. This means that
RPNI runs in polynomial time in the size of the given sample, and for each
regular language $L$ there is a characteristic sample $S_{L}$ of polynomial
size, such that RPNI produces the minimal DFA for $L$ for each sample that is
consistent with $L$ and contains $S_{L}$ [21]. The RPNI algorithm is a simple
algorithm that also produces useful results if the sample does not include the
characteristic sample of any language $L$. Therefore its principle of state
merging has been used for other automaton models, e.g., probabilistic automata
[8, 17] and sequential transducers [20].

In this paper we propose and analyze an extension of RPNI to
$\omega$-automata. In the setting of infinite words, one uses ultimately
periodic words of the form $uv^{\omega}$ for finite words $u,v$. These are
infinite words with a finite representation, and each regular
$\omega$-language is uniquely determined by the set of ultimately periodic
words that it contains (see [26]). There are two main obstacles that one has
to overcome for a generalization of RPNI. First, it is not clear how to
generalize the prefix tree acceptor to infinite words, since a tree shaped
acceptor for a set of infinite words necessarily needs to be infinite. We
therefore propose a formulation of the algorithm that inserts transitions
instead of merging states, and creates new states in case none of the existing
states can be used as a target of the transition. In the setting of finite
words, this method of inserting transitions produces the same result as RPNI,
and it can easily be used for infinite words as well. Because this algorithm
produces growing transition system, we call it
$\operatorname{\mathsf{Sprout}}$.

The second problem arises in the test whether a merge (in our formulation an
inserted transition) should be kept or discarded. In the case of finite words,
one can simply check whether there are a positive and a negative example that
reach the same state, which obviously is not possible in a DFA that is
consistent with the sample. For $\omega$-automata the situation is a bit more
involved, because acceptance of a word is not determined by a single state,
but rather the set of states that is reached infinitely often. And
furthermore, there are various acceptance conditions using different ways of
classifying these infinity sets into accepting and rejecting. To solve this
problem, we propose polynomial time algorithms for checking whether a
deterministic transition system admits an acceptance condition of a given type
(Büchi, generalized Büchi, parity, or Rabin) that turns the transition system
into a deterministic $\omega$-automaton that is consistent with the sample.
These consistency algorithms are then used in $\operatorname{\mathsf{Sprout}}$
in order to check whether a merge (inserted transition) produces a transition
system that can still be consistent with the sample (for the acceptance
condition under consideration). However, we believe that these consistency
algorithms are of interest on their own and might also be useful in other
contexts. We also show that bounding the size of the acceptance condition can
make the problem hard: consistency with a Rabin condition with three pairs or
generalized Büchi condition with three sets is NP-hard.

Our analysis of $\operatorname{\mathsf{Sprout}}$ reveals that it can learn
every $\omega$-regular language with an informative right congruence (IRC) in
the limit from polynomial time and data. A deterministic $\omega$-automaton
has an informative right congruence if it has only one state for each
Myhill/Nerode equivalence class of the language that it defines [3]. Recently,
another algorithm that can learn every $\omega$-regular language with an IRC
in the limit from polynomial time and data has been proposed [4]. This
algorithm is an extension of the approach from [12] from finite to infinite
words. However, the algorithm from [4] has explicitly been developed for
automata with an IRC, and it can only produce such automata (it defaults to an
automaton accepting precisely the positive examples in case the sample does
not completely characterize the target automaton). In contrast,
$\operatorname{\mathsf{Sprout}}$ is not specifically designed for IRC
languages, it can also construct automata that do not have an IRC. But on the
negative side we also show that $\operatorname{\mathsf{Sprout}}$ cannot learn
a deterministic $\omega$-automaton for every regular $\omega$-language.

The positive results for passive learning of IRC languages raise the question
whether this class is also simpler for active learning than general
deterministic $\omega$-automata. The standard model for active learning of
automata uses membership and equivalence queries, and DFA can be learned in
polynomial time in this model [1]. This approach has been extended to the
class of weak deterministic Büchi automata [16], whose minimal automata can
also be defined using the standard right congruence. For general regular
$\omega$-languages, the only known algorithms either learn a different
representation based on DFA [2], or add another query about the loop structure
of the target automaton [19]. Since the characterization of the minimal
automata by a right congruence is a crucial point in many active learning
algorithms, it is tempting to believe that the algorithms can be extended to
the classes of languages with an IRC. We prove that this is not the case by
showing that a polynomial time active learning algorithm for deterministic
$\omega$-automata with an IRC can be turned into a polynomial time learning
algorithm for general deterministic $\omega$-automata.

Finally, we also make the observation that polynomial time active learning
(with membership and equivalence queries) is at least as hard as learning in
the limit with polynomial time and data.

The paper is structured as follows. In Section 2 we give basic definitions. In
Section 3 we present the consistency algorithms, and in Section 4 we describe
our extension of RPNI to $\omega$-automata. In Section 5 we show that the
property of an IRC does not help for polynomial time active learning, and in
Section 6 we conclude.

##  2 Preliminaries

For a finite alphabet $\Sigma$ we use $\Sigma^{*}$ and $\Sigma^{\omega}$ to
refer to the set of finite and infinite words respectively. The empty word is
denoted by $\varepsilon$, and
$\Sigma^{+}=\Sigma^{*}\setminus\\{\varepsilon\\}$. A deterministic transition
system (TS) is defined by a tuple $\mathcal{T}=(Q,\Sigma,q_{0},\delta)$ where
$Q$ is a finite set of states, $\Sigma$ a finite alphabet, $q_{0}\in Q$ the
initial state and $\delta:Q\times\Sigma\to Q$ is the transition function. We
use $\delta(q,a)=\bot$ to indicate that a transition $(q,a)\in Q\times\Sigma$
is not defined in $\mathcal{T}$. Further we extend $\delta$ to
$\delta^{*}:Q\times\Sigma^{*}\to Q$ defined as $\delta^{*}(q,\varepsilon)=q$
and $\delta^{*}(q,aw)=\delta^{*}(\delta(q,a),w)$ for $q\in Q,a\in\Sigma$ and
$w\in\Sigma^{*}$. Unless otherwise specified $\mathcal{T}$ will be used to
refer to a transition system with components as above. The unique run of
$\mathcal{T}$ on $w\in\Sigma^{\omega}$ is a sequence of transitions
$\rho=q_{0}w_{0}q_{1}w_{1}\dotsc$ with $q_{i+1}=\delta(q_{i},w_{i})$. For an
infinite run $\rho$ we denote by $\operatorname{\mathsf{inf}}(\rho)$ the
_infinity set_ of $\rho$, consisting of all state-symbol pairs that occur
infinitely often in $\rho$. A set of states $\emptyset\neq C\subseteq Q$ is
called _strongly connected_ if for all $p,q\in C$ we have $\delta^{*}(p,w)=q$
for some $w\in\Sigma^{+}$. The $\subseteq$-maximal strongly connected sets of
$\mathcal{T}$ are called strongly connected components (SCCs) and for a set
$R$ we use $\operatorname{\mathsf{SCC}}(R)$ to refer to the set of all SCCs
$S\subseteq R$.

Augmenting a transition system $\mathcal{T}$ with an acceptance condition
$\mathcal{C}$ yields an $\omega$-automaton
$\langle\mathcal{T},\mathcal{C}\rangle=(Q,\Sigma,q_{0},\delta,\mathcal{C})$.
We now introduce different types of acceptance conditions (based on the survey
[26]), give a notion of their size $|\mathcal{C}|$ and define which sets
$X\subseteq Q\times\Sigma$ satisfy them. Note that while acceptance is often
defined based on _states_ that occur infinitely often, we opt for transition-
based acceptance due to its succinctness (state-based acceptance can be turned
into transition-based acceptance without changing the transition system, while
the transformation in the other direction requires a blow-up of the transition
system depending on the acceptance condition).

A _Büchi condition_ $F\subseteq Q\times\Sigma$ is satisfied if $X\cap
F\neq\emptyset$, whereas a _generalized Büchi condition_
$\mathcal{B}=\\{F_{1},\dotsc,F_{k}\\}$ with $F_{i}\subseteq Q\times\Sigma$ is
satisfied if $X\cap F_{i}\neq\emptyset$ for all
$i\in[1,k]\subseteq\mathbb{N}$. The set $X$ satisfies a _parity condition_
$\kappa:(Q\times\Sigma)\to C$ for a finite $C\subseteq\mathbb{N}$ if
$\min(\kappa(X))$ is even where $\kappa(X)=\\{\kappa(q,a):(q,a)\in X\\}$. We
call $\mathcal{R}=\\{(E_{1},F_{1}),\dotsc,(E_{k},F_{k})\\}$ with
$E_{i},F_{i}\subseteq(Q\times\Sigma)$ a _Rabin condition_ and it is satisfied
if $E_{i}\cap X=\emptyset$ and $F_{i}\cap X\neq\emptyset$ for some
$i\in[1,k]\subseteq\mathbb{N}$. Finally a _Muller condition_
$\mathcal{F}\subseteq 2^{Q\times\Sigma}$ is satisfied if $X\in\mathcal{F}$.
For an acceptance condition $\mathcal{C}$ of type
$\Omega\in\\{\text{Parity},\text{generalized Büchi},\text{Rabin}\\}$ we use
$|\mathcal{C}|$ to refer to the number of priorities/recurring sets/Rabin
pairs respectively. We use abbreviations (g)DBA, DPA, DRA to refer to
deterministic (generalized) Büchi, Parity and Rabin automata and introduce a
set $\mathsf{Acc}$ containing these acceptance types. An automaton
$\mathcal{A}=\langle\mathcal{T},\mathcal{C}\rangle$ accepts
$w\in\Sigma^{\omega}$ if $\operatorname{\mathsf{inf}}(\rho)$ satisfies
$\mathcal{C}$, where $\rho$ refers to the unique run of $\mathcal{T}$ on $w$.
The set of all words that are accepted by $\mathcal{A}$ is the language
accepted by $\mathcal{A}$, denoted by $L(\mathcal{A})$.

Let $\sim$ be an equivalence relation over $\Sigma^{*}$. We refer to the
equivalence class of $x$ under $\sim$ as $[x]_{\sim}=\\{y\in\Sigma^{*}:x\sim
y\\}$ and call $\sim$ a (right) _congruence_ if $u\sim v$ implies $ua\sim va$
for all $a\in\Sigma$. A regular language $L\subseteq\Sigma^{\omega}$ induces
the _canonical right congruence_ $\sim_{L}$ in which $u\sim_{L}v$ holds if and
only if $u^{-1}L=v^{-1}L$ with $u^{-1}L=\\{w\in\Sigma^{\omega}:uw\in L\\}$.
Using the terminology of [3], we say that an automaton $\mathcal{A}$ has an
_informative right congruence_ (IRC) if $u\sim_{L(\mathcal{A})}v$ implies that
$\mathcal{A}$ reaches the same state from $q_{0}$ when reading $u$ or $v$. A
language $L$ has an $\Omega$-IRC for $\Omega\in\mathsf{Acc}$ if an
$\Omega$-automaton with an IRC which recognizes $L$ exists and we denote by
$\operatorname{\mathsf{ind}}(L)$ the number of equivalence classes of
$\sim_{L}$.

A word $w\in\Sigma^{\omega}$ is called _ultimately periodic_ if
$w=uv^{\omega}$ with $u\in\Sigma^{*},v\in\Sigma^{+}$. We denote by
$\mathsf{UP}_{\Sigma}$ the set of all ultimately periodic words in
$\Sigma^{\omega}$ and note that two regular languages
$K,L\subseteq\Sigma^{\omega}$ are equal if and only if
$K\cap\mathsf{UP}_{\Sigma}=L\cap\mathsf{UP}_{\Sigma}$ [7]. Note that there
always exists a reduced form $w=uv^{\omega}$ in which $u$ and $v$ are as short
as possible. We call a pair $S=(S_{+},S_{-})$ with
$S_{+},S_{-}\subseteq\mathsf{UP}_{\Sigma}$ and $S_{+}\cap S_{-}=\emptyset$ a
_sample_ and say that $S$ is _in reduced form_ if each $uv^{\omega}\in S$ is
in a reduced form where $w\in S$ is used as a shorthand for $w\in S_{+}\cup
S_{-}$. For $L\subseteq\Sigma^{\omega}$ we say that $S$ is consistent with $L$
if $S_{+}\subseteq L$ and $S_{-}\cap L=\emptyset$. Similarly an automaton
$\mathcal{A}$ is consistent with $S$ if $S_{+}\subseteq L(\mathcal{A})$ and
$S_{-}\cap L(\mathcal{A})=\emptyset$.

For $\Omega\in\mathsf{Acc}$ we call a function $f$ that maps a sample to an
$\Omega$-automaton a _passive learner_. $f$ is called _consistent_ if for any
sample $S$ the constructed automaton $f(S)$ is consistent with $S$. A sample
$S_{L}$ is _characteristic_ for $L$ and $f$ if for any sample $S$ that is
consistent with $L$ and that contains $S_{L}$, the learner produces an
automaton $f(S)$ recognizing $L$. For a class of representations of languages
$\mathbb{C}$ (in our case deterministic $\omega$-automata) we use
$\mathcal{L}(\mathbb{C})$ to refer to the represented languages and define the
size of $L\in\mathcal{L}(\mathbb{C})$ to be the size of the minimal
representation of $L$ in $\mathbb{C}$. Based on the definition in [10] we say
$\mathbb{C}$ is _learnable in the limit using polynomial time and data_ if
there exists a learner $f$ that runs in polynomial time for any input sample,
and for each $L\in\mathcal{L}(\mathbb{C})$ there exists a characteristic
sample whose size is polynomial in the size of $L$.

We call $w\in\Sigma^{\omega}$ _escaping_ from $p\in Q$ with $a\in\Sigma$ in
$\mathcal{T}$ if there exists a decomposition $w=uav$ with
$v\in\Sigma^{\omega}$ such that $\delta^{*}(q_{0},u)=p$ and
$\delta(p,a)=\bot$. We refer to $ua$ as the _escape-prefix_ and call $av$ the
_exit string_ of $w$. Two escaping words $w_{1},w_{2}$ are _indistinguishable_
if they escape $\mathcal{T}$ from the same state and their exit strings
coincide. We call $\mathcal{T}$ $\Omega$-_consistent_ with a sample $S$ if
there exists an $\Omega$-acceptance condition $\mathcal{C}$ such that $\\{w\in
S_{+}:w\text{ not escaping in }\mathcal{T}\\}\subseteq
L(\mathcal{T},\mathcal{C}),S_{-}\cap L(\mathcal{T},\mathcal{C})=\emptyset$ and
no pair of sample words from $S_{+}\times S_{-}$ is indistinguishable. Note
that $\Omega$-consistency with a transition system does not require all words
from $S_{+}$ to have an infinite run in the transition system. It just means
that $\mathcal{T}$ does not produce any conflicts between words in $S_{+}$ and
in $S_{-}$. In contrast, for an automaton to be considered consistent with $S$
it is required that all words from $S_{+}$ are accepted.

##  3 Consistency Algorithms

The algorithm for learning $\omega$-automata that we describe in Section 4
constructs a transition system and then tests whether an acceptance condition
can be found such that all sample words are accepted and rejected accordingly.
In this section we develop algorithms for this test, so we assume that a
transition system $\mathcal{T}=(Q,\Sigma,q_{0},\delta)$ is given. We do not
work with the sample directly in this section, and rather work with the
infinity sets induced by the sample words. This leads to the notion of a
partial condition, which we define below. Then we investigate how different
types of acceptance conditions that are consistent with such a partial
condition can be constructed.

Recall that a Muller condition $\mathcal{F}\subseteq 2^{Q\times\Sigma}$ is
satisfied by an infinity set $X\subseteq Q\times\Sigma$ if and only if
$X\in\mathcal{F}$. Instead of specifying such a Muller condition based solely
on the infinity sets that satisfy it, we can also define it as a partition
$\mathcal{F}=(\mathcal{F}_{0},\mathcal{F}_{1})$ of $2^{Q\times\Sigma}$ into
accepting and rejecting sets, in the following also referred to as positive
and negative sets respectively. In other words such a condition assigns to
each possible set $X\subseteq Q\times\Sigma$ a _classification_
$\sigma\in\\{0,1\\}$, which we denote as $\mathcal{F}(X)=\sigma$ for
$X\in\mathcal{F}_{\sigma}$. Note that any acceptance condition $\mathcal{C}$
can be viewed as a Muller condition
$(\mathcal{F}^{\mathcal{C}}_{0},\mathcal{F}^{\mathcal{C}}_{1})$ by assigning
to $\mathcal{F}^{\mathcal{C}}_{0}$ exactly those sets $X\subseteq
Q\times\Sigma$ that satisfy $\mathcal{C}$ and defining
$\mathcal{F}^{\mathcal{C}}_{1}$ to contain all others.

To incorporate the fact that the infinity sets induced by sample words might
not classify all subsets of $Q\times\Sigma$, we introduce the concept of a
_partial condition_ $\mathcal{H}=(\mathcal{H}_{0},\mathcal{H}_{1})$ with
$\mathcal{H}_{0},\mathcal{H}_{1}\subseteq 2^{Q\times\Sigma}$ in which only a
subset of all elements $X\subseteq Q\times\Sigma$ receives a classification
$\mathcal{H}(X)\in\\{0,1\\}$. We use $X\in\mathcal{H}$ to denote
$X\in\mathcal{H}_{0}\cup\mathcal{H}_{1}$ and call a partial condition
$\mathcal{H}=(\mathcal{H}_{0},\mathcal{H}_{1})$ _consistent_ if
$\mathcal{H}_{0}\cap\mathcal{H}_{1}=\emptyset$. A component
$\mathcal{H}_{\sigma}$ of a partial condition is called _union-closed_ if for
any finite collection $X_{1},\dotsc,X_{n}\in\mathcal{H}_{\sigma}$ we have
$X_{1}\cup\dotsc\cup X_{n}\notin\mathcal{H}_{1-\sigma}$ or in other words the
union of positive sets is not negative and vice versa. We call an acceptance
condition $\mathcal{C}$ _consistent with_ a partial condition
$\mathcal{H}=(\mathcal{H}_{0},\mathcal{H}_{1})$ if
$\mathcal{H}_{0}\subseteq\mathcal{F}^{\mathcal{C}}_{0}$ and
$\mathcal{H}_{1}\subseteq\mathcal{F}^{\mathcal{C}}_{1}$.

For each $\Omega\in\mathsf{Acc}$ we can now define the decision problem
$\Omega$-Consistency: Given a transition system
$\mathcal{T}=(Q,\Sigma,q_{0},\delta)$ and a partial condition
$\mathcal{H}=(\mathcal{H}_{0},\mathcal{H}_{1})$ with
$\mathcal{H}_{0},\mathcal{H}_{1}\subseteq 2^{Q\times\Sigma}$, the question is
whether there exists an acceptance condition $\mathcal{C}$ of type $\Omega$
over $Q\times\Sigma$ that is consistent with $\mathcal{H}$. In the following
we provide algorithms that decide $\Omega\textsc{-consistency}$ for the
various acceptance types we introduced and investigate their complexity.

#### Büchi and generalized Büchi conditions

For a Büchi condition $F\subseteq Q\times\Sigma$ we know that every superset
of some $X\subseteq Q\times\Sigma$ with $X\cap F\neq\emptyset$ clearly has a
non-empty intersection with $F$. Based on this observation we can define an
algorithm that computes for a given partial condition
$\mathcal{H}=(\mathcal{H}_{0},\mathcal{H}_{1})$ a Büchi condition $F$ which is
consistent with $\mathcal{H}$. We forego a formal definition of the algorithm
itself and instead define the partial function it computes, where a result of
$\bot$ is used to indicate that no Büchi condition exists that is consistent
with $\mathcal{H}$.

$\operatorname{\mathsf{BuchiCons}}(\mathcal{H}_{0},\mathcal{H}_{1})=\begin{cases}\texttt{return
}\bot&\text{ if }P\in\mathcal{H}_{0}\text{ exists with
}P\subseteq\bigcup\mathcal{H}_{1}\\\ \texttt{return
}(Q\times\Sigma)\setminus\bigcup\mathcal{H}_{1}&\text{ otherwise}\end{cases}$

It is easily verified that $\operatorname{\mathsf{BuchiCons}}$ is computable
in polynomial time and a formal proof for the correctness of this algorithm
can be found in the appendix.

With generalized Büchi conditions it is no longer guaranteed that the union of
two negative sets $N,N^{\prime}\in\mathcal{H}_{1}$ is also negative. Consider
a generalized Büchi condition $\mathcal{B}=\\{F,F^{\prime}\\}$ such that $N$
has a non-empty intersection with $F$ but not with $F^{\prime}$, whereas
$N^{\prime}\cap F=\emptyset$ and $N^{\prime}\cap F^{\prime}\neq\emptyset$.
Then their union $F\cup F^{\prime}$ has a non-empty intersection with both $F$
and $F^{\prime}$ and hence satisfies $\mathcal{B}$. Therefore we first isolate
the $\subseteq$-maximal sets $N_{1},\dotsc,N_{k}$ in $\mathcal{H}_{1}$. As
before we give a function

$\operatorname{\mathsf{genBuchiCons}}(\mathcal{H}_{0},\mathcal{H}_{1})=\begin{cases}\texttt{return
}\bot&\text{ if }P\in\mathcal{H}_{0}\text{ with }P\subseteq N_{i}\text{
exists}\\\ \texttt{return }\\{(Q\times\Sigma)\setminus N_{i}:i\leq k\\}&\text{
otherwise}\end{cases}$

which maps a partial condition to a generalized Büchi condition that is
consistent with $\mathcal{H}$ or $\bot$ if no such condition exists. It is
again not difficult to see that an algorithm can compute
$\operatorname{\mathsf{genBuchiCons}}$ in polynomial time. A formal proof of
the correctness of $\operatorname{\mathsf{genBuchiCons}}$ can be found in the
appendix.

######  Theorem 3.1.

The algorithm $(\textsf{gen})\textsf{BuchiCons}$ decides the (generalized)
Büchi-Consistency problem in polynomial time and returns a corresponding
acceptance condition if one exists.

#### Parity Conditions

It is a well-known observation that for a given Muller condition
$(\mathcal{F}_{0},\mathcal{F}_{1})$ there exists an equivalent parity
condition $\kappa$ if and only if $\mathcal{F}_{0}$ and $\mathcal{F}_{1}$ are
union-closed [28]. We show an analogous statement for partial conditions,
starting with the following lemma which establishes that if the union of
positive and negative elements coincide, then no equivalent parity condition
can be found.

######  Lemma 3.2.

Let $\mathcal{H}=(\mathcal{H}_{0},\mathcal{H}_{1})$ be a consistent partial
condition. If we have $P=N$ for $P=P_{1}\cup\dotsc\cup P_{k}$ and
$N=N_{1}\cup\dotsc\cup N_{l}$ with $P_{i}\in\mathcal{H}_{0}$ and
$N_{j}\in\mathcal{H}_{1}$ then there exists no parity condition that is
consistent with $\mathcal{H}$

It turns out that the opposite direction also holds, meaning if no such unions
of positive and negative sets can be found, then an equivalent parity
condition must exist. This implication arises as a consequence of the
$\operatorname{\mathsf{ParityCons}}$ algorithm we present later together with
the proofs of its correctness. For a given partial condition
$\operatorname{\mathsf{ParityCons}}$ (see algorithm 1) attempts to construct a
chain of sets of transitions $Z_{0}\supseteq Z_{1}\supseteq\dotsc\supseteq
Z_{n-1}$ with alternating classifications $\sigma_{i}\in\\{0,1\\}$, i.e.,
$\sigma_{i+1}=1-\sigma_{i}$ for $i<n-1$. We refer to this as a _Zielonka path_
because it corresponds to the Split or Zielonka tree representation of a
parity condition [28, 11].

$\\{\tau_{1},\tau_{2},\tau_{3},\tau_{4},\tau_{5},\tau_{6},\tau_{7}\\}$$\\{\tau_{1},\tau_{2},\tau_{3},\tau_{4}\\}$$\\{\tau_{4},\tau_{5},\tau_{6},\tau_{7}\\}$$\\{\tau_{1},\tau_{2}\\}$$\\{\tau_{2},\tau_{3},\tau_{4}\\}$$\\{\tau_{4},\tau_{5},\tau_{7}\\}$$\\{\tau_{4},\tau_{6},\tau_{7}\\}$$\\{\tau_{1}\\}$$\\{\tau_{2},\tau_{3}\\}$$\\{\tau_{5}\\}$$\\{\tau_{4},\tau_{6}\\}$

$\\{\tau_{1},\tau_{2},\tau_{3},\tau_{4},\tau_{5},\tau_{6},\tau_{7}\\}$$\\{\tau_{1},\tau_{2},\tau_{3},\tau_{4},\tau_{5},\tau_{6}\\}$$\\{\tau_{1},\tau_{2},\tau_{3},\tau_{4}\\}$$\\{\tau_{1},\tau_{2},\tau_{3}\\}$$\\{\tau_{1},\tau_{2}\\}$$\\{\tau_{1}\\}$

Figure 1: On the left an inclusion graph for the partial condition
$\mathcal{H}$ from 3.3 can be seen in which positive elements are depicted
with rounded and negative ones with rectangular borders. The path depicted on
the right corresponds to a priority function $\kappa$ with domain
$\\{0,1,2,3,4,5\\}$ such that $\tau_{7}\mapsto 0,\tau_{6}\mapsto
1,\tau_{5}\mapsto 1,\tau_{4}\mapsto 2,\tau_{3}\mapsto 3,\tau_{2}\mapsto
4,\tau_{1}\mapsto 5$ which is the minimal parity condition that is consistent
with $\mathcal{H}$.

From such a Zielonka path one obtains a parity condition $\kappa$ where
$\kappa(q,a)=\sigma_{0}+i$ for the maximal $i$ such that $(q,a)\in Z_{i}$. On
the other hand every parity condition $\kappa$ with priorities $C$ determines
a chain $Z_{0}\supseteq Z_{1}\supseteq\dotsc\supseteq Z_{|C|-1}$ and
alternating classifications $\sigma_{i}$ where $\sigma_{0}=\min(C)\bmod 2$,
$\sigma_{i+1}=1-\sigma_{i}$ and $Z_{i}$ contains all state-symbol pairs whose
color is greater or equal to $\sigma_{0}+i$. To guarantee the existence of
such an alternating chain, we assume that $\kappa$ is optimal and contains no
gaps, which can be ensured in polynomial time [9].

######  Example 3.3.

As an example consider a partial condition
$\mathcal{H}=(\mathcal{H}_{0},\mathcal{H}_{1})$ with set inclusion diagram as
shown on the left of Figure 1, where $\mathcal{H}_{0}$ contains the transition
sets drawn with rounded border, and $\mathcal{H}_{1}$ those with rectangular
border (the leaves of the tree, in this example). We assume an underlying
transition system in which the transition sets in $\mathcal{H}$ are strongly
connected. It is easily verified that $\mathcal{H}$ does not satisfy the
condition of 3.2. Since we claimed the converse of 3.2 to be true, a parity
condition that is consistent with $\mathcal{H}$ should exist. It turns out
that such a parity condition requires $6$ distinct priorities (the
corresponding Zielonka path is shown on the right of Figure 1) even though
there is at most one alternation between positive and negative sets along
inclusion chains in $\mathcal{H}$. This is due to the fact that more
alternations are introduced by unions of positive and negative sets.

We now present an algorithm that given a consistent partial condition
$\mathcal{H}$ over $Q\times\Sigma$ constructs an equivalent parity condition
with the least number of distinct priorities if one exists. As a
simplification we assume that the set $Q\times\Sigma$ of all transitions is
classified by $\mathcal{H}$, which enables us to use $Q\times\Sigma$ as the
first set $Z_{0}$ of the chain that is constructed. We describe later how
partial conditions that do not satisfy this assumption can be dealt with.

Input: A consistent partial condition
$\mathcal{H}=(\mathcal{H}_{0},\mathcal{H}_{1})$ with
$Q\times\Sigma\in\mathcal{H}$

Output: A Zielonka path
$(Z_{0},\sigma_{0}),(Z_{1},\sigma_{1}),\dotsc,(Z_{n-1},\sigma_{n-1})$

$Z_{0}\leftarrow Q\times\Sigma$,
$\sigma_{0}\leftarrow\mathcal{H}(Q\times\Sigma)$, $i\leftarrow 0$

repeat

$i\leftarrow i+1$

$Z\leftarrow\bigcup\\{X\subseteq Z_{i-1}:\mathcal{H}(X)=1-\sigma_{i-1}\\}$

if  _$Z=Z_{i-1}$_ then

return _No consistent parity condition exists._

$Z_{i}\leftarrow Z$, $\sigma_{i}\leftarrow 1-\sigma_{i-1}$

until  _$Z=\emptyset$_

return _$(Z_{0},\sigma_{0}),\dotsc,(Z_{i-1},\sigma_{i-1})$_

Algorithm 1 $\operatorname{\mathsf{ParityCons}}$

After $Z_{0}$ and its corresponding classification
$\sigma_{0}=\mathcal{H}(Z_{0})$ have been determined, the algorithm computes
$Z_{1}$ as the union of all $1-\sigma_{0}$ subsets of $Z_{0}$. If this union
coincides with $Z_{0}$ then the conditions for 3.2 are met and the algorithm
terminates prematurely as no equivalent parity condition can exist. Otherwise
this construction ensures that every strict superset of $Z_{1}$ receives the
same classification as $Z_{0}$ from the constructed parity condition. This
process is then repeated for $Z_{1}$ with $\sigma_{1}=1-\sigma_{0}$, $Z_{2}$
with $\sigma_{2}=1-\sigma_{1}$ and so on until no subsets of opposite
classification remain. At this point the algorithm terminates and returns the
constructed chain of sets of transitions together with their corresponding
classification.

Proving the correctness of this approach forms the opposite direction of 3.2
as it entails that if no union of positive and negative sets as in 3.2 is
found, an equivalent parity condition can be constructed. One restriction on
the partial conditions that can be passed to
$\operatorname{\mathsf{ParityCons}}$ is that the set of all transitions,
$Q\times\Sigma$, must be present in either $\mathcal{H}_{0}$ or
$\mathcal{H}_{1}$. As these partial conditions arise from the infinity sets
that words from a finite sample induce, however, it is easily conceivable that
there are many scenarios - for example when the automaton that we want to
learn is made up of multiple SCCs - in which no word inducing $Q\times\Sigma$
exists. In this case we can simply define two extended partial conditions
$\mathcal{H}^{p}$ and $\mathcal{H}^{n}$ in which $Q\times\Sigma$ is added as a
positive or negative set respectively and execute
$\operatorname{\mathsf{ParityCons}}$ separately for each of them. If only one
computation results in a Zielonka path we are done, otherwise the two
resulting paths are compared with regard to their length and the longer one is
discarded.

######  Theorem 3.4.

$\operatorname{\mathsf{ParityCons}}$ decides Parity-Consistency in polynomial
time and returns a corresponding parity condition with a minimal number of
priorities if one exists.

######  Proof 3.5 (Proof (sketch)).

We proceed in two steps and first show that the classification obtained by the
Zielonka path computed by $\operatorname{\mathsf{ParityCons}}$ are indeed
consistent with the original partial condition. Subsequently one shows that if
the computation exits prematurely, then there exist positive and negative sets
whose unions coincide, which by 3.2 means that no equivalent parity condition
exists.

#### Rabin Conditions

We now turn towards computing an equivalent Rabin condition based on a given
partial condition, for which we again utilize an observation about union-
closedness. Specifically, a Muller condition is equivalent to a Rabin
condition if and only if $\mathcal{F}_{1}$ is union-closed [28]. The algorithm
$\operatorname{\mathsf{RabinCons}}$ (see algorithm 2) computes for each
positive set $P$ in $\mathcal{H}$ a separate Rabin pair $(E_{P},F_{P})$ in
which each transition that is not part of $P$ belongs to $E_{P}$ and every
transition which does not occur in a negative subloop of $P$ belongs to
$F_{P}$. In case a positive loop is equal to the union of its maximal negative
subloops, no equivalent Rabin condition can be found as the condition on
union-closedness outlined above is violated.

Input: A consistent partial condition
$\mathcal{H}=(\mathcal{H}_{0},\mathcal{H}_{1})$

Output: A Rabin condition $\mathcal{R}$ consistent with $\mathcal{H}$

$\mathcal{R}\leftarrow\emptyset$

foreach  _$P\in\mathcal{H}_{0}$_ do

$N_{1},\dotsc,N_{k}\leftarrow$ maximal sets in
$\mathcal{P}(P)\cap\mathcal{H}_{1}$

$E_{P}\leftarrow(Q\times\Sigma)\setminus P$

$F_{P}\leftarrow P\setminus(N_{1}\cup\dotsc\cup N_{k})$

if  _$F_{P}=\emptyset$_ then

return _No consistent Rabin condition exists_

$\mathcal{R}\leftarrow\mathcal{R}\cup\\{(E_{P},F_{P})\\}$

return _$\mathcal{R}$_

Algorithm 2 $\operatorname{\mathsf{RabinCons}}$

######  Theorem 3.6.

The algorithm $\operatorname{\mathsf{RabinCons}}$ decides Rabin-Consistency in
polynomial time and returns a corresponding Rabin condition if one exists.

A Rabin condition produced by $\operatorname{\mathsf{RabinCons}}$ has
$|\mathcal{H}_{0}|$ pairs and is not guaranteed to have the minimal number of
pairs. Even though it is possible to find optimizations which might make use
of the underlying structure with regard to strongly connected components and
subset relations between positive and negative loops, we now illustrate why
the computation of an optimal Rabin condition (with a minimal number of pairs)
is NP-hard.

#### Fixed-size consistency

For each acceptance type $\Omega\in\\{\text{generalized
Büchi},\text{Parity},\text{Rabin}\\}$ and every natural number
$k\in\mathbb{N}$ we define the decision problem $k$-$\Omega$-Consistency:
Given a transition system $\mathcal{T}$ and a consistent partial condition
$\mathcal{H}$ the question is whether there is an acceptance condition
$\mathcal{C}$ of type $\Omega$ in $\mathcal{T}$ which is consistent with
$\mathcal{H}$ such that $|\mathcal{C}|\leq k$. The algorithm
$\operatorname{\mathsf{ParityCons}}$ we provided earlier decides $k$-Parity-
Consistency in polynomial time, however finding a Rabin or generalized Büchi
condition of bounded size turns out to be much more difficult.

Intuitively, the difficulty in finding an optimal generalized Büchi condition
with at most $k$ components arises from the fact that the union of two
negative sets is not necessarily guaranteed to also be negative. As there are
in general exponentially many possible ways of partitioning the transitions
into $k$ sets, a procedure for constructing an optimal generalized Büchi
condition would need to consider all of them. In the following we establish
that the fixed-size consistency problem for generalized Büchi conditions is
already NP-complete when $k=3$. This is done by giving a reduction from
$3$-Coloring for directed graphs, which is known to be NP-complete [14].

$0$$1$$1$$2$$2$$3$$3$$4$$4$$5$$5$$\dotsc$$n$$n$ Figure 2: This figure contains
a depiction of the transition system $\mathcal{T}_{\mathcal{G}}$, which can be
used to show NP-completeness of $k$-generalized Büchi-Consistency and
$k$-Rabin-Consistency.

######  Lemma 3.7.

$3$-generalized Büchi-Consistency is NP-complete.

######  Proof 3.8.

Let $\mathcal{G}=(V,E)$ be a finite directed graph with
$V=\\{v_{1},v_{2},\dotsc,v_{n}\\}$. We define the deterministic partial
transition system

$\mathcal{T}_{\mathcal{G}}=(\\{0,1,2,\dotsc,n\\},\\{1,2,\dotsc,n\\},0,\delta)\text{
with }\delta(q,a)=\begin{cases}a\text{ if }q=0\\\ 0\text{ if }q=a\\\
\bot\text{ otherwise}\end{cases}$

which is depicted in Figure 2. Note that it is possible to construct an
equivalent transition system over a binary alphabet
$\Sigma^{\prime}=\\{a,b\\}$ by encoding $i\in\Sigma$ as $a^{i}b$. Thus our
choice of $\Sigma$ depending on the size of the graph merely serves to
simplify notation in the following. We define a sample
$S_{\mathcal{G}}=(P_{\mathcal{G}},N_{\mathcal{G}})$ with

$P_{\mathcal{G}}=\\{p_{ij}:(v_{i},v_{j})\in E\\}\text{ and
}N_{\mathcal{G}}=\\{n_{i}:0<i\leq n\\}\text{ where
}p_{ij}=(iijj)^{\omega},n_{i}=i^{\omega}$

In the following we use $\bar{p_{ij}}$ and $\bar{n_{i}}$ to refer to the
infinity set of the unique run of $\mathcal{T}_{\mathcal{G}}$ on $p_{ij}$ and
$n_{i}$ respectively. Let $c:V\to\\{1,2,3\\}$ be a 3-coloring for $V$ such
that $c(v_{i})\neq c(v_{j})$ for all $(v_{i},v_{j})\in E$. We construct a
generalized Büchi condition $\mathcal{B}_{\mathcal{G}}=(F_{1},F_{2},F_{3})$
with $F_{k}=\\{i:c(v_{i})\neq k\\}$, witnessing membership in $3$-generalized
Büchi-Consistency. For all $i\leq n$ we have for $k=c(v_{i})$ that
$\bar{n_{i}}\cap F_{k}=\\{0,i\\}\cap F_{k}=\emptyset$ and thus $n_{i}\notin
L(\mathcal{T},\mathcal{B}_{\mathcal{G}})$. On the other hand $\bar{p_{ij}}\cap
F_{k}=\\{0,i,j\\}\cap F_{k}\neq\emptyset$ for all $k$ as $c(v_{i})\neq
c(v_{j})$ is guaranteed for all $(v_{i},v_{j})\in E$ by the coloring function
$c$. Hence $p_{ij}\in L(\mathcal{T},\mathcal{B}_{\mathcal{G}})$ and the
constructed condition is indeed consistent with the sample.

For the other direction assume that there exists a generalized Büchi condition
$\mathcal{B}=(F_{1},F_{2},F_{3})$ such that
$\langle\mathcal{T},\mathcal{B}\rangle$ is consistent with $S$. Clearly it
must hold that $F_{1}\cap F_{2}\cap F_{3}=\emptyset$ as otherwise there would
exist some word $n_{i}\in N_{\mathcal{G}}$ with $\bar{n_{i}}\cap
F_{k}=\\{0,i\\}\cap F_{k}\neq\emptyset$ for all $k$, which would contradict
consistency with $S$. We can now define a coloring $c:V\to\\{1,2,3\\}$ with
$c(v_{i})=\min\\{k:i\notin F_{k}\\}$. For any $v_{i},v_{j}\in V$ with
$c(v_{i})=c(v_{j})=k$ we have $(v_{i},v_{j})\notin E$. If not then there would
exist a word $p_{ij}\in P_{\mathcal{G}}$ for which consistency guarantees that
$\bar{p_{ij}}\cap F_{k}=\\{0,i,j\\}\cap F_{k}\neq\emptyset$, which can only
hold if $v_{i}$ and $v_{j}$ are assigned different colors. Thus $c$ is indeed
a valid $3$-coloring, which concludes the reduction proof.

Membership in NP holds as it is possible to verify for a guessed generalized
Büchi condition $\mathcal{B}$ of size $3$ whether
$\langle\mathcal{T},\mathcal{B}\rangle$ is consistent with $S$ in polynomial
time by iterating over all $w\in P_{\mathcal{G}}\cup N_{\mathcal{G}}$ and
verifying adequate acceptance/rejection by
$\langle\mathcal{T},\mathcal{B}\rangle$.

A similar reduction can be used to show the NP-hardness of $k$-Rabin-
Consistency as well. This leads to the following theorem, which establishes
the complexity of all fixed-size consistency decision problems we defined
above.

######  Theorem 3.9.

$k$-Parity-Consistency is solvable in polynomial time. For $k>2$ both
$k$-generalized Büchi-Consistency and $k$-Rabin-Consistency are NP-complete.

##  4 Passive learning

Our procedure for the construction of a deterministic partial transition
system is inspired by the well known regular positive negative inference
(RPNI) algorithm through which deterministic finite automata can be
constructed [21]. RPNI first constructs a prefix tree automaton which accepts
precisely the positive sample words from $S_{+}$ and subsequently attempts to
merge states of this automaton in canonical order. If a merge introduces an
inconsistency with the sample (i.e. the resulting automaton accepts a word in
$S_{-}$) it is reverted. Otherwise the algorithm continues with the resulting
automaton until no further merges are possible at which point it terminates.

When attempting to transfer this principle to infinite words, it is difficult
to find a suitable counterpart for the prefix tree automaton. If we simply
attached disjoint loops to the prefix tree at a certain depth, the resulting
transition system could certainly be equipped with an acceptance condition
such that it accepts precisely $S_{+}$. However, through the introduction of
loops with a fixed length that cannot be resolved during the execution, we
already determine parts of the structure of the resulting automaton. Instead,
we start with a transition system consisting of a single initial state and
attempt to introduce new transitions in a specific order (which is reminiscent
of the algorithm presented in [6]).

The resulting algorithm $\operatorname{\mathsf{Sprout}}$ is shown in algorithm
3. In each iteration we begin by computing
$\operatorname{\mathsf{Escapes}}(S_{+},\mathcal{T})$, the set of all prefixes
of words in $S_{+}$ which are escaping in $\mathcal{T}$. From this set we now
determine the word with the minimal escape-prefix $ua$ in length-lexicographic
order. The existing states are then tested as a target for the missing
transition in canonical order and if the resulting transition system is
$\Omega$-consistent with the sample, we continue with the next escaping word.
Checking for consistency is done by using the results from section 3 and
ensuring that no pair of indistinguishable words in $S_{+}\times S_{-}$
exists, both of which are possible in polynomial time. If no suitable target
can be found, a new state is introduced instead. See Figure 3 for an
illustration. Note that the order in which states are checked as a potential
transition target coincides with the order in which merges are attempted in
RPNI.

Input: A Sample $S=(S_{+},S_{-})$ over the alphabet $\Sigma$ and an acceptance
type $\Omega\in\mathsf{Acc}$

Output: The deterministic $\Omega$-automaton
$\mathcal{A}=(Q,\Sigma,q_{0},\delta,\mathcal{C})$ consistent with $S$

$Q\leftarrow\\{\varepsilon\\},\ \delta\leftarrow\emptyset,\
\mathcal{T}\leftarrow(Q,\Sigma,\varepsilon,\delta)$

while  _$\operatorname{\mathsf{Escapes}}(S_{+},\mathcal{T})\neq\emptyset$_ do

$ua\leftarrow$ length-lexicographic minimal escape-prefix of a word in $S_{+}$

if  _$|u| >\operatorname{\mathsf{Thres}}(S,\mathcal{T})$_ then

return
_$\operatorname{\mathsf{Aut}}(\operatorname{\mathsf{Extend}}(Q,\Sigma,\varepsilon,\delta,S_{+},S_{-}),S,\Omega)$_

forall  _$q\in Q$ in canonical order_ do

$\delta^{\prime}\leftarrow\delta\cup\\{\hat{u}\xrightarrow{a}q\\}$ for the
$\hat{u}\in Q$ with $\delta^{*}(\varepsilon,u)=\hat{u}$

if  _$(Q,\Sigma,\varepsilon,\delta^{\prime})$ is $\Omega$-consistent with $S$_
then

$\delta\leftarrow\delta^{\prime}\text{ and {continue} with the next escpaing
word}$

$Q\leftarrow Q\cup\\{\hat{u}a\\},\
\delta\leftarrow\delta\cup\\{\hat{u}\xrightarrow{a}\hat{u}a\\}$ for the
$\hat{u}\in Q$ with $\delta^{*}(\varepsilon,u)=\hat{u}$

return _$\operatorname{\mathsf{Aut}}(\mathcal{T},S,\Omega)$_

Algorithm 3 $\operatorname{\mathsf{Sprout}}$

Unfortunately there exist samples for which this approach of introducing
transitions does not terminate. When executed on
$S=(\\{(baa)^{\omega}\\},\\{(ab)^{\omega},(ba)^{\omega},(babaa)^{\omega}\\})$
for example, the algorithm would not terminate and instead construct an
infinite $b$-chain with $a$-loops on each state. We therefore introduce a
threshold on the maximal length of escape-prefixes that are considered in the
algorithm. Once this threshold is exceeded, the algorithm terminates. We have
choosen the threshold such that we can show completeness for IRC, which works
for $\operatorname{\mathsf{Thres}}(S,\mathcal{T})=l_{b}+l_{e}^{2}+1$, where
$l_{e}$ and $l_{b}$ denote the maximal length of $u$ and $v$ for any sample
word $uv^{\omega}\in S$. Intuitively, this value is sufficient to obtain
completeness for IRC as any two sample words must have already differed in at
least one position once it is exceeded.

If the threshold is exceeded before a transition system is found that is
consistent with the sample and has no escaping words from $S_{+}$, the
transition system is extended with disjoint loops that guarantee acceptance of
the remaining words in $S_{+}$ through the function
$\operatorname{\mathsf{Extend}}$, which we describe in the following. Assume
that the algorithm has constructed a transition system
$\mathcal{T}=(Q,\Sigma,\varepsilon,\delta)$ for which it then encounters an
escape-prefix exceeding the defined threshold. For each state $q\in Q$ we
collect all exit strings that leave $\mathcal{T}$ from $q$ in a set $E_{q}$.
Note that since the shortest escape-prefix in $\mathcal{T}$ exceeded the
threshold, each word in $E_{q}$ must be of the form $u^{\omega}$ for some
$u\in\Sigma^{+}$ and we can write
$E_{q}=\\{u_{1}^{\omega},\dotsc,u_{k}^{\omega}\\}$.

For each state $q$ such that $E_{q}\neq\emptyset$ we now construct the
transition system $\mathcal{T}^{\circlearrowleft}_{E_{q}}$ in which exactly
those words that belong to $E_{q}$ induce loops. To prevent any unintended
words from being accepted, we additionally ensure that the initial state of
$\mathcal{T}^{\circlearrowleft}_{E_{q}}$ is transient (meaning it cannot be
reached from any state within $\mathcal{T}^{\circlearrowleft}_{E_{q}}$). In
the following we use $\operatorname{\mathsf{Prf}}(u)$ for a word
$u\in\Sigma^{*}$ to denote the set of all prefixes of $u$. Formally we define
$\mathcal{T}^{\circlearrowleft}_{E_{q}}=(Q^{\circlearrowleft}_{E_{q}},\Sigma,q_{0},\delta^{\circlearrowleft}_{E_{q}})$
with

$\displaystyle Q^{\circlearrowleft}_{E_{q}}$
$\displaystyle=\\{q_{0}\\}\cup\bigcup_{u^{\omega}\in
E_{q}}\operatorname{\mathsf{Prf}}(u)$
$\displaystyle\delta^{\circlearrowleft}_{E_{q}}(w,a)$
$\displaystyle=\begin{cases}a&\text{ if }w=q_{0}\text{ and }a\in\Sigma\cap
Q^{\circlearrowleft}_{E_{q}}\\\ \varepsilon&\text{ if }(wa)^{\omega}\in
E_{q}\\\ wa&\text{ if }wa\in Q^{\circlearrowleft}_{E_{q}}\text{ and
}(wa)^{\omega}\notin E_{q}\\\ \bot&\text{ otherwise }\end{cases}$

It is easy to see that $q_{0}$ is indeed transient in
$\mathcal{T}^{\circlearrowleft}_{E_{q}}$ and we can clearly find a Büchi (and
thus also a generalized Büchi, Rabin and Parity) condition such that every
word in $E_{q}$ induces an accepting run in
$\mathcal{T}^{\circlearrowleft}_{E_{q}}$. By attaching the corresponding
$\mathcal{T}^{\circlearrowleft}_{E_{q}}$ to each state $q$ for which $E_{q}$
is non-empty, we obtain a transition system in which no word from $S_{+}$ is
escaping.

Once the main loop terminates, the function $\operatorname{\mathsf{Aut}}$ is
called, which uses the results from section 3 to compute an automaton that is
$\Omega$-consistent with $S$, which is then returned.

$\varepsilon$$b$$\scriptstyle\mathcal{T}_{1}:$$a$$b$$a$

$\varepsilon$$b$$bb$$\scriptstyle\mathcal{T}_{2}:$$a$$b$$a$$b$

$\varepsilon$$b$$bb$$\scriptstyle\mathcal{T}_{3}:$$a$$b$$a$$b$$a,b$

$\varepsilon$$b$$bb$$\scriptstyle\mathcal{A}:$$a:1$$b:1$$a:1$$b:1$ $a:1$
---
$b:0$

$\scriptstyle
S_{+}=\\{b^{\omega},(bbbabbaba)^{\omega},(abbb)^{\omega},(babb)^{\omega},(bbab)^{\omega},(bbba)^{\omega}\\}\text{
and }S_{-}=\\{a^{\omega},(ba)^{\omega},(bba)^{\omega}\\}$

Figure 3: In this figure three transition systems that arise during the
execution of $\operatorname{\mathsf{Sprout}}$ on the sample $S=(S_{+},S_{-})$
are depicted. The dashed transition cannot lead to $\varepsilon$ as otherwise
the union of the infinity sets of $(ba)^{\omega}$ and $(bba)^{\omega}$ would
coincide with that of $(bbbabbaba)^{\omega}$ and thus no consistent parity
condition exists. Similarly a self-loop on $b$ would mean that the infinity
sets induced by $(babb)^{\omega}$ and $(bba)^{\omega}$ would coincide. Thus
the $b$-transition must lead to a new state $bb$. On the right we can see the
DPA obtained by augmenting $\mathcal{T}_{3}$ with the parity function computed
by $\operatorname{\mathsf{ParityCons}}$ on the partial condition induced by
$S$.

######  Proposition 4.1.

For a given sample $S$ and an acceptance type $\Omega\in\mathsf{Acc}$ the
algorithm $\operatorname{\mathsf{Sprout}}$ computes in polynomial time an
automaton of type $\Omega$ that is consistent with $S$.

While $\operatorname{\mathsf{Sprout}}$ cannot learn all regular
$\omega$-languages in the limit (see 4.4), we can show completeness for
languages with an IRC.

######  Theorem 4.2.

The algorithm $\operatorname{\mathsf{Sprout}}$ learns every $\Omega$-IRC
language $L$ for $\Omega\in\mathsf{Acc}$ in the limit with polynomial time and
data.

######  Proof 4.3 (Proof (sketch)).

We describe the properties that a sample $S=(S_{+},S_{-})$ has to satisfy in
order to be _characteristic_ for an $\Omega$-IRC language $L$:

  * •

The set of prefixes of $S_{+}$ has to contain for each $\sim_{L}$ equivalence
class the minimal word in length-lexicographic order on which it is reached.

  * •

Further the sample needs to contain words with which all pairs of equivalence
classes can be separated.

  * •

Finally $S$ needs to contain sufficient information about the acceptance
condition of an automaton recognizing $L$.

The first two requirements can be satisfied in a similar way as for the
original RPNI algorithm [21]. For parity conditions this has already been
investigated in [4]. Below we give a description for Rabin conditions.
Detailed definitions for the remaining types of acceptance conditions we
introduced can be found in the appendix.

A sample $S_{\mathcal{R}}=(S_{+},S_{-})$ capturing a Rabin condition
$\mathcal{R}$ can be obtained as follows: For each pair $(E_{i},F_{i})$ we
remove all transitions in $E_{i}$ from the transition system that
$\mathcal{R}$ is defined in, decompose the result into its SCCs
$C_{1},\dotsc,C_{k}$ and compute sets $K_{i}$ consisting of all transitions in
$C_{i}$. If the set of all transitions $K_{i}$ in such an SCC satisfies
$\mathcal{R}$ we add a word $w_{i}$ inducing $K_{i}$ to $S_{+}$, otherwise
$w_{i}$ is added to $S_{-}$. For each accepting $K_{i}$ we then remove all
transitions in an $F_{j}$ for which $K_{i}\cap E_{j}=\emptyset$, and decompose
the resulting transition system into its SCCs $D_{1},\dotsc,D_{l}$. These are
the maximal negative subloops of $K_{i}$ and for each $D_{j}$ a word visiting
all transitions in $D_{j}$ is added to $S_{-}$.

While every $\Omega$-IRC language can be learned through a characteristic
sample, the same does not hold for arbitrary $\omega$-regular languages as the
following proposition establishes.

$q_{j}$$\dotsc$$q_{j+1}$$\dotsc$$q_{n-1}$$q_{n}$$\scriptstyle\sigma_{j}$$\scriptstyle
1-\sigma_{j}$$\scriptstyle\sigma_{j+1}$$\scriptstyle
1-\sigma_{j+1}$$\scriptstyle
1-\sigma_{n-2}$$\scriptstyle\sigma_{n-1}$$\scriptstyle
1-\sigma_{n-1}$$\scriptstyle\sigma_{n}$$\scriptstyle 1-\sigma_{n}$ Figure 4:
In this figure an excerpt of the transition system for the proof of 4.4 is
depicted. The transition from $q_{n}$ to $q_{j}$ forms a closed loop and words
$w_{1}\in L_{\vee},w_{2}\notin L_{\vee}$ which induce the same infinity set
can be found. Based on the existence of these words we can conclude that
$\operatorname{\mathsf{Sprout}}$ constructs a chain with self-loops on each
state when attempting to learn an automaton recognizing $L_{\vee}$

######  Proposition 4.4.

The language $L_{\vee}=\\{w\in\\{a,b\\}^{\omega}:aaaa\text{ occurrs infinitely
often in }w\text{ or}\allowbreak bbbb\text{ occurrs infinitely often in }w\\}$
cannot be learned by $\operatorname{\mathsf{Sprout}}$.

######  Proof 4.5.

To simplify notation, we exchange the alphabet and use $\Sigma=\\{0,1\\}$
instead, as it allows arithmetic on the symbols in $\Sigma$. We prove this
claim by showing through induction that the transition system constructed by
$\operatorname{\mathsf{Sprout}}$ must be a chain with loops on each state.
Specifically we show that every intermediate transition system
$\mathcal{T}=(Q,\Sigma,q_{0},\delta)$ with $Q=\\{q_{0},q_{1},\dotsc,q_{n}\\}$
created by $\operatorname{\mathsf{Sprout}}$ before the threshold is exceeded
is either not $\Omega$-consistent with $L_{\vee}$ for any
$\Omega\in\mathsf{Acc}$ or the following holds:

  * •

for each $i<n$ there exists a symbol $\sigma\in\Sigma$ such that
$\delta(q_{i},\sigma)=q_{i}$ and $\delta(q_{i},1-\sigma)=q_{i+1}$

  * •

if $q_{n}$ has an outgoing transition on some $\sigma\in\Sigma$ then
$\delta(q_{n},\sigma)=q_{n}$ and $\delta(q_{n},1-\sigma)=\bot$

The initial transition system is clearly $\Omega$-consistent with $L_{\vee}$
for all $\Omega\in\mathsf{Acc}$. Further it trivially satisfies the two
outlined conditions as it has only one state, for which no outgoing
transitions exist. For the induction step assume that
$\operatorname{\mathsf{Sprout}}$ has constructed a transition system
$\mathcal{T}=(Q,\Sigma,q_{0},\delta)$ with $Q=\\{q_{0},q_{1},\dotsc,q_{n}\\}$
for which the claim holds. We now show that the next inserted transition
either introduces an inconsistency with $L_{\vee}$ or it leads to a transition
system that also satisfies the two conditions.

If a transition from $q_{n}$ to some $q_{j}$ with $j<n$ were inserted, then a
closed cycle is formed. As $q_{j}$ is reachable there must exist some word
$u\in\Sigma^{*}$ such that $\delta^{*}(q_{0},u)=q_{j}$. Consider now the word
$v\in\Sigma^{*}$ such that $\delta^{*}(q_{j},v)=q_{j}$ and the letters in $v$
are such that they alternate between taking the self-loop and moving to the
next state along the cycle. If the loop on $q_{n}$ does not exist, then $v$
just transitions back to $q_{j}$ at this point. As can be seen in Figure 4, no
alphabet symbol can occur more than once in a row in $v$ if the dashed self-
loop on $q_{n}$ is present. Otherwise at most three consecutive occurrences of
the same symbol can appear in $v$ and we clearly have that
$w_{1}=uv^{\omega}\notin L_{\vee}$. Consider now a word $w_{2}$ which takes
each self-loop on the cycle four times before moving to the next state. This
means $w_{2}\in L_{\vee}$ but because the infinity sets induced by $w_{1}$ and
$w_{2}$ coincide (as both words take all possible transitions infinitely
often), an automaton containing such a closed cycle cannot be consistent with
$L_{\vee}$.

We have thus shown that no transition can lead from $q_{n}$ back to a state
$q_{j}$ with $j<n$. If $q_{n}$ has no outgoing transitions, then a self-loop
on the currently escaping symbol is inserted as it clearly does not introduce
an inconsistency. On the other hand if $q_{n}$ already has a self-loop on some
symbol $\sigma\in\Sigma$, then the transition on $1-\sigma$ must lead to a new
state $q_{n+1}$ as otherwise $(ab)^{\omega}\notin L_{\vee}$ and
$(aaab)^{\omega}\in L_{\vee}$ would induce the same infinity set. Thus the
$\operatorname{\mathsf{Sprout}}$ algorithm indeed constructs a chain with
self-loops until it eventually exceeds the threshold. Once this happens, the
transition system is extended such that it accepts precisely the positive
sample words. As the sample is finite, the resulting automaton cannot
recognize $L_{\vee}$ since there will always be some word $w\in L_{\vee}$ that
is not present in the sample.

However on the other hand $\operatorname{\mathsf{Sprout}}$ is not limited to
learning automata for languages with IRC of some type. In the following
proposition we give an infinite family of languages which are not in
$\Omega$-IRC for any $\Omega\in\mathsf{Acc}$, and have polynomial size
characteristic samples for $\operatorname{\mathsf{Sprout}}$.

######  Proposition 4.6.

For $i>1$, consider $L_{i}=(\Sigma^{*}b^{i})^{\omega}$ and the sample
$S^{i}=(S_{+}^{i},S_{-}^{i})$ with
$S^{i}_{+}=\\{b^{\omega},(b^{i}ab^{i-1}a\dotsc
b^{2}ab^{1}a)^{\omega}\\}\cup\\{(b^{j}ab^{k})^{\omega}:j+k=i\\}\allowbreak\text{
and }\allowbreak S^{i}_{-}=\\{(b^{j}a)^{\omega}:j<i\\}.$ Then $S^{i}$ is a
characteristic sample for $L_{i}$ and the learner
$\operatorname{\mathsf{Sprout}}$ with parity as target condition. (The sample
for $i=3$ is used in the example in Figure 3.)

######  Proof 4.7.

In the following we show that $\operatorname{\mathsf{Sprout}}$ constructs a
DPA for the language $L_{i}$ from the characteristic sample $S^{i}$. Note
first that the exit-strings of any two sample words are distinct for every
transition system constructed by $\operatorname{\mathsf{Sprout}}$, since all
words in $S^{i}$ consist of only a periodic part. Further in every word
$v^{\omega}\in S_{+}^{i}$ the infix $b^{i}$ occurs, which means that an
infinite run on any positive sample word is only possible in a transition
system that permits $i$ consecutive transitions on the symbol $b$.

Initially, the algorithm inserts a self-loop on $a$ as no sample words prevent
this. Subsequently the $b$-transition cannot be a self-loop as otherwise the
infinity sets induced by positive and negative sample words would coincide.
Thus a new state is added to which the $b$-transition from $\varepsilon$
leads. We now proceed inductively to show that a $b$-chain of length $i-1$
with $a$-transitions leading back to the initial state is created. We will
identify each state on this chain with the minimal word of the form $b^{j}$
that reaches it.

Formally such a chain satisfies that for all $j<i$ we have
$\delta^{*}(\varepsilon,b^{j})=b^{j}$ and
$\delta^{*}(\varepsilon,b^{k}a)=\varepsilon$ for all $k<j$. The base case for
$j=1$ has already been described above so assume now that the statement holds
for $j-1$ and consider the two transitions that
$\operatorname{\mathsf{Sprout}}$ inserts for the state $b^{j-1}$. We see that
inserting an $a$-transition from $b^{j-1}$ to $\varepsilon$ does not introduce
an inconsistency. This is because as outlined above no positive sample word
induces an infinite run and the exit string of any two sample words must be
distinct.

It remains to be shown that the $b$-transition from $b^{j-1}$ must lead to a
new state $b^{j}$. To see this assume to the contrary that the introduction of
a $b$-transition from $b^{j-1}$ to some $b^{l}$ with $l<j$ leads to a
transition system $\mathcal{T}^{\prime}$ which is Parity-consistent with
$S^{i}$. It is not hard to see that the infinity set $P$ induced by the
positive sample word $(b^{i}ab^{i-1}\dotsc b^{1}a)^{\omega}$ contains all
transitions in $\mathcal{T}^{\prime}$. Now let $N_{0},N_{1},\dotsc,N_{j}$ be
the infinity sets induced by the negative sample words
$a^{\omega},(ba)^{\omega},\dotsc,(b^{j}a)^{\omega}$. It is easily verified
that $P=N_{0}\cup N_{1}\cup\dotsc\cup N_{j}$, thus satisfying the conditions
for 3.2. This means that $\mathcal{T}^{\prime}$ cannot be Parity-consistent
with $S^{i}$ and hence no $b$-transition from $b^{j-1}$ to any $b^{l}$ with
$l<j$ is kept.

Once this $b$-chain of length $i-1$ is constructed, we simply need to verify
that inserting both the $a$\- and $b$-transition from $b^{i-1}$ to
$\varepsilon$ does not lead to an inconsistent transition system. Since only
positive sample words contain $i$ consecutive occurrences of $b$, the
$b$-transition from $b^{i-1}$ to $\varepsilon$ occurs exclusively in the
infinity set induced by positive but not negative words. Thus a consistent
parity condition exists and $\operatorname{\mathsf{Sprout}}$ constructs a DPA
recognizing $L_{i}$.

##  5 Active Learning

We consider the standard minimal adequate teacher (MAT) active learning
scenario [1], in which the learning algorithm has access to a teacher that can
answer membership queries and equivalence queries for the target language, and
returns a counterexample if the automaton for an equivalence query is not
correct. A natural extension to $\omega$-automata considers membership queries
for ultimately periodic words and equivalence queries with ultimately periodic
words as counterexamples (see [16]).

Since there is a polynomial time active learning algorithm for deterministic
weak automata [16], a natural next candidate for polynomial time active
learning are deterministic automata with an informative right congruence.
However, the theorem below basically shows that this class is as hard for
active learning as general regular $\omega$-languages.

######  Theorem 5.1.

Let $\Omega\in\mathsf{Acc}$ be an acceptance type, and consider the active
learning setting with membership and equivalence queries for ultimately
periodic words. There is a polynomial time active learning algorithm for
deterministic automata of type $\Omega$ with informative right congruence if,
and only if, there is a polynomial time active learning algorithm for general
deterministic automata of type $\Omega$.

######  Proof 5.2 (Proof (sketch)).

Assume that $\mathit{AL}_{\mathit{IRC}}$ is an active learning algorithm for
automata with informative right congruence of type $\Omega$. The arguments
used below work for all acceptance types $\Omega\in\mathsf{Acc}$. For
simplicity we use the parity condition in the following.

Our goal is to use $\mathit{AL}_{\mathit{IRC}}$ in order to define an active
learning algorithm $\mathit{AL}$ for general DPA that runs in polynomial time
if $\mathit{AL}_{\mathit{IRC}}$ does. The rough idea is as follows: We have to
learn an automaton $\mathcal{A}$ for a target language
$L\subseteq\Sigma^{\omega}$ that does not have an IRC, in general. Such an
automaton $\mathcal{A}$ can be turned into an automaton with IRC by adding new
letters to the alphabet, and then extending the automaton such that from each
state a different word over these new letters is accepted. Restricted to the
original alphabet, this extended automaton still accepts the same language as
before. Since the new automaton has an IRC, we can use
$\mathit{AL}_{\mathit{IRC}}$ to learn it. The only problem with this approach
is that we do not know the target automaton $\mathcal{A}$, so we cannot simply
extend it and let $\mathit{AL}_{\mathit{IRC}}$ learn the extension. However,
we can simulate a teacher for $\mathit{AL}_{\mathit{IRC}}$ that answers
queries of $\mathit{AL}_{\mathit{IRC}}$ such that these answers are consistent
with such an extension of $\mathcal{A}$. We give the answers such that they
only reveal information on the original target language $L$. Hence,
$\mathit{AL}_{\mathit{IRC}}$ first has to learn, in some sense, an automaton
for $L$ in order to obtain information on the newly added letters in the
extension.

More formally, define an extended alphabet
$\Sigma_{\star}=\Sigma\mathbin{\dot{\cup}}\\{\star,0,1\\}$ with new letters
$\star,0,1$ that do not occur in $\Sigma$. Now let $L\subseteq\Sigma^{\omega}$
be a target language which we want to learn. Our algorithm $\mathit{AL}$
simulates $\mathit{AL}_{\mathit{IRC}}$ over the alphabet $\Sigma_{\star}$.
Note that $\mathit{AL}$ has access to a teacher $T$ that answers queries for
the language $L$ over the alphabet $\Sigma$. We define a teacher
$T_{\mathit{IRC}}$ that answers queries that are asked by
$\mathit{AL}_{\mathit{IRC}}$ during its simulation as follows:

  * •

_Membership query for a word $w=uv^{\omega}$:_ If none of the newly introduced
symbols occur in $w$, i.e. $w\in\Sigma^{\omega}$ then we simply copy the
answer $T(w)$. Otherwise $w$ must contain $0,1$ or $\star$ in which case
$T_{\mathit{IRC}}$ always gives a negative answer.

  * •

_Equivalence query for an automaton $\mathcal{A}$:_ We construct a new
automaton $\mathcal{B}$ by removing from $\mathcal{A}$ all transitions on
symbols $0$, $1$ or $\star$ and pruning any unreachable states. $\mathcal{B}$
is then given to $T$ for an equivalence query. If $T(\mathcal{B})$ returns a
counterexample $w$, then this is used as the result of
$T_{\mathit{IRC}}(\mathcal{A})$.

Otherwise the automaton $\mathcal{B}$ must recognize the target language $L$.
In this case, the simulation of $\mathit{AL}_{\mathit{IRC}}$ is stopped, and
our algorithm $\mathit{AL}$ returns $\mathcal{B}$.

It can be shown that this algorithm $\mathit{AL}$ learns the target language
$L$ in polynomial time if $\mathit{AL}_{\mathit{IRC}}$ is a polynomial time
algorithm.

So the property of an IRC does not help for active learning, while for passive
learning in the limit it seems to make the problem simpler. We finish this
section with the observation that polynomial time active learning is at least
as hard as learning in the limit with polynomial time and data, given that the
class $\mathcal{K}$ of target automata satisfies the following properties
(which are satisfied by standard classes of deterministic automata):

  * •

(P1) It is decidable in polynomial time if a given word is accepted by a given
automaton from $\mathcal{K}$.

  * •

(P2) For a given sample $S$, one can construct in polynomial time an automaton
from $\mathcal{K}$ that is consistent with $S$.

  * •

(P3) If two automata from $\mathcal{K}$ are not equivalent, then there exists
a word of polynomial size witnessing the difference.

######  Proposition 5.3.

Consider a class $\mathcal{K}$ of finite automata for which properties
(P1)–(P3) are satisfied. If there is a polynomial time active learning
algorithm for $\mathcal{K}$, then $\mathcal{K}$ can be learned in the limit
with polynomial time and data.

######  Proof 5.4 (Proof (sketch)).

Assume that there is a polynomial time active learning algorithm
$\mathit{AL}_{\mathcal{K}}$ for target automata from $\mathcal{K}$. A passive
learner can simulate an execution of $\mathit{AL}_{\mathcal{K}}$ in which
equivalence queries are always answered with the smallest counterexample. A
characteristic sample can be constructed from all the words that are used in
such an execution of $\mathit{AL}_{\mathcal{K}}$.

##  6 Conclusion

We have presented polynomial time algorithms for checking the consistency of a
(partial) deterministic transition system with a set of positive and negative
ultimately periodic words for the acceptance conditions Büchi, generalized
Büchi, parity, and Rabin. Since co-Büchi and Streett conditions are dual to
Büchi and Rabin conditions, respectively, one also obtains algorithms for
these conditions by flipping negative and positive examples.

The consistency algorithms allow us to extend the principle of the RPNI
algorithm from finite to infinite words, leading to the polynomial time
algorithm $\operatorname{\mathsf{Sprout}}$ that constructs a deterministic
$\omega$-automaton from given ultimately periodic examples. We have shown that
$\operatorname{\mathsf{Sprout}}$ can learn deterministic automata for
languages with an IRC in the limit with polynomial time and data. While
$\operatorname{\mathsf{Sprout}}$ is not restricted to IRC languages, there are
regular $\omega$-langauges which it cannot learn. It is obviously an
interesting open question whether there is an algorithm that learns
deterministic automata for general regular $\omega$-languages with polynomial
time and data. Our results in Section 5 show that finding such an algorithm is
not more difficult than finding an active learning algorithm that learns
deterministic automata for IRC languages from membership and equivalence
queries.

## References

  * [1] Dana Angluin.  Learning regular sets from queries and counterexamples.  Information and Computation, 75(2):87–106, 1987.  URL: https://www.sciencedirect.com/science/article/pii/0890540187900526, doi:https://doi.org/10.1016/0890-5401(87)90052-6.
  * [2] Dana Angluin and Dana Fisman.  Learning regular omega languages.  Theor. Comput. Sci., 650:57–72, 2016.  doi:10.1016/j.tcs.2016.07.031.
  * [3] Dana Angluin and Dana Fisman.  Regular omega-languages with an informative right congruence.  In Proceedings Ninth International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2018, Saarbrücken, Germany, 26-28th September 2018, volume 277 of EPTCS, pages 265–279, 2018.  doi:10.4204/EPTCS.277.19.
  * [4] Dana Angluin, Dana Fisman, and Yaara Shoval.  Polynomial identification of ømega-automata.  In Armin Biere and David Parker, editors, Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part II, volume 12079 of Lecture Notes in Computer Science, pages 325–343. Springer, 2020.  doi:10.1007/978-3-030-45237-7\\_20.
  * [5] Christel Baier and Joost-Pieter Katoen.  Principles of model checking.  MIT Press, 2008.
  * [6] Andreas Birkendorf, Andreas Böker, and Hans Simon.  Learning deterministic finite automata from smallest counterexamples.  SIAM J. Discrete Math., 13:465–491, 01 2000.  doi:10.1137/S0895480198340943.
  * [7] J Richard Büchi.  On a decision method in restricted second order arithmetic, logic, methodology and philosophy of science (proc. 1960 internat. congr.), 1962.
  * [8] Rafael C. Carrasco and José Oncina.  Learning stochastic regular grammars by means of a state merging method.  In Grammatical Inference and Applications, Second International Colloquium, ICGI-94, Alicante, Spain, September 21-23, 1994, Proceedings, volume 862 of Lecture Notes in Computer Science, pages 139–152. Springer, 1994.  doi:10.1007/3-540-58473-0\\_144.
  * [9] Olivier Carton and Ramón Maceiras.  Computing the rabin index of a parity automaton.  RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, 33(6):495–505, 1999.  URL: http://www.numdam.org/item/ITA_1999__33_6_495_0/.
  * [10] Colin De La Higuera.  Characteristic sets for polynomial grammatical inference.  In Laurent Miclet and Colin de la Higuera, editors, Grammatical Interference: Learning Syntax from Sentences, pages 59–71, Berlin, Heidelberg, 1996. Springer Berlin Heidelberg.
  * [11] Stefan Dziembowski, Marcin Jurdziński, and Igor Walukiewicz.  How much memory is needed to win infinite games?  In Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science, LICS ’97, pages 99–110, Los Alamitos, California, 1997. IEEE Computer Society Press.  doi:10.1109/lics.1997.614939.
  * [12] E. Mark Gold.  Complexity of automaton identification from given data.  Inf. Control., 37(3):302–320, 1978.  doi:10.1016/S0019-9958(78)90562-4.
  * [13] John E. Hopcroft and Jeffrey D. Ullman.  Formal Languages and their Relation to Automata.  Addison-Wesley, 1969.
  * [14] Richard M Karp.  Reducibility among combinatorial problems.  In Complexity of computer computations, pages 85–103. Springer, 1972.  doi:10.1007/978-1-4684-2001-2_9.
  * [15] Christof Löding and Anton Pirogov.  Determinization of büchi automata: Unifying the approaches of safra and muller-schupp.  In 46th International Colloquium on Automata, Languages, and Programming, ICALP 2019, volume 132 of LIPIcs, pages 120:1–120:13. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2019.  URL: http://www.dagstuhl.de/dagpub/978-3-95977-109-2.
  * [16] Oded Maler and Amir Pnueli.  On the learnability of infinitary regular sets.  Inf. Comput., 118(2):316–326, 1995.  doi:10.1006/inco.1995.1070.
  * [17] Hua Mao, Yingke Chen, Manfred Jaeger, Thomas D. Nielsen, Kim G. Larsen, and Brian Nielsen.  Learning probabilistic automata for model checking.  In Eighth International Conference on Quantitative Evaluation of Systems, QEST 2011, Aachen, Germany, 5-8 September, 2011, pages 111–120. IEEE Computer Society, 2011.  doi:10.1109/QEST.2011.21.
  * [18] Philipp J. Meyer, Salomon Sickert, and Michael Luttenberger.  Strix: Explicit reactive synthesis strikes back!  In Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I, pages 578–586, 2018.  doi:10.1007/978-3-319-96145-3\\_31.
  * [19] Jakub Michaliszyn and Jan Otop.  Learning deterministic automata on infinite words.  In ECAI 2020 - 24th European Conference on Artificial Intelligence, volume 325 of Frontiers in Artificial Intelligence and Applications, pages 2370–2377. IOS Press, 2020.  doi:10.3233/FAIA200367.
  * [20] José Oncina, Pedro García, and Enrique Vidal.  Learning subsequential transducers for pattern recognition interpretation tasks.  IEEE Trans. Pattern Anal. Mach. Intell., 15(5):448–458, 1993\.  doi:10.1109/34.211465.
  * [21] Jose Oncina and Pedro García.  Inferring regular languages in polynomial update time.  World Scientific, 01 1992.  doi:10.1142/9789812797902_0004.
  * [22] Nir Piterman.  From nondeterministic Büchi and Streett automata to deterministic parity automata.  In Proceedings of the 21st IEEE Symposium on Logic in Computer Science (LICS 2006), pages 255–264. IEEE Computer Society, 2006.  doi:10.2168/LMCS-3(3:5)2007.
  * [23] Shmuel Safra.  On the complexity of omega-automata.  In Proceedings of the 29th Annual Symposium on Foundations of Computer Science, FoCS ’88, pages 319–327, Los Alamitos, California, 1988. IEEE Computer Society Press.  doi:10.1109/SFCS.1988.21948.
  * [24] Sven Schewe.  Tighter bounds for the determinisation of Büchi automata.  In Proceedings of Foundations of Software Science and Computational Structures, 12th International Conference, FOSSACS 2009, volume 5504 of Lecture Notes in Computer Science, pages 167–181. Springer, 2009.  doi:10.1007/978-3-642-00596-1_13.
  * [25] 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.  URL: http://drops.dagstuhl.de/opus/volltexte/2010/2881, doi:10.4230/LIPIcs.FSTTCS.2010.400.
  * [26] Wolfgang Thomas.  Automata on Infinite Objects, page 133–191.  MIT Press, Cambridge, MA, USA, 1991.
  * [27] 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.  doi:10.1007/978-3-642-00596-1_1.
  * [28] Wieslaw Zielonka.  Infinite games on finitely coloured graphs with applications to automata on infinite trees.  Theoretical Computer Science, 200(1):135–183, 1998.  URL: https://www.sciencedirect.com/science/article/pii/S0304397598000097, doi:https://doi.org/10.1016/S0304-3975(98)00009-7.

##  Appendix A Consistency Algorithms

###  A.1 (generalized) Büchi conditions: Full proof of Theorem 3.1

We now provide the formal correctness proofs that were excluded from section 3
due to the constrained space. The proof of Theorem 3.1 is split into two
parts, each dealing with one of the two acceptance types, starting with Büchi
conditions.

######  Lemma A.1.

Let $F=\operatorname{\mathsf{BuchiCons}}(\mathcal{H}_{0},\mathcal{H}_{1})$ for
a consistent partial condition
$\mathcal{H}=(\mathcal{H}_{0},\mathcal{H}_{1})$. If $F\neq\bot$ then $F$ is
consistent with $\mathcal{H}$, otherwise no such Büchi condition exists.

######  Proof A.2.

Assume to the contrary that there exists some $F\subseteq Q\times\Sigma$ that
is consistent with $\mathcal{H}$ but
$\operatorname{\mathsf{BuchiCons}}(\mathcal{H}_{0},\mathcal{H}_{1})=\bot$ and
hence there exists some $P\in\mathcal{H}_{0}$ such that $P\subseteq
N_{1}\cup\dotsc\cup N_{k}$ with $N_{i}\in\mathcal{H}_{1}$ for $i\leq k$. Since
$F$ is consistent with $\mathcal{H}$ it must be that $P\cap F\neq\emptyset$.
But then there exists an index $i\leq k$ such that $N_{i}\cap F\neq\emptyset$,
which is a contradiction since $N_{i}\in\mathcal{H}_{1}$.

Let $F=\operatorname{\mathsf{BuchiCons}}(\mathcal{H}_{0},\mathcal{H}_{1})$,
which means $F=(Q\times\Sigma)\setminus\bigcup\mathcal{H}_{1}$. For all
$P\in\mathcal{H}_{0}$ we have $P\setminus\bigcup\mathcal{H}_{1}\neq\emptyset$
and thus clearly $P\cap F\neq\emptyset$ as well. On the other hand for an
$N\in\mathcal{H}_{1}$ it holds that $N\subseteq\bigcup\mathcal{H}_{1}$ and
hence $N\cap F=\emptyset$.

The proof for generalized Büchi conditions follows a similar structure.

######  Lemma A.3.

If $\mathcal{H}=(\mathcal{H}_{0},\mathcal{H}_{1})$ is a consistent partial
condition then
$\operatorname{\mathsf{genBuchiCons}}(\mathcal{H}_{0},\mathcal{H}_{1})$ is
defined if and only if
$\operatorname{\mathsf{genBuchiCons}}(\mathcal{H}_{0},\mathcal{H}_{1})$ is
consistent with $\mathcal{H}$.

######  Proof A.4.

We assume that
$\operatorname{\mathsf{genBuchiCons}}(\mathcal{H}_{0},\mathcal{H}_{1})=\bot$
but the generalized Büchi condition $\mathcal{B}=\\{F_{1},\dotsc,F_{k}\\}$ is
consistent with $\mathcal{H}$. Since $\operatorname{\mathsf{genBuchiCons}}$
terminated prematurely there exists a set $P\in\mathcal{H}_{0}$ with
$P\subseteq N$ for a $\subseteq$-maximal $N\in\mathcal{H}_{1}$. Since
$\mathcal{B}$ is consistent with $\mathcal{H}$ we must have that $P\cap
F_{i}\neq\emptyset$ for all $i\leq k$ and $P\subseteq N$, this entails $N\cap
F_{i}\neq\emptyset$ for all $i\leq k$. But then $N$ satisfies $\mathcal{B}$
and $\mathcal{B}$ cannot be consistent with $\mathcal{H}$, which is a
contradiction.

Let
$\mathcal{B}=\operatorname{\mathsf{BuchiCons}}(\mathcal{H}_{0},\mathcal{H}_{1})$
and consider some $P\in\mathcal{H}_{0}$. By definition we have $P\not\subseteq
N_{i}$ for all $\subseteq$-maximal negative $N_{i}\in\mathcal{H}_{1}$ and
hence $P\cap((Q\times\Sigma)\setminus N_{i})\neq\emptyset$, meaning $P$
satisfies $\mathcal{B}$. For any $N\in\mathcal{H}_{1}$ there exists some
$\subseteq$-maximal $N_{i}\supseteq N$ and consequently
$N\cap((Q\times\Sigma)\setminus N_{i})=\emptyset$. Overall we can thus
conclude that $\mathcal{B}$ is consistent with $\mathcal{H}$.

We are now able to prove Theorem 3.1 which establishes the efficient
decidability of the consistency problem for Büchi and generalized Büchi
conditions.

See 3.1

The correctness of both algorithms directly follows from A.1 and A.3 and since
both algorithms make use of only elementary operations on sets, it is easily
verified that they run in polynomial time.

###  A.2 Parity consistency: Full proof of Theorem 3.4

We begin by giving a proof for 3.2.

See 3.2

######  Proof A.5.

Assume to the contrary that there exists some parity condition $\kappa$ which
is consistent with $\mathcal{H}$, then for $i\leq k$ we have that
$\min(\kappa(P_{i}))$ is even as each $P_{i}$ must satisfy $\kappa$. This
clearly entails that $\min(\kappa(P))$ is even as well. However by an
analogous argument it must be that $\min(\kappa(N))$ is odd as each $N_{j}$
for $j\leq l$ is negative. This is a contradiction as $N=P$ hence $\kappa$
cannot be consistent with $\mathcal{H}$.

We now justify our claim that the converse of 3.2 also holds. To that end we
first show that the Zielonka path $\operatorname{\mathsf{ParityCons}}$
constructs correctly classifies all sample loops.

######  Lemma A.6.

For all $i$ the Zielonka path $(Z_{0},\sigma_{0}),\dotsc,(Z_{i},\sigma_{i})$
computed by $\operatorname{\mathsf{ParityCons}}$ correctly classifies all
sample loops $S$ with $S\not\subseteq Z_{i}$.

######  Proof A.7.

We prove this statement by induction on $i$. Clearly the base case for $i=0$
holds as $Z_{0}=Q\times\Sigma$ and hence we have for all possible loops $S$
that $S\subseteq Z_{0}$. Now assume the statement holds for all $j<i$ and
consider some sample loop $S\not\subseteq Z_{i}$. If $S\not\subseteq Z_{i-1}$
then the induction hypothesis guarantees that $S$ is correctly classified.
Otherwise $S\subseteq Z_{i-1}$ and $S\cap(Z_{i-1}\setminus
Z_{i})\neq\emptyset$, which in turn means that $S$ cannot be a negative loop
as $Z_{i}$ is the union of all negative subloops of $Z_{i-1}$. Therefore
$\mathcal{H}(S)=\sigma_{i-1}$ and $S$ is indeed assigned a correct
classification.

We can now show that whenever $\operatorname{\mathsf{ParityCons}}$ terminates
prematurely, there must exist positive and negative sets in $\mathcal{H}$,
which satisfy the conditions in 3.2. This in turn means that no parity
condition consistent with $\mathcal{H}$ can exist.

######  Lemma A.8.

If $\operatorname{\mathsf{ParityCons}}$ terminates prematurely, then no parity
condition correctly classifying all sample loops exists.

######  Proof A.9.

Assume that $\mathcal{H}=(\mathcal{H}_{0},\mathcal{H}_{1})$ is consistent and
$\operatorname{\mathsf{ParityCons}}$ terminates without producing a Zielonka
path. Such a failure can only occur during some iteration $i>0$ for which we
assume without loss of generality that $\sigma_{i}=0$, i.e. $Z_{i}$ is
positive. If not then due to the inherent symmetry of parity conditions we can
simply exchange both components of $\mathcal{H}$. We compute $Z_{i+1}$ as the
union of $N_{1},\dotsc,N_{k}$ with each $N_{j}$ being a maximal negative
subloop of $Z_{i}$. Furthermore $Z_{i}$ itself is the union of
$P_{1},\dotsc,P_{l}$, which are the maximal positive subloops of $Z_{i-1}$.
The only condition under which $\operatorname{\mathsf{ParityCons}}$ terminates
without prematurely without producing a Zielonka path is if $Z_{i}=Z_{i+1}$.
But then we have $P_{1}\cup\dotsc\cup P_{l}=N_{1}\cup\dotsc\cup N_{k}$. Thus
the conditions of 3.2 are satisfied, which means that no parity condition that
is consistent with $\mathcal{H}$ exists.

A.6 and A.8 can be used in conjunction to establish the correctness of
$\operatorname{\mathsf{ParityCons}}$. To show optimality (with regard to the
number of distinct priorities), we now show that under the assumption of
$Q\times\Sigma\in\mathcal{H}$ no parity condition exists that has strictly
fewer distinct priorities than the one computed by
$\operatorname{\mathsf{ParityCons}}$.

######  Lemma A.10.

Let $\mathcal{T}=(Q,\Sigma,q_{0},\delta)$ be a deterministic (partial)
transition system and $\mathcal{H}=(\mathcal{H}_{0},\mathcal{H}_{1})$ be a
consistent partial condition over $Q\times\Sigma$ with
$Q\times\Sigma\in\mathcal{H}$. The parity condition
$\kappa:Q\to\\{0,1,\dotsc,n-1\\}$ determined by the Zielonka path
$(Z_{0},\sigma_{0}),\dotsc,(Z_{n-1},\sigma_{n-1})$ computed in
$\operatorname{\mathsf{ParityCons}}$ is optimal, i.e. for all
$\kappa^{\prime}:Q\to C^{\prime}$ for some $C^{\prime}\subseteq\mathbb{N}$
which are consistent with $\mathcal{H}$ we have $|C^{\prime}|\geq n$.

######  Proof A.11.

Assume $\kappa^{\prime}:Q\to C^{\prime}$ is a parity function which is
consistent with $\mathcal{H}$, meaning for all $S\subseteq Q$ the minimal
priority associated with a state in $S$ is even if and only if
$S\in\mathcal{H}_{0}$. For all $i<n$ we have $Z_{i}=X_{i}^{1}\cup\dotsc\cup
X_{i}^{k_{i}}$ where all $X_{i}^{j}$ have the same classification as $Z_{i}$.
Let $p^{*}_{n-1}\in Z_{n-1}$ be a state with
$\kappa^{\prime}(p^{*}_{n-1})=\min(\kappa^{\prime}(Z_{n-1}))$ and let $j$ be
an index such that $p^{*}_{n-1}\in X_{n-2}^{j}$ which must exist since
$Z_{n-2}\supseteq Z_{n-1}$. Because furthermore
$X_{n-2}^{j}\in\mathcal{H}_{1-\sigma_{n-1}}$, we know that $X_{n-2}^{j}$ must
contain some state $p^{*}_{n-2}$ with
$\kappa^{\prime}(p^{*}_{n-2})<\kappa^{\prime}(p^{*}_{n-1})$. Successive
application of this argument yields a sequence
$p^{*}_{n-1},p^{*}_{n-2},\dotsc,p^{*}_{0}$ where
$\kappa^{\prime}(p^{*}_{i+1})>\kappa^{\prime}(p^{*}_{i})$ for $i<n-1$. Hence
we know that $C^{\prime}$ has to contain at least $n$ distinct priorities.

Up to this point we always assumed that $Q\times\Sigma\in\mathcal{H}$, which
clearly does not hold for all partial conditions. In the following we
establish that there exists a suitable way of dealing with partial conditions
that do not satisfy this assumption. If $\mathcal{H}$ does not classify the
set of all transitions, we define $\mathcal{H}^{p}$ and $\mathcal{H}^{n}$
which are obtained by adding $Q\times\Sigma$ to $\mathcal{H}_{0}$ and
$\mathcal{H}_{1}$ respectively. By executing
$\operatorname{\mathsf{ParityCons}}$ for both of these newly constructed
partial conditions, we are guaranteed to obtain an optimal parity condition
consistent with $\mathcal{H}$ if one exists.

######  Lemma A.12.

Let $\mathcal{H}=(\mathcal{H}_{0},\mathcal{H}_{1})$ be a consistent partial
condition with $Q\times\Sigma\notin\mathcal{H}_{0}\cup\mathcal{H}_{1}$. If
$\operatorname{\mathsf{ParityCons}}$ does not yield a Zielonka path for either
$\mathcal{H}^{p}$ or $\mathcal{H}^{n}$ then $\mathcal{H}$ is not consistent
with any parity condition. If two distinct parity conditions $\kappa^{p}$ and
$\kappa^{n}$ are arise from the computations then
$||\kappa^{p}|-|\kappa^{n}||\leq 1$ with the smaller one of them being
optimal.

######  Proof A.13.

Assume that $\operatorname{\mathsf{ParityCons}}$ terminates early for both
$\mathcal{H}^{p}$ and $\mathcal{H}^{n}$, but $\mathcal{H}$ is consistent with
some parity condition $\kappa$. Clearly $\kappa$ must classify $Q\times\Sigma$
either positively or negatively, which means that either $\mathcal{H}^{p}$ or
$\mathcal{H}^{n}$ must be consistent with $\kappa$ as well. This is a
contradiction since $\operatorname{\mathsf{ParityCons}}$ terminated without
producing a Zielonka path, which by A.8 implies that no such condition can
exist. If we assume that $\kappa$ has the least number of distinct priorities
any parity condition consistent with $\mathcal{H}$ can have, then it is clear
by A.10 that $\operatorname{\mathsf{ParityCons}}$ applied to either
$\mathcal{H}^{p}$ or $\mathcal{H}^{n}$ must also yield an optimal parity
condition.

We now want to show $||\kappa^{p}|-|\kappa^{n}||\leq 1$ and assume without
loss of generality that $|\kappa^{p}|>|\kappa^{n}|$. By definition
$\kappa^{p}$ is equivalent to a Zielonka path $Z_{0}\supseteq
Z_{1}\supseteq\dotsc\supseteq Z_{k-1}$ with alternating classifications
$\sigma_{i}$ in $\kappa^{p}$. For $i>0$ we have that the classification of
$Z_{i}$ by $\kappa^{p}$ and $\kappa^{n}$ coincide as they do not depend on the
attribution of $Q\times\Sigma$. Then clearly $Z_{1}\supseteq\dotsc\supseteq
Z_{k-1}$ forms a chain of length $k-1$ with alternating classifications in
$\kappa^{n}$. This means that $\kappa^{n}$ must contain at least $k-1$
distinct priorities and the statement follows.

We can now prove Theorem 3.4.

See 3.4

######  Proof A.14.

Correctness follows from A.6 and A.8. The size of the $Z_{i}$ constructed by
$\operatorname{\mathsf{ParityCons}}$ is strictly decreasing and as in each
iteration of the loop at least one set of the partial condition is processed,
there are at most as many iterations as there are sets in $\mathcal{H}$. Since
computing the union of all subsets with opposite classification can be done in
polynomial time, the algorithm overall runs in polynomial time. For partial
conditions that classify the set of all transitions, A.10 guarantees
optimality. On the other hand if $Q\times\Sigma\notin\mathcal{H}$, we know by
A.12 that an optimal parity condition can be obtained by executing
$\operatorname{\mathsf{ParityCons}}$ for both $\mathcal{H}^{p}$ and
$\mathcal{H}^{n}$ and choosing the result with fewer distinct priorities. As
the algorithm runs in polynomial time and comparing the size of two parity
conditions is trivial, the statement follows.

###  A.3 Rabin consistency: Full proof of Theorem 3.6

This subsection follows a similar structure as the preceding one and we begin
by establishing that the Rabin condition constructed by
$\operatorname{\mathsf{RabinCons}}$ actually produces correct classifications.

######  Lemma A.15.

Let $\mathcal{H}=(\mathcal{H}_{0},\mathcal{H}_{1})$ be a consistent partial
condition, then for
$\mathcal{R}=\operatorname{\mathsf{RabinCons}}(\mathcal{H})$ we have that
$\mathcal{R}(X)=\mathcal{H}(X)$ for all
$X\in\mathcal{H}_{0}\cup\mathcal{H}_{1}$.

######  Proof A.16.

Let $P\in\mathcal{H}_{0}$ be a positive loop then there exists a pair
$(E_{P},F_{P})\in\mathcal{R}$ for which we have $P\cap
E_{P}=P\cap((Q\times\Sigma)\setminus P)=\emptyset$. For the maximal negative
subloops $N_{1},\dotsc,N_{k}$ of $P$ it holds that
$F_{P}=P\setminus(N_{1}\cup\dotsc\cup N_{k})\neq\emptyset$ as the algorithm
did not terminate prematurely. This in turn guarantees that $F_{P}\cap
P\neq\emptyset$ and thus $P$ satisfies $\mathcal{R}$.

For a negative loop $N\in\mathcal{H}_{1}$ and any pair
$(E_{P},F_{P})\in\mathcal{R}$ we want to show that either $N\cap
E_{P}\neq\emptyset$ or $N\cap F_{P}=\emptyset$. For pairs where $N$ intersects
$E_{P}$ we are immediately done, so assume that $N\cap E_{P}=\emptyset$, which
implies $N\subseteq P$. We have $N\subseteq N^{\prime}$ for a maximal negative
subloop $N^{\prime}$ of $P$ and thus since $F_{P}\subseteq P\setminus
N^{\prime}$ we have $F_{P}\cap N=\emptyset$.

It remains to be shown that premature termination of the algorithm entails
that it is impossible to find a Rabin condition which is consistent with the
given partial condition.

######  Lemma A.17.

If $\operatorname{\mathsf{RabinCons}}$ terminates prematurely then there
exists no Rabin condition that is consistent with $\mathcal{H}$.

######  Proof A.18.

Assume the algorithm terminates in an iteration of the outer loop for some
$P\in\mathcal{H}_{0}$. This can only happen if $F_{P}=\emptyset$ which means
for the negative subloops $N_{1},\dotsc,N_{k}$ of $P$ we have
$N_{1}\cup\dotsc\cup N_{k}=P$. Now assume there exists some Rabin condition
$\mathcal{R}=\\{(E_{1},F_{1}),\dotsc,(E_{k},F_{k})\\}$ that is consistent with
$\mathcal{H}$, which classifies each of the $N_{i}$ negatively, meaning
$N_{i}\cap E_{j}\neq\emptyset$ or $N_{i}\cap F_{j}=\emptyset$ for all $j\leq
k$. Clearly the union of any two negative loops $N=N_{i_{1}}\cup N_{i_{2}}$
must also be classified negatively and thus $P$ is a negative loop in
$\mathcal{R}$. But since $P\in\mathcal{H}_{0}$ we know that $\mathcal{R}$
cannot be consistent with $\mathcal{H}$.

By combining A.15 and A.17 we can show that
$\operatorname{\mathsf{RabinCons}}$ is correct, which forms the first part of
Theorem 3.6.

See 3.6

For each positive set in $\mathcal{H}$ the outer loop of
$\operatorname{\mathsf{RabinCons}}$ is executed once. In each of these
iterations only elementary set operations on the $\subseteq$-maximal negative
subsets are executed. As the number of these sets cannot exceed the
$|\mathcal{H}_{1}|$, the overall runtime of
$\operatorname{\mathsf{RabinCons}}$ is polynomial in the size of the partial
condition.

###  A.4 Fixed-size consistency: Full proof of Theorem 3.9

Since the positively classified sets of a Rabin condition are not closed under
union, a similar situation as with generalized Büchi conditions (as outlined
in section 3) arises and no clear efficient way of constructing the a
condition with the fewest number of distinct Rabin pairs exists. The
$\operatorname{\mathsf{RabinCons}}$ algorithm we presented in algorithm 2
produces Rabin conditions with $|\mathcal{H}_{0}|$ pairs, which is not optimal
in general. Even though it is possible to introduce optimizations that reduce
this number, we prove in the following that $k$-Rabin-Consistency is NP-hard
already for $k=3$. The proof follows a similar structure as the previous one
and uses a reduction from $3$-Coloring.

######  Lemma A.19.

$3$-Rabin-Consistency is NP-complete.

######  Proof A.20.

In this reduction we use the same transition system
$\mathcal{T}_{\mathcal{G}}$ (which is depicted in Figure 2) but define a
different sample, $S_{\mathcal{G}}=(P_{\mathcal{G}},N_{\mathcal{G}})$, as
follows:

$P_{\mathcal{G}}=\\{p_{i}:0<i\leq n\\}\text{ and
}N_{\mathcal{G}}=\\{n_{ij}:(v_{i},v_{j})\in E\\}\text{ for
}p_{i}=i^{\omega},n_{ij}=(iijj)^{\omega}.$

We again use $\bar{p_{i}}$ and $\bar{n_{ij}}$ to denote the infinity sets
induced by $p_{i}$ and $n_{ij}$ in $\mathcal{T}_{\mathcal{G}}$. Based on a
given 3-coloring $c:V\to\\{1,2,3\\}$ for $\mathcal{G}$ we now define the Rabin
condition

$\mathcal{R}=\\{(E_{1},F_{1}),(E_{2},F_{2}),(E_{3},F_{3})\\}\text{ with
}E_{i}=\\{j:c(v_{j})\neq i\\}\text{ and }F_{i}=\\{j:c(v_{j})=i\\}$

For any positive sample word $p_{i}$ let $j=c(v_{i})$. We have
$\bar{p_{i}}\cap E_{j}=\\{0,i\\}\cap E_{j}=\emptyset$ and $\bar{p_{i}}\cap
F_{j}=\\{0,i\\}\cap F_{j}\neq\emptyset$ and thus $P_{\mathcal{G}}\subseteq
L(\mathcal{T}_{\mathcal{G}},\mathcal{R})$. Consider now the infinity set
$\bar{n_{ij}}=\\{0,i,j\\}$ induced by some negative sample word $n_{ij}$.
Clearly we have that $\bar{n_{ij}}\cap E_{k}\neq\emptyset$ for all $k\leq 3$
as $c(v_{i})\neq c(v_{j})$, which is guaranteed by $c$ being a valid
$3$-coloring of $\mathcal{G}$. Thus $\mathcal{R}$ is indeed a Rabin condition
of size $3$ such that $\langle\mathcal{T}_{\mathcal{G}},\mathcal{R}\rangle$ is
consistent with $S_{\mathcal{G}}$.

For the other direction assume that a Rabin condition $\mathcal{R}$ of size
$3$ exists such that $\langle\mathcal{T}_{\mathcal{G}},\mathcal{R}\rangle$ is
consistent with $S_{V}$. We define a coloring $c:V\to\\{1,2,3\\}$ with
$c(v_{i})=\sigma$ for a $\sigma$ such that $i\notin E_{\sigma}$ and
$\\{0,i\\}\cap F_{\sigma}\neq\emptyset$, which clearly has to exist since
$p_{i}$ is accepted by $\langle\mathcal{T}_{\mathcal{G}},\mathcal{R}\rangle$.
To show that $c$ is a valid $3$-coloring of $\mathcal{G}$ let
$(v_{i},v_{j})\in E$ and assume to the contrary that $c(v_{i})=c(v_{j})$. Then
for the infinity set $\\{0,i,j\\}=\bar{n_{ij}}$ induced by the negative sample
word $n_{ij}$ and $k=c(v_{i})$ we have $\bar{n_{ij}}\cap E_{k}=\emptyset$ and
$\bar{n_{ij}}\cap F_{k}\neq\emptyset$. But this would imply $n_{ij}\in
L(\mathcal{T}_{\mathcal{G}},\mathcal{R})$ which contradicts consistency with
$S_{\mathcal{G}}$. Thus the assumption of $c(v_{i})=c(v_{j})$ must have been
incorrect and $c$ is indeed a valid $3$-coloring.

Membership in NP is again follows from the fact that consistency with $S$ is
verifiable in polynomial time through iterating over all sample words.

Using these hardness results we are now able to prove Theorem 3.9 which
establishes the complexity of all fixed-size consistency decision problems we
introduced.

See 3.9

######  Proof A.21.

Since the parity condition returned by $\operatorname{\mathsf{ParityCons}}$ is
optimal as established in Theorem 3.4, we can compare the number of distinct
priorities it uses to $k$ and thereby decide membership in $k$-Parity-
Consistency. By Theorem 3.4 this can be done in polynomial time. NP-
completeness of $k$-Rabin-Consistency and $k$-generalized Büchi-Consistency is
established in 3.7 and A.19 respectively.

##  Appendix B Passive learning

In the main part of the paper we introduced the
$\operatorname{\mathsf{Sprout}}$ algorithm for constructing deterministic
automata based on finite samples and mentioned that it defaults to extending
the transition system with disjoint loops once a certain threshold is
exceeded. We now give a formal definition of how this extension is constructed
and subsequently show that $\operatorname{\mathsf{Sprout}}$ returns an
automaton that is consistent with the given sample in polynomial time.

Assume that the algorithm has constructed a transition system
$\mathcal{T}=(Q,\Sigma,\varepsilon,\delta)$ for which it then encounters an
escape-prefix exceeding the defined threshold. To compute
$\operatorname{\mathsf{Extend}(\mathcal{T},S)}$ we first define a function

$E:Q\to\mathcal{P}(\Sigma^{\omega})\text{ with }E(q)=\\{av:uav\in S_{+}\text{
is escaping from }q\text{ with }a\\}$

which for each state $q\in Q$ returns the set of all exit strings that belong
to words from $S_{+}$ which escape $\mathcal{T}$ from $q$. We then construct a
transition system $\mathcal{T}^{\circlearrowleft}_{E(q)}$ in which exactly
those words that belong to $E(q)$ induce loops. To prevent acceptance of
unintended words, we additionally ensure that the initial state of
$\mathcal{T}^{\circlearrowleft}_{E(q)}$ is transient (meaning it is not
reachable from any state within $\mathcal{T}^{\circlearrowleft}_{E(q)}$).

In the following we denote by $\operatorname{\mathsf{Prf}}(L)$ for a
$L\subseteq\Sigma^{\omega}$ the set of all words $u\in\Sigma^{*}$ that are
prefix of some $w\in L$. Note that since the shortest escape-prefix in
$\mathcal{T}$ exceeded the threshold, all words in $E(q)$ must be of the form
$u^{\omega}$ for some $u\in\Sigma^{+}$ and we can write
$E(q)=\\{u_{1}^{\omega},\dotsc,u_{k}^{\omega}\\}$ with $u_{i}\in\Sigma^{+}$.
We now define the transition system
$\mathcal{T}^{\circlearrowleft}_{E(q)}=(Q^{\circlearrowleft}_{E(q)},\Sigma,q_{0},\delta^{\circlearrowleft}_{E(q)})$
with
$Q^{\circlearrowleft}_{E(q)}=\\{q_{0}\\}\cup\operatorname{\mathsf{Prf}}(E(q))$
and

$\delta^{\circlearrowleft}_{E(q)}(w,a)=\begin{cases}a&\text{ if }w=q_{0}\text{
and }a\in\Sigma\cap\operatorname{\mathsf{Prf}}({E(q)})\\\ \varepsilon&\text{
if }(wa)^{\omega}\in{E(q)}\\\ wa&\text{ if
}wa\in\operatorname{\mathsf{Prf}}(E(q))\\\ \bot&\text{ otherwise }\end{cases}$

It is easy to see that $q_{0}$ is indeed transient in
$\mathcal{T}^{\circlearrowleft}_{E(q)}$ and we can clearly find both a parity
and a Rabin condition such that every word in $E(q)$ induces an accepting run
in $\mathcal{T}^{\circlearrowleft}_{E(q)}$. By attaching the corresponding
$\mathcal{T}^{\circlearrowleft}_{E(q)}$ to each state $q$ for which $E(q)$ is
non-empty, we obtain a transition system in which no word from $S_{+}$ is
escaping.

###  B.1 Full proof of 4.1

We now give a proof for 4.1 from the main part of the paper.

See 4.1

######  Proof B.1.

As the initial transition system, $\mathcal{T}_{0}$, contains no transitions,
all words in $S=(S_{+},S_{-})$ are escaping. Since $S_{+}\cap S_{-}=\emptyset$
every pair of words in $S_{+}\times S_{-}$ must be distinguishable and thus
$\mathcal{T}_{0}$ is $\Omega$-consistent with $S$. Furthermore
$\operatorname{\mathsf{Sprout}}$ keeps only those transitions for which
$\Omega$-consistency with $S$ is maintained.

It is easy to see that calling $\operatorname{\mathsf{Extend}}$ once the
threshold is exceeded cannot lead to a violation of $\Omega$-consistency,
since no words from $S_{-}$ that were previously escaping can now induce
infinite runs. On the other hand no word from $S_{+}$ is escaping in the
extended transition system we obtain. Similarly if the threshold is not
exceeded, a point where $\operatorname{\mathsf{Escapes}}$ is empty must be
reached, also guaranteeing that no word in $S_{+}$ is escaping. Since we
showed the consistency algorithms from section 3 to be correct, we can thus
conclude that the automaton computed by $\operatorname{\mathsf{Aut}}$, which
is subsequently returned by $\operatorname{\mathsf{Sprout}}$, must be
consistent with $S$.

Assume now that $S_{+}$ consists of $n$ words and let $l_{b}$ and $l_{e}$ be
the maximal length of $u$ and $v$ for any $uv^{\omega}\in S$ respectively. In
the worst case $\operatorname{\mathsf{Sprout}}$ runs until the threshold
$T=l_{b}+l_{e}^{2}+1$ is exceeded. As the outer loop is executed no more than
$n\cdot T$ times and each iteration can lead to the introduction of at most
one new state, the size of the constructed transition system is bounded by
$n\cdot T$. Each state is checked as a potential transition target by the
inner loop, meaning it can be executed at most $n\cdot T$ times. We have shown
in subsection A.1 that the consistency check, which is run in each of these
iteration can be performed in polynomial time. Testing for all pairs of words
in $S_{+}\times S_{-}$ whether they are indistinguishable is also possible in
polynomial time. As computing the extended transition system once the
threshold is exceeded takes only linear time, the algorithm has an overall
polynomial complexity.

###  B.2 Full proof of Theorem 4.2

In this subsection we formalize the definition of characteristic samples based
on minimal (transition) representatives. Subsequently we show that in spite of
the introduced threshold, completeness for IRC is retained. Finally we
introduce characteristic samples for various acceptance condition types, which
ultimately allows the proof of See 4.2

We begin with an auxiliary statement that establishes a bound on the number of
positions of two distinct ultimately periodic words in reduced form that can
coincide.

######  Lemma B.2.

Let $uv^{\omega},xy^{\omega}\in\mathsf{UP}_{\Sigma}$ be two ultimately
periodic words in reduced form. If $uv^{\omega}\neq xy^{\omega}$ then they
must differ in one of the first $\max\\{|u|,|x|\\}+|v|\cdot|y|$ positions.

######  Proof B.3.

We associate with the two words a unique sequence
$\alpha\in(\Sigma\times\Sigma)^{\omega}$ such that
$\operatorname{\mathsf{proj}}_{1}(\alpha)=uv^{\omega}$ and
$\operatorname{\mathsf{proj}}_{2}(\alpha)=xy^{\omega}$ where
$\operatorname{\mathsf{proj}}_{i}((a_{1}^{1},a_{2}^{1}),(a_{1}^{2},a_{2}^{2}),\dotsc)=a_{i}^{1},a_{i}^{2},\dotsc$
for an infinite sequence of tuples refers to the projection onto its $i$-th
component. Let $n=\max\\{|u|,|x|\\}$ then due to the periodic nature of both
words we have that $\alpha_{n+i}=(v_{j},y_{k})$ with $j=(n+i-|u|)\bmod|v|$ and
$k=(n+i-|x|)\bmod|y|$. By considering the indices for letters of $v$ and $y$
that appear simultaneously in elements of $\alpha$, we can observe that they
are taken from the quotient rings $\mathbb{Z}/_{|v|\mathbb{Z}}$ and
$\mathbb{Z}/_{|y|\mathbb{Z}}$, which have cardinality $|v|$ and $|y|$
respectively. Therefore these indices must repeat with a period of at most
$m=|v|\cdot|y|$ and we have $\alpha_{n+i}=\alpha_{n+i+j\cdot m}$ for $i\leq m$
and all $j\in\mathbb{N}$. If there was a position $d>n+m$ in which the two
words differ, we could write $d=n+i+j\cdot m$ for a $j>0$ and $i<m$. But then
by our previous considerations the words must already have differed at the
position $d^{\prime}=n+i<n+m$, which consequently means if two words agree on
the first $n+m$ symbols then they are equal.

We now provide a formal definition of minimal (transition) representatives,
which are used in the subsequent construction of characteristic samples. To
that end we make use of the _congruence automaton_ $\mathcal{A}_{L}$ of an
$\Omega$-IRC language $L$ for $\Omega\in\mathsf{Acc}$. It consists of a
transition system
$\mathcal{T}_{L}=(Q_{L},\Sigma,[\varepsilon]_{\sim_{L}},\delta_{L})$ which is
augmented with an acceptance condition $\mathcal{C}_{L}$ of type $\Omega$ such
that $L(\mathcal{A}_{L})=L$. $\mathcal{T}_{L}$ has a state for each $\sim_{L}$
equivalence class and defines $\delta_{L}$ as
$\delta_{L}([u]_{\sim_{L}},a)=[ua]_{\sim_{L}}$.

The minimal representatives of an $\Omega$-IRC language $L$ correspond to the
minimal words in length-lexicographic order on which each class of $\sim_{L}$
(and thus state of $\mathcal{A}_{L}$) can be reached. Similarly, each minimal
transition representative corresponds to the length-lexicographically shortest
word on which a transition in $\mathcal{A}_{L}$ is reached. In the following
we use $\operatorname{\mathsf{Prf}}(L)$ for a language
$L\subseteq\Sigma^{\omega}$ to denote the set of all $u\in\Sigma^{*}$ that are
a prefix of some $w\in L$ and denote by $\prec$ the length-lexicographic
order.

######  Definition B.4 (Minimal Representatives).

Let $L\subseteq\Sigma^{\omega}$ be an $\Omega$-IRC language for some
$\Omega\in\mathsf{Acc}$. We define the set of _minimal representatives_

$\operatorname{\mathsf{MR}}(L)=\\{\hat{u}\in\operatorname{\mathsf{Prf}}(L):\text{
for all }v\sim_{L}\hat{u}\text{ we have }\hat{u}\prec v\\}$

as well as the set of _minimal transition representatives_

$\operatorname{\mathsf{MTR}}(L)=\\{\hat{u}a:\hat{u}\in\operatorname{\mathsf{MR}}(L),a\in\Sigma\text{
and }\hat{u}a\in\operatorname{\mathsf{Prf}}(L)\\}.$

We can now define a characteristic sample for $\sim_{L}$ based on which
$\operatorname{\mathsf{Sprout}}$ is then able to reconstruct the transition
system $\mathcal{T}_{L}$ underlying the congruence automaton
$\mathcal{A}_{L}$. To guarantee that all states and transitions of
$\mathcal{T}_{L}$ are inserted by $\operatorname{\mathsf{Sprout}}$, we require
each minimal (transition) representative to be a prefix of some word in
$S_{+}$. To prevent the algorithm from inserting wrong transitions, we add a
second requirement, through which separation of the $\sim_{L}$-classes is
ensured.

######  Definition B.5 (Characteristic Sample).

For an $\Omega$-IRC language $L$ with $\Omega\in\mathsf{Acc}$ we define the
sample $S_{\sim}=(S_{+},S_{-})$ to be the smallest sample satisfying the
following conditions:

  * •

for all $v\in\operatorname{\mathsf{MTR}}(L)$ there exists a
$w\in\Sigma^{\omega}$ such that $vw\in S_{+}$

  * •

for
$\hat{u}\in\operatorname{\mathsf{MR}}(L),v\in\operatorname{\mathsf{MTR}}(L)$
with $\hat{u}\not\sim_{L}v$ there exists some suffix $w\in\Sigma^{\omega}$
such that $\hat{u}w,vw\in S$ and $\hat{u}w\in S_{+}\Leftrightarrow vw\in
S_{-}$

A sample $S^{\prime}$ that extends $S_{\sim}$ is called _characteristic for_
$\sim_{L}$.

In the following proof we use $\mathcal{T}_{i}$ to denote the deterministic
transition system constructed in iteration $i$ of the
$\operatorname{\mathsf{Sprout}}$ algorithm called on a characteristic sample
$S=(S_{+},S_{-})$ for $\sim_{L}$. Note that the extension
$\operatorname{\mathsf{Sprout}}$ computes once the threshold is exceeded is
explicitly excluded from this sequence. We use the concept of injective
embeddings (which we define below) to show that each of these
$\mathcal{T}_{i}$ is structurally compatible with $\mathcal{T}_{L}$.

######  Definition B.6.

For two transition systems $\mathcal{T}$ and $\mathcal{T}$ we call
$\varphi:Q\hookrightarrow Q^{\prime}$ an _injective embedding of $\mathcal{T}$
in $\mathcal{T}^{\prime}$_ if $\varphi$ is injective,
$\varphi(q_{0})=q_{0}^{\prime}$ and for all $q\in Q,a\in\Sigma$ with
$\delta(q,a)\neq\bot$ we have
$\varphi(\delta(q,a))=\delta^{\prime}(\varphi(q),a)$.

We can now prove that there exists an injective embedding of each
$\mathcal{T}_{i}$ into $\mathcal{T}_{L}$, where $\mathcal{T}_{L}$ denotes the
transition system underlying $\mathcal{A}_{L}$. To simplify notation, we use
$\operatorname{\mathsf{Prf}}(L)$ for an $\omega$-language $L$ to denote the
set of all prefixes of a word in $L$.

######  Lemma B.7.

For all $i$ the mapping $\varphi_{i}:Q_{i}\to Q_{L}$ defined as
$\varphi(u)=\hat{u}$ for the minimal representative
$\hat{u}\in\operatorname{\mathsf{MR}}(L)$ with $\hat{u}\sim_{L}u$ is an
injective embedding.

######  Proof B.8.

We use induction to show a slightly stronger statement: For all $i$ the
function $\varphi_{i}$ is an injective embedding of $\mathcal{T}_{i}$ in
$\mathcal{T}_{L}$ and $Q_{i}\subseteq\operatorname{\mathsf{MR}}(L)$. Note that
for all $i$ it naturally holds that $\varphi_{i}$ maps the initial state
$\varepsilon$ of $\mathcal{T}_{i}$ to the initial state of $\mathcal{A}_{L}$.
In the base case for $i=0$ we know that $\mathcal{T}_{0}$ has no transitions
and thus $\varphi_{0}$ is an injective embedding. Since $\varepsilon$ must be
a minimal representative the second part of the statement holds as well.

Now let $i>0$ and assume that the statement holds for all $j<i$. Let $ua$ be
the escape-prefix in step $i$ of the algorithm. We know that
$\delta^{*}_{i-1}(\varepsilon,u)=\hat{u}\in Q_{i-1}$ and thus by the induction
hypothesis $\hat{u}\in\operatorname{\mathsf{MR}}(L)$ and
$\hat{u}a\in\operatorname{\mathsf{MTR}}(L)$. Because $\varphi_{i-1}$ is an
injective embedding we have $u\sim_{L}\hat{u}$ and thus
$\delta^{*}_{L}(\varepsilon,u)=\delta^{*}_{i-1}(\varepsilon,u)$. In the
following we consider the possible ways in which
$\operatorname{\mathsf{Sprout}}$ can extend the transition system
$\mathcal{T}_{i-1}$ and show that the statement holds for all of them.

For $\hat{w}\in Q_{i-1}$ and $\hat{w}\not\sim_{L}\hat{u}a$ we know by the
induction hypothesis that $\hat{w}\in\operatorname{\mathsf{MR}}(L)$. Since
$\hat{u}a\in\operatorname{\mathsf{MTR}}(L)$ we know by the second condition on
characteristic samples there exist separating words
$s_{+},s_{-}\in\\{\hat{u}axy^{\omega},\hat{w}xy^{\omega}\\}$ such that
$s_{+}\in S_{+}$ and $s_{-}\in S_{-}$. But then the addition of
$\hat{u}\xrightarrow{\scriptstyle{a}}\hat{w}$ would mean that
$\delta^{*}(\varepsilon,\hat{u}a)=\delta^{*}(\varepsilon,\hat{w})$ and after
reading $\hat{u}a$ and $\hat{w}$ the same state is reached in
$\mathcal{T}_{i}$. Therefore $s_{+}$ and $s_{-}$ either become inseparable or
induce the same infinity set in $\mathcal{T}_{i}$. Hence $\mathcal{T}_{i}$
cannot be $\Omega$-consistent with $S$ and no transition of the form
$\hat{u}\xrightarrow{\scriptstyle{a}}\hat{w}$ for a
$\hat{w}\not\sim_{L}\hat{u}a$ is inserted by $\operatorname{\mathsf{Sprout}}$.

In case a $\hat{v}\in Q_{i-1}$ with $\hat{v}\sim_{L}\hat{u}a$ exists then
$\delta_{L}(\hat{u},a)=\hat{v}$. If adding the transition
$\hat{u}\xrightarrow{\scriptstyle{a}}\hat{v}$ to $\delta_{i-1}$ would
introduce an inconsistency with $S$, then $\mathcal{A}_{L}$ would also be
inconsistent with $S$ as the transition
$\hat{u}\xrightarrow{\scriptstyle{a}}\hat{v}$ is also present in
$\mathcal{T}_{L}$. Because this is not the case we have
$\delta_{i}=\delta_{i-1}\cup\\{\hat{u}\xrightarrow{\scriptstyle{a}}\hat{v}\\}$.
Since $\varphi_{i-1}$ is an injective embedding by the induction hypothesis
and $\delta_{L}(\hat{u},a)=\hat{v}$, we can conclude that $\varphi_{i}$ is
also an injective embedding.

A new state $\hat{u}a$ is added if $\hat{w}\not\sim_{L}\hat{u}a$ for all
$\hat{w}\in Q_{i-1}$. We show that $\hat{u}a\in\operatorname{\mathsf{MR}}(L)$.
Then $\delta_{L}(\hat{u},a)=\hat{u}a$ and $\varphi_{i}$ is also an injective
embedding. Assume to the contrary that $\hat{w}\sim_{L}\hat{u}a$ for a
$\hat{w}\in\operatorname{\mathsf{MR}}(L)$ with $\hat{w}\prec\hat{u}a$, which
means $\hat{w}\in\operatorname{\mathsf{Prf}}(S_{+})$. Since the escape-
prefixes are considered in canonical order, however, we know that no prefix of
$\hat{w}$ can be escaping. Thus
$\delta^{*}_{i-1}(\varepsilon,\hat{w})=\hat{w}\in Q_{i-1}$, which is a
contradiction.

Now that we have established that $\operatorname{\mathsf{Sprout}}$ inserts
states and transitions in accordance to $\mathcal{T}_{L}$, we need to ensure
that this actually happens for _all_ states and transitions. Regular
termination (i.e. without exceeding the threshold) of the algorithm only
occurs if no word from $S_{+}$ is escaping. Since all minimal (transition)
representatives occur as prefixes of words in $S_{+}$, a complete
reconstruction of $\mathcal{T}_{L}$ is guaranteed in this case. We now
establish that the threshold we introduced was chosen to be large that all
minimal (transition) representatives are encountered before it is exceeded.

######  Lemma B.9.

For an $\Omega$-IRC language $L$ with $\Omega\in\mathsf{Acc}$ and a sample
$S=(S_{+},S_{-})$ that is characteristic for $\sim_{L}$ we have

$\operatorname{\mathsf{MR}}(L)\subseteq\left(\operatorname{\mathsf{Prf}}(S_{+})\cap\left(\bigcup_{i=0}^{k}\Sigma^{i}\right)\right)\text{
where }k=\max_{uv^{\omega}\in S}|u|+\left(\max_{uv^{\omega}\in
S}|v|\right)^{2}.$

######  Proof B.10.

We begin by considering the basic case of
$\varepsilon\in\operatorname{\mathsf{MR}}(L)$ and then proceed inductively.
Clearly we have $\varepsilon\in\operatorname{\mathsf{Prf}}(S_{+})$ and since
$|\varepsilon|=0$ the claim trivially holds. Now let
$\hat{u}a\in\operatorname{\mathsf{MR}}(L)$ be a minimal representative. The
minimality of $\hat{u}a$ guarantees that
$\hat{u}\in\operatorname{\mathsf{MR}}(L)$ and thus
$\hat{u}a\in\operatorname{\mathsf{MTR}}(L)$. By the first condition for
characteristic samples we know that $\hat{u}a$ must be the prefix of some word
in $S_{+}$. Thus it remains to be shown that $|\hat{u}a|\leq k$.

Because $\hat{u}a\in\operatorname{\mathsf{MR}}(L)$, we cannot have
$\hat{u}\sim\hat{u}a$ as this would contradict the minimality of $\hat{u}a$,
which means $\hat{u}\not\sim\hat{u}a$. Since $S$ is representative for $L$ we
know that a $w\in\Sigma^{\omega}$ exists such that $\hat{u}w,\hat{u}aw\in S$
and $\hat{u}w\in S_{+}\iff\hat{u}aw\in S_{-}$. These words share the common
prefix $\hat{u}$ and their opposing position in $S$ guarantees
$\hat{u}w\neq\hat{u}aw$. By B.2 we know that for the common prefix $\hat{u}$
of these two distinct sample words it must hold that $|\hat{u}|<k$. Hence we
have $|\hat{v}|\leq k$ for each minimal representative
$\hat{v}\in\operatorname{\mathsf{MR}}(L)$.

This bound guarantees that once the shortest escape prefix in length-
lexicographic order exceeds a length of $\max_{uv^{\omega}\in
S}|u|+\left(\max_{uv^{\omega}\in S}|v|\right)^{2}$, no additional minimal
representatives can be discovered. Since the difference between the longest
element in $\operatorname{\mathsf{MTR}}(L)$ and the longest element in
$\operatorname{\mathsf{MR}}(L)$ is at most one, every state and transition of
$\mathcal{T}_{L}$ must be discovered by $\operatorname{\mathsf{Sprout}}$
before the threshold is exceeded.

In the full proof of Theorem 4.2 we create a sample that is characteristic for
both the underlying transition system and the acceptance condition of a target
automaton. To prove that our consistency algorithms can accurately reconstruct
the acceptance condition in the presence of additional sample words, we
consider consistent extensions of characteristic samples which we define
below.

######  Definition B.11.

Let $S=(S_{+},S_{-})$ be a sample that is consistent with some language
$L\subseteq\Sigma^{\omega}$. We call
$S^{\prime}=(S^{\prime}_{+},S^{\prime}_{-})$ an _$L$ -consistent extension of
$S$_ if $S_{+}^{\prime}\supseteq S_{+}$ and $S_{-}^{\prime}\supseteq S_{-}$
and $S^{\prime}$ is consistent with $L$.

For each acceptance type $\Omega\in\mathsf{Acc}$ we now define a set words
that induce infinity sets based on which an $\Omega$-acceptance condition can
be fully reconstructed using the consistency algorithms outlined in section 3.
For every loop $S\subseteq Q\times\Sigma$ in a transition system $\mathcal{T}$
it is always possible to find an ultimately periodic word $w$ such that
$\operatorname{\mathsf{inf}}(\rho)=S$ where $\rho$ refers to the unique run of
$\mathcal{T}$ on $w$. This is guaranteed by the fact that the set of states
that occur on the loop $S$ must be strongly connected in $\mathcal{T}$.

######  Lemma B.12.

Let $C\subseteq Q$ be a strongly connected set of states in a deterministic
transition system $\mathcal{T}$. There exists an ultimately periodic word
$uv^{\omega}\in\Sigma^{\omega}$ such that $uv^{\omega}$ visits all transitions
in $C$ infinitely often and $|uv|$ is polynomial in the size of $\mathcal{T}$.

######  Proof B.13.

Fix some enumeration $\tau_{1},\tau_{2},\dotsc,\tau_{k}$ with
$\tau_{i}=(p_{i},a,q_{i})$ of all transitions with origin and target in $S$.
The number of these transitions is clearly bounded by $|Q|\cdot|\Sigma|$. Let
$u\in\Sigma^{*}$ be some word on which $p_{1}$ is reached from the initial
state. Clearly it holds that $|u|<|Q|$. We now construct words
$v_{2},v_{3},\dotsc,v_{k}$ such that $v_{i}=v_{i}^{\prime}a$ with
$\delta^{*}(q_{i},v_{i}^{\prime})=p_{i+1}$ and $\delta(p_{i+1},a)=q_{i+1}$ and
identify a word $v_{1}=v^{\prime}_{1}a$ such that
$\delta^{*}(q_{k},v^{\prime}_{1})=p_{1}$ and $\delta(p_{1},a)=q_{1}$. Since
$|C|\leq|Q|$ we know that $|v_{i}|\leq|Q|$ for all $i\leq k$. The
concatenation $v=v_{2}v_{3}\dotsc v_{k}v_{1}$ is bounded in length by
$|\Sigma|\cdot|Q|^{2}$ and forms a closed loop that visits all transitions in
$C$. Thus the word $uv^{\omega}$ visits all transitions in $C$ infinitely
often and is polynomial in the size of $\mathcal{T}$.

In the following we assume $\mathcal{T}$ to be a deterministic (partial)
transition system in which the respective acceptance conditions are defined.
To construct a sample $S_{F}=(S_{+},S_{-})$ characterizing a Büchi condition
$F\subseteq(Q\times\Sigma)$ we first remove from $\mathcal{T}$ all transitions
in $F$ and decompose the resulting transition system into its SCCs
$C_{1},\dotsc,C_{k}$. For each $C_{i}$ we identify a word $w_{i}$ visiting all
transitions in $C_{i}$ infinitely often, which is then added to $S_{-}$. As
$\operatorname{\mathsf{BuchiCons}}$ implicitly assumes $Q\times\Sigma$ to be
positive, we set $S_{+}=\emptyset$.

######  Lemma B.14.

Let $\mathcal{A}=\langle\mathcal{T},F\rangle$ be a DBA. The size of $S_{F}$ is
polynomial in $|Q|$ and for the partial condition
$\mathcal{H}=(\mathcal{H}_{0},\mathcal{H}_{1})$ induced by any
$L(\mathcal{A})$-consistent extension of $S_{F}$ we have
$L(\mathcal{T},F)=L(\mathcal{T},F^{\prime})$ with
$F^{\prime}=\operatorname{\mathsf{BuchiCons}}(\mathcal{H}_{0},\mathcal{H}_{1})$.

######  Proof B.15.

It is not difficult to see that $S_{F}$ contains at most one word per SCC and
is thus polynomial in $|Q|$. Further by B.12 each of these words is polynomial
in the size of $\mathcal{T}$.

Assume $w\in L(\mathcal{T},F)$ then for $D=\operatorname{\mathsf{inf}}(\rho)$
where $\rho$ is the unique run of $\mathcal{T}$ on $w$ we have that $D\cap
F\neq\emptyset$. For all negative elements
$C_{1},\dotsc,C_{k}\in\mathcal{H}_{1}$ we have $C_{i}\cap F=\emptyset$ and
hence $D\not\subseteq(C_{1}\cup\dotsc\cup C_{k})$. But as
$F^{\prime}=(Q\times\Sigma)\setminus(C_{1}\cup\dotsc\cup C_{k})$ we must have
$D\cap F^{\prime}\neq\emptyset$ and consequently $w\in
L(\mathcal{T},F^{\prime})$.

For the opposite direction assume $w\notin L(\mathcal{T},F)$ which means for
$D$ as chosen before we have $D\cap F=\emptyset$. This means that $D\subseteq
C_{i}$ for some SCC of $(Q\times\Sigma)\setminus F$ and as
$F^{\prime}\subseteq(Q\times\Sigma)\setminus C_{i}$, we have $D\cap
F^{\prime}=\emptyset$ and $w\notin L(\mathcal{T},F^{\prime})$.

To define the characteristic sample $S_{\mathcal{B}}=(S_{+},S_{-})$ of a
generalized Büchi condition $\mathcal{B}=\\{F_{1},\dotsc,F_{k}\\}$ with
$F_{i}\subseteq(Q\times\Sigma)$ we proceed in a similar way. For each
acceptance component $F_{i}$ we remove from $\mathcal{T}$ all transitions in
$F_{i}$ to obtain the transition system $\mathcal{T}_{i}$, which is then
decomposed into its SCCs $S_{1},\dotsc,S_{k}$. For each $S_{j}$ we add an
ultimately periodic word visiting all transitions in $S_{j}$ infinitely often
to $S_{-}$. Additionally for each accepting SCC $C$ of $\mathcal{T}$, a word
visiting all transitions in $C$ is added to $S_{+}$.

######  Lemma B.16.

Let $\mathcal{A}=\langle\mathcal{T},\mathcal{B}\rangle$ be a generalized Büchi
automaton then $S_{\mathcal{B}}$ for $\mathcal{B}=(F_{1},\dotsc,F_{k})$ is
polynomial in the size of $\mathcal{A}$ and $\mathcal{B}$. For the partial
condition $\mathcal{H}=(\mathcal{H}_{0},\mathcal{H}_{1})$ induced by any
$L(\mathcal{A})$-consistent extension of $S_{\mathcal{B}}$ we have
$L(\mathcal{T},\mathcal{B})=L(\mathcal{T},\mathcal{B}^{\prime})$ where
$\mathcal{B}^{\prime}=(F_{1}^{\prime},\dotsc,F^{\prime}_{l})$ represents the
generalized Büchi condition computed by
$\operatorname{\mathsf{genBuchiCons}}(\mathcal{H}_{0},\mathcal{H}_{1})$.

######  Proof B.17.

The sample $S_{\mathcal{B}}$ contains a word for each SCC of $\mathcal{T}$ and
each SCC of a $\mathcal{T}_{i}$. Clearly there are at most $|Q|$ SCCs in
$\mathcal{T}$ or any sub-transition system obtained by removing transitions.
Since we compute $k$ such sub-transition systems (one for each of the $k$ sets
in $\mathcal{B}$), the overall size of $S_{\mathcal{B}}$ is clearly polynomial
in $\mathcal{A}$ and $\mathcal{B}$. Additionally, the length of any word added
in this way is polynomial in the size of $\mathcal{T}$ by B.12.

Let $w\in L(\mathcal{T},\mathcal{B})$ and denote by $D$ the infinity set of
the unique run of $\mathcal{T}$ on $w$. We have $D\cap F_{i}\neq\emptyset$ for
$i\leq k$. Assume now that $w\notin L(\mathcal{T},\mathcal{B}^{\prime})$ which
would mean $D\cap((Q\times\Sigma)\setminus N_{i})=\emptyset$ for some
$\subseteq$-maximal negative loop $N_{i}\in\mathcal{H}_{1}$ and thus
$D\subseteq N_{i}$. Each $N_{i}$ must be an SCC in a $\mathcal{T}_{j}$ which
is obtained by removing from $\mathcal{T}$ all transitions in $F_{j}$. This,
however, would mean that neither $N_{i}$ nor $D$ can contain any transitions
belonging to $F_{j}$, which is a contradiction to $D$ satisfying
$\mathcal{B}$.

For the other direction assume that $w\notin L(\mathcal{T},\mathcal{B})$ which
means for $D$, the infinity set of the unique run of $\mathcal{T}$ on $w$,
there exists some index such that $D\cap F_{i}=\emptyset$. Thus $D\subseteq C$
for some SCC $C$ of $\mathcal{T}_{i}$, which we obtain by removing $F_{i}$
from $\mathcal{T}$. But then since $S_{-}$ contains an ultimately periodic
word inducing $C$ as its infinity set, we know that there must exist some
$F^{\prime}_{j}=(Q\times\Sigma)\setminus C$. Clearly we have $D\cap
F^{\prime}_{j}=\emptyset$, which then entails $w\notin
L(\mathcal{T},\mathcal{B}^{\prime})$.

Conveying sufficient information about a parity condition
$\kappa:Q\times\Sigma\to C$ in a sample $S_{\kappa}=(S_{+},S_{-})$ requires us
to identify the maximal positive and negative subloops, which might be nested
into each other. Our approach is similar to the one used in [4] to define a
characteristic sample for a parity condition and the decompositions used in
[9] for the minimization of a parity condition. The idea is to first decompose
the full transition system into its strongly connected components
$C_{1},\dotsc,C_{k}$. For each $C_{i}$ we then identify a word $w_{i}$
visiting all transitions in $C_{i}$ infinitely often. If the smallest priority
on those transitions is even, $w_{i}$ is added to $S_{+}$, otherwise it is
placed in $S_{-}$. Subsequently all transitions with the minimal priority are
removed to obtain the transition system $\mathcal{T}_{1}$. We proceed with
$\mathcal{T}_{1}$ in a similar way, by first decomposing it into its SCCs. For
each of these SCCs we identify a word that visits all transitions and add it
to the sample based on the least priority it sees. By repeating the removal
and decomposition until the largest priority in $C$ is reached, we cover each
maximal positive and negative loop in $\mathcal{A}$, which allows
$\operatorname{\mathsf{ParityCons}}$ to correctly reconstruct the acceptance
condition of $\mathcal{A}$.

######  Lemma B.18.

For a DPA $\mathcal{A}=\langle\mathcal{T},\kappa\rangle$ the sample
$S_{\kappa}$ is polynomial in the size of $\mathcal{A}$. Applying
$\operatorname{\mathsf{ParityCons}}$ to the partial condition
$\mathcal{H}=(\mathcal{H}_{0},\mathcal{H}_{1})$ induced by an
$L(\mathcal{A})$-consistent extension of $S_{\kappa}$ returns a parity
function $\kappa^{\prime}$ such that
$L(\mathcal{T},\kappa)=L(\mathcal{T},\kappa^{\prime})$.

######  Proof B.19.

During the computation of $S_{\kappa}$, we construct $k$ smaller transition
systems, each consisting of at most $|Q|$ SCCs. Since by B.12 the length of
each added word is polynomial in the size of $\mathcal{A}$ and thus the size
of $S_{\kappa}$ is thus clearly polynomial in the size of $\mathcal{A}$.

Let $w\in L(\mathcal{T},\kappa)$ then $m=\min(\kappa(D^{\prime}))$ is even for
the strongly connected set $D^{\prime}=\operatorname{\mathsf{inf}}(\rho)$
where $\rho$ refers to the unique run of $\mathcal{T}$ on $w$. This means that
$D^{\prime}\subseteq D$ for an SCC $D$ in $\mathcal{T}_{m}$ as
$\mathcal{T}_{m}$ contains all transitions with priority greater or equal to
$m$. If $\kappa^{\prime}$ falsely classified $D^{\prime}$ as negative then we
would have $D^{\prime}\subseteq N$ for a maximal negative subloop $N\subseteq
D$. As $m$ is even, this means $\min(\kappa(N))>m$. This is a contradiction
because at least one state in $D^{\prime}$ must have priority $m$ and thus
$D^{\prime}\not\subseteq N$ for all negative subloops $N$ of $D$. This by
definition means that $D^{\prime}$ is classified as positive by
$\kappa^{\prime}$ and thus $w\in L(\mathcal{T},\kappa^{\prime})$. The opposite
direction for a $w\notin L(\mathcal{T},\kappa)$ for which least priority that
is seen infinitely often is odd can be shown in an analogous way due to the
symmetry of parity conditions.

Similar to parity conditions, we define the characteristic sample for a Rabin
condition based on decompositions of restricted transition systems. We begin
by removing the set of all transitions that belong to $E_{i}$ of a pair
$(E_{i},F_{i})$ and decompose the resulting transition system into its SCCs
$C_{1},\dotsc,C_{k}$. If the set of all transitions $K_{i}$ in such an SCC
satisfies $\mathcal{R}$, we add a word $w_{i}$ inducing $K_{i}$ to $S_{+}$,
otherwise $w_{i}$ is added to $S_{-}$. For each accepting $K_{i}$ we then
remove all transitions in an $F_{j}$ such that $K_{i}\cap E_{j}=\emptyset$ at
the same time and decompose the resulting transition system into its SCCs
$D_{1},\dotsc,D_{l}$. These are the maximal negative subloops of $K_{i}$ and
for each $D_{j}$ a word visiting all transitions in $D_{j}$ is added to
$S_{-}$.

######  Lemma B.20.

Let $\mathcal{A}=\langle\mathcal{T},\mathcal{R}\rangle$ be a DRA with
acceptance component $\mathcal{R}$ and
$\mathcal{H}=(\mathcal{H}_{0},\mathcal{H}_{1})$ by the partial condition
induced by some $L(\mathcal{A})$-consistent extension of
$S_{\mathcal{R}}=(S_{+},S_{-})$. For the Rabin condition
$\mathcal{R}^{\prime}$ constructed by $\operatorname{\mathsf{RabinCons}}$ we
have $L(\mathcal{T},\mathcal{R})=L(\mathcal{T},\mathcal{R}^{\prime})$ and the
size of $S_{\mathcal{R}}$ is polynomial in the size of $\mathcal{A}$.

######  Proof B.21.

Each Rabin pair induces at most $2\cdot|Q|$ sample words. Since by B.12 we
know that the length of each sample word is polynomial in the size of
$\mathcal{T}$, we can conclude that the size of $S_{\mathcal{R}}$ is
polynomial in $\mathcal{A}$ and $\mathcal{R}$.

Let $w\in L(\mathcal{T},\mathcal{R})$ then for
$C=\operatorname{\mathsf{inf}}(\rho)$ where $\rho$ refers to the unique run of
$\mathcal{T}$ on $w$ we have that $C\cap E_{i}=\emptyset$ and $C\cap
F_{i}\neq\emptyset$ for some $i\leq|\mathcal{R}|$. This means $C\subseteq D$
for the set of all transitions $D$ in some SCC of the transition system
obtained by removing from $\mathcal{T}$ all transitions in $E_{i}$. Because
$C^{\prime}\cap F_{i}\neq\emptyset$ we know that $C$ satisfies $\mathcal{R}$
and hence $\mathcal{R}^{\prime}$ contains a pair $(E_{P},F_{P})$ with
$E_{P}=(Q\times\Sigma)\setminus D$ and $F_{P}=D\setminus(N_{1}\cup\dotsc\cup
N_{k})$ for the maximal negative subloops $N_{i}$ of $D$. Since clearly
$E_{P}\cap C=\emptyset$ it suffices to show that $F_{P}\cap C\neq\emptyset$.
Assume to the contrary that $F_{P}\cap C=\emptyset$, then $C\subseteq N_{i}$
for some maximal negative subloop of $D$. Each negative subloop of $D$ present
in the sample arose by by removing all transitions in an $F_{j}$ such that
$D\cap F_{j}\neq\emptyset$, which would mean that $N_{i}\cap F_{j}=\emptyset$.
But then as $C\subseteq N_{i}$ we would have $C\cap F_{i}=\emptyset$, which is