1–LABEL:LastPageDec. 29, 2016Feb. 14, 2018

*The present article extends [ABF16].

# Families of DFAs as Acceptors of $\omega$-Regular Languages*

Dana Angluin  Yale University, New Haven, CT, USA  ,  Udi Boker
Interdisciplinary Center (IDC), Herzliya, Israel  and  Dana Fisman  Ben-Gurion
University, Beer-Sheva, Israel

###### Abstract.

Families of dfas (fdfas) provide an alternative formalism for recognizing
$\omega$-regular languages. The motivation for introducing them was a desired
correlation between the automaton states and right congruence relations, in a
manner similar to the Myhill-Nerode theorem for regular languages. This
correlation is beneficial for learning algorithms, and indeed it was recently
shown that $\omega$-regular languages can be learned from membership and
equivalence queries, using fdfas as the acceptors.

In this paper, we look into the question of how suitable fdfas are for
defining $\omega$-regular languages. Specifically, we look into the complexity
of performing Boolean operations, such as complementation and intersection, on
fdfas, the complexity of solving decision problems, such as emptiness and
language containment, and the succinctness of fdfas compared to standard
deterministic and nondeterministic $\omega$-automata.

We show that fdfas enjoy the benefits of deterministic automata with respect
to Boolean operations and decision problems. Namely, they can all be performed
in nondeterministic logarithmic space. We provide polynomial translations of
deterministic B$\ddot{\textrm{u}}$chi and co-B$\ddot{\textrm{u}}$chi automata
to fdfas and of fdfas to nondeterministic B$\ddot{\textrm{u}}$chi automata
(nbas). We show that translation of an nba to an fdfa may involve an
exponential blowup. Last, we show that fdfas are more succinct than
deterministic parity automata (dpas) in the sense that translating a dpa to an
fdfa can always be done with only a polynomial increase, yet the other
direction involves an inevitable exponential blowup in the worst case.

###### Key words and phrases:

Finite automata, Omega-Regular Languages

This research was supported by the United States - Israel Binational Science
Foundation (BSF) grant 2016239 and the Israel Science Foundation (ISF) grant
1373/16.

##  1\. Introduction

The theory of finite-state automata processing infinite words was developed in
the early sixties, starting with B$\ddot{\textrm{u}}$chi [Büc60] and Muller
[Mul63], and motivated by problems in logic and switching theory. Today,
automata for infinite words are extensively used in verification and synthesis
of _reactive systems_ , such as operating systems and communication protocols.

An automaton processing finite words makes its decision according to the last
visited state. On infinite words, B$\ddot{\textrm{u}}$chi defined that a run
is accepting if it visits a designated set of states infinitely often. Since
then several other accepting conditions were defined, giving rise to various
$\omega$-automata, among which are Muller, Rabin, Streett and parity automata.

The theory of $\omega$-regular languages is more involved than that of finite
words. This was first evidenced by B$\ddot{\textrm{u}}$chi’s observation that
nondeterministic B$\ddot{\textrm{u}}$chi automata are more expressive than
their deterministic counterpart. While for some types of $\omega$-automata the
nondeterministic and deterministic variants have the same expressive power,
none of them possesses all the nice qualities of acceptors for finite words.
In particular, none has a corresponding Myhill-Nerode theorem [Ner58], i.e. a
direct correlation between the states of the automaton and the equivalence
classes corresponding to the canonical right congruence of the recognized
language.

The absence of a Myhill-Nerode like property in $\omega$-automata has been a
major drawback in obtaining learning algorithms for $\omega$-regular
languages, a question that has received much attention lately due to
applications in verification and synthesis, such as black-box checking
[PVY02], assume-guarantee reasoning [AvMN05, PGB+08, CCF+10, FKP11], error
localization [WN05, CCK+15], regular model checking [VSVA05, NJ13], finding
security bugs [RMSM09, CPPdR14, FJV14], programming networks [RMSM09, YAL14]
and more. The reason is that learning algorithms typically build on this
correspondence between the automaton and the right congruence.

Recently, several algorithms for learning an unknown $\omega$-regular language
were proposed, all using non-conventional acceptors. One uses a reduction due
to [CNP93] named $L_{\$}$-automata of $\omega$-regular languages to regular
languages [FCTW08], and the others use a representation termed _families of
dfas_ [AF14, LCZL16]. Both representations are founded on the following well
known property of $\omega$-regular languages: two $\omega$-regular languages
are equivalent iff they agree on the set of ultimately periodic words. An
ultimately periodic word $uv^{\omega}$, where $u\in\Sigma^{*}$ and
$v\in\Sigma^{+}$, can be represented as a pair of finite words $(u,v)$. Both
$L_{\$}$-automata and families of dfas process such pairs and interpret them
as the corresponding ultimately periodic words. Families of dfas have been
shown to be up to exponentially more succinct than $L_{\$}$-automata [AF14].

A family of dfas (fdfa) is composed of a _leading automaton_ ${{\mathcal{Q}}}$
with no accepting states and for each state $q$ of ${{\mathcal{Q}}}$, a
_progress dfa_ ${{\mathcal{P}}}_{q}$. Intuitively, the leading automaton is
responsible for processing the non-periodic part $u$, and depending on the
state $q$ reached when ${{\mathcal{Q}}}$ terminated processing $u$, the
respective progress dfa ${{\mathcal{P}}}_{q}$ processes the periodic part $v$,
and determines whether the pair $(u,v)$, which corresponds to $uv^{\omega}$,
is accepted. (The exact definition is more subtle and is provided in Section
3.) If the leading automaton has $n$ states and the size of the maximal
progress dfa is $k$, we say that the fdfa is of size $(n,k)$. An earlier
definition of fdfas, given in [Kla94], provided a machine model for the
_families of right congruences_ of [MS97].111Another related formalism is of
Wilke algebras [Wil91, Wil93], which are two-sorted algebras equipped with
several operations. An $\omega$-language over $\Sigma^{\omega}$ is
$\omega$-regular if and only if there exists a two-sorted morphism from
$\Sigma^{\infty}$ into a finite Wilke structure [Wil91]. A central difference
between the FDFA theory and the algebraic theory of recognition by monoids,
semigroups, $\omega$-semigroups, and Wilke structures is that the former
relates to right-congruences, while the latter is based on two-sided
congruences. They were redefined in [AF14], where their acceptance criterion
was adjusted, and their size was reduced by up to a quadratic factor. We
follow the definition of [AF14].

In order for an fdfa to properly characterize an $\omega$-regular language, it
must satisfy the _saturation_ property: considering two pairs $(u,v)$ and
$(u^{\prime},v^{\prime})$, if $uv^{\omega}=u^{\prime}v^{\prime\omega}$ then
either both $(u,v)$ and $(u^{\prime},v^{\prime})$ are accepted or both are
rejected (cf. [CNP93, Saë90]). Saturated fdfas are shown to exactly
characterize the set of $\omega$-regular languages. Saturation is a semantic
property, and the check of whether a given fdfa is saturated is shown to be in
PSPACE. Luckily, the fdfas that result from the learning algorithm of [AF14]
are guaranteed to be saturated.

Saturated fdfas bring an interesting potential – they have a Myhill-Nerode
like property, and while they are “mostly” deterministic, a nondeterministic
aspect is hidden in the separation of the prefix and period parts of an
ultimately periodic infinite word. This gives rise to the natural questions of
how “dominant” are the determinism and nondeterminism in fdfas, and how “good”
are they for representing $\omega$-regular languages. These abstract questions
translate to concrete questions that concern the succinctness of fdfas and the
complexity of solving their decision problems, as these measures play a key
role in the usefulness of applications built on top of them.

Our purpose in this paper is to analyze the fdfa formalism and answer these
questions. Specifically, we ask: What is the complexity of performing the
Boolean operations of complementation, union, and intersection on saturated
fdfas? What is the complexity of solving the decision problems of membership,
emptiness, universality, equality, and language containment for saturated
fdfas? How succinct are saturated fdfas, compared to deterministic and
nondeterministic $\omega$-automata?

We show that saturated fdfas enjoy the benefits of deterministic automata with
respect to Boolean operations and decision functions. Namely, the Boolean
operations can be performed in logarithmic space, and the decision problems
can be solved in nondeterministic logarithmic space. The constructions and
algorithms that we use extend their counterparts on standard dfas. In
particular, complementation of saturated fdfas can be obtained on the same
structure, and union and intersection is done on a product of the two given
structures. The correctness proof of the latter is a bit subtle.

As for the succinctness, which turns out to be more involved, we show that
saturated fdfas properly lie in between deterministic and nondeterministic
$\omega$-automata. We provide polynomial translations from deterministic
$\omega$-automata to fdfas and from fdfas to nondeterministic
$\omega$-automata, and show that an exponential state blowup in the opposite
directions is inevitable in the worst case.

Specifically, a saturated fdfa of size $(n,k)$ can always be transformed into
an equivalent nondeterministic B$\ddot{\textrm{u}}$chi automaton (nba) with
$O(n^{2}k^{3})$ states. (Recall that an fdfa of size $(n,k)$ can have up to
$n+nk$ states in total, having $n$ states in the leading automaton and up to
$k$ states in each of the $n$ progress automata.) As for the other direction,
transforming an nba with $n$ states to an equivalent fdfa is shown to be in
$2^{\Theta(n\log n)}$. This is not surprising since, as shown by Michel
[Mic88], complementing an nba involves a $2^{\Omega(n\log n)}$ state blowup,
while fdfa complementation requires no state blowup.

Considering deterministic $\omega$-automata, a B$\ddot{\textrm{u}}$chi or
co-B$\ddot{\textrm{u}}$chi automaton (dba or dca) with $n$ states can be
transformed into an equivalent fdfa of size $(n,2n)$, and a deterministic
parity automaton (dpa) with $n$ states and $k$ colors can be transformed into
an equivalent fdfa of size $(n,kn)$. As for the other direction, since dba and
dca do not recognize all the $\omega$-regular languages, while saturated fdfas
do, a transformation from an fdfa to a dba or dca need not exist. Comparing
fdfas to dpas, which do recognize all $\omega$-regular languages, we get that
fdfas can be exponentially more succinct: We show a family of languages
$\\{L_{n}\\}_{n\geq 1}$, such that for every $n$, there exists an fdfa of size
$(n+1,n^{2})$ for $L_{n}$, but any dpa recognizing $L_{n}$ must have at least
$2^{n-1}$ states. (A deterministic Rabin or Streett automaton for $L_{n}$ is
also shown to be exponential in $n$, requiring at least $2^{\frac{n}{2}}$
states.)

##  2\. Preliminaries

An _alphabet_ $\Sigma$ is a finite set of symbols. The set of finite words
over $\Sigma$ is denoted by $\Sigma^{*}$, and the set of infinite words,
termed $\omega$-words, over $\Sigma$ is denoted by $\Sigma^{\omega}$. As
usual, we use $x^{*}$, $x^{+}$, and $x^{\omega}$ to denote finite, non-empty
finite, and infinite concatenations of $x$, respectively, where $x$ can be a
symbol or a finite word. We use $\epsilon$ for the empty word. An infinite
word $w$ is _ultimately periodic_ if there are two finite words
$u\in\Sigma^{*}$ and $v\in\Sigma^{+}$, such that $w=uv^{\omega}$. A _language_
is a set of finite words, that is, a subset of $\Sigma^{*}$, while an
$\omega$-language is a set of $\omega$-words, that is, a subset of
$\Sigma^{\omega}$. For natural numbers $i$ and $j$ and a word $w$, we use
$[i..j]$ for the set $\\{i,i+1,\ldots,j\\}$, $w[i]$ for the $i$-th letter of
$w$, and $w[i..j]$ for the subword of $w$ starting at the $i$-th letter and
ending at the $j$-th letter, inclusive.

An _automaton_ is a tuple ${\mathcal{A}}=\langle\Sigma,Q,\iota,\delta\rangle$
consisting of an alphabet $\Sigma$, a finite set $Q$ of states, an initial
state $\iota\in Q$, and a transition function $\delta:Q\times\Sigma\rightarrow
2^{Q}$. A run of an automaton on a finite word $v=a_{1}a_{2}\ldots a_{n}$ is a
sequence of states ${q_{0},q_{1},\ldots,q_{n}}$ such that $q_{0}=\iota$, and
for each $i\geq 0$, ${q_{i+1}\in\delta(q_{i},a_{i})}$. A run on an infinite
word is defined similarly and results in an infinite sequence of states. The
transition function is naturally extended to a function
$\delta:Q\times\Sigma^{*}\rightarrow 2^{Q}$, by defining
$\delta(q,\epsilon)=\\{q\\}$, and
$\delta(q,av)=\cup_{p\in\delta(q,a)}\delta(p,v)$ for ${q\in Q}$,
${a\in\Sigma}$, and ${v\in\Sigma^{*}}$. We often use ${\mathcal{A}}(v)$ as a
shorthand for $\delta(\iota,v)$ and $|{\mathcal{A}}|$ for the number of states
in $Q$. We use ${\mathcal{A}}^{q}$ to denote the automaton
$\langle\Sigma,Q,q,\delta\rangle$ obtained from ${\mathcal{A}}$ by replacing
the initial state with $q$. We say that ${\mathcal{A}}$ is _deterministic_ if
$|\delta(q,a)|\leq 1$ and _complete_ if $|\delta(q,a)|\geq 1$, for every $q\in
Q$ and $a\in\Sigma$. For simplicity, we consider all automata to be complete.
(As is known, every automaton can be linearly translated to an equivalent
complete automaton, with respect to the relevant equivalence notion, as
defined below.)

By augmenting an automaton with an acceptance condition $\alpha$, thereby
obtaining a tuple $\langle\Sigma,Q,\iota,$ $\delta,\alpha\rangle$, we get an
_acceptor_ , a machine that accepts some words and rejects others. An acceptor
accepts a word if at least one of the runs on that word is accepting. For
finite words the acceptance condition is a set $F\subseteq Q$ of _accepting
states_ , and a run on a word $v$ is accepting if it ends in an accepting
state, i.e., if $\delta(\iota,v)$ contains an element of $F$. For infinite
words, there are various acceptance conditions in the literature; here we
mention three: B$\ddot{\textrm{u}}$chi, co-B$\ddot{\textrm{u}}$chi, and
parity.222There are other acceptance conditions in the literature, the most
known of which are weak, Rabin, Streett, and Muller. The three conditions that
we concentrate on are the most used ones; B$\ddot{\textrm{u}}$chi and
co-B$\ddot{\textrm{u}}$chi due to their simplicity, and parity due to being
the simplest for which the deterministic variant is strong enough to express
all $\omega$-regular languages. The B$\ddot{\textrm{u}}$chi and
co-B$\ddot{\textrm{u}}$chi acceptance conditions are also a set $F\subseteq
Q$. A run of a B$\ddot{\textrm{u}}$chi automaton is accepting if it visits $F$
infinitely often. A run of a co-B$\ddot{\textrm{u}}$chi automaton is accepting
if it visits $F$ only finitely many times. A parity acceptance condition is a
map $\kappa:Q\rightarrow[1..k]$ assigning each state a color (or rank). A run
is accepting if the minimal color visited infinitely often is odd. We use
${{\llbracket{\mathcal{A}}\rrbracket}}$ to denote the set of words accepted by
a given acceptor ${\mathcal{A}}$, and say that ${\mathcal{A}}$ _accepts_ or
_recognizes_ ${{\llbracket{\mathcal{A}}\rrbracket}}$. Two acceptors
${\mathcal{A}}$ and ${{\mathcal{B}}}$ are _equivalent_ if
${{\llbracket{\mathcal{A}}\rrbracket}}={{\llbracket{{\mathcal{B}}}\rrbracket}}$.

We use three letter acronyms to describe acceptors, where the first letter is
either d or n depending on whether the automaton is _deterministic_ or
_nondeterministic_ , respectively. The second letter is one of
$\\{\textsc{f,b,c,p}\\}$: f if this is an acceptor over finite words, b, c, or
p if it is an acceptor over infinite words with B$\ddot{\textrm{u}}$chi,
co-B$\ddot{\textrm{u}}$chi, or parity acceptance condition, respectively. The
third letter is always a for an acceptor (or automaton).

For finite words, nfa and dfa have the same expressive power. A language is
said to be _regular_ if it is accepted by an nfa. For infinite words, the
theory is more involved. While npas, dpas, and nbas have the same expressive
power, dbas, ncas, and dcas are strictly weaker than nbas. An
$\omega$-language is said to be _$\omega$ -regular_ if it is accepted by an
nba.

##  3\. Families of DFAs (FDFAs)

It is well known that two $\omega$-regular languages are equivalent if they
agree on the set of ultimately periodic words (this is a consequence of
McNaughton’s theorem [McN66]). An ultimately periodic word $uv^{\omega}$,
where $u\in\Sigma^{*}$ and $v\in\Sigma^{+}$, is usually represented by the
pair $(u,v)$. A canonical representation of an $\omega$-regular language can
thus consider only ultimately periodic words, namely define a language of
pairs $(u,v)\in\Sigma^{*}\times\Sigma^{+}$. Such a representation
${{\mathcal{F}}}$ should satisfy the _saturation_ property: considering two
pairs $(u,v)$ and $(u^{\prime},v^{\prime})$, if
$uv^{\omega}=u^{\prime}v^{\prime\omega}$ then either both $(u,v)$ and
$(u^{\prime},v^{\prime})$ are accepted by ${{\mathcal{F}}}$ or both are
rejected by ${{\mathcal{F}}}$.

A family of dfas (fdfa) accepts such pairs $(u,v)$ of finite words.
Intuitively, it consists of a deterministic _leading automaton_
${{\mathcal{Q}}}$ with no acceptance condition that runs on the prefix-word
$u$, and for each state $q$ of ${{\mathcal{Q}}}$, a _progress automaton_
${{\mathcal{P}}}_{q}$, which is a dfa that runs on the period-word $v$.

A straightforward definition of acceptance for a pair $(u,v)$, could have been
that the run of the leading automaton ${{\mathcal{Q}}}$ on $u$ ends at some
state $q$, and the run of the progress automaton ${{\mathcal{P}}}_{q}$ on $v$
is accepting. This goes along the lines of $L_{\$}$-automata [CNP93]. However,
such an acceptance definition does not fit well the saturation requirement,
and might enforce very large automata [AF14]. The intuitive reason is that
every progress automaton might need to handle the period-words of all prefix-
words.

To better fit the saturation requirement, the acceptance condition of an fdfa
is defined with respect to a _normalization_ of the input pair $(u,v)$. The
normalization is a new pair $(x,y)$, such that $xy^{\omega}=uv^{\omega}$, and
in addition, the run of the leading automaton ${{\mathcal{Q}}}$ on $xy^{i}$
ends at the same state for every natural number $i$. Over the normalized pair
$(x,y)$, the acceptance condition follows the straightforward approach
discussed above. This normalization resembles the implicit flexibility in the
acceptance conditions of $\omega$-automata, such as the
B$\ddot{\textrm{u}}$chi condition, and allows saturated fdfas to be up to
exponentially more succinct than $L_{\$}$-automata [AF14].

Below, we formally define an fdfa, the normalization of an input pair $(u,v)$,
and the acceptance condition. We shall use ${\Sigma^{*+}}$ as a shorthand for
$\Sigma^{*}\times\Sigma^{+}$, whereby the input to an fdfa is a pair
$(u,v)\in{\Sigma^{*+}}$.

[A family of dfas (fdfa)]333The fdfas defined here follow the definition in
[AF14], which is a little different from the definition of fdfas in [Kla94];
the latter provide a machine model for the families of right congruences
introduced in [MS97]. The main differences between the two definitions are: i)
In [Kla94], a pair $(u,v)$ is accepted by an fdfa
${{\mathcal{F}}}=({{\mathcal{Q}}},{{\mathbf{P}}})$ if there is some
factorization $(x,y)$ of $(u,v)$, such that ${{\mathcal{Q}}}(x)=q$ and
${{\mathcal{P}}}_{q}$ accepts $y$; and ii) in [Kla94], the fdfa
${{\mathcal{F}}}$ should also satisfy the constraint that for all words
$u\in\Sigma^{*}$ and $v,v^{\prime}\in\Sigma^{+}$, if
${{\mathcal{P}}}_{{{\mathcal{Q}}}(u)}(v)={{\mathcal{P}}}_{{{\mathcal{Q}}}(u)}(v^{\prime})$
then ${{\mathcal{Q}}}(uv)={{\mathcal{Q}}}(uv^{\prime})$.

  * •

A _family of dfas_ (fdfa) is a pair $({{\mathcal{Q}}},{{\mathbf{P}}})$, where
${{\mathcal{Q}}}=(\Sigma,Q,\iota,\delta)$ is a deterministic _leading_
automaton, and ${{\mathbf{P}}}$ is a set of $|{{\mathcal{Q}}}|$ dfas,
including for each state $q\in Q$, a _progress_ dfa
${{\mathcal{P}}}_{q}=(\Sigma,P_{q},\iota_{q},\delta_{q},F_{q})$.

  * •

Given a pair $(u,v)\in{\Sigma^{*+}}$ and an automaton ${\mathcal{A}}$, the
_normalization_ of $(u,v)$ w.r.t ${\mathcal{A}}$ is the pair
$(x,y)\in{\Sigma^{*+}}$, such that $x={u}{v}^{i}$, $y={v}^{j}$, and $i\geq 0$,
$j\geq 1$ are the smallest numbers for which
${\mathcal{A}}({u}{v}^{i})={\mathcal{A}}({u}{v}^{i+j})$. (By “smallest
numbers” $(i,j)$, one can consider lexicographic order, having the smallest
$i$, and for it the smallest $j$. By Fine and Wilf’s theorem, however, there
is no ambiguity by just requiring “smallest numbers”. Notice that since we
consider complete automata, such a unique pair $(x,y)$ is indeed guaranteed.)

  * •

Let ${{\mathcal{F}}}=({{\mathcal{Q}}},{{\mathbf{P}}})$ be an fdfa,
$(u,v)\in{\Sigma^{*+}}$, and $(x,y)\in{\Sigma^{*+}}$ the normalization of
$(u,v)$ w.r.t ${{\mathcal{Q}}}$. We say that $(u,v)$ is _accepted_ by
${{\mathcal{F}}}$ iff ${{\mathcal{Q}}}(x)=q$ for some state $q$ of
${{\mathcal{Q}}}$ and ${{\mathcal{P}}}_{q}(y)$ is an accepting state of
${{\mathcal{P}}}_{q}$.

  * •

We use ${\llbracket{{\mathcal{F}}}\rrbracket}$ to denote the set of pairs
accepted by ${{\mathcal{F}}}$.

  * •

We define the _size_ of ${{\mathcal{F}}}$, denoted by $|{{\mathcal{F}}}|$, as
the pair
$(|{{\mathcal{Q}}}|,\max\\{|{{\mathcal{P}}}_{q}|\\}_{q\in{{\mathcal{Q}}}})$.

  * •

An fdfa ${{\mathcal{F}}}$ is _saturated_ if for every two pairs $(u,v)$ and
$(u^{\prime},v^{\prime})$ such that $uv^{\omega}=u^{\prime}v^{\prime\omega}$,
either both $(u,v)$ and $(u^{\prime},v^{\prime})$ are in
${\llbracket{{\mathcal{F}}}\rrbracket}$ or both are not in
${\llbracket{{\mathcal{F}}}\rrbracket}$.

A saturated fdfa can be used to characterize an $\omega$-regular language (see
Theorem 8), while an unsaturated fdfa cannot.

An unsaturated fdfa is depicted in Figure 1 on the left. Consider the pairs
$(b,a)$ and $(ba,aa)$. The former is normalized into $(b,aa)$, as the run of
the leading automaton ${\mathcal{U}}$ on “$b$” reaches the state $l$, and then
when ${\mathcal{U}}$ iterates on “$a$”, the first state to be revisited is
$l$, which happens after two iterations. The latter is normalized into
$(ba,aa)$, namely it was already normalized. Now, $(b,a)$ is accepted since in
the run on its normalization $(b,aa)$, ${\mathcal{U}}$ reaches the state $l$
when running on “$b$”, and the progress automaton
${{\mathcal{P}}}_{l}^{\mathcal{U}}$ accepts “$aa$”. On the other hand,
$(ba,aa)$ is not accepted since the run of ${\mathcal{U}}$ on “$ba$” reaches
the state $r$, and the progress automaton ${{\mathcal{P}}}_{r}^{\mathcal{U}}$
does not accept “$aa$”. Yet, $ba^{\omega}=ba(aa)^{\omega}$, so the fdfa should
have either accepted or rejected both $(b,a)$ and $(ba,aa)$, were it
saturated, which is not the case.

A saturated fdfa is depicted in Figure 1 on the right. It accepts pairs of the
forms $(\Sigma^{*},a^{+})$ and $(\Sigma^{*},b^{+})$, and characterizes the
$\omega$-regular language $(a+b)^{*}(a^{\omega}+b^{\omega})$ of words in which
there are eventually only $a$’s or only $b$’s.

${\mathcal{U}}:$$l$$r$$b$$a$$a,b$${{\mathcal{P}}}_{l}^{\mathcal{U}}:$$a,b$${{\mathcal{P}}}_{r}^{\mathcal{U}}:$$a$$b$$a,b$${{\mathcal{S}}}:$$l$$r$$a$$b$$b$$a$${{\mathcal{P}}}_{l}^{{\mathcal{S}}}:$$a$$b$$a,b$${{\mathcal{P}}}_{r}^{{\mathcal{S}}}:$$b$$a$$a,b$

Figure 1. Left: an unsaturated fdfa with the leading automaton ${\mathcal{U}}$
and progress dfas ${{\mathcal{P}}}_{l}^{\mathcal{U}}$ and
${{\mathcal{P}}}_{r}^{\mathcal{U}}$. Right: a saturated fdfa with the leading
automaton ${{\mathcal{S}}}$ and progress dfas
${{\mathcal{P}}}_{l}^{{\mathcal{S}}}$ and
${{\mathcal{P}}}_{r}^{{\mathcal{S}}}$.

##  4\. Boolean Operations and Decision Procedures

We provide below algorithms for performing the Boolean operations of
complementation, union, and intersection on saturated fdfas, and deciding the
basic questions on them, such as emptiness, universality, and language
containment. All of these algorithms can be done in nondeterministic
logarithmic space, taking advantage of the partial deterministic nature of
fdfas.444Another model that lies in between deterministic and nondeterministic
automata are “semi-deterministic Büchi automata” [VW86], which are Büchi
automata that are deterministic in the limit: from every accepting state
onward, their behaviour is deterministic. Yet, as opposed to fdfas,
complementation of semi-deterministic Büchi automata might involve an
exponential state blowup [BHS+16]. We conclude the section with the decision
problem of whether an arbitrary fdfa is saturated, showing that it can be
resolved in polynomial space.

#### Boolean operations

Saturated fdfas are closed under Boolean operations as a consequence of
Theorem 8, which shows that they characterize exactly the set of
$\omega$-regular languages. We provide below explicit algorithms for these
operations, showing that they can be done effectively.

Complementation of an fdfa is simply done by switching between accepting and
non-accepting states in the progress automata, as is done with dfas.

######  Theorem 1.

Let ${{\mathcal{F}}}$ be an fdfa. There is a constant-space algorithm to
obtain an fdfa ${{\mathcal{F}}}^{c}$, such that
${\llbracket{{\mathcal{F}}}^{c}\rrbracket}={\Sigma^{*+}}\setminus{\llbracket{{\mathcal{F}}}\rrbracket}$,
$|{{\mathcal{F}}}^{c}|=|{{\mathcal{F}}}|$, and ${{\mathcal{F}}}^{c}$ is
saturated iff ${{\mathcal{F}}}$ is.

######  Proof 4.1.

Let ${{\mathcal{F}}}=({{\mathcal{Q}}},{{\mathbf{P}}})$, where for each state
$q$ of ${{\mathcal{Q}}}$, ${{\mathbf{P}}}$ has the dfa
${{\mathcal{P}}}_{q}=(\Sigma,P_{q},\iota_{q},\delta_{q},F_{q})$. We define
${{\mathcal{F}}}^{c}$ to be the fdfa $({{\mathcal{Q}}},{{\mathbf{P}}}^{c})$,
where for each state $q$ of ${{\mathcal{Q}}}$, ${{\mathbf{P}}}^{c}$ has the
dfa ${{\mathcal{P}}}^{c}_{q}=(\Sigma,P_{q},\iota_{q},\delta_{q},P_{q}\setminus
F_{q})$. We claim that ${{\mathcal{F}}}^{c}$ recognizes the complement
language of ${{\mathcal{F}}}$. Indeed, let $(u,v)\in{\Sigma^{*+}}$ and $(x,y)$
its normalization with respect to ${{\mathcal{Q}}}$. Then
$(u,v)\in{\llbracket{{\mathcal{F}}}\rrbracket}$ iff
$y\in{\llbracket{{\mathcal{P}}}_{{{\mathcal{Q}}}(x)}\rrbracket}$. Thus
$(u,v)\notin{\llbracket{{\mathcal{F}}}\rrbracket}$ iff
$y\notin{\llbracket{{\mathcal{P}}}_{{{\mathcal{Q}}}(x)}\rrbracket}$ iff
$y\in{\llbracket{{\mathcal{P}}}^{c}_{{{\mathcal{Q}}}(x)}\rrbracket}$ iff
$(u,v)\in{\llbracket{{\mathcal{F}}}^{c}\rrbracket}$.

Since ${{\mathcal{F}}}$ is saturated, so is ${{\mathcal{F}}}^{c}$, as for all
pairs $(u,v)$ and $(u^{\prime},v^{\prime})$ such that
$uv^{\omega}=u^{\prime}v^{\prime\omega}$, ${{\mathcal{F}}}$ either accepts or
rejects them both, implying that ${{\mathcal{F}}}^{c}$ either rejects or
accepts them both, respectively.

Union and intersection of saturated fdfas also resemble the case of dfas, and
are done by taking the product of the leading automata and each pair of
progress automata. Yet, the correctness proof is a bit subtle, and relies on
the following lemma, which shows that for a normalized pair $(x,y)$, the
period-word $y$ can be manipulated in a certain way, while retaining
normalization.

######  Lemma 2.

Let ${{\mathcal{Q}}}$ be an automaton, and let $(x,y)$ be the normalization of
some $(u,v)\in{\Sigma^{*+}}$ w.r.t. ${{\mathcal{Q}}}$. Then for every $i\geq
0$, $j\geq 1$ and finite words $y^{\prime},y^{\prime\prime}$ such that
$y=y^{\prime}y^{\prime\prime}$, we have that
$(xy^{i}y^{\prime},(y^{\prime\prime}y^{\prime})^{j})$ is the normalization of
itself w.r.t. ${{\mathcal{Q}}}$.

######  Proof 4.2.

Let $x_{1}=xy^{i}y^{\prime}$ and $y_{1}=(y^{\prime\prime}y^{\prime})^{j}$.
Since $(x,y)$ is normalized w.r.t. ${{\mathcal{Q}}}$, we know that the run of
${{\mathcal{Q}}}$ on $xy^{\omega}$ is of the form
$q_{0},q_{1},\ldots,q_{k-1},(q_{k},q_{k+1},$ $q_{k+2},\ldots,q_{m})^{\omega}$,
where $|x|=k$ and $|y|=(m-k)+1$. As $xy^{\omega}=x_{1}y_{1}^{\omega}$, the run
of ${{\mathcal{Q}}}$ on $x_{1}y_{1}^{\omega}$ is identical. Since $x$ is a
prefix of $x_{1}$, the position $|x_{1}|$ lies within the repeated period,
implying that $|x_{1}|$ is the first position, from $|x_{1}|$ onwards, that is
repeated along the aforementioned run. Since $y_{1}$ is a cyclic repetition of
$y$, and ${{\mathcal{Q}}}$ loops back over $y$, it also loops back over
$y_{1}$. Thus $(x_{1},y_{1})$ is the normalization of itself w.r.t. $Q$.

We continue with the union and intersection of saturated fdfas.

######  Theorem 3.

Let ${{\mathcal{F}}}_{1}$ and ${{\mathcal{F}}}_{2}$ be saturated fdfas of size
$(n_{1},k_{1})$ and $(n_{2},k_{2})$, respectively. There exist logarithmic-
space algorithms to obtain saturated fdfas ${{\mathcal{H}}}$ and
${{\mathcal{H}}}^{\prime}$ of size $(n_{1}n_{2},\ k_{1}k_{2})$, such that
${\llbracket{{\mathcal{H}}}\rrbracket}={\llbracket{{\mathcal{F}}}_{1}\rrbracket}\cap{\llbracket{{\mathcal{F}}}_{2}\rrbracket}$
and
${\llbracket{{\mathcal{H}}}^{\prime}\rrbracket}={\llbracket{{\mathcal{F}}}_{1}\rrbracket}\cup{\llbracket{{\mathcal{F}}}_{2}\rrbracket}$.

######  Proof 4.3.

The constructions of the union and intersection of fdfas are similar, only
differing by the accepting states. We shall thus describe them together.

##### Construction

Given two automata ${\mathcal{A}}_{1}$ and ${\mathcal{A}}_{2}$, where
${\mathcal{A}}_{i}=(\Sigma,A_{i},\iota_{i},\delta_{i})$, we denote by
${\mathcal{A}}_{1}\\!\times\\!{\mathcal{A}}_{2}$ the product automaton
$(\Sigma,A_{1}\\!\times\\!A_{2},(\iota_{1},\iota_{2}),\delta_{\times})$, where
for every $\sigma\in\Sigma$,
$\delta_{\times}((q_{1},q_{2}),\sigma)=(\delta(q_{1},\sigma),\delta(q_{2},\sigma))$.

Given two dfas ${{\mathcal{D}}}_{1}=({\mathcal{A}}_{1},F_{1})$ and
${{\mathcal{D}}}_{2}=({\mathcal{A}}_{2},F_{2})$, over the automata
${\mathcal{A}}_{1}$ and ${\mathcal{A}}_{2}$, and with the accepting states
$F_{1}$ and $F_{2}$, respectively, we define the dfas
${{\mathcal{D}}}_{1}\otimes{{\mathcal{D}}}_{2}$ and
${{\mathcal{D}}}_{1}\oplus{{\mathcal{D}}}_{2}$ as follows:

  * •

${{\mathcal{D}}}_{1}\otimes{{\mathcal{D}}}_{2}=({\mathcal{A}}_{1}\\!\times\\!{\mathcal{A}}_{2},F_{1}\\!\times\\!F_{2})$

  * •

${{\mathcal{D}}}_{1}\oplus{{\mathcal{D}}}_{2}=({\mathcal{A}}_{1}\\!\times\\!{\mathcal{A}}_{2},F_{1}\\!\times\\!A_{2}\cup
A_{1}\\!\times\\!F_{2})$

Given two sets of dfas ${{\mathbf{P}}}_{1}$ and ${{\mathbf{P}}}_{2}$, we
define the sets of dfas ${{\mathbf{P}}}_{1}\otimes{{\mathbf{P}}}_{2}$ and
${{\mathbf{P}}}_{1}\oplus{{\mathbf{P}}}_{2}$ as follows:

  * •

${{\mathbf{P}}}_{1}\otimes{{\mathbf{P}}}_{2}=\\{{{\mathcal{D}}}_{1}\otimes{{\mathcal{D}}}_{2}~{}|~{}{{\mathcal{D}}}_{1}\in{{\mathbf{P}}}_{1}\mbox{
and }{{\mathcal{D}}}_{2}\in{{\mathbf{P}}}_{2}\\}$

  * •

${{\mathbf{P}}}_{1}\oplus{{\mathbf{P}}}_{2}=\\{{{\mathcal{D}}}_{1}\oplus{{\mathcal{D}}}_{2}~{}|~{}{{\mathcal{D}}}_{1}\in{{\mathbf{P}}}_{1}\mbox{
and }{{\mathcal{D}}}_{2}\in{{\mathbf{P}}}_{2}\\}$

Given saturated fdfas
${{\mathcal{F}}}_{1}=({{\mathcal{Q}}}_{1},{{\mathbf{P}}}_{1})$ and
${{\mathcal{F}}}_{2}=({{\mathcal{Q}}}_{2},{{\mathbf{P}}}_{2})$, we claim that
${{\mathcal{H}}}=({{\mathcal{Q}}}_{1}\times{{\mathcal{Q}}}_{2},{{\mathbf{P}}}_{1}\otimes{{\mathbf{P}}}_{2})$
and
${{\mathcal{H}}}^{\prime}=({{\mathcal{Q}}}_{1}\times{{\mathcal{Q}}}_{2},{{\mathbf{P}}}_{1}\oplus{{\mathbf{P}}}_{2})$
are saturated fdfas that recognize the intersection and union of
${\llbracket{{\mathcal{F}}}_{1}\rrbracket}$ and
${\llbracket{{\mathcal{F}}}_{2}\rrbracket}$, respectively.

Notice that the number of states in ${{\mathcal{H}}}$ and
${{\mathcal{H}}}^{\prime}$ is quadratic in the number of states in
${{\mathcal{F}}}_{1}$ and ${{\mathcal{F}}}_{2}$, yet the algorithm can
generate the representation of ${{\mathcal{H}}}$ and
${{\mathcal{H}}}^{\prime}$ in space logarithmic in the size of
${{\mathcal{F}}}_{1}$ and ${{\mathcal{F}}}_{2}$: It sequentially traverses the
states of ${{\mathcal{Q}}}_{1}$, and for each of its states, it sequentially
traverses the states of ${{\mathcal{Q}}}_{2}$. Thus, it should only store the
currently traversed states in ${{\mathcal{Q}}}_{1}$ and ${{\mathcal{Q}}}_{2}$,
where each of them requires a storage space of size logarithmic in the number
of states in ${{\mathcal{Q}}}_{1}$ and ${{\mathcal{Q}}}_{2}$, respectively.
The same holds for generating the product of ${{\mathbf{P}}}_{1}$ and
${{\mathbf{P}}}_{2}$.

##### Correctness

Consider a pair $(u,v)\in{\Sigma^{*+}}$. Let $(x_{1},y_{1})$ and
$(x_{2},y_{2})$ be its normalization with respect to ${{\mathcal{Q}}}_{1}$ and
${{\mathcal{Q}}}_{2}$, respectively, where $x_{1}={u}{v}^{i_{1}}$,
$y_{1}={v}^{j_{1}}$, $x_{2}={u}{v}^{i_{2}}$, and $y_{2}={v}^{j_{2}}$. Let
$i=\max(i_{1},i_{2})$ and $j$ be the least common multiple of $(j_{1},j_{2})$.
Define $x={u}{v}^{i}$ and $y={v}^{j}$.

Observe that the normalization of $(u,v)$ with respect to
${{\mathcal{Q}}}_{1}\\!\times\\!{{\mathcal{Q}}}_{2}$ is $(x,y)$: i) The
equality
${{\mathcal{Q}}}_{1}\\!\times\\!{{\mathcal{Q}}}_{2}(x)={{\mathcal{Q}}}_{1}\\!\times\\!{{\mathcal{Q}}}_{2}(xy)$
follows from taking $i$ to be bigger than both $i_{1}$ and $i_{2}$, which
guarantees that further concatenations of $v$ will be along a cycle w.r.t.
both $Q_{1}$ and $Q_{2}$, and taking $j$ to be multiple of both $j_{1}$ and
$j_{2}$, which guarantees that both $Q_{1}$ and $Q_{2}$ complete a cycle along
$y$. ii) The minimality of $i$ follows from the fact that it is equal to
either $i_{1}$ or $i_{2}$, as a smaller number will contradict the minimality
of either $i_{1}$ or $i_{2}$, and the minimality of $j$ follows from the fact
that it is the minimal number divided by both $j_{1}$ and $j_{2}$, as a number
not divided by one of them will not allow either $Q_{1}$ or $Q_{2}$ to
complete a cycle.

We have
${{{\mathcal{Q}}}_{1}\\!\times\\!{{\mathcal{Q}}}_{2}}\,(xy)={{{\mathcal{Q}}}_{1}\\!\times\\!{{\mathcal{Q}}}_{2}}\,(x)=({{\mathcal{Q}}}_{1}(x),{{\mathcal{Q}}}_{2}(x))$.
Since $xy^{\omega}=x_{1}y_{1}^{\omega}$ and ${{\mathcal{F}}}_{1}$ is
saturated, we get that $(x,y)\in{\llbracket{{\mathcal{F}}}_{1}\rrbracket}$ iff
$(x_{1},y_{1})\in{\llbracket{{\mathcal{F}}}_{1}\rrbracket}$. Since the pair
$(x,y)$ satisfies the requirements of Lemma 2 w.r.t. $(x_{1},y_{1})$ and
${{\mathcal{Q}}}_{1}$, it follows that $(x,y)$ is a normalization of itself
w.r.t. ${{\mathcal{Q}}}_{1}$. Thus,
$y\in{{\mathcal{P}}}_{{{\mathcal{Q}}}_{1}(x)}$ iff
$y_{1}\in{{\mathcal{P}}}_{{{\mathcal{Q}}}_{1}(x_{1})}$. Analogously,
$y\in{{\mathcal{P}}}_{{{\mathcal{Q}}}_{2}(x)}$ iff
$y_{2}\in{{\mathcal{P}}}_{{{\mathcal{Q}}}_{2}(x_{2})}$.

Hence, $(u,v)\in{\llbracket{{\mathcal{F}}}_{1}\rrbracket}\cap{\llbracket
F_{2}\rrbracket}$ iff $(y_{1}\in{{\mathcal{P}}}_{{{\mathcal{Q}}}_{1}(x_{1})}$
and $y_{2}\in{{\mathcal{P}}}_{{{\mathcal{Q}}}_{2}(x_{2})})$ iff
$y\in{{\mathcal{P}}}_{{{\mathcal{Q}}}_{1}(x)}\otimes{{\mathcal{P}}}_{{{\mathcal{Q}}}_{2}(x)}$
iff $(u,v)\in{{\mathcal{H}}}$. Similarly,
$(u,v)\in{\llbracket{{\mathcal{F}}}_{1}\rrbracket}\cup{\llbracket
F_{2}\rrbracket}$ iff $(y_{1}\in{{\mathcal{P}}}_{{{\mathcal{Q}}}_{1}(x_{1})}$
or $y_{2}\in{{\mathcal{P}}}_{{{\mathcal{Q}}}_{2}(x_{2})})$ iff
$y\in{{\mathcal{P}}}_{{{\mathcal{Q}}}_{1}(x)}\oplus{{\mathcal{P}}}_{{{\mathcal{Q}}}_{2}(x)}$
iff $(u,v)\in{{\mathcal{H}}}^{\prime}$.

The saturation of ${{\mathcal{H}}}$ and ${{\mathcal{H}}}^{\prime}$ directly
follows from the above proof of the languages they recognize: consider two
pairs $(u,v)$ and $(u^{\prime},v^{\prime})$, such that
$uv^{\omega}=u^{\prime}v^{\prime\omega}$. Then, by the saturation of
${{\mathcal{F}}}_{1}$ and ${{\mathcal{F}}}_{2}$, both pairs either belong, or
not, to each of ${\llbracket{{\mathcal{F}}}_{1}\rrbracket}$ and
${\llbracket{{\mathcal{F}}}_{2}\rrbracket}$. Hence, both pairs belong, or not,
to each of
${\llbracket{{\mathcal{H}}}\rrbracket}={\llbracket{{\mathcal{F}}}_{1}\rrbracket}\cap{\llbracket{{\mathcal{F}}}_{2}\rrbracket}$
and
${\llbracket{{\mathcal{H}}}^{\prime}\rrbracket}={\llbracket{{\mathcal{F}}}_{1}\rrbracket}\cup{\llbracket{{\mathcal{F}}}_{2}\rrbracket}$.

#### Decision procedures

All of the basic decision problems can be resolved in nondeterministic
logarithmic space, using the Boolean operations above and corresponding
decision algorithms for dfas.

The first decision question to consider is that of _membership_ : given a pair
$(u,v)$ and an fdfa ${{\mathcal{F}}}=({{\mathcal{Q}}},{{\mathbf{P}}})$, does
${{\mathcal{F}}}$ accept $(u,v)$? The question is answered by normalizing
$(u,v)$ into a pair $(x,y)$ and evaluating the runs of ${{\mathcal{Q}}}$ over
$x$ and of ${{\mathcal{P}}}_{{{\mathcal{Q}}}(x)}$ over $y$. A normalized pair
is determined by traversing along ${{\mathcal{Q}}}$, making up to $|Q|$
repetitions of $v$. Notice that memory wise, $x$ and $y$ only require a
logarithmic amount of space, as they are of the form $x=uv^{i}$ and $y=v^{j}$,
where the representation of $i$ and $j$ is bounded by $\log|Q|$. The overall
logarithmic-space solution follows from the complexity of algorithms for
deterministically traversing along an automaton.

######  Proposition 4.

Given a pair $(u,v)\in{\Sigma^{*+}}$ and an fdfa ${{\mathcal{F}}}$ of size
$(n,k)$, the membership question, of whether
$(u,v)\in{\llbracket{{\mathcal{F}}}\rrbracket}$, can be resolved in
deterministic space of $O(\log n+\log k)$.

The next questions to consider are those of _emptiness_ and _universality_ ,
namely given an fdfa ${{\mathcal{F}}}=({{\mathcal{Q}}},{{\mathbf{P}}})$,
whether ${\llbracket{{\mathcal{F}}}\rrbracket}=\emptyset$, and whether
${\llbracket{{\mathcal{F}}}\rrbracket}={\Sigma^{*+}}$, respectively. Notice
that the universality problem is equivalent to the emptiness problem over the
complement of ${{\mathcal{F}}}$. For nondeterministic automata, the complement
automaton might be exponentially larger than the original one, making the
universality problem much harder than the emptiness problem. Luckily, fdfa
complementation is done in constant space, as is the case with deterministic
automata, making the emptiness and universality problems equally easy.

The emptiness problem for an fdfa $({{\mathcal{Q}}},{{\mathbf{P}}})$ cannot be
resolved by only checking whether there is a nonempty progress automaton in
${{\mathbf{P}}}$, since it might be that the accepted period $v$ is not part
of any normalized pair. Yet, the existence of a prefix-word $x$ and a period-
word $y$, such that ${{\mathcal{Q}}}(x)={{\mathcal{Q}}}(xy)$ and
${{\mathcal{P}}}_{{{\mathcal{Q}}}(x)}$ accepts $y$ is a sufficient and
necessary criterion for the nonemptiness of ${{\mathcal{F}}}$. This can be
tested in NLOGSPACE. Hardness in NLOGSPACE follows by a reduction from graph
reachability [Jon75].

######  Theorem 5.

Emptiness and universality for fdfas are NLOGSPACE-complete.

######  Proof 4.4.

An fdfa ${{\mathcal{F}}}=({{\mathcal{Q}}},{{\mathbf{P}}})$ is not empty iff
there exists a pair $(u,v)\in{\Sigma^{*+}}$, whose normalization is some pair
$(x,y)$, such that ${{\mathcal{P}}}_{{{\mathcal{Q}}}(x)}$ accepts $y$. By
Lemma 2, a normalized pair is a normalization of itself, implying that a
sufficient and necessary criterion for the nonemptiness of ${{\mathcal{F}}}$
is the existence of a pair $(x,y)$, such that
${{\mathcal{Q}}}(x)={{\mathcal{Q}}}(xy)$ and
${{\mathcal{P}}}_{{{\mathcal{Q}}}(x)}$ accepts $y$.

We can nondeterministically find such a pair $(x,y)$ in logarithmic space by
guessing $x$ and $y$ (a single letter at each step), and traversing along
${{\mathcal{Q}}}$ and ${{\mathcal{P}}}_{{{\mathcal{Q}}}(x)}$ [GJ79].

Hardness in NLOGSPACE follows by a reduction from graph reachability [Jon75],
taking an fdfa whose leading automaton has a single state.

As fdfa complementation is done in constant space (Theorem 1), the
universality problem has the same space complexity.

The last decision questions we handle are those of _equality_ and
_containment_ , namely given saturated fdfas ${{\mathcal{F}}}$ and
${{\mathcal{F}}}^{\prime}$, whether
${\llbracket{{\mathcal{F}}}\rrbracket}={\llbracket{{\mathcal{F}}}^{\prime}\rrbracket}$
and whether
${\llbracket{{\mathcal{F}}}\rrbracket}\subseteq{\llbracket{{\mathcal{F}}}^{\prime}\rrbracket}$,
respectively. Equality reduces to containment, as
${\llbracket{{\mathcal{F}}}\rrbracket}={\llbracket{{\mathcal{F}}}^{\prime}\rrbracket}$
iff
${\llbracket{{\mathcal{F}}}\rrbracket}\subseteq{\llbracket{{\mathcal{F}}}^{\prime}\rrbracket}$
and
${\llbracket{{\mathcal{F}}}^{\prime}\rrbracket}\subseteq{\llbracket{{\mathcal{F}}}\rrbracket}$.
Containment can be resolved by intersection, complementation, and emptiness
check, as
${\llbracket{{\mathcal{F}}}\rrbracket}\subseteq{\llbracket{{\mathcal{F}}}^{\prime}\rrbracket}$
iff
${\llbracket{{\mathcal{F}}}\rrbracket}\cap{\llbracket{{\mathcal{F}}}^{\prime}\rrbracket}^{c}=\emptyset$.
Hence, by Theorems 1, 3, and 5, these problems are NLOGSPACE-complete. Note
that NLOGSPACE hardness immediately follows by reduction from the emptiness
problem, which asks whether ${\llbracket{{\mathcal{F}}}\rrbracket}=\emptyset$.
The complexity for _equality_ and _containment_ is easily derived from that of
emptiness, intersection and complementation.

######  Proposition 6.

Equality and containment for saturated fdfas are NLOGSPACE-complete.

#### Saturation check

All of the operations and decision problems above assumed that the given fdfas
are saturated. This is indeed the case when learning fdfas via the algorithm
of [AF14], and when translating $\omega$-automata to fdfas (see Section 5). We
show below that the decision problem of whether an arbitrary fdfa is saturated
is in PSPACE. We leave the question of whether it is PSPACE-complete open.

######  Theorem 7.

The problem of deciding whether a given fdfa is saturated is in PSPACE.

######  Proof 4.5.

Let ${{\mathcal{F}}}=({{\mathcal{Q}}},{{\mathbf{P}}})$ be an fdfa of size
$(n,k)$. We first show that if ${{\mathcal{F}}}$ is unsaturated then there
exist words $u,v^{\prime},v^{\prime\prime}$ such that $|u|\leq n$ and
$|v^{\prime}|,|v^{\prime\prime}|\leq n^{n}k^{2k}$, and non-negative integers
$l,r\leq k$ such that
$(u,(v^{\prime}v^{\prime\prime})^{l})\in{\llbracket{{\mathcal{F}}}\rrbracket}$
while
$(uv^{\prime},(v^{\prime\prime}v^{\prime})^{r})\notin{\llbracket{{\mathcal{F}}}\rrbracket}$.

If ${{\mathcal{F}}}$ is unsaturated then there exists some ultimately periodic
word $w\in\Sigma^{\omega}$ that has two different decompositions to prefix and
periodic words on which ${{\mathcal{F}}}$ provides different answers. Let
${{\mathcal{P}}}$ and ${{\mathcal{P}}}^{\prime}$ be the respective progress
automata, corresponding to some states $q$ and $q^{\prime}$ of
${{\mathcal{Q}}}$. Let the run of ${{\mathcal{Q}}}$ on $w$ be
$q_{0},q_{1},q_{2},\ldots$. Since $w$ is ultimately periodic, there exist
$i,j\in\mathbb{N}$ such that $q_{h+j}=q_{h}$ for all $h>i$. That is,
eventually the run cycles through a certain sequence of states. Then $q$ and
$q^{\prime}$ must be on the cycle where $w$ settles. Let $v^{\prime}$ and
$v^{\prime\prime}$ be the subwords of $w$ that are read on the part of the
shortest such cycle from $q$ to $q^{\prime}$ and from $q^{\prime}$ back to
$q$, respectively. (In case that $q=q^{\prime}$, we let $v^{\prime}=\epsilon$
and $v^{\prime\prime}$ be the whole cycle.) Then the different decompositions
are of the form $(u,(v^{\prime}v^{\prime\prime})^{l})$ and
$(uv^{\prime},(v^{\prime\prime}v^{\prime})^{r})$ where $u$ is a string that
takes $Q$ to $q$. Let $l$ and $r$ be the shortest such, then since
${{\mathcal{P}}}$ and ${{\mathcal{P}}}^{\prime}$ have at most $k$ states, we
can assume $l,r\leq k$. We can also assume $u$ is a shortest such string and
thus $|u|\leq n$.

For a dfa ${\mathcal{A}}=\langle\Sigma,Q,\iota,\delta,F\rangle$ and a word
$v\in\Sigma^{*}$, we use $\chi^{{\mathcal{A}}}_{v}$ to denote the function
from $Q$ to $Q$ defined as $\chi^{{\mathcal{A}}}_{v}(q)=\delta(q,v)$. Note
that given $|Q|=n$ there are at most $n^{n}$ different such functions. Let
${{\mathcal{X}}}=\\{\chi_{v}~{}|~{}\chi_{v}=\langle\chi^{{\mathcal{Q}}}_{v},\chi^{{{\mathcal{P}}}}_{v},\chi^{{{\mathcal{P}}}^{\prime}}_{v}\rangle,\
v\in\Sigma^{*}\\}$. Then ${{\mathcal{X}}}$ is the set of congruence classes of
the relation $v_{1}\approx_{{{\mathcal{X}}}}v_{2}$ iff
$\chi^{{{\mathcal{Q}}}}_{v_{1}}=\chi^{{{\mathcal{Q}}}}_{v_{2}}$,
$\chi^{{{\mathcal{P}}}}_{v_{1}}=\chi^{{{\mathcal{P}}}}_{v_{2}}$, and
$\chi^{{{\mathcal{P}}}^{\prime}}_{v_{1}}=\chi^{{{\mathcal{P}}}^{\prime}}_{v_{2}}$.
We can build an automaton such that each state corresponds to a class in
${{\mathcal{X}}}$, the initial state is $\chi_{\epsilon}$, and the transition
relation is $\delta_{{\mathcal{X}}}(\chi_{w},\sigma)=\chi_{w\sigma}$. The
cardinality of ${{\mathcal{X}}}$ is at most $n^{n}{k}^{2k}$. Thus, every state
has a representative word of length at most $n^{n}{k}^{2k}$ taking the initial
state to that state. Therefore, there exist words
$y^{\prime},y^{\prime\prime}$ such that
$y^{\prime}\approx_{{{\mathcal{X}}}}v^{\prime}$ and
$y^{\prime\prime}\approx_{{{\mathcal{X}}}}v^{\prime\prime}$ and
$|y^{\prime}|,|y^{\prime\prime}|\leq n^{n}{k}^{2k}$. Thus
$u,y^{\prime},y^{\prime\prime}$ and $l,r$ satisfy the promised bounds.

Now, to see that fdfa saturation is in PSPACE note we can construct an
algorithm that guesses integers $l,r\leq k$ and words
$u,v^{\prime},v^{\prime\prime}$ such that $|u|\leq n$ and
$|v^{\prime}|,|v^{\prime\prime}|\leq n^{n}k^{2k}$. It guesses the words letter
by letter and constructs on the way $\chi_{v^{\prime}v^{\prime\prime}}$ and
$\chi_{v^{\prime\prime}v^{\prime}}$. It also constructs along the way the
states $q^{\prime}$ and $q$ such that $q=\delta(u)$ and
$q^{\prime}=\delta(uv^{\prime})$. It then computes the $l$ and $r$ powers of
$\chi_{v^{\prime}v^{\prime\prime}}$ and $\chi_{v^{\prime\prime},v^{\prime}}$,
respectively. Finally, it checks whether one of
$(\chi^{{\mathcal{P}}}_{v^{\prime}v^{\prime\prime}})^{l}(q)$ and
$(\chi^{{{\mathcal{P}}}^{\prime}}_{v^{\prime\prime}v^{\prime}})^{r}(q^{\prime})$
is accepting and the other is not, and if so returns that ${{\mathcal{F}}}$ is
unsaturated. The required space is $O(nk^{2}\log nk^{2})$. This shows that
saturation is in coNPSPACE, and by Savitch’s and Immerman-Szelepcsényi’s
theorems, in PSPACE.

##  5\. Translating To and From $\omega$-Automata

As two $\omega$-regular languages are equivalent iff they agree on the set of
ultimately periodic words [McN66], an $\omega$-regular language can be
characterized by a language of pairs of finite words, and in particular by a
saturated fdfa. We shall write $L\equiv L^{\prime}$ to denote that a language
$L\subseteq{\Sigma^{*+}}$ characterizes an $\omega$-regular language
$L^{\prime}$. Formally:

A language $L\subseteq{\Sigma^{*+}}$ _characterizes_ an $\omega$-regular
language $L^{\prime}\subseteq\Sigma^{\omega}$, denoted by $L\equiv
L^{\prime}$, if for every pair $(u,v)\in L$, we have $uv^{\omega}\in
L^{\prime}$, and for every ultimately periodic word $uv^{\omega}\in
L^{\prime}$, we have $(u,v)\in L$.

The families of dfas defined in [Kla94], as well as the analogous families of
right congruences of [MS97], are known to characterize exactly the set of
$\omega$-regular languages [Kla94, MS97]. This is also the case with our
definition of saturated fdfas.

######  Theorem 8.

Every saturated fdfa characterizes an $\omega$-regular language, and for every
$\omega$-regular language, there is a saturated fdfa characterizing it.

######  Proof 5.1.

The two directions are proved in Theorems 10 and 14, below.

In this section, we analyze the state blowup involved in translating
deterministic and nondeterministic $\omega$-automata into equivalent saturated
fdfas, and vice versa. For nondeterministic automata, we consider the
B$\ddot{\textrm{u}}$chi acceptance condition, since it is the simplest and
most commonly used among all acceptance conditions. For deterministic
automata, we consider the parity acceptance condition since it is the simplest
among all acceptance conditions whose deterministic version is equi-
expressible to the $\omega$-regular languages. We also consider deterministic
B$\ddot{\textrm{u}}$chi and co-B$\ddot{\textrm{u}}$chi, for the simple sub-
classes they recognize.

###  5.1. From $\omega$-Automata to FDFAs

We show that dba, dca, and dpa have polynomial translations to saturated
fdfas, whereas translation of nbas to fdfas may involve an inevitable
exponential blowup.

#### From deterministic $\omega$-automata

The constructions of a saturated fdfa that characterizes a given dba, dca, or
dpa ${{\mathcal{D}}}$ share the same idea: The leading automaton is equivalent
to ${{\mathcal{D}}}$, except for ignoring the acceptance condition, and each
progress automaton consists of several copies of ${{\mathcal{D}}}$, memorizing
the acceptance level of the period-word. For a dba or a dca, two such copies
are enough, memorizing whether or not a B$\ddot{\textrm{u}}$chi
(co-B$\ddot{\textrm{u}}$chi) accepting state was visited. For a dpa with $k$
colors, $k$ such copies are required.

We start with the constructions of an fdfa for a given dba or dca, which are
almost the same. (B$\ddot{\textrm{u}}$chi and co-B$\ddot{\textrm{u}}$chi
automata are special cases of parity automata, and therefore their
translations to an fdfa, as described in Theorem 9, are special cases of the
translation given in Theorem 9. Nevertheless, for clarity reasons, we do give
their explicit translations below.)

######  Theorem 9.

Let ${{\mathcal{D}}}$ be a dba or a dca with $n$ states. There exists a
saturated fdfa ${{\mathcal{F}}}$ of size $(n,2n)$, such that
${\llbracket{{\mathcal{F}}}\rrbracket}\equiv{\llbracket{{\mathcal{D}}}\rrbracket}$.

######  Proof 5.2.

##### Construction

Let ${{\mathcal{D}}}=\langle\Sigma,Q,\iota,\delta,\alpha\rangle$ be a dba or a
dca. We define the fdfa ${{\mathcal{F}}}=({{\mathcal{Q}}},{{\mathbf{P}}})$,
where ${{\mathcal{Q}}}$ is the same as ${{\mathcal{D}}}$ (without acceptance),
and each progress automaton ${{\mathcal{P}}}_{q}$ has two copies of
${{\mathcal{D}}}$, having $(q,0)$ as its initial state, and moving from the
first to the second copy upon visiting a ${{\mathcal{D}}}$-accepting state.
Formally: ${{\mathcal{Q}}}=\langle\Sigma,Q,\iota,\delta\rangle$, and for each
state $q\in Q$, ${{\mathbf{P}}}$ has the dfa
${{\mathcal{P}}}_{q}=\langle\Sigma,Q\\!\times\\!\\{0,1\\},(q,0),\delta^{\prime},F\rangle$,
where for every
$\sigma\in\Sigma,\delta^{\prime}((q,0),\sigma)=(\delta(q,\sigma),0)$ if
$\delta(q,\sigma)\not\in\alpha$ and $(\delta(q,\sigma),1)$ otherwise; and
$\delta^{\prime}((q,1),\sigma)=(\delta(q,\sigma),1)$. The set $F$ of accepting
states is $Q\\!\times\\!\\{1\\}$ if ${{\mathcal{D}}}$ is a dba and
$Q\\!\times\\!\\{0\\}$ if ${{\mathcal{D}}}$ is a dca.

##### Correctness

We show the correctness for the case that ${{\mathcal{D}}}$ is a dba. The case
that ${{\mathcal{D}}}$ is a dca is analogous.

Consider a word $uv^{\omega}\in{\llbracket{{\mathcal{D}}}\rrbracket}$, and let
$(x,y)$ be the normalization of $(u,v)$ w.r.t. ${{\mathcal{Q}}}$. Since
$xy^{\omega}=uv^{\omega}\in{\llbracket{{\mathcal{D}}}\rrbracket}$, it follows
that ${{\mathcal{D}}}$ visits an accepting state when running on $y$ from the
state ${{\mathcal{D}}}(x)$, implying that
${{\mathcal{P}}}_{{{\mathcal{Q}}}(x)}(y)$ is an accepting state. Hence,
$(u,v)\in{\llbracket{{\mathcal{F}}}\rrbracket}$.

As for the other direction, consider a pair
$(u,v)\in{\llbracket{{\mathcal{F}}}\rrbracket}$, and let $(x,y)$ be the
normalization of $(u,v)$ w.r.t. ${{\mathcal{Q}}}$. Since
${{\mathcal{P}}}_{{{\mathcal{Q}}}(x)}(y)$ is an accepting state,
${{\mathcal{D}}}$ has the same structure as ${{\mathcal{Q}}}$, and
${{\mathcal{Q}}}(x)={{\mathcal{Q}}}(xy)$, it follows that ${{\mathcal{D}}}$
visits an accepting state when running on $y$ from the state
${{\mathcal{D}}}(x)$, implying that
$xy^{\omega}=uv^{\omega}\in{\llbracket{{\mathcal{D}}}\rrbracket}$.

Note that ${{\mathcal{F}}}$ is saturated as a direct consequence of the proof
that it characterizes an $\omega$-regular language.

We continue with the construction of an fdfa for a given dpa.

######  Theorem 10.

Let ${{\mathcal{D}}}$ be a dpa with $n$ states and $k$ colors. There exists a
saturated fdfa ${{\mathcal{F}}}$ of size $(n,kn)$, such that
${\llbracket{{\mathcal{F}}}\rrbracket}\equiv{\llbracket{{\mathcal{D}}}\rrbracket}$.

######  Proof 5.3.

##### Construction

Let ${{\mathcal{D}}}=\langle\Sigma,Q,\iota,\delta,\kappa\rangle$ be a dpa,
where $\kappa:Q\rightarrow[1..k]$. We define the fdfa
${{\mathcal{F}}}=({{\mathcal{Q}}},{{\mathbf{P}}})$, where ${{\mathcal{Q}}}$ is
the same as ${{\mathcal{D}}}$ (without acceptance), and each progress
automaton ${{\mathcal{P}}}_{q}$ has $k$ copies of ${{\mathcal{D}}}$, having
$(q,\kappa(q))$ as its initial state, and moving to a $j$-th copy upon
visiting a state with color $j$, provided that $j$ is lower than the index of
the current copy. The accepting states are those of the odd copies.

Formally: ${{\mathcal{Q}}}=\langle\Sigma,Q,\iota,\delta\rangle$, and for each
state $q\in Q$, ${{\mathbf{P}}}$ has the dfa
${{\mathcal{P}}}_{q}=\langle\Sigma,Q~{}\\!\times\\!~{}[1..k],$
$(q,\kappa(q)),\delta^{\prime},F\rangle$, where for every $\sigma\in\Sigma$
and $i\in[1..k]$,

$\delta^{\prime}((q,i),\sigma)=(\delta(q,\sigma),\min(i,\kappa(\delta(q,\sigma)))).$

The set $F$ of accepting states is $\\{Q\\!\times\\!\\{i\\}~{}|~{}i\mbox{ is
odd }\\}$.

##### Correctness

Analogous to the arguments in the proof of Theorem 9.

#### From nondeterministic $\omega$-automata

An nba ${\mathcal{A}}$ can be translated into a saturated fdfa
${{\mathcal{F}}}$, by first determinizing ${\mathcal{A}}$ into an equivalent
dpa ${\mathcal{A}}^{\prime}$ [Pit06, FL15] (which might involve a $2^{O(n\log
n)}$ state blowup and $O(n)$ colors [Sch09b]), and then polynomially
translating ${\mathcal{A}}^{\prime}$ into an equivalent fdfa (Theorem 10).

######  Proposition 11.

Let ${{\mathcal{B}}}$ be an nba with $n$ states. There is a saturated fdfa
that characterizes ${\llbracket{{\mathcal{B}}}\rrbracket}$ with a leading
automaton and progress automata of at most $2^{O(n\log n)}$ states each.

A $2^{O(n\log n)}$ state blowup in this case is inevitable, based on the lower
bound for complementing nbas [Mic88, Yan06, Sch09a], the constant
complementation of fdfas, and the polynomial translation of a saturated fdfa
to an nba:

######  Theorem 12.

There exists a family of nbas
${{\mathcal{B}}}_{1},{{\mathcal{B}}}_{2},\ldots$, such that for every
$n\in\mathbb{N}$, ${{\mathcal{B}}}_{n}$ is of size $n$, while a saturated fdfa
that characterizes ${\llbracket{{\mathcal{B}}}_{n}\rrbracket}$ must be of size
$(m,k)$, such that $\max(m,k)\geq 2^{\Omega(n\log n)}$.

######  Proof 5.4.

Michel [Mic88] has shown that there exists a family of languages
$\\{L_{n}\\}_{n\geq 1}$, such that for every $n$, there exists an nba of size
$n$ for $L_{n}$, but an nba for $L_{n}^{c}$, the complement of $L_{n}$, must
have at least $2^{n\log n}$ states.

Assume, towards a contradiction, that exist $n\in\mathbb{N}$ and a saturated
fdfa ${{\mathcal{F}}}$ of size $(m,k)$ that characterizes $L_{n}$, such that
$\max(m,k)<2^{\Omega(n\log n)}$. Then, by Theorem 1, there is a saturated fdfa
${{\mathcal{F}}}^{c}$ of size $(m,k)$ that characterizes $L_{n}^{c}$. Thus, by
Theorem 14, we have an nba of size smaller than $(2^{\Omega(n\log
n)})^{5}=2^{\Omega(n\log n)}$ for $L_{n}^{c}$. Contradiction.

###  5.2. From FDFAs to $\omega$-automata

We show that saturated fdfas can be polynomially translated into nbas, yet
translations of saturated fdfas to dpas may involve an inevitable exponential
blowup.

#### To nondeterministic $\omega$-automata

We show below that every saturated fdfa can be polynomially translated to an
equivalent nba. Since an nba can be viewed as a special case of an npa, a
translation of saturated fdfas to npas follows. Translating saturated fdfas to
ncas is not always possible, as the latter are not expressive enough.

The translation goes along the lines of the construction given in [CNP93] for
translating an $L_{\$}$-automaton into an equivalent nba. We prove below that
the construction is correct for saturated fdfas, despite the fact that
saturated fdfas can be exponentially smaller than $L_{\$}$-automata.

We start with a lemma from [CNP93], which will serve us for one direction of
the proof.

######  Lemma 13 ([CNP93]).

Let $M,N\subseteq\Sigma^{*}$ such that $M\cdot N^{*}=M$ and $N^{+}=N$. Then
for every ultimately periodic word $w\in\Sigma^{\omega}$ we have that $w\in
M\cdot N^{\omega}$ iff there exist words $u\in M$ and $v\in N$ such that
$uv^{\omega}=w$.

We continue with the translation and its correctness.

######  Theorem 14.

For every saturated fdfa ${{\mathcal{F}}}$ of size $(n,k)$, there exists an
nba ${{\mathcal{B}}}$ with $O(n^{2}k^{3})$ states, such that
${\llbracket{{\mathcal{F}}}\rrbracket}\equiv{\llbracket{{\mathcal{B}}}\rrbracket}$.

######  Proof 5.5.

##### Construction

Consider a saturated fdfa ${{\mathcal{F}}}=({{\mathcal{Q}}},{{\mathbf{P}}})$,
where ${{\mathcal{Q}}}=\langle\Sigma,Q,\iota,\delta\rangle$, and for each
state $q\in Q$, ${{\mathbf{P}}}$ has the progress dfa
${{\mathcal{P}}}_{q}=\langle\Sigma,P_{q},\iota_{q},\delta_{q},F_{q}\rangle$.

For every $q\in Q$, let $M_{q}$ be the language of finite words on which
${{\mathcal{Q}}}$ reaches $q$, namely
$M_{q}=\\{u\in\Sigma^{*}~{}|~{}{{\mathcal{Q}}}(u)=q\\}$. For every $q\in Q$
and for every accepting state $f\in F_{q}$, let $N_{q,f}$ be the language of
finite words on which ${{\mathcal{Q}}}$ makes a self-loop on $q$,
${{\mathcal{P}}}_{q}$ reaches $f$, and ${{\mathcal{P}}}_{q}$ makes a self-loop
on $f$, namely
$N_{q,f}=\\{v\in\Sigma^{*}~{}|~{}(\delta(q,v)=q)\land({{\mathcal{P}}}_{q}(v)=f)\land(\delta_{q}(f,v)=f)\\}$.
We define the $\omega$-regular language

$L=\bigcup_{\\{(q,f)~{}|~{}(q\in Q)\land(f\in F_{q})\\}}M_{q}\cdot
N_{q,f}^{\omega}$ (1)

One can construct an nba ${{\mathcal{B}}}$ that recognizes $L$ and has up to
$O(n^{2}k^{3})$ states: $L$ is the union of $nk$ sublanguages;
${{\mathcal{B}}}$ will have $nk$ corresponding subautomata, and will
nondeterministically start in one of them. In each subautomaton, recognizing
the language $M_{q}\cdot N_{q,f}^{\omega}$, a component of size $n$ for
$M_{q}$ is obtained by a small modification to ${{\mathcal{Q}}}$, in which $q$
can nondeterministically continue with an $\epsilon$-transition555The
$\epsilon$-transitions can be removed from an nba with no state blowup. to a
component realizing $N_{q,f}^{\omega}$. An nba for the language $N_{q,f}$
consists of the intersection of three nbas, for the languages
$\\{v\in\Sigma^{*}~{}|~{}\delta(q,v)=q\\}$,
$\\{v\in\Sigma^{*}~{}|~{}{{\mathcal{P}}}_{q}(v)=f\\}$, and
$\\{v\in\Sigma^{*}~{}|~{}\delta_{q}(f,v)=f\\}$, each of which can be obtained
by small modifications to either ${{\mathcal{Q}}}$ or ${{\mathcal{P}}}_{q}$,
resulting in $nk^{2}$ states. Finally, the automaton for $N_{q,f}^{\omega}$ is
obtained by adding $\epsilon$-transitions in the automaton of $N_{q,f}$ from
its accepting states to its initial state. Thus, each subautomaton is of size
$n+nk^{2}$, and ${{\mathcal{B}}}$ is of size $nk(n+nk^{2})\in O(n^{2}k^{3})$.

##### Correctness

Consider an ultimately periodic word
$uv^{\omega}\in{\llbracket{{\mathcal{B}}}\rrbracket}$. By the construction of
${{\mathcal{B}}}$, $uv^{\omega}\in L$, where $L$ is defined by Equation (1).
Hence, $uv^{\omega}\in M_{q}\cdot N_{q,f}^{\omega}$, for some $q\in Q$ and
$f\in F_{q}$. By the definitions of $M_{q}$ and $N_{q,f}$, we get that $M_{q}$
and $N_{q,f}$ satisfy the hypothesis of Lemma 13, namely $N_{q,f}^{+}=N_{q,f}$
and $M_{q}\cdot N_{q,f}^{*}=M_{q}$. Therefore, by Lemma 13, there exist finite
words $u^{\prime}\in M_{q}$ and $v^{\prime}\in N_{q,f}$ such that
$u^{\prime}v^{\prime\omega}=uv^{\omega}$. From the definitions of $M_{q}$ and
$N_{q,f}$, it follows that the run of ${{\mathcal{Q}}}$ on $u^{\prime}$ ends
in the state $q$, and ${{\mathcal{P}}}_{q}$ accepts $v^{\prime}$. Furthermore,
by the definition of $N_{q,f}$, we have $\delta(q,v^{\prime})=q$, implying
that $(u^{\prime},v^{\prime})$ is the normalization of itself. Hence,
$(u^{\prime},v^{\prime})\in{\llbracket{{\mathcal{F}}}\rrbracket}$. Since
${{\mathcal{F}}}$ is saturated and $u^{\prime}v^{\prime\omega}=uv^{\omega}$,
it follows that $(u,v)\in{\llbracket{{\mathcal{F}}}\rrbracket}$, as required.

As for the other direction, consider a pair
$(u,v)\in{\llbracket{{\mathcal{F}}}\rrbracket}$, and let $(x,y)$ be the
normalization of $(u,v)$ w.r.t. ${{\mathcal{Q}}}$. We will show that
$xy^{\omega}\in L$, where $L$ is defined by Equation (1), implying that
$uv^{\omega}\in{\llbracket{{\mathcal{B}}}\rrbracket}$. Let
$q={{\mathcal{Q}}}(x)$, so we have that ${{\mathcal{P}}}_{q}(y)$ reaches some
accepting state $f$ of ${{\mathcal{P}}}_{q}$. Note, however, that it still
does not guarantee that $y\in N_{q,f}$, since it might be that
$\delta_{q}(f,y)\neq f$.

To prove that $xy^{\omega}\in L$, we will show that there is a pair
$(x,y^{\prime})\in{\Sigma^{*+}}$ and an accepting state
$f^{\prime}\in{{\mathcal{P}}}_{q}$, such that $y^{\prime}=y^{t}$ for some
positive integer $t$, and $y^{\prime}\in N_{q,f^{\prime}}$; namely
$\delta(q,y^{\prime})=q$, ${{\mathcal{P}}}_{q}(y^{\prime})=f^{\prime}$, and
$\delta_{q}(f^{\prime},y^{\prime})=f^{\prime}$. Note first that since
${{\mathcal{F}}}$ is saturated, it follows that for every positive integer
$i$, $(x,y^{i})\in{\llbracket{{\mathcal{F}}}\rrbracket}$, as
$x(y^{i})^{\omega}=xy^{\omega}$.

Now, for every positive integer $i$, ${{\mathcal{P}}}_{q}$ reaches some
accepting state $f_{i}$ when running on $y^{i}$. Since ${{\mathcal{P}}}_{q}$
has finitely many states, for a large enough $i$, ${{\mathcal{P}}}_{q}$ must
reach the same accepting state $\hat{f}$ twice when running on $y^{i}$. Let
$h$ be the smallest positive integer such that
${{\mathcal{P}}}_{q}(y^{h})=\hat{f}$, and $r$ the smallest positive integer
such that $\delta_{q}(\hat{f},y^{r})=\hat{f}$. Now, one can verify that
choosing $t$ to be an integer that is bigger than or equal to $h$ and is
divisible by $r$ guarantees that $\delta(q,y^{t})=q$ and
$\delta_{q}(f^{\prime},y^{t})=f^{\prime}$, where
$f^{\prime}={{\mathcal{P}}}_{q}(y^{t})$.

#### To deterministic $\omega$-automata

Deterministic B$\ddot{\textrm{u}}$chi and co-B$\ddot{\textrm{u}}$chi automata
are not expressive enough for recognizing every $\omega$-regular language. We
thus consider the translation of saturated fdfas to deterministic parity
automata. A translation is possible by first polynomially translating the fdfa
into an nba (Theorem 14) and then determinizing the latter into a dpa (which
might involve a $2^{O(n\log n)}$ state blowup [Mic88]).

######  Proposition 15.

Let ${{\mathcal{F}}}$ be a saturated fdfa of size $(n,k)$. There exists a dpa
${{\mathcal{D}}}$ of size $2^{O(n^{2}k^{3}\log n^{2}k^{3})}$, such that
$\textbullet{\llbracket{{\mathcal{F}}}\rrbracket}\equiv{\llbracket{{\mathcal{D}}}\rrbracket}$.

We show below that an exponential state blowup is inevitable.666This is also
the case when translating fdfas to deterministic Rabin [Rab69] and Streett
[Str82] automata, as explained in Remark 19. The family of languages
$\\{L_{n}\\}_{n\geq 1}$ below demonstrates the inherent gap between fdfas and
dpas; an fdfa for $L_{n}$ may only “remember” the smallest and biggest read
numbers among $\\{1,2,...,n\\}$, using $n^{2}$ states, while a dpa for it must
have at least $2^{n-1}$ states.

We define the family of languages $\\{L_{n}\\}_{n\geq 1}$ as follows. The
alphabet of $L_{n}$ is $\\{1,2,...,n\\}$, and a word belongs to it iff the
following two conditions are met:

  * •

A letter $i$ is always followed by a letter $j$, such that $j\leq i+1$. For
example, $533245\ldots$ is a bad prefix, since 2 was followed by 4, while
$55234122\ldots$ is a good prefix.

  * •

The number of letters that appear infinitely often is odd. For example,
$2331(22343233)^{\omega}$ is in $L_{n}$, while $1(233)^{\omega}$ is not.

We show below how to construct, for every $n\geq 1$, a saturated fdfa of size
polynomial in $n$ that characterizes $L_{n}$. Intuitively, the leading
automaton handles the safety condition of $L_{n}$, having $n+1$ states, and
ensuring that a letter $i$ is always followed by a letter $j$, such that
$j\leq i+1$. The progress automata, which are identical, maintain the smallest
and biggest number-letters that appeared, denoted by $s$ and $b$,
respectively. Since a number-letter $i$ cannot be followed by a number-letter
$j$, such that $j>i+1$, it follows that the total number of letters that
appeared is equal to $b-s+1$. Then, a state is accepting iff $b-s+1$ is odd.

######  Lemma 16.

Let $n\geq 1$. There is a saturated fdfa of size $(n+1,n^{2})$ characterizing
$L_{n}$.

######  Proof 5.6.

We formally define an fdfa ${{\mathcal{F}}}=({{\mathcal{Q}}},{{\mathbf{P}}})$
for $L_{n}$ over $\Sigma=\\{1,2,\ldots,n\\}$, as follows.

The leading automaton is ${{\mathcal{Q}}}=(\Sigma,Q,\iota,\delta)$, where
$Q=\\{\bot,q_{1},q_{2},\ldots,q_{n}\\}$; $\iota=q_{n}$; and for every
$i,j\in[1..n],\delta(q_{i},j)=q_{j}$ if $j\leq i+1$, and $\bot$ otherwise, and
$\delta(\bot,j)=\bot$.

The progress automaton for the state $\bot$ consists of a single non-accepting
state with a self-loop over all letters.

For every $i\in[1..n]$, the progress automaton for $q_{i}$ is
${{\mathcal{P}}}_{i}=(\Sigma,P_{i},\iota_{i},\delta_{i},F_{i})$, where:

  * •

$P_{i}=[1..n]\times[1..n]$

  * •

$\iota_{i}=(n,1)$

  * •

$\delta_{i}$: For every $\sigma\in\Sigma$ and
$s,b\in[1..n],\delta_{i}((s,b),\sigma)=(\min(s,\sigma),\max(b,\sigma))$.

  * •

$F_{i}=\\{(s,b)~{}|~{}b-s\mbox{ is even }\\}$

Notice that the progress automaton need not handle the safety requirement, as
the leading automaton ensures it, due to the normalization in the acceptance
criterion of an fdfa.

A dpa for $L_{n}$ cannot just remember the smallest and largest letters that
were read, as these letters might not appear infinitely often. Furthermore, we
prove below that the dpa must be of size exponential in $n$, by showing that
its state space must be doubled when moving from $L_{n}$ to $L_{n+1}$.

######  Lemma 17.

Every dpa that recognizes $L_{n}$ must have at least $2^{n-1}$ states.

######  Proof 5.7.

The basic idea behind the proof is that the dpa cannot mix between 2 cycles of
$n$ different letters each. This is because a mixed cycle in a parity
automaton is accepting/rejecting if its two sub-cycles are, while according to
the definition of $L_{n}$, a mixed cycle might reject even though both of its
sub-cycles accept, and vice versa. Hence, whenever adding a letter, the state
space must be doubled.

In the formal proof below, we dub a reachable state from which the automaton
can accept some word a _live state_ , and for every
$n\in\mathbb{N}\setminus\\{0\\}$, define the alphabet
$\Sigma_{n}=\\{1,2,\ldots,n\\}$. Consider a dpa ${{\mathcal{D}}}_{n}$ over
$\Sigma_{n}$ that recognizes $L_{n}$, and let $q$ be some live state of
${{\mathcal{D}}}_{n}$. Observe that
${\llbracket{{\mathcal{D}}}_{n}^{q}\rrbracket}$, namely the language of the
automaton that we get from ${{\mathcal{D}}}_{n}$ by changing the initial state
to $q$, is the same as $L_{n}$ except for having some restriction on the word
prefixes. More formally, for every $n\in\mathbb{N}$ and $u\in\Sigma_{n}^{*}$,
we define the language $L_{n,u}=\\{w~{}|~{}uw\in L_{n}\\}$, and let
$\mathfrak{L}_{n}$ denote the set of languages
$\\{L_{n,u}\neq\emptyset~{}|~{}u\in\Sigma_{n}^{*}\\}$. Given some $L_{n,u}$,
since $L_{n,u}\neq\emptyset$, there is a live state $q$ that
${{\mathcal{D}}}_{n}$ reaches when reading $u$, and we have
$L_{n,u}={\llbracket{{\mathcal{D}}}_{n}^{q}\rrbracket}$. Conversely, given a
dpa $D_{n}$ for $L_{n}$ and a live state $q$ of ${{\mathcal{D}}}_{n}$, let $u$
be a finite word on which ${{\mathcal{D}}}_{n}$ reaches $q$, then
${\llbracket{{\mathcal{D}}}_{n}^{q}\rrbracket}=L_{n,u}$.

We prove by induction on $n$ the following claim, from which the statement of
the lemma immediately follows: Let ${{\mathcal{D}}}_{n}$ be a dpa over
$\Sigma_{n}$ that recognizes some language in $\mathfrak{L}_{n}$. Then there
are finite words $u,v\in\Sigma_{n}^{*}$, such that:

  1. i)

$v$ contains all the letters in $\Sigma_{n}$;

  2. ii)

the run of ${{\mathcal{D}}}_{n}$ on $u$ reaches some live state $p$; and

  3. iii)

the run of ${{\mathcal{D}}}_{n}$ on $v$ from $p$ returns to $p$, while
visiting at least $2^{n-1}$ different states.

The base cases, for $n\in\\{1,2\\}$, are simple, as they mean a cycle of size
at least $1$ over $v$, for $n=1$, and at least $2$ for $n=2$. Formally, for
$n=1$, $L_{1}=\\{1^{\omega}\\}$ and $\mathfrak{L}_{1}=\\{L_{1}\\}$. A dpa
${{\mathcal{D}}}_{1}$ for $L_{1}$ must have a live state $p$ that is visited
infinitely often when ${{\mathcal{D}}}_{1}$ reads $1^{\omega}$. Thus, there is
a cycle from $p$ back to $p$ along a word $v$ of length at least 1, containing
the letter ‘1’. For $n=2$, it is still the case that the restriction on the
next letter (to be up to 1-bigger than the current letter) does not influence.
Hence,
$L_{2}=\\{u1^{\omega}~{}|~{}u\in\Sigma_{2}^{*}\\}\cup\\{u2^{\omega}~{}|~{}u\in\Sigma_{2}^{*}\\}$
and $\mathfrak{L}_{2}=\\{L_{2}\\}$. Consider a dpa ${{\mathcal{D}}}_{2}$ for
$L_{2}$, having $k$ states. The run of ${{\mathcal{D}}}_{2}$ over the finite
word $(12)^{k}$ must reach some live state $p$ twice. Thus, there is a cycle
from $p$ back to itself along a word $v$ that contains both ‘1’ and ‘2’.
Observe that $v$ must be of length at least 2, as otherwise there are only
self loops from $p$, implying that ${{\mathcal{D}}}_{2}^{p}$ either accepts or
rejects all words, in contradiction to the definition of
${{\mathcal{D}}}_{2}$.

In the induction step, we consider a dpa ${{\mathcal{D}}}_{n+1}$, for $n\geq
2$, that recognizes some language $L\in\mathfrak{L}_{n+1}$. We shall define
${{\mathcal{D}}}^{\prime}$ and ${{\mathcal{D}}}^{\prime\prime}$ to be the dpas
that result from ${{\mathcal{D}}}_{n+1}$ by removing all the transitions over
the letter $n\mathord{+}1$ and by removing all the transitions over the letter
$1$, respectively.

Observe that for every state $q$ that is live w.r.t. ${{\mathcal{D}}}_{n+1}$,
we have that ${\llbracket{{\mathcal{D}}}^{\prime
q}\rrbracket}\in\mathfrak{L}_{n}$, namely the language of the dpa that results
from ${{\mathcal{D}}}_{n+1}$ by removing all the transitions over the letter
$n\mathord{+}1$ and setting the initial state to $q$ is in $\mathfrak{L}_{n}$.
This is the case since even if $q$ is only reachable via the letter
$n\mathord{+}1$, it must have outgoing transitions over letters in $[2..n]$.
Analogously, ${\llbracket{{\mathcal{D}}}^{\prime\prime q}\rrbracket}$ is
isomorphic to a language in $\mathfrak{L}_{n}$ via the alphabet mapping of
$i\mapsto(i-1)$. Hence, for every state $q$ that is live w.r.t.
${{\mathcal{D}}}_{n+1}$, the induction hypothesis holds for
${{\mathcal{D}}}^{\prime q}$ and ${{\mathcal{D}}}^{\prime\prime q}$.

We shall prove the induction claim by describing words
$u,v\in\Sigma_{n+1}^{*}$, and showing that they satisfy the requirements above
w.r.t. ${{\mathcal{D}}}_{n+1}$. We iteratively construct words
$u^{\prime}_{i},u^{\prime\prime}_{i},v^{\prime}_{i},v^{\prime\prime}_{i}$
until, roughly speaking, the run of ${{\mathcal{D}}}_{n+1}$ on the
concatenation of these words closes a loop. More precisely, upon the first
iteration $k$ for which there exists $j<k$ such that
${{\mathcal{D}}}_{n+1}(u^{\prime}_{1}u^{\prime\prime}_{1}u^{\prime}_{2}u^{\prime\prime}_{2}\ldots
u^{\prime}_{j}u^{\prime\prime}_{j})={{\mathcal{D}}}_{n+1}(u^{\prime}_{1}\,u^{\prime\prime}_{1}\,u^{\prime}_{2}\,u^{\prime\prime}_{2}\ldots
u^{\prime}_{k}\,u^{\prime\prime}_{k})$, we stop the iteration and define $u$
to be the word
$u^{\prime}_{1}u^{\prime\prime}_{1}u^{\prime}_{2}u^{\prime\prime}_{2}\ldots
u^{\prime}_{j}u^{\prime\prime}_{j}$ and $v$ to be the word
$u^{\prime}_{j+1}\,v^{\prime}_{j+1}\,u^{\prime\prime}_{j+1}\,v^{\prime\prime}_{j+1}\ldots
u^{\prime}_{k}\,v^{\prime}_{k}\,u^{\prime\prime}_{k}\,v^{\prime\prime}_{k}$.

For the first iteration, we define:

  * •

$u^{\prime}_{1}$ and $v^{\prime}_{1}$ are the words that follow from the
induction hypothesis on ${{\mathcal{D}}}^{\prime q_{1}}$, where $q_{1}$ is the
initial state of ${{\mathcal{D}}}_{n+1}$.

  * •

$u^{\prime\prime}_{1}$ and $v^{\prime\prime}_{1}$ are the words that follow
from the induction hypothesis on ${{\mathcal{D}}}^{\prime\prime
q^{\prime}_{1}}$, where $q^{\prime}_{1}$ is the state that
${{\mathcal{D}}}_{n+1}$ reaches when reading $u^{\prime}_{1}$.

For the next iterations, we define for every $i>1$:

  * •

$u^{\prime}_{i}$ and $v^{\prime}_{i}$ are the words that follow from the
induction hypothesis on ${{\mathcal{D}}}^{\prime q_{i}}$, where $q_{i}$ is the
state that ${{\mathcal{D}}}_{n+1}$ reaches when reading
$u^{\prime}_{1}\,u^{\prime\prime}_{1}\,\ldots
u^{\prime}_{i-1}\,u^{\prime\prime}_{i-1}$. (The state $q_{i}$ indeed belongs
to ${{\mathcal{D}}}^{\prime q_{i}}$, since it has outgoing transitions on some
letters in $[1..n]$.)

  * •

$u^{\prime\prime}_{i}$ and $v^{\prime\prime}_{i}$ are the words that follow
from the induction hypothesis on ${{\mathcal{D}}}^{\prime\prime
q^{\prime}_{i}}$, where $q^{\prime}_{i}$ is the state that
${{\mathcal{D}}}_{n+1}$ reaches when reading
$u^{\prime}_{1}\,u^{\prime\prime}_{1}\,\ldots
u^{\prime}_{i-1}\,u^{\prime\prime}_{i-1}\,u^{\prime}_{i}$. (The state
$q^{\prime}_{i}$ indeed belongs to ${{\mathcal{D}}}^{\prime\prime q_{i}}$,
since it has outgoing transitions on some letters in $[2..n\mathord{+}1]$.)

Note that, for all $i$, by the induction hypothesis $v^{\prime}_{i}$ contains
all letters of $\Sigma_{n}$ and $v^{\prime\prime}_{i}$ contains all the
letters in $\Sigma_{n+1}\setminus\\{1\\}$. Since $v$ is composed of
$v^{\prime}_{i}$’s and $v^{\prime\prime}_{i}$’s it follows that $v$ contains
all the letters in $\Sigma_{n+1}$. By the definition of $u$ and $v$, we also
have that the run of ${{\mathcal{D}}}_{n+1}$ on $u$ reaches some live state
$p$, and the run of ${{\mathcal{D}}}_{n+1}$ on $v$ from $p$ returns to $p$.
Moreover, for every prefix $v_{1}$ of $v$ that reaches a state $s$, we have
that $s$ is a live state, and for $v_{2}$ such that $v=v_{1}v_{2}$, the run of
${{\mathcal{D}}}_{n+1}$ on $v_{2}v_{1}$ returns to $s$. Now, we need to prove
that the run of ${{\mathcal{D}}}_{n+1}$ on $v$ from $p$ visits at least
$2^{n}$ states.

$v^{\prime}$$v^{\prime\prime}$$l^{\prime}$$r^{\prime}$$l^{\prime\prime}$$r^{\prime\prime}$$u$$v$$x$$y$

Figure 2. Subwords of $v$.

Let $v^{\prime}$ be some $v^{\prime}_{i}$ subword of $v$ and likewise let
$v^{\prime\prime}$ be some $v^{\prime\prime}_{j}$ subword of $v$. We claim
that the run of ${{\mathcal{D}}}_{n+1}$ on $uv^{\omega}$ traverses disjoint
sets of states while reading the subwords $v^{\prime}$ and $v^{\prime\prime}$.
This will provide the required result, since when traversing either
$v^{\prime}$ or $v^{\prime\prime}$ we know that ${{\mathcal{D}}}_{n+1}$ visits
at least $2^{n-1}$ different states, by the induction hypothesis.

Assume, by way of contradiction, a state $s$ that is visited by
${{\mathcal{D}}}_{n+1}$ when traversing both $v^{\prime}$ and
$v^{\prime\prime}$. Let $l^{\prime}$ and $r^{\prime}$ be the parts of
$v^{\prime}$ that ${{\mathcal{D}}}_{n+1}$ reads before and after reaching $s$,
respectively, and $l^{\prime\prime}$ and $r^{\prime\prime}$ the analogous
parts of $v^{\prime\prime}$, as shown in Fig. 2. Let $x$ be the subword of
$uv^{\omega}$ between $u$ and $r^{\prime}$ and let $y$ be the subword of
$uv^{\omega}$ between $u$ and $r^{\prime\prime}$. Now, define the
$\omega$-words $m^{\prime}=ux(r^{\prime}\,l^{\prime})^{\omega}$,
$m^{\prime\prime}=uy\,(r^{\prime\prime}\,l^{\prime\prime})^{\omega}$, and
$m=uy\,(r^{\prime\prime}\,l^{\prime\prime}\,r^{\prime}\,l^{\prime})^{\omega}$.

Observe that $m^{\prime}$ and $m^{\prime\prime}$ both belong or both do not
belong to $L$, since there is the same number of letters ($n$) that appear
infinitely often in each of them. The word $m$, on the other hand, belongs to
$L$ if $m^{\prime}$ and $m^{\prime\prime}$ do not belong to $L$, and vice
versa, since $n+1$ letters appear infinitely often in it. However, the set of
states that are visited infinitely often in the run of ${{\mathcal{D}}}_{n+1}$
on $m$ is the union of the sets of states that appear infinitely often in the
runs of ${{\mathcal{D}}}_{n+1}$ on $m^{\prime}$ and $m^{\prime\prime}$. Thus,
if ${{\mathcal{D}}}_{n+1}$ accepts both $m^{\prime}$ and $m^{\prime\prime}$ it
also accepts $m$, and if it rejects both $m^{\prime}$ and $m^{\prime\prime}$
it rejects $m$. (This follows from the fact that the minimal number in a union
of two sets is even/odd iff the minimum within both sets is even/odd.)
Contradiction.

######  Theorem 18.

There is a family of languages $\\{L_{n}\\}_{n\geq 1}$ over the alphabet
$\\{1,2,\ldots,n\\}$, such that for every $n\geq 1$, there is a saturated fdfa
of size $(n+1,n^{2})$ that characterizes $L_{n}$, while a dpa for $L_{n}$ must
be of size at least $2^{n-1}$.

######  Proof 5.8.

By Lemmas 16 and 17.

######  Remark 19.

A small adaptation to the proof of Lemma 17 shows an inevitable exponential
state blowup also when translating a saturated fdfa to a deterministic
$\omega$-automaton with a stronger acceptance condition of Rabin [Rab69] or
Streett [Str82]: A mixed cycle in a Rabin automaton is rejecting if its two
sub-cycles are, and a mixed cycle in a Streett automaton is accepting if its
two sub-cycles are. Hence, the proof of Lemma 17 holds for both Rabin and
Streett automata if proceeding in the induction step from an alphabet of size
$n$ to an alphabet of size $n+2$, yielding a Rabin/Streett automaton of size
at least $2^{\frac{n}{2}}$.

As for translating a saturated fdfa to a deterministic Muller automaton
[Mul63], it is known that translating a dpa of size $n$ into a deterministic
Muller automaton might require the latter to have an accepting set of size
exponential in $n$ [Saf89, Bok17]. Hence, by Theorem 10, which shows a
polynomial translation of dpas to fdfas, we get that translating an fdfa to a
deterministic Muller automaton entails an accepting set of exponential size,
in the worst case.

##  6\. Discussion

The interest in fdfas as a representation for $\omega$-regular languages stems
from the fact that they possess a correlation between the automaton states and
the language right congruences, a property that traditional $\omega$-automata
lack. This property is beneficial in the context of learning, and indeed
algorithms for learning $\omega$-regular languages by means of saturated fdfas
were recently provided [AF14, LCZL16]. Analyzing the succinctness of saturated
fdfas and the complexity of their Boolean operations and decision problems, we
believe that they provide an interesting formalism for representing
$\omega$-regular languages. Indeed, Boolean operations and decision problems
can be performed in nondeterministic logarithmic space and their succinctness
lies between deterministic and nondeterministic $\omega$-automata.

## References

  * [ABF16] D. Angluin, U. Boker, and D. Fisman.  Families of DFAs as acceptors of $\omega$-regular languages.  In 41st International Symposium on Mathematical Foundations of Computer Science, MFCS 2016, August 22-26, 2016 - Kraków, Poland, pages 11:1–11:14, 2016.
  * [AF14] D. Angluin and D. Fisman.  Learning regular omega languages.  In Peter Auer, Alexander Clark, Thomas Zeugmann, and Sandra Zilles, editors, Algorithmic Learning Theory - 25th International Conference, ALT 2014, Bled, Slovenia, October 8-10, 2014. Proceedings, volume 8776 of Lecture Notes in Computer Science, pages 125–139. Springer, 2014.
  * [AvMN05] Rajeev Alur, Pavol Černý, P. Madhusudan, and Wonhong Nam.  Synthesis of interface specifications for Java classes.  In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’05, pages 98–109, New York, NY, USA, 2005. ACM.
  * [BHS+16] F. Blahoudek, M. Heizmann, S. Schewe, J. Strejcek, and M.H. Tsai.  Complementing semi-deterministic Büchi automata.  In Proc. of Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 9636 of LNCS, pages 770–787. Springer, 2016.
  * [Bok17] U. Boker.  On the (in)succinctness of Muller automata.  In CSL, pages 12:1–12:16, 2017.
  * [Büc60] J.R. Büchi.  Weak second-order arithmetic and finite automata.  Zeit. Math. Logik und Grundl. Math., 6:66–92, 1960.
  * [CCF+10] Yu-Fang Chen, Edmund M. Clarke, Azadeh Farzan, Ming-Hsien Tsai, Yih-Kuen Tsay, and Bow-Yaw Wang.  Automated assume-guarantee reasoning through implicit learning.  In Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings, pages 511–526, 2010\.
  * [CCK+15] M. Chapman, H. Chockler, P. Kesseli, D. Kroening, O. Strichman, and M. Tautschnig.  Learning the language of error.  In 13th Int. Symp. on Automated Technology for Verification and Analysis, pages 114–130, 2015.
  * [CNP93] H. Calbrix, M. Nivat, and A. Podelski.  Ultimately periodic words of rational w-languages.  In Proceedings of the 9th International Conference on Mathematical Foundations of Programming Semantics, pages 554–566, London, UK, 1993. Springer-Verlag.
  * [CPPdR14] Georg Chalupar, Stefan Peherstorfer, Erik Poll, and Joeri de Ruiter.  Automated reverse engineering using lego®.  In 8th USENIX Workshop on Offensive Technologies (WOOT 14), San Diego, CA, August 2014. USENIX Association.
  * [FCTW08] A. Farzan, Y. Chenand E.M. Clarke, Y. Tsay, and B. Wang.  Extending automated compositional verification to the full class of omega-regular languages.  In C.R. Ramakrishnan and Jakob Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 4963 of Lecture Notes in Computer Science, pages 2–17. Springer Berlin Heidelberg, 2008\.
  * [FJV14] Paul Fiterau-Brostean, Ramon Janssen, and Frits W. Vaandrager.  Learning fragments of the TCP network protocol.  In FMICS, volume 8718 of Lecture Notes in Computer Science, pages 78–93. Springer, 2014.
  * [FKP11] Lu Feng, Marta Z. Kwiatkowska, and David Parker.  Automated learning of probabilistic assumptions for compositional reasoning.  In Fundamental Approaches to Software Engineering - 14th International Conference, FASE 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings, pages 2–17, 2011.
  * [FL15] D. Fisman and Y. Lustig.  A modular approach for Büchi determinization.  In Luca Aceto and David de Frutos-Escrig, editors, 26th International Conference on Concurrency Theory, CONCUR 2015, Madrid, Spain, September 1.4, 2015, volume 42 of LIPIcs, pages 368–382. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015.
  * [GJ79] M. Garey and D.S. Johnson.  Computers and Intractability: A Guide to the Theory of NP-completeness.  MIT Press, 1979.
  * [Jon75] N.D. Jones.  Space-bounded reducibility among combinatorial problems.  Journal of Computer and System Sciences, 1975.
  * [Kla94] N. Klarlund.  A homomorphism concept for omega-regularity.  In L. Pacholski and J. Tiuryn, editors, Computer Science Logic, 8th International Workshop, CSL ’94, Kazimierz, Poland, September 25-30, 1994, Selected Papers, volume 933 of Lecture Notes in Computer Science, pages 471–485. Springer, 1994.
  * [LCZL16] Yong Li, Yu-Fang Chen, Lijun Zhang, and Depeng Liu.  A novel learning algorithm for Büchi automata based on family of DFAs and classification trees.  arXiv preprint arXiv:1610.07380, 2016.
  * [McN66] R. McNaughton.  Testing and generating infinite sequences by a finite automaton.  Information and Control, 9(5):521–530, 1966.
  * [Mic88] M. Michel.  Complementation is much more difficult with automata on infinite words.  In Manuscript, CNET, 1988.
  * [MS97] O. Maler and L. Staiger.  On syntactic congruences for omega-languages.  Theor. Comput. Sci., 183(1):93–112, 1997.
  * [Mul63] D.E. Muller.  Infinite sequences and finite machines.  In Proc. 4th IEEE Symp. on Switching Circuit Theory and Logical design, pages 3–16, 1963.
  * [Ner58] A. Nerode.  Linear automaton transformations.  Proc. of the American Mathematical Society, 9(4):541–544, 1858\.
  * [NJ13] D. Neider and N. Jansen.  Regular model checking using solver technologies and automata learning.  In NASA Formal Methods, 5th International Symposium, NFM 2013, Moffett Field, CA, USA, May 14-16, 2013. Proceedings, pages 16–31, 2013\.
  * [PGB+08] Corina S. Pasareanu, Dimitra Giannakopoulou, Mihaela Gheorghiu Bobaru, Jamieson M. Cobleigh, and Howard Barringer.  Learning to divide and conquer: applying the l* algorithm to automate assume-guarantee reasoning.  Formal Methods in System Design, 32(3):175–205, 2008.
  * [Pit06] N. Piterman.  From nondeterministic B$\ddot{\textrm{u}}$chi and Streett automata to deterministic parity automata.  In 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, WA, USA, Proceedings, pages 255–264. IEEE Computer Society, 2006.
  * [PVY02] D. Peled, M. Vardi, and M. Yannakakis.  Black box checking.  Journal of Automata, Languages and Combinatorics, 7(2):225–246, 2002.
  * [Rab69] M.O. Rabin.  Decidability of second order theories and automata on infinite trees.  Transaction of the AMS, 141:1–35, 1969.
  * [RMSM09] Harald Raffelt, Maik Merten, Bernhard Steffen, and Tiziana Margaria.  Dynamic testing via automata learning.  STTT, 11(4):307–324, 2009.
  * [Saë90] B. L. Saëc.  Saturating right congruences.  ITA, 24:545–560, 1990.
  * [Saf89] S. Safra.  Complexity of automata on infinite objects.  PhD thesis, Weizmann Institute of Science, 1989.
  * [Sch09a] S. Schewe.  Büchi complementation made tight.  In Proc. 26th Symp. on Theoretical Aspects of Computer Science (STACS), volume 3 of LIPIcs, pages 661–672, 2009.
  * [Sch09b] S. Schewe.  Tighter bounds for the determinization of Büchi automata.  In Proc. 12th Int. Conf. on Foundations of Software Science and Computation Structures (FoSSaCS), pages 167–181, 2009.
  * [Str82] R.S. Streett.  Propositional dynamic logic of looping and converse.  Information and Control, 54:121–141, 1982.
  * [VSVA05] Abhay Vardhan, Koushik Sen, Mahesh Viswanathan, and Gul Agha.  Using language inference to verify omega-regular properties.  In Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, TACAS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings, pages 45–60, 2005.
  * [VW86] M. Y. Vardi and P. Wolper.  An automata-theoretic approach to automatic program verification (preliminary report).  In LICS, pages 332–344. IEEE Computer Society, 1986.
  * [Wil91] T. Wilke.  An Eilenberg theorem for $\infty$-languages, pages 588–599.  Springer Berlin Heidelberg, Berlin, Heidelberg, 1991.
  * [Wil93] T. Wilke.  An algebraic theory for regular languages of finite and infinite words.  IJAC, 3(4):447–490, 1993.
  * [WN05] Westley Weimer and George C. Necula.  Mining temporal specifications for error detection.  In Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, TACAS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings, pages 461–476, 2005.
  * [YAL14] Yifei Yuan, Rajeev Alur, and Boon Thau Loo.  Netegg: Programming network policies by examples.  In Proceedings of the 13th ACM Workshop on Hot Topics in Networks, HotNets-XIII, Los Angeles, CA, USA, October 27-28, 2014, pages 20:1–20:7, 2014.
  * [Yan06] Q. Yan.  Lower bounds for complementation of $\omega$-automata via the full automata technique.  In Proc. 33rd Int. Colloq. on Automata, Languages, and Programming (ICALP), volume 4052 of LNCS, pages 589–600, 2006.