University of Liverpool,
UKsven.schewe@liverpool.ac.ukhttps://orcid.org/0000-0002-9093-9518 University
of Liverpool, UKqiyi.tang@liverpool.ac.ukhttps://orcid.org/0000-0002-9265-3011
Sven Schewe and Qiyi Tang <ccs2012> <concept>
<concept_id>10003752.10003766.10003770</concept_id> <concept_desc>Theory of
computation Automata over infinite objects</concept_desc>
<concept_significance>500</concept_significance> </concept> <concept>
<concept_id>10002950.10003648.10003700.10003701</concept_id>
<concept_desc>Mathematics of computing Markov processes</concept_desc>
<concept_significance>500</concept_significance> </concept> </ccs2012>
[500]Theory of computation Automata over infinite objects [500]Mathematics of
computing Markov processes John Q. Open and Joan R. Access 2 42nd Conference
on Very Important Topics (CVIT 2016) CVIT 2016 CVIT 2016 December 24–27, 2016
Little Whinging, United Kingdom 42 23

# On the Succinctness of Good-for-MDPs Automata

Sven Schewe  Qiyi Tang

###### Abstract

Good-for-MDPs and good-for-games automata are two recent classes of
nondeterministic automata that reside between general nondeterministic and
deterministic automata. Deterministic automata are good-for-games, and good-
for-games automata are good-for-MDPs, but not vice versa. One of the question
this raises is how these classes relate in terms of succinctness. Good-for-
games automata are known to be exponentially more succinct than deterministic
automata, but the gap between good-for-MDPs and good-for-games automata as
well as the gap between ordinary nondeterministic automata and those that are
good-for-MDPs have been open. We establish that these gaps are exponential,
and sharpen this result by showing that the latter gap remains exponential
when restricting the nondeterministic automata to separating safety or
unambiguous reachability automata.

###### keywords:

Good-for-MDPs automata, Good-for-games automata, Büchi automata, Markov
Decision Processes, Omega-regular objectives, Reinforcement learning

##  1 Introduction

Good-for-games (GfG) and good-for-MDPs (GfM) automata are automata with a
special form of nondeterminism that can be resolved on-the-fly. In the case of
good-for-games automata this needs to be possible in every context, while it
only needs to be possible for GfM automata in the context of finite MDPs. This
makes the restrictions posed on GfM automata milder. One of the implications
is that GfM automata are less complex than GfG automata, as GfM Büchi automata
can recognise all regular languages. But are they also significantly more
succinct?

We show that this is the case, establishing that GfM automata are
exponentially more succinct than GfG automata, where exponentially more
succinct means that a translation of automata with $n$ states (or transitions)
require automata with $2^{\Omega(n)}$ states in the worst case.

To show this, we develop a family ${\mathcal{G}}_{n}$ of automata with $n+2$
states and $3n+7$ transitions, and show that the smallest language equivalent
deterministic Büchi automaton (DBAs) has at least $2^{n}/(n+2)$ states. As GfG
Büchi automata are only quadratically more succinct than DBAs [8], this
implies that GfG auatomata recognising the language are in
$\Omega(\sqrt{2^{n}/n})$ (or: $\Omega(2^{n/2}/\sqrt{n})$).

We then continue to show a similar gap between Büchi automata with general
nondeterminism and those that are GfM, producing two families of automata,
$\mathcal{R}_{n}$ and $\mathcal{S}_{n}$, with $n+2$ states and $2n+5$
transitions and $n+1$ states and $2n$ transitions, respectively, and show that
a language equivalent GfM automaton requires at least $2^{n}$ states to
recognise either of these languages.

This is not only close to the known translation to slim automata [6] that
results in $3^{n}$ states (and no more than $2$ successors for any state
letter pair), but it provides more: each $\mathcal{R}_{n}$ is an
unambiguous111An _unambiguous_ automaton has, for every $\omega$-word, no more
than one accepting run reachability automaton, while each $\mathcal{S}_{n}$ is
a safety automaton, which is strongly unambiguous222A _strongly unambiguous_
automaton has, for every $\omega$-word, no more than one run and
separating333An automaton is _separated_ if different states have disjoint
languages; separating automata are therefore in particular unambiguous..
Moreover, we show the languages recognised by $\mathcal{R}_{n}$ are also
recognised by a separating Büchi automaton $\mathcal{R}_{n}^{\prime}$ with
$n+2$ states and $3(n+2)$ transitions.

That the succinctness gap extends to these smaller classes of automata is not
only interesting from a principle point of view, unambiguous automata appear
naturally both as a standard translation from LTL, and in model checking
Markov chains [3]. Being unambiguous is thus a different type of restriction
to nondeterminism, very different in nature, and yet with related fields of
application to GfM. It is also interesting to note that strong disambiguation
is more expensive ($\Omega((n-1)!)$, [7]) than translating a nondeterministic
Büchi automaton into one that is GfM ($O(3^{n})$, cf. [4, 5, 11, 6]).

##  2 Preliminaries

We write ${\rm Nature}$ for the set of nonnegative integers. Let $S$ be a
finite set. We denote by $\mathrm{Distr}(S)$ ($\mathrm{SubDistr}(S)$) the set
of probability (sub)distributions on $S$. For a (sub)distribution
$\varphi\in\mathrm{Distr}(S)$ (resp. $\mu\in\mathrm{SubDistr}(S)$), we write
${\mathsf{support}}(\varphi)=\\{s\in S\;|\;\varphi(s)>0\\}$ for its support.
The cardinal of $S$ is denoted $|S|$. We use $\Sigma$ to denote a finite
alphabet. We denote by $\Sigma^{*}$ the set of finite words over $\Sigma$ and
$\Sigma^{\omega}$ the set of $\omega$-words over $\Sigma$. We use the standard
notions of prefix and suffix of a word. By $w\alpha$ we denote the
concatenation of a finite word $w$ and an $\omega$-word $\alpha$.

###  2.1 Automata

A _nondeterministic_ word automaton is a tuple
${\mathcal{A}}=(\Sigma,Q,q_{0},\delta,F)$, where $\Sigma$ is a finite
alphabet, $Q$ is a finite set of states, $q_{0}\in Q$ is the initial state,
$\delta:Q\times\Sigma\to 2^{Q}$ is the transition function, and $F\subseteq Q$
is the set of final (or accepting) states444Especially for GfG automata, the
decision of putting acceptance on states or transitions can be quite important
for some questions, e.g. the minimisation of CoBüchi GfG automata is tractable
for transition based acceptance [9], but not for state based acceptance [10].
For establishing exponential succinctness gaps, however, it is not relevant,
as the translation from the more succinct transition based to state based
acceptance can only double the size of an automaton.. A nondeterministic word
automaton is _complete_ if $\delta(q,\sigma)\neq\emptyset$ for all $q\in Q$
and $\sigma\in\Sigma$. For a state $q\in Q$, we denote ${\mathcal{A}}_{q}$ the
NBA obtained from ${\mathcal{A}}$ by making $q$ the initial state.

A finite run $r$ of ${\mathcal{A}}$ on $w\in\Sigma^{*}$ is a finite word
$q_{0},w_{0},q_{1},w_{1},\ldots\in Q\times(\Sigma\times Q)^{*}$ such that
$q_{i}\in\delta(q_{i-1},w_{i-1})$ for all $i>0$. A nondeterministic finite
automaton (NFA) ${\mathcal{A}}$ accepts exactly those runs, in which it ends
in a state in $F$. A word in $\Sigma^{*}$ is accepted by the automaton if it
has an accepting run, and the language of an automaton, denoted
${\mathcal{L}}({\mathcal{A}})$, is the set of accepted words in $\Sigma^{*}$.
A family of NBAs is given in Figure 5.

A run $r$ of ${\mathcal{A}}$ on $w\in\Sigma^{\omega}$ is an $\omega$-word
$q_{0},w_{0},q_{1},w_{1},\ldots\in(Q\times\Sigma)^{\omega}$ such that
$q_{i}\in\delta(q_{i-1},w_{i-1})$ for all $i>0$. A nondeterministic Büchi word
automaton (NBA) ${\mathcal{A}}$ accepts exactly those runs, in which at least
one of the infinitely often occurring states is in $F$. A word in
$\Sigma^{\omega}$ is accepted by the automaton if it has an accepting run, and
the language of an automaton, denoted ${\mathcal{L}}({\mathcal{A}})$, is the
set of accepted words in $\Sigma^{\omega}$. Two example NBAs are given in
Figures 1 and 2.

A nondeterministic word automaton is called a _safety automaton_ if all states
are final (and therefore all runs accepting), and a _reachability automaton_
if there is only a single final state, say $f$, and that final state is a
sink, i.e. $\delta(f,\sigma)=\\{f\\}$ for all $\sigma\in\Sigma$.

$q_{0}$$q_{1}$$f$$0,1,\$$$1$$\$$$0,1$$0,1,\$$ Figure 1: The NBA
${\mathcal{G}}_{1}$ which recognises the language ${\mathcal{L}}_{1}^{\omega}$
in which there are infinitely many finite words from
${\mathcal{L}}_{1}=\\{0,1\\}^{*}1\$$. This NBA is GfM. It is neither GfG nor
unambiguous (or separated). $q_{0}$$q_{1}$$0,1$$1$$\$$ Figure 2:  The safety
NBA $\mathcal{S}_{1}$, which recognises the language
${\mathcal{L}}_{1}^{s}=\\{0,1\\}^{*}1\$^{\omega}\cup\\{0,1\\}^{\omega}$ that
contains all words over the alphabet $\\{0,1,\$\\}$ that contain either no
$\$$, or that contain a $1$ that is succeeded by only $\$$s. This NBA is
separated (and thus unambiguous), but neither GfG nor GfM.

A nondeterministic word automaton is _deterministic_ if the transition
function $\delta$ maps each state and letter pair to a singleton set, a set
consisting of a single state. For deterministic automata, we also extend
$\delta$ to words, by letting $\delta(q,\varepsilon)=q$ and
$\delta(q,w_{0}w_{1}\cdots w_{n})=\delta(\delta(q,w_{0}),w_{1}\cdots w_{n})$,
where we have $n\geq 1$ and $w_{i}\in\Sigma$ for $i\in\\{0,\cdots,n\\}$.

A nondeterministic automaton is called _good-for-games (GfG)_ if it only
relies on a limited form of nondeterminism: GfG automata can make their
decision of how to resolve their nondeterministic choices on the history at
any point of a run rather than using the knowledge of the complete word as a
nondeterministic automaton normally would without changing their language.
They can be characterised in many ways, including as automata that simulate
deterministic automata.

The NBA in Figure 1 is good-for-MDPs (GfM) as shown later in Lemma 4.4, but
neither GfG nor unambiguous (or separated). The NBA in Figure 2 is neither GfG
nor good-for-MDPs (GfM) as shown later at the end of Section 2.3, while it is
both unambiguous and separated.

###  2.2 Markov Decision Processes (MDPs)

A _(finite, transition-labelled) Markov decision process_ (MDP) is a tuple
$\langle S,{\mathsf{Act}},{\sf P},\Sigma,\ell\rangle$ consisting of a finite
set $S$ of states, a finite set ${\mathsf{Act}}$ of actions, a partial
function ${\sf
P}:S\times{\mathsf{Act}}\times\Sigma\mathrel{\ooalign{\hfil$\mapstochar\mkern
5.0mu$\hfil\cr$\to$\cr}}\mathrm{SubDistr}(S)$ denoting the probabilistic
transition, and a labelling function
$\ell:S\times{\mathsf{Act}}\times\Sigma\times S\to\Sigma$ such that
$\ell(s,{\sf m},\sigma,s^{\prime})=\sigma$. We have $\sum_{\sigma\text{ s.t.
}{\sf P}(s,{\sf m},\sigma)\text{ is defined}}{\sf P}(s,{\sf m},\sigma)\leq 1$.
The set of available actions in a state $s$ is ${\mathsf{Act}}(s)=\\{{\sf
m}\in{\mathsf{Act}}\;|\;\exists\sigma\in\Sigma\text{ such that }{\sf P}(s,{\sf
m},\sigma)\text{ is defined}\\}$. An MDP is a Markov chain (MC) if
$|{\mathsf{Act}}(s)|=1$ for all $s\in S$.

$s_{0}$$s_{1}$$s_{f}$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}:0$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\frac{1}{4}}:0$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\frac{1}{4}}:1$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\frac{1}{2}}:\$$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}:\$$
Figure 3:  An MDP with initial state $s_{0}$. Since each state has only one
available action ${\sf m}$ (not shown in the figure), the MDP is actually an
MC. The set of labels is $\\{0,1,\$\\}$ and the labelling function for the MC
is as follows: $\ell(s_{0},{\sf m},0,s_{1})=\ell(s_{1},{\sf m},0,s_{1})=0$,
$\ell(s_{1},{\sf m},1,s_{1})=1$, $\ell(s_{1},{\sf m},\$,s_{f})=\ell(s_{f},{\sf
m},\$,s_{f})=\$$. The probabilities of the transitions are indicated in red
before the labels. The chance that it produces a word in
${\mathcal{L}}_{1}^{s}$ recognised by $\mathcal{S}_{1}$ from Figure 2 is
$\frac{1}{4}$.

An infinite _run (path)_ of an MDP ${\mathcal{M}}$ is a sequence $s_{0}{\sf
m}_{1}\sigma_{1}\ldots\in(S\times{\mathsf{Act}}\times\Sigma)^{\omega}$ such
that ${\sf P}(s_{i},{\sf m}_{i+1},\sigma_{i+1})$ is defined and ${\sf
P}(s_{i},{\sf m}_{i+1},\sigma_{i+1})(s_{i+1})>0$ for all $i\geq 0$. A finite
run is a finite such sequence. Let $\Omega({\mathcal{M}})$ (${\rm
Paths}({\mathcal{M}})$) denote the set of (finite) runs in ${\mathcal{M}}$ and
$\Omega({\mathcal{M}})_{s}$ (${\rm Paths}({\mathcal{M}})_{s}$) denote the set
of (finite) runs in ${\mathcal{M}}$ starting from $s$. Abusing the notation
slightly, for an infinite run $r=s_{0}{\sf m}_{1}\sigma_{1}s_{1}{\sf
m}_{2}\sigma_{2}\ldots$ we write
$\ell(r)=\sigma_{1}\sigma_{2}\ldots\in\Sigma^{\omega}$.

A _strategy_ for an MDP is a function $\mu:{\rm
Paths}({\mathcal{M}})\to\mathrm{Distr}({\mathsf{Act}})$ that, given a finite
run $r$, returns a probability distribution on all the available actions at
the last state of $r$. A _deterministic_ strategy for an MDP is a function
$\mu:{\rm Paths}({\mathcal{M}})\to{\mathsf{Act}}$ that, given a finite run
$r$, returns a single available action at that state. The set of runs
$\Omega({\mathcal{M}})_{s}^{\mu}$ is a subset of $\Omega({\mathcal{M}})_{s}$
that correspond to strategy $\mu$ and initial state $s$. Given a finite-memory
strategy $\mu$ for ${\mathcal{M}}$, an MC $({\mathcal{M}})_{\mu}$ is induced
[2, Section 10.6].

A _sub-MDP_ of ${\mathcal{M}}$ is an MDP ${\mathcal{M}}^{\prime}=\langle
S^{\prime},{\mathsf{Act}}^{\prime},{\sf
P}^{\prime},\Sigma,\ell^{\prime}\rangle$, where $S^{\prime}\subseteq S$,
${\mathsf{Act}}^{\prime}\subseteq{\mathsf{Act}}$ is such that
${\mathsf{Act}}^{\prime}(s)\subseteq{\mathsf{Act}}(s)$ for every $s\in
S^{\prime}$, and ${\sf P}^{\prime}$ and $\ell^{\prime}$ are analogous to ${\sf
P}$ and $\ell$ when restricted to $S^{\prime}$ and ${\mathsf{Act}}^{\prime}$.
In particular, ${\mathcal{M}}^{\prime}$ is closed under probabilistic
transitions, i.e. for all $s\in S^{\prime}$, ${\sf
m}\in{\mathsf{Act}}^{\prime}$ and $\sigma\in\Sigma$ we have that ${\sf
P}^{\prime}(s,{\sf m},\sigma)(s^{\prime})>0$ implies that $s^{\prime}\in
S^{\prime}$. An _end-component_ [1, 2] of an MDP ${\mathcal{M}}$ is a sub-MDP
${\mathcal{M}}^{\prime}$ of ${\mathcal{M}}$ such that its underlying graph is
strongly connected555A set of states is strongly connected if every pair of
states are mutually reachable. and it has no outgoing transitions. An example
MDP (MC) is presented in Figure 3.

A strategy $\mu$ and an initial state $s\in S$ induce a standard probability
measure on sets of infinite runs, see, e.g., [2]. Such measurable sets of
infinite runs are called events or objectives. We write
$\mathrm{Pr}_{s}^{\mu}$ for the probability of an event $E\subseteq
sS^{\omega}$ of runs starting from $s$.

###  2.3 The Product of MDPs and NBAs

Given an MDP ${\mathcal{M}}=\langle S,{\mathsf{Act}},{\sf
P},\Sigma,\ell\rangle$ with initial state $s_{0}\in S$ and an NBA
${\mathcal{A}}=\langle\Sigma,Q,\delta,q_{0},F\rangle$, we want to compute an
optimal strategy satisfying the objective that the run of ${\mathcal{M}}$ is
in the language of ${\mathcal{A}}$. We define the semantic satisfaction
probability for ${\mathcal{A}}$ and a strategy $\mu$ from state $s\in S$ as:
$\mathrm{PSem}_{{\mathcal{A}}}^{{\mathcal{M}}}(s,\mu)=\mathrm{Pr}_{s}^{\mu}\\{r\in\Omega_{s}^{\mu}:\ell(r)\in{\mathcal{L}}({\mathcal{A}})\\}$
and
$\mathrm{PSem}_{{\mathcal{A}}}^{{\mathcal{M}}}(s)=\sup_{\mu}\big{(}\mathrm{PSem}_{{\mathcal{A}}}^{{\mathcal{M}}}(s,\mu)\big{)}$.
In the case that ${\mathcal{M}}$ is an MC, we simply have
$\mathrm{PSem}_{{\mathcal{A}}}^{{\mathcal{M}}}(s)=\mathrm{Pr}_{s}\\{r\in\Omega_{s}:\ell(r)\in{\mathcal{L}}({\mathcal{A}})\\}$.

$s_{0},q_{0}$$({\sf m},q_{0})$$s_{1},q_{0}$$({\sf m},q_{0})$$({\sf
m},q_{1})$$s_{1},q_{1}$$({\sf m},q_{2})$$s_{f},q_{1}$$({\sf
m},q_{1})$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}:\$$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}:0$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\frac{1}{4}}:1$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\frac{1}{4}}:0$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\frac{1}{4}}:1$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\frac{1}{2}}:\$$
Figure 4: An example of a product MDP ${\mathcal{M}}\times{\mathcal{S}}_{1}$
with initial state $(s_{0},q_{0})$ and
$F^{\times}=\\{(s_{1},q_{1}),(s_{f},q_{1})\\}$ where ${\mathcal{M}}$ is the
MDP (MC) in Figure 3 and ${\mathcal{S}}_{1}$ is the safety NBA from Figure 2.
The maximum chance for the product MDP of generating a word in
${\mathcal{L}}(\mathcal{S}_{1})={\mathcal{L}}_{n}^{s}$ is $\frac{1}{8}$.

The _product_ of ${\mathcal{M}}$ and ${\mathcal{A}}$ is an MDP
${\mathcal{M}}\times{\mathcal{A}}=\langle S\times Q,{\mathsf{Act}}\times
Q,{\sf P}^{\times},\Sigma,\ell^{\times}\rangle$ augmented with the initial
state $(s_{0},q_{0})$ and the Büchi acceptance condition
$F^{\times}=\\{(s,q)\in S\times Q\;|\;q\in F\\}$. The labelling function
$\ell^{\times}$ maps each transition $\big{(}(s,q),({\sf
m},q^{\prime}),(s^{\prime},q^{\prime})\big{)}$ to $\ell\big{(}(s,{\sf
m},s^{\prime})\big{)}$.

We define the partial function ${\sf P}^{\times}:(S\times
Q)\times({\mathsf{Act}}\times Q)\mathrel{\ooalign{\hfil$\mapstochar\mkern
5.0mu$\hfil\cr$\to$\cr}}\mathrm{Distr}(S\times Q)$ as follows: for all
$(s,{\sf m})\in{\mathsf{support}}({\sf P})$, $s^{\prime}\in S$ and
$q,q^{\prime}\in Q$, we have

${\sf P}^{\times}\big{(}(s,q),({\sf
m},q^{\prime}),\sigma\big{)}\big{(}(s^{\prime},q^{\prime})\big{)}=\left\\{\begin{array}[]{ll}{\sf
P}(s,{\sf m},\sigma)(s^{\prime})&\mbox{if $q^{\prime}\in\delta(q,\sigma)$}\\\
0&\mbox{otherwise.}\end{array}\right.$

We define the syntactic satisfaction probability for the product MDP and a
strategy $\mu^{\times}$ from a state $(s,q)$ as:
$\mathrm{PSyn}_{{\mathcal{A}}}^{{\mathcal{M}}}\big{(}(s,q),\mu^{\times}\big{)}=\mathrm{Pr}_{s,q}^{\mu^{\times}}\\{r\in\Omega_{s,q}^{\mu^{\times}}:\ell^{\times}(r)\in{\mathcal{L}}({\mathcal{A}})\\}$666Let
$\mathrm{inf}(r)$ be the set of states that appears infinite often in a run
$r$. We also have
$\mathrm{PSyn}_{{\mathcal{A}}}^{{\mathcal{M}}}((s,q),\mu^{\times})=\mathrm{Pr}_{s,q}^{\mu^{\times}}\\{r\in\Omega_{s,q}^{\mu^{\times}}:\mathrm{inf}(r)\cap
F^{\times}\neq\emptyset\\}$. and
$\mathrm{PSyn}_{{\mathcal{A}}}^{{\mathcal{M}}}(s)=\sup_{\mu^{\times}}(\mathrm{PSyn}_{{\mathcal{A}}}^{{\mathcal{M}}}\big{(}(s,q_{0}),\mu^{\times})\big{)}$.
The set of actions is ${\mathsf{Act}}$ in the MDP ${\mathcal{M}}$ while it is
${\mathsf{Act}}\times Q$ in the product MDP. This makes $\mathrm{PSem}$ and
$\mathrm{PSyn}$ potentially different. In general,
$\mathrm{PSyn}_{{\mathcal{A}}}^{{\mathcal{M}}}(s)\leq\mathrm{PSem}_{{\mathcal{A}}}^{{\mathcal{M}}}(s)$
for all $s\in S$, because accepting runs can only occur on accepted words. If
${\mathcal{A}}$ is deterministic,
$\mathrm{PSyn}_{{\mathcal{A}}}^{{\mathcal{M}}}(s)=\mathrm{PSem}_{{\mathcal{A}}}^{{\mathcal{M}}}(s)$
holds for all $s\in S$.

End-components and runs are defined for products just like for MDPs. A run of
${\mathcal{M}}\times{\mathcal{A}}$ is accepting if it satisfies the product’s
acceptance condition. An accepting end-component of
${\mathcal{M}}\times{\mathcal{A}}$ is an end-component which contains some
states in $F^{\times}$.

######  Definition 2.1.

[6] An NBA ${\mathcal{A}}$ is good-for-MDPs (GfM) if, for all finite MDPs
${\mathcal{M}}$ with initial state $s_{0}$,
$\mathrm{PSyn}_{{\mathcal{A}}}^{{\mathcal{M}}}(s_{0})=\mathrm{PSem}_{{\mathcal{A}}}^{{\mathcal{M}}}(s_{0})$
holds.

An example of a product MDP is presented in Figure 4. It is the product of the
MC in Figure 3 and the safety NBA in Figure 2. Note that we have omitted
rejecting sink states, so that some outgoing probabilities do not sum up to
$1$. The chance that the MC produces a word in
${\mathcal{L}}_{1}^{s}={\mathcal{L}}(\mathcal{S}_{1})$ recognised by the
automaton from Figure 2 is $\frac{1}{4}$. However, the syntactic satisfaction
probability
$\mathrm{PSyn}_{\mathcal{S}_{1}}^{{\mathcal{M}}}(s_{0})=\frac{1}{8}$ is
witnessed by the memoryless strategy that chooses the action $({\sf m},q_{1})$
at the state $(s_{1},q_{0})$. We do not need to specify the strategy for the
other states since there is only one available action for any remaining state.
According Definition 2.1, the reachability NBA $\mathcal{S}_{1}$ in Figure 2
is not GfM as witnessed by the MC in Figure 3.

##  3 Outline

To establish our main result that

> GfM automata are exponentially more succinct than GfG automata,

we proceed in three steps. We first recall the standard result that NFAs are
exponentially more succinct than deterministic finite automata (DFAs), and use
a textbook example of a family of languages that witnesses this, namely

${\mathcal{L}}_{n}=\\{0,1\\}^{*}1\\{0,1\\}^{n-1}\$\ ,$

the language of those words $w\in\\{0,1\\}^{*}\$$, where the
$n^{\mbox{\scriptsize th}}$ letter before $\$$ in $w$ is $1$. NFAs that
recognise this language need $n+2$ states, while DFAs need $>2^{n}$.

In a second step, we then build an NBA from the standard NFA for this language
that recognises the $\omega$-language of infinite words that contain
infinitely many sequences of the form $1\,\\{0,1\\}^{n-1}\$$, such that the
resulting automaton has the same states as the NFA, and almost the same
structure (cf. Figures 5 and 6). We call this language
${\mathcal{L}}_{n}^{\omega}$ and show that the resulting NBA that recognises
it is GfM.

This $\omega$-language proves to have many useful properties:

  * •

it is Büchi recognisable (i.e. recognised by a _deterministic_ Büchi
automaton) and

  * •

it is a tail language, such that all reachable states of a DBA recognising it
are language equivalent and complete.

It is indeed easy to obtain a DBA that recognises ${\mathcal{L}}_{n}^{\omega}$
from a DFA that recognises ${\mathcal{L}}_{n}$ in the same way as we obtained
a (GfM) NBA for the NFA that recognises ${\mathcal{L}}_{n}$.

For our third and final step we observe that, should the resulting DBA be
minimal—or should a minimal DBA be broadly of the same size—then we are
essentially done: a minimal DBA would be exponential in the size of the
minimal GfM NBA, and using that GfG NBA are only quadratically more succinct
than DBAs [8], our main result would follow.

The heavy lifting we need to do is therefore to establish just this: that a
minimal DBA that recognises ${\mathcal{L}}_{n}^{\omega}$ cannot be
significantly smaller than a minimal DFA that recognises ${\mathcal{L}}_{n}$.

After having established our main result, we also show that general
nondeterministic automata are exponentially more succinct than good-for-MDP
automata. This even holds when the languages are restricted to reachability or
safety languages, and indeed if the automata are restricted to unambiguous
reachability automata or separating safety automata.

The languages we use to demonstrate this are the extension of
${\mathcal{L}}_{n}$ to reachability,

${\mathcal{L}}_{n}^{r}=\\{w\\{0,1,\$\\}^{\omega}\mid w\in{\mathcal{L}}_{n}\\}\
.$

Instead of using its safety closure,

${\mathcal{L}}_{n}^{\prime}={\mathcal{L}}_{n}^{r}\cup\\{0,1\\}^{\omega}\ ,$

we use the safety language

${\mathcal{L}}_{n}^{s}=\\{w\$^{\omega}\mid
w\in{\mathcal{L}}_{n}\\}\cup\\{0,1\\}^{\omega}\ ,$

because this translates more natural into a separating automaton.

We show that ${\mathcal{L}}_{n}^{r}$ resp. ${\mathcal{L}}_{n}^{s}$ are
recognised by a nondeterministic reachability resp. safety automaton with
$n+2$ states, while we show that a GfM automaton for these languages needs to
have $2^{n}$ states, not counting accepting or rejecting sinks.

We then obtain the refined results by showing that the safety automaton is
separating, while the reachability automaton is unambiguous. We finally show
that the reachability language ${\mathcal{L}}_{n}^{r}$ can be recognised by a
separating NBA $\mathcal{R}_{n}^{\prime}$; however, this automaton is not, and
cannot be, a reachability automaton.

##  4 GfM vs GfG

###  4.1 The language ${\mathcal{L}}_{n}^{\omega}$ and the GfM NBA
${\mathcal{G}}_{n}$

For an arbitrary $n\in{\rm Nature}$, define the language

${\mathcal{L}}_{n}=\\{w\in\\{0,1\\}^{*}\$\mid\text{ the $n^{\mbox{\scriptsize
th}}$ letter before $\$$ in $w$ is $1$}\\}\ ,$

where we assume for clarity that all words of length $\leq n$ are not in
${\mathcal{L}}_{n}$.

######  Claim 1.

For any $n$, there is an NFA with $n+2$ states recognising
${\mathcal{L}}_{n}$.

Let $\Sigma=\\{0,1,\$\\}$. Define the NFA
${\mathcal{A}}_{n}=(\Sigma,Q,q_{0},\delta_{\mathcal{A}},\\{f\\})$ where
$Q=\\{q_{0},\ldots,q_{n},f\\}$ and $\delta_{\mathcal{A}}$ is defined as
follows: $\delta_{\mathcal{A}}(q_{0},0)=\\{q_{0}\\}$;
$\delta_{\mathcal{A}}(q_{0},1)=\\{q_{0},q_{1}\\}$;
$\delta_{\mathcal{A}}(q_{i},\sigma)=\\{q_{i+1}\\}$ for all
$i\in\\{1,\ldots,n-1\\}$ and $\sigma\in\\{0,1\\}$;
$\delta_{\mathcal{A}}(q_{n},\$)=\\{f\\}$.

$q_{0}$$q_{1}$$q_{2}$$q_{3}$$\ldots$$q_{n}$$f$$0,1$$1$$0,1$$0,1$$\$$ Figure 5:
The NFA ${\mathcal{A}}_{n}$ that recognises ${\mathcal{L}}_{n}$.
$q_{0}$$q_{1}$$q_{2}$$q_{3}$$\ldots$$q_{n}$$f$$0,1,\$$$1$$0,1$$\$$$0,1$$\$$$\$$$\$$$0,1$$0,1,\$$
Figure 6: The NBA ${\mathcal{G}}_{n}$ that recognises
${\mathcal{L}}_{n}^{\omega}$.

Since it is a standard textbook language, we give the following theorem
without proof. The intuition is that a DFA needs to store the previous $n$
letters in their order of occurrence in order to recognise this language.

######  Theorem 4.1.

For all $n$, any DFA recognising ${\mathcal{L}}_{n}$ must have at least
$2^{n}$ states.

######  Claim 2.

For any $n$, there is an NBA with $n+2$ states recognising
${\mathcal{L}}_{n}^{\omega}$.

Define the NBA ${\mathcal{G}}_{n}=(\Sigma,Q,q_{0},\delta,\\{f\\})$ where
$Q=\\{q_{0},\ldots,q_{n},f\\}$ and $\delta$ is defined as follows:
$\delta(q_{0},0)=\\{q_{0}\\}$; $\delta(q_{0},1)=\\{q_{0},q_{1}\\}$;
$\delta(q_{i},\sigma)=\\{q_{i+1}\\}$ for all $i\in\\{1,\ldots,n-1\\}$ and
$\sigma\in\\{0,1\\}$; $\delta(q_{n},\$)=\\{f\\}$;
$\delta(q_{n},\sigma)=\\{q_{0}\\}$ for $\sigma\in\\{0,1\\}$;
$\delta(f,0)=\\{q_{0}\\}$; $\delta(f,1)=\\{q_{0}\\}$;
$\delta(q,\$)=\\{q_{0}\\}$ for all $q_{n}\neq q\in Q$.

${\mathcal{G}}_{n}$ is obtained from ${\mathcal{A}}_{n}$ by returning to
$q_{0}$ whenever the resulting automaton would block. The intuition why
${\mathcal{G}}_{n}$ is GfM is that, if there is any sequence in
${\mathcal{L}}_{n}$ in an BSCC777A strongly connected component (SCC) is a
maximally strongly connected set of states. A bottom SCC (BSCC) is an SCC from
which no state outside it is reachable. of a Markov chain, then it can almost
surely try infinitely often to facilitate it for acceptance. Each of these
attempts will succeed with a positive probability $p>0$, so that almost surely
infinitely many of these infinite attempts will succeed.

######  Lemma 4.2.

${\mathcal{G}}_{n}$ recognises ${\mathcal{L}}_{n}^{\omega}$.

######  Proof 4.3.

‘${\mathcal{L}}({\mathcal{G}}_{n})\subseteq{\mathcal{L}}_{n}^{\omega}$’: It is
easy to see that by the construction of ${\mathcal{G}}_{n}$, to visit $f$
infinitely often, ${\mathcal{G}}_{n}$ has to take the path
$q_{0},1,q_{1},\sigma_{1},q_{2},\ldots,q_{n},\$,f$ on the word
$1\sigma_{1}\cdots\sigma_{n-1}\$\in{\mathcal{L}}_{n}$ where
$\sigma_{i}\in\\{0,1\\}$ for all $i\in\\{1,\ldots,n-1\\}$ infinitely often.

‘${\mathcal{L}}_{n}^{\omega}\subseteq{\mathcal{L}}({\mathcal{G}}_{n})$’: We
only need to show there is an accepting run of ${\mathcal{G}}_{n}$ on any word
in ${\mathcal{L}}_{n}^{\omega}$. A word $w\in{\mathcal{L}}_{n}^{\omega}$ is of
the form $w_{1}w_{1}^{\prime}w_{2}w_{2}^{\prime}w_{3}w_{3}^{\prime}\ldots$
such that, for all $i\in{\rm Nature}$, $w_{i}\in\\{0,1,\$\\}^{*}$ and
$w_{i}^{\prime}\in{\mathcal{L}}_{n}$. Let $w_{i}^{\prime}=u_{i}1v_{i}$ where
$u_{i}\in\\{0,1\\}^{*}$ and $v_{i}\in\\{0,1\\}^{n-1}\$$ for all $i>0$. We can
build the run as follows.

For odd indices $i$, ${\mathcal{G}}_{n}$ always stays in $q_{0}$ on
$w_{i}u_{i}$, transitions to $q_{1}$ on $1$ and to $f$ on $v_{i}$; (at the
beginning, ${\mathcal{G}}_{n}$ starts from $q_{0}$ and stays in $q_{0}$ on
$w_{1}u_{1}$, transitions to $q_{1}$ on $1$ and to $f$ on $v_{1}$.) For even
indices $i$, ${\mathcal{G}}_{n}$ starts from the state $f$, then traverses to
$q_{0}$ and stays in $q_{0}$ on $w_{i}w_{i}^{\prime}$.

For every $w_{i}^{\prime}\in{\mathcal{L}}_{n}$ such that $i$ is odd, the run
we build will visit the accepting state $f$. As there are infinitely many such
$w_{i}^{\prime}$s, the run will visit the accepting state $f$ infinitely
often, and thus, is accepting.

######  Lemma 4.4.

${\mathcal{G}}_{n}$ is good for MDPs.

######  Proof 4.5.

Consider an arbitrary MC ${\mathcal{M}}$ with initial state $s_{0}$. We show
that ${\mathcal{G}}_{n}$ is good for ${\mathcal{M}}$, that is,
$\mathrm{PSem}_{{\mathcal{G}}_{n}}^{{\mathcal{M}}}(s_{0})=\mathrm{PSyn}_{{\mathcal{G}}_{n}}^{{\mathcal{M}}}(s_{0})$.
It suffices to show
$\mathrm{PSyn}_{{\mathcal{G}}_{n}}^{{\mathcal{M}}}(s_{0})\geq\mathrm{PSem}_{{\mathcal{G}}_{n}}^{{\mathcal{M}}}(s_{0})$
since by definition the converse
$\mathrm{PSem}_{{\mathcal{G}}_{n}}^{{\mathcal{M}}}(s_{0})\geq\mathrm{PSyn}_{{\mathcal{G}}_{n}}^{{\mathcal{M}}}(s_{0})$
always holds.

First, we construct a language equivalent deterministic Büchi automaton (DBA)
${\mathcal{D}}_{n}$. We start with the NFA ${\mathcal{A}}_{n}^{\prime}$, see
Figure 7, which recognises the language $\\{w\in\\{0,1\\}^{*}\mid\text{ the
$n^{\mbox{\scriptsize th}}$ to the last letter in $w$ is $1$}\\}$. The NFA
${\mathcal{A}}_{n}^{\prime}$ is very similar to ${\mathcal{A}}_{n}$: it has
the same states $q_{i}$ for $i\in\\{0,\ldots,n\\}$ and the same transitions
between them; the only difference is that $q_{n}$ is accepting without any
outgoing transitions as there is no $f$ state in ${\mathcal{A}}_{n}^{\prime}$.
We then determinise ${\mathcal{A}}_{n}^{\prime}$ to a DFA
${\mathcal{B}}_{n}^{\prime}$ by a standard subset construction and then obtain
${\mathcal{B}}_{n}$ from ${\mathcal{B}}_{n}^{\prime}$ by adding a fresh $f$
state, adding a $\$$ transition from all accepting states to $f$ and making
$f$ the only accepting state. It is easy to see that ${\mathcal{B}}_{n}$ is
deterministic and
${\mathcal{L}}({\mathcal{A}}_{n})={\mathcal{L}}({\mathcal{B}}_{n})$. Now we
obtain the DBA ${\mathcal{D}}_{n}$ from the DFA ${\mathcal{B}}_{n}$ in the
same way as we obtain the NBA ${\mathcal{G}}_{n}$ from the NFA
${\mathcal{A}}_{n}$.

$q_{0}$$q_{1}$$q_{2}$$q_{3}$$\ldots$$q_{n}$$0,1$$1$$0,1$$0,1$ Figure 7: The
NFA ${\mathcal{A}}_{n}^{\prime}$, which recognises the language
$\\{w\in\\{0,1\\}^{*}\mid\text{ the $n^{\mbox{\scriptsize th}}$ to the last
letter in $w$ is $1$}\\}$.

Since ${\mathcal{L}}({\mathcal{G}}_{n})={\mathcal{L}}({\mathcal{D}}_{n})$, we
have that
$\mathrm{PSem}_{{\mathcal{G}}_{n}}^{{\mathcal{M}}}(s_{0})=\mathrm{PSem}_{{\mathcal{D}}_{n}}^{{\mathcal{M}}}(s_{0})$.
In addition, since ${\mathcal{D}}_{n}$ is deterministic, we have
$\mathrm{PSem}_{{\mathcal{D}}_{n}}^{{\mathcal{M}}}(s_{0})=\mathrm{PSyn}_{{\mathcal{D}}_{n}}^{{\mathcal{M}}}(s_{0})$.

It remains to show
$\mathrm{PSyn}_{{\mathcal{G}}_{n}}^{{\mathcal{M}}}(s_{0})\geq\mathrm{PSyn}_{{\mathcal{D}}_{n}}^{{\mathcal{M}}}(s_{0})$.
For that, it suffices to show that for an arbitrary accepting run $r$ of
${\mathcal{M}}\times{\mathcal{D}}_{n}$, there is a deterministic strategy for
${\mathcal{M}}\times{\mathcal{G}}_{n}$ such that $r^{\prime}$ (the
corresponding run in the product) is accepting in
${\mathcal{M}}\times{\mathcal{G}}_{n}$ where the projections of $r$ and
$r^{\prime}$ on ${\mathcal{M}}$ are the same.

Consider an accepting run of ${\mathcal{M}}\times{\mathcal{D}}_{n}$. Before
entering an accepting end-component of ${\mathcal{M}}\times{\mathcal{D}}_{n}$,
${\mathcal{G}}_{n}$ always stays in $q_{0}$. Once an accepting end-component
of ${\mathcal{M}}\times{\mathcal{D}}_{n}$ is entered, since its projection on
${\mathcal{D}}_{n}$ is an SCC in ${\mathcal{D}}_{n}$, there must exist a word
$w\in{\mathcal{L}}({\mathcal{B}}_{n})$ (and thus
$w\in{\mathcal{L}}({\mathcal{A}}_{n})$), which is a possible initial sequence
of letters produced from some state $m$ of
${\mathcal{M}}\times{\mathcal{D}}_{n}$ in this end-component. We fix such a
word $w$; such a state $m$ of the end-component in
${\mathcal{M}}\times{\mathcal{D}}_{n}$ from which this word $w$ can be
produced; and strategy of the NBW ${\mathcal{G}}_{n}$ to follow the word $w$
from $q_{0}$ to the accepting state $f$.

In an accepting end-component we can be in two modes: _tracking_ , or _not
tracking_. If we are _not tracking_ and reach $m$, we start to _track_ $w$: If
we are not in $q_{0}$, we move to _not tracking_. Otherwise, we use
${\mathcal{G}}_{n}$ to reach an accepting state after reading $w$ (ignoring
what happens in any other case) with the strategy we have fixed. Note that,
when starting from $m$, it is always possible, with a fixed probability $p>0$,
to read $w$ from $q_{0}$, and thus to accept. If we read an unexpected letter
(where the ‘expected’ letter is always the next letter from $w$) or the end of
the word $w$ is reached, we move to _not tracking_.

In the _not tracking_ mode, the strategy for ${\mathcal{G}}_{n}$ is to always
stay in $q_{0}$ when it is in $q_{0}$. Thus, ${\mathcal{G}}_{n}$ can always
re-set to the $q_{0}$ state. We do not need to specify actions for the other
states in ${\mathcal{G}}_{n}$ as they have only deterministic transitions.

Once in an accepting end-component of ${\mathcal{M}}\times{\mathcal{D}}_{n}$,
tracking is almost surely started infinitely often, and it is thus almost
surely successful infinitely often. Thus, we have
$\mathrm{PSyn}_{{\mathcal{G}}_{n}}^{{\mathcal{M}}}(s_{0})\geq\mathrm{PSyn}_{{\mathcal{D}}_{n}}^{{\mathcal{M}}}(s_{0})$.

###  4.2 The Marking Algorithm

We show that the DBA which recognises ${\mathcal{L}}_{n}^{\omega}$ is at least
$\frac{1}{n+2}$ times the size of the minimum DFA which recognises
${\mathcal{L}}_{n}$. To do that, we first present an algorithm which marks the
states of the DBA with finite words from $\Sigma^{+}$.

We assume that the input DBA is finite, complete and all states are reachable
from the initial state. It is a reasonable assumption, as we can see from
Lemma 4.6, a DBA which recognises ${\mathcal{L}}_{n}^{\omega}$ with all states
reachable from the initial state is complete. All states of
${\mathcal{D}}_{n}$ are complete because ${\mathcal{L}}_{n}^{\omega}$ is a
tail objective, an objective whose occurrence is independent of any finite
prefix.

######  Lemma 4.6.

Let ${\mathcal{D}}_{n}$ be a DBA that recognises ${\mathcal{L}}_{n}^{\omega}$.
Let all states in ${\mathcal{D}}_{n}$ are reachable from the initial state.
The DBA ${\mathcal{D}}_{n}$ is complete.

######  Proof 4.7.

Assume for contradiction that the state $q$ in ${\mathcal{D}}_{n}$ is not
complete and is missing a $\sigma$-transition where
$\sigma\in\Sigma=\\{0,1,\$\\}$. Since all states are reachable, there is a
finite word $w$ that takes the initial state to $q$. All infinite words that
start with $w\sigma$ will be rejected by ${\mathcal{D}}_{n}$. For any infinite
word $w^{\prime}\in{\mathcal{L}}_{n}^{\omega}$ that begins with $\sigma$, the
infinite word $ww^{\prime}$ should also be in ${\mathcal{L}}_{n}^{\omega}$.
However, $ww^{\prime}$ is rejected by ${\mathcal{D}}_{n}$; hence, the
contradiction.

For an arbitrary $n\in{\rm Nature}$, define the language

$\Gamma_{n}=\\{w\in\\{0,1\\}^{*}\$\mid\text{ the $n^{\mbox{\scriptsize th}}$
letter before $\$$ in $w$ is $0$}\\}\ .$

We have $\Gamma_{n}$ is a subset of the complement language of
${\mathcal{L}}_{n}$, that is,
$\Gamma_{n}\subseteq\Sigma^{*}\setminus{\mathcal{L}}_{n}$. Same as
${\mathcal{L}}_{n}$, all words in $\Gamma_{n}$ are at least of length $n+1$.

Here comes the marking algorithm for a DBA ${\mathcal{D}}_{n}$ which
recognises ${\mathcal{L}}_{n}^{\omega}$:

Input: A complete DBA ${\mathcal{D}}_{n}$ which recognises
${\mathcal{L}}_{n}^{\omega}$ and an empty marking function
$V:Q^{\mathcal{D}}\mathrel{\ooalign{\hfil$\mapstochar\mkern
5.0mu$\hfil\cr$\to$\cr}}\Sigma^{+}$

Output: A (partial) marking function
$V:Q^{\mathcal{D}}\mathrel{\ooalign{\hfil$\mapstochar\mkern
5.0mu$\hfil\cr$\to$\cr}}\Sigma^{+}$

1 Mark all final states with $0$, that is, $V(q)=0$ for all $q\in
Q^{\mathcal{D}}_{f}$;

2 For every unmarked state $q$ from which a final state can be reached through
a word $w\in\\{0,1\\}^{+}$, fix such a word $w_{q}$ and mark it with this
word, that is, $V(q)=w_{q}$;

3 For every unmarked state $q$ from which a marked state can be reached
through a word $w\in\Gamma_{n}$, fix such a word $w_{q}$ and mark it with this
word, that is, $V(q)=w_{q}$.

Algorithm 1 Marking Algorithm for DBA

Given an empty marking function and a finite, complete DBA in which all states
are reachable from the initial state, the marking algorithm proceeds in three
simple steps. It first marks all final states with the letter $0$ on line 1.
Next, it marks all states that can reach the final states by going through a
finite word of only $0$s and $1$s with that word on line 2. Finally, it marks
one by one the state that can reach any already marked state via a word in
$\Gamma_{n}$ with that word. As there are only finitely many states in the
input DBA, the marking algorithm always terminates.

###  4.3 GfM More Succinct Than GfG

In this section, we show that GfM NBA is exponentially more succinct than GfG
NBA. We show that, in the marked DBA output by Algorithm 1, there must be some
states that are unmarked. We produce a new DFA, $\mathcal{P}$, by collapsing
all marked states into a single accepting sink without any outgoing
transitions. In $\mathcal{P}$, the unmarked states and the transitions between
them are the same as the original marked DBA. We then show that $\mathcal{P}$
is at least $\frac{1}{n+2}$ times the number of states as the DFA which
recognises ${\mathcal{L}}_{n}$.

Let the input DBA be
${\mathcal{D}}_{n}=(\Sigma,Q^{\mathcal{D}},q_{0}^{\mathcal{D}},\delta^{{\mathcal{D}}},Q_{f}^{{\mathcal{D}}})$.
When the algorithm terminates, a state $q$ is unmarked if $V(q)$ is undefined.
We first show an important property of the algorithm:

######  Lemma 4.8.

After line 2 and after line 3, we have for every unmarked state $q$ that
$\delta^{{\mathcal{D}}}(q,0)$ and $\delta^{{\mathcal{D}}}(q,1)$ are unmarked.

######  Proof 4.9.

It is easy to see that, for a state $q$ that is unmarked after executing line
2, all finite word $w\in\\{0,1\\}^{+}$ will take $q$ to unmarked states only.
Otherwise, assume for contradiction that $q$ reaches a marked state
$q^{\prime}$ on a finite word $w\in\\{0,1\\}^{+}$, we have two cases:

  * •

If $q^{\prime}$ is final, $q$ should be marked on line 2.

  * •

If $q^{\prime}$ is marked with $V(q^{\prime})$ on line 2, then $q$ will reach
a final state on $wV(q^{\prime})$, and $q$ should also be marked on line 2.

Now we prove for a state $q$ which remains unmarked after line 3, both
$\delta^{{\mathcal{D}}}(q,0)$ and $\delta^{{\mathcal{D}}}(q,1)$ are unmarked.
Assume for contradiction $q^{\prime}=\delta^{{\mathcal{D}}}(q,0)$ is marked.
We distinguish the following two cases.

  * •

If $q^{\prime}$ is marked after executing line 2, a final state is reached
through the finite word $V(q^{\prime})\in\\{0,1\\}^{+}$ from $q^{\prime}$.
Thus, a final state is reached through the finite word
$0V(q^{\prime})\in\\{0,1\\}^{+}$ from $q$, which is a contradiction as $q$
should be marked on line 2.

  * •

Otherwise, $q^{\prime}$ is unmarked after executing line 2, it is then marked
on line 3. A marked state is reached through the finite word
$V(q^{\prime})\in\Gamma_{n}$ from $q^{\prime}$. Thus, the same marked state is
reached through the finite word the finite word $0V(q^{\prime})\in\Gamma_{n}$
from $q$, then $q$ should be marked on line 3, which again is a contradiction.

Similarly, we can show by contradiction that $\delta^{{\mathcal{D}}}(q,1)$ is
also unmarked.

When the algorithm terminates, we have a partial marking function such that a
state of the DBA is either marked with a finite word $w\in\Sigma^{+}$ or
unmarked. Lemma 4.8 tells us that in the marked DBA, on any word from
$\\{0,1\\}^{+}$ any unmarked states will only go through unmarked states on
the way. We show in the next lemma that there must be some unmarked states.

######  Lemma 4.10.

There exist states $q$ such that $V(q)$ is undefined.

######  Proof 4.11.

Assume for contradiction that all states are marked, that is,
$V(q)\in\Sigma^{+}$ for all $q\in Q^{\mathcal{D}}$. We successively build an
infinite word which consists of a sequence of finite words. While we are
building this infinite word, we also build the run of ${\mathcal{D}}_{n}$ on
this word. We start with the finite word $V(q_{0}^{\mathcal{D}})$ where
$q_{0}^{\mathcal{D}}$ is the initial state. The selection of subsequent finite
words is based on the end state that is reached in the run sequence that
${\mathcal{D}}_{n}$ produces when traversing the input word $w$: for state
$q$, we use $V(q)$ where $q=\delta^{\mathcal{D}}(q_{0}^{\mathcal{D}},w)$ and
$w$ is the word we have built before adding $V(q)$.

It is not hard to see that the infinite word we have built does not belong to
${\mathcal{L}}_{n}^{\omega}$ as it does not contain any finite word in
${\mathcal{L}}_{n}$. We show that the run on this word, however, is accepting
in ${\mathcal{D}}_{n}$, which contradicts that ${\mathcal{D}}_{n}$ recognises
${\mathcal{L}}_{n}^{\omega}$.

Let
$w=V(q_{0}^{\mathcal{D}})V(q_{1}^{\mathcal{D}})V(q_{2}^{\mathcal{D}})\ldots$
be the infinite word we have built. Let the prefix be
$w_{i}=V(q_{0}^{\mathcal{D}})\ldots V(q_{i}^{\mathcal{D}})$ for $i\geq 0$ and
$q_{i}^{\mathcal{D}}=\delta(q_{0}^{\mathcal{D}},w_{i-1})$ for $i>0$. The run
of ${\mathcal{D}}_{n}$ on $w$ will visit all states $q_{i}^{{\mathcal{D}}}$
for $i\geq 0$. If there are infinitely many indices $i$ such that
$q_{i}^{{\mathcal{D}}}$ is final, the run is accepting. Otherwise, there are
only finitely many indices $i$ such that $q_{i}^{{\mathcal{D}}}$ is final. We
distinguish the following two cases:

  * •

Assume that we have infinitely many indices $i$ such that
$q_{i}^{{\mathcal{D}}}$ is marked on line 2 of Algorithm 1. We have that
$q_{i+1}^{{\mathcal{D}}}$ is final by running from $q_{i}^{{\mathcal{D}}}$ on
the finite word $V(q_{i}^{{\mathcal{D}}})$, which contradicts the assumption
that we only have finitely many indices $i$ such that $q_{i}^{{\mathcal{D}}}$
is final.

  * •

Assume that starting from some positive index $i$, we only have states
$q_{i}^{{\mathcal{D}}}$ that are marked on line 3 of Algorithm 1. Since the
input DBA is finite, there must exist indices $j$ and $k$ such that $i<j<k$
and $q_{j}^{{\mathcal{D}}}=q_{k}^{{\mathcal{D}}}$. For each index $x$ such
that $j\leq x<k$, we have
$q_{x+1}^{{\mathcal{D}}}=\delta\big{(}q_{x}^{{\mathcal{D}}},V(q_{x}^{{\mathcal{D}}})\big{)}$
and $q_{x+1}^{{\mathcal{D}}}$ must be marked before $q_{x}^{{\mathcal{D}}}$
when running line 3 of Algorithm 1. This implies $q_{k}^{{\mathcal{D}}}$ is
marked before $q_{j}^{{\mathcal{D}}}$, which leads to the desired
contradiction as they are the same state.

After Algorithm 1 terminates, there must be some states that are marked, as
all final states in $Q^{{\mathcal{D}}}_{f}$ are marked on line 1. The set of
final states $Q^{{\mathcal{D}}}_{f}$ could not be empty, otherwise
${\mathcal{L}}({\mathcal{D}}_{n})=\emptyset\neq{\mathcal{L}}_{n}^{\omega}$.
There also must be some unmarked states by Lemma 4.10. We produce a new
automaton, $\mathcal{P}$, by collapsing all marked states into a single
accepting sink without any outgoing transitions. We treat $\mathcal{P}$ as a
DFA.

We show two important properties of $\mathcal{P}$. First, we show a property
that holds for all states in $\mathcal{P}$, that is, for all states $q$ in
$\mathcal{P}$, $\mathcal{P}_{q}$ rejects all words in $\Gamma_{n}$.

######  Lemma 4.12.

For all states $q$ in the automaton $\mathcal{P}$ and all words $w$ in
$\Gamma_{n}$, $\mathcal{P}_{q}$ rejects $w$.

######  Proof 4.13.

Let $q$ be a state in the automaton $\mathcal{P}$. Let $w$ be a word in
$\Gamma_{n}$. Towards contradiction, we assume $\mathcal{P}_{q}$ accepts $w$.
The sink state of $\mathcal{P}$ is reached through $w$ from $q$. Then, in the
marked DBA ${\mathcal{D}}_{n}$, a marked state $q^{\prime}$ is reached through
$w$ from the unmarked state $q$. The $q^{\prime}$ state could be final (marked
on line 1), or non-final (marked on line 2 or 3). We have:

  * •

Assume $q^{\prime}$ is final. The state $q^{\prime}$ should be marked on line
1. Since a final state is reached through $w\in\Gamma_{n}$, $q$ should be
marked on line 3, which contradicts that $q$ is unmarked.

  * •

Assume $q^{\prime}$ is marked on line 2 or 3. Since a marked state is reached
through $w\in\Gamma_{n}$, $q$ should be marked on line 3, which contradicts
that $q$ is unmarked.

Next, we show a property which holds for some state in $\mathcal{P}$, that is,
there is a state $q$ in the automaton $\mathcal{P}$ such that
$\mathcal{P}_{q}$ accepts all words in ${\mathcal{L}}_{n}$.

######  Lemma 4.14.

There is a state $q$ in $\mathcal{P}$ such that for all
$w\in{\mathcal{L}}_{n}$, $\mathcal{P}_{q}$ accepts $w$.

######  Proof 4.15.

Towards contradiction, we assume that for all unmarked state $q$ in
$\mathcal{P}$ (every state but the sink), there is a finite word
$w_{q}\in{\mathcal{L}}_{n}$ that is rejected by $\mathcal{P}_{q}$. By Lemma
4.8 and the assumption $\mathcal{P}_{q}$ rejects $w_{q}$, we have that the
automaton $\mathcal{P}_{q}$ not only traverses through unmarked states but
also ends in an unmarked state. Using the words $w_{q}$ for all $q$ in
$\mathcal{P}$, we build an infinite word. We show that this word is in
${\mathcal{L}}_{n}$ but is rejected by ${\mathcal{D}}_{n}$. Similar to the
proof of Lemma 4.10, we successively build this infinite word which consists
of a sequence of finite words.

We start with $q_{0}^{\mathcal{D}}$. If $q_{0}^{\mathcal{D}}$ is marked in the
DBA, we select $w_{q_{0}^{\mathcal{D}}}$ as the first finite word such that
$\delta^{{\mathcal{D}}}(q_{0}^{\mathcal{D}},w_{q_{0}^{\mathcal{D}}})$ is
unmarked. Such a word must exist, otherwise as ${\mathcal{D}}_{n}$ is
complete, all states are marked, which contradicts Lemma 4.6. If
$q_{0}^{\mathcal{D}}$ is not marked in the DBA and $w_{q_{0}^{\mathcal{D}}}$
is defined, we select $w_{q_{0}^{\mathcal{D}}}$ as the first finite word. The
selection of subsequent finite words is based on the end state that is reached
in the run sequence that ${\mathcal{D}}_{n}$ produces when traversing the
input word $w$: for state $q$, we use $w_{q}$ where
$q=\delta^{\mathcal{D}}(q_{0}^{\mathcal{D}},w)$ and $w$ is the word we have
built before adding $w_{q}$.

The infinite word we have built belongs to ${\mathcal{L}}_{n}^{\omega}$ as it
contains infinite many finite words from ${\mathcal{L}}_{n}$. As we argued
before, after reaching the first unmarked state, the run visits only unmarked
states via the selected words from ${\mathcal{L}}_{n}$. Thus, the run on the
infinite word we built is rejecting in ${\mathcal{D}}_{n}$, as we visit no
final states after we traverse the prefix $w_{q_{0}^{\mathcal{D}}}$, which
contradicts that ${\mathcal{D}}_{n}$ recognises ${\mathcal{L}}_{n}^{\omega}$.

With Lemma 4.12 and Lemma 4.14, we have our main theorem which gives a lower
bound of the size of $\mathcal{P}$.

######  Theorem 4.16.

The DFA $\mathcal{P}$ is at least $\frac{1}{n+2}$ times the size of the
minimum DFA which recognises ${\mathcal{L}}_{n}$.

######  Proof 4.17.

According to Lemma 4.14, there exists a state $q$ such that $\mathcal{P}_{q}$
accepts all words in ${\mathcal{L}}_{n}$. By Lemma 4.12, we also have
$\mathcal{P}_{q}$ rejects all words in $\Gamma_{n}$. Let ${\mathcal{C}}_{n}$
be the DFA which recognises the language $(0,1)^{n}(0,1)^{*}\$$. The DFA
${\mathcal{C}}_{n}$ (shown in Figure 8) has $n+2$ states.

$q_{0}$$q_{1}$$q_{2}$$q_{3}$$\ldots$$q_{n}$$f$$0,1$$0,1$$0,1$$0,1$$\$$ Figure
8: The DFA $\mathcal{C}_{n}$ which recognises the language
$(0,1)^{n}(0,1)^{*}\$$.

We have
${\mathcal{L}}(P_{q})\cap{\mathcal{L}}({\mathcal{C}}_{n})={\mathcal{L}}_{n}$.
This is because:

  * •

Any word $w$ in ${\mathcal{L}}_{n}$ is obviously in
${\mathcal{L}}({\mathcal{C}}_{n})$, and in ${\mathcal{L}}(\mathcal{P}_{q})$ by
Lemma 4.14;

  * •

Any word $w$ in the intersection of ${\mathcal{L}}(P_{q})$ and
${\mathcal{L}}({\mathcal{C}}_{n})$ must be in the language $\\{0,1\\}^{+}\$$
and have length at least $n+1$. Also, the $n^{\mbox{\scriptsize th}}$ letter
before $\$$ in $w$ must be $1$. If the $n^{\mbox{\scriptsize th}}$ letter is
$0$, it follows that the word is in $\Gamma_{n}$, which contradicts that
$\mathcal{P}_{q}$ rejects all words in $\Gamma_{n}$. Thus,
$w\in{\mathcal{L}}_{n}$.

We can construct a DFA which accepts
${\mathcal{L}}(P_{q})\cap{\mathcal{L}}({\mathcal{C}}_{n})$, thus
${\mathcal{L}}_{n}$, by intersecting $\mathcal{P}_{q}$ and
${\mathcal{C}}_{n}$. The resulting DFA then has $n+2$ times as many states as
$\mathcal{P}_{q}$, and thus at most $n+2$ times the number of states as
$\mathcal{P}$. Hence, $\mathcal{P}$ is at least $\frac{1}{n+2}$ times the size
of the minimum DFA which recognises ${\mathcal{L}}_{n}$.

The DFA which recognises ${\mathcal{L}}_{n}$ should have at least $2^{n}$
states by Theorem 4.1. By Theorem 4.16, the automaton $\mathcal{P}$ should
have at least $\frac{2^{n}}{n+2}$ states. This implies the simple corollary
that ${\mathcal{D}}_{n}$ is at least as big as $\mathcal{P}$, and thus has at
least $\frac{2^{n}}{n+2}$ states.

######  Corollary 4.18.

${\mathcal{D}}_{n}$ has at least $\frac{2^{n}}{n+2}$ states.

Noting that ${\mathcal{D}}_{n}$ can be chosen minimal, it is now easy to infer
that GfM Büchi automata are exponentially more succinct than DBA by using the
result that GfG Büchi automata are only up to quadratically more succinct than
DBA for the same language [8]. The size of GfG automata is therefore in
$\Omega(\sqrt{2^{n}/n})$ (or: $\Omega(2^{n/2}/\sqrt{n})$).

######  Corollary 4.19.

GfM Büchi automata are exponentially more succinct than GfG Büchi automata.

##  5 GfM vs General Nondeterminism

In this section, we show that general nondeterministic automata are
exponentially more succinct than GfM automata. As we can see in the following,
this even holds when the languages are restricted to reachability or safety
languages. Using the same languages and general NBAs, we also observe
unambiguous and separating automata are exponentially more succinct than GfM
automata. Missing proofs can be found in Appendix A.

The reachability languages we use are the extension of ${\mathcal{L}}_{n}$ to
reachability:

${\mathcal{L}}_{n}^{r}=\\{w\\{0,1,\$\\}^{\omega}\mid w\in{\mathcal{L}}_{n}\\}\
,$

the language of infinite words that contain at least one $\$$, as well as a
$1$ that occurs exactly $n$ letters before this first $\$$. In particular,
words where the first $\$$ is one of the first $n$ letters is not part of
${\mathcal{L}}_{n}^{r}$.

An NBA $\mathcal{R}_{n}$ that recognises ${\mathcal{L}}_{n}^{r}$ is shown in
Figure 9. The automaton is a reachability automaton as there is only one
accepting state, which is a sink.

$q_{0}$$q_{1}$$q_{2}$$q_{3}$$\ldots$$q_{n}$$f$$0,1$$1$$0,1$$0,1$$\$$$0,1,\$$
Figure 9: The reachability NBA $\mathcal{R}_{n}$ that recognises
${\mathcal{L}}_{n}^{r}$.

The safety languages we use are the safety closure of an extension of words in
${\mathcal{L}}_{n}$ by infintely many $\$$s:

${\mathcal{L}}_{n}^{s}=\\{w\$^{\omega}\mid
w\in{\mathcal{L}}_{n}\\}\cup\\{0,1\\}^{\omega}\ ,$

An NBA $\mathcal{S}_{n}$ that recognises ${\mathcal{L}}_{n}^{s}$ is shown in
Figure 10. The automaton is a safety automaton as all states are accepting.

$q_{0}$$q_{1}$$q_{2}$$q_{3}$$\ldots$$q_{n}$$0,1$$1$$0,1$$0,1$$\$$ Figure 10:
The safety NBA $\mathcal{S}_{n}$ that recognises ${\mathcal{L}}_{n}^{s}$.

Next, we show that a GfM automaton for these languages needs to have $2^{n}$
states, not counting accepting or rejecting sinks. For that, we construct a
family of Markov chains as shown in Figure 11. We show that for an automaton,
which recognises ${\mathcal{L}}_{n}^{r}$ or ${\mathcal{L}}_{n}^{s}$, to be
good for this family of Markov chains, it needs at least $2^{n}$ states.

$s_{0}$$s_{1}$$s_{2}$$s_{3}$$\ldots$$s_{n}$$s_{f}$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}:\sigma_{1}$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}:\sigma_{2}$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}:\sigma_{3}$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\frac{1}{4}}:0$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\frac{1}{4}}:1$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\frac{1}{2}}:\$$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}:\$$
Figure 11: A family of Markov chains, where
$\sigma_{1},\ldots,\sigma_{n}\in\\{0,1\\}$. For a Markov chain with fixed
values of $\sigma_{1},\ldots,\sigma_{n}$, the chance that it produces a word
in ${\mathcal{L}}_{n}^{r}$ (and ${\mathcal{L}}_{n}^{s}$) is
$2^{-(n+1)}+\sum_{i=1}^{n}\sigma_{i}2^{-i}$. This is also the value that the
product from the automaton state and $s_{n}$ has when $s_{n}$ is first
reached. Thus, $s_{n}$ must be reached with different states of a GfM
automaton that recognises ${\mathcal{L}}_{n}^{r}$ (or ${\mathcal{L}}_{n}^{s}$)
that resolves its nondeterminism optimally for different parameters
$\sigma_{1},\ldots,\sigma_{n}$, and there are $2^{n}$ combinations.

######  Theorem 5.1.

A GfM automaton that recognises ${\mathcal{L}}_{n}^{r}$ or
${\mathcal{L}}_{n}^{s}$ has at least $2^{n}$ states.

######  Proof 5.2.

Let $n>0$ and $\sigma_{1},\ldots,\sigma_{n}\in\\{0,1\\}$. The family of Markov
chains is shown in Figure 11. Since there are $2^{n}$ combinations of
$\sigma_{1},\ldots,\sigma_{n}$, we have $2^{n}$ Markov chains in this family.

The chance that a Markov chain in this family produces a word in
${\mathcal{L}}_{n}^{r}$ (and ${\mathcal{L}}_{n}^{s}$) is
$2^{-(n+1)}+\sum_{i=1}^{n}\sigma_{i}2^{-i}$. We briefly explain how we obtain
this value. The chance that the first $\$$ is $i\leq n$ steps after reaching
$s_{n}$ is $2^{-i}$, and the relative chance of winning then is
$\sigma_{i}2^{-i}$; this is the $\sum_{i=1}^{n}\sigma_{i}2^{-i}$ part. The
chance that there never is a $\$$ is $0$. The chance that there is a $\$$
after $>n$ steps after reaching $s_{n}$ is $2^{-n}$. The chance of winning in
this case is $\frac{1}{2}$ (as a $0$ and $1$ exactly $n$ steps earlier are
equally likely); this is the $2^{-(n+1)}$ part.

Let ${\mathcal{G}}$ be a GfM automaton that recognises ${\mathcal{L}}_{n}^{r}$
(or ${\mathcal{L}}_{n}^{s}$). Now consider its product with one of the Markov
chains ${\mathcal{M}}$. The chance that ${\mathcal{M}}$ produces a word in
${\mathcal{L}}_{n}^{r}$ (and ${\mathcal{L}}_{n}^{s}$) should also be the value
of the state (a pair of $s_{n}$ and a state in ${\mathcal{G}}$) in the product
${\mathcal{M}}\times{\mathcal{G}}$ when $s_{n}$ is first reached. Since the
sub Markov chain that contain $s_{n}$ and $s_{f}$ is the same for all Markov
chains in this family, in the product MDP ${\mathcal{M}}\times{\mathcal{G}}$,
the state (a pair of $s_{n}$ and a state in ${\mathcal{G}}$) when $s_{n}$ is
first reached must be different. That is, $s_{n}$ must be paired with
different states of ${\mathcal{G}}$ for different Markov chains in this
family. As there are $2^{n}$ different Markov chains, there are at least
$2^{n}$ states in ${\mathcal{G}}$.

It can be seen from Figure 9 resp. Figure 10 that ${\mathcal{L}}_{n}^{r}$
resp. ${\mathcal{L}}_{n}^{s}$ are recognised by a nondeterministic
reachability resp. safety automaton with $n+2$ resp. $n+1$ states. With
Theorem 5.1, we have:

######  Corollary 5.3.

General nondeterministic automata are exponentially more succinct than GfM
automata.

We now consider the $\mathcal{R}_{n}$ and $\mathcal{S}_{n}$ more closely to
see that we have used small subclasses of nondeterministic Büchi automata: the
$\mathcal{R}_{n}$ are unambiguous reachability automata, while
$\mathcal{S}_{n}$ is a strongly unambiguous separating safety automata. Let us
start with the latter.

######  Lemma 5.4.

For each $n\in\mathbb{N}$, $\mathcal{S}_{n}$ is a strongly unambiguous
separating safety automaton.

With Theorem 5.1, this lemma provides:

######  Corollary 5.5.

Strongly unambiguous separating automata are exponentially more succinct than
GfM automata.

######  Lemma 5.6.

For each $n\in\mathbb{N}$, $\mathcal{R}_{n}$ is an unambiguous reachability
automaton.

As both $\mathcal{R}_{n}$ and $\mathcal{S}_{n}$ are unambiguous automata by
the previous lemmas, Theorem 5.1 provides:

######  Corollary 5.7.

Unambiguous reachability and safety automata are exponentially more succinct
than GfM automata.

Finally, we can create a separating automaton with $n+2$ states that
recognises the reachability language ${\mathcal{L}}_{n}^{r}$, shown in Figure
12. However, one cannot expect such automata to be (syntactic) reachability
automata, because all words are accepted from an accepting sink state.

$q_{0}$$q_{1}$$q_{2}$$q_{3}$$\ldots$$q_{n}$$f$$0,1$$1$$0,1$$0,1$$\$$$\$$$\$$$\$$$\$$$0,1$$\$$$0$
Figure 12: The separating NBA $\mathcal{R}_{n}^{\prime}$ recognises the
reachability language ${\mathcal{L}}_{n}^{r}$.

######  Lemma 5.8.

For each $n\in\mathbb{N}$, $\mathcal{R}_{n}^{\prime}$ is a separating
automaton that recognises ${\mathcal{L}}_{n}^{r}$.

With Theorem 5.1, this lemma provides:

######  Corollary 5.9.

Separating automata that recognise reachability languages are exponentially
more succinct than GfM automata.

##  6 Conclusion

We have established that GfM automata are exponentially more succinct than GfG
automata, while general nondeterministic automata are exponentially more
succinct than GfM automata. For the latter, we have shown that this is still
the case when we restrict the class of general nondeterministic automata
further, requiring them to be strongly unambiguous separating safety automata,
unambiguous reachability automata, or separating automata that recognise a
reachability language.

For all of these automata, we have provided very simple families of automata
that witness the exponentially succinctness advantage.

## References

  * [1] Luca Alfaro.  Formal Verification of Probabilistic Systems.  PhD thesis, Stanford University, Stanford, CA, USA, 1998.
  * [2] Christel Baier and Joost-Pieter Katoen.  Principles of Model Checking.  MIT Press, 2008.
  * [3] Christel Baier, Stefan Kiefer, Joachim Klein, David Müller, and James Worrell.  Markov chains and unambiguous automata.  J. Comput. Syst. Sci., 136:113–134, 2023.  doi:10.1016/j.jcss.2023.03.005.
  * [4] C. Courcoubetis and M. Yannakakis.  Markov decision processes and regular events.  In Automata, Languages and Programming, pages 336–349, 1990.  LNCS 443.
  * [5] E. M. Hahn, G. Li, S. Schewe, A. Turrini, and L. Zhang.  Lazy probabilistic model checking without determinisation.  In Concurrency Theory, pages 354–367, 2015.
  * [6] Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, and Dominik Wojtczak.  Good-for-MDPs automata for probabilistic analysis and reinforcement learning.  In Armin Biere and David Parker, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 306–323, Cham, 2020. Springer International Publishing.
  * [7] Hrishikesh Karmarkar, Manas Joglekar, and Supratik Chakraborty.  Improved upper and lower bounds for büchi disambiguation.  In Dang Van Hung and Mizuhito Ogawa, editors, Automated Technology for Verification and Analysis, pages 40–54, Cham, 2013. Springer International Publishing.
  * [8] Denis Kuperberg and Michal Skrzypczak.  On determinisation of good-for-games automata.  In Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann, editors, Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II, volume 9135 of Lecture Notes in Computer Science, pages 299–310. Springer, 2015.  doi:10.1007/978-3-662-47666-6\\_24.
  * [9] Bader Abu Radi and Orna Kupferman.  Minimization and canonization of GFG transition-based automata.  Log. Methods Comput. Sci., 18(3), 2022.  doi:10.46298/lmcs-18(3:16)2022.
  * [10] Sven Schewe.  Minimising good-for-games automata is np-complete.  In Nitin Saxena and Sunil Simon, editors, 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2020, December 14-18, 2020, BITS Pilani, K K Birla Goa Campus, Goa, India (Virtual Conference), volume 182 of LIPIcs, pages 56:1–56:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020\.  doi:10.4230/LIPIcs.FSTTCS.2020.56.
  * [11] S. Sickert, J. Esparza, S. Jaax, and J. Křetínský.  Limit-deterministic Büchi automata for linear temporal logic.  In Computer Aided Verification, pages 312–332, 2016.  LNCS 9780.

##  Appendix A Proofs of Section 5

See 5.4

######  Proof A.1.

It is obviously a safety automaton, as all states are final.

To see that $\mathcal{S}_{n}$ is separating, for all $i>0$ the language
accepted from state $q_{i}$ is $\\{0,1\\}^{i-1}\$^{\omega}$, while the
language from state $q_{0}$ contains only words, whose first $n$ letters are
in ${0,1}$ (as it would block on any word containing a $\$$ in its first $n$
letters).

To see that $\mathcal{S}_{n}$ is strongly unambiguous, we distinguish two
types of words: those that do, and those that do not contain a $\$$. For the
latter, $q_{0}^{\omega}$ is the only run, as all other runs that leave $q_{0}$
continue with $q_{1},q_{2},\ldots,q_{n}$ and then block. For the former, as
the automaton blocks when reading a $\$$ from every state except $q_{n}$, the
only possible run is to move to $q_{1}$ exactly $n$ steps before the first
$\$$ and then continue with $q_{2},q_{3},\ldots,q_{n-1},q_{n}^{\omega}$. (This
will only be a run if the word is in ${\mathcal{L}}_{n}^{s}$, but we only have
to show that there is no other run.)

See 5.6

######  Proof A.2.

It is obviously a reachability automaton, as it has only a single accepting
state, which is a sink.

To see that $\mathcal{R}_{n}$ is unambiguous, we look at a word in the
language ${\mathcal{L}}_{n}^{r}$ of the automaton. A word in
${\mathcal{L}}_{n}^{r}$ has the form
$\\{0,1\\}^{m}1\\{0,1\\}^{n-1}\\}\$\\{0,1,\$\\}^{\omega}$, and its only
accepting run is $q_{0}^{m+1},q_{1},q_{2},\ldots,q_{n},f^{\omega}$: any run
that would move to $q_{1}$ earlier would block on reading a $0$ or $1$ while
in $q_{n}$, while any run that would move to $q_{1}$ either later or not at
all would block when reading a $\$$ in a state $q_{i}$ with $i<n$.

See 5.8

######  Proof A.3.

To see that $\mathcal{R}_{n}^{\prime}$ is separating, we note that

  * •

words starting with $\$$ can only be accepted from $q_{n}$, as the automaton
blocks when reading $\$$ from any other state,

  * •

words starting with $\\{0,1\\}^{i}\$$, with $0<i<n$, can only be accepted from
$q_{n-i}$, because

    * –

when starting at $q_{j}$ with $j>n-i$, the automaton would block when reading
a $0$ or $1$ after reaching $q_{n}$, while

    * –

for all other states, the automaton would block when reading the first $\$$
while not having reached $q_{n}$,

  * •

words starting with $\\{0,1\\}^{i}1\\{0,1\\}^{n-1}\$$ can only be accepted
from $q_{0}$, because

    * –

from $q_{i}$ with $0<i\leq n$, the automaton would block when reading the
$(n+1-i)$-th letter which is a $0$ or a $1$, while

    * –

from $f$, it would block when moving upon reading the $j$-th letter with
$j\leq i$ to $q_{1}$ when, reading the $(n+j)$-th letter (a $0$ or $1$) in
state $q_{n}$ or, where $j>i+1$ (or where the automaton never moves to
$q_{1}$), when reading the $(1+i+n)$-th letter, a $\$$, in a state in $q_{k}$
with $k<n$ (or $f$),

  * •

words starting with $\\{0,1\\}^{i}0\\{0,1\\}^{n-1}\$$ can only be accepted
from $f$, using a similar argument, and

  * •

finally, words containing no $\$$ can only be accepted from $f$, because the
only final state reachable from any other state of the automaton is $q_{n}$,
and from $q_{n}$ the automaton would block, as it only accepts a $\$$ from
there.

This partitions the set of words. To see that $\mathcal{R}_{n}^{\prime}$
recognises ${\mathcal{L}}_{n}^{r}$, we note that, for all of the words that do
contain a $\$$, this provides a recipe to be in $q_{n}$ when this $\$$ arrives
from _some_ state, while for a word that does not contain a $\$$, we accept
from $f$ by simply staying there for ever. For a word in
${\mathcal{L}}_{n}^{r}$, we can therefore follow this recipe until a $\$$
arrives, and then pick a successor state $q$ so that the tail of the word
(after that $\$$) is in the language that can only be accepted from $q$, and
so forth. This constructs an accepting run. (Note that we have already shown
that words not in ${\mathcal{L}}_{n}^{r}$ cannot be accepted from the only
initial state, $q_{0}$.)