11institutetext:  Faculty of Information Technology, Brno University of
Technology, Brno, Czech Republic 22institutetext: Department of Computer
Science, University of Liverpool, UK 33institutetext: State Key Laboratory of
Computer Science, Institute of Software,
Chinese Academy of Sciences, Beijing, P. R. China 44institutetext: Institute
of Intelligent Software, Guangzhou, Guangzhou, P. R. China

#  Modular Mix-and-Match
Complementation of Büchi Automata
(Technical Report)

Vojtěch Havlena 11 Ondřej Lengál 11 Yong Li 2233
Barbora Šmahlíková 11 Andrea Turrini 3344

###### Abstract

Complementation of nondeterministic Büchi automata (BAs) is an important
problem in automata theory with numerous applications in formal verification,
such as termination analysis of programs, model checking, or in decision
procedures of some logics. We build on ideas from a recent work on BA
determinization by Li _et al._ and propose a new modular algorithm for BA
complementation. Our algorithm allows to combine several BA complementation
procedures together, with one procedure for a subset of the BA’s strongly
connected components (SCCs). In this way, one can exploit the structure of
particular SCCs (such as when they are inherently weak or deterministic) and
use more efficient specialized algorithms, regardless of the structure of the
whole BA. We give a general framework into which partial complementation
procedures can be plugged in, and its instantiation with several algorithms.
The framework can, in general, produce a complement with an Emerson-Lei
acceptance condition, which can often be more compact. Using the algorithm, we
were able to establish an exponentially better new upper bound of
$\mathcal{O}(4^{n})$ for complementation of the recently introduced class of
elevator automata. We implemented the algorithm in a prototype and performed a
comprehensive set of experiments on a large set of benchmarks, showing that
our framework complements well the state of the art and that it can serve as a
basis for future efficient BA complementation and inclusion checking
algorithms.

##  1 Introduction

Nondeterministic Büchi automata (BAs) [8] are an elegant and conceptually
simple framework to model infinite behaviors of systems and the properties
they are expected to satisfy. BAs are widely used in many important
verification tasks, such as termination analysis of programs [27], model
checking [51], or as the underlying formal model of decision procedures for
some logics (such as S1S [8] or a fragment of the first-order logic over
Sturmian words [28]). Many of these applications require to perform
_complementation_ of BAs: For instance, in termination analysis of programs
within Ultimate Automizer [27], complementation is used to keep track of the
set of paths whose termination still needs to be proved. On the other hand, in
model checking111Here, we consider model checking w.r.t. a specification given
in some more expressive logic, such as S1S [8], QPTL [47], or HyperLTL [12],
rather than LTL [41], where negation is simple. and decision procedures of
logics, complement is usually used to implement negation and quantifier
alternation. Complementation is often the most difficult automata operation
performed here; its worst-case state complexity is $\mathcal{O}((0.76n)^{n})$
[45, 2] (which is tight [52]).

In these applications, efficiency of the complementation often determines the
overall efficiency (or even feasibility) of the top-level application. For
instance, the success of Ultimate Automizer in the Termination category of the
International Competition on Software Verification (SV-COMP) [48] is to a
large degree due to an efficient BA complementation algorithm [6, 11] tailored
for BAs with a special structure that it often encounters (as of the time of
writing, it has won 6 gold medals in the years 2017–2022 and two silver medals
in 2015 and 2016). The special structure in this case are the so-called _semi-
deterministic BAs_ (SDBAs), BAs consisting of two parts:  (i) an initial part
without accepting states/transitions and  (ii) a deterministic part containing
accepting states/transitions that cannot transition into the first part.

Complementation of SDBAs using one from the family of the so-called NCSB
algorithms [6, 5, 11, 25] has the worst-case complexity $\mathcal{O}(4^{n})$
(and usually also works much better in practice than general BA
complementation procedures). Similarly, there are efficient complementation
procedures for other subclasses of BAs, e.g.,  (i) _deterministic BAs_(DBAs)
can be complemented into BAs with $2n$ states [32] (or into co-Büchi automata
with $n+1$ states) or  (ii) _inherently weak BAs_(BAs where in each _strongly
connected component_ (SCC), either all cycles are accepting or all cycles are
rejecting) can be complemented into DBAs with $\mathcal{O}(3^{n})$ states
using the Miyano-Hayashi algorithm [39].

For a long time, there has been no efficient algorithm for complementation of
BAs that are highly structured but do not fall into one of the categories
above, e.g., BAs containing inherently weak, deterministic, and some
nondeterministic SCCs. For such BAs, one needed to use a general
complementation algorithm with the $\mathcal{O}((0.76n)^{n})$ (or worse)
complexity. To the best of our knowledge, only recently has there appeared
works that exploit the structure of BAs to obtain a more efficient
complementation algorithm:  (i) The work of Havlena _et al._ [26], who
introduce the class of _elevator automata_ (BAs with an arbitrary mixture of
inherently weak and deterministic SCCs) and give a $\mathcal{O}(16^{n})$
algorithm for them.  (ii) The work of Li _et al._ [34], who propose a BA
determinization procedure (into a deterministic Emerson-Lei automaton) that is
based on decomposing the input BA into SCCs and using a different
determinization procedure for different types of SCCs (inherently weak,
deterministic, general) in a synchronous construction.

In this paper, we propose a new BA complementation algorithm inspired by [34],
where we exploit the fact that complementation is, in a sense, more relaxed
than determinization. In particular, we present a  _framework_ where one can
plug-in different partial complementation procedures fine-tuned for SCCs with
a specific structure. The procedures work only with the given SCCs, to some
degree _independently_ (thus reducing the potential state space explosion)
from the rest of the BA. Our top-level algorithm then orchestrates runs of the
different procedures in a  _synchronous_ manner (or completely independently
in the so-called _postponed_ strategy), obtaining a resulting automaton with
potentially a more general acceptance condition (in general an Emerson-Lei
condition), which can help keeping the result small. If the procedures satisfy
given correctness requirements, our framework guarantees that its
instantiation will also be correct. We also propose its optimizations by,
e.g., using round-robin to decrease the amount of nondeterminism, using shared
breakpoint to reduce the size and the number of colours for certain class of
partial algorithms, and generalize simulation-based pruning of macrostates.

We provide a detailed description of partial complementation procedures for
inherently weak, deterministic, and initial deterministic SCCs, which we use
to obtain a  _new_ exponentially better upper bound of $\mathcal{O}(4^{n})$
for the class of elevator automata (i.e., the same upper bound as for its
strict subclass of SDBAs). Furthermore, we also provide two partial procedures
for general SCCs based on determinization (from [34]) and the rank-based
construction. Using a prototype implementation, we then show our algorithm
complements well existing approaches and significantly improves the state of
the art.

##  2 Preliminaries

We fix a finite non-empty alphabet $\Sigma$ and the first infinite ordinal
$\omega$. An (infinite) word $w$ is a function $w\colon\omega\to\Sigma$ where
the $i$-th symbol is denoted as $w_{i}$. Sometimes, we represent $w$ as an
infinite sequence $w=w_{0}w_{1}\dots$ We denote the set of all infinite words
over $\Sigma$ as $\Sigma^{\omega}$; an _$\omega$ -language_ is a subset of
$\Sigma^{\omega}$.

#### Emerson-Lei Acceptance Conditions.

Given a set $\Gamma=\\{0,\ldots,k-1\\}$ of $k$ _colours_ (often depicted as 0,
1, etc.), we define the set of _Emerson-Lei acceptance conditions_
$\mathbb{EL}(\Gamma)$ as the set of formulae constructed according to the
following grammar:

$\alpha::=\mathsf{Inf}(c)\mid\mathsf{Fin}(c)\mid(\alpha\land\alpha)\mid(\alpha\lor\alpha)\\\
$ (1)

for $c\in\Gamma$. The _satisfaction_ relation $\models$ for a set of colours
$M\subseteq\Gamma$ and condition $\alpha$ is defined inductively as follows
(for $c\in\Gamma$):

$\displaystyle M\models\mathsf{Fin}(c)$ $\displaystyle\text{~{} iff
~{}}c\notin M,$ $\displaystyle M\models\alpha_{1}\lor\alpha_{2}$
$\displaystyle\text{~{} iff ~{}}M\models\alpha_{1}\text{ or
}M\models\alpha_{2},$ $\displaystyle M\models\mathsf{Inf}(c)$
$\displaystyle\text{~{} iff ~{}}c\in M,$ $\displaystyle
M\models\alpha_{1}\land\alpha_{2}$ $\displaystyle\text{~{} iff
~{}}M\models\alpha_{1}\text{ and }M\models\alpha_{2}.$

#### Emerson-Lei Automata.

A (nondeterministic transition-based222We only consider transition-based
acceptance in order to avoid cluttering the paper by always dealing with
accepting states _and_ accepting transitions. Extending our approach to
state/transition-based (or just state-based) automata is straightforward. )
_Emerson-Lei automaton_ (TELA) over $\Sigma$ is a tuple
$\mathcal{A}=(Q,\delta,I,\Gamma,\mathsf{p},\mathsf{Acc})$, where $Q$ is a
finite set of _states_ , $\delta\subseteq Q\times\Sigma\times Q$ is a set of
_transitions_ 333Note that some authors use a more general definition of TELAs
with $\delta\subseteq Q\times\Sigma\times 2^{\Gamma}\times Q$; since we only
use them on the output, we suffice with the simpler definition., $I\subseteq
Q$ is the set of _initial_ states, $\Gamma$ is the set of _colours_ ,
$\mathsf{p}\colon\delta\to 2^{\Gamma}$ is a  _colouring function_ of
transitions, and $\mathsf{Acc}\in\mathbb{EL}(\Gamma)$. We use
$p\overset{a}{\rightarrow}q$ to denote that $(p,a,q)\in\delta$ and sometimes
also treat $\delta$ as a function with the signature $\delta\colon
Q\times\Sigma\to 2^{Q}$. Moreover, we extend $\delta$ to sets of states
$P\subseteq Q$ as $\delta(P,a)=\bigcup_{p\in P}\delta(p,a)$. We use
$\mathcal{A}{}[q]$ for $q\in Q$ to denote the automaton
$\mathcal{A}{}[q]=(Q,\delta,\\{q\\},\Gamma,\mathsf{p},\mathsf{Acc})$, i.e.,
the TELA obtained from $\mathcal{A}$ by setting $q$ as the only initial state.
$\mathcal{A}$ is called _deterministic_ if $|I|\leq 1$ and $|\delta(q,a)|\leq
1$ for each $q\in Q$ and $a\in\Sigma$. If $\Gamma=\\{\leavevmode\hbox
to9.39pt{\vbox to9.39pt{\pgfpicture\makeatletter\hbox{\hskip
4.6947pt\lower-4.6947pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}
\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{}{0.0pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{}{0.0pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}\pgfsys@moveto{4.6947pt}{0.0pt}\pgfsys@curveto{4.6947pt}{2.59283pt}{2.59283pt}{4.6947pt}{0.0pt}{4.6947pt}\pgfsys@curveto{-2.59283pt}{4.6947pt}{-4.6947pt}{2.59283pt}{-4.6947pt}{0.0pt}\pgfsys@curveto{-4.6947pt}{-2.59283pt}{-2.59283pt}{-4.6947pt}{0.0pt}{-4.6947pt}\pgfsys@curveto{2.59283pt}{-4.6947pt}{4.6947pt}{-2.59283pt}{4.6947pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.0pt}{-2.57777pt}\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{\footnotesize{\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}0}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\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}}\\}$ and
$\mathsf{Acc}=\mathsf{Inf}(\leavevmode\hbox to9.39pt{\vbox
to9.39pt{\pgfpicture\makeatletter\hbox{\hskip 4.6947pt\lower-4.6947pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}
\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{}{0.0pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{}{0.0pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}\pgfsys@moveto{4.6947pt}{0.0pt}\pgfsys@curveto{4.6947pt}{2.59283pt}{2.59283pt}{4.6947pt}{0.0pt}{4.6947pt}\pgfsys@curveto{-2.59283pt}{4.6947pt}{-4.6947pt}{2.59283pt}{-4.6947pt}{0.0pt}\pgfsys@curveto{-4.6947pt}{-2.59283pt}{-2.59283pt}{-4.6947pt}{0.0pt}{-4.6947pt}\pgfsys@curveto{2.59283pt}{-4.6947pt}{4.6947pt}{-2.59283pt}{4.6947pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.0pt}{-2.57777pt}\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{\footnotesize{\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}0}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\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}})$, we call
$\mathcal{A}$ a  _Büchi automaton_ (BA) and denote it as
$\mathcal{A}=(Q,\delta,I,F)$ where $F$ is the set of all transitions coloured
by 0, i.e., $F=\mathsf{p}^{-1}(\\{\leavevmode\hbox to9.39pt{\vbox
to9.39pt{\pgfpicture\makeatletter\hbox{\hskip 4.6947pt\lower-4.6947pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}
\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{}{0.0pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{}{0.0pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}\pgfsys@moveto{4.6947pt}{0.0pt}\pgfsys@curveto{4.6947pt}{2.59283pt}{2.59283pt}{4.6947pt}{0.0pt}{4.6947pt}\pgfsys@curveto{-2.59283pt}{4.6947pt}{-4.6947pt}{2.59283pt}{-4.6947pt}{0.0pt}\pgfsys@curveto{-4.6947pt}{-2.59283pt}{-2.59283pt}{-4.6947pt}{0.0pt}{-4.6947pt}\pgfsys@curveto{2.59283pt}{-4.6947pt}{4.6947pt}{-2.59283pt}{4.6947pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.0pt}{-2.57777pt}\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{\footnotesize{\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}0}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\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}}\\}$). For a BA, we
use
$\delta_{F}(p,a)=\\{q\in\delta(p,a)\mid\mathsf{p}(p\overset{a}{\rightarrow}q)=\\{\leavevmode\hbox
to9.39pt{\vbox to9.39pt{\pgfpicture\makeatletter\hbox{\hskip
4.6947pt\lower-4.6947pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}
\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{}{0.0pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{}{0.0pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}\pgfsys@moveto{4.6947pt}{0.0pt}\pgfsys@curveto{4.6947pt}{2.59283pt}{2.59283pt}{4.6947pt}{0.0pt}{4.6947pt}\pgfsys@curveto{-2.59283pt}{4.6947pt}{-4.6947pt}{2.59283pt}{-4.6947pt}{0.0pt}\pgfsys@curveto{-4.6947pt}{-2.59283pt}{-2.59283pt}{-4.6947pt}{0.0pt}{-4.6947pt}\pgfsys@curveto{2.59283pt}{-4.6947pt}{4.6947pt}{-2.59283pt}{4.6947pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.0pt}{-2.57777pt}\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{\footnotesize{\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}0}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\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}}\\}\\}$ (and extend
the notation to sets of states as for $\delta$). A BA
$\mathcal{A}=(Q,\delta,I,F)$ is called _semi-deterministic_ (SDBA) if for
every accepting transition $(p\overset{a}{\rightarrow}q)\in F$, the reachable
fragment of $\mathcal{A}{}[q]$ is deterministic.

A  _run_ of $\mathcal{A}$ from $q\in Q$ on an input word $w$ 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{w_{i}}{\rightarrow}\rho_{i+1}\in\delta$. Let
$\mathrm{inf}_{\delta}(\rho)\subseteq\delta$ denote the set of transitions
occurring in $\rho$ infinitely often and
$\mathrm{inf}_{\Gamma}(\rho)=\bigcup\\{\mathsf{p}(x)\mid
x\in\mathrm{inf}_{\delta}(\rho)\\}$ be the set of infinitely often occurring
colours. A run $\rho$ is _accepting_ in $\mathcal{A}$ iff
$\mathrm{inf}_{\Gamma}(\rho)\models\mathsf{Acc}$ and the _language_ of
$\mathcal{A}$, denoted as $\mathcal{L}(\mathcal{A})$, is defined as the set of
words $w\in\Sigma^{\omega}$ for which there exists an accepting run in
$\mathcal{A}$ starting with some state in $I$.

Consider a BA $\mathcal{A}=(Q,\delta,I,F)$. For a set of states $S\subseteq Q$
we use $\mathcal{A}_{S}$ to denote the copy of $\mathcal{A}$ where accepting
transitions only occur between states from $S$, i.e., the BA
$\mathcal{A}_{S}=(Q,\delta,I,F\cap\delta\raisebox{-2.15277pt}{$|$}_{S})$ where
$\delta\raisebox{-2.15277pt}{$|$}_{S}=\\{p\overset{a}{\rightarrow}q\in\delta\mid
p,q\in S\\}$. We say that a non-empty set of states $C\subseteq Q$ is a
_strongly connected component_ (SCC) if every pair of states of $C$ can reach
each other and $C$ is a maximal such set. An SCC of $\mathcal{A}$ is _trivial_
if it consists of a single state that does not contain a self-loop and _non-
trivial_ otherwise. An SCC $C$ is _accepting_ if it contains at least one
accepting transition and _inherently weak_ iff either  (i) every cycle in $C$
contains a transition from $F$ or  (ii) no cycle in $C$ contains any
transitions from $F$.  An SCC $C$ is _deterministic_ iff the BA
$(C,\delta\raisebox{-2.15277pt}{$|$}_{C},\\{q\\},\emptyset)$ for any $q\in C$
is deterministic. We denote inherently weak components as IWCs, accepting
deterministic components that are not inherently weak as DACs (deterministic
accepting), and the remaining accepting components as NACs (nondeterministic
accepting). A BA $\mathcal{A}$ is called an _elevator automaton_ if it
contains no NAC.

We assume that $\mathcal{A}$ contains no accepting transition outside its SCCs
(no run can cycle over such transitions). We use $\delta_{\mathrm{SCC}}$ to
denote the restriction of $\delta$ to transitions that do not leave their
SCCs, formally,
$\delta_{\mathrm{SCC}}=\\{p\overset{a}{\rightarrow}q\in\delta\mid p\text{ and
}q\text{ are in the same SCC}\\}$. A  _partition block_ $P\subseteq Q$ of
$\mathcal{A}$ is a nonempty union of its accepting SCCs, and a  _partitioning_
of $\mathcal{A}$ is a sequence $P_{1},\ldots,P_{n}$ of pairwise disjoint
partition blocks of $\mathcal{A}$ that contains all accepting SCCs of
$\mathcal{A}$.

The complement (automaton) of a BA $\mathcal{A}$ is a TELA that accepts the
complement language $\Sigma^{\omega}\setminus\mathcal{L}(\mathcal{A})$ of
$\mathcal{L}(\mathcal{A})$. In the paper, we call a state and a run of a
complement automaton a _macrostate_ and a _macrorun_ , respectively.

##  3 A Modular Complementation Algorithm

In a nutshell, the main idea of our BA complementation algorithm is that we
first decompose a BA $\mathcal{A}$ into several partition blocks according to
their properties, and then perform complementation for each of the partition
blocks (potentially using a different algorithm) independently, using either a
_synchronous_ construction, synchronizing the complementation algorithms for
all partition blocks in each step, or a  _postponed_ construction, which
proceeds by complementing the partition blocks independently and combines the
partial results later using automata product construction. The decomposition
of $\mathcal{A}$ into partition blocks can either be trivial—i.e., with one
block for each accepting SCC—, or more elaborate, e.g., a partitioning where
one partition block contains all accepting IWCs, another contains all DACs,
and each NAC is given its own partition block.

In this way, one can avoid running a general complementation algorithm for
unrestricted BAs with the state complexity upper bound
$\mathcal{O}((0.76n)^{n})$ and, instead, apply the most suitable
complementation procedure for each of the partition blocks. This comes with
three main advantages:

  1. 1.

The complementation algorithm for each partition block can be selected
differently in order to exploit the properties of the block. For instance, for
partition blocks with IWCs, one can use complementation based on the
breakpoint (the so-called Miyano-Hayashi) construction [39] with
$\mathcal{O}(3^{n})$ macrostates (cf. Sec. 4.1), while for partition blocks
with only DACs, one can use an algorithm with the state complexity
$\mathcal{O}(4^{n})$ based on an adaptation of the NCSB construction [6, 5,
11, 25] for SDBAs (cf. Sec. 4.2). For NACs, one can choose between, e.g.,
rank- [31, 21, 45, 10, 24, 26] or determinization-based [43, 40, 42]
algorithms, depending on the properties of the NACs (cf. Sec. 6).

  2. 2.

The different complementation algorithms can focus only on the respective
blocks and do not need to consider other parts of the BA. This is
advantageous, e.g., for rank-based algorithms, which can use this restriction
to obtain tighter bounds on the considered ranks (even tighter than using the
refinement in [26]).

  3. 3.

The obtained automaton can be more compact due to the use of a more general
acceptance condition than Büchi [44]—in general, it can be a conjunction of
any $\mathbb{EL}$ conditions (one condition for each partition block),
depending on the output of the complementation procedures; this can allow a
more compact encoding of the produced automaton allowed by using a mixture of
conditions. E.g., a deterministic BA can be complemented with constant extra
generated states when using a co-Büchi condition rather than a linear number
of generated states for a Büchi condition (see Sec. 5.1).

Those partial complementation algorithms then need to be orchestrated by a
top-level algorithm to produce the complement of $\mathcal{A}$.

One might regard our algorithm as an optimization of an approach that would
for each partition block $P$ obtain a BA $\mathcal{A}_{P}$, complement
$\mathcal{A}_{P}$ using the selected algorithm, and perform the intersection
of all $\mathcal{A}_{P}$’s obtained in this way (which would, however, not be
able to obtain the upper bound for elevator automata that we give in Sec.
4.3). Indeed, we also implemented the mentioned procedure (called the
_postponed_ approach, described in Sec. 5.2) and compared it to our main
procedure (called the _synchronous_ approach) described below.

###  3.1 Basic Synchronous Algorithm

In this section, we describe the basic _synchronous_ top-level algorithm.
Then, in Sec. 4, we provide its instantiation for elevator automata and give a
new upper bound for their complementation; in Sec. 5, we discuss several
optimizations of the algorithm; and in Sec. 6, we give a generalization for
unrestricted BAs. Let us fix a BA $\mathcal{A}=(Q,\delta,I,F)$ and, w.l.o.g.,
assume that $\mathcal{A}$ is _complete_ , i.e., $|I|>0$ and all states $q\in
Q$ have an outgoing transition over all symbols $a\in\Sigma$.

The synchronous algorithm works with partial complementation algorithms for
BA’s partition blocks. Each such algorithm $\mathtt{Alg}$ is provided with a
structural condition $\varphi_{\mathtt{Alg}}$ characterizing properties of
partition blocks that the algorithm is able to complement. For a BA
$\mathcal{B}$, we abuse the notation and use $\mathcal{B}\models\varphi$ to
denote that $\mathcal{B}$ satisfies the condition $\varphi$. We say that
$\mathtt{Alg}$ is a  _partial complementation algorithm for a partition block
$P$_ if $\mathcal{A}_{P}\models\varphi_{\mathtt{Alg}}$. We distinguish between
$\mathtt{Alg}$, a general algorithm able to complement a partition block of a
given type, and $\mathtt{Alg}_{P}$, its instantiation for the partition block
$P$. We require each instance $\mathtt{Alg}_{P}$ to provide the following:

  * •

$\mathtt{T}^{\mathtt{Alg}_{P}}$ — the type of the macrostates produced by the
algorithm;

  * •

$\mathtt{Colours}^{\mathtt{Alg}_{P}}=\\{0,\ldots,k^{\mathtt{Alg}_{P}}-1\\}$ —
the set of used colours;

  * •

$\mathtt{Init}^{\mathtt{Alg}_{P}}\in 2^{\mathtt{T}^{\mathtt{Alg}_{P}}}$ — the
set of initial macrostates;

  * •

$\mathtt{Succ}^{\mathtt{Alg}_{P}}\colon(2^{Q}\times\mathtt{T}^{\mathtt{Alg}_{P}}\times\Sigma)\to
2^{\mathtt{T}^{\mathtt{Alg}_{P}}\times\mathtt{Colours}^{\mathtt{Alg}_{P}}}$ —
a function returning the successors of a macrostate such that
$\mathtt{Succ}^{\mathtt{Alg}_{P}}(H,M,a)=\\{(M_{1},\alpha_{1}),\ldots,(M_{k},\alpha_{k})\\}$,
where $H$ is the set of all states of $\mathcal{A}$ reached over the same
word, $M$ is the $\mathtt{Alg}_{P}$’s macrostate for the given partition
block, $a$ is the input symbol, and each $(M_{i},\alpha_{i})$ is a pair
(_macrostate_ , _set of colours_) such that $M_{i}$ is a successor of $M$ over
$a$ w.r.t. $H$ and $\alpha_{i}$ is a set of colours on the edge from $M$ to
$M_{i}$ ($H$ helps to keep track of _new_ runs coming into the partition
block); and

  * •

$\mathtt{Acc}^{\mathtt{Alg}_{P}}\in\mathbb{EL}(\mathtt{Colours}^{\mathtt{Alg}_{P}})$
— the acceptance condition.

Let $P_{1},\ldots,P_{n}$ be a partitioning of $\mathcal{A}$ (w.l.o.g., we
assume that $n>0$), and $\mathtt{Alg}^{1},\ldots,\mathtt{Alg}^{n}$ be a
sequence of algorithms such that $\mathtt{Alg}^{i}$ is a partial
complementation algorithm for $P_{i}$. Furthermore, let us define the
following auxiliary _renumbering_ function $\lambda$ as
$\lambda(c,j)=c+\sum_{i=1}^{j-1}|\mathtt{Colours}^{\mathtt{Alg}^{i}_{P_{i}}}|$,
which is used to make the colours and acceptance conditions from the partial
complementation algorithms disjoint. We also lift $\lambda$ to sets of colours
in the natural way, and also to $\mathbb{EL}$ conditions such that
$\lambda(\varphi,j)$ has the same structure as $\varphi$ but each atom
$\mathsf{Inf}(c)$ is substituted with the atom $\mathsf{Inf}(\lambda(c,j))$
(and likewise for $\mathsf{Fin}$ atoms). The synchronous complementation
algorithm then produces the TELA
$\textsc{ModCompl}(\mathtt{Alg}^{1}_{P_{1}},\dots,\mathtt{Alg}^{n}_{P_{n}},\mathcal{A})=(Q^{\mathcal{C}},\delta^{\mathcal{C}},I^{\mathcal{C}},\Gamma^{\mathcal{C}},\mathsf{p}^{\mathcal{C}},\mathsf{Acc}^{\mathcal{C}})$
with components defined as follows (we use $[S_{i}]_{i=1}^{n}$ to abbreviate
$S_{1}\times\cdots\times S_{n}$):

  * •

$Q^{\mathcal{C}}=2^{Q}\times[\mathtt{T}^{\mathtt{Alg}^{i}_{P_{i}}}]_{i=1}^{n}$,

  * •

$I^{\mathcal{C}}=\\{I\\}\times[\mathtt{Init}^{\mathtt{Alg}^{i}_{P_{i}}}]_{i=1}^{n}$,

  * •

$\Gamma^{\mathcal{C}}=\\{0,\ldots,\lambda(k^{\mathtt{Alg}^{n}_{P_{n}}}-1,n)\\}$,

  * •

$\mathsf{Acc}^{\mathcal{C}}=\bigwedge_{i=1}^{n}\lambda(\mathtt{Acc}^{\mathtt{Alg}^{i}_{P_{i}}},i)$,444If
we drop the condition that $\mathcal{A}$ is complete, we also need to add an
_accepting sink state_ (representing the case for $H=\emptyset$) with self-
loops over all symbols marked by a new colour $s$, and enrich
$\mathsf{Acc}^{\mathcal{C}}$ with $\ldots\lor\mathsf{Inf}(\leavevmode\hbox
to9.39pt{\vbox to9.39pt{\pgfpicture\makeatletter\hbox{\hskip
4.6947pt\lower-4.6947pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}
\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{}{0.0pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.3125,0.3125,0.3125}\pgfsys@color@rgb@fill{0.3125}{0.3125}{0.3125}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{}{0.0pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.3125,0.3125,0.3125}\pgfsys@color@rgb@fill{0.3125}{0.3125}{0.3125}\pgfsys@invoke{
}\pgfsys@moveto{4.6947pt}{0.0pt}\pgfsys@curveto{4.6947pt}{2.59283pt}{2.59283pt}{4.6947pt}{0.0pt}{4.6947pt}\pgfsys@curveto{-2.59283pt}{4.6947pt}{-4.6947pt}{2.59283pt}{-4.6947pt}{0.0pt}\pgfsys@curveto{-4.6947pt}{-2.59283pt}{-2.59283pt}{-4.6947pt}{0.0pt}{-4.6947pt}\pgfsys@curveto{2.59283pt}{-4.6947pt}{4.6947pt}{-2.59283pt}{4.6947pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.875pt}{-1.72221pt}\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{\footnotesize{\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}$s$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\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}})$. and

  * •

$\delta^{\mathcal{C}}$ and $\mathsf{p}^{\mathcal{C}}$ are defined such that if

$((M^{\prime}_{1},\alpha_{1}),\ldots,(M^{\prime}_{n},\alpha_{n}))\in[\mathtt{Succ}^{\mathtt{Alg}^{i}_{P_{i}}}(H,M_{i},a)]_{i=1}^{n},\\\
$

then $\delta^{\mathcal{C}}$ contains the transition
$t\colon(H,M_{1},\ldots,M_{n})\overset{a}{\rightarrow}(\delta(H,a),M^{\prime}_{1},\ldots,M^{\prime}_{n})$,
coloured by $\mathsf{p}^{\mathcal{C}}(t)=\bigcup\\{\lambda(\alpha_{i},i)\mid
1\leq i\leq n\\}$, and $\delta^{\mathcal{C}}$ is the smallest such a set.

In order for ModCompl to be correct, the partial complementation algorithms
need to satisfy certain properties, which we discuss below.

For a structural condition $\varphi$ and a BA $\mathcal{B}=(Q,\delta,I,F)$, we
define $\mathcal{B}\models_{P}\varphi$ iff $\mathcal{B}\models\varphi$, $P$ is
a partition block of $\mathcal{B}$, and $\mathcal{B}$ contains no accepting
transitions outside $P$. We can now provide the correctness condition on
$\mathtt{Alg}$.

###### Definition 1

We say that $\mathtt{Alg}$ is _correct_ if for each $\mathcal{B}$ such that
$\mathcal{B}\models_{P}\varphi_{\mathtt{Alg}}$ we have
$\mathcal{L}(\textsc{ModCompl}(\mathtt{Alg}_{P},\mathcal{B}))=\Sigma^{\omega}\setminus\mathcal{L}(\mathcal{B})$.

The correctness of the synchronous algorithm (provided that each partial
complementation algorithm is correct) is then established by Theorem 3.1.

######  Theorem 3.1 ()

Let $\mathcal{A}$ be a BA, $P_{1},\ldots,P_{n}$ be a partitioning of
$\mathcal{A}$, and $\mathtt{Alg}^{1},\ldots,\mathtt{Alg}^{n}$ be a sequence of
partial complementation algorithms such that $\mathtt{Alg}^{i}$ is _correct_
for $P_{i}$. Then, we have
$\mathcal{L}(\textsc{ModCompl}(\mathtt{Alg}^{1}_{P_{1}},\dots,\mathtt{Alg}^{n}_{P_{n}},\mathcal{A}))=\Sigma^{\omega}\setminus\mathcal{L}(\mathcal{A})$.

##  4 Modular Complementation of Elevator Automata

In this section, we first give partial algorithms to complement partition
blocks with only accepting IWCs (Sec. 4.1) and partition blocks with only DACs
(Sec. 4.2). Then, in Sec. 4.3, we show that using our algorithm, the upper
bound on the size of the complement of elevator BAs is in
$\mathcal{O}(4^{n})$, which is _exponentially better_ than the known upper
bound $\mathcal{O}(16^{n})$ established in [26].

###  4.1 Complementation of Inherently Weak Accepting Components

First, we introduce a partial algorithm $\mathtt{MH}$ with the condition
$\varphi_{\mathtt{MH}}$ specifying that all SCCs in the partition block $P$
are _accepting_ IWCs. Let $P$ be a partition block of $\mathcal{A}$ such that
$\mathcal{A}_{P}\models\varphi_{\mathtt{MH}}$. Our proposed approach makes use
of the Miyano-Hayashi construction [39]. Since in accepting IWCs, all runs are
accepting, the idea of the construction is to accept words such that all runs
over the words eventually leave $P$.

Therefore, we use a pair $(C,B)$ of sets of states as a macrostate for
complementing $P$. Intuitively, we use $C$ to denote the set of all runs of
$\mathcal{A}$ that are in $P$ ($C$ for “ _check_ ”). The set $B\subseteq C$
represents the runs being inspected whether they leave $P$ at some point ($B$
for “ _breakpoint_ ”). Initially, we let $C=I\cap P$ and also sample into
breakpoint all runs in $P$, i.e., set $B=C$. Along reading an $\omega$-word
$w$, if all runs that have entered $P$ eventually leave $P$, i.e., $B$ becomes
empty infinitely often, the complement language of $P$ should contain $w$
(when $B$ becomes empty, we sample $B$ with all runs from the current $C$). We
formalize $\mathtt{MH}_{P}$ as a partial procedure in the framework from Sec.
3.1 as follows:

  * •

$\mathtt{T}^{\mathtt{MH}_{P}}=2^{P}\times 2^{P}$,
$\mathtt{Colours}^{\mathtt{MH}_{P}}=\\{\leavevmode\hbox to9.39pt{\vbox
to9.39pt{\pgfpicture\makeatletter\hbox{\hskip 4.6947pt\lower-4.6947pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}
\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{}{0.0pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,0.30078125,0.62890625}\pgfsys@color@rgb@fill{1}{0.30078125}{0.62890625}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{}{0.0pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,0.30078125,0.62890625}\pgfsys@color@rgb@fill{1}{0.30078125}{0.62890625}\pgfsys@invoke{
}\pgfsys@moveto{4.6947pt}{0.0pt}\pgfsys@curveto{4.6947pt}{2.59283pt}{2.59283pt}{4.6947pt}{0.0pt}{4.6947pt}\pgfsys@curveto{-2.59283pt}{4.6947pt}{-4.6947pt}{2.59283pt}{-4.6947pt}{0.0pt}\pgfsys@curveto{-4.6947pt}{-2.59283pt}{-2.59283pt}{-4.6947pt}{0.0pt}{-4.6947pt}\pgfsys@curveto{2.59283pt}{-4.6947pt}{4.6947pt}{-2.59283pt}{4.6947pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.0pt}{-2.57777pt}\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{\footnotesize{\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}0}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\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}}\\}$,
$\mathtt{Init}^{\mathtt{MH}_{P}}=\\{(I\cap P,I\cap P)\\}$,

  * •

$\mathtt{Acc}^{\mathtt{MH}_{P}}=\mathsf{Inf}(\leavevmode\hbox to9.39pt{\vbox
to9.39pt{\pgfpicture\makeatletter\hbox{\hskip 4.6947pt\lower-4.6947pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}
\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{}{0.0pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,0.30078125,0.62890625}\pgfsys@color@rgb@fill{1}{0.30078125}{0.62890625}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{}{0.0pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,0.30078125,0.62890625}\pgfsys@color@rgb@fill{1}{0.30078125}{0.62890625}\pgfsys@invoke{
}\pgfsys@moveto{4.6947pt}{0.0pt}\pgfsys@curveto{4.6947pt}{2.59283pt}{2.59283pt}{4.6947pt}{0.0pt}{4.6947pt}\pgfsys@curveto{-2.59283pt}{4.6947pt}{-4.6947pt}{2.59283pt}{-4.6947pt}{0.0pt}\pgfsys@curveto{-4.6947pt}{-2.59283pt}{-2.59283pt}{-4.6947pt}{0.0pt}{-4.6947pt}\pgfsys@curveto{2.59283pt}{-4.6947pt}{4.6947pt}{-2.59283pt}{4.6947pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.0pt}{-2.57777pt}\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{\footnotesize{\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}0}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\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}})$, and
$\mathtt{Succ}^{\mathtt{MH}_{P}}(H,(C,B),a)=\\{((C^{\prime},B^{\prime}),\alpha)\\}$
where

    * –

$C^{\prime}=\delta(H,a)\cap P$,
– $B^{\prime}=\begin{cases}C^{\prime}&\text{if }B^{\star}=\emptyset\text{ for
}B^{\star}=\delta(B,a)\cap C^{\prime},\\\ B^{\star}&\text{otherwise,
and}\end{cases}$ – $\alpha=\begin{cases}\\{\leavevmode\hbox to9.39pt{\vbox
to9.39pt{\pgfpicture\makeatletter\hbox{\hskip 4.6947pt\lower-4.6947pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}
\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{}{0.0pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,0.30078125,0.62890625}\pgfsys@color@rgb@fill{1}{0.30078125}{0.62890625}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{}{0.0pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,0.30078125,0.62890625}\pgfsys@color@rgb@fill{1}{0.30078125}{0.62890625}\pgfsys@invoke{
}\pgfsys@moveto{4.6947pt}{0.0pt}\pgfsys@curveto{4.6947pt}{2.59283pt}{2.59283pt}{4.6947pt}{0.0pt}{4.6947pt}\pgfsys@curveto{-2.59283pt}{4.6947pt}{-4.6947pt}{2.59283pt}{-4.6947pt}{0.0pt}\pgfsys@curveto{-4.6947pt}{-2.59283pt}{-2.59283pt}{-4.6947pt}{0.0pt}{-4.6947pt}\pgfsys@curveto{2.59283pt}{-4.6947pt}{4.6947pt}{-2.59283pt}{4.6947pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.0pt}{-2.57777pt}\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{\footnotesize{\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}0}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\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}}\\}&\text{if
}B^{\star}=\emptyset\text{ and}\\\ \emptyset&\text{otherwise.}\end{cases}$

We can see that checking whether $w$ is accepted by the complement of $P$
reduces to check whether $B$ has been cleared infinitely often. Since every
time when $B$ becomes empty, we emit the color 0, we have that $w$ is not
accepted within $P$ if and only if 0 occurs infinitely often. Note that the
transition function $\mathtt{Succ}^{\mathtt{MH}_{P}}$ is deterministic, i.e.,
there is exactly one successor.

######  Lemma 1 ()

The partial algorithm $\mathtt{MH}$ is correct.

###  4.2 Complementation of Deterministic Accepting Components

In this section, we give a partial algorithm $\mathtt{CSB}$ with the condition
$\varphi_{\mathtt{CSB}}$ specifying that a partition block $P$ consists of
_DACs_. Let $P$ be a partition block of $\mathcal{A}$ such that
$\mathcal{A}_{P}\models\varphi_{\mathtt{CSB}}$. Our approach is based on the
NCSB family of algorithms [6, 11, 5, 25] for complementing SDBAs, in
particular the NCSB-MaxRank construction [25]. The algorithm utilizes the fact
that runs in DACs are deterministic, i.e., they do not branch into new runs.
Therefore, one can check that a run is non-accepting if there is a time point
from which the run does not see accepting transitions any more. We call such a
run that does not see accepting transitions any more _safe_. Then, an
$\omega$-word $w$ is not accepted in $P$ iff all runs over $w$ in $P$ either
(i) leave $P$ or (ii) eventually become safe.

For checking point (i), we can use a similar technique as in algorithm
$\mathtt{MH}$, i.e., use a pair $(C,B)$. Moreover, to be able to check point
(ii), we also use the set $S$ that contains runs that are supposed to be
_safe_ , resulting in macrostates of the form $(C,S,B)$555In contrast to
$\mathtt{MH}$, here we use $C\cup S$ rather than $C$ to keep track of all runs
in $P$.. To make sure that all runs are deterministic, we will use
$\delta_{\mathrm{SCC}}$ instead of $\delta$ when computing the successors of
$S$ and $B$ since there may be nondeterministic jumps between different DACs
in $P$; we will not miss any run in $P$ since if a run moves between DACs of
$P$, it can be seen as the run leaving $P$ and a new run entering $P$. Since a
run eventually stays in one SCC, this guarantees that the run will not be
missed.

We formalize $\mathtt{CSB}_{P}$ in the top-level framework as follows:

  * •

$\mathtt{T}^{\mathtt{CSB}_{P}}=2^{P}\times 2^{P}\times 2^{P}$,
$\mathtt{Init}^{\mathtt{CSB}_{P}}=\\{(I\cap P,\emptyset,I\cap P)\\}$,

  * •

$\mathtt{Colours}^{\mathtt{CSB}_{P}}=\\{\leavevmode\hbox to9.39pt{\vbox
to9.39pt{\pgfpicture\makeatletter\hbox{\hskip 4.6947pt\lower-4.6947pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}
\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{}{0.0pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{}{0.0pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}\pgfsys@moveto{4.6947pt}{0.0pt}\pgfsys@curveto{4.6947pt}{2.59283pt}{2.59283pt}{4.6947pt}{0.0pt}{4.6947pt}\pgfsys@curveto{-2.59283pt}{4.6947pt}{-4.6947pt}{2.59283pt}{-4.6947pt}{0.0pt}\pgfsys@curveto{-4.6947pt}{-2.59283pt}{-2.59283pt}{-4.6947pt}{0.0pt}{-4.6947pt}\pgfsys@curveto{2.59283pt}{-4.6947pt}{4.6947pt}{-2.59283pt}{4.6947pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.0pt}{-2.57777pt}\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{\footnotesize{\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}0}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\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}}\\}$,
$\mathtt{Acc}^{\mathtt{CSB}_{P}}=\mathsf{Inf}(\leavevmode\hbox to9.39pt{\vbox
to9.39pt{\pgfpicture\makeatletter\hbox{\hskip 4.6947pt\lower-4.6947pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}
\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{}{0.0pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{}{0.0pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}\pgfsys@moveto{4.6947pt}{0.0pt}\pgfsys@curveto{4.6947pt}{2.59283pt}{2.59283pt}{4.6947pt}{0.0pt}{4.6947pt}\pgfsys@curveto{-2.59283pt}{4.6947pt}{-4.6947pt}{2.59283pt}{-4.6947pt}{0.0pt}\pgfsys@curveto{-4.6947pt}{-2.59283pt}{-2.59283pt}{-4.6947pt}{0.0pt}{-4.6947pt}\pgfsys@curveto{2.59283pt}{-4.6947pt}{4.6947pt}{-2.59283pt}{4.6947pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.0pt}{-2.57777pt}\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{\footnotesize{\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}0}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\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}})$, and

  * •

$\mathtt{Succ}^{\mathtt{CSB}_{P}}(H,(C,S,B),a)=U$ such that

    * –

if $\delta_{F}(S,a)\neq\emptyset$, then $U=\emptyset$ (Runs in $S$ must be
_safe_),

    * –

otherwise $U$ contains $((C^{\prime},S^{\prime},B^{\prime}),c)$ where

      * *

$S^{\prime}=\delta_{\mathrm{SCC}}(S,a)\cap P$ , $C^{\prime}=(\delta(H,a)\cap
P)\setminus S^{\prime}$,
* $B^{\prime}=\begin{cases}C^{\prime}&\text{if }B^{\star}=\emptyset\text{ for }B^{\star}=\delta_{\mathrm{SCC}}(B,a)\text{, }\\\ B^{\star}&\text{otherwise, and}\end{cases}$ * $c=\begin{cases}\\{\leavevmode\hbox to9.39pt{\vbox to9.39pt{\pgfpicture\makeatletter\hbox{\hskip 4.6947pt\lower-4.6947pt\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\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}} \hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@beginscope\pgfsys@invoke{ }{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setdash{}{0.0pt}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setdash{}{0.0pt}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{ }\pgfsys@moveto{4.6947pt}{0.0pt}\pgfsys@curveto{4.6947pt}{2.59283pt}{2.59283pt}{4.6947pt}{0.0pt}{4.6947pt}\pgfsys@curveto{-2.59283pt}{4.6947pt}{-4.6947pt}{2.59283pt}{-4.6947pt}{0.0pt}\pgfsys@curveto{-4.6947pt}{-2.59283pt}{-2.59283pt}{-4.6947pt}{0.0pt}{-4.6947pt}\pgfsys@curveto{2.59283pt}{-4.6947pt}{4.6947pt}{-2.59283pt}{4.6947pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.0pt}{-2.57777pt}\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{\footnotesize{\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}0}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \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}}\\}&\text{if }B^{\star}=\emptyset\text{,}\\\ \emptyset&\text{otherwise}.\end{cases}$

Moreover, in the case
$\delta_{F}(B,a)\cap\delta_{\mathrm{SCC}}(B,a)=\emptyset$, then $U$ also
contains
$((C^{\prime\prime},S^{\prime\prime},C^{\prime\prime}),\\{\leavevmode\hbox
to9.39pt{\vbox to9.39pt{\pgfpicture\makeatletter\hbox{\hskip
4.6947pt\lower-4.6947pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}
\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{}{0.0pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{}{0.0pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}\pgfsys@moveto{4.6947pt}{0.0pt}\pgfsys@curveto{4.6947pt}{2.59283pt}{2.59283pt}{4.6947pt}{0.0pt}{4.6947pt}\pgfsys@curveto{-2.59283pt}{4.6947pt}{-4.6947pt}{2.59283pt}{-4.6947pt}{0.0pt}\pgfsys@curveto{-4.6947pt}{-2.59283pt}{-2.59283pt}{-4.6947pt}{0.0pt}{-4.6947pt}\pgfsys@curveto{2.59283pt}{-4.6947pt}{4.6947pt}{-2.59283pt}{4.6947pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.0pt}{-2.57777pt}\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{\footnotesize{\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}0}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\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}}\\})$ where
$S^{\prime\prime}=S^{\prime}\cup B^{\prime}$ and
$C^{\prime\prime}=C^{\prime}\setminus S^{\prime\prime}$.

Intuitively, when $\delta_{F}(B,a)\cap\delta_{\mathrm{SCC}}(B,a)=\emptyset$,
we make two guesses:  (i) either the runs in $B$ all become safe (we move them
to $S$) or  (ii) there might be some unsafe runs (we keep them in $B$).  Since
the runs in $B$ are deterministic, the number of tracked runs in $B$ will not
increase. Moreover, if all runs in $B$ are eventually safe, we are guaranteed
to move all of them to $S$ at the right time point, e.g., the maximal time
point where all runs are safe since the number of runs is finite.

$p$$q$$r$$s$$\mathcal{A}_{\mathit{ex}}$$P_{0}$$P_{1}$$a,b$$a,b$$a$$\bullet$$b$$a$$a$$b$$\bullet$$b$$a$$\bullet$$p$$\emptyset,\emptyset,\emptyset$$\emptyset,\emptyset$$p+q$$q,\emptyset,q$$\emptyset,\emptyset$$p+q$$\emptyset,q,\emptyset$$\emptyset,\emptyset$$p+q+r$$q,\emptyset,q$$r,r$$p+q+r+s$$q,\emptyset,q$$r+s,r+s$$p+q+r+s$$q,\emptyset,q$$r+s,r$$p+q+r+s$$\emptyset,q,\emptyset$$r+s,r+s$01$b$01$b$1$b$01$b$01$a$1$a$$b$$b$1$a$$a$$b$1$a$0$b$0$b$0$b$0$b$
Figure 1: Left: BA $\mathcal{A}_{\mathit{ex}}$ (dots represent accepting
transitions). Right: the outcome of
$\textsc{ModCompl}(\mathtt{CSB}_{P_{0}},\mathtt{MH}_{P_{1}},\mathcal{A}_{\mathit{ex}})$
with $\mathsf{Acc}\colon\mathsf{Inf}(\leavevmode\hbox to9.39pt{\vbox
to9.39pt{\pgfpicture\makeatletter\hbox{\hskip 4.6947pt\lower-4.6947pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}
\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{}{0.0pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{}{0.0pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}\pgfsys@moveto{4.6947pt}{0.0pt}\pgfsys@curveto{4.6947pt}{2.59283pt}{2.59283pt}{4.6947pt}{0.0pt}{4.6947pt}\pgfsys@curveto{-2.59283pt}{4.6947pt}{-4.6947pt}{2.59283pt}{-4.6947pt}{0.0pt}\pgfsys@curveto{-4.6947pt}{-2.59283pt}{-2.59283pt}{-4.6947pt}{0.0pt}{-4.6947pt}\pgfsys@curveto{2.59283pt}{-4.6947pt}{4.6947pt}{-2.59283pt}{4.6947pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.0pt}{-2.57777pt}\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{\footnotesize{\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}0}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\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}})\land\mathsf{Inf}(\leavevmode\hbox
to9.39pt{\vbox to9.39pt{\pgfpicture\makeatletter\hbox{\hskip
4.6947pt\lower-4.6947pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}
\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{}{0.0pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,0.30078125,0.62890625}\pgfsys@color@rgb@fill{1}{0.30078125}{0.62890625}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{}{0.0pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,0.30078125,0.62890625}\pgfsys@color@rgb@fill{1}{0.30078125}{0.62890625}\pgfsys@invoke{
}\pgfsys@moveto{4.6947pt}{0.0pt}\pgfsys@curveto{4.6947pt}{2.59283pt}{2.59283pt}{4.6947pt}{0.0pt}{4.6947pt}\pgfsys@curveto{-2.59283pt}{4.6947pt}{-4.6947pt}{2.59283pt}{-4.6947pt}{0.0pt}\pgfsys@curveto{-4.6947pt}{-2.59283pt}{-2.59283pt}{-4.6947pt}{0.0pt}{-4.6947pt}\pgfsys@curveto{2.59283pt}{-4.6947pt}{4.6947pt}{-2.59283pt}{4.6947pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.0pt}{-2.57777pt}\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{\footnotesize{\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}1}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\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}})$. States are given
as $(H,(C_{0},S_{0},B_{0}),(C_{1},B_{1}))$; to avoid too many braces, sets are
given as sums.

As mentioned above, $w$ is not accepted within $P$ iff all runs over $w$
either (i) leave $P$ or (ii) become safe. In the context of the presented
algorithm, this corresponds to (i) $B$ becoming empty infinitely often and
(ii) $\delta_{F}(S,a)$ never seeing an accepting transition. Then we only need
to check if there exists an infinite sequence of macrostates
$\hat{\rho}=(C_{0},S_{0},B_{0})\ldots$ that emits 0 infinitely often.

######  Lemma 2 ()

The partial algorithm $\mathtt{CSB}$ is correct.

It is worth noting that when the given partition block $P$ contains all DACs
of $\mathcal{A}$, we can still use the construction above, while the
construction in [25] only works on SDBAs.

###### Example 1

In Fig. 1, we give an example of the run of our algorithm on the BA
$\mathcal{A}_{\mathit{ex}}$. The BA contains three SCCs, one of them (the one
containing $p$) non-accepting (therefore, it does not need to occur in any
partition block). The partition block $P_{0}$ contains a single DAC, so we can
use algorithm $\mathtt{CSB}$, and the partition block $P_{1}$ contains a
single accepting IWC, so we can use $\mathtt{MH}$. The resulting
$\textsc{ModCompl}(\mathtt{CSB}_{P_{0}},\mathtt{MH}_{P_{1}},\mathcal{A}_{\mathit{ex}})$
uses two colours, 0 from $\mathtt{CSB}$ and 1 from $\mathtt{MH}$. The
acceptance condition is $\mathsf{Inf}(\leavevmode\hbox to9.39pt{\vbox
to9.39pt{\pgfpicture\makeatletter\hbox{\hskip 4.6947pt\lower-4.6947pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}
\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{}{0.0pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{}{0.0pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}\pgfsys@moveto{4.6947pt}{0.0pt}\pgfsys@curveto{4.6947pt}{2.59283pt}{2.59283pt}{4.6947pt}{0.0pt}{4.6947pt}\pgfsys@curveto{-2.59283pt}{4.6947pt}{-4.6947pt}{2.59283pt}{-4.6947pt}{0.0pt}\pgfsys@curveto{-4.6947pt}{-2.59283pt}{-2.59283pt}{-4.6947pt}{0.0pt}{-4.6947pt}\pgfsys@curveto{2.59283pt}{-4.6947pt}{4.6947pt}{-2.59283pt}{4.6947pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.0pt}{-2.57777pt}\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{\footnotesize{\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}0}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\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}})\land\mathsf{Inf}(\leavevmode\hbox
to9.39pt{\vbox to9.39pt{\pgfpicture\makeatletter\hbox{\hskip
4.6947pt\lower-4.6947pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}
\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{}{0.0pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,0.30078125,0.62890625}\pgfsys@color@rgb@fill{1}{0.30078125}{0.62890625}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{}{0.0pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,0.30078125,0.62890625}\pgfsys@color@rgb@fill{1}{0.30078125}{0.62890625}\pgfsys@invoke{
}\pgfsys@moveto{4.6947pt}{0.0pt}\pgfsys@curveto{4.6947pt}{2.59283pt}{2.59283pt}{4.6947pt}{0.0pt}{4.6947pt}\pgfsys@curveto{-2.59283pt}{4.6947pt}{-4.6947pt}{2.59283pt}{-4.6947pt}{0.0pt}\pgfsys@curveto{-4.6947pt}{-2.59283pt}{-2.59283pt}{-4.6947pt}{0.0pt}{-4.6947pt}\pgfsys@curveto{2.59283pt}{-4.6947pt}{4.6947pt}{-2.59283pt}{4.6947pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.0pt}{-2.57777pt}\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{\footnotesize{\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}1}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\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}})$. ∎

###  4.3 Upper-bound for Elevator Automata Complementation

We now give an upper bound on the size of the complement generated by our
algorithm for elevator automata, which significantly improves the best
previously known upper bound of $\mathcal{O}(16^{n})$ [26] to
$\mathcal{O}(4^{n})$, the same as for SDBAs, which are a strict subclass of
elevator automata [6] (we note that this upper bound cannot be obtained by a
determinization-based algorithm, since determinization of SDBAs is in
$\Omega(n!)$ [17, 37]).

######  Theorem 4.1 ()

Let $\mathcal{A}$ be an elevator automaton with $n$ states. Then there exists
a BA with $\mathcal{O}(4^{n})$ states accepting the complement of
$\mathcal{L}(\mathcal{A})$.

######  Proof (Sketch)

Let $Q_{W}$ be all states in accepting IWCs, $Q_{D}$ be all states in DACs,
and $Q_{N}$ be the remaining states, i.e., $Q=Q_{W}\uplus Q_{D}\uplus Q_{N}$.
We make two partition blocks: $P_{0}=Q_{W}$ and $P_{1}=Q_{D}$ and use
$\mathtt{MH}$ and $\mathtt{CSB}$ respectively as the partial algorithms, with
macrostates of the form $(H,(C_{0},B_{0}),(C_{1},S_{1},B_{1}))$. For each
state $q_{N}\in Q_{N}$, there are two options: either $q_{N}\notin H$ or
$q_{N}\in H$. For each state $q_{W}\in Q_{W}$, there are three options:  (i)
$q_{W}\notin C_{0}$,  (ii) $q_{W}\in C_{0}\setminus B_{0}$, or  (iii)
$q_{W}\in C_{0}\cap B_{0}$.  Finally, for each $q_{D}\in Q_{D}$, there are
four options:  (i) $q_{D}\notin C_{1}\cup S_{1}$,  (ii) $q_{D}\in S_{1}$,
(iii) $q_{D}\in C_{1}\setminus B_{1}$, or  (iv) $q_{D}\in C_{1}\cap B_{1}$.
Therefore, the total number of macrostates is $2\cdot 2^{|Q_{N}|}\cdot
3^{|Q_{W}|}\cdot 4^{|Q_{D}|}\in\mathcal{O}(4^{n})$ where the initial factor
$2$ is due to degeneralization from two to one colour (the two colours can
actually be avoided by using our shared breakpoint optimization from Sec.
5.4). ∎

##  5 Optimizations of the Modular Construction

In this section, we propose optimizations of the basic modular algorithm. In
Sec. 5.1, we give a partial algorithm to complement initial partition blocks
with DACs. Further, in Sec. 5.2, we propose the postponed construction
allowing to use automata reduction on intermediate results. In Sec. 5.3, we
propose the round-robin algorithm alleviating the problem with the explosion
of the size of the Cartesian product of partial successors. In Sec. 5.4, we
provide an optimization for partial algorithms that are based on the
breakpoint construction, and, finally, in Sec. 5.5, we show how to employ
simulation to decrease the size of macrostates in the synchronous
construction.

###  5.1 Complementation of Initial Deterministic Partition Blocks

Our first optimization is an optimized algorithm $\mathtt{CoB}$ for a subclass
of partition blocks containing DACs. In particular, the condition
$\varphi_{\mathtt{CoB}}$ specifies that the partition block $P$ is
deterministic and can be reached only deterministically in $\mathcal{A}$
(i.e., $\mathcal{A}_{P}$ after removing redundant states is deterministic). In
that case we say that $P$ is an _initial deterministic_ partition block. The
algorithm is based on complementation of deterministic BAs into co-Büchi
automata.

The algorithm $\mathtt{CoB}_{P}$ is formalized below:

  * •

$\mathtt{T}^{\mathtt{CoB}_{P}}=P\cup\\{\emptyset\\}$,
$\mathtt{Init}^{\mathtt{CoB}_{P}}=I\cap P$,
$\mathtt{Colours}^{\mathtt{CoB}_{P}}=\\{\leavevmode\hbox to9.39pt{\vbox
to9.39pt{\pgfpicture\makeatletter\hbox{\hskip 4.6947pt\lower-4.6947pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}
\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{}{0.0pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.19921875,0.62890625,0.171875}\pgfsys@color@rgb@fill{0.19921875}{0.62890625}{0.171875}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{}{0.0pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.19921875,0.62890625,0.171875}\pgfsys@color@rgb@fill{0.19921875}{0.62890625}{0.171875}\pgfsys@invoke{
}\pgfsys@moveto{4.6947pt}{0.0pt}\pgfsys@curveto{4.6947pt}{2.59283pt}{2.59283pt}{4.6947pt}{0.0pt}{4.6947pt}\pgfsys@curveto{-2.59283pt}{4.6947pt}{-4.6947pt}{2.59283pt}{-4.6947pt}{0.0pt}\pgfsys@curveto{-4.6947pt}{-2.59283pt}{-2.59283pt}{-4.6947pt}{0.0pt}{-4.6947pt}\pgfsys@curveto{2.59283pt}{-4.6947pt}{4.6947pt}{-2.59283pt}{4.6947pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.0pt}{-2.57777pt}\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{\footnotesize{\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}0}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\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}}\\}$,
$\mathtt{Acc}^{\mathtt{CoB}_{P}}=\mathsf{Fin}(\leavevmode\hbox to9.39pt{\vbox
to9.39pt{\pgfpicture\makeatletter\hbox{\hskip 4.6947pt\lower-4.6947pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}
\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{}{0.0pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.19921875,0.62890625,0.171875}\pgfsys@color@rgb@fill{0.19921875}{0.62890625}{0.171875}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{}{0.0pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.19921875,0.62890625,0.171875}\pgfsys@color@rgb@fill{0.19921875}{0.62890625}{0.171875}\pgfsys@invoke{
}\pgfsys@moveto{4.6947pt}{0.0pt}\pgfsys@curveto{4.6947pt}{2.59283pt}{2.59283pt}{4.6947pt}{0.0pt}{4.6947pt}\pgfsys@curveto{-2.59283pt}{4.6947pt}{-4.6947pt}{2.59283pt}{-4.6947pt}{0.0pt}\pgfsys@curveto{-4.6947pt}{-2.59283pt}{-2.59283pt}{-4.6947pt}{0.0pt}{-4.6947pt}\pgfsys@curveto{2.59283pt}{-4.6947pt}{4.6947pt}{-2.59283pt}{4.6947pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.0pt}{-2.57777pt}\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{\footnotesize{\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}0}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\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}})$,

  * •

$\mathtt{Succ}^{\mathtt{CoB}_{P}}(H,q,a)=\\{(q^{\prime},\alpha)\\}$ where

    * –

$q^{\prime}=\begin{cases}r&\text{if }\delta(H,a)\cap P=\\{r\\}\text{ and}\\\
\emptyset&\text{otherwise},\end{cases}$

    * –

$\alpha=\begin{cases}\\{\leavevmode\hbox to9.39pt{\vbox
to9.39pt{\pgfpicture\makeatletter\hbox{\hskip 4.6947pt\lower-4.6947pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}
\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{}{0.0pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.19921875,0.62890625,0.171875}\pgfsys@color@rgb@fill{0.19921875}{0.62890625}{0.171875}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{}{0.0pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.12109375,0.46875,0.70703125}\pgfsys@color@rgb@fill{0.12109375}{0.46875}{0.70703125}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.19921875,0.62890625,0.171875}\pgfsys@color@rgb@fill{0.19921875}{0.62890625}{0.171875}\pgfsys@invoke{
}\pgfsys@moveto{4.6947pt}{0.0pt}\pgfsys@curveto{4.6947pt}{2.59283pt}{2.59283pt}{4.6947pt}{0.0pt}{4.6947pt}\pgfsys@curveto{-2.59283pt}{4.6947pt}{-4.6947pt}{2.59283pt}{-4.6947pt}{0.0pt}\pgfsys@curveto{-4.6947pt}{-2.59283pt}{-2.59283pt}{-4.6947pt}{0.0pt}{-4.6947pt}\pgfsys@curveto{2.59283pt}{-4.6947pt}{4.6947pt}{-2.59283pt}{4.6947pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.0pt}{-2.57777pt}\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{\footnotesize{\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}0}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\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}}\\}&\text{if
}q\overset{a}{\rightarrow}{q^{\prime}}\in F\text{ and}\\\
\emptyset&\text{otherwise.}\end{cases}$

Intuitively, all runs reach $P$ deterministically, which means that over a
word $w$, at most one run can reach $P$. Thus, we have $|\delta(H,w_{j})\cap
P|=1$ for some $j\geq 0$ if there is a run over $w$ to $P$, corresponding to
$\delta(H,a)\cap P=\\{r\\}$ in the construction. To check whether $w$ is not
accepted in $P$, we only need to check whether the run from $r\in P$ over $w$
visits accepting transitions only finitely often. We give an example of
complementation of a BA containing an initial deterministic partition block in
Fig. 5 in Appendix 0.D. Notice that the use of the $\mathsf{Fin}$ condition
helps to obtain a more concise automaton with only two states (even in this
simple example, using $\mathtt{CSB}$ instead of $\mathtt{CoB}$ would yield a
TELA with 4 states).

######  Lemma 3 ()

The partial algorithm $\mathtt{CoB}$ is correct.

###  5.2 Postponed Construction

The modular synchronous construction from Sec. 3.1 utilizes the assumption
that in the simultaneous construction of successors for each partition block
over $a$, if one partial macrostate $M_{i}$ does not have a successor over
$a$, then there will be no successor of the $(H,M_{1},\ldots,M_{n})$
macrostate in $\delta^{\mathcal{C}}$ as well. This is useful, e.g., for
inclusion testing, where it is not necessary to generate the whole complement.
On the other hand, if we need to generate the whole automaton, a drawback of
the proposed modular construction is that each partial complementation
algorithm itself may generate a lot of useless states. In this section, we
propose the _postponed construction_ , which complements the partition blocks
(with their surrounding) independently and later combines the intermediate
results to obtain the complement automaton for $\mathcal{A}$. The main
advantage of the postponed construction is that one can apply automata
reduction (e.g., based on removing useless states or using simulation [13, 18,
1, 9]) to decrease the size of the intermediate automata.

In the postponed construction, we use automata product operation implementing
language intersection (i.e., for two TELAs $\mathcal{B}_{1}$ and
$\mathcal{B}_{2}$, a product automaton $\mathcal{B}_{1}\cap\mathcal{B}_{2}$
satisfying
$\mathcal{L}(\mathcal{B}_{1}\cap\mathcal{B}_{2})=\mathcal{L}(\mathcal{B}_{1})\cap\mathcal{L}(\mathcal{B}_{2})$666Alternatively,
one might also avoid the product and generate linear-sized _alternating_ TELA,
but working with those is usually much harder and not used in practice.).
Further, we employ a function $\mathtt{Red}$ performing some language-
preserving reduction of an input TELA. Then, the postponed construction for an
elevator automaton $\mathcal{A}$ with a partitioning $P_{1},\ldots,P_{n}$ and
a sequence of algorithms $\mathtt{Alg}^{1},\ldots,\mathtt{Alg}^{n}$ such that
$\mathtt{Alg}^{i}$ is a partial complementation algorithm for $P_{i}$, is
defined as follows:

$\textsc{PostpCompl}(\mathtt{Alg}^{1}_{P_{1}},\dots,\mathtt{Alg}^{n}_{P_{n}},\mathcal{A})=\bigcap_{i=1}^{n}\mathtt{Red}\left(\textsc{ModCompl}(\mathtt{Alg}^{i}_{P_{i}},\mathcal{A}_{P_{i}})\right).$
(2)

The example of the postponed construction applied on the BA from Fig. 1 is
shown in Appendix 0.D. The correctness of the construction is then summarized
by the following theorem.

######  Theorem 5.1 ()

Let $\mathcal{A}$ be a BA, $P_{1},\ldots,P_{n}$ be a partitioning of
$\mathcal{A}$, and $\mathtt{Alg}^{1},\ldots,\mathtt{Alg}^{n}$ be a sequence of
partial complementation algorithms such that $\mathtt{Alg}^{i}$ is _correct_
for $P_{i}$. Then,
$\mathcal{L}(\textsc{PostpCompl}(\mathtt{Alg}^{1}_{P_{1}},\dots,\mathtt{Alg}^{n}_{P_{n}},\mathcal{A}))=\Sigma^{\omega}\setminus\mathcal{L}(\mathcal{A})$.

###  5.3 Round-Robin Algorithm

The proposed basic synchronous approach from Sec. 3.1 may suffer from the
combinatorial explosion because the successors of a macrostate are given by
the Cartesian product of all successors of the partial macrostates. To
alleviate this explosion, we propose a  _round-robin_ top-level algorithm.
Intuitively, the round-robin algorithm actively tracks runs in only one
partial complementation algorithm at a time (while other algorithms stay
passive). The algorithm periodically changes the active algorithm to avoid
starvation (the decision to leave the active state is, however, fully directed
by the partial complementation algorithm). This can alleviate an explosion in
the number of successors for algorithms that generate more than one successor
(e.g., for rank-based algorithms where one needs to make a nondeterministic
choice of decreasing ranks of states in order to be able to accept [31, 21,
45, 10, 24, 26]; such a choice needs to be made only in the active phase while
in the passive phase, the construction just needs to make sure that the run is
consistent with the given ranking, which can be done deterministically).

The round-robin algorithm works on the level of _partial complementation
round-robin algorithms_. Each instance of the partial algorithm provides
_passive types_ to represent partial macrostates that are passive and _active
types_ to represent currently active partial macrostates. In contrast to the
basic partial complementation algorithms from Sec. 3.1, which provide only a
single successor function, the round-robin partial algorithms provide several
variants of them. In particular, $\mathtt{SuccPass}$ returns (passive)
successors of a passive partial macrostate, $\mathtt{Lift}$ gives all possible
active counterparts of a passive macrostate, and $\mathtt{SuccAct}$ returns
successors of an active partial macrostate. If $\mathtt{SuccAct}$ returns a
partial macrostate of the passive type, the round-robin algorithm promotes the
next partial algorithm to be the active one. For instance, in the round-robin
version of $\mathtt{CSB}$, the passive type does not contain the breakpoint
and only checks that safe runs stay safe, so it is deterministic. Due to space
limitations, we give a formal definition and more details about the round-
robin algorithm in Appendix 0.A.

###  5.4 Shared Breakpoint

The partial complementation algorithms $\mathtt{CSB}$ and $\mathtt{MH}$ (and
later $\mathtt{RNK}$ defined in Appendix 0.C) use a breakpoint to check
whether the runs under inspection are accepting or not. As an optimization, we
consider merging of breakpoints of several algorithms and keeping only a
single breakpoint for all supported algorithms. The top-level algorithm then
needs to manage only one breakpoint and emit a colour only if this sole
breakpoint becomes empty. This may lead to a smaller number of generated
macrostates since we synchronize the breakpoint sampling among several
algorithms. The second benefit is that this allows us to generate fewer
colours (in the case of elevator automata complemented using algorithms
$\mathtt{CSB}$ and $\mathtt{MH}$, we get only one colour).

###  5.5 Simulation Pruning

Our construction can be further optimized by a simulation (or other
compatible) relation for pruning macrostates.777This optimization can be seen
as a generalization of the simulation-based pruning techniques that appeared,
e.g., in [38, 25] in the context of concrete determinization/complementation
procedures. Here, we generalize the technique to all procedures that are based
on run tracking. A simulation is, broadly speaking, a relation
${\preccurlyeq}\subseteq Q\times Q$ implying language inclusion of states,
i.e., $\forall p,q\in Q\colon p\preccurlyeq
q\Longrightarrow\mathcal{L}(\mathcal{A}{}[p])\subseteq\mathcal{L}(\mathcal{A}{}[q])$.
Intuitively, our optimization allows to remove a state $p$ from a macrostate
$M$ if there is also a state $q$ in $M$ such that  (i) $p\preccurlyeq q$,
(ii) $p$is not reachable from $q$, and  (iii) $p$is smaller than $q$ in an
arbitrary total order over $Q$ (this serves as a tie-breaker for simulation-
equivalent mutually unreachable states).  The reason why $p$ can be removed is
that its behaviour can be completely mimicked by $q$. In our construction, we
can then, roughly speaking, replace each call to the functions $\delta(U,a)$
and $\delta_{F}(U,a)$, for a set of states $U$, by $\mathit{pr}(\delta(U,a))$
and $\mathit{pr}(\delta_{F}(U,a))$ respectively in each partial
complementation algorithm, as well as in the top-level algorithm, where
$\mathit{pr}(S)$ is obtained from $S$ by pruning all eligible states. The
details are provided in Appendix 0.B.

##  6 Modular Complementation of Non-Elevator Automata

A non-elevator automaton $\mathcal{A}$ contains at least one NAC, besides
possibly other IWCs or DACs. To complement $\mathcal{A}$ in a modular way, we
apply the techniques seen in Sec. 4 to its DACs and IWCs, while for its NACs
we resort to a general complementation algorithm $\mathtt{Alg}$. In theory,
rank- [31], slice- [29], Ramsey- [47], subset-tuple- [2], and determinization-
[43] based complementation algorithms adapted to work on a single partition
block instead of the whole automaton are all valid instantiations of
$\mathtt{Alg}$. Below, we give a high-level description of two such
algorithms: rank- and determinization-based.

#### Rank-based partial complementation algorithm.

Working on each NAC independently benefits the complementation algorithm even
if the input BA contains only NACs. For instance, in rank-based algorithms
[31, 21, 45, 30, 10, 24, 26], the fact whether all runs of $\mathcal{A}$ over
a given $\omega$-word $w$ are non-accepting is determined by _ranks_ of
states, given by the so-called _ranking functions_. A ranking function is a
(partial) function from $Q$ to $\omega$. The main idea of rank-based
algorithms is the following:  (i) every run is initially nondeterministically
assigned a rank,  (ii) ranks can only decrease along a run,  (iii) ranks need
to be even every time a run visits an accepting transition, and  (iv) the
complement automaton accepts iff all runs eventually get trapped in odd
ranks888Since we focus on intuition here, we use runs rather than the directed
acyclic graphs of runs..  In the standard rank-based procedure, the initial
assignment of ranks to states in (i) is a function
$Q\mathrel{\rightharpoonup}\\{0,\ldots,2n-1\\}$ for $n=|Q|$. Using our
framework, we can, however, significantly restrict the considered ranks in a
partition block $P$ to only $P\mathrel{\rightharpoonup}\\{0,\ldots,2m-1\\}$
for $m=|P|$ (here, it makes sense to use partition blocks consisting of single
SCCs). One can further reduce the considered ranks using the techniques
introduced in, e.g., [24, 26].

In order to adapt the rank-based construction as a partial complementation
algorithm $\mathtt{RNK}$ in our framework, we need to extend the ranking
functions by a fresh “box state”  representing states outside the partition
block. The ranking function then uses  to represent ranks of runs newly coming
into the partition block. The box-extension also requires to change the
transition in a way that  always represents reachable states from the outside.
We provide the details of the construction, which includes the MaxRank
optimization from [24], in Appendix 0.C.

#### Determinization-based partial complementation algorithm.

In [49, 26] we can see that determinization-based complementation is also a
good instantiation of $\mathtt{Alg}$ in practice, so, we also consider the
standard Safra-Piterman determinization [43, 40, 42] as a choice of
$\mathtt{Alg}$ for complementing NACs. Determinization-based algorithms use a
layered subset construction to organize all runs over an $\omega$-word $w$.
The idea is to identify a subset $S\subseteq H$ of reachable states that occur
infinitely often along reading $w$ such that between every two occurrences of
$S$, we have that (i) every state in the second occurrence of $S$ can be
reached by a state in the first occurrence of $S$ and (ii) every state in the
second occurrence is reached by a state in the first occurrence while seeing
an accepting transition. According to König’s lemma, there must then be an
accepting run of $\mathcal{A}$ over $w$.

The construction initially maintains only one set $H$: the set of reachable
states. Since $S$ as defined does not necessarily need to be $H$, every time
there are runs visiting accepting transitions, we create a new subset $C$ for
those runs and remember which subset $C$ is coming from. This way, we actually
organize the current states of all runs into a tree structure and do subset
construction in parallel for the sets in each tree node. If we find a tree
node whose labelled subset, say $S^{\prime}$, is equal to the union of states
in its children, we know the set $S^{\prime}$ satisfies the condition above
and we remove all its child nodes and emit a good event. If such good event
happens infinitely often, it means that $S^{\prime}$ also occurs infinitely
often. So in complementation, we only need to make sure those good events only
happen for finitely many times. Working on each NAC separately also benefits
the determinization-based approach since the number of possible trees will be
less with smaller number of reachable states. Following the idea of [34], to
adapt for the construction as the partial complementation algorithm, we put
all the newly coming runs from other partition blocks in a newly created node
without a parent node. In this way, we actually maintain a forest of trees for
the partial complementation construction. We denote the determinization-based
construction as $\mathtt{DET}$; cf. [34] for details.

##  7 Experimental Evaluation

To evaluate the proposed approach, we implemented it in a prototype tool
Kofola (written in C++) built on top of Spot [16] and compared it against COLA
[34], Ranker [25] (v. 2), Seminator [5] (v. 2.0), and Spot [15, 16] (v.
2.10.6), which are the state of the art in BA complementation [26, 25, 34].
Due to space restrictions, we give results for only two instantiations of our
framework: KofolaS and KofolaP. Both instantiations use $\mathtt{MH}$ for
IWCs, $\mathtt{CSB}$ for DACs, and $\mathtt{DET}$ for NACs. The partitioning
selection algorithm merges all IWCs into one partition block, all DACs into
one partition block, and keeps all NACs separate. Simulation-based pruning
from Sec. 5.5 is turned on, and round-robin from Sec. 5.3 is turned off (since
the selected algorithms are quite deterministic). KofolaS employs the
_synchronous_ and KofolaP employs the _postponed_ strategy. We also consider
the Virtual Best Solver (VBS), i.e., a virtual tool that would choose the best
solver for each single benchmark among all tools (VBS+) and among all tools
except both versions of Kofola (VBS-). We ran our experiments on an Ubuntu
20.04.4 LTS system running on a desktop machine with 16 GiB RAM and an Intel
3.6 GHz i7-4790 CPU. To constrain and collect statistics about the executions
of the tools, we used BenchExec [3] and imposed a memory limit of 12 GiB and a
timeout of 10 minutes; we used Spot to cross-validate the equivalence of the
automata generated by the different tools.

As our data set, we used 39,837 BAs from the automata-benchmarks repository
[33] (used before by, e.g., [26, 25, 34]), which contains BAs from the
following sources:  (i) randomly generated BAs used in [49] (21,876 BAs),
(ii) BAs obtained from LTL formulae from the literature and randomly generated
LTL formulae [5] (3,442 BAs),  (iii) BAs obtained from Ultimate Automizer [11]
(915 BAs),  (iv) BAs obtained from the solver for first-order logic over
Sturmian words Pecan [28] (13,216 BAs),  (v) BAs obtained from an S1S solver
[23] (370 BAs), and  (vi) BAs from LTL to SDBA translation [46] (18 BAs).
From these BAs, 23,850 are deterministic, 6,147 are SDBAs (but not
deterministic), 4,105 are elevator (but not SDBAs), and 5,735 are the rest.

Table 1:  Statistics for our experiments. The column unsolved classifies
unsolved instances by the form _timeouts : out of memory : other failures_.
For the cases of VBS we provide just the number of unsolved cases. The columns
states and runtime provide _mean : median_ of the number of states and
runtime, respectively.

tool | solved | unsolved | states | runtime
---|---|---|---|---
KofolaS | 39,738 | 89 | : | 10 | : | 0 | 76 | : | 3 | 0.32 | : | 0.03
KofolaP | 39,750 | 76 | : | 11 | : | 0 | 86 | : | 3 | 0.41 | : | 0.03
VBS+ | 39,834 |  |  | 3 |  |  | 78 | : | 3 | 0.05 | : | 0.01
VBS- | 39,834 |  |  | 3 |  |  | 96 | : | 3 | 0.05 | : | 0.01

tool | solved | unsolved | states | runtime
---|---|---|---|---
COLA | 39,814 | 21 | : | 0 | : | 2 | 80 | : | 3 | 0.17 | : | 0.02
Ranker | 38,837 | 61 | : | 939 | : | 0 | 45 | : | 4 | 3.31 | : | 0.01
Seminator | 39,026 | 238 | : | 573 | : | 0 | 247 | : | 3 | 1.98 | : | 0.03
Spot | 39,827 | 8 | : | 0 | : | 2 | 160 | : | 4 | 0.08 | : | 0.02

In Table 1 we present an overview of the outcomes. Despite being a prototype,
Kofola is already able to complement a large portion of the input automata,
with very few cases that can be complemented successfully only by Spot or
COLA. Regarding the mean number of states, KofolaS has the least mean value
from all tools (except Ranker, which, however, had 1,000 unsolved cases)
Moreover, Kofola significantly decreased the mean number of states when
included into the VBS: from 96 to 78! We consider this to be a strong
validation of the usefulness of our approach. Regarding the running time, both
versions of Kofola are rather similar; Kofola is just slightly slower than
Spot and COLA but much faster than both Ranker and Seminator (the runtime plot
is in the appendix). Being a prototype, there are many engineering
opportunities for speed-up.

Figure 2: Scatter plots comparing the numbers of states generated by the
tools.

In Fig. 2 we present a comparison of the number of states generated by KofolaS
with those generated by the other tools; we omit VBS+ since the corresponding
plot can be derived from the one for VBS- (since Ranker and Seminator only
output BAs, we compare the sizes of outputs transformed into BAs for all tools
to be fair). In the plots, the number of benchmarks represented by each mark
is given by its color; a mark above the diagonal means that KofolaS generated
an automaton smaller than the other tool while a mark on the top border means
that the other tool failed while KofolaS succeeded, and symmetrically for the
bottom part and the right-hand border. Dashed lines represent the maximum
number of states generated by one of the tools in the plot, axes are
logarithmic.

From the results, KofolaS clearly dominates state-of-the-art tools that are
not based on SCC decomposition (Ranker, Spot, Seminator). The outputs are
quite comparable to COLA, which also uses SCC decomposition and can be seen as
an instantiation of our framework. This supports our intuition that working on
the single SCCs helps in reducing the size of the final automaton, confirming
the validity of our modular mix-and-match Büchi complementation approach.
Lastly, in the figure in the right, we compare our algorithm for elevator
automata with the one in Ranker (the only other tool with a dedicated
algorithm for this subclass). Our new algorithm clearly dominates the one in
Ranker.

##  8 Related Work

To the best of our knowledge, we provide the _first general framework_ where
one can plug-in different BA complementation algorithms while taking advantage
of the specific structure of SCCs. We will discuss the difference between our
work and the literature.

The breakpoint construction [39] was designed to complement BAs with only
IWCs, while our construction treats it as a partial complementation procedure
for IWCs and differs in the need to handle incoming states from other
partition blocks. The NCSB family of algorithms [6, 11, 5, 25] for SDBAs do
not work when there are nondeterministic jumps between DACs; they can,
however, be adapted as partial procedures for complementing DACs in our
framework, cf. Sec. 4.2. In [26], a deelevation-based procedure is applied to
elevator automata to obtain BAs with a fixed maximum rank of 3, for which a
rank-based construction produces a result of the size in
$\mathcal{O}(16^{n})$. In our work, we exploit the structure of the SCCs much
more to obtain an exponentially better upper bound of $\mathcal{O}(4^{n})$
(the same as for SDBAs). The upper bound $\mathcal{O}(4^{n})$ for
complementing unambiguous BAs was established in [36], which is orthogonal to
our work, but seems to be possible to incorporate into our framework in the
future.

There is a huge body of work on complementation of general BAs [8, 47, 7, 31,
21, 22, 10, 24, 26, 45, 2, 43, 40, 42, 5, 49, 29, 50, 19, 20]; all of them
work on the whole graph structure of the input BAs. Our framework is general
enough to allow including all of them as partial complementation procedures
for NACs. On the contrary, our framework does not directly allow (at least in
the synchronous strategy) to use algorithms that _do not_ work on the
structure of the input BA, such as the learning-based complementation
algorithm from [35]. The recent determinization algorithm from [34], which
serves as our inspiration, also handles SCCs separately (it can actually be
seen as an instantiation of our framework). Our current algorithm is, however,
more flexible, allowing to mix-and-match various constructions, keep SCCs
separate or merge them into partition blocks, and allows to obtain the
complexity $\mathcal{O}(4^{n})$, while [34] only allowed $\mathcal{O}(n!)$
(which is tight since SDBA determinization is in $\Omega(n!)$ [17, 37]).

Regarding the tool Spot [15, 16], it should not be perceived as a single
complementation algorithm. Instead, Spot should be seen as a highly engineered
platform utilizing breakpoint construction for inherently weak BAs, NCSB [6,
11] for SDBAs, and determinization-based complementation [43, 40, 42] for
general BAs, while using many other heuristics along the way. Seminator uses
semi-determinization [14, 4, 5] to make sure the input is an SDBA and then
uses NCSB [6, 11] to compute the complement.

##  9 Conclusion and Future Work

We have proposed a general framework for BA complementation where one can
plug-in different partial complementation procedures for SCCs by taking
advantage of their specific structure. Our framework not only obtains
exponentially better upper bound for elevator automata, but also complements
existing approaches well. As shown by the experimental results (especially for
the VBS), our framework significantly improves the current portfolio of
complementation algorithms.

We believe that our framework is an ideal testbed for experimenting with
different BA complementation algorithms, e.g., for the following two reasons:
(i) One can develop an efficient complementation algorithm that only works for
a quite restricted sub-class of BAs (such as the algorithm for initial
deterministic SCCs that we showed in Sec. 5.1) and the framework can leverage
it for complementation of all BAs that contain such a sub-structure.  (ii)
When one tries to improve a general complementation algorithm, they can focus
on complementation of the structurally hard SCCs (mainly the nondeterministic
accepting SCCs) and do not need to look for heuristics that would improve the
algorithm if there were some easier substructure present in the input BA (as
was done, e.g., in [26]).  From how the framework is defined, it immediately
offers opportunities for being used for on-the-fly BA _language inclusion_
testing, leveraging the partial complementation procedures present. Finally,
we believe that the framework also enables new directions for future research
by developing smart ways, probably based on machine learning, of selecting
which partial complementation procedure should be used for which SCC, based on
their features. In future, we want to incorporate other algorithms for
complementation of NACs, and identify properties of SCCs that allow to use
more efficient algorithms (such as unambiguous NACs [36]). Moreover, it seems
that generalizing the Delayed optimization from [24] on the top-level
algorithm could also help reduce the state space.

#### Acknowledgements.

We thank the anonymous reviewers for their useful remarks that helped us
improve the quality of the paper and Alexandre Duret-Lutz for sharing a TikZ
package for beautiful automata. This work was supported by the Strategic
Priority Research Program of the Chinese Academy of Sciences (grant no.
XDA0320000); the National Natural Science Foundation of China (grants no.
62102407 and 61836005); the CAS Project for Young Scientists in Basic Research
(grant no. YSBR-040); the Engineering and Physical Sciences Research Council
(grant no. EP/X021513/1); the Czech Ministry of Education, Youth and Sports
project LL1908 of the ERC.CZ programme; the Czech Science Foundation project
GA23-07565S; and the FIT BUT internal project FIT-S-23-8151.  This project has
received funding from the European Union’s Horizon 2020 research and
innovation programme under the Marie Sklodowska-Curie grant agreement no.
101008233.

## References

  * [1] Abdulla, P.A., Chen, Y., Holík, L., Vojnar, T.: Mediating for reduction (on minimizing alternating büchi automata). Theor. Comput. Sci. 552, 26–43 (2014). https://doi.org/10.1016/j.tcs.2014.08.003, https://doi.org/10.1016/j.tcs.2014.08.003
  * [2] Allred, J.D., Ultes-Nitsche, U.: A simple and optimal complementation algorithm for Büchi automata. In: Dawar, A., Grädel, E. (eds.) Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018. pp. 46–55. ACM (2018). https://doi.org/10.1145/3209108.3209138, https://doi.org/10.1145/3209108.3209138
  * [3] Beyer, D., Löwe, S., Wendler, P.: Reliable benchmarking: requirements and solutions. Int. J. Softw. Tools Technol. Transf. 21(1), 1–29 (2019). https://doi.org/10.1007/s10009-017-0469-y, https://doi.org/10.1007/s10009-017-0469-y
  * [4] Blahoudek, F., Duret-Lutz, A., Klokocka, M., Kretínský, M., Strejcek, J.: Seminator: A tool for semi-determinization of omega-automata. In: Eiter, T., Sands, D. (eds.) LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017. EPiC Series in Computing, vol. 46, pp. 356–367. EasyChair (2017). https://doi.org/10.29007/k5nl, https://doi.org/10.29007/k5nl
  * [5] Blahoudek, F., Duret-Lutz, A., Strejcek, J.: Seminator 2 can complement generalized Büchi automata via improved semi-determinization. In: Lahiri, S.K., Wang, C. (eds.) Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II. Lecture Notes in Computer Science, vol. 12225, pp. 15–27. Springer (2020). https://doi.org/10.1007/978-3-030-53291-8_2, https://doi.org/10.1007/978-3-030-53291-8_2
  * [6] 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. Lecture Notes in Computer Science, vol. 9636, pp. 770–787. Springer (2016). https://doi.org/10.1007/978-3-662-49674-9_49, https://doi.org/10.1007/978-3-662-49674-9_49
  * [7] Breuers, S., Löding, C., Olschewski, J.: Improved Ramsey-based Büchi complementation. In: Birkedal, L. (ed.) Foundations of Software Science and Computational Structures - 15th International Conference, FOSSACS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012\. Proceedings. Lecture Notes in Computer Science, vol. 7213, pp. 150–164. Springer (2012). https://doi.org/10.1007/978-3-642-28729-9_10, https://doi.org/10.1007/978-3-642-28729-9_10
  * [8] Büchi, J.R.: On a decision method in restricted second order arithmetic. In: Mac Lane, S., Siefkes, D. (eds.) The Collected Works of J. Richard Büchi, pp. 425–435. Springer (1990). https://doi.org/10.1007/978-1-4613-8928-6_23, https://doi.org/10.1007/978-1-4613-8928-6_23
  * [9] Bustan, D., Grumberg, O.: Simulation-based Minimization. ACM Transactions on Computational Logic 4(2), 181–206 (2003)
  * [10] 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. Lecture Notes in Computer Science, vol. 11893, pp. 447–467. Springer (2019). https://doi.org/10.1007/978-3-030-34175-6_23, https://doi.org/10.1007/978-3-030-34175-6_23
  * [11] 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. pp. 135–150. ACM (2018). https://doi.org/10.1145/3192366.3192405, https://doi.org/10.1145/3192366.3192405
  * [12] Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., Sánchez, C.: Temporal logics for hyperproperties. In: Abadi, M., Kremer, S. (eds.) Principles of Security and Trust - Third International Conference, POST 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings. Lecture Notes in Computer Science, vol. 8414, pp. 265–284. Springer (2014). https://doi.org/10.1007/978-3-642-54792-8_15, https://doi.org/10.1007/978-3-642-54792-8_15
  * [13] Clemente, L., Mayr, R.: Efficient reduction of nondeterministic automata with application to language inclusion testing. Log. Methods Comput. Sci. 15(1) (2019). https://doi.org/10.23638/LMCS-15(1:12)2019, https://doi.org/10.23638/LMCS-15(1:12)2019
  * [14] 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. pp. 338–345. IEEE Computer Society (1988). https://doi.org/10.1109/SFCS.1988.21950, https://doi.org/10.1109/SFCS.1988.21950
  * [15] Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, E., Xu, L.: Spot 2.0 - A framework for LTL and $\omega$-automata manipulation. In: Artho, C., Legay, A., Peled, D. (eds.) Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings. Lecture Notes in Computer Science, vol. 9938, pp. 122–129 (2016). https://doi.org/10.1007/978-3-319-46520-3_8, https://doi.org/10.1007/978-3-319-46520-3_8
  * [16] Duret-Lutz, A., Renault, E., Colange, M., Renkin, F., Aisse, A.G., Schlehuber-Caissier, P., Medioni, T., Martin, A., Dubois, J., Gillard, C., Lauko, H.: From Spot 2.0 to Spot 2.10: What’s new? In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part II. Lecture Notes in Computer Science, vol. 13372, pp. 174–187. Springer (2022). https://doi.org/10.1007/978-3-031-13188-2_9, https://doi.org/10.1007/978-3-031-13188-2_9
  * [17] Esparza, J., Kretínský, J., Raskin, J., Sickert, S.: From LTL and limit-deterministic Büchi automata to deterministic parity automata. In: Legay, A., Margaria, T. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part I. Lecture Notes in Computer Science, vol. 10205, pp. 426–442 (2017). https://doi.org/10.1007/978-3-662-54577-5_25, https://doi.org/10.1007/978-3-662-54577-5_25
  * [18] Etessami, K., Wilke, T., Schuller, R.A.: Fair simulation relations, parity games, and state space reduction for Büchi automata. SIAM J. Comput. 34(5), 1159–1175 (2005). https://doi.org/10.1137/S0097539703420675, https://doi.org/10.1137/S0097539703420675
  * [19] Fogarty, S., Kupferman, O., Vardi, M.Y., Wilke, T.: Profile trees for Büchi word automata, with application to determinization. Inf. Comput. 245, 136–151 (2015). https://doi.org/10.1016/j.ic.2014.12.021, https://doi.org/10.1016/j.ic.2014.12.021
  * [20] Fogarty, S., Kupferman, O., Wilke, T., Vardi, M.Y.: Unifying Büchi complementation constructions. Log. Methods Comput. Sci. 9(1) (2013). https://doi.org/10.2168/LMCS-9(1:13)2013, https://doi.org/10.2168/LMCS-9(1:13)2013
  * [21] Friedgut, E., Kupferman, O., Vardi, M.Y.: Büchi complementation made tighter. Int. J. Found. Comput. Sci. 17(4), 851–868 (2006). https://doi.org/10.1142/S0129054106004145, https://doi.org/10.1142/S0129054106004145
  * [22] 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. Lecture Notes in Computer Science, vol. 2860, pp. 96–110. Springer (2003). https://doi.org/10.1007/978-3-540-39724-3_10, https://doi.org/10.1007/978-3-540-39724-3_10
  * [23] Havlena, V., Lengál, O., Smahlíková, B.: Deciding S1S: down the rabbit hole and through the looking glass. In: Echihabi, K., Meyer, R. (eds.) Networked Systems - 9th International Conference, NETYS 2021, Virtual Event, May 19-21, 2021, Proceedings. Lecture Notes in Computer Science, vol. 12754, pp. 215–222. Springer (2021). https://doi.org/10.1007/978-3-030-91014-3_15, https://doi.org/10.1007/978-3-030-91014-3_15
  * [24] Havlena, V., Lengál, O.: Reducing (to) the ranks: Efficient rank-based Büchi automata complementation. In: Haddad, S., Varacca, D. (eds.) 32nd International Conference on Concurrency Theory, CONCUR 2021, August 24-27, 2021, Virtual Conference. LIPIcs, vol. 203, pp. 2:1–2:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021). https://doi.org/10.4230/LIPIcs.CONCUR.2021.2, https://doi.org/10.4230/LIPIcs.CONCUR.2021.2
  * [25] Havlena, V., Lengál, O., Šmahlíková, B.: Complementing Büchi automata with Ranker. In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part II. Lecture Notes in Computer Science, vol. 13372, pp. 188–201. Springer (2022). https://doi.org/10.1007/978-3-031-13188-2_10, https://doi.org/10.1007/978-3-031-13188-2_10
  * [26] Havlena, V., Lengál, O., Šmahlíková, B.: Sky is not the limit - tighter rank bounds for elevator automata in Büchi automata complementation. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part II. Lecture Notes in Computer Science, vol. 13244, pp. 118–136. Springer (2022). https://doi.org/10.1007/978-3-030-99527-0_7, https://doi.org/10.1007/978-3-030-99527-0_7
  * [27] Heizmann, M., Hoenicke, J., Podelski, A.: Termination analysis by learning terminating programs. In: Biere, A., Bloem, R. (eds.) Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings. Lecture Notes in Computer Science, vol. 8559, pp. 797–813. Springer (2014). https://doi.org/10.1007/978-3-319-08867-9_53, https://doi.org/10.1007/978-3-319-08867-9_53
  * [28] Hieronymi, P., Ma, D., Oei, R., Schaeffer, L., Schulz, C., Shallit, J.O.: Decidability for Sturmian words. In: Manea, F., Simpson, A. (eds.) 30th EACSL Annual Conference on Computer Science Logic, CSL 2022, February 14-19, 2022, Göttingen, Germany (Virtual Conference). LIPIcs, vol. 216, pp. 24:1–24:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022). https://doi.org/10.4230/LIPIcs.CSL.2022.24, https://doi.org/10.4230/LIPIcs.CSL.2022.24
  * [29] Kähler, D., Wilke, T.: Complementation, disambiguation, and determinization of Büchi automata unified. In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds.) Automata, Languages and Programming, 35th International Colloquium, ICALP 2008, Reykjavik, Iceland, July 7-11, 2008, Proceedings, Part I: Tack A: Algorithms, Automata, Complexity, and Games. Lecture Notes in Computer Science, vol. 5125, pp. 724–735. Springer (2008). https://doi.org/10.1007/978-3-540-70575-8_59, https://doi.org/10.1007/978-3-540-70575-8_59
  * [30] 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. Lecture Notes in Computer Science, vol. 5799, pp. 228–243. Springer (2009). https://doi.org/10.1007/978-3-642-04761-9_18, https://doi.org/10.1007/978-3-642-04761-9_18
  * [31] Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM Trans. Comput. Log. 2(3), 408–429 (2001). https://doi.org/10.1145/377978.377993, https://doi.org/10.1145/377978.377993
  * [32] Kurshan, R.P.: Complementing deterministic Büchi automata in polynomial time. J. Comput. Syst. Sci. 35(1), 59–71 (1987). https://doi.org/10.1016/0022-0000(87)90036-5, https://doi.org/10.1016/0022-0000(87)90036-5
  * [33] Lengál, O.: Automata benchmarks (2022), https://github.com/ondrik/automata-benchmarks
  * [34] Li, Y., Turrini, A., Feng, W., Vardi, M.Y., Zhang, L.: Divide-and-conquer determinization of Büchi automata based on SCC decomposition. In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part II. Lecture Notes in Computer Science, vol. 13372, pp. 152–173. Springer (2022). https://doi.org/10.1007/978-3-031-13188-2_8, https://doi.org/10.1007/978-3-031-13188-2_8
  * [35] Li, Y., Turrini, A., Zhang, L., Schewe, S.: Learning to complement Büchi automata. In: Dillig, I., Palsberg, J. (eds.) Verification, Model Checking, and Abstract Interpretation - 19th International Conference, VMCAI 2018, Los Angeles, CA, USA, January 7-9, 2018, Proceedings. Lecture Notes in Computer Science, vol. 10747, pp. 313–335. Springer (2018). https://doi.org/10.1007/978-3-319-73721-8_15, https://doi.org/10.1007/978-3-319-73721-8_15
  * [36] Li, Y., Vardi, M.Y., Zhang, L.: On the power of unambiguity in Büchi complementation. In: Raskin, J., Bresolin, D. (eds.) Proceedings 11th International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2020, Brussels, Belgium, September 21-22, 2020. EPTCS, vol. 326, pp. 182–198 (2020). https://doi.org/10.4204/EPTCS.326.12, https://doi.org/10.4204/EPTCS.326.12
  * [37] Löding, C.: Optimal bounds for transformations of omega-automata. In: Rangan, C.P., Raman, V., Ramanujam, R. (eds.) Foundations of Software Technology and Theoretical Computer Science, 19th Conference, Chennai, India, December 13-15, 1999, Proceedings. Lecture Notes in Computer Science, vol. 1738, pp. 97–109. Springer (1999). https://doi.org/10.1007/3-540-46691-6_8, https://doi.org/10.1007/3-540-46691-6_8
  * [38] Löding, C., Pirogov, A.: New optimizations and heuristics for determinization of Büchi automata. In: Chen, Y., Cheng, C., Esparza, J. (eds.) Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11781, pp. 317–333. Springer (2019). https://doi.org/10.1007/978-3-030-31784-3_18, https://doi.org/10.1007/978-3-030-31784-3_18
  * [39] Miyano, S., Hayashi, T.: Alternating finite automata on omega-words. Theor. Comput. Sci. 32, 321–330 (1984). https://doi.org/10.1016/0304-3975(84)90049-5, https://doi.org/10.1016/0304-3975(84)90049-5
  * [40] Piterman, N.: From nondeterministic Büchi and Streett automata to deterministic parity automata. Log. Methods Comput. Sci. 3(3) (2007). https://doi.org/10.2168/LMCS-3(3:5)2007, https://doi.org/10.2168/LMCS-3(3:5)2007
  * [41] Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977. pp. 46–57. IEEE Computer Society (1977). https://doi.org/10.1109/SFCS.1977.32, https://doi.org/10.1109/SFCS.1977.32