* This is a full and combined version of publications [1] and [2].

# Minimization and Canonization of
GFG Transition-Based Automata*

Bader Abu Radi  School of Computer Science and Engineering, The Hebrew
University, Jerusalem, Israel<EMAIL_ADDRESS>and  Orna Kupferman
School of Computer Science and Engineering, The Hebrew University, Jerusalem,
Israel<EMAIL_ADDRESS>
###### Abstract.

While many applications of automata in formal methods can use nondeterministic
automata, some applications, most notably synthesis, need deterministic or
good-for-games (GFG) automata. The latter are nondeterministic automata that
can resolve their nondeterministic choices in a way that only depends on the
past. The minimization problem for deterministic Büchi and co-Büchi word
automata is NP-complete. In particular, no canonical minimal deterministic
automaton exists, and a language may have different minimal deterministic
automata. We describe a polynomial minimization algorithm for GFG co-Büchi
word automata with transition-based acceptance. Thus, a run is accepting if it
traverses a set $\alpha$ of designated transitions only finitely often. Our
algorithm is based on a sequence of transformations we apply to the automaton,
on top of which a minimal quotient automaton is defined. We use our
minimization algorithm to show canonicity for transition-based GFG co-Büchi
word automata: all minimal automata have isomorphic safe components (namely
components obtained by restricting the transitions to these not in $\alpha$)
and once we saturate the automata with $\alpha$-transitions, we get full
isomorphism.

###### Key words and phrases:

Determinisitc Automata on Infinite Words, Good-For-Games Automata, co-Büchi
acceptance condition, Minimization, Canonization,

###### Contents

  1. 1 Introduction
  2. 2 Preliminaries
  3. 3 Minimizing GFG-tNCWs
    1. 3.1 A Sufficient Condition for GFG-tNCW Minimality
    2. 3.2 Safe Centralization
    3. 3.3 Safe-Minimization
  4. 4 Canonicity in GFG-tNCWs
    1. 4.1 Safe isomorphism
    2. 4.2 Isomorphism
    3. 4.3 Obtaining Canonical Minimal GFG-tNCWs
      1. 4.3.1 Obtaining canonical minimal $\alpha$-maximal up to homogeneity GFG-tNCWs
      2. 4.3.2 Obtaining canonical minimal $\alpha$-maximal GFG-tNCWs
    4. 4.4 Canonicity in GFG-NCWs and tDCWs
  5. 5 An Example
  6. 6 Discussion
  7. 7 Glossary
    1. 7.1 Relations between states
    2. 7.2 Properties of a GFG-tNCW

##  1\. Introduction

Automata theory is one of the longest established areas in Computer Science. A
classical problem in automata theory is minimization: generation of an
equivalent automaton with a minimal number of states. For automata on finite
words, the picture is well understood: For nondeterministic automata,
minimization is PSPACE-complete [23], whereas for deterministic automata, a
minimization algorithm, based on the Myhill-Nerode right congruence [38, 39],
generates in polynomial time a canonical minimal deterministic automaton [21].
Essentially, the canonical automaton, a.k.a. the quotient automaton, is
obtained by merging equivalent states.

A prime application of automata theory is specification, verification, and
synthesis of reactive systems [47, 14]. The automata-theoretic approach
considers relationships between systems and their specifications as
relationships between languages. Since we care about the on-going behavior of
nonterminating systems, the automata run on infinite words. Acceptance in such
automata is determined according to the set of states that are visited
infinitely often along the run. In Büchi automata [11] (NBW and DBW, for
nondeterministic and deterministic Büchi word automata, respectively), the
acceptance condition is a subset $\alpha$ of states, and a run is accepting
iff it visits $\alpha$ infinitely often. Dually, in co-Büchi automata (NCW and
DCW), a run is accepting iff it visits $\alpha$ only finitely often. In spite
of the extensive use of automata on infinite words in verification and
synthesis algorithms and tools, some fundamental problems around their
minimization are still open. For nondeterministic automata, minimization is
PSPACE-complete, as it is for automata on finite words. Before we describe the
situation for deterministic automata, let us elaborate some more on the power
of nondeterminism in the context of automata on infinite words, as this is
relevant to our contribution.

For automata on finite words, nondeterminism does not increase the expressive
power, yet it leads to exponential succinctness [41]. For automata on infinite
words, nondeterminism may increase the expressive power and also leads to
exponential succinctness. For example, NBWs are strictly more expressive than
DBWs [29]. In some applications of automata on infinite words, such as model
checking, algorithms can proceed with nondeterministic automata, whereas in
other applications, such as synthesis and control, they cannot. There, the
advantages of nondeterminism are lost, and the algorithms involve complicated
determinization constructions [42] or acrobatics for circumventing
determinization [28]. Essentially, the inherent difficulty of using
nondeterminism in synthesis lies in the fact that each guess of the
nondeterministic automaton should accommodate all possible futures.

A study of nondeterministic automata that can resolve their nondeterministic
choices in a way that only depends on the past started in [27], where the
setting is modeled by means of tree automata for derived languages. It then
continued by means of good for games (GFG) automata [20].111GFGness is also
used in [12] in the framework of cost functions under the name “history-
determinism”. A nondeterministic automaton ${\mathcal{A}}$ over an alphabet
$\Sigma$ is GFG if there is a strategy $g$ that maps each finite word
$u\in\Sigma^{*}$ to the transition to be taken after $u$ is read; and
following $g$ results in accepting all the words in the language of
${\mathcal{A}}$. Note that a state $q$ of ${\mathcal{A}}$ may be reachable via
different words, and $g$ may suggest different transitions from $q$ after
different words are read. Still, $g$ depends only on the past, namely on the
word read so far. Obviously, there exist GFG automata: deterministic ones, or
nondeterministic ones that are determinizable by pruning (DBP); that is, ones
that just add transitions on top of a deterministic automaton. In fact, the
GFG automata constructed in [20] are DBP.222As explained in [20], the fact
that the GFG automata constructed there are DBP does not contradict their
usefulness in practice, as their transition relation is simpler than the one
of the embodied deterministic automaton and it can be defined symbolically.

In terms of expressive power, it is shown in [27, 40] that GFG automata with
an acceptance condition $\gamma$ (e.g., Büchi) are as expressive as
deterministic $\gamma$ automata. The picture in terms of succinctness is
diverse. For automata on finite words, GFG automata are always DBP [27, 36].
For automata on infinite words, in particular NBWs and NCWs, GFG automata need
not be DBP [7]. Moreover, the best known determinization construction for GFG-
NBWs is quadratic, whereas determinization of GFG-NCWs has a tight exponential
(blow up) bound [24]. Thus, GFG automata on infinite words are more succinct
(possibly even exponentially) than deterministic ones.333We note that some of
the succinctness results are known only for GFG automata with _transition-
based_ acceptance. Further research studies characterization, typeness,
complementation, and further constructions and decision procedures for GFG
automata [24, 9, 5], as well as an extension of the GFG setting to pushdown
$\omega$-automata [30] and to alternating automata [10, 8].

Back to the minimization problem. Recall that for finite words, an equivalent
minimal deterministic automaton can be obtained by merging equivalent states.
A similar algorithm is valid for determinisitic weak automata on infinite
words: DBWs in which each strongly connected component is either contained in
$\alpha$ or is disjoint from $\alpha$ [37, 32]. For general DBWs (and hence,
also DCWs, as the two dualize each other), merging of equivalent states fails,
and minimization is NP-complete [43].

The intractability of the minimization problem has led to a development of
numerous heuristics. The heuristics either relax the minimality requirement,
for example algorithms based on fair bisimulation [17], which reduce the state
space but need not return a minimal automaton, or relax the equivalence
requirement, for example algorithms based on hyper-minimization [4, 22] or
almost-equivalence [43], which come with a guarantee about the difference
between the language of the original automaton and the ones generated by the
algorithm. In some cases, these algorithms do generate a minimal equivalent
automaton (in particular, applying relative minimization based on almost-
equivalence on a deterministic weak automaton results in an equivalent minimal
weak automaton [43]), but in general, they are only heuristics. In an
orthogonal line of work, researchers have studied minimization in richer
settings of automata on finite words. One direction is to allow some
nondeterminism. As it turns out, however, even the slightest extension of the
deterministic model towards a nondeterministic one, for example by allowing at
most one nondeterministic choice in every accepting computation or allowing
just two initial states instead of one, results in NP-complete minimization
problems [33]. Another direction is a study of quantitative settings. Here,
the picture is diverse. For example, minimization of deterministic lattice
automata [26] is polynomial for automata over linear lattices and is NP-
complete for general lattices [18], and minimization of deterministic weighted
automata over the tropical semiring is polynomial [35], yet the problem is
open for general semirings.

Proving NP-hardness for DBW minimization, Schewe used a reduction from the
vertex-cover problem [43]. Essentially444The exact reduction is more
complicated and involves an additional letter that is required for cases in
which vertices in the graph have similar neighbours. Since, however, the
vertex-cover problem is NP-hard also for instances in which different vertices
have different sets of successors, it is possible to simplify this component
of the reduction., given a graph $G=\langle V,E\rangle$, we seek a minimal DBW
for the language $L_{G}$ of words of the form $v_{i_{1}}^{+}\cdot
v_{i_{2}}^{+}\cdot v_{i_{3}}^{+}\cdots\in V^{\omega}$, where for all $j\geq
1$, we have that $\langle v_{i_{j}},v_{i_{j+1}}\rangle\in E$. We can recognize
$L_{G}$ by an automaton obtained from $G$ by adding self loops to all
vertices, labelling each edge by its destination, and requiring a run to
traverse infinitely many original edges of $G$. Indeed, such runs correspond
to words that traverse an infinite path in $G$, possibly looping at vertices,
but not getting trapped in a self loop, as required by $L_{G}$. When, however,
the acceptance condition is defined by a set of vertices, rather than
transitions, we need to duplicate some states, and a minimal duplication
corresponds to a minimal vertex cover. Thus, a natural question arises: Is
there a polynomial minimization algorithms for DBWs and DCWs whose acceptance
condition is transition based? In such automata, the acceptance is a subset
$\alpha$ of transitions, and a run is required to traverse transitions in
$\alpha$ infinitely often (in Büchi automata, denoted tNBW), or finitely often
(in co-Büchi automata, denoted tNCW). Beyond the theoretical interest, there
is recently growing use of transition-based automata in practical
applications, with evidences they offer a simpler translation of LTL formulas
to automata and enable simpler constructions and decision procedures [15, 16,
13, 45, 31].

In this paper we describe a polynomial-time algorithm for the minimization of
GFG-tNCWs. Consider a GFG-tNCW ${\mathcal{A}}$. Our algorithm is based on a
chain of transformations we apply to ${\mathcal{A}}$. Some of the
transformations are introduced in [24], in algorithms for deciding GFGness.
These transformations result in nice GFG-tNCWs, and satisfy some simple
syntactic and semantic properties. We add two more transformations and prove
that they guarantee minimality. Our reasoning is based on a careful analysis
of the safe components of ${\mathcal{A}}$, namely its strongly connected
components obtained by removing transitions in $\alpha$. Note that every
accepting run of ${\mathcal{A}}$ eventually reaches and stays forever in a
safe component. We show that a minimal GFG-tNCW equivalent to ${\mathcal{A}}$
can be obtained by defining an order on the safe components, and applying the
quotient construction on a GFG-tNCW obtained by restricting attention to
states that belong to components that form a frontier in this order. All
involved transformations require polynomial time, thus so does the obtained
minimization algorithm.

Minimization and its complexity are tightly related to the canonicity
question. Recall that $\omega$-regular languages do not have a unique minimal
DBW or DCW [25]. We continue and study canonicity for GFG and transition-based
automata. We start with GFG-tNCWs and show that all minimal nice GFG-tNCWs are
safe isomorphic, namely their safe components are isomorphic. More formally,
if ${\mathcal{A}}_{1}$ and ${\mathcal{A}}_{2}$ are nice minimal GFG-tNCWs for
the same language, then there exists a bijection between the state spaces of
${\mathcal{A}}_{1}$ and ${\mathcal{A}}_{2}$ that induces a bijection between
their $\bar{\alpha}$-transitions (these not in $\alpha$). We then show that by
saturating the GFG-tNCW with $\alpha$-transitions we get isomorphism among all
minimal automata. We suggest two possible saturations. One adds as many
$\alpha$-transitions as possible, and the second does so in a way that
preserves $\alpha$-homogeneity, thus for every state $q$ and letter $\sigma$,
all the transitions labeled $\sigma$ from $q$ are $\alpha$-transitions or are
all $\bar{\alpha}$-transitions. Since our minimization algorithm generates
minimal $\alpha$-homogenous GFG-tNCWs, both forms of canonical minimal GFG-
tNCWs can be obtained in polynomial time.

We then show that GFGness is not a sufficient condition for canonicity,
raising the question of canonicity in tDCWs. Note that unlike the GFG-tNCW
setting, dualization of the acceptance condition in deterministic automata
complements the language of an automaton, and thus our results apply also to
canonicity of tDBWs. We start with some bad news, showing that as has been the
case with DCWs and DBWs, minimal tDCWs and tDBWs need not be isomorphic.
Moreover, we cannot change membership of transitions in $\alpha$ or add
transitions in order to make them isomorphic. On the positive side, safe
isomorphism is helpful also in the tDCW setting: Consider an $\omega$-regular
language $L$. Recall that the minimal GFG-tNCW for $L$ may be smaller than a
minimal tDCW for $L$ [24]. We say that $L$ is GFG-helpful if this is the case.
We prove that all minimal tDCWs for an $\omega$-regular language that is not
GFG-helpful are safe isomorphic. For $\omega$-regular languages that are GFG-
helpful, safe isomorphism is left open. For such languages, however, we care
more about minimal GFG-tNCWs, which may be exponentially smaller [24], and
which do have a canonical form. Also, natural $\omega$-regular languages are
not GFG-helpful, and in fact the existence of $\omega$-regular languages that
are GFG-helpful had been open for quite a while [7]. Accordingly, we view our
results as good news about canonicity in deterministic automata with
transition-based acceptance.

##  2\. Preliminaries

For a finite nonempty alphabet $\Sigma$, an infinite word
$w=\sigma_{1}\cdot\sigma_{2}\cdots\in\Sigma^{\omega}$ is an infinite sequence
of letters from $\Sigma$. A language $L\subseteq\Sigma^{\omega}$ is a set of
words. We denote the empty word by $\epsilon$, and the set of finite words
over $\Sigma$ by $\Sigma^{*}$. For $i\geq 0$, we use $w[1,i]$ to denote the
(possibly empty) prefix $\sigma_{1}\cdot\sigma_{2}\cdots\sigma_{i}$ of $w$ and
use $w[i+1,\infty]$ to denote its suffix
$\sigma_{i+1}\cdot\sigma_{i+2}\cdots$.

A _nondeterministic automaton_ over infinite words is
${\mathcal{A}}=\langle\Sigma,Q,q_{0},\delta,\alpha\rangle$, where $\Sigma$ is
an alphabet, $Q$ is a finite set of _states_ , $q_{0}\in Q$ is an _initial
state_ , $\delta:Q\times\Sigma\to 2^{Q}\setminus\emptyset$ is a _transition
function_ , and $\alpha$ is an _acceptance condition_ , to be defined below.
For states $q$ and $s$ and a letter $\sigma\in\Sigma$, we say that $s$ is a
$\sigma$-successor of $q$ if $s\in\delta(q,\sigma)$. Note that ${\mathcal{A}}$
is total, in the sense that it has at least one successor for each state and
letter, and that ${\mathcal{A}}$ may be _nondeterministic_ , as the transition
function may specify several successors for each state and letter. If
$|\delta(q,\sigma)|=1$ for every state $q\in Q$ and letter $\sigma\in\Sigma$,
then ${\mathcal{A}}$ is _deterministic_. We define the _size_ of
${\mathcal{A}}$, denoted $|{\mathcal{A}}|$, as its number of states555Note
that our definition of size follows the traditional complexity measure of
deterministic automata on finite words. As argued in [6], it is interesting to
study additional complexity measures, in particular the size of the transition
function of the automaton., thus, $|{\mathcal{A}}|=|Q|$.

When ${\mathcal{A}}$ runs on an input word, it starts in the initial state and
proceeds according to the transition function. Formally, a _run_ of
${\mathcal{A}}$ on $w=\sigma_{1}\cdot\sigma_{2}\cdots\in\Sigma^{\omega}$ is an
infinite sequence of states $r=r_{0},r_{1},r_{2},\ldots\in Q^{\omega}$, such
that $r_{0}=q_{0}$, and for all $i\geq 0$, we have that
$r_{i+1}\in\delta(r_{i},\sigma_{i+1})$. We sometimes consider finite runs on
finite words. In particular, we sometimes extend $\delta$ to sets of states
and finite words. Then, $\delta:2^{Q}\times\Sigma^{*}\to 2^{Q}$ is such that
for every $S\in 2^{Q}$, finite word $u\in\Sigma^{*}$, and letter
$\sigma\in\Sigma$, we have that $\delta(S,\epsilon)=S$,
$\delta(S,\sigma)=\bigcup_{s\in S}\delta(s,\sigma)$, and
$\delta(S,u\cdot\sigma)=\delta(\delta(S,u),\sigma)$. Thus, $\delta(S,u)$ is
the set of states that ${\mathcal{A}}$ may reach when it reads $u$ from some
state in $S$.

The transition function $\delta$ induces a transition relation
$\Delta\subseteq Q\times\Sigma\times Q$, where for every two states $q,s\in Q$
and letter $\sigma\in\Sigma$, we have that $\langle
q,\sigma,s\rangle\in\Delta$ iff $s\in\delta(q,\sigma)$. We sometimes view the
run $r=r_{0},r_{1},r_{2},\ldots$ on $w=\sigma_{1}\cdot\sigma_{2}\cdots$ as an
infinite sequence of successive transitions $\langle
r_{0},\sigma_{1},r_{1}\rangle,\langle
r_{1},\sigma_{2},r_{2}\rangle,\ldots\in\Delta^{\omega}$. The acceptance
condition $\alpha$ determines which runs are “good”. We consider here
_transition-based_ automata, in which $\alpha$ is a set of transitions – these
that should be traversed infinitely often during the run; specifically,
$\alpha\subseteq\Delta$. We use the terms $\alpha$-transitions and
$\bar{\alpha}$-transitions to refer to transitions in $\alpha$ and in
$\Delta\setminus\alpha$, respectively. We also refer to restrictions
$\delta^{\alpha}$ and $\delta^{\bar{\alpha}}$ of $\delta$, where for all
$q,s\in Q$ and $\sigma\in\Sigma$, we have that $s\in\delta^{\alpha}(q,\sigma)$
iff $\langle q,\sigma,s\rangle\in\alpha$, and
$s\in\delta^{\bar{\alpha}}(q,\sigma)$ iff $\langle
q,\sigma,s\rangle\in\Delta\setminus\alpha$.

We say that ${\mathcal{A}}$ is _$\alpha$ -homogenous_ if for every state $q\in
Q$ and letter $\sigma\in\Sigma$, either
$\delta^{\alpha}_{\mathcal{A}}(q,\sigma)=\emptyset$ or
$\delta^{\bar{\alpha}}_{\mathcal{A}}(q,\sigma)=\emptyset$. Thus, either all
the $\sigma$-labeled transitions from $q$ are $\alpha$-transitions, or they
are all $\bar{\alpha}$-transitions. For a run $r\in\Delta^{\omega}$, let ${\it
inf}(r)\subseteq\Delta$ be the set of transitions that $r$ traverses
infinitely often. Thus, ${\it inf}(r)=\\{\langle
q,\sigma,s\rangle\in\Delta:q=r_{i},\sigma=\sigma_{i+1}\text{ and
}s=r_{i+1}\text{ for infinitely many $i$'s}\\}$. In co-Büchi automata, $r$ is
_accepting_ iff ${\it inf}(r)\cap\alpha=\emptyset$, thus if $r$ traverses
transitions in $\alpha$ only finitely often. A run that is not accepting is
_rejecting_. A word $w$ is accepted by ${\mathcal{A}}$ if there is an
accepting run of ${\mathcal{A}}$ on $w$. The language of ${\mathcal{A}}$,
denoted $L({\mathcal{A}})$, is the set of words that ${\mathcal{A}}$ accepts.
Two automata are _equivalent_ if their languages are equivalent. We use tNCW
and tDCW to abbreviate nondeterministic and deterministic transition-based co-
Büchi automata over infinite words, respectively. We say that a
nondeterministic automaton ${\mathcal{A}}$ is determinizable by prunning (DBP)
if we can remove some of the transitions of ${\mathcal{A}}$ and get a
deterministic automaton that recognizes $L({\mathcal{A}})$.

We continue to definitions and notations that are relevant to our study. See
Section 7 for a glossary. For a state $q\in Q$ of an automaton
${\mathcal{A}}=\langle\Sigma,Q,q_{0},\delta,\alpha\rangle$, we define
${\mathcal{A}}^{q}$ to be the automaton obtained from ${\mathcal{A}}$ by
setting the initial state to be $q$. Thus,
${\mathcal{A}}^{q}=\langle\Sigma,Q,q,\delta,\alpha\rangle$. We say that two
states $q,s\in Q$ are _equivalent_ , denoted $q\sim_{{\mathcal{A}}}s$, if
$L({\mathcal{A}}^{q})=L({\mathcal{A}}^{s})$. The automaton ${\mathcal{A}}$ is
_semantically deterministic_ if different nondeterministic choices lead to
equivalent states. Thus, for every state $q\in Q$ and letter
$\sigma\in\Sigma$, all the $\sigma$-successors of $q$ are equivalent: for
every two states $s,s^{\prime}\in Q$ such that $\langle q,\sigma,s\rangle$ and
$\langle q,\sigma,s^{\prime}\rangle$ are in $\Delta$, we have that
$s\sim_{{\mathcal{A}}}s^{\prime}$. The following proposition follows
immediately from the definitions.

######  Proposition .

Consider a semantically deterministic automaton ${\mathcal{A}}$, states
$q,s\in Q$, letter $\sigma\in\Sigma$, and transitions $\langle
q,\sigma,q^{\prime}\rangle,\langle s,\sigma,s^{\prime}\rangle\in\Delta$. If
$q\sim_{{\mathcal{A}}}s$, then $q^{\prime}\sim_{{\mathcal{A}}}s^{\prime}$.

An automaton ${\mathcal{A}}$ is _good for games_ (_GFG_ , for short) if its
nondeterminism can be resolved based on the past, thus on the prefix of the
input word read so far. Formally, ${\mathcal{A}}$ is _GFG_ if there exists a
strategy $f:\Sigma^{*}\to Q$ such that the following hold:

  1. (1)

The strategy $f$ is consistent with the transition function. That is,
$f(\epsilon)=q_{0}$, and for every finite word $u\in\Sigma^{*}$ and letter
$\sigma\in\Sigma$, we have that $\langle
f(u),\sigma,f(u\cdot\sigma)\rangle\in\Delta$.

  2. (2)

Following $f$ causes ${\mathcal{A}}$ to accept all the words in its language.
That is, for every infinite word
$w=\sigma_{1}\cdot\sigma_{2}\cdots\in\Sigma^{\omega}$, if $w\in
L({\mathcal{A}})$, then the run $f(w[1,0]),f(w[1,1]),f(w[1,2]),\ldots$, which
we denote by $f(w)$, is an accepting run of ${\mathcal{A}}$ on $w$.

Note that by definition, the strategy $f$ maps a finite word $u$ to the state
that the run induced by $f$ visits after reading $u$. We sometimes abuse
notation and use $f(w)$, for an infinite word $w$, to denote the run on $w$
that is induced by $f$. We say that the strategy $f$ _witnesses_
${\mathcal{A}}$’s GFGness. For an automaton ${\mathcal{A}}$, we say that a
state $q$ of ${\mathcal{A}}$ is _GFG_ if ${\mathcal{A}}^{q}$ is GFG. Note that
every deterministic automaton is GFG.

Consider a directed graph $G=\langle V,E\rangle$. A _strongly connected set_
in $G$ (SCS, for short) is a set $C\subseteq V$ such that for every two
vertices $v,v^{\prime}\in C$, there is a path from $v$ to $v^{\prime}$. A SCS
is _maximal_ if it is maximal w.r.t containment, that is, for every non-empty
set $C^{\prime}\subseteq V\setminus C$, it holds that $C\cup C^{\prime}$ is
not a SCS. The _maximal strongly connected sets_ are also termed _strongly
connected components_ (SCCs, for short). The _SCC graph of $G$_ is the graph
defined over the SCCs of $G$, where there is an edge from a SCC $C$ to another
SCC $C^{\prime}$ iff there are two vertices $v\in C$ and $v^{\prime}\in
C^{\prime}$ with $\langle v,v^{\prime}\rangle\in E$. A SCC is _ergodic_ iff it
has no outgoing edges in the SCC graph. The SCC graph of $G$ can be computed
in linear time by standard SCC algorithms [46]. An automaton
${\mathcal{A}}=\langle\Sigma,Q,q_{0},\delta,\alpha\rangle$ induces a directed
graph $G_{{\mathcal{A}}}=\langle Q,E\rangle$, where $\langle
q,q^{\prime}\rangle\in E$ iff there is a letter $\sigma\in\Sigma$ such that
$\langle q,\sigma,q^{\prime}\rangle\in\Delta$. The SCSs and SCCs of
${\mathcal{A}}$ are those of $G_{{\mathcal{A}}}$. We say that a tNCW
${\mathcal{A}}$ is _safe deterministic_ if by removing its
$\alpha$-transitions, we remove all nondeterministic choices. Thus, for every
state $q\in Q$ and letter $\sigma\in\Sigma$, it holds that
$|\delta^{\bar{\alpha}}(q,\sigma)|\leq 1$.

We refer to the SCCs we get by removing ${\mathcal{A}}$’s $\alpha$-transitions
as the _safe components_ of ${\mathcal{A}}$; that is, the _safe components_ of
${\mathcal{A}}$ are the SCCs of the graph
$G_{{\mathcal{A}}^{\bar{\alpha}}}=\langle Q,E^{\bar{\alpha}}\rangle$, where
$\langle q,q^{\prime}\rangle\in E^{\bar{\alpha}}$ iff there is a letter
$\sigma\in\Sigma$ such that $\langle
q,\sigma,q^{\prime}\rangle\in\Delta\setminus\alpha$. We denote the set of safe
components of ${\mathcal{A}}$ by ${\mathcal{S}}({\mathcal{A}})$. For a safe
component $S\in{\mathcal{S}}({\mathcal{A}})$, the _size_ of $S$, denoted
$|S|$, is the number of states in $S$. Note that an accepting run of
${\mathcal{A}}$ eventually gets trapped in one of ${\mathcal{A}}$’s safe
components. A tNCW ${\mathcal{A}}$ is _normal_ if there are no
$\bar{\alpha}$-transitions connecting different safe components. That is, for
all states $q$ and $s$ of ${\mathcal{A}}$, if there is a path of
$\bar{\alpha}$-transitions from $q$ to $s$, then there is also a path of
$\bar{\alpha}$-transitions from $s$ to $q$.

We now combine several properties defined above and say that a GFG-tNCW
${\mathcal{A}}$ is nice if all the states in ${\mathcal{A}}$ are reachable and
GFG, and ${\mathcal{A}}$ is normal, safe deterministic, and semantically
deterministic. In the theorem below we combine arguments from [24] showing
that each of these properties can be obtained in at most polynomial time, and
without the properties being conflicting. For some properties, we give an
alternative and simpler proof.

######  Theorem .

[24] Every GFG-tNCW ${\mathcal{A}}$ can be turned, in polynomial time, into an
equivalent nice GFG-tNCW ${\mathcal{B}}$ such that
$|{\mathcal{B}}|\leq|{\mathcal{A}}|$.

###### Proof.

It is shown in [24] that one can decide the GFGness of a tNCW ${\mathcal{A}}$
in polynomial time. The proof goes through an intermediate step where the
authors construct a two-player game such that if the first player does not win
the game, then ${\mathcal{A}}$ is not GFG, and otherwise a winning strategy
for the first player induces a safe deterministic GFG-tNCW ${\mathcal{B}}$
equivalent to ${\mathcal{A}}$ of size at most $|{\mathcal{A}}|$. As we start
with a GFG-tNCW ${\mathcal{A}}$, such a winning strategy is guaranteed to
exist, and, by [24], can be found in polynomial time. Thus, we obtain an
equivalent safe deterministic GFG-tNCW ${\mathcal{B}}$ of size at most
$|{\mathcal{A}}|$ in polynomial time. In fact, it can be shown that
${\mathcal{B}}$ is also semantically deterministic. Yet, for completeness we
give below a general procedure for semantic determinization.

For a tNCW ${\mathcal{A}}$, we say that a transition $\langle
q,\sigma,s\rangle\in\Delta$ is _covering_ if for every transition $\langle
q,\sigma,s^{\prime}\rangle$, it holds that
$L({{\mathcal{A}}}^{s^{\prime}})\subseteq L({\mathcal{A}}^{s})$. If
${\mathcal{A}}$ is GFG and $f$ is a strategy witnessing its GFGness, we say
that a state $q$ of ${\mathcal{A}}$ is _used by_ $f$ if there is a finite word
$u$ with $f(u)=q$, and we say that a transition $\langle
q,\sigma,q^{\prime}\rangle$ of ${\mathcal{A}}$ is _used by_ $f$ if there is a
finite word $u$ with $f(u)=q$ and $f(u\cdot\sigma)=q^{\prime}$. Since states
that are not GFG can be detected in polynomial time, and as all states that
are used by a strategy that witnesses ${\mathcal{B}}$’s GFGness are GFG, the
removal of non-GFG states does not affect ${\mathcal{B}}$’s language. Note
that removing the non-GFG states may result in a non-total automaton, in which
case we add a rejecting sink. Note that we add a rejecting sink only after
removing some state, thus this step does not add states. Now, using the fact
that language containment of GFG-tNCWs can be checked in polynomial time [19,
24], and transitions that are used by strategies are covering [24], one can
semantically determinize ${\mathcal{B}}$ by removing non-covering transitions.

States that are not reachable are easy to detect, and their removal does not
affect ${\mathcal{B}}$’s language nor its GFGness. Normalization is also easy
to obtain and involves adding some existing transitions to $\alpha$ [24].
Indeed, if there are $\bar{\alpha}$-transitions connecting different safe
components of ${\mathcal{B}}$, then they can be added to $\alpha$ without
affecting the acceptance of runs in ${\mathcal{B}}$, as every accepting run
traverses such transitions only finitely often. Thus, the language and GFGness
of all states are not affected. Finally, it is not hard to verify that the
properties, in the order we obtain them in the proof, are not conflicting, and
thus the described sequence of transformations results in a nice GFG-tNCW
whose size is bounded by $|{\mathcal{A}}|$. ∎

##  3\. Minimizing GFG-tNCWs

A GFG-tNCW ${\mathcal{A}}$ is _minimal_ if for every equivalent GFG-tNCW
${\mathcal{B}}$, it holds that $|{\mathcal{A}}|\leq|{\mathcal{B}}|$. In this
section, we suggest a polynomial-time minimization algorithm for GFG-tNCWs.

###  3.1. A Sufficient Condition for GFG-tNCW Minimality

In this section, we define two additional properties for nice GFG-tNCWs,
namely _safe-centralized_ and _safe-minimal_ , and we prove that nice GFG-
tNCWs that satisfy these properties are minimal. In Sections 3.2 – 3.3, we are
going to show that the two properties can be attained in polynomial time.
Before we start, let us note that a GFG-tNCW may be nice and still not be
minimal. A simple example is the tDCW ${\mathcal{A}}_{\sf fm}$ for the
language $(a+b)^{*}\cdot a^{\omega}$ that appears in Figure 1 below. The
dashed transitions are $\alpha$-transitions. It is easy to see that
${\mathcal{A}}_{\sf fm}$ is a nice GFG-tNCW, but it is not minimal.

Figure 1. The tDCW ${\mathcal{A}}_{\sf fm}$.

Consider a tNCW ${\mathcal{A}}=\langle\Sigma,Q,q_{0},\delta,\alpha\rangle$. A
run $r$ of ${\mathcal{A}}$ is _safe_ if it does not traverse
$\alpha$-transitions. The _safe language_ of ${\mathcal{A}}$, denoted $L_{{\it
safe}}({\mathcal{A}})$, is the set of infinite words $w$, such that there is a
safe run of ${\mathcal{A}}$ on $w$. Accordingly, each state $q\in Q$ induces
two languages: the language of $q$, namely $L({\mathcal{A}}^{q})$, which
includes words accepted from $q$, and the safe language of $q$, namely
$L_{{\it safe}}({\mathcal{A}}^{q})$, which is the set of infinite words that
can be read from $q$ without traversing an $\alpha$-transition. Clearly,
$L_{{\it safe}}({\mathcal{A}}^{q})\subseteq L({\mathcal{A}}^{q})$. Recall that
two states $q,s\in Q$ are equivalent ($q\sim_{{\mathcal{A}}}s$) if
$L({\mathcal{A}}^{q})=L({\mathcal{A}}^{s})$. Then, $q$ and $s$ are _strongly-
equivalent_ , denoted $q\approx_{{\mathcal{A}}}s$, if $q\sim_{{\mathcal{A}}}s$
and $L_{{\it safe}}({\mathcal{A}}^{q})=L_{{\it safe}}({\mathcal{A}}^{s})$.
Thus, $q$ and $s$ agree on both their languages and safe languages. Finally,
$q$ is _subsafe-equivalent to_ $s$, denoted $q\precsim_{{\mathcal{A}}}s$, if
$q\sim_{{\mathcal{A}}}s$ and $L_{{\it safe}}({\mathcal{A}}^{q})\subseteq
L_{{\it safe}}({\mathcal{A}}^{s})$. Note that the three relations are
transitive. When ${\mathcal{A}}$ is clear from the context, we omit it from
the notations, thus write $q\precsim s$, $q\approx s$, etc. The tNCW
${\mathcal{A}}$ is _safe-minimal_ if it has no strongly-equivalent states.
Thus, every two states differ in their languages or safe-languages. Then,
${\mathcal{A}}$ is _safe-centralized_ if for every two states $q,s\in Q$, if
$q\precsim s$, then $q$ and $s$ are in the same safe component of
${\mathcal{A}}$. Intuitively, this suggests that ${\mathcal{A}}$ is compact,
in the sense that states that agree on their languages and have comparable
safe languages are not spread in different safe components.

######  Example .

The nice GFG-tNCW ${\mathcal{A}}_{\sf fm}$ from Figure 1 is neither safe-
minimal (its two states are strongly-equivalent) nor safe-centralized (its two
states are in different safe components). As another example, consider the
tDCW ${\mathcal{A}}$ appearing in Figure 2. Recall that the dashed transitions
are $\alpha$-transitions. All the states of ${\mathcal{A}}$ are equivalent,
yet they all differ in their safe language. Accordingly, ${\mathcal{A}}$ is
safe-minimal. Since $\\{a^{\omega}\\}=L_{{\it
safe}}({\mathcal{A}}^{q_{2}})\subseteq L_{{\it safe}}({\mathcal{A}}^{q_{0}})$,
we have that $q_{2}\precsim q_{0}$. Hence, as $q_{0}$ and $q_{2}$ are in
different safe components, the tDCW ${\mathcal{A}}$ is not safe-centralized. ∎

Figure 2. The tDCW ${\mathcal{A}}$.

We continue and specify useful properties of nice GFG-tNCWs. Intuitively,
these properties show that the coincidence of language equivalence with
bisimulation [34] in the setting of deterministic automata is carried over to
GFG-tNCWs when restricted to their safe components.

######  Proposition .

Consider a nice GFG-tNCW ${\mathcal{A}}$ and states $q$ and $s$ of
${\mathcal{A}}$ such that $q\approx s$ ($q\precsim s$). For every letter
$\sigma\in\Sigma$ and $\bar{\alpha}$-transition $\langle
q,\sigma,q^{\prime}\rangle$, there is an $\bar{\alpha}$-transition $\langle
s,\sigma,s^{\prime}\rangle$ such that $q^{\prime}\approx s^{\prime}$
($q^{\prime}\precsim s^{\prime}$, respectively).

###### Proof.

We prove the proposition for the case $q\approx s$. The case $q\precsim s$ is
similar. Since ${\mathcal{A}}$ is normal, the existence of the
$\bar{\alpha}$-transition $\langle q,\sigma,q^{\prime}\rangle$ implies that
there is a safe run from $q^{\prime}$ back to $q$. Hence, there is a word
$z\in L_{{\it safe}}({\mathcal{A}}^{q^{\prime}})$. Clearly, $\sigma\cdot z$ is
in $L_{{\it safe}}({\mathcal{A}}^{q})$. Now, since $q\approx s$, we have that
$L_{{\it safe}}({\mathcal{A}}^{q})=L_{{\it safe}}({\mathcal{A}}^{s})$. In
particular, $\sigma\cdot z\in L_{{\it safe}}({\mathcal{A}}^{s})$, and thus
there is an $\bar{\alpha}$-transition $\langle s,\sigma,s^{\prime}\rangle$. We
prove that $q^{\prime}\approx s^{\prime}$. Since
$L({\mathcal{A}}^{q})=L({\mathcal{A}}^{s})$ and ${\mathcal{A}}$ is
semantically deterministic, then, by Proposition 2, we have that
$L({\mathcal{A}}^{q^{\prime}})=L({\mathcal{A}}^{s^{\prime}})$. It is left to
prove that $L_{{\it safe}}({\mathcal{A}}^{q^{\prime}})=L_{{\it
safe}}({\mathcal{A}}^{s^{\prime}})$. We prove that $L_{{\it
safe}}({\mathcal{A}}^{q^{\prime}})\subseteq L_{{\it
safe}}({\mathcal{A}}^{s^{\prime}})$. The second direction is similar. Since
${\mathcal{A}}$ is safe deterministic, the transition $\langle
s,\sigma,s^{\prime}\rangle$ is the only $\sigma$-labeled
$\bar{\alpha}$-transition from $s$. Hence, if by contradiction there is a word
$z\in L_{{\it safe}}({\mathcal{A}}^{q^{\prime}})\setminus L_{{\it
safe}}({\mathcal{A}}^{s^{\prime}})$, we get that $\sigma\cdot z\in L_{{\it
safe}}({\mathcal{A}}^{q})\setminus L_{{\it safe}}({\mathcal{A}}^{s})$,
contradicting the fact that $L_{{\it safe}}({\mathcal{A}}^{q})=L_{{\it
safe}}({\mathcal{A}}^{s})$. ∎

We continue with propositions that relate two automata,
${\mathcal{A}}=\langle\Sigma,Q_{{\mathcal{A}}},q^{0}_{{\mathcal{A}}},\delta_{{\mathcal{A}}},\alpha_{{\mathcal{A}}}\rangle$
and
${\mathcal{B}}=\langle\Sigma,Q_{{\mathcal{B}}},q^{0}_{{\mathcal{B}}},\delta_{{\mathcal{B}}},\alpha_{{\mathcal{B}}}\rangle$.
We assume that $Q_{{\mathcal{A}}}$ and $Q_{{\mathcal{B}}}$ are disjoint, and
extend the $\sim$, $\approx$, and $\precsim$ relations to states in
$Q_{{\mathcal{A}}}\cup Q_{{\mathcal{B}}}$ in the expected way. For example,
for $q\in Q_{{\mathcal{A}}}$ and $s\in Q_{{\mathcal{B}}}$, we use $q\sim s$ to
indicate that $L({\mathcal{A}}^{q})=L({\mathcal{B}}^{s})$. Propositions 3.1
and 3.1 suggest that states of equivalent GFG-tNCWs are related through their
languages and safe-languages. In Lemma 3.1, we use this fact in order to show
that among equivalent GFG-tNCWs, safe-centralized automata have minimal number
of safe-components.

######  Proposition .

Let ${\mathcal{A}}$ and ${\mathcal{B}}$ be equivalent nice GFG-tNCWs. For
every state $q\in Q_{{\mathcal{A}}}$, there is a state $s\in
Q_{{\mathcal{B}}}$ such that $q\precsim s$.

###### Proof.

Let $g$ be a strategy witnessing ${\mathcal{B}}$’s GFGness. Consider a state
$q\in Q_{{\mathcal{A}}}$. Let $u\in\Sigma^{*}$ be such that
$q\in\delta_{{\mathcal{A}}}(q^{0}_{\mathcal{A}},u)$. Since ${\mathcal{A}}$ and
${\mathcal{B}}$ are equivalent and semantically deterministic, an iterative
application of Proposition 2 implies that for every state
$s\in\delta_{{\mathcal{B}}}(q^{0}_{\mathcal{B}},u)$, we have $q\sim s$. In
particular, $q\sim g(u)$. If $L_{{\it safe}}({\mathcal{A}}^{q})=\emptyset$,
then we are done, as $L_{{\it safe}}({\mathcal{A}}^{q})\subseteq L_{{\it
safe}}({\mathcal{B}}^{g(u)})$. If $L_{{\it
safe}}({\mathcal{A}}^{q})\neq\emptyset$, then the proof proceeds as follows.
Assume by way of contradiction that for every state $s\in Q_{{\mathcal{B}}}$
that is equivalent to $q$, it holds that $L_{{\it
safe}}({\mathcal{A}}^{q})\not\subseteq L_{{\it safe}}({\mathcal{B}}^{s})$. We
define an infinite word $z\in\Sigma^{\omega}$ such that ${\mathcal{A}}$
accepts $u\cdot z$, yet $g(u\cdot z)$ is a rejecting run of ${\mathcal{B}}$.
Since ${\mathcal{A}}$ and ${\mathcal{B}}$ are equivalent, this contradicts the
fact that $g$ witnesses ${\mathcal{B}}$’s GFGness.

Before defining the word $z$, note that the following holds for every state
$s\in Q_{\mathcal{B}}$ that is equivalent to $q$. Recall that we assume that
$L_{{\it safe}}({\mathcal{A}}^{q})\not\subseteq L_{{\it
safe}}({\mathcal{B}}^{s})$. Hence, there is a finite nonempty word
$z_{s}\in\Sigma^{*}$ such that there is a safe run of ${\mathcal{A}}^{q}$ on
$z_{s}$, but every run of ${\mathcal{B}}^{s}$ on $z_{s}$ is not safe. To see
why, assume contrarily that for every finite nonempty word
$z_{s}\in\Sigma^{*}$, if $q$ has a safe run on $z_{s}$, then there is also a
safe run of ${\mathcal{B}}^{s}$ on $z_{s}$. Then, consider an infinite word
$x=\sigma_{1}\cdot\sigma_{2}\cdot\sigma_{3}\cdots\in L_{{\it
safe}}({\mathcal{A}}^{q})\setminus L_{{\it safe}}({\mathcal{B}}^{s})$. For all
$i\geq 1$, the state $q$ has a safe run on the prefix $x[1,i]$. Therefore, by
the assumption, so does $s$. Now, as ${\mathcal{B}}$ is nice, in particular,
safe deterministic, it follows that the safe runs of $s$ on different prefixes
of $x$ extend each other. Hence, one can iteratively define a safe run
$r=s_{0},s_{1},s_{2},\ldots$ of $s$ on $x$ by taking $s_{i}$ to be the state
that is reachable by reading $x[1,i]$ from $s$ via a safe run, which
contradicts the fact that $x\notin L_{{\it safe}}({\mathcal{B}}^{s})$.

Now back to our Proposition. We can define the word $z\in\Sigma^{\omega}$ as
follows. Let $s_{0}=g(u)$. Since $L_{{\it
safe}}({\mathcal{A}}^{q})\not\subseteq L_{{\it safe}}({\mathcal{B}}^{s_{0}})$,
then as argued above, there is a finite nonempty word $z_{1}$ such that there
is a safe run of ${\mathcal{A}}^{q}$ on $z_{1}$, but every run of
${\mathcal{B}}^{s_{0}}$ on $z_{1}$ is not safe. In particular, the run of
${\mathcal{B}}^{s_{0}}$ that is induced by $g$, namely $g(u),g(u\cdot
z_{1}[1,1]),g(u\cdot z_{1}[1,2]),\ldots,g(u\cdot z_{1})$, traverses an
$\alpha$-transition. Since ${\mathcal{A}}$ is normal, we can define $z_{1}$ so
the safe run of ${\mathcal{A}}^{q}$ on $z_{1}$ ends in $q$. Let
$s_{1}=g(u\cdot z_{1})$. We have so far two finite runs:
$q\xrightarrow{z_{1}}q$ in ${\mathcal{A}}$ and $s_{0}\xrightarrow{z_{1}}s_{1}$
in ${\mathcal{B}}$. The first run is safe, and the second is the non-safe run
induced by $g$ on the input word $u\cdot z_{1}$. Now, since $q\sim s_{0}$,
then again by Proposition 2 we have that $q\sim s_{1}$, and by applying the
same considerations, we can define a finite nonempty word $z_{2}$ and
$s_{2}=g(u\cdot z_{1}\cdot z_{2})$ such that $q\xrightarrow{z_{2}}q$ and
$s_{1}\xrightarrow{z_{2}}s_{2}$. Here too, the first run is safe, and the
second is the non-safe run induced by $g$ on the input word $u\cdot z_{1}\cdot
z_{2}$. Proceeding similarly, we can iteratively define an infinite word
$z=z_{1}\cdot z_{2}\cdot z_{3}\cdots$, where for all $i\geq 1$, we have that
$q\xrightarrow{z_{i}}q$ and $s_{i-1}\xrightarrow{z_{i}}s_{i}=g(u\cdot
z_{1}\cdot z_{2}\cdots z_{i})$, where the first run is safe, and the second is
the non-safe run induced by $g$ on the input word $u\cdot z_{1}\cdot
z_{2}\cdots z_{i}$. Also, $q\sim s_{i}$. On the one hand, since
$q\in\delta_{{\mathcal{A}}}(q^{0}_{\mathcal{A}},u)$ and there is a safe run of
${\mathcal{A}}^{q}$ on $z$, we have that $u\cdot z\in L({\mathcal{A}})$. On
the other hand, the run of ${\mathcal{B}}$ on the infinite word $u\cdot z$
that is induced by $g$, namely $g(u\cdot z)$, traverses $\alpha$-transitions
infinitely often, and is thus rejecting. ∎

######  Proposition .

Let ${\mathcal{A}}$ and ${\mathcal{B}}$ be equivalent nice GFG-tNCWs. For
every state $p\in Q_{{\mathcal{A}}}$, there are states $q\in
Q_{{\mathcal{A}}}$ and $s\in Q_{{\mathcal{B}}}$ such that $p\precsim q$ and
$q\approx s$.

###### Proof.

The proposition follows from the combination of Proposition 3.1 with the
transitivity of $\precsim$ and the fact $Q_{\mathcal{A}}$ and
$Q_{\mathcal{B}}$ are finite. Formally, consider the directed bipartite graph
$G=\langle Q_{{\mathcal{A}}}\cup Q_{{\mathcal{B}}},E\rangle$, where
$E\subseteq(Q_{{\mathcal{A}}}\times
Q_{{\mathcal{B}}})\cup(Q_{{\mathcal{B}}}\times Q_{{\mathcal{A}}})$ is such
that $\langle p_{1},p_{2}\rangle\in E$ iff $p_{1}\precsim p_{2}$. Proposition
3.1 implies that $E$ is total. That is, from every state in
$Q_{{\mathcal{A}}}$ there is an edge to some state in $Q_{{\mathcal{B}}}$, and
from every state in $Q_{{\mathcal{B}}}$ there is an edge to some state in
$Q_{{\mathcal{A}}}$. Since $Q_{\mathcal{A}}$ and $Q_{\mathcal{B}}$ are finite,
this implies that for every $p\in Q_{{\mathcal{A}}}$, there is a path in $G$
that starts in $p$ and reaches a state $q\in Q_{{\mathcal{A}}}$ (possibly
$q=p$) that belongs to a nonempty cycle. We take $s$ to be some state in
$Q_{\mathcal{B}}$ in this cycle. By the transitivity of $\precsim$, we have
that $p\precsim q$, $q\precsim s$, and $s\precsim q$. The last two imply that
$q\approx s$, and we are done. ∎

######  Lemma .

Consider a nice GFG-tNCW ${\mathcal{A}}$. If ${\mathcal{A}}$ is safe-
centralized and safe-minimal, then for every nice GFG-tNCW ${\mathcal{B}}$
equivalent to ${\mathcal{A}}$, there is an injection
$\eta:{\mathcal{S}}({\mathcal{A}})\to{\mathcal{S}}({\mathcal{B}})$ such that
for every safe component $T\in{\mathcal{S}}({\mathcal{A}})$, it holds that
$|T|\leq|\eta(T)|$.

###### Proof.

We define $\eta$ as follows. Consider a safe component
$T\in{\mathcal{S}}({\mathcal{A}})$. Let $p_{T}$ be some state in $T$. By
Proposition 3.1, there are states $q_{T}\in Q_{{\mathcal{A}}}$ and $s_{T}\in
Q_{{\mathcal{B}}}$ such that $p_{T}\precsim q_{T}$ and $q_{T}\approx s_{T}$.
Since ${\mathcal{A}}$ is safe-centralized, the states $p_{T}$ and $q_{T}$ are
in the same safe component, thus $q_{T}\in T$. We define $\eta(T)$ to be the
safe component of $s_{T}$ in ${\mathcal{B}}$. We show that $\eta$ is an
injection; that is, for every two distinct safe components $T_{1}$ and $T_{2}$
in ${\mathcal{S}}({\mathcal{A}})$, it holds that $\eta(T_{1})\neq\eta(T_{2})$.
Assume by way of contradiction that $T_{1}$ and $T_{2}$ are such that
$s_{T_{1}}$ and $s_{T_{2}}$, chosen as described above, are in the same safe
component of ${\mathcal{B}}$. Then, there is a safe run from $s_{T_{1}}$ to
$s_{T_{2}}$. Since $s_{T_{1}}\approx q_{T_{1}}$, an iterative application of
Proposition 3.1 implies that there is a safe run from $q_{T_{1}}$ to some
state $q$ such that $q\approx s_{T_{2}}$. Since the run from $q_{T_{1}}$ to
$q$ is safe, the states $q_{T_{1}}$ and $q$ are in the same safe component,
and so $q\in T_{1}$. Since $q_{T_{2}}\approx s_{T_{2}}$, then $q\approx
q_{T_{2}}$. Since ${\mathcal{A}}$ is safe-centralized, the latter implies that
$q$ and $q_{T_{2}}$ are in the same safe component, and so $q\in T_{2}$, and
we have reached a contradiction.

It is left to prove that for every safe component
$T\in{\mathcal{S}}({\mathcal{A}})$, it holds that $|T|\leq|\eta(T)|$. Let
$T\in{\mathcal{S}}({\mathcal{A}})$ be a safe component of ${\mathcal{A}}$. By
the definition of $\eta$, there are $q_{T}\in T$ and $s_{T}\in\eta(T)$ such
that $q_{T}\approx s_{T}$. Since $T$ is a safe component, there is a safe run
$q_{0},q_{1},\ldots,q_{m}$ of ${\mathcal{A}}$ that starts in $q_{T}$ and
traverses all the states in $T$. Since ${\mathcal{A}}$ is safe-minimal, no two
states in $T$ are strongly equivalent. Therefore, there is a subset
$I\subseteq\\{0,1,\ldots,m\\}$ of indices, with $|I|=|T|$, such that for every
two different indices $i_{1},i_{2}\in I$, it holds that $q_{i_{1}}\not\approx
q_{i_{2}}$. By applying Proposition 3.1 iteratively, there is a safe run
$s_{0},s_{1},\ldots,s_{m}$ of ${\mathcal{B}}$ that starts in $s_{T}$ and such
that for every $0\leq i\leq m$, it holds that $q_{i}\approx s_{i}$. Since the
run is safe and ${\mathcal{B}}$ is normal, it stays in $\eta(T)$. Then,
however, for every two different indices $i_{1},i_{2}\in I$, we have that
$s_{i_{1}}\not\approx s_{i_{2}}$, and so $s_{i_{1}}\neq s_{i_{2}}$. Hence,
$|\eta(T)|\geq|I|=|T|$. ∎

We can now prove that the additional two properties imply the minimality of
nice GFG-tNCWs.

######  Theorem .

Consider a nice GFG-tNCW ${\mathcal{A}}$. If ${\mathcal{A}}$ is safe-
centralized and safe-minimal, then ${\mathcal{A}}$ is a minimal GFG-tNCW for
$L({\mathcal{A}})$.

###### Proof.

Let ${\mathcal{B}}$ be a GFG-tNCW equivalent to ${\mathcal{A}}$. By Theorem 2,
we can assume that ${\mathcal{B}}$ is nice. Indeed, otherwise we can make it
nice without increasing its state space. Then, by Lemma 3.1, there is an
injection $\eta:{\mathcal{S}}({\mathcal{A}})\to{\mathcal{S}}({\mathcal{B}})$
such that for every safe component $T\in{\mathcal{S}}({\mathcal{A}})$, it
holds that $|T|\leq|\eta(T)|$. Hence,

$|{\mathcal{A}}|=\sum\limits_{T\in{\mathcal{S}}({\mathcal{A}})}|T|\leq\sum\limits_{T\in{\mathcal{S}}({\mathcal{A}})}|\eta(T)|\leq\sum\limits_{{T}^{\prime}\in{\mathcal{S}}({\mathcal{B}})}|{T}^{\prime}|=|{\mathcal{B}}|.$

Indeed, the first inequality follows from the fact $|T|\leq|\eta(T)|$, and the
second inequality follows from the fact that $\eta$ is injective. ∎

######  Remark .

Recall that we assume that the transition function of GFG-tNCWs is total.
Clearly, a non-total GFG-tNCW can be made total by adding a rejecting sink.
One may wonder whether the additional state that this process involves
interferes with our minimality proof. The answer is negative: if
${\mathcal{B}}$ in Theorem 3.1 is not total, then, by Proposition 3.1,
${\mathcal{A}}$ has a state $s$ such that $q_{rej}\precsim s$, where $q_{rej}$
is a rejecting sink we need to add to ${\mathcal{B}}$ if we want to make it
total. Thus, $L({\mathcal{A}}^{s})=\emptyset$, and we may not count the state
$s$ if we allow GFG-tNCWs without a total transition function. ∎

###  3.2. Safe Centralization

Consider a nice GFG-tNCW
${\mathcal{A}}=\langle\Sigma,Q_{{\mathcal{A}}},q^{0}_{{\mathcal{A}}},\delta_{{\mathcal{A}}},\alpha_{{\mathcal{A}}}\rangle$.
Recall that ${\mathcal{A}}$ is safe-centralized if for every two states
$q,s\in Q_{\mathcal{A}}$, if $q\precsim s$, then $q$ and $s$ are in the same
safe component. In this section we describe how to turn a given nice GFG-tNCW
into a nice safe-centralized GFG-tNCW. The resulted tNCW is also going to be
$\alpha$-homogenous.

Let $H\subseteq{\mathcal{S}}({\mathcal{A}})\times{\mathcal{S}}({\mathcal{A}})$
be such that for all safe components
$S,{S}^{\prime}\in{\mathcal{S}}({\mathcal{A}})$, we have that
$H(S,{S}^{\prime})$ iff there exist states $q\in S$ and
$q^{\prime}\in{S}^{\prime}$ such that $q\precsim q^{\prime}$. That is, when
$S\neq{S}^{\prime}$, then the states $q$ and $q^{\prime}$ witness that
${\mathcal{A}}$ is not safe-centralized. Recall that $q\precsim q^{\prime}$
iff $L({\mathcal{A}}^{q})=L({\mathcal{A}}^{q^{\prime}})$ and $L_{{\it
safe}}({\mathcal{A}}^{q})\subseteq L_{{\it
safe}}({\mathcal{A}}^{q^{\prime}})$. Since language containment for GFG-tNCWs
can be checked in polynomial time [19, 24], the first condition can be checked
in polynomial time. Since ${\mathcal{A}}$ is safe deterministic, the second
condition reduces to language containment between deterministic automata, and
can also be checked in polynomial time. Hence, the relation $H$ can be
computed in polynomial time.

######  Lemma .

Consider safe components $S,{S}^{\prime}\in{\mathcal{S}}({\mathcal{A}})$ such
that $H(S,{S}^{\prime})$. Then, for every $p\in S$ there is
$p^{\prime}\in{S}^{\prime}$ such that $p\precsim p^{\prime}$.

###### Proof.

Since $H(S,{S}^{\prime})$, then, by definition, there are states $q\in S$ and
$q^{\prime}\in{S}^{\prime}$, such that $q\precsim q^{\prime}$. Let $p$ be a
state in $S$. Since $S$ is a safe component, there is a safe run from $q$ to
$p$ in $S$. Since $q\precsim q^{\prime}$, an iterative application of
Proposition 3.1 implies that there is a safe run $r$ from $q^{\prime}$ to some
state $p^{\prime}$ for which $p\precsim p^{\prime}$. As ${\mathcal{A}}$ is
normal and $r$ is safe, the run $r$ stays in $S^{\prime}$; in particular,
$p^{\prime}\in S^{\prime}$, and we are done. ∎

######  Lemma .

The relation $H$ is transitive: for every safe components
$S,{S}^{\prime},{S}^{\prime\prime}\in{\mathcal{S}}({\mathcal{A}})$, if
$H(S,{S}^{\prime})$ and $H({S}^{\prime},{S}^{\prime\prime})$, then
$H(S,{S}^{\prime\prime})$.

###### Proof.

Let $S,{S}^{\prime},{S}^{\prime\prime}\in{\mathcal{S}}({\mathcal{A}})$ be safe
components of ${\mathcal{A}}$ such that $H(S,{S}^{\prime})$ and
$H({S}^{\prime},{S}^{\prime\prime})$. Since $H(S,{S}^{\prime})$, there are
states $q\in S$ and $q^{\prime}\in{S}^{\prime}$ such that $q\precsim
q^{\prime}$. Now, since $H({S}^{\prime},{S}^{\prime\prime})$, we get by Lemma
3.2 that for all states in ${S}^{\prime}$, in particular for $q^{\prime}$,
there is a state $q^{\prime\prime}\in{S}^{\prime\prime}$ such that
$q^{\prime}\precsim q^{\prime\prime}$. The transitivity of $\precsim$ then
implies that $q\precsim q^{\prime\prime}$, and so $H(S,{S}^{\prime\prime})$. ∎

We say that a set ${{\mathcal{S}}}\subseteq{\mathcal{S}}({\mathcal{A}})$ is a
_frontier of ${\mathcal{A}}$_ if for every safe component
$S\in{\mathcal{S}}({\mathcal{A}})$, there is a safe component
${S}^{\prime}\in{{\mathcal{S}}}$ with $H(S,{S}^{\prime})$, and for all safe
components $S,{S}^{\prime}\in{{\mathcal{S}}}$ such that $S\neq{S}^{\prime}$,
we have that $\neg H(S,{S}^{\prime})$ and $\neg H({S}^{\prime},S)$. Once $H$
is calculated, a frontier of ${\mathcal{A}}$ can be found in linear time. For
example, as $H$ is transitive, we can take one vertex from each ergodic SCC in
the graph $\langle{\mathcal{S}}({\mathcal{A}}),H\rangle$. Note that all
frontiers of ${\mathcal{A}}$ are of the same size, namely the number of
ergodic SCCs in this graph.

Given a frontier ${\mathcal{S}}$ of ${\mathcal{A}}$, we define the automaton
${\mathcal{B}}_{{\mathcal{S}}}=\langle\Sigma,Q_{{\mathcal{S}}},q^{0}_{{\mathcal{S}}},\delta_{{\mathcal{S}}},\alpha_{{\mathcal{S}}}\rangle$,
where $Q_{{\mathcal{S}}}=\\{q\in Q_{{\mathcal{A}}}:q\in S\text{ for some
}S\in{{\mathcal{S}}}\\}$, and the other elements are defined as follows. The
initial state $q^{0}_{{\mathcal{S}}}$ is chosen such that
$q^{0}_{{\mathcal{S}}}\sim_{\mathcal{A}}q^{0}_{\mathcal{A}}$. Specifically, if
$q^{0}_{\mathcal{A}}\in Q_{{\mathcal{S}}}$, we take
$q^{0}_{{\mathcal{S}}}=q^{0}_{\mathcal{A}}$. Otherwise, by Lemma 3.2 and the
definition of ${\mathcal{S}}$, there is a state $q^{\prime}\in
Q_{{\mathcal{S}}}$ such that $q^{0}_{{\mathcal{A}}}\precsim q^{\prime}$, and
we take $q^{0}_{{\mathcal{S}}}=q^{\prime}$. The transitions in
${\mathcal{B}}_{{\mathcal{S}}}$ are either $\bar{\alpha}$-transitions of
${\mathcal{A}}$, or $\alpha$-transitions that we add among the safe components
in ${\mathcal{S}}$ in a way that preserves language equivalence. Formally,
consider a state $q\in Q_{{\mathcal{S}}}$ and a letter $\sigma\in\Sigma$. If
$\delta^{\bar{\alpha}}_{\mathcal{A}}(q,\sigma)\neq\emptyset$, then
$\delta^{\bar{\alpha}}_{\mathcal{S}}(q,\sigma)=\delta^{\bar{\alpha}}_{\mathcal{A}}(q,\sigma)$
and $\delta^{\alpha}_{\mathcal{S}}(q,\sigma)=\emptyset$. If
$\delta^{\bar{\alpha}}_{\mathcal{A}}(q,\sigma)=\emptyset$, then
$\delta^{\bar{\alpha}}_{\mathcal{S}}(q,\sigma)=\emptyset$ and
$\delta^{\alpha}_{\mathcal{S}}(q,\sigma)=\\{q^{\prime}\in
Q_{\mathcal{S}}:\mbox{ there is
}q^{\prime\prime}\in\delta^{\alpha}_{\mathcal{A}}(q,\sigma)\mbox{ such that
}q^{\prime}\sim_{\mathcal{A}}q^{\prime\prime}\\}$. Note that
${\mathcal{B}}_{{\mathcal{S}}}$ is total and $\alpha$-homogenous.

######  Example .

Consider the tDCW ${\mathcal{A}}$ appearing in Figure 2. Recall that the
dashed transitions are $\alpha$-transitions. Since ${\mathcal{A}}$ is normal
and deterministic, it is nice. By removing the $\alpha$-transitions of
${\mathcal{A}}$, we get the safe components described in Figure 3.

Figure 3. The safe components of ${\mathcal{A}}$.

Since $q_{2}\precsim q_{0}$, we have that ${\mathcal{A}}$ has a single
frontier ${\mathcal{S}}=\\{\\{q_{0},q_{1}\\}\\}$. The automaton
${\mathcal{B}}_{{\mathcal{S}}}$ appears in Figure 4. As all the states of
${\mathcal{A}}$ are equivalent, we direct a $\sigma$-labeled
$\alpha$-transition to $q_{0}$ and to $q_{1}$, for every state with no
$\sigma$-labeled transition in ${\mathcal{S}}$. ∎

Figure 4. The tNCW ${\mathcal{B}}_{\mathcal{S}}$, for
${\mathcal{S}}={\\{\\{q_{0},q_{1}\\}\\}}$.

We now prove some properties that will enable us to conclude that a nice GFG-
tNCW ${\mathcal{A}}$ can be turned into a nice, safe-centralized, and
$\alpha$-homogenous GFG-tNCW by constructing ${\mathcal{B}}_{{\mathcal{S}}}$
for some frontier ${\mathcal{S}}$ of ${\mathcal{A}}$. We first extend
Proposition 2 to the setting of ${\mathcal{A}}$ and
${\mathcal{B}}_{\mathcal{S}}$.

######  Proposition .

Consider states $q$ and $s$ of ${\mathcal{A}}$ and
${\mathcal{B}}_{{\mathcal{S}}}$, respectively, a letter $\sigma\in\Sigma$, and
transitions $\langle q,\sigma,q^{\prime}\rangle$ and $\langle
s,\sigma,s^{\prime}\rangle$ of ${\mathcal{A}}$ and
${\mathcal{B}}_{{\mathcal{S}}}$, respectively. If $q\sim_{{\mathcal{A}}}s$,
then $q^{\prime}\sim_{{\mathcal{A}}}s^{\prime}$.

###### Proof.

If $\langle s,\sigma,s^{\prime}\rangle$ is an $\bar{\alpha}$-transition of
${\mathcal{B}}_{{\mathcal{S}}}$, then, by the definition of
$\Delta_{{\mathcal{S}}}$, it is also an $\bar{\alpha}$-transition of
${\mathcal{A}}$. Hence, since $q\sim_{{\mathcal{A}}}s$ and ${\mathcal{A}}$ is
nice, in particular, semantically deterministic, we get by Proposition 2 that
$q^{\prime}\sim_{{\mathcal{A}}}s^{\prime}$. If $\langle
s,\sigma,s^{\prime}\rangle$ is an $\alpha$-transition of
${\mathcal{B}}_{{\mathcal{S}}}$, then, by the definition of
$\Delta_{{\mathcal{S}}}$, there is some
$s^{\prime\prime}\in\delta_{{\mathcal{A}}}(s,\sigma)$ with
$s^{\prime}\sim_{{\mathcal{A}}}s^{\prime\prime}$. Again, since
$q\sim_{{\mathcal{A}}}s$ and ${\mathcal{A}}$ is semantically deterministic, we
have by Proposition 2 that $s^{\prime\prime}\sim_{{\mathcal{A}}}q^{\prime}$,
and thus $s^{\prime}\sim_{{\mathcal{A}}}q^{\prime}$. ∎

Note that an iterative application of Proposition 3.2 implies that runs of
${\mathcal{A}}$ and ${\mathcal{B}}_{\mathcal{S}}$ on the same finite prefix
end in ${\mathcal{A}}$-equivalent states. Hence, as safe runs in
${\mathcal{B}}_{\mathcal{S}}$ exist also in ${\mathcal{A}}$, one can show that
$L({\mathcal{B}}_{\mathcal{S}})\subseteq L({\mathcal{A}})$. Conversely, one
can show that there is a strategy $g:\Sigma^{*}\to Q_{\mathcal{S}}$ such that
following $g$ results in accepting all words $w\in L({\mathcal{A}})$ in
${\mathcal{B}}_{\mathcal{S}}$. Essentially, $g$ follows a GFG strategy $f$ for
${\mathcal{A}}$; that is, whenever $g$ needs to make some nondeterministic
choice after reading a prefix $x$, it moves to a state $q^{\prime}$ with
$f(x)\precsim_{\mathcal{A}}q^{\prime}$. As $f(w)$ is accepting for all $w\in
L({\mathcal{A}})$, then it eventually becomes safe, and thus $g(w)$ cannot
make infinitely many bad nondeterministic choices. The following proposition
formalizes the above idea and generalizes it to all pairs of equivalent
states.

######  Proposition .

Let $q$ and $s$ be states of ${\mathcal{A}}$ and
${\mathcal{B}}_{{\mathcal{S}}}$, respectively, with $q\sim_{{\mathcal{A}}}s$.
It holds that ${\mathcal{B}}_{{\mathcal{S}}}^{s}$ is a GFG-tNCW equivalent to
${\mathcal{A}}^{q}$.

###### Proof.

We first prove that $L({\mathcal{B}}_{{\mathcal{S}}}^{s})\subseteq
L({\mathcal{A}}^{q})$. Consider a word $w=\sigma_{1}\sigma_{2}\cdots\in
L({\mathcal{B}}_{{\mathcal{S}}}^{s})$. Let $s_{0},s_{1},s_{2},\ldots$ be an
accepting run of ${\mathcal{B}}_{{\mathcal{S}}}^{s}$ on $w$. Then, there is
$i\geq 0$ such that $s_{i},s_{i+1},\ldots$ is a safe run of
${\mathcal{B}}_{{\mathcal{S}}}^{s_{i}}$ on the suffix $w[i+1,\infty]$. Let
$q_{0},q_{1},\ldots,q_{i}$ be a run of ${\mathcal{A}}^{q}$ on the prefix
$w[1,i]$. Since $q_{0}\sim_{{\mathcal{A}}}s_{0}$, we get, by an iterative
application of Proposition 3.2, that $q_{i}\sim_{{\mathcal{A}}}s_{i}$. In
addition, as the run of ${\mathcal{B}}_{{\mathcal{S}}}^{s_{i}}$ on the suffix
$w[i+1,\infty]$ is safe, it is also a safe run of ${\mathcal{A}}^{s_{i}}$.
Hence, $w[i+1,\infty]\in L({\mathcal{A}}^{q_{i}})$, and thus
$q_{0},q_{1},\ldots,q_{i}$ can be extended to an accepting run of
${\mathcal{A}}^{q}$ on $w$.

Next, we prove that $L({\mathcal{A}}^{q})\subseteq
L({\mathcal{B}}_{{\mathcal{S}}}^{s})$ and that
${\mathcal{B}}_{{\mathcal{S}}}^{s}$ is a GFG-tNCW. We do this by defining a
strategy $g:\Sigma^{*}\to Q_{{\mathcal{S}}}$ such that for all words $w\in
L({\mathcal{A}}^{q})$, we have that $g(w)$ is an accepting run of
${\mathcal{B}}_{{\mathcal{S}}}^{s}$ on $w$. First, $g(\epsilon)=s$. Then, for
$u\in\Sigma^{*}$ and $\sigma\in\Sigma$, we define $g(u\cdot\sigma)$ as
follows. Recall that ${\mathcal{A}}$ is nice. So, in particular,
${\mathcal{A}}^{q}$ is GFG. Let $f$ be a strategy witnessing
${\mathcal{A}}^{q}$’s GFGness. If
$\delta^{\bar{\alpha}}_{\mathcal{S}}(g(u),\sigma)\neq\emptyset$, then
$g(u\cdot\sigma)=q^{\prime}$ for some
$q^{\prime}\in\delta^{\bar{\alpha}}_{\mathcal{S}}(g(u),\sigma)$. If
$\delta^{\bar{\alpha}}_{\mathcal{S}}(g(u),\sigma)=\emptyset$, then
$g(u\cdot\sigma)=q^{\prime}$ for some state $q^{\prime}\in Q_{{\mathcal{S}}}$
such that $f(u\cdot\sigma)\precsim_{\mathcal{A}}q^{\prime}$. Note that since
${\mathcal{S}}$ is a frontier, such a state $q^{\prime}$ exists. We prove that
$g$ is consistent with $\Delta_{{\mathcal{S}}}$. In fact, we prove a stronger
claim, namely for all $u\in\Sigma^{*}$ and $\sigma\in\Sigma$, we have that
$f(u)\sim_{\mathcal{A}}g(u)$ and $\langle
g(u),\sigma,g(u\cdot\sigma)\rangle\in\Delta_{{\mathcal{S}}}$.

The proof proceeds by an induction on $|u|$. For the induction base, as
$f(\epsilon)=q$, $g(\epsilon)=s$, and $q\sim_{\mathcal{A}}s$, we are done.
Given $u$ and $\sigma$, consider a transition $\langle
g(u),\sigma,s^{\prime}\rangle\in\Delta_{{\mathcal{S}}}$. Since
${\mathcal{B}}_{{\mathcal{S}}}$ is total, such a transition exists. We
distinguish between two cases. If
$\delta^{\bar{\alpha}}_{\mathcal{S}}(g(u),\sigma)\neq\emptyset$, then, as
${\mathcal{B}}_{{\mathcal{S}}}$ is $\alpha$-homogenous and safe deterministic,
the state $s^{\prime}$ is the only state in
$\delta^{\bar{\alpha}}_{\mathcal{S}}(g(u),\sigma)$. Hence, by the definition
of $g$, we have that $g(u\cdot\sigma)=s^{\prime}$ and so $\langle
g(u),\sigma,g(u\cdot\sigma)\rangle\in\Delta_{{\mathcal{S}}}$. If
$\delta^{\bar{\alpha}}_{\mathcal{S}}(g(u),\sigma)=\emptyset$, we claim that
$g(u\cdot\sigma)\sim_{\mathcal{A}}s^{\prime}$. Then, as
$s^{\prime}\in\delta^{\alpha}_{\mathcal{S}}(g(u),\sigma)$, the definition of
$\Delta_{{\mathcal{S}}}$ for the case
$\delta^{\bar{\alpha}}_{\mathcal{S}}(g(u),\sigma)=\emptyset$ implies that
$\langle g(u),\sigma,g(u\cdot\sigma)\rangle\in\Delta_{{\mathcal{S}}}$. By the
induction hypothesis, we have that $f(u)\sim_{\mathcal{A}}g(u)$. Hence, as
$\langle f(u),\sigma,f(u\cdot\sigma))\rangle\in\Delta_{\mathcal{A}}$ and
$\langle g(u),\sigma,s^{\prime}\rangle\in\Delta_{{\mathcal{S}}}$, we have, by
Proposition 3.2, that $f(u\cdot\sigma)\sim_{\mathcal{A}}s^{\prime}$. Recall
that $g$ is defined so that
$f(u\cdot\sigma)\precsim_{\mathcal{A}}g(u\cdot\sigma)$. In particular,
$f(u\cdot\sigma)\sim_{\mathcal{A}}g(u\cdot\sigma)$. Hence, by transitivity of
$\sim_{\mathcal{A}}$, we have that
$g(u\cdot\sigma)\sim_{\mathcal{A}}s^{\prime}$, and we are done. In addition,
by the induction hypothesis, we have that $f(u)\sim_{\mathcal{A}}g(u)$, and
so, in both cases, Proposition 3.2 implies that
$f(u\cdot\sigma)\sim_{{\mathcal{A}}}g(u\cdot\sigma)$.

It is left to prove that for every infinite word
$w=\sigma_{1}\sigma_{2}\cdots\in\Sigma^{\omega}$, if $w\in
L({\mathcal{A}}^{q})$, then $g(w)$ is accepting. Assume that $w\in
L({\mathcal{A}}^{q})$ and consider the run $f(w)$ of ${\mathcal{A}}^{q}$ on
$w$. Since $f(w)$ is accepting, there is $i\geq 0$ such that
$f(w[1,i]),f(w[1,i+1])\ldots$ is a safe run of ${\mathcal{A}}^{f(w[1,i])}$ on
the suffix $w[i+1,\infty]$. We prove that $g(w)$ may traverse at most one
$\alpha$-transition when it reads the suffix $w[i+1,\infty]$. Assume that
there is some $j\geq i$ such that $\langle
g(w[1,j]),\sigma_{j+1},g(w[1,j+1])\rangle\in\alpha_{\mathcal{S}}$. Then, by
$g$’s definition, we have that $f(w[1,j+1])\precsim_{\mathcal{A}}g(w[1,j+1])$.
Therefore, as ${\mathcal{B}}_{{\mathcal{S}}}$ follows the safe components in
${\mathcal{S}}$, we have that $L_{{\it
safe}}({\mathcal{A}}^{f(w[1,j+1])})\subseteq L_{{\it
safe}}({\mathcal{A}}^{g(w[1,j+1])})=L_{{\it
safe}}({\mathcal{B}}_{{\mathcal{S}}}^{g(w[1,j+1])})$, and thus
$w[j+2,\infty]\in L_{{\it
safe}}({\mathcal{B}}_{{\mathcal{S}}}^{g(w[1,j+1])})$. Since
${\mathcal{B}}_{{\mathcal{S}}}$ is $\alpha$-homogenous and safe deterministic,
there is a single run of ${\mathcal{B}}^{g(w[1,j+1])}_{{\mathcal{S}}}$ on
$w[j+2,\infty]$, and this is the run that $g$ follows. Therefore,
$g(w[1,j+1]),g(w[1,j+2]),\ldots$ is a safe run, and we are done. ∎

######  Remark .

As we argue below, for every frontier ${\mathcal{S}}$, all the states of the
tNCW ${\mathcal{B}}_{\mathcal{S}}$ are reachable. Since, however, states that
are not reachable are easy to detect and their removal does not affect
${\mathcal{B}}_{{\mathcal{S}}}$’s language, its other properties mentioned in
Proposition 3.2, and arguments that refer to its construction, we can simply
assume that all the states of ${\mathcal{B}}_{\mathcal{S}}$ are reachable.

To see that indeed all the states of the tNCW ${\mathcal{B}}_{\mathcal{S}}$
are reachable, assume by way of contradiction that there is an unreachable
state $q$ of ${\mathcal{B}}_{\mathcal{S}}$. Let $P$ be the nonempty set of
states in ${\mathcal{B}}_{\mathcal{S}}$ that are reachable in
${\mathcal{B}}_{\mathcal{S}}$ and are ${\mathcal{A}}$-equivalent to $q$. In
order to reach a contradiction, one can define, using the fact that
${\mathcal{S}}$ is a frontier, a finite word $z\in\Sigma^{*}$ such that there
is a safe run from $q$ back to $q$ on the input word $z$ and for all $p\in P$,
all runs of $p$ on $z$ are not safe. If such a word $z$ exists, then one can
show that $L({\mathcal{A}})\setminus L({\mathcal{B}}_{\mathcal{S}})$ is
nonempty, contradicting their equivalence. ∎

The following proposition shows that the modifications applied to
${\mathcal{A}}$ in order to obtain ${\mathcal{B}}_{{\mathcal{S}}}$ maintain
the useful properties of ${\mathcal{A}}$.

######  Proposition .

For every frontier ${\mathcal{S}}$, the GFG-tNCW
${\mathcal{B}}_{{\mathcal{S}}}$ is nice, safe-centralized, and
$\alpha$-homogenous.

###### Proof.

It is easy to see that the fact ${\mathcal{A}}$ is nice implies that
${\mathcal{B}}_{{\mathcal{S}}}$ is normal and safe deterministic. Also, as we
explained in Remark 3.2, all the states in ${\mathcal{B}}_{\mathcal{S}}$ are
reachable. Finally, Proposition 3.2 implies that all its states are GFG. To
conclude that ${\mathcal{B}}_{{\mathcal{S}}}$ is nice, we prove below that it
is semantically deterministic. Consider transitions $\langle
q,\sigma,s_{1}\rangle$ and $\langle q,\sigma,s_{2}\rangle$ in
$\Delta_{{\mathcal{S}}}$. We need to show that
$s_{1}\sim_{{\mathcal{B}}_{{\mathcal{S}}}}s_{2}$. By the definition of
$\Delta_{{\mathcal{S}}}$, there are transitions $\langle
q,\sigma,s^{\prime}_{1}\rangle$ and $\langle q,\sigma,s^{\prime}_{2}\rangle$
in $\Delta_{\mathcal{A}}$ for states $s^{\prime}_{1}$ and $s^{\prime}_{2}$
such that $s_{1}\sim_{\mathcal{A}}s^{\prime}_{1}$ and
$s_{2}\sim_{\mathcal{A}}s^{\prime}_{2}$. As ${\mathcal{A}}$ is semantically
deterministic, we have that $s^{\prime}_{1}\sim_{\mathcal{A}}s^{\prime}_{2}$,
thus by transitivity of $\sim_{\mathcal{A}}$, we get that
$s_{1}\sim_{\mathcal{A}}s_{2}$. Then, Proposition 3.2 implies that
$L({\mathcal{A}}^{s_{1}})=L({\mathcal{B}}^{s_{1}}_{{\mathcal{S}}})$ and
$L({\mathcal{A}}^{s_{2}})=L({\mathcal{B}}^{s_{2}}_{{\mathcal{S}}})$, and so we
get that $s_{1}\sim_{{\mathcal{B}}_{{\mathcal{S}}}}s_{2}$. Thus,
${\mathcal{B}}_{{\mathcal{S}}}$ is semantically deterministic.

As we noted in the definition of its transitions,
${\mathcal{B}}_{{\mathcal{S}}}$ is $\alpha$-homogenous. It is thus left to
prove that ${\mathcal{B}}_{{\mathcal{S}}}$ is safe-centralized. Let $q$ and
$s$ be states of ${\mathcal{B}}_{{\mathcal{S}}}$ such that
$q\precsim_{{\mathcal{B}}_{{\mathcal{S}}}}s$; that is,
$L({\mathcal{B}}^{q}_{{\mathcal{S}}})=L({\mathcal{B}}^{s}_{{\mathcal{S}}})$
and $L_{{\it safe}}({\mathcal{B}}^{q}_{{\mathcal{S}}})\subseteq L_{{\it
safe}}({\mathcal{B}}^{s}_{{\mathcal{S}}})$. Let $S,T\in{\mathcal{S}}$ be the
safe components of $q$ and $s$, respectively. We need to show that $S=T$. By
Proposition 3.2, we have that
$L({\mathcal{A}}^{q})=L({\mathcal{B}}^{q}_{{\mathcal{S}}})$ and
$L({\mathcal{A}}^{s})=L({\mathcal{B}}^{s}_{{\mathcal{S}}})$. As
${\mathcal{B}}_{{\mathcal{S}}}$ follows the safe components in
${{\mathcal{S}}}$, we have that $L_{{\it safe}}({\mathcal{A}}^{q})=L_{{\it
safe}}({\mathcal{B}}^{q}_{{\mathcal{S}}})$ and $L_{{\it
safe}}({\mathcal{A}}^{s})=L_{{\it safe}}({\mathcal{B}}^{s}_{{\mathcal{S}}})$.
Hence, $q\precsim_{{\mathcal{A}}}s$, implying $H(S,T)$. Since ${\mathcal{S}}$
is a frontier, this is possible only when $S=T$, and we are done. ∎

######  Theorem .

Every nice GFG-tNCW can be turned in polynomial time into an equivalent nice,
safe-centralized, and $\alpha$-homogenous GFG-tNCW.

###  3.3. Safe-Minimization

In the setting of finite words, a quotient automaton is obtained by merging
equivalent states, and is guaranteed to be minimal. In the setting of co-Büchi
automata, it may not be possible to define an equivalent language on top of
the quotient automaton. For example, all the states in the GFG-tNCW
${\mathcal{A}}$ in Figure 2 are equivalent, and still it is impossible to
define its language on top of a single-state tNCW. In this section we show
that when we start with a nice, safe-centralized, and $\alpha$-homogenous GFG-
tNCW ${\mathcal{B}}$, the transition to a quotient automaton, namely merging
of strongly-equivalent states, is well defined and results in a GFG-tNCW
equivalent to ${\mathcal{B}}$ that attains all the helpful properties of
${\mathcal{B}}$, and is also safe-minimal666In fact, $\alpha$-homogeneity is
not required, but as the GFG-tNCW ${\mathcal{B}}_{\mathcal{S}}$ obtained in
Section 3.2 is $\alpha$-homogenous, which simplifies the proof, we are going
to rely on it.. Then, by Theorem 3.1, the obtained GFG-tNCW is also minimal.

Consider a nice, safe-centralized, and $\alpha$-homogenous GFG-tNCW
${\mathcal{B}}=\langle\Sigma,Q,q_{0},\delta,\alpha\rangle$. For a state $q\in
Q$, define $[q]=\\{q^{\prime}\in Q:q\approx_{{\mathcal{B}}}q^{\prime}\\}$. We
define the tNCW
${\mathcal{C}}=\langle\Sigma,Q_{\mathcal{C}},[q_{0}],\delta_{{\mathcal{C}}},\alpha_{{\mathcal{C}}}\rangle$
as follows. First, $Q_{\mathcal{C}}=\\{[q]:q\in Q\\}$. Then, the transition
function is such that $\langle[q],\sigma,[p]\rangle\in\Delta_{\mathcal{C}}$
iff there are $q^{\prime}\in[q]$ and $p^{\prime}\in[p]$ such that $\langle
q^{\prime},\sigma,p^{\prime}\rangle\in\Delta$, and
$\langle[q],\sigma,[p]\rangle\in\alpha_{\mathcal{C}}$ iff $\langle
q^{\prime},\sigma,p^{\prime}\rangle\in\alpha$. Note that ${\mathcal{B}}$ being
$\alpha$-homogenous implies that $\alpha_{\mathcal{C}}$ is well defined; that
is, independent of the choice of $q^{\prime}$ and $p^{\prime}$. To see why,
assume that $\langle q^{\prime},\sigma,p^{\prime}\rangle\in\bar{\alpha}$, and
let $q^{\prime\prime}$ be a state in $[q]$. As
$q^{\prime}\approx_{\mathcal{B}}q^{\prime\prime}$, we have, by Proposition
3.1, that there is $p^{\prime\prime}\in[p]$ such that $\langle
q^{\prime\prime},\sigma,p^{\prime\prime}\rangle\in\bar{\alpha}$. Thus, as
${\mathcal{B}}$ is $\alpha$-homogenous, there is no $\sigma$-labeled
$\alpha$-transition from $q^{\prime\prime}$ in ${\mathcal{B}}$. In particular,
there is no $\sigma$-labeled $\alpha$-transition from $q^{\prime\prime}$ to a
state in $[p]$. Note that, by the above, the tNCW ${\mathcal{C}}$ is
$\alpha$-homogenous. Also, if $\langle[q],\sigma,[p]\rangle$ is an
$\bar{\alpha}$-transition of ${\mathcal{C}}$, then for every
$q^{\prime}\in[q]$, there is $p^{\prime}\in[p]$ such that $\langle
q^{\prime},\sigma,p^{\prime}\rangle$ is an $\bar{\alpha}$-transition of
${\mathcal{B}}$. The latter implies by induction the $\supseteq$-direction in
the following proposition, stating that a safe run in ${\mathcal{C}}$ induces
a safe run in ${\mathcal{B}}$. The $\subseteq$-direction follows immediately
from the definition of ${\mathcal{C}}$.

######  Proposition .

For every $[p]\in Q_{{\mathcal{C}}}$ and every $s\in[p]$, it holds that
$L_{{\it safe}}({\mathcal{B}}^{s})=L_{{\it safe}}({\mathcal{C}}^{[p]})$.

We extend Propositions 2 and 3.2 to the setting of ${\mathcal{B}}$ and
${\mathcal{C}}$:

######  Proposition .

Consider states $s\in Q$ and $[p]\in Q_{\mathcal{C}}$, a letter
$\sigma\in\Sigma$, and transitions $\langle s,\sigma,s^{\prime}\rangle$ and
$\langle[p],\sigma,[p^{\prime}]\rangle$ of ${\mathcal{B}}$ and
${\mathcal{C}}$, respectively. If $s\sim p$, then $s^{\prime}\sim p^{\prime}$.

###### Proof.

As $\langle[p],\sigma,[p^{\prime}]\rangle$ is a transition of ${\mathcal{C}}$,
there are states $t\in[p]$ and $t^{\prime}\in[p^{\prime}]$, such that $\langle
t,\sigma,t^{\prime}\rangle\in\Delta$. If $s\sim p$, then $s\sim t$. Since
${\mathcal{B}}$ is nice, in particular, semantically deterministic, and
$\langle s,\sigma,s^{\prime}\rangle\in\Delta$, we get by Proposition 2 that
$s^{\prime}\sim t^{\prime}$. Thus, as $t^{\prime}\sim p^{\prime}$, we are
done. ∎

It is not hard to see that $L({\mathcal{B}})\subseteq L({\mathcal{C}})$.
Indeed, an accepting run $q_{0},q_{1},q_{2},\ldots$ in ${\mathcal{B}}$ induces
the run $[q_{0}],[q_{1}],[q_{2}],\ldots$ in ${\mathcal{C}}$. The harder
direction is to show that $L({\mathcal{C}})\subseteq L({\mathcal{B}})$. Note
that an iterative application of Proposition 3.3 implies that runs of
${\mathcal{B}}$ and ${\mathcal{C}}$ on the same finite prefix end in states
$s\in Q$ and $[p]\in Q_{\mathcal{C}}$ with $s\sim p$. Hence, as safe runs in
${\mathcal{C}}$ induce safe runs in ${\mathcal{B}}$, one can show that
$L({\mathcal{C}})\subseteq L({\mathcal{B}})$. Formally, we have the following.

######  Proposition .

For every $[p]\in Q_{{\mathcal{C}}}$ and $s\in[p]$, we have that
${\mathcal{C}}^{[p]}$ is a GFG-tNCW equivalent to ${\mathcal{B}}^{s}$.

###### Proof.

We first prove that $L({\mathcal{C}}^{[p]})\subseteq L({\mathcal{B}}^{s})$.
Consider a word $w=\sigma_{1}\sigma_{2}\cdots\in L({\mathcal{C}}^{[p]})$. Let
$[p_{0}],[p_{1}],[p_{2}],\ldots$ be an accepting run of ${\mathcal{C}}^{[p]}$
on $w$. Then, there is $i\geq 0$ such that $[p_{i}],[p_{i+1}],\ldots$ is a
safe run of ${\mathcal{C}}^{[p_{i}]}$ on the suffix $w[i+1,\infty]$. Let
$s_{0},s_{1},\ldots,s_{i}$ be a run of ${\mathcal{B}}^{s}$ on the prefix
$w[1,i]$. Note that $s_{0}=s$. Since $s_{0}\in[p_{0}]$, we have that
$s_{0}\sim p_{0}$, and thus an iterative application of Proposition 3.3
implies that $s_{i}\sim p_{i}$. In addition, as $w[i+1,\infty]$ is in $L_{{\it
safe}}({\mathcal{C}}^{[p_{i}]})$, we get, by Proposition 3.3, that
$w[i+1,\infty]\in L_{{\it safe}}({\mathcal{B}}^{p_{i}})$. Since $L_{{\it
safe}}({\mathcal{B}}^{p_{i}})\subseteq L({\mathcal{B}}^{p_{i}})$ and
$s_{i}\sim p_{i}$, we have that $w[i+1,\infty]\in L({\mathcal{B}}^{s_{i}})$.
Hence, $s_{0},s_{1},\ldots,s_{i}$ can be extended to an accepting run of
${\mathcal{B}}^{s}$ on $w$.

Next, we prove that $L({\mathcal{B}}^{s})\subseteq L({\mathcal{C}}^{[p]})$ and
that ${\mathcal{C}}^{[p]}$ is a GFG-tNCW. We do this by defining a strategy
$h:\Sigma^{*}\to Q_{\mathcal{C}}$ such that for all words $w\in
L({\mathcal{B}}^{s})$, we have that $h(w)$ is an accepting run of
${\mathcal{C}}^{[p]}$ on $w$. We define $h$ as follows. Recall that
${\mathcal{B}}$ is nice. So, in particular, ${\mathcal{B}}^{s}$ is GFG. Let
$g$ be a strategy witnessing ${\mathcal{B}}^{s}$’s GFGness. We define
$h(u)=[g(u)]$, for every finite word $u\in\Sigma^{*}$. Consider a word $w\in
L({\mathcal{B}}^{s})$, and consider the accepting run
$g(w)=g(w[1,0]),g(w[1,1]),g(w[1,2]),\ldots$ of ${\mathcal{B}}^{s}$ on $w$.
Note that by the definition of ${\mathcal{C}}$, we have that
$h(w)=[g(w[1,0])],[g(w[1,1])],[g(w[1,2])],\ldots$ is an accepting run of
${\mathcal{C}}^{[p]}$ on $w$, and so we are done. ∎

The following proposition shows that the transition from ${\mathcal{B}}$ to
${\mathcal{C}}$ maintains the useful properties of ${\mathcal{B}}$. The
considerations are similar to these applied in the proof of Proposition 3.2.
In particular, for safe-minimality, note that for states $q$ and $s$ of
${\mathcal{B}}$, we have that $[q]\approx[s]$ iff $[q]\preceq[s]$ and
$[s]\preceq[q]$. Thus, it is sufficient to prove that if $[q]\preceq[s]$, then
$q\preceq s$.

######  Proposition .

The GFG-tNCW ${\mathcal{C}}$ is nice, safe-centralized, safe-minimal, and
$\alpha$-homogenous.

###### Proof.

To begin with, as ${\mathcal{B}}$ is nice, it is easy to see that all the
states in ${\mathcal{C}}$ are reachable. In addition, Proposition 3.3 implies
that all its states are GFG. We show next that ${\mathcal{C}}$ is safe
deterministic. Let $\langle[q],\sigma,[s_{1}]\rangle$ and
$\langle[q],\sigma,[s_{2}]\rangle$ be $\bar{\alpha}$-transitions of
${\mathcal{C}}$, and let
$q^{\prime},q^{\prime\prime}\in[q],s^{\prime}_{1}\in[s_{1}],s^{\prime}_{2}\in[s_{2}]$
be such that $t_{1}=\langle q^{\prime},\sigma,s^{\prime}_{1}\rangle$ and
$t_{2}=\langle q^{\prime\prime},\sigma,s^{\prime}_{2}\rangle$ are
$\bar{\alpha}$-transitions of ${\mathcal{B}}$. Now, as $q^{\prime}\approx
q^{\prime\prime}$ and ${\mathcal{B}}$ is nice, in particular, safe
deterministic, Proposition 3.1 implies that $s^{\prime}_{1}\approx
s^{\prime}_{2}$, and thus ${\mathcal{C}}$ is safe deterministic. Next, we
prove that ${\mathcal{C}}$ is normal. Consider a safe run
$[p_{0}],[p_{1}],\ldots,[p_{n}]$ of ${\mathcal{C}}^{[p_{0}]}$ on the finite
word $w=\sigma_{1}\sigma_{2}\cdots\sigma_{n}\in\Sigma^{*}$. We need to show
that there is a safe run from $[p_{n}]$ to $[p_{0}]$ in ${\mathcal{C}}$. As
mentioned in ${\mathcal{C}}$’s definition, a safe run in ${\mathcal{C}}$
induces a safe run in ${\mathcal{B}}$. Thus, there is a safe run
$s_{0},s_{1},\ldots,s_{n}$ of ${\mathcal{B}}^{s_{0}}$ on $w$, where
$s_{0}\in[p_{0}]$ and $s_{n}\in[p_{n}]$. Now as ${\mathcal{B}}$ is nice, in
particular, normal, we have that there is a safe run
$r_{0},r_{1},\ldots,r_{m}$ of ${\mathcal{B}}^{r_{0}}$ on
$w^{\prime}=\sigma^{\prime}_{1}\sigma^{\prime}_{2}\cdots\sigma^{\prime}_{m}$,
where $r_{0}=s_{n}$ and $r_{m}=s_{0}$, and since $s_{n}\in[p_{n}]$ and
$s_{0}\in[p_{0}]$, we get by ${\mathcal{C}}$’s definition that
$[r_{0}],[r_{1}],\ldots,[r_{m}]$ is a safe run on $w^{\prime}$ from
$[r_{0}]=[s_{n}]=[p_{n}]$ to $[r_{m}]=[s_{0}]=[p_{0}]$, and so ${\mathcal{C}}$
is normal. To conclude that ${\mathcal{C}}$ is nice, we prove below that it is
semantically deterministic. Consider the transitions
$\langle[q],\sigma,[s_{1}]\rangle$ and $\langle[q],\sigma,[s_{2}]\rangle$ in
${\mathcal{C}}$. We need to show that
$L({\mathcal{C}}^{[s_{1}]})=L({\mathcal{C}}^{[s_{2}]})$. By ${\mathcal{C}}$’s
definition, there are states $q^{\prime},q^{\prime\prime}\in[q]$,
$s^{\prime}_{1}\in[s_{1}]$ and $s^{\prime}_{2}\in[s_{2}]$ with the transitions
$\langle q^{\prime},\sigma,s^{\prime}_{1}\rangle$ and $\langle
q^{\prime\prime},\sigma,s^{\prime}_{2}\rangle$ in ${\mathcal{B}}$. Now as
${\mathcal{B}}$ is semantically deterministic and
$L({\mathcal{B}}^{q^{\prime}})=L({\mathcal{B}}^{q^{\prime\prime}})$, we have
by Proposition 2 that
$L({\mathcal{B}}^{s^{\prime}_{1}})=L({\mathcal{B}}^{s^{\prime}_{2}})$, and
thus Proposition 3.3 implies that
$L({\mathcal{C}}^{[s_{1}]})=L({\mathcal{B}}^{s^{\prime}_{1}})=L({\mathcal{B}}^{s^{\prime}_{2}})=L({\mathcal{C}}^{[s_{2}]})$,
and so ${\mathcal{C}}$ is semantically deterministic.

To prove that ${\mathcal{C}}$ is safe-minimal, note that $[q]\approx[s]$ iff
$[q]\precsim[s]$ and $[s]\precsim[q]$. Thus, it is sufficient to prove that if
$[q]\precsim[s]$ then $q\precsim s$. If
$L({\mathcal{C}}^{[q]})=L({\mathcal{C}}^{[s]})$ and $L_{{\it
safe}}({\mathcal{C}}^{[q]})\subseteq L_{{\it safe}}({\mathcal{C}}^{[s]})$,
then by Proposition 3.3, we have that
$L({\mathcal{B}}^{q})=L({\mathcal{C}}^{[q]})=L({\mathcal{C}}^{[s]})=L({\mathcal{B}}^{s})$,
and thus $L({\mathcal{B}}^{q})=L({\mathcal{B}}^{s})$. Similarly, by
Proposition 3.3, we have that $L_{{\it safe}}({\mathcal{B}}^{q})=L_{{\it
safe}}({\mathcal{C}}^{[q]})\subseteq L_{{\it
safe}}({\mathcal{C}}^{[s]})=L_{{\it safe}}({\mathcal{B}}^{s})$, and thus
$q\precsim s$.

As we noted in the definition of its transitions, ${\mathcal{C}}$ is
$\alpha$-homogenous. It is thus left to prove that ${\mathcal{C}}$ is safe-
centralized. If $[q]\precsim[s]$, then as seen previously, $q\precsim s$, and
since ${\mathcal{B}}$ is safe-centralized, we get that $q$ and $s$ are in the
same safe component of ${\mathcal{B}}$. Therefore, there is a safe run,
$r_{0},r_{1},\ldots,r_{n}$, from $q$ to $s$ in ${\mathcal{B}}$, and thus we
have by ${\mathcal{C}}$’s definition that $[r_{0}],[r_{1}],\ldots,[r_{n}]$ is
a safe run from $[q]$ to $[s]$ in ${\mathcal{C}}$, implying that $[q]$ and
$[s]$ are in the same safe component as ${\mathcal{C}}$ is normal, and so we
are done. ∎

We can thus conclude with the following.

######  Theorem .

Every nice, safe-centralized, and $\alpha$-homogenous GFG-tNCW can be turned
in polynomial time into an equivalent nice, safe-centralized, safe-minimal,
and $\alpha$-homogenous GFG-tNCW.

######  Example .

The safe languages of the states $q_{0}$ and $q_{1}$ of the GFG-tNCW
${\mathcal{B}}_{\mathcal{S}}$ from Figure 4 are different. Thus,
$q_{0}\not\approx q_{1}$, and applying safe-minimization to
${\mathcal{B}}_{\mathcal{S}}$ results in the GFG-tNCW ${\mathcal{C}}$
identical to ${\mathcal{B}}_{\mathcal{S}}$. ∎

##  4\. Canonicity in GFG-tNCWs

In this section we study canonicity for GFG-tNCWs. Recall that unlike the case
of finite words, for $\omega$-regular languages, no canonical minimal
deterministic automaton exists [25]. This classical result refers to automata
with state-based acceptance condition. There, for an automaton
${\mathcal{A}}=\langle\Sigma,Q,q_{0},\delta,\alpha\rangle$, we have that
$\alpha\subseteq Q$. In Büchi automata (NBWs or DBWs), a run $r$ is accepting
iff ${\it inf}(r)\cap\alpha\neq\emptyset$, where now ${\it inf}(r)$ is the set
of states that $r$ visits infinitely often. Thus, $r$ is accepting if it
visits states in $\alpha$ infinitely often. Dually, in co-Büchi automata (NCWs
or DCWs), a run $r$ is accepting iff ${\it inf}(r)\cap\alpha=\emptyset$. No
canonicity means that an $\omega$-regular language may have different minimal
DCWs or DBWs. Consider for example the DCWs ${\mathcal{A}}_{1}$ and
${\mathcal{A}}_{2}$ appearing in Figure 5. Both are minimal DCWs for the
language $L=(a+b)^{*}\cdot(a^{\omega}+b^{\omega})$ (“only finitely many $a$’s
or only finitely many $b$’s”; it is easier to see this by considering the dual
DBWs, for “infinitely many $a$’s and infinitely many $b$’s”).

Figure 5. The DCWs ${\mathcal{A}}_{1}$ and ${\mathcal{A}}_{2}$.

Since all the states of ${\mathcal{A}}_{1}$ and ${\mathcal{A}}_{2}$ recognize
the language $L$ and may serve as initial states, Figure 5 actually presents
six different DCWs for $L$, and more three-state DCWs for $L$ exist. The DCWs
${\mathcal{A}}_{1}$ and ${\mathcal{A}}_{2}$, are however “more different” than
variants of ${\mathcal{A}}_{1}$ obtained by changing the initial state: they
have a different structure, or more formally, there is no isomorphism between
their graphs.

We are going to show that unlike the case of DCWs and DBWs, GFG-tNCWs do have
a canonical form. Our positive results about canonicity of GFG-tNCWs are
related to the miniminization algorithm, and we first show that the sufficient
conditions for minimality of nice GFG-tNCWs specified in Theorem 3.1 are
necessary.

######  Theorem .

Nice minimal GFG-tNCWs are safe-centralized and safe-minimal.

###### Proof.

Consider a nice minimal GFG-tNCW ${\mathcal{A}}$. We argue that if
${\mathcal{A}}$ is not safe-centralized or not safe-minimal, then it can be
minimized further by the minimization algorithm described in Section 3. Assume
first that ${\mathcal{A}}$ is not safe-centralized. Then, there are two
different safe components $S,S^{\prime}\in{\mathcal{S}}({\mathcal{A}})$ and
states $q\in S$ and $q^{\prime}\in S^{\prime}$ such that $q\precsim
q^{\prime}$. Then, $H(S,S^{\prime})$, implying that the safe components in
${\mathcal{S}}({\mathcal{A}})$ are not a frontier. Then, safe-centralization,
as described in Section 3.2, minimizes ${\mathcal{A}}$ further. Indeed, in the
transition to the automaton ${\mathcal{B}}_{\mathcal{S}}$, at least one safe
component in ${\mathcal{S}}({\mathcal{A}})$ is removed from ${\mathcal{A}}$
when the frontier ${\mathcal{S}}$ is computed. Assume now that ${\mathcal{A}}$
is safe-centralized. Then, for every two different safe components
$S,S^{\prime}\in{\mathcal{S}}({\mathcal{A}})$, it holds that $\neg
H(S,S^{\prime})$ and $\neg H(S^{\prime},S)$. Hence, every strict subset of
${\mathcal{S}}({\mathcal{A}})$ is not a frontier. Thus,
${\mathcal{S}}({\mathcal{A}})$ is the only frontier of ${\mathcal{A}}$. Hence,
the automaton ${\mathcal{B}}_{\mathcal{S}}$, constructed in Section 3.2, has
${\mathcal{S}}={\mathcal{S}}({\mathcal{A}})$, and is obtained from
${\mathcal{A}}$ by adding $\alpha$-transitions that do not change the
languages and safe languages of its states. Accordingly,
${\mathcal{B}}_{\mathcal{S}}$ is safe-minimal iff ${\mathcal{A}}$ is safe-
minimal. Therefore, if ${\mathcal{A}}$ is not safe-minimal, then safe-
minimizing ${\mathcal{B}}_{\mathcal{S}}$, as in Section 3.3, merges at least
two different states. Hence, also in this case, ${\mathcal{A}}$ is minimized
further. ∎

We formalize relations between tNCWs by means of isomorphism and safe
isomorphism. Consider two tNCWs
${\mathcal{A}}=\langle\Sigma,Q_{\mathcal{A}},q^{0}_{\mathcal{A}},\delta_{\mathcal{A}},\alpha_{\mathcal{A}}\rangle$
and
${\mathcal{B}}=\langle\Sigma,Q_{\mathcal{B}},q^{0}_{\mathcal{B}},\delta_{\mathcal{B}},\alpha_{\mathcal{B}}\rangle$,
and a bijection $\kappa:Q_{\mathcal{A}}\to Q_{\mathcal{B}}$. We say that
$\kappa$ is:

  * $\triangleright$

$\alpha$-transition respecting, if $\kappa$ induces a bijection between the
$\alpha$-transitions of ${\mathcal{A}}$ and ${\mathcal{B}}$. Formally, for all
states $q,q^{\prime}\in Q_{\mathcal{A}}$ and letter $\sigma\in\Sigma$, we have
that $q^{\prime}\in\delta^{\alpha_{\mathcal{A}}}_{\mathcal{A}}(q,\sigma)$ iff
$\kappa(q^{\prime})\in\delta^{\alpha_{\mathcal{B}}}_{\mathcal{B}}(\kappa(q),\sigma)$.

  * $\triangleright$

$\bar{\alpha}$-transition respecting, if $\kappa$ induces a bijection between
the $\bar{\alpha}$-transitions of ${\mathcal{A}}$ and ${\mathcal{B}}$.
Formally, for all states $q,q^{\prime}\in Q_{\mathcal{A}}$ and letter
$\sigma\in\Sigma$, we have that
$q^{\prime}\in\delta^{\bar{\alpha}_{\mathcal{A}}}_{\mathcal{A}}(q,\sigma)$ iff
$\kappa(q^{\prime})\in\delta^{\bar{\alpha}_{\mathcal{B}}}_{\mathcal{B}}(\kappa(q),\sigma)$.

Then, ${\mathcal{A}}$ and ${\mathcal{B}}$ are _safe isomorphic_ if there is a
bijection $\kappa:Q_{\mathcal{A}}\to Q_{\mathcal{B}}$ that is
$\bar{\alpha}$-transition respecting. If, in addition, $\kappa$ is
$\alpha$-transition respecting, then ${\mathcal{A}}$ and ${\mathcal{B}}$ are
_isomorphic_. Note that if $\kappa$ is $\bar{\alpha}$-transition respecting,
then for every state $q\in Q_{\mathcal{A}}$, it holds that $q$ and $\kappa(q)$
have equivalent safe languages. Also, if $\kappa$ is both $\alpha$-transition
respecting and $\bar{\alpha}$-transition respecting, then for every state
$q\in Q_{\mathcal{A}}$, we have that $q\approx\kappa(q)$.

###  4.1. Safe isomorphism

Theorem 4 suggests that safe-minimization and safe-centralization characterize
nice minimal GFG-tNCWs. Hence, if we take two nice minimal equivalent GFG-
tNCWs ${\mathcal{A}}$ and ${\mathcal{B}}$, and apply Lemma 3.1 to both of
them, one can conclude that the injection
$\eta:{\mathcal{S}}({\mathcal{A}})\to{\mathcal{S}}({\mathcal{B}})$ is actually
a bijection. The following theorem uses the latter fact in order to show that
$\eta$ induces a bijection $\kappa:Q_{\mathcal{A}}\to Q_{\mathcal{B}}$ that is
$\bar{\alpha}$-transition respecting.

######  Theorem .

Every two equivalent, nice, and minimal GFG-tNCWs are safe isomorphic.

###### Proof.

Consider two equivalent, nice, and minimal GFG-tNCWs ${\mathcal{A}}$ and
${\mathcal{B}}$. By Theorem 4, ${\mathcal{A}}$ is safe-minimal and safe-
centralized. Hence, by Lemma 3.1, there is an injection
$\eta:{\mathcal{S}}({\mathcal{A}})\to{\mathcal{S}}({\mathcal{B}})$ such that
for every safe component $T\in{\mathcal{S}}({\mathcal{A}})$, it holds that
$|T|\leq|\eta(T)|$. For a safe component $T\in{\mathcal{S}}({\mathcal{A}})$,
let $p_{T}$ be some state in $T$. By Proposition 3.1, there are states
$q_{T}\in Q_{{\mathcal{A}}}$ and $s_{T}\in Q_{{\mathcal{B}}}$ such that
$p_{T}\precsim q_{T}$ and $q_{T}\approx s_{T}$. Since ${\mathcal{A}}$ is safe-
centralized, the state $q_{T}$ is in $T$, and in the proof of Lemma 3.1, we
defined $\eta(T)$ to be the safe component of $s_{T}$ in ${\mathcal{B}}$.
Likewise, ${\mathcal{B}}$ is safe-minimal and safe-centralized, and there is
an injection
$\eta^{\prime}:{\mathcal{S}}({\mathcal{B}})\to{\mathcal{S}}({\mathcal{A}})$.
The existence of the two injections implies that
$|{\mathcal{S}}({\mathcal{A}})|=|{\mathcal{S}}({\mathcal{B}})|$. Thus, the
injection $\eta$ is actually a bijection. Hence,

$|{\mathcal{A}}|=\sum\limits_{T\in{\mathcal{S}}({\mathcal{A}})}|T|\leq\sum\limits_{T\in{\mathcal{S}}({\mathcal{A}})}|\eta(T)|=\sum\limits_{T^{\prime}\in{\mathcal{S}}({\mathcal{B}})}|T^{\prime}|=|{\mathcal{B}}|$

Indeed, the first inequality follows from the fact $|T|\leq|\eta(T)|$, and the
second equality follows from the fact that $\eta$ is a bijection. Now, as
${\mathcal{A}}$ and ${\mathcal{B}}$ are both minimal, we have that
$|{\mathcal{A}}|=|{\mathcal{B}}|$, and so it follows that for every safe
component $T\in{\mathcal{S}}({\mathcal{A}})$, we have that $|T|=|\eta(T)|$. We
use the latter fact in order to show that $\eta$ induces a bijection
$\kappa:Q_{\mathcal{A}}\to Q_{\mathcal{B}}$ that is $\bar{\alpha}$-transition
respecting.

Consider a safe component $T\in{\mathcal{S}}({\mathcal{A}})$. By Lemma 3.1, we
have that $|T|\leq|\eta(T)|$. The proof of the lemma associates with a safe
run $r_{T}=q_{0},q_{1},\ldots,q_{m}$ of ${\mathcal{A}}$ that traverses all the
states in the safe component $T$, a safe run
$r_{\eta(T)}=s_{0},s_{1},\ldots,s_{m}$ of ${\mathcal{B}}$ that traverses
states in $\eta(T)$ and $q_{i}\approx s_{i}$, for every $0\leq i\leq m$.
Moreover, if $0\leq i_{1},i_{2}\leq m$ are such that $q_{i_{1}}\not\approx
q_{i_{2}}$, then $s_{i_{1}}\not\approx s_{i_{2}}$. Let
$\kappa_{T}:T\to\eta(T)$ be a function that maps each state $q_{i}$ in $r_{T}$
to the state $s_{i}$ in $r_{\eta(T)}$. If there are $0\leq i_{1},i_{2}\leq m$
with $q_{i_{1}}=q_{i_{2}}$, then $q_{i_{1}}\approx q_{i_{2}}$, and thus by
transitivity of $\approx$, it holds that $s_{i_{1}}\approx s_{i_{2}}$. Then,
safe-minimality of ${\mathcal{B}}$ implies that $s_{i_{1}}=s_{i_{2}}$, and
thus $\kappa_{T}$ is a well defined function from $T$ to $\eta(T)$. Since
${\mathcal{A}}$ is safe-minimal, every two states in $T$ are not strongly
equivalent. Therefore, the function $\kappa_{T}$ is an injection from $T$ to
$\eta(T)$. Thus, as $|T|=|\eta(T)|$, the injection $\kappa_{T}$ is actually a
bijection. The desired bijection $\kappa$ is then the union of the bijections
$\kappa_{T}$ for $T\in{\mathcal{S}}({\mathcal{A}})$.

Clearly, as $\eta:{\mathcal{S}}({\mathcal{A}})\to{\mathcal{S}}({\mathcal{B}})$
is a bijection, the function $\kappa$ is a bijection from $Q_{\mathcal{A}}$ to
$Q_{\mathcal{B}}$. We prove that $\kappa$ is $\bar{\alpha}$-transition
respecting. Consider states $q,q^{\prime}\in Q_{\mathcal{A}}$ and a letter
$\sigma\in\Sigma$ such that $\langle q,\sigma,q^{\prime}\rangle$ is an
$\bar{\alpha}$-transition of ${\mathcal{A}}$. Let $T$ be $q$’s safe component.
By the definition of $\kappa_{T}$, we have that $q\approx\kappa_{T}(q)$. By
Proposition 3.1, there is an $\bar{\alpha}$-transition of ${\mathcal{B}}$ of
the form $t=\langle\kappa(q),\sigma,s^{\prime}\rangle$, where
$q^{\prime}\approx s^{\prime}$. As $t$ is an $\bar{\alpha}$-transition of
${\mathcal{B}}$, we know that $s^{\prime}$ is in $\eta(T)$. Recall that
${\mathcal{B}}$ is safe-minimal; in particular, there are no strongly-
equivalent states in $\eta(T)$. Hence, $s^{\prime}=\kappa(q^{\prime})$, and so
$\langle\kappa(q),\sigma,\kappa(q^{\prime})\rangle$ is an
$\bar{\alpha}$-transition of ${\mathcal{B}}$. Likewise, if
$\langle\kappa(q),\sigma,\kappa(q^{\prime})\rangle$ is an
$\bar{\alpha}$-transition of ${\mathcal{B}}$, then $\langle
q,\sigma,q^{\prime}\rangle$ is an $\bar{\alpha}$-transition of
${\mathcal{A}}$, and so we are done. ∎

###  4.2. Isomorphism

Theorem 4.1 implies that all nice minimal GFG-tNCWs for a given language are
safe isomorphic. We continue and show that it is possible to make these GFG-
tNCWs isomorphic. We propose two canonical forms that guarantee isomorphism.
Both forms are based on saturating the GFG-tNCW with $\alpha$-transitions. One
adds as many $\alpha$-transitions as possible, and the second does so in a way
that preserves $\alpha$-homogeneity.

Consider a nice GFG-tNCW
${\mathcal{A}}=\langle\Sigma,Q,q_{0},\delta,\alpha\rangle$. We say that a
triple $\langle q,\sigma,s\rangle\in Q\times\Sigma\times Q$ is an allowed
transition in ${\mathcal{A}}$ if there is a state $s^{\prime}\in Q$ such that
$s\sim s^{\prime}$ and $\langle q,\sigma,s^{\prime}\rangle\in\Delta$. Note
that since for all states $s\in Q$, we have that $s\approx s$, then all the
transitions in $\Delta$ are allowed. We now define two types of
$\alpha$-maximality.

  * $\triangleright$

We say that ${\mathcal{A}}$ is $\alpha$-maximal if all allowed transitions in
$Q\times\Sigma\times Q$ are in $\Delta$.

  * $\triangleright$

We say that ${\mathcal{A}}$ is $\alpha$-maximal up to homogeneity if
${\mathcal{A}}$ is $\alpha$-homogenous, and for every state $q\in Q$ and
letter $\sigma\in\Sigma$, if $q$ has no outgoing $\sigma$-labeled
$\bar{\alpha}$-transitions, then all allowed transitions in
$\\{q\\}\times\\{\sigma\\}\times Q$ are in $\Delta$.

Thus, $\alpha$-maximal automata include all allowed transitions, and
$\alpha$-maximal up to homogeneity automata include all allowed transitions as
long as their inclusion does not conflict with $\alpha$-homogeneity.

######  Example .

Recall the minimal GFG-tNCW ${\mathcal{B}}_{{\mathcal{S}}}$ appearing in
Figure 4. The GFG-tNCWs ${\mathcal{C}}_{1}$ and ${\mathcal{C}}_{2}$ in Figure
6 are obtained from ${\mathcal{B}}_{\mathcal{S}}$ by removing a $c$-labeled
$\alpha$-transition from $q_{0}$. This does not change the language and
results in two nice minimal equivalent GFG-tNCWs that are safe isomorphic yet
are not $\alpha$-maximal nor $\alpha$-maximal up to homogeneity. ∎

Figure 6. Two safe isomorphic yet not isomorphic nice minimal equivalent GFG-
tNCWs.

We now prove that both types of $\alpha$-maximality guarantee isomorphism.

######  Theorem .

Every two equivalent, nice, minimal, and $\alpha$-maximal GFG-tNCWs are
isomorphic.

###### Proof.

Consider two equivalent, nice, minimal, and $\alpha$-maximal GFG-tNCWs
${\mathcal{C}}_{1}$ and ${\mathcal{C}}_{2}$. By Theorem 4.1, we have that
${\mathcal{C}}_{1}$ and ${\mathcal{C}}_{2}$ are safe isomorphic. Thus, there
is a bijection $\kappa:Q_{{\mathcal{C}}_{1}}\to Q_{{\mathcal{C}}_{2}}$ that is
$\bar{\alpha}$-transition respecting. The bijection $\kappa$ was defined such
that $q\approx\kappa(q)$, for every state $q\in Q_{{\mathcal{C}}_{1}}$. We
show that $\kappa$ is also $\alpha$-transition respecting. Let $\langle
q,\sigma,s\rangle$ be an $\alpha$-transition of ${\mathcal{C}}_{1}$. Then, as
$\kappa$ is $\bar{\alpha}$-transition respecting, and $\langle
q,\sigma,s\rangle$ is not an $\bar{\alpha}$-transition in ${\mathcal{C}}_{1}$,
the triple $\langle\kappa(q),\sigma,\kappa(s)\rangle$ cannot be an
$\bar{\alpha}$-transition in ${\mathcal{C}}_{2}$. We show that
$\langle\kappa(q),\sigma,\kappa(s)\rangle$ is a transition in
${\mathcal{C}}_{2}$, and thus it has to be an $\alpha$-transition. As
${\mathcal{C}}_{2}$ is total, there is a transition
$\langle\kappa(q),\sigma,s^{\prime}\rangle$ in ${\mathcal{C}}_{2}$. As
$q\sim\kappa(q)$ and both automata are nice, in particular, semantically
deterministic, Proposition 2 then implies that $s\sim s^{\prime}$. Now since
$s\sim\kappa(s)$, we get by the transitivity of $\sim$ that
$s^{\prime}\sim\kappa(s)$. Therefore, the existence of the transition
$\langle\kappa(q),\sigma,s^{\prime}\rangle$ in ${\mathcal{C}}_{2}$, implies
that the transition $\langle\kappa(q),\sigma,\kappa(s)\rangle$ is an allowed
transition, and so $\alpha$-maximality of ${\mathcal{C}}_{2}$ implies that it
is also a transition in ${\mathcal{C}}_{2}$. Likewise, if
$\langle\kappa(q),\sigma,\kappa(s)\rangle$ is an $\alpha$-transition in
$C_{2}$, then $\langle q,\sigma,s\rangle$ is an $\alpha$-transition in
$C_{1}$, and so we are done. ∎

######  Theorem .

Every two equivalent, nice, minimal, and $\alpha$-maximal up to homogeneity
GFG-tNCWs are isomorphic.

###### Proof.

The proof is identical to that of Theorem 4.2, except that we also have to
prove that $\kappa(q)$ has no outgoing $\sigma$-labeled
$\bar{\alpha}$-transitions in ${\mathcal{C}}_{2}$. To see this, assume by way
of contradiction that there is an $\bar{\alpha}$-transition
$\langle\kappa(q),\sigma,s^{\prime}\rangle$ in ${\mathcal{C}}_{2}$. Then, as
$q\approx\kappa(q)$, Proposition 3.1 implies that $q$ has an outgoing
$\sigma$-labeled $\bar{\alpha}$-transition in ${\mathcal{C}}_{1}$,
contradicting the fact that ${\mathcal{C}}_{1}$ is $\alpha$-homogenous. ∎

###  4.3. Obtaining Canonical Minimal GFG-tNCWs

In this section we show how the two types of canonical minimal GFG-tNCWs can
be obtained in polynomial time. We start with $\alpha$-maximality up to
homogeneity and show that the minimization construction described in Section 3
results in GFG-tNCWs that are $\alpha$-maximial up to homogeneity. We continue
with $\alpha$-maximality, and show that adding allowed transitions to a GFG-
tNCW does not change its language, and conclude that $\alpha$-maximization can
be performed on top of the minimization construction described in Section 3.

####  4.3.1. Obtaining canonical minimal $\alpha$-maximal up to homogeneity
GFG-tNCWs

######  Theorem .

Consider a nice GFG-tNCW ${\mathcal{A}}$, and let ${\mathcal{C}}$ be the
minimal GFG-tNCW generated from ${\mathcal{A}}$ by the minimization
construction described in Section 3. Then, ${\mathcal{C}}$ is $\alpha$-maximal
up to homogeneity.

###### Proof.

Consider the minimization construction described in Section 3. We first show
that the safe-centralized GFG-tNCW ${\mathcal{B}}_{{\mathcal{S}}}$, defined in
Section 3.2, is $\alpha$-maximal up to homogeneity. Then, we show that
$\alpha$-maximality up to homogeneity is maintained in the transition to the
GFG-tNCW ${\mathcal{C}}$, defined in Section 3.3.

By Proposition 3.2, we know that ${\mathcal{B}}_{\mathcal{S}}$ is
$\alpha$-homogenous. Assume that $q$ is a state in
${\mathcal{B}}_{\mathcal{S}}$ with no outgoing $\sigma$-labeled
$\bar{\alpha}$-transitions, and assume that $\langle q,\sigma,s\rangle$ is an
allowed transition. We need to show that $\langle q,\sigma,s\rangle$ is a
transition in ${\mathcal{B}}_{\mathcal{S}}$. As $\langle q,\sigma,s\rangle$ is
an allowed transition, there is a transition $\langle
q,\sigma,s^{\prime}\rangle$ in ${\mathcal{B}}_{\mathcal{S}}$ with
$s\sim_{{\mathcal{B}}_{\mathcal{S}}}s^{\prime}$, and by the assumption,
$\langle q,\sigma,s^{\prime}\rangle$ has to be an $\alpha$-transition. By the
definition of the transition function of ${\mathcal{B}}_{\mathcal{S}}$, we
have that $s^{\prime}\sim_{\mathcal{A}}q^{\prime}$ for some state
$q^{\prime}\in\delta^{\alpha}_{\mathcal{A}}(q,\sigma)$. Now, as
$s\sim_{{\mathcal{B}}_{\mathcal{S}}}s^{\prime}$, Proposition 3.2 implies that
$L({\mathcal{A}}^{s})=L({\mathcal{B}}^{s}_{\mathcal{S}})=L({\mathcal{B}}^{s^{\prime}}_{\mathcal{S}})=L({\mathcal{A}}^{s^{\prime}})$;
that is, $s\sim_{\mathcal{A}}s^{\prime}$, and since
$s^{\prime}\sim_{\mathcal{A}}q^{\prime}$, we get by the transitivity of
$\sim_{\mathcal{A}}$ that $s\sim_{\mathcal{A}}q^{\prime}$, and so $\langle
q,\sigma,s\rangle$ is a transition in ${\mathcal{B}}_{\mathcal{S}}$.

Next, we show that the GFG-tNCW ${\mathcal{C}}$ is $\alpha$-maximal up to
homogeneity. By Proposition 3.3, we have that ${\mathcal{C}}$ is
$\alpha$-homogenous. Assume that $[q]$ is a state in ${\mathcal{C}}$ with no
outgoing $\sigma$-labeled $\bar{\alpha}$-transitions, and assume that
$\langle[q],\sigma,[s]\rangle$ is an allowed transition. We need to show that
$\langle[q],\sigma,[s]\rangle$ is a transition in ${\mathcal{C}}$. As
$\langle[q],\sigma,[s]\rangle$ is an allowed transition, there is a transition
$\langle[q],\sigma,[s^{\prime}]\rangle$ in ${\mathcal{C}}$ with
$[s]\sim[s^{\prime}]$. Thus, by Proposition 3.3, we have that
$L({\mathcal{B}}^{s}_{\mathcal{S}})=L({\mathcal{C}}^{[s]})=L({\mathcal{C}}^{[s^{\prime}]})=L({\mathcal{B}}^{s^{\prime}}_{\mathcal{S}})$;
that is, $s^{\prime}\sim_{{\mathcal{B}}_{\mathcal{S}}}s$. By the assumption,
$\langle[q],\sigma,[s^{\prime}]\rangle$ has to be an $\alpha$-transition.
Therefore, by the definition of ${\mathcal{C}}$, there are states
$q^{\prime\prime}\in[q]$ and $s^{\prime\prime}\in[s^{\prime}]$, such that
$\langle q^{\prime\prime},\sigma,s^{\prime\prime}\rangle$ is an
$\alpha$-transition in ${\mathcal{B}}_{\mathcal{S}}$. Now, by transitivity of
$\sim_{{\mathcal{B}}_{\mathcal{S}}}$ and the fact that
$s^{\prime\prime}\sim_{{\mathcal{B}}_{\mathcal{S}}}s^{\prime}$, we get that
$s^{\prime\prime}\sim_{{\mathcal{B}}_{\mathcal{S}}}s$. Finally, as
${\mathcal{B}}_{\mathcal{S}}$ is $\alpha$-homogenous, we get that
$q^{\prime\prime}$ has no outgoing $\sigma$-labeled $\bar{\alpha}$-transitions
in ${\mathcal{B}}_{\mathcal{S}}$, and so by the $\alpha$-maximality up to
homogeneity of ${\mathcal{B}}_{\mathcal{S}}$, we have that $\langle
q^{\prime\prime},\sigma,s\rangle$ is a transition in
${\mathcal{B}}_{\mathcal{S}}$. Therefore, by the definition of
${\mathcal{C}}$, we have that $\langle[q],\sigma,[s]\rangle$ is a transition
in ${\mathcal{C}}$, and we are done. ∎

We can thus conclude with the following.

######  Theorem .

Every GFG-tNCW ${\mathcal{A}}$ can be canonized into a nice, minimal, and
$\alpha$-maximal up to homogeneity GFG-tNCW in polynomial time.

####  4.3.2. Obtaining canonical minimal $\alpha$-maximal GFG-tNCWs

Consider a nice GFG-tNCW
${\mathcal{A}}=\langle\Sigma,Q,q_{0},\delta,\alpha\rangle$. Recall that the
transition function $\delta$ can be viewed as a transition relation
$\Delta\subseteq Q\times\Sigma\times Q$, where for every two states $q,s\in Q$
and letter $\sigma\in\Sigma$, we have that $\langle
q,\sigma,s\rangle\in\Delta$ iff $s\in\delta(q,\sigma)$. We say that a set of
triples ${\mathcal{E}}\subseteq\left(Q\times\Sigma\times
Q\right)\setminus\Delta$ is an _allowed set_ if all the triples in it are
allowed transitions in ${\mathcal{A}}$. For every allowed set
${\mathcal{E}}\subseteq\left(Q\times\Sigma\times Q\right)\setminus\Delta$, we
define the tNCW
${\mathcal{A}}_{\mathcal{E}}=\langle\Sigma,Q_{,}q_{0},\delta_{\mathcal{E}},\alpha_{\mathcal{E}}\rangle$,
where $\Delta_{\mathcal{E}}=\Delta\cup{\mathcal{E}}$ and
$\alpha_{\mathcal{E}}=\alpha\cup{\mathcal{E}}$. Clearly, as ${\mathcal{A}}$
and ${\mathcal{A}}_{\mathcal{E}}$ have the same set of states and the same set
of $\bar{\alpha}$-transitions, they have equivalent safe languages.

In Propositions 4.3.2 and 4.3.2 below, we prove that for every allowed set
${\mathcal{E}}$, we have that ${\mathcal{A}}_{{\mathcal{E}}}$ is a nice GFG-
tNCW equivalent to ${\mathcal{A}}$. We first extend Proposition 2 to the
setting of ${\mathcal{A}}$ and ${\mathcal{A}}_{\mathcal{E}}$:

######  Proposition .

Consider states $q$ and $s$ of ${\mathcal{A}}$ and
${\mathcal{A}}_{\mathcal{E}}$, respectively, a letter $\sigma\in\Sigma$, and
transitions $\langle q,\sigma,q^{\prime}\rangle$ and $\langle
s,\sigma,s^{\prime}\rangle$ of ${\mathcal{A}}$ and
${\mathcal{A}}_{\mathcal{E}}$, respectively. If $q\sim_{{\mathcal{A}}}s$, then
$q^{\prime}\sim_{{\mathcal{A}}}s^{\prime}$.

###### Proof.

If $\langle s,\sigma,s^{\prime}\rangle\notin{\mathcal{E}}$, then, by the
definition of $\Delta_{{\mathcal{E}}}$, it is also a transition of
${\mathcal{A}}$. Hence, since $q\sim_{{\mathcal{A}}}s$ and ${\mathcal{A}}$ is
nice, in particular, semantically deterministic, Proposition 2 implies that
$q^{\prime}\sim_{{\mathcal{A}}}s^{\prime}$. If $\langle
s,\sigma,s^{\prime}\rangle\in{\mathcal{E}}$, then it is an allowed transition
of ${\mathcal{A}}$. Therefore, there is a state $p^{\prime}\in Q$ such that
$s^{\prime}\sim_{\mathcal{A}}p^{\prime}$ and $\langle
s,\sigma,p^{\prime}\rangle\in\Delta$. As $q\sim_{\mathcal{A}}s$ and
${\mathcal{A}}$ is semantically deterministic, Proposition 2 implies that
$q^{\prime}\sim_{{\mathcal{A}}}p^{\prime}$. Therefore, using the fact that
$p^{\prime}\sim_{\mathcal{A}}s^{\prime}$, the transitivity of
$\sim_{\mathcal{A}}$ implies that $q^{\prime}\sim_{\mathcal{A}}s^{\prime}$,
and so we are done. ∎

Now, we can iteratively apply Proposition 4.3.2 and show that equivalent
states in ${\mathcal{A}}$ stay equivalent in ${\mathcal{A}}_{\mathcal{E}}$,
which is GFG.

######  Proposition .

Let $p$ and $s$ be states of ${\mathcal{A}}$ and
${\mathcal{A}}_{\mathcal{E}}$, respectively, with $p\sim_{{\mathcal{A}}}s$.
Then, ${\mathcal{A}}^{s}_{\mathcal{E}}$ is a GFG-tNCW equivalent to
${\mathcal{A}}^{p}$.

###### Proof.

We first prove that $L({\mathcal{A}}^{s}_{\mathcal{E}})\subseteq
L({\mathcal{A}}^{p})$. Consider a word $w=\sigma_{1}\sigma_{2}\cdots\in
L({\mathcal{A}}^{s}_{\mathcal{E}})$, and let $s_{0},s_{1},s_{2},\ldots$ be an
accepting run of ${\mathcal{A}}^{s}_{\mathcal{E}}$ on $w$. Then, there is
$i\geq 0$ such that $s_{i},s_{i+1},\ldots$ is a safe run of
${\mathcal{A}}^{s_{i}}_{\mathcal{E}}$ on the suffix $w[i+1,\infty]$. Let
$p_{0},p_{1},\ldots,p_{i}$ be a run of ${\mathcal{A}}^{p}$ on the prefix
$w[1,i]$. Since $p_{0}\sim_{{\mathcal{A}}}s_{0}$, we get, by an iterative
application of Proposition 4.3.2, that $p_{i}\sim_{{\mathcal{A}}}s_{i}$. In
addition, as the run of ${\mathcal{A}}^{s_{i}}_{\mathcal{E}}$ on the suffix
$w[i+1,\infty]$ is safe, it is also a safe run of ${\mathcal{A}}^{s_{i}}$.
Hence, $w[i+1,\infty]\in L({\mathcal{A}}^{p_{i}})$, and thus
$p_{0},p_{1},\ldots,p_{i}$ can be extended to an accepting run of
${\mathcal{A}}^{p}$ on $w$.

Next, as ${\mathcal{A}}$ is nice, all of its states are GFG, in particular,
there is a strategy $f^{s}$ witnessing ${\mathcal{A}}^{s}$’s GFGness. Recall
that ${\mathcal{A}}$ is embodied in ${\mathcal{A}}_{\mathcal{E}}$. Therefore,
every run in ${\mathcal{A}}$ exists also in ${\mathcal{A}}_{\mathcal{E}}$.
Thus, as $p\sim_{\mathcal{A}}s$, we get that for every word $w\in
L({\mathcal{A}}^{p})$, the run $f^{s}(w)$ is an accepting run of
${\mathcal{A}}^{s}$ on $w$, and thus is also an accepting run of
${\mathcal{A}}^{s}_{\mathcal{E}}$ on $w$. Hence,
$L({\mathcal{A}}^{p})\subseteq L({\mathcal{A}}^{s}_{\mathcal{E}})$ and $f^{s}$
witnesses ${\mathcal{A}}^{s}_{\mathcal{E}}$’s GFGness. ∎

######  Proposition .

For every allowed set ${\mathcal{E}}$, the GFG-tNCW
${\mathcal{A}}_{\mathcal{E}}$ is nice.

###### Proof.

It is easy to see that the fact ${\mathcal{A}}$ is nice implies that
${\mathcal{A}}_{\mathcal{E}}$ is normal and safe deterministic. Also, as
${\mathcal{A}}$ is embodied in ${\mathcal{A}}_{\mathcal{E}}$ and both automata
have the same state-space and initial states, then all the states in
${\mathcal{A}}_{\mathcal{E}}$ are reachable. Finally, Proposition 4.3.2
implies that all the states in ${\mathcal{A}}_{\mathcal{E}}$ are GFG. To
conclude that ${\mathcal{A}}_{\mathcal{E}}$ is nice, we prove below that it is
semantically deterministic. Consider transitions $\langle
q,\sigma,s_{1}\rangle$ and $\langle q,\sigma,s_{2}\rangle$ in
$\Delta_{{\mathcal{E}}}$. We need to show that
$s_{1}\sim_{{\mathcal{A}}_{\mathcal{E}}}s_{2}$. By the definition of
$\Delta_{\mathcal{E}}$, there are transitions $\langle
q,\sigma,s^{\prime}_{1}\rangle$ and $\langle q,\sigma,s^{\prime}_{2}\rangle$
in $\Delta$ for states $s^{\prime}_{1}$ and $s^{\prime}_{2}$ such that
$s_{1}\sim_{\mathcal{A}}s^{\prime}_{1}$ and
$s_{2}\sim_{\mathcal{A}}s^{\prime}_{2}$. As ${\mathcal{A}}$ is nice, in
particular, semantically deterministic, we have that
$s^{\prime}_{1}\sim_{\mathcal{A}}s^{\prime}_{2}$. Hence, as
$s_{1}\sim_{\mathcal{A}}s^{\prime}_{1}$ and
$s^{\prime}_{2}\sim_{\mathcal{A}}s_{2}$, we get by the transitivity of
$\sim_{\mathcal{A}}$ that $s_{1}\sim_{\mathcal{A}}s_{2}$. Then, Proposition
4.3.2 implies that
$L({\mathcal{A}}^{s_{1}})=L({\mathcal{A}}^{s_{1}}_{{\mathcal{E}}})$ and
$L({\mathcal{A}}^{s_{2}})=L({\mathcal{A}}^{s_{2}}_{{\mathcal{E}}})$, and so we
get that $s_{1}\sim_{{\mathcal{A}}_{{\mathcal{E}}}}s_{2}$. Thus,
${\mathcal{A}}_{{\mathcal{E}}}$ is semantically deterministic. ∎

Let ${\mathcal{C}}$ be a nice minimal GFG-tNCW equivalent to ${\mathcal{A}}$,
and let $\hat{{\mathcal{E}}}$ be the set of all allowed transitions in
${\mathcal{C}}$ that are not transitions of ${\mathcal{C}}$. By Propositions
4.3.2 and 4.3.2, we have that ${\mathcal{C}}_{\hat{{\mathcal{E}}}}$ is a nice
minimal GFG-tNCW equivalent to ${\mathcal{A}}$. Below we argue that it is also
$\alpha$-maximal.

######  Proposition .

Let ${\mathcal{C}}$ be a nice GFG-tNCW, and let $\hat{{\mathcal{E}}}$ be the
set of all allowed transitions in ${\mathcal{C}}$ that are not transitions of
${\mathcal{C}}$. Then, ${\mathcal{C}}_{\hat{{\mathcal{E}}}}$ is
$\alpha$-maximal.

###### Proof.

Let ${\mathcal{C}}=\langle\Sigma,Q,q_{0},\delta,\alpha\rangle$, and consider
an allowed transition $\langle q,\sigma,s\rangle\in Q\times\Sigma\times Q$ in
${\mathcal{C}}_{\hat{{\mathcal{E}}}}$. We prove that $\langle
q,\sigma,s\rangle$ is an allowed transition also in ${\mathcal{C}}$. Hence, it
is in $\Delta_{\hat{{\mathcal{E}}}}$, and thus is a transition in
${\mathcal{C}}_{\hat{{\mathcal{E}}}}$.

By the definition of allowed transitions, there is a state $s^{\prime}\in Q$
with $s\sim_{{\mathcal{C}}_{\hat{{\mathcal{E}}}}}s^{\prime}$ such that
$s^{\prime}\in\delta_{\hat{{\mathcal{E}}}}(q,\sigma)$. Proposition 4.3.2
implies that
$L({\mathcal{C}}^{s})=L({\mathcal{C}}^{s}_{\hat{{\mathcal{E}}}})=L({\mathcal{C}}^{s^{\prime}}_{\hat{{\mathcal{E}}}})=L({\mathcal{C}}^{s^{\prime}})$,
and thus $s\sim_{\mathcal{C}}s^{\prime}$. Also, by the definition of
$\delta_{\hat{{\mathcal{E}}}}$, there is a state $s^{\prime\prime}\in Q$ such
that $s^{\prime\prime}\sim_{\mathcal{C}}s^{\prime}$ and
$s^{\prime\prime}\in\delta(q,\sigma)$. Therefore, as the transitivity of
$\sim_{\mathcal{C}}$ implies that $s\sim_{\mathcal{C}}s^{\prime\prime}$, we
have that $\langle q,\sigma,s\rangle$ is also an allowed transition in
${\mathcal{C}}$, and we are done. ∎

Since the relation $\sim$ can be calculated in polynomial time [19, 24], and
so checking if a triple in $Q\times\Sigma\times Q$ is an allowed transition
can be done in polynomial time, then applying $\alpha$-maximization on top of
the minimization construction described in Section 3, is still polynomial. We
can thus conclude with the following.

######  Theorem .

Every GFG-tNCW ${\mathcal{A}}$ can be canonized into a nice minimal
$\alpha$-maximal GFG-tNCW in polynomial time.

######  Example .

Consider the minimal GFG-tNCW ${\mathcal{B}}_{\mathcal{S}}$ appearing in
Figure 4. By applying $\alpha$-maximization to ${\mathcal{B}}_{\mathcal{S}}$,
we obtain the $\alpha$-maximal GFG-tNCW ${\mathcal{C}}_{\hat{{\mathcal{E}}}}$
appearing in Figure 7. ∎

Figure 7. The $\alpha$-maximal GFG-tNCW for the GFG-tNCW
${\mathcal{B}}_{\mathcal{S}}$ in Figure 4.

###  4.4. Canonicity in GFG-NCWs and tDCWs

The positive canonicity results in Section 4.3 refer to GFG-tNCWs. In this
section we study each of the features, namely GFGness and transition-based
acceptance, in isolation. We start with GFG-NCWs. For automata with state-
based acceptance, an analogue definition of isomorphism between automata
${\mathcal{A}}$ and ${\mathcal{B}}$ with acceptance conditions
$\alpha_{\mathcal{A}}\subseteq Q_{\mathcal{A}}$ and
$\alpha_{\mathcal{B}}\subseteq Q_{\mathcal{B}}$, seeks a bijection
$\kappa:Q_{\mathcal{A}}\to Q_{\mathcal{B}}$ such that for every $q\in
Q_{\mathcal{A}}$, we have that $q\in\alpha_{\mathcal{A}}$ iff
$\kappa(q)\in\alpha_{\mathcal{B}}$, and for every letter $\sigma\in\Sigma$,
and state $q^{\prime}\in Q_{\mathcal{A}}$, we have that
$q^{\prime}\in\delta_{\mathcal{A}}(q,\sigma)$ iff
$\kappa(q^{\prime})\in\delta_{\mathcal{B}}(\kappa(q),\sigma)$. It is easy to
see that the DCWs ${\mathcal{A}}_{1}$ and ${\mathcal{A}}_{2}$ from Figure 5
are not isomorphic, which is a well known property of DCWs [25]. In Theorem
4.4 below, we extend the “no canonicity” result to GFG-NCWs. As in the study
of GFG-tNCWs, we focus on nice GFG-NCWs. Note that the definitions of the
underlying properties of nice GFG-tNCWs naturally extend to GFG-NCWs. For
example, a GFG-NCW ${\mathcal{A}}$ is _safe deterministic_ if by removing
$\alpha$-states and all transitions that touch them, we remove all
nondeterministic choices. An exception is the definition of normal. For a GFG-
NCW ${\mathcal{A}}$, we say that ${\mathcal{A}}$ is normal if for all states
$q\in Q$, if $q$ is not part of a cycle in ${\mathcal{A}}$, then $q\in\alpha$.
Also, rather than $\alpha$-maximization, here we refer to $\alpha$-mutation,
which amounts to changing the membership of states in $\alpha$ while keeping
the NCW nice and without changing its language.

As we show in Theorem 4.4, the fact the GFG automata we consider have
transition-based acceptance conditions is crucial for canonization.

######  Theorem .

Nice, equivalent, and minimal GFG-NCWs need not be isomorphic, and need not be
made isomorphic by $\alpha$-mutation.

###### Proof.

Consider the language $L=(a+b)^{*}\cdot(a^{\omega}+b^{\omega})$. In Figure 5,
we described two non-isomorphic DCWs ${\mathcal{A}}_{1}$ and
${\mathcal{A}}_{2}$ for $L$. The DCWs ${\mathcal{A}}_{1}$ and
${\mathcal{A}}_{2}$ can be viewed as nice GFG-NCWs. It is not hard to see that
there is no $2$-state GFG-NCW for $L$, implying that ${\mathcal{A}}_{1}$ and
${\mathcal{A}}_{2}$ are nice, equivalent, and minimal GFG-NCWs that are not
isomorphic, as required. Moreover, no $\alpha$-mutation leads to isomorphism.
∎

We continue to tDCWs. Again, we refer to $\alpha$-mutation, which amounts to
changing the membership of transitions in $\alpha$ while keeping the tNCW nice
and without changing its language. Note that unlike the case of GFG automata,
where dualization, i.e., viewing a tNCW as a tNBW, need not result in an
automaton for the complementary language, here results on tDCWs immediately
apply also to tDBWs. We start with some bad news, showing that there is no
canonicity also in the transition-based setting. Again, we refer to nice
minimal automata. Note that some of the properties of nice GFG-tNCWs are
trivial for minimal deterministic tDCW: being minimal and deterministic, then
clearly all states are reachable and GFG, the automata are semantically
deterministic and safe deterministic, and we only have to make them normal by
classifying transitions between safe components as $\alpha$-transitions. As we
show in Theorem 4.4, the fact we consider GFG automata is crucial for
canonization.

######  Theorem .

Nice, equivalent, and minimal tDCWs and tDBWs need not be isomorphic, and need
not be made isomorphic by $\alpha$-mutation.

###### Proof.

As a first example, consider the GFG-tNCW ${\mathcal{B}}_{\mathcal{S}}$ from
Figure 4. Recall that ${\mathcal{B}}_{\mathcal{S}}$ is DBP; that is, we can
prune some of its transitions and get an equivalent tDCW. In Figure 8 below,
we describe two tDCWs obtained from it by two different prunnings. It is not
hard to see that both tDCWs are nice and equivalent to
${\mathcal{B}}_{\mathcal{S}}$, yet are not isomorphic. Moreover, no
$\alpha$-mutation leads to isomorphism.

Figure 8. Two non-isomorphic equivalent minimal nice tDCWs, obtained by
different prunnings of ${\mathcal{B}}_{\mathcal{S}}$.

By removing the $a$-labeled transitions from the tDCWs in Figure 8, we obtain
a simpler example. Consider the tDCWs ${\mathcal{D}}^{\prime}_{1}$ and
${\mathcal{D}}^{\prime}_{2}$ in Figure 9. It is easy to see that
$L({\mathcal{D}}^{\prime}_{1})=L({\mathcal{D}}^{\prime}_{2})=(b+c)^{*}\cdot(b\cdot
c)^{\omega}$. Clearly, there is no single-state tDCW for this language. Also,
the tDCWs are not isomorphic, as a candidate bijection $\kappa$ has to be
$\bar{\alpha}$-transition respecting, and thus have $\kappa(q_{0})=s_{0}$ and
$\kappa(q_{1})=s_{1}$, yet then it is not $\alpha$-transition respecting. By
dualizing the acceptance condition of ${\mathcal{D}}^{\prime}_{1}$ and
${\mathcal{D}}^{\prime}_{2}$, we obtain two non-isomorphic tDBWs for the
complement language, of all words with infinitely many occurrences of $bb$ or
$cc$. Also here, no $\alpha$-mutation leads to isomorphism. ∎

Figure 9. Two non-isomorphic equivalent minimal nice tDCWs.

Hence, both GFGness and the use of transition-based acceptance conditions are
crucial for canonization, and we can conclude with the following.

######  Theorem .

There is no canonicity for minimal GFG-NCWs and for minimal tDCWs.

######  Remark .

Note that our definition of $\alpha$-mutations does not add new transitions to
the automaton. In particular, it preserves determinism and may thus seem
weaker in the context of GFG-NCWs than the definition used for GFG-tNCWs.
Note, however, that even if we allow the addition of transitions, there is no
canonicity for GFG-NCWs. Indeed, we cannot add transitions to the DCWs
${\mathcal{A}}_{1}$ and ${\mathcal{A}}_{2}$ from Figure 5 and obtain a GFG-NCW
that embodies both DCWs and still recognizes their language. As another
example, as we discuss in Section 6, it is shown in [44] that the NP-hardness
proof of DBW minimization applies also to GFG-NBW. While GFG-NBWs and GFG-NCWs
do not dualize each other, the proof in [44] applies also for GFG-NCW
minimization, and is based on associating a graph $G$ with a language $L_{G}$
such that there is a correspondence between minimal GFG-NCWs for $L_{G}$ and
minimal vertex covers for $G$. In more detail, for each vertex cover of $G$,
the state space of a minimal GFG-NCW for $L_{G}$ has an $\bar{\alpha}$-state
for each vertex of $G$ and an $\alpha$-state for each vertex in the cover.
Thus, vertices in the cover induce two states each. The transitions of the
automaton depend on the edges of $G$. Accordingly, different vertex covers
induce GFG-NCWs with different structures. In particular, different minimal
GFG-NCWs for $L_{G}$ are incomparable in many aspects, making $L_{G}$
resistant to more flexible definitions of canonicity.  ∎

The tDCWs in the proof of Theorem 4.4 are safe isomorphic. We continue with
some good news and study safe isomorphism between minimal nice tDCWs.

We say that an $\omega$-regular language $L$ is GFG-helpful if a minimal tDCW
for $L$ is bigger than a minimal GFG-tNCW for $L$.

######  Theorem .

Consider an $\omega$-regular language $L$. If $L$ is not GFG-helpful, then
every two nice and minimal tDCWs for $L$ are safe isomorphic.

###### Proof.

Consider a language $L$ that is not GFG-helpful, and consider two nice minimal
tDCWs ${\mathcal{A}}_{1}$ and ${\mathcal{A}}_{2}$ for $L$. Since $L$ is not
GFG-helpful, then ${\mathcal{A}}_{1}$ and ${\mathcal{A}}_{2}$ are also nice
minimal GFG-tNCWs for $L$. Hence, by Theorem 4.1, they are safe isomorphic. ∎

Note that safe isomorphism for $\omega$-regular languages that are GFG-helpful
is left open. Theorem 4.4 suggests that searching for a language $L$ that has
two minimal tDCWs that are not safe isomorphic, we can restrict attention to
languages that are GFG-helpful. Such languages are not common. Moreover, their
canonicity is less crucial, as working with a minimal GFG-tNCW for them is
more appealing. An examples of a family of languages that are GFG-helpful can
be found in [24], where it was shown that GFG-tNCWs may be exponentially more
succinct than tDCWs. In Section 5, we demonstrate the execution of our
algorithm on a GFG-helpful language in this family.

##  5\. An Example

Recall that an $\omega$-regular language $L$ is GFG-helpful if a minimal tDCW
for $L$ is bigger than a minimal GFG-tNCW for $L$. In this section, we present
a GFG-helpful language, and demonstrate an execution of our minimization
algorithm on a tDCW ${\mathcal{A}}$ that recognizes it. The language belongs
to the family of languages presented in [24], where it was shown that GFG-
tNCWs may be exponentially more succinct than tDCWs.

Consider the tDCW ${\mathcal{A}}$ over $\Sigma=\\{\sigma,\pi,\\#\\}$ that
appears in Figure 10.

Figure 10. The tDCW ${\mathcal{A}}$.

Recall that dashed transitions are $\alpha$-transitions. As ${\mathcal{A}}$ is
normal and deterministic, it is nice. Let
$L^{\prime}=\bigcup_{i\in\\{1,2,3\\}}L_{{\it
safe}}({\mathcal{A}}^{\\{q_{i}\\}})$. Then, it is not hard to see that all the
states in ${\mathcal{A}}$ are equivalent and they all recognizes the language
$L({\mathcal{A}})=\\{w:w\mbox{ has a suffix in }L^{\prime}\\}$.

Intuitively, as the language of ${\mathcal{A}}$ can be specified in terms of
the safe languages of the states $\\{q_{1}\\},\\{q_{2}\\}$, and $\\{q_{3}\\}$,
it is not surprising that we can define a GFG-tNCW for the language on top of
their safe component. The beauty of the example in [24] is the fact that a
minimal tDCW for the language needs more states.

As explained in [24], the letters $\sigma$, $\pi$ and $\\#$ can be viewed as
actions performed to tokens placed on a graph with vertices $\\{1,2,3\\}$. The
letter $\sigma$ moves each token from vertex $i$ to vertex $(i\mod 3)+1$. The
letter $\pi$ switches the tokens in vertices $1$ and $2$ (and leaves the token
in vertex $3$ in its vertex), and the letter $\\#$ “chops” the path traversed
by the token placed in vertex $1$ (and does not chop the paths traversed by
the other tokens). Then, ${\mathcal{A}}$ recognizes the set of words in which
at least one token traverses an infinite path.

Clearly, a nondeterministic automaton for $L$ can guess a single token and
follows its path, using the co-Büchi condition to make sure that there are
only finitely many positions in which the token is in vertex $1$ and the
letter $\\#$ is read (and so the path is chopped). On the other hand, a
deterministic automaton must remember the subset of tokens whose paths have
not been chopped since some break-point. For example, when the tDCW
${\mathcal{A}}$ is in state $\\{q_{1},q_{3}\\}$, indicating that the tokens in
vertices $1$ and $3$ are “alive”, and it reads the letter $\sigma$, it updates
the locations of the two living tokens to $(1\mod 3)+1$ and $(3\mod 3)+1$, and
so it moves to the state $\\{q_{1},q_{2}\\}$. When, however, ${\mathcal{A}}$
reads the letter $\\#$ from the state $\\{q_{1},q_{3}\\}$, only the token in
vertex $3$ stays alive, and ${\mathcal{A}}$ moves to the state $\\{q_{3}\\}$.
A break-point happens when ${\mathcal{A}}$ reads $\\#$ in the state
$\\{q_{1}\\}$. Then, all paths have been chopped, and so ${\mathcal{A}}$ has
an $\alpha$-transition to the state $\\{q_{2},q_{3}\\}$, from which it
continues to follow the tokens in vertices $2$ and $3$. The other
$\alpha$-transitions in ${\mathcal{A}}$ can also be defined as safe
transitions, but are in $\alpha$ due to normalization.

As explained in [24] and demonstrated by our minimization algorithm, a GFG
automaton for $L({\mathcal{A}})$ can also guess a single token and follow it.
Essentially, a guess should be made when the path traversed by the token we
follow is chopped. The GFG strategy makes use of the past and chooses to
continue and follow the token with the longest path traversed so far.

Formally, we proceed with minimizing ${\mathcal{A}}$ by applying the
minimization algorithm presented in Section 3. We begin by safe-centralizing
${\mathcal{A}}$, as explained in Section 3.2. First, by removing the
$\alpha$-transitions of ${\mathcal{A}}$, we get the safe components described
in Figure 11.

Figure 11. The safe components of ${\mathcal{A}}$.

Recall that ${\mathcal{A}}$ is nice and all of its states are equivalent. As
$\\{q_{1},q_{2}\\}\precsim\\{q_{1}\\}$, we have that ${\mathcal{A}}$ has a
single frontier
${\mathcal{S}}=\\{\\{\\{q_{1}\\},\\{q_{2}\\},\\{q_{3}\\}\\}\\}$. The automaton
${\mathcal{B}}_{{\mathcal{S}}}$ appears in Figure 12. As all the states of
${\mathcal{A}}$ are equivalent, we direct a $\\#$-labeled $\alpha$-transition
from $\\{q_{1}\\}$ to $\\{q_{1}\\},\\{q_{2}\\}$ and to $\\{q_{3}\\}$.

Figure 12. The tNCW ${\mathcal{B}}_{\mathcal{S}}$, for
${\mathcal{S}}={\\{\\{\\{q_{1}\\},\\{q_{2}\\},\\{q_{3}\\}\\}\\}}$.

We proceed by safe-minimizing ${\mathcal{B}}_{\mathcal{S}}$, as explained in
Section 3.3. Note that the safe languages of the states
$\\{q_{1}\\},\\{q_{2}\\}$ and $\\{q_{3}\\}$ of the GFG-tNCW
${\mathcal{B}}_{\mathcal{S}}$ from Figure 12 are pairwise different. Indeed,
$\\#^{\omega}\in(L_{{\it safe}}({\mathcal{A}}^{\\{q_{2}\\}})\cap L_{{\it
safe}}({\mathcal{A}}^{\\{q_{3}\\}}))\setminus L_{{\it
safe}}({\mathcal{A}}^{\\{q_{1}\\}})$ and $\sigma\cdot\\#^{\omega}\in L_{{\it
safe}}({\mathcal{A}}^{\\{q_{2}\\}})\setminus L_{{\it
safe}}({\mathcal{A}}^{\\{q_{3}\\}})$. Thus, there are no strongly-equivalent
states in ${\mathcal{B}}_{\mathcal{S}}$, and applying safe-minimization to
${\mathcal{B}}_{\mathcal{S}}$ results in the GFG-tNCW ${\mathcal{C}}$
identical to ${\mathcal{B}}_{\mathcal{S}}$.

To complete the example, we show that $L({\mathcal{A}})$ is GFG-helpful.

######  Proposition .

$L({\mathcal{A}})$ is GFG-helpful.

###### Proof.

Assume by contradiction that there is a tDCW
${\mathcal{D}}=\langle\Sigma,Q_{\mathcal{D}},q^{0}_{\mathcal{D}},\delta_{\mathcal{D}},\alpha_{\mathcal{D}}\rangle$
for $L({\mathcal{A}})$ with three states, and assume without loss of
generality that ${\mathcal{D}}$ is normal (and thus is nice). As
${\mathcal{D}}$ is deterministic, it is GFG. Hence, by Theorem 4.1, we have
that ${\mathcal{D}}$ and the GFG t-NCW ${\mathcal{C}}$ are safe isomorphic.
Therefore, ${\mathcal{D}}$ is obtained by pruning the transitions of the GFG-
tNCW ${\mathcal{B}}_{\mathcal{S}}$ in Figure 12 and by choosing one of its
states as the initial state. Let $x_{1}$ be a finite word such that
$\delta_{\mathcal{D}}(q^{0}_{\mathcal{D}},x_{1})=\\{q_{1}\\}$. To reach a
contradiction, we distinguish between three cases. If the $\alpha$-transition
$\langle\\{q_{1}\\},\\#,\\{q_{1}\\}\rangle$ is in ${\mathcal{D}}$, then
consider the word $w=x_{1}\cdot\\#^{\omega}$. As $\\#^{\omega}\in L_{{\it
safe}}({\mathcal{A}}^{\\{q_{2}\\}})$, we conclude that $w\in
L({\mathcal{A}})$. On the other hand, as $\\#^{\omega}$ is rejected from the
state $\\{q_{1}\\}$ in ${\mathcal{D}}$, we conclude that $w\notin
L({\mathcal{D}})$. Also, if the $\alpha$-transition
$\langle\\{q_{1}\\},\\#,\\{q_{2}\\}\rangle$ is in ${\mathcal{D}}$, then
consider the word $w=x_{1}\cdot(\\#\cdot\pi)^{\omega}$. As
$(\\#\cdot\pi)^{\omega}\in L_{{\it safe}}({\mathcal{A}}^{\\{q_{3}\\}})$, we
conclude that $w\in L({\mathcal{A}})$. On the other hand, as
$(\\#\cdot\pi)^{\omega}$ is rejected from the state $\\{q_{1}\\}$ in
${\mathcal{D}}$, we conclude that $w\notin L({\mathcal{D}})$. Finally, if the
$\alpha$-transition $\langle\\{q_{1}\\},\\#,\\{q_{3}\\}\rangle$ is in
${\mathcal{D}}$, then consider the word
$w=x_{1}\cdot(\\#\cdot\pi\cdot\sigma)^{\omega}$. As
$(\\#\cdot\pi\cdot\sigma)^{\omega}\in L_{{\it
safe}}({\mathcal{A}}^{\\{q_{2}\\}})$, we conclude that $w\in
L({\mathcal{A}})$. On the other hand, as $(\\#\cdot\pi\cdot\sigma)^{\omega}$
is rejected from the state $\\{q_{1}\\}$ in ${\mathcal{D}}$, we conclude that
$w\notin L({\mathcal{D}})$. As all different prunings of
${\mathcal{B}}_{\mathcal{S}}$ result in losing words from the language, we
conclude that ${\mathcal{D}}$ cannot be equivalent to ${\mathcal{A}}$, and we
have reached a contradiction. ∎

##  6\. Discussion

Recall that for DCWs, minimization is NP-complete [43]. Considering GFG-tNCWs
rather than DCWs involves two modifications of the original DCW-minimization
question: a transition to GFG rather than deterministic automata, and a
transition to transition-based rather than state-based acceptance. A natural
question that arises is whether both modifications are crucial for efficiency.
It was recently shown [44] that the NP-completeness proof of Schewe for DBW
minimization can be generalized to GFG-NBWs and GFG-NCWs. This suggests that