$|T_v| \le |Z_F|$, and therefore the size of $\mathcal{ACD}_{TS}$ is polynomial in $Z_F$. This, and the question of the complexity of computing the ACD is the subject of an independent work [26].

**Local Muller languages.** For a recurrent state $v$ of $TS$, we define the *local Muller language of* $TS$ at $v$ as the Muller language defined over the alphabet $\Gamma_v = Cycles_v(TS)$ associated to:

$$ \text{LocalMuller}_{\mathcal{T}S}(v) = \{C \subseteq Cycles_v(\mathcal{T}S) \mid \bigcup_{\ell \in C} \ell \text{ is an accepting cycle}\}. $$

We note that $\text{LocalMuller}_{\mathcal{T}S}(v)$ is determined by singletons ($C \in \text{LocalMuller}_{\mathcal{T}S}(v)$ if and only if $\{\bigcup_{\ell \in C} \ell\} \in \text{LocalMuller}_{\mathcal{T}S}(v)$). For simplicity, and by a slight abuse of notation, we will work as if $\text{LocalMuller}_{\mathcal{T}S}(v) \subseteq Cycles_v(\mathcal{T}S)$. Also, to lighten notations, we will just write $\text{LocalMuller}_{\mathcal{T}S}(v)$ to denote $\text{Muller}(\text{LocalMuller}_{\mathcal{T}S}(v))$ whenever no confusion arises.

The following lemma directly follows from the definition of $T_v$ and that of the Zielonka tree. It provides insight in the structure of the trees $T_v$, and it will be a key ingredient in the proof of the optimality of the transformations based on the alternating cycle decomposition.

**LEMMA 5.9.** The tree $T_v$ is the Zielonka tree of the family $\text{LocalMuller}_{\mathcal{T}S}(v)$,<fnref n="9" /> for any recurrent vertex $v$.

## 5.2 An optimal transformation to parity transition systems

We now define the ACD-parity-transform, an optimal transformation turning a Muller TS into a parity TS while preserving determinism. In order to obtain the optimality in the number of output colours, we need to pay attention to the parity of the minimal colour used in different SCCs. To incorporate this parameter in the transformation, we define positive and negative ACDs.

Let $TS$ be a Muller transition system and let $\mathcal{ACD}_{TS} = \{\text{AltTree}(\ell_1), \dots, \text{AltTree}(\ell_k)\}$ be its alternating cycle decomposition.

We say that a tree $\text{AltTree}(\ell_i) \in \mathcal{ACD}_{TS}$ is *positive* if $\ell_i$ is an accepting cycle, and that it is *negative* otherwise. We say that the alternating cycle decomposition of $TS$ is *positive* if all the trees of maximal height of $\mathcal{ACD}_{TS}$ are positive, that it is *negative* if all trees of maximal height are negative, and that it is *equidistant* if there are positive and negative trees of maximal height.

As for the Zielonka tree, we associate a non-negative integer to each level of the trees of $\mathcal{ACD}_{TS}$ via a function $p_{\mathcal{ACD}}(n): \text{Nodes}(\mathcal{ACD}_{TS}) \to \mathbb{N}$. Let $\ell_i$ be a maximal cycle of $TS$ and $n \in N_{\ell_i}$.

— If $\mathcal{ACD}_{TS}$ is positive or equidistant:

— $p_{\mathcal{ACD}}(n) = \text{Depth}(n)$, if $\ell_i$ is accepting,

<footnote n="9">9 Formally, the labelling $v$ of $T_v$ goes to $Cycles_v(TS)$, and not to $2_+^{Cycles_v(TS)}$, as required by the definition of the Zielonka tree. To obtain a proper Zielonka tree with a labelling of nodes $v': N_v \to 2_+^{Cycles_v(TS)}$, we would have to define $v'(n) = \{\ell' \in Cycles_v(TS) | \ell' \subseteq v(n)\}$.</footnote>
— $p_{\mathcal{ACD}}(n) = \text{Depth}(n) + 1$, if $\ell_i$ is rejecting.

— If $\mathcal{ACD}_{\mathcal{TS}}$ is negative:

— $p_{\mathcal{ACD}}(n) = \text{Depth}(n) + 2$, if $\ell_i$ is accepting,

— $p_{\mathcal{ACD}}(n) = \text{Depth}(n) + 1$, if $\ell_i$ is rejecting.

We let $\min_{\mathcal{TS}}$ (resp. $\max_{\mathcal{TS}}$) be the minimum (resp. maximum) value taken by the function $p_{\mathcal{ACD}}$.

**REMARK 5.10.** A node $n$ in $\text{AltTree}(\ell_i)$ verifies that $p_{\mathcal{ACD}}(n)$ is even if and only if $\nu(n)$ is an accepting cycle (that is, if $n$ is a round node).

**REMARK 5.11.** It is satisfied:

— $\min_{\mathcal{TS}} = 0$ if $\mathcal{ACD}_{\mathcal{TS}}$ is positive or equidistant,

— $\min_{\mathcal{TS}} = 1$ if $\mathcal{ACD}_{\mathcal{TS}}$ is negative.

**EXAMPLE 5.12.** In the previous Example 5.5, $\text{AltTree}(\ell_1)$ is a positive tree and $\text{AltTree}(\ell_2)$ is negative. As $\text{AltTree}(\ell_2)$ is the tree of maximal height, $\mathcal{ACD}_{\mathcal{TS}}$ is negative. The function $p_{\mathcal{ACD}}$ is represented in Figure 16 by the integers on the right of each tree. It takes values 2 and 3 over $\text{AltTree}(\ell_1)$ ($p_{\mathcal{ACD}}(\alpha) = 2$ and $p_{\mathcal{ACD}}(\beta) = 3$), because $\mathcal{ACD}_{\mathcal{TS}}$ is negative. In this example, $\min_{\mathcal{TS}} = 1$ and $\max_{\mathcal{TS}} = 3$. We note that if we had associated integers 0 and 1 to the levels of $\text{AltTree}(\ell_1)$, we would have used 4 integers in total, instead of just 3 of them. ♦

**DEFINITION 5.13 (ACD-parity-transform).** Let $\mathcal{TS}$ be a Muller TS with $\mathcal{ACD}_{\mathcal{TS}} = \{\text{AltTree}(\ell_1), \dots, \text{AltTree}(\ell_k)\}$. We define the *ACD-parity-transform* of $\mathcal{TS}$ be the parity TS $\text{ACD}_{\text{parity}}(\mathcal{TS}) = (G', \text{Acc}'),$ with $G' = (V', E', \text{Source}', \text{Target}', I')$, and $\text{Acc}' = (\gamma', [\min_{\mathcal{TS}}, \max_{\mathcal{TS}}], \text{parity})$ defined as follows.

**Vertices.** The set of vertices is

$$V' = \bigcup_{v \in V} (\{v\} \times \text{Leaves}(\mathcal{T}_v)).$$

**Initial vertices.** $I' = \{(v_0, n) \mid v_0 \in I \text{ and } n \text{ is the leftmost leaf in } \mathcal{T}_{v_0}\}$.

**Edges and output colours.** For each $(v, n) \in V'$ and each edge $e = v \to v' \in \text{Out}(v)$ in $\mathcal{TS}$ we define an edge $e_n = (v, n) \xrightarrow{\gamma'(e_n)} (v', n')$. Formally,

$$E' = \bigcup_{e \in E} (\{e\} \times \text{Leaves}(\mathcal{T}_{\text{Source}(e)})).$$

If $v$ and $v'$ are not in the same SCC, we let $n'$ be the leftmost leaf in $\mathcal{T}_{v'}$ and $\gamma'(e_n) = \min_{\mathcal{TS}}$.<fnref n="10" /> If $v$ and $v'$ belong to the same SCC, we let:

— $n' = \text{Jump}_{\mathcal{T}_{v'}}(n, \text{Supp}(n, e))$,

— $\gamma'(e_n) = p_{\mathcal{ACD}}(\text{Supp}(n, e))$.

<footnote n="10">10 The colours associated to transitions changing of SCC are almost arbitrary (we could even leave them uncoloured). We define them to be the minimal colour used so that the obtained transition system is normalised in the sense of Section 6.2.</footnote>
**Labellings.** If $\mathcal{T}\mathcal{S}$ is a labelled transition system, with labels $l_V: V \to L_V$ and $l_E: E \to L_E$, we label $\text{ACD}_{\text{parity}}(\mathcal{T}\mathcal{S})$ by $l'_{V'}(v, n) = l_V(v)$ and $l'_{E'}(e_n) = l_E(e)$.

Intuitively, a run in the transition system $\text{ACD}_{\text{parity}}(\mathcal{T}\mathcal{S})$ follows a run in $\mathcal{T}\mathcal{S}$ with some extra information, updated in the same manner as it was the case with the ZT-parity-automaton. To define transitions in $\text{ACD}_{\text{parity}}(\mathcal{T}\mathcal{S})$, we move simultaneously in $\mathcal{T}\mathcal{S}$ and in $\mathcal{ACD}_{\mathcal{T}\mathcal{S}}$. When we take a transition $e$ in $\mathcal{T}\mathcal{S}$ that goes from $v$ to $v'$, while being in a node $n$ in the ACD, we climb the branch of $n$ searching the lowest node $\tilde{n}$ with $e$ and $v'$ in its label ($\tilde{n} = \text{Supp}(n, e)$). We produce as output the colour corresponding to the level reached. If no such node exists in the current tree (this occurs if we change of SCC), we jump to the root of the tree containing $v'$. After having reached the node $\tilde{n}$, we move to its next child in the tree $\mathcal{T}_{v'}$ (in a cyclic way), and we pick the leftmost leaf under it.

**EXAMPLE 5.14.** We show in Figure 17 the ACD-parity-transform $\text{ACD}_{\text{parity}}(\mathcal{T}\mathcal{S})$ of the transition system $\mathcal{T}\mathcal{S}$ from Figure 15 (Example 5.5). For each vertex $v$ in $\mathcal{T}\mathcal{S}$, we make as many copies as leaves of the tree $\mathcal{T}_v$. We note that, as $v_0$ is transient, the tree $\mathcal{T}_{v_0}$ consists of a single node (by definition), that we name $\iota$. Transitions are of the form $(e, l)$, for $e$ a transition from $\mathcal{T}\mathcal{S}$ and $l$ a leaf of some local subtree; these are denoted $e_\iota$ in the figure for the sake of space convenience. These labels simply indicate the names of the edges, they should not be interpreted as input letters ($\text{ACD}_{\text{parity}}(\mathcal{T}\mathcal{S})$ is not an automaton).

We observe that the mappings $\varphi_V(v, \iota) = v$ and $\varphi_E(e_\iota) = e$ define a locally bijective morphism of transition systems from $\text{ACD}_{\text{parity}}(\mathcal{T}\mathcal{S})$ to $\mathcal{T}\mathcal{S}$.

<figure><img src="image_28.png" /><figcaption>**Figure 17.** ACD-parity-transform $\text{ACD}_{\text{parity}}(\mathcal{T}\mathcal{S})$ of the transition system $\mathcal{T}\mathcal{S}$ from Figure 15.</figcaption></figure>

Another example can be found in Figure 18.

<figure><img src="image_29.png" /></figure>
**REMARK 5.15.** The size of the ACD-parity-transformation of $\mathcal{T}S$ is:

$$|\text{ACD}_{\text{parity}}(\mathcal{T}S)| = \sum_{v \in V} |\text{Leaves}(\mathcal{T}_v)| = \sum_{v \in V_{\text{rec}}} |\text{Leaves}(\mathcal{T}_v)| + |V_{\text{trans}}|,$$

where $V_{\text{rec}}$ and $V_{\text{trans}}$ are the sets of recurrent and transient vertices of $\mathcal{T}S$, respectively.

**REMARK 5.16.** We remark that if $\mathcal{T}S = (G_{\mathcal{T}S}, \text{Acc}_{\mathcal{T}S})$ is already a parity TS, then the underlying graphs of $\text{ACD}_{\text{parity}}(\mathcal{T}S)$ and $\mathcal{T}S$ are isomorphic. In fact, by Proposition 5.19, $\text{ACD}_{\text{parity}}(\mathcal{T}S)$ and $\mathcal{T}S$ will also be isomorphic as transition systems. In this case, the construction of $\text{ACD}_{\text{parity}}(\mathcal{T}S)$ boils down to the application of the procedure described by Carton and Maceiras [19].

**REMARK 5.17.** The ACD-parity-transform is oblivious to the labelling $\gamma$ of the acceptance condition of $\mathcal{T}S$; the only information taken into account to define the graph of $\text{ACD}_{\text{parity}}(\mathcal{T}S)$ and its output colours is the structure of the trees of $\mathcal{ACD}_{\mathcal{T}S}$. That is, the definition of this transformation is independent of the actual representation of the acceptance condition of $\mathcal{T}S$ (whether it is Emerson-Lei, Muller, Rabin...), and we only use that any such representation induces a mapping $f: \text{Cycles}(\mathcal{T}S) \to \{\text{Accept, Reject}\}$.

**REMARK 5.18.** The ZT-parity-automaton can be seen as a special case of the ACD-parity-transform, as $\mathcal{A}_{\mathcal{ZF}}^{\text{parity}}$ coincides with the DPA $\text{ACD}_{\text{parity}}(\mathcal{A})$, where $\mathcal{A}$ is the DMA with a single state recognising Muller($\mathcal{F}$) (see Remark 5.7).

**Correctness of the ACD-parity-transform.**

**PROPOSITION 5.19 (Correctness of the ACD-parity-transform).** Let $\mathcal{T}S$ be a (labelled) Muller TS and let $\text{ACD}_{\text{parity}}(\mathcal{T}S)$ be its ACD-parity-transform. There is a locally bijective morphism of (labelled) transition systems $\varphi: \text{ACD}_{\text{parity}}(\mathcal{T}S) \to \mathcal{T}S$.

The following lemma, analogous to Lemma 4.11 from Section 4.2, follows from the definition of the ACD-parity-transform.

**LEMMA 5.20.** Let $n$ be a node of $\text{AltTree}(\ell_i)$, let $\tilde{n}$ be an ancestor of $n$ and let $e = v \to v'$ be an edge in $\ell_i$. Then, $\text{Supp}(n, e)$ is a descendant of $\tilde{n}$ if and only if $e \in v(\tilde{n})$, and in this case, if $e_n = (v, n) \to (v', n')$ is an edge of $\text{ACD}_{\text{parity}}(\mathcal{T}S)$, then $n'$ is a descendant of $\tilde{n}$ too.

**PROOF OF PROPOSITION 5.19.** We consider the mapping $\varphi = (\varphi_V, \varphi_E)$ naturally defined by $\varphi_V(v, n) = v$ and $\varphi_E(e_n) = e$. It is immediate to check that $\varphi$ is a weak morphism of transition systems (it preserves initial states and transitions). Also, it is easy to see that it is locally bijective: for each initial state $v_0 \in I$, there is exactly one node in $I'$ of the form $(v_0, n)$: the node where $n$ is the leftmost leaf of $\mathcal{T}_v$; and for each vertex $(v, n)$ and edge $e \in \text{Out}(v)$ of $\mathcal{T}S$, we have defined exactly one edge outgoing from $(v, n)$ corresponding to $e$.
We prove that $\varphi$ preserves the acceptance of runs, following the proof scheme from Proposition 4.10. We can assume w.l.o.g. (see Remarks 2.1 and 5.17) that the set of output colours used by $\mathcal{T}S$ is its set of edges $E$. Let $\rho \in \mathcal{R}un(\mathcal{ACD}_{parity}(\mathcal{T}S))$ be an infinite run in $\mathcal{ACD}_{parity}(\mathcal{T}S)$. Eventually, $\rho$ will remain in one SCC, and $\text{Inf}(\rho)$ will form a cycle that is accepting if and only if $\rho$ is an accepting run. We will assume that all the edges in $\rho$ appear infinitely often and belong to this cycle (we can do it by using a similar argument as the one presented in the proof of Proposition 4.10), and we let:

$$ \rho = (v_0, n_0) \xrightarrow{x_0} (v_1, n_1) \xrightarrow{x_1} (v_2, n_2) \xrightarrow{x_3} \dots $$

The projection of $\rho$ under $\varphi$ is:

$$ \varphi_{\mathcal{R}uns}(\rho) = v_0 \xrightarrow{e_0} v_1 \xrightarrow{e_1} v_2 \xrightarrow{e_3} \dots $$

We note that the edges $\{e_0, e_1, \dots\}$ form a cycle in $\mathcal{T}S$, that we will call $\ell_{\rho}$. In particular, $\ell_{\rho}$ is contained in some maximal cycle $\ell_{\max}$, and all the nodes $n_i$ belong to the same tree $\text{AltTree}(\ell_{\max})$ of the ACD. Our objective is to show that $\ell_{\rho}$ is an accepting cycle in $\mathcal{T}S$ if and only if $\min\{x_0, x_1, x_2, \dots\}$ is even. We let $\tilde{n}_i = \text{Supp}(n_i, e_i)$ be the node of $\mathcal{ACD}_{\mathcal{T}S}$ determining the $i^{th}$ transition of $\rho$, so we have that $x_i = p_{\mathcal{ACD}}(\tilde{n}_i)$. Finally, let $n_{\rho}$ be the deepest ancestor of $n_0$ such that $\ell_{\rho} \subseteq \nu(n_{\rho})$.

**CLAIM 5.21.** For all $i \ge 0$, $n_i \ge n_{\rho}$ and $\tilde{n}_i \ge n_{\rho}$ (that is, all nodes appearing in $\rho$ are below $n_{\rho}$). In particular, $x_i \ge p_{\mathcal{ACD}}(n_{\rho})$.

**Proof.** The claim follows from Lemma 5.20 and induction.

<figure><img src="image_30.png" /></figure>

**CLAIM 5.22.** Let $n_{\rho,1}, \dots, n_{\rho,s}$ be an enumeration of Children$_{\text{AltTree}(\ell_{\max})}(n_{\rho})$. It holds that:

1. $\text{Supp}(n_i, e_i) = n_{\rho}$ infinitely often. In particular, $x_i = p_{\mathcal{ACD}}(n_{\rho})$ for infinitely many $i$'s.

2. There is no $n_{\rho,k} \in \text{Children}(n_{\rho})$ such that $\ell_{\rho} \subseteq \nu(n_{\rho,k})$.

**Proof.** The proof is identical to that of Claim 4.13, from Proposition 4.10.

<figure><img src="image_31.png" /></figure>

We conclude that $\min\{x_0, x_1, x_2, \dots\} = p_{\mathcal{ACD}}(n_{\rho})$, which is even if and only if $\ell_{\rho}$ is an accepting cycle, by Remarks 5.2 and 5.10.

<figure><img src="image_32.png" /></figure>

**REMARK 5.23.** We can give an alternative interpretation of the previous proof. Given a run $\rho$ in $\mathcal{T}S$ and a vertex $v$ appearing infinitely often in $\rho$, we can decompose the run into:

$$ \rho_0 \rightsquigarrow v \rho_1 \rightsquigarrow v \rho_2 \rightsquigarrow v \rho_3 \rightsquigarrow v \rho_4 \rightsquigarrow \dots, $$

where the finite runs $\rho_i$ are cycles over $v$, for $i > 0$. Therefore, the sequence of these cycles can be processed by the ZT-parity-automaton corresponding to the local Muller condition $\text{LocalMuller}_{\mathcal{T}S}(v)$. By Lemma 5.9 and the correctness of the ZT-parity-automaton, the minimal
colour produced by a run over this sequence of cycles in $\mathcal{A}_{\mathcal{Z}_{\text{LocalMuller}_{\mathcal{TS}}(v)}}^{\text{parity}}$ coincides with the minimal output colour produced by the run $\varphi_{\mathcal{R}uns}^{-1}(\rho)$ in the ACD-parity-transform $\text{ACD}_{\text{parity}}(\mathcal{TS})$ (disregarding the initial path $\rho_0$). This colour is exactly the one corresponding to the deepest node in $\mathcal{T}_v$ above the leftmost leaf containing $\text{Inf}(\rho)$.

The locally bijective morphism given by Proposition 5.19 witnesses that $\text{ACD}_{\text{parity}}(\mathcal{TS})$ shares the same semantic properties as $\mathcal{TS}$. The next corollaries follow from Proposition 3.16 and Corollary 3.19 (and the fact that the choice of initial vertices in $\text{ACD}_{\text{parity}}(\mathcal{TS})$ is arbitrary).

**COROLLARY 5.24.** Let $\mathcal{A}$ be a Muller automaton and let $\text{ACD}_{\text{parity}}(\mathcal{A})$ be its ACD-parity-transform. Then, $\mathcal{L}(\mathcal{A}) = \mathcal{L}(\text{ACD}_{\text{parity}}(\mathcal{A}))$, and $\mathcal{A}$ is deterministic (resp. history-deterministic) if and only if $\text{ACD}_{\text{parity}}(\mathcal{A})$ is deterministic (resp. history-deterministic).

**COROLLARY 5.25.** Let $\mathcal{G}$ be a Muller game and let $\text{ACD}_{\text{parity}}(\mathcal{G})$ be its ACD-parity-transform. Eve wins $\text{ACD}_{\text{parity}}(\mathcal{G})$ from a vertex of the form $(v, n)$ if and only if she wins $\mathcal{G}$ from $v$.

## 5.3 An optimal history-deterministic transformation to Rabin transition systems

In this section we describe the ACD-HD-Rabin-transform, an optimal transformation of Muller TS to Rabin TS preserving history-determinism. This construction generalises that from Section 4.3.

**DEFINITION 5.26 (ACD-HD-Rabin-transform).** Let $\mathcal{TS}$ be a Muller TS. For each vertex $v \in V$ we let $\eta_v: \text{Leaves}(\mathcal{T}_v) \to \{1, \dots, \text{rbw}(\mathcal{T}_v)\}$ be a mapping satisfying Property (⋆) from Lemma 4.42.

We define the ACD-HD-Rabin-transform of $\mathcal{TS}$ to be the Rabin TS $\text{ACD}_{\text{Rabin}}(\mathcal{TS}) = (G', \text{Acc}')$, with $G' = (V', E', \text{Source}', \text{Target}', I')$, and $\text{Acc}' = (\gamma', \text{Nodes}(\mathcal{ACD}_{\mathcal{TS}}), \text{Rabin}(R))$ defined as follows.

**Vertices.** The set of vertices is

$$V' = \bigcup_{v \in V} (\{v\} \times \{1, \dots, \text{rbw}(\mathcal{T}_v)\}),$$

where $\text{rbw}(\mathcal{T}_v)$ is the round-branching width of $\mathcal{T}_v$.

**Initial vertices.** $I' = \{(v_0, x) | v_0 \in I \text{ and } x \in \{1, \dots, \text{rbw}(\mathcal{T}_{v_0})\}\}$.

**Edges and output colours.** We let

$$E' = \bigcup_{e \in E} (\{e\} \times \text{Leaves}(\mathcal{T}_{\text{Source}(e)})).$$

For each edge $e = v \to v' \in E$ in $\mathcal{TS}$ and $x \in \{1, \dots, \text{rbw}(\mathcal{T}_v)\}$, we will place one edge from $(v, x)$ for each leaf $l$ of $\mathcal{T}_v$ such that $\eta_v(l) = x$. More precisely, we let $(v, x) \xrightarrow{n} (v', x') \in E'$ if either
— $v$ and $v'$ are not in the same SCC (in this case the output colour $n$ is irrelevant), or
— $v$ and $v'$ are in the same SCC and there are leaves $l$ and $l'$ of $\mathcal{T}_v$ and $\mathcal{T}_{v'}$, respectively, such that:
— $\eta_v(l) = x, \eta_{v'}(l') = x'$,

— $l' = \text{Jump}_{\mathcal{T}_{v'}}(l, \text{Supp}(l, e))$,

— $n = \text{Supp}(l, e)$.

**Rabin condition.** $R = \{(G_n, R_n)\}_{n \in \text{Nodes}(\mathcal{ACD}_{\mathcal{T}_S})}$, where $G_n$ and $R_n$ are defined as follows: Let $n$ be a round node, and let $n'$ be any node in $\text{Nodes}(\mathcal{ACD}_{\mathcal{T}_S})$,

$$ \begin{cases} n' \in G_n & \text{if } n' = n, \\ n' \in R_n & \text{if } n' \neq n \text{ and } n \text{ is not an ancestor of } n'. \end{cases} $$

**Labellings.** If $\mathcal{T}_S$ is a labelled transition system, with labels $l_V: V \to L_V$ and $l_E: E \to L_E$, we label $\text{ACD}_{\text{Rabin}}(\mathcal{T}_S)$ by $l'_{V}(v, x) = l_V(v)$ and $l'_{E'}(e') = l_E(e)$, if $e' \in E'(e)$.

This construction generalises the ZT-HD-Rabin-automaton in the same way as the ACD-parity-transform generalises the ZT-parity-automaton. Intuitively, a run in $\text{ACD}_{\text{Rabin}}(\mathcal{T}_S)$ can be identified with a promenade through the nodes of the ACD, which are used as the output colours to define the Rabin acceptance condition.

**REMARK 5.27.** The size of the ACD-HD-Rabin-transform of $\mathcal{T}_S$ is:

$$ |\text{ACD}_{\text{Rabin}}(\mathcal{T}_S)| = \sum_{v \in V} \text{rbw}(\mathcal{T}_v) = \sum_{v \in V_{\text{rec}}} \text{rbw}(\mathcal{T}_v) + |V_{\text{trans}}|, $$

where $V_{\text{rec}}$ and $V_{\text{trans}}$ are the sets of recurrent and transient vertices of $\mathcal{T}_S$, respectively.

**Correctness of the ACD-HD-Rabin-transform.** To obtain the correctness of the ACD-HD-Rabin-transform, we follow the same steps as in the proof of the correctness of the ZT-HD-Rabin-automaton (Proposition 4.48).

**PROPOSITION 5.28 (Correctness of the ACD-HD-Rabin-transform).** Let $\mathcal{T}_S$ be a (labelled) Muller TS and let $\text{ACD}_{\text{Rabin}}(\mathcal{T}_S)$ be its ACD-HD-Rabin-transform. There is an HD mapping of (labelled) transition systems $\varphi: \text{ACD}_{\text{Rabin}}(\mathcal{T}_S) \to \mathcal{T}_S$.

The proof of the next two lemmas are completely analogous to those of Lemmas 4.49 and 4.50.

**LEMMA 5.29.** Let $u = n_0 n_1 n_2 \cdots \in \text{Nodes}(\mathcal{ACD}_{\mathcal{T}_S})^\omega$ be an infinite sequence of nodes of the ACD of $\mathcal{T}_S$. The word $u$ belongs to $\text{Rabin}(R)$, for $R = \{(G_n, R_n)\}_{n \in \text{Nodes}(\mathcal{ACD}_{\mathcal{T}_S})}$ the Rabin condition of $\text{ACD}_{\text{Rabin}}(\mathcal{T}_S)$, if and only if there is a unique minimal node for the ancestor relation in $\text{Inf}(u)$ and this minimal node is round.

**LEMMA 5.30.** There exists a morphism of transition systems $\varphi: \text{ACD}_{\text{parity}}(\mathcal{T}_S) \to \text{ACD}_{\text{Rabin}}(\mathcal{T}_S)$.

Using these lemmas we can prove Proposition 5.28.
**PROOF OF PROPOSITION 5.28.** We define the mapping $\varphi: ACD_{\text{Rabin}}(\mathcal{TS}) \to \mathcal{TS}$ in the natural way: $\varphi_V(v, x) = v$ and $\varphi_E(e, l) = e$. It is immediate to check that $\varphi$ is a weak morphism. The fact that $\varphi$ preserves accepting runs can be proven analogously to the fact that $\mathcal{L}(\mathcal{A}_{\mathcal{Z}_{\mathcal{F}}^{\text{Rabin}}}) \subseteq \text{Muller}_{\Sigma}(\mathcal{F})$ in Proposition 4.48 (by using Lemma 5.29).

Definition of a sound resolver for $\varphi$: In order to show how to simulate runs of $\mathcal{TS}$ in $\text{ACD}_{\text{Rabin}}(\mathcal{TS})$, we use the fact that we can see $\text{ACD}_{\text{Rabin}}(\mathcal{TS})$ as a quotient of $\text{ACD}_{\text{parity}}(\mathcal{TS})$ (Lemma 5.30). Let $\tilde{\varphi}: \text{ACD}_{\text{parity}}(\mathcal{TS}) \to \mathcal{TS}$ be the locally bijective morphism given by Proposition 5.19, and let $\hat{\varphi}: \text{ACD}_{\text{parity}}(\mathcal{TS}) \to \text{ACD}_{\text{Rabin}}(\mathcal{TS})$ be the morphism given by Lemma 5.30. Since $\tilde{\varphi}$ is locally bijective, $\tilde{\varphi}_{\text{Runs}}$ is a bijection between the runs of the transitions systems $\text{ACD}_{\text{parity}}(\mathcal{TS})$ and $\mathcal{TS}$, admitting an inverse $\tilde{\varphi}_{\text{Runs}}^{-1}$. Composing this mapping with $\hat{\varphi}$, we obtain a way to simulate the runs from $\mathcal{TS}$ in $\text{ACD}_{\text{Rabin}}(\mathcal{TS})$:

$$ \hat{\varphi}_{\text{Runs}} \circ \tilde{\varphi}_{\text{Runs}}^{-1} : \text{Run}^{\infty}(\mathcal{TS}) \to \text{Run}^{\infty}(\text{ACD}_{\text{Rabin}}(\mathcal{TS})). $$

This composition of mappings provides a sound resolver simulating $\varphi$. Formally, let $(r_{\text{Init}}, r)$ be the resolver defined as follows. The choice of initial vertices $r_{\text{Init}}: I \to I'$ is given by $r_{\text{Init}}(v_0, x) = v_0$. The function $r: E'^* \times E \to E'$ associates to a finite run $\rho \in E'^*$ and $e \in E$ the last edge of the run $\hat{\varphi}(\tilde{\varphi}^{-1}(\varphi(\rho)e))$ (subscripts have been omitted for legibility). It is easy to check that $(r_{\text{Init}}, r)$ indeed defines a resolver simulating $\varphi$. Its soundness follows from the fact that $\tilde{\varphi}$ and $\hat{\varphi}$ preserve the acceptance of runs. ■

From Proposition 3.16 we obtain:

**COROLLARY 5.31.** Let $\mathcal{A}$ be a Muller automaton and let $\text{ACD}_{\text{Rabin}}(\mathcal{A})$ be its ACD-HD-Rabin-transform. Then, $\mathcal{L}(\text{ACD}_{\text{Rabin}}(\mathcal{A})) = \mathcal{L}(\mathcal{A})$. Moreover, $\text{ACD}_{\text{Rabin}}(\mathcal{A})$ is history-deterministic if and only if $\mathcal{A}$ is history-deterministic.

**ACD-HD-Rabin-transform-for-games.** In Section 2.1, we discussed some technical difficulties appearing when we wanted to define the composition of a game $\mathcal{G}$ and an HD automaton: as the output of such operation, we would like to obtain a game in which Eve always chooses the transitions taken in the automaton, even if it is Adam who makes a move in the game, which is not the case if $\mathcal{G}$ is an arbitrary game. Also, in Section 3.3 we had to introduce HD-for-games mappings in order to formalise correct transformations of games. A similar difficulty appears in the context of the ACD-HD-Rabin-transform; we can see the ACD-HD-Rabin-transform of a game $\mathcal{G}$ as a game in which, at each moment, first, a move takes place in $\mathcal{G}$, and then a choice is made to update the current node in $\mathcal{ACD}_{\mathcal{G}}$. With the current definition of $\text{ACD}_{\text{Rabin}}(\mathcal{G})$, it is the player who makes the move in the game component who chooses how to update the node in $\mathcal{ACD}_{\mathcal{G}}$. This is potentially a problem, as in order to obtain an equivalent game we would like that Eve had full control to decide how to update the nodes in $\mathcal{ACD}_{\mathcal{G}}$, even when it was Adam who moved in the game component (we note that in Proposition 5.28 we did not claim that
there is an HD-for-games mapping $\varphi: \text{ACD}_{\text{Rabin}}(\mathcal{T}\mathcal{S}) \to \mathcal{T}\mathcal{S})$. In order to obtain a transformation working for games, we need to slightly modify the definition of the ACD-HD-Rabin-transform.

For a Muller game $\mathcal{G}$ suitable for transformations, we define its ACD-HD-Rabin-transform-for-games, written $\text{ACD}_{\text{parity}}^{\text{game}}(\mathcal{G})$. The idea is simply to take from Adam the power to update the $\mathcal{A}\mathcal{C}\mathcal{D}_{\mathcal{G}}$-component of vertices. The update of this information is delayed of one transition, so it is Eve who makes the choice of how to move in the ACD. To do this, we need to introduce some additional vertices controlled by Eve. The formal details of this construction and the proof of correctness can be found in Appendix B.

**PROPOSITION 5.32 (Correctness of the ACD-HD-Rabin-transform-for-games).** Let $\mathcal{G}$ be a Muller game suitable for transformations, and let $\text{ACD}_{\text{parity}}^{\text{game}}(\mathcal{G})$ be its ACD-HD-Rabin-transform-for-games. Then, there is an HD-for-games mapping $\varphi: \text{ACD}_{\text{parity}}^{\text{game}}(\mathcal{G}) \to \mathcal{T}\mathcal{S}$.

**COROLLARY 5.33.** Let $\mathcal{G}$ be a Muller game suitable for transformations, and let $\text{ACD}_{\text{parity}}^{\text{game}}(\mathcal{G})$ be its ACD-HD-Rabin-transform-for-games. Then, Eve's full winning region in $\mathcal{G}$ is the projection of her full winning region in $\text{ACD}_{\text{parity}}^{\text{game}}(\mathcal{G})$.

## 5.4 Optimality of the ACD-transforms

We now state and prove the optimality of both the ACD-parity-transform (Theorems 5.34 and 5.35) and the ACD-HD-Rabin-transform (Theorem 5.36). The proofs of these results will use the optimality of the automata based on the Zielonka tree (c.f. Section 4) as a black-box, which will allow us to prove the optimality of both transformations at the same time. The key idea is that if $\varphi: \mathcal{T}\mathcal{S} \to \mathcal{T}\mathcal{S}'$ is an HD mapping, we can see $\mathcal{T}\mathcal{S}$ as an HD automaton recognising the accepting runs of $\mathcal{T}\mathcal{S}'$. We can then use local Muller conditions at vertices of $\mathcal{T}\mathcal{S}'$ to reduce the problem to automata recognising Muller languages.

### 5.4.1 Statement of the optimality results

We state the optimality of the transformations based on the ACD. All the results below apply to labelled transition systems too. For technical reasons, we need to suppose that all the states of transition systems under consideration are accessible, an hypothesis that can always be made without loss of generality. We recall that HD mappings are in particular locally bijective morphisms and HD-for-games mappings (c.f. Figure 7).

**THEOREM 5.34.** Let $\mathcal{T}\mathcal{S}$ be a Muller TS whose states are accessible and let $\overline{\mathcal{T}\mathcal{S}}$ be a parity TS. If $\overline{\mathcal{T}\mathcal{S}}$ admits an HD mapping $\varphi: \overline{\mathcal{T}\mathcal{S}} \to \mathcal{T}\mathcal{S}$, then, its acceptance condition uses at least as many colours as that of $\text{ACD}_{\text{parity}}(\mathcal{T}\mathcal{S})$.

**THEOREM 5.35.** Let $\mathcal{T}\mathcal{S}$ be a Muller TS whose states are accessible and let $\overline{\mathcal{T}\mathcal{S}}$ be a parity TS. If $\overline{\mathcal{T}\mathcal{S}}$ admits an HD mapping $\varphi: \overline{\mathcal{T}\mathcal{S}} \to \mathcal{T}\mathcal{S}$, then, $|\text{ACD}_{\text{parity}}(\mathcal{T}\mathcal{S})| \le |\overline{\mathcal{T}\mathcal{S}}|$.
**THEOREM 5.36.** Let $\mathcal{T}\mathcal{S}$ be a Muller TS whose states are accessible and let $\tilde{\mathcal{T}}\mathcal{S}$ be a Rabin TS. If $\tilde{\mathcal{T}}\mathcal{S}$ admits an HD mapping $\varphi: \tilde{\mathcal{T}}\mathcal{S} \to \mathcal{T}\mathcal{S}$, then, $|\mathrm{ACD}_{\mathrm{Rabin}}(\mathcal{T}\mathcal{S})| \le |\tilde{\mathcal{T}}\mathcal{S}|$.

We obtain an analogous optimality result for the ACD-HD-Rabin-transform-for-games. In this case, the bound is not tight due to the additional vertices that are added to $\mathrm{ACD}_{\mathrm{parity}}^{\mathrm{game}}(G)$ (see Appendix B for details).

**COROLLARY 5.37.** Let $G$ be a Muller game suitable for transformations whose states are accessible and let $\tilde{G}$ be a Rabin game. If $\tilde{G}$ admits an HD-for-games mapping $\varphi: \tilde{G} \to G$, then, $|\mathrm{ACD}_{\mathrm{parity}}^{\mathrm{game}}(G)| \le 2|\tilde{G}|$.

## 5.4.2 Discussion: Limits on the applicability of HD automata and preservation of minimality

Before presenting the proofs of the optimality theorems, we discuss some consequences and limitations of our results.

**Difficulty of finding succinct history-deterministic automata.** As mentioned in the introduction, several years had to pass after the introduction of history-deterministic automata [44] before finding HD automata that were actually smaller than equivalent deterministic ones [57]. As of today, we only know a handful of examples of $\omega$-regular languages admitting succinct HD automata [1, 57, 24], and their applicability in practice has yet to be fully determined. We assert that we can derive from our results some enlightening explanations on the difficulty of finding succinct HD parity automata, and set some limits in their usefulness in practical scenarios such as LTL synthesis.

First, Corollary 4.16 already sets the impossibility of the existence of small HD parity automata recognising Muller languages. Corollary 5.39 states that if an HD parity automaton $\mathcal{A}$ has been obtained as a transformation of a DMA $\mathcal{B}$, then $\mathcal{A}$ is not strictly smaller than a minimal deterministic parity automaton for $\mathcal{L}(\mathcal{A})$.

**COROLLARY 5.38.** Let $\mathcal{T}\mathcal{S}$ be a Muller TS. A minimal parity TS admitting an HD mapping to $\mathcal{T}\mathcal{S}$ has the same size than a minimal parity TS admitting a locally bijective morphism to $\mathcal{T}\mathcal{S}$.

**COROLLARY 5.39.** Let $\mathcal{A}$ be a history-deterministic parity automaton. Assume that there exists a DMA $\mathcal{B}$ such that $\mathcal{A}$ admits an HD mapping to $\mathcal{B}$. Then, there exists a DPA $\mathcal{A}'$ recognising $\mathcal{L}(\mathcal{A})$ such that $|\mathcal{A}'| \le |\mathcal{A}|$.

Both corollaries follow from an immediate application of Theorem 5.35.

**The ACD-transform does not preserve minimality.** A natural question is whether the ACD-parity-transform preserves minimality of automata, that is, given a DMA $\mathcal{A}$ with a min-
imal number of states for the language it recognises, is ACD<sub>parity</sub>(A) minimal amongst DPAs recognising L(A)?<sup>11</sup> The answer to this question is negative, as we show now.

**PROPOSITION 5.40.** There exists a DMA A that is minimal amongst DMAs recognising L(A), but such that its ACD-parity-transform ACD<sub>parity</sub>(A) is not a minimal DPA.

We consider the alphabet Σ = {a, b, c} and the language

$$L = \{w \in \Sigma^\omega \mid c \in \mathrm{Inf}(w) \text{ and } w \text{ contains infinitely often the factor } ab\}.$$

A minimal DMA for L is depicted in Figure 18a. Its minimality follows simply from the fact that, as L is not a Muller language ((abc)<sup>ω</sup> ∈ L but (bac)<sup>ω</sup> ∉ L, c.f. Remark 2.10), a DMA with just one state cannot recognise L. In Figure 18 we show its alternating cycle decomposition and its ACD-parity-transform that has 4 states. However, we can find a DPA with just 3 states recognising L, as shown in Figure 18d.

<figure><img src="image_33.png" /><figcaption>(a) A Muller automaton with acceptance set given by F = {{α, β, λ}}.</figcaption></figure>

<figure><img src="image_34.png" /><figcaption>(b) Alternating cycle decomposition of A. To indicate the labels of the nodes of this ACD, we include just the colours of the corresponding edges.</figcaption></figure>

<figure><img src="image_35.png" /><figcaption>(c) ACD-parity-transform of A, ACD<sub>parity</sub>(A), with 4 states.</figcaption></figure>

<figure><img src="image_36.png" /><figcaption>(d) A parity automaton recognising L with only 3 states.</figcaption></figure>

<caption>**Figure 18.** A minimal DMA whose ACD-parity-transform is not a minimal DPA.</caption>

<footnote n="11">11 This question was left open as a conjecture in the conference version of this paper [23].</footnote>
### 5.4.3 Optimality of the parity condition of ACD<sub>parity</sub>(TS)

We show next the proof of Theorem 5.34. To prove this result, we would like to use the Flower Lemma 2.16, however, the statement of Theorem 5.34 does not involve $\omega$-regular languages. In order to set up a context in which apply the Flower Lemma, we show that, whenever we have a morphism $\varphi: \mathcal{TS} \to \mathcal{TS}'$, $\mathcal{TS}$ can be seen as an automaton reading the runs of $\mathcal{TS}'$.

Let $\mathcal{TS} = (G, \text{Acc})$ and $\mathcal{TS}' = (G', \text{Acc}')$ be transition systems with underlying graphs $G = (V, E, \text{Source}, \text{Target}, I)$ and $G' = (V', E', \text{Source}', \text{Target}', I')$, and acceptance conditions $\text{Acc} = (\gamma, \Gamma, \mathcal{W})$ and $\text{Acc}' = (\gamma', \Gamma', \mathcal{W}')$. A weak morphism of transition systems $\varphi: \mathcal{TS} \to \mathcal{TS}'$ provides a labelling of the edges of $\mathcal{TS}$ by $\varphi_E: E \to E'$. Therefore, we can see $\mathcal{TS}$ as an automaton with input alphabet $E'$, inheriting the underlying graph and acceptance condition from $\mathcal{TS}$. We say that this is the automaton of morphism $\varphi$ and denote it by $\mathcal{A}_{\varphi}$.

We define the language of accepting runs of a transition system $\mathcal{TS}$ as:

$$ \mathcal{L}_{\mathcal{Runs}}(\mathcal{TS}) = \{\rho \in E^{\omega} \mid \rho \text{ is an accepting run in } \mathcal{TS}\}. $$

**LEMMA 5.41.** Let $\mathcal{TS}$ and $\mathcal{TS}'$ be transition systems with a single initial state, let $\varphi: \mathcal{TS} \to \mathcal{TS}'$ be a weak morphism of transition systems, and let $\mathcal{A}_{\varphi}$ be its automaton. Then, $\varphi$ is an HD mapping if and only if the automaton $\mathcal{A}_{\varphi}$ is history-deterministic, and, in this case,

$$ \mathcal{L}(\mathcal{A}_{\varphi}) = \mathcal{L}_{\mathcal{Runs}}(\mathcal{TS}') $$

**PROOF.** We first note that a resolver for $\mathcal{A}_{\varphi}$ (in the sense of HD automata) is a mapping of the form $r: E^* \times E' \to E$, as $E'$ is the input alphabet of this automaton. A resolver simulating $\varphi$ (in the sense of HD mappings) is a mapping of the same form. It is straightforward to check that $(q_0, r)$ is a sound resolver for $\mathcal{A}_{\varphi}$ if and only if $(r_{\text{Init}}, r)$ is a sound resolver simulating $\varphi$ (where $r_{\text{Init}}(q'_0) = q_0$ is the only possible choice of initial vertex).

We prove that $\mathcal{L}(\mathcal{A}_{\varphi}) = \{\rho' \in \mathcal{Run}(\mathcal{TS}') \mid \rho' \text{ is an accepting run}\}$. First, we remark that if $\rho$ is a run in $\mathcal{A}_{\varphi}$ over $\rho' \in \mathcal{Run}(\mathcal{TS}')$, then $\rho' = \varphi_{\mathcal{Runs}}(\rho)$, since the labelling of $\mathcal{A}_{\varphi}$ by input letters is given exactly by $\varphi$ itself. Therefore, if $\rho' \in \mathcal{L}(\mathcal{A}_{\varphi})$, there exists an accepting run $\rho$ over $\rho'$, and since $\varphi$ preserves accepting runs, $\rho' = \varphi_{\mathcal{Runs}}(\rho)$ is accepting in $\mathcal{TS}'$, proving the inclusion from left to right. For the other inclusion, we let $(r_{\text{Init}}, r)$ be a sound resolver simulating $\varphi$. If $\rho'$ is an accepting run in $\mathcal{TS}'$, then $r_{\mathcal{Runs}}(\rho')$ is an accepting run over $\rho'$ in $\mathcal{A}_{\varphi}$. ■

We recall that $[\min_{\mathcal{TS}}, \max_{\mathcal{TS}}]$ are the colours used by the ACD-parity-transform of $\mathcal{TS}$, which coincides with the maximal height of a tree in $\mathcal{ACD}_{\mathcal{TS}}$. We also recall that $\min_{\mathcal{TS}} = 0$ if $\mathcal{ACD}_{\mathcal{TS}}$ is positive or equidistant, and that $\min_{\mathcal{TS}} = 1$ if $\mathcal{ACD}_{\mathcal{TS}}$ is negative.

**LEMMA 5.42.** Let $\mathcal{TS}$ be a Muller TS, and let AltTree($\ell$) $\in \mathcal{ACD}_{\mathcal{TS}}$ be a positive (resp. negative) tree of the ACD of $\mathcal{TS}$ of height $d$. Then, $\mathcal{TS}$ admits a positive (resp. negative) d-flower.
**PROOF.** We use the same argument as the one used in the proof of Theorem 4.14. Let $n_1 \le n_2 \le \dots \le n_d$ be a branch of length $d$ of AltTree($\ell$) (where $n_1$ is the root and $n_d$ is a leaf of the tree). Let $v \in v_{\text{States}}(n_d)$ be a vertex appearing in the leaf. Then, the whole branch is contained in $\mathcal{T}_v$ (by Remark 5.4), that is, $v(n_i) \in \text{Cycles}_{\mathcal{T}_S}(v)$. Moreover, $v(n_1) \supseteq v(n_2) \supseteq \dots \supseteq v(n_d)$ is a chain that alternates accepting and rejecting cycles, so it is a $d$-flower that is positive if and only if $v(n_1) = \ell$ is an accepting cycle, that is, if AltTree($\ell$) is positive. ■

**LEMMA 5.43.** Let $\mathcal{T}_S$ be a Muller TS with a single initial vertex and whose vertices are all accessible. Then, the parity index of $\mathcal{L}_{\mathcal{R}uns}(\mathcal{T}_S)$ is:

- $[\min_{\mathcal{T}_S}, \max_{\mathcal{T}_S}]$ if $\mathcal{ACD}_{\mathcal{T}_S}$ is positive or negative,

- Weak$_{\max_{\mathcal{T}_S}}$ if $\mathcal{ACD}_{\mathcal{T}_S}$ is equidistant.

**PROOF.** We consider the identity morphism $\text{Id}_{\mathcal{T}_S} : \mathcal{T}_S \to \mathcal{T}_S$ and its automaton $\mathcal{A}_{\text{Id}_{\mathcal{T}_S}}$, which is a deterministic automaton trivially recognising $\mathcal{L}_{\mathcal{R}uns}(\mathcal{T}_S)$ (that is, we see $\mathcal{T}_S$ as an automaton reading its own edges as input letters). The result follows from the Flower Lemma 2.16 and the fact that a tree AltTree($\ell$) $\in \mathcal{ACD}_{\mathcal{T}_S}$ of height $d$ provides a $d$-flower that is positive if $\ell$ is accepting and negative if $\ell$ is rejecting (Lemma 5.42). These flowers are accessible as we have supposed that all the vertices of $\mathcal{T}_S$ are accessible. ■

The previous lemmas allow us to obtain Theorem 5.34 for transition systems with a single initial vertex. We introduce some further notations to deal with the general case.

For a Muller TS $\mathcal{T}_S$ and a vertex $v$, we let $\mathcal{ACD}_{(\mathcal{T}_S, v)}$ be the alternating cycle decomposition of the accessible part of $\mathcal{T}_S$ from $v$. We note that the trees of $\mathcal{ACD}_{(\mathcal{T}_S, v)}$ are a subset of the trees of $\mathcal{ACD}_{\mathcal{T}_S}$: a tree AltTree($\ell_i$) $\in \mathcal{ACD}_{\mathcal{T}_S}$ appears in $\mathcal{ACD}_{(\mathcal{T}_S, v)}$ if and only if the cycle $\ell_i$ is accessible from $v$. Accordingly, for each vertex $v$ of $\mathcal{T}_S$ we let $\min_{(\mathcal{T}_S, v)}$ (resp. $\max_{(\mathcal{T}_S, v)}$) be the minimum (resp. maximum) value taken by the function $p_{\mathcal{ACD}}$ when restricted to the trees of $\mathcal{ACD}_{(\mathcal{T}_S, v)}$.

**REMARK 5.44.** For every transition system $\mathcal{T}_S$, one of the two following statements holds:

- There is some vertex $v$ such that $[\min_{\mathcal{T}_S}, \max_{\mathcal{T}_S}] = [\min_{(\mathcal{T}_S, v)}, \max_{(\mathcal{T}_S, v)}]$.

- There are two vertices $v_0$ and $v_1$ such that $\min_{(\mathcal{T}_S, v_0)} = 0$, $\max_{(\mathcal{T}_S, v_0)} = \max_{\mathcal{T}_S} - 1$ and $\min_{(\mathcal{T}_S, v_1)} = 1$, $\max_{(\mathcal{T}_S, v_1)} = \max_{\mathcal{T}_S}$.

Moreover, if all the states of $\mathcal{T}_S$ are accessible, we can choose $v$ (resp. $v_0$ and $v_1$) to be an initial vertex.

We can finally deduce Theorem 5.34 from the preceding lemmas.

**PROOF OF THEOREM 5.34.** We assume that we are in the first case of Remark 5.44 (a proof for the second case follows easily). First, we show that we can suppose that $\overline{\mathcal{T}_S}$ and $\mathcal{T}_S$ have a single initial vertex. Let $v$ be an initial vertex of $\mathcal{T}_S$ such that $[\min_{\mathcal{T}_S}, \max_{\mathcal{T}_S}] =$
$[\min_{(\mathcal{T}_S, v)}, \max_{(\mathcal{T}_S, v)}]$. Let $\varphi: \overline{\mathcal{T}S} \to \mathcal{T}S$ be an HD mapping, and let $(r_{\text{Init}}, r)$ be a sound resolver simulating it. We let $\tilde{v} = r_{\text{Init}}(v)$ be the initial vertex in $\overline{\mathcal{T}S}$ chosen by the resolver. It suffices then to prove the result for the accessible part of $\overline{\mathcal{T}S}$ from $\tilde{v}$, the transition system $\mathcal{T}S_v$, and the restriction of $\varphi$ to these transition systems.

From now on, we assume that both $\overline{\mathcal{T}S}$ and $\mathcal{T}S$ have a single initial vertex. By Lemma 5.43 and Proposition 2.15, a parity history-deterministic automaton recognising $L_{\mathcal{R}uns}(\overline{\mathcal{T}S})$ uses at least $|[\min_{\mathcal{T}S}, \max_{\mathcal{T}S}]|$ colours. By Lemma 5.41, the automaton $A_\varphi$ of the morphism $\varphi$ is a parity history-deterministic automaton recognising $L_{\mathcal{R}uns}(\mathcal{T}S)$, and therefore uses at least $|[\min_{\mathcal{T}S}, \max_{\mathcal{T}S}]|$ colours. Since the acceptance condition of $\overline{\mathcal{T}S}$ is exactly the same as that of $A_\varphi$, we can conclude. ■

### 5.4.4 Optimality of the sizes of ACD<sub>parity</sub>(*TS*) and ACD<sub>Rabin</sub>(*TS*)

We prove now Theorems 5.35 and 5.36.

**SKETCH OF THE PROOF.** Let $\varphi: \overline{\mathcal{T}S} \to \mathcal{T}S$ be an HD mapping, and let $v$ be a vertex in $\mathcal{T}S$. We can see the set $\varphi^{-1}(v)$ as the states of an HD automaton reading finite runs in $\mathcal{T}S$ looping around $v$. This allows to define an HD automaton having $\varphi^{-1}(v)$ as set of states and recognising LocalMuller<sub>TS</sub>(v). As the Zielonka tree of LocalMuller<sub>TS</sub>(v) is the tree $\mathcal{T}_v$, by optimality of the ZT-parity-automaton (resp. the ZT-HD-Rabin-automaton), we deduce that $|\varphi^{-1}(v)| \ge |\text{Leaves}(\mathcal{T}_v)|$ (resp. $|\varphi^{-1}(v)| \ge \text{rbw}(\mathcal{T}_v)$). ■

**DEFINITION 5.45.** Let $\mathcal{T}S$ and $\mathcal{T}S'$ be two transition systems, and let $(\gamma, \Gamma, \text{Muller}_\Gamma(\mathcal{F}))$ be the acceptance condition of $\mathcal{T}S$. Let $\varphi: \mathcal{T}S \to \mathcal{T}S'$ be a weak morphism of transition systems that is locally surjective, and let $v'$ be an accessible recurrent state of $\mathcal{T}S'$. For each $\ell' \in \text{Cycles}_{v'}(\mathcal{T}S')$ we let $\rho_{\ell'}$ be a finite path starting and ending in $v'$ visiting exactly the edges of $\ell'$. We define the *cycle-preimage-automaton at* $v'$ to be the Muller automaton $A_{(\varphi^{-1}, v')} = (Q_{v'}, \text{Cycles}_{v'}(\mathcal{T}S'), Q_v, 2_+, \delta, \text{Muller}_{2_+}(\tilde{F}))$ over the input alphabet $\text{Cycles}_{\mathcal{T}S'}(v')$ defined as:

- the set of states is $Q_{v'} = \varphi^{-1}(v')$,

- all the states are initial,

- the output colours are non-empty subsets of the colours used by $\mathcal{T}S$,

- $(q_2, C) \in \delta(q_1, \ell')$ if there is a finite path $\rho \in \text{Path}^{\text{fin}}_{q_1}(\mathcal{T}S)$ from $q_1$ to $q_2$ such that $\varphi(\rho) = \rho_{\ell'}$ producing as output the colours in $C \subseteq \Gamma$, that is $\gamma(\rho) = C$. If $C$ is empty, this corresponds to an uncoloured edge $q_1 \xrightarrow{\ell' : \varepsilon} q_2$. We remark that, since $\varphi$ is assumed locally surjective, there is at least one such path $\rho$.

- $\{C_1, \dots, C_k\} \in \tilde{F}$ if and only if $\bigcup_{i=1}^k C_i \in \mathcal{F}$.

We remark that a transition $e = q_1 \xrightarrow{\ell' : C} q_2$ in $A_{(\varphi^{-1}, v')}$ induces a finite path $\text{Unfold}(e) = q_1 \stackrel{C}{\rightsquigarrow} q_2$ in $\mathcal{T}S$ called the *unfolding* of $e$, producing as output the set of colours $C$ and such
that $\varphi(\text{Unfold}(e)) = \ell'$. In particular, a run $\rho$ in $\mathcal{A}_{(\varphi^{-1}, v')}$ is accepting if and only if $\text{Unfold}(\rho)$ is accepting.

**LEMMA 5.46.** If $L = \text{Muller}_\Gamma(\mathcal{F})$ is a parity (resp. Rabin) language, then, so is the language $\tilde{L} = \text{Muller}_{2_+^\Gamma}(\tilde{\mathcal{F}})$ used by the acceptance condition of $\mathcal{A}_{(\varphi^{-1}, v')}$. ■

**PROOF.** Assume that $L$ is a parity language, that is, there are $d_{\min} \le d_{\max}$ and $\varphi: \Gamma \to [d_{\min}, d_{\max}]$ such that for any non-empty subset $C \subseteq \Gamma$, $C \in \mathcal{F}$ if and only if $\min \varphi(C)$ is even. We define $\tilde{\varphi}: 2_+^\Gamma \to [d_{\min}, d_{\max}]$ as: $\tilde{\varphi}(C) = \min \varphi(C)$. It is immediate to see that $\{C_1, \dots, C_k\} \in \tilde{\mathcal{F}}$ if and only if $\min \tilde{\varphi}(\{C_1, \dots, C_k\})$ is even.

Assume now that $L$ is a Rabin language represented by the Rabin pairs $\{(G_1, R_1), \dots, (G_r, R_r)\}$. We define a family of Rabin pairs $\tilde{R} = \{(\tilde{G}_1, \tilde{R}_1), \dots, (\tilde{G}_r, \tilde{R}_r)\}$ for $\tilde{L}$ as: $\{C_1, \dots, C_k\} \in \tilde{G}_i$ (resp. $\in \tilde{R}_i$) if $\cup_{i=1}^k C_i \in G_i$ (resp. $\in \tilde{R}_i$). It is immediate to see that $\tilde{L} = \text{Rabin}_{2_+^\Gamma}(\tilde{R})$. ■

**LEMMA 5.47.** Let $\mathcal{TS}$ and $\mathcal{TS}'$ be two Muller $\mathcal{TS}$, $\varphi: \mathcal{TS} \to \mathcal{TS}'$ a weak morphism of $\mathcal{TS}$, and $v'$ an accessible recurrent state of $\mathcal{TS}'$. If $\varphi$ is an HD mapping, then the automaton $\mathcal{A}_{(\varphi^{-1}, v')}$ is history-deterministic and recognises the local Muller condition of $\mathcal{TS}'$ at $v'$. ■

**PROOF.** $\mathcal{L}(\mathcal{A}_{(\varphi^{-1}, v')}) \subseteq \text{LocalMuller}_{v'}(\mathcal{TS})$: Let $\ell'_1 \ell'_2 \dots \in \text{Cycles}_{v'}(\mathcal{TS})^\omega$ be a sequence of cycles accepted by $\mathcal{A}_{(\varphi^{-1}, v')}$. By prefix-independence of Muller languages we can assume that all the cycles $\ell'_i$ appear infinitely often. Let $\rho = q_0 \xrightarrow{\ell'_1:C_1} q_1 \xrightarrow{\ell'_2} q_2 \to \dots$ be an accepting run in $\mathcal{A}_{(\varphi^{-1}, v')}$ over $\ell'_1 \ell'_2 \dots$, and let $\text{Unfold}(\rho)$ be its unfolding. As $\rho$ is an accepting run, so is $\text{Unfold}(\rho)$, and since $\varphi$ preserves accepting runs, $\varphi(\text{Unfold}(\rho))$ is an accepting run in $\mathcal{TS}'$. The edges visited by $\varphi(\text{Unfold}(\rho))$ form the cycle $\cup_{i \ge 1} \ell'_i$, which is therefore an accepting cycle, so $\ell'_1 \ell'_2 \dots \in \text{LocalMuller}_{v'}(\mathcal{TS})$ by definition of local Muller condition.

LocalMuller$_{\mathcal{TS}'}(v') \subseteq \mathcal{L}(\mathcal{A}_{(\varphi^{-1}, v')})$ and history-determinism: Let $r_\varphi: E^* \times E' \to E$ be a sound resolver simulating $\varphi$. We will transfer the strategy given by $r_\varphi$ to define a resolver $r_\mathcal{A}: \Delta^* \times \text{Cycles}_{v'}(\mathcal{TS}') \to \Delta$ for $\mathcal{A}_{(\varphi^{-1}, v')}$, where $\Delta$ is the set of transitions of the automaton. Let $\rho'_0 \in \mathcal{R}un^{\text{fin}}(\mathcal{TS}')$ be a finite run reaching $v'$, and let $\rho_0 = r_{\varphi, \mathcal{R}uns}(\rho'_0)$ the preimage given by the resolver, ending in some $q_0 \in Q_{v'}$ that is going to be used as initial state for $\mathcal{A}_{(\varphi^{-1}, v')}$. For a sequence $e_1 e_2 \dots e_k \in \Delta^*$ and $\ell' \in \text{Cycles}_{v'}(\mathcal{TS}')$, we let

$$r_{\mathcal{A}}(e_1 e_2 \dots e_k, \ell') = r_{\varphi}(\rho'_0 \rho'_1 \dots \rho'_k, \rho_{\ell'}), \quad 12$$

where $\rho'_j = \varphi(\text{Unfold}(e_j))$ and $v' \xrightarrow{\rho_{\ell'}} v'$ is the finite run corresponding to $\ell'$ fixed in the definition of $\mathcal{A}_{(\varphi^{-1}, v')}$. By definition, the obtained resolver satisfies the following property:

If $e_1 e_2 \dots \in \Delta^\omega$ is the run induced by $r_\mathcal{A}$ over $\ell'_1 \ell'_2 \dots \in \text{Cycles}_{v'}(\mathcal{TS}')^\omega$, then $\rho_0 \text{Unfold}(e_1 e_2 \dots) = r_{\varphi, \mathcal{R}uns}(\rho'_0 \rho'_1 \rho'_2 \dots)$.

<footnote n="12">12 Here we use a slight abuse of notation, since, formally, $r_\varphi$ takes as input elements in $E^* \times E'$, but $\rho_{\ell'} \in E'^*$. We can naturally extend $r_\varphi$ to $E'^*$ by induction. Equivalently, we can say that $r_{\varphi, \mathcal{R}uns}(e_1 e_2 \dots e_k, \ell')$ is a suffix of $r_{\varphi, \mathcal{R}uns}(\rho'_0 \rho'_1 \dots \rho'_k \rho_{\ell'})$.</footnote>
This gives us:

$\bigcup \text{Inf}(\ell'_1, \ell'_2, \dots)$ is accepting cycle in $\mathcal{T}S' \iff \rho'_0 \rho'_1 \rho'_2 \dots$ is accepting run in $\mathcal{T}S' \Rightarrow \rho_0 \text{Unfold}(e_1 e_2 \dots)$ accepting run in $\mathcal{T}S \iff e_1 e_2 \dots$ accepting run in $\mathcal{A}_{(\varphi^{-1}, \nu')}.$

Which allows us to conclude that the $\mathcal{A}_{(\varphi^{-1}, \nu')}$ recognises $\text{LocalMuller}_{\nu'}(\mathcal{T}S)$ and that $r_{\mathcal{A}}$ is a sound resolver. ■

**COROLLARY 5.48.** Let $\mathcal{T}S$ and $\widetilde{\mathcal{T}S}$ be a Muller and a parity transition system, respectively, and let $\varphi: \widetilde{\mathcal{T}S} \to \mathcal{T}S$ be an HD mapping. Let $\nu$ be an accessible recurrent state of $\mathcal{T}S$. Then,

$$|\varphi^{-1}(\nu)| \ge |\text{Leaves}(\mathcal{Z}_{\text{LocalMuller}_{\mathcal{T}S}(\nu)})| = |\text{Leaves}(\mathcal{T}_{\nu})|.$$

**PROOF.** By Lemma 5.47, the automaton $\mathcal{A}_{(\varphi^{-1}, \nu)}$ is a history-deterministic automaton recognising $\text{LocalMuller}_{\nu}(\mathcal{T}S)$ of size $|\varphi^{-1}(\nu)|$, and by Lemma 5.46, it is a parity automaton. The optimality of the ZT-parity-automaton (Theorem 4.15) gives us the first inequality. The second equality follows from the fact that $\mathcal{T}_{\nu}$ is the Zielonka tree of $\text{LocalMuller}_{\mathcal{T}S}(\nu)$ (Lemma 5.9). ■

The next corollary admits an identical proof, using the optimality of the ZT-HD-Rabin-automaton (Theorem 4.51).

**COROLLARY 5.49.** Let $\mathcal{T}S$ and $\widetilde{\mathcal{T}S}$ be a Muller and a Rabin transition system, respectively, and let $\varphi: \widetilde{\mathcal{T}S} \to \mathcal{T}S$ be an HD mapping. Let $\nu$ be an accessible recurrent state of $\mathcal{T}S$. Then,

$$|\varphi^{-1}(\nu)| \ge |\text{rbw}(\mathcal{Z}_{\text{LocalMuller}_{\mathcal{T}S}(\nu)})| = |\text{rbw}(\mathcal{T}_{\nu})|.$$

Theorems 5.35 and 5.36 follow from these two corollaries, the formulas for the size of the ACD-transforms (Remarks 5.15 and 5.27) and the fact that a locally surjective morphism $\varphi: \widetilde{\mathcal{T}S} \to \mathcal{T}S$ is surjective if all vertices of $\mathcal{T}S$ are accessible (Lemma 3.5).

# 6. Corollaries

In this section, we discuss some further applications of the Zielonka tree and the alternating cycle decomposition. In Section 6.1, we use the insights gained from the ACD to conduct a comprehensive study of typeness results for deterministic Muller automata (that is, when can we relabel a DMA with an equivalent and simpler acceptance condition). In Section 6.2 we present a normal form for parity transition systems and prove the main properties exhibited by TS in this form. In Section 6.3, we provide a polynomial-time algorithm minimising DPA recognising Muller languages.
## 6.1 Typeness results

As we have seen, there are many different types of acceptance conditions for $\omega$-regular automata. An important question is the following:

Question: Given a Muller automaton $\mathcal{A}$, can we define a simpler acceptance condition over the underlying graph of $\mathcal{A}$ obtaining an equivalent automaton $\mathcal{A}'$?

This question was first studied (in the context of automata using state-based acceptance) by Krishnan, Puri and Brayton [55, 56], who showed how to determine if a DMA can be relabelled with an equivalent Büchi condition. Their work was generalised to parity automata by Boker, Kupferman and Steinitz [11], and related questions about typeness were studied for non-deterministic automata by Kupferman, Morgenstern and Murano [59], and for history-deterministic automata by Boker, Kupferman and Skrzypczak [10].

In this section, we provide new general characterisations of typeness for Muller transition systems. The main contributions of this section appear in Propositions 6.9, 6.10 and 6.11, which characterise when a Muller TS can be relabelled with equivalent parity, Rabin, or Streett conditions in terms of properties of the cycles of the TS. For instance, Proposition 6.9 states that a Muller TS can be relabelled with an equivalent Rabin condition if and only if its rejecting cycles are closed under union. The “only if” part of these results was already known [63], but the fact that this is indeed a characterisation is a novel result, for which the use of the ACD is essential. These characterisations directly imply the results from [11, 55, 56]. We also show how to use the ACD to determine the parity index of the language recognised by a DMA (Proposition 6.13), which can be seen as a simplification of the results from [56, Section 3.2]. Further results concerning generalised Büchi languages and weak automata can be found in Appendix A.

### 6.1.1 Typeness for Muller languages

We first present some results proven by Zielonka [94, Section 5] that show how we can use the Zielonka tree to deduce if a Muller language is a Rabin, a Streett or a parity language. These results are generalised to transition systems in the next subsection. A study of further types of Muller languages can be found in Appendix A.

We do not include the proofs of the results of this section in the main body of the paper, as they are known results [94, Section 5] and they are special cases of the proofs in Section 6.1.2. Nevertheless, we include them in Appendix E.

We first introduce some definitions. The terminology will be justified by the upcoming results.

**DEFINITION 6.1.** Let $T$ be a tree with nodes partitioned into round nodes and square nodes. We say that $T$ has:
— *Rabin shape* if every round node has at most one child.

— *Streett shape* if every square node has at most one child.

— *Parity shape* if every node has at most one child.

**PROPOSITION 6.2.** Let $\mathcal{F} \subseteq 2_+^\Gamma$ be a family of non-empty subsets. The following conditions are equivalent:

1. *Muller$_\Gamma(\mathcal{F})$ is a Rabin language.*

2. $2_+^\Gamma \setminus \mathcal{F}$ is closed under union: If $C_1 \notin \mathcal{F}$ and $C_2 \notin \mathcal{F}$, then $C_1 \cup C_2 \notin \mathcal{F}$.

3. $\mathcal{Z}_\mathcal{F}$ has *Rabin shape*.

**PROPOSITION 6.3.** Let $\mathcal{F} \subseteq 2_+^\Gamma$ be a family of non-empty subsets. The following conditions are equivalent:

1. *Muller$_\Gamma(\mathcal{F})$ is a Streett language.*

2. The family $\mathcal{F}$ is closed under union.

3. $\mathcal{Z}_\mathcal{F}$ has *Streett shape*.

**PROPOSITION 6.4.** Let $\mathcal{F} \subseteq 2_+^\Gamma$ be a family of non-empty subsets. The following conditions are equivalent:

1. *Muller$_\Gamma(\mathcal{F})$ is a parity language.*

2. Both $\mathcal{F}$ and $2_+^\Gamma \setminus \mathcal{F}$ are closed under union: If $C_1 \in \mathcal{F} \iff C_2 \in \mathcal{F}$, then, $C_1 \cup C_2 \in \mathcal{F} \iff C_1 \notin \mathcal{F}$.

3. $\mathcal{Z}_\mathcal{F}$ has *parity shape*.

Moreover, if some of these conditions is satisfied, *Muller$_\Gamma(\mathcal{F})$ is a $[\min_\mathcal{F}, \max_\mathcal{F}]$-parity language*.

**COROLLARY 6.5.** A *Muller language* $L \subseteq \Gamma^\omega$ is a *parity language* if and only if it is both a *Rabin* and a *Streett language*.

**6.1.2 Typeness for Muller transition systems and deterministic automata**

We start this subsection by introducing the necessary definitions about equivalence of acceptance conditions and typeness. Then, we state and prove our main contributions concerning typeness of transition systems.

**Equivalence of acceptance conditions and typeness.** Let $\mathcal{T}S_1 = (G, \text{Acc}_1)$ and $\mathcal{T}S_2 = (G, \text{Acc}_2)$ be two transitions systems over the same underlying graph $G$, with acceptance conditions $\text{Acc}_i = (\gamma_i, \Gamma_i, \mathcal{W}_i)$, for $i \in \{1, 2\}$. We say that $\text{Acc}_1$ and $\text{Acc}_2$ are equivalent over $G$, written $\text{Acc}_1 \cong_G \text{Acc}_2$, if for all runs $\rho \in \mathcal{R}un(G)$, $\rho$ is accepting for $\mathcal{T}S_1$ if and only if it is accepting for $\mathcal{T}S_2$; that is, $\gamma_1(\rho) \in \mathcal{W}_1 \iff \gamma_2(\rho) \in \mathcal{W}_2$.
We write $\mathcal{TS}_1 \simeq \mathcal{TS}_2$ if $\mathcal{TS}_1$ and $\mathcal{TS}_2$ are isomorphic. We recall that two transition systems are isomorphic if there is a morphism of transition systems $\varphi: \mathcal{TS}_1 \to \mathcal{TS}_2$ whose inverse is also a morphism, that is, $\varphi$ and $\varphi^{-1}$ preserve the acceptance of runs.

**REMARK 6.6.** If $\varphi: \mathcal{TS}_1 \to \mathcal{TS}_2$ is an isomorphism, then $(\gamma_2 \circ \varphi, \Gamma_2, W_2)$ is an acceptance condition over the underlying graph of $\mathcal{TS}_1$ that is equivalent to $(\gamma_1, \Gamma_1, W_1)$ over this graph.

Conversely, if two acceptance conditions $\mathrm{Acc}_1$ and $\mathrm{Acc}_2$ are equivalent over a same graph $G$, then the identity function is an isomorphism between $\mathcal{TS}_1 = (G, \mathrm{Acc}_1)$ and $\mathcal{TS}_2 = (G, \mathrm{Acc}_2)$.

For *X* one of types of languages defined in Section 2.2 (Büchi, parity, Muller, etc...), we say that a transition system $\mathcal{TS}$ is *X* type if there exists an isomorphic transition system $\mathcal{TS}' \simeq \mathcal{TS}$ using an *X* acceptance condition. We note that, by the previous remark, in that case an *X* acceptance condition can be defined directly over the underlying graph of $\mathcal{TS}$.

We remark that, given a pointed graph $G$ (whose states are accessible), the equivalence classes of Muller acceptance conditions for the relation $\simeq_G$ are given exactly by the mappings $f: \mathcal{Cycles}(G) \to \{\text{Accept, Reject}\}$.

**The ACD determines the type of transition systems.**

**DEFINITION 6.7.** Let $\mathcal{TS}$ be a Muller transition system with a set of states $V$. We say that its alternating cycle decomposition $\mathcal{ACD}_{\mathcal{TS}}$ is a:

- Rabin ACD if for every state $v \in V$, the tree $\mathcal{T}_v$ has Rabin shape.

- Streett ACD if for every state $v \in V$, the tree $\mathcal{T}_v$ has Streett shape.

- Parity ACD if for every state $v \in V$, the tree $\mathcal{T}_v$ has parity shape.

- $[0, d-1]$-parity ACD (resp. $[1, d]$-parity ACD) if it is a parity ACD, trees of $\mathcal{ACD}_{\mathcal{TS}}$ have height at most *d* and trees of height *d* are positive (resp. negative).

**REMARK 6.8.** $\mathcal{ACD}_{\mathcal{TS}}$ is a parity ACD if and only if it is both a Rabin and a Streett ACD.

**PROPOSITION 6.9.** Let $\mathcal{TS} = (G_{\mathcal{TS}}, \mathrm{Acc}_{\mathcal{TS}})$ be a Muller transition system whose states are accessible. The following conditions are equivalent:

1. $\mathcal{TS}$ is Rabin type.

2. For every pair of rejecting cycles $\ell_1, \ell_2 \in \mathcal{Cycles}(\mathcal{TS})$ with some state in common, $\ell_1 \cup \ell_2$ is a rejecting cycle.

3. $\mathcal{ACD}_{\mathcal{TS}}$ is a Rabin ACD.

**PROOF.** (1 $\Rightarrow$ 2) Let $\mathrm{Acc}_R = (\gamma, \Gamma, \mathrm{Rabin}(R))$ be the Rabin acceptance condition equivalent to $\mathrm{Acc}_{\mathcal{TS}}$, and let $R = (G_1, R_1), \dots, (G_r, R_r)$ be its Rabin pairs. Let $\ell_1$ and $\ell_2$ be two cycles with a state in common, and suppose that $\ell_1 \cup \ell_2$ is accepting; we show that either $\ell_1$ or $\ell_2$ is accepting. The cycle $\ell_1 \cup \ell_2$ is accepted by some Rabin pair $(G_j, R_j)$, so for all edges $e \in \ell_1 \cup \ell_2$, $\gamma(e) \notin R_j$,
and there is some $e_0 \in \ell_1 \cup \ell_2$ such that $\gamma(e_0) \in G_j$. If $e_0$ belongs to $\ell_1$, then $\ell_1$ is accepted by the Rabin pair $(G_j, R_j)$, and if $e_0 \in \ell_2$, then $\ell_2$ is accepted by it.

(2 $\Rightarrow$ 3) Let $v$ be a vertex of $\mathcal{T}S$ and $\mathcal{T}_v$ the local subtree at $v$. Suppose that there is a round node $n \in \mathcal{T}_v$ with two different children $n_1$ and $n_2$. The cycles $v(n_1)$ and $v(n_2)$ are rejecting cycles over $v$, but their union is an accepting cycle (by Remark 5.2).

(3 $\Rightarrow$ 1) We observe that $\mathcal{ACD}_{\mathcal{T}S}$ is a Rabin ACD if and only if $rbw(\mathcal{T}_v) = 1$ for all vertices $v$ of $\mathcal{T}S$. In particular, the ACD-HD-Rabin-transform of $\mathcal{T}S$ does not add any state to $\mathcal{T}S$. It is immediate to check that the morphism $\varphi: \text{ACD}_{\text{Rabin}}(\mathcal{T}S) \to \mathcal{T}S$ given by $\varphi_v(v, x) = v, \varphi_E(e, l) = e$ defined in the proof of Proposition 5.28 is an isomorphism, and $\mathcal{T}S$ uses a Rabin acceptance condition. $\blacksquare$

**PROPOSITION 6.10.** Let $\mathcal{T}S = (G_{\mathcal{T}S}, \text{Acc}_{\mathcal{T}S})$ be a *Muller transition system*. The following conditions are equivalent:

1. $\mathcal{T}S$ is *Streett type*.

2. For every pair of accepting cycles $\ell_1, \ell_2 \in \textit{Cycles}(\mathcal{T}S)$ with some state in common, $\ell_1 \cup \ell_2$ is an accepting cycle.<fnref n="13" />

3. $\mathcal{ACD}_{\mathcal{T}S}$ is a *Streett ACD*.

**PROOF.** Implications (1 $\Rightarrow$ 2) and (2 $\Rightarrow$ 3) are analogous to those from Proposition 6.9.

(3 $\Rightarrow$ 1) We consider the transition system $\overline{\mathcal{T}S}$ obtained by complementing the acceptance set of $\text{Acc}_{\mathcal{T}S}$. By Remark 5.6, the ACD of $\overline{\mathcal{T}S}$ is obtained from $\mathcal{ACD}_{\mathcal{T}S}$ by turning round nodes into square nodes and vice-versa. Thus, the ACD of $\overline{\mathcal{T}S}$ is a Rabin ACD, and by applying the previous proposition we can define a Rabin condition $\text{Acc}_R = (\gamma, \Gamma, \text{Rabin}_\Gamma(R))$ such that the transition system $(G_{\mathcal{T}S}, \text{Acc}_R)$ is isomorphic to $\overline{\mathcal{T}S}$. Since $\text{Streett}_\Gamma(R)$ is the complement language of $\text{Rabin}_\Gamma(R)$, we obtain that $\text{Acc}_S = (\gamma, \Gamma, \text{Streett}_\Gamma(R))$ is a Streett acceptance condition equivalent to $\text{Acc}_{\mathcal{T}S}$ over $G_{\mathcal{T}S}$. $\blacksquare$

**PROPOSITION 6.11.** Let $\mathcal{T}S = (G_{\mathcal{T}S}, \text{Acc}_{\mathcal{T}S})$ be a *Muller transition system*. The following conditions are equivalent:

1. $\mathcal{T}S$ is *parity type*.

2. For every pair of accepting (resp. rejecting) cycles $\ell_1, \ell_2 \in \textit{Cycles}(\mathcal{T}S)$ with some state in common, $\ell_1 \cup \ell_2$ is an accepting (resp. rejecting) cycle.

3. $\mathcal{ACD}_{\mathcal{T}S}$ is a *parity ACD*.

Moreover, if some condition is satisfied, $\mathcal{T}S$ is $[0, d-1]$ (resp. $[1, d]$)-parity type if and only if $\mathcal{ACD}_{\mathcal{T}S}$ is a $[0, d-1]$ (resp. $[1, d]$)-parity ACD.

**PROOF.** (1 $\Rightarrow$ 2) Proven in Lemma 4.21.

<footnote n="13">13 This property was introduced by Le Saëc under the name *cyclically closed automata* [82]. We point out that the "if" direction of the result stated in [82, Theorem 5.2] does not hold. That statement can be rephrased as: If a DMA $\mathcal{A}$ is cyclically closed, then the parity index of $\mathcal{A}$ is $[0, 1]$. We refer to Proposition 6.13 for a correct characterisation.</footnote>
(2 $\Rightarrow$ 3) Admits an analogous proof to the corresponding implication in Proposition 6.9.

(3 $\Rightarrow$ 1) By definition, $\mathcal{A}CD_{\mathcal{T}_S}$ is a parity ACD if and only if $\text{Leaves}(\mathcal{T}_v)$ is a singleton for each vertex $v$ of $\mathcal{T}_S$. In particular, the ACD-parity-transform of $\mathcal{T}_S$ does not add any state to $\mathcal{T}_S$. It is immediate to check that the morphism $\varphi: \text{ACD}_{\text{parity}}(\mathcal{T}_S) \to \mathcal{T}_S$ defined in the proof of Proposition 5.19 is an isomorphism. Therefore, $\mathcal{T}_S$ and $\text{ACD}_{\text{parity}}(\mathcal{T}_S)$ are isomorphic transition systems, and the latter uses a parity acceptance condition that is a $[0, d-1]$ (resp. $[1, d]$)-parity condition if $\mathcal{A}CD_{\mathcal{T}_S}$ is a $[0, d-1]$ (resp. $[1, d]$)-parity ACD. If $\mathcal{A}CD_{\mathcal{T}_S}$ is not a $[0, d-1]$ (resp. $[1, d]$)-parity ACD, then the number of colours cannot be reduced by the optimality of the number of colours of the ACD-parity-transform (Theorem 5.34). ■

**COROLLARY 6.12.** *A Muller transition system is parity type if and only if it is both Rabin and Streett type.*

**The ACD and the parity index of $\omega$-regular languages.**

**PROPOSITION 6.13.** *Let $\mathcal{A}$ be a deterministic Muller automaton whose states are accessible. Then, the parity index of $\mathcal{L}(\mathcal{A})$ is:*

— $[0, d-1]$ (resp. $[1, d]$) if and only if:

— trees of $\mathcal{A}CD_{\mathcal{A}}$ have height at most $d$,

— there is at least one tree of height $d$, and

— trees of height $d$ are positive (resp. negative).

— *Weak*<sub>*d*</sub> if and only if:

— trees of $\mathcal{A}CD_{\mathcal{A}}$ have height at most $d$,

— there is at least one positive tree of height $d$, and

— there is at least one negative tree of height $d$.

**PROOF.** We prove the right-to-left implication for the case *Weak*<sub>*d*</sub>. Assume that $\mathcal{A}CD_{\mathcal{A}}$ verifies the previous list of conditions (in particular, it is equidistant). Then, the ACD-parity-transform $\text{ACD}_{\text{parity}}(\mathcal{A})$ is a DPA recognising $\mathcal{L}(\mathcal{A})$ using colours in $[0, d]$. In order to obtain a DPA for $\mathcal{L}(\mathcal{A})$ with colours in $[1, d+1]$ we need to introduce a small modification to the function $p_{\mathcal{A}CD}$.
For $\ell_i$ a maximal cycle of $\mathcal{A}$ and $n \in N_{\ell_i}$ we define:

— $p'_{\mathcal{A}CD}(n) = \text{Depth}(n) + 2$, if $\ell_i$ is accepting,

— $p'_{\mathcal{A}CD}(n) = \text{Depth}(n) + 1$, if $\ell_i$ is rejecting.

It is a routine check to see that the version of the ACD-parity-transform using $p'_{\mathcal{A}CD}$ is indeed a correct parity automaton using colours in $[1, d+1]$.

To prove that no DPA recognising *L* uses less than *d* colours, it suffices to use the Flower Lemma 2.16 and the fact that a branch of length *d* in a tree of the ACD induces a *d*-flower in $\mathcal{A}$, which is positive if and only if the corresponding tree is positive (Lemma 5.42).
This is indeed a complete characterisation, since for any ACD there is a minimal *d* such that
*ACD*<sub>*A*</sub> lies in one and only one of the classes specified in the statement of the proposition. ■

**PROPOSITION 6.14.** Let $L \subseteq \Sigma^\omega$ be an $\omega$-regular language of parity index at least $[0, d-1]$ (resp. $[1, d]$). Any history-deterministic Muller automaton recognising $L$ uses an acceptance condition with at least $d$ different output colours.

**PROOF.** We first prove the result for deterministic automata. Let $\mathcal{A}$ be a DMA recognising $L$ using the acceptance condition $(\gamma, \Gamma, \text{Muller}_\Gamma(\mathcal{F}))$. By Proposition 6.13, there is a tree $\text{AltTree}(\ell_i)$ in the ACD of $\mathcal{A}$ of height at least $d$. We define $\gamma_{\mathcal{A}CD}: \text{Nodes}(\mathcal{A}CD_{\Gamma_S}) \to \Gamma$ to be the function that assigns to each node of the ACD the colours appearing in it, that is: $\gamma_{\mathcal{A}CD}(n) = \gamma(\nu(n))$. We remark that if $n'$ is a descendant of $n$ then $\gamma_{\mathcal{A}CD}(n') \subseteq \gamma_{\mathcal{A}CD}(n)$, and that a node $n$ is round if and only if $\gamma_{\mathcal{A}CD}(n) \in \mathcal{F}$. Therefore, by the alternation of round and square nodes, if $n'$ is a strict descendent of $n$, $\gamma_{\mathcal{A}CD}(n') \subseteq \gamma_{\mathcal{A}CD}(n)$. We conclude that the root of $\text{AltTree}(\ell_i)$ must contain at least $d$ different colours.

In order to obtain the result for history-deterministic automata we use finite-memory
resolvers as defined in Section 4.2. If $\mathcal{A}$ is a history-deterministic Muller automaton, it admits
a sound resolver implemented by a finite memory structure $(\mathcal{M}, \sigma)$ (Lemma 4.24). Then, the
composition $\mathcal{A} \triangleleft_{\sigma} \mathcal{M}$ is a DMA using the same number of colours, that has to be at least $d$. ■

The following result (which was already known, as it is a consequence of the construction
by Carton and Maceiras [19]), is refined and proven in Appendix A (Corollary A.16).

**PROPOSITION 6.15.** Let $\mathcal{A}$ be a deterministic parity automaton such that all its states are accessible and the parity index of $\mathcal{L}(\mathcal{A})$ is $[0, d-1]$ (resp. $[1, d]$). Then, $\mathcal{A}$ is $[0, d-1]$ (resp. $[1, d]$)-parity type.

The previous result does not hold for history-deterministic automata, as we could artifi-
cially add transitions augmenting the complexity of the structure of the automaton (enlarging
the flowers of the automaton) without modifying the language it recognises. Nevertheless, some
analogous results applying to HD automata can be obtained. Boker, Kupferman and Skrzypczak
proved that any HD parity automaton recognising a language of parity index $[0, 1]$ (resp. $[1, 2]$)
admits an equivalent HD subautomaton using a Büchi (resp. coBüchi) condition [10, Theorems 10
and 13]. We do not know whether the result holds for languages of arbitrary parity index.

**Typeness for deterministic automata.** Two automata $\mathcal{A}_1$ and $\mathcal{A}_2$ such that $\mathcal{A}_1 \simeq \mathcal{A}_2$ recognise the same language: $\mathcal{L}(\mathcal{A}_1) = \mathcal{L}(\mathcal{A}_2)$. However, the converse only holds for deterministic automata.

**LEMMA 6.16.** Let $\mathcal{A}_1$ and $\mathcal{A}_2$ be two deterministic automata over the same underlying graph and with the same labelling by input letters. Then, $\mathcal{L}(\mathcal{A}_1) = \mathcal{L}(\mathcal{A}_2)$ if and only if $\mathcal{A}_1 \simeq \mathcal{A}_2$.
**PROOF.** The implication from right to left is trivial. For the other implication, suppose that $\mathcal{L}(\mathcal{A}_1) = \mathcal{L}(\mathcal{A}_2)$, and let $\rho \in \mathcal{Run}(\mathcal{A}_1) = \mathcal{Run}(\mathcal{A}_2)$ be an infinite run over the underlying graph of $\mathcal{A}_1$. Let $w \in \Sigma^\omega$ be the word over the input alphabet $\Sigma$ labelling the run $\rho$. Since $\mathcal{A}_1$ and $\mathcal{A}_2$ are deterministic, $\rho$ is the only run over $w$, and therefore:

$$ \rho \text{ is accepting for } \mathcal{A}_1 \iff w \in \mathcal{L}(\mathcal{A}_1) = \mathcal{L}(\mathcal{A}_2) \iff \rho \text{ is accepting for } \mathcal{A}_2. \blacksquare $$

**COROLLARY 6.17 (First proven in [11, Theorem 7]).** Let $G_A$ be the underlying graph of a deterministic automaton. Then, there are Rabin and Streett conditions $Acc_R$ and $Acc_S$ such that $\mathcal{L}(G_A, Acc_R) = \mathcal{L}(G_A, Acc_S)$ if and only if there is a parity condition $Acc_p$ such that $\mathcal{L}(G_A, Acc_p) = \mathcal{L}(G_A, Acc_R) = \mathcal{L}(G_A, Acc_S)$.

We remark that the hypothesis of determinism in the previous corollary is necessary, as it has been shown that an analogous result does not hold for non-deterministic automata [11].

**PROPOSITION 6.18 (First proven in [55, Theorem 15]).** Let $\mathcal{A}$ be a deterministic Rabin (resp. Streett) automaton, and assume that $\mathcal{L}(\mathcal{A})$ can be recognised by a deterministic Büchi (resp. coBüchi) automaton; that is, the parity index of $\mathcal{L}(\mathcal{A})$ is at most [0, 1] (resp. at most [1, 2]). Then, $\mathcal{A}$ is Büchi type (resp. coBüchi type).

**PROOF.** We do the proof for the case Rabin-Büchi. We can assume that all the states of $\mathcal{A}$ are accessible, as we can define a trivial acceptance condition in the part of $\mathcal{A}$ that is not accessible. Since $\mathcal{L}(\mathcal{A})$ has parity index at most [0, 1], the trees of the ACD of $\mathcal{A}$ have height at most 2, and trees of height 2 are positive (the root is a round node), by Proposition 6.13. As $\mathcal{A}$ is a Rabin automaton, its ACD has Rabin shape (Proposition 6.9), so round nodes have at most one child. We conclude that the trees of the ACD of $\mathcal{A}$ have a single branch, so it is a [0, 1]-parity ACD, and by Proposition 6.11, $\mathcal{A}$ is Büchi type. ■

## 6.2 A normal form for parity transition systems

In this section, we propose a definition of a normal form of parity automata. This is exactly the form of automata resulting by applying the procedure defined by Carton and Maceiras [19], or, equivalently, of automata resulting from the ACD-parity-transform (Corollary 6.24). These automata satisfy that they are parity-index-tight, that is, their acceptance condition uses the minimal possible number of colours. But they offer some further convenient properties, stated in Propositions 6.25 and 6.27, which make them particularly well-suited for reasoning about deterministic parity automata.

This normal form, or partial versions of it, have already been used in the literature to prove results about parity automata in different contexts, such as history-deterministic coBüchi automata [1, 35, 57], positionality of languages defined by deterministic Büchi automata [15] or learning of DPAs [6]. The normalisation of transition systems also facilitates solving parity
games in practice [41]. However, the application of this normal form in the literature is limited to specific cases, and no prior works have provided a formal and systematic study of it.

From our results we obtain three equivalent ways of defining the normal form of a parity transition system $\mathcal{T}S$. Informally, they can be stated as:

1. $\mathcal{T}S$ use the smallest possible colour in each of its transitions (Definition 6.20).

2. $\mathcal{T}S = \text{ACD}_{\text{parity}}(\mathcal{T}S)$ (Corollary 6.24).

3. Paths in $\mathcal{T}S$ producing colour $d > 0$ can be closed into a cycle producing $d'$ as minimal colour, for all $d' \le d$ (Theorem 6.28).

**REMARK 6.19.** If $\text{Acc} = (\gamma, [d_{\min}, d_{\max}], \text{parity})$ is a parity acceptance condition over a pointed graph $G$, we can always assume that $d_{\min}$ is 0 or 1. Indeed, define $\chi = d_{\min}$ if $d_{\min}$ is even, and $\chi = d_{\min} - 1$ if $d_{\min}$ is odd. The parity acceptance condition $(\gamma', [d_{\min} - \chi, d_{\max} - \chi], \text{parity})$ defined as $\gamma'(e) = \gamma(e) - \chi$ is equivalent to $\text{Acc}$ over $G$.

**Definition of the normal form.** Just as in the definition of the ACD-parity-transform we had to define positive and negative ACDs to obtain an accurate optimality result in the number of colours, we need now to take care of a small technical detail so that $\mathcal{T}S$ in normal form are parity-index-tight.

We say that a transition system $\mathcal{T}S$ is *negative* if $\text{ACD}_{\mathcal{T}S}$ is negative, that is, if for some $d$ $\mathcal{T}S$ contains a negative $d$-flower but contains no positive $d$-flower. Intuitively, a parity $\mathcal{T}S$ is negative if and only if the minimal colour used by a parity acceptance condition using an optimal number of colours is 1.

**DEFINITION 6.20 (Normal form).** Let $\mathcal{T}S = (G_{\mathcal{T}S}, \text{Acc}_{\mathcal{T}S})$ be a parity transition system using a colouring function $\gamma$. If $\mathcal{T}S$ is not negative, we say that $\mathcal{T}S$ is in *normal form* if any other parity acceptance condition equivalent to $\text{Acc}_{\mathcal{T}S}$ over $G_{\mathcal{T}S}$ using a colouring function $\gamma'$ satisfies that for every edge $e$:

$$ \gamma(e) \le \gamma'(e). $$

If $\mathcal{T}S$ is negative, we say that it is in *normal form* if any other equivalent colouring $\gamma'$ not using colour 0 satisfies that for any edge $e$:

$$ 1 \le \gamma(e) \le \gamma'(e). $$

If $\mathcal{T}S$ is in normal form, we will also say that its acceptance condition or the colouring function it uses are in normal form.

**EXAMPLE 6.21.** Parity transition systems from Figures 3, 10, 17 and 18 are all in normal form. Parity automata appearing in Figures 10 and 17 are negative (the minimal colour used by an optimal acceptance condition is odd), whereas parity automata in Figure 18 are not.
On the other hand, the automaton from Figure 1 is not in normal form (even if it uses an
optimal number of colours). We can put it in normal form by assigning colour 1 to transitions
$q_1 \xrightarrow{a,b} q_0$ and $q_1 \xrightarrow{b,c} q_2$. The automaton obtained in this way recognises the same language. ♦

**PROPOSITION 6.22.** Let $\mathcal{T}S = (G_{\mathcal{T}S}, \mathrm{Acc}_{\mathcal{T}S})$ be a parity transition system with a colouring function $\gamma$. There is a unique parity acceptance condition equivalent to $\mathrm{Acc}_{\mathcal{T}S}$ over $G_{\mathcal{T}S}$ in normal form. Moreover, this acceptance condition is exactly the parity condition of the ACD-parity-transform of $\mathcal{T}S$.

Before showing the proof of Proposition 6.22, we prove a useful technical lemma.

**LEMMA 6.23.** Let $\mathcal{T}S$ be a parity transition system with colouring function $\gamma$. If $\ell_1 \supseteq \ell_2 \supseteq \dots \supseteq \ell_k$ is a positive (resp. negative) $k$-flower of $\mathcal{T}S$, then $\min \gamma(\ell_i) \ge k-1$ (resp. $\min \gamma(\ell_i) \ge k$).

**PROOF.** We show the result for negative flowers. Let $d_i = \min \gamma(\ell_i)$. We show that $d_i \ge i$ by induction. Since $\ell_i$ is an accepting cycle if and only if $i$ is even, we have that $d_i$ is even if and only if $i$ is even. Clearly, $d_1 \ge 1$, as 1 is the least odd number. Also, $d_{i+1} \ge d_i$, since $\ell_{i+1} \subseteq \ell_i$, and the inequality is strict by the alternation of the parity, concluding the proof. ■

**PROOF OF PROPOSITION 6.22.** We first remark that the uniqueness is directly implied by
the definition of normal form.

We prove that the acceptance condition of the ACD-parity-transform is in normal form. We note its colouring function by $\gamma_{\mathcal{A}CD}$. The transitions not belonging to any SCC are coloured 0 if $\mathcal{T}S$ is not negative and 1 if $\mathcal{T}S$ is negative, as desired. It suffices to prove the result for edges in SCCs.

We assume that $\mathcal{T}S$ is not negative and we let $S$ be an accepting SCC of $\mathcal{T}S$ (the proof is similar for $\mathcal{T}S$ negative and a rejecting SCC). Let $e = v \to v'$ be an edge in $S$, and let $\mathcal{T}_v$ be the local subtree at $v$, which is composed of a single branch (see Proposition 6.11). We let $n_0 \le n_1 \le \dots \le n_r$ be that branch, where $n_0$ is the root and $n_r$ the leaf. Let $n_k$ be the deepest node of $\mathcal{T}_v$ such that $e \in v(n_k)$. By definition of the ACD-parity-transform, $\gamma_{\mathcal{A}CD}(e) = p_{\mathcal{A}CD}(e) = k$. Also, $v(n_0) \le v(n_1) \le \dots \le v(n_k)$ is a positive $k+1$-flower (by Lemma 5.42). Lemma 6.23 implies then that any equivalent parity condition using a colouring function $\gamma'$ verifies $\gamma'(e) \ge \gamma_{\mathcal{A}CD}(e) = k$. ■

**COROLLARY 6.24.** *The ACD-parity-transform $\mathrm{ACD}_{\mathrm{parity}}(\mathcal{T}S)$ of any Muller transition system $\mathcal{T}S$ is in normal form.*

**Fundamental properties of the normal form.** We now state what we consider to be the two fundamental properties of parity transition systems in normal form. Theorem 6.28 states that these properties characterise the normal form.
**PROPOSITION 6.25.** Let $\mathcal{T}S$ be a parity transition system in normal form. If there is a path $v \rightsquigarrow v'$ producing $d$ as minimal colour, then, either:

- $v$ and $v'$ are in different SCCs (and in this case $d \in \{0, 1\}$), or

- there is a path $v' \rightsquigarrow v$ producing no colour strictly smaller than $d$.

**PROOF.** By Proposition 6.22, we know that the colouring of $\mathcal{T}S$ is the one given by its ACD-transform, that we note $\gamma_{\mathcal{A}CD}$. If $v$ and $v'$ are in different SCCs the result is trivial. Let $v$ and $v'$ be in the same SCC, that we suppose to be an accepting SCC without loss of generality. Let $\rho = v \xrightarrow{e_1} \dots \xrightarrow{e_k} v'$ be a path from $v$ to $v'$ producing min $\gamma_{\mathcal{A}CD}(\rho) = d$ as minimal colour. We remark that, as $\mathcal{A}CD_{\mathcal{T}S}$ is a parity ACD, each edge $e$ appears in one and only one branch of $\mathcal{A}CD_{\mathcal{T}S}$, and that $\gamma_{\mathcal{A}CD}(e)$ equals the depth of the deepest node containing $e$. In particular, if $e \in v(n)$ for some node $e$, $\gamma_{\mathcal{A}CD}(e) \ge \text{Depth}(n)$. Our objective is to show that a similar result holds for the path $\rho$ as a set of edges:

**CLAIM 6.26.** Let $N_\rho$ be the set of nodes of $\mathcal{A}CD_{\mathcal{T}S}$ containing the edges of the path $\rho$ in their label, that is, $N_\rho = \{n \in \text{Nodes}(\mathcal{A}CD_{\mathcal{T}S}) \mid \{e_1, \dots, e_k\} \subseteq v(n)\}$. Then, $\min(\gamma_{\mathcal{A}CD}(\rho))$ equals the depth of a node of maximal depth of $N_\rho$.<fnref n="14" />

This claim allows us to conclude. Indeed, let $n$ be a node of maximal depth of $N_\rho$, verifying $\text{Depth}(n) = d$. Then, $v(n)$ is a cycle containing the vertices $v$ and $v'$, and for all the edges $e \in v(n)$, $\gamma_{\mathcal{A}CD}(e) \ge \text{Depth}(n) = d$. This provides the desired path from $v'$ to $v$.

**Proof of Claim 6.26.** First, we remark that if $\ell_1, \ell_2, \dots, \ell_k$ are cycles such that $\ell_i$ and $\ell_{i+1}$ have some state in common, then $\cup_{i=1}^k \ell_i$ is a cycle. Let $n$ be a node of maximal depth in $N_\rho$. By the previous remarks, $\gamma_{\mathcal{A}CD}(e) \ge \text{Depth}(n)$. Suppose by contradiction that $\gamma_{\mathcal{A}CD}(\rho) > \text{Depth}(n)$. Then, each edge $e_i$ of $\rho$ would appear in some strict descendant $n_i$ of $n$ (we can assume that $n_i$ is a child of $n$). Then, $v(n_1), \dots, v(n_k)$ would be cycles such that $v(n_i)$ and $v(n_{i+1})$ have some state in common (namely, $\text{Target}(e_i) = \text{Source}(e_{i+1})$), so their union is a cycle. However, this is not possible in a parity transition system, as $v(n)$ is accepting if and only if each of the $v(n_i)$ is rejecting (see Lemma 4.21).

This completes the proof of Proposition 6.25.

**PROPOSITION 6.27 (Normal flowers do not lack petals).** Let $v$ be a state of a parity transition system in normal form belonging to an accepting (resp. rejecting) SCC. Let $\ell \in \text{Cycles}_v(\mathcal{T}S)$ be a cycle over $v$ and let $d_\ell$ be the minimal colour appearing in it.

- If $\mathcal{T}S$ is not negative, for each $x \in [0, d_\ell]$ (resp. $x \in [1, d_\ell]$) there is a cycle $\ell_x \in \text{Cycles}_v(\mathcal{T}S)$ producing $x$ as minimal colour.

<footnote n="14">14 In fact, the nodes of $N_\rho$ are totally ordered by the ancestor relation, so there is a unique node of maximal depth in $N_\rho$. This fact is not used in our proof.</footnote>
— If $\mathcal{TS}$ is negative, for each $x \in [2, d_\ell]$ (resp. $x \in [1, d_\ell]$) there is a cycle $\ell_x \in \text{Cycles}_v(\mathcal{TS})$ producing $x$ as minimal colour.

**PROOF.** We do the proof for the case in which $\mathcal{TS}$ is not negative and $v$ belongs to an accepting SCC. By Proposition 6.22, the colouring of $\mathcal{TS}$ is the one given by its ACD-transform, noted $\gamma_{\mathcal{ACD}}$. Consider the local subtree at $v$, $\mathcal{T}_v$, consisting in a single branch, as it has parity shape (Proposition 6.11). Let $n_0 \le \dots \le n_k$ be that branch, and let $n_i$ be the deepest node such that $\ell \subseteq v(n_i)$. We remark that, by definition of $\gamma_{\mathcal{ACD}}$, $d_\ell = \text{Depth}(n_i) = i$. The desired cycles are obtained by taking $\ell_x = v(n_x)$, for $x \in [0, d_\ell]$. ■

The next theorem states a simple characterisation of transition systems in normal form. It provides a useful tool to show normality of parity TS in many proofs. In essence, it shows that the two previous propositions characterise the normal form. We state it for non-negative transition systems for simplicity; a similar characterisation for negative transition systems is immediate.

We say that an SCC of a parity TS is *positive* if the minimal colour appearing on it is even, and that it is *negative* if this minimal colour is odd.

**THEOREM 6.28.** A non-negative parity transition system is in normal form if and only if:

— transitions changing of SCCs are coloured 0, and

— if $v$ and $v'$ belong to a same positive (resp. negative) SCC and there is a transition $v \xrightarrow{d} v'$ producing colour $d > 0$ (resp. $d > 1$), then there are two paths $v' \rightsquigarrow v$ producing as minimal colour $d$ and $d-1$, respectively.

**PROOF.** The fact that a TS in normal form satisfies these properties follows from the previous propositions.

Let $\mathcal{TS}$ be a TS satisfying these properties and using $\gamma$ as colouring function. Let $e = v \xrightarrow{d} v'$ be an edge with $\gamma(e) = d$. We will show that for any other equivalent colouring $\gamma'$, we have $\gamma'(e) \ge d$. This is trivial if $d=0$. If $d>0$, $v$ and $v'$ must be in the same SCC, that we assume positive without loss of generality. By hypothesis, we can close cycles $\ell_d$ and $\ell_{d-1}$ over $v$ producing $d$ and $d-1$ as minimal colour, respectively. Cycle $\ell_{d-1}$ can be decomposed in $v \to v' \rightsquigarrow v_1 \xrightarrow{d-1} v'_1 \rightsquigarrow v$. Applying the hypothesis over the edge $v_1 \xrightarrow{d-1} v'_1$ gives a path $v'_1 \rightsquigarrow v_1$ producing $d-2$ as minimal colour, which can be merged with $\ell_{d-1}$ to produce a cycle $\ell_{d-2}$ over $v$ producing $d-2$ as minimal colour. Iterating this process, we can find cycles $\ell_0 \supseteq \ell_1 \supseteq \dots \supseteq \ell_d$ over $v$ such that $\ell_i$ produces $i$ as minimal colour. Taking $\ell'_i = \bigcup_{j=i}^d \ell_j$, we obtain a positive $(d+1)$-flower $\ell'_0 \supseteq \ell'_1 \supseteq \dots \supseteq \ell'_d$, so by Lemma 6.23 we conclude that $\gamma'(e) \ge d$. ■

**Parity index from automata in normal form.** The next definition constitutes a syntactic version of the parity index, defined at the level of parity transition systems. The following
results establish the tight relation between the semantic notion of parity index and its syntactic counterpart, and state that the parity index of a language can be directly read from a DPA in normal form.

**DEFINITION 6.29.** We say that a parity transition system $\mathcal{T}S = (G_{\mathcal{T}S}, \text{Acc}_{\mathcal{T}S})$ is *parity-index-tight* if any other parity condition $\text{Acc}'$ over $G_{\mathcal{T}S}$ such that $\text{Acc}' \cong_{G_{\mathcal{T}S}} \text{Acc}_{\mathcal{T}S}$ uses at least as many colours as $\text{Acc}_{\mathcal{T}S}$.

We have shown in Corollary 6.24 that the ACD-parity-transform is always in normal form. Therefore, the optimality properties of the colouring of $\text{ACD}_{\text{parity}}(\mathcal{T}S)$ (Theorem 5.34) transfer to parity transition systems in normal form.

**COROLLARY 6.30.** A parity transition system in normal form is parity-index-tight.

Moreover, the parity index of an $\omega$-regular language can be read from any DPA in normal form recognising it.

**COROLLARY 6.31.** Let $\mathcal{A}$ be a deterministic parity automaton in normal form such that all its states are accessible. If $\mathcal{A}$ uses colours in $[0, d-1]$ (resp. $[1, d]$), then the parity index of $\mathcal{L}(\mathcal{A})$ is $\text{Weak}_{d-1}$ or $[0, d-1]$ (resp. $\text{Weak}_{d-1}$ or $[1, d]$).

We prove this result in Appendix A (Corollary A.15), and we provide there a refined characterisation by using generalised weak automata.

## 6.3 Minimisation of deterministic parity automata recognising Muller languages

The minimisation of $\omega$-automata is a fundamental problem of an intriguing complexity. In 2010, Schewe showed that the minimisation of deterministic Büchi and parity automata is NP-complete, if the acceptance condition is defined over the states [86]. However, the reduction of NP-hardness does not generalise to automata with edge-based acceptance. A surprising positive result was obtained in 2019 by Abu Radi and Kupferman: we can minimise in polynomial time HD coBüchi automata using transition-based acceptance [1]. Schewe showed that the minimisation was again NP-hard for HD automata with state-based acceptance [87]. To the best of our knowledge, the only existing hardness result applying to transition-based automata is Casares' result about the NP-completeness of the minimisation of deterministic Rabin automata [21]. In fact, in [21] a stronger result is proven: it is NP-hard to minimise deterministic Rabin automata recognising Muller languages.

In this section, we provide a polynomial-time algorithm for the minimisation of DPA recognising Muller languages (with acceptance condition over transitions). By Proposition 4.10 and Theorem 4.15, we know that a minimal (history-)deterministic parity automaton recognising a Muller language $L = \text{Muller}_\Sigma(\mathcal{F})$ can be constructed in linear time from the Zielonka tree $\mathcal{Z}_F$.
We will therefore provide a polynomial-time algorithm computing this Zielonka tree from a DPA recognising *L*.

**THEOREM 6.32.** Let $\mathcal{A}$ be a DPA recognising a Muller language $L = \text{Muller}_\Sigma(\mathcal{F})$. We can find a minimal deterministic (resp. history-deterministic) parity automaton recognising $L$ in polynomial time in the size of the representation of $\mathcal{A}$.<fnref n="15" />

**Description of the algorithm.** Let $\mathcal{A} = (Q, \Sigma, q_0, \Gamma, \Delta, \text{parity})$ be a DPA recognising $L = \text{Muller}_\Sigma(\mathcal{F})$. We outline a recursive algorithm building $\mathcal{Z}_\mathcal{F} = (N, \leq, \nu)$ in a top-down fashion; it starts from the root of the tree (which is always labelled $\Sigma$), and each time that some node is added to $N$, we compute its children. If we have built $\mathcal{Z}_\mathcal{F}$ up to a node $n$, we compute the children of $n$ by using the procedure *AlternatingSets* described in Algorithm 1, which we disclose next.

We assume without loss of generality that $n$ is round, that is, $\nu(n) \in \mathcal{F}$. First, we take the restriction of $\mathcal{A}$ to transitions labelled with letters in $\nu(n)$ and pick a final SCC on it. Such final SCC induces a subautomaton $\mathcal{A}'$ of $\mathcal{A}$ recognising $\text{Muller}_{\nu(n)}(\mathcal{F}|_{\nu(n)})$ (see also Lemma 4.20). Our objective is to find the maximal subautomata of $\mathcal{A}'$ using as input letters sets $X \subseteq \nu(n)$ such that $X \notin \mathcal{F}$. We will keep all such subsets $X$ in a list *altSets*. The labels of the children of $n$ will then correspond to the maximal sets appearing in this list, which are returned by the algorithm *AlternatingSets* (Line 11). In order to find them, we remove the transitions using the minimal colour in $\mathcal{A}'$ (that is even, since $\nu(n) \in \mathcal{F}$) and compute a decomposition in strongly connected components of the obtained graph. Let $S$ be a component of this decomposition and let $\Sigma_S \subseteq \nu(n)$ be the input letters appearing in it. Then, $\Sigma_S \notin \mathcal{F}$ if and only if the minimal output colour in $S$ is odd (see Lemma 6.33 below). In this case, we add $\Sigma_S$ to *altSets*. On the contrary, we remove the minimal (even) colour from $S$, and we start again finding a decomposition in SCCs of the obtained graph.

We include the pseudocode for the procedure *AlternatingSets* in Algorithm 1. We use the following notations:

- *Letters*(S) is the set of input letters appearing in S,

- *MinColour*(S) is the minimal output colour appearing in S (which determines whether *Letters*(S) ∈ F, if S is strongly connected),

- *SCC-Decomposition*(A) outputs a list of the strongly connected components of A. If A is empty, it outputs an empty list.

- *MaxInclusion*(lst) returns the list of the maximal subsets in lst.

<footnote n="15">15 We can assume that the representation of $\mathcal{A}$ has size polynomial in $|Q| + |\Sigma|$, where $Q$ and $\Sigma$ are the set of states and the input alphabet of $\mathcal{A}$. Indeed, as $\mathcal{A}$ is deterministic the number of transitions is at most $|Q| \cdot |\Sigma|$, and we can assume that $\mathcal{A}$ has no more output colours than transitions.</footnote>
**Input:** A strongly connected automaton $\mathcal{A}$ over $\Sigma$; $\mathcal{L}(\mathcal{A}) = \text{Muller}(\mathcal{F})$
**Output:** Maximal subsets $\Sigma_1, \dots, \Sigma_k \subseteq \Sigma$ such that $\Sigma_i \in \mathcal{F} \iff \Sigma \notin \mathcal{F}$
1: $d \leftarrow \text{MinColour}(\mathcal{A})$
2: $\mathcal{A}_{>d} \leftarrow$ restriction of $\mathcal{A}$ to transitions $\Delta_{>d} = \{q \xrightarrow{a:x} q' \in \Delta \mid x > d\}$
3: $\langle S_1, \dots, S_r \rangle \leftarrow \text{SCC-Decomposition}(\mathcal{A}_{>d})$
4: $\text{altSets} \leftarrow \{$
5: **for** $i = 1, \dots, r$ **do**
6: &nbsp;&nbsp;&nbsp;&nbsp;**if** $\text{MinColour}(S_i)$ is odd if and only if $d$ is even **then**
7: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;altSets $\leftarrow$ altSets $\cup \{\text{Letters}(S_i)\}$
8: &nbsp;&nbsp;&nbsp;&nbsp;**else**
9: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;altSets $\leftarrow$ altSets $\cup \text{AlternatingSets}(S_i)$
10: $\text{maxAltSets} \leftarrow \text{MaxInclusion}(\text{altSets})$
11: **return** $\text{maxAltSets}$

<caption>**Algorithm 1.** AlternatingSets($\mathcal{A}$): Computing the children of a node.</caption>

**Correctness of the algorithm.** Let $n$ be a node of the Zielonka tree of $\mathcal{F}$ labelled with $v(n)$, and let $\mathcal{A}_n$ be an accessible subautomaton of $\mathcal{A}$ over $v(n)$ recognising $\text{Muller}_{v(n)}(\mathcal{F}|_{v(n)})$. We prove that $\text{AlternatingSets}(\mathcal{A}_n)$ returns a list of sets corresponding to the labels of the children of $n$ in $\mathcal{Z}_{\mathcal{F}}$. We assume without loss of generality that $v(n) \in \mathcal{F}$ and therefore the minimal colour $d$ in $\mathcal{A}_n$ is even.

First, we observe that if $X \subseteq \Sigma$ is added to altSets during the execution of the procedure AlternatingSets, then $X$ is the set of input letters appearing in a cycle whose minimal colour is odd. Next lemma implies that in this case, $X \notin \mathcal{F}$. In particular, no subset is added if $n$ is a leaf of $\mathcal{Z}_{\mathcal{F}}$.

**LEMMA 6.33.** Let $\mathcal{A}$ be a DPA such that $\mathcal{L}(\mathcal{A}) = \text{Muller}_{\Sigma}(\mathcal{F})$. Let $\ell \in \text{Cycles}(\mathcal{A})$ be an accessible cycle of $\mathcal{A}$. Let $\Sigma_{\ell} \subseteq \Sigma$ be the input letters appearing in $\ell$, and let $d_{\ell}$ be the minimal colour on $\ell$. Then, $\Sigma_{\ell} \in \mathcal{F}$ if and only if $d_{\ell}$ is even.

**PROOF.** Since $\ell$ is an accessible cycle, there is a word $w \in \Sigma^\omega$ such that $\text{Inf}(w) = \Sigma_\ell$ and verifying that the edges visited infinitely often by the (only) run over $w$ in $\mathcal{A}$ are the edges of $\ell$. Therefore $w \in \mathcal{L}(\mathcal{A})$ if and only if $d_\ell$ is even, and since $\mathcal{L}(\mathcal{A})$ is a Muller language, $w \in \mathcal{L}(\mathcal{A})$ if and only if $\text{Inf}(w) = \Sigma_\ell \in \mathcal{F}$. $\blacksquare$
As the final output of the algorithm consists solely on the maximal subsets in altSets, and no accepting set is added to this list, it suffices to show that each maximal rejecting subset $\Sigma_{max} \subseteq \nu(n)$ is added to altSets at some point.

Let $\Sigma_{max} \subseteq \nu(n)$ be one of the maximal rejecting subsets of $\nu(n)$. Let $S$ be a final SCC of the restriction of $A_n$ to transitions labelled with letters in $\Sigma_{max}$ (by the previous lemma, MinColour($S$) is odd). We show that $\Sigma_{max}$ will eventually be considered by the recursive procedure AlternatingSets, and therefore $\Sigma_{max}$ will be added to altSets. We use of the following remark:

**CLAIM 6.34.** If $S'$ is a strongly connected subautomaton of $A_n$ such that $S \subseteq S' \subseteq A_n$, then the minimal colour in $S'$ is even.

**Proof.** Let $\Sigma'$ be the input letters appearing in $S'$. As $S \subseteq S'$ and no transition labelled with a letter in $\Sigma_{max}$ leaves $S$, we must have $\Sigma_{max} \subseteq \Sigma'$. The claim follows from Lemma 6.33. ♦

<figure><img src="image_37.png" /></figure>

Therefore, either $S$ is one of the SCCs of $A_{>d}$ (in this case, $\Sigma_{max}$ is added to altSets in Line 7), or it is contained in one SCC of $A_{>d}$ whose minimal colour is even, and we can conclude by induction.

**Complexity analysis.** We will show that the proposed algorithm works in time $O(|Q|^3|\Sigma|^2|\Gamma|)$, where $Q$, $\Sigma$ and $\Gamma$ are the states, set of input letters and set of output colours of the automaton, respectively. We remark that, since $\mathcal{A}$ is deterministic, $|\Delta| \le |Q||\Sigma|$.

First, we study the complexity of the procedure AlternatingSets($\mathcal{A}$). At each recursive call, at least one edge is removed from $\Delta$, and a decomposition in strongly connected components of the automaton is performed, which can be done in $O(|Q||\Sigma|)$ [91]. Therefore, the children of a node of the Zielonka tree can be computed in $O(|Q|^2|\Sigma|^2)$.

We perform this operation for each node of the Zielonka tree. By the optimality of the ZT-parity-automaton (Theorems 4.14 and 4.15), we know that $|Q| \ge |\text{Leaves}(Z_F)|$ and that the height of $Z_F$ is at most $|\Gamma|$. Therefore, $|Z_F| \le |Q||\Gamma|$, and the procedure AlternatingSets is called at most $|Q||\Gamma|$ times. We conclude that the proposed algorithm works in time $O(|Q|^3|\Sigma|^2|\Gamma|)$.

**REMARK 6.35 (State-based automata).** The acceptance condition of the parity automaton obtained from the Zielonka tree appears naturally over the transitions of the automaton. In order to make it a state-based automaton, we would need to add one state per colour it uses. It turns out that, in this specific case, this is optimal, and the state-based parity automaton we obtain is minimal. Therefore, we can also minimise in polynomial time state-based parity automata recognising Muller languages. However, it is no longer possible to obtain optimal transformations towards state-based parity automata based on the ACD (see [25, Section 5.3] and [22, Section I.8] for further details).
# 7. Conclusion

In this work, we have carried out an extensive study of transformations of automata and games that use Muller acceptance conditions. We have proposed different types of morphisms to formalise the idea of valid transformations of transition systems, which distil the central features of existing transformations. Our main contribution resides in the introduction of a new structure, the alternating cycle decomposition, which is a succinct representation of the alternating chains of loops of a Muller automaton – in the sense of Wagner [93] – and provides the necessary information to understand the interplay between its acceptance condition and its underlying graph.

**Optimal and practical transformations of automata.** We have presented a transformation that, given a deterministic Muller automaton, provides an equivalent deterministic parity automaton, and another that provides an equivalent history-deterministic Rabin automaton. These transformations are optimal in a strong sense; the obtained automata have a minimal number of states amongst those which accept a history-deterministic mapping to the original Muller automaton. The first of these transformations has been implemented in the open-source tools Spot 2.10 [2] and Owl 21.0 [52], and it has been shown to perform extremely well in practice [25], as the natural definition of the ACD provides a fairly efficient way to compute the transformation, while its optimality guarantees to produce automata as small as possible.

**Understanding the limitations of history-deterministic automata.** As a corollary of our results, we have obtained that minimal deterministic and history-deterministic parity automata recognising Muller languages have the same size (Corollary 4.16). Moreover, we have shown that HD parity automata that are strictly smaller than equivalent deterministic ones cannot come from a deterministic Muller automaton (Corollary 5.39). This provides a partial explanation on the difficulty to find succinct HD parity automata, as we could argue that a simple way to conceptualise $\omega$-regular languages is through deterministic Muller automata. Maybe most importantly, this sets a limitation in the usefulness of history-determinism in practice, as procedures that use a DMA as an intermediate step – as the ones from the tools Strix [65] and ltlsynt [70], or automata determinisation [78, 88, 64] – cannot benefit from the succinctness of HD automata.

On the other hand, we have shown that, if our objective is to obtain Rabin automata as output, the ACD-HD-Rabin-transform allows us to benefit from succinct HD automata. In this case, it has been shown that these automata can be exponentially smaller than equivalent deterministic ones [24, Theorem 21].

**Disclosing the structure of $\omega$-automata.** As an application of the insights gained from the alternating cycle decomposition, we have derived results concerning typeness of automata. In
particular, we have characterised when we can define a parity, Rabin or Streett condition on top of a Muller automaton, obtaining an equivalent automaton (Propositions 6.9, 6.10 and 6.11). These characterisations have already been proven instrumental in works about the memory for games [21], and to obtain lower bounds on the size of deterministic Rabin automata [24].

We have also employed the ACD to present a normal form for parity transition systems and systematically proved the most important properties that make this form a valuable tool for manipulating parity automata. We believe that this normal form will be useful to extend existing results about Büchi and coBüchi automata (as the ones in [1, 10, 15]) to parity automata.

## References

[1] Bader Abu Radi and Orna Kupferman. Minimization and canonization of GFG transition-based automata. Logical Methods in Computer Science, 18(3), 2022. DOI (4, 6, 7, 70, 83, 88, 93)

[2] Alexandre Duret-Lutz, Etienne Renault, Maximilien Colange, Florian Renkin, Alexandre Gbaguidi Aisse, Philipp Schlehuber-Caissier, Thomas Medioni, Antoine Martin, Jérôme Dubois, Clément Gillard, and Henrich Lauko. From Spot 2.0 to Spot 2.10: what's new? International Conference on Computer-Aided Verification, CAV, volume 13372 of Lecture Notes in Computer Science, pages 174–187, 2022. DOI (7, 92)

[3] André Arnold, Jacques Duparc, Filip Murlak, and Damian Niwiński. On the topological complexity of tree languages. Logic and Automata: History and Perspectives [in Honor of Wolfgang Thomas], volume 2 of Texts in Logic and Games, pages 9–28, 2008. DOI (3)

[4] Tomáš Babiak, František Blahoudek, Alexandre Duret-Lutz, Joachim Klein, Jan Křetínský, David Müller, David Parker, and Jan Strejček. The Hanoi omega-automata format. International Conference on Computer-Aided Verification, CAV, pages 479–486, 2015. DOI (107)

[5] Roderick Bloem, Krishnendu Chatterjee, and Barbara Jobstmann. Graph games and reactive synthesis. Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pages 921–962. Springer International Publishing, 2018. DOI (2)

[6] León Bohn and Christof Löding. Constructing deterministic parity automata from positive and negative examples. CoRR, abs/2302.11043, 2023. DOI (6, 83)

[7] Bernard Boigelot, Sébastien Jodogne, and Pierre Wolper. On the use of weak automata for deciding linear arithmetic with integer and real variables. International Joint Conference on Automated Reasoning, IJCAR, pages 611–625, 2001. DOI (6, 101)

[8] Udi Boker. Why these automata types? Logic for Programming, Artificial Intelligence and Reasoning, LPAR, volume 57 of EPiC Series in Computing, pages 143–163, 2018. DOI (16)

[9] Udi Boker, Denis Kuperberg, Orna Kupferman, and Michał Skrzypczak. Nondeterminism in the presence of a diverse or unknown future. International Colloquium on Automata, Languages and Programming, ICALP, pages 89–100, 2013. DOI (10, 42)

[10] Udi Boker, Orna Kupferman, and Michał Skrzypczak. How deterministic are good-for-games automata? Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS, volume 93, 18:1–18:14, 2017. DOI (77, 82, 93)

[11] Udi Boker, Orna Kupferman, and Avital Steinitz. Parityizing Rabin and Streett. Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS, volume 8 of LIPIcs, pages 412–423, 2010. DOI (6, 77, 83)

[12] Udi Boker and Karoliina Lehtinen. Good for Games Automata: From Nondeterminism to Alternation. International Conference on Concurrency Theory, CONCUR, volume 140, 19:1–19:16, 2019. DOI (19, 52)

[13] Udi Boker and Karoliina Lehtinen. History determinism vs. good for gameness in quantitative automata. Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS, volume 213, 38:1–38:20, 2021. DOI (14)

[14] Udi Boker and Karoliina Lehtinen. When a little nondeterminism goes a long way: an introduction to history-determinism. ACM SIGLOG News, 10(1):24–51, 2023. DOI (4, 10)

[15] Patricia Bouyer, Antonio Casares, Mickael Randour, and Pierre Vandenhove. Half-positional objectives recognized by deterministic Büchi automata. International Conference on Concurrency Theory, CONCUR, volume 243, 20:1–20:18, 2022. DOI (6, 7, 83, 93)
[16] Julian C. Bradfield. Simplifying the modal mu-calculus alternation hierarchy. Symposium on Theoretical Aspects of Computer Science, STACS, pages 39–49, 1998. DOI (3)

[17] J. Richard Büchi. On a decision method in restricted second order arithmetic. Proceedings of the International Congress on Logic, Methodology and Philosophy of Science:1–11, 1960. (17)

[18] Cristian S. Calude, Sanjay Jain, Bakhadyr Khoussainov, Wei Li, and Frank Stephan. Deciding parity games in quasip polynomial time. Symposium on Theory of Computing, STOC, pages 252–263. ACM, 2017. DOI (3)

[19] Olivier Carton and Ramón Maceiras. Computing the Rabin index of a parity automaton. Theoretical Informatics and Applications, RAIRO:495–506, 1999. DOI (6, 18, 64, 82, 83)

[20] Olivier Carton and Max Michel. Unambiguous Büchi automata. Theoretical Computer Science, 297(1):37–81, 2003. DOI (32)

[21] Antonio Casares. On the minimisation of transition-based Rabin automata and the chromatic memory requirements of Muller conditions. Computer Science Logic, CSL, volume 216, 12:1–12:17, 2022. DOI (3, 7, 34, 88, 93)

[22] Antonio Casares. Structural properties of automata over infinite words and memory for games (Propriétés structurelles des automates sur les mots infinis et mémoire pour les jeux). PhD Thesis, Université de Bordeaux, France, 2023. URL (91)

[23] Antonio Casares, Thomas Colcombet, and Nathanaël Fijalkow. Optimal transformations of games and automata using Muller conditions. International Colloquium on Automata, Languages and Programming, ICALP, volume 198, 123:1–123:14, 2021. DOI (1, 7, 71)

[24] Antonio Casares, Thomas Colcombet, and Karoliina Lehtinen. On the size of good-for-games Rabin automata and its link with the memory in Muller games. International Colloquium on Automata, Languages and Programming, ICALP, volume 229, 117:1–117:20, 2022. DOI (1, 3, 7, 34, 70, 92, 93)

[25] Antonio Casares, Alexandre Duret-Lutz, Klara J. Meyer, Florian Renkin, and Salomon Sickert. Practical applications of the Alternating Cycle Decomposition. International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS, volume 13244 of Lecture Notes in Computer Science, pages 99–117, 2022. DOI (7, 91, 92)

[26] Antonio Casares and Corto Mascle. The complexity of simplifying $\omega$-automata through the alternating cycle decomposition. CoRR, abs/2401.03811, 2024. DOI (61)

[27] Thomas Colcombet. Forms of Determinism for Automata (Invited Talk). Symposium on Theoretical Aspects of Computer Science, STACS, volume 14, pages 1–23, 2012. DOI (4, 22)

[28] Thomas Colcombet. The theory of stabilisation monoids and regular cost functions. International Colloquium on Automata, Languages and Programming, ICALP, pages 139–150, 2009. DOI (4, 14)

[29] Thomas Colcombet. Unambiguity in automata theory. International Conference on Descriptional Complexity of Formal Systems, DFCS, volume 9118 of Lecture Notes in Computer Science, pages 3–18, 2015. DOI (32)

[30] Thomas Colcombet and Christof Löding. The non-deterministic Mostowski hierarchy and distance-parity automata. International Colloquium on Automata, Languages and Programming, ICALP, volume 5126, pages 398–409, 2008. DOI (3)

[31] Thomas Colcombet and Damian Niwiński. On the positional determinacy of edge-labeled games. Theoretical Computer Science, 352(1-3):190–196, 2006. DOI (3, 7)

[32] Thomas Colcombet and Konrad Zdanowski. A tight lower bound for determinization of transition labeled Büchi automata. International Colloquium on Automata, Languages and Programming, ICALP, pages 151–162, 2009. DOI (7)

[33] Antonio Di Stasio, Aniello Murano, Vincenzo Prignano, and Loredana Sorrentino. Improving parity games in practice. Annals of Mathematics and Artificial Intelligence, 2021. DOI (2)

[34] Stefan Dziembowski, Marcin Jurdziński, and Igor Walukiewicz. How much memory is needed to win infinite games? Symposium on Logic in Computer Science, LICS, pages 99–110, 1997. DOI (4, 5, 34, 44, 48, 52, 56)

[35] Rüdiger Ehlers and Sven Schewe. Natural colors of infinite words. Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS, volume 250, 36:1–36:17, 2022. DOI (6, 7, 83)

[36] E. Allen Emerson and Charanjit S. Jutla. The complexity of tree automata and logics of programs. SIAM Journal of Computing, 29(1):132–158, 1999. DOI (3)

[37] E. Allen Emerson and Charanjit S. Jutla. Tree automata, mu-calculus and determinacy (extended abstract). Symposium on Foundations of Computer Science, FOCS, pages 368–377, 1991. DOI (3)

[38] E. Allen Emerson, Charanjit S. Jutla, and A. Prasad Sistla. On model-checking for fragments of $\mu$-calculus. International Conference on Computer-Aided Verification, CAV, volume 697 of Lecture Notes in Computer Science, pages 385–396, 1993. DOI (3)

[39] Javier Esparza, Jan Křetínský, Jean-François Raskin, and Salomon Sickert. From LTL and limit-deterministic Büchi automata to deterministic parity automata. International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS, pages 426–442, 2017. DOI (2)

[40] Seth Fogarty, Orna Kupferman, Moshe Y. Vardi, and Thomas Wilke. Profile trees for Büchi word automata, with application to determinization. Information and Computation, 245:136–151, 2015. DOI (3)
[41] Oliver Friedmann and Martin Lange. Solving parity games in practice. *International Symposium on Automated Technology for Verification and Analysis*, ATVA, pages 182–196, 2009. DOI (2, 6, 84)

[42] Dimitra Giannakopoulou and Flavio Lerda. From states to transitions: improving translation of LTL formulae to Büchi automata. *International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE*, pages 308–326, 2002. DOI (7)

[43] Yuri Gurevich and Leo Harrington. Trees, automata, and games. *Symposium on Theory of Computing*, STOC, pages 60–65, 1982. DOI (3)

[44] Thomas A. Henzinger and Nir Piterman. Solving games without determinization. *Computer Science Logic, CSL*, pages 395–410, 2006. DOI (4, 10, 14, 44, 45, 70)

[45] Florian Horn. Explicit Muller games are PTIME. *Conference on Foundations of Software Technology and Theoretical Computer Science*, FSTTCS, pages 235–243, 2008. DOI (16)

[46] Florian Horn. Random fruits on the Zielonka tree. *Symposium on Theoretical Aspects of Computer Science, STACS*, volume 3, pages 541–552, 2009. DOI (4)

[47] Paul Hunter and Anuj Dawar. Complexity bounds for regular games. *International Symposium on Mathematical Foundations of Computer Science*, MFCS, pages 495–506, 2005. DOI (3, 16)

[48] Swen Jacobs, Guillermo A. Perez, Remco Abraham, Veronique Bruyere, Michael Cadilhac, Maximilien Colange, Charly Delfosse, Tom van Dijk, Alexandre Duret-Lutz, Peter Faymonville, Bernd Finkbeiner, Ayrat Khalimov, Felix Klein, Michael Luttenberger, Klara Meyer, Thibaud Michaud, Adrien Pommellet, Florian Renkin, Philipp Schlehuber-Caissier, Mouhammad Sakr, Salomon Sickert, Gaetan Staquet, Clement Tamines, Leander Tentrup, and Adam Walker. The reactive synthesis competition (SYNTCOMP): 2018-2021, 2022. DOI (2)

[49] Marcin Jurdziński. Deciding the winner in parity games is in UP ∩ co-UP. *Information Processing Letters*, 68(3):119–124, 1998. DOI (3)

[50] Michael Kaminski. A classification of ω-regular languages. *Theoretical Computer Science*, 36:217–229, 1985. DOI (18)

[51] Nils Klarlund. Progress measures, immediate determinacy, and a subset construction for tree automata. *Annals of Pure and Applied Logic*, 69(2):243–268, 1994. DOI (56)

[52] Jan Kretínský, Tobias Meggendorfer, and Salomon Sickert. Owl: A library for ω-words, automata, and LTL. *International Symposium on Automated Technology for Verification and Analysis*, ATVA, volume 11138 of Lecture Notes in Computer Science, pages 543–550, 2018. DOI (7, 92)

[53] Jan Křetínský, Tobias Meggendorfer, Clara Waldmann, and Maximilian Weininger. Index appearance record for transforming Rabin automata into parity automata. *International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS*, pages 443–460, 2017. DOI (3)

[54] Jan Křetínský, Tobias Meggendorfer, Clara Waldmann, and Maximilian Weininger. Index appearance record with preorders. *Acta Informatica*, 59:585–618, 2021. DOI (4)

[55] Sriram C. Krishnan, Anuj Puri, and Robert K. Brayton. Deterministic ω-automata vis-a-vis deterministic Büchi automata. *International Symposium on Algorithms and Computation, ISAAC*, volume 834 of Lecture Notes in Computer Science, pages 378–386, 1994. DOI (6, 77, 83)

[56] Sriram C. Krishnan, Anuj Puri, and Robert K. Brayton. Structural complexity of omega-automata. *Symposium on Theoretical Aspects of Computer Science, STACS*, pages 143–156, 1995. DOI (18, 77)

[57] Denis Kuperberg and Michał Skrzypczak. On determinisation of good-for-games automata. *International Colloquium on Automata, Languages and Programming, ICALP*, pages 299–310, 2015. DOI (4, 6, 70, 83)

[58] Orna Kupferman. Automata theory and model checking. *Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem*, editors, *Handbook of Model Checking*, pages 107–151. Springer International Publishing, 2018. DOI (2)

[59] Orna Kupferman, Gila Morgenstern, and Aniello Murano. Typeness for omega-regular automata. *International Journal on Foundations of Computer Science*, 17(4):869–884, 2006. DOI (77)

[60] Orna Kupferman, Shmuel Safra, and Moshe Y. Vardi. Relating word and tree automata. *Symposium on Logic in Computer Science, LICS*, pages 322–332, 1996. DOI (3)

[61] Orna Kupferman and Moshe Y. Vardi. Safraless decision procedures. *Symposium on Foundations of Computer Science, FOCS*, pages 531–542, 2005. DOI (2)

[62] Oebele Lijzenga and Tom van Dijk. Symbolic parity game solvers that yield winning strategies. *International Symposium on Games, Automata, Logics, and Formal Verification, GandALF*, volume 326, pages 18–32, 2020. DOI (2)

[63] Christof Löding. Optimal bounds for transformations of ω-automata. *Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS*, pages 97–109, 1999. DOI (3, 5, 77)

[64] Christof Löding and Anton Pirogov. Determinization of Büchi automata: unifying the approaches of Safra and Muller-Schupp. *International Colloquium on Automata, Languages and Programming, ICALP*, 120:1–120:13, 2019. DOI (2, 92)
[65] Michael Luttenberger, Philipp J. Meyer, and Salomon Sickert. Practical synthesis of reactive systems from LTL specifications via parity games. Acta Informatica:3–36, 2020. DOI (2, 92)

[66] Robert McNaughton. Infinite games played on finite graphs. Annals of Pure and Applied Logic, 65(2):149–184, 1993. DOI (44, 49)

[67] Robert McNaughton. Testing and generating infinite sequences by a finite automaton. Information and Control, 9(5):521–530, 1966. DOI (17, 19)

[68] Philipp Meyer and Salomon Sickert. On the optimal and practical conversion of Emerson-Lei automata into parity automata, 2021. Personal Communication (4, 5)

[69] Philipp J. Meyer and Salomon Sickert. Modernising strix, 2021. URL (2, 7)

[70] Thibaud Michaud and Maximilien Colange. Reactive synthesis from LTL specification with Spot. Workshop on Synthesis, SYNT, Electronic Proceedings in Theoretical Computer Science, 2018. (2, 92)

[71] Andrzej W. Mostowski. Regular expressions for infinite trees and a standard form of automata. Symposium on Computation Theory, SCT, pages 157–168, 1984. DOI (16–18)

[72] David E. Muller. Infinite sequences and finite machines. Symposium on Switching Circuit Theory and Logical Design, SWCT, pages 3–16, 1963. DOI (17)

[73] David Müller and Salomon Sickert. LTL to deterministic Emerson-Lei automata. International Symposium on Games, Automata, Logics, and Formal Verification, GandALF, pages 180–194, 2017. DOI (2)

[74] Damian Niwiński. On fixed-point clones (extended abstract). International Colloquium on Automata, Languages and Programming, ICALP, volume 226, pages 464–473, 1986. DOI (3)

[75] Damian Niwiński and Igor Walukiewicz. Deciding nondeterministic hierarchy of deterministic tree automata. Workshop on Logic, Language, Information and Computation, WoLLIC, volume 123 of Electronic Notes in Theoretical Computer Science, pages 195–208, 2004. DOI (3)

[76] Damian Niwiński and Igor Walukiewicz. Relating hierarchies of word and tree automata. Symposium on Theoretical Aspects of Computer Science, STACS, pages 320–331, 1998. DOI (3, 19)

[77] Dominique Perrin and Jean-Eric Pin. Infinite words - automata, semigroups, logic and games, volume 141 of Pure and applied mathematics series. Elsevier Morgan Kaufmann, 2004. (17)

[78] Nir Piterman. From nondeterministic Büchi and Streett automata to deterministic parity automata. Symposium on Logic in Computer Science, LICS, pages 255–264, 2006. DOI (2, 92)

[79] Nir Piterman and Amir Pnueli. Temporal logic and fair discrete systems. Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pages 27–73. Springer International Publishing, 2018. DOI (2)

[80] Amir Pnueli and Roni Rosner. On the synthesis of a reactive module. POPL, pages 179–190, 1989. DOI (2)

[81] Florian Renkin, Alexandre Duret-Lutz, and Adrien Pommellet. Practical “paritizing” of Emerson-Lei automata. International Symposium on Automated Technology for Verification and Analysis, ATVA, volume 12302 of Lecture Notes in Computer Science, pages 127–143, 2020. DOI (4)

[82] Bertrand Le Saëc. Saturating right congruences. Theoretical Informatics and Applications, RAIRO, 24:545–559, 1990. DOI (80)

[83] Schmuel Safra. On the complexity of $\omega$-automata. Symposium on Foundations of Computer Science, FOCS, pages 319–327, 1988. DOI (3)

[84] Jacques Sakarovitch. A construction on finite automata that has remained hidden. Theoretical Computer Science, 204(1-2):205–231, 1998. DOI (21)

[85] Jacques Sakarovitch and Rodrigo de Souza. Lexicographic decomposition of $k$-valued transducers. Theoretical Computer Science, 47(3):758–785, 2010. DOI (21)

[86] Sven Schewe. Beyond hyper-minimisation—minimising DBAs and DPAs is NP-complete. Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS, volume 8, pages 400–411, 2010. DOI (88)

[87] Sven Schewe. Minimising Good-For-Games automata is NP-complete. Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS, volume 182, 56:1–56:13, 2020. DOI (88)

[88] Sven Schewe. Tighter bounds for the determinisation of Büchi automata. International Conference on Foundations of Software Science and Computation Structures, FoSSaCS, pages 167–181, 2009. DOI (2, 3, 92)

[89] Sven Schewe and Thomas Varghese. Determinising parity automata. International Symposium on Mathematical Foundations of Computer Science, MFCS, pages 486–498, 2014. DOI (7)

[90] Michał Skrzypczak. Topological extension of parity automata. Information and Computation, 228-229:16–27, 2013. DOI (3)

[91] Robert Tarjan. Depth first search and linear graph algorithms. SIAM Journal on Computing, 1(2):114–121, 1972. DOI (91)

[92] Tom van Dijk. Oink: an implementation and evaluation of modern parity game solvers. International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS, volume 10805 of Lecture Notes in Computer Science, pages 291–308, 2018. DOI (2)

[93] Klaus Wagner. On $\omega$-regular sets. Information and Control, 43(2):123–177, 1979. DOI (3, 5, 18, 19, 57, 92)
[94] Wiesław Zielonka. Infinite games on finitely coloured graphs with applications to automata on infinite trees. *Theoretical Computer Science*, 200(1-2):135–183, 1998. DOI (3, 4, 6, 7, 16, 34, 56, 77)
# A. Generalised classes of acceptance conditions

## Further acceptance conditions.

**Generalised Büchi.** Given $k$ non-empty subsets $B_1, \dots, B_k \subseteq \Gamma$, we define the *generalised Büchi language associated to* $B = \{B_1, \dots, B_k\}$ as

$$ \text{genBüchi}_{\Gamma}(B) = \{w \in \Gamma^{\omega} \mid \text{Inf}(w) \cap B_i \neq \emptyset \text{ for all } i \in \{1, \dots, k\}\}. $$

We say that a language $L \subseteq \Gamma^{\omega}$ is a *generalised Büchi language* if there is a family of sets $B = \{B_1, \dots, B_k\}$ such that $L = \text{genBüchi}_{\Gamma}(B)$.

**Generalised coBüchi.** Given $k$ non-empty subsets $B_1, \dots, B_k \subseteq \Gamma$, we define the *generalised coBüchi language associated to* $B = \{B_1, \dots, B_k\}$ as

$$ \text{genCoBüchi}_{\Gamma}(B) = \{w \in \Gamma^{\omega} \mid \text{Inf}(w) \cap B_i = \emptyset \text{ for some } i \in \{1, \dots, k\}\}. $$

We say that a language $L \subseteq \Gamma^{\omega}$ is a *generalised coBüchi language* if there is a family of sets $B = \{B_1, \dots, B_k\}$ such that $L = \text{genCoBüchi}_{\Gamma}(B)$.

**REMARK A.1.** Deterministic generalised Büchi (resp. generalised coBüchi) automata have the same expressive power than deterministic Büchi (resp. coBüchi) automata: they recognise languages of *parity index* at most $[0, 1]$ (resp. $[1, 2]$).

We will also define *conditions that depend on the structure* of the transition system and not only on the set of colours.

**Generalised weak transition systems.** Let $\mathcal{T}S = (G_{\mathcal{T}S}, \text{Acc}_{\mathcal{T}S})$ be a transition system using a *parity condition* $\text{Acc}_{\mathcal{T}S} = (\gamma, [d_{\min}, d_{\max}], \text{parity})$. We say that $\mathcal{T}S$ is *Weak$_d$* if in each strongly connected component $S \subseteq G_{\mathcal{T}S}$ there are at most $d$ different colours that appear, that is, $|\gamma(E_S)| \le d$, where $E_S$ is the set of edges of $S$.

As for the rest of conditions, we say that a transition system $\mathcal{T}S$ is *Weak$_d$ type* if there exists an isomorphic *parity transition system* $\mathcal{T}S' \simeq \mathcal{T}S$ that is *Weak$_d$*.

The adjective *Weak* has typically been used to refer to the condition corresponding to a partition of $\mathcal{T}S$ into accepting and rejecting SCC. A run will be accepting if the component it finally stays in is accepting. It corresponds to *Weak$_1$* with our notation.

As we will show (Corollary A.11), the notation is justified by the fact that an $\omega$-regular language of parity index *Weak$_d$* can be recognised by a deterministic *Weak$_d$* automaton.

## The Zielonka tree of generalised acceptance conditions.

**DEFINITION A.2.** Let $T$ be a tree $T$ with nodes partitioned into round nodes and square nodes. We say that $T$ has:
— *Büchi shape* if it has a single branch, height at most 2, and if it has height 2 its root is round.

— *coBüchi shape* if it has a single branch, height at most 2, and if it has height 2 its root is square.

— *Generalised Büchi shape* if it has height at most 2, and if it has height 2 its root is round.

— *Generalised coBüchi shape* if it has height at most 2, and if it has height 2 its root is square.

**PROPOSITION A.3.** Let $\mathcal{F} \subseteq 2_+^\Gamma$ be a family of non-empty subsets. Then $\text{Muller}_\Gamma(\mathcal{F})$ is a Büchi (resp. coBüchi) language if and only if $\mathcal{Z}_\mathcal{F}$ has Büchi (resp. coBüchi) shape.

**PROOF.** This is just a special case of Proposition 6.4. ■

<figure><img src="image_38.png" /></figure>

**PROPOSITION A.4.** Let $\mathcal{F} \subseteq 2_+^\Gamma$ be a family of non-empty subsets. Then $\text{Muller}_\Gamma(\mathcal{F})$ is a generalised Büchi (resp. coBüchi) language if and only if $\mathcal{Z}_\mathcal{F}$ has generalised Büchi (resp. generalised coBüchi) shape.

**PROOF.** We do the proof for the case generalised Büchi (symmetric for generalised coBüchi). Assume that $\text{Muller}_\Gamma(\mathcal{F}) = \text{genBüchi}_\Gamma(B)$ for some family $B = \{B_1, \dots, B_k\}$. Then, $\Gamma \in \mathcal{F}$, as $\Gamma \cap B_i \neq \emptyset$, so the root of $\mathcal{Z}_\mathcal{F}$ is round. If $C \subseteq \Gamma$ is rejecting, $C \cap B_i = \emptyset$ for all $i$, then it is the same for any subset $C' \subseteq C$, so square nodes of $\mathcal{Z}_\mathcal{F}$ are leaves and $\mathcal{Z}_\mathcal{F}$ has height at most 2.

Conversely, assume that $\mathcal{Z}_\mathcal{F}$ has height 2 and that its root is round ($\Gamma \in \mathcal{F}$). Let $A_1, \dots, A_k$ be the labels of the $k$ leaves of $\mathcal{Z}_\mathcal{F}$ and define $B_i = A_i$. We claim that $\text{Muller}_\Gamma(\mathcal{F}) = \text{genBüchi}_\Gamma(B)$, for $B = \{B_1, \dots, B_k\}$. Indeed, if $C \in \mathcal{F}$ if and only if $C \not\subseteq A_i$ for any $i$ if and only if $C \cap B_i \neq \emptyset$ for all $i$. ■

<figure><img src="image_39.png" /></figure>

**COROLLARY A.5.** Let $\mathcal{A}$ be a deterministic generalised Büchi (resp. generalised coBüchi) automaton recognising a Muller language $L = \text{Muller}_\Sigma(\mathcal{F})$. There is a deterministic generalised Büchi (resp. generalised coBüchi) automaton recognising $L$ with just one state, that can be computed in polynomial time in the size of the representation of $\mathcal{A}$.

**PROOF.** We do the proof for the case generalised Büchi. By Remark A.1, the parity index of $L$ is at most $[0, 1]$, so by Proposition 6.13, the Zielonka tree of $\mathcal{F}$ has generalised Büchi shape. Therefore, by Proposition A.4, $L$ is a generalised Büchi that can be trivially recognised by a generalised Büchi automaton with just one state.

The acceptance condition of such automaton can be deduced in linear time from the Zielonka tree $\mathcal{Z}_\mathcal{F}$, as indicated in the proof of Proposition A.4. The Zielonka tree $\mathcal{Z}_\mathcal{F}$ can be computed from the original automaton $\mathcal{A}$ using a similar argument than in the proof of Theorem 6.32. Suppose that the generalised Büchi condition used by $\mathcal{A}$ is given by the sets $B_1, \dots, B_k \subseteq \Gamma$. Then, for each $i \in \{1, \dots, k\}$ we compute the restriction of $\mathcal{A}$ to the transitions using colours in $\Gamma \setminus B_i$, and perform a decomposition in SCCs of the obtained graph. If $\Sigma_S \subseteq \Sigma$ is the set of input letters appearing in one of those SCC, then $\Sigma_S \notin \mathcal{F}$. We put all the subsets of letters obtained in that way in a list *altSets*. The leaves of $\mathcal{Z}_\mathcal{F}$ correspond then to the maximal subsets of *altSets*. ■

<figure><img src="image_40.png" /></figure>
**ACD and typeness for generalised acceptance conditions.**

**DEFINITION A.6.** Let $\mathcal{T}S$ be a Muller transition system with a set of states $V$. We say that its alternating cycle decomposition $\mathcal{ACD}_{\mathcal{T}S}$ is a:

- *Büchi ACD* if it is a [0, 1]-parity ACD.

- *coBüchi ACD* if it is a [1, 2]-parity ACD.

- *Generalised Büchi ACD* if for every state $v \in V$, the tree $\mathcal{T}_v$ has generalised Büchi shape.

- *Generalised coBüchi ACD* if for every state $v \in V$, the tree $\mathcal{T}_v$ has generalised coBüchi shape.

- *Weak<sub>d</sub> ACD* if it is a parity ACD and trees of $\mathcal{ACD}_{\mathcal{T}S}$ have height at most *d*.

**REMARK A.7.** $\mathcal{ACD}_{\mathcal{T}S}$ is a *Weak<sub>d</sub> ACD* if and only if it is a [0, *d*)-parity ACD and a [*d* + 1]-parity ACD.

**PROPOSITION A.8.** A transition system $\mathcal{T}S$ is *Büchi* (resp. *coBüchi*) type if and only if $\mathcal{ACD}_{\mathcal{T}S}$ is a *Büchi ACD* (resp. *coBüchi ACD*).

**PROOF.** This is a special case of Proposition 6.11. ■

<figure><img src="image_41.png" /></figure>

**PROPOSITION A.9.** A transition system $\mathcal{T}S$ is *generalised Büchi* (resp. *generalised coBüchi*) type if and only if $\mathcal{ACD}_{\mathcal{T}S}$ is a *generalised Büchi ACD* (resp. *generalised coBüchi ACD*).

**PROOF.** The result follows by applying the same argument and construction than in Proposition A.4, using as set of output colours the set of edges of $\mathcal{T}S$. ■

<figure><img src="image_42.png" /></figure>

**PROPOSITION A.10.** A transition system $\mathcal{T}S$ is *Weak<sub>d</sub>* type if and only if $\mathcal{ACD}_{\mathcal{T}S}$ is a *Weak<sub>d</sub> ACD*.

**PROOF.** Proposition 6.11 already provides that $\mathcal{T}S$ is *parity type* if and only if $\mathcal{ACD}_{\mathcal{T}S}$ is a *parity ACD*. As in the proof of the aforementioned proposition, we observe that $\mathcal{T}S$ and $\mathcal{ACD}_{\text{parity}(\mathcal{T}S)}$ are isomorphic. If $\mathcal{ACD}_{\mathcal{T}S}$ is a *Weak<sub>d</sub> ACD*, then $\mathcal{ACD}_{\text{parity}(\mathcal{T}S)}$ is *Weak<sub>d</sub>*. Conversely, if $\mathcal{ACD}_{\mathcal{T}S}$ is not a *Weak<sub>d</sub> ACD*, then $\mathcal{T}S$ contains a (*d* + 1)-flower, so the number of colours cannot be reduced (using the same argument as in the proof of Theorem 5.34). ■

<figure><img src="image_43.png" /></figure>

**COROLLARY A.11.** If $L \subseteq \Sigma^\omega$ is an $\omega$-regular language of parity index *Weak<sub>d</sub>*, then *L* can be recognised by a deterministic *Weak<sub>d</sub>* automaton.

**PROOF.** Let *L* be of parity index *Weak<sub>d</sub>*. By definition, *L* is recognised by parity automaton $\mathcal{A}$ using colours in [0, *d*) (it is also recognised by an automaton using colours in [*d* + 1]; we make an arbitrary choice). We will prove that $\mathcal{A}$ is in fact *Weak<sub>d</sub>*. We will show that its ACD $\mathcal{ACD}_{\mathcal{A}}$ is *Weak<sub>d</sub>* type, which allows to conclude by Proposition A.10. Suppose that this was not the case, that is, that some tree of $\mathcal{ACD}_{\mathcal{A}}$ has height at least *d* + 1. In this case, $\mathcal{A}$ would contain a (*d* + 1)-flower (Lemma 5.42), so by the Flower Lemma 2.16, *L* has parity index at least [0, *d*) or [*d* + 1], a contradiction. ■

<figure><img src="image_44.png" /></figure>
The following result generalises [7, Theorem 2].

**COROLLARY A.12.** A Muller transition system is *Weak*<sub>*d*</sub> type if and only if it is both [0, *d*) and [1, *d* + 1]-parity type.

**Deterministic automata using generalised acceptance conditions.**

**COROLLARY A.13.** Let $G_A$ be the underlying graph of a deterministic automaton. There are [0, *d* − 1] and [1, *d*)-parity conditions $Acc_{p,0}$ and $Acc_{p,1}$ such that $\mathcal{L}(G_A, Acc_{p,0}) = \mathcal{L}(G_A, Acc_{p,1})$ if and only if there is a *Weak*<sub>*p*</sub> condition $Acc_W$ such that $\mathcal{L}(G_A, Acc_W) = \mathcal{L}(G_A, Acc_{p,0}) = \mathcal{L}(G_A, Acc_{p,1})$.

**PROPOSITION A.14.** Let $\mathcal{A}$ be a deterministic Muller automaton, and assume that $\mathcal{L}(\mathcal{A})$ can be recognised by a deterministic Büchi (resp. coBüchi) automaton; that is, the parity index of $\mathcal{L}(\mathcal{A})$ is at most [0, 1] (resp. at most [1, 2]). Then, $\mathcal{A}$ is generalised Büchi type (resp. generalised coBüchi type).

**PROOF.** We prove the result for the case generalised Büchi (analogous for coBüchi). We can assume that all the states of $\mathcal{A}$ are accessible, as we can define a trivial acceptance condition in the part of $\mathcal{A}$ that is not accessible. Since $\mathcal{L}(\mathcal{A})$ has parity index at most [0, 1], the trees of the ACD of $\mathcal{A}$ have height at most 2, and trees of height 2 are positive (the root is a round node), by Proposition 6.13, so it is a generalised Büchi ACD, and by Proposition A.9, $\mathcal{A}$ is generalised Büchi type. $\blacksquare$

**Parity index from automata in normal form.**

**COROLLARY A.15.** Let $\mathcal{A}$ be a deterministic parity automaton in normal form using colours in [0, *d* − 1] (resp. [1, *d*]) such that all its states are accessible. If $\mathcal{A}$ is *Weak*<sub>*d*−1</sub>, then the parity index of $\mathcal{L}(\mathcal{A})$ is *Weak*<sub>*d*−1</sub>. If not, the parity index of $\mathcal{L}(\mathcal{A})$ is [0, *d* − 1] (resp. [1, *d*]).

**PROOF.** We assume that $\mathcal{A}$ uses colours in [0, *d* − 1] (in particular, it is not negative). If $\mathcal{A}$ is not *Weak*<sub>*d*−1</sub>, there is an SCC containing all the colours [0, *d* − 1]. By Proposition 6.27, such SCC contains a positive *d*-flower, so by the Flower Lemma 2.16, the parity index of $\mathcal{L}(\mathcal{A})$ is [0, *d* − 1].

Suppose now that $\mathcal{A}$ is *Weak*<sub>*d*−1</sub>. Let $\ell$ be a cycle of $\mathcal{A}$ in which the colour *d* − 1 occurs. By Proposition 6.27, $\ell$ contains a negative (*d* − 1)-flower. As $\mathcal{A}$ is not negative, it also contains a positive (*d* − 1)-flower. By the Flower Lemma 2.16, the parity index of $\mathcal{L}(\mathcal{A})$ is *Weak*<sub>*d*−1</sub>. $\blacksquare$

**COROLLARY A.16.** Let $\mathcal{A}$ be a deterministic parity automaton such that all its states are accessible and the parity index of $\mathcal{L}(\mathcal{A})$ is [0, *d* − 1] (resp. [1, *d*) / *Weak*<sub>*d*</sub>). Then, $\mathcal{A}$ is [0, *d* − 1] (resp. [1, *d*) / *Weak*<sub>*d*</sub>)-parity type.
**PROOF.** We assume that $\mathcal{L}(\mathcal{A})$ has parity index $[0, d-1]$ (the other cases are similar). By the Flower Lemma 2.16, $\mathcal{A}$ does not contain any negative $d$-flower. By Proposition 6.13, the trees of the ACD of $\mathcal{A}$ have height at most $d$, and trees of height $d$ are positive. That is, $\mathcal{ACD}_{\mathcal{A}}$ is a $[0, d-1]$-parity ACD, and we conclude by applying Proposition 6.11. ■

## B. Transformations for games

**Games suitable for transformations.** As we have indicated throughout the paper, defining transformations not preserving determinism in the case of games poses certain formal challenges. This difficulties appear both when such transformations arise as the product $\mathcal{G} \times \mathcal{A}$ of a game $\mathcal{G}$ by an non-deterministic automaton $\mathcal{A}$, or when they are witnessed by an HD mapping $\varphi: \mathcal{G} \to \mathcal{G}'$. The problem comes from the fact that the semantics of non-determinism in automata (or history-determinism of morphisms) are inherently asymmetric, and this asymmetry needs to be made compatible with the semantics of games. The choices we have made to overcome this technical difficulty are:

- Restrict transformations of games to games in a standard form, which we have called *games suitable for transformations*.

- Add a restriction to HD mappings in the case of games, introducing the notion of HD-for-games mapping.

The main motivation for the standard form of games that we propose comes from viewing games as originating from logical formulas. Indeed, an equivalent model for games can be given as follows: vertices in the game graph are not partitioned into Eve's and Adam's nodes, instead, we assign a boolean formula to each transition that determines an interaction between the two players. The outcome of this interaction is (1) the next vertex, and (2) the output colour of the acceptance condition. We can obtain a game of the kind we have defined in this paper by unfolding the boolean formulas of the transitions. There is a natural way to standardize such games: putting the boolean formulas in disjunctive normal form (DNF). Then, the unfolding of a game with formulas in DNF yields a game in which the partition into Eve-Adam nodes induces a bipartite graph with a particular structure: first, Adam chooses an uncoloured transition leading to a vertex controlled by Eve (with only one ingoing transition), and then Eve picks a transition producing some output colour.

We recall that a game is *suitable for transformations* if it verifies that for every edge $e = v \to v'$, if $v$ is controlled by Adam, then $e$ is uncoloured ($\gamma(e) = \varepsilon$), $v' \in V_{\text{Eve}}$, and $e$ is the only incoming edge to $v'$ ($\text{In}(v') = \{e\}$).

Games in this form have an asymmetric structure that makes them suitable for any type of transformation. As any pair of consecutive transitions are of the form $v \xrightarrow{\varepsilon} \tilde{v} \xrightarrow{c} v'$, with $\tilde{v} \in V_{\text{Eve}}$, we can force it so that if a decision needs to be made in a product, Eve is the one who makes it.
**LEMMA B.1.** For every game $\mathcal{G}$ with vertices $V$ and edges $E$, there exists a game $\tilde{\mathcal{G}}$ that is suitable for transformations, of size $|\tilde{\mathcal{G}}| = O(|E|)$, and equivalent to $\mathcal{G}$ in the following sense: there is an injective function $f: V \to \tilde{V}$ such that Eve wins $\mathcal{G}$ from $v$ if and only if she wins $\tilde{\mathcal{G}}$ from $f(v)$.

**PROOF.** We define $\tilde{\mathcal{G}}$ as follows. We let its set of vertices be $\tilde{V} = V \cup E$. Vertices of the form $v \in V$ will correspond to vertices coming from $\mathcal{G}$, and vertices $e \in E$ will be intermediate vertices added to force the suitability for transformations property. We let $\tilde{V}_{\text{Adam}} = V_{\text{Adam}}$ and $\tilde{V}_{\text{Eve}} = V_{\text{Eve}} \cup E$. If $e = v \xrightarrow{c} v'$ is an edge in $\mathcal{G}$, we add the edges $v \xrightarrow{\epsilon} e$ and $e \xrightarrow{c} v'$ to $\mathcal{G}'$. It is clear that $\tilde{\mathcal{G}}$ is suitable for transformations and that Eve wins $\mathcal{G}$ from $v$ if and only if she wins $\tilde{\mathcal{G}}$ from $v$. ■

**ACD-HD-Rabin-transform-for-games.** As discussed in Section 5.3, the ACD-HD-Rabin-transform of a game $\mathcal{G}$ does not always induce an HD-for-games mapping $\varphi: \text{ACD}_{\text{Rabin}}(\mathcal{G}) \to \mathcal{G}$, and $\mathcal{G}$ and $\text{ACD}_{\text{Rabin}}(\mathcal{G})$ do not necessarily have the same winner. This is to be expected, as the ACD-HD-Rabin-transform does not take into account the partition into Eve and Adam nodes. In this paragraph we propose a small modification on the transformation to obtain a correct transformation for games.

Let $\mathcal{G}$ be a game. If there is an edge $v \to v'$ with $v \in V_{\text{Adam}}$, we say that $v'$ is an A-succesor. We remark that if $\mathcal{G}$ is suitable for transformations, an A-succesor is controlled by Eve and has a unique predecessor. We let $V_{\text{A-succ}}$ be the set of A-successor of $\mathcal{G}$ and $V_{\text{normal}} = V \setminus V_{\text{A-succ}}$. If $\mathcal{G}$ is suitable for transformations, for each $v \in V_{\text{A-succ}}$ we let $\text{pred}(v)$ be its unique predecessor.

The idea to define the ACD-HD-Rabin-transform-for-games $\text{ACD}_{\text{parity}}^{\text{game}}(\mathcal{G})$ is the following: starting from the regular ACD-HD-Rabin-transform $\text{ACD}_{\text{Rabin}}(\mathcal{G})$, we make some local changes to vertices that are A-successors. First, if $v \in V_{\text{Adam}}$, we replace edges of the form $(v, x) \xrightarrow{n} (v', x')$ in $\text{ACD}_{\text{Rabin}}(\mathcal{G})$ by $(v, x) \xrightarrow{\epsilon} (v', x)$ (we forbid Adam to choose how to update the ACD-component). If such an edge is followed by $(v', x') \xrightarrow{n'} (v'', x'')$ in $\text{ACD}_{\text{Rabin}}(\mathcal{G})$, then we add $(v', x) \xrightarrow{n} (v'', x'')$ to $\text{ACD}_{\text{parity}}^{\text{game}}(\mathcal{G})$ (we note that $v' \in V_{\text{Eve}}$). That is, Eve chooses retroactively how to update the ACD-components performing two consecutive updates. We note that the node $n'$ is not output in the new game; this is not a problem, since $n$ must be an ancestor of $n'$ (we could say that $n$ contains more information regarding the acceptance condition).

**REMARK B.2.** Let $\mathcal{G}$ be a game suitable for transformations, let $v \in V_{\text{Adam}}$ and $v \xrightarrow{e_1} v' \xrightarrow{e_2} v''$ be a path of size 2 in $\mathcal{G}$ from $v$. It holds:

- If some cycle $\ell$ contains $e_2$, it also contains $e_1$.

- $\mathcal{T}_{v'}$ is a subtree of $\mathcal{T}_{v}$.

- Let $n_1 \in \text{Leaves}(\mathcal{T}_v)$ and $n_2 = \text{Jump}_{\mathcal{T}_{v'}}(n_1, \text{Supp}(n_1, e_1))$. Then, $\text{Supp}(n_2, e_2)$ is a descendant of $\text{Supp}(n_1, e_1)$ in $\mathcal{T}_{v'}$.

**DEFINITION B.3 (ACD-HD-Rabin-transform-for-games).** Let $\mathcal{G}$ be a Muller game suitable for transformations. For each vertex $v \in V$ we let $\eta_v: \text{Leaves}(\mathcal{T}_v) \to \{1, \dots, \text{rbw}(\mathcal{T}_v)\}$ be a mapping
satisfying Property (⋆) from Lemma 4.42. We define the ACD-HD-Rabin-transform-for-games of $\mathcal{G}$ to be the Rabin transition system ACD<sub>parity</sub><sup>game</sup>($\mathcal{G}$) defined as follows.

**Vertices.** The set of vertices is

$$ \tilde{V} = \bigcup_{v \in V_{\text{normal}}} \{v\} \times [1, \text{rbw}(\mathcal{T}_v)] \cup \bigcup_{v \in V_{\text{A-succ}}} \{v\} \times [1, \text{rbw}(\mathcal{T}_{\text{pred}(v)}). $$

**Players partition.** A vertex $(v, x)$ belongs to Eve if and only if $v$ belongs to Eve in $\mathcal{G}$.

**Initial vertices.** $\tilde{I} = \{(v_0, x) | v_0 \in I \text{ and } x \in \{1, \dots, \text{rbw}(\mathcal{T}_{v_0})\}\}$.

**Edges and output colours.** Let $e = v \to v'$ in $\mathcal{G}$.

— If $v \in V_{\text{Eve}} \cap V_{\text{normal}}$, we add $(v, x) \xrightarrow{n} (v', x')$ to ACD<sub>parity</sub><sup>game</sup>($\mathcal{G}$) exactly in the same cases as in the regular ACD-HD-Rabin-transform.

— If $v \in V_{\text{Adam}}$, we let $(v, x) \xrightarrow{\varepsilon} (v', x)$ in $\tilde{E}$ for each $x \in \{1, \dots, \text{rbw}(\mathcal{T}_v)\}$.

— If $v \in V_{\text{A-succ}}$, we add $(v, x) \xrightarrow{n} (v', x')$ to ACD<sub>parity</sub><sup>game</sup>($\mathcal{G}$) if in the regular ACD-HD-Rabin-transform there is a path of size 2 of the form

$$ (\text{pred}(v), x) \xrightarrow{n} (v, \tilde{x}) \xrightarrow{\tilde{n}} (v', x'). $$

Formally,

$$ \tilde{E} = \bigcup_{\substack{e=v \to v' \in E \\ v \in V_{\text{normal}}}} \{e\} \times \text{Leaves}(\mathcal{T}_v) \cup \bigcup_{\substack{e=v \to v' \in E \\ v \in V_{\text{A-succ}}}} \{e\} \times \text{Leaves}(\mathcal{T}_{\text{pred}(v)}). $$

**Rabin condition.** $R = \{(G_n, R_n)\}_{n \in \text{Nodes}(\mathcal{A}C\mathcal{D}_{\mathcal{T}_S})}$, where $G_n$ and $R_n$ are defined as follows: Let $n$ be a round node, and let $n'$ be any node in $\text{Nodes}(\mathcal{A}C\mathcal{D}_{\mathcal{T}_S})$,

$$ \left\{ \begin{array}{ll} n' \in G_n & \text{if } n' = n, \\ n' \in R_n & \text{if } n' \neq n \text{ and } n \text{ is not an ancestor of } n'. \end{array} \right. $$

## Correctness of the ACD-HD-Rabin-transform-for-games

**PROPOSITION 5.32 (Correctness of the ACD-HD-Rabin-transform-for-games).** Let $\mathcal{G}$ be a Muller game suitable for transformations, and let ACD<sub>parity</sub><sup>game</sup>($\mathcal{G}$) be its ACD-HD-Rabin-transform-for-games. Then, there is an HD-for-games mapping $\varphi: \text{ACD}_{\text{parity}}^{\text{game}}(\mathcal{G}) \to \mathcal{T}_S$.

**PROOF.** The proof is analogous to that of the correctness of the usual ACD-HD-Rabin-transform (Proposition 5.28). We define the mapping $\varphi: \text{ACD}_{\text{parity}}^{\text{game}}(\mathcal{G}) \to \mathcal{G}$ as $\varphi_V(v, x) = v$ and $\varphi_E(e, l) = e$. It is clear that it is a weak morphism, and it preserve accepting runs by Lemma 5.29 and Remark B.2.

We define a resolver $(r_0, r)$ simulating $\varphi$ similarly to the proof of Proposition 5.28: We use ACD<sub>parity</sub>($\mathcal{G}$) to guide the resolver. Let $\rho = v_0 \to v_1 re \dots$ be a run in $\mathcal{G}$, and let $(v_0, l_0) \to (v_1, l_1) \to \dots$ be the preimage of this run in ACD<sub>parity</sub>($\mathcal{G}$). We simulate $\rho$ in ACD<sub>parity</sub><sup>game</sup>($\mathcal{G}$) as
follows: We ensure that at every moment $i$, if $v_i \notin V_{A-succ}$, the current vertex $(v_i, x_i)$ is such that $x_i = \eta_{v_i}(l_i)$. There distinguish two cases to simulate the edge $e_i = v_i \to v_{i+1}$:

- If $v_i \in V_{Adam}$, there is a single outgoing edge from $(v_i, x_i)$ mapped to the edge $v_i \to v_{i+1}$ in $\rho: (v_i, x_i) \xrightarrow{\epsilon} (v_{i+1}, x_i)$. This must be the edge picked by the resolver

- If $v_i \in V_{Eve}$, we pick the edge $(v_i, x_i) \xrightarrow{n_i} (v_{i+1}, x_{i+1})$ such that $x_{i+1} = \eta_{l_{i+1}}$ and $n_i = \text{Supp}(l_i, e_i)$.

If $v_i \in V_{A-succ}$, the vertex $(v_i, x_i)$ will verify $x_i = x_{i-1} = \eta_{v_i}(l_i)$. In this case, we pick the edge $(v_i, x_i) \xrightarrow{n_i} (v_{i+1}, x_{i+1})$ such that $x_{i+1} = \eta_{l_{i+1}}$ and $n_i = \text{Supp}(l_i, e_i)$. This is indeed an edge appearing in $\text{ACD}_{\text{parity}}^{\text{game}}(G)$, as the path $(v_{i-1}, x_{i-1}) \xrightarrow{n'_{i-1}} (v_i, x'_i) \xrightarrow{n_i} (v_{i+1}, x_{i+1})$ exists in the regular $\text{ACD}_{\text{Rabin}}(G)$, with $x'_i = \eta_{v_i}(l_i)$.

The resolver obtained in this way is sound for $\text{ACD}_{\text{parity}}^{\text{game}}(G)$, as there is a unique way to simulate edges issued from Adam vertices, and the rest of the edges are simulated in the same way as the resolver defined for the regular ACD-HD-Rabin-transform, which we proved to be sound. ■

## Optimality of the ACD-HD-Rabin-transform-for-games

**COROLLARY 5.37.** Let $G$ be a Muller game suitable for transformations whose states are accessible and let $\tilde{G}$ be a Rabin game. If $\tilde{G}$ admits an HD-for-games mapping $\varphi: \tilde{G} \to G$, then, $|\text{ACD}_{\text{parity}}^{\text{game}}(G)| \le 2|\tilde{G}|$.

**PROOF.** The vertices of $\text{ACD}_{\text{parity}}^{\text{game}}(G)$ corresponding to vertices in $V_{\text{normal}}$ are exactly the same that those in $\text{ACD}_{\text{Rabin}}(G)$:

$$ \{(v, x) \in \text{ACD}_{\text{parity}}^{\text{game}}(G) \mid v \in V_{\text{normal}}\} = \{(v, x) \in \text{ACD}_{\text{Rabin}}(G) \mid v \in V_{\text{normal}}\}. $$

Moreover, for $v \in V_{A-succ}$, there is one vertex of the form $(v, x)$ for each vertex $(\text{pred}(v), x)$, and each $v \in V_{A-succ}$ has exactly one predecessor in $V_{\text{normal}}$, so we conclude that:

$$ |\text{ACD}_{\text{parity}}^{\text{game}}(G)| \le 2 \cdot |\{(v, x) \in \text{ACD}_{\text{parity}}^{\text{game}}(G) \mid v \in V_{\text{normal}}\}| \le 2 \cdot |\text{ACD}_{\text{Rabin}}(G)| \le 2 \cdot G', $$

where the last inequality follows from Theorem 5.36. ■

## C. Simplifications for prefix-independent conditions

We prove in this appendix results applying to automata recognising prefix-independent languages and games using prefix-independent winning conditions. We recall that a language $L \subseteq \Sigma^\omega$ is prefix-independent if for all $w \in \Sigma^\omega$ and $u \in \Sigma^*$, $uw \in L$ if and only if $w \in L$.

**LEMMA 2.5.** Let $\mathcal{A}$ be a history-deterministic automaton recognising a prefix-independent language and using as acceptance set a prefix-independent language. For any state $q$ of $\mathcal{A}$ that
is reachable using some sound resolver, it holds that $\mathcal{A}$ recognises the same language if we fix $q$ as initial state, that is, $\mathcal{L}(\mathcal{A}) = \mathcal{L}(\mathcal{A}_q)$. Moreover, $\mathcal{A}_q$ is also history-deterministic. In particular, if $\mathcal{A}$ is deterministic, this is the case for any reachable state $q$.

**PROOF.** Let $(r_0, r)$ be a sound resolver for $\mathcal{A}$ such that $q$ is reachable using $(r_0, r)$ (there is a word $w_0 \in \Sigma^*$ and a run $\rho_0 = r_0 \stackrel{w_0}{\rightleftharpoons}$ $q$ induced by $r$ over $w$). We first show that $\mathcal{L}(\mathcal{A}_q) \subseteq \mathcal{L}(\mathcal{A})$. Let $w \in \Sigma^\omega$ be a word accepted from $q$. Then, $w_0w$ admits an accepting run from the original initial state (by prefix-independence of the acceptance set), so $w_0w \in \mathcal{L}(\mathcal{A})$, and by the prefix-independence of $\mathcal{L}(\mathcal{A})$, $w \in \mathcal{L}(\mathcal{A})$ too.

For the converse direction, we define a sound resolver $(r'_0, r')$ for $\mathcal{A}_q$. We let $r'_0 = q$, and $r'(\rho, a) = r(\rho_0\rho, a)$ be the strategy that acts as the resolver $r$ assuming that $\rho_0$ has happened in the past. It is clear that for every word $w \in \Sigma^\omega$, the run induced by $(r'_0, r')$ over $w$ has a common suffix with the run induced by $(r_0, r)$ over $w_0w$. Therefore, by the prefix-independence assumptions:

$$ w \in \mathcal{L}(\mathcal{A}) \iff w_0w \text{ is accepted using } (r_0, r) \iff w_0w \text{ is accepted using } (r'_0, r'). \blacksquare $$

**LEMMA 3.14.** Let $\mathcal{T}S$ and $\mathcal{T}S'$ be two $\mathcal{T}S$ such that all their states are accessible, and let $\varphi: \mathcal{T}S \to \mathcal{T}S'$ be an HD (resp. HD-for-games) mapping between them. If $\mathcal{W}$ and $\mathcal{W}'$ are prefix-independent, the mapping $\varphi$ is also HD (resp. HD-for-games) when considered between the transition systems $\mathcal{T}S_V$ and $\mathcal{T}S'_{V'}$, consisting of the transition systems $\mathcal{T}S$ and $\mathcal{T}S'$ where all the states are set to be initial.

**PROOF.** First, $\varphi: \mathcal{T}S_V \to \mathcal{T}S'_{V'}$ is trivially a weak morphism. We claim that it preserves accepting runs. Let $v \in V$ be a state in $\mathcal{T}S$ and let $\rho = v \stackrel{w}{\rightleftharpoons}$ be an accepting run from $v$. Since all the states are reachable, there is some $v_0 \in I$ and finite run $\rho_v = v_0 \stackrel{u}{\rightleftharpoons} v$. Since $\varphi$ is a weak morphism we have that $\varphi_{\mathcal{R}uns}(\rho_v\rho) = \varphi(v_0) \stackrel{u'}{\rightleftharpoons} \varphi(v) \stackrel{w'}{\rightleftharpoons}$. It holds that:

$$ w \in \mathcal{W} \stackrel{\mathcal{W}}{\Rightarrow} uw \in \mathcal{W} \Rightarrow u'w' \in \mathcal{W}' \stackrel{\mathcal{W}'}{\Rightarrow} w' \in \mathcal{W}', $$

where the central implication follows from the fact that $\varphi$ preserves accepting runs between $\mathcal{T}S$ and $\mathcal{T}S'$. Therefore $\varphi_{\mathcal{R}uns}(\rho)$ is also an accepting run.

In the rest of the proof we assume that $\varphi$ is an HD-for-games mapping, (which covers the HD case). Let $(r_{\text{Init}}, r)$ be a resolver sound for $\mathcal{T}S$ simulating $\varphi: \mathcal{T}S \to \mathcal{T}S'$. We define a resolver $(\tilde{r}_{\text{Init}}, \tilde{r})$ for the new mapping. For every state $v$ of $\mathcal{T}S$, we fix a finite run $\rho_v \in \text{Path}_I^{\text{fin}}(\mathcal{T}S)$ ending in $v$ that is consistent with $(r_{\text{Init}}, r)$ over some $\rho'$, if such a run exists. We let $V_{\text{Reach}} \subseteq V$ be the set of vertices for which $\rho_v$ is well-defined. We note that for each $v' \in V'$ there exists at least one $v \in \varphi^{-1}(v')$ such that $v \in V_{\text{Reach}}$; indeed, if $\rho'_{v'}$ is a finite run reaching $v'$ in $\mathcal{T}S'$, one such $v$ is Target$(r_{\mathcal{R}uns}(\rho'_{v'}))$ (that is, the vertex to which we arrive in $\mathcal{T}S$ when simulating $\rho'_{v'}$ via the original resolver). We let $\tilde{r}_{\text{Init}}(v')$ be this vertex. If $e' \in \text{Out}(v')$ is an edge in $\mathcal{T}S'$, we let
$\tilde{r}(\epsilon, e') = r(\rho_v, e')$, for $v = \tilde{r}_{\text{Init}}(v')$. For $\rho$ a non-empty finite run starting in $v \in V_{\text{Reach}}$ and $e' \in E'$, we define $\tilde{r}(\rho, e') = r(\rho_v\rho, e')$. If $\rho$ starts in $v \notin V_{\text{Reach}}$ we let $\tilde{r}(\rho, e')$ be any edge in $\phi^{-1}(e')$ (if $e' \in \text{Out}(\phi(\text{Target}(\rho)))$ we pick it in $\text{Out}(\text{Target}(\rho)))$. We check that $(\tilde{r}_{\text{Init}}, \tilde{r})$ satisfies the four requirements to be a resolver:

1. $\tilde{r}_{\text{Init}}(v')$ has been chosen in $\phi^{-1}(v')$.

2. $\tilde{r}(e')$ is chosen in $\phi^{-1}(e')$.

3. Let $e' \in \text{Out}(v')$. We have defined $\tilde{r}(\epsilon, e') = r(\rho_v, e')$, where $\rho_v$ is a finite run consistent with $r$ ending in $v = r_{\text{Init}}(v')$. By Property 4 of a resolver, $r(\rho_v, e') \in \text{Out}(v)$.

4. Let $\rho = v_0 \rightsquigarrow v \in \mathcal{R}un^{\text{fin}}(\mathcal{T}S_v)$ and $e' \in \text{Out}(\phi(v))$. If $v_0 \notin V_{\text{Reach}}$, then we have picked $\tilde{r}(\rho, e')$ in $\text{Out}(v)$. If $v_0 \in V_{\text{Reach}}$, then $\tilde{r}(\rho, e') = r(\rho_{v_0}\rho, e')$; as $\rho_{v_0}\rho$ is a run ending in $v$ and $r$ verifies Property 4 of a resolver $r(\rho_{v_0}\rho, e') \in \text{Out}(v)$.

Finally, we show that $(\tilde{r}_{\text{Init}}, \tilde{r})$ is sound for $\mathcal{T}S$. Let $\rho' = v' \rightsquigarrow w' \in \mathcal{R}un(\mathcal{T}S'_{v'})$ be an accepting run, and let $\rho = v \rightsquigarrow w$ be a run consistent with $(\tilde{r}_{\text{Init}}, \tilde{r})$ over $\rho'$. In particular, $v = \tilde{r}_{\text{Init}}(v')$. Let $\rho_v = v_0 \rightsquigarrow v$ be the chosen run reaching $v$ and let $\rho'_v = v'_0 \rightsquigarrow v'$ be a finite run in $\mathcal{R}un^{\text{fin}}(\mathcal{T}S')$ such that $\rho_v$ is consistent with $(r_{\text{Init}}, r)$ over $\rho'_v$. It is immediate to check that $\rho_v\rho$ is consistent with $(r_{\text{Init}}, r)$ over $\rho'_v\rho'$. Since $\rho'$ is accepting, we have that $w' \in \mathcal{W}'$, and by prefix-independence of the acceptance sets and the fact that $\rho_v\rho$ is accepting if $\rho'_v\rho'$ is, we have:

$$w' \in \mathcal{W}' \implies u'w' \in \mathcal{W}' \implies uw \in \mathcal{W} \implies w \in \mathcal{W},$$

so we conclude that $\rho$ is accepting in $\mathcal{T}S$, as we wanted to show. ■

<figure><img src="image_45.png" /></figure>

## D. Simplifying automata with duplicated edges

Given an automaton $\mathcal{A} = (Q, \Sigma, I, \Gamma, \delta, \mathcal{W})$ we say that it has duplicated edges if there is some pair of states $q, q' \in Q$ and two different transitions between them labelled with the same input letter: $q \xrightarrow{a:\alpha} q'$, $q \xrightarrow{a:\beta} q'$.

As commented in Remark 4.47, the construction of the ZT-HD-Rabin-automaton we have presented potentially introduces duplicated edges, which can be seen as an undesirable property (even if some automata models such as the HOA format [4] allow them). We show next that we can always derive an equivalent automaton without duplicated edges. Intuitively, in the Rabin case, if we want to merge two transitions having as output letters $\alpha$ and $\beta$, we add a fresh letter $(\alpha\beta)$ to label the new transition. For each Rabin pair, this new letter will simulate the best of either $\alpha$ or $\beta$ depending upon the situation.

**PROPOSITION D.1 (Simplification of automata).** Let $\mathcal{A}$ be a Muller (resp. Rabin) automaton presenting duplicated edges. There exists a Muller (resp. Rabin) automaton $\mathcal{A}'$ on the same set of states without duplicated edges such that $\mathcal{L}(\mathcal{A}) = \mathcal{L}(\mathcal{A}')$. Moreover, if $\mathcal{A}$ is history-
deterministic, $\mathcal{A}'$ can be chosen history-deterministic. In the Rabin case, the number of Rabin
pairs is also preserved.

**PROOF.** For the Rabin case, let $\mathcal{A}'$ be an automaton that is otherwise as $\mathcal{A}$ except that instead of the transitions $\Delta$ of $\mathcal{A}$ it only has one $a$-transition $q \xrightarrow{a:x} q' \in \Delta'$ (with a fresh colour $x$ per transition) per state-pair $q, q'$ and letter $a \in \Sigma$. That is, $\Delta' = \{(q, a, x_j, q') : (q, a, y, q') \in \Delta$ for some $y\}$. The new Rabin condition $\{(G'_1, R'_1), \dots, (G'_r, R'_r)\}$ is defined as follows. For each transition $q \xrightarrow{a:x} q'$:

- $x \in G'_i$ if $q \xrightarrow{a:y} q' \in \Delta$ for some $y \in G_i$,

- $x \in R'_i$ if for all $q \xrightarrow{a:y} q' \in \Delta$, $y \in R_i$.

We claim that $\mathcal{L}(\mathcal{A}') = \mathcal{L}(\mathcal{A})$. Indeed, if $u \in \mathcal{L}(\mathcal{A})$, as witnessed by some run $\rho$ and a Rabin pair $(G_i, R_i)$, then the corresponding run $\rho'$ in $\mathcal{A}'$ over $u$ is also accepted by the Rabin pair $(G'_i, R'_i)$: the transitions of $\mathrm{Inf}(\rho) \cap G_i$ induce transitions of $\mathrm{Inf}(\rho') \cap G'_i$ and the fact that $\mathrm{Inf}(\rho) \cap R_i = \emptyset$ guarantees that $\mathrm{Inf}(\rho') \cap R'_i = \emptyset$.

Conversely, if $u \in \mathcal{L}(\mathcal{A}')$ as witnessed by a run $\rho'$ and Rabin pair $(G'_i, R'_i)$, then there is an accepting run $\rho$ over $u$ in $\mathcal{A}$: such a run can be obtained by choosing for each transition $q \xrightarrow{a:x} q'$ of $\rho'$ where $x \in G'_i$ a transition $q \xrightarrow{a:y} q' \in \Delta$ such that $y \in G_i$, which exists by definition of $\mathcal{A}'$, for each transition $q \xrightarrow{a:x} q'$ where $x \notin G_i \cup R_i$ a transition $q \xrightarrow{q,y} q' \in \Delta$ such that $y \notin R_i$, which also exists by definition of $\mathcal{A}'$, and for other transitions $q \xrightarrow{a:x} q'$ (that is, those for which $x \in R'_i$) an arbitrary transition $q \xrightarrow{a:y} q' \in \Delta$. Since $\rho'$ is accepting, we have $\mathrm{Inf}(\rho') \cap G_i \neq \emptyset$ and $\mathrm{Inf}(\rho) \cap R_i = \emptyset$, that is, $\rho$ is also accepting.

For the Muller case, the argument is even simpler. As above, we consider $\mathcal{A}'$ that is otherwise like $\mathcal{A}$ except that instead of the transitions $\Delta$ of $\mathcal{A}$, it only has one $a$-transition $q \xrightarrow{a:x} q' \in \Delta'$ (with a fresh colour per transition) per state-pair $q, q'$ and the accepting condition is defined as follows. A set of transitions $T$ is accepting if and only if for each $t = q \xrightarrow{a:x} q' \in T$ there is a non-empty set $S_t \subseteq \{q \xrightarrow{a:y} q' \in \Delta\}$ such that $\cup_{t \in T} S_t$ is accepting in $\mathcal{A}$. In other words, a set of transitions in $\mathcal{A}'$ is accepting if for each transition we can choose a non-empty subset of the original transitions in $\mathcal{A}$ that form an accepting run in $\mathcal{A}$.

We claim that $\mathcal{L}(\mathcal{A}') = \mathcal{L}(\mathcal{A})$. Indeed if $u \in \mathcal{L}(\mathcal{A})$, as witnessed by some run $\rho$, the run $\rho'$ that visits the same sequence of states in $\mathcal{A}'$ is accepting as witnessed by the transitions that occur infinitely often in $\rho$.

Conversely, assume $u \in \mathcal{L}(\mathcal{A}')$, as witnessed by a run $\rho'$ and a non-empty subset $S_t$ for each transition $t$ that occurs infinitely often in $\rho'$ such that $\cup_{t \in \mathrm{Inf}(\rho')} S_t$ is accepting in $\mathcal{A}$. Then there is an accepting run $\rho$ over $u$ in $\mathcal{A}$ that visits the same sequence of states as $\rho'$ and chooses instead of a transition $t \in \mathrm{Inf}(\rho)$ each transition in $S_t$ infinitely often, and otherwise takes an arbitrary transition. The set of transitions $\rho$ visits infinitely often is exactly $\cup_{t \in \mathrm{Inf}(\rho)} S_t$, and is therefore accepting.
Finally, observe that in both cases, if $\mathcal{A}$ is HD, then the automaton $\mathcal{A}'$ without duplicate edges is also HD since $\mathcal{A}'$ is obtained from $\mathcal{A}$ by merging transitions. Indeed, the resolver $r$ of $\mathcal{A}$ induces a resolver $r'$ for $\mathcal{A}'$ by outputting the unique transition with the same letter and state-pair as $r$. By the same argument as above, the run induced by $r'$ is accepting if and only if the run induced by $r$ is. ■

**EXAMPLE D.2.** The ZT-HD-Rabin-automaton from Figure 14 has duplicated transitions. In Figure 19 we present an equivalent HD Rabin automaton without duplicates. For this, we have merged the self-loops in state 1 labelled with $a$ and $b$ respectively. We have added the output colours $(\alpha\beta)$ and $(\theta\xi)$. The new Rabin pairs are given by:

$$G'_{\beta} = \{\beta, (\alpha\beta)\}, \quad R'_{\beta} = \{\alpha, \lambda, \xi, \zeta\},$$

$$G'_{\lambda} = \{\lambda\}, \quad R'_{\lambda} = \{\alpha, \beta, (\alpha\beta), \theta\}.$$

<figure><img src="image_46.png" /><figcaption>**Figure 19.** The simplified ZT-HD-Rabin-automaton.</figcaption></figure>

<figure><img src="image_47.png" /></figure>

## E. Proofs for Section 6.1.1

**PROOF OF PROPOSITIONS 6.2 AND 6.3.** We prove it for the Rabin case, Streett conditions being the dual notion.

If all round nodes of $\mathcal{Z}_F = (N = N_\circ \sqcup N_\square, \leq, v: N \to 2_+^\Gamma)$ have at most one child, we define a family of Rabin pairs $R = \{(G_n, R_n) | n \in N_\circ\}$ such that $\text{Rabin}(R) = \text{Muller}(F)$ as follows: for each round node $n \in N_\circ$, we add a Rabin pair $(G_n, R_n)$. We let $G_n = \Gamma \setminus v(n)$. In order to define $R_n$, we observe that $n$ has at most one child $n'$, and we define $R_n = v(n) \setminus v(n')$, for $n'$ the only child of $n$, if it exists, or $R_n = v(n)$ if $n$ has no children at all. This is, the pair $(G_n, R_n)$ accepts the sets of colours $A \subseteq \Gamma$ that contain some of the colours that disappear in the step $n \to n'$ and none of the colours appearing up in the tree. We show that $\text{Rabin}(R) = \text{Muller}(F)$. Let $A$ be a set of colours. If $A \in F$, let $n$ be a maximal node (for $\leq$) containing $A$. It is a round node and there is some colour $c \in A$ not appearing in the only child of $n$. Therefore, $c \in G_n$ and $A \cap R_n = \emptyset$. Conversely, if $A \notin F$, then for every round node $n$ with a child $n'$, either $A \subseteq v(n')$ (and therefore $A \cap G_n = \emptyset$) or $A \not\subseteq v(n)$ (and in that case $A \cap R_n \neq \emptyset$).
We remark that this construction uses more Rabin pairs than necessary, since we could
reuse Rabin pairs for nodes that are in the same level and that are not siblings.

Conversely, suppose that Muller($\mathcal{F}$) = Rabin($R$) for the Rabin language associated to $R = \{(G_1, R_1), \dots, (G_r, R_r)\}$. If $n \in \mathcal{Z}_{\mathcal{F}}$ is a round node ($A = v(n) \in \mathcal{F}$), then its label $A$ contains some colours that belongs to $G_{i_1}, \dots, G_{i_k}$ and none belonging to $R_{i_1}, \dots, R_{i_k}$ for some $i_1, \dots, i_k, k \ge 1$. A child of $n$ must not have these colours, so the only maximal subset of $A$ that is not in $\mathcal{F}$ is $A \setminus (G_{i_1} \cup \dots \cup G_{i_k})$. ■

**PROOF OF PROPOSITION 6.4.** We assume $\Gamma \in \mathcal{F}$ ($\min_{\mathcal{F}} = 0$), the other case is symmetric.

Assume that $\mathcal{Z}_F$ has a single branch of length $\max_F + 1$. We define a mapping $\phi: \Gamma \to [0, \max_F]$ as follows: for each colour $c \in \Gamma$ we let $n_c$ be the deepest node in $\mathcal{Z}_F$ containing $c$, and we define $\phi(c) = v(n_c)$. It is easy to check that for all $w \in \Gamma^\omega$, $w \in \text{Muller}(\mathcal{F})$ if and only if $\phi(w) \in \text{parity}$.

Conversely, assume that we can assign colours to the elements of $\Gamma$ by $\phi : \Gamma \to [0, d]$, whose
corresponding parity language is Muller($\mathcal{F}$). We show that any node of the Zielonka tree $\mathcal{Z}_F$
has at most one child. Indeed, let $n \in N$ and let $c \in v(n)$ such that $\phi(c) = \min\{\phi(c) \mid c \in v(n)\}$.
We suppose that $\phi(c)$ is odd (the proof is symmetric for $\phi(c)$ even). Let $p = \min\{\phi(c') \mid c' \in v(n)$ and $\phi(c')$ even$\}$. In every child of $n$ the elements with a smaller colour than $p$ must
disappear, so the set of elements $v(n) \cap \{c \in \Gamma \mid \phi(c) \ge p\}$ is the only maximal subset of $v(n)$
belonging to $\mathcal{F}$. Moreover, in the label of the child of $n$ there is at least one colour less, so the
height of $\mathcal{Z}_F$ will be at most $d+1$. ■