RWTH Aachen University, Ahornstr. 55, 52074 Aachen<EMAIL_ADDRESS>aachen.dehttps://orcid.org/0000-0003-0881-3199Supported by DFG grant LO
1174/7-1 RWTH Aachen University, Ahornstr. 55, 52074 Aachen,
Germanyloeding@cs.rwth-aachen.dehttps://orcid.org/0000-0002-1529-2806 Leon
Bohn and Christof Löding Theory of computation Automata over infinite objects
Mikołaj Bojańczyk, Emanuela Merelli, and David P. Woodruff 3 49th
International Colloquium on Automata, Languages, and Programming (ICALP 2022)
ICALP 2022 ICALP 2022 July 4–8, 2022 Paris, France 229 127

# Constructing Deterministic Parity Automata from Positive and Negative
Examples

León Bohn  Christof Löding

###### Abstract

We present a polynomial time algorithm that constructs a deterministic parity
automaton (DPA) from a given set of positive and negative ultimately periodic
example words. We show that this algorithm is complete for the class of
$\omega$-regular languages, that is, it can learn a DPA for each regular
$\omega$-language. For this purpose, we propose a canonical form of DPA, which
we call precise DPA (of a language), and show that it can be constructed from
the syntactic family of right congruences for that language (introduced by
Maler and Staiger in 1997). The precise DPA can be of exponential size
compared to a minimal DPA for a language, but it can also be a minimal DPA,
depending on the structure of the language. The upper bound that we obtain on
the number of examples required for our algorithm to find a DPA for $L$ is
therefore exponential in the size of a minimal DPA, in general. But we
identify two parameters of regular $\omega$-languages such that fixing these
parameters makes the bound polynomial.

###### keywords:

deterministic parity automata, learning from examples, learning in the limit

##  1 Introduction

Construction of deterministic finite automata (DFA) from labeled example words
is usually referred to as passive learning of automata, and has been studied
since the 1970s [7, 29, 17], see [20] for a survey. A passive learning
algorithm (passive learner for short) receives a sample $S=(S_{+},S_{-})$ of
positive and negative example words as input, and should return a DFA that
accepts all words in $S_{+}$ and rejects all words in $S_{-}$. In order to
find passive learners that are robust and generalize from the sample, Gold
proposed the notion of “learning in the limit” [16]. Given a class
$\mathcal{C}$ of regular languages, a learner is said to learn every language
in $\mathcal{C}$ in the limit, if for each language $L\in\mathcal{C}$ there is
a DFA $\mathcal{A}$ and a characteristic sample $S^{L}$ that is consistent
with $L$, such that the learner returns $\mathcal{A}$ for each sample that is
consistent with $L$ and contains all examples from $S^{L}$. In this case, we
also say that the learner is complete for the class $\mathcal{C}$.

In active DFA learning, the learning algorithm (referred to as active learner)
has access to an oracle for a regular target language $L$. Angluin proposed an
active learner that finds the minimal DFA for a target language $L$ in
polynomial time based on membership and equivalence queries [1]. A membership
query asks for a specific word if it is in the target language, and the oracle
answers “yes” or “no”. An equivalence query asks if a hypothesis DFA accepts
the target language, and the oracle provides a counterexample if it does not.

Starting from these first works on DFA learning, many variations of the basic
algorithms have been developed and were implemented in recent years, e.g., in
the framework learnlib [19] and the library flexfringe [31].

The key property that is used in most learning algorithms for regular
languages is the characterization of regular languages by the Myhill/Nerode
congruence: For a language $L$, two words $u,v$ are equivalent if for each
word $w$, either both $uw,vw$ are in $L$, or both are not in $L$. It is a
basic result from automata theory that $L$ is regular iff the Myhill/Nerode
congruence has finitely many classes, and that these classes can be used as
state set of the minimal DFA for $L$ (see basic textbooks on automata theory,
e.g. [18]). In particular, this means that two words can lead to the same
state if they cannot be separated by a common suffix. Based on this
observation, the transition structure of a minimal $n$ state DFA can be fully
characterized by a set of examples (words together with the information
whether they are in $L$ or not) whose size is polynomial in $n$.

In this paper, we consider the problem of constructing deterministic automata
on infinite words, so called $\omega$-automata, from examples. Automata on
infinite words have been studied since the early 1960s as a tool for solving
decision problems in logic [11] (see also [26]), and are nowadays used in
procedures for formal verification and synthesis of reactive systems (see,
e.g., [6, 28, 23] for surveys and recent work). But in contrast to standard
finite automata, very little is known about learning deterministic
$\omega$-automata.

The first problem, how to represent infinite example words, is easily solved
by considering ultimately periodic words. An infinite word is called periodic
if it is of the form $v^{\omega}$ for a finite word $v$, and ultimately
periodic if it is of the form $uv^{\omega}$ for finite words $u,v$. It is a
classical result that a regular $\omega$-language is uniquely determined by
the ultimately periodic words that it contains [11].

The main obstacle in learning deterministic $\omega$-automata is that there is
no Myhill/Nerode-style characterization of deterministic $\omega$-automata. It
is still true that two finite words $u,v$ that are separated by $L$ with a
common suffix $w$ (which is an infinite word in this case) have to lead to
different states in any deterministic $\omega$-automaton for $L$. But it is
not true anymore that all words that are not separated can all lead to the
same state. Currently, there are no active or passive polynomial time learners
that can infer a deterministic $\omega$-automaton for each regular
$\omega$-language. The existing algorithms either learn different
representations, use information about the target automaton (not just the
language), or can only learn subclasses of the regular $\omega$-languages:
There is an active learning algorithm for deterministic weak Büchi automata
[21], and passive learning algorithms [5, 8] that are only complete for
languages which can be accepted using an automaton with the Myhill/Nerode
congruence as transitions structure. The passive algorithm from [9] is
restricted to deterministic Büchi automata (and complete for that class). The
active learner from [3] uses a representation of $\omega$-languages called
families of DFAs. This representation of languages is based on the notion of
family of right congruences (FORC) [22], which we also use in an intermediate
step in this work. And in [24], the active learning algorithm uses some
additional information on the loop length in the target automaton.

In this paper, we focus on passive learning of deterministic parity automata
(DPA). We show that there is a polynomial time passive learner that can learn
a DPA for every regular $\omega$-language in the limit. To the best of our
knowledge, this is the first polynomial time passive learner for deterministic
$\omega$-automata that can learn every regular $\omega$-language in the limit.
In more detail, our contributions can be summarized as follows:

  1. 1.

We introduce a canonical DPA for a regular language $L$ that we call the
precise DPA. The priority assignment computed by this DPA corresponds to a
priority assignment that is obtained in a natural way by analyzing the
periodic parts (not ultimately periodic) of words in the language.

  2. 2.

We show how the precise DPA for $L$ can be constructed from another canonical
object, the syntactic FORC of $L$ [22]. While it is known that such a
construction must be exponential [2], our construction is only exponential in
the number of required priorities. In particular, it is polynomial (in the
size of the syntactic FORC) if the number of priorities is fixed.

  3. 3.

We present a polynomial time algorithm for constructing a consistent DPA from
given sets of positive and negative examples. The algorithm can be seen as an
extension of the algorithm from [9], which is for deterministic Büchi
automata. However, this extension has completely new parts that are based on
the insights on the precise DPA of a language and its construction from the
syntactic FORC. We show that this algorithm, in the limit, infers a DPA for
each regular $\omega$-language $L$ (either the precise DPA or a smaller one).
In general, our upper bound for the number of examples that is required for
inferring a DPA for $L$ is exponential in the size of a minimal DPA for $L$.
However, we identify two parameters of regular $\omega$-languages such that
the required data is polynomial if we fix these parameters. This generalizes
the currently known results for passive learning of deterministic
$\omega$-automata [5, 8, 9] to the class of all regular $\omega$-languages.

The paper is structured as follows. In Section 2 we introduce required
notation and results. In Section 3 we introduce the notion of precise DPA and
prove some results on this class of DPAs. In Section 4 we show how to
construct the precise DPA of a language from its syntactic FORC. In Section 5
we present the learning algorithm, and in Section 6 we conclude. The proofs of
all statements are given in the appendix.

##  2 Preliminaries

We use standard definitions and terminology from the theory of finite automata
and $\omega$-automata, and assume some familiarity with these concepts (see,
e.g., [27, 30, 32] for some background). An alphabet $\Sigma$ is a non-empty,
finite set of symbols. We use the standard notations
$\Sigma^{*},\Sigma^{\omega}$ for the sets of all finite words and all
$\omega$-words, respectively, and let
$\Sigma^{+}:=\Sigma^{*}\setminus\\{\varepsilon\\}$, where $\varepsilon$ is the
empty word, and $\Sigma^{\infty}:=\Sigma^{*}\cup\Sigma^{\omega}$. For
$u\in\Sigma^{*}$ we write $|u|$ for its length. A word $u\in\Sigma^{*}$ is
called _prefix_ of $v\in\Sigma^{\infty}$ if $v=ux$ for some
$x\in\Sigma^{\infty}$ and we write $u\sqsubseteq v$ in that case. For a word
$w\in\Sigma^{\infty}$ we write $\operatorname{\mathsf{Prf}}(w)$ for the set of
all prefixes of $w$, and for $X\subseteq\Sigma^{\infty}$ we write
$\operatorname{\mathsf{Prf}}(X)$ for the union of all
$\operatorname{\mathsf{Prf}}(x)$ for $x\in X$. For $u\in\Sigma^{*}$ and
$X\subseteq\Sigma^{\infty}$, we let $u^{-1}X:=\\{w\in\Sigma^{\infty}\mid uw\in
X\\}$. We use the _length-lexicographic (llex) ordering_ on finite words that
is based on some underlying ordering of the alphabet, and first compares words
by length, and words of same length in the lexicographic ordering.

We call $\sim\subseteq\Sigma^{*}\times\Sigma^{*}$ a _right congruence (RC)_ if
$\sim$ is an equivalence relation and $u\sim v$ implies $ua\sim va$ for all
$a\in\Sigma$. For a word $u\in\Sigma^{*}$, we use $[u]_{\sim}$ (just $[u]$ if
$\sim$ is clear from the context) to denote the _class_ of $u$ in $\sim$ and
write $[\sim]$ for the set of all classes in $\sim$. We say that _$\sim_{1}$
refines $\sim_{2}$_, written as $\sim_{1}\mathbin{\preceq}\sim_{2}$ if
$u\sim_{1}v$ implies $u\sim_{2}v$. We often use families indexed by classes of
an RC. In such cases we also use words as indices representing their class.
For example, if we have a family $(\gamma_{c})_{c\in[\sim]}$, then we often
write $\gamma_{u}$ to refer to $\gamma_{[u]_{\sim}}$. The size $|\sim|$ or
index of an RC $\sim$ is the number of its classes. In the following, we
tacitly assume that all considered RCs are of finite index, and not always
explicitly mention this.

A (deterministic) transition system (TS) $\mathcal{T}=(Q,\Sigma,\delta,\iota)$
over the finite alphabet $\Sigma$ consists of a finite, non-empty set of
states $Q$, a transition function $\delta:Q\times\Sigma\to Q$ and an initial
state $\iota\in Q$. We define $\delta^{*}:Q\times\Sigma^{*}\to Q$ inductively
by $\delta^{*}(q,\varepsilon)=q$ and
$\delta^{*}(q,aw)=\delta^{*}(\delta(q,a),w)$, and write $\delta^{*}(u)$ or
$\mathcal{T}(u)$ for $\delta^{*}(\iota,u)$. The _run_ of $\mathcal{T}$ on
$w=a_{0}a_{1}\ldots\in\Sigma^{\infty}$ from $q_{0}\in Q$ is a (possibly
infinite) sequence $q_{0}q_{1}\ldots$ with $q_{i+1}=\delta(q_{i},a_{i})$. We
write $\operatorname{\mathrm{Inf}}_{\mathcal{T}}(w)$ for the set of states
that occur infinitely often in the run of $\mathcal{T}$ on
$w\in\Sigma^{\omega}$, and $\operatorname{\mathrm{Inf}}_{\mathcal{T}}(X)$ for
the union of $\operatorname{\mathrm{Inf}}_{\mathcal{T}}(w)$ for $w\in X$. A
_strongly connected component (SCC)_ of $\mathcal{T}$ is a maximal strongly
connected set (with the usual definition). We write
$\text{SCC}_{\mathcal{T}}(q)$ for the SCC that contains $q$. A _partial TS_ is
a TS in which $\delta$ is a partial function.

An RC $\sim$ induces a TS
$\mathcal{T}_{\sim}=([\sim],\Sigma,[\varepsilon],\delta_{\sim})$, where
$\delta_{\sim}(c,a)=[ca]$ with $[ca]$ being the class of $ua$ for an arbitrary
$u\in c$. Vice versa, a transition system $\mathcal{T}$ gives rise to the
congruence $\sim_{\mathcal{T}}$, where $u\sim_{\mathcal{T}}v$ iff
$\mathcal{T}(u)=\mathcal{T}(v)$. So we interchange these objects and often
just speak of the TS $\sim$, meaning the TS $\mathcal{T}_{\sim}$.

For an RC $\sim$ and a class $c\in[\sim]$, we define
$E^{\sim}_{c}=\\{x\in\Sigma^{+}\mid cx\sim c\\}$ as the set of words that loop
on $c$. Often we omit the superscript $\sim$ if it is clear from the context.

A _language_ (over $\Sigma$) is a subset of $\Sigma^{*}$. A _deterministic
finite automaton (DFA)_ $\mathcal{D}$ consists of a transition system and a
subset $F\subseteq Q$ of final or accepting states. The accepted language is
$L(\mathcal{D})$ with the standard definition. An _$\omega$ -language_ is a
set $L\subseteq\Sigma^{\omega}$ of $\omega$-words. There are different
automaton models for defining the class of $\omega$-regular languages (see
[27, 30, 32]). We are interested in (transition-based) deterministic parity
automata defined below.

A _priority mapping_ is a function $\pi:\Sigma^{+}\to\\{0,\dotsc,k-1\\}$ for
some $k>0$. We overload notation and write $\pi(w)$ for $w\in\Sigma^{\omega}$
to denote the least $i$ such that $\pi(x)=i$ for infinitely many prefixes $x$
of $w$. The language $L(\pi)$ defined by $\pi$ is the set of all
$\omega$-words $w$ such that $\pi(w)$ is even. We call $\pi$ _weak_ if
$\pi(xy)\leq\pi(x)$ for all $x\in\Sigma^{+}$ and $y\in\Sigma^{+}$. If $\sim$
is a right congruence and $\pi_{c}$ for each $c$ is a weak priority mapping,
then $\overline{\pi}=(\pi_{c})_{c\in[\sim]}$ is called a _family of weak
priority mappings_ (FWPM).

A _deterministic parity automaton (DPA)_ is of the form
${\mathcal{A}}=(Q,\Sigma,\iota,\delta,\kappa)$ with a TS
$\mathcal{T}_{\mathcal{A}}=(Q,\Sigma,\iota,\delta)$ and a function
$\kappa:Q\times\Sigma\rightarrow\\{0,\ldots,k-1\\}$. It induces a priority
mapping ${\mathcal{A}}:\Sigma^{+}\rightarrow\\{0,\ldots,k\\}$ by
${\mathcal{A}}(ua):=\kappa(\delta^{*}(u),a)$ for $u\in\Sigma^{*}$ and
$a\in\Sigma$. The $\omega$-language $L({\mathcal{A}})$ accepted by
${\mathcal{A}}$ is the language of the induced priority mapping. The RC
$\sim_{\mathcal{A}}$ of ${\mathcal{A}}$ is the RC of its transition system. We
call an $\omega$-language regular if it is accepted by a DPA. The
Myhill/Nerode congruence $\sim_{L}$ for an $\omega$-language $L$ is the RC
defined by $u\sim_{L}v$ if $\forall w\in\Sigma^{\omega}:\,(uw\in
L\Leftrightarrow vw\in L)$. If $L$ is regular, then $\sim_{L}$ is of finite
index. For an RC $\sim$ that refines $\sim_{L}$ and $c\in[\sim]$ we let
$L_{c}:=u^{-1}L$ for an arbitrary $u\in c$.

For $u\in\Sigma^{+}$ and $q\in Q$ define
$\mathcal{A}_{\operatorname{\mathrm{min}}}(q,u)$ to be the minimal priority in
the run of ${\mathcal{A}}$ on $u$ from $q$. For a right congruence $\sim$ that
is refined by $\sim_{\mathcal{A}}$, and a class $c$ of $\sim$, we say that $q$
is a $c$-state if the words that lead to $q$ in ${\mathcal{A}}$ from the
initial state are in $c$.

The _parity complexity_ of a regular $\omega$-language $L$, denoted
$\operatorname{\mathsf{pc}}(L)$, is the least $k$ such that $L$ is accepted by
a DPA with priorities $\\{0,\ldots,k-1\\}$ (often one distinguishes also
whether the smallest priority required is $0$ or $1$, but we omit this for
simplicity). We call a DPA ${\mathcal{A}}=(Q,\Sigma,\iota,\delta,\kappa)$
_normalized_ if $\kappa$ is minimal in the following sense: For every
$\kappa^{\prime}:Q\times\Sigma\rightarrow\mathbb{N}$ with
$L((\mathcal{T}_{\mathcal{A}},\kappa^{\prime}))=L({\mathcal{A}})$, we have
$\kappa(q,a)\leq\kappa^{\prime}(q,a)$ for all $q$ and $a$. This unique minimal
priority function on $\mathcal{T}_{\mathcal{A}}$ can be computed in polynomial
time [13] (see also [15] for an adaption to transition-based DPAs). We refer
to this as _normalization of ${\mathcal{A}}$_.

Deterministic parity automata can also be viewed as Mealy machines (with the
priorities as output alphabet). Given a DPA ${\mathcal{A}}$, there is thus a
unique minimal DPA that induces the same priority mapping (when minimizing
${\mathcal{A}}$ as Mealy machine). Active learning algorithms for DFAs (as
described in the introduction) can be adapted to Mealy machines. In Section 5
we use the fact that there are polynomial time active learning algorithms for
Mealy machines that produce growing sequences of hypotheses (so their
hypotheses are always bounded by the target Mealy machine). See [25] for a
detailed introduction to Mealy machines, their minimization and active
learning.

For $v\in\Sigma^{+}$ we write $v^{\omega}$ for the _periodic_ $\omega$-word
$vvv\cdots$, and call an $\omega$-word _ultimately periodic_ if it is of the
form $uv^{\omega}$ for $u\in\Sigma^{*}$ and $v\in\Sigma^{+}$. It follows from
[11] that two regular $\omega$-languages are the same if they contain the same
ultimately periodic words, see also [12]. We use _$\omega$ -samples_ of the
form $S=(S_{+},S_{-})$, where $S_{\sigma}$ for $\sigma\in\\{+,-\\}$ is a
finite set of ultimately periodic words. For simplicity, we do not explicitly
distinguish ultimately periodic words and their representations, and
$uv^{\omega}\in S_{\sigma}$ means that some representation of that word is in
$S_{\sigma}$. We sometimes write $uv^{\omega}\in S$ for $uv^{\omega}\in
S_{+}\cup S_{-}$. A sample $S$ is consistent with $L$ if $L\cap
S_{-}=\emptyset$ and $S_{+}\subseteq L$.

A _passive learner_ (for DPAs) is a function $f$ that maps $\omega$-samples to
DPAs. $f$ is called a polynomial-time learner if $f$ can be computed in
polynomial time. A learner $f$ is _consistent_ if it constructs from each
$\omega$-sample $S=(S_{+},S_{-})$ a DPA ${\mathcal{A}}$ such that
$L({\mathcal{A}}$) is consistent with $S$. We say that $f$ can _learn every
regular $\omega$-language in the limit_ if for each such language $L$ there is
a _characteristic sample_ $S^{L}$ such that $L(f(S^{L}))=L$ and
$f(S^{L})=f(S)$ is the same DPA for all samples $S$ containing $S^{L}$ that
are consistent with $L$ and contains $S^{L}$. For a class $\mathcal{C}$ of
regular $\omega$-languages we say that $f$ can learn every language in
$\mathcal{C}$ in the limit _from polynomial data_ if the characteristic
samples for the languages in $\mathcal{C}$ are of polynomial size (in a
smallest DPA for the corresponding language).

##  3 Precise DPA of a language

In this section we introduce the precise DPA for a regular $\omega$-language
$L$ (Definition 3.13). We give a definition that is parameterized by a right
congruence $\sim$ of finite index that refines $\sim_{L}$, so there is a
precise DPA for $L$ and each such $\sim$. The precise DPA is then the one
where $\sim$ is the same as $\sim_{L}$. For defining the precise DPA, we first
introduce families of weak priority mappings that capture the periodic part of
the language $L$ wrt. $\sim$ (up to Lemma 3.9). Then we show how to combine
them into a single priority mapping (Definition 3.10, Lemma 3.11), and how to
build a DPA for this combined priority mapping (Lemma 3.12). We finish the
section with two observations on precise DPAs (Lemma 3.15, Theorem 3.16).
Because of space constraints we only have one running example. See Appendix
A.7 for another family of examples that might give some further intuition on
the precise DPA.

######  Definition 3.1.

Let $L$ be a regular $\omega$-language and $\sim$ be a right congruence that
refines $\sim_{L}$. For each class $c$ of $\sim$, we define

$\displaystyle P_{c,0}^{\sim}(L)$ $\displaystyle=\\{u\in\Sigma^{+}\mid\forall
x\in u^{-1}E_{c}\ (ux)^{\omega}\in L_{c}\\}$ $\displaystyle P_{c,i}^{\sim}(L)$
$\displaystyle=\\{u\in\Sigma^{+}\mid\forall x\in u^{-1}E_{c}\
\big{(}(ux)^{\omega}\in P^{\sim}_{c,i-1}(L)\Sigma^{\omega}\text{ or
}((ux)^{\omega}\in L_{c}\text{ iff }i\text{ is even})\big{)}\\}.$

######  Example 3.2.

Let $L\subseteq\\{a,b\\}^{\omega}$ consist of all $\omega$-words with finitely
many occurrences of $b$, or infinitely many occurrences of the infix $aba$. As
$\sim$ we take $\sim_{L}$, which has only one class (adding or removing finite
prefixes is irrelevant for membership in $L$). Then clearly all finite words
that contain the infix $aba$ are in $P_{\varepsilon,0}^{\sim}(L)$. If a finite
word contains $b$, then its iteration contains infinitely many $b$, so it is
not in $L$ except if its iteration also contains infinitely many $aba$, which
means it has a prefix in $P_{\varepsilon,0}^{\sim}(L)$. If a word does not
contain $b$, then its iteration is in the language because it contains
finitely many $b$. We thus obtain
$P_{\varepsilon,0}^{\sim}(L)=\Sigma^{*}aba\Sigma^{*}$,
$P_{\varepsilon,1}^{\sim}(L)=\Sigma^{*}b\Sigma^{*}$, and
$P_{\varepsilon,2}^{\sim}(L)=\Sigma^{+}$.

In Example 3.2 the sets are regular and the used indices $0,1,2$ naturally
correspond to the priorities that a DPA would use to accept the language (emit
priority $0$ whenever an infix $aba$ is detected, and priority $1$ for every
occurrence of $b$, and priority $2$ otherwise). We show that this is not a
coincidence by establishing a tight connection between the sets
$P^{\sim}_{c,i}(L)$ and the priorities visited by a normalized DPA for $L$.

######  Lemma 3.3.

Let ${\mathcal{A}}$ be a normalized DPA with priorities $\\{0,\dotsc,k-1\\}$
recognizing the language $L\subseteq\Sigma^{\omega}$ and $\sim$ be a right
congruence with
$\sim_{\mathcal{A}}\mathbin{\preceq}\sim\mathbin{\preceq}\sim_{L}$. Then for
each class $c$ of $\sim$ and each $i\geq 0$:
$P^{\sim}_{c,i}(L)=P^{\sim}_{c,i}({\mathcal{A}}):=\\{u\in\Sigma^{+}\mid\max\\{\mathcal{A}_{\operatorname{\mathrm{min}}}(q,u)\mid
q\text{ is $c$-state}\\}\leq i\\}$.

As consequence of Lemma 3.3, if $L$ is of parity complexity $k$, we obtain an
inclusion chain $P_{c,0}^{\sim}(L)\subseteq\cdots\subseteq
P_{c,k-1}^{\sim}(L)=\Sigma^{+}$ of regular sets, implying that the priority
mappings from the next definition are totally defined, weak, and can be
computed by Mealy machines.

######  Definition 3.4.

With the terminology from Definition 3.1 and $L$ of parity complexity $k$, we
represent the sets $P_{c,i}^{\sim}(L)$ for each class by a priority mapping
$\pi^{\sim}_{c}:\Sigma^{+}\rightarrow\\{0,\ldots,k-1\\}$ defined by
$\pi^{\sim}_{c}(u)=i$ for the minimal $i$ such that $u\in P_{c,i}^{\sim}(L)$.
We write $\overline{\pi^{\sim}}=(\pi^{\sim}_{c})_{c\in[\sim]}$ for the family
of these priority mappings, and refer to it as the _precise FWPM for $L$ and
$\sim$_.

With $L$ and $\sim$ as in Example 3.2, we obtain that
$\pi_{\varepsilon}^{\sim}(u)=0$ if $u$ contains $aba$,
$\pi_{\varepsilon}^{\sim}(u)=1$ if $u$ contains $b$ but not $aba$, and
$\pi_{\varepsilon}^{\sim}(u)=2$ otherwise. The left-hand side of Figure 1
shows a Mealy machine that computes $\pi_{\varepsilon}^{\sim}(u)$. We give a
bound on the size of Mealy machines for computing the precise FWPM, which can
be derived from Lemma 3.3.

$m_{\varepsilon}$$\scriptstyle{{\mathcal{M}}}$$m_{a}$$m_{b}$$m_{ab}$$m_{ba}$$m_{aba}$$a:2$$b:1$$a:2$$b:1$$b:1$$a:1$$a:0$$b:1$$a:1$$b:1$
$a:0$
---
$b:0$

$q_{0}$$\scriptstyle{\mathcal{D}_{0}}$$q_{2}$$q_{1}$$q_{3}$$a$$b$$a$$b$$a$$b$$a,b$$p_{0}$$\scriptstyle{\mathcal{D}_{1}}$$p_{2}$$p_{1}$$a$$b$$a$$b$$a,b$

$q_{0},p_{0}$$\scriptstyle{{\mathcal{A}}}$$q_{1},p_{1}$$q_{2},p_{0}$$a:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}2}$$b:{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}$$a:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}2}$$b:{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}$
$a:{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}0}$
---
$b:{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}$

Figure 1: On the left-hand side a Mealy machine ${\mathcal{M}}$ that computes
$\pi_{\varepsilon}^{\sim}$ for $L$ and $\sim$ from Example 3.2. The DFAs
$\mathcal{D}_{i}$ for $i\in\\{0,1\\}$ represent the words that are assigned
priority $\leq i$ by ${\mathcal{M}}$. On the right-hand side the precise DPA
that is obtained from the $\mathcal{D}_{i}$.

######  Theorem 3.5.

Let ${\mathcal{A}}$ be a normalized DPA with $n$ states and $k$ priorities
that recognizes $L$, and $\sim$ be a right congruence with
$\sim_{\mathcal{A}}\mathbin{\preceq}\sim\mathbin{\preceq}\sim_{L}$. Then for
each class $c$ of $\sim$, the mapping $\pi_{c}^{\sim}$ can be computed by a
Mealy machine ${\mathcal{M}}_{c}$ with at most $(nk)^{d}$ states, where $d$ is
the number of $c$-states in ${\mathcal{A}}$.

To justify the name “precise” as introduced in Definition 3.4, we show that
$\overline{\pi^{\sim}}$ is the least weak priority mapping that describes the
loops on the classes of $\sim$ wrt. the language $L$.

######  Definition 3.6.

We say (with the terminology from Definition 3.1) that an FWPM
$(\gamma_{c})_{c\in[\sim]}$ _captures the periodic part of $(L,\sim)$_, if for
all classes $c\in[\sim]$ and $v\in E_{c}$ holds that $v^{\omega}\in L_{c}$ iff
$v^{\omega}\in L(\gamma_{c})$. And we partially order FWPMs by point wise
comparison, that is, for two FWPMs
$\overline{\gamma}=(\gamma_{c})_{c\in[\sim]}$ and
$\overline{\gamma}^{\prime}=(\gamma^{\prime}_{c})_{c\in[\sim]}$ we let
$\overline{\gamma}\leq\overline{\gamma}^{\prime}$ if for all classes $c$ of
$\sim$ and $u\in\Sigma^{+}$ holds $\gamma_{c}(u)\leq\gamma_{c}^{\prime}(u)$.

######  Lemma 3.7.

Let $L$ be a regular $\omega$-language and $\sim$ refine $\sim_{L}$. The
family $\overline{\pi^{\sim}}=(\pi_{c}^{\sim})_{c\in[\sim]}$ captures the
periodic part of $(L,\sim)$. Furthermore, it is the unique least such FWPM.

The fact that $\overline{\pi^{\sim}}$ is the least FWPM that captures the
periodic part of $(L,\sim)$ somehow means that each $\pi_{c}^{\sim}(u)$ gives
the most precise information wrt. $L$ for words that loop on $c$ and start
with $u$. Hence, the name “precise FWPM”. The precise DPA for $L$ and $\sim$
that we introduce below is derived from this precise FWPM for $L$ and $\sim$.
In general, for the construction of a DPA from a FWPM that captures the
periodic part of $(L,\sim)$, it is important that the individual priority
mappings are compatible with each other. Specifically, adding a prefix to a
word should only lead to a smaller (i.e. more significant) priority. This is
expressed formally in the following definition.

######  Definition 3.8.

We call a FWPM $\overline{\gamma}=(\gamma_{c})_{c\in[\sim]}$ _monotonic_ if
$\gamma_{u}(vx)\leq\gamma_{uv}(x)$ for all $u,v\in\Sigma^{*},x\in\Sigma^{+}$.

######  Lemma 3.9.

Let $L$ be a regular $\omega$-language, and $\sim$ refine $\sim_{L}$. The
precise FWPM $\overline{\pi^{\sim}}$ of $(L,\sim)$ is monotonic.

#### The Precise DPA.

Our goal is now to construct from a monotonic FWPM
$\overline{\gamma}=(\gamma_{c})_{c\in[\sim]}$ that captures the periodic part
of $(L,\sim)$ a combined priority mapping ${\gamma}_{\bowtie}$ that defines
$L$. We refer to ${\gamma}_{\bowtie}$ as the _join of $\overline{\gamma}$_.

For an ultimately periodic word $xy^{\omega}$ with $x\sim xy$, we know that
$\gamma_{x}(y^{\omega})$ is an even priority iff $xy^{\omega}\in L$ (from the
fact that $\overline{\gamma}$ captures the periodic part of $(L,\sim)$). The
problem is that ${\gamma}_{\bowtie}$ does not “know” when the periodic part of
an ultimately periodic word starts. So the priority ${\gamma}_{\bowtie}(u)$
for a finite word $u$ should take into account all possible prefixes of $u$ as
potential starting points of the periodic part. That means that for every
possible division $u=xy$, the value $\gamma_{x}(y)$ has to be taken into
account. We capture this with the following definitions (where we refer to
partial priority mappings because we are going to define ${\gamma}_{\bowtie}$
inductively, and need to refer to properties of the partially defined
mapping). While the definition is quite natural, it is a bit technical to
write, so we encourage the reader to look at the example after the definition.

######  Definition 3.10.

Let $u\in\Sigma^{+}$ and $\gamma$ be a partial priority mapping that is
defined for all non-empty prefixes of $u$. Let $y$ be a non-empty suffix of
$u$, that is $u=xy$ for an $x\in\Sigma^{*}$. We say that $\gamma$ _covers_
$\overline{\gamma}$ on the suffix $y$ of $u$ if $\gamma(xz)\leq\gamma_{x}(y)$
for some non-empty prefix $z$ of $y$.

The priority mapping ${\gamma}_{\bowtie}$ is defined inductively as follows.
Assume that ${\gamma}_{\bowtie}$ has been defined for all non-empty prefixes
of $u\in\Sigma^{*}$, and let $a\in\Sigma$. Then ${\gamma}_{\bowtie}(ua)$ is
the maximal value such that ${\gamma}_{\bowtie}$ covers $\overline{\gamma}$ on
all non-empty suffixes of $ua$.

$\begin{array}[]{rccccc}u:&a&b&a&b&a\\\ \hline\cr\pi^{\sim}_{c}:&2&1&0&0&0\\\
&&1&1&1&0\\\ &&&2&1&0\\\ &&&&1&1\\\ &&&&&2\\\
\hline\cr{\pi}_{\bowtie}^{\sim}:&2&1&0&1&2\end{array}$

Consider the FWPM $\overline{\pi^{\sim}}$ for $L$ and $\sim$ from Example 3.2,
where $\sim$ has a single class $c$, and $\pi^{\sim}_{c}(u)$ is $0$ if $u$
contains $aba$, $1$ if $u$ contains $b$ but not $aba$, and $2$ otherwise. Now
take the word $u=ababa$. The table on the right shows the $\pi^{\sim}_{c}$
values for the different suffixes of $u$, and the resulting
${\pi}_{\bowtie}^{\sim}$-values. For finding ${\pi}_{\bowtie}^{\sim}(u)$, we
have to consider the $\pi^{\sim}_{c}$-values of all suffixes of $u$, which
corresponds to the last column of the $\pi^{\sim}_{c}$-values. The top three
entries in this column are $0$, corresponding to
$\pi^{\sim}_{c}(ababa),\pi^{\sim}_{c}(baba),\pi^{\sim}_{c}(aba)$. All of these
suffixes are already covered by ${\pi}_{\bowtie}^{\sim}(aba)=0$. Furthermore,
$\pi^{\sim}_{c}(ba)=1$ (corresponding to the fourth entry in the last column)
is already covered by ${\pi}_{\bowtie}^{\sim}(abab)=1$. Hence, it only remains
to cover the suffix $a$ with the value $\pi^{\sim}_{c}(a)=2$. The maximal
value for covering this is $2$ itself, so we set
${\pi}_{\bowtie}^{\sim}(ababa)=2$.

######  Lemma 3.11.

Let $L$ be an $\omega$-regular language and $\sim$ refine $\sim_{L}$. If
$\overline{\gamma}$ is a monotonic FWPM that captures the periodic part of
$(L,\sim)$, then $L({\gamma}_{\bowtie})=L$. In particular,
$L({\pi}_{\bowtie}^{\sim})=L$.

We now explain how to construct a DPA that computes the priority mapping
${\gamma}_{\bowtie}$ if $\overline{\gamma}$ is a monotonic FWPM given by a
family $\overline{{\mathcal{M}}}=({\mathcal{M}}_{c})_{c\in[\sim]}$ of Mealy
machines. This DPA, which we denote DPA by
${{\mathcal{A}}}_{\bowtie}(\overline{\mathcal{M}})$, has one component for
tracking $\sim$, and one component for each priority $i$ that checks if there
is a suffix of the input read so far that has to be covered and produces
priority $i$. The minimal such $i$ is emitted as priority, and all components
for priorities $\geq i$ are reset to start tracking suffixes from this point.
Note that the construction can be applied even if ${\gamma}_{\bowtie}$ is not
monotonic (but then we do not have any guarantees on the behavior of the
resulting DPA). We formalize this below.

Assume that the range of the mappings in $\overline{\gamma}$ is
$\\{0,\ldots,k-1\\}$. First, we extract for each priority
$i\in\\{0,\ldots,k-1\\}$ from each Mealy machine ${\mathcal{M}}_{c}$ a DFA
$\mathcal{D}_{c,i}=(Q_{c,i},\Sigma,\iota_{c,i},\delta_{c,i},F_{c,i})$ with
$L(\mathcal{D}_{c,i})=\\{u\in\Sigma^{+}\mid\gamma_{c}(u)\leq i\\}$. This is
achieved by taking the transition structure of ${\mathcal{M}}_{c}$ and
redirecting all transitions with output $\leq i$ into an accepting sink state
(recall that $\gamma_{c}$ is weak), and then minimizing the resulting DFA.
This step is illustrated in Figure 1, where the class index is omitted because
there is only one class. Note that the DFA $\mathcal{D}_{c,k-1}$ always
accepts every non-empty word, so it is omitted in the example. However, it is
convenient to keep it in the formal construction.

To simplify notation, we assume that the $Q_{c,i}$ are pairwise disjoint,
allowing us to write $\delta(q,a)$ and $q\in F$ to refer to
$\delta_{c,i}(q,a)$ resp. $q\in F_{c,i}$ for the unique $c\in[\sim]$ and $i<k$
such that $q\in Q_{c,i}$. We now define the DPA
${{\mathcal{A}}}_{\bowtie}(\overline{\mathcal{M}})=({Q}_{\bowtie},\Sigma,{\iota}_{\bowtie},{\delta}_{\bowtie},{\kappa}_{\bowtie})$
with

${Q}_{\bowtie}=Q_{0}\times\cdots\times Q_{k-1}\times Q_{\sim},\ \text{where}\
Q_{i}=\bigcup_{c\in[\sim]}(Q_{c,i}\setminus F_{c,i})\ \text{and}\
{\iota}_{\bowtie}=(\iota_{[\varepsilon],0},\dotsc,\iota_{[\varepsilon],k-1},[\varepsilon]).$

In this product, we refer to the $i$th component as the _component for
priority $i$_ for $i\in\\{0,\ldots,k-1\\}$. For each transition from some
state $\tilde{q}=(q_{0},\dotsc,q_{k-1},c)\in Q$ on a symbol $a\in\Sigma$, we
begin by computing the reset point $r<k$, which corresponds to the least index
of a DFA that reaches a final state, meaning formally
$r=\operatorname{\mathrm{min}}\\{i<k\mid\delta(q_{i},a)\in F\\}$. Note that
$r$ is always defined because the DFA for priority $k-1$ accepts everything.

The reset point directly determines the priority of the transition, meaning
${\kappa}_{\bowtie}(\tilde{q},a)=r$.
For computing the target of the transition, we first advance each $q_{j}$ for
$j<r$ by $a$ in the respective DFA and then reset all other states to the
initial state of the appropriate DFA, i.e.

${\delta}_{\bowtie}(q_{0},\dotsc,q_{k-1},c)=(\delta(q_{0},a),\dotsc,\delta(q_{r-1},a),\iota_{c^{\prime},r},\dotsc,\iota_{c^{\prime},k-1},c^{\prime})\quad\text{where
}c^{\prime}=[ca]_{\sim}.$

In Figure 1 the resulting DPA is shown on the right-hand side. We omit the
component for the $\sim$-class and the component for priority $2$, because
they both only consists of one state.

The following lemma establishes that
${{\mathcal{A}}}_{\bowtie}({\mathcal{M}})$ indeed computes the join.

######  Lemma 3.12.

If $\overline{\mathcal{M}}$ is a family of Mealy machines representing a
monotonic FWPM $\overline{\gamma}$, then
${{\mathcal{A}}}_{\bowtie}(\overline{\mathcal{M}})(u)={\gamma}_{\bowtie}(u)$
for each $u\in\Sigma^{+}$. In particular,
$L({{\mathcal{A}}}_{\bowtie}(\overline{\mathcal{M}}))=L({\gamma}_{\bowtie})$.

We know from Theorem 3.5 that the precise FWPM $\overline{\pi^{\sim}}$ for
$(L,\sim)$ can be computed by a family of Mealy machines. This enables us now
to define the central object of this section.

######  Definition 3.13.

Let $L$ be a regular $\omega$-language, and let $\sim$ be a right congruence
that refines $\sim_{L}$. The _precise DPA ${\mathcal{A}}_{L,\sim}$ for
$(L,\sim)$_ is the minimal DPA whose priority mapping is the join
${\pi}_{\bowtie}^{\sim}$ of the precise FWPM $\overline{\pi^{\sim}}$ for
$(L,\sim)$. The _precise DPA ${\mathcal{A}}_{L}$ for $L$_ is
${\mathcal{A}}_{L,\sim_{L}}$.

The DPA on the right-hand side of Figure 1 is minimal as Mealy machine, so it
is the precise DPA for the language from Example 3.2.

Note that $L({\mathcal{A}}_{L,\sim})=L$ because the precise FWPM
$\overline{\pi^{\sim}}$ for $L$ and $\sim$ captures the periodic part of
$(L,\sim)$ according to Lemma 3.7, and hence $L({\pi}_{\bowtie}^{\sim})=L$ by
Lemma 3.11. Since, by definition, the priority mapping of
${\mathcal{A}}_{L,\sim}$ is ${\pi}_{\bowtie}^{\sim}$, we obtain that
$L({\mathcal{A}}_{L,\sim})=L$. Furthermore, given an arbitrary DPA
${\mathcal{A}}$ for $L$, and $\sim$ given as transition system, one can
construct ${\mathcal{A}}_{L,\sim}$ as follows: Take the product of
${\mathcal{A}}$ and $\sim$ in order to ensure that $\sim_{\mathcal{A}}$
refines $\sim$. Then normalize the result and construct a family
$\overline{\mathcal{M}}$ of Mealy machines representing the precise FWPM
${\pi}_{\bowtie}^{\sim}$ for $(L,\sim)$ according to Theorem 3.5. Then
construct ${{\mathcal{A}}}_{\bowtie}(\overline{{\mathcal{M}}})$ and minimize
it as a Mealy machine. For use in the Section 5, we give an upper bound on the
size of the precise DPA resulting from this construction. See Appendix A.7 for
an example that the precise DPA can be exponential compared to a minimal DPA.

######  Theorem 3.14.

Let ${\mathcal{A}}$ be a DPA with $n$ states and priorities in
$\\{0,\ldots,k-1\\}$ accepting some language $L$. If ${\mathcal{A}}$ has for
each class $c$ of $\sim_{L}$ at most $d$ many $c$-states, then
$|{\mathcal{A}}_{L}|\leq(nk)^{k(d+1)}$.

The construction of the precise DPA for $L$ sets out a rough road map for the
construction of a DPA from a collection $S$ of positive and negative example
words: Extract a right congruence $\sim$ from $S$ as candidate for $\sim_{L}$
(this is known how to do it). Then extract Mealy machines
$\overline{{\mathcal{M}}}$ that capture the periodic part of $S$ and $\sim$.
Construct ${{\mathcal{A}}}_{\bowtie}(\overline{{\mathcal{M}}})$.

In Section 4 we present some results that enable us to realize the extraction
of Mealy machines. The problem with the last step is that the size of
${{\mathcal{A}}}_{\bowtie}(\overline{{\mathcal{M}}})$ is of order
$|\overline{{\mathcal{M}}}|^{k}$, where $k$ is the number of priorities. In a
polynomial time procedure we thus cannot simply construct
${{\mathcal{A}}}_{\bowtie}(\overline{{\mathcal{M}}})$ from the Mealy machines
because this would result in an exponential step. The following lemma helps us
to solve this problem (the details how it is used are given in Section 5).
Note that the FWPM in the lemma is not required to be monotonic.

######  Lemma 3.15.

Let $u\in\Sigma^{*},v\in\Sigma^{+}$ and $\overline{\mathcal{M}}$ be a family
of mealy machines computing an FWPM $\overline{\gamma}$. The sequence of
priorities produced by ${{\mathcal{A}}}_{\bowtie}(\overline{\mathcal{M}})$ on
$uv^{\omega}$ can be written as an ultimately periodic word $rs^{\omega}$
where $|rs|$ is polynomial in $|uv|$ and $|\overline{\mathcal{M}}|$.
Furthermore, $r,s$ can be computed in polynomial time.

Finally, as a side remark, we mention that a precise DPA
${\mathcal{A}}_{L,\sim}$ needs not to be normalized, in general. As an
example, consider the precise DPA from Figure 1. The $a$-transition from
$(q_{0},p_{0})$ to $(q_{1},p_{1})$ has priority $2$, but it could be assigned
priority $1$ without changing the accepted language. Thus, this DPA is not
normalized. While this seems to be an argument against precise DPAs as
canonical objects, in this specific example there is actually no reason,
besides normalization, to assign priority $1$ to that transition, since the
letter $a$ does not “contribute to a word not being in $L$”. So $2$ seems to
be the more natural priority for this transition. It turns out that the class
of precise DPAs for a language $L$ (recall that there is a precise DPA for
each $\sim$ that refines $\sim_{L}$) subsumes the class of normalized DPAs for
$L$ in the following sense:

######  Theorem 3.16.

If a DPA ${\mathcal{A}}$ for $L$ is normalized and minimal as Mealy machine,
then ${\mathcal{A}}$ is the precise DPA for $(L,\sim_{\mathcal{A}})$.

##  4 Families of Right Congruences

In Section 3 we have seen that we can construct a DPA for $L$ from $\sim_{L}$
or any right congruence $\sim$ that refines $\sim_{L}$, and from Mealy
machines for the colorings
$\overline{\pi}^{\sim}=(\pi^{\sim}_{c})_{c\in[\sim]}$. Our goal is to learn
such Mealy machines from given examples. For this purpose, we explain in this
section how to define the Mealy machines using the formalism of families of
right congruences (FORCs) [22]. We start by giving some intuition, why and how
we use this formalism, and then go into the formal details.

The usual way to obtain a method that can construct a class of transition
systems in the limit from examples, is to characterize them by a right
congruence on finite words, such that non-equivalence of two words is
witnessed by a finite set of positive and negative examples for $L$. For
example, the non-equivalence of $x,y$ for $\sim_{L}$ is witnessed by two
examples $xuv^{\omega}\in L\Leftrightarrow yuv^{\omega}\not\in L$. Then an
appropriate method can extract the desired transition system if enough non-
equivalences are specified by the examples. We did not manage to characterize
the transition structure of a minimal Mealy machine for a coloring
$\pi^{\sim}_{c}$ in such a way. To illustrate this, consider the case that
$\sim=\sim_{L}$ has only one class $c$, and that only the priorities $0$ and
$1$ are used. A minimal Mealy machine for $\pi^{\sim}_{c}$ consists of an
initial part that assigns $1$ to the words in $P_{1}(L)$, and a sink state
that that is reached for all words in $P_{0}(L)$. So two words $x,y$ lead to
different states in this Mealy machine iff there is an extension $z$ with
($xz\in P_{0}(L)\Leftrightarrow yz\not\in P_{0}(L)$). Substituting the
definition of $P_{0}(L)$, we obtain that $x$ and $y$ lead to a different state
iff $\exists z\in\Sigma^{*}:\,(\forall
z^{\prime}\in\Sigma^{*}:\,(xzz^{\prime})^{\omega}\in L)\Leftrightarrow(\exists
z^{\prime}\in\Sigma^{*}:\,(yzz^{\prime})^{\omega}\not\in L).$

This characterization of non-equivalence has a universal quantifier, and thus
cannot be witnessed by a finite set of examples. However, we can use a
condition that is implied by the above one, which means that we characterize a
possibly larger transition system. If $x$ and $y$ satisfy the above non-
equivalence condition, then, in particular, there are
$z,z^{\prime}\in\Sigma^{*}$ with $(xzz^{\prime})^{\omega}\in
L\Leftrightarrow(yzz^{\prime})^{\omega}\not\in L$. Rewriting this with a
single word $z$ instead of $zz^{\prime}$, we get the condition $\exists
z\in\Sigma^{*}:\,(xz)^{\omega}\in L\Leftrightarrow(yz)^{\omega}\not\in L$ for
non-equivalence of $x$ and $y$, which is implied by the first condition.
Generalizing this to a right congruence $\sim$ with several classes, directly
leads to the notion of a canonical FORC for $\sim$, as defined below.

A _family of right congruences (FORC)_ [22] is a tuple
$\mathcal{F}=(\sim,(\approx_{c})_{c\in[\sim]})$ such that $\sim$ is a right
congruence over $\Sigma^{*}$, each $\approx_{c}$ for $c\in[\sim]$ is a right
congruence over $\Sigma^{+}$, and for all $x,y\in\Sigma^{*}$ and $c\in[\sim]$
it holds that $x\approx_{c}y$ implies $ux\sim uy$, for an arbitrary element
$u\in c$. Instead of writing $\approx_{c}$ for a class $c$, we sometimes also
write $\approx_{u}$ for an arbitrary word $u\in c$. We extend $\approx_{c}$
from $\Sigma^{+}$ to $\Sigma^{*}$ by adding a new class that contains only
$\varepsilon$.

Adopting the terminology of [3], we call $\sim$ the _leading right congruence_
(LRC) of $\mathcal{F}$, and each $\approx_{c}$ the _progress right congruence_
(PRC) for $c$. FORCs can be used as acceptors for $\omega$-languages (see [22,
3]) but since this is not relevant for our results, so we not go into the
details of it. We are interested in the _canonical FORC_ for
$L\subseteq\Sigma^{\omega}$ and an LRC $\sim$ that refines $\sim_{L}$. For
$u\in\Sigma^{*}$, we define the _canonical PRC_ $\simeq_{u}$ for $L$ and
$\sim$ by

$x\simeq_{u}y\text{ iff }ux\sim uy\text{ and }\forall z\in\Sigma^{*}:\,uxz\sim
u\Rightarrow(u(xz)^{\omega}\in L\Leftrightarrow u(yz)^{\omega}\in L).$

The _syntactic FORC_ of $L$ [22] is the canonical FORC for $L$ and $\sim_{L}$.
As a running example, consider the language $L$ from Example 3.2. Then
$\sim_{L}$ has only one class, and the PRC for this class is shown in Figure
2. The transition structure of the Mealy machine in Figure 1 is obtained by
merging some of the classes in the PRC.

$\varepsilon$$\scriptstyle{\simeq_{\varepsilon}}$$a$$b$$abba$$ab$$abb$$ba$$bab$$babb$$bb$$bba$$bbab$$aba$$a$$b$$a$$b$$a$$b$$a$$b$$a$$b$$b$$a$$a$$b$$a$$b$$a$$b$$a$$b$$a$$b$$a$$b$$a,b$
Figure 2: The PRC $\simeq_{\varepsilon}$ of the syntactic FORC for the
language from Example 3.2. The colors code the idempotent classes that are
positive ($aba$ and $a$) and negative.

The syntactic FORC is a canonical object for representing regular
$\omega$-languages: In [22] it is shown that $L\subseteq\Sigma^{\omega}$ is
regular if and only if its syntactic FORC is finite, and the syntactic FORC is
the coarsest FORC with $\sim_{L}$ as leading right congruence that recognizes
$L$.

We define the size of a FORC as the sum of the sizes of the LRC and the PRC.
Note that if the syntactic FORC of $L$ is finite, then also the canonical PRCs
for each $\sim$ that refines $L$ are finite, as a direct consequence of the
definition of the canonical FORC for $\sim$.

We now explain how we can use the PRCs $\simeq_{c}$ of the canonical FORC for
$L$ and $\sim$ in order to obtain a Mealy machine for the priority mappings
$\pi_{c}^{\sim}$. So in the following, let $L\subseteq\Sigma^{\omega}$ be
regular with parity complexity $k$, let $\sim$ be a refinement of $\sim_{L}$,
and let $\simeq_{c}$ be the canonical PRC for each class $c$ of $\sim$. We
call a class $[x]_{\simeq_{c}}$ _positive_ if $x^{\omega}\in L_{c}$, and
_negative_ otherwise (by the definition of $\simeq_{c}$ this is independent of
the chosen word from the class). In the example from Figure 2, the positive
classes are the ones of $a$, $ab$, $ba$, and $aba$.

We define a coloring $\kappa_{c}$ on the classes of $\simeq_{c}$ (so on the
states of the transition system defined by $\simeq_{c}$) such that the Mealy
machine that outputs the color of its target state on each transition defines
$\pi_{c}^{\sim}$ (see Lemma 4.2). For this coloring, idempotent classes of
$\simeq_{c}$ play a central role. We call a word $x\in\Sigma^{+}$ _idempotent_
in $\simeq_{c}$ if $x\in E_{c}$ and $x\simeq_{c}xx$. The following lemma
states two useful properties on idempotent words in $\simeq_{c}$.

######  Lemma 4.1.

If $x\in\Sigma^{+}$ is idempotent in $\simeq_{c}$, then each $y\in\Sigma^{+}$
with $y\simeq_{c}x$ is idempotent in $\simeq_{c}$. Furthermore, for each $x\in
E_{c}$, there is a number $n\geq 1$ such that $x^{n}$ is idempotent in
$\simeq_{c}$.

Accordingly, we call a class of $\simeq_{c}$ idempotent if one (and hence all)
its members are idempotent. In the example PRC in Figure 2, the only non-
idempotent classes are the classes of $b$, $ab$ and $ba$.

The algorithm for computing $\kappa_{c}$ considers positive and negative
idempotent classes (the classification of non-idempotent classes as positive
or negative does not play any role). In the example from Figure 2, the
positive idempotent classes are the ones of $a$ and $aba$. The other two
positive classes $ab$ and $ba$ are not idempotent.

Now let $\kappa_{c}:[\simeq_{c}]\rightarrow\\{0,\ldots,k\\}$ be defined by

  * •

$\kappa_{c}([x]_{\simeq_{c}})=0$ if there is no $z$ such that
$[xz]_{\simeq_{c}}$ is a negative idempotent class. In other words, if no
negative idempotent class is reachable from $x$.

  * •

Let $i\geq 1$ and assume that $\kappa_{c}$ has already been defined for all
values $\\{0,\ldots,i-1\\}$. Then $\kappa_{c}([x]_{\simeq_{c}})=i$ for $i\geq
1$ if each idempotent class of the form $[xz]_{\simeq_{c}}$

    * –

either already has a $\kappa_{c}$ value less than $i$,

    * –

or is positive iff $i$ is even.

In the example from Figure 2, the class of $aba$ is assigned $0$. Then all
remaining classes of words that contain a $b$ are assigned value $1$, and
finally, the class of $a$ is assigned $2$.

The following lemma shows that this indeed gives the desired coloring of
$\Sigma^{+}$. In particular, all classes of $\simeq_{c}$ are assigned a value
by the above procedure.

######  Lemma 4.2.

For all $x\in\Sigma^{+}$: $\kappa_{c}(x)=i$ iff $\pi_{c}^{\sim}(x)=i$.

If there are a negative and a positive idempotent class in the same SCC of a
PRC, then none of them will satisfy the conditions for being assigned value
$i$ by $\kappa_{c}$. This contradicts the fact that every class is assigned a
value as a consequence of Lemma 4.2. We use this structural property of the
PRCs in Section 5, and hence state it as a lemma.

######  Lemma 4.3.

If two idempotent classes in a PRC of a canonical FORC are in the same SCC,
then both are positive or both are negative. Furthermore, two classes in the
same SCC of $\simeq_{c}$ have the same $\kappa_{c}$-value.

As a consequence of Lemma 4.2, we obtain a construction from canonical FORCs
to DPAs that is only exponential in the parity complexity of the language,
improving the upper bound from [2] that is exponential in the size of the FORC
(the statement in [2] is about saturated families of DFAs, which are basically
refinements of canonical FORCs up to some small details).

######  Theorem 4.4.

Let $L$ be a regular $\omega$-language of parity complexity $k$, $\sim$ be a
right congruence that refines $\sim_{L}$, and
$(\sim,(\approx_{c})_{c\in[\sim]})$ be the canonical FORC for $L$ and $\sim$.
Then the precise DPA $\mathcal{A}_{L}^{\sim}$ for $L$ and $\sim$ has at most
$n^{k}$ states, where $n$ is the size of the FORC.

Our completeness result for the learning algorithm uses the fact that we can
infer the syntactic FORC of a language if the sample contains enough
information. For bounding the number of required examples, we give an upper
bound on the size of the syntactic FORC for $L$ in the size of a DPA for $L$.

######  Proposition 4.5.

Let $\mathcal{A}$ be a DPA for $L$ with $n$ states, priorities in
$\\{0,\ldots,k-1\\}$, and at most $d$ many $c$-states for class $c$ of
$\sim_{L}$. Then for the syntactic FORC of $L$, the size of the LRC $\sim_{L}$
is at most $n$, and the size of each PRC is at most $(nk)^{d}$.

##  5 DPA learner

In this section, we introduce the passive learner
$\operatorname{\mathsf{DPAInf}}$ (for “DPA inference”), which constructs in
polynomial time a DPA that is consistent with a given input sample.
Throughout, we assume $S=(S_{+},S_{-})$ is a finite $\omega$-sample of
ultimately periodic words. The overall idea is to infer a FORC from $S$ and
color it according to the procedure outlined in Section 4. We later show that
if $S$ contains enough information from $L$, then the syntactic FORC and the
precise coloring will be inferred.

Input: A function $\operatorname{\mathsf{cons}}$ taking a partial TS as input
and returning a boolean.

A complete TS $\mathcal{T}_{0}$ with
$\operatorname{\mathsf{cons}}(\mathcal{T}_{0})=\operatorname{\mathsf{true}}$,
serving as default.

Output: A complete TS $\mathcal{T}$ such that
$\operatorname{\mathsf{cons}}(\mathcal{T})=\operatorname{\mathsf{true}}$ and
$|\mathcal{T}|\leq|\mathcal{T}_{0}|$.

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

while  _$\mathcal{T}$ is not complete_ do

if  _$|\mathcal{T}| >|\mathcal{T}_{0}|$_ then return _$T_{0}$_

$pa\leftarrow$ llex. minimal word with $p\in Q,a\in\Sigma$ such that
$\delta(p,a)$ is undefined

foreach  _$q\in Q$ in length-lexicographic order_ do

$\delta^{\prime}\leftarrow\delta\cup\\{p\xrightarrow{a}q\\}$

if  _$\operatorname{\mathsf{cons}}((Q,\Sigma,\varepsilon,\delta^{\prime}))$
returns $\operatorname{\mathsf{true}}$_ then

$\delta\leftarrow\delta^{\prime}$ and continue with next iteration of while
loop

$Q\leftarrow Q\cup\\{pa\\},\delta\leftarrow\delta\cup\\{p\xrightarrow{a}pa\\}$

return _$\mathcal{T}$_

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

For learning the FORC, we use the procedure _G_ reedily _Le_ arn _R_ ight _C_
ongruence ($\operatorname{\mathsf{GLeRC}}$), which can be seen in Algorithm 1.
It receives as input a consistency function $\operatorname{\mathsf{cons}}$ and
incrementally constructs a TS $\mathcal{T}$ by adding missing transitions,
first trying existing states as targets in canonical order. After inserting a
transition to a potential target, $\operatorname{\mathsf{GLeRC}}$ verifies
whether $\operatorname{\mathsf{cons}}$ is satisfied. If yes,
$\operatorname{\mathsf{GLeRC}}$ keeps the transition and proceeds to the next
iteration. Otherwise, if no existing state works,
$\operatorname{\mathsf{GLeRC}}$ adds a new state as target for the transition.
To ensure termination, $\operatorname{\mathsf{GLeRC}}$ has a second input,
which is a fallback transition system $\mathcal{T}_{0}$. If the constructed TS
$\mathcal{T}$ exceeds $\mathcal{T}_{0}$ in size at any point, the algorithm
terminates and returns $\mathcal{T}_{0}$. This guarantees runtime that is
polynomial in the execution time of $\operatorname{\mathsf{cons}}$ and in the
size of $\mathcal{T}_{0}$, since $\operatorname{\mathsf{GLeRC}}$ attempts to
insert at most polynomially many transitions.

######  Proposition 5.1.

For a consistency function $\operatorname{\mathsf{cons}}$ and a complete
transition system $\mathcal{T}_{0}$ with
$\operatorname{\mathsf{cons}}(\mathcal{T}_{0})=\operatorname{\mathsf{true}}$,
the algorithm $\operatorname{\mathsf{GLeRC}}$ computes a complete TS
$\mathcal{T}$ such that
$\operatorname{\mathsf{cons}}(\mathcal{T})=\operatorname{\mathsf{true}}$ in
time polynomial in the runtime of $\operatorname{\mathsf{cons}}$ and the size
of $\mathcal{T}_{0}$.

The $\operatorname{\mathsf{cons}}$ functions that we pass to
$\operatorname{\mathsf{GLeRC}}$, verify that the constructed TS satisfies
certain notions of consistency with the sample, which we outline below. We use
this specific algorithm, since it can be ensured that
$\operatorname{\mathsf{GLeRC}}$ infers the appropriate transition system in
the limit. In the following, we introduce the different notions of
consistency, which relativize the definitions of the canonical FORC and its
coloring from Section 4 to a sample $S$.

Given a partial TS $\mathcal{T}$, we say that $x,y\in\Sigma^{*}$ _do not lead
to the same state in $\mathcal{T}$_ if $\mathcal{T}(x)$ or $\mathcal{T}(y)$ is
undefined, or if $\mathcal{T}(x)\neq\mathcal{T}(y)$. We call $\mathcal{T}$
_MN-consistent with $S$_ (MN for “Myhill/Nerode”) if for all $xuv^{\omega}\in
S_{+}$ and $yuv^{\omega}\in S_{-}$, $x$ and $y$ do not lead to the same state
in $\mathcal{T}$.

######  Lemma 5.2.

It can be verified in polynomial time whether a (partial) transition system
$\mathcal{T}$ is MN-consistent with an $\omega$-sample $S$.

Now, let $\sim$ represent a complete TS that is MN-consistent with $S$, and
let $c\in[\sim]$. A partial transition system $\mathcal{T}$ is called
_iteration consistent with $(S,\sim,c)$_, if for all $xz,yz\in E^{\sim}_{c}$
with $(xz)^{\omega}\in S_{+}$ and $(yz)^{\omega}\in S_{-}$, $x$ and $y$ do not
lead to the same state in $\mathcal{T}$.

######  Lemma 5.3.

Let $S$ be a finite $\omega$-sample and $\sim$ be a right congruence
representing a complete TS that is MN-consistent with $S$. For each class $c$
of $\sim$, it can be verified in polynomial time whether a given partial TS
$\mathcal{T}$ is iteration consistent with $(S,\sim,c)$.

######  Definition 5.4.

A FORC $(\sim,(\approx_{c})_{c\in[\sim]})$ is _consistent with $S$_ if

  * •

$\sim$ is MN-consistent with $S$ and

  * •

for each $c\in[\sim]$, $\approx_{c}$ is MN-consistent with $S_{c}$ and
iteration consistent with $(S_{c},\sim,c)$, where $S_{c}=(S_{c,+},S_{c,-})$
and $S_{c,\sigma}=\\{uv^{\omega}\mid\exists x\in c$ with $xuv^{\omega}\in
S_{\sigma}\\}$ for $\sigma\in\\{+,-\\}$.

For a given sample $S$, we can construct default structures that are MN- and
iteration consistent as follows, see Appendix C.3 for a small example.
Consider the prefix tree of $S$, to which we add one sink state for words that
are not prefixes of $S$, and loops on the shortest words which are prefix of
exactly one example word. Formally, we define $\sim_{S}$ as $x\sim_{S}y$ if
$x,y\notin\operatorname{\mathsf{Prf}}{(S)}$ or we have $x^{-1}S=y^{-1}S$ and
$|x^{-1}S|=1$. It is not hard to see that the size of $\sim_{S}$ is polynomial
in $|S|$, see for example [10, Appendix B].

In the following, we give a formal description of
$\operatorname{\mathsf{DPAInf}}$. An overview of the algorithm is given in
Figure 3.

input
---
$S=(S_{+},S_{-})$
$\sim$
---
consistent with $S$
FORC $(\sim,(\approx_{c})_{c\in[\sim]})$
---
consistent with $S$
Family of MMs $\overline{\mathcal{M}}$
---
for FWPM that captures
the periodic part of $(S,\sim)$
DPA $\mathcal{B}$ consistent with
---
$S$, which computes ${{\mathcal{A}}}_{\bowtie}(\overline{\mathcal{M}})$
on the prefixes of $S$
Active learner
---
for Mealy Machines
output$\mathcal{H}$$\scriptstyle{\operatorname{\mathsf{equiv}}}$no, c.ex. $u$
if consistent
---
with $S$
$\scriptstyle{\operatorname{\mathsf{output}}}$$u$$\begin{cases}\scriptstyle{\mathcal{B}(u)\text{
if }u\in\operatorname{\mathsf{Prf}}(S)}\\\
\scriptstyle{0\quad\phantom{i}\text{
else}}\end{cases}$1234$\operatorname{\mathsf{GLeRC}}$$\operatorname{\mathsf{GLeRC}}$
coloring
---
Section 4
Lemma 3.15 Figure 3: Schematic view of the $\operatorname{\mathsf{DPAInf}}$
algorithm, details for each step are in the text.

#### Step 1

In the first step, $\operatorname{\mathsf{DPAInf}}$ learns a FORC that is
consistent with the sample $S$. For the LRC, it calls
$\operatorname{\mathsf{GLeRC}}$ with $\sim_{S}$ as default and using
$\operatorname{\mathsf{LRC-cons}}$ as constraint function, where
$\operatorname{\mathsf{LRC-cons}}(T)$ returns $\operatorname{\mathsf{true}}$
iff $T$ is MN-consistent with $S$. We denote the resulting right congruence
with $\sim$. For each $c\in[\sim]$ and $\sigma\in\\{+,-\\}$, the learner now
computes the sets

$\displaystyle S_{c,\sigma}$ $\displaystyle=\\{uv^{\omega}\mid\exists x\in
c\text{ with }xuv^{\omega}\in S_{\sigma}\\}\quad
R_{c,\sigma}=\\{v^{\omega}\mid\exists x\in c\text{ with }xv^{\omega}\in
S_{\sigma}\text{ and }xv\sim x\\}.$

It then executes $\operatorname{\mathsf{GLeRC}}$ with the product
$(\sim_{S_{c}}\times\sim)$ as default and the constraint function
$\operatorname{\mathsf{PRC-cons}}(\mathcal{T})$, which returns
$\operatorname{\mathsf{true}}$ if

  * •

$\mathcal{T}$ is MN-consistent and iteration consistent with $S_{c}$

  * •

$\operatorname{\mathsf{SCC}}_{\mathcal{T}}(q)\cap\operatorname{\mathsf{SCC}}_{\mathcal{T}}(q^{\prime})=\emptyset$
for all
$q\in\operatorname{\mathrm{Inf}}_{\mathcal{T}}(R_{c,+}),q^{\prime}\in\operatorname{\mathrm{Inf}}_{\mathcal{T}}(R_{c,-})$.

Thereby, a FORC $\mathcal{F}=(\sim,(\approx_{c})_{c\in[\sim]})$ that is
consistent with $S$ is obtained. The second condition ensures that
$\mathcal{F}$ meets the properties of Lemma 4.3. This makes it possible to
compute a coloring analogous to $\kappa_{c}$, in the next step.

#### Step 2

In the following, we use $\mathcal{F}=(\sim,(\approx_{c})_{c\in[\sim]})$ to
refer to the FORC that is constructed in step 1. The algorithm now builds a
family of Mealy machines
$\overline{\mathcal{M}}=({\mathcal{M}}_{c})_{c\in[\sim]}$ computing a weak
priority mapping $\overline{\gamma}=(\gamma_{c})_{c\in[\sim]}$. This is done
in a way which mimics the definition of the coloring $\kappa_{c}$ in Section 4
and ensures that $\overline{\gamma}$ is the precise coloring of $L$, provided
the syntactic FORC was learned in step 1 and the sample contains enough
information. For a class $c\in[\sim]$, we proceed as follows:

  * •

Label all states with $\sigma$ in $\mathcal{T}_{\approx_{c}}$, the TS that
represents $\approx_{c}$, that appear in
$\operatorname{\mathrm{Inf}}_{\mathcal{T}}(R_{c,\sigma})$ with
$\sigma\in\\{+,-\\}$.

  * •

For each state $q$, compute the set $P_{q}$ containing all states that are
reachable from $q$ and have a classification.

  * •

Starting with $i=0$ and increasing $i$ after every iteration, assign $i$ to
those states $q$ such that each $p\in P_{q}$ either already has a priority, or
($p$ has classification $+$ iff $i$ is even).

As the construction of $\mathcal{F}$ in step 1 ensures that no SCCs with
positive and negative looping sample words exist, each class of a PRC
$\approx_{c}$ is assigned a priority. For each class $c$ of $\sim$, we obtain
a Mealy machine ${\mathcal{M}}_{c}$ on the transition system of $\approx_{c}$,
which uses the priority (wrt. the computed coloring) of the target state for
each transition. Overall, this procedure returns in polynomial time a family
of Mealy machines $\overline{\mathcal{M}}=({\mathcal{M}}_{c})_{c\in[\sim]}$
whose size is polynomial in $\mathcal{F}$.

#### Step 3

In the following, we use ${{\mathcal{A}}}_{\bowtie}$ to refer the DPA
${{\mathcal{A}}}_{\bowtie}(\overline{\mathcal{M}})$ from Section 3.
$\operatorname{\mathsf{DPAInf}}$ builds a DPA $\mathcal{B}$ which computes the
priority mapping

$\mathcal{B}:u\mapsto{{\mathcal{A}}}_{\bowtie}(u)\text{ if
$u\in\operatorname{\mathsf{Prf}}(S)$ and }u\mapsto 0\text{ otherwise}.$

It can be shown by using Lemma 3.15, that constructing $\mathcal{B}$ is
possible in polynomial time. Then, it is verified that $\mathcal{B}$ is
consistent with $S$, i.e. that $S_{+}\subseteq L(\mathcal{B})$ and $S_{-}\cap
L(\mathcal{B})=\emptyset$. If yes, the algorithm proceeds to step 4.
Otherwise, we redefine $\mathcal{B}$ as a fallback DPA that outputs $1$ on
infixes of negative loops and $0$ otherwise. Formally, the fallback DPA
computes the priority mapping $\mathcal{B}:\Sigma^{+}\to\\{0,1\\}$ with
$\mathcal{B}(u)\mapsto 1$ iff
$u\in\operatorname{\mathsf{Prf}}\big{(}\bigcup_{c\in[\sim]}R_{c,-}\big{)}$.

#### Step 4

$\operatorname{\mathsf{DPAInf}}$ now runs an active learner
$\operatorname{\mathsf{MMAL}}$ for Mealy machines as black box. The oracle
provided to $\operatorname{\mathsf{MMAL}}$ uses the DPA $\mathcal{B}$ from
step 3 and reacts to queries as follows:

$\displaystyle\operatorname{\mathsf{output}}(u)$
$\displaystyle\rightsquigarrow\text{ answer }\mathcal{B}(u)$
$\displaystyle\operatorname{\mathsf{equiv}}(\mathcal{H})$
$\displaystyle\rightsquigarrow\begin{cases}\text{terminate and return
$\mathcal{H}$}&\text{if $\mathcal{H}$ is consistent with $S$}\\\ \text{answer
}\operatorname{\mathrm{min}}_{\text{llex}}\\{x\in\operatorname{\mathsf{Prf}}(S)\mid\mathcal{B}(x)\neq\mathcal{H}(x)\\}&\text{otherwise.}\end{cases}$

This ends the description of the algorithm, and we now state the main results
of this section.

######  Theorem 5.5.

$\operatorname{\mathsf{DPAInf}}$ computes in polynomial time a DPA that is
consistent with the $\omega$-sample $S$ it receives as input.

The core idea for constructing a characteristic sample is to simulate a run
$\operatorname{\mathsf{DPAInf}}$ and whenever the algorithm would make a
mistake in producing the canonical object we are interested in, we add words
preventing it, which leads to the following theorem.

######  Theorem 5.6.

$\operatorname{\mathsf{DPAInf}}$ can learn a DPA ${\mathcal{A}}$ for every
$\omega$-regular language $L$ in the limit. Moreover, the size of
${\mathcal{A}}$ is bounded by the size of the precise DPA ${\mathcal{A}}_{L}$
for $L$, and there exists a characteristic sample $S^{L}$ for $L$ that is
polynomial in the maximum of the size of ${\mathcal{A}}_{L}$ and the size of
the syntactic FORC for $L$.

Consider the subclass of the $\omega$-regular languages
$d\text{-}\mathbb{IRC}(k\text{-}\mathbb{DPA})$, containing all languages $L$
that can be recognized by a DPA with up to $k$ priorities and at most $d$ many
$c$-states for each $\sim_{L}$ class $c$. We obtain the following corollary
from Theorem 5.6 in combination with Proposition 4.5 and Theorem 3.14.

######  Corollary 5.7.

For every fixed $k$ and $d$, $\operatorname{\mathsf{DPAInf}}$ can learn a DPA
for every language in $d\text{-}\mathbb{IRC}(k\text{-}\mathbb{DPA})$ in the
limit from polynomial data.

##  6 Conclusion

We have presented a passive learner for deterministic parity automata that
runs in polynomial time and can learn a DPA for every regular
$\omega$-language in the limit. Our upper bound for the size of complete
samples is, in general, exponential in the size of a minimal DPA for the
language. However, for fixed number of priorities and fixed maximal number of
pairwise language equivalent states, this bound becomes polynomial. The
learning algorithm is based on the canonical DPA for a language that we
introduced as the precise DPA, and that can be constructed from the syntactic
FORC of the language.

We see two natural main directions of future research based on the results
presented here. First of all, we proposed a basic version of the algorithm
that is complete for the class of regular $\omega$-languages and runs in
polynomial time. But there are many parts of the algorithm that allow for
optimizations and variations without losing these properties. These variations
should then be implemented and compared in an empirical study. For example,
all the progress congruences of the FORC are learned independently, while
there are strong dependencies between the progress congruences of the
syntactic FORC. One can explore techniques for learning these congruences
while respecting mutual dependencies. And one can also try other types of
passive learning algorithms from finite automata adapted to learning FORCs.
Also, variations of the active learner used in the last step of the algorithm
can have an impact on the running time and the result produced by the overall
procedure.

Second, the precise DPA for a language deserves further study. An
understanding which structural properties of a language can cause the precise
DPA to be much larger than a minimal DPA for the language might give insights
to minimization problems for DPAs. Furthermore, our construction of the
precise DPA from the syntactic FORC has similarities with a construction that
starts from the syntactic semigroup (see [14]). We plan to investigate the
relation between these two constructions in more detail, and also the relation
(if any) to the canonical representation by good-for-games automata from [15].

## 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:10.1016/0890-5401(87)90052-6.
  * [2] Dana Angluin, Udi Boker, and Dana Fisman.  Families of DFAs as acceptors of omega-regular languages.  In 41st International Symposium on Mathematical Foundations of Computer Science, MFCS 2016, volume 58 of LIPIcs, pages 11:1–11:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016.  URL: http://www.dagstuhl.de/dagpub/978-3-95977-016-3.
  * [3] Dana Angluin and Dana Fisman.  Learning regular omega languages.  Theor. Comput. Sci., 650:57–72, 2016.  doi:10.1016/j.tcs.2016.07.031.
  * [4] Dana Angluin and Dana Fisman.  Polynomial time algorithms for inclusion and equivalence of deterministic omega acceptors, 2020.  URL: https://arxiv.org/abs/2002.03191, doi:10.48550/ARXIV.2002.03191.
  * [5] Dana Angluin, Dana Fisman, and Yaara Shoval.  Polynomial identification of ømega-automata.  In Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, volume 12079 of Lecture Notes in Computer Science, pages 325–343. Springer, 2020.  doi:10.1007/978-3-030-45237-7\\_20.
  * [6] Christel Baier and Joost-Pieter Katoen.  Principles of model checking.  MIT Press, 2008.
  * [7] Alan W. Biermann and Jerome A. Feldman.  On the synthesis of finite-state machines from samples of their behavior.  IEEE Trans. Computers, 21(6):592–597, 1972.  doi:10.1109/TC.1972.5009015.
  * [8] León Bohn and Christof Löding.  Constructing deterministic $\omega$-automata from examples by an extension of the RPNI algorithm.  In 46th International Symposium on Mathematical Foundations of Computer Science, MFCS 2021, volume 202 of LIPIcs, pages 20:1–20:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021.  doi:10.4230/LIPIcs.MFCS.2021.20.
  * [9] León Bohn and Christof Löding.  Passive learning of deterministic büchi automata by combinations of DFAs.  In 49th International Colloquium on Automata, Languages, and Programming, ICALP 2022, July 4-8, 2022, Paris, France, volume 229 of LIPIcs, pages 114:1–114:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.  doi:10.4230/LIPIcs.ICALP.2022.114.
  * [10] León Bohn and Christof Löding.  Constructing deterministic $\omega$-automata from examples by an extension of the rpni algorithm, 2021.  URL: https://arxiv.org/abs/2108.03735, doi:10.48550/ARXIV.2108.03735.
  * [11] J Richard Büchi.  On a decision method in restricted second order arithmetic, logic, methodology and philosophy of science (proc. 1960 internat. congr.), 1962.
  * [12] Hugues Calbrix, Maurice Nivat, and Andreas Podelski.  Ultimately periodic words of rational $\omega$-languages.  In Stephen Brookes, Michael Main, Austin Melton, Michael Mislove, and David Schmidt, editors, Mathematical Foundations of Programming Semantics, pages 554–566, Berlin, Heidelberg, 1994. Springer Berlin Heidelberg.
  * [13] 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/.
  * [14] Thomas Colcombet.  Green’s relations and their use in automata theory.  In Language and Automata Theory and Applications - 5th International Conference, LATA 2011, volume 6638 of Lecture Notes in Computer Science, pages 1–21. Springer, 2011.  doi:10.1007/978-3-642-21254-3\\_1.
  * [15] Rüdiger Ehlers and Sven Schewe.  Natural colors of infinite words.  In Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2022, volume 250 of LIPIcs, pages 36:1–36:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.  doi:10.4230/LIPIcs.FSTTCS.2022.36.
  * [16] E Mark Gold.  Language identification in the limit.  Information and Control, 10(5):447–474, 1967.  URL: https://www.sciencedirect.com/science/article/pii/S0019995867911655, doi:10.1016/S0019-9958(67)91165-5.
  * [17] 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.
  * [18] John E. Hopcroft and Jeffrey D. Ullman.  Formal Languages and their Relation to Automata.  Addison-Wesley, 1969.
  * [19] Malte Isberner, Falk Howar, and Bernhard Steffen.  The open-source learnlib - A framework for active automata learning.  In Computer Aided Verification - 27th International Conference, CAV 2015, volume 9206 of Lecture Notes in Computer Science, pages 487–495. Springer, 2015.  doi:10.1007/978-3-319-21690-4\\_32.
  * [20] Damian López and Pedro Garcíía.  On the inference of finite state automata from positive and negative data.  In Sempere J. In: Heinz J., editor, Topics in Grammatical Inference. Springer, 2016.  doi:10.1007/978-3-662-48395-4_4.
  * [21] 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.
  * [22] Oded Maler and Ludwig Staiger.  On syntactic congruences for $\omega$-languages.  Theoretical Computer Science, 183(1):93–112, 1997.
  * [23] 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.
  * [24] 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.
  * [25] Bernhard Steffen, Falk Howar, and Maik Merten.  Introduction to active automata learning from a practical perspective.  In Formal Methods for Eternal Networked Software Systems - 11th International School on Formal Methods for the Design of Computer, Communication and Software Systems, SFM 2011, Bertinoro, Italy, June 13-18, 2011\. Advanced Lectures, volume 6659 of Lecture Notes in Computer Science, pages 256–296. Springer, 2011.  doi:10.1007/978-3-642-21455-4\\_8.
  * [26] Wolfgang Thomas.  Automata on Infinite Objects, page 133–191.  MIT Press, Cambridge, MA, USA, 1991.
  * [27] Wolfgang Thomas.  Languages, automata, and logic.  In Grzegorz Rozenberg and Arto Salomaa, editors, Handbook of Formal Languages, Volume 3: Beyond Words, pages 389–455. Springer, 1997.  doi:10.1007/978-3-642-59126-6\\_7.
  * [28] 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.
  * [29] Boris A. Trakhtenbrot and Y.M. Barzdin.  Finite Automata: Behavior and Synthesis.  North-Holland Publishing Company, Amsterdam, 1973.
  * [30] Moshe Y. Vardi and Thomas Wilke.  Automata: from logics to algorithms.  In Jörg Flum, Erich Grädel, and Thomas Wilke, editors, Logic and Automata: History and Perspectives [in Honor of Wolfgang Thomas], volume 2 of Texts in Logic and Games, pages 629–736. Amsterdam University Press, 2008.
  * [31] Sicco Verwer and Christian A. Hammerschmidt.  flexfringe: A passive automaton learning package.  In 2017 IEEE International Conference on Software Maintenance and Evolution, ICSME 2017, pages 638–642. IEEE Computer Society, 2017.  URL: http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=8090480.
  * [32] Thomas Wilke.  $\omega$-automata.  CoRR, abs/1609.03062, 2016.  URL: http://arxiv.org/abs/1609.03062, arXiv:1609.03062.

##  Appendix A Proofs for Section 3

###  A.1 Proof of Lemma 3.3

For the proof of Lemma 3.3 we need some basic facts about normalized DPAs that
are somehow known but we cannot give a concrete reference. Hence, we first
prove an auxiliary lemma. The intuition behind the lemma is the following: If
a normalized DPA reads a word $u$ from some state $q$ and visits minimal
priority $i$ on the way, then it is possible to complete a loop on $q$ that
starts with $u$ and has $i$ as minimal priority (or the run changed the SCC
and then $i=0$). Furthermore, if it is possible to have a loop with priority
$i$ on $q$, then also with priority $i-1$ (for $i\geq 2$).

######  Lemma A1.

Let ${\mathcal{A}}=(Q,\Sigma,\iota,\delta,\kappa)$ be a normalized DPA, $q\in
Q$ and $u\in\Sigma^{+}$ with
$\mathcal{A}_{\operatorname{\mathrm{min}}}(q,u)=i$.

  1. (a)

Either there exists $v\in\Sigma^{*}$ with $\delta^{*}(q,uv)=q$ and
$\mathcal{A}_{\operatorname{\mathrm{min}}}(q,uv)=i$, or $i=0$ and
$\delta^{*}(q,uv)\not=q$ for all $v\in\Sigma^{*}$.

  2. (b)

If $i\geq 2$, then there is $y\in\Sigma^{+}$ with $\delta^{*}(q,y)=q$ and
$\mathcal{A}_{\operatorname{\mathrm{min}}}(q,y)=i-1$.

######  Proof A2.

For (a), remove from ${\mathcal{A}}$ all transitions with priority $<i$ and
call the resulting partial DPA ${\mathcal{A}}^{\prime}$. Let
$q^{\prime}:=\delta^{*}(q,u)$. Since
$\mathcal{A}_{\operatorname{\mathrm{min}}}(q,u)=i$, the $u$-path from $q$ to
$q^{\prime}$ still exists in ${\mathcal{A}}^{\prime}$. If there is a path from
$q^{\prime}$ to $q$ in ${\mathcal{A}}^{\prime}$, then let $v$ be a word
labeling such a path. Then $\mathcal{A}_{\operatorname{\mathrm{min}}}(q,uv)=i$
and $\delta^{*}(q,uv)=q$.

If there is no path from $q^{\prime}$ to $q$ in ${\mathcal{A}}^{\prime}$, let
$u=u_{1}au_{2}$ with $u_{1},u_{2}\in\Sigma^{*}$ and $a\in\Sigma$ such that
$q_{1}:=\delta^{*}(q,u_{1})$ is in $\text{SCC}_{{\mathcal{A}}^{\prime}}(q)$
and $\delta(q_{1},a)$ is not in $\text{SCC}_{{\mathcal{A}}^{\prime}}(q)$. Then
every run in ${\mathcal{A}}$ that takes the $a$-transition from $q_{1}$
infinitely often, contains a transition of priority $<i$ infinitely often. So,
if $i>0$, we can change the priority of the $a$-transition from $q_{1}$ to
$i-1$ without changing the language of ${\mathcal{A}}$, contradicting the fact
that ${\mathcal{A}}$ is normalized. Thus, $i=0$ and
${\mathcal{A}}^{\prime}={\mathcal{A}}$. This means that $q$ and $q^{\prime}$
are in different SCCs and thus there is no path back from $q^{\prime}$ to $q$.

For (b), remove all transitions of priority $<i-1$ from ${\mathcal{A}}$,
obtaining ${\mathcal{A}}^{\prime\prime}$. By (a),
$\text{SCC}_{{\mathcal{A}}^{\prime\prime}}(q)$ contains a loop and thus at
least one transition. If $\text{SCC}_{{\mathcal{A}}^{\prime\prime}}(q)$
contains a transition with priority $i-1$, we are done (take as $y$ the label
of a path that starts in $q$, takes this ($i-1$)-transition, and goes back to
$q$).

Otherwise, we show that ${\mathcal{A}}$ cannot be normalized: Lower in
${\mathcal{A}}$ the priority of all transitions that are in
$\text{SCC}_{{\mathcal{A}}^{\prime\prime}}(q)$ by $2$. Since $i\geq 2$ and no
transition in $\text{SCC}_{{\mathcal{A}}^{\prime\prime}}(q)$ has priority
$i-1$, this is possible. Call the resulting DPA $\mathcal{B}$. Consider the
infinity set $X$ of transitions of a run (since ${\mathcal{A}}$ and
$\mathcal{B}$ have the same transition structure, it is the same infinity set
in both). If $X\cap\text{SCC}_{{\mathcal{A}}^{\prime\prime}}(q)=\emptyset$,
the smallest priority in $X$ is the same in ${\mathcal{A}}$ and $\mathcal{B}$.
If $X\subseteq\text{SCC}_{{\mathcal{A}}^{\prime\prime}}(q)$, then the minimal
priority in $X$ differs by exactly $2$ in ${\mathcal{A}}$ and $\mathcal{B}$.
Otherwise, $X$ contains a transition that exits
$\text{SCC}_{{\mathcal{A}}^{\prime\prime}}(q)$, and hence has priority $\leq
i-2$. Since all transitions inside
$\text{SCC}_{{\mathcal{A}}^{\prime\prime}}(q)$ have priority $\geq i-2$ in
${\mathcal{A}}$ and $\mathcal{B}$, the minimal priority in $X$ is the same in
${\mathcal{A}}$ and $\mathcal{B}$. So in all cases, $X$ is accepting in
${\mathcal{A}}$ iff it is in $\mathcal{B}$, contradicting the fact that
${\mathcal{A}}$ is normalized.

See 3.3

######  Proof A3.

For every class $c$ of $\sim$ we show
$P^{\sim}_{c,i}(L)=P^{\sim}_{c,i}({\mathcal{A}})$ by induction on $i$. Note
that by setting $P_{c,-1}^{\sim}(L)=\emptyset$, we obtain a uniform definition
of all $P_{c,i}^{\sim}(L)$ for $i\geq 0$. We can start the induction at $-1$.
Since ${\mathcal{A}}$ only uses priorities $\geq 0$, we obtain
$P^{\sim}_{c,-1}({\mathcal{A}})=\emptyset$. So let $i\geq 0$ and assume by
induction that $P_{c,i-1}^{\sim}(L)=P_{c,i-1}^{\sim}({\mathcal{A}})$.

We first show that $P_{c,i}^{\sim}(L)\subseteq P_{c,i}^{\sim}({\mathcal{A}})$.
Let $u\in P_{c,i}^{\sim}(L)\setminus P_{c,i-1}^{\sim}(L)$ and show that $u\in
P_{c,i}^{\sim}({\mathcal{A}})$. Let $q$ be a $c$-state, and let
$i^{\prime}:=\mathcal{A}_{\operatorname{\mathrm{min}}}(q,u)$. We have to show
that $i^{\prime}\leq i$. Assume for contradiction that $i^{\prime}>i$. Let $x$
be such that ${\mathcal{A}}:q\xrightarrow{ux}q$ with minimal priority
$i^{\prime}$ on this loop (according to Lemma A1). Then no prefix of
$(ux)^{\omega}$ is in $P_{c,i}^{\sim}({\mathcal{A}})$ because the minimal
priority seen from $q$ on any prefix of $(ux)^{\omega}$ is a least
$i^{\prime}>i$. Since $P_{c,i}^{\sim}({\mathcal{A}})\supseteq
P_{c,i-1}^{\sim}({\mathcal{A}})$, also no prefix of $(ux)^{\omega}$ is in
$P_{c,i-1}^{\sim}({\mathcal{A}})$. By induction, no prefix of $(ux)^{\omega}$
is in $P_{c,i-1}^{\sim}(L)$, and thus $(ux)^{\omega}\in L_{c}$ iff $i$ is
even. Since $(ux)^{\omega}$ is accepted from the $c$-state $q$ iff
$i^{\prime}$ is even, we obtain that $i$ is even iff $i^{\prime}$ is even, and
hence $i^{\prime}-1>i$ because $i^{\prime}>i$.

Let $y\in\Sigma^{*}$ be such that ${\mathcal{A}}:q\xrightarrow{y}q$ with
minimal priority $i^{\prime}-1$ (according to Lemma A1). Then $(uxy)^{\omega}$
is accepted from $q$ iff $i^{\prime}-1$ is even iff $i$ is odd. Since $u$ is
in $P_{c,i}^{\sim}(L)$, we obtain that $(uxy)^{\omega}$ has a prefix in
$P_{c,i-1}^{\sim}(L)$. This implies by induction that $(uxy)^{\omega}$ has a
prefix in $P_{c,i-1}^{\sim}({\mathcal{A}})$, contradicting the fact that the
minimal priority that is seen from $q$ on $(uxy)^{\omega}$ is
$i^{\prime}-1>i$.

We now show the other inclusion $P_{c,i}^{\sim}({\mathcal{A}})\subseteq
P_{c,i}^{\sim}(L)$. Let $u\in P_{c,i}^{\sim}({\mathcal{A}})\setminus
P_{c,i-1}^{\sim}({\mathcal{A}})$ and show that $u\in P_{c,i}^{\sim}(L)$. So
let $x\in\Sigma^{*}$ with $ux\in E_{c}$, and let $n>|{\mathcal{A}}|$. Since
$u\in P_{c,i}^{\sim}({\mathcal{A}})$, also $(ux)^{n}\in
P_{c,i}^{\sim}({\mathcal{A}})$.

If $(ux)^{n}\in P_{c,i-1}^{\sim}({\mathcal{A}})$, then by induction
$(ux)^{\omega}$ has a prefix in $P_{c,i-1}^{\sim}(L)$.

If $(ux)^{n}\in P_{c,i}^{\sim}({\mathcal{A}})\setminus
P_{c,i-1}^{\sim}({\mathcal{A}})$, then let $q$ be a $c$-state such that
$\mathcal{A}_{\operatorname{\mathrm{min}}}(q,(ux)^{n})=i$. Since
$n>|{\mathcal{A}}|$ and $ux\in E_{c}$, there is a $c$-state $q^{\prime}$ and
$n_{1},n_{2}$ with $n_{1}+n_{2}\leq n$ such that
${\mathcal{A}}:q\xrightarrow{(ux)^{n_{1}}}q^{\prime}\xrightarrow{(ux)^{n_{2}}}q^{\prime}$.
Since $u\in P_{c,i}^{\sim}({\mathcal{A}})$, the minimal priority on the loop
$q^{\prime}\xrightarrow{(ux)^{n_{2}}}q^{\prime}$ is at most $i$. And by choice
of $q$, the minimal priority on
${\mathcal{A}}:q\xrightarrow{(ux)^{n_{1}}}q^{\prime}\xrightarrow{(ux)^{n_{2}}}q^{\prime}$
is $i$. Hence, the minimal priority on the loop
$q^{\prime}\xrightarrow{(ux)^{n_{2}}}q^{\prime}$ is $i$, and thus
$(ux)^{\omega}\in L_{c}$ iff $i$ is even.

We conclude that $u\in P_{c,i}^{\sim}(L)$.

###  A.2 Proof of Theorem 3.5

See 3.5

######  Proof A4.

According to Lemma 3.3, a Mealy machine only needs to keep track of the
minimal priority that is visited from each $c$-state of ${\mathcal{A}}$ (and
then outputs the maximum of those numbers).

Let ${\mathcal{A}}=(Q,\Sigma,q_{0},\delta,\kappa)$ and let $Q_{c}$ be the set
of $c$ states in ${\mathcal{A}}$. The states of ${\mathcal{M}}_{c}$ are pairs
$(\tau,\mu)$ of functions $\tau:Q_{c}\rightarrow Q$ and
$\mu:Q_{c}\rightarrow\\{0,\ldots,k-1\\}$. There are $(nk)^{d}$ such pairs of
functions (not all of which need to be reachable in ${\mathcal{M}}$).

The initial state is $(\tau_{0},\mu_{0})$ with $\tau_{0}(q)=q$ and
$\mu_{0}(q)=k-1$ for all $q\in Q_{c}$. For $(\tau,\mu)$ and an input
$a\in\Sigma$, let the $a$-successor of $(\tau,\mu)$ be
$(\tau^{\prime},\mu^{\prime})$ with $\tau^{\prime}(q)=\delta(\tau(q),a)$ and
$\mu^{\prime}(q)=\operatorname{\mathrm{min}}(\mu(q),\kappa(\tau(q),a))$. The
output of ${\mathcal{M}}_{c}$ on this transition is $\max_{q\in
Q_{c}}(\mu^{\prime}(q))$.

Then ${\mathcal{M}}$ outputs on $u$ the least $i$ such that $u\in
P_{c,i}({\mathcal{A}})$, which corresponds to $\pi_{c}^{\sim}(u)$ according to
Lemma 3.3 and Definition 3.4.

###  A.3 Proof of Lemma 3.7

See 3.7

######  Proof A5.

We first show that $\overline{\pi^{\sim}}$ captures the periodic part of
$(L,\sim)$.

Let $c$ be a class of $\sim$, $v\in E_{c}$ and set
$i:=\pi_{c}^{\sim}(v^{\omega})$. We show that $i$ is even if and only if
$v^{\omega}\in L_{c}$, where $L_{c}=r^{-1}L$ for an arbitrary $r\in c$.
Pick an $n$ such that $\pi_{c}^{\sim}(v^{n}x)=i$ for all $x\sqsubseteq
v^{\omega}$. This is possible since $\pi_{c}^{\sim}$ is weak. By definition,
$\pi_{c}^{\sim}(v^{n})=i$ implies that either $(v^{n})^{\omega}$ has a prefix
in $P_{c,i-1}^{\sim}(L)$ or ($(v^{n})^{\omega}\in L_{c}$ iff $i$ is even). In
the former case, there would exist some $x\sqsubseteq v^{\omega}$ with
$\pi_{c}^{\sim}(v^{n}x)<i$, contradicting our choice of $n$. Hence the second
case must be true, which is what we set out to show.

We now show that $\overline{\pi^{\sim}}$ is the least such FWPM. The proof
makes use of Lemma A6 stated below, whose proof uses the fact that
$\overline{\pi^{\sim}}$ captures the periodic part of $(L,\sim)$, which we
have already shown.

Let $\overline{\gamma}$ be an FWPM which captures the periodic part of
$(L,\sim)$. We show $\overline{\pi}\leq\overline{\gamma}$. Let
$v\in\Sigma^{+}$ be an arbitrary word with $\gamma_{c}(v)=i$. We show by
induction on $i$ that $\pi^{\sim}_{c}(v)\leq i$.
For the base, let $i=0$. Then $\gamma_{c}((vx)^{\omega})=0$ for all $x\in
v^{-1}E_{c}$ since $\gamma_{c}$ is weak. This means for all $x\in\Sigma^{*}$,
if $vx\in E_{c}$, then $(vx)^{\omega}\in L_{c}$ since $\overline{\gamma}$
captures the periodic part of $(L,\sim)$. Thus $v\in P_{c,0}^{\sim}$ and
therefore $\pi^{\sim}_{c}(v)=0$.
For an $i>0$, we assume towards a contradiction that $\pi_{c}^{\sim}(v)=j>i$,
implying $j\geq 2$. By Lemma A6, there exists some $x\in\Sigma^{*}$ such that
$vx\in E_{c}$ and $\pi_{c}^{\sim}((vx)^{\omega})=j$. Further, it must be that
$\gamma_{c}((ux)^{\omega})=i$, as otherwise if $\gamma_{c}((ux)^{\omega})<i$,
it would follow by induction that $\pi^{\sim}_{c}((ux)^{\omega})<i$. This
means $j$ is even iff $i$ is even and thus $j-1>i$.
Using Lemma A6 once more, we pick some $y\in\Sigma^{*}$ with $vxy\in E_{c}$
and $\pi_{c}^{\sim}((vxy)^{\omega})=j-1$. Again, by induction
$\gamma_{c}((vxy)^{\omega})=i$ and hence $(vxy)^{\omega}\in L(\gamma_{c})$ iff
$(vxy)^{\omega}\notin L(\pi^{\sim}_{c})$. This contradicts our assumption that
both $\overline{\gamma}$ and $\overline{\pi^{\sim}}$ capture the periodic part
of $(L,\sim)$. Hence $\pi_{c}^{\sim}(v)\leq i$, concluding the proof.

######  Lemma A6.

Let $\overline{\pi^{\sim}}$ be as in Definition 3.4 and $v\in\Sigma^{+}$. If
$\pi_{c}^{\sim}(v)=i$ then there exists an $x\in\Sigma^{*}$ such that $vx\in
E_{c}$ and $\pi_{c}^{\sim}((vx)^{\omega})=i$. Moreover, if $i\geq 2$, then
there exists $y\in\Sigma^{*}$ with $vy\in E_{c}$ and
$\pi_{c}^{\sim}((vy)^{\omega})=i-1$.

######  Proof A7.

We show this claim by induction on $i$. To simplify the argument, we define
$P^{\sim}_{c,-1}(L):=\emptyset$. The base for $i=0$ is trivial since
$\pi_{c}^{\sim}$ is weak and thus $\pi_{c}^{\sim}(vx)=0$ for all
$x\in\Sigma^{*}$, which directly implies the claim.
Let $i>0$. Since $\pi_{c}^{\sim}(v)\notin P^{\sim}_{c,i-1}(L)$, there exists
an $x\in\Sigma^{*}$ such that $vx\in E_{c}$, ($(vx)^{\omega}\in L_{c}$ iff
$i-1$ is odd), and $\operatorname{\mathsf{Prf}}((vx)^{\omega})\cap
P^{\sim}_{c,i-2}(L)=\emptyset$. Further, $(vx)^{\omega}$ also has no prefix in
$P^{\sim}_{c,i-1}(L)$. Otherwise $\pi^{\sim}_{c}((vx)^{\omega})=i-1$,
contradicting the fact that by Lemma 3.7, $\overline{\pi}^{\sim}$ captures the
periodic part of $L$. Thus it must be that $\pi_{c}^{\sim}((vx)^{\omega})=i$.
For the second part, assume towards a contradiction that $i\geq 2$ and
$\pi_{c}^{\sim}((vy)^{\omega})\neq i-1$ for all $y\in\Sigma^{*}$ with $vy\in
E_{c}$. Then for each such $y$, either
$\pi_{c}^{\sim}((vy)^{\omega})\in\\{i,i-2\\}$ or
$\pi_{c}^{\sim}((vy)^{\omega})<i-2$. The former implies $(vy)^{\omega}\in
L_{c}$ iff $i-2$ is even, while the latter means that $(vy)^{\omega}$ has some
prefix in $P^{\sim}_{c,i-3}(L)$. In either case, $v\in P^{\sim}_{c,i-2}(L)$,
contradicting $\pi_{c}^{\sim}(v)=i$.

###  A.4 Proof of Lemma 3.9

See 3.9

######  Proof A8.

Let $u,v\in\Sigma^{*},x\in\Sigma^{+}$, and let $c=[u]_{\sim}$ and
$c^{\prime}=[uv]_{\sim}$. We use Lemma 3.3, so let
${\mathcal{A}}=(Q,\Sigma,q_{0},\delta,\kappa)$ be a normalized DPA for $L$.
Denote by $Q_{c}$ and $Q_{c^{\prime}}$ the sets of $c$-states and
$c^{\prime}$-states in ${\mathcal{A}}$, respectively. By Lemma 3.3,
$\pi_{u}^{\sim}(vx)=\max\\{\mathcal{A}_{\operatorname{\mathrm{min}}}(q,vx)\mid
q\in Q_{c}\\}$. Further, for each $q\in Q_{c}$ we have
$\mathcal{A}_{\operatorname{\mathrm{min}}}(q,vx)\leq\mathcal{A}_{\operatorname{\mathrm{min}}}(\delta^{*}(q,v),x)$
because $\mathcal{A}_{\operatorname{\mathrm{min}}}(\delta^{*}(q,v),x)$ takes
the minimal priority of a run that is the suffix of the run considered in
$\mathcal{A}_{\operatorname{\mathrm{min}}}(q,vx)$. We conclude that

$\begin{array}[]{lcl}\pi_{u}^{\sim}(vx)&=&\max\\{\mathcal{A}_{\operatorname{\mathrm{min}}}(q,vx)\mid
q\in Q_{c}\\}\\\
&\leq&\max\\{\mathcal{A}_{\operatorname{\mathrm{min}}}(\delta^{*}(q,v),x)\mid
q\in Q_{c}\\}\\\
&\leq&\max\\{\mathcal{A}_{\operatorname{\mathrm{min}}}(q^{\prime},x)\mid
q^{\prime}\in Q_{c^{\prime}}\\}\\\ &=&\pi_{uv}^{\sim}(x)\end{array}$

where the second inequality follows from the fact that $\delta^{*}(q,v)$ is a
$c^{\prime}$-state for a $c$-state $q$.

###  A.5 Proof of Lemma 3.11

We first show that ${\gamma}_{\bowtie}$ behaves correctly on ultimately
periodic words in an auxiliary lemma. From this we can easily deduce that
${\gamma}_{\bowtie}$ defines the correct language.

######  Lemma A9.

Let $\overline{\gamma}=(\gamma_{c})_{c\in[\sim]}$ be a monotonic FWPM,
$u\in\Sigma^{*}$ and $v\in\Sigma^{+}$. If $u\sim uv$, then
${\gamma}_{\bowtie}(uv^{\omega})=\gamma_{u}(v^{\omega})$.

######  Proof A10.

First note that if $u^{\prime}$ and $v^{\prime}$ are such that
$u^{\prime}(v^{\prime})^{\omega}=uv^{\omega}$ and $u^{\prime}\sim
u^{\prime}v^{\prime}$, then
$\gamma_{u}(v^{\omega})=\gamma_{u^{\prime}}((v^{\prime})^{\omega})$. This is
implied by monotonicity of $\overline{\gamma}$ (Definition 3.8): Assume
w.l.o.g. that $u$ is a prefix of $u^{\prime}$. Then by monotonicity, we have
$\gamma_{u}(v^{\omega})\leq\gamma_{u^{\prime}}((v^{\prime})^{\omega})$. Now
choose $n$ such that $u^{\prime}$ is a prefix of $uv^{n}$. Then again by
monotonicity, we have
$\gamma_{u^{\prime}}((v^{\prime})^{\omega})\leq\gamma_{uv^{n}}(v^{\omega})=\gamma_{u}(v^{\omega})$.

This means that we can choose any representation of the given ultimately
periodic word for proving the claim.

We now turn to the claim of the lemma. Let
${\gamma}_{\bowtie}(uv^{\omega})=i$, then the least color assigned to
infinitely many prefixes of $uv^{\omega}$ is $i$. Thus we can rewrite
$uv^{\omega}$ such that ${\gamma}_{\bowtie}(u)=i$ and
${\gamma}_{\bowtie}(ux)\geq i$ for all non-empty prefixes $x\sqsubset
v^{\omega}$. Further, we assume that $u$ is picked to be the shortest prefix
with this property.
Consider any non-empty $x\sqsubseteq v^{\omega}$ with
${\gamma}_{\bowtie}(ux)=i$. By definition of ${\gamma}_{\bowtie}$, there is a
suffix $z$ of $ux$ that would not be covered if we had
${\gamma}_{\bowtie}(ux)>i$. Since ${\gamma}_{\bowtie}(u)=i$, we conclude that
$z$ is a suffix of $x$ (otherwise it would be covered by the value of
${\gamma}_{\bowtie}(u)$). Thus we can write $x=yz$ with $\gamma_{uy}(z)=i$.
Since $\overline{\gamma}$ is monotonic, it follows that
$\gamma_{u}(x)=\gamma_{u}(yz)\leq\gamma_{uy}(z)=i$. This inequality cannot be
strict because otherwise the suffix $x$ of $ux$ would not be covered by
${\gamma}_{\bowtie}$ since all ${\gamma}_{\bowtie}$-values after $u$ are $\geq
i$. We conclude that $\gamma_{u}(v^{\omega})=i$ as desired.

See 3.11

######  Proof A11.

If follows from [11] that if $K\cap\mathbb{UP}=L\cap\mathbb{UP}$ for two
regular $\omega$-languages $K$ and $L$, then $K=L$. Thus it suffices to verify
that for all $u\in\Sigma^{*},v\in\Sigma^{+}$ holds $uv^{\omega}\in L$ iff
$uv^{\omega}\in L({\gamma}_{\bowtie})$. Consider the sequence of classes
$[u],[uv],[uvv],\dotsc$. Because $\sim$ has only finitely many classes, there
must exist $i<j\leq|\sim|+1$ such that $[uv^{i}]=[uv^{j}]$. Thus we can pick
$x$ and $y$ such that $uv^{\omega}=xy^{\omega}$ and $xy\sim x$.
By definition, we have $xy^{\omega}\in L$ iff $y^{\omega}\in L_{x}$. Since
$y\in E_{x}$ and $\overline{\gamma}$ captures the periodic part of $L$, it
further holds that $y^{\omega}\in L_{x}$ iff $y^{\omega}\in L(\gamma_{x})$.
Applying Lemma A9 now gives us
${\gamma}_{\bowtie}(xy^{\omega})=\gamma_{x}(y^{\omega})$, from which we
immediately conclude that $xy^{\omega}\in L({\gamma}_{\bowtie})$ iff
$xy^{\omega}\in L$.

The claim $L({\pi}_{\bowtie}^{\sim})=L$ directly follows from Lemma 3.7 and
Lemma 3.9.

###  A.6 Proof of Lemma 3.12

See 3.12

######  Proof A12.

We write ${{\mathcal{A}}}_{\bowtie}$ for
${{\mathcal{A}}}_{\bowtie}(\overline{\mathcal{M}})$. Further, for avoiding
case distinctions, we let
${\gamma}_{\bowtie}(\varepsilon):={{\mathcal{A}}}_{\bowtie}(\varepsilon):=0$.
Note that this has no influence on the claim of the lemma because the claim is
only on non-empty words.

We first prove the following characterization of ${\gamma}_{\bowtie}$, and
then show that this is precisely what
${{\mathcal{A}}}_{\bowtie}(\overline{\mathcal{M}})$ computes:

Claim: For $u\in\Sigma^{+}$, we have that ${\gamma}_{\bowtie}(u)$ is the
minimal $i$ such that there are $x\in\Sigma^{*}$, $y\in\Sigma^{+}$ with $u=xy$
and

  1. (1)

$\gamma_{x}(y)=i$,

  2. (2)

$\forall z\in\Sigma^{+}:z\sqsubsetneq y\Rightarrow{\gamma}_{\bowtie}(xz)>i$,
and

  3. (3)

${\gamma}_{\bowtie}(x)\leq i$.

(Where $z\sqsubsetneq y$ means that $z$ is a prefix of $y$ but not equal to
$y$.)

From the definition of ${\gamma}_{\bowtie}$ it follows that
${\gamma}_{\bowtie}(u)$ is the minimal $i$ for which $u=xy$ with properties
(1) and (2) exist, because these are precisely the suffixes of $u$ that need
to be covered by the value ${\gamma}_{\bowtie}(u)$. So let $i$ be minimal such
that there are $x\in\Sigma^{*}$, $y\in\Sigma^{+}$ with $u=xy$,
$\gamma_{x}(y)=i$, and ${\gamma}_{\bowtie}(xz)>i$ for all strict non-empty
prefixes of $y$. Furthermore, choose $x$ and $y$ such that $y$ has maximal
length with these properties. We now show that (3) is also satisfied, thus
proving the claim.

Assume for contradiction that ${\gamma}_{\bowtie}(x)=j>i$. Then $x$ is non-
empty because we defined ${\gamma}_{\bowtie}(\varepsilon)=0$. Let
$x=x^{\prime}a$ with $a\in\Sigma$. Since $\overline{\gamma}$ is monotonic,
$i^{\prime}:=\gamma_{x^{\prime}}(ay)\leq\gamma_{x}(y)=i$. Now let $z$ be a
nonempty strict prefix of $ay$. If $z=a$, then
${\gamma}_{\bowtie}(x^{\prime}z)={\gamma}_{\bowtie}(x)=j>i$. If
$z=az^{\prime}$ with nonempty $z^{\prime}$, then
${\gamma}_{\bowtie}(x^{\prime}z)={\gamma}_{\bowtie}(xz^{\prime})>i$ because
$x,y$ and $i$ satisfy property (2). Overall, we obtain that $x^{\prime},ay$
and $i^{\prime}$ satisfy properties (1) and (2). If $i^{\prime}<i$, this
contradicts the choice of $i$ as the minimal such value, and if
$i^{\prime}=i$, this contradicts the choice of $y$ as longest suffix of $u$
such that $x,y$ and $i$ have properties (1) and (2).

Now let us show that the priority of ${{\mathcal{A}}}_{\bowtie}$ after reading
$u$ is the one characterized in the claim. We assume inductively that
${{\mathcal{A}}}_{\bowtie}$ has produced the same priorities as
${\gamma}_{\bowtie}$ on all strict non-empty prefixes of $u$. Let
${{\mathcal{A}}}_{\bowtie}(u)=:i$. Then the component for priority $i$ in
${{\mathcal{A}}}_{\bowtie}$ has reached a final state of the respective DFA
that is currently running in that component, and none of the DFAs in the
components of smaller priorities has reached a final state. Let $x$ be the
longest strict prefix of $u$ such that ${{\mathcal{A}}}_{\bowtie}(x)\leq i$
(by our convention ${{\mathcal{A}}}_{\bowtie}(\varepsilon)=0$, such an $x$
always exists), and let $y\in\Sigma^{+}$ be such that $u=xy$.

By definition of ${{\mathcal{A}}}_{\bowtie}$, the component for priority $i$
is reset to the initial state of $\mathcal{D}_{x,i}$ after reading $x$, and
since $x$ is the longest prefix on which priority $\leq i$ is produced, none
of the components for priorities $\leq i$ is reset after $x$. We had seen
above that the component for priority $i$ in ${{\mathcal{A}}}_{\bowtie}$ has
reached a final state, which means that $\gamma_{x}(y)\leq i$ by definition of
$\mathcal{D}_{x,i}$. Since the components for priorities smaller than $i$ have
not reached a final state, we obtain by monotonicity that $\gamma_{x}(y)=i$.
Hence, $x,y$ and $i$ satisfy the properties (1)–(3) of the claim, and thus
${{\mathcal{A}}}_{\bowtie}(u)=i\geq{\gamma}_{\bowtie}(u)$.

Now assume that there is $j<i$ that satisfies (1)–(3) for some appropriate $x$
and $y$. Then, along the same lines as above, the component for priority $j$
is reset after that $x$, and reaches a final state after reading $y$. This
means that ${{\mathcal{A}}}_{\bowtie}$ would output a priority $\leq j$.

###  A.7 The precise DPA can be exponential in the size of a minimal DPA

We present a family of examples showing that the precise DPA can be
exponential in the size of a minimal DPA. This is already witnessed by Büchi
automata, so DPAs with priorities $\\{0,1\\}$. The example is taken from [9,
Proposition 14].

For a number $d\geq 1$, consider the alphabet
$\Sigma_{d}=\\{a_{0},\ldots,a_{d-1}\\}$ and let
$L_{d}\subseteq\Sigma_{d}^{\omega}$ be the language consisting of all
$\omega$-words that contain each symbol from $\Sigma_{d}$ infinitely often.
Then $\sim_{L_{d}}$ has only one class.

In a first approach for constructing a DPA for $L_{d}$, one would maybe build
an automaton that tracks precisely which symbols it has seen. So the states
are subsets of $\Sigma_{d}$, with $\emptyset$ as initial state, and
transitions adding the processed symbol to the current state. Whenever a
transition would result in a state for the full set $\Sigma_{d}$, the DPA
emits priority $0$, and resets the state to $\emptyset$. All other transitions
have priority $1$.

Indeed, this is what the precise DPA does: The precise FWPM for $L_{d}$ and
$\sim_{L_{d}}$ (consisting only of one weak priority mapping since there is
only one class), maps a finite word to priority $0$ if it contains all symbols
from $\Sigma_{d}$, and to $1$ otherwise. The precise DPA resulting from that
precise FWPM then behaves exactly as described above. So it has $2^{d}-1$
states.

However, one can build a DPA with only $d$ states that waits for the next
symbol from $\Sigma_{d}$ for some fixed order on $\Sigma_{d}$, and resets to
the initial state with priority $0$ if it has reached the last symbol in this
order.

For the standard order on $\\{0,\ldots,d-1\\}$ and state set
$\\{q_{0},\ldots,q_{d-1}\\}$, the resulting transition function is
$\delta(q_{h},a_{h})=a_{h+1\mod d}$ with priority $0$ if $h=d-1$ and $1$
otherwise, and $\delta(q_{h},a_{h^{\prime}})=q_{h}$ if $h\not=h^{\prime}$.

This family of examples might also convey some further intuition why we chose
the name “precise DPA”: It emits the accepting priority $0$ precisely when all
symbols have occurred. The small DPA with only $d$ states emits priority $0$
if all symbols have occurred in a specific order, so it would not emit
priority $0$ on the finite word $a_{2}a_{1}a_{0}$ (for $d=3$) but on
$a_{0}a_{1}a_{2}$. It seems hard to define such a behavior just from the
language definition in a canonical way.

The small DPA that we explained is not normalized. Normalization would assign
priority $0$ to all transitions the do not loop on the same state but advance
to the next state in the order. In this case, the DPA would assign priority
$0$ already to the first prefix containing $a_{0}$. Again, it seems hard to
extract such a behavior in a canonical way just from the language definition.

###  A.8 Proof of Theorem 3.14

See 3.14

######  Proof A13.

By Theorem 3.5, the size of the Mealy machines representing the precise FWPM
${\pi}_{\bowtie}^{\sim}$ is bounded by $(nk)^{d}$. Hence, the size of the DFAs
extracted from the Mealy machines in the construction of
${{\mathcal{A}}}_{\bowtie}(\overline{{\mathcal{M}}})$ is also bounded by that
term. The number of states used in the component for a priority $i$ is the sum
of sizes of the $\mathcal{D}_{c,i}$ for all classes $c$ of $\sim_{L}$. The
number of classes is bounded by $n$, and hence the number of states for the
priority $i$ component is bounded by $n(nk)^{d}$. The number of states of
${{\mathcal{A}}}_{\bowtie}(\overline{{\mathcal{M}}})$ is thus bounded by
$n(n(nk)^{d})^{k-1}=n^{k}(nk)^{d(k-1)}\leq(nk)^{k(d+1)}$.

###  A.9 Proof of Lemma 3.15

We first state a simple auxiliary lemma.

######  Lemma A14.

Let $v\in\Sigma^{+}$. A DFA $\mathcal{D}$ with $n$ accepts a prefix
$v^{\omega}$ from a state $q$, if and only if there exists a non-empty
$x\in\operatorname{\mathsf{Prf}}(v^{\omega})\cap L(\mathcal{D})$ with $|x|\leq
n\cdot|v|$.

######  Proof A15.

Consider the run
$q=q_{0}\xrightarrow{v}q_{1}\xrightarrow{v}q_{2}\xrightarrow{v}\cdots$ of
$\mathcal{D}$ on $v^{\omega}$. As $\mathcal{D}$ has $n$ states, there must be
positions $i<j\leq n$ at which a state repeats, i.e. $q_{i}=q_{j}$. Either a
final state is visited before position $j$, or the DFA loops on $v^{\omega}$
without visiting a final state at all.

See 3.15

######  Proof A16.

To simplify notation, we let
${\mathcal{A}}:={{\mathcal{A}}}_{\bowtie}(\overline{\mathcal{M}})$ and use
$\gamma$ to refer to the priority mapping computed by ${\mathcal{A}}$.
Further, we assume that $uv\sim u$. Otherwise we can rewrite the
representation of $uv^{\omega}$ accordingly with only a polynomial blow-up of
the representation.

We decompose $uv^{\omega}$ into a sequence of non-empty finite factors
$x_{0},x_{1}\cdots$ by making the next for each $x_{h}$ is right after the
first time ${\mathcal{A}}$ emits the smallest priority $i_{h}$ it will emit on
the remaining suffix $w_{h}$. Formally, we define the sequence inductively
with $y_{0}:=\varepsilon$, $w_{0}:=uv^{\omega}$, and if $y_{h},w_{h}$ with
$y_{h}w_{h}=uv^{\omega}$ are given, we let $x_{h}$ be the shortest prefix of
$w_{h}$ such that $\gamma(y_{h}x_{h})\leq\gamma(y_{h}x)$ for all non-empty
prefixes $x$ of $w_{h}$. Then let $i_{h}:=\gamma(y_{h}x_{h})$,
$y_{h+1}:=y_{h}x_{h}$ and $w_{h+1}$ such that $w_{h}=x_{h}w_{h+1}$.

We first explain why $i_{h},x_{h}$ can be computed in polynomial time, and why
the length of each $x_{h}$ is polynomial in $|uv|$ and
$|\overline{\mathcal{M}}|$.

By definition, the states of ${\mathcal{A}}$ are tuples of the form
$(p_{0},\dotsc,p_{k-1},c)$, where $c$ is a class of $\sim$ and the $p_{i}$ are
states of DFAs whose size is bounded by the size of the Mealy machines in
$\overline{{\mathcal{M}}}$. We already know that ${\mathcal{A}}$ only emits
priorities $\geq i_{h-1}$ on the remaining suffix $w_{h}$ (letting $i_{-1}=0$
for $h=0$). And after the prefix $y_{h}$, all components for priorities $j\geq
i_{h-1}$ are set to the initial state of the DFAs for the current $\sim$-class
$c_{h}$. To determine $i_{h}$, we can check in increasing order starting from
$j=i_{h-1}$, whether $\mathcal{D}_{c_{h},j}$ accepts a prefix of $w_{h}$. By
Lemma A14 this can be done in polynomial time, and if there is such a prefix,
its length bounded by $|u|+|v||\mathcal{D}_{c_{h},j}|$.

We now explain why we only need to compute a polynomial number of the factors.

Since each $i_{h}$ is the smallest priority that appears on the remaining
suffix, we have $i_{0}\leq i_{1}\leq\cdots$. So for $h\geq k-1$, all $i_{h}$
are the same, say $i$. Since ${\mathcal{A}}$ resets all components for
priorities $\geq i$ after emitting $i$, we get that for all $h,h^{\prime}\geq
k$ with $w_{h}=w_{h^{\prime}}$ that $x_{h}=x_{h^{\prime}}$. Furthermore, the
sequence of priorities emitted on the factors $x_{h}$ and $x_{h^{\prime}}$ is
also the same because it only depends on the states in the components for
priorities $\geq i$, which are reset every time after $i$ is emitted.

Since the $w_{h}$ are suffixes of $uv^{\omega}$, such a repetition of a suffix
happens after at most $|u|+|v|$ steps. But if $w_{h}=w_{h^{\prime}}$ and
$x_{h}=x_{h^{\prime}}$, then also $w_{h+1}=w_{h^{\prime}+1}$ and thus the
sequence of priorities becomes periodic at this point.

Thus, in order to compute an ultimately periodic representation of the
priority sequence of ${\mathcal{A}}$ on $uv^{\omega}$, it suffices to compute
the sequence of the $w_{h},y_{h},x_{h},i_{h}$ up to a point $h_{1}$ such that
there is $h_{0}<h_{1}$ with $w_{h_{1}}=w_{h_{0}}$ and $i_{h_{1}}=i_{h_{0}}$.
The resulting prefix $x_{0}x_{1}\cdots x_{h_{1}-1}$ is of polynomial length in
$|uv|$ and $|\overline{{\mathcal{M}}}|$ according to the above explanations.
Then we let $r$ be the priority sequence of ${\mathcal{A}}$ on $x_{0}\cdots
x_{h_{0}-1}$ and $s$ the priority sequence of ${\mathcal{A}}$ on
$x_{h_{0}}\cdots x_{h_{1}-1}$. These can be computed on the fly without fully
constructing ${\mathcal{A}}$, so their computation is polynomial in $|uv|$ and
$|\overline{{\mathcal{M}}}|$.

###  A.10 Proof of Theorem 3.16

See 3.16

######  Proof A17.

Let ${\mathcal{A}}=(Q,\Sigma,\iota,\delta,\kappa)$. Write $\sim$ for
$\sim_{\mathcal{A}}$, and let $\overline{\pi^{\sim}}$ be the precise FWPM for
$(L,\sim)$.

The classes of $\sim$ correspond to the states of ${\mathcal{A}}$, which means
that for the class $q$, the only $q$-state is $q$ itself. Thus, by Lemma 3.3,
$\pi_{q}^{\sim}(u)=\mathcal{A}_{\operatorname{\mathrm{min}}}(q,u)$. We show
that ${\pi}_{\bowtie}^{\sim}(ua)=\kappa(\delta^{*}(u),a)$ for all
$u\in\Sigma^{*}$ and $a\in\Sigma$, which means that the priority mapping of
${\mathcal{A}}$ is ${\pi}_{\bowtie}^{\sim}$. Since ${\mathcal{A}}$ is, by
assumption, minimal as Mealy machine, we obtain that ${\mathcal{A}}$ is the
precise DPA for $L$ and $\sim$ by definition of precise DPAs.

So let $i:={\pi}_{\bowtie}^{\sim}(ua)$. By definition of the join,
${\pi}_{\bowtie}^{\sim}(ua)$ is the maximal value that ensures that all
suffixes of $ua$ are covered. So there are $x,y\in\Sigma^{*}$ with $u=xy$ such
that the suffix $ya$ of $ua$ needs to be covered with value $i$. That means
with $q:=\delta^{*}(x)$ that $i=\pi_{q}^{\sim}(ya)$, and $i<\pi_{q}^{\sim}(y)$
(the latter because otherwise the value of $\pi_{q}^{\sim}(ya)$ would already
be covered by ${\pi}_{\bowtie}^{\sim}(xy)$). Hence
$\mathcal{A}_{\operatorname{\mathrm{min}}}(q,ya)=\pi_{q}^{\sim}(ya)=i<\pi_{q}^{\sim}(y)=\mathcal{A}_{\operatorname{\mathrm{min}}}(q,y)$,
which means that $i=\kappa(\delta^{*}(q,y),a)=\kappa(\delta^{*}(u),a)$.

##  Appendix B Proofs for Section 4

###  B.1 Proof of Lemma 4.1

See 4.1

######  Proof B1.

We begin with the first claim. Let $u\in c$. First note that $y\in E_{c}$
because $x\in E_{c}$ and $y\simeq_{c}x$ implies $ux\sim uy$. For showing
$y\simeq_{c}yy$, consider $z\in\Sigma^{+}$ with $uyz\sim u$. Then

$\displaystyle u(yz)^{\omega}\in L\quad$ $\displaystyle\Leftrightarrow\quad$
$\displaystyle u(xz)^{\omega}$ $\displaystyle\in L\quad\qquad$ because
$y\simeq_{c}x$ $\displaystyle\Leftrightarrow$ $\displaystyle u(xxz)^{\omega}$
$\displaystyle\in L$ as $x\in E_{c}$ is idempotent
$\displaystyle\Leftrightarrow$ $\displaystyle u(yxz)^{\omega}$
$\displaystyle\in L$ $y\simeq_{c}x$ $\displaystyle\Leftrightarrow$
$\displaystyle uy(xzy)^{\omega}$ $\displaystyle\in L$ $uy\sim u$ and $\sim$
refines $\sim_{L}$ $\displaystyle\Leftrightarrow$ $\displaystyle
uy(yzy)^{\omega}$ $\displaystyle\in L$ $y\simeq_{c}x$
$\displaystyle\Leftrightarrow$ $\displaystyle u(yyz)^{\omega}$
$\displaystyle\in L$ $\displaystyle\text{as $uy\sim u$ and $\sim$ refines
$\sim_{L}$}.$

We now show the second claim. Since $\simeq_{c}$ has finitely many classes,
there are $n_{1},n_{2}\geq 1$ such that $x^{n_{1}}\simeq_{c}x^{n_{1}+n_{2}}$.
Then it is not hard to see that for $n:=n_{1}n_{2}$ we have $x^{n}\simeq
x^{2n}$.

###  B.2 Proof of Lemma 4.2

See 4.2

######  Proof B2.

The proof goes by induction on $i$. For the base case, note that $x\in
P_{c,0}^{\sim}(L)$ iff $(xz)^{\omega}\in L_{c}$ for all $z\in\Sigma^{*}$ with
$xz\in E_{c}$. In particular, this means that all idempotent classes of
$\simeq_{c}$ that are reachable from the class of $x$, and hence contain a
word of the form $xz$, must be positive. So $\kappa_{c}$ assigns $0$ to all
classes $[x]_{\simeq_{c}}$ with $\pi_{c}^{\sim}(x)=0$. Vice versa, if no
negative idempotent classes are reachable from the class of $x$, then
$(xz)^{\omega}\in L_{c}$ for all $z\in\Sigma^{*}$ with $xz\in E_{c}$ (if
$(xz)^{\omega}\not\in L_{c}$, then it has an idempotent $(xz)^{n}$ as prefix
by Lemma 4.1, which would then be negative).

Now let $i\geq 1$ and assume by induction that $\kappa_{c}$ and
$\pi_{c}^{\sim}$ coincide for all values less than $i$. The proof is a simple
reasoning using the definitions of $\kappa_{c}$ and $\pi_{c}^{\sim}$.

Let $x\in\Sigma^{+}$. If $\pi_{c}^{\sim}(x)=i$, then we already know by
induction that $\kappa_{c}(x)\geq i$. We show that $\kappa_{c}(x)=i$. Consider
an idempotent class that is reachable from the class of $x$. This class is of
the form $[xz]_{\simeq_{c}}$ for some $z$ with $xz\in E_{c}$. By definition,
$\pi_{c}^{\sim}(x)=i$ implies that for each $z\in\Sigma^{*}$ with $xz\in
E_{c}$, either $(xz)^{\omega}$ has a prefix in $P_{c,i-1}^{\sim}(L)$, or
($(xz)^{\omega}\in L_{c}$ iff $i$ is even). In the first case, if
$(xz)^{\omega}$ has a prefix in $P_{c,i-1}^{\sim}(L)$, then there is an $n$
such that $\pi_{c}^{\sim}((xz)^{n})\leq i-1$ (because $\pi_{c}^{\sim}$ is
weak). Then by induction also $\kappa_{c}((xz)^{n})\leq i-1$. Since $xz$ is
idempotent, we have $xz\simeq_{c}(xz)^{n}$, and thus also $\kappa_{c}(xz)\leq
i-1$. In the second case, ($(xz)^{\omega}\in L_{c}$ iff $i$ is even), the
class of $xz$ is positive iff $i$ is even. Hence, each class reachable from
$x$ either has a $\kappa_{c}$ value smaller than $i$ or is positive iff $i$ is
even. Hence $\kappa_{c}(x)=i$.

For the other direction, assume that $\kappa_{c}(x)=i$ and show that
$\pi_{c}^{\sim}(x)=i$. By induction, $\pi_{c}^{\sim}(x)\geq i$, which means
that $x\notin P_{c,i-1}^{\sim}$. Let $z\in\Sigma^{*}$ be such that $xz\in
E_{c}$. Let $n$ be such that the class of $(xz)^{n}$ is idempotent (by Lemma
4.1). Since $\kappa_{c}(x)=i$, the class of $(xz)^{n}$ has a
$\kappa_{c}$-value less than $i$, or it is positive iff $i$ is even. In the
first case, we get by induction that $(xz)^{n}\in P_{c,i-1}^{\sim}$. In the
second case, $((xz)^{n})^{\omega}=(xz)^{\omega}\in L_{c}$ iff $i$ is even. So
$x\in P_{c,i}^{\sim}$ and hence $\pi_{c}^{\sim}(x)=i$.

###  B.3 Proof of Theorem 4.4

See 4.4

######  Proof B3.

The Mealy machine obtained from the PRC $\simeq_{c}$ by using the transition
structure of $\simeq_{c}$ and assigning the $\kappa_{c}$-value of the target
state to a transition computes $\pi_{c}^{\sim}$ according to Lemma 4.2. Denote
the resulting family of Mealy machines by $\overline{{\mathcal{M}}}$. Then
${{\mathcal{A}}}_{\bowtie}(\overline{{\mathcal{M}}})$ computes the priority
mapping ${\pi}_{\bowtie}^{\sim}$ and thus accepts $L$ by Lemma 3.11. Since
each $\simeq_{c}$ refines $\sim$ by definition, the component for $\sim$ in
the construction of ${{\mathcal{A}}}_{\bowtie}(\overline{{\mathcal{M}}})$ is
not required (and even if it is used it does not blow up the state space). The
states used for the component of priority $i$ in
${{\mathcal{A}}}_{\bowtie}(\overline{{\mathcal{M}}})$ is the sum of the states
of the $\mathcal{D}_{c,i}$, each of which has size bounded by the size of
$\simeq_{c}$. So the number of states used for the component of priority $i$
is at most $n$.

Hence, the size of ${{\mathcal{A}}}_{\bowtie}(\overline{{\mathcal{M}}})$ is
bounded by $n^{k}$.

###  B.4 Proof of Proposition 4.5

See 4.5

######  Proof B4.

Let $\mathcal{A}=(Q,\Sigma,q_{0},\delta,\kappa)$.

The first claim is obvious because two words that lead to the same state of
$\mathcal{A}$ are clearly $\sim_{L}$ equivalent.

Let $c$ be a class of $\sim_{L}$, and let $\approx_{c}$ be the canonical PRC
for $c$. Let $Q_{c}$ be the set of states from which $L_{c}$ is accepted. Then
by assumption $|Q_{c}|\leq d$. For $x\in\Sigma^{*}$ define the function
$\Delta_{c,x}:Q_{c}\rightarrow Q\times\\{0,\ldots,k-1\\}$ by induction on the
length of $x$ by $\Delta_{c,\varepsilon}(q)=(q,k-1)$ and for $x=x^{\prime}a$
with $\Delta_{c,x^{\prime}}(q)=(q^{\prime},i)$ let
$\Delta_{c,x^{\prime}a}(q)=(\delta(q^{\prime},a),\operatorname{\mathrm{min}}(i,\kappa(q,a)))$.

If two words $x,y\in\Sigma^{+}$ with $ux\sim_{L}uy$ define the same function
$\Delta_{c,x}=\Delta_{c,y}$, then $x\approx_{c}y$. To see this, let $u\in c$,
and $z\in\Sigma^{*}$ such that $uxz\sim_{L}u$. For verifying $ux\sim_{L}uy$,
let $q:=\delta^{*}(q_{0},u)\in Q_{c}$. By assumption
$\Delta_{c,x}(q)=\Delta_{c,y}(q)=:(q^{\prime},i)$. Thus,
$\delta^{*}(q_{0},ux)=\delta^{*}(q_{0},uy)=q^{\prime}$, and hence
$ux\sim_{L}uy$.

For verifying $(u(xz)^{\omega}\in L\Leftrightarrow u(yz)^{\omega}\in L)$,
consider the runs of $\mathcal{A}$ on the two words. On $u$ they are the same.
On $x$ and $y$ they might differ, but they reach the same state and see the
same minimal priority on the way (because $\Delta_{c,x}=\Delta_{c,y}$). On $z$
they agree again, so they are in the same state after $uxz$ and $uyz$. Since
$uxz\sim_{L}u$, this state is in $Q_{c}$. We can now repeat this argument, so
the two runs only differ on the parts resulting from the $x$, respectively
$y$, segments of the word. But on these segments, the same minimal priority is
visited. Hence, the minimal priority that appears infinitely often is the same
in the two runs.

Since there are $(nk)^{d}$ functions from $Q_{c}$ to
$Q\times\\{0,\ldots,k-1\\}$, the number of classes of $\approx_{c}$ on
$\Sigma^{+}$ is bounded by $(nk)^{d}$.

##  Appendix C Full proofs for Section 5

###  C.1 Consistency and Polynomial Runtime: full proof of Lemma 5.2, Lemma
5.3 and Theorem 5.5

The proofs for showing that MN- and iteration consistency can be verified in
polynomial time use the same overall approach. We reduce the problem of
deciding whether a given $\mathcal{T}$ is consistent with the sample (for both
notions of consistency) to a unified setting, which can be solved by
performing a polynomial number of reachability analyses. Specifically, we use
two DFAs ${\mathcal{A}}_{1},{\mathcal{A}}_{2}$ and a conflict relation
$C\subseteq Q_{1}\times Q_{2}$ to encode the pairs of words $x,y$ which are
not allowed to lead to the same state in $\mathcal{T}$. Now we can check for
consistency of $\mathcal{T}$ by verifying for all $x,y\in\Sigma^{*}$, that
$(\delta^{*}_{1}(\iota_{1},x),\delta^{*}_{2}(\iota_{2},y))\in C$ implies that
$x$ and $y$ do not lead to the same state in $\mathcal{T}$. In other words
$\mathcal{T}$ is not consistent iff there is some $q$ in $\mathcal{T}$ such
that $(q,q_{1})$ and $(q,q_{2})$ are reachable in
$\mathcal{T}\times{\mathcal{A}}_{1}$ and $\mathcal{T}\times{\mathcal{A}}_{2}$,
respectively, and $(q_{1},q_{2})\in C$. This can clearly be checked in time
polynomial in the size of $|\mathcal{T}|$, $|{\mathcal{A}}_{1}|$ and
$|{\mathcal{A}}_{2}|$. In the proof of the following two lemmas, we thus only
need to show that suitable DFAs ${\mathcal{A}}_{1},{\mathcal{A}}_{2}$ and a
conflict relation $C$ can be constructed in polynomial time. See 5.2

######  Proof C1.

We compute the DFAs ${\mathcal{A}}_{1},{\mathcal{A}}_{2}$ such that
${\mathcal{A}}_{1}$ and ${\mathcal{A}}_{2}$ accept all prefixes of $S_{+}$ and
$S_{-}$, respectively. Similar to how the default transition systems for
$\operatorname{\mathsf{GLeRC}}$ in Section 5 are built, we start the
construction of the DFAs with a prefix tree for $S$. In both cases, we attach
loops to states that are reached on exactly one sample word and introduce a
rejecting sink state that is reached on all remaining transitions. One easily
verifies that this construction is possible in polynomial time.

A pair $(q_{1},q_{2})$ of states with $q_{i}\in{\mathcal{A}}_{i}$ for
$i\in\\{1,2\\}$ is in the conflict relation $C$, if there exists an infinite
run in the product automaton ${\mathcal{A}}_{1}\times{\mathcal{A}}_{2}$, which
starts in $(q_{1},q_{2})$ and stays in $F_{1}\times F_{2}$. Checking for the
existence of such an infinite run starting in a pair $(q_{1},q_{2})$ can be
done by restricting the product to $F_{1}\times F_{2}$ and searching for a
loop. As the product ${\mathcal{A}}_{1}\times{\mathcal{A}}_{2}$ is polynomial
in $S$, the construction of $C$ is clearly possible in polynomial time.

To see that the construction is correct, let $q$ be a state of $\mathcal{T}$
such that $(q,q_{1})$ and $(q,q_{2})$ are reachable in
$\mathcal{T}\times{\mathcal{A}}_{1}$ and $\mathcal{T}\times{\mathcal{A}}_{2}$,
respectively, and $(q_{1},q_{2})\in C$. Further, let
$r_{1},r_{2}\in\Sigma^{*}$ be such that $\mathcal{T}\times{\mathcal{A}}_{i}$
reaches $(q,q_{i})$ when reading $r_{i}$ from the initial state. As
$(q_{1},q_{2})\in C$, there exists an infinite run from $(q_{1},q_{2})$ in
${\mathcal{A}}_{1}\times{\mathcal{A}}_{2}$, which stays in $F_{1}\times
F_{2}$. This means for some $x\in\Sigma^{*},y\in\Sigma^{+}$ we have
$(q_{1},q_{2})\xrightarrow{x}(p_{1},p_{2})\xrightarrow{y}(p_{1},p_{2})$ while
only visiting states from $F_{1}\times F_{2}$. Then $r_{1}xy^{\omega}\in
S_{+}$ and $r_{2}xy^{\omega}\in S_{-}$ and because $r_{1}$ and $r_{2}$ reach
the same state in $\mathcal{T}$, $\mathcal{T}$ cannot be MN-consistent with
$S$.

For the other direction, assume that $\mathcal{T}$ is not MN-consistent with
$S$. This means there exist $xw,yw\in S$ with $xw\in S_{+}$ and $yw\in S_{-}$,
but $x$ and $y$ lead to the same state $q$ in $\mathcal{T}$. The pair
$(q_{1},q_{2}):=(\delta^{*}_{1}(\iota_{1},x),\delta^{*}_{2}(\iota_{2},y))$ is
in $C$, because for each prefix $z$ of $w$,
$xz,yz\in\operatorname{\mathsf{Prf}}{S}$, guaranteeing that there exists an
infinite run that starts in $(q_{1},q_{2})$ and remains in $F_{1}\times
F_{2}$.

Overall, $\mathcal{T}$ is _not MN-consistent_ with $S$, if and only if there
is some $q$ in $\mathcal{T}$ such that $(q,q_{1})$ and $(q,q_{2})$ are
reachable in $\mathcal{T}\times{\mathcal{A}}_{1}$ and
$\mathcal{T}\times{\mathcal{A}}_{2}$, respectively, and $(q_{1},q_{2})\in C$.
As the sizes of ${\mathcal{A}}_{1},{\mathcal{A}}_{2}$ and $C$ are polynomial
in $|S|$, it follows from the remarks preceding this proof that MN-consistency
can be checked in polynomial time.

See 5.3

######  Proof C2.

The proof of this lemma is analogous to the preceding Lemma 5.2, but differs
in the construction of the ${\mathcal{A}}_{1},{\mathcal{A}}_{2}$ and the
conflict relation. We build the DFAs such that

  * •

${\mathcal{A}}_{1}$ accepts a word $x$ if $x\in E_{c}^{\sim}$ and
$x^{\omega}\in S_{c,+}$, whereas

  * •

${\mathcal{A}}_{2}$ accepts $x$ if $x\in E_{c}^{\sim}$ and $x^{\omega}\in
S_{c,-}$.

Let $\check{R}_{c,\sigma}$ for $\sigma\in\\{+,-\\}$ be a set consisting all
$x^{\omega}$ such that $x$ is the shortest word with $x^{\omega}=w$ for some
$w\in R_{c,\sigma}$. To see that such a shortest $x$ can be computed in
polynomial time, note that because $S$ contains only ultimately periodic
words, $w=u^{\omega}$ for some $u=a_{0}\dotsc a_{n}\in\Sigma^{+}$. Then
$x=a_{0}\dotsc a_{i}$ for the least $i\leq n$ such that $(a_{0}\dotsc
a_{i})^{\omega}=u^{\omega}$. Checking for equality can be done in polynomial
time because two distinct periodic words $v_{1}^{\omega},v_{2}^{\omega}$ must
differ in one the first $|v_{1}|\cdot|v_{2}|$ letters. This can be shown by a
simple combinatorial argument, see e.g. Lemma 23 in [10].

For the DFAs ${\mathcal{A}}_{1},{\mathcal{A}}_{2}$, we begin with the prefix
tree for $\check{R}_{c}$, to which we add a rejecting sink that is reached on
all words which are not a prefix of $\check{R}_{c}$. Additionally, we attach
loops to states of the prefix tree that are only reached on exactly one word
from $\check{R}_{c}$. Finally, we intersect the resulting automata with DFAs
${\mathcal{A}}_{E,c,\sim}$ for $E_{c}^{\sim}$, which can be directly obtained
from the transition structure of $\sim$ by using $c$ as initial and final
state. Note that we need to prevent ${\mathcal{A}}_{E,c,\sim}$ from accepting
the empty word, which can be achieved by building the product with a simple
two state DFA. Overall, the size of ${\mathcal{A}}_{1}$ and
${\mathcal{A}}_{2}$ is clearly polynomial in $|S|$.

The conflict relation is the least relation $C$ over $Q_{1}\times Q_{2}$
containing $F_{1}\times F_{2}$ and verifying that
$(\delta_{1}(q_{1},a),\delta_{2}(q_{2},a))\in C$ implies $(q_{1},q_{2})\in C$.
The relation $C$ can be obtained by a fixpoint iteration, ensuring that the
number of iterations is bounded by $|Q_{1}\times Q_{2}|$. Thus, the
computation of $C$ is possible in polynomial time.

For the correctness of the construction, let $q$ be a state of a partial TS
$\mathcal{T}$ which is MN-consistent with $S$. Further, let $(q,q_{1})$ and
$(q,q_{2})$ with $(q_{1},q_{2})\in C$ be reachable on $r_{1}$ in
$\mathcal{T}\times{\mathcal{A}}_{1}$ and on $r_{2}$ in
$\mathcal{T}\times{\mathcal{A}}_{2}$, respectively. As $(q_{1},q_{2})\in C$,
there must exist some word $x\in\Sigma^{*}$ such that
$(p_{1},p_{2}):=(\delta^{*}_{1}(q_{1},x),\delta^{*}_{2}(q_{2},x))\in
F_{1}\times F_{2}$. This means $r_{1}x,r_{2}x\in E_{c}^{\sim}$ and
$(r_{1}x)^{\omega},(r_{2}x)^{\omega}\in S_{c}$ with $((r_{1}x)^{\omega}\in
S_{c,+}\Leftrightarrow(r_{2}x)^{\omega}\in S_{c,-}$. But then because $r_{1}$
and $r_{2}$ reach the same state in $\mathcal{T}$, it follows that
$\mathcal{T}$ is not iteration consistent with $(S,\sim,c)$.

For the other direction, assume that $\mathcal{T}$ is MN-consistent with $S$
but not iteration consistent with $(S,\sim,c)$. This means we can find
$xz,yz\in E^{\sim}_{c}$ such that $(xz)^{\omega}\in S_{+}$, $(yz)^{\omega}\in
S_{-}$ and $x,y$ lead to the same state $p$ in $\mathcal{T}$. Clearly it holds
that $(q_{1},q_{2}):=(\delta^{*}_{1}(xz),\delta^{*}_{2}(yz))\in F_{1}\times
F_{2}\subseteq C$. Moreover, our definition of $C$ ensures that removing the
common suffix $z$ from both words retains membership in $C$, meaning
$(\delta^{*}_{1}(x),\delta^{*}_{2}(y))\in C$.

Overall, we obtain that $\mathcal{T}$ is _not_ iteration consistent with
$(S,\sim,c)$, if and only if there is some $q$ in $\mathcal{T}$ such that
$(q,q_{1})$ and $(q,q_{2})$ are reachable in
$\mathcal{T}\times{\mathcal{A}}_{1}$ and $\mathcal{T}\times{\mathcal{A}}_{2}$,
respectively, and $(q_{1},q_{2})\in C$. As
${\mathcal{A}}_{1},{\mathcal{A}}_{2}$ and $C$ can be constructed in polynomial
time, checking for iteration consistency effectively reduces to computing the
reachable states in the two products $\mathcal{T}\times{\mathcal{A}}_{1}$ and
$\mathcal{T}\times{\mathcal{A}}_{2}$ and checking whether a pair with the
properties outlined above exists. This is clearly possible time polynomial in
the size of $|\mathcal{T}|$, $|{\mathcal{A}}_{1}|$ and $|{\mathcal{A}}_{2}|$,
thus concluding the proof.

We can now prove that $\operatorname{\mathsf{DPAInf}}$ indeed terminates in
polynomial time and returns a DPA that is consistent with the given input
sample $S$.

See 5.5

######  Proof C3.

Let $S=(S_{+},S_{-})$ be the sample on which $\operatorname{\mathsf{DPAInf}}$
is called. If step 4 terminates, then by definition of the procedure, it does
so with a DPA $\mathcal{B}$ that is consistent with $S$. Thus, it remains to
show that $\operatorname{\mathsf{DPAInf}}$ always terminates in polynomial
time. In the following, we consider each step of the algorithm individually:

  * •

In Lemma 5.2 and Lemma 5.3, it was established that the two constraint
functions $\operatorname{\mathsf{LRC-cons}}$ and $\operatorname{\mathsf{PRC-
cons}}$, which are passed to $\operatorname{\mathsf{GLeRC}}$, run in
polynomial time. Thus by Proposition 5.1, it follows that the first step
terminates in polynomial time.

  * •

The second step begins by computing the infinity sets of all sample words from
$R_{c}$ in the respective PRC $\approx_{c}$ for a $c\in[\sim]$, which is
possible in time polynomial in $|\approx_{c}|$ and $S$. Further, the number of
distinct priorities is bounded for each class $c\in[\sim]$ by the number of
SCCs in $\approx_{c}$. Therefore the computation of each $\kappa_{c}$
terminates after at most polynomially many iterations. Since each iteration
consists of a reachability analysis and some elementary operations, the
construction of $\overline{{\mathcal{M}}}$ is clearly possible in polynomial
time.

  * •

We use ${{\mathcal{A}}}_{\bowtie}$ to denote
${{\mathcal{A}}}_{\bowtie}(\overline{{\mathcal{M}}})$. For the computation of
$\mathcal{B}$, we first build what we call a _colored sample_ $\hat{S}$ as
follows. For each sample word $uv^{\omega}\in S$, we compute sequence of
colors produced by ${{\mathcal{A}}}_{\bowtie}$ on $uv^{\omega}$. By Lemma
3.15, we can write this sequence as $rs^{\omega}$, where $|rs|$ is polynomial
in $|uv|$ and $|\overline{{\mathcal{M}}}|$. The product of $uv^{\omega}$ with
$rs^{\omega}$ (which is a sequence of letter-priority pairs), is clearly
polynomial in $|S|$. Overall, the size of the colored sample $\hat{S}$ is
polynomial in $|S|$.
The DPA $\mathcal{B}$ uses the transition structure $\mathcal{T}$ for the
default relation $\sim_{\hat{S}}$ for the colored sample $\hat{S}$, which can
be constructed as outlined after Definition 5.4. The priority for a transition
in $\mathcal{B}$, that originates in some state $q$ on a letter $a\in\Sigma$
can then be defined as follows. If there is no
$xa\in\operatorname{\mathsf{Prf}}{S}$, where $x$ reaches $q$, then we set
$\kappa(q,a)=0$. Otherwise, let
$(a_{1},c_{1})\dotsc(a_{n},c_{n})\in\operatorname{\mathsf{Prf}}{\hat{S}}$ be
such that $a_{1}\dotsc a_{n}=xa$. By definition of $\hat{S}$, such a word
clearly has to exist. The priority of the $a$-transition from $q$ in
$\mathcal{B}$ is then set to $c_{n}$, i.e. the priority of the position in the
colored word $(a_{1},c_{1})\dotsc(a_{n},c_{n})$ reached by $ua$. Clearly,
every step in the computation can be done in polynomial time.
In case $\mathcal{B}$ is not consistent with $S$,
$\operatorname{\mathsf{DPAInf}}$ constructs a fallback DPA, which we denote
$\mathcal{B}_{0}$ in the following. Then, we construct $\mathcal{T}$, the
transition structure of the default structure $\sim_{R}$. Finally, we assign
the priority $1$ to all transitions which do not reach the sink state and
priority $0$ to every transition whose target is the sink state. As the
construction of both $\mathcal{B}$ and the fallback DPA can be achieved in
polynomial time, it is guaranteed that the third step terminates in polynomial
time.

  * •

Finally in step 4, all answers provided to $\operatorname{\mathsf{MMAL}}$ are
consistent with the DPA $\mathcal{B}$ from step 3, which by the previous
considerations is polynomial in $|S|$. Since $\mathcal{B}$ itself is
consistent with $S$, it follows from the properties of
$\operatorname{\mathsf{MMAL}}$, that it terminates at the latest with the DPA
$\mathcal{B}$, or it terminates earlier with a strictly smaller DPA that is
consistent with $S$.
To conclude that the execution of $\operatorname{\mathsf{MMAL}}$ indeed
terminates in polynomial time, we need to verify that each counterexample
provided by the teacher is polynomial in $|S|$. So let $\mathcal{H}$ be the
hypothesis posed by $\operatorname{\mathsf{MMAL}}$, which is not consistent
with $S$. This means $\mathcal{H}$ and $\mathcal{B}$ viewed as Mealy machines
compute different priority mappings and a counterexample correponds to a
prefix $x$ of $S$ witnessing that $\mathcal{H}(x)\neq\mathcal{B}(x)$. As all
hypotheses given by $\operatorname{\mathsf{MMAL}}$ in an equivalence query
have at most as many states as $\mathcal{B}$, the shortest such $x$ is clearly
polynomial in $S$.