11institutetext: School of Computer Science and Engineering,
The Hebrew University, Jerusalem, Israel.
11email<EMAIL_ADDRESS>11email<EMAIL_ADDRESS>22institutetext: Technische Universität München, Munich, Germany.
22email<EMAIL_ADDRESS>
# Certifying Inexpressibility††thanks: This is the full version of an article
with the same title that appears in the FoSSaCS 2021 conference proceedings.
Orna Kupferman is supported in part by the Israel Science Foundation, grant
No. 2357/19. Salomon Sickert is supported in part by the Deutsche
Forschungsgemeinschaft (DFG) under project numbers 436811179 and 317422601
(“Verified Model Checkers”), and in part funded by the European Research
Council (ERC) under the European Union’s Horizon 2020 research and innovation
programme under grant agreement No. 787367 (PaVeS).

Orna Kupferman  11 Salomon Sickert (🖂)  1122

###### Abstract

Different classes of automata on infinite words have different expressive
power. Deciding whether a given language $L\subseteq\Sigma^{\omega}$ can be
expressed by an automaton of a desired class can be reduced to deciding a game
between Prover and Refuter: in each turn of the game, Refuter provides a
letter in $\Sigma$, and Prover responds with an annotation of the current
state of the run (for example, in the case of Büchi automata, whether the
state is accepting or rejecting, and in the case of parity automata, what the
color of the state is). Prover wins if the sequence of annotations she
generates is correct: it is an accepting run iff the word generated by Refuter
is in $L$. We show how a winning strategy for Refuter can serve as a simple
and easy-to-understand certificate to inexpressibility, and how it induces
additional forms of certificates. Our framework handles all classes of
deterministic automata, including ones with structural restrictions like weak
automata. In addition, it can be used for refuting separation of two languages
by an automaton of the desired class, and for finding automata that
approximate $L$ and belong to the desired class.

###### Keywords:

Automata on infinite words Expressive power Games.

##  1 Introduction

Finite automata on infinite objects were first introduced in the 60’s, and
were the key to the solution of several fundamental decision problems in
mathematics and logic [8, 32, 41]. Today, automata on infinite objects are
used for specification, verification, and synthesis of nonterminating systems.
The automata-theoretic approach reduces questions about systems and their
specifications to questions about automata [27, 49], and is at the heart of
many algorithms and tools. Industrial-strength property-specification
languages such as the IEEE 1850 Standard for Property Specification Language
(PSL) [14] include regular expressions and/or automata, making specification
and verification tools that are based on automata even more essential and
popular.

A run $r$ of an automaton on infinite words is an infinite sequence of states,
and acceptance is determined with respect to the set of states that $r$ visits
infinitely often. For example, in Büchi automata, some of the states are
designated as accepting states, denoted by $\alpha$, and a run is accepting
iff it visits states from the accepting set $\alpha$ infinitely often [8].
Dually, in co-Büchi automata, a run is accepting if it visits the set $\alpha$
only finitely often. Then, in parity automata, the acceptance condition maps
each state to a color in some set $C=\\{j,\ldots,k\\}$, for $j\in\\{0,1\\}$
and some index $k\geq 0$, and a run is accepting if the maximal color it
visits infinitely often is odd.

The different classes of automata have different expressive power. For
example, while deterministic parity automata can recognize all
$\omega$-regular languages, deterministic Büchi automata cannot [28]. We use
DBW, DCW, and DPW to denote a deterministic Büchi, co-Büchi, and parity word
automaton, respectively, or (this would be clear from the context) the set of
languages recognizable by the automata in the corresponding class. There has
been extensive research on expressiveness of automata on infinite words [48,
20]. In particular, researchers have studied two natural expressiveness
hierarchies induced by different classes of deterministic automata. The first
hierarchy is the Mostowski Hierarchy, induced by the index of parity automata
[34, 50]. Formally, let DPW[$0,k$] denote a DPW with $C=\\{0,\ldots,k\\}$, and
similarly for DPW[$1,k$] and $C=\\{1,\ldots,k\\}$. Clearly, DPW[$0,k$]
$\subseteq$ DPW[$0,k+1$], and similarly DPW[$1,k$] $\subseteq$ DPW[$1,k+1$].
The hierarchy is infinite and strict. Moreover, DPW[$0,k$] complements
DPW[$1,k+1$], and for every $k\geq 0$, there are languages $L_{k}$ and
$L^{\prime}_{k}$ such that $L_{k}\in$ DPW[$0,k$] $\setminus$ DPW[$1,k+1$] and
$L^{\prime}_{k}\in$ DPW[$1,k+1$] $\setminus$ DPW[$0,k$]. At the bottom of this
hierarchy, we have DBW and DCW. Indeed, DBW=DPW[$0,1$] and DCW=DPW[$1,2$].

While the Mostowski Hierarchy refines DPWs, the second hierarchy, which we
term the depth hierarchy, refines deterministic weak automata (DWWs). Weak
automata can be viewed as a special case of Büchi or co-Büchi automata in
which every strongly connected component in the graph induced by the structure
of the automaton is either contained in $\alpha$ or is disjoint from $\alpha$,
where $\alpha$ is depending on the acceptance condition the set of accepting
or rejecting states. The structure of weak automata captures the alternation
between greatest and least fixed points in many temporal logics, and they were
introduced in this context in [35]. DWWs have been used to represent vectors
of real numbers [6], and they have many appealing theoretical and practical
properties [31, 21]. In terms of expressive power, DWW = DCW $\cap$ DBW.

The depth hierarchy is induced by the depth of alternation between accepting
and rejecting components in DWWs. For this, we view a DWW as a DPW in which
the colors visited along a run can only increase. Accordingly, each run
eventually gets trapped in a single color, and is accepting iff this color is
odd. We use DWW[$0,k$] and DWW[$1,k$] to denote weak-DPW[$0,k$] and weak-
DPW[$1,k$], respectively. The picture obtained for the depth hierarchy is
identical to that of the Mostowski hierarchy, with DWW[$j,k$] replacing
DPW[$j,k$] [50]. At the bottom of the depth hierarchy we have co-safety and
safety languages [2]. Indeed, co-safety languages are DWW[$0,1$] and safety
are DWW[$1,2$].

Beyond the theoretical interest in expressiveness hierarchies, their study is
motivated by the fact many algorithms, like synthesis and probabilistic model
checking, need to operate on deterministic automata [5, 3]. The lower the
automata are in the expressiveness hierarchy, the simpler are algorithms for
reasoning about them. Simplicity goes beyond complexity, which typically
depends on the parity index [16], and involves important practical
considerations like minimization and canonicity (exists only for DWWs [31]),
circumvention of Safra’s determinization [26], and symbolic implementations
[47]. Of special interest is the characterization of DBWs. For example, it is
shown in [25] that given a linear temporal logic formula $\psi$, there is an
alternation-free $\mu$-calculus formula equivalent to $\forall\psi$ iff $\psi$
can be recognized by a DBW. Further research studies typeness for
deterministic automata, examining the ability to define a weaker acceptance
condition on top of a given automaton [19, 21].

Our goal in this paper is to provide a simple and easy-to-understand
explanation to inexpressibility results. The need to accompany results of
decision procedures by an explanation (often termed “certificate”) is not new,
and includes certification of a “correct” decision of a model checker [24,
44], reachability certificates in complex multi-agent systems [1], and
explainable reactive synthesis [4]. To the best of our knowledge, our work is
the first to provide certification to inexpressibility results.

The underlying idea is simple: Consider a language $L$ and a class $\gamma$ of
deterministic automata. We consider a turn-based two-player game in which one
player (Refuter) provides letters in $\Sigma$, and the second player (Prover)
responds with letters from a set $A$ of annotations that describe states in a
deterministic automaton. For example, when we consider a DBW, then
$A=\\{\mbox{\sc acc},\mbox{\sc rej}\\}$, and when we consider a DPW[$0,k$],
then $A=\\{0,\ldots,k\\}$. Thus, during the interaction, Refuter generates a
word $x\in\Sigma^{\omega}$ and Prover responds with a word $y\in A^{\omega}$.
Prover wins if for all words $x\in\Sigma^{\omega}$, we have that $x\in L$ iff
$y$ is accepting according to $\gamma$. Clearly, if there is a deterministic
$\gamma$ automaton for $L$, then Prover can win by following its run on $x$.
Dually, a finite-state winning strategy for Prover induces a deterministic
$\gamma$ automaton for $L$. The game-based approach is not new, and has been
used for deciding the membership of given $\omega$-regular languages in
different classes of deterministic automata [26]. Further, the game-based
formulation is used in descriptive set theory to classify sets into
hierarchies, see for example [39, Chapters 4 and 5] for an introduction that
focuses on $\omega$-regular languages. Our contribution is a study of
strategies for Refuter. Indeed, since the above described game is determined
[9] and the strategies are finite-state, Refuter has a winning strategy iff no
deterministic $\gamma$ automaton for $L$ exists, and this winning strategy can
serve as a certificate for inexpressibility.

Figure 1: A refuter for DBW-recognizability of “only finitely many $a$’s”.

###### Example 1

Consider the language $L_{\neg\infty a}\subseteq\\{a,b\\}^{\omega}$ of all
words with only finitely many $a$’s. It is well known that $L$ cannot be
recognized by a DBW [28]. In Figure 1 we describe what we believe to be the
neatest proof of this fact. The figure describes a transducer ${\cal R}$ with
inputs in $\\{\mbox{\sc acc,rej}\\}$ and outputs in $\\{a,b\\}$ – the winning
strategy of Refuter in the above described game. The way to interpret ${\cal
R}$ is as follows. In each round of the game, Prover tells Refuter whether the
run of her DBW for $L_{\neg\infty a}$ is in an accepting or a rejecting state,
and Refuter uses ${\cal R}$ in order to respond with the next letter in the
input word. For example, if Prover starts with acc, namely declaring that the
initial state of her DBW is accepting, then Refuter responds with $a$, and if
Prover continues with rej, namely declaring that the state reachable with $a$
is rejecting, then Refuter responds with $b$. If Prover continues with rej
forever, then Prover continues with $b$ forever. Thus, together Prover and
Refuter generate two words: $y\in\\{\mbox{\sc acc,rej}\\}^{\omega}$ and
$x\in\\{a,b\\}^{\omega}$. Prover wins whenever $x\in L_{\neg\infty a}$ iff $y$
contains infinitely many acc’s. If Prover indeed has a DBW for $L_{\neg\infty
a}$, then she can follow its transition function and win the game. By
following the refuter ${\cal R}$, however, Refuter can always fool Prover and
generate a word $x$ such that $x\in L_{\neg\infty a}$ iff $y$ contains only
finitely many acc’s. $\blacksquare$

We first define refuters for DBW-recognizability, and study their construction
and size for languages given by deterministic or nondeterministic automata.
Our refuters serve as a first inexpressibility certificate. We continue and
argue that each DBW-refuter for a language $L$ induces three words
$x\in\Sigma^{*}$ and $x_{1},x_{2}\in\Sigma^{*}$, such that
$x\cdot(x_{1}+x_{2})^{*}\cdot x_{1}^{\omega}\subseteq L$ and
$x\cdot(x_{1}^{*}\cdot x_{2})^{\omega}\cap L=\emptyset$. The triple $\langle
x,x_{1},x_{2}\rangle$ is an additional certificate for $L$ not being in DBW.
Indeed, we show that a language $L$ is not in DBW iff it has a certificate as
above. For example, the language $L_{\neg\infty a}$ has a certificate
$\langle\epsilon,b,a\rangle$. In fact, we show that Landweber’s proof for
$L_{\neg\infty a}$ can be used as is for all languages not in DBW, with
$x_{1}$ replacing $b$, $x_{2}$ replacing $a$, and adding $x$ as a prefix.

We then generalize our results on DBW-refutation and certification in two
orthogonal directions. The first is an extension to richer classes of
deterministic automata, in particular all classes in the two hierarchies
discussed above, as well as all deterministic Emerson-Lei automata (DELWs)
[17]. For the depth hierarchy, we add to the winning condition of the game a
structural restriction. For example, in a weak automaton, Prover loses if the
sequence $y\in A^{\omega}$ of annotations she generates includes infinitely
many alternations between acc and rej. We show how structural restrictions can
be easily expressed in our framework.

The second direction is an extension of the recognizability question to the
questions of separation and approximation: We say that a language
$L\subseteq\Sigma^{\omega}$ is a separator for two languages
$L_{1},L_{2}\subseteq\Sigma^{\omega}$ if $L_{1}\subseteq L$ and $L\cap
L_{2}=\emptyset$. Studies of separation include a search for regular
separators of general languages [11], as well as separation of regular
languages by weaker classes of languages, e.g., FO-definable languages [40] or
piecewise testable languages [12]. In the context of $\omega$-regular
languages, [2] presents an algorithm computing the smallest safety language
containing a given language $L_{1}$, thus finding a safety separator for
$L_{1}$ and $L_{2}$. As far as we know, besides this result there has been no
systematic study of separation of $\omega$-regular languages by deterministic
automata.

In addition to the interest in separators, we use them in the context of
recognizability in two ways. First, a third type of certificate that we
suggest for DBW-refutation of a language $L$ are “simple” languages $L_{1}$
and $L_{2}$ such that $L_{1}\subseteq L$, $L\cap L_{2}=\emptyset$, and
$\langle L_{1},L_{2}\rangle$ are not DBW-separable. Second, we use
separability in order to approximate languages that are not in DBW. Consider
such a language $L\subseteq\Sigma^{\omega}$. A user may be willing to
approximate $L$ in order to obtain DBW-recognizability. Specifically, we
assume that there are languages $I_{\downarrow}\subseteq L$ and
$I_{\uparrow}\subseteq\Sigma^{\omega}\setminus L$ of words that the user is
willing to under- and over-approximate $L$ with. Thus, the user searches for a
language that is a separator for $L\setminus I_{\downarrow}$ and
$\Sigma^{\omega}\setminus(L\cup I_{\uparrow})$. We study DBW-separability and
DBW-approximation, namely separability and approximation by languages in DBW.
In particular, we are interested in finding “small” approximating languages
$I_{\downarrow}$ and $I_{\uparrow}$ with which $L$ has a DBW-approximation,
and we show how certificates that refute DBW-separation can direct the search
to for successful $I_{\downarrow}$ and $I_{\uparrow}$. Essentially, as in
counterexample guided abstraction-refinement (CEGAR) for model checking [10],
we use certificates for non-DBW-separability in order to suggest interesting
radius languages. While in CEGAR the refined system excludes the
counterexample, in our setting the approximation of $L$ excludes the
certificate. As has been the case with recognizability, we extend our results
to all classes of deterministic automata.

##  2 Preliminaries

###  2.1 Transducers and Realizability

Consider two finite alphabets $\Sigma$ and $A$. It is convenient to think
about $\Sigma$ as the “main” alphabet, and about $A$ as an alphabet of
annotations. For two words $x=x_{0}\cdot x_{1}\cdot
x_{2}\cdots\in\Sigma^{\omega}$ and $y=y_{0}\cdot y_{1}\cdot y_{2}\cdots\in
A^{\omega}$, we define $x\oplus y$ as the word in $(\Sigma\times A)^{\omega}$
obtained by merging $x$ and $y$. Thus, $x\oplus
y=(x_{0},y_{0})\cdot(x_{1},y_{1})\cdot(x_{2},y_{2})\cdots$.

A $(\Sigma/A)$-transducer models a finite-state system that responds with
letters in $A$ while interacting with an environment that generates letters in
$\Sigma$. Formally, a $(\Sigma/A)$-transducer is ${\cal
T}=\langle\Sigma,A,\iota,S,s_{0},\rho,\tau\rangle$, where $\iota\in\\{{\it
sys,env}\\}$ indicates who initiates the interaction – the system or the
environment, $S$ is a set of states, $s_{0}\in S$ is an initial state,
$\rho:S\times\Sigma\rightarrow S$ is a transition function, and
$\tau:S\rightarrow A$ is a labelling function on the states. Consider an input
word $x=x_{0}\cdot x_{1}\cdot x_{2}\cdots\in\Sigma^{\omega}$. The run of
${\cal T}$ on $x$ is the sequence $s_{0},s_{1},s_{2}\ldots$ such that for all
$j\geq 0$, we have that $s_{j+1}=\rho(s_{j},x_{j})$. The annotation of $x$ by
${\cal T}$, denoted ${\cal T}(x)$, depends on $\iota$. If $\iota={\it sys}$,
then ${\cal T}(x)=\tau(s_{0})\cdot\tau(s_{1})\cdot\tau(s_{2})\cdots\in
A^{\omega}$. Note that the first letter in $A$ is the output of ${\cal T}$ in
$s_{0}$. This reflects the fact that the system initiates the interaction. If
$\iota={\it env}$, then ${\cal
T}(x)=\tau(s_{1})\cdot\tau(s_{2})\cdot\tau(s_{3})\cdots\in A^{\omega}$. Note
that now, the output in $s_{0}$ is ignored, reflecting the fact that the
environment initiates the interaction.

Consider a language $L\subseteq(\Sigma\times A)^{\omega}$. Let ${\it comp}(L)$
denote the complement of $L$. Thus, ${\it comp}(L)=(\Sigma\times
A)^{\omega}\setminus L$. We say that a language $L\subseteq(\Sigma\times
A)^{\omega}$ is $(\Sigma/A)$-realizable by the system if there is a
$(\Sigma/A)$-transducer ${\cal T}$ with $\iota={\it sys}$ such that for every
word $x\in\Sigma^{\omega}$, we have that $x\oplus{\cal T}(x)\in L$. Then, $L$
is $(A/\Sigma)$-realizable by the environment if there is an
$(A/\Sigma)$-transducer ${\cal T}$ with $i={\it env}$ such that for every word
$y\in A^{\omega}$, we have that ${\cal T}(y)\oplus y\in L$. When the language
$L$ is regular, realizability reduces to deciding a game with a regular
winning condition. Then, by determinacy of games and due to the existence of
finite-memory winning strategies [9], we have the following.

###### Proposition 1

For every $\omega$-regular language $L\subseteq(\Sigma\times A)^{\omega}$,
exactly one of the following holds.

  1. 1.

$L$ is $(\Sigma/A)$-realizable by the system.

  2. 2.

${\it comp}(L)$ is $(A/\Sigma)$-realizable by the environment.

###  2.2 Automata

A deterministic word automaton over a finite alphabet $\Sigma$ is ${\cal
A}=\langle\Sigma,Q,q_{0},\delta,\alpha\rangle$, where $Q$ is a set of states,
$q_{0}\in Q$ is an initial state, $\delta:Q\times\Sigma\rightarrow Q$ is a
transition function, and $\alpha$ is an acceptance condition. We extend
$\delta$ to words in $\Sigma^{*}$ in the expected way, thus for $q\in Q$,
$w\in\Sigma^{*}$, and letter $\sigma\in\Sigma$, we have that
$\delta(q,\epsilon)=q$ and $\delta(q,w\sigma)=\delta(\delta(q,w),\sigma)$. A
run of ${\cal A}$ on an infinite word
$\sigma_{0},\sigma_{1},\dots\in\Sigma^{\omega}$ is the sequence of states
$r=q_{0},q_{1},\dots$, where for every position $i\geq 0$, we have that
$q_{i+1}=\delta(q_{i},\sigma_{i})$. We use ${\it inf}(r)$ to denote the set of
states that $r$ visits infinitely often. Thus, ${\it inf}(r)=\\{q:\text{
}q_{i}=q\text{ for infinitely many }i\geq 0\\}$.

The acceptance condition $\alpha$ refers to ${\it inf}(r)$ and determines
whether the run $r$ is accepting. For example, in the Büchi, acceptance
condition, we have that $\alpha\subseteq Q$, and a run is accepting iff it
visits states in $\alpha$ infinitely often; that is, $\alpha\cap{\it
inf}(r)\neq\emptyset$. Dually, in co-Büchi, $\alpha\subseteq Q$, and a run is
accepting iff it visits states in $\alpha$ only finitely often; that is,
$\alpha\cap{\it inf}(r)=\emptyset$. The language of ${\cal A}$, denoted
$L({\cal A})$, is then the set of words $w$ such that the run of ${\cal A}$ on
$w$ is accepting.

A parity condition is $\alpha:Q\rightarrow\\{0,\ldots,k\\}$, for $k\geq 0$,
termed the index of $\alpha$. A run $r$ satisfies $\alpha$ iff the maximal
color $i\in\\{0,\ldots,k\\}$ such that $\alpha^{-1}(i)\cap{\it
inf}(r)\neq\emptyset$ is odd. That is, $r$ is accepting iff the maximal color
that $r$ visits infinitely often is odd. Then, a Rabin condition is
$\alpha=\\{\langle G_{1},B_{1}\rangle,\ldots,\langle G_{k},B_{k}\rangle\\}$,
with $G_{i},B_{i}\subseteq Q$, for all $0\leq i\leq k$. A run $r$ satisfies
$\alpha$ iff there is $1\leq i\leq k$ such that ${\it inf}(r)\cap
G_{i}\neq\emptyset$ and ${\it inf}(r)\cap B_{i}=\emptyset$. Thus, there is a
pair $\langle G_{i},B_{i}\rangle$ such that $r$ visits states in $G_{i}$
infinitely often and visits states in $B_{i}$ only finitely often.

All the acceptance conditions above can be viewed as special cases of the
Emerson-Lei acceptance condition (EL-condition, for short) [17], which we
define below. Let $\mathbb{M}$ be a finite set of marks. Given an infinite
sequence $\pi=M_{0}\cdot M_{1}\cdots\in(2^{\mathbb{M}})^{\omega}$ of subsets
of marks, let ${\it inf}(\pi)$ be the set of marks that appear infinitely
often in sets in $\pi$. Thus, ${\it inf}(\pi)=\\{m\in\mathbb{M}$ : there exist
infinitely many $i\geq 0$ such that $m\in M_{i}\\}$. An EL-condition is a
Boolean assertion over atoms in $\mathbb{M}$. For simplicity, we consider
assertions in positive normal form, where negation is applied only to atoms.
Intuitively, marks that appear positively should repeat infinitely often and
marks that appear negatively should repeat only finitely often. Formally, a
deterministic EL-automaton is ${\cal
A}=\langle\Sigma,Q,q_{0},\delta,\mathbb{M},\tau,\theta\rangle$, where
$\tau\colon Q\to 2^{\mathbb{M}}$ maps each state to a set of marks, and
$\theta$ is an EL-condition over $\mathbb{M}$. A run $r$ of a ${\cal A}$ is
accepting if ${\it inf}(\tau(r))$ satisfies $\theta$.

For example, a Büchi condition $\alpha\subseteq Q$ can be viewed as an EL-
condition with $\mathbb{M}=\\{\mbox{\sc acc}\\}$ and $\tau(q)=\\{\mbox{\sc
acc}\\}$ for $q\in\alpha$ and $\tau(q)=\emptyset$ for $q\not\in\alpha$. Then,
the assertion $\theta=\mbox{\sc acc}$ is satisfied by sequences $\pi$ induced
by runs $r$ with ${\it inf}(r)\cap\alpha\neq\emptyset$. Dually, the assertion
$\theta=\neg\mbox{\sc rej}$ with $\mathbb{M}=\\{\mbox{\sc rej}\\}$ is
satisfied by sequences $\pi$ induced by runs $r$ with ${\it
inf}(r)\cap\alpha=\emptyset$, and thus corresponds to a co-Büchi condition. In
the case of a parity condition $\alpha:Q\rightarrow\\{0,\ldots,k\\}$, it is
not hard to see that $\alpha$ is equivalent to an EL-condition in which
$\mathbb{M}=\\{0,1,\ldots,k\\}$, for every state $q\in Q$, we have that
$\tau(q)=\\{\alpha(q)\\}$, and $\theta=\theta_{k}$ expresses the parity
condition, where $\theta_{k}$ is inductively defined as:

$\theta_{k}=\begin{cases}\neg 0&\text{if }k=0,\\\ \neg
k\wedge\theta_{k-1}&\text{if }k\text{ is even,}\\\
\phantom{\neg}k\vee\theta_{k-1}&\text{If $k>0$ and $k$ is odd.}\end{cases}$

Lastly, a Rabin condition $\alpha=\\{\langle G_{1},B_{1}\rangle,\ldots,\langle
G_{k},B_{k}\rangle\\}$ is equivalent to an EL-condition with
$\mathbb{M}=\\{G_{1},B_{1},\dots,G_{k},B_{k}\\}$ and
$\tau(q)=\\{m\in\mathbb{M}:q\in m\\}$. Note that now, the mapping $\tau$ is
not to singletons, and each state is marked by all sets in $\alpha$ in which
it is a member. Then, $\theta=\bigvee_{1\leq i\leq k}(G_{i}\wedge\neg B_{i})$.

We use DBW, DCW, DPW, DRW, DELW to denote deterministic Büchi, co-Büchi,
parity, Rabin, and EL word automata, respectively. For parity automata, we
also use DPW[$0,k$] and DPW[$1,k$], for $k\geq 0$, to denote DPWs in which the
colours are in $\\{0,\ldots,k\\}$ and $\\{1,\ldots,k\\}$, respectively. For
Rabin automata, we use DRW[$k$], for $k\geq 0$, to denote DRWs that have at
most $k$ elements in $\alpha$. Finally, we use DELW[$\theta$], to denote DELWs
with EL-condition $\theta$. We sometimes use the above acronyms in order to
refer to the set of languages that are recognizable by the corresponding class
of automata. For example, we say that a language $L$ is in DBW if $L$ is _DBW-
recognizable_ , thus there is a DBW ${\cal A}$ such that $L=L({\cal A})$. Note
that DBW = DPW[$0,1$], DCW = DPW[$1,2$], and DRW[$1$] = DPW[$0,2$]. In fact,
in terms of expressiveness, DRW[$k$] = DPW[$0,2k$] [43, 30].

Consider a directed graph $G=\langle V,E\rangle$. A strongly connected set of
$G$ (SCS) is a set $C\subseteq V$ of vertices such that for every two vertices
$v,v^{\prime}\in C$, there is a path from $v$ to $v^{\prime}$. An SCS $C$ is
maximal if it cannot be extended to a larger SCS. Formally, for every nonempty
$C^{\prime}\subseteq V\setminus C$, we have that $C\cup C^{\prime}$ is not an
SCS. The maximal strongly connected sets are also termed strongly connected
components (SCC). An automaton ${\cal
A}=\langle\Sigma,Q,Q_{0},\delta,\alpha\rangle$ induces a directed graph
$G_{\cal A}=\langle Q,E\rangle$ in which $\langle q,q^{\prime}\rangle\in E$
iff there is a letter $\sigma$ such that $q^{\prime}\in\delta(q,\sigma)$. When
we talk about the SCSs and SCCs of ${\cal A}$, we refer to those of $G_{\cal
A}$. Consider a run $r$ of an automaton ${\cal A}$. It is not hard to see that
the set ${\it inf}(r)$ is an SCS. Indeed, since every two states $q$ and
$q^{\prime}$ in ${\it inf}(r)$ are visited infinitely often, the state
$q^{\prime}$ must be reachable from $q$.

A DBW ${\cal A}=\langle\Sigma,Q,q_{0},\delta,\alpha\rangle$ is _weak_ (DWW) if
every SCC $C$ of ${\cal A}$ is accepting, namely $C\subseteq\alpha$, or
rejecting, namely $C\cap\alpha=\emptyset$. Thus, each run of ${\cal A}$
eventually visits either states in $\alpha$ or only states not in $\alpha$. It
is easy to see that every DWW can be viewed as a DBW and as a DCW. In order to
refer to the depth of the SCCs in ${\cal A}$, we also refer to ${\cal A}$ also
as a DPW. Indeed, a DPW ${\cal A}=\langle\Sigma,Q,q_{0},\delta,\alpha\rangle$
is _weak_ if for every transition $q^{\prime}=\delta(q,\sigma)$ we have
$\alpha(q^{\prime})\geq\alpha(q)$, i.e., $\alpha$ is monotonically increasing
along a run. We use DWW[$0,k$] and DWW[$1,k$] to denote weak DPW[$0,k$] and
weak DPW[$1,k$], respectively. Finally, note that for each safety
$\omega$-regular language $L$, there exists a DWW[$1,2$] that recognises $L$
and all DWW[$1,2$] recognise a safety language. Dually, co-safety languages
correspond to DWW[$0,1$].

##  3 Refuting DBW-Recognizability

Let $A=\\{\mbox{\sc acc},\mbox{\sc rej}\\}$. We use $\infty\mbox{\sc acc}$ to
denote the subset $\\{a_{0}\cdot a_{1}\cdot a_{2}\cdots\in A^{\omega}:\mbox{
there are infinitely many $j\geq 0$ with }a_{j}=\mbox{\sc acc}\\}$ and
$\neg\infty\mbox{\sc acc}={\it comp}(\infty\mbox{\sc acc})=\\{a_{0}\cdot
a_{1}\cdot a_{2}\cdots\in A^{\omega}:\mbox{ there are only finitely many
$j\geq 0$ with }a_{j}=\mbox{\sc acc}\\}$.

A DBW ${\cal A}=\langle\Sigma,Q,q_{0},\delta,\alpha\rangle$ can be viewed as a
$(\Sigma/A)$-transducer ${\cal T}_{\cal A}=\langle\Sigma,A,{\it sys}$, $Q$,
$q_{0},\delta,\tau\rangle$, where for every state $q\in Q$, we have that
$\tau(q)=\mbox{\sc acc}$ if $q\in\alpha$, and $\tau(q)=\mbox{\sc rej}$
otherwise. Then, for every word $x\in\Sigma^{\omega}$, we have that $x\in
L({\cal A})$ iff ${\cal T}_{\cal A}(x)\in\infty{\mbox{\sc acc}}$.

For a language $L\subseteq\Sigma^{\omega}$, we define the language
$\operatorname{DBW}(L)\subseteq(\Sigma\times A)^{\omega}$ of words with
correct annotations. Thus,

$\operatorname{DBW}(L)=\\{x\oplus y:x\in L\mbox{ iff }y\in\infty{\mbox{\sc
acc}}\\}.$

Note that ${\it comp}(\operatorname{DBW}(L))$ is the language

$\operatorname{NoDBW}(L)=\\{x\oplus y:(x\in L\mbox{ and
}y\not\in\infty{\mbox{\sc acc}})\mbox{ or }(x\not\in L\mbox{ and
}y\in\infty{\mbox{\sc acc}})\\}.$

A DBW-refuter for $L$ is an $(A/\Sigma)$-transducer with $\iota={\it env}$
realizing $\operatorname{NoDBW}(L)$.

###### Example 2

For every language $R\subseteq\Sigma^{*}$ of finite words, the language
$R^{\omega}\subseteq\Sigma^{\omega}$ consists of infinite concatenations of
words in $R$. It was recently shown that $R^{\omega}$ may not be in DBW [29].
The language used in [29] is $R=\$+(0\cdot\\{0,1,\$\\}^{*}\cdot 1)$. In Figure
2 below we describe a DBW-refuter for $R^{\omega}$.

Figure 2: A DBW-refuter for $(\$+(0\cdot\\{0,1,\$\\}^{*}\cdot 1))^{\omega}$.

Following ${\cal R}$, Refuter starts by generating a prefix $0\cdot 1$ and
then responds to acc with $1$ and responds with $\$$ to rej. Accordingly, if
Prover generates a rejecting run, Prover generates a word in $0\cdot
1\cdot(1+\$)^{*}\cdot\$^{\omega}$, which is in $R^{\omega}$. Also, if Prover
generates an accepting run, Prover generates a word in $0\cdot
1\cdot(1^{+}\cdot\$^{*})^{\omega}$, which has a single $0$ and infinitely many
$1$’s, and is therefore not in $R^{\omega}$. $\blacksquare$

By Proposition 1, we have the following.

###### Proposition 2

Consider a language $L\subseteq\Sigma^{\omega}$. Let $A=\\{\mbox{\sc
acc},\mbox{\sc rej}\\}$. Exactly one of the following holds:

  * •

$L$ is in DBW, in which case the language $\operatorname{DBW}(L)$ is
$(\Sigma/A)$-realizable by the system, and a finite-memory winning strategy
for the system induces a DBW for $L$.

  * •

$L$ is not in DBW, in which case the language $\operatorname{NoDBW}(L)$ is
$(A/\Sigma)$-realizable by the environment, and a finite-memory winning
strategy for the environment induces a DBW-refuter for $L$.

###  3.1 Complexity

In this section we analyze the size of refuters. We start with the case where
the language $L$ is given by a DPW.

###### Theorem 3.1

Consider a DPW ${\cal A}$ with $n$ states. Let $L=L({\cal A})$. One of the
following holds.

  1. 1.

There is a DBW for $L$ with $n$ states.

  2. 2.

There is a DBW-refuter for $L$ with $2n$ states.

###### Proof

If $L$ is in DBW, then, as DPWs are Büchi type [19], a DBW for $L$ can be
defined on top of the structure of ${\cal A}$, and so it has $n$ states. If
$L$ is not in DBW, then by Proposition 2, there is a DBW-refuter for $L$,
namely a $(\\{\mbox{\sc acc},\mbox{\sc rej}\\}/\Sigma)$-transducer that
realizes $\operatorname{NoDBW}(L)$. We show we can define a DRW ${\cal U}$
with $2n$ states for $\operatorname{NoDBW}(L)$. The result then follows from
the fact a realizable DRW is realized by a transducer of the same size as the
DRW [15].

We construct ${\cal U}$ by taking the union of the acceptance conditions of a
DRW ${\cal U}_{1}$ for $\\{x\oplus y:x\in L\mbox{ and
}y\not\in\infty{\mbox{\sc acc}}\\}$ and a DRW ${\cal U}_{2}$ for $\\{x\oplus
y:x\not\in L\mbox{ and }y\in\infty{\mbox{\sc acc}}\\}$. We obtain both DRWs by
taking the product of ${\cal A}$, extended to the alphabet
$\Sigma\times\\{\mbox{\sc acc},\mbox{\sc rej}\\}$, with a $2$-state automaton
for $\infty{\mbox{\sc acc}}$, again extended to the alphabet
$\Sigma\times\\{\mbox{\sc acc},\mbox{\sc rej}\\}$.

We describe the construction in detail. Let ${\cal
A}=\langle\Sigma,Q,q_{0},\delta,\alpha\rangle$. Then, the state space of
${\cal U}_{1}$ is $Q\times\\{\mbox{\sc acc},\mbox{\sc rej}\\}$ and its
transition on a letter $\langle\sigma,a\rangle$ follows $\delta$ when it reads
$\sigma$, with $a$ determining whether ${\cal U}_{1}$ moves to the acc or rej
copy. Let $\alpha_{1}$ be the Rabin condition equivalent to $\alpha$. We
obtain the acceptance condition of ${\cal U}_{1}$ by replacing each pair
$\langle G,B\rangle$ in $\alpha_{1}$ by $\langle G\times\\{\mbox{\sc
rej}\\},B\times\\{\mbox{\sc rej}\\}\cup Q\times\\{\mbox{\sc acc}\\}\rangle$.
It is not hard to see that a run of ${\cal U}_{1}$ satisfies the latter pair
iff its projection on $Q$ satisfies the pair $\langle G,B\rangle$ and its
projection on $\\{\mbox{\sc acc},\mbox{\sc rej}\\}$ has only finitely many
acc. The construction of ${\cal U}_{2}$ is similar, with $\alpha_{2}$ being a
Rabin condition that complements $\alpha$, and then replacing each pair
$\langle G,B\rangle$ in $\alpha_{2}$ by $\langle G\times\\{\mbox{\sc
acc}\\},B\times\\{\mbox{\sc acc},\mbox{\sc rej}\\})\rangle$. Since ${\cal
U}_{1}$ and ${\cal U}_{2}$ have the same state space, and we only have to take
the union of the pairs in their acceptance conditions, the $2n$ bound follows.
∎

Now, when $L$ is given by an NBW, an exponential bound follows from the
exponential blow up in determinization [42]. If we are also given an NBW for
${\it comp}(L)$, the complexity can be tightened. Formally, we have the
following.

###### Theorem 3.2

Given NBWs with $n$ and $m$ states, for $L$ and ${\it comp}(L)$, respectively,
one of the following holds.

  1. 1.

There is a DBW for $L$ with $\min\\{(1.65n)^{n},3^{m}\\}$ states.

  2. 2.

There is a DBW-refuter for $L$ with
$\min\\{2\cdot(1.65n)^{n},2\cdot(1.65m)^{m}\\}$ states.

###### Proof

If $L$ is in DBW, then a DBW for $L$ can be defined on top of a DPW for $L$,
which has at most $(1.65n)^{n}$ states [45], or by dualizing a DCW for ${\it
comp}(L)$. Since the translation of an NBW with $m$ states to a DCW, when it
exists, results in a DCW with $3^{m}$ states [7], we are done. If $L$ is not
in DBW, then we proceed as in the proof of Theorem 3.1, defining ${\cal U}$ on
the top of a DPW for either $L$ or ${\it comp}(L)$. ∎

###  3.2 Certifying DBW-Refutation

Consider a DBW-refuter ${\cal R}=\langle\\{\mbox{\sc acc},\mbox{\sc
rej}\\},\Sigma,{\it env},S,s_{0},\rho,\tau\rangle$. We say that a path
$s_{0},\ldots,s_{m}$ in ${\cal R}$ is an $\mbox{\sc rej}^{+}$-path if it
contains at least one transition and all the transitions along it are labeled
by rej; thus, for all $0\leq j<m$, we have that $s_{j+1}=\rho(s_{j},\mbox{\sc
rej})$. Then, a path $s_{0},\ldots,s_{m}$ in ${\cal R}$ is an acc-path if it
contains at least one transition and its first transition is labeled by acc.
Thus, $s_{1}=\rho(s_{0},\mbox{\sc acc})$.

###### Lemma 1

Consider a DBW-refuter ${\cal R}=\langle\\{\mbox{\sc acc},\mbox{\sc
rej}\\},\Sigma,{\it env},S,s_{0},\rho,\tau\rangle$. Then there exists a state
$s\in S$, a (possibly empty) path $p=s_{0},s_{1},\dots s_{m}$, a $\mbox{\sc
rej}^{+}$-cycle $p_{1}=s^{1}_{0},s^{1}_{1}\dots s^{1}_{m_{1}}$, and an acc-
cycle $p_{2}=s^{2}_{0},s^{2}_{1}\dots s^{2}_{m_{2}}$, such that
$s_{m}=s^{1}_{0}=s^{1}_{m_{1}}=s^{2}_{0}=s^{2}_{m_{2}}=s$.

###### Proof

Let $s_{i}\in S$ be a reachable state that belongs to an ergodic component in
the graph of ${\cal R}$ (that is, $s_{i}\in C$, for a set $C$ of strongly
connected states that can reach only states in $C$). Since ${\cal R}$ is
responsive, in the sense it can read in each round both acc and rej, we can
read from $s_{i}$ the input sequence $\mbox{\sc rej}^{\omega}$. Hence, ${\cal
R}$ has a $\mbox{\sc rej}^{+}$-path $s_{i},\ldots,s_{l},\ldots,s_{k}$ with
$s_{l}=s_{k}$, for $l<k$. It is easy to see that the claim holds with
$s=s_{l}$. In particular, since ${\cal R}$ is responsive and $C$ is strongly
connected, there exists an acc-cycle from $s_{l}$ to itself. ∎

Figure 3: The structure from Lemma 1 that exists in every DBW-refuter.

###### Theorem 3.3

An $\omega$-regular language $L$ is not in DBW iff there exist three finite
words $x\in\Sigma^{*}$ and $x_{1},x_{2}\in\Sigma^{+}$, such that

$x\cdot(x_{1}+x_{2})^{*}\cdot x_{1}^{\omega}\subseteq L\quad\text{ and }\quad
x\cdot(x_{1}^{*}\cdot x_{2})^{\omega}\cap L=\emptyset.$

###### Proof

Assume first that $L$ is not in DBW. Then, by Theorem 3.2, there exists a DBW-
refuter ${\cal R}$ for it. Let $p=s_{0},s_{1},\dots s_{m}$,
$p_{1}=s^{1}_{0},s^{1}_{1},\dots,s^{1}_{m_{1}}$, and
$p_{2}=s^{2}_{0},s^{2}_{1},\dots,s^{2}_{m_{2}}$, be the path, $\mbox{\sc
rej}^{+}$-cycle, and acc-cycle that are guaranteed to exist by Lemma 1. Let
$x,x_{1}$, and $x_{2}$ be the outputs that ${\cal R}$ generates along them.
Formally, $x=\tau(s_{1})\cdot\tau(s_{2})\cdots\tau(s_{m})$,
$x_{1}=\tau(s^{1}_{1})\cdot\tau(s^{1}_{2})\cdots\tau(s^{1}_{m_{1}})$, and
$x_{2}=\tau(s^{2}_{1})\cdot\tau(s^{2}_{1})\cdots\tau(s^{2}_{m_{2}})$. Note
that as the environment initiates the interaction, the first letter in the
words $x$, $x_{1}$, and $x_{2}$, are the outputs in the second states in $p$,
$p_{1}$, and $p_{2}$. We prove that $x,x_{1}$, and $x_{2}$ satisfy the two
conditions in the theorem.

Let $y\in\\{\mbox{\sc acc},\mbox{\sc rej}\\}^{*}$, and
$y_{1},y_{2}\in\\{\mbox{\sc acc},\mbox{\sc rej}\\}^{+}$ be the input sequences
read along $p,p_{1}$, and $p_{2}$, respectively. Thus,
$y=a_{0},a_{1},\ldots,a_{m-1}$ is such that for all $0\leq j<m$, we have that
$s_{j+1}=\rho(s_{j},a_{j})$, and similarly for $y_{1}$ and $y_{2}$ with
$p_{1}$ and $p_{2}$.

Consider a word $w\in x\cdot(x_{1}+x_{2})^{*}\cdot x_{1}^{\omega}$. Let $a\in
y\cdot(y_{1}+y_{2})^{*}\cdot y_{1}^{\omega}$ be such that ${\cal R}(a)=w$.
Note we can obtain $a$ from $w$ by replacing each subword $x$ by $y$, $x_{1}$
by $y_{1}$, and $x_{2}$ by $y_{2}$. Since $p_{1}$ is a $\mbox{\sc
rej}^{+}$-cycle, we have that $a\in(\mbox{\sc acc}+\mbox{\sc
rej})^{*}\cdot\mbox{\sc rej}^{\omega}$, and so $a\in\neg\infty\mbox{\sc acc}$.
Since ${\cal R}$ is a refuter for $L$, it follows that ${\cal R}(a)\in L$.
Hence, $x\cdot(x_{1}+x_{2})^{*}\cdot x_{1}^{\omega}\subseteq L$.

For this direction it remains to show that $x\cdot(x_{1}^{*}\cdot
x_{2})^{\omega}\cap L=\emptyset$. Consider a word $w\in x\cdot(x_{1}^{*}\cdot
x_{2})^{\omega}$, and let $a\in y\cdot(y_{1}^{*}\cdot y_{2})^{\omega}$ be such
that ${\cal R}(a)=w$. Since $p_{1}$ is an acc-cycle, we have that
$a\in(\mbox{\sc rej}^{*}\mbox{\sc acc})^{\omega}$, and so $a\in\infty\mbox{\sc
acc}$. Since ${\cal R}$ is a refuter for $L$, it follows that ${\cal
R}(a)\notin L$. Hence, $x\cdot(x_{1}^{*}\cdot x_{2})^{\omega}\cap
L=\emptyset$, and we are done.

For the other direction, we adjust Landweber’s proof [28] for the non-DBW-
recognizability of $\neg\infty a$ to $L$. Essentially, $\neg\infty a$ can be
viewed as a special case of $x\cdot(x_{1}+x_{2})^{*}\cdot x_{1}^{\omega}$,
with $x=\epsilon$, $x_{1}=b$, and $x_{2}=a$. Assume by way of contradiction
that there is a DBW ${\cal A}$ with $L({\cal A})=L$. Let ${\cal
A}=\langle\Sigma,Q,q_{0},\delta,\alpha\rangle$. Consider the infinite word
$w_{0}=x\cdot x_{1}^{\omega}$. Since $w_{0}\in x\cdot(x_{1}+x_{2})^{*}\cdot
x_{1}^{\omega}$, and so $w\in L$, the run of ${\cal A}$ on $w_{0}$ is
accepting. Thus, there is $i_{1}\geq 0$ such that ${\cal A}$ visits $\alpha$
when it reads the $x_{1}$ suffix of $x\cdot x_{1}^{i_{1}}$. Consider now the
infinite word $w_{1}=x\cdot x_{1}^{i_{1}}\cdot x_{2}\cdot x_{1}^{\omega}$.
Since $w_{1}$ is also in $L$, the run of ${\cal A}$ on $w_{1}$ is accepting.
Thus, there is $i_{2}\geq 0$ such that ${\cal A}$ visits $\alpha$ when it
reads the $x_{1}$ suffix of $x\cdot x_{1}^{i_{1}}\cdot x_{2}\cdot
x_{1}^{i_{2}}$. In a similar fashion we can continue to find indices
$i_{1},i_{2},\ldots$ such for all $j\geq 1$, we have that ${\cal A}$ visits
$\alpha$ when it reads the $x_{1}$ suffix of $x\cdot x_{1}^{i_{1}}\cdot
x_{2}\cdot x_{1}^{i_{2}}\cdot x_{2}\cdots x_{2}\cdot x_{1}^{i_{j}}$. Since $Q$
is finite, there are iterations $j$ and $k$, such that $1\leq j<k\leq|Q|+1$
and there is a state $q$ such that $q=\delta(q_{0},x\cdot x_{1}^{i_{1}}\cdot
x_{2}\cdot x_{1}^{i_{2}}\cdot x_{2}\cdots x_{2}\cdot
x_{1}^{i_{j}})=\delta(q_{0},x\cdot x_{1}^{i_{1}}\cdot x_{2}\cdot
x_{1}^{i_{2}}\cdot x_{2}\cdots x_{2}\cdot x_{1}^{i_{k}})$. Since $j<k$, the
extension $x_{2}\cdot x_{1}^{i_{j+1}}\cdots x_{1}^{i_{k-1}}\cdot x_{2}\cdot
x_{1}^{i_{k}}$ is not empty and at least one state in $\alpha$ is visited when
${\cal A}$ loops in $q$ while reading it. It follows that the run of ${\cal
A}$ on the word

$w=x\cdot x_{1}^{i_{1}}\cdot x_{2}\cdot x_{1}^{i_{2}}\cdot x_{2}\cdots
x_{2}\cdot x_{1}^{i_{j}}\cdot(x_{2}\cdot x_{1}^{i_{j+1}}\cdots
x_{1}^{i_{k-1}}\cdot x_{2}\cdot x_{1}^{i_{k}})^{\omega}$

is accepting. But $w\in x\cdot(x_{1}^{*}\cdot x_{2})^{\omega}$, so it is not
in $L$, and we have reached a contradiction. ∎

###### Remark 1

Theorem 3.3, as well as the yet to be presented Theorems 6.2 and 6.3 are
special cases of [50, Lemma 14]. However, our alternative proof relies on
Proposition 1 and the analysis of the resulting refuter, while the proof of
[50] examines the structure of a deterministic Muller automaton. Due to the
game-based setting we can easily extend our approach to refuting separability
of languages (Section 4), which requires substantial modifications of the
approach from [50].

We refer to a triple $\langle x,x_{1},x_{2}\rangle$ of words that satisfy the
conditions in Theorem 3.3 as a certificate to the non-DBW-recognizability of
$L$.

###### Example 3

In Example 2, we described a DBW-refuter for
$L=(\$+(0\cdot\\{0,1,\$\\}^{*}\cdot 1))^{\omega}$. A certificate to its non-
DBW-recognizability is $\langle x,x_{1},x_{2}\rangle$, with $x=01$,
$x_{1}=\$$, and $x_{2}=1$. Indeed, $01\cdot(\$+1)^{*}\cdot\$^{\omega}\subseteq
L$ and $01\cdot(\$^{*}\cdot 1)^{\omega}\cap L=\emptyset$. $\blacksquare$

Note that obtaining certificates according to the proof of Theorem 3.3 may not
give us the shortest certificate. For example, for $L$ in Example 3, the proof
would give us $x=01\$$, $x_{1}=\$$, and $x_{2}=1\$,$ with
$01\$\cdot(\$+1\$)^{*}\cdot\$^{\omega}\subseteq L$ and $01\$\cdot(\$^{*}\cdot
1\$)^{\omega}\cap L=\emptyset$. The problem of generating smallest
certificates is related to the problem of finding smallest witnesses to DBW
non-emptiness [22] and is harder. Formally, defining the length of a
certificate $\langle x,x_{1},x_{2}\rangle$ as $|x|+|x_{1}|+|x_{2}|$, we have
the following:

###### Theorem 3.4

Consider a DPW ${\cal A}$ and a threshold $l\geq 1$. The problem of deciding
whether there is a certificate of length at most $l$ for non-DBW-
recognizability of $L({\cal A})$ is NP-complete, for $l$ given in unary or
binary.

###### Proof

We start with membership in NP. Let $n$ be the number of states in ${\cal A}$.
By Theorem 3.1 and the construction in Theorem 3.3 we can bound the length of
a certificate to be at most $6n$, since these are constructed from simple
paths. Given a witness certificate $\langle x,x_{1},x_{2}\rangle$ of length at
most $l$ (the latter can be checked in polynomial time, regardless of how $l$
is given), checking the conditions in Theorem 3.3 involves checking
$x\cdot(x_{1}+x_{2})^{*}\cdot x_{1}^{\omega}\subseteq L({\cal A})$, namely
containment of a DCW of size linear in the certificate in the language of a
DPW, which can be done in polynomial time, and checking $x\cdot(x_{1}^{*}\cdot
x_{2})^{\omega}\cap L({\cal A})=\emptyset$, namely emptiness of the
intersection with a DBW, which again can be done in polynomial time.

For the NP-hardness, we describe a reduction from the Hamiltonian-cycle
problem on directed graphs. Formally, given a directed graph $G=\langle
V,E\rangle$, we describe a DPW that is not in DBW and which has a certificate
of length $|V|+1$ iff $G$ has a Hamiltonian cycle, namely a cycle that visits
each vertex in $V$ exactly once. The proof elaborates on the NP-hardness proof
of the problem of finding a shortest witness to DBW non-emptiness [22].

Let $V=\\{1,\ldots,n\\}$, and assume that $n\geq 2$ and $E$ is not empty. We
define a DPW ${\cal A}=\langle E,(V\times V)\cup\\{\langle
1,1\rangle_{\text{err}}\\},\\{\langle 1,1\rangle\\},\delta,\alpha\rangle$,
where $\alpha(\langle n,n\rangle)=1$, $\alpha(\langle
1,1\rangle_{\text{err}})=2$, $\alpha(q)=0$ for all other states $q$, and

$\displaystyle\delta(\langle i,j\rangle,(k,h))$
$\displaystyle=\begin{cases}\langle h,(j\text{ mod }n)+1\rangle&\text{if
}i=k=j,\\\ \langle h,j\rangle&\text{if }i=k\neq j,\\\ \langle
1,1\rangle_{\text{err}}&\text{otherwise.}\end{cases}$
$\displaystyle\delta(\langle 1,1\rangle_{err},(k,h))$
$\displaystyle=\begin{cases}\langle h,2\rangle\hskip 57.50008pt&\text{if
}k=1,\\\ \langle 1,1\rangle_{\text{err}}&\text{otherwise.}\end{cases}$

Intuitively, ${\cal A}$ interprets a word $w\in E^{\omega}$, as an infinite
path starting in vertex $1$, and it verifies that the path is valid on $G$.
Whenever ${\cal A}$ encounters an edge that does not match the current state,
which is tracked in the first component of the state space, it resets and
moves to $\langle 1,1\rangle_{\text{err}}$. The second component of a state
$\langle i,j\rangle$ is the vertex the path owes a visit in order to visit all
vertices infinitely often. It is easy to see that $w\in L({\cal A})$ iff there
is a suffix $w^{\prime}$ of $w$ that describes a valid path in $G$ that visits
every vertex infinitely often. Notice that $L({\cal A})$ is not DBW-
recognizable and that ${\cal A}$ is polynomial in the size of $G$.

Clearly, the reduction is polynomial, we now prove its correctness. Assume
first that $G$ has a Hamiltonian cycle $c$. Then, from the word $w$ read along
$c$ from vertex 1, we construct the certificate
$\langle\epsilon,w,(2,1)\rangle$ showing non-DBW-recognizabilty. Indeed, the
certificate is correct, since $(w+(2,1))^{*}\cdot w^{\omega}\subseteq L({\cal
A})$ and $(w^{*}\cdot(2,1))^{\omega}\cap L({\cal A})=\emptyset$. This
certificate has size $n+1$.

For the other direction, assume that $\langle x,x_{1},x_{2}\rangle$ is a
certificate of size (at most) $n+1$. Then, $x\cdot x_{1}^{\omega}\in L({\cal
A})$ and as $x_{2}$ is not empty, it must be that $|x|+|x_{1}|\leq n$. Let $r$
be the corresponding accepting run and thus $r$ visits $\langle n,n\rangle$
infinitely often. By the definition of $\delta$, the run $r$ also visits the
states $\langle i,i\rangle$, for all $1\leq i\leq n$. Since the transitions to
each of these states are labelled differently, $x_{1}$ must contain at least
$n$ different letters. Hence, $|x_{1}|$ must be $n$ and thus $G$ has a
Hamiltonian cycle.

###### Remark 2

[Relation with existing characterizations] By [28], the language of a DPW
${\cal A}=\langle\Sigma,Q,q_{0},\delta,\alpha\rangle$ is in DBW iff for every
accepting SCS $C\subseteq Q$ and SCS $C^{\prime}\supseteq C$, we have that
$C^{\prime}$ is accepting. The proof of Landweber relies on a complicated
analysis of the structural properties of ${\cal A}$. As we elaborate below,
Theorem 3.3, which relies instead on determinacy of games, suggests an
alternative proof. Similarly, [50] examines the structure of a deterministic
Muller automaton, and Theorem 3.3 can be viewed as a special case of Lemma 14
there, with a proof based on the game setting.

We use certificates in order to prove that a DPW ${\cal
A}=\langle\Sigma,Q,q_{0},\delta,\alpha\rangle$ is in DBW iff for every
accepting SCS $C\subseteq Q$ and SCS $C^{\prime}\supseteq C$, we have that
$C^{\prime}$ is accepting. First, an accepting SCS $C\subseteq Q$ and a
rejecting SCS $C^{\prime}\supseteq C$ induce a certificate $\langle
x,x_{1},x_{2}\rangle$. Indeed, taking a state $s\in C$, we can define $x$ to
be a word that leads from $q_{0}$ to $s$, $x_{1}$ to be a word that traverses
$C$, and $x_{2}$ a word that traverses $C^{\prime}$. Then, the set of states
traversed infinitely often in a run on a word in $x\cdot(x_{1}+x_{2})^{*}\cdot
x_{1}^{\omega}$ is $C$, and the set of states traversed infinitely often in a
run on a word in $x\cdot(x_{1}^{*}\cdot x_{2})^{\omega}$ is $C^{\prime}$. For
the other direction, a certificate $\langle x,x_{1},x_{2}\rangle$ induces an
accepting SCS $C\subseteq Q$ and a rejecting SCS $C^{\prime}\supseteq C$ as
follows. Consider a graph $G=\langle Q,E\rangle$, where $E(s,s^{\prime})$ iff
$\delta(s,x_{1})=s^{\prime}$ or $\delta(s,x_{2})=s^{\prime}$. We consider an
ergodic SCC that is reachable from $\delta(q_{0},x)$ in $G$. In this ergodic
SCC, we can traverse both words in $x\cdot(x_{1}+x_{2})^{*}\cdot
x_{1}^{\omega}$ along an accepting cycle $C$, and words in
$x\cdot(x_{1}^{*}\cdot x_{2})^{\omega}$ along a rejecting cycle, whose union
with $C$ can serve as $C^{\prime}$. $\blacksquare$

Being an $(A/\Sigma)$-transducer, every DBW-refuter ${\cal R}$ is responsive
and may generate many different words in $\Sigma^{\omega}$. Below we show that
we can leave ${\cal R}$ responsive and yet let it generate only words induced
by a certificate. Formally, we have the following.

###### Lemma 2

Given a certificate $\langle x,x_{1},x_{2}\rangle$ to non-DBW-recognizability
of a language $L\subseteq\Sigma^{\omega}$, we can define a refuter ${\cal R}$
for $L$ such that for every $y\in A^{\omega}$, if $y\models\infty\mbox{\sc
acc}$, then ${\cal R}(y)\in x\cdot(x_{1}^{*}\cdot x_{2})^{\omega}$, and if
$y\models\neg\infty\mbox{\sc acc}$, then ${\cal R}(y)\in
x\cdot(x_{1}+x_{2})^{*}\cdot x_{1}^{\omega}$.

###### Proof

Intuitively, ${\cal R}$ first ignores the inputs and outputs $x$. It then
repeatedly outputs either $x_{1}$ or $x_{2}$, according to the following
policy: in the first iteration, ${\cal R}$ outputs $x_{1}$. If during the
output of $x_{1}$ all inputs are rej, then ${\cal R}$ outputs $x_{1}$ also in
the next iteration. If an input acc has been detected, thus the prover tries
to accept the constructed word, the refuter outputs $x_{2}$ in the next
iteration, again keeping track of an acc input. If no acc has been input,
${\cal R}$ switches back to outputting $x_{1}$.

Formally, let $\langle x,x_{1},x_{2}\rangle$ be a certificate with
$x=x^{1}\cdots x^{n}$, $x_{1}=x^{1}_{1}\cdots x^{n_{1}}_{1}$, and
$x_{2}=x^{1}_{2}\cdots x_{2}^{n_{2}}$. We define ${\cal R}=\langle\\{\mbox{\sc
acc},\mbox{\sc rej}\\},\Sigma,{\it env},S,s_{0},\rho,\tau\rangle$ with the
components $S$, $\rho$, and $\tau$ defined as follows:

  * •

$S=\\{s_{0},s_{1},\dots,s_{n},(s^{1}_{1},a),\dots,(s^{n_{1}}_{1},a),(s^{1}_{2},a),\dots,(s^{n_{2}}_{2},a):a\in\\{\mbox{\sc
acc},\mbox{\sc rej}\\}\\}$

  * •

$\rho(s,a)=\begin{cases}s_{1}&\text{if }s=s_{0}\text{ and }n>0,\\\
s_{i+1}&\text{if }s=s_{i}\text{ and }n>i>0,\\\ (s^{1}_{1},\mbox{\sc
rej})&\text{if }s=s_{n},\\\ (s^{1}_{1},\mbox{\sc rej})&\text{if
}s\in\\{(s^{n_{1}}_{1},\mbox{\sc rej}),(s^{n_{2}}_{2},\mbox{\sc rej})\\}\text{
and }a=\mbox{\sc rej},\\\ (s^{1}_{2},\mbox{\sc rej})&\text{if
}s\in\\{(s^{n_{1}}_{1},\mbox{\sc rej}),(s^{n_{2}}_{2},\mbox{\sc rej})\\}\text{
and }a=\mbox{\sc acc},\\\ (s^{1}_{2},\mbox{\sc rej})&\text{if
}s\in\\{(s^{n_{1}}_{1},\mbox{\sc acc}),(s^{n_{2}}_{2},\mbox{\sc acc})\\}\\\
(s^{i+1}_{1},\mbox{\sc rej})&\text{if }s=(s^{i}_{1},\mbox{\sc rej})\text{ and
}n_{1}>i>0\text{ and }a=\mbox{\sc rej},\\\ (s^{i+1}_{1},\mbox{\sc
acc})&\text{if }s=(s^{i}_{1},\mbox{\sc rej})\text{ and }n_{1}>i>0\text{ and
}a=\mbox{\sc acc},\\\ (s^{i+1}_{1},\mbox{\sc acc})&\text{if
}s=(s^{i}_{1},\mbox{\sc acc})\text{ and }n_{1}>i>0,\\\ (s^{i+1}_{2},\mbox{\sc
rej})&\text{if }s=(s^{i}_{2},\mbox{\sc rej})\text{ and }n_{2}>i>0\text{ and
}a=\mbox{\sc rej},\\\ (s^{i+1}_{2},\mbox{\sc acc})&\text{if
}s=(s^{i}_{2},\mbox{\sc rej})\text{ and }n_{2}>i>0\text{ and }a=\mbox{\sc
acc},\\\ (s^{i+1}_{2},\mbox{\sc acc})&\text{if }s=(s^{i}_{2},\mbox{\sc
acc})\text{ and }n_{2}>i>0.\end{cases}$

  * •

$\tau(s_{i})=x^{i}$ and $\tau((s^{i}_{j},a))=x^{i}_{j}$. ∎

By Theorem 3.3, every language not in DBW has a certificate $\langle
x,x_{1},x_{2}\rangle$. As we argue below, these certificates are linear in the
number of states of the refuters.

###### Lemma 3

Let ${\cal R}$ be a DBW-refuter for $L\subseteq\Sigma^{\omega}$ with $n$
states. Then, $L$ has a certificate of the form $\langle x,x_{1},x_{2}\rangle$
such that $|x|+|x_{1}|+|x_{2}|\leq 2\cdot n$.

###### Proof

The paths $p$, $p_{1}$, and $p_{2}$ that induce $x$, $x_{1}$ and $x_{2}$ in
the proof of Theorem 3.3 are simple, and so they are all of length at most
$n$. Also, while these paths may share edges, we can define them so that each
edge appears in at most two paths. Indeed, if an edge appears in all three
path, we can shorten $p$. Hence, $|x|+|x_{1}|+|x_{2}|\leq 2\cdot n$, and we
are done. ∎

###### Theorem 3.5

Consider a language $L\subseteq\Sigma^{\omega}$ not in DBW. The length of a
certificate for the non-DBW-recognizability of $L$ is linear in a DPW for $L$
and is exponential in an NBW for $L$. These bounds are tight.

###### Proof

The upper bounds follow from Theorem 3.1 and Lemma 3, and the exponential
determinization of NBWs. The lower bound in the NBW case follows from the
exponential lower bound on the size of shortest non-universality witnesses for
non-deterministic finite word automata (NFW) [33]. We sketch the reduction:
Let $L_{n}\subseteq\\{0,1\\}^{*}$ be a language such that the shortest witness
for non-universality of $L_{n}$ is exponential in $n$, but $L_{n}$ has a
polynomial sized NFW. We then define
$L^{\prime}_{n}=(L_{n}\cdot\$\cdot(0^{*}\cdot
1)^{\omega})+((0+1)^{*}\cdot\$\cdot(0+1)^{*}\cdot 0^{\omega})$. It is clear
that $L^{\prime}_{n}$ has a NBW polynomial in $n$ and is not DBW-recognizable.
Note that for every word $w\in L_{n}$, we have
$w\cdot\$\cdot(0+1)^{\omega}\subseteq L_{n}^{\prime}$. Thus, in order to
satisfy Theorem 3.3, every certificate $\langle x,x_{1},x_{2}\rangle$ needs to
have $w\cdot\$$ as prefix of $x$, for some $w\notin L_{n}$. Hence, it is
exponential in the size of the NBW. ∎

###### Remark 3

[LTL] When the language $L$ is given by an LTL formula $\varphi$, then
$\operatorname{DBW}(\varphi)=\varphi\leftrightarrow\textbf{GF}\mbox{\sc acc}$
and thus an off-the-shelf LTL synthesis tool can be used to extract a DBW-
refuter, if one exists. As for complexity, a doubly-exponential upper bound on
the size of a DPW for $\operatorname{NoDBW}(L)$, and then also on the size of
DBW-refuters and certificates, follows from the double-exponential translation
of LTL formulas to DPWs [49, 42]. The length of certificates, however, and
then, by Lemma 2, also the size of a minimal refuter, is related to the
diameter of the DPW for $\operatorname{NoDBW}(L)$, and we leave its tight
bound open. $\blacksquare$

##  4 Separability and Approximations

Consider three languages $L_{1},L_{2},L\subseteq\Sigma^{\omega}$. We say that
$L$ is a separator for $\langle L_{1},L_{2}\rangle$ if $L_{1}\subseteq L$ and
$L_{2}\cap L=\emptyset$. We say that a pair of languages $\langle
L_{1},L_{2}\rangle$ is DBW-separable iff there exists a language $L$ in DBW
such that $L$ is a separator for $\langle L_{1},L_{2}\rangle$.

###### Example 4

Let $\Sigma=\\{a,b\\}$, $L_{1}=(a+b)^{*}\cdot b^{\omega}$, and
$L_{2}=(a+b)^{*}\cdot a^{\omega}$. By [28], $L_{1}$ and $L_{2}$ are not in
DBW. They are, however, DBW-separable. A witness for this is $L=(a^{*}\cdot
b)^{\omega}$. Indeed, $L_{1}\subseteq L$, $L\cap L_{2}=\emptyset$, and $L$ is
DBW-recognizable. $\blacksquare$

Consider a language $L\subseteq\Sigma^{\omega}$, and suppose we know that $L$
is not in DBW. A user may be willing to approximate $L$ in order to obtain
DBW-recognizability. Specifically, we assume that there is a language
$I\subseteq\Sigma^{\omega}$ of words that the user is indifferent about.
Formally, the user is satisfied with a language in DBW that agrees with $L$ on
all words that are not in $I$. Formally, we say that a language $L^{\prime}$
approximates $L$ with radius $I$ if $L\setminus I\subseteq L^{\prime}\subseteq
L\cup I$. It is easy to see that, equivalently, $L^{\prime}$ is a separator
for $\langle L\setminus I,{\it comp}(L\cup I)\rangle$. Note that the above
formulation embodies the case where the user has in mind different over- and
under-approximation radiuses, thus separating $\langle L\setminus
I_{\downarrow},{\it comp}(L\cup I_{\uparrow})\rangle$ for possibly different
$I_{\downarrow}$ and $I_{\uparrow}$. Indeed, by defining
$I=(I_{\downarrow}\cap L)\cup(I_{\uparrow}\setminus L)$, we get $\langle
L\setminus I,{\it comp}(L\cup I)\rangle=\langle L\setminus I_{\downarrow},{\it
comp}(L)\setminus I_{\uparrow})\rangle$.

It follows that by studying DBW-separability, we also study DBW-approximation,
namely approximation by a language that is in DBW, possibly with different
over- and under-approximation radiuses.

Figure 4: Reduction of approximation to separability.

###### Remark 4

[From recognizability to separation] It is easy to see that DBW-separability
generalizes DBW-recognizability, as $L$ is in DBW iff $\langle L,{\it
comp}(L)\rangle$ is DBW-separable. Given $L\subseteq\Sigma^{\omega}$, we say
that a pair of languages $\langle L_{1},L_{2}\rangle$ is a no-DBW-witness for
$L$ if $L$ is a separator for $\langle L_{1},L_{2}\rangle$ and $\langle
L_{1},L_{2}\rangle$ is not DBW-separable. Note that the latter indeed implies
that $L$ is not in DBW.

A simple no-DBW witness for $L$ can be obtained as follows. Let ${\cal R}$ be
a DBW refuter for $L$. Then, we define $L_{1}=\\{{\cal
R}(y):y\in\neg\infty\mbox{\sc acc}\\}$ and $L_{2}=\\{{\cal
R}(y):y\in\infty\mbox{\sc acc}\\}$. By the definition of DBW-refuters, we have
$L_{1}\subseteq L$ and $L_{2}\cap L=\emptyset$, and so $\langle
L_{1},L_{2}\rangle$ is a no-DBW witness for $L$. It is simple, in the sense
that when we describe $L_{1}$ and $L_{2}$ by a tree obtained by pruning the
$\Sigma^{*}$-tree, then each node has at most two children – these that
correspond to the responses of ${\cal R}$ to acc and rej. $\blacksquare$

###  4.1 Refuting Separability

For a pair of languages $\langle L_{1},L_{2}\rangle$, we define the language
$\operatorname{SepDBW}(L)\subseteq(\Sigma\times A)^{\omega}$ of words with
correct annotations for separation. Thus,

$\operatorname{SepDBW}(L_{1},L_{2})=\\{x\oplus y:(x\in L_{1}\rightarrow
y\in\infty{\mbox{\sc acc}})\wedge(x\in L_{2}\rightarrow
y\not\in\infty{\mbox{\sc acc}})\\}.$

Note that ${\it comp}(\operatorname{SepDBW}(L_{1},L_{2}))$ is then the
language

$\operatorname{NoSepDBW}(L_{1},L_{2})=\\{x\oplus y:(x\in L_{1}\wedge
y\not\in\infty{\mbox{\sc acc}})\vee(x\in L_{2}\wedge y\in\infty{\mbox{\sc
acc}})\\}.$

A DBW-sep-refuter for $\langle L_{1},L_{2}\rangle$ is an
$(A/\Sigma)$-transducer with $\iota={\it env}$ that realizes
$\operatorname{NoSepDBW}(L_{1},L_{2})$.

###### Example 5

Consider the language $L_{\neg\infty a}=(a+b)^{*}\cdot b^{\omega}$, which is
not DBW. Let $I=a^{*}\cdot b^{\omega}+b^{*}\cdot a^{\omega}$, thus we are
indifferent about words with only one alternation between $a$ and $b$. In
Figure 5 we describe a DBW-sep refuter for $\langle L_{\neg\infty a}\setminus
I,{\it comp}(L_{\neg\infty a}\cup I)\rangle$. Note that the refuter generates
only words in $a\cdot b\cdot a\cdot(a+b)^{\omega}$, whose intersection with
$I$ is empty. Consequently, the refutation is similar to the DBW-refutation of
$L_{\neg\infty a}$. $\blacksquare$

Figure 5: A DBW-sep refuter for $\langle L_{\neg\infty a}\setminus I,{\it
comp}(L_{\neg\infty a}\cup I)\rangle$.

By Proposition 1, we have the following extension of Proposition 2.

###### Proposition 3

Consider two languages $L_{1},L_{2}\subseteq\Sigma^{\omega}$. Let
$A=\\{\mbox{\sc acc},\mbox{\sc rej}\\}$. Exactly one of the following holds:

  * •

$\langle L_{1},L_{2}\rangle$ is DBW-separable, in which case the language
$\operatorname{SepDBW}(L_{1},L_{2})$ is $(\Sigma/A)$-realizable by the system,
and a finite-memory winning strategy for the system induces a DBW for a
language $L$ that separates $L_{1}$ and $L_{2}$.

  * •

$\langle L_{1},L_{2}\rangle$ is not DBW-separable, in which case the language
$\operatorname{NoSepDBW}(L)$ is $(A/\Sigma)$-realizable by the environment,
and a finite-memory winning strategy for the environment induces a DBW-sep-
refuter for $\langle L_{1},L_{2}\rangle$.

As for complexity, the construction of the game for
$\operatorname{SepDBW}(L_{1},L_{2})$ is similar to the one described in
Theorem 3.1. Here, however, the input to the problem includes two DPWs. Also,
the positive case, namely the construction of the separator does not follow
from known results.

###### Theorem 4.1

Consider DPWs ${\cal A}_{1}$ and ${\cal A}_{2}$ with $n_{1}$ and $n_{2}$
states, respectively. Let $L_{1}=L({\cal A}_{1})$ and $L_{2}=L({\cal A}_{2})$.
One of the following holds.

  1. 1.

There is a DBW ${\cal A}$ with $2\cdot n_{1}\cdot n_{2}$ states such that
$L({\cal A})$ DBW-separates $\langle L_{1},L_{2}\rangle$.

  2. 2.

There is a DBW-sep-refuter for $\langle L_{1},L_{2}\rangle$ with $2\cdot
n_{1}\cdot n_{2}$ states.

###### Proof

We show that $\operatorname{SepDBW}(L_{1},L_{2})$ and
$\operatorname{NoSepDBW}(L_{1},L_{2})$ can be recognised by DRWs with at most
$2\cdot n_{1}\cdot n_{2}$ states. Then, by [15], we can construct a DBW or a
DBW-sep-refuter with at most $2\cdot n_{1}\cdot n_{2}$ states. The
construction is similar to the one described in the proof of Theorem 3.1. The
only technical challenge is the fact $\operatorname{SepDBW}(L_{1},L_{2})$ is
defined as the intersection, rather than union, of two languages. For this, we
observe that we can define $\operatorname{SepDBW}(L_{1},L_{2})$ also as
$\\{x\oplus y:(y\in\infty\mbox{\sc acc}\text{ and }x\notin L_{2})\text{ or
}(y\notin\infty\mbox{\sc acc}\text{ and }x\notin L_{1})\\}$. With this
formulation we then can reuse the union construction as seen in Theorem 3.1 to
obtain DRWs with at most $2\cdot n_{1}\cdot n_{2}$ states. ∎

As has been the case with DBW-recognizability, one can generate certificates
from a DBW-sep-refuter. The proof is similar to that of Theorem 3.3, with
membership in $L_{1}$ replacing membership in $L$ and membership in $L_{2}$
replacing being disjoint from $L$. Formally, we have the following.

###### Theorem 4.2

Two $\omega$-regular languages $L_{1},L_{2}\subseteq\Sigma^{\omega}$ are not
DBW-separable iff there exist three finite words $x\in\Sigma^{*}$ and
$x_{1},x_{2}\in\Sigma^{+}$, such that

$x\cdot(x_{1}+x_{2})^{*}\cdot x_{1}^{\omega}\subseteq L_{1}\quad\text{ and
}\quad x\cdot(x_{1}^{*}\cdot x_{2})^{\omega}\subseteq L_{2}.$

We refer to a triple $\langle x,x_{1},x_{2}\rangle$ of words that satisfy the
conditions in Theorem 4.2 as a certificate to the non-DBW-separability of
$\langle L_{1},L_{2}\rangle$. Observe that the same way we generated a no-DBW
witness in Remark 4, we can extract, given a DBW-sep-refuter ${\cal R}$ for
$\langle L_{1},L_{2}\rangle$, languages $L^{\prime}_{1}\subseteq L_{1}$ and
$L^{\prime}_{2}\subseteq L_{2}$ that tighten $\langle L_{1},L_{2}\rangle$ and
are still not DBW-separable.

###  4.2 Certificate-Guided Approximation

In this section we describe a method for finding small approximating languages
$I_{\downarrow}$ and $I_{\uparrow}$ such that $\langle L\setminus
I_{\downarrow},{\it comp}(L)\setminus I_{\uparrow}\rangle$ is DBW-separable.
If this method terminates we obtain an approximation for $L$ that is DBW-
recognizable. As in counterexample guided abstraction-refinement (CEGAR) for
model checking [10], we use certificates for non-DBW-separability in order to
suggest interesting approximating languages. Intuitively, while in CEGAR the
refined system excludes the counterexample, here the approximation of $L$
excludes the certificate.

Consider a certificate $\langle x,x_{1},x_{2}\rangle$ for the non-DBW-
separability of $\langle L_{1},L_{2}\rangle$. We suggest the following five
approximations:

$\begin{array}[]{lcl}C_{0}=x\cdot(x_{1}+x_{2})^{\omega}&\rightsquigarrow&\langle
L_{1}\setminus C_{0},L_{2}\setminus C_{0}\rangle\\\
C_{1}=x\cdot(x_{1}+x_{2})^{*}\cdot x_{1}^{\omega}=L_{1}\cap
C_{0}&\rightsquigarrow&\langle L_{1}\setminus C_{1},L_{2}\rangle\\\
C_{2}=x\cdot(x_{2}^{*}\cdot x_{1})^{\omega}\supset
C_{1}&\rightsquigarrow&\langle L_{1},L_{2}\setminus C_{2}\rangle\\\
C_{3}=x\cdot(x_{1}^{*}\cdot x_{2})^{\omega}=L_{2}\cap
C_{0}&\rightsquigarrow&\langle L_{1},L_{2}\setminus C_{3}\rangle\\\
C_{4}=x\cdot(x_{1}+x_{2})^{*}\cdot x_{2}^{\omega}\subset
C_{3}&\rightsquigarrow&\langle L_{1},L_{2}\setminus C_{4}\rangle\end{array}$

First, it is easy to verify that $\langle x,x_{1},x_{2}\rangle$ is indeed not
a certificate for the non-DBW-separability of the obtained candidate pairs
$\langle L_{1}^{\prime},L_{2}^{\prime}\rangle$. If $\langle
L_{1}^{\prime},L_{2}^{\prime}\rangle$ is DBW-separable, we are done (yet may
try to tighten the approximation). Otherwise, we can repeat the process with a
certificate for the non-DBW-separability of $\langle
L_{1}^{\prime},L_{2}^{\prime}\rangle$. As in CEGAR, some suggestions may be
more interesting than others, in some cases the process terminates, in some it
does not, and the user takes part directing the search.

###### Example 6

Consider again the language $L=(a+b)^{*}\cdot b^{\omega}$ and the certificate
$\langle x,x_{1},x_{2}\rangle=\langle\epsilon,b,a\rangle$. Trying to
approximate $L$ by a language in DBW, we start with the pair $\langle L,{\it
comp}(L)\rangle$. Our five suggestions are then as follows.

$\begin{array}[]{lcl}C_{0}=\Sigma^{\omega}&\rightsquigarrow&\langle L\setminus
C_{0},{\it comp}(L)\setminus C_{0}\rangle=\langle\emptyset,\emptyset\rangle\\\
C_{1}=(b+a)^{*}\cdot b^{\omega}&\rightsquigarrow&\langle L\setminus C_{1},{\it
comp}(L)\rangle=\langle\emptyset,{\it comp}(L)\rangle\\\ C_{2}=(a^{*}\cdot
b)^{\omega}&\rightsquigarrow&\langle L,{\it comp}(L)\setminus
C_{2}\rangle=\langle L,(a+b)^{*}\cdot a^{\omega}\rangle\\\ C_{3}=(b^{*}\cdot
a)^{\omega}&\rightsquigarrow&\langle L,{\it comp}(L)\setminus
C_{3}\rangle=\langle L,\emptyset\rangle\\\ C_{4}=(b+a)^{*}\cdot
a^{\omega}&\rightsquigarrow&\langle L,{\it comp}(L)\setminus
C_{4}\rangle=\langle L,(a+b)^{*}\cdot(a\cdot a^{*}\cdot b\cdot
b^{*})^{\omega}\rangle\end{array}$

Candidates $C_{0}$, $C_{1}$, and $C_{3}$ induce trivial approximations. Then,
$C_{2}$ suggests to over-approximate $L$ by setting $I_{\uparrow}$ to
$(a^{*}\cdot b)^{\omega}$, which we view as a nice solution, approximating
“eventually always $b$” by “infinitely often $b$”. Then, the pair derived from
$C_{4}$ is not DBW-separable. We can try to approximate it. Note, however,
that repeated approximations in the spirit of $C_{4}$ are going to only extend
the prefix of $x$ in the certificates, and the process does not terminate.

Let us now consider the slightly different certificate $\langle
x,x_{1},x_{2}\rangle=\langle a,b,a\rangle$ and the derived candidates:

$\begin{array}[]{lcl}C_{0}=a\cdot\Sigma^{\omega}&\rightsquigarrow&\langle
L\setminus C_{0},{\it comp}(L)\setminus C_{0}\rangle=\langle b\cdot
L,b\cdot{\it comp}(L)\rangle\\\ C_{1}=a\cdot(b+a)^{*}\cdot
b^{\omega}&\rightsquigarrow&\langle L\setminus C_{1},{\it
comp}(L)\rangle=\langle b\cdot L,{\it comp}(L)\rangle\\\
C_{2}=a\cdot(a^{*}\cdot b)^{\omega}&\rightsquigarrow&\langle L,{\it
comp}(L)\setminus C_{2}\rangle\\\ &&=\langle L,b\cdot{\it
comp}(L)+a\cdot(a+b)^{*}\cdot a^{\omega}\rangle\\\ C_{3}=a\cdot(b^{*}\cdot
a)^{\omega}&\rightsquigarrow&\langle L,{\it comp}(L)\setminus
C_{3}\rangle=\langle L,b\cdot{\it comp}(L)\rangle\\\
C_{4}=a\cdot(b+a)^{*}\cdot a^{\omega}&\rightsquigarrow&\langle L,{\it
comp}(L)\setminus C_{4}\rangle\\\ &&=\langle L,b\cdot{\it
comp}(L)+a\cdot(a+b)^{*}\cdot(a\cdot a^{*}\cdot b\cdot
b^{*})^{\omega}\rangle\end{array}$

One can easily verify that $\langle x,x_{1},x_{2}\rangle=\langle b\cdot
a,b,a\rangle$ is a certificate showing that none of the suggested pairs are
DBW-separable. In fact $\langle x,x_{1},x_{2}\rangle=\langle b^{i}\cdot
a,b,a\rangle$, for $i=0,1,2,\dots$, describes an infinite sequence such that
no refinement obtained after a finite number of steps is DBW-separable.
$\blacksquare$

##  5 Other Classes of Deterministic Automata

In this section we generalise the idea of DBW-refuters to other classes of
deterministic automata. For this we take again the view that a deterministic
automaton is a $\langle\Sigma,A\rangle$-transducer over a suitable annotation
alphabet $A$. We then characterize each class of deterministic automata by two
languages over $A$:

  * •

The language $L_{\textnormal{acc}}\subseteq A^{\omega}$, describing when a run
is accepting. For example, for DBWs, we have $A=\\{\mbox{\sc acc},\mbox{\sc
rej}\\}$ and $L_{\textnormal{acc}}=\infty\mbox{\sc acc}$.

  * •

The language $L_{\textnormal{struct}}\subseteq A^{\omega}$, describing
structural conditions on the run. For example, recall that a DWW is a DBW in
which the states of each SCS are either all accepting or all rejecting, and so
each run eventually get trapped in an accepting or rejecting SCS. Accordingly,
the language of runs that satisfy the structural condition is
$L_{\textnormal{struct}}=A^{*}\cdot(\mbox{\sc acc}^{\omega}+\mbox{\sc
rej}^{\omega})$.

We now formalize this intuition. Let $A$ be a finite set of annotations and
let $\gamma=\langle L_{\textnormal{acc}},L_{\textnormal{struct}}\rangle$, for
$L_{\textnormal{acc}},L_{\textnormal{struct}}\subseteq A^{\omega}$. A
deterministic automaton ${\cal A}=\langle\Sigma,Q,q_{0},\delta,\alpha\rangle$
is a deterministic $\gamma$ automaton (D$\gamma$W, for short) if there is a
function $\tau\colon Q\to A$ that maps each state to an annotation such that a
run $r$ of ${\cal A}$ satisfies $\alpha$ iff $\tau(r)\in
L_{\textnormal{acc}}$, and all runs $r$ satisfy the structural condition, thus
$\tau(r)\in L_{\textnormal{struct}}$. We then say that a language $L$ is
$\gamma$-recognizable if there a D$\gamma$W ${\cal A}$ such that $L=L({\cal
A})$.

Before we continue to study $\gamma$-recognizability, let us demonstrate the
$\gamma$-characterization of common deterministic automata. We first start
with classes $\gamma$ for which $L_{\textnormal{struct}}$ is trivial; i.e.,
$L_{\textnormal{struct}}=A^{\omega}$.

  * •

DBW: $A=\\{\mbox{\sc acc},\mbox{\sc rej}\\}$ and
$L_{\textnormal{acc}}=\infty\mbox{\sc acc}$.

  * •

DCW: $A=\\{\mbox{\sc acc},\mbox{\sc rej}\\}$ and
$L_{\textnormal{acc}}=\neg\infty\mbox{\sc acc}$.

  * •

DPW[$i,k$]: $A=\\{i,\dots,k\\}$ and $L_{\textnormal{acc}}=\\{y\in
A^{\omega}:\max({\it inf}(y))\text{ is odd}\\}$.

  * •

DELW[$\theta$]: $A=2^{\mathbb{M}}$ and $L_{\textnormal{acc}}=\\{y\in
A^{\omega}:y\models\theta\\}$.

Note that the characterizations for Büchi, co-Büchi, and parity are special
cases of the characterization for DELW. In a similar way, we could define a
language $L_{\textnormal{acc}}$ for DRW[$k$] and other common special cases of
DELWs. We continue to classes in the depth hierarchy, where $\gamma$ includes
also a structural restriction:

  * •

DWW: The set $A$ and the language $L_{\textnormal{acc}}$ are as for DBW or
DCW. In addition, $L_{\textnormal{struct}}=A^{*}\cdot(\mbox{\sc
acc}^{\omega}+\mbox{\sc rej}^{\omega})$.

  * •

DWW[$j,k$], for $j\in\\{0,1\\}$: The set $A$ and the language
$L_{\textnormal{acc}}$ are as for DPW[$j,k$]. In addition,
$L_{\textnormal{struct}}=\\{y_{0}\cdot y_{1}\cdots\in A^{\omega}:$ for all
$i\geq 0$, we have that $y_{i}\leq y_{i+1}\\}$.

  * •

Bounded Languages: A language $L$ is bounded if it is both safety and co-
safety. Thus, every word $w\in\Sigma^{\omega}$ has a prefix $v\in\Sigma^{*}$
such that either for all $u\in\Sigma^{\omega}$ we have $v\cdot u\in L$, or for
all $u\in\Sigma^{\omega}$ we have $v\cdot u\not\in L$ [23]. To capture this,
we use $A=\\{\mbox{\sc acc},\mbox{\sc rej},?\\}$, where $``?"$ is used for
annotating states with both accepting and rejecting continuations. Then,
$L_{\textnormal{acc}}=A^{*}\cdot\mbox{\sc acc}^{\omega}$, and
$L_{\textnormal{struct}}=?^{*}\cdot(\mbox{\sc acc}^{\omega}+\mbox{\sc
rej}^{\omega})$.

  * •

Deterministic $(m,n)$-Superparity Automata [39]: $A=\\{(i,j):0\leq i\leq
m,0\leq j\leq n\\}$, $L_{\textnormal{acc}}=\\{y_{m}\oplus y_{n}\in
A^{\omega}:\max({\it inf}(y_{m}))+\max(y_{n})\text{ is odd}\\}$, and
$L_{\textnormal{struct}}=\\{y_{m}\oplus(y_{0}\cdot y_{1}\cdots)\in
A^{\omega}:y_{i}\leq y_{i+1},\mbox{ for all }i\geq 0\\}$.

Let $\Sigma$ be an alphabet, let $A$ be an annotation alphabet, and let
$\gamma=\langle L_{\textnormal{acc}},$ $L_{\textnormal{struct}}\rangle$, for
$L_{\textnormal{acc}},L_{\textnormal{struct}}\subseteq A^{\omega}$. We define
the language $\mathrm{Real}(L,\gamma)\subseteq(\Sigma\times A)^{\omega}$ of
words with correct annotations.

$\mathrm{Real}(L,\gamma)=\\{x\oplus y:y\in L_{\textnormal{struct}}\text{ and
}(x\in L\text{ iff }y\in L_{\textnormal{acc}})\\}.$

Note that the language $\operatorname{DBW}(L)$ can be viewed as a special case
of our general framework. In particular, in cases
$L_{\textnormal{struct}}=A^{\omega}$, we can remove the $y\in
L_{\textnormal{struct}}$ conjunct from $\mathrm{Real}(L,\gamma)$. Note that
${\it comp}(\mathrm{Real}(L,\gamma))$ is the language

$\mathrm{NoReal}(L,\gamma)=\\{x\oplus y:y\not\in L_{\textnormal{struct}}\mbox{
or }(x\in L\mbox{ iff }y\not\in L_{\textnormal{acc}})\\}.$

A $\gamma$-refuter for $L$ is then an $(A/\Sigma)$-transducer with $\iota={\it
env}$ that realizes $\mathrm{NoReal}(L,\gamma)$. We can now state the
“D$\gamma$W-generalization” of Proposition 2.

###### Proposition 4

Consider an $\omega$-regular language $L\subseteq\Sigma^{\omega}$, and a pair
$\gamma=\langle L_{\textnormal{acc}},L_{\textnormal{struct}}\rangle$, for
$\omega$-regular languages
$L_{\textnormal{acc}},L_{\textnormal{struct}}\subseteq A^{\omega}$. Exactly
one of the following holds:

  1. 1.

$L$ is in D$\gamma$W, in which case the language $\mathrm{Real}(L,\gamma)$ is
$(\Sigma/A)$-realizable by the system, and a finite-memory winning strategy
for the system induces a D$\gamma$W for $L$.

  2. 2.

$L$ is not in D$\gamma$W, in which case the language
$\mathrm{NoReal}(L,\gamma)$ is $(A/\Sigma)$-realizable by the environment, and
a finite-memory winning strategy for the environment induces a
$\gamma$-refuter for $L$.

Note that every DELW can be complemented by dualization, thus by changing its
acceptance condition from $\theta$ to $\neg\theta$. In particular, DBW and DCW
dualize each other. As we argue below, dualization is carried over to
refutation. For example, the $(\\{\mbox{\sc acc},\mbox{\sc
rej}\\}/\Sigma)$-transducer ${\cal R}$ from Figure 1 is both a DBW-refuter for
$\neg\infty a$ and a DCW-refuter for $\infty a$. Formally, we have the
following.

###### Theorem 5.1

Consider an EL-condition $\theta$ over $\mathbb{M}$. Let $A=2^{\mathbb{M}}$.
For every $(A/\Sigma)$-transducer ${\cal R}$ and language $L$, we have that
${\cal R}$ is a DELW$[\theta]$-refuter for $L$ iff ${\cal R}$ is a
DELW$[\neg\theta]$-refuter for ${\it comp}(L)$. In particular, for every
language $L$ and $(\\{\mbox{\sc acc},\mbox{\sc rej}\\}/\Sigma)$-transducer
${\cal R}$, we have that ${\cal R}$ is a DBW-refuter for $L$ iff ${\cal R}$ is
a DCW-refuter for ${\it comp}(L)$.

###### Proof

For DELW[$\theta$]-recognizability of $L$, the language of correct annotations
is $\\{x\oplus y:(x\in L\text{ iff }y\models\theta)\\}$, which is equal to
$\\{x\oplus y:(x\in{\it comp}(L)\text{ iff }y\models\neg\theta)\\}$, which is
the language of correct annotations for DELW[$\neg\theta$]-recognizability of
${\it comp}(L)$. ∎

While dualization is nicely carried over to refutation, this is not the case
for all expressiveness results. For example, while DWW=DBW$\cap$DCW, and in
fact DBW and DCW are weak type (that is, when the language of a DBW is in DWW,
an equivalent DWW can be defined on top of its structure, and similarly for
DCW [21]), we describe below a DWW-refuter that is neither a DBW- nor a DCW-
refuter. Intuitively, this is possible as in DWW refutation, Prover loses when
the input is not in $A^{*}\cdot(\mbox{\sc acc}^{\omega}+\mbox{\sc
rej}^{\omega})$, whereas in DBW and DCW refutation, Refuter has to respond
correctly also for these inputs.

###### Example 7

Let $\Sigma=\\{a,b,c,d\\}$, and $A=\\{\mbox{\sc acc},\mbox{\sc rej}\\}$.
Consider the language $L=(a^{+}\cdot b\cdot c^{*}\cdot d)^{*}\cdot
a^{\omega}+(a\cdot b\cdot d)^{\omega}$. Note that $L$ is in DCW, but not in
DBW, and hence also not in DWW. The $(A/\Sigma)$-transducer ${\cal R}$ in
Figure 6 is a DWW-refuter for $L$. To see this, recall that for DWWs, we have
that $L_{\textnormal{struct}}=A^{*}\cdot(\mbox{\sc acc}^{\omega}+\mbox{\sc
rej}^{\omega})$, and so all input sequences $y\in A^{\omega}$ that satisfy
$L_{\textnormal{struct}}$ eventually gets trapped in the $a^{\omega}$ loop,
generating a rejecting run on a word in the language, or gets trapped in the
$c^{\omega}$ loop, generating an accepting run on a word not in the language.

On the other hand, while $L$ is not in DBW, the transducer ${\cal R}$ is not a
DBW-refuter for $L$. To see this, observe that the DBW ${\cal A}$ in the
figure suggests a winning strategy for Prover in the game corresponding to
DBW. Indeed, when Prover generates $(\mbox{\sc rej}\cdot\mbox{\sc
acc}\cdot\mbox{\sc rej})^{\omega}$, which is accepting, then by following
${\cal R}$, Refuter responds with $(a\cdot b\cdot d)^{\omega}$, which is in
$L$, and so Prover wins. Note that, unsurprisingly, the input generated by
Prover does not satisfy $L_{\textnormal{struct}}$. $\blacksquare$

Figure 6: The DWW-refuter ${\cal R}$ looses as a DBW-refuter when it plays
against ${\cal A}$.

On the other hand, as every DWW is also a DBW and a DCW, every DBW-refuter or
DCW-refuter is also a DWW-refuter.

#### Separability and Approximation.

Consider a characterization $\gamma=\langle
L_{\textnormal{acc}},L_{\textnormal{struct}}\rangle$. Two languages
$L_{1},L_{2}\subseteq\Sigma^{\omega}$ are _$\gamma$ -separable_ if there
exists a D$\gamma$W${\cal A}$ such that $L_{1}\subseteq L({\cal A})$ and
$L_{2}\cap L({\cal A})=\emptyset$. We define the corresponding languages of
correct and incorrect annotations as follows.

  * •

$\mathrm{Sep}(L_{1},L_{2},L_{\textnormal{acc}},L_{\textnormal{struct}})=\\\
\\{x\oplus y:y\in L_{\textnormal{struct}}\text{ and }((x\in L_{1}\text{ and
}y\in L_{\textnormal{acc}})\text{ or }(x\in L_{2}\text{ and }y\notin
L_{\textnormal{acc}}))\\}$.

  * •

$\mathrm{NoSep}(L_{1},L_{2},L_{\textnormal{acc}},L_{\textnormal{struct}})={\it
comp}(\mathrm{Sep}(L_{1},L_{2},L_{\textnormal{acc}},L_{\textnormal{struct}}))=\\\
\\{x\oplus y:y\notin L_{\textnormal{struct}}\text{ or }((x\in L_{1}\text{ and
}y\notin L_{\textnormal{acc}})\text{ or }(x\in L_{2}\text{ and }y\in
L_{\textnormal{acc}}))\\}$.

Note that the language $\operatorname{SepDBW}(L_{1},L_{2})$ can be viewed as a
special case of our general framework and as before in cases
$L_{\textnormal{struct}}=A^{\omega}$, we can remove the $y\in
L_{\textnormal{struct}}$ conjunct from $\mathrm{Sep}$. A $\gamma$-sep-refuter
for $L$ is an $(A/\Sigma)$-transducer with $\iota={\it env}$ that realizes
$\mathrm{NoSep}(L_{1},L_{2},L_{\textnormal{acc}},L_{\textnormal{struct}})$. By
Proposition 1, exactly one of the following holds:

###### Proposition 5

Consider $\omega$-regular languages $L_{1},L_{2}\subseteq\Sigma^{\omega}$, and
a characterization $\gamma=\langle
L_{\textnormal{acc}},L_{\textnormal{struct}}\rangle$, for $\omega$-regular
languages $L_{\textnormal{acc}},L_{\textnormal{struct}}\subseteq A^{\omega}$.
Exactly one of the following holds:

  1. 1.

$\langle L_{1},L_{2}\rangle$ are $\gamma$-separable, in which case the
language $\mathrm{Sep}(L_{1},L_{2},\gamma)$ is $(\Sigma/A)$-realizable by the
system, and a finite-memory winning strategy for the system induces a
D$\gamma$W for some $L$ such that $L_{1}\subseteq L$ and $L\cap
L_{2}=\emptyset$.

  2. 2.

$\langle L_{1},L_{2}\rangle$ are not $\gamma$-separable, in which case the
language $\mathrm{NoSep}(L_{1},L_{2},\gamma)$ is $(A/\Sigma)$-realizable by
the environment, and a finite-memory winning strategy for the environment
induces a $\gamma$-sep-refuter for $\langle L_{1},L_{2}\rangle$.

##  6 Certifying D$\gamma$W-Refutation

In this section we extend the three-word certificates for non-DBW-
recognizability to richer classes of deterministic automata. The idea is
similar (and in fact a little tedious): each D$\gamma$W-refuter embodies a
structure (analogous to the one in Lemma 1) from which we can extract finite
words that constitute the corresponding certificate (analogous to the one in
Theorem 3.3). We describe here the details for classes in the Mostowski
hierarchy and well as for classes of the depth-hierarchy. We also restrict
ourselves to word-certificates for non-recognizability and do not show the
word-certificates for non-separability which have an identical structure.

###  6.1 Mostowski Hierarchy

First, by Theorem 5.1, certificates for a class and its dual class are
related. For example, dualizing Theorem 3.3, we obtain certificates for non-
DCW-recognizability as follows.

###### Theorem 6.1

An $\omega$-regular language $L$ is not in DCW iff there exist three finite
words $x\in\Sigma^{*}$ and $x_{1},x_{2}\in\Sigma^{+}$, such that

$x\cdot(x_{1}+x_{2})^{*}\cdot x_{1}^{\omega}\cap L=\emptyset\qquad\text{ and
}\qquad x\cdot(x_{1}^{*}\cdot x_{2})^{\omega}\subseteq L.$

Handling DPWs, we first define the analogue of a $\mbox{\sc rej}^{+}$-path,
and then point to the desired structure and the certificate it induces.
Consider a DPW[$i,k$]-refuter ${\cal R}=\langle\\{i,\dots,k\\},\Sigma,{\it
env},S,s_{0},\rho,\tau\rangle$ with $i\in\\{0,1\\}$ and $i\leq k$. Let
$\ell\in\\{i,\dots,k\\}$. We say that a path $s_{1},\ldots,s_{m}$ in ${\cal
R}$ is an $\ell^{+}_{\leq}$-path if its first transition is labelled $\ell$
and all its other transitions are labeled by colors in $\\{i,\dots\ell\\}$.
Thus, $s_{2}=\rho(s_{1},\ell)$ and, for all $1\leq j<m$, we have that
$s_{j+1}=\rho(s_{j},\ell^{\prime})$, for some $\ell^{\prime}\leq\ell$.

###### Lemma 4

Consider a DPW$[i,k]$-refuter ${\cal R}=\langle\\{i,\dots,k\\},\Sigma,{\it
env},S,s_{0},\rho,\tau\rangle$ with $i\in\\{0,1\\}$ and $i\leq k$. There
exists a state $s\in S$, a (possibly empty) path $p=s_{0},s_{1},\dots s_{m}$,
and for each $\ell\in\\{i,\dots,k\\}$, a $\ell^{+}_{\leq}$-cycle
$p_{\ell}=s^{\ell}_{1}\dots s^{\ell}_{m_{\ell}}$, such that
$s_{m}=s^{\ell}_{1}=s^{\ell}_{m_{\ell}}=s$.

###### Proof

Let ${\cal R}_{\leq j}$ denote the transducer that we obtain from ${\cal R}$
when we restrict $\delta$ to transitions labelled by at most $j$. Note that
${\cal R}$ is ${\cal R}_{\leq k}$. We proceed by induction on $j$ with $i\leq
j\leq k$ and show that in the transducer ${\cal R}_{\leq j}$ for every state
$s\in S$ there exists a state $s^{\prime}\in S$, a (possibly empty) path
$p=s_{1},\dots s_{m}$ with $s=s_{1}$, and that for each
$\ell\in\\{i,\dots,j\\}$ there exists a $\ell^{+}_{\leq}$-cycle
$p_{\ell}=s^{\ell}_{1},s^{\ell}_{2}\dots s^{\ell}_{m_{\ell}}$, such that
$s_{m}=s^{\ell}_{1}=s^{\ell}_{m_{\ell}}=s^{\prime}$. The base case for $j=i$
follows immediately from the fact that ${\cal R}_{\leq i}$ is responsive on
$\\{i\\}$ and by reading $i^{\omega}$ we obtain a lasso with the required
properties.

Let $j>i$ and let $s\in S$ be an arbitrary state. Further, let $s_{j}\in S$ be
a reachable state from $s$ that belongs to an ergodic component in the graph
of ${\cal R}_{\leq j}$ (that is, $s_{j}\in C$, for a set $C$ of strongly
connected states that can reach only states in $C$). By induction hypothesis
there exists $s^{\prime}\in S$, a (possibly empty) path $p=s_{j},s_{j+1},\dots
s_{m}$, and for each $\ell\in\\{i,\dots,j-1\\}$ there exists a
$\ell^{+}_{\leq}$-cycle $p_{\ell}=s^{\ell}_{1},s^{\ell}_{2}\dots
s^{\ell}_{m_{\ell}}$, such that
$s_{m}=s^{\ell}_{1}=s^{\ell}_{m_{\ell}}=s^{\prime}$ for every
$\ell\in\\{i,\dots,j-1\\}$. Since ${\cal R}_{\leq j}$ is responsive on
$\\{i,\dots,j\\}$ we can take from $s^{\prime}$ a transition labelled $\ell$
and since $C$ is ergodic we can find a path back to $s^{\prime}$. Thus we
obtain the missing $j^{+}_{\leq}$-cycle and by concatenating the path from $s$
to $s_{j}$ and the path $p$, we show that $s^{\prime}$ can be reached from
$s$. ∎

###### Theorem 6.2

Let $i\in\\{0,1\\}$ and $i\leq k$. An $\omega$-regular language $L$ is not in
DPW$[i,k]$ iff there exist finite words $x\in\Sigma^{*}$ and
$x_{i},\dots,x_{k}\in\Sigma^{+}$, such that for every even $i\leq\ell\leq k$,
we have

$x\cdot(x_{i}+\dots+x_{k})^{*}\cdot((x_{i}+x_{i+1}+\dots+x_{\ell-1})^{*}\cdot
x_{\ell})^{\omega}\subseteq L,$

and for every odd $i\leq\ell\leq k$, we have

$x\cdot(x_{i}+\dots+x_{k})^{*}\cdot((x_{i}+x_{i+1}+\dots+x_{\ell-1})^{*}\cdot
x_{\ell})^{\omega}\cap L=\emptyset.$

###### Proof

Assume first that $L$ is not in DPW[$i,k$]. Then, by Proposition 4, there
exists a DPW[$i,k$]-refuter ${\cal R}$ for it. From this refuter we can
extract via Lemma 4 a path $p$ and $\ell^{+}_{\leq}$-cycles. We then construct
the postulated finite words in the exact same way as in the proof of Theorem
3.3.

For the other direction, we first simplify the presentation by assuming $i=0$.
The proof for $i=1$ is analogous. Assume by way of contradiction that there is
a DPW$[0,k]$ ${\cal A}$ with $L({\cal A})=L$. Let ${\cal
A}=\langle\Sigma,Q,q_{0},\delta,\alpha\rangle$. Let $n=|Q|$ and consider the
following sequence of words $w_{0}=x_{0}^{n}$, $w_{1}=(w_{0}\cdot x_{1})^{n}$,
…, $w_{k}=(w_{k-1}\cdot x_{k})^{n}$. Let $q=\delta(q_{0},w)$ be a state that
is reached after reading $w\in x\cdot(x_{i}+x_{i+1}+\dots x_{k})^{*}$. Since
$w\cdot w_{0}^{\omega}\in L$, there must be a state $p_{0}$ that is visited
infinitely often and $\alpha(p_{0})$ is odd. Since $|w_{0}|\geq|Q|$, this
state must have been visited while reading $w_{0}$. Now, consider $w\cdot
w_{1}^{\omega}$. This word is rejected and by the same reasoning as before
there must be some $p_{1}$ such that $\alpha(p_{1})$ is even, it is visited
while reading $w_{1}$, and for every $p_{0}$ that belongs to a $w_{0}$
subsequences we have $\alpha(p_{1})>\alpha(p_{0})$. We continue and obtain a
sequence $\alpha(p_{k})>\dots>\alpha(p_{0})$ with $k$ strict inequalities.
Since $\alpha(p_{0})$ is odd, we have $\alpha(p_{0})>0$ and thus
$\alpha(p_{k})>k$, which contradicts the fact that ${\cal A}$ is a DPW$[0,k]$.
∎

Note that, by [38], the “flower”-structure that induces the certificate exists
also in DPWs for $L$. Specifically, while Lemma 4 shows that every
DPW$[i,k]$-refuter contains a “flower” with $k-i+1$ petals, it is shown in
[38] that for every $\omega$-language $L$ not in DPW[$1,k+1$], there exists a
DPW for $L$ that contains a flower with $k+1$ petals and this flower occurs in
some accepting run.

#### Rabin and Streett acceptance.

Recall that for all $k\geq 0$, we have that DRW[$k$] = DPW[$0,2k$] . Hence,
the certificates obtained through Theorem 6.2 carry over to the Rabin case.
Further, in a deterministic generalized Rabin automaton (DGRW), the acceptance
condition is of the form

$\alpha=\\{\langle B_{1},G_{1,1},\dots,G_{1,n_{1}}\rangle,\dots\langle
B_{k},G_{k,1},\dots,G_{n,k_{n}}\rangle\\},$

and a run $r$ is accepting if there is $j\in\\{1,\dots,k\\}$, such that ${\it
inf}(r)\cap B_{j}=\emptyset$ and ${\it inf}(r)\cap G_{j,\ell}\neq\emptyset$
for every $1\leq\ell\leq n_{j}$. Since degeneralization does not increase the
number of Rabin pairs, we have that DGRW[$k$] = DRW[$k$] = DPW[$0,2k$], and so
again the certificates obtained through Theorem 6.2 are applicable.
Nevertheless, a refuter for the DRW[$k$] may be more succinct than a
DPW$[0,2k]$-refuter.

Finally, the Streett and generalized acceptance conditions are dual to Rabin
and generalized Rabin, and certificates for them can be obtained dually.

###  6.2 Depth-Hierarchy

We continue to certificates for non-DWW[$i,k$]-recognizability. Consider a
DWW[$i,k$]-refuter ${\cal R}=\langle\\{i,\dots,k\\},\Sigma,{\it
env},S,s_{0},\rho,\tau\rangle$, with $i\in\\{0,1\\}$ and $i\leq k$. Let
$\ell\in\\{i,\dots,k\\}$. We say that a path $s_{1},\ldots,s_{m}$ in ${\cal
R}$ is an $\ell^{+}$-path if all transitions are labelled by $\ell$. Thus, for
all $1\leq j<m$, we have that $s_{j+1}=\rho(s_{j},\ell)$.

###### Lemma 5

Consider a DWW$[i,k]$-refuter ${\cal R}=\langle\\{i,\dots,k\\},\Sigma,{\it
env},S,s_{0},\rho,\tau\rangle$ with $i\in\\{0,1\\}$ and $i\leq k$. Let
$s^{i-1}$ be an alias for $s_{0}$. Then there exists a sequence of states
$s^{i},s^{i+1},\dots s^{k}\in S$, such that for every $j\in\\{i,\dots,k\\}$
there exists a (possibly empty) $j^{+}$-path $p^{j}=s^{j}_{1},s^{j}_{2},\dots
s^{j}_{m_{j}}$, and a $j^{+}$-cycle
$c^{j}=s^{j}_{m_{j}+1},s^{j}_{m_{j}+2}\dots s^{j}_{m_{j}+m^{\prime}_{j}}$ such
that $s^{j}_{m_{j}}=s^{j}_{m_{j}+1}=s^{j}_{m_{j}+m_{j}^{\prime}}=s^{j}$ and
$s^{j}_{1}=s^{j-1}$.

###### Proof

Such a structure can be found by constructing a sequence of lassos. Start by
reading $i^{\omega}$ from $s_{0}$ to construct an $i^{+}$-path $p^{i}$ and an
$i^{+}$-cycle $c^{i}$. $s^{i}$ is then the last state of $c^{i}$,
respectively. Then, continue by reading $(i+1)^{\omega}$ from $s^{i}$ to find
the next lasso and continue until all lassos are found. ∎

###### Theorem 6.3

Let $i\in\\{0,1\\}$ and $i\leq k$. An $\omega$-regular language $L$ is not in
DWW$[i,k]$ iff there exist finite words
$\hat{x}_{i},\hat{x}_{i+1},\dots,\hat{x}_{k}\in\Sigma^{*}$ and
$x_{i},x_{i+1},\dots,x_{k}\in\Sigma^{+}$, such that for every even
$i\leq\ell\leq k$, we have

$\hat{x}_{i}\cdot x_{i}^{*}\cdot\hat{x}_{i+1}\cdot
x_{i+1}^{*}\cdots\hat{x}_{\ell}\cdot x_{\ell}^{\omega}\subseteq L,$

and for every odd $i\leq\ell\leq k$, we have

$\hat{x}_{i}\cdot x_{i}^{*}\cdot\hat{x}_{i+1}\cdot
x_{i+1}^{*}\cdots\hat{x}_{\ell}\cdot x_{\ell}^{\omega}\cap L=\emptyset.$

###### Proof

Assume first that $L$ is not in DWW[$i,k$]. Then, by Proposition 4, there
exists a DWW[$i,k$]-refuter ${\cal R}$ for it. From this refuter we can
extract via Lemma 5 a sequence of states with the corresponding paths and
cycles. We then obtain words in the same manner as in the proof of Theorem
3.3.

For the remaining direction assume by way of contradiction that there is a
DWW[$i,k$] ${\cal A}=\langle\Sigma,Q,q_{0},\delta,\alpha\rangle$ with $L({\cal
A})=L$. We simplify the presentation by assuming $i=0$. The proof for $i=1$ is
analogous. Let $n=|Q|$ and consider the following sequence of words
$w_{0}=\hat{x}_{0}\cdot x_{0}^{n}$, $w_{1}=w_{0}\cdot\hat{x}_{1}\cdot
x_{1}^{n}$, …, $w_{k}=w_{k-1}\cdot\hat{x}_{k}\cdot x_{k}^{n}$. Since
$w_{0}\cdot x_{0}^{\omega}\in L$ and $w_{0}$ has more letters than ${\cal A}$
has states, we have $\alpha(\delta(q_{0},w_{0}))$ is odd. By the same argument
we have due to $w_{1}\cdot x_{1}^{\omega}\notin L$ that
$\alpha(\delta(q_{0},w_{1}))$ is even and since $w_{0}$ is a prefix of $w_{1}$
we also have $\alpha(\delta(q_{0},w_{1}))>\alpha(\delta(q_{0},w_{0}))$.
Continuing in this manner we obtain a chain of length
$\alpha(\delta(q_{0},w_{k}))>\alpha(\delta(q_{0},w_{k-1}))>\dots>\alpha(\delta(q_{0},w_{0}))$
with $k$ strict inequalities. Since the smallest element is odd, we have
$\alpha(\delta(q_{0},w_{0}))>0$ and thus $\alpha(\delta(q_{0},w_{k}))>k$ which
contradicts ${\cal A}$ being a DWW$[0,k]$. ∎

We continue with general DWWs.

###### Lemma 6

Consider a DWW-refuter ${\cal R}=\langle\\{\mbox{\sc acc},\mbox{\sc
rej}\\},\Sigma,{\it env},S,s_{0},\rho,\tau\rangle$. There exist two states
$s^{1},s^{2}\in S$, (possibly empty) paths $p_{0}=s_{0},s_{1},\dots
s_{m_{0}}$, $p_{1}=s_{m_{0}+1},\dots,s_{m_{0}+m_{1}}$, and
$p_{2}=s_{m_{0}+m_{1}+1},\dots,s_{m_{0}+m_{1}+m_{2}}$, a $\mbox{\sc
rej}^{+}$-cycle $c^{1}=s^{1}_{1},s^{1}_{2}\dots s^{1}_{l_{1}}$, and a
$\mbox{\sc acc}^{+}$-cycle $c^{2}=s^{2}_{1},s^{2}_{2}\dots s^{2}_{l_{2}}$,
such that
$s_{m_{0}}=s_{m_{0}+1}=s_{m_{0}+m_{1}+m_{2}}=s^{1}_{1}=s^{1}_{l_{1}}$ and
$s_{m_{0}+m_{1}}=s_{m_{0}+m_{1}+1}=s^{2}_{1}=s^{2}_{l_{2}}$.

###### Proof

Let $s\in S$ be state in an ergodic SCC of the graph of ${\cal R}$. Then the
$\mbox{\sc acc}^{+}$\- and $\mbox{\sc rej}^{+}$-cycle are obtained from the
lassos formed by reading from $s$ the words $\mbox{\sc acc}^{\omega}$ and
$\mbox{\sc rej}^{\omega}$, respectively. Since $s$ belongs to an ergodic SCC,
there exist paths connecting the first states of these cycles. ∎

We now obtain in the same way as before from Proposition 4 and Lemma 6, the
desired certificate:

###### Theorem 6.4

An $\omega$-regular language $L$ is not in DWW iff there exist five finite
words $x,x_{2},x_{4}\in\Sigma^{*}$ and $x_{1},x_{3}\in\Sigma^{+}$, such that

$x\cdot(x_{1}+x_{2}\cdot x_{3}^{*}\cdot x_{4})^{*}\cdot
x_{1}^{\omega}\subseteq L\leavevmode\nobreak\ \text{ and }\leavevmode\nobreak\
x\cdot(x_{1}+x_{2}\cdot x_{3}^{*}\cdot x_{4})^{*}\cdot x_{2}\cdot
x_{3}^{\omega}\cap L=\emptyset.$

Recall that DWW=DBW$\cap$DCW, so one would define a DWW certificate by
disjuncting the certificates for DBW and DCW in Theorems 3.3 and 6.1. Theorem
6.4, however, suggests a different certificate, and it is interesting to
relate it to the ones for DBW and DCW. Also note that while the DBW, DCW, and
DPW certificates are covered by [50, Lemma 14], this is not the case for the
DWW certificate in Theorem 6.4.

Recall that at the bottom of the depth hierarchy we have safety and co-safety
languages, whose intersection is the set of bounded languages.

###### Theorem 6.5

An $\omega$-regular language $L$ is not a bounded language iff there exist six
finite words $\hat{x}_{0},\hat{x}_{1},\hat{x}_{2}\in\Sigma^{*}$ and
$x_{0},x_{1},x_{2}\in\Sigma^{+}$, such that

$\hat{x}_{0}\cdot x_{0}^{*}\cdot\hat{x}_{1}\cdot x_{1}^{\omega}\subseteq
L\qquad\text{ and }\qquad\hat{x}_{0}\cdot x_{0}^{*}\cdot\hat{x}_{2}\cdot
x_{2}^{\omega}\cap L=\emptyset.$

###### Proof

Assume first that $L$ is not bounded. Then, by Proposition 4, there exists a
$\langle
L_{\textnormal{acc}}^{\text{bounded}},L_{\textnormal{struct}}^{\text{bounded}}\rangle$-refuter
${\cal R}$ for it. From this refuter we can extract three lassos: a
$?$-labeled lasso from which we obtain $\hat{x}_{0}$ and $x_{0}$; a rej-
labeled lasso starting at the entry-point of the first lasso from which we
obtain $\hat{x}_{1}$ and $x_{1}$; and a acc-labeled lasso starting at the
entry-point of the first lasso from which we obtain $\hat{x}_{2}$ and $x_{2}$.

For the other direction assume by way of contradiction that there is a
deterministic $\langle
L_{\textnormal{acc}}^{\text{bounded}},L_{\textnormal{struct}}^{\text{bounded}}\rangle$-automaton
${\cal A}=\langle\Sigma,Q,q_{0},\delta,\tau,\gamma\rangle$ with $L({\cal
A})=L$. Assume that $\hat{x}_{0}\cdot x_{0}^{\omega}\in L$. Thus after reading
$|Q|$ letters one state has been repeated and by the constraint it must be
accepting. Thus $\hat{x}_{0}\cdot x_{0}^{|Q|}\cdot\hat{x}_{2}\cdot
x_{2}^{\omega}\in L$ which is a contradiction. The other case is analogous. ∎

##  7 Discussion and Directions for Future Research

The automation of decision procedures makes certification essential. We
suggest to use the winning strategy of the refuter in expressiveness games as
a certificate to inexpressibility. We show that beyond this state-based
certificate, the strategy induces a word-based certificate, generated from
words traversed along a “flower structure” the strategy contains, as well as a
language-based certificate, consisting of languages that under- and over-
approximate the language in question and that are not separable by automata in
the desired class.

While our work considers expressive power, one can use similar ideas in order
to question the size of automata needed to recognize a given language. For
example, in the case of a regular language $L$ of finite words, the Myhill-
Nerode characterization [36, 37] suggests to refute the existence of
deterministic finite word automata (DFW) with $n$ states for $L$ by providing
$n+1$ prefixes that are not right-congruent. Using our approach, one can
alternatively consider the winning strategy of Refuter in a game in which the
set of annotations includes also the state space, and
$L_{\textnormal{struct}}$ ensures consistency of the transition relation. Even
more interesting is refutation of size in the setting of automata on infinite
words. Indeed, there, minimization is NP-complete [46], and there are
interesting connections between polynomial certificates and possible
membership in co-NP, as well as connections between size of certificates and
succinctness of the different classes of automata.

Finally, while the approximation scheme we studied is based on suggested over-
and under-approximating languages, it is interesting to study approximations
that are based on more flexible distance measures [13, 18].

## References

  * [1] Almagor, S., Lahijanian, M.: Explainable multi agent path finding. In: Proc. 19th International Conference on Autonomous Agents and Multiagent Systems. pp. 34–42 (2020)
  * [2] Alpern, B., Schneider, F.: Recognizing safety and liveness. Distributed computing 2, 117–126 (1987)
  * [3] Baier, C., de Alfaro, L., Forejt, V., Kwiatkowska, M.: Model checking probabilistic systems. In: Handbook of Model Checking., pp. 963–999. Springer (2018)
  * [4] Baumeister, T., Finkbeiner, B., Torfah, H.: Explainable reactive synthesis. In: 18th Int. Symp. on Automated Technology for Verification and Analysis (2020). https://doi.org/10.1007/978-3-030-59152-6_23
  * [5] Bloem, R., Chatterjee, K., Jobstmann, B.: Graph games and reactive synthesis. In: Handbook of Model Checking., pp. 921–962. Springer (2018)
  * [6] Boigelot, B., Jodogne, S., Wolper, P.: On the use of weak automata for deciding linear arithmetic with integer and real variables. In: Proc. Int. Joint Conf. on Automated Reasoning. Lecture Notes in Computer Science, vol. 2083, pp. 611–625. Springer (2001)
  * [7] Boker, U., Kupferman, O.: Co-ing Büchi made tight and useful. In: Proc. 24th IEEE Symp. on Logic in Computer Science. pp. 245–254 (2009)
  * [8] Büchi, J.: On a decision method in restricted second order arithmetic. In: Proc. Int. Congress on Logic, Method, and Philosophy of Science. 1960. pp. 1–12. Stanford University Press (1962)
  * [9] Büchi, J., Landweber, L.: Solving sequential conditions by finite-state strategies. Trans. AMS 138, 295–311 (1969)
  * [10] Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. Journal of the ACM 50(5), 752–794 (2003)
  * [11] Czerwinski, W., Lasota, S., Meyer, R., Muskalla, S., Kumar, K., Saivasan, P.: Regular separability of well-structured transition systems. In: Proc. 29th Int. Conf. on Concurrency Theory. LIPIcs, vol. 118, pp. 35:1–35:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)
  * [12] Czerwinski, W., Martens, W., Masopust, T.: Efficient separability of regular languages by subsequences and suffixes. In: Proc. 40th Int. Colloq. on Automata, Languages, and Programming. Lecture Notes in Computer Science, vol. 7966, pp. 150–161. Springer (2013)
  * [13] Dimitrova, R., Finkbeiner, B., Torfah, H.: Approximate automata for omega-regular languages. In: 17th Int. Symp. on Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, vol. 11781, pp. 334–349. Springer (2019)
  * [14] Eisner, C., Fisman, D.: A Practical Introduction to PSL. Springer (2006)
  * [15] Emerson, E., Jutla, C.: The complexity of tree automata and logics of programs. In: Proc. 29th IEEE Symp. on Foundations of Computer Science. pp. 328–337 (1988)
  * [16] Emerson, E., Jutla, C.: Tree automata, $\mu$-calculus and determinacy. In: Proc. 32nd IEEE Symp. on Foundations of Computer Science. pp. 368–377 (1991)
  * [17] Emerson, E., Lei, C.L.: Modalities for model checking: Branching time logic strikes back. Science of Computer Programming 8, 275–306 (1987)
  * [18] Gange, G., Ganty, P., Stuckey, P.: Fixing the state budget: Approximation of regular languages with small dfas. In: 15th Int. Symp. on Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, vol. 10482, pp. 67–83. Springer (2017)
  * [19] Krishnan, S., Puri, A., Brayton, R.: Deterministic $\omega$-automata vis-a-vis deterministic Büchi automata. In: Algorithms and Computations. Lecture Notes in Computer Science, vol. 834, pp. 378–386. Springer (1994)
  * [20] Kupferman, O.: Automata theory and model checking. In: Handbook of Model Checking, pp. 107–151. Springer (2018)
  * [21] Kupferman, O., Morgenstern, G., Murano, A.: Typeness for $\omega$-regular automata. International Journal on the Foundations of Computer Science 17(4), 869–884 (2006)
  * [22] Kupferman, O., Sheinvald-Faragy, S.: Finding shortest witnesses to the nonemptiness of automata on infinite words. In: Proc. 17th Int. Conf. on Concurrency Theory. Lecture Notes in Computer Science, vol. 4137, pp. 492–508. Springer (2006)
  * [23] Kupferman, O., Vardi, M.: On bounded specifications. In: Proc. 8th Int. Conf. on Logic for Programming Artificial Intelligence and Reasoning. Lecture Notes in Computer Science, vol. 2250, pp. 24–38. Springer (2001)
  * [24] Kupferman, O., Vardi, M.: From complementation to certification. Theoretical Computer Science 305, 591–606 (2005)
  * [25] Kupferman, O., Vardi, M.: From linear time to branching time. ACM Transactions on Computational Logic 6(2), 273–294 (2005)
  * [26] Kupferman, O., Vardi, M.: Safraless decision procedures. In: Proc. 46th IEEE Symp. on Foundations of Computer Science. pp. 531–540 (2005)
  * [27] Kurshan, R.: Computer Aided Verification of Coordinating Processes. Princeton Univ. Press (1994)
  * [28] Landweber, L.: Decision problems for $\omega$–automata. Mathematical Systems Theory 3, 376–384 (1969)
  * [29] Leshkowitz, O., Kupferman, O.: On repetition languages. In: 45th Int. Symp. on Mathematical Foundations of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs) (2020)
  * [30] Löding, C.: Methods for the transformation of automata: Complexity and connection to second order logic (1999), M.Sc. Thesis, Christian-Albrechts-University of Kiel
  * [31] Löding, C.: Efficient minimization of deterministic weak $\omega$-automata. Information Processing Letters 79(3), 105–109 (2001)
  * [32] McNaughton, R.: Testing and generating infinite sequences by a finite automaton. Information and Control 9, 521–530 (1966)
  * [33] Meyer, A., Stockmeyer, L.: The equivalence problem for regular expressions with squaring requires exponential space. In: Proc. 13th IEEE Symp. on Switching and Automata Theory. pp. 125–129 (1972)
  * [34] Mostowski, A.: Regular expressions for infinite trees and a standard form of automata. In: Computation Theory. Lecture Notes in Computer Science, vol. 208, pp. 157–168. Springer (1984)
  * [35] Muller, D., Saoudi, A., Schupp, P.: Alternating automata, the weak monadic theory of the tree and its complexity. In: Proc. 13th Int. Colloq. on Automata, Languages, and Programming. Lecture Notes in Computer Science, vol. 226, pp. 275 – 283. Springer (1986)
  * [36] Myhill, J.: Finite automata and the representation of events. Tech. Rep. WADD TR-57-624, pages 112–137, Wright Patterson AFB, Ohio (1957)
  * [37] Nerode, A.: Linear automaton transformations. Proceedings of the American Mathematical Society 9(4), 541–544 (1958)
  * [38] Niwinski, D., Walukiewicz, I.: Relating hierarchies of word and tree automata. In: Proc. 15th Symp. on Theoretical Aspects of Computer Science. Lecture Notes in Computer Science, vol. 1373. Springer (1998)
  * [39] Perrin, D., Pin, J.E.: Infinite words - automata, semigroups, logic and games, Pure and applied mathematics series, vol. 141. Elsevier Morgan Kaufmann (2004)
  * [40] Place, T., Zeitoun, M.: Separating regular languages with first-order logic. Log. Methods Comput. Sci. 12(1) (2016)
  * [41] Rabin, M.: Decidability of second order theories and automata on infinite trees. Transaction of the AMS 141, 1–35 (1969)
  * [42] Safra, S.: On the complexity of $\omega$-automata. In: Proc. 29th IEEE Symp. on Foundations of Computer Science. pp. 319–327 (1988)
  * [43] Safra, S.: Exponential determinization for $\omega$-automata with strong-fairness acceptance condition. In: Proc. 24th ACM Symp. on Theory of Computing (1992)
  * [44] S.Almagor, Chistikov, D., Ouaknine, J., Worrell, J.: O-minimal invariants for linear loops. In: Proc. 45th Int. Colloq. on Automata, Languages, and Programming. LIPIcs, vol. 107, pp. 114:1–114:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)
  * [45] Schewe, S.: Büchi complementation made tight. In: Proc. 26th Symp. on Theoretical Aspects of Computer Science. LIPIcs, vol. 3, pp. 661–672. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany (2009)
  * [46] Schewe, S.: Beyond Hyper-Minimisation—Minimising DBAs and DPAs is NP-Complete. In: Proc. 30th Conf. on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), vol. 8, pp. 400–411 (2010)
  * [47] di Stasio, A., Murano, A., Vardi, M.: Solving parity games: Explicit vs symbolic. In: 23rd International Conference on Implementation and Application of Automata. Lecture Notes in Computer Science, vol. 10977, pp. 159–172. Springer (2018)
  * [48] Thomas, W.: Automata on infinite objects. Handbook of Theoretical Computer Science pp. 133–191 (1990)
  * [49] Vardi, M., Wolper, P.: Reasoning about infinite computations. Information and Computation 115(1), 1–37 (1994)
  * [50] Wagner, K.: On $\omega$-regular sets. Information and Control 43, 123–177 (1979)

Open Access This chapter is licensed under the terms of the Creative
CommonsAttribution 4.0 International License
(http://creativecommons.org/licenses/by/4.0/), which permits use, sharing,
adaptation, distribution and reproduction in any medium or format, as long as
you give appropriate credit to the original author(s) and the source, provide
a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the
chapter’s Creative Commons license, unless indicated otherwise in a credit
line to the material. If material is not included in the chapter’s Creative
Commons license and your intendeduse is not permitted by statutory regulation
or exceeds the permitted use, you will need to obtain permission directly from
the copyright holder.