0  11institutetext:  State Key Laboratory of Computer Science, Institute of
Software, Chinese Academy of Sciences, China 22institutetext: Institute of
Intelligent Software Guangzhou, China 33institutetext: University of Chinese
Academy of Sciences, China 44institutetext: Rice University, USA

# Divide-and-Conquer Determinization of Büchi Automata Based on SCC
Decomposition

Yong Li 11 0000-0002-7301-9234 Andrea Turrini 1122 0000-0003-4343-9323 Weizhi
Feng 1133 0000-0003-0710-223X
Moshe Y. Vardi 44 0000-0002-0661-5773 Lijun Zhang 1122 0000-0002-3692-2088

###### Abstract

The determinization of a nondeterministic Büchi automaton (NBA) is a
fundamental construction of automata theory, with applications to
probabilistic verification and reactive synthesis. The standard
determinization constructions, such as the ones based on the Safra-Piterman’s
approach, work on the whole NBA. In this work we propose a divide-and-conquer
determinization approach. To this end, we first classify the strongly
connected components (SCCs) of the given NBA as inherently weak, deterministic
accepting, and nondeterministic accepting. We then present how to determinize
each type of SCC _independently_ from the others; this results in an easier
handling of the determinization algorithm that takes advantage of the
structure of that SCC. Once all SCCs have been determinized, we show how to
compose them so to obtain the final equivalent deterministic Emerson-Lei
automaton, which can be converted into a deterministic Rabin automaton without
blow-up of states and transitions. We implement our algorithm in a our tool
COLA and empirically evaluate COLA with the state-of-the-art tools Spot and
Owl on a large set of benchmarks from the literature. The experimental results
show that our prototype COLA outperforms Spot and Owl regarding the number of
states and transitions.

##  1 Introduction

Nondeterministic Büchi automata (NBAs) [6] are finite automata accepting
infinite words; they are a simple and popular formalism used in model checking
to represent reactive and non-terminating systems and their specifications,
characterized by $\omega$-regular languages [2]. Due to their nondeterminism,
however, there are situations in which NBAs are not suitable, so deterministic
automata are required, as it happens in probabilistic verification [2] and
reactive synthesis from logical specifications [33]. Consequently, translating
NBAs into equivalent deterministic $\omega$-automata (that is, deterministic
automata accepting the same $\omega$-regular language) is a necessary
operation for solving these problems. While there exists a direct translation
from linear temporal logic (LTL) to deterministic $\omega$-automata [15], not
all problems of interests can be formalized by LTL formulas, since LTL cannot
express the full class of $\omega$-regular properties [41]. For instance, we
have to use Linear Dynamic Logic (LDL) [40, 11] instead of LTL to express the
$\omega$-regular property “the train will arrive in every odd minute”. To the
best of our knowledge, we still need to go through the determinization of NBAs
for LDL to obtain deterministic $\omega$-automata. Therefore, NBA
determinization is very important in verifying the whole class of
$\omega$-regular properties.

The determinization of NBAs is a fundamental problem in automata theory that
has been actively studied for decades. For the determinization of
nondeterministic automata accepting finite words, it suffices to use a subset
construction [20]. Determinization constructions for NBAs are, however, much
more involved since the simple subset construction is not sufficient [35].
Safra [35] gave the first determinization construction for NBAs with the
optimal complexity $2^{\mathsf{O}(n\log n)}$, here $n$ is the number of states
of the input NBA; Michel [29] then gave a lower bound $n!$ for determinizing
NBAs. Safra’s construction has been further optimized by Piterman [32] to
$\mathsf{O}((n!)^{2})$ [37], resulting in the widely known Safra-Piterman’s
construction. The Safra-Piterman’s construction is rather challenging, while
still being the most practical way for Büchi complementation [39]. Research on
determinization since then either aims at developing alternative Safraless
constructions [21, 18, 27] or further tightening the upper and lower bounds of
the NBA determinization [9, 42, 38, 25].

In this paper, we focus on the _practical_ aspects of Büchi determinization.
All works on determinization mentioned above focus on translating NBAs to
either deterministic Rabin or deterministic parity automata. According to
[36], the more relaxed an acceptance condition is, the more succinct a finite
automaton can be, regarding the number of states. In view of this, we consider
the translation of NBAs to deterministic _Emerson-Lei_ automata (DELAs) [13,
36] whose acceptance condition is an arbitrary Boolean combination of sets of
transitions to be seen finitely or infinitely often, the most generic
acceptance condition for a deterministic automaton. We consider here
transition-based automata rather than the usual state-based automata since the
former can be more succinct [12].

The Büchi determinization algorithms available in literature operate on the
_whole_ NBA structure at once, which does not scale well in practice due to
the complex structure and the big size of the input NBA. In this work we apply
a _divide-and-conquer_ methodology to Büchi determinization. We propose a
determinization algorithm for NBAs to DELAs based on their strongly connected
components (SCCs) decomposition. We first classify the SCCs of the given NBA
into three types: _inherently weak_ , in which either all cycles do not visit
accepting transitions or all must visit accepting transitions; _deterministic
accepting_ and _nondeterministic accepting_ , which contain an accepting
transition and are deterministic or nondeterministic, respectively. We show
how to divide the whole Büchi determinization problem into the determinization
for each type of SCCs _independently_ , in which the determinization for an
SCC takes advantage of the structure of that SCC. Then we show how to compose
the results of the local determinization for each type of SCCs, leading to the
final equivalent DELA. An extensive experimental evaluation confirms that the
divide-and-conquer approach pays off also for the determinization of the whole
NBA.

##### Contributions.

First, we propose a _divide-and-conquer_ determinization algorithm for NBAs,
which takes advantage of the structure of different types of SCCs and
determinizes SCCs independently. Our construction builds an equivalent DELA
that can be converted into a deterministic Rabin automaton without blowing up
states and transitions (cf. Theorem 4). To the best of our knowledge, we
propose the _first_ determinization algorithm that constructs a DELA from an
NBA. Second, we show that there exists a family of NBAs for which our
algorithm gives a DELA of size $2^{n+2}$ while classical works construct a DPA
of size at least $n!$ (cf. Theorem 5). Third, we implement our algorithm in
our tool COLA and evaluate it with the state-of-the-art tools Spot [12] and
Owl [23] on a large set of benchmarks from the literature. The experiments
show that COLA outperforms Spot and Owl regarding the number of states and
transitions. Finally, we remark that the determinization complexity for some
classes of NBAs can be exponentially better than the known ones (cf. Corollary
4).

We defer all proofs to Appendix 0.A.

##  2 Preliminaries

Let $\Sigma$ be a given alphabet, i.e., a finite set of letters. A transition-
based Emerson-Lei automaton can be seen as a generalization of other types of
$\omega$-automata, like Büchi, Rabin or parity. Formally, it is defined in the
HOA format [1] as follows:

######  Definition 1.

A _nondeterministic Emerson-Lei automaton_ (NELA) is a tuple
$\mathcal{A}=(Q,\iota,\delta,\Gamma_{k},\mathsf{p},\mathsf{Acc})$, where $Q$
is a finite set of _states_ ; $\iota\in Q$ is the _initial state_ ;
$\delta\subseteq Q\times\Sigma\times Q$ is a _transition relation_ ;
$\Gamma_{k}=\\{0,1,\cdots,k\\}$, where $k\in\mathbb{N}$, is a set of _colors_
; $\mathsf{p}\colon\delta\to 2^{\Gamma_{k}}$ is a _coloring function_ for
transitions; and $\mathsf{Acc}$ is an _acceptance formula_ over $\Gamma_{k}$
given by the following grammar, where $x\in\Gamma_{k}$:

$\alpha:=\mathsf{tt}\mid\mathsf{ff}\mid\mathsf{Fin}(x)\mid\mathsf{Inf}(x)\mid\alpha\lor\alpha\mid\alpha\land\alpha.$

We remark that the colors in $\Gamma_{k}$ are not required to be all used in
$\mathsf{Acc}$. We call a NELA a _deterministic_ Emerson-Lei automaton (DELA)
if for each $q\in Q$ and $a\in\Sigma$, there is at most one $q^{\prime}\in Q$
such that $(q,a,q^{\prime})\in\delta$.

In the remainder of the paper, we consider $\delta$ also as a function
$\delta\colon Q\times\Sigma\to 2^{Q}$ such that $q^{\prime}\in\delta(q,a)$
whenever $(q,a,q^{\prime})\in\delta$; we also write
$q\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle
a$\cr\kern 1.29167pt\cr$\longrightarrow$\cr}}}q^{\prime}$ for
$(q,a,q^{\prime})\in\delta$ and we extend it to words
$u=u_{\\_}{0}u_{\\_}{1}\cdots u_{\\_}{n}\in\Sigma^{*}$ in the natural way,
i.e., $q\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle
u$\cr\kern
1.29167pt\cr$\longrightarrow$\cr}}}q^{\prime}=q\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle{u}[0]$\cr\kern
1.29167pt\cr$\longrightarrow$\cr}}}q_{\\_}{1}\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle{u}[1]$\cr\kern
1.29167pt\cr$\longrightarrow$\cr}}}\cdots\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle{u}[n]$\cr\kern
1.29167pt\cr$\longrightarrow$\cr}}}q^{\prime}$, where ${\sigma}[i]$ denotes
the element $s_{\\_}{i}$ of the sequence of elements
$\sigma=s_{\\_}{0}s_{\\_}{1}s_{\\_}{2}\cdots$ at position $i$. We assume
without loss of generality that each automaton is _complete_ , i.e., for each
state $q\in Q$ and letter $a\in\Sigma$, we have $\delta(q,a)\neq\emptyset$. If
it is not complete, we make it complete by adding a fresh state
$q_{\\_}{\bot}\notin Q$ and redirecting all missing transitions to it.

A _run_ of $\mathcal{A}$ over an $\omega$-word $w\in\Sigma^{\omega}$ is an
infinite sequence of states $\rho$ such that ${\rho}[0]=\iota$, and for each
$i\in\mathbb{N}$, $({\rho}[i],{w}[i],{\rho}[i+1])\in\delta$.

The _language_ $\mathsf{L}(\mathcal{A})$ of $\mathcal{A}$ is the set of words
accepted by $\mathcal{A}$, i.e., the set of words $w\in\Sigma^{\omega}$ such
that there exists a run $\rho$ of $\mathcal{A}$ over $w$ such that
$\mathsf{p}(\mathit{inf}({\rho}))\models\mathsf{Acc}$, where
$\mathit{inf}({\rho})=\\{\,(q,a,q^{\prime})\in\delta\mid\forall
i\in\mathbb{N}.\exists
j>i.({\rho}[j],{w}[j],{\rho}[j+1])=(q,a,q^{\prime})\,\\}$ and the satisfaction
relation $\models$ is defined recursively as follows: given
$M\subseteq\Gamma_{k}$,

$\displaystyle M$ $\displaystyle\models\mathsf{tt},$ $\displaystyle M$
$\displaystyle\models\mathsf{Fin}(x)\text{ iff $x\notin M$,}$ $\displaystyle
M$ $\displaystyle\models\alpha_{\\_}{1}\lor\alpha_{\\_}{2}\text{ iff
$M\models\alpha_{\\_}{1}$ or $M\models\alpha_{\\_}{2}$,}$ $\displaystyle M$
$\displaystyle\not\models\mathsf{ff},$ $\displaystyle M$
$\displaystyle\models\mathsf{Inf}(x)\text{ iff $x\in M$,}$ $\displaystyle M$
$\displaystyle\models\alpha_{\\_}{1}\land\alpha_{\\_}{2}\text{ iff
$M\models\alpha_{\\_}{1}$ and $M\models\alpha_{\\_}{2}$.}$

Intuitively, a run $\rho$ over $w$ is accepting if the set of colors (induced
by $\mathsf{p}$) that occur infinitely often in $\rho$ satisfies the
acceptance formula $\mathsf{Acc}$. Here $\mathsf{Fin}(x)$ specifies that the
color $x$ only appears for finitely many times while $\mathsf{Inf}(x)$
requires the color $x$ to be seen infinitely often.

The more common types of $\omega$-automata, such as Büchi, parity and Rabin
can be treated as Emerson-Lei automata with the following acceptance formulas.

######  Definition 2.

A NELA $\mathcal{A}=(Q,\iota,\delta,\Gamma_{k},\mathsf{p},\mathsf{Acc})$ is
said to be

  * •

a _Büchi automaton_ (BA) if $k=0$ and $\mathsf{Acc}=\mathsf{Inf}(0)$.
Transition with color $0$ are usually called _accepting_ transitions. Thus, a
run $\rho$ is accepting if
$\mathsf{p}(\mathit{inf}({\rho}))\cap\\{0\\}\neq\emptyset$, i.e., $\rho$ takes
accepting transitions infinitely often;

  * •

a _parity automaton_ (PA) if $k$ is even and
$\mathsf{Acc}=\bigvee_{\\_}{c=0}^{k/2}(\bigwedge_{\\_}{i=1}^{c}\mathsf{Fin}(2i-1)\land\mathsf{Inf}(2c))$.
A run $\rho$ is accepting if the minimum color in
$\mathsf{p}(\mathit{inf}({\rho}))$ is even;

  * •

a _Rabin automaton_ (RA) if $k$ is an odd number and
$\mathsf{Acc}=(\mathsf{Fin}(0)\land\mathsf{Inf}(1))\lor\cdots\lor(\mathsf{Fin}(k-1)\land\mathsf{Inf}(k))$.
Intuitively, a run $\rho$ is accepting if there exists an odd integer $0<j\leq
k$ such that $j-1\notin\mathsf{p}(\mathit{inf}({\rho}))$ and
$j\in\mathsf{p}(\mathit{inf}({\rho}))$.

When the NELA
$\mathcal{A}=(Q,\iota,\delta,\Gamma_{k},\mathsf{p},\mathsf{Acc})$ is a
nondeterministic BA (NBA), we just write $\mathcal{A}$ as $(Q,\iota,\delta,F)$
where $F$ is the set of accepting transitions. We call a set $C\subseteq Q$ a
_strongly connected component_ (SCC) of $\mathcal{A}$ if for every pair of
states $q,q^{\prime}\in C$, we have that
$q\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle
u$\cr\kern 1.29167pt\cr$\longrightarrow$\cr}}}q^{\prime}$ for some
$u\in\Sigma^{*}$ and
$q^{\prime}\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle
v$\cr\kern 1.29167pt\cr$\longrightarrow$\cr}}}q$ for some $v\in\Sigma^{*}$,
i.e., $q$ and $q^{\prime}$ can be reached by each other; by default, each
state $q\in Q$ reaches itself. $C$ is a _maximal_ SCC if it is _not_ a proper
subset of another SCC. _All_ SCCs considered in the work are maximal. We call
an SCC $C$ _accepting_ if there is a transition
$(q,a,q^{\prime})\in(C\times\Sigma\times C)\cap F$ and _nonaccepting_
otherwise. We say that an SCC $C^{\prime}$ is _reachable_ from an SCC $C$ if
there exist $q\in C$ and $q^{\prime}\in C^{\prime}$ such that
$q\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle
u$\cr\kern 1.29167pt\cr$\longrightarrow$\cr}}}q^{\prime}$ for some
$u\in\Sigma^{*}$. An SCC $C$ is _inherently weak_ if either every cycle going
through the $C$-states visits at least one accepting transition or none of the
cycles visits an accepting transition. We say that an SCC $C$ is
_deterministic_ if for every state $q\in C$ and $a\in\Sigma$, we have
$|\delta(q,a)\cap C|\leq 1$. Note that a state $q$ in a deterministic SCC $C$
can have multiple successors for a letter $a$, but at most one successor
remains in $C$.

Figure 1: An example of NBA.

Figure 1 shows an example of NBA we will use for our examples in the remainder
of the paper; we depict the accepting transitions with a double arrow.
Clearly, inside each SCC, depicted as a box, each state can be reached by any
other state, and the SCCs are maximal. The SCC $\\{q_{\\_}{2},q_{\\_}{3}\\}$
is inherently weak and accepting, since every cycle takes an accepting
transition; the SCC $\\{q_{\\_}{6}\\}$ is also inherently weak, but
nonaccepting, since every cycle never takes an accepting transition. The
remaining two SCCs, i.e., $\\{q_{\\_}{0},q_{\\_}{1}\\}$ and
$\\{q_{\\_}{4},q_{\\_}{5}\\}$, are not inherently weak, since some cycle takes
accepting transitions (like the cycle
$q_{\\_}{0}\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle
a$\cr\kern 1.29167pt\cr$\longrightarrow$\cr}}}q_{\\_}{0}$) while others do not
(like the cycle
$q_{\\_}{0}\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle
b$\cr\kern 1.29167pt\cr$\longrightarrow$\cr}}}q_{\\_}{0}$). Both SCCs contain
an accepting transition, so they are accepting; the SCC
$\\{q_{\\_}{0},q_{\\_}{1}\\}$ is clearly nondeterministic, while the SCC
$\\{q_{\\_}{4},q_{\\_}{5}\\}$ is deterministic. Note that from $q_{\\_}{5}$ we
have two transitions labelled by $b$, but only the transition
$q_{\\_}{5}\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle
b$\cr\kern 1.29167pt\cr$\longrightarrow$\cr}}}q_{\\_}{4}$ remains inside the
SCC, while the other transition
$q_{\\_}{5}\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle
b$\cr\kern 1.29167pt\cr$\longrightarrow$\cr}}}q_{\\_}{6}$ leaves the SCC, so
the SCC is still deterministic.

The following proposition is well known and is often used in prior works.

######  Proposition 1.

Let $\mathcal{A}$ be an NBA and $w\in\Sigma^{\omega}$. A run of $\mathcal{A}$
over $w$ will eventually stay in an SCC. Moreover, if
$w\in\mathsf{L}(\mathcal{A})$, every accepting run of $\mathcal{A}$ over $w$
will eventually stay in an accepting SCC.

Proposition 1 is the key ingredient of our algorithm: it allows us to
determinize the SCCs independently as $\mathsf{L}(\mathcal{A})$ is the union
of the words whose runs stay in each accepting SCCs. In the remainder of the
paper, we first present a translation from an NBA $\mathcal{A}$ to a DELA
$\mathcal{A}^{\mathsf{E}}$ based on the SCC decomposition of $\mathcal{A}$.
The obtained DELA $\mathcal{A}^{\mathsf{E}}$ in fact can be converted to a
_deterministic_ Rabin automaton (DRA) $\mathcal{A}^{\mathsf{R}}$ without
blowing up states and transitions, i.e., we can just convert the coloring
function and the acceptance formula of $\mathcal{A}^{\mathsf{E}}$ to DRAs.

##  3 Determinization Algorithms of SCCs

Determinizing each SCC of $\mathcal{A}$ independently is not straightforward
since it may be reached from the initial state only after reading a nonempty
finite word; moreover, there can be words of different length leading to the
SCC, entering through different states. To keep track of the different
arrivals in an SCC at different times, we make use of run DAGs [24], that are
a means to organize the runs of $\mathcal{A}$ over a word $w$. In this
section, we first recall the concept of run DAGs and then describe how to
determinize SCCs with their help.

######  Definition 3.

Let $\mathcal{A}=(Q,\iota,\delta,F)$ be an NBA and $w\in\Sigma^{\omega}$ be a
word. The run DAG $\mathcal{G}_{\mathcal{A},w}=\langle{V},{E}\rangle$ of
$\mathcal{A}$ over $w$ is defined as follows: the set of vertices $V\subseteq
Q\times\mathbb{N}$ is defined as $V=\bigcup_{\\_}{l\geq
0}(V_{\\_}{l}\times\\{l\\})$ where $V_{\\_}{0}=\\{\iota\\}$ and
$V_{\\_}{l+1}=\delta(V_{\\_}{l},{w}[l])$ for every $l\in\mathbb{N}$; there is
an edge $(\langle{q},{l}\rangle,\langle{q^{\prime}},{l^{\prime}}\rangle)\in E$
if $l^{\prime}=l+1$ and $q^{\prime}\in\delta(q,{w}[l])$.

Intuitively, a state $q$ at a level $\ell$ may occur in several runs and only
one vertex is needed to represent it, i.e., the vertex
$\langle{q},{\ell}\rangle$ who is said to be on level $\ell$. Note that by
definition, there are at most $|Q|$ vertices on each level. An edge
$(\langle{q},{l}\rangle,\langle{q^{\prime}},{l+1}\rangle)$ is an _$F$ -edge_
if $(q,{w}[l],q^{\prime})\in F$. An infinite sequence of vertices
$\gamma=\langle{q_{\\_}{0}},{0}\rangle\langle{q_{\\_}{1}},{1}\rangle\cdots$ is
called an _$\omega$ -branch_ of $\mathcal{G}_{\mathcal{A},w}$ if
$q_{\\_}{0}=\iota$ and for each $\ell\in\mathbb{N}$, we have
$(\langle{q_{\\_}{\ell}},{\ell}\rangle,\langle{q_{\\_}{\ell+1}},{\ell+1}\rangle)\in
E$. We can observe that there is a bijection between the set of runs of
$\mathcal{A}$ on $w$ and the set of $\omega$-branches in
$\mathcal{G}_{\mathcal{A},w}$. In fact, to a run
$\rho=q_{\\_}{0}q_{\\_}{1}\cdots$ of $\mathcal{A}$ over $w$ corresponds the
$\omega$-branch
$\hat{\rho}=\langle{q_{\\_}{0}},{0}\rangle\langle{q_{\\_}{1}},{1}\rangle\cdots$
and, symmetrically, to an $\omega$-branch
$\gamma=\langle{q_{\\_}{0}},{0}\rangle\langle{q_{\\_}{1}},{1}\rangle\cdots$
corresponds the run $\hat{\gamma}=q_{\\_}{0}q_{\\_}{1}\cdots$. Thus $w$ is
accepted by $\mathcal{A}$ if and only if there exists an $\omega$-branch in
$\mathcal{G}_{\mathcal{A},w}$ that takes $F$-edges infinitely often.

In the remainder of this section, we will introduce the algorithms for
computing the successors of the current states inside different types of SCCs,
with the help of run DAGs. We fix an NBA $\mathcal{A}=(Q,\iota,\delta,F)$ and
a word $w\in\Sigma^{\omega}$. We let $Q=\\{q_{\\_}{1},\dots,q_{\\_}{n}\\}$ and
apply a total order $\preccurlyeq$ on $Q$ such that $q_{\\_}{i}\preccurlyeq
q_{\\_}{j}$ if $i<j$. Let $S_{\\_}{\ell}\subseteq Q$, $\ell\in\mathbb{N}$, be
the set of states reached at the level $\ell$ in the run DAG
$\mathcal{G}_{\mathcal{A},w}$; we assume that this sequence
$S_{\\_}{0},\cdots,S_{\\_}{\ell},\cdots$ is available as a _global_ variable
during the computations of every SCC where $S_{\\_}{0}=\\{\iota\\}$ and
$S_{\\_}{\ell+1}=\delta(S_{\\_}{\ell},{w}[\ell])$.

When determinizing the given NBA $\mathcal{A}$, we classify its SCCs into
three types, namely inherently weak SCCs (IWCs), deterministic-accepting SCCs
(DACs) and nondeterministic-accepting SCCs (NACs). We assume that all DACs and
NACs are _not_ inherently weak, otherwise they will be classified as IWCs.

In our determinization construction, every level in
$\mathcal{G}_{\mathcal{A},w}$ corresponds to a state in our constructed DELA
$\mathcal{A}^{\mathsf{E}}$ while reading the $\omega$-word $w$. Let
$m_{\\_}{\ell}$ be the state of $\mathcal{A}^{\mathsf{E}}$ at level $\ell$.
The computation of the successor $m_{\\_}{\ell+1}$ of $m_{\\_}{\ell}$ for the
letter ${w}[\ell]$ will be divided into the successor computation for states
in IWCs, DACs and NACs independently. Then the successor $m_{\\_}{\ell+1}$ is
just the Cartesian product of these successors. In the remainder of this
section, we present how to compute the successors for the states in each type
of SCCs.

###  3.1 Successor Computation inside IWCs

As we have seen, $\mathcal{G}_{\mathcal{A},w}$ contains all runs of
$\mathcal{A}$ over $w$, including those within DACs and NACs. Since we want to
compute the successor only for IWCs, we focus on the states inside the IWCs
and ignore other states in DACs and NACs. Let $\mathsf{W}$ be the set of
states in all IWCs and $\mathsf{WA}\subseteq\mathsf{W}$ be the set of states
in all accepting IWCs.

For the run DAG $\mathcal{G}_{\mathcal{A},w}$, we use a pair of sets of states
$(P_{\\_}{\ell},O_{\\_}{\ell})\in 2^{\mathsf{W}}\times 2^{\mathsf{WA}}$ to
represent the set of IWC states reached in $\mathcal{G}_{\mathcal{A},w}$ at
level $\ell$. The set $P_{\\_}{\ell}$ is used to keep track of the states in
$\mathsf{W}$ reached at level $\ell$, while $O_{\\_}{\ell}$, inspired by the
breakpoint construction used in [30], keeps only the states reached in
$\mathsf{WA}$, that is, it is used to track the runs that stay in accepting
IWCs. Since by definition each cycle inside an accepting IWC must visit an
accepting transition, for each run tracked by $O_{\\_}{\ell}$ we do not need
to remember whether we have taken an accepting transition: it suffices to know
whether the run is still inside some accepting IWC or whether the run has left
them.

We now show how to compute the sets $(P_{\\_}{\ell},O_{\\_}{\ell})$ along $w$.
For level $0$, we simply set $P_{\\_}{0}=\\{\iota\\}\cap\mathsf{W}$ and
$O_{\\_}{0}=\emptyset$. For the other levels, given
$(P_{\\_}{\ell},O_{\\_}{\ell})$ at level $\ell\in\mathbb{N}$, the encoding
$(P_{\\_}{\ell+1},O_{\\_}{\ell+1})$ for the next level $\ell+1$ is defined as
follows:

  * •

$P_{\\_}{\ell+1}=S_{\\_}{\ell+1}\cap\mathsf{W}$, i.e., $P_{\\_}{\ell+1}$ keeps
track of the $\mathsf{W}$-states reached at level $\ell+1$;

  * •

if $O_{\\_}{\ell}\neq\emptyset$, then
$O_{\\_}{\ell+1}=\delta(O_{\\_}{\ell},{w}[\ell])\cap\mathsf{WA}$, otherwise
$O_{\\_}{\ell+1}=P_{\\_}{\ell+1}\cap\mathsf{WA}$.

Intuitively, the $O$-set keeps track of the runs that stay in the accepting
IWCs. So if $O_{\\_}{\ell}\neq\emptyset$, then $O_{\\_}{\ell+1}$ maintains the
runs remaining in some accepting IWC; otherwise, $O_{\\_}{\ell}=\emptyset$
means that at level $\ell$ all runs seen so far in the accepting IWCs have
left them, so we can just start to track the new runs that entered the
accepting IWCs but were not tracked yet.

On the right we show the fragment of the run DAG
$\mathcal{G}_{\mathcal{A},a^{\omega}}$ for the NBA $\mathcal{A}$ shown in
Figure 1 and its IWCs; we have
$\mathsf{W}=\\{q_{\\_}{2},q_{\\_}{3},q_{\\_}{6}\\}$ and
$\mathsf{WA}=\\{q_{\\_}{2},q_{\\_}{3}\\}$. The set $P_{\\_}{\ell}$ contains
all states $q$ at level $\ell$; the set $O_{\\_}{\ell}$ contains the
underlined ones. As a concrete application of the construction given above,
from $P_{\\_}{3}=\\{q_{\\_}{2},q_{\\_}{3}\\}$ and
$O_{\\_}{3}=\delta(O_{\\_}{2},a)\cap\mathsf{WA}=\\{q_{\\_}{3}\\}$, at level
$4$ we get $P_{\\_}{4}=\\{q_{\\_}{2},q_{\\_}{3},q_{\\_}{6}\\}$ and
$O_{\\_}{4}=\delta(O_{\\_}{3},a)\cap\mathsf{WA}=\\{q_{\\_}{2}\\}$.

It is not difficult to see that checking whether $w$ is accepted reduces to
check whether the number of empty $O$-sets is finite. We assign color $1$ to
the transition from $(P_{\\_}{\ell},O_{\\_}{\ell})$ to
$(P_{\\_}{\ell+1},O_{\\_}{\ell+1})$ via ${w}[\ell]$ if
$O_{\\_}{\ell}=\emptyset$, otherwise we assign color $2$. Lemma 3.1 formalizes
the relation between accepting runs staying in accepting IWCs and the colors
we get from our construction.

lemmaAccIWCs  (1) There exists an accepting run of $\mathcal{A}$ over $w$
eventually staying in an accepting IWC if and only if we receive color $1$
finitely many times when constructing the sequence
$(P_{\\_}{0},O_{\\_}{0})\cdots(P_{\\_}{\ell},O_{\\_}{\ell})\cdots$ while
reading $w$.  (2) The number of possible $(P,O)$ pairs is at most
$3^{|\mathsf{W}|}$.  The proof idea is trivial: an accepting run $\rho$ that
stays in an accepting IWC will make the $O$-set contain $\rho$ forever and we
always get color $2$ from some point on. A possible pair $(P,O)$ can be seen
as choosing a state from $\mathsf{W}$, which can be from $\mathsf{W}\setminus
P$, $P\cap O$ and $P\setminus O$, respectively. It thus gives at most
$3^{|\mathsf{W}|}$ possibilities. We refer to Appendix 0.A.1 for the detailed
proof of Lemma 3.1.

To ease the construction for the whole NBA $\mathcal{A}$, we make the above
computation of successors available as a function $\mathsf{weakSucc}$, which
takes as input a pair of sets $(P,O)$ and a letter $a$, and returns the
successor $(P^{\prime},O^{\prime})$ and the corresponding color
$c\in\\{1,2\\}$ for the transition $((P,O),a,(P^{\prime},O^{\prime}))$.

The construction we gave above works on all IWCs at the same time; considering
IWCs separately does not improve the resulting complexity. If there are two
accepting IWCs with $n_{\\_}{1}$ and $n_{\\_}{2}$ states, respectively, then
the number of possible $(P,O)$ pairs for the two IWCs is $3^{n_{\\_}{1}}$ and
$3^{n_{\\_}{2}}$, respectively. When combining the pairs for each IWC
together, the resulting number of pairs in the Cartesian product is
$3^{n_{\\_}{1}}\times 3^{n_{\\_}{2}}=3^{n_{\\_}{1}+n_{\\_}{2}}$, which is the
same as considering them together. On the other hand, for each accepting IWC,
we need to use two colors, so we need $2\cdot i$ colors in total for $i$
accepting IWCs, instead of just two colors by operating on all IWCs together.
Hence, we prefer to work on all IWCs at once.

###  3.2 Successor Computation inside DACs

In contrast to IWCs, we do not work on all DACs at once but we process each
DAC separately. This is because there may be nondeterminism between DACs: a
run in a DAC may branch into multiple runs that jump to different DACs, which
requires us to resort to a Safra-Piterman’s construction [35, 32] when
considering all DACs at once. Working on each DAC separately, instead, allows
us to take advantage of the internal determinism: for a given DAC
$\mathsf{D}$, the transition relation $\delta$ inside $\mathsf{D}$, denoted as
$\delta_{D}=(\mathsf{D}\times\Sigma\times\mathsf{D})\cap\delta$, is now
deterministic.

Although every run $\rho$ entering $\mathsf{D}$ can have only one successor in
$\mathsf{D}$, $\rho$ may just leave $\mathsf{D}$ while new runs can enter
$\mathsf{D}$, which makes it difficult to check whether there exists an
accepting run that remains trapped into $\mathsf{D}$. In order to identify
accepting runs staying in $\mathsf{D}$, we identify the following two rules
for distinguishing runs that come to $\mathsf{D}$ by means of _unique_
labelling numbers:

(1) the runs already in $\mathsf{D}$ have precedence over newly entering runs,
thus the latter get assigned a higher number. In practice, the labelling keeps
track of the relative order of entering $\mathsf{D}$, thus the lower the
labelling value is, the earlier the run came to $\mathsf{D}$;  (2) when two
runs in $\mathsf{D}$ merge, we only keep the run that came to $\mathsf{D}$
earlier, i.e., the run with lower number. If two runs enter $\mathsf{D}$ at
the same time, we let them enter according to the total state order
$\preccurlyeq$ for their respective entry states.

We use a level-labelling function
$\mathfrak{g}_{\\_}{\ell}\colon\mathsf{D}\to\\{1,\cdots,2\cdot|\mathsf{D}|\\}\cup\\{\infty\\}$
to encode the set of $\mathsf{D}$-states reached at level $\ell$ of the run
DAG $\mathcal{G}_{\mathcal{A},w}$.

Here we use $\mathfrak{g}_{\\_}{\ell}(q)=\infty$ to indicate that the state
$q\in\mathsf{D}$ is not reached by $\mathcal{A}$ at level $\ell$.

At level $0$, we set $\mathfrak{g}_{\\_}{0}(q)=\infty$ for every state
$q\in\mathsf{D}\setminus\\{\iota\\}$, and $\mathfrak{g}_{\\_}{0}(\iota)=1$ if
$\iota\in\mathsf{D}$. Note that the SCC that $\iota$ resides in can be an IWC,
a DAC or a NAC.

For a given level-labelling function $\mathfrak{g}_{\\_}{\ell}$, we will make
$\\{\,q\in\mathsf{D}\mid\mathfrak{g}_{\\_}{\ell}(q)\neq\infty\,\\}=S_{\\_}{\ell}\cap\mathsf{D}$
hold, i.e., tracing correctly the set of $\mathsf{D}$-states reached by
$\mathcal{A}$ at level $\ell$; we denote the set
$\mathfrak{g}_{\\_}{\ell}(\mathsf{D})\setminus\\{\infty\\}$ by
$\beta(\mathfrak{g}_{\\_}{\ell})$, so $\beta(\mathfrak{g}_{\\_}{\ell})$ is the
set of unique labelling numbers at level $\ell$. By the construction given
below about how to generate $\mathfrak{g}_{\\_}{\ell+1}$ from
$\mathfrak{g}_{\\_}{\ell}$ on reading ${w}[\ell]$, we ensure that
$\beta(\mathfrak{g}_{\\_}{\ell})\subseteq\\{1,\cdots,2\cdot|\mathsf{D}|\\}$
for all $\ell\in\mathbb{N}$.

We now present how to compute the successor level-labelling function
$\mathfrak{g}_{\\_}{\ell+1}$ of $\mathfrak{g}_{\\_}{\ell}$ on letter
${w}[\ell]$. The states reached by $\mathcal{A}$ at level $\ell+1$, i.e.,
$S_{\\_}{\ell+1}\cap\mathsf{D}$, may come from two sources: some state may
come from states not in $\mathsf{D}$ via transitions in
$\delta\setminus\delta_{D}$; some other via $\delta_{D}$ from states in
$S_{\\_}{\ell}\cap\mathsf{D}$. In order to generate
$\mathfrak{g}_{\\_}{\ell+1}$, we first compute an intermediate level-labelling
function $\mathfrak{g}^{\prime}_{\\_}{\ell+1}$ as follows.

  1. 1.

To obey Rule (2), for every state
$q^{\prime}\in\delta_{D}(S_{\\_}{\ell}\cap\mathsf{D},{w}[\ell])$, we set

$\mathfrak{g}^{\prime}_{\\_}{\ell+1}(q^{\prime})=\min\\{\,\mathfrak{g}_{\\_}{\ell}(q)\mid
q\in S_{\\_}{\ell}\cap\mathsf{D}\land\delta_{D}(q,{w}[\ell])=q^{\prime}\,\\}.$

That is, when two runs merge, we only keep the run with the lower labelling
number, i.e., the run entered in $\mathsf{D}$ earlier.

  2. 2.

To respect Rule (1), we set
$\mathfrak{g}^{\prime}_{\\_}{\ell+1}(q^{\prime})=|\mathsf{D}|+i$ for the
$i$-th newly entered state
$q^{\prime}\in(S_{\\_}{\ell+1}\cap\mathsf{D})\setminus\delta_{D}(S_{\\_}{\ell}\cap\mathsf{D},{w}[\ell])$
and the states $q^{\prime}$ are ordered by the total order $\preccurlyeq$ of
the states. Since every state in
$\delta_{D}(S_{\\_}{\ell}\cap\mathsf{D},{w}[\ell])$ is on a run that already
entered $\mathsf{D}$, its labelling has already been determined by the case 1.

It is easy to observe that in order to compute the transition relation between
two consecutive levels, we only need to know the labelling at the previous
level. More precisely, we do not have to know the exact labelling numbers,
since it suffices to know their relative order. Therefore, we can compress the
level-labelling $\mathfrak{g}^{\prime}_{\\_}{\ell+1}$ to
$\mathfrak{g}_{\\_}{\ell+1}$ as follows. Let
$\mathsf{ord}\colon\beta(\mathfrak{g}^{\prime}_{\\_}{\ell+1})\to\\{1,\cdots,|\beta(\mathfrak{g}^{\prime}_{\\_}{\ell+1})|\\}$
be the function that maps each labelling value in
$\beta(\mathfrak{g}^{\prime}_{\\_}{\ell+1})$ to its relative position once the
values in $\beta(\mathfrak{g}^{\prime}_{\\_}{\ell+1})$ have been sorted in
ascending order. For instance, if
$\beta(\mathfrak{g}^{\prime}_{\\_}{\ell+1})=\\{2,4,7\\}$, then
$\mathsf{ord}=\\{2\mapsto 1,4\mapsto 2,7\mapsto 3\\}$. Then we set
$\mathfrak{g}_{\\_}{\ell+1}(q)=\mathsf{ord}(\mathfrak{g}^{\prime}_{\\_}{\ell+1}(q))$
for each $q\in S_{\\_}{\ell+1}\cap\mathsf{D}$, and
$\mathfrak{g}_{\\_}{\ell+1}(q^{\prime})=\infty$ for each
$q^{\prime}\in\mathsf{D}\setminus S_{\\_}{\ell+1}$. In this way, all level-
labelling functions $\mathfrak{g}_{\\_}{\ell}$ we use are such that
$\beta(\mathfrak{g}_{\\_}{\ell})\subseteq\\{1,\cdots,|\mathsf{D}|\\}$.

The intuition behind the use of these level-labelling functions is that, if we
always see a labelling number $h$ in the intermediate level-labelling
$\mathfrak{g}^{\prime}_{\\_}{\ell}$ for all $\ell\geq k$ after some level $k$,
we know that there is a run that eventually stays in $\mathsf{D}$ and is
eventually always labelled with $h$. To check whether this run also visits
infinitely many accepting transitions, we will color every transition
$e=(\mathfrak{g}_{\\_}{\ell},{w}[\ell],\mathfrak{g}_{\\_}{\ell+1})$. To decide
what color to assign to $e$, we first identify which runs have merged with
others or got out of $\mathsf{D}$ (corresponding to _bad_ events and _odd_
colors) and which runs still continue to stay in $\mathsf{D}$ and take an
accepting transition (corresponding to _good_ events and _even_ colors).

The bad events correspond to the discontinuation of labelling values between
$\mathfrak{g}_{\\_}{\ell}$ and $\mathfrak{g}^{\prime}_{\\_}{\ell+1}$, defined
as
$\mathsf{B}(e)=\beta(\mathfrak{g}_{\\_}{\ell})\setminus\beta(\mathfrak{g}^{\prime}_{\\_}{\ell+1})$.
Intuitively, if a labelling value $k$ exists in the set $\mathsf{B}(e)$, then
the run $\rho$ associated with labelling $k$ merged with a run with lower
labelling value $k^{\prime}<k$, or $\rho$ left the DAC $\mathsf{D}$. The good
events correspond to the occurrence of accepting transitions in some runs,
whose labelling we collect into

$\mathsf{G}(e)=\\{\,k\in\beta(\mathfrak{g}_{\\_}{\ell})\mid\exists(q,{w}[\ell],q^{\prime})\in
F.\mathfrak{g}_{\\_}{\ell}(q)=\mathfrak{g}^{\prime}_{\\_}{\ell+1}(q^{\prime})=k\neq\infty\,\\}$.
In practice, a labelling value $k$ in $\mathsf{G}(e)$ indicates that we have
seen a run with labelling $k$ that visits an accepting transition. We then let
$\mathsf{B}(e)=\mathsf{B}(e)\cup\\{|\mathsf{D}|+1\\}$ and
$\mathsf{G}(e)=\mathsf{G}(e)\cup\\{|\mathsf{D}|+1\\}$ where the value
$|\mathsf{D}|+1$ is used to indicate that no bad (i.e., no run merged or left
the DAC) or no good (i.e., no run took an accepting transition) events
happened, respectively.

In order to declare a sequence of labelling functions as accepting, we want
the good events to happen infinitely often and bad events to happen only
finitely often, when the runs with bad events have a labelling number lower
than that of the runs with good events. So we assign the color
$c=\min\\{2\cdot\min\mathsf{B}(e)-1,2\cdot\min\mathsf{G}(e)\\}$ to the
transition $e$.

Since the labelling numbers are in $\\{1,\cdots,|\mathsf{D}|\\}$, we have that
$c\in\\{1,\cdots,2\cdot|\mathsf{D}|+1\\}$. The intuition why we assign colors
in this way is given as the proof idea of the following lemma.
lemmaDACAcceptingRunSize  (1) An accepting run of $\mathcal{A}$ over $w$
eventually stays in the DAC $\mathsf{D}$ if and only if the minimal color $c$
we receive infinitely often is even.  (2) The number of possible labelling
functions $\mathfrak{g}$ is at most $3\cdot|\mathsf{D}|!$.  The proof idea is
as follows: an accepting run $\rho$ on the word $w$ that stays in $\mathsf{D}$
will have stable labelling number, say $k\geq 1$, after some level since the
labelling value cannot increase by construction and is finite. So all runs on
$w$ that have labelling values lower than $k$ will not leave $\mathsf{D}$: if
they would leave or just merge with other runs, their labelling value
vanishes, so $\mathsf{ord}$ would decrease the value for $\rho$. This implies
that the color we receive afterwards infinitely often is either  1) an odd
color larger than $2k$, due to vanishing runs with value at least $k+1$ or
simply because no bad or good events occur, or  2) an even color at most $2k$,
depending on whether there is some run with value smaller than $\rho$ also
taking accepting transitions.  Thus the minimum color occurring infinitely
often is even. The number of labelling functions $\mathfrak{g}$ is bounded by
$\sum_{\\_}{i=0}^{|\mathsf{D}|}\binom{|\mathsf{D}|}{i}\cdot i!\leq
3\cdot|\mathsf{D}|!$. We refer to Appendix 0.A.2 for the detailed proof of
Lemma 3.2.

The fragment of the DAG $\mathcal{G}_{\mathcal{A},a^{\omega}}$ shown on the
right is relative to the only DAC $\mathsf{D}=\\{q_{\\_}{4},q_{\\_}{5}\\}$.
The value of $\mathfrak{g}^{\prime}_{\\_}{\ell}(q)$,
$\mathfrak{g}_{\\_}{\ell}(q)$ and the corresponding $\mathsf{ord}$ is given by
the mapping near each state $q$; as a concrete application of the construction
given above, consider how to get $\mathfrak{g}_{\\_}{4}$ from
$\mathfrak{g}_{\\_}{3}$, defined as $\mathfrak{g}_{\\_}{3}(q_{\\_}{4})=1$ and
$\mathfrak{g}_{\\_}{3}(q_{\\_}{5})=\infty$: since
$q_{\\_}{5}\in\delta_{D}(S_{\\_}{3}\cap\mathsf{D},a)$, according to case 1 we
define $\mathfrak{g}^{\prime}_{\\_}{4}(q_{\\_}{5})=1$ because
$q_{\\_}{5}=\delta_{D}(q_{\\_}{4},a)$ and
$\mathfrak{g}_{\\_}{3}(q_{\\_}{4})=1$; since
$q_{\\_}{4}\in(S_{\\_}{4}\cap\mathsf{D})\setminus\delta_{D}(S_{\\_}{3}\cap\mathsf{D},a)$,
then case 2 applies, so $\mathfrak{g}^{\prime}_{\\_}{4}(q_{\\_}{4})=3$. The
function $\mathsf{ord}$ is $\mathsf{ord}=[1\mapsto 1,3\mapsto 2]$, thus we get
$\mathfrak{g}_{\\_}{4}(q_{\\_}{4})=2$ and
$\mathfrak{g}_{\\_}{4}(q_{\\_}{5})=1$. As bad/good sets for the transition
$e=\mathfrak{g}_{\\_}{3}\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptstyle
a$\cr\kern 1.29167pt\cr$\longrightarrow$\cr}}}\mathfrak{g}_{\\_}{4}$, we have
$\mathsf{B}(e)=\emptyset\cup\\{3\\}$ while $\mathsf{G}(e)=\\{1\\}\cup\\{3\\}$,
so the resulting color is $2$.

Again, we make the above computation of successors available as a function
$\mathsf{detSucc}$, which takes as input the DAC $\mathsf{D}$, a labelling
$\mathfrak{g}$ and a letter $a$, and returns the successor labelling
$\mathfrak{g}^{\prime}$ and the color
$c\in\\{1,\cdots,2\cdot|\mathsf{D}|+1\\}$.

###  3.3 Successor Computation inside NACs

The computation of the successor inside a NAC is more involved since runs can
branch, so it is more difficult to check whether there exists an accepting
run. To identify accepting runs, researchers usually follow the Safra-
Piterman’s idea [35, 32] to give the runs that take more accepting transitions
the precedence over other runs that join them. We now present how to compute
labelling functions encoding this idea for NACs, instead of the whole NBA.
Differently to the previous case about DACs, the labelling functions we use
here use lists of numbers, instead of single numbers, to keep track of the
branching, merging and new incoming runs. This can be seen as a generalization
of the numbered brackets used in [34] to represent ordinary Safra-Piterman’s
trees. Differently from this construction, in our setting the main challenge
we have to consider is how to manage correctly the newly entering runs, which
are simply not occurring in [34] since there the whole NBA is considered. The
fact that runs can merge, instead, is a common aspect, while the fact that a
run $\rho$ leaves the current NAC can be treated similarly to dying out runs
in [34]. Below we assume that $\mathsf{N}$ is a given NAC; we denote by
$\delta_{N}=(\mathsf{N}\times\Sigma\times\mathsf{N})\cap\delta$ the transition
function $\delta$ inside $\mathsf{N}$.

To manage the branching and merging of runs of $\mathcal{A}$ over $w$ inside a
NAC, and to keep track of the accepting transitions taken so far, we use
level-labelling functions as for the DAC case. For a given NAC $\mathsf{N}$,
the functions we use have lists of natural numbers as codomain; more
precisely, let $\mathcal{L}_{\mathsf{N}}$ be the set of lists taking value in
the set $\\{1,\cdots,2\cdot|\mathsf{N}|\\}$, where a list is a finite sequence
of values in ascending order. Given two lists $[v_{\\_}{1},\cdots,v_{\\_}{k}]$
and $[v^{\prime}_{\\_}{1},\cdots,v^{\prime}_{\\_}{k^{\prime}}]$, we say that
$[v_{\\_}{1},\cdots,v_{\\_}{k}]$ is a prefix of
$[v^{\prime}_{\\_}{1},\cdots,v^{\prime}_{\\_}{k^{\prime}}]$ if $1\leq k\leq
k^{\prime}$ and for each $1\leq j\leq k$, we have
$v_{\\_}{j}=v^{\prime}_{\\_}{j}$. Note that the empty list _is not_ a prefix
of any list. Given two lists $[v_{\\_}{1},\cdots,v_{\\_}{k}]$ and
$[v^{\prime}_{\\_}{1},\cdots,v^{\prime}_{\\_}{k^{\prime}}]$, we denote by
$[v_{\\_}{1},\cdots,v_{\\_}{k}]{\smallfrown}[v^{\prime}_{\\_}{1},\cdots,v^{\prime}_{\\_}{k^{\prime}}]$
their concatenation, that is the list
$[v_{\\_}{1},\cdots,v_{\\_}{k},v^{\prime}_{\\_}{1},\cdots,v^{\prime}_{\\_}{k^{\prime}}]$.
Moreover, we define a total order on lists as follows: given two lists
$[v_{\\_}{1},\cdots,v_{\\_}{k}]$ and
$[v^{\prime}_{\\_}{1},\cdots,v^{\prime}_{\\_}{k^{\prime}}]$, we order them by
padding the shorter of the two with $\infty$ in the rear, so to make them of
the same length, and then by comparing them by the usual lexicographic order.
This means, for instance, that the empty list $[]$ is the largest list and
that $[1,3,5]$ is smaller than $[1,3]$ but larger than $[1,2]$. The lists help
to keep track of the branching history from their prefixes, such as $[1,2]$ is
branched from $[1]$.

As done for DACs, we use a level-labelling function
$\mathfrak{t}_{\\_}{\ell}\colon\mathsf{N}\to\mathcal{L}_{\mathsf{N}}$ to
encode the set of $\mathsf{N}$-states reached in the run DAG
$\mathcal{G}_{\mathcal{A},w}$ at level $\ell$. We denote by
$\beta(\mathfrak{t}_{\\_}{\ell})$ the set of non-empty lists in the image of
$\mathfrak{t}_{\\_}{\ell}$, that is,
$\beta(\mathfrak{t}_{\\_}{\ell})=\\{\,\mathfrak{t}_{\\_}{\ell}(q)\mid
q\in\mathsf{N}\land\mathfrak{t}_{\\_}{\ell}(q)\neq[]\,\\}$. We use the empty
list $[]$ for the states in $\mathsf{N}$ that do not occur in the vertexes of
$\mathcal{G}_{\mathcal{A},w}$ at level $\ell$, so
$\beta(\mathfrak{t}_{\\_}{\ell})$ contains only lists associated with states
that $\mathcal{A}$ is currently located at. Similarly to the other types of
SCCs, at level $0$, we set $\mathfrak{t}_{\\_}{0}(\iota)=[1]$ if
$\iota\in\mathsf{N}$, and $\mathfrak{t}_{\\_}{0}(q)=[]$ for each state
$q\in\mathsf{N}\setminus\\{\iota\\}$.

To define the transition from $\mathfrak{t}_{\\_}{\ell}$ to
$\mathfrak{t}_{\\_}{\ell+1}$ through the letter ${w}[\ell]$, we use again an
intermediate level-labelling function $\mathfrak{t}^{\prime}_{\\_}{\ell+1}$
that we construct step by step as follows. We start with
$\mathfrak{t}^{\prime}_{\\_}{\ell+1}(q)=[]$ for each $q\in\mathsf{N}$ and with
the set of unused numbers $U=\\{\,u\geq 1\mid
u\notin\beta(\mathfrak{t}_{\\_}{\ell})\,\\}$, i.e., the numbers not used in
$\beta(\mathfrak{t}_{\\_}{\ell})$.

  1. 1.

For every state
$q^{\prime}\in\delta_{N}(S_{\\_}{\ell}\cap\mathsf{N},{w}[\ell])$, let
$P_{\\_}{q^{\prime}}=\\{\,q\in
S_{\\_}{\ell}\cap\mathsf{N}\mid(q,{w}[\ell],q^{\prime})\in\delta_{N}\,\\}$ be
the set of currently reached predecessors of $q^{\prime}$, and
$C_{\\_}{q^{\prime}}=\emptyset$. For each $q\in P_{\\_}{q^{\prime}}$, if
$(q,{w}[\ell],q^{\prime})\in F$, then we add
$\mathfrak{t}_{\\_}{\ell}(q){\smallfrown}[u]$ to $C_{\\_}{q^{\prime}}$, where
$u=\min U$, and we remove $u$ from $U$, so that each number in $U$ is used
only once; otherwise, for $(q,{w}[\ell],q^{\prime})\in\delta_{N}\setminus F$,
we add $\mathfrak{t}_{\\_}{\ell}(q)$ to $C_{\\_}{q^{\prime}}$. Lastly, we set
$\mathfrak{t}^{\prime}_{\\_}{\ell+1}(q^{\prime})=\min C_{\\_}{q^{\prime}}$,
where the minimum is taken according to the list order.

Intuitively, if a run $\rho$ can branch into two kinds of runs, some via
accepting transitions and some others via nonaccepting transitions at level
$\ell+1$, then we let those from nonaccepting transitions inherit the
labelling from $\rho$, i.e., $\mathfrak{t}_{\\_}{\ell}({\rho}[\ell])$; for the
runs taking accepting transitions we create a new labelling
$\mathfrak{t}_{\\_}{\ell}({\rho}[\ell]){\smallfrown}[u]$. In this way, the
latter get precedence over the former. Moreover, if a run $\rho$ has received
multiple labelling values, collected in $C_{\\_}{{\rho}[\ell+1]}$, then it
will keep the smallest one, by
$\mathfrak{t}^{\prime}_{\\_}{\ell+1}({\rho}[\ell+1])=\min
C_{\\_}{{\rho}[\ell+1]}$.

  2. 2.

For each state
$q^{\prime}\in(S_{\\_}{\ell+1}\cap\mathsf{N})\setminus\delta_{N}(S_{\\_}{\ell}\cap\mathsf{N},{w}[\ell])$
taken according to the state order $\preccurlyeq$, we first set
$\mathfrak{t}^{\prime}_{\\_}{\ell+1}(q^{\prime})=[u]$, where $u=\min U$, and
then we remove $u$ from $U$, so we do not reuse the same values. That is, we
give the newly entered runs lower precedence than those already in
$\mathsf{N}$, by means of the larger list $[u]$.

We now need to prune the lists in $\beta(\mathfrak{t}^{\prime}_{\\_}{\ell+1})$
and recognize good and bad events. Similarly to DACs, a bad event means that a
run has left $\mathsf{N}$ or has been merged with runs with smaller labelling,
which is indicated by a discontinuation of a labelling between
$\beta(\mathfrak{t}_{\\_}{\ell})$ and
$\beta(\mathfrak{t}^{\prime}_{\\_}{\ell+1})$. For the transition
$e=(\mathfrak{t}_{\\_}{\ell},{w}[\ell],\mathfrak{t}_{\\_}{\ell+1})$ we are
constructing, to recognize bad events, we put into the set $\mathsf{B}(e)$ the
number $|\mathsf{N}|+1$ and all numbers in $\beta(\mathfrak{t}_{\\_}{\ell})$
that have disappeared in $\beta(\mathfrak{t}^{\prime}_{\\_}{\ell+1})$, that
is, $\mathsf{B}(e)=\\{|\mathsf{N}|+1\\}\cup\\{\,v\in\mathbb{N}\mid\text{$v$
occurs in $\beta(\mathfrak{t}_{\\_}{\ell})$ but not in
$\beta(\mathfrak{t}^{\prime}_{\\_}{\ell+1})$}\,\\}$.

Differently from the good events for DACs, which require to visit an accepting
transition, we need all runs branched from a run to visit an accepting
transition, which is indicated by the fact that there are no states labelled
by $\mathfrak{t}^{\prime}_{\\_}{\ell+1}$ with some list
$l\in\beta(\mathfrak{t}_{\\_}{\ell})$ but there are extensions of $l$
associated with some state. To recognize good events, let
$\mathsf{G}(e)=\\{|\mathsf{N}|+1\\}$ and
$\mathfrak{t}^{\prime\prime}_{\\_}{\ell+1}$ be another intermediate labelling
function. For each $q^{\prime}\in S_{\\_}{\ell+1}\cap\mathsf{N}$, consider the
list $\mathfrak{t}^{\prime}_{\\_}{\ell+1}(q^{\prime})$: if for each prefix
$[v_{\\_}{1},\cdots v_{\\_}{k}]$ of
$\mathfrak{t}^{\prime}_{\\_}{\ell+1}(q^{\prime})$ we have $[v_{\\_}{1},\cdots
v_{\\_}{k}]\in\beta(\mathfrak{t}^{\prime}_{\\_}{\ell+1})$, then we set
$\mathfrak{t}^{\prime\prime}_{\\_}{\ell+1}(q^{\prime})=\mathfrak{t}^{\prime}_{\\_}{\ell+1}(q^{\prime})$.
Otherwise, let $[v_{\\_}{1},\cdots
v_{\\_}{\bar{k}}]\notin\beta(\mathfrak{t}^{\prime}_{\\_}{\ell+1})$ be the
shortest prefix of $\mathfrak{t}^{\prime}_{\\_}{\ell+1}(q^{\prime})$ not in
$\beta(\mathfrak{t}^{\prime}_{\\_}{\ell+1})$; we set
$\mathfrak{t}^{\prime\prime}_{\\_}{\ell+1}(q^{\prime})=[v_{\\_}{1},\cdots
v_{\\_}{\bar{k}}]$ and add $v_{\\_}{\bar{k}}$ to $\mathsf{G}(e)$. Setting
$\mathfrak{t}^{\prime\prime}_{\\_}{\ell+1}(q^{\prime})=[v_{\\_}{1},\cdots
v_{\\_}{\bar{k}}]$ in fact corresponds, in the Safra’s construction [35], to
the removal of all children of a node $\mathfrak{N}$ for which the union of
the states in the children is equal to the states in $\mathfrak{N}$. Lastly,
similarly to the DAC case, we set
$\mathfrak{t}_{\\_}{\ell+1}(q)=\mathsf{ord}(\mathfrak{t}^{\prime\prime}_{\\_}{\ell+1}(q))$
for each $q\in S_{\\_}{\ell+1}\cap\mathsf{N}$ and
$\mathfrak{t}_{\\_}{\ell+1}(q^{\prime})=[]$ for each
$q^{\prime}\in\mathsf{N}\setminus S_{\\_}{\ell+1}$, where
$\mathsf{ord}([v_{\\_}{1},\cdots,v_{\\_}{k}])=[\mathsf{ord}(v_{\\_}{1}),\cdots,\mathsf{ord}(v_{\\_}{k})]$.
Regarding the color to assign to the transition $e$, we just assign the color
$c=\min\\{2\cdot\min\mathsf{G}(e),2\cdot\min\mathsf{B}(e)-1\\}$.

lemmanacAccCond  (1) An accepting run of $\mathcal{A}$ over $w$ eventually
stays in the NAC $\mathsf{N}$ if and only if the minimal color $c$ we receive
infinitely often is even.  (2) The number of possible labelling functions
$\mathfrak{t}$ is at most $2\cdot(|\mathsf{N}|!)^{2}$.

Similarly to DACs, also for NACs we have handled each NAC independently. The
reason for this is that this potentially reduces the complexity of the single
cases: assume that we have two NACs $\mathsf{N}_{\\_}{1}$ and
$\mathsf{N}_{\\_}{2}$. If we apply the Safra-Piterman’s construction directly
to $\mathsf{N}_{\\_}{1}\cup\mathsf{N}_{\\_}{2}$, we might incur in the worst-
case complexity $2\cdot((|\mathsf{N}_{\\_}{1}|+|\mathsf{N}_{\\_}{2}|)!)^{2}$,
as mentioned in the introduction. However, if we determinize them separately,
then the worst complexity for each NAC $\mathsf{N}_{\\_}{i}$ is
$2\cdot(\mathsf{N}_{\\_}{i}!)^{2}$, for an overall
$4\cdot(|\mathsf{N}_{\\_}{1}|!\cdot|\mathsf{N}_{\\_}{2}|!)^{2}$, much smaller
than $2\cdot((|\mathsf{N}_{\\_}{1}|+|\mathsf{N}_{\\_}{2}|)!)^{2}$.

As usual, we make the above construction available as a function
$\mathsf{nondetSucc}$, which takes as input the NAC $\mathsf{N}$, a labelling
$\mathfrak{t}$ and a letter $a$, and returns the successor labelling
$\mathfrak{t}^{\prime}$ and the corresponding color
$c\in\\{1,\cdots,2\cdot|\mathsf{N}|+1\\}$.

Similarly to the constructions for other SCCs, we show on the right the
fragment of run DAG $\mathcal{G}_{\mathcal{A},a^{\omega}}$ for the NAC
$\mathsf{N}=\\{q_{\\_}{0},q_{\\_}{1}\\}$, with $q_{\\_}{0}\preccurlyeq
q_{\\_}{1}$. The construction of $\mathfrak{t}_{\\_}{1}$ is easy, so consider
its $a$-successor $\mathfrak{t}_{\\_}{2}$: we start with $U=\\{3,4,\cdots\\}$;
for $q_{\\_}{0}$, we have $P_{\\_}{q_{\\_}{0}}=\\{q_{\\_}{0},q_{\\_}{1}\\}$
and $C_{\\_}{q_{\\_}{0}}=\\{[1,2,3],[1]\\}$, hence
$\mathfrak{t}^{\prime}_{\\_}{2}(q_{\\_}{0})=[1,2,3]$. For $q_{\\_}{1}$, we get
$P_{\\_}{q_{\\_}{1}}=\\{q_{\\_}{0}\\}$ and $C_{\\_}{q_{\\_}{1}}=\\{[1,2]\\}$,
so $\mathfrak{t}^{\prime}_{\\_}{2}(q_{\\_}{1})=[1,2]$. Thus, for
$e=(\mathfrak{t}_{\\_}{1},{w}[1],\mathfrak{t}_{\\_}{2})$, we have
$\mathsf{B}(e)=\\{3\\}$ while $\mathsf{G}(e)=\\{1,3\\}$, since both lists in
$\beta(\mathfrak{t}^{\prime}_{\\_}{2})=\\{[1,2],[1,2,3]\\}$ are missing the
prefix $[1]$, so we get
$\mathfrak{t}_{\\_}{2}(q_{\\_}{0})=\mathfrak{t}_{\\_}{2}(q_{\\_}{1})=[1]$ and
color $c=2$.

##  4 Determinization of NBAs to DELAs

In this section, we fix an NBA $\mathcal{A}=(Q,\iota,\delta,F)$ with $n=|Q|$
states and we show how to construct an equivalent DELA
$\mathcal{A}^{\mathsf{E}}=(Q^{\mathsf{E}},\iota^{\mathsf{E}},\delta^{\mathsf{E}},\Gamma^{\mathsf{E}},\mathsf{p}^{\mathsf{E}},\mathsf{Acc}^{\mathsf{E}})$,
by using the algorithms developed in the previous section. We assume that
$\mathcal{A}$ has $\\{\mathsf{D}^{1},\cdots,\mathsf{D}^{d}\\}$ as set of DACs
and $\\{\mathsf{N}^{1},\cdots,\mathsf{N}^{k}\\}$ as set of NACs.

When computing the successor for each type of SCCs while reading a word $w$,
we just need to know the set $S_{\\_}{\ell}$ of states reached at the current
level $\ell$ and the letter $a\in\Sigma$ to read. We can ignore the actual
level $\ell$, since if $S_{\\_}{\ell}=S_{\\_}{\ell^{\prime}}$, then their
successors under the same letter will be the same. As mentioned before, every
state of $\mathcal{A}^{\mathsf{E}}$ corresponds to a level of
$\mathcal{G}_{\mathcal{A},w}$. We call a state of $\mathcal{A}^{\mathsf{E}}$ a
_macrostate_ and a run of $\mathcal{A}^{\mathsf{E}}$ a _macrorun_ , to
distinguish them from those of $\mathcal{A}$.

##### Macrostates $Q^{\mathsf{E}}$.

Each macrostate consists of the pair $(P,O)$ for encoding the states in IWCs,
a labelling function
$\mathfrak{g}^{i}\colon\mathsf{D}^{i}\to\\{1,\cdots,|\mathsf{D}^{i}|\\}\cup\\{\infty\\}$
for the states of each DAC $\mathsf{D}^{i}$ and a labelling function
$\mathfrak{t}^{j}\colon\mathsf{N}^{j}\to\mathcal{L}_{\mathsf{N}^{j}}$ for each
NAC $\mathsf{N}^{j}$, without the explicit level number. The initial
macrostate $\iota^{\mathsf{E}}$ of $\mathcal{A}^{\mathsf{E}}$ is the encoding
of level $0$, defined as the set
$\\{(P_{\\_}{0},O_{\\_}{0})\\}\cup\\{\,\mathfrak{g}^{i}_{\\_}{0}\mid\text{$\mathsf{D}^{i}$
is a DAC}\,\\}\cup\\{\,\mathfrak{t}^{j}_{\\_}{0}\mid\text{$\mathsf{N}^{j}$ is
a NAC}\,\\}$, where each encoding for the different types of SCCs is the one
for level $0$.

We note that $\iota$ must be present in one type of SCCs. In particular, if
$\iota$ is a transient state, then $\\{\iota\\}$ is classified as an IWC.

##### Transition function $\delta^{\mathsf{E}}$.

Let $m$ be the current macrostate in $Q^{\mathsf{E}}$ and $a\in\Sigma$ be the
letter to read. Then we define $m^{\prime}=\delta^{\mathsf{E}}(m,a)$ as
follows.

  1. (i)

For $(P_{\\_}{m},O_{\\_}{m})\in m$, we set
$(P_{\\_}{m^{\prime}},O_{\\_}{m^{\prime}})=\mathsf{weakSucc}((P_{\\_}{m},O_{\\_}{m}),a)$
in $m^{\prime}$.

  2. (ii)

For $\mathfrak{g}^{i}_{\\_}{m}\in m$ relative to the DAC $\mathsf{D}^{i}$, we
set
$\mathfrak{g}^{i}_{\\_}{m^{\prime}}=\mathsf{detSucc}(\mathsf{D}^{i},\mathfrak{g}^{i}_{\\_}{m},a)$
in $m^{\prime}$.

  3. (iii)

For $\mathfrak{t}^{j}_{\\_}{m}\in m$ from the NAC $\mathsf{N}^{j}$, we set
$\mathfrak{t}^{j}_{\\_}{m^{\prime}}=\mathsf{nondetSucc}(\mathsf{N}^{j},\mathfrak{t}^{j}_{\\_}{m},a)$
in $m^{\prime}$.

Note that the set $S$ of the current states of $\mathcal{A}$ used by the
different successor functions is implicitly given by the sets $P$,
$\\{\,q\in\mathsf{D}^{i}\mid\mathfrak{g}^{i}(q)\neq\infty\,\\}$ for each DAC
$\mathsf{D}^{i}$ and
$\\{\,q\in\mathsf{N}^{j}\mid\mathfrak{t}^{j}(q)\neq[]\,\\}$ for each NAC
$\mathsf{N}^{j}$ in the current macrostate $m$.

##### Color set $\Gamma^{\mathsf{E}}$ and coloring function
$\mathsf{p}^{\mathsf{E}}$.

From the constructions given in Section 3, we have two colors from the IWCs,
$2\cdot|\mathsf{D}^{i}|+1$ colors for each DAC $\mathsf{D}^{i}$, and
$2\cdot|\mathsf{N}^{j}|+1$ colors for each NAC $\mathsf{N}^{j}$, yielding a
total of at most $3\cdot|Q|$ colors. Thus we set
$\Gamma^{\mathsf{E}}=\\{0,1,\cdots,3\cdot|Q|\\}$ with color $0$ not being
actually used.

Regarding the color to assign to each transition, we need to ensure that the
colors returned by the single SCCs are treated separately, so we transpose
them. For a transition $e=(m,a,m^{\prime})\in\delta^{\mathsf{E}}$, we define
the coloring function $\mathsf{p}^{\mathsf{E}}$ as follows.

  * •

If we receive color $1$ for the transition
$((P_{\\_}{m},O_{\\_}{m}),a,(P_{\\_}{m^{\prime}},O_{\\_}{m^{\prime}}))$, then
we put $1\in\mathsf{p}^{\mathsf{E}}(e)$. Intuitively, every time we see an
empty $O$-set along reading an $\omega$-word $w$ in the IWCs, we put the color
$1$ on the transition $(m,a,m^{\prime})$.

  * •

For each DAC $\mathsf{D}^{i}$, we transpose its colors after the colors for
the IWCs and the other DACs with smaller index. So we set the base number for
the colors of the DAC $\mathsf{D}^{i}$ to be
$\mathsf{b}_{\\_}{i}=2+\sum_{\\_}{1\leq h<i}(2\cdot|\mathsf{D}^{h}|+1)$, i.e.,
the number of colors already being used. Then, if we receive the color $c$ for
the transition
$(\mathfrak{g}^{i}_{\\_}{m},a,\mathfrak{g}^{i}_{\\_}{m^{\prime}})$ from
$\mathsf{detSucc}$, we put
$c+\mathsf{b}_{\\_}{i}\in\mathsf{p}^{\mathsf{E}}(e)$.

  * •

We follow the same approach for the NAC $\mathsf{N}^{j}$: we set its base
number to be $\mathsf{b}_{\\_}{j}=2+\sum_{\\_}{1\leq h\leq
d}(2\cdot|\mathsf{D}^{h}|+1)+\sum_{\\_}{1\leq h<j}(2\cdot|\mathsf{N}^{h}|+1)$.
Then, if we receive the color $c$ for the transition
$(\mathfrak{t}^{j}_{\\_}{m},a,\mathfrak{t}^{j}_{\\_}{m^{\prime}})$ from
$\mathsf{nondetSucc}$, we put
$c+\mathsf{b}_{\\_}{j}\in\mathsf{p}^{\mathsf{E}}(e)$.

Intuitively, we make the colors returned for each SCC not overlap with those
of other SCCs without changing their relative order. In this way, we can still
independently check whether there exists an accepting run staying in an SCC.

##### Acceptance formula $\mathsf{Acc}^{\mathsf{E}}$.

We now define the acceptance $\mathsf{Acc}^{\mathsf{E}}$, which is basically
the _disjunction_ of the acceptance formula for each different types of SCCs,
after transposing them. Regarding the IWCs, we trivially define
$\mathsf{Acc}^{\mathsf{E}}_{\\_}{\mathsf{W}}=\mathsf{Fin}(1)$, since this is
the acceptance formula for IWCs; as said before, color $0$ is not used.

For DACs and NACs, the definition is more involved. For instance, regarding
the DAC $\mathsf{D}^{i}$, we know that all returned colors are inside
$\\{1,\cdots,2\cdot|\mathsf{D}^{i}|+1\\}$. According to Lemma 3.2, an
accepting run eventually stays in $\mathsf{D}^{i}$ if and only if the minimum
color that we receive infinitely often is even. Thus, the acceptance formula
for the above lemma is
$\mathsf{parity}(|\mathsf{D}^{i}|)=\bigvee_{\\_}{c=1}^{|\mathsf{D}^{i}|}(\bigwedge_{\\_}{j=1}^{c}\mathsf{Fin}(2j-1)\land\mathsf{Inf}(2c))$.
Let $\mathsf{b}_{\\_}{i}=2+\sum_{\\_}{h<i}(2\cdot|\mathsf{D}_{\\_}{h}|+1)$ be
the base number for the colors of $\mathsf{D}^{i}$, which is also the number
of colors already used by IWCs and the DACs $\mathsf{D}^{h}$ with $h<i$. Since
we have added the base number $\mathsf{b}^{i}$ to every color of
$\mathsf{D}^{i}$, we then have the acceptance formula
$\mathsf{Acc}^{\mathsf{E}}_{\\_}{\mathsf{D}^{i}}=\bigvee_{\\_}{c=1}^{|\mathsf{D}^{i}|}(\bigwedge_{\\_}{j=1}^{c}\mathsf{Fin}(2j-1+\mathsf{b}_{\\_}{i})\land\mathsf{Inf}(2c+\mathsf{b}_{\\_}{i}))$.

For each NAC $\mathsf{N}^{j}$, the colors we receive are in
$\\{1,\cdots,2\cdot|\mathsf{N}^{j}|+1\\}$. Let
$\mathsf{b}_{\\_}{j}=2+\sum_{\\_}{1\leq h\leq
d}(2\cdot|\mathsf{D}^{h}|+1)+\sum_{\\_}{h<j}(2\cdot|\mathsf{N}^{j}|+1)$ be the
base number for $\mathsf{N}^{j}$. Similarly to the DAC case, for each NAC
$\mathsf{N}^{j}$, we let
$\mathsf{Acc}^{\mathsf{E}}_{\\_}{\mathsf{N}^{j}}=\bigvee_{\\_}{c=1}^{|\mathsf{N}^{j}|}(\bigwedge_{\\_}{i=1}^{c}\mathsf{Fin}(2i-1+\mathsf{b}_{\\_}{j})\land\mathsf{Inf}(2c+\mathsf{b}_{\\_}{j}))$.

The acceptance formula for $\mathcal{A}^{\mathsf{E}}$ is
$\mathsf{Acc}^{\mathsf{E}}=\mathsf{Acc}^{\mathsf{E}}_{\\_}{\mathsf{W}}\lor\bigvee_{\\_}{i=1}^{d}\mathsf{Acc}^{\mathsf{E}}_{\\_}{\mathsf{D}^{i}}\lor\bigvee_{\\_}{j=1}^{k}\mathsf{Acc}^{\mathsf{E}}_{\\_}{\mathsf{N}^{j}}$.

Consider again the NBA $\mathcal{A}$ given in Figure 1 and its various SCCs.
As acceptance formula for the constructed DELA, it is the disjunction of the
formulas $\mathsf{Acc}^{\mathsf{E}}_{\\_}{\mathsf{W}}=\mathsf{Fin}(1)$;
$\mathsf{Acc}^{\mathsf{E}}_{\\_}{\mathsf{D}}=\bigvee_{\\_}{c=1}^{2}(\bigwedge_{\\_}{j=1}^{c}\mathsf{Fin}(2j-1+2)\land\mathsf{Inf}(2c+2))$,
since the base number for $\mathsf{D}$ is $2$; and
$\mathsf{Acc}^{\mathsf{E}}_{\\_}{\mathsf{N}}=\bigvee_{\\_}{c=1}^{2}(\bigwedge_{\\_}{i=1}^{c}\mathsf{Fin}(2i-1+7)\land\mathsf{Inf}(2c+7))$,
since $7$ is the base number for $\mathsf{N}$.

The construction given in this section is correct, as stated by Theorem 4.

theoremLDBAlanguageSizeParityAutomaton Given an NBA $\mathcal{A}$ with $n=|Q|$
states, let $\mathcal{A}^{\mathsf{E}}$ be the DELA constructed by our method.
Then  (1) $\mathsf{L}(\mathcal{A}^{\mathsf{E}})=\mathsf{L}(\mathcal{A})$and
(2) $\mathcal{A}^{\mathsf{E}}$has at most
$3^{|\mathsf{W}|}\cdot\Big{(}\prod_{\\_}{i=1}^{d}3\cdot|\mathsf{D}^{i}|!\Big{)}\cdot\Big{(}\prod_{\\_}{j=1}^{k}2\cdot(|\mathsf{N}^{i}|!)^{2}\Big{)}$
macrostates and $3n+1$ colors.

Obviously, if $d=k=0$, $\mathcal{A}$ is a weak BA [31]. If $k=0$,
$\mathcal{A}$ is an elevator BA, a new class of BAs recently introduced in
[19] which have only IWCs and DACs, a strict superset of semi-deterministic
BAs (SDBAs) [10]. SDBAs will behave _deterministically_ after seeing
acceptance transitions. An elevator BA that is not an SDBA can be obtained
from the NBA $\mathcal{A}$ shown in Figure 1 by setting $q_{\\_}{2}$ as
initial state and by removing all states and transitions relative to the NAC.

It is known that the lower bound for determinizing SDBAs is $n!$ [14, 26].
Then the determinization complexity of weak BAs and elevator BAs can be easily
improved exponentially as follows. corollaryworstCaseDeterminizationSubclass
(1) Given a weak Büchi automaton $\mathcal{A}$ with $n=|Q|$ states, the DELA
constructed by our algorithm has at most $3^{n}$ macrostates.  (2) Given an
elevator Büchi automaton $\mathcal{A}$ with $n=|Q|$ states, our algorithm
constructs a DELA with $\mathsf{\Theta}(n!)$ macrostates; it is asymptotically
optimal.  The upper bound for determinizing weak BAs is already known [5].
Elevator BAs are, to the best of our knowledge, the _largest_ subclass of NBAs
known so far to have determinization complexity $\mathsf{\Theta}(n!)$.

The acceptance formula for an SCC can be seen as a parity acceptance formula
with colors being shifted to different ranges. A parity automaton can be
converted into a Rabin one without blow-up of states and transitions [16].
Since $\mathsf{Acc}^{\mathsf{E}}$ is a disjunction of parity acceptance
formulas, Theorem 4 then follows. theoremDELAtoDRA Let
$\mathcal{A}^{\mathsf{E}}$ be the constructed DELA for the given NBA
$\mathcal{A}$. Then $\mathcal{A}^{\mathsf{E}}$ can be converted into a DRA
$\mathcal{A}^{\mathsf{R}}$ without blow-up of states and transitions.

##### Translation to deterministic Parity automata (DPAs).

We note that there is an _optimal_ translation from a DRA to a DPA described
in[7], implemented in Spot via the function $\mathsf{acd\\_transform}$ [8].

##  5 Empirical Evaluation

To analyze the effectiveness of our Divide-and-Conquer determinization
construction proposed in Section 3, we implemented it in our tool COLA, which
is built on top of Spot [12]. The source code of COLA is publicly available
from https://github.com/liyong31/COLA. We compared COLA with the official
versions of Spot [12] (2.10.2) and Owl [23] (21.0). Spot implements the
algorithm described in [34], a variant of [32] for transition-based NBAs,
while Owl implements the algorithms described in [27, 28], both constructing
DPAs as result. To make the comparison fair, we let all tools generate DPAs,
so we used the command autfilt --deterministic --parity=min\ even -F file.hoa
to call Spot and owl nbadet -i file.hoa to call Owl. Recall that we use the
function $\mathsf{acd\\_transform}$ [8] from Spot for obtaining DPAs from our
DRAs. The tools above also implement optimizations for reducing the size of
the output DPA, like simulation and state merging [28], or stutter invariance
[22] (except for Owl); we use the default settings for all tools. We performed
our experiments on a desktop machine equipped with 16GB of RAM and a 3.6 GHz
Intel Core i7-4790 CPU. We used BenchExec 111https://github.com/sosy-
lab/benchexec/ [3] to trace and constrain the tools’ executions: we allowed
each execution to use a single core and 12 GB of memory, and imposed a timeout
of 10 minutes. We used Spot to verify the results generated by three tools and
found only outputs equivalent to the inputs.

As benchmarks, we considered all NBAs in the HOA format [1] available in the
automata-benchmarks repository222https://github.com/ondrik/automata-
benchmarks/. We have pre-filtered them with autfilt to exclude all
deterministic cases and to have nondeterministic BAs, obtaining in total
15,913 automata coming from different sources in literature.

Figure 2: The cactus plot for the determinization of NBAs from automata-
benchmarks.

In Figure 2 we show a cactus plot reporting how many input automata have been
determinized by each tool, over time. As we can see, COLA works better than
Spot, with COLA solving in total $15,903$ cases and Spot $15,862$ cases, with
Owl solving in total $15,749$ cases and taking more time to solve as many
instances as COLA and Spot. From the plot given in Figure 2 we see that COLA
is already very competitive with respect to its performance.

Figure 3: States comparison for the determinization of NBAs from automata-
benchmarks.

In Figure 3 we show the number of states of the generated DPAs. In the plot we
indicate with the bold dashed line the maximum number of states of the
automata produced by either of the two tools, and we place a mark on the upper
or right border of the plot to indicate that one tool has generated an
automaton with that size while the other tool just failed. The color of each
mark represents how many instances have been mapped to the corresponding
point. As the plots show, Spot and COLA generate automata with similar size,
with COLA being more likely to generate smaller automata, in particular for
larger outputs. Owl, instead, very frequently generates automata larger than
COLA. In fact, on the 15,710 cases solved by all tools, on average COLA
generated 44 states, Spot 65, and Owl 87\. If we compare COLA with just one
tool at a time, on the 15,854 cases solved by both COLA and Spot, we have 125
states for COLA and 246 for Spot; on the 15,749 cases solved by both COLA and
Owl, we have 45 states for COLA and 88 for Owl. A similar situation occurs for
the number of transitions, so we omit it.

Figure 4: Acceptance sets comparison for the determinization of NBAs from
automata-benchmarks.

Lastly, in Figure 4 we compare the number of acceptance sets (i.e., the colors
in Definition 1) of the generated DPAs; more precisely, we consider the
integer value occurring in the mandatory Acceptance: INT acceptance-cond
header item of the HOA format [1], which can be $0$ for the automata with all
or none accepting transitions. From the plots we can see that COLA generates
more frequently DPAs with a number of colors that is no more than the number
used by Spot, as indicated by the yellow/red marks on (10,394 cases) or above
(5,495 cases) the diagonal. Only in very few cases COLA generates DPAs with
more colors than Spot (22 cases), as indicated by the few blue/greenish marks
below the diagonal. Regarding Owl, however, from the plot we can clearly see
that COLA uses almost always (15,840 cases) fewer colors than Owl; the only
exception is for the mark at $(0,0)$ representing 63 cases.

Table 1: Pearson correlation coefficients for the automata-benchmarks experiments. | # input states | # input SCCs | average SCC size
---|---|---|---
runtime | 0.77 | 0.62 | -0.01
output states | 0.41 | 0.17 | 0.05

The number and sizes of SCCs influence the performance of COLA, so we provide
some statistics about the correlation between these and the runtime and size
of the generated DPA. By combining the execution statistics with the input
SCCs and states, we get the Pearson correlation coefficients shown in Table 1.
Here the larger the number in a cell is, the stronger the positive correlation
between the element that the row and the column represent. From these
coefficients we can say that there is a quite strong positive correlation
between the number of states and of SCCs and the running time, but not for the
average SCC size; regarding the output states, the situation is similar but
much weaker.

We also considered a second set of benchmarks – 644 NBAs generated by Spot’s
ltl2tgba on the LTL formulas considered in [23], as available in the Owl’s
repository at https://gitlab.lrz.de/i7/owl. The outcomes for these benchmarks
are similar, but a bit better for COLA, to the ones for automata-benchmarks,
so we do not present them in detail. In Appendix 0.B we provide additional
plots for the automata-benchmarks benchmarks as well as the ones for these 644
NBAs.

##  6 Related Work

To the best of our knowledge, our determinization construction is the _first_
algorithm that determinizes SCCs _independently_ while taking advantage of
different structures of SCCs, which is the main difference between our
algorithm and existing works. We illustrate other minor differences below.

Different types of SCCs, like DACs and IWCs, are also taken with special care
in [28] as in our work, modulo the handling details. However, the work [28]
does not treat them independently as the labelling numbers in those SCCs still
have relative order with those in other SCCs. Thus their algorithm can be
exponentially worse than ours (cf. Theorem 5) and performs not as well as ours
in practice; see the comparison with Owl in Section 5. The determinization
algorithm given in [14] for SDBAs is a special case of the one presented in
[34] for NBAs, which gives precedence to the deterministic runs seeing
accepting transitions earlier, while we give precedence to runs that enter
DACs earlier. More importantly, the algorithm from [14] does not work when
there is nondeterminism between DACs, while our algorithm overcomes this by
considering DACs separately and by ignoring runs going to other SCCs.

Current works for determinization of general NBAs, such as [34, 35, 18, 27,
21, 37] can all be interpreted as different flavours of the Safra-Piterman
based algorithm. Our determinization of NACs is also based on Safra-trees,
except that we may have newly arriving states from other SCCs while other
works only need to consider the successors from the current states in the
Safra-tree. The modular approach for determinizing Büchi automata given in
[17] builds on reduced split trees [21] and can construct the deterministic
automaton with a given tree-width. The algorithm constructs the final
deterministic automaton by running in parallel the NBA for all possible tree-
widths, rather than working on SCCs independently as we do in this work.

Figure 5: A family of NBAs $\mathcal{A}_{\\_}{n}$ with
$\Sigma=\\{0,1,\cdots,n\\}$.

Compared to the algorithms operating on the whole NBA, our algorithm can be
exponentially better on the family of NBAs shown in Figure 5, as formalized in
Theorem 5; we can encounter some variation of this family of NBAs when working
with fairness properties. The intuition is that we take care of the DACs
$\\{q_{\\_}{i}\\}_{\\_}{i=1}^{n}$ independently, so for each of them we have
only two choices: either the run is in the DAC, or it is not in the DAC;
resulting in a single exponential number of combinations. Existing works [14,
34, 35, 32, 21, 27] order the runs entering the DACs based on when they visit
accepting transitions, in which every order corresponds to a permutation of
$\\{q_{\\_}{1},\cdots,q_{\\_}{n}\\}$. See Appendix 0.A.7 for a detailed proof.

[]theoremfamilyOfNbasBetterComplexity There exists a family of NBAs
$\mathcal{A}_{\\_}{n}$ with $n+2$ states for which the algorithms in [14, 34,
35, 32, 21, 27] give a DPA with at least $n!$ macrostates while ours gives a
DELA with at most $2^{n+2}$ macrostates. In practice, for each NBA
$\mathcal{A}_{\\_}{n}$, $n\geq 3$, COLA produces a DELA/DPA with $n$
macrostates, while both Spot and Owl give a DPA with $n!+1$ macrostates.

##  7 Conclusion and Future Work

We proposed a divide-and-conquer determinization construction for NBAs that
takes advantage of the structure of different types of SCCs and determinizes
them independently. In particular, our construction can be exponentially
better than classical works on a family of NBAs. Experiments showed that our
algorithm outperforms the state-of-the-art implementations regarding the
number of states and transitions on a large set of benchmarks. To summarize,
our divide-and-conquer determinization construction is very _practical_ ,
being a good complement to existing theoretical approaches.

Our divide-and-conquer approach for NBAs can also be applied to the
complementation problems of NBAs. By Proposition 1, $w$ is not accepted by
$\mathcal{A}$ if and only if there are no accepting runs staying in an SCC.
Thus we can construct a _generalized_ Büchi automaton with a conjunction of
$\mathsf{Inf}(i)$ as the acceptance formula to accept the complement language
$\Sigma^{\omega}\setminus\mathsf{L}(\mathcal{A})$ of $\mathcal{A}$; the
generalized Büchi automaton in fact takes the _intersection_ of the complement
language of each type of SCCs. For complementing IWCs, we use the same
construction as determinization except that the acceptance formula will be
$\mathsf{Inf}(1)$. For complementing DACs, we can borrow the idea of NCSB
complementation construction [4] which complements SDBAs in time $4^{n}$. For
complementing NACs, we just adapt the _slice-based_ complementation [21] of
general NBAs. We leave the details of this divide-and-conquer complementation
construction for NBAs as future work.

#### Acknowledgements.

We thank the anonymous reviewers for their valuable suggestions to this paper.
This work is supported in part by the National Natural Science Foundation of
China (Grant No. 62102407 and 61836005), NSF grants IIS-1527668, CCF-1704883,
IIS-1830549, CNS-2016656, DoD MURI grant N00014-20-1-2787, and an award from
the Maryland Procurement Office.
This project has received funding from the European Union’s Horizon 2020
research and innovation programme under the Marie Skłodowska-Curie grant
agreement No 101008233.

## References

  * [1] Babiak, T., Blahoudek, F., Duret-Lutz, A., Klein, J., Křetínský, J., Müller, D., Parker, D., Strejček, J.: The Hanoi Omega-Automata Format. In: CAV. LNCS, vol. 9206, pp. 479–486 (2015)
  * [2] Baier, C., Katoen, J.P.: Principles of Model Checking. MIT press (2008)
  * [3] Beyer, D., Löwe, S., Wendler, P.: Reliable benchmarking: requirements and solutions. Int. J. Softw. Tools Technol. Transf. 21(1), 1–29 (2019)
  * [4] Blahoudek, F., Heizmann, M., Schewe, S., Strejček, J., Tsai, M.H.: Complementing semi-deterministic Büchi automata. In: TACAS. LNCS, vol. 9636, pp. 770–787 (2016)
  * [5] Boigelot, B., Jodogne, S., Wolper, P.: On the use of weak automata for deciding linear arithmetic with integer and real variables. In: IJCAR. LNCS, vol. 2083, pp. 611–625 (2001)
  * [6] Büchi, J.R.: On a decision method in restricted second order arithmetic. In: The Collected Works of J. Richard Büchi, pp. 425–435. Springer (1990)
  * [7] Casares, A., Colcombet, T., Fijalkow, N.: Optimal transformations of games and automata using muller conditions. In: ICALP. LIPIcs, vol. 198, pp. 123:1–123:14 (2021)
  * [8] Casares, A., Duret-Lutz, A., Meyer, K.J., Renkin, F., Sickert, S.: Practical applications of the alternating cycle decomposition. In: TACAS. LNCS, vol. 13244, pp. 99–117 (2022)
  * [9] Colcombet, T., Zdanowski, K.: A tight lower bound for determinization of transition labeled Büchi automata. In: ICALP. LNCS, vol. 5556, pp. 151–162 (2009)
  * [10] Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. J. ACM 42(4), 857–907 (1995)
  * [11] De Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: IJCAI. pp. 854–860 (2013)
  * [12] Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, E., Xu, L.: Spot 2.0 – a framework for LTL and $\omega$-automata manipulation. In: ATVA. LNCS, vol. 9938, pp. 122–129 (2016)
  * [13] Emerson, E.A., Lei, C.: Modalities for Model Checking: Branching Time Logic Strikes Back. Sci. Comput. Program. 8(3), 275–306 (1987)
  * [14] Esparza, J., Kretínský, J., Raskin, J., Sickert, S.: From LTL and limit-deterministic Büchi automata to deterministic parity automata. In: TACAS. LNCS, vol. 10205, pp. 426–442 (2017)
  * [15] Esparza, J., Křetínský, J., Sickert, S.: A unified translation of linear temporal logic to $\omega$-automata. J. ACM 67(6) (oct 2020)
  * [16] Farwer, B.: omega-automata. In: Automata, Logics, and Infinite Games: A Guide to Current Research. LNCS, vol. 2500, pp. 3–20 (2001)
  * [17] Fisman, D., Lustig, Y.: A modular approach for Büchi determinization. In: CONCUR. LIPIcs, vol. 42, pp. 368–382 (2015)
  * [18] Fogarty, S., Kupferman, O., Vardi, M.Y., Wilke, T.: Profile trees for Büchi word automata, with application to determinization. Inf. Comput. 245, 136–151 (2015)
  * [19] Havlena, V., Lengál, O., Smahlíková, B.: Sky is not the limit - tighter rank bounds for elevator automata in Büchi automata complementation. In: TACAS. LNCS, vol. 13244, pp. 118–136 (2022)
  * [20] Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley Longman Publishing Co., Inc. (2006)
  * [21] Kähler, D., Wilke, T.: Complementation, disambiguation, and determinization of Büchi automata unified. In: ICALP. pp. 724–735 (2008)
  * [22] Klein, J., Baier, C.: On-the-fly stuttering in the construction of deterministic _omega_ -automata. In: CIAA. LNCS, vol. 4783, pp. 51–61 (2007)
  * [23] Kretínský, J., Meggendorfer, T., Sickert, S.: Owl: A library for $\omega$-words, automata, and LTL. In: ATVA. LNCS, vol. 11138, pp. 543–550 (2018)
  * [24] Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM Trans. Comput. Log. 2(3), 408–429 (2001)
  * [25] Liu, W., Wang, J.: A tighter analysis of Piterman’s Büchi determinization. Inf. Process. Lett. 109(16), 941–945 (2009)
  * [26] Löding, C.: Optimal bounds for transformations of omega-automata. In: FSTTCS. LNCS, vol. 1738, pp. 97–109 (1999)
  * [27] Löding, C., Pirogov, A.: Determinization of Büchi automata: Unifying the approaches of Safra and Muller-Schupp. In: ICALP. LIPIcs, vol. 132, pp. 120:1–120:13 (2019)
  * [28] Löding, C., Pirogov, A.: New optimizations and heuristics for determinization of Büchi automata. In: ATVA. LNCS, vol. 11781, pp. 317–333 (2019)
  * [29] Michel, M.: Complementation is more difficult with automata on infinite words. Tech. rep., CNET, Paris (Manuscript) (1988)
  * [30] Miyano, S., Hayashi, T.: Alternating finite automata on $\omega$-words. Theor. Comput. Sci. 32(3), 321–330 (1984)
  * [31] Muller, D.E., Saoudi, A., Schupp, P.E.: Alternating automata, the weak monadic theory of trees and its complexity. Theor. Comput. Sci. 97(2), 233–244 (1992)
  * [32] Piterman, N.: From nondeterministic Büchi and Streett automata to deterministic parity automata. Log. Methods Comput. Sci. 3(3) (2007)
  * [33] Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL. pp. 179–190 (1989)
  * [34] Redziejowski, R.R.: An improved construction of deterministic omega-automaton using derivatives. Fundam. Informaticae 119(3-4), 393–406 (2012)
  * [35] Safra, S.: On the complexity of $\omega$-automata. In: FOCS. pp. 319–327 (1988)
  * [36] Safra, S., Vardi, M.Y.: On omega-automata and temporal logic (preliminary report). In: STOC. pp. 127–137 (1989)
  * [37] Schewe, S.: Büchi complementation made tight. In: STACS. LIPIcs, vol. 3, pp. 661–672 (2009)
  * [38] Schewe, S.: Tighter bounds for the determinisation of Büchi automata. In: FOSSACS. LNCS, vol. 5504, pp. 167–181 (2009)
  * [39] Tsai, M., Fogarty, S., Vardi, M., Tsay, Y.: State of Büchi complementation. Log. Methods Comput. Sci. 10(4) (2014)
  * [40] Vardi, M.Y.: The rise and fall of linear temporal logic. In: GandALF. EPTCS (2011)
  * [41] Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1–37 (1994)
  * [42] Yan, Q.: Lower bounds for complementation of $\omega$-automata via the full automata technique. Log. Methods Comput. Sci. 4(1:5) (2008)

##  Appendix 0.A Formal Proofs of the Theorems

###  0.A.1 Proof of Lemma 3.1

*

#### Statement (1): correctness.

Assume that there is a run $\rho$ that enters into an accepting IWC
$C\subseteq\mathsf{WA}$ at level $k$ and then stays there forever. By
definition, we have that ${\rho}[\ell]\in S_{\\_}{\ell}$ as well as
${\rho}[\ell]\in\mathsf{WA}\subseteq\mathsf{W}$ for all $\ell\geq k$, thus
also ${\rho}[\ell]\in P_{\\_}{\ell}$; recall that color $1$ is emitted solely
when $O$ is empty. If in the $(P,O)$-sequence, $O$ never becomes empty after
level $k$, then we never get color $1$ anymore, so the claim follows trivially
since we have got color $1$ at most $k$ times. Suppose now that $O$ becomes
empty at some level $h>k$; this implies that ${\rho}[h+1]\in O_{\\_}{h+1}$,
since by definition we have
$O_{\\_}{h+1}=\delta(P_{\\_}{h},{w}[h])\cap\mathsf{WA}$ and ${\rho}[h+1]\in
P_{\\_}{h+1}$ as well as ${\rho}[h+1]\in\mathsf{WA}$. Since we have
${\rho}[j]\in\mathsf{WA}$ for all $j\geq h+1$ by the hypothesis that $\rho$
enters into an accepting IWC $C\subseteq\mathsf{WA}$ at level $k$ and then
stays there forever, we have that $O_{\\_}{j}$ can never become empty anymore.
As before, we never get color $1$ anymore, so the claim follows since we have
got color $1$ at most $h$ times.

On the other hand, if we receive color $1$ finitely many times, then by
definition there are only finitely many empty $O$-sets. There must be
$k\in\mathbb{N}$ such that $O_{\\_}{j}\neq\emptyset$ for all $j\geq k$.
Therefore, according to König’s lemma, there must be a run $\rho$ of
$\mathcal{A}$ over $w$ such that ${\rho}[j]\in O_{\\_}{j}$ for all $j\geq k$
(the states ${\rho}[i]$ with $i<k$ are not necessarily $\mathsf{WA}$-states).
According to Proposition 1, $\rho$ will end up in an SCC, which must be an
accepting IWC since $O_{\\_}{j}\subseteq\mathsf{WA}$ for all $j\geq k$. By
definition, it follows that $\rho$ takes accepting transitions infinitely
often, thus $\rho$ is accepting.

####  0.A.1.1 Statement (2): complexity.

Regarding the number of pairs $(P,O)$, note that $O\subseteq
P\subseteq\mathsf{W}$. Thus for each $q\in\mathsf{W}$, either $q\in O\subseteq
P$, or $q\in P$ but $q\notin O$, or $q\notin P\supseteq O$. Therefore, the
number of possible $(P,O)$ pairs is at most $3^{|\mathsf{W}|}$.

###  0.A.2 Proof of Lemma 3.2

*

#### Statement (1): correctness.

Assume that there is an accepting run $\rho$ of $\mathcal{A}$ over $w$ that
enters and never leaves the DAC $\mathsf{D}$: this means that there is
$\ell\in\mathbb{N}$ such that ${\rho}[j]\in S_{\\_}{j}\cap\mathsf{D}$ for all
$j\geq\ell$. By definition, for all such $j\geq\ell$ the sequence of values
$\mathfrak{g}_{\\_}{j}({\rho}[j])$ never becomes $\infty$ and never increases.
This implies that such sequence eventually stabilizes, thus from some point
$h>\ell$, we have $\mathfrak{g}_{\\_}{j}({\rho}[j])=k$ for all $j\geq h$;
moreover, we also have
$\\{1,\cdots,k\\}\subseteq\beta(\mathfrak{g}_{\\_}{j})$. This implies that
$\min\mathsf{B}(\mathfrak{g}_{\\_}{j},{w}[j],\mathfrak{g}_{\\_}{j+1})=p>k$
after level $h$ while
$\mathsf{G}(\mathfrak{g}_{\\_}{j},{w}[j],\mathfrak{g}_{\\_}{j+1})$ can be
empty (resulting in the color $c=\min\\{2\cdot(|\mathsf{D}|+1),2p-1\\}>2k$) or
non-empty (resulting in the color
$c=2\cdot\min\mathsf{G}(\mathfrak{g}_{\\_}{j},{w}[j],\mathfrak{g}_{\\_}{j+1})\leq
2k<2\cdot|\mathsf{D}|$), depending on whether accepting transitions are taken.
Since the run $\rho$ is accepting, we know that accepting transitions are
taken infinitely often, so the minimum color occurring infinitely often is
some even number at most $2k$.

Assume that the minimum color occurring infinitely often is even; let us call
it $2k$ with $k\geq 1$. Let $h>0$ be the level after which the minimum color
we receive infinitely often is $2k$. It is easy to see that after level $h$,
the run $\rho$ with the labelling number $k$ stays in $\mathsf{D}$ and is
accepting by definition. Since ${\rho}[h]$ is a state reachable from the
initial state $\iota$, we then have an accepting run of $\mathcal{A}$ over $w$
that stays in $\mathsf{D}$.

#### Statement (2): complexity.

Let $n_{\\_}{d}=|\mathsf{D}|$. Every possible labelling function can be seen
as first choosing $0\leq k\leq n_{\\_}{d}$ states and getting a permutation
from those states. So the number of possible labeling functions is

$\displaystyle\sum_{\\_}{k=0}^{n_{\\_}{d}}\binom{n_{\\_}{d}}{k}\cdot k!$
$\displaystyle=\sum_{\\_}{k=0}^{n_{\\_}{d}}\frac{n_{\\_}{d}!}{(n_{\\_}{d}-k)!\cdot
k!}\cdot k!$
$\displaystyle=\sum_{\\_}{k=0}^{n_{\\_}{d}}\frac{n_{\\_}{d}!}{(n_{\\_}{d}-k)!}$
$\displaystyle\leq
n_{\\_}{d}!\cdot\Bigg{(}\frac{1}{0!}+\frac{1}{1}+\frac{1}{1\times
2}+\frac{1}{2\times
3}+\cdots+\frac{1}{(n_{\\_}{d}-1)\times(n_{\\_}{d})}\Bigg{)}$
$\displaystyle=n_{\\_}{d}!\cdot\Bigg{(}1+1+\Big{(}\frac{1}{1}-\frac{1}{2}\Big{)}+\Big{(}\frac{1}{2}-\frac{1}{3}\Big{)}+\cdots+\Big{(}\frac{1}{n_{\\_}{d}-1}-\frac{1}{n_{\\_}{d}}\Big{)}\Bigg{)}$
$\displaystyle=n_{\\_}{d}!\cdot\Bigg{(}1+1+\frac{1}{1}-\frac{1}{2}+\frac{1}{2}-\frac{1}{3}+\cdots+\frac{1}{n_{\\_}{d}-1}-\frac{1}{n_{\\_}{d}}\Bigg{)}$
$\displaystyle=n_{\\_}{d}!\cdot\Bigg{(}3-\frac{1}{n_{\\_}{d}}\Bigg{)}$
$\displaystyle\leq 3\cdot n_{\\_}{d}!.$

Thus the number of possible labelling functions $\mathfrak{g}$ is at most
$3\cdot|\mathsf{D}|!$.

###  0.A.3 Proof of Lemma 3.3

*

#### Statement (1): correctness.

Assume that there exists an accepting run $\rho$ of $\mathcal{A}$ over $w$
eventually staying in $\mathsf{N}$. Assume that at level $\ell_{\\_}{0}$,
$\rho$ enters $\mathsf{N}$ and is assigned with labelling $[p]$. We then have
the sequence of labellings of $\rho$ inside $\mathsf{N}$ as
$\mathfrak{t}_{\\_}{\ell_{\\_}{0}}({\rho}[\ell_{\\_}{0}])\mathfrak{t}_{\\_}{\ell_{\\_}{0}+1}({\rho}[\ell_{\\_}{0}+1])\cdots$.

Every time $\rho$ visits an accepting transition, the labelling list
associated with the $\rho$-state will be appended with an additional integer
larger than the ones already in the labelling list. By construction, the first
integer in $\mathfrak{t}_{\\_}{\ell}({\rho}[\ell])$ with
$\ell\geq\ell_{\\_}{0}$ cannot increase while reading $w$, i.e., when $\ell$
increases. Since $\rho$ stays in $\mathsf{N}$ forever, the first integer in
each labelling list of $\rho$ must stabilize at some level. The second integer
in each labelling list of $\rho$ may also become stable at some point,
depending on whether it will be removed due to the occurrence of good events.
In general, there must exist a maximum integer $k$ and a level
$\ell_{\\_}{1}>\ell_{\\_}{0}$ such that $k$ occurs in
$\mathfrak{t}^{\prime\prime}_{\\_}{\ell}({\rho}[\ell])$ and
$\mathfrak{t}_{\\_}{\ell}({\rho}[\ell])$ for all $\ell>\ell_{\\_}{1}$ and all
integers $k^{\prime}\leq k$ after level $\ell_{\\_}{1}$ will not disappear; if
one of such $k^{\prime}$ would disappear, $k$ will be mapped to a smaller
integer via the function $\mathsf{ord}$.

Thus, every time we are at a level $\ell>\ell_{\\_}{1}$ where the maximum
number in $\mathfrak{t}_{\\_}{\ell}({\rho}[\ell])$ is larger than $k$ but the
maximum integer in $\mathfrak{t}_{\\_}{\ell+1}({\rho}[\ell+1])$ is $k$, we
also need to have seen a good event; thus we will put the integer $k$ into
$\mathsf{G}(e)$, where $e$ is the transition
$e=(\mathfrak{t}_{\\_}{\ell}({\rho}[\ell]),{w}[\ell],\mathfrak{t}_{\\_}{\ell+1}({\rho}[\ell+1]))$.

Let $k^{\prime}$ be the maximum number occurring in the list
$\mathfrak{t}_{\\_}{\ell}({\rho}[\ell])$; we have states associated with
$k^{\prime}$ since $\rho$ always continues. Thus, by definition, we must have
seen a good event represented by the integer $k$. We then will receive an even
color at most $2k$. Moreover, it is not possible to put an integer less than
$k$ in $\mathsf{B}(e)$, since there are states associated with them, otherwise
$k$ would be renumbered against the assumption that $k$ is stable. Thus we
have proved that the minimum color we receive infinitely often is even and it
must be at most $2k$.

As for the other direction, we assume that the minimum color we receive
infinitely often is even, say $2k$. Assume that the sequence of labelling
functions over $w$ is
$\mathfrak{t}_{\\_}{0}\cdots\mathfrak{t}_{\\_}{\ell}\cdots$. There are
infinitely many transitions between two successive labelling functions where
we receive the color $2k$. Thus, by construction, this happens because there
must be infinitely many labelling function $\mathfrak{t}_{\\_}{i}$ such that
$(\mathfrak{t}_{\\_}{i-1},{w}[i-1],\mathfrak{t}_{\\_}{i})$ is associated with
the color $2k$. Since the number of possible labelling functions is finite,
there must be a labelling function, say $\mathfrak{t}$, such that
$(\mathfrak{t}_{\\_}{i-1},{w}[i-1],\mathfrak{t}=\mathfrak{t}_{\\_}{i})$ is
assigned the color $2k$. That is, the labelling function $\mathfrak{t}$ has
been visited for infinitely many times. It follows that all the states in
$\mathsf{N}$ associated with the color $k$ in $\mathfrak{t}$ have been reached
for infinitely many times and all runs branched from those states have all
visited accepting transitions, since by definition we set all branched runs
back to the labelling list whose last integer is $k$. According to the König’s
lemma, there must be a run that visits accepting transitions infinitely often
starting from the states in $\mathsf{N}$. Since every state in $\mathsf{N}$ is
reachable from the initial state $\iota$, there must be an accepting run
staying in the NAC $\mathsf{N}$.

#### Statement (2): complexity.

For a given NAC $\mathsf{N}$, we can map a labelling function
$\mathfrak{t}_{\\_}{\ell}$ at level $\ell$ to a Safra-tree like structure in
which each node is labelled with a set of $\mathcal{A}$-states. The root node
is constantly labelled with the set $\mathsf{N}$. The tree has at most
$|\mathsf{N}|$ nodes with the root node being $0$. For a state $q\in
S_{\\_}{\ell}\cap\mathsf{N}$, $\mathfrak{t}_{\\_}{\ell}(q)$ is in fact a list
of node numbers where the state $q$ resides in. We say that the maximal number
of the labelling $\mathfrak{t}_{\\_}{\ell}(q)$ is the host node of $q$. We
denote by $\mathsf{node}(q)$ the host node of $q$. By definition, the integers
in a labelling are already in ascending order. Therefore, we have the
following properties:

  * •

if $\mathfrak{t}_{\\_}{\ell}(q)$ is a prefix of
$\mathfrak{t}_{\\_}{\ell}(q^{\prime})$, then $\mathsf{node}(q)$ is an ancestor
node of $\mathsf{node}(q^{\prime})$. Moreover, we have
$\mathsf{node}(q)<\mathsf{node}(q^{\prime})$. In particular, if
$\mathfrak{t}_{\\_}{\ell}(q)$ has one less integer than
$\mathfrak{t}_{\\_}{\ell}(q^{\prime})$, then $\mathsf{node}(q)$ is the parent
of $\mathsf{node}(q^{\prime})$;

  * •

the states labelled in a parent node $n$ must form a superset of all states in
its children, just like that in history trees [37]; and

  * •

the states in two different child nodes of a node are disjoint. This is
immediate by construction.

Also, the node number of a parent node must be smaller than that of its every
child [37, 32] according to the order of entering $\mathsf{N}$. (This is
called later introduction record in literature.) The labelling of the tree
with the states can be seen as a function from $\mathsf{N}$ to
$\\{1,\cdots,m\\}$, where $m$ is the number of nodes, that maps a state
$q\in\mathsf{N}$ to the largest node number it resides in and to $0$ if the
state is not reached in the current level, thus it is in the root node.
According to [37] (in the second paragraph of page 179), the number of
different trees is $2\cdot(|\mathsf{N}|-1)!\cdot|\mathsf{N}|!\leq
2\cdot(|\mathsf{N}|!)^{2}$.

###  0.A.4 Proof of Theorem 4

*

#### Statement (1): correctness.

Each word $w$ accepted by $\mathcal{A}$, by Proposition 1, eventually gets
trapped in an accepting SCC, i.e., either by the IWCs, or a DAC or a NAC; thus
the corresponding results given in Lemmas 3.1, 3.2, and 3.3 apply,
respectively. Since $\mathcal{A}^{\mathsf{E}}$ accepts the union of the words
accepted by each single construction, we have that $w$ is also accepted by
$\mathcal{A}^{\mathsf{E}}$, that is,
$\mathsf{L}(\mathcal{A})\subseteq\mathsf{L}(\mathcal{A}^{\mathsf{E}})$.

On the other hand, if a word $w$ is accepted by $\mathcal{A}^{\mathsf{E}}$,
then it must be accepted by one of its components, i.e., either the one for
IWCs, for DACs or for NACs; thus the corresponding results given in Lemmas
3.1, 3.2, and 3.3 apply, respectively. In all cases, we derive that $w$ is
accepted by $\mathcal{A}$, that is,
$\mathsf{L}(\mathcal{A}^{\mathsf{E}})\subseteq\mathsf{L}(\mathcal{A})$. By
combining the obtained language inclusions, we derive
$\mathsf{L}(\mathcal{A}^{\mathsf{E}})=\mathsf{L}(\mathcal{A})$ as required.

#### Statement (2): complexity

The size of $\mathcal{A}^{\mathsf{E}}$ follows directly by taking the product
of the number of pairs or labelling functions given by Lemmas 3.1, 3.2, and
3.3; the number of colors is just by definition.

###  0.A.5 Proof of Corollary 4

*

#### Statement (1): weak BAs.

The $3^{n}$ macrostates for the weak BAs case is a trivial consequence of
Theorem 4: since a weak BA has no DACs or NACs, only IWCs, we have
$\mathsf{W}=Q$ and $d=k=0$ that give $3^{n}$ when instantiating the formula
for the number of macrostates in Theorem 4.

#### Statement (2): elevator BAs.

We now prove that determinizing elevator BAs can be done in
$\mathsf{\Theta}(n!)$; it is in fact a direct result of Theorem 4. It is
trivial to see that the constructed DELA has the same language as the input,
according to Theorem 4, so we just need to prove that the determinization
complexity is in $\mathsf{\Theta}(n!)$.

Recall that elevator BAs have only IWCs and DACs as SCCs, thus $k=0$. Let
$n_{\\_}{w}=|\mathsf{W}|$ and $n_{\\_}{i}=|\mathsf{D}^{i}|$ for each of the
$d$ DACs $\mathsf{D}^{i}$. In this case, the worst-case complexity of our
algorithm is only

$\displaystyle 3^{n_{\\_}{w}}\cdot\prod_{\\_}{i=1}^{d}3\cdot n_{\\_}{i}!$
$\displaystyle=3^{n_{\\_}{w}+d}\cdot(n_{\\_}{1}+\cdots+n_{\\_}{d})!\cdot\frac{1}{\binom{n_{\\_}{1}+\cdots+n_{\\_}{d}}{n_{\\_}{1}}}\cdot\frac{1}{\binom{n_{\\_}{2}+\cdots+n_{\\_}{d}}{n_{\\_}{2}}}\cdot\cdots\cdot\frac{1}{\binom{n_{\\_}{d}}{n_{\\_}{d}}}$
$\displaystyle\leq 3^{n}\cdot
n!\cdot\prod_{\\_}{i=1}^{d}\frac{1}{n_{\\_}{i}}\in\mathsf{O}(n!),$

where $n=n_{\\_}{w}+\sum_{\\_}{i=1}^{d}n_{\\_}{i}$. It is already known [26,
14] that the lower bound for determinizing semi-deterministic Büchi automata
(SDBAs), a strict subset of elevator NBAs, is $n!$. Thus our determinization
algorithm for elevator Büchi automata is already asymptotically optimal since
the lower bound and the upper bound coincide as $\mathsf{\Theta}(n!)$.

###  0.A.6 Proof of Theorem 4

* The different algorithms presented in Section 3, that form the basis for the construction of $\mathcal{A}^{\mathsf{E}}$ in Section 4, generate a parity condition for the acceptance inside the various SCCs.

It is known that a DPA $\mathcal{A}^{\mathsf{P}}$ can be trivially transformed
into a Rabin automaton $\mathcal{A}^{\mathsf{R}}$ by changing only the
accepting formula $\mathsf{Acc}$ and the coloring function $\mathsf{p}$, that
is, states and transitions remain the same (cf. [16, Transformation 1.18]); we
adopt a similar approach for our case, just we have to consider the transpose
operation we applied to the colors and the fact that the global acceptance
condition $\mathsf{Acc}^{\mathsf{E}}$ is the disjunction of the parity
conditions of the various SCCs.

By definition, a word $w$ is accepted by a parity automaton with color set
$\Gamma_{k}$ if there is a run $\rho$ over $w$ such that
$\min\mathsf{p}(\mathit{inf}({\rho}))$ is even, that is, $p$ is the minimum
even color occurring infinitely often and all other colors $p^{\prime}<p$
occur only finitely often. To define the Rabin acceptance formula, we just
give all transitions originally with color $p$ the color $p/2$, and all
transitions with smaller value the color $p/2-1$; then the Rabin acceptance
formula is
$\mathsf{Acc}=(\mathsf{Fin}(0)\land\mathsf{Inf}(1))\lor\cdots\lor(\mathsf{Fin}(k/2-1)\land\mathsf{Inf}(k/2))$
and the color set is $\Gamma_{k/2}$ (note that $k$ is an even number by
definition).

From the definition of the acceptance formula $\mathsf{Acc}^{\mathsf{E}}$, we
can see that it is a disjunction of parity-like acceptance conditions. So it
follows that we can also translate $\mathcal{A}^{\mathsf{E}}$ to a DRA without
blow-up of states and transitions.

###  0.A.7 Proof of Theorem 5

*

Each NBA $\mathcal{A}_{\\_}{n}=(Q,q_{\\_}{0},\delta,F)$ in the family is like
the one depicted in Figure 5.

Consider our construction: for the NBA $\mathcal{A}_{\\_}{n}$, there are $n$
DACs $\mathsf{D}^{i}=\\{q_{\\_}{i}\\}$, for $1\leq i\leq n$. The SCCs
$\\{q_{\\_}{0}\\}$ and $\\{q_{\\_}{\bot}\\}$ are both nonaccepting IWCs. So in
our algorithm, the DELA we construct has at most $2^{2}\times 2^{n}=2^{n+2}$
macrostates: $2^{2}$ pairs $(P,O)$ for the IWCs, since $\mathsf{WA}=\emptyset$
thus the $O$-sets for the IWCs are always empty; $2^{n}$ choices for the DAC
level encoding, since for each DAC $\mathsf{D}^{i}=\\{q_{\\_}{i}\\}$, we have
$2$ choices: either no state or only $q_{\\_}{i}$ is currently visited in
$\mathsf{D}^{i}$. In this way we can give a more precise bound than the
general one provided by Theorem 4.

Consider now the constructions from literature: the deterministic part of
$\mathcal{A}_{\\_}{n}$ is
$Q_{D}=\\{q_{\\_}{1},\cdots,q_{\\_}{n},q_{\\_}{\bot}\\}$; the algorithms
described in [14, 34, 35, 21, 32, 27] give precedence to the runs that see an
accepting transition earlier and visit more accepting transitions. That is,
when reading the letter $i\in\\{1,\cdots,n\\}$, the order of the runs entering
in $Q_{D}$ is
$q_{\\_}{i}<q_{\\_}{1}<\cdots<q_{\\_}{i-1}<q_{\\_}{i+1}<\cdots<q_{\\_}{n}$ if
$i\neq 1$ and $q_{\\_}{1}<\cdots<q_{\\_}{n}$ otherwise.

To prove that the DPA constructed by [14, 34, 35, 21, 32, 27] has at least
$n!$ macrostates, we show how to ensure that the order of the states
$D=\\{q_{\\_}{1},\cdots,q_{\\_}{n}\\}$ in a reachable macrostate is a
permutation of the states in $D$; since there are $n!$ permutations, there
need to be at least $n!$ macrostates. To this end, we assume that we are given
a permutation
$\pi=q_{\\_}{i_{\\_}{1}}<q_{\\_}{i_{\\_}{2}}<q_{\\_}{i_{\\_}{3}}<\cdots<q_{\\_}{i_{\\_}{n}}$
and we show how to reach the corresponding macrostate from the initial state
of the DPA via a finite word $u_{\\_}{\pi}$, by constructing such a word
$u_{\\_}{\pi}$ from the above permutation $\pi$. Note that we ignore the place
where we have $q_{\\_}{\bot}$ and only focus on the order of the $D$-states.

From the initial state of the DPA, which contains only the initial state
$q_{\\_}{0}$ of $\mathcal{A}_{\\_}{n}$, to put $q_{\\_}{i_{\\_}{1}}$ in the
first place, we first read the letter $i_{\\_}{1}$, which leads to the
macrostate with $q_{\\_}{i_{\\_}{1}}<q_{\\_}{1}<\cdots
q_{\\_}{i_{\\_}{1}-1}<q_{\\_}{i_{\\_}{1}+1}<\cdots<q_{\\_}{n}$. Note that we
see an accepting transition from $q_{\\_}{0}$ to $q_{\\_}{i_{\\_}{1}}$ via
$i_{\\_}{1}$, so the algorithm gives precedence to the run that reaches
$q_{\\_}{i_{\\_}{1}}$ and orders the other states according to the usual state
order $\preccurlyeq$. To put $q_{\\_}{i_{\\_}{2}}$ in the second position, we
can just read once each letter from
$\\{1,\cdots,n\\}\setminus\\{i_{\\_}{1},i_{\\_}{2}\\}$ in ascending order.
This makes all states in $D$, except for $q_{\\_}{i_{\\_}{1}}$ and
$q_{\\_}{i_{\\_}{2}}$, transition to $q_{\\_}{\bot}$, leaving
$q_{\\_}{i_{\\_}{2}}$ just after $q_{\\_}{i_{\\_}{1}}$, obtaining the order
$q_{\\_}{i_{\\_}{1}}<q_{\\_}{i_{\\_}{2}}<q_{\\_}{1}<\cdots<q_{\\_}{n}$. Note
that states will keep coming from the initial state $q_{\\_}{0}$ and if the
newly arrived states are already present, they will be ignored. To put
$q_{\\_}{i_{\\_}{3}}$ in the third position, similarly to the previous case we
read all letters from
$\\{1,\cdots,n\\}\setminus\\{i_{\\_}{1},i_{\\_}{2},i_{\\_}{3}\\}$ in ascending
order. By proceeding in the same way, we obtain the order
$q_{\\_}{i_{\\_}{1}}<q_{\\_}{i_{\\_}{2}}<q_{\\_}{i_{\\_}{3}}<\cdots<q_{\\_}{i_{\\_}{n}}$,
which is exactly the given permutation $\pi$. Given the arbitrary choice of
$\pi$, we have that all permutations correspond to a different macrostate in
the DPA constructed by the algorithms given in [14, 34, 35, 21, 32, 27], so
the DPA has at least $n!$ macrostates.

####  0.A.7.1 Consistent experiments.

To check whether the behavior of the actual implementations of the algorithms
given in [14, 34, 35, 21, 32, 27] are consistent with the bounds given by
Theorem 5, we have performed some experiments on the family of NBAs with COLA,
Spot and Owl, finding that they behave consistently with Theorem 5. In
practice, for the given NBA $\mathcal{A}_{\\_}{n}$, with $n\geq 3$, COLA gives
a DPA with $n$ macrostates and $\mathsf{Fin}(0)\land\mathsf{Inf}(1)$ as
acceptance formula; Spot returns a DPA with $n!+1$ macrostates and the same
acceptance formula $\mathsf{Fin}(0)\land\mathsf{Inf}(1)$; and Owl produces a
DPA with also $n!+1$ macrostates while the acceptance formula is
$\mathsf{Inf}(0)\lor(\mathsf{Fin}(1)\land(\mathsf{Inf}(2)\lor\mathsf{Fin}(3)))$;
however it fails on $\mathcal{A}_{\\_}{7}$ and larger automata with a
java.lang.StackOverflowError when it tries to optimize the constructed
automaton. On the other hand, COLA can go up for a very large $n$, while Spot
already timeouts on $\mathcal{A}_{\\_}{11}$. We remark that the acceptance
formulas from COLA and Spot have been simplified by the algorithms implemented
in Spot.

##  Appendix 0.B Additional Plots for the Experiments

In this appendix we provide additional plots for the experiments presented in
Section 5, which we omitted in the main part of the paper to keep it short.

###  0.B.1 Determinization of NBAs from automata-benchmarks

Figure 6: Runtime comparison on the determinization of automata-benchmarks.

In Figure 6 we provide scatter plots showing the detailed comparison of COLA
with Spot and Owl with respect to the running time on the single cases. In the
plots, the solid line just before $10^{3}$ indicates the timeout (set to $600$
seconds); the dashed line at $10^{3}$ an out of memory result, and the border
of the plot other failures. As we can see from the plots, Owl is usually
slower than COLA, except for few cases requiring less than one second.
Regarding Spot, it is frequently faster than COLA, showing how well it
performs. COLA, on the other hand, is better than Spot in several cases, on
which it is faster or even able to produce a DPA within 10 seconds while Spot
goes timeout. By comparing these results with the cactus plot in Figure 2, we
can conclude that there is no clear winner between Spot and COLA when we
consider just the running time of the tools.

Figure 7: Transitions comparison on the determinization of automata-
benchmarks; a mark at $10^{-1}$ represents automata without transitions.

In Figure 7 we complete the comparison of COLA with Spot and Owl by
considering the number of transitions in the DPAs generated from the NBAs
available in automata-benchmarks. Since we use logarithmic axes and automata
can have zero transitions (this happens for the automata accepting the empty
language, since the HOA format allows the tools to specify automata that are
not complete), in the plots we place a mark at $10^{-1}$ to represent the fact
that the corresponding tool has returned an automaton with no transitions at
all. As already mentioned in the main part of the paper, the plots are very
similar to the ones about the states shown in Figure 3. Regarding the average
number of transitions generated by the tools, on the 15,710 commonly solved
cases, we have 167 transitions on average by COLA, 266 by Spot, and 292 by
Owl. By splitting the comparison, on the 15,854 cases solved by both COLA and
Spot, we have on average 900 transitions from COLA and 2,174 from Spot; on the
15,749 common cases for COLA and Owl, we have 173 transitions from COLA and
302 from Owl.

###  0.B.2 Determinization of NBAs from LTL Formulas

We now present the plots about the detailed comparison of the different tools
on the NBAs generated from the LTL formulas considered in [23], as available
in the Owl’s repository. As said in the main part of the paper, we used the
Spot’s ltl2tgba command to convert them to NBAs: out of 645 formulas, ltl2tgba
failed to provide the NBA for just one formula.

Figure 8: The cactus plot for the determinization of NBAs from LTL formulas.

The cactus plot shown in Figure 8 is the counterpart of the one about
automata-benchmarks shown in Figure 2. We can see that the two plots show the
same trend: COLA slightly above Spot, with Owl quite below them. If we look at
the actual numbers, we have that both COLA and Spot are able to determinize
643 cases, while Owl only 628, with a common failure for all tools.

Figure 9: Runtime comparison on the determinization of NBAs from LTL formulas.

The plots in Figure 9 are relative to the running time of the different tools.
By comparing them with the corresponding plots in Figure 6, we can see that
they are rather similar. For the NBAs in this set of benchmarks, however, we
can note that COLA is usually faster than Spot, in particular for the inputs
requiring more than $0.1$ seconds to be determinized, as already hinted by the
cactus plot shown in Figure 8.

Figure 10: States comparison on the determinization of NBAs from LTL formulas.

Figure 11: Transitions comparison on the determinization of NBAs from LTL
formulas.

The scatter plots in Figure 10 and Figure 11 are relative to the number of
states and transitions, respectively, of the generated DPAs. Similarly to the
plots about the running time, we again have that COLA and Spot produce
automata of similar size, with COLA more frequently generating smaller
automata than Spot in this benchmark than in automata-benchmarks (cf. Figure 3
and Figure 7, respectively). By looking at the actual number of states, we
have that on the 628 commonly solved cases, on average the DPA generated by
COLA has 9 states, by Spot 11, and by Owl 45\. If we just compare COLA and
Spot on all 643 solved cases, we have that COLA generates 22 states while Spot
49, on average. This situation is similar also for the average number of
transitions: for the 628 cases solved by all tools, we have 72 for COLA, 108
for Spot, and 609 for Owl; for the 643 cases solved by COLA and Spot, we have
275 and 1547 transitions on average, respectively.

Figure 12: Acceptance sets comparison on the determinization of NBAs from LTL
formulas.

Lastly, the plots in Figure 12 are relative to the number of colors in the
generated DPAs. Differently from the automata-benchmarks plots shown in Figure
4, on the NBAs from LTL formulas COLA always produces a DPA with at most the
number of acceptance sets/colors of the corresponding one produced by Spot;
more precisely, COLA generates 118 times fewer colors than Spot and 525 time
the same number of colors. Owl, on the other hand, behaves better than on
automata-benchmarks, but it still generates more acceptance sets/colors than
COLA, with just 3 cases (out of 628) having the same number of colors for both
tools.