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.

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

§ 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 <cit.> 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 <cit.> using automata and games devised more than four decades ago is still at the heart of the state of the art synthesis tools <cit.>.
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 <cit.>, Strix <cit.> and  <cit.>)  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" <cit.>. 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 $\oo$-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" <cit.>, 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, -complete <cit.> and -complete <cit.>. From a theoretical point of view, "parity conditions" can be considered as the simplest family of conditions that can be used to "recognise" all "$\oo$-regular languages" with "deterministic" "automata"; it could even be argued that there is a canonical aspect to them:

* For every "$\oo$-regular language" $L$, the minimal number of "output colours" needed by "deterministic" "Muller" "automata" to "recognise" $L$ is attained with "parity" "automata" (Proposition <ref>). 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$ <cit.>.

* "Parity languages" are exactly "Muller languages" corresponding to families $\F\subseteq \powplus{\GG}$ of subsets of "colours" such that both $\F$ and its complement are closed under union (Proposition <ref>).

* "Parity languages" are bipositional <cit.> (in a "parity" "game", both players can play optimally using positional "strategies", that is, "strategies" that use no "memory@@game"). Moreover, over infinite "game graphs", these are the only bipositional languages <cit.>, and over finite "game graphs", these are the unique bipositional "Muller languages" <cit.>.

* Solving "parity" "games" is both in $\NP$ and $\coNP$ <cit.>.

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" <cit.>, there exists a correspondence between "Rabin" "automata" and "memory structures" for "Muller" "games" <cit.>, and the determinisation of "Büchi" "automata" naturally produces "Rabin" "automata" <cit.>.

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 <cit.> and is known as the Latest Appearance Record (LAR).
Löding proved that the LAR is optimal in the worst case <cit.>: 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" <cit.>.
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 <cit.>. 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" $\pp\colon \B \to \A$ that sends states of the form $(q, x)$ to $q$. A theory of "morphisms" of "transition systems" is developed in Section <ref>.

History-deterministic automata.
For the purposes of LTL synthesis and "game" transformations, it is imperative to eliminate "non-determinism" from "automata", since "non-deterministic" "automata" do not yield correct "games". Unfortunately, "deterministic" automata can be exponentially larger than "non-deterministic" ones.
Recently, an intermediate model of "automata", named "history-deterministic" (also called good-for-games), has received considerable attention. The reason is that "history-determinism" exactly captures the features of "deterministic" "automata" that make them suitable for synthesis purposes, while being a less restrictive model.
A natural question that arises is whether "history-deterministic" "automata" can be more succinct that "deterministic" ones, and, in that case, which languages and automata types can benefit from this succinctness. It was not until several years after the introduction of "history-determinism" <cit.> that an example of an "$\oo$-regular language" for which "history-deterministic" "automata" are smaller than "deterministic" ones was exhibit <cit.> (and it was even conjectured that such "automaton" could not exist <cit.>).
"History-deterministic automata" are the focus of several lines of research (we refer to the survey <cit.> 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 <cit.>.

The Zielonka tree and the alternating cycle decomposition.
The starting point of our work is the notion of "Zielonka tree", introduced by Zielonka <cit.> 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" <cit.>, and, most importantly, it characterises their exact "memory requirements", both in two-player games <cit.> and stochastic games <cit.>.

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

§.§ Contributions

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

1. Minimal automata for Muller languages. The basis on which we build up our work is a study of minimal automata "recognising" "Muller languages". Using the "Zielonka tree", we propose a construction of a "deterministic" "parity" automaton "recognising" a "Muller language" (Section <ref>). This construction implicitly appears in the long version of <cit.>. 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 <ref>). Moreover, it uses the optimal number of "output colours" to "recognise" $L$ (Theorem <ref>).  The optimality result we obtain is much stronger than the worst case optimality result of the LAR transformation <cit.>, 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 <ref>).
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 <ref>), and prove that this automaton is minimal amongst "history-deterministic" "Rabin" automata (Theorem <ref>). 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".

The optimality of the "Zielonka-tree-parity-automaton" amongst "deterministic" automata has also been obtained in the independent unpublished work <cit.>.

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 <ref>). Intuitively, a morphism $\pp\colon \B\to \A$ witnesses the fact that $\B$ has been obtained from $\A$ by blowing up each state $q\in \A$ to the states in $\inv{\pp}(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$.

3. The alternating cycle decomposition and optimal transformations of Muller transition systems. In order to generalise the fruitful applications of the "Zielonka tree" to "Muller" "automata" and "games", we introduce the "alternating cycle decomposition" (ACD), a data structure that captures the interplay of the "underlying graph" of these "transition systems" and their "acceptance condition"  (Section <ref>). 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" $\pp\colon \B\to \A$). This transformation comes with a strong optimality guarantee: for any other "parity" "automaton" $\B'$ admitting a "locally bijective morphism" (or even "HD mapping") $\pp'\colon \B'\to \A$, the automaton $\B$ is smaller than $\B'$ and it uses less "output colours" (Theorems <ref> and <ref>).
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" $\Lang{\B}$, then $\B$ cannot be derived from a "deterministic" "Muller" "automaton" (Corollary <ref>). 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 "history-deterministic" "Rabin" "automaton" $\B$ in an optimal way: for any other "Rabin" "automaton" $\B'$ admitting an "HD mapping" $\pp'\colon \B'\to \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 <ref>). For instance,  we show that given a "Muller" "automaton" $\A$, we can define a "Rabin" "condition@@accep" over the "underlying graph" of $\A$ obtaining an "equivalent@@aut" "automaton" if and only if the union of "rejecting@@cycle" "cycles" of $\A$ is again a "rejecting@@cycle" "cycle". Our results unify and extend those from <cit.>.

In Section <ref>, we conduct a comprehensive examination of a "normal form" for "parity" "automata". This "normal form" implicitly appears in <cit.>, and has since proven instrumental in proofs about "history-deterministic" "automata" <cit.>, positionality of "$\oo$-regular languages" <cit.> and learning of $\oo$-automata <cit.>. Similar normalisation procedures are commonly applied to "parity" "games" to speed up algorithms solving them <cit.>. 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 <cit.>, the determinisation of "Büchi" "automata" <cit.>, or the minimisation of "history-deterministic automata" <cit.>. It has also proven to be more applicable in practical scenarios <cit.>.  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 <ref>).

*Related versions

This paper is based on a preceding conference version <cit.>, and incorporates material from another conference paper <cit.>. 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 <cit.>. Most of the material concerning "deterministic" "automata" and "locally bijective morphisms" comes from <cit.>. This includes the construction of a "parity" "automaton" from the "Zielonka tree" (Section <ref>), the definition of the "ACD" (Section <ref>) and the construction of a "parity" "automata" from it (Section <ref>), as well as the introduction of "locally bijective morphisms" (Section <ref>) and the typeness results from Section <ref>. However, in <cit.>, the optimality of the "Zielonka-tree-parity-automaton" and the "ACD-parity-transform" was proven only with respect to "deterministic" "automata" and "locally bijective morphisms", respectively. Moreover, the proof of the optimality of the "ACD-parity-transform" (Theorem <ref>) has been simplified.

ICALP 2022 <cit.>. The construction of "history-deterministic" "Rabin" "automata" for "Muller languages" (Section <ref>) and its optimality (Theorem <ref>) come from <cit.>.

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 <ref>);

* the definition of "HD mappings", as well as the systematic study of the different kinds of "morphisms" (Sections <ref> and <ref>);

* the "ACD-HD-Rabin-transform" (Section <ref>) and its optimality (Theorem <ref>); and

* the introduction of a "normal form" for "parity" "automata" (Section <ref>).

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 <cit.>, 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 <cit.> and Owl 21.0 <cit.>, and it is used in the LTL-synthesis tools  <cit.> and Strix <cit.>. These implementations were presented in the conference paper <cit.>, where transformations based on the "ACD" are compared to the state-of-the-art existing paritizing methods.

The "typeness" results steaming from the "ACD" <cit.> have also been proven instrumental in theoretical applications. They have been used to show a correspondence between "Rabin" "automata" and "memory structures" for "games" <cit.>, and to provide lower bounds in the size of "deterministic" "Rabin" "automata" <cit.>.

§ 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, $\pow{A}$ its power set and $\intro*\powplus{A} = \pow{A} \setminus \{\emptyset\}$.
For a family of subsets $\F\subseteq \pow{A}$ and $A'\subseteq A$, we write $\intro*\restSubsets{\F}{A'} = \F \cap \pow{A'}$.

For natural numbers $i\leq j$, $[i,j]$ stands for $\{i,i+1, \dots, j-1,j \}$.

For a set $\Sigma$, a ""word"" over $\Sigma$ is a sequence of elements from $\Sigma$.

An ""$\omega$-word"" (or simply an infinite word) is a word of length $\oo$.
The sets of finite and infinite words over $\Sigma$ will be written $\Sigma^*$ and $\Sigma^{\oo}$, respectively,
and we let $\intro*\SigmaInfty = \Sigma^* \cup \Sigma^\oo$. Subsets of $\SS^*$ and $\SS^\oo$ will be called languages.  For a word $w\in \SigmaInfty$ we write $w_i$ to represent the $i$-th letter of $w$.

We let $\ee$ denote the ""empty word"", and let $\SS^+ = \SS^*\setminus\{\ee\}$. The concatenation of two words $u\in \Sigma^*$ and $v\in \SigmaInfty$ is written $u\cdot v$, or simply $uv$. If $u=v\cdot w$ for $v\in \Sigma^*, u,w\in \SigmaInfty$, we say that $v$ is a  ""prefix"" of $u$ and we write $v \intro*\prefix u$.

For a word $w\in \Sigma^\oo$, we let $\intro*\minf(w)=\{ a\in \Sigma \mid w_i=a \text{ for infinitely many } i\in \NN\}$.

We say that a language $L\subseteq \SS^\oo$ is ""prefix-independent"" if for all $w\in \SS^\oo$ and $u\in \SS^*$,  $uw\in L$ if and only if $w\in L$.

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

A ""graph"" is a tuple $G=(V,E,\msource,\mtarget)$ where $V$ is a set of vertices, $E$ a set of edges and $\intro*\msource\colon E\to  V$ and $\intro*\mtarget\colon E\to  V$ are maps indicating the source and target for each edge.
A ""path"" is a (finite or infinite) sequence $\rr = e_0e_1...\in \kl{E^\infty}$ such that  $\msource(e_{i})=\mtarget(e_{i-1})$ for all $i>0$. For notational convenience, we  write $v_0 \re {e_0} v_1 \cdots  \re{e_{n-1}} v_n$ to denote a finite path from $v_0 = \msource(e_0)$ to $v_n = \mtarget(e_{n-1})$ and we let $\intro*\msourcePath(\rr) = v_0$ and $\intro*\mtargetPath(\rr) = v_n$.
For $A\subseteq V$, we let $\intro*\PathSetFin{G}{A}$ and $\intro*\PathSet{G}{A}$ denote, respectively, the set of finite and infinite "paths"  on $G$ starting from some $v\in A$ (we omit brackets if $A=\{v\}$ is a singleton).  We let $\intro*\PathSetInfty{G}{A} = \PathSetFin{G}{A}\cup \PathSet{G}{A}$.

For a subset of vertices $A\subseteq V$ we write:

* $\intro*\mIn(A)=\{ e\in E \mid \mtarget(e)\in A \}$,

* $\intro*\mout(A)=\{ e\in E \mid \msource(e)\in A \}$.

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

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,\msource,\mtarget)$ is a graph $(V',E',\msource',\mtarget')$ such that $V'\subseteq V$, $E'\subseteq E$ and $\msource'$ and $\mtarget'$ are the restrictions  of $\msource$ and $\mtarget$ to $E'$, respectively. A ""strongly connected component"" (SCC) is a maximal "strongly connected" "subgraph". We say that a SCC is ""final@@SCC"" 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, \msource, \mtarget, I)$ is a "graph"
together with a non-empty subset of ""initial vertices"" $I\subseteq V$.
An ""acceptance condition"" over $G$ is a tuple $\mathrm{Acc} = (\gg, \GG, \WW)$ where $\GG$ is a finite set of ""colours"", $\gg:E\to \GG\cup\{\ee\}$ is an ""edge-colouring"" of $G$ and $\WW\subseteq \GG^\oo$ is a language of infinite words called the ""acceptance set"". We allow ""uncoloured edges"" ($\ee$-edges), but we impose the condition that no infinite path of $G$ is eventually composed exclusively of $\ee$-edges (that is, every "cycle" contains some edge $e$ with $\gg(e)\neq \ee$).

A ""transition system"" (abbreviated ""TS"") is a tuple $\TS = (\intro*\underlyingGraph{\TS}, \intro*\macc{\TS})$, where $\underlyingGraph{\TS} = (V,E, \msource, \mtarget, I)$ is a "pointed graph", called the ""underlying graph"" of $\TS$, and $\macc{\TS} = (\gg, \GG, \WW)$ is an "acceptance condition" over $\underlyingGraph{\TS}$. We will also refer to vertices and edges as states and transitions, respectively. We write $v \re c v'$ if there is $e\in E$ such that $\msource(e)=v$, $\mtarget(e)=v'$ and $\gg(e)=c$.
We will suppose for technical convenience that "transition systems" contain no sink, that is, every vertex has at least one outgoing edge .
For any non-empty subset of vertices $\tilde{I} \subseteq V$, we let $\intro*\initialTS{\TS}{\tilde{I}}$ be the "transition system" obtained from $\TS$ by setting $\tilde{I}$ to be its set of "initial vertices".
The ""size@@transSys"" of a transition system $\TS$ is the cardinality of its set of vertices, written $\intro*\size{\TS}$.

A ""run@@transSys"" on a "transition system" $\TS$ (or on a "pointed graph") is a (finite or infinite)
"path" $\rr=e_0e_1\dots \in \kl{E^\infty}$ starting from an "initial vertex", that is, $\msource(e_0)\in I$.
We let $\intro*\RunsFin{\TS}$ and $\intro*\Runs{\TS}$ be the set of finite and infinite "runs" on $\TS$, respectively, and we let $\intro*\RunsInfty{\TS} = \RunsFin{\TS}\cup \Runs{\TS}$. (We note that $\Runs{\TS} = \PathSet{\underlyingGraph{\TS}}{I}$.)

The ""output"" of a "run@@transSys" $\rr \in \RunsInfty{\TS}$ is the sequence of colours in $\GG^\infty$ obtained by removing the occurrences of $\ee$ from $\gamma(\rr)$; which we will also denote by $\gamma(\rr)$ by a small abuse of notation.
A "run@@transSys" $\rr$ is ""accepting@@run"" if $\gamma(\rr)\in \WW$, and ""rejecting@@run"" otherwise (in particular, finite runs will be rejecting).
We write $\rr = v\lrp{w} v'$ to denote a "run" with $\msourcePath(\rr)=v$, $\mtargetPath(\rr)=v'$ and $\gg(\rr)=w$.

We say that a vertex $v\in V$ is ""accessible@@fromVertex"" (or reachable) from a vertex $v_0$ if there exists a finite "path" from $v_0$ to $v$. We say that $v$ is ""accessible@@vertex"" if it is accessible from some "initial vertex". A set of states $B\subseteq V$ is ""accessible@@set"" if every state $v\in B$ is "accessible@@vertex".
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"" $\left(G, (l_V, L_V), (l_E, L_E)\right)$ is a "graph"  together with labelling functions $l_V: V \rightarrow L_V$, $l_E: E \rightarrow 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@@graph" "underlying graph".

We remark that, whenever necessary, we can suppose without loss of generality that in the "acceptance condition" $\mathrm{Acc} = (\gg, \GG, \WW)$ of a "transition system",  $\GG=E$ is the whole set of edges and $\gamma$ is the identity function.
Indeed, an "equivalent acceptance condition" can always be defined by using the "acceptance set" $\WW' = \{w\in E^\oo \mid \gg(w)\in \WW\} \subseteq E^\oo$ .

A ""(non-deterministic) automaton"" over $\SS$ is an "edge-labelled" "transition system" $\A = (\underlyingGraph{\A}, \macc{\A}, (l_\SS, \SS))$, where $\SS$ is a finite set of ""input letters"".
Let $\A$ be an "automaton" with $\underlyingGraph{\A} = (Q,\DD,\msource, \mtarget, I)$ as "underlying graph" and $\macc{\A} = (\gg, \GG, \WW)$ as "acceptance condition".
We write $e = q\re{a:c}q'$ to denote that $e\in \DD$ satisfies $l_\SS(e) = a$ and $\gg(e) = c$.
We can suppose that $\DD\subseteq Q\times \SS\times \GG \times Q$.
We define:

\[\intro*\transAut{}(q, a) = \{ (q', c)\in Q\times \GG \mid \text{ there is } e = q\re{a:c} q' \in \DD\}.\]

We note that we can now recover the classical representation of an automaton as a tuple $\A = (Q,\Sigma, I, \Gamma, \transAut{}, \WW)$, (or $(Q,\Sigma, I, \Gamma, \DD, \WW)$) 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\in Q$ and $a\in \Sigma$, $|\transAut{}(q,a)| \leq 1$.
We say that $\A$ is  ""complete""
if for every $q\in Q$ and $a\in \Sigma$, $|\transAut{}(q,a)| \geq 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\in \SigmaInfty$, a  ""run over $w$"" in $\A$ is a "run@@transSys" $\rr = e_0e_1\dots  \in \RunsInfty{\A}$ such that $l_\SS(e_i) = w_i$ for all $i \geq 0$.
A word $w\in \SS^\oo$ is  ""accepted@@word"" by $\A$ if it exists a "run over $w$" that is "accepting" (that is, a "run@@automaton" $\rr$ such that $\gg(\rr)\in \WW$).
The ""language accepted"" (or recognised) by an automaton $\A$ is the set

\[ \intro*\Lang{\A}:= \{ w\in \Sigma^\oo \mid w \text{ is "accepted@@word" by } \A \}.\]

Two "automata" "recognising" the same language are said ""equivalent@@aut"".

We remark that if $\A$ is "deterministic" (resp. "complete"), there is at most one (resp. at least one) "run over" $w$ for each $w\in \SigmaInfty$.

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 $\SS$ with $\DD$ as set of transitions and $I$ as set of "initial states".
A ""resolver@@aut"" for $\A$ is a pair $(r_0,r)$, consisting of a choice of an "initial state", $r_0\in I$, and a function $r\colon \DD^* \times \SS \to \DD$ such that for all words $w = w_0w_1\dots \in \SS^\oo$, the sequence $e_0e_1\dots \in \DD^\oo$, called the ""run induced by@@aut"" $r$ over $w$ and defined by $e_i = r(e_0\dots e_{i-1}, w_i)$ is actually a "run over" $w$ in $\A$ starting from $r_0$.
We say that the resolver is ""sound@@aut"" if it satisfies that for every $w\in \Lang{\A}$, the "run induced by@@aut" $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 $\Lang \A$.
An "automaton" $\A$ is called ""history-deterministic"" (shortened HD, also called good-for-games in the literature) if there is a "sound resolver@@aut" for it.

Sometimes in the literature <cit.> the initial state $r_0$ is not required to be specified. This would permit to choose it after the first letter $w_0$ is given. We consider that a resolver constructing a run without guessing the future should pick the initial state before the first letter is revealed, hence the introduction of $r_0$ in the definition of a resolver. The suitability of this choice will be further supported by the generalisation of "HD automata" to "HD mappings" (Section <ref>).

"Deterministic" "automata" are "history-deterministic", and they admit a unique "resolver".

In Figure <ref>, we show an "automaton" $\A$ over $\SS = \{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 $\GG=\{1,2\}$ and its "acceptance set" is $\WW = \{u\in \{1,2\}^\oo \mid u \text{ contains finitely many } 1s\}$ (this is a "coBüchi" condition, as introduced in the next section).
It is easy to check that $\A$ "recognises" the language:

\[ \Lang{\A} = \{w\in \SS^\oo \mid \minf(w)\subseteq \{a,b\} \tor \minf(w)\subseteq \{b,c\} \}. \]

A "resolver@@aut" 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@@aut" "resolver@@aut" 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$.

An example of a "history-deterministic" automaton that is not "deterministic".
The "acceptance set" is $\WW = \{u\in \{1,2\}^\oo \mid u \text{ contains finitely many } 1s\}$.
An arrow of the form $q\re{a,b:2} q'$ represents two different transitions with input letters $a$ and $b$, respectively. The "initial state" $q_0$ is marked with one incoming arrow.

We say that an state $q$ is ""reachable using the resolver $(r_0, r)$"" if there is a finite run $\rr = r_0 \lrpE q$ such that $\rr$ is the "run induced by@@aut" $r$ over some word $w\in\SS^*$.

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

Let $\A$ be an "HD automaton", let $(r_0,r)$ be a "sound@@aut" "resolver@@aut" for it and let $\tilde{\A}$ be the "subautomaton" induced by the set of states "reachable using $(r_0, r)$", with initial state $r_0$. Then, $\Lang{\A} = \Lang{\tilde{\A}}$.

The following lemma provides a simplification for "automata" "recognising" "prefix-independent" languages. Its proof can be found in Appendix <ref>. Together with Remark <ref>, 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.

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, $\Lang{\A} = \Lang{\initialTS{\A}{q}}$. Moreover, $\initialTS{\A}{q}$ is also "history-deterministic".  In particular, if $\A$ is "deterministic", this is the case for any "reachable" state $q$.

A ""game"" is a "vertex-labelled" "transition system" $\G = \left(\underlyingGraph{\G}, \macc{\G}, (\intro*\lPlayers, \{\Eve, \Adam\})\right)$, with $\underlyingGraph{\G} = (V,E,\msource, \mtarget, I)$ a "pointed graph",
and $l_{\mathrm{Players}}\colon V \to \{\Eve, \Adam\}$ a "vertex-labelling" function inducing a partition of $V$ into vertices controlled by two ""players"" that we refer to as ""Eve"" and ""Adam"". We let $\intro*\VEve = \inv{\lPlayers}(\Eve)$ and $\intro*\VAdam = \inv{\lPlayers}(\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 $\mout(v)$ and the token travels through this edge to its "target". In this way, they produce an infinite "run" $\rr$ on $\G$ (that we also call a ""play"").
The objective of Eve is to produce an "accepting run" (a sequence of "colours" in $\WW$), and Adam tries to prevent it.

A ""strategy"" from $v\in V$ for "Eve" is a (partial) function $\strat_{v}: \PathSetFin{\G}{v}  \partialF E$, defined for finite paths from $v$ ending in a vertex in $\VEve$, that tells "Eve" which move to choose after any possible "finite play".
We say that a "play" $\rr\in \PathSetInfty{\G}{v}$ is ""consistent with the strategy"" $\strat_v$ if after each finite prefix $\rr' \prefix \rr$ ending in a vertex controlled by "Eve", the next edge in $\rr$ is $\strat_v(\rr')$.
We say that $\strat_v$ is a ""winning strategy for Eve"" if all "plays" from $v$ "consistent with" $\strat_v$ are "accepting@@run". 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 $\intro*\winRegion{\Eve}{\G}$, is the set of "initial vertices" $v\in 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" $\initialTS{\G}{V}$ where all vertices are initial, that is, the set of vertices $v\in 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@@graph" "pointed graph" $\M = (M, E_M, \msource, \mtarget, m_0)$ with a single "initial state" $m_0$ and labels $l_M\colon E_M\to X$ inducing a deterministic structure, that is, satisfying that for each $m\in M$ and $x\in X$ there is at most one transition $e\in \mout(m)$ labelled $x$.
We denote $\intro*\transMem\colon M \times X \partialF M$ the ""update function@@mem"" given by $\transMem(m, x) = m'$ if $m\re{x}m'$ is the (only) transition from $m$ labelled $x$. We extend $\transMem$ to $\transMem\colon M\times X^* \partialF M$ by induction ($\transMem(m,\ee) = m$ and $\transMem(m,x_1\dots x_n) = \transMem(\transMem(m,x_1\dots 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"" $\intro*\nextmove\colon \VEve\times M \to E$.
We say that$(\M, \nextmove)$ ""implements@@memStrat"" a "strategy" $\strat_{v}: \PathSetFin{\G}{v}  \partialF E$  if for any "finite play" $\rr\in \PathSetFin{\G}{v}$ ending in $\VEve$, $\strat_{v}(\rr) = \nextmove(\mtargetPath(\rr), \transMem(m_0, \rr))$. 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@@mem" 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" $\WW_1$ to another one using a different "acceptance set" $\WW_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 <ref>, <ref>, and <ref>).

Let $\TS =(\underlyingGraph{\TS}, \macc{\TS})$ be a "transition system", with $\underlyingGraph{\TS} = (V, E, \msource_\TS, \mtarget_\TS, I_{\TS})$ and $\macc{\TS} = (\gg_{\TS}, \SS, \WW_{\TS})$,
and let $\A=\left(\underlyingGraph{\A}, \macc{\A}, (l_\SS, \SS)\right)$ be a "complete" "automaton" over the alphabet $\Sigma$, where $\underlyingGraph{\A} = (Q,  \DD, \msource_\A, \mtarget_\A, I_{\A})$ and $\macc{\A} = (\gg_{\A}, \GG, \WW_{\A})$.
The ""composition"" of $\TS$ and $\A$ (also called their product) is the "transition system" $\TS \intro*\compositionAut \A$ defined as follows:

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

* The set of "initial vertices" is $I_{\TS} \times I_{\A}$.

* The set of edges $\intro*\edgesProduct$ contains a transition $(v,q)\re{c} (v', q')$ if there is $a\in \SS$ and transitions $e_1 = v\re{a} v'\in E$  and $e_2 = q\re{a:c} q'\in \DD$. It also contains "$\ee$-edges" $(v,q)\re{\ee} (v', q)$ if $v\re{\ee}v'\in E$. Formally,

\[ \edgesProduct = \{(e_1,e_2) \in E\times \DD \mid \gg_{\TS}(e_1) = l_\SS(e_2)\} \; \cup \; \{e_1 \in E \mid \gg_{\TS}(e_1) = \ee \} \; \subseteq \; (E \times \DD) \cup E. \]

* The "acceptance condition" is inherited from that of $\A$: the "colouring function" $\gamma'\colon \edgesProduct \to \Gamma$ is defined as $\gamma'(e_1,e_2)= \gamma(e_2)$, and the "acceptance set" is $\WW_\A \subseteq \Gamma^\oo$.

We remark that if $\TS$ does not contain an "uncoloured" "cycle", neither does $\TS \compositionAut \A$. Also, $\TS \compositionAut \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 \compositionAut \A$ as a "labelled transition system" with the functions $l_V^\ltimes(v,q) = l_V(v)$ and $l^\ltimes_E(e_1, e_2) = l_E(e_1)$ (resp. $l^\ltimes_E(e_1) = l_E(e_1)$ if $e_1$ is an "uncoloured" edge).

Intuitively, a computation in $\TS \compositionAut \A$ happens as follows: we start from a vertex $v_0\in I_{\TS}$ in $\TS$ and from $q_0 \in I_{\A}$. When we are in a position $(v, q)\in V \times Q$, a transition $e$ between $v$ and $v'$ takes place in $\TS$, producing a letter $a\in \Sigma$ as "output". Then, the automaton $\A$ proceeds using a transition corresponding to $a$, producing an output in $\Gamma$. In this way, a word in $\Gamma^\oo$ is generated and we can use the "acceptance set" $\WW_\A \subseteq \Gamma^\oo$ of the "automaton" as the "acceptance set" for $\TS \compositionAut \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\compositionAut \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\re{}v'$ such that $v\in \VAdam$, the edge $e$ is "uncoloured" ($\gg(e)=\ee$), $v'\in \VEve$, and $e$ is the only incoming edge to $v'$ ($\mIn(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 <ref>.

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 <ref>, which generalise them.

Let $\B$ be an automaton with "acceptance set" $\WW_{\B}$  and let $\A$ be an "automaton" "recognising" $\Lang \A=\WW_{\B}$. Then, $\Lang{ \B \compositionAut \A}=\Lang \B$.
Moreover, if $\A$ and $\B$ are "deterministic" (resp. "history-deterministic"), so is $\B \compositionAut \A$.

Let $\G$ be a "game" that is "suitable for transformations" with "acceptance set" $\WW_\G$, and let $\A$ be a "history-deterministic" "automaton" "recognising" $\Lang \A=\WW_{\G}$. Then, the "winning region" of Eve in $\G$ is the projection of her "winning region" in $\G\compositionAut \A$, that is, Eve "wins $\G$ from" an "initial vertex" $v$ if and only if she "wins $\G\compositionAut \A$ from $(v, q_0)$", for $q_0$  some initial vertex of $\A$.

Proposition <ref> 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 <cit.>.

Let $\A$ be an "automaton" "recognising" $\WW_{\G}\subseteq \Sigma^\oo$ satisfying that for every "game" $\G$ "suitable for transformations"  with "acceptance set" $\WW_\G$, "Eve" "wins" the "game" $\G$ from an "initial vertex" $v$ if and only if she "wins" $\G \compositionAut \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 "$\oo$-regular automata" as "acceptance sets".
We let $\Gamma$ stand for a finite set of "colours".

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

\[ \intro*\BuchiC{B}{\GG}  = \{w\in \GG^\oo \mid \minf(w) \cap B \neq \emptyset\}. \]

We say that a language $L\subseteq \GG^\oo$ is a ""Büchi language"" if there is a set $B\subseteq \GG$ such that $L = \BuchiC{B}{\GG}$.

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

\[ \intro*\coBuchiC{B}{\GG}  = \{w\in \GG^\oo \mid \minf(w) \cap B = \emptyset\}. \]

We say that a language $L\subseteq \GG^\oo$ is a ""coBüchi language"" if there is a set $B\subseteq \GG$ such that $L = \coBuchiC{B}{\GG}$.

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

\[ \intro*\RabinC{R}{\GG} = \{w\in \GG^\oo \mid [\minf(w)\cap G_j \neq \emptyset \text{ and } \minf(w)\cap R_j = \emptyset] \text{ for some index } j \}. \]

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

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

\[ \intro*\StreettC{S}{\GG} = \{w\in \GG^\oo \mid [\minf(w)\cap G_j \neq \emptyset \text{ implies } \minf(w)\cap R_j = \emptyset] \text{ for all indices } j \}. \]

We say that a language $L\subseteq \GG^\oo$ is a ""Streett language"" if there is a family of "Rabin pairs" $S$ such that $L = \StreettC{S}{\GG}$.

Parity. We define the parity language over the alphabet $[d_{\min}, d_{\max}]\subseteq \NN$

\[ \intro*\parity_{[d_{\min}, d_{\max}]} = \{ w\in [d_{\min}, d_{\max}]^\oo \mid \min \minf(w) \text{ is even}\}.\]

We say that a language $L\subseteq \GG^\oo$ is a ""$[d_{\min}, d_{\max}]$-parity language"" if there is a mapping $\phi\colon \GG \to [d_{\min}, d_{\max}]$ such that for all $w\in \GG^\oo$, $w\in L$ if and only if $\phi(w)\in \parity_{[d_{\min}, d_{\max}]}$. We say that $L$ is a ""parity language"" if there are $d_{\min}, d_{\max}\in \NN$ such that $L$ is a "$[d_{\min}, d_{\max}]$-parity language".

Muller. We define the ""Muller language associated to"" a family $\F\subseteq \powplus{\Gamma}$ of non-empty subsets of $\Gamma$ as:

\[ \intro*\MullerC{\F}{\GG} = \{w\in \GG^\oo \mid \minf(w) \in \F\}. \]

We say that a language $L\subseteq \GG^\oo$ is a ""Muller language"" if there is a family $\F\subseteq \powplus{\Gamma}$ such that $L = \MullerC{\F}{\GG}$.

We drop the subscript $\GG$ (resp. $[d_{\min}, d_{\max}]$) whenever the set of colours is clear from the context.
We remark that all languages of the classes above are "prefix-independent" (for all $w\in \GG^\oo$ and $u\in \GG^*$,  $uw\in L$ if and only if $w\in L$).

We say that an "acceptance condition" (resp. "transition system", "automaton") is an ""$X$ condition"" (resp. $X$ transition system, $X$ automaton), for $X$ one of the classes of languages above, if its "acceptance set" is an $X$ language.
In the case of "parity" "transition systems", we will always suppose that the set of "colours" is a subset of $\NN$ and $\phi$ is the identity function.

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

We discuss further classes of languages in Appendix <ref> ("generalised Büchi" and "coBüchi@@generalised" languages, as well as "generalised weak" acceptance). We refer to the survey <cit.> for a more detailed account on different types of acceptance conditions.

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" <cit.>.
In particular, all  classes above are special cases of "Muller languages".
The relations between these classes of languages are outlined in Figure <ref>.

[square/.style=regular polygon,regular polygon sides=4, align=center,node distance=2cm,inner sep=3pt]
at (-0.5,0.5)  (Buchi) "Büchi" $=$ "$[0,1]$-parity";
at (-0.7,-0.5)  (co-Buchi) "coBüchi" $=$ "$[1,2]$-parity";
at (3.4,0)  (Parity) "Parity";
at (6,0.5)  (Streett) "Streett";
at (6,-0.5)  (Rabin) "Rabin";
at (8,0)  (Muller) "Muller";

(Buchi) edge[->] (Parity)
(co-Buchi) edge[->] (Parity)
(Parity) edge[->] (Streett)
(Parity) edge[->] (Rabin)
(Streett) edge[->] (Muller)
(Rabin) edge[->] (Muller);

Relations between subclasses of "Muller languages". An arrow from a class $X$ towards a class $Y$ means that if a language $L\subseteq \GG^\oo$ 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" <cit.>.

A language $L\subseteq \GG^\oo$ is a "Muller language" if and only if it satisfies:

\[ \text{For all } w,w'\in \GG^\oo, \tif \minf(w) = \minf(w'), \text{ then } w\in L \iff w' \in L. \qedEx\]

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" <cit.>.

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.

In Figure <ref> we show three different types of "automata" over the alphabet $\SS=\{a,b\}$ "recognising" the language

\[ L = \{ w \in \SS^\oo \mid w=ub^\oo \text{ or } \left(w=ua^\oo \text{ and } u\text{ has an even number of `b's }\right) \}.\qedEx \]

Different types of "automata" "recognising" the language $L = \{ w \in \SS^\oo \mid w=ub^\oo \text{ or } \left(w=ua^\oo \text{ and } u\text{ has an even number of `b's }\right) \}$.

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

Let $L\subseteq \SS^\oo$ be a language of infinite words. The following properties are equivalent:

* $L$ can be "recognised" by a non-deterministic "Büchi" "automaton".

* $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 ""$\oo$-regular@@language"".
Many other equivalent definitions exist. Notably, "$\oo$-regular languages" are exactly the languages that can be defined using monadic second-order logic <cit.>, those that can be described by using $\oo$-regular expressions <cit.>, and those that can be "recognised" by an $\oo$-semigroup <cit.>.

Let $\TS$ be a "transition system" with $V$ and $E$ as set of vertices and edges, respectively. A ""cycle"" of $\TS$ is a subset $\ell \subseteq E$ such that there is a finite "path" $v_0 \re {e_0}v_1 \re {e_1}v_2 \re{} \dots v_r \re {e_r} v_0$ with $\ell = \{e_0, e_1, \dots, e_r\}$.
We remark that we do not require this "path" to be simple, that is, edges and vertices may appear multiple times.
The set of ""states of the cycle"" $\ell$ is $\intro*\states{\ell} = \{v_0, v_1, \dots v_r\}$.

The set of "cycles" of a "transition system" $\TS$ is written $\intro*\cycles{\TS}$.
We will consider the set of "cycles" ordered by inclusion.
For a state $v\in V$, we note $\intro*\cyclesState{\TS}{v}$ the subset of "cycles" of $\TS$ "containing@@cycle" $v$.
We remark that a vertex $v$ is "recurrent" if and only if $\cyclesState{\TS}{v}\neq \emptyset$.
We note that $\cyclesState{\TS}{v}$ is closed under union; moreover, the union of two "cycles" $\ell_1, \ell_2\in \cycles{\TS}$ is again a "cycle" if and only if there is some state $v$ such that both $\ell_1$ and $\ell_2$ contain $v$.

Let $\TS$ be a "Muller" "transition system" with "acceptance condition" $(\gg, \GG, \MullerC{\F}{\GG})$.
Given a "cycle" $\ell\in \cycles{\TS}$, we say that $\ell$ is ""accepting@@cycle"" (resp. ""rejecting@@cycle"") if $\gg(\ell) \in \F$ (resp. $\gg(\ell) \notin \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@@SCC"" and ""rejecting@@SCC"" similarly to the "SCCs" of a "Muller" "transition system".

We note that, by definition, the "acceptance@@run" of a "run" in a "Muller" "transition system" only depends on the set of transitions taken infinitely often. For any infinite "run" $\rr \in \Runs{\TS}$, the set of transitions taken infinitely often forms a "cycle", $\minf(\rr) = \ell_\rr\in \cycles{\TS}$, and $\rr$ is an "accepting run" if and only if $\ell_\rr$ is an "accepting cycle".

The deterministic and history-deterministic parity hierarchy.

As we have mentioned, every "$\oo$-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 "$\oo$-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 <cit.>, Kaminski <cit.>, and Mostowski <cit.>. We represented this hierarchy in Figure <ref>. This hierarchy is strict, that is, for each level of the hierarchy there are languages that do not appear in lower levels <cit.>. It is known that we can decide in polynomial time the "parity index" of an "$\oo$-regular language" represented by a "deterministic" "parity" "automaton" <cit.>, but this problem is $\NPcomplete$ if the language is given by a "deterministic" "Rabin" or "Streett" "automaton" <cit.>.

[square/.style=regular polygon,regular polygon sides=4, align=center,node distance=2cm,inner sep=3pt]

at (0,0)  (00) $[0,0]$;
at (4,0)  (11) $[1,1]$;
at (2,0.75)  (Weak1) $\WeakIndex{1}$;

at (0,1.5)  (01) $[0,1]$;
at (4,1.5)  (12) $[1,2]$;
at (2,2.25)  (Weak2) $\WeakIndex{2}$;

at (0,3)  (02) $[0,2]$;
at (4,3)  (13) $[1,3]$;
at (2,3.75)  (Weak3) $\WeakIndex{3}$;

at (0,4.25)  (dotsLeft) $\vdots$;
at (4,4.25)  (dotsRight) $\vdots$;
at (2,4.5)  (dotsRight) $\vdots$;

(00) edge (Weak1)
(11) edge (Weak1)
(Weak1) edge (01)
(Weak1) edge (12)

(01) edge (Weak2)
(12) edge (Weak2)
(Weak2) edge (02)
(Weak2) edge (13)

(02) edge (Weak3)
(13) edge (Weak3);

The (history-)deterministic parity hierarchy.

Let $L\subseteq \SS^\oo$ be an "$\oo$-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} \geq d-1$, and in case of equality $d_{\min}$ is even (resp. odd).
We say that the ""parity index"" of $L$ is $[0, d-1]$ (resp. $[1, d]$) if, moreover, there is a "DPA" "recognising" $L$ with a "parity" "acceptance condition" over the set of colours $[0,d-1]$ (resp. $[1,d]$).

We say that $L$ has parity index at least $\intro*\WeakIndex{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} \geq d$. We say that the parity index of $L$ is $\WeakIndex{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 "$\oo$-regular language" $L$, there is a unique $d$ such that either $L$ has "parity index" $[0,d-1]$, $[1,d]$ or $\WeakIndex{d}$, and these options are mutually exclusive. See also Appendix <ref> for more details about languages of "parity index" $\WeakIndex{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 "$\oo$-regular language" of "parity index" $[0, d-1]$ uses at least $d$ different colours (Proposition <ref>).

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

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 $\WeakIndex{d}$, then $\A$ uses at least $d+1$ output colours.

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

Let $\TS$ be a "transition system" using the "Muller@@condition" "acceptance condition" $(\gg, \GG, \MullerC{\F}{\GG})$.
A ""$d$-flower"" over a state $v$ of $\TS$ is a set of $d$ "cycles" $\ell_1, \ell_2, \dots, \ell_{d}\in \cyclesState{\TS}{v}$ such that $\ell_i \supsetneq \ell_{i+1}$ and $\gg(\ell_i)\in \F \iff \gg(\ell_{i+1})\notin \F$. We say that it is a ""positive flower""  if $\gg(\ell_{1})\in \F$ and that it is ""negative@@flower"" otherwise.

Let $\A$ be a "DMA". If $\A$ admits an "accessible" "positive@@flower" (resp. "negative@@flower") "$d$-flower", then $\Lang{\A}$ has "parity index at least" $[0,d-1]$ (resp. $[1,d]$). If $\A$ admits both "accessible" "positive@@flower" and "negative@@flower" "$d$-flowers", then $\Lang{\A}$ has "parity index at least" $\WeakIndex{d}$.

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

§.§ Trees

We introduce some technical notations that will be used to define "automata" based on the "Zielonka tree" (Sections <ref> and <ref>) and the transformations based on the "ACD" (Sections <ref> and <ref>).

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

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

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

\[ \intro*\nextChild_{T'}(n')=\begin{cases}
\min_{\leq_n}\{n''\in \children_{T'}(n) \mid n' <_n n''\} \text{ if this set is not empty},\\[2mm]
\min_{\leq_n}\{ n''\in \children_{T'}(n) \} \tow.
\end{cases} \]

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

Let $T'=(N',\preceq')$ be a "subtree" of $T = (N,\preceq)$. Let $n_{m}\in N'$ and $n_o\in N$ such that $n_{m}$ is a strict "ancestor" of $n_o$ ($n_{m} \prec n_o$).
If $n_m$ is a "leaf" of $T'$, we define  $\intro*\jump_{T'}(n_o, n_m) = n_m$.
If not, we define  $\jump_{T'}(n_o, n_m) = l_{\mathrm{dest}}\in \leaves(T')$ to be the only node satisfying that there are two children of $n_m$ in $T$, $n_1, n_2\in \children_T(n_m)$ such that:

* $n_1 \ancestor n_o$,

* $n_2 = \nextChild_{T'}(n_1)$ (in particular, $n_2\in N'$),

* $l_{\mathrm{dest}} \descendant n_2$ is the "leftmost@@tree" "leaf" in $T'$ (minimal for $\orderTree{T'}$) below $n_2$.

The choice of the leftmost "leaf" is arbitrary. In all our uses of the function $\jump$, it could be replaced by any "leaf" below $n_2$.

(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@@tree" $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") "tree" $T$ together with a labelling function $\nu \colon N \to A$.
A set of "trees" is called a ""forest"".

We refer the reader to Examples <ref> and <ref> 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" $\pp \colon \B\to \A$ witnesses that each state $q\in \A$ has been augmented to $\inv{\pp}(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@@morp" for mappings.

In all this section, $\TS = (\underlyingGraph{}, \macc{})$ and $\TS' = (\underlyingGraph{}', \macc{}')$ will stand for "transition systems" with "underlying graphs" $\underlyingGraph{} =(V ,E , \msource , \mtarget, I)$ and $\underlyingGraph{}' =(V' ,E' , \msource' , \mtarget', I')$, and "acceptance conditions" $\macc{} = (\gg, \GG, \WW)$ and  $\macc{}' = (\gg', \GG', \WW')$.

§.§ Morphisms of transition systems

A ""morphism of graphs"" from $G$ to $G'$ is a pair of mappings $\pp = (\pp_V: V \rightarrow V', \pp_E: E \rightarrow E')$ preserving edges, that is:

* $\msource'(\pp_E(e))=\pp_V(\msource(e))$ for every $e\in E$,

* $\mtarget'(\pp_E(e))=\pp_V(\mtarget(e))$ for every $e\in E$.

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

* $\pp_V(v_0)\in I'$ for every $v_0\in I$.

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

* $l_V'(\pp_V(v))=l_V(v)$ for every $v\in V$,

* $l_E'(\pp_E(e))=l_E(e)$ for every $e\in V$.

We will write $\pp\colon G \to G'$ to denote a "morphism@@graphs" $\pp$. We will drop the subscript in $\pp_V$ and $\pp_E$ whenever it can be deduced from its use.
We say that $\pp$ is ""surjective"" (resp. injective) if $\pp_V$ is.

Note that the mapping $\pp_V$ does not completely determine a "morphism@@graphs" $\pp$, as multiple edges might exist between two given vertices. However, if $G$ has no isolated vertices, the mapping $\pp_E$ does determine it. It will be convenient nonetheless to also keep the notation for $\pp_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" $\pp\colon G \to G'$ induces a mapping
\[\intro*\ppRuns\colon \RunsInfty{G}\to \RunsInfty{G'}.\]

Let $\TS$ and $\TS'$ be two ("labelled") "transition systems". A ""weak morphism of (labelled) transition systems"" $\pp\colon \TS \to \TS'$ is a "morphism of (labelled) pointed graphs" between their "underlying graphs", $\pp: G \to 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" $\rr \in \Runs{\TS}$,  $\gg(\rr) \in \WW \; \iff \; \gg'(\ppRuns(\rr)) \in \WW'$.

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" $\pp\colon \TS \to \TS'$ is an ""isomorphism@@TS"" if $\pp_V$ and $\pp_E$ are bijective and $\inv{\pp} = (\inv{\pp_V}, \inv{\pp_E})$ is a "morphism" from $\TS'$ to $\TS$. In that case, we say that $\TS$ and $\TS'$ are ""isomorphic@@TS"".

§.§ Local properties of morphisms

A "morphism of pointed graphs" $\pp: G \rightarrow G'$ is called:

* ""Locally surjective"" if it verifies:

* For every $v_0'\in I'$ there exists $v_0\in I$ such that $\pp(v_0)=v_0'$.

* For every $v\in V$ and every $ e'\in \mout(\pp(v))$
there exists $e\in \mout(v) $ such that $ \pp(e)=e' $.

* ""Locally injective"" if it verifies:

* For every $v_0'\in I'$, there is at most one $v_0\in I$ such that $\pp(v_0)=v_0'$.

* For every $ v\in V$ and every couple $ e_1,e_2\in \mout(v) $,  $\pp(e_1)=\pp(e_2)$ implies $e_1=e_2$.

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

Equivalently, a "morphism of pointed graphs" $\pp$ is "locally surjective" (resp. "locally injective") if for every $v\in V$ the restriction of $\pp_E$ to $\mout(v)$ is a surjection onto $\mout(\pp(v))$ (resp. an injection into $\mout(\pp(v))$), and the restriction of $\pp_V$ to $I$ is a surjection onto $I'$ (resp. an injection into $I'$).

Let $\pp: \TS \rightarrow \TS'$ be a  "(weak) morphism", and let $\rr'= v_0'\re{e_0'}v_1'\re{e_1'}\dots$ be a "run" in $\TS'$. If $\pp$ is "locally surjective", we can pick an initial vertex $v_0$ in $\inv{\pp}(v_0')$ and build step-by-step a run $\rr$ in $\TS$ from $v_0$ that is sent to $\rr'$ under $\pp$. If $\pp$ 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 $\pp$ in a unique way.
Said differently, if $\pp: \TS \rightarrow \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 <ref>).
This property will allow us to show that a "locally bijective" "morphism@@TS" witnesses the semantic equivalence of $\TS$ and $\TS'$ (see Section <ref>).

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@@run" of a run as a whole; we do not impose the "output colour" of an edge $\gg(e)$ to coincide with the "colour" $\gg'(\pp(e))$. This allows us to compare "transition systems" using different types of "acceptance conditions".

Let $\pp$ be a "morphism of pointed graphs".

* If $\pp$ is "locally surjective", then $\ppRuns$ is surjective.

* If $\pp$ is "locally injective", then $\ppRuns$ is injective.

* If $\pp$ is "locally bijective", then $\ppRuns$ 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.

If $\pp\colon \TS \to \TS'$ is a "locally surjective" "weak morphism", it is onto the "accessible part" of $\TS'$. That is, for every "accessible" state $v'\in \TS'$, there exists some state $v\in \TS$ such that $\pp_V(v)=v'$. In particular, if every state of $\TS'$ is "accessible", $\pp$ is "surjective".

Let $v'$ be an accessible state of $\TS'$. By definition, there exists a "finite run" $\rr'$ from an initial vertex of $\TS'$ to $v'$. By surjectivity of $\ppRuns$, there is a finite "run" $\rr\in \RunsFin{\TS}$ such that $\ppRuns(\rr) = \rr'$. As $\pp$ is a "morphism of graphs", we have that $\pp(\mtargetPath(\rr)) = v'$.

In Figure <ref> we provide an example of a "locally bijective morphism" between the two rightmost "transition systems" from Figure <ref> (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 = \{\{\alpha\},\{\beta\}\}$.
The morphism is given by $\pp_V(v_1) = \pp_V(v_2) = v'$ and $\pp_V(v_2) = v_2'$. In this case, the mapping $\pp_V$ determines a unique "morphism"; the (uniquely determined) mapping $\pp_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".

A "locally bijective morphism" from a "parity" "TS" to a "Muller" "TS" with "acceptance set" given by $\F = \{\{\alpha\},\{\beta\}\}$. We use dashed arrows to represent the images of vertices, and colours to represent the image of edges (that can be inferred from $\pp_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 $\pp(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@@aut" "automaton" "recognising" the "acceptance set" ot $\TS$, the "composition" $\TS \compositionAut \A$ does not admit a "locally bijective morphism" to $\TS$, although it shares most semantic properties with it (Proposition <ref>).

We introduce next "HD mappings", which are "weak morphisms" with the minimal set of hypothesis ensuring that, if $\pp\colon \TS \to \TS'$ is an "HD mapping", we can "simulate@@morph" "runs" of $\TS'$ in $\TS$ via $\pp$ while preserving their "acceptance@@run". This will allow us to show that $\pp$ witnesses the semantic equivalence of $\TS$ and $\TS'$ (Section <ref>).

Different types of morphisms and the relations between them. The fact that "locally surjective morphisms" are "HD mappings" is given by Lemma <ref>. Note that "HD mappings" are also "locally surjective" "weak morphisms" (Remark <ref>).

*History-deterministic mappings

Let $\TS$ and $\TS'$ be "transition systems" and $\pp:\TS \to \TS'$ a "weak morphism" between them.
A ""resolver simulating $\pp$"" consists in a pair of functions $\intro* \rInit\colon I' \to I$ and $r\colon E^* \times E' \to E$ such that:

* $\pp(\rInit(v_0')) = v_0'$ for all $v_0'\in I'$,

* $\pp(r(\rr,e')) = e'$, for all $\rr\in E^*$ and $e'\in E'$,

* if $e_0'\in \mout(I')$, $\msource(r(\ee,e_0')) = \rInit(\msource(e_0'))$,  and

* if $\rr$ is a finite run in $\TS$ ending in $v$ and $e'\in \mout(\pp(v))$, then $r(\rr, e')\in \mout(v)$.

Given a "run" $\rr' = e_0'e_1'\dots \in \RunsInfty{\TS'}$ starting in some $v_0'\in I'$, the ""run induced by@@morphism"" $r$ is the sequence $\intro*\rRuns(\rr') = e_0e_1e_2\dots\in \RunsInfty{\TS}$ defined by $e_i = r(e_0\dots e_{i-1}, e_i')$, which is indeed a "run" in $\TS$.
We say that the "resolver@@HDmorphism" is ""sound@@resolverMorphism"" if for every "accepting run" $\rr'\in \Runs{\TS'}$, the "run" $\rRuns(\rr')$ is "accepting@@run" in $\TS$.
Note that we do not impose $\rRuns(\rr')$ to be "rejecting@@run" if $\rr'$ is.

Provided that all states of $\TS'$ are "accessible", a "resolver simulating $\pp$" can only exist if $\pp$ is a "locally surjective" "weak morphism".

Said differently, a "sound@@morph" "resolver simulating" $\pp$ 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 $\pp(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 $\pp(e_n) = e_n'$.

* Duplicator wins if either $e_1e_2\dots$ is an "accepting run" in $\TS$ from $v_0$ or $e_1'e_2'\dots$ is not an "accepting run" in $\TS'$ from $v_0'$ (it is either not a "run from $v_0$" or not "accepting@@run"). Spoiler wins otherwise.

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 $\pp = (\pp_V: V \rightarrow V', \pp_E: E \rightarrow E')$ such that:

* $\pp$ is a "weak morphism",

* $\pp$ ""preserves accepting runs"":  $\rr \in \Runs{\TS}$ and  $\gg(\rr) \in \WW \; \implies \; \gg'(\ppRuns(\rr)) \in \WW'$, and

* there exists a "sound@@morph" "resolver simulating" $\pp$.

Even if a "history-deterministic mapping" is not necessarily "locally bijective" (and not even a "morphism of transition systems"), the existence of a "sound@@morph" "resolver@@HDmorphism" allows to define a right inverse to $\ppRuns$ preserving the "acceptance@@runs" of "runs".

Let $\pp\colon \TS \to \TS'$ be an "HD mapping" and let $(\rInit, r)$ be a "sound@@morph" "resolver simulating" it. The following holds:

* $\ppRuns \circ \rRuns = \Id{\RunsInfty{\TS'}}$.

* $\rRuns$ preserves the "acceptance@@runs" of "runs" in $\TS'$, that is,  for every "run" $\rr' \in \Runs{\TS'}$,  $\rr'$ is "accepting@@run" if and only if $\rRuns(\rr')$ is "accepting@@run" in $\TS$.

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

For the second item, the definition of a "sound resolver@@morph" imposes that if $\rr'$ is "accepting@@run", so is $\rRuns(\rr')$. For the other direction, if $\rRuns(\rr')$ is "accepting@@run", then $\ppRuns(\rRuns(\rr')) = \rr'$ has to be "accepting@@run", as an "HD mapping" "preserves accepting runs".

In Figure <ref> we give an example of a "weak morphism" $\pp\colon \TS \to \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 = \{\{\aa\},\{\aa,\bb\}, \{\aa,\lambda\}\}$; that is, a "run" in $\TS'$ is "accepting@@run" if and only if it eventually avoids either transition $e'$ or transition $f'$.
The "weak morphism" we propose is given by: $\pp(v_0)= \pp(v_1) = \pp(v_2) = v'$, and $\pp(u_1) = \pp(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 $\pp(e_1)=\pp(e_2) = e'$ and $\pp(f_1)=\pp(f_2) = f'$.

A "history-deterministic mapping" from a "parity" "TS" to a "Muller" "TS" with "acceptance set" given by $\F = \{\{\aa\},\{\aa,\bb\}, \{\aa,\lambda\}\}$. We use dashed arrows to represent the images of vertices, and colours to represent the image of edges.

We remark that $\pp$ 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@@run", but its image is "accepting@@run" in $\TS'$.
However,  $\pp$ "preserves accepting runs": a "run" is "accepting@@run" 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 $\pp$ avoids transition $f'$ in $\TS'$, and in the second case, its image avoids transition $e'$.

Finally, we describe a "sound@@morph" "resolver simulating $\pp$". 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'\re{\aa}u'$ is simulated by $v_0\re{1}u_1$ and $v'\re{\aa}v'$ is simulated by $v_0\re{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'$).

*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 $\pp\colon\G \to \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 $\pp$" 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 $\pp:\G \to \G'$ be a "weak morphism" between them admitting a "resolver@@morphism" $(\rInit, r)$ "simulating@@resolver" $\pp$.
Given "runs" $\rr' = e_0'e_1'\dots \in \Runs{\G'}$ and $\rr = e_0e_1\dots \in \Runs{\G}$, we say that $\rr$ is ""consistent with@@resolver"" $(\rInit, r)$ over $\rr'$ if:

* $\msource(e_0) = \rInit(\msource(e_0')$,

* $\pp(e_i) = e_i'$, and

* for every finite prefix $e_0e_1\dots e_{n-1} \prefix \rr$ ending in a vertex "controlled by Eve", the next edge in $\rr$ is $e_n = r(e_0\dots e_{n-1}, e_n')$.

We remark that there exists at least one run "consistent with@@mapping" $(\rInit, r)$ over $\rr'$, namely $\rRuns(\rr')$.

We say that $(\rInit, r)$ is ""sound for $\G$"" if it verifies that for any "accepting run" $\rr'\in \Runs{\G'}$, all runs "consistent with@@resolver" $(\rInit, r)$ over $\rr'$ 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 $\pp(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}\re{} v_{n}\in \mout(v_{n-1})$ such that $\pp(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_1e_2\dots$ is an "accepting run" in $\G $ from $v_0$ or $e_1'e_2'\dots$ is not an "accepting run" in $\G'$ from $v_0'$. Spoiler wins otherwise.

An "HD mapping" "of games@@morphism" $\pp:\G \to \G'$ is called ""history-deterministic-for-games"" if it admits a "resolver" "sound for $\G$".

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

In the next lemma, we prove that "HD@@mapping" 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").

If $\pp: \TS \to \TS'$ is a "locally surjective morphism", it is also an "HD mapping". If $\TS$ and $\TS'$ are "games", $\pp$ is moreover "HD-for-games".

We need to define a "sound@@morph" "resolver simulating" $\pp$. Let $\rInit\colon I' \to I$ be any function choosing initial vertices satisfying that $\pp\circ\rInit = \Id{I'}$ (which exists by "local surjectivity" of $\pp$). For each $v\in V$ and edge $e'\in \mout(\pp(v))$ we choose one edge $f(v,e')\in \mout(v)$ such that $\pp(f(v,e')) = e'$ (which exists by "local surjectivity"), and we let $r$ be the "resolver" induced by these choices. Formally, we define $r \colon E^*\times E' \to E$ recursively. For the base case, if $e_0'\in \mout(v')$, with $v'\in I'$, we define $r(\ee, e_0') = f(\rInit(v'), e_0')$. Suppose that $r$ has been defined for "runs" of length $\leq n$, and let $\rr\in E^*$ be of length $n+1$ and $e'\in E'$. If $\rr$ is not a "run" or $e'\notin \mout(\mtarget(\pp(\rr)))$, we let $r(\rr,e')$ be any edge in $\inv{\pp}(e')$. If not, let $v = \mtarget(\rr)$ and we define $r(\rr,e')$ to be the edge $f(v,e')$.

It is straightforward to check that $(\rInit, r)$ is indeed a "resolver@@mapping"  (for every "run" $\rr'\in \Runs{\TS'}$, the sequence $\rRuns(\rr')$ is a "run" in $\TS$ and $\rr'$ is its image under $\pp$). Finally, since $\pp$ is a "morphism", for every $\rr'\in \Runs{\TS'}$ and every $\rr\in \Runs{\TS}$ "consistent with@@resolver" $(\rInit, r)$ over $\rr'$, $\rr$ is "accepting@@run" in $\TS$ if and only if $\rr' = \ppRuns(\rr)$ is  "accepting@@run" in $\TS'$. We conclude that $(\rInit ,r)$ is a "sound resolver@@morph" (resp. "sound for $\TS$") and therefore $\pp$ 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@@mapping" of mappings.

Let $\TS$ and $\TS'$ be two "TS" such that there is an "HD@@mapping" (resp. "HD-for-games") mapping $\pp\colon \TS \to \TS'$.
For any non-empty subset $\tilde{I} \subseteq I'$, $\pp$ is also an "HD@@mapping" (resp. "HD-for-games") mapping between the "transition systems" $\initialTS{\TS}{\rInit(\tilde{I})}$ and $\initialTS{\TS'}{\tilde{I}}$; that is, the "transitions systems" obtained by setting $\rInit(\tilde{I})$ and $\tilde{I}$ as "initial vertices", respectively.

For arbitrary "acceptance conditions", enlarging the set of "initial vertices" does not preserve "history-determinism@@mapping". 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 <ref>.

Let $\TS$ and $\TS'$ be two "TS" such that all their states are "accessible", and let $\pp\colon \TS \to \TS'$ be an "HD@@mapping" (resp. "HD-for-games") mapping between them. If $\WW$ and $\WW'$ are "prefix-independent", the mapping $\pp$ is also "HD@@mapping" (resp. "HD-for-games") when considered between the "transition systems" $\initialTS{\TS}{V}$ and $\initialTS{\TS'}{V'}$, consisting of the "transition systems" $\TS$ and $\TS'$ where all the states are set to be "initial@@state".

§.§ 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 <ref>).
Then, we prove that these mappings witness the semantic equivalence of the "transition systems" under consideration. That is, (1) if $\pp\colon \A\to \A'$ is an "HD mapping" "of automata@@morph", then $\Lang{\A} = \Lang{\A'}$, and if $\pp$ is "locally bijective", $\A$ is "deterministic" (or "unambiguous") if and only if $\A'$ is (Proposition <ref>); and (2) if $\pp\colon \G\to \G'$ is an "HD-for-games mapping", $\G$ and $\G'$ have the same "winner" (Proposition <ref> and Corollary <ref>).

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\compositionAut \A$ "recognises" the same language than $\B$, if $\A$ is not "history-deterministic" (Proposition <ref>). In that case, the equality $\Lang{\B\compositionAut \A} = \Lang{\B}$ follows from the idea that "runs" in $\B$ can be simulated in $\B\compositionAut \A$ “guided by the non-deterministic choices of $\A$”, which we do not formalise in this work.

*Morphisms generalise composition by an automaton

Let $\A$ be a "complete" "automaton" "accepting@@automaton" the language $\Lang{\A} = \WW\subseteq \SS^\oo$, and let $\TS$ be a "(labelled) TS" with "acceptance set" $\WW$.
Then, there exists a "locally surjective" "weak morphism of (labelled) TS" $\pp\colon \TS \compositionAut \A \to \TS$ that "preserves accepting runs". Moreover:

* If $\A$ is "deterministic", $\pp$ can be chosen to be a "locally bijective morphism".

* If $\A$ is "HD@@aut", then $\pp$ can be chosen to be an "HD mapping".

* If $\A$ is "HD@@aut" and $\TS$ is a "game" "suitable for transformations", then $\pp$ can be chosen to be an "HD-for-games mapping".

We recall that the set of states of $\TS \compositionAut \A$ is $V\times Q$ and its set of transitions $\edgesProduct$ is a subset of $(E\times \DD) \sqcup E$, where $V$ and $Q$ (resp. $E$ and $\DD$) are the states (resp. transitions) of $\TS$ and $\A$, respectively.
We let $\WW_\A\subseteq \GG^\oo$ be the "acceptance set" of $\A$.
We define $\pp_V(v,q) = v$ and $\pp_E(e_1,e_2) = e_1$ for $(e_1,e_2)\in E\times \DD$ and $\pp_E(e_1) = e_1$ for $e_1\in E$.
It is immediate to check that $\pp$ is a "weak morphism".

Given a "run" $\rr = (v_0,q_0) \re{c_0}  (v_1,q_1) \re{c_1} \dots$ in $\TS \compositionAut \A$, we can consider its projection over $\TS$, $\ppRuns(\rr) = v_0 \re{a_0}  v_1 \re{a_1} \dots$. We note that there must exist a unique "run" in $\A$ of the form

\[ \pp_\A(\rr) = q_0 \re{a_0:c_0}  q_1 \re{a_1:c_1} \dots .\]

(Formally, some of the letters $a_i$ might equal $\ee$, and in this case $q_{i} \re{a_i:c_i}  q_{i+1}$ does not appear in the "run" $\pp_\A(\rr)$).

We show that $\pp$ "preserves accepting runs". Let $\rr$ be an "accepting run" in $\TS\compositionAut \A$. In that case, $c_0c_1c_2\dots \in \WW_\A$, and therefore $\pp_\A(\rr)$ is an "accepting run" in $\A$ over $a_0a_1a_2\dots$, so we conclude that $a_0a_1a_2\dots\in \WW$ and $\ppRuns(\rr)$ is an "accepting run" in $\TS$.

We prove next the "local surjectivity" of $\pp$. Clearly, $\pp$ induces a surjection between the "initial vertices" of $\TS \compositionAut \A$ (which are $I_\TS \times I_\A$) and those of $\TS$.
Let $(v,q)\in V\times Q$ and $e_1 = v\re{a}v'\in E$. If $a=\ee$, the edge $e_1$ belongs to $\edgesProduct$ and $\pp(e_1)=e_1$. If $a\neq \ee$, since $\A$ is "complete" there is a transition $e_2 = q\re{a}q'\in \DD$ and $\pp(e_1,e_2) = e_1$, so $\pp$ is "locally surjective".

* Since $\A$ has a single "initial state" $q_0$, $\pp$ induces a bijection between the "initial vertices" of $\TS \compositionAut \A$ (which are $I_\TS \times \{q_0\}$) and those of $\TS$.
Let $\edgesProduct_\mathrm{col}\subseteq E\times \DD$ and $\edgesProduct_\ee\subseteq E$ such that $\edgesProduct = \edgesProduct_\mathrm{col} \cup \edgesProduct_\ee$. We remark that $\restr{\pp}{\edgesProduct_\ee}$ is the identity function (so injective) and that $\pp(\edgesProduct_\mathrm{col}) \cap \pp(\edgesProduct_\ee) = \emptyset$ because $\pp(\edgesProduct_\mathrm{col})$ are exactly "coloured" transitions of $\TS$. Finally, let $(e_1, e_2)$ and $(e_1', e_2')$ in $\mout(v,q) \cap \edgesProduct_\mathrm{col}$. Their $\pp(e_1, e_2) = \pp(e_1', e_2')$ if and only if $e_1 = e_1'$. Let $a\in \SS$ 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 $\pp$ is "locally injective".

Let $\rr$ be a "rejecting run" in $\TS\compositionAut \A$ (we use the notations introduced above). In that case, $c_0c_1c_2\dots \notin \WW_\A$, and therefore $\pp_\A(\rr)$ is a "rejecting run" over $a_0a_1a_2\dots$. Since $\A$ is "deterministic", this is the only "run over" $a_0a_1a_2\dots$ so we conclude that it does not belong to $\WW.$ We conclude that $\ppRuns(\rr)$ is a "rejecting run" in $\TS$.

* Let $(r_0, r_\A)$ be a "resolver" for $\A$. We define a "resolver@@HDmapping" $(\rInit, r_\pp)$ "simulating" $\pp$. First, we let $\rInit(v_0) = (v_0,r_0)$ for all $v_0\in I_\TS$. We define $r_\pp\colon {\edgesProduct}^*\times E \to \edgesProduct$ by induction on the length of the "runs".
Let $e_0 = v_0\re{a}v_1\in \mout(v_0)$ be an edge in $\TS$. If $e_0$ is "uncoloured" ($a=\ee$), we let $r_\pp(\ee, e_0) = e_0 = (v_0,r_0)\re{\ee}(v_1,r_0)$. If not, we let $r_\pp(\ee, e_0) = (e_0, e_a)$, where $e_a = r(\ee,a)$.
Suppose that $r_\pp$ has been defined for sequences of edges of $\TS \compositionAut \A$ of length $< n$ and let  $\rr =e_0e_1\dots e_{n-1}\in {\edgesProduct}^*$ be a sequence length $n+1$ and $e_\TS = v_n\re{a_n} v_{n+1}$ be an edge in $\TS$.
If $\rr$ is not a "run" or if it does not end in $\inv{\pp}(v_n)$, we let $r_\pp(\rr, e_\TS)$ be any edge in $\inv{\pp}(e_\TS)$.
Suppose that $\rr$ is a "run" ending in $\inv{\pp}(v_n)$. If $a_n = \ee$, we define $r_\pp(\rr, e_\TS) = e_\TS$. As noted before, $\rr$ induces a "run" $\pp_\A(\rr) = q_0 \re{a_0:c_0}  q_1 \re{a_1:c_1} \dots \re{}q_n$ in $\A$. We let $e_\A = r_\A(\pp_\A(\rr), a_n)$ be the transition chosen by the "resolver" of $\A$ after this "run",  and we define $r_\pp(\rr, e_\TS) = (e_\TS, e_\A)$.

It directly follows from this definition that $(\rInit, r_\pp)$ is indeed a "resolver". The proof that if $\rr\in \Runs{\TS}$ is an "accepting run" then $\rRunsOption{\pp}(\rr)$ is "accepting" follows the same lines than the previous item.

* We prove that, if $\TS$ is a "game" "suitable for transformations", the "resolver@@HDmapping" $(\rInit, r_\pp)$ defined in the previous item is "sound for $\TS$". We claim that if $\rr$ is a "run" in $\TS$, the only "run" "consistent with@@resolver" $(\rInit, r_\pp)$ over $\rr$ is $\rRunsOption{\pp}(\rr)$. This follows from the fact that if $(v,q)$ is a vertex in $\TS \compositionAut\A$ "controlled by Adam" and $e\in \mout(v)$, then there is a unique $e'\in \mout(v,q)$ such that $\pp(e') = e$. This is indeed the case: as $\TS$ is "suitable for transformations", if $v$ is an "Adam's vertex", every $e\in \mout(v)$ is "uncoloured", so by definition of $\pp$ we have that $\pp(e') = e \implies e'=e$. (This can be seen as that $\pp$ is locally bijective in Adam's vertices).
We conclude that if $\rr$ is an "accepting run" in $\TS$ and $\rr^\ltimes$ is a "run" "consistent with@@resolver" $(\rInit, r_\pp)$ over $\rr$, then $\rr^\ltimes = \rRunsOption{\pp}(\rr)$, which is "accepting" by "soundness@@morph" of the "resolver@@mapping" $(\rInit, r_\pp)$.

*Morphisms witness equivalence of automata

Let $\A$, $\A'$ be two "automata" over the same "input alphabet" such that there is an "HD mapping" of "automata@@mapping" $\pp\colon \A \to \A'$. Then, $\Lang{\A}=\Lang{\A'}$, and $\A$ is "HD@@aut" if and only if $\A'$ is "HD@@aut".
If $\pp$ is moreover "locally bijective" and "surjective", $\A$ is "deterministic" (resp. "complete") if and only if $\A'$ is.

Since $\pp$ "preserves accepting runs", it is clear that $\Lang{\A}\subseteq \Lang{\A'}$. Since $\pp$ admits a "sound resolver@@morph" $(\rInit, r)$, if $\rr$ is an "accepting@@run" "run over" $w\in \SS^\oo$ in $\A'$, then $\rRuns(\rr)$ is an "accepting@@run" "run over" $w$ in $\A$, so $\Lang{\A'}\subseteq \Lang{\A}$.

Let $(\rInit, r_\pp)$ be a "sound@@morph" "resolver simulating" $\pp$.
Suppose that $\A$ is "HD@@aut", admitting a "resolver" $(r_0,r)$. A "resolver" $(r_0',r')$ for $\A'$ can be obtained just by composing $r_\pp$ and $\pp$, that is: $r_0' = \pp(r_0)$ and for $\rr'\in \RunsFin{\A'}$ and $a\in \SS$, $r'(\rr', a) = \pp(r(\rRunsOption{\pp}(\rr'),a)))$. That is, given a "run" $\rr'$ in $\A'$, we simulate it in $\A$ using $r_\pp$, 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 $\pp$.
Suppose now that $\A'$ is "HD@@aut" and that $(r_0',r')$ is a "resolver" for it. We define a "resolver" $(r_0,r)$ for $\A$. We let $r_0 = \rInit(r_0')$, and for $\rr\in \RunsFin{\A}$ and $a\in \SS$, $r(\rr, a) = r_\pp((\ppRuns(\rr), r(\ppRuns(\rr),a))$. That is, given a "run" $\rr$ in $\A$, we simulate it in $\A'$ using $\pp$, 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_\pp$.
It is a direct check that the "resolvers" defined this way witness that $\A'$ and $\A$, respectively, are "HD@@aut".

The proof that $\A$ is "deterministic" (resp. "complete") if and only if $\A'$ is "deterministic" (resp. "complete"), assuming "surjectivity" and "local bijectivity" of $\pp$, 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 <cit.> for a detailed exposition). An automaton is ""unambiguous"" if for every input word $w\in \SS^\oo$ 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 <ref>, "locally bijective morphisms" also preserve "(strongly) unambiguity": if $\pp\colon \A \to \A'$ is a "locally bijective" "morphism@@aut" then $\A$ is ("strongly@@unamb") "unambiguous" if and only if  $\A'$ is.

*Morphisms preserve winning regions of games

Let $\G, \G'$ be two "games", such that there is a "weak morphism" "of games@@morphism" $\pp\colon \G \to \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 $\pp(v)$.

Let $v' = \pp(v)$, and let $\strat_v\colon \PathSetFin{\G}{v}\to E$ be a "strategy" from $v$ for Eve in $G$.
Intuitively, we will define a "strategy" in $\G'$ as follows: for each finite run $\rr'$ from $v'$ in $\G'$, we pick a preimage $\rr\in \inv{\pp}(\rr')$ in $\G$, look at the decision made by $\strat_v$ at the end of $\rr$ and transfer it back to $\G'$ via $\pp$. 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 $\choicestrat \colon \PathSetFin{\G'}{v'} \to \PathSetFin{\G}{v}$ satisfying that for any $\rr' = e_0'e_1'\dots e_{n-1}'e_n'\in \PathSetFin{\G'}{v'}$:

* The run $\choicestrat(\rr')$ has length $n+1$.

* $\ppRuns(\choicestrat(\rr')) = \rr'$.

* Monotonicity: if $\tilde{\rr}' \prefix \rr'$ then $\choicestrat(\tilde{\rr}') \prefix \choicestrat(\rr')$.

* If there exists $e_n\in \inv{\pp}(e_n')$ such that $\choicestrat(e_0'e_1'\dots e_{n-1}')e_n$ is "consistent with@@strat" $\strat_v$, then $\choicestrat(\rr')$ is "consistent with@@strat" $\strat_v$.

Assume for now that such a function exists, and define a "strategy" in $\G'$ as
\[\strat'_{v'}(\rr') = \pp(\strat_v(\choicestrat(\rr'))), \;\text{ for } \rr'\in \PathSetFin{\G'}{v'}.\]

We prove that $\strat'_{v'}$ is "winning@@strat".
Let $\rr' =e_0'e_1'\dots\in \Runs{\G'}$ be an infinite "play" "consistent with@@strat" $\strat'_{v'}$. For each finite prefix $\tilde{\rr'}\prefix \rr'$, $\choicestrat(\tilde{\rr'})$ is a finite play in $\G$, and by the monotonicity assumption, we can define the limit of these runs as:

\[ \vec{\rr} = e_0e_1e_2\dots \in \Runs{\G}, \;\text{ where } e_0e_1\dots e_n = \choicestrat(e_0'e_1'\dots e_n'),  \]

which is indeed a "run" in $\G$. We show that $\vec{\rr}$ is "consistent with" $\strat_v$ by induction. Let $\rr_n = e_0e_1\dots e_{n-1}$ be the "prefix" of size $n$ of $\vec{\rr}$, and suppose that it ends in a vertex $v_n$ controlled by "Eve". We want to show that $e_n = \strat_v(\rr_n)$. By definition of $\strat'_{v'}$, $e_n' = \pp(\strat_v(\rr_n)) = \pp(e_n)$, and as $v_n$ is controlled by "Eve", $\strat_v(\rr_n)$ is the only continuation of $\rr_n$ "consistent with" $\strat_v$, so by the last property of $\choicestrat$, $e_n$ has to coincide with $\strat_v(\rr_n)$, as we wanted. As $\vec{\rr}$ is "consistent with" the "winning strategy" $\strat_v$, it is an "accepting run" in $\G$, and since $\pp$ "preserves accepting runs", $\rr' = \ppRuns(\vec{\rr})$ is also an "accepting run".

Finally, we show how to build a function $\choicestrat \colon \PathSetFin{\G'}{v'} \to \PathSetFin{\G}{v}$ by induction on the length of the runs. Suppose that $\choicestrat$ has been defined for "runs" of length $\leq n$, and let $e_0'e_1'\dots e_n'$ be a run of length $n+1$, with $\choicestrat(e_0'e_1'\dots e_{n-1}') = e_0e_1\dots e_{n-1}$. If $e_0e_1\dots e_{n-1}$ is not "consistent with" $\strat_v$, it ends in a vertex $v_n$ controlled by "Adam", or $\strat_v(e_0e_1\dots e_{n-1})\notin \inv{\pp}(e_n)$,  we let $e_n\in \inv{\pp}(e_n)\cap \mout(v_n)$ be any edge (one such edge exists by "local surjectivity").
On the contrary, we let $e_n = \strat_v(e_0e_1\dots e_{n-1})$.
We define $\choicestrat(e_0'e_1'\dots e_{n-1}'e_n') = e_0e_1\dots e_{n-1}e_n$.
By construction, the obtained function fulfils the 4 requirements.

Let $\G, \G'$ be two "games" such that there is an "HD-for-games mapping" $\pp\colon \G \to \G'$. "Eve's" "winning region" in $\G'$ is the projection of her "winning region" in $\G$: $\winRegion{\Eve}{\G'} = \pp(\winRegion{\Eve}{\G})$.

If "Eve" "wins" $\G$ from an "initial vertex" $v$, Lemma <ref> guarantees that she "wins" $\G'$ from $\pp(v)$.

Suppose now that "Eve" "wins" $\G'$ from an "initial vertex" $v'$ with a "strategy" $\strat'_{v'}\colon \PathSetFin{\G'}{v'}\to E'$. We need to show that she "wins" $\G$ from some "initial vertex" in $\inv{\pp}(v')$. Let $(\rInit,r)$ be a "resolver simulating" $\pp$ "sound for $\G$" and let $v=\rInit(v')$.  We define

\[\strat_{v}(\rr) = r(\rr, \strat'_{v'}(\ppRuns(\rr)), \; \text{ for } \rr\in \PathSetFin{\G}{v}.\]

That  is, $\strat_{v}$ is a "strategy" in $\G$ from $v$ that, given a finite run $\rr$, simulates $\rr$ 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@@morphism" $r$. We prove that $\strat_{v}$ is "winning for Eve" in $\G$. Let $\rr = e_0e_1\dots\in \PathSet{\G}{v}$ be a "play" consistent with $\strat_{v}$. We claim that $\pp(\rr)$  is "consistent with@@strat" $\strat'_{v'}$ and that $\rr$ is "consistent with@@resolver" $(\rInit,r)$ over $\pp(\rr)$. This implies the desired result; "consistency with@@strat" $\strat'_{v'}$ implies that $\pp(\rr)$ is "accepting", and since $(\rInit,r)$ is "sound for $\G$", $\rr$ would be "accepting@@run" in $\G$.

We prove that $\pp(\rr)$ is "consistent with@@strat" $\strat'_{v'}$. Let $e_0'e_1'\dots e_{n-1}'$ be a subplay of $\pp(\rr)$ ending in a vertex $v_n$ "controlled by Eve". By definition of the strategy $\strat_{v}$, we have that $e_n = r(e_0\dots e_{n-1}, \strat'_{v'}(e_0'\dots e_{n-1}'))$, and by definition of a "resolver@@mapping" (item <ref>), $e_n' = \pp(e_n) = \strat'_{v'}(e_0'\dots e_{n-1}'))$, as we wanted.

The fact that $\rr$ is "consistent with@@resolver" $(\rInit,r)$ over $\pp(\rr)$ follows directly from the definition of $\strat_{v}$.

The next corollary follows from the previous proposition and Lemma <ref>.

Let $\G, \G'$ be two "games" whose states are "accessible" and such that their "acceptance sets" $\WW_\G$ and $\WW_{\G'}$ are "prefix-independent". If there is an "HD-for-games mapping" $\pp\colon \G \to \G'$, then "Eve's" "full winning region" in $\G'$ is the projection of her "full winning region" in $\G$: $\winRegion{\Eve}{\initialTS{\G'}{V'}} = \pp(\winRegion{\Eve}{\initialTS{\G}{V}})$.

§ 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" <cit.>.
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 <ref>, we describe the construction of a minimal "deterministic" "parity" "automaton" $\zielonkaAutomaton{\F}$ for a given "Muller language" $\Muller{\F}$. Theorem <ref>, the main contribution of this section, states the minimality of $\zielonkaAutomaton{\F}$ both amongst "deterministic" and "HD@@aut" "parity" "automata". Theorem <ref> states the optimality on the number of "colours" of the "acceptance condition" of $\zielonkaAutomaton{\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" $\zielonkaAutomaton{\F}$ to provide a polynomial-time algorithm minimising "DPAs" "recognising" "Muller languages" in Section <ref>.

In Section <ref>, we describe the construction of a minimal "history-deterministic" "Rabin" "automaton" $\zielonkaHDAutomaton{\F}$ for a "Muller language" $\Muller{\F}$. Its minimality amongst "HD@@aut" "automata" is shown in Theorem <ref>, by using the characterisation of the "memory requirements" of a "Muller language" in terms of its "Zielonka tree" <cit.>.

On the other hand, it has been shown that finding a minimal "deterministic" "Rabin" "automaton" "recognising" a given "Muller language" is $\NPcomplete$, if the language is represented by a "parity" or "Rabin" "automaton", or even by its "Zielonka tree" <cit.>.
Therefore, unless $\PTime = \NP$, there are "Muller languages" for which minimal "deterministic" "Rabin" automata are strictly larger than minimal "HD@@aut" "Rabin" "automata". Some explicit such languages were shown in <cit.>.
A summary of the minimal automata "recognising" "Muller languages" appears in Table <ref>.

Type of automata      "Deterministic"      "History-"

"Parity"	      $\zielonkaAutomaton{\F}$       $\zielonkaAutomaton{\F}$

"Rabin"	     $\NPcomplete$        $\zielonkaHDAutomaton{\F}$

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

Let $\F\subseteq\powplus{\SS}$ be a family of non-empty subsets over a finite set $\SS$. A ""Zielonka tree"" for $\F$ (over $\SS$), denoted $\intro*\zielonkaTree{\F} = (N, \ancestor, \intro*\nu :N \to \powplus{\SS})$ is a "$\powplus{\SS}$-labelled tree" with nodes partitioned into ""round nodes"" and ""square nodes"", $N= \intro*\roundnodes \sqcup \intro*\squarenodes$, such that:

* The "root" is labelled $\SS$.

* If a "node" is labelled $X\subseteq \SS$, with $X\in\F$, then it is a "round node", and it has a child for each maximal non-empty subset $Y\subseteq X$ such that $Y\not\in\F$, which is labelled $Y$.

* If a "node" is labelled $X\subseteq \SS$, with $X\not\in\F$, then it is a "square node", and it has a child for each maximal non-empty subset $Y\subseteq X$ such that $Y\in\F$, which is labelled $Y$.

The definition of $\zielonkaTree{\F}$, as well as most subsequent definitions, do not only depend on $\F$ but also on the alphabet $\SS$. 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.

We note that for each family of subsets $\F\subseteq\powplus{\SS}$, there is only one "Zielonka tree" up to renaming of its nodes, so we will talk of the "Zielonka tree" of $\F$.

We remark that if $n$ is a node of $\zielonkaTree{\F}$, then the "subtree of $\zielonkaTree{\F}$ rooted at $n$" is the "Zielonka tree" for the family $\restSubsets{\F}{\nu(n)}$ over the alphabet $\nu(n)$, that is, for the restriction of $\F$ to the subsets included in the label of $n$.

Let $n$ be a node of $\zielonkaTree{\F}$ and let $n_1$ be a "child" of it. If $\nu(n_1) \subsetneq X \subseteq \nu(n)$, then $\nu(n_1)\in \F \iff X\notin \F \iff \nu(n)\notin \F$. In particular, if $n_1, n_2$ are two different "children" of $n$, then
$\nu(n_1)\in \F \iff \nu(n_2)\in \F \iff \nu(n_1)\cup \nu(n_2)\notin \F$.

We equip "Zielonka trees" with an "order@@tree" to navigate in them. That is, we equip each set $\children_{\zielonkaTree{\F}}(n)$ with a total order, making $\zielonkaTree{\F}$ an "ordered tree". The precise order considered will be irrelevant for our purposes.
From now on, we will suppose that all "Zielonka trees" are "ordered", without explicitly mentioning it.

For a "leaf" $l \in \leaves(\zielonkaTree{\F})$ and a letter $a\in \SS$ we define $\intro*\supp(l,a) = n$ to be the "deepest" "ancestor" of $l$ (maximal for $\ancestor$) such that $a\in \nu(n)$.

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

\[ \F = \{\{a,b\}, \{a,c\}, \{b\}\}. \]

In Figure <ref> 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(\xi, c) = \lambda$ and $\supp(\xi, b) = \aa$ .
Also, $\jump(\xi, \lambda)=\zeta$  is the "leaf" reached by going from $\xi$ to $\lambda$, then changing to the next branch (in a cyclic way) and re-descend by taking the leftmost path. Similarly, $\jump(\xi,\aa)=\theta$.

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

Zielonka tree $\zielonkaTree{\F}$ for
$\F=\{ \{a,b\}, \{a,c\}, \{b\}\}$.

§.§ 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" $\zielonkaTree{\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" $\zielonkaTree{\F}= (N, \ancestor, \nu)$.
We let $\intro*\parityNodes: N \to \NN$ be the function defined as:

* if $\SS\in \F$, $\parityNodes(n)=\depth(n)$,

* if $\SS\notin \F$, $\parityNodes(n)=\depth(n) + 1$.

We let $\intro*\minparityZ{\F}$ (resp. $\intro*\maxparityZ{\F}$) be the minimum (resp. maximum) value taken by the function $\parityNodes$.

A node $n$ in the "Zielonka tree" $\zielonkaTree{\F}$ verifies that $\parityNodes(n)$ is even if and only if $\nu(n)\in \F$.
If $\SS\in \F$, $\minparityZ{\F} = 0$ and $\maxparityZ{\F}$ equals the "height" of the "Zielonka tree" minus one. If $\SS\notin \F$, $\minparityZ{\F} = 1$ and $\maxparityZ{\F}$ equals the "height" of the "Zielonka tree".

The "Muller language" from Example <ref> satisfies $\SS\notin \F$. The values taken by the function $\parityNodes$ are represented at the right of the "Zielonka tree" in Figure <ref>. We have $\parityNodes(\aa)=1$, $\parityNodes(\bb)=\parityNodes(\lambda) = 2$ and $\parityNodes(\theta) = \parityNodes(\xi) = \parityNodes(\zeta) = 3$, so $\minparityZ{\F}=1$ and $\maxparityZ{\F}=3$.

Given a family of non-empty subsets $\F\subseteq \powplus{\SS}$,

we define the  ""ZT-parity-automaton"" $\intro*\zielonkaAutomaton{\F}=(Q, \SS, q_0, [\minparityZ{\F}, \maxparityZ{\F}], \transAut{}, \parity)$ as the "deterministic" "parity" "automaton" given by:

* $Q=\leaves(\zielonkaTree{\F})$,

* $q_0$ is the "leftmost" "leaf" of $\zielonkaTree{\F}$,

* The transition reading $a\in\SS$ from $q\in Q$ goes to $\jump(q,\supp(q,a))$  and produces $\parityNodes(\supp(q,a))$ as "output", that is,
\[\transAut{}(q,a) = \left(\jump(q,\supp(q,a)), \parityNodes(\supp(q,a))\right).\qedEx\]

Any state can be chosen as "initial state" (see Lemma <ref>).

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 $\parityNodes(n)$, determined by the "depth" of $n$.

In Figure <ref> we show the "ZT-parity-automaton" $\zielonkaAutomaton{\F}$ of the family of subsets from Example <ref>.

"ZT-parity-automaton" "recognising" the "Muller language associated to" $\F=\{ \{a,b\}, \{a,c\}, \{b\}\}$.

*Correctness of the Zielonka-tree-parity-automaton

Let $\F\subseteq \powplus{\SS}$ be a family of non-empty subsets. Then,

\[ \Lang{\zielonkaAutomaton{\F}} = \MullerC{\F}{\SS}. \]

That is, a word $w\in \SS^\oo$ is "accepted@@word" by $\zielonkaAutomaton{\F}$ if and only if $\minf(w)\in \F$.

The following useful lemma follows directly from the definition of $\supp$ and $\jump$.

Let $q$ be a "leaf" of $\zielonkaTree{\F}$ and let $n$ be a node "above" $q$. Then, $\supp(q, a)$ is a "descendant" of $n$ if and only if $a\in \nu(n)$, and in this case, $\jump(q,\supp(q,a))$ is a "descendant" of  $n$ too.

Let $w = w_0w_1w_2\dots \in \SS^\oo$ be an infinite word. For $i>0$, let

$q_i$ be the "leaf" of $\zielonkaTree{\F}$ reached after the (only) "run over" $w_0w_1\dots w_{i-1}$ in $\zielonkaAutomaton{\F}$.
For $i\geq 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 = \parityNodes(n_i) = \gg(q_i, w_i) \in [\minparityZ{\F}, \maxparityZ{\F}]$ be that output colour (the "output" of the "run over" $w$ being therefore $c_0c_1c_2\dots \in \NN^\oo$).
Let $q_\infty$ be a node appearing infinitely often in the sequence $q_0q_1q_2\dots$, and let $n_w$ be the "deepest" "ancestor" of $q_\infty$ such that $\minf(w)\subseteq \nu(n_w)$.
There is $K\in \NN$ such that for all $i \geq K$, $q_i \descendant n_w$ and $\supp(q_i, w_i) \descendant n_w$. In particular, $c_i \geq \parityNodes(n_w)$ for $i\geq K$.

Let $K\in \NN$ be a position such that $w_i \in \minf(w)$ for all $i\geq K$ and $q_K = q_\infty$.
The claim follows from Lemma <ref> and induction.

Let $n_{w,1},\dots, n_{w,s}$ be an enumeration of $\children_{\zielonkaTree{\F}}(n_w)$ "from left to right". It is verified that:

* $\supp(q_i,w_i) = n_w$ infinitely often. In particular, $c_i = \parityNodes(n_w)$ for infinitely many $i$'s.

* There is no $n_{w,k}\in \children(n_w)$ such that $\minf(w) \subseteq \nu(n_{w,k})$.

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) \descendant n_{w,k}$, and by Lemma <ref>, $\minf(w)\subseteq \nu(n_{w,k})$. In particular, $q_\infty$ is "below" $n_{w,k}$, contradicting the fact that $n_w$ is the "deepest" "ancestor" of $q_\infty$ containing $\minf(w)$.

Let $K$ be like in the Claim <ref>.
We show that if $i\geq K$ and $q_i\descendant n_{w,k}$, then there is $j> i$ such that $w_j\notin \nu(n_{w,k})$, $\supp(q_{j},w_{j}) = n_{w}$ and $q_{j+1}\descendant n_{w,k+1}$ (by an abuse of notation we let $s+1 = 1$).
It suffices to consider the least $j \geq i$ such that $\supp(q_{j},w_{j})\nsucceq n_{w,k}$ (which exists by the previous remark). Since $\minf(w)\subseteq \nu(n_w)$ we have that $\supp(q_{j},w_{j}) = n_{w}$, so $w_j\notin \nu(n_{w,j})$ (by Lemma <ref>) and by definition of the transitions of $\zielonkaAutomaton{\F}$, $q_{j+1}$ will be a "leaf" "below" $n_{w,k+1}$.

The fact that $q_{j+1}\descendant n_{w,k+1}$ implies that for any child $n_{w,k'}$, infinitely many states $q_i$ will be below $n_{w,k'}$ (we go around the children in a round-robin fashion). Therefore, for any $k$, there are arbitrarily large $j$ such that $w_j\notin \nu(n_{w,j})$ and $\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 $\parityNodes(n_w)$. By Remark <ref>, $\parityNodes(n_w)$ is even if and only if $n_w$ is a "round node" (if $\nu(n_w)\in \F$). It remains to show that $\minf(w) \in \F$ if and only if $\nu(n_w)\in \F$, which holds by the second item in Claim <ref> and Remark <ref>.

§.§.§ Optimality of the Zielonka-tree-parity-automaton

We now state and prove the main results of this section: the optimality of the "ZT-parity-automaton" in both number of states (Theorem <ref>) and number of "colours" of the "acceptance condition" (Theorem <ref>).
The minimality of the "ZT-parity-automaton" comes in two version. A weaker one states its minimality only amongst "deterministic" "automata" (Theorem <ref>), and a stronger one states its minimality amongst all "history-deterministic"  "automata" (Theorem <ref>). 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

The "parity index" of a "Muller language" $\MullerC{\F}{\SS}$ is $[\minparityZ{\F}, \maxparityZ{\F}]$. That is, the "ZT-parity-automaton" of $\MullerC{\F}{\SS}$ uses the optimal number of colours to recognise this language.

Let $\A$ be a "history-deterministic" "parity" "automaton" "recognising@@automaton" a "Muller language" $\MullerC{\F}{\SS}$. Then, $|\zielonkaAutomaton{\F}|\leq \size{\A}$.

For every "Muller language" $L$, a minimal "deterministic" "parity" "automaton" "recognising" $L$ has the same size than a minimal "HD@@aut" "parity" "automaton" "recognising" $L$.

We remark that, nonetheless, there are non-trivial "HD@@aut" "parity" "automata" "recognising" "Muller languages". The automaton provided in Example <ref> is an "HD@@aut" "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 $\DD'\subseteq \DD$ of its transitions and an "initial state" $q_0$ such that the "subautomaton induced" by $\DD'$ with initial state $q_0$ is "deterministic" and "recognises" $\Lang{\A}$.

There exists an  "HD@@aut" "parity" "automaton" "recognising" a "Muller language" that is not "determinisable by prunning".

*Optimality of the parity condition

Let $L= \MullerC{\F}{\SS}$.
The "ZT-parity-automaton" of $L$ is a "parity" "automaton" recognising $L$ using colours in $[\minparityZ{\F}, \maxparityZ{\F}]$, therefore, the "parity index@@atMost" of $L$ is at most $[\minparityZ{\F}, \maxparityZ{\F}]$.

To prove that the "parity index is not less" than $[\minparityZ{\F}, \maxparityZ{\F}]$, we use the Flower Lemma <ref>. The language $L$ is trivially recognised by a "deterministic" "Muller" "automaton" $\A_L$ with just one state $q$, transitions $q\re{a:a}q$ for each $a\in \SS$, and "acceptance condition" given by $L$ itself. Let $n_1\ancestor n_2\ancestor \dots \ancestor n_d$ be a branch of maximal length of $\zielonkaTree{\F}$ (that must verify $d= \maxparityZ{\F} - \minparityZ{\F}$, and that the "root" $n_1$ is a "round node" if and only if $\minparityZ{\F}$ is even). If we let $\ell_i$ be the "cycle" in $\A_L$ containing exactly the transitions corresponding to letters in $\nu(n_i)$, we obtain that $\ell_1\supsetneq \ell_2\supsetneq \dots \supsetneq \ell_d$ is a "$d$-flower" over $q$, which is "positive@@flower" if and only if  $n_1$ is a "round node". Lemma <ref> allows us to conclude.

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

Before presenting the proof of Theorem <ref>, 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.

Let $\A$ be a "DPA"  "recognising@@automaton" a "Muller language" $\MullerC{\F}{\SS}$. Then, $|\zielonkaAutomaton{\F}| \leq \size{\A}$.

We recall that, by Remark <ref> and Lemma <ref>, 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, \SS, I, \GG, \Delta, \WW)$ be an "automaton", and let $X\subseteq \SS$ be a subset of the "input alphabet".
We say that a "subgraph" $\S$ of the "underlying graph" of $\A$ is ""$X$-closed@@automaton"" if for every state $q$ in $\S$ and every letter $a\in X$ there is some transition $q\re{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\subseteq Q$ is the set of states of an "$X$-FSCC" if and only if:

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

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

Let $\A$ be a "complete" "automaton". For every subset $X\subseteq \SS$, $\A$ contains an "accessible@@set" "$X$-FSCC".

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@@aut" of $\A$, one such "final SCC" has to be an "$X$-closed" "subgraph", so it is an "$X$-FSCC".

Let $\A$ be a "DMA" "recognising" a "Muller language" $\MullerC{\F}{\SS}$, let $X\subseteq \SS$ and let $\S_X$ be an "accessible@@set" "$X$-FSCC" of $\A$. Then, the "automaton induced by" $\S_X$ is a "deterministic" "automaton" "recognising" $\MullerC{\restSubsets{\F}{X}}{X} = \{w\in X^\oo \mid \minf(w)\in \F\}$.

Let $\A = (Q,\Sigma, q_0, \Gamma, \transAut{}, \WW)$ (where $\WW$ is a "Muller language"). Let $q_S$ be the state in $\S_X$ chosen to be "initial", and let $u_0\in \SS^*$ be a finite word such that the "run over" $u_0$ from $q_0$ ends in $q_S$.
By "prefix-independence" of "Muller languages", a word $w\in X^\oo$ belongs to $\MullerC{\F}{\SS}$ if and only if $u_0w\in \MullerC{\F}{\SS}$, and therefore, $\A$ "accepts@@aut" $w$ if and only if it "accepts@@aut" $u_0w$.
Since the "run@@aut" in $\A$ over $u_0w$ and the "run@@aut" in $\S_X$ over $w$ have a suffix in common, and by "prefix-independence" of $\WW$, we have that $w\in \Lang{\S_X}$ if and only if $u_0w\in \Lang{\A}$ if and only if $\minf(w)\in \F$.

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

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

Let $\gg\colon \DD\to \NN$ be the "colouring function" of $\A$. The "cycles" $\ell_1$ and $\ell_2$ are "accepting@@cycle" if and only if $d_i = \min \gg(\ell_i)$ is even, for $i=1,2$. In this case, $\min \gg(\ell_1 \cup \ell_2) = \min\{ d_1, d_2\}$ is even. The proof is symmetric if $\ell_1$ and $\ell_2$ are "rejecting@@cycle".

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

Let $\F\subseteq \powplus{\SS}$ be a family of subsets with "Zielonka tree" $\zielonkaTree{\F} = (N, \ancestor, \nu)$, and let $\A$
be a "DPA" "recognising" $\MullerC{\F}{\SS}$. Let $n\in N$ be a node of the "Zielonka tree" of $\F$, and let $n_1, n_2\in \children_{\zielonkaTree{\F}}(n)$ be two different "children" of $n$. If $\S_1$ and $\S_2$ are two "accessible@@sets" "$\nu(n_1)$-FSCC" and "$\nu(n_2)$-FSCC" in $\A$, respectively, then $\S_1\cap \S_2 = \emptyset$.

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_\SS\colon \DD \to \SS$ be the labelling of the transitions of $\A$ with "input letters".
Let $\S_i$ be a "$\nu(n_i)$-FSCC" in $\A$, for $i=1,2$, and let $\ell_i$ be its set of edges, which form a "cycle" satisfying $l_\SS(\ell_i) = \nu(n_i)$.
Suppose by contradiction that $\S_1\cap \S_2 \neq \emptyset$. Then $\ell_1$ and $\ell_2$ have some state in common, and their union is also a "cycle" satisfying $l_\SS(\ell_1\cup\ell_2) = \nu(n_1)\cup \nu(n_2)$. By Lemma <ref>, we must have

\[ \ell_1 \text{ "accepting" } \iff \ell_1\cup \ell_2 \text{ "accepting"},\]

contradicting the fact that $\nu(n_1)\in \F$ if and only if $\nu(n_1)\cup \nu(n_2)\notin \F$ (Remark <ref>).

We proceed by induction in the "height" of $\zielonkaTree{\F}$. For "height" $1$, the result is trivial, since $|\zielonkaAutomaton{\F}| = 1$.
Let $\A$ be a "DPA" "recognising" $\MullerC{\F}{\SS}$. Let $n_0$ be the "root" of $\zielonkaTree{\F}$ and $n_1, n_2, \dots, n_k$ be an enumeration of the "children" of $n_0$ in $\zielonkaTree{\F}$.
By Lemma <ref>, for each $i\in \{1, \dots, k\}$, $\A$ contains some "accessible" "$\nu(n_i)$-FSCC" $\S_i$, and by Lemma <ref> these must be pairwise disjoint. By Lemma <ref>, each $\S_i$ induces a "deterministic" "subautomaton@@induced" "recognising" $\MullerC{\restSubsets{\F}{\nu(n_i)}}{\nu(n_i)}$. Let $\Z_i$ by the "subtree of $\zielonkaTree{\F}$ rooted at" $n_i$, which we recall that is the "Zielonka tree" for $\restSubsets{\F}{\nu(n_i)}$. By induction hypothesis, it must be the case that $|\leaves(\Z_i)| \leq |\S_i|$, so we can conclude:

\[ |\zielonkaAutomaton{\F}| = |\leaves(\zielonkaTree{\F})| = \sum\limits_{i=1}^k |\leaves(\Z_i)| \leq  \sum\limits_{i=1}^k |\S_i| \leq |\A|.\qedhere\]

*Minimality of the ZT-parity-automaton with respect to HD automata
We intend to prove Theorem <ref>, that is, that for any $\F\subseteq \powplus{\SS}$, the automaton $\zielonkaAutomaton{\F}$ is minimal amongst "HD@@aut" "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@@aut" "parity" "automaton" for $\Muller{\F}$ and that $n_0$ is the "root" of $\zielonkaTree{\F}$ having $n_1, \dots, n_k$ as "children". For each "child" $n_i$ we want to find an "HD@@aut" "subautomaton" $\A_i$ "recognising" the "language associated@@Muller" to $\restSubsets{\F}{\nu(n_i)}$ 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| \geq |\leaves(\zielonkaTree{\F})| = |\zielonkaAutomaton{\F}|$. Our objective will be therefore to prove:

Let $n_0$ be the "root" of the "Zielonka tree" of $\F$, and let $n_1, n_2, \dots, n_k$ be an enumeration of the "children" of $n_0$. If $\A$ is an "HD automaton" "recognising" $\MullerC{\F}{\SS}$, then, $\A$ contains $k$ pairwise disjoint "subautomata" $\A_1, \dots, \A_k$ that are "history-deterministic" and such that $\Lang{\A_i} = \MullerC{\restSubsets{\F}{\nu(n_i)}}{\nu(n_i)}$.

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@@aut" 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" ($\SS\in \F$) or "square" ($\SS\notin \F$).