Das Kapitel untersucht die Ergänzung von transitionsbasierten Emerson-Lei-Automaten (TELAs), einem entscheidenden Vorgang bei der formalen Verifikation mit Anwendungen bei der Modellüberprüfung und Sprachintegrationstests. Es beginnt mit der Diskussion des theoretischen Hintergrunds und der Bedeutung der Ergänzung von Automaten mit komplexen Akzeptanzbedingungen wie verallgemeinerten Büchi, Rabin, Streett und Paritätsautomaten. Der Text führt einen rangbasierten Ergänzungsalgorithmus für -TELAs ein, das sind TELAs ohne bestimmte atomare Bedingungen, die eine Zustandskomplexität von n ^ k erreichen, wobei n die Anzahl der Zustände und k die Anzahl der minimalen Modelle der Akzeptanzbedingung ist. Dieser Algorithmus wird dann instanziiert, um einen Komplementationsalgorithmus für generalisierte Büchi-Automaten zu erhalten, der einen Büchi-Automaten mit verbesserter Zustandskomplexität konstruiert. Das Kapitel stellt auch ein modulares Verfahren zur Ergänzung von TELAs mit komplexeren Akzeptanzbedingungen vor, das für Rabin-Paare und verallgemeinerte Rabin-Paare eingeführt wird, was zu besseren oberen Grenzen für die Ergänzung von Rabin und verallgemeinerten Rabin-Automaten führt. Darüber hinaus wird in diesem Kapitel die Beziehung zwischen unterschiedlichen Akzeptanzbedingungen diskutiert und ein umfassender Überblick über die damit verbundenen Arbeiten in diesem Bereich gegeben. Die detaillierte Analyse und die verbesserten Algorithmen machen dieses Kapitel zu einer wertvollen Ressource für Forscher und Praktiker in der formalen Verifikations- und Automatentheorie.
KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
Abstract
We give new constructions for complementing subclasses of Emerson-Lei automata using modifications of rank-based Büchi automata complementation. In particular, we propose a specialized rank-based construction for a Boolean combination of Inf acceptance conditions, which heavily relies on a novel way of a run DAG labelling enhancing the ranking functions with models of the acceptance condition. Moreover, we propose a technique for complementing generalized Rabin automata, which are structurally as concise as general Emerson-Lei automata (but can have a larger acceptance condition). The construction is modular in the sense that it extends a given complementation algorithm for a condition \(\varphi \) in a way that the resulting procedure handles conditions of the form \(\text {Fin}\wedge \varphi \). The proposed constructions give upper bounds that are exponentially better than the state of the art for some of the classes.
1 Introduction
Complementation of \(\omega \)-automata is an important operation in formal verification with various applications, for example in model checking wrt expressive temporal logics such as QPTL [25] or HyperLTL [10]; testing language inclusion of \(\omega \)-automata, or in decision procedures of various logics [6, 21]. For Büchi automata (BAs)—i.e., \(\omega \)-automata with the simplest acceptance condition—complementation has been, from the theoretical point of view, thoroughly explored, starting with constructions having the \(2^{2^{\mathcal {O}(n)}}\) state complexity [6] coming down to constructions asymptotically matching the lower bound \(\Omega ((0.76n)^n)\) (modulo a polynomial factor) [1, 38]. Over the years, \(\omega \)-automata with more complex acceptance conditions (such as generalized Büchi (GBAs), (generalized) Rabin/Streett, parity) have found uses in practice. The most general acceptance condition used is the so-called Emerson-Lei condition [11], which is an arbitrary Boolean formula consisting of \(\textsf{Fin}\) and \(\textsf{Inf}\) atoms.
denotes that all transitions labeled with
must occur only finitely often in an accepting run and
denotes that there must be a transition labeled with
occurring infinitely often. There are two main reasons for using more complex acceptance conditions: (i) more compact representation of automata and (ii) the ability to determinize (deterministic BAs are strictly less expressive than BAs).
From the theoretical point of view, precise bounds on complementation of automata with more complex acceptance condition is much less researched, demonstrated by the best upper bound for (transition-based) Emerson-Lei automata (TELAs) being \(2^{2^{\mathcal {O}(n)}}\) [37] states. Here, the \(\mathcal {O}\) in the exponent can hide a linear (or constant) factor, which would have a doubly-exponential effect, giving little information about the actual complexity. In this paper, we present complementation algorithms for several subclasses of TELAs and thoroughly study their complexity, giving better upper bounds than the currently-best known algorithms.
Anzeige
Our contributions can be summarized as follows:
1.
We propose a rank-based complementation algorithm for \(\text {Inf}\)-TELAs, i.e., TELAs where the acceptance condition does not contain any \(\text {Fin}\) atom, with the state complexity \(\mathcal {O}(n (0.76nk)^n)\) where n is the number of states and k is the number of minimal models of the acceptance condition.
2.
By instantiating the previously mentioned algorithm, we obtain a complementation algorithm for generalized Büchi automata with k colours constructing a BA with the state complexity \(\mathcal {O}(n(0.76nk)^n)\), which is, to the best of our knowledge, better than the best previously known algorithms.
3.
We propose a modular procedure for complementing TELAs with the acceptance condition
given a compatible complementation procedure for formula \(\varphi \).
4.
Next, we instantiate the modular procedure to handle Rabin pairs (
) and, in turn, obtain an algorithm for complementing Rabin automata with k Rabin pairs with the complexity \(\mathcal {O}(n^k(0.76n)^{nk})\), which is, again, better than any other algorithm that we know of.
5.
Finally, we instantiate the procedure also for generalized Rabin pairs (
) and obtain complementation constructions for generalized Rabin automata and TELAs with the upper bound \(\mathcal {O}(n^{2^k}(0.76 nk)^{n2^k})\), which is the best upper bound for complementation of general TELAs that we are aware of.
An extended version of the paper with missing proofs can be found at [20].
2 Preliminaries
We fix a finite non-empty alphabet \(\Sigma \) and the first infinite ordinal \(\omega \). For \(k \in \omega \), we use \(\lfloor \!\!\lfloor k \rfloor \!\!\rfloor \) to represent the largest even number less than or equal to k, e.g., \(\lfloor \!\!\lfloor 43 \rfloor \!\!\rfloor = \lfloor \!\!\lfloor 42 \rfloor \!\!\rfloor = 42\). An (infinite) word \(w\) is a function \(w:\omega \rightarrow \Sigma \) where the i-th symbol is denoted as \(w_{i}\). Sometimes, we represent \(w\) as an infinite sequence \(w= w_{~}\hbox {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 \). We use \(\cdot \) for ellipsis, e.g., if interested only in the second component of a triple, we may write the triple as \((\cdot , x, \cdot )\).
2.1 Emerson-Lei Acceptance Conditions
Given a set \(\Gamma = \{0, \ldots , k -1\}\) of kcolours (often depicted as
, etc.), we define the set of Emerson-Lei acceptance conditions\(\mathbb{E}\mathbb{L}(\Gamma )\) as the set of formulae constructed according to the following grammar:
for \(c \in \Gamma \). The satisfaction relation \(\models \) for a set of colours \(M \subseteq \Gamma \) and a condition \(\alpha \) is defined inductively as follows (for \(c \in \Gamma \)):
If \(M \models \alpha \), we say that M is a model of \(\alpha \) We denote by \(|\alpha |\) the number of atomic conditions contained in \(\alpha \), where multiple occurrences of the same atomic condition are counted multiple times.
Anzeige
2.2 Emerson-Lei Automata
Fig. 1.
\(\mathcal {A}_{ ex }\)
A (nondeterministic) transition-based1Emerson-Lei automaton (TELA) over \(\Sigma \) is a tuple \(\mathcal {A}= (\mathcal {Q}, \delta , I, \Gamma , \textsf{p}, \textsf{Acc})\), where \(\mathcal {Q}\) is a finite set of states (we often use n to denote \(|\mathcal {Q}|\)), \(\delta \subseteq \mathcal {Q}\times \Sigma \times \mathcal {Q}\) is a set of transitions2, \(I\subseteq \mathcal {Q}\) is the set of initial states, \(\Gamma \) is the set of colours, \(\textsf{p}:\delta \rightarrow 2^{\Gamma }\) is a colouring of transitions, and \(\textsf{Acc}\in \mathbb{E}\mathbb{L}(\Gamma )\). We use \(p \overset{a}{\rightarrow } q\) to denote that \((p,a,q) \in \delta \) and sometimes treat \(\delta \) as a function \(\delta :\mathcal {Q}\times \Sigma \rightarrow 2^{\mathcal {Q}}\). Moreover, we extend \(\delta \) to sets of states \(P \subseteq \mathcal {Q}\) as \(\delta (P, a) = \bigcup _{p \in P} \delta (p,a)\). See Fig. 1 for an example TELA \(\mathcal {A}_{ ex }\) over \(\Sigma = \{a,b,c\}\) with 3 colours
and the acceptance condition
. We define \(|\mathcal {A}| = |\mathcal {Q}|\).
A run of \(\mathcal {A}\) from \(q \in \mathcal {Q}\) on an input word \(w\) is an infinite sequence \(\rho :\omega \rightarrow \mathcal {Q}\) that starts in q and respects \(\delta \), i.e., \(\rho (0) = q\) and \(\forall i \ge 0:\rho (i) \overset{w_{i}}{\rightarrow }\rho (i+1) \in \delta \). Let \( inf (\rho )\subseteq \delta \) denote the set of transitions occurring in \(\rho \) infinitely often and \( inf _{\Gamma }(\rho )= \bigcup \{\textsf{p}(x) \mid x \in inf (\rho )\}\) be the set of infinitely often occurring colours. A run \(\rho \) is accepting wrt an acceptance condition \(\alpha \), written as \(\rho \models \alpha \), iff \( inf _{\Gamma }(\rho )\models \alpha \) and \(\rho \) is accepting in \(\mathcal {A}\) iff \(\rho \models \textsf{Acc}\). 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\). Classical acceptance conditions can be in this more general framework described as follows (we only provide those used later in the paper and include their abbreviations):
where \(B_j, G_j, G_{j,\ell } \in \Gamma \) for all \(j, \ell \). Further, we use \(\text {Inf}\)-TELA to denote a TELA where the acceptance condition contains no \(\text {Fin}\) atoms. We also use the syntactic sugar \(\mathcal {A}= (\mathcal {Q}, \delta , I, F)\) to denote a (transition-based) BA that would be defined using the TELA definition above as
.
2.3 Run DAGs
In this section, we recall the terminology from [19] (which is a minor modification of the terminology from [26] and [38]) used heavily in the paper. Let \(\mathcal {A}= (\mathcal {Q}, \delta , I, \Gamma , \textsf{p}, \textsf{Acc})\) be a TELA. We fix the definition of the run DAG of \(\mathcal {A}\) over a word \(w\) to be a DAG (directed acyclic graph) \(\mathcal {G}_{w}= (V,E)\) of vertices V and edges E where
\(V \subseteq \mathcal {Q}\times \omega \) s.t. \((q, i) \in V\) iff there is a run \(\rho \) of \(\mathcal {A}\) from \(I\) over \(w\) with \(\rho _i = q\),
A labelled run DAG of \(\mathcal {A}_{ ex }\) over the word \(caa(cab)^\omega \notin \mathcal {L}(\mathcal {A}_{ ex })\)
See Fig. 2 for an example of a run DAG of \(\mathcal {A}_{ ex }\) from Fig. 1 over the word \(caa(cab)^\omega \notin \mathcal {L}(\mathcal {A}_{ ex })\) (we will return to the additional labels in the figure later). Given a DAG \(\mathcal {G}= (V,E)\), we often identify \(\mathcal {G}\) with V, for instance, we will write \((p, i) \in \mathcal {G}\) to denote that \((p, i) \in V\). For a vertex \(v \in \mathcal {G}\), we denote the set of vertices of \(\mathcal {G}\) reachable from v (including v itself) as \( reach _{\mathcal {G}}(v)\) or just \( reach (v)\) if \(\mathcal {G}\) is clear from the context. A vertex \(v \in \mathcal {G}\) is finite iff \( reach (v)\) is finite and infinite if it is not finite. In Fig. 2, the vertices \((s,2), (s,3), (s,5), \ldots \) are finite and all other vertices are infinite. Moreover, for a colour
, an edge \(((q, i), (q', i+1)) \in E\) is a
-edge if
and a vertex \(v \in V\) is
-endangered iff it cannot reach any
-edge. For a set of colours \(C \subseteq \Gamma \), v is C-endangered iff it is
-endangered for every
. For example, in Fig. 2, the vertices (q, 1) and (t, 2) are
-endangered but they are not
-endangered. A pair of vertices \(v_1, v_2 \in V\) is converging iff \( reach (v_1) \cap reach (v_2) \ne \emptyset \) (\(v_1\) and \(v_2\)converge). A function \(r:V \rightarrow \omega \) is a run DAG ranking if for every \(v \in V\) it holds that \(\forall u \in reach (v) :r(u) \le r(v)\). We use \(\max (r)\) to denote the rank of r, i.e., the maximum value from \(\{r(u) \mid u \in V\}\) if it exists and \(\infty \) otherwise. A ranking r of \(\mathcal {G}\) is called tight iff there exists a level i such that (i) \(m = \max \{r((q,i)) \mid q \in \mathcal {Q}\}\) is odd and (ii) for all levels \(j \ge i\) it holds that \(\{1,3,\dots ,m\} \subseteq \{ r((q,j)) \mid q\in \mathcal {Q}\}\).
3 Complementation of \(\text {Inf}\)-TELAs
In this section, we describe a complement construction for \(\text {Inf}\)-TELAs. Our approach is an extension of rank-based BA complementation algorithms [9, 14, 16, 19, 24, 26, 38], which construct a BA whose runs simulate a run DAG ranking procedure. We start with giving the run DAG ranking procedure (which extends the ranking procedure from [26] with the introduction of models) and then proceed to the complementation algorithm itself. One can see our algorithm also as an improvement of the algorithm for complementing GBAs in [28] by (i) introducing model assignments, (ii) getting better complexity through the use of tight rankings, and (iii) generalizing the construction from GBAs to arbitrary \(\text {Inf}\)-TELAs.
3.1 \(\text {Inf}\)-TELA Run DAG Labelling
Let \(\mathcal {A}= (\mathcal {Q}, \delta , I, \Gamma , \textsf{p}, \textsf{Acc})\) be an \(\text {Inf}\)-TELA. We use \(\overline{\textsf{Acc}}\) to denote the propositional formula obtained from \(\textsf{Acc}\) by replacing conjunctions by disjunctions and vice versa, and substituting atoms of the form
by
(this can be viewed as negating \(\textsf{Acc}\), transforming it into the negation normal form, substituting
by
, and denoting each
just by
). Let \(\mathcal {M}_{\overline{\textsf{Acc}}}\) be the set of models of \(\overline{\textsf{Acc}}\) where the colours
are interpreted as propositional variables. For example, if
, then
and
(\(\mathcal {M}_{\overline{\textsf{Acc}}}\) can be interpreted as saying which combinations of \(\text {Inf}\)-conditions need to be broken in order to break \(\textsf{Acc}\); in the example above, we can, e.g., break
, we can break both
and
, etc.). Furthermore, we use \(\mathcal {M}^{\min }_{\overline{\textsf{Acc}}}\) to denote the set of minimal models of \(\overline{\textsf{Acc}}\), i.e., \(\mathcal {M}^{\min }_{\overline{\textsf{Acc}}}\) is the set where (i) for every model \(m \in \mathcal {M}_{\overline{\textsf{Acc}}}\), there exists a model \(m' \in \mathcal {M}^{\min }_{\overline{\textsf{Acc}}}\) such that \(m' \subseteq m\), and (ii) there are no \(m, m' \in \mathcal {M}^{\min }_{\overline{\textsf{Acc}}}\) such that \(m \subset m'\). We note that \(\mathcal {M}_{\overline{\textsf{Acc}}}\) can be obtained as the upward closure of \(\mathcal {M}^{\min }_{\overline{\textsf{Acc}}}\) (and \(\mathcal {M}^{\min }_{\overline{\textsf{Acc}}}\) is an antichain). For the example acceptance condition above,
. Moreover, we use \({\textbf {lex-min}}(\overline{\textsf{Acc}})\) to denote the lexicographically smallest model from \(\mathcal {M}^{\min }_{\overline{\textsf{Acc}}}\) (w.l.o.g., we assume \(\mathcal {M}_{\overline{\textsf{Acc}}}\ne \emptyset \)). \({\textbf {lex-min}}(\overline{\textsf{Acc}})\) is used to pinpoint one model when any model can be used.
Let \(\mathcal {G}= (V,E)\) be a run DAG of \(\mathcal {A}\) over \(w\). For a set of vertices \(U\subseteq V\), a mapping \(\eta :U\rightarrow \mathcal {M}^{\min }_{\overline{\textsf{Acc}}}\) is called endangered in\(\mathcal {G}\) if
1.
U is finite and nonempty,
2.
each \(v\in U\) is \(\eta (v)\)-endangered in \(\mathcal {G}\), and
3.
for each pair of vertices \(v_1, v_2\in U\) converging in \(\mathcal {G}\), we have \(\eta (v_1) = \eta (v_2)\).
A function m with the signature \(m:V \rightarrow \mathcal {M}^{\min }_{\overline{\textsf{Acc}}}\) is called a model assignment. For instance, for \(\mathcal {A}_{ ex }\) in Fig. 1, we have
since \(\mathcal {A}_{ ex }\) is a GBA. In addition, for the run DAG in Fig. 2 and a set \(\{(q,1),(t,2)\}\), the mapping
is endangered in \(\mathcal {G}\). On the other hand, there exists no endangered mapping for the set \(\{(s,2)\}\) in \(\mathcal {G}\), as (s, 2) can reach both a
-edge as well as a
-edge.
Algorithm 1
\(\text {Inf}\)-TELA run DAG labelling
In Algorithm 1, we give a (nondeterministic) ranking procedure that assigns ranks and minimal models of \(\overline{\textsf{Acc}}\) to each vertex of \(\mathcal {G}\). Intuitively, the algorithm starts by giving all initially finite vertices the rank 0 and assigning their model to \({\textbf {lex-min}}(\overline{\textsf{Acc}})\) (Line 4). Then, it proceeds in iterations, each starting with the DAG \(\mathcal {G}^i\) and consisting of two steps:
1.
First, the algorithm tries to find a model assignment \(\eta :U \rightarrow \mathcal {M}^{\min }_{\overline{\textsf{Acc}}}\) for a finite nonempty set of vertices U of \(\mathcal {G}^i\) s.t. for all \(u \in U\), if
, then every path in \(\mathcal {G}^i\) starting in u satisfies the condition
(the path breaks all the
conditions, i.e., \(\eta \) is endangered). If such a model assignment exists (the choice is nondeterministic), the algorithm assigns rank \(i+1\) to all vertices reachable from U and removes them from the DAG, creating DAG \(\mathcal {G}^{i+1}\) (Lines 7–9).
2.
Second, the algorithm assigns rank \(i+2\) to all vertices in \(\mathcal {G}^{i+1}\) that became finite (after the previous step) and removes them from the DAG, creating DAG \(\mathcal {G}^{i+2}\) (Lines 10–12). The counter i is incremented by two and the next iteration continues.
The iterations end when \(\mathcal {G}^i\) is empty or when no suitable model assignment \(\eta \) is found (which happens when w is accepted by \(\mathcal {A}\)). Note that due to the nondeterminism within the algorithm, it may be possible to obtain, in two different runs of the algorithm on the same run DAG, two different pairs \((r_1, m_1)\) and \((r_2, m_2)\) with \(\max (r_1) \ne \max (r_2)\).
Example 1
See Fig. 2 for a possible labelling of the run DAG of \(\mathcal {A}_{ ex }\) over the word \(caa(cab)^\omega \). The ranking procedure proceeds in the following steps:
1.
\((i=0)\) First, all finite vertices, which are in this example vertices of the form (s, 3), (s, 5), ..., \((s, 3j+2)\) for all \(1 \le j\), are assigned rank 0 and model \({\textbf {lex-min}}(\overline{\textsf{Acc}})\), and \(\mathcal {G}^0\) is set to be \(\mathcal {G}^w\) without those vertices. (Lines 2–4)
2.
Second, we set \(\eta _1\) to the mapping
. The mapping \(\eta _1\) is endangered in \(\mathcal {G}^0\) because the following conditions hold:
(a)
\(\eta _1\) is finite and nonempty,
(b)
neither (q, 1) nor (t, 2) can reach a
transition, and
(c)
(q, 1) and (t, 2) converge (in (q, 3)) and they are both assigned the same model (
).
In particular, \(\eta _1\) is the endangered mapping that gives the largest number of vertices of \(\mathcal {G}^0\) rank 1. (Line 6)
3.
Third, we assign every vertex in \(\mathcal {G}^0\) reachable from (q, 1) or (t, 2) the rank 1 and model
. (Line 7)
4.
Fourth, we obtain \(\mathcal {G}^1\) from \(\mathcal {G}^0\) by removing vertices with rank 1. (Line 9)
5.
\(\mathcal {G}^1\) contains three vertices (\(\{(q,0), (r,1), (s,2)\}\)), which all get rank 2 (Line 10) and are removed in \(\mathcal {G}^2\) (Line 12). The ranking procedure finishes. \(\square \)
Lemma 2
If Algorithm 1 returns \(\bot \), then \(w\in \mathcal {L}(\mathcal {A})\).
Proof
Let \(\textsf{Acc}'\) be a formula in the disjunctive normal form (DNF) equivalent to \(\textsf{Acc}\), i.e., \(\textsf{Acc}' = \bigvee _{j=1}^\ell \varphi _j\) where \(\varphi _j = \text {Inf}(c^j_1) \wedge \dots \wedge \text {Inf}(c^j_{k_j})\) for some \(\ell \) and \(k_1, \ldots , k_\ell \). Note that \(\mathcal {M}^{\min }_{\overline{\textsf{Acc}}}= \mathcal {M}^{\min }_{\overline{\textsf{Acc}'}}\) contains sets of colours \(M \subseteq \Gamma \), each of them with at least one colour from \(\varphi _1\), at least one colour from \(\varphi _2\), etc. In order for Algorithm 1 to return \(\bot \), it needs to hold that there is some \(i \ge 0\) such that \(\mathcal {G}^i\) is nonempty and there does not exist any mapping \(\eta :U \rightarrow \mathcal {M}^{\min }_{\overline{\textsf{Acc}}}\), with \(U \subseteq V^i\), that would be endangered in \(\mathcal {G}^i\). In particular, such a (nonempty) mapping \(\eta \) does not exist iff no vertex \(v \in \mathcal {G}^i\) satisfies point (2) of the definition of an endangered mapping (i.e., when we can find an accepting path from all vertices remaining in \(\mathcal {G}^i\)). Therefore, it follows that no vertex \(v \in \mathcal {G}^i\) is M-endangered for any \(M \in \mathcal {M}^{\min }_{\overline{\textsf{Acc}}}\), i.e., in other words,
We will now construct an accepting path \(\pi \) in \(\mathcal {G}_{w}\). Note that not all paths in \(\mathcal {G}^i\) are necessarily accepting (consider the TELA over a unary alphabet and the run DAG in the right, with the acceptance condition
; there are many non-accepting paths from (q, 0)—e.g., a path that alternates between a q-vertex and an r-vertex and never touches any s-vertex). While constructing \(\pi \), for every clause \(\varphi _j\) we will be tracking the information about which atom of \(\varphi _j\) we should see next in order to satisfy \(\varphi _j\) on the path. In particular, we will start from a vertex \(v_0\) that is a root vertex of \(\mathcal {G}^i\) and we will use the tuple \(t_0 = (c^1_1, \ldots , c^\ell _1)\) to keep track of the colours. Using (Reach), it follows that there is a clause \(\varphi _j\) s.t. \(v_0\) can reach a \(c^j_1\)-edge \(e_1\). We will set \(t_1 = (c^1_1, \ldots , c^j_2, \ldots , c^\ell _1)\) and continue in a similar way: from every vertex we encounter, we use (Reach) to obtain an edge that is a c-edge for some c in \(t_i\). In the case we need to increment some component of \(t_i\) from \(c^j_{k_j}\), we set the new value to \(c^j_1\). The path \(\pi \) is then constructed as an infinite path that goes through the infinite sequence \(v_0, e_1, e_2, \ldots \) Note that because the sequence \(v_0, e_1, e_2 \ldots \) is infinite, due to the pigeonhole principle there will be a clause \(\varphi _j\) s.t. the sequence \(t_0, t_1, \ldots \) infinitely often increments the j-th component and so \(\pi \) is accepting. From \(\pi \), we can now extract the accepting run of \(\mathcal {A}\) on w. \(\square \)
Lemma 3
Algorithm 1 always terminates with \(i \le 2n\).
Proof
Consider a run DAG \(\mathcal {G}_{w}\) for a word w. First observe that at the end of the main loop of Algorithm 1 (Line 13), \(\mathcal {G}^i\) has no finite vertices (all of them were removed). Due to Line 2, \(\mathcal {G}^i\) at the beginning of the main loop (Line 6) also has no finite vertices. Let \(\mathcal {G}_m^i\) be the DAG \((V^i_m, E^i \cap (V^i_m\times V^i_m))\) where \(V^i_m = \{ (q,j) \in V^i \mid j \ge m \}\), i.e., the projection of \(\mathcal {G}^i\) from level m down, and \( width (\mathcal {G}_m^i)\) be the maximum number of vertices on any level of the run DAG below level m, formally, \( width (\mathcal {G}_m^i) = \max \{|\{(q,j) : (q,j) \in V^i_m\}| : j \ge m\}\). From the definition of endangered mapping and the loop on Line 7, we have that if the condition on Line 6 holds, there is some \(m\in \omega \) s.t. \( width (\mathcal {G}_m^{i+1}) < width (\mathcal {G}_m^{i})\). This holds because if the mapping \(\eta \) is non-empty, then there is at least one infinite path in \(\mathcal {G}^i\) that is completely removed in the next step, i.e., from some level m, the width of all levels below get decreased by at least one. If the condition on Line 6 does not hold, the algorithm terminates and we are done. From the previous claim we have that in each successful iteration of the main loop, the width of \(\mathcal {G}^{i+2}\) in the limit is at most the one of \(\mathcal {G}^{i}\) minus one. Since the maximum width of \(\mathcal {G}_{w}\) is n, then, if \(w \notin \mathcal {L}(\mathcal {A})\), at latest \(\mathcal {G}_m^{2n-1}\) is empty for some \(m \in \omega \), and hence \(\mathcal {G}^{2n}\) is empty and the algorithm terminates. \(\square \)
Lemma 4
If \(w\in \mathcal {L}(\mathcal {A})\), then Algorithm 1 terminates with \(\bot \).
Proof
Consider some \(w\in \mathcal {L}(\mathcal {A})\). Then, there is an accepting run \(\rho \) on \(w\) in \(\mathcal {A}\). We have \((\rho _j, j) \in \mathcal {G}_{w}\) for all \(j\in \omega \); we show that \((\rho _j, j)\) is not M-endangered for every \(M \in \mathcal {M}^{\min }_{\overline{\textsf{Acc}}}\). The fact that no \(\rho _j\) is finite follows from the fact that \(\rho \) is infinite. Observe that for each \(M \in \mathcal {M}^{\min }_{\overline{\textsf{Acc}}}\), there is some
s.t.
(otherwise, \(w\) would not be accepted by \(\mathcal {A}\)). Therefore, \((\rho _j, j)\) is not M-endangered. Hence, in every iteration of Algorithm 1, all vertices \((\rho _j, j)\) stay in \(\mathcal {G}^i\). From Lemma 3 we have that Algorithm 1 always terminates, but \(\mathcal {G}^i \ne \emptyset \) for each i. Therefore, the algorithm terminates with \(\bot \). \(\square \)
Corollary 5
\(w\notin \mathcal {L}(\mathcal {A})\) iff Algorithm 1 on \(\mathcal {G}_{w}\) terminates with (r, m).
The following lemma about the ranking procedure will be useful later.
Lemma 6
If Algorithm 1 terminates with (r, m), then \(\max (r) \le 2n\) and, moreover, either \(\max (r) = 0\) or r is tight.
Proof
The first part (\(\max (r) \le 2n\)) follows directly from Lemma 3. For the second part, there are two options: either \(\mathcal {G}_{w}\) is finite (i.e., there is no infinite run of \(\mathcal {A}\) on \(w\)), in which case Algorithm 1 assigns all vertices in \(\mathcal {G}_{w}\) rank 0 and does not even enter the loop at Line 5. In the other case (\(\mathcal {G}\) is infinite), let \(k = \max (r)\) if \(\max (r)\) is odd and \(k = \max (r) - 1\) otherwise (from the previous case, we know that \(k\ge 1\)). We know that for every \(\ell \in \{1, 3, \ldots , k\}\), there is a vertex \(v_\ell = (q_\ell , i_\ell ) \in \mathcal {G}_{w}\) with \(r(v_\ell ) = \ell \) (this is because the mapping at Line 6 in the algorithm needs to be non-empty) and that such a vertex is the beginning of an infinite path of vertices with rank \(\ell \). Therefore, there needs to be a level i containing vertices with all ranks \(\{1, 3, \ldots , k\}\). From the previous, all levels \(j > i\) will also have all of the odd ranks up to k. Choosing i large enough will prevent level i having a vertex with an even rank higher than k. Therefore, r is tight. \(\square \)
3.2 \(\text {Inf}\)-TELA Complement Construction
Let \(\mathcal {A}= (\mathcal {Q}, \delta , I, \Gamma , \textsf{p}, \textsf{Acc})\) be an \(\text {Inf}\)-TELA and \(n = |\mathcal {Q}|\). We define a (level) ranking to be a function \(f:\mathcal {Q}\rightarrow \{0, \ldots , 2n\}\). The rank of f is defined as \(f = \max \{f(q) \mid q \in \mathcal {Q}\}\). We call a mapping \(\mu :Q\rightarrow \mathcal {M}^{\min }_{\overline{\textsf{Acc}}}\) a level model. We say that \(\mu \) is consistent wrt f if \(\mu (q) = {\textbf {lex-min}}(\overline{\textsf{Acc}})\) whenever f(q) is even. We denote the set of all level models by \(\textsf{LM}\). For a set of states \(S \subseteq \mathcal {Q}\) and a level model \(\mu \), f is \((S, \mu )\text {-} tight \) if
A ranking is \(\mu \text {-} tight \) if it is \((\mathcal {Q},\mu )\)-tight; we use \(\mathcal {T}\) to denote the set of all \(\mu \)-tight rankings for some level model \(\mu \).
For two level rankings \(f, f'\) and two level models \(\mu , \mu '\), we say that \((f', \mu ')\) is a consistent successor of \((f,\mu )\) over \(a \in \Sigma \), denoted as
, iff
(i)
\(\mu \) and \(\mu '\) are consistent wrt f and \(f'\), respectively, and
(ii)
for all \(q \in \mathcal {Q}\) and \(q'\in \delta (q,a)\) the following holds:
Intuitively, the rankings guess the ranks of states in the run DAG and the level models guess the models assigned to states in the labelling procedure from Section 3.1. Consistent successors respect the labelling procedure. On every path in a run DAG, the ranks are nonincreasing. If some odd-ranked vertex v has an outgoing
-edge to \(v'\) and
is in the model assigned to v, the vertex \(v'\) has to have a lower rank than v, because when v is removed from \(\mathcal {G}_{w}^i\), there is no reachable
-edge in \(\mathcal {G}_{w}^i\). Moreover, if the model is changed between v and \(v'\) and the rank is odd, then the rank also has to be decreased.
The complement of \(\mathcal {A}\) is given as the BA \(\textsc {CInfTela} (\mathcal {A}) = (\mathcal {Q}', \delta ', I', F')\) whose components are defined as follows:
\(\mathcal {Q}' = \mathcal {Q}_1 \cup \mathcal {Q}_2\) where
\(\mathcal {Q}_1 = 2^\mathcal {Q}\) and
\(\mathcal {Q}_2 = \begin{array}{ll} \{(S,O,f,i,\mu ) \in & 2^\mathcal {Q}\times 2^\mathcal {Q}\times \mathcal {T}\times \{0, 2, \ldots , 2n - 2\}\times \textsf{LM}\mid \\ & f \text { is } (S, \mu )\text {-tight}, O \subseteq S \cap f^{-1}(i)\}, \end{array}\)
Intuitively, a run of \(\textsc {CInfTela} (\mathcal {A})\) on a word \(w\) tries to construct the run DAG \(\mathcal {G}_{w}\) of \(\mathcal {A}\) on the same word, with rankings encoded within the states. The restrictions on \(\delta _3\) encode the rules from Algorithm 1. The partitioning of \(\mathcal {Q}'\) into \(\mathcal {Q}_1\) and \(\mathcal {Q}_2\) allows us to consider only tight rankings, as in [14]. Moreover, the i-component of a macrostate allows us to further decrease the number of states in the same way as in [38] (we know that all states in O have the same rank i).
Theorem 7
Let \(\mathcal {A}\) be an \(\text {Inf}\)-TELA. Then, \(\mathcal {L}(\textsc {CInfTela} (\mathcal {A})) = \Sigma ^\omega \setminus \mathcal {L}(\mathcal {A})\).
Proof
(\(\subseteq \)) We use Boolean laws and prove an equivalent statement \(\mathcal {L}(\mathcal {A}) \subseteq \Sigma ^\omega \setminus \mathcal {L}(\textsc {CInfTela} (\mathcal {A}))\). Let \(w\in \mathcal {L}(\mathcal {A})\) be a word and \(\rho \) be an accepting run of \(\mathcal {A}\) on \(w\). First, let \(\rho '\) be the run \(\rho ' = S_0 S_1\ldots \) with \(S_0=I\) and \(S_{i+1}=\delta _1(S_i,w(i))\) for all \(i \in \omega \) (i.e., \(\rho '\) stays in \(\mathcal {Q}_1\)). The run \(\rho '\) cannot be accepting in \(\textsc {CInfTela} (\mathcal {A})\), because \(\rho (i) \in S_i\) and so \(S_i \ne \emptyset \) for any \(i \in \omega \) (in \(\mathcal {Q}_1\), the only accepting transitions are those from state \(\emptyset \) to state \(\emptyset \)). Second, let
be a run of \(\textsc {CInfTela} (\mathcal {A})\) on \(w\) (\(\rho ''\) jumps to \(\mathcal {Q}_2\) at position p). From the construction, it holds that
for all \(j>p\). Since \(\rho \) is accepting in \(\mathcal {A}\), eventually there will be a position \(k > p\) such that \(f_k(\rho (k))\), \(f_{k+1}(\rho (k+1))\), \(f_{k+2}(\rho (k+2))\), ...are all even (because there is no model satisfying \(\rho \) in \(\mathcal {M}^{\min }_{\overline{\textsf{Acc}}}\), so points (iib) and (iic) from the definition of
will enforce this). For the sake of contradiction, assume that \(\rho ''\) is accepting. Then for some position \(\ell > k\), because the i-component of a macrostate rotates over all even ranks, it holds that \(i_\ell = f_\ell (\rho (\ell ))\) and \(\rho (\ell ) \in O_\ell = f_\ell ^{-1}(\rho (\ell ))\). We can easily show by induction that for all \(j \ge \ell \), it holds that \(\rho (j) \in O_j \ne \emptyset \), which is in contradiction with the assumption that \(\rho ''\) is accepting.
(\(\supseteq \)) Consider any word \(w\not \in \mathcal {L}(\mathcal {A})\). From Corollary 5 and Lemma 6 it follows that the run DAG \(\mathcal {G}_{w}\) has a bounded rank. If all vertices of \(\mathcal {G}_{w}\) are finite, then there is an accepting run \(\rho '\) on \(\textsc {CInfTela} (\mathcal {A})\) where \(\rho ' = S_0 S_1 \ldots \) with \(S_0 = I\) and \(S_{i+1} = \delta (S_i, w_i)\) for all \(i \in \omega \). Otherwise, Algorithm 1 terminates with a tight ranking r and a model m. From the definition of
, there is a run
such that \(f_k(q) = r((q,k))\) and \(\mu _k(q) = m((q,k))\) for all \(k > p\). In order to show that \(\rho ''\) is acepting, we need to show that the O-component of the macrostates on the run is empty infinitely often. Assume by contradiction that there is an index \(\ell > p\) such that \(O_j\) is non-empty for all \(j \ge \ell \). Then, there is a vertex \((q,\ell ) \in \mathcal {G}_{w}\) s.t. \(r((q,\ell ))\) is even and there are infinitely many vertices reachable from \((q,\ell )\) with the same even rank, which is a contradiction with the construction of r in Algorithm 1, which would give some of the vertices odd ranks. \(\square \)
For the complexity analysis, we use \( tight (n)\) to denote the number of \(\mu \)-tight level rankings for an automaton with n states (\(\mu \)-tight rankings for \(\text {Inf}\)-TELAs correspond to tight rankings for BAs). It holds that \( tight (n) \approx (0.76n)^n\) [14, 38].
Theorem 8
The number of states of \(\textsc {CInfTela} (\mathcal {A})\) is in \(\mathcal {O}(k^n\cdot tight (n+1)) = \mathcal {O}(n (0.76nk)^n)\) for \(k = |\mathcal {M}^{\min }_{\overline{\textsf{Acc}}}|\).
Proof
The set of macrostates \(\mathcal {Q}_1\) is obtained by a simple subset construction, therefore \(|\mathcal {Q}_1| \in \mathcal {O}(2^n)\). That is much smaller than \(\mathcal {O}(k^n\cdot tight (n+1))\), so it is sufficient to count only the number of macrostates of the form \((S, O, f, i, \mu )\). For this, we uniquely encode each macrostate as a pair (h, i) where \(h :\mathcal {Q}\rightarrow \{ -2, -1, \ldots , 2n-1 \} \times \mathcal {M}^{\min }_{\overline{\textsf{Acc}}}\) is defined as follows:
We compute the number of encodings h for a fixed i. We divide all encodings into four groups according to the set \(\textrm{img}(h)_0 \cap \{ -2, -1 \}\) where \(\textrm{img}(h)_0\) denotes the set of first elements of the pairs in \(\textrm{img}(h)\). We show that we can obtain the bound \(\mathcal {O}(k^n \cdot tight (n))\) for each of the groups. The groups are denoted by \(g_M\) with \(M \subseteq \{-2, -1\}\). For \(h(q) = (m, \mu )\), we use \(h(q)_m\) and \(h(q)_\mu \) to denote m and \(\mu \).
\(g_\emptyset \):
from the definition, f is \(\mu \)-tight. The level model \(\mu \) is of the form \(\mu :\mathcal {Q}\rightarrow \mathcal {M}^{\min }_{\overline{\textsf{Acc}}}\), so there are k possible assignments for every state from \(\mathcal {Q}\). The number of level models is therefore \(k^n\) and \(|g_\emptyset | = \mathcal {O}(k^n \cdot tight (n))\).
\(g_{\{-1\}}\):
since there is at least one state q with \(h(q)_m = -1\), this means that \(q \in O\) so q has an even rank. As a consequence, at least one of the positive odd ranks of h (up to \(2n-1\)) will not be taken, so we can infer that \(h:\mathcal {Q}\rightarrow \{-1, \ldots , 2n-3\} \times \mathcal {M}^{\min }_{\overline{\textsf{Acc}}}\). We can therefore uniquely represent h by a mapping \(h'\) by incrementing all ranks of h by two, so \(h':\mathcal {Q}\rightarrow \{0, \ldots , 2n-1\} \times \mathcal {M}^{\min }_{\overline{\textsf{Acc}}}\). But then \(h' \in \mathcal {T}(n)\) and the number of all level models is \(k^n\), so \(|g_{\{-1\}}| \in \mathcal {O}(k^n \cdot tight (n))\).
\(g_{\{-2,-1\}}\):
similarly as for \(g_{\{-1\}}\) we get that \(|g_{\{-2,-1\}}| \in \mathcal {O}(k^n \cdot tight (n))\).
\(g_{\{-2\}}\):
the reasoning is similar to the one for \(g_{\{-1\}}\), with the exception that now, we know that there is a state \(q \in \mathcal {Q}\setminus S\), which is, according to the definition of a ranking, assigned the rank 0. This means that one positive odd rank of h is, again, not taken, so we increment all non-negative ranks of h by two and map all states in \(\mathcal {Q}\setminus S\) to 1, obtaining a tight ranking \(h' \in \mathcal {T}(n)\). The number of level models is \(k^n\), therefore, \(|g_{\{-2\}}| \in \mathcal {O}(k^n \cdot tight (n))\).
Since the size of all groups is bounded by \(\mathcal {O}(k^n \cdot tight (n))\), for a fixed i, the total number of these encodings is still \(\mathcal {O}(k^n \cdot tight (n))\). When we sum the encodings for all i’s, we obtain that the number is bounded by \(\mathcal {O}(k^n \cdot tight (n+1))\), since \(\mathcal {O}(n \cdot tight (n)) = \mathcal {O}( tight (n+1))\) [38]. The rest follows from the approximation of \( tight (n)\). \(\square \)
Corollary 9
Let \(\mathcal {A}\) be an \(\text {Inf}\)-TELA with n states and k colours \(\Gamma \). The number of states of \(\textsc {CInfTela} (\mathcal {A})\) is in \(\mathcal {O}({k \atopwithdelims ()\lfloor k/2 \rfloor }^{n} \cdot tight (n+1)) = \mathcal {O}(n \cdot ({k \atopwithdelims ()\lfloor k/2 \rfloor } \cdot 0.76n)^n) \subseteq \mathcal {O}(n (2^k \cdot 0.76n)^n)\).
Proof
The proof of the more precise bound follows directly from Theorem 8 and the fact that the size of \(\mathcal {M}^{\min }_{\overline{\textsf{Acc}}}\) is bounded by the size of the largest antichain in \(2^\Gamma \), which is at most \({k \atopwithdelims ()\lfloor k/2 \rfloor }\) by Sperner’s theorem. \(\square \)
Corollary 10
Let \(\mathcal {A}\) be a GBA with n states and k colours. Then the number of states of \(\textsc {CInfTela} (\mathcal {A})\) is in \(\mathcal {O}(k^n \cdot tight (n+1)) = \mathcal {O}(n (0.76nk)^n)\).
Proof
The proof follows directly from Theorem 8. For a GBA it holds that
. The formula is in DNF, hence
and \(|\mathcal {M}^{\min }_{\overline{\textsf{Acc}}}| = k\). The number of all level models is \(k^n\). \(\square \)
We note that to the best of our knowledge, our bound on the complementation of GBAs is better than other bounds in the literature. In particular, it is clearly better than the bound \(\mathcal {O}(k^n(2n + 1)^n)\) from [28], which is the best upper bound for complementing GBAs that we are aware of. It is also better than an approach that would go through determinization by using the procedure in [39], which outputs a deterministic Rabin automaton with the number states bounded by \((1.47nk)^n\) for large k and \(2^n- 1\) accepting pairs, which can be complemented easily into a Streett automaton.
4 Modular Complementation of
TELAs
In this section, we propose a modular algorithm \(\textsf{FinCompl}\) for complementation of TELAs with the acceptance condition
for any \(\varphi \), parameterized by an algorithm for complementing TELAs with the condition \(\varphi \). In Section 5, we will then instantiate the algorithm for some common acceptance conditions, eventually obtaining an efficient complementation algorithm for general TELAs.
Let us fix a TELA
and let \(\Delta \) be \(\delta \) without transitions whose label contains
. For a word \(w\in \Sigma ^\omega \), we define a relaxed run DAG (RRDAG) over \(w\), denoted by \(\mathcal {G}^{\Delta }_{w}\), as any sequence of states \(\mathcal {G}^{\Delta }_{w}= (S_0, S_1, \dots )\) where \(S_i \subseteq \mathcal {Q}\) and \(\Delta (S_{i}, w_{i}) \subseteq S_{i+1}\). Intuitively, an RRDAG over a word may contain more states on each level than it is necessary from the reachability of \(\Delta \). Note that this definition of RRDAGs is equivalent to having vertices of the form (q, i), where \(q \in S_i\) with edges given implicitly by \(\Delta \). We use these definitions interchangeably. Clearly, there may be multiple RRDAGs over a single word, they are all, however, subgraphs of the (standard) run DAG \(\mathcal {G}_{w}\). We say that \(\mathcal {G}^{\Delta }_{w}= (S_0, S_1, \dots )\) is accepting wrt \(\varphi \), written as \(\mathcal {G}^{\Delta }_{w}\models \varphi \), if there is a run \(\rho = q_k q_{k+1} \ldots \) for \(k \ge 0\) in \(\Delta \) such that for every \(i \ge k\) it holds that \(q_i \in S_i\) and \(q_{i+1} \in \Delta (q_i, w_{i})\), and, moreover, \(\rho \models \varphi \) (i.e., the accepting run does not need to start at the beginning of \(\mathcal {G}^{\Delta }_{w}\)). The reason for introducing RRDAGs is that the algorithm for condition \(\varphi \) will construct a BA that runs over RRDAGs constructed using the restricted transition relation \(\Delta \). The relaxation allows us to introduce new vertices (not connected to the root of the RRDAG) at any level that represent runs that have seen finitely many times a
transition in \(\delta \).
Our definition of the modular procedure \(\textsf{FinCompl}\) for
is given wrt a subprocedure for complementing a TELA with condition \(\varphi \). The subprocedure is given as a tuple \(\mathbb {S}_{\Delta }^{\varphi }= (\mathcal {M}, \mathcal {M}_0, \textsf{SuccAct}_{\Delta }, \textsf{SuccTrack}_{\Delta }, \textsf{EmptyBreak})\), where
(i)
\(\mathcal {M}\) is a set of macrostates,
(ii)
\(\mathcal {M}_0 \subseteq \mathcal {M}\) is a set of initial macrostates,
(iii)
\(\textsf{SuccAct}_{\Delta }:2^\mathcal {Q}\times \Sigma \times \mathcal {M}\rightarrow 2^\mathcal {M}\) is an active transition function,
(iv)
\(\textsf{SuccTrack}_{\Delta }:2^\mathcal {Q}\times \Sigma \times \mathcal {M}\rightarrow 2^\mathcal {M}\) is a tracking transition function, and
(v)
\(\textsf{EmptyBreak}\subseteq \mathcal {M}\) is an empty-breakpoint predicate.
We use \(\textsf{Succ}_\Delta \) to denote \(\textsf{SuccAct}_\Delta \cup \textsf{SuccTrack}_\Delta \) (when treated as relations). Intuitively, \(\mathcal {M}\) is a set of macrostates given by the subprocedure for \(\varphi \). \(\textsf{EmptyBreak}\) is a condition that has to hold for a macrostate to be accepting in \(\mathbb {S}_{\Delta }^{\varphi }\). The transitions between macrostates of \(\mathcal {M}\) are described using transition functions \(\textsf{SuccAct}_\Delta \) and \(\textsf{SuccTrack}_\Delta \). In particular, \(\textsf{M}' \in \textsf{Succ}_\Delta (P', a, \textsf{M})\) is computed by taking the successor of the macrostate \(\textsf{M}\) over a, but also while taking into account the set \(P'\) of states (\(\textsf{M}\) corresponds to index i of the run while \(\textsf{M}'\) and \(P'\) correspond to index \(i+1\)) provided by \(\textsf{FinCompl}\), which represent breaking the
condition. The reason for using two transition functions (\(\textsf{SuccAct}_\Delta \) and \(\textsf{SuccTrack}_\Delta \)) is that some subprocedures that we will introduce later will use two types of macrostates: active and tracking. For instance, if \(\mathbb {S}_{\Delta }^{\varphi }\) is a rank-based procedure (cf. Section 5.2), active macrostates will contain breakpoints, which the construction will try to empty, and once a breakpoint is seen, \(\textsf{FinCompl}\) will add some more runs to the rank-based algorithm. The new runs might not be tight at the given point, so we switch into the tracking mode and wait for newly added runs to become tight before switching into the active mode again.
Let \(w\) be a word and \(\mathcal {G}^{\Delta }_{w}= (S_0, S_1, \dots )\) be an RRDAG over \(w\). A Fin-run\(R\) of \(\mathbb {S}_{\Delta }^{\varphi }\) over \(\mathcal {G}^{\Delta }_{w}\) is a sequence \((\textsf{M}_0, \textsf{M}_1, \dots )\) s.t. \(\textsf{M}_0 \in \mathcal {M}_0\) and \(\textsf{M}_{i+1} \in \textsf{Succ}_\Delta (S_{i+1}, w_{i}, \textsf{M}_i)\) for all \(i \ge 0\). \(R\) is accepting if \(\textsf{EmptyBreak}(\textsf{M}_i)\) holds for infinitely many i’s. We say that the subprocedure \(\mathbb {S}_{\Delta }^{\varphi }\) is correct for\(\varphi \) if for each word \(w\) and every RRDAG \(\mathcal {G}^{\Delta }_{w}\) over \(w\) it holds that \(\mathcal {G}^{\Delta }_{w}\) is not accepting wrt \(\varphi \) iff there is an accepting Fin-run \(R\) of \(\mathbb {S}_{\Delta }^{\varphi }\) over \(\mathcal {G}^{\Delta }_{w}\).
Let us now move to the definition of \(\textsf{FinCompl}\). For subprocedure \(\mathbb {S}_{\Delta }^{\varphi }\) and TELA \(\mathcal {A}\) given above, the algorithm will construct the BA \(\textsf{FinCompl}(\mathbb {S}_{\Delta }^{\varphi }, \mathcal {A})= (\mathcal {Q}', I', \delta ', F')\) defined as follows:
Intuitively, the construction executes \(\mathbb {S}_{\Delta }^{\varphi }\) on the restricted transition relation \(\Delta \), while also keeping track of all runs (in S) and runs that either need to terminate or see a
-transition (in P). Whenever \(\mathbb {S}_{\Delta }^{\varphi }\) clears its breakpoint, P is re-sampled (and some new runs can be added to \(\mathbb {S}_{\Delta }^{\varphi }\)).
Since in \((S, P, \textsf{M})\), it always holds that \(P \subseteq S\), each state of \(\mathcal {A}\) can be in one of the three following sets: (i) \(\mathcal {Q}\setminus S\), (ii) \(S \cap P\), and (iii) \(S \setminus P\). \(\square \)
5 Complementation of TELAs and their Subclasses
We proceed by instantiating the modular algorithm \(\textsf{FinCompl}\) from the previous section for several common automata classes—co-Büchi automata, Rabin automata, parity automata, generalized Rabin automata, and, eventually, TELAs.
5.1 Co-Büchi Automata
As a simple demonstration of instantiation of \(\textsf{FinCompl}\), we use it to create a complementation algorithm for co-Büchi automata. The acceptance condition for co-Büchi automata is
, we therefore need to provide a trivial subprocedure \(\mathbb {S}^{ tt }=(\mathcal {M}^{ tt }, \mathcal {M}^{ tt }_0, \textsf{SuccAct}^{ tt }_\Delta , \emptyset , \textsf{EmptyBreak}^{ tt })\) that is correct for \( tt \) (notice that \(\textsf{SuccTrack}^{ tt }_\Delta \) is empty). In the subprocedure, \(\mathcal {M}^{ tt }= 2^\mathcal {Q}\), \(\mathcal {M}^{ tt }_0 = \{ I \}\), and the remaining components are given as follows:
Intuitively, the instantiated procedure works with macrostates (S, P, P) (i.e., to adhere to the formal definition of \(\textsf{FinCompl}\), P is there twice) where S tracks all runs and P is a breakpoint that contains runs that yet need to either terminate or see
. To accept, P needs to be emptied infinitely often. One can observe that \(\textsf{FinCompl}(\mathbb {S}^{ tt }, \mathcal {A})\) resembles the well-known Miyano-Hayashi construction [34] for complementation of co-Büchi automata.
Lemma 13
The subprocedure \(\mathbb {S}^{ tt }\) is correct for the acceptance condition \( tt \).
Corollary 14
For a co-Büchi automaton \(\mathcal {A}\), \(\mathcal {L}(\textsf{FinCompl}(\mathbb {S}^{ tt }, \mathcal {A})) = \Sigma ^\omega \setminus \mathcal {L}(\mathcal {A})\).
Proof
Follows from Lemma 13 and Theorem 11. \(\square \)
Since the result of the construction can be mapped to the Miyano-Hayashi’s algorithm [34], the complexities also match.
In this section, we give an instantiation of \(\textsf{FinCompl}\) with subprocedure \(\mathbb {S}^{\textsf{inf}}= (\mathcal {M}^{\textsf{inf}}\), \(\mathcal {M}^{\textsf{inf}}_0\), \(\textsf{SuccAct}^{\textsf{inf}}_\Delta \), \(\textsf{SuccTrack}^{\textsf{inf}}_\Delta , \textsf{EmptyBreak}^{\textsf{inf}})\) for
, which will allow us to complement TELAs where the acceptance condition is a single Rabin pair. The algorithm is based on the optimal rank-based BA complementation algorithm from [38] adjusted to the needs of the modular construction. The macrostates of the instantiation are given as
where \(\mathcal {M}^{\textsf{inf}}_0 = \{ I \}\). Notice that active macrostates (\(\mathcal {M}^{\textsf{inf}}_{\textsf{Act}}\)) are either sets of states (from \(2^\mathcal {Q}\), just keeping track of all runs) or states of the form (f, O, i) (representing tight runs). On the other hand, tracking macrostates (\(\mathcal {M}^{\textsf{inf}}_{\textsf{Track}}\)) are of the form (f, i); these are used to wait for newly arrived runs to become tight. The remaining components are then defined as follows:
Fig. 3.
Example of \(\textsf{FinCompl}\) instantiated with \(\mathbb {S}^{\textsf{inf}}\) for complementation of automata with the acceptance condition containing a single Rabin pair.
An example of the construction is shown in Fig. 3. The correctness of the instantiation is then summarized by the following lemma.
Lemma 16
The subprocedure \(\mathbb {S}^{\textsf{inf}}\) is correct for the acceptance condition
.
Proof (Sketch)
In order to show that the subprocedure \(\mathbb {S}^{\textsf{inf}}\) is correct, we need to show that for each word w and every RRDAG \(\mathcal {G}_w^\Delta \) it holds that \(\mathcal {G}_w^\Delta \) is not accepting wrt
iff there is an accepting \(\textsf{Fin}\)-run of \(\mathbb {S}^{\textsf{inf}}\) over \(\mathcal {G}_w^\Delta \). We begin with the proof of the statement from left to right. Assume that \(\mathcal {G}_w^\Delta \) is not accepting wrt
. There is either no run of \(\mathcal {G}_w^\Delta \) on \(w\) at all or all runs do not satisfy the formula. If there is no run of \(\mathcal {G}_w^\Delta \) on \(w\), then there is a sequence \((M_0, M_1, \ldots )\) where \(M_0 = I\) and \(M_{j+1} = \Delta (M_j, a)\) for all \(j\ge 0\) such that there is some \(i \ge 0\) such that \(M_l = \emptyset \) for all \(l \ge i\). The predicate \(\textsf{EmptyBreak}(M_l)\) is true for all \(l \ge i\), so it holds infinitely often, and there therefore exists an accepting run of \(\mathbb {S}^{\textsf{inf}}\) over \(\mathcal {G}_w^\Delta \). Now assume that there is a run of \(\mathcal {G}_w^\Delta \) on w. Then, no matter from which point there are no transitions from
, the condition
does not hold for the particular run. With every transition \((f,i) \rightarrow (f',O',i')\) we sample all currently reachable states and then check that all runs from these states contain transitions from
only finitely often by modified Schewe’s rank-based algorithm. The O-component is emptied infinitely often and so there is an accepting run of \(\mathbb {S}^{\textsf{inf}}\) over \(\mathcal {G}_w^\Delta \).
Now we prove the equivalence in the opposite direction. Assume that there is an accepting run of \(\mathbb {S}^{\textsf{inf}}\) over \(\mathcal {G}_w^\Delta \). There is therefore a run where the \(\textsf{EmptyBreak}\) predicate is true infinitely often. The first possible option is that \(\textsf{EmptyBreak}(P)\) is true infinitely many times. That can happen only if there is no run on \(w\) and \(\mathcal {G}_w^\Delta \) is finite. If there is no such run, the formula is not satisfied and \(\mathcal {G}_w^\Delta \) is not accepting. The second option is that \(\textsf{EmptyBreak}((f,O,i))\) is true infinitely many times. That means that the formula
does not hold for any run, no matter when the run stops containing transitions from
. The formula is therefore not satisfied in any run and \(\mathcal {G}_w^\Delta \) is not accepting. \(\square \)
The following lemma shows that using our approach, handling the
condition is “for free,” i.e., the asymptotical complexity stays the same as for the optimal algorithm for BA complementation from [38].
It suffices to count the number of macrostates of the form (S, P, f, O, i). Consider a macrostate (S, P, f, O, i). We uniquely encode the macrostate as (h, i) where \(h:\mathcal {Q}\rightarrow \{-3, \ldots , 2n-1\}\) is defined as follows:
For a fixed i we compute the number of such encodings h. First we divide all encodings into groups according to the set \(\textrm{img}(h) \cap \{ -3, -2, -1 \}\) (8 groups at most) and we will show for each of the groups how we can “shuffle” the ranks in h to obtain the bound \(\mathcal {O}( tight (n))\) for each of the groups. We will denote each of the groups by \(g_M\) with \(M \subseteq \{-3, -2, -1\}\).
\(g_\emptyset \):
from the definition, f is tight so \(|g_\emptyset | = \mathcal {O}( tight (n))\)
\(g_{\{-1\}}\):
since there is at least one state q with \(h(q) = -1\), this means that \(q \in O\) so q has an even rank. As a consequence, at least one of the positive odd ranks of h will not be taken, so we can infer that \(h:\mathcal {Q}\rightarrow \{-1, \ldots , 2n-3\}\). We can therefore uniquely map h to a mapping \(h'\) by incrementing all ranks of h by two, so \(h':\mathcal {Q}\rightarrow \{1, \ldots , 2n-1\}\). But then \(h' \in \mathcal {T}(n)\), so \(|g_{\{-1\}}| \in \mathcal {O}( tight (n))\).
\(g_{\{-2,-1\}}\):
via the same reasoning as for \(g_{\{-1\}}\) we get that \(|g_{\{-2,-1\}}| \in \mathcal {O}( tight (n))\).
\(g_{\{-2\}}\):
the reasoning is similar to the one for \(g_{\{-1\}}\), with the exception that now, we know that there is a state \(q \in \mathcal {Q}\setminus S\), which is, according to the definition of a ranking, assigned the rank 0. This means that one positive odd rank of h is, again, not taken, so we increment all non-negative ranks of h by two and map all states in \(\mathcal {Q}\setminus S\) to 1, obtaining a tight ranking \(h' \in \mathcal {T}(n)\). Therefore, \(|g_{\{-2\}}| \in \mathcal {O}( tight (n))\).
\(g_{\{-3\}}\):
the reasoning is, again, similar to the one for \(g_{\{-1\}}\), with the exception that now, we know that there is a state \(q \in S \setminus P\) such that its rank is, according to the definition 0. Therefore, we increment all non-negative ranks of h by two and map the states in \(S \setminus P\) to 1, obtaining a tight ranking \(h' \in \mathcal {T}(n)\); therefore, \(|g_{\{-3\}}| \in \mathcal {O}( tight (n))\).
\(g_{\{-3,-2\}}\), \(g_{\{-3, -1\}}\):
similarly as for \(g_{\{-2\}}\), we increment all non-negative ranks of h by two and set \(h'(q) = 0\) if \(h(q) = -3\) and \(h'(q) = 1\) if \(h(q) = -2\) (resp. if \(h(q) = -1\)). Then \(h' \in \mathcal {T}(n)\) and so \(|g_{\{-3,-2\}}| = \mathcal {O}( tight (n))\) and \(|g_{\{-3, -1\}}| \in \mathcal {O}( tight (n))\).
\(g_{\{-3, -2, -1\}}\):
in this case, we know that there is at least one state \(q_1 \in O\) and at least one state \(q_2 \in \mathcal {Q}\setminus S\). Therefore, there will be at least two odd positions not taken in h, so we can infer that \(h:\{-3, \ldots , 2n-5\}\). We create \(h'\) by incrementing all ranks in h by four; in this way, we obtain a tight ranking \(h':\mathcal {Q}\rightarrow \{0, \ldots , 2n-1\}\), so \(|g_{\{-3, -2, -1\}}| \in \mathcal {O}( tight (n))\).
Since the size of all groups is bounded by \(\mathcal {O}( tight (n))\), for a fixed i, the total number of these encodings is still \(\mathcal {O}( tight (n))\). When we sum the encodings for all possible i’s, we obtain that the number is bounded by \(\mathcal {O}( tight (n+1))\), since \(\mathcal {O}(n \cdot tight (n)) = \mathcal {O}( tight (n+1))\) [38]. \(\square \)
The modular construction instantiated with \(\mathbb {S}^{\textsf{inf}}\) gives us a procedure for complementing Rabin automata with a single pair. To get a procedure for general Rabin automata, we construct a complement automaton for each Rabin pair, make a product of these automata, and obtain a GBA accepting the complement of the original automaton. The complexity reasoning is straightforward and is summarized by the following corollary.
Corollary 18
Let \(\mathcal {A}\) be a Rabin automaton with k Rabin pairs. Then we can construct a GBA accepting the complement of the language of \(\mathcal {A}\) with \(\mathcal {O}( tight (n+1)^k) = \mathcal {O}(n^k(0.76n)^{nk})\) states and k colours.
To the best of our knowledge, the state complexity of our procedure is better than the complexity of other approaches for complementing Rabin automata (even if we require the output to be a BA and not a GBA—the BA would have \(\mathcal {O}(k\cdot tight (n+1)^k) = \mathcal {O}(k n^k(0.76n)^{nk})\) states). In particular, it is better than the complexity \(\mathcal {O}(k\cdot 3^n \cdot (2n+1)^{nk})\) of [27]. Comparing the two techniques, the main difference is that our modular approach allows us to use tight rankings (and the optimal construction of, e.g., Schewe [38]), which are a significant factor in decreasing the size of the complement (both in theory and in practice). On the other hand, [27] does not use tight rankings (their run DAG ranking procedure does not allow it since ranks can change arbitrarily when a \(\textsf{Fin}\) state is encountered), however, it performs the complementation for the k Rabin pairs at once and avoids performing the product. The complexity of our approach is better; combining the two approaches to get an even better complexity is future work.
The complexity of our approach is also better than the complexity of a procedure that would first transform the input Rabin automaton into a BA with \(m = nk\) states and run the optimal BA complementation with complexity \(\mathcal {O}(m(0.76m)^m) = \mathcal {O}(nk(0.76nk)^{nk})\) [38], as shown by the following lemmas.
\(n^k(0.76n)^{nk} = (\root n \of {n}\cdot 0.76n)^{nk}\). The global maximum of the function \(\root n \of {n}\) is less than 1.5, so \((\root n \of {n}\cdot 0.76n)^{nk} < (1.14n)^{nk} < (2n+1)^{nk}\) for \(n \ge 1\). \(\square \)
Similar reasoning as in the proof of Lemma 19. \(\square \)
5.3 Parity Automata
Since the parity condition is a special case of the Rabin condition [15], we can easily give an upper bound on the complementation of parity automata.
Lemma 21
For a parity automaton \(\mathcal {A}\) with index k, there is a GBA for the complement of \(\mathcal {L}(\mathcal {A})\) with \(\frac{k}{2}\) colours and \(\mathcal {O}( tight (n\!+\!1)^{\frac{k}{2}}) \!=\! \mathcal {O}(n^{\frac{k}{2}} (0.76n)^{\frac{nk}{2}})\) states.
Proof
The min-odd parity acceptance condition is of the form
. If we transform the acceptance condition into the DNF, we obtain
which is a Rabin acceptance condition with \(\frac{k}{2}\) Rabin pairs. In the condition, e.g.,
denotes union of colours
and
, obtained by changing all occurrences of
and
in \(\mathcal {A}\)’s colouring function \(\textsf{p}\) to the new colour
. Note that we can use a new colour for each union of colours and we obtain the same number of colours as in \(\textsf{Acc}\). According to Corollary 18, the parity automaton \(\mathcal {A}\) can be complemented into a GBA with \(\mathcal {O}( tight (n+1)^{\frac{k}{2}})\) states. \(\square \)
We note that the complexity obtained by our general procedure is worse than the best one we are aware of, which is \(2^{\mathcal {O}(n \log n)}\) [7].
5.4 Generalized Rabin Automata
Recall that the generalized Rabin pair is of the form
. We can now easily combine the procedure for (standard) Rabin automata from the previous section and the procedure for \(\text {Inf}\)-TELA from Section 3.2 to construct the subprocedure \(\mathbb {S}^{\wedge \textsf{inf}}\) for
. The set of macrostates will be
Details are given in [20]. Similarly to Sections 3.2 and 5.2, one can then obtain the following bound on the size of the complement.
Lemma 22
Let \(\mathcal {A}\) be a generalized Rabin automaton with one generalized Rabin pair with \(\ell \)\(\text {Inf}\)s. Then, there exists a BA accepting the complement of \(\mathcal {A}\) with \(\mathcal {O}(\ell ^{n} tight (n+1)) = \mathcal {O}(n\ell ^n (0.76n)^n)\) states.
Theorem 23
Let \(\mathcal {A}\) be a generalized Rabin automaton with k generalized Rabin pairs, each with at most \(\ell \)\(\text {Inf}\)s. Then, there exists a GBA with k colours and \(\mathcal {O}(\ell ^{nk} tight (n+1)^k) = \mathcal {O}(n^k(0.76 \ell n)^{nk})\) states accepting \(\Sigma ^\omega \setminus \mathcal {L}(\mathcal {A})\).
There is not much work on the complementation of generalized Rabin automata or general TELAs (we are only aware of the upper bound \(2^{2^{\mathcal {O}(n)}}\) from [37])). One could approach the complementation by translation of the generalized Rabin automaton into a GBA using the technique from [22]. The technique first performs \(\text {Fin}\)-removal, i.e., it makes k copies of \(\mathcal {A}\), each with the corresponding \(\text {Fin}\)-transitions removed, obtaining a GBA with \(n(k+1)\) states and \(\ell \) colours (one can share colours across the independent copies). After that, we could use our GBA complementation algorithm from Section 3, which would give us a BA with \(\mathcal {O}(n(k+1)(0.76\ell n(k+1))^{n(k+1)})\) states, which is worse.
Let us observe the behaviour of the fraction with a simplified right-hand side: \(\frac{nk(0.76\ell nk)^{nk}}{n^k(0.76 \ell n)^{nk}} = \frac{nk^{nk+1}}{n^k}\). There are two options:
(i)
\(n \ge k\): in this case, \(k^{nk} \gg n^k\) and the claim holds.
(ii)
\(k \ge n\): in this case, \(k^k \gg n^k\) and the claim holds. \(\square \)
5.5 General TELAs
For complementation of general TELAs, we use the fact that any TELA can be converted into a generalized Rabin automaton with the same structure by modifying the acceptance condition into the DNF form (and not touching the structure of the automaton). For a TELA with k colours, the DNF will have at most \(2^k\) clauses (i.e., generalized Rabin pairs), each one with at most k literals.
Theorem 25
Let \(\mathcal {A}\) be a TELA with k colours. Then, there exists a GBA with \(2^k\) colours and \(\mathcal {O}(k^{n2^k} tight (n+1)^{2^k}) = \mathcal {O}(n^{2^k}(0.76 nk)^{n2^k})\) states accepting \(\Sigma ^\omega \setminus \mathcal {L}(\mathcal {A})\).
Lower bounds for complementation of classes of \(\omega \)-automata using the full automata technique were established in [45] (improving the previous \(\Omega (n!)\) lower bound of Michel [33]). The technique was later generalized to improve the lower bound of Rabin automata complementation [8]. A double exponential lower bound for complementation of general Emerson-Lei automata was given in [37]. See the survey in [4] for more details.
Simultaneously to establishing the lower bound, there emerged algorithms for determinizing and complementing various classes of \(\omega \)-automata. The optimal determinization approach for GBAs introduced in [39] yields a deterministic Rabin automaton with the number of states bounded by \((1.47 nk)^n\) for large k and \(2^n-1\) Rabin pairs. In [13], the Miyano-Hayashi construction [34] is used within Büchi determinization. Rank-based complementation of GBAs was proposed in [28]. Furthermore, there are approaches for semideterminization-based complementation of GBAs [3] with double exponential complexity. Regarding other acceptance conditions, determinization of parity automata based on root history trees was proposed in [40]. A rank-based complementation of Streett and Rabin automata was introduced in [27] and later improved by tree structures in [7]. Tight determinization of Streett automata was presented in [43]. A tight complementation technique for parity automata based on flattened nested history trees was then proposed in [41]. A lot of effort has been put into complementation of Büchi automata leading to algorithms roughly divided into several groups: Ramsey-based [5, 6, 42], rank-based [16, 18, 19, 26, 38, 44], determinization-based [30, 35, 36], slice-based [23], and others [1, 17, 31]. There are specialized more efficient algorithms for subclasses of BAs, such as inherently-weak [34], deterministic [29], semideterministic [2], elevator [17, 19], or unambiguous [12, 32] BAs.
Acknowledgments
We thank the anonymous reviewers for their insightful comments that helped improve the quality of the paper. This work has been supported by the Czech Ministry of Education, Youth and Sports ERC.CZ project LL1908, the Czech Science Foundation project 25-18318S, and the FIT BUT internal project FIT-S-23-8151.
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
We only consider transition-based acceptance in order to avoid cluttering the paper by dealing with accepting states and accepting transitions. Extending our approach to state/transition-based (or just state-based) automata is straightforward.
Note that there is also a more general definition of TELAs with \(\delta \subseteq \mathcal {Q}\times \Sigma \times 2^{\Gamma } \times \mathcal {Q}\); in this paper, we use the simpler one.
We consider the so-called parity min odd condition; any parity condition from the set \(\{\text {min}, \text {max}\} \times \{\text {even}, \text {odd}\}\) can be easily translated to it.
denotes that all transitions labeled with
must occur only finitely often in an accepting run and
denotes that there must be a transition labeled with
occurring infinitely often. There are two main reasons for using more complex acceptance conditions: (i) more compact representation of automata and (ii) the ability to determinize (deterministic BAs are strictly less expressive than BAs).
given a compatible complementation procedure for formula \(\varphi \).
) and, in turn, obtain an algorithm for complementing Rabin automata with k Rabin pairs with the complexity \(\mathcal {O}(n^k(0.76n)^{nk})\), which is, again, better than any other algorithm that we know of.
) and obtain complementation constructions for generalized Rabin automata and TELAs with the upper bound \(\mathcal {O}(n^{2^k}(0.76 nk)^{n2^k})\), which is the best upper bound for complementation of general TELAs that we are aware of.
, etc.), we define the set of Emerson-Lei acceptance conditions \(\mathbb{E}\mathbb{L}(\Gamma )\) as the set of formulae constructed according to the following grammar:for \(c \in \Gamma \). The satisfaction relation \(\models \) for a set of colours \(M \subseteq \Gamma \) and a condition \(\alpha \) is defined inductively as follows (for \(c \in \Gamma \)): 
and the acceptance condition
. We define \(|\mathcal {A}| = |\mathcal {Q}|\).
.
,
,
,
,
,
, and
,
, an edge \(((q, i), (q', i+1)) \in E\) is a
-edge if
and a vertex \(v \in V\) is
-endangered iff it cannot reach any
-edge. For a set of colours \(C \subseteq \Gamma \), v is C-endangered iff it is
-endangered for every
. For example, in Fig. 2, the vertices (q, 1) and (t, 2) are
-endangered but they are not
-endangered. A pair of vertices \(v_1, v_2 \in V\) is converging iff \( reach (v_1) \cap reach (v_2) \ne \emptyset \) (\(v_1\) and \(v_2\) converge). A function \(r:V \rightarrow \omega \) is a run DAG ranking if for every \(v \in V\) it holds that \(\forall u \in reach (v) :r(u) \le r(v)\). We use \(\max (r)\) to denote the rank of r, i.e., the maximum value from \(\{r(u) \mid u \in V\}\) if it exists and \(\infty \) otherwise. A ranking r of \(\mathcal {G}\) is called tight iff there exists a level i such that (i) \(m = \max \{r((q,i)) \mid q \in \mathcal {Q}\}\) is odd and (ii) for all levels \(j \ge i\) it holds that \(\{1,3,\dots ,m\} \subseteq \{ r((q,j)) \mid q\in \mathcal {Q}\}\).
by
(this can be viewed as negating \(\textsf{Acc}\), transforming it into the negation normal form, substituting
by
, and denoting each
just by
). Let \(\mathcal {M}_{\overline{\textsf{Acc}}}\) be the set of models of \(\overline{\textsf{Acc}}\) where the colours
are interpreted as propositional variables. For example, if
, then
and
(\(\mathcal {M}_{\overline{\textsf{Acc}}}\) can be interpreted as saying which combinations of \(\text {Inf}\)-conditions need to be broken in order to break \(\textsf{Acc}\); in the example above, we can, e.g., break
, we can break both
and
, etc.). Furthermore, we use \(\mathcal {M}^{\min }_{\overline{\textsf{Acc}}}\) to denote the set of minimal models of \(\overline{\textsf{Acc}}\), i.e., \(\mathcal {M}^{\min }_{\overline{\textsf{Acc}}}\) is the set where (i) for every model \(m \in \mathcal {M}_{\overline{\textsf{Acc}}}\), there exists a model \(m' \in \mathcal {M}^{\min }_{\overline{\textsf{Acc}}}\) such that \(m' \subseteq m\), and (ii) there are no \(m, m' \in \mathcal {M}^{\min }_{\overline{\textsf{Acc}}}\) such that \(m \subset m'\). We note that \(\mathcal {M}_{\overline{\textsf{Acc}}}\) can be obtained as the upward closure of \(\mathcal {M}^{\min }_{\overline{\textsf{Acc}}}\) (and \(\mathcal {M}^{\min }_{\overline{\textsf{Acc}}}\) is an antichain). For the example acceptance condition above,
. Moreover, we use \({\textbf {lex-min}}(\overline{\textsf{Acc}})\) to denote the lexicographically smallest model from \(\mathcal {M}^{\min }_{\overline{\textsf{Acc}}}\) (w.l.o.g., we assume \(\mathcal {M}_{\overline{\textsf{Acc}}}\ne \emptyset \)). \({\textbf {lex-min}}(\overline{\textsf{Acc}})\) is used to pinpoint one model when any model can be used.
since \(\mathcal {A}_{ ex }\) is a GBA. In addition, for the run DAG in Fig. 2 and a set \(\{(q,1),(t,2)\}\), the mapping
is endangered in \(\mathcal {G}\). On the other hand, there exists no endangered mapping for the set \(\{(s,2)\}\) in \(\mathcal {G}\), as (s, 2) can reach both a
-edge as well as a
-edge.
, then every path in \(\mathcal {G}^i\) starting in u satisfies the condition
(the path breaks all the
conditions, i.e., \(\eta \) is endangered). If such a model assignment exists (the choice is nondeterministic), the algorithm assigns rank \(i+1\) to all vertices reachable from U and removes them from the DAG, creating DAG \(\mathcal {G}^{i+1}\) (Lines 7–9).
. The mapping \(\eta _1\) is endangered in \(\mathcal {G}^0\) because the following conditions hold:
transition, and
).
. (Line 7)
; there are many non-accepting paths from (q, 0)—e.g., a path that alternates between a q-vertex and an r-vertex and never touches any s-vertex). While constructing \(\pi \), for every clause \(\varphi _j\) we will be tracking the information about which atom of \(\varphi _j\) we should see next in order to satisfy \(\varphi _j\) on the path. In particular, we will start from a vertex \(v_0\) that is a root vertex of \(\mathcal {G}^i\) and we will use the tuple \(t_0 = (c^1_1, \ldots , c^\ell _1)\) to keep track of the colours. Using (Reach), it follows that there is a clause \(\varphi _j\) s.t. \(v_0\) can reach a \(c^j_1\)-edge \(e_1\). We will set \(t_1 = (c^1_1, \ldots , c^j_2, \ldots , c^\ell _1)\) and continue in a similar way: from every vertex we encounter, we use (Reach) to obtain an edge that is a c-edge for some c in \(t_i\). In the case we need to increment some component of \(t_i\) from \(c^j_{k_j}\), we set the new value to \(c^j_1\). The path \(\pi \) is then constructed as an infinite path that goes through the infinite sequence \(v_0, e_1, e_2, \ldots \) Note that because the sequence \(v_0, e_1, e_2 \ldots \) is infinite, due to the pigeonhole principle there will be a clause \(\varphi _j\) s.t. the sequence \(t_0, t_1, \ldots \) infinitely often increments the j-th component and so \(\pi \) is accepting. From \(\pi \), we can now extract the accepting run of \(\mathcal {A}\) on w. \(\square \)
s.t.
(otherwise, \(w\) would not be accepted by \(\mathcal {A}\)). Therefore, \((\rho _j, j)\) is not M-endangered. Hence, in every iteration of Algorithm 1, all vertices \((\rho _j, j)\) stay in \(\mathcal {G}^i\). From Lemma 3 we have that Algorithm 1 always terminates, but \(\mathcal {G}^i \ne \emptyset \) for each i. Therefore, the algorithm terminates with \(\bot \). \(\square \)
, iff
-edge to \(v'\) and
is in the model assigned to v, the vertex \(v'\) has to have a lower rank than v, because when v is removed from \(\mathcal {G}_{w}^i\), there is no reachable
-edge in \(\mathcal {G}_{w}^i\). Moreover, if the model is changed between v and \(v'\) and the rank is odd, then the rank also has to be decreased.
,\(*\)\( rank (f) = rank (f')\),\(*\)and\(\cdot \)\(i' = (i+2) \mod ( rank (f') + 1)\) and \(O' = f'^{-1}(i')\) if \(O = \emptyset \) or\(\cdot \)\(i' = i\) and \(O' = \delta (O, a) \cap f'^{-1}(i)\) if \(O \ne \emptyset \), and
for all \(j>p\). Since \(\rho \) is accepting in \(\mathcal {A}\), eventually there will be a position \(k > p\) such that \(f_k(\rho (k))\), \(f_{k+1}(\rho (k+1))\), \(f_{k+2}(\rho (k+2))\), ...are all even (because there is no model satisfying \(\rho \) in \(\mathcal {M}^{\min }_{\overline{\textsf{Acc}}}\), so points (iib) and (iic) from the definition of
will enforce this). For the sake of contradiction, assume that \(\rho ''\) is accepting. Then for some position \(\ell > k\), because the i-component of a macrostate rotates over all even ranks, it holds that \(i_\ell = f_\ell (\rho (\ell ))\) and \(\rho (\ell ) \in O_\ell = f_\ell ^{-1}(\rho (\ell ))\). We can easily show by induction that for all \(j \ge \ell \), it holds that \(\rho (j) \in O_j \ne \emptyset \), which is in contradiction with the assumption that \(\rho ''\) is accepting.
, there is a runsuch that \(f_k(q) = r((q,k))\) and \(\mu _k(q) = m((q,k))\) for all \(k > p\). In order to show that \(\rho ''\) is acepting, we need to show that the O-component of the macrostates on the run is empty infinitely often. Assume by contradiction that there is an index \(\ell > p\) such that \(O_j\) is non-empty for all \(j \ge \ell \). Then, there is a vertex \((q,\ell ) \in \mathcal {G}_{w}\) s.t. \(r((q,\ell ))\) is even and there are infinitely many vertices reachable from \((q,\ell )\) with the same even rank, which is a contradiction with the construction of r in Algorithm 1, which would give some of the vertices odd ranks. \(\square \)
. The formula is in DNF, hence
and \(|\mathcal {M}^{\min }_{\overline{\textsf{Acc}}}| = k\). The number of all level models is \(k^n\). \(\square \)
TELAs
for any \(\varphi \), parameterized by an algorithm for complementing TELAs with the condition \(\varphi \). In Section 5, we will then instantiate the algorithm for some common acceptance conditions, eventually obtaining an efficient complementation algorithm for general TELAs.
and let \(\Delta \) be \(\delta \) without transitions whose label contains
. For a word \(w\in \Sigma ^\omega \), we define a relaxed run DAG (RRDAG) over \(w\), denoted by \(\mathcal {G}^{\Delta }_{w}\), as any sequence of states \(\mathcal {G}^{\Delta }_{w}= (S_0, S_1, \dots )\) where \(S_i \subseteq \mathcal {Q}\) and \(\Delta (S_{i}, w_{i}) \subseteq S_{i+1}\). Intuitively, an RRDAG over a word may contain more states on each level than it is necessary from the reachability of \(\Delta \). Note that this definition of RRDAGs is equivalent to having vertices of the form (q, i), where \(q \in S_i\) with edges given implicitly by \(\Delta \). We use these definitions interchangeably. Clearly, there may be multiple RRDAGs over a single word, they are all, however, subgraphs of the (standard) run DAG \(\mathcal {G}_{w}\). We say that \(\mathcal {G}^{\Delta }_{w}= (S_0, S_1, \dots )\) is accepting wrt \(\varphi \), written as \(\mathcal {G}^{\Delta }_{w}\models \varphi \), if there is a run \(\rho = q_k q_{k+1} \ldots \) for \(k \ge 0\) in \(\Delta \) such that for every \(i \ge k\) it holds that \(q_i \in S_i\) and \(q_{i+1} \in \Delta (q_i, w_{i})\), and, moreover, \(\rho \models \varphi \) (i.e., the accepting run does not need to start at the beginning of \(\mathcal {G}^{\Delta }_{w}\)). The reason for introducing RRDAGs is that the algorithm for condition \(\varphi \) will construct a BA that runs over RRDAGs constructed using the restricted transition relation \(\Delta \). The relaxation allows us to introduce new vertices (not connected to the root of the RRDAG) at any level that represent runs that have seen finitely many times a
transition in \(\delta \).
is given wrt a subprocedure for complementing a TELA with condition \(\varphi \). The subprocedure is given as a tuple \(\mathbb {S}_{\Delta }^{\varphi }= (\mathcal {M}, \mathcal {M}_0, \textsf{SuccAct}_{\Delta }, \textsf{SuccTrack}_{\Delta }, \textsf{EmptyBreak})\), where
condition. The reason for using two transition functions (\(\textsf{SuccAct}_\Delta \) and \(\textsf{SuccTrack}_\Delta \)) is that some subprocedures that we will introduce later will use two types of macrostates: active and tracking. For instance, if \(\mathbb {S}_{\Delta }^{\varphi }\) is a rank-based procedure (cf. Section 5.2), active macrostates will contain breakpoints, which the construction will try to empty, and once a breakpoint is seen, \(\textsf{FinCompl}\) will add some more runs to the rank-based algorithm. The new runs might not be tight at the given point, so we switch into the tracking mode and wait for newly added runs to become tight before switching into the active mode again.
-transition (in P). Whenever \(\mathbb {S}_{\Delta }^{\varphi }\) clears its breakpoint, P is re-sampled (and some new runs can be added to \(\mathbb {S}_{\Delta }^{\varphi }\)).
, we therefore need to provide a trivial subprocedure \(\mathbb {S}^{ tt }=(\mathcal {M}^{ tt }, \mathcal {M}^{ tt }_0, \textsf{SuccAct}^{ tt }_\Delta , \emptyset , \textsf{EmptyBreak}^{ tt })\) that is correct for \( tt \) (notice that \(\textsf{SuccTrack}^{ tt }_\Delta \) is empty). In the subprocedure, \(\mathcal {M}^{ tt }= 2^\mathcal {Q}\), \(\mathcal {M}^{ tt }_0 = \{ I \}\), and the remaining components are given as follows:Intuitively, the instantiated procedure works with macrostates (S, P, P) (i.e., to adhere to the formal definition of \(\textsf{FinCompl}\), P is there twice) where S tracks all runs and P is a breakpoint that contains runs that yet need to either terminate or see
. To accept, P needs to be emptied infinitely often. One can observe that \(\textsf{FinCompl}(\mathbb {S}^{ tt }, \mathcal {A})\) resembles the well-known Miyano-Hayashi construction [34] for complementation of co-Büchi automata.
, which will allow us to complement TELAs where the acceptance condition is a single Rabin pair. The algorithm is based on the optimal rank-based BA complementation algorithm from [38] adjusted to the needs of the modular construction. The macrostates of the instantiation are given aswhere \(\mathcal {M}^{\textsf{inf}}_0 = \{ I \}\). Notice that active macrostates (\(\mathcal {M}^{\textsf{inf}}_{\textsf{Act}}\)) are either sets of states (from \(2^\mathcal {Q}\), just keeping track of all runs) or states of the form (f, O, i) (representing tight runs). On the other hand, tracking macrostates (\(\mathcal {M}^{\textsf{inf}}_{\textsf{Track}}\)) are of the form (f, i); these are used to wait for newly arrived runs to become tight. The remaining components are then defined as follows:
.
iff there is an accepting \(\textsf{Fin}\)-run of \(\mathbb {S}^{\textsf{inf}}\) over \(\mathcal {G}_w^\Delta \). We begin with the proof of the statement from left to right. Assume that \(\mathcal {G}_w^\Delta \) is not accepting wrt
. There is either no run of \(\mathcal {G}_w^\Delta \) on \(w\) at all or all runs do not satisfy the formula. If there is no run of \(\mathcal {G}_w^\Delta \) on \(w\), then there is a sequence \((M_0, M_1, \ldots )\) where \(M_0 = I\) and \(M_{j+1} = \Delta (M_j, a)\) for all \(j\ge 0\) such that there is some \(i \ge 0\) such that \(M_l = \emptyset \) for all \(l \ge i\). The predicate \(\textsf{EmptyBreak}(M_l)\) is true for all \(l \ge i\), so it holds infinitely often, and there therefore exists an accepting run of \(\mathbb {S}^{\textsf{inf}}\) over \(\mathcal {G}_w^\Delta \). Now assume that there is a run of \(\mathcal {G}_w^\Delta \) on w. Then, no matter from which point there are no transitions from
, the condition
does not hold for the particular run. With every transition \((f,i) \rightarrow (f',O',i')\) we sample all currently reachable states and then check that all runs from these states contain transitions from
only finitely often by modified Schewe’s rank-based algorithm. The O-component is emptied infinitely often and so there is an accepting run of \(\mathbb {S}^{\textsf{inf}}\) over \(\mathcal {G}_w^\Delta \).
does not hold for any run, no matter when the run stops containing transitions from
. The formula is therefore not satisfied in any run and \(\mathcal {G}_w^\Delta \) is not accepting. \(\square \)
condition is “for free,” i.e., the asymptotical complexity stays the same as for the optimal algorithm for BA complementation from [38].
. If we transform the acceptance condition into the DNF, we obtain
which is a Rabin acceptance condition with \(\frac{k}{2}\) Rabin pairs. In the condition, e.g.,
denotes union of colours
and
, obtained by changing all occurrences of
and
in \(\mathcal {A}\)’s colouring function \(\textsf{p}\) to the new colour
. Note that we can use a new colour for each union of colours and we obtain the same number of colours as in \(\textsf{Acc}\). According to Corollary 18, the parity automaton \(\mathcal {A}\) can be complemented into a GBA with \(\mathcal {O}( tight (n+1)^{\frac{k}{2}})\) states. \(\square \)
. We can now easily combine the procedure for (standard) Rabin automata from the previous section and the procedure for \(\text {Inf}\)-TELA from Section 3.2 to construct the subprocedure \(\mathbb {S}^{\wedge \textsf{inf}}\) for
. The set of macrostates will beDetails are given in [20]. Similarly to Sections 3.2 and 5.2, one can then obtain the following bound on the size of the complement.
