11institutetext:  Faculty of Information Technology, Brno University of
Technology, Czech Republic

# Sky Is Not the Limit

Tighter Rank Bounds for Elevator Automata in
Büchi Automata Complementation
(Technical Report)

Vojtěch Havlena  Ondřej Lengál  Barbora Šmahlíková

###### Abstract

We propose several heuristics for mitigating one of the main causes of
combinatorial explosion in rank-based complementation of Büchi automata (BAs):
unnecessarily high bounds on the ranks of states. First, we identify _elevator
automata_ , which is a large class of BAs (generalizing semi-deterministic
BAs), occurring often in practice, where ranks of states are bounded according
to the structure of strongly connected components. The bounds for elevator
automata also carry over to general BAs that contain elevator automata as a
sub-structure. Second, we introduce two techniques for refining bounds on the
ranks of BA states using data-flow analysis of the automaton. We implement out
techniques as an extension of the tool Ranker for BA complementation and show
that they indeed greatly prune the generated state space, obtaining
significantly better results and outperforming other state-of-the-art tools on
a large set of benchmarks.

##  1 Introduction

_Büchi automata_ (BA) complementation has been a fundamental problem
underlying many applications already since it was introduced in 1962 by Büchi
[1] as an essential part of a decision procedure for a fragment of the second-
order arithmetic. BA complementation has been used as a crucial part of, e.g.,
termination analysis of programs [2, 3, 4] or decision procedures for various
logics, such as S1S [1], the first-order logic of Sturmian words [5], or the
temporal logics ETL and QPTL [6]. Moreover, BA complementation also underlies
BA inclusion and equivalence testing, which are essential instruments in the
BA toolbox. Optimal algorithms, whose output asymptotically matches the lower
bound of $(0.76n)^{n}$ [7] (potentially modulo a polynomial factor), have been
developed [8, 9]. For a successful real-world use, asymptotic optimality is,
however, not enough and these algorithms need to be equipped with a range of
optimizations to make them behave better than the worst case on BAs occurring
in practice.

In this paper, we focus on the so-called _rank-based_ approach to
complementation, introduced by Kupferman and Vardi [10], further improved with
the help of Friedgut [11], and finally made optimal by Schewe [8]. The
construction stores in a macrostate partial information about all runs of a BA
$\mathcal{A}$ over some word $\alpha$. In addition to tracking states that
$\mathcal{A}$ can be in (which is sufficient, e.g., in the determinization of
NFAs), a macrostate also stores a guess of the rank of each of the tracked
states in the _run DAG_ that captures all these runs. The guessed ranks impose
restrictions on how the future of a state might look like (i.e., when
$\mathcal{A}$ may accept). The number of macrostates in the complement depends
combinatorially on the maximum rank that occurs in the macrostates. The
constructions in [10, 11, 8] provides only coarse bounds on the maximum ranks.

A way of decreasing the maximum rank has been suggested in [12] using a PSpace
(and, therefore, not really practically applicable) algorithm (the problem of
finding the optimal rank is PSpace-complete). In our previous paper [13], we
have identified several basic optimizations of the construction that can be
used to refine the _tight-rank upper bound_ (TRUB) on the maximum ranks of
states. In this paper, we push the applicability of rank-based techniques much
further by introducing two novel lightweight techniques for refining the TRUB,
thus significantly reducing the generated state space.

Firstly, we introduce a new class of the so-called _elevator automata_ , which
occur quite often in practice (e.g., as outputs of natural algorithms for
translating LTL to BAs). Intuitively, an elevator automaton is a BA whose
strongly connected components (SCCs) are all either inherently weak111An SCC
is inherently weak if it either contains no accepting states or, on the other
hand, all cycles of the SCC contain an accepting state.  or deterministic.
Clearly, the class substantially generalizes the popular inherently weak [14]
and semi-deterministic BAs [15, 16, 17]). The structure of elevator automata
allows us to provide tighter estimates of the TRUBs, not only for elevator
automata _per se_ , but also for BAs where elevator automata occur as a sub-
structure (which is even more common). Secondly, we propose a lightweight
technique, inspired by data flow analysis, allowing to propagate rank
restriction along the skeleton of the complemented automaton, obtaining even
tighter TRUBs. We also extended the optimal rank-based algorithm to
transition-based BAs (TBAs).

We implemented our optimizations within the Ranker tool [18] and evaluated our
approach on thousands of hard automata from the literature (15 % of them were
elevator automata that were not semi-deterministic, and many more contained an
elevator sub-structure). Our techniques drastically reduce the generated state
space; in many cases we even achieved exponential improvement compared to the
optimal procedure of Schewe and our previous heuristics. The new version of
Ranker gives a smaller complement in the majority of cases of hard automata
than other state-of-the-art tools.

##  2 Preliminaries

#### Words, functions.

We fix a finite nonempty alphabet $\Sigma$ and the first infinite ordinal
$\omega=\\{0,1,\ldots\\}$. For $n\in\omega$, by $[n]$ we denote the set
$\\{0,\dots,n\\}$. For $i\in\omega$ we use $\lfloor\\!\\!\lfloor
i\rfloor\\!\\!\rfloor$ to denote the largest even number smaller of equal to
$i$, e.g., $\lfloor\\!\\!\lfloor 42\rfloor\\!\\!\rfloor=\lfloor\\!\\!\lfloor
43\rfloor\\!\\!\rfloor=42$. An (infinite) word $\alpha$ is represented as a
function $\alpha\colon\omega\to\Sigma$ where the $i$-th symbol is denoted as
$\alpha_{i}$. We abuse notation and sometimes also represent $\alpha$ as an
infinite sequence $\alpha=\alpha_{0}\alpha_{1}\dots$ We use $\Sigma^{\omega}$
to denote the set of all infinite words over $\Sigma$. For a (partial)
function $f\colon X\to Y$ and a set $S\subseteq X$, we define
$f(S)=\\{f(x)\mid x\in S\\}$. Moreover, for $x\in X$ and $y\in Y$, we use
$f\triangleleft\\{x\mapsto y\\}$ to denote the function
$(f\setminus\\{x\mapsto f(x)\\})\cup\\{x\mapsto y\\}$.

#### Büchi automata.

A (nondeterministic transition/state-based) _Büchi automaton_ (BA) over
$\Sigma$ is a quadruple $\mathcal{A}=(Q,\delta,I,Q_{F}\cup\delta_{F})$ where
$Q$ is a finite set of _states_ , $\delta\colon Q\times\Sigma\to 2^{Q}$ is a
_transition function_ , $I\subseteq Q$ is the sets of _initial_ states, and
$Q_{F}\subseteq Q$ and $\delta_{F}\subseteq\delta$ are the sets of _accepting
states_ and _accepting transitions_ respectively. We sometimes treat $\delta$
as a set of transitions $p\overset{a}{\rightarrow}q$, for instance, we use
$p\overset{a}{\rightarrow}q\in\delta$ to denote that $q\in\delta(p,a)$.
Moreover, we extend $\delta$ to sets of states $P\subseteq Q$ as
$\delta(P,a)=\bigcup_{p\in P}\delta(p,a)$, and to sets of symbols
$\Gamma\subseteq\Sigma$ as $\delta(P,\Gamma)=\bigcup_{a\in\Gamma}\delta(P,a)$.
We define the inverse transition function as
$\delta^{-1}=\\{p\overset{a}{\rightarrow}q\mid
q\overset{a}{\rightarrow}p\in\delta\\}$. The notation
$\delta\raisebox{-2.15277pt}{$|$}_{S}$ for $S\subseteq Q$ is used to denote
the restriction of the transition function $\delta\cap(S\times\Sigma\times
S)$. Moreover, for $q\in Q$, we use $\mathcal{A}[q]$ to denote the BA
$(Q,\delta,\\{q\\},Q_{F}\cup\delta_{F})$.

A  _run_ of $\mathcal{A}$ from $q\in Q$ on an input word $\alpha$ is an
infinite sequence $\rho\colon\omega\to Q$ that starts in $q$ and respects
$\delta$, i.e., $\rho_{0}=q$ and $\forall i\geq
0\colon\rho_{i}\overset{\alpha_{i}}{\rightarrow}\rho_{i+1}\in\delta$. Let
$\inf_{Q}(\rho)$ denote the states occurring in $\rho$ infinitely often and
$\inf_{\delta}(\rho)$ denote the transitions occurring in $\rho$ infinitely
often. The run $\rho$ is called _accepting_ iff $\inf_{Q}(\rho)\cap
Q_{F}\neq\emptyset$ or $\inf_{\delta}(\rho)\cap\delta_{F}\neq\emptyset$.

A word $\alpha$ is accepted by $\mathcal{A}$ from a state $q\in Q$ if there is
an accepting run $\rho$ of $\mathcal{A}$ from $q$, i.e., $\rho_{0}=q$. The set
$\mathcal{L}_{\mathcal{A}}(q)=\\{\alpha\in\Sigma^{\omega}\mid\mathcal{A}\text{
accepts }\alpha\text{ from }q\\}$ is called the _language_ of $q$ (in
$\mathcal{A}$). Given a set of states $R\subseteq Q$, we define the language
of $R$ as $\mathcal{L}_{\mathcal{A}}(R)=\bigcup_{q\in
R}\mathcal{L}_{\mathcal{A}}(q)$ and the language of $\mathcal{A}$ as
$\mathcal{L}(\mathcal{A})=\mathcal{L}_{\mathcal{A}}(I)$. We say that a state
$q\in Q$ is _useless_ iff $\mathcal{L}(\mathcal{A}[q])=\emptyset$. If
$\delta_{F}=\emptyset$, we call $\mathcal{A}$ _state-based_ and if
$Q_{F}=\emptyset$, we call $\mathcal{A}$ _transition-based_. In this paper, we
fix a BA $\mathcal{A}=(Q,\delta,I,Q_{F}\cup\delta_{F})$.

##  3 Complementing Büchi automata

In this section, we describe a generalization of the rank-based
complementation of state-based BAs presented by Schewe in [8] to our notion of
transition/state-based BAs.

###  3.1 Run DAGs

First, we recall the terminology from [8] (which is a minor modification of
the one in [10]), which we use in the paper. Let the _run DAG_ of
$\mathcal{A}$ over a word $\alpha$ be a DAG (directed acyclic graph)
$\mathcal{G}_{\alpha}=(V,E)$ containing vertices $V$ and edges $E$ such that

  * •

$V\subseteq Q\times\omega$ s.t. $(q,i)\in V$ iff there is a run $\rho$ of
$\mathcal{A}$ from $I$ over $\alpha$ with $\rho_{i}=q$,

  * •

$E\subseteq V\times V$ s.t. $((q,i),(q^{\prime},i^{\prime}))\in E$ iff
$i^{\prime}=i+1$ and $q^{\prime}\in\delta(q,\alpha_{i})$.

Given $\mathcal{G}_{\alpha}$ as above, we will write
$(p,i)\in\mathcal{G}_{\alpha}$ to denote that $(p,i)\in V$. A vertex $(p,i)\in
V$ is called _accepting_ if $p$ is an accepting state and an edge
$((q,i),(q^{\prime},i^{\prime}))\in E$ is called _accepting_ if
$q\overset{\alpha_{i}}{\rightarrow}q^{\prime}$ is an accepting transition. A
vertex $v\in\mathcal{G}_{\alpha}$ is _finite_ if the set of vertices reachable
from $v$ is finite, _infinite_ if it is not finite, and _endangered_ if it
cannot reach an accepting vertex or an accepting edge.

We assign ranks to vertices of run DAGs as follows: Let
$\mathcal{G}_{\alpha}^{0}=\mathcal{G}_{\alpha}$ and $j=0$. Repeat the
following steps until the fixpoint or for at most $2n+1$ steps, where $n=|Q|$.

  * •

Set $\mathit{rank}_{\alpha}(v)\leftarrow j$ for all finite vertices $v$ of
$\mathcal{G}_{\alpha}^{j}$ and let $\mathcal{G}_{\alpha}^{j+1}$ be
$\mathcal{G}_{\alpha}^{j}$ minus the vertices with the rank $j$.

  * •

Set $\mathit{rank}_{\alpha}(v)\leftarrow j+1$ for all endangered vertices $v$
of $\mathcal{G}_{\alpha}^{j+1}$ and let $\mathcal{G}_{\alpha}^{j+2}$ be
$\mathcal{G}_{\alpha}^{j+1}$ minus the vertices with the rank $j+1$.

  * •

Set $j\leftarrow j+2$.

For all vertices $v$ that have not been assigned a rank yet, we assign
$\mathit{rank}_{\alpha}(v)\leftarrow\omega$.

We define the _rank of $\alpha$_, denoted as $\mathit{rank}(\alpha)$, as
$\max\\{\mathit{rank}_{\alpha}(v)\mid v\in\mathcal{G}_{\alpha}\\}$ and the
_rank of $\mathcal{A}$_, denoted as $\mathit{rank}(\mathcal{A})$, as
$\max\\{\mathit{rank}(w)\mid
w\in\Sigma^{\omega}\setminus\mathcal{L}(\mathcal{A})\\}$.

######  Lemma 1 ()

If $\alpha\notin\mathcal{L}(\mathcal{A})$, then $\mathit{rank}(\alpha)\leq
2|Q|$.

###  3.2 Rank-Based Complementation

In this section, we describe a construction for complementing BAs developed in
the work of Kupferman and Vardi [10]—later improved by Friedgut, Kupferman,
and Vardi [11], and by Schewe [8]—extended to our definition of BAs with
accepting states and transitions (see [19] for a step-by-step introduction).
The construction is based on the notion of tight level rankings storing
information about levels in run DAGs. For a BA $\mathcal{A}$ and $n=|Q|$, a
_(level) ranking_ is a function $f\colon Q\to[2n]$ such that
$f(Q_{F})\subseteq\\{0,2,\ldots,2n\\}$, i.e., $f$ assigns even ranks to
accepting states of $\mathcal{A}$. For two rankings $f$ and $f^{\prime}$ we
define $f\leavevmode\hbox to13.12pt{\vbox
to6.12pt{\pgfpicture\makeatletter\hbox{\hskip 2.32pt\lower-3.0613pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\pgfsys@setlinewidth{0.6pt}\pgfsys@invoke{ } {}{{}}{} {{}{}}{}{}{{
{\pgfsys@beginscope
\pgfsys@setdash{}{0.0pt}\pgfsys@roundcap\pgfsys@roundjoin{} {}{}{} {}{}{}
\pgfsys@moveto{-2.32pt}{2.76129pt}\pgfsys@curveto{-1.89615pt}{1.10449pt}{-0.95163pt}{0.32214pt}{0.0pt}{0.0pt}\pgfsys@curveto{-0.95163pt}{-0.32214pt}{-1.89615pt}{-1.10449pt}{-2.32pt}{-2.76129pt}\pgfsys@stroke\pgfsys@endscope}}
}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{9.89995pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{10.19995pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}
{}{{}}{}{{{}}{}{}{}{}{}{}{}{}}{}\pgfsys@moveto{4.19998pt}{0.0pt}\pgfsys@moveto{6.30968pt}{0.0pt}\pgfsys@curveto{6.30968pt}{1.16516pt}{5.36514pt}{2.1097pt}{4.19998pt}{2.1097pt}\pgfsys@curveto{3.03482pt}{2.1097pt}{2.09029pt}{1.16516pt}{2.09029pt}{0.0pt}\pgfsys@curveto{2.09029pt}{-1.16516pt}{3.03482pt}{-2.1097pt}{4.19998pt}{-2.1097pt}\pgfsys@curveto{5.36514pt}{-2.1097pt}{6.30968pt}{-1.16516pt}{6.30968pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{4.19998pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}_{S}^{a}f^{\prime}$
iff for each $q\in S$ and $q^{\prime}\in\delta(q,a)$ we have
$f^{\prime}(q^{\prime})\leq f(q)$ and for each
$q^{\prime\prime}\in\delta_{F}(q,a)$ it holds
$f^{\prime}(q^{\prime\prime})\leq\lfloor\\!\\!\lfloor
f(q)\rfloor\\!\\!\rfloor$. The set of all rankings is denoted by
$\mathcal{R}$. For a ranking $f$, the _rank_ of $f$ is defined as
$\mathit{rank}(f)=\max\\{f(q)\mid q\in Q\\}$. We use $f\leq f^{\prime}$ iff
for every state $q\in Q$ we have $f(q)\leq f^{\prime}(q)$ and we use
$f<f^{\prime}$ iff $f\leq f^{\prime}$ and there is a state $q\in Q$ with
$f(q)<f^{\prime}(q)$. For a set of states $S\subseteq Q$, we call $f$ to be
$S$-_tight_ if  (i) it has an odd rank $r$,  (ii)
$f(S)\supseteq\\{1,3,\ldots,r\\}$, and  (iii) $f(Q\setminus S)=\\{0\\}$.  A
ranking is _tight_ if it is $Q$-tight; we use $\mathcal{T}$ to denote the set
of all tight rankings.

The original rank-based construction [10] uses macrostates of the form
$(S,O,f)$ to track all runs of $\mathcal{A}$ over $\alpha$. The $f$-component
contains guesses of the ranks of states in $S$ (which is obtained by the
classical subset construction) in the run DAG and the $O$-set is used to check
whether all runs contain only a finite number of accepting states. Friedgut,
Kupferman, and Vardi [11] improved the construction by having $f$ consider
only tight rankings. Schewe’s construction [8] extends the macrostates to
$(S,O,f,i)$ with $i\in\omega$ representing a particular even rank such that
$O$ tracks states with rank $i$. At the cut-point (a macrostate with
$O=\emptyset$) the value of $i$ is changed to $i+2$ modulo the rank of $f$.
Macrostates in an accepting run hence iterate over all possible values of $i$.
Formally, the complement of $\mathcal{A}=(Q,\delta,I,Q_{F}\cup\delta_{F})$ is
given as the (state-based) BA
$\textsc{Schewe}(\mathcal{A})=(Q^{\prime},\delta^{\prime},I^{\prime},Q_{F}^{\prime}\cup\emptyset)$,
whose components are defined as follows:

  * •

$Q^{\prime}=Q_{1}\cup Q_{2}$ where

    * –

$Q_{1}=2^{Q}$ and

    * –

$Q_{2}=\begin{array}[t]{ll}\\{(S,O,f,i)\in&2^{Q}\times
2^{Q}\times\mathcal{T}\times\\{0,2,\ldots,2n-2\\}\mid f\text{ is
$S$-tight},\\\ &O\subseteq S\cap f^{-1}(i)\\},\end{array}$

  * •

$I^{\prime}=\\{I\\}$,

  * •

$\delta^{\prime}=\delta_{1}\cup\delta_{2}\cup\delta_{3}$ where

    * –

$\delta_{1}\colon Q_{1}\times\Sigma\to 2^{Q_{1}}$ such that
$\delta_{1}(S,a)=\\{\delta(S,a)\\}$,

    * –

$\delta_{2}\colon Q_{1}\times\Sigma\to 2^{Q_{2}}$ such that
$\delta_{2}(S,a)=\\{(S^{\prime},\emptyset,f,0)\mid
S^{\prime}=\delta(S,a),\linebreak f\text{ is }S^{\prime}\text{-tight}\\}$, and

    * –

$\delta_{3}\colon Q_{2}\times\Sigma\to 2^{Q_{2}}$ such that
$(S^{\prime},O^{\prime},f^{\prime},i^{\prime})\in\delta_{3}((S,O,f,i),a)$ iff

      * *

$S^{\prime}=\delta(S,a)$,

      * *

$f\leavevmode\hbox to11.1pt{\vbox
to6.12pt{\pgfpicture\makeatletter\hbox{\hskip 0.3pt\lower-3.0613pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\pgfsys@setlinewidth{0.6pt}\pgfsys@invoke{ } {}{{}}{}
{{}{}}{}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{9.89995pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{10.19995pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}
{}{{}}{}{{{}}{}{}{}{}{}{}{}{}}{}\pgfsys@moveto{4.19998pt}{0.0pt}\pgfsys@moveto{6.30968pt}{0.0pt}\pgfsys@curveto{6.30968pt}{1.16516pt}{5.36514pt}{2.1097pt}{4.19998pt}{2.1097pt}\pgfsys@curveto{3.03482pt}{2.1097pt}{2.09029pt}{1.16516pt}{2.09029pt}{0.0pt}\pgfsys@curveto{2.09029pt}{-1.16516pt}{3.03482pt}{-2.1097pt}{4.19998pt}{-2.1097pt}\pgfsys@curveto{5.36514pt}{-2.1097pt}{6.30968pt}{-1.16516pt}{6.30968pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{4.19998pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}_{S}^{a}f^{\prime}$,

      * *

$\mathit{rank}(f)=\mathit{rank}(f^{\prime})$,

      * *

and

        * $\circ$

if $O=\emptyset$ then $i^{\prime}=(i+2)\mod(\mathit{rank}(f^{\prime})+1)$ and
$O^{\prime}=f^{\prime-1}(i^{\prime})$, and

        * $\circ$

if $O\neq\emptyset$ then $i^{\prime}=i$ and $O^{\prime}=\delta(O,a)\cap
f^{\prime-1}(i)$; and

  * •

$Q_{F}^{\prime}=\\{\emptyset\\}\cup((2^{Q}\times\\{\emptyset\\}\times\mathcal{T}\times\omega)\cap
Q_{2})$.

We call the part of the automaton with states from $Q_{1}$ the _waiting_ part
(denoted as Waiting), and the part corresponding to $Q_{2}$ the _tight_ part
(denoted as Tight).

######  Theorem 3.1 ()

Let $\mathcal{A}$ be a BA. Then
$\mathcal{L}(\textsc{Schewe}(\mathcal{A}))=\Sigma^{\omega}\setminus\mathcal{L}(\mathcal{A})$.

The space complexity of Schewe’s construction for BAs matches the theoretical
lower bound $\mathcal{O}((0.76n)^{n})$ given by Yan [7] modulo a quadratic
factor $\mathcal{O}(n^{2})$. Note that our extension to BAs with accepting
transitions does not increase the space complexity of the construction.

$r$$s$$t$$b$$b$$b$$a$$a$$a$

(a) BA $\mathcal{A}$ over $\\{a,b\\}$

$\\{r\\}$$\\{r,s,t\\}$$\\{s,t\\}$$\emptyset$$\big{(}\\{r{:}3,s{:}0,t{:}1\\},\emptyset\big{)}$$\big{(}\\{r{:}3,s{:}2,t{:}1\\},\emptyset\big{)}$$\big{(}\\{r{:}1,s{:}2,t{:}3\\},\emptyset\big{)}$$\big{(}\\{r{:}1,s{:}0,t{:}0\\},\emptyset\big{)}$$\big{(}\\{r{:}1,s{:}0,t{:}1\\},\emptyset\big{)}$$\big{(}\\{r{:}1\\},\emptyset\big{)}$$\big{(}\\{r{:}1,s{:}0,t{:}0\\},\\{r,s\\}\big{)}$$\big{(}\\{s{:}0,t{:}1\\},\emptyset\big{)}$$b$$b$$b$$b$$b$$b$$a$$a$$b$$a$$a$$a$$b$$a,b$$b$$b$$b$$b$

(b) A part of $\textsc{Schewe}(\mathcal{A})$

Figure 1: Schewe’s complementation

Example 3.2. Consider the BA $\mathcal{A}$ over $\\{a,b\\}$ given in Fig.
1(a). A part of $\textsc{Schewe}(\mathcal{A})$ is shown in Fig. 1(b) (we use
$(\\{s{:}0,t{:}1\\},\emptyset)$ to denote the macrostate
$(\\{s,t\\},\emptyset,\\{s\mapsto 0,t\mapsto 1\\},0)$). We omit the $i$-part
of each macrostate since the corresponding values are 0 for all macrostates in
the figure. Useless states are covered by grey stripes. The full automaton
contains even more transitions from $\\{r\\}$ to useless macrostates of the
form $(\\{r{:}\cdot,s{:}\cdot,t{:}\cdot\\},\emptyset)$. ∎

From the construction of $\textsc{Schewe}(\mathcal{A})$, we can see that the
number of states is affected mainly by sizes of macrostates and by the maximum
rank of $\mathcal{A}$. In particular, the upper bound on the number of states
of the complement with the maximum rank $r$ is given in the following lemma.

######  Lemma 2 ()

For a BA $\mathcal{A}$ with sufficiently many states $n$ such that
$\mathit{rank}(\mathcal{A})=r$ the number of states of the complemented
automaton is bounded by $2^{n}+\frac{(r+m)^{n}}{(r+m)!}$ where
$m=\max\\{0,3-\lceil\frac{r}{2}\rceil\\}$.

From Lemma 1 we have that the rank of $\mathcal{A}$ is bounded by $2|Q|$. Such
a bound is often too coarse and hence $\textsc{Schewe}(\mathcal{A})$ may
contain many redundant states. Decreasing the bound on the ranks is essential
for a practical algorithm, but an optimal solution is PSpace-complete [12].
The rest of this paper therefore proposes a framework of lightweight
techniques for decreasing the maximum rank bound and, in this way,
significantly reducing the size of the complemented BA.

###  3.3 Tight Rank Upper Bounds

Let $\alpha\notin\mathcal{L}(\mathcal{A})$. For $\ell\in\omega$, we define the
$\ell$-th _level_ of $\mathcal{G}_{\alpha}$ as
$\mathit{level}_{\alpha}(\ell)=\\{q\mid(q,\ell)\in\mathcal{G}_{\alpha}\\}$.
Furthermore, we use $f^{\alpha}_{\ell}$ to denote the ranking of level $\ell$
of $\mathcal{G}_{\alpha}$. Formally,

$f^{\alpha}_{\ell}(q)=\begin{cases}\mathit{rank}_{\alpha}((q,\ell))&\text{if
}q\in\mathit{level}_{\alpha}(\ell),\\\ 0&\text{otherwise.}\end{cases}$ (1)

We say that a level $\ell$ is _tight in $\mathcal{G}_{\alpha}$_ if for all
$k\geq\ell$ it holds that  (i) $f^{\alpha}_{k}$is tight, and  (ii)
$\mathit{rank}(f^{\alpha}_{k})=\mathit{rank}(f^{\alpha}_{\ell})$.  Let
$\rho=S_{0}S_{1}\dots S_{\ell-1}(S_{\ell},O_{\ell},f_{\ell},i_{\ell})\dots$ be
a run on a word $\alpha$ in $\textsc{Schewe}(\mathcal{A})$. We say that $\rho$
is a _super-tight run_ [13] if $f_{k}=f^{\alpha}_{k}$ for each $k\geq\ell$.
Finally, we say that a mapping $\mu\colon 2^{Q}\to\mathcal{R}$ is a  _tight
rank upper bound (TRUB) wrt $\alpha$_ iff

$\exists\ell\in\omega\colon\mathit{level}_{\alpha}(\ell)\text{ is
tight}\land(\forall k\geq\ell\colon\mu(\mathit{level}_{\alpha}(k))\geq
f^{\alpha}_{k}).$ (2)

Informally, a TRUB is a ranking that gives a conservative (i.e., larger)
estimate on the necessary ranks of states in a super-tight run. We say that
$\mu$ is a TRUB iff $\mu$ is a TRUB wrt all
$\alpha\notin\mathcal{L}(\mathcal{A})$. We abuse notation and use the term
TRUB also for a mapping $\mu^{\prime}\colon 2^{Q}\to\omega$ if the mapping
$\mathit{inner}(\mu^{\prime})$ is a TRUB where
$\mathit{inner}(\mu^{\prime})(S)=\\{q\mapsto m\mid
m=\mu^{\prime}(S)\mathbin{\text{\ooalign{\raise
4.30554pt\hbox{.}\cr$-$\cr}}}1\text{ if }q\in Q_{F}\text{ else
}m=\mu^{\prime}(S)\\}$ for all $S\in 2^{Q}$. ($\mathbin{\text{\ooalign{\raise
4.30554pt\hbox{.}\cr$-$\cr}}}$ is the _monus_ operator, i.e., minus with
negative results saturated to zero.) Note that the mappings
$\mu_{t}=\\{S\mapsto(2|S\setminus Q_{F}|\mathbin{\text{\ooalign{\raise
4.30554pt\hbox{.}\cr$-$\cr}}}1)\\}_{S\in 2^{Q}}$ and $\mathit{inner}(\mu_{t})$
are trivial TRUBs.

The following lemma shows that we can remove from
$\textsc{Schewe}(\mathcal{A})$ macrostates whose ranking is not covered by a
TRUB (in particular, we show that the reduced automaton preserves super-tight
runs).

######  Lemma 3 ()

Let $\mu$ be a TRUB and $\mathcal{B}$ be a BA obtained from
$\textsc{Schewe}(\mathcal{A})$ by replacing all occurrences of $Q_{2}$ by
$Q_{2}^{\prime}=\\{(S,O,f,i)\mid f\leq\mu(S)\\}$. Then,
$\mathcal{L}(\mathcal{B})=\Sigma^{\omega}\setminus\mathcal{L}(\mathcal{A})$.

##  4 Elevator Automata

In this section, we introduce _elevator automata_ , which are BAs having a
particular structure that can be exploited for complementation and semi-
determinization; elevator automata can be complemented in
$\mathcal{O}(16^{n})$ space instead of $2^{\mathcal{O}(n\log n)}$, which is
the lower bound for unrestricted BAs, and semi-determinized in
$\mathcal{O}(2^{n})$ instead of $\mathcal{O}(4^{n})$ (see Appendix 0.A for the
semi-determinization). The class of elevator automata is quite general: it can
be seen as a substantial generalization of semi-deterministic BAs (SDBAs) [15,
20]. Intuitively, an elevator automaton is a BA whose strongly connected
components are all either deterministic or inherently weak.

Let $\mathcal{A}=(Q,\delta,I,Q_{F}\cup\delta_{F})$. $C\subseteq Q$ is a
_strongly connected component_ (SCC) of $\mathcal{A}$ if for any pair of
states $q,q^{\prime}\in C$ it holds that $q$ is reachable from $q^{\prime}$
and $q^{\prime}$ is reachable from $q$. $C$ is _maximal_ (MSCC) if it is not a
proper subset of another SCC. An MSCC $C$ is _trivial_ iff $|C|=1$ and
$\delta\raisebox{-2.15277pt}{$|$}_{C}=\emptyset$. The  _condensation_ of
$\mathcal{A}$ is the DAG
$\mathit{cond}(\mathcal{A})=(\mathcal{M},\mathcal{E})$ where $\mathcal{M}$ is
the set of $\mathcal{A}$’s MSCCs and $\mathcal{E}=\\{(C_{1},C_{2})\mid\exists
q_{1}\in C_{1},\exists q_{2}\in C_{2},\exists a\in\Sigma\colon
q_{1}\overset{a}{\rightarrow}q_{2}\in\delta\\}$. An MSCC is _non-accepting_ if
it contains no accepting state and no accepting transition, i.e., $C\cap
Q_{F}=\emptyset$ and
$\delta\raisebox{-2.15277pt}{$|$}_{C}\cap\delta_{F}=\emptyset$. The _depth_ of
$(\mathcal{M},\mathcal{E})$ is defined as the number of MSCCs on the longest
path in $(\mathcal{M},\mathcal{E})$.

We say that an SCC $C$ is _inherently weak accepting_ (IWA) iff _every cycle_
in the transition diagram of $\mathcal{A}$ restricted to $C$ contains an
accepting state or an accepting transition. $C$ is _inherently weak_ if it is
either non-accepting or IWA, and $\mathcal{A}$ is inherently weak if all of
its MSCCs are inherently weak. $\mathcal{A}$ is _deterministic_ iff $|I|\leq
1$ and $|\delta(q,a)|\leq 1$ for all $q\in Q$ and $a\in\Sigma$. An SCC
$C\subseteq Q$ is _deterministic_ iff
$(C,\delta\raisebox{-2.15277pt}{$|$}_{C},\emptyset,\emptyset)$ is
deterministic. $\mathcal{A}$ is a  _semi-deterministic BA_ (SDBA) if
$\mathcal{A}[q]$ is deterministic for every $q\in Q_{F}\cup\\{p\in Q\mid
s\overset{a}{\rightarrow}p\in\delta_{F},s\in Q,a\in\Sigma\\}$, i.e., whenever
a run in $\mathcal{A}$ reaches an accepting state or an accepting transition,
it can only continue deterministically.

$0$$1$$2$$3$$4$$5$$\neg a$$a$$\neg a$$a$$\neg b$$b$$\neg b$$b$$\neg c$$c$$\neg
c$$c$$\neg a\wedge b$$\neg a\wedge b$$\neg b\wedge c$$\neg b\wedge c$$\neg
a\wedge\neg b\wedge c$$\neg a\wedge\neg b\wedge c$_det_ _det_ _det_

Figure 2: The BA for LTL formula
$\mathsf{G}\mathsf{F}(a\vee\mathsf{G}\mathsf{F}(b\vee\mathsf{G}\mathsf{F}c))$
is elevator

$\mathcal{A}$ is an _elevator (Büchi) automaton_ iff for every MSCC $C$ of
$\mathcal{A}$ it holds that $C$ is  (i) deterministic,  (ii) IWA, or  (iii)
non-accepting.  In other words, a BA is an elevator automaton iff every
nondeterministic SCC of $\mathcal{A}$ that contains an accepting state or
transition is inherently weak. An example of an elevator automaton obtained
from the LTL formula
$\mathsf{G}\mathsf{F}(a\vee\mathsf{G}\mathsf{F}(b\vee\mathsf{G}\mathsf{F}c))$
is shown in Fig. 2. The BA consists of three connected deterministic
components. Note that the automaton is neither semi-deterministic nor
unambiguous.

The rank of an elevator automaton $\mathcal{A}$ does not depend on the number
of states (as in general BAs), but only on the number of MSCCs and the depth
of $\mathit{cond}(\mathcal{A})$. In the worst case, $\mathcal{A}$ consists of
a chain of deterministic components, yielding the upper bound on the rank of
elevator automata given in the following lemma.

######  Lemma 4 ()

Let $\mathcal{A}$ be an elevator automaton such that its condensation has the
depth $d$. Then $\mathit{rank}(\mathcal{A})\leq 2d$.

###  4.1 Refined Ranks for Elevator Automata

Notice that the upper bound on ranks provided by Lemma 4 can still be too
coarse. For instance, for an SDBA with three linearly ordered MSCCs such that
the first two MSCCs are non-accepting and the last one is deterministic
accepting, the lemma gives us an upper bound on the rank $6$, while it is
known that every SDBA has the rank at most $3$ (cf. [20]). Another examples
might be two deterministic non-trivial MSCCs connected by a path of trivial
MSCCs, which can be assigned the same rank.

Instead of refining the definition of elevator automata into some quite
complex list of constraints, we rather provide an algorithm that performs a
traversal through $\mathit{cond}(\mathcal{A})$ and assigns each MSCC a label
of the form _type_ :_rank_ that contains  (i) a type and  (ii) a bound on the
maximum rank of states in the component.  The types of MSCCs that we consider
are the following:

$\mathsf{T}$:

_trivial_ components,

$\mathsf{IWA}$:

_inherently weak accepting_ components,

$\mathsf{D}$:

_deterministic_ (potentially accepting) components, and

$\mathsf{N}$:

_non-accepting_ components.

Note that the type in an MSCC is not given _a priori_ but is determined by the
algorithm (this is because for deterministic non-accepting components, it is
sometimes better to treated them as $\mathsf{D}$ and sometimes as
$\mathsf{N}$, depending on their neighbourhood). In the following, we assume
that $\mathcal{A}$ is an elevator automaton without useless states and,
moreover, all accepting conditions on states and transitions not inside non-
trivial MSCCs are removed (any BA can be easily transformed into this form).

We start with terminal MSCCs $C$, i.e., MSCCs that cannot reach any other
MSCC:

  1. T1:

If $C$ is IWA, then we label it with $\mathsf{IWA}$:0.

  2. T2:

Else if $C$ is deterministic accepting, we label it with $\mathsf{D}$:2.

$\mathsf{IWA}{:}\ell$$\ell=\max\\{\ell_{D},\ell_{N}+1,\ell_{W}\\}$$C\colon$$\mathsf{D}{:}\ell_{D}$$\mathsf{N}{:}\ell_{N}$$\mathsf{IWA}{:}\ell_{W}$

(a) $C$ is $\mathsf{IWA}$

$\mathsf{D}{:}\ell$$\ell=\max\\{\ell_{D}+\leavevmode\hbox to8.08pt{\vbox
to8.08pt{\pgfpicture\makeatletter\hbox{\hskip 10.01283pt\lower-2.04889pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{
{}{{}}{{}}{{}}{{}}{}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.8,0.4,0}\pgfsys@color@rgb@fill{0.8}{0.4}{0}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.8,0.4,0}\pgfsys@color@rgb@stroke{0.8}{0.4}{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.8,0.4,0}\pgfsys@color@rgb@fill{0.8}{0.4}{0}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.8,0.4,0}\pgfsys@color@rgb@stroke{0.8}{0.4}{0}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.13168pt}{1.99168pt}\pgfsys@curveto{-2.13168pt}{4.1128pt}{-3.85115pt}{5.83226pt}{-5.97226pt}{5.83226pt}\pgfsys@curveto{-8.09337pt}{5.83226pt}{-9.81284pt}{4.1128pt}{-9.81284pt}{1.99168pt}\pgfsys@curveto{-9.81284pt}{-0.12943pt}{-8.09337pt}{-1.84889pt}{-5.97226pt}{-1.84889pt}\pgfsys@curveto{-3.85115pt}{-1.84889pt}{-2.13168pt}{-0.12943pt}{-2.13168pt}{1.99168pt}\pgfsys@closepath\pgfsys@moveto{-5.97226pt}{1.99168pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.7}{0.0}{0.0}{0.7}{-7.72224pt}{-0.26385pt}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@invoke{
}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{1,1,1}\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}$2$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} }
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}},\ell_{N}+1,\ell_{W}+\leavevmode\hbox
to8.08pt{\vbox
to8.08pt{\pgfpicture\makeatletter\hbox{\hskip-1.93167pt\lower-2.04889pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{
{}{{}}{{}}{{}}{{}}{}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0,0,0.8}\pgfsys@color@rgb@fill{0}{0}{0.8}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0.8}\pgfsys@color@rgb@stroke{0}{0}{0.8}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0,0,0.8}\pgfsys@color@rgb@fill{0}{0}{0.8}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0.8}\pgfsys@color@rgb@stroke{0}{0}{0.8}\pgfsys@invoke{
}{}\pgfsys@moveto{9.81282pt}{1.99168pt}\pgfsys@curveto{9.81282pt}{4.1128pt}{8.09335pt}{5.83226pt}{5.97224pt}{5.83226pt}\pgfsys@curveto{3.85114pt}{5.83226pt}{2.13167pt}{4.1128pt}{2.13167pt}{1.99168pt}\pgfsys@curveto{2.13167pt}{-0.12943pt}{3.85114pt}{-1.84889pt}{5.97224pt}{-1.84889pt}\pgfsys@curveto{8.09335pt}{-1.84889pt}{9.81282pt}{-0.12943pt}{9.81282pt}{1.99168pt}\pgfsys@closepath\pgfsys@moveto{5.97224pt}{1.99168pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.7}{0.0}{0.0}{0.7}{4.22226pt}{-0.26385pt}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@invoke{
}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{1,1,1}\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}$2$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} }
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}},2\\}$$C\colon$$\mathsf{D}{:}\ell_{D}$$2$$\mathsf{N}{:}\ell_{N}$$\mathsf{IWA}{:}\ell_{W}$$2$

(b) $C$ is $\mathsf{D}$

$\mathsf{N}{:}\ell$$\ell=\max\\{\ell_{D}+1,\ell_{N},\ell_{W}+1\\}$$C\colon$$\mathsf{D}{:}\ell_{D}$$\mathsf{N}{:}\ell_{N}$$\mathsf{IWA}{:}\ell_{W}$

(c) $C$ is $\mathsf{N}$

Figure 3: Rules for assigning types and rank bounds to MSCCs. The symbols $2$
and $2$ are interpeted as $0$ if all the corresponding edges from the
components having rank $\ell_{D}$ and $\ell_{W}$, respectively, are
deterministic; otherwise they are interpreted as $2$. Transitions between two
components $C_{1}$ and $C_{2}$ are deterministic if the BA
$(C,\delta\raisebox{-1.93748pt}{$|$}_{C},\emptyset,\emptyset)$ is
deterministic for $C=\delta(C_{1},\Sigma)\cap(C_{1}\cup C_{2})$.

$t{:}\ell$$C\colon$$\mathsf{D}{:}\ell_{D}$$\mathsf{N}{:}\ell_{N}$$\mathsf{IWA}{:}\ell_{W}$

Figure 4: Structure of elevator ranking rules

(Note that the previous two options are complete due to our requirements on
the structure of $\mathcal{A}$.) When all terminal MSCCs are labelled, we
proceed through $\mathit{cond}(\mathcal{A})$, inductively on its structure,
and label non-terminal components $C$ based on the rules defined below.

$\\{r\\}$$\\{r,s,t\\}$$\\{s,t\\}$$\emptyset$$\big{(}\\{r{:}3,s{:}0,t{:}1\\},\emptyset\big{)}$$\big{(}\\{r{:}3,s{:}2,t{:}1\\},\emptyset\big{)}$$\big{(}\\{r{:}1,s{:}2,t{:}3\\},\emptyset\big{)}$$\big{(}\\{r{:}1,s{:}0,t{:}0\\},\emptyset\big{)}$$\big{(}\\{r{:}1,s{:}0,t{:}1\\},\emptyset\big{)}$$\big{(}\\{r{:}1\\},\emptyset\big{)}$$\big{(}\\{r{:}1,s{:}0,t{:}0\\},\\{r,s\\}\big{)}$$\big{(}\\{s{:}0,t{:}1\\},\emptyset\big{)}$$b$$b$$b$$b$$b$$b$$a$$a$$b$$a$$a$$a$$b$$a,b$$b$$b$$b$$b$

Figure 5: A part of $\textsc{Schewe}(\mathcal{A})$. The TRUB computed by
elevator rules is used to prune states outside the yellow area.

The rules are of the form that uses the structure depicted in Fig. 4, where
children nodes denote already processed MSCCs. In particular, a child node of
the form $k$:$\ell_{k}$ denotes an aggregate node of _all_ siblings of the
type $k$ with $\ell_{k}$ being the maximum rank of these siblings. Moreover,
we use $\mathrm{typemax}\\{e_{D},e_{N},e_{W}\\}$ to denote the type
$j\in\\{\mathsf{D,N,IWA}\\}$ for which $e_{j}=\max\\{e_{D},e_{N},e_{W}\\}$
where $e_{i}$ is an expression containing $\ell_{i}$ (if there are more such
types, $j$ is chosen arbitrarily). The rules for assigning a type $t$ and a
rank $\ell$ to $C$ are the following:

  1. I1:

If $C$ is trivial, we set $t=\mathrm{typemax}\\{\ell_{D},\ell_{N},\ell_{W}\\}$
and $\ell=\max\\{\ell_{D},\ell_{N},\ell_{W}\\}$.

  2. I2:

Else if $C$ is IWA, we use the rule in Fig. 3(a).

  3. I3:

Else if $C$ is deterministic accepting, we use the rule in Fig. 3(b).

  4. I4:

Else if $C$ is deterministic and non-accepting, we try both rules from Figs.
3(b) and 3(c) and pick the rule that gives us a smaller rank.

  5. I5:

Else if $C$ is nondeterministic and non-accepting, we use the rule in Fig.
3(c).

Then, for every MSCC $C$ of $\mathcal{A}$, we assign each of its states the
rank of $C$. We use $\chi\colon Q\to\omega$ to denote the rank bounds computed
by the procedure above.

######  Lemma 5 ()

$\chi$ is a TRUB.

Using Lemma 3, we can now use $\chi$ to prune states during the construction
of $\textsc{Schewe}(\mathcal{A})$, as shown in the following example.

Example 4.1. As an example, consider the BA $\mathcal{A}$ in Fig. 1(a). The
set of MSCCs with their types is given as
$\\{\\{q\\}{:}\mathsf{N},\\{s,t\\}{:}\mathsf{IWA}\\}$ showing that BA
$\mathcal{A}$ is an elevator. Using the rules T1 and I4 we get the TRUB
$\chi=\\{q{:}1,s{:}0,t{:}0\\}$. The TRUB can be used to prune the generated
states as shown in Fig. 5. ∎

###  4.2 Efficient Complementation of Elevator Automata

In Section 4.1 we proposed an algorithm for assigning ranks to MSCCs of an
elevator automaton $\mathcal{A}$. The drawback of the algorithm is that the
maximum obtained rank is not bounded by a constant but by the depth of the
condensation of $\mathcal{A}$. We will, however, show that it is actually
possible to change $\mathcal{A}$ by at most doubling the number of states and
obtain an elevator BA with the rank at most 3.

Intuitively, the construction copies every non-trivial MSCC $C$ with an
accepting state or transition into a component $C^{\bullet}$, copies all
transitions going into states in $C$ to also go into the corresponding states
in $C^{\bullet}$, and, finally, removes all accepting conditions from $C$.
Formally, let $\mathcal{A}=(Q,\delta,I,Q_{F}\cup\delta_{F})$ be a BA. For
$C\subseteq Q$, we use $C^{\bullet}$ to denote a unique copy of $C$, i.e.,
$C^{\bullet}=\\{q^{\bullet}\mid q\in C\\}$ s.t. $C^{\bullet}\cap Q=\emptyset$.
Let $\mathcal{M}$ be the set of MSCCs of $\mathcal{A}$. Then, the _deelevated_
BA
$\textsc{DeElev}(\mathcal{A})=(Q^{\prime},\delta^{\prime},I^{\prime},Q_{F}^{\prime}\cup\delta_{F}^{\prime})$
is given as follows:

  * •

$Q^{\prime}=Q\cup Q^{\bullet}$,

  * •

$\delta^{\prime}:Q^{\prime}\times\Sigma\to 2^{Q^{\prime}}$ where for $q\in Q$

    * –

$\delta^{\prime}(q,a)=\delta(q,a)\cup(\delta(q,a))^{\bullet}$ and

    * –

$\delta^{\prime}(q^{\bullet},a)=(\delta(q,a)\cap C)^{\bullet}$ for $q\in
C\in\mathcal{M}$;

  * •

$I^{\prime}=I$, and

  * •

$Q_{F}^{\prime}=Q_{F}^{\bullet}$ and
$\delta_{F}^{\prime}=\\{q^{\bullet}\overset{a}{\rightarrow}r^{\bullet}\mid
q\overset{a}{\rightarrow}r\in\delta_{F}\\}\cap\delta^{\prime}$.

It is easy to see that the number of states of the deelevated automaton is
bounded by $2|Q|$. Moreover, if $\mathcal{A}$ is elevator, so is
$\textsc{DeElev}(\mathcal{A})$. The construction preserves the language of
$\mathcal{A}$, as shown by the following lemma.

######  Lemma 6 ()

Let $\mathcal{A}$ be a BA. Then,
$\mathcal{L}(\mathcal{A})=\mathcal{L}(\textsc{DeElev}(\mathcal{A}))$.

Moreover, for an elevator automaton $\mathcal{A}$, the structure of
$\textsc{DeElev}(\mathcal{A})$ consists of (after trimming useless states)
several non-accepting MSCCs with copied terminal deterministic or IWA MSCCs.
Therefore, if we apply the algorithm from Section 4.1 on
$\textsc{DeElev}(\mathcal{A})$, we get that its rank is bounded by $3$, which
gives the following upper bound for complementation of elevator automata.

######  Lemma 7 ()

Let $\mathcal{A}$ be an elevator automaton with suffficiently many states $n$.
Then the language $\Sigma^{\omega}\setminus\mathcal{L}(\mathcal{A})$ can be
represented by a BA with at most $\mathcal{O}(16^{n})$ states.

The complementation through $\textsc{DeElev}(\mathcal{A})$ gives a better
upper bound than the rank refinement from Section 4.1 applied directly on
$\mathcal{A}$, however, based on our experience, complementation through
$\textsc{DeElev}(\mathcal{A})$ behaves worse in many real-world instances.
This poor behaviour is caused by the fact that the complement of
$\textsc{DeElev}(\mathcal{A})$ can have a larger Waiting and macrostates in
Tight can have larger $S$-components, which can yield more generated states
(despite the rank bound 3). It seems that the most promising approach would to
be a combination of the approaches, which we leave for future work.

###  4.3 Refined Ranks for Non-Elevator Automata

The algorithm from Section 4.1 computing a TRUB for elevator automata can be
extended to compute TRUBs even for general non-elevator automata (i.e., BAs
with nondeterministic accepting components that are not inherently weak). To
achieve this generalization, we extend the rules for assigning types and ranks
to MSCCs of elevator automata from Section 4.1 to take into account general
non-deterministic components. For this, we add into our collection of MSCC
types _general_ components (denoted as $\mathsf{G}$). Further, we need to
extend the rules for terminal components with the following rule:

  1. T3:

Otherwise, we label $C$ with $\mathsf{G}$:$2|C\setminus Q_{F}|$.

$\mathsf{IWA}{:}\ell$$\ell=\max\\{\ell_{D},\ell_{N}+1,\ell_{W},\ell_{G}\\}$$C\colon$$\mathsf{D}{:}\ell_{D}$$\mathsf{N}{:}\ell_{N}$$\mathsf{IWA}{:}\ell_{W}$$\mathsf{G}{:}\ell_{G}$

(a) $C$ is $\mathsf{IWA}$

$\mathsf{D}{:}\ell$$\ell=\max\\{\ell_{D}+\leavevmode\hbox to8.08pt{\vbox
to8.08pt{\pgfpicture\makeatletter\hbox{\hskip 10.01283pt\lower-2.04889pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{
{}{{}}{{}}{{}}{{}}{}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.8,0.4,0}\pgfsys@color@rgb@fill{0.8}{0.4}{0}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.8,0.4,0}\pgfsys@color@rgb@stroke{0.8}{0.4}{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.8,0.4,0}\pgfsys@color@rgb@fill{0.8}{0.4}{0}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.8,0.4,0}\pgfsys@color@rgb@stroke{0.8}{0.4}{0}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.13168pt}{1.99168pt}\pgfsys@curveto{-2.13168pt}{4.1128pt}{-3.85115pt}{5.83226pt}{-5.97226pt}{5.83226pt}\pgfsys@curveto{-8.09337pt}{5.83226pt}{-9.81284pt}{4.1128pt}{-9.81284pt}{1.99168pt}\pgfsys@curveto{-9.81284pt}{-0.12943pt}{-8.09337pt}{-1.84889pt}{-5.97226pt}{-1.84889pt}\pgfsys@curveto{-3.85115pt}{-1.84889pt}{-2.13168pt}{-0.12943pt}{-2.13168pt}{1.99168pt}\pgfsys@closepath\pgfsys@moveto{-5.97226pt}{1.99168pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.7}{0.0}{0.0}{0.7}{-7.72224pt}{-0.26385pt}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@invoke{
}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{1,1,1}\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}$2$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} }
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}},\ell_{N}+1,\ell_{W}+\leavevmode\hbox
to8.08pt{\vbox
to8.08pt{\pgfpicture\makeatletter\hbox{\hskip-1.93167pt\lower-2.04889pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{
{}{{}}{{}}{{}}{{}}{}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0,0,0.8}\pgfsys@color@rgb@fill{0}{0}{0.8}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0.8}\pgfsys@color@rgb@stroke{0}{0}{0.8}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0,0,0.8}\pgfsys@color@rgb@fill{0}{0}{0.8}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0.8}\pgfsys@color@rgb@stroke{0}{0}{0.8}\pgfsys@invoke{
}{}\pgfsys@moveto{9.81282pt}{1.99168pt}\pgfsys@curveto{9.81282pt}{4.1128pt}{8.09335pt}{5.83226pt}{5.97224pt}{5.83226pt}\pgfsys@curveto{3.85114pt}{5.83226pt}{2.13167pt}{4.1128pt}{2.13167pt}{1.99168pt}\pgfsys@curveto{2.13167pt}{-0.12943pt}{3.85114pt}{-1.84889pt}{5.97224pt}{-1.84889pt}\pgfsys@curveto{8.09335pt}{-1.84889pt}{9.81282pt}{-0.12943pt}{9.81282pt}{1.99168pt}\pgfsys@closepath\pgfsys@moveto{5.97224pt}{1.99168pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.7}{0.0}{0.0}{0.7}{4.22226pt}{-0.26385pt}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@invoke{
}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{1,1,1}\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}$2$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} }
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}},\ell_{G}+2,2\\}$$C\colon$$\mathsf{D}{:}\ell_{D}$$2$$\mathsf{N}{:}\ell_{N}$$\mathsf{IWA}{:}\ell_{W}$$2$$\mathsf{G}{:}\ell_{G}$

(b) $C$ is $\mathsf{D}$

$\mathsf{N}{:}\ell$$\ell=\max\\{\ell_{D}+1,\ell_{N},\ell_{W}+1,\ell_{G}+1\\}$$C\colon$$\mathsf{D}{:}\ell_{D}$$\mathsf{N}{:}\ell_{N}$$\mathsf{IWA}{:}\ell_{W}$$\mathsf{G}{:}\ell_{G}$

(c) $C$ is $\mathsf{N}$

Figure 6: Rules assigning types and rank bounds for non-elevator automata.

$\mathsf{G}{:}\ell$$\ell=\max\\{\ell_{D},\ell_{N}+1,\ell_{W},\ell_{G}\\}+2|C\setminus
Q_{F}|$$C\colon$$\mathsf{D}{:}\ell_{D}$$\mathsf{N}{:}\ell_{N}$$\mathsf{IWA}{:}\ell_{W}$$\mathsf{G}{:}\ell_{G}$

Figure 7: $C$ is $\mathsf{G}$

Moreover, we adjust the rules for assigning a type $t$ and a rank $\ell$ to
$C$ to the following (the rule I1 is the same as for the case of elevator
automata):

  1. I2–I5:

_(We replace the corresponding rules for their counterparts including general
components from Fig. 6)._

  2. I6:

Otherwise, we use the rule in Fig. 7.

Then, for every MSCC $C$ of a BA $\mathcal{A}$, we assign each of its states
the rank of $C$. Again, we use $\chi\colon Q\to\omega$ to denote the rank
bounds computed by the adjusted procedure above.

######  Lemma 8 ()

$\chi$ is a TRUB.

##  5 Rank Propagation

$\mu^{\prime}(S)$$\mu(R_{1})$$a_{1}$$\mu(R_{2})$$a_{2}$$\cdots$$\mu(R_{m})$$a_{m}$

Figure 8: Rank propagation flow

In the previous section, we proposed a way, how to obtain a TRUB for elevator
automata (with generalization to general automata). In this section, we
propose a way of using the structure of $\mathcal{A}$ to refine a TRUB using a
propagation of values and thus reduce the size of Tight. Our approach uses
_data flow analysis_ [21] to reason on how ranks and rankings of macrostates
of $\textsc{Schewe}(\mathcal{A})$ can be decreased based on the ranks and
rankings of the _local neighbourhood_ of the macrostates. We, in particular,
use a special case of _forward analysis_ working on the _skeleton_ of
$\textsc{Schewe}(\mathcal{A})$, which is defined as the BA
$\mathcal{K}_{\mathcal{A}}=(2^{Q},\delta^{\prime},\emptyset,\emptyset)$ where
$\delta^{\prime}=\\{R\overset{a}{\rightarrow}S\mid S=\delta(R,a)\\}$ (note
that we are only interested in the structure of $\mathcal{K}_{\mathcal{A}}$
and not its language; also notice the similarity of
$\mathcal{K}_{\mathcal{A}}$ with Waiting). Our analysis refines a rank/ranking
estimate $\mu(S)$ for a macrostate $S$ of $\mathcal{K}_{\mathcal{A}}$ based on
the estimates for its predecessors $R_{1},\ldots,R_{m}$ (see Fig. 8). The new
estimate is denoted as $\mu^{\prime}(S)$.

More precisely, $\mu\colon 2^{Q}\to\mathbb{V}$ is a function giving each
macrostate of $\mathcal{K}_{\mathcal{A}}$ a value from the domain
$\mathbb{V}$. We will use the following two value domains:  (i)
$\mathbb{V}=\omega$, which is used for estimating _ranks_ of macrostates (in
the _outer macrostate analysis_) and  (ii) $\mathbb{V}=\mathcal{R}$, which is
used for estimating _rankings_ within macrostates (in the _inner macrostate
analysis_).  For each of the analyses, we will give the _update function_
$\mathit{up}\colon(2^{Q}\to\mathbb{V})\times(2^{Q})^{m+1}\to\mathbb{V}$, which
defines how the value of $\mu(S)$ is updated based on the values of
$\mu(R_{1}),\ldots,\mu(R_{m})$. We then construct a system with the following
equation for every $S\in 2^{Q}$:

$\mu(S)=\mathit{up}(\mu,S,R_{1},\ldots,R_{m})\quad\text{where
}\\{R_{1},\ldots,R_{m}\\}=\delta^{\prime-1}(S,\Sigma).$ (3)

We then solve the system of equations using standard algorithms for data flow
analysis (see, e.g., [21, Chapter 2]) to obtain the fixpoint $\mu^{*}$. Our
analyses have the important property that if they start with $\mu_{0}$ being a
TRUB, then $\mu^{*}$ will also be a TRUB.

As the initial TRUB, we can use a trivial TRUB or any other TRUB (e.g., the
output of elevator state analysis from Section 4).

###  5.1 Outer Macrostate Analysis

We start with the simpler analysis, which is the _outer macrostate analysis_ ,
which only looks at sizes of macrostates. Recall that the rank $r$ of every
super-tight run in $\textsc{Schewe}(\mathcal{A})$ does not change, i.e., a
super tight run stays in Waiting as long as needed so that when it jumps to
Tight, it takes the rank $r$ and never needs to decrease it. We can use this
fact to decrease the maximum rank of a macrostate $S$ in
$\mathcal{K}_{\mathcal{A}}$. In particular, let us consider all cycles going
through $S$. For each of the cycles $c$, we can bound the maximum rank of a
super-tight run going through $c$ by $2m-1$ where $m$ is the smallest number
of non-accepting states occurring in any macrostate on $c$ (from the
definition, the rank of a tight ranking does not depend on accepting states).
Then we can infer that the maximum rank of any super-tight run going through
$S$ is bounded by the maximum rank of any of the cycles going through $S$
(since $S$ can never assume a higher rank in any super-tight run). Moreover,
the rank of each cycle can also be estimated in a more precise way, e.g. using
our elevator analysis.

Since the number of cycles in $\mathcal{K}_{\mathcal{A}}$ can be
large222$\mathcal{K}_{\mathcal{A}}$ can be exponentially larger than
$\mathcal{A}$ and the number of cycles in $\mathcal{K}_{\mathcal{A}}$ can be
exponential to the size of $\mathcal{K}_{\mathcal{A}}$, so the total number of
cycles can be double-exponential. , instead of their enumeration, we employ
data flow analysis with the value domain $\mathbb{V}=\omega$ (i.e, for every
macrostate $S$ of $\mathcal{K}_{\mathcal{A}}$, we remember a bound on the
maximum rank of $S$) and the following update function:

$\mathit{up}_{\mathit{out}}(\mu,S,R_{1},\ldots,R_{m})=\min\\{\mu(S),\max\\{\mu(R_{1}),\ldots,\mu(R_{m})\\}\\}.$
(4)

Intuitively, the new bound on the maximum rank of $S$ is taken as the smaller
of the previous bound $\mu(S)$ and the largest of the bounds of all
predecessors of $S$, and the new value is propagated forward by the data flow
analysis.

$p$$q$$r$$s$$a$$a$$a$$\bullet$$a$$a$$a$$\bullet$ (a)
$\mathcal{A}_{\mathit{ex}}$

$\\{p\\}$${:}1$$\\{p,q\\}$${:}3$$\\{p,q,r,s\\}$${:}7$$a$$a$$a$ (b) $\mu_{0}$

$\\{p\\}$${:}1$$\\{p,q\\}$${:}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}$$\\{p,q,r,s\\}$${:}7$$a$$a$$a$
(c) $\mu_{\mathit{out}}^{*}$

Figure 9: Example of outer macrostate analysis. (9(a))
$\mathcal{A}_{\mathit{ex}}$ ($\bullet$ denotes accepting transitions). The
initial TRUB $\mu_{0}$ in (9(b)) is refined to $\mu_{\mathit{out}}^{*}$ in
(9(c)).

Example 5.1. Consider the BA $\mathcal{A}_{\mathit{ex}}$ in Fig. 9(a). When
started from the initial TRUB $\mu_{0}=\\{\\{p\\}\mapsto 1,\\{p,q\\}\mapsto
3$, $\\{p,q,r,s\\}\mapsto 7\\}$ (Fig. 9(b)), outer macrostate analysis
decreases the maximum rank estimate for $\\{p,q\\}$ to 1, since
$\min\\{\mu_{0}(\\{p,q\\},\max\\{\mu_{0}(\\{p\\})\\}\\}=\min\\{3,1\\}=1$. The
estimate for $\\{p,q,r,s\\}$ is not affected, because
$\min\\{7,\max\\{1,7\\}\\}=7$ (Fig. 9(c)). ∎

######  Lemma 9 ()

If $\mu$ is a TRUB, then
$\mu\lhd\\{S\mapsto\mathit{up}_{\mathit{out}}(\mu,S,R_{1},\ldots,R_{m})\\}$ is
a TRUB.

######  Corollary 1 ()

When started with a TRUB $\mu_{0}$, the outer macrostate analysis terminates
and returns a TRUB $\mu_{\mathit{out}}^{*}$.

###  5.2 Inner Macrostate Analysis

Our second analysis, called _inner macrostate analysis_ , looks deeper into
super-tight runs in $\textsc{Schewe}(\mathcal{A})$. In particular, compared
with the outer macrostate analysis from the previous section—which only looks
at the _ranks_ , i.e., the bounds on the numbers in the rankings—, inner
macrostate analysis looks at how the _rankings_ assign concrete values to the
_states_ of $\mathcal{A}$ _inside the macrostates_.

Inner macrostate analysis is based on the following. Let $\rho$ be a super-
tight run of $\textsc{Schewe}(\mathcal{A})$ on
$\alpha\notin\mathcal{L}(\mathcal{A})$ and $(S,O,f,i)$ be a macrostate from
Tight. Because $\rho$ is super-tight, we know that the rank $f(q)$ of a state
$q\in S$ is bounded by the ranks of the predecessors of $q$. This holds
because in super-tight runs, the ranks are only _as high as necessary_ ; if
the rank of $q$ were higher than the ranks of its predecessors, this would
mean that we may wait in Waiting longer and only jump to $q$ with a lower rank
later.

Let us introduce some necessary notation. Let $f,f^{\prime}\in\mathcal{R}$ be
rankings (i.e., $f,f^{\prime}\colon Q\to\omega$). We use $f\sqcup f^{\prime}$
to denote the ranking $\\{q\mapsto\max\\{f(q),f^{\prime}(q)\\}\mid q\in Q\\}$,
and $f\sqcap f^{\prime}$ to denote the ranking
$\\{q\mapsto\min\\{f(q),f^{\prime}(q)\\}\mid q\in Q\\}$. Moreover, we define
$\textit{max-succ-rank}_{S}^{a}(f)=\max_{\leq}\\{f^{\prime}\in\mathcal{R}\mid
f\leavevmode\hbox to11.1pt{\vbox to6.12pt{\pgfpicture\makeatletter\hbox{\hskip
0.3pt\lower-3.0613pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\hbox to0.0pt{\hbox to0.0pt{\hbox
to0.0pt{\hbox to0.0pt{ {}{ {}{}{}}{{{ {}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{
{}{}{}}}}{ {}{}{}}{{{ {}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{
{}{}{}}{{{ {}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@stroke@opacity{0.1}\pgfsys@invoke{
}\pgfsys@fill@opacity{0.1}\pgfsys@invoke{ }{{}{}\pgfsys@beginscope{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@setlinewidth{3.0pt}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{8.0pt}{8.0pt}\pgfsys@stroke
\pgfsys@endscope\pgfsys@endscope{{}}{{}}{{}}{{}}}\pgfsys@invoke{
\lxSVG@closescope \lxSVG@closescope }{-0.17365}{0.98482}{0.0pt}{0.0pt}{
\lxSVG@closescope \lxSVG@closescope
}{0}\definecolor[named]{pgf@tempcolor}{rgb}{0,0,0}\pgfsys@invoke{\lxSVG@setpatternuncolored@{21}{0}{0}{0}
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@stroke@opacity{0.1}\pgfsys@invoke{
}\pgfsys@fill@opacity{0.1}\pgfsys@invoke{
}\definecolor[named]{pgf@tempcolor}{rgb}{0,0,0}\pgfsys@invoke{\lxSVG@setpatternuncolored@{21}{0}{0}{0}
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{-33.3043pt}{34.70076pt}\pgfsys@lineto{-75.95824pt}{34.70076pt}\pgfsys@curveto{-80.37657pt}{34.70076pt}{-83.95824pt}{31.1191pt}{-83.95824pt}{26.70076pt}\pgfsys@lineto{-83.95824pt}{-14.70033pt}\pgfsys@curveto{-83.95824pt}{-19.11867pt}{-80.37657pt}{-22.70033pt}{-75.95824pt}{-22.70033pt}\pgfsys@lineto{-33.3043pt}{-22.70033pt}\pgfsys@curveto{-28.88597pt}{-22.70033pt}{-25.3043pt}{-19.11867pt}{-25.3043pt}{-14.70033pt}\pgfsys@lineto{-25.3043pt}{26.70076pt}\pgfsys@curveto{-25.3043pt}{31.1191pt}{-28.88597pt}{34.70076pt}{-33.3043pt}{34.70076pt}\pgfsys@closepath\pgfsys@moveto{-83.95824pt}{-22.70033pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-78.95824pt}{6.00021pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{\minipage[t]{48.65395pt}\endminipage}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{ {}{}{}}{{{
{}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@stroke@opacity{0.1}\pgfsys@invoke{
}\pgfsys@fill@opacity{0.1}\pgfsys@invoke{
}\definecolor[named]{pgf@tempcolor}{rgb}{0,0,0}\pgfsys@invoke{\lxSVG@setpatternuncolored@{21}{0}{0}{0}
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@stroke@opacity{0.1}\pgfsys@invoke{
}\pgfsys@fill@opacity{0.1}\pgfsys@invoke{
}\definecolor[named]{pgf@tempcolor}{rgb}{0,0,0}\pgfsys@invoke{\lxSVG@setpatternuncolored@{21}{0}{0}{0}
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{118.65771pt}{-20.03073pt}\pgfsys@lineto{86.21097pt}{-20.03073pt}\pgfsys@curveto{81.79263pt}{-20.03073pt}{78.21097pt}{-23.6124pt}{78.21097pt}{-28.03073pt}\pgfsys@lineto{78.21097pt}{-33.431pt}\pgfsys@curveto{78.21097pt}{-37.84933pt}{81.79263pt}{-41.431pt}{86.21097pt}{-41.431pt}\pgfsys@lineto{118.65771pt}{-41.431pt}\pgfsys@curveto{123.07605pt}{-41.431pt}{126.65771pt}{-37.84933pt}{126.65771pt}{-33.431pt}\pgfsys@lineto{126.65771pt}{-28.03073pt}\pgfsys@curveto{126.65771pt}{-23.6124pt}{123.07605pt}{-20.03073pt}{118.65771pt}{-20.03073pt}\pgfsys@closepath\pgfsys@moveto{78.21097pt}{-41.431pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{83.21097pt}{-30.73087pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{\minipage[t]{38.44675pt}\endminipage}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \hss}
{}{{}}{{{{}}}}{{{{}}}}{{{{}}}}{{{{}}}}{{}}{{{{}}}}{{{{}}}}{{{{}}}}{{{{}}}}{}
{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{3.0pt,3.0pt}{0.0pt}\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{1,0.875,0.875}\pgfsys@color@rgb@fill{1}{0.875}{0.875}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{3.0pt,3.0pt}{0.0pt}\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{1,0.875,0.875}\pgfsys@color@rgb@fill{1}{0.875}{0.875}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{72.40164pt}{32.33197pt}\pgfsys@lineto{-15.79614pt}{32.33197pt}\pgfsys@curveto{-20.21448pt}{32.33197pt}{-23.79614pt}{28.7503pt}{-23.79614pt}{24.33197pt}\pgfsys@lineto{-23.79614pt}{-7.26031pt}\pgfsys@curveto{-23.79614pt}{-11.67865pt}{-20.21448pt}{-15.26031pt}{-15.79614pt}{-15.26031pt}\pgfsys@lineto{72.40164pt}{-15.26031pt}\pgfsys@curveto{76.81998pt}{-15.26031pt}{80.40164pt}{-11.67865pt}{80.40164pt}{-7.26031pt}\pgfsys@lineto{80.40164pt}{24.33197pt}\pgfsys@curveto{80.40164pt}{28.7503pt}{76.81998pt}{32.33197pt}{72.40164pt}{32.33197pt}\pgfsys@closepath\pgfsys@moveto{-23.79614pt}{-15.26031pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-8.79614pt}{8.53583pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{\minipage[t]{74.1978pt}\endminipage} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{}{{}}{{{{}}}}{{{{}}}}{{{{}}}}{{{{}}}}{{}}{{{{}}}}{{{{}}}}{{{{}}}}{{{{}}}}{}
{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{3.0pt,3.0pt}{0.0pt}\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{1,0.875,0.875}\pgfsys@color@rgb@fill{1}{0.875}{0.875}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{3.0pt,3.0pt}{0.0pt}\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{1,0.875,0.875}\pgfsys@color@rgb@fill{1}{0.875}{0.875}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{72.40164pt}{-32.82484pt}\pgfsys@lineto{-15.79614pt}{-32.82484pt}\pgfsys@curveto{-20.21448pt}{-32.82484pt}{-23.79614pt}{-36.40651pt}{-23.79614pt}{-40.82484pt}\pgfsys@lineto{-23.79614pt}{-72.41713pt}\pgfsys@curveto{-23.79614pt}{-76.83546pt}{-20.21448pt}{-80.41713pt}{-15.79614pt}{-80.41713pt}\pgfsys@lineto{72.40164pt}{-80.41713pt}\pgfsys@curveto{76.81998pt}{-80.41713pt}{80.40164pt}{-76.83546pt}{80.40164pt}{-72.41713pt}\pgfsys@lineto{80.40164pt}{-40.82484pt}\pgfsys@curveto{80.40164pt}{-36.40651pt}{76.81998pt}{-32.82484pt}{72.40164pt}{-32.82484pt}\pgfsys@closepath\pgfsys@moveto{-23.79614pt}{-80.41713pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-8.79614pt}{-56.62099pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{\minipage[t]{74.1978pt}\endminipage} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{}{{}}{{{{}}}}{{{{}}}}{{{{}}}}{{{{}}}}{{}}{{{{}}}}{{{{}}}}{{{{}}}}{{{{}}}}{}
{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{3.0pt,3.0pt}{0.0pt}\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{1,0.875,0.875}\pgfsys@color@rgb@fill{1}{0.875}{0.875}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{3.0pt,3.0pt}{0.0pt}\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{1,0.875,0.875}\pgfsys@color@rgb@fill{1}{0.875}{0.875}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{72.40164pt}{-92.86017pt}\pgfsys@lineto{-15.79614pt}{-92.86017pt}\pgfsys@curveto{-20.21448pt}{-92.86017pt}{-23.79614pt}{-96.44183pt}{-23.79614pt}{-100.86017pt}\pgfsys@lineto{-23.79614pt}{-132.45245pt}\pgfsys@curveto{-23.79614pt}{-136.87079pt}{-20.21448pt}{-140.45245pt}{-15.79614pt}{-140.45245pt}\pgfsys@lineto{72.40164pt}{-140.45245pt}\pgfsys@curveto{76.81998pt}{-140.45245pt}{80.40164pt}{-136.87079pt}{80.40164pt}{-132.45245pt}\pgfsys@lineto{80.40164pt}{-100.86017pt}\pgfsys@curveto{80.40164pt}{-96.44183pt}{76.81998pt}{-92.86017pt}{72.40164pt}{-92.86017pt}\pgfsys@closepath\pgfsys@moveto{-23.79614pt}{-140.45245pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-8.79614pt}{-116.65631pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{\minipage[t]{74.1978pt}\endminipage} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\hss} {}{ {}{}{}}{{{}}{{}}}{}{{}}{}{ {}{}{}}{{{}}{{}}}{}{}{}{
{}}{{{}}{{}}{{}}}{}{}{}{{}{}{}}{{{}}{{}}}{}{}{}{ {}{}{}}{{{}}{{}}{{}}}{}{}{}{
{}}{{{}}{{}}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{3.0pt,3.0pt}{0.0pt}\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{1,1,0.8}\pgfsys@color@cmyk@fill{0}{0}{0.2}{0}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{-31.15569pt}{-30.72968pt}\pgfsys@lineto{-31.15569pt}{45.6111pt}\pgfsys@curveto{-31.15569pt}{48.37256pt}{-28.91714pt}{50.6111pt}{-26.15569pt}{50.6111pt}\pgfsys@lineto{37.68066pt}{50.6111pt}\pgfsys@curveto{40.44212pt}{50.6111pt}{44.9192pt}{50.6111pt}{47.68066pt}{50.6111pt}\pgfsys@lineto{94.22546pt}{50.6111pt}\pgfsys@curveto{96.98692pt}{50.6111pt}{99.22546pt}{48.37256pt}{99.22546pt}{45.6111pt}\pgfsys@lineto{99.22546pt}{-5.04164pt}\pgfsys@curveto{99.22546pt}{-7.8031pt}{96.98692pt}{-10.04164pt}{94.22546pt}{-10.04164pt}\pgfsys@lineto{36.15569pt}{-10.04164pt}\pgfsys@curveto{33.39423pt}{-10.04164pt}{31.15569pt}{-12.28018pt}{31.15569pt}{-15.04164pt}\pgfsys@lineto{31.15569pt}{-25.72968pt}\pgfsys@curveto{31.15569pt}{-28.49113pt}{31.15569pt}{-32.96822pt}{31.15569pt}{-35.72968pt}\pgfsys@lineto{31.15569pt}{-84.17421pt}\pgfsys@curveto{31.15569pt}{-86.93567pt}{28.91714pt}{-89.17421pt}{26.15569pt}{-89.17421pt}\pgfsys@lineto{-0.12154pt}{-89.17421pt}\pgfsys@curveto{-2.883pt}{-89.17421pt}{-7.36008pt}{-89.17421pt}{-10.12154pt}{-89.17421pt}\pgfsys@lineto{-26.15569pt}{-89.17421pt}\pgfsys@curveto{-28.91714pt}{-89.17421pt}{-31.15569pt}{-86.93567pt}{-31.15569pt}{-84.17421pt}\pgfsys@lineto{-31.15569pt}{-25.02954pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss} {}{ {}{}{}}{{{
{}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{ {}{}{}}{{{
{}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{ {}{}{}}{{{
{}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@stroke@opacity{0.1}\pgfsys@invoke{
}\pgfsys@fill@opacity{0.1}\pgfsys@invoke{
}\definecolor[named]{pgf@tempcolor}{rgb}{0,0,0}\pgfsys@invoke{\lxSVG@setpatternuncolored@{21}{0}{0}{0}
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@stroke@opacity{0.1}\pgfsys@invoke{
}\pgfsys@fill@opacity{0.1}\pgfsys@invoke{
}\definecolor[named]{pgf@tempcolor}{rgb}{0,0,0}\pgfsys@invoke{\lxSVG@setpatternuncolored@{21}{0}{0}{0}
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{-33.3043pt}{34.70076pt}\pgfsys@lineto{-75.95824pt}{34.70076pt}\pgfsys@curveto{-80.37657pt}{34.70076pt}{-83.95824pt}{31.1191pt}{-83.95824pt}{26.70076pt}\pgfsys@lineto{-83.95824pt}{-14.70033pt}\pgfsys@curveto{-83.95824pt}{-19.11867pt}{-80.37657pt}{-22.70033pt}{-75.95824pt}{-22.70033pt}\pgfsys@lineto{-33.3043pt}{-22.70033pt}\pgfsys@curveto{-28.88597pt}{-22.70033pt}{-25.3043pt}{-19.11867pt}{-25.3043pt}{-14.70033pt}\pgfsys@lineto{-25.3043pt}{26.70076pt}\pgfsys@curveto{-25.3043pt}{31.1191pt}{-28.88597pt}{34.70076pt}{-33.3043pt}{34.70076pt}\pgfsys@closepath\pgfsys@moveto{-83.95824pt}{-22.70033pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-78.95824pt}{6.00021pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{\minipage[t]{48.65395pt}\endminipage}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{ {}{}{}}{{{
{}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@stroke@opacity{0.1}\pgfsys@invoke{
}\pgfsys@fill@opacity{0.1}\pgfsys@invoke{
}\definecolor[named]{pgf@tempcolor}{rgb}{0,0,0}\pgfsys@invoke{\lxSVG@setpatternuncolored@{21}{0}{0}{0}
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@stroke@opacity{0.1}\pgfsys@invoke{
}\pgfsys@fill@opacity{0.1}\pgfsys@invoke{
}\definecolor[named]{pgf@tempcolor}{rgb}{0,0,0}\pgfsys@invoke{\lxSVG@setpatternuncolored@{21}{0}{0}{0}
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{118.65771pt}{-20.03073pt}\pgfsys@lineto{86.21097pt}{-20.03073pt}\pgfsys@curveto{81.79263pt}{-20.03073pt}{78.21097pt}{-23.6124pt}{78.21097pt}{-28.03073pt}\pgfsys@lineto{78.21097pt}{-33.431pt}\pgfsys@curveto{78.21097pt}{-37.84933pt}{81.79263pt}{-41.431pt}{86.21097pt}{-41.431pt}\pgfsys@lineto{118.65771pt}{-41.431pt}\pgfsys@curveto{123.07605pt}{-41.431pt}{126.65771pt}{-37.84933pt}{126.65771pt}{-33.431pt}\pgfsys@lineto{126.65771pt}{-28.03073pt}\pgfsys@curveto{126.65771pt}{-23.6124pt}{123.07605pt}{-20.03073pt}{118.65771pt}{-20.03073pt}\pgfsys@closepath\pgfsys@moveto{78.21097pt}{-41.431pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{83.21097pt}{-30.73087pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{\minipage[t]{38.44675pt}\endminipage}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\hss}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\pgfsys@setlinewidth{0.6pt}\pgfsys@invoke{ } {}{{}}{}
{{}{}}{}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{9.89995pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{10.19995pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}
{}{{}}{}{{{}}{}{}{}{}{}{}{}{}}{}\pgfsys@moveto{4.19998pt}{0.0pt}\pgfsys@moveto{6.30968pt}{0.0pt}\pgfsys@curveto{6.30968pt}{1.16516pt}{5.36514pt}{2.1097pt}{4.19998pt}{2.1097pt}\pgfsys@curveto{3.03482pt}{2.1097pt}{2.09029pt}{1.16516pt}{2.09029pt}{0.0pt}\pgfsys@curveto{2.09029pt}{-1.16516pt}{3.03482pt}{-2.1097pt}{4.19998pt}{-2.1097pt}\pgfsys@curveto{5.36514pt}{-2.1097pt}{6.30968pt}{-1.16516pt}{6.30968pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{4.19998pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}_{S}^{a}f^{\prime}\\}$
and a function $\mathit{dec}\colon\mathcal{R}\to\mathcal{R}$ such that
$\mathit{dec}(\theta)$ is the ranking $\theta^{\prime}$ for which

$\theta^{\prime}(q)=\begin{cases}\theta(q)\mathbin{\text{\ooalign{\raise
4.30554pt\hbox{.}\cr$-$\cr}}}1&\text{if }\theta(q)=\mathit{rank}(\theta)\text{
and }q\notin Q_{F},\\\
\lfloor\\!\\!\lfloor\theta(q)\mathbin{\text{\ooalign{\raise
4.30554pt\hbox{.}\cr$-$\cr}}}1\rfloor\\!\\!\rfloor&\text{if
}\theta(q)=\mathit{rank}(\theta)\text{ and }q\in Q_{F},\\\
\theta(q)&\text{otherwise.}\end{cases}$ (5)

Intuitively, $\textit{max-succ-rank}_{S}^{a}(f)$ is the (pointwise) maximum
ranking that can be reached from macrostate $S$ with ranking $f$ over $a$ (it
is easy to see that there is a unique such maximum ranking) and
$\mathit{dec}(\theta)$ decreases the maximum ranks in a ranking $\theta$ by
one (or by two for even maximum ranks and accepting states).

_$\mathit{up}_{\mathit{in}}(\mu,S,R_{1},\ldots,R_{m})$_ :

2 foreach  _$1\leq i\leq m$ and $a\in\Sigma$_ do

3 if  _$\delta(R_{i},a)=S$_ then

4 $g_{i}^{a}\leftarrow\textit{max-succ-rank}^{a}_{R_{i}}(\mu(R_{i}))$

5 $\theta\leftarrow\mu(S)\sqcap\bigsqcup\\{g_{i}^{a}\mid g_{i}^{a}\text{ is
defined}\\}$;

6 if  _$\mathit{rank}(\theta)$ is even_ then
$\theta\leftarrow\mathit{dec}(\theta)$;

7 return $\theta$;

8

The analysis uses the value domain $\mathbb{V}=\mathcal{R}$ (i.e., each
macrostate of $\mathcal{K}_{\mathcal{A}}$ is assigned a ranking giving an
upper bound on the rank of each state in the macrostate) and the update
function $\mathit{up}_{\mathit{in}}$ given in the right-hand side of the page.
Intuitively, $\mathit{up}_{\mathit{in}}$ updates $\mu(q)$ for every $q\in S$
to hold the maximum rank compatible with the ranks of its predecessors. We
note line Section 5.2, which makes use of the fact that we can only consider
tight rankings (whose rank is odd), so we can decrease the estimate using the
function $\mathit{dec}$ defined above.

$\\{p{:}1,$$q{:}1\\}$$\\{p{:}7,$$q{:}7,$$r{:}7,$$s{:}7\\}$$\\{p{:}6,$$q{:}7,$$r{:}7,$$s{:}7\\}$$\\{p{:}6,$$q{:}6,$$r{:}7,$$s{:}7\\}$$\\{p{:}6,$$q{:}6,$$r{:}6,$$s{:}6\\}$$\\{p{:}5,$$q{:}5,$$r{:}5,$$s{:}5\\}$$\mathit{dec}$

Example 5.2. Let us continue in Fig. 9 and perform inner macrostate analysis
starting with the TRUB
$\\{\\{p{:}1\\},\\{p{:}1,q{:}1\\},\\{p{:}7,q{:}7,r{:}7,s{:}7\\}\\}$ obtained
from $\mu_{\mathit{out}}^{*}$. We show three iterations of the algorithm for
$\\{p,q,r,s\\}$ in the right-hand side (we do not show $\\{p,q\\}$ except the
first iteration since it does not affect intermediate steps). We can notice
that in the three iterations, we could decrease the maximum rank estimate to
$\\{p{:}6,q{:}6,r{:}6,s{:}6\\}$ due to the accepting transitions from $r$ and
$s$. In the last of the three iterations, when all states have the even rank
$6$, the condition on Section 5.2 would become true and the rank of all states
would be decremented to $5$ using $\mathit{dec}$. Then, again, the accepting
transitions from $r$ and $s$ would decrease the rank of $p$ to $4$, which
would be propagated to $q$ and so on. Eventually, we would arrive to the TRUB
$\\{p{:}1,q{:}1,r{:}1,s{:}1\\}$, which could not be decreased any more, since
$\\{p{:}1,q{:}1\\}$ forces the ranks of $r$ and $s$ to stay at 1. ∎

######  Lemma 10 ()

If $\mu$ is a TRUB, then
$\mu\lhd\\{S\mapsto\mathit{up}_{\mathit{in}}(\mu,S,R_{1},\ldots,R_{m})\\}$ is
a TRUB.

######  Corollary 2 ()

When started with a TRUB $\mu_{0}$, the inner macrostate analysis terminates
and returns a TRUB $\mu_{\mathit{in}}^{*}$.

##  6 Experimental Evaluation

#### Used tools and evaluation environment.

We implemented the techniques described in the previous sections as an
extension of the tool Ranker [18] (written in C++). Speaking in the terms of
[13], the heuristics were implemented on top of the
$\textsc{Ranker}_{\textsc{MaxR}}$ configuration (we refer to this previous
version as $\textsc{Ranker}_{\textsc{Old}}$). We tested the correctness of our
implementation using Spot’s autcross on all BAs in our benchmark. We compared
modified Ranker with other state-of-the-art tools, namely, Goal [22]
(implementing Piterman [23], Schewe [8], Safra [24], and Fribourg [25]), Spot
2.9.3 [26] (implementing Redziejowski’s algorithm [27]), Seminator 2 [17],
LTL2dstar 0.5.4 [28], and Roll [29]. All tools were set to the mode where they
output an automaton with the standard state-based Büchi acceptance condition.
The experimental evaluation was performed on a 64-bit GNU/Linux Debian
workstation with an Intel(R) Xeon(R) CPU E5-2620 running at 2.40 GHz with 32
GiB of RAM and using a timeout of 5 minutes.

#### Datasets.

As the source of our benchmark, we use the two following datasets:  (i)
randomcontaining 11,000 BAs over a two letter alphabet used in [30], which
were randomly generated via the Tabakov-Vardi approach [31], starting from 15
states and with various different parameters;  (ii) LTLwith 1,721 BAs over
larger alphabets (up to 128 symbols) used in [17], which were obtained from
LTL formulae from literature (221) or randomly generated (1,500).  We
preprocessed the automata using Rabit [32] and Spot’s autfilt (using the
`--high` simplification level), transformed them to state-based acceptance BAs
(if they were not already), and converted to the HOA format [33]. From this
set, we removed automata that were  (i) semi-deterministic,  (ii) inherently
weak,  (iii) unambiguous, or  (iv) have an empty language,  since for these
automata types there exist more efficient complementation procedures than for
unrestricted BAs [20, 17, 14, 34]. In the end, we were left with 2,592
(random) and 414 (LTL) _hard_ automata. We use all to denote their union
(3,006 BAs). Of these hard automata, 458 were elevator automata.

(a) Ranker vs Schewe

(b) Ranker vs $\textsc{Ranker}_{\textsc{Old}}$

Figure 10: Comparison of the state space generated by our optimizations and
other rank-based procedures (horizontal and vertical dashed lines represent
timeouts). Blue data points are from random and red data points are from LTL.
Axes are logarithmic.

###  6.1 Generated State Space

In our first experiment, we evaluated the effectiveness of our heuristics for
pruning the generated state space by comparing the sizes of complemented BAs
without postprocessing. This use case is directed towards applications where
postprocessing is irrelevant, such as inclusion or equivalence checking of
BAs.

We focused on a comparison with two less optimized versions of the rank-based
complementation procedure: Schewe (the version “Reduced Average Outdegree”
from [8] implemented in Goal under -m rank -tr -ro) and its optimization
$\textsc{Ranker}_{\textsc{Old}}$. The scatter plots in Fig. 10 compare the
numbers of states of automata generated by Ranker and the other algorithms and
the upper part of Table 1 gives summary statistics. Observe that our
optimizations from this paper drastically reduced the generated search space
compared with both Schewe and $\textsc{Ranker}_{\textsc{Old}}$ (the mean for
Schewe is lower than for $\textsc{Ranker}_{\textsc{Old}}$ due to its much
higher number of timeouts); from Fig. 10(b) we can see that the improvement
was in many cases _exponential_ even when compared with our previous
optimizations in $\textsc{Ranker}_{\textsc{Old}}$. The median (which is a more
meaningful indicator with the presence of timeouts) decreased by 44 % w.r.t.
$\textsc{Ranker}_{\textsc{Old}}$, and we also reduced the number of timeouts
by 23 %. Notice that the numbers for the LTL dataset do not differ as much as
for random, witnessing the easier structure of the BAs in LTL.

Table 1: Statistics for our experiments. The upper part compares various
optimizations of the rank-based procedure (no postprocessing). The lower part
compares Ranker to other approaches (with postprocessing). The left-hand side
compares sizes of complement BAs and the right-hand side runtimes of the
tools. The wins and losses columns give the number of times when Ranker was
strictly better and worse. The values are given for the three datasets as “all
(random : LTL)”. Approaches in Goal are labelled with .

method | mean | median | wins | losses | mean runtime [s] | median runtime [s] | timeouts
---|---|---|---|---|---|---|---
Ranker | 3812 | (4452 | : | 207) | 79 | (93 | : | 26) |  |  |  |  |  |  |  |  | 7.83 | (8.99 | : | 1.30) | 0.51 | (0.84 | : | 0.04) | 279 | (276 | : | 3)
$\textsc{Ranker}_{\textsc{Old}}$ | 7398 | (8688 | : | 358) | 141 | (197 | : | 29) | 2190 | (2011 | : | 179) | 111 | (107 | : | 4) | 9.37 | (10.73 | : | 1.99) | 0.61 | (1.04 | : | 0.04) | 365 | (360 | : | 5)
Schewe | 4550 | (5495 | : | 665) | 439 | (774 | : | 35) | 2640 | (2315 | : | 325) | 55 | (1 | : | 54) | 21.05 | (24.28 | : | 7.80) | 6.57 | (7.39 | : | 5.21) | 937 | (928 | : | 9)
Ranker | 47 | (52 | : | 18) | 22 | (27 | : | 10) |  |  |  |  |  |  |  |  | 7.83 | (8.99 | : | 1.30) | 0.51 | (0.84 | : | 0.04) | 279 | (276 | : | 3)
Piterman | 73 | (82 | : | 22) | 28 | (34 | : | 14) | 1435 | (1124 | : | 311) | 416 | (360 | : | 56) | 7.29 | (7.39 | : | 6.65) | 5.99 | (6.04 | : | 5.62) | 14 | (12 | : | 2)
Safra | 83 | (91 | : | 30) | 29 | (35 | : | 17) | 1562 | (1211 | : | 351) | 387 | (350 | : | 37) | 14.11 | (15.05 | : | 8.37) | 6.71 | (6.92 | : | 5.79) | 172 | (158 | : | 14)
Spot | 75 | (85 | : | 15) | 24 | (32 | : | 10) | 1087 | (936 | : | 151) | 683 | (501 | : | 182) | 0.86 | (0.99 | : | 0.06) | 0.02 | (0.02 | : | 0.02) | 13 | (13 | : | 0)
Fribourg | 91 | (104 | : | 13) | 23 | (31 | : | 9) | 1120 | (1055 | : | 65) | 601 | (376 | : | 225) | 17.79 | (19.53 | : | 7.22) | 9.25 | (10.15 | : | 5.48) | 81 | (80 | : | 1)
LTL2dstar | 73 | (82 | : | 21) | 28 | (34 | : | 13) | 1465 | (1195 | : | 270) | 465 | (383 | : | 82) | 3.31 | (3.84 | : | 0.11) | 0.04 | (0.05 | : | 0.02) | 136 | (130 | : | 6)
Seminator 2 | 79 | (91 | : | 15) | 21 | (29 | : | 10) | 1266 | (1131 | : | 135) | 571 | (367 | : | 204) | 9.51 | (11.25 | : | 0.08) | 0.22 | (0.39 | : | 0.02) | 363 | (362 | : | 1)
Roll | 18 | (19 | : | 14) | 10 | (9 | : | 11) | 2116 | (1858 | : | 258) | 569 | (443 | : | 126) | 31.23 | (37.85 | : | 7.28) | 8.19 | (12.23 | : | 2.74) | 1109 | (1106 | : | 3)

###  6.2 Comparison with Other Complementation Techniques

In our second experiment, we compared the improved Ranker with other state-of-
the-art tools. We were comparing sizes of output BAs, therefore, we
postprocessed each output automaton with autfilt (simplification level
`--high`). Scatter plots are given in Fig. 11, where we compare Ranker with
Spot (which had the best results on average from the other tools except Roll)
and Roll, and summary statistics are in the lower part of Table 1. Observe
that Ranker has by far the lowest mean (except Roll) and the third lowest
median (after Seminator 2 and Roll, but with less timeouts). Moreover,
comparing the numbers in columns wins and losses we can see that Ranker gives
strictly better results than other tools (wins) more often than the other way
round (losses).

In Fig. 11(a) see that indeed in the majority of cases Ranker gives a smaller
BA than Spot, especially for harder BAs (Spot, however, behaves slightly
better on the simpler BAs from LTL). The results in Fig. 11(b) do not seem so
clear. Roll uses a learning-based approach—more heavyweight and completely
orthogonal to any of the other tools—and can in some cases output a tiny
automaton, but does not scale, as observed by the number of timeouts much
higher than any other tool. It is, therefore, positively surprising that
Ranker could in most of the cases still obtain a much smaller automaton than
Roll.

Regarding runtimes, the prototype implementation in Ranker is comparable to
Seminator 2, but slower than Spot and LTL2dstar (Spot is the fastest tool).
Implementations of other approaches clearly do not target speed. We note that
the number of timeouts of Ranker is still higher than of some other tools (in
particular Piterman, Spot, Fribourg); further state space reduction targeting
this particular issue is our future work.

##  7 Related Work

BA complementation remains in the interest of researchers since their first
introduction by Büchi in [1]. Together with a hunt for efficient
complementation techniques, the effort has been put into establishing the
lower bound. First, Michel showed that the lower bound is $n!$ (approx.
$(0.36n)^{n}$) [35] and later Yan refined the result to $(0.76n)^{n}$ [7].

The complementation approaches can be roughly divided into several branches.
_Ramsey-based complementation_ , the very first complementation construction,
where the language of an input automaton is decomposed into a finite number of
equivalence classes, was proposed by Büchi and was further enhanced in [36].
_Determinization-based complementation_ was presented by Safra in [24] and
later improved by Piterman in [23] and Redziejowski in [27]. The main idea of
this approach is to convert an input BA into an equivalent deterministic
automaton with different acceptance condition that can be easily complemented
(e.g. Rabin automaton). The complemented automaton is then converted back into
a BA (often for the price of some blow-up). _Slice-based complementation_
tracks the acceptance condition using a reduced abstraction on a run tree [37,
38]. _A learning-based approach_ was introduced in [39, 29]. Allred and Utes-
Nitsche then presented a novel optimal complementation algorithm in [25]. For
some special types of BAs, e.g., deterministic [40], semi-deterministic [20],
or unambiguous [34], there exist specific complementation algorithms. _Semi-
determinization based complementation_ converts an input BA into a semi-
deterministic BA [15], which is then complemented [17].

(a) Ranker vs Spot

(b) Ranker vs Roll

Figure 11: Comparison of the complement size obtained by Ranker and other
state-of-the-art tools (horizontal and vertical dashed lines represent
timeouts). Axes are logarithmic.

_Rank-based complementation_ , studied in [10, 12, 11, 8, 41], extends the
subset construction for determinization of finite automata by storing
additional information in each macrostate to track the acceptance condition of
all runs of the input automaton. Optimizations of an alternative (sub-optimal)
rank-based construction from [10] going through _alternating Büchi automata_
were presented in [12]. Furthermore, the work in [41] introduces an
optimization of Schewe, in some cases producing smaller automata (this
construction is not compatible with our optimizations). As shown in [42], the
rank-based construction can be optimized using simulation relations. We
identified several heuristics that help reducing the size of the complement in
[13], which are compatible with the heuristics in this paper.

## References

  * [1] Büchi, J.R.:  On a decision method in restricted second order arithmetic.  In: Proc. of International Congress on Logic, Method, and Philosophy of Science 1960, Stanford Univ. Press, Stanford (1962)
  * [2] Fogarty, S., Vardi, M.Y.:  Büchi complementation and size-change termination.  In: Proc. of TACAS’09, Springer (2009) 16–30
  * [3] Heizmann, M., Hoenicke, J., Podelski, A.:  Termination analysis by learning terminating programs.  In: Proc. of CAV’14, Springer (2014) 797–813
  * [4] Chen, Y., Heizmann, M., Lengál, O., Li, Y., Tsai, M., Turrini, A., Zhang, L.:  Advanced automata-based algorithms for program termination checking.  In Foster, J.S., Grossman, D., eds.: Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, June 18-22, 2018, ACM (2018) 135–150
  * [5] Oei, R., Ma, D., Schulz, C., Hieronymi, P.:  Pecan: An automated theorem prover for automatic sequences using büchi automata.  CoRR abs/2102.01727 (2021)
  * [6] Sistla, A.P., Vardi, M.Y., Wolper, P.:  The Complementation Problem for Büchi Automata with Applications to Temporal Logic.  Theoretical Computer Science 49(2-3) (1987) 217–237
  * [7] Yan, Q.:  Lower bounds for complementation of $\omega$-automata via the full automata technique.  In Bugliesi, M., Preneel, B., Sassone, V., Wegener, I., eds.: Automata, Languages and Programming, Berlin, Heidelberg, Springer Berlin Heidelberg (2006) 589–600
  * [8] Schewe, S.:  Büchi complementation made tight.  In Albers, S., Marion, J., eds.: 26th International Symposium on Theoretical Aspects of Computer Science, STACS 2009, February 26-28, 2009, Freiburg, Germany, Proceedings. Volume 3 of LIPIcs., Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany (2009) 661–672
  * [9] Allred, J.D., Ultes-Nitsche, U.:  A simple and optimal complementation algorithm for Büchi automata.  In: Proc. of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, ACM (2018) 46–55
  * [10] Kupferman, O., Vardi, M.Y.:  Weak alternating automata are not that weak.  ACM Trans. Comput. Log. 2(3) (2001) 408–429
  * [11] Friedgut, E., Kupferman, O., Vardi, M.:  Büchi complementation made tighter.  International Journal of Foundations of Computer Science 17 (2006) 851–868
  * [12] Gurumurthy, S., Kupferman, O., Somenzi, F., Vardi, M.Y.:  On complementing nondeterministic Büchi automata.  In Geist, D., Tronci, E., eds.: Correct Hardware Design and Verification Methods, 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L’Aquila, Italy, October 21-24, 2003, Proceedings. Volume 2860 of Lecture Notes in Computer Science., Springer (2003) 96–110
  * [13] Havlena, V., Lengál, O.:  Reducing (To) the Ranks: Efficient Rank-Based Büchi Automata Complementation.  In: 32nd International Conference on Concurrency Theory (CONCUR 2021). Volume 203 of Leibniz International Proceedings in Informatics (LIPIcs)., Dagstuhl, Germany, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) 2:1–2:19 ISSN: 1868-8969.
  * [14] Boigelot, B., Jodogne, S., Wolper, P.:  On the use of weak automata for deciding linear arithmetic with integer and real variables.  In Goré, R., Leitsch, A., Nipkow, T., eds.: Automated Reasoning, First International Joint Conference, IJCAR 2001, Siena, Italy, June 18-23, 2001, Proceedings. Volume 2083 of Lecture Notes in Computer Science., Springer (2001) 611–625
  * [15] Courcoubetis, C., Yannakakis, M.:  Verifying temporal properties of finite-state probabilistic programs.  In: 29th Annual Symposium on Foundations of Computer Science, White Plains, New York, USA, 24-26 October 1988, IEEE Computer Society (1988) 338–345
  * [16] Blahoudek, F., Heizmann, M., Schewe, S., Strejček, J., Tsai, M.H.:  Complementing semi-deterministic büchi automata.  In Chechik, M., Raskin, J.F., eds.: Tools and Algorithms for the Construction and Analysis of Systems, Berlin, Heidelberg, Springer Berlin Heidelberg (2016) 770–787
  * [17] Blahoudek, F., Duret-Lutz, A., Strejček, J.:  Seminator 2 can complement generalized Büchi automata via improved semi-determinization.  In: Proceedings of the 32nd International Conference on Computer-Aided Verification (CAV’20). Volume 12225 of Lecture Notes in Computer Science., Springer (July 2020) 15–27
  * [18] Havlena, V., Lengál, O., Šmahlíková, B.:  Ranker (2021) https://github.com/vhavlena/ba-inclusion.
  * [19] Havlena, V., Lengál, O.:  Reducing (to) the ranks: Efficient rank-based Büchi automata complementation (technical report).  Technical report (2021) https://arxiv.org/abs/2010.07834.
  * [20] Blahoudek, F., Heizmann, M., Schewe, S., Strejček, J., Tsai, M.:  Complementing semi-deterministic Büchi automata.  In Chechik, M., Raskin, J., eds.: Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings. Volume 9636 of Lecture Notes in Computer Science., Springer (2016) 770–787
  * [21] Nielson, F., Nielson, H.R., Hankin, C.:  Principles of program analysis.  Springer (1999)
  * [22] Tsai, M.H., Tsay, Y.K., Hwang, Y.S.:  GOAL for games, omega-automata, and logics.  In Sharygina, N., Veith, H., eds.: Computer Aided Verification, Berlin, Heidelberg, Springer Berlin Heidelberg (2013) 883–889
  * [23] Piterman, N.:  From nondeterministic Büchi and Streett automata to deterministic parity automata.  In: Proc. of LICS’06, IEEE (2006) 255–264
  * [24] Safra, S.:  On the complexity of $\omega$-automata.  In: Proc. of FOCS’88, IEEE (1988) 319–327
  * [25] Allred, J.D., Ultes-Nitsche, U.:  A simple and optimal complementation algorithm for Büchi automata.  In: Proceedings of the Thirty third Annual IEEE Symposium on Logic in Computer Science (LICS 2018), IEEE Computer Society Press (July 2018) 46–55
  * [26] Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, É., Xu, L.:  Spot 2.0 — a framework for LTL and $\omega$-automata manipulation.  In Artho, C., Legay, A., Peled, D., eds.: Automated Technology for Verification and Analysis, Cham, Springer International Publishing (2016) 122–129
  * [27] Redziejowski, R.R.:  An improved construction of deterministic omega-automaton using derivatives.  Fundam. Informaticae 119(3-4) (2012) 393–406
  * [28] Klein, J., Baier, C.:  On-the-fly stuttering in the construction of deterministic _omega_ -automata.  In Holub, J., Zdárek, J., eds.: Implementation and Application of Automata, 12th International Conference, CIAA 2007, Prague, Czech Republic, July 16-18, 2007, Revised Selected Papers. Volume 4783 of Lecture Notes in Computer Science., Springer (2007) 51–61
  * [29] Li, Y., Sun, X., Turrini, A., Chen, Y., Xu, J.:  ROLL 1.0: $\omega$-regular language learning library.  In Vojnar, T., Zhang, L., eds.: Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part I. Volume 11427 of Lecture Notes in Computer Science., Springer (2019) 365–371
  * [30] Tsai, M.H., Fogarty, S., Vardi, M.Y., Tsay, Y.K.:  State of Büchi complementation.  In Domaratzki, M., Salomaa, K., eds.: Implementation and Application of Automata, Berlin, Heidelberg, Springer Berlin Heidelberg (2011) 261–271
  * [31] Tabakov, D., Vardi, M.Y.:  Experimental evaluation of classical automata constructions.  In: Proc. of LPAR’05, Springer (2005) 396–411
  * [32] Mayr, R., Clemente, L.:  Advanced automata minimization.  In: Proc. of POPL’13. (2013) 63–74
  * [33] 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 Kroening, D., Pasareanu, C.S., eds.: Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I. Volume 9206 of Lecture Notes in Computer Science., Springer (2015) 479–486
  * [34] Li, Y., Vardi, M.Y., Zhang, L.:  On the power of unambiguity in Büchi complementation.  In Raskin, J.F., Bresolin, D., eds.: Proceedings 11th International Symposium on Games, Automata, Logics, and Formal Verification, Brussels, Belgium, September 21-22, 2020. Volume 326 of Electronic Proceedings in Theoretical Computer Science., Open Publishing Association (2020) 182–198
  * [35] Michel, M.:  Complementation is more difficult with automata on infinite words.  CNET, Paris 15 (1988)
  * [36] Breuers, S., Löding, C., Olschewski, J.:  Improved Ramsey-based Büchi complementation.  In: Proc. of FOSSACS’12, Springer (2012) 150–164
  * [37] Vardi, M.Y., Wilke, T.:  Automata: From logics to algorithms.  Logic and Automata 2 (2008) 629–736
  * [38] Kähler, D., Wilke, T.:  Complementation, disambiguation, and determinization of Büchi automata unified.  In: Proc. of ICALP’08, Springer (2008) 724–735
  * [39] Li, Y., Turrini, A., Zhang, L., Schewe, S.:  Learning to complement Büchi automata.  In: Proc. of VMCAI’18, Springer (2018) 313–335
  * [40] Kurshan, R.P.:  Complementing deterministic Büchi automata in polynomial time.  J. Comput. Syst. Sci. 35(1) (1987) 59–71
  * [41] Karmarkar, H., Chakraborty, S.:  On minimal odd rankings for Büchi complementation.  In Liu, Z., Ravn, A.P., eds.: Automated Technology for Verification and Analysis, 7th International Symposium, ATVA 2009, Macao, China, October 14-16, 2009. Proceedings. Volume 5799 of Lecture Notes in Computer Science., Springer (2009) 228–243
  * [42] Chen, Y., Havlena, V., Lengál, O.:  Simulations in rank-based Büchi automata complementation.  In Lin, A.W., ed.: Programming Languages and Systems - 17th Asian Symposium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1-4, 2019, Proceedings. Volume 11893 of Lecture Notes in Computer Science., Springer (2019) 447–467

##  Appendix 0.A Semi-Determinization of Elevator Automata

The deelevation procedure from Section 4.2 also provides a good starting point
for transforming an elevator automaton into an SDBA. For an elevator automaton
$\mathcal{A}$ with no nondeterministic IWA component, the output of
$\textsc{DeElev}(\mathcal{A})$ is already an SDBA. If $\mathcal{A}$, on the
other hand, contains some nondeterministic IWA component, so will
$\textsc{DeElev}(\mathcal{A})$. In such a case, we can determinize each of the
(terminal) IWA components in $\textsc{DeElev}(\mathcal{A})$, which will cause
a blow-up of at most $2^{|Q|}$333Nondeterministic inherently weak BAs are
stricly more expressive than deterministic inherently weak BAs (observed,
e.g., by the $\omega$-regular language $(a+b)^{*}b^{\omega}$ for which no
deterministic BA exists but is recognized by a nondeterministic weak BA). It
is, however, folklore knowledge that inherently weak components can be
determinized by the powerset construction., which would yield an SDBA with at
most $2|Q|+2^{|Q|}$ states (while the standard semi-determinization of [15]
has the upper bound of $4^{|Q|}$).

###### Lemma 11

Let $\mathcal{A}$ be an elevator automaton with $n$ states. Then there exists
an SDBA with $\mathcal{O}(2^{n})$ states with the same language.

##  Appendix 0.B Proofs of Section 3

See 1

###### Proof

This proof is a modification of [10] to BAs with mixed transition/state-based
acceptance condition. We prove by induction that for every $i\geq 0$ there
exists $l_{i}$ such that for all $l\geq l_{i}$, $\mathcal{G}_{\alpha}^{2i}$
contains at most $|Q|-i$ vertices of the form $(q,l)$. The proof for the base
case $i=0$ follows from the definition of $\mathcal{G}_{\alpha}^{0}$, because
all levels $l\geq 0$ have at most $|Q|$ vertices of the form $(q,l)$. Assume
that the hypothesis holds for $i$. We prove it for $i+1$. First, if
$\mathcal{G}_{\alpha}^{2i}$ is finite, then it is clear that
$\mathcal{G}_{\alpha}^{2i+1}$ and $\mathcal{G}_{\alpha}^{2i+2}$ are empty as
well. If $\mathcal{G}_{\alpha}^{2i}$ is not finite, then there must be some
endangered vertex in $\mathcal{G}_{\alpha}^{2i+1}$. Assume, by way of
contradiction, that $\mathcal{G}_{\alpha}^{2i}$ is infinite and no vertex in
$\mathcal{G}_{\alpha}^{2i+1}$ is endangered. Since $\mathcal{G}_{\alpha}^{2i}$
is infinite, $\mathcal{G}_{\alpha}^{2i+1}$ is also infinite and therefore each
vertex in $\mathcal{G}_{\alpha}^{2i+1}$ has at least one successor. Consider
some vertex $(q_{0},l_{0})$ in $\mathcal{G}_{\alpha}^{2i+1}$. Since, by the
assumption, it is not endangered, there exists an accepting vertex
$(q^{\prime}_{0},l^{\prime}_{0})$ reachable from $(q_{0},l_{0})$ or an
accepting edge
$(q^{\prime\prime}_{0},l^{\prime\prime}_{0})\xrightarrow{a}(q^{\prime}_{0},l^{\prime}_{0})$
with both vertices $(q^{\prime\prime}_{0},l^{\prime\prime}_{0})$ and
$(q^{\prime}_{0},l^{\prime}_{0})$ reachable from $(q_{0},l_{0})$. Let
$(q_{1},l_{1})$ be a successor of $(q^{\prime}_{0},l^{\prime}_{0})$. By the
assumption, $(q_{1},l_{1})$ is also not endangered and hence, there exists a
vertex $(q^{\prime}_{1},l^{\prime}_{1})$ that is accepting and reachable from
$(q_{1},l_{1})$ or an accepting edge
$(q^{\prime\prime}_{1},l^{\prime\prime}_{1})\xrightarrow{a}(q^{\prime}_{1},l^{\prime}_{1})$
with both $(q^{\prime\prime}_{1},l^{\prime\prime}_{1})$ and
$(q^{\prime}_{1},l^{\prime}_{1})$ reachable from $(q_{1},l_{1})$. Let
$(q_{2},l_{2})$ be a successor of $(q^{\prime}_{1},l^{\prime}_{1})$. We can
continue similarly and construct an infinite sequence of vertices
$(q_{1},l_{1}),(q^{\prime}_{1},l^{\prime}_{1}),(q_{2},l_{2}),\ldots,(q_{j},l_{j}),(q^{\prime}_{j},l^{\prime}_{j}),(q_{j+1},l_{j+1}),\ldots$
such that $(q_{j+1},l_{j+1})$ is a successor of
$(q^{\prime}_{j},l^{\prime}_{j})$ and $(q^{\prime}_{j},l^{\prime}_{j})$ is an
accepting vertex or there is a path from $(q_{j},l_{j})$ to
$(q^{\prime}_{j},l^{\prime}_{j})$ containing an accepting edge. Such a
sequence corresponds to a path which contains an accepting vertex or an
accepting edge infinitely often, and which is therefore not accepting, which
contradicts the assumption that $\alpha\not\in\mathcal{L}(\mathcal{A})$. Let
$(q,l)$ be an endangered vertex in $\mathcal{G}_{\alpha}^{2i+1}$. Since
$(q,l)$ is in $\mathcal{G}_{\alpha}^{2i+1}$, it is not finite in
$\mathcal{G}_{\alpha}^{2i}$. There are therefore infinitely many vertices
reachable from $(q,l)$ in $\mathcal{G}_{\alpha}^{2i}$. Hence, by König’s
Lemma, $\mathcal{G}_{\alpha}^{2i}$ contains an infinite path
$(q,l),(q_{1},l+1),(q_{2},l+2),\ldots$. For all $k\geq 1$, the vertex
$(q_{k},l+k)$ has infinitely many vertices reachable from it in
$\mathcal{G}_{\alpha}^{2i}$ and thus, it is not finite in
$\mathcal{G}_{\alpha}^{2i}$. Therefore, the path $(q,l),(q_{1},l+1),\ldots$
exists also in $\mathcal{G}_{\alpha}^{2i+1}$. Since $(q,l)$ is endangered, all
the vertices $(q_{k},l+k)$ \- reachable from $(q,l)$ \- are endangered as
well. They are therefore not in $\mathcal{G}_{\alpha}^{2i+2}$. For all $j\geq
l$, the number of vertices of the form $(q,j)$ in
$\mathcal{G}_{\alpha}^{2i+2}$ is strictly smaller than in
$\mathcal{G}_{\alpha}^{2i}$, which, by the induction hypothesis, is $|Q|-i$.
So there are at most $|Q|-(i+1)$ nodes of the form $(q,j)$ in
$\mathcal{G}_{\alpha}^{2i+2}$. It is now clear that
$\mathcal{G}_{\alpha}^{2|Q|}$ is empty and therefore it holds that
$rank(\alpha)\leq 2|Q|$.

∎

###### Lemma 12

There is a level $l\geq 0$ such that for each level $l^{\prime}>l$, and for
all odd ranks $j$ up to the maximal odd rank, there is a vertex
$(q,l^{\prime})$ such that $rank(q,l^{\prime})=j$.

###### Proof

This proof is a modification of [11] (Lemma 2) to BAs with mixed
transition/state-based acceptance condition. Let $k$ be the minimal index for
which $\mathcal{G}_{2k}$ is finite. For every $0\leq i\leq k-1$, the DAG
$\mathcal{G}_{2i+1}$ contains an endangered vertex. Let $l_{i}$ be the minimal
level such that $\mathcal{G}_{2i+1}$ contains an endangered vertex
$(q,l_{i})$. Since $(q,l_{i})$ is in $\mathcal{G}_{2i+1}$, it is not finite in
$\mathcal{G}_{2i}$. Thus, there are infinitely many vertices in
$\mathcal{G}_{2i}$ that are reachable from $(q,l_{i})$. Hence, by König’s
Lemma, $\mathcal{G}_{2i}$ contains an infinite path
$(q,l_{i}),(q_{1},l_{i}+1),(q_{2},l_{i}+2),\ldots$. For all $j\geq 1$, the
vertex $(q_{j},l_{i}+j)$ has infinitely many vertices reachable from it in
$\mathcal{G}_{2i}$ and thus, it is not finite in $\mathcal{G}_{2i}$.
Therefore, the path $(q,l_{i}),(q_{1},l_{i}+1),(q_{2},l_{i}+2),\ldots$ exists
also in $\mathcal{G}_{2i+1}$. Since $(q,l_{i})$ is endangered, all vertices
$(q_{j},l_{i}+j)$ are endangered as well. It follows that for every $0\leq
i\leq k-1$ there exists a level $l_{i}$ such that for all $l^{\prime}\geq
l_{i}$, there is an endangered vertex $(q,l^{\prime})$ from which it cannot be
reached to any accepting edge and for which $rank(q,l^{\prime})$ would
therefore be $2i+1$. ∎

###### Lemma 13

There is a level $l\geq 0$ such that for each level $l^{\prime}>l$, the level
ranking that corresponds to $l^{\prime}$ is tight.

###### Proof

This proof is a modification of [11] (Lemma 3) to BAs with mixed
transition/state-based acceptance condition. According to Lemma 12, there is a
level $l_{1}\geq 0$ such that for all levels $l_{2}\geq l_{1}$ there is a
vertex $(q,l_{2})$ such that $rank(q,l_{2})=j$ for all odd ranks $j$ up to the
maximal odd rank. In order to be tight, a level ranking must have an odd rank.
Since even ranks label finite vertices, only a finite number of levels $l_{2}$
have even ranks greater than maximal odd rank. Therefore there exists a level
$l\geq l_{2}$ such that all $l^{\prime}\geq l$ have odd rank. ∎

See 3.1

###### Proof

This proof is a modification of Schewe’s proof from [8] to BAs with mixed
transition/state-based acceptance condition.

First, we show that
$\mathcal{L}(\textsc{Schewe}(\mathcal{A}))\subseteq\Sigma^{\omega}\setminus\mathcal{L}(\mathcal{A})$.
Consider some $\alpha\in\mathcal{L}(\textsc{Schewe}(\mathcal{A}))$. Let
$\rho=S_{0}\ldots S_{k}(S_{k+1},O_{k+1},f_{k+1},i_{k+1})\ldots$ be a run of
$\textsc{Schewe}(\mathcal{A})$ on $\alpha$ and
$\rho^{\prime}=q_{0}q_{1}\ldots$ be a run of $\mathcal{A}$ on $\alpha$. From
the construction of $\textsc{Schewe}(\mathcal{A})$ it holds that
$f_{l}\leavevmode\hbox to11.1pt{\vbox
to6.12pt{\pgfpicture\makeatletter\hbox{\hskip 0.3pt\lower-3.0613pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\hbox to0.0pt{\hbox to0.0pt{\hbox
to0.0pt{\hbox to0.0pt{ {}{ {}{}{}}{{{ {}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{
{}{}{}}}}{ {}{}{}}{{{ {}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{
{}{}{}}{{{ {}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@stroke@opacity{0.1}\pgfsys@invoke{
}\pgfsys@fill@opacity{0.1}\pgfsys@invoke{ }{{}{}\pgfsys@beginscope{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@setlinewidth{3.0pt}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{8.0pt}{8.0pt}\pgfsys@stroke
\pgfsys@endscope\pgfsys@endscope{{}}{{}}{{}}{{}}}\pgfsys@invoke{
\lxSVG@closescope \lxSVG@closescope }{-0.17365}{0.98482}{0.0pt}{0.0pt}{
\lxSVG@closescope \lxSVG@closescope
}{0}\definecolor[named]{pgf@tempcolor}{rgb}{0,0,0}\pgfsys@invoke{\lxSVG@setpatternuncolored@{21}{0}{0}{0}
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@stroke@opacity{0.1}\pgfsys@invoke{
}\pgfsys@fill@opacity{0.1}\pgfsys@invoke{
}\definecolor[named]{pgf@tempcolor}{rgb}{0,0,0}\pgfsys@invoke{\lxSVG@setpatternuncolored@{21}{0}{0}{0}
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{-33.3043pt}{34.70076pt}\pgfsys@lineto{-75.95824pt}{34.70076pt}\pgfsys@curveto{-80.37657pt}{34.70076pt}{-83.95824pt}{31.1191pt}{-83.95824pt}{26.70076pt}\pgfsys@lineto{-83.95824pt}{-14.70033pt}\pgfsys@curveto{-83.95824pt}{-19.11867pt}{-80.37657pt}{-22.70033pt}{-75.95824pt}{-22.70033pt}\pgfsys@lineto{-33.3043pt}{-22.70033pt}\pgfsys@curveto{-28.88597pt}{-22.70033pt}{-25.3043pt}{-19.11867pt}{-25.3043pt}{-14.70033pt}\pgfsys@lineto{-25.3043pt}{26.70076pt}\pgfsys@curveto{-25.3043pt}{31.1191pt}{-28.88597pt}{34.70076pt}{-33.3043pt}{34.70076pt}\pgfsys@closepath\pgfsys@moveto{-83.95824pt}{-22.70033pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-78.95824pt}{6.00021pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{\minipage[t]{48.65395pt}\endminipage}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{ {}{}{}}{{{
{}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@stroke@opacity{0.1}\pgfsys@invoke{
}\pgfsys@fill@opacity{0.1}\pgfsys@invoke{
}\definecolor[named]{pgf@tempcolor}{rgb}{0,0,0}\pgfsys@invoke{\lxSVG@setpatternuncolored@{21}{0}{0}{0}
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@stroke@opacity{0.1}\pgfsys@invoke{
}\pgfsys@fill@opacity{0.1}\pgfsys@invoke{
}\definecolor[named]{pgf@tempcolor}{rgb}{0,0,0}\pgfsys@invoke{\lxSVG@setpatternuncolored@{21}{0}{0}{0}
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{118.65771pt}{-20.03073pt}\pgfsys@lineto{86.21097pt}{-20.03073pt}\pgfsys@curveto{81.79263pt}{-20.03073pt}{78.21097pt}{-23.6124pt}{78.21097pt}{-28.03073pt}\pgfsys@lineto{78.21097pt}{-33.431pt}\pgfsys@curveto{78.21097pt}{-37.84933pt}{81.79263pt}{-41.431pt}{86.21097pt}{-41.431pt}\pgfsys@lineto{118.65771pt}{-41.431pt}\pgfsys@curveto{123.07605pt}{-41.431pt}{126.65771pt}{-37.84933pt}{126.65771pt}{-33.431pt}\pgfsys@lineto{126.65771pt}{-28.03073pt}\pgfsys@curveto{126.65771pt}{-23.6124pt}{123.07605pt}{-20.03073pt}{118.65771pt}{-20.03073pt}\pgfsys@closepath\pgfsys@moveto{78.21097pt}{-41.431pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{83.21097pt}{-30.73087pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{\minipage[t]{38.44675pt}\endminipage}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \hss}
{}{{}}{{{{}}}}{{{{}}}}{{{{}}}}{{{{}}}}{{}}{{{{}}}}{{{{}}}}{{{{}}}}{{{{}}}}{}
{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{3.0pt,3.0pt}{0.0pt}\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{1,0.875,0.875}\pgfsys@color@rgb@fill{1}{0.875}{0.875}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{3.0pt,3.0pt}{0.0pt}\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{1,0.875,0.875}\pgfsys@color@rgb@fill{1}{0.875}{0.875}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{72.40164pt}{32.33197pt}\pgfsys@lineto{-15.79614pt}{32.33197pt}\pgfsys@curveto{-20.21448pt}{32.33197pt}{-23.79614pt}{28.7503pt}{-23.79614pt}{24.33197pt}\pgfsys@lineto{-23.79614pt}{-7.26031pt}\pgfsys@curveto{-23.79614pt}{-11.67865pt}{-20.21448pt}{-15.26031pt}{-15.79614pt}{-15.26031pt}\pgfsys@lineto{72.40164pt}{-15.26031pt}\pgfsys@curveto{76.81998pt}{-15.26031pt}{80.40164pt}{-11.67865pt}{80.40164pt}{-7.26031pt}\pgfsys@lineto{80.40164pt}{24.33197pt}\pgfsys@curveto{80.40164pt}{28.7503pt}{76.81998pt}{32.33197pt}{72.40164pt}{32.33197pt}\pgfsys@closepath\pgfsys@moveto{-23.79614pt}{-15.26031pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-8.79614pt}{8.53583pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{\minipage[t]{74.1978pt}\endminipage} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{}{{}}{{{{}}}}{{{{}}}}{{{{}}}}{{{{}}}}{{}}{{{{}}}}{{{{}}}}{{{{}}}}{{{{}}}}{}
{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{3.0pt,3.0pt}{0.0pt}\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{1,0.875,0.875}\pgfsys@color@rgb@fill{1}{0.875}{0.875}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{3.0pt,3.0pt}{0.0pt}\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{1,0.875,0.875}\pgfsys@color@rgb@fill{1}{0.875}{0.875}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{72.40164pt}{-32.82484pt}\pgfsys@lineto{-15.79614pt}{-32.82484pt}\pgfsys@curveto{-20.21448pt}{-32.82484pt}{-23.79614pt}{-36.40651pt}{-23.79614pt}{-40.82484pt}\pgfsys@lineto{-23.79614pt}{-72.41713pt}\pgfsys@curveto{-23.79614pt}{-76.83546pt}{-20.21448pt}{-80.41713pt}{-15.79614pt}{-80.41713pt}\pgfsys@lineto{72.40164pt}{-80.41713pt}\pgfsys@curveto{76.81998pt}{-80.41713pt}{80.40164pt}{-76.83546pt}{80.40164pt}{-72.41713pt}\pgfsys@lineto{80.40164pt}{-40.82484pt}\pgfsys@curveto{80.40164pt}{-36.40651pt}{76.81998pt}{-32.82484pt}{72.40164pt}{-32.82484pt}\pgfsys@closepath\pgfsys@moveto{-23.79614pt}{-80.41713pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-8.79614pt}{-56.62099pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{\minipage[t]{74.1978pt}\endminipage} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{}{{}}{{{{}}}}{{{{}}}}{{{{}}}}{{{{}}}}{{}}{{{{}}}}{{{{}}}}{{{{}}}}{{{{}}}}{}
{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{3.0pt,3.0pt}{0.0pt}\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{1,0.875,0.875}\pgfsys@color@rgb@fill{1}{0.875}{0.875}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{3.0pt,3.0pt}{0.0pt}\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{1,0.875,0.875}\pgfsys@color@rgb@fill{1}{0.875}{0.875}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{72.40164pt}{-92.86017pt}\pgfsys@lineto{-15.79614pt}{-92.86017pt}\pgfsys@curveto{-20.21448pt}{-92.86017pt}{-23.79614pt}{-96.44183pt}{-23.79614pt}{-100.86017pt}\pgfsys@lineto{-23.79614pt}{-132.45245pt}\pgfsys@curveto{-23.79614pt}{-136.87079pt}{-20.21448pt}{-140.45245pt}{-15.79614pt}{-140.45245pt}\pgfsys@lineto{72.40164pt}{-140.45245pt}\pgfsys@curveto{76.81998pt}{-140.45245pt}{80.40164pt}{-136.87079pt}{80.40164pt}{-132.45245pt}\pgfsys@lineto{80.40164pt}{-100.86017pt}\pgfsys@curveto{80.40164pt}{-96.44183pt}{76.81998pt}{-92.86017pt}{72.40164pt}{-92.86017pt}\pgfsys@closepath\pgfsys@moveto{-23.79614pt}{-140.45245pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-8.79614pt}{-116.65631pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{\minipage[t]{74.1978pt}\endminipage} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\hss} {}{ {}{}{}}{{{}}{{}}}{}{{}}{}{ {}{}{}}{{{}}{{}}}{}{}{}{
{}}{{{}}{{}}{{}}}{}{}{}{{}{}{}}{{{}}{{}}}{}{}{}{ {}{}{}}{{{}}{{}}{{}}}{}{}{}{
{}}{{{}}{{}}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{3.0pt,3.0pt}{0.0pt}\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{1,1,0.8}\pgfsys@color@cmyk@fill{0}{0}{0.2}{0}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{-31.15569pt}{-30.72968pt}\pgfsys@lineto{-31.15569pt}{45.6111pt}\pgfsys@curveto{-31.15569pt}{48.37256pt}{-28.91714pt}{50.6111pt}{-26.15569pt}{50.6111pt}\pgfsys@lineto{37.68066pt}{50.6111pt}\pgfsys@curveto{40.44212pt}{50.6111pt}{44.9192pt}{50.6111pt}{47.68066pt}{50.6111pt}\pgfsys@lineto{94.22546pt}{50.6111pt}\pgfsys@curveto{96.98692pt}{50.6111pt}{99.22546pt}{48.37256pt}{99.22546pt}{45.6111pt}\pgfsys@lineto{99.22546pt}{-5.04164pt}\pgfsys@curveto{99.22546pt}{-7.8031pt}{96.98692pt}{-10.04164pt}{94.22546pt}{-10.04164pt}\pgfsys@lineto{36.15569pt}{-10.04164pt}\pgfsys@curveto{33.39423pt}{-10.04164pt}{31.15569pt}{-12.28018pt}{31.15569pt}{-15.04164pt}\pgfsys@lineto{31.15569pt}{-25.72968pt}\pgfsys@curveto{31.15569pt}{-28.49113pt}{31.15569pt}{-32.96822pt}{31.15569pt}{-35.72968pt}\pgfsys@lineto{31.15569pt}{-84.17421pt}\pgfsys@curveto{31.15569pt}{-86.93567pt}{28.91714pt}{-89.17421pt}{26.15569pt}{-89.17421pt}\pgfsys@lineto{-0.12154pt}{-89.17421pt}\pgfsys@curveto{-2.883pt}{-89.17421pt}{-7.36008pt}{-89.17421pt}{-10.12154pt}{-89.17421pt}\pgfsys@lineto{-26.15569pt}{-89.17421pt}\pgfsys@curveto{-28.91714pt}{-89.17421pt}{-31.15569pt}{-86.93567pt}{-31.15569pt}{-84.17421pt}\pgfsys@lineto{-31.15569pt}{-25.02954pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss} {}{ {}{}{}}{{{
{}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{ {}{}{}}{{{
{}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{ {}{}{}}{{{
{}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@stroke@opacity{0.1}\pgfsys@invoke{
}\pgfsys@fill@opacity{0.1}\pgfsys@invoke{
}\definecolor[named]{pgf@tempcolor}{rgb}{0,0,0}\pgfsys@invoke{\lxSVG@setpatternuncolored@{21}{0}{0}{0}
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@stroke@opacity{0.1}\pgfsys@invoke{
}\pgfsys@fill@opacity{0.1}\pgfsys@invoke{
}\definecolor[named]{pgf@tempcolor}{rgb}{0,0,0}\pgfsys@invoke{\lxSVG@setpatternuncolored@{21}{0}{0}{0}
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{-33.3043pt}{34.70076pt}\pgfsys@lineto{-75.95824pt}{34.70076pt}\pgfsys@curveto{-80.37657pt}{34.70076pt}{-83.95824pt}{31.1191pt}{-83.95824pt}{26.70076pt}\pgfsys@lineto{-83.95824pt}{-14.70033pt}\pgfsys@curveto{-83.95824pt}{-19.11867pt}{-80.37657pt}{-22.70033pt}{-75.95824pt}{-22.70033pt}\pgfsys@lineto{-33.3043pt}{-22.70033pt}\pgfsys@curveto{-28.88597pt}{-22.70033pt}{-25.3043pt}{-19.11867pt}{-25.3043pt}{-14.70033pt}\pgfsys@lineto{-25.3043pt}{26.70076pt}\pgfsys@curveto{-25.3043pt}{31.1191pt}{-28.88597pt}{34.70076pt}{-33.3043pt}{34.70076pt}\pgfsys@closepath\pgfsys@moveto{-83.95824pt}{-22.70033pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-78.95824pt}{6.00021pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{\minipage[t]{48.65395pt}\endminipage}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{ {}{}{}}{{{
{}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@stroke@opacity{0.1}\pgfsys@invoke{
}\pgfsys@fill@opacity{0.1}\pgfsys@invoke{
}\definecolor[named]{pgf@tempcolor}{rgb}{0,0,0}\pgfsys@invoke{\lxSVG@setpatternuncolored@{21}{0}{0}{0}
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@stroke@opacity{0.1}\pgfsys@invoke{
}\pgfsys@fill@opacity{0.1}\pgfsys@invoke{
}\definecolor[named]{pgf@tempcolor}{rgb}{0,0,0}\pgfsys@invoke{\lxSVG@setpatternuncolored@{21}{0}{0}{0}
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{118.65771pt}{-20.03073pt}\pgfsys@lineto{86.21097pt}{-20.03073pt}\pgfsys@curveto{81.79263pt}{-20.03073pt}{78.21097pt}{-23.6124pt}{78.21097pt}{-28.03073pt}\pgfsys@lineto{78.21097pt}{-33.431pt}\pgfsys@curveto{78.21097pt}{-37.84933pt}{81.79263pt}{-41.431pt}{86.21097pt}{-41.431pt}\pgfsys@lineto{118.65771pt}{-41.431pt}\pgfsys@curveto{123.07605pt}{-41.431pt}{126.65771pt}{-37.84933pt}{126.65771pt}{-33.431pt}\pgfsys@lineto{126.65771pt}{-28.03073pt}\pgfsys@curveto{126.65771pt}{-23.6124pt}{123.07605pt}{-20.03073pt}{118.65771pt}{-20.03073pt}\pgfsys@closepath\pgfsys@moveto{78.21097pt}{-41.431pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{83.21097pt}{-30.73087pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{\minipage[t]{38.44675pt}\endminipage}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\hss}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\pgfsys@setlinewidth{0.6pt}\pgfsys@invoke{ } {}{{}}{}
{{}{}}{}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{9.89995pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{10.19995pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}
{}{{}}{}{{{}}{}{}{}{}{}{}{}{}}{}\pgfsys@moveto{4.19998pt}{0.0pt}\pgfsys@moveto{6.30968pt}{0.0pt}\pgfsys@curveto{6.30968pt}{1.16516pt}{5.36514pt}{2.1097pt}{4.19998pt}{2.1097pt}\pgfsys@curveto{3.03482pt}{2.1097pt}{2.09029pt}{1.16516pt}{2.09029pt}{0.0pt}\pgfsys@curveto{2.09029pt}{-1.16516pt}{3.03482pt}{-2.1097pt}{4.19998pt}{-2.1097pt}\pgfsys@curveto{5.36514pt}{-2.1097pt}{6.30968pt}{-1.16516pt}{6.30968pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{4.19998pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}_{S}^{a}f_{l+1}$ for
all $l>k$. The sequence $f_{k+1}(q_{k+1})\geq f_{k+2}(q_{k+2})\geq\ldots$ is
decreasing, and stabilizes eventually. There is therefore some $m>k$ and
$r<2|Q|$ s.t. $f_{p}(q_{p})=r$ for all $p\geq m$. If $r$ is even, then there
exists some $l>k$ such that for all $l^{\prime}\geq l$ it holds that
$i_{l^{\prime}}=r$ and $O_{l^{\prime}}\neq\emptyset$, which contradicts the
assumption that $\rho$ is an accepting run and must therefore contain some
state with $O=\emptyset$ infinitely often. If $r$ is odd, then from some
position in the run there is no accepting state of $\mathcal{A}$ (because
accepting states have even rank), and also no accepting transition, because
two states $q$ and $q^{\prime}$ such that $q^{\prime}\in\delta_{F}(q,a)$
cannot have the same odd rank. $\rho$ is therefore non-accepting.

Now we show that
$\Sigma^{\omega}\setminus\mathcal{L}(\mathcal{A})\subseteq\mathcal{L}(\textsc{Schewe}(\mathcal{A}))$.
Consider some $\alpha\in\Sigma^{\omega}\setminus\mathcal{L}(\mathcal{A})$. If
there is no run of $\mathcal{A}$ on $\alpha$, then there is an accepting run
$\rho=S_{0}S_{1}\ldots$ of $\textsc{Schewe}(\mathcal{A})$ on $\alpha$, which
accepts $\alpha$ in the waiting part of the automaton. Otherwise, there is a
super-tight run $\rho^{\prime}=S_{0}\ldots
S_{k}(S_{k+1},O_{k+1},f_{k+1},i_{k+1})\ldots$ of
$\textsc{Schewe}(\mathcal{A})$ on $\alpha$ matching the levels of
$\mathcal{G}_{\alpha}$ (see [13] for a definition of super-tight run). The
existence of such a run is established by Lemma 13 and Lemma 1. Since
$\alpha\in\Sigma^{\omega}\setminus\mathcal{L}(\mathcal{A})$, there is no run
with infinitely many accepting states or transitions on $\alpha$. The ranking
of each run therefore stabilizes on some odd rank, which means that
$\rho^{\prime}$ contains some accepting state infinitely often and is
therefore accepting. If this were not true, then there would be some $l>k$
such that for all $l^{\prime}\geq l$ it holds $O_{l^{\prime}}\neq\emptyset$
and $i_{l^{\prime}}=i_{l}$. This contradicts the fact that the ranking of each
run stabilizes on some odd rank. $\rho^{\prime}$ is therefore accepting. ∎

See 3

###### Proof

We prove that
$\mathcal{L}(\textsc{Schewe}(\mathcal{A}))=\mathcal{L}(\mathcal{B})$. The
inclusion
$\mathcal{L}(\textsc{Schewe}(\mathcal{A}))\supseteq\mathcal{L}(\mathcal{B})$
is clear (we just omit certain states from the automaton), so let us focus on
the inclusion
$\mathcal{L}(\textsc{Schewe}(\mathcal{A}))\subseteq\mathcal{L}(\mathcal{B})$.
Consider some $\alpha\in\mathcal{L}(\textsc{Schewe}(\mathcal{A}))$. From Lemma
1 and Theorem 3.1 we have that $\alpha\notin\mathcal{L}(\mathcal{A})$ and
there is a ranking of $\mathcal{G}_{\alpha}$ having the rank at most $2|Q|$.
Since $\mu$ is a TRUB wrt $\alpha$, there is some $\ell\in\omega$ such that
$\ell$ is tight and $\forall
k\geq\ell\colon\mu(\mathit{level}_{\alpha}(k))\geq f^{\alpha}_{k}$. We can use
this fact to construct an accepting run $\rho$ of $\mathcal{B}$ on $\alpha$ as
follows:

$\rho=\underset{\text{waiting
part}}{\underbrace{\mathit{level}_{\alpha}(0)\overset{\alpha_{0}}{\rightarrow}\mathit{level}_{\alpha}(1)\overset{\alpha_{1}}{\rightarrow}\cdots\overset{\alpha_{\ell-1}}{\rightarrow}\mathit{level}_{\alpha}(\ell)}}\overset{\alpha_{\ell}}{\rightarrow}\underset{\text{tight