# Positionality in Σ and a Completeness Result

Pierre Ohlmann, Michal Skrzypczak

► To cite this version:

Pierre Ohlmann, Michal Skrzypczak. Positionality in Σ and a Completeness Result. Symposium on Theoretical Aspects of Computer Science (STACS), 2024, Clermont - Ferrand, France. 10.4230/LIPICS.STACS.2024.54 . hal-04894067

HAL Id: hal-04894067

https://amu.hal.science/hal-04894067v1

Submitted on 17 Jan 2025

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

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

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

Distributed under a Creative Commons Attribution 4.0 International License
# Positionality in $\Sigma_2^0$ and a Completeness Result

Pierre Ohlmann

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

Institute of Informatics, University of Warsaw, Poland

Michał Skrzypczak

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

Institute of Informatics, University of Warsaw, Poland

## Abstract

We study the existence of positional strategies for the protagonist in infinite duration games over arbitrary game graphs. We prove that prefix-independent objectives in $\Sigma_2^0$ which are positional and admit a (strongly) neutral letter are exactly those that are recognised by history-deterministic monotone co-Büchi automata over countable ordinals. This generalises a criterion proposed by [Kopczyński, ICALP 2006] and gives an alternative proof of closure under union for these objectives, which was known from [Ohlmann, TheoretiCS 2023].

We then give two applications of our result. First, we prove that the mean-payoff objective is positional over arbitrary game graphs. Second, we establish the following completeness result: for any objective $W$ which is prefix-independent, admits a (weakly) neutral letter, and is positional over finite game graphs, there is an objective $W'$ which is equivalent to $W$ over finite game graphs and positional over arbitrary game graphs.

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

Keywords and phrases infinite duration games, positionality, Borel class $\Sigma_2^0$, history determinism

Digital Object Identifier 10.4230/LIPIcs.STACS.2024.54

Funding Pierre Ohlmann: Author supported by the European Research Council (grant agreement No 948057 – BOBR).

Michał Skrzypczak: Author supported by the National Science Centre, Poland (grant no. 2021/41/B/ST6/03914).

Acknowledgements We thank Antonio Casares and Lorenzo Clemente for discussions on and around the topic.

# 1 Introduction

## 1.1 Context

**Games.** We study infinite duration games on graphs. In such a game, two players, Eve and Adam, alternate forever in moving a token along the edges of a directed, possibly infinite graph (called *arena*), whose edges are labelled with elements of some set $C$. An *objective* $W \subseteq C^\omega$ is specified in advance; Eve wins the game if the label of the produced infinite path belongs to $W$. A *strategy* in such a game is called *positional* if it depends only on the current vertex occupied by the token, regardless of the history of the play.

We are interested in *positional objectives*: those for which existence of a winning strategy for Eve entails existence of a winning positional strategy for Eve, on a arbitrary arena. Sometimes we also consider a weaker property: an objective is *positional over finite arenas* if the above implication holds on any finite arena.

<figure><img src="image_4.png" /></figure>
## 54:2 Positionality in $\Sigma_2^0$ and a Completeness Result

**Early results.** Although the notion of positionality is already present in Shapley's seminal work [29], the first positionality result for infinite duration games was established by Ehrenfeucht and Mycielsky [10], and it concerns the mean-payoff objective

$$ \text{Mean-Payoff}_{\le 0} = \{ w_0 w_1 \cdots \in \mathbb{Z}^\omega \mid \limsup_k \frac{1}{k} \sum_{i=0}^{k-1} w_i \le 0 \}, $$

over finite arenas. Nowadays, many proofs are known that establish positionality of mean-payoff games over finite arenas.

Later, and in a different context, Emerson and Jutla [11] as well as Mostowski [23] independently established positionality of the parity objective

$$ \text{Parity}_d = \{ p_0 p_1 \cdots \in \{0, 1, \dots, d\}^\omega \mid \limsup_k p_k \text{ is even} \} $$

over arbitrary arenas. This result was used to give a direct proof of the possibility of complementing automata over infinite trees, which is the key step in modern proofs of Rabin's theorem on decidability of S2S [27]. By now, several proofs are known for positionality of parity games, some of which apply to arbitrary arenas.

Both parity games and mean-payoff games have been the object of considerable attention over the past three decades; we refer to [12] for a thorough exposition. By symmetry, these games are positional not only for Eve but also for the opponent, a property we call *bi-positionality*. Parity and mean-payoff objectives, as well as the vast majority of objectives that are considered in this context, are *prefix-independent*, that is, invariant under adding or removing finite prefixes.

**Bi-positionality.** Many efforts were devoted to understanding positionality in the early 2000's. These culminated in Gimbert and Zielonka's work [15] establishing a general characterisation of bi-positional objectives over finite arenas, from which it follows that an objective is bi-positional over finite arenas if and only if it is the case for 1-player games. On the other hand, Colcombet and Niwiński [8] established that bi-positionality over arbitrary arenas is very restrictive: any prefix-independent objective which is bi-positional over arbitrary arenas can be recast as a parity objective.

Together, these two results give a good understanding of bi-positional objectives, both over finite and arbitrary arenas.

**Positionality for Eve.** In contrast, less is known about those objectives which are positional for Eve, regardless of the opponent (this is sometimes called half-positionality). This is somewhat surprising, considering that positionality is more in-line with the primary application in synthesis of reactive systems, where the opponent, who models an antagonistic environment, need not have structured strategies. The thesis of Kopczyński [19] proposes a number of results on positionality, but no characterisation. Kopczyński proposed two classes of prefix-independent objectives, *concave objectives* and *monotone objectives*, which are positional respectively over finite and over arbitrary arenas. Both classes are closed under unions, which motivated the following conjecture.

**Conjecture 1 (Kopczyński's conjecture [19, 18]).** *Prefix-independent positional objectives are closed under unions.*

This conjecture was disproved by Kozachinskiy in the case of finite arenas [20], however, it remains open for arbitrary ones (even in the case of countable unions instead of unions).
**Neutral letters.** Many of the considered objectives contain a *neutral letter*, that is an element $\epsilon \in C$ such that $W$ is invariant under removing arbitrary many occurrences of the letter $\epsilon$ from any infinite word. For instance, $\epsilon = 0$ is a neutral letter of the parity objective $\text{Parity}_d$. There are two variants of this definition, *strongly neutral letter* and *weakly neutral letter*, which are formally introduced in the preliminaries. It is unknown whether adding a neutral letter to a given objective may affect its positionality [19, 25].

Neutral letters are typically used when one wants to modify a given game arena, by
allowing players to make some additional decisions. This requires to create intermediate
edges in such a way that their labels do not affect the overall outcome of the play.

**Borel classes.** To stratify the complexity of the considered objectives we use the Borel hierarchy [17]. This follows the classical approach to Gale-Stewart games [13], where the determinacy theorem was gradually proved for more and more complex Borel classes: $\Sigma_2^0$ in [31] and $\Sigma_3^0$ in [9]. This finally led to Martin's celebrated result on all Borel objectives [22].

To apply this technique, we assume for the rest of the paper that *C* is at most countable. Thus, *C*<sup>ω</sup> is a Polish topological space, with open sets of the form *L* &middot; *C*<sup>ω</sup> where *L* &sube; *C*<sup>*</sup> is arbitrary. Closed sets are those whose complement is open. The class Σ<sub>2</sub><sup>0</sup> contains all sets which can be obtained as a countable union of some closed sets.

**Recent developments.** A step forward in the study of positionality (for Eve) was recently made by Ohlmann [25] who established that an objective admitting a (strongly) neutral letter is positional over arbitrary arenas if and only if it admits well-ordered monotone universal graphs. Note that this characterisation concerns only positionality over arbitrary arenas. This allowed Ohlmann to prove closure of prefix-independent positional objectives (over arbitrary arenas) admitting a (strongly) neutral letter under finite lexicographic products, and, further assuming membership in Σ<sub>2</sub><sup>0</sup>, under countable unions<sup>1</sup>.

Bouyer, Casares, Randour, and Vandenhove [2] also used universal graphs to characterise positionality for objectives recognised by deterministic Büchi automata. They observed that for such an objective W finiteness of the arena does not impact positionality: W is positional over arbitrary arenas if and only if it is positional over finite ones.

Going further, Casares and Ohlmann [6, 4] recently proved a characterisation of posi-
tionality for all $\omega$-regular objectives. As a by-product, it follows that Conjecture 1 holds for
$\omega$-regular objectives$^2$, and that again finiteness of the arena does not impact positionality.

**1.2 Contributions**

**Positionality in Σ<sub>2</sub><sup>0</sup>.** As mentioned above, Kopczyński introduced the class of *monotonic objectives*, defined as those of the form *C*<sup>ω</sup> \ *L*<sup>ω</sup>, where *L* is a language recognised by a finite linearly-ordered automaton with certain monotonicity properties on transitions. He then proved that monotonic objectives are positional over arbitrary arenas. Such objectives are prefix-independent and belong to Σ<sub>2</sub><sup>0</sup>; our first contribution is to extend Kopczyński's result to a complete characterisation (up to neutral letters) of positional objectives in Σ<sub>2</sub><sup>0</sup>.

<footnote n="1">¹ In [25], an assumption called “non-healing” is used. This assumption is in fact implied by membership in $\Sigma_2^0$.</footnote>

<footnote n="2">² In fact, Casares proved a strengthening of the conjecture when only one objective is required to be prefix-independent.</footnote>
54:4 Positionality in $\Sigma_2^0$ and a Completeness Result

**Theorem 2.** Let $W \subseteq C^\omega$ be a prefix-independent $\Sigma_2^0$ objective admitting a strongly neutral letter. Then $W$ is positional over arbitrary arenas if and only if it is recognised by a countable history-deterministic well-founded monotone co-Büchi automaton.

The proof of Theorem 2 is based on Ohlmann's *structuration* technique which is the key ingredient to the proof of [25]. As an easy by-product of the above characterisation, we reobtain the result that Kopczynski's conjecture holds for countable unions of $\Sigma_2^0$ objectives (assuming that the given objectives all have strongly neutral letters).

**Corollary 3.** If $W_0, W_1, \dots$ are all positional prefix-independent $\Sigma_2^0$ objectives, each admitting a strongly neutral letter, then the union $\bigcup_{i \in \mathbb{N}} W_i$ is also positional.

**From finite to arbitrary arenas.** The most important natural example of an objective which is positional over finite arenas but not over infinite ones is Mean-Payoff$_{\le 0}$, as defined above. As a straightforward consequence of their positionality [3, Theorem 3], it holds that over finite arenas, Mean-Payoff$_{\le 0}$ coincides with the energy condition

$$ \text{Bounded} = \{ w_0 w_1 \dots \in \mathbb{Z}^\omega \mid \sup_k \sum_{i=0}^{k-1} w_i \text{ is finite} \}, $$

which turns out to be positional even over arbitrary arenas [25].

Applying Corollary 3, we establish that with strict threshold, the mean-payoff objective

$$ \text{Mean-Payoff}_{<0} = \{ w_0 w_1 \dots \in \mathbb{Z}^\omega \mid \limsup_k \frac{1}{k} \sum_{i=0}^{k-1} w_i < 0 \} $$

is in fact positional over arbitrary arenas.

Now say that two prefix-independent objectives are *finitely equivalent*, written $W \equiv W'$, if they are won by Eve over the same finite arenas. As observed above, Mean-Payoff$_{\le 0} \equiv$ Bounded, which is positional over arbitrary arenas. Likewise, its complement

$$ \mathbb{Z}^\omega \setminus \text{Mean-Payoff}_{\le 0} = \{ w_0 w_1 \dots \in \mathbb{Z}^\omega \mid \limsup_k \frac{1}{k} \sum_{i=0}^{k-1} w_i \ge 0 \} $$

is, up to changing each weight $w \in \mathbb{Z}$ by the opposite one $-w \in \mathbb{Z}$, isomorphic to

$$ \{ w_0 w_1 \dots \in \mathbb{Z}^\omega \mid \liminf_k \frac{1}{k} \sum_{i=0}^{k-1} w_i < 0 \}. $$

The latter condition is finitely equivalent to Mean-Payoff$_{< 0}$ (where the $\liminf$ is replaced with a $\limsup$), which, as explained above, turns out to be positional over arbitrary arenas.

Thus, both Mean-Payoff$_{\le 0}$ and its complement are finitely equivalent to objectives that are positional over arbitrary arenas. This brings us to our main contribution, which generalises the above observation to any prefix-independent objective admitting a (weakly) neutral letter which is positional over finite arenas.

**Theorem 4.** Let $W \subseteq C^\omega$ be a prefix-independent objective which is positional over finite arenas and admits a weakly neutral letter. Then there exists an objective $W' \equiv W$ which is positional over arbitrary arenas.
**Structure of the paper.** Section 2 introduces all necessary notions, including Ohlmann's structurations results. Section 3 proves our characterisation result Theorem 2 and its consequence Corollary 3, and provides a few examples. Then we proceed in Section 4 with establishing positionality of Mean-Payoff<sub>0</sub> over arbitrary arenas, and proving Theorem 4.

## 2 Preliminaries

**Graphs.** We fix a set of letters $C$, which we assume to be at most countable. A $C$-graph $G$ is comprised of a (potentially infinite) set of vertices $V(G)$ together with a set of edges $E(G) \subseteq V(G) \times C \times V(G)$. An edge $e = (v, c, v') \in E(G)$ is written $v \stackrel{c}{\rightarrow} v'$, with $c$ being the label of this edge. We say that $e$ is outgoing from $v$, that it is incoming to $v'$, and that it is adjacent to both $v$ and to $v'$. We assume that each vertex $v \in V(G)$ has at least one outgoing edge (we call this condition being sinkless, with a sink understood as a vertex with no outgoing edge).

We say that $G$ is *finite* (resp. *countable*) if both $V(G)$ and $E(G)$ are finite (resp. countable). The size of a graph is defined to be $|G| = |V(G)|$.

A (finite) *path* is a (finite) sequence of edges with matching endpoints, meaning of the form $v_0 \xrightarrow{c_0} v_1, v_1 \xrightarrow{c_1} v_2, \dots$, which we conveniently write as $v_0 \xrightarrow{c_0} v_1 \xrightarrow{c_1} \dots$. We say that $\pi$ is a *path from $v_0$ in $G$*, and that vertices $v_0, v_1, v_2, \dots$ appearing on the path are reachable from $v_0$. We use $G[v_0]$ to denote the restriction of $G$ to vertices reachable from $v_0$. The label of a path $\pi$ is the sequence $c_0 c_1 \dots$ of labels of its edges; it belongs to $C^\omega$ if $\pi$ is infinite and to $C^*$ otherwise. We sometimes write $v \stackrel{w}{\rightsquigarrow}$ to say that $w$ labels an infinite path from $v$, or $v \stackrel{w}{\rightsquigarrow} v'$ to say that $w$ labels a finite path from $v$ to $v'$. We write $L(G, v_0) \subseteq C^\omega$ for the set of labels of all infinite paths from $v_0$ in $G$, and $L(G) \subseteq C^\omega$ for the set of labels of all infinite paths in $G$, that is the union of $L(G, v_0)$ over all $v_0 \in V(G)$.

A *graph morphism* from $G$ to $G'$ is a map $\phi: V(G) \rightarrow V(G')$ such that for every edge $v \xrightarrow{c} v' \in E(G)$, it holds that $\phi(v) \xrightarrow{c} \phi(v') \in E(G')$. We write $G \stackrel{\phi}{\rightarrow} G'$. We sometimes say that $G$ *embeds* in $G'$ or that $G'$ *embeds* $G$, and we write $G \rightarrow G'$, to say that there exists a morphism from $G$ to $G'$. Note that $G \rightarrow G'$ implies $L(G) \subseteq L(G')$.

A graph $G$ is $v_0$-rooted if it has a distinguished vertex $v_0 \in V(G)$ called the *root*. A tree $T$ is a $t_0$-rooted graph such that all vertices in $T$ admit a unique finite path from the root $t_0$.

**Games.** A $C$-arena is given by a $C$-graph $A$ together with a partition of its vertices $V(A) = V_{\text{Eve}} \sqcup V_{\text{Adam}}$ into those controlled by Eve $V_{\text{Eve}}$ and those controlled by Adam $V_{\text{Adam}}$. A *strategy* (for Eve) $(S, \pi)$ in an arena $A$ is a graph $S$ together with a surjective morphism $\pi: S \rightarrow A$ satisfying that for every vertex $v \in V_{\text{Adam}}$, every outgoing edge $v \xrightarrow{c} v' \in E(A)$, and every $s \in \pi^{-1}(v)$, there is an outgoing edge $s \xrightarrow{c} s' \in E(S)$ with $\pi(s') = v'$. Recall that under our assumptions every vertex needs to have at least one outgoing edge, thus for every $v \in V_{\text{Eve}}$ and every $s \in \pi^{-1}(v)$ there must be at least one outgoing edge from $s$ in $S$.

The example arenas in this work are drawn following a standard notation, where circles (resp. squares) denote vertices controlled by Eve (resp. Adam). Vertices with a single outgoing edge are denoted by a simple dot, it does not matter who controls them.

A strategy is *positional* if $\pi$ is injective. In this case, we can assume that $V(S) = V(A)$ and $E(S) \subseteq E(A)$, with $\pi$ being identity.

An *objective* is a set $W \subseteq C^\omega$ of infinite sequences of elements of $C$. In this paper, we will always work with *prefix-independent* objectives, meaning objectives which satisfy $cW = W$ for all $c \in C$; this allows us to simplify many of the definitions. A graph $G$ satisfies an objective $W$ if $L(G) \subseteq W$. A *game* is given by a $C$-arena $A$ together with an objective $W$.
54:6 Positionality in $\Sigma_2^0$ and a Completeness Result

It is winning (for Eve) if there is a strategy $(S, \pi)$ such that $S$ satisfies $W$. In this case, we also say that Eve wins the game $(A, W)$ with the strategy $(S, \pi)$. We say that an objective $W$ is positional (over finite arenas or over arbitrary arenas) if for any (finite or arbitrary) arena $A$, if Eve wins the game $(A, W)$ then she wins $(A, W)$ with a positional strategy.

**Neutral letters.** A letter $\varepsilon \in C$ is said to be weakly neutral for an objective $W \subseteq C^\omega$ if for any word $w \in C^\omega$ decomposed into $w = w_0w_1...$ with non-empty words $w_i \in C^+$,

$$w \in W \iff \varepsilon w_0 \varepsilon w_1 \varepsilon \cdots \in W.$$

A weakly neutral letter $\varepsilon \in C$ is strongly neutral if in the above, the $w_i$ can be chosen empty, and moreover, $\varepsilon^\omega \in W$.

A few examples: for the parity objective, the priority 0 is strongly neutral; for Bounded, the weight 0 is strongly neutral; for Mean-Payoff$_{\le 0}$, the letter 0 is only weakly neutral (because $1^\omega \notin$ Mean-Payoff$_{\le 0}$ however $010010001\cdots \in$ Mean-Payoff$_{\le 0}$), and likewise for Mean-Payoff$_{< 0}$ because $0^\omega \notin$ Mean-Payoff$_{< 0}$.

**Monotone and universal graphs.** An ordered graph is a graph $G$ equipped with a total order $\ge$ on its set of vertices $V(G)$. We say that it is monotone if

$$v \ge u \stackrel{c}{\rightarrow} v' \ge u' \text{ in } G \quad \text{implies} \quad v \stackrel{c}{\rightarrow} v' \in E(G).$$

Such a graph is well founded if the order $\ge$ on $V(G)$ is well founded.

We will use a variant of universality called (uniform) almost-universality (for trees), which is convenient when working with prefix-independent objectives. A C-graph $U$ is almost W-universal, if $U$ satisfies $W$, and for any tree $T$ satisfying $W$, there is a vertex $t \in V(T)$ such that $T[t] \rightarrow U$. We will rely on the following inductive result from [25].

**Theorem 5 (Follows from Theorem 3.2 and Lemma 4.5 in [25]).** Let $W \subseteq C^\omega$ be a pre-fix-independent objective such that there is a graph which is almost W-universal. Then $W$ is positional over arbitrary arenas.

**Structuration results.** The following results were proved in Ohlmann's PhD thesis (Theorems 3.1 and 3.2 in [24]); the two incomparable variants stem from two different techniques.

**Lemma 6 (Finite structuration).** Let $W$ be a prefix-independent objective which is positional over finite arenas and admits a weakly neutral letter, and let $G$ be a finite graph satisfying $W$. Then there is a monotone graph $G'$ satisfying $W$ such that $G \rightarrow G'$.

**Lemma 7 (Infinite structuration).** Let $W$ be a prefix-independent objective which is positional over arbitrary arenas and admits a strongly neutral letter, and let $G$ be any graph satisfying $W$. Then there is a well-founded monotone graph $G'$ satisfying $W$ such that $G \rightarrow G'$.

Note that in both results, we may assume that $|G'| \le |G|$, simply by restricting to the image of $G$. Details of the proof of Lemma 7 can be found in [25, Theorem 3]; Lemma 6 appears only in Ohlmann's PhD thesis [24].

**Automata.** A co-Büchi automaton over $C$ is a $q_0$-rooted $C \times \{\mathcal{N}, \mathcal{F}\}$-graph $A$. In this context, vertices $V(A)$ are called states, edges $E(A)$ are called transitions, and the root $q_0$ is called the initial state. Moreover, transitions of the form $q \xrightarrow{(c, \mathcal{N})} q'$ are called normal transitions and simply denoted $q \stackrel{c}{\rightarrow} q'$, while transitions of the form $q \xrightarrow{(c, \mathcal{F})} q'$ are called
co-Büchi transitions and denoted $q \stackrel{c}{\rightarrow} q'$. For simplicity, we assume automata to be complete (for any state $q$ and any letter $c$, there is at least one outgoing transition labelled $c$ from $q$) and reachable (for any state $q$ there is some path from $q_0$ to $q$ in $A$).

A path $q_0 \xrightarrow{(c_0,a_0)} q_1 \xrightarrow{(c_1,a_1)} \dots$ in $A$ is *accepting* if it contains only finitely many co-Büchi transitions, meaning that only finitely many of $a_i$ equal $\mathcal{F}$. If $q \in V(A)$ is a state then define the *language* $L(A, q) \subseteq C^\omega$ of a co-Büchi automaton from a state $q \in V(A)$ as the set of infinite words which label accepting paths from $q$ in $A$. The *language* of $A$ denoted $L(A)$ is $L(A, q_0)$. Note that in this paper, automata are not assumed to be finite.

We say that an automaton is *monotone* if it is monotone as a $C \times \{\mathcal{N}, \mathcal{F}\}$-graph. Likewise, morphisms between automata are just morphisms of the corresponding $C \times \{\mathcal{N}, \mathcal{F}\}$-graphs that moreover preserve the initial state. Note that $A \to A'$ implies $L(A) \subseteq L(A')$. A co-Büchi automaton is *deterministic* if for each state $q \in V(A)$ and each letter $c \in C$ there is exactly one transition labelled by $c$ outgoing from $q$.

A resolver for an automaton $A$ is a deterministic automaton $R$ with a morphism $R \to A$. Note that the existence of this morphism implies that $L(R) \subseteq L(A)$. Such a resolver is *sound* if additionally $L(R) \supseteq L(A)$ (and thus $L(R) = L(A)$). A co-Büchi automaton is *history-deterministic* if there exists a sound resolver $R$. Our definition of history-determinism is slightly non-standard, but it fits well with our overall use of morphisms and of possibly infinite automata. This point of view was also adopted by Colcombet (see [7, Definition 13]). For more details on history-determinism of co-Büchi automata, we refer to [21, 1, 28].

We often make use of the following simple lemma, which follows directly from the definitions and the fact that composing morphisms results in a morphism.

**Lemma 8.** Let $A$, $A'$ be automata such that $A \to A'$, $A$ is history-deterministic, and $L(A) = L(A')$. Then $A'$ is history-deterministic.

Say that an automaton $A$ is *saturated* if it has all possible co-Büchi transitions: $V(A) \times (C \times \{\mathcal{F}\}) \times V(A) \subseteq E(A)$. The saturation of an automaton $A$ is obtained from $A$ by adding all possible co-Büchi transitions. Similar techniques of saturating co-Büchi automata have been previously used to study their structure [21, 16, 28].

Note that languages of saturated automata are always prefix-independent. The lemma below states that co-Büchi transitions are somewhat irrelevant in history-deterministic automata recognising prefix-independent languages.

**Lemma 9.** Let $A$ be a history-deterministic automaton recognising a prefix-independent language and let $A'$ be its saturation. Then $L(A) = L(A')$ and $A'$ is history-deterministic. Moreover, $L(A') = L(A', q)$ for any state $q$ of $A'$.

**Proof.** Clearly $A \to A'$ thus $L(A) \subseteq L(A')$; it suffices to prove $L(A') \subseteq L(A)$ and conclude by Lemma 8. Let $w_0w_1\cdots \in L(A')$ and let $q_0 \xrightarrow{(w_0,a_0)} q_1 \xrightarrow{(w_1,a_1)} \cdots$ be an accepting path for $w$ in $A'$. Then for some $i$, $q_i \xrightarrow{(w_i,a_i)} q_{i+1} \xrightarrow{(w_{i+1},a_{i+1})} \cdots$ is comprised only of normal transitions. Thus, this suffix of the path does not use edges added during the saturation process, which means this suffix is an accepting path in $A$. We conclude that $w_iw_{i+1}\cdots \in L(A)$ and thus $w \in L(A)$ by prefix-independence.

The claim that $L(A', q)$ is independent on $q$ follows directly from prefix-independence and the fact that $A'$ is saturated. $\quad$

<figure><img src="image_5.png" /></figure>
# 3 Positional prefix-independent $\Sigma_2^0$ objectives

## 3.1 A characterisation

Recall that $\Sigma_2^0$ objectives are countable unions of closed objectives; for the purpose of this paper it is convenient to observe that these are exactly those objectives recognised by (countable) deterministic co-Büchi automata (see for instance [30]).

The goal of the section is to prove Theorem 2 which we now restate for convenience.

**▶ Theorem 2.** Let $W \subseteq C^\omega$ be a prefix-independent $\Sigma_2^0$ objective admitting a strongly neutral letter. Then $W$ is positional over arbitrary arenas if and only if it is recognised by a countable history-deterministic well-founded monotone co-Büchi automaton.

Before moving on to the proof, we proceed with a quick technical statement that allows us to put automata in a slightly more convenient form.

**▶ Lemma 10.** Let $A$ be a history-deterministic automaton recognising a non-empty prefix-independent language. There exists a history-deterministic automaton $A'$ with $L(A') = L(A)$ and such that from every state $q' \in V(A')$, there is an infinite path comprised only of normal transitions. Moreover, if $A$ is countable, well founded, and monotone, then so is $A'$.

**Proof.** Let $V \subseteq V(A)$ be the set of states $q \in V(A)$ from which there is an infinite path of normal transitions. Note that $V \neq \emptyset$ since $L(A)$ is non-empty. First, since every path from $V(A) \setminus V$ visits at least one co-Büchi transition, we turn all normal transitions adjacent to states in $V(A) \setminus V$ into co-Büchi ones; this does not affect $L(A)$ or history-determinism. Next, we saturate $A$ and restrict it to $V$. Call $A'$ the resulting automaton; if $q_0 \notin V$ then we pick the initial state $q'_0$ of $A'$ arbitrarily in $V$. It is clear that restricting $A$ to some subset of states, changing the initial state, as well as saturating, are operations that preserve being countable, well founded, and monotone.

We claim that $L(A) = L(A')$. The inclusion $L(A') \subseteq L(A)$ follows from the proof of Lemma 9 so we focus on the converse: let $w = w_0w_1\cdots \in L(A)$ and take an accepting path $\pi$ for $w$. Then there is a suffix of $\pi$ which remains in $V$ and therefore defines a path in $A'$; we conclude thanks to prefix-independence of $L(A')$.

It remains to see that $A'$ is history-deterministic. For this, we observe that any transition adjacent to states in $V(A) \setminus V$ is a co-Büchi transition; therefore the map $\phi: V(A) \to V(A') = V$ which is identity on $V$ and sends $V(A) \setminus V$ to the initial state of $A'$ defines a morphism $A \to A'$. We conclude by Lemma 8. ◀

To prove Theorem 2, we separate both directions so as to provide more precise hypotheses.

**▶ Lemma 11.** Let $W$ be a prefix-independent $\Sigma_2^0$ objective admitting a strongly neutral letter. Then $W$ is recognised by a countable history-deterministic monotone well-founded automaton.

**Proof.** If $W = \emptyset$ then the saturated automaton with a single state and no normal transitions gives the wanted result; therefore we assume $W$ to be non-empty. Let $A$ be a history-deterministic co-Büchi automaton recognising $W$ with initial state $q_0$; thanks to Lemma 10 we assume that every state in $A$ participates in an infinite path of normal transitions. Let $G$ be the $C$-graph obtained from $A$ by removing all the co-Büchi transitions. The fact that $G$ is sinkless (and therefore, $G$ is indeed a graph) follows from the assumption on $A$. Since $W$ is prefix-independent, it holds that $G$ satisfies $W$.
Apply the infinite structuration result (Lemma 7, which requires the strongly neutral letter) to G to obtain a well-founded monotone graph $G'$ satisfying W and such that $G \xrightarrow{\phi} G'$. Note that we may restrict $V(G')$ to the image of $\phi$. Due to the fact that C is countable, this guarantees that $G'$ is countable.

Now let $A'$ be the co-Büchi automaton obtained from $G'$ by turning every edge into a normal transition, setting the initial state to be $q'_0 = \phi(q_0)$, and saturating. Note that $A'$ is countable monotone and well-founded; we claim that $A'$ is history-deterministic and recognises W, as required.

Let $w \in L(A')$. Then $w = uw'$ where $w' \in L(G') \subseteq W$. It follows from prefix-independence that $w \in W$. Conversely, let $w_0w_1\cdots \in W$ as witnessed by an accepting path $\pi = q_0 \xrightarrow{(w_0,a_0)} q_1 \xrightarrow{(w_1,a_1)} \dots$ from $q_0$ in A. This path has only finitely many co-Büchi transitions.

Then consider the path $\pi' = \phi(q_0) \xrightarrow{w_0} \phi(q_1) \xrightarrow{w_1} \dots$ in $A'$, where we use co-Büchi transitions only when necessary, meaning when there is no normal transition $\phi(q_i) \xrightarrow{w_i} \phi(q_{i+1})$ in $A'$. Since $\pi$ visits only finitely many co-Büchi transitions, it is eventually a path in G, and thus since $\phi$ is a morphism, $\pi'$ is eventually a path in $G'$, and hence it sees only finitely many co-Büchi transitions in $A'$. Hence $L(A') = W$.

It remains to show that $A'$ is history-deterministic. But since $A'$ is saturated and $G \to G'$ we have $A \to A'$ and thus Lemma 8 concludes. ◀

For the converse direction, we do not require a neutral letter.

**► Lemma 12.** If W is a prefix-independent objective recognised by a countable history-deterministic monotone well-founded co-Büchi automaton then W is positional over arbitrary arenas.

**Proof.** As previously, if W is empty then it is trivially positional, so we assume that W is non-empty, and we take an automaton A satisfying the hypotheses above and apply Lemma 10 so that every state participates in an infinite path of normal transitions. Let U be the C-graph obtained from A by removing all co-Büchi transitions and turning normal transitions into edges; thanks to Lemma 10, U is sinkless so it is indeed a graph. We prove that U is almost W-universal for trees. Let T be a tree satisfying W and let $t_0$ be its root.

Since A is history-deterministic, there is a mapping $\phi : V(T) \to V(A)$ such that for each edge $t \stackrel{c}{\to} t' \in E(T)$, there is a transition $\phi(t) \xrightarrow{(c,a)} \phi(t')$ in A with some $a \in \{\mathcal{N}, \mathcal{F}\}$, and such that for all infinite paths $t_0 \xrightarrow{w_0} t_1 \xrightarrow{w_1} \dots$ in T, there are only finitely many co-Büchi transitions on the path $\phi(t_0) \xrightarrow{(w_0,a_0)} \phi(t_1) \xrightarrow{(w_1,a_1)} \dots$ in A.

► Claim 13. There is a vertex $t'_0 \in V(T)$ such that for all infinite paths $t'_0 \xrightarrow{w_0} t'_1 \xrightarrow{w_1} \dots$ from $t'_0$ in T, there is no co-Büchi transition on the path $\phi(t_0) \xrightarrow{w_0} \phi(t_1) \xrightarrow{w_1} \dots$ in A.

**Proof.** Assume towards contradiction that no such vertex exists. Then starting from the root $t_0$, we build an infinite path $t_0 \xrightarrow{w_0} t_1 \xrightarrow{w_1} \dots$ in T such that $\phi(t_0) \xrightarrow{w_0} \phi(w_1) \xrightarrow{w_1} \dots$ has infinitely many co-Büchi transitions in A. Indeed, assuming the path built up to $t_i$, we simply pick $t_i \xrightarrow{w_i} t_{i+1}$ such that there is a co-Büchi transition in A on the corresponding path $\phi(t_i) \xrightarrow{w_i} \phi(t_{i+1})$. Thus, we constructed a path contradicting the observation below: this path has infinitely many co-Büchi transitions in A. ◁

There remains to observe that $\phi$ maps $T[t'_0]$ to U, and thus U is almost W-universal for trees. We conclude by applying Lemma 5. ◁
54:10 Positionality in $\Sigma_2^0$ and a Completeness Result

## 3.2 A few examples

**Kopczyński-monotonic objectives.** In our terminology, Kopczyński's monotonic objectives correspond to the prefix-independent languages that are recognised by finite monotone co-Büchi automata. Note that such automata are of course well-founded, but also they are history-deterministic (even determinisable by pruning): one should always follow a transition to a maximal state. Therefore our result proves that such objectives are positional over arbitrary arenas. A very easy example is the co-Büchi objective

$$ \text{co-Büchi} = \{w \in \{\mathcal{N}, \mathcal{F}\}^{\omega} \mid w \text{ has finitely many occurrences of } \mathcal{F}\}, $$

which is recognised by a (monotone) automaton with a single state. Some more advanced examples are given in Figure 1.

<figure><img src="image_6.png" /><figcaption>■ **Figure 1** Two finite monotone co-Büchi automata recognising prefix-independent languages. For clarity, the co-Büchi transitions are not depicted but connect every pair of states; likewise, edges following from monotonicity (such as the dashed ones for example), are omitted. The automaton on the left recognises words with finitely many *aab* infixes. The automaton on the right recognises words with finitely many infixes in $c(a^*cb^*)^+c$.</figcaption></figure>

**Finite support.** The finite support objective is defined over $\omega$ by

$$ \text{Finite} = \{w \in \omega^{\omega} \mid \text{finitely many distinct letters appear in } w\} $$

Consider the automaton $A$ over $V(A) = \omega$ with

$$ v \xrightarrow{w} v' \in E(A) \iff w, v' \le v, $$

co-Büchi transitions everywhere, and initial state 0 (see Figure 2).

<figure><img src="image_7.png" /><figcaption>■ **Figure 2** An automaton $A$ for objective Finite. Co-Büchi edges, as well as some edges following from monotonicity (such as the dashed one) are omitted for clarity.</figcaption></figure>

It is countable, history-deterministic, well-founded, and monotone and recognises $L(A) = \text{Finite}$. Details of the proof are easy and left to the reader. Positionality of Finite can also be established by Corollary 3, as it is a countable union of the safety languages $F^{\omega} \subseteq \omega^{\omega}$, where $F$ ranges over finite subsets of $\omega$. As far as we are aware, this result is novel.<fnref n="3" />

<footnote n="3">³ A similar positionality result is proved in [14], but it assumes finite degree of the arena, vertex-labels (which is more restrictive), and injectivity of the colouring of the arena.</footnote>
**Energy objectives.** Recall the energy objective

$$ \text{Bounded} = \{ w_0 w_1 \cdots \in \mathbb{Z}^\omega \mid \sup_k \sum_{i=0}^{k-1} w_i \text{ is finite} \}, $$

which is prefix-independent and belongs to $\Sigma_2^0$. Consider the automaton A whose set of states is $\omega$, with the initial state 0 and with all possible co-Büchi transitions, and normal transitions of the form $v \xrightarrow{w} v'$ where $w \le v - v'$. Note that A is well-founded and monotone, so we should prove that it is history-deterministic and recognises Bounded.

Note that any infinite path of normal edges $v_0 \xrightarrow{w_0} v_1 \xrightarrow{w_1} \dots$ in A is such that for all $i$, $w_i \le v_i - v_{i+1}$, and therefore

$$ \sum_{i=0}^{k-1} w_i \le v_0 - v_k \le v_0 $$

and thus $L(A) \subseteq$ Bounded.

A resolver for A works as follows: keep a counter c (initialised to zero), and along the run, from a vertex v and when reading an edge w,

- if $v \ge w$ then take the normal transition $v \xrightarrow{w} v - w$;

- otherwise, take the co-Büchi transition $v \xrightarrow{w} c$ and increment the counter.

**Eventually non-increasing objective.** Over the alphabet $\omega$, consider the objective

$$ \text{ENI} = \{ w_0 w_1 \cdots \in \omega^\omega \mid \text{there are finitely many } i \text{ such that } w_{i+1} > w_i \}. $$

Note that since $\omega$ is well-founded, a sequence belongs to ENI if and only if it is eventually constant. Consider the automaton A over $\omega$ with the initial state 0, with all possible co-Büchi transitions, and with normal transitions $v \xrightarrow{w} v'$ if and only if $v \ge w \ge v'$. Note that A is countable, well-founded, and monotone, so we should prove that it recognises ENI and is history-deterministic.

First, note that any infinite path of normal edges $v_0 \xrightarrow{w_0} v_1 \xrightarrow{w_1} \dots$ in A is such that $v_0 \ge w_0 \ge v_1 \ge w_1 \ge \dots$, and therefore $L(A) \subseteq$ ENI. A sound resolver for A simply goes to the state w when reading a letter w, using a normal transition if possible, and a co-Büchi transition otherwise. We leave the formal definition to the reader.

**Eventually non-decreasing objective.** In contrast, the objective

$$ \text{END} = \{ w_0 w_1 \cdots \in \omega^\omega \mid \text{there are finitely many } i \text{ such that } w_{i+1} < w_i \}. $$

is not positional over arbitrary arenas, as witnessed by Figure 3.

<figure><img src="image_8.png" /><figcaption>■ **Figure 3** An arena over which Eve requires a non-positional strategy in order to produce a sequence which is eventually non-decreasing.</figcaption></figure>
## 3.3 Closure under countable unions

We now move on to Corollary 3, which answers Kopczyński's conjecture in the affirmative in the case of $\Sigma_2^0$ objectives.

**Corollary 3.** If $W_0, W_1, \dots$ are all positional prefix-independent $\Sigma_2^0$ objectives, each admitting a strongly neutral letter, then the union $\bigcup_{i \in \mathbb{N}} W_i$ is also positional.

**Proof.** Let $W_0, W_1, \dots$ be a family of countably many prefix-independent $\Sigma_2^0$ objectives admitting strongly neutral letters. Using Theorem 2 we get countable history-deterministic well-founded monotone co-Büchi automata $A_0, A_1, \dots$ for the respective objectives; without loss of generality we assume that they are saturated (Lemma 9).

Then consider the automaton $A$ obtained from the disjoint union of the $A_i$'s by adding all possible co-Büchi transitions, and all normal transitions from $A_i$ to $A_j$ with $i > j$. The initial state in $A$ can be chosen arbitrarily. Note that $A$ is well-founded, monotone, and countable, so we should prove that it recognises $W = \bigcup_i W_i$ and is history-deterministic.

Note that any infinite path in $A$ which visits finitely many co-Büchi transitions eventually remains in some $A_i$, and thus by prefix-independence, $L(A) \subseteq W$.

It remains to prove history-determinism of $A$. Let $R_0, R_1, \dots$ be resolvers for $A_0, A_1, \dots$ witnessing that these automata are history deterministic. Consider a resolver which stores a sequence of states $(r_0, r_1, \dots)$, with $r_i$ being a state of $R_i$. Initially these are all initial states of the respective resolvers and the transitions follow the transitions of all the resolvers synchronously. Additionally, we store a round-robin counter, which indicates one of the resolvers, following the sequence $R_0; R_0, R_1; R_0, R_1, R_2; R_0, R_1, R_2, R_3; \dots$ If we see a normal transition in the currently indicated resolver, then we also see a normal transition in $R$, and otherwise, we update the counter to the next resolver and see a co-Büchi transition in $R$.

We now prove that the above resolver is sound. For that, consider a word $w$ which belongs to $L(A_n)$ for some $n$. Assume for the sake of contradiction that the path in $A$ constructed by the above resolver reading $w$ contains infinitely many co-Büchi transitions. It means that infinitely many times the resolver $R_n$ reached a co-Büchi state in $A_n$. But this contradicts the assumption that $R_n$ is sound. We conclude that $W$ is positional by applying Lemma 12. ◀

# 4 From finite to arbitrary arenas

In this section we study the difference between positionality over finite and arbitrary arenas.

## 4.1 Mean-payoff games

There are, in fact, four non-isomorphic variants of the mean-payoff objective. Three of them fail to be positional over arbitrary arenas (even over bounded degree arenas), as expressed by the following facts.

**Proposition 14.** *The mean-payoff objective Mean-Payoff$_{\le 0}$ over $w_0w_1\cdots \in \mathbb{Z}^\omega$ with the condition $\limsup_k \frac{1}{k} \sum_{i=0}^{k-1} w_i \le 0$ is not positional over arbitrary arenas.*

**Proof.** Consider the arena depicted on Figure 4. Eve can win by following bigger and bigger loops which reach arbitrarily far to the right. This strategy brings the average of the weights closer and closer to 0.

Nevertheless, each positional strategy of Eve either moves infinitely far to the right (resulting in $\lim_k \frac{1}{k} \sum_{i=0}^{k-1} w_i = 1$) or repeats some finite loop which results in a fixed positive limit $\lim_k \frac{1}{k} \sum_{i=0}^{k-1} w_i > 0$. In both cases it violates Mean-Payoff$_{\le 0}$. ◂
<figure><img src="image_9.png" /><figcaption>Figure 4 The arena used in the proof of Proposition 14.</figcaption></figure>

**Proposition 15.** Consider two lim inf variants of the mean-payoff objective over $w_0w_1 \cdots \in \mathbb{Z}^\omega$: one where we require that $\liminf_k \frac{1}{k} \sum_{i=0}^{k-1} w_i \le 0$, and the other where that same quantity is $< 0$. Both these objectives are not positional over arbitrary arenas.

<figure><img src="image_10.png" /><figcaption>Figure 5 The arena used in the proof of Proposition 15.</figcaption></figure>

**Proof.** Consider the arena depicted on Figure 5. Again, Eve has a winning strategy for both these objectives by always going sufficiently far to the left, to ensure that the average drops below for instance $-\frac{1}{2}$.

Nevertheless, each positional strategy of Eve either moves infinitely far to the left (resulting again in $\lim_k \frac{1}{k} \sum_{i=0}^{k-1} w_i = 1$), or repeats some finite loop, reaching a minimal negative weight $-2^n$ for some $n > 0$. Now, Adam can win against this strategy by repeating a loop going to the right, in such a way to reach a weight $2^{n+1}$. The label of such a path satisfies $\lim_k \frac{1}{k} \sum_{i=0}^{k-1} w_i = \frac{2^{n+1}-1}{4n+4} > 0$, violating both objectives. ◀

The remaining fourth type of a mean-payoff objective is „lim sup $< 0$“:

$$ \text{Mean-Payoff}_{<0} = \{ w_0 w_1 \cdots \in \mathbb{Z}^\omega \mid \limsup_k \frac{1}{k} \sum_{i=0}^{k-1} w_i < 0 \}. $$

**Proposition 16.** The objective Mean-Payoff$_<0$ is positional over arbitrary arenas.

**Proof.** Consider the tilted boundedness objective with parameter $n \ge 1$, defined as

$$ \text{Tilted-Bounded}_n = \{ w_0 w_1 \cdots \in \mathbb{Z}^\omega \mid \sup_k \sum_{i=0}^{k-1} (w_i + 1/n) \text{ is finite} \} $$

Note that renaming weights by $w \mapsto nw$ maps Tilted-Bounded$_n$ to Bounded$\cap (nw\mathbb{Z})^\omega$, therefore it follows easily that Tilted-Bounded$_n$ is positional over arbitrary arenas. Note also that for every $n$ the objective Tilted-Bounded$_n$ belongs to $\Sigma_2^0$, as a union ranging over $N \in \mathbb{N}$ of closed (in other words safety) objectives $\{w_0 w_1 \cdots \in \mathbb{Z}^\omega \mid \forall k \in \mathbb{N} \sum_{i=0}^{k-1} (w_i + 1/n) \le N\}$.

▷ Claim 17. It holds that Mean-Payoff$_<0 = \bigcup_{n \ge 1} \text{Tilted-Bounded}_n$.
54:14 Positionality in $\Sigma_2^0$ and a Completeness Result

Proof of Claim 17. Write $mp(w) = \limsup_k 1/k \sum_{i=0}^{k-1} w_i$. If

$$w = w_0 w_1 \cdots \in \text{Tilted-Bounded}_n$$

then there is a bound $N$ such that for all $k$, $\sum_{i=0}^{k-1} (w_i + 1/n) \le N$, therefore $1/k \sum_{i=0}^{k-1} w_i \le N/k - 1/n$ and thus $mp(w) \le -1/n < 0$, so $w \in \text{Mean-Payoff}_{<0}$. Conversely, if $w \in \text{Mean-Payoff}_{<0}$ and $n$ is large enough so that $1/n \le mp(w)$, then $w \in \text{Tilted-Bounded}_n$. $\triangleleft$

Now, positionality of $\text{Mean-Payoff}_{<0}$ follows from the claim together with Corollary 3, as all $\text{Tilted-Bounded}_n$ are prefix-independent, admit a strongly neutral letter, are positional, and belong to $\Sigma_2^0$.<fnref n="4" />

## 4.2 A completeness result

**Equivalence over finite arenas.** Recall that two prefix-independent objectives $W, W' \subseteq C^\omega$ are said to be *finitely equivalent*, written $W \equiv W'$, if for all finite $C$-arenas $A$,

$$\text{Eve wins } (A, W) \iff \text{Eve wins } (A, W').$$

Since one may view strategies as games controlled by Adam, we obtain the following motivating result.

**Lemma 18.** If $W \equiv W'$ and $W$ is positional over finite arenas then so is $W'$.

**Proof.** Let $A$ be a finite $C$-arena such that Eve wins $(A, W')$. Then Eve wins $(A, W)$, so she wins with a positional strategy $S$. Looking at $S$ as a finite $C$-arena controlled by Adam yields that Eve wins $(S, W')$, thus $S$ satisfies $W'$. $\triangleleft$

We now move on to the proof of our completeness result.

**Theorem 4.** Let $W \subseteq C^\omega$ be a prefix-independent objective which is positional over finite arenas and admits a weakly neutral letter. Then there exists an objective $W' \equiv W$ which is positional over arbitrary arenas.

We start with the following observation, which is a standard topological argument based on König's lemma. Note that the assumption of finiteness of $G$ is essential here.

**Lemma 19.** Let $G$ be a finite $C$-graph and $v \in G$. Then $L(G, v)$ is a closed subset of $C^\omega$.

We may now give the crucial definition. Given a prefix-independent objective $W \subseteq C^\omega$, we define its finitary substitute to be

$$W_{\text{fin}} = \{w \in C^\omega \mid w \text{ labels a path in some finite graph } G \text{ which satisfies } W\}.$$

Note that $W_{\text{fin}} \subseteq W$. Now observe that

$$W = \bigcup_{\substack{G \text{ finite graph} \\ G \text{ satisfies } W}} L(G) = \bigcup_{\substack{G \text{ finite graph} \\ G \text{ satisfies } W \\ v \in V(G)}} L(G, v),$$

and since there are (up to isomorphism) only countably many finite graphs, it follows from Lemma 19 that $W_{\text{fin}} \in \Sigma_2^0$.

<footnote n="4">⁴ We thank Lorenzo Clemente for suggesting to use closure under union. A direct proof (constructing a universal graph) is available in the unpublished preprint [26].</footnote>
**Lemma 20.** Let $W \subseteq C^\omega$ be a prefix-independent objective which is positional over finite arenas. Then $W_{\text{fin}} \equiv W$.

**Proof.** Let $A$ be a finite $C$-arena. Since $W_{\text{fin}} \subseteq W$, it is clear that if Eve wins $(A, W_{\text{fin}})$ then she wins $(A, W)$. Conversely, assume Eve wins $(A, W)$. Then she has a positional strategy $S$ in $A$ which is winning for $W$. Since $S$ is a finite graph, it is also winning for $W_{\text{fin}}$ and therefore Eve wins $(A, W_{\text{fin}})$. ◀

We should make the following sanity check.

**Lemma 21.** If $W$ is prefix-independent, then $W_{\text{fin}}$ as well.

**Proof.** Take a letter $c \in C$, we aim to show that $cW_{\text{fin}} = W_{\text{fin}}$. Let $w \in cW_{\text{fin}}$, and let $G$ be a finite graph satisfying $W$ such that $cw$ labels a path from $v \in V[G]$ in $G$. Then $w$ labels a path from a $c$-successor of $v$ in $G$, thus $w \in W_{\text{fin}}$.

Conversely, let $w \in W_{\text{fin}}$, and let $G$ be a finite graph satisfying $W$ such that $w$ labels a path from $v \in V[G]$ in $G$. Let $G'$ be the graph obtained from $G$ by adding a fresh vertex $v'$ with a unique outgoing $c$-edge towards $v$. Since $W$ is prefix-independent, $G'$ satisfies $W$. Since $cw$ labels a path from $v'$ in $G'$, it follows that $cw \in W_{\text{fin}}$. ◀

We are now ready to prove Theorem 4.

**Proof of Theorem 4.** Let $W$ be a prefix-independent objective which is positional over finite arenas and admits a weakly neutral letter $\varepsilon$. We show that $W_{\text{fin}}$ is positional over arbitrary arenas. Since Lemma 20 implies that $W_{\text{fin}} \equiv W$, this concludes the proof of Theorem 4.

Thanks to Lemma 6, any finite graph $H$ satisfying $W$ can be embedded into a monotone finite graph $G$ which also satisfies $W$; note that $L(H) \subseteq L(G)$. Therefore

$$W_{\text{fin}} = \bigcup_{\substack{H \text{ finite graph} \\ H \text{ satisfies W}}} L(H) = \bigcup_{\substack{G \text{ finite monotone graph} \\ G \text{ satisfies W}}} L(G).$$

Let $G_0, G_1, \dots$ be an enumeration (up to isomorphism) of all finite monotone graphs satisfying $W$. Then consider the automaton $A$ obtained from the disjoint union of the $G_i$'s by adding all normal transitions from $G_i$ to $G_j$ for $i > j$, and saturating with co-Büchi transitions. The initial state $q_0$ is chosen to be $\max V(G_0)$, the maximal state in $G_0$. Note that $A$ is countable, monotone, and well founded, so there remains to prove that $L(A) = W_{\text{fin}}$ and that $A$ is history-deterministic.

Clearly for any monotone graph $G$ satisfying $W$, it holds that $L(G) \subseteq L(A)$, and thus $W_{\text{fin}} \subseteq L(A)$. Conversely, let $w \in L(A)$, and consider an accepting path $\pi$ for $W$. Then eventually, $\pi$ visits only normal edges, and therefore eventually, $\pi$ remains in some $G_i$. Thus $w = uw'$ with $w' \in L(G_i) \subseteq W_{\text{fin}}$, we conclude by prefix-independence of $W_{\text{fin}}$ (Lemma 21).

To prove that $A$ is history-deterministic we now build a resolver: intuitively, we deterministically try to read in $G_0$, then if we fail, go to $G_1$, then $G_2$ and so on. The fact that reading in each $G_i$ can be done deterministically follows from monotonicity: for each $v \in V(G_i)$ and each $c \in C$, the set $\{v' \in V(G_i) \mid v \stackrel{c}{\to} v' \in E(G_i)\}$ of $c$-successors of $v$ is downward closed. We let $\delta_i(v, c)$ denote the maximal $c$-successor of $v$ in $G_i$ if it exists, and $\delta_i(v, c) = \perp$ if $v$ does not have a $c$-successor. It is easy to see that in a monotone graph $G$, $v \le v'$ implies $L(G, v) \subseteq L(G, v')$; in words, more continuations are available from bigger states.

Now we define the resolver $A$ by $V(R) = V(A)$, $r_0 = q_0 = \max V(G_0)$, and for any $q, q' \in V(A)$ and $c \in C$,

$$q \stackrel{c}{\to} q' \in E(A) \iff \exists i, q, q' \in V(G_i) \text{ and } q' = \delta_i(q) \neq \perp$$

$$q \stackrel{c}{\to} q' \in E(A) \iff \exists i, q \in V(G_i) \text{ and } \delta_i(q, c) = \perp \text{ and } q' = \max V(G_{i+1}).$$
Clearly, $R$ is deterministic and $R \to A$ so $R$ is a resolver; it remains to prove soundness. Take $w \in L(A)$ and let $i$ such that $w \in L(G_i)$. Let $\pi$ be the unique path from $r_0 = \max V(G_0)$ in $R$ labelled by $w$. We claim that $\pi$ remains in $\bigcup_{j \le i} V(G_j)$ and thus it can only visit at most $i$ co-Büchi transitions, so it is accepting. Assume for contradiction that $\pi$ reaches $V(G_{i+1})$.

Then it is of the form $\pi = \pi_0\pi_1\dots\pi_i\pi'$ where each $\pi_j$ is a path from $\max(V(G_j))$ in $G_j$ and $\pi'$ starts from $\max(G_{i+1})$. Let $w_0, w_1, \dots, w_i$ and $w'$ be the words labelling the paths, so that $w = w_0w_1\dots w_iw'$. Denote $q = \max(V(G_i))$. Then $w_i$ is not a label of a finite path from $q$ in $G_i$, therefore $w_iw' \notin L(G_i, q) = L(G_i)$. At the same time $w \in L(G_i)$ thus $q \stackrel{w_0\dots w_{i-1}}{\rightleftharpoons} q' \stackrel{w_i w'}{\rightleftharpoons}$ for some $q' \in V(G_i)$. But then $w_iw' \in L(G_i, q') \subseteq L(G_i, q)$, a contradiction. ◀

## 5 Conclusion

We gave a characterisation of prefix-independent $\Sigma_2^0$ objectives which are positional over arbitrary arenas as being those recognised by countable history-deterministic well-founded monotone co-Büchi automata. We moreover deduced that this class is closed by unions. We proved that, with a proper definition, mean-payoff games are positional over arbitrary arenas. Finally, we showed that any prefix-independent objective which is positional over finite arenas is finitely equivalent to an objective which is positional over arbitrary arenas.

**Open questions.** There are many open questions on positionality. Regarding $\Sigma_2^0$ objectives, the remaining step would be to lift the prefix-independence assumptions; this requires some new techniques as the proofs presented here do not immediately adapt to this case. Another open question is whether the 1-to-2 player lift holds in $\Sigma_2^0$: is there a $\Sigma_2^0$ objective which is positional on arenas controlled by Eve, but not on two player arenas?

As mentioned in the introduction, Casares [4] obtained a characterisation of positional $\omega$-regular objectives, while we characterised (prefix-independent) $\Sigma_2^0$ positional objectives. A common generalisation, which we see as a far reaching open question would be to characterise positionality within $\Delta_3^0$; hopefully establishing closure under union for this class.

Another interesting direction would be to understand finite memory for prefix-independent $\Sigma_2^0$ objectives; useful tools (such as structuration results) are already available [5]. A related (but independent) path is to develop a better understanding of (non-prefix-independent) closed objectives, which so far has remained elusive.

## References

1. Udi Boker, Orna Kupferman, and Michał Skrzypczak. How deterministic are good-for-games automata? In *FSTTCS*, volume 93 of *LIPIcs*, pages 18:1–18:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. doi:10.4230/LIPIcs.FSTTCS.2017.18.

2. Patricia Bouyer, Antonio Casares, Mickael Randour, and Pierre Vandenhove. Half-positional objectives recognized by deterministic büchi automata. In Bartek Klin, Slawomir Lasota, and Anca Muscholl, editors, *33rd International Conference on Concurrency Theory, CONCUR 2022, September 12-16, 2022, Warsaw, Poland*, volume 243 of *LIPIcs*, pages 20:1–20:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. doi:10.4230/LIPIcs.CONCUR.2022.20.

3. Lubos Brim, Jakub Chaloupka, Laurent Doyen, Raffaella Gentilini, and Jean-François Raskin. Faster algorithms for mean-payoff games. *Formal Methods Syst. Des.*, 38(2):97–118, 2011. doi:10.1007/s10703-010-0105-x.

4. Antonio Casares. *Structural properties of $\omega$-automata and strategy complexity in infinite duration games*. PhD thesis, Université de Bordeaux, 2023.

5. Antonio Casares and Pierre Ohlmann. Characterising memory in infinite games. *CoRR*, abs/2209.12044, 2022. doi:10.48550/arXiv.2209.12044.
6 Antonio Casares and Pierre Ohlmann. Half-positional $\omega$-regular languages. CoRR, abs/2401.15384, 2024. arXiv:2401.15384, doi:10.48550/arXiv.2401.15384.

7 Thomas Colcombet. Forms of determinism for automata (invited talk). In STACS, volume 14 of LIPIcs, pages 1–23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. doi:10.4230/LIPIcs.STACS.2012.1.

8 Thomas Colcombet and Damian Niwiński. On the positional determinacy of edge-labeled games. Theor. Comput. Sci., 352(1-3):190–196, 2006. doi:10.1016/j.tcs.2005.10.046.

9 Morton Davis. Infinite games of perfect information. In Advances in game theory, pages 85–101. Princeton Univ. Press, Princeton, N.J., 1964.

10 Andrzej Ehrenfeucht and Jan Mycielski. Positional strategies for mean payoff games. International Journal of Game Theory, 109(8):109–113, 1979. doi:10.1007/BF01768705.

11 E. Allen Emerson and Charanjit S. Jutla. Tree automata, mu-calculus and determinacy (extended abstract). In 32nd Annual Symposium on Foundations of Computer Science, San Juan, Puerto Rico, 1-4 October 1991, pages 368–377. IEEE Computer Society, 1991. doi:10.1109/SFCS.1991.185392.

12 Nathanaël Fijalkow, Nathalie Bertrand, Patricia Bouyer-Decitre, Romain Brenguier, Arnaud Carayol, John Fearnley, Hugo Gimbert, Florian Horn, Rasmus Ibsen-Jensen, Nicolas Markey, Benjamin Monmege, Petr Novotný, Mickael Randour, Ocan Sankur, Sylvain Schmitz, Olivier Serre, and Mateusz Skomra. Games on Graphs. Online, 2023.

13 David Gale and Frank M. Stewart. Infinite games with perfect information. In Contributions to the theory of games, volume 2 of Annals of Mathematics Studies, no. 28, pages 245–266. Princeton University Press, 1953.

14 Hugo Gimbert. Parity and exploration games on infinite graphs. In Jerzy Marcinkowski and Andrzej Tarlecki, editors, Computer Science Logic, 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 20-24, 2004, Proceedings, volume 3210 of Lecture Notes in Computer Science, pages 56–70. Springer, 2004. doi:10.1007/978-3-540-30124-0_8.

15 Hugo Gimbert and Wiesław Zielonka. Games where you can play optimally without any memory. In CONCUR, volume 3653 of Lecture Notes in Computer Science, pages 428–442. Springer, 2005. doi:10.1007/11539452_33.

16 Simon Iosti and Denis Kuperberg. Eventually safe languages. In Piotrek Hofman and Michał Skrzypczak, editors, Developments in Language Theory - 23rd International Conference, DLT 2019, Warsaw, Poland, August 5-9, 2019, Proceedings, volume 11647 of Lecture Notes in Computer Science, pages 192–205. Springer, 2019. doi:10.1007/978-3-030-24886-4_14.

17 Alexander Kechris. Classical descriptive set theory. Springer-Verlag, New York, 1995.

18 Eryk Kopczyński. Half-positional determinacy of infinite games. In ICALP, volume 4052 of Lecture Notes in Computer Science, pages 336–347. Springer, 2006. doi:10.1007/11787006_29.

19 Eryk Kopczyński. Half-positional determinacy of infinite games. PhD thesis, University of Warsaw, 2009. URL: https://www.mimuw.edu.pl/~erykk/papers/hpwc.pdf.

20 Alexander Kozachinskiy. Energy games over totally ordered groups. CoRR, abs/2205.04508, 2022. doi:10.48550/arXiv.2205.04508.

21 Denis Kuperberg and Michał Skrzypczak. On determinisation of good-for-games automata. In ICALP, volume 9135 of Lecture Notes in Computer Science, pages 299–310. Springer, 2015. doi:10.1007/978-3-662-47666-6_24.

22 Donald A. Martin. Borel determinacy. Annals of Mathematics, 102(2):363–371, 1975.

23 Andrzej W. Mostowski. Games with forbidden positions. Technical Report 78, University of Gdansk, 1991.

24 Pierre Ohlmann. Monotone graphs for solving parity and mean-payoff games. PhD thesis, Université de Paris, 2021.

25 Pierre Ohlmann. Characterizing Positionality in Games of Infinite Duration over Infinite Graphs. TheoretiCS, Volume 2, January 2023. doi:10.46298/theoretics.23.3.
54:18 Positionality in Σ₀₂ and a Completeness Result

26 Pierre Ohlmann. Positionality of mean-payoff games on infinite graphs, 2023. arXiv:2305.00347.

27 Michael O. Rabin. Decidability of second-order theories and automata on infinite trees. *Transactions of the American Mathematical Society*, 141:1–35, 1969. URL: http://www.jstor.org/stable/1995086.

28 Bader Abu Radi and Orna Kupferman. Minimization and canonization of GFG transition-based automata. *Log. Methods Comput. Sci.*, 18(3), 2022. doi:10.46298/lmcs-18(3:16)2022.

29 Lloyd S. Shapley. Stochastic games. *Proceedings of the National Academy of Sciences*, 39(10):1095–1100, 1953. doi:10.1073/pnas.39.10.1095.

30 Michał Skrzypczak. Topological extension of parity automata. *Information and Computation*, 228:16–27, 2013.

31 Philip Wolfe. The strict determinateness of certain infinite games. *Pacific Journal of Mathematics*, 5:841–847, 1955.