Antonio Casares

Thomas Colcombet

Nathanaël Fijalkow

Karoliina Lehtinen

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

Keywords: 2012 ACM Subject Classification Theory of computation → Automata over infinite Emerson-lei automata, good-for-games, paritizing, omega-regular languages

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.

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,[START_REF] Bloem | Graph games and reactive synthesis[END_REF] 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 ω-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 ω-regular languages with deterministic automata; it could even be argued that there is a canonical aspect to them:

For every ω-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 F ⊆ 2 Γ + of subsets of colours such that both 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,[START_REF] Boker | History determinism vs. good for gameness in quantitative automata[END_REF], 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 A with a deterministic parity automaton recognising the acceptance condition used by 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 [START_REF] Schewe | Determinising parity automata[END_REF]: 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,[START_REF] Schewe | Determinising parity automata[END_REF]. 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 B has been obtained as a transformation of a Muller automaton A, there will be a morphism ϕ : B → 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 historydeterminism [START_REF] Boker | When a little nondeterminism goes a long way: An introduction to history-determinism[END_REF]21] that an example of an ω-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 [START_REF] Casares | Optimal transformations of games and automata using Muller conditions[END_REF] 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 [START_REF] Piterman | Temporal logic and fair discrete systems[END_REF] and stochastic games [40].

The contribution at the core of this work is a generalisation of Zielonka trees to general Muller automata recognising any ω-regular language, which we call the alternating cycle decomposition (ACD). The ACD, greatly inspired from Wagner's work on ω-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.

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 [START_REF] Piterman | Temporal logic and fair discrete systems[END_REF]. 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)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 [START_REF] Schewe | Determinising parity automata[END_REF], 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 ϕ : B → A witnesses the fact that B has been obtained from A by blowing up each state q ∈ A to the states in ϕ -1 (q). However, this property on its own does not suffice to guarantee the semantic equivalence of A and 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 defined using a minimal set of hypothesis guaranteeing the semantic equivalence of A and B.

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 A into an equivalent parity automaton B while preserving the determinism of A (formally, there is a locally bijective morphism ϕ : B → A). This transformation comes with a strong optimality guarantee: for any other parity automaton B admitting a locally bijective morphism (or even HD mapping) ϕ : B → A, the automaton B is smaller than B and it uses less output colours (Theorems 5.31 and 5.32).

An interesting corollary of our result is the following: if B is an HD parity automaton that is strictly smaller than any deterministic parity automaton recognising L(B), then 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 A into a historydeterministic Rabin automaton B in an optimal way: for any other Rabin automaton B admitting an HD mapping ϕ : B → A, the automaton B is smaller than 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 A, we can define a Rabin condition over the underlying graph of A obtaining an equivalent automaton if and only if the union of rejecting cycles of A is again a rejecting cycle. Our results unify and extend those from [START_REF] Boigelot | On the use of weak automata for deciding linear arithmetic with integer and real variables[END_REF]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 ω-regular languages [START_REF] Muller | Infinite sequences and finite machines[END_REF] and learning of ω-automata [START_REF] Bohn | Constructing deterministic parity automata from positive and negative examples[END_REF]. 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 [START_REF] Muller | Infinite sequences and finite machines[END_REF]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,[START_REF] Emerson | Tree automata, mu-calculus and determinacy (extended abstract)[END_REF]. 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 [START_REF] Boker | Parityizing Rabin and Streett[END_REF], and incorporates material from another conference paper [START_REF] Boker | History determinism vs. good for gameness in quantitative automata[END_REF]. 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 [START_REF] Boker | Parityizing Rabin and Streett[END_REF]. Most of the material concerning deterministic automata and locally bijective morphisms comes from [START_REF] Boker | Parityizing Rabin and Streett[END_REF]. 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 [START_REF] Boker | Parityizing Rabin and Streett[END_REF], the optimality of the Zielonka-tree-parity-automaton and the ACDparity-transform was proven only with respect to deterministic automata and locally bijective morphisms, respectively. Moreover, the proof of the optimality of the ACDparity-transform (Theorem 5.32) has been simplified. ICALP 2022 [START_REF] Boker | History determinism vs. good for gameness in quantitative automata[END_REF]. The construction of history-deterministic Rabin automata for Muller languages (Section 4.3) and its optimality (Theorem 4.48) come from [START_REF] Boker | History determinism vs. good for gameness in quantitative automata[END_REF]. 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 [START_REF] Boker | Parityizing Rabin and Streett[END_REF], 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 [START_REF] Büchi | On a decision method in restricted second order arithmetic[END_REF], where transformations based on the ACD are compared to the state-of-the-art existing paritizing methods.

The typeness results steaming from the ACD [START_REF] Boker | Parityizing Rabin and Streett[END_REF]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 [START_REF] Boker | History determinism vs. good for gameness in quantitative automata[END_REF].

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 \ {∅}. For a family of subsets F ⊆ 2 A and A ⊆ A, we write F| A = F ∩ 2 A . For natural numbers i ≤ j, [i, j] stands for {i, i + 1, . . . , j -1, j}.

For a set Σ, a word over Σ is a sequence of elements from Σ. An ω-word (or simply an infinite word) is a word of length ω. The sets of finite and infinite words over Σ will be written Σ * and Σ ω , respectively, and we let Σ ∞ = Σ * ∪ Σ ω . Subsets of Σ * and Σ ω will be called languages. For a word w ∈ Σ ∞ we write w i to represent the i-th letter of w. We let ε denote the empty word, and let Σ + = Σ * \ {ε}. The concatenation of two words u ∈ Σ * and v ∈ Σ ∞ is written u • v, or simply uv. If u = v • w for v ∈ Σ * , u, w ∈ Σ ∞ , we say that v is a prefix of u and we write v u. For a word w ∈ Σ ω , we let Inf(w) = {a ∈ Σ | w i = a for infinitely many i ∈ N}.

We say that a language L ⊆ Σ ω is prefix-independent if for all w ∈ Σ ω and u ∈ Σ * , uw ∈ L if and only if w ∈ L.

Given a map α : A → B, we will extend α to words component-wise, i.e., α : A ∞ → B ∞ will be defined as α(w 0 w 1 w 2 . . . ) = α(w 0 )α(w 1 )α(w 2 ) . . . . We will use this convention throughout the paper without explicitly mentioning it. If A ⊆ A, we note α| A the restriction of α to A . We let Id A be the identity function on A. We write α : A B if α is a partial mapping (it is defined only over some subset of A).

A graph2 is a tuple G = (V, E, Source, Target) where V is a set of vertices, E a set of edges and Source : E → V and Target : E → V are maps indicating the source and target for each edge. A path is a (finite or infinite) sequence ρ = e 0 e 1 ... ∈ E ∞ such that Source(e i ) =

Target(e i-1 ) for all i > 0. For notational convenience, we write v 0

e0 -→ v 1 • • • en-1
---→ v n to denote a finite path from v 0 = Source(e 0 ) to v n = Target(e n-1 ) and we let Source(ρ) = v 0 and Target(ρ) = v n . For A ⊆ V , we let Path fin A (G) and Path A (G) denote, respectively, the set of finite and infinite paths on G starting from some v ∈ A (we omit brackets if

A = {v} is a singleton). We let Path ∞ A (G) = Path fin A (G) ∪ Path A (G).
For a subset of vertices A ⊆ V we write:

In(A) = {e ∈ E | Target(e) ∈ A}, Out(A) = {e ∈ E | Source(e) ∈ 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, Source, Target) is a graph (V , E , Source , Target ) such that V ⊆ V , E ⊆ E and Source and Target are the restrictions of Source and 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.

Transition systems, automata and games

Transition systems. A pointed graph G = (V, E, Source, Target, I) is a graph together with a non-empty subset of initial vertices I ⊆ V . An acceptance condition over G is a tuple Acc = (γ, Γ, W) where Γ is a finite set of colours, γ : E → Γ ∪ {ε} is an edge-colouring of G and W ⊆ Γ ω is a language of infinite words called the acceptance set. We allow uncoloured edges (ε-edges), but we impose the condition that no infinite path of G is eventually composed exclusively of ε-edges (that is, every cycle contains some edge e with γ(e) = ε).

A transition system (abbreviated TS) is a tuple TS = (G TS , Acc TS ), where G TS = (V, E, Source, Target, I) is a pointed graph, called the underlying graph of TS, and Acc TS = (γ, Γ, W) is an acceptance condition over G TS . We will also refer to vertices and edges as states and transitions, respectively. We write v c -→ v if there is e ∈ E such that Source(e) = v, Target(e) = v and γ(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 Ĩ ⊆ V , we let TS Ĩ be the transition system obtained from TS by setting Ĩ to be its set of initial vertices. The size of a transition system TS is the cardinality of its set of vertices, written |TS|.

A run on a transition system TS (or on a pointed graph) is a (finite or infinite) path ρ = e 0 e 1 • • • ∈ E ∞ starting from an initial vertex, that is, Source(e 0 ) ∈ I. We let Run fin (TS) and Run(TS) be the set of finite and infinite runs on TS, respectively, and we let Run ∞ (TS) = Run fin (TS) ∪ Run(TS). (We note that Run(TS) = Path I (G TS ).)

The output of a run ρ ∈ Run ∞ (TS) is the sequence of colours in Γ ∞ obtained by removing the occurrences of ε from γ(ρ); which we will also denote by γ(ρ) by a small abuse of notation. A run ρ is accepting if γ(ρ) ∈ W, and rejecting otherwise (in particular, finite runs will be rejecting). We write ρ = v w v to denote a run with Source(ρ) = v, Target(ρ) = v and

γ(ρ) = w.
We say that a vertex v ∈ 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 ⊆ V is accessible if every state v ∈ 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 → L V , l E : E → 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 Acc = (γ, Γ, W) of a transition system, Γ = E is the whole set of edges and γ is the identity function. Indeed, an equivalent acceptance condition can always be defined by using the acceptance set

W = {w ∈ E ω | γ(w) ∈ W} ⊆ E ω .
Automata. A (non-deterministic) automaton over Σ is an edge-labelled transition system A = (G A , Acc A , (l Σ , Σ)), where Σ is a finite set of input letters. Let A be an automaton with G A = (Q, ∆, Source, Target, I) as underlying graph and Acc A = (γ, Γ, W) as acceptance condition. We write e = q a:c --→ q to denote that e ∈ ∆ satisfies l Σ (e) = a and γ(e) = c. We can suppose that ∆ ⊆ Q × Σ × Γ × Q. We define:

δ(q, a) = {(q , c) ∈ Q × Γ | there is e = q a:c --→ q ∈ ∆}.
We note that we can now recover the classical representation of an automaton as a tuple A = (Q, Σ, I, Γ, δ, W), (or (Q, Σ, I, Γ, ∆, W)) which we might use when working exclusively with automata.

We say that an automaton A is deterministic if I is a singleton and for every q ∈ Q and a ∈ Σ, |δ(q, a)| ≤ 1. We say that A is complete if for every q ∈ Q and a ∈ Σ, |δ(q, a)| ≥ 1. We remark that we can suppose that automata are complete without loss of generality by adding a sink state.

Given an automaton A and a word w ∈ Σ ∞ , a run over w in A is a run ρ = e 0 e 1 • • • ∈ Run ∞ (A) such that l Σ (e i ) = w i for all i ≥ 0. A word w ∈ Σ ω is accepted by A if it exists a run over w that is accepting (that is, a run ρ such that γ(ρ) ∈ W). The language accepted (or recognised) by an automaton A is the set

L(A) := {w ∈ Σ ω | w is accepted by A}.
Two automata recognising the same language are said equivalent.

We remark that if A is deterministic (resp. complete), there is at most one (resp. at least one) run over w for each w ∈ Σ ∞ .

Given a subgraph G of the underlying graph of an automaton 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 A.

History-deterministic automata.

Let A be a (non-deterministic) automaton over Σ with ∆ as set of transitions and I as set of initial states. A resolver for A is a pair (r 0 , r), consisting of a choice of an initial state3 , r 0 ∈ I, and a function r : ∆ * × Σ → ∆ such that for all words w = w 0 w 1 • • • ∈ Σ ω , the sequence e 0 e 1 • • • ∈ ∆ ω , called the run induced by r over w and defined by e i = r(e 0 . . . e i-1 , w i ) is actually a run over w in A starting from r 0 . We say that the resolver is sound if it satisfies that for every w ∈ L(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 A letter-by-letter with only the knowledge of the word so far, for all words in L(A). An automaton 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 A over Σ = {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 Γ = {1, 2} and its acceptance set is W = {u ∈ {1, 2} ω | u contains finitely many 1s} (this is a coBüchi condition, as introduced in the next section). It is easy to check that A recognises the language:

L(A) = {w ∈ Σ ω | Inf(w) ⊆ {a, b} or Inf(w) ⊆ {b, c}}.
A resolver for 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: 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. ---→ q represents two different transitions with input letters a and b, respectively. The initial state q0 is marked with one incoming arrow.

q 0 q 1 q 2 a, b : 2 c : 1 a, b : 2 b, c : 2 a : 1 b, c : 2
We say that an state q is reachable using the resolver (r 0 , r) if there is a finite run ρ = r 0 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 A be an HD automaton, let (r 0 , r) be a sound resolver for it and let à be the subautomaton induced by the set of states reachable using (r 0 , r), with initial state r 0 . Then, L(A) = L( Ã).

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 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 A that is reachable using some sound resolver, it is verified that A recognises the same language if we fix q as initial state, that is, L(A) = L(A q ). Moreover, A q is also history-deterministic. In particular, if A is deterministic, this is the case for any reachable state q.

Games. A game is a vertex-labelled transition system G = (G G , Acc G , (l Players , {Eve, Adam})), with G G = (V, E, Source, Target, I) a pointed graph, and l Players : V → {Eve, Adam} a vertexlabelling function inducing a partition of V into vertices controlled by two players that we refer to as Eve and Adam. We let V Eve = l -1 Players (Eve) and V Adam = l -1 Players (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 Out(v) and the token travels through this edge to its target. In this way, they produce an infinite run ρ on G (that we also call a play). The objective of Eve is to produce an accepting run (a sequence of colours in W), and Adam tries to prevent it.

A strategy from v ∈ V for Eve is a (partial) function strat v : Path fin v (G) E, defined for finite paths from v ending in a vertex in V Eve , that tells Eve which move to choose after any possible finite play. We say that a play ρ ∈ Path ∞ v (G) is consistent with the strategy strat v if after each finite prefix ρ ρ ending in a vertex controlled by Eve, the next edge in ρ is strat v (ρ ). We say that strat v is a winning strategy for Eve if all plays from v consistent with strat v are accepting. We say that Eve wins the game G from v if there is a winning strategy from v for her. Strategies for Adam are defined dually.

Given a game G, the winning region of G for Eve, written W Eve (G), is the set of initial vertices v ∈ I such that she wins the game G from v. The full winning region of G for Eve is her winning region in the game G V where all vertices are initial, that is, the set of vertices v ∈ V such that Eve wins the game 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 M = (M, E M , Source, Target, m 0 ) with a single initial state m 0 and labels l M : E M → X inducing a deterministic structure, that is, satisfying that for each m ∈ M and x ∈ X there is at most one transition e ∈ Out(m) labelled x. We denote µ : M × X M the update function

given by µ(m, x) = m if m x -→ m is the (only) transition from m labelled x. We extend µ to µ : M × X * M by induction (µ(m, ε) = m and µ(m, x 1 . . . x n ) = µ(µ(m, x 1 . . . x n-1 ), x n )).
A memory structure (for Eve) for a game G is a memory skeleton over the set E of edges of G together with a next-move function σ :

V Eve × M → E. We say that(M, σ) implements a strategy strat v : Path fin v (G) E if for any finite play ρ ∈ Path fin v (G) ending in V Eve , strat v (ρ) = σ(Target(ρ), µ(m 0 , ρ)).
We remark that a memory structure for G implements at most one strategy from a given vertex. We say that 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 TS = (G TS , Acc TS ) be a transition system, with G TS = (V, E, Source TS , Target TS , I TS ) and Acc TS = (γ TS , Σ, W TS ), and let A = (G A , Acc A , (l Σ , Σ)) be a complete automaton over the alphabet Σ, where G A = (Q, ∆, Source A , Target A , I A ) and Acc A = (γ A , Γ, W A ). The composition of TS and A (also called their product) is the transition system TS A defined as follows:

The set of vertices is the cartesian product V × Q. The set of initial vertices is

I TS × I A . The set of edges E contains a transition (v, q) c - → (v , q ) if there is a ∈ Σ and transitions e 1 = v a -→ v ∈ E and e 2 = q a:c --→ q ∈ ∆. It also contains ε-edges (v, q) ε -→ (v , q) if v ε -→ v ∈ E. Formally, E = {(e 1 , e 2 ) ∈ E × ∆ | γ TS (e 1 ) = l Σ (e 2 )} ∪ {e 1 ∈ E | γ TS (e 1 ) = ε} ⊆ (E × ∆) ∪ E.
The acceptance condition is inherited from that of A: the colouring function γ : E → Γ is defined as γ (e 1 , e 2 ) = γ(e 2 ), and the acceptance set is

W A ⊆ Γ ω .
We remark that if TS does not contain an uncoloured cycle, neither does TS A. Also, TS A does not contain sinks by completeness of A.

If TS is a labelled transition system, labelled by the functions l V and l E , we consider TS A as a labelled transition system with the functions l V (v, q) = l V (v) and l E (e 1 , e 2 ) = l E (e 1 ) (resp. l E (e 1 ) = l E (e 1 ) if e 1 is an uncoloured edge).

Intuitively, a computation in TS A happens as follows: we start from a vertex v 0 ∈ I TS in TS and from q 0 ∈ I A . When we are in a position (v, q) ∈ V × Q, a transition e between v and v takes place in TS, producing a letter a ∈ Σ as output. Then, the automaton A proceeds using a transition corresponding to a, producing an output in Γ. In this way, a word in Γ ω is generated and we can use the acceptance set W A ⊆ Γ ω of the automaton as the acceptance set for TS A.

In particular, we can perform this operation if TS is an automaton. We obtain in this way a new automaton that uses the acceptance condition of A.

We could, of course, apply this construction to a game G, obtaining a new game G A in which the player who makes a move in G also chooses a transition in 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 - → v such that v ∈ V Adam , the edge e is uncoloured (γ(e) = ε), v ∈ V Eve
, and e is the only incoming edge to v (In(v ) = {e}). We remark that any game 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 B be an automaton with acceptance set W B and let A be an automaton recognising L(A) = W B . Then, L(B A) = L(B). Moreover, if A and B are deterministic (resp. history-deterministic), so is B A. Proposition 2.7 ([38]). Let G be a game that is suitable for transformations with acceptance set W G , and let A be a history-deterministic automaton recognising L(A) = W G . Then, the winning region of Eve in G is the projection of her winning region in G A, that is, Eve wins G from an initial vertex v if and only if she wins G A from (v, q 0 ), for q 0 some initial vertex of 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 A be an automaton recognising W G ⊆ Σ ω satisfying that for every game G suitable for transformations with acceptance set W G , Eve wins the game G from an initial vertex v if and only if she wins G A from (v, q 0 ), for q 0 some initial vertex of A. Then, A is history-deterministic.

Muller languages, cycles and the parity hierarchy

Languages commonly used as acceptance sets. We now define the main classes of languages used by ω-regular automata as acceptance sets. We let Γ stand for a finite set of colours.

Büchi. Given a subset B ⊆ Γ, we define the Büchi language associated to B as:

Büchi Γ (B) = {w ∈ Γ ω | Inf(w) ∩ B = ∅}.
We say that a language L ⊆ Γ ω is a Büchi language if there is a set B ⊆ Γ such that L = Büchi Γ (B). coBüchi. Given a subset B ⊆ Γ, we define the coBüchi language associated to B as:

coBüchi Γ (B) = {w ∈ Γ ω | Inf(w) ∩ B = ∅}.
We say that a language L ⊆ Γ ω is a coBüchi language if there is a set

B ⊆ Γ such that L = coBüchi Γ (B). Rabin. A Rabin language is represented by a family R = {(G 1 , R 1 ), . . . , (G r , R r )} of Rabin
pairs, where G j , R j ⊆ Γ. The Rabin language associated to R is defined as:

Rabin Γ (R) = {w ∈ Γ ω | [Inf(w) ∩ G j = ∅ and Inf(w) ∩ R j = ∅] for some index j}. If [Inf(w) ∩ G j = ∅ and Inf(w) ∩ R j = ∅],
we say that w is accepted by the Rabin pair (G j , R j ). We say that a language L ⊆ Γ ω is a Rabin language if there is a family of Rabin pairs R such that L = Rabin Γ (R). Streett. The Streett language associated to a family

S = {(G 1 , R 1 ), . . . , (G r , R r )} of Rabin
pairs is defined as:

Streett Γ (S) = {w ∈ Γ ω | [Inf(w) ∩ G j = ∅ implies Inf(w) ∩ R j = ∅] for all indices j}.
We say that a language L ⊆ Γ ω is a Streett language if there is a family of Rabin pairs S such that L = Streett Γ (S). Parity. We define the parity language over the alphabet [d min , d max ] ⊆ N as:

parity [dmin,dmax] = {w ∈ [d min , d max ] ω | min Inf(w) is even}.
We say that a language L ⊆ Γ ω is a [d min , d max ]-parity language if there is a mapping φ : Γ → [d min , d max ] such that for all w ∈ Γ ω , w ∈ L if and only if φ(w) ∈ parity [dmin,dmax] . We say that L is a parity language if there are d min , d max ∈ N such that L is a [d min , d max ]parity language. Muller. We define the Muller language associated to a family F ⊆ 2 Γ + of non-empty subsets of Γ as:

Muller Γ (F) = {w ∈ Γ ω | Inf(w) ∈ F}.
We say that a language L ⊆ Γ ω is a Muller language if there is a family F ⊆ 2 Γ + such that L = Muller Γ (F).

We drop the subscript Γ (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 ∈ Γ ω and u ∈ Γ * , uw ∈ L if and only if w ∈ 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 N and φ 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 [START_REF] Boker | Why these automata types?[END_REF] 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. Relations between subclasses of Muller languages. An arrow from a class X towards a class Y means that if a language L ⊆ Γ ω 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].

Remark 2.10. A language L ⊆ Γ ω is a Muller language if and only if it satisfies: For all w, w ∈ Γ ω , if Inf(w) = Inf(w ), then w ∈ L ⇐⇒ w ∈ 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 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 ω-regular. Many other equivalent definitions exist. Notably, ω-regular languages are exactly the languages that can be defined using monadic second-order logic [14], those that can be described by using ω-regular expressions [57], and those that can be recognised by an ω-semigroup [66, Chapter 2].

Cycles. Let TS be a transition system with V and E as set of vertices and edges, respectively. A cycle of TS is a subset ⊆ E such that there is a finite path v 0

e0 -→ v 1 e1 -→ v 2 - → . . . v r er
-→ v 0 with = {e 0 , e 1 , . . . , 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 is States( ) = {v 0 , v 1 , . . . v r }. The set of cycles of a transition system TS is written Cycles(TS). We will consider the set of cycles ordered by inclusion. For a state v ∈ V , we note Cycles v (TS) the subset of cycles of TS containing v. We remark that a vertex v is recurrent if and only if Cycles v (TS) = ∅. We note that Cycles v (TS) is closed under union; moreover, the union of two cycles 1 , 2 ∈ Cycles(TS) is again a cycle if and only if there is some state v such that both 1 and 2 contain v.

Let TS be a Muller transition system with acceptance condition (γ, Γ, Muller Γ (F)). Given a cycle ∈ Cycles(TS), we say that is accepting (resp. rejecting) if γ( ) ∈ F (resp. γ( ) / ∈ 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 ρ ∈ Run(TS), the set of transitions taken infinitely often forms a cycle, Inf(ρ) = ρ ∈ Cycles(TS), and ρ is an accepting run if and only if ρ is an accepting cycle.

The deterministic and history-deterministic parity hierarchy. As we have mentioned, every ω-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 ω-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 ω-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]. Definition 2.14 (Parity index of a language). Let L ⊆ Σ ω be an ω-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 ≥ 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]).

[0, 0] [1, 1] Weak 1 [0, 1] [1, 2] Weak 2 [0, 2] [1, 3]
We say that L has parity index at least 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 ≥ d. We say that the parity index of L is 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 ω-regular language L, there is a unique d such that either L has parity index [0, d -1], [1, d] or Weak d , and these options are mutually exclusive. See also Appendix A for more details about languages of parity index 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 ω-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 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 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 Weak d , then A uses at least d + 1 output colours.

We show next that the parity index of an ω-regular language can be read directly from a deterministic Muller automaton.

Let TS be a transition system using the Muller acceptance condition (γ, Γ, Muller Γ (F)). A d-flower over a state v of TS is a set of d cycles 1 , 2 , . . . , d ∈ Cycles v (TS) such that i i+1 and γ( i ) ∈ F ⇐⇒ γ( i+1 ) / ∈ F. We say that it is a positive flower if γ( 1 ) ∈ F and that it is negative otherwise. Lemma 2.16 (Flower Lemma,[65,80]). Let A be a DMA. If A admits an accessible positive (resp. negative) d-flower, then L(A) has parity index at least [0, d -1] (resp. [1, d]). If A admits both accessible positive and negative d-flowers, then L(A) has parity index at least Weak d .

Conversely, if an ω-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.

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, ) is a non-empty finite set of nodes N equipped with an order relation called the ancestor relation (we say that x is an ancestor of y, or that y is below x if x y), such that (1) there is a minimal node for , called the root, and (2) the ancestors of an element are totally ordered by . The converse relation is the descendant relation. Maximal nodes are called leaves, and the set of leaves of T is denoted by Leaves(T ). The minimal strict descendants of a node are called its children. The set of children of n in T is written Children T (n). The depth of a node n is the number of strict ancestors of it. We note it Depth(n). The height of a tree T is the maximal length of a chain for the ancestor relation.

A subtree of T = (N, ) is a tree T = (N , ) such that N ⊆ N ,
is the restriction of to N and Children T (n ) ⊆ Children T (n ) for all n ∈ 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 .

An ordered tree is a tree T = (N, ) together with a total order ≤ n over Children T (n), for each node n ∈ 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 ≤ T on T (the depth-first order): let n, n ∈ N . If n n , we let n ≤ 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 ∈ Children T (n m ) such that n 1 n and n 2 n . We let n ≤ T n if and only if n 1 ≤ nm 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 ∈ Children T (n), we let

Next T (n ) =    min ≤n {n ∈ Children T (n) | n < n n } if this set is not empty, min ≤n {n ∈ Children T (n)} otherwise.
That is, the function Next T maps each child of n to a sibling that is its successor in T for the ≤ n -order, in a cyclic way.

Let T = (N , ) be a subtree of T = (N, ). Let n m ∈ N and

n o ∈ N such that n m is a strict ancestor of n o (n m ≺ n o ). If n m is a leaf of T , we define Jump T (n o , n m ) = n m .
If not, we define Jump T (n o , n m ) = l dest ∈ Leaves(T ) to be the only node satisfying that there are two children of n m in T , n 1 , n 2 ∈ Children T (n m ) such that:

n 1 n o , n 2 = Next T (n 1 ) (in particular, n 2 ∈ N ), l dest n 2 is the leftmost 4 leaf in T (minimal for ≤ 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 Jump T (n o , n m ) to be the leftmost leaf of T below n o . Intuitively, l = 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 ν : N → 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.

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 ϕ : B → A witnesses that each state q ∈ A has been augmented to ϕ -1 (q). To ensure that B is semantically equivalent to A, the morphism has to grant a further guarantee, namely, we need to be able to simulate runs of A in B. We will examine two properties of morphisms that allow to do this: local bijectivity and history-determinism for mappings.

In all this section, TS = (G, Acc) and TS = (G , Acc ) will stand for transition systems with underlying graphs G = (V, E, Source, Target, I) and G = (V , E , Source , Target , I ), and acceptance conditions Acc = (γ, Γ, W) and Acc = (γ , Γ , W ).

Morphisms of transition systems

Definition 3.1. A morphism of graphs from G to G is a pair of mappings ϕ = (ϕ V : V → V , ϕ E : E → E ) preserving edges, that is: Source (ϕ E (e)) = ϕ V (Source(e)) for every e ∈ E, Target (ϕ E (e)) = ϕ V (Target(e)) for every e ∈ E.
We say that ϕ is a morphism of pointed graphs if, moreover, it preserves initial vertices:

ϕ V (v 0 ) ∈ I for every v 0 ∈ 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 ϕ is a morphism of labelled graphs if, in addition, L V ⊆ L V , L E ⊆ L E and ϕ preserves labels: l V (ϕ V (v)) = l V (v) for every v ∈ V , l E (ϕ E (e)) = l E (e)
for every e ∈ V .

We will write ϕ : G → G to denote a morphism ϕ. We will drop the subscript in ϕ V and ϕ E whenever it can be deduced from its use. We say that ϕ is surjective (resp. injective) if ϕ V is.

Note that the mapping ϕ V does not completely determine a morphism ϕ, as multiple edges might exist between two given vertices. However, if G has no isolated vertices, the mapping ϕ E does determine it. It will be convenient nonetheless to also keep the notation for ϕ 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 ϕ : G → G induces a mapping

ϕ Runs : Run ∞ (G) → Run ∞ (G ).
Definition 3.2. Let TS and TS be two (labelled) transition systems. A weak morphism of (labelled) transition systems ϕ : TS → TS is a morphism of (labelled) pointed graphs between their underlying graphs, ϕ : G → G . We say that it is a morphism of (labelled) transition systems if it preserves the acceptance of runs, that is:

for every infinite run ρ ∈ Run(TS), γ(ρ) ∈ W ⇐⇒ γ (ϕ Runs (ρ)) ∈ W .
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 ϕ : TS → TS is an isomorphism if ϕ V and ϕ E are bijective and ϕ -1 = (ϕ -1

V , ϕ -1 E ) is a morphism from TS to TS. In that case, we say that TS and TS are isomorphic.

Local properties of morphisms Definition 3.3. A morphism of pointed graphs ϕ : G → G is called:

Locally surjective if it verifies:

1. For every v 0 ∈ I there exists v 0 ∈ I such that ϕ(v 0 ) = v 0 . 2. For every v ∈ V and every e ∈ Out(ϕ(v)) there exists e ∈ Out(v) such that ϕ(e) = e .

Locally injective if it verifies:

1. For every v 0 ∈ I , there is at most one v 0 ∈ I such that ϕ(v 0 ) = v 0 . 2. For every v ∈ V and every couple e 1 , e 2 ∈ Out(v), ϕ(e 1 ) = ϕ(e 2 ) implies e 1 = e 2 .

Locally bijective if it is both locally surjective and locally injective.

Equivalently, a morphism of pointed graphs ϕ is locally surjective (resp. locally injective) if for every v ∈ V the restriction of ϕ E to Out(v) is a surjection onto Out(ϕ(v)) (resp. an injection into Out(ϕ(v))), and the restriction of ϕ V to I is a surjection onto I (resp. an injection into I ).

Let ϕ : TS → TS be a (weak) morphism, and let ρ = v 0 e 0 -→ v 1 e 1 -→ . . . be a run in TS . If ϕ is locally surjective, we can pick an initial vertex v 0 in ϕ -1 (v 0 ) and build step-by-step a run ρ in TS from v 0 that is sent to ρ under ϕ. If ϕ is moreover locally bijective, the choices of the initial vertex and the edges at each step are unique, so runs in TS can be simulated in TS via ϕ in a unique way. Said differently, if ϕ : TS → TS is a locally bijective morphism, we can see TS as an automaton that processes runs of 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 TS and 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 γ(e) to coincide with the colour γ (ϕ(e)). This allows us to compare transition systems using different types of acceptance conditions. Remark 3.4. Let ϕ be a morphism of pointed graphs.

1.

If ϕ is locally surjective, then ϕ Runs is surjective. 2. If ϕ is locally injective, then ϕ Runs is injective.

3.

If ϕ is locally bijective, then ϕ Runs 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 ϕ : TS → TS is a locally surjective weak morphism, it is onto the accessible part of TS . That is, for every accessible state v ∈ TS , there exists some state v ∈ TS such that ϕ V (v) = v . In particular, if every state of TS is accessible, ϕ is surjective.

Proof. Let v be an accessible state of TS . By definition, there exists a finite run ρ from an initial vertex of TS to v . By surjectivity of ϕ Runs , there is a finite run ρ ∈ Run fin (TS) such that ϕ Runs (ρ) = ρ . As ϕ is a morphism of graphs, we have that ϕ(Target(ρ)) = v .

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 F = {{α}, {β}}. The morphism is given by ϕ

V (v 1 ) = ϕ V (v 2 ) = v and ϕ V (v 2 ) = v 2 .
In this case, the mapping ϕ V determines a unique morphism; the (uniquely determined) mapping ϕ 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.

v 1 v 2 u 1 2 1 2 1 1 2 v ′ u ′ α β β λ Figure 5
A locally bijective morphism from a parity TS to a Muller TS with acceptance set given by F = {{α}, {β}}. We use dashed arrows to represent the images of vertices, and colours to represent the image of edges (that can be inferred from ϕV ).

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 ϕ(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 A is an HD automaton recognising the acceptance set ot TS, the composition TS A does not admit a locally bijective morphism to TS, 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 ϕ : TS → TS is an HD mapping, we can simulate runs of TS in TS via ϕ while preserving their acceptance. This will allow us to show that ϕ witnesses the semantic equivalence of TS and TS (Section 3.4).

Morphisms

Loc. Injective Morphisms

Loc. Surjective Morphisms

Loc. Bijective Morphisms

HD Mappings Weak Morphisms

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).

History-deterministic mappings

Let TS and TS be transition systems and ϕ : TS → TS a weak morphism between them. A resolver simulating ϕ consists in a pair of functions r Init : I → I and r : E * × E → E such that:

1. ϕ(r Init (v 0 )) = v 0 for all v 0 ∈ I , 2. ϕ(r(ρ, e )) = e , for all ρ ∈ E * and e ∈ E , 3. if e 0 ∈ Out(I ), Source(r(ε, e 0 )) = r Init (Source(e 0 )), and 4. if ρ is a finite run in TS ending in v and e ∈ Out(ϕ(v)), then r(ρ, e ) ∈ Out(v). Given a run ρ = e 0 e 1 • • • ∈ Run ∞ (TS ) starting in some v 0 ∈ I , the run induced by r is the sequence r Runs (ρ ) = e 0 e 1 e 2 • • • ∈ Run ∞ (TS)
defined by e i = r(e 0 . . . e i-1 , e i ), which is indeed a run in TS. We say that the resolver is sound if for every accepting run ρ ∈ Run(TS ), the run r Runs (ρ ) is accepting in TS. Note that we do not impose r Runs (ρ ) to be rejecting if ρ is.

Remark 3.7. Provided that all states of TS are accessible, a resolver simulating ϕ can only exist if ϕ is a locally surjective weak morphism.

Said differently, a sound resolver simulating ϕ is a winning strategy for the player Duplicator in the following game:

In round 0, Spoiler picks an initial vertex v 0 in TS . Duplicator responds by picking an initial vertex v 0 in TS such that ϕ(v 0 ) = v 0 . In round n > 0, Spoiler picks an edge e n in TS , and Duplicator responds by picking an edge e n in TS such that ϕ(e n ) = e n . Duplicator wins if either e 1 e 2 . . . is an accepting run in TS from v 0 or e 1 e 2 . . . is not an accepting run in TS from v 0 (it is either not a run from v 0 or not accepting). Spoiler wins otherwise. Definition 3.8. Let TS and TS be (labelled) transition systems. A history-deterministic mapping (HD mapping) of transition systems from TS to TS is a pair of mappings ϕ = (ϕ

V : V → V , ϕ E : E → E ) such that:
ϕ is a weak morphism, ϕ preserves accepting runs: ρ ∈ Run(TS) and γ(ρ) ∈ W =⇒ γ (ϕ Runs (ρ)) ∈ W , and there exists a sound resolver simulating ϕ.

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 ϕ Runs preserving the acceptance of runs. Lemma 3.9. Let ϕ : TS → TS be an HD mapping and let (r Init , r) be a sound resolver simulating it. The following holds:

ϕ Runs • r Runs = Id Run ∞ (TS ) .
r Runs preserves the acceptance of runs in TS , that is, for every run ρ ∈ Run(TS ), ρ is accepting if and only if r Runs (ρ ) is accepting in TS.

Proof. The first item follows from the fact that ϕ(r(ρ, e )) = e for every ρ ∈ E * and e ∈ E .

For the second item, the definition of a sound resolver imposes that if ρ is accepting, so is r Runs (ρ ). For the other direction, if r Runs (ρ ) is accepting, then ϕ Runs (r Runs (ρ )) = ρ 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 ϕ : TS → TS that is a history-deterministic mapping, but which is neither a morphism, nor locally bijective. Transition system TS, on the left of the figure, is a parity TS (more precisely, a coBüchi TS). Transition system TS , depicted on the right of the figure, is a Muller TS using as acceptance set the Muller language associated to F = {{α}, {α, β}, {α, λ}}; that is, a run in TS is accepting if and only if it eventually avoids either transition e or transition f . The weak morphism we propose is given by: ϕ

(v 0 ) = ϕ(v 1 ) = ϕ(v 2 ) = v , and ϕ(u 1 ) = ϕ(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 ϕ(e 1 ) = ϕ(e 2 ) = e and ϕ(f

1 ) = ϕ(f 2 ) = f .
We remark that ϕ does not preserve rejecting runs. Indeed, a run in TS alternating between v 0 and u 1 , taking transition f 1 infinitely often, is rejecting, but its image is accepting in TS . However, ϕ preserves accepting runs: a run is accepting in TS 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 ϕ avoids transition f in TS , and in the second case, its image avoids transition e .

Finally, we describe a sound resolver simulating ϕ. When simulating a run from TS in TS, we have a choice to make only when we are in state v 0 . If the previous transition in TS was e , we will go up, that is,

v α -→ u is simulated by v 0 1 -→ u 1 and v α -→ v is simulated by v 0 1 -→ v 1 .
If the previous transition in TS was f , we will go down in a symmetric manner. In this way, if transition f is eventually not visited by the run in TS , we ensure to stay in {v 1 , u 1 } in TS (and symmetrically, we ensure to stay in {v 2 , u 2 } if e is avoided in TS ).

v 2 v 0 v 1 u 2 u 1 1 1 1 1 2 2 2 2 e 1 : 2 f 1 : 1 e 2 : 1 f 2 : 2 v ′ u ′ α α e ′ : β f ′ : λ Figure 7
A history-deterministic mapping from a parity TS to a Muller TS with acceptance set given by F = {{α}, {α, β}, {α, λ}}. We use dashed arrows to represent the images of vertices, and colours to represent the image of edges.

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 ϕ : G → G , then G and G have the same winner. In order to show that if Eve wins G then she wins G, we need a method to transfer strategies in G to G. A regular resolver simulating ϕ 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 G in 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 G and G be two games, and ϕ : G → G be a weak morphism between them admitting a resolver (r Init , r) simulating ϕ. Given runs ρ = e 0 e 1 • • • ∈ Run(G ) and ρ = e 0 e 1 • • • ∈ Run(G), we say that ρ is consistent with (r Init , r) over ρ if:

1. Source(e 0 ) = r Init (Source(e 0 ), 2. ϕ(e i ) = e i , and 3. for every finite prefix e 0 e 1 . . . e n-1 ρ ending in a vertex controlled by Eve, the next edge in ρ is e n = r(e 0 . . . e n-1 , e n ).

We remark that there exists at least one run consistent with (r Init , r) over ρ , namely r Runs (ρ ). We say that (r Init , r) is sound for G if it verifies that for any accepting run ρ ∈ Run(G ), all runs consistent with (r Init , r) over ρ are accepting in G.

Said differently, a resolver sound for G is a winning strategy for Duplicator in the following game:

In round 0, Spoiler picks an initial vertex v 0 in G . Duplicator responds by picking an

initial vertex v 0 in G such that ϕ(v 0 ) = v 0 . In round n > 0, Spoiler picks an edge e n in G . If v n-1 is controlled by Adam, Spoiler chooses an edge e n = v n-1 - → v n ∈ Out(v n-1 ) such that ϕ(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 . . . is an accepting run in G from v 0 or e 1 e 2 . . . is not an accepting run in G from v 0 . Spoiler wins otherwise. Definition 3.11. An HD mapping of games ϕ : G → G is called history-deterministic-forgames if it admits a resolver sound for G.

Whenever we apply the term HD-for-games to a map ϕ : TS → TS , it will implicitly imply that TS and TS are games (that is, they have a fixed vertex-labelling l Players : V → {Eve, Adam}), and that ϕ 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 ϕ : TS → TS is a locally surjective morphism, it is also an HD mapping. If TS and TS are games, ϕ is moreover HD-for-games.

Proof. We need to define a sound resolver simulating ϕ. Let r Init : I → I be any function choosing initial vertices satisfying that ϕ • r Init = Id I (which exists by local surjectivity of ϕ). For each v ∈ V and edge e ∈ Out(ϕ(v)) we choose one edge f (v, e ) ∈ Out(v) such that ϕ(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 * × E → E recursively. For the base case, if e 0 ∈ Out(v ), with v ∈ I , we define r(ε, e 0 ) = f (r Init (v ), e 0 ). Suppose that r has been defined for runs of length ≤ n, and let ρ ∈ E * be of length n + 1 and e ∈ E . If ρ is not a run or e / ∈ Out(Target(ϕ(ρ))), we let r(ρ, e ) be any edge in ϕ -1 (e ). If not, let v = Target(ρ) and we define r(ρ, e ) to be the edge f (v, e ).

It is straightforward to check that (r Init , r) is indeed a resolver (for every run ρ ∈ Run(TS ), the sequence r Runs (ρ ) is a run in TS and ρ is its image under ϕ). Finally, since ϕ is a morphism, for every ρ ∈ Run(TS ) and every ρ ∈ Run(TS) consistent with (r Init , r) over ρ , ρ is accepting in TS if and only if ρ = ϕ Runs (ρ) is accepting in TS . We conclude that (r Init , r) is a sound resolver (resp. sound for TS) and therefore ϕ 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 TS and TS be two TS such that there is an HD (resp. HD-for-games) mapping ϕ : TS → TS . For any non-empty subset Ĩ ⊆ I , ϕ is also an HD (resp. HD-forgames) mapping between the transition systems TS r Init ( Ĩ) and TS Ĩ ; that is, the transitions systems obtained by setting r Init ( Ĩ) and Ĩ 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 TS and TS be two TS such that all their states are accessible, and let ϕ : TS → TS be an HD (resp. HD-for-games) mapping between them. If W and W are prefix-independent, the mapping ϕ is also HD (resp. HD-for-games) when considered between the transition systems TS V and TS V , consisting of the transition systems TS and TS where all the states are set to be initial.

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 ϕ : A → A is an HD mapping of automata, then L(A) = L(A ), and if ϕ is locally bijective, A is deterministic (or unambiguous) if andonly if A is (Proposition 3.16) 5 ; and(2) if ϕ : G → G is an HD-for-games mapping, G andG have the same winner (Proposition 3.18 andCorollary 3.19).

Morphisms generalise composition by an automaton

Proposition 3.15. Let A be a complete automaton accepting the language L(A) = W ⊆ Σ ω , and let TS be a (labelled) TS with acceptance set W. Then, there exists a locally surjective weak morphism of (labelled) TS ϕ : TS A → TS that preserves accepting runs. Moreover:

1. If A is deterministic, ϕ can be chosen to be a locally bijective morphism. 2. If A is HD, then ϕ can be chosen to be an HD mapping.

If

A is HD and TS is a game suitable for transformations, then ϕ can be chosen to be an HD-for-games mapping.

Proof. We recall that the set of states of TS A is V × Q and its set of transitions E is a subset of (E × ∆) E, where V and Q (resp. E and ∆) are the states (resp. transitions) of TS and A, respectively. We let W A ⊆ Γ ω be the acceptance set of A. We define ϕ

V (v, q) = v and ϕ E (e 1 , e 2 ) = e 1 for (e 1 , e 2 ) ∈ E × ∆ and ϕ E (e 1 ) = e 1 for e 1 ∈ E. It is immediate to check that ϕ is a weak morphism. Given a run ρ = (v 0 , q 0 ) c0 -→ (v 1 , q 1 ) c1 -→ . . . in TS A, we can consider its projection over TS, ϕ Runs (ρ) = v 0 a0 -→ v 1 a1
-→ . . . . We note that there must exist a unique run in A of the form

ϕ A (ρ) = q 0 a0:c0 ---→ q 1 a1:c1 ---→ . . . .
(Formally, some of the letters a i might equal ε, and in this case q i ai:ci ---→ q i+1 does not appear in the run ϕ A (ρ)).

We show that ϕ preserves accepting runs. Let ρ be an accepting run in TS A. In that case, c 0 c 1 c 2 • • • ∈ W A , and therefore ϕ A (ρ) is an accepting run in A over a 0 a 1 a 2 . . . , so we conclude that a 0 a 1 a 2 • • • ∈ W and ϕ Runs (ρ) is an accepting run in TS.

We prove next the local surjectivity of ϕ. Clearly, ϕ induces a surjection between the initial vertices of TS A (which are

I TS × I A ) and those of TS. Let (v, q) ∈ V × Q and e 1 = v a -→ v ∈ E. If a = ε, the edge e 1 belongs to E and ϕ(e 1 ) = e 1 . If a = ε, since A is complete there is a transition e 2 = q a -→ q ∈ ∆ and ϕ(e 1 , e 2 ) = e 1 ,
so ϕ is locally surjective.

1.

Since A has a single initial state q 0 , ϕ induces a bijection between the initial vertices of TS A (which are I TS × {q 0 }) and those of TS.

Let E col ⊆ E × ∆ and E ε ⊆ E such that E = E col ∪ E ε .
We remark that ϕ| E ε is the identity function (so injective) and that Let a ∈ Σ be the colour of e 1 . Since 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 ϕ is locally injective.

ϕ(E col ) ∩ ϕ(E ε ) = ∅ because ϕ(E col )
Let ρ be a rejecting run in TS A (we use the notations introduced above). In that case, c 0 c 1 c 2 . . . / ∈ W A , and therefore ϕ A (ρ) is a rejecting run over a 0 a 1 a 2 . . . . Since A is deterministic, this is the only run over a 0 a 1 a 2 . . . so we conclude that it does not belong to W. We conclude that ϕ Runs (ρ) is a rejecting run in TS. 2. Let (r 0 , r A ) be a resolver for A. We define a resolver (r Init , r ϕ ) simulating ϕ. First, we let

r Init (v 0 ) = (v 0 , r 0 ) for all v 0 ∈ I TS . We define r ϕ : E * × E → E by induction on the length of the runs. Let e 0 = v 0 a -→ v 1 ∈ Out(v 0 ) be an edge in TS. If e 0 is uncoloured (a = ε), we let r ϕ (ε, e 0 ) = e 0 = (v 0 , r 0 ) ε -→ (v 1 , r 0 ). If not, we let r ϕ (ε, e 0 ) = (e 0 , e a )
, where e a = r(ε, a). Suppose that r ϕ has been defined for sequences of edges of TS A of length < n and let ρ = e 0 e 1 . . . e n-1 ∈ E * be a sequence length n + 1 and e TS = v n an --→ v n+1 be an edge in TS. If ρ is not a run or if it does not end in ϕ -1 (v n ), we let r ϕ (ρ, e TS ) be any edge in ϕ -1 (e TS ). Suppose that ρ is a run ending in ϕ

-1 (v n ). If a n = ε, we define r ϕ (ρ, e TS ) = e TS . As noted before, ρ induces a run ϕ A (ρ) = q 0 a0:c0 ---→ q 1 a1:c1 ---→ . . . - → q n in A.
We let e A = r A (ϕ A (ρ), a n ) be the transition chosen by the resolver of A after this run, and we define r ϕ (ρ, e TS ) = (e TS , e A ). It directly follows from this definition that (r Init , r ϕ ) is indeed a resolver. The proof that if ρ ∈ Run(TS) is an accepting run then r ϕ,Runs (ρ) is accepting follows the same lines than the previous item.

3.

We prove that, if TS is a game suitable for transformations, the resolver (r Init , r ϕ ) defined in the previous item is sound for TS. We claim that if ρ is a run in TS, the only run consistent with (r Init , r ϕ ) over ρ is r ϕ,Runs (ρ). This follows from the fact that if (v, q) is a vertex in TS A controlled by Adam and e ∈ Out(v), then there is a unique e ∈ Out(v, q) such that ϕ(e ) = e. This is indeed the case: as TS is suitable for transformations, if v is an Adam's vertex, every e ∈ Out(v) is uncoloured, so by definition of ϕ we have that ϕ(e ) = e =⇒ e = e. (This can be seen as that ϕ is locally bijective in Adam's vertices).

We conclude that if ρ is an accepting run in TS and ρ is a run consistent with (r Init , r ϕ ) over ρ, then ρ = r ϕ,Runs (ρ), which is accepting by soundness of the resolver (r Init , r ϕ ).

Morphisms witness equivalence of automata

Proposition 3.16. Let A, A be two automata over the same input alphabet such that there is an HD mapping of automata ϕ :

A → A . Then, L(A) = L(A ),

and A is HD if and only if A is HD. If ϕ is moreover locally bijective and surjective, A is deterministic (resp. complete) if and only if A is.

Proof. Since ϕ preserves accepting runs, it is clear that L(A) ⊆ L(A ). Since ϕ admits a sound resolver (r Init , r), if ρ is an accepting run over w ∈ Σ ω in A , then r Runs (ρ) is an accepting run over w in A, so L(A ) ⊆ L(A).

Let (r Init , r ϕ ) be a sound resolver simulating ϕ. Suppose that A is HD, admitting a resolver (r 0 , r). A resolver (r 0 , r ) for A can be obtained just by composing r ϕ and ϕ, that is: r 0 = ϕ(r 0 ) and for ρ ∈ Run fin (A ) and a ∈ Σ, r (ρ , a) = ϕ(r(r ϕ,Runs (ρ ), a))). That is, given a run ρ in A , we simulate it in A using r ϕ , 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 A using ϕ. Suppose now that A is HD and that (r 0 , r ) is a resolver for it.

We define a resolver (r 0 , r) for A. We let r 0 = r Init (r 0 ), and for ρ ∈ Run fin (A) and a ∈ Σ, r(ρ, a) = r ϕ ((ϕ Runs (ρ), r(ϕ Runs (ρ), a)). That is, given a run ρ in A, we simulate it in A using ϕ, 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 A using r ϕ . It is a direct check that the resolvers defined this way witness that A and A, respectively, are HD.

The proof that A is deterministic (resp. complete) if and only if A is deterministic (resp. complete), assuming surjectivity and local bijectivity of ϕ, 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 ∈ Σ ω 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 ϕ : A → A is a locally bijective morphism then A is (strongly) unambiguous if and only if A is.

Morphisms preserve winning regions of games

Lemma 3.17. Let G, G be two games, such that there is a weak morphism of games ϕ : G → G that is locally surjective and preserves accepting runs. If Eve wins the game G from an initial vertex v, then she wins G from ϕ(v).

Proof. Let v = ϕ(v), and let strat v : Path fin v (G) → E be a strategy from v for Eve in G. Intuitively, we will define a strategy in G as follows: for each finite run ρ from v in G , we pick a preimage ρ ∈ ϕ -1 (ρ ) in G, look at the decision made by strat v at the end of ρ and transfer it back to G via ϕ. 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 choice st : Path fin v (G ) → Path fin v (G) satisfying that for any ρ = e 0 e 1 . . . e n-1 e n ∈ Path fin v (G ):

The run choice st (ρ ) has length n + 1. ϕ Runs (choice st (ρ )) = ρ . Monotonicity: if ρ ρ then choice st (ρ ) choice st (ρ ). If there exists e n ∈ ϕ -1 (e n ) such that choice st (e 0 e 1 . . . e n-1 )e n is consistent with strat v , then choice st (ρ ) is consistent with strat v .

Assume for now that such a function exists, and define a strategy in G as

strat v (ρ ) = ϕ(strat v (choice st (ρ ))), for ρ ∈ Path fin v (G ).
We prove that strat v is winning. Let ρ = e 0 e 1 • • • ∈ Run(G ) be an infinite play consistent with strat v . For each finite prefix ρ ρ , choice st ( ρ ) is a finite play in G, and by the monotonicity assumption, we can define the limit of these runs as:

ρ = e 0 e 1 e 2 • • • ∈ Run(G)
, where e 0 e 1 . . . e n = choice st (e 0 e 1 . . . e n ), which is indeed a run in G. We show that ρ is consistent with strat v by induction. Let ρ n = e 0 e 1 . . . e n-1 be the prefix of size n of ρ, and suppose that it ends in a vertex v n controlled by Eve. We want to show that e n = strat v (ρ n ). By definition of strat v , e n = ϕ(strat v (ρ n )) = ϕ(e n ), and as v n is controlled by Eve, strat v (ρ n ) is the only continuation of ρ n consistent with strat v , so by the last property of choice st , e n has to coincide with strat v (ρ n ), as we wanted. As ρ is consistent with the winning strategy strat v , it is an accepting run in G, and since ϕ preserves accepting runs, ρ = ϕ Runs ( ρ) is also an accepting run.

Finally, we show how to build a function choice st : Path fin v (G ) → Path fin v (G) by induction on the length of the runs. Suppose that choice st has been defined for runs of length ≤ n, and let e 0 e 1 . . . e n be a run of length n + 1, with choice st (e 0 e 1 . . . e n-1 ) = e 0 e 1 . . . e n-1 . If e 0 e 1 . . . e n-1 is not consistent with strat v , it ends in a vertex v n controlled by Adam, or strat v (e 0 e 1 . . . e n-1 ) / ∈ ϕ -1 (e n ), we let e n ∈ ϕ -1 (e n ) ∩ Out(v n ) be any edge (one such edge exists by local surjectivity). On the contrary, we let e n = strat v (e 0 e 1 . . . e n-1 ). We define choice st (e 0 e 1 . . . e n-1 e n ) = e 0 e 1 . . . 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 ϕ : G → G . Eve's winning region in G is the projection of her winning region in G:

W Eve (G ) = ϕ(W Eve (G)).
Proof. If Eve wins G from an initial vertex v, Lemma 3.17 guarantees that she wins G from ϕ(v).

Suppose now that Eve wins G from an initial vertex v with a strategy strat v : Path fin v (G ) → E . We need to show that she wins G from some initial vertex in ϕ -1 (v ). Let (r Init , r) be a resolver simulating ϕ sound for G and let v = r Init (v ). We define

strat v (ρ) = r(ρ, strat v (ϕ Runs (ρ)), for ρ ∈ Path fin v (G).
That is, strat v is a strategy in G from v that, given a finite run ρ, simulates ρ 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 v is winning for Eve in G. Let ρ = e 0 e 1 • • • ∈ Path v (G) be a play consistent with strat v . We claim that ϕ(ρ) is consistent with strat v and that ρ is consistent with (r Init , r) over ϕ(ρ). This implies the desired result; consistency with strat v implies that ϕ(ρ) is accepting, and since (r Init , r) is sound for G, ρ would be accepting in G.

We prove that ϕ(ρ) is consistent with strat v . Let e 0 e 1 . . . e n-1 be a subplay of ϕ(ρ) ending in a vertex v n controlled by Eve. By definition of the strategy strat v , we have that e n = r(e 0 . . . e n-1 , strat v (e 0 . . . e n-1 )), and by definition of a resolver (item 2), e n = ϕ(e n ) = strat v (e 0 . . . e n-1 )), as we wanted.

The fact that ρ is consistent with (r Init , r) over ϕ(ρ) follows directly from the definition of strat v .

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 ϕ : G → G , then Eve's full winning region in G is the projection of her full winning region in

G: W Eve (G V ) = ϕ(W Eve (G V )).

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 parity Z F for a given Muller language Muller(F). Theorem 4.13, the main contribution of this section, states the minimality of A parity Z F both amongst deterministic and HD parity automata. Theorem 4.12 states the optimality on the number of colours of the acceptance condition of A parity Z F , 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 parity Z F 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 Rabin Z F for a Muller language Muller(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 [START_REF] Piterman | Temporal logic and fair discrete systems[END_REF].

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 [START_REF] Boker | History determinism vs. good for gameness in quantitative automata[END_REF]Section 4]. A summary of the minimal automata recognising Muller languages appears in Table 1.

Type of automata Deterministic

Historydeterministic

Parity

A parity

Z F A parity Z F Rabin NP-complete A Rabin Z F
Table 1 Minimal automata recognising a Muller language Muller(F), according to the type of acceptance condition (parity or Rabin) and the form of determinism.

The Zielonka tree

Definition 4.1 ([81]). Let F ⊆ 2 Σ + be a family of non-empty subsets over a finite set Σ. A Zielonka tree for F (over Σ) 6 , denoted Z F = (N, , ν : N → 2 Σ + ) is a 2 Σ + -labelled tree with nodes partitioned into round nodes and square nodes, N = N N , such that:

The root is labelled Σ. If a node is labelled X ⊆ Σ, with X ∈ F, then it is a round node, and it has a child for each maximal non-empty subset Y ⊆ X such that Y ∈ F, which is labelled Y . If a node is labelled X ⊆ Σ, with X ∈ F, then it is a square node, and it has a child for each maximal non-empty subset Y ⊆ X such that Y ∈ F, which is labelled Y .

Remark 4.2. We note that for each family of subsets F ⊆ 2 Σ + , there is only one Zielonka tree up to renaming of its nodes, so we will talk of the Zielonka tree of F. Remark 4.3. We remark that if n is a node of Z F , then the subtree of Z F rooted at n is the Zielonka tree for the family F| ν(n) over the alphabet ν(n), that is, for the restriction of F to the subsets included in the label of n. Remark 4.4. Let n be a node of Z F and let n 1 be a child of it.

If ν(n 1 ) X ⊆ ν(n), then ν(n 1 ) ∈ F ⇐⇒ X / ∈ F ⇐⇒ ν(n) / ∈ F. In particular, if n 1 , n 2 are two different children of n, then ν(n 1 ) ∈ F ⇐⇒ ν(n 2 ) ∈ F ⇐⇒ ν(n 1 ) ∪ ν(n 2 ) / ∈ F.
We equip Zielonka trees with an order to navigate in them. That is, we equip each set Children Z F (n) with a total order, making 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 ∈ Leaves(Z F ) and a letter a ∈ Σ we define Supp(l, a) = n to be the deepest ancestor of l (maximal for ) such that a ∈ ν(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 Σ = {a, b, c} and let F be:

F = {{a, b}, {a, c}, {b}}.
In Figure 8 we show the Zielonka tree of 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 Supp(ξ, c) = λ and Supp(ξ, b) = α . Also, Jump(ξ, λ) = ζ is the leaf reached by going from ξ to λ, then changing to the next branch (in a cyclic way) and re-descend by taking the leftmost path. Similarly, Jump(ξ, α) = θ.

The subtree rooted at λ contains the nodes {λ, ξ, ζ}. We note that this is the Zielonka tree of F| {a,c} = {{a, c}} (over the alphabet {a, c}).

A minimal deterministic parity automaton

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

The Zielonka-tree-parity-automaton

We associate a non-negative integer to each level of a Zielonka tree Z F = (N, , ν). We let p Z : N → N be the function defined as:

if Σ ∈ F, p Z (n) = Depth(n), if Σ / ∈ F, p Z (n) = Depth(n) + 1.
We let min F (resp. max F ) be the minimum (resp. maximum) value taken by the function p Z .

(α) = 1, p Z (β) = p Z (λ) = 2 and p Z (θ) = p Z (ξ) = p Z (ζ) = 3, so min F = 1 and max F = 3.
Definition 4.8 (Zielonka-tree-parity-automaton). Given a family of non-empty subsets F ⊆ 2 Σ + , we define the ZT-parity-automaton A parity

Z F = (Q, Σ, q 0 , [min F , max F ],
δ, parity) as the deterministic parity automaton given by:

Q = Leaves(Z F ), q 0 is the leftmost leaf of Z F 7 ,
The transition reading a ∈ Σ from q ∈ Q goes to Jump(q, Supp(q, a)) and produces p Z (Supp(q, a)) as output, that is, δ(q, a) = (Jump(q, Supp(q, a)), p Z (Supp(q, a))) .

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 A parity Z F of the family of subsets from Example 4.5.

Correctness of the Zielonka-tree-parity-automaton

Proposition 4.10 (Correctness). Let F ⊆ 2 Σ + be a family of non-empty subsets. Then,

L(A parity Z F ) = Muller Σ (F).
That is, a word w ∈ Σ ω is accepted by A parity

Z F if and only if Inf(w) ∈ F.
The following useful lemma follows directly from the definition of Supp and Jump.

Lemma 4.11. Let q be a leaf of Z F and let n be a node above q. Then, Supp(q, a) is a descendant of n if and only if a ∈ ν(n), and in this case, Jump(q, Supp(q, a)) is a descendant of n too.

Proof of Proposition 4.10. Let w = w 0 w 1 w 2 • • • ∈ Σ ω be an infinite word. For i > 0, let q i be the leaf of Z F reached after the (only) run over w 0 w 1 . . . w i-1 in A parity Z F . For i ≥ 0 let n i = 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 ) = γ(q i , w i ) ∈ [min F , max F ] be that output colour (the output of the run over w being therefore c 0 c 1 c 2 • • • ∈ N ω ). Let q ∞ be a node appearing infinitely often in the sequence q 0 q 1 q 2 . . . , and let n w be the deepest ancestor of q ∞ such that Inf(w) ⊆ ν(n w ).

Claim 4.10.1. There is K ∈ N such that for all i ≥ K, q i n w and Supp(q i , w i ) n w . In particular, c i ≥ p Z (n w ) for i ≥ K.

Proof. Let K ∈ N be a position such that w i ∈ Inf(w) for all i ≥ K and q K = q ∞ . The claim follows from Lemma 4.11 and induction.

Claim 4.10.2. Let n w,1 , . . . , n w,s be an enumeration of Children Z F (n w ) from left to right. It is verified that:

1. 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 ∈ Children(n w ) such that Inf(w) ⊆ ν(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 Supp(q i , w i ) n w,k , and by Lemma 4.11, Inf(w) ⊆ ν(n w,k ). In particular, q ∞ is below n w,k , contradicting the fact that n w is the deepest ancestor of q ∞ containing Inf(w).

Let K be like in the Claim 4.10.1. We show that if i ≥ K and q i n w,k , then there is j > i such that w j / ∈ ν(n w,k ), Supp(q j , w j ) = n w and q j+1 n w,k+1 (by an abuse of notation we let s + 1 = 1). It suffices to consider the least j ≥ i such that Supp(q j , w j ) n w,k (which exists by the previous remark). Since Inf(w) ⊆ ν(n w ) we have that Supp(q j , w j ) = n w , so w j / ∈ ν(n w,j ) (by Lemma 4.11) and by definition of the transitions of A parity Z F , q j+1 will be a leaf below n w,k+1 .

The fact that q j+1 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 / ∈ ν(n w,j ) and 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 ν(n w ) ∈ F). It remains to show that Inf(w) ∈ F if and only if ν(n w ) ∈ F, which holds by the second item in Claim 4.10.2 and Remark 4.4.

Optimality of the Zielonka-tree-parity-automaton

We now state and prove the main results of this section: the optimality of the ZT-parityautomaton 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 A be a history-deterministic parity automaton recognising a Muller language Muller Σ (F). Then, |A parity Z F | ≤ |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 A is determinisable by prunning if there is a subset ∆ ⊆ ∆ of its transitions and an initial state q 0 such that the subautomaton induced by ∆ with initial state q 0 is deterministic and recognises L(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 = Muller Σ (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 A L with just one state q, transitions q a:a --→ q for each a ∈ Σ, and acceptance condition given by L itself. Let n 1 n 2 . . . n d be a branch of maximal length of 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 i be the cycle in A L containing exactly the transitions corresponding to letters in ν(n i ), we obtain that 1 2

• • •

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.

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. 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 A = (Q, Σ, I, Γ, ∆, W) be an automaton, and let X ⊆ Σ be a subset of the input alphabet. We say that a subgraph S of the underlying graph of A is X-closed if for every state q in S and every letter a ∈ X there is some transition q a:c --→ q in S. An X-final strongly connected component (X-FSCC) of A is an X-closed final SCC in the graph obtained by taking the restriction of the underlying graph of A to the edges labelled by letters in X. We remark that a subset S ⊆ Q is the set of states of an X-FSCC if and only if:

for any two states q, q ∈ S there is a finite word w ∈ X * labelling a finite path from q to q , and if q ∈ S and there is a finite path from q to q labelled with a word w ∈ X * , then q ∈ S. Lemma 4.17. Let A be a complete automaton. For every subset X ⊆ Σ, A contains an accessible X-FSCC.

Proof. As any graph without sinks contains some final SCC, the accessible part of the restriction of A to edges labelled by letters in X contains one. By completeness of A, one such final SCC has to be an X-closed subgraph, so it is an X-FSCC. Lemma 4.18. Let A be a DMA recognising a Muller language Muller Σ (F), let X ⊆ Σ and let S X be an accessible X-FSCC of A. Then, the automaton induced by S X is a deterministic automaton recognising

Muller X (F| X ) = {w ∈ X ω | Inf(w) ∈ F}.
Proof. Let A = (Q, Σ, q 0 , Γ, δ, W) (where W is a Muller language). Let q S be the state in S X chosen to be initial, and let u 0 ∈ Σ * 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 ∈ X ω belongs to Muller Σ (F) if and only if u 0 w ∈ Muller Σ (F), and therefore, A accepts w if and only if it accepts u 0 w. Since the run in A over u 0 w and the run in S X over w have a suffix in common, and by prefix-independence of W, we have that w ∈ L(S X ) if and only if u 0 w ∈ L(A) if and only if Inf(w) ∈ 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 A be a parity automaton. Let 1 , 2 ∈ Cycles(A) be two cycles with some state in common. If 1 and 2 are both accepting (resp. rejecting), then 1 ∪ 2 is also accepting (resp. rejecting).

Proof. Let γ : ∆ → N be the colouring function of A. The cycles 1 and 2 are accepting if and only if

d i = min γ( i ) is even, for i = 1, 2. In this case, min γ( 1 ∪ 2 ) = min{d 1 , d 2 } is even. The proof is symmetric if 1 and 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 ∩ S 2 = ∅, if their sets of states are disjoint. Proof. Without loss of generality, we can suppose that all states in A are accessible, and since the language that A recognises is prefix-independent, we can also suppose that A is complete. Let l Σ : ∆ → Σ be the labelling of the transitions of A with input letters. Let S i be a ν(n i )-FSCC in A, for i = 1, 2, and let i be its set of edges, which form a cycle satisfying l Σ ( i ) = ν(n i ). Suppose by contradiction that S 1 ∩ S 2 = ∅. Then 1 and 2 have some state in common, and their union is also a cycle satisfying l Σ ( 1 ∪ 2 ) = ν(n 1 ) ∪ ν(n 2 ). By Lemma 4.19, we must have

1 accepting ⇐⇒ 1 ∪ 2 accepting, contradicting the fact that ν(n 1 ) ∈ F if and only if ν(n 1 ) ∪ ν(n 2 ) / ∈ F (Remark 4.4).
Proof of Theorem 4.16. We proceed by induction in the height of Z F . For height 1, the result is trivial, since |A parity

Z F | = 1.
Let A be a DPA recognising Muller Σ (F). Let n 0 be the root of Z F and n 1 , n 2 , . . . , n k be an enumeration of the children of n 0 in Z F . By Lemma 4.17, for each i ∈ {1, . . . , k}, A contains some accessible ν(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 Muller ν(ni) (F| ν(ni) ). Let Z i by the subtree of Z F rooted at n i , which we recall that is the Zielonka tree for F| ν(ni) . By induction hypothesis, it must be the case that |Leaves(Z i )| ≤ |S i |, so we can conclude:

|A parity Z F | = |Leaves(Z F )| = k i=1 |Leaves(Z i )| ≤ k i=1 |S i | ≤ |A|.

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

We intend to prove Theorem 4.13, that is, that for any F ⊆ 2 Σ + , the automaton A parity Z F is minimal amongst HD parity automata recognising Muller(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 A is an HD parity automaton for Muller(F) and that n 0 is the root of Z F having n 1 , . . . , n k as children. For each child n i we want to find an HD subautomaton A i recognising the language associated to F| ν(ni) in such a way that the automata A i are pairwise disjoint, which would allow us to carry out the induction and obtain that |A| ≥ |Leaves(Z F )| = |A parity Z F |. Our objective will be therefore to prove: Proposition 4.21. Let n 0 be the root of the Zielonka tree of F, and let n 1 , n 2 , . . . , n k be an enumeration of the children of n 0 . If A is an HD automaton recognising Muller Σ (F), then, A contains k pairwise disjoint subautomata A 1 , . . . , A k that are history-deterministic and such that L(A i ) = Muller ν(ni) (F| ν(ni) ).

The non-determinism of 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 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 (Σ ∈ F) or square (Σ / ∈ 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: Σ / ∈ F. Let A = (Q, Σ, q 0 , Γ, ∆, W) be a non-deterministic automaton. A memory structure for A is a memory skeleton M over ∆ together with a function σ : Q × M × Σ → ∆, where M is the set of states of M. We say that (M, σ) implements a resolver (q 0 , r) if for all a ∈ Σ, r(ε, a) = σ(q 0 , m 0 , a) and for all ρ ∈ ∆ + , r(ρ, a) = σ(Target(ρ), µ(m 0 , ρ), a), where m 0 is the initial state of M and µ : M × ∆ * → M is its update function.

Lemma 4.22 ([7]). Every HD parity automaton admits a sound resolver implemented by a finite memory structure.

As M is a pointed graph labelled with the transitions of A, we could consider the product automaton A M. We want to furthermore restrict the transitions of this automaton to those that are indicated by the next-move function σ. Given an automaton A and a memory structure (M, σ), we define their composition, which we write A σ M = (Q × M, Σ, (q 0 , m 0 ), Γ, ∆ , W) as the automaton having transitions (q, m) a:c --→ (q , m ) if σ(q, m, a) = e = q a:c --→ q and µ(m, e) = m (formally, ∆ is a subset of ∆ × E M , where E M are the edges of the memory skeleton). We note that A σ M is deterministic, and it is complete if 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. For the rest of the paragraph, we let A = (Q, Σ, q 0 , N, ∆, parity) be a complete historydeterministic automaton recognising the Muller language Muller F (Σ) admitting a sound resolver (q 0 , r) implemented by a memory structure (M, σ). We let π A : A σ M → A be the morphism of automata given by the projection into the first component:

π A,V (q, m) = q and π A,E (e 1 , e 2 ) = e 1 . Remark 4.24. If ρ is a path in A σ M that is labelled by input letters a 0 a 1 • • • ∈ Σ ∞ and producing output c 0 c 1 • • • ∈ N ∞ , then the π A -projection of ρ is a path in A labelled by a 0 a 1 • • • ∈ Σ ∞ and producing c 0 c 1 • • • ∈ N ∞ as output.
Lemma 4.25. Let X ⊆ Σ and let S X be an accessible X-FSCC of A σ M. Then, π A (S X ) induces an HD subautomaton of A recognising Muller X (F| X ) = {w ∈ X ω | Inf(w) ∈ F}.

Proof. Let q S be a state in π A (S X ) chosen to be initial. Let m S be a state in M such that (q S , m S ) ∈ S X . By Lemma 4.18, S X induces a deterministic subautomaton with initial state (q S , m S ) recognising Muller X (F| X ). On the one hand, since π A (S X ) is an accessible subautomaton of A having only transitions labelled by X and by prefix-independence of L(A), we have that

L(π A (S X )) ⊆ L(A) ∩ X ω = Muller X (F X ).
On the other hand, the projection of any accepting run in S X provides an accepting run in π A (S X ) (by Remark 4.24), so

L(S X ) = Muller X (F X ) ⊆ L(π A (S X )).
Moreover, a sound resolver for π A (S X ) is implemented by (M m S , σ) (the memory structure with initial state set to m S ).

(n 2 )-FSCC in A σ M, respectively, then π A (S 1 ) ∩ π A (S 2 ) = ∅.
Proof. Suppose by contradiction that there is some state q in π A (S 1 ) ∩ π A (S 2 ), and let m 1 , m 2 ∈ 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 i ∈ Cycles (q,mi) (A σ M) be the cycle over (q, m i ) containing all edges in S i . We note that l Σ ( i ) = ν(n i ) and therefore min γ( i ) has to be even (as A σ M is deterministic), where l Σ and γ are the labellings of A σ M with input letters and output colours, respectively. By Remark 4.24, the π A -projections of 1 and 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 ∈ Σ ω with Inf(w) = ν(n 1 ) ∪ ν(n 2 ), contradicting the fact that ν(n 1 ) ∪ ν(n 2 ) / ∈ 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: Σ ∈ 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 Σ ∈ F. Indeed, even if we can find two rejecting cycles 1 , 2 such that 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 ) ∪ ν(n 2 ) ∈ 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 [START_REF] Boker | When a little nondeterminism goes a long way: An introduction to history-determinism[END_REF], 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 [START_REF] Piterman | Temporal logic and fair discrete systems[END_REF].

Let A = (Q, Σ, q 0 , [d min , d max ], ∆, parity) be a parity automaton recognising Muller(F), and suppose that Σ ∩ [d min , d max ] = ∅. The letter game for A is the game G A defined as follows:

The set of vertices is V = Q (Q × Σ). Adam controls vertices in Q, and Eve controls vertices in Q × Σ. For each letter a ∈ Σ and each q ∈ Q, there is an edge q a -→ (q, a). For each position (q, a) ∈ Q × Σ, and for each transition q a:c --→ q in A, there is an edge (q, a) c -→ q . The set of colours is Γ = Σ [d min , d max ], and the acceptance set is the Muller language associated to

F → parity = {C ⊆ Γ | [C ∩ Σ ∈ F] =⇒ [min(C ∩ [d min , d max ]) 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 aut A : G A A that sends states of the form q ∈ Q to q and edges of the form (q, a) c -→ q to q 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. Remark 4.28. If two subsets of vertices of the letter game

q 0 q 1 q 2 q 0 , a q 0 , b q 1 , a q 0 , c q 1 , b q 1 , c q 2 , a q 2 , b q 2 , c
S 1 , S 2 ⊆ V are disjoint, then aut A (S 1 ) ∩ aut A (S 2 ) = ∅. Remark 4.29. If ρ is a play in G A , labelled a 0 c 0 a 1 c 1 • • • ∈ (Σ • [d min , d max ]) ∞ , the aut A - projection of ρ is a run in A over a 0 a 1 • • • ∈ Σ ∞ producing c 0 c 1 • • • ∈ [d min , d max ] ∞ as output.
Lemma 4.30 ([38]). A parity automaton A is HD if and only if Eve wins the letter game from some initial state of A.

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

Attr G (X) = {v ∈ V | there is a strategy for Eve ensuring to eventually visit X from v}.

For a colour c ∈ Γ we note Attr G (c) = Attr G (E c ), where E c is the set of edges coloured c.

For the rest of the paragraph, let A = (Q, Σ, q 0 , [0, d], ∆, parity) be a complete historydeterministic parity automaton recognising Muller(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 Γ = Σ [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 Γ to [0, d]. From the prefix-independence of Muller(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 F (supposed to be round, that is ν(n 0 ) ∈ F), let n 1 , . . . , n k be its children, and let

Σ i = ν(n i ) ⊆ Σ (note that Σ i / ∈ F for i ≥ 1
). Let us examine the condition F → 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 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 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 Σ i . We use this idea to define next attractor decompositions for G A .

Given a subset of vertices V ⊆ V we write G A (V ) to denote the subgame of G A containing the vertices of V and the edges between them.

Σ ∪ [0, d] Σ ∪ [1, d] Σ ∪ [2, d] Σ 1 ∪ [1, d] • • • Σ k ∪ [1, d]
. . . . . . . . .

Figure 11

First levels of the Zielonka tree of the Muller condition F → parity, which is the winning condition of the letter game GA.

Let x be an even integer. For a subgame G = G A (V ) of G A with no colour strictly smaller than x, we define an x-attractor decomposition of G as a partition of V into

V = Attr G (x) V 1 A 1 • • • V l A l , satisfying: Attr G (x) is Eve's attractor to x in G .
For each V j , either (1) there is some i ∈ {1, . . . , k} such that no colour of Σ \ Σ i appears in G A (V j ), or (2) Eve has a winning strategy for 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 a -→ v (v ∈ V j , v / ∈ V j ), then v ∈ Attr G (x) V 1 A 1 . . . V j-1 A j-1 .
In case (1) we say that V j is a Σ i -region of the attractor decomposition and in case ( 2) that V j is an x + 1-avoiding region. Eve wins G A (V j ) from every vertex for all j. A j = Attr Gj (V j ), where G j is the subgame induced by the subset of vertices given by V \ (Attr G (x) V 1 . . . V j-1 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 G j be the subgame obtained from G A (V j ) by removing the transitions labelled x + 1.

An x-recursive attractor decomposition of G is:

D G = Attr G (x), (V 1 , A 1 , D G 1 ), (V 2 , A 2 , D G 2 ), . . . , (V l , A l , D G l ) ,
where

Attr G (x) V 1 A 1 • • • V l A l is an x-attractor decomposition of G , and, if V j is an x + 1-avoiding region, then D G j is an x + 2-recursive attractor decomposition of G j . (If V j is an Σ i -region, D G j can be disregarded).
A representation of an attractor decomposition appears in Figure 12.

We say that a subgame S of G is a Σ i -region of D G if it is a Σ 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 D G if it is a y-avoiding region of some of the recursively defined attractor decompositions. We say that the full game 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 G there is one and only one minimal y-avoiding region of D G containing S (note that y might equal -1).

Remark 4.31. A 0-recursive attractor decomposition D G A of G A induces a partition of the vertices into

V = S 1 • • • S r A 1 . . . A r B 1 • • • B s , Region Region

1-avoiding region

Region Region

Region Region

Figure 12 On the left, a 0-attractor decomposition of a game G. On the right, the coloured part represents a 2-attractor decomposition of the subgame G 2 induced by the 1-avoiding region V2. Since no 3-avoiding region appears on it, this is a full attractor decomposition of the game G, inducing a partition into three different kinds of regions. The order over the Σi-regions is given by V1 <D V2,1 <D V2,2 <D V3. 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.

such that: S j is a Σ i -region of D G A , for some i ∈ {1, . . . , k}, A j = Attr Gj (S j ) for some subgame G j appearing at some level of the decomposition, B j = Attr G j (x) for some even integer x and some x -1-avoiding region G j appearing at some level of the decomposition.

Moreover, such a decomposition induces a total order over the Σ 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 G A such that j < j , S t ⊆ V j and S t ⊆ V k .

We call such a partition a full attractor decomposition of G A . We remark that, by definition of an attractor decomposition, Eve wins G A (S j ) from every vertex for every S j . See Figure 12 for an illustration.

The proof that G A admits a full attractor decomposition uses the ideas appearing in [START_REF] Piterman | Temporal logic and fair discrete systems[END_REF]Section 3]. Lemma 4.32. Let x be an even integer. If G is a subgame of 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, G A admits a full attractor decomposition.

Proof. We suppose without loss of generality that x = 0. Suppose that V 1 , A 1 , . . . V j-1 , A j-1 have already been defined and that they verify the desired properties. Suppose that the game 1) is non-empty. First, note that Eve wins G j from any position. Indeed, Eve wins G from any vertex v in G j (as we suppose that she can win G starting anywhere); moreover, since v / ∈ A j for any j < j, Adam has a strategy from v to force to remain in G j , and Eve has to be able to win against any such strategy.

G j with vertices V \ (Attr G (0) V 1 . . . V j-1 A j-
We prove that either (1) there is some i ∈ {1, . . . , k} and v vertex in G j such that Eve has a winning strategy from v forcing to produce no colour in Σ \ Σ i , or (2) there is some vertex v in 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 Σ 1 , followed by a color not in Σ 2 , and continues this pattern until a color not in Σ 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(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 Σ \ Σ i . We let V j be the set of such vertices, and for each of them we fix a strategy strat v that is winning in G j and avoids colours in Σ \ Σ i . By definition of V j , if ρ = v v is a finite play consistent with strat v in G j , then v ∈ V j (Eve can still win without producing colours in Σ \ Σ i ), so Adam cannot force to leave V j . This proves that:

1. strat v is winning in G A (V j ) from v, 2. if v ∈ V j is controlled by Adam and v - → v is an edge in G A , then v ∈ Attr G (0) V 1 A 1 . . . V j-1 A j-1 V j . Also, if a vertex v controlled by Adam is in V j , no edge v a / ∈Σi ---→ v appears in G j , so no colour of Σ \ Σ 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 (M, σ) over G implementing a winning strategy uniformly, that is, for every vertex v of G there is a memory state m v in M such that the memory structure (M mv , σ) implements a winning strategy from v.

For the rest of the paragraph, we fix a 0-recursive attractor decomposition D G A for G A and let S 1 < D S 2 . . . < D S r be the Σ i -regions of the induced full attractor decomposition. For each region S j we fix a memory structure (M j , σ 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 ) σj M j consisting of the product game in which the choices for Eve are restricted to those of the form (v, m)

c - → (v , m ) if σ j (v, m) = e = v c - → v and µ j (m, e) = m
. By definition, Eve does not have any choice in G A (S j ) σj M j , and since (M j , σ j ) implements a winning strategy, any infinite path in G A (S j ) σj M j produces a set of colours in F → parity. We let π G : G A (S j ) σj M j → G A (S j ) be the projection into G A (S j ).

A subgraph G j of G A (S j ) σj M j is X-closed, for a subset X ⊆ Σ, if for every vertex (q, m) controlled by Adam and every a ∈ X there is a transition (q, m) a -→ ((q, a), m ) in G j (that is, q a -→ (q, a) ∈ 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 ) σj M j to the graph where Adam's choices are restricted to letters in X. We say that a subgraph G of G A is an X-closed subgame (with respect to the attractor decomposition D G A and a family of finite memory strategies) if G = π G (G j ) for G j some X-closed SCC of some product G A (S j ) σj 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 , σ 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 ⊆ Σ, and let G X ⊆ G A be an X-closed subgame of G A . The subautomaton of A induced by aut A (G X ) is HD and recognises Muller X (F| X ). Lemma 4.36. If a product G A (S j ) σj M j does not contain any X-closed subgraph, for X ⊆ Σ, 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) (q , m ) in G A (S j ) σj M j producing exclusively letters in X such that, for some a ∈ X, the edge q 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 ) σ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 Σ i of the children of the root of Z

F , G A admits some Σ i -closed subgame contained in a Σ 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 • • • S r A 1 . . . A r B 1 • • • B s ,
We fix the following strategy strat for Eve in the letter game:

whenever the play lands to B j , where B j = 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 , σ j ). More precisely, let m v be the state of M j such that (M j,v , σ 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 , σ j ).

Claim 4.37.1. Let ρ be a play consistent with strat (from any vertex), and let y ≥ -1 be the maximal odd number such that Inf(ρ) is contained in a y-avoiding region S of D G A . Then, either ρ eventually stays in a Σ i -region S j contained in S, or the minimal colour produced infinitely often by ρ is y + 1.

Proof. Let Attr S (y + 1) V 1 A 1 . . . . . . , V l 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 ∈ Attr S (y + 1)

V 1 A 1 . . . V j-1 A j-1 . First, if V j is a y + 2-
avoiding region, ρ cannot stay in it (by maximality of y). Thus, if ρ does not eventually stay in a Σ 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 Σ i -region S j , it has to be winning since the strategy implemented by (M j , σ j ) is winning in there.

We remark that we can extract a Σ i -FSCC from any Σ i -closed subgraph of G A (S j ) σj M j , that will be contained in the Σ i -region S j , so it suffices to prove the existence of such Σ i -closed subgraphs. We also recall that in G A (S j ) σ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 Σ 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 ∈ Σ ω such that Inf(w) = Σ 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 Σ 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 A, obtaining an accepting run over w. This is a contradiction, since w / ∈ Muller(F) = L(A) (because Σ i / ∈ F). We conclude that some G A (S j ) σj M j admits a Σ i -FSCC, and therefore G A admits some Σ i -closed subgame.

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

A minimal history-deterministic Rabin automaton

In this section, we present the construction of a history-deterministic Rabin automaton A Rabin Z F for a Muller language Muller(F) using the Zielonka tree Z F , and prove its minimality (Theorem 4.48). The automaton A Rabin Z F can be seen as a quotient of the ZT-parity-automaton; that is, A Rabin Z F is obtained by merging some of the states of A parity Z F . Thus, we replace the complexity in the number of states by complexity in the acceptance condition. The size of the automaton A Rabin Z F is a well-studied parameter of Zielonka trees: its round-branching width, rbw(Z F ). This parameter was introduced by Dziembowski, Jurdziński and Walukiewicz [START_REF] Piterman | Temporal logic and fair discrete systems[END_REF] (under the name of memory of Z F ) and shown to coincide with the memory required by Eve to win in games using Muller(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 [START_REF] Piterman | Temporal logic and fair discrete systems[END_REF] to obtain the minimality of A Rabin Z F . 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).

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 , . . . , 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 rbw(T ) as:

rbw(T ) =            1 if T has exactly one node, max{rbw(T 1 ), . . . , rbw(T k )} if the root is square, k i=1 rbw(T i ) if the root is round.
Next lemma directly follows from the definition of rbw(T ).

Lemma 4.39. Let T = (N = N N , ) be a tree with nodes partitioned into round and square nodes. There exists a mapping η : Leaves(T ) → {1, 2, . . . , rbw(T )} satisfying:

If n ∈ N is a round node with children n 1 = n 2 , for any pair of leaves l 1 and l 2 below n 1 and n 2 , respectively, η(l 1 ) = η(l 2 ).

( ) Example 4.40. Let F = {{a, b}, {a, c}, {b}} be the family of subsets considered in Example 4.5. The round-branching width of Z F is rbw(Z F ) = 2. A labelling η : Leaves(Z F ) → {1, 2} satisfying Property is given by η(θ) = η(ξ) = 1 and η(ζ) = 2. This labelling is represented in the Zielonka tree Z F on the left of Figure 13. Definition 4.41 (Zielonka-tree-HD-Rabin-automaton). Let F ⊆ 2 Σ + , Z F = (N = N N , ) its Zielonka tree and η : Leaves(Z F ) → {1, 2, . . . , rbw(Z F )} a mapping satisfying Property ( ). We define the ZT-HD-Rabin-automaton A Rabin Z F = (Q, Σ, I, Γ, ∆, Rabin Γ (R)) as a (non-deterministic) automaton using a Rabin acceptance condition, where:

Q = {1, 2, . . . , rbw(Z F )}, I = Q 8 , Γ = N (
the colours of the acceptance condition are the nodes of the Zielonka tree), δ(q, a) = { Jump(l, Supp(l, a)), Supp(l, a)

| l ∈ Leaves(Z F ) such that η(l) = q}, R = {(G n , R n )} n∈N ,
where G n and R n are defined as follow: Let n be a round node and n be any node of

Z F , n ∈ G n if n = n, n ∈ R n if n = n and n is not an ancestor of n .
Remark 4.42. Although we will usually say that A Rabin Z F is the ZT-HD-Rabin-automaton of 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 η.

The intuition behind this definition is the following. The automaton A Rabin Z F has rbw(Z F ) states, and each of them can be associated to a subset of leaves of Z F by η -1 (q). The mapping η is such that the lowest common ancestor of two leaves in η -1 (q) is a square node. As for the ZT-parity-automaton, for each leaf of l ∈ Leaves(Z F ) and letter a ∈ Σ, we identify the deepest ancestor n = 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 a:n --→ q if there are leaves l ∈ η -1 (q) and l ∈ η -1 (q ) giving such a path. This way, we can identify a run in the automaton A Rabin Z F with a promenade through the nodes of the Zielonka tree in which jumps between leaves with the same η-image are allowed. If during this promenade a unique minimal node (for ) is visited infinitely often, it is not difficult to see that the sequence of input colours belongs to F if and only if the label of this minimal node belongs to 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 A Rabin Z F is as a quotient of the deterministic parity automaton A parity Z F . Indeed, the graph structure and the labelling by input letters of A Rabin Z F is obtained by merging the states of A parity Z F (which are the leaves of Z F ) with the same η-image, and keeping all the transitions between them. However, a parity acceptance condition over this smaller structure is no longer sufficient to accept Muller(F). The Rabin condition of this automaton is given by two Rabin pairs (corresponding to the round nodes of the Zielonka tree): We note that the automaton A Rabin Z F is obtained by merging the states θ and ξ from the ZT-parity-automaton A parity Z F appearing in Figure 9, and replacing the output colours by suitable nodes from the Zielonka tree.

G β = {β}, R β = {α, λ, ξ, ζ}, G λ = {λ}, R λ = {α, β, θ}.
Remark 4.44. We observe that the automaton from Figure 13 presents duplicated edges, in the sense that there are two transitions q a:x --→ q and q 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 F ⊆ 2 Σ + be a family of non-empty subsets. Then,

L(A Rabin Z F ) = Muller Σ (F).

Moreover, the automaton

A Rabin Z F is history-deterministic. Lemma 4.46. Let u = n 0 n 1 n 2 • • • ∈ N ω be

an infinite sequence of nodes of the Zielonka tree. The word u belongs to Rabin

N (R), for R = {(G n , R n )} n∈N the Rabin condition of A Rabin Z F ,

if and only if there is a unique minimal node for the ancestor relation in Inf(u) and this minimal node is round (recall that the root is the minimal element for ).

Proof. Suppose that there is a unique minimal node in 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 Inf(u) ∩ G n = ∅, because n ∈ G n . It suffices to show that Inf(u) ∩ R n = ∅: By minimality, any other node n ∈ Inf(u) is a descendant of n (equivalently, n is an ancestor of n ), so n / ∈ R n . Conversely, suppose that u ∈ Rabin N (R). Then, there is some round node n ∈ N such that Inf(u) ∩ G n = ∅ and Inf(u) ∩ R n = ∅. Since G n = {n}, we deduce that n ∈ Inf(u).
Moreover, as Inf(u) ∩ R n = ∅, all nodes in Inf(u) are descendants of n. We conclude that n is the unique minimal node in Inf(u), and it is round.

Lemma 4.47. There exists a morphism of automata

ϕ : A parity Z F → A Rabin Z F . Proof.
We define the morphism ϕ as follows:

ϕ V (l) = η(l), for l ∈ Leaves(A parity Z F ), for a transition e = l a:c --→ l in A parity
Z F , we let ϕ E (e) = (η(l), a, Supp(l, a), l ). It is clear that ϕ is a weak morphism. We prove that it preserve the acceptance of runs.

Let ρ = l 0 w0 --→ l 1 w1 --→ l 2 w2 --→ • • • ∈ Run(A parity Z F ) be an infinite run in A parity Z F
(the only run over w 0 w 1 w 2 • • • ∈ Σ ω ), and let n i = Supp(l i , w i ). By definition of the morphism, the output of the run ) and let u ∈ N ω be the sequence of nodes produced as output of an accepting run over w in A Rabin Z F . By Lemma 4.46, there is a unique minimal node n for appearing infinitely often in u and moreover n is round. Let n 1 , . . . , n k be an enumeration of the children of n (from left to right), with labels ν(n i ) ⊆ Σ (we remark that ν(n i ) / ∈ F, for 1 ≤ i ≤ k). We will prove that Inf(w) ⊆ ν(n) and Inf(w) ν(n i ) for 1 ≤ i ≤ k. By definition of the Zielonka tree, as n is round, this implies that Inf(w) ∈ F.

ρ = ϕ Runs (ρ) in A Rabin Z F is γ (ρ ) = n 0 n 1 n 2 • • • ∈ N ω .
Since eventually all nodes produced as output are descendants of n (by minimality), Inf(w) must be contained in ν(n) (by definition of the transitions of A Rabin Z F ). We suppose, towards a contradiction, that Inf(w) ⊆ ν(n j ) for some 1 ≤ j ≤ k. Let Q i = {η(l) : l is a leaf below n i } be the set of states corresponding to leaves under n i , for 1 ≤ i ≤ 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 k i=1 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 ( ), we have

Q i ∩ Q j = ∅, for all i = j. By definition of the transitions of A Rabin Z F , if a ∈ Σ is a letter in ν(n) but not in ν(n i ), all transitions from some state in Q i reading the colour a go to Q i+1 , for 1 ≤ i ≤ k -1 (and to Q 1 if i = k). Also, if a ∈ ν(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 Inf(w) ⊆ ν(n j ). However, the only transitions from Q j that would produce n as output are those corresponding to a colour a / ∈ ν(n j ), so the node n is not produced infinitely often, a contradiction.

Muller Σ (F) ⊆ L(A Rabin Z F ) and history-determinism: The existence of a morphism ϕ : 4.47) and the correctness of A parity Z F (Proposition 4.10) imply that

A parity Z F → A Rabin Z F (Lemma
L(A Rabin Z F ) = L(A parity Z F ) = Muller(F).
Indeed, if ρ is an accepting run over w ∈ Σ ω in A parity Z F , then ϕ Runs (ρ) is an accepting run over w in A Rabin Z F . We can moreover use A parity

Z F
and ϕ to define a sound resolver (r 0 , r) for A Rabin Z F : we let r 0 = ϕ(q 0 ) be the image of the initial state of

A parity Z F . If ρ R ∈ Run fin (A Rabin Z F )
is the image under ϕ Runs of some finite run ρ P ∈ Run fin (A parity Z F ), we let r(ρ R , a) = ϕ(e), where e is the only a-labelled transition from Target(ρ P ). We define r arbitrarily in other case. This way, for every w ∈ Σ ω , the run induced by r over w is the image of a run over w in A parity Z F , which must be accepting if w ∈ Muller(F).

Optimality of the Zielonka-tree-HD-Rabin-automaton

We devote this section to the proof of the optimality of A Rabin Z F .

Theorem 4.48 (Optimality of the ZT-HD-Rabin-automaton). Let A be a history-deterministic Rabin automaton accepting a Muller language Muller Σ (F). Then, |A Rabin Z F | ≤ |A|.

Proposition 4.49 ([28]). Let L = Muller Σ (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 rbw(Z F ).

2.

There exists a game 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 rbw(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 A be a history-deterministic Rabin automaton. Then, if Eve wins a game with W = L(A) as acceptance set from a position v, there is a winning strategy from v for her implemented by a memory structure of size |A|.

Proof. Let G be a game with W = L(A) as acceptance set. In order to be able to take the product by A and obtain an equivalent game, we transform G into a game suitable for transformations. Let G be the game obtained from G in the following way: for every edge e = v a -→ v in G, we add a position (v, e) controlled by Eve and replace edge e by v ε -→ (v, e) a -→ v . It is clear that Eve wins G from a vertex v if and only if she wins G from that same vertex. By Proposition 2.7, if Eve wins G from a vertex v, she wins G A from a vertex (v, q 0 ), where q 0 is an initial vertex of A. Moreover, the game G A uses the acceptance set from A, which is a Rabin language, so, by Lemma 4.50, she can win using a strategy given by a function σ : ṼEve → Ẽ, where Q is the set of states of A and ṼEve the vertices controlled by Eve in G (a subset of (V Eve (V × E)) × Q). We build a memory structure (M, σ M ) of size |Q| that projects the strategy implemented by σ onto G:

its set of states is M = Q, the initial state is q 0 , the update function µ : M × E → M sends µ(q, e) = q if σ((v, e), q) = ((v, e), q) - → (v , q ) is the move chosen by σ from vertex ((v, e), q), for v ∈ V Eve , q ∈ M , we let σ M (v, q) = e if e is the move chosen by σ from (v, q), that is, if σ(v, q) = (v, q) - → ((v, q), e).
Since σ implements a winning strategy in G A from (v, q 0 ), its projection onto G via the memory structure (M, σ M ) is a strategy that verifies that any play consistent with it produces as output a word in L(A), so it is winning.

Theorem 4.48 is obtained by combining the fact that |A Rabin Z F | = rbw(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 A into an equivalent DPA ACD parity (A). Formally, the validity of this transformation is witnessed by a locally bijective morphism ϕ : ACD parity (A) → A (Proposition 5.18). In Section 5.3, we describe the ACD-HD-Rabin-transform that turns a DMA A into an equivalent history-deterministic Rabin automaton ACD Rabin (A). The validity of the transformation is witnessed by an HD mapping ϕ : ACD Rabin (A) → A (Proposition 5.25). These constructions grant strong optimality guarantees. The automaton ACD parity (A) (resp. ACD Rabin (A)) has a minimal number of states amongst parity (resp. Rabin) automata admitting an HD mapping to A (Theorems 5.32 and 5.33). We note that this implies minimality amongst automata admitting a locally bijective morphism to A. Moreover, the acceptance condition of ACD parity (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 TS = (G TS , Acc TS ) be a Muller transition system with underlying graph G TS = (V, E, Source, Target, I) and using a Muller acceptance condition Acc TS = (γ, Γ, Muller Γ (F)).

The alternating cycle decomposition

Definition 5.1. Let 0 ∈ Cycles(TS) be a cycle. We define the tree of alternating subcycles of 0 , denoted AltTree( 0 ) = (N, , ν : N → Cycles(TS)) as a Cycles(TS)-labelled tree with nodes partitioned into round nodes and square nodes, N = N N , such that:

The root is labelled 0 . If a node is labelled ∈ Cycles(TS), and is an accepting cycle (γ( ) ∈ F), then it is a round node, and its children are labelled exactly with the maximal subcycles ⊆ such that is rejecting (γ( ) / ∈ F).

If a node is labelled ∈ Cycles(TS), and is a rejecting cycle (γ( ) / ∈ F), then it is a square node, and its children are labelled exactly with the maximal subcycles ⊆ such that is accepting (γ( ) ∈ F).

For a Cycles(TS)-labelled tree T = (N, , ν : N → Cycles(TS)) and n ∈ N , we let ν States (n) = States(ν(n)) be the set of states of the cycle labelling n.

Remark 5.2. Let n be a node of AltTree( 0 ) and let n 1 be a child of it. If is a cycle such that ν(n 1 )

⊆ ν(n), then ν(n 1 ) is accepting ⇐⇒ is rejecting ⇐⇒ ν(n) is rejecting.

Definition 5.3 (Alternating cycle decomposition).

Let TS be a transition system, and let 1 , 2 , . . . , k be an enumeration of its maximal cycles (that is, the edges sets of its SCCs). We define the alternating cycle decomposition of TS to be the forest ACD TS = {AltTree( 1 ), . . . , AltTree( k )}.

We let N i be the set of nodes of AltTree( i ), and n i its root. We will suppose that

N i ∩ N j = ∅ if i = j.
We define the set of nodes of ACD TS to be Nodes(ACD TS ) = k i=1 N i , and we let Nodes (ACD TS ) (resp. Nodes (ACD TS )) be the subset of round (resp. square) nodes. As for Zielonka trees, we equip the trees of ACD TS 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 TS, there is one and only one tree AltTree( i ) in ACD TS such that v ∈ ν States (n i ). On the other hand, transient vertices do not appear in the trees of ACD TS .

If v is a recurrent vertex of TS, we define the local subtree at v, noted T v , as the subtree of AltTree( i ) containing the nodes

N v = {n ∈ N i | v ∈ ν States (n)}. If v is a transient vertex,
we define T v to be a tree with a single node.

For v recurrent, as N v is a subset of the nodes of AltTree( i ), the tree T v inherits the order from AltTree( i ), as well as its partition into round and square nodes,

N v = N v,
N v, . Also, it inherits the labelling given by the mapping ν, whose restriction to T v has an image in Cycles v (TS).

Remark 5.4. Let v ∈ ν States (n i ). If n ∈ N v and n is an ancestor of n in AltTree( i ), then n ∈ N v . In particular, T v is indeed a subtree of AltTree( i ). Also, we note that the root of T v is n i .

For a node n ∈ N i and an edge e ∈ i we define Supp(n, e) = n to be the deepest ancestor of n such that e ∈ ν(n ). We remark that if e = v -→ v , then Supp(n, e) is a node in both T v and T v .

Example 5.5. We will use the transition system TS from Figure 14 as a running example. We have named the edges of TS with letters from a to l, that are also used as the output colours of the acceptance condition. The acceptance set of TS is the Muller language associated to: d, e}, {e}, {g, h, i}, {l}, {h, i, j, k}, {j, k}}. The initial vertex of TS, v 0 , is its only transient vertex, all the others vertices are recurrent. TS has 2 strongly connected components, corresponding to cycles 1 and 2 .

F = {{c,
The alternating cycle decomposition of TS is shown in Figure 15. It consists of two trees, AltTree( 1 ) and AltTree( 2). We use Greek letters (in pink) to name the nodes of the tree. Inside each node we indicate both its label ν(n) and the set of states of it. For example, {{c, d, e}, {e}, {g, h, i}, {l}, {h, i, j, k}, {j, k}}. The two maximal cycles, 1 and 2, are encircled by blue and red dashed lines, respectively. ν(κ) = {g, h, i} and ν States (κ) = {v 3 , v 4 }. We have that Supp(τ, g) = κ and Supp(τ, j) = λ. We highlight in bold orange the local subtree at v 4 , T v4 . The tree T v0 , consisting in a single node, does not appear in the figure. The numbering on the right of the trees will be used in next section.

v 0 v 1 v 2 v 3 v 4 v 5
c,d,e v 1 , v 2 c,d v 1 , v 2 2 3 α β AltTree(ℓ 1 ) g,h,i,j,k,l v 3 , v 4 , v 5 g,h,i v 3 , v 4 l v 5 h,i,j,k v 3 , v 4 , v 5 g v 3 h,i v 3 , v 4 h,i v 3 , v 4 1 2 3 λ κ ζ χ ξ τ θ
AltTree(ℓ 2 )

Figure 15 Alternating cycle decomposition of TS. In bold orange, the local subtree at v4, Tv 4 .

Remark 5.6. Let TS be a Muller TS using as acceptance set W = Muller Γ (F), and let TS be the TS obtained by replacing W with W = Γ ω \ W (which is a Muller language). Then, the ACD of TS coincides with that of TS, with the only difference that the partition into round and square nodes is inverted: Nodes (ACD TS ) = Nodes (ACD TS ) and Nodes (ACD TS ) = Nodes (ACD TS ).

We note that if A is a DMA recognising L ⊆ Σ ω , the automaton A is a DMA recognising Σ ω \ L.

Remark 5.7. The Zielonka tree can be seen as a special case of the alternating cycle decomposition. Indeed, a Muller language Muller(F)Σ can be trivially recognised by a DMA A with a single state q and self-loops q a:a --→ q. The ACD of this automaton is exactly the Zielonka tree of F.

Local Muller languages.

For a recurrent state v of TS, we define the local Muller language of TS at v as the Muller language defined over the alphabet Γ v = Cycles v (TS) associated to:

LocalMuller TS (v) = {C ⊆ Cycles v (TS) | ∈C is an accepting cycle}.
We note that LocalMuller TS (v) is completely determined by singletons (C ∈ LocalMuller TS (v) if and only if { ∈C } ∈ LocalMuller TS (v)). For simplicity, and by a slight abuse of notation, we will work as if LocalMuller TS (v) ⊆ Cycles v (TS). To lighten notations, we will just write LocalMuller TS (v) to denote Muller(LocalMuller TS (v)) whenever no confusion arises.

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

Lemma 5.8. Let v be a recurrent vertex. The tree T v is the Zielonka tree of the family LocalMuller TS (v) 9 .

An optimal transformation to parity transition systems

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

Let TS be a Muller transition system and let ACD TS = {AltTree( 1 ), . . . , AltTree( k )} be its alternating cycle decomposition.

We say that a tree AltTree( i ) ∈ ACD TS is positive if i is an accepting cycle, and that it is negative otherwise. We say that the alternating cycle decomposition of TS is positive if all the trees of maximal height of ACD TS are positive, that it is negative if all trees of maximal height are negative, and that it is equidistant if there are positive and negative trees of maximal height.

As for the Zielonka tree, we associate a non-negative integer to each level of the trees of ACD TS via a function p ACD (n) : Nodes(ACD TS ) → N. Let i be a maximal cycle of TS and n ∈ N i .

If ACD TS is positive or equidistant:

p ACD (n) = Depth(n), if i is accepting, p ACD (n) = Depth(n) + 1, if i is rejecting.
If ACD TS is negative:

p ACD (n) = Depth(n) + 2, if i is accepting, p ACD (n) = Depth(n) + 1, if i is rejecting.
We let min TS (resp. max TS ) be the minimum (resp. maximum) value taken by the function p ACD .

9 Formally, the labelling ν of Tv goes to Cycles v (TS), and not to 2

(n) = { ∈ Cycles v (TS) | ⊆ ν(n)}.
Remark 5.9. A node n in AltTree( i ) verifies that p ACD (n) is even if and only if ν(n) is an accepting cycle (that is, if n is a round node).

Remark 5.10. It is satisfied:

min TS = 0 if ACD TS is positive or equidistant, min TS = 1 if ACD TS is negative.
Example 5.11. In the previous Example 5.5, AltTree( 1) is a positive tree and AltTree( 2) is negative. As AltTree( 2) is the tree of maximal height, ACD TS is negative. The function p ACD is represented in Figure 15 by the integers on the right of each tree. It takes values 2 and 3 over AltTree( 1) (p ACD (α) = 2 and p ACD (β) = 3), because ACD TS is negative. In this example, min TS = 1 and max TS = 3. We note that if we had associated integers 0 and 1 to the levels of AltTree( 1), we would have used 4 integers in total, instead of just 3 of them. Definition 5.12 (ACD-parity-transform). Let TS be a Muller TS with ACD TS = {AltTree( 1 ), . . . , AltTree( k )}. We define the ACD-parity-transform of TS be the parity TS ACD parity (TS) = (G , Acc ), with G = (V , E , Source , Target , I ), and Acc = (γ , [min TS , max TS ], parity) defined as follows.

Vertices. The set of vertices is

V = v∈V ({v} × Leaves(T v )) . Initial vertices. I = {(v 0 , n) | v 0 ∈ I and n is the leftmost leaf in T v0 }.

Edges and output colours. For each

(v, n) ∈ V and each edge e = v - → v ∈ Out(v) in TS we define an edge e n = (v, n) γ (en) ----→ (v , n ). Formally, E = e∈E {e} × Leaves(T Source(e) ) .
If v and v are not in the same SCC, we let n be the leftmost leaf in T v and γ (e n ) = min TS10 . If v and v belong to the same SCC, we let:

n = Jump T v (n, Supp(n, e)), γ (e n ) = p ACD (Supp(n, e)).
Labellings. If TS is a labelled transition system, with labels l

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

Example 5.13. We show in Figure 16 the ACD-parity-transform ACD parity (TS) of the transition system TS from Figure 14 (Example 5.5). For each vertex v in TS, we make as many copies as leaves of the tree T v . We note that, as v 0 is transient, the tree T v0 consists of a single node (by definition), that we name ι. Transitions are of the form (e, l), for e a transition from TS and l a leaf of some local subtree; these are denoted e l in the figure for the sake of space convenience. These labels simply indicate the names of the edges, they should not be interpreted as input letters (ACD parity (TS) is not an automaton).

We observe that there is a locally bijective morphism of transition systems ϕ from ACD parity (TS) to TS given by ϕ

V (v, l) = v and ϕ E (e l ) = e. v 0 , ι v 1 , β v 2 , β v 3 , ξ v 3 , τ v 3 , θ v 4 , τ v 4 , θ v 5 , ζ v 5 , χ a ι : 1 b ι : 1 c β : 3 f β : 1 d β : 3 e β : 2
g ξ : 3 h ξ : 2 g τ : 2 h τ : 3 g θ : 1 h θ : 3 i τ : 3 j τ : 1 i θ : 3 j θ : 2 k χ : 2 l χ : 1 k ζ : 1 l ζ : 2
Figure 16 ACD-parity-transform ACDparity(TS) of the transition system TS from Figure 14.

Another example can be found in Figure 17.

Remark 5.14. The size of the ACD-parity-transformation of TS is:

|ACD parity (TS)| = v∈V |Leaves(T v )| = v∈Vrec |Leaves(T v )| + |V trans |,
where V rec and V trans are the sets of recurrent and transient vertices of TS, respectively. Remark 5.15. We remark that if TS = (G TS , Acc TS ) is already a parity TS, then the underlying graphs of ACD parity (TS) and TS are isomorphic. In fact, by Proposition 5.18, ACD parity (TS) and TS will also be isomorphic as transition systems. In this case, the construction of ACD parity (TS) boils down to the application of the procedure described by Carton and Maceiras [15].

Remark 5.16. The ACD-parity-transform is oblivious to the labelling γ of the acceptance condition of TS; the only information taken into account to define the graph of ACD parity (TS) and its output colours is the structure of the trees of ACD TS . That is, the definition of this transformation is independent of the actual representation of the acceptance condition of TS (whether it is Emerson-Lei, Muller, Rabin...), and we only use that any such representation induces a mapping f : Cycles(TS) → {Accept, Reject}.

Remark 5.17. The ZT-parity-automaton can be seen as a special case of the ACD-paritytransform, as A parity Z F coincides with the DPA ACD parity (A), where A is the DMA with a single state recognising Muller(F) (see Remark 5.7).

Correctness of the ACD-parity-transform

Proposition 5.18 (Correctness of the ACD-parity-transform). Let TS be a (labelled) Muller TS and let ACD parity (TS) be its ACD-parity-transform. There is a locally bijective morphism of (labelled) transition systems ϕ : ACD parity (TS) → TS.

The following lemma, analogous to Lemma 4.11 from Section 4.2, follows from the definition of the ACD-parity-transform. Lemma 5.19. Let n be a node of AltTree( i ), let ñ be an ancestor of n and let e = v -→ v be an edge in i . Then, Supp(n, e) is a descendant of ñ if and only if e ∈ ν(ñ), and in this case, if

e n = (v, n) - → (v , n ) is an edge of ACD parity (TS), then n is a descendant of ñ too.
Proof of Proposition 5.18. We consider the mapping ϕ = (ϕ V , ϕ E ) naturally defined by

ϕ V (v, n) = v and ϕ E (e n ) = e.
It is immediate to check that ϕ is a weak morphism of transition systems (it preserves initial states and transitions). Also, it is easy to see that it is locally bijective: for each initial state v 0 ∈ I, there is exactly one node in I of the form (v 0 , n): the node where n is the leftmost leaf of T v ; and for each vertex (v, n) and edge e ∈ Out(v) of TS, we have define exactly one edge outgoing from (v, n) corresponding to e. We prove that ϕ preserves the acceptance of runs, following the proof scheme from Proposition 4.10. We can suppose w.l.o.g. (see Remarks 2.1 and 5.16) that the set of output colours used by TS is its set of edges E. Let ρ ∈ Run(ACD parity (TS)) be an infinite run in ACD parity (TS). Eventually, ρ will remain in one SCC, and Inf(ρ) will form a cycle that is accepting if and only if ρ is an accepting run. We will suppose that all the edges in ρ appear infinitely often and belong to this cycle (we can do it by using a similar argument as the one presented in the proof of Proposition 4.10), and we let:

ρ = (v 0 , n 0 ) x0 -→ (v 1 , n 1 ) x1 -→ (v 2 , n 2 ) x3 -→ . . . .
The projection of ρ under ϕ is:

ϕ Runs (ρ) = v 0 e0 -→ v 1 e1 -→ v 2 e3 -→ . . . .
We note that the edges {e 0 , e 1 , . . . } form a cycle in TS, that we will call ρ . In particular, ρ is contained in some maximal cycle max , and all the nodes n i belong to the same tree AltTree( max ) of the ACD. Our objective is to show that ρ is an accepting cycle in TS if and only if min{x 0 , x 1 , x 2 , . . . } is even. We let ñi = Supp(n i , e i ) be the node of ACD TS determining the i th transition of ρ, so we have that x i = p ACD (ñ i ). Finally, let n ρ be the deepest ancestor of n 0 such that ρ ⊆ ν(n ρ ).

Claim 5.18.1. For all i ≥ 0, n i n ρ and ñi n ρ (that is, all nodes appearing in ρ are below n ρ ). In particular, x i ≥ p ACD (n ρ ).

Proof. The claim follows from Lemma 5.19 and induction.

Claim 5.18.2. Let n ρ,1 , . . . , n ρ,s be an enumeration of Children AltTree( max) (n ρ ). It is verified that:

1. Supp(n i , e i ) = n ρ infinitely often. In particular, x i = p ACD (n ρ ) for infinitely many i's.

There is no n

ρ,k ∈ Children(n ρ ) such that ρ ⊆ ν(n ρ,k ).
Proof. The proof is identical to that of Claim 4.10.2, from Proposition 4.10.

We conclude that min{x 0 , x 1 , x 2 , . . . } = p ACD (n ρ ), which is even if and only if ρ is an accepting cycle, by Remarks 5.2 and 5.9. Remark 5.20. We can give an alternative interpretation of the previous proof. Given a run ρ in TS and a vertex v appearing infinitely often in ρ, we can decompose the run into:

ρ0 v ρ1 v ρ2 v ρ3 v ρ4 . . . ,
where the finite runs ρ i are cycles over v, for i > 0. Therefore, the sequence of these cycles can be processed by the ZT-parity-automaton corresponding to the local Muller condition LocalMuller TS (v). By Lemma 5.8 and the correctness of the ZT-parity-automaton, the minimal colour produced by a run over this sequence of cycles in A parity Z LocalMuller T S (v) coincides with the minimal output colour produced by the run ϕ -1 Runs (ρ) in the ACD-parity-transform ACD parity (TS) (disregarding the initial path ρ 0 ). This colour is exactly the one corresponding to the deepest node in T v above the leftmost leaf containing Inf(ρ).

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

Corollary 5.21. Let A be a Muller automaton and let ACD parity (A) be its ACD-paritytransform. Then, L(A) = L(ACD parity (A)), and A is deterministic (resp. history-deterministic) if and only if ACD parity (A) is deterministic (resp. history-deterministic).

Corollary 5.22. Let G be a Muller game and let ACD parity (G) be its ACD-parity-transform. Eve wins ACD parity (G) from a vertex of the form (v, n) if and only if she wins G from v.

An optimal history-deterministic transformation to Rabin transition systems

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

Definition 5.23 (ACD-HD-Rabin-transform).

Let TS be a Muller TS. For each vertex v ∈ V we let η v : Leaves(T v ) → {1, . . . , rbw(T v )} be a mapping satisfying Property ( ) from Lemma 4.39. We define the ACD-HD-Rabin-transform of TS to be Rabin TS ACD Rabin (TS) = (G , Acc ), with G = (V , E , Source , Target , I ), and Acc = (γ , Nodes(ACD TS ), Rabin(R)) defined as follows.

Vertices. The set of vertices is

V = v∈V ({v} × {1, . . . , rbw(T v )}) ,
where rbw(T v ) is the round-branching width of T v .

Initial vertices. I

= {(v 0 , x) | v 0 ∈ I and x ∈ {1, . . . , rbw(T v0 )}}.
Edges and output colours. We let

E = e∈E {e} × Leaves(T Source(e) ) .
For each edge e = v -→ v ∈ E in TS and x ∈ {1, . . . , rbw(T v )}, we will place one edge from

(v, x) for each leaf l of T v such that η v (l) = x. More precisely, we let (v, x) n -→ (v , x ) ∈ E if either
v and v are not in the same SCC (in this case the output colour n is irrelevant), or v and v are in the same SCC and there are leaves l and l of T v and T v , respectively, such that:

η v (l) = x, η v (l ) = x , l = Jump T v (l, Supp(l, e)), n = Supp(l, e). Rabin condition. R = {(G n , R n )} n∈Nodes (ACD T S )
, where G n and R n are defined as follow:

Let n be a round node, and let n be any node in Nodes(ACD TS ),

n ∈ G n if n = n, n ∈ R n if n = n and n is not an ancestor of n .
Labellings. If TS is a labelled transition system, with labels l

V : V → L V and l E : E → L E , we label ACD Rabin (TS) by l V (v, x) = l V (v) and l E (e ) = l E (e), if e ∈ E (e).
This construction generalises the ZT-HD-Rabin-automaton in the same way as the ACDparity-transform generalises the ZT-parity-automaton. Intuitively, a run in ACD Rabin (TS) can be identified with a promenade through the nodes of the ACD, which are used as the output colours to define the Rabin acceptance condition.

Remark 5.24. The size of the ACD-HD-Rabin-transform of TS is:

|ACD Rabin (TS)| = v∈V rbw(T v ) = v∈Vrec rbw(T v ) + |V trans |,
where V rec and V trans are the sets of recurrent and transient vertices of TS, respectively.

Correctness of the ACD-HD-Rabin-transform

To obtain the correctness of the ACD-HD-Rabin-transform, we follow the same steps as in the proof of the correctness of the ZT-HD-Rabin-automaton (Proposition 4.45). Proposition 5.25 (Correctness of the ACD-HD-Rabin-transform). Let TS be a (labelled) Muller TS and let ACD Rabin (TS) be its ACD-HD-Rabin-transform. There is an HD mapping of (labelled) transition systems ϕ : ACD Rabin (TS) → TS.

The proof of next two lemmas are completely analogous to those of Lemmas 4.46 and 4.47.

Lemma 5.26. Let u = n 0 n 1 n 2 • • • ∈ Nodes(ACD TS ) ω be an infinite sequence of nodes of the ACD of TS. The word u belongs to Rabin(R), for R = {(G n , R n )} n∈Nodes (ACD T S )
the Rabin condition of ACD Rabin (TS), if and only if there is a unique minimal node for the ancestor relation in Inf(u) and this minimal node is round. Lemma 5.27. There exists a morphism of transition systems ϕ : ACD parity (TS) → ACD Rabin (TS).

Using these lemmas we can prove Proposition 5.25.

Proof of Proposition 5.25. We define the mapping ϕ : ACD Rabin (TS) → TS in the natural way: ϕ V (v, x) = v and ϕ E (e, l) = e. It is immediate to check that ϕ is a weak morphism. The fact that ϕ preserves accepting runs can be proven analogously to the fact that L(A Rabin Z F ) ⊆ Muller Σ (F) in Proposition 4.45 (by using Lemma 5.26).

Definition of a sound resolver for ϕ: In order to show how to simulate runs of TS in ACD Rabin (TS), we use the fact that we can see ACD Rabin (TS) as a quotient of ACD parity (TS) (Lemma 5.27). Let φ : ACD parity (TS) → TS be the locally bijective morphism given by Proposition 5.18, and let φ : ACD parity (TS) → ACD Rabin (TS) be the morphism given by Lemma 5.27. Since φ is locally bijective, φRuns is a bijection between the runs of the transitions systems ACD parity (TS) and TS, admitting an inverse φ-1

Runs . Composing this mapping with φ, we obtain a way to simulate the runs from TS in ACD Rabin (TS):

φRuns • φ-1
Runs : Run ∞ (TS) → Run ∞ (ACD Rabin (TS)). This composition of mappings provides a sound resolver simulating ϕ. Formally, let (r Init , r) be the resolver defined as follows. The choice of initial vertices r Init : I → I is given by r Init (v 0 , x) = v 0 . The function r : E * × E → E associates to a finite run ρ ∈ E * and e ∈ E the last edge of the run φ( φ-1 (ϕ(ρ)e)) (subscripts have been omitted for legibility). It is easy to check that (r Init , r) indeed defines a resolver simulating ϕ. Its soundness follows from the fact that φ and φ preserve the acceptance of runs.

From Proposition 3.16 we obtain: Corollary 5.28. Let A be a Muller automaton and let ACD Rabin (A) be its ACD-HD-Rabintransform. Then, L(A) = L(ACD Rabin (A)), and A is history-deterministic if and only if ACD Rabin (A) is history-deterministic.

ACD-HD-Rabin-transform-for-games

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

For a Muller game G suitable for transformations, we define its ACD-HD-Rabin-transformfor-games, written ACD game parity (G). The idea is simply to take from Adam the power to update the ACD G -component of vertices. The update of this information is delayed of one transition, so it is Eve who makes the choice of how to move in the ACD. To do this, we need to introduce some additional vertices controlled by Eve. The formal details of this construction and the proof of correctness can be found in Appendix B. Proposition 5.29 (Correctness of the ACD-HD-Rabin-transform-for-games). Let G be a Muller game suitable for transformations, and let ACD game parity (G) be its ACD-HD-Rabin-transform-forgames. There is an HD-for-games mapping ϕ : ACD game parity (G) → TS. Corollary 5.30. Let G be a Muller game suitable for transformations, and let ACD game parity (G) be its ACD-HD-Rabin-transform-for-games. Then, Eve's full winning region in G is the projection of her full winning region in ACD game parity (G).

Optimality of the ACD-transforms

We now state and prove the optimality of both the ACD-parity-transform (Theorems 5.31 and 5.32) and the ACD-HD-Rabin-transform (Theorem 5.33). The proofs of these results will use the optimality of the automata based on the Zielonka tree (c.f. Section 4) as a black-box, which will allow us to prove the optimality of both transformations at the same time. The key idea is that if ϕ : TS → TS is an HD mapping, we can see TS as an HD automaton recognising the accepting runs of TS . We can then use local Muller conditions at vertices of TS to reduce the problem to automata recognising Muller languages.

Statements of the optimality results

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

Theorem 5.31. Let TS be a Muller TS whose states are accessible and let TS be a parity TS. If TS admits an HD mapping ϕ : TS → TS, then, its acceptance condition uses at least as many colours as that of ACD parity (TS). We obtain an analogous optimality result for the ACD-HD-Rabin-transform-for-games. In this case, the bound is not tight due to the additional vertices that are added to ACD game parity (G) (see Appendix B for details).

Discussion

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

Difficulty of finding succinct history-deterministic automata.

As mentioned in the introduction, several years had to pass after the introduction of history-deterministic automata [START_REF] Boker | When a little nondeterminism goes a long way: An introduction to history-determinism[END_REF] before finding HD automata that were actually smaller than equivalent deterministic ones [49].

As of today, we only know a handful of examples of ω-regular languages admitting succinct HD automata [1,49,[START_REF] Boker | History determinism vs. good for gameness in quantitative automata[END_REF], and their applicability in practice has yet to be fully determined.

We assert that we can derive from our results some enlightening explanations on the difficulty of finding succinct HD parity automata, and set some limits in their usefulness in practical scenarios such as LTL synthesis. First, Corollary 4.14 already sets the impossibility of the existence of small HD parity automata recognising Muller languages. Corollary 5.36 states that if an HD parity automaton A has been obtained as a transformation of a DMA B, then A is not strictly smaller than a minimal deterministic parity automaton for L(A). α, β, λ q 0 , q 1 α, λ q 0 , q 1 β, λ q 0 , q 1 0 1 ξ τ (b) Alternating cycle decomposition of A. To indicate the labels of the nodes of this ACD, we include just the colours of the corresponding edges. Figure 17 A minimal DMA whose ACD-parity-transform is not a minimal DPA.

q 0 , ξ q 1 , ξ q 0 , τ q 1 , τ c : 1 b : 1 a : 1 a : 1 b : 0 c : 1 c : 0 b : 1 a : 1 a : 1 b : 1 c : 0 (c) ACD-parity-transform of A, ACDparity(A), with 4 states.
Proof. We first note that a resolver for A ϕ (in the sense of HD automata) is a mapping of the form r : E * × E → E, as E is the input alphabet of this automaton. A resolver simulating ϕ (in the sense of HD mappings) is a mapping of the same form. It is straightforward to check that (q 0 , r) is a sound resolver for A ϕ if and only if (r Init , r) is a sound resolver simulating ϕ (where r Init (q 0 ) = q 0 is the only possible choice of initial vertex).

We prove that L(A ϕ ) = {ρ ∈ Run(TS ) | ρ is an accepting run}. First, we remark that if ρ is a run in A ϕ over ρ ∈ Run(TS ), then ρ = ϕ Runs (ρ), since the labelling of A ϕ by input letters is given exactly by ϕ itself. Therefore, if ρ ∈ L(A ϕ ), there exists an accepting run ρ over ρ , and since ϕ preserves accepting runs, ρ = ϕ Runs (ρ) is accepting in TS , proving the inclusion from left to right. For the other inclusion, we let (r Init , r) be a sound resolver simulating ϕ. If ρ is an accepting run in TS , then r Runs (ρ ) is an accepting run over ρ in A ϕ .

We recall that [min TS , max TS ] are the colours used by the ACD-parity-transform of TS, which coincides with the maximal height of a tree in ACD TS . We also recall that min TS = 0 if ACD TS is positive or equidistant, and that min TS = 1 if ACD TS is negative. Lemma 5.39. Let TS be a Muller TS, and let AltTree( ) ∈ ACD TS be a positive (resp. negative) tree of the ACD of TS of height d. Then, TS admits a positive (resp. negative) d-flower.

Proof. We use the same argument than the one used in the proof of Theorem 4.12. Let n 1 n 2 . . . n d be a branch of length d of AltTree( ) (where n 1 is the root and n d is a leaf of the tree). Let v ∈ ν States (n d ) be a vertex appearing in the leaf. Then, the whole branch is contained in T v (by Remark 5.4), that is, ν(n i ) ∈ Cycles TS (v). Moreover, ν(n 1 ) ν(n 2 ) . . . ν(n d ) is a chain that alternates accepting and rejecting cycles, so it is a d-flower that is positive if and only if ν(n 1 ) = is an accepting cycle, that is, if AltTree( ) is positive.

Lemma 5.40. Let TS be a Muller TS with a single initial vertex and whose vertices are all accessible. Then, the parity index of L Runs (TS) is:

[min TS , max TS ] if ACD TS is positive or negative, Weak max T S if ACD TS is equidistant.
Proof. We consider the identity morphism Id TS : TS → TS and its automaton A Id T S , which is a deterministic automaton trivially recognising L Runs (TS) (that is, we see TS as an automaton reading its own edges as input letters). The result follows from the Flower Lemma 2.16 and the fact that a tree AltTree( ) ∈ ACD TS of height d provides a d-flower that is positive if is accepting and negative if is rejecting (Lemma 5.39). These flowers are accessible as we have supposed that all the vertices of TS are accessible.

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

For a Muller TS TS and a vertex v, we let ACD (TS,v) be the alternating cycle decomposition of the accessible part of TS from v. We note that the trees of ACD (TS,v) are a subset of the trees of ACD TS : a tree AltTree( i ) ∈ ACD TS appears in ACD (TS,v) if and only if the cycle i is accessible from v. Accordingly, for each vertex v of TS we let min (TS,v) (resp. max (TS,v) ) be the minimum (resp. maximum) value taken by the function p ACD when restricted to the trees of ACD (TS,v) .

Remark 5.41. For every transition system TS, one of the two following statements holds:

There is some vertex v such that [min TS , max TS ] = [min (TS,v) , max (TS,v) ]. There are two vertices v 0 and v 1 such that min (TS,v0) = 0, max (TS,v0) = max TS -1 and min (TS,v1) = 1, max (TS,v1) = max TS .

Moreover, if all the states of TS are accessible, we can choose v (resp. v 0 and v 1 ) to be an initial vertex.

We can finally deduce Theorem 5.31 from the preceding lemmas.

Proof of Theorem 5.31. We suppose that we are in the first case of Remark 5.41 (a proof for the second case follows easily). First, we show that we can suppose that TS and TS have a single initial vertex. Let v be an initial vertex of TS such that [min TS , max TS ] = [min (TS,v) , max (TS,v) ]. Let ϕ : TS → TS be an HD mapping, and let (r Init , r) be a sound resolver simulating it. We let ṽ = r Init (v) be the initial vertex in TS chosen by the resolver. It suffices then to prove the result for the accessible part of TS from ṽ, the transition system TS v , and the restriction of ϕ to these transition systems.

From now on, we suppose that both TS and TS have a single initial vertex. By Lemma 5.40 and Proposition 2.15, a parity history-deterministic automaton recognising L Runs (TS) uses at least |[min TS , max TS ]| colours. By Lemma 5.38, the automaton A ϕ of the morphism ϕ is a parity history-deterministic automaton recognising L Runs (TS), and therefore uses at least |[min TS , max TS ]| colours. Since the acceptance condition of TS is exactly the same as that of A ϕ , we can conclude.

Optimality of the sizes of ACD parity (TS) and ACD Rabin (TS)

We prove now Theorems 5.32 and 5.33. Sketch of the proof. Let ϕ : TS → TS be an HD mapping, and let v be a vertex in TS. We can see the set ϕ -1 (v) as the states of an HD automaton reading finite runs in TS looping around v. This allows to define an HD automaton having ϕ -1 (v) as set of states and recognising LocalMuller TS (v). As the Zielonka tree of LocalMuller TS (v) is the tree T v , by optimality of the ZT-parity-automaton (resp. the ZT-HD-Rabin-automaton), we deduce that

|ϕ -1 (v)| ≥ |Leaves(T v )| (resp. |ϕ -1 (v)| ≥ rbw(T v )).
Definition 5.42. Let TS and TS be two transition systems, and let (γ, Γ, Muller Γ (F)) be the acceptance condition of TS. Let ϕ : TS → TS be a weak morphism of transition systems that is locally surjective, and let v be an accessible recurrent state of TS . For each ∈ Cycles v (TS ) we let ρ be a finite path starting and ending in v visiting exactly the edges of . We define the cycle-preimage-automaton at v to be the Muller automaton

A (ϕ -1 ,v ) = (Q v , Cycles v (TS ), Q v , 2 Γ + , δ, Muller 2 Γ + ( F )) over the input alphabet Cycles TS (v ) defined as: the set of states is Q v = ϕ -1 (v ),
all the states are initial, the output colours are non-empty subsets of the colours used by TS, (q 2 , C) ∈ δ(q 1 , ) if there is a finite path ρ ∈ Path fin q1 (TS) from q 1 to q 2 such that ϕ(ρ) = ρ producing as output the colours in C ⊆ Γ, that is γ(ρ) = C. If C is empty, this corresponds to an uncoloured edge q 1 :ε --→ q 2 . We remark that, since ϕ is supposed locally surjective, there is at least one such path ρ.

{C 1 , . . . , C k } ∈ F if and only if ∪ k i=1 C i ∈ F.
We remark that a transition e = q 1 :C

--→ q 2 in A (ϕ -1 ,v ) induces a finite path Unfold(e) = q 1 C q 2 in TS called the unfolding of e, producing as output the set of colours C and such that ϕ(Unfold(e)) = . In particular, a run ρ in A (ϕ Suppose now that L is a Rabin language represented by the Rabin pairs {(G 1 , R 1 ), . . . , (G r , R r )}. We define a family of Rabin pairs R = {( G1 , R1 ), . . . , ( Gr , Rr )} for L as:

{C 1 , . . . , C k } ∈ Gi (resp. ∈ Ri ) if ∪ k i=1 C i ∈ G i (resp. ∈ Ri ). It is immediate to see that L = Rabin 2 Γ + ( R).
Lemma 5.44. Let TS and TS be two Muller TS, ϕ : TS → TS a weak morphism of TS, and v an accessible recurrent state of TS . If ϕ is an HD mapping, then the automaton A (ϕ -1 ,v ) is history-deterministic and recognises the local Muller condition of TS at v .

Proof. L(A

(ϕ -1 ,v ) ) ⊆ LocalMuller v (TS): Let 1 2 • • • ∈ Cycles v (TS
) ω be a sequence of cycles accepted by A (ϕ -1 ,v ) . By prefix-independence of Muller languages we can suppose that all the cycles i appear infinitely often. Let ρ = q 0 1 :C1 ---→ q 1 2 -→ q 2 -→ . . . be an accepting run in A (ϕ -1 ,v ) over 1 2 . . . , and let Unfold(ρ) be its unfolding. As ρ is an accepting run, so is Unfold(ρ), and since ϕ preserves accepting runs, ϕ(Unfold(ρ)) is an accepting run in TS . The edges visited by ϕ(Unfold(ρ)) form the cycle ∪ i≥1 i , which is therefore an accepting cycle, so 1 2 • • • ∈ LocalMuller v (TS) by definition of local Muller condition.

LocalMuller TS (v ) ⊆ L(A (ϕ -1 ,v ) ) and history-determinism: Let r ϕ : E * × E → E be a sound resolver simulating ϕ. We will transfer the strategy given by r ϕ to define a resolver r A : ∆ * × Cycles v (TS ) → ∆ for A (ϕ -1 ,v ) , where ∆ is the set of transitions of the automaton. Let ρ 0 ∈ Run fin (TS ) be a finite run reaching v , and let ρ 0 = r ϕ,Runs (ρ 0 ) the preimage given by the resolver, ending in some q 0 ∈ Q v that is going to by used as initial state for A (ϕ -1 ,v ) . For a sequence e 1 e 2 . . . e k ∈ ∆ * and ∈ Cycles v (TS ), we let r A (e 1 e 2 . . . e k , ) = r ϕ (ρ 0 ρ 1 . . . ρ k , ρ ) 12 , where ρ j = ϕ(Unfold(e j )) and v ρ v is the finite run corresponding to fixed in the definition of A (ϕ -1 ,v ) . By definition, the obtained resolver satisfies the following property:

If e 1 e 2 • • • ∈ ∆ ω is the run induced by r A over 1 2 • • • ∈ Cycles v (TS ) ω , then ρ 0 Unfold(e 1 e 2 . . . )) = r ϕ,Runs (ρ 0 ρ 1 ρ 2 . . . ).

This gives us:

Inf( 1 , 2 , . . . ) is accepting cycle in TS ⇐⇒ ρ 0 ρ 1 ρ 2 . . . is accepting run in TS =⇒ =⇒ ρ 0 Unfold(e 1 e 2 . . . ) accepting run in TS ⇐⇒ e 1 e 2 . . . accepting run in A (ϕ -1 ,v ) .

Which allows us to conclude that the A (ϕ -1 ,v ) recognises LocalMuller v (TS) and that r A is a sound resolver.

Corollary 5.45. Let TS and TS be a Muller and a parity transition system, respectively, and let ϕ : TS → TS be an HD mapping. Let v be an accessible recurrent state of TS. Then,

|ϕ -1 (v)| ≥ |Leaves(Z LocalMuller T S (v) )| = |Leaves(T v )|.
Proof. By Lemma 5.44, the automaton A (ϕ -1 ,v) is a history-deterministic automaton recognising LocalMuller v (TS) of size |ϕ -1 (v)|, and by Lemma 5.43, it is a parity automaton. The optimality of the ZT-parity-automaton (Theorem 4.13) gives us the first inequality. The second equality follows from the fact that T v is the Zielonka tree of LocalMuller TS (v) (Lemma 5.8).

The next corollary admits an identical proof, using the optimality of the ZT-HD-Rabinautomaton (Theorem 4.48).

Corollary 5.46. Let TS and TS be a Muller and a Rabin transition system, respectively, and let ϕ : TS → TS be an HD mapping. Let v be an accessible recurrent state of TS. Then,

|ϕ -1 (v)| ≥ |rbw(Z LocalMuller T S (v) )| = |rbw(T v )|.
Theorems 5.32 and 5.33 follow from these two corollaries, the formulas for the size of the ACD-transforms (Remarks 5.14 and 5.24) and the fact that a locally surjective morphism ϕ : TS → TS is surjective if all vertices of TS are accessible (Lemma 3.5).

Corollaries

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

Typeness results

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

Question: Given a Muller automaton A, can we define a simpler acceptance condition over the underlying graph of A obtaining an equivalent automaton A ?

This question was first studied (in the context of automata using state-based acceptance) by Krishnan,Puri and Brayton [47,48], who showed how to determine if a DMA can be relabelled with an equivalent Büchi condition. Their work was generalized to parity automata by Boker,Kupferman and Steinitz [9], and related questions about typeness were studied for non-deterministic automata by Kupferman,Morgenstern and Murano [51], and for history-deterministic automata by Boker, Kupferman and Skrzypczak [START_REF] Niwiński | Relating hierarchies of word and tree automata[END_REF].

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

Typeness for Muller languages

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

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

We first introduce some definitions. The terminology will be justified by the upcoming results. Definition 6.1. Let T be a tree T with nodes partitioned into round nodes and square nodes. We say that T has:

: If C 1 ∈ F ⇐⇒ C 2 ∈ F, then, C 1 ∪ C 2 ∈ F ⇐⇒ C 1 ∈ F. 3. Z F has parity shape.
Moreover, if some of these conditions is satisfied, Muller Γ (F) is a [min F , max F ]-parity language. Corollary 6.5. A Muller language L ⊆ Γ ω is a parity language if and only if it is both a Rabin and a Streett language.

Typeness for Muller transition systems and deterministic automata

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

Equivalence of acceptance conditions and typeness

Let TS 1 = (G, Acc 1 ) and TS 2 = (G, Acc 2 ) be two transitions systems over the same underlying graph G, with acceptance conditions Acc i = (γ i , Γ i , W i ), for i ∈ {1, 2}. We say that Acc 1 and Acc 2 are equivalent over G, written Acc 1 G Acc 2 , if for all runs ρ ∈ Run(G), ρ is accepting for TS 1 if and only if it is accepting for TS 2 ; that is,

γ 1 (ρ) ∈ W 1 ⇐⇒ γ 2 (ρ) ∈ W 2 .
We write TS 1 TS 2 if TS 1 and TS 2 are isomorphic. We recall that two transition systems are isomorphic if there is a morphism of transition systems ϕ : TS 1 → TS 2 whose inverse is also a morphism, that is, ϕ and ϕ -1 preserve the acceptance of runs. Remark 6.6. If ϕ : TS 1 → TS 2 is an isomorphism, then (γ 2 • ϕ, Γ 2 , W 2 ) is an acceptance condition over the underlying graph of TS 1 that is equivalent to (γ 1 , Γ 1 , W 1 ) over this graph.

Conversely, if two acceptance conditions Acc 1 and Acc 2 are equivalent over a same graph G, then the identity function is an isomorphism between TS 1 = (G, Acc 1 ) and TS 2 = (G, Acc 2 ).

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

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

The ACD determines the type of transition systems Definition 6.7. Let TS be a Muller transition system with a set of states V . We say that its alternating cycle decomposition ACD TS is a:

Rabin ACD if for every state v ∈ V , the tree T v has Rabin shape. Streett ACD if for every state v ∈ V , the tree T v has Streett shape. Parity ACD if for every state v ∈ V , the tree T v has parity shape. [0, d -1]-parity ACD (resp. [1, d] Proof. (1 ⇒ 2) Let Acc R = (γ, Γ, Rabin(R) be the Rabin acceptance condition equivalent to Acc TS , and let R = (G 1 , R 1 ), . . . , (G r , R r ) be its Rabin pairs. Let l 1 and 2 be two cycles with a state in common, and suppose that 1 ∪ 2 is accepting; we show that either 1 or 2 is accepting. The cycle 1 ∪ 2 is accepted by some Rabin pair (G j , R j ), so for all edges e ∈ 1 ∪ 2 , γ(e) / ∈ R j , and there is some e 0 ∈ 1 ∪ 2 such that γ(e 0 ) ∈ G j . If e 0 belongs to 1 , then 1 is accepted by the Rabin pair (G j , R j ), and if e 0 ∈ 2 , then 2 is accepted by it.

(2 ⇒ 3) Let v be a vertex of TS and T v the local subtree at v. Suppose that there is a round node n ∈ T v with two different children n 1 and n 2 . The cycles ν(n 1 ) and ν(n 2 ) are rejecting cycles over v, but their union is an accepting cycle (by Remark 5.2). (3 ⇒ 1) We observe that ACD TS is a Rabin ACD if and only if rbw(T v ) = 1 for all vertices v of TS. In particular, the ACD-HD-Rabin-transform of TS does not add any state to TS.

It is immediate to check that the morphism ϕ : ACD Rabin (TS) → TS given by ϕ V (v, x) = v, ϕ E (e, l) = e defined in the proof of Proposition 5.25 is an isomorphism, and TS uses a Rabin acceptance condition. Proposition 6.10. Let TS = (G TS , Acc TS ) be a Muller transition system. The following conditions are equivalent:

1. TS is Streett type. 2.
For every pair of accepting cycles 1 , 2 ∈ Cycles(TS) with some state in common, 1 ∪ 2 is an accepting cycle. 13 3. ACD TS is a Streett ACD.

Proof. Implications (1 ⇒ 2) and (2 ⇒ 3) are analogous to those from Proposition 6.9.

(3 ⇒ 1) We consider the transition system TS obtained by complementing the acceptance set of Acc TS . By Remark 5.6, the ACD of TS is obtained from ACD TS by turning round nodes into square nodes and vice-versa. Thus, the ACD of TS is a Rabin ACD, and by applying the previous proposition we can define a Rabin condition Acc R = (γ, Γ, Rabin Γ (R)) such that the transition system (G TS , Acc R ) is isomorphic to TS. (2 ⇒ 3) Admits an analogous proof to the corresponding implication in Proposition 6.9.

(3 ⇒ 1) By definition, ACD TS is a parity ACD if and only if Leaves(T v ) is a singleton for each vertex v of TS. In particular, the ACD-parity-transform of TS does not add any state to TS. It is immediate to check that the morphism ϕ : ACD parity (TS) → TS defined in the proof of Proposition 5.18 is an isomorphism. Therefore, TS and ACD parity (TS) are isomorphic transition systems, and the latter uses a parity acceptance condition that is a [0, d -1] (resp. [1, d])-parity condition if ACD TS is a [0, d -1] (resp. [1, d])-parity ACD. If ACD TS is not a [0, d -1](resp. [1, d])-parity ACD, then the number of colours cannot be reduced by the optimality of the number of colours of the ACD-parity-transform (Theorem 5.31).

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

The ACD and the parity index of ω-regular languages Proposition 6.13. Let A be a deterministic Muller automaton whose states are accessible. Then, the parity index of L(A) is: trees of ACD A have height at most d, there is at least one positive tree of height d, and there is at least one negative tree of height d.

[0, d -1] (resp. [1, d]) if
Proof. We prove the right-to-left implication for the case Weak d . Suppose that ACD A verifies the previous list of conditions (in particular, it is equidistant). Then, the ACD-paritytransform ACD parity (A) is a DPA recognising L(A) using colours in [0, d]. In order to obtain a DPA for L(A) with colours in [1, d + 1] we need to introduce a small modification to the function p ACD . For i a maximal cycle of A and n ∈ N i we define:

p ACD (n) = Depth(n) + 2, if i is accepting, p ACD (n) = Depth(n) + 1, if i is rejecting.
It is a routine check to see that the version of the ACD-parity-transform using p ACD is indeed a correct parity automaton using colours in [1, d + 1].

To prove that no DPA recognising L uses less than d colours, it suffices to use the Flower Lemma 2.16 and the fact that a branch of length d in a tree of the ACD induces a d-flower in A, which is positive if and only if the corresponding tree is positive (Lemma 5.39). This is indeed a complete characterisation, since for any ACD there is a minimal d such that ACD A lies in one and only one of the classes specified in the statement of the proposition. Proposition 6.14. Let L ⊆ Σ ω be an ω-regular language of parity index at least [0, d -1] (resp. [1, d]). Any history-deterministic Muller automaton recognising L uses an acceptance condition with at least d different output colours.

Proof. We first prove the result for deterministic automata. Let A be a DMA recognising L using the acceptance condition (γ, Γ, Muller Γ (F)). By Proposition 6.13, there is a tree AltTree( i ) in the ACD of A of height at least d. We define γ ACD : Nodes(ACD TS ) → Γ to be the function that assigns to each node of the ACD the colours appearing in it, that is: γ ACD (n) = γ(ν(n)). We remark that if n is a descendant of n then γ ACD (n ) ⊆ γ ACD (n), and that a node n is round if and only if γ ACD (n) ∈ F. Therefore, by the alternation of round and square nodes, if n is a strict descendent of n, γ ACD (n ) γ ACD (n). We conclude that the root of AltTree( i ) must contain at least d different colours.

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

The following result (which was already known, as it is a consequence of the construction by Carton and Maceiras [15]), is refined and proven in Appendix A (Corollary A.16). Proposition 6.15. Let A be a deterministic parity automaton such that all its states are accessible and the parity index of L(A) is [0, d -1] (resp. [1, d]). Then, A is [0, d -1] (resp. [1, d])-parity type.

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

Typeness for deterministic automata

Two automata A 1 and A 2 such that A 1 A 2 recognise the same language: L(A 1 ) = L(A 2 ). However, the converse only holds for deterministic automata. Lemma 6.16. Let A 1 and A 2 be two deterministic automata over the same underlying graph and with the same labelling by input letters. Then,

L(A 1 ) = L(A 2 ) if and only if A 1 A 2 .
Proof. The implication from right to left is trivial. For the other implication, suppose that L(A 1 ) = L(A 2 ), and let ρ ∈ Run(A 1 ) = Run(A 2 ) be an infinite run over the underlying graph of A 1 . Let w ∈ Σ ω be the word over the input alphabet Σ labelling the run ρ. Since A 1 and A 2 are deterministic, ρ is the only run over w, and therefore:

ρ is accepting for A 1 ⇐⇒ w ∈ L(A 1 ) = L(A 2 ) ⇐⇒ ρ is accepting for A 2 .
Corollary 6.17 (First proven in [9,Theorem 7]). Let G A be the underlying graph of a deterministic automaton. There are Rabin and Streett conditions Acc R and Acc

S such that L(G A , Acc R ) = L(G A , Acc S ), if and only if there is a parity condition Acc p such that L(G A , Acc p ) = L(G A , Acc R ) = L(G A , Acc S ).
We remark that the hypothesis of determinism in the previous corollary is necessary, as it has been shown that an analogous result does not hold for non-deterministic automata [9]. Proposition 6.18 (First proven in [47,Theorem 15]). Let A be a deterministic Rabin (resp. Streett) automaton, and suppose that L(A) can be recognised by a deterministic Büchi (resp. coBüchi) automaton; that is, the parity index of L(A) is at most [0, 1] (resp. at most [1,2]). Then, A is Büchi type (resp. coBüchi type).

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

A normal form for parity transition systems

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

This normal form, or partial versions of it, have already been used in the literature to prove results about parity automata in different contexts, such as history-deterministic coBüchi automata [1,29,49], positionality of languages defined by deterministic Büchi automata [START_REF] Muller | Infinite sequences and finite machines[END_REF] or learning of DPAs [START_REF] Bohn | Constructing deterministic parity automata from positive and negative examples[END_REF]. This normal form also facilitates the resolution of parity games in practice [35]. However, the application of this normal form in the literature is limited to specific cases, and no prior studies have provided a formal and systematic analysis of it. Next definition constitutes a syntactic version of the parity index, defined at the level of parity transition systems. The following results establish the tight relation between the semantic notion of parity index and its syntactic counterpart. Definition 6.20. We say that a parity transition system TS = (G TS , Acc TS ) is parity-indextight if any other parity condition Acc over G TS such that Acc G T S Acc TS uses at least as many colours as Acc TS . Lemma 6.21 ([15]). Any parity transition system admits an equivalent parity acceptance condition making it parity-index-tight. Moreover, such an acceptance condition can be computed in polynomial time.

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

We say that a transition system TS is negative if ACD TS is negative, that is, if for some d TS contains a negative d-flower but contains no positive d-flower. Intuitively, a parity TS is negative if and only if the minimal colour used by a parity acceptance condition using an optimal number of colours is 1. Definition 6.22 (Normal form). Let TS = (G TS , Acc TS ) be a parity transition system using a colouring function γ. If TS is not negative, we say that TS is in normal form if any other parity acceptance condition equivalent to Acc TS over G TS using a colouring function γ satisfies that for every edge e: γ(e) ≤ γ (e).

If TS is negative, we say that it is in normal form if any other equivalent colouring γ not using colour 0 satisfies that for any edge e:

1 ≤ γ(e) ≤ γ (e).
If TS is in normal form, we will also say that its acceptance condition or the colouring function it uses are in normal form. Example 6.23. Parity transition systems from Figures 3,9, 16 and 17 are all in normal form. Parity automata appearing in Figures 9 and 16 are negative (the minimal colour used by an optimal acceptance condition is odd), whereas parity automata in Figure 17 are not.

On the other hand, the automaton from Figure 1 is not in normal form (even if it uses an optimal number of colours). We can put it in normal form by assigning colour 1 to transitions q 1 a,b --→ q 0 and q 1 b,c --→ q 2 . The automaton obtained in this way recognises the same language. minimal colour. We remark that, as ACD TS is a parity ACD, each edge e appears in one and only one branch of ACD TS , and that γ ACD (e) equals the depth of the deepest node containing e. In particular, if e ∈ ν(n) for some node e, γ ACD (e) ≥ Depth(n). Our objective is to show that a similar result holds for the path ρ as a set of edges: Claim 6.28.1. Let N ρ be the set of nodes of ACD TS containing the edges of the path ρ in their label, that is, N ρ = {n ∈ Nodes(ACD TS ) | {e 1 , . . . , e k } ⊆ ν(n)}. Then, min(γ ACD (ρ)) equals the depth of a node of maximal depth of N ρ .14

This claim allows us to conclude. Indeed, let n be a node of maximal depth of N ρ , verifying Depth(n) = d. Then, ν(n) is a cycle containing the vertices v and v , and for all the edges e ∈ ν(n), γ ACD (e) ≥ Depth(n) = d. This provides the desired path from v to v.

Proof of Claim 6.28.1. First, we remark that if 1 , 2 , . . . , k are cycles such that i and i+1 have some state in common, then ∪ k i=1 i is a cycle. Let n be a node of maximal depth in N ρ . By the previous remarks, γ ACD (e) ≥ Depth(n). Suppose by contradiction that γ ACD (ρ) > Depth(n). Then, each edge e i of ρ would appear in some strict descendant n i of n (we can suppose that n i is a child of n). Then, ν(n 1 ), . . . , ν(n k ) would be cycles such that ν(n i ) and ν(n i+1 ) have some state in common (namely, Target(e i ) = Source(e i+1 )), so their union is a cycle. However, this is not possible in a parity transition system, as ν(n) is accepting if and only if each of the ν(n i ) is rejecting (see Lemma 4.19). Proposition 6.29 (Normal flowers do not lack petals). Let v be a state of a parity transition system in normal form belonging to an accepting (resp. rejecting) SCC. Let ∈ Cycles v (TS) be a cycle over v and let d be the minimal colour appearing on it.

If TS is not negative, for each x ∈ [0, d ] (resp. x ∈ [1, d ]) there is a cycle x ∈ Cycles v (TS) producing x as minimal colour. If TS is negative, for each x ∈ [2, d ] (resp. x ∈ [1, d ]) there is a cycle x ∈ Cycles v (TS) producing x as minimal colour.

Proof. We do the proof for the case in which TS is not negative and v belongs to an accepting SCC. By Proposition 6.24, the colouring of TS is the one given by its ACD-transform, noted γ ACD . Consider the local subtree at v, T v , consisting in a single branch, as it has parity shape (Proposition 6.11). Let n 0 . . . n k be that branch, and let n i be the deepest node such that ⊆ ν(n i ). We remark that, by definition of γ ACD , d = Depth(n i ) = i. The desired cycles are obtained by taking

x = ν(n x ), for x ∈ [0, d ].

Parity index from automata in normal form

A refined version of the following result is proven in Appendix A (Corollary A.15), in which we give a full characterisation by using generalised weak automata. Corollary 6.30. Let A be a deterministic parity automaton in normal form such that all its states are accessible. If A uses colours in [0, d -1] (resp. [1, d]), then the parity index of

L(A) is Weak d-1 or [0, d -1] (resp. Weak d-1 or [1, d]).

Minimisation of deterministic parity automata recognising Muller languages

The minimisation of ω-automata is a fundamental problem of an intriguing complexity. In 2010, Schewe showed that the minimisation of deterministic Büchi and parity automata is NP-complete, if the acceptance condition is defined over the states [74]. However, the reduction of NP-hardness does not generalise to automata with edge-based acceptance.

A surprising positive result was obtained in 2019 by Abu Radi and Kupferman: we can minimise in polynomial time HD coBüchi automata using transition-based acceptance [1]. In this section, we provide a polynomial-time algorithm for the minimisation of DPA recognising Muller languages (with acceptance condition over transitions). By Proposition 4.10 and Theorem 4.13, we know that a minimal (history-)deterministic parity automaton recognising a Muller language L = Muller Σ (F) can be constructed in linear time from the Zielonka tree Z F . We will therefore provide a polynomial-time algorithm computing this Zielonka tree from a DPA recognising L. Theorem 6.31. Let A be a DPA recognising a Muller language L = Muller Σ (F). We can find a minimal deterministic (resp. history-deterministic) parity automaton recognising L in polynomial time in the size of the representation of A.15 Description of the algorithm. Let A = (Q, Σ, q 0 , Γ, ∆, parity) be a DPA recognising L = Muller Σ (F). We outline a recursive algorithm building Z F = (N, , ν) in a top-down fashion; it starts from the root of the tree (which is always labelled Σ), and each time that some node is added to N , we compute its children. If we have built Z F up to a node n, we compute the children of n by using the procedure AlternatingSets described in Algorithm 1, which we disclose next.

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

We include the pseudocode for the procedure AlternatingSets in Algorithm 1. We use the following notations: Letters(S) is the set of input letters appearing in S, MinColour(S) is the minimal output colour appearing in S (which determines whether Letters(S) ∈ F, if S is strongly connected), SCC-Decomposition(A) outputs a list of the strongly connected components of A. If A is empty, it outputs an empty list. MaxInclusion(lst) returns the list of the maximal subsets in lst. end if 13: end for 14: maxAltSets ← MaxInclusion(altSets) 15: return maxAltSets Correctness of the algorithm. Let n be a node of the Zielonka tree of F labelled with ν(n), and let A n be an accessible subautomaton of A over ν(n) recognising Muller ν(n) (F| ν(n) ). We prove that AlternatingSets(A n ) returns a list of sets corresponding to the labels of the children of n in Z F . We suppose without loss of generality that ν(n) ∈ F and therefore the minimal colour d in A n is even.

First, we observe that if X ⊆ Σ is added to altSets during the execution of the procedure AlternatingSets, then X is the set of input letters appearing in a cycle whose minimal colour is odd. Next lemma implies that in this case, X / ∈ F. In particular, no subset is added if n is a leaf of Z F . Lemma 6.32. Let A be a DPA such that L(A) = Muller Σ (F). Let ∈ Cycles(A) be an accessible cycle of A. Let Σ ⊆ Σ be the input letters appearing on , and let d be the minimal colour on . Then, Σ ∈ F if and only if d is even.

Proof. Since is an accessible cycle, there is a word w ∈ Σ ω such that Inf(w) = Σ and verifying that the edges visited infinitely infinitely often by the (only) run over w in A are the edges of . Therefore w ∈ L(A) if and only if d is even, and since L(A) is a Muller language, w ∈ L(A) if and only if Inf(w) = Σ ∈ F.

As the final output of the algorithm consists solely on the maximal subsets in altSets, and no accepting set is added to this list, it suffices to show that each maximal rejecting subset Σ max ⊆ ν(n) is added to altSets at some point.

Let Σ max ⊆ ν(n) be one of the maximal rejecting subsets of ν(n). Let S be a final SCC of the restriction of A n to transitions labelled with letters in Σ max (by the previous lemma, MinColour(S) is odd). We show that Σ max will eventually be considered by the recursive procedure AlternatingSets, and therefore Σ max will be added to altSets We use of the following remark: Claim 6.32.1. If S is a strongly connected subautomaton of A n such that S S ⊆ A n , then the minimal colour in S is even.

Proof. Let Σ be the input letters appearing in S . As S S and no transition labelled with a letter in Σ max leaves S, we must have Σ max Σ . The claim follows from Lemma 6.32.

Therefore, either S is one of the SCCs of A >d (in this case, Σ max is added to altSets in Line 9), or it is contained in one SCC of A >d whose minimal colour is even and we can conclude by induction.

Complexity analysis. We will show that the proposed algorithm works in O(|Q| 3 |Σ| 2 |Γ|), where Q, Σ and Γ are the states, set of input letters and set of output colours of the automaton, respectively. We remark that, since A is deterministic, |∆| ≤ |Q||Σ|.

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

We perform this operation for each node of the Zielonka tree. By the optimality of the ZT-parity-automaton (Theorems 4.12 and 4.13), we know that |Q| ≥ |Leaves(Z F )| and that the height of Z F is at most |Γ|. Therefore, |Z F | ≤ |Q||Γ|, and the procedure AlternatingSets is called at most |Q||Γ| times. We conclude that the proposed algorithm works in O(|Q| 3 |Σ| 2 |Γ|).

Conclusion

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

Optimal and practical transformations of automata. We have presented a transformation that, given a deterministic Muller automaton, provides an equivalent deterministic parity automaton, and another that provides an equivalent history-deterministic Rabin automaton. These transformations are optimal in a strong sense; the obtained automata have a minimal number of states amongst those which accept a history-deterministic mapping to the original Muller automaton. The first of these transformations has been implemented in the opensource tools Spot 2.10 [27] and Owl 21.0 [45], and it has been shown to perform extremely well in practice [START_REF] Büchi | On a decision method in restricted second order arithmetic[END_REF], as the natural definition of the ACD provides a fairly efficient way to compute the transformation, while its optimality guarantees to produce automata as small as possible.

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

On the other hand, we have shown that, if our objective is to obtain Rabin automata as output, the ACD-HD-Rabin-transform allows us to benefit from succinct HD automata. In this case, it has been shown that these automata can be exponentially smaller than equivalent deterministic ones [START_REF] Boker | History determinism vs. good for gameness in quantitative automata[END_REF]Theorem 21].

Disclosing the structure of ω-automata. As an application of the insights gained from the alternating cycle decomposition, we have derived results concerning typeness of automata.

In particular, we have characterised when we can define a parity, Rabin or Streett condition on top of a Muller automaton, obtaining an equivalent automaton (Propositions 6.9, 6.10 and 6.11). These characterisations have already been proven instrumental in works about the memory for games [17], and to obtain lower bounds for ω-automata [START_REF] Boker | History determinism vs. good for gameness in quantitative automata[END_REF].

We have also employed the ACD to present a normal form for parity transition systems and systematically prove the most important properties that make this form a valuable tool for manipulating parity automata. We believe that this normal form will be useful to extend existing results about Büchi and coBüchi automata (as the ones in [1,[START_REF] Niwiński | Relating hierarchies of word and tree automata[END_REF][START_REF] Muller | Infinite sequences and finite machines[END_REF]) to parity automata. We say that a language L ⊆ Γ ω is a generalised Büchi language if there is a family of sets B = {B 1 , . . . , B k } such that L = genBüchi Γ (B). Generalised coBüchi. Given k non-empty subsets B 1 , . . . , B k ⊆ Γ, we define the generalised coBüchi language associated to B = {B 1 , . . . , B k } as genCoBüchi Γ (B) = {w ∈ Γ ω | Inf(w) ∩ B i = ∅ for some i ∈ {1, . . . , k}}.

A Generalised classes of acceptance conditions

We say that a language L ⊆ Γ ω is a generalised coBüchi language if there is a family of sets B = {B 1 , . . . , B k } such that L = genCoBüchi Γ (B).

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

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

Generalised weak transition systems. Let TS = (G TS , Acc TS ) be a transition system using a parity condition Acc TS = (γ, [d min , d max ], parity). We say that TS is Weak d if in each strongly connected component S ⊆ G TS there are at most d different colours that appear, that is, |γ(E S )| ≤ d, where E S is the set of edges of S.

As for the rest of conditions, we say that a transition system TS is Weak d type if there exists an isomorphic parity transition system TS TS that is Weak d . The adjective Weak has typically been used to refer to the condition corresponding to a partition of TS into accepting and rejecting SCC. A run will be accepting if the component it finally stays in is accepting. It corresponds to Weak 1 with our notation.

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

The Zielonka tree of generalised acceptance conditions

Definition A.2. Let T be a tree T with nodes partitioned into round nodes and square nodes. We say that T has:

Parity index from automata in normal form

Corollary A.15. Let A be a deterministic parity automaton in normal form using colours in [0, d -1] (resp. [1, d]) such that all its states are accessible. If A is Weak d-1 , then the parity index of L(A) is Weak d-1 . If not, the parity index of L(A) is [0, d -1] (resp. [1, d]).

Proof. We suppose that A uses colours in [0, d -1] (in particular, it is not negative). If A in not Weak d-1 , there is a SCC containing all the colours [0, d -1]. By Proposition 6.29, such SCC contains a positive d-flower, so by the Flower Lemma 2.16, the parity index of L(A) is [0, d -1].

Suppose now that A is Weak d-1 . Let be a cycle of A in which the colour d -1 occurs. By Proposition 6.29, contains a negative (d -1)-flower. As A is not negative, it also contains a positive (d -1)-flower. By the Flower Lemma 2.16, the parity index of L(A) is Weak d-1 .

Corollary A.16. Let A be a deterministic parity automaton such that all its states are accessible and the parity index of L(A) is [0, d -1] (resp. [1, d] / Weak d ). Then, A is [0, d -1] (resp. [1, d] / Weak d )-parity type.

Proof. We suppose that L(A) has parity index [0, d -1] (the other cases are similar). By the Flower Lemma 2.16, A does not contain any negative d-flower. By Proposition 6.13, the trees of the ACD of A have height at most d, and trees of height d are positive. That is, ACD A is a [0, d -1]-parity ACD and we conclude by applying Proposition 6.11.

B Transformations for games

Games suitable for transformations

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

Restrict transformations of games to games in a standard form, which we have called games suitable for transformations. Add a restriction to HD mappings in the case of games, introducing the notion of HD-for-games mapping.

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

D Simplifying automata with duplicated edges

Given an automaton A = (Q, Σ, I, Γ, δ, W) we say that it has duplicated edges if there are some pair of states q, q ∈ Q and two different transitions between them labelled with the same input letter: q a:α --→ q , q a:β --→ q . As commented in Remark 4.44, the construction of the ZT-HD-Rabin-automaton we have presented potentially introduces duplicated edges, which can be seen as an undesirable property (even if some automata models such as the HOA format [2] allow them). We show next that we can always derive an equivalent automaton without duplicated edges. Intuitively, in the Rabin case, if we want to merge two transitions having as output letters α and β, we add a fresh letter (αβ) to label the new transition. For each Rabin pair, this new letter will simulate the best of either α or β depending upon the situation.

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

Proof. For the Rabin case, let A be an automaton that is otherwise as A except that instead of the transitions ∆ of A it only has one a-transition q a:x --→ q ∈ ∆ (with a fresh colour x per transition) per state-pair q, q and letter a ∈ Σ. That is, ∆ = {(q, a, x j , q ) : (q, a, y, q ) ∈ ∆ for some y}. The new Rabin condition {(G 1 , R 1 ), . . . , (G r , R r )} is defined as follows. For each transition q a:x --→ q :

x ∈ G i if q a:y --→ q ∈ ∆ for some y ∈ G i , x ∈ R i if for all q a:y --→ q ∈ ∆, y ∈ R i .

We claim that L(A ) = L(A). Indeed, if u ∈ L(A), as witnessed by some run ρ and a Rabin pair (G i , R i ), then the corresponding run ρ in A over u is also accepted by the Rabin pair (G i , R i ): the transitions of Inf(ρ) ∩ G i induce transitions of Inf(ρ ) ∩ G i and the fact that Inf(ρ) ∩ R i = ∅ guarantees that Inf(ρ ) ∩ R i = ∅.

Conversely, if u ∈ L(A ) as witnessed by a run ρ and Rabin pair (G i , R i ), then there is an accepting run ρ over u in A: such a run can be obtained by choosing for each transition q a:x --→ q of ρ where x ∈ G i a transition q a:y --→ q ∈ ∆ such that y ∈ G i , which exists by definition of A , for each transition q a:x --→ q where x / ∈ G i ∪ R i a transition q q,y --→ q ∈ ∆ such that y / ∈ R i , which also exists by definition of A , and for other transitions q a:x --→ q (that is, those for which x ∈ R i ) an arbitrary transition q a:y --→ q ∈ ∆. Since ρ is accepting, we have Inf(ρ ) ∩ G i = ∅ and Inf(ρ) ∩ R i = ∅, that is, ρ is also accepting.

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

We claim that L(A ) = L(A). Indeed if u ∈ L(A), as witnessed by some run ρ, the run ρ that visits the same sequence of states in A is accepting as witnessed by the transitions that occur infinitely often in ρ.

Conversely, assume u ∈ L(A ), as witnessed by a run ρ and a non-empty subset S t for each transitions t that occurs infinitely often in ρ such that t∈Inf(ρ) S t is accepting in A. Then there is an accepting run ρ over u in A that visits the same sequence of states as ρ and chooses instead of a transition t ∈ Inf(ρ) each transition in S t infinitely often, and otherwise takes an arbitrary transition. The set of transitions ρ visits infinitely often is exactly t∈Inf(ρ) S t , and is therefore accepting.

Finally, observe that in both cases, if A is HD, then the automaton A without duplicate edges is also HD since A is obtained from A by merging transitions. Indeed, the resolver r of A induces a resolver r for A by outputting the unique transition with the same letter and state-pair as r. By the same argument as above, the run induced by r is accepting if and only if the run induced by r is.

Example D.2. The ZT-HD-Rabin-automaton from Figure 13 has duplicated transitions. In Figure 18 we present an equivalent HD Rabin automaton without duplicates. For this, we have merged the self-loops in state 1 labelled with a and b respectively. We have added the output colours (αβ) and (θξ). The new Rabin pairs are given by: G β = {β, (αβ)}, R β = {α, λ, ξ, ζ}, G λ = {λ}, R λ = {α, β, (αβ), θ}. for each round node n ∈ N , we add a Rabin pair (G n , R n ). We let G n = Γ\ν(n). In order to define R n , we observe that n has at most one child n , and we define R n = ν(n)\ν(n ), for n the only child of n, if it exists, or R n = ν(n) if n has no children at all. This is, the pair (G n , R n ) accepts the sets of colours A ⊆ Γ that contain some of the colours that disappear in the step n → n and none of the colours appearing up in the tree. We show that Rabin(R) = Muller(F). Let A be a set of colours. If A ∈ F, let n be a maximal node (for ) containing A. It is a round node and there is some colour c ∈ A not appearing in the only child of n. Therefore, c ∈ G n and A ∩ R n = ∅. Conversely, if A / ∈ F, then for every round node n with a child n , either A ⊆ ν(n ) (and therefore A ∩ G n = ∅) or A ν(n) (and in that case A ∩ R n = ∅).

Figure 1

 1 Figure 1 An example of a history-deterministic automaton that is not deterministic. The acceptance set is W = {u ∈ {1, 2} ω | u contains finitely many 1s}. An arrow of the form q a,b:2

Büchi

  Figure 2Relations between subclasses of Muller languages. An arrow from a class X towards a class Y means that if a language L ⊆ Γ ω 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].

  we show three different types of automata over the alphabet Σ = {a, b} recognising the language L = {w ∈ Σ ω | w = ub ω or (w = ua ω and u 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.

Figure 3

 3 Figure 3 Different types of automata recognising the language L = {w ∈ Σ ω | w = ub ω or (w = ua ω and u has an even number of 'b's )}.

Figure 4

 4 Figure 4The (history-)deterministic parity hierarchy.

Figure 8

 8 Figure 8 Zielonka tree ZF for F = {{a, b}, {a, c}, {b}}.

Remark 4 . 6 .

 46 A node n in the Zielonka tree Z F verifies that p Z (n) is even if and only if ν(n) ∈ F. If Σ ∈ F, min F = 0 and max F equals the height of the Zielonka tree minus one. If Σ / ∈ F, min F = 1 and max F equals the height of the Zielonka tree.

Example 4 . 7 .

 47 The Muller language from Example 4.5 satisfies Σ / ∈ F. The values taken by the function p Z are represented at the right of the Zielonka tree in Figure8. We have p Z

Figure 9

 9 Figure9ZT-parity-automaton recognising the Muller language associated to F = {{a, b}, {a, c}, {b}}.

Theorem 4 .

 4 16 (Minimality of the Zielonka Tree automaton with respect to deterministic automata). Let A be a DPA recognising a Muller language Muller Σ (F). Then, |A parity Z F | ≤ |A|.

Lemma 4 . 20 .

 420 Let F ⊆ 2 Σ + be a family of subsets with Zielonka tree Z F = (N, , ν), and let A be a DPA recognising Muller Σ (F). Let n ∈ N be a node of the Zielonka tree of F, and let n 1 , n 2 ∈ Children Z F (n) be two different children of n. If S 1 and S 2 are two accessible ν(n 1 )-FSCC and ν(n 2 )-FSCC in A, respectively, then S 1 ∩ S 2 = ∅.

Lemma 4 .

 4 23.Let A be an automaton and (M, σ) a memory structure for A. The resolver implemented by (M, σ) is sound if and only if A and A σ M recognise the same language.

Lemma 4 .

 4 26. Let n ∈ N be a square node of the Zielonka tree of F (ν(n) / ∈ F), and let n 1 , n 2 ∈ Children Z F (n) be two different children of n. If S 1 and S 2 are two accessible ν(n 1 )-FSCC and ν

Figure 10

 10 Figure 10Letter game for the HD automaton from Figure1, recognising the Muller language associated to 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 (q1, b). In this example, Eve has a winning strategy corresponding to the resolver described in Example 2.3.

Example 4 .

 4 43.The ZT-HD-Rabin-automaton A Rabin Z F of the family F = {{a, b}, {a, c}, {b}} from Example 4.5 is shown on the right of Figure13. The Zielonka tree Z F appears on the left of the figure, and the labelling η : Leaves(Z F ) → {1, 2} is represented by the numbers below its branches.

Figure 13

 13 Figure[START_REF] Muller | Infinite sequences and finite machines[END_REF] On the left, the Zielonka tree of F = {{a, b}, {a, c}, {b}}. On the right, the ZT-HD-Rabin-automaton A Rabin Z F . Blue transitions correspond to those coming from leaf θ, and green ones to those originating from leaf ξ.

Figure 14

 14 Figure 14Transition system TS using a Muller acceptance condition given by F = {{c, d, e}, {e}, {g, h, i}, {l}, {h, i, j, k}, {j, k}}. The two maximal cycles, 1 and 2, are encircled by blue and red dashed lines, respectively.

  Cycles v (TS) +, as required by the definition of the Zielonka tree. To obtain a proper Zielonka tree with a labelling of nodes ν : Nv → 2Cycles v (TS) + , we would have to define ν

Theorem 5 .

 5 32. Let TS be a Muller TS whose states are accessible and let TS be a parity TS. If TS admits an HD mapping ϕ : TS → TS, then, |ACD parity (TS)| ≤ | TS|. Theorem 5.33. Let TS be a Muller TS whose states are accessible and let TS be a Rabin TS. If TS admits an HD mapping ϕ : TS → TS, then, |ACD Rabin (TS)| ≤ | TS|.

Corollary 5 .

 5 34. Let G be a Muller game suitable for transformations whose states are accessible and let G be a Rabin game. If G admits an HD-for-games mapping ϕ : G → G, then, |ACD game parity (G)| ≤ 2| G|.

  A Muller automaton with acceptance set given by F = {{α, β}}.

  A parity automaton recognising L with only 3 states .

Remark 6 . 19 .

 619 We remark that if Acc = (γ, [d min , d max ], parity) is a parity acceptance condition over a pointed graph G, we can always suppose that d min is 0 or 1. Indeed, define χ = d min if d min is even, and χ = d min -1 if d min is odd. The parity acceptance condition (γ , [d min -χ, d max -χ], parity) defined as γ (e) = γ(e) -χ is equivalent to Acc over G.

Algorithm 1

 1 AlternatingSets(A): Computing the children of a node 1: Input: A strongly connected automaton A over Σ such that L(A) = Muller(F) 2: Output: The maximal subsets Σ 1 , . . . , Σ k ⊆ Σ such that Σ i ∈ F ⇐⇒ Σ / ∈ F. 3: d ← MinColour(A) 4: A >d ← restriction of A to transitions ∆ >d = {q a:x --→ q ∈ ∆ | x > d} 5: S 1 , . . . , S r ← SCC-Decomposition(A >d ) 6: altSets ← {} 7: for i = 1, . . . ,r do 8: if MinColour(S i ) is odd if and only if d is even then 9:altSets ← altSets ∪ {Letters(S i )}

  Given k non-empty subsets B 1 , . . . , B k ⊆ Γ, we define the generalised Büchi language associated to B = {B 1 , . . . , B k } as genBüchi Γ (B) = {w ∈ Γ ω | Inf(w) ∩ B i = ∅ for all i ∈ {1, . . . , k}}.

Figure 18 3 .

 183 Figure 18The simplified ZT-HD-Rabin-automaton.

  are exactly coloured transitions of TS. Finally, let (e 1 , e 2 ) and (e 1 , e 2 ) in Out(v, q) ∩ E col . Their ϕ(e 1 , e 2 ) = ϕ(e 1 , e 2 ) if and only if e 1 = e 1 .

  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 γ (ρ ). Moreover, we proved that ρ is accepting in A parity Z F if and only if n w is round. Lemma 4.46 allows us to conclude that ϕ Runs (ρ) is accepting in A Rabin

	accepting in A parity Z F .	Z F	if and only if ρ is

Proof of Proposition 4.45. L(A

Rabin Z F ) ⊆ Muller Σ (F): Let w ∈ L(A Rabin Z F

  -1 ,v ) is accepting if and only if Unfold(ρ) is accepting. If L = Muller Γ (F) is a parity (resp. Rabin) language, then, so is the language L = Muller 2 Γ + ( F ) used by the acceptance condition of A (ϕ -1 ,v ) . Proof. Suppose that L is a parity language, that is, there are d min ≤ d max and φ : Γ → [d min , d max ] such that for any non-empty subset C ⊆ Γ, C ∈ F if and only if min φ(C) is even. We define φ : 2 Γ + → [d min , d max ] as: φ(C) = min φ(C). It is immediate to see that {C 1 , . . . , C k } ∈ F if and only if min φ({C 1 , . . . , C k }) is even.

	Lemma 5.43.

.

  Rabin shape if every round node has at most one child. Streett shape if every square node has at most one child. Parity shape if every node has at most one child. Muller Γ (F) is a Streett language. 2. The family F is closed under union. 3. Z F has Streett shape.

	Proposition 6.2. Let F ⊆ 2 Γ + be a family of non-empty subsets. The following conditions
	are equivalent:
	1. Muller Γ (F) is a Rabin language.
	2. 2 Γ + \ F is closed under union: If C 1 / ∈ F and C 2 / ∈ F, then C 1 ∪ C 2 / ∈ F.
	3. Z F has Rabin shape.
	Proposition 6.3. Let F ⊆ 2 Γ + be a family of non-empty subsets. The following conditions
	are equivalent:
	1Proposition 6.4. Let F ⊆ 2 Γ + be a family of non-empty subsets. The following conditions
	are equivalent:
	1. Muller Γ (F) is a parity language.
	2. Both F and 2 Γ + \ F are closed under union

  -parity ACD) if it is a parity ACD, trees of ACD TS have height at most d and trees of height d are positive (resp. negative). 6.8. ACD TS is a parity ACD if and only if it is both a Rabin and a Streett ACD. Let TS = (G TS , Acc TS ) be a Muller transition system whose states are accessible. The following conditions are equivalent: 1. TS is Rabin type. 2. For every pair of rejecting cycles 1 , 2 ∈ Cycles(TS) with some state in common, 1 ∪ 2 is a rejecting cycle. 3. ACD TS is a Rabin ACD.

	Remark Proposition 6.9.

  Since Streett Γ (R) is the complement language of Rabin Γ (R), we obtain that Acc S = (γ, Γ, Streett Γ (R)) is a Streett acceptance condition equivalent to Acc TS over G TS . Let TS = (G TS , Acc TS ) be a Muller transition system. The following conditions are equivalent:1. TS is parity type. 2.For every pair of accepting (resp. rejecting) cycles 1 , 2 ∈ Cycles(TS) with some state in common, 1 ∪ 2 is an accepting (resp. rejecting) cycle.3. ACD TS is a parity ACD.Moreover, if some of the conditions is satisfied, TS is [0, d -1] (resp.[1, d])-parity type if and only if ACD TS is a [0, d -1](resp.[1, d])-parity ACD.

	Proposition 6.11.

Proof. (1 ⇒ 2) Proven in

Lemma 4.19.

  and only if: trees of ACD A have height at most d, there is at least one tree of height d, and trees of height d are positive (resp. negative). This property was introduced by Le Saëc under the name cyclically closed automata [71]. We point

	Weak d if and only if:

13

out that the "if" direction of the result stated in [71,

Theorem 5.2]

does not hold. That statement can be rephrased as: If a DMA A is cyclically closed, then the parity index of A is [0, 1]. We refer to Proposition 6.13 for a correct characterisation.

  Schewe showed that the minimisation was again NP-hard for HD automata with state-based acceptance[75]. To the best of our knowledge, the only existing hardness result applying to transition-based automata is Casares' result about the NP-completeness of the minimisation of deterministic Rabin automata[17]. In fact, in [17] a stronger result is proven: it is NP-hard to minimise deterministic Rabin automata recognising Muller languages.

  Büchi shape if it has a single branch, height at most 2, and if it has height 2 its root is round. coBüchi shape if it has a single branch, height at most 2, and if it has height 2 its root is square. Generalised Büchi shape if it has height at most 2, and if it has height 2 its root is round. Generalised coBüchi shape if it has height at most 2, and if it has height 2 its root is square. Let F ⊆ 2 Γ + be a family of non-empty subsets. Then Muller Γ (F) is a Büchi (resp. coBüchi) language if and only if Z F has Büchi (resp. coBüchi) shape.

	Proposition A.3.

The optimality of the Zielonka-tree-parity-automaton amongst deterministic automata has also been obtained in the independent unpublished work[59].

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).

Sometimes in the literature[7,[START_REF] Casares | Optimal transformations of games and automata using Muller conditions[END_REF][START_REF] Boker | When a little nondeterminism goes a long way: An introduction to history-determinism[END_REF] the initial state r0 is not required to be specified. This would permit to choose it after the first letter w0 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 r0 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).

The choice of the leftmost leaf is arbitrary. In all our uses of the function Jump, it could be replaced by any leaf below n2.

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 A recognises the same language than B, if A is not historydeterministic (Proposition 2.6). In that case, the equality L(B A) = L(B) follows from the idea that runs in B can be simulated in B A "guided by the non-deterministic choices of A", which we do not formalise in this work.

The definition of Z F , as well as most subsequent definitions, do not only depend on F but also on the alphabet Σ. 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.

Any non-empty subset of Q can be chosen as the set of initial states.

The colours associated to transitions changing of SCC are almost arbitrary (we could even leave them uncoloured). We define them to be the minimal colour used so that the obtained transition system is normalised in the sense of Section 6.2.

Here we use a slight abuse of notation, since, formally, rϕ takes as input elements in E * ×E , but ρ ∈ E * . We can naturally extend rϕ to E * by induction. Equivalently, we can say that r A (e1e2 . . . e k , ) is a suffix of rϕ,Runs (ρ 0 ρ 1 . . . ρ k ρ ).

In fact, the nodes of Nρ are totally ordered by the ancestor relation, so there is a unique node of maximal depth in Nρ. This fact is not used in our proof.

We can suppose that the representation of A has size polynomial in |Q| + |Σ|, where Q and Σ are the set of states and the input alphabet of. Indeed, as A is deterministic the number of transitions is at most |Q| • |Σ| and we can suppose that A has no more output colours than transitions.

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.

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).

https://drops.dagstuhl.de/opus/volltexte/2021/14192/ We incorporate results from [START_REF] Boker | History determinism vs. good for gameness in quantitative automata[END_REF]: https://drops.dagstuhl.de/

Corollary 5.35. Let TS be a Muller TS. A minimal parity TS admitting an HD mapping to TS has the same size than a minimal parity TS admitting a locally bijective morphism to TS.

Corollary 5.36. Let A be a history-deterministic parity automaton. Suppose that there exists a DMA B such that A admits an HD mapping to B. Then, there exists a DPA A recognising L(A) such that |A | ≤ |A|.

Both corollaries follow from an immediate application of Theorem 5.32.

The ACD-transform does not preserve minimality. A natural question is whether the ACD-parity-transform preserves minimality of automata, that is, given a DMA A with a minimal number of states for the language it recognises, is ACD parity (A) minimal amongst DPAs recognising L(A)? 11 The answer to this question is negative, as we show now.

Proposition 5.37. There exists a DMA A that is minimal amongst DMAs recognising L(A), but such that its ACD-parity-transform ACD parity (A) is not a minimal DPA.

We consider the alphabet Σ = {a, b, c} and the language L = {w ∈ Σ ω | c ∈ Inf(w) and w contains infinitely often the factor ab}.

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

Optimality of the parity condition of ACD parity (TS)

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

Let TS = (G, Acc) and TS = (G , Acc ) be transition systems with underlying graphs G = (V, E, Source, Target, I) and G = (V , E , Source , Target , I ), and acceptance conditions Acc = (γ, Γ, W) and Acc = (γ , Γ , W ). A weak morphism of transition systems ϕ : TS → TS provides a labelling of the edges of TS by ϕ E : E → E . Therefore, we can see TS as an automaton with input alphabet E , inheriting the underlying graph and acceptance condition from TS. We say that this is the automaton of morphism ϕ and denote it by A ϕ .

We define the language of accepting runs of a transition system TS as:

Lemma 5.38. Let TS and TS be transition systems with a single initial state, let ϕ : TS → TS be a weak morphism of transition systems, and let A ϕ be its automaton. Then, ϕ is an HD mapping if and only if the automaton A ϕ is history-deterministic, and, in this case, L(A ϕ ) = L Runs (TS ). Proposition 6.24. Let TS = (G TS , Acc TS ) be a parity transition system with a colouring function γ. There is a unique parity acceptance condition equivalent to Acc TS over G TS in normal form. Moreover, this acceptance condition is exactly the parity condition of the ACD-parity-transform of TS.

Before showing the proof of Proposition 6.24, we prove a useful technical lemma. Lemma 6.25. Let TS be a parity transition system with colouring function γ.

Proof. We show the result for negative flowers. Let d i = min γ( i ). We show that d i ≥ i by induction. Since i is an accepting cycle if and only if i is even, we have that d i is even if and only if i is even. Clearly, d 1 ≥ 1, as 1 is the least odd number. Also, d i+1 ≥ d i , since i+1 ⊆ i , and the inequality is strict by the alternation of the parity, concluding the proof.

Proof of Proposition 6.24. We first remark that the uniqueness is directly implied by the definition of normal form.

We prove that the acceptance condition of the ACD-parity-transform is in normal form. We note its colouring function by γ ACD . The transitions not belonging to any SCC are coloured 0 if TS is not negative and 1 if TS is negative, as desired. It suffices to prove the result for edges in SCCs.

We suppose that TS is not negative and we let S be an accepting SCC of TS (the proof is similar for TS negative and a rejecting SCC). Let e = v -→ v be an edge in S, and let T v be the local subtree at v, which is composed of a single branch (see Proposition 6.11). We let n 0 n 1 . . . n r be that branch, where n 0 is the root and n r the leaf . Let n k be the deepest node of T v such that e ∈ ν(n k ). By definition of the ACD-parity-transform, γ ACD (e) = p ACD (e) = k. Also, ν(n 0 ) ν(n 1 ) . . . ν(n k ) is a positive k + 1-flower (by Lemma 5.39). Lemma 6.25 implies then that any equivalent parity condition using a colouring function γ verifies γ (e) ≥ γ ACD (e) = k. Corollary 6.26. The ACD-parity-transform ACD parity (TS) of any Muller transition system TS is in normal form.

We can deduce that the optimality properties of the colouring of ACD parity (TS) (Theorem 5.31) transfer to parity transition systems in normal form. Corollary 6.27. A parity transition system in normal form is parity-index-tight.

We now state what we consider to be the two fundamental properties of parity transition systems in normal form. Proof. We do the proof for the case generalised Büchi (symmetric for generalised coBüchi). Suppose that Muller Γ (F) = genBüchi Γ (B) for some family B = {B 1 , . . . , B k }. Then, Γ ∈ F, as Γ ∩ B i = ∅, so the root of Z F is round. If C ⊆ Γ is rejecting, C ∩ B i = ∅ for all i, then it the same for any subset C ⊆ C, so square nodes of Z F are leaves and Z F has height at most 2.

Conversely, suppose that Z F has height 2 and that its root is round (Γ ∈ F). Let A 1 , . . . , A k be the labels of the k leaves of Z F and define

Corollary A.5. Let A be a deterministic generalised Büchi (resp. generalised coBüchi) automaton recognising a Muller language L = Muller Σ (F). There is a deterministicgeneralised Büchi (resp. generalised coBüchi) automaton recognising L with just one state, that can be computed in polynomial time in the size of the representation of A.

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

The acceptance condition of such automaton can be deduced in linear time from the Zielonka tree Z F , as indicated in the proof of Proposition A.4. The Zielonka tree Z F can be computed from the original automaton A using a similar argument than in the proof of Theorem 6.31. Suppose that the generalised Büchi condition used by A is given by the sets B 1 , . . . , B k ⊆ Γ. Then, for each i ∈ {1, . . . , k} we compute the restriction of A to the transitions using colours in Γ \ B i , and perform a decomposition in SCCs of the obtained graph. If Σ S ⊆ Σ is the set of input letters appearing in one of those SCC, then Σ S / ∈ F. We put all the subsets of letters obtained in that way in a list altSets. The leaves of Z F correspond then to the maximal subsets of altSets.

ACD and typeness for generalised acceptance conditions

Definition A.6. Let TS be a Muller transition system with a set of states V . We say that its alternating cycle decomposition ACD TS is a: Proof. This is a special case of Proposition 6.11. Proposition A.9. A transition system TS is generalised Büchi (resp. generalised coBüchi) type if and only if ACD TS is a generalised Büchi ACD (resp. generalised coBüchi ACD).

Proof. The result follows by applying the same argument and construction than in Proposition A.4, using as set of output colours the set of edges of TS.

Proposition A.10. A transition system TS is Weak d type if and only if ACD TS is a Weak d ACD.

Proof. Proposition 6.11 already provides that TS is parity type if and only if ACD TS is a parity ACD. As in the proof of the aforementioned proposition, we observe that TS and ACD parity (TS) are isomorphic. If ACD TS is a Weak d ACD, then ACD parity (TS) is Weak d . Conversely, if ACD TS is not a Weak d ACD, then TS contains a (d + 1)-flower, so the number of colours cannot be reduced (using the same argument as in the proof of Theorem 5.31).

Corollary A.11. If L ⊆ Σ ω is an ω-regular language of parity index Weak d , then L can be recognised by a deterministic Weak d automaton.

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

The following result generalises [START_REF] Boigelot | On the use of weak automata for deciding linear arithmetic with integer and real variables[END_REF]Theorem 2].

Corollary A.12. A Muller transition system is Weak d type if and only if it is both [0, d] and [1, d + 1]-parity type.

Deterministic automata using generalised acceptance conditions

Corollary A.13. Let G A be the underlying graph of a deterministic automaton. There are [0, d -1] and [1, d]-parity conditions Acc p,0 and Acc p,

Proposition A.14. Let A be a deterministic Muller automaton, and suppose that L(A) can be recognised by a deterministic Büchi (resp. coBüchi) automaton; that is, the parity index of L(A) is at most [0, 1] (resp. at most [1,2]). Then, A is generalised Büchi type (resp. generalised coBüchi type).

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

Adam chooses an uncoloured transition leading to a vertex controlled by Eve (with only one ingoing transition), and then Eve picks a transition producing some output colour.

We recall that a game is suitable for transformations if it verifies that for every edge e = v -→ v , if v is controlled by Adam, then e is uncoloured (γ(e) = ε), v ∈ V Eve , and e is the only incoming edge to v (In(v ) = {e}).

Games in this form have an asymmetric structure that makes them suitable for any type of transformation. As any pair of consecutive transitions are of the form v ε -→ ṽ c -→ v , with ṽ ∈ V Eve , we can force it so that if a decision needs to be made in a product, Eve is the one who makes it.

Lemma B.1. For every game G with vertices V and edges E, there exists a game G that is suitable for transformations, of size | G| = O(|E|), and equivalent to G in the following sense: there is an injective function f : V → V such that Eve wins G from v if and only if she wins G from f (v).

Proof. We define G as follows. We let its set of vertices be V = V ∪ E. Vertices of the form v ∈ V will correspond to vertices coming from G, and vertices e ∈ E will be intermediate vertices added to force the suitability for transformations property. We let

ACD-HD-Rabin-transform-for-games

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

Let G be a game. If there is an edge v -→ v with v ∈ V Adam , we say that v is an A-successor. We remark that if G is suitable for transformations, an A-successor is controlled by Eve and has a unique predecessor. We let V A-succ be the set of A-successor of G and V normal = V \ V A-succ . If G is suitable for transformations, for each v ∈ V A-succ we let pred(v) be its unique predecessor.

The idea to define the ACD-HD-Rabin-transform-for-games ACD game parity (G) is the following: starting from the regular ACD-HD-Rabin-transform ACD Rabin (G), we make some local changes to vertices that are A-successors. First, if v ∈ V Adam , we replace edges of the form (v, x)

That is, Eve chooses retroactively how to update the ACD-components performing two consecutive updates. We note that the node n is not output in the new game; this is not a problem, since n must be an ancestor of n (we could say that n contains more information regarding the acceptance condition). T v is a subtree of T v .

Definition B.3 (ACD-HD-Rabin-transform-for-games).

Let G be a Muller game suitable for transformations. For each vertex v ∈ V we let η v : Leaves(T v ) → {1, . . . , rbw(T v )} be a mapping satisfying Property ( ) from Lemma 4.39. We define the ACD-HD-Rabin-transformfor-games of G to be the Rabin transition system ACD game parity (G) defined as follows. Vertices. The set of vertices is

Players partition. A vertex (v, x) belongs to Eve if and only if v belongs to Eve in G.

Initial vertices. I

Edges and output colours. Let

) to ACD game parity (G) exactly in the same cases as in the regular ACD-HD-Rabin-transform.

if in the regular ACD-HD-Rabin-transform there is a path of size 2 of the form

Formally,

, where G n and R n are defined as follow:

Let n be a round node, and let n be any node in Nodes(ACD TS ),

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

Proposition 5.29 (Correctness of the ACD-HD-Rabin-transform-for-games). Let G be a Muller game suitable for transformations, and let ACD game parity (G) be its ACD-HD-Rabin-transform-forgames. There is an HD-for-games mapping ϕ : ACD game parity (G) → TS. Proof. The proof is analogous to that of the correctness of the regular ACD-HD-Rabintransform (Proposition 5.25). We define the mapping ϕ :

It is clear that it is a weak morphism, and it preserve accepting runs by Lemma 5.26 and Remark B.2. We define a resolver (r 0 , r) simulating ϕ in a similar way as in the proof of Proposition 5.25: We use ACD parity (G) to guide the resolver. Let ρ = v 0 -→ v 1 re . . . be a run in G, and let (v 0 , l 0 ) -→ (v 1 , l 1 ) -→ . . . be the preimage of this run in ACD parity (G). We simulate ρ in ACD game parity (G) as follows: We ensure that at every moment i,

There distinguish two cases to simulate the edge

This must be the edge picked by the resolver

) such that x i+1 = η li+1 and n i = Supp(l i , e i ). This is indeed an edge appearing in ACD game parity (G), as the path (v i-1 , x i- 1)

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

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

Corollary 5.34. Let G be a Muller game suitable for transformations whose states are accessible and let G be a Rabin game. If G admits an HD-for-games mapping ϕ : G → G, then,

Proof. The vertices of ACD game parity (G) corresponding to vertices in V normal are exactly the same that those in ACD Rabin (G):

Moreover, for v ∈ V A-succ , there is one vertex of the form (v, x) for each vertex (pred(v), x), and each v ∈ V A-succ has exactly one predecessor in V normal , so we conclude that:

where the last inequality follows from Theorem 5.33.

C Simplifications for prefix-independent conditions

We prove in this appendix results applying to automata recognising prefix-independent languages and games using prefix-independent winning conditions. We recall that a language L ⊆ Σ ω is prefix-independent if for all w ∈ Σ ω and u ∈ Σ * , uw ∈ L if and only if w ∈ L.

Lemma 2.5. Let 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 A that is reachable using some sound resolver, it is verified that A recognises the same language if we fix q as initial state, that is, L(A) = L(A q ). Moreover, A q is also history-deterministic. In particular, if A is deterministic, this is the case for any reachable state q.

Proof. Let (r 0 , r) be a sound resolver for A such that q is reachable using (r 0 , r) (there is a word w 0 ∈ Σ * and a run ρ 0 = r 0 w0 q induced by r over w). We first show that L(A q ) ⊆ L(A). Let w ∈ Σ ω be a word accepted from q. Then, w 0 w admits an accepting run from the original initial state (by prefix-independence of the acceptance set), so w 0 w ∈ L(A), and by the prefix-independence of L(A), w ∈ L(A) too.

For the converse direction, we define a sound resolver (r 0 , r ) for A q . We let r 0 = q, and r (ρ, a) = r(ρ 0 ρ, a) be the strategy that acts as the resolver r assuming that ρ 0 has happened in the past. It is clear that for every word w ∈ Σ ω , the run induced by (r 0 , r ) over w has a common suffix with the run induced by (r 0 , r) over w 0 w. Therefore, by the prefix-independence assumptions: w ∈ L(A) ⇐⇒ w 0 w is accepted using (r 0 , r) ⇐⇒ w 0 w is accepted using (r 0 , r ). Lemma 3.14. Let TS and TS be two TS such that all their states are accessible, and let ϕ : TS → TS be an HD (resp. HD-for-games) mapping between them. If W and W are prefix-independent, the mapping ϕ is also HD (resp. HD-for-games) when considered between the transition systems TS V and TS V , consisting of the transition systems TS and TS where all the states are set to be initial.

Proof. First, ϕ : TS V → TS V is trivially a weak morphism. We claim that it preserves accepting runs. Let v ∈ V be a state in TS and let ρ = v w be an accepting run from v.

Since all the states are reachable, there is some v 0 ∈ I and finite run

where the central implication follows from the fact that ϕ preserves accepting runs between TS and TS . Therefore ϕ Runs (ρ) is also an accepting run.

In the rest of the proof we suppose that ϕ is an HD-for-games mapping, (which covers the HD case). Let (r Init , r) be a resolver sound for TS simulating ϕ : TS → TS . We define a resolver (r Init , r) for the new mapping. For every state v of TS, we fix a finite run ρ v ∈ Path fin I (TS) ending in v that is consistent with (r Init , r) over some ρ , if such a run exists. We let V Reach ⊆ V be the set of vertices for which ρ v is well-defined. We note that for each v ∈ V there exists at least one v ∈ ϕ -1 (v ) such that v ∈ V Reach ; indeed, if ρ v is a finite run reaching v in TS , one such v is Target(r Runs (ρ v )) (that is, the vertex to which we arrive in TS when simulating ρ v via the original resolver). We let rInit (v ) be this vertex. If e ∈ Out(v ) is an edge in TS , we let r(ε, e ) = r(ρ v , e ), for v = rInit (v ). For ρ a non-empty finite run starting in v ∈ V Reach and e ∈ E , we define r(ρ, e ) = r(ρ v ρ, e ). If ρ starts in v / ∈ V Reach we let r(ρ, e ) be any edge in ϕ -1 (e ) (if e ∈ Out(ϕ(Target(ρ))) we pick it in Out(Target(ρ))). We check that (r Init , r) satisfies the four requirements to be a resolver:

1. rInit (v ) has been chosen in ϕ -1 (v ). 2. r(e ) is chosen in ϕ -1 (e ). 3. Let e ∈ Out(v ). We have defined r(ε, e ) = r(ρ v , e ), where ρ v is a finite run consistent with r ending in v = r Init (v ). By Property 4 of a resolver, r(ρ v , e ) ∈ Out(v).

Let

r(ρ v0 ρ, e ); as ρ v0 ρ is a run ending in v and r verifies Property 4 of a resolver r(ρ v0 ρ, e ) ∈ Out(v).

Finally, we show that (r Init , r) is sound for TS. Let ρ = v w ∈ Run(TS V ) be an accepting run, and let ρ = v w be a run consistent with (r Init , r) over ρ . In particular, v = rInit (v ). Let ρ v = v 0 u v be the chosen run reaching v and let ρ v = v 0 u v be a finite run in Run fin (TS ) such that ρ v is consistent with (r Init , r) over ρ v . It is immediate to check that ρ v ρ is consistent with (r Init , r) over ρ v ρ . Since ρ is accepting, we have that w ∈ W , and by prefix-independence of the acceptance sets and the fact that ρ v ρ is accepting if ρ v ρ is, we have:

We remark that this construction uses more Rabin pairs than necessary, since we could reuse Rabin pairs for nodes that are in the same level and that are not siblings.

Conversely, suppose that Muller(F) = Rabin(R) for the Rabin language associated to R = {(G 1 , R 1 ), . . . , (G r , R r )}. If n ∈ Z F is a round node (A = ν(n) ∈ F), then its label A contains some colours that belongs to G i1 , . . . , G i k and none belonging to R i1 , . . . , R i k for some i 1 , . . . , i k , k ≥ 1. A child of n must not have these colours, so the only maximal subset of A that is not in

Proof of Proposition 6.4. We suppose Γ ∈ F (min F = 0), the other case is symmetric.

Suppose that Z F has a single branch of length max F +1. We define a mapping φ : Γ → [0, max F ] as follows: for each colour c ∈ Γ we let n c be the deepest node in Z F containing c, and we define φ(c) = ν(n c ). It is easy to check that for all w ∈ Γ ω , w ∈ Muller(F) if and only if φ(w) ∈ parity.

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