Simulations in Rank-Based B\"uchi Automata Complementation (Technical Report)

TL;DR

This paper introduces simulation-based techniques to optimize the size of automata produced by rank-based B"uchi automata complementation, making the process more efficient in practice.

Contribution

It proposes novel methods using simulation relations to reduce automaton size in rank-based complementation, improving practical efficiency.

Findings

Techniques significantly reduce automaton size in experiments.

Methods effectively ignore non-contributing macrostates.

Saturation with simulation-smaller states decreases macrostate count.

Abstract

Complementation of B\"uchi automata is an essential technique used in some approaches for termination analysis of programs. The long search for an optimal complementation construction climaxed with the work of Schewe, who proposed a worst-case optimal rank-based procedure that generates complements of a size matching the theoretical lower bound of $(0.76n)^n$, modulo a polynomial factor of $O(n^2)$. Although worst-case optimal, the procedure in many cases produces automata that are unnecessarily large. In this paper, we propose several ways of how to use the direct and delayed simulation relations to reduce the size of the automaton obtained in the rank-based complementation procedure. Our techniques are based on either (i) ignoring macrostates that cannot be used for accepting a word in the complement or (ii) saturating macrostates with simulation-smaller states, in order to decrease their total number. We experimentally showed that our techniques can indeed considerably decrease the size of the output of the complementation.

Equations

$${\mathcal{P}}_{di}(S,O,f,i)\text{iff}\exists p,q\in S:p{⪯}_{di}q\wedge f(p)>f(q).$$

$$Q_2^{di}=Q_2\setminus \{(S,O,f,i)\in Q_2\mid {\mathcal{P}}_{di}(S,O,f,i)\}.$$

$${\mathcal{P}}_{de}(S,O,f,i)\text{iff}\exists p,q\in S:p{⪯}_{de}q\wedge f(p)>\lceil \lceil f(q)\rceil \rceil ,$$

$$Q_2^{de}=Q_2\setminus \{(S,O,f,i)\in Q_2\mid {\mathcal{P}}_{de}(S,O,f,i)\}.$$

$$Q_2^{di+de}=Q_2\setminus \{(S,O,f,i)\in Q_2\mid {\mathcal{P}}_{di}(S,O,f,i)\vee {\mathcal{P}}_{de}(S,O,f,i)\}.$$

$$\rho =S_0{S}_1\dots S_p(S_{p+1},O_{p+1},f_{p+1},i_{p+1})(S_{p+2},O_{p+2},f_{p+2},i_{p+2})\dots$$

$$\{p\}$$

$$\stackrel{a}{\to }(\{p,q\},\varnothing ,\{p\mapsto 3,q\mapsto 2,r\mapsto 1\},2)\stackrel{a}{\to }(\{p,r\},\{r\},\{p\mapsto 3,q\mapsto 1,r\mapsto 2\},0)$$

$$\stackrel{a}{\to }(\{p,q\},\varnothing ,\{p\mapsto 3,q\mapsto 2,r\mapsto 1\},0)\stackrel{a}{\to }\cdots$$

$$\mathcal{A}/{\approx }_x=(Q/{\approx }_x,{\delta }_{{\approx }_x},I_{{\approx }_x},F_{{\approx }_x})$$

Full text

1 Introduction

Büchi automata (BA) complementation is a fundamental problem in program analysis and formal verification, from both theoretical and practical angles. It is, for instance, a critical step in some approaches for termination analysis, which is an essential part of establishing total correctness of programs [14, 19, 9]. Moreover, BA complementation is used as a component of decision procedures of some logics for reasoning about programs, such as S1S capturing a decidable fragment of second-order arithmetic [6] or the temporal logics ETL and QPTL [35].

The study of the BA complementation problem can be traced back to 1962, when Büchi introduced his automaton model in the seminal paper [6] in the context of a decision procedure for the S1S fragment of second-order arithmetic. In the paper, a doubly exponential complementation algorithm based on the infinite Ramsey theorem is proposed. In 1988, Safra [32] introduced a complementation procedure with an $n^{\mathcal{O}(n)}$ upper bound and, in the same year, Michel [28] established an $n!$ lower bound. From the traditional theoretical point of view, the problem was already solved, since exponents in the two bounds matched under the $\mathcal{O}$ notation (recall that $n!$ is approximately $(n/e)^{n}$). From a more practical point of view, a linear factor in an exponent has a significant impact on real-world applications. It was established that the upper bound of Safra’s construction is $2^{2n}$, so the hunt for an optimal algorithm continued [38]. A series of research efforts participated in narrowing the gap [24, 15, 39, 23, 41]. The long journey climaxed with the result of Schewe [33], who proposed an optimal rank-based procedure that generates complements of a size matching the theoretical lower bound of $(0.76n)^{n}$ found by Yan [41], modulo a polynomial factor of $\mathcal{O}(n^{2})$.

Although the algorithm of Schewe is worst-case optimal, it often generates unnecessarily large complements. The standard approach to alleviate this problem is to decrease the size of the input BA before the complementation starts. Since minimization of (nondeterministic) BAs is a PSpace-complete problem, more lightweight reduction methods are necessary. The most prevalent approaches are those based on various notions of simulation-based reduction, such as reductions based on direct simulation [7, 36], a richer delayed simulation [12], or their multi-pebble variants [13]. These approaches first compute a simulation relation over the input BA—which can be done with the time complexity $\mathcal{O}(mn)$ [20, 22, 30, 31, 8] and $\mathcal{O}(mn^{3})$ [12] for direct and delayed simulation respectively, with the number of states $n$ and transitions $m$—and then construct a quotient BA by merging simulation-equivalent states, while preserving the language of the input BA. The other approach is a reduction based on fair simulation [18]. The fair simulation cannot, however, be used for quotienting, but still it can be used for merging certain states and removing transitions. The reduced BA is used as the input of the complementation, which often significantly reduces the size of the result.

In this paper, we propose several ways of how to exploit the direct and delayed simulations in BA complementation even further to obtain smaller complements and shorter running times. We focus, in particular, on the optimal rank-based complementation procedure of Schewe [33]. Essentially, the rank-based construction is an extension of traditional subset construction for determinizing finite automata, with some additional information kept in each macrostate (a state in the complemented BA) to track the acceptance condition of all runs of the input automaton on a given word. In particular, it stores the rank of each state in a macrostate, which, informally, measures the distance to the last accepting state on the corresponding run in the input BA. The main contributions of this paper are the following optimisations of rank-based complementation for BAs, for an input BA $\mathcal{A}$ and the output of the rank-based complementation algorithm $\mathcal{B}$.

Purging: We use simulation relations over $\mathcal{A}$ to remove some useless macrostates during the construction of $\mathcal{B}$. In particular, if a state $p$ is simulated by $q$ in $\mathcal{A}$, this puts a restriction on the relation between the ranks of runs from $p$ and from $q$. As a consequence, macrostates that assign ranks violating this restriction can be purged from $\mathcal{B}$. 2. 2.

Saturation: We saturate macrostates with states that are simulated by the macrostate; this can reduce the total number of states of $\mathcal{B}$ because two or more macrostates can be mapped to a single saturated macrostate. This is inspired by the technique of Glabbeek and Ploeger that uses closures in finite automata determinization [17].

The proposed optimizations are orthogonal to simulation-based size reduction mentioned above. Since the quotienting methods are based on taking only the symmetric fragment of the simulation, i.e., they merge states that simulate each other, after the quotienting, there might still be many pairs where the simulation holds in only one way, and can therefore be exploited by our techniques. Since the considered notions of simulation-based quotienting preserve the respective simulations, our techniques can be used to optimize the complementation at no additional cost. Our experimental evaluation of the optimizations showed that in many cases, they indeed significantly reduce the size of the complemented BA.

2 Preliminaries

We fix a finite nonempty alphabet $\Sigma$ and the first infinite ordinal $\omega=\{0,1,\ldots\}$. For $n\in\omega$, by $[n]$ we denote the set $\{0,\dots,n\}$. An (infinite) word $\alpha$ is represented as a function $\alpha:\omega\to\Sigma$ where the $i$-th symbol is denoted as $\alpha_{i}$. A finite word $w$ of length $n+1$ is represented as a function $w:[n]\to\Sigma$. The finite word of length [math] is denoted as $\epsilon$. We abuse notation and sometimes also represent $\alpha$ as an infinite sequence $\alpha=\alpha_{0}\alpha_{1}\dots$ and $w$ as a finite sequence $w=w_{0}\dots w_{n-1}$. The suffix $\alpha_{i}\alpha_{i+1}\ldots$ of $\alpha$ is denoted by $\alpha_{i:\omega}$. We use $\Sigma^{\omega}$ to denote the set of all infinite words over $\Sigma$ and $\Sigma^{*}$ to denote the set of all finite words. For $L\subseteq\Sigma^{*}$ we define $L^{*}=\{u\in\Sigma^{*}~{}|~{}u=w_{1}\cdots w_{n}\wedge\forall 1\leq i\leq n:w_{i}\in L\}$ and $L^{\omega}=\{\alpha\in\Sigma^{\omega}~{}|~{}\alpha=w_{1}w_{2}\cdots\wedge\forall i\geq 1:w_{i}\in L\}$ (note that $\{\epsilon\}^{\omega}=\emptyset$). Given $L_{1},L_{2}\subseteq\Sigma^{*}$, we use $L_{1}L_{2}$ to denote the set $\{w_{1}w_{2}\mid w_{1}\in L_{1},w_{2}\in L_{2}\}$.

A (nondeterministic) Büchi automaton (BA) over $\Sigma$ is a quadruple $\mathcal{A}=(Q,\delta,I,F)$ where $Q$ is a finite set of states, $\delta$ is a transition function $\delta:Q\times\Sigma\to 2^{Q}$, and $I,F\subseteq Q$ are the sets of initial and accepting states respectively. We sometimes treat $\delta$ as a set of transitions $p\mathop{\xrightarrow{a}}q$, for instance, we use $p\mathop{\xrightarrow{a}}q\in\delta$ to denote that $q\in\delta(p,a)$. Moreover, we extend $\delta$ to sets of states $P\subseteq Q$ as $\delta(P,a)=\bigcup_{p\in P}\delta(p,a)$. A run of $\mathcal{A}$ from $q\in Q$ on an input word $\alpha$ is an infinite sequence $\rho:\omega\to Q$ that starts in $q$ and respects $\delta$, i.e., $\rho_{0}=q$ and $\forall i\geq 0:\rho_{i}\mathop{\xrightarrow{\alpha_{i}}}\rho_{i+1}\in\delta$. We say that $\rho$ is accepting iff it contains infinitely many occurrences of some accepting state, i.e., $\exists q_{f}\in F:|\{i\in\omega\mid\rho_{i}=q_{f}\}|=\omega$. A word $\alpha$ is accepted by $\mathcal{A}$ from a state $q\in Q$ if there is an accepting run $\rho$ of $\mathcal{A}$ from $q$, i.e., $\rho_{0}=q$. The set $\mathcal{L}_{\mathcal{A}}(q)=\{\alpha\in\Sigma^{\omega}\mid\mathcal{A}\text{ accepts }\alpha\text{ from }q\}$ is called the language of $q$ (in $\mathcal{A}$). Given a set of states $R\subseteq Q$, we define the language of $R$ as $\mathcal{L}_{\mathcal{A}}(R)=\bigcup_{q\in R}\mathcal{L}_{\mathcal{A}}(q)$ and the language of $\mathcal{A}$ as $\mathcal{L}(\mathcal{A})=\mathcal{L}_{\mathcal{A}}(I)$. For a pair of states $p$ and $q$ in $\mathcal{A}$, we use $p\mathrel{\subseteq_{\mathcal{L}}}q$ to denote $\mathcal{L}_{\mathcal{A}}(p)\subseteq\mathcal{L}_{\mathcal{A}}(q)$.

Without loss of generality, in this paper, we assume $\mathcal{A}$ to be complete, i.e., for every state $q$ and symbol $a$, it holds that $\delta(q,a)\neq\emptyset$. A trace over a word $\alpha$ is an infinite sequence $\pi=q_{0}\mathop{\xrightarrow{\alpha_{0}}}q_{1}\mathop{\xrightarrow{\alpha_{1}}}\cdots$ such that $\rho=q_{0}q_{1}\ldots$ is a run of $\mathcal{A}$ over $\alpha$ from $q_{0}$. We say $\pi$ is fair if it contains infinitely many accepting states. Moreover, we use $p\overset{w}{\leadsto}q$ for $w\in\Sigma^{*}$ to denote that $q$ is reachable from $p$ over the word $w$; if a path from $p$ to $q$ over $w$ contains an accepting state, we can write $p\overset{w}{\underset{F}{\leadsto}}q$. In this paper, we fix a complete BA $\mathcal{A}=(Q,\delta,I,F)$.

2.1 Simulations

We introduce simulation relations between states of a BA $\mathcal{A}$ using the game semantics in a similar manner as in the extensive study of Clemente and Mayr [26]. In particular, in a simulation game between two players (called Spoiler and Duplicator) in $\mathcal{A}$ from a pair of states $(p_{0},r_{0})$, for any (infinite) trace over a word $\alpha$ that Spoiler takes starting from $p_{0}$, Duplicator tries to mimic the trace starting from $r_{0}$. On the other hand, Spoiler tries to find a trace that Duplicator cannot mimic. The game starts in the configuration $(p_{0},r_{0})$ and every $i$-th round proceeds by, first, Spoiler choosing a transition $p_{i}\mathop{\xrightarrow{\alpha_{i}}}p_{i+1}$ and, second, Duplicator mimicking Spoiler by choosing a matching transition $r_{i}\mathop{\xrightarrow{\alpha_{i}}}r_{i+1}$ over the same symbol $\alpha_{i}$. The next game configuration is $(p_{i+1},r_{i+1})$. Suppose that $\pi_{p}=p_{0}\mathop{\xrightarrow{\alpha_{0}}}p_{1}\mathop{\xrightarrow{\alpha_{1}}}\cdots$ and $\pi_{r}=r_{0}\mathop{\xrightarrow{\alpha_{0}}}r_{1}\mathop{\xrightarrow{\alpha_{1}}}\cdots$ are the two (infinite) traces constructed during the game. Duplicator wins the simulation game if $\mathcal{C}^{x}(\pi_{p},\pi_{r})$ holds, where $\mathcal{C}^{x}(\pi_{p},\pi_{r})$ is a condition that depends on the particular simulation. In the current paper, we consider the following simulation relations:

• •

direct [11]:        $\mathcal{C}^{\mathit{di}}(\pi_{p},\pi_{r})\mathrel{\stackrel{{\scriptstyle\mathrm{def}}}{{\iff}}}\forall i:p_{i}\in F\Rightarrow r_{i}\in F,$

• •

delayed [12]:     $\mathcal{C}^{\mathit{de}}(\pi_{p},\pi_{r})\mathrel{\stackrel{{\scriptstyle\mathrm{def}}}{{\iff}}}\forall i:p_{i}\in F\Rightarrow\exists k\geq i:r_{k}\in F,$ and

• •

fair [21]:            $\mathcal{C}^{f}(\pi_{p},\pi_{r})\mathrel{\stackrel{{\scriptstyle\mathrm{def}}}{{\iff}}}$ if $\pi_{p}$ is fair, then $\pi_{r}$ is fair.

A maximal $x$-simulation relation ${\mathrel{\preceq_{x}}}\subseteq Q\times Q$, for $x\in\{\mathit{di},\mathit{de},f\}$, is defined such that $p\preceq_{x}r$ iff Duplicator has a winning strategy in the simulation game with the winning condition $\mathcal{C}^{x}$ starting from $(p,r)$. Formally, we define a strategy to be a (total) mapping $\sigma:Q\times(Q\times\Sigma\times Q)\to Q$ such that $\sigma(r,p\mathop{\xrightarrow{a}}p^{\prime})\in\delta(r,a)$, i.e., if Duplicator is in state $r$ and Spoiler selects a transition $p\mathop{\xrightarrow{a}}p^{\prime}$, the strategy picks a state $r^{\prime}$ such that $r\mathop{\xrightarrow{a}}r^{\prime}\in\delta$ (and because $\mathcal{A}$ is complete, such a transition always exists). Note that Duplicator cannot look ahead at Spoiler’s future moves. We use $\sigma_{x}$ to denote any winning strategy of Duplicator in the $\mathcal{C}^{x}$ simulation game. Let $\sigma_{x}$ and $\sigma_{x}^{\prime}$ be a pair of winning strategies in the $\mathcal{C}^{x}$ simulation game. We say that $\sigma_{x}$ is dominated by $\sigma_{x}^{\prime}$ if for all states $p$ and all transitions $q\mathop{\xrightarrow{a}}q^{\prime}$ it holds that $\sigma_{x}(p,q\mathop{\xrightarrow{a}}q^{\prime})\mathrel{\preceq_{x}}\sigma_{x}^{\prime}(p,q\mathop{\xrightarrow{a}}q^{\prime})$, and that $\sigma_{x}$ is strictly dominated by $\sigma_{x}^{\prime}$ if $\sigma_{x}$ is dominated by $\sigma_{x}^{\prime}$ and $\sigma_{x}$ does not dominate $\sigma_{x}^{\prime}$. A strategy is dominating if it is not strictly dominated by any other strategy. Strategies are also lifted to traces as follows: let $\pi_{p}$ be as above, then $\sigma(r_{0},\pi_{p})=r_{0}\mathop{\xrightarrow{\alpha_{0}}}r_{1}\mathop{\xrightarrow{\alpha_{1}}}\cdots$ where for all $i\leq 0$ it holds that $\sigma(r_{i},p_{i}\mathop{\xrightarrow{\alpha_{i}}}p_{i+1})=r_{i+1}$. The considered simulation relations form the following hierarchy: ${}\mathrel{\preceq_{\mathit{di}}}{}\subseteq{}\mathrel{\preceq_{\mathit{de}}}{}\subseteq{}\mathrel{\preceq_{f}}{}\subseteq{}\mathrel{\subseteq_{\mathcal{L}}}{}$. Note that every maximal simulation relation is a preorder, i.e., reflexive and transitive.

2.2 Run DAGs

In this section, we recall the terminology from [33] (which is a minor modification of the terminology from [24]). We fix the definition of the run DAG of $\mathcal{A}$ over a word $\alpha$ to be a DAG (directed acyclic graph) $\mathcal{G}_{\alpha}=(V,E)$ of vertices $V$ and edges $E$ where

• •

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

• •

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

Given $\mathcal{G}_{\alpha}$ as above, we will write $(p,i)\in\mathcal{G}_{\alpha}$ to denote that $(p,i)\in V$. We call $(p,i)$ accepting if $p$ is an accepting state. $\mathcal{G}_{\alpha}$ is rejecting if it contains no path with infinitely many accepting vertices. A vertex $(p,i)\in\mathcal{G}_{\alpha}$ is finite if the set of vertices reachable from $(p,i)$ is finite, infinite if it is not finite, and endangered if $(p,i)$ cannot reach an accepting vertex.

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

• •

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

• •

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

• •

Set $j:=j+2$.

For all vertices $v$ that have not been assigned a rank yet, we assign $\mathit{rank}_{\alpha}(v):=\omega$. (Note that since $\mathcal{A}$ is complete, then $\mathcal{G}_{\alpha}^{1}=\mathcal{G}_{\alpha}^{0}$.)

Lemma 1

If $\alpha\notin\mathcal{L}(\mathcal{A})$, then $0\leq\mathit{rank}_{\alpha}(v)\leq 2n$ for all $v\in\mathcal{G}_{\alpha}$. Moreover, if $\alpha\in\mathcal{L}(\mathcal{A})$, then there is a vertex $(p,0)\in\mathcal{G}_{\alpha}$ s.t. $\mathit{rank}_{\alpha}(p,0)=\omega$.

Proof

Follows from Corollary 3.3 in [24]. ∎

3 Complementing Büchi Automata

We use as the starting point the complementation procedure of Schewe [33, Section 3.1], which we denote as Comp${}_{\text{S}}$ (the ‘S’ stands for ‘Schewe’). The procedure works with the notion of level rankings. Given $n=|Q|$, a (level) ranking is a function $f:Q\to[2n]$ such that $\{f(q_{f})\mid q_{f}\in F\}\subseteq\{0,2,\ldots,2n\}$, i.e., $f$ assigns even ranks to accepting states of $\mathcal{A}$.111Note that our basic definitions slightly differs from the ones in Section 2.3 of [33]. This is because of a typo in [33]; indeed, if the procedure from [33] is implemented as is, the output does not accept the complement (there might be a macrostate $(S,O,f)$ where $S$ contains accepting states and $O$ is empty, and, therefore, the whole macrostate is accepting, which is wrong).

For a ranking $f$, the rank of $f$ is defined as $\mathit{rank}(f)=\max\{f(q)\mid q\in Q\}$. For a set of states $S\subseteq Q$, we call $f$ to be $S$-tight if (i) it has an odd rank $r$, (ii) $\{f(s)\mid s\in S\}\supseteq\{1,3,\ldots,r\}$, and (iii) $\{f(q)\mid q\notin S\}=\{0\}$. A ranking is tight if it is $Q$-tight; we use $\mathcal{T}$ to denote the set of all tight rankings. For a pair of rankings $f$ and $f^{\prime}$, a set $S\subseteq Q$, and a symbol $a\in\Sigma$, we use $f^{\prime}\mathrel{\leq^{S}_{a}}f$ iff for every $q\in S$ and $q^{\prime}\in\delta(q,a)$ it holds that $f^{\prime}(q^{\prime})\leq f(q)$.

The Comp${}_{\text{S}}$ procedure constructs the BA $\mathcal{B}_{\mathit{S}}=(Q^{\prime},\delta^{\prime},I^{\prime},F^{\prime})$ whose components are defined as follows:

• •

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

• –

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

• –

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

• •

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

• •

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

• –

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

• –

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

• –

$\delta_{3}:Q_{2}\times\Sigma\to 2^{Q_{2}}$ such that $(S^{\prime},O^{\prime},f^{\prime},i^{\prime})\in\delta_{3}((S,O,f,i),a)$ iff $S^{\prime}=\delta(S,a),f^{\prime}\mathrel{\leq^{S}_{a}}f$, $\mathit{rank}(f)=\mathit{rank}(f^{\prime})$, $f^{\prime}$ is $S^{\prime}$-tight, and

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

• *

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

• •

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

Intuitively, Comp${}_{\text{S}}$ is an extension of the classical subset construction for determinization of finite automata. In particular, $Q_{1},\delta_{1}$, and $I_{1}$ constitute the deterministic finite automaton obtained from $\mathcal{A}$ using the subset construction. The automaton can, however, nondeterministically guess a point at which it will make a transition to a macrostate $(S,O,f,i)$ in the $Q_{2}$ part; this guess corresponds to a level in the run DAG of the accepted word from which the ranks of all levels form an $S$-tight ranking, where the $S$ component of the macrostate is again a subset from the subset construction. In the $Q_{2}$ part, $\mathcal{B}_{\mathit{S}}$ makes sure that in order for a word to be accepted by $\mathcal{B}_{\mathit{S}}$, all runs of $\mathcal{A}$ over the word need to touch an accepting state only finitely many times. This is ensured by the $f$ component, which, roughly speaking, maps states to ranks of corresponding vertices in the run DAG over the given word. The $O$ component is used for a standard cut-point construction, and is used to make sure that all runs that have reached an accepting state in $\mathcal{A}$ will eventually leave it (this can happen for different runs at a different point). The $S,O$, and $f$ components were already present in [24]. The $i$ component was introduced by Schewe to improve the complexity of the construction; it is used to cycle over phases, where in each phase we focus on cut-points of a different rank. See [33] for a more elaborate exposition.

Proposition 1 (Corollary 3.3 in [33])

$\mathcal{L}(\mathcal{B}_{\mathit{S}})=\overline{\mathcal{L}(\mathcal{A})}$.

4 Purging Macrostates with Incompatible Rankings

Our first optimisation is based on removing from $\mathcal{B}_{\mathit{S}}$ macrostates $(S,O,f,i)\in Q_{2}$ whose level ranking $f$ assigns some states of $S$ an unnecessarily high rank. Intuitively, when $S$ contains a state $p$ and a state $q$ such that $p$ is (directly) simulated by $q$, i.e. $p\mathrel{\preceq_{\mathit{di}}}q$, then $f(p)$ needs to be at most $f(q)$. This is because in any word $\alpha$ and its run DAG $\mathcal{G}_{\alpha}$ in $\mathcal{A}$, if $p$ and $q$ are at the same level $i$ of $\mathcal{G}_{\alpha}$, then the ranks of their vertices $v_{p}$ and $v_{q}$ at the given level are either both $\omega$ (when $\alpha\in\mathcal{L}(\mathcal{A})$), or such that $\mathit{rank}_{\alpha}(v_{p})\leq\mathit{rank}_{\alpha}(v_{q})$ otherwise. This is because, intuitively, the DAG rooted in $v_{p}$ in $\mathcal{G}_{\alpha}$ is isomorphic to a subgraph of the DAG rooted in $v_{q}$.

Formally, consider the following predicate on macrostates of $\mathcal{B}_{\mathit{S}}$:

[TABLE]

We modify Comp${}_{\text{S}}$ to purge macrostates that satisfy $\mathcal{P}_{\mathit{di}}$. That is, we create a new procedure Purgedi obtained from Comp${}_{\text{S}}$ by modifying the definition of $\mathcal{B}_{\mathit{S}}$ such that all occurrences of $Q_{2}$ are substituted by $Q_{2}^{\mathit{di}}$ and

[TABLE]

We denote the BA obtained from Purgedi as $\mathcal{B}_{\mathit{S}}^{\mathit{di}}$. The following lemma, proved in Section 4.1 states the correctness of this construction.

Lemma 2 ()

$\mathcal{L}(\mathcal{B}_{\mathit{S}}^{\mathit{di}})=\mathcal{L}(\mathcal{B}_{\mathit{S}})$**

The following natural question arises: Is it possible to extend the purging technique from direct simulation to other notions of simulation? For fair simulation, this cannot be done. The reason is that, for a pair of states $p$ and $q$ s.t. $p\mathrel{\preceq_{f}}q$, it can happen that for a word $\beta\in\Sigma^{\omega}$, there can be a trace from $p$ over $\beta$ that finitely many times touches an accepting state (i.e., a vertex of $p$ in the corresponding run DAG can have any rank between [math] and $2n$), while all traces from $q$ over $\beta$ can completely avoid touching any accepting state. From the point of view of fair simulation, these are both unfair traces, and, therefore, disregarded.

On the other hand, delayed simulation—which is often much richer than direct simulation—can be used, with a small change. Intuitively, the delayed simulation can be used because $p\mathrel{\preceq_{\mathit{de}}}q$ guarantees that on every level of trees in $\mathcal{G}_{\alpha}$ rooted in $v_{p}$ and in $v_{q}$ respectively, the rank of the vertex $v_{p}$ is at most by one larger than the rank of vertex $v_{q}$ (or by any number smaller). Formally, let $\mathcal{P}_{\mathit{de}}$ be the following predicate on macrostates of $\mathcal{B}_{\mathit{S}}$:

[TABLE]

where $\lceil\!\!\lceil x\rceil\!\!\rceil$ for $x\in\omega$ denotes the smallest even number greater or equal to $x$ and $\lceil\!\!\lceil\omega\rceil\!\!\rceil=\omega$. Similarly as above, we create a new procedure, called Purgede, which is obtained from Comp${}_{\text{S}}$ by modifying the definition of $\mathcal{B}_{\mathit{S}}$ such that all occurrences of $Q_{2}$ are substituted by $Q_{2}^{\mathit{de}}$ and

[TABLE]

We denote the BA obtained from Purgede as $\mathcal{B}_{\mathit{S}}^{\mathit{de}}$.

Lemma 3 ()

$\mathcal{L}(\mathcal{B}_{\mathit{S}}^{\mathit{de}})=\mathcal{L}(\mathcal{B}_{\mathit{S}})$**

The use of $\lceil\!\!\lceil f(q)\rceil\!\!\rceil$ in $\mathcal{P}_{\mathit{de}}$ results in the fact that the two purging techniques are incomparable. For instance, consider a macrostate $(\{p,q\},\emptyset,\{p\mapsto 2,q\mapsto 1\},0)$ such that $p\mathrel{\preceq_{\mathit{di}}}q$ and $p\mathrel{\preceq_{\mathit{de}}}q$. Then the macrostate will be purged in Purgedi, but not in Purgede.

The two techniques can, however, be easily combined into a third procedure Purgedi+de, when $Q_{2}$ is substituted in Comp${}_{\text{S}}$ with $Q_{2}^{\mathit{di+de}}$ defined as

[TABLE]

We denote the resulting BA as $\mathcal{B}_{\mathit{S}}^{\mathit{di+de}}$.

Lemma 4 ()

$\mathcal{L}(\mathcal{B}_{\mathit{S}}^{\mathit{di+de}})=\mathcal{L}(\mathcal{B}_{\mathit{S}})$**

4.1 Proofs of Lemmas 2, 3, and 4

We first give a lemma that an $x$-strategy $\sigma_{x}$ preserves an $x$-simulation $\mathrel{\preceq_{x}}$.

Lemma 5

Let $\mathrel{\preceq_{x}}$ be an $x$-simulation (for $x\in\{\mathit{di,de,f}\}$). Then, the following holds: $\forall p,q\in Q:p\mathrel{\preceq_{x}}q\land p\mathop{\xrightarrow{a}}p^{\prime}\in\delta\Rightarrow\exists q^{\prime}\in Q:q\mathop{\xrightarrow{a}}q^{\prime}\in\delta\land p^{\prime}\mathrel{\preceq_{x}}q^{\prime}$.

Proof

Let $p,q\in Q$ such that $p\mathrel{\preceq_{x}}q$ and $p\mathop{\xrightarrow{a}}p^{\prime}\in\delta$, and let $\pi_{p}$ be a trace starting from $p$ with the first transition $p\mathop{\xrightarrow{a}}p^{\prime}$. From the definition of $x$-simulation, there is a winning Duplicator strategy $\sigma_{x}$; let $\pi_{q}=\sigma_{x}(q^{\prime},\pi_{p})$ and let $q\mathop{\xrightarrow{a}}q^{\prime}$ be the first transition of $\pi_{q}$. Let $\pi_{p^{\prime}}$ and $\pi_{r^{\prime}}$ be traces obtained from $\pi_{p}$ and $\pi_{r}$ by removing their first transitions. It is easy to see that if $\mathcal{C}^{x}(\pi_{p},\pi_{r})$ then also $\mathcal{C}^{x}(\pi_{p^{\prime}},\pi_{r^{\prime}})$ for any $x\in\{\mathit{di,de,f}\}$. It follows that $\sigma_{x}$ is also a winning Duplicator strategy from $(p^{\prime},r^{\prime})$. ∎

Next, we focus on delayed simulation and the proof of Lemma 3. In the next lemma, we show that if there is a pair of vertices on some level of the run DAG where one vertex delay-simulates the other one, there exists a relation between their rankings. This will be used to purge some useless rankings from the complemented BA.

Lemma 6

Let $p,q\in Q$ such that $p\mathrel{\preceq_{\mathit{de}}}q$ and $\mathcal{G}_{\alpha}=(V,E)$ be the run DAG of $\mathcal{A}$ over $\alpha$. For all $i\geq 0$, it holds that $(p,i)\in V\wedge(q,i)\in V\Rightarrow\mathit{rank}_{\alpha}(p,i)\leq\lceil\!\!\lceil\mathit{rank}_{\alpha}(q,i)\rceil\!\!\rceil$.

Proof

Consider some $(p,i)\in V$ and $(q,i)\in V$. First, suppose that $\mathit{rank}_{\alpha}(q,i)=\omega$. Since the rank can be at most $\omega$, it will always hold that $\mathit{rank}_{\alpha}(p,i)\leq\lceil\!\!\lceil\mathit{rank}_{\alpha}(q,i)\rceil\!\!\rceil$.

On the other hand, suppose that $\mathit{rank}_{\alpha}(q,i)$ is finite, i.e., $\alpha_{i:\omega}$ is not accepted by $q$. Then, due to Lemma 1, $0\leq\mathit{rank}_{\alpha}(q,i)\leq 2n$. Because $p\mathrel{\preceq_{\mathit{de}}}q$, it holds that $\alpha_{i:\omega}$ is also not accepted by $p$, and therefore also $0\leq\mathit{rank}_{\alpha}(p,i)\leq 2n$. We now need to show that $0\leq\mathit{rank}_{\alpha}(p,i)\leq\lceil\!\!\lceil\mathit{rank}_{\alpha}(q,i)\rceil\!\!\rceil\leq 2n$.

Let $\{\mathcal{G}_{\alpha}^{k}\}_{k=0}^{2n+1}$ be the sequence of run DAGs obtained from $\mathcal{G}_{\alpha}$ in the ranking procedure from Section 2.2. In the following text we use the abbreviation $v\in\mathcal{G}_{\alpha}^{m}\setminus\mathcal{G}_{\alpha}^{n}$ for $v\in\mathcal{G}_{\alpha}^{m}\wedge v\notin\mathcal{G}_{\alpha}^{n}$. Since the rank of a node $(r,j)$ is given as the number $l$ s.t. $(r,j)\in\mathcal{G}_{\alpha}^{l}\setminus\mathcal{G}_{\alpha}^{l+1}$, we will finish the proof of this lemma by proving the following claim:

Claim

Let $k$ and $l$ be s.t. $(p,i)\in\mathcal{G}_{\alpha}^{k}\setminus\mathcal{G}_{\alpha}^{k+1}$ and $(q,i)\in\mathcal{G}_{\alpha}^{l}\setminus\mathcal{G}_{\alpha}^{l+1}$. Then $k\leq\lceil\!\!\lceil l\rceil\!\!\rceil$.

Proof: We prove the claim by induction on $l$.

• •

Base case: ($l=0$) Since we assume $\mathcal{A}$ is complete, no vertex in $\mathcal{G}_{\alpha}^{0}$ is finite.

($l=1$) We prove that if $(q,i)$ is endangered in $\mathcal{G}_{\alpha}^{1}$, then $(p,i)$ is endangered in $\mathcal{G}_{\alpha}^{1}$ as well (so both would be removed in $\mathcal{G}_{\alpha}^{2}$). For the sake of contradiction, assume that $(q,i)$ is endangered in $\mathcal{G}_{\alpha}^{1}$ and $(p,i)$ is not. Therefore, since $\mathcal{G}_{\alpha}^{1}$ contains no finite vertices, there is an infinite path $\pi$ from $(p,i)$ s.t. $\pi$ contains at least one accepting state. In the following, we abuse notation and, given a strategy $\sigma_{\mathit{de}}$ and a state $s\in Q$, use $\sigma_{\mathit{de}}((s,i),\pi)$ to denote the path $(s_{0},i)(s_{1},i+1)(s_{2},i+2)\ldots$ such that $s_{0}=s$ and $\forall j\geq 0$, it holds that $s_{j+1}=\sigma_{\mathit{de}}(s_{j},r_{i+j}\mathop{\xrightarrow{\alpha_{i+j}}}r_{i+j+1})$ where $\pi_{x}=(r_{x},x)$ for every $x\geq 0$. Since $p\mathrel{\preceq_{\mathit{de}}}q$, there is a corresponding infinite path $\pi^{\prime}=\sigma_{\mathit{de}}((q,i),\pi)$ that also contains at least one accepting state. Therefore, $(q,i)$ is not endangered, a contradiction to the assumption, so we conclude that $l=1\Rightarrow k=1$.

• •

Inductive step: We assume the claim holds for all $l<2j$ and prove the inductive step for even and odd steps independently.

($l=2j$) We prove that if $(q,i)$ is finite in $\mathcal{G}_{\alpha}^{l}$ (and therefore would be removed in $\mathcal{G}_{\alpha}^{l+1}$), then either $(p,i)\notin\mathcal{G}_{\alpha}^{l}$, or $(p,i)$ is also finite in $\mathcal{G}_{\alpha}^{l}$. For the sake of contradiction, we assume that $(q,i)$ is finite in $\mathcal{G}_{\alpha}^{l}$ and that $(p,i)$ is in $\mathcal{G}_{\alpha}^{l}$, but is not finite there (and, therefore, $k>l$). Since $(p,i)$ is not finite in $\mathcal{G}_{\alpha}^{l}$, there is an infinite path $\pi$ from $(p,i)$ in $\mathcal{G}_{\alpha}^{l}$. Because $p\mathrel{\preceq_{\mathit{de}}}q$, it follows that there is an infinite path $\pi^{\prime}=\sigma_{\mathit{de}}((q,i),\pi)$ in $\mathcal{G}_{\alpha}^{0}$ ($\pi^{\prime}$ is not in $\mathcal{G}_{\alpha}^{l}$ because $(q,i)$ is finite there). Using Lemma 5 (possibly multiple times) and the fact that $(q,i)$ is finite, we can find vertices $(p^{\prime},x)$ in $\pi$ and $(q^{\prime},x)$ in $\pi^{\prime}$ s.t. $p^{\prime}\mathrel{\preceq_{\mathit{de}}}q^{\prime}$ and $(q^{\prime},x)$ is not in $\mathcal{G}_{\alpha}^{l}$, therefore, $(q^{\prime},x)\in\mathcal{G}_{\alpha}^{e}\setminus\mathcal{G}_{\alpha}^{e+1}$ for some $e<l$. Because $(p^{\prime},x)\in\mathcal{G}_{\alpha}^{l}$ and it is not finite ($\pi$ is infinite), it follows that $(p^{\prime},x)\in\mathcal{G}_{\alpha}^{f}\setminus\mathcal{G}_{\alpha}^{f+1}$ for some $f>l$, and since $e<l<f$, we have that $f\not\leq e+1$, implying $f\not\leq\lceil\!\!\lceil e\rceil\!\!\rceil$, which is in contradiction to the induction hypothesis.

$(l=2j+1)$ We prove that if $(q,i)$ is endangered in $\mathcal{G}_{\alpha}^{l}$ (and therefore would be removed in $\mathcal{G}_{\alpha}^{l+1}$), then either $(p,i)\notin\mathcal{G}_{\alpha}^{l}$, or $(p,i)$ is removed at the latest in $\mathcal{G}_{\alpha}^{l+1}$. For the sake of contradiction, assume that $(q,i)$ is endangered in $\mathcal{G}_{\alpha}^{l}$ while $(p,i)$ is removed later than in $\mathcal{G}_{\alpha}^{l+1}$. Therefore, since $\mathcal{G}_{\alpha}^{l}$ contains no finite vertices (they were removed in the $(l-1)$-th step), there is an infinite path $\pi$ from $(p,i)$ s.t. $\pi$ contains at least one accepting state. Because $p\mathrel{\preceq_{\mathit{de}}}q$, there is a corresponding path $\pi^{\prime}=\sigma_{\mathit{de}}((q,i),\pi)$ from $(q,i)$ in $\mathcal{G}_{\alpha}^{0}$ that also contains at least one accepting state and moreover $\pi^{\prime}\notin\mathcal{G}_{\alpha}^{l}$. Since $\pi^{\prime}$ has an infinite number of states (and at least one accepting), not all states from $\pi^{\prime}$ were removed in $\mathcal{G}_{\alpha}^{l-1}$, i.e., there is at least one node with rank less or equal to $l-2$. Using Lemma 5 (also possibly multiple times) we can hence find states $(p^{\prime},x)$ in $\pi$ and $(q^{\prime},x)$ in $\pi^{\prime}$ s.t. $p^{\prime}\mathrel{\preceq_{\mathit{de}}}q^{\prime}$ and $(q^{\prime},x)$ is not in $\mathcal{G}_{\alpha}^{l}$ and has a rank less or equal to $l-2$, therefore, $(q^{\prime},x)\in\mathcal{G}_{\alpha}^{e}\setminus\mathcal{G}_{\alpha}^{e+1}$ for some $e<l-1$. Because $(p^{\prime},x)\in\mathcal{G}_{\alpha}^{l}$, it follows that $(p^{\prime},x)\in\mathcal{G}_{\alpha}^{f}\setminus\mathcal{G}_{\alpha}^{f+1}$ for some $f\geq l$, and, therefore, $f\not\leq e+1$, which is in contradiction to the induction hypothesis. $\blacksquare$

This concludes the proof. ∎

Lemma 7

Let $p,q\in Q$ such that $p\mathrel{\preceq_{\mathit{di}}}q$ and $\mathcal{G}_{\alpha}=(V,E)$ be the run DAG of $\mathcal{A}$ over $\alpha$. For all $i\geq 0$, it holds that $(p,i)\in V\wedge(q,i)\in V\Rightarrow\mathit{rank}_{\alpha}(p,i)\leq\mathit{rank}_{\alpha}(q,i)$.

Proof

Can be obtained as a simplified version of the proof of Lemma 6. ∎

We are now ready to prove Lemma 3.

See 3

Proof

• $(\subseteq)$

Follows directly from the fact that $\mathcal{B}_{\mathit{S}}^{\mathit{de}}$ is obtained by removing states from $\mathcal{B}_{\mathit{S}}$.

• $(\supseteq)$

Let $\alpha\in\mathcal{L}(\mathcal{B}_{\mathit{S}})$. As shown in the proof of Lemma 3.2 in [33], there are two cases. The first case is when all vertices of $\mathcal{G}_{\alpha}$ are finite, which we do not need to consider, since we assume complete automata.

The other case is when $\mathcal{G}_{\alpha}$ contains an infinite vertex. In this case, $\mathcal{B}_{\mathit{S}}$ contains an accepting run

[TABLE]

with

• –

$S_{0}=I,O_{p+1}=\emptyset$, and $i_{p+1}=0$,

• –

$S_{j+1}=\delta(S_{j},\alpha_{j})$ for all $j\in\omega$,

and, for all $j>p$,

• –

$O_{j+1}=f^{-1}_{j+1}(i_{j+1})$ if $O_{j}=\emptyset$ or

$O_{j+1}=\delta(O_{j},\alpha_{j})\cap f^{-1}_{j+1}(i_{j+1})$ if $O_{j}\neq\emptyset$, respectively,

• –

$f_{j}$ is the $S_{j}$-tight level ranking that maps each $q\in S_{j}$ to the rank of $(q,j)\in\mathcal{G}_{\alpha}$,

• –

$i_{j+1}=i_{j}$ if $O_{j}\neq\emptyset$ or

$i_{j+1}=(i_{j}+2)\mod(\mathit{rank}(f)+1)$ if $O_{j}=\emptyset$, respectively.

The ranks assigned by $f_{j}$ to states of $S_{j}$ match the ranks of the corresponding vertices in $\mathcal{G}_{\alpha}$.

$\circledast$ Using Lemma 6, we conclude that $\rho$ contains no macrostate $(S,O,f,j)$ where $f(p)>\lceil\!\!\lceil f(q)\rceil\!\!\rceil$ and $p\mathrel{\preceq_{\mathit{de}}}q$ for $p,q\in S$. Therefore, $\rho$ is also an accepting run in $\mathcal{B}_{\mathit{S}}^{\mathit{de}}$. (We use $\circledast$ to refer to this paragraph later.) ∎

See 2

Proof

The same as for Lemma 3 with $\circledast$ substituted by the following:

$\circledast$ Using Lemma 7, we conclude that $\rho$ contains no macrostate $(S,O,f,j)$ where $f(p)>f(q)$ and $p\mathrel{\preceq_{\mathit{di}}}q$ for $p,q\in S$. So $\rho$ is also an accepting run in $\mathcal{B}_{\mathit{S}}^{\mathit{di}}$.∎

See 4

Proof

The same as for Lemma 3 with $\circledast$ substituted by the following:

$\circledast$ Using Lemmas 7 and 6, we conclude that $\rho$ contains no macrostate $(S,O,f,j)$ where either $f(p)>f(q)$ and $p\mathrel{\preceq_{\mathit{di}}}q$, or $f(p)>\lceil\!\!\lceil f(q)\rceil\!\!\rceil$ and $p\mathrel{\preceq_{\mathit{de}}}q$ for $p,q\in S$. Therefore, $\rho$ is also an accepting run in $\mathcal{B}_{\mathit{S}}^{\mathit{di+de}}$. ∎

5 Saturation of Macrostates

Our second optimisation is inspired by an optimisation of determinisation of classical finite automata from [17, Section 5]. Their optimisation is based on saturating every constructed macrostate in the classical subset construction with all direct-simulation-smaller states. This can reduce the total number of states of the determinized automaton because two or more macrostates can be mapped to a single saturated macrostate. (In Section 5.2, we show why an analogue of their compression cannot be used.)

We show that a similar technique can be applied to BAs. We do not restrain ourselves to direct simulation, though, and generalize the technique to delayed simulation. In particular, in our optimisation, we saturate the $S$ components of macrostates $(S,O,f,i)$ obtained in Comp${}_{\text{S}}$ with all $\mathrel{\preceq_{\mathit{de}}}$-smaller states. Formally, we modify Comp${}_{\text{S}}$ by substituting the definition of the constructed transition function $\delta^{\prime}$ with $\delta_{\mathit{Sat}}^{\prime}$ defined as follows:

• •

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

• –

$\delta^{\mathit{Sat}}_{1}:Q_{1}\times\Sigma\to 2^{Q_{1}}$ with $\delta^{\mathit{Sat}}_{1}(S,a)=\{\mathit{cl}[\delta(S,a)]\}$,

• –

$\delta^{\mathit{Sat}}_{2}:Q_{1}\times\Sigma\to 2^{Q_{2}}$ with $\delta^{\mathit{Sat}}_{2}(S,a)=\{(S^{\prime},\emptyset,f,0)\mid S^{\prime}=\mathit{cl}[\delta(S,a)]\}$, and

• –

$\delta^{\mathit{Sat}}_{3}:Q_{2}\times\Sigma\to 2^{Q_{2}}$ with $(S^{\prime},O^{\prime},f^{\prime},i^{\prime})\in\delta^{\mathit{Sat}}_{3}((S,O,f,i),a)$ iff $S^{\prime}=\mathit{cl}[\delta(S,a)],f^{\prime}\mathrel{\leq^{S}_{a}}~{}f$, $\mathit{rank}(f)=\mathit{rank}(f^{\prime})$, and

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

• *

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

where $\mathit{cl}[S]=\{q\in Q~{}|~{}\exists s\in S:q\mathrel{\preceq_{\mathit{de}}}s\}$. We denote the obtained procedure as Saturate and the obtained BA as $\mathcal{B}_{\mathit{Sat}}$.

Lemma 8 ()

$\mathcal{L}(\mathcal{B}_{\mathit{Sat}})=\mathcal{L}(\mathcal{B}_{\mathit{S}})$**

Obviously, as direct simulation is stronger than delayed simulation, the previous technique can also use direct simulation only (e.g., when computing the full delayed simulation is computationally too demanding). Moreover, Saturate is also compatible with all Purgex algorithms for $x\in\{\mathit{di},\mathit{de},\mathit{di+de}\}$ (because they just remove macrostates with incompatible rankings from $Q_{2}$)—we call the combined versions Purgex ​​​+Saturate and the complement BAs they output $\mathcal{B}^{x}_{\mathit{Sat}}$.

Lemma 9 ()

$\mathcal{L}(\mathcal{B}^{\mathit{di}}_{\mathit{Sat}})=\mathcal{L}(\mathcal{B}^{\mathit{de}}_{\mathit{Sat}})=\mathcal{L}(\mathcal{B}^{\mathit{di+de}}_{\mathit{Sat}})=\mathcal{L}(\mathcal{B}_{\mathit{S}})$**

5.1 Proofs of Lemmas 8 and 9

We start with a lemma, used later, that talks about languages of states related by delayed simulation when there is a path between them.

Lemma 10

For $p,q\in Q$ such that $p\mathrel{\preceq_{\mathit{de}}}q$, let $L_{\top}=\{w\in\Sigma^{*}~{}|~{}p\overset{w}{\underset{F}{\leadsto}}q\}$ and $L_{\bot}=\{w\in\Sigma^{*}~{}|~{}p\overset{w}{\leadsto}q\}$. Then $L(q)\supseteq(L_{\bot}^{*}L_{\top})^{\omega}$.

Proof

First we prove the following claim:

Claim

For every word $\alpha=w_{0}w_{1}w_{2}\dots\in\Sigma^{\omega}$ where $w_{i}\in L_{\top}\cup L_{\bot}$, we can construct a trace $\pi=p\overset{w_{0}}{\leadsto}q_{0}\overset{w_{1}}{\leadsto}q_{1}\overset{w_{2}}{\leadsto}\cdots$ over $\alpha$ such that $p\mathrel{\preceq_{\mathit{de}}}q_{0}$ and $q_{i}\mathrel{\preceq_{\mathit{de}}}q_{i+1}$ for all $i\geq 0$.

Proof: We assign $q_{0}:=q$ and construct the rest of $\pi$ by the following inductive construction.

• •

Base case: ($i=0$) From the assumption it holds that $p\overset{w_{1}}{\leadsto}q_{0}$ and $p\mathrel{\preceq_{\mathit{de}}}q_{0}$. From Lemma 5 there is some $r\in Q$ s.t. $q_{0}\overset{w_{1}}{\leadsto}r$ and $q_{0}\mathrel{\preceq_{\mathit{de}}}r$. We assign $q_{1}:=r$, so $q_{0}\mathrel{\preceq_{\mathit{de}}}q_{1}$.

• •

Inductive step: Let $\pi^{\prime}=p\overset{w_{0}}{\leadsto}q_{0}\overset{w_{1}}{\leadsto}\cdots\overset{w_{i}}{\leadsto}q_{i}$ be a prefix of a trace such that $q_{j}\mathrel{\preceq_{\mathit{de}}}q_{j+1}$ for every $j<i$. From the transitivity of $\mathrel{\preceq_{\mathit{de}}}$, it follows that $p\mathrel{\preceq_{\mathit{de}}}q_{i}$. From Lemma 5 there is some $r\in Q$ s.t. $q_{i}\overset{w_{i}}{\leadsto}r$ and $q\mathrel{\preceq_{\mathit{de}}}r$. We assign $q_{i+1}:=r$, so $q_{i}\mathrel{\preceq_{\mathit{de}}}q_{i+1}$. $\blacksquare$

Consider a word $\alpha\in(L_{\bot}^{*}L_{\top})^{\omega}$ such that $\alpha=w_{0}w_{1}w_{2}\dots$ for $w_{i}\in L_{\top}\cup L_{\bot}$. We show that $\alpha\in\mathcal{L}(q)$. According to the previous claim, we can construct a trace $\pi=p\overset{w_{0}}{\leadsto}q=q_{0}\overset{w_{1}}{\leadsto}q_{1}\overset{w_{2}}{\leadsto}\cdots$ over $\alpha$ s.t. $p\mathrel{\preceq_{\mathit{de}}}q_{0}$ and $q_{i}\mathrel{\preceq_{\mathit{de}}}q_{i+1}$ for all $i\geq 0$. Since $p\mathrel{\preceq_{\mathit{de}}}q$, from Lemma 5 it follows that we can construct a trace $\pi^{\prime}=q\overset{w_{0}}{\leadsto}r_{0}\overset{w_{1}}{\leadsto}r_{1}\overset{w_{2}}{\leadsto}\cdots$ s.t. $q_{i}\mathrel{\preceq_{\mathit{de}}}r_{i}$ for every $i\geq 0$. Because $\alpha$ contains infinitely often a subword from $L_{\top}$, there is some $\ell\in\omega$ such that $q_{\ell}\overset{w_{\ell}}{\leadsto}q_{\ell+1}$ and $r_{\ell}\overset{w_{\ell}}{\leadsto}r_{\ell+1}$ for $w_{\ell}\in L_{\top}$. Note that it holds that $p\mathrel{\preceq_{\mathit{de}}}q_{\ell}\mathrel{\preceq_{\mathit{de}}}r_{\ell}$. We can again use the claim above to construct a trace $\pi^{\star}=p\overset{w_{\ell}}{\underset{F}{\leadsto}}q=s_{0}\overset{w_{\ell+1}}{\leadsto}s_{1}\overset{w_{\ell+2}}{\leadsto}\cdots$ over $\alpha_{\ell}=w_{\ell}w_{\ell+1}w_{\ell+2}\dots$ such that $p\mathrel{\preceq_{\mathit{de}}}s_{0}$ and $s_{i}\mathrel{\preceq_{\mathit{de}}}s_{i+1}$ for all $i\geq 0$. Since $p\mathrel{\preceq_{\mathit{de}}}r_{\ell}$, we can simulate $\pi^{\star}$ from $r_{\ell}$ by a trace $\pi^{\star\prime}$, and because $p\overset{w_{\ell}}{\underset{F}{\leadsto}}q$, we know that $\pi^{\star\prime}$ will touch an accepting state in finitely many steps (this holds because $w_{\ell}$ is from $L_{\top}$, which are the words over which we can go from $p$ to $q$ and touch an accepting state). Consider $m\geq\ell$ such that $s_{m}$ is the first state after the accepting state that is one of the $\{s_{0},s_{1},\ldots\}$ in $\pi^{\star\prime}$. This reasoning could be repeated for all occurrences of a subword from $L_{\top}$ in $\pi^{\star}$, therefore $\alpha\in\mathcal{L}(q)$. ∎

Next, we give a lemma used for establishing correctness of saturating macrostates with $\mathrel{\preceq_{\mathit{de}}}$-smaller states.

Lemma 11

Let $p,q,r\in Q$ such that $r\mathop{\xrightarrow{a}}q\in\delta$ and $p\mathrel{\preceq_{\mathit{de}}}q$. Further, let $\mathcal{A}^{\prime}=(Q,\delta^{\prime},I,F)$ where $\delta^{\prime}=\delta\cup\{r\mathop{\xrightarrow{a}}p\}$. Then $\mathcal{L}(\mathcal{A})=\mathcal{L}(\mathcal{A}^{\prime})$.

Proof

• $(\subseteq)$

Clear.

• $(\supseteq)$

Consider some $\alpha\in\mathcal{L}(\mathcal{A}^{\prime})$ and an accepting trace $\pi$ in $\mathcal{A}^{\prime}$ over $\alpha$. There are two cases:

($\pi$ contains only finitely many transitions $r\mathop{\xrightarrow{a}}p$)

In this case, $\pi$ is of the form $\pi=\pi_{i}\pi_{\omega}$ where $\pi_{i}$ is a finite prefix $\pi_{i}=q_{0}\overset{w_{0}}{\leadsto}r\mathop{\xrightarrow{a}}p\overset{w_{1}}{\leadsto}r\mathop{\xrightarrow{a}}p\overset{w_{2}}{\leadsto}\cdots\overset{w_{n}}{\leadsto}r\mathop{\xrightarrow{a}}p$, for $q_{0}\in I$, and $\pi_{\omega}$ is an infinite trace from $p$ that does not contain any occurrence of the transition $r\mathop{\xrightarrow{a}}p$. We construct in $\mathcal{A}$ a trace $\pi^{\prime}=q_{0}\overset{w_{0}}{\leadsto}r\mathop{\xrightarrow{a}}q\overset{w_{1}}{\leadsto}r_{1}\mathop{\xrightarrow{a}}q_{1}\overset{w_{2}}{\leadsto}\cdots\overset{w_{n}}{\leadsto}r_{n}\mathop{\xrightarrow{a}}q_{n}.\pi^{\prime}_{\omega}$ as follows. Let $\sigma_{\mathit{de}}$ be a strategy for $\mathrel{\preceq_{\mathit{de}}}$. We set $r_{1}:=\sigma_{\mathit{de}}(q,p\overset{w_{1}}{\leadsto}r)$, so $r\mathrel{\preceq_{\mathit{de}}}r_{1}$. Since $r\mathop{\xrightarrow{a}}q\in\delta$, it follows that there is $r_{1}\mathop{\xrightarrow{a}}q_{1}\in\delta$ such that $p\mathrel{\preceq_{\mathit{de}}}q_{1}$. For $i>1$, we set $r_{i}:=\sigma_{\mathit{de}}(q_{i-1},p\overset{w_{i}}{\leadsto}r)$. By induction, it follows that $\forall 1\leq i\leq n:p\mathrel{\preceq_{\mathit{de}}}q_{i}$, in particular $p\mathrel{\preceq_{\mathit{de}}}q_{n}$. We set $\pi^{\prime}_{\omega}:=\sigma_{\mathit{de}}(q_{n},\pi_{\omega})$. Since $\pi_{\omega}$ starts in $p$ and contains infinitely many accepting states and $\pi^{\prime}_{\omega}$ starts in $q_{n}$ and $p\mathrel{\preceq_{\mathit{de}}}q_{n}$, then $\pi^{\prime}_{\omega}$ also contains infinitely many accepting states. It follows that $\pi^{\prime}$ is accepting, so $\alpha\in\mathcal{L}(\mathcal{A})$. 2. 2.

($\pi$ contains infinitely many transitions $r\mathop{\xrightarrow{a}}p$)

In this case, $\pi$ is of the form $\pi=q_{0}\overset{w_{0}}{\leadsto}r\mathop{\xrightarrow{a}}p\overset{w_{1}}{\leadsto}r\mathop{\xrightarrow{a}}p\overset{w_{2}}{\leadsto}\cdots\overset{w_{n}}{\leadsto}r\mathop{\xrightarrow{a}}p\overset{w_{\omega}}{\leadsto}\cdots$, for $q_{0}\in I$ and $\alpha=w_{0}aw_{1}aw_{2}\dots$ Since $\pi$ is accepting, for infinitely many $i\in\omega$, we have $p\overset{w_{i}a}{\underset{F}{\leadsto}}p$ in $\mathcal{A}^{\prime}$ and hence also $p\overset{w_{i}a}{\underset{F}{\leadsto}}q$ in the original BA $\mathcal{A}$. Using Lemma 10 and the fact that $p\mathrel{\preceq_{\mathit{de}}}q$, we have $w_{1}aw_{2}a\dots\in L(q)$ and hence $\alpha=w_{0}aw_{1}aw_{2}a\dots\in\mathcal{L}(\mathcal{A})$. ∎

The following lemma guarantees that adding transitions in the way of Lemma 11 does not break the computed delayed simulation and can, therefore, be performed repeatedly, without the need to recompute the simulation.

Lemma 12

Let $\mathrel{\preceq_{\mathit{de}}}$ be the delayed simulation on $\mathcal{A}$. Further, let $p,q,r\in Q$ be such that $r\mathop{\xrightarrow{a}}q\in\delta$ and $p\mathrel{\preceq_{\mathit{de}}}q$, and let $\mathcal{A}^{\prime}=(Q,\delta^{\prime},I,F)$ where $\delta^{\prime}=\delta\cup\{r\mathop{\xrightarrow{a}}p\}$. Then $\mathrel{\preceq_{\mathit{de}}}$ is included in the delayed simulation on $\mathcal{A}^{\prime}$.

Proof

Let $\sigma_{\mathit{de}}$ be a dominating strategy compatible with $\mathrel{\preceq_{\mathit{de}}}$ and $\sigma_{\mathit{de}}^{\prime}$ be a strategy defined for all $s\in Q$ such that $r\mathrel{\preceq_{\mathit{de}}}s$ as $\sigma_{\mathit{de}}^{\prime}(s,x)=\sigma_{\mathit{de}}(s,x)$ when $x\neq(r\mathop{\xrightarrow{a}}p)$ and $\sigma_{\mathit{de}}^{\prime}(s,r\mathop{\xrightarrow{a}}p)=\sigma_{\mathit{de}}(s,r\mathop{\xrightarrow{a}}q)$. Note that $\sigma_{\mathit{de}}^{\prime}$ is also dominating wrt $\mathrel{\preceq_{\mathit{de}}}$. This can be shown by the following proof by contradiction: Suppose $\sigma_{\mathit{de}}^{\prime}$ is not dominating; then there is a strategy $\rho$ such that $\sigma_{\mathit{de}}^{\prime}(s,r\mathop{\xrightarrow{a}}p)$ must be simulated by $\rho(s,r\mathop{\xrightarrow{a}}p)=t$. But then $\sigma_{\mathit{de}}(s,r\mathop{\xrightarrow{a}}q)$ must also (transitivity of simulation) be simulated by $t$, so $\sigma_{\mathit{de}}$ is not dominating. Contradiction.

Further, let $t,u\in Q$ be such that $t\mathrel{\preceq_{\mathit{de}}}u$. Let $\pi_{t}=t\overset{w_{1}}{\leadsto}t_{f}\overset{w_{2}}{\leadsto}r\mathop{\xrightarrow{a}}p.\pi^{\prime}_{t}$ be a trace over $\alpha=w_{1}w_{2}aw_{\omega}\in\Sigma^{\omega}$ in $\mathcal{A}^{\prime}$ such that $t_{f}$ is an accepting state and $t_{f}\overset{w_{2}}{\leadsto}r$ does not contain any occurrence of $r\mathop{\xrightarrow{a}}p$. Further, let $\pi_{u}=u_{0}\overset{w_{1}}{\leadsto}u_{f}\overset{w_{2}}{\leadsto}u_{i}\mathop{\xrightarrow{a}}u_{i+1}.\pi^{\prime}_{u}$ be a trace corresponding to a run $u_{0}u_{1}u_{2}\dots$ over $\alpha$ in $\mathcal{A}$, where $u_{0}=u$, constructed as $\pi_{u}=\sigma_{\mathit{de}}^{\prime}(u,\pi_{t})$.

Claim

There is a trace $\pi_{v}=t\overset{w_{1}}{\leadsto}v_{f}.\pi_{v}^{\prime}$ over $\alpha$ such that $\pi^{\prime}_{v}$ contains an accepting state and $\pi_{v}$ is $\mathrel{\preceq_{\mathit{de}}}$-simulated by $\pi_{u}$ at every position.

Proof: We have the following two cases:

• •

($t\overset{w_{1}}{\leadsto}t_{f}$ does not contain any occurrence of $r\mathop{\xrightarrow{a}}p$)

Let $\pi_{v}=t\overset{w_{1}}{\leadsto}t_{f}\overset{w_{2}}{\leadsto}r\mathop{\xrightarrow{a}}q.\pi^{\prime}_{v}$ be a trace in $\mathcal{A}$ over $\alpha$ obtained from $\pi_{t}$ by starting with its prefix up to $r$, taking $r\mathop{\xrightarrow{a}}q$, and continuing with $\pi^{\prime}_{v}=\sigma_{\mathit{de}}^{\prime}(q,\pi^{\prime}_{t})$. Since in $\pi_{v}$, it holds that $t_{f}$ is at the same position as $t_{f}$ in $\pi_{t}$, the first part of the claim holds. Further, $\pi_{u}$ clearly $\mathrel{\preceq_{\mathit{de}}}$-simulates $\pi_{v}$ on $t\overset{w_{1}}{\leadsto}t_{f}\overset{w_{2}}{\leadsto}r$, and because $\sigma_{\mathit{de}}^{\prime}$ simulates $r\mathop{\xrightarrow{a}}p$ by a transition to a state $u_{i+1}$ such that $q\mathrel{\preceq_{\mathit{de}}}u_{i+1}$ and $\pi^{\prime}_{v}$ is constructed using $\sigma_{\mathit{de}}^{\prime}$, then also the second part of the claim holds.

• •

($t\overset{w_{1}}{\leadsto}t_{f}$ contains at least one occurrence of $r\mathop{\xrightarrow{a}}p$)

Suppose that $\pi_{t}$ starts with $t\overset{w_{11}}{\leadsto}r\mathop{\xrightarrow{a}}p\overset{w_{12}}{\leadsto}t_{f}$ such that $t\overset{w_{11}}{\leadsto}r$ does not contain any $r\mathop{\xrightarrow{a}}p$. Then let us start building $\pi_{v}$ such that it starts with $t\overset{w_{11}}{\leadsto}r\mathop{\xrightarrow{a}}q$. On this prefix, $\pi_{v}$ is clearly $\mathrel{\preceq_{\mathit{de}}}$-simulated by the corresponding prefix of $\pi_{u}$. We continue from $q$ using the strategy $\sigma_{\mathit{de}}^{\prime}$. In particular, the next time we reach $r\mathop{\xrightarrow{a}}p$ in $\pi_{t}$ while we are at some state $v_{1}$ such that $r\mathrel{\preceq_{\mathit{de}}}v_{1}$, we simulate the transition by $\sigma_{\mathit{de}}^{\prime}(v_{1},r\mathop{\xrightarrow{a}}p)$ and so on. We can observe that when we arrive to $t_{f}$ in $\pi_{t}$, we also arrive to $v_{f}$ in $\pi_{v}$ such that $t_{f}\mathrel{\preceq_{\mathit{de}}}v_{f}$. Therefore, $\pi^{\prime}_{v}$ contains an accepting state. Moreover, since $\sigma_{\mathit{de}}^{\prime}$ is dominating, the second part of the claim also holds. $\blacksquare$

From the claim above, it follows that the trace $u_{f}\overset{w_{2}}{\leadsto}u_{i}\mathop{\xrightarrow{a}}u_{i+1}.\pi^{\prime}_{u}$ contains an accepting state, so $\mathcal{C}^{\mathit{de}}(\pi_{t},\pi_{u})$. ∎

Finally, we are ready to prove Lemma 8.

See 8

Proof

• $(\subseteq)$

Let $\alpha\in\mathcal{L}(\mathcal{B}_{\mathit{Sat}})$ and $\rho$ be an arbitrary accepting run over $\alpha$ in $\mathcal{B}_{\mathit{Sat}}$ such that $\rho=S_{0}S_{1}\dots S_{n-1}(S_{n},O_{n},f_{n},i_{n})(S_{n+1},O_{n+1},f_{n+1},i_{n+1})\dots$. For the sake of contradiction, assume that $\alpha\in\mathcal{L}(\mathcal{A})$, therefore, there is a run $\rho^{\prime}$ on $\alpha$ in $\mathcal{A}$ having infinitely many accepting states. From the fact that tight level rankings form a non-increasing sequence, we have that $f_{n}(\rho^{\prime}(n))\geq f_{n+1}(\rho^{\prime}(n+1))\geq\cdots$. This sequence eventually stabilizes and from the property of level rankings and the fact that $\rho^{\prime}$ is accepting, it stabilizes in some $\ell$ such that $f_{\ell}(\rho^{\prime}(\ell))$ is even. This, however, means that the $O$ component of macrostates in $\rho$ cannot be emptied infinitely often, and, therefore, $\rho$ is not accepting, which is a contradiction. Hence $\alpha\notin\mathcal{L}(\mathcal{A})$, so (from Proposition 1) $\alpha\in\mathcal{L}(\mathcal{B}_{\mathit{S}})$.

• $(\supseteq)$

Consider some $\alpha\in\mathcal{L}(\mathcal{B}_{\mathit{S}})$. Let $\mathcal{A}^{\prime}$ be a BA obtained from $\mathcal{A}$ by adding transitions according to Lemma 12. Then from Lemma 11, we have that $\mathcal{L}(\mathcal{A})=\mathcal{L}(\mathcal{A}^{\prime})$. Therefore, $\alpha\in\mathcal{L}(\mathcal{B}_{\mathit{S}}^{\prime})$ where $\mathcal{B}_{\mathit{S}}^{\prime}$ is the BA obtained from $\mathcal{A}^{\prime}$ using Comp${}_{\text{S}}$. It is easy to see that we can construct a run in $\mathcal{B}_{\mathit{Sat}}$ that mimics the levels of run DAG of $\alpha$ in $\mathcal{A}^{\prime}$ (i.e., we are able to empty the $O$ component infinitely often). Hence $\alpha\in\mathcal{L}(\mathcal{B}_{\mathit{Sat}})$. ∎

See 9

Proof

• $(\subseteq)$

This part is the same as in the proof of Lemma 8.

• $(\supseteq)$

Consider some $\alpha\in\mathcal{L}(\mathcal{B}_{\mathit{S}})$. Let $\mathcal{A}^{\prime}$ be a BA obtained from $\mathcal{A}$ by adding transitions according to Lemma 12. Then from Lemma 11, we have that $\mathcal{L}(\mathcal{A})=\mathcal{L}(\mathcal{A}^{\prime})$. Therefore, $\alpha\in\mathcal{L}(\mathcal{B}_{\mathit{S}}^{\prime})$ where $\mathcal{B}_{\mathit{S}}^{\prime}$ is the BA obtained from $\mathcal{A}^{\prime}$ using Comp${}_{\text{S}}$. It is easy to see that we can construct a run in $\mathcal{B}_{\mathit{Sat}}$ that mimics the levels of run DAG of $\alpha$ in $\mathcal{A}^{\prime}$ (i.e., we are able to empty the $O$ component infinitely often). Using Lemmas 7 and 6, we can conclude that the run contains no macrostate of the form $(S,O,f,j)$, where $f(p)>f(q)$ and $p\mathrel{\preceq_{\mathit{di}}}q$, or $f(p)>\lceil\!\!\lceil f(q)\rceil\!\!\rceil$ and $p\mathrel{\preceq_{\mathit{de}}}q$ for $p,q\in S$. Therefore, $\rho$ is also an accepting run in $\mathcal{B}^{\mathit{di+de}}_{\mathit{Sat}}$. Hence $\alpha\in\mathcal{L}(\mathcal{B}^{\mathit{di+de}}_{\mathit{Sat}})$. ∎

5.2 Remarks on Compression of Macrostates

An analogy to saturation of macrostates is their compression [17, Section 6], based on removing simulation-smaller states from a macrostate. This is, however, not possible even for direct simulation, as we can see in the following example.

Example 1

Consider the BA over $\Sigma=\{a\}$ given below.

p$$q$$r$$a$$a$$a$$a$$a

For this BA we have $q\mathrel{\preceq_{\mathit{di}}}r$ and $r\mathrel{\preceq_{\mathit{di}}}q$. If we compress the macrostates obtained in Comp${}_{\text{S}}$, there is the following trace in the output automaton:

[TABLE]

This trace contains infinitely many final states (we flush the $O$-set infinitely often), hence we are able to accept the word $a^{\omega}$, which is, however, in the language of the input BA. ∎

6 Use after Simulation Quotienting

In this short section, we establish that our optimizations introduced in Sections 4 and 5 can be applied with no additional cost in the setting when BA complementation is preceded with simulation-based reduction of the input BA (which is usually helpful), i.e., when the simulation is already computed beforehand for another purpose. In particular, we show that simulation-based reduction preserves the simulation (when naturally extended to the quotient automaton). First, let us formally define the operation of quotienting.

Given an $x$-simulation $\mathrel{\preceq_{x}}$ for $x\in\{\mathit{di},\mathit{de}\}$, we use $\mathrel{\mathrel{\approx}_{x}}$ to denote the $x$-similarity relation (i.e., the symmetric fragment) ${\mathrel{\mathrel{\approx}_{x}}}={\mathrel{\preceq_{x}}}\cap{\preceq_{x}^{-1}}$. Note that since $\mathrel{\preceq_{x}}$ is a preorder, it holds that $\mathrel{\mathrel{\approx}_{x}}$ is an equivalence. We use $[q]_{x}$ to denote the equivalence class of $q$ wrt $\mathrel{\mathrel{\approx}_{x}}$. The quotient of a BA $\mathcal{A}=(Q,\delta,I,F)$ wrt $\mathrel{\mathrel{\approx}_{x}}$ is the automaton

[TABLE]

with the transition function $\delta_{\mathrel{\mathrel{\approx}_{x}}}([q]_{x},a)=\{[r]_{x}\mid r\in\delta([q]_{x},a)\}$ and the set of initial and accepting states $I_{\mathrel{\mathrel{\approx}_{x}}}=\{[q]_{x}\in Q/{\mathrel{\mathrel{\approx}_{x}}}\mid q\in I\}$ and $F_{\mathrel{\mathrel{\approx}_{x}}}=\{[q]_{x}\in Q/{\mathrel{\mathrel{\approx}_{x}}}\mid q\in F\}$ respectively.

Proposition 2 ([7], [12])

If $x\in\{\mathit{di},\mathit{de}\}$, then $\mathcal{L}(\mathcal{A}/{\mathrel{\mathrel{\approx}_{x}}})=\mathcal{L}(\mathcal{A})$.

Remark 1 ([12])

$\mathcal{L}(\mathcal{A}/{\mathrel{\mathrel{\approx}_{f}}})\neq\mathcal{L}(\mathcal{A})$

Finally, the following lemma shows that quotienting preserves direct and delayed simulations, therefore, when complementing $\mathcal{A}$, it is possible to first quotient $\mathcal{A}$ wrt a direct/delayed simulation and then use the same simulation (lifted to the states of the quotient automaton) to optimize the complementation.

Lemma 13 ()

Let $\mathrel{\preceq_{x}}$ be the $x$-simulation on $\mathcal{A}$ for $x\in\{\mathit{di},\mathit{de}\}$. Then the relation $\mathrel{\preceq^{\mathrel{\approx}}_{x}}$ defined as $[q]_{x}\mathrel{\preceq^{\mathrel{\approx}}_{x}}[r]_{x}$ iff $q\mathrel{\preceq_{x}}r$ is the $x$-simulation on $\mathcal{A}/{\mathrel{\mathrel{\approx}_{x}}}$.

Proof

First, we show that $\mathrel{\preceq^{\mathrel{\approx}}_{x}}$ is well defined, i.e., if $q\mathrel{\preceq_{x}}r$, then for all $q^{\prime}\in[q]_{x}$ and $r^{\prime}\in[r]_{x}$, it holds that $q^{\prime}\mathrel{\preceq_{x}}r^{\prime}$. Indeed, this holds because $q^{\prime}\mathrel{\mathrel{\approx}_{x}}q$ and $r\mathrel{\mathrel{\approx}_{x}}r$, and therefore $q^{\prime}\mathrel{\preceq_{x}}q\mathrel{\preceq_{x}}r\mathrel{\preceq_{x}}r^{\prime}$; the transitivity of simulation yields $q^{\prime}\mathrel{\preceq_{x}}r^{\prime}$.

Next, let $\sigma_{x}$ be a strategy that gives $\mathrel{\preceq_{x}}$. Consider a trace defined as $[\pi_{q}]_{x}=[q_{0}]_{x}\mathop{\xrightarrow{\alpha_{0}}}[q_{1}]_{x}\mathop{\xrightarrow{\alpha_{1}}}\cdots$ over a word $\alpha\in\Sigma^{\omega}$ in $\mathcal{A}/{\mathrel{\mathrel{\approx}_{x}}}$. Then,

for $x=\mathit{di}$ there is a trace $\pi_{q}=q_{0}^{\prime}\mathop{\xrightarrow{\alpha_{0}}}q_{1}^{\prime}\mathop{\xrightarrow{\alpha_{1}}}\cdots$ in $\mathcal{A}$ s.t. $q_{0}^{\prime}\in[q_{0}]_{x}$ and $q_{i}\mathrel{\preceq_{x}}q_{i}^{\prime}$ for $i\geq 0$. Therefore, if $[q_{i}]_{x}$ is accepting then so is $q_{i}^{\prime}$; 2. 2.

for $x=\mathit{de}$ there is a trace $\pi_{q}=q_{0}^{\prime}\mathop{\xrightarrow{\alpha_{0}}}q_{1}^{\prime}\mathop{\xrightarrow{\alpha_{1}}}\cdots$ in $\mathcal{A}$ s.t. $q_{0}^{\prime}\in[q_{0}]_{x}$, $q_{i}\mathrel{\preceq_{x}}q_{i}^{\prime}$ for $i\geq 0$ and, moreover, if $[q_{i}]_{x}$ is accepting then there is $q_{k}^{\prime}$ for $k\geq i$ s.t. $q_{k}^{\prime}\in F$.

Further, let $[q_{0}]_{x}\mathrel{\preceq^{\mathrel{\approx}}_{x}}[r_{0}]_{x}$. Then there is a trace $\pi_{r}=\sigma_{x}(r,\pi_{q})=(r=r_{0})\mathop{\xrightarrow{\alpha_{0}}}r_{1}\mathop{\xrightarrow{\alpha_{1}}}\cdots$ simulating $\pi_{q}$ in $\mathcal{A}$ from $r$. Further, consider its projection $[\pi_{r}]_{x}=[r_{0}]_{x}\mathop{\xrightarrow{\alpha_{0}}}[r_{1}]_{x}\mathop{\xrightarrow{\alpha_{1}}}\cdots$ into $\mathcal{A}/{\mathrel{\mathrel{\approx}_{x}}}$. For all $i\geq 0$, we have that $q_{i}\mathrel{\preceq_{x}}r_{i}$, and therefore also $[q_{i}]_{x}\mathrel{\preceq^{\mathrel{\approx}}_{x}}[r_{i}]_{x}$. Since $\mathcal{C}^{x}(\pi_{q},\pi_{r})$, then also $\mathcal{C}^{x}([\pi_{q}]_{x},[\pi_{r}]_{x})$.

Finally, we show that $\mathrel{\preceq^{\mathrel{\approx}}_{x}}$ is maximal. For the sake of contradiction, suppose that $[r]_{x}$ is $x$-simulating $[q]_{x}$ for some $q,r\in Q$ s.t. $q\not\mathrel{\preceq_{x}}r$. Consider a word $\alpha\in\Sigma^{\omega}$ and a trace $\pi_{q}=(q=q_{0})\mathop{\xrightarrow{\alpha_{0}}}q_{1}\mathop{\xrightarrow{\alpha_{1}}}\cdots$ over $\alpha$ in $\mathcal{A}$. Then there is a trace $[\pi_{q}]_{x}=[q=q_{0}]_{x}\mathop{\xrightarrow{\alpha_{0}}}[q_{1}]_{x}\mathop{\xrightarrow{\alpha_{1}}}\cdots$ over $\alpha$ in $\mathcal{A}/{\mathrel{\mathrel{\approx}_{x}}}$. According to the assumption, there is also a trace $[\pi_{r}]_{x}=[r=r_{0}]_{x}\mathop{\xrightarrow{\alpha_{0}}}[r_{1}]_{x}\mathop{\xrightarrow{\alpha_{1}}}\cdots$ such that $[\pi_{r}]_{x}$ is $x$-simulating $[\pi_{q}]_{x}$. But then there will also exist a trace $\pi_{r}=(r=r_{0})\mathop{\xrightarrow{\alpha_{0}}}r_{1}^{\prime}\mathop{\xrightarrow{\alpha_{1}}}r_{1}^{\prime}\mathop{\xrightarrow{\alpha_{2}}}\cdots$ such that $r_{i}\mathrel{\preceq_{x}}r_{i}^{\prime}$ for all $i\in\omega$ and $\mathcal{C}^{x}(\pi_{q},\pi_{r})$ (see the previous part of the proof). Therefore, since $\mathrel{\preceq_{x}}$ is maximal, we have that $q\mathrel{\preceq_{x}}r$, which is in contradiction with the assumption. ∎

7 Experimental Evaluation

We implemented our optimisations in a prototype tool222https://github.com/vhavlena/ba-complement written in Haskell and performed preliminary experimental evaluation on a set of 124 random BAs with a non-trivial language over a two-symbol alphabet generated using Tabakov and Vardi’s model [37]. The parameters of input automata were set to the following bounds: number of states: 6–7, transition density: 1.2–1.3, and acceptance density: 0.35–0.5. Before complementing, the BAs were quotiented wrt the direct simulation for experiments with Purgedi and the delayed simulation for experiments with Purgede and Purgedi+de. The timeout was set to 300 s.

We present the results for our strongest optimizations for outputs of the size up to 500 states in Fig. 1. As can be seen in Fig. 1(a), purging alone often significantly reduces the size of the output. The situation with saturation is, on the other hand, more complicated. In Fig. 1(b), we can see that in some cases, the saturation produces even smaller BAs than only purging, on the other hand, in some cases, larger BAs are produced. This is expected, because saturating the $S$ component of macrostates also means that more level rankings (the $f$ component) need to be considered.

For outputs of a larger size (we had 11 of them), the results follow a similar trend, but the probability that saturation will increase the size of the result decreases. For some concrete results, for one BA, the size of the output BA decreased from 4065 (Comp${}_{\text{S}}$) to 985 (Purgedi+de) to 929 (Purgedi+de ​​​+Saturate), which yields a reduction to 24 %, resp. 22 %! Further, we observed that all Purgex methods usually give similar results, with the difference of only a few states (when Purgedi and Purgede differ, Purgedi usually wins over Purgede).

8 Related Work

BA complementation has a long research track. Known approaches can be roughly classified into Ramsey-based [34], determinization-based [32, 29], rank-based [33], slice-based [23, 39], learning-based [25], and the recently proposed subset-tuple construction [4]. Those approaches build on top of different concepts of capturing words accepted by a complement automaton. Some concepts can be translated into others, such as the slice-based approach, which can be translated to the rank-based approach [40]. Such a translation can help us get a deeper understanding of the BA complementation problem and the relationship between optimization techniques for different complementation algorithms.

Because of the high computational complexity of complementing a BA, and, consequently, also checking BA inclusion and universality (which use complementation as their component), there has been some effort to develop heuristics that help to reduce the number of explored states in practical cases. The most prominent ones are heuristics that leverage various notions of simulation relations, which often provide a good compromise between the overhead they impose and the achieved state space reduction. Direct [7, 36], delayed [12], fair [12], their variants for alternating Büchi automata [16], and multi-pebble simulations [13] are the best-studied relations of this kind. Some of the relations can be used quotienting, but also for pruning transitions entering simulation-smaller states (which may cause some parts of the BA to become inaccessible). A series of results in this direction was recently developed by Clemente and Mayr [10, 26, 27].

Not only can the relations be used for reducing the size of the input BA, they can also be used for under-approximating inclusion of languages of states. For instance, during a BA inclusion test $\mathcal{L}(\mathcal{A}_{S})\stackrel{{\scriptstyle?}}{{\subseteq}}\mathcal{L}(\mathcal{A}_{B})$, if every initial state of $\mathcal{A}_{S}$ is simulated by an initial state of $\mathcal{A}_{B}$, the inclusion holds and no complementation needs to be performed. But simulations can also be used to reduce the explored state space within, e.g., the inclusion check itself, for instance in the context of Ramsey-based algorithms [1, 2]. Ramsey-based complementation algorithms [34] in the worst case produce $2^{\mathcal{O}(n^{2})}$ states, which is a significant gap from the lower bound of Michel [28] and Yan [41]. The Ramsey-based construction was, however, later improved by Breuers et al. [5] to match the upper bound $2^{\mathcal{O}(n\log n)}$. The way simulations are applied in the Ramsey-based approach is fundamentally different from the current work, which is based on rank-based construction. Taking universality checking as an example, the algorithm checks if the language of the complement automaton is empty. They run the complementation algorithm and the emptiness check together, on the fly, and during the construction check if a macrostate with a larger language has been produced before; if yes, then they can stop the search from the language-smaller macrostate. Note that, in contrast to our approach, their algorithm does not produce the complement automaton.

9 Conclusion and Future Work

We developed two novel optimizations of the rank-based complementation algorithm for Büchi automata that are based on leveraging direct and delayed simulation relations to reduce the number of states of the complemented automaton. The optimizations are directly usable in rank-based BA inclusion and universality checking. We conjecture that the decision problem of checking BA language inclusion might also bring another opportunities for exploiting simulation, such as in a similar manner as in [3]. Another, orthogonal, directions of future work are (i) applying simulation in other than the rank-based approach (in addition to the particular use within [1, 2]), e.g., complementation based on Safra’s construction [32], which, according to our experience, often produces smaller complements than the rank-based procedure, (ii) applying our ideas within determinization constructions for BAs, and (iii) generalizing our techniques for richer simulations, such as the multi-pebble simulation [13] or various look-ahead simulations [26, 27]. Since the richer simulations are usually harder to compute, it would be interesting to find the sweet spot between the overhead of simulation computation and the achieved state space reduction.

Acknowledgement

We thank the anonymous reviewers for their helpful comments on how to improve the exposition in this paper. This work was supported by the Ministry of Science and Technology of Taiwan project 106-2221-E-001-009-MY3 the Czech Science Foundation project 19-24397S, the FIT BUT internal project FIT-S-17-4014, and The Ministry of Education, Youth and Sports from the National Programme of Sustainability (NPU II) project IT4Innovations excellence in science—LQ1602.