# From Muller to Parity and Rabin Automata: Optimal Transformations Preserving (History-)Determinism

Antonio Casares, Thomas Colcombet, Nathanaël Fijalkow, Karoliina Lehtinen

► To cite this version:

Antonio Casares, Thomas Colcombet, Nathanaël Fijalkow, Karoliina Lehtinen. From Muller to Parity and Rabin Automata: Optimal Transformations Preserving (History-)Determinism. 2023. hal-04324130

HAL Id: hal-04324130

https://hal.science/hal-04324130v1

Preprint submitted on 5 Dec 2023

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

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

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
# From Muller to Parity and Rabin Automata:
Optimal Transformations Preserving
(History-)Determinism

Antonio Casares ☐

LaBRI, Université de Bordeaux, France

Thomas Colcombet ☐

CNRS, IRIF, Université Paris Cité, France

Nathanaël Fijalkow ☐

CNRS, LaBRI, Université de Bordeaux, France
MIMUW, University of Warsaw, Poland

Karoliina Lehtinen ☐

CNRS, Aix-Marseille Université, LIS, France

## Abstract

We study transformations of automata and games using Muller conditions into equivalent ones using parity or Rabin conditions. We present two transformations, one that turns a deterministic Muller automaton into an equivalent deterministic parity automaton, and another that provides an equivalent history-deterministic Rabin automaton. We show a strong optimality result: the obtained automata are minimal amongst those that can be derived from the original automaton by duplication of states. We introduce the notions of locally bijective morphisms and history-deterministic mappings to formalise the correctness and optimality of these transformations.

The proposed transformations are based on a novel structure, called the alternating cycle decomposition, inspired by and extending Zielonka trees. In addition to providing optimal transformations of automata, the alternating cycle decomposition offers fundamental information on their structure. We use this information to give crisp characterisations on the possibility of relabelling automata with different acceptance conditions and to perform a systematic study of a normal form for parity automata.

**2012 ACM Subject Classification** Theory of computation → Automata over infinite objects

**Keywords and phrases** Emerson-lei automata, good-for-games, paritizing, omega-regular languages.

**Related Version** Conference version [18]: https://drops.dagstuhl.de/opus/volltexte/2021/14192/
We incorporate results from [19]: https://drops.dagstuhl.de/opus/volltexte/2022/16458/

**Funding** Thomas Colcombet: Supported by the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation programme (grant agreement No.670624) – DuaLL – and the DeLTA ANR project (ANR-16-CE40-0007).

**Acknowledgements** We want to thank Klara J. Meyer and Salomon Sickert for their comments and for spotting a mistake in a previous version. We also thank Alexandre Duret-Lutz and Florian Renkin for stimulating discussions around the alternating cycle decomposition, and Corto Mascle for his valuable suggestions about the presentation of this paper.

This document contains hyperlinks. Each occurrence of a notion is linked to its *definition*. On an electronic device, the reader can click on words or symbols (or just hover over them on some PDF readers) to see their definition.
# Contents

<table><tr><td>1 Introduction</td><td>3</td></tr><tr><td>2 Preliminaries</td><td>8</td></tr><tr><td>2.1 Transition systems, automata and games</td><td>9</td></tr><tr><td>2.2 Muller languages, cycles and the parity hierarchy</td><td>14</td></tr><tr><td>2.3 Trees</td><td>18</td></tr><tr><td>3 Morphisms as witnesses of transformations</td><td>19</td></tr><tr><td>3.1 Morphisms of transition systems</td><td>19</td></tr><tr><td>3.2 Local properties of morphisms</td><td>20</td></tr><tr><td>3.3 History-deterministic mappings</td><td>21</td></tr><tr><td>3.4 Preservation of semantic properties of automata and games</td><td>26</td></tr><tr><td>4 The Zielonka tree: An optimal approach to Muller languages</td><td>29</td></tr><tr><td>4.1 The Zielonka tree</td><td>30</td></tr><tr><td>4.2 A minimal deterministic parity automaton</td><td>31</td></tr><tr><td>4.2.1 The Zielonka-tree-parity-automaton</td><td>31</td></tr><tr><td>4.2.2 Optimality of the Zielonka-tree-parity-automaton</td><td>33</td></tr><tr><td>4.3 A minimal history-deterministic Rabin automaton</td><td>44</td></tr><tr><td>4.3.1 The Zielonka-tree-HD-Rabin-automaton</td><td>44</td></tr><tr><td>4.3.2 Optimality of the Zielonka-tree-HD-Rabin-automaton</td><td>48</td></tr><tr><td>5 The alternating cycle decomposition: An optimal approach to Muller transition systems</td><td>49</td></tr><tr><td>5.1 The alternating cycle decomposition</td><td>49</td></tr><tr><td>5.2 An optimal transformation to parity transition systems</td><td>52</td></tr><tr><td>5.3 An optimal history-deterministic transformation to Rabin transition systems</td><td>56</td></tr><tr><td>5.4 Optimality of the ACD-transforms</td><td>59</td></tr><tr><td>5.4.1 Statements of the optimality results</td><td>59</td></tr><tr><td>5.4.2 Discussion</td><td>59</td></tr><tr><td>5.4.3 Optimality of the parity condition of ACD<sub>parity</sub>(TS)</td><td>60</td></tr><tr><td>5.4.4 Optimality of the sizes of ACD<sub>parity</sub>(TS) and ACD<sub>Rabin</sub>(TS)</td><td>63</td></tr><tr><td>6 Corollaries</td><td>65</td></tr><tr><td>6.1 Typeness results</td><td>65</td></tr><tr><td>6.1.1 Typeness for Muller languages</td><td>65</td></tr><tr><td>6.1.2 Typeness for Muller transition systems and deterministic automata</td><td>66</td></tr><tr><td>6.2 A normal form for parity transition systems</td><td>70</td></tr><tr><td>6.3 Minimisation of deterministic parity automata recognising Muller languages</td><td>74</td></tr><tr><td>7 Conclusion</td><td>76</td></tr><tr><td>A Generalised classes of acceptance conditions</td><td>82</td></tr><tr><td>B Transformations for games</td><td>85</td></tr><tr><td>C Simplifications for prefix-independent conditions</td><td>88</td></tr><tr><td>D Simplifying automata with duplicated edges</td><td>90</td></tr><tr><td>E Proofs for Section 6.1.1</td><td>91</td></tr></table>
# 1 Introduction

## Context

**Games and automata for LTL synthesis.** Games and automata over infinite words form the theoretical basis for the verification and synthesis of reactive systems; we refer to chapters 2, 4, and 27 of the recent Handbook of Model Checking [68, 50, 3] for a broad exposition of this research area. A milestone objective is the synthesis of reactive systems with specifications given in *Linear Temporal Logic* (LTL). The original approach of Pnueli and Rosner [69] using automata and games devised more than four decades ago is still at the heart of the state of the art synthesis tools [33, 55, 61, 63]. The limiting factor in this method is the transformation of the LTL formula to a deterministic parity automaton. This automaton is then used to build a game, and a controller for the reactive system can be obtained from a winning strategy for this game. Most solutions to this problem (including the top-ranked tools in the SyntComp competitions [42], Strix [55, 60] and ltlsynt [61]) first construct a Muller (or Emerson-Lei) automaton, and then transform it into an equivalent parity automaton. The use of an intermediate Muller automaton is also present (although sometimes implicitly) in the most recent improvements in the determinisation of Büchi automata towards deterministic parity automata [54, 67, 73]. For this reason, understanding transformations of Muller automata and finding efficient procedures for it is of great importance.

**Which are the simplest acceptance conditions?** There exist multiple kinds of acceptance conditions that are commonly employed by $\omega$-automata (Büchi, Rabin, Muller...). The use of parity conditions for LTL synthesis is justified by both practical and theoretical reasons. Firstly, there exist several high-performing algorithms solving parity games [26, 35, 53, 79], so the last step in the LTL synthesis method described above can be carried out smoothly, once the parity game is obtained. Contrarily, solving Muller games and Rabin games is, respectively, PSPACE-complete [41] and NP-complete [31]. From a theoretical point of view, parity conditions can be considered as the simplest family of conditions that can be used to recognise all $\omega$-regular languages with deterministic automata; it could even be argued that there is a canonical aspect to them:

- For every $\omega$-regular language $L$, the minimal number of output colours needed by deterministic Muller automata to recognise $L$ is attained with parity automata (Proposition 6.14). The optimal number of colours needed by a parity automaton to recognise a language $L$ reveals a fundamental information about it, called its parity index. This is a measure of the topological complexity of $L$ [77, 80].

- Parity languages are exactly Muller languages corresponding to families $\mathcal{F} \subseteq 2_+^\Gamma$ of subsets of colours such that both $\mathcal{F}$ and its complement are closed under union (Proposition 6.4).

- Parity languages are bipositional [30] (in a parity game, both players can play optimally using positional strategies, that is, strategies that use no memory). Moreover, over infinite game graphs, these are the only bipositional languages [24], and over finite game graphs, these are the unique bipositional Muller languages [81].

- Solving parity games is both in NP and co-NP [32].

However, these are not the only kind of conditions that deserve our attention. In this work, we further investigate transformations producing automata using a Rabin acceptance condition. Although in practice solvers for Rabin games are not as developed, Rabin languages are a natural choice and interesting from a theoretical point of view: they are exactly the half-positional Muller languages [81], there exists a correspondence between Rabin automata
and memory structures for Muller games [17, 19], and the determinisation of Büchi automata naturally produces Rabin automata [34, 72, 73].

**Transformations of games and automata.** There are various existing techniques to transform Muller automata or games into parity ones. The majority of these methods involve composing the input automaton $\mathcal{A}$ with a deterministic parity automaton recognising the acceptance condition used by $\mathcal{A}$. The first such parity automaton was introduced by Gurevich and Harrington in the 1980s [37] and is known as the Latest Appearance Record (LAR). Löding proved that the LAR is optimal in the worst case [56]: there exists a family of Muller languages $L_i$ for which the LAR is minimal amongst deterministic parity automata recognising $L_i$. However, the LAR is far from being minimal in every case, as it only uses the information about the size of the alphabet. Since its introduction, many refinements of the LAR have been proposed for subclasses of Muller languages [46, 56]. The approach using composition of automata has one significant drawback: it disregards the structure of the original automaton, and only its acceptance condition is taken into account. Some works have explored heuristics to improve this aspect [52, 59, 70]. These refined transformations do still have the following property: each original state $q$ is turned into multiple states of the form $(q, x)$ – although this is done in a non-uniform way, with each state possibly being copied a different number of times. In this work, we introduce morphisms of transition systems to formalise the idea of transformations of automata and games; if a parity automaton $\mathcal{B}$ has been obtained as a transformation of a Muller automaton $\mathcal{A}$, there will be a morphism $\varphi: \mathcal{B} \to \mathcal{A}$ that sends states of the form $(q, x)$ to $q$. A theory of morphisms of transition systems is developed in Section 3.

**History-deterministic automata.** For the purposes of LTL synthesis and game transformations, it is imperative to eliminate non-determinism from automata, since non-deterministic automata do not yield correct games. Unfortunately, deterministic automata can be exponentially larger than non-deterministic ones. Recently, an intermediate model of automata, named history-deterministic (also called good-for-games), has received considerable attention. The reason is that history-determinism exactly captures the features of deterministic automata that make them suitable for synthesis purposes, while being a less restrictive model. A natural question that arises is whether history-deterministic automata can be more succinct that deterministic ones, and, in that case, which languages and automata types can benefit from this succinctness. It was not until several years after the introduction of history-determinism [38, 21] that an example of an $\omega$-regular language for which history-deterministic automata are smaller than deterministic ones was exhibit [49] (and it was even conjectured that such automaton could not exist [22]). History-deterministic automata are the focus of several lines of research (we refer to the survey [12] for a detailed exposition). Despite this, a complete understanding of history-deterministic automata remains elusive, and their scope of applicability is still uncertain. One key aspect that has not yet been addressed is how to design techniques as general as possible for building history-deterministic automata. To the best of our knowledge, the only existing result in this direction is a polynomial-time algorithm to minimise coBüchi history-deterministic automata [1].

**The Zielonka tree and the alternating cycle decomposition.** The starting point of our work is the notion of Zielonka tree, introduced by Zielonka [81] as an informative representation of Muller languages – languages that can be described by a boolean combination of atomic propositions of the form “the letter ‘a’ appears infinitely often”. The Zielonka tree
captures many important properties of Muller languages, such as being Rabin or parity [81], and, most importantly, it characterises their exact memory requirements, both in two-player games [28] and stochastic games [40].

The contribution at the core of this work is a generalisation of Zielonka trees to general Muller automata recognising any $\omega$-regular language, which we call the alternating cycle decomposition (ACD). The ACD, greatly inspired from Wagner's work on $\omega$-automata [80], is a data structure that provides an abridged representation of the accepting and rejecting cycles of the automaton, encapsulating the interplay between the structure of the underlying graph and the acceptance condition of a Muller automaton.

## Contributions

In this work, we carry out an extensive study of transformations of Muller automata and games. We outline next our main contributions.

1. **Minimal automata for Muller languages.** The basis on which we build up our work is a study of minimal automata recognising Muller languages. Using the Zielonka tree, we propose a construction of a deterministic parity automaton recognising a Muller language (Section 4.2). This construction implicitly appears in the long version of [28]. We show a strong optimality result: for all Muller language $L$, the parity automaton obtained from the Zielonka tree is minimal both amongst deterministic and history-deterministic parity automata recognising $L$ (Theorem 4.13)<fnref n="1" />. Moreover, it uses the optimal number of output colours to recognise $L$ (Theorem 4.12). The optimality result we obtain is much stronger than the worst case optimality result of the LAR transformation [56], since it applies to every Muller language. In particular, our characterisation yields an algorithm to minimise deterministic parity automata recognising Muller languages in polynomial time (Theorem 6.31). In light of our result, we conclude that the use of history-determinism does not yield any gain in the state complexity of parity automata recognising Muller languages.

We further propose a construction of a history-deterministic Rabin automaton recognising a Muller language (Section 4.3), and prove that this automaton is minimal amongst history-deterministic Rabin automata (Theorem 4.48). This construction is also based on the Zielonka tree.

In essence, our results reinforce the idea that the Zielonka tree precisely captures the fundamental properties of Muller languages.

2. **Introducing morphisms as witnesses of transformations.** In order to formalise transformations of games and automata, we develop a theory of morphisms of transition systems (Section 3). Intuitively, a morphism $\varphi: \mathcal{B} \to \mathcal{A}$ witnesses the fact that $\mathcal{B}$ has been obtained from $\mathcal{A}$ by blowing up each state $q \in \mathcal{A}$ to the states in $\varphi^{-1}(q)$. However, this property on its own does not suffice to guarantee the semantic equivalence of $\mathcal{A}$ and $\mathcal{B}$. It is for this reason that we introduce different variants of morphisms, offering a range of definitions with varying degrees of restrictiveness. Two kind of morphisms will be of central importance: (1) locally bijective morphisms, which generalise composition by deterministic automata and preserve determinism, and (2) history-deterministic mappings (HD mappings), which generalise composition by history-deterministic automata and are

<footnote n="1">¹ The optimality of the Zielonka-tree-parity-automaton amongst deterministic automata has also been obtained in the independent unpublished work [59].</footnote>
defined using a minimal set of hypothesis guaranteeing the semantic equivalence of $\mathcal{A}$ and $\mathcal{B}$.

3. **The alternating cycle decomposition and optimal transformations of Muller transition systems.** In order to generalise the fruitful applications of the Zielonka tree to Muller automata and games, we introduce the alternating cycle decomposition (ACD), a data structure that captures the interplay of the underlying graph of these transition systems and their acceptance condition (Section 5). Using the ACD, we describe a construction that transforms a Muller automaton $\mathcal{A}$ into an equivalent parity automaton $\mathcal{B}$ while preserving the determinism of $\mathcal{A}$ (formally, there is a locally bijective morphism $\varphi: \mathcal{B} \to \mathcal{A}$). This transformation comes with a strong optimality guarantee: for any other parity automaton $\mathcal{B}'$ admitting a locally bijective morphism (or even HD mapping) $\varphi': \mathcal{B}' \to \mathcal{A}$, the automaton $\mathcal{B}$ is smaller than $\mathcal{B}'$ and it uses less output colours (Theorems 5.31 and 5.32). An interesting corollary of our result is the following: if $\mathcal{B}$ is an HD parity automaton that is strictly smaller than any deterministic parity automaton recognising $\mathcal{L}(\mathcal{B})$, then $\mathcal{B}$ cannot be derived from a deterministic Muller automaton (Corollary 5.36). This result sheds light on the difficulty to obtain succinct HD automata and their potential applicability.

We also provide a transformation that translates a Muller automaton $\mathcal{A}$ into a history-deterministic Rabin automaton $\mathcal{B}$ in an optimal way: for any other Rabin automaton $\mathcal{B}'$ admitting an HD mapping $\varphi': \mathcal{B}' \to \mathcal{A}$, the automaton $\mathcal{B}$ is smaller than $\mathcal{B}'$.

4. **Structural results for Muller transition systems.** The ACD does not only provide optimal transformations of games and automata, it also features some of their fundamental structural properties. As an application, we give a set of crisp characterisations for relabelling automata with different classes of acceptance conditions (Section 6.1). For instance, we show that given a Muller automaton $\mathcal{A}$, we can define a Rabin condition over the underlying graph of $\mathcal{A}$ obtaining an equivalent automaton if and only if the union of rejecting cycles of $\mathcal{A}$ is again a rejecting cycle. Our results unify and extend those from [5, 9, 47, 81].

In Section 6.2, we conduct a comprehensive examination of a normal form for parity automata. This normal form implicitly appears in [15], and has since proven instrumental in proofs about history-deterministic automata [1, 29, 49], positionality of $\omega$-regular languages [13] and learning of $\omega$-automata [4]. Similar normalisation procedures are commonly applied to parity games to speed up algorithms solving them [35]. We use the ACD to provide straightforward proofs of the fundamental properties which make automata in normal form practical in both theoretical proofs and applications.

**Our model: transition systems and acceptance over edges.** We want to point out a few technical details about the model used in this paper. First, we work with general transition systems for two reasons: (1) to seamlessly encompass both automata and games models, and (2) to emphasise that the ACD and the transformations we propose do only depend in the underlying graph and the acceptance condition; we can view the input letters of an automaton, or the partition of the vertices in a game, as add-ons that do not affect the core of our approach.

Also, we define acceptance conditions over the edges of transitions systems – instead of over the vertices. This choice has been shown to yield more canonical results in theory, for instance, in the study of strategy complexity for games [13, 17, 24, 81], the determinisation of Büchi automata [25, 76], or the minimisation of history-deterministic automata [1, 29]. It has also proven to be more applicable in practical scenarios [27, 36]. We believe that the
present work provides further evidence to this claim, as the minimal automaton obtained
from the Zielonka tree, as well as the transformations based on the ACD, substantially rely
on the use of edge-based acceptance.

Finally, we remark that in this work we are concerned with *state complexity*, that is,
the efficiency of a construction is measured based on the number of states of the resulting
transition system. We do not focus in the representation of the acceptance conditions; for
instance, we will not differentiate between Muller or Emerson-Lei conditions, as they have
the same expressive power (see also Remark 2.11).

Related versions

This paper is based on a preceding conference version [18], and incorporates material from
another conference paper [19]. In addition, we have introduced some new content, revised
the presentation and simplified various proofs. We outline the provenance of the different
results:

**ICALP 2021 [18].** Most of the material concerning deterministic automata and locally bijective morphisms comes from [18]. This includes the construction of a parity automaton from the Zielonka tree (Section 4.2.1), the definition of the ACD (Section 5.1) and the construction of a parity automata from it (Section 5.2), as well as the introduction of locally bijective morphisms (Section 3.2) and the typeness results from Section 6.1. However, in [18], the optimality of the Zielonka-tree-parity-automaton and the ACD-parity-transform was proven only with respect to deterministic automata and locally bijective morphisms, respectively. Moreover, the proof of the optimality of the ACD-parity-transform (Theorem 5.32) has been simplified.

**ICALP 2022 [19].** The construction of history-deterministic Rabin automata for Muller languages (Section 4.3) and its optimality (Theorem 4.48) come from [19].

**Original content.** The following content has not appeared in any precedent work:

- optimality of the Zielonka-tree-parity-automaton with respect to HD automata (Theorem 4.13);

- the definition of HD mappings, as well as the systematic study of the different kinds of morphisms (Sections 3.3 and 3.4);

- the ACD-HD-Rabin-transform (Section 5.3) and its optimality (Theorem 5.33); and

- the introduction of a normal form for parity automata (Section 6.2).

In this paper, we have tried to integrate these results to present a coherent and complete
exposition of the theory of optimal transformations of Muller automata.

Follow-up work

Despite its recent introduction [18], the alternating cycle decomposition has already found
applications in both practical and theoretical scenarios. The ACD-parity-transform has been
implemented in two open-source tools: Spot 2.10 [27] and Owl 21.0 [45], and it is used in the
LTL-synthesis tools *ltlsynt* [27] and Strix [60]. These implementations were presented in
the conference paper [20], where transformations based on the ACD are compared to the
state-of-the-art existing paritizing methods.

The typeness results steaming from the ACD [18, Section 5] have also been proven
instrumental in theoretical applications. They have been used to show a correspondence
between Rabin automata and memory structures for games [17], and to provide lower bounds
in the size of deterministic Rabin automata [19].
## 2 Preliminaries

In this section we introduce definitions that will be used throughout the paper.

### Basic definitions

For a set $A$ we let $|A|$ denote its cardinality, $2^A$ its power set and $2_+^A = 2^A \setminus \{\emptyset\}$. For a family of subsets $\mathcal{F} \subseteq 2^A$ and $A' \subseteq A$, we write $\mathcal{F}|_{A'} = \mathcal{F} \cap 2^{A'}$. For natural numbers $i \le j$, $[i, j]$ stands for $\{i, i+1, \dots, j-1, j\}$.

For a set $\Sigma$, a *word* over $\Sigma$ is a sequence of elements from $\Sigma$. An $\omega$-*word* (or simply an *infinite word*) is a word of length $\omega$. The sets of finite and infinite words over $\Sigma$ will be written $\Sigma^*$ and $\Sigma^\omega$, respectively, and we let $\Sigma^\infty = \Sigma^* \cup \Sigma^\omega$. Subsets of $\Sigma^*$ and $\Sigma^\omega$ will be called *languages*. For a word $w \in \Sigma^\infty$ we write $w_i$ to represent the $i$-th letter of $w$. We let $\varepsilon$ denote the *empty word*, and let $\Sigma^+ = \Sigma^* \setminus \{\varepsilon\}$. The concatenation of two words $u \in \Sigma^*$ and $v \in \Sigma^\infty$ is written $u \cdot v$, or simply $uv$. If $u = v \cdot w$ for $v \in \Sigma^*$, $u, w \in \Sigma^\infty$, we say that $v$ is a *prefix* of $u$ and we write $v \subseteq u$. For a word $w \in \Sigma^\omega$, we let $\text{Inf}(w) = \{a \in \Sigma \mid w_i = a \text{ for infinitely many } i \in \mathbb{N}\}$.

We say 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$.

Given a map $\alpha : A \to B$, we will extend $\alpha$ to words component-wise, i.e., $\alpha : A^\infty \to B^\infty$ will be defined as $\alpha(w_0w_1w_2\dots) = \alpha(w_0)\alpha(w_1)\alpha(w_2)\dots$. We will use this convention throughout the paper without explicitly mentioning it. If $A' \subseteq A$, we note $\alpha|_{A'}$ the restriction of $\alpha$ to $A'$. We let $\text{Id}_A$ be the identity function on $A$. We write $\alpha : A \to B$ if $\alpha$ is a *partial mapping* (it is defined only over some subset of $A$).

A graph<sup>2</sup> is a tuple $G = (V, E, \text{Source}, \text{Target})$ where $V$ is a set of vertices, $E$ a set of edges and **Source**: $E \to V$ and **Target**: $E \to V$ are maps indicating the source and target for each edge. A *path* is a (finite or infinite) sequence $\rho = e_0e_1\dots \in E^\infty$ such that **Source**($e_i$) = **Target**($e_{i-1}$) for all $i > 0$. For notational convenience, we write $v_0 \xrightarrow{e_0} v_1 \cdots \xrightarrow{e_{n-1}} v_n$ to denote a finite path from $v_0 = \text{Source}(e_0)$ to $v_n = \text{Target}(e_{n-1})$ and we let $\text{Source}(\rho) = v_0$ and $\text{Target}(\rho) = v_n$. For $A \subseteq V$, we let $\text{Path}_A^{\text{fin}}(G)$ and $\text{Path}_A(G)$ denote, respectively, the set of finite and infinite paths on $G$ starting from some $v \in A$ (we omit brackets if $A = \{v\}$ is a singleton). We let $\text{Path}_A^{\infty}(G) = \text{Path}_A^{\text{fin}}(G) \cup \text{Path}_A(G)$. For a subset of vertices $A \subseteq V$ we write:

$$ \text{In}(A) = \{e \in E \mid \text{Target}(e) \in A\}, $$

$$ \text{Out}(A) = \{e \in E \mid \text{Source}(e) \in A\}. $$

All graphs considered in this paper will be finite.

A graph is *strongly connected* if there is a path connecting each pair of vertices. A *subgraph* of $(V, E, \text{Source}, \text{Target})$ is a graph $(V', E', \text{Source}', \text{Target}')$ such that $V' \subseteq V$, $E' \subseteq E$ and $\text{Source}'$ and $\text{Target}'$ are the restrictions of $\text{Source}$ and $\text{Target}$ to $E'$, respectively. A *strongly connected component* (SCC) is a maximal strongly connected subgraph. We say that a SCC is *final* if there is no edge leaving it. We say that a vertex $v$ is *recurrent* if it belongs to some SCC, and that it is *transient* on the contrary.

<footnote n="2"><sup>2</sup> In this work we will use the term *graph* to denote what is sometimes called a *directed multigraph* (edges are directed, and multiple edges between two vertices are allowed).</footnote>
## 2.1 Transition systems, automata and games

**Transition systems.** A pointed graph $G = (V, E, \text{Source}, \text{Target}, I)$ is a graph together with a non-empty subset of initial vertices $I \subseteq V$. An acceptance condition over $G$ is a tuple $\text{Acc} = (\gamma, \Gamma, \mathcal{W})$ where $\Gamma$ is a finite set of colours, $\gamma: E \to \Gamma \cup \{\varepsilon\}$ is an edge-colouring of $G$ and $\mathcal{W} \subseteq \Gamma^\omega$ is a language of infinite words called the acceptance set. We allow uncoloured edges ($\varepsilon$-edges), but we impose the condition that no infinite path of $G$ is eventually composed exclusively of $\varepsilon$-edges (that is, every cycle contains some edge $e$ with $\gamma(e) \neq \varepsilon$).

A transition system (abbreviated $\mathcal{T}S$) is a tuple $\mathcal{T}S = (G_{\mathcal{T}S}, \text{Acc}_{\mathcal{T}S})$, where $G_{\mathcal{T}S} = (V, E, \text{Source}, \text{Target}, I)$ is a pointed graph, called the underlying graph of $\mathcal{T}S$, and $\text{Acc}_{\mathcal{T}S} = (\gamma, \Gamma, \mathcal{W})$ is an acceptance condition over $G_{\mathcal{T}S}$. We will also refer to vertices and edges as states and transitions, respectively. We write $v \stackrel{c}{\to} v'$ if there is $e \in E$ such that $\text{Source}(e) = v$, $\text{Target}(e) = v'$ and $\gamma(e) = c$. We will suppose for technical convenience that transition systems contain no sink, that is, every vertex has at least one outgoing edge. For any non-empty subset of vertices $\tilde{I} \subseteq V$, we let $\mathcal{T}S_I$ be the transition system obtained from $\mathcal{T}S$ by setting $\tilde{I}$ to be its set of initial vertices. The size of a transition system $\mathcal{T}S$ is the cardinality of its set of vertices, written $|\mathcal{T}S|$.

A run on a transition system $\mathcal{T}S$ (or on a pointed graph) is a (finite or infinite) path $\rho = e_0 e_1 \cdots \in E^\infty$ starting from an initial vertex, that is, $\text{Source}(e_0) \in I$. We let $\mathcal{R}un^{\text{fin}}(\mathcal{T}S)$ and $\mathcal{R}un(\mathcal{T}S)$ be the set of finite and infinite runs on $\mathcal{T}S$, respectively, and we let $\mathcal{R}un^{\infty}(\mathcal{T}S) = \mathcal{R}un^{\text{fin}}(\mathcal{T}S) \cup \mathcal{R}un(\mathcal{T}S)$. (We note that $\mathcal{R}un(\mathcal{T}S) = \text{Path}_I(G_{\mathcal{T}S})$.)

The output of a run $\rho \in \mathcal{R}un^{\infty}(\mathcal{T}S)$ is the sequence of colours in $\Gamma^\infty$ obtained by removing the occurrences of $\varepsilon$ from $\gamma(\rho)$; which we will also denote by $\gamma(\rho)$ by a small abuse of notation. A run $\rho$ is accepting if $\gamma(\rho) \in \mathcal{W}$, and rejecting otherwise (in particular, finite runs will be rejecting). We write $\rho = v \rightsquigarrow^w v'$ to denote a run with $\text{Source}(\rho) = v$, $\text{Target}(\rho) = v'$ and $\gamma(\rho) = w$.

We say that a vertex $v \in V$ is accessible (or reachable) from a vertex $v_0$ if there exists a finite path from $v_0$ to $v$. We say that $v$ is accessible if it is accessible from some initial vertex. A set of states $B \subseteq V$ is accessible if every state $v \in B$ is accessible. The accessible part of a transition system is the set of accessible states. We define analogously the accessible part from a vertex $v_0$.

A labelled graph $(G, (l_V, L_V), (l_E, L_E))$ is a graph together with labelling functions $l_V: V \to L_V$, $l_E: E \to L_E$, where $L_V$ and $L_E$ are sets of labels for vertices and edges, respectively. If only the first (resp. the second) of these labelling functions appears, we will use the terms vertex-labelled (resp. edge-labelled) graphs. A labelled transition system is a transition system with labelled underlying graph.

**Remark 2.1.** We remark that, whenever necessary, we can suppose without loss of generality that in the acceptance condition $\text{Acc} = (\gamma, \Gamma, \mathcal{W})$ of a transition system, $\Gamma = E$ is the whole set of edges and $\gamma$ is the identity function. Indeed, an equivalent acceptance condition can always be defined by using the acceptance set $\mathcal{W}' = \{w \in E^\omega \mid \gamma(w) \in \mathcal{W}\} \subseteq E^\omega$.

**Automata.** A (non-deterministic) automaton over $\Sigma$ is an edge-labelled transition system $\mathcal{A} = (G_{\mathcal{A}}, \text{Acc}_{\mathcal{A}}, (l_\Sigma, \Sigma))$, where $\Sigma$ is a finite set of input letters. Let $\mathcal{A}$ be an automaton with $G_{\mathcal{A}} = (Q, \Delta, \text{Source}, \text{Target}, I)$ as underlying graph and $\text{Acc}_{\mathcal{A}} = (\gamma, \Gamma, \mathcal{W})$ as acceptance condition. We write $e = q \xrightarrow{a:c} q'$ to denote that $e \in \Delta$ satisfies $l_\Sigma(e) = a$ and $\gamma(e) = c$. We can suppose that $\Delta \subseteq Q \times \Sigma \times \Gamma \times Q$. We define:

$$ \delta(q, a) = \{(q', c) \in Q \times \Gamma \mid \text{there is } e = q \xrightarrow{a:c} q' \in \Delta\}. $$
We note that we can now recover the classical representation of an automaton as a tuple $\mathcal{A} = (Q, \Sigma, I, \Gamma, \delta, W)$, (or $(Q, \Sigma, I, \Gamma, \Delta, W)$) which we might use when working exclusively with automata.

We say that an automaton $\mathcal{A}$ is *deterministic* if $I$ is a singleton and for every $q \in Q$ and $a \in \Sigma$, $|\delta(q, a)| \le 1$. We say that $\mathcal{A}$ is *complete* if for every $q \in Q$ and $a \in \Sigma$, $|\delta(q, a)| \ge 1$. We remark that we can suppose that automata are complete without loss of generality by adding a sink state.

Given an automaton $\mathcal{A}$ and a word $w \in \Sigma^\infty$, a run over $w$ in $\mathcal{A}$ is a run $\rho = e_0e_1\cdots \in \mathcal{R}un^\infty(\mathcal{A})$ such that $l_\Sigma(e_i) = w_i$ for all $i \ge 0$. A word $w \in \Sigma^\omega$ is accepted by $\mathcal{A}$ if it exists a run over $w$ that is accepting (that is, a run $\rho$ such that $\gamma(\rho) \in W$). The language accepted (or recognised) by an automaton $\mathcal{A}$ is the set

$$ \mathcal{L}(\mathcal{A}) := \{w \in \Sigma^\omega \mid w \text{ is accepted by } \mathcal{A}\}. $$

Two automata recognising the same language are said equivalent.

We remark that if $\mathcal{A}$ is deterministic (resp. complete), there is at most one (resp. at least one) run over $w$ for each $w \in \Sigma^\infty$.

Given a subgraph $G'$ of the underlying graph of an automaton $\mathcal{A}$ and a subset of states $I'$ in $G'$, the *subautomaton induced by $G'$* with initial states $I'$ is the automaton having $G'$ as underlying graph, $I'$ as set of initial states, and whose acceptance condition and labelling with input letters are the restrictions of those of $\mathcal{A}$.

**History-deterministic automata.** Let $\mathcal{A}$ be a (non-deterministic) automaton over $\Sigma$ with $\Delta$ as set of transitions and $I$ as set of initial states. A resolver for $\mathcal{A}$ is a pair $(r_0, r)$, consisting of a choice of an initial state$^3$, $r_0 \in I$, and a function $r: \Delta^* \times \Sigma \to \Delta$ such that for all words $w = w_0w_1\cdots \in \Sigma^\omega$, the sequence $e_0e_1\cdots \in \Delta^\omega$, called the *run induced by $r$* over $w$ and defined by $e_i = r(e_0\dots e_{i-1}, w_i)$ is actually a run over $w$ in $\mathcal{A}$ starting from $r_0$. We say that the resolver is *sound* if it satisfies that for every $w \in \mathcal{L}(\mathcal{A})$, the run induced by $r$ over $w$ is an accepting run. In other words, $r$ should be able to construct an accepting run in $\mathcal{A}$ letter-by-letter with only the knowledge of the word so far, for all words in $\mathcal{L}(\mathcal{A})$. An automaton $\mathcal{A}$ is called *history-deterministic* (shortened HD, also called *good-for-games* in the literature) if there is a sound resolver for it.

**Remark 2.2.** Deterministic automata are history-deterministic, and they admit a unique resolver.

**Example 2.3.** In Figure 1, we show an automaton $\mathcal{A}$ over $\Sigma = \{a, b, c\}$ that is not deterministic (as it has two $b$-transitions from $q_1$) but is history-deterministic. Its set of output colours is $\Gamma = \{1, 2\}$ and its acceptance set is $W = \{u \in \{1, 2\}^\omega \mid u \text{ contains finitely many 1s}\}$ (this is a coBüchi condition, as introduced in the next section). It is easy to check that $\mathcal{A}$ recognises the language:

$$ \mathcal{L}(\mathcal{A}) = \{w \in \Sigma^\omega \mid \mathrm{Inf}(w) \subseteq \{a, b\} \text{ or } \mathrm{Inf}(w) \subseteq \{b, c\}\}. $$

A resolver for $\mathcal{A}$ only has to take a decision when the automaton is in the state $q_1$ and letter $b$ is provided. In this case, a sound resolver is obtained by using the following strategy:

<footnote>$^3$ Sometimes in the literature [7, 12, 38] the initial state $r_0$ is not required to be specified. This would permit to choose it after the first letter $w_0$ is given. We consider that a resolver constructing a run without guessing the future should pick the initial state before the first letter is revealed, hence the introduction of $r_0$ in the definition of a resolver. The suitability of this choice will be further supported by the generalisation of HD automata to HD mappings (Section 3.3).</footnote>
if the last letter seen was *a*, we take the transition leading to state $q_0$; if it was *c*, we take the transition leading to $q_2$. This strategy ensures that, if eventually only letters in $\{a, b\}$ (resp. $\{b, c\}$) are seen, the run will end up in state $q_0$ (resp. $q_2$) and remain there indefinitely, without producing any colour 1.

<figure><img src="image_2.png" /><figcaption>Figure 1 An example of a history-deterministic automaton that is not deterministic. The acceptance set is $W = \{u \in \{1, 2\}^\omega \mid u \text{ contains finitely many 1s}\}$. An arrow of the form $q \xrightarrow{a,b:2} q'$ represents two different transitions with input letters *a* and *b*, respectively. The initial state $q_0$ is marked with one incoming arrow.</figcaption></figure>

We say that an state *q* is reachable using the resolver (*r*₀, *r*) if there is a finite run
*ρ* = *r*₀ ⇌ *q* such that *ρ* is the run induced by *r* over some word *w* ∈ Σ*^*.

Next remark indicates that we can suppose without loss of generality that all states in an
HD automaton are reachable using some sound resolver.

► **Remark 2.4.** Let $\mathcal{A}$ be an HD automaton, let $(r_0, r)$ be a sound resolver for it and let $\tilde{\mathcal{A}}$ be the subautomaton induced by the set of states reachable using $(r_0, r)$, with initial state $r_0$. Then, $\mathcal{L}(\mathcal{A}) = \mathcal{L}(\tilde{\mathcal{A}})$.

The following lemma provides a simplification for automata recognising prefix-independent
languages. Its proof can be found in Appendix C. Together with Remark 2.4, it indicates that
when dealing with HD automata for this kind of languages, we can suppose that any state of
the automaton is the initial one. In particular there will be no need to specify the initial
states of subautomata induced by subgraphs of HD automata recognising prefix-independent
languages.

**► 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 is verified 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$.

**Games.** A game is a vertex-labelled transition system $\mathcal{G} = (G_G, \text{Acc}_G, (l_{\text{Players}}, \{\text{Eve}, \text{Adam}\}))$, with $G_G = (V, E, \text{Source}, \text{Target}, I)$ a pointed graph, and $l_{\text{Players}}: V \to \{\text{Eve}, \text{Adam}\}$ a vertex-labelling function inducing a partition of $V$ into vertices controlled by two players that we refer to as *Eve* and *Adam*. We let $V_{\text{Eve}} = l_{\text{Players}}^{-1}(\text{Eve})$ and $V_{\text{Adam}} = l_{\text{Players}}^{-1}(\text{Adam})$.

During a play, players move a token from one vertex to another for an infinite amount of
time. The player who owns the vertex $v$ where the token is placed chooses an edge in $\text{Out}(v)$
and the token travels through this edge to its target. In this way, they produce an infinite
run $\rho$ on $\mathcal{G}$ (that we also call a *play*). The objective of Eve is to produce an accepting run (a
sequence of colours in $\mathcal{W}$), and Adam tries to prevent it.

A strategy from $v \in V$ for Eve is a (partial) function $\text{strat}_v : \mathcal{P}ath_v^{\text{fin}}(\mathcal{G}) \to E$, defined for finite paths from $v$ ending in a vertex in $V_{\text{Eve}}$, that tells Eve which move to choose after any possible finite play. We say that a play $\rho \in \mathcal{P}ath_v^{\infty}(\mathcal{G})$ is consistent with the strategy $\text{strat}_v$
if after each finite prefix $\rho' \subseteq \rho$ ending in a vertex controlled by Eve, the next edge in $\rho$ is $\text{strat}_v(\rho')$. We say that $\text{strat}_v$ is a winning strategy for Eve if all plays from $v$ consistent with $\text{strat}_v$ are accepting. We say that Eve wins the game $\mathcal{G}$ from $v$ if there is a winning strategy from $v$ for her. Strategies for Adam are defined dually.

Given a game $\mathcal{G}$, the winning region of $\mathcal{G}$ for Eve, written $W_{\text{Eve}}(\mathcal{G})$, is the set of initial vertices $v \in I$ such that she wins the game $\mathcal{G}$ from $v$. The full winning region of $\mathcal{G}$ for Eve is her winning region in the game $G_V$ where all vertices are initial, that is, the set of vertices $v \in V$ such that Eve wins the game $\mathcal{G}$ from $v$.

In some proofs, we will need to take a close look into the strategies used in games, for which we need to introduce finite memory strategies. For a set $X$ (usually the set of edges of a game), we define a memory skeleton over $X$ as an edge-labelled pointed graph $\mathcal{M} = (M, E_M, \text{Source}, \text{Target}, m_0)$ with a single initial state $m_0$ and labels $l_M: E_M \to X$ inducing a deterministic structure, that is, satisfying that for each $m \in M$ and $x \in X$ there is at most one transition $e \in \text{Out}(m)$ labelled $x$. We denote $\mu: M \times X \to M$ the update function given by $\mu(m, x) = m'$ if $m \xrightarrow{x} m'$ is the (only) transition from $m$ labelled $x$. We extend $\mu$ to $\mu: M \times X^* \to M$ by induction ($\mu(m, \varepsilon) = m$ and $\mu(m, x_1 \dots x_n) = \mu(\mu(m, x_1 \dots x_{n-1}), x_n)$). A memory structure (for Eve) for a game $\mathcal{G}$ is a memory skeleton over the set $E$ of edges of $\mathcal{G}$ together with a next-move function $\sigma: V_{\text{Eve}} \times M \to E$. We say that $(\mathcal{M}, \sigma)$ implements a strategy $\text{strat}_v: \text{Path}_v^{\text{fin}}(\mathcal{G}) \to E$ if for any finite play $\rho \in \text{Path}_v^{\text{fin}}(\mathcal{G})$ ending in $V_{\text{Eve}}$, $\text{strat}_v(\rho) = \sigma(\text{Target}(\rho), \mu(m_0, \rho))$. We remark that a memory structure for $\mathcal{G}$ implements at most one strategy from a given vertex. We say that $\text{strat}_v$ is a finite memory strategy if it can be implemented by a finite memory structure.

**Composition of a transition system and an automaton.** We now present the construction of the composition (or product) of a transition system with an automaton, which constitutes the standard method for transforming a transition system that uses an acceptance set $W_1$ to another one using a different acceptance set $W_2$. To guarantee the correctness of the resulting transition system (that is, that it has the same semantic properties as the original one), the automaton must be deterministic or history-deterministic (see Propositions 2.6, 2.7, and 2.8).

Let $\mathcal{T}\mathcal{S} = (G_{\mathcal{T}\mathcal{S}}, \text{Acc}_{\mathcal{T}\mathcal{S}})$ be a transition system, with $G_{\mathcal{T}\mathcal{S}} = (V, E, \text{Source}_{\mathcal{T}\mathcal{S}}, \text{Target}_{\mathcal{T}\mathcal{S}}, I_{\mathcal{T}\mathcal{S}})$ and $\text{Acc}_{\mathcal{T}\mathcal{S}} = (\gamma_{\mathcal{T}\mathcal{S}}, \Sigma, W_{\mathcal{T}\mathcal{S}})$, and let $\mathcal{A} = (G_{\mathcal{A}}, \text{Acc}_{\mathcal{A}}, (l_{\Sigma}, \Sigma))$ be a complete automaton over the alphabet $\Sigma$, where $G_{\mathcal{A}} = (Q, \Delta, \text{Source}_{\mathcal{A}}, \text{Target}_{\mathcal{A}}, I_{\mathcal{A}})$ and $\text{Acc}_{\mathcal{A}} = (\gamma_{\mathcal{A}}, \Gamma, W_{\mathcal{A}})$. The composition of $\mathcal{T}\mathcal{S}$ and $\mathcal{A}$ (also called their product) is the transition system $\mathcal{T}\mathcal{S} \times \mathcal{A}$ defined as follows:

- The set of vertices is the cartesian product $V \times Q$.

- The set of initial vertices is $I_{\mathcal{T}\mathcal{S}} \times I_{\mathcal{A}}$.

- The set of edges $E^{\times}$ contains a transition $(v, q) \xrightarrow{c} (v', q')$ if there is $a \in \Sigma$ and transitions $e_1 = v \xrightarrow{a} v' \in E$ and $e_2 = q \xrightarrow{a:c} q' \in \Delta$. It also contains $\varepsilon$-edges $(v, q) \xrightarrow{\varepsilon} (v', q)$ if $v \xrightarrow{\varepsilon} v' \in E$. Formally,

$$E^{\times} = \{(e_1, e_2) \in E \times \Delta \mid \gamma_{\mathcal{T}\mathcal{S}}(e_1) = l_{\Sigma}(e_2)\} \cup \{e_1 \in E \mid \gamma_{\mathcal{T}\mathcal{S}}(e_1) = \varepsilon\} \subseteq (E \times \Delta) \cup E.$$

- The acceptance condition is inherited from that of $\mathcal{A}$: the colouring function $\gamma': E^{\times} \to \Gamma$ is defined as $\gamma'(e_1, e_2) = \gamma(e_2)$, and the acceptance set is $W_{\mathcal{A}} \subseteq \Gamma^{\omega}$.

We remark that if $\mathcal{T}\mathcal{S}$ does not contain an uncoloured cycle, neither does $\mathcal{T}\mathcal{S} \times \mathcal{A}$. Also, $\mathcal{T}\mathcal{S} \times \mathcal{A}$ does not contain sinks by completeness of $\mathcal{A}$.
If $\mathcal{T}\mathcal{S}$ is a labelled transition system, labelled by the functions $l_V$ and $l_E$, we consider $\mathcal{T}\mathcal{S} \times \mathcal{A}$ as a labelled transition system with the functions $l_V^\times(v, q) = l_V(v)$ and $l_E^\times(e_1, e_2) = l_E(e_1)$ (resp. $l_E^\times(e_1) = l_E(e_1)$ if $e_1$ is an uncoloured edge).

Intuitively, a computation in $\mathcal{T}\mathcal{S} \times \mathcal{A}$ happens as follows: we start from a vertex $v_0 \in I_{\mathcal{T}\mathcal{S}}$ in $\mathcal{T}\mathcal{S}$ and from $q_0 \in I_{\mathcal{A}}$. When we are in a position $(v, q) \in V \times Q$, a transition $e$ between $v$ and $v'$ takes place in $\mathcal{T}\mathcal{S}$, producing a letter $a \in \Sigma$ as output. Then, the automaton $\mathcal{A}$ proceeds using a transition corresponding to $a$, producing an output in $\Gamma$. In this way, a word in $\Gamma^\omega$ is generated and we can use the acceptance set $W_\mathcal{A} \subseteq \Gamma^\omega$ of the automaton as the acceptance set for $\mathcal{T}\mathcal{S} \times \mathcal{A}$.

In particular, we can perform this operation if $\mathcal{T}\mathcal{S}$ is an automaton. We obtain in this way a new automaton that uses the acceptance condition of $\mathcal{A}$.

We could, of course, apply this construction to a game $\mathcal{G}$, obtaining a new game $\mathcal{G} \times \mathcal{A}$ in which the player who makes a move in $\mathcal{G}$ also chooses a transition in $\mathcal{A}$ corresponding to the letter produced by the selected move. However, in most applications, we intend to obtain an asymmetric form of product game in which one player has full control of the transitions of the automaton (we take the point of view of Eve and want her to choose these transitions). For this reason, we restrain the class of games to which we can apply the product construction by a non-deterministic automaton.

We say that a game is *suitable for transformations* if it satisfies that for every edge $e = v \to v'$ such that $v \in V_{\text{Adam}}$, the edge $e$ is uncoloured ($\gamma(e) = \varepsilon$), $v' \in V_{\text{Eve}}$, and $e$ is the only incoming edge to $v'$ ($\ln(v') = \{e\}$). We remark that any game $\mathcal{G}$ can be made suitable for transformations with at most a linear blow up on the size by inserting an intermediate Eve-vertex in each edge outgoing from an Adam-vertex. A formal construction, as well as further motivation for this definition, can be found in Appendix B.

The following results are well known and constitute the main application of automata composition. They can be seen as corollaries of our results from Section 3.4, which generalise them.

**Proposition 2.6 (Folklore).** Let $\mathcal{B}$ be an automaton with acceptance set $W_\mathcal{B}$ and let $\mathcal{A}$ be an automaton recognising $\mathcal{L}(\mathcal{A}) = W_\mathcal{B}$. Then, $\mathcal{L}(\mathcal{B} \times \mathcal{A}) = \mathcal{L}(\mathcal{B})$. Moreover, if $\mathcal{A}$ and $\mathcal{B}$ are deterministic (resp. history-deterministic), so is $\mathcal{B} \times \mathcal{A}$.

**Proposition 2.7 ([38]).** Let $\mathcal{G}$ be a game that is suitable for transformations with acceptance set $W_\mathcal{G}$, and let $\mathcal{A}$ be a history-deterministic automaton recognising $\mathcal{L}(\mathcal{A}) = W_\mathcal{G}$. Then, the winning region of Eve in $\mathcal{G}$ is the projection of her winning region in $\mathcal{G} \times \mathcal{A}$, that is, Eve wins $\mathcal{G}$ from an initial vertex $v$ if and only if she wins $\mathcal{G} \times \mathcal{A}$ from $(v, q_0)$, for $q_0$ some initial vertex of $\mathcal{A}$.

Proposition 2.7 fails if the automaton is not HD. In fact, this property characterises history-determinism, which is the reason why HD automata are also called *good-for-games* in the literature. However, it should be noted that history-determinism and good-for-gameness have been generalised to other contexts in which they do not necessarily yield equivalent notions [11, 21].

**Proposition 2.8 ([38]).** Let $\mathcal{A}$ be an automaton recognising $W_\mathcal{G} \subseteq \Sigma^\omega$ satisfying that for every game $\mathcal{G}$ suitable for transformations with acceptance set $W_\mathcal{G}$, Eve wins the game $\mathcal{G}$ from an initial vertex $v$ if and only if she wins $\mathcal{G} \times \mathcal{A}$ from $(v, q_0)$, for $q_0$ some initial vertex of $\mathcal{A}$. Then, $\mathcal{A}$ is history-deterministic.
## 2.2 Muller languages, cycles and the parity hierarchy

**Languages commonly used as acceptance sets.** We now define the main classes of languages used by $\omega$-regular automata as acceptance sets. We let $\Gamma$ stand for a finite set of colours.

**Büchi.** Given a subset $B \subseteq \Gamma$, we define the *Büchi language associated to B* as:

$$ \text{Büchi}_{\Gamma}(B) = \{w \in \Gamma^{\omega} \mid \text{Inf}(w) \cap B \neq \emptyset\}. $$

We say that a language $L \subseteq \Gamma^\omega$ is a *Büchi language* if there is a set $B \subseteq \Gamma$ such that $L = \text{Büchi}_{\Gamma}(B)$.

**coBüchi.** Given a subset $B \subseteq \Gamma$, we define the *coBüchi language associated to B* as:

$$ \text{coBüchi}_{\Gamma}(B) = \{w \in \Gamma^{\omega} \mid \text{Inf}(w) \cap B = \emptyset\}. $$

We say that a language $L \subseteq \Gamma^\omega$ is a *coBüchi language* if there is a set $B \subseteq \Gamma$ such that $L = \text{coBüchi}_{\Gamma}(B)$.

**Rabin.** A Rabin language is represented by a family $R = \{(G_1, R_1), \dots, (G_r, R_r)\}$ of Rabin pairs, where $G_j, R_j \subseteq \Gamma$. The Rabin language associated to $R$ is defined as:

$$ \text{Rabin}_{\Gamma}(R) = \{w \in \Gamma^{\omega} \mid [\text{Inf}(w) \cap G_j \neq \emptyset \text{ and } \text{Inf}(w) \cap R_j = \emptyset] \text{ for some index } j\}. $$

If $[\text{Inf}(w) \cap G_j \neq \emptyset \text{ and } \text{Inf}(w) \cap R_j = \emptyset]$, we say that $w$ is accepted by the Rabin pair $(G_j, R_j)$. We say that a language $L \subseteq \Gamma^\omega$ is a Rabin language if there is a family of Rabin pairs $R$ such that $L = \text{Rabin}_{\Gamma}(R)$.

**Streett.** The *Streett language associated to* a family $S = \{(G_1, R_1), \dots, (G_r, R_r)\}$ of Rabin pairs is defined as:

$$ \text{Streett}_{\Gamma}(S) = \{w \in \Gamma^{\omega} \mid [\text{Inf}(w) \cap G_j \neq \emptyset \text{ implies } \text{Inf}(w) \cap R_j = \emptyset] \text{ for all indices } j\}. $$

We say that a language $L \subseteq \Gamma^\omega$ is a *Streett language* if there is a family of Rabin pairs $S$ such that $L = \text{Streett}_{\Gamma}(S)$.

**Parity.** We define the *parity language* over the alphabet $[d_{\min}, d_{\max}] \subseteq \mathbb{N}$ as:

$$ \text{parity}_{[d_{\min}, d_{\max}]} = \{w \in [d_{\min}, d_{\max}]^{\omega} \mid \min \text{Inf}(w) \text{ is even}\}. $$

We say that a language $L \subseteq \Gamma^\omega$ is a $[d_{\min}, d_{\max}]$-parity language if there is a mapping $\phi: \Gamma \to [d_{\min}, d_{\max}]$ such that for all $w \in \Gamma^\omega$, $w \in L$ if and only if $\phi(w) \in \text{parity}_{[d_{\min}, d_{\max}]}$. We say that $L$ is a *parity language* if there are $d_{\min}, d_{\max} \in \mathbb{N}$ such that $L$ is a $[d_{\min}, d_{\max}]$-parity language.

**Muller.** We define the *Muller language associated to* a family $\mathcal{F} \subseteq 2_+^\Gamma$ of non-empty subsets of $\Gamma$ as:

$$ \text{Muller}_{\Gamma}(\mathcal{F}) = \{w \in \Gamma^{\omega} \mid \text{Inf}(w) \in \mathcal{F}\}. $$

We say that a language $L \subseteq \Gamma^\omega$ is a *Muller language* if there is a family $\mathcal{F} \subseteq 2_+^\Gamma$ such that $L = \text{Muller}_{\Gamma}(\mathcal{F})$.

We drop the subscript $\Gamma$ (resp. $[d_{\min}, d_{\max}]$) whenever the set of colours is clear from the context. We remark that all languages of the classes above are prefix-independent (for all $w \in \Gamma^\omega$ and $u \in \Gamma^*$, $uw \in L$ if and only if $w \in L$).
We say that an acceptance condition (resp. transition system, automaton) is an *X condition* (resp. *X* transition system, *X* automaton), for *X* one of the classes of languages above, if its acceptance set is an *X* language. In the case of parity transition systems, we will always suppose that the set of colours is a subset of $\mathbb{N}$ and $\phi$ is the identity function.

We let *DPA* stand for deterministic parity automaton and *DMA* for deterministic Muller automaton.

We discuss further classes of languages in Appendix A (generalised Büchi and coBüchi languages, as well as generalised weak acceptance). We refer to the survey [6] for a more detailed account on different types of acceptance conditions.

**Remark 2.9 (Inclusions between classes).** We observe that there are many inclusions between the classes of languages that we have introduced. For example, Büchi languages are exactly $[0, 1]$-parity languages, and parity languages are Rabin languages [62]. In particular, all classes above are special cases of Muller languages. The relations between these classes of languages are outlined in Figure 2.

<figure><img src="image_3.png" /><figcaption>Figure 2 Relations between subclasses of Muller languages. An arrow from a class *X* towards a class *Y* means that if a language *L* ⊆ Γ<sup>ω</sup> is an *X* language, then it is also a *Y* language. Arrows obtained by transitivity have been omitted. Inclusions are strict: if an arrow from *X* to *Y* cannot be obtained by transitivity, then there are *X* languages that are not *Y* languages [81].</figcaption></figure>

**Remark 2.10.** A language $L \subseteq \Gamma^\omega$ is a Muller language if and only if it satisfies:

For all $w, w' \in \Gamma^\omega$, if $\text{Inf}(w) = \text{Inf}(w')$, then $w \in L \iff w' \in L$.

**Remark 2.11 (Representation of acceptance conditions).** In practice, there exists a variety of ways to represent Muller languages and acceptance conditions of automata: using boolean formulas (Emerson-Lei conditions), as a list of accepting subsets of edges, etc. The complexity and practicality of algorithms manipulating automata and games may greatly differ depending on the representation of their acceptance conditions [39, 41]. However, in this work, we are mostly interested in the expressive power of acceptance conditions, and the results we present will not depend on how they are represented.

**Example 2.12.** In Figure 3 we show three different types of automata over the alphabet $\Sigma = \{a, b\}$ recognising the language

$$L = \{w \in \Sigma^\omega \mid w = ub^\omega \text{ or } (w = ua^\omega \text{ and } u \text{ has an even number of 'b's})\}.$$

**ω-regular languages.** The class of ω-regular languages plays a central role in the theory of formal languages and verification. The significance of ω-regular languages is (partly) due to the robustness of its definition, as they admit multiple equivalent characterisations relating different areas of study.

**Proposition 2.13 ([62, 64]).** Let $L \subseteq \Sigma^\omega$ be a language of infinite words. The following properties are equivalent:

- $L$ can be recognised by a non-deterministic Büchi automaton.
<figure><img src="image_4.png" /><figcaption>■ **Figure 3** Different types of automata recognising the language $L = \{w \in \Sigma^\omega \mid w = ub^\omega \text{ or } (w = ua^\omega \text{ and } u \text{ has an even number of 'b's})\}$.</figcaption></figure>

- L can be recognised by a deterministic parity automaton.

- L can be recognised by a non-deterministic Muller automaton.

A language satisfying the previous conditions is called $\omega$-regular. Many other equivalent definitions exist. Notably, $\omega$-regular languages are exactly the languages that can be defined using *monadic second-order logic* [14], those that can be described by using $\omega$-regular expressions [57], and those that can be recognised by an $\omega$-semigroup [66, Chapter 2].

**Cycles.** Let $\mathcal{TS}$ be a transition system with $V$ and $E$ as set of vertices and edges, respectively. A cycle of $\mathcal{TS}$ is a subset $\ell \subseteq E$ such that there is a finite path $v_0 \xrightarrow{e_0} v_1 \xrightarrow{e_1} v_2 \to \dots v_r \xrightarrow{e_r} v_0$ with $\ell = \{e_0, e_1, \dots, e_r\}$. We remark that we do not require this path to be simple, that is, edges and vertices may appear multiple times. The set of *states of the cycle* $\ell$ is $\mathbf{States}(\ell) = \{v_0, v_1, \dots v_r\}$. The set of cycles of a transition system $\mathcal{TS}$ is written $\mathbf{Cycles}(\mathcal{TS})$. We will consider the set of cycles ordered by inclusion. For a state $v \in V$, we note $\mathbf{Cycles}_v(\mathcal{TS})$ the subset of cycles of $\mathcal{TS}$ containing $v$. We remark that a vertex $v$ is recurrent if and only if $\mathbf{Cycles}_v(\mathcal{TS}) \neq \emptyset$. We note that $\mathbf{Cycles}_v(\mathcal{TS})$ is closed under union; moreover, the union of two cycles $\ell_1, \ell_2 \in \mathbf{Cycles}_v(\mathcal{TS})$ is again a cycle if and only if there is some state $v$ such that both $\ell_1$ and $\ell_2$ contain $v$.

Let $\mathcal{TS}$ be a Muller transition system with acceptance condition $(\gamma, \Gamma, \text{Muller}_\Gamma(\mathcal{F}))$. Given a cycle $\ell \in \mathbf{Cycles}(\mathcal{TS})$, we say that $\ell$ is *accepting* (resp. *rejecting*) if $\gamma(\ell) \in \mathcal{F}$ (resp. $\gamma(\ell) \notin \mathcal{F}$). We remark that the maximal cycles of a transition system are exactly the sets of edges of its strongly connected components. In particular, we can apply the adjectives *accepting* and *rejecting* similarly to the SCCs of a Muller transition system.

We note that, by definition, the acceptance of a run in a Muller transition system only depends on the set of transitions taken infinitely often. For any infinite run $\rho \in \mathcal{Run}(\mathcal{TS})$, the set of transitions taken infinitely often forms a cycle, $\text{Inf}(\rho) = \ell_\rho \in \mathbf{Cycles}(\mathcal{TS})$, and $\rho$ is an accepting run if and only if $\ell_\rho$ is an accepting cycle.

**The deterministic and history-deterministic parity hierarchy.** As we have mentioned, every $\omega$-regular language can be recognised by a deterministic parity automaton, but the number of colours required to do so might be arbitrarily large. We can assign to each $\omega$-regular language the optimal number of colours needed to recognise it using a deterministic automaton. We obtain in this way the *deterministic parity hierarchy*, having its origins in the works of
Wagner [80], Kaminski [43], and Mostowski [62]. We represented this hierarchy in Figure 4. This hierarchy is strict, that is, for each level of the hierarchy there are languages that do not appear in lower levels [80]. It is known that we can decide in polynomial time the parity index of an $\omega$-regular language represented by a deterministic parity automaton [15], but this problem is NP-complete if the language is given by a deterministic Rabin or Streett automaton [48].

<figure><img src="image_5.png" /><figcaption>Figure 4 The (history-)deterministic parity hierarchy.</figcaption></figure>

**► Definition 2.14 (Parity index of a language).** Let $L \subseteq \Sigma^\omega$ be an $\omega$-regular language. We say that $L$ has parity index at least $[0, d-1]$ (resp. $[1, d]$) if any DPA recognising $L$ with a parity acceptance condition over the set of colours $[d_{\min}, d_{\max}]$ satisfies that $d_{\max} - d_{\min} \ge d-1$, and in case of equality $d_{\min}$ is even (resp. odd). We say that the parity index of $L$ is $[0, d-1]$ (resp. $[1, d]$) if, moreover, there is a DPA recognising $L$ with a parity acceptance condition over the set of colours $[0, d-1]$ (resp. $[1, d]$).

We say that $L$ has parity index at least $\text{Weak}_d$ if any DPA recognising $L$ with a parity acceptance condition over the set of colours $[d_{\min}, d_{\max}]$ satisfies that $d_{\max} - d_{\min} \ge d$. We say that the parity index of $L$ is $\text{Weak}_d$ if, moreover, there are DPAs $A_1$ and $A_2$ recognising $L$ with parity acceptance conditions over the sets of colours $[0, d]$ and $[1, d+1]$, respectively. ▼

If follows from the definition that for each $\omega$-regular language $L$, there is a unique $d$ such that either $L$ has parity index $[0, d-1]$, $[1, d]$ or $\text{Weak}_d$, and these options are mutually exclusive. See also Appendix A for more details about languages of parity index $\text{Weak}_d$.

One of our contributions is to show that the parity index also applies to Muller automata: any deterministic or HD Muller automaton recognising an $\omega$-regular language of parity index $[0, d-1]$ uses at least $d$ different colours (Proposition 6.14).

The following proposition states that the notion of parity index of a language does not change by using HD automata instead of deterministic ones in the definition. However, for non-deterministic automata, the hierarchy collapses at level $[0, 1]$ (Büchi automata) [57].

**► Proposition 2.15 ([10, Theorem 19]).** Let $\mathcal{A}$ be an HD parity automaton recognising a language $L$, and suppose that the parity index of $L$ is $[0, d-1]$ (resp. $[1, d]$). Then, the acceptance condition of $\mathcal{A}$ uses at least $d$ output colours, and if it uses exactly $d$ colours, the least of them is even (resp. odd). If the parity index of $L$ is $\text{Weak}_d$, then $\mathcal{A}$ uses at least $d+1$ output colours.

We show next that the parity index of an $\omega$-regular language can be read directly from a deterministic Muller automaton.
Let $\mathcal{T}\mathcal{S}$ be a transition system using the Muller acceptance condition $(\gamma, \Gamma, \text{Muller}_\Gamma(\mathcal{F}))$. A $d$-flower over a state $v$ of $\mathcal{T}\mathcal{S}$ is a set of $d$ cycles $\ell_1, \ell_2, \dots, \ell_d \in \text{Cycles}_v(\mathcal{T}\mathcal{S})$ such that $\ell_i \supseteq \ell_{i+1}$ and $\gamma(\ell_i) \in \mathcal{F} \iff \gamma(\ell_{i+1}) \notin \mathcal{F}$. We say that it is a positive flower if $\gamma(\ell_1) \in \mathcal{F}$ and that it is negative otherwise.

**Lemma 2.16 (Flower Lemma, [65, 80]).** Let $\mathcal{A}$ be a DMA. If $\mathcal{A}$ admits an accessible positive (resp. negative) $d$-flower, then $\mathcal{L}(\mathcal{A})$ has parity index at least $[0, d-1]$ (resp. $[1, d]$). If $\mathcal{A}$ admits both accessible positive and negative $d$-flowers, then $\mathcal{L}(\mathcal{A})$ has parity index at least $\text{Weak}_d$.

Conversely, if an $\omega$-regular language $L$ has parity index at least $[0, d-1]$ (resp. $[1, d]$), then any DMA recognising $L$ admits a positive (resp. negative) $d$-flower.

## 2.3 Trees

We introduce some technical notations that will be used to define automata based on the Zielonka tree (Sections 4.2 and 4.3) and the transformations based on the ACD (Sections 5.2 and 5.3).

A tree $T = (N, \preceq)$ is a non-empty finite set of nodes $N$ equipped with an order relation $\preceq$ called the ancestor relation (we say that $x$ is an ancestor of $y$, or that $y$ is below $x$ if $x \preceq y$), such that (1) there is a minimal node for $\preceq$, called the root, and (2) the ancestors of an element are totally ordered by $\preceq$. The converse relation $\succeq$ is the descendant relation. Maximal nodes are called leaves, and the set of leaves of $T$ is denoted by $\text{Leaves}(T)$. The minimal strict descendants of a node are called its children. The set of children of $n$ in $T$ is written $\text{Children}_T(n)$. The depth of a node $n$ is the number of strict ancestors of it. We note it $\text{Depth}(n)$. The height of a tree $T$ is the maximal length of a chain for the ancestor relation. A subtree of $T = (N, \preceq)$ is a tree $T' = (N', \succeq')$ such that $N' \subseteq N, \preceq'$ is the restriction of $\preceq$ to $N'$ and $\text{Children}_T(n') \subseteq \text{Children}_T(n')$ for all $n' \in N'$. Given a node $n$ of a tree $T$, the subtree of $T$ rooted at $n$ is the subtree of $T$ whose nodes are the nodes of $T$ that have $n$ as ancestor. A branch is a maximal chain of the order $\preceq$.

An ordered tree is a tree $T = (N, \preceq)$ together with a total order $\leq_n$ over $\text{Children}_T(n)$, for each node $n \in N$ that is not a leaf. We remark that a subtree of an ordered tree can be seen as an ordered tree with the restrictions of these total orders to the existing children. These orders induce a total order $\leq_T$ on $T$ (the depth-first order): let $n, n' \in N$. If $n \preceq n'$, we let $n \leq_T n'$. If $n$ and $n'$ are incomparable for the ancestor relation, let $n_m$ be the deepest common ancestor, and let $n_1, n_2 \in \text{Children}_T(n_m)$ such that $n_1 \preceq n$ and $n_2 \preceq n'$. We let $n \leq_T n'$ if and only if $n_1 \leq_n n_2$. In the latter case, we say that $n$ is on the left of $n'$.

We will make use of these orders through some auxiliary functions. Let $T'$ be a subtree of $T$ and $n$ a node of $T'$ that is not a leaf in $T'$. For $n' \in \text{Children}_T(n)$, we let

$$ \text{Next}_{T'}(n') = \begin{cases} \min_{\leq_n} \{n'' \in \text{Children}_{T'}(n) \mid n' <_n n''\} & \text{if this set is not empty,} \\ \min_{\leq_n} \{n'' \in \text{Children}_{T'}(n)\} & \text{otherwise.} \end{cases} $$

That is, the function $\text{Next}_{T'}$ maps each child of $n$ to a sibling that is its successor in $T'$ for the $\leq_n$-order, in a cyclic way.

Let $T' = (N', \preceq')$ be a subtree of $T = (N, \preceq)$. Let $n_m \in N'$ and $n_o \in N$ such that $n_m$ is a strict ancestor of $n_o$ ($n_m \prec n_o$). If $n_m$ is a leaf of $T'$, we define $\text{Jump}_{T'}(n_o, n_m) = n_m$. If not, we define $\text{Jump}_{T'}(n_o, n_m) = l_{\text{dest}} \in \text{Leaves}(T')$ to be the only node satisfying that there are two children of $n_m$ in $T$, $n_1, n_2 \in \text{Children}_T(n_m)$ such that:

$$ \text{ children of } n_1 \text{ are in } T, \text{ and } n_2 \text{ is a } \text{leaf of } T. $$
- $n_2 = \text{Next}_{T'}(n_1)$ (in particular, $n_2 \in N'$),

- $l_{\text{dest}} \ge n_2$ is the leftmost$^4$ leaf in $T'$ (minimal for $\le_{T'}$) below $n_2$.

(We remark that $n_1 = n_2$ if $n_1$ is the only child of $n_m$ in $T'$. For $n_m = n_o$, we define $\text{Jump}_{T'}(n_o, n_m)$ to be the leftmost leaf of $T'$ below $n_o$. Intuitively, $l = \text{Jump}_{T'}(n_o, n_m)$ if we can reach $l$ by the following procedure: we start at $n_o$, we go up the tree $T$ until finding the node $n_m$, we change to the next child of $n_m$ in $T'$ (in a cyclic way) and we re-descend to $l$ in $T'$ taking the leftmost branch. We drop the subscript $T'$ if $T' = T$.

An A-labelled (ordered) tree is an (ordered) tree $T$ together with a labelling function $\nu: N \to A$. A set of trees is called a forest.

We refer the reader to Examples 4.5 and 5.5 for illustrations of the notations introduced here.

### 3 Morphisms as witnesses of transformations

As mentioned in the introduction, all existing transformations of automata follow a common approach: they turn each state $q$ into multiple states of the form $(q, x)$, where $x$ stores some information about the acceptance condition. It is reasonable to put forward this characteristic as the defining trait establishing that an automaton has been obtained as a transformation of another. In this section, we introduce morphisms of transition systems, which formalise this idea: a morphism $\varphi: \mathcal{B} \to \mathcal{A}$ witnesses that each state $q \in \mathcal{A}$ has been augmented to $\varphi^{-1}(q)$. To ensure that $\mathcal{B}$ is semantically equivalent to $\mathcal{A}$, the morphism has to grant a further guarantee, namely, we need to be able to simulate runs of $\mathcal{A}$ in $\mathcal{B}$. We will examine two properties of morphisms that allow to do this: local bijectivity and history-determinism for mappings.

In all this section, $\mathcal{TS} = (G, \text{Acc})$ and $\mathcal{TS}' = (G', \text{Acc}')$ will stand for 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}')$.

#### 3.1 Morphisms of transition systems

► **Definition 3.1.** A morphism of graphs from $G$ to $G'$ is a pair of mappings $\varphi = (\varphi_V : V \to V', \varphi_E : E \to E')$ preserving edges, that is:

- Source'($\varphi_E(e)$) = $\varphi_V(\text{Source}(e))$ for every $e \in E$,

- Target'($\varphi_E(e)$) = $\varphi_V(\text{Target}(e))$ for every $e \in E$.

We say that $\varphi$ is a morphism of pointed graphs if, moreover, it preserves initial vertices:

- $\varphi_V(v_0) \in I'$ for every $v_0 \in I$.

If $(G, (l_V, L_V), (l_E, L_E))$ and $(G, (l'_V, L'_V), (l'_E, L'_E))$ are labelled graphs, we say that $\varphi$ is a morphism of labelled graphs if, in addition, $L_V \subseteq L'_V$, $L_E \subseteq L'_E$ and $\varphi$ preserves labels:

- $l'_V(\varphi_V(v)) = l_V(v)$ for every $v \in V$,

- $l'_E(\varphi_E(e)) = l_E(e)$ for every $e \in V$.

<footnote n="4">⁴ The choice of the leftmost leaf is arbitrary. In all our uses of the function Jump, it could be replaced by any leaf below $n_2$.</footnote>
We will write $\varphi: G \to G'$ to denote a morphism $\varphi$. We will drop the subscript in $\varphi_V$ and $\varphi_E$ whenever it can be deduced from its use. We say that $\varphi$ is *surjective* (resp. *injective*) if $\varphi_V$ is.

Note that the mapping $\varphi_V$ does not completely determine a morphism $\varphi$, as multiple edges might exist between two given vertices. However, if $G$ has no isolated vertices, the mapping $\varphi_E$ does determine it. It will be convenient nonetheless to also keep the notation for $\varphi_V$.

We remark that the image of a run in $G$ by a morphism of pointed graphs is a run in $G'$. Therefore, a morphism of pointed graphs $\varphi: G \to G'$ induces a mapping

$$ \varphi_{\mathcal{R}uns}: \mathcal{R}un^{\infty}(G) \to \mathcal{R}un^{\infty}(G'). $$

**Definition 3.2.** Let $\mathcal{TS}$ and $\mathcal{TS}'$ be two (labelled) transition systems. A weak morphism of (labelled) transition systems $\varphi: \mathcal{TS} \to \mathcal{TS}'$ is a morphism of (labelled) pointed graphs between their underlying graphs, $\varphi: G \to G'$. We say that it is a morphism of (labelled) transition systems if it preserves the acceptance of runs, that is:

$$ \text{for every infinite run } \rho \in \mathcal{R}un(\mathcal{TS}), \gamma(\rho) \in \mathcal{W} \iff \gamma'(\varphi_{\mathcal{R}uns}(\rho)) \in \mathcal{W}'. \quad \llap{\vrule width 0.5pt height 12pt width 12pt} $$

A morphism of labelled TS between automata (resp. between games) will be called a *morphism of automata* (resp. *morphism of games*).

We say that a morphism of TS $\varphi: \mathcal{TS} \to \mathcal{TS}'$ is an *isomorphism* if $\varphi_V$ and $\varphi_E$ are bijective and $\varphi^{-1} = (\varphi_V^{-1}, \varphi_E^{-1})$ is a morphism from $\mathcal{TS}'$ to $\mathcal{TS}$. In that case, we say that $\mathcal{TS}$ and $\mathcal{TS}'$ are *isomorphic*.

## 3.2 Local properties of morphisms

**Definition 3.3.** A morphism of pointed graphs $\varphi: G \to G'$ is called:

■ Locally surjective if it verifies:

1. For every $v'_0 \in I'$ there exists $v_0 \in I$ such that $\varphi(v_0) = v'_0$.

2. For every $v \in V$ and every $e' \in \mathrm{Out}(\varphi(v))$ there exists $e \in \mathrm{Out}(v)$ such that $\varphi(e) = e'$.

■ Locally injective if it verifies:

1. For every $v'_0 \in I'$, there is at most one $v_0 \in I$ such that $\varphi(v_0) = v'_0$.

2. For every $v \in V$ and every couple $e_1, e_2 \in \mathrm{Out}(v)$, $\varphi(e_1) = \varphi(e_2)$ implies $e_1 = e_2$.

■ Locally bijective if it is both locally surjective and locally injective. \quad $\llap{\vrule width 0.5pt height 12pt width 12pt}$

Equivalently, a morphism of pointed graphs $\varphi$ is locally surjective (resp. locally injective) if for every $v \in V$ the restriction of $\varphi_E$ to $\mathrm{Out}(v)$ is a surjection onto $\mathrm{Out}(\varphi(v))$ (resp. an injection into $\mathrm{Out}(\varphi(v)))$, and the restriction of $\varphi_V$ to $I$ is a surjection onto $I'$ (resp. an injection into $I'$).

Let $\varphi: \mathcal{TS} \to \mathcal{TS}'$ be a (weak) morphism, and let $\rho' = v'_0 \xrightarrow{e'_0} v'_1 \xrightarrow{e'_1} \dots$ be a run in $\mathcal{TS}'$. If $\varphi$ is locally surjective, we can pick an initial vertex $v_0$ in $\varphi^{-1}(v'_0)$ and build step-by-step a run $\rho$ in $\mathcal{TS}$ from $v_0$ that is sent to $\rho'$ under $\varphi$. If $\varphi$ is moreover locally bijective, the choices of the initial vertex and the edges at each step are unique, so runs in $\mathcal{TS}'$ can be simulated in $\mathcal{TS}$ via $\varphi$ in a unique way. Said differently, if $\varphi: \mathcal{TS} \to \mathcal{TS}'$ is a locally bijective morphism, we can see $\mathcal{TS}$ as an automaton that processes runs of $\mathcal{TS}'$ in a deterministic fashion (this idea is formalised in Section 5.4.3). This property will allow us to show that a locally bijective morphism witnesses the semantic equivalence of $\mathcal{TS}$ and $\mathcal{TS}'$ (see Section 3.4).
We note that the notion of locally bijective morphisms of transition systems almost coincide with the usual concept of bisimulation. The main difference is that locally bijective morphisms treat the acceptance of a run as a whole; we do not impose the output colour of an edge $\gamma(e)$ to coincide with the colour $\gamma'(\varphi(e))$. This allows us to compare transition systems using different types of acceptance conditions.

**Remark 3.4.** Let $\varphi$ be a morphism of pointed graphs.

1. If $\varphi$ is locally surjective, then $\varphi_{\mathcal{R}_{uns}}$ is surjective.

2. If $\varphi$ is locally injective, then $\varphi_{\mathcal{R}_{uns}}$ is injective.

3. If $\varphi$ is locally bijective, then $\varphi_{\mathcal{R}_{uns}}$ is bijective.

In the following, the weak morphisms under consideration will be locally surjective. Next lemma ensures that we can suppose that they are surjective without loss of generality.

**Lemma 3.5.** If $\varphi: \mathcal{TS} \to \mathcal{TS}'$ is a locally surjective weak morphism, it is onto the accessible part of $\mathcal{TS}'$. That is, for every accessible state $v' \in \mathcal{TS}'$, there exists some state $v \in \mathcal{TS}$ such that $\varphi_V(v) = v'$. In particular, if every state of $\mathcal{TS}'$ is accessible, $\varphi$ is surjective.

**Proof.** Let $v'$ be an accessible state of $\mathcal{TS}'$. By definition, there exists a finite run $\rho'$ from an initial vertex of $\mathcal{TS}'$ to $v'$. By surjectivity of $\varphi_{\mathcal{R}_{uns}}$, there is a finite run $\rho \in \mathcal{R}_{un}^{\text{fin}}(\mathcal{TS})$ such that $\varphi_{\mathcal{R}_{uns}}(\rho) = \rho'$. As $\varphi$ is a morphism of graphs, we have that $\varphi(\text{Target}(\rho)) = v'$. $\quad \blacksquare$

**Example 3.6.** In Figure 5 we provide an example of a locally bijective morphism between the two rightmost transition systems from Figure 3 (we have removed input letters for simplicity). We recall that the acceptance set of the rightmost transition system is the Muller language associated to $\mathcal{F} = \{\{\alpha\}, \{\beta\}\}$. The morphism is given by $\varphi_V(v_1) = \varphi_V(v_2) = v'$ and $\varphi_V(v_2) = v'_2$. In this case, the mapping $\varphi_V$ determines a unique morphism; the (uniquely determined) mapping $\varphi_E$ is represented by the colours of the edges in the figure. It is easy to check that this mapping preserves the acceptance of runs and that it is locally bijective.

<figure><img src="image_6.png" /><figcaption>Figure 5 A locally bijective morphism from a parity TS to a Muller TS with acceptance set given by $\mathcal{F} = \{\{\alpha\}, \{\beta\}\}$. We use dashed arrows to represent the images of vertices, and colours to represent the image of edges (that can be inferred from $\varphi_V$).</figcaption></figure>

## 3.3 History-deterministic mappings

Locally bijective morphisms are a natural generalisation of the composition of a transition system with a deterministic automaton. They guarantee the semantic equivalence of the
two involved transition systems, but at the cost of the use of some strong hypothesis, as the outgoing edges of a vertex $v$ must exactly correspond to the outgoing edges of its image $\varphi(v)$. We can imagine correct transformations that do not satisfy this requirement. Notably, history-deterministic automata have been introduced as a method to bypass this restriction, with the hope of outperforming transformations that are witnessed by locally bijective morphisms. In general, if $\mathcal{A}$ is an HD automaton recognising the acceptance set of $\mathcal{T}\mathcal{S}$, the composition $\mathcal{T}\mathcal{S} \times \mathcal{A}$ does not admit a locally bijective morphism to $\mathcal{T}\mathcal{S}$, although it shares most semantic properties with it (Proposition 2.7).

We introduce next HD mappings, which are weak morphisms with the minimal set of hypothesis ensuring that, if $\varphi: \mathcal{T}\mathcal{S} \to \mathcal{T}\mathcal{S}'$ is an HD mapping, we can simulate runs of $\mathcal{T}\mathcal{S}'$ in $\mathcal{T}\mathcal{S}$ via $\varphi$ while preserving their acceptance. This will allow us to show that $\varphi$ witnesses the semantic equivalence of $\mathcal{T}\mathcal{S}$ and $\mathcal{T}\mathcal{S}'$ (Section 3.4).

<figure><img src="image_7.png" /><figcaption>Figure 6 Different types of morphisms and the relations between them. The fact that locally surjective morphisms are HD mappings is given by Lemma 3.12. Note that HD mappings are also locally surjective weak morphisms (Remark 3.7).</figcaption></figure>

## History-deterministic mappings

Let $\mathcal{T}\mathcal{S}$ and $\mathcal{T}\mathcal{S}'$ be transition systems and $\varphi: \mathcal{T}\mathcal{S} \to \mathcal{T}\mathcal{S}'$ a weak morphism between them. A resolver simulating $\varphi$ consists in a pair of functions $r_{\text{Init}}: I' \to I$ and $r: E^* \times E' \to E$ such that:

1. $\varphi(r_{\text{Init}}(v'_0)) = v'_0$ for all $v'_0 \in I'$,

2. $\varphi(r(\rho, e')) = e'$, for all $\rho \in E^*$ and $e' \in E'$,

3. if $e'_0 \in \text{Out}(I')$, $\text{Source}(r(\epsilon, e'_0)) = r_{\text{Init}}(\text{Source}(e'_0))$, and

4. if $\rho$ is a finite run in $\mathcal{T}\mathcal{S}$ ending in $v$ and $e' \in \text{Out}(\varphi(v))$, then $r(\rho, e') \in \text{Out}(v)$.

Given a run $\rho' = e'_0 e'_1 \cdots \in \mathcal{R}un^\infty(\mathcal{T}\mathcal{S}')$ starting in some $v'_0 \in I'$, the run induced by $r$ is the sequence $r_{\mathcal{R}uns}(\rho') = e_0 e_1 e_2 \cdots \in \mathcal{R}un^\infty(\mathcal{T}\mathcal{S})$ defined by $e_i = r(e_0 \dots e_{i-1}, e'_i)$, which is indeed a run in $\mathcal{T}\mathcal{S}$. We say that the resolver is *sound* if for every accepting run $\rho' \in \mathcal{R}un(\mathcal{T}\mathcal{S}')$, the run $r_{\mathcal{R}uns}(\rho')$ is accepting in $\mathcal{T}\mathcal{S}$. Note that we do not impose $r_{\mathcal{R}uns}(\rho')$ to be rejecting if $\rho'$ is.

**Remark 3.7.** Provided that all states of $\mathcal{T}\mathcal{S}'$ are accessible, a resolver simulating $\varphi$ can only exist if $\varphi$ is a locally surjective weak morphism.

Said differently, a sound resolver simulating $\varphi$ is a winning strategy for the player Duplicator in the following game:
- In round 0, Spoiler picks an initial vertex $v'_0$ in $\mathcal{T}\mathcal{S}'$. Duplicator responds by picking an initial vertex $v_0$ in $\mathcal{T}\mathcal{S}$ such that $\varphi(v_0) = v'_0$.

- In round $n > 0$, Spoiler picks an edge $e'_n$ in $\mathcal{T}\mathcal{S}'$, and Duplicator responds by picking an edge $e_n$ in $\mathcal{T}\mathcal{S}$ such that $\varphi(e_n) = e'_n$.

- Duplicator wins if either $e_1e_2\dots$ is an accepting run in $\mathcal{T}\mathcal{S}$ from $v_0$ or $e'_1e'_2\dots$ is not an accepting run in $\mathcal{T}\mathcal{S}'$ from $v'_0$ (it is either not a run from $v_0$ or not accepting). Spoiler wins otherwise.

**Definition 3.8.** Let $\mathcal{T}\mathcal{S}$ and $\mathcal{T}\mathcal{S}'$ be (labelled) transition systems. A history-deterministic mapping (HD mapping) of transition systems from $\mathcal{T}\mathcal{S}$ to $\mathcal{T}\mathcal{S}'$ is a pair of mappings $\varphi = (\varphi_V : V \to V', \varphi_E : E \to E')$ such that:

- $\varphi$ is a weak morphism,

- $\varphi$ preserves accepting runs: $\rho \in \mathcal{R}un(\mathcal{T}\mathcal{S})$ and $\gamma(\rho) \in \mathcal{W} \implies \gamma'(\varphi_{\mathcal{R}uns}(\rho)) \in \mathcal{W}',$ and

- there exists a sound resolver simulating $\varphi$.

Even if a history-deterministic mapping is not necessarily locally bijective (and not even a morphism of transition systems), the existence of a sound resolver allows to define a right inverse to $\varphi_{\mathcal{R}uns}$ preserving the acceptance of runs.

**Lemma 3.9.** Let $\varphi: \mathcal{T}\mathcal{S} \to \mathcal{T}\mathcal{S}'$ be an HD mapping and let $(r_{\text{Init}}, r)$ be a sound resolver simulating it. The following holds:

- $\varphi_{\mathcal{R}uns} \circ r_{\mathcal{R}uns} = \text{Id}_{\mathcal{R}un_{\infty}(\mathcal{T}\mathcal{S}')}$.

- $r_{\mathcal{R}uns}$ preserves the acceptance of runs in $\mathcal{T}\mathcal{S}'$, that is, for every run $\rho' \in \mathcal{R}un(\mathcal{T}\mathcal{S}')$, $\rho'$ is accepting if and only if $r_{\mathcal{R}uns}(\rho')$ is accepting in $\mathcal{T}\mathcal{S}$.

**Proof.** The first item follows from the fact that $\varphi(r(\rho, e')) = e'$ for every $\rho \in E^*$ and $e' \in E'$.

For the second item, the definition of a sound resolver imposes that if $\rho'$ is accepting, so is $r_{\mathcal{R}uns}(\rho')$. For the other direction, if $r_{\mathcal{R}uns}(\rho')$ is accepting, then $\varphi_{\mathcal{R}uns}(r_{\mathcal{R}uns}(\rho')) = \rho'$ has to be accepting, as an HD mapping preserves accepting runs. ◀

**Example 3.10.** In Figure 7 we give an example of a weak morphism $\varphi: \mathcal{T}\mathcal{S} \to \mathcal{T}\mathcal{S}'$ that is a history-deterministic mapping, but which is neither a morphism, nor locally bijective. Transition system $\mathcal{T}\mathcal{S}$, on the left of the figure, is a parity TS (more precisely, a coBüchi TS). Transition system $\mathcal{T}\mathcal{S}'$, depicted on the right of the figure, is a Muller TS using as acceptance set the Muller language associated to $\mathcal{F} = \{\{\alpha\}, \{\alpha, \beta\}, \{\alpha, \lambda\}\}$; that is, a run in $\mathcal{T}\mathcal{S}'$ is accepting if and only if it eventually avoids either transition $e'$ or transition $f'$. The weak morphism we propose is given by: $\varphi(v_0) = \varphi(v_1) = \varphi(v_2) = v'$, and $\varphi(u_1) = \varphi(u_2) = u'$. The image of most edges is uniquely determined, and we use colours to represent them. We have named the only edges whose image is not uniquely determined, and we define $\varphi(e_1) = \varphi(e_2) = e'$ and $\varphi(f_1) = \varphi(f_2) = f'$.

We remark that $\varphi$ does not preserve rejecting runs. Indeed, a run in $\mathcal{T}\mathcal{S}$ alternating between $v_0$ and $u_1$, taking transition $f_1$ infinitely often, is rejecting, but its image is accepting in $\mathcal{T}\mathcal{S}'$. However, $\varphi$ preserves accepting runs: a run is accepting in $\mathcal{T}\mathcal{S}$ if and only if it eventually stays in $\{v_1, u_1\}$ or in $\{v_2, u_2\}$. In the first case, the image under $\varphi$ avoids transition $f'$ in $\mathcal{T}\mathcal{S}'$, and in the second case, its image avoids transition $e'$.

Finally, we describe a sound resolver simulating $\varphi$. When simulating a run from $\mathcal{T}\mathcal{S}'$ in $\mathcal{T}\mathcal{S}$, we have a choice to make only when we are in state $v_0$. If the previous transition in $\mathcal{T}\mathcal{S}'$ was $e'$, we will go up, that is, $v' \xrightarrow{\alpha} u'$ is simulated by $v_0 \xrightarrow{1} u_1$ and $v' \xrightarrow{\alpha} v'$ is simulated by $v_0 \xrightarrow{1} v_1$. If the previous transition in $\mathcal{T}\mathcal{S}'$ was $f'$, we will go down in a symmetric manner. In this way, if transition $f'$ is eventually not visited by the run in $\mathcal{T}\mathcal{S}'$, we ensure to stay in $\{v_1, u_1\}$ in $\mathcal{T}\mathcal{S}$ (and symmetrically, we ensure to stay in $\{v_2, u_2\}$ if $e'$ is avoided in $\mathcal{T}\mathcal{S}'$). ▼
<figure><img src="image_8.png" /><figcaption>■ **Figure 7** A history-deterministic mapping from a parity TS to a Muller TS with acceptance set given by $\mathcal{F} = \{\{\alpha\}, \{\alpha, \beta\}, \{\alpha, \lambda\}\}$. We use dashed arrows to represent the images of vertices, and colours to represent the image of edges.</figcaption></figure>

## History-deterministic-for-games mappings

In the case of games, we need to slightly strengthen the definition of HD mappings to guarantee that, if there is a suitable mapping $\varphi: \mathcal{G} \to \mathcal{G}'$, then $\mathcal{G}$ and $\mathcal{G}'$ have the same winner. In order to show that if Eve wins $\mathcal{G}'$ then she wins $\mathcal{G}$, we need a method to transfer strategies in $\mathcal{G}'$ to $\mathcal{G}$. A regular resolver simulating $\varphi$ does not suffice to do this, as it does not take into account the partition into Eve and Adam vertices. We need to be able to simulate a play of $\mathcal{G}'$ in $\mathcal{G}$ in a two-players-game fashion, Adam's moves will be simulated by Adam, and Eve's moves by Eve. This idea leads to the notion of HD-for-games mapping.

Let $\mathcal{G}$ and $\mathcal{G}'$ be two games, and $\varphi: \mathcal{G} \to \mathcal{G}'$ be a weak morphism between them admitting a resolver $(r_{\text{Init}}, r)$ simulating $\varphi$. Given runs $\rho' = e'_0 e'_1 \dots \in \mathcal{R}un(\mathcal{G}')$ and $\rho = e_0 e_1 \dots \in \mathcal{R}un(\mathcal{G})$, we say that $\rho$ is *consistent with* $(r_{\text{Init}}, r)$ over $\rho'$ if:

1. Source($e_0$) = $r_{\text{Init}}$(Source($e'_0$)),

2. $\varphi(e_i) = e'_i$, and

3. for every finite prefix $e_0 e_1 \dots e_{n-1} \subseteq \rho$ ending in a vertex controlled by Eve, the next edge in $\rho$ is $e_n = r(e_0 \dots e_{n-1}, e'_n)$.

We remark that there exists at least one run consistent with $(r_{\text{Init}}, r)$ over $\rho'$, namely $r_{\mathcal{R}un}(\rho')$. We say that $(r_{\text{Init}}, r)$ is *sound for* $\mathcal{G}$ if it verifies that for any accepting run $\rho' \in \mathcal{R}un(\mathcal{G}')$, all runs consistent with $(r_{\text{Init}}, r)$ over $\rho'$ are accepting in $\mathcal{G}$.

Said differently, a resolver sound for $\mathcal{G}$ is a winning strategy for Duplicator in the following game:

- In round 0, Spoiler picks an initial vertex $v'_0$ in $\mathcal{G}'$. Duplicator responds by picking an initial vertex $v_0$ in $\mathcal{G}$ such that $\varphi(v_0) = v'_0$.

- In round $n > 0$, Spoiler picks an edge $e'_n$ in $\mathcal{G}'$. If $v_{n-1}$ is controlled by Adam, Spoiler chooses an edge $e_n = v_{n-1} \to v_n \in \text{Out}(v_{n-1})$ such that $\varphi(e_n) = e'_n$. If $v_n$ is controlled by Eve, it is Duplicator who chooses one such $e_n$.

- Duplicator wins if either $e_1 e_2 \dots$ is an accepting run in $\mathcal{G}$ from $v_0$ or $e'_1 e'_2 \dots$ is not an accepting run in $\mathcal{G}'$ from $v'_0$. Spoiler wins otherwise.
**► Definition 3.11.** An HD mapping of games $\varphi : \mathcal{G} \to \mathcal{G}'$ is called history-deterministic-for-games if it admits a resolver sound for $\mathcal{G}$.

Whenever we apply the term HD-for-games to a map $\varphi : \mathcal{TS} \to \mathcal{TS}'$, it will implicitly imply that $\mathcal{TS}$ and $\mathcal{TS}'$ are games (that is, they have a fixed vertex-labelling $l_{\text{Players}}: V \to \{\text{Eve}, \text{Adam}\}$), and that $\varphi$ preserves those vertex-labellings).

In the next lemma, we prove that HD and HD-for-games mappings are a strict generalisation of locally surjective morphisms (and therefore, also of locally bijective ones). On the other hand, we remark that HD mappings must be locally surjective, but they are not necessarily morphisms (they might not preserve rejecting runs).

**Lemma 3.12.** If $\varphi : \mathcal{TS} \to \mathcal{TS}'$ is a locally surjective morphism, it is also an HD mapping. If $\mathcal{TS}$ and $\mathcal{TS}'$ are games, $\varphi$ is moreover HD-for-games.

**Proof.** We need to define a sound resolver simulating $\varphi$. Let $r_{\text{Init}}: I' \to I$ be any function choosing initial vertices satisfying that $\varphi \circ r_{\text{Init}} = \text{Id}_{I'}$ (which exists by local surjectivity of $\varphi$). For each $v \in V$ and edge $e' \in \text{Out}(\varphi(v))$ we choose one edge $f(v, e') \in \text{Out}(v)$ such that $\varphi(f(v, e')) = e'$ (which exists by local surjectivity), and we let $r$ be the resolver induced by these choices. Formally, we define $r: E^* \times E' \to E$ recursively. For the base case, if $e'_0 \in \text{Out}(v')$, with $v' \in I'$, we define $r(\varepsilon, e'_0) = f(r_{\text{Init}}(v'), e'_0)$. Suppose that $r$ has been defined for runs of length $\le n$, and let $\rho \in E^*$ be of length $n+1$ and $e' \in E'$. If $\rho$ is not a run or $e' \notin \text{Out}(\text{Target}(\varphi(\rho)))$, we let $r(\rho, e')$ be any edge in $\varphi^{-1}(e')$. If not, let $v = \text{Target}(\rho)$ and we define $r(\rho, e')$ to be the edge $f(v, e')$.

It is straightforward to check that $(r_{\text{Init}}, r)$ is indeed a resolver (for every run $\rho' \in \mathcal{Run}(\mathcal{TS}')$, the sequence $r_{\mathcal{Run}(\rho')}$ is a run in $\mathcal{TS}$ and $\rho'$ is its image under $\varphi$). Finally, since $\varphi$ is a morphism, for every $\rho' \in \mathcal{Run}(\mathcal{TS}')$ and every $\rho \in \mathcal{Run}(\mathcal{TS})$ consistent with $(r_{\text{Init}}, r)$ over $\rho'$, $\rho$ is accepting in $\mathcal{TS}$ if and only if $\rho' = \varphi_{\mathcal{Run}(\rho)}(\rho)$ is accepting in $\mathcal{TS}'$. We conclude that $(r_{\text{Init}}, r)$ is a sound resolver (resp. sound for $\mathcal{TS}$) and therefore $\varphi$ is an HD mapping (resp. HD-for-games mapping).

**Restrictions and extensions of initial sets**

The following simple lemma states that reducing the number of initial vertices preserves the history-determinism of mappings.

**Lemma 3.13.** Let $\mathcal{TS}$ and $\mathcal{TS}'$ be two TS such that there is an HD (resp. HD-for-games) mapping $\varphi : \mathcal{TS} \to \mathcal{TS}'$. For any non-empty subset $\tilde{I} \subseteq I'$, $\varphi$ is also an HD (resp. HD-for-games) mapping between the transition systems $\mathcal{T}_{r_{\text{Init}}(\tilde{I})}$ and $\mathcal{T}_{\tilde{I}}'$; that is, the transitions systems obtained by setting $r_{\text{Init}}(\tilde{I})$ and $\tilde{I}$ as initial vertices, respectively.

For arbitrary acceptance conditions, enlarging the set of initial vertices does not preserve history-determinism. However, for transition systems using the acceptance conditions considered in this work, we can enlarge the set of initial vertices without loss of generality. The proof can be found in Appendix C.

**Lemma 3.14.** Let $\mathcal{TS}$ and $\mathcal{TS}'$ be two TS such that all their states are accessible, and let $\varphi : \mathcal{TS} \to \mathcal{TS}'$ 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}_{\mathcal{SV}}$ and $\mathcal{T}_{\mathcal{V}'}$, consisting of the transition systems $\mathcal{TS}$ and $\mathcal{TS}'$ where all the states are set to be initial.
## 3.4 Preservation of semantic properties of automata and games

We start this section by showing that locally bijective morphisms and HD mappings are a strict generalisation of compositions by deterministic and history-deterministic automata, respectively (Proposition 3.15). Then, we prove that these mappings witness the semantic equivalence of the transition systems under consideration. That is, (1) if $\varphi: A \to A'$ is an HD mapping of automata, then $\mathcal{L}(A) = \mathcal{L}(A')$, and if $\varphi$ is locally bijective, $A$ is deterministic (or unambiguous) if and only if $A'$ is (Proposition 3.16)<fnref n="5" />; and (2) if $\varphi: G \to G'$ is an HD-for-games mapping, $G$ and $G'$ have the same winner (Proposition 3.18 and Corollary 3.19).

### Morphisms generalise composition by an automaton

**Proposition 3.15.** Let $A$ be a complete automaton accepting the language $\mathcal{L}(A) = W \subseteq \Sigma^\omega$, and let $\mathcal{T}S$ be a (labelled) $\mathcal{T}S$ with acceptance set $W$. Then, there exists a locally surjective weak morphism of (labelled) $\mathcal{T}S$ $\varphi: \mathcal{T}S \times A \to \mathcal{T}S$ that preserves accepting runs. Moreover:

1. If $A$ is deterministic, $\varphi$ can be chosen to be a locally bijective morphism.

2. If $A$ is HD, then $\varphi$ can be chosen to be an HD mapping.

3. If $A$ is HD and $\mathcal{T}S$ is a game suitable for transformations, then $\varphi$ can be chosen to be an HD-for-games mapping.

**Proof.** We recall that the set of states of $\mathcal{T}S \times A$ is $V \times Q$ and its set of transitions $E^{\times}$ is a subset of $(E \times \Delta) \sqcup E$, where $V$ and $Q$ (resp. $E$ and $\Delta$) are the states (resp. transitions) of $\mathcal{T}S$ and $A$, respectively. We let $W_A \subseteq \Gamma^\omega$ be the acceptance set of $A$. We define $\varphi_V(v, q) = v$ and $\varphi_E(e_1, e_2) = e_1$ for $(e_1, e_2) \in E \times \Delta$ and $\varphi_E(e_1) = e_1$ for $e_1 \in E$. It is immediate to check that $\varphi$ is a weak morphism.

Given a run $\rho = (v_0, q_0) \xrightarrow{c_0} (v_1, q_1) \xrightarrow{c_1} \dots$ in $\mathcal{T}S \times A$, we can consider its projection over $\mathcal{T}S$, $\varphi_{\mathcal{R}uns}(\rho) = v_0 \xrightarrow{a_0} v_1 \xrightarrow{a_1} \dots$. We note that there must exist a unique run in $A$ of the form

$$ \varphi_A(\rho) = q_0 \xrightarrow{a_0:c_0} q_1 \xrightarrow{a_1:c_1} \dots $$

(Formally, some of the letters $a_i$ might equal $\varepsilon$, and in this case $q_i \xrightarrow{a_i:c_i} q_{i+1}$ does not appear in the run $\varphi_A(\rho)$).

We show that $\varphi$ preserves accepting runs. Let $\rho$ be an accepting run in $\mathcal{T}S \times A$. In that case, $c_0 c_1 c_2 \dots \in W_A$, and therefore $\varphi_A(\rho)$ is an accepting run in $A$ over $a_0 a_1 a_2 \dots$, so we conclude that $a_0 a_1 a_2 \dots \in W$ and $\varphi_{\mathcal{R}uns}(\rho)$ is an accepting run in $\mathcal{T}S$.

We prove next the local surjectivity of $\varphi$. Clearly, $\varphi$ induces a surjection between the initial vertices of $\mathcal{T}S \times A$ (which are $I_{\mathcal{T}S} \times I_A$) and those of $\mathcal{T}S$. Let $(v, q) \in V \times Q$ and $e_1 = v \xrightarrow{a} v' \in E$. If $a = \varepsilon$, the edge $e_1$ belongs to $E^{\times}$ and $\varphi(e_1) = e_1$. If $a \neq \varepsilon$, since $A$ is complete there is a transition $e_2 = q \xrightarrow{a} q' \in \Delta$ and $\varphi(e_1, e_2) = e_1$, so $\varphi$ is locally surjective.

1. Since $A$ has a single initial state $q_0$, $\varphi$ induces a bijection between the initial vertices of $\mathcal{T}S \times A$ (which are $I_{\mathcal{T}S} \times \{q_0\}$) and those of $\mathcal{T}S$. Let $E_{\text{col}}^{\times} \subseteq E \times \Delta$ and $E_{\varepsilon}^{\times} \subseteq E$ such that $E^{\times} = E_{\text{col}}^{\times} \cup E_{\varepsilon}^{\times}$. We remark that $\varphi|_{E_{\varepsilon}^{\times}}$ is the identity function (so injective) and that

<footnote n="5">⁵ The results in this section do not directly imply that if $A$ is an automaton recognising the acceptance set of another automaton $B$, then $B \times A$ recognises the same language than $B$, if $A$ is not history-deterministic (Proposition 2.6). In that case, the equality $\mathcal{L}(B \times A) = \mathcal{L}(B)$ follows from the idea that runs in $B$ can be simulated in $B \times A$ “guided by the non-deterministic choices of $A$”, which we do not formalise in this work.</footnote>
$\varphi(E_{\text{col}}^{\times}) \cap \varphi(E_{\varepsilon}^{\times}) = \emptyset$ because $\varphi(E_{\text{col}}^{\times})$ are exactly coloured transitions of $\mathcal{T}\mathcal{S}$. Finally, let $(e_1, e_2)$ and $(e'_1, e'_2)$ in $\text{Out}(v, q) \cap E_{\text{col}}^{\times}$. Their $\varphi(e_1, e_2) = \varphi(e'_1, e'_2)$ if and only if $e_1 = e'_1$. Let $a \in \Sigma$ be the colour of $e_1$. Since $\mathcal{A}$ is deterministic, there is at most one transition from $q$ labelled by $a$, that must be $e_2 = e'_2$. We conclude that $(e_1, e_2) = (e'_1, e'_2)$ and that $\varphi$ is locally injective.

Let $\rho$ be a rejecting run in $\mathcal{T}\mathcal{S} \times \mathcal{A}$ (we use the notations introduced above). In that case, $c_0, c_1, c_2 \notin W_{\mathcal{A}}$, and therefore $\varphi_{\mathcal{A}}(\rho)$ is a rejecting run over $a_0, a_1, a_2, \dots$. Since $\mathcal{A}$ is deterministic, this is the only run over $a_0, a_1, a_2, \dots$ so we conclude that it does not belong to $W$. We conclude that $\varphi_{\mathcal{R}_{\text{uns}}}(\rho)$ is a rejecting run in $\mathcal{T}\mathcal{S}$.

2. Let $(r_0, r_{\mathcal{A}})$ be a resolver for $\mathcal{A}$. We define a resolver $(r_{\text{Init}}, r_{\varphi})$ simulating $\varphi$. First, we let $r_{\text{Init}}(v_0) = (v_0, r_0)$ for all $v_0 \in I_{\mathcal{T}\mathcal{S}}$. We define $r_{\varphi}: E^{\times*} \times E \to E^{\times}$ by induction on the length of the runs. Let $e_0 = v_0 \xrightarrow{a} v_1 \in \text{Out}(v_0)$ be an edge in $\mathcal{T}\mathcal{S}$. If $e_0$ is uncoloured ($a = \varepsilon$), we let $r_{\varphi}(\varepsilon, e_0) = e_0 = (v_0, r_0) \xrightarrow{\varepsilon} (v_1, r_0)$. If not, we let $r_{\varphi}(\varepsilon, e_0) = (e_0, e_a)$, where $e_a = r(\varepsilon, a)$. Suppose that $r_{\varphi}$ has been defined for sequences of edges of $\mathcal{T}\mathcal{S} \times \mathcal{A}$ of length $< n$ and let $\rho = e_0 e_1 \dots e_{n-1} \in E^{\times*}$ be a sequence length $n+1$ and $e_{\mathcal{T}\mathcal{S}} = v_n \xrightarrow{a_n} v_{n+1}$ be an edge in $\mathcal{T}\mathcal{S}$. If $\rho$ is not a run or if it does not end in $\varphi^{-1}(v_n)$, we let $r_{\varphi}(\rho, e_{\mathcal{T}\mathcal{S}})$ be any edge in $\varphi^{-1}(e_{\mathcal{T}\mathcal{S}})$. Suppose that $\rho$ is a run ending in $\varphi^{-1}(v_n)$. If $a_n = \varepsilon$, we define $r_{\varphi}(\rho, e_{\mathcal{T}\mathcal{S}}) = e_{\mathcal{T}\mathcal{S}}$. As noted before, $\rho$ induces a run $\varphi_{\mathcal{A}}(\rho) = q_0 \xrightarrow{a_0:c_0} q_1 \xrightarrow{a_1:c_1} \dots \to q_n$ in $\mathcal{A}$. We let $e_{\mathcal{A}} = r_{\mathcal{A}}(\varphi_{\mathcal{A}}(\rho), a_n)$ be the transition chosen by the resolver of $\mathcal{A}$ after this run, and we define $r_{\varphi}(\rho, e_{\mathcal{T}\mathcal{S}}) = (e_{\mathcal{T}\mathcal{S}}, e_{\mathcal{A}})$.

It directly follows from this definition that $(r_{\text{Init}}, r_{\varphi})$ is indeed a resolver. The proof that if $\rho \in \mathcal{R}_{\text{un}}(\mathcal{T}\mathcal{S})$ is an accepting run then $r_{\varphi, \mathcal{R}_{\text{uns}}}(\rho)$ is accepting follows the same lines than the previous item.

3. We prove that, if $\mathcal{T}\mathcal{S}$ is a game suitable for transformations, the resolver $(r_{\text{Init}}, r_{\varphi})$ defined in the previous item is sound for $\mathcal{T}\mathcal{S}$. We claim that if $\rho$ is a run in $\mathcal{T}\mathcal{S}$, the only run consistent with $(r_{\text{Init}}, r_{\varphi})$ over $\rho$ is $r_{\varphi, \mathcal{R}_{\text{uns}}}(\rho)$. This follows from the fact that if $(v, q)$ is a vertex in $\mathcal{T}\mathcal{S} \times \mathcal{A}$ controlled by Adam and $e \in \text{Out}(v)$, then there is a unique $e' \in \text{Out}(v, q)$ such that $\varphi(e') = e$. This is indeed the case: as $\mathcal{T}\mathcal{S}$ is suitable for transformations, if $v$ is an Adam's vertex, every $e \in \text{Out}(v)$ is uncoloured, so by definition of $\varphi$ we have that $\varphi(e') = e \implies e' = e$. (This can be seen as that $\varphi$ is locally bijective in Adam's vertices). We conclude that if $\rho$ is an accepting run in $\mathcal{T}\mathcal{S}$ and $\rho^{\times}$ is a run consistent with $(r_{\text{Init}}, r_{\varphi})$ over $\rho$, then $\rho^{\times} = r_{\varphi, \mathcal{R}_{\text{uns}}}(\rho)$, which is accepting by soundness of the resolver $(r_{\text{Init}}, r_{\varphi})$. $\quad$

## Morphisms witness equivalence of automata

**Proposition 3.16.** Let $\mathcal{A}, \mathcal{A}'$ be two automata over the same input alphabet such that there is an HD mapping of automata $\varphi: \mathcal{A} \to \mathcal{A}'$. Then, $\mathcal{L}(\mathcal{A}) = \mathcal{L}(\mathcal{A}')$, and $\mathcal{A}$ is HD if and only if $\mathcal{A}'$ is HD. If $\varphi$ is moreover locally bijective and surjective, $\mathcal{A}$ is deterministic (resp. complete) if and only if $\mathcal{A}'$ is.

*Proof.* Since $\varphi$ preserves accepting runs, it is clear that $\mathcal{L}(\mathcal{A}) \subseteq \mathcal{L}(\mathcal{A}')$. Since $\varphi$ admits a sound resolver $(r_{\text{Init}}, r)$, if $\rho$ is an accepting run over $w \in \Sigma^\omega$ in $\mathcal{A}'$, then $r_{\mathcal{R}_{\text{uns}}}(\rho)$ is an accepting run over $w$ in $\mathcal{A}$, so $\mathcal{L}(\mathcal{A}') \subseteq \mathcal{L}(\mathcal{A})$.

Let $(r_{\text{Init}}, r_{\varphi})$ be a sound resolver simulating $\varphi$. Suppose that $\mathcal{A}$ is HD, admitting a resolver $(r_0, r)$. A resolver $(r'_0, r')$ for $\mathcal{A}'$ can be obtained just by composing $r_{\varphi}$ and $\varphi$, that is: $r'_0 = \varphi(r_0)$ and for $\rho' \in \mathcal{R}_{\text{un}}^{\text{fin}}(\mathcal{A}')$ and $a \in \Sigma$, $r'(\rho', a) = \varphi(r_{\varphi, \mathcal{R}_{\text{uns}}}(\rho'), a))$. That is, given a run $\rho'$ in $\mathcal{A}'$, we simulate it in $\mathcal{A}$ using $r_{\varphi}$, then, we look at what is the continuation proposed by the resolver $r$ when we give the letter $a$, and we transfer back this choice to $\mathcal{A}'$ using $\varphi$. Suppose now that $\mathcal{A}'$ is HD and that $(r'_0, r')$ is a resolver for it.
We define a resolver $(r_0, r)$ for $\mathcal{A}$. We let $r_0 = r_{\text{Init}}(r'_0)$, and for $\rho \in \mathcal{R}_{\text{unfin}}(\mathcal{A})$ and $a \in \Sigma$, $r(\rho, a) = r_{\varphi}((\varphi_{\mathcal{R}_{\text{uns}}}(\rho), r(\varphi_{\mathcal{R}_{\text{uns}}}(\rho), a)))$. That is, given a run $\rho$ in $\mathcal{A}$, we simulate it in $\mathcal{A}'$ using $\varphi$, then, we look at what is the continuation proposed by the resolver $r'$ when we give the letter $a$, and we transfer back this choice to $\mathcal{A}$ using $r_{\varphi}$. It is a direct check that the resolvers defined this way witness that $\mathcal{A}'$ and $\mathcal{A}$, respectively, are HD.

The proof that $\mathcal{A}$ is deterministic (resp. complete) if and only if $\mathcal{A}'$ is deterministic (resp. complete), assuming surjectivity and local bijectivity of $\varphi$, follows the same lines. ◀

A subclass of automata with a restrictive amount of non-determinism that is widely
study is that of unambiguous automata (we refer to [23, 16] for a detailed exposition). An
automaton is unambiguous if for every input word $w \in \Sigma^\omega$ there is at most one accepting run
over $w$, and it is strongly unambiguous if there is at most one run over $w$. By Remark 3.4,
locally bijective morphisms also preserve (strongly) unambiguity: if $\varphi: \mathcal{A} \to \mathcal{A}'$ is a locally
bijective morphism then $\mathcal{A}$ is (strongly) unambiguous if and only if $\mathcal{A}'$ is.

Morphisms preserve winning regions of games

**► Lemma 3.17.** Let $\mathcal{G}, \mathcal{G}'$ be two games, such that there is a weak morphism of games $\varphi: \mathcal{G} \to \mathcal{G}'$ that is locally surjective and preserves accepting runs. If Eve wins the game $\mathcal{G}$ from an initial vertex $v$, then she wins $\mathcal{G}'$ from $\varphi(v)$.

**Proof.** Let $v' = \varphi(v)$, and let $\mathbf{strat}_v: \mathcal{Path}_v^{\text{fin}}(\mathcal{G}) \to E$ be a strategy from $v$ for Eve in $\mathcal{G}$. Intuitively, we will define a strategy in $\mathcal{G}'$ as follows: for each finite run $\rho'$ from $v'$ in $\mathcal{G}'$, we pick a preimage $\rho \in \varphi^{-1}(\rho')$ in $\mathcal{G}$, look at the decision made by $\mathbf{strat}_v$ at the end of $\rho$ and transfer it back to $\mathcal{G}'$ via $\varphi$. In order to define a correct strategy, the choices of the preimages have to be made in a coherent manner. We formalise this idea next.

We will make use of a function $\mathbf{choice}_{st}: \mathcal{Path}_{v'}^{\text{fin}}(\mathcal{G}') \to \mathcal{Path}_v^{\text{fin}}(\mathcal{G})$ satisfying that for any $\rho' = e'_0 e'_1 \dots e'_{n-1} e'_n \in \mathcal{Path}_{v'}^{\text{fin}}(\mathcal{G}')$:

- The run $\mathbf{choice}_{st}(\rho')$ has length $n+1$.

- $\varphi_{\mathcal{R}_{\text{uns}}}(\mathbf{choice}_{st}(\rho')) = \rho'$.

- Monotonicity: if $\tilde{\rho}' \subseteq \rho'$ then $\mathbf{choice}_{st}(\tilde{\rho}') \subseteq \mathbf{choice}_{st}(\rho')$.

- If there exists $e_n \in \varphi^{-1}(e'_n)$ such that $\mathbf{choice}_{st}(e'_0 e'_1 \dots e'_{n-1}) e_n$ is consistent with $\mathbf{strat}_v$, then $\mathbf{choice}_{st}(\rho')$ is consistent with $\mathbf{strat}_v$.

Assume for now that such a function exists, and define a strategy in $\mathcal{G}'$ as

$$
\mathbf{strat}'_{v'}(\rho') = \varphi(\mathbf{strat}_v(\mathbf{choice}_{st}(\rho'))), \text{ for } \rho' \in \mathcal{Path}_{v'}^{\text{fin}}(\mathcal{G}').
$$

We prove that $\mathbf{strat}'_{v'}$ is winning. Let $\rho' = e'_0 e'_1 \cdots \in \mathcal{R}_{\text{un}}(\mathcal{G}')$ be an infinite play consistent with $\mathbf{strat}'_{v'}$. For each finite prefix $\tilde{\rho}' \subseteq \rho'$, $\mathbf{choice}_{st}(\tilde{\rho}')$ is a finite play in $\mathcal{G}$, and by the monotonicity assumption, we can define the limit of these runs as:

$$
\vec{\rho} = e_0 e_1 e_2 \cdots \in \mathcal{R}_{\text{un}}(\mathcal{G}), \text{ where } e_0 e_1 \cdots e_n = \text{choice}_{st}(e'_0 e'_1 \cdots e'_n),
$$

which is indeed a run in $\mathcal{G}$. We show that $\vec{\rho}$ is consistent with $\mathbf{strat}_v$ by induction. Let $\rho_n = e_0 e_1 \dots e_{n-1}$ be the prefix of size $n$ of $\vec{\rho}$, and suppose that it ends in a vertex $v_n$ controlled by Eve. We want to show that $e_n = \mathbf{strat}_v(\rho_n)$. By definition of $\mathbf{strat}'_{v'}$, $e'_n = \varphi(\mathbf{strat}_v(\rho_n)) = \varphi(e_n)$, and as $v_n$ is controlled by Eve, $\mathbf{strat}_v(\rho_n)$ is the only continuation of $\rho_n$ consistent with $\mathbf{strat}_v$, so by the last property of $\mathbf{choice}_{st}$, $e_n$ has to coincide with $\mathbf{strat}_v(\rho_n)$, as we wanted. As $\vec{\rho}$ is consistent with the winning strategy $\mathbf{strat}_v$, it is an accepting run in $\mathcal{G}$, and since $\varphi$ preserves accepting runs, $\rho' = \varphi_{\mathcal{R}_{\text{uns}}}(\vec{\rho})$ is also an accepting run.
Finally, we show how to build a function choice<sub>st</sub> : $Path_{v'}^{fin}(G') \to Path_{v}^{fin}(G)$ by induction on the length of the runs. Suppose that choice<sub>st</sub> has been defined for runs of length $\le n$, and let $e'_0 e'_1 \dots e'_n$ be a run of length $n+1$, with choice<sub>st</sub>($e'_0 e'_1 \dots e'_{n-1}$) = $e_0 e_1 \dots e_{n-1}$. If $e_0 e_1 \dots e_{n-1}$ is not consistent with strat<sub>v</sub>, it ends in a vertex $v_n$ controlled by Adam, or strat<sub>v</sub>($e_0 e_1 \dots e_{n-1}$) /\notin $\varphi^{-1}(e_n)$, we let $e_n \in \varphi^{-1}(e_n) \cap \text{Out}(v_n)$ be any edge (one such edge exists by local surjectivity). On the contrary, we let $e_n = \text{strat}_v(e_0 e_1 \dots e_{n-1})$. We define choice<sub>st</sub>($e'_0 e'_1 \dots e'_{n-1} e'_n$) = $e_0 e_1 \dots e_{n-1} e_n$. By construction, the obtained function fulfils the 4 requirements. ◀

**Proposition 3.18.** Let $G, G'$ be two games such that there is an HD-for-games mapping $\varphi: G \to G'$. Eve's winning region in $G'$ is the projection of her winning region in $G: W_{\text{Eve}}(G') = \varphi(W_{\text{Eve}}(G))$.

**Proof.** If Eve wins $G$ from an initial vertex $v$, Lemma 3.17 guarantees that she wins $G'$ from $\varphi(v)$.

Suppose now that Eve wins $G'$ from an initial vertex $v'$ with a strategy strat'$_{v'}$: $Path_{v'}^{fin}(G') \to E'$. We need to show that she wins $G$ from some initial vertex in $\varphi^{-1}(v')$. Let $(r_{\text{Init}}, r)$ be a resolver simulating $\varphi$ sound for $G$ and let $v = r_{\text{Init}}(v')$. We define

$$ \text{strat}_v(\rho) = r(\rho, \text{strat}'_{v'}(\varphi_{\text{Runs}}(\rho))), \text{ for } \rho \in \mathcal{P}\text{ath}_v^{\text{fin}}(G). $$

That is, strat<sub>v</sub> is a strategy in $G$ from $v$ that, given a finite run $\rho$, simulates $\rho$ in $G'$, looks at the move done by the strategy strat'$_{v'}$, in there, and transfers this choice back to $G'$ by using the resolver $r$. We prove that strat<sub>v</sub> is winning for Eve in $G$. Let $\rho = e_0 e_1 \dots \in Path_v(G)$ be a play consistent with strat<sub>v</sub>. We claim that $\varphi(\rho)$ is consistent with strat'$_{v'}$, and that $\rho$ is consistent with $(r_{\text{Init}}, r)$ over $\varphi(\rho)$. This implies the desired result; consistency with strat'$_{v'}$ implies that $\varphi(\rho)$ is accepting, and since $(r_{\text{Init}}, r)$ is sound for $G$, $\rho$ would be accepting in $G$.

We prove that $\varphi(\rho)$ is consistent with strat'$_{v'}$. Let $e'_0 e'_1 \dots e'_{n-1}$ be a subplay of $\varphi(\rho)$ ending in a vertex $v_n$ controlled by Eve. By definition of the strategy strat<sub>v</sub>, we have that $e_n = r(e_0 \dots e_{n-1}, \text{strat}'_{v'}(e'_0 \dots e'_{n-1}))$, and by definition of a resolver (item 2), $e'_n = \varphi(e_n) = \text{strat}'_{v'}(e'_0 \dots e'_{n-1})$, as we wanted.

The fact that $\rho$ is consistent with $(r_{\text{Init}}, r)$ over $\varphi(\rho)$ follows directly from the definition of strat<sub>v</sub>. ◀

The next corollary follows from the previous proposition and Lemma 3.14.

**Corollary 3.19.** Let $G, G'$ be two games whose states are accessible and such that their acceptance sets $W_G$ and $W_{G'}$ are prefix-independent. If there is an HD-for-games mapping $\varphi: G \to G'$, then Eve's full winning region in $G'$ is the projection of her full winning region in $G: W_{\text{Eve}}(G') = \varphi(W_{\text{Eve}}(G))$.

# 4 The Zielonka tree: An optimal approach to Muller languages

In this section, we take a close look into the Zielonka tree, a structure introduced (under the name of split trees) to study Muller languages [81]. We show how to use the Zielonka tree to construct minimal deterministic parity automata and minimal history-deterministic Rabin automata recognising Muller languages. In Section 4.2, we describe the construction of a minimal deterministic parity automaton $A_{\mathbb{Z}_F}^{\text{parity}}$ for a given Muller language Muller($\mathcal{F}$). Theorem 4.13, the main contribution of this section, states the minimality of $A_{\mathbb{Z}_F}^{\text{parity}}$ both amongst deterministic and HD parity automata. Theorem 4.12 states the optimality on the number of colours of the acceptance condition of $A_{\mathbb{Z}_F}^{\text{parity}}$, and implies that we can determine
the parity index of a Muller language from its Zielonka tree. We will use the optimality of automaton $A_{Z_F}^{\text{parity}}$ to provide a polynomial-time algorithm minimising DPAs recognising Muller languages in Section 6.3.

In Section 4.3, we describe the construction of a minimal history-deterministic Rabin automaton $A_{Z_F}^{\text{Rabin}}$ for a Muller language Muller($\mathcal{F}$). Its minimality amongst HD automata is shown in Theorem 4.48, by using the characterisation of the memory requirements of a Muller language in terms of its Zielonka tree [28].

On the other hand, it has been shown that finding a minimal deterministic Rabin automaton recognising a given Muller language is NP-complete, if the language is represented by a parity or Rabin automaton, or even by its Zielonka tree [17]. Therefore, unless $P = NP$, there are Muller languages for which minimal deterministic Rabin automata are strictly larger than minimal HD Rabin automata. Some explicit such languages were shown in [19, Section 4]. A summary of the minimal automata recognising Muller languages appears in Table 1.

<table><caption>Table 1 Minimal automata recognising a Muller language Muller($\mathcal{F}$), according to the type of acceptance condition (parity or Rabin) and the form of determinism.</caption><thead><tr><th>Type of automata</th><th>Deterministic</th><th>History-deterministic</th></tr></thead><tbody><tr><td>Parity</td><td>$A_{Z_F}^{\text{parity}}$</td><td>$A_{Z_F}^{\text{parity}}$</td></tr><tr><td>Rabin</td><td>NP-complete</td><td>$A_{Z_F}^{\text{Rabin}}$</td></tr></tbody></table>

## 4.1 The Zielonka tree

**► Definition 4.1** ([81]). Let $\mathcal{F} \subseteq 2_+^\Sigma$ be a family of non-empty subsets over a finite set $\Sigma$. A Zielonka tree for $\mathcal{F}$ (over $\Sigma$)$^6$, denoted $\mathcal{Z}_F = (N, \preceq, \nu : N \to 2_+^\Sigma)$ is a $2_+^\Sigma$-labelled tree with nodes partitioned into round nodes and square nodes, $N = N_\circ \sqcup N_\square$, such that:

- The root is labelled $\Sigma$.

- If a node is labelled $X \subseteq \Sigma$, with $X \in \mathcal{F}$, then it is a round node, and it has a child for each maximal non-empty subset $Y \subseteq X$ such that $Y \notin \mathcal{F}$, which is labelled $Y$.

- If a node is labelled $X \subseteq \Sigma$, with $X \notin \mathcal{F}$, then it is a square node, and it has a child for each maximal non-empty subset $Y \subseteq X$ such that $Y \in \mathcal{F}$, which is labelled $Y$. ▼

**► Remark 4.2.** We note that for each family of subsets $\mathcal{F} \subseteq 2_+^\Sigma$, there is only one Zielonka tree up to renaming of its nodes, so we will talk of the Zielonka tree of $\mathcal{F}$.

**► Remark 4.3.** We remark that if $n$ is a node of $\mathcal{Z}_F$, then the subtree of $\mathcal{Z}_F$ rooted at $n$ is the Zielonka tree for the family $\mathcal{F}|_{\nu(n)}$ over the alphabet $\nu(n)$, that is, for the restriction of $\mathcal{F}$ to the subsets included in the label of $n$. ▼

**► Remark 4.4.** Let $n$ be a node of $\mathcal{Z}_F$ and let $n_1$ be a child of it. If $\nu(n_1) \subseteq X \subseteq \nu(n)$, then $\nu(n_1) \in \mathcal{F} \iff X \notin \mathcal{F} \iff \nu(n) \notin \mathcal{F}$. In particular, if $n_1, n_2$ are two different children of $n$, then $\nu(n_1) \in \mathcal{F} \iff \nu(n_2) \in \mathcal{F} \iff \nu(n_1) \cup \nu(n_2) \notin \mathcal{F}$. ▼

<footnote n="6">⁶ The definition of $\mathcal{Z}_F$, as well as most subsequent definitions, do not only depend on $\mathcal{F}$ but also on the alphabet $\Sigma$. Although this dependence is important, we do not explicitly include it in the notations in order to lighten them, as most of the times the alphabet will be clear from the context.</footnote>
We equip Zielonka trees with an order to navigate in them. That is, we equip each set $Children_{\mathcal{Z}_F}(n)$ with a total order, making $\mathcal{Z}_F$ an ordered tree. The precise order considered will be irrelevant for our purposes. From now on, we will suppose that all Zielonka trees are ordered, without explicitly mentioning it.

For a leaf $l \in \text{Leaves}(\mathcal{Z}_F)$ and a letter $a \in \Sigma$ we define $\text{Supp}(l, a) = n$ to be the deepest ancestor of $l$ (maximal for $\leq$) such that $a \in \nu(n)$.

**► Example 4.5.** We will use the Muller language associated to the following family of subsets as a running example throughout the paper. Let $\Sigma = \{a, b, c\}$ and let $\mathcal{F}$ be:

$$ \mathcal{F} = \{\{a, b\}, \{a, c\}, \{b\}\}. $$

In Figure 8 we show the Zielonka tree of $\mathcal{F}$. We use Greek letters (in pink) to name the nodes of the tree. Integers appearing on the right of the tree will be used in next section.

We have that $\text{Supp}(\xi, c) = \lambda$ and $\text{Supp}(\xi, b) = \alpha$. Also, $\text{Jump}(\xi, \lambda) = \zeta$ is the leaf reached by going from $\xi$ to $\lambda$, then changing to the next branch (in a cyclic way) and re-descend by taking the leftmost path. Similarly, $\text{Jump}(\xi, \alpha) = \theta$.

The subtree rooted at $\lambda$ contains the nodes $\{\lambda, \xi, \zeta\}$. We note that this is the Zielonka tree of $\mathcal{F}|_{\{a,c\}} = \{\{a, c\}\}$ (over the alphabet $\{a, c\}$).

<figure><img src="image_9.png" /><figcaption>■ Figure 8 Zielonka tree $\mathcal{Z}_F$ for $\mathcal{F} = \{\{a, b\}, \{a, c\}, \{b\}\}$.</figcaption></figure>

## 4.2 A minimal deterministic parity automaton

We present next the Zielonka-tree-parity-automaton, a minimal deterministic parity automaton for a Muller language $\text{Muller}(\mathcal{F})$ built from the Zielonka tree $\mathcal{Z}_F$. Our construction will furthermore let us determine the parity index of the language $\text{Muller}(\mathcal{F})$ from its Zielonka tree.

### 4.2.1 The Zielonka-tree-parity-automaton

We associate a non-negative integer to each level of a Zielonka tree $\mathcal{Z}_F = (N, \leq, \nu)$. We let $p_Z : N \to \mathbb{N}$ be the function defined as:

- if $\Sigma \in \mathcal{F}$, $p_Z(n) = \text{Depth}(n)$,

- if $\Sigma \notin \mathcal{F}$, $p_Z(n) = \text{Depth}(n) + 1$.

We let $\min_F$ (resp. $\max_F$) be the minimum (resp. maximum) value taken by the function $p_Z$.

**► Remark 4.6.** A node $n$ in the Zielonka tree $\mathcal{Z}_F$ verifies that $p_Z(n)$ is even if and only if $\nu(n) \in \mathcal{F}$. If $\Sigma \in \mathcal{F}$, $\min_F = 0$ and $\max_F$ equals the height of the Zielonka tree minus one. If $\Sigma \notin \mathcal{F}$, $\min_F = 1$ and $\max_F$ equals the height of the Zielonka tree.
**Example 4.7.** The Muller language from Example 4.5 satisfies $\Sigma \notin \mathcal{F}$. The values taken by the function $p_Z$ are represented at the right of the Zielonka tree in Figure 8. We have $p_Z(\alpha) = 1$, $p_Z(\beta) = p_Z(\lambda) = 2$ and $p_Z(\theta) = p_Z(\xi) = p_Z(\zeta) = 3$, so $\min_{\mathcal{F}} = 1$ and $\max_{\mathcal{F}} = 3$.

**Definition 4.8 (Zielonka-tree-parity-automaton).** Given a family of non-empty subsets $\mathcal{F} \subseteq 2_+^\Sigma$, we define the ZT-parity-automaton $\mathcal{A}_{\mathcal{Z}_\mathcal{F}}^{\text{parity}} = (Q, \Sigma, q_0, [\min_{\mathcal{F}}, \max_{\mathcal{F}}], \delta, \text{parity})$ as the deterministic parity automaton given by:

- $Q = \text{Leaves}(\mathcal{Z}_\mathcal{F})$,

- $q_0$ is the leftmost leaf of $\mathcal{Z}_\mathcal{F}^7$,

- The transition reading $a \in \Sigma$ from $q \in Q$ goes to $\text{Jump}(q, \text{Supp}(q, a))$ and produces $p_Z(\text{Supp}(q, a))$ as output, that is,

$$ \delta(q, a) = (\text{Jump}(q, \text{Supp}(q, a)), p_Z(\text{Supp}(q, a))). \quad \llap{\text{}}$$

Intuitively, the transitions of the automaton are determined as follows: if we are in a leaf $l$ and we read a colour $a$, then we move up in the branch of $l$ until we reach a node $n$ that contains the letter $a$ in its label. Then we pick the child of $n$ just on the right of the branch that we took before (in a cyclic way) and we move to the leftmost leaf below it. The colour produced as output is $p_Z(n)$, determined by the depth of $n$.

**Example 4.9.** In Figure 9 we show the ZT-parity-automaton $\mathcal{A}_{\mathcal{Z}_\mathcal{F}}^{\text{parity}}$ of the family of subsets from Example 4.5.

<figure><img src="image_10.png" /><figcaption>■ **Figure 9** ZT-parity-automaton recognising the Muller language associated to $\mathcal{F} = \{\{a, b\}, \{a, c\}, \{b\}\}$.</figcaption></figure>

### Correctness of the Zielonka-tree-parity-automaton

**Proposition 4.10 (Correctness).** Let $\mathcal{F} \subseteq 2_+^\Sigma$ be a family of non-empty subsets. Then,

$$ \mathcal{L}(\mathcal{A}_{\mathcal{Z}_\mathcal{F}}^{\text{parity}}) = \text{Muller}_{\Sigma}(\mathcal{F}). $$

That is, a word $w \in \Sigma^\omega$ is accepted by $\mathcal{A}_{\mathcal{Z}_\mathcal{F}}^{\text{parity}}$ if and only if $\text{Inf}(w) \in \mathcal{F}$.

The following useful lemma follows directly from the definition of $\text{Supp}$ and $\text{Jump}$.

**Lemma 4.11.** Let $q$ be a leaf of $\mathcal{Z}_\mathcal{F}$ and let $n$ be a node above $q$. Then, $\text{Supp}(q, a)$ is a descendant of $n$ if and only if $a \in \nu(n)$, and in this case, $\text{Jump}(q, \text{Supp}(q, a))$ is a descendant of $n$ too.

<footnote n="7">⁷ Any state can be chosen as initial state (see Lemma 2.5).</footnote>
**Proof of Proposition 4.10.** Let $w = w_0w_1w_2\cdots \in \Sigma^\omega$ be an infinite word. For $i > 0$, let $q_i$ be the leaf of $\mathcal{Z}_F$ reached after the (only) run over $w_0w_1\dots w_{i-1}$ in $A_{\mathcal{Z}_F}^{\text{parity}}$. For $i \ge 0$ let $n_i = \text{Supp}(q_i, w_i)$ be the “intermediate node” used to determine the next state and the output colour of each transition, and let $c_i = p_Z(n_i) = \gamma(q_i, w_i) \in [\min_F, \max_F]$ be that output colour (the output of the run over $w$ being therefore $c_0c_1c_2\cdots \in \mathbb{N}^\omega$). Let $q_\infty$ be a node appearing infinitely often in the sequence $q_0q_1q_2\dots$, and let $n_w$ be the deepest ancestor of $q_\infty$ such that $\text{Inf}(w) \subseteq \nu(n_w)$.

▷ Claim 4.10.1. There is $K \in \mathbb{N}$ such that for all $i \ge K$, $q_i \supseteq n_w$ and $\text{Supp}(q_i, w_i) \supseteq n_w$. In particular, $c_i \ge p_Z(n_w)$ for $i \ge K$.

*Proof.* Let $K \in \mathbb{N}$ be a position such that $w_i \in \text{Inf}(w)$ for all $i \ge K$ and $q_K = q_\infty$. The claim follows from Lemma 4.11 and induction. ▲

▷ Claim 4.10.2. Let $n_{w,1}, \dots, n_{w,s}$ be an enumeration of $\text{Children}_{\mathcal{Z}_F}(n_w)$ from left to right. It is verified that:

1. $\text{Supp}(q_i, w_i) = n_w$ infinitely often. In particular, $c_i = p_Z(n_w)$ for infinitely many $i$'s.

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

*Proof.* We first remark that for all $n_{w,k}$ there are arbitrarily large positions $i$ such that $q_i$ is not below $n_{w,k}$. Suppose by contradiction that this is not the case. Then, for all $i$ sufficiently large we have that $\text{Supp}(q_i, w_i) \supseteq n_{w,k}$, and by Lemma 4.11, $\text{Inf}(w) \subseteq \nu(n_{w,k})$. In particular, $q_\infty$ is below $n_{w,k}$, contradicting the fact that $n_w$ is the deepest ancestor of $q_\infty$ containing $\text{Inf}(w)$.

Let $K$ be like in the Claim 4.10.1. We show that if $i \ge K$ and $q_i \supseteq n_{w,k}$, then there is $j > i$ such that $w_j \notin \nu(n_{w,k})$, $\text{Supp}(q_j, w_j) = n_w$ and $q_{j+1} \supseteq n_{w,k+1}$ (by an abuse of notation we let $s+1=1$). It suffices to consider the least $j \ge i$ such that $\text{Supp}(q_j, w_j) \not\supseteq n_{w,k}$ (which exists by the previous remark). Since $\text{Inf}(w) \subseteq \nu(n_w)$ we have that $\text{Supp}(q_j, w_j) = n_w$, so $w_j \notin \nu(n_{w,j})$ (by Lemma 4.11) and by definition of the transitions of $A_{\mathcal{Z}_F}^{\text{parity}}$, $q_{j+1}$ will be a leaf below $n_{w,k+1}$.

The fact that $q_{j+1} \supseteq n_{w,k+1}$ implies that for any child $n_{w,k'}$, infinitely many states $q_i$ will be below $n_{w,k'}$ (we go around the children in a round-robin fashion). Therefore, for any $k$, there are arbitrarily large $j$ such that $w_j \notin \nu(n_{w,j})$ and $\text{Supp}(q_j, w_j) = n_w$, implying both items in the claim. ▲

Combining both claims, we obtain that the minimum of the colours that are produced as output infinitely often is $p_Z(n_w)$. By Remark 4.6, $p_Z(n_w)$ is even if and only if $n_w$ is a round node (if $\nu(n_w) \in \mathcal{F}$). It remains to show that $\text{Inf}(w) \in \mathcal{F}$ if and only if $\nu(n_w) \in \mathcal{F}$, which holds by the second item in Claim 4.10.2 and Remark 4.4. ◀

### 4.2.2 Optimality of the Zielonka-tree-parity-automaton

We now state and prove the main results of this section: the optimality of the ZT-parity-automaton in both number of states (Theorem 4.13) and number of colours of the acceptance condition (Theorem 4.12). The minimality of the ZT-parity-automaton comes in two version. A weaker one states its minimality only amongst deterministic automata (Theorem 4.16), and a stronger one states its minimality amongst all history-deterministic automata (Theorem 4.13). Although the weaker version is implied by the stronger one, we find it instructive to provide a proof for this easier case. The proof of the stronger statement is one of the most technical parts of the paper, but the argument used in its proof is just a careful refinement of the ideas appearing in the weaker version.
## Statement of the results

**Theorem 4.12** (Optimality of the parity condition). *The parity index of a Muller language Muller$_Σ$(F) is [min$_F$, max$_F$]. That is, the ZT-parity-automaton of Muller$_Σ$(F) uses the optimal number of colours to recognise this language.*

**Theorem 4.13** (Minimality of the ZT-parity-automaton). *Let $\mathcal{A}$ be a history-deterministic parity automaton recognising a Muller language Muller$_Σ$(\mathcal{F})$. Then, $|\mathcal{A}_{\mathcal{Z}_F}^{\text{parity}}| \le |\mathcal{A}|$.*

**Corollary 4.14.** For every Muller language $L$, a minimal deterministic parity automaton recognising $L$ has the same size than a minimal HD parity automaton recognising $L$.

We remark that, nonetheless, there are non-trivial HD parity automata recognising Muller languages. The automaton provided in Example 2.3 is an HD coBüchi automaton recognising a Muller language that cannot be made deterministic just by removing transitions. We note that the (deterministic) ZT-parity-automaton for this Muller language has only 2 states.

We say that an automaton $\mathcal{A}$ is *determinisable by prunning* if there is a subset $\Delta' \subseteq \Delta$ of its transitions and an initial state $q_0$ such that the subautomaton induced by $\Delta'$ with initial state $q_0$ is deterministic and recognises $\mathcal{L}(\mathcal{A})$.

**Proposition 4.15.** There exists an HD parity automaton recognising a Muller language that is not determinisable by prunning.

## Optimality of the parity condition

**Proof of Theorem 4.12.** Let $L = \text{Muller}_\Sigma(\mathcal{F})$. The ZT-parity-automaton of $L$ is a parity automaton recognising $L$ using colours in $[\min_F, \max_F]$, therefore, the parity index of $L$ is at most $[\min_F, \max_F]$.

To prove that the parity index is not less than $[\min_F, \max_F]$, we use the Flower Lemma 2.16. The language $L$ is trivially recognised by a deterministic Muller automaton $\mathcal{A}_L$ with just one state $q$, transitions $q \xrightarrow{a:a} q$ for each $a \in \Sigma$, and acceptance condition given by $L$ itself. Let $n_1 \preceq n_2 \preceq \dots \preceq n_d$ be a branch of maximal length of $\mathcal{Z}_F$ (that must verify $d = \max_F - \min_F$, and that the root $n_1$ is a round node if and only if $\min_F$ is even). If we let $\ell_i$ be the cycle in $\mathcal{A}_L$ containing exactly the transitions corresponding to letters in $\nu(n_i)$, we obtain that $\ell_1 \supsetneq \ell_2 \supsetneq \dots \supsetneq \ell_d$ is a $d$-flower over $q$, which is positive if and only if $n_1$ is a round node. Lemma 2.16 allows us to conclude. $\quad \blacksquare$

## Minimality of the ZT-parity-automaton with respect to deterministic automata

Before presenting the proof of Theorem 4.13, we prove a weaker result, namely, that the ZT-parity-automaton is minimal amongst deterministic parity automata recognising a Muller language. We find that a proof of this weaker result might be enlightening for the reader, and it will allow us to introduce the main ingredients used in the proof of the stronger optimality result in a simpler setting.

**Theorem 4.16** (Minimality of the Zielonka Tree automaton with respect to deterministic automata). *Let $\mathcal{A}$ be a DPA recognising a Muller language Muller$_Σ$(\mathcal{F})$. Then, $|\mathcal{A}_{\mathcal{Z}_F}^{\text{parity}}| \le |\mathcal{A}|$.*

We recall that, by Remark 2.4 and Lemma 2.5, we can suppose that all the states of automata recognising Muller languages are accessible, and that any of them can be chosen to be initial. When considering subautomata of these automata, we will sometimes not mention their initial state.
Let $\mathcal{A} = (Q, \Sigma, I, \Gamma, \Delta, \mathbb{W})$ be an automaton, and let $X \subseteq \Sigma$ be a subset of the input alphabet. We say that a subgraph $\mathcal{S}$ of the underlying graph of $\mathcal{A}$ is $X$-closed if for every state $q$ in $\mathcal{S}$ and every letter $a \in X$ there is some transition $q \xrightarrow{a:c} q'$ in $\mathcal{S}$. An $X$-final strongly connected component (X-FSCC) of $\mathcal{A}$ is an $X$-closed final SCC in the graph obtained by taking the restriction of the underlying graph of $\mathcal{A}$ to the edges labelled by letters in $X$. We remark that a subset $S \subseteq Q$ is the set of states of an $X$-FSCC if and only if:

- for any two states $q, q' \in S$ there is a finite word $w \in X^*$ labelling a finite path from $q$ to $q'$, and

- if $q \in S$ and there is a finite path from $q$ to $q'$ labelled with a word $w \in X^*$, then $q' \in S$.

**Lemma 4.17.** Let $\mathcal{A}$ be a complete automaton. For every subset $X \subseteq \Sigma$, $\mathcal{A}$ contains an accessible $X$-FSCC.

**Proof.** As any graph without sinks contains some final SCC, the accessible part of the restriction of $\mathcal{A}$ to edges labelled by letters in $X$ contains one. By completeness of $\mathcal{A}$, one such final SCC has to be an $X$-closed subgraph, so it is an $X$-FSCC. ◀

**Lemma 4.18.** Let $\mathcal{A}$ be a DMA recognising a Muller language $\text{Muller}_\Sigma(\mathcal{F})$, let $X \subseteq \Sigma$ and let $S_X$ be an accessible $X$-FSCC of $\mathcal{A}$. Then, the automaton induced by $S_X$ is a deterministic automaton recognising $\text{Muller}_X(\mathcal{F}|_X) = \{w \in X^\omega \mid \text{Inf}(w) \in \mathcal{F}\}$.

**Proof.** Let $\mathcal{A} = (Q, \Sigma, q_0, \Gamma, \delta, \mathbb{W})$ (where $\mathbb{W}$ is a Muller language). Let $q_S$ be the state in $S_X$ chosen to be initial, and let $u_0 \in \Sigma^*$ be a finite word such that the run over $u_0$ from $q_0$ ends in $q_S$. By prefix-independence of Muller languages, a word $w \in X^\omega$ belongs to $\text{Muller}_\Sigma(\mathcal{F})$ if and only if $u_0w \in \text{Muller}_\Sigma(\mathcal{F})$, and therefore, $\mathcal{A}$ accepts $w$ if and only if it accepts $u_0w$. Since the run in $\mathcal{A}$ over $u_0w$ and the run in $S_X$ over $w$ have a suffix in common, and by prefix-independence of $\mathbb{W}$, we have that $w \in \mathcal{L}(S_X)$ if and only if $u_0w \in \mathcal{L}(\mathcal{A})$ if and only if $\text{Inf}(w) \in \mathcal{F}$. ◀

Next lemma states that, in a parity automaton, the union of two accepting cycles must be accepting, and similarly for rejecting cycles. In Section 6.1, we will see that this property is actually a characterisation of parity transition systems (Proposition 6.11).

**Lemma 4.19.** Let $\mathcal{A}$ be a parity automaton. Let $\ell_1, \ell_2 \in \text{Cycles}(\mathcal{A})$ be two cycles with some state in common. If $\ell_1$ and $\ell_2$ are both accepting (resp. rejecting), then $\ell_1 \cup \ell_2$ is also accepting (resp. rejecting).

**Proof.** Let $\gamma: \Delta \to \mathbb{N}$ be the colouring function of $\mathcal{A}$. The cycles $\ell_1$ and $\ell_2$ are accepting if and only if $d_i = \min \gamma(\ell_i)$ is even, for $i = 1, 2$. In this case, $\min \gamma(\ell_1 \cup \ell_2) = \min\{d_1, d_2\}$ is even. The proof is symmetric if $\ell_1$ and $\ell_2$ are rejecting. ◀

By a small abuse of notation, we will say that two SCC $S_1$ and $S_2$ are disjoint, and write $S_1 \cap S_2 = \emptyset$, if their sets of states are disjoint.

**Lemma 4.20.** Let $\mathcal{F} \subseteq 2_+^\Sigma$ be a family of subsets with Zielonka tree $\mathcal{Z}_\mathcal{F} = (N, \prec, \nu)$, and let $\mathcal{A}$ be a DPA recognising $\text{Muller}_\Sigma(\mathcal{F})$. Let $n \in N$ be a node of the Zielonka tree of $\mathcal{F}$, and let $n_1, n_2 \in \text{Children}_{\mathcal{Z}_\mathcal{F}}(n)$ be two different children of $n$. If $S_1$ and $S_2$ are two accessible $\nu(n_1)$-FSCC and $\nu(n_2)$-FSCC in $\mathcal{A}$, respectively, then $S_1 \cap S_2 = \emptyset$.

**Proof.** Without loss of generality, we can suppose that all states in $\mathcal{A}$ are accessible, and since the language that $\mathcal{A}$ recognises is prefix-independent, we can also suppose that $\mathcal{A}$ is complete. Let $l_\Sigma: \Delta \to \Sigma$ be the labelling of the transitions of $\mathcal{A}$ with input letters. Let
$S_i$ be a $\nu(n_i)$-FSCC in $\mathcal{A}$, for $i = 1, 2$, and let $\ell_i$ be its set of edges, which form a cycle satisfying $l_{\Sigma}(\ell_i) = \nu(n_i)$. Suppose by contradiction that $S_1 \cap S_2 \neq \emptyset$. Then $\ell_1$ and $\ell_2$ have some state in common, and their union is also a cycle satisfying $l_{\Sigma}(\ell_1 \cup \ell_2) = \nu(n_1) \cup \nu(n_2)$. By Lemma 4.19, we must have

$$ \ell_1 \text{ accepting} \iff \ell_1 \cup \ell_2 \text{ accepting,} $$

contradicting the fact that $\nu(n_1) \in \mathcal{F}$ if and only if $\nu(n_1) \cup \nu(n_2) \notin \mathcal{F}$ (Remark 4.4). $\quad \triangle$

**Proof of Theorem 4.16.** We proceed by induction in the height of $\mathcal{Z}_F$. For height 1, the result is trivial, since $|\mathcal{A}_{\mathcal{Z}_F}^{\text{parity}}| = 1$. Let $\mathcal{A}$ be a DPA recognising $\text{Muller}_{\Sigma}(\mathcal{F})$. Let $n_0$ be the root of $\mathcal{Z}_F$ and $n_1, n_2, \dots, n_k$ be an enumeration of the children of $n_0$ in $\mathcal{Z}_F$. By Lemma 4.17, for each $i \in \{1, \dots, k\}$, $\mathcal{A}$ contains some accessible $\nu(n_i)$-FSCC $S_i$, and by Lemma 4.20 these must be pairwise disjoint. By Lemma 4.18, each $S_i$ induces a deterministic subautomaton recognising $\text{Muller}_{\nu(n_i)}(\mathcal{F}|_{\nu(n_i)})$. Let $\mathcal{Z}_i$ by the subtree of $\mathcal{Z}_F$ rooted at $n_i$, which we recall that is the Zielonka tree for $\mathcal{F}|_{\nu(n_i)}$. By induction hypothesis, it must be the case that $|\text{Leaves}(\mathcal{Z}_i)| \le |S_i|$, so we can conclude:

$$ |\mathcal{A}_{\mathcal{Z}_F}^{\text{parity}}| = |\text{Leaves}(\mathcal{Z}_F)| = \sum_{i=1}^{k} |\text{Leaves}(\mathcal{Z}_i)| \le \sum_{i=1}^{k} |S_i| \le |\mathcal{A}|. \quad \triangle $$

## Minimality of the ZT-parity-automaton with respect to HD automata

We intend to prove Theorem 4.13, that is, that for any $\mathcal{F} \subseteq 2_{\Sigma}^{\Sigma}$, the automaton $\mathcal{A}_{\mathcal{Z}_F}^{\text{parity}}$ is minimal amongst HD parity automata recognising $\text{Muller}(\mathcal{F})$. We will follow the same proof scheme than in the deterministic case, performing an induction over the height of the Zielonka tree. Suppose that $\mathcal{A}$ is an HD parity automaton for $\text{Muller}(\mathcal{F})$ and that $n_0$ is the root of $\mathcal{Z}_F$ having $n_1, \dots, n_k$ as children. For each child $n_i$ we want to find an HD subautomaton $\mathcal{A}_i$ recognising the language associated to $\mathcal{F}|_{\nu(n_i)}$ in such a way that the automata $\mathcal{A}_i$ are pairwise disjoint, which would allow us to carry out the induction and obtain that $|\mathcal{A}| \ge |\text{Leaves}(\mathcal{Z}_F)| = |\mathcal{A}_{\mathcal{Z}_F}^{\text{parity}}|$. Our objective will be therefore to prove:

**Proposition 4.21.** Let $n_0$ be the root of the Zielonka tree of $\mathcal{F}$, and let $n_1, n_2, \dots, n_k$ be an enumeration of the children of $n_0$. If $\mathcal{A}$ is an HD automaton recognising $\text{Muller}_{\Sigma}(\mathcal{F})$, then, $\mathcal{A}$ contains $k$ pairwise disjoint subautomata $A_1, \dots, A_k$ that are history-deterministic and such that $\mathcal{L}(\mathcal{A}_i) = \text{Muller}_{\nu(n_i)}(\mathcal{F}|_{\nu(n_i)})$.

The non-determinism of $\mathcal{A}$ will make this task considerably more laborious than in the previous paragraph, and we will have to thoroughly examine the strategies used by the resolvers for $\mathcal{A}$. By the inherently asymmetric semantics of non-deterministic automata, there are two well-differentiated cases to consider, depending on whether the root of the Zielonka tree is round ($\Sigma \in \mathcal{F}$) or square ($\Sigma \notin \mathcal{F}$).

In order to simplify the proof, we will suppose that all states are reachable using a sound resolver and that all automata have a single initial state, which can be done without lost of generality since a resolver for an HD automaton fixes such initial state in advance.

**Case 1: The root of the Zielonka tree is a square node: $\Sigma \notin \mathcal{F}$**. Let $\mathcal{A} = (Q, \Sigma, q_0, \Gamma, \Delta, \mathbb{W})$ be a non-deterministic automaton. A memory structure for $\mathcal{A}$ is a memory skeleton $\mathcal{M}$ over $\Delta$ together with a function $\sigma: Q \times M \times \Sigma \to \Delta$, where $M$ is the set of states of $\mathcal{M}$. We say that $(\mathcal{M}, \sigma)$ implements a resolver $(q_0, r)$ if for all $a \in \Sigma$, $r(\varepsilon, a) = \sigma(q_0, m_0, a)$ and for all $\rho \in \Delta^+$, $r(\rho, a) = \sigma(\text{Target}(\rho), \mu(m_0, \rho), a)$, where $m_0$ is the initial state of $\mathcal{M}$ and $\mu: M \times \Delta^* \to M$ is its update function.
**► Lemma 4.22 ([7]).** Every HD parity automaton admits a sound resolver implemented by a finite memory structure.

As $\mathcal{M}$ is a pointed graph labelled with the transitions of $\mathcal{A}$, we could consider the product automaton $\mathcal{A} \times \mathcal{M}$. We want to furthermore restrict the transitions of this automaton to those that are indicated by the next-move function $\sigma$. Given an automaton $\mathcal{A}$ and a memory structure $(\mathcal{M}, \sigma)$, we define their composition, which we write $\mathcal{A} \triangleleft_{\sigma} \mathcal{M} = (Q \times M, \Sigma, (q_0, m_0), \Gamma, \Delta', \mathbb{W})$ as the automaton having transitions $(q, m) \xrightarrow{a:c} (q', m')$ if $\sigma(q, m, a) = e = q \xrightarrow{a:c} q'$ and $\mu(m, e) = m'$ (formally, $\Delta'$ is a subset of $\Delta \times E_{\mathcal{M}}$, where $E_{\mathcal{M}}$ are the edges of the memory skeleton). We note that $\mathcal{A} \triangleleft_{\sigma} \mathcal{M}$ is deterministic, and it is complete if $\mathcal{A}$ is.

The following lemma follows directly from the definition of soundness of a resolver and the definition of composition of an automaton and a memory structure.

**► Lemma 4.23.** Let $\mathcal{A}$ be an automaton and $(\mathcal{M}, \sigma)$ a memory structure for $\mathcal{A}$. The resolver implemented by $(\mathcal{M}, \sigma)$ is sound if and only if $\mathcal{A}$ and $\mathcal{A} \triangleleft_{\sigma} \mathcal{M}$ recognise the same language.

For the rest of the paragraph, we let $\mathcal{A} = (Q, \Sigma, q_0, \mathbb{N}, \Delta, \text{parity})$ be a complete history-deterministic automaton recognising the Muller language $\text{Muller}_\mathcal{F}(\Sigma)$ admitting a sound resolver $(q_0, r)$ implemented by a memory structure $(\mathcal{M}, \sigma)$. We let $\pi_\mathcal{A}: \mathcal{A} \triangleleft_\sigma \mathcal{M} \to \mathcal{A}$ be the morphism of automata given by the projection into the first component: $\pi_{\mathcal{A},V}(q, m) = q$ and $\pi_{\mathcal{A},E}(e_1, e_2) = e_1$.

**► Remark 4.24.** If $\rho$ is a path in $\mathcal{A} \triangleleft_{\sigma} \mathcal{M}$ that is labelled by input letters $a_0a_1\cdots \in \Sigma^\infty$ and producing output $c_0c_1\cdots \in \mathbb{N}^\infty$, then the $\pi_\mathcal{A}$-projection of $\rho$ is a path in $\mathcal{A}$ labelled by $a_0a_1\cdots \in \Sigma^\infty$ and producing $c_0c_1\cdots \in \mathbb{N}^\infty$ as output. ▼

**► Lemma 4.25.** Let $X \subseteq \Sigma$ and let $S_X$ be an accessible X-FSCC of $\mathcal{A} \triangleleft_{\sigma} \mathcal{M}$. Then, $\pi_\mathcal{A}(S_X)$ induces an HD subautomaton of $\mathcal{A}$ recognising $\text{Muller}_X(\mathcal{F}|_X) = \{w \in X^\omega | \text{Inf}(w) \in \mathcal{F}\}$.

**Proof.** Let $q_S$ be a state in $\pi_\mathcal{A}(S_X)$ chosen to be initial. Let $m_S$ be a state in $\mathcal{M}$ such that $(q_S, m_S) \in S_X$. By Lemma 4.18, $S_X$ induces a deterministic subautomaton with initial state $(q_S, m_S)$ recognising $\text{Muller}_X(\mathcal{F}|_X)$. On the one hand, since $\pi_\mathcal{A}(S_X)$ is an accessible subautomaton of $\mathcal{A}$ having only transitions labelled by X and by prefix-independence of $\mathcal{L}(\mathcal{A})$, we have that

$$ \mathcal{L}(\pi_{\mathcal{A}}(S_X)) \subseteq \mathcal{L}(\mathcal{A}) \cap X^{\omega} = \text{Muller}_X(\mathcal{F}|_X). $$

On the other hand, the projection of any accepting run in $S_X$ provides an accepting run in $\pi_\mathcal{A}(S_X)$ (by Remark 4.24), so

$$ \mathcal{L}(S_X) = \text{Muller}_X(\mathcal{F}|_X) \subseteq \mathcal{L}(\pi_\mathcal{A}(S_X)). $$

Moreover, a sound resolver for $\pi_\mathcal{A}(S_X)$ is implemented by $(M_{m_S}, \sigma)$ (the memory structure with initial state set to $m_S$). ◀

**► Lemma 4.26.** Let $n \in \mathbb{N}$ be a square node of the Zielonka tree of $\mathcal{F}$ ($\nu(n) \notin \mathcal{F}$), and let $n_1, n_2 \in \text{Children}_{\mathcal{F}}(n)$ be two different children of n. If $S_1$ and $S_2$ are two accessible $\nu(n_1)$-FSCC and $\nu(n_2)$-FSCC in $\mathcal{A} \triangleleft_{\sigma} \mathcal{M}$, respectively, then $\pi_\mathcal{A}(S_1) \cap \pi_\mathcal{A}(S_2) = \emptyset$.

**Proof.** Suppose by contradiction that there is some state $q$ in $\pi_\mathcal{A}(S_1) \cap \pi_\mathcal{A}(S_2)$, and let $m_1, m_2 \in M$ be such that $(q, m_1)$ and $(q, m_2)$ are states in $S_1$ and $S_2$, respectively. For $i = 1, 2$, let $\ell_i \in \text{cycles}_{(q,m_i)}(\mathcal{A} \triangleleft_{\sigma} \mathcal{M})$ be the cycle over $(q, m_i)$ containing all edges in
$S_i$. We note that $l_Σ(l_i) = ν(n_i)$ and therefore $minγ(l_i)$ has to be even (as $A \triangleleft_σ M$ is deterministic), where $l_Σ$ and $γ$ are the labellings of $A \triangleleft_σ M$ with input letters and output colours, respectively. By Remark 4.24, the $π_A$-projections of $l_1$ and $l_2$ are cycles over $q$ in $A$ labelled with $ν(n_1)$ and $ν(n_2)$ and in which the minimal colour appearing is even. By alternating these two cycles, we can build an accepting run in $A$ over a word $w \in Σ^ω$ with $Inf(w) = ν(n_1) \cup ν(n_2)$, contradicting the fact that $ν(n_1) \cup ν(n_2) \notin F$ (Remark 4.4). ◀

Lemmas 4.17, 4.25 and 4.26 imply Proposition 4.21 in the case in which the root of the Zielonka tree is a square node.

**Case 2: The root of the Zielonka tree is a round node: $Σ \in F$.** Before presenting the formal proof, let us discuss why considering these two cases separately is necessary. A first idea to obtain the desired result would be to follow the same steps as in Case 1. However, this approach encounters a major difficulty: the argument used in the proof of Lemma 4.26 is not valid if $Σ \in F$. Indeed, even if we can find two rejecting cycles $l_1, l_2$ such that $l_Σ(l_i) = ν(n_i)$, their $π_A$-projections could a priori have a state in common; this would imply the existence of a rejecting run over the set of letters $ν(n_1) \cup ν(n_2) \in F$, which is not enough to conclude, as the non-determinism of $A$ leaves room for the existence of other accepting runs over this set of letters. To circumvent this difficulty, we need to take a closer look at the strategies used by the resolver. Rather than considering any finite memory strategy resolving the non-determinism of $A$, we will show that we can choose a very precise resolver for which we will be able to obtain a result analogous to Lemma 4.26. To do this, we first construct the letter game of $A$, as introduced in [38], which is a Muller game satisfying that a strategy for it yields a resolver for $A$. The strategy that we will use in this game is the one obtained by applying McNaughton's algorithm to solve Muller games [58] guided by the Zielonka tree, as presented in [28].

Let $A = (Q, Σ, q_0, [d_{min}, d_{max}], Δ, parity)$ be a parity automaton recognising Muller($F$), and suppose that $Σ \cap [d_{min}, d_{max}] = \emptyset$. The letter game for $A$ is the game $G_A$ defined as follows:

- The set of vertices is $V = Q \sqcup (Q \times Σ)$. Adam controls vertices in $Q$, and Eve controls vertices in $Q \times Σ$.

- For each letter $a \in Σ$ and each $q \in Q$, there is an edge $q \xrightarrow{a} (q, a)$.

- For each position $(q, a) \in Q \times Σ$, and for each transition $q \xrightarrow{a:c} q'$ in $A$, there is an edge $(q, a) \xrightarrow{c} q'$.

- The set of colours is $Γ = Σ \sqcup [d_{min}, d_{max}]$, and the acceptance set is the Muller language associated to

$$F \to \text{parity} = \{C \subseteq Γ \mid [C \cap Σ \in F] \implies [\min(C \cap [d_{min}, d_{max}]) \text{ is even}]\}.$$

That is, in the letter game, Adam provides input letters one by one, and Eve chooses transitions corresponding to those letters in the automaton $A$. Eve wins this game if she manages to build an accepting run every time that Adam gives as input an infinite word in the language recognised by $A$.

We remark that a subgraph of $G_A$ induces a subautomaton of $A$ via the (partial) mapping $\text{aut}_A: G_A \to A$ that sends states of the form $q \in Q$ to $q$ and edges of the form $(q, a) \xrightarrow{c} q'$ to $q \xrightarrow{a:c} q'$.

**Remark 4.27.** A strategy for Eve in $G_A$ induces a resolver in $A$, which is sound if and only if the strategy is winning.
<figure><img src="image_11.png" /><figcaption>Figure 10 Letter game for the HD automaton from Figure 1, recognising the Muller language associated to $\mathcal{F} = \{\{a\}, \{b\}, \{c\}, \{a, b\}, \{b, c\}\}$. Squares represent Adam's vertices (the states of the automaton) and circles Eve's ones. Blue edges correspond to input-letters, and orange edges to the choices of transitions in the automaton after each input letter. The only vertex where Eve has a non-trivial choice to make to resolve the non-determinism of the automaton is $(q_1, b)$. In this example, Eve has a winning strategy corresponding to the resolver described in Example 2.3.</figcaption></figure>

► Remark 4.28. If two subsets of vertices of the letter game $S_1, S_2 \subseteq V$ are disjoint, then $\text{aut}_A(S_1) \cap \text{aut}_A(S_2) = \emptyset$.

► Remark 4.29. If $\rho$ is a play in $\mathcal{G}_A$, labelled $a_0c_0a_1c_1 \cdots \in (\Sigma \cdot [d_{\min}, d_{\max}])^{\infty}$, the $\text{aut}_A$-projection of $\rho$ is a run in $\mathcal{A}$ over $a_0a_1 \cdots \in \Sigma^{\infty}$ producing $c_0c_1 \cdots \in [d_{\min}, d_{\max}]^{\infty}$ as output.

► Lemma 4.30 ([38]). A parity automaton $\mathcal{A}$ is HD if and only if Eve wins the letter game from some initial state of $\mathcal{A}$.

For a subset $X$ of vertices or edges of a game $\mathcal{G}$, we define Eve's attractor to $X$ as:

$$ \text{Attr}_{\mathcal{G}}(X) = \{v \in V \mid \text{there is a strategy for Eve ensuring to eventually visit } X \text{ from } v\}. $$

For a colour $c \in \Gamma$ we note $\text{Attr}_c(c) = \text{Attr}_c(E_c)$, where $E_c$ is the set of edges coloured $c$.

For the rest of the paragraph, let $\mathcal{A} = (Q, \Sigma, q_0, [0, d], \Delta, \text{parity})$ be a complete history-deterministic parity automaton recognising Muller($\mathcal{F}$). We can suppose without loss of generality that the minimal colour that it uses is 0. We let $V$ and $E$ denote the sets of vertices and edges, respectively, of the letter game and $\Gamma = \Sigma \sqcup [0, d]$ its set of colours. Whenever we use expressions like “the minimal colour appearing in a play”, it will refer to the restriction of $\Gamma$ to $[0, d]$. From the prefix-independence of Muller($\mathcal{F}$) we can moreover suppose that Eve wins the letter game from any vertex (see Lemma 2.5). We let $n_0$ be the root of the Zielonka tree of $\mathcal{F}$ (supposed to be round, that is $\nu(n_0) \in \mathcal{F}$), let $n_1, \dots, n_k$ be its children, and let $\Sigma_i = \nu(n_i) \subseteq \Sigma$ (note that $\Sigma_i \notin \mathcal{F}$ for $i \ge 1$).

Let us examine the condition $\mathcal{F} \to \text{parity}$ used in the letter game a bit closer. The first levels of its Zielonka tree of this condition are depicted in Figure 11. It is clear that a strategy in $\mathcal{G}_A$ ensuring to produce colour 0 infinitely often is winning. It might be the case that Adam can prevent Eve from doing this, however, since Eve wins $\mathcal{G}_A$, in that case she could ensure to produce infinitely often a set of colours included in some of the round nodes below the root, that is, to either avoid colour 1, or to produce letters included in some $\Sigma_i$. We use this idea to define next *attractor decompositions* for $\mathcal{G}_A$.

Given a subset of vertices $V' \subseteq V$ we write $\mathcal{G}_A(V')$ to denote the subgame of $\mathcal{G}_A$ containing the vertices of $V'$ and the edges between them.
<figure><img src="image_12.png" /><figcaption>Figure 11 First levels of the Zielonka tree of the Muller condition $\mathcal{F} \to \text{parity}$, which is the winning condition of the letter game $\mathcal{G}_A$.</figcaption></figure>

Let $x$ be an even integer. For a subgame $\mathcal{G}' = \mathcal{G}_A(V')$ of $\mathcal{G}_A$ with no colour strictly smaller than $x$, we define an $x$-attractor decomposition of $\mathcal{G}'$ as a partition of $V'$ into

$$V' = \text{Attr}_{\mathcal{G}'}(x) \sqcup V_1 \sqcup A_1 \sqcup \dots \sqcup V_l \sqcup A_l,$$

satisfying:

- $\text{Attr}_{\mathcal{G}'}(x)$ is Eve's attractor to $x$ in $\mathcal{G}'$.

- For each $V_j$, either (1) there is some $i \in \{1, \dots, k\}$ such that no colour of $\Sigma \setminus \Sigma_i$ appears in $\mathcal{G}_A(V_j)$, or (2) Eve has a winning strategy for $\mathcal{G}_A(V_j)$ (from any vertex) avoiding colour $x+1$; and in both cases, if Adam can leave $V_j$ taking an edge $v \xrightarrow{a} v'(v \in V_j, v' \notin V_j)$, then $v' \in \text{Attr}_{\mathcal{G}'}(x) \sqcup V_1 \sqcup A_1 \sqcup \dots \sqcup V_{j-1} \sqcup A_{j-1}$. In case (1) we say that $V_j$ is a $\Sigma_i$-region of the attractor decomposition and in case (2) that $V_j$ is an $x+1$-avoiding region.

- Eve wins $\mathcal{G}_A(V_j)$ from every vertex for all $j$.

- $A_j = \text{Attr}_{\mathcal{G}_j}(V_j)$, where $\mathcal{G}_j$ is the subgame induced by the subset of vertices given by $V \setminus (\text{Attr}_{\mathcal{G}'}(x) \sqcup V_1 \sqcup \dots \sqcup V_{j-1} \sqcup A_{j-1})$ (we note that this game does not contain edges coloured with $x$).

If $V_j$ is an $x+1$-avoiding region, we let $\mathcal{G}'_j$ be the subgame obtained from $\mathcal{G}_A(V_j)$ by removing the transitions labelled $x+1$.

An $x$-recursive attractor decomposition of $\mathcal{G}'$ is:

$$\mathcal{D}_{\mathcal{G}'} = \langle \text{Attr}_{\mathcal{G}'}(x), (V_1, A_1, \mathcal{D}_{\mathcal{G}'_1}), (V_2, A_2, \mathcal{D}_{\mathcal{G}'_2}), \dots, (V_l, A_l, \mathcal{D}_{\mathcal{G}'_l}) \rangle,$$

where $\text{Attr}_{\mathcal{G}'}(x) \sqcup V_1 \sqcup A_1 \sqcup \dots \sqcup V_l \sqcup A_l$ is an $x$-attractor decomposition of $\mathcal{G}'$, and, if $V_j$ is an $x+1$-avoiding region, then $\mathcal{D}_{\mathcal{G}'_j}$ is an $x+2$-recursive attractor decomposition of $\mathcal{G}'_j$. (If $V_j$ is an $\Sigma_i$-region, $\mathcal{D}_{\mathcal{G}'_j}$ can be disregarded).

A representation of an attractor decomposition appears in Figure 12.

We say that a subgame $S$ of $\mathcal{G}'$ is a $\Sigma_i$-region of $\mathcal{D}_{\mathcal{G}'_j}$ if it is a $\Sigma_i$-region of some of the recursively defined attractor decompositions. Similarly, for $y > x$ an odd integer, we say that $S$ is a $y$-avoiding region of $\mathcal{D}_{\mathcal{G}'_j}$ if it is a $y$-avoiding region of some of the recursively defined attractor decompositions. We say that the full game $\mathcal{G}'$ is an $x-1$-avoiding region (note that $x$ might take the value 0). We remark that for any subset $S$ of vertices of $\mathcal{G}'$ there is one and only one minimal $y$-avoiding region of $\mathcal{D}_{\mathcal{G}'_j}$ containing $S$ (note that $y$ might equal $-1$).

**Remark 4.31.** A 0-recursive attractor decomposition $\mathcal{D}_{\mathcal{G}_A}$ of $\mathcal{G}_A$ induces a partition of the vertices into

$$V = S_1 \sqcup \dots \sqcup S_r \sqcup A_1 \sqcup \dots A_r \sqcup B_1 \sqcup \dots \sqcup B_s,$$
<figure><img src="image_13.png" /><figcaption>■ **Figure 12** On the left, a 0-attractor decomposition of a game $\mathcal{G}$. On the right, the coloured part represents a 2-attractor decomposition of the subgame $\mathcal{G}'_2$ induced by the 1-avoiding region $V_2$. Since no 3-avoiding region appears on it, this is a full attractor decomposition of the game $\mathcal{G}$, inducing a partition into three different kinds of regions. The order over the $\Sigma_i$-regions is given by $V_1 <_D V_{2,1} <_D V_{2,2} <_D V_3$. Adam can only force to decrease with respect to this order, that is, at each sublevel of the decomposition, Adam cannot force to go to the right.</figcaption></figure>

such that:

- $S_j$ is a $\Sigma_i$-region of $D_{\mathcal{G}_A}$, for some $i \in \{1, \dots, k\}$,

- $A_j = \text{Attr}_{\mathcal{G}_j}(S_j)$ for some subgame $\mathcal{G}_j$ appearing at some level of the decomposition,

- $B_j = \text{Attr}_{\mathcal{G}'_j}(x)$ for some even integer $x$ and some $x-1$-avoiding region $\mathcal{G}'_j$ appearing at some level of the decomposition.

Moreover, such a decomposition induces a total order over the $\Sigma_i$-regions: for two sets $S_t, S_{t'}$, we write $S_t <_D S_{t'}$ if there are two regions $V_j, V_{j'}$ belonging to the same attractor decomposition in $D_{\mathcal{G}_A}$ such that $j < j'$, $S_t \subseteq V_j$ and $S_{t'} \subseteq V_{j'}$.

We call such a partition a *full attractor decomposition of* $\mathcal{G}_A$. We remark that, by definition of an attractor decomposition, Eve wins $\mathcal{G}_A(S_j)$ from every vertex for every $S_j$. See Figure 12 for an illustration. ▼

The proof that $\mathcal{G}_A$ admits a full attractor decomposition uses the ideas appearing in [28, Section 3].

**► Lemma 4.32.** Let $x$ be an even integer. If $\mathcal{G}'$ is a subgame of $\mathcal{G}_A$ with no colour smaller than $x$ and such that Eve can win from every vertex, then it admits an $x$-attractor decomposition. In particular, $\mathcal{G}_A$ admits a full attractor decomposition.

**Proof.** We suppose without loss of generality that $x=0$. Suppose that $V_1, A_1, \dots, V_{j-1}, A_{j-1}$ have already been defined and that they verify the desired properties. Suppose that the game $\mathcal{G}_j$ with vertices $V \setminus (\text{Attr}_{\mathcal{G}'_j}(0) \sqcup V_1 \sqcup \dots \sqcup V_{j-1} \sqcup A_{j-1})$ is non-empty. First, note that Eve wins $\mathcal{G}_j$ from any position. Indeed, Eve wins $\mathcal{G}'_j$ from any vertex $v$ in $\mathcal{G}_j$ (as we suppose that she can win $\mathcal{G}'_j$ starting anywhere); moreover, since $v \notin A_{j'}$ for any $j' < j$, Adam has a strategy from $v$ to force to remain in $\mathcal{G}_j$, and Eve has to be able to win against any such strategy.

We prove that either (1) there is some $i \in \{1, \dots, k\}$ and $v$ vertex in $\mathcal{G}_j$ such that Eve has a winning strategy from $v$ forcing to produce no colour in $\Sigma \setminus \Sigma_i$, or (2) there is some vertex $v$ in $\mathcal{G}_j$ such that Eve has a winning strategy from $v$ avoiding colour 1. Suppose by contradiction that this was not the case. Then, Adam can use the following strategy:
first, he forces to produce colour 1, then, a colour not in $\Sigma_1$, followed by a color not in $\Sigma_2$, and continues this pattern until a color not in $\Sigma_l$ is produced (and this without producing colour 0, since no 0-edge appears in $G_j$). Afterward, he continue repeating these steps in a round-robin fashion. This allows him to produce a play winning for him (the word produced is in Muller($\mathcal{F}$) while the minimal number produced is 1), contradicting the fact that Eve wins $G_j$ from $v$.

We suppose that we are in the case (1) (case (2) is identical), so from some vertices Eve can win producing no colour in $\Sigma \setminus \Sigma_i$. We let $V_j$ be the set of such vertices, and for each of them we fix a strategy $\text{strat}_v$ that is winning in $G_j$ and avoids colours in $\Sigma \setminus \Sigma_i$. By definition of $V_j$, if $\rho = v \rightsquigarrow v'$ is a finite play consistent with $\text{strat}_v$ in $G_j$, then $v' \in V_j$ (Eve can still win without producing colours in $\Sigma \setminus \Sigma_i$), so Adam cannot force to leave $V_j$. This proves that:

1. $\text{strat}_v$ is winning in $G_A(V_j)$ from $v$,

2. if $v \in V_j$ is controlled by Adam and $v \to v'$ is an edge in $G_A$, then $v' \in \text{Attr}_{G'}(0) \sqcup V_1 \sqcup A_1 \sqcup \dots \sqcup V_{j-1} \sqcup A_{j-1} \sqcup V_j$.

Also, if a vertex $v$ controlled by Adam is in $V_j$, no edge $v \xrightarrow{a \notin \Sigma_i} v'$ appears in $G_j$, so no colour of $\Sigma \setminus \Sigma_i$ appears in $G_A(V_j)$.

To finish the proof, we define $A_j$ to be the attractor of $V_j$ in $G_j$.

The existence of a full attractor decomposition for $G_A$ follows from the fact that any $x+1$-avoiding region of an $x$-attractor decomposition verifies the hypothesis of the lemma. ◀

**Lemma 4.33 ([58]).** Let $G$ be a game using a Muller acceptance condition such that Eve wins $G$ from every vertex. Then, there is a finite memory structure $(\mathcal{M}, \sigma)$ over $G$ implementing a winning strategy uniformly, that is, for every vertex $v$ of $G$ there is a memory state $m_v$ in $\mathcal{M}$ such that the memory structure $(\mathcal{M}_{m_v}, \sigma)$ implements a winning strategy from $v$.

For the rest of the paragraph, we fix a 0-recursive attractor decomposition $\mathcal{D}_{G_A}$ for $G_A$ and let $S_1 <_D S_2 \dots <_D S_r$ be the $\Sigma_i$-regions of the induced full attractor decomposition. For each region $S_j$ we fix a memory structure $(\mathcal{M}_j, \sigma_j)$ uniformly implementing a winning strategy for Eve in $G_A(S_j)$ (as given by Lemma 4.33). As in the previous paragraph, we can consider the composition $G_A(S_j) \triangleleft_{\sigma_j} \mathcal{M}_j$ consisting of the product game in which the choices for Eve are restricted to those of the form $(v, m) \xrightarrow{c} (v', m')$ if $\sigma_j(v, m) = e = v \xrightarrow{c} v'$ and $\mu_j(m, e) = m'$. By definition, Eve does not have any choice in $G_A(S_j) \triangleleft_{\sigma_j} \mathcal{M}_j$, and since $(\mathcal{M}_j, \sigma_j)$ implements a winning strategy, any infinite path in $G_A(S_j) \triangleleft_{\sigma_j} \mathcal{M}_j$ produces a set of colours in $\mathcal{F} \to \text{parity}$. We let $\pi_G: G_A(S_j) \triangleleft_{\sigma_j} \mathcal{M}_j \to G_A(S_j)$ be the projection into $G_A(S_j)$.

A subgraph $G_j$ of $G_A(S_j) \triangleleft_{\sigma_j} \mathcal{M}_j$ is X-closed, for a subset $X \subseteq \Sigma$, if for every vertex $(q, m)$ controlled by Adam and every $a \in X$ there is a transition $(q, m) \xrightarrow{a} ((q, a), m')$ in $G_j$ (that is, $q \xrightarrow{a} (q, a) \in G_A(S_j)$). We say that $G_j$ is an X-FSCC if it is an X-closed final SCC of the restriction of $G_A(S_j) \triangleleft_{\sigma_j} \mathcal{M}_j$ to the graph where Adam's choices are restricted to letters in $X$. We say that a subgraph $\mathcal{G}$ of $G_A$ is an X-closed subgame (with respect to the attractor decomposition $\mathcal{D}_{G_A}$ and a family of finite memory strategies) if $\mathcal{G} = \pi_G(G_j)$ for $G_j$ some X-closed SCC of some product $G_A(S_j) \triangleleft_{\sigma_j} \mathcal{M}_j$.

**Lemma 4.34.** Eve wins any X-closed subgame of $G_A$ (from any vertex).
**Proof.** In an $X$-closed subgame included in a region $G_A(S_j)$, Adam's moves have been restricted; however, all Eve's moves coming from the strategy implemented by $(M_j, \sigma_j)$ are available. Therefore, this strategy is also winning in such a subgame, since it is winning in the full $G_A(S_j)$. ◀

Putting this lemma together with Remark 4.27 we obtain:

**Lemma 4.35.** Let $X \subseteq \Sigma$, and let $G_X \subseteq G_A$ be an $X$-closed subgame of $G_A$. The subautomaton of $A$ induced by $\mathrm{aut}_A(G_X)$ is HD and recognises $\mathrm{Muller}_X(F|_X)$.

**Lemma 4.36.** If a product $G_A(S_j) \triangleleft_{\sigma_j} M_j$ does not contain any $X$-closed subgraph, for $X \subseteq \Sigma$, then from any vertex $(q, m)$ Adam can force to leave $S_j$ while playing only letters in $X$. That is, there is a path $(q, m) \rightsquigarrow (q', m')$ in $G_A(S_j) \triangleleft_{\sigma_j} M_j$ producing exclusively letters in $X$ such that, for some $a \in X$, the edge $q' \xrightarrow{a} (q', a)$ does not belong to $G_A(S_j)$.

**Proof.** If this was not the case, the subgraph of $G_A(S_j) \triangleleft_{\sigma_j} M_j$ consisting of the vertices that can be reachable from $(q, m)$ by reading letters in $X$ would form an $X$-closed subgraph. ◀

**Lemma 4.37.** For each label $\Sigma_i$ of the children of the root of $Z_F$, $G_A$ admits some $\Sigma_i$-closed subgame contained in a $\Sigma_i$-region of $D_{G_A}$.

**Proof.** Suppose that the full attractor decomposition of $G_A$ induced by $D_{G_A}$ is the following:

$$V = S_1 \sqcup \dots \sqcup S_r \sqcup A_1 \sqcup \dots A_r \sqcup B_1 \sqcup \dots \sqcup B_s,$$

We fix the following strategy strat for Eve in the letter game:

- whenever the play lands to $B_j$, where $B_j = \mathrm{Attr}_{G_j}(x)$ for some even colour $x$, she forces to produce colour $x$,

- whenever the play arrives to some $A_j$, she forces to go to $S_j$,

- in regions $S_j$ she uses the strategy $(M_j, \sigma_j)$. More precisely, let $m_v$ be the state of $M_j$ such that $(M_{j,v}, \sigma_j)$ implements a winning strategy for $G_A(V_j)$ from $(v, m_v)$. Each time that the play arrives to a vertex $v$ in $V_j$ from a different region, Eve uses $(M_{j,v}, \sigma_j)$.

**Claim 4.37.1.** Let $\rho$ be a play consistent with strat (from any vertex), and let $y \ge -1$ be the maximal odd number such that $\mathrm{Inf}(\rho)$ is contained in a $y$-avoiding region $S$ of $D_{G_A}$. Then, either $\rho$ eventually stays in a $\Sigma_i$-region $S_j$ contained in $S$, or the minimal colour produced infinitely often by $\rho$ is $y+1$.

**Proof.** Let $\mathrm{Attr}_S(y+1) \sqcup V_1 \sqcup A_1 \sqcup \dots, V_l \sqcup A_l$ be the attractor decomposition of $S$ appearing in $D_{G_A}$. By definition of an attractor decomposition, each time that the play leaves a $V_j$ region, the next vertex is in $v' \in \mathrm{Attr}_S(y+1) \sqcup V_1 \sqcup A_1 \sqcup \dots V_{j-1} \sqcup A_{j-1}$. First, if $V_j$ is a $y+2$-avoiding region, $\rho$ cannot stay in it (by maximality of $y$). Thus, if $\rho$ does not eventually stay in a $\Sigma_i$-region, it leaves regions $V_j$ infinitely often, so it must produce $y+1$ infinitely often too. Since $S$ is a $y$-avoiding region, no colour smaller than $y+1$ is produced. ◁

We obtain as a consequence that strat is winning for Eve from any initial position: any play staying in a $y$-avoiding region and producing infinitely many $y+1$'s is winning, and if a play eventually stays in a $\Sigma_i$-region $S_j$, it has to be winning since the strategy implemented by $(M_j, \sigma_j)$ is winning in there.

We remark that we can extract a $\Sigma_i$-FSCC from any $\Sigma_i$-closed subgraph of $G_A(S_j) \triangleleft_{\sigma_j} M_j$, that will be contained in the $\Sigma_i$-region $S_j$, so it suffices to prove the existence of such $\Sigma_i$-closed
subgraphs. We also recall that in $\mathcal{G}_A(S_j) \triangleleft_{\sigma_j} M_j$ all choices are left to Adam, so he can choose to produce any path in this product whenever the play arrives to a vertex $v$ in $S_j$.

Suppose by contradiction that no accessible $\Sigma_i$-closed subgraph exists in any of the products. We consider a play in which Adam does the following:

(a) the letters that he gives form a word $w \in \Sigma^\omega$ such that $\text{Inf}(w) = \Sigma_i$,

(b) each time that the play arrives to a region $S_j$, he exists this region in a finite number of steps.

Indeed, he can ensure to exit regions $S_j$ while only producing letters in $\Sigma_i$ by Lemma 4.36. By Claim 4.37.1, the minimal colour produced infinitely often by such a play is even. By Remark 4.29, we can project such a play in the automaton $\mathcal{A}$, obtaining an accepting run over $w$. This is a contradiction, since $w \notin \text{Muller}(\mathcal{F}) = \mathcal{L}(\mathcal{A})$ (because $\Sigma_i \notin \mathcal{F}$). We conclude that some $\mathcal{G}_A(S_j) \triangleleft_{\sigma_j} M_j$ admits a $\Sigma_i$-FSCC, and therefore $\mathcal{G}_A$ admits some $\Sigma_i$-closed subgame. ◀

We can now infer Proposition 4.21 in the case in which the root of $\mathcal{Z}_F$ is round: from Lemma 4.37, we obtain $\Sigma_i$-closed subgames in $\mathcal{G}_A$ for each $i \in \{1, \dots, k\}$ that are moreover contained in $\Sigma_i$-regions. Therefore, their $\text{aut}_A$-projections are disjoint (Remark 4.28), and each of these projections induces an HD-subautomaton recognising $\mathcal{F}|_{\Sigma_i}$ (Lemma 4.35).

## 4.3 A minimal history-deterministic Rabin automaton

In this section, we present the construction of a history-deterministic Rabin automaton $\mathcal{A}_{\mathcal{Z}_F}^{\text{Rabin}}$ for a Muller language $\text{Muller}(\mathcal{F})$ using the Zielonka tree $\mathcal{Z}_F$, and prove its minimality (Theorem 4.48). The automaton $\mathcal{A}_{\mathcal{Z}_F}^{\text{Rabin}}$ can be seen as a quotient of the ZT-parity-automaton; that is, $\mathcal{A}_{\mathcal{Z}_F}^{\text{Rabin}}$ is obtained by merging some of the states of $\mathcal{A}_{\mathcal{Z}_F}^{\text{parity}}$. Thus, we replace the complexity in the number of states by complexity in the acceptance condition. The size of the automaton $\mathcal{A}_{\mathcal{Z}_F}^{\text{Rabin}}$ is a well-studied parameter of Zielonka trees: its round-branching width, $\text{rbw}(\mathcal{Z}_F)$. This parameter was introduced by Dziembowski, Jurdziński and Walukiewicz [28] (under the name of memory of $\mathcal{Z}_F$) and shown to coincide with the memory required by Eve to win in games using $\text{Muller}(\mathcal{F})$ as an acceptance condition (see Proposition 4.49 below). In this paper, we are not concerned with the memory of winning conditions, but we will use the result from [28] to obtain the minimality of $\mathcal{A}_{\mathcal{Z}_F}^{\text{Rabin}}$.

We note that this construction is asymmetric, in the sense that we show it for Rabin automata, but not for Streett automata (their dual notion). The reason why we cannot dualize the construction is due to the semantics of non-deterministic automata. However, we could use the same idea to obtain a minimal universal history-deterministic Streett automaton (we refer to [10] for the definition of universal HD automata).

### 4.3.1 The Zielonka-tree-HD-Rabin-automaton

**Definition 4.38** ([28]). Let $T$ be a tree with nodes partitioned into round and square nodes, and let $T_1, \dots, T_k$ be the subtrees of $T$ rooted at the children of the root of $T$. We define inductively the round-branching width of $T$, denoted $\text{rbw}(T)$ as:

$$ \text{rbw}(T) = \begin{cases} 1 & \text{if } T \text{ has exactly one node,} \\ \max\{\text{rbw}(T_1), \dots, \text{rbw}(T_k)\} & \text{if the root is square,} \\ \sum_{i=1}^k \text{rbw}(T_i) & \text{if the root is round.} \end{cases} $$
Next lemma directly follows from the definition of rbw(T).

**Lemma 4.39.** Let $T = (N = N_{\bigcirc} \sqcup N_{\square}, \preceq)$ be a tree with nodes partitioned into round and square nodes. There exists a mapping $\eta$: $\text{Leaves}(T) \to \{1, 2, \dots, \text{rbw}(T)\}$ satisfying:

$$ \text{If } n \in N \text{ is a round node with children } n_1 \neq n_2, \text{ for any pair} \\ \text{of leaves } l_1 \text{ and } l_2 \text{ below } n_1 \text{ and } n_2, \text{ respectively, } \eta(l_1) \neq \eta(l_2). \tag{\star} $$

**Example 4.40.** Let $\mathcal{F} = \{\{a, b\}, \{a, c\}, \{b\}\}$ be the family of subsets considered in Example 4.5. The round-branching width of $\mathcal{Z}_{\mathcal{F}}$ is $\text{rbw}(\mathcal{Z}_{\mathcal{F}}) = 2$. A labelling $\eta$: $\text{Leaves}(\mathcal{Z}_{\mathcal{F}}) \to \{1, 2\}$ satisfying Property $\star$ is given by $\eta(\theta) = \eta(\xi) = 1$ and $\eta(\zeta) = 2$. This labelling is represented in the Zielonka tree $\mathcal{Z}_{\mathcal{F}}$ on the left of Figure 13.

**Definition 4.41** (Zielonka-tree-HD-Rabin-automaton). Let $\mathcal{F} \subseteq 2_{+}^{\Sigma}$, $\mathcal{Z}_{\mathcal{F}} = (N = N_{\bigcirc} \sqcup N_{\square}, \preceq)$ its Zielonka tree and $\eta$: $\text{Leaves}(\mathcal{Z}_{\mathcal{F}}) \to \{1, 2, \dots, \text{rbw}(\mathcal{Z}_{\mathcal{F}})\}$ a mapping satisfying Property $(\star)$. We define the ZT-HD-Rabin-automaton $\mathcal{A}_{\mathcal{Z}_{\mathcal{F}}^{\text{Rabin}}}$ = $(Q, \Sigma, I, \Gamma, \Delta, \text{Rabin}_{\Gamma}(R))$ as a (non-deterministic) automaton using a Rabin acceptance condition, where:

- $Q = \{1, 2, \dots, \text{rbw}(\mathcal{Z}_{\mathcal{F}})\}$,

- $I = Q^8$,

- $\Gamma = N$ (the colours of the acceptance condition are the nodes of the Zielonka tree),

- $\delta(q, a) = \{(\text{Jump}(l, \text{Supp}(l, a)), \text{Supp}(l, a)) \mid l \in \text{Leaves}(\mathcal{Z}_{\mathcal{F}}) \text{ such that } \eta(l) = q\}$,

- $R = \{(G_n, R_n)\}_{n \in N_{\bigcirc}}$, where $G_n$ and $R_n$ are defined as follows: Let $n$ be a round node and $n'$ be any node of $\mathcal{Z}_{\mathcal{F}}$,

$$ \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} \]

**Remark 4.42.** Although we will usually say that $\mathcal{A}_{\mathcal{Z}_{\mathcal{F}}^{\text{Rabin}}}$ is the ZT-HD-Rabin-automaton of $\mathcal{F}$, the structure of this automaton is not unique, it depends on two choices: the order over the nodes of the Zielonka tree and the mapping $\eta$. $\blacksquare$

The intuition behind this definition is the following. The automaton $\mathcal{A}_{\mathcal{Z}_{\mathcal{F}}^{\text{Rabin}}}$ has $\text{rbw}(\mathcal{Z}_{\mathcal{F}})$ states, and each of them can be associated to a subset of leaves of $\mathcal{Z}_{\mathcal{F}}$ by $\eta^{-1}(q)$. The mapping $\eta$ is such that the lowest common ancestor of two leaves in $\eta^{-1}(q)$ is a square node. As for the ZT-parity-automaton, for each leaf of $l \in \text{Leaves}(\mathcal{Z}_{\mathcal{F}})$ and letter $a \in \Sigma$, we identify the deepest ancestor $n = \text{Supp}(l, a)$ containing $a$ in its label, and, using the Jump function, pick a leaf $l'$ below the next child of $n$. We add a transition $q \xrightarrow{a:n} q'$ if there are leaves $l \in \eta^{-1}(q)$ and $l' \in \eta^{-1}(q')$ giving such a path. This way, we can identify a run in the automaton $\mathcal{A}_{\mathcal{Z}_{\mathcal{F}}^{\text{Rabin}}}$ with a promenade through the nodes of the Zielonka tree in which jumps between leaves with the same $\eta$-image are allowed. If during this promenade a unique minimal node (for $\preceq$) is visited infinitely often, it is not difficult to see that the sequence of input colours belongs to $\mathcal{F}$ if and only if the label of this minimal node belongs to $\mathcal{F}$ (it is a round node). The Rabin condition over the set of nodes of the Zielonka tree is devised so that it accepts exactly these sequences of nodes (see Lemma 4.46 below).

Another way of presenting the automaton $\mathcal{A}_{\mathcal{Z}_{\mathcal{F}}^{\text{Rabin}}}$ is as a quotient of the deterministic parity automaton $\mathcal{A}_{\mathcal{Z}_{\mathcal{F}}^{\text{parity}}}$.

<footnote n="8">⁸ Any non-empty subset of $Q$ can be chosen as the set of initial states.</footnote>
**► Example 4.43.** The ZT-HD-Rabin-automaton $\mathcal{A}_{\mathcal{Z}_F}^{\text{Rabin}}$ of the family $\mathcal{F} = \{\{a, b\}, \{a, c\}, \{b\}\}$ from Example 4.5 is shown on the right of Figure 13. The Zielonka tree $\mathcal{Z}_F$ appears on the left of the figure, and the labelling $\eta$: $\text{Leaves}(\mathcal{Z}_F) \to \{1, 2\}$ is represented by the numbers below its branches.

The Rabin condition of this automaton is given by two Rabin pairs (corresponding to the round nodes of the Zielonka tree):

$$ 
\begin{aligned}
G_{\beta} &= \{\beta\}, & R_{\beta} &= \{\alpha, \lambda, \xi, \zeta\}, \\
G_{\lambda} &= \{\lambda\}, & R_{\lambda} &= \{\alpha, \beta, \theta\}.
\end{aligned}
$$

<figure><img src="image_14.png" /><figcaption>■ **Figure 13** On the left, the Zielonka tree of $\mathcal{F} = \{\{a, b\}, \{a, c\}, \{b\}\}$. On the right, the ZT-HD-Rabin-automaton $\mathcal{A}_{\mathcal{Z}_F}^{\text{Rabin}}$. Blue transitions correspond to those coming from leaf $\theta$, and green ones to those originating from leaf $\xi$.</figcaption></figure>

We note that the automaton $\mathcal{A}_{\mathcal{Z}_F}^{\text{Rabin}}$ is obtained by merging the states $\theta$ and $\xi$ from the ZT-parity-automaton $\mathcal{A}_{\mathcal{Z}_F}^{\text{parity}}$ appearing in Figure 9, and replacing the output colours by suitable nodes from the Zielonka tree.

**► Remark 4.44.** We observe that the automaton from Figure 13 presents duplicated edges, in the sense that there are two transitions $q \xrightarrow{a:x} q'$ and $q \xrightarrow{a:y} q'$ between the same pair of states and reading the same input letter. We can always avoid this and remove duplicated edges from any automaton. We provide a proof in Appendix D (Proposition D.1). For the language from the previous example, an equivalent automaton is proposed in Figure 18

## Correctness of the Zielonka-tree-HD-Rabin-automaton

**► Proposition 4.45 (Correctness).** Let $\mathcal{F} \subseteq 2_+^\Sigma$ be a family of non-empty subsets. Then,
$$ \mathcal{L}(\mathcal{A}_{\mathcal{Z}_F}^{\text{Rabin}}) = \text{Muller}_\Sigma(\mathcal{F}). $$

Moreover, the automaton $\mathcal{A}_{\mathcal{Z}_F}^{\text{Rabin}}$ is history-deterministic.

**► Lemma 4.46.** Let $u = n_0 n_1 n_2 \cdots \in N^\omega$ be an infinite sequence of nodes of the Zielonka tree. The word $u$ belongs to $\text{Rabin}_N(R)$, for $R = \{(G_n, R_n)\}_{n \in N_0}$ the Rabin condition of $\mathcal{A}_{\mathcal{Z}_F}^{\text{Rabin}}$, if and only if there is a unique minimal node for the ancestor relation in $\text{Inf}(u)$ and this minimal node is round (recall that the root is the minimal element for $\leq$).

**Proof.** Suppose that there is a unique minimal node in $\text{Inf}(u)$, called $n$, and that $n$ is round. We claim that $u$ is accepted by the Rabin pair $(G_n, R_n)$. It is clear that $\text{Inf}(u) \cap G_n \neq \emptyset$, because $n \in G_n$. It suffices to show that $\text{Inf}(u) \cap R_n = \emptyset$: By minimality, any other node $n' \in \text{Inf}(u)$ is a descendant of $n$ (equivalently, $n$ is an ancestor of $n'$), so $n' \notin R_n$.

Conversely, suppose that $u \in \text{Rabin}_N(R)$. Then, there is some round node $n \in N_0$ such that $\text{Inf}(u) \cap G_n \neq \emptyset$ and $\text{Inf}(u) \cap R_n = \emptyset$. Since $G_n = \{n\}$, we deduce that $n \in \text{Inf}(u)$.
Moreover, as $\text{Inf}(u) \cap R_n = \emptyset$, all nodes in $\text{Inf}(u)$ are descendants of $n$. We conclude that $n$ is the unique minimal node in $\text{Inf}(u)$, and it is round. ◀

**▶ Lemma 4.47.** There exists a morphism of automata $\varphi: \mathcal{A}_{\mathbb{Z}_F}^{\text{parity}} \to \mathcal{A}_{\mathbb{Z}_F}^{\text{Rabin}}$.

*Proof.* We define the morphism $\varphi$ as follows:

- $\varphi_V(l) = \eta(l)$, for $l \in \text{Leaves}(\mathcal{A}_{\mathbb{Z}_F}^{\text{parity}})$,

- for a transition $e = l \xrightarrow{a:c} l'$ in $\mathcal{A}_{\mathbb{Z}_F}^{\text{parity}}$, we let $\varphi_E(e) = (\eta(l), a, \text{Supp}(l, a), l')$.

It is clear that $\varphi$ is a weak morphism. We prove that it preserve the acceptance of runs. Let $\rho = l_0 \xrightarrow{w_0} l_1 \xrightarrow{w_1} l_2 \xrightarrow{w_2} \dots \in \mathcal{R}un(\mathcal{A}_{\mathbb{Z}_F}^{\text{parity}})$ be an infinite run in $\mathcal{A}_{\mathbb{Z}_F}^{\text{parity}}$ (the only run over $w_0 w_1 w_2 \dots \in \Sigma^\omega$), and let $n_i = \text{Supp}(l_i, w_i)$. By definition of the morphism, the output of the run $\rho' = \varphi_{\mathcal{R}uns}(\rho)$ in $\mathcal{A}_{\mathbb{Z}_F}^{\text{Rabin}}$ is $\gamma'(\rho') = n_0 n_1 n_2 \dots \in N^\omega$. In the proof of Proposition 4.10, we proved (Claims 4.10.1 and 4.10.2) that there exists a unique node $n_w$ appearing infinitely often in $\gamma'(\rho')$. Moreover, we proved that $\rho$ is accepting in $\mathcal{A}_{\mathbb{Z}_F}^{\text{parity}}$ if and only if $n_w$ is round. Lemma 4.46 allows us to conclude that $\varphi_{\mathcal{R}uns}(\rho)$ is accepting in $\mathcal{A}_{\mathbb{Z}_F}^{\text{Rabin}}$ if and only if $\rho$ is accepting in $\mathcal{A}_{\mathbb{Z}_F}^{\text{parity}}$. ◀

**Proof of Proposition 4.45.** $\mathcal{L}(\mathcal{A}_{\mathbb{Z}_F}^{\text{Rabin}}) \subseteq \text{Muller}_\Sigma(\mathcal{F})$: Let $w \in \mathcal{L}(\mathcal{A}_{\mathbb{Z}_F}^{\text{Rabin}})$ and let $u \in N^\omega$ be the sequence of nodes produced as output of an accepting run over $w$ in $\mathcal{A}_{\mathbb{Z}_F}^{\text{Rabin}}$. By Lemma 4.46, there is a unique minimal node $n$ for $\leq$ appearing infinitely often in $u$ and moreover $n$ is round. Let $n_1, \dots, n_k$ be an enumeration of the children of $n$ (from left to right), with labels $\nu(n_i) \subseteq \Sigma$ (we remark that $\nu(n_i) \notin \mathcal{F}$, for $1 \leq i \leq k$). We will prove that $\text{Inf}(w) \subseteq \nu(n)$ and $\text{Inf}(w) \not\subseteq \nu(n_i)$ for $1 \leq i \leq k$. By definition of the Zielonka tree, as $n$ is round, this implies that $\text{Inf}(w) \in \mathcal{F}$.

Since eventually all nodes produced as output are descendants of $n$ (by minimality), $\text{Inf}(w)$ must be contained in $\nu(n)$ (by definition of the transitions of $\mathcal{A}_{\mathbb{Z}_F}^{\text{Rabin}}$).

We suppose, towards a contradiction, that $\text{Inf}(w) \subseteq \nu(n_j)$ for some $1 \leq j \leq k$. Let $Q_i = \{\eta(l) : l$ is a leaf below $n_i\}$ be the set of states corresponding to leaves under $n_i$, for $1 \leq i \leq k$. We can suppose that the leaves corresponding to transitions of an accepting run over $w$ are all below $n$, and therefore, transitions of such a run only visit states in $\cup_{i=1}^k Q_i$. Indeed, eventually this is going to be the case, because if some of the leaves $l, l'$ corresponding to a transition $(q, a, n', q')$ are not below $n$, then $n'$ would not be a descendant of $n$ (since $n'$ is the least common ancestor of $l$ and $l'$). Also, by Property $(\star)$, we have $Q_i \cap Q_j = \emptyset$, for all $i \neq j$. By definition of the transitions of $\mathcal{A}_{\mathbb{Z}_F}^{\text{Rabin}}$, if $a \in \Sigma$ is a letter in $\nu(n)$ but not in $\nu(n_i)$, all transitions from some state in $Q_i$ reading the colour $a$ go to $Q_{i+1}$, for $1 \leq i \leq k-1$ (and to $Q_1$ if $i=k$). Also, if $a \in \nu(n_i)$, transitions from states in $Q_i$ reading $a$ stay in $Q_i$. We deduce that a run over $w$ will eventually only visit states in $Q_j$, for some $j$ such that $\text{Inf}(w) \subseteq \nu(n_j)$. However, the only transitions from $Q_j$ that would produce $n$ as output are those corresponding to a colour $a \notin \nu(n_j)$, so the node $n$ is not produced infinitely often, a contradiction.

**Muller-$\Sigma(\mathcal{F})$ and history-determinism:** The existence of a morphism $\varphi: \mathcal{A}_{\mathbb{Z}_F}^{\text{parity}} \to \mathcal{A}_{\mathbb{Z}_F}^{\text{Rabin}}$ (Lemma 4.47) and the correctness of $\mathcal{A}_{\mathbb{Z}_F}^{\text{parity}}$ (Proposition 4.10) imply that $\mathcal{L}(\mathcal{A}_{\mathbb{Z}_F}^{\text{Rabin}}) = \mathcal{L}(\mathcal{A}_{\mathbb{Z}_F}^{\text{parity}}) = \text{Muller}(\mathcal{F})$. Indeed, if $\rho$ is an accepting run over $w \in \Sigma^\omega$ in $\mathcal{A}_{\mathbb{Z}_F}^{\text{parity}}$, then $\varphi_{\mathcal{R}uns}(\rho)$ is an accepting run over $w$ in $\mathcal{A}_{\mathbb{Z}_F}^{\text{Rabin}}$. We can moreover use $\mathcal{A}_{\mathbb{Z}_F}^{\text{parity}}$ and $\varphi$ to define a sound resolver $(r_0, r)$ for $\mathcal{A}_{\mathbb{Z}_F}^{\text{Rabin}}$: we let $r_0 = \varphi(q_0)$ be the image of the initial state of $\mathcal{A}_{\mathbb{Z}_F}^{\text{parity}}$. If $\rho_R \in \mathcal{R}un^{\text{fin}}(\mathcal{A}_{\mathbb{Z}_F}^{\text{Rabin}})$ is the image under $\varphi_{\mathcal{R}uns}$ of some finite run $\rho_P \in \mathcal{R}un^{\text{fin}}(\mathcal{A}_{\mathbb{Z}_F}^{\text{parity}})$, we let $r(\rho_R, a) = \varphi(e)$, where $e$ is the only $a$-labelled transition from Target($\rho_P$). We define $r$ arbitrarily in other case. This way, for every $w \in \Sigma^\omega$, the run induced by $r$ over $w$ is the image of a run over $w$ in $\mathcal{A}_{\mathbb{Z}_F}^{\text{parity}}$, which must be accepting if $w \in \text{Muller}(\mathcal{F})$. ◀
### 4.3.2 Optimality of the Zielonka-tree-HD-Rabin-automaton

We devote this section to the proof of the optimality of $\mathcal{A}_{\mathcal{Z}_F}^{\text{Rabin}}$.

**Theorem 4.48 (Optimality of the ZT-HD-Rabin-automaton).** Let $\mathcal{A}$ be a history-deterministic Rabin automaton accepting a Muller language $\text{Muller}_\Sigma(\mathcal{F})$. Then, $|\mathcal{A}_{\mathcal{Z}_F}^{\text{Rabin}}| \le |\mathcal{A}|$.

**Proposition 4.49 ([28]).** Let $L = \text{Muller}_\Sigma(\mathcal{F})$ be a Muller language.

1. If Eve wins a game with $L$ as acceptance set from a position $v$, there is a winning strategy from $v$ for her implemented by a memory structure of size $\text{rbw}(\mathcal{Z}_F)$.

2. There exists a game $\mathcal{G}$ using $L$ as acceptance condition in which Eve can win from a position $v$, but there is no winning strategy from $v$ for her implemented by a memory structure of size strictly smaller than $\text{rbw}(\mathcal{Z}_F)$.

**Lemma 4.50 ([44, 81]).** Rabin languages are positionally determined, that is, if Eve wins a game using a Rabin acceptance condition from a position $v$, there is a winning strategy from $v$ for her implemented by a memory structure of size 1.

**Corollary 4.51.** Let $\mathcal{A}$ be a history-deterministic Rabin automaton. Then, if Eve wins a game with $W = \mathcal{L}(\mathcal{A})$ as acceptance set from a position $v$, there is a winning strategy from $v$ for her implemented by a memory structure of size $|\mathcal{A}|$.

**Proof.** Let $\mathcal{G}$ be a game with $W = \mathcal{L}(\mathcal{A})$ as acceptance set. In order to be able to take the product by $\mathcal{A}$ and obtain an equivalent game, we transform $\mathcal{G}$ into a game suitable for transformations. Let $\tilde{\mathcal{G}}$ be the game obtained from $\mathcal{G}$ in the following way: for every edge $e = v \xrightarrow{a} v'$ in $\mathcal{G}$, we add a position $(v, e)$ controlled by Eve and replace edge $e$ by $v \xrightarrow{e} (v, e) \xrightarrow{a} v'$. It is clear that Eve wins $\mathcal{G}$ from a vertex $v$ if and only if she wins $\tilde{\mathcal{G}}$ from that same vertex. By Proposition 2.7, if Eve wins $\mathcal{G}$ from a vertex $v$, she wins $\tilde{\mathcal{G}} \times \mathcal{A}$ from a vertex $(v, q_0)$, where $q_0$ is an initial vertex of $\mathcal{A}$. Moreover, the game $\tilde{\mathcal{G}} \times \mathcal{A}$ uses the acceptance set from $\mathcal{A}$, which is a Rabin language, so, by Lemma 4.50, she can win using a strategy given by a function $\sigma: \tilde{V}_{\text{Eve}} \to \tilde{E}$, where $Q$ is the set of states of $\mathcal{A}$ and $\tilde{V}_{\text{Eve}}$ the vertices controlled by Eve in $\tilde{\mathcal{G}}$ (a subset of $(V_{\text{Eve}} \sqcup (V \times E)) \times Q)$. We build a memory structure $(\mathcal{M}, \sigma_{\mathcal{M}})$ of size $|Q|$ that projects the strategy implemented by $\sigma$ onto $\mathcal{G}$:

- its set of states is $M = Q$,

- the initial state is $q_0$,

- the update function $\mu: M \times E \to M$ sends $\mu(q, e) = q'$ if $\sigma((v, e), q) = ((v, e), q) \to (v', q')$ is the move chosen by $\sigma$ from vertex $((v, e), q)$,

- for $v \in V_{\text{Eve}}$, $q \in M$, we let $\sigma_{\mathcal{M}}(v, q) = e$ if $e$ is the move chosen by $\sigma$ from $(v, q)$, that is, if $\sigma(v, q) = (v, q) \to ((v, q), e)$.

Since $\sigma$ implements a winning strategy in $\tilde{\mathcal{G}} \times \mathcal{A}$ from $(v, q_0)$, its projection onto $\mathcal{G}$ via the memory structure $(\mathcal{M}, \sigma_{\mathcal{M}})$ is a strategy that verifies that any play consistent with it produces as output a word in $\mathcal{L}(\mathcal{A})$, so it is winning. ◀

Theorem 4.48 is obtained by combining the fact that $|\mathcal{A}_{\mathcal{Z}_F}^{\text{Rabin}}| = \text{rbw}(\mathcal{Z}_F)$ with Proposition 4.49 (second item) and Corollary 4.51.
# 5 The alternating cycle decomposition: An optimal approach to Muller transition systems

In Section 4, we have provided minimal parity and Rabin automata for Muller languages, using the Zielonka tree. We can use these automata to transform Muller transition systems, by applying the product construction. However, this approach overlooks the structure of the transition system, meaning it does not take into account the relevant interplay between the underlying graph and the acceptance condition.

In this section, we present our main contributions: optimal transformations of Muller transition systems into parity and Rabin ones. The key novelty is that they precisely capture the way the transition system interacts with the acceptance condition. This is achieved by generalising Zielonka trees from Muller languages to Muller transition systems; we define the alternating cycle decomposition (ACD), consisting in a collection of Zielonka-tree-like structures subsuming all the structural information of the transition system necessary to determine whether a run is accepting or not. More precisely, the ACD is a succinct representation of the alternating chains of loops of a Muller automaton, in the sense of Wagner [80]. The alternating chains of loops of a DMA are known to determine the parity index of the language it recognises [80], and, as we will show, they also capture the essential information to define optimal transformations of automata.

We start with the definition of the alternating cycle decomposition in Section 5.1. In Section 5.2, we describe the ACD-parity-transform, turning a DMA $\mathcal{A}$ into an equivalent DPA ACD$_{parity}(\mathcal{A})$. Formally, the validity of this transformation is witnessed by a locally bijective morphism $\varphi: \text{ACD}_{parity}(\mathcal{A}) \to \mathcal{A}$ (Proposition 5.18). In Section 5.3, we describe the ACD-HD-Rabin-transform that turns a DMA $\mathcal{A}$ into an equivalent history-deterministic Rabin automaton ACD$_{Rabin}(\mathcal{A})$. The validity of the transformation is witnessed by an HD mapping $\varphi: \text{ACD}_{Rabin}(\mathcal{A}) \to \mathcal{A}$ (Proposition 5.25). These constructions grant strong optimality guarantees. The automaton ACD$_{parity}(\mathcal{A})$ (resp. ACD$_{Rabin}(\mathcal{A})$) has a minimal number of states amongst parity (resp. Rabin) automata admitting an HD mapping to $\mathcal{A}$ (Theorems 5.32 and 5.33). We note that this implies minimality amongst automata admitting a locally bijective morphism to $\mathcal{A}$. Moreover, the acceptance condition of ACD$_{parity}(\mathcal{A})$ uses an optimal number of colours (Theorem 5.31). The optimality of these constructions is shown in Section 5.4. We are able to prove the optimality of both constructions at the same time, by reducing the problem to an application of the minimality of the ZT-parity-automaton and the ZT-HD-Rabin-automaton.

In all this section, we let $\mathcal{T}\mathcal{S} = (G_{\mathcal{T}\mathcal{S}}, \text{Acc}_{\mathcal{T}\mathcal{S}})$ be a Muller transition system with underlying graph $G_{\mathcal{T}\mathcal{S}} = (V, E, \text{Source}, \text{Target}, I)$ and using a Muller acceptance condition $\text{Acc}_{\mathcal{T}\mathcal{S}} = (\gamma, \Gamma, \text{Muller}_{\Gamma}(\mathcal{F}))$.

## 5.1 The alternating cycle decomposition

► **Definition 5.1.** Let $\ell_0 \in \textit{Cycles}(\mathcal{T}\mathcal{S})$ be a cycle. We define the tree of alternating subcycles of $\ell_0$, denoted $\textit{AltTree}(\ell_0) = (N, \leq, \nu: N \to \textit{Cycles}(\mathcal{T}\mathcal{S}))$ as a $\textit{Cycles}(\mathcal{T}\mathcal{S})$-labelled tree with nodes partitioned into round nodes and square nodes, $N = N_\circ \sqcup N_\square$, such that:

- The root is labelled $\ell_0$.

- If a node is labelled $\ell \in \textit{Cycles}(\mathcal{T}\mathcal{S})$, and $\ell$ is an accepting cycle $(\gamma(\ell) \in \mathcal{F})$, then it is a round node, and its children are labelled exactly with the maximal subcycles $\ell' \subseteq \ell$ such that $\ell'$ is rejecting $(\gamma(\ell') \notin \mathcal{F})$.
■ If a node is labelled $\ell \in \text{Cycles}(\mathcal{T}\mathcal{S})$, and $\ell$ is a rejecting cycle ($\gamma(\ell) \notin \mathcal{F}$), then it is a square node, and its children are labelled exactly with the maximal subcycles $\ell' \subseteq \ell$ such that $\ell'$ is accepting ($\gamma(\ell') \in \mathcal{F}$). ▼

For a $\text{Cycles}(\mathcal{T}\mathcal{S})$-labelled tree $T = (N, \preceq, \nu: N \to \text{Cycles}(\mathcal{T}\mathcal{S}))$ and $n \in N$, we let $\nu_{\text{States}}(n) = \text{States}(\nu(n))$ be the set of states of the cycle labelling $n$.

► **Remark 5.2.** Let $n$ be a node of $\text{AltTree}(\ell_0)$ and let $n_1$ be a child of it. If $\ell'$ is a cycle such that $\nu(n_1) \subseteq \ell' \subseteq \nu(n)$, then $\nu(n_1)$ is accepting $\iff \ell'$ is rejecting $\iff \nu(n)$ is rejecting. ▼

► **Definition 5.3 (Alternating cycle decomposition).** Let $\mathcal{T}\mathcal{S}$ be a transition system, and let $\ell_1, \ell_2, \dots, \ell_k$ be an enumeration of its maximal cycles (that is, the edges sets of its SCCs). We define the alternating cycle decomposition of $\mathcal{T}\mathcal{S}$ to be the forest $\mathcal{ACD}_{\mathcal{T}\mathcal{S}} = \{\text{AltTree}(\ell_1), \dots, \text{AltTree}(\ell_k)\}$.

We let $N_{\ell_i}$ be the set of nodes of $\text{AltTree}(\ell_i)$, and $n_{\ell_i}$ its root. We will suppose that $N_{\ell_i} \cap N_{\ell_j} = \emptyset$ if $i \neq j$. ▼

We define the set of nodes of $\mathcal{ACD}_{\mathcal{T}\mathcal{S}}$ to be $\text{Nodes}(\mathcal{ACD}_{\mathcal{T}\mathcal{S}}) = \bigcup_{i=1}^k N_{\ell_i}$, and we let $\text{Nodes}_\circ(\mathcal{ACD}_{\mathcal{T}\mathcal{S}})$ (resp. $\text{Nodes}_\square(\mathcal{ACD}_{\mathcal{T}\mathcal{S}})$) be the subset of round (resp. square) nodes. As for Zielonka trees, we equip the trees of $\mathcal{ACD}_{\mathcal{T}\mathcal{S}}$ with an arbitrary order making them ordered trees. From now on, we will suppose that all trees of alternating subcycles are ordered, without explicitly mentioning it.

We remark that for a recurrent vertex $v$ of $\mathcal{T}\mathcal{S}$, there is one and only one tree $\text{AltTree}(\ell_i)$ in $\mathcal{ACD}_{\mathcal{T}\mathcal{S}}$ such that $v \in \nu_{\text{States}}(n_{\ell_i})$. On the other hand, transient vertices do not appear in the trees of $\mathcal{ACD}_{\mathcal{T}\mathcal{S}}$.

If $v$ is a recurrent vertex of $\mathcal{T}\mathcal{S}$, we define the *local subtree at* $v$, noted $\mathcal{T}_v$, as the subtree of $\text{AltTree}(\ell_i)$ containing the nodes $N_v = \{n \in N_{\ell_i} | v \in \nu_{\text{States}}(n)\}$. If $v$ is a transient vertex, we define $\mathcal{T}_v$ to be a tree with a single node.

For $v$ recurrent, as $N_v$ is a subset of the nodes of $\text{AltTree}(\ell_i)$, the tree $\mathcal{T}_v$ inherits the order from $\text{AltTree}(\ell_i)$, as well as its partition into round and square nodes, $N_v = N_{v,\circ} \sqcup N_{v,\square}$. Also, it inherits the labelling given by the mapping $\nu$, whose restriction to $\mathcal{T}_v$ has an image in $\text{Cycles}_v(\mathcal{T}\mathcal{S})$.

► **Remark 5.4.** Let $v \in \nu_{\text{States}}(n_{\ell_i})$. If $n \in N_v$ and $n'$ is an ancestor of $n$ in $\text{AltTree}(\ell_i)$, then $n' \in N_v$. In particular, $\mathcal{T}_v$ is indeed a subtree of $\text{AltTree}(\ell_i)$. Also, we note that the root of $\mathcal{T}_v$ is $n_{\ell_i}$. ▼

For a node $n \in N_{\ell_i}$ and an edge $e \in \ell_i$ we define $\text{Supp}(n, e) = n'$ to be the deepest ancestor of $n$ such that $e \in \nu(n')$. We remark that if $e = v \to v'$, then $\text{Supp}(n, e)$ is a node in both $\mathcal{T}_v$ and $\mathcal{T}_{v'}$.

► **Example 5.5.** We will use the transition system $\mathcal{T}\mathcal{S}$ from Figure 14 as a running example. We have named the edges of $\mathcal{T}\mathcal{S}$ with letters from $a$ to $l$, that are also used as the output colours of the acceptance condition. The acceptance set of $\mathcal{T}\mathcal{S}$ is the Muller language associated to:

$$ \mathcal{F} = \{\{c, d, e\}, \{e\}, \{g, h, i\}, \{l\}, \{h, i, j, k\}, \{j, k\}\}. $$

The initial vertex of $\mathcal{T}\mathcal{S}$, $v_0$, is its only transient vertex, all the others vertices are recurrent. $\mathcal{T}\mathcal{S}$ has 2 strongly connected components, corresponding to cycles $\ell_1$ and $\ell_2$.

The alternating cycle decomposition of $\mathcal{T}\mathcal{S}$ is shown in Figure 15. It consists of two trees, $\text{AltTree}(\ell_1)$ and $\text{AltTree}(\ell_2)$. We use Greek letters (in pink) to name the nodes of the tree. Inside each node we indicate both its label $\nu(n)$ and the set of states of it. For example,