As observed above different nodes of the Zielonka tree may be labelled by the
same set of colours. Hence it is tempting to represent a Muller condition not with its
Zielonka tree but rather with the Zielonka DAG (Directed Acyclic Graph) where nodes
labelled by the same set of colours are identified. However with this representation
solving Muller games is again PSPACE-complete:

**Theorem 24** (Complexity of solving Muller games represented by the Zielonka DAG). *Solving Muller games where the condition is represented by a Zielonka DAG is PSPACE-complete.*

The algorithm presented in Theorem 17 runs in polynomial space for this repre-
sentation. To obtain the PSPACE-hardness we observe that in the reduction from QBF
constructed in Theorem 20, the Muller objective is of polynomial size when repre-
sented by a Zielonka DAG (but of exponential size when represented by a Zielonka
tree).

**The exact memory requirements**

The second and most interesting use of the Zielonka tree is for characterising the memory requirements.

Note that a node in the Zielonka tree $T_{\mathcal{F}}$ represents another Muller objective, over the set of colours labelling this node. For instance in Figure 2.3 the node labelled $\{1,2,3\}$ corresponds to Muller($\mathcal{F}$') with $\mathcal{F}' = \{\{2\}, \{3\}, \{1,2\}, \{1,3\}\}$.

**Definition 4** (Memory requirements for Muller objectives). Let Muller($\mathcal{F}$) be a Muller objective over the set of colours $C$. We define $m_{\mathcal{F}}$ by induction:

• if the tree consists of a single leaf, then $m_{\mathcal{F}} = 1$;

• otherwise, let $\mathcal{F}_1, \dots, \mathcal{F}_k$ be the families induced by the children of the root, there are two cases:

- if $C \in \mathcal{F}$, then $m_{\mathcal{F}}$ is the sum of $m_{\mathcal{F}_1}, \dots, m_{\mathcal{F}_k}$;

- if $C \notin \mathcal{F}$, then $m_{\mathcal{F}}$ is the maximum of $m_{\mathcal{F}_1}, \dots, m_{\mathcal{F}_k}$.

For the Muller objective represented in Figure 2.3, we have $m_{\mathcal{F}} = 3$.

**Theorem 25** (Memory requirements for Muller games). *Muller objectives Muller($\mathcal{F}$) are determined with finite memory strategies of size $m_{\mathcal{F}}$. This bound is tight: there exists a game with objective Muller($\mathcal{F}$) where Eve wins using $m_{\mathcal{F}}$ memory states but not with less.*

We will not construct the lower bound, meaning the game where Eve needs $m_{\mathcal{F}}$
memory states to win. However, we will now prove the upper bound. To this end
we revisit the recursive algorithm presented in Lemma 17 and Lemma 18. This algo-
rithm was removing colours one by one and relying on the recursive solutions. We
show that we can adapt the algorithm to follow instead the structure of the Zielonka
tree: for solving a Muller game, it is enough to recursively solve the induced Muller
games corresponding to the children of the root of the Zielonka tree. The following
lemma is an improved variant of Lemma 17. The corresponding pseudocode is given in Algorithm 2.6.

**Lemma 19** (Fixed point characterisation of the winning regions for Muller games using the Zielonka tree). Let $\mathcal{G}$ be a Muller game with objective Muller($\mathcal{F}$) such that $C \in \mathcal{F}$. Let $C_1, \dots, C_k$ be the maximal subsets of $C$ such that $C_i \notin \mathcal{F}$. We let $\mathcal{F}_1, \dots, \mathcal{F}_k$ be the corresponding induced families, and define $\mathcal{G}_i$ be the subgame of $\mathcal{G}$ induced by $V \setminus \text{Attr}_{\text{Eve}}(C_i)$ with objective Muller($\mathcal{F}_i$).

* If for all $i \in [1, k]$, we have $W_{\text{Adam}}(\mathcal{G}_i) = \emptyset$, then $W_{\text{Eve}}(\mathcal{G}) = V$.

* If there exists $i \in [1, k]$ such that $W_{\text{Adam}}(\mathcal{G}_i) \neq \emptyset$, let $\mathcal{G}'$ be the subgame of $\mathcal{G}$ induced by $V \setminus \text{Attr}_{\text{Adam}}(W_{\text{Adam}}(\mathcal{G}_i))$, then $W_{\text{Eve}}(\mathcal{G}) = W_{\text{Eve}}(\mathcal{G}')$.

We will prove the memory requirement at the same time inductively. Note that by duality, the case where $C \notin \mathcal{F}$ corresponds to the memory requirement for Adam when $C \in \mathcal{F}$:

$$m_{2C \setminus \mathcal{F}} = \max_{i \in [1, k]} m_{2C_i \setminus \mathcal{F}_i}.$$

*Proof.* We prove the first item.

For each $i \in [1, k]$, let $\sigma_i$ be an attractor strategy ensuring to reach $C_i$ from $\text{Attr}_{\text{Eve}}(C_i)$, and consider a winning strategy for Eve from $V \setminus \text{Attr}_{\text{Eve}}(C_i)$ in $\mathcal{G}_i$, it induces a strategy $\sigma'_i$ in $\mathcal{G}$. We construct a strategy $\sigma$ in $\mathcal{G}$ which will simulate the strategies above in turn; to do so it uses $[1, k]$ as top-level memory states. (We will look at more closely at the memory structure at the end of the proof.) The strategy $\sigma$ with memory $i$ simulates $\sigma_i$ from $\text{Attr}_{\text{Eve}}(C_i)$ and $\sigma'_i$ from $V \setminus \text{Attr}_{\text{Eve}}(C_i)$, and if it ever reaches a vertex in $C_i$ it updates its memory state to $i+1$ and $1$ if $i=k$. Any play consistent with $\sigma$ either updates its memory state infinitely many times, or eventually remains in $V \setminus \text{Attr}_{\text{Eve}}(C_i)$ and is eventually consistent with $\sigma'_i$. In the first case it sees a colour from each $C_i$ infinitely many times, so by definition of the $C_i$'s and since $C \in \mathcal{F}$ the play satisfies Muller($\mathcal{F}$), and in the other case since $\sigma'_i$ is winning the play satisfies Muller($\mathcal{F}$). Thus $\sigma$ is winning from $V$.

Let us now discuss how many memory states are necessary to implement the strategy $\sigma$. By induction hypothesis, each of the strategies $\sigma'_i$ uses $m_{\mathcal{F}_i}$ memory states. Using a disjoint union of the memory structures we implement $\sigma$ using $\sum_{i \in [1, k]} m_{\mathcal{F}_i}$ memory states, corresponding to the definition of $m_{\mathcal{F}}$.

We now look at the second item.

Consider a winning strategy for Adam from $W_{\text{Adam}}(\mathcal{G}_i)$ in $\mathcal{G}_i$, it induces a strategy $\tau_i$ in $\mathcal{G}$. Thanks to Lemma 10 $\tau_i$ is a winning strategy in $\mathcal{G}$. Let $\tau_a$ denote an attractor strategy from $\text{Attr}_{\text{Adam}}(W_{\text{Adam}}(\mathcal{G}_i)) \setminus W_{\text{Adam}}(\mathcal{G}_i)$. Consider now a winning strategy in the game $\mathcal{G}'$ from $W_{\text{Adam}}(\mathcal{G}')$, it induces a strategy $\tau'$ in $\mathcal{G}$. The set $V \setminus \text{Attr}_{\text{Adam}}(W_{\text{Adam}}(\mathcal{G}_i))$ may not be a trap for Eve, so we cannot conclude that $\tau'$ is a winning strategy in $\mathcal{G}$, and it indeed may not be. We construct a strategy $\tau$ in $\mathcal{G}$ as the (disjoint) union of the strategy $\tau_a$ on $\text{Attr}_{\text{Adam}}(W_{\text{Adam}}(\mathcal{G}_i)) \setminus W_{\text{Adam}}(\mathcal{G}_i)$, the strategy $\tau_i$ on $W_{\text{Adam}}(\mathcal{G}_i)$ and the strategy $\tau'$ on $W_{\text{Adam}}(\mathcal{G}')$. We argue that $\tau$ is winning from $\text{Attr}_{\text{Adam}}(W_{\text{Adam}}(\mathcal{G}_i)) \cup W_{\text{Adam}}(\mathcal{G}')$ in $\mathcal{G}$. Indeed, any play consistent
with this strategy in $\mathcal{G}$ either stays forever in $W_{\text{Adam}}(\mathcal{G}')$ hence is consistent with $\tau'$ or enters $\text{Attr}_{\text{Adam}}(W_{\text{Adam}}(\mathcal{G}_i))$, so it is eventually consistent with $\tau_i$. In both cases this implies that the play is winning. Thus we have proved that $\text{Attr}_{\text{Adam}}(W_{\text{Adam}}(\mathcal{G}_c)) \cup W_{\text{Adam}}(\mathcal{G}') \subseteq W_{\text{Adam}}(\mathcal{G})$.

We now show that $W_{\text{Eve}}(\mathcal{G}') \subseteq W_{\text{Eve}}(\mathcal{G})$, which implies the converse inclusion. Consider a winning strategy from $W_{\text{Eve}}(\mathcal{G}')$ in $\mathcal{G}'$, it induces a strategy $\sigma$ in $\mathcal{G}$. Thanks to Lemma 11 $\sigma$ is winning from $W_{\text{Eve}}(\mathcal{G}')$ in $\mathcal{G}$.

Let us now discuss how many memory states are necessary to implement the strategy $\tau$. By induction hypothesis, the strategy $\tau_i$ uses $m_{2C_i \setminus \mathcal{F}_i}$ memory states and the strategy $\tau'$ uses $\max_{j \neq i} m_{2C_j \setminus \mathcal{F}_j}$ memory states. Since $\tau$ is a disjoint union of strategies the memory can be reused so we can implement $\tau$ using $\max_{i \in [1,k]} m_{2C_i \setminus \mathcal{F}_i}$ memory states, corresponding to the definition of $m_{2C \setminus \mathcal{F}}$. $\square$

The corresponding lemma when $C \notin \mathcal{F}$ is stated below, its proof is analogous to the previous one by swapping the two players.

**Lemma 20** (Dual fixed point characterisation of the winning regions for Muller games using the Zielonka tree). Let $\mathcal{G}$ be a Muller game such that $C \notin \mathcal{F}$. Let $C_1, \dots, C_k$ be the maximal subsets of $C$ such that $C_i \in \mathcal{F}$. We let $\mathcal{F}_1, \dots, \mathcal{F}_k$ be the corresponding induced Muller objectives, and define $\mathcal{G}_i$ be the subgame of $\mathcal{G}$ induced by $V \setminus \text{Attr}_{\text{Adam}}(C_i)$ with objective Muller($\mathcal{F}_i$).

* If for all $i \in [1, k]$, we have $W_{\text{Eve}}(\mathcal{G}_i) = \emptyset$, then $W_{\text{Adam}}(\mathcal{G}) = V$.

* If there exists $i \in [1, k]$ such that $W_{\text{Eve}}(\mathcal{G}_i) \neq \emptyset$, let $\mathcal{G}'$ be the subgame of $\mathcal{G}$ induced by $V \setminus \text{Attr}_{\text{Eve}}(W_{\text{Eve}}(\mathcal{G}_i))$, then $W_{\text{Adam}}(\mathcal{G}) = W_{\text{Adam}}(\mathcal{G}')$.

## Revisiting Streett, Rabin, and parity objectives

Let us look at the Streett, Rabin, and parity objectives under the new light shed by Theorem 25. It is instructive to look at the Zielonka tree of a Rabin objective, illustrated in Figure 2.4. It has a simple recursive structure: the Zielonka tree of the Rabin objective for $d$ pairs contains $d$ copies of the Zielonka tree of the Rabin objective for $d-1$ pairs. Naturally, this implies that $m_{\text{Rabin}} = 1$, so Theorem 25 implies the half-positional determinacy result stated in Theorem 18. Note that the two proofs are very different: the proof of Theorem 25 is by induction over the Zielonka tree and can be extended to infinite games, while the proof of Theorem 16 applies only to finite games but gives a general sufficient condition for half-positional determinacy.

Recall that we defined Streett objectives using closure under union, and Rabin objectives as the complement of Streett objectives.

**Theorem 26** (Positionally determined Muller objectives). Let Muller($\mathcal{F}$) be a Muller objective.

* Muller($\mathcal{F}$) is half-positionally determined if and only if Muller($\mathcal{F}$) is a Rabin objective;
<caption>**Algorithm 2.6:** A recursive algorithm for computing the winning regions of Muller games following the Zielonka tree.</caption>

**Data:** A Muller game $\mathcal{G}$ over $C$

**Function** SolveIn($\mathcal{G}$):
    // Assumes $C \in \mathcal{F}$
    if $C = \{c\}$ then
        $\lfloor$ return $V$
    Let $C_1, \dots, C_k$ the labels of the children of the root of the Zielonka tree of
    Muller($\mathcal{F}$)
    for $i \in [1, k]$ do
        $\mathcal{G}_i \leftarrow \mathcal{G} \setminus \text{Attr}_{\text{Eve}}(C_i)$
        $W_{\text{Eve}}(\mathcal{G}_i) \leftarrow \text{SolveOut}(\mathcal{G}_i)$ // The Zielonka tree of $\mathcal{G}_i$
        is the $i$-th subtree
    if $\forall i \in [1, k], W_{\text{Adam}}(\mathcal{G}_i) = \emptyset$ then
        $\lfloor$ return $V$
    else
        Let $i$ such that $W_{\text{Adam}}(\mathcal{G}_i) \neq \emptyset$
        $\mathcal{G}' \leftarrow \mathcal{G} \setminus \text{Attr}_{\text{Adam}}(W_{\text{Adam}}(\mathcal{G}_i))$
        $\lfloor$ return SolveIn($\mathcal{G}'$) // $\mathcal{G}'$ has less vertices
    $\lfloor$ return SolveOut($\mathcal{G}$)
    $\lfloor$ // Symmetric to SolveIn, assumes $C \notin \mathcal{F}$

    if $C \in \mathcal{F}$ then
        $\lfloor$ SolveIn($\mathcal{G}$)
    else
        $\lfloor$ SolveOut($\mathcal{G}$)

<figure><img src="image_19.png" /><figcaption>Figure 2.4: The (beginning of the) Zielonka tree for Rabin with three pairs: $C = \{G_1, R_1, G_2, R_2, G_3, R_3\}$.</figcaption></figure>
• *Muller(\mathcal{F}) is positionally determined if and only if Muller(\mathcal{F}) is a parity objective.*

This theorem gives a characterisation of Rabin and parity objectives: they form the class of Muller objectives which are respectively half-positional and positional.

*Proof.* Thanks to Theorem 25 the objective Muller(\mathcal{F}) is half-positionally determined if and only if $m_{\mathcal{F}} = 1$, which is equivalent to saying that all nodes labelled $S \in \mathcal{F}$ in the Zielonka tree of \mathcal{F} have at most one child. Indeed, for such nodes the number $m$ is obtained as the sum of the numbers for the children, so there can be at most one, and conversely if this is the case then $m_{\mathcal{F}} = 1$. This characterisation of the Zielonka tree is equivalent to the complement of \mathcal{F} being closed under union:

• Assume that the complement of \mathcal{F} is closed under union and let $S \in \mathcal{F}$ be a node in the Zielonka tree of \mathcal{F}. Let $S_1, \dots, S_k$ be the children of $S$, by definition they are the maximal subsets of $S$ such that $S_i \notin \mathcal{F}$. The union $\cup_i S_i$ is a subset of $S$ and by closure under union of the complement of \mathcal{F} it is in the complement of \mathcal{F}, implying by maximality that it is one of the children, so they are all equal and $k = 1$.

• Conversely, assume that all nodes labelled $S \in \mathcal{F}$ in the Zielonka tree of \mathcal{F} have at most one child. Let $S_1, S_2 \notin \mathcal{F}$, towards contradiction assume that $S_1 \cup S_2 \in \mathcal{F}$. By definition of the Zielonka tree, if $S_1 \cup S_2$ is included into a node $S \notin \mathcal{F}$, then $S_1 \cup S_2$ is included into one of its children. Starting from the root and applying this we find a node $S \in \mathcal{F}$ such that $S_1 \cup S_2 \subseteq S$ and $S_1 \cup S_2 \not\subseteq S'$ with $S'$ the only child of $S$ (the case where $S$ does not have any children is easy and treated separately). By definition of the Zielonka tree, since $S_1, S_2 \notin \mathcal{F}$ and $S_1, S_2 \subseteq S$, then $S_1, S_2 \subseteq S'$, implying that $S_1 \cup S_2 \subseteq S'$, a contradiction.

We have proved the first equivalence: Muller(\mathcal{F}) is half-positionally determined if and only if the complement of \mathcal{F} is closed under union, which is the definition of Rabin objectives.

For the second equivalence, we already have that Muller(\mathcal{F}) is positionally determined if and only if all nodes in the Zielonka tree of \mathcal{F} have at most one child. The Zielonka tree is in this case a chain:

$$S_1 \subseteq S_2 \subseteq S_3 \subseteq S_4 \subseteq \dots \subseteq S_{2d-1} \subseteq S_{2d} \subseteq C,$$

with $S_{2i} \in \mathcal{F}$ and $S_{2i-1} \notin \mathcal{F}$. Then $X \in \mathcal{F}$ is equivalent to asking that the largest $i \in [1, d]$ such that if $X \cap S_i \neq \emptyset$ is even. Assigning priority $i$ to $S_i$ we get that $X \in \text{Muller}(\mathcal{F})$ if and only if the largest priority appearing infinitely many times in $X$ is even: this is the definition of the parity objective over the set of priorities $[1, 2d]$. Conversely, we observe that the Zielonka tree of a parity objective is indeed a chain. $\square$

## Bibliographic references

The interest in reachability objectives goes beyond automata theory and logic. The attractor computation presented in Section 2.1 is inspired by the backward induction
principle due to Zermelo [Zer13], which was used to show that well founded games (i.e. where all plays are finite) are determined. The word 'attractor' (together with 'traps' and 'subgames') first appeared in Zielonka's work on Muller games [Zie98], but without the algorithmic point of view. A naive implementation of the attractor would have a quadratic time complexity. It is difficult to give credit for the linear time algorithm since the problem being very natural it has appeared in several contexts, for instance in database theory as an inference algorithm by Beeri and Bernstein [BB79] or in the framework of computing least fixed points over transition systems by Arnold and Crubillé [AC88].

The other objectives studied in this chapter are called $\omega$-regular, let us discuss their relevance in automata theory and logic. An important application of automata theory is to make logic effective: by translating, sometimes called compiling, a logical formula into an equivalent automaton, we can solve problems such as satisfiability or model-checking by reducing them to analysing automata and in particular their underlying graph structures. In this context, the reachability objective is used for automata over finite words: the classical definition is that a run is accepting if the last state is accepting. Monadic second-order logic over finite words can be effectively translated into finite automata, marking the beginning of a close connection between logic and automata theory.

Considering logics over infinite structures led to the study of automata over infinite structures such as words and trees. The first objective to be studied in this context was Büchi objective, introduced by Büchi [Büc62]: a run is accepting if it visits infinitely many times an accepting state. Unfortunately the class of languages of infinite words recognised by deterministic Büchi automata is not closed under projection (corresponding in logic to existential quantification), said differently non-deterministic Büchi automata are strictly more expressive than deterministic ones hence not equivalent to monadic second-order logic over infinite words. Muller [Mul63] introduced the Muller objectives and attempted to prove the closure under projection for deterministic Muller automata. Alas, the proof had a flaw. The first correct proof of the result is due to McNaughton [McN66].

The correspondence between monadic second-order logic and Muller automata was extended from infinite words to infinite binary trees by Rabin [Rab69a], yielding the celebrated decidability of monadic second-order logic over infinite trees. Rabin introduced and worked with Rabin objectives; his proof is arguably very complicated and a lot of subsequent works focussed on finding the right notions and tools for better understanding his approach. Streett [Str81] suggested to use the complement of Rabin objectives, now called Streett objectives, for translating temporal logics to Streett automata. As discussed in Section 1.10, a key step was made by applying dterminacy results for games to complementation results for automata. The parity objectives appeared in this context as a (and in fact, the) subclass of Muller objectives which is positionally determined. They have been defined (with some variants) independently by several authors: Wagner [Wag79], Mostowski [Mos84] who called them 'Rabin chain', Emerson and Jutla [EJ91] who first used the name parity, and McNaughton [McN93]. The idea can be traced back to the 'difference hierarchy' by Hausdorff [Hau14]. The proof of the positionality was obtained independently by Mostowski [Mos91], Emer-
son and Jutla [EJ91], and McNaughton [McN93] (the latter proof is for finite games).
Later Walukiewicz [Wal02] gave another very elegant proof.

McNaughton [McN93] introduced the idea of solving Muller games by induction on the colours, leading to McNaughton algorithm as presented in Section 2.5. To some extent, the algorithms for solving Büchi, CoBüchi, and parity games are all special cases of McNaughton algorithm. Taking a step back in time, McNaughton already proposed the *Latest Appearance Record* (LAR) discussed in Section 2.6 for solving Muller games in his flawed attempt to solve the synthesis problem [McN65] (see Section 1.10). The LAR was later used by Gurevich and Harrington [GH82] as memory for winning strategies in Muller games. Thomas [Tho95] showed that the LAR can be used to reduce Muller games to parity games. Zielonka [Zie98] greatly contributed to the study of Muller objectives and their subclasses through his illuminating analysis of Zielonka trees. One of the many contributions of Zielonka's landmark paper [Zie98] was to follow McNaughton's approach for constructing a recursive algorithm for solving parity games, and show that it implies their positionality. We follow in Section 2.3 Zielonka's presentation of the algorithm, which is sometimes called Zielonka algorithm but more accurately McNaughton Zielonka algorithm. The characterisation result showing how Zielonka tree captures the exact memory requirements of Muller objectives is due to Dziembowski, Jurdziński, and Walukiewicz [DJW97].

The NP-completeness stated in Theorem 19 for solving Rabin games is due to Emerson and Jutla [EJ88]. The study of the complexity of solving Muller games is due to Dawar and Hunter [HD05]. The PSPACE-completeness results stated in Theorems 20 and 24 only concern two representations for Muller objectives. There are several others, which are not equally succinct. For all representations but one the PSPACE-completeness result holds; the only exception is the explicit representation where the condition is specified by listing all sets of vertices in $\mathcal{F}$. Surprisingly, solving Muller games with the explicit representation is in P as shown by Horn [Hor08].

The complexity results stated for Muller games are not optimal, as they predate the quasi-polynomial time algorithms for parity games. The state of the art for Rabin and Muller games in terms of theoretical complexity is obtained by extending these algorithms.

Theorem 16 stating that submixing prefix independent objectives are half-positionally determined over finite arenas is inspired by the fairly mixing property of Gimbert and Zielonka [GZ04]. The word ‘concave’ is used in lieu of ‘submixing’ by Kopczyński [Kop06, Kop08]. Gimbert and Zielonka [GZ05] further refined the submixing property to give a characterisation of objectives which are positionally determined over finite games (they work in the more general framework of preference relations, which includes both qualitative and quantitative objectives). We refer to Section 4.1 for general approaches for proving half-positional determinacy for quantitative objectives.
# PARITY GAMES

<figure><img src="image_20.png" /></figure>
Chapter 3

# Parity Games

JOHN FEARNLEY, NATHANAËL FIJALKOW

We will construct several algorithms for solving parity games.

• We start in Section 3.1 with an exponential time *strategy improvement algorithm*. The algorithm constructs a sequence of improving strategies until reaching an optimal strategy.

• We continue in Section 3.2 by constructing a quasi-polynomial time algorithm *attractor decomposition algorithms*, which decompose a game through a sequence of attractor computations. The first and archetypical example is McNaughton Zielonka algorithm defined in Section 2.3, which we improve here to obtain a quasi-polynomial runtime.

• We introduce in Section 3.3 the framework of *separating automata* and give a quasi-polynomial time algorithm as an instantiation of it. Separating automata formalise a family of algorithms for reducing parity games to safety games. The algorithm has mildly smaller runtime than the algorithm from the previous section.

• We proceed in Section 3.4 with the construction of a quasi-polynomial time and quasi-linear space *value iteration algorithms*, which finds an optimal strategy through the computation of a value function. This is based on the notion of universal trees.

As a conclusion Section 3.5 discusses the relationships between the different algorithms: in what sense are separating automata and value iteration algorithms equivalent through the notion of universal trees, and how does this family compare to the other two families of algorithms described above.

**Remark 9** (Positional determinacy). *We already proved in Theorem 15 that parity games are positionally determined, so in this chapter when considering a strategy we implicitly assume that it is positional.*
## 3.1 An exponential time strategy improvement algorithm

**Theorem 27 (Strategy improvement).** *There exists a strategy improvement algorithm for solving parity games in exponential time.*

One can identify from the literature at least four strategy improvement algorithms for solving parity games, all running in exponential time. Two of them are better explained as consequences of their counterparts for energy games and discounted payoff games: we first reduce parity games to the corresponding games, and apply the strategy improvement algorithm in that setting. We refer the reader to Chapter 4 for them. The other two are specific to parity games, although they are closely related to the first two algorithms.

In a nutshell: the algorithm constructs a sequence of strategies, the next one being an improvement over the current one, until reaching an optimal strategy.

**Adding the option of stopping the game.** Let $\mathcal{G}$ a parity game with $n$ vertices and priorities in $[1, d]$. Let us give Eve an extra move – that indicates that the game should stop and that she can play from any vertex of hers. So a strategy for Eve is now a function $\sigma: V_{Eve} \to E \cup \{-\}$ where $\sigma(v) = -$ indicates that Eve has chosen to stop the game, and $\sigma(v) \neq -$ should be interpreted as normal. Adam is not allowed to stop the game, so strategies for Adam remain unchanged. We say that a play ending with $-\$ is stopped.

**Evaluating a strategy.** The first question is: given a strategy $\sigma$, how to evaluate it? Let $Y = \mathbb{N}^d \cup \{\top\}$. We first explain how to evaluate plays, using a function $f: [1, d]^\omega \cup [1, d]^* \to Y$:

* Stopped plays: if $\rho \in [1, d]^*$, then $f(\rho)$ is the tuple $(x_1, x_2, \dots, x_d)$ where $x_p$ is the number of times that priority $p$ appears in $\rho$.

* Infinite plays: if $\rho \in [1, d]^\omega$, then $f(\rho)$ is $\top$.

The evaluation for finite plays can be computed using an automaton as follows: we define $\delta: Y \times [1, d] \to Y$ by

$$ \delta((x_1, x_2, \dots, x_d), p) = (x_1, x_2, \dots, x_p + 1, x_{p+1}, \dots, x_d) $$

and $\delta(\top, p) = \top$. Extending to $\delta: Y \times [1, d]^* \to Y$, we obtain the following fact.

**Fact 9.** For $\rho \in [1, d]^*$ we have $f(\rho) = \delta((0, \dots, 0), \rho)$.

We now define a total order $\leq$ on $Y$ making it a complete lattice. First, $\top$ is the greatest element. For $t, t' \in \mathbb{N}^d$, we say that $t < t'$ if and only if $p$ is the largest index such that $t_p \neq t'_p$ and

* either $p$ is even and $t_p < t'_p$,

* or $p$ is odd and $t_p > t'_p$.
Then $\le$ is the reflexive closure of $<$: we have $t \le t'$ if $t < t'$ or $t = t'$. These conditions specify which priorities Eve likes to see along a play. Given a choice, Eve would prefer to see even priorities and to avoid odd priorities, but these preferences are hierarchical: assuming that $d$ is even, Eve would like to see as many edges of priority $d$ as possible. If two plays see $d$ the same number of times, Eve prefers the play that visits the fewest vertices of priority $d-1$, and if two plays see $d$ and $d-1$ the same number of times, then Eve would like to maximise the number of times that $d-2$ is visited, and so on recursively.

We can now define the value of a strategy $\sigma$:

$$ \mathrm{val}^{\sigma}(v) = \inf_{\tau} f(\pi_{v}^{\sigma, \tau}), $$

where $\tau$ ranges over (general) strategies for Adam.

Since $Y$ is totally ordered, we can naturally cast the computation of the value function as a shortest path problem: $\mathrm{val}^{\sigma}(v)$ is the value of the shortest path<fnref n="1" /> (with respect to $Y$) in $\mathcal{G}[\sigma]$. Thus, any algorithm for the shortest path problem can be applied, such as the Bellman-Ford algorithm. In particular computing $\mathrm{val}^{\sigma}$ can be done in cubic time, and even more efficiently through a refined analysis which we do not perform here.

Recall that we say that a parity graph (without stopping option) satisfies parity from $v$ if all infinite paths from $v$ satisfy parity. Then a strategy $\sigma$ is winning from $v$ if and only if the parity graph $\mathcal{G}[\sigma]$ satisfies parity from $v$. We extend this definition to parity graphs with the stopping option: a strategy $\sigma$ satisfies parity if all infinite plays consistent with $\sigma$ satisfy parity. Crucially, this does not require anything of stopped plays. We say that a cycle is even if the maximal priority along the cycle is even, and it is odd otherwise. The characterisation of satisfying parity using cycles extends to this setting:

**Fact 10 (Strategy satisfying parity in the presence of stopped plays).** A strategy $\sigma$ satisfies parity if and only if all cycles in $\mathcal{G}[\sigma]$ are even.

The algorithm will only manipulate strategies satisfying parity.

**Improving a strategy.** We reach the last item in the construction of the algorithm: the notion of improving edges. Let $\sigma$ a strategy. Let us consider a vertex $u \in V_{\mathrm{Eve}}$, we say that $e: u \xrightarrow{p} v$ is an improving edge if

$$ \delta(\mathrm{val}^{\sigma}(v), p) > \mathrm{val}^{\sigma}(u). $$

Intuitively: according to $\mathrm{val}^{\sigma}$, playing $e$ is better than playing $\sigma(u)$. Given a strategy $\sigma$ and a set of improving edges $S$, we write $\sigma[S]$ for the strategy

$$ \sigma[S](u) = \begin{cases} e & \text{if there exists } e = u \xrightarrow{p} v \in S, \\ \sigma(u) & \text{otherwise.} \end{cases} $$

<footnote n="1">¹We use the usual albeit sometimes confusing terminology from graph algorithms: “shortest path” means of smallest value with respect to $Y$, not in number of edges.</footnote>
**The algorithm.** The algorithm starts with a specified initial strategy, which is the
strategy $\sigma_0$ where $\sigma_0(v) = -$ for all vertices $v \in V_{\text{Eve}}$. It may not hold that $\sigma_0$ satisfies
parity since $\mathscr{G}$ may contain odd cycles fully controlled by Adam. This can be checked
in linear time and the attractor to the corresponding vertices removed from the game.
After this preprocessing $\sigma_0$ indeed satisfies parity.

The pseudocode of the algorithm is given in Algorithm 3.1.

<caption>**Algorithm 3.1:** The strategy improvement algorithm for parity games.</caption>

**Data:** A parity game $\mathscr{G}$
**for** $v \in V_{\text{Eve}}$ **do**
    $\lfloor \sigma_0(v) \lfloor$ ← $-$
    $C \leftarrow \{v \in V : v$ contained in an odd cycle in $\mathscr{G}[\sigma_0]\}$
    $\mathscr{G} \leftarrow \mathscr{G} \setminus \text{Attr}_{\text{Adam}}(C)$
    **repeat**
        **for** $i = 0, 1, 2, \dots$ **do**
            Compute $\text{val}^{\sigma_i}$ and the set of improving edges
            **if** $\sigma_i$ does not have improving edges **then**
                $\lfloor \text{return } \{v \in V : \text{val}^{\sigma_i}(v) = \top\} \lfloor$
                Choose a non-empty set $S_i$ of improving edges
                $\sigma_{i+1} \leftarrow \sigma_i[S_i]$

**Proof of correctness.** As per usual for strategy improvement algorithms, the correctness depend on the following two principles:

• **Progress**: updating a strategy using improving edges is a strict improvement,

• Optimality: a strategy which does not have any improving edges is optimal.

The difficulty is that an edge being improving does not mean that it is a better move
than the current one in any context, but only according to the value function val<sup>σ</sup>, so it
is not clear that σ[S] is better than σ. Let us write σ ≤ σ' if for all vertices v we have
val<sup>σ</sup>(v) ≤ val<sup>σ'</sup>(v), and σ < σ' if additionally ¬(σ' ≤ σ).

We start by stating a very simple property of $\delta$.

**Fact 11 (Key property of $\delta$).** Let $t \in Y$ and $p_1, \dots, p_k \in [1, d]$ with $\delta(t, p_1 \dots p_k) \neq \top$. The following holds:

• $t \neq \delta(t, p_1 \dots p_k)$.

• $t < \delta(t, p_1 \dots p_k)$ if and only if $\max\{p_1, \dots, p_k\}$ is even.

• $t > \delta(t, p_1 \dots p_k)$ if and only if $\max\{p_1, \dots, p_k\}$ is odd.

The following lemma states the two important properties of $(Y, \le)$ and $\delta$.

**Lemma 21.** Let $G$ a parity graph (with no stopping option).
* If there exists $\mu: V \to Y$ such that for all vertices $u$ we have $\mu(u) \neq \top$ and for all edges $u \stackrel{p}{\to} v \in E$ we have $\mu(u) \leq \delta(\mu(v), p)$, then $G$ satisfies parity.

* If there exists $\mu: V \to Y$ such that for all vertices $v$ we have $\mu(u) \neq \top$ and for all edges $u \stackrel{p}{\to} v \in E$ we have $\mu(u) \geq \delta(\mu(v), p)$, then $G$ satisfies the complement of parity.

*Proof.* We prove the first property, the second is proved in exactly the same way. Thanks to the characterisation using cycles it is enough to show that all cycles in $G$ are even. Let us consider a cycle in $G$:

$$ \pi = v_0 \xrightarrow{p_0} v_1 \xrightarrow{p_1} v_2 \cdots v_{k-1} \xrightarrow{p_{k-1}} v_0. $$

For all $i \in [0, k-1]$ we have $\mu(v_i) \leq \delta(\mu(v_{i+1} \bmod k), p_i)$. By monotonicity of $\delta$ this implies $\mu(v_0) \leq \delta(\mu(v_0), p_{k-1} \cdots p_0)$. Thanks to Fact 11 this implies that the maximum priority in $\{p_0, \dots, p_{k-1}\}$ is even. $\square$

Let us fix a strategy $\sigma$. We let $F_V^\sigma$ denote the set of functions $\mu: V \to Y$ such that $\mu(v) = (0, \dots, 0)$ if $\sigma(v) = -$, it is a lattice when equipped with the componentwise (partial) order induced by $Y$: we say that $\mu \leq \mu'$ if for all vertices $v$ we have $\mu(v) \leq \mu'(v)$. We then define an operator $\mathcal{O}^\sigma: F_V^\sigma \to F_V^\sigma$ by

$$ \mathcal{O}^{\sigma}(\mu)(u) = \begin{cases} \min\{\delta(\mu(v), p) : u \xrightarrow{p} v \in E\} & \text{if } u \in V_{\text{Adam}}, \\ \delta(\mu(v), p) & \text{if } u \in V_{\text{Eve}} \text{ and } \sigma(u) = u \xrightarrow{p} v, \\ (0, \dots, 0) & \text{if } u \in V_{\text{Eve}} \text{ and } \sigma(u) = - \end{cases} $$

**Lemma 22.** For all $\sigma$ satisfying parity, $\text{val}^\sigma$ is a fixed point of $\mathcal{O}^\sigma$. Further, $\text{val}^\sigma(u) = \top$ if and only if all paths consistent with $\sigma$ from $u$ are infinite, and if $\text{val}^\sigma(u) < \top$, then there exists $\pi$ stopped play such that $\text{val}^\sigma(u) = f(\pi)$.

We now rely on Lemmata 21 and 22 to prove the two principles: progress and optimality.

**Lemma 23 (Progress).** Let $\sigma$ a strategy satisfying parity and $S$ a set of improving edges. We let $\sigma'$ denote $\sigma[S]$. Then $\sigma'$ satisfies parity and $\sigma < \sigma'$.

*Proof.* We first argue that $\sigma'$ satisfies parity. To this end let us consider the parity graph $\mathcal{G}[\sigma']$. We claim that for all edges $e = u \xrightarrow{p} v$ in $\mathcal{G}[\sigma']$, we have $\text{val}^\sigma(u) \leq \delta(\text{val}^\sigma(v), p)$:

* Either $e$ is an edge in $\mathcal{G}[\sigma]$ and this is because $\text{val}^\sigma$ is a fixed point of $\mathcal{O}^\sigma$,

* Or $e$ was an improving edge, in which case $\text{val}^\sigma(u) < \delta(\text{val}^\sigma(v), p)$.

Since $\sigma$ satisfies parity, for all vertices $u$ such that $\text{val}^\sigma(u) = \top$ all paths starting from $u$ satisfy parity. Let us write $G$ for the graph obtained from $\mathcal{G}[\sigma']$ by removing all such vertices. The first item of Lemma 21 implies that $G$ satisfies parity, hence $\mathcal{G}[\sigma']$ satisfies parity.
At this point we know that $\sigma'$ satisfies parity, let us show that $\text{val}^{\sigma} \le \text{val}^{\sigma'}$. Let $u_0 \in V$, let $\pi'$ consistent with $\sigma'$ from $u_0$ such that $\text{val}^{\sigma'}(u_0) = f(\pi')$, we show that $\text{val}^{\sigma}(u_0) \le f(\pi')$.

If $f(\pi') = \top$ this is clear, so let us assume that $f(\pi') < \top$, meaning $\pi'$ is finite. We reason by induction on the number of improving edges in $\pi'$. If there are none, then $\pi'$ is consistent with $\sigma$ and we are done. Let us consider the induction step: we write $\pi' = \pi'_1 \cdot u_1 \xrightarrow{p_1} v_1 \cdot \pi'_2$ with $u_1 \xrightarrow{p_1} v_1$ the first improving edge in $\pi'$. By definition of an improving edge we have $\text{val}^{\sigma}(u_1) < \delta(\text{val}^{\sigma}(v_1), p_1)$. Note that $\text{val}^{\sigma'}(v_1) = f(\pi'_2)$, by induction hypothesis this implies that $\text{val}^{\sigma}(v_1) \le f(\pi'_2)$. Since $\text{val}^{\sigma'}(u_1) = \delta(\text{val}^{\sigma'}(v_1), p_1)$, we obtain $\text{val}^{\sigma}(u_1) \le \text{val}^{\sigma'}(u_1)$. Since $\pi'_1$ does not contain any improving edges, it is consistent with $\sigma$, hence an easy induction implies that $\text{val}^{\sigma}(u_0) \le \text{val}^{\sigma'}(u_0)$.

We now show that $\text{val}^{\sigma} < \text{val}^{\sigma'}$. Let us consider $e = u \xrightarrow{p} v$ an improving edge. Using $\text{val}^{\sigma}(v) \le \text{val}^{\sigma'}(v)$ and the monotonicity of $\delta$ we obtain that $\delta(\text{val}^{\sigma}(v), p) \le \delta(\text{val}^{\sigma'}(v), p)$. Since $\text{val}^{\sigma'}$ is a fixed point of $\mathcal{O}^{\sigma'}$ we have $\text{val}^{\sigma'}(u) = \delta(\text{val}^{\sigma'}(v), p)$ and since $e$ is improving we have $\text{val}^{\sigma}(u) < \delta(\text{val}^{\sigma}(v), p)$. This implies that $\text{val}^{\sigma}(u) < \text{val}^{\sigma'}(u)$. $\square$

**Lemma 24 (Optimality).** Let $\sigma$ a strategy satisfying parity that has no improving edges, then $\sigma$ is winning from all vertices of $W_{\text{Eve}}(\mathcal{G})$.

*Proof.* The fact that $\sigma$ satisfies parity means that it is a winning strategy from all vertices $v$ such that $\text{val}^{\sigma}(v) = \top$. We now prove that Adam has a winning strategy from all vertices $v$ such that $\text{val}^{\sigma}(v) \ne \top$. We construct a strategy of Adam by

$$ \forall u \in V_{\text{Adam}}, \tau(u) \in \underset{\delta(\text{val}^{\sigma}(v), p) : u \xrightarrow{p} v \in E}{\text{argmin}} \{ \delta(\text{val}^{\sigma}(v), p) \}. $$

We argue that $\tau$ ensures the complement of parity from all vertices $v$ such that $\text{val}^{\sigma}(v) \ne \top$. Let us consider $G$ the subgraph of $\mathcal{G}[\tau]$ restricted to such vertices. We argue that for all edges $u \xrightarrow{p} v$ in $G$, we have $\text{val}^{\sigma}(u) \ge \delta(\text{val}^{\sigma}(v), p)$. Once this is proved we conclude using the second item of Lemma 21 implying that $G$ satisfies the complement of parity.

The first case is when $u \in V_{\text{Eve}}$. Let $\sigma(u) = u \xrightarrow{p'} v'$. Consider an edge $e = u \xrightarrow{p} v$, since it is not improving we have $\delta(\text{val}^{\sigma}(v), p) \le \delta(\text{val}^{\sigma}(v'), p')$. Since $\text{val}^{\sigma}$ is a fixed point of $\mathcal{O}^{\sigma}$ we have $\text{val}^{\sigma}(u) = \delta(\text{val}^{\sigma}(v'), p')$, implying the desired inequality.

The second case is when $u \in V_{\text{Adam}}$, it holds by definition of $\tau$ and because $\text{val}^{\sigma}$ is a fixed point of $\mathcal{O}^{\sigma}$. $\square$

**Complexity analysis.** One aspect of the algorithm we do not elaborate on here is the choice of improving edges at each iteration. Many possible rules for choosing this set have been studied, as for instance the greedy all-switches rule, choosing maximal improving edges. This impacts the number of iterations of the algorithm, meaning the length of the sequence $\sigma_0, \sigma_1, \dots$. It is at most exponential since it is bounded by the number of strategies (which is bounded aggressively by $m^n$). There are lower bounds
showing that the sequence can be of exponential length, which apply to different rules
for choosing sets of improving edges. Hence the overall complexity is exponential

**The other strategy improvement algorithm for parity games.** The main drawback of the algorithm we constructed is that it requires the initial strategy to be the one stopping at every vertex. This is in contrast with many practical scenarios, where the fact that the algorithm can be initialised with any strategy (hence a potentially good one) is a key factor for performances. As discussed at the beginning of this section, there are several other strategy improvement algorithms. All but one are obtained by reducing parity games to another class of games and applying a strategy improvement algorithm there. The remaining one is defined directly on parity games. The valuation of a play is a triple:

• the maximum priority *p* seen infinitely many times,

• the set of higher priorities seen before the first occurrence of *p*,

• the length of the prefix before the first occurrence of *p*.

The key benefit of this algorithm is that it can be initialised with any strategy. We do not present here a correctness proof. Let us note that the algorithm is actually closely related to the one we built here, in the sense that after adding a stopping option the two algorithms coincide. Both algorithms have exponential complexity, with exponential lower bounds on the number of iterations.

**3.2 A quasi-polynomial time attractor decomposition algorithm**

**Theorem 28** (Quasi-polynomial McNaughton Zielonka algorithm). *There exists a quasi-polynomial time algorithm for solving parity games, and more specifically of complexity $n^{O(\log n)}$.*

We revisit the exponential recursive algorithm presented in Section 2.3. We refer to Algorithm 3.2 for an equivalent presentation of this algorithm, where we make explicit all recursive calls involving the maximal priority $d$. The benefit of doing this is to make the following observation: during the $i^{th}$ recursive call for $d$, the algorithm removes from the game $\mathcal{G}$ the subset $X_i = \text{Attr}_{\text{Adam}}(W_{\text{Adam}}(\mathcal{G}_i))$. Note that $X_i$ is a trap for Eve in $\mathcal{G}$ and a subset of the winning region of Adam in $\mathcal{G}$: we say that $X_i$ is a dominion for Eve. More generally, given a game $\mathcal{G}$, a set $X$ of vertices is a *dominion* for Eve if it is a trap for Adam and a subset of the winning region of Eve.

Let $i_{\infty}$ be the final value of $i$, the sets $X_0, \dots, X_{i_{\infty}-1}$ are disjoint. The *key idea* is that this implies that at most one of them can have size more than half the total size.

To take advantage of this, we change the specification of the algorithm: the new
algorithm takes as input a parity game and two parameters $s_{\text{Eve}}$ and $s_{\text{Adam}}$. As before,
they are two mutually recursive procedures, *SolveE* and *SolveA*. At an intuitive level,
**Algorithm 3.2:** The recursive algorithm for computing the winning region of parity games.

**Data:** A parity game $\mathcal{G}$ with priorities in $[1, d]$

**Function** SolveEven($\mathcal{G}$):
    $i \leftarrow -1$
    $V_0 \leftarrow V$
    **repeat**
        $i \leftarrow i + 1$
        Let $\mathcal{G}_i$ the subgame of $\mathcal{G}$ induced by $V_i \setminus \text{Attr}_{\text{Eve}}^{\mathcal{G}_i}(d)$
        $W_{\text{Eve}}(\mathcal{G}_i) \leftarrow \text{SolveOdd}(\mathcal{G}_i)$
        $V_{i+1} \leftarrow V_i \setminus \text{Attr}_{\text{Adam}}^{\mathcal{G}_i}(W_{\text{Adam}}(\mathcal{G}_i))$
    **until** $W_{\text{Adam}}(\mathcal{G}_i) = \emptyset$
    **return** $V_i$

**Function** SolveOdd($\mathcal{G}$):
    **if** $d = 1$ **then**
        **return** $V$
    $i \leftarrow -1$
    $V_0 \leftarrow V$
    **repeat**
        $i \leftarrow i + 1$
        Let $\mathcal{G}_i$ the subgame of $\mathcal{G}$ induced by $V_i \setminus \text{Attr}_{\text{Adam}}^{\mathcal{G}_i}(d)$
        $W_{\text{Adam}}(\mathcal{G}_i) \leftarrow \text{SolveEven}(\mathcal{G}_i)$
        $V_{i+1} \leftarrow V_i \setminus \text{Attr}_{\text{Eve}}^{\mathcal{G}_i}(W_{\text{Eve}}(\mathcal{G}_i))$
    **until** $W_{\text{Eve}}(\mathcal{G}_i) = \emptyset$
    **return** $V_i$

**if** $d$ **is even then**
    **return** SolveEven($\mathcal{G}$)
**else**
    **return** SolveOdd($\mathcal{G}$)
## 3.2. A QUASI-POLYNOMIAL TIME ATTRACTOR DECOMPOSITION ALGORITHM101

the objective of SolveE($\mathcal{G}$, $s_{Eve}$, $s_{Adam}$) is to return a (non-empty whenever possible) dominion for Eve of size at most $s_{Eve}$.

We spell out the pseudocode of SolveE in Algorithm 3.3, leaving out the perfectly symmetric SolveA. The base cases are when there is only one priority, in which case Eve wins everywhere if the priority is even, and Adam wins everywhere if the priority is odd.

<caption>**Algorithm 3.3:** A recursive quasi-polynomial algorithm for computing the winning regions of parity games – the procedure SolveE.</caption>

**Data:** A parity game $\mathcal{G}$ with priorities in $[1, d]$, and $d$ even, two parameters $s_{Eve}$ and $s_{Adam}$
Let $i = 0$ and $V_0 = V$
Let $\mathcal{H}_0$ the subgame of $\mathcal{G}$ induced by $V_0$
Let $\mathcal{G}_0$ the subgame of $\mathcal{H}_0$ induced by $V_0 \setminus \text{Attr}_{\text{Eve}}^{\mathcal{H}_0}(d)$

**Function** Treat $(X_i)$:
Let $V_{i+1} = V_i \setminus \text{Attr}_{\text{Adam}}^{\mathcal{H}_i}(X_i)$
Let $\mathcal{H}_{i+1}$ the subgame of $\mathcal{H}_i$ induced by $V_{i+1}$
Let $\mathcal{G}_{i+1}$ the subgame of $\mathcal{H}_{i+1}$ induced by $V_{i+1} \setminus \text{Attr}_{\text{Eve}}^{\mathcal{H}_{i+1}}(d)$
$\quad i = i+1$

// recursive calls for small dominions
while $X_i = \text{SolveA}(\mathcal{G}_i, s_{\text{Eve}}, \lfloor s_{\text{Adam}}/2 \rfloor) \neq \emptyset$ do
    Treat $(X_i)$
// one recursive call for a large dominion
if $X_i = \text{SolveA}(\mathcal{G}_i, s_{\text{Eve}}, s_{\text{Adam}}) \neq \emptyset$ then
    Treat $(X_i)$
// recursive calls for small dominions
while $X_i = \text{SolveA}(\mathcal{G}_i, s_{\text{Eve}}, \lfloor s_{\text{Adam}}/2 \rfloor) \neq \emptyset$ do
    Treat $(X_i)$
return $V_i$

We need three simple facts about traps.

**Fact 12 (Facts about traps).**

* Let $S$ be a trap for Eve in the game $\mathcal{G}$ and $X$ a set of vertices, then $S \setminus \text{Attr}_{\text{Eve}}(X)$ is a trap for Eve in the subgame of $\mathcal{G}$ induced by $V \setminus \text{Attr}_{\text{Eve}}(X)$.

* Let $S$ be a trap for Eve in the game $\mathcal{G}$ and $X$ a set of vertices such that $S \cap X = \emptyset$, then $S \subseteq V \setminus \text{Attr}_{\text{Adam}}(X)$ and $S$ is a trap for Eve in the subgame of $\mathcal{G}$ induced by $V \setminus \text{Attr}_{\text{Adam}}(X)$.

* Let $S$ be a trap for Eve in the game $\mathcal{G}$ and $Z$ a trap for Eve in the subgame of $\mathcal{G}$ induced by $S$, then $Z$ is a trap for Eve in $\mathcal{G}$.

The following lemma implies the correctness of the algorithm.
**Lemma 25** (Correctness of the quasi-polynomial McNaughton Zielonka algorithm).

* For all dominions $S$ for Eve, if $|S| \le s_{\text{Eve}}$, then $S \subseteq \text{SolveE}(\mathcal{G}, s_{\text{Eve}}, s_{\text{Adam}})$.

* For all dominions $S$ for Adam, if $|S| \le s_{\text{Adam}}$, then $S \cap \text{SolveE}(\mathcal{G}, s_{\text{Eve}}, s_{\text{Adam}}) = \emptyset$.

Indeed, $W_{\text{Eve}}(\mathcal{G})$ and $W_{\text{Adam}}(\mathcal{G})$ are dominions for Eve and Adam in $\mathcal{G}$, so Lemma 25 implies that $\text{SolveE}(\mathcal{G}, n, n) = W_{\text{Eve}}(\mathcal{G})$.

*Proof.* The proof is by induction on the number of priorities: indeed all recursive calls to $\text{SolveA}$ are for games with one less priority. It follows that by induction hypothesis the following two properties hold, for all $i$.

* For all dominions $S$ in $\mathcal{G}_i$ for Adam, if $|S| \le s_{\text{Adam}}$, then

$$S \subseteq \text{SolveA}(\mathcal{G}_i, s_{\text{Eve}}, s_{\text{Adam}}).$$

* For all dominions $S$ in $\mathcal{G}_i$ for Eve, if $|S| \le s_{\text{Eve}}$, then

$$S \cap \text{SolveA}(\mathcal{G}_i, s_{\text{Eve}}, s_{\text{Adam}}) = \emptyset.$$

Since there will be an induction inside this induction, we refer to the induction above as the external induction, and the second one as the internal induction.

We write $i_{\infty}$ for the final value of $i$, i.e. such that $\text{SolveE}(\mathcal{G}, s_{\text{Eve}}, s_{\text{Adam}}) = V_{i_{\infty}}$. Note that the first item reads $S \subseteq V_{i_{\infty}}$.

Let $S$ be a dominion for Eve in $\mathcal{G}$ such that $|S| \le s_{\text{Eve}}$. We show by internal induction on $i$ that $S \subseteq V_i$.

For $i = 0$ this is by definition. We now assume that $S \subseteq V_i$. Recall that $\mathcal{G}_i$ is the subgame of $\mathcal{H}_i$ induced by $V_i \setminus \text{Attr}_{\text{Eve}}^{\mathcal{H}_i}(d)$. It follows from the first item of Fact 12 that $S \setminus \text{Attr}_{\text{Eve}}^{\mathcal{H}_i}(d)$ is a dominion for Eve in $\mathcal{G}_i$. Since $S \setminus \text{Attr}_{\text{Eve}}^{\mathcal{H}_i}(d)$ has size at most $s_{\text{Eve}}$, the second item of the external induction hypothesis implies that $S \setminus \text{Attr}_{\text{Eve}}^{\mathcal{H}_i}(d)$ has an empty intersection with $X_i = \text{SolveA}(\mathcal{G}_i, s_{\text{Eve}}, s_{\text{Adam}})$, implying that $S \cap X_i = \emptyset$. It follows from the second item of Fact 12 that $S \subseteq V_i \setminus \text{Attr}_{\text{Adam}}^{\mathcal{H}_i}(X_i) = V_{i+1}$. This finishes the internal induction, and implies the first item.

We now prove the second item.

Let $S$ be a (non-empty) dominion for Adam in $\mathcal{G}$ such that $|S| \le s_{\text{Adam}}$. We write $S_i = S \cap V_i$. Note that the second item reads $S_{i_{\infty}} = \emptyset$.

We first show by internal induction on $i$ that $S_i$ is a dominion for Adam in $\mathcal{H}_i$. For $i = 0$ this is by definition. We now assume that $S_i$ is a dominion for Adam in $\mathcal{H}_i$. Recall that $\mathcal{H}_{i+1}$ is the subgame of $\mathcal{H}_i$ induced by $V_{i+1} = V_i \setminus \text{Attr}_{\text{Adam}}^{\mathcal{H}_i}(X_i)$. It follows from the first item of Fact 12 applied to $S_i$ (swapping the roles of Eve and Adam) that $S_i \setminus \text{Attr}_{\text{Adam}}^{\mathcal{H}_i}(X_i) = S_{i+1}$ is a dominion for Adam in $\mathcal{H}_{i+1}$. This finishes the internal induction.

We showed that $S_i$ is a dominion for Adam in $\mathcal{H}_i$ for each $i$. To apply the external inductive hypothesis, we need to exhibit dominions for Adam in $\mathcal{G}_i$ for each $i$. We consider $\mathcal{H}'_i$ the subgame of $\mathcal{H}_i$ induced by $S_i$. Let $Z_i = W_{\text{Adam}}^{\mathcal{H}'_i}(\text{Parity} \cup \text{Reach}(d))$: in words, $Z_i$ is the subset of vertices of $S_i$ from where Adam can ensure that the parity objective is not satisfied and never to see priority $d$. We prove two properties:
• If $Z_i = \emptyset$, then $S_i = \emptyset$.

The fact that $Z_i$ is empty implies that Eve has a strategy $\sigma$ in $\mathcal{G}_i$ which from $S_i$ ensures Parity or to see priority $d$. Since $S_i$ is a dominion for Adam in $\mathcal{H}_i$, there exists a strategy $\tau$ for Adam which from $S_i$ ensures the complement of Parity and to stay in $S_i$. Playing $\sigma$ against $\tau$ yields a contradiction, since $\sigma$ ensures Parity if the play remains in $S_i$.

• $Z_i$ is a dominion for Adam in $\mathcal{G}_i$.

That $Z_i$ is a subset of the winning region of Adam in $\mathcal{G}_i$ is clear. To see that $Z_i$ is a trap for Eve in $\mathcal{G}_i$, we first note that since $S_i$ is a trap for Eve in $\mathcal{H}_i$ and $Z_i$ is a trap for Eve in $\mathcal{H}_i'$, the subgame of $\mathcal{H}_i$ induced by $S_i$, then $Z_i$ is a trap in $\mathcal{H}_i$ by the third item of Fact 12. Now, since $Z_i$ has an empty intersection with $d$, by the second item of Fact 12 this implies that $Z_i$ is a trap for Eve in the subgame of $\mathcal{H}_i$ induced by $V_i \setminus \text{Attr}_{\text{Eve}}^{\mathcal{H}_i}(d)$, which is exactly $\mathcal{G}_i$.

We are now fully equipped to prove that $S_{i\infty} = \emptyset$. Let $i_\ell$ be the value of $i$ for which the algorithm performs a recursive call for a large dominion. Since the sequence $(S_i)_i$ is non-increasing, if $S_i$ is empty for some $i$, then $S_{i\infty}$ as well.

The first while loop was exited for $i = i_\ell$, implying that

$$ \text{SolveA}(\mathcal{G}_{i_\ell}, s_{\text{Eve}}, \lfloor s_{\text{Adam}}/2 \rfloor) = \emptyset. $$

We apply the external inductive hypothesis to the dominion $Z_{i_\ell}$ for Adam in $\mathcal{G}_{i_\ell}$ for the parameter $\lfloor s_{\text{Adam}}/2 \rfloor$: if $|Z_{i_\ell}| \le \lfloor s_{\text{Adam}}/2 \rfloor$, then $Z_{i_\ell} \subseteq \text{SolveA}(\mathcal{G}_{i_\ell}, s_{\text{Eve}}, \lfloor s_{\text{Adam}}/2 \rfloor)$, implying that $Z_{i_\ell}$ is empty, which by the first property above implies that $S_{i_\ell}$ is empty, thus $S_{i_\ell}$ as well, proving the second item of Lemma 25. Excluding this case, we then analyse the situation where $|Z_{i_\ell}| > \lfloor s_{\text{Adam}}/2 \rfloor$.

We apply again the external inductive hypothesis to $Z_{i_\ell}$, but this time for the parameter $s_{\text{Adam}}$: if $|Z_{i_\ell}| \le s_{\text{Adam}}$, then $Z_{i_\ell} \subseteq X_{i_\ell}$. Since $Z_{i_\ell} \subseteq S$ and $|S| \le s_{\text{Adam}}$, the premise is satisfied, so $Z_{i_\ell} \subseteq X_{i_\ell}$. Since $Z_{i_\ell}$ is non-empty, so is $X_{i_\ell}$: the search for a large dominion was successful, and in particular $i$ is incremented at this stage, implying that $i_\ell < i_\infty$.

Consider $S_{i_\ell+1} = S_{i_\ell} \setminus \text{Attr}_{\text{Adam}}^{\mathcal{H}_{i_\ell}}(X_{i_\ell})$. In particular $S_{i_\ell+1} \subseteq S_{i_\ell} \setminus X_{i_\ell} \subseteq S_{i_\ell} \setminus Z_{i_\ell}$, so

$$ |S_{i_\ell+1}| \le |S_{i_\ell}| - |Z_{i_\ell}| \le \lfloor s_{\text{Adam}}/2 \rfloor. $$

The second while loop was exited for $i = i_\infty$, implying that

$$ \text{SolveA}(\mathcal{G}_{i_\infty}, s_{\text{Eve}}, \lfloor s_{\text{Adam}}/2 \rfloor) = \emptyset. $$

We apply the external inductive hypothesis to the dominion $Z_{i_\infty}$ for Adam in $\mathcal{G}_{i_\infty}$ for the parameter $\lfloor s_{\text{Adam}}/2 \rfloor$: if $|Z_{i_\infty}| \le \lfloor s_{\text{Adam}}/2 \rfloor$, then $Z_{i_\infty} \subseteq \text{SolveA}(\mathcal{G}_{i_\infty}, s_{\text{Eve}}, \lfloor s_{\text{Adam}}/2 \rfloor)$. The premise holds because $|S_{i_\ell+1}| \le \lfloor s_{\text{Adam}}/2 \rfloor$, the sequence $(S_i)_i$ is non-increasing, $i_\ell < i_\infty$, and $Z_{i_\infty} \subseteq S_{i_\infty}$. Hence $Z_{i_\infty}$ is empty. Thanks to the first property above for $Z_i$, this implies that $S_{i_\infty}$ is empty. This finishes the proof of the second item of Lemma 25. $\square$
We obtain an algorithm for computing the winning regions of parity games using SolveE($\mathcal{G}$,n,n), where $\mathcal{G}$ is a parity game with n vertices.

We now perform a complexity analysis. Let us write $f(m,n,d, s_{Eve}, s_{Adam})$ for the complexity of the algorithm over parity games with $m$ edges, $n$ vertices, $d$ priorities, and parameters $s_{Eve}$ and $s_{Adam}$. We have $f(m,n, 1, s_{Eve}, s_{Adam}) = O(n)$ and $f(m, 0, d, s_{Eve}, s_{Adam}) = f(m, n, d, 0, s_{Adam}) = f(m, n, d, s_{Eve}, 0) = O(1)$, with the general induction

$$f(m,n,d, s_{Eve}, s_{Adam}) \leq n \cdot f(m,n,d-1, s_{Eve}, \lfloor s_{Adam}/2 \rfloor) + f(m,n,d-1, s_{Eve}, s_{Adam}) + O(nm).$$

The term $n \cdot f(m,n,d-1, s_{Eve}, \lfloor s_{Adam}/2 \rfloor)$ corresponds to the recursive calls for small dominions, the term $f(m,n,d-1, s_{Eve}, s_{Adam})$ to the recursive call for a large dominion, and $O(nm)$ for the computation of the attractors. We obtain

$$f(m,n,d,n,n) \leq m \cdot n^{1+2\lfloor \log n \rfloor} \cdot \left( \frac{d+2\lfloor \log n \rfloor}{2\lfloor \log n \rfloor} \right).$$

which implies a quasi-polynomial upper bound of $n^{O(\log n)}$.

## 3.3 A quasi-polynomial time separating automata algorithm

### The separation framework

We describe a general approach for reducing parity games to safety games. Section 1.6 constructs reductions between objectives using automata: in the case at hand parity reduces to safety if there exists a deterministic automaton $\mathbf{A}$ over the alphabet $[1, d]$ with acceptance objective Safe and defining Parity([1, d]), meaning $L(\mathbf{A}) = \text{Parity}([1, d])$. With such an automaton in hand Lemma 6 implies the following reduction: from a parity game $\mathcal{G}$ construct the safety game $\mathcal{G} \times \mathbf{A}$ satisfying that Eve has a winning strategy in $\mathcal{G}$ from $v_0$ if and only if she has a winning strategy in $\mathcal{G} \times \mathbf{A}$ from $(v_0, q_0)$.

Unfortunately, it can be shown (using a topological argument) that there is no such automaton. The separation framework defines a (weaker) sufficient condition for the reduction above to be correct. Instead of insisting that $L(\mathbf{A}) = \text{Parity}([1, d])$, it is enough to have $W_{Eve}(\mathcal{A}, \text{Parity}[c]) = W_{Eve}(\mathcal{A}, L(\mathbf{A})[c])$. To ensure this equality we will only require that $L(\mathbf{A})$ separates winning plays from losing plays. The two key ideas are first to take advantage of the positionality of parity objectives by restricting further winning plays to positional winning plays, and second to require

$$W_{Eve}(\mathcal{A}, \text{Parity}[c]) = W_{Eve}(\mathcal{A}, L(\mathbf{A})[c])$$

not for all parity games, but only for parity games with $n$ vertices and priorities in $[1, d]$.
A deterministic safety automaton over the alphabet $[1, d]$ is given by

$$A = (Q, q_0, \delta : Q \times [1, d] \to Q, \text{Safe}[c_A]),$$

where $c_A: Q \times [1, d] \to \{\text{Win, Lose}\}$. A word $w \in [1, d]^\omega$ is accepted if the run $\rho$ over $w$ only contains transitions in Win. We use the following simplifying convention for safety automata: we distinguish a special rejecting state $\perp$ and assume that all transitions are accepting except the ones leading to $\perp$. Said differently, a word $w$ is accepted if and only if it the run over $w$ does not contain the state $\perp$. Hence we do not need to specify $c_A$: in the next two sections by an automaton we mean a deterministic safety automaton given by $A = (Q, q_0, \delta : Q \times [1, d] \to Q)$.

Let us now give a sufficient condition for the automaton $A$ to imply the correctness of the reduction from the parity game $\mathcal{G}$ to the safety game $\mathcal{G} \times A$. The condition that we define now is that the automaton $A$ is $(n, d)$-separating; it relies on the notion of parity graphs. Recall a parity graph satisfies parity from $v$ if all infinite paths from $v$ satisfy parity, and that a strategy $\sigma$ is winning from $v$ if and only if the parity graph $\mathcal{G}[\sigma]$ satisfies parity from $v$.

We say that an automaton reads, accepts, or rejects a path $\pi$ in a parity graph, which is an abuse because what the automaton reads is the induced sequence of colours $c(\pi)$.

**Definition 5** (Separating automata). An automaton $A$ is $(n, d)$-separating if the two following properties hold.

* For all parity graphs $G$ with $n$ vertices and priorities in $[1, d]$ satisfying parity, all paths from $v$ are accepted by $A$.

* All words accepted by $A$ satisfy parity.

We define the objective $\text{Parity}_{|n}$ over the set of colours $[1, d]$ as:

$$\text{Parity}_{|n} = \left\{ \pi : \begin{array}{l} \pi \text{ is a path starting in some parity graph} \\ \text{with } n \text{ vertices and priorities in } [1, d] \text{ satisfying Parity} \end{array} \right\}.$$

The definition of $(n, d)$-separating automata is illustrated in Figure 3.1 and can be summarised as $\text{Parity}_{|n} \subseteq L(A) \subseteq \text{Parity}$.

<figure><img src="image_21.png" /><figcaption>Figure 3.1: The separation problem.</figcaption></figure>

The following lemma shows the definition of separating automata in action.
**Lemma 26** (Game equivalence using separating automata). Let $\mathbf{A}$ an $(n, d)$-separating automaton. Then for all parity games $\mathcal{G} = (\mathcal{A}, \text{Parity}[\mathbf{c}])$ with $n$ vertices and priorities in $[1, d]$, we have

$$W_{\text{Eve}}(\mathcal{G}) = W_{\text{Eve}}(\mathcal{A}, L(\mathbf{A})[\mathbf{c}]).$$

*Proof.* The inclusion $W_{\text{Eve}}(\mathcal{G}) \subseteq W_{\text{Eve}}(\mathcal{A}, L(\mathbf{A})[\mathbf{c}])$ follows from positional determinacy and the inclusion $\text{Parity}_{|n} \subseteq L(\mathbf{A})$. Let $v \in W_{\text{Eve}}(\mathcal{G})$. Consider $\sigma$ a positional strategy ensuring parity from $v$ and construct the parity graph $\mathcal{G}[\sigma]$, it satisfies parity from $v$. Hence the strategy $\sigma$ also ensures $L(\mathbf{A})[\mathbf{c}]$ from $v$, so $v \in W_{\text{Eve}}(\mathcal{A}, L(\mathbf{A})[\mathbf{c}])$.

Conversely, $L(\mathbf{A}) \subseteq \text{Parity}$ implies $L(\mathbf{A})[\mathbf{c}] \subseteq \text{Parity}[\mathbf{c}]$, which in turn implies $W_{\text{Eve}}(\mathcal{A}, L(\mathbf{A})[\mathbf{c}]) \subseteq W_{\text{Eve}}(\mathcal{G})$. $\square$

The last step is to explain how to solve a game with objective $L(\mathbf{A})$, as already discussed in Section 1.6. Let $\mathcal{G} = (\mathcal{A}, L(\mathbf{A})[\mathbf{c}])$. We construct a safety game by making the synchronised product of the arena with the automaton:

$$\mathcal{G} \times \mathbf{A} = (\mathcal{A} \times \mathbf{A}, \text{Safe}[\mathbf{c}]),$$

where the safety condition ensures that the play is accepted by $\mathbf{A}$. Formally, we construct the arena $\mathcal{A} \times \mathbf{A}$ as follows. We first define the graph $G \times Q$ whose set of vertices is $V \times Q$ and set of edges is defined as follows: for every edge $u \xrightarrow{p} v \in E$ and state $q \in Q$ there is an edge from $(u, q)$ to $(v, \delta(q, p))$. The arena is $\mathcal{A} \times \mathbf{A} = (G \times Q, V_{\text{Eve}} \times Q, V_{\text{Adam}} \times Q)$. Using the convention for safety automata that the rejecting transitions are precisely those leading to the rejecting state $\perp$, the colouring function is defined by $c'(v, q) = \text{Win}$ if $q \neq \perp$, and $\text{Lose}$ otherwise.

**Fact 13** (Reduction to safety games using separating automata). *Eve has a winning strategy in $\mathcal{G}$ from $v_0$ if and only if she has a winning strategy in $\mathcal{G} \times \mathbf{A}$ from $(v_0, q_0)$.*

**Theorem 29** (Algorithm using separating automata). Let $\mathbf{A}$ an $(n, d)$-separating automaton. There exists an algorithm for solving parity games of complexity $O(m \cdot |\mathbf{A}|)$.

*Proof.* Let $\mathcal{G}$ a parity game with $n$ vertices and priorities in $[1, d]$. Thanks to Lemma 26 and Fact 13, solving $\mathcal{G}$ is equivalent to solving the safety game $\mathcal{G} \times \mathbf{A}$. Thanks to Theorem 12 solving safety games can be done in time linear in the number of edges. This yields an algorithm for solving parity games whose running time is $O(m \cdot |\mathbf{A}|)$. $\square$

In the remainder of this section we give a construction for a quasi-polynomial $(n, d)$-separating automaton.

## The original separating automaton

**Theorem 30** (The original separating automaton). There exists an $(n, d)$-separating automaton of size $n^{O(\log d)}$, inducing an algorithm for solving parity games of complexity $n^{O(\log d)}$.
**i-sequences.** The key definition used by the original separating automaton is an *i*-sequence. Let $\pi = p_1, p_2, \dots, p_t$ a finite sequence of priorities. An *i*-sequence is a set of indices that splits $\pi$ into sub-sequences. An *i*-sequence consists of exactly $2^i$ indices $1 \le j_1 < j_2 < \dots < j_{2^i} \le t$, where each $j_k$ is an integer that refers to the priority $p_{j_k}$ from the sequence $\pi$. An *i*-sequence is required to satisfy the following properties.

* **Evenness.** Each index (except possibly the last index) refers to an even priority, meaning that $p_{j_k}$ is an even priority for all $k < 2^i$.

* **Inner domination.** The subsequence of priorities between any two indices $j_k$ and $j_{k+1}$ is dominated by either $p_{j_k}$ or $p_{j_{k+1}}$. Formally, this means that whenever $j_k < l < j_{k+1}$, we have that $p_l \le p_{j_k}$ or we have that $p_l \le p_{j_{k+1}}$.

* **Outer domination.** The final subsequence between $p_{j_{2i}}$ and $p_t$ is dominated by $p_{j_{2i}}$, meaning that for all $l > j_{2i}$ we have $p_l \le p_{j_{2i}}$.

<figure><img src="image_22.png" /><figcaption>Figure 3.2: A 2-sequence.</figcaption></figure>

Figure 3.2 gives an example of a 2-sequence. The circled priorities are the indices used in the sequence. Note that there are exactly $2^2 = 4$ indices used, and that every circled priority is even. Inner domination is satisfied because every priority that is between two circled priorities is lower than one of the two end points, and outer domination is satisfied because the final circled priority 8 is larger than all the priorities that come after it.

**The relationship to parity games.** The relationship between *i*-sequences and parity games is explained by the following lemma.

**Lemma 27 (Completeness for the separating automaton).** *Suppose that Adam and Eve play positional strategies in the parity game, and let $\pi$ the resulting play.*

* If Eve wins the parity game, then there exists prefixes of $\pi$ that contain arbitrarily long *i*-sequences.

* If Adam wins the parity game, then no prefix of $\pi$ will contain a $\lceil \log n \rceil$-sequence.

*Proof.* If Eve wins the parity game then the largest priority occurring in $\pi$ infinitely often is even. Let $p$ this priority. To construct a prefix containing an *i*-sequence, we find the first index $j$ after which no priority $q > p$ is seen. We take as our indices $j_1 < j_2 < \dots < j_{2^i}$ the first $2^i$ occurrences of priority $p$ after index $j$. Evenness is trivially satisfied, and both inner and outer domination are satisfied because no priority larger than $p$ is seen after index $j$.
We prove the second claim by contradiction. Suppose that Adam wins the game, but that there is a prefix of $\pi$ that contains a $\lceil \log n \rceil$-sequence. Since the sequence indexes $2^{\lceil \log n \rceil} \ge n$ vertices of the game, it must index the same vertex $v$ twice. Thus our $i$-sequence must contain a cycle passing through $v$. Note that inner domination ensures that the largest priority on the cycle that passes through $v$ is even. However, no even cycle can be formed when Adam wins the game by playing a positional winning strategy, and so we have arrived at our contradiction. $\square$

To summarise, if Eve wins the game, then she has a strategy that ensures that arbitrarily long $i$-sequences occur, while if Adam wins the game then he has a strategy that ensures that no $\lceil \log n \rceil$-sequence occurs. So to solve the parity game, it is sufficient to determine whether Eve can force a $\lceil \log n \rceil$-sequence to occur.

**A data structure for recognising i-sequences.** We will build a quasi-polynomial sized automaton that reads a sequence of priorities, and determines whether that sequence of priorities contains a $k$-sequence. The automaton is defined by a data structure that we call a *record*, which contains information about the $i$-sequences that have been seen so far in the sequence.

A record is a sequence $b_k, b_{k-1}, \dots, b_1, b_0$, where each $b_i$ is either a priority, or the special symbol $-$.

* **Witnessing.** If $b_i \neq -$, then we have seen an $i$-sequence, and the final priority on that $i$-sequence is $b_i$.

* **Order.** If $b_i \neq -$ and $b_j \neq -$ and $j < i$, then the first index of the $j$-sequence witnessed by $b_j$ occurs after the last index of the $i$-sequence witnessed by $b_i$.

Note that, although each element $b_i$ records the existence of an $i$-sequence, the record data structure *does not* store the $2^i$ indices of this $i$-sequence, it only stores the priority of the final index of that sequence.

<figure><img src="image_23.png" /><figcaption>Figure 3.3: An example sequence that corresponds to the record $b_3 = -$.</figcaption></figure>

Figure 3.3 shows an example sequence that is consistent with the record that sets $b_3 = -$, $b_2 = 8$, $b_1 = 4$, and $b_0 = 2$. The red 2-sequence is represented by $b_2 = 8$, which is the last priority of the 2-sequence. The blue 1-sequence starts after the end of the 2-sequence, and it is represented by $b_1 = 4$. Likewise the grey 0-sequence starts after the end of the 1-sequence, and is represented by $b_0 = 2$. There is no 3-sequence in the example, and this is represented by setting $b_3 = -$.

**The update rule.** Suppose that we have a record that represents the $i$-sequences in a finite sequence of priorities, and that we then read the next priority $p$ in that sequence. We need to update the record to take this priority into account. We do this by applying
the following update rule. The update rule consists of two steps, which occur one after the other.

* **Step 1.** In this step, we find the largest index *i* such that $b_j$ is even for all $j \le i$. If $b_i = -$, or $b_i < p$, then we create a new record $b'_k, b'_{k-1}, \dots, b'_0$ by setting:

$$b'_{j} = \begin{cases} b_j & \text{if } j > i, \\ p & \text{if } j = i, \\ - & \text{if } j < i. \end{cases}$$

If there is no index *i* that satisfies the conditions, then we do not modify the record.

* **Step 2.** In step 2, we take the output of step 1, and we find the largest index *i* such that $p > b_i$ and we create a new record $b'_k, b'_{k-1}, \dots, b'_0$ by setting:

$$b'_{j} = \begin{cases} b_j & \text{if } j > i, \\ p & \text{if } j = i, \\ - & \text{if } j < i. \end{cases}$$

Again, if there is no such index *i*, then the record is not modified.

<figure><img src="image_24.png" /><figcaption>Figure 3.4: An example of a Step 1 update applied to the sequence and record from Figure 3.3</figcaption></figure>

Intuitively, Step 1 attempts to combine the *i*-sequences in the existing record into a longer *i*-sequence. Suppose that we have read the sequence shown in Figure 3.3, that we have compute the record -842, and that the next priority in the sequence is 4. Figure 3.4 shows the result of applying Step 1 to this situation. Observe that 3 is the largest index *i* such that for all $j < i$ we have that $b_j$ is even, so Step 1 will output the record 4---.

So in this circumstance, Step 1 claims that we have now seen a 3-sequence. Figure 3.4 shows why this is correct: the 0-sequence of $b_0$, the 1-sequence of $b_1$, and the 2-sequence of $b_2$ can be merged together, along with the new priority, to create a 3-sequence. Observe that inner domination in this new 3-sequence is satisfied due to the outer domination property for each of the *i*-sequences that it was constructed from. For example, the 2-sequence ends at priority 8, and the 1-sequence begins at priority 2, and we know that 8 must dominate all priorities between the 8 and the 2 because 8 is required to dominate all priorities that follow it.

Step 2 ensures that the outer domination property holds. In Figure 3.5, we show the result of applying Step 2 to the record -842 that corresponds to the sequence shown
<figure><img src="image_25.png" /><figcaption>Figure 3.5: An example of a Step 2 update applied to the sequence and record from Figure 3.3</figcaption></figure>

in Figure 3.3, when the next priority in the sequence is 9. Observe that since $9 > 8$, the outer domination property for the 2-sequence ending at 8 now fails to hold, and likewise for the sequences ending at 4 and 2. Hence, Step 2 deletes the 0-sequence and 1-sequence from the record, and updates the 2-sequence to end at 9, thereby restoring outer domination. The resulting record is $-9--$.

**Correctness.** To compute a record for a particular sequence of priorities, we start with the record $--...-$, and then process the sequence one priority at a time, using the update rule that we have described.

We must now argue that the record data structure and update rule is sufficient to decide the winner of a parity game. The following lemma states that a record will never falsely claim that an *i*-sequence has occurred.

**Lemma 28 (Correctness for the separating automaton).** Let $b_k, b_{k-1}, \dots, b_0$ be the record for a sequence of priorities $\pi$. If $b_i \neq -$, then $\pi$ contains an *i*-sequence.

*Proof.* This can be proved by induction over the components of the record. In fact we will prove the slightly stronger order property that we mentioned earlier: the *i*-sequence corresponding to $b_i$ starts after the *j* sequence corresponding to $b_j$ whenever $i < j$ and $b_i \neq -$ and $b_j \neq -$.

The base case is trivially true, since the value of $b_0$ asserts the existence of a 0-sequence, and any priority by itself is a 0-sequence. So when Step 1 or Step 2 updates $b_0$, the corresponding 0-sequence is the new priority, and this clearly starts after all other *i*-sequences in the record.

For the inductive step, we must prove that the two steps of the update rule are correct.

* For Step 1 updates, we can use the inductive hypothesis to argue that, for each $j < i$, the *j*-sequence corresponding to $b_j$ exists, and that they appear in order in the sequence, and that it ends before the sequence corresponding to $b_{j-1}$ starts. Furthermore, the outer domination property the *j*-sequence ensures that all priorities between the end of the *j*-sequence and the start of the $(j-1)$-sequence are dominated by the last priority in the *j*-sequence, which must be even according to the definition of a Step 1 update. Hence, we can combine all of the *j*-sequences with $j < i$ together, along with the new priority, to create an *i*-sequence. This new *i*-sequence starts at exactly the same point as the sequence corresponding to $b_{i-1}$, and so the order property still holds.
* For Step 2 updates, we only need to argue that the value of $b_i'$ correspond to an *i* sequence. This can be constructed as we showed in Figure 3.5: take the *i*-sequence that corresponds to $b_i$, and replace the final priority with the new pri-ority. Observe that the final priority of an *i*-sequence is permitted to be odd, and so this new sequence satisfies all of the requirements of an *i*-sequence. Fur-thermore, the starting point of this sequence has not changed, and so the order property is preserved.

☐

As a consequence of the lemma above, if Adam has a strategy to ensure that no *k*-sequence occurs in the game, then Adam has a strategy to ensure that the $b_k$ component of the record is never set so that $b_k \neq -$.

It can be shown that the other direction is also true: if an *i*-sequence has occurred, then there will be some index $j \ge i$ such that $b_j \neq -$. However, the proof is somewhat tedious, and this statement is actually stronger than what we need. To argue that the record can determine the winner of a parity game, the following weaker lemma suffices.

**Lemma 29 (Weaker correctness for the separating automaton).** Let $\pi$ an infinite play that is winning for Eve. For all $k$, there exists a prefix of $\pi$ such that $b_k \neq -$.

*Proof.* Let $p$ the largest even priority that is seen infinitely often, and let $j$ be the first index after which no priority larger than $p$ is visited. We argue that after index $j$ has been reached, the record will eventually set $b_i \neq -$ for all $i$.

To see why, observe that after index $j$ has been reached, Step 2 cannot replace any component $b_j$ with $b_j = p$, since Step 2 can only overwrite the priority in $b_j$ when the new priority $p'$ satisfies $p' > b_j$, but no priority $p' > p$ is seen after index $j$.

On the other hand, Step 1 will always be triggered whenever we visit the priority $p$. Step 1 will always set some component of the record to $p$, and as we have observed this cannot be overwritten by Step 2. Moreover, since $p$ is even, repeated application of Step 1 will build a longer and longer *i*-sequences whose outer domination priority is $p$. Thus, after we have made $2^k$ visits to $p$, we will have set $b_k = p \neq -$, if we have not done so already. ☐

Hence, if Eve wins the parity game, then she has a strategy to eventually ensure that $b_k \neq -$. Combining the two lemmas above, with Lemma 27 gives the following corollary.

**Corollary 4 (Correctness of the reduction for the separating automaton).** Suppose that we monitor the play of a parity game with a record $b_{\lfloor \log n \rfloor}, \dots, b_0$. Eve has a strategy that ensures $b_{\lfloor \log n \rfloor} \neq -$ if and only if Eve wins the parity game.

**The size of the automaton.** The record data structure and update rule can be encoded as a deterministic finite automaton that reads the play. Each state of the automaton is associated with some configuration of $b_{\lfloor \log n \rfloor}, \dots, b_0$, and the transitions of the automaton are defined by the update rule.

This automaton has quasi-polynomial size. The number of states used in the automaton is the number of possible configurations of $b_{\lfloor \log n \rfloor}, \dots, b_0$. Each $b_i$ can be one
of the *d* priorities in the game, or the symbol `-`, and so there are *d* + 1 possible values that it can take. Moreover there are $\log n + 1$ components of the record, so the total number of configurations is at most $(d+1)^{\log n+1} = n^{O(\log d)}$.

## 3.4 A quasi-polynomial time value iteration algorithm

**Theorem 31 (Value iteration).** *There exists a value iteration algorithm for solving parity games in time*

$$O\left(nm \cdot \log(n) \log(d) \cdot n^{2.45+\log_2\left(1+\frac{d/2-1}{\log_2(n)}\right)}\right),$$

which is quasi-polynomial in general and polynomial if $d = O(\log_2(n))$. The space complexity of the algorithm is quasi-linear, and more precisely $O(m + n \log_2(d))$.

The presentation follows the introduction to value iteration algorithms given in Section 1.9, although it does not technically rely on it. Let $\mathcal{G} = (\mathcal{A}, \text{Parity}[c])$ a parity game with *n* vertices and priorities in $[1, d]$, and without loss of generality *d* is even.

The first step is to define a notion of value function $\text{val}^{\mathcal{G}}: V \to Y$ with $(Y, \leq)$ a lattice satisfying the characterisation principle: for all vertices $u$ we have that Eve wins from $u$ if and only if $\text{val}^{\mathcal{G}}(u) \neq \top$, where $\top$ is the largest element in $Y$. The goal of the algorithm is to compute $\text{val}^{\mathcal{G}}$, from which we then easily obtain the winning region thanks to the characterisation principle.

We let $F_V$ be the lattice of functions $V \to Y$ equipped with the componentwise order induced by $Y$. We are looking for a monotonic function $\delta: Y \times [1, d] \to Y$ inducing the operator $\mathcal{O}: F_V \to F_V$ defined by:

$$\mathcal{O}(\mu)(u) = \begin{cases} \min \left\{ \delta(\mu(v), p) : u \xrightarrow{p} v \in E \right\} & \text{if } u \in V_{\text{Eve}}, \\ \max \left\{ \delta(\mu(v), p) : u \xrightarrow{p} v \in E \right\} & \text{if } u \in V_{\text{Adam}}, \end{cases}$$

such that $\text{val}^{\mathcal{G}}$ is the least fixed point of $\mathcal{O}$. The algorithm will then simply use Kleene's fixed point theorem (Theorem 4) to compute $\text{val}^{\mathcal{G}}$ by iterating the operator $\mathcal{O}$.

Let us look at this question using the notion of progress measures, which are pre-fixed points of $\mathcal{O}$, meaning $\mu$ such that $\mathcal{O}(\mu) \leq \mu$. Since the least fixed point of $\mathcal{O}$ is also its least pre-fixed point, an equivalent formulation of the characterisation principle above reads: for all vertices $u$ we have that Eve wins from $u$ if and only if there exists a progress measure $\mu$ such that $\mu(u) \neq \top$.

To summarise this discussion, we are looking for a lattice $(Y, \leq)$ and a monotonic function $\delta: Y \times [1, d] \to Y$ such that for all parity games $\mathcal{G}$ with *n* vertices and priorities in $[1, d]$, for all vertices $u$ we have that Eve wins from $u$ if and only if there exists a progress measure $\mu$ such that $\mu(u) \neq \top$. Our next step is to show how the notion of universal trees provides a class of solutions to this problem.
Universal trees

The trees we consider have three properties: they are rooted, every leaf has the same
depth, and the children of a node are totally ordered. Formally, a tree of height 0 is a
leaf, and a tree t of height h + 1 is an ordered list [t₁, ..., tₖ] of subtrees each of height h.

We consider two parameters for trees: the height, and the size which is defined to
be the number of leaves.

<figure><img src="image_26.png" /><figcaption>Figure 3.6: On the left, a tree of height h = 2, which is the smallest (5,2)-universal tree: it has size 11 (meaning it has 11 leaves). On the right, a tree of size 5 and one possible embedding into the universal tree.</figcaption></figure>

We say that a tree *t* embeds into another tree *T* if:

• either both are leaves,

* or let $t = [t_1, \dots, t_k]$ and $T = [T_1, \dots, T_{k'}]$, there exist $i_1 < \dots < i_k$ such that for all $j \in [1, k]$ we have that $t_j$ embeds into $T_{i_j}$.

**Definition 6 (Universal trees).** A tree is (n,h)-universal if it embeds all trees of size n and height h.

We refer to Figure 3.6 for an example of a (5,2)-universal tree. A first example of an (n,h)-universal tree is the tree where each node has degree n: formally we define it recursively by T<sub>n,0</sub> is a leaf, and T<sub>n,h+1</sub> = [T<sub>n,h</sub>,...,T<sub>n,h</sub>]. It has size n<sup>h</sup>. <sup>n copies</sup>

A quasi-polynomial universal tree

We present an inductive construction of a quasi-polynomial universal tree.

**Theorem 32 (Construction of a quasi-polynomial universal tree).** There exists an (n,h)-universal tree with size f(n,h) satisfying the following:

$$
f(n,h) = f(n,h-1) + f(\lfloor n/2 \rfloor, h) + f(n-1-\lfloor n/2 \rfloor, h),
$$

$$
f(n,0) = 1,
$$

$$
f(0,h) = 0.
$$

An upper bound is given by

$$
f(n,h) \le n \cdot \binom{h-1 + \lfloor \log_2(n) \rfloor}{\lfloor \log_2(n) \rfloor}.
$$
This is also bounded from above by $n^{2.45+\log_2(1+\frac{h-1}{\log_2(n)})}$, which is quasi-polynomial in $n$ and $h$ in general, and polynomial if $h = O(\log_2(n))$.

*Proof.* To construct the $(n, h)$-universal tree $T$, let:

* $T_{\text{left}}$ be a $(\lfloor n/2 \rfloor, h)$-universal tree,

* $T_{\text{middle}}$ be a $(n, h-1)$-universal tree,

* $T_{\text{right}}$ be a $(n-1-\lfloor n/2 \rfloor, h)$-universal tree.

The intuitive construction of $T$ is as follows: we merge the roots of $T_{\text{left}}$ and $T_{\text{right}}$ and insert in-between them a child of the root to which is attached $T_{\text{middle}}$. Formally, let $T_{\text{left}} = [T_{\text{left}}^1, \dots, T_{\text{left}}^k]$ and $T_{\text{right}} = [T_{\text{right}}^1, \dots, T_{\text{right}}^{k'}]$, we define $T$ as

$$[T_{\text{left}}^1, \dots, T_{\text{left}}^k, T_{\text{middle}}, T_{\text{right}}^1, \dots, T_{\text{right}}^{k'}].$$

The construction is illustrated in Figure 3.7.

<figure><img src="image_27.png" /><figcaption>Figure 3.7: The inductive construction.</figcaption></figure>

We argue that $T$ is $(n, h)$-universal. Consider a tree $t = [t_1, \dots, t_k]$ with $n$ leaves. The question is where to cut, i.e. which subtree of $t$ gets mapped to $T_{\text{middle}}$. Let $n(t_i)$ be the number of leaves in $t_i$. Since $t$ has $n$ leaves, we have $n(t_1) + \dots + n(t_k) = n$. There exists a unique $p \in [1, k]$ such that $n(t_1) + \dots + n(t_{p-1}) \le \lfloor n/2 \rfloor$ and $n(t_1) + \dots + n(t_p) > \lfloor n/2 \rfloor$. The choice of $p$ implies that $n(t_{p+1}) + \dots + n(t_k) \le n - 1 - \lfloor n/2 \rfloor$. To embed $t$ into $T$, we proceed as follows:

* the tree $[t_1, \dots, t_{p-1}]$ has at most $\lfloor n/2 \rfloor$ leaves, so it embeds into $T_{\text{left}}$ by induction hypothesis;

* the tree $t_p$ has height $h-1$ and at most $n$ leaves, so it embeds into $T_{\text{middle}}$ by induction hypothesis;

* the tree $[t_{p+1}, \dots, t_k]$ has at most $n-1-\lfloor n/2 \rfloor$ leaves, so it embeds into $T_{\text{right}}$ by induction hypothesis.
☐

The construction given in the proof yields the smallest (5,2)-universal tree illustrated in Figure 3.6.

## Ordering the leaves

Let us consider a tree $t$ of height $h$, and write $d = 2h$. A leaf is given by a list of directions that we define now. For technical convenience that will manifest itself later, the list of directions is indexed by odd numbers $p \in [1, d]$ downwards: for example for $d = 10$ a leaf is $(D_9, D_7, D_5, D_3, D_1)$.

We write $Y_t$ for the set of leaves of $t$ and $\le$ for the lexicographic order on $Y_t$. Note that its interpretation on the tree is: for two leaves $\ell, \ell'$, we have $\ell \le \ell'$ if and only if $\ell$ is to the left of $\ell'$. The strict version of $\le$ is $<$.

We introduce a set of relations $\triangleleft_p$ over $Y_t$ for each $p \in [1, d]$. For a leaf $\ell = (D_{d-1}, \dots, D_1)$ we write $\ell_{\ge p}$ for the tuple $(D_{d-1}, \dots, D_p)$, which we call the $p$-truncated branch of $\ell$.

* For $p$ odd, we say that $\ell \triangleleft_p \ell'$ if $\ell_{\ge p} < \ell'_{\ge p}$.

* For $p$ even, we say that $\ell \triangleleft_p \ell'$ if $\ell_{\ge p} \le \ell'_{\ge p}$.

To interpret $\triangleleft_p$ on the tree, we label the levels by priorities from bottom to top as in Figure 3.6. Then $\ell \triangleleft_p \ell'$ if and only if the $p$-truncated branch of $\ell$ is to the left of the $p$-truncated branch of $\ell'$, strictly if $p$ is odd, and non-strictly if $p$ is even.

<figure><img src="image_28.png" /><figcaption>Figure 3.8: Illustration of the relations $\triangleleft_p$.</figcaption></figure>

We refer to Figure 3.8 for some examples. In red, we see that $\ell_1 \triangleleft_3 \ell_2$.

$$ \ell_2 \triangleleft_1 \ell_3 ; \quad \ell_2 \triangleleft_2 \ell_3 ; \quad \ell_3 \triangleleft_2 \ell_2 ; \quad \ell_1 \triangleleft_3 \ell_2 ; \quad \ell_1 \triangleleft_2 \ell_2. $$

**Lemma 30 (Properties of the tree orders).** The relations $\triangleleft_p$ for $p \in [1, d]$ induced by a tree $t$ satisfy the following properties:

* $\triangleleft_d$ is the full relation: for all $b, b'$ we have $b \triangleleft_d b'$;

* if $\ell \triangleleft_p \ell'$ and $\ell' \triangleleft_q \ell''$ then $\ell \triangleleft_{\max(p,q)} \ell''$;
* the relation $\triangleleft_p$ is non-reflexive if $p$ is odd;

* the relation $\triangleleft_1$ is total;

* for $p < d$ even we have $\ell \triangleleft_p \ell'$ if and only if $\neg(\ell' \triangleleft_{p+1} \ell)$.

The following observation rephrases the notion of embeddings between trees using the ordering on leaves.

**Fact 14** (Equivalence between embedding and orders). Let $t, T$ be two trees of height $h$ and $d = 2h$. Then $t$ embeds into $T$ if and only if there exists a function $\mu: Y_t \to Y_T$ such that for all leaves $\ell, \ell'$, for all $p \in [1, d]$:

$$ \ell \triangleleft_p \ell' \implies \mu(\ell) \triangleleft_p^T \mu(\ell'). $$

## Progress measures

We explain how a tree $t$ induces both a lattice $(Y_t, \leq)$ and a monotonic function $\delta_t$: $Y_t \times [1, d] \to Y_t$. The set $Y_t$ is the set of leaves of $t$ augmented with a new element $\top$, and $\leq$ is the lexicographic order on leaves with $\top$ as greatest element. For each $p \in [1, d]$ and $\ell \in Y_t$ we extend $\triangleleft_p$ with $\ell \triangleleft_p \top$. We then define $\delta_t: Y_t \times [1, d] \to Y_t$ by

$$ \delta_t(\ell, p) = \min_{\leq} \{\ell' : \ell \triangleleft_p \ell'\}. $$

This in turn induces a monotonic operator $\mathcal{O}_t: F_V \to F_V$ defined by:

$$ \mathcal{O}_t(\mu)(u) = \begin{cases} \min\{\delta_t(\mu(v), p) : u \xrightarrow{p} v \in E\} & \text{if } u \in V_{\text{Eve}}, \\ \max\{\delta_t(\mu(v), p) : u \xrightarrow{p} v \in E\} & \text{if } u \in V_{\text{Adam}}, \end{cases} $$

Let $\mathcal{G}$ be a parity game, a progress measure is a function $\mu: V \to Y_t$ which is a pre-fixed point: $\mathcal{O}_t(\mu) \leq \mu$. Unfolding the definitions, this means that for all vertices $u$, we have

$$ \exists u \xrightarrow{p} v \in E, \quad \delta_t(\mu(v), p) \leq \mu(u) \quad \text{if } u \in V_{\text{Eve}}, $$

$$ \forall u \xrightarrow{p} v \in E, \quad \delta_t(\mu(v), p) \leq \mu(u) \quad \text{if } u \in V_{\text{Adam}}. $$

The definition of $\delta_t$ further simplifies it to: for all vertices $u$, we have

$$ \exists u \xrightarrow{p} v \in E, \quad \mu(v) \triangleleft_p \mu(u) \quad \text{if } u \in V_{\text{Eve}}, $$

$$ \forall u \xrightarrow{p} v \in E, \quad \mu(v) \triangleleft_p \mu(u) \quad \text{if } u \in V_{\text{Adam}}. $$

The following theorem is our first and main step towards proving the characterization principle.

**Theorem 33** (Fundamental theorem for progress measures). Let $\mathcal{G}$ be a parity game and $v$ a vertex. Then Eve wins from $v$ if and only if there exists a tree $t$ and a progress measure $\mu: V \to Y_t$ such that $\mu(v) \neq \top$.
In order to prove Theorem 33, we first consider the case of parity graphs. A progress measure in a parity graph is a function $\mu: V \to Y_t$ such that for all edges $u \stackrel{p}{\to} v \in E$ we have $\mu(v) \triangleleft_p \mu(u)$.

Recall that a graph satisfies parity from $v$ if all infinite paths from $v$ satisfy parity. This is equivalent to asking whether all cycles reachable from $v$ are even, meaning the maximal priority appearing in the cycle is even.

**Lemma 31** (Fundamental lemma for progress measures over graphs). Let $G$ be a parity graph and $v$ a vertex. Then $G$ satisfies parity from $v$ if and only if there exists a tree $t$ and a progress measure $\mu: V \to Y_t$ such that $\mu(v) \neq \top$.

*Proof.* Let us assume that there exists a tree $t$ and a progress measure $\mu: V \to Y_t$ such that $\mu(v) \neq \top$ and for all edges $u \stackrel{p}{\to} v \in E$ we have $\mu(v) \triangleleft_p \mu(u)$. To show that $G$ satisfies parity from $v$ we show that any cycle reachable from $v$ is even. Let us consider such a cycle:

$$v_1 \stackrel{p_1}{\to} v_2 \stackrel{p_2}{\to} v_3 \cdots v_k \stackrel{p_k}{\to} v_1.$$

Since the cycle is reachable from $v$ and $\mu(v) \neq \top$, this implies that $\mu(v_i) \neq \bot$ for $i \in [1, k]$. Let us assume towards contradiction that its maximal priority is odd, and without loss of generality it is $p_1$. Applying our hypothesis to each edge of the cycle we have

$$\mu(v_1) \triangleleft_{p_1} \mu(v_k) \triangleleft_{p_{k-1}} \cdots \triangleleft_{p_2} \mu(v_k) \triangleleft_{p_1} \mu(v_1).$$

The second item of Lemma 30 implies that $\mu(v_1) \triangleleft_{p_1} \mu(v_1)$, which contradicts the third item since $\triangleleft_{p_1}$ is non-reflexive given that $p_1$ is odd.

Let us now prove the converse implication. We prove the following property by induction on the number of priorities: for all graphs satisfying parity (without the usual assumption that every vertex has an outgoing edge), there exists a tree $t$ and a progress measure $\mu: V \to Y_t$ such that $\mu(v) \neq \top$ for all vertices $v \in V$.

Let $G$ a graph satisfying parity. Without loss of generality the largest priority $d$ in the graph is even. Let us define $G'$ the graph obtained from $G$ by removing all edges with priority $d$. We consider its decomposition in strongly connected components: let $G_1, \dots, G_k$ denote the strongly connected components of $G'$, numbered so that for any edge $u \to v \in E(G')$, if $u \in V(G_i)$ then $v \in V(G_j)$ for $j \ge i$. A stronger property holds for edges $u \stackrel{d-1}{\to} v \in E(G')$: if $u \in V(G_i)$ then $v \in V(G_j)$ for $j > i$. Indeed, if $v \in V(G_i)$ then we could form a cycle in $G'$ whose largest priority is $d-1$, a contradiction. Hence each $G_i$ has priorities in $[1, d-2]$, and being a subgraph of $G$ it satisfies parity. By induction hypothesis, there exists a tree $t_i$ and a progress measure $\mu_i: V(G_i) \to Y_{t_i}$ such that $\mu_i(v) \neq \top$ for all vertices $v \in V(G_i)$.

Let us define $t = [t_1, \dots, t_k]$, and the function $\mu: V(G) \to Y_t$ by $\mu(v) = \mu_i(v)$ if $v \in V(G_i)$. We claim that $\mu$ is a progress measure: let us consider an edge $u \stackrel{p}{\to} v \in E(G)$, then

* if $p = d$, then $\mu(v) \triangleleft_d \mu(u)$ because $\triangleleft_d$ is the full relation;

* if $p = d-1$, then $\mu(v) \triangleleft_{d-1} \mu(u)$ because $u \in V(G_i)$ and $v \in V(G_j)$ for $j > i$;
* if $p < d-1$, then $\mu(v) \triangleleft_p \mu(u)$. Indeed $u \in V(G_i)$ and $v \in V(G_j)$ for $j \ge i$, so either $j = i$ and this follows from the fact that $\mu_i$ is a progress measure, or $j > i$ and we have $\mu(v) \triangleleft_{d-1} \mu(u)$ so a fortiori $\mu(v) \triangleleft_p \mu(u)$.

☐

We can now prove Theorem 33.

*Proof.* Assume that Eve wins from $v$ and let $\sigma$ be a positional strategy. The parity graph $\mathcal{G}[\sigma]$ satisfies parity from $v$, so thanks to Lemma 31 there exists a tree $t$ and a function $\mu : V \to Y_t$ such that $\mu(v) \neq \top$ and for all edges $u \xrightarrow{p} v \in E$ we have $\mu(v) \triangleleft_p \mu(u)$. We remark that $\mu : V \to Y_t$ is actually a progress measure: the condition for $u \in V_{\text{Eve}}$ is ensured by the edge $\sigma(u)$, and the condition for $v \in V_{\text{Adam}}$ by assumption on $\mu$.

Conversely, assume that there exists a tree $t$ and a progress measure $\mu : V \to Y_t$. It induces a positional strategy defined by $\sigma(u) = u \xrightarrow{p} v$ such that $\mu(v) \triangleleft_p \mu(u)$. We argue that $\sigma$ is a winning strategy from any vertex $v$ such that $\mu(v) \neq \top$. This is a consequence of Lemma 31 for the parity graph $\mathcal{G}[\sigma]$. ☐

Theorem 33 is very close to the characterisation principle we are after, the only
difference being that the lattice $(Y_t, \le)$ depends on an existentially quantified tree $t$.
This is where we use universal trees:

**Corollary 5 (Fundamental corollary for progress measures).** Let $\mathcal{G}$ be a parity game with $n$ vertices and priorities in $[1, d]$, and $v$ a vertex. Let $T$ be a $(n, d/2)$-universal tree. Then Eve wins from $v$ if and only if there exists a progress measure $\mu : V \to Y_T$ such that $\mu(v) \neq \top$.

*Proof.* Assume that Eve wins from $v$, thanks to Theorem 33 there exists a tree $t$ and a progress measure $\mu : V \to Y_t$ such that $\mu(v) \neq \top$. Since $T$ is $(n, d/2)$-universal and $t$ has at most $n$ leaves, $t$ embeds into $T$, which thanks to Fact 14 implies that there exists $\mu' : Y_t \to Y_T$ respecting the relations $\triangleleft$. We extend it to $\mu' : Y_t \to Y_T$ by $\mu'(\bot) = \bot$. Then the composition $\mu' \circ \mu : V \to Y_T$ is a progress measure such that $(\mu' \circ \mu)(v) \neq \bot$.

The converse implication is a direct consequence of Theorem 33. ☐

We have thus proved that the characterisation principle holds for any $(n, d/2)$-universal tree.

**The algorithm**

Let us fix $T$ an $(n, d/2)$-universal tree. It induces both a lattice $(Y_T, \le)$ and a monotonic function $\delta_T : Y_T \times [1, d] \to Y_T$, which in turn induces a monotonic operator $\mathcal{O}_T : F_V \to F_V$. Since $T$ is fixed we do not specify the subscript $T$ for all these objects.

The last step is to construct an algorithm returning the minimal progress measure relying on Kleene's fixed point theorem (stated as Theorem 4). The generic algorithm is explained in Section 1.9, let us instantiate it here.
<figure><img src="image_29.png" /><figcaption>Figure 3.9: The operator $\mathcal{O}$ in action: the updated value for $u$ is the minimal leaf (meaning the leftmost leaf) which satisfies $\mu(v) \triangleleft_1 \ell$ and $\mu(v') \triangleleft_2 \ell$.</figcaption></figure>

We say that an edge $u \xrightarrow{p} v$ is *incorrect* if $\neg(\mu(v) \triangleleft_p \mu(u))$, and a vertex $u$ is *incorrect* if either $u \in V_{\text{Eve}}$ and all outgoing edges are incorrect or $u \in V_{\text{Adam}}$ and there exists an incorrect outgoing edge.

The pseudocode for the algorithm is given in Algorithm 3.4, where we let $\ell_{\min}$ denote the minimal leaf in $T$.

**Algorithm 3.4:** The value iteration algorithm.

**Data:** A parity game with $n$ vertices priorities in $[1, d]$ and a $(n, d/2)$-universal tree $T$.

**for** $v \in V$ **do**
$\lfloor \mu(v) \lfloor \ell_{\min}$

**repeat**
$\lceil \mu \rceil \leftarrow \mathcal{O}(\mu)$

**until** $\mu = \mathcal{O}(\mu)$

**return** $\mu$

**Theorem 34 (Generic value iteration algorithm).** For all $(n, d/2)$-universal tree $T$, for all parity games $\mathcal{G}$ with $n$ vertices and priorities in $[1, d]$, the value iteration algorithm over the tree $T$ returns the minimal progress measure $\mu$ for $\mathcal{G}$ over $T$.

Thanks to Corollary 5, the minimal progress measure yields a solution for parity games: Eve wins from $v$ if and only if $\mu(v) \neq \top$.

## Complexity analysis

The number of times the operator $\mathcal{O}$ is used is bounded by the number of leaves of $T$, which we write $|T|$, implying that the total number of iterations is bounded by $n \cdot |T|$. To determine the overall complexity we need to discuss two aspects of the algorithm:

* the data structure and in particular the choice of the vertex $u$ in the loop;
• the computation of $\mathcal{O}$ and in particular the encoding of leaves of $T$.

Recall that a vertex $u \in V_{\text{Eve}}$ is incorrect if and only if all its outgoing edges are incorrect, and a vertex $u \in V_{\text{Adam}}$ is incorrect if and only if it has an incorrect outgoing edge. Hence checking whether a vertex $u$ is incorrect requires considering all of its outgoing edges $u \xrightarrow{p} v$ and checking whether $\mu(v) \triangleleft_p \mu(u)$. Let us write $\Delta$ for the complexity of checking whether $\mu(v) \triangleleft_p \mu(u)$. Hence checking whether $u$ is incorrect costs $O(|\text{In}^{-1}(u)| \cdot \Delta)$, where $|\text{In}^{-1}(u)|$ is the number of outgoing edges of $u$. A naive implementation of Algorithm 3.4 would in each repeat loop go through every vertex $u$ to check whether it is incorrect. This would incur the following cost for a single iteration

$$ \sum_{u \in V} O(|\text{In}^{-1}(u)| \cdot \Delta) = O(n \cdot m \cdot \Delta). $$

Thus the overall running time of the algorithm would be

$$ O((n \cdot m \cdot \Delta) \cdot (n \cdot |T|)) = O(n^2 \cdot m \cdot \Delta \cdot |T|). $$

Typically $\Delta$ is small (we will see that for a well chosen universal tree $T$ it is polylogarithmic in $n$ and $d$), and $T$ is the dominating factor (quasi-polynomial in $n$ and $d$ thanks to Theorem 32).

A less naive implementation maintains the list of incorrect vertices using a better data structure, saving a linear factor in the complexity. We first explain this, and then discuss the cost $\Delta$ by choosing an appropriate encoding of the quasi-polynomial universal tree constructed in Theorem 32.

## Data structure

We use a data structure similar to the attractor computation presented in Section 2.1, also presented in general terms in Section 1.9. The pseudocode is given in Algorithm 3.5.

The data structure consists of the following objects:

• a leaf of $T$ for each vertex, representing the current function $\mu: V \to Y$;

• a set *Incorrect* of vertices (the order in which vertices are stored and retrieved from the set does not matter);

• a table *Count* storing for each vertex of Eve a number of edges.

For our complexity analysis we use the unit cost RAM model, see Section 1.2 for details. In the case at hand let us choose for the machine word size $w = \log_2(m) + \log_2(d)$, so that an edge together with its priority can be stored in one machine word. The space complexity of this data structure depends on the encoding of $T$, which we will discuss later.

The invariant of the algorithm satisfied before each iteration of the repeat loop is the following:

• for $u \in V_{\text{Eve}}$, the value of *Count*($u$) is the number of incorrect edges of $u$;
• Incorrect is the set of incorrect vertices.

The invariant is satisfied initially thanks to the function Init. Let us assume that we choose and remove $u$ from Incorrect. Since we modify only $\mu(u)$ the only potentially incorrect vertices are in Incorrect (minus $u$) and the incoming edges of $u$; for the latter each of them is checked and added to Incorrect' when required. By monotonicity, incorrect vertices remain incorrect so all vertices in Incorrect (minus $u$) are still incorrect. Hence the invariant is satisfied.

The invariant implies that the algorithm indeed implements Algorithm 3.4 hence returns the minimal progress measure, but it also has implications on the complexity. Indeed one iteration of the repeat loop over some vertex $u$ involves

$$O((|\text{In}^{-1}(u)| + |\text{Out}^{-1}(u)|) \cdot \Delta)$$

operations, the first term corresponds to updating $\mu(u)$ and Incorrect, which requires for each outgoing edge of $u$ to compute $\delta$, and the second term corresponds to considering all incoming edges of $u$. Thus the overall complexity for a single iteration is

$$O\left(\sum_{u \in V} (|\text{In}^{-1}(u)| + |\text{Out}^{-1}(u)|) \cdot \Delta\right) = O(m \cdot \Delta).$$

Since there are at most $n \cdot |T|$ iterations, the running time of the whole algorithm follows as announced.

## Encoding leaves

Let us fix $T$ to be the quasi-polynomial universal tree constructed in Theorem 32.

In our definition of trees we say that a tree is an ordered list of subtrees $[t_1, \dots, t_k]$, so we use $[1, k]$ with the natural order for ordering the subtrees. Any other total order can be used to that effect, and a more appropriate order may lead to smaller encoding. Indeed, using $[1, k]$ for ordering subtrees, if a tree has height $h$ and $n$ leaves then a leaf is a sequence of $h$ numbers in $[1, n]$, so it uses $O(h \log_2(n))$ bits.

Let us consider an order well suited for encoding $T$. We use $\{0, 1\}^*$ the set of binary words and order them using the following three rules that apply for any $u, v \in \{0, 1\}^*$:

$$0u < \varepsilon < 1u \quad ; \quad (0u < 0v \iff u < v) \quad ; \quad (1u < 1v \iff u < v).$$

For words of length at most 2 the order is $00 < 0 < 01 < \varepsilon < 10 < 1 < 11$.

We can now revisit the construction of the universal tree by defining directly the set of leaves. Recall that $T$ is obtained from $T_{\text{left}}$, $T_{\text{middle}}$, and $T_{\text{right}}$. By induction hypothesis leaves in $T_{\text{left}}$ and $T_{\text{right}}$ are tuples of length $h-1$ and leaves in $T_{\text{middle}}$ tuples of length $h$. The leaves of $T$ are:

• leaves of $T_{\text{left}}$ where the first component is prefixed with a 0;

• leaves of $T_{\text{middle}}$ augmented with a new component $\varepsilon$;

• leaves of $T_{\text{right}}$ where the first component is prefixed with a 1.
**Algorithm 3.5:** The value iteration algorithm with explicit data structure.

**Data:** A parity game with $n$ vertices priorities in $[1, d]$ and a $(n, d/2)$-universal tree $T$.

**Function** Init():

```
for u ∈ V do
    ⏐ μ(u) ← ℓ_min

for u ∈ V_Eve do
    for u $p$ → v ∈ E do
        if incorrect: ¬(μ(v) ⊲$_p$ μ(u)) then
            ⏐ Count(u) ← Count(u) + 1
        if Count(u) = Degree(u) then
            ⏐ Add u to Incorrect
    for u ∈ V_Adam do
        for u $p$ → v ∈ E do
            if incorrect: ¬(μ(v) ⊲$_p$ μ(u)) then
                ⏐ Add v to Incorrect
```

**Function** Treat(u):

```
if u ∈ V_Eve then
    ⏐ μ(u) ← min{δ(μ(v), p) : u $p$ → v ∈ E}

if u ∈ V_Adam then
    ⏐ μ(u) ← max{δ(μ(v), p) : u $p$ → v ∈ E}
```

**Function** Update(u):

```
if u ∈ V_Eve then
    ⏐ Count(u) ← 0

for v $p$ → u ∈ E do
    if v $p$ → u is incorrect then
        if v ∈ V_Eve then
            ⏐ Count(v) ← Count(v) + 1
        if Count(v) = Degree(v) then
            ⏐ Add v to Incorrect'
    if v ∈ V_Adam then
        ⏐ Add v to Incorrect'
```

**Function** Main():

```
Init()

for i = 0, 1, 2, ... do
    Incorrect' ← ∅

    for u ∈ Incorrect do
        Treat(u)
        Update(u)
    if Incorrect' = ∅ then
        return μ
    else
        Incorrect ← Incorrect'
```
<figure><img src="image_30.png" /><figcaption>Figure 3.10: The succinct encoding on the (5, 2)-universal tree.</figcaption></figure>

We call this encoding the *succinct encoding*, it is illustrated in Figure 3.10 for the (5,2)-universal tree. The leftmost leaf is (00, ε), and the middle leaf (ε, ε). In general, the inductive construction implies that every leaf is a tuple (D<sub>d-1</sub>, ..., D<sub>1</sub>) such that the sum of the lengths of the directions D<sub>i</sub> is at most log<sub>2</sub>(n). Thus a leaf is encoded using O(log<sub>2</sub>(h) log<sub>2</sub>(n)) bits: for each of the log<sub>2</sub>(n) bits we need log<sub>2</sub>(h) bits to specify its component.

In terms of machine words of size $w = \log_2(n) + \log_2(d)$, this means that a leaf can be stored using $\log_2(d)$ machine words. Hence the data structure uses $O(n \log_2(d))$ machine words, with together with the input size $O(m)$ means that the space complexity of the algorithm is $O(m+n \log_2(d))$.

Using the succinct encoding and a tedious but simple case analysis we can compute $\delta(\ell, p)$ in time $O(\log_2(n) \log_2(d))$. Putting everything together we obtain the overall complexity stated in Theorem 31.

**3.5 Comparing the three families of algorithms**

At the beginning of the chapter we described three families of algorithms: strategy improvement, attractor decomposition, and value iterations.

Let us first clarify the relationship between the separation framework discussed in Section 3.3 and the value iteration paradigm presented in Section 3.4. Both are families of algorithms:

* An (n, d)-separating automaton **A** induces an algorithm for solving parity games in time $O(m \cdot |A|)$ where $|A|$ is the size of **A**, meaning the number of states.

* An (n, d/2)-universal tree **T** induces a value iteration algorithm for solving parity games in time proportional to $|T|$ where $|T|$ is the size of **T**, meaning the number of leaves (the exact complexity depends on the cost of computing $\delta$ in **T**, which is typically small).

These two families are in a strong sense equivalent:

**Theorem 35** (Equivalence between separating automata and universal trees).
* An $(n, d)$-separating automaton induces an $(n, d/2)$-universal tree of the same size;

* An $(n, d/2)$-universal tree induces an $(n, d)$-separating automaton of the same size.

We do not prove this theorem here but note that it can be stated more generally for any half-positionally determined objective, replacing universal trees by the notion of universal graphs. The main advantage of the value iteration presentation is the space complexity, which for a good choice of the universal tree can be made very small (quasi-linear).

In terms of complexity, the strategy improvement has exponential complexity, while both attractor decompositions and value iterations algorithms have quasi-polynomial complexity. Let us make a finer comparison: the complexity of the attractor decomposition algorithm is a polynomial multiplied by the (non polynomial) term

$$ \binom{d-1+\lfloor\log(n)\rfloor}{\lfloor\log(n)\rfloor}, $$

while for the value iteration algorithm the complexity is a polynomial multiplied by the (also non polynomial) term

$$ \binom{d/2-1+\lfloor\log(n)\rfloor}{\lfloor\log(n)\rfloor}. $$

The key difference is that the former performs an induction using all priorities, while the latter considers only odd priorities hence the dependence in $d/2$. Although our presentation of the attractor decomposition algorithm does not make it explicit, this class of algorithms is also related to the notion of universal trees; however an algorithm is induced not by one $(n, d/2)$-universal tree, but by two: one for each player, which are then interleaved to organise the recursive calls of the algorithm.

Since both value iteration and attractor decomposition algorithms are connected to the combinatorial notion of universal trees, the next question is whether the construction given in Section 3.4 is optimal. The answer is unfortunately yes, there exists a lower bound on the size of universal trees which matches this construction up to polynomial factors.

The last question we discuss here is whether there exists a quasi-polynomial strategy improvement algorithm. In particular a natural attempt would be to use universal trees for this endeavour. Unfortunately, the natural approach fails, as we explain now. As we have seen, universal trees can be used to represent progress measures for Eve: given a graph, a vertex is assigned $\top$ if all paths satisfy the complement of parity, and some left of the tree otherwise. Hence they can be used for a strategy improvement algorithm iterating over strategies of Adam. Let us consider the exponential universal tree, we present in Figure 3.11 a game where the strategy improvement algorithm alternates between two strategies, hence does not terminate. The minimal progress measures are illustrated on the right hand side, for both strategies. One can verify that in both cases, the missing edge is an improving edge.
<figure><img src="image_31.png" /><figcaption>Figure 3.11: A game where the strategy improvement over the exponential universal tree does not terminate.</figcaption></figure>

<figure><img src="image_32.png" /><figcaption>Figure 3.12: The two strategies have opposing improving edges (dashed).</figcaption></figure>
Bibliographic references

We refer to Section 2.6 for the role of parity objectives and how they emerged in au-
tomata theory as a subclass of Muller objectives. Another related motivation comes
from the works of Emerson, Jutla, and Sistla [EJS93], who showed that solving parity
games is linear-time equivalent to the model-checking problem for modal µ-calculus.
This logical formalism is an established tool in program verification, and a common
denominator to a wide range of modal, temporal and fixpoint logics used in various
fields.

Let us discuss the progress obtained over the years for each of the three families of
algorithms.

*Value iteration algorithms and separating automata.* The heart of value iteration algorithms is the value function, which in the context of parity games and related developments for automata have been studied under the name progress measures or signatures. They appear naturally in the context of fixed point computations so it is hard to determine who first introduced them. Streett and Emerson [SE84, SE89] defined signatures for the study of the modal µ-calculus, and Stirling and Walker [SW89] later developed the notion. Both the proofs of Emerson and Jutla [EJ91] and of Walukiewicz [Wal96] use signatures to show the positionality of parity games over infinite games.

Jurdziński [Jur00] used this notion to give the first value iteration algorithm for parity games, with running time $O(mn^{d/2})$. The algorithm is called ‘small progress measure lifting’ and is an instance of the class of value iteration algorithms we construct in Section 3.4 by considering the universal tree of size $n^h$. Bernet, Janin, and Walukiewicz [BJW02] investigated the notion of permissive strategies and obtained reductions from parity games to safety games. In essence, they constructed the separating automaton corresponding to the universal tree of size $n^h$, although the general framework of separating automata came later, introduced by Bojańczyk and Czerwiński [BC18].

The new era for parity games started in 2017 when Calude, Jain, Khoussainov, Li, and Stephan [CJK+17] constructed a quasi-polynomial time algorithm. Our presentation follows the technical developments of the subsequent paper by Fearnley, Jain, Schewe, Stephan, and Wojtczak [FJS+17] which recasts the algorithm as a value iteration algorithm. Bojańczyk and Czerwiński [BC18] introduce the separation framework to better understand the original algorithm.

Soon after two other quasi-polynomial time algorithms emerged. Jurdziński and Lazić [JL17] showed that the small progress measure algorithm can be adapted to a ‘succinct progress measure’ algorithm, matching (and slightly improving) the quasi-polynomial time complexity. The presentation using universal tree that we follow in Section 3.4 and an almost matching lower bound on their sizes is due to Fijalkow [Fij18]. The connection between separating automata and universal trees was shown by Czerwiński, Daviaud, Fijalkow, Jurdziński, Lazić, and Parys [CDF+19].

The third quasi-polynomial time algorithm is due to Lehtinen [Leh18]. The original algorithm has a slightly worse complexity ($n^{O(\log(n))}$ instead of $n^{O(\log(d))}$), but it was later improved to (essentially) match the complexity of the previous two algo-
rithms [Par20]. Although not explicitly, the algorithm constructs an automaton with
similar properties as a separating automaton, but the automaton is non-deterministic.
Colcombet and Fijalkow [CF19] revisited the link between separating automata and
universal trees and proposed the notion of good for small games automata, capturing
the automaton defined by Lehtinen's algorithm. The equivalence result between sepa-
rating automata, good for small games automata, and universal graphs, holds for any
half-positionally determined objective, giving a strong theoretical foundation for the
family of value iteration algorithms.

*Attractor decomposition algorithms.* The McNaughton Zielonka's algorithm has complexity $O(mn^d)$. Parys [Par19] constructed the fourth quasi-polynomial time algorithm as an improved take over McNaughton Zielonka's algorithm. As for Lehtinen's algorithm, the original algorithm has a slightly worse complexity ($n^{O(\log(n))}$ instead of $n^{O(\log(d))}$). The construction was later improved [LPSW22]. As discussed in Section 3.5 the complexity of this algorithm is quasi-polynomial and of the form $n^{O(\log(d))}$, but a bit worse than the three previous algorithms since the algorithm is symmetric and has a recursion depth of $d$, while the value iteration algorithms only consider odd priorities hence replace $d$ by $d/2$.

Jurdziński, Morvan, and Thejaswini [JMT22] constructed a generic McNaughton Zielonka's algorithm parameterised by the choice of two universal trees, one for each player. How the value iteration algorithm can simulate the attractor decomposition algorithm was explained by Ohlmann [Ohl21].

*Strategy improvement algorithms.* As we will see in Chapter 4, parity games can be reduced to mean payoff games or energy games, as well as discounted payoff games, so any algorithm for solving them can be used for solving parity games. In particular, the existing strategy improvement algorithms for these games can be run on parity games. Vöge and Jurdziński [VJ00] introduced the first discrete strategy improvement for parity games, running in exponential time. The algorithm we present is due to Björklund, Sandberg, and Vorobyov [BSV03], which was shown to run in sub-exponential time using a randomisation procedure. Our proof of correctness is original. The complexity was reduced to sub-exponential with deterministic algorithms by Jurdziński, Paterson, and Zwick [JPZ08]. For some time there was some hope that the strategy improvement algorithm, for some well chosen policy on switching edges, solves parity games in polynomial time. Friedmann [Fri11] cast some serious doubts by constructing numerous exponential lower bounds applying to different variants of the algorithm. Fearnley [Fea17] investigated efficient implementations of the algorithm, focussing on the cost of computing and updating the value function for a given strategy.

A natural question is whether there exists a quasi-polynomial strategy improvement algorithm. Koh and Loho [KL22] constructed a quasi-polynomial time algorithm and presented it as a strategy improvement algorithm: the subtlety is that in their algorithm, an iteration considers a strategy $\sigma$ together with its valuation $\text{val}^{\sigma}$ and builds a new strategy $\sigma'$ with the additional constraint that $\text{val}^{\sigma'} < \text{val}^{\sigma}$. In other words, it does not improve only based on the strategy $\sigma$. Hence in some sense it is closer to a value iteration algorithm. As discussed in Section 3.5 the notion of universal trees cannot be used to achieve this: the example is due to Ohlmann [Ohl21]. Whether there exists
a quasi-polynomial time strategy improvement algorithm for parity games remains to
this day open.
# GAMES WITH PAYOFFS

<figure><img src="image_33.png" /></figure>
Chapter 4

# Games with Payoffs

NATHANAËL FIJALKOW, BENJAMIN MONMEGE

This chapter considers quantitative objectives defined using payoffs. Adding quantities can serve two goals: the first is for refining qualitative objectives by quantifying how well, how fast, or at what cost a qualitative objective is satisfied, and the second is to define richer specifications and preferences over outcomes.

* We start in Section 4.2 by studying extensions of the classical qualitative objectives. Among two strategies in a reachability game that guarantee to reach a target in ten steps or in a billion steps, we would certainly prefer the first one from a pragmatic point of view.

* We continue in Section 4.1 by introducing two approaches for proving positional determinacy, that imply the results we need in this chapter.

* We study mean payoff games in Section 4.3, and energy games along the way. We present three algorithms for solving them, the first two based on value iteration and the third on strategy improvement. Along the way we show that parity games reduce to mean payoff games.

* We study discounted payoff games in Section 4.4. We construct a strategy improvement algorithm for computing the value function. We also show that mean payoff games reduce to discounted payoff games, so the previous algorithm yields an algorithm for computing the value function of a mean payoff game.

* We study shortest path games in Section 4.5. They extend reachability games by requiring that Min reaches her target with minimal cost, which if the weights are all equal means as soon as possible.

* We study total payoff games in Section 4.6.
## Notations

In this chapter all objectives we consider use the set of colours $C = \mathbb{Z}$ the set of integers (or $C = \mathbb{Z} \cup \{\text{Win}\}$ for the shortest path objective), so a colour is called a weight interpreted as a payoff for Max. We will study different quantitative objectives corresponding to different ways of aggregating the weights. We let $\text{val}_{\text{Max}}^{\mathcal{G}}(v)$ and $\text{val}_{\text{Min}}^{\mathcal{G}}(v)$ be the values for Max and Min in the game $\mathcal{G}$: this is the best each player can unilaterally guarantee from the vertex $v$, no matter which strategy the other player uses. All the quantitative objectives we will study in this chapter are Borel, hence determined thanks to Corollary 1: $\text{val}_{\text{Max}}^{\mathcal{G}}(v) = \text{val}_{\text{Min}}^{\mathcal{G}}(v)$ for all vertices $v$. We thus let $\text{val}^{\mathcal{G}}(v)$ denote this value (and $\text{val}^{\mathcal{G}}(v)$ if $\mathcal{G}$ is clear from the context).

For complexity statements we use the unit cost RAM model as defined in Section 1.2. Let us make some preliminary remarks, and consider a game $\mathcal{G}$ with an objective using the set of colours $C = \mathbb{Z}$. We let $W$ denote the largest weight appearing in $\mathcal{G}$ in absolute value. Choosing the machine word size $w = \log(m) + \log(W)$ implies that an edge together with its weight can be stored in one machine word and that we can perform arithmetic operations on weights, hence for most objectives we use the machine word size $w = \log(m) + \log(W)$. The only exception will be the discounted payoff objectives, which additionally have a discount factor $\lambda \in (0, 1)$ that needs to be given in the input.

## 4.1 Proving positional determinacy over finite arenas

In this section we present two approaches for proving positional determinacy of quantitative objectives over finite arenas.

### Positional determinacy via first cycle games

**Theorem 36 (First cycle games).** Let $\Phi: C^\omega \to R \cup \{\pm\infty\}$ a quantitative objective, and $f: C^* \to R \cup \{\pm\infty\}$. We assume that the following properties are satisfied. For all games $\mathcal{G}$ with objective $\Phi$:

* for all $x \in R \cup \{\pm\infty\}$, for all plays $\pi$,

$$ (\forall c \in \text{Cycles}(\pi), f(c) \ge x) \implies \Phi(\pi) \ge x, $$

* for all $x \in R \cup \{\pm\infty\}$, for all plays $\pi$,

$$ (\forall c \in \text{Cycles}(\pi), f(c) \le x) \implies \Phi(\pi) \le x, $$

* $\Phi$ is prefix independent.

Then $\Phi$ is uniformly positionally determined over finite arenas.

To build some intuition, let us consider the case of mean payoff: let $\Phi = \text{MeanPayoff}^+$. Then the properties above hold when considering for $f$ the function Mean:

$$ \text{Mean}(w_0 \dots w_{k-1}) = \frac{1}{k} \sum_{i=0}^{k-1} w_i. $$
Let us argue that the first property holds. To estimate MeanPayoff<sup>+</sup>(π) let us look at the prefix π<sub><k</sub> of π of length k. Indeed MeanPayoff<sup>+</sup>(π) = limsup<sub>k</sub> Mean(π<sub><k</sub></sub>). To calculate Mean(π<sub><k</sub></sub>) we use the fact that every vertex in π<sub><k</sub></sub> either belongs to exactly one cycle in Cycles(π<sub><k</sub></sub>) or to π̂<sub><k</sub>, and the linearity of the arithmetic mean:

$$
\mathrm{Mean}(\pi_{<k}) = \mathrm{Mean}\{\mathrm{Mean}(\hat{\pi}_{<k}), \{\mathrm{Mean}(c) : c \in \mathrm{Cycles}(\pi_{<k})\}\}.
$$

By assumption each Mean(c) is greater than or equal to x. Note that since $\pi_{<k}$ does not contain any cycle, it has length at most n, independently of k. On the other hand Cycles($\pi_{<k}$) has size at least k/n. Hence when k tends to infinity the term Mean($\pi_{<k}$) vanishes and we have MeanPayoff<sup>+</sup>(π) = limsup<sub>k</sub> Mean($\pi_{<k}$)} ≥ x.

The second property follows as above from the linearity of the arithmetic mean and
the cycle decomposition. The third property will be proved in Lemma 32.

**Corollary 6 (Positional determinacy of mean payoff).** *Mean payoff objectives are uniformly positionally determined over finite arenas.*

By duality this is equivalent to saying that both limit superior and limit inferior
mean payoff objectives are uniformly positionally determined over finite arenas.

Proof. Let $\mathcal{A}$ an arena. A cycle is a sequence $c = v_0 \xrightarrow{w_0} v_1 \xrightarrow{w_1} v_2 \dots v_{k-1} \xrightarrow{w_{k-1}} v_0$. For technical convenience we do not indicate the returning vertex $v_0$ when introducing a cycle.

Let us consider a finite play $\pi = v_0 \xrightarrow{w_0} v_1 \xrightarrow{w_1} \dots$, we define two objects by induction: the cycle decomposition Cycles($\pi$) and the folded play $\hat{\pi}$. To guide the intuition: Cycles($\pi$) is a list of some cycles in $\pi$, and $\hat{\pi}$ is obtained from $\pi$ by removing the cycles from Cycles($\pi$) and does not contain any cycle.

If $\pi$ is a single vertex then the cycle decomposition is empty and the folded play is equal to $\pi$. Otherwise let $\pi' = \pi \xrightarrow{w} v$, by induction we have already defined Cycles($\pi'$) and $\hat{\pi}'$. There are two cases:

* Either $v$ appears in $\hat{\pi}'$ and then $\hat{\pi}$ is obtained from $\hat{\pi}' \xrightarrow{w} v$ by replacing that cycle by $v$ and Cycles($\pi$) by adding the cycle to Cycles($\pi'$).

* Or $v$ does not appear in $\hat{\pi}'$ and then $\hat{\pi} = \hat{\pi}' \xrightarrow{w} v$ and Cycles($\pi$) = Cycles($\pi'$).

The cycle decomposition breaks down $\pi$ into (possibly interleaved) cycles and the
folded play: every vertex in $\pi$ either belongs to exactly one cycle in $\text{Cycles}(\pi)$ or
to $\hat{\pi}$. For instance for

$$
\pi = v_0 \xrightarrow{w_0} v_1 \xrightarrow{w_1} v_2 \xrightarrow{w_2} v_3 \xrightarrow{w_3} v_2 \xrightarrow{w_4} v_4 \xrightarrow{w_5} v_1 \xrightarrow{w_6} v_5
$$

we have Cycles(π) = (c₁ = v₂ w₂ → v₃ w₃ → ; c₂ = v₁ w₁ → v₂ w₄ → v₄ w₅ →) and π̂ = v₀ w₀ → v₁ w₆ → v₅, as illustrated in Figure 4.1.

The definition of Cycles(π) is extended for infinite plays. We write FC(π) for the first cycle in π.

Let $\mathcal{G} = (\mathcal{A}, \Phi(c))$. The outline of the proof is as follows.
<figure><img src="image_34.png" /><figcaption>Figure 4.1: An example for the cycle decomposition. The first cycle is $c_1$ and is in red, the cycle $c_2$ is in blue, and $\hat{\pi} = v_0 \xrightarrow{w_0} v_1 \xrightarrow{w_6} v_5$.</figcaption></figure>

1. We define the condition FirstCycle and $\mathcal{G}_{FC} = (\mathcal{A}, \text{FirstCycle})$, and show that $\text{val}^{\mathcal{G}} = \text{val}^{\mathcal{G}_{FC}}$ and that if $\mathcal{G}_{FC}$ is positionally determined then $\mathcal{G}$ is positionally determined.

2. We define the condition FirstCycleReset$_v$ (parameterised by a vertex $v$) and $\mathcal{G}_{FCR(v)} = (\mathcal{A}, \text{FirstCycleReset}_v)$, and show that $\text{val}^{\mathcal{G}} = \text{val}^{\mathcal{G}_{FCR(v)}}$.

3. We show that $\mathcal{G}_{FC}$ is positionally determined.

**Step 1.** The condition FirstCycle computes the value of $f$ on the first cycle. Formally:

$$ \text{FirstCycle}(\pi) = f(\text{FC}(\pi)). $$

Let us define $\mathcal{G}_{FC} = (\mathcal{A}, \text{FirstCycle})$. We make two claims:

* let $\sigma_{FC}$ a strategy in $\mathcal{G}_{FC}$, it induces a strategy $\sigma$ in $\mathcal{G}$ such that $\text{val}^{\sigma_{FC}} \le \text{val}^{\sigma}$, and $\sigma$ is positional if $\sigma_{FC}$ is, and

* let $\tau_{FC}$ a strategy in $\mathcal{G}_{FC}$, it induces a strategy $\tau$ in $\mathcal{G}$ such that $\text{val}^{\tau_{FC}} \ge \text{val}^{\tau}$, and $\tau$ is positional if $\tau_{FC}$ is.

Let us prove the first claim. We let $\sigma(\pi) = \sigma_{FC}(\hat{\pi})$: by definition if $\pi$ is a play consistent with $\sigma$ then $\hat{\pi}$ is a play consistent with $\sigma_{FC}$. Note that indeed if $\sigma_{FC}$ is positional then so is $\sigma$. We show that $\text{val}^{\sigma_{FC}} \le \text{val}^{\sigma}$.

Let $\pi$ be a play consistent with $\sigma$ from $v_0$ and $x = \text{val}^{\sigma_{FC}}(v_0)$. We first argue that all cycles in Cycles($\pi$) have value for $f$ greater than or equal to $x$. Indeed consider a cycle $c$ in Cycles($\pi$) and let $\pi'$ the prefix of $\pi$ ending with the cycle $c$. The play $\hat{\pi}'$ is consistent with $\sigma_{FC}$, implying that $f(c) \ge x$. Thanks to the first property, this implies that $\Phi(\pi) \ge x$.

We turn to the second claim. The construction is identical for Min: we let $\tau(\pi) = \tau_{FC}(\hat{\pi})$. We show that $\text{val}^{\tau_{FC}} \ge \text{val}^{\tau}$ following the same arguments. Let $\pi$ be a play consistent with $\tau$ from $v_0$ and $x = \text{val}^{\tau_{FC}}(v_0)$. Thanks to the second property, this implies that $\Phi(\pi) \le x$.

Let us now prove that $\text{val}^{\mathcal{G}} = \text{val}^{\mathcal{G}_{FC}}$ using the two claims. We first need to establish that $\mathcal{G}_{FC}$ is determined: one argument is that FirstCycle is a Borel condition, hence determinacy follows from the general Borel determinacy result (Theorem 1). Another
simpler argument is that FirstCycle is a finite duration condition, meaning that the
outcome of the play is determined with a finite number of steps (at most $n$), hence
determinacy follows from an easier direct argument for finite duration games.

It follows from the two claims that

$$
\begin{align*}
\mathrm{val}_{\mathcal{G}_{\mathrm{FC}}}^{\mathcal{G}} &= \sup_{\sigma_{\mathrm{FC}}} \mathrm{val}^{\sigma_{\mathrm{FC}}} \leq \sup_{\sigma} \mathrm{val}^{\sigma} = \mathrm{val}^{\mathcal{G}} \\
\mathrm{val}_{\mathcal{G}_{\mathrm{FC}}}^{\mathcal{G}} &= \inf_{\tau_{\mathrm{FC}}} \mathrm{val}^{\tau_{\mathrm{FC}}} \geq \inf_{\tau} \mathrm{val}^{\tau} = \mathrm{val}^{\mathcal{G}},
\end{align*}
$$

where in both lines: the first equalities is by determinacy of $\mathcal{G}_{\text{FC}}$, the inequalities thanks to the two claims, and the last equalities by determinacy of $\mathcal{G}$. The two obtained inequalities imply that $\text{val}^{\mathcal{G}} = \text{val}^{\mathcal{G}_{\text{FC}}}$, and positional optimal strategies for either player in $\mathcal{G}_{\text{FC}}$ induce positional optimal strategies in $\mathcal{G}$.

**Step 2.** We define a third condition on $\mathcal{A}$:

$$
\text{FirstCycleReset}_v(\pi) = \begin{cases} \text{FirstCycle}(\pi) & \text{if } \pi \text{ does not visit } v \text{ before FC}(\pi), \\ \text{FirstCycle}(\pi_{\ge k}) & \text{for } k \text{ the first index such that } \text{In}(\pi_k) = v. \end{cases}
$$

In words: if a cycle is closed before visiting $v$, then the condition is FirstCycle and otherwise when reaching $v$ the game is ‘reset’ and the condition is FirstCycle from this point onwards.

This second step is similar to the first step; the reason why we separated them is
because this step relies on the fact that $\Phi$ is prefix independent.

Let us define $\mathcal{G}_{\text{FCR}(v)} = (\mathcal{A}, \text{FirstCycleReset}_v)$. We make two claims:

* let $\sigma_{\text{FCR}(v)}$ an optimal strategy in $\mathcal{G}_{\text{FCR}(v)}$, it induces a strategy $\sigma$ in $\mathcal{G}$ such that $\text{val}^{\sigma_{\text{FCR}(v)}} \le \text{val}^{\sigma}$, and

* let $\tau_{\text{FCR}(v)}$ an optimal strategy in $\mathcal{G}_{\text{FCR}(v)}$, it induces a strategy $\tau$ in $\mathcal{G}$ such that $\text{val}^{\tau_{\text{FCR}(v)}} \ge \text{val}^{\tau}$.

Let us prove the first claim. We let

$$
\sigma(\pi) = \begin{cases} \sigma_{\text{FCR}(v)}(\hat{\pi}) & \text{if } \pi \text{ does not contain } v, \\ \sigma_{\text{FCR}(v)}(\hat{\pi}_{\ge k}) & \text{for } k \text{ the first index such that } \text{In}(\pi_k) = v. \end{cases}
$$

We show that $\text{val}^{\sigma_{\text{FCR}(v)}} \le \text{val}^{\sigma}$. Let $\pi$ a play consistent with $\sigma$ from $v_0$ and $x = \text{val}^{\sigma_{\text{FCR}(v)}}(v_0)$. There are two cases.

Either $\pi$ does not contain $v$, and then as in the first step this implies that all cycles
in $\pi$ have an arithmetic mean greater than or equal to $x$, and we conclude as in the first
step that $\text{FirstCycleReset}_v(\pi) \ge x$.

Or $\pi$ contains $v$. We first argue that $x = \text{val}^{\sigma_{\text{FCR}(v)}}(v_0) \le \text{val}^{\sigma_{\text{FCR}(v)}}(v)$. Indeed, let $\pi_0$ be a play without cycles from $v_0$ to $v$ consistent with $\sigma_{\text{FCR}(v)}$, we let $\sigma'(\pi) = \sigma_{\text{FCR}(v)}(\pi_0\pi)$. Then $\text{val}^{\sigma_{\text{FCR}(v)}}(v_0) \le \text{val}^{\sigma'}(v) \le \text{val}^{\sigma_{\text{FCR}(v)}}(v)$, the first inequality is because a play $\pi$ consistent with $\sigma'$ from $v$ correspond to the play $\pi_0\pi$ consistent with $\sigma_{\text{FCR}(v)}$ from $v_0$, and the second inequality by optimality of $\sigma_{\text{FCR}(v)}$.

Let $y = \text{val}^{\sigma_{\text{FCR}(v)}}(v)$, the inequality above reads $x \le y$. Let $\pi'$ the suffix of $\pi$ starting from the first occurrence of $v$, then $\pi'$ is consistent with $\sigma_{\text{FCR}(v)}$ from $v$, so as in the first
step this implies that all cycles in $\pi'$ have an arithmetic mean greater than or equal to $y$. We conclude as in the first step that $\Phi(\pi') \ge y \ge x$, The last but important argument is that $\Phi$ is prefix independent, implying that $\Phi(\pi) \ge x$.

We prove that $\text{val}^{\mathcal{G}} = \text{val}^{\mathcal{G}_{\text{FCR}(v)}}$ using the two claims following the same arguments as in the first step. In particular we need to establish that $\mathcal{G}_{\text{FCR}(v)}$ is determined, and again it either follows from the general Borel determinacy result (Theorem 1) or by determinacy for finite duration games.

**Step 3.** We (finally!) prove that $\mathcal{G}_{\text{FC}}$ is positionally determined. Let us consider the case of Max, the case of Min being symmetric. We show that for all games there exists an optimal positional strategy, by induction on the number of vertices of Max with more than one outgoing edge. The base case is clear since in that case there is a unique strategy and it is positional. Let $v \in V_{\text{Max}}$ with more than one outgoing edge.

Let $\sigma_{\text{FCR}(v)}$ an optimal strategy in $\mathcal{G}_{\text{FCR}(v)}$. Intuitively, since the game is reset at the first visit of $v$ and that the second visit to $v$ would close a loop hence determine the outcome, we can use any optimal strategy from $v$. We define $\sigma'$ as follows:

$$ \sigma'(\pi) = \begin{cases} \sigma(\pi) & \text{if } \pi \text{ does not contain } v, \\ \sigma(\pi_{\ge k}) & \text{for } k \text{ the last index such that } \text{In}(\pi_k) = v. \end{cases} $$

Note that indeed $\sigma'$ uses only one outgoing edge of $v$. We show that $\text{val}^{\mathcal{G}_{\text{FCR}(v)},\sigma}(v_0) \le \text{val}^{\mathcal{G}_{\text{FCR}(v)},\sigma'}(v_0)$, implying that $\sigma'$ is optimal in $\mathcal{G}_{\text{FCR}(v)}$ and the inequality is an equality.

Let $\pi$ be a play consistent with $\sigma'$ from $v_0$. If it does not contain $v$ it is consistent with $\sigma$, so FirstCycleReset$_v(\pi) \ge \text{val}^{\mathcal{G}_{\text{FCR}(v)},\sigma}(v_0)$. If it contains $v$, let $\pi'$ the suffix of $\pi$ starting from the first occurrence of $v$, then FirstCycleReset$_v(\pi) = \text{FirstCycle}(\pi')$. Since $\pi'$ is consistent with $\sigma$ (until a cycle is formed) we have $\text{FirstCycle}(\pi') \ge \text{val}^{\mathcal{G}_{\text{FCR}(v)},\sigma}(v_0)$, implying that FirstCycleReset$_v(\pi) \ge \text{val}^{\mathcal{G}_{\text{FCR}(v)},\sigma}(v_0)$. We conclude: $\text{val}^{\mathcal{G}_{\text{FCR}(v)},\sigma'}(v_0) \le \text{val}^{\mathcal{G}_{\text{FCR}(v)},\sigma}(v_0)$.

Let $\mathcal{B}$ the arena obtained from $\mathcal{A}$ by removing all outgoing edges of $v$ not used by $\sigma'$. Let $\mathcal{G}'_{\text{FCR}(v)} = (\mathcal{B}, \text{FirstCycleReset}_v)$ and $\mathcal{G}'_{\text{FC}} = (\mathcal{B}, \text{FirstCycle})$. By definition we have $\text{val}^{\mathcal{G}_{\text{FCR}(v)},\sigma'} = \text{val}^{\mathcal{G}'_{\text{FCR}(v)},\sigma'} = \text{val}^{\mathcal{G}'_{\text{FCR}(v)}}$. In the previous step we proved that $\text{val}^{\mathcal{G}'_{\text{FC}}} = \text{val}^{\mathcal{G}'_{\text{FCR}(v)}}$, so $\text{val}^{\mathcal{G}'_{\text{FC}}} = \text{val}^{\mathcal{G}_{\text{FC}}}$. The arena $\mathcal{B}$ contains one less vertex of Max with more than one outgoing edge, so the induction hypothesis applies and implies that there exists an optimal strategy in $\mathcal{G}'_{\text{FC}}$, which is also optimal in $\mathcal{G}_{\text{FC}}$ thanks to the equality $\text{val}^{\mathcal{G}'_{\text{FC}}} = \text{val}^{\mathcal{G}_{\text{FC}}}$. $\square$

## Positional determinacy via fairly mixing property

**Definition 7** (Fairly mixing). A quantitative objective $\Phi: C^\omega \to R \cup \{\pm\infty\}$ is fairly mixing if:

1. for all $x \in C^+$, $y_0, y_1 \in C^\omega$, if $\Phi(y_0) \le \Phi(y_1)$ then $\Phi(xy_0) \le \Phi(xy_1)$;

2. for all $x \in C^+$, $y \in C^\omega$, $\min(\Phi(x^\omega), \Phi(y)) \le \Phi(xy) \le \max(\Phi(x^\omega), \Phi(y))$;
3. if $(x_i)_{i \in \mathbb{N}}$ is a sequence of non-empty words $x_i \in C^+$ such that $x_0x_1x_2\cdots$ contains only a finite number of colours, and $I \uplus J = \mathbb{N}$ is a partition of $\mathbb{N}$ into two infinite sets, then

$$ \inf(\mathcal{P}_I \cup \mathcal{P}_J) \leq \Phi(x_0x_1x_2\cdots) \leq \sup(\mathcal{P}_I \cup \mathcal{P}_J) \\ \text{with } \mathcal{P}_I = \{\Phi(x_{i_0}x_{i_1}x_{i_2}\cdots) \mid i_k \in I\} \text{ and } \mathcal{P}_J = \{\Phi(x_{j_0}x_{j_1}x_{j_2}\cdots) \mid j_k \in J\}. $$

It is not difficult to convince oneself that the following quantitative objectives: Inf, Sup, LimInf, LimSup, MeanPayoff$^+$, MeanPayoff$^-$, Energy, DiscountedPayoff, TotalPayoff are all are fairly mixing.

**Theorem 37** (Fairly mixing induces positional determinacy). If $\Phi$ is a fairly mixing quantitative objective, then $\Phi$ is uniformly positionally determined over finite arenas.

The (rather technical) proof is by induction on the number of vertices.

**Corollary 7.** The quantitative objectives Inf, Sup, LimInf, LimSup, MeanPayoff$^+$, MeanPayoff$^-$, Energy, DiscountedPayoff, TotalPayoff are all uniformly positionally determined over finite arenas.

## 4.2 Refining qualitative objectives with quantities

In this section we define quantitative objectives extending the qualitative objectives Safe, Reach, Buchi, and CoBuchi. The four quantitative objectives we will define in this section return as outcome some weight in the sequence (for instance, the maximum weight). This is in contrast with the MeanPayoff and DiscountedPayoff objectives that we will study later, which perform arithmetic operations on the sequence of weights.

A first way to compute a payoff from a sequence of weights $\rho \in \mathbb{Z}^\omega$ is to consider the maximum weight in the sequence:

$$ \text{Sup}(\rho) = \sup_i \rho_i. $$

This extends the qualitative objective Reach(Win) in the following sense: the objective Reach(Win) corresponds to the quantitative objective Sup using two weights: 0 for Lose and 1 for Win. The outcome of a sequence is 1 if and only if the sequence contains Win. It refines Reach(Win) by specifying (numerical) preferences.

The dual objective is to consider the smallest weight:

$$ \text{Inf}(\rho) = \inf_i \rho_i. $$

The qualitative objective Safe(Win) corresponds to the quantitative objective Inf using two weights: 0 for Win and 1 for Lose. The outcome of a sequence is 0 if and only if the sequence does not contain Lose.

Similarly the following quantitative objectives refine Buchi and CoBuchi:

$$ \text{LimSup}(\rho) = \limsup_i \rho_i, \quad \text{LimInf}(\rho) = \liminf_i \rho_i. $$

The analyses and algorithms for solving games with Reach, Safe, Buchi, and CoBuchi objectives extend to these four quantitative objectives.
**Theorem 38** (Sup, Inf, LimSup, LimInf objectives). *Games with objectives Sup, Inf, LimSup, and LimInf are uniformly positionally determined. There exists an algorithm for computing the value function of those games in polynomial time and space. More precisely, let $k$ be the number of different weights in the game, the time complexity is $O(m)$ for objectives Sup and Inf, and $O(knm)$ for objectives LimSup and LimInf, and for all algorithms the space complexity is $O(m)$.*

*Proof.* We sketch the algorithm for the objective Sup, the other cases are similar. Let $c_1 < \dots < c_k$ be the ordered enumeration of all weights in the game. The set of vertices of value $c_k$ is $\text{Attr}_{\text{Max}}(c_k)$, which can be computed in linear time. We then construct the subgame $\mathcal{G}'$ of $\mathcal{G}$ induced by $V \setminus \text{Attr}_{\text{Max}}(c_k)$, and continue recursively: $\mathcal{G}'$ has one less weight.

A naive complexity analysis yields a time complexity $O(km)$, but it is easily refined to $O(m)$ by revisiting the attractor computation and showing that each edge in the whole game is treated at most once throughout the recursive attractor computations. This complexity analysis does not extend to $\text{LimSup}$ and $\text{LimInf}$ objectives, where the complexity is multiplied by $k$. $\square$

## 4.3 Mean payoff games

A natural approach for aggregating an infinite sequence of weights is to consider the arithmetic mean. Since the sequence $(\frac{1}{k}\sum_{i=0}^{k-1} \rho_i)_{k \in \mathbb{N}}$ may not converge, we can either consider the limit superior or the limit inferior, leading to the two definitions:

$$ \text{MeanPayoff}^{+}(\rho) = \limsup_{k} \frac{1}{k} \sum_{i=0}^{k-1} \rho_i \quad ; \quad \text{MeanPayoff}^{-}(\rho) = \liminf_{k} \frac{1}{k} \sum_{i=0}^{k-1} \rho_i. $$

Note that $\text{MeanPayoff}^{+}(-\rho) = -\text{MeanPayoff}^{-}(\rho)$, where in $-\rho$ we take the opposite of each weight. In other words, $\text{MeanPayoff}^{+}$ and $\text{MeanPayoff}^{-}$ are dual objectives.

In this section we study mean payoff games. We will first prove that they are prefix independent, then that they are positionally determined, and then construct algorithms for solving them and compute the value function. The best known time complexity for both problems is pseudo-polynomial, meaning polynomial when the numerical inputs are given in unary.

**Lemma 32** (Prefix independence). $\text{MeanPayoff}^{+}$ is prefix independent.

*Proof.* We show that $\text{MeanPayoff}^{+}(\rho_0\rho_1\dots) = \text{MeanPayoff}^{+}(\rho_p\rho_{p+1}\dots)$ for a fixed
$p \in \mathbb{N}:$

$$ \limsup_k \frac{1}{k} \sum_{i=0}^{k-1} \rho_i = \limsup_k \left( \underbrace{\frac{1}{k} \sum_{i=0}^{p-1} \rho_i}_{\to 0 \text{ for } k \to \infty} + \underbrace{\frac{k-p}{k}}_{\to 1 \text{ for } k \to \infty} \cdot \frac{1}{k-p} \sum_{i=p}^{k-1} \rho_i \right) \\ = \liminf_k \frac{1}{k-p} \sum_{i=0}^{p-1} \rho_{p+i}. $$

□

Note that by duality this implies that MeanPayoff⁻ is also prefix independent.

In the setting we consider in this chapter, meaning two player zero sum games of perfect information, the two objectives are equivalent, which will be a corollary of Corollary 6.

As an example, consider the mean payoff game represented in Figure 4.2. As we will show later, the positional strategies defined below are optimal strategies for Max and Min:

$$ \sigma^*(v_0) = v_0 \xrightarrow{4} v_1 ; \quad \sigma^*(v_2) = v_2 \xrightarrow{4} v_3 \\ \tau^*(v_1) = v_1 \xrightarrow{2} v_2 ; \quad \tau^*(v_3) = v_3 \xrightarrow{-1} v_1 ; \quad \tau^*(v_4) = v_4 \xrightarrow{-2} v_0. $$

The play consistent with $\sigma^*$ and $\tau^*$ starting from $v_0$ is the lasso word

$$ v_0 \xrightarrow{4} v_1 \left( v_1 \xrightarrow{2} v_2 \xrightarrow{4} v_3 \xrightarrow{-1} v_1 \right)^\omega, $$

which has as mean payoff the average weight of the cycle $v_1 \xrightarrow{2} v_2 \xrightarrow{4} v_3 \xrightarrow{-1} v_1$, i.e. 5/3. If we restrict ourselves to memoryless strategies for both players, we may easily convince ourselves that this is the best that both players may aim for. Indeed,

* the loop around $v_4$ has average weight 2;

* the simple cycle alternating between $v_0$ and $v_4$ has average weight 1.5;

* the simple cycle alternating between $v_0$ and $v_1$ has average weight 2;

* the loop around $v_2$ has average weight 1, and

* the simple cycle alternating between $v_0$, $v_1$, $v_2$ and $v_3$ has average weight 2.

Therefore, we may check that no player can obtain a better mean payoff than 5/3, from its own point of view: for instance, if Max switches her decision in $v_0$, hoping to get value 2, she will get a lower value 1.5 since Min still prefers cycle alternating between $v_0$ and $v_4$ to his self-loop around $v_4$. This is the case for all starting vertices, which proves that all vertices have the same value 5/3.

Let us draw some corollaries from positional determinacy of mean payoff games.

**Corollary 8 (Limit superior and limit inferior mean payoff games).**
<figure><img src="image_35.png" /><figcaption>Figure 4.2: A mean payoff game.</figcaption></figure>

* Limit superior and limit inferior mean payoff games are equivalent: for every arena $\mathcal{A}$ and colouring function $c: E \to \mathbb{Z}$, let $\mathcal{G}_+ = (\mathcal{A}, \text{MeanPayoff}^+(c))$ and $\mathcal{G}_- = (\mathcal{A}, \text{MeanPayoff}^-(c))$, then $\text{val}^{\mathcal{G}_+} = \text{val}^{\mathcal{G}_-}$. This implies that a positional strategy is optimal in $\mathcal{G}_+$ if and only if it is optimal in $\mathcal{G}_-$.

Since they are equivalent we speak of mean payoff games without specifying whether the objective is $\text{MeanPayoff}^+$ or $\text{MeanPayoff}^-$, and write $\text{MeanPayoff}$ instead.

* For a mean payoff game with $n$ vertices and weights in $[-W, W]$, the mean payoff values are rational numbers in $[-W, W]$ whose denominators are at most $n$.

*Proof.* Thanks to Corollary 6, there exist $\sigma_+$ and $\tau_+$ optimal positional strategies in $\mathcal{G}_+$ and $\sigma_-$ and $\tau_-$ optimal positional strategies in $\mathcal{G}_-$ (for the latter by duality). By definition $\text{val}^{\mathcal{G}_+}(v) = \text{MeanPayoff}^+(\pi_{\sigma_+, \tau_+}^v)$ and $\text{val}^{\mathcal{G}_-}(v) = \text{MeanPayoff}^-(\pi_{\sigma_-, \tau_-}^v)$. Since $\text{MeanPayoff}^- \le \text{MeanPayoff}^+$ we already have $\text{val}^{\mathcal{G}_-} \le \text{val}^{\mathcal{G}_+}$.

For two positional strategies $\sigma$ and $\tau$, the play $\pi_{\sigma, \tau}$ is a lasso, meaning of the form $\pi_c^\omega$ with $\pi$ a simple path and $c$ a simple cycle, implying that $\text{MeanPayoff}^+(\pi_{\sigma, \tau}) = \text{MeanPayoff}^-(\pi_{\sigma, \tau})$, let us write $\text{MeanPayoff}(\pi_{\sigma, \tau})$ for this value.

We have:

$$ \text{MeanPayoff}(\pi_{\sigma_+, \tau_+}^v) \le \text{MeanPayoff}(\pi_{\sigma_+, \tau_-}^v) \le \text{MeanPayoff}(\pi_{\sigma_-, \tau_-}^v), $$

where the first inequality is by optimality of $\tau_-$ and the second inequality by optimality of $\sigma_-$. Hence $\text{val}^{\mathcal{G}_+} \le \text{val}^{\mathcal{G}_-}$, and finally $\text{val}^{\mathcal{G}_+} = \text{val}^{\mathcal{G}_-}$.

For the second item, recall that $\text{val}^{\mathcal{G}}(v) = \text{MeanPayoff}(\pi_{\sigma, \tau}^v)$ with $\sigma$ and $\tau$ optimal positional strategies. Let us write $\pi_{\sigma, \tau}^v = \pi_c^\omega$ with $\pi$ a simple path and $c$ a simple cycle, then by prefix independence $\text{MeanPayoff}(\pi_{\sigma, \tau}^v) = \text{Mean}(c)$, thus $\text{val}^{\mathcal{G}}(v)$ is the mean of at most $n$ weights from $\mathcal{G}$. $\square$

## Solving mean payoff games in NP $\cap$ coNP

The positional determinacy of mean payoff games easily gives an upper bound on the complexity of solving these games.
**Theorem 39 (Complexity of mean payoff).** *Solving mean payoff games is in NP ∩ coNP.*

*Proof.* The first ingredient for this proof is a polynomial time algorithm for solving the one player variants of mean payoff games. Indeed, they correspond to the minimum cycle mean problem in a weighted graph, which can be solved in polynomial time by a dynamic programming algorithm. The second ingredient is the positional determinacy result proved in Corollary 6.

Let us show the NP membership. Consider a mean payoff game $\mathcal{G}$, a vertex $v$ and a threshold $x \in \mathbb{Q} \cup \{\pm\infty\}$. Thanks to Corollary 6, we know that there exist an optimal positional strategy for Max. With a non-deterministic Turing machine, we may guess a positional strategy for Max, and check that it ensures $x$ in $\mathcal{G}$ from $v$.

Let us now show the coNP membership. By determinacy of mean payoff games, whether Max cannot ensure $x$ in $\mathcal{G}$ from $v$ is equivalent to whether Min can ensure $x$ in $\mathcal{G}$ from $v$. Again thanks to Corollary 6, we know that there exist an optimal positional strategy for Min. With a non-deterministic Turing machine, we may guess a positional strategy for Min, and check that it ensures $x$ in $\mathcal{G}$ from $v$. □

We can turn the non-deterministic algorithm given in Theorem 39 into a deterministic algorithm with exponential complexity since there are exponentially many positional strategies.

**Reducing parity games to mean payoff games**

We now show that solving mean payoff games is at least as hard as solving parity games.

**Theorem 40 (Reducing parity games to mean payoff games).** *Solving parity games reduce in polynomial time to solving mean payoff games with threshold 0.*

*Proof.* Let $\mathcal{G} = (\mathcal{A}, \text{Parity}(c))$ a parity game with $n$ vertices and priorities in $[1, d]$. We construct a mean payoff game $\mathcal{G}' = (\mathcal{A}, \text{MeanPayoff}[c'])$ using the same arena and the colouring function:

$$c'(e) = (-n)^{c(e)}.$$

Note that $c'(e)$ is of polynomial size since $\log(|c'(e)|) = c(e) \log(n) \le d \log(n)$.

The key property relating $c'$ and $c$ is the following: let $c$ a simple cycle

$$v_0 \xrightarrow{p_0} p_1 \xrightarrow{p_2} v_2 \cdots v_{k-1} \xrightarrow{p_{k-1}} v_0,$$

then the largest priority in $c$ is even if and only if the mean value with respect to $c'$ is non-negative. Indeed, if the largest priority in $c$ is $p$ even, then it contributes $n^p$ and all other values are greater than or equal to $-n^{p-1}$, and since there are at most $n$ in total, the largest priority dominates the others.

We claim that for all vertices $v$, $v \in W_{\text{Eve}}(\mathcal{G})$ if and only if $\text{val}^{\mathcal{G}'} \ge 0$. Let $v \in W_{\text{Eve}}(\mathcal{G})$, and $\sigma$ a positional strategy winning from $v$ in $\mathcal{G}$, we show that $\sigma$ ensures mean payoff at least 0 in $\mathcal{G}'$ from $v$. Indeed, in $\mathcal{G}[\sigma, v]$ all cycles are even, which
thanks to the above implies that all cycles in $\mathcal{G}'[\sigma, v]$ are non-negative. The converse implication is similar: a positional strategy $\sigma'$ in $\mathcal{G}'$ ensuring mean payoff at least 0 from $v$ has the property that all cycles in $\mathcal{G}'[\sigma, v]$ are non-negative, hence that all cycles in $\mathcal{G}[\sigma, v]$ are even, therefore that it is winning in $\mathcal{G}$ from $v$. $\square$

Note that we did not construct a reduction between objectives as defined in Section 1.6: indeed it is not true that Parity reduces to $\text{MeanPayoff}_{\ge 0}$, the reduction depends on the number $n$ of vertices. As a corollary of Theorem 39, this polynomial reduction gives an alternative proof of the fact that solving parity games is in $\text{NP} \cap \text{coNP}$.

## A first value iteration algorithm using finite horizon payoffs

Let us give a first algorithm for solving mean payoff games using the value iteration paradigm. The idea is to consider the game where we only play for a fixed number of steps $k$, and the payoff is the sum of the weights. We compute iteratively the optimal values for increasing values of $k$, and show that for $k$ large enough it allows us to obtain the values of mean payoff up by a simple rounding procedure.

Let $\mathcal{G} = (\mathcal{A}, \text{MeanPayoff}[c])$ a mean payoff game with $n$ vertices and weights in $[-W, W]$. Recall that for a vertex $u$, the mean payoff value is defined as

$$ \text{val}^{\mathcal{G}}(u) = \sup_{\sigma} \inf_{\tau} \text{MeanPayoff}[c](\pi_{u}^{\sigma, \tau}). $$

Our goal is to compute these values, or compare them to a threshold.

Let us fix a number $k$ and define the following objective summing the first $k$ weights:

$$ \text{Payoff}_k(\rho) = \sum_{i=0}^{k-1} \rho_i. $$

Let us define $\text{val}^{\mathcal{G},k}: V \to \mathbb{Z}$ the value function for the $\text{Payoff}_k$ objective:

$$ \text{val}^{\mathcal{G},k}(u) = \sup_{\sigma} \inf_{\tau} \text{Payoff}_k[c](\pi_{u}^{\sigma, \tau}). $$

We let $F_V$ be the set of functions $V \to \mathbb{Z}$, we define the operator $\mathcal{O}^{\mathcal{G}}: F_V \to F_V$ by:

$$ \mathcal{O}^{\mathcal{G}}(\mu)(u) = \begin{cases} \max\{\mu(v) + w: u \xrightarrow{w} v \in E\} & \text{if } u \in V_{\text{Max}}, \\ \min\{\mu(v) + w: u \xrightarrow{w} v \in E\} & \text{if } u \in V_{\text{Min}}. \end{cases} $$

Let $\mu_0$ defined by $\mu_0(u) = 0$ for all $u$ and $\mu_{k+1} = \mathcal{O}^{\mathcal{G}}(\mu_k)$.

**Lemma 33.** The following holds for all $k$.

* We have $\mu_k = \text{val}^{\mathcal{G},k}$.

* For all $u \in V$ we have $k \cdot \text{val}^{\mathcal{G}}(u) - 2nW \le \text{val}^{\mathcal{G},k} \le k \cdot \text{val}^{\mathcal{G}}(u) + 2nW$.
*Proof.* The proof of the first item is an easy induction on $k$. We turn to the second item. Let us consider $\sigma$ a positional optimal strategy for Max. We claim that for all $k$, the strategy $\sigma$ ensures from $u$ that $\text{Payoff}_k[c]$ is at least $(k-n) \cdot \text{val}^{\mathcal{G}}(u) - nW$. We first note that all cycles reachable from $u$ in $\mathcal{G}[\sigma]$ have values (meaning, average value of the weights) at least $\text{val}^{\mathcal{G}}(u)$. Now, consider a path of length $k$, and iteratively remove cycles from it. What remains is a most $n$ edges, which contribute in the worst case to $-nW$. The remaining $k-n$ edges are included in some cycle, hence contribute $(k-n) \cdot \text{val}^{\mathcal{G}}(u)$. Since $\text{val}^{\mathcal{G}}(u) \le W$, we obtain a lower bound of $k \cdot \text{val}^{\mathcal{G}}(u) - 2nW$.

The argument is symmetrical for Adam.

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

A direct corollary is as follows.

**Corollary 9.** We have $\lim_{k \to \infty} \frac{1}{k} \cdot \text{val}^{\mathcal{G},k} = \text{val}^{\mathcal{G}}$.

However, we can make this effective using Corollary 8, which places bounds on the mean payoff values. This yields two very simple algorithms, one for computing the mean payoff values, and the other one for solving mean payoff games.

**Theorem 41.** The following holds.

* There exists an algorithm running in time $O(n^3mW)$ for computing the mean payoff values.

* There exists an algorithm running in time $O(n^2mW)$ for solving the mean payoff games, meaning determining whether $\text{val}^{\mathcal{G}}(u) \ge c$ for some threshold $c$.

*Proof.* Both arguments rely on Corollary 8.

* Let us fix $k = 4n^3W$. We can compute the values $\text{val}^{\mathcal{G},k}$ in time $O(n^3mW)$ as explained above. The value of $k$ was chosen in such a way that

$$ \text{val}^{\mathcal{G},k}(u) - \frac{1}{2n(n-1)} < \text{val}^{\mathcal{G}}(u) < \text{val}^{\mathcal{G},k}(u) + \frac{1}{2n(n-1)}. $$

Indeed, since $\text{val}^{\mathcal{G}}(u)$ is a rational number whose denominator is at most $n$, the minimum distance between two possible values of $\text{val}^{\mathcal{G}}(u)$ is at most $\frac{1}{n(n-1)}$.

Hence the exact value of $\text{val}^{\mathcal{G}}(u)$ is the unique rational number with a denominator at most $n$ that lies in the interval

$$ \left[ \text{val}^{\mathcal{G},k}(u) - \frac{1}{2n(n-1)}, \text{val}^{\mathcal{G},k}(u) + \frac{1}{2n(n-1)} \right], $$

which is easily computed.

* The distance between $c$ and the closest rational number with a denominator at most $n$ is $\frac{1}{n}$, so to determine whether $\text{val}^{\mathcal{G}}(u) \ge c$ it is enough to compute the values $\text{val}^{\mathcal{G},k}$ for $k = 4n^2W$.

<figure><img src="image_37.png" /></figure>
A second value iteration algorithm using energy

Let us give a second algorithm, based on energy games. The construction of the algo-
rithm will follow closely the high-level presentation of value iteration algorithms given
in Section 1.9. Let $\mathcal{G} = (\mathcal{A}, \text{MeanPayoff}[c])$ a mean payoff game with $n$ vertices and
weights in $[-W, W]$.

The key insight is to use the energy objective. Recall that the energy quantitative
objective is defined over the set of colours $C = \mathbb{Z}$:

$$
\text{Energy}(\rho) = \inf \left\{ \ell \in \mathbb{N} : \forall k \in \mathbb{N}, \ell + \sum_{i=0}^{k-1} \rho_i \ge 0 \right\}.
$$

The interpretation is the following: weights are energy consumptions (negative values) and recharges (positive values), and Energy($\rho$) is the smallest initial budget $\ell$ such that Min can ensure that the energy level remains non-negative forever. Let us be careful here: maximising the mean payoff objective corresponds to minimising the energy objective. We formalise the relationship between mean payoff and energy in the following lemma.

**Lemma 34** (Relating mean payoff and energy objectives). Let $G$ be a mean payoff graph. Then $G$ satisfies $\text{MeanPayoff}^{-} \ge 0$ if and only if it satisfies $\text{Energy} < \infty$.

*Proof.* Let us say that a cycle in $G$ is non-negative if the sum of its weights is non-negative. We consider the following properties:

(i) $G$ satisfies $\text{MeanPayoff}^{-} \ge 0$.

(ii) All cycles in $G$ are non-negative.

(iii) $G$ satisfies $\text{Energy} < \infty$.

We prove the implications $(i) \Rightarrow (ii)$, then $(ii) \Rightarrow (iii)$, and finally $(iii) \Rightarrow (i)$.

$(i) \Rightarrow (ii)$ is clear.

$(ii) \Rightarrow (iii)$. Let us consider an infinite path, and strike out all edges involved in a cycle in it. At most $n$ edges are not stricken out, incurring at most $-nW$ in energy drop. Since cycles are non-negative, the lowest level in a cycle is also lower bounded by $-nW$. Hence the energy level of the infinite path is at most $2nW$.

$(iii) \Rightarrow (i)$. Assume that $G$ satisfies $\text{Energy} < \infty$, this implies that all partial sums are greater than or equal to a constant $\ell$. This implies that the means of the partial sums are lower bounded by $\ell/k$, which converges to 0 when $k$ goes to infinity. Therefore $G$ satisfies $\text{MeanPayoff}^{-} \ge 0$. $\square$

It is tempting to claim that a stronger property hold, namely $\text{MeanPayoff}^{-}(\rho) \ge 0$ if and only if $\text{Energy}(\rho) < \infty$. This is not the case.

**Corollary 10.** Let $\mathcal{G}$ a mean payoff game. We define $\mathcal{G}'$ the energy game induced by $\mathcal{G}$. Then for all vertices $u$, we have $\text{val}^{\mathcal{G}}(u) \ge 0$ if and only if $\text{val}^{\mathcal{G}'}(u) < \infty$. Consequently:

* An algorithm computing the energy values induces an algorithm for solving mean payoff games with the same complexity.
* An algorithm computing the energy values in time $T(n,m,W)$ induces an algorithm for computing the mean payoff values in time $O(\log(n^2W) \cdot T(n,m,W))$.

*Proof.* We consider $\sigma$ a positional optimal strategy for Max in $\mathcal{G}$, we have $\text{val}^{\mathcal{G}} = \text{val}^{\mathcal{G},\sigma}$. Let $u$ such that $\text{val}^{\mathcal{G}}(u) \ge 0$, we consider the subgraph of $\mathcal{G}[\sigma, u]$ of vertices reachable from $u$. Thanks to Lemma 34 applied to this graph, since $\text{val}^{\mathcal{G},\sigma}(u) \ge 0$ we have $\text{val}^{\mathcal{G}',\sigma}(u) < \infty$. This implies that $\sigma$ (seen as a strategy for Min in $\mathcal{G}'$) ensures $\text{Energy} < \infty$, hence $\text{val}^{\mathcal{G}'}(u) < \infty$.

Conversely, we consider $\tau$ a positional optimal strategy for Min in $\mathcal{G}'$, we have $\text{val}^{\mathcal{G}'} = \text{val}^{\mathcal{G}',\tau}$. Let $u$ such that $\text{val}^{\mathcal{G}'}(u) < \infty$, we consider the subgraph of $\mathcal{G}[\tau, u]$ of vertices reachable from $u$. Thanks to Lemma 34 applied to this graph, since $\text{val}^{\mathcal{G}',\tau}(u) < \infty$ we have $\text{val}^{\mathcal{G}',\tau}(u) \ge 0$. This implies that $\tau$ (seen as a strategy for Max in $\mathcal{G}$) ensures $\text{MeanPayoff} \ge 0$, hence $\text{val}^{\mathcal{G}}(u) \ge 0$.

The first consequence is immediate. For the second, we use a simply binary search. Indeed, to determine whether $\text{val}^{\mathcal{G}}(u) \ge c$, we can shift all weights by $c$, thus reducing to the question whether $\text{val}^{\mathcal{G}}(u) \ge 0$, and compute the energy values. Thanks to Corollary 8 the mean payoff values are rational numbers in $[-W, W]$ whose denominators are at most $n$, so this requires $O(\log(n^2W))$ calls. $\square$

Therefore, we set as a goal to compute the energy values.

**Theorem 42 (Value iteration algorithm).** *There exists a value iteration algorithm which computes the energy values in time $O(mnW)$.*

We define $Y = \mathbb{N} \cup \{\infty\}$, equipped with the natural total order on integers. We let $F_V$ be the lattice of functions $V \to Y$ equipped with the componentwise order induced by $Y$. We define a function $\delta: Y \times [-W, W] \to Y$ by $\delta(l, w) = \max(l - w, 0)$. This induces an operator $\mathcal{O}^{\mathcal{G}}: F_V \to F_V$:

$$ \mathcal{O}^{\mathcal{G}}(\mu)(u) = \begin{cases} \min \left\{ \delta(\mu(v), w) : u \xrightarrow{w} v \in E \right\} & \text{if } u \in V_{\text{Min}}, \\ \max \left\{ \delta(\mu(v), w) : u \xrightarrow{w} v \in E \right\} & \text{if } u \in V_{\text{Max}}. \end{cases} $$

We note that $\mathcal{O}^{\mathcal{G}}$ is a monotonic operator, therefore it has a least fixed point.

**Lemma 35 (Least fixed point for energy games).** Let $\mathcal{G}$ an energy game with $n$ vertices and weights in $[-W, W]$. Then the least fixed point of $\mathcal{O}^{\mathcal{G}}$ computes the energy values of $\mathcal{G}$.

*Proof.* We first argue that the energy values, meaning the function $\text{val}^{\mathcal{G}}: V \to \mathbb{Z} \cup \{\infty\}$, form a fixed point of the operator $\mathcal{O}^{\mathcal{G}}$. The fact that $\text{val}^{\mathcal{G}} = \mathcal{O}^{\mathcal{G}}(\text{val}^{\mathcal{G}})$ is a routine verification, which follows from two properties (see Lemma 8).

* For all $\rho$ sequences of weights, we have $\text{Energy}(w \cdot \rho) = \delta(\text{Energy}(\rho), w)$.

* The function $\delta$ is monotonic and continuous.
It already yields one inequality: $\text{val}^\mathcal{G}$ is larger than or equal to the least fixed point of $\mathcal{O}^\mathcal{G}$. Let us give another proof of the same inequality. We recall that thanks to Kleene fixed point theorem (Theorem 4), the least fixed point of $\mathcal{O}^\mathcal{G}$ is computed as follows:

$$ \forall u \in V, \mu_0(u) = 0 \quad ; \quad \mu_{b+1} = \mathcal{O}^\mathcal{G}(\mu_b). $$

We have $\mu_0 \le \mu_1 \le \dots$, and since $F_V$ is a finite lattice, for some $k$ we have that $\mu_k$ is the least fixed point of $\mathcal{O}^\mathcal{G}$. The crux here is to understand what are the values $\mu_b$ for $b = 0, 1, \dots$. Let us define the truncated energy objective:

$$ \text{Energy}_b(\rho) = \inf \left\{ \ell \in \mathbb{N} : \forall k \in [0, b], \ell + \sum_{i=0}^{k-1} \rho_i \ge 0 \right\}. $$

The interpretation is the following: $\text{Energy}_b(\rho)$ is the smallest initial budget $\ell$ such that Min can ensure that the energy level remain non-negative for the first $b$ steps. A simple induction on $b$ shows that $\mu_b$ is the values for $\text{Energy}_b$ in $\mathcal{G}$. Note that $\text{Energy}_0 \le \text{Energy}_1 \le \dots \le \text{Energy}$, hence $\mu_b = \text{val}^{\text{Energy}_b} \le \text{val}^\mathcal{G}$, the desired inequality.

Let us now prove the converse inequality: $\text{val}^\mathcal{G}$ is smaller than or equal to the least fixed point of $\mathcal{O}^\mathcal{G}$. For this, we consider a fixed point $\mu$ of $\mathcal{O}^\mathcal{G}$, and argue that $\text{val}^\mathcal{G} \le \mu$. To this end, we extract from $\mu$ a strategy $\tau$ for Min, and show that $\text{val}^\tau \le \mu$; since we know that $\text{val}^\mathcal{G} \le \text{val}^\tau$, this implies $\text{val}^\mathcal{G} \le \mu$. We define $\tau$ as an argmin strategy:

$$ u \in V_{\text{Min}} : \tau(u) \in \text{argmin} \left\{ \delta(\mu(v), w) : u \xrightarrow{w} v \in E \right\}. $$

Let us define the graph $G = \mathcal{G}[\tau]$, by definition of $\tau$ for all edges $u \xrightarrow{w} v$ in $G$ we have $\mu(u) \ge \delta(\mu(v), w)$. We claim that this implies that for all paths $\rho$ from $u$ in $G$, we have $\text{Energy}(\rho) \le \mu(u)$. To this end, we show that for all $k \in \mathbb{N}$ we have $\mu(u) + \sum_{i=0}^{k-1} \rho_i \ge 0$. We proceed by induction on $k$. This is clear for $k = 0$, let us assume that it holds for $k$ and show that it also does for $k + 1$. Let us write $\rho_0 = u \xrightarrow{w} v$. By the property above, we have $\mu(u) \ge \delta(\mu(v), w) = \max(\mu(v) - w, 0) \ge \mu(v) - w$. Hence

$$ \mu(u) + \sum_{i=0}^{k} \rho_i = \mu(u) + w + \sum_{i=1}^{k} \rho_i \ge \mu(v) + \sum_{i=0}^{k-1} \rho_i \ge 0, $$

where the last inequality is by induction hypothesis for the path $\rho_1 \dots \rho_{k-1}$ from $v$. This concludes the induction. $\square$

Lemma 35 does not immediately yield a value iteration algorithm because the lattice $Y$ is infinite. However, let us note that by positional determinacy, the value of a vertex is the value of a path consisting of a prefix of length at most $n$ and a simple cycle, which is $\infty$ if the cycle is negative and in $[0, nW]$ otherwise. Hence we can equivalently define $Y = [0, nW] \cup \{\infty\}$ and $\delta(\ell, w) = \max(\ell - w, 0)$ if $\ell - w \le nW$, and $\infty$ otherwise. It is clear that the least fixed points for both operators coincide thanks to the remark above, and now that we have a finite lattice we obtain the value iteration algorithm presented in Algorithm 4.1.
<caption>**Algorithm 4.1:** The value iteration algorithm for energy games.</caption>

**Data:** An energy game
**for** $u \in V$ **do**
  **while** $\mu(u) \neq 0$
    **repeat**
      $\mu \leftarrow \mathcal{O}^{\mathcal{G}}(\mu)$
    **until** $\mu = \mathcal{O}^{\mathcal{G}}(\mu)$;
    **return** $\mu$

The value iteration algorithm for energy games is conceptually very simple, its pseudocode is given in Algorithm 4.1. Since for each vertex its value can only increase, and at each iteration at least one vertex increases, the total number of iterations before reaching the fixed point is at most $O(nW)$. However to obtain the announced complexity of $O(nmW)$, one needs to be a little bit more subtle: in the naive version the computational cost of an iteration of $\mathcal{O}^{\mathcal{G}}$ is $O(nm)$, since we need to look at each vertex and each outgoing edge. This can be improved using a more involved data structure keeping track of vertices to be updated. We detail this below.

**Refined value iteration algorithm for energy values**

The pseudocode is given in Algorithm 4.2. For an edge $u \xrightarrow{w} v$ we say that it is incorrect if $\mu(u) < \delta(\mu(v), w)$. A vertex $u \in V_{\text{Max}}$ is incorrect if it has an outgoing edge which is incorrect, and a vertex $u \in V_{\text{Min}}$ is incorrect if all of its outgoing edges are incorrect. The key idea of the data structure we are building is not to keep track of all incorrect edges for vertices in $V_{\text{Min}}$, but rather to count them.

The data structure consists of the following objects:

* a value of $Y$ for each vertex, representing the current function $\mu: V \to Y$;

* a set *Incorrect* of vertices (the order in which vertices are stored and retrieved from the set does not matter);

* a table *Count* storing for each vertex of Min a number of edges.

For our complexity analysis we use the unit cost RAM model, see Section 1.2 for details. In the case at hand let us choose for the machine word size $w = \log_2(m) + \log_2(W)$, so that an edge together with its weight can be stored in one machine word.

The invariant of the algorithm satisfied before each iteration of the repeat loop is the following:

* for $u \in V_{\text{Min}}$, the value of *Count*($u$) is the number of incorrect edges of $u$;

* *Incorrect* is the set of incorrect vertices.

The invariant is satisfied initially thanks to the function *Init*. Let us assume that we choose and remove $u$ from *Incorrect*. Since we modify only $\mu(u)$ the only potentially incorrect vertices are in *Incorrect* (minus $u$) and the incoming edges of
u; for the latter each of them is checked and added to Incorrect' when required. By monotonicity, incorrect vertices remain incorrect so all vertices in Incorrect (minus u) are still incorrect. Hence the invariant is satisfied.

The invariant implies that the algorithm indeed implements Algorithm 4.1 hence returns the minimal fixed point, but it also has implications on the complexity. Indeed one iteration of the repeat loop over some vertex u involves

$$O((|\text{In}^{-1}(u)| + |\text{Out}^{-1}(u)|))$$

operations: the first term corresponds to updating $\mu(u)$ and Incorrect, which requires for each outgoing edge of $u$ to compute $\delta$, and the second term corresponds to considering all incoming edges of $u$. Thus the running time for a single iteration is

$$O\left(\sum_{u \in V} (|\text{In}^{-1}(u)| + |\text{Out}^{-1}(u)|)\right) = O(m).$$

Since there are at most $n \cdot W$ iterations, we obtain the running time of $O(n \cdot m \cdot W)$.

## A strategy improvement algorithm for energy games

As explained above, solving energy games yields algorithms for solving mean payoff games. So, we continue our investigation of energy games, and now construct a strategy improvement algorithm for them.

**Theorem 43 (Strategy improvement algorithm for energy games).** There exists a strategy improvement algorithm for solving energy games in exponential time.

We rely on the high-level presentation of strategy improvement algorithms given in Section 1.10, although it is not necessary to have read that part. We have already proved in Lemma 35 that the energy values correspond to the least fixed point of the operator $\mathcal{O}^{\mathcal{G}}$ defined by:

$$\mathcal{O}^{\mathcal{G}}(\mu)(u) = \begin{cases} \min \{ \delta(\mu(v), w) : u \xrightarrow{w} v \in E \} & \text{if } u \in V_{\text{Min}}, \\ \max \{ \delta(\mu(v), w) : u \xrightarrow{w} v \in E \} & \text{if } u \in V_{\text{Max}}. \end{cases}$$

Recall that $Y = [0, nW] \cup \{\infty\}$, and $F_V$ is the lattice of functions $V \to Y$ equipped with the componentwise order induced by $Y$. The function $\delta: Y \times [-W, W] \to Y$ is defined by $\delta(\ell, w) = \max(\ell - w, 0)$ if $\ell - w \le nW$, and $\infty$ otherwise.

**Improving a strategy.** Let $\sigma$ a (positional) strategy for Max, and a vertex $u \in V_{\text{Max}}$, we say that $e: u \xrightarrow{w} v$ is an improving edge if

$$\delta(\text{val}^{\sigma}(v), w) > \text{val}^{\sigma}(u).$$

Intuitively: according to $\text{val}^{\sigma}$, playing $e$ is better than playing $\sigma(u)$.
<caption>**Algorithm 4.2:** The refined value iteration algorithm for energy games.</caption>

**Function Init() :**
**for** $u \in V$ **do**
  $\lfloor \mu(u) \rfloor \leftarrow 0$
**for** $u \in V_{\text{Min}}$ **do**
  **for** $u \xrightarrow{w} v \in E$ **do**
    **if** incorrect: $\mu(u) < \delta(\mu(v), w)$ **then**
      $\lfloor \text{Count}(u) \rfloor \leftarrow \text{Count}(u) + 1$
    **if** Count($u$) = Degree($u$) **then**
      $\lfloor \text{Add } u \text{ to Incorrect} \rfloor$
**for** $u \in V_{\text{Max}}$ **do**
  **for** $u \xrightarrow{w} v \in E$ **do**
    **if** incorrect: $\mu(u) < \delta(\mu(v), w)$ **then**
      $\lfloor \text{Add } u \text{ to Incorrect} \rfloor$

**Function Treat(u):**
**if** $u \in V_{\text{Max}}$ **then**
  $\lfloor \mu(u) \rfloor \leftarrow \max\{\delta(\mu(v),w) : u \xrightarrow{w} v \in E\}$
**if** $u \in V_{\text{Min}}$ **then**
  $\lfloor \mu(u) \rfloor \leftarrow \min\{\delta(\mu(v),w) : u \xrightarrow{w} v \in E\}$

**Function Update(u):**
**if** $u \in V_{\text{Min}}$ **then**
  $\lfloor \text{Count}(u) \rfloor \leftarrow 0$
**for** $v \xrightarrow{w} u \in E$ which is incorrect **do**
  **if** $v \in V_{\text{Min}}$ **then**
    $\lfloor \text{Count}(v) \rfloor \leftarrow \text{Count}(v) + 1$
    **if** Count($v$) = Degree($v$) **then**
      $\lfloor \text{Add } v \text{ to Incorrect}' \rfloor$
  **if** $v \in V_{\text{Max}}$ **then**
    $\lfloor \text{Add } v \text{ to Incorrect}' \rfloor$

**Function Main() :**
**Init ()**
**for** $i = 0, 1, 2, \dots$ **do**
  Incorrect' $\leftarrow \emptyset$
  **for** $u \in \text{Incorrect}$ **do**
    Treat($u$)
    Update($u$)
    **if** Incorrect' $= \emptyset$ **then**
      **return** $\mu$
    **else**
      $\lfloor \text{Incorrect} \leftarrow \text{Incorrect}' \rfloor$
Given a strategy $\sigma$ and a set of improving edges $S$ (for each $u \in V_{\text{Max}}$, $S$ contains at most one outgoing edge of $u$), we write $\sigma[S]$ for the strategy

$$ \sigma[S](u) = \begin{cases} e & \text{if there exists } e = u \xrightarrow{w} v \in S, \\ \sigma(v) & \text{otherwise.} \end{cases} $$

The difficulty is that an edge being improving does not mean that it is a better move than the current one in any context, but only according to the value function $\text{val}^{\sigma}$, so it is not clear that $\sigma[S]$ is better than $\sigma$. Strategy improvement algorithms depend on the following two principles:

* **Progress:** updating a strategy using improving edges is a strict improvement,

* **Optimality:** a strategy which does not have any improving edges is optimal.

Let us write $\sigma \le \sigma'$ if for all vertices $v$ we have $\text{val}^{\sigma}(v) \le \text{val}^{\sigma'}(v)$, and $\sigma < \sigma'$ if additionally $\neg(\sigma' \le \sigma)$.

**The algorithm.** The pseudocode of the algorithm is given in Algorithm 4.3.

<caption>**Algorithm 4.3:** The strategy improvement algorithm for energy games.</caption>

**Data:** An energy game $\mathcal{G}$
Choose an initial strategy $\sigma_0$ for Max
**for** $i = 0, 1, 2, \dots$ **do**
&emsp;Compute $\text{val}^{\sigma_i}$ and the set of improving edges
&emsp;&emsp;**if** $\sigma_i$ does not have improving edges **then**
&emsp;&emsp;&emsp;**return** $\sigma_i$
&emsp;Choose a non-empty set $S_i$ of improving edges
&emsp;&emsp;$\sigma_{i+1} \leftarrow \sigma_i[S_i]$

**The potential reduction point of view.** A first important insight into the algorithm is through so-called potential reductions. From a game $\mathcal{G}$ and a strategy $\sigma$ with value $\text{val}^{\sigma}$, we define $\mathcal{G}_{\sigma}$ as follows. The two games are identical, except for the weights: if $u \xrightarrow{w} v$ in $\mathcal{G}$, then $u \xrightarrow{w+\text{val}^{\sigma}(v)-\text{val}^{\sigma}(u)} v$ in $\mathcal{G}_{\sigma}$.

**Fact 15.** We have $\text{val}^{\mathcal{G}} = \text{val}^{\sigma} + \text{val}^{\mathcal{G}_{\sigma}}$.

*Proof.* This follows from the observation that given any finite play

$$ \pi = v_0 \xrightarrow{w_0} v_1 \cdots v_{k-1} \xrightarrow{w_{k-1}} v_k $$

in $\mathcal{G}$, writing the corresponding play $\pi' = v_0 \xrightarrow{w_0} v_1 \cdots v_{k-1} \xrightarrow{w'_{k-1}} v_k$ in $\mathcal{G}_{\sigma}$, we have a telescoping sum:

$$ \sum_{i=0}^{k-1} w'_{i} = \text{val}^{\sigma}(v_k) - \text{val}^{\sigma}(v_0) + \sum_{i=0}^{k-1} w_i. $$

□
<figure><img src="image_38.png" /><figcaption>Figure 4.3: An example of potential reduction.</figcaption></figure>

The benefit of this point of view is to interpret the notion of improving edges in $\mathcal{G}_\sigma$.

**Fact 16.** Let $e = u \xrightarrow{w} v$ an edge in $\mathcal{G}$.

* if $u \in V_{\text{Max}}$, then $e$ is an improving edge if and only if its weight in $\mathcal{G}_\sigma$ is negative.

* if $u \in V_{\text{Max}}$ and $\sigma(u) = e$ then the weight of $e$ in $\mathcal{G}_\sigma$ is zero.

* if $u \in V_{\text{Min}}$, then the weight of $e$ in $\mathcal{G}_\sigma$ is non-negative.

The second and third properties directly follow from the fact that $\text{val}^\sigma$ is a fixed point of $\mathcal{O}^{\mathcal{G}[\sigma]}$.

**Proof of correctness.** We now rely on Lemma 35 to prove the two principles: progress and optimality.

**Lemma 36** (Progress for the strategy improvement algorithm for energy games). Let $\sigma$ a strategy and $S$ a set of improving edges. We let $\sigma'$ denote $\sigma[S]$. Then $\sigma < \sigma'$.
**Proof.** We use the potential reduction point of view. Let us apply Fact 15 to the game $\mathcal{G}[\sigma']$: we have $\text{val}^{\sigma'} = \text{val}^{\sigma} + \text{val}^{G'}$. Thanks to Fact 16 in $G'$ all weights are non-positive, implying that $\text{val}^{G'} \ge 0$, and even $\text{val}^{G'} > 0$ because the weights corresponding to improving edges are negative. $\square$

**Lemma 37** (Optimality for the strategy improvement algorithm for energy games). Let $\sigma$ be a strategy that has no improving edges, then $\sigma$ is optimal.

**Proof.** We prove the contrapositive: assume that $\sigma$ is not optimal, we show that it must have some improving edge. The fact that $\sigma$ is not optimal means that $\text{val}^{\sigma} < \text{val}^{G}$. Since $\text{val}^{G}$ is the least fixed point of $\mathcal{O}^{G}$, it is also its least pre-fixed point. Therefore $\text{val}^{\sigma}$ is not a pre-fixed point: $\neg(\text{val}^{\sigma} \ge \mathcal{O}^{G}(\text{val}^{\sigma}))$. Hence there exists $u \in V$ such that $\text{val}^{\sigma}(u) < \mathcal{O}^{G}(\text{val}^{\sigma})(u)$.

We rule out the case that $u \in V_{\text{Min}}$: since $\text{val}^{\sigma}$ is a fixed point of $\mathcal{O}^{G}[\sigma]$, this implies that for $u \in V_{\text{Min}}$ we have $\text{val}^{\sigma}(u) = \min\{\delta(\text{val}^{\sigma}(v), w) : u \xrightarrow{w} v \in E\}$, equal to $\mathcal{O}^{G}(\text{val}^{\sigma})(u)$. Therefore $u \in V_{\text{Max}}$, implying that there exists $u \xrightarrow{w} v$ such that $\text{val}^{\sigma}(u) < \delta(\text{val}^{\sigma}(v), w)$. This is the definition of $u \xrightarrow{w} v$ being an improving edge. $\square$

**Complexity analysis.** The computation of $\text{val}^{\sigma}$ for a strategy $\sigma$ can be seen to be a shortest path problem. Thus, any algorithm for the shortest path problem can be applied, such as the Bellman-Ford algorithm. In particular computing $\text{val}^{\sigma}$ can be done in polynomial time, and even more efficiently through a refined analysis.

An aspect of the algorithm we did not develop is choosing the set of improving edges. Many possible rules for choosing this set have been studied, as for instance the greedy all-switches rule.

The next question is the number of iterations, meaning the length of the sequence $\sigma_0, \sigma_1, \dots$. It is at most exponential since it is bounded by the number of strategies (which is bounded aggressively by $m^n$). There are lower bounds showing that the sequence can be of exponential length, which apply to different rules for choosing improving edges. Hence the overall complexity is exponential; we do not elaborate further here. We refer to Section 4.6 for bibliographic references and a discussion on the family of strategy improvement algorithms.

## 4.4 Discounted payoff games

From a practical point of view, the modelling of a real-world situation via mean payoff games requires that only the long-term behaviour is important. Since mean payoff only depends on the limit of the play, it cannot be used to model the beginning of the execution: the mean payoff is prefix independent. In economical studies, there is a tendency to make the prefixes count more, since they represent short-term implications of the actions taken, even if long-term behaviours also matter. The common payoff used to model this preference to prefixes is the discounted payoff that associates to a
play $\rho$ the value

$$ \text{DiscountedPayoff}(\rho) = (1 - \lambda) \cdot \sum_{i=0}^{\infty} \lambda^i \rho_i, $$

where $\lambda$ is a parameter in the interval (0, 1), ensuring the convergence of the infinite series (since weights $\pi_i$ are bounded). We assume that $\lambda$ is a rational number, it is part of the input of a discounted payoff game. The coefficient $1 - \lambda$ before the series is just to counterbalance the fact that if all weights in the game are 1, we would like the payoff to be 1 too, which then holds since $\sum_{i=0}^{\infty} \lambda^i = \frac{1}{1-\lambda}$. When $\lambda$ tends to 0, only the prefixes (and even the first weight) matters. On the contrary, when $\lambda$ tends to 1, the discounted payoff looks more and more like the mean payoff. To grasp an intuition why this holds, consider a play that results from positional strategies in a mean payoff game. The weights encountered during the play then ultimately follow a periodic sequence $w_0, w_1, \dots, w_{r-1}, w_0, w_1, \dots, w_{r-1}, w_0, \dots$ with average payoff $\frac{1}{r} \sum_{i=0}^{r-1} w_i$. Grouping the terms of the series $(1 - \lambda) \sum_{i=0}^{\infty} \lambda^i w_i$ by batches of r terms, we then obtain

$$ (1 - \lambda) \sum_{i=0}^{\infty} \lambda^{r_i} \sum_{j=0}^{r_i-1} \lambda^j w_j = \frac{1 - \lambda}{1 - \lambda^r} \sum_{j=0}^{r_i-1} \lambda^j w_j = \frac{1}{1 + \lambda + \dots + \lambda^{r-1}} \sum_{j=0}^{r_i-1} \lambda^j w_j $$

that tends towards the average-payoff $\frac{1}{r} \sum_{j=0}^{r-1} w_j$ when $\lambda$ tends to 1.

The game of Figure 4.2 can also be equipped with a discounted payoff condition. If $\lambda$ is close to 1, for instance $\lambda = 0.9$, then optimal strategies are the same as for the mean payoff objective:

$$ \begin{aligned} \sigma^*(v_0) &= v_0 \xrightarrow{4} v_1 \quad ; \quad \sigma^*(v_2) = v_2 \xrightarrow{4} v_3 \\ \tau^*(v_1) &= v_1 \xrightarrow{2} v_2 \quad ; \quad \tau^*(v_3) = v_3 \xrightarrow{-1} v_1 \quad ; \quad \tau^*(v_4) = v_4 \xrightarrow{-2} v_0. \end{aligned} $$

The play consistent with $\sigma^*$ and $\tau^*$ starting from $v_0$ is the lasso word

$$ v_0 \xrightarrow{4} v_1 \cdot (v_1 \xrightarrow{2} v_2 \xrightarrow{4} v_3 \xrightarrow{-1} v_1)^\omega, $$

which has as discounted payoff $(1 - \lambda) \left(4 + \frac{2\lambda + 4\lambda^2 - \lambda^3}{1 - \lambda^3}\right)$, it is approximately 1.7 when $\lambda = 0.99$. Recall that the mean payoff optimal value of vertex $v_0$ was $5/3 \approx 1.67$. However, the situation completely changes when $\lambda$ decreases. When $\lambda = 0.5$ for instance, Min changes his decision in vertex $v_1$ and his optimal move is $v_1 \xrightarrow{0} v_0$. For a really low value of $\lambda$, for instance $\lambda = 0.1$, the decisions again change drastically for both players: now the optimal (positional) strategies become

$$ \begin{aligned} \sigma^*(v_0) &= v_0 \xrightarrow{4} v_1 \quad ; \quad \sigma^*(v_2) = v_2 \xrightarrow{4} v_3 \\ \tau^*(v_1) &= v_1 \xrightarrow{0} v_0 \quad ; \quad \tau^*(v_3) = v_3 \xrightarrow{-2} v_0 \quad ; \quad \tau^*(v_4) = v_4 \xrightarrow{-2} v_0. \end{aligned} $$

### Computing the values using a contracting fixed point

Let us consider a discounted payoff game $\mathcal{G}$ with $n$ vertices and weights in $[-W, W]$. We define $Y$ as $R \cup \{\pm\infty\}$, equipped with the natural total order on the reals. We let
$F_V$ be the lattice of functions $V \to Y$ equipped with the componentwise order induced by $Y$. We equip $F_V$ with the infinity norm: $||\mu|| = \max_{u \in V} |\mu(u)|$.

We define a function $\delta: Y \times [-W, W] \to Y$ by $\delta(x, w) = \lambda \cdot x + (1 - \lambda) \cdot w$. To understand the definition of $\delta$, the key observation is that the discounted payoff can be computed recursively:

$$ \begin{aligned} \text{DiscountedPayoff}(\rho) &= (1 - \lambda) \cdot \sum_{i=0}^{\infty} \lambda^i \rho_i \\ &= (1 - \lambda) \cdot \rho_0 + \lambda \cdot \text{DiscountedPayoff}(\rho_{\ge 1}). \end{aligned} $$

The function $\delta$ induces an operator $\mathcal{O}^{\mathcal{G}}: F_V \to F_V$:

$$ \mathcal{O}^{\mathcal{G}}(\mu)(u) = \begin{cases} \max \left\{ \delta(\mu(v), w) : u \xrightarrow{w} v \in E \right\} & \text{if } u \in V_{\text{Max}}, \\ \min \left\{ \delta(\mu(v), w) : u \xrightarrow{w} v \in E \right\} & \text{if } u \in V_{\text{Min}}. \end{cases} $$

We note that $\mathcal{O}^{\mathcal{G}}$ is a monotonic operator. Even more interesting, it is contracting:

**Fact 17.** The operator $\mathcal{O}^{\mathcal{G}}$ is contracting with contraction factor $\lambda$, meaning that for all $\mu, \mu' \in F_V$:

$$ \|\mathcal{O}^{\mathcal{G}}(\mu) - \mathcal{O}^{\mathcal{G}}(\mu')\| \le \lambda \cdot \|\mu - \mu'\|. $$

By Banach fixed point theorem, see Theorem 5, a direct consequence of this fact is that $\mathcal{O}^{\mathcal{G}}$ has a unique fixed point. The following theorem is the cornerstone of the study of discounted payoff games.

**Lemma 38** (Values as unique fixed point). The discounted payoff values are the unique fixed point of the operator $\mathcal{O}^{\mathcal{G}}$. Moreover, the unique fixed point induces a pair of optimal positional strategies:

$$ \begin{aligned} u \in V_{\text{Max}}: & \sigma(u) \in \operatorname*{argmax}\left\{\delta(\operatorname{val}^{\mathcal{G}}(v), w) : u \xrightarrow{w} v \in E\right\} \\ u \in V_{\text{Min}}: & \tau(u) \in \operatorname*{argmin}\left\{\delta(\operatorname{val}^{\mathcal{G}}(v), w) : u \xrightarrow{w} v \in E\right\}. \end{aligned} $$

*Proof.* Since we already know that $\mathcal{O}^{\mathcal{G}}$ has a unique fixed point, it is enough to show that $\operatorname{val}^{\mathcal{G}}$ is a fixed point of $\mathcal{O}^{\mathcal{G}}$. This follows from two properties, see Lemma 8:

* For all $\rho$ sequences of weights, we have

$$ \text{DiscountedPayoff}(w \cdot \rho) = \delta(\text{DiscountedPayoff}(\rho), w). $$

* The function $\delta$ is monotonic and continuous.

We now move to the second point: the values imply optimal positional strategies. Let us define $\sigma, \tau$ two positional strategies:

$$ \begin{aligned} u \in V_{\text{Max}}: & \sigma(u) \in \operatorname*{argmax}\left\{\delta(\operatorname{val}^{\mathcal{G}}(v), w) : u \xrightarrow{w} v \in E\right\} \\ u \in V_{\text{Min}}: & \tau(u) \in \operatorname*{argmin}\left\{\delta(\operatorname{val}^{\mathcal{G}}(v), w) : u \xrightarrow{w} v \in E\right\}. \end{aligned} $$

To show that $(\sigma, \tau)$ is a pair of optimal strategies, we claim that $\operatorname{val}^{\sigma} = \operatorname{val}^{\tau} = \operatorname{val}^{\mathcal{G}}$. Indeed, both $\operatorname{val}^{\sigma}$ and $\operatorname{val}^{\tau}$ are fixed points of $\mathcal{O}^{\mathcal{G}}$, and since there exists a unique fixed point the claim follows. $\square$
Let us illustrate the operator $\mathcal{O}^{\mathcal{G}}$ on the discounted payoff game of Figure 4.2. It is convenient to the contracting operator is:

$$ \mathcal{O}^{\mathcal{G}}(\mu)(v_0) = \max((1-\lambda) \cdot 4 + \lambda \cdot \mu(v_1), (1-\lambda) \cdot 5 + \lambda \cdot \mu(v_4)) $$

$$ \mathcal{O}^{\mathcal{G}}(\mu)(v_1) = \min((1-\lambda) \cdot 0 + \lambda \cdot \mu(v_0), (1-\lambda) \cdot 2 + \lambda \cdot \mu(v_2)) $$

$$ \mathcal{O}^{\mathcal{G}}(\mu)(v_2) = \max((1-\lambda) \cdot 1 + \lambda \cdot \mu(v_2), (1-\lambda) \cdot 4 + \lambda \cdot \mu(v_3)) $$

$$ \mathcal{O}^{\mathcal{G}}(\mu)(v_3) = \min((1-\lambda) \cdot (-2) + \lambda \cdot \mu(v_0), (1-\lambda) \cdot (-1) + \lambda \cdot \mu(v_1)) $$

$$ \mathcal{O}^{\mathcal{G}}(\mu)(v_4) = \min((1-\lambda) \cdot (-2) + \lambda \cdot \mu(v_0), (1-\lambda) \cdot 2 + \lambda \cdot \mu(v_4)) $$

A careful analysis gives the fixed points for all values of $\lambda \in (0,1)$, which in turn allows us to find the associated optimal positional strategies $\sigma^*$ and $\tau^*$ on the various intervals of values for $\lambda$, summarised in the following table:

<table><thead><tr><th>λ</th><th>(0, λ<sub>1</sub>]</th><th>(λ<sub>1</sub>, λ<sub>2</sub>]</th><th>(λ<sub>2</sub>, λ<sub>3</sub>]</th><th>(λ<sub>3</sub>, 1)</th></tr></thead><tbody><tr><th>σ<sup>*</sup>(v<sub>0</sub>)</th><td>ν<sub>4</sub></td><td>ν<sub>4</sub></td><td>ν<sub>1</sub></td><td>ν<sub>1</sub></td></tr><tr><th>τ<sup>*</sup>(v<sub>1</sub>)</th><td>ν<sub>0</sub></td><td>ν<sub>0</sub></td><td>ν<sub>0</sub></td><td>ν<sub>2</sub></td></tr><tr><th>σ<sup>*</sup>(v<sub>2</sub>)</th><td>ν<sub>3</sub></td><td>ν<sub>3</sub></td><td>ν<sub>3</sub></td><td>ν<sub>3</sub></td></tr><tr><th>τ<sup>*</sup>(v<sub>3</sub>)</th><td>ν<sub>0</sub></td><td>ν<sub>1</sub></td><td>ν<sub>1</sub></td><td>ν<sub>1</sub></td></tr><tr><th>τ<sup>*</sup>(v<sub>4</sub>)</th><td>ν<sub>0</sub></td><td>ν<sub>0</sub></td><td>ν<sub>0</sub></td><td>ν<sub>0</sub></td></tr></tbody></table>

The frontiers are at $\lambda_1 = 1 - \sqrt{2}/2 \approx 0.293$, $\lambda_2 = 1/2$, and $\lambda_3 \approx 0.841$. For instance, on interval $(0, \lambda_1]$, Min gets discounted payoff $\frac{5\lambda-2}{1+\lambda}$ when starting in vertex $v_3$, while switching his decision in interval $(\lambda_1, \lambda_2]$ allows him to secure $\frac{-2\lambda^3+6\lambda^2-1}{1+\lambda}$: this gives the explanation for the value of $\lambda_1$ which allows one to equal the two values. A similar reasoning provides the values of $\lambda_2$ and $\lambda_3$.

**Solving discounted payoff games is in NP ∩ coNP**

The first step in proving NP ∩ coNP upper bounds is to solve the one-player variants in polynomial time.

**Lemma 39 (One player discounted payoff games).** *There exists a polynomial time algorithm for computing the optimal values of one-player discounted payoff games.*

*Proof.* Let us consider a discounted payoff game where only Max has moves. We claim that $\text{val}^{\sigma}$ (seen as a vector $(x_u)_{u \in V}$) is the unique solution of the following linear program

$$ \begin{array}{ll} \text{maximise} & \sum_{u \in V} x_u \\ \text{subject to} & x_u \le (1-\lambda) \cdot w + \lambda x_v \quad \text{for } w \to c \in E, \end{array} $$

Indeed, vectors satisfying the constraints are exactly pre-fixed points of $\mathcal{O}^{\sigma}$, and since $\mathcal{O}^{\sigma}$ is monotonic the least fixed point of $\mathcal{O}^{\sigma}$ coincide with its least pre-fixed point. Linear programming can be solved in polynomial time, see Theorem 2.

A dual argument solves the case where only Min has moves. □

As for mean payoff (or parity) games, the existence of positional optimal (or winning) strategies for both players, and the ability to solve in polynomial time the one-player version of these games, allows us to obtain easily an NP ∩ coNP complexity to
solve discounted payoff games. The use of the above contracting operator even ensures that the Turing machines guessing and checking the optimal strategies may indeed be designed as unambiguous (instead of just non-deterministic). Calling UP the class of problems that can be solved by an unambiguous Turing machine running in polynomial time, and coUP the class of problems whose complement are in UP, we then obtain the theorem:

**Theorem 44 (Complexity).** *Solving discounted payoff games is in UP ∩ coUP.*

*Proof.* Using the previous result, we know that the value of a discounted payoff game is the unique solution of the fixed point equation $\mu = \mathcal{O}^{\mathcal{G}}(\mu)$. Therefore, guessing $\mu$ and checking it is indeed a fixed point of $\mathcal{O}^{\mathcal{G}}$ can be done by an unambiguous Turing machine. To ensure that the machine runs in polynomial time, it only remains to show that the solution is of polynomial size. Let us fix $\sigma, \tau$ a pair of positional optimal strategies. Let us rewrite the equation in a matrix form:

* We write $\vec{x}$ for a vector of values, $\vec{x} \in \mathbb{R}^V$.

* We define the matrix $Q \in \{0,1\}^{V \times V}$: the entry $Q_{u,v}$ is 1 if $u \in V_{\text{Min}}$ and $\sigma(u) = u \xrightarrow{w} v$ or $u \in V_{\text{Max}}$ and $\tau(u) = u \xrightarrow{w} v$, and 0 otherwise.

* We define the vector $\vec{c} \in \mathbb{Z}^V$: the entry $c_u$ is the weight of the edge $u \xrightarrow{w} v$ chosen by the strategies $\sigma$ and $\tau$.

With these notations, the equation rewrites

$$ \vec{x} = (1 - \lambda) \cdot \vec{c} + \lambda \cdot Q \cdot \vec{x}. $$

Letting $\lambda = a/b$ the rational discount factor, the above equation rewrites into

$$ A \cdot \vec{x} = (b-a) \cdot \vec{c} \qquad (4.1) $$

with $A = b \cdot I - a \cdot Q$ ($I$ being the identity matrix). Therefore, $A$ is a matrix that has at most two non-zero elements in each row: each of these non-zero elements can be written using at most $N = \max(\log_2 a, \log_2 b)$ bits (therefore polynomial in the representation of the game), and are therefore bounded in absolute value by $2^N$. By induction on the size of the matrix, we can then show that the determinant of $A$ is at most $4^{n \cdot N}$. The solution to Equation (4.1), using Cramer's formula, reads $x_v = \det(A_v)/\det(A)$ where $A_v$ is the matrix obtained from $A$ by replacing the $v$-th column with the vector $(b-a) \cdot \vec{c}$. Therefore, all components of $\vec{x}$ can be written with only a polynomial number of bits with respect to the size of the weights in the game and $N$.

The coUP membership follows, as in Theorem 39, from a dual reasoning for Min.

□

## A value iteration algorithm for discounted payoff games

Let us recall that thanks to Banach fixed point theorem, see Theorem 5, the fixed point is obtained as the limit of the following sequence:

$$ \forall u \in V, \mu_0(u) = 0 \ ; \ \mu_{k+1} = \mathcal{O}^{\mathcal{G}}(\mu_k). $$
We have $\lim_k \mu_k = \text{val}^{\mathcal{G}}$. To make sense of this sequence, let us define the following condition for each $k$:

$$ \text{DiscountedPayoff}_k(\rho) = (1 - \lambda) \cdot \sum_{i=0}^{k-1} \lambda^i \rho_i. $$

We define $\text{val}^{\mathcal{G},k}: V \to R \cup \{\pm\infty\}$ the value function by

$$ \text{val}^{\mathcal{G},k}(u) = \sup_{\sigma} \inf_{\tau} \text{DiscountedPayoff}_k[c](\pi_{it}^{\sigma, \tau}) $$

**Fact 18.** For all $k$, we have $\text{val}^{\mathcal{G},k} = \mu_k$.

The remaining question is therefore to design a rounding procedure to compute the exact values. The following lemma places bounds on the discounted payoff values, in a similar manner as for Corollary 8 for mean payoff.

**Lemma 40** (Upper bound on values in discounted payoff games). Let us write $\lambda = \frac{a}{b} \in (0, 1)$. The discounted payoff values are rational numbers in $[-W, W]$ whose denominators are at most $D = b^{n-1} \prod_{j=1}^{n} (b^j - a^j)$.

*Proof.* Let $\sigma, \tau$ a pair of optimal positional strategies. The corresponding play consists of a prefix of length at most $n$ and a simple cycle, hence the sequence of weights is:

$$ w_0, w_1, \dots, w_{k-1}, (w_k, \dots, w_l)^\omega, $$

with $k, l \le n$.

$$
\begin{align*}
\text{val}^{\mathcal{G}}(v) &= (1 - \lambda) \left[ \sum_{i=0}^{k-1} \lambda^i w_i + \lambda^k \sum_{m=0}^{\infty} \lambda^{(l-k+1)m} \sum_{i=0}^{l-k} \lambda^i w_{k+i} \right] \\
&= \frac{b-a}{b} \left[ \sum_{i=0}^{k-1} \frac{b^{k-1-i} a^i}{b^{k-1}} \cdot w_i + \frac{\lambda^k}{1 - \lambda^{l-k+1}} \sum_{i=0}^{l-k} \frac{b^{l-k-i} a^i}{b^{l-k}} \cdot w_{k+i} \right] \\
&= \frac{N_1}{b^k} + \frac{a^k b^{l-k+1}}{b^{k+1}(b^{l-k+1} - a^{l-k+1})} \frac{N_2}{b^{l-k}} \quad (\text{with } N_1, N_2 \in \mathbb{Z}) \\
&= \frac{N_3}{b^k (b^{l-k+1} - a^{l-k+1})} \quad (\text{with } N_3 \in \mathbb{Z}) \\
&= \frac{N}{b^{n-1} \prod_{j=1}^{n} (b^j - a^j)} \quad (\text{with } N \in \mathbb{Z})
\end{align*}
$$

□

It follows from Lemma 40 that if we have an approximation $\eta$ of $\text{val}^{\mathcal{G}}(v)$ such that $|\text{val}^{\mathcal{G}}(v) - \eta| < \frac{1}{2D}$, we can recover the value as $\text{val}^{\mathcal{G}}(v) = \frac{|D\eta + 1/2|}{D}$.

Let

$$ K = \left[ \frac{1}{-\log_2 \lambda} \left( \frac{n(n+3)}{2} \log_2 b + \log_2 W + 2 \right) \right] $$
**Lemma 41** (Number of steps of value iteration). For the value K above, we have
$$ \|F^K(\vec{0}) - val\| < \frac{1}{2D}. $$

*Proof.* First, we bound *D* by $b^{n+\frac{n(n+1)}{2}}$, so that $\frac{n(n+3)}{2}\log_2 b \ge \log_2 D$. Therefore $K \ge \frac{1}{-\log_2 \lambda}(\log_2 D + \log_2 W + \log_2 4) = \log_1/\lambda (4DW)$. This implies that $\lambda^K W \le \frac{1}{4D} < \frac{1}{2D}$.
Since $\mathcal{O}^\mathcal{G}$ is contracting with contraction factor $\lambda$, we have $\|F^K(\vec{0}) - val^\mathcal{G}\|_\infty \le \lambda^K$.
$\|val^\mathcal{G}\|_\infty$. Since $|val^\mathcal{G}(v)| \le W$, we obtain the desired inequality. $\square$

**Algorithm 4.4:** The value iteration algorithm for discounted payoff games.

**Data:** A discounted payoff game $\mathcal{G}$ with discount factor $\lambda = a/b \in (0, 1)$, and $F$ the contracting operator

for $u \in V$ do

$\lfloor \mu(u) \rfloor \leftarrow 0$

$K \leftarrow \left\lfloor \frac{1}{-\log_2 \lambda} \left( \frac{n(n+3)}{2} \log_2 b + \log_2 W + 2 \right) \right\rfloor$;

for $i = 1$ to $K$ do

$\lfloor \mu \rfloor \leftarrow \mathcal{O}^{\mathcal{G}}(\mu)$

return $\mu$

**Theorem 45** (Value iteration algorithm for discounted payoff games). There exists a value iteration algorithm computing in pseudo-polynomial time the discounted payoff values.

One can check that *K* is polynomial in the size of the arena, but not in the discount factor λ. Indeed, consider that λ = 1 - 1/b, with b ∈ N \ {0}. Then, we may store λ with log₂ b bits, yet (1/(-log₂λ)) ~ b~to~∞ b * ln2 is exponential in log₂ b. As a consequence, the value iteration algorithm runs in pseudo-polynomial time.

**Strategy improvement algorithm for discounted payoff games**

**Theorem 46** (Strategy improvement for discounted payoff games). There exists a strategy improvement algorithm computing the discounted payoff values in exponential time.

We construct a strategy improvement algorithm, following the presentation in Section 1.10. Let us consider a (positional) strategy $\sigma$ for Max. We compute $val^\sigma$ (for instance by solving a linear program as in Lemma 39). Now there are two cases:

* Either $val^\sigma = \mathcal{O}^\mathcal{G}(val^\sigma)$, in which case we have found a fixed point of $\mathcal{O}^\mathcal{G}$. By uniqueness, this is the discounted payoff values, and $\sigma$ is an optimal strategy for Max.

* Or $val^\sigma \neq \mathcal{O}^\mathcal{G}(val^\sigma)$, in which case we need to improve the strategy $\sigma$.