In the context of two-player games over graphs, a language $L$ is called half-positional if, in all games using $L$ as winning objective, the protagonist can play optimally using positional strategies, that is, strategies that do not depend on the history of the play.
In this work, we describe the class of parity automata recognising half-positional languages, providing a complete characterisation of half-positionality for $\omega$-regular languages.
As corollaries, we establish decidability of half-positionality in polynomial time,   finite-to-infinite and 1-to-2-players lifts, and show the closure under union of prefix-independent half-positional objectives, answering a conjecture by Kopczyński.

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

§ INTRODUCTION

§.§ Context: Strategy complexity in infinite duration games

We study games in which two antagonistic players, that we call Eve and Adam, take turns in moving a token along the edges of a given (potentially infinite) edge-coloured directed graph. Vertices of the graph are partitioned
into those belonging to Eve and those belonging to Adam; when the token lands in a vertex, it is the owner of this vertex who chooses where to move next. This interaction goes on in a non-terminating mode, producing an infinite path in the graph called a "play". The winner of such a play is determined according to a language of infinite sequences of colours $W$, called the "objective" of the game; plays producing a sequence of colours in $W$ are winning for Eve, and plays that do not satisfy the "objective" $W$ are winning for the opponent Adam.

One of the central applications of "games" on graphs is the problem of reactive synthesis: given a system interacting with its environment and a formal specification, we want to obtain a controller for the system ensuring that the specification is met.
The interaction between the system and the environment can be modelled as a game where a winning strategy corresponds to a correct implementation of a controller <cit.>.

In this context, a crucial parameter is the complexity of "strategies" required by the players to "play optimally". Games admitting simple strategies are both easier to solve algorithmically, and the controllers obtained for them can be represented succinctly.

Positional strategies.
The simplest "strategies" are "positional@@strat" ones, those that depend only on the current vertex, and not on the history of the "play".
In this work, we are interested in the following question: Given a fixed "objective" $W$, is it the case that players can "play optimally using positional strategies" in all "games" that have $W$ as "winning objective"?
We can ask this question just for one player (player "Eve") – we say in the affirmative case that $W$ is "half-positional" – or for both players – we say that $W$ is "bipositional". Also, it might be relevant to consider the question for subclasses of games, in particular, for finite games, or for 1-player games.

The class of "bipositional" "objectives", both over finite and infinite games, is already well understood.
A characterisation of "bipositionality" over finite games was obtained by Gimbert and Zielonka <cit.>, using two properties called monotonicity and selectivity. An important and useful corollary of their result is what is commonly known as a 1-to-2-player lift: an objective $W$ is "bipositional" over finite games if and only if both players can "play optimally using positional strategies" in finite 1-player games.

Over infinite games, a very simple and elegant characterisation of "bipositionality" was given by Colcombet and Niwiński for "prefix-independent" objectives <cit.>: a "prefix-independent" objective $W$ is "bipositional" if and only if it is the "parity objective".
In particular, these objectives are necessarily "$\oo$-regular".
No such characterisation is known for non-"prefix-independent" objectives (although a generalisation of this result for finite memory without the "prefix-independent" assumption is studied in <cit.>).

Although "half-positionality" is arguably more relevant than "bipositionality" in the context of reactive synthesis (the controller is built basing on "Eve's" "strategies"), much less is known for this class.
During the 90s, "half-positionality" of some central objectives was proved, notably of "parity@@obj" <cit.> and Rabin languages <cit.>,
but the first thorough study of "half-positionality" was conducted by Kopczyński in his PhD thesis <cit.>.
There, he provides some sufficient conditions for "half-positionality" (which were generalised in <cit.>) and introduces an important set of conjectures that have greatly influenced research in the area in the recent years.
However, no general characterisation was found for "half-positionality".

Recently, Ohlmann made a step forward by providing a characterisation of "half-positionality" by means of the existence of graph-theoretical structures known as "monotone@@graph" "universal graphs" <cit.>.
While this characterisation is a valuable tool for proving "half-positionality", it is not constructive and does not directly yield decidability results.
Also, Ohlmann's result comes with a caveat: necessity of the existence of "universal graphs" for "half-positional" objectives is only guaranteed for those containing a "neutral letter" (a letter that does not change membership to $W$ after its removal).
He conjectures that this restriction is not essential, as the addition of a "neutral letter" to any objective should not break "half-positionality".

$\oo$-regular languages.
A central class of languages over infinite words is the class of "$\oo$-regular languages", which admits several alternative definitions: these are the languages "recognised" by "deterministic" "parity automata", by "non-deterministic" "Büchi automata", definable using $\oo$-expressions, or using monadic second order logic <cit.>.

One of the main contributions of Kopczyński was to show decidability of "half-positionality" over finite games for "prefix-independent" "$\oo$-regular objectives" <cit.>.
His procedure works by enumerating all possible arenas where positionality might fail (up to a sufficiently large size); it runs in $\O(n^{\O(n^2)})$ time, and does not reveal much about the structure of automata "recognising" "positional" languages.

Regarding "half-positionality" over arbitrary games and for non-"prefix-independent" "objectives", characterisations have been found for some subclasses of "$\oo$-regular" "objectives".
For "closed objectives" (objectives recognised by safety automata), "half-positionality" was characterised by Colcombet, Fijalkow and Horn in 2014 <cit.>.

Recently, a characterisation of "half-positionality" for languages "recognised" by "deterministic" "Büchi automata" was provided by Bouyer, Casares, Randour and Vandenhove <cit.> (see also Proposition.
As a corollary, they establish polynomial-time decidability of "half-positionality" for  "deterministic" "Büchi automata".
However, the conditions they provide are not necessary for "half-positionality" in general, for instance, for languages "recognised" by "coBüchi automata".

Finite-to-infinite and 1-to-2-player lifts.
As mentioned above, a consequence of Gimbert and Zielonka's result <cit.> is that, in order to check "bipositionality" over finite games, it suffices to check whether players can "play optimally" in 1-player games.
Recently, generalisations of 1-to-2-player lifts have been studied in the setting of finite memory by Kozachinskiy <cit.> and Vandenhove <cit.>.
Vandenhove conjectures that if $W$ is "half-positional" over "Eve-games" (resp. over finite games), then $W$ is "half-positional" over all games <cit.>.
This conjecture has been shown to hold in the case of languages "recognised" by "deterministic" "Büchi automata" <cit.>.

Closure under union.
One of the recurring themes in Kopczyński's PhD thesis <cit.> is the following question.

Let $W_1,W_2\subseteq \SS^\oo$ be two "prefix-independent" "half-positional" objectives. Then $W_1\cup W_2$ is "half-positional".

Very recently, Kozachinskiy <cit.> disproved this conjecture, but only for "half-positionality" over finite games. Also, the counter-example he gives is not "$\oo$-regular".
On the positive side, "Kopczyński's conjecture" has been proved to hold for "objectives" "recognised" by "deterministic" "Büchi automata" <cit.>, as well as for the family of $\SigmaTwo$ objectives (objectives "recognised" by infinite "coBüchi automata") <cit.>. "Kopczyński's conjecture" and this latter result have been generalised to the setting of finite memory <cit.>.
Solving "Kopczyński's conjecture" over infinite games is one of the driving open questions for the field.

§.§ Contributions and organisation

Our main contribution is a characterisation of "half-positionality" for "$\oo$-regular languages", stated in Theorem <ref>.
We propose a syntactic description of a family of "deterministic" "parity automata", so that any automaton in this class "recognises" a "half-positional" language, and any "half-positional" language can be "recognised" by such an automaton.
In fact, we describe two slightly different such families, called, respectively, "fully progress consistent" "signature automata" and "$\ee$-completable" automata. These families offer distinct advantages and complement our intuitions on "half-positionality".

From this characterisation, we derive multiple corollaries that address the majority of open questions related to "half-positionality" in the case of "$\oo$-regular languages":

* Decidability in polynomial time. Given a "deterministic" "parity automaton" $\A$, we can decide in polynomial time whether $\Lang{\A}$ is "half-positional" or not (Theorem <ref>).

* Finite-to-infinite and 1-to-2-players lift. An "$\oo$-regular" objective $W$ is "half-positional" over arbitrary games if and only if it is "half-positional" over finite, "$\ee$-free" "Eve-games" (Theorem <ref>). This answers a question raised by Vandenhove <cit.>.

* Closure under union. The union of two "$\oo$-regular" "half-positional" objectives is "half-positional", provided that one of them is "prefix-independent" (Theorem <ref>). This solves a stronger variant of "Kopczyński's conjecture" in the case of "$\oo$-regular languages".

* Closure under addition of a neutral letter. If $W$ is "$\oo$-regular" and "half-positional", the objective obtained by adding a "neutral letter" to $W$ is "half-positional" too (Theorem <ref>). This solves "Ohlmann's conjecture" in the case of "$\oo$-regular languages".

We obtain some additional results pertaining to classes of objectives that are not necessarily "$\oo$-regular". We relax the "$\oo$-regularity" hypothesis in two orthogonal ways.

* Characterisation of bipositionality of all objectives. We extend the characterisation of "bipositionality" of Colcombet and Niwiński <cit.> to all objectives, getting rid of the "prefix-independence" assumption (Theorem <ref>).

* Characterisation of half-positionality of closed and open objectives.
We characterise "half-positionality" for "closed@@obj" and "open@@obj" objectives. We also obtain as corollaries 1-to-2 players lifts and closure under addition of a "neutral letter" for these classes of objectives.

§.§.§ Technical tools
We would like to highlight some technical tools that take primary importance in our proofs.

Universal graphs. In general, showing that a given objective is "half-positional" can be challenging, as we need to show that for every game "Eve" can "play optimally using positional strategies".
Ohlmann's characterisation using "monotone@@graph" "universal graphs" provides a painless path to prove "half-positionality" (see Proposition <ref>).
We rely on this result to show that "parity automata" satisfying the syntactic conditions imposed in Theorem <ref> do indeed "recognise" "half-positional" languages.

History-deterministic automata. "History-deterministic" automata are a model in between "deterministic" and "non-deterministic" ones; we refer to <cit.> for detailed expositions on them.
Although the statements of our results do not mention "history-determinism", they appear naturally in two different parts of our proofs:

* Establishing necessity of the syntactic conditions from our main characterisation requires a very fine control of the structure of automata. We develop a technique for decomposing automata, for which we need to use and generalise the methods introduced by Abu Radi and Kupferman <cit.> for the minimisation of "HD" "coBüchi automata".

* To show the sufficiency of these conditions, we build a "monotone@@graph" "universal" graph from a "signature automaton". To facilitate this process, we first “saturate” automata, adding as many transitions as possible without modifying the languages they "recognise". This procedure generates non-determinism, but preserves "history-determinism", the key property that allows us to prove "universality" of the obtained graph.

We believe that this use of "history-determinism" showcases their usefulness and canonicity.

Normal form of parity automata. In our central proof, we rely on a "normal form" of parity automata, as defined in <cit.>.
Automata in "normal form" present a set of properties that simplify manipulating them and reasoning about their runs.
We make consistent use of these properties in our combinatorial arguments.
The use of this "normal form", or variants of it, is common in the literature,
and finds application in diverse contexts, such as the study of "history-deterministic" "coBüchi" "automata" <cit.> or automata learning <cit.>.

Congruences for parity automata. Since the beginning of the theory of finite automata, the notion of "congruence" has played a fundamental role <cit.>.
Here, we propose a notion of "congruences" for parity automata that make it possible to build quotient automata that are compatible with the acceptance condition. This newly introduced vocabulary allows us to formalise the details of the proof of Theorem <ref> in a simpler way.
We believe that it will be useful for the study of "parity automata" in other contexts.

§.§.§ Organisation of the paper

Given the technical complexity of this paper, the decisions regarding its presentation have been done with the utmost focus on clarity, aiming to help the reader understand the contributions, as well as the newly introduced definitions and techniques.
To this end, we have incorporated many examples and intuitive explanations, including a dedicated warm-up section. Consequently, the paper's length has expanded, and some aspects of its organisation might have deviated from conventional choices.

After introducing some general definitions and terminology used throughout the paper, we begin Section <ref> by stating the characterisation result (Theorem <ref>) and its main consequences, without providing formal details about the technical concepts appearing in its statement.  Section <ref> is a warm-up for the definitions used in the main characterisation and for the techniques used in its proof. We gradually introduce conditions that are necessary for "half-positionality", obtaining partial results and providing numerous examples along the way.
Section <ref> contains the most technical part of the paper. We introduce the notions of "signature automata", "full progress consistency" and "$\ee$-complete automata" appearing in the statement of Theorem <ref>, and we give a proof of it. Nevertheless, most details in the proof of necessity are relegated to Appendix <ref>.
In Section <ref> we provide two conceptually different polynomial-time decision methods for deciding "half-positionality".
Sections <ref> and <ref> contain, respectively, the two last contributions of the paper: a characterisation of "bipositionality" for all objectives and a characterisation of "half-positionality" for "open" and "closed" objectives.
The proofs appearing in these latter sections are much simpler.

§ PRELIMINARIES

We introduce definitions and notations used throughout the paper. First we introduce in Section <ref> "games" and "positionality", as well as the more technical notion of "universal graphs" used in our proofs for "positionality". In Section <ref> we introduce definitions about "parity automata" and notions about "congruences" for them.

The reader who does not plan to get into the more technical details of Sections <ref> and <ref> can skip Subsections <ref> and <ref> from this preliminaries. Also, the hyperlinks on words should help the reader to easily refer to the definitions.

§.§ Games and positionality

§.§.§ Games on graphs

A ""$\SS$-graph"" $G$ is given by a (potentially infinite) set of vertices $V$ together with a set of coloured directed edges $E\subseteq V\times \SS \times V$.
We write $v \re c v'$ to refer to an edge in $G$ with source $v$, target $v'$, and colour $c$.
This notation naturally extends to finite and infinite paths.

The ""size@@graph"" of a graph $G$ is defined to be the cardinality of $V$.

We assume throughout the paper that "$\Sigma$-graphs" do not contain ""sinks"", that is, every vertex has at least one outgoing edge. (This assumption is useful when considering infinite paths.)

A ""game"" is an edge-coloured "graph" together with a set of winning sequences of colours and a partition of the vertices into those controlled by a ""player"" named ""Eve"" and her opponent, named ""Adam"".
Formally, it is represented by a tuple $\G = \left(V,E, \intro*\VEve, W\right)$, where $G=(V,E)$ is a "$\SS\cup\{\ee\}$-graph" (called the ""game graph""),  $\VEve$ is the set of vertices owned by "Eve" and $W\subseteq \SS^\oo$ is the ""winning objective"".
Letter $\ee$ is a fresh element used to represent ""uncoloured edges""; we impose that no infinite path in $G$ is composed exclusively of $\ee$-edges.
Games not containing "uncoloured edges" are called ""$\ee$-free"".
We let $\intro*\VAdam = V\setminus \VEve$ be the vertices controlled by "Adam".
An ""Eve-game"" is a "game" $\G$ in which all the vertices are controlled by "Eve", that is, $V = \VEve$.
A "game" having $W$ as "winning objective" is called a ""$W$-game"".

Unless stated otherwise, we take the point of view of player "Eve"; expressions as “winning” will implicitly stand for “winning for Eve”, and "strategies" will be defined for her.

In this paper, the words “language” and “""objective""” are synonyms.

In a game, players move a pebble from one vertex to another for an infinite amount of time.
The player who owns the vertex $v$ where the pebble is placed chooses an edge  $v\re{c}v'$ and the pebble travels through this edge to its target, producing colour $c$. In this way, they produce a path $\rr=v_0\re{c_0}v_1\re{c_1}v_2\re{c_2}\dots\in E^\oo$, that we call a ""play"".
Such a "play" is ""winning@@play"" (for "Eve") if the sequence $w\in \SS^\oo$ obtained by removing from $c_0c_1c_2\dots$ the occurrences of $\ee$ belongs to $W$. We say that it is ""losing@@play"" (or winning for Adam) on the contrary.

Strategies and winning regions.
A ""strategy"" (for "Eve") is a function $\strat: E^* \to E$,  that tells "Eve" which move to choose after any possible "finite play".
We say that a "play" $\rr\in E^\oo$ is ""consistent with the strategy"" $\strat$ if after each finite prefix $\rr' \sqsubset \rr$ ending in a vertex controlled by "Eve", the next edge in $\rr$ is $\strat(\rr')$.
We say that the strategy $\strat$ is ""winning from@@strat"" a vertex $v\in V$ if all infinite "plays" starting in $v$ "consistent with" $\strat$ are "winning@@play". If such a "strategy" exists, we say that "Eve" ""wins $\G$ from $v$"".
Strategies for "Adam" are defined symmetrically.

The ""winning region"" of a game $\G$, written $\intro*\winRegion{\Eve}{\G}$, is the set of vertices $v\in V$ such that "Eve" "wins" $\G$ from $v$.
We say that a "strategy" is ""optimal (for Eve)"" if it is "winning@@strat" from all vertices in $\winRegion{\Eve}{\G}$.

"Eve" always has an "optimal strategy", that is,
there is a strategy $\strat_{\mathsf{opt}}$ that is "winning from" all $v\in \winRegion{\Eve}{\G}$.

We say that a game $\G$ is ""determined"" if either "Eve" or "Adam" have a "winning strategy from $v$", for every vertex $v$.
In this work, all "games" will be "determined", as by Martin's theorem <cit.> games using Borel "objectives" are "determined", and all "objectives" that we will consider (for instance, all "$\omega$-regular objectives") are Borel.

Graphical representation of games.

We use circles to represent vertices controlled by "Eve" and squares to represent those controlled by "Adam".
We will allow ourselves to consider games with edges labelled by finite words $w=w_1w_2\dots w_n\in \SS^*$. Formally, such transitions will stand for a sequence of $n$ transitions, with $n-1$ intermediate vertices.
We represent this kind of transitions by a wiggly arrow.

We will also use this notation for infinite words: for $w\in \SS^\oo$ we write $v\lrp{w\phantom{.}}$ for an infinite sequence of edges labelled with the letters of $w$ starting from $v$. In this case, the resulting "game graph" is necessarily infinite.

§.§.§ Positionality

Positional strategies.

We say that a "strategy" $\strat: E^* \to E$ is ""positional@@strategy"" if there exists a mapping $\ss\colon \VEve\to E$ such that for every finite "play" $\rr=v_0\re{c_0}\dots \re{c_{n-1}} v_n$  ending in a vertex $v_n$ controlled by "Eve" we have:

\[ \strat(\rr) = \ss(v_n). \]

That is, a "strategy" is "positional@@strat" if the choice of the next transition only depends on the current position, and not on the history of the path.

We say that "Eve" (resp. Adam) can ""win positionally"" from a subset $A\subseteq V$ if there is a "positional strategy" that is "winning" from any vertex in $A$.
We say that "Eve" (resp. Adam) can ""play optimally in $\G$ using a positional strategy"" if she can "win positionally" from her "winning region".

Our notion of "positionality" uses what sometimes are called ""uniform strategies"", that is, we require that a single "positional strategy" suffices to win independently of the initial vertex.
This notion is strictly stronger than the non-uniform version in which we allow to use different "strategies" depending on the initial vertex.
Said differently, Remark <ref> does not hold if we require "strategies" to be "positional".
See Figure <ref> for an example.

Positional objectives.

An "objective" $W\subseteq \SS^\oo$ is ""half-positional"" if for every "$W$-game", "Eve" can "play optimally using positional strategies".  We say that $W$ is ""bipositional@@objective"" if both $W$ and $\SS^\oo\setminus W$ are "half-positional", or, equivalently, if both "Eve" and "Adam" can "play optimally using positional strategies" in "$W$-games".
If $\mathcal{X}$ is a subclass of $W$-games (notably, finite, "$\ee$-free" and "Eve-games"), we say that $W$ is  ""half-positional over $\mathcal{X}$ games"" if for every "$W$-game" in $\mathcal{X}$, "Eve" can "play optimally using positional strategies".
The same terminology is used for "bipositionality".

As in other definitions, the notion of "half-positionality" depends not only on the set $W$, but also on the set of colours $\SS$. As the set of colours will always be clear from the context, we omit including $\SS$ in the notations.

Consider the game above, where "Eve" controls both vertices $v_1$ and $v_2$. Let $W = ab(a+b)^\oo$ be the "winning condition" of the game, that is, "Eve" "wins" if the play starts by $ab$. She has two "positional strategies" $\strat_1$ and $\strat_2$ "winning" from $v_1$ and $v_2$, respectively. However, no "positional strategy" is winning from the entire "winning region" $\{v_1,v_2\}$.

§.§.§ Universal graphs

We now introduce "universal graphs", which will serve as our main tool for deriving "positionality" results.

Morphisms of $\SS$-graphs.
Given two "$\SS$-graphs" $G=(V,E)$ and $G'=(V',E')$, a ""morphism of $\SS$-graphs@@univ"" $\phi$ from $G$ to $G'$ is a map $\phi:V\to V'$ such that for each edge $v \re c v' \tin G$, it holds that $\phi(v) \re c \phi(v')$ defines an edge in $G'$.
We write $\phi:G \to G'$ to denote that $\phi$ is a "morphism@@univ".

Given a "$\SS$-graph" $G$, a vertex $v$ of $G$ and an "objective" $W \subseteq \SS^\omega$, we say that ""$v$ satisfies@@univ"" $W$ in $G$ if for any infinite path $v \lrp{w\phantom{.}} \tin G$, it holds that $w \in W$.
Given a cardinal $\kappa$, a graph $U$ is ""$(\kappa,W)$-universal"" if all graphs $G$ of size $<\kappa$ admit a "morphism@@univ" $\phi:G \to U$ such that any vertex $v$ that "satisfies@@univ" $W$ in $G$ is mapped to a vertex $\phi(v)$ that "satisfies@@univ" $W$ in $U$.

A ""totally ordered graph"" (resp. ""well-ordered graph"") is a graph $G$ together with a total order (resp. well-order) $\leq$ on its vertex set $V$.
Such a graph is called ""monotone@@univ"" if

\[
u\leq v, \, v'\leq u' \tand u \re c u' \tin G \; \implies \; v \re c v' \tin G.
\]

We often note the conditions on the left by $v \geq u \re c u' \geq v'$.

We now state our main tool for proving "half-positionality".

Let $W \subseteq \SS^\oo$ be an "objective". If for
all cardinals $\kappa$ there exists a "$(\kappa, W)$-universal" "well-ordered@@univ" "monotone@@univ"  graph, then $W$ is
"half-positional" over all "games".

Universality for trees.

It is often more convenient to work with trees.
A ""$\SS$-tree"" is a "$\SS$-graph" $T$ with a distinguished vertex $t_0$, called the ""root@@univ"", and such that every vertex $t$ of $T$ admits a unique path from the root.
Since graphs (and in particular trees) are assumed sinkless, trees are always infinite.
We say that a tree $T$ ""satisfies@@treeUniv"" $W$ if its root $t_0$ "satisfies@@univ" $W$ in $T$.

We say that a graph $U$ is ""$(\kappa,W)$-universal for trees"" if all "trees@@univ" $T$ of size $<\kappa$ which "satisfy@@treeUniv" $W$ admit a "morphism@@univ" $\phi\colon T \to U$ mapping the "root@@univ" $t_0$ to a vertex $\phi(t_0)$ that "satisfies@@univ" $W$ in $U$.

Given an "ordered@@univ" "$\SS$-graph" $U$, we let $\intro*\UTop{U}$ be the "$\SS$-graph" obtained by adding a fresh vertex $\top$, maximal for the order of the graph, with transitions $\top \re a v$ for every $a\in \SS$ and every vertex $v$ of the graph.
The following useful result follows directly from the proof of <cit.> (see also <cit.>).

Let $W \subseteq \SS^\omega$ be an "objective" and $\kappa$ a cardinal.
If $U$ is a  a "well-ordered@@graph" "monotone graph@@univ" that is "$(\kappa,W)$-universal for trees", then $\UTop{U}$ is "well-ordered@@graph" "monotone@@univ" "$(\kappa,W)$-universal"  (for graphs).

Therefore, thanks to Proposition <ref>, building graphs that are "universal for trees" suffices to prove positionality.

Universal graph for the parity objective.

As an important example, we give a "universal graph" for the "parity objective"; it is implicit in the works of Emerson and Jutla <cit.> and Walukiewicz <cit.>. In the latter, the term signatures  was used to name tuples of ordinals ordered lexicographically (term first used in <cit.>).
Such a tuple is meant to count, for each odd priority, how many times it is seen before a stronger (even or odd) priority.

[""Universal graph for the parity objective""]
Consider the ""parity objective"" over $[0,d]$, (we assume $d$ even):

\[
\intro*\parity_{} = \{w \in \{0,\dots,d\}^\oo \mid \liminf w \text{ is even}\}.
\]

Fix a cardinal $\kappa$. We define a graph $\intro*\UPar$ having as set of vertices tuples $(\lambda_1,\lambda_3,\dots,\lambda_{d-1}) \in \kappa^{d/2}$ that we consider ordered lexicographically. This is indeed a "well-order". We let its edges be:

\[
(\lambda_1,\dots,\lambda_{d-1}) \re x (\lambda'_1,\dots,\lambda'_{d-1}) \iff \begin{cases}
(\lambda'_1,\dots,\lambda'_{x-1}) \leq (\lambda_1,\dots,\lambda_{x-1})  &\tif x \text{ is even}, \\
(\lambda'_1,\dots,\lambda'_{x}) < (\lambda_1,\dots,\lambda_{x}) &\tow.
\end{cases}
\]

Where the order between truncated tuples as on the right is also the lexicographic one.
A representation of the graph $\UPar$ appears in Figure <ref>.

Clearly, $\UPar$ is "monotone@@univ".
We show in Lemma <ref> below that all vertices in $\UPar$ "satisfy@@univ" $\parity$. Lemma <ref> states that $\UPar$ is  "$(\kappa,\parity)$-universal for trees", so, by Lemma <ref>, $\UTop{\UPar}$ is a "well-ordered@@graph" "monotone@@univ" "$(\kappa,\parity)$-universal" graph.

"Universal graph" $\UPar$ for the "parity objective" over "priorities" $[0,5]$.
Vertices are ordered from left to right.
Edges between two boxes $B_1 \re{x} B_2$ represent that there are edges $v_1\re{x} v_2$ for all $v_1\in B_1$ and all $v_2\in B_2$.
Edges obtained by monotonicity are not represented: if $v\re{x}v'$ and $v''\leq v'$, then $v\re{x}v''$ too; for example, by reading colour $5$ from a vertex $v$ one can go to any vertex strictly on the left of $v$.
Edges coloured $0$ are not depicted in the figure: they appear between every pair of vertices.
The label of a box represents the forms of the names of vertices inside it.

Every infinite path in $\UPar$ "satisfies@@graph" the "objective" $\parity$.

Consider an infinite path $\rr = (\lambda_1^1,\dots,\lambda_{d+1}^1) \re{w_1} (\lambda_1^2,\dots,\lambda_{d+1}^2) \re{w_2} \dots$ in $\UPar$. Let $x$ be the minimal priority appearing infinitely often in $\rr$, which we assume odd for contradiction.
Then, from some position, no priority $>x$ is read, thus the sequence of prefixes $(\lambda_1^i,\dots,\lambda_{x}^i)$ is decreasing and moreover strictly decreases in infinitely many places.
This contradicts well-foundedness of the lexicographical order over tuples of ordinals.

Graph $\UPar$ is "$(\kappa,\parity)$-universal for trees".

Take a "tree@@univ" $T$ of size $<\kappa$ which "satisfies@@treeUniv" $\parity$; note that by "prefix-independence", all vertices in $T$ "satisfy@@univ" $\parity$.
We aim to construct a "morphism@@univ" $\phi:T \to \UPar$.

Fix a vertex $t \in T$ and an odd priority $y \in \{1,3,\dots,d-1\}$.
Then, in any path $t \lrp{w\phantom{.}}$ in $T$ there are only finitely many occurrences of $y$ before a smaller priority appears.
We may define an ordinal $\intro*\rankOrd_y(t)$ capturing the number of such occurrences: $\rankOrd_y(t)$ satisfies that, if $t'$ is an $x$-sucessor of $t$ (that is, $t\re{x}t'$), then:

* $\rankOrd_y(t')\leq \rankOrd_y(t)$, if $y<x$, and

* $\rankOrd_y(t')< \rankOrd_y(t)$ if $x=y$.

One easily verifies that $\phi:v \mapsto (\rankOrd_1(v),\rankOrd_3(v),\dots,\rankOrd_{d-1}(v))$ defines a "morphism@@univ" from $T$ to $\UPar$.

§.§ Automata over infinite words

§.§.§ Parity automata

A ""(non-deterministic) parity automaton"" over the alphabet $\SS$ is represented by a tuple $\A = (Q,\Sigma, q_\init, \DD, \intro*\colAut)$, where $Q$ is a set of states, $\SS$ is a set of letters called the ""input alphabet"", $q_\init$ is the ""initial state"", $\DD\subseteq Q\times \SS \times Q$ is a set of transitions, and $\colAut\colon \DD \to [d_{\min},d_{\max}]$ is a function assigning numbers to transitions; we refer to this numbers as ""priorities"".

We write $q\re{a:x}q'$ to indicate that there is a transition $e=(q,a,q')\in\DD$ with $\colAut(e)=x$.

We refer to transitions of a "parity automaton" labelled with "priority" $x\in \NN$ as ""$x$-transitions@@out"". Similarly, we refer to transitions having input letter $a\in \SS$ as ""$a$-transitions@@in"". The difference between the two uses of the term will always be clear from the context.
An "automaton" $\A' = (Q',\Sigma', q'_\init, \DD', \colAut')$ is a ""subautomaton"" of $\A$ if $Q'\subseteq Q$, $\DD'\subseteq \DD$ and $\colAut'$ is the restriction of $\colAut$ to $\DD'$.

For a state $q\in Q$, we write $\intro*\initialAut{\A}{q}$ to denote the automaton obtaining by setting $q$ as "initial state".

We assume in all the paper that all automata are ""complete"", that is if for every $q\in Q$ and $a\in \Sigma$, there is at least one transition $q\re{a:s}$.

A ""strongly connected component"" (shortened SCC) of an automaton $\A$ is a maximal set of states $S\subseteq Q$ such that any pair of states in $S$ are interreachable. We say that it is ""trivial@@SCC"" if it is a singleton.
A state $q$ is ""recurrent"" if it belongs to some "non-trivial" "SCC", and ""transient"" otherwise.

An ""automaton structure"" $\S$ is an "automaton@@parity" without colouring function $\colAut$, and $\A$ is a ""parity automaton on top of"" $\S$ if it has been obtained by defining a colouring $\colAut$ on $\S$.

Runs and recognisability.

A  ""run over"" an infinite word $w=a_0a_1a_2\dots\in \SS^\oo$ in $\A$ is a path

\[\rr = q_\init \re{a_0:x_0}q_1\re{a_1:x_1}q_2\re{a_2:x_2}\dots\in \DD^\oo.\]

It is ""accepting@@run"" if

\[ \min \{x\in \NN \mid x = x_i \text{ for infinitely many } i\}	\; \text{ is even},   \]

and ""rejecting@@run"" if the minimal "priority" produced infinitely often is odd.
A word $w\in \SS^\oo$ is  ""accepted@@word"" by $\A$ if there exists an "accepting@@runAut" "run over $w$".
The ""language 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 to be ""equivalent@@aut"".
A language is called ""$\oo$-regular"" if it can be "recognised" by a "parity" automaton.

For an even "priority" $x$, we say that a word $w\in \SS^\oo$ can be ""accepted with priority $x$"" in $\A$ if there exists a "run over $w$" such that the minimal "priority" produced infinitely often is $x$.
For an odd priority $x$, we say that $w$ ""is rejected with priority $x$"" if the minimal "priority" produced infinitely often in every "run over $w$" is $x$.
Note that a word which is "rejected" does not have to be rejected by with some odd priority.

We emphasise that in our definition, the acceptance condition is put over the transitions of the automata. This will be a crucial element in our characterisation. We refer to <cit.> for further discussions on the comparison between transition-based and state-based automata.

Büchi and coBüchi automata.

A ""Büchi automaton"" is a "parity automaton" using $[0,1]$ as its set of "priorities".
"Parity automata" using $[1,2]$ as set of "priorities" are called ""coBüchi@@aut"".
We say that a language $W$ is ""Büchi recognisable"" (resp. ""coBüchi recognisable"") if it can be "recognised" by a "deterministic" "Büchi automaton"  (resp. "deterministic" "coBüchi automaton"). We note that these classes are incomparable and strict subclasses of the "$\oo$-regular languages".

For $u\in\SS^*$, we write $\intro*\infOften(u)$ (resp. $\intro*\finOften(u)$) to denote the language of infinite words containing infinitely often (resp. finitely often) the factor $u$. We note that these languages are "Büchi@@rec" and "coBüchi recognisable", respectively.
We also write $\intro*\noOcc(u)$ for the language of infinite words avoiding any occurrence of the factor $u$.

Determinism and homogeneity.

We say that an "automaton" $\A$ is ""deterministic"" if for every $q\in Q$ and $a\in \Sigma$, there is only one $a$-transition $q\re{a:x}$ outgoing from $q$.
Let $\DD'\subseteq \DD$ be a subset of transitions of an "automaton" $\A$. We say that $\A$ is ""deterministic over $\DD'$"" if the restriction of $\A$ to $\DD'$ is "deterministic", that is, for each letter $a$, there is a most one outgoing "$a$-transition@@out" in $\DD'$ from each state.
Any "parity" automaton admits an "equivalent" "deterministic" one <cit.>.

We say that a "parity automaton" $\A$ is ""homogeneous"" if for every state $q\in Q$ and letter $a\in \SS$, if $q\re{a:x}p$ is a transition in $\A$, then any other "$a$-transition@@in" from $q$ produces "priority" $x$.

Let $\A$ be an "homogeneous" "parity automaton" that is "deterministic over" transitions producing priority $x$. If $q\re{a:x}p$ is a transition in $\A$, then there is no other "$a$-transition@@out" outgoing from $q$ in $\A$.

Notations for paths.

For two states $q, p$ of a "parity automaton" $\A$ and a finite word $w\in \SS^*$, we write $q\lrp{w:x}p$ if there exists a path from $q$ to $p$ labelled $w$ such that the minimal priority appearing on it is $x\in \NN$.
We write $q\lrp{w:\geq x}p$ to denote that there exists such a path producing no "priority" strictly smaller than $x$. This is possibly the empty path $q\re{\ee}q$, producing no priority.
We use similar notations for $\leq x$, $<x$ and $>x$.
We generalise these notations for infinite paths: for an infinite word $w\in \SS^\oo$ we write $q\lrp{w:x}$ if there exists an infinite path from $q$ labelled $w$ such that the minimal priority seen on it is $x$.

We may apply this notations to "non-deterministic" automata – hence the use of an existential quantification – though in most cases we will work with "deterministic" ones.

History-deterministic automata.

Let $\A= (Q,\Sigma, q_\init, \DD,\colAut)$ be a (non-deterministic) "parity automaton".
A ""resolver@@aut"" for $\A$ is a function $\resolv\colon \DD^* \times \SS \to \DD$ such that, for all words $w = a_0a_1\dots \in \SS^\oo$, the sequence $e_0e_1\dots \in \DD^\oo$, called the ""run induced by@@aut"" $\resolv$ over $w$ and defined by $e_i = \resolv(e_0\dots e_{i-1}, a_i)$, is actually a "run over" $w$ in $\A$.
We write $q_\init \intro*\lrpResolver{\resolv}{w:x} q$ to denote that the "run induced by@@aut" $\resolv$ over $w$ produces $x$ as minimal priority and lands in $q$.

We say that the resolver is ""sound@@aut"" if it satisfies that, for every $w\in \Lang{\A}$, the "run induced by@@aut" $\resolv$ over $w$ is an "accepting run@@aut".
In other words, $\resolv$ should be able to construct an "accepting run@@aut" 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) if there is a "sound resolver@@aut" for it. "History-deterministic" automata are sometimes called good-for-games in the literature, we refer to <cit.> for a discussion on the relation between these notions and a survey on them.

Normal form of parity automata

Let $\A = (Q,\Sigma, q_\init, \DD, \colAut)$ be a "parity automaton". We say that a labelling $\colAut'\colon \DD \to [d_{\min}',d_{\max}']$ is ""equivalent to@@labelling"" $\colAut$ over $\A$ if for every cycle $\ell\subseteq \DD$, $\min \colAut(\ell)$ is even if and only if $\min \colAut'(\ell)$ is even.
We say that a "SCC" of a "parity automaton" is ""positive@@SCC"" if the minimal "priority" appearing on it is even, and ""negative@@SCC"" otherwise.

A "parity automaton" $\A$ is in ""normal form"" if it holds that for every pair of states $q, p$ in a same "positive SCC" (resp. "negative SCC"), whenever there is a path $q\lrp{w:x} p$ producing $x$ as minimal "priority", then, for every $0\leq y\leq x$ (resp. $1\leq y\leq x$), there is a returning path $p\lrp{w':y}q$  producing $y$ as minimal priority.[This notion can be refined in the natural way to fit automata not using priority $0$ at all (for instance "coBüchi automata"). We refer to <cit.> for formal details.]

That is, if $\A$ is in "normal form", the restriction of $\A$ to priorities $\geq x$ consists in a disjoint union of "strongly connected components". Moreover, if priority $y>x$ appears in one of these "SCCs", then all priorities between $x$ and $y$ appear on it.

Every "parity automaton" admits an "equivalent labelling" so that the obtained automaton is in "normal form", and this labelling is unique (modulo choices of priorities changing of "SCC").
This labelling is the one assigning to each transition the smallest possible priority <cit.>.
Moreover, it can be computed in polynomial time.

Given a "parity automaton" $\A$, we can compute in polynomial time an "equivalent labelling" defining an automaton in "normal form".

Automata with $\ee$-transitions.

An ""automaton with $\ee$-transitions"" is defined just as an "automaton" over the alphabet $\SS \cup \{\ee\}$, where $\ee \notin \SS$ is a distinguished letter.
The language of an automaton $\A$ with $\ee$-transitions is the set of words $w \in \SS^\omega$ such that there exists $w' \in (\SS \cup \{\ee\})^\omega$ which is "accepted by" $\A$ and such that $w$ is obtained from $w'$ by removing all occurrences of the letter $\ee$.

Alphabets of words

As an important element of our main proof, we will need to consider automata whose transitions are labelled from an alphabet $A \subseteq \SS^+$ of finite words.
Such an automaton defines a language $L \subseteq A^\omega$ which we would like to see as a language $L \subseteq \SS^\omega$; however, this may pose a problem if a word $w \in \SS^\omega$ admits several decompositions in $A^\omega$.

We say that a set $A\subseteq \SS^+$ is a ""proper alphabet"" if any word $w\in \SS^\omega$ admits a unique decomposition as elements of $A$: for any infinite sequences $a_1,a_2,\dots$ and $a'_1,a'_2,\dots$ of elements of $A$, if $a_1 a_2 \dots = a'_1 a'_2 \dots$ then $a_i=a'_i$ for all $i$.

We will only consider alphabets of words $A \subseteq \SS^+$ which are ""prefix codes"": if $a \in A$, then no proper prefix of $a$ belongs to $A$.
It is an easy check that these are "proper alphabets", and therefore one may indeed see a language $L \subseteq A^\omega$ as $L \subseteq \SS^\omega$.

§.§.§ Congruences and monotone preorders over automata

Equivalence relations and preorders.

We will use $\sim_X$ to denote different equivalence relations, and $[q]_X$ to denote the ""equivalence class"" of an element $q$ (which is usually a state in an automaton).

A ""preorder"" $\leq_X$ is a binary relation that is reflexive and transitive.
We say that it is ""total@@preorder"" if every pair of elements are comparable.
The ""equivalence relation induced from a preorder"" $\leq_X$ is the relation defined as:

\[ q \sim_X q'  \; \iff\; q \leq_X q' \tand q' \leq_X q.\]

Given a "preorder" $\leq_X$, we always write $\sim_X$ for the induced equivalence relation, and simply write $\leq$ for the ""induced order@@eqRel"" over equivalence classes, for instance we may write $[q]_X \leq [q']_X$.

Let $\R_1$ and $\R_2$ be two binary relations over a set $A$ (usually "preorders" or equivalence relations). We say that $\R_1$ is a ""refinement"" of $\R_2$ if for all $q,p\in A$, $q\mathrel{\R_1} p$ implies $q\mathrel{\R_2} p$.
We note that if $\leq_1$ is a "preorder" "refining" $\leq_2$, then the "induced equivalence relation" $\sim_1$ "refines" $\sim_2$.

Congruences, uniformity and monotonicity.

Let $\A$ be a (possibly "non-deterministic") "automaton" over $\SS$ with states $Q$ and transitions $\DD$.
Let $\sim$ be an equivalence relation over $Q$ and let $\DD'\subseteq \DD$ be a subset of transitions (usually $\DD'$ will be the set of transitions using a given "priority").
We say that transitions of $\DD'$ ""are uniform over $\sim$-classes"" if for all $q\sim q'$ and $a \in \SS$, if $q \re {a}p\in \DD'$ then all "$a$-transitions@@out" $q' \re{a}$ are in $\DD'$.
We say that $\sim$ is a ""congruence for"" $\DD'$ (or that transitions in $\DD'$ preserve $\sim$) if for all $q\sim q'$ and $a \in \SS$, if $q \re {a}p\in \DD'$ then there exists $q' \re{a}p' \in \DD'$, and for all such transitions $p\sim p'$. If $\DD'=\DD$, we just say that $\sim$ is a ""congruence"".
We say that $\sim$ is a ""strong congruence for"" $\DD'$ if, moreover, we have the equality $p= p'$ for transitions as above.

If $\A$ is "deterministic" and $\sim$ is a "congruence for" $\DD'$, then these transitions "are uniform over $\sim$-classes".

Representation of the notions of "uniformity", "congruence" and "strong congruence". We picture an automaton with three equivalence classes, each of them represented by a yellow bubble. Green-dotted transitions are "uniform" over the classes, but the relation is not a "congruence" for them. The relation is a "congruence for" blue-dashed transitions, and a "strong congruence for" red-solid transitions.

Let $\leq$ be a "preorder" over $Q$.
We say that transitions in $\DD'$ ""are monotone for"" $\leq$ if for all $q \leq q'$ and $a \in \SS$, if $q \re a p\in\DD'$ then there exists $q' \re a p'\in \DD'$ and for all such transitions, $p\leq p'$.
Transitions in $\DD'$ are said ""strictly monotone for"" $\leq$ if, moreover, whenever $q < q'$,  $q \re a p\in\DD'$ and $q'\re a p'\in \DD'$, we have $p<p'$.
If $\DD'=\DD$, we simply say that $(\A,\leq)$ is ""(strictly) monotone@@aut"".

All these properties can equivalently be stated with words $w \in \SS^*$ instead of letters $a \in \SS$.

If transitions in $\DD'$ are "monotone for a preorder" $\leq$, then its "induced equivalence relation" is a "congruence for $\DD'$".

Quotient by a congruence.
Let $\A$ be an automaton and let $\sim$ be a "congruence" over its set of states $Q$.
We define the ""quotient of $\A$ by $\sim$"" to be the "automaton structure" $\intro*\quotAut{\A}{}$ given by:

* The set of states are the $\sim$-classes.

* There is a transition $[q]\re{a}[p]$ if there are $q'\in [q]$, $p'\in [p]$ such that $q'\re{a}p'$ in $\A$.

* The "initial state" is $[q_\init]$.

We note that if $\sim$ comes from a "monotone@@cong" preorder, the obtained "automaton structure" $\quotAut{\A}{}$ with the induced order over the classes is "monotone@@aut".

The quotient $\quotAut{\A}{}$ is a "deterministic" "automaton structure".

A "run over a word" $w$ in $\A$, $\rr = q_0\re{w_0} q_1\re{w_1}\dots$ naturally induces a "run over" $w$ in $\quotAut{\A}{}$, $[q_0]\re{w_0} [q_1]\re{w_1}\dots$, that we call the ""projection of $\rr$@@quot"" in the quotient automaton.

Let $\sim$ be a "congruence" in $\A$.
Any run in $\quotAut{\A}{}$ is the "projection@@quot" of some "run" in $\A$.

Let $[q_0]\re{w_0} [q_1]\re{w_1}\dots$ be a "run" in $\quotAut{\A}{}$. We build the desired run in $\A$ recursively. For the base case, it suffices to take $p_0\in [q_0]$ to be the "initial state" of $\A$ (which belongs to $[q_0]$ by definition of the "initial state" of $\quotAut{\A}{}$).
Suppose that $p_0\re{w_0} p_1\re{w_1}\dots p_k$ has already been built, with $p_i\in [q_i]$. By definition of the "quotient automaton", there are $q_k'\in [q_k]$ and $q_{k+1}'\in [q_{k+1}]$ with $q_k'\re{w_k} q_{k+1}'$. By the definition of a "congruence", there is a transition $p_k\re{w_k} p_{k+1}$ and $p_{k+1}\in [q_{k+1}]$.

Notations on paths in automata with a congruence.

Let $\sim$ be a "congruence" over the states of a "parity automaton" $\A$. We write $[q]\re{a:x} [p]$ if for all $q'\sim q$, every "$a$-transition" from $q'$ is of the form $q'\re{a:x}p'$ with $p'\sim p$.
We extend this notations to paths $[q]\lrp{w:x} [p]$ and for outputs ${\leq}x$, ${<}x$, ${\geq}x$ and ${>}x$ in the natural way.

If $\sim$ is a "congruence for" transitions producing priority $x$, $q\lrp{w:x} p$ implies $[q]\lrp{w:x} [p]$.

Let $\A$ be a "history-deterministic" automaton with initial state $q_\init$ and let $\resolv$ be a "resolver" for it.
We recall that we write $q_\init\lrpResolver{\resolv}{u:x}q$ to denote the "run induced by@@res" $\resolv$ over $u$. We use the same conventions as above regarding outputs with the symbols ${\leq}x$, ${<}x$, ${\geq}x$ and ${>}x$.

For $u_0\in \SS^*$, we write $q\intro*\lrpResolverWord{\resolv}{u_0}{w:x}p$ if:

* $q_\init\lrpResolver{\resolv}{u_0}q$, and

* the "induced run of $\resolv$" over $u_0w$ ends in $p$ and produces $x$ as minimal "priority" in the part of the run corresponding to $w$.

We write $q \intro*\lrpExistsResolver{\resolv}{w:x}p$ if $q\lrpResolverWord{\resolv}{u_0}{w:x}p$ for some $u_0\in \SS^*$.
We write $q \intro*\lrpAllResolver{\resolv}{w:x}p$ if, for any word $u_0\in \SS^*$ such that $q_\init\lrpResolver{\resolv}{u_0}q$, we have $q\lrpResolverWord{\resolv}{u_0}{w:x}p$.

If $\sim$ is a "congruence" in $\A$, we write $[q] \lrpAllResolver{\resolv}{w:x}[p]$ if, for any word $u_0\in \SS^*$ such that $q_\init\lrpResolver{\resolv}{u_0}q'\in[q]$, we have $q'\lrpResolverWord{\resolv}{u_0}{w:x}p'\in [p]$.
We avoid using this notation for paths quantified existentially, as we consider that the corresponding semantics are not as intuitive.

§.§.§ Residuals and semantic determinism

Residuals of a language.

Let $L\subseteq \SS^\oo$ be a language of infinite words and let $u\in \SS^*$.
We define the ""residual of $L$ with respect to"" $u$ by

\[
\intro*\lquot{u}{L} = \{ w\in \SS^\oo \mid uw\in L\}.
\]

We denote $\intro*\Res{L}$ the set of "residuals" of $L$, which we will always order by inclusion.
This induces a partial "preorder" $\leq_L$ over $\SS^*$ defined by

\[
u \leq_L u' \iff \lquot{u}{L} \subseteq \lquot{u'}{L}.
\]

The "induced equivalence relation" $\intro*\eqRes{L}$ is given by the equality of "residuals".
This yields a notion of ordered ""residual classes"" $\intro*\resClass{u}_L=\{u'\in \SS^*\mid \lquot{u}{L} = \lquot{u'}{L} \}$, which we sometimes write as $\resClass{u}$ when $L$ is clear from context.

If $L$ is "$\oo$-regular", $\Res{L}$ is finite, and for all $u\in \SS^*$, $\lquot{u}{L}$ is also "$\oo$-regular". Contrary to the case of finite words, there are non "$\oo$-regular" languages with a finite set of "residuals".

We now state a key monotonicity property for residuals; its proof is a direct check.

For any language $L \subseteq \SS^\oo$ and for any finite words $u,u',w \in \SS^*$, if $\resClass{u} \leq \resClass{u'}$ then $\resClass{uw} \leq \resClass{u'w}$. In particular, if $\resClass{u} = \resClass{u'}$ then $\resClass{uw} = \resClass{u'w}$.

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$.
Equivalently, $L$ is "prefix-independent" if and only if $\Res{L}$ is a singleton.

Semantic determinism.

We say that an "automaton" $\A$ is ""semantically deterministic"" if for all state $q\in Q$, letter $a\in \SS$ and transitions $q\re{a}p_1$ and $q\re{a}p_2$, it is satisfied that $\Lang{\initialAut{\A}{p_1}} = \Lang{\initialAut{\A}{p_2}}$, where   $\initialAut{\A}{p}$ is the automaton obtained by setting $p$ as "initial state".

Any "history-deterministic" "automaton" contains an "equivalent@@aut" "semantically deterministic" and "history-deterministic" "subautomaton". Moreover, for "parity automata", this "subautomaton" can be computed in polynomial time.

We assume in the whole paper that "history-deterministic" automata are "semantically deterministic".

We refer to <cit.> for more details on "semantically deterministic" automata.

Residual associated to a state.

We write $q\intro*\eqResState{\A} q'$ if $\Lang{\initialAut{\A}{q}}= \Lang{\initialAut{\A}{q'}}$ (and drop the subscript if $\A$ is clear from the context). The ""class of $q$"", written $\intro*\resClassState{q}$, is the set of states equivalent to $q$.

If $\A$ is "semantically deterministic" and $q$ is reachable, $\Lang{\initialAut{\A}{q}}$ coincides with
$\lquot{u}{L}$ for any word $u\in \SS^*$ leading to $q$ from the "initial state" of $\A$. In that case, we say that the "class of states" $\resClassState{q}$ is ""associated to@@residual"" the "residual class" $[u]$.

The inclusion of these languages induces a "preorder" $\intro*\leqResState_\A$ on the states of $\A$ (with its corresponding equivalence relation). By Lemma <ref>, if $\A$ is "semantically deterministic", relation $\eqResState{\A}$ is a "congruence" and "preorder" $\leqRes_{\A}$ makes $\A$ a "monotone automaton".

An "automaton" $\A$ without unreachable states is "semantically deterministic" if and only if $\eqResState{\A}$ is a "congruence".

Automaton of residuals.
Let $L\subseteq \SS^\oo$ be a language of infinite words.
The ""automaton of residuals"" of $L$ is a "deterministic" "automaton structure" $\intro*\autRes{L}$ over $\SS$  defined as follows:

* The set of states is the set of "residual classes" of $\Res{L}$:  $Q = \{\resClass{u} \mid u\in \SS^*\}$.

* The "initial state" is $\resClass{\ee}$.

* For each state $\resClass{u}$ and letter $a\in \SS$, it contains the transition $\resClass{u}\re{a}\resClass{ua}$.

We will be interested in the question of whether we can define a "parity@@aut" or "Büchi automaton" "on top of" the $\autRes{L}$ so that the obtained "automaton" "recognises" $L$.

The states of $\autRes{L}$ are ordered by the inclusion of "residuals". By Lemma <ref>,  transitions of $\autRes{L}$ are "monotone@@cong" for this order.

We remark that, for any "semantically deterministic" automaton $\A$ "recognising" $L$, the "automaton of residuals" $\autRes{L}$ coincides with the "quotient of $\A$ by" the "congruence" $\eqResState{\A}$.

§ HALF-POSITIONALITY OF $\OO$-REGULAR OBJECTIVES: STATEMENT OF THE RESULTS

In this section, we state the central result of the paper and its consequences: a full characterisation of "deterministic" "parity automata" "recognising" "half-positional" "$\oo$-regular languages" (Theorem <ref>).
The statement of the theorem uses terminology that will be formally introduced in Section <ref>, here we just provide some intuitive explanations.

§.§ Characterisation of half-positionality for $\oo$-regular objectives

We state our main characterisation theorem.

Let $W\subseteq \SS^\oo$ be an "$\oo$-regular" "objective". The following are equivalent:

*  $W$ is "half-positional" over finite "$\ee$-free" "Eve-games".

*  There is a "deterministic" "fully progress consistent" "signature automaton" "recognising" $W$.

*  There is an "$\ee$-completable" "deterministic" "parity automaton" "recognising" $W$.

*  For all cardinals $\kappa$, there is a "well-ordered@@graph" "monotone@@univ" "$(\kappa,W)$-universal" graph.

*  $W$ is "half-positional" over all "games" (potentially infinite and containing "$\ee$-edges").

The notion which is most central to the proof is that of "signature automata".
These are "parity automata" with a very restricted syntactic structure: for all "priorities" $x$ there is a "total preorder" $\leqSig{x}$ over the states, such that these refine one another and satisfy some local "monotonicity@@cong" properties (see Section <ref> for the precise definition, which is quite involved).
Our main technical contribution is to show that any "half-positional" "$\oo$-regular" "objective" $W$ can be "recognised" by a "signature automaton" (implication from <ref> to <ref>).
This is achieved by applying a number of transformations to a given "parity automaton", until obtaining an automaton with all the desired structural properties.

The final automaton satisfies a further more global property – necessary for "half-positionality" – that we call "full progress consistency": words making a strict progress in the automaton with respect to some of the preorders must be "accepted@@aut" if repeated infinitely often.

Next, we prove that "deterministic" "fully progress consistent" "signature" automata are in fact "$\ee$-completable": one may add $\ee$-transitions along a tree structure without augmenting their language, as illustrated in Figure <ref> (see Section <ref> for a formal definition).
This corresponds to the implication from <ref> to <ref>.

On the left, a deterministic automaton recognising the "half-positional" language $\infOften(a) \vee (\noOcc(a) \wedge \finOften(bb))$. On the right, a representation of an "$\ee$-completion" of the automaton. All arrows on the right correspond to "$\ee$-transitions" that may be added without augmenting the language, such as the three dashed ones.

In fact, regarding "$\ee$-completable" automata we obtain a stronger result:
any "parity automaton" "recognising" a "half-positional" language is "$\ee$-completable" (including "non-deterministic" ones, see Corollary <ref>). However, the proof of this result relies on Theorem <ref> and its consequences (mainly Theorem <ref> about closure under union). We precise the exact set of equivalences concerning "$\ee$-complete" automata in the next proposition (we refer to Section <ref> for a proof).
We do not know whether the existence of a "non-deterministic" "$\ee$-complete" automaton suffices to prove "half-positionality".

Let $W$ be an "$\oo$-regular" "objective".
The following are equivalent:

* There is a "deterministic" "$\ee$-completable" automaton "recognising" $W$.

* There is a "history-deterministic" "$\ee$-complete" automaton "recognising" $W$.

* $W$ is "half-positional" over all "games".

* Any ("non-deterministic") automaton "recognising" $\A$ is "$\ee$-completable".

To conclude the proof of Theorem <ref>, we show how to obtain "well-ordered" "monotone@@univ" "universal" graphs from "$\ee$-complete" automata (implication from <ref> to <ref>), which is fairly straightforward, and conclude thanks to Proposition <ref>.

§.§ Main consequences on half-positionality

We now discuss consequences of Theorem <ref>.

*Decidability of half-positionality in polynomial time

Given a "deterministic" "parity automaton" $\A$, we can decide in polynomial time whether $\Lang{\A}$ is "half-positional".

We will give two proofs for Theorem <ref>, both of which are detailed in Section <ref>.
The first proof applies the procedure turning a "deterministic" parity automaton into a "signature" "automaton"; if some step of the procedure fails, then the "objective" is not "half-positional".
The second proof is more direct and builds up on another consequence of Theorem <ref>, namely the closure under union (see discussion below).

*Finite-to-infinite and 1-to-2 player lifts

The following result simply restates the implication <ref> $\implies$ <ref> from Theorem <ref>.

If an "$\oo$-regular" objective is "half-positional over" finite, "$\ee$-free" "Eve-games", then it is "half-positional" over all games (potentially infinite and containing $\ee$-edges).

*Closure under union of prefix-independent half-positional languages

We now show that "Kopczyński's conjecture" holds for "$\oo$-regular languages": "prefix-independent" "half-positional" languages are closed under union. In fact, we show a stronger result: it suffices to suppose that only one of the objectives is "prefix-independent".

Let $W_1,W_2\subseteq \SS^\oo$ be two "half-positional" "$\oo$-regular" objectives, and suppose that $W_1$ is "prefix-independent". Then, $W_1\cup W_2$ is "half-positional".

In order to obtain this theorem, we use the 1-to-2-players lift stated in Theorem <ref>. The result from Theorem <ref> can be easily obtained for "Eve-games", so it suffices then to apply the lift to get the result for all types of games.

Let $W_1,W_2\subseteq \SS^\oo$ be two objectives that are "half-positional over@@eve" "Eve-games", and suppose that $W_1$ is "prefix-independent". Then, $W_1\cup W_2$ is "half-positional over@@eve" "Eve-games".

Let $\G$ be an "Eve-game" using $W_1\cup W_2$ as "winning condition".
We show that "Eve" has a "positional strategy" that "wins from" any vertex of her "winning region".
We let $\G_1$ be the "game" with the same "game graph" than $\G$ and $W_1$ as "winning condition". Consider "Eve's" "winning region" in this game, $\winRegion{\Eve}{\G_1}$. By "half-positionality" of $W_1$, she has a "positional strategy" $\strat_1$ ensuring to produce paths labelled with $W_1$ from states in $\winRegion{\Eve}{\G_1}$.
Moreover, by "prefix-independence" of $W_1$, there is no path leading to $\winRegion{\Eve}{\G_1}$ from a vertex that is not in this "winning region".

We let $\G_2$ be the "game" with $\G\setminus \winRegion{\Eve}{\G_1}$ as "game graph", and using $W_2$ as "winning condition". By "half-positionality" of $W_2$, "Eve" has a "positional strategy" $\strat_2$ for this game that is winning from $\winRegion{\Eve}{\G_2}$.

We consider the "positional strategy" $\strat$ in $\G$ that coincides with $\strat_1$ over $\winRegion{\Eve}{\G_1}$ and coincides with $\strat_2$ over $\G_2$. It is clear that this "strategy" is "winning@@strat" from vertices in $\winRegion{\Eve}{\G_1}\cup \winRegion{\Eve}{\G_2}$. We show that these are all vertices from which "Eve" can win $\G$, so $\strat$ is an "optimal strategy".

$\winRegion{\Eve}{\G} = \winRegion{\Eve}{\G_1} \cup \winRegion{\Eve}{\G_2}$.

Let $v$ be a vertex in $\G$ such that "Eve" "wins from" it. A "strategy" in an "Eve-game" is just an infinite path in the "game graph". Let therefore $\rr_v$ be an infinite path from $v$ labelled with a word $w\in W_1\cup W_2$.
Suppose that $v\notin \winRegion{\Eve}{\G_1}$. In particular $w\notin W_1$, so $w\in W_2$. As there is no path leading to $\winRegion{\Eve}{\G_1}$ from a vertex that is not in this region, the path $\rr_v$ is contained in $\G \setminus\winRegion{\Eve}{\G_1}$, which is the "game graph" of  $\G_2$. Therefore, $v\in \winRegion{\Eve}{\G_2}$.

"Kopczyński's conjecture" and its stronger version in which only one of the objectives is supposed to by "prefix-independent" remain open for arbitrary objectives.

*Closure of positionality under addition of neutral letters
As mentioned in the introduction,  Ohlmann recently characterised "half-positional" objectives by means of the existence of "universal graphs" <cit.>. One direction (stated in Proposition <ref>) holds for any objective: if $W$ admits "well-ordered" "monotone@@graph" "universal graphs", then it is "half-positional". To obtain the converse, the proof proposed by Ohlmann requires a further hypothesis: $W$ has to contain a "neutral letter", that is a letter that can be removed from any word without modifying the membership in $W$.
In his work, he left open the problem of whether adding a "neutral letter" preserves "positionality". This is a central question in the theory of "positionality", as it would imply that "universal graphs" completely characterise "half-positionality" without any further hypothesis on the objectives.
This question is almost[The only difference is that in "$\ee$-free" games we assume that there are no infinite paths composed exclusively of $\ee$-edges, whereas these may appear in "$\addNeutral{W}$-games".] equivalent to the one raised by Kopczyński in his PhD thesis <cit.>: if $W$ is "half-positional" over "$\ee$-free" games, is it "half-positional" over all games?

Let $W\subseteq \SS^\oo$ be an objective. A letter $c\in \SS$ is ""neutral for $W$"" if, for all $w_1,w_2,\dots \in \SS^+$ and $n_1,n_2,\dots \in \NN$:

* $c^{n_1}w_1c^{n_2}w_2\dots \in W \: \iff \: w_1w_2\dots \in W$, and

* $w_1c^\oo \in W \iff \lquotW{w_1}\neq \emptyset$.

Given an objective $W$, we let $\intro*\addNeutral{W}$ denote the unique objective obtained by adding a fresh "neutral letter" $\ee$ to $W$.

Let $W\subseteq \SS^\oo$. Objective $\addNeutral{W}$ is "half-positional" if and only if for all cardinals $\kappa$ there is a "well-ordered" "monotone@@univ" "$(\kappa,W)$-universal" graph.

For every "half-positional" objective $W$, objective $\addNeutral{W}$ is "half-positional".

Our characterisation (Item <ref> in Theorem <ref>), together with Proposition <ref>, answers this question in the case of "$\oo$-regular" objectives.

Let $W\subseteq \SS^\oo$ be an "$\oo$-regular objective". If $W$ is "half-positional", then $\addNeutral{W}$ is "half-positional".
Also, $W$ is "half-positional" over "$\ee$-free" games if and only if $W$ is "half-positional" over all games.

§ WARM-UP: ILLUSTRATING IDEAS ON RESTRICTED CLASSES OF LANGUAGES

The goal of this section is to give a gentle introduction to the techniques and ideas which are used in the proof of our main result (implication from <ref> to <ref> in Theorem <ref>).
We single out four crucial properties that a "parity automaton" "recognising" a "half-positional" objective should satisfy.

* "Half-positional" objectives have totally ordered "residuals", which define a "congruence" over states of automata "recognising" them.

* This order should satisfy a semantical property called "progress consistency".

* Transitions with "priority" $0$ "preserve this congruence" (if $q\eqResState p$ and $q\re{a:0}$, then $p\re{a:0}$).

* In each "congruence class", states which are interreachable using paths avoiding priorities $\leq 1$ have comparable "$({\leq}1)$-safe languages".

We propose to study four restricted classes of "$\omega$-regular objectives" that allow us to isolate these different points, namely, "closed", "open", "Büchi recognisable" and "coBüchi recognisable" "objectives".
Considering objectives in these four classes allows us to illustrate the necessity of the four properties above, and the techniques we use to derive them.
In each case, we state a characterisation of "half-positionality" and give a full proof of necessity, which is the more difficult direction.
These characterisation and proof techniques are generalised to all "$\omega$-regular languages" in our main inductive proof of necessity (Section <ref>).

We moreover incorporate in this section many examples illustrating our results and the ideas in our proofs.

§.§ Closed objectives and total order on the residuals

We now discuss the first property announced above: "residuals" of "half-positional" objectives are totally ordered by inclusion. The necessity of this condition holds even for non "$\oo$-regular" objectives.

*Residuals of half-positional objectives are totally ordered

If an objective $W\subseteq \SS^\oo$ is "half-positional", then $\Res{W}$ is totally ordered by inclusion.

We show the contrapositive.
Suppose that $W$ has two incomparable "residuals", $\lquotW{u_1}$ and $\lquotW{u_2}$.
Take $w_1\in \lquot{u_1}{W}\setminus\lquot{u_2}{W}$ and $w_2\in \lquot{u_2}{W}\setminus\lquot{u_1}{W}$.
Stated differently, we have

$u_1w_1\in W$,     $u_1w_2\notin W$,

$u_2w_1\notin W$,     $u_2w_2\in W$.

Consider the (infinite) "Eve-game" $\G$ represented in Figure <ref>.
"Eve" "wins" $\G$ from $v_1$ and $v_2$: if a "play" starts in $v_i$, for $i=1,2$, she just has to take the path labelled $w_i$ from $v_{\mathsf{choice}}$. However, she cannot win from both $v_1$ and $v_2$ using a "positional strategy". Indeed, such a "positional strategy" would choose one transition $v_{\mathsf{choice}} \lrp{w_i}$, and the "play" induced when starting from $v_{j}$, $j\neq i$, would be "losing@@play".

A game $\G$ in which "Eve" cannot "play optimally using positional strategies" if $\Res{W}$ is not totally ordered.

*Closed objectives

Let $\SS$ be a set of letters and $L \subseteq \SS^*$ be a language of finite words.
The ""safety objective associated to $L$"" is defined by

\[
\intro*\Safe{L}= \{ w\in \SS^\oo \mid w \text{ does not contain any prefix in } L\}.
\]

An "objective" $W$ is ""topologically closed"" if $W=\Safe{L}$ for some $L\subseteq \SS^*$. This terminology is justified since "objectives" of the form $\Safe{L}$ are exactly the closed subsets of $\SS^\oo$ for the Cantor topology (see for example <cit.>).

An objective $W=\Safe{L}$ is "$\oo$-regular" if and only if $L$ is a regular language of finite words if and only if $\Res{W}$ is finite.
We refer to this class as ""$\oo$-regular closed objectives"".

It turns out that for "$\omega$-regular closed" objectives the converse of Lemma <ref> holds.
This was first established in <cit.>.

Let $W\subseteq \SS^\oo$ be an "$\oo$-regular closed objective".
Then, $W$ is "half-positional" if and only if $\Res{W}$ is totally ordered by inclusion.

Thus, "residuals" encode the information needed to decide whether an "$\omega$-regular closed" objective is "half-positional".
We do not include a proof of sufficiency in this warm-up; a proof for all (non-necessarily "$\oo$-regular") "closed objectives" is given in Theorem <ref>.
However, a much subtler understanding is needed for non-"closed objectives", as witnessed by the example below.

[Non-positional open objective]
Consider the non-"closed objective"

\[ W = \{w\in \SS^\oo \mid w \text{ contains the factor } aa \}. \]

Its three "residuals" are totally ordered by inclusion:

\[ \lquotW{\ee} \subseteq \lquotW{a} \subseteq \lquotW{aa}. \]

However, it is not "half-positional", as witnessed by the "game" in Figure <ref>.

A game $\G$ in which "Eve" cannot produce the factor $aa$ "positionally@@strat".

§.§ Open objectives and progress consistency

We now introduce "progress consistency", a semantical property of the order of "residuals" which is necessary for "half-positionality". For "$\oo$-regular open" objectives, this property, together with the total order of "residuals" is also sufficient.

*Progress consistency

An objective $W\subseteq \SS^\oo$ is ""progress consistent"" if for all $u,w\in \SS^*$:

\[ \resClass{u}_W \lRes \resClass{uw}_W \implies uw^\oo \in W. \]

Intuitively, a "progress consistent" objective satisfies that whenever we read a word that makes some strict progress with respect to the order of the "residuals", by repeating this word we produce a sequence in $W$.

We remark that the objective $\Reach{\SS^*aa}$ from Example <ref> is not "progress consistent", as the word $ba$ makes progress from residual $\lquotW{\ee}$, but $(ba)^\oo\notin W$.

Let us establish necessity of progress consistency for "half-positional" objectives.

Any "half-positional" objective is "progress consistent".

We show the contrapositive of the statement. Let $W$ be an objective that is not "progress consistent", that is, there are $u,w\in \SS^*$ such that $\resClass{u} \lRes \resClass{uw}$ and $uw^\oo \notin W$.
Let $w'\in \lquotW{uw}  \setminus \lquotW{u}$.
Consider the game $\G$ depicted in Figure <ref>.

A game $\G$ in which "Eve" cannot "play optimally using positional strategies" if $W$ is not "progress consistent".

"Eve" "wins" game $\G$ from vertex $v_0$ by producing the "play"

\[ v_0\lrp{u\phantom{.}}v_\mathsf{choice} \lrp{w\phantom{.}}v_\mathsf{choice} \lrp{w'\phantom{.}}.\]

However, she cannot "win positionally" from $v_0$ since "positional strategies" produce either $uw^\omega$ or $uw'$, and both of these words are "losing".

The previous lemma applies, in particular, to "$\oo$-regular closed" objectives. We did not need to add "progress consistency" as an hypothesis in Proposition <ref>, as this property is granted for "closed@@obj" objective by Lemma <ref>.

We are now ready to move on to the characterisation of "$\oo$-regular open" objectives.

*Open objectives

We now study the dual of "closed objectives", namely, "open@@obj" ones.
Let $L\subseteq \SS^*$.
The ""reachability objective associated to $L$"" is defined by

\[
\intro*\Reach{L}= \{ w\in \SS^\oo \mid w \text{ contains a prefix in } L\}.
\]

An objective $W$ is ""topologically open"" if $W=\Reach{L}$ for some $L\subseteq \SS^*$. (These are the open subsets of $\SS^\oo$ for the Cantor topology.)
Similarly to the previous subsection, we define the class of ""$\oo$-regular open objectives"" as those that are both "open@@obj" and "$\oo$-regular".

An open objective $W=\Reach{L}$ is "$\oo$-regular" if and only if $L$ is a regular language of finite words if and only if $\Res{W}$ is finite.

Let us state a characterisation of "half-positionality" for "$\omega$-regular open" objectives.
Characterisations for the full classes of "open" and "closed" objectives (without "$\oo$-regularity" assumptions) will be obtained in Section <ref>.

An "$\oo$-regular open" objective $W$ is "half-positional" if and only if it is "progress consistent" and its set of "residuals" $\Res W$ is totally ordered.

Necessity follows from combining Lemmas <ref> and <ref>; we omit a proof of sufficiency in this warp-up.
In particular, we obtain the following corollary of Propositions <ref> and <ref>.

Any "half-positional" "$\oo$-regular open" objective is "bipositional".

We now give an example of an objective that satisfies the requirement from the previous proposition.

[Half-positional open objective]
Consider the "$\omega$-regular open" objective

\[
W_n = \Reach {(a\SS^*)^n}.
\]

It was introduced (for $n=2$) in <cit.> as an example of a "bipositional" "objective" which is not ""concave"" (that is, no shuffle of two words outside $W$ belongs to $W$; see <cit.> for details).
Its "residuals" are given by

\[
\lquotW{\ee} < \lquotW{a} < \lquotW{aa} < \dots < \lquotW{a^n}=\SS^\oo,
\]

which are totally ordered.
Moreover, for any "residual class" $[a^i]$ with $i<n$, we have $[a^i] <[a^iu]$ if and only if $u$ contains the letter $a$, in which case $a^iu^\omega \in W$.
Therefore, $W$ is "progress consistent", so we conclude that it is "bipositional".

Many natural examples of objectives are in fact "prefix-independent"; for those, the two conditions about the "residuals" above are trivially satisfied.
Yet, this does not suffice to guarantee their positionality.
We continue our introductory exploration with objectives recognised by "deterministic" "Büchi automata".

§.§ Büchi recognisable objectives: Uniformity of $0$-transitions

Our goal in this section is to present another property of "half-positional" "$\omega$-regular objectives" $W$, namely, that they can be  "recognised" by a "deterministic" "parity automaton" $\A$ in which "$0$-transitions" are "uniform over" each "residual class":

For any $q \eqRes{\A} q'$ and $a \in \SS$, if $q \re{a:0}$ then $q' \re{a:0}$.

In our main induction (Section <ref>), we will derive a similar property for all even "priorities".
To illustrate the technique, we now only focus on the case of "Büchi recognisable" languages, which helps alleviate some of the technicalities while preserving the important ideas behind the proof.
On the way, we characterise "half-positionality" for these objectives, reobtaining the main result of <cit.>.

The proof is split into two parts: first, we focus on the "prefix-independent" case, and then reduce to it.

*Prefix-independent Büchi recognisable objectives

It is well-known that ""Büchi languages"" are "half-positional" <cit.>, that is, those of the form

\[ \AP \intro*\BuchiC{B}{\SS} =\{ w\in \SS^\oo \mid \text{ letters of } B \text{ appear infinitely often in } w\}. \]

We prove now that these are the only "half-positional" "prefix-independent" "Büchi recognisable" objectives.
Our proof considerably simplifies that of <cit.>.

A "prefix-independent" "Büchi recognisable" $W$ is "half-positional" if and only if it is a "Büchi language".

In particular, Proposition <ref> tells us that there is a "Büchi automaton" with just one state "recognising" $W$. In this automaton,  "$0$-transitions" are trivially "uniform@@trans".

Super words and super letters.

We say that $u\in \SS^+$ is a ""super word@@buchi"" (for $W$) if, for every $w\in \SS^\oo$, if $w$ contains $u$ infinitely often as a factor, then $w\in W$.
If $u$ is a letter, we say that it is a ""super letter@@buchi"".
Let $\intro*\BLettersBuchi{W}\subseteq \SS$ be the set of "super letters@@buchi" for $W$. It is clear that $\BuchiC{\BLettersBuchi{W}}{\SS}\subseteq W$. We will show that, if $W$ is "half-positional", this is in fact an equality.

A non-empty "prefix-independent" "half-positional" objective $W$ "recognised" by a "deterministic" "Büchi automaton" admits a "super letter@@buchi".

One may easily deduce Proposition <ref> from Lemma <ref>: the restriction $W'$ of $W$ to "non-super letters@@buchi" is a "prefix-independent" "Büchi recognisable" "half-positional" objective which contains no "super letter@@buchi". Thus, Lemma <ref> tells us that $W' = \emptyset$ and therefore $W=\BuchiC{\BLettersBuchi{W}}{\SS}$.

Fix a non-empty "prefix-independent" "half-positional" objective $W$ "recognised" by a "deterministic" "Büchi automaton" $\A$, and assume without loss of generality that $\A$ is strongly connected (thus, every state can be chosen initial) and in "normal form".
Since $W$ is non-empty, note that $\A$ must contain a transition with "priority" $0$.
We will use the following observation.

[Super words in Büchi automata]
A word $w\in \SS^+$ is a "super word@@buchi" if and only if for all states $q$ of $\A$, "priority" $0$ appears on the path $q\lrp{w:0}$.
This is in particular the case if $w$ is a letter.

By "normality" of $\A$, if there is $q$ such that $q\lrp{w:1}q'$ then there is a word $w'\in \SS^*$ labelling a returning path $q'\lrp{w':1}q$. Therefore, $(ww')^\oo\notin W$, so $w$ is not a "super word@@buchi".
The converse implication is clear, since each time word $w$ is read, the automaton produces "priority" $0$.

We now prove existence of super words.

[Existence of super words]
There is a "super word@@buchi" for $\Lang{\A}$.

We note that, as $\A$ is strongly connected and contains some "priority" $0$, for each state $q$ there is a finite word that produces "priority" $0$ when read from $q$.
We let $\{q_1,q_2,\dots,q_k\}$ be an enumeration of the states of $\A$ and recursively define $k$ finite words $w_1,w_2,\dots, w_k\in \SS^*$ satisfying:

\[ q_i \lrp{w_1w_2\dots w_{i-1}} q' \lrp{w_i:0} q''. \]

In words, for $i\in{1,\dots,k}$, reading $w_1w_2\dots w_i$ from $q_i$, produces priority $0$.
This implies that $w_1w_2\dots w_i$ produces "priority" $0$ when read from any $q_j$ for $j\leq i$.
Therefore, $w=w_1w_2\dots w_k$ produces priority $0$ when read from any state of $\A$, so by Claim <ref>, $w$ is a "super word@@buchi".

We now prove that, by "half-positionality" of $W$, "super words@@buchi" can be chopped into smaller super words.
This implies Lemma <ref> by repeatedly chopping a "super word@@buchi" obtained from Claim <ref> until obtaining a "super letter@@buchi".

[Chopping super words]
Let $w=w_1w_2 \in \SS^+$ be a "super word@@buchi".
Then either $w_1$ or $w_2$ is a "super word@@buchi".

Suppose by contradiction that neither $w_1$ nor $w_2$ are "super words@@buchi". Then, by Claim <ref>, there are states $q_1$ and $q_2$ such that $q_1\lrp{w_1:1}q_1'$ and $q_2\lrp{w_2:1}q_2'$.
By "normality", we obtain returning paths $q_1'\lrp{u_1:1}q_1$ and $q_2'\lrp{u_2:1}q_2$.
Therefore, $(w_1u_1)^\oo\notin W$ and $(w_2u_2)^\oo\notin W$.
We consider the "game" $\G$ depicted in Figure <ref>.
"Eve" can  "win" this game, as alternating the two self loops she produces the word $(u_1w_1w_2u_2)^\oo$, which belongs to $\Lang{\A}$ since $w_1w_2$ is a "super word@@buchi".
However, "positional strategies" in this game produce either $(w_1u_1)^\oo$ or $(w_2u_2)^\oo$, both losing.
This contradicts the "half-positionality" of $\Lang{\A}$.

A game $\G$ in which "Eve" can win by forming the "super word@@buchi" $w_1w_2$ infinitely often, but in which she cannot "win" using a "positional strategy".

*Half-positionality for Büchi recognisable objectives

We now state a characterisation of "half-positionality" for all "Büchi recognisable" objectives, without assuming "prefix-independence".

Let $W\subseteq \SS^\oo$ be a "Büchi recognisable" "objective". Then, $W$ is "half-positional" if and only if:

* $\ResW$ is totally ordered,

* $W$ is "progress consistent", and

* $W$ can be "recognised" by a "Büchi automaton" "on top of" the "automaton of residuals".

[Half-positional Büchi recognisable objective <cit.>]
Over the alphabet $\SS = \{a,b\}$, let

\[ W = \infOften(a) \cup \Reach{aa}, \]

that is, a word $w\in \SS^\oo$ belongs to $W$ if either it contains letter $a$ infinitely often, or it contains the factor $aa$ at some point.
This objective has three different "residuals",

\[
[\ee] < [a] < [aa]=\SS^\oo.
\]

Figure <ref> depicts a deterministic "Büchi automaton" defined on top of the "residual automaton" of $W$.
It is easy to verify that this objective is "progress consistent", so by Proposition <ref>, it is a positional objective.

"Büchi automaton" "recognising" the objective $W = \infOften(a) \cup \Reach{aa}$.

As earlier, we focus on explaining the necessity of the conditions from Proposition <ref>, and we omit a proof of sufficiency in this warm-up. We already know that the two first conditions are necessary (Lemmas <ref> and <ref>).
We now present the techniques used to obtain the necessity of the third condition.

*Uniformity of $0$-transitions for half-positional objectives

Our objective is to derive the following result.

Let $W\subseteq \SS^\oo$ be a "half-positional" "Büchi recognisable" language.
There is a "deterministic" "Büchi automaton" $\A$ "recognising" $W$ such that for every pair $q\eqResState{\A} q'$ of equivalent states and for every letter $a$, transition $q\re{a}$ produces "priority" $0$ if and only if  transition $q'\re{a}$ produces "priority" $0$.

Necessity of the conditions from Proposition <ref> easily follows. In fact, what the previous lemma tells us is that we can take the "quotient automaton@@res" $\quotAut{\A}{\A}$ and assign priorities to its transitions consistently.

The techniques we now introduce for proving Lemma <ref> will be extended in our main induction (Section <ref>).
The idea is to reduce to the "prefix-independent" case, captured by Proposition <ref>. For this, we associate a "prefix-independent" language, over an ad-hoc alphabet, to each "residual" of the objective under consideration.

For the rest of this part of the section, we fix a "half-positional" objective $W$ "recognised" by a "deterministic" "Büchi automaton" $\A$.

Localising to a residual.

For each "residual class" $\resClass{u}$ of $W$, we define the ""local alphabet at $\resClass{u}$"" as:

\[
\intro*\locAlphBuchi{u} = \{w\in \SS^+ \mid \resClass{uw} = \resClass{u} \text{ and for any proper prefix } w' \text{ of } w, \resClass{uw'} \neq \resClass{u} \}.
\]

Note that, if it is non-empty, $\locAlphBuchi{u}$ is a "prefix code", and therefore it is a "proper alphabet".
Note that in general $\locAlphBuchi{u}$ may be infinite, however this is completely harmless in this context, and we will freely allow ourselves to talk about automata over infinite alphabets. Also, $\locAlphBuchi{u}$ is possibly empty; in the following definitions we assume that this is not the case.
Note that in a finite automata over an infinite alphabet, there are finitely many classes of letters such that two letters from the same class admit exactly the same transitions. Hence one may easily turn such automata into automata over finite alphabets.

Seeing words in $\locAlphBuchi{u}^\omega$ as words in $\SS^\omega$, define the ""localisation of $W$ to $\resClass{u}$"" to be the objective

\[
\intro*\locLangBuchi W u = \{ w \in \locAlphBuchi{u}^\omega \mid uw \in W\}.
\]

Observe that $\locLangBuchi W u$ is "prefix-independent". Moreover it is "half-positional": any "$\locLangBuchi{W}{u}$-game" in which "Eve" could not "play optimally using positional strategies" would provide a counterexample for the "half-positionality" of $W$.

For a state $q$ of a "Büchi automaton" $\A$ "recognising" $W$, define $\locAlphBuchi{q}$ and $\locLangBuchi{W}{q}$ in the natural way: $\locAlphBuchi{q} = \locAlphBuchi{u}$ and $\locLangBuchi{W}{q}=\locLangBuchi{W}{u}$ for $u$ a word that reaches $q$ from the "initial state".
Observe that a word $w\in \SS^*$ belongs to $\locAlphBuchi{q}^*$ if and only if it connects states in the class $\resClassState{q}$. Elements in $\locAlphBuchi{q}$ are those that do not pass twice through this class.
We remark that $\locAlphBuchi{q} \neq \emptyset$ if and only if $q$ is a "recurrent" state (it belongs to some non-trivial "SCC").

Let $q$ be a "recurrent" state. The ""local automaton of the residual $\resClassState{q}$"" is the "Büchi automaton" $\intro*\localAutResBuchi{q}$ defined as:

* The set of states is $\resClassState{q}$.

* The initial state is arbitrary.

* For $w\in \locAlphBuchi{q}$, $q\re{w:x}q'$ if $q\lrp{w:x}q'$ in $\A$.

The language of $\localAutResBuchi{q}$ is $\locLangBuchi W u$, thus $\locLangBuchi W u$ is "Büchi recognisable".
Therefore, Proposition <ref> yields that $\locLangBuchi{W}{u}$ is a "Büchi language": there exists a set $\BLettersBuchi{[u]} \subseteq \locAlphBuchi{u}$ such that $\locLangBuchi{W}{u} = \BuchiC{\BLettersBuchi{[u]}}{\locAlphBuchi{u}}$.
We let $\intro*\NLettersBuchi{[u]} = \SS_{[u]} \setminus \BLettersBuchi{[u]}$ be the set of "non-super letters", and extend these notations to states of $\A$ by putting $\BLettersBuchi{[q]} = \BLettersBuchi{[u]}$ and $\NLettersBuchi{[q]}=\NLettersBuchi{[u]}$ where $u$ is any word leading from the initial state to $q$.

Polished automata.
For a "recurrent" state $q$, we say that a "residual class" $\resClassState{q}$ is ""polished in $\A$@@buchi"" if:

* For all $q_1,q_2\in \resClassState{q}$, there is a word $u\in \NLettersBuchi{[q]}^*$ such that $q_1\lrp{u:1}q_2$.

* For every $q'\in \resClassState{q}$ and every word $u\in \NLettersBuchi{[q]}$, reading $u$ from $q'$ produces "priority" 1.

Stated differently, $\resClassState{q}$ is "polished@@classBuchi" if the restriction of $\localAutResBuchi{q}$ to transitions labelled with letters in $\NLettersBuchi{[q]}$ is strongly connected and does not contain any transition with "priority" $0$.

We say that the automaton $\A$ is ""polished@@autBuchi"" if all its "residual classes" are "polished@@classBuchi".

If $\A$ is "polished@@autBuchi" and $q$ is a "transient" state, then, it is the only state in its "residual class": $\resClassState{q} = \{q\}$.
We will apply the term ""recurrent@@class"" (resp. ""transient@@class"") to a class $\resClassState{q}$ if $q$ is "recurrent" (resp. "transient"). This is well defined by the previous comment.

Any "half-positional" "Büchi recognisable" language $W$ can be "recognised" by a "polished@@autBuchi" "deterministic" "Büchi automaton".

Let $\A$ be a "deterministic" "Büchi automaton" "recognising" $W$.
We will first "polish@@classBuchi" the "residual class" $\resClass{q}$ of a fixed state $q$.
Consider the restriction $\localAutResBuchi{q}'$ of $\localAutResBuchi{q}$ to transitions labelled with $\NLettersBuchi{[q]}$, and take $S_{[q]}$ to be a final SCC of $\localAutResBuchi{q}'$; without loss of generality we assume that $q \in S_{[q]}$.

Now consider the automaton $\A'$ obtained from $\A$ by removing states in $[q] \setminus S_{[q]}$, and ""redirecting@@buchi"" transitions that go to $[q] \setminus S_{[q]}$ in $\A$ to transitions towards $q$ producing "priority" $0$.
Note that this transformation ""preserves the residuals@@transform"": if $p_1\re{a}p_2$ in $\A$ and  $p_1\re{a}p_2'$ in $\A'$, then $p_2\eqRes{\A}p_2'$. Also, either $\sizeAut{\A'}<\sizeAut{\A}$, or $\A$ is left unchanged.
We now prove that it preserves the language.

Automaton $\A'$ "recognises" the objective $W$.

Let $w\in \SS^\oo$.
Suppose first that the "run over $w$" in $\A'$ eventually does not take "redirected@@buchi" transitions. Then, this run contains a suffix that is also a "run" in $\A$. As the transformation "preserves the residuals@@transform", $w$ is "accepted by@@aut" $\A'$ if and only if it is "accepted by@@aut" $\A'$.

Suppose now that the "run over $w$" in $\A'$ takes infinitely many "redirected transitions@@buchi".
Such a run in $\A'$ is of the form

\[
q_{\mathsf{init}} \lrp{w_0} q \lrp{w_1} p_1 \re{a_1:0} q \lrp{w_2} p_2 \re{a_2:0} q  \lrp{w_3} p_3 \re{a_3:0}\dots,
\]

where for all $i$ the transition $p_i \re{a_i:0} q$ is a "redirected@@buchi" one, meaning that in $\A$, reading $a_i$ from $p_i$ leads to $[q] \setminus S_{[q]}$.
Note that $w$ is "accepted by@@aut" $\A'$, so we should prove that $w \in \L(\A)=W$.
Observe that, for $i\geq 1$, $w_ia_i \in \locAlphBuchi{q}^*$ and reading $w_ia_i$ in $\A$ takes $q$ to $[q] \setminus S_{[q]}$, and thus by definition of $S_{[q]}$, it holds that $w_ia_i \notin \NLettersBuchi{[q]}^*$, so $w_i a_i \in \NLettersBuchi{[q]}^*\BLettersBuchi{[q]}^+\NLettersBuchi{[q]}^*$.
We conclude that $w_1 a_1 w_2 a_2 \dots \in \BuchiC{\BLettersBuchi{[q]}}{\locAlphBuchi{q}} = q^{-1}W$ hence $w \in W$.

It follows that the residual class of $q$ in $\A'$ is $[q]_{\A'} = [q]_{\A} \cap Q'=S_{[q]}$.
We now prove that it is "polished@@classBuchi".

The residual class $[q]$ is "polished@@classBuchi" in $\A'$.

Let $q_1,q_2 \in S_{[q]}$.
By definition of $S_{[q]}$ there is $w \in \NLettersBuchi{[q]}$ such that $q_1 \lrp {w} q_2$ in $\A$. As this path avoids $[q] \setminus S_{[q]}$ in $\A$, it also belongs to $\A'$. We show that it produces exclusively priorities $1$.

By definition of $S_{[q]}$, there is a path $q_2 \lrp {w'} q_1$ with $w' \in \NLettersBuchi{[q]}$.
Therefore $(ww')^\omega$ does not belongs to $\locLangBuchi{W}{q}$, so the path $q_1 \lrp {w} q_2$ cannot produce "priority" $0$, which proves the first point in the definition of a "polished class@@buchi".

Now take $q' \in S_{[q]}$ and $u \in \NLettersBuchi{[q]}^*$.
Then by definition of $S_{[q]}$, reading $u$ from $q'$ in $\A$ leads back to $S_{[q]}$. By the previous argument, the minimal "priority" in this path is $1$.
Again, this path avoids $[q] \setminus S_{[q]}$ in $\A$, so it also belongs to $\A'$.

Thus we have obtained an automaton $\A'$ for $W$ in which the class $\resClass{q}$ is "polished@@classBuchi".
Since there are finitely many "residual classes", and the obtained automaton $\A'$ is strictly smaller than $\A$, we can repeat the process ("normalising" the automata after each iteration) until obtaining an automaton in which all the classes are "polished@@classBuchi". (We remark that we do not claim that classes $\resClass{p}\neq \resClass{q}$ that were "polished@@classBuchi" in $\A$ will remain "polished@@classBuchi" in $\A'$. Nevertheless, the process reaches a fixpoint in which all classes are "polished@@classBuchi".)

We will later on use the following property, which is our main reason for introducing "polished@@autBuchi" automata.

Let $q\eqResState{\A}q'$ be two different "recurrent" equivalent states of a "polished automaton@@buchi" $\A$. Then there is a word $u\in \locAlphBuchi{q}^+$ such that $q\lrp{u}q'$ and $u^\oo \notin \Lang{\initialAut{\A}{q}}$.

As the "automaton" $\A$ is "polished@@autBuchi", there is a word $u\in \NLettersBuchi{[q]}^+$ such that $q\lrp{u}q'$. This word satisfies the desired requirement.

Uniform behaviour of $0$-transitions.

We are now ready to prove Lemma <ref>.
Let $\A$ be a "polished@@autBuchi" and "normalised" deterministic Büchi automaton "recognising" $W$, and suppose by contradiction that there are two states $q_1\eqResState{\A}q_2$ and a letter $a\in \SS$ such that $q_1\re{a:0}p_1$ and $q_2\re{a:1}p_2$.

By "normality", there is a word $w\in \SS^*$ such that $p_2\lrp{w:1}q_2$.
In particular, since $q_2 \rp{aw} q_2$, the "class@@res" $\resClassState{q_2}$ is "recurrent@class" in $\A$.
Note that $aw\in \locAlphBuchi{q_1}^*$ and $(aw)^\oo \notin q_1^{-1}W$.
Let $q'$ be the state such that $p_1\lrp{w}q'$, note that $q'\in \resClassState{q_1}$.
Let $u_0$ be such that $q_\init \lrp {u_0} q_1$.
See Figure <ref> for an illustration of the situation.

Since $(aw)^\omega \notin q_1^{-1}W$, and $q_1 \lrp {aw:0} q'$, it cannot be that case that $q'=q_1$.
Hence, Lemma <ref> gives a word $u\in \locAlphBuchi{q}^+$ such that $q'\lrp{u\phantom{.}}q_1$ and $u^\oo\notin \Lang{\initialAut{\A}{q}}$.
Together, the facts that

* $(aw)^\oo\notin \Lang{\initialAut{\A}{q}}$,

* $u^\oo\notin \Lang{\initialAut{\A}{q}}$, and

* $(awu)^\oo\in \Lang{\initialAut{\A}{q}}$

prove that Eve wins the game on the right of Figure <ref>, but not "positionally@@win".

On the left, the situation in the automaton $\A$. We have the equivalences $q_1\eqRes{\A}q_2\eqRes{\A}q'$ and $p_1\eqRes{\A}p_2$. On the right, a game where "Eve" can "win" but not "positionally@@win".

Thus we proved that if $W$ is a "Büchi recognisable" "half-positional" objective, it can be "recognised" by a "Büchi automaton" in which  "$0$-transitions" "behave uniformly".
By extending the technique from this section, we will show in Section <ref> that this property (and its generalisation to all even priorities) also holds for automata using higher "priorities".

§.§ Objectives recognised by coBüchi automata: Total order given by safe languages

We now consider "coBüchi recognisable" objectives.
Our analysis requires using "history-deterministic" automata and techniques from <cit.>.

Most of the section is devoted to the case of "prefix-independent" objectives, for which we propose a characterisation of "half-positionality" (Proposition <ref>).
At the end of the section, we comment on how to extend this characterisation to any "coBüchi recognisable" objective (Proposition <ref>).
In the spirit of this warm-up, we omit proofs of sufficiency.

*Prefix-independent coBüchi recognisable objectives

Let us start by introducing some terminology relative to "coBüchi automata".
Our analysis requires considering "automata" that are not necessarily "deterministic", however, we have a fine control of the non-determinism that will appear.
First, all automata in this subsection will be "history-deterministic".
Moreover, we can suppose that they are "deterministic over" transitions producing "priority" $2$ by the following result of Kuperberg et Skrzypczak <cit.> (this property is sometimes called safe determinism).

Every "history-deterministic" "coBüchi automaton" contains an "equivalent@@aut" "subautomaton" that is "deterministic over" $2$-transitions, which can be computed in polynomial time.

Safe languages and safe components.
Consider a (possibly "non-deterministic") "coBüchi automaton" $\A$.
We define the ""$({<}2)$-safe language@@coB"" of a state $q$ (or just safe language)  as the set of finite or infinite words such that, when read from $q$, "priority" $1$ can be avoided, that is:

\[ \intro*\safeCoB{q} = \{w\in \SS^*\cup \SS^\oo \mid \text{ there is a run } q\lrp{w:2} \; \}. \]

Two "safe languages" coincide if and only if their restrictions to finite (resp. infinite) words coincide. Indeed, an infinite word $w\in \SS^\oo$ belongs to $\safeCoB{q}$ if and only all its finite prefixes do.

We write $ q \intro*\leqCoB q'$ if $\safeCoB{q}\subseteq \safeCoB{q'}$; this defines a partial preorder on states of $\A$.
We will sometimes use the term ""safe path@@coB"" to refer to paths in $\A$ that do not produce "priority" $1$.
The use of the notation “$(<2)$-safe” will be justified by the generalisation of this notion to any "parity automaton".
The next lemma follows directly from the definition of "safe language@@coB".

Let $\A$ be a "coBüchi automaton" which is "deterministic over" $2$-transitions, and let $q,q'$ be two states such that $q\leqCoB q'$. Let $u$ be a finite word in $\safeCoB q$ and write $q\lrp{u:2}p$. There is a unique path $q'\lrp{u:2}p'$ and $p\leqCoB p'$.

A ""$({<}2)$-safe component@@coB"" (or just safe component) of $\A$ is a set of states forming a "strongly connected component" in the "subautomaton" obtained by removing from $\A$ all transitions labelled $1$.
By Lemma <ref>, we can suppose that these subautomata are "deterministic".
Also, note that if $\A$ is in "normal form", transitions between different "safe components@@coB" produce "priority" $1$, that is, states connected by a "safe path@@coB" are in the same "safe component".

Statement of the characterisation of half-positionality.

We are now ready to state a characterisation of positionality of "prefix-independent" "coBüchi recognisable" objectives.

A "prefix-independent" "coBüchi recognisable" objective is "half-positional" if and only if it can be "recognised" by a "deterministic" "coBüchi automaton" satisfying that within each "safe component@@coB", states are totally ordered by inclusion of "safe languages@@coB".

Before going on with the proof, we discuss two examples.

In Figure <ref> we represent a "coBüchi automaton" over $\SS = \{a,b,c\}$ "recognising" the following objective:

\[ W = \text{ Words containing finitely many factors in } {c(a^*c b^*)^+c}. \]

This is an example of an objective that is not "concave", as by shuffling words $a(ccaa)^\oo\notin W$ and $(bbcc)^\oo\notin W$ we can obtain $(abcc)^\oo\in W$. However, we show that it satisfies the hypothesis of Proposition <ref>, so it is "half-positional".
This automaton has a single "safe component@@coB".
The inclusions of the "safe languages@@coB" follows from the fact that the transitions are monotone: for every letter $\aa\in \SS$, if $q_i\re{\aa:2}q_{j}$ and $i\leq i'$, then $q_{i'}\re{\aa:2}q_{j'}$ with $j\leq j'$.

"Deterministic" "coBüchi automaton" "recognising" objective $W$ from Example <ref>.

Let $\SS = \{a,b,c\}$ and

\[ W = \finOften(ac) \vee \finOften(bb). \]

We give a "coBüchi automaton" "recognising" $W$ and satisfying the hypothesis of Proposition <ref> in Figure <ref>. This automaton has two "safe components@@coB": $S_1 = \{q_1,q_2\}$ and $S_2 = \{p_1,p_2\}$. The states of each component are totally ordered by inclusion of "safe languages@@coB", as we have $q_1\lCoB q_2$ and $p_1\lCoB p_2$.
Therefore, $W$ is "half-positional".

"Deterministic" "coBüchi automaton" "recognising" objective $W$ from Example <ref>. This automaton has two "safe components@@coB": $S_1 = \{q_1,q_2\}$ and $S_2 = \{p_1,p_2\}$, and the states of each of them are totally ordered by inclusion of "safe languages@@coB".

In his PhD thesis <cit.>, Kopczyński introduced a notion of monotonic automata over finite words, and showed that if $L\subseteq \SS^*$ is recognised by such an automaton, then the ("prefix-independent") "objective" $\SS^\oo \setminus L^\oo$ is "half-positional" <cit.>.
It turns out that these correspond exactly to the "objectives" characterised in Proposition <ref>.

At the level of intuition, starting from a deterministic coBüchi automaton $\A$ "recognising" a "half-positional" objective $W$, our proof of the necessity in Proposition <ref> proceeds as follows:

* We turn $\A$ into a "history-deterministic" "safe centralised@@coB" automaton (see definition below) using the minimisation technique of Abu Radi and Kupferman <cit.>.

* Using "half-positionality", we prove that $\leqCoB$ defines a total order on each "safe component".

* Exploiting the total order, we are able to re-determinise $\A$.

Safe centralisation and safe minimality.

Let $\A$ be a (possibly "non-deterministic") "coBüchi automaton" with only one "residual class@@state".
We say that $\A$ is ""safe centralised@@coB"" if, for every pair of states $q_1,q_2$,
if $q_1\leqCoB q_2$, then $q_1$ and $q_2$ are in the same "safe component@@coB".
We say that $\A$ is ""safe minimal@@coB"" if there are no two different states with the same "safe language@@coB".

Any "prefix-independent" "coBüchi recognisable" language can be "recognised" by a  "history-deterministic" "coBüchi automaton" that is "safe centralised@@coB" and "safe minimal".

Let us present a proof of Lemma <ref>.
We say that an automaton is ""$1$-saturated"" if for all pair of states $q,q'$, the transition $q \re {a:1} q'$ appears in $\A$.
The ""$1$-saturation@@coB"" of a "coBüchi automaton" is the automaton obtained by simply adding all possible transitions of the form $q \re {a:1} q'$; note that this transformation preserves "determinism over" $2$-transitions.

Let $\A$ be a "coBüchi automaton" "recognising" a "prefix-independent" language  $W$. Then, its "$1$-saturation@@coB" $\A'$ also recognises $W$. Moreover, if $\A$ is "history-deterministic" and "deterministic over" $2$-transitions, then so is $\A'$.

We first show $\Lang{\A'}\subseteq W$.
An "accepting@@run" "run over" a word $w$ in $\A'$ eventually only reads transitions with "priority" $2$, so it eventually coincides with a run in $\A$. We conclude by "prefix-independence".
The fact that $W \subseteq \Lang{\A'}$ and "history-determinism" are clear: one can use the same "resolver" in $\A'$ as in $\A$.

Let $\A$ be a "normalised", "$1$-saturated", "history-deterministic", "deterministic over" $2$-transitions automaton "recognising" $W$, obtained by Lemma <ref>.
We say that a "safe component@@coB" $S$ is ""redundant@@coB"" if there is $q \in S$ and $q' \notin S$ such that $q \leqCoB q'$.
Let $S$ be "redundant@@coB" and consider the automaton $\A'$ obtained from $\A$ by deleting $S$.
Then $\A'$ is "history-deterministic" and "recognises" $W$.

Clearly $\L(\A') \subseteq W$.
We will describe a "sound resolver" proving that $\L(\A') = W$ and that $\A'$ is "history-deterministic".
Let $q \in S$ and $q' \notin S$ such that $q \leqCoB q'$.
For each $p \in S$, pick $u\in \SS^*$ such that $q \lrp{u:2} p$, and let $f(p)$ be such that $q' \lrp{u:2} f(p)$; this is well defined since $q \leqCoB q'$.
Note that we have $p \leqCoB f(p)$ by Lemma <ref>.
By "normality" of $\A$, there is a returning path $f(p) \lrp{w:2} q'$ and thus $f(p)$ is in the same "safe component" as $q'$, so it does not belong to $S$.
We extend $f$ to all of $Q$ by setting it to be the identity over $Q \setminus S$.

Take a "sound resolver" $(q_0,\resolv)$ in $\A$, let $w\in \SS^\oo$, and write

\[		\rho=q_0 \re{w_0} q_1 \re{w_1} \dots\]

for the run in $\A$ "induced by@@resolver" $\resolv$ over $w$.
We will build a "resolver" $(q_0',\resolv')$ in $\A'$ satisfying the property that the "run induced over $w$", $\rho'=q'_0 \re{w_0} q'_1 \re{w_1} \dots$ is such that for each $i$, $q_i \leqCoB q'_i$.
We let $q'_0=f(q_0)$, and assume $\rho'$ constructed up to $q'_i$, and $q_i\leqCoB q_i'$.
If there is a state $q'_{i+1} \notin S$ such that $q'_i \re{w_i:2} q'_{i+1}$ then we take this one,  which satisfies $q_{i+1} \leqCoB q_{i+1}'$ by Lemma <ref>. Otherwise, take the transition $q'_{i} \re{w_i:1} f(q_{i+1})$. In particular, if $w\in \safeCoB{q_i}$, the "induced run" from $q_i$ does not produce "priority" $1$.

We now show that if $\rr$ is "accepting@@run", then  $\rho'$ is an "accepting run" too: if $\rr$ is "accepting@@run", for some $i$ the suffix $w_iw_{i+1} \dots \in \safeCoB{q_i} \subseteq \safeCoB{q'_i}$. Therefore, the run $q'_i \re {w_i:2} q'_{i+1}\re {w_{i+1}:2}\dots$ in $\A'$ is "safe@@runCoB", and $\rr'$ is "accepting@@run".

Using Claim <ref>, we successively remove "redundant@@coB" "safe components@@coB" until obtaining a "safe centralised@@coB" automaton.

Finally, to obtain a "safe minimal" automaton it suffices to merge states with the same "safe language". That is, we define a "$1$-saturated" automaton that has for states the classes $[q]_2$ of states of $\A$, and transitions $[q]_2 \re{a:2} [p]_2$ whenever for some (or equivalently, for all) state $q'\in [q]_2$ there is transition $q'\re{a:2}p'$ in $\A$, with $p'\in [p]_2$. It is not difficult to check that the obtained automaton "recognises" $W$, is "history-deterministic" and remains "safe centralised@@coB".

Total order in each safe component.
The intuitive idea on why having states of a same "safe component@@coB" totally ordered by $\leqCoB$ is necessary for positionality is the same than in the case of "closed objectives" (Lemma <ref>): if $q$ and $q'$ are incomparable, there are two words $w,w'$ that produce "priority" $1$ from one state but not from the other.
In a game, if "Eve" has not kept track of where we are in the automaton, she will not know what is the best option between $w$ and $w'$.
However, an issue arises when turning this idea into an actual proof: one needs to build two full differentiating runs from $q$ and $q'$; producing "priority" $1$ just once does not suffice.
"Safe centrality@@coB" will come in handy for this purpose.

By definition, if $q\nleqCoB q'$, there is a word which produces "priority" $1$ when read from $q'$, and stays in the corresponding "safe component@@coB" when read from $q$.
The following lemma exploits "safe centrality@@coB" to extend those runs to synchronise them in the same state, while the run starting from $q$ remains safe.
For the purpose of the warm up, we only prove it assuming $\A$ is "deterministic"; extending it to the "history-deterministic" case requires some additional technicalities that will be dealt with in Section <ref>.

Let $\A$ be a "normalised", "safe centralised@@coB" and "safe minimal" "deterministic" "coBüchi automaton" with a single "residual class". Let $q$ and $q'$ be two states such that $q\nleqCoB q'$ and $p$ be any state in the "safe component@@coB" of $q$.
There is a word $w\in \SS^*$ such that $q\lrp{w:2} p$ and $q'\lrp{w:1}p$.

Since $\safeCoB{q}\nsubseteq\safeCoB{q'}$, there is a word $w_1\in \SS^*$ such that $q\lrp{w_1:2}q_1$ and $q'\lrp{w_1:1}q_1'$.
By "normality", note that $q_1$ is in the same "safe component@@coB" as $q$.
If we have again that $q_1\nleqCoB q_1'$, we can find a word $w_2$ with the same properties.
While the non-inclusion of "safe languages@@coB" is satisfied, repeating the argument yields two runs:

qw_1:2      q_1w_2:2      q_2w_3:2 …

q'w_1:1      q_1'w_2:1      q_2'w_3:1 …
We claim that the process should stop after finite time, meaning that for some $i$, we have $q_i\leqCoB q_i'$.
Otherwise, we would obtain two infinite runs over $w_1w_2w_3\dots\in \SS^\oo$, one of them "accepting@@run" and the other "rejecting@@run",
contradicting the fact that $\A$ has a single "residual class@@state".

Let $i$ be the step in which $q_i\leqCoB q_i'$. First, we note that both states are in the "safe component@@coB" of $q$: state $q_i$ is in there because there is a path $q\lrp{2}q_i$, and by "safe centrality@@coB", $q_i'$ must also be in the same "safe component@@coB".
Let $q_{\max}$ be a state in this "safe component@@coB" maximal amongst states such that $q_i'\leqCoB q_{\max}$. Let $u\in \SS^*$ be a word labelling a path $q_i\lrp{u:2} q_{\max}$ (which exists by definition of "safe components@@coB").
By Lemma <ref>, maximality of $q_{\max}$, and "safe minimality", we also have $q_i'\lrp{u:2} q_{\max}$.
Finally, if suffices to take a word $u'\in \SS^*$ labelling a path $q_{\max}\lrp{u':2} p $ and define $w = w_1w_2\dots w_iuu'$.

We may derive the sought total orders.

Let $\A$ be a "deterministic" "coBüchi automaton" "recognising" a "prefix-independent" "half-positional" objective $W$.
Suppose that $\A$ is "safe centralised@@coB" and "safe minimal".
Let $q$ and $q'$ be two different states in the same "safe component@@coB".
Then, either $q\lCoB q'$ or $q'\lCoB q$.

By "safe minimality", $q\nlCoB q'$ implies $q\nleqCoB q'$.
Suppose by contradiction that $q\nleqCoB q'$ and $q'\nleqCoB q$. Let $p$ be a state in this "safe component@@coB", and let $u,u'\in \SS^*$ be such that $p\lrp{u:2}q$ and $p\lrp{u':2}q'$.
By Lemma <ref>, there are $w,w'\in \SS^\oo$ such that:

$q\lrp{w:2}p$,     $q\lrp{w':1}p$,

$q'\lrp{w:1}p$,     $q'\lrp{w':2}p$.

The situation is depicted in Figure <ref>.
We obtain that:

* $(w'u)^\oo\notin W$,

* $(wu')^\oo\notin W$,

* $(wu'w'u)^\oo\in W$.

Situation occurring in the proof Lemma <ref>.

Thus consider the "game" in which "Eve" controls a vertex with two self loops labelled $w'u$ and $wu'$; she can "win" by alternating both loops, but fails to "win positionally".

We have stated last two lemmas of the previous paragraph for "deterministic" automata, in order to simplify the presentation.
However, "safe centralisation@@coB" only yields "history-deterministic" automaton.
We now explain how to use the total order from Lemma <ref> to determinise "HD" "coBüchi automata" "recognising" "half-positional" languages.

Let $\A$ be a "normalised", "history-deterministic" and "deterministic over" $2$-transitions "coBüchi automaton" recognising a "prefix-independent" half-positional language. Order $\leqCoB$ is total over each "safe component@@coB", by Lemma <ref>.
We show how to rearrange the $1$-transitions in order to define an "equivalent@@aut" "deterministic" "automaton" $\A'$ with the same structure of "safe components@@coB".

Let $\{S_1,S_2,\dots, S_k\}$ be the "safe components@@coB" of $\A$, enumerated in an arbitrary order.
If a word $w\in \SS^\oo$ is "accepted by@@aut" $\A$, there is a "run over" $w$ that eventually stays in one of the components $S_i$.
The main idea is that, when reading a word $w$, we can "resolve@@aut" the "non-determinism" by trying each "safe component@@coB" in a round-robin fashion.
If for a state $q$ and for a letter $a\in \SS$ there is a (unique) transition $q\re{a:2}$, we keep it as the only "$a$-transition@@in" from $q$.
If there is no transition $q\re{a:2}$, and $q$ belongs to $S_i$, we define a transition $q\re{a:1}q'$ towards some $q'$ in $S_{i+1}$.
The total order in $S_{i+1}$ identifies a state in $S_{i+1}$ which is the best to go to: we define $q\re{a:1}q_{i+1}^{\max}$, where $q_{i+1}^{\max}$ is the unique maximal state of $S_{i+1}$ for the total order $\leqCoB$.
This defines a "deterministic" automaton $\A$'.

We prove that $\Lang{\A'} = \Lang{\A}$. Clearly $\Lang{\A'} \subseteq \Lang{\A}$, as $\A'$ is a "subautomaton" of the "$1$-saturation@@coB" of $\A$.
To show the other inclusion, let $w\in \Lang{\A}$. There is a "run over@@aut" $w$ in $\A$ that eventually remains in a "safe component@@coB", without loss of generality, we assume that it is $S_1$.
Let $w'=w_1'w_2'\dots$ be a suffix of $w$ labelling a "run@@aut" in $S_1$: $q^1\re{w_1'}q^2\re{w_2'}\dots$. Consider a "run over" $w'$ in $\A'$.
If this "run" never visits $S_1$, it must be because it eventually remains in some "safe component@@coB", so $w'$ is "accepted by@@aut" $\A'$ in that case. If the run eventually arrives to $S_1$ (at the ith step), it will arrive to the maximal element $q_1^{\max}$.
At this point, the run in $\A$ is in $q^i\leqCoB q_1^{\max}$. Since  $w_i'w_{i+1}'\dots \in \safeCoB{q^i} \subseteq \safeCoB{q_1^{\max}}$, the run over this suffix is "safe@@runCoB" in $\A'$, and word $w$ is "accepted by" $\A'$.

The automaton from Figure <ref> has the shape we have described: transitions producing "priority" $1$ cycle between the two "safe components@@coB", and they go to the maximal state of the other component ($p_1\re{b:1}q_2$ and $q_1\re{c:1}p_2$).

*Generalisation to non prefix-independent coBüchi recognisable languages

To remove the "prefix-independence" assumption, we work with the "localisation to residuals" of the objectives, as defined in Section <ref>.
If $W$ is a "half-positional" objective, for each residual $\resClass{u}$ the objective $\locLangBuchi{W}{u}$ is  "half-positional".
In turns out that this property, together with the hypothesis over residuals that were already necessary for "open objectives", provides a characterisation.

Let $W\subseteq \SS^\oo$ be a "coBüchi recognisable" language. Then, $W$ is "half-positional" if and only if:

* $\ResW$ is totally ordered,

* $W$ is "progress consistent", and

* for all "residual class" $\resClass{u}$, objective $\locLangBuchi{W}{u}$ is "half-positional".

This result is not fully satisfying (and hard to prove directly), as it relies on the "half-positionality" of languages $\locLangBuchi{W}{u}$.
As these objectives are "prefix-independent", we have a characterisation for their "half-positionality" (Proposition <ref>), and we can put them together to obtain a statement using exclusively structural properties of "parity automata".
The statement we obtain uses a decomposition of parity automata in three layers:

* States are totally "preordered" by their "residual class" (layer 0).

* Within each "residual class", states are grouped into "safe components" (layer 1).

* Within each "safe component", states are totally ordered by inclusion of the "safe languages" (layer 2).

This decomposition foreshadows the definition of "structured" "signature automata" that we will use in Section <ref> to derive a characterisation of "half-positionality" for all "$\oo$-regular" languages.

Let $W\subseteq \SS^\oo$ be a "coBüchi recognisable" language. Then, $W$ is "half-positional" if and only if:

* $\ResW$ is totally ordered,

* $W$ is "progress consistent", and

* $W$ can be "recognised" by a "deterministic" "coBüchi automaton" $\A$ such that, for all "residual class" $\resClassState{q}$, the "local automaton of the residual" $\localAutResBuchi{q}$ satisfies that its "safe components@@coB" are totally ordered by inclusion of "safe languages@@coB".

We do not include a proof of this proposition; it is a special case of Theorem <ref>.

We consider the following objective over the alphabet $\SS = \{a,b,c\}$:

\[ W = \SS^*a^\oo \cup  \SS^*b^\oo \cup c\SS^*c\SS^\oo.\]

This objective was studied in <cit.> to show that there are "half-positional" objectives that are not "concave", nor "bipositional" (objectives from Examples <ref> and <ref> also have this property); their proof of half-positionality is quite involved.

A "coBüchi automaton" "recognising" objective $W$ is depicted in Figure <ref>. Its "residuals" are totally ordered, and it is easy to check that it is "progress consistent".
Moreover, all its "safe components@@coB" are trivial. Therefore,
Proposition <ref> implies that it is "half-positional".

Automaton "recognising" objective $W$ from Example <ref>.

§.§ Towards objectives of higher complexity: An example

We revisit the example from Figure <ref>, depicted here in Figure <ref>. It "recognises" the "objective" of words that either contain `$a$' infinitely often, or contain no `$a$' at all and only finitely many occurrences of the factor `$bb$':

\[ W = \infOften(a) \vee (\noOcc(a) \wedge \finOften(bb)), \; \text{ over } \SS = \{a,b,c\}.\]

This "objective" is neither "Büchi@@rec" nor  "coBüchi recognisable", so none of the characterisations of this section applies to it. However, we can combine the techniques presented above to equip $\A$ with a “nicely behaved” total order. In the next section, we will see that this can be formalised as the fact that $\A$ is a "deterministic" "fully progress consistent" "signature automaton", so by Theorem <ref>, $W$ is "half-positional".

Automaton "recognising" the objective $W= \infOften(a) \vee (\finOften(bb) \wedge \noOcc(a))$.

Objective $W$ has two "residuals": $\lquotW{\ee}$ and $\lquotW{x}$.
It is clear that $\lquotW{a} \subseteq \lquotW{\ee}$, and, since there is no transition $\resClass{a}\re{} \resClass{\ee}$, it is trivially "progress consistent".
The "states associated to@@res" $\resClass{a}$ and $\resClass{\ee}$ are, respectively, $\{q_1\}$ and $\{q_2, q_3\}$.
The "subautomaton" over $\{q_1\}$ "recognises" the "Büchi objective" $\Buchi{a}$, which is "half-positional".
Let us focus on the "subautomaton" induced by $\{q_2,q_3\}$, that coincides with $\localAutResBuchi{\ee}$.
We observe that it satisfies the hypothesis of Lemma <ref>: transitions with "priority" $0$ "act uniformly" within $\localAutResBuchi{\ee}$; indeed, these transitions are those reading letter $a$ (in red).
Consider the restriction of this subautomaton to letters $\{b,c\}$. The obtained automaton $\localAutResBuchi{\ee}'$ is a "coBüchi automaton", satisfying the hypothesis of Lemma <ref>:  the states of the "safe component@@coB" of $\localAutResBuchi{\ee}'$ are totally ordered by inclusion of "safe languages@@coB", as $q_2 \lCoB q_3$.
In this way, we obtain a decomposition such that:

* "Residuals" are totally ordered by inclusion, and are "progress consistent".

* $0$-transitions "act uniformly" within the "states of@@res" each "residual class".

* The "safe components@@coB" of the "coBüchi automata" obtained as the restriction of each class to transitions with "priority" $\geq 1$ are totally ordered by  inclusion of "safe languages@@coB".

Generalising such decomposition to any "parity automaton" will be the central point of the next section.

We also note that the "$\ee$-completion" of this automaton presented in Figure <ref> follows the decomposition presented here: $\re{\ee:0}$-transitions follow the order of the residuals, and $\re{2}$-transitions the one given by the inclusion of safe languages.
This procedure of "$\ee$-completion" will be generalised in Section <ref>.

§ OBTAINING THE STRUCTURAL CHARACTERISATION OF HALF-POSITIONALITY

We now move on to the proof of Theorem <ref>.
The first step is to identify the common structural properties of "deterministic" "parity automata" "recognising" "half-positional" objectives.
In Section <ref>, we define a class of "parity automata", which we call "signature" automata, that underscores this structure.
We also introduce "full progress consistency", a further necessary condition for automata recognising "half-positional" languages.
To obtain the implication from <ref> to <ref> in Theorem <ref> we need then to show how to obtain a "fully progress consistent" "signature automaton" for a "half-positional" "$\oo$-regular" objective.
This is the most technical part of the proof, and it is the object of Section <ref>.
We then proceed to defining "$\ee$-complete automata" and closing the cycle of implications in Section <ref>.

§.§ Signature automata and full progress consistency

Before finally moving on to the crucial definition of "signature automata", we need more precise concepts of congruences which we introduce now.

§.§.§ Priority-faithful congruences and quotient automata

Priority-faithful congruences.
We recall that a "congruence" in an automaton allows us to define a "quotient@@aut" $\quotAut{\A}{}$, which is a "deterministic" "automaton structure". However, in general, no "colouring with priorities" can be defined "on top of" $\quotAut{\A}{}$ in a sensible way, as the "congruence" does not have to be compatible with the "output priorities@@aut" of the automaton. We now strengthen the definition of "congruence" for parity automata so that it will be possible to define an approximation of a correct parity condition "on top of" the "quotient automaton".

Let $\A$ be a "parity automaton" and let $\sim$ be a "congruence" over its set of states $Q$. We say that $\sim$ is ""$[0,x]$-faithful"" if:

* for each $0\leq y\leq x$, "$y$-transitions@@out" "are uniform" over $\sim$-classes and relation $\sim$ is a "congruence for $y$-transitions", and

* relation $\sim$ is a "congruence for $({>}x)$-transitions".

Stated differently, a relation $\sim$ is a "$[0,x]$-faithful congruence" if, whenever there is a transition $q\re{a:y}p$ with "priority" $y\leq x$, then for every $q'\sim q$ a transition $q'\re{a}p'$ produces "priority" $y$ and goes to a state $p'\sim p$.
If there is a transition $q \re{a:y} p$ producing "priority" $y> x$, we only require that transitions $q'\re{a:>x}p'$ produce "priorities" $>x$ and go to $p'\sim p$ (but the exact "priority" produced may differ). (We remark that, although it is not explicitly imposed, "$({>}x)$-transitions@@out" "are uniform" over $\sim$-classes by the first property. Also, we recall that we assume that automata are "complete".)

For "deterministic" automata we can give a simpler definition. An equivalence relation $\sim$ on a "deterministic automaton" $\A$ is a "$[0,x]$-faithful congruence" if and only if, whenever $q\sim_x q'$, $q\re{a:y} p$ and $q'\re{a:y'} p'$, then $p\sim p'$ and $y=y'$ if $y\leq x$.

A "$[0,x]$-faithful congruence" is "$[0,y]$-faithful" for any $y\leq x$.

$({\leq}x)$-quotient automata.
What the definition of "$[0,x]$-faithful congruence" tells us is that transitions producing priorities $y\leq x$ are well defined in the "quotient automaton" $\quotAut{\A}{}$, in the sense that we can associate a "priority" $y$ to these transitions reliably. For transitions producing priorities $>x$, on the other hand, we only obtain the information that the "priority" produced from any state of the class will be large, but we lose some precision.

If $\sim$ is a "$[0,x]$-faithful congruence", we can define the ""$({\leq}x)$-quotient of $\A$ by $\sim$"" to be the "parity automaton" $\intro*\autLeq{\A}{}{x}$ given by:

* Its set of states are the $\sim$-classes of $\A$.

* The initial state is $[q_{\mathsf{init}}]$, where $q_{\mathsf{init}}$ is the initial state of $\A$.

* For $y\leq x$, there is a transition $[q] \re{a:y} [p]$ if  $\A$ has a transition $q'\re{a:y} p'$ with $q'\in [q]$, $p'\in [p]$.

* There is a transition $[q] \re{a:x'}[p]$ if $\A$ has a transition $q'\re{a:>x} p'$ with $q'\in [q]$, $p'\in [p]$; where $x'=x+1$ if $x$ even, and $x'=x$ if $x$ odd.

The automaton $\autLeq{\A}{}{x}$ is defined so transitions coming from those producing a "priority" $>x$ in $\A$ are assigned the least important odd "priority". This guarantees that the "projection@@quot" of "runs" that eventually only produce priorities $>x$ in $\A$ are "rejecting@@run" in $\autLeq{\A}{}{x}$. The next lemma refines this comment.

Let $\A$ be a "parity automaton" and let $\sim$ be a "$[0,x]$-faithful congruence" over it.
The "$({\leq}x)$-quotient" of $\A$ by $\sim$ "recognises" the language:

\[ \Lang{\autLeq{\A}{}{x}} = \{w\in\SS^\oo \mid w \text{ is "accepted with an even priority" } y\leq x \tin \A \}. \]

Moreover, if $\A$ is in "normal form", then so is $\autLeq{\A}{}{x}$.

A "run" $\rr$ in $\A$ produces a "priority" $y\leq x$ infinitely often if and only its "projection@@quot" in $\autLeq{\A}{}{x}$ produces "priority" $y$ infinitely often, which gives the equality of the languages.
It is a direct check that $\autLeq{\A}{}{x}$ inherits being in "normal form".

§.§.§ Signature automata

We give the definition of "signature automata", at the core of our characterisation.

We say that a sequence of "total preorders" $\leq_0, \leq_1,\leq_2,\dots, \leq_k$ over $Q$ is a ""collection of nested total preorders"" if $\leq_i$ "refines" $\leq_{i-1}$, for $i>1$.

We note that, in that case, the "induced equivalence relation@@preord" $\sim_i$ also "refines" $\sim_{i-1}$.

Let $d\in \NN$ be a "priority". A ""$d$-signature automaton"" is a "semantically deterministic" "parity automaton" $\A$
together with a "collection of nested total preorders" $\intro*\leqSig{0}, \leqSig{1}, \leqSig{2},\dots, \leqSig{d}$ over $Q$ such that:

*  Refinements of residual inclusion. Preorder $\leqSig{0}$ "refines" the preorder $\leqRes_\A$ given by the inclusion of "residuals".

*  Faithful partitions at even layers. For  $0\leq x\leq d$,  $x$ even, the equivalence relation $\eqSig{x}$ is a "$[0,x]$-faithful congruence".

*  ""$({<}x)$-safe separation"" at odd layers. For  $2\leq x\leq d$,  $x$ even, and $q\eqSig{x-2}q'$:

\[  q\lSig{x-1} q' \;\; \implies \;\; \text{ there is no path } q\lrp{w:\geq x} q'. \]

*  ""Local monotonicity"" of $({\geq}x)$-transitions. For an even "priority" $x\leq d$, transitions using priorities ${\geq}x$ are "monotone for $\leqSig{x}$" over each $\eqSig{x-1}$ class. That is, for $q\eqSig{x-1}q'$, if $q\leqSig{x}q'$:

\[  q\re{a:\geq x}p \;\; \implies \;\; q'\re{a:\geq x}p', \; p\eqSig{x-1}p' \;  \tand  p\leqSig{x}p',\; \text{ for all } a\text{-transitions from } q'. \]

We say that $\A$ is a ""signature automaton"" if it is a "$d$-signature automaton", for $d$ the maximal "priority" appearing in $\A$.

For notational convenience, we let $\sim_{-2}$ be the trivial relation over $\A$ throughout this definition. That is, $q\sim_{-2}p$ for all pairs of states in $Q$.

We note that even and odd preorders play a completely different role in the previous definition. In fact, the only purpose of odd preorders is to delimit the areas in which the "local monotonicity" property will apply. Item <ref> constrains $\eqSig{x-1}$-classes to be “sufficiently large”.

We note that, by Item <ref>, for $x$ even the equivalence relations $\eqSig{x-1}$ is a "congruence for" "${\geq}x$-transitions". However, the restrictions on these odd preorders are much weaker, as we do not impose them to be "faithful".

Consider the automaton $\A$ from Figure <ref> from the warm-up. This automaton has $3$ states, $q_1,q_2$, and $q_3$. It can be equipped with the structure of a "signature automaton" as follows:

* Preorder $\leqSig{0}$ is given by the inclusion of residuals: $q_1 \lSig{0} q_2,q_3$, and $q_2\eqSig{0}q_3$.

* Preorder $\leqSig{1}$ coincides with preorder $\leqSig{0}$.

* Preorder $\leqSig{2}$ is a total order: $q_1 \lSig{2} q_2\lSig{2}q_3$.

Signature automata are not minimal in general, but we conjecture that by merging $\eqSig{d}$-equivalent states we should obtain a minimal automaton (see Section <ref> for more discussions).

§.§.§ Full progress consistency.
The existence of a "signature automaton" "recognising" an objective $W$ does not suffice to ensure "half-positionality" of $W$.
The problem is similar to the one we encountered when studying "open@@reg" objectives in Section <ref>: there are "open@@reg" objectives whose "residuals" are totally ordered but their are not "half-positional" (see Example <ref>). In that case, we needed to add the property of "progress consistency" to characterise "positionality@@half".
We generalise this notion to "signature automata" with multiple preorders.

We say that a "signature automaton" $\A$ is ""fully progress consistent"" if, for each preorder $\leqSig{x}$, for $x$ even, and every finite word $w\in \SS^*$:

\[ q\lSig{x} p \; \tand \; q\lrp{w:\geq x} p \;\; \implies \;\; w^\oo \in \Lang{\initialAut{\A}{q}}. \]

A "fully progress consistent" "signature automaton" is in particular "progress consistent", as the $\leqSig{0}$-preorder refines that coming from the inclusion of "residuals".

§.§.§ Structured signature automata from semantic properties of languages

To prove the implication <ref> $\implies$ <ref> from Theorem <ref>, we build a "signature automaton" from a "deterministic"  "parity automaton" $\A$ "recognising" $W$ recursively.
In order to be able to carry out the recursion, we will in fact obtain a "signature automaton" with even stronger properties. This reinforcement of "signature automata" is done by ensuring that the preorders $\leqSig{x}$ come from semantic properties of the automata, for which the notion of "${<}x$-safe languages" will play a major role.

The properties that are imposed are essentially a generalisation of the ones satisfied by the canonical "history-deterministic" coBüchi automata defined by Abu Radi and Kupferman <cit.>.

We introducing some further notation used in our semantic reinforcement of the definition of a signature automaton.

${<}x$-safe languages.
Let $\A$ be a (possibly "non-deterministic") "parity automaton". We define the ""$({<}x)$-safe language"" of a state $q$ of $\A$ as:

\[\intro*\safeSigAut{x}{q}{\A} = \{w\in \SS^*\cup \SS^\oo \mid \text{ there exists } q\lrp{w:\geq x}\}.\]

We remark that $\safeSigAut{x}{q}{\A}$ is completely determined by its finite (resp. infinite) words.
We drop the superscript $\A$ whenever the automaton is clear from the context.
A path producing no "priority" strictly smaller than $x$ is called ""$({<}x)$-safe@@path"".

Next lemma simply follows from the definition.

Let $\A$ be a "parity automaton" that is "deterministic over" transitions using priorities $\geq x$. Let $q$ and $p$ be two states such that $\safeSig{x}{q}\subseteq \safeSig{x}{p}$, and let $q\lrp{u:\geq x} q'$ be a "${<}x$-safe run" over $u$ from $q$. Then, there is a unique "${<}x$-safe run" over $u$ from $p$, $p\lrp{u:\geq x} p'$, and it leads to a state $p'$ satisfying $\safeSig{x}{q'}\subseteq \safeSig{x}{p'}$.

${<}x$-safe components.

A ""$({<}x)$-safe component"" of $\A$ is a "strongly connected component" of the "subautomaton" obtained by removing all transitions producing a priority $<x$ from $\A$. Note that if $\A$ is in "normal form" and $x>0$, transitions changing of "$({<}x)$-safe component" produce a "priority" $<x$. That is, $q\lrp{u:\geq x} p$ implies that $q$ and $p$ are in the same "$({<}x)$-safe component".

The partition of $\A$ into "${<}x$-safe components" is a "refinement" of its partition into "${<}y$-safe components", for $y\leq x$.

For the following, we fix a "parity automaton" $\A$ in "normal form" using priorities in $[0,d_{\max}]$. For each $x\in [1,d_{\max}]$, we will totally order the "${<}x$-safe components" of $\A$ in such a way that these orders successively refine each other.
For $x\in [1,d_{\max}]$ we let $\intro*\safeComp{x}_1,\dots, \safeComp{x}_{k_x}$ be the "${<}x$-safe components" of $\A$.
For $x=1$, we let $\safeComp{1}_1 <_1 S_2^{<1} <_1\dots <_1 S_{k_1}^{<1}$ be an arbitrary order over the "${<}1$-safe components".
Assume that an order has already been fixed at level $x-2$. Then, we fix an arbitrary total order for the "${<}x$-safe components" contained in a same "${<}(x-1)$-safe components", which yields a total order for the set of all those safe components, that refines the previous layers.