Games on Graphs

Nathanaël Fijalkow, Nathalie Bertrand, Patricia Bouyer, Romain Brenguier, Arnaud Carayol, John Fearnley, Hugo Gimbert, Florian Horn, Rasmus Ibsen-Jensen, Nicolas Markey, et al.

► To cite this version:

Nathanaël Fijalkow (Dir.). Games on Graphs. pp.1-491, inPress, 10.48550/arXiv.2305.10546 . hal-04273394

HAL Id: hal-04273394

https://hal.science/hal-04273394v1

Submitted on 9 Nov 2023

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

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

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

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
# Games on Graphs
(version 1)

Nathalie Bertrand

Patricia Bouyer-Decitre

Romain Brenguier

Arnaud Carayol

John Fearnley

Nathanaël Fijalkow

Hugo Gimbert

Florian Horn

Rasmus Ibsen-Jensen

Nicolas Markey

Benjamin Monmege

Petr Novotný

Mickael Randour

Ocan Sankur

Sylvain Schmitz

Olivier Serre

Mateusz Skomra

Coordinated by Nathanaël Fijalkow
GAMES ON
GRAPHS

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

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

## What is this book about?

The objective of this book is to present the state of the art on games on graphs, which is part of a larger research topic called game theory. Games on graphs is the field concerned with games whose rules and evolution are represented by a graph. We mostly focus on infinite duration games, but their study is deeply interleaved with finite duration games. They form a prominent model in two related subjects: the first is automata theory and logic, and the second is verification and synthesis, both of which have been very active for decades. Some of the models were introduced and studied in neighbouring research communities such as optimisation, reinforcement learning, model theory, and set theory.

This book does not claim to give a full account of all existing results or models in the literature, which is close to impossible for two reasons: the wealth of existing results and the constant flow of new ones.

The primary objective in this book is algorithmic: constructing efficient algorithms for analysing different types of games. Yet the goal is not to describe their implementation in full details but rather to explain their theoretical foundations. In this endeavour we often need to set the stage by proving properties of the corresponding games and most prominently of their winning strategies. So the language of this book is mathematics.

This book owes a lot to two reference textbooks on games: Automata, Logics, and Infinite Games: A Guide to Current Research, edited by Erich Grädel, Wolfgang Thomas, and Thomas Wilke [GTW02], and Lectures in Game Theory for Computer Scientists, edited by Krzysztof R. Apt and Erich Grädel [AG11].

## How to read

All the material presented in this book is accessible to an advanced master student or a PhD student with a background in computer science or mathematics. The goal is at the same time to present all the basic and fundamental results commonly assumed by
the research community working on games on graphs, and most of the latest prominent advances. We assume familiarity with complexity theory and the notions of graphs and automata but as much as possible do not rely on advanced results in these fields.

The book is divided in five parts each including two or three chapters. At the end of each chapter is a section dedicated to bibliographic references. Chapter 1 introduces some notations and notions used throughout the book. After that and to some extent each part is independent. As much as possible we avoid back references but some chapters naturally build on the previous ones in which case we clearly indicate this.

## How to cite

To cite the whole book, here is a bib item.

```json
@book{gamesbook,
  title = {Games on Graphs},
  author = {Nathanaël Fijalkow and
    Nathalie Bertrand and
    Patricia Bouyer-Decitre and
    Romain Brenguier and
    Arnaud Carayol and
    John Fearnley and
    Hugo Gimbert and
    Florian Horn and
    Rasmus Ibsen-Jensen and
    Nicolas Markey and
    Benjamin Monmege and
    Petr Novotný and
    Mickael Randour and
    Ocan Sankur and
    Sylvain Schmitz and
    Olivier Serre and
    Mateusz Skomra},
  editor = {Nathanaël Fijalkow},
  publisher = {Online},
  date = {2023},
}
```

If you wish to only cite one chapter, here is an example.

```json
@InCollection{timedgameschapter,
  title = {Timed Games},
  author = {Nicolas Markey, Ocan Sankur},
  booktitle = {Games on Graphs},
  editor = {Nathanaël Fijalkow},
  year = {2023}
}
```
## Acknowledgements

The following people have contributed to early versions of the book in different ways, we thank them warmly for their comments, suggestions, discussions, bug fixes and reports: Antonio Casares, Hugo Francon, Pierre Gaillard, Théo Matricon, Rémi Morvan, Damian Niwiński, Pierre Ohlmann.

Please send any comments (including typos) you may have to

nathanael.fijalkow@gmail.com,

or directly to the relevant authors.

## Versions

A full version of the book is available on ArXiv. The current document is version 1. A printed published version will be considered at a later point. An online HTML version is under preparation.

## Illustrations

The illustrations (cover and each chapter) were realised by Podpunkt:

http://podpunkt.pl/
# Contents

## Preface 3

## 1 Introduction 13

NATHANAËL FIJALKOW

1.1 A first model of games 14

1.2 Computational models 25

1.3 Objectives 27

1.4 Automata 33

1.5 Memory 34

1.6 Reductions 38

1.7 Traps and subgames 40

1.8 Generic fixed point algorithms 41

1.9 Value iteration algorithms 42

1.10 Strategy improvement algorithms 48

## I Classic 55

## 2 Regular Games 59

NATHANAËL FIJALKOW, FLORIAN HORN

2.1 Reachability games 59

2.2 Büchi games 64

2.3 Parity games 68

2.4 Proving half-positional determinacy for qualitative games 71

2.5 Rabin, Streett, and Muller games 72

2.6 Zielonka tree 80

## 3 Parity Games 93
JOHN FEARNLEY, NATHANAËL FIJALKOW

<table><tr><td>3.1</td><td>An exponential time strategy improvement algorithm</td><td>94</td></tr><tr><td>3.2</td><td>A quasi-polynomial time attractor decomposition algorithm</td><td>99</td></tr><tr><td>3.3</td><td>A quasi-polynomial time separating automata algorithm</td><td>104</td></tr><tr><td>3.4</td><td>A quasi-polynomial time value iteration algorithm</td><td>112</td></tr><tr><td>3.5</td><td>Comparing the three families of algorithms</td><td>123</td></tr></table>

4 **Games with Payoffs** **131**

NATHANAËL FIJALKOW, BENJAMIN MONMEGE

<table><tr><td>4.1</td><td>Proving positional determinacy over finite arenas</td><td>132</td></tr><tr><td>4.2</td><td>Refining qualitative objectives with quantities</td><td>137</td></tr><tr><td>4.3</td><td>Mean payoff games</td><td>138</td></tr><tr><td>4.4</td><td>Discounted payoff games</td><td>152</td></tr><tr><td>4.5</td><td>Shortest path games</td><td>163</td></tr><tr><td>4.6</td><td>Total payoff games</td><td>168</td></tr></table>

II **Stochastic** **173**

5 **Markov Decision Processes** **177**

PETR NOVOTNÝ

<table><tr><td>5.1</td><td>Positive and almost-sure reachability and safety in MDPs</td><td>182</td></tr><tr><td>5.2</td><td>Discounted payoff in MDPs</td><td>188</td></tr><tr><td>5.3</td><td>Mean payoff in MDPs: General properties and linear programming</td><td>196</td></tr><tr><td>5.4</td><td>Mean payoff optimality in strongly connected MDPs</td><td>199</td></tr><tr><td>5.5</td><td>End components</td><td>207</td></tr><tr><td>5.6</td><td>Reductions to optimal reachability</td><td>209</td></tr><tr><td>5.7</td><td>Optimal reachability</td><td>215</td></tr></table>

6 **Stochastic Games** **221**

NATHALIE BERTRAND, PATRICIA BOUYER-DECITRE, NATHANAËL FIJALKOW, MATEUSZ SKOMRA

<table><tr><td>6.1</td><td>Fixed point characterisation and positional determinacy</td><td>223</td></tr><tr><td>6.2</td><td>Normalisation: stopping, binary, simple</td><td>228</td></tr><tr><td>6.2.1</td><td>Normalised games</td><td>228</td></tr><tr><td>6.2.2</td><td>Simple stochastic games</td><td>231</td></tr><tr><td>6.2.3</td><td>Stopping games</td><td>232</td></tr><tr><td>6.3</td><td>A value iteration algorithm</td><td>236</td></tr><tr><td>6.4</td><td>A strategy improvement algorithm</td><td>237</td></tr><tr><td>6.5</td><td>Algorithms based on permutations of random vertices</td><td>241</td></tr><tr><td>6.6</td><td>Reductions to simple stochastic games</td><td>246</td></tr><tr><td>6.6.1</td><td>From discounted payoff games to stochastic reachability games</td><td>246</td></tr><tr><td>6.6.2</td><td>From stochastic mean payoff games to stochastic discounted payoff games</td><td>247</td></tr><tr><td>6.6.3</td><td>From stochastic parity to stochastic mean payoff</td><td>247</td></tr></table>
III Information 251

7 Concurrent Games 255

RASMUS IBSEN-JENSEN

7.1 Notations 256

7.2 Matrix games 257

7.3 Concurrent discounted payoff games 258

7.4 Concurrent reachability games 265

7.5 Concurrent mean payoff games 274

8 Games with Signals 281

HUGO GIMBERT

8.1 Notations 282

8.2 Finite duration 285

8.2.1 Existence and computability of the value 286

8.2.2 The Koller-Meggido-von Stengel reduction to linear programming 288

8.3 Infinite duration 291

8.3.1 Playing games with infinite duration and imperfect information 291

8.3.2 The value problem. 292

8.3.3 Winning with probability 1 or > 0 293

8.3.4 Qualitative determinacy: proof of Theorem 96 294

8.3.5 Decidability: proof of Theorem 97 and Theorem 98 299

IV Infinite 305

9 Timed Games 309

NICOLAS MARKEY, OCAN SANKUR

9.1 Notations 310

9.2 State-Space Representation 312

9.3 Controllable-Predecessor Operator 315

9.4 Backward Algorithm 316

9.5 Forward Algorithm 317

10 Pushdown Games 327

ARNAUD CARAYOL, OLIVIER SERRE

10.1 Notations 327

10.2 Profiles and regularity of the winning regions 330

10.2.1 Reachability Pushdown Game 333

10.3 Parity pushdown games 334

10.3.1 Computing the Profiles 335

10.3.2 Solving the Game and Computing the Winning Region and Strategy 344

10.3.3 Pushdown and Regular Winning Strategies 346
11 Games with Counters 355

SYLVAIN SCHMITZ

<table><tbody><tr><td>11.1</td><td>Vector games</td><td>356</td></tr><tr><td>11.1.1</td><td>Arenas and Games</td><td>357</td></tr><tr><td>11.1.2</td><td>Undecidability</td><td>361</td></tr><tr><td>11.2</td><td>Games in dimension one</td><td>363</td></tr><tr><td>11.2.1</td><td>Countdown Games</td><td>363</td></tr><tr><td>11.2.2</td><td>Vector Games in Dimension One</td><td>366</td></tr><tr><td>11.3</td><td>Asymmetric games</td><td>367</td></tr><tr><td>11.3.1</td><td>The Case of Configuration Reachability</td><td>367</td></tr><tr><td>11.3.2</td><td>Asymmetric Monotone Games</td><td>370</td></tr><tr><td>11.4</td><td>Resource-conscious games</td><td>375</td></tr><tr><td>11.4.1</td><td>Energy Semantics</td><td>376</td></tr><tr><td>11.4.2</td><td>Bounded Semantics</td><td>378</td></tr><tr><td>11.5</td><td>The complexity of asymmetric monotone games</td><td>381</td></tr><tr><td>11.5.1</td><td>Upper Bounds</td><td>381</td></tr><tr><td>11.5.2</td><td>Lower Bounds</td><td>386</td></tr><tr><td>11.5.3</td><td>Dimension One</td><td>391</td></tr></tbody></table>

V Multi 395

12 Games with multiple objectives 399

MICKAEL RANDOUR

<table><tbody><tr><td>12.1</td><td>From one to multiple dimensions</td><td>400</td></tr><tr><td>12.2</td><td>Mean payoff and energy</td><td>402</td></tr><tr><td>12.2.1</td><td>Finite memory</td><td>403</td></tr><tr><td>12.2.2</td><td>Infinite memory</td><td>404</td></tr><tr><td>12.3</td><td>Total payoff and shortest path</td><td>410</td></tr><tr><td>12.3.1</td><td>Total payoff vs. mean payoff</td><td>410</td></tr><tr><td>12.3.2</td><td>Undecidability</td><td>412</td></tr><tr><td>12.4</td><td>Beyond worst-case synthesis</td><td>414</td></tr><tr><td>12.4.1</td><td>The decision problem</td><td>414</td></tr><tr><td>12.4.2</td><td>The approach in a nutshell</td><td>416</td></tr><tr><td>12.5</td><td>Percentile queries</td><td>429</td></tr><tr><td>12.5.1</td><td>An additional leap in complexity</td><td>429</td></tr><tr><td>12.5.2</td><td>Complexity overview</td><td>432</td></tr></tbody></table>

13 Multiplayer Games 439

ROMAIN BRENGUIER, OCAN SANKUR

<table><tbody><tr><td>13.1</td><td>Nash Equilibria for games in normal form</td><td>440</td></tr><tr><td>13.1.1</td><td>Definitions</td><td>442</td></tr><tr><td>13.1.2</td><td>The Nash equilibrium problem</td><td>443</td></tr><tr><td>13.1.3</td><td>Deviators</td><td>444</td></tr><tr><td>13.1.4</td><td>Deviator Game</td><td>445</td></tr><tr><td>13.1.5</td><td>Extensions of Nash Equilibria</td><td>450</td></tr></tbody></table>
CONTENTS

11

<table><tr><td>13.2 Admissible strategies</td><td>453</td></tr><tr><td>13.2.1 Definition</td><td>454</td></tr><tr><td>13.2.2 Simple Safety games</td><td>455</td></tr><tr><td>13.2.3 Parity games</td><td>457</td></tr><tr><td>13.2.4 Iterated elimination</td><td>458</td></tr></table>

Conclusions

461
INTRO
DUCTION

<figure><img src="image_4.png" /></figure>
Chapter 1

# Introduction

NATHANAËL FIJALKOW

Section 1.1 defines a first model of games, which is the common denominator of (almost all) models studied in this book. We introduce the computational models that we use in Section 1.2 and briefly discuss linear programming. In Section 1.3 we list the main objectives appearing in all chapters. A few notions will be useful throughout the book: they are developed in this chapter. We start with the notion of automata, discussed in Section 1.4, and then memory for strategies in Section 1.5. We then show how automata and memory structures can be used to construct reductions between games in Section 1.6. We introduce in Section 1.7 the notions of subgames and traps.

The notion of fixed point algorithms is central to the study of games. We first recall the main two methods for proving the existence and computing fixed points in Section 1.8. We then give an overview of two prominent families of fixed point algorithms for games: value iteration algorithms in Section 1.9 and strategy improvement algorithms in Section 1.10.

## Usual notations

We write $[i, j]$ for the interval $\{i, i+1, \dots, j-1, j\}$, and use parentheses to exclude extremal values, so $[i, j)$ is $\{i, i+1, \dots, j-1\}$.

An alphabet $\Sigma$ is a finite set. We let $\Sigma^*$ denote the set of finite sequences of $\Sigma$ (also called finite words), $\Sigma^+$ the subset of non-empty sequences, and $\Sigma^\omega$ the set of infinite sequences of $\Sigma$ (also called infinite words). For a (finite or infinite) sequence $u = u_0u_1\cdots$, we let $u_i$ denote the $i^{th}$ element of $u$ and $u\leq i$ the prefix of $u$ of length $i$, i.e. the finite sequence $u_0u_1\cdots u_{i-1}$. Similarly $u\leq i = u_0u_1\cdots u_i$. The length of $u$ is $|u|$.
## 1.1 A first model of games

The first model we define is the common denominator of most models studied in this book:

* 2-player,

* zero sum,

* turn based,

* deterministic,

* perfect information

game.

### Players

The term 2-player means that there are two players. Many, many different names have been used: Eve and Adam, Player 0 and Player 1, Player I and Player II as in descriptive complexity, Éloïse and Abélard, Circle and Square, corresponding to the graphical representation, Even and Odd, mostly for parity objectives, Player and Opponent, Pathfinder and Verifier in the context of automata, Min and Max, which makes sense for quantitative objectives, and this is only a very partial list of names they have been given. In the names Eve and Adam, the first letters refer to ∃ and ∀ suggesting a duality between them. We will use the pronouns she/her for Eve and he/him for Adam, so we can speak of her or his strategy. In this book, we will use Eve and Adam in qualitative contexts (win / lose), and Min and Max in quantitative contexts.

We speak of 1-player games when there is only one player. In the context of stochastic games, we refer to random as a third player, and more precisely as half a player. Hence a 2$^{1/2}$-player game is a stochastic game with two players, and a 1$^{1/2}$-player game is a stochastic game with one player.

The situation where there are more than two players is called multiplayer games.

### Graphs

A (directed) graph is given by a set V of vertices and a set E of edges given by the functions In, Out : E → V : for an edge e we write In(e) for the incoming vertex and Out(e) for the outgoing vertex. We say that e is an outgoing edge of In(e) and an incoming edge to Out(e). To introduce an edge, it is convenient to write e = v → v' to express that v = In(e) and v' = Out(e). A path π is a finite or infinite sequence:

$$ \pi = v_0 \to v_1 \to v_2 \dots $$

We let first(π) denote the first vertex occurring in π and last(π) the last one if π is finite. We say that π starts from first(π) and if π is finite that π ends in last(π). We write π≤i for the finite path v_0 → v_1 → \dots → v_i. We sometimes talk of a path and let the context determine whether it is finite or infinite.
We let $Paths(G)$ denote the set of finite paths in the graph $G$, sometimes omitting $G$ when clear from the context. To restrict to paths starting from $v$ we write $Paths(G, v)$. The set of infinite paths is $Paths_\omega(G)$, and $Paths_\omega(G, v)$ for those starting from $v$. We naturally see sets of infinite paths as subsets of $E^\omega$.

We use the standard terminology of graphs: for instance a vertex $v'$ is a successor of $v$ if there exists $e \in E$ such that $\mathrm{In}(e) = v$ and $\mathrm{Out}(e) = v'$, and then $v$ is a predecessor of $v'$, a vertex $v'$ is reachable from $v$ if there exists a path starting from $v$ and ending in $v'$, the outdegree of a vertex is its number of outgoing edges, the indegree is its number of incoming edges, a simple path is a path with no repetitions of vertices, a cycle is a path whose first and last vertex coincide, it is a simple cycle if it does not strictly contain another cycle, a self loop is an edge from a vertex to itself, and a sink is a vertex with only self loops as outgoing edges.

**Remark 1** (Edges as subsets of pairs of vertices). *Our definition with $\mathrm{In}, \mathrm{Out} : E \to V$ includes graphs where there can be multiple edges between a single pair of vertices. Although this can be useful in some cases, we will also sometimes simply define the set of edges as $E \subseteq V \times V$, which implies that an edge is fully determined by incoming and outgoing vertices.*

## Arenas

The *arena* is the place where the game is played, they have also been called game structures or game graphs.

In the turn based setting we define here, the set of vertices is divided into vertices controlled by each player. Since we are for now interested in 2-player games, we have $V = V_{\text{Eve}} \uplus V_{\text{Adam}}$, where $V_{\text{Eve}}$ is the set of vertices controlled by Eve and $V_{\text{Adam}}$ the set of vertices controlled by Adam. We represent vertices in $V_{\text{Eve}}$ by circles, and vertices in $V_{\text{Adam}}$ by squares, and also say that $v \in V_{\text{Eve}}$ belongs to Eve, or that Eve owns or controls $v$, and similarly for Adam. An arena is given by a graph and the sets $V_{\text{Eve}}$ and $V_{\text{Adam}}$. In the context of games, vertices are often referred to as positions.

We adapt the notations to $V = V_{\text{Min}} \uplus V_{\text{Max}}$ if the players are Min and Max. Circles are controlled by Max and squares by Min.

The adjective *finite* means that the arena is finite, i.e. there are finitely many vertices and edges. We oppose *deterministic* to *stochastic*: in the first definition we are giving here, there is no stochastic aspect in the game. An important assumption, called *perfect information*, says that the players see everything about how the game is played out, in particular they see the other player's moves.

We assume that all vertices have an outgoing edge. This is for technical convenience, as it implies that we do not need to explain what happens when a play cannot be prolonged.

## Playing

The interaction between the two players consists in moving a token on the vertices of the arena. The token is initially on some vertex. When the token is in some vertex $v$,
<figure><img src="image_5.png" /><figcaption>Figure 1.1: An example of an arena. In a qualitative context, circles are controlled by Eve and squares by Adam, and in a quantitative context circles are controlled by Max and squares by Min.</figcaption></figure>

the player who controls the vertex chooses an edge $e = v \to v'$ and pushes the token along this edge to the next vertex $v'$. The outcome of this interaction is the sequence of vertices and edges traversed by the token: it is a path. In the context of games a path is also called a *play* and as for paths usually written $\pi$. We note that plays can be finite (but non empty) or infinite.

## Strategies

The most important notion in this book is that of *strategies* (sometimes called policies). A strategy for a player is a full description of his or her moves in all situations. Formally, a *strategy* is a function mapping finite plays to edges:

$$ \sigma: \text{Paths} \to E. $$

**Convention 1.** We use $\sigma$ for strategies of Eve and Max, and $\tau$ for strategies of Adam and Min, so when considering a strategy $\sigma$ it is implicitly for Eve or Max, and similarly $\tau$ is implicitly a strategy for Adam or Min.

We say that a play $\pi = v_0 \to v_1 \to \dots$ is consistent with a strategy $\sigma$ of Eve if for all $i$ such that $v_i \in V_{Eve}$ we have $\sigma(\pi_{\le i}) = v_i \to v_{i+1}$. The definition is easily adapted for strategies of Adam.

Once an initial vertex $v$ and two strategies $\sigma$ and $\tau$ have been fixed, there exists a unique infinite play starting from $v$ and consistent with both strategies, it is written $\pi_{\sigma, \tau}$. Note that the fact that it is infinite follows from our assumption that all vertices have an outgoing edge.

## Conditions

The last ingredient to wrap up the definitions is (winning) *conditions*, which is what Eve wants to achieve. There are two types of conditions: the *qualitative*, or Boolean ones, and the *quantitative* ones.

A *qualitative condition* is $W \subseteq \text{Paths}_\omega$: it separates winning from losing plays, in other words a play which belongs to $W$ is winning and otherwise it is losing. We also say that the play satisfies $W$.
A quantitative condition is $f: \text{Paths}_\omega \to \mathbb{R} \cup \{\pm\infty\}$: it assigns a real value (or plus or minus infinity) to a play, which can be thought of as a payoff or a score. More generally, we sometimes consider quantitative conditions of the form $f: \text{Paths}_\omega \to \mathbb{Y}$ with $\mathbb{Y}$ a totally ordered set.

Often we define $W$ as a subset of $E^\omega$ and $f$ as $f: E^\omega \to \mathbb{R} \cup \{\pm\infty\}$, since $\text{Paths}_\omega$ is included in $E^\omega$.

## Objectives

To reason about classes of games with the same conditions, we introduce the notions of objectives and colouring functions. An objective and a colouring function together induce a condition. The main point is that objectives are independent of the arenas, so we can speak of the class of conditions induced by a given objective, and by extension a class of games induced by a given objective, for instance parity games.

We fix a set $C$ of colours. A qualitative objective is $\Omega \subseteq C^\omega$, and a quantitative objective is a function $\Phi: C^\omega \to \mathbb{R} \cup \{\pm\infty\}$.

## Colouring functions

The link between an arena and an objective is given by a colouring function $c: E \to C$ labelling edges of the graph by colours. We extend $c$ componentwise to induce $c$: $\text{Paths}_\omega \to C^\omega$ mapping plays to sequences of colours:

$$c(e_0 e_1 \dots) = c(e_0) c(e_1) \dots$$

A qualitative objective $\Omega$ and a colouring function $c$ induce a qualitative condition $\Omega(c)$ defined by:

$$\Omega(c) = \{\pi \in \text{Paths}_\omega : c(\pi) \in \Omega\}.$$

When $c$ is clear from the context we sometimes say that a play $\pi$ satisfies $\Omega$ but the intended meaning is that $\pi$ satisfies $\Omega(c)$, equivalently that $c(\pi) \in \Omega$.

Similarly, a quantitative objective $\Phi: C^\omega \to \mathbb{R} \cup \{\pm\infty\}$ and a colouring function $c$ induce a quantitative condition $\Phi(c): \text{Paths}_\omega \to \mathbb{R} \cup \{\pm\infty\}$ defined by:

$$\Phi(c)(\pi) = \Phi(c(\pi)).$$

We extend the notation $v \to v'$ in the presence of a colouring function: $e = v \stackrel{c}{\to} v'$ further indicates that $c(e) = c$. As we will see, a convenient abuse of notations consists in identifying a colour $c$ and the set of edges of that colour $c^{-1}(c)$.

## Games

We can now give the following definitions.

### Definition 1 (Games).

* A graph is a tuple $G = (V, E, \text{In}, \text{Out})$ where $V$ is a set of vertices, $E$ is a set of edges, and $\text{In}, \text{Out}: E \to V$ define the incoming and outgoing vertices of edges.
* An arena is a tuple $\mathcal{A} = (G, V_{\text{Eve}}, V_{\text{Adam}})$ where $G$ is a graph over the set of vertices $V$ and $V = V_{\text{Eve}} \uplus V_{\text{Adam}}$. In a quantitative context we use $V = V_{\text{Min}} \uplus V_{\text{Max}}$.

* A colouring function is a function $c : E \to C$ where $C$ is a set of colours.

* A qualitative condition is $W \subseteq \text{Paths}_\omega$.

* A qualitative objective is a subset $\Omega \subseteq C^\omega$. A colouring function $c$ and a qualitative objective $\Omega$ induce a qualitative condition $\Omega(c)$.

* A qualitative game $\mathcal{G}$ is a tuple $(\mathcal{A}, W)$ where $\mathcal{A}$ is an arena and $W$ a qualitative condition.

* A quantitative condition is $f : \text{Paths}_\omega \to \mathbb{R} \cup \{\pm\infty\}$.

* A quantitative objective $\Phi$ is a function $\Phi : C^\omega \to \mathbb{R} \cup \{\pm\infty\}$. A colouring function $c$ and a quantitative objective $\Phi$ induce a quantitative condition $\Phi(c)$.

* A quantitative game $\mathcal{G}$ is a tuple $(\mathcal{A}, f)$ where $\mathcal{A}$ is an arena and $f$ a quantitative condition.

To be specific, the definition above is for 2-player zero sum turn based deterministic perfect information games. As a convention we use the condition to qualify games, so for instance parity games are games equipped with a parity condition. This extends to graphs: we speak of a graph with condition $W$ for a graph equipped with a condition $W$, and for instance a mean payoff graph if $W$ is a mean payoff condition.

We often introduce notations implicitly: for instance when we introduce a qualitative game $\mathcal{G}$ without specifying the arena and the condition, it is understood that the arena is $\mathcal{A}$ and the condition $W$.

We always implicitly take the point of view of Eve. Since we consider zero sum games we can easily reverse the point of view by considering the qualitative game $(\mathcal{A}, \text{Paths}_\omega \setminus W)$ and the quantitative game $(\mathcal{A}, -f)$. Indeed for the latter minimising $f$ is equivalent to maximising $-f$. The term zero sum comes from this: the total outcome for the two players is $f + (-f)$, meaning zero.

We sometimes speak of a coloured graphs or a coloured arena when attaching a colouring function to a graph or an arena.

**Remark 2 (Finite graphs).** Unless otherwise stated we assume that graphs are finite, meaning that there are finitely many vertices and finitely many edges. We equivalently say that the arena or the game is finite. Part IV will study games over infinite graphs.

## Labelling edges or vertices

In our definition the colouring function labels edges: $c : C \to E$, and infinite paths are infinite sets of edges. It is sometimes convenient to label vertices instead: $c : C \to V$, and in some cases it may feel more natural: for instance for reachability conditions (to be defined in Section 1.3), the target is naturally a set of vertices rather than a set of edges. But labelling edges is often technically easier, and more succinct, so it is the
preferred convention in this book. There is a third option: labelling vertices with partial colouring functions, i.e. allowing some vertices to remain uncoloured. To keep things well defined, in that case we make the assumption that every path contains infinitely many coloured vertices. There are two consequences to the convention of labelling edges or vertices: the complexity of algorithms, and the memory requirements, both (often) mildly affected by the choice.

Let us state simple and general reduction results between the three conventions. Clearly,

vertex labelling $\subseteq$ partial vertex labelling $\subseteq$ edge labelling.

Indeed, to go from (partial) vertex labelling to edge labelling it is enough to define $c'(e) = c(\mathrm{In}(e))$: the colour of an edge is the colour of its incoming vertex. A path induces the same sequence of colours for both $c$ and $c'$, implying a strong equivalence between the two games.

Conversely, we can reduce from edge labelling to partial vertex labelling:

**Lemma 1** (From labelling edges to labelling vertices). Let $G$ a graph with $n$ vertices and $m$ edges, $c: E \to C$ an edge colouring function, we define a graph $G'$ with $n+m$ vertices and $2m$ edges and a partial vertex colouring function $c': V' \to C$ such that there is a one to one correspondence between infinite paths in $G$ coloured by $c$ and infinite paths in $G'$ coloured by $c'$.

As a consequence, an algorithm using edge colouring functions of complexity $T(n,m)$ induces an algorithm for partial vertex colouring functions of complexity $T(n+m, 2m)$.

*Proof.* We add edges as intermediate vertices. Both the sets of vertices and of edges of $G'$ are (disjoint copies of) $V \cup E$. For each edge $e = v \to v'$ of $G$, we add two edges in $G'$: one from $v$ to $e$, and one from $e$ to $v'$. The colouring function $c'$ is defined only on $E$ by $c'(e) = c(e)$. The construction is illustrated in Figure 1.2. Infinite paths in $G$ and in $G'$ are in one to one correspondence, and the sequences of colours are the same, since colours appear exactly every second position in every infinite path of $G'$. $\square$

<figure><img src="image_6.png" /><figcaption>Figure 1.2: Reduction from edge colouring to vertex colouring.</figcaption></figure>

There are no easy reductions from partial vertex labelling to vertex labelling, but in most cases an ad-hoc simple trick proves the two conventions to be (essentially) equivalently. For instance, of the objective contains a neutral letter, then the construction above can be replicated: for an objective $\Omega \subseteq C^\omega$, we say that $\epsilon \in C$ is a neutral letter if for all $\rho \in C^\omega$, let $\rho_\epsilon$ the sequence obtained from $\rho$ by removing all $\epsilon$, then $\rho \in \Omega$ if and only if $\rho_\epsilon$ is finite or in $\Omega$.
## Winning in qualitative games

Now that we have the definitions of a game we can ask the main question: given a game $\mathcal{G}$ and a vertex $v$, who wins $\mathcal{G}$ from $v$?

Let $\mathcal{G}$ be a qualitative game and $v$ a vertex. A strategy $\sigma$ for Eve is called *winning* from $v$ if every play starting from $v$ consistent with $\sigma$ is winning, i.e. satisfies $W$. Another common terminology is that $\sigma$ ensures $W$. In that case we say that Eve has a winning strategy from $v$ in $\mathcal{G}$, or equivalently that Eve wins $\mathcal{G}$ from $v$. This vocabulary also applies to Adam: for instance a strategy $\tau$ for Adam is called *winning* from $v$ if every play starting from $v$ consistent with $\tau$ is losing, i.e. does not satisfy $W$.

We let $W_{\text{Eve}}(\mathcal{G})$ denote the set of vertices $v$ such that Eve wins $\mathcal{G}$ from $v$, it is called *winning region*, or sometimes winning set. A vertex in $W_{\text{Eve}}(\mathcal{G})$ is said winning for Eve. The analogous notation for Adam is $W_{\text{Adam}}(\mathcal{G})$.

We say that a strategy is *optimal* if it is winning from all vertices in $W_{\text{Eve}}(\mathcal{G})$.

**Fact 1 (Winning regions are disjoint).** For all qualitative games $\mathcal{G}$ we have $W_{\text{Eve}}(\mathcal{G}) \cap W_{\text{Adam}}(\mathcal{G}) = \emptyset$.

*Proof.* Assume for the sake of contradiction that both players have a winning strategy from $v$, then $\pi_{\sigma, \tau}^v$ would both satisfy $W$ and not satisfy $W$, a contradiction. $\square$

It is however not clear that for every vertex $v$, some player has a winning strategy from $v$, which symbolically reads $W_{\text{Eve}}(\mathcal{G}) \cup W_{\text{Adam}}(\mathcal{G}) = V$. One might imagine that if Eve picks a strategy, then Adam can produce a counter strategy beating Eve's strategy, and vice versa, if Adam picks a strategy, then Eve can come up with a strategy winning against Adam's strategy. A typical example would be rock-paper-scissors (note that this is a concurrent game, meaning the two players play simultaneously, hence it does not match the definitions given so far), where neither player has a winning strategy.

Whenever $W_{\text{Eve}}(\mathcal{G}) \cup W_{\text{Adam}}(\mathcal{G}) = V$, we say that the game is *determined*. Being determined can be understood as follows: the outcome can be determined before playing assuming both players play optimally, since one of them can ensure to win whatever is the strategy of the opponent.

**Theorem 1 (Borel determinacy).** Qualitative games with Borel conditions are determined.

The definition of Borel sets goes beyond the scope of this book. Suffice to say that all conditions studied in this book are (very simple) examples of Borel sets, implying that our qualitative games are all determined (as long as we consider perfect information and turn based games, the situation will change with more general models of games).

## Computational problems for qualitative games

We identify three computational problems. The first is that of *solving a game*, which is the simplest one and since it induces a decision problem, allows us to make complexity theoretic statements.

**Problem 1 (Solving the game).**
**INPUT:** A qualitative game $\mathcal{G}$ and a vertex $v$

**OUTPUT:** Does Eve win $\mathcal{G}$ from $v$?

The second problem extends the previous one: most algorithms solve games for all vertices at once instead of only for the given initial vertex. This is called computing the winning regions.

**Problem 2 (Computing the winning regions).**

**INPUT:** A qualitative game $\mathcal{G}$

**OUTPUT:** Compute $W_{\text{Eve}}(\mathcal{G})$ and $W_{\text{Adam}}(\mathcal{G})$

We did not specify how the winning regions or the winning strategies are represented, this will depend on the types of games we consider. The third problem is constructing a winning strategy.

**Problem 3 (Constructing a winning strategy).**

**INPUT:** A qualitative game $\mathcal{G}$ and a vertex $v$

**OUTPUT:** Construct a winning strategy for Eve from $v$

## Values in quantitative games

Let $\mathcal{G}$ be a quantitative game and $v$ a vertex. Given $x \in \mathbb{R}$ called a threshold, we say that a strategy $\sigma$ for Max ensures $x$ from $v$ if every play $\pi$ starting from $v$ consistent with $\sigma$ has value at least $x$ under $f$, i.e. $f(\pi) \ge x$. In that case we say that Max has a strategy ensuring $x$ in $\mathcal{G}$ from $v$.

Note that by doing so we are actually considering a qualitative game in disguise, where the qualitative condition is the set of plays having value at least $x$ under $f$. Formally, a quantitative condition $f$ and a threshold $x$ induce a qualitative condition

$$f_{\ge x} = \{\pi \in \text{Paths}_{\omega} | f(\pi) \ge x\}.$$

Analogously, we say that a strategy $\tau$ for Min ensures $x$ from $v$ if every play $\pi$ starting from $v$ consistent with $\tau$ has value at most $x$ under $f$, i.e. $f(\pi) \le x$.

We let $\text{val}_{\text{Max}}^{\mathcal{G}}(v)$ denote the quantity

$$\sup_{\sigma} \inf_{\tau} f(\pi_{\sigma, \tau}^{v}),$$

where $\sigma$ ranges over all strategies of Max and $\tau$ over all strategies of Min. We also write $\text{val}_{\text{Max}}^{\sigma}(v) = \inf_{\tau} f(\pi_{\sigma, \tau}^{v})$ so that $\text{val}_{\text{Max}}^{\mathcal{G}}(v) = \sup_{\sigma} \text{val}_{\text{Max}}^{\sigma}(v)$. This is called the value of Max in the game $\mathcal{G}$ from $v$, and represents the best outcome that she can ensure against any strategy of Min. Note that $\text{val}_{\text{Max}}^{\mathcal{G}}(v)$ is either a real number, $\infty$, or $-\infty$.

A strategy $\sigma$ such that $\text{val}_{\text{Max}}^{\sigma}(v) = \text{val}_{\text{Max}}^{\mathcal{G}}(v)$ is called optimal from $v$, and it is simply optimal if the equality holds for all vertices. Equivalently, $\sigma$ is optimal from $v$ if for every play $\pi$ consistent with $\sigma$ starting from $v$ we have $f(\pi) \ge \text{val}_{\text{Max}}^{\mathcal{G}}(v)$.
There may not exist optimal strategies which is why we introduce the following notion. For $\varepsilon > 0$, a strategy $\sigma$ such that $\text{val}_{\text{Max}}^{\sigma}(v) \ge \text{val}_{\text{Max}}^{\mathcal{G}}(v) - \varepsilon$ is called $\varepsilon$-optimal. If $\text{val}_{\text{Max}}^{\mathcal{G}}(v)$ is finite there exist $\varepsilon$-optimal strategies for any $\varepsilon > 0$.

Symmetrically, we let $\text{val}_{\text{Min}}^{\mathcal{G}}(v)$ denote

$$ \inf_{\tau} \sup_{\sigma} f(\pi_{\sigma, \tau}). $$

**Fact 2 (Comparison of values for Min and Max).** For all quantitative games $\mathcal{G}$ and vertex $v$ we have $\text{val}_{\text{Max}}^{\mathcal{G}}(v) \le \text{val}_{\text{Min}}^{\mathcal{G}}(v)$.

*Proof.* For any function $F: X \times Y \to R \cup \{\pm\infty\}$, we have

$$ \sup_{x \in X} \inf_{y \in Y} F(x, y) \le \sup_{y \in Y} \inf_{x \in X} F(x, y). $$

□

If this inequality is an equality, meaning

$$ \text{val}_{\text{Max}}^{\mathcal{G}}(v) = \text{val}_{\text{Min}}^{\mathcal{G}}(v), $$

we say that the game $\mathcal{G}$ is determined in $v$, and let $\text{val}^{\mathcal{G}}(v)$ denote the value in the game $\mathcal{G}$ from $v$. Similarly as for the qualitative case, being determined can be understood as follows: the outcome can be determined before playing assuming both players play optimally, and in that case the outcome is the value.

We say that a quantitative objective $f: C^{\omega} \to R \cup \{\pm\infty\}$ is Borel if for all $x \in R$, the qualitative objective $f_{\ge x} \subseteq C^{\omega}$ is a Borel set.

**Corollary 1 (Borel determinacy for quantitative games).** *Quantitative games with Borel conditions are determined, meaning that for all quantitative games $\mathcal{G}$ we have $\text{val}_{\text{Max}}^{\mathcal{G}} = \text{val}_{\text{Min}}^{\mathcal{G}}$.*

*Proof.* If $\text{val}_{\text{Max}}^{\mathcal{G}}(v) = \infty$ then thanks to the inequality above $\text{val}_{\text{Min}}^{\mathcal{G}}(v) = \infty$ and the equality holds. Assume $\text{val}_{\text{Max}}^{\mathcal{G}}(v) = -\infty$ and let $r$ be a real number. (The argument is actually the same as for the finite case but for the sake of clarity we treat them independently.) We consider $f_{\ge r}$. By definition, this a qualitative Borel condition, so Theorem 1 implies that it is determined. Since Max cannot have a winning strategy for $f_{\ge r}$, as this would contradict the definition of $\text{val}_{\text{Max}}^{\mathcal{G}}(v)$, this implies that Min has a winning strategy for $f_{\ge r}$, meaning a strategy $\tau$ such that every play $\pi$ starting from $v$ consistent with $\tau$ satisfy $f(\pi) < r$. In other words, $\text{val}_{\text{Min}}^{\tau}(v) = \sup_{\sigma} f(\pi_{\sigma, \tau}) \le r$, which implies that $\text{val}_{\text{Min}}^{\mathcal{G}}(v) \le r$. Since this is true for any real number $r$, this implies $\text{val}_{\text{Min}}^{\mathcal{G}}(v) = -\infty$.

Let us now assume that $x = \text{val}_{\text{Max}}^{\mathcal{G}}(v)$ is finite and let $\varepsilon > 0$. We consider $f_{\ge x + \varepsilon}$. By definition, this a qualitative Borel condition, so Theorem 1 implies that it is determined. Since Max cannot have a winning strategy for $f_{\ge x + \varepsilon}$, as this would contradict the definition of $\text{val}_{\text{Max}}^{\mathcal{G}}(v)$, this implies that Min has a winning strategy for $f_{\ge x + \varepsilon}$, meaning a strategy $\tau$ such that every play $\pi$ starting from $v$ consistent with $\tau$ satisfy $f(\pi) < x + \varepsilon$. In other words, $\text{val}_{\text{Min}}^{\tau}(v) = \sup_{\sigma} f(\pi_{\sigma, \tau}) \le x + \varepsilon$, which implies that $\text{val}_{\text{Min}}^{\mathcal{G}}(v) \le x + \varepsilon$. Since this is true for any $\varepsilon > 0$, this implies $\text{val}_{\text{Min}}^{\mathcal{G}}(v) \le \text{val}_{\text{Max}}^{\mathcal{G}}(v)$. As we have seen the converse inequality holds, implying the equality. □
Note that this determinacy result does not imply the existence of optimal strategies.

**Computational problems for quantitative games**

As for qualitative games, we identify different computational problems. The first is
solving the game.

**Problem 4 (Solving the game).**

INPUT: A quantitative game $\mathcal{G}$, a vertex $v$, and a threshold $x \in \mathbb{Q} \cup \{\pm\infty\}$

OUTPUT: Does Max have a strategy ensuring $x$ from $v$?

A very close problem is the *value problem*.

**Problem 5 (Solving the value problem).**

INPUT: A quantitative game $\mathcal{G}$, a vertex $v$, and a threshold $x \in \mathbb{Q} \cup \{\pm\infty\}$

OUTPUT: Is it true that $val^{\mathcal{G}}(v) \geq x$?

The two problems of solving a game and the value problem are not quite equivalent:
they become equivalent if we assume the existence of optimal strategies.

The value problem is directly related to *computing the value*.

**Problem 6 (Computing the value).**

INPUT: A quantitative game $\mathcal{G}$ and a vertex $v$

OUTPUT: Compute $val^{\mathcal{G}}(v)$

What computing the value means may become unclear if the value is not a ratio-
nal number, making its representation complicated. Especially in this case, it may be
enough to approximate the value, which is indeed what the value problem gives us: by
repeatedly applying an algorithm solving the value problem one can approximate the
value to any given precision, using a binary search.

**Lemma 2 (Binary search for computing the value).** *If there exists an algorithm A for solving the value problem of a class of games, then there exists an algorithm for approximating the value of games in this class within precision ε using log(1/ε) calls to the algorithm A.*

The following problem is global, in the same way as computing the winning re-
gions.

**Problem 7 (Computing the value function).**

INPUT: A quantitative game $\mathcal{G}$

OUTPUT: Compute the value function $val^{\mathcal{G}}: V \to R \cup \{\pm\infty\}$

Finally, we are sometimes interested in constructing optimal strategies provided
they exist.

**Problem 8 (Constructing an optimal strategy).**

INPUT: A quantitative game $\mathcal{G}$ and a vertex $v$

OUTPUT: Compute an optimal strategy from $v$

A close variant is to construct $\epsilon$-optimal strategies, usually with $\epsilon$ given as input.
## Prefix independent objectives

A qualitative objective $\Omega$ is:

* closed under adding prefixes if for every finite sequence $\rho$ and for every infinite sequence $\rho'$, if $\rho' \in \Omega$ then $\rho\rho' \in \Omega$;

* closed under removing prefixes if for every finite sequence $\rho$ and for every infinite sequence $\rho'$, if $\rho\rho' \in \Omega$ then $\rho' \in \Omega$;

* prefix independent if it is closed under both adding and removing prefixes; in other words whether a sequence satisfies $\Omega$ does not depend upon finite prefixes.

Let $\pi$ be a finite play consistent with $\sigma$, we write $\sigma|_{\pi}$ for the strategy defined by

$$ \sigma|_{\pi}(\pi') = \sigma(\pi\pi'). $$

**Fact 3** (Winning for objectives closed under removing prefixes). Let $\mathcal{G}$ be a qualitative game with objective $\Omega$ closed under removing prefixes, $\sigma$ a winning strategy from $v$, and $\pi$ a finite play consistent with $\sigma$ starting from $v$. Then $\sigma|_{\pi}$ is winning from $v' = \text{last}(\pi)$.

*Proof.* Let $\pi'$ be an infinite play consistent with $\sigma|_{\pi}$ from $v'$, then $\pi\pi'$ is an infinite play consistent with $\sigma$ starting from $v$, implying that it is winning, and since $\Omega$ is closed under removing prefixes the play $\pi'$ is winning. Thus $\sigma|_{\pi}$ is winning from $v'$. $\square$

**Corollary 2** (Reachable vertices of a winning strategy for objectives closed under removing prefixes). Let $\mathcal{G}$ be a qualitative game with objective $\Omega$ closed under removing prefixes and $\sigma$ a winning strategy from $v$. Then all vertices reachable from $v$ by a play consistent with $\sigma$ are winning.

In other words, when playing a winning strategy the play does not leave the winning region.

Similarly, a quantitative objective $\Phi$ is:

* monotonic under adding prefixes if for every finite sequence $\rho$ and for every infinite sequence $\rho'$ we have $\Phi(\rho') \le \Phi(\rho\rho')$;

* monotonic under removing prefixes if for every finite sequence $\rho$ and for every infinite sequence $\rho'$ we have $\Phi(\rho') \ge \Phi(\rho\rho')$;

* prefix independent if it is monotonic under both adding and removing prefixes.

The fact above extends to quantitative objectives with the same proof.

**Fact 4** (Winning for objectives monotonic under removing prefixes). Let $\mathcal{G}$ be a quantitative game with objective $\Phi$ monotonic under removing prefixes, $\sigma$ a strategy ensuring $x$ from $v$, and $\pi$ a finite play consistent with $\sigma$ starting from $v$. Then $\sigma|_{\pi}$ ensures $x$ from $v' = \text{last}(\pi)$.
*Proof.* Let $\pi'$ be an infinite play consistent with $\sigma|_{\pi}$ from $v'$, then $\pi\pi'$ is an infinite play consistent with $\sigma$ starting from $v$, implying that $\Phi(\pi\pi') \ge x$, and since $\Phi$ is monotonic under removing prefixes this implies that $\Phi(\pi') \ge x$. Thus $\sigma|_{\pi}$ ensures $x$ from $v'$. $\square$

**Corollary 3 (Comparison of values along a play).** Let $\mathcal{G}$ be a quantitative game with objective $\Phi$ monotonic under removing prefixes and $\sigma$ an optimal strategy from $v$. Then for all vertices $v'$ reachable from $v$ by a play consistent with $\sigma$ we have $\text{val}^q(v) \le \text{val}^q(v')$.

In other words, when playing an optimal strategy the value is non-decreasing along the play.

## 1.2 Computational models

### The Random Access Machine model of computation

For complexity statements we consider the classical Turing model of computation. However for algorithmic results the Turing model is a bit painful and unnatural hence it is customary to use the Random Access Machine (RAM) model instead. Intuitively this corresponds to using a standard imperative programming language on a usual computer which can create, access, and update variables. There are variants of the RAM model; to be specific the one we use and describe here is called *'word RAM'*. The main reason to use the RAM model is to make our life easier by hiding some small computational costs which are inessential for our purposes.

The memory is arranged in *machine words* whose size is a parameter $w$ to be fixed depending on the problem. A machine word is a register which stores some information as a binary word of length $w$. The first key assumption of the RAM model is that *memory can be accessed in constant time*. In other words, machine words are registers with a unique address and can be accessed either directly or indirectly. A concrete implication is that checking whether an element belongs to a set is a single operation (if each element of the set can be stored in a single machine word).

We consider an (often implicit) set of basic operations operating on a constant number of machine words; addition, multiplication, subtraction, division, and comparison of integers are typical examples. The second key assumption is the *'unit cost model'*, it says that the time complexity (also called cost) of basic operations is constant. This convention implies that we can manipulate counters for small numbers with no additional complexity, this will be useful in many situations.

We note that this is unrealistic as it means that for instance we can compute the number $2^{2^n}$ by repeatedly squaring 2: the complexity is $O(n)$ but this number uses $O(2^n)$ bits hence cannot be generated in polynomial time using a Turing machine. We will not make use of such weaknesses in our algorithms.

The size of an input is the number of machine words required to store it. The most common choice for the machine word size is $w = \log(s)$ where $s$ is the size of the input
as we want to at least be able to store an integer $x$ of order $s$ in one machine word.
However in situations in which there are numerical inputs, it is reasonable to assume
that each input number fits into one machine word, leading to a potentially larger $w$.
Note that an algorithm in the word RAM model with machine word size $w$ is allowed
to use numbers that are larger than $2^w$, but such numbers should be split among several
machine words.

The time complexity is the number of steps performed by the machine, as a function of the input size, and the space complexity is the maximal number of machine words used throughout the computation.

## Games representations in the RAM model

The important parameters for algorithms on games are $n$ the number of vertices and $m$
the number of edges. Note that our assumption that every vertex has an outgoing edge
implies that $n \le m$.

The machine word size is always at least $w = \log(m)$, so that both a vertex and an
edge can be stored in one machine word. A graph is given by the list of vertices and
the list of edges, which implies that its size is $O(n+m) = O(m)$. An algorithm can go
through all vertices, all edges, or all successors or predecessors of a given vertex, with
no additional cost for the space complexity.

An arena additionally specifies for each vertex which player controls the vertex,
which is a boolean value also stored in one machine word. The representation of con-
ditions and colouring functions is different for each and is discussed when introducing
them.

## Polynomial versus strongly polynomial time algorithms

Let us consider a computational problem in which the input consists of a sequence of
$N$ integers plus a number $n$ of other input bits. We write $L$ for the total number of bits
needed to encode the input integer numbers. We say that an algorithm runs in *strongly polynomial time* if:

* the number of arithmetic operations is bounded by a polynomial in the number of integers $N$ in the input instance; and

* the space used by the algorithm is bounded by a polynomial in the size $L+n$ of the input.

An equivalent definition using the unit cost word RAM model is that the algorithm uses
machine word size $w = L + \log(n)$ and runs in polynomial time.

## Linear programming

We give here only the very essential definitions and results related to linear programming, and refer to [BT97] for a reference book on the topic.
A linear program (in canonical form) uses a set of real variables organised in a vector x and is defined by

$$
\begin{array}{ll}
\text{maximise} & c^T x \\
\text{subject to} & Ax \leq b,
\end{array}
$$

where c and b are rational vectors (with c^T the transpose of c) and A is a rational matrix. More explicitly:

$$
\begin{array}{ll}
\text{maximize} & c_1 x_1 + \dots + c_n x_n \\
\text{subject to} & a_{11} x_1 + \dots + a_{1n} x_n \leq b_1 \\
& \vdots \\
& a_{m1} x_1 + \dots + a_{mn} x_n \leq b_m.
\end{array}
$$

Solving a linear program is finding an optimal assignment $x^*$ of the variables.

**Theorem 2 (Linear programming).** *There exists a polynomial time algorithm for solving linear programs.*

Note that we define here linear programs with a maximising objective, but the same problem with minimising $c^T x$ can be easily shown to be equivalent.

The statement above says that there exists a weakly polynomial time algorithm;
whether there exists a strongly polynomial algorithm for linear programming is a long
standing open question.

**1.3 Objectives**

We present in this section the main objectives and their representations. An objective may depend upon a set of parameters which are sometimes omitted when clear from the context.

Let us recall how we define classes of conditions: we first define an objective,
for instance Safe ⊆ {Win, Lose}ⁿ. For an arena and a colouring function c : E →
{Win, Lose} defined over this arena this induces the safety condition Safe(c). Given
an arena and a condition W over this arena we say that W is a safety condition if there
exists c such that W = Safe(c). The same terminology is used for all other objectives.

**Prefix dependent qualitative objectives: safety and reachability**

The safety objective is the simplest qualitative objective: the set of colours is {Win, Lose}, and safety requires that the colour Lose is never seen. Formally:

$$
\mathbf{Safe} = \{ \rho \in \{\text{Win}, \text{Lose}\}^{\omega} : \forall i, \rho_i \neq \text{Lose} \}.
$$

In the example represented in Figure 1.3, a play is winning if it never visits $v_7$. Eve wins from the four vertices on the left and loses from all the others, which is represented by the two dotted areas.
<figure><img src="image_7.png" /><figcaption>Figure 1.3: An example of a safety game. The unlabelled edges are implicitly labelled by Win. The condition of Eve is to avoid the colour Lose, hence equivalently here to avoid vertex $v_7$. The two dotted areas represent the winning regions of each player.</figcaption></figure>

The dual of the safety objective is the reachability objective: the set of colours is $\{\text{Win}, \text{Lose}\}$, and reachability requires that the colour Win is seen at least once. Formally:

$$ \text{Reach} = \{ \rho \in \{\text{Win}, \text{Lose}\}^{\omega} : \exists i, \rho_i = \text{Win} \}. $$

Safety and reachability conditions are dual:

$$ \text{Paths}_{\omega} \setminus \text{Safe}(c) = \text{Reach}(\bar{c}) \quad ; \quad \text{Paths}_{\omega} \setminus \text{Reach}(c) = \text{Safe}(\bar{c}). $$

where $\bar{c}$ swaps Win and Lose in $c$. Consequently, if the condition for Eve is a safety condition, then the condition for Adam is a reachability condition, and conversely.

**Remark 3 (Labelling vertices for safety and reachability conditions).** Safety and reachability conditions are most of the time defined on vertices rather than edges, as indeed it is more natural to set as target a vertex or a set of vertices than a set of edges. However in this book we use the more general convention of labelling edges. As illustrated in Lemma 1, labelling vertices is a special case of labelling edges. In Figure 1.3, the condition of Eve is to avoid the colour Lose, and since this is $v_7$ is a self loop with colour Lose, the condition can be equivalently stated as avoiding vertex $v_7$.

## Prefix independent qualitative objectives: Büchi and Parity

Safety and reachability objectives specify which colours occur or not, hence are prefix dependent. We now introduce objectives specifying which colours occur infinitely many times, which will naturally be prefix independent.

The Büchi objective is over the set of colours $\{1, 2\}$, it requires that the colour 2 is seen infinitely many times. Formally:

$$ \text{Buchi} = \{ \rho \in \{1, 2\}^{\omega} : \forall j, \exists i \ge j, \rho_i = 2 \}. $$

The dual of the Büchi objective is the CoBüchi objective: the set of colours is $\{2, 3\}$, it requires that the colour 3 is seen finitely many times. Formally:

$$ \text{CoBuchi} = \{ \rho \in \{2, 3\}^{\omega} : \exists j, \forall i \ge j, \rho_i \neq 3 \}. $$
Büchi and CoBüchi conditions are dual:

$$ \text{Paths}_{\omega} \setminus \text{Buchi}(c) = \text{CoBuchi}(c+1) \ ; \ \text{Paths}_{\omega} \setminus \text{CoBuchi}(c) = \text{Buchi}(c-1). $$

where $c+1$ adds one to $c$ (since $c$ maps vertices to $\{1,2\}$, $c+1$ maps vertices to $\{2,3\}$), and similarly for $c-1$. Consequently, if the condition for Eve is a Büchi condition, then the condition for Adam is a CoBüchi condition, and conversely.

We now define the parity objectives. Let $[i, j]$ be an interval with $i, j \in \mathbb{N}$ used as a parameter defining the range of priorities. The *parity objective* with parameters $i, j$ uses the set of colours $[i, j]$, which are referred to as priorities, and is defined by

$$ \text{Parity}([i, j]) = \left\{ \rho \in [i, j]^{\omega} \mid \begin{array}{l} \text{the largest priority appearing} \\ \text{infinitely many times in } \rho \text{ is even} \end{array} \right\}. $$

We made the dependence in $[i, j]$ explicit by writing $\text{Parity}([i, j])$, but we will most of the time write $\text{Parity}$ and assume that the range of priorities is $[1, d]$, so $d$ is the number of priorities. There are two possible conventions for defining parity objectives: considering the largest priority appearing infinitely many times, or the smallest one. They are strictly equivalent (through the transformation $p \mapsto 2d-p$) but depending on the situation one can be technically more convenient than the other.

We illustrate the definition on two examples.

$$ 12475536363636 \cdots \in \text{Parity}, $$

because the two priorities which appear infinitely often are 3 and 6, and the largest one is 6, which is even.

$$ 222417533333333 \cdots \notin \text{Parity}, $$

because the only priority which appears infinitely often is 3 and it is odd.

Two remarks are in order. First, Büchi and CoBüchi objectives are parity objectives for the set of colours $[1,2]$ and $[2,3]$, respectively. Second, the parity conditions are self dual:

$$ \text{Paths}_{\omega} \setminus \text{Parity}([i, j])(c) = \text{Parity}([i+1, j+1])(c+1), $$

where $c+1$ adds one to $c$. Hence if the condition for Eve is a parity condition, then the condition for Adam is also a parity condition.

Figure 1.4 presents an example of a parity game. The priority of an edge is given by its label.

## Conventions

Given an objective $\Omega \subseteq C^{\omega}$ we use a colouring function $c: E \to C$ to induce the condition $\Omega(c)$. It is convenient to extend this notation to sets of colours, edges, and vertices as follows.

* A set of colours $F \subseteq C$ induces the colouring function $c_F: E \to \{\text{Win}, \text{Lose}\}$ defined by $c_F(X) = \text{Win}$ if $c \in F$ and $\text{Lose}$ otherwise.
<figure><img src="image_8.png" /><figcaption>Figure 1.4: An example of a parity game. The two dotted areas represent the winning regions of each player.</figcaption></figure>

* A set of edges $F \subseteq E$ induces the colouring function $c_F : E \to \{\text{Win, Lose}\}$ defined by $c_F(e) = \text{Win}$ if $e \in F$ and Lose otherwise.

* A set of vertices $F \subseteq V$ induces the colouring function $c_F : E \to \{\text{Win, Lose}\}$ defined by $c_F(e) = \text{Win}$ if $\text{In}(e) \in F$ and Lose otherwise.

As a convention, we write `Reach(F)`, `Safe(F)`, `Buchi(F)`, and `CoBuchi(F)` as a short-hand for `Reach(c_F)`, `Safe(c_F)`, `Buchi(c_F)`, and `CoBuchi(c_F)`, respectively, for all three cases above.

## Representations for qualitative objectives

For reachability, safety, Büchi, and CoBüchi conditions we need one bit per vertex to specify its colour, hence the machine word size $w = \log(m)$ implies that one machine word can store either an edge or a vertex together with this one bit of information.

The situation changes for parity conditions, where each vertex has a priority in $[1, d]$ hence requiring $\log(d)$ bits. We then choose the machine word size $w = \log(m) + \log(d)$ in such a way that one machine word can store either an edge or a vertex together with its priority.

## Quantitative objectives

We define five quantitative objectives, which are variations of each other: shortest path, mean payoff, total payoff, energy, and discounted payoff. For all these objectives, the set of colours is (essentially) $C = \mathbb{Z}$, the set of integers. A colour is called a *weight*, interpreted as a cost. The cost of a finite path is the sum over the weights, which Max wants to maximise and Min to minimise. The problem is that mathematically, the cost of infinite paths may not be defined: the four definitions below can be seen as four different ways to tackle this mathematical obstacle.

### Shortest path

The following definition resolves the problem above by adding a reachability objective, ensuring that paths of interest are finite. The *shortest path* quantitative objective is
<figure><img src="image_9.png" /><figcaption>Figure 1.5: An example of a mean payoff game with threshold 0.</figcaption></figure>

defined over the set of colours $C = \mathbb{Z} \cup \{\text{Win}\}$ by

$$ \text{ShortestPath}(\rho) = \begin{cases} \sum_{i=0}^{k-1} \rho_i & \text{for } k \text{ the first index such that } \rho_k = \text{Win}, \\ \infty & \text{if } \rho_k \neq \text{Win for all } k. \end{cases} $$

Note that we are looking for a path of minimal cost, hence not necessarily the shortest in number of edges.

## Mean payoff

The mean payoff quantitative objective weights paths by their length. It comes in two different flavours: using the supremum limit

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

or the infimum limit

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

As we shall see, in most settings the two objectives will be equivalent. For this reason, we often use MeanPayoff to denote MeanPayoff⁻.

Figure 1.5 presents an example of a mean payoff game. The weight of an edge is given by its label. In this example the threshold is 0, i.e. the induced qualitative condition is MeanPayoff$_{≥0}$ = {$\rho \in C^ω : \text{MeanPayoff}(\rho) \ge 0$}.

## Total payoff

The following definition simply replaces limit by supremum limit. We define the total payoff quantitative objective over the set of colours $C = \mathbb{Z}$ by

$$ \text{TotalPayoff}(\rho) = \limsup_{n} \sum_{i=0}^{n-1} \rho_i $$
Total payoff is closely related to mean payoff, in the sense that it refines it. Indeed, the total payoff of a play is finite if and only if the mean payoff of this play is null. Hence, if a vertex in a game has value 0 for mean payoff, computing its value for total payoff gives an additional insight: it quantifies how the partial sums are fluctuating around the mean payoff. For instance, this allows one to distinguish situation 1, -1, 1, -1, 1, ... where the total payoff is 1 from a close situation -1, 1, -1, 1, ... with total payoff 0.

## Energy

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 \geq 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 all partial sums remain non-negative. In a counter-intuitive way, the objective of Min is to collect higher (positive) weights.

We can observe that Energy($\rho$) = sup $\{\sum_{i=0}^{k-1} (-\rho_i) : k \in \mathbb{N}\}$, which motivates defining:

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

The two objectives are clearly equivalent since one can reduce from one to the other by switching the signs of every weight. The benefit of this definition is that it is intuitively simpler: Max aims at positive weights.

## Discounted payoff

The discounted payoff quantitative objective is parameterised by a discount factor $\lambda \in (0, 1)$. It is defined by:

$$ \text{DiscountedPayoff}_{\lambda}(\rho) = \lim_{k} \sum_{i=0}^{k-1} \lambda^{i} \rho_{i}. $$

Expanding the definition: DiscountedPayoff$_{λ}$($\rho$) = $\rho_0 + \lambda\rho_1 + \lambda^2\rho_2 + ...$. Intuitively, the importance of the weights decrease over time: the weight $\rho_i$ is multiplied by $\lambda^i$ which goes to 0 as $i$ goes to infinity. The discount factor ensures that the limit exists for sequences with bounded weights, which holds for all plays since a (finite) game contains finitely many different weights.

## Representations for quantitative objectives

Let us consider a game $\mathcal{G}$ with one of the payoff conditions defined above. 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 either an edge or a vertex together with its weight can be stored in one machine word and that we can perform arithmetic operations on weights. For all payoff games except discounted games, this means that the input size is $O(m)$.

For discounted payoff games we additionally need to represent the discount factor $\lambda$, which we assume is a rational number $\lambda = \frac{a}{b}$. Since we want to perform arithmetic operations on $\lambda$ it is convenient to store it on one machine word, hence the choice for the machine word size $w = \log(m) + \log(W) + \log(b)$.

## 1.4 Automata

The study of games is deeply intertwined with automata over infinite words and trees. We will not elaborate much on that aspect in this book, but in a few places we will use automata. We define here (non-deterministic) automata over infinite words, and refer to [Tho97] for a survey on automata theory over infinite objects (words and trees) and logic, and to [Pin21] for the most recent and complete textbook on automata theory.

**Definition 2 (Automata).** Let $\Sigma$ be an alphabet. An automaton over the alphabet $\Sigma$ is a tuple $\mathbf{A} = (Q, q_0, \Delta, A)$ where:

* $Q$ is a finite set of states,

* $q_0 \in Q$ is the initial state,

* $\Delta \subseteq Q \times \Sigma \times Q$ is the transition relation,

* $A \subseteq \Delta^\omega$ is the acceptance condition.

The size of $\mathbf{A}$ is its number of states, written $|\mathbf{A}|$. We assume that automata are complete: from any state $q$ and letter $a$, there exists a transition $(q, a, q') \in \Delta$. This mirrors the convention for games that every vertex has an outgoing edge.

We use transition based acceptance conditions instead of state based acceptance conditions, for the same reasons as we use edge labelling colouring functions rather than vertex labelling. This more succinct definition of automata naturally composes with games see Section 1.6.

For a (finite or infinite) word $w = w_0w_1\dots$, a run $\rho = (q_0, w_0, q_1)(q_1, w_1, q_2)\dots$ over $w$ is a sequence of consecutive transitions starting from the initial state $q_0$. An infinite run is accepting if it belongs to $A$, in which case we also say that it satisfies $A$. A word $w$ is accepted if there exists an accepting run over $w$. We let $L(\mathbf{A})$ denote the set of accepted words and call it the language defined by $\mathbf{A}$, or sometimes recognised by $\mathbf{A}$.

An automaton is *deterministic* if for all states $q \in Q$ and letter $a \in \Sigma$, there exists at most one transition $(q, a, q') \in \Delta$. In that case the transition relation becomes a transition function $\delta: Q \times \Sigma \to Q$. The key property of deterministic automata is that for every word there exists exactly one run over it.
We use the same approach as for games for defining classes of automata with the same conditions: an objective $\Omega \subseteq C^\omega$ and a colouring function $c: \Delta \to C$ induce an acceptance condition $\Omega[c] \subseteq \Delta^\omega$. For deterministic automata the colouring function becomes $c: Q \times \Sigma \to C$. As for games the objective qualifies the automaton, so we speak of a parity automaton if it uses a parity objective.

**Theorem 3** (Omega-regular languages). *Non-deterministic Büchi, CoBüchi, parity, and deterministic parity automata define the same class of languages called $\omega$-regular languages.*

## 1.5 Memory

A strategy can be a very complicated object, in particular it is infinite. Indeed, it is a function $\sigma: \text{Paths} \to E$, which means that in order to choose the next move the strategy considers everything played so far: the strategy depends upon the whole play.

An important part of the study of games is to prove that simple strategies suffice for many purposes, and one aspect that makes strategies simple is that they use little memory. For understanding a certain class of games a great insight is often to prove the existence of *simple winning strategies*, as for instance *positional or using finite memory*.

### Positional strategies

*Positional strategies* carry no memory about the play constructed so far and in choosing an edge only look at the current vertex. The word memoryless is sometimes used in lieu of positional. Formally, a *positional strategy* for Eve is a function

$$ \sigma: V_{\text{Eve}} \to E. $$

A positional strategy induces a strategy by $\hat{\sigma}(\pi) = \sigma(\text{last}(\pi))$.

For reasoning about positional strategies it is useful to define the following notion. Let $\mathcal{G}$ be a game and $\sigma$ a positional strategy, we define $\mathcal{G}[\sigma]$ the graph with condition W induced by $\sigma$ on $\mathcal{G}$. The set of vertices is $V$ and the set of edges is

$$ E[\sigma] = \{e = v \to v' \in E: v \in V_{\text{Adam}} \text{ or } (v \in V_{\text{Eve}} \text{ and } \sigma(v) = e)\}. $$

It is equipped with the condition W inherited from $\mathcal{G}$.

**Fact 5** (Game induced by a positional strategy). Let $\mathcal{G}$ be a game with condition W, $\sigma$ a positional strategy, and $v$ a vertex. Then the strategy $\sigma$ is winning from $v$ if and only if all infinite paths in $\mathcal{G}[\sigma]$ from $v$ satisfy W.

We say that a qualitative objective $\Omega$ is *positionally determined* if for every game $\mathcal{G}$ with objective $\Omega$ and every vertex $v$, either of the two players has a positional winning strategy from $v$. We sometimes simply say that $\Omega$ is positional, and talk about a positional determinacy result.

We also say that a qualitative objective $\Omega$ is *half-positionally determined* if for every game $\mathcal{G}$ with objective $\Omega$ and every vertex $v$, if Eve has a winning strategy from
v, then she has a positional winning strategy from v. Similarly, we sometimes shorten to 'Ω is half-positional', and speak of a half-positional determinacy result.

**Remark 4.** Another popular terminology replaces ‘half-positionally determined’ and ‘positionally determined’ by ‘positionally determined’ and ‘bi-positionally determined’. The best argument for the terminology we adopt in this book is that in general determinacy is about both players, hence it naturally extends to positional determinacy.

As we discussed earlier, the task of solving a game does not include constructing winning strategies. We present a general binary search technique for doing so assuming half-positional determinacy.

**Lemma 3** (Binary search for constructing positional strategies). Let Ω be a half-positionally determined qualitative objective. If there exists an algorithm A for solving games with objective Ω, then there exists an algorithm for constructing winning strategies for Eve for games in this class using $n \cdot \log(\frac{m}{n})$ calls to the algorithm A.

*Proof.* Let Ω be a half-positionally determined objective and $\mathcal{G}$ a qualitative game with objective Ω. We first determine $W_{Eve}(\mathcal{G})$, which requires one call to a solving algorithm for each vertex. We fix a vertex $v \in W_{Eve}(\mathcal{G})$ and determine a winning positional move from v. We let $d(v)$ denote the outdegree of v. We choose a subset of $\lfloor \frac{d(v)}{2} \rfloor$ outgoing edges of v, construct the game where we remove these edges, and solve it using v as initial vertex. If Eve wins this game from v, then there is a positional winning strategy that picks one of the remaining outgoing edges of v, otherwise we need to choose one of the removed edges. This binary search algorithm requires $O(\log(d(v)))$ calls to a solving algorithm for finding a winning positional move from v. Doing so for all vertices requires

$$O\left(\sum_{v \in V} \log d(v)\right) \leq n \cdot \log\left(\frac{m}{n}\right)$$

calls to a solving algorithm.

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

Positional determinacy may hold only for some class of arenas (such that finite arenas or arenas with finite outdegree), in which case this is made explicit: *positionally determined over finite arenas*.

Parity objectives are positionally determined; this will be proved in Chapter 2. We illustrate it on Figure 1.6 by annotating Figure 1.4 with the positional winning strategies for both players.

We say that a quantitative objective $\Phi$ is *positionally determined* if for every game $\mathcal{G}$ with objective $\Phi$ and every vertex v, there exists a pair of positional optimal strategies from v. Let us state the quantitative counterpart of Lemma 3. The proof is the same.

Similarly, a quantitative objective $\Phi$ is *half-positionally determined* if for every game $\mathcal{G}$ with objective $\Phi$ and every vertex v, there exists a positional optimal strategy for Max from v.
<figure><img src="image_11.png" /><figcaption>Figure 1.6: The example of a parity game given in Figure 1.4 with additional positional winning strategies for both players (corresponding to dashed edges).</figcaption></figure>

**Lemma 4** (Binary search for constructive winning strategies, quantitative case). Let $\Omega$ be a half-positionally determined quantitative objective. If there exists an algorithm $A$ for computing the value of games with objective $\Omega$, then there exists an algorithm for constructing optimal positional strategies for Max for games in this class using $n \cdot \log(\frac{m}{n})$ calls to $A$.

Uniformity

A qualitative objective $\Omega$ is uniformly positionally determined if for every game $\mathcal{G}$ with objective $\Omega$, there exists a pair $(\sigma, \tau)$ of positional optimal strategies: $\sigma$ is winning from $W_{\text{Eve}}(\mathcal{G})$, meaning from every vertex in $W_{\text{Eve}}(\mathcal{G})$, and $\tau$ is winning from $W_{\text{Adam}}(\mathcal{G})$. Similarly, a quantitative objective $\Phi$ is uniformly positionally determined if for every game with objective $\Phi$, there exists a pair $(\sigma, \tau)$ of positional strategies which are optimal from every vertex.

Being uniformly (half-)positionally determined is a stronger property than being (half-)positionally determined, but in most cases an objective satisfies either both or none, as for example if the objective is prefix independent.

**Lemma 5** (From (half-)positional to uniformly (half-)positional prefix independent objectives). If an objective is (half-)positionally determined and prefix independent then it is uniformly (half-)positionally determined.

*Proof.* Let us consider a game $\mathcal{G}$ with qualitative objective $\Omega$ and assume that $\Omega$ is half-positionally determined. (The argument is exactly the same for positionally determined, and for quantitative objectives, so we will not repeat it.) For each $v \in W_{\text{Eve}}(\mathcal{G})$ let $\sigma_v$ be a positional winning strategy. Thanks to Fact 3 the strategy $\sigma_v$ is winning from all vertices reachable by a play consistent with $\sigma_v$ starting from $v$. Without loss of generality let us assume that $\sigma_v$ is only defined on these vertices.

We fix $\le$ a total order on the set of vertices<fnref n="1" />. We let $\sigma$ be the positional strategy defined by $\sigma(u)$ is $\sigma_v(u)$ where $v$ is the least vertex (with respect to $\le$) such that $\sigma_v$ is defined on $u$. We say that $\sigma$ uses $\sigma_v$ at $u$.

<footnote n="1">¹The argument we give in this proof extends to infinite games whose set of vertices can be well ordered. A well-order is a total order such that every non-empty subset has a least element, which is exactly the property we need in this proof.</footnote>
We argue that $\sigma$ is winning from $W_{Eve}(\mathcal{G})$. Consider a play consistent with $\sigma$ starting from some vertex in $W_{Eve}(\mathcal{G})$ and look at the sequence of strategies it uses. By definition this sequence is non-increasing (with respect to $\le$), hence it is stationary. In other words the play is eventually consistent with some strategy $\sigma_v$, implying that this suffix satisfies $\Omega$. Since $\Omega$ is prefix independent this means that the play itself satisfies $\Omega$, so $\sigma$ is indeed winning. $\square$

Finite memory strategies

Memoryless strategies are sometimes not enough. A more powerful class of strategies is finite memory strategies. Intuitively, a finite memory strategy uses a finite state machine called a memory structure to store the relevant pieces of information about the play constructed so far.

To define finite memory strategies formally, we fix a graph $G$. A memory structure is $\mathcal{M} = (M, m_0, \delta)$: the set $M$ is a set of (memory) states, $m_0 \in M$ is the initial state and $\delta: M \times E \to M$ is the update function. The update function is extended to $\delta^*: E^* \to M$ by $\delta^*(\varepsilon) = m_0$ and $\delta^*(\rho e) = \delta(\delta^*(\rho), e)$. The size of a memory structure is its number of states. Note that a memory structure is a deterministic automaton over the alphabet $E$ but without specifying the acceptance condition.

We define a strategy using $\mathcal{M}$ as a function

$$ \sigma: V_{Eve} \times M \to E. $$

It induces a strategy $\hat{\sigma}$ via $\hat{\sigma}(\pi) = \sigma(\text{last}(\pi), \delta^*(\pi))$. A common abuse of notations is to write $\sigma$ for $\hat{\sigma}$.

We note that positional strategies correspond to strategies using the trivial memory structure consisting of only one state.

We say that a qualitative objective $\Omega$ is determined with finite memory strategies if for every game $\mathcal{G}$ and every vertex $v$, either of the two players has a finite-memory winning strategy. There are several variants of this definition covering cases where the memory is constant or bounded, and uniformly over all vertices or not.

We give in Figure 1.7 an example of a game where Eve has a winning strategy using two memory states but no positional winning strategy. The condition is Buchi(Win₁) ∧ Buchi(Win₂), meaning that a play is winning if both Win₁ and Win₂ are visited infinitely many times. A positional strategy would either always choose the edge labelled Win₁ or the one labelled Win₂, hence does not satisfy the condition. Some memory is required to switch between the two.

Formally, let $e_1$ be the edge labelled by Win₁ and $e_2$ be the one labelled by Win₂. We let $\mathcal{M} = (\{m_1, m_2\}, m_1, \delta)$ defined by $\delta(m_1, e_1) = m_2$ and $\delta(m_2, e_2) = m_1$. In words, $m_1$ is the memory state saying that the last chosen edge was $e_1$ and $m_2$ correspondingly for $e_2$. We switch from $m_1$ to $m_2$ when traversing $e_1$ and conversely with $e_2$. Then we define $\sigma(v_0, m_1) = e_1$ and $\sigma(v_0, m_2) = e_2$ inducing the strategy $\hat{\sigma}$ using $\mathcal{M}$.

Let us note that to transform this example into one where colours label vertices, we would need three states instead of one. Memory requirements for edge-labelled games and vertex-labelled games are not equivalent.
<figure><img src="image_12.png" /><figcaption>Figure 1.7: An example of a game where Eve has a winning strategy for Buchi(Win₁) ∧ Buchi(Win₂) using two memory states but no positional winning strategy.</figcaption></figure>

## 1.6 Reductions

Automata and memory structures can be used to construct reductions between games. Automata operate at the level of objectives, independently of the colouring function and the arena, while memory structures work at the level of conditions, hence depend on the graph.

### Reductions between objectives using automata

Let $\Omega$ a qualitative objective over the set of colours $C$, and $\Omega'$ a second qualitative objective. We say that $\Omega$ *reduces to* $\Omega'$ if there exists a deterministic automaton $A$ over the alphabet $C$ with acceptance objective $\Omega'$ defining $\Omega$, i.e. such that $L(A) = \Omega$.

This implies that we can transform a game $\mathcal{G}$ with objective $\Omega$ into an equivalent one $\mathcal{G} \times A$ with objective $\Omega'$ by composing $\mathcal{G}$ with $A$: the automaton reads the sequence of colours from $C$ induced by the play and produces a new sequence of colours which is accepted if its satisfies $\Omega'$.

Formally, let $\mathcal{A}$ an arena and

$$A = (Q, q_0, \delta : Q \times C \to Q, \Omega'(c_A))$$

a deterministic automaton with $c_A : Q \times C \to C'$. We construct the arena $\mathcal{A} \times 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 $e = v \xrightarrow{c} v' \in E$ and state $q \in Q$ there is an edge $e[q] = (v, q) \xrightarrow{c_A(q, c)} (v', \delta(q, c))$: the second component computes the run of $A$ on the sequence of colours induced by the play. The arena is $\mathcal{A} \times A = (G \times Q, V_{Eve} \times Q, V_{Adam} \times Q)$. The game is $\mathcal{G} \times A = (\mathcal{A} \times A, \Omega'(c'))$.

The following lemma states two consequences to the fact that $\Omega$ reduces to $\Omega'$.

**Lemma 6 (Automata reductions).** If $\Omega$ reduces to $\Omega'$ through the automaton $A$, then Eve has a winning strategy in $\mathcal{G}$ from $v_0$ if and only if she has a winning strategy in $\mathcal{G} \times A$ from $(v_0, q_0)$.

Consequently, the following properties hold:

* Assume that there exists an algorithm for solving games with objective $\Omega'$ with complexity $T(n, m)$. Then there exists an algorithm for solving games with objectives $\Omega$ of complexity $T(n \cdot |A|, m \cdot |A|)$.

* If $\Omega'$ is determined with finite memory strategies of size $m$, then $\Omega$ is determined with finite memory strategies of size $m \cdot |A|$.
Since the next type of reduction extends this one and the two proofs are very similar we will prove this lemma as a corollary of the next one.

Reductions between objectives using automata are very general: they operate at the level of objectives and therefore completely ignore the arena.

## Reductions between conditions using memory structures

Reductions between conditions using memory structures extend the previous ones, the main difference being that the memory structure reads the sequences of edges and produces a sequence of memory states. The edges contain more information than the sequence of colours (which is what the automaton reads), and this information is dependent on the graph.

Formally, let $\mathcal{A}$ an arena and $\mathcal{M}$ a memory structure. We construct the arena $\mathcal{A} \times \mathcal{M}$ as follows. We first define the graph $G \times M$ whose set of vertices is $V \times M$ and set of edges $E_M$ is defined as follows: for every edge $e = v \to v' \in E$ and state $m \in M$ there is an edge $e[m] = (v, m) \to (v', \delta(m, e))$. The arena is $\mathcal{A} \times \mathcal{M} = (G \times M, V_{\text{Eve}} \times M, V_{\text{Adam}} \times M)$.

**Fact 6 (Strategies with memory).** There is a one to one correspondence between plays in $\mathcal{A}$ from $v_0$ and in $\mathcal{A} \times \mathcal{M}$ from $(v_0, m_0)$.

To the play

$$ \pi = e_0 e_1 \dots \text{ where } e_i = v_i \to v_{i+1} $$

we associate the play

$$ \pi' = e_0[m_0] e_1[m_1] \dots, $$

where for all $i$ we define inductively $m_{i+1} = \delta(m_i, e_i[m_i])$.

Let $W$ be a condition on $\mathcal{A}$ and $W'$ a condition on $\mathcal{A} \times \mathcal{M}$. We say that $W$ reduces to $W'$ (through $\mathcal{M}$) if for all plays $\pi$ in $\mathcal{A}$, we have

$$ \pi \in W \iff \pi' \in W'. $$

Let $\mathcal{M}$ and $\mathcal{M}'$ two memory structure over the same graph, we let $\mathcal{M} \times \mathcal{M}'$ denote the memory structure obtained by direct product.

**Lemma 7 (Memory structure reductions).** If $W$ reduces to $W'$ through the memory structure $\mathcal{M}$, then Eve has a winning strategy in $\mathcal{G} = (\mathcal{A}, W)$ from $v_0$ if and only if she has a winning strategy in $\mathcal{G} \times \mathcal{M} = (\mathcal{A} \times \mathcal{M}, W')$ from $(v_0, m_0)$.

More specifically, if Eve has a winning strategy in $\mathcal{G} \times \mathcal{M}$ from $(v, m_0)$ using $\mathcal{M}'$ as memory structure, then she has a winning strategy in $\mathcal{G}$ from $v$ using $\mathcal{M} \times \mathcal{M}'$ as memory structure. In particular if the strategy in $\mathcal{G} \times \mathcal{M}$ is memoryless, then the strategy in $\mathcal{G}$ uses $\mathcal{M}$ as memory structure.

*Proof.* A winning strategy in $\mathcal{G}$ directly induces a winning strategy in $\mathcal{G} \times \mathcal{M}$ simply by ignoring the additional information and thanks to the equivalence above because $W$ reduces to $W'$. For the converse implication, let $\sigma$ be a winning strategy in $\mathcal{G} \times \mathcal{M}$ using $\mathcal{M}'$ as memory structure. Recall that $\sigma$ is defined through the function $\sigma: (V_{\text{Eve}} \times$
$M) \times M' \to E_M$. Let $p: E_M \to E$ mapping the edge $e_m$ to $e$. We construct a strategy $\sigma'$ in $\mathcal{G}$ using $M \times M'$ as memory structure by

$$ \sigma'(v, (m, m')) = p(\sigma((v, m), m')). $$

The correspondence between plays in $\mathcal{A}$ and $\mathcal{A} \times M$ maps plays consistent with $\sigma$ to plays consistent with $\sigma'$, which together with the fact that $W$ reduces to $W'$ implies that $\sigma'$ is a winning strategy in $\mathcal{G}$ from $v$. $\square$

To obtain Lemma 6 as a corollary of Lemma 7 we observe that a reduction between objectives using an automaton induces a reduction between the induced conditions using a memory structure. Formally, let us assume that $\Omega$ reduces to $\Omega'$, and let $\mathbf{A} = (Q, q_0, \delta, \Omega'(c_{\mathbf{A}}))$ such that $L(\mathbf{A}) = \Omega$. Let $\mathcal{G} = (\mathcal{A}, \Omega(c))$ a game.

We first define the memory structure $\mathcal{M} = (Q, q_0, \delta')$. The transition function is $\delta': Q \times E \to Q$, it is defined by $\delta'(q, e) = \delta(q, c(e))$. We consider the arena $\mathcal{A} \times M$, and define the colouring function $c'(e_q) = c_{\mathbf{A}}(q, c(e))$.

We note that $\Omega(c)$ reduces to $\Omega'(c')$: for all plays $\pi$ in $\mathcal{A}$, we have $\pi \in \Omega(c)$ if and only if $\pi' \in \Omega'(c')$: this is a reformulation of the fact that $L(\mathbf{A}) = \Omega$.

We construct the game $\mathcal{G}' = (\mathcal{A} \times M, \Omega'(c'))$. Thanks to Lemma 7 the two games have the same winner and a strategy in the latter induce a strategy in the former by composing with the memory structure $M$, implying Lemma 6.

## 1.7 Traps and subgames

Let us consider a game $\mathcal{G}$ and a set $X$ of vertices. Assume that for every $v \in X$ there exists $v \to v' \in E$ such that $v' \in X$, then we can define the game $\mathcal{G}[X]$ by restricting $\mathcal{G}$ to the vertices in $X$ and say that $\mathcal{G}[X]$ is the subgame of $\mathcal{G}$ induced by $X$. Formally, the arena is $\mathcal{A}[X]$ with $X$ the set of vertices and $E[X]$ is the set of edges such that both incoming and outgoing vertices are in $X$. The assumption on $X$ ensures that every vertex of $\mathcal{G}[X]$ has an outgoing edge. Both the colouring function and the conditions are naturally induced from $\mathcal{G}$ to $\mathcal{G}[X]$.

We say that $X$ is a trap for Adam if

* for every $v \in X \cap V_{\text{Eve}}$, there exists $v \to v' \in E$ with $v' \in X$, and

* for every $v \in X \cap V_{\text{Adam}}$, for all $v \to v' \in E$, we have $v' \in X$.

Intuitively, a trap for Adam is a subset of vertices which Eve can decide to stay in while Adam cannot force to leave. The same notion can be defined for Eve. Traps satisfy the property above so if $X$ is a trap then the game $\mathcal{G}[X]$ described above is well defined, meaning that every vertex has an outgoing edge.

**Fact 7 (Traps induce subgames).** Let $\mathcal{G}$ be a game, $X$ a trap for Adam, and $\sigma$ a winning strategy for Eve in the subgame $\mathcal{G}[X]$. Then $\sigma$ induces a winning strategy in $\mathcal{G}$.

*Proof.* Any play consistent with $\sigma$ in $\mathcal{G}$ stays forever in $X$ because $X$ is a trap for Adam, hence is winning. $\square$
The notion of traps is very useful when decomposing games. We present some
simple facts about traps, here stated for Adam but easily transposed for Eve.

**Fact 8 (Traps).** Let $\mathcal{G}$ a game.

• Let P, Q two traps for Adam in the game $\mathcal{G}$, then P is a trap for Adam in the subgame of $\mathcal{G}$ induced by Q (but P ∩ Q may not be a trap in $\mathcal{G}$).

• Let P a trap for Eve in the game $\mathcal{G}$ and Q a trap for Adam in the game $\mathcal{G}$, then P ∩ Q is a trap for Eve in the subgame of $\mathcal{G}$ induced by Q.

• Let P a trap for Adam in the game $\mathcal{G}$ and Q a trap for Adam in the subgame of $\mathcal{G}$ induced by X, then Q is a trap for Adam in $\mathcal{G}$.

**1.8 Generic fixed point algorithms**

Let $X$ be a set and $\O: X \to X$ a function that we call an *operator*, we say that $x \in X$ is a *fixed point* of $\O$ if $\O(x) = x$. Fixed points will appear extensively in this book. We describe here two general approaches for computing them: Kleene and Banach fixed point theorems.

**Kleene fixed point theorem**

Let us consider a *lattice* $(X, \leq)$: the binary relation $\leq$ is a partial order, and every pair of elements has a least upper bound and a greatest lower bound. It is a *complete lattice* if every set has a least upper bound and a greatest lower bound. A lattice is finite if the set $X$ is finite. Note that finite lattices are always complete.

We write $\perp$ for the least element in $X$ and $\top$ for the greatest element. An operator $\O: X \to X$ is *monotonic* if for all $x, y \in X$ such that $x \leq y$ we have $\O(x) \leq \O(y)$, and *preserves suprema* if $\O(\sup_n x_n) = \sup_n \O(x_n)$ for all increasing sequences $(x_n)_{n \in \mathbb{N}}$. The twin notion *preserves infima* is defined accordingly.

We say that $x$ is a *pre-fixed point* if $\O(x) \leq x$ and a *post-fixed point* if $\O(x) \geq x$.

**Theorem 4 (Kleene fixed point theorem).** Let $(X, \leq)$ be a complete lattice and $\O: X \to X$ a monotonic operator, then $\O$ has a least fixed point which is also the least pre-fixed point.

Furthermore:

• if X is finite the sequence defined by $u_0 = \perp$ and $u_{k+1} = \O(u_k)$ is stationary and its limit is the least fixed point of $\O$;

• if $\mathcal{O}$ preserves suprema then the least fixed point of $\mathcal{O}$ is $\sup\{\mathcal{O}^k(\perp) : k \in \mathbb{N}\}$.

Under the same assumptions $\mathcal{O}$ has a greatest fixed point which is the greatest post-
fixed point and can be computed in similar ways, replacing ‘preserves suprema’ by
‘preserves infima’.

The typical example of a complete lattice and one that we will use often in this
book is the powerset of a set equipped with the inclusion between subsets. The least
element is the empty set, the greatest element the full set, and least and greatest upper bounds are given by union and intersection. An example of an infinite complete lattice is $R \cup \{\pm\infty\}$ equipped with the natural order.

## Banach fixed point theorem

Let us consider a set $X$ equipped with some norm $\|\cdot\|$. It is called a complete space if all Cauchy sequences converge. The typical example of a complete space is $R^d$ for some $d \in \mathbb{N}$ equipped with the infinity norm $\|x\| = \max_{i \in [1, d]} |x_i|$.

An operator $\mathcal{O}: X \to X$ is contracting if there exists $\lambda < 1$ such that for all $x, y \in X$ we have $\|\mathcal{O}(x) - \mathcal{O}(y)\| \le \lambda \|x - y\|$.

**Theorem 5 (Banach fixed point theorem).** Let $(X, \|\cdot\|)$ be a complete space and $\mathcal{O}: X \to X$ a contracting operator, then $\mathcal{O}$ has a unique fixed point $x_*$. For any $x_0 \in X$, the sequence $(\mathcal{O}^k(x_0))_{k \in \mathbb{N}}$ converges towards $x_*$ and the rate of convergence is given by

$$ \|\mathcal{O}^k(x_0) - x_*\| \le \frac{\lambda^k}{1-\lambda} \|\mathcal{O}(x_0) - x_0\|. $$

## 1.9 Value iteration algorithms

In this section and the next we discuss two families of fixed point algorithms for solving games. The goal is to highlight the main ingredients for constructing algorithms in these two families. If the descriptions below are too abstract it may be useful to see concrete instantiations, referenced below.

### Quantitative games

Let us consider a quantitative game $\mathcal{G}$ with condition $f = \Phi[c]$. Assuming that $\mathcal{G}$ is determined it admits a value function

$$ \mathrm{val}^{\mathcal{G}}: V \to R \cup \{\pm\infty\}, $$

which is defined as

$$ \mathrm{val}^{\mathcal{G}} = \sup_{\sigma} \inf_{\tau} f(\pi_{\sigma, \tau}^{\nu}) = \inf_{\tau} \sup_{\sigma} f(\pi_{\sigma, \tau}^{\nu}), $$

where $\sigma$ ranges over strategies of Max, $\tau$ over strategies of Min, and $\pi_{\sigma, \tau}^{\nu}$ is the play consistent with $\sigma$ and $\tau$ from $v$. In particular we write $\mathrm{val}^{\sigma}(v)$ for $\inf_{\tau} f(\pi_{\sigma, \tau}^{\nu})$ and $\mathrm{val}^{\tau}(v)$ for $\sup_{\sigma} f(\pi_{\sigma, \tau}^{\nu})$.

Let us write $Y = R \cup \{\pm\infty\}$, and note that $Y$ is a total order (and a fortiori a lattice) for the usual order over the reals.

### Qualitative games

For a qualitative game $\mathcal{G}$ there is no notion of a value function so the first step in constructing a value iteration algorithm is to define a meaningful notion of value function.
Let us assume that the condition is $\Omega[c]$ over the set of colours $C$. The first ingredient is a lattice $(Y, \leq)$ together with a function $f: C^\omega \to Y$ for evaluating plays. The value function is $\text{val}^\mathcal{G}: V \to Y$ defined as

$$ \text{val}^\mathcal{G}(v) = \sup_\sigma \inf_\tau f(\pi_{\sigma,\tau}^v), $$

where $\sigma$ ranges over strategies of Max, $\tau$ over strategies of Min, and $\pi_{\sigma,\tau}^v$ is the play consistent with $\sigma$ and $\tau$ from $v$. As above we write $\text{val}^\sigma(v)$ for $\inf_\tau f(\pi_{\sigma,\tau}^v)$ and $\text{val}^\tau(v)$ for $\sup_\sigma f(\pi_{\sigma,\tau}^v)$.

We let $\top$ denote the largest element in $Y$, and $\bot$ for the smallest. The following principle implies that computing the value function in particular yields the winning regions, relating the condition $\Omega$ to the function $f$:

**Property 1 (Characterisation of the winning regions).** For all games $\mathcal{G}$, for all vertices $v$, Eve wins from $v$ for the qualitative objective $\Omega[c]$ if and only if $\text{val}^\mathcal{G}(v) \neq \top$.

This implies that the goal is now to compute or approximate the value function $\text{val}^\mathcal{G}: V \to Y$. Indeed choosing $Y = R \cup \{\pm\infty\}$ covers the quantitative case.

## Fixed point

Let us consider a game $\mathcal{G}$. We let $F_V$ denote the set of functions $V \to Y$, 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)$. The main ingredient is an operator $\mathcal{O}^\mathcal{G}: F_V \to F_V$. The intent is to obtain the function $\text{val}^\mathcal{G}$ as a fixed point of the operator $\mathcal{O}^\mathcal{G}$, using the two different approaches for fixed points we introduced above. Whenever $\mathcal{G}$ is clear from the context, we simply write $\mathcal{O}$ instead of $\mathcal{O}^\mathcal{G}$.

## Fixed point through monotonicity

The first family of algorithms is based on Kleene fixed point theorem as stated in Theorem 4.

**Property 2 (Fixed point through monotonicity).** For all games $\mathcal{G}$, the operator $\mathcal{O}^\mathcal{G}$ is monotonic, and $\text{val}^\mathcal{G}$ is the least fixed point of $\mathcal{O}^\mathcal{G}$.

**Remark 5 (Greatest versus least fixed point).** Whenever technically convenient or more intuitive, we will obtain the value function as the greatest fixed point of $\mathcal{O}^\mathcal{G}$. For value iteration algorithms, only small adjustments are necessary. This will be different for strategy improvement algorithms, in the next section.

Theorem 4 further states that $\text{val}^\mathcal{G}$ is the limit of the sequence $(\mathcal{O}^k(\bot))_{k \in \mathbb{N}}$. The pseudocode is given in Algorithm 1.1.

**Theorem 6 (Generic value iteration algorithm through monotonicity).** Assume Property 2 (fixed point through monotonicity) and that $Y$ is finite. Then the generic value iteration algorithm outputs $\text{val}^\mathcal{G}$ within at most $n \cdot |Y|$ iterations.

A concrete instantiation of this theorem is for energy games, see Section 4.3.
**Algorithm 1.1:** A generic value iteration algorithm based on fixed point through monotonicity – naive version.

**for** $v \in V$ **do**

$\lfloor \mu(v) \rfloor \leftarrow \perp$

**repeat**

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

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

**return** $\mu$

*Proof.* If $Y$ is a finite lattice then so is $F_V$. For each $v$, the sequence $(\mathcal{O}^k(\mu)(v))_{k \in \mathbb{N}}$ is non-decreasing, so it can be strictly decreased at most $|Y|$ times. At each iteration the value of at least one vertex is strictly decreased. Hence there are at most $n \cdot |Y|$ iterations. $\square$

If $Y$ is not finite then the sequence $(\mathcal{O}^k(\mu))_{k \in \mathbb{N}}$ converges towards $\text{val}^{\mathcal{G}}$ but further analysis is required to evaluate the convergence speed.

## Fixed point through contraction

The second family of value iteration algorithms is based on Banach fixed point theorem as stated in Theorem 5, let us fix as a goal to approximate $\text{val}^{\mathcal{G}}$. We equip $F_V$ with a norm $\| \cdot \|$.

**Property 3 (Fixed point through contraction).** *The operator $\mathcal{O}^{\mathcal{G}}$ is contracting in the complete space $(F_V, \| \cdot \|)$, and $\text{val}^{\mathcal{G}}$ is the unique fixed point of $\mathcal{O}^{\mathcal{G}}$.*

The pseudocode of the algorithm is given in Algorithm 1.2.

**Algorithm 1.2:** A generic value iteration algorithm based on fixed point through contraction – naive version.

**Data:** Desired precision $\varepsilon$.

Choose $\mu \in F_V$

**repeat**

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

**until** $\|\mathcal{O}^{\mathcal{G}}(\mu) - \mu\| \le \varepsilon \cdot (1 - \lambda)$

**return** $\mu$

**Theorem 7 (Generic value iteration algorithm through contraction).** Assume Property 3 (fixed point through contraction). Then the generic value iteration algorithm computes an $\varepsilon$-approximation of $\text{val}^{\mathcal{G}}$ within at most $O\left(\frac{\log(\varepsilon)}{\log(\lambda)}\right)$ iterations, where $\lambda \in (0, 1)$ is the contraction factor of $\mathcal{O}^{\mathcal{G}}$.

A concrete instantiation of this theorem is for stochastic reachability games, see Section 6.3.
*Proof.* Thanks to Theorem 5, for any $\mu$ we have

$$ \|\mathcal{O}^k(\mu) - \text{val}^\mathcal{G}\| \le \frac{\lambda^k}{1-\lambda} \cdot \|\mathcal{O}^\mathcal{G}(\mu) - \mu\|. $$

Let us write $\mu_k = \mathcal{O}^k(\mu_0)$, and set the number of iterations to be $k = \frac{\log\left(\frac{\varepsilon(1-\lambda)^2}{\|\mathcal{O}^\mathcal{G}(\mu_0)-\mu_0\|}\right)}{\log(\lambda)}$. It has been chosen so that

$$ \frac{\lambda^k}{1-\lambda} \cdot \|\mathcal{O}^\mathcal{G}(\mu_0) - \mu_0\| \le \varepsilon \cdot (1-\lambda). $$

Thanks to the inequality above for $\mu = \mu_0$, this implies that $\|\mathcal{O}^\mathcal{G}(\mu_k) - \mu_k\| \le \varepsilon \cdot (1 - \lambda)$. Again thanks to the inequality above for $\mu = \mu_k$ this implies that $\|\mu_k - \text{val}^\mathcal{G}\| \le \varepsilon$. Thus, after $k$ iterations, the algorithm outputs an $\varepsilon$-approximation of $\text{val}^\mathcal{G}$. $\square$

## Wrap up

Let us wrap up this section: to construct a value iteration algorithm, one needs:

* for qualitative games, a notion of values induced by a function $f: C^\omega \to Y$ satisfying Property 1;

* in all cases, either a monotonic operator satisfying Property 2 or a contracting operator satisfying Property 3.

## Local operator

In the general case above where nothing is known about the operator $\mathcal{O}^\mathcal{G}$, we cannot hope for a finer analysis. However in most cases the operator is defined in the following way, called ‘local’. Fix a game $\mathcal{G}$. Let us consider a function $\delta: Y \times C \to Y$, which can be though of as the transition function of a deterministic automaton whose set of states is $Y$ and which reads colours. It induces an operator $\mathcal{O}^\mathcal{G}: F_V \to F_V$ defined by:

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

A first interesting fact about this family of operators is that if $\delta$ is monotonic, meaning for all $y, y' \in Y$, $c \in C$, if $y \le y'$ then $\delta(y, c) \le \delta(y', c)$, then $\mathcal{O}^\mathcal{G}$ is monotonic. Let us formulate this assumption explicitly:

**Property 4 (Monotonicity of the $\delta$ function).** *The function $\delta$ is monotonic.*

Let us examine the property that $\text{val}^\mathcal{G}$ is a fixed point of $\mathcal{O}^\mathcal{G}$. We give sufficient conditions in the following lemma:

**Lemma 8.** Let $\mathcal{G}$ a game. Assume that:

* For all $\rho \in C^\omega$ and $c \in C$, we have $f(c \cdot \rho) = \delta(f(\rho), c)$.
• The function $\delta$ is monotonic and continuous.

Then $\text{val}^\mathcal{G}$ is a fixed point of $\mathcal{O}^\mathcal{G}$.

*Proof.* We show that $\text{val}^\mathcal{G} \ge \mathcal{O}^\mathcal{G}(\text{val}^\mathcal{G})$. Let $u \in V_{\text{Max}}$, we consider $\sigma, \tau$ two strategies from $v$. We write $\sigma(u) = u \xrightarrow{c} v$. We let $\sigma', \tau'$ denote the strategies induced by $\sigma, \tau$ after playing $u \xrightarrow{c} v$, $\pi_{u,\tau}$ the play consistent with $\sigma$ and $\tau$ from $u$, and $\pi_{v,\tau'}$ the play consistent with $\sigma'$ and $\tau'$ from $v$. The first property implies that $f(\pi_{u,\tau}) = \delta(f(\pi_{v,\tau'}), c)$. Carefully using infimum and supremum as well as monotonicity and continuity of $\delta$, we obtain the series of inequalities:

$$ 
\begin{align*}
f(\pi_{u,\tau}) &= \delta(f(\pi_{v,\tau'}, c), c) \\
f(\pi_{u,\tau}) &\ge \inf_{\tau'} \delta(f(\pi_{v,\tau'}, c)) = \delta(\inf_{\tau'} f(\pi_{v,\tau'}, c)) \\
\inf_{\tau} f(\pi_{u,\tau}) &\ge \delta(\inf_{\tau'} f(\pi_{v,\tau'}, c)) \\
\sup_{\sigma} \inf_{\tau} f(\pi_{u,\tau}) &\ge \delta(\inf_{\tau'} f(\pi_{v,\tau'}, c)) \\
\sup_{\sigma} \inf_{\tau} f(\pi_{u,\tau}) &\ge \sup_{\sigma'} \delta(\inf_{\tau'} f(\pi_{v,\tau'}, c)) = \delta(\sup_{\sigma'} \inf_{\tau'} f(\pi_{v,\tau'}, c)) \\
\text{val}^\mathcal{G}(u) &\ge \max \left\{ \delta(\text{val}^\mathcal{G}(v) : u \xrightarrow{c} v \in E \right\}.
\end{align*}
$$

The reasoning is similar for $u \in V_{\text{Min}}$, and the converse inequality is also proved along the same lines. $\square$

Saying that $\text{val}^\mathcal{G}$ is a fixed point of $\mathcal{O}^\mathcal{G}$ defined this way is tightly related to the fact the $\mathcal{G}$ is positionally determined, but not equivalent. Indeed, the fact that $\text{val}^\mathcal{G} = \mathcal{O}^\mathcal{G}(\text{val}^\mathcal{G})$ means that from a vertex $u$, the value $\text{val}^\mathcal{G}(u)$ can be computed locally, i.e. by considering the maximum or the minimum over all outgoing edges. It is very tempting to define the argmax and argmin (positional) strategies as follows

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

and to claim that they are optimal. This is unfortunately often not the case, and one needs to be more careful to define optimal positional strategies. We refer to Figure 6.2 for a counter-example for the case of (stochastic) reachability games.

Let us discuss Property 2, which states that $\text{val}^\mathcal{G}$ is the least fixed point of $\mathcal{O}^\mathcal{G}$, and specifically how to prove that such a property holds. Under the assumptions of Lemma 8 we already know that $\text{val}^\mathcal{G}$ is a fixed point of $\mathcal{O}^\mathcal{G}$, which implies that $\text{val}^\mathcal{G}$ is larger than the least fixed point. Let us mention another approach for proving this inequality: we define a sequence of objectives $(f_k)_{k \in \mathbb{N}}$ and show the following two properties.

• Writing $\text{val}^\mathcal{G},f_k$ for the values of the game equipped with objective $f_k$, we have $\text{val}^\mathcal{G},f_k = \mathcal{O}^k(\mu_0)$, meaning that the $k^{\text{th}}$ iteration of $\mathcal{O}$ computes the values for $f_k$.

• We have $f_0 \le f_1 \le \cdots \le f_k \le f$.
The second property directly implies that $val_{\mathcal{G},f_0}^{\mathcal{G}} \le val_{\mathcal{G},f_1}^{\mathcal{G}} \le \dots \le val_{\mathcal{G},f_k}^{\mathcal{G}} \le val_{\mathcal{G}}^{\mathcal{G}}$.
Since the least fixed point of $\mathcal{O}$ is the limit of $\mathcal{O}^k(\mu_0)$, by the inequality above it is
smaller than $val_{\mathcal{G}}^{\mathcal{G}}$. This approach is not easier to use than Lemma 8, but it may be use-
ful as it explains what are the iterations of $\mathcal{O}^{\mathcal{G}}$. We refer to Lemma 35 for an example.

Now let us discuss how to prove that $val_{\mathcal{G}}^{\mathcal{G}}$ is the least fixed point. For this, we
consider a fixed point $\mu$ of $\mathcal{O}^{\mathcal{G}}$, and argue that $val_{\mathcal{G}}^{\mathcal{G}} \le \mu$. To this end, we extract from
$\mu$ a strategy $\tau$ for Min, and show that $val_{\mathcal{G}}^{\mathcal{G}} \le \mu$; since we know that $val_{\mathcal{G}}^{\mathcal{G}} \le val_{\mathcal{G}}^{\mathcal{T}}$, this
implies $val_{\mathcal{G}}^{\mathcal{G}} \le \mu$. Again we refer to Lemma 35 for an example.

**Refined complexity analysis**

The definition of local operators allows us to refine the complexity analysis for the
generic value iteration algorithm. Let us say that $u \xrightarrow{c} v \in E$ is incorrect if $\mu(u) <
\delta(\mu(v), c)$, and that $u$ is incorrect if either $u \in V_{\text{Min}}$ and all outgoing edges are incorrect,
or $u \in V_{\text{Max}}$ and there exists an incorrect outgoing edge. The algorithmic improvement
of the upcoming algorithm over the naive implementations above is that instead of ap-
plying the operator $\mathcal{O}^{\mathcal{G}}$ to all vertices at each iteration we can keep track of incorrect
vertices and only update them. This computes exactly the same sequence of functions,
but at a lesser computational cost. For $u \in V_{\text{Max}}$, it is easy to determine whether it is
incorrect, as it relies on the existence of a single outgoing edge. This is more compli-
cated for $u \in V_{\text{Min}}$: the idea here is not to keep track of all incorrect edges, but rather to
count them.

Let us write $\Delta$ for the complexity of computing $\delta(y,c)$ for given $y \in Y$ and $c \in C$,
and of determining whether $y \le y'$ for $y, y' \in Y$.

**Theorem 8 (Complexity analysis of the refined generic value iteration algorithm based on fixed point through monotonicity).** Assume Properties 2 and 4 (fixed point through monotonicity and monotonicity of $\delta$), and that $Y$ is finite. Then the generic value iteration algorithm outputs $val_{\mathcal{G}}^{\mathcal{G}}$ within at most $n \cdot |Y|$ iterations. The computational cost of a single iteration is $O(m \cdot \Delta)$, so the running time of the whole algorithm is $O(nm \cdot \Delta \cdot |Y|)$.

The data structure consists of the following objects:

* an element 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.

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 outgoing 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 1.3 hence returns the least fixed point, but it also has implications on the complexity. Indeed one iteration of the repeat loop over some vertex $u$ involves

$$O((|\mathrm{In}^{-1}(u)| + |\mathrm{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$ and treating the incorrect ones. Thus the overall complexity for a single iteration is

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

The pseudocode for the case of fixed point through monotonicity is given in Algorithm 1.3. It can be easily adapted to the case of fixed point through contraction by adding a stopping criterion when $||\mathcal{O}^{\mathcal{G}}(\mu) - \mu||$ is small enough.

The correctness of the algorithm is a consequence of the following invariant: for $\mu \in F_Y$, if Incorrect is the set of incorrect vertices and for all $u \in V_{\mathrm{Min}}$, Count($u$) the number of incorrect outgoing edges of $u$, then applying Treat($u$) and Update($u$) to all vertices $u \in \mathrm{Incorrect}$ results in updating $\mu$ to $\mathcal{O}^{\mathcal{G}}(\mu)$ and correctly updating Incorrect and Count. The counting trick is valid because the edge $v \xrightarrow{c} u$ is considered at most once in calls to the function Update between two calls to Update($u$).

**Theorem 9 (Complexity analysis of the refined generic value iteration algorithm based on fixed point through contraction).** Assume Properties 3 and 4 (fixed point through contraction, monotonicity of $\delta$). Then the generic value iteration algorithm computes an $\varepsilon$-approximation of $\mathrm{val}^{\mathcal{G}}$ within at most $O\left(\frac{\log(\varepsilon)}{\log(\lambda)}\right)$ iterations, where $\lambda \in (0, 1)$ is the contraction factor of $\mathcal{O}^{\mathcal{G}}$. The computational cost of a single iteration is $O(m \cdot \Delta)$, so the running time of the whole algorithm is $O(nm \cdot \Delta \cdot |Y|)$.

## 1.10 Strategy improvement algorithms

Value iteration algorithms manipulate value functions and never construct any strategy, at least explicitly. This is a key difference with strategy improvement algorithms (also called policy iteration algorithms) whose fundamental idea is to maintain and improve a strategy. Let us consider a 'local' operator $\mathcal{O}^{\mathcal{G}}$, induced by a function $\delta: Y \times C \to Y$:

$$\mathcal{O}^{\mathcal{G}}(\mu)(u) = \begin{cases} \max\{\delta(\mu(v), c) : u \xrightarrow{c} v \in E\} & \text{if } u \in V_{\mathrm{Max}}, \\ \min\{\delta(\mu(v), c) : u \xrightarrow{c} v \in E\} & \text{if } u \in V_{\mathrm{Min}}. \end{cases}$$
Let us recall from the previous section that we consider two scenarios:

* in the quantitative case, we start from a quantitative condition $f: C^\omega \to \mathbb{R} \cup \{\pm\infty\}$,

* in the qualitative case, we assume the existence of a function $f: C^\omega \to Y$, and thanks to Property 1 computing the value function $\text{val}^\mathcal{G}$ yields the winning regions.

For value iteration algorithms it was enough for $Y$ to be a lattice. Here we need a stronger assumption: $Y$ is a total order.

Let us consider a game $\mathcal{G}$ and set as a goal to construct an optimal strategy for Max. The key idea behind strategy improvement is to use $\text{val}^\sigma$ to improve the strategy $\sigma$ by switching edges, which is an operation that creates a new strategy. This involves defining the notion of improving edges: let us consider a vertex $u \in V_{\text{Max}}$, we say that $e: u \xrightarrow{c} v$ is an improving edge if

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

Intuitively: according to $\text{val}^\sigma$, playing $e$ is better<fnref n="2" /> than playing $\sigma(u)$.

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{c} 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.

The pseudocode of the algorithm is given in Algorithm 1.4. The algorithm is non-deterministic, in the sense that both the initial strategy and at each iteration, the choice of improving edge can be chosen arbitrarily. A typical choice, called the “greedy all-switches” rule, choosing for each $u \in V_{\text{Max}}$ a maximal improving edge, meaning

$$ \operatorname{argmax} \{ \delta(\text{val}^\sigma(v), c) : u \xrightarrow{c} v \in E \}. $$

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)$. Unfortunately, there are no generic correctness proofs for the progress property for this algorithm (we refer to the reference section for further discussion). However, the optimality property can be proved at this level of generality,

<footnote n="2">²We need $Y$ to be totally ordered here.</footnote>
<caption>**Algorithm 1.4:** The generic strategy improvement algorithm.</caption>

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

for the two approaches for fixed point computations: this is the object of the next two subsections.

We refer to Section 4.3 for a concrete instantiation for energy games using monotonic fixed point computations, and to Section 4.4 for discounted payoff games using contracting fixed point computations.

## Fixed point through monotonicity

Let us start with an important remark: Property 2 (fixed point through monotonicity) assumes that the value function is computed as the least fixed point of the monotonic operator $\mathcal{O}^{\mathcal{G}}$. It is very important in the developments below that this is a least fixed point, and not a greatest fixed point: the proof cannot be easily adapted to this latter case.

**Theorem 10 (Optimality property for strategy improvement algorithms based on fixed point through monotonicity).** Assume Properties 2 and 4 (fixed point through monotonicity, monotonicity of $\delta$). Let $\sigma$ 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}^{\mathcal{G}}$. Since $\text{val}^{\mathcal{G}}$ is the least fixed point of $\mathcal{O}^{\mathcal{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}^{\mathcal{G}}(\text{val}^{\sigma}))$. Hence there exists $u \in V$ such that $\text{val}^{\sigma}(u) < \mathcal{O}^{\mathcal{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}^{\mathcal{G}}[\sigma]$, this implies that for $u \in V_{\text{Min}}$ we have $\text{val}^{\sigma}(u) = \min\{\delta(\text{val}^{\sigma}(v), c) : u \xrightarrow{c} v \in E\}$, equal to $\mathcal{O}^{\mathcal{G}}(\text{val}^{\sigma})(u)$. Therefore $u \in V_{\text{Max}}$, implying that there exists $u \xrightarrow{c} v$ such that $\text{val}^{\sigma}(u) < \delta(\text{val}^{\sigma}(v), c)$. This is the definition of $u \xrightarrow{c} v$ being an improving edge. $\square$

## Fixed point through contraction

**Theorem 11 (Optimality property for strategy improvement algorithms based on fixed point through contraction).** Assume Property 3 (fixed point through contraction). Let $\sigma$ be a strategy that has no improving edges, then $\sigma$ is optimal.
*Proof.* Let $\sigma$ be a strategy that has no improving edges. We claim that $val^\sigma$ is a fixed point of $\mathcal{O}^{\mathcal{G}}$, which thanks to Property 3 implies that $val^\sigma = val^\mathcal{G}$, meaning that $\sigma$ is optimal.

Thanks to Property 3 $val^\sigma$ is the unique fixed point of $\mathcal{O}^{\mathcal{G}|\sigma}$, so for $u \in V_{\text{Min}}$ we have $val^\sigma(u) = \min\{\delta(val^\sigma(v), c) : u \xrightarrow{c} v \in E\}$.

The fact that $\sigma$ has no improving edges reads: for all $u \in V_{\text{Max}}$, for all $u \xrightarrow{c} v' \in E$, $\delta(val^\sigma(v'), c') \le \delta(val^\sigma(v), c)$ where $\sigma(u) = u \xrightarrow{c} v$. Since $val^\sigma(u) = \delta(val^\sigma(v), c)$, this implies that $val^\sigma(u) = \max\{\delta(val^\sigma(v'), c) : u \xrightarrow{c} v' \in E\}$.

The two equalities above witness that $val^\sigma$ is the unique fixed point of $\mathcal{O}^{\mathcal{G}}$. $\square$

**Bibliographic references**

The study of games, usually called game theory, has a very long history rooted in mathematics, logic, and economics, among other fields. Foundational ideas and notions emerged from set theory with for instance backward induction by Zermelo [Zer13], and topology with determinacy results by Martin [Mar75] (stated as Theorem 1 in this chapter), and Banach-Mazur and Gale-Stewart games [GS53].

The topic of this book is a small part of game theory: we focus on infinite duration games played on graphs. In this chapter we defined deterministic games, meaning games with no source of randomness, which will be the focus of Part I. Part II introduces stochastic games, which were initially studied in mathematics. We refer to Section 6.6.3 for more bibliographic references on stochastic games, and focus in this chapter on references for deterministic games.

The model presented in this chapter emerged from the study of automata theory and logic, where it is used as a tool for various purposes. Let us first discuss the role of games in two contexts: for solving the synthesis problem of reactive systems and for automata and logic over infinite trees.

The synthesis problem for non-terminating reactive systems was formulated in general terms by Church [Chu57, Chu62] and is therefore also called Church's problem: from a specification of a step-by step transformation of an input stream given in some logical formalism, construct a system satisfying the specification. The first published paper solving Church's problem for monadic second-order logic was written by Büchi and Landweber [BL69], following a paper by Landweber [Lan67] (then Büchi's PhD student) focussing on solving games. However, the idea of casting the synthesis problem as a game between a system and its environment is due to McNaughton: in the technical report [McN65] McNaughton attempted to give a solution to the synthesis problem using games, initiating many of the most important ideas for analysing games. Unfortunately the proof contained an error which Landweber detected and communicated to McNaughton, who then decided to let Landweber publish his complete solution. One of the most difficult step in the solution of Church's problem for monadic second-order logic by Büchi and Landweber [BL69] is the determinisation procedure from Büchi to Muller automata due to McNaughton [McN66]. We refer to Thomas'
survey [Tho09] for more details on some historical and technical aspects of the early
papers on Church's synthesis problem.

Games emerged in another aspect of automata theory: for understanding the diffi-
cult result of Rabin [Rab69a] saying that automata over infinite trees can be effectively
complemented. This is the key step for proving Rabin's seminal result that the monadic
second-order theory of the infinite binary tree is decidable. The celebrated paper of
Gurevich and Harrington [GH82] revisits Rabin's result by reducing the complementa-
tion question to a determinacy result for games. Interestingly, they credit McNaughton
for 'airing the idea' of using games in this context and then for exploiting it to Landwe-
ber [Lan67], Büchi and Landweber [BL69], and Büchi [Büc77].

Both lines of work have been highly influential in automata theory and logic; we
refer to the reference section in Chapter 2 for more bibliographic references on this
connection. They bind automata theory and logic to the study of games on graphs and
provide motivations and questions many of which are still open today.

Beyond these two examples there are many applications of games in theoretical
computer science and logic in particular. The following quote is due to Hodges [Hod93]:

An extraordinary number of basic ideas in model theory can be expressed in terms of games.

Let us mention model checking games, which are used for checking whether a model
satisfies a formula. They often form both a theoretical tool for understanding the model
checking problem and proving its properties, as well as an algorithmic backend for ef-
fectively deciding properties of a logical formalism (we refer to [Grä02] for a survey on
model checking games). Another important construction of a game for understanding
logical properties is the Ehrenfeucht-Fraïssé games [Ehr61, Fra50, Fra53] whose goal
is to determine whether two models are equivalent against a logical formalism.

Value iteration and strategy improvement algorithms are the most common families
of algorithms. The latter are also often called policy improvement or policy iteration.
There are many frameworks presenting them in generic terms as we did in this chap-
ter, see for instance [CFGO22] for value iteration and [Ohl21, Koz21] for strategy
improvement algorithms. The PhD thesis [Ohl21] shows a generic argument for the
progress property to hold in the setting of monotonic universal graphs, but it considers
the restricted version where only one edge can be switched at a time.
# Part I

## Classic
<figure><img src="image_13.png" /></figure>
REGULAR
GAMES

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

<figure><img src="image_15.png" /></figure>
Chapter 2

# Regular Games

NATHANAËL FIJALKOW, FLORIAN HORN

This chapter considers the so-called regular games, which from the easiest to the most complicated are: reachability, Büchi, parity, Rabin, and then Muller games. We develop in Section 2.1 the notion of attractors for solving reachability games. This is the main building block for constructing algorithms throughout the book. The next step is Büchi games in Section 2.2. We then construct a conceptually simple exponential time recursive algorithm for solving parity games in Section 2.3. Section 2.4 is a short regression about a general result for proving positional determinacy of qualitative games. We come back to regular games in Section 2.5, extending the recursive algorithm of parity games to Muller games, and discuss the computational complexities of solving Rabin, Streett, and Muller games. Finally, Section 2.6 is devoted to the combinatorial notion of the Zielonka tree, which beautifully explains the memory requirements for Muller games and gives additional insights into the structures of Rabin and parity objectives.

**Remark 6** (Finite versus infinite games). As in the rest of the book unless otherwise specified we consider finite games. However all positionality and finite memory determinacy results proved in this chapter hold for infinite games. In all cases the proofs we give use the finiteness of the games. In many cases, the proofs can be extended to infinite games with a technical overhead involving in particular a transfinite induction. The difficulty is illustrated before the proof of Theorem 12.

## 2.1 Reachability games

Recall that the objective Reach requires that the colour Win appears at least once and Safe requires that the colour Lose never appears. We identify the colour Win with $c^{-1}(\text{Win})$ the set of edges labelled Win, so we write $e \in \text{Win}$ when $c(e) = \text{Win}$, and similarly for Lose. Therefore $\text{Reach}(c)$ can equivalently be described as $\text{Reach}(\text{Win})$.
**Theorem 12** (Positional determinacy and complexity of reachability games). *Reachability objectives are uniformly positionally determined. There exists an algorithm for computing the winning regions of reachability games in linear time and space. More precisely the time and space complexity are both $O(m)$.*

The positional determinacy result holds for infinite arenas.

The complexity results are stated in the unit cost RAM model with machine word size $w = \log(m)$ with $m$ the number of edges. We refer to Section 1.2 for more details about the model, which is in subtle ways different than the Turing model. The complexity would be slightly different in the Turing model: an additional $\log(m)$ factor would be incurred for manipulating numbers of order $m$, which the unit cost RAM model allows us to conveniently hide.

In the literature the complexity $O(n+m)$ is often reported for solving reachability games. Since we make the assumption that every vertex has an outgoing edge this implies that $n \le m$, so $O(n+m) = O(m)$.

Reachability and safety games are most often defined labelling vertices than edges. As explained in Section 1.1, labelling edges is slightly more general than labelling vertices. To improve readability, let us first consider the case where we label vertices, and then explain how this (seamlessly) extends to labelling edges. The condition is Reach(Win) with Win a set of vertices. Let us introduce some notations. For a subset $X \subseteq V$, we let $\text{Pre}_{\text{Eve}}(X) \subseteq V$ the set of vertices from which Eve can ensure that the next vertex is in $X$:

$$ \text{Pre}_{\text{Eve}}(X) = \{u \in V_{\text{Eve}} : \exists u \to v \in E, v \in X\} \\ \cup \quad \{u \in V_{\text{Adam}} : \forall u \to v \in E, v \in X\}. $$

Let us define an operator on subsets of vertices:

$$ X \mapsto \text{Win} \cup \text{Pre}_{\text{Eve}}(X). $$

We note that this operator is monotonic when equipping the powerset of vertices with the inclusion preorder: if $X \subseteq X'$ then $\text{Pre}_{\text{Eve}}(X) \subseteq \text{Pre}_{\text{Eve}}(X')$. Hence Theorem 4 applies: this operator has a least fixed point which we call the attractor of Win for Eve and write $\text{Attr}_{\text{Eve}}(\text{Win})$, and it is computed by the following sequence: we let $\text{Attr}_{\text{Eve}}^0(\text{Win}) = \text{Win}$ and

$$ \text{Attr}_{\text{Eve}}^{k+1}(\text{Win}) = \text{Win} \cup \text{Pre}_{\text{Eve}}(\text{Attr}_{\text{Eve}}^k(\text{Win})). $$

This constructs a sequence $(\text{Attr}_{\text{Eve}}^k(\text{Win}))_{k \in \mathbb{N}}$ of non-decreasing subsets of $V$. If the game is finite and $n$ is the number of vertices, the sequence stabilises after at most $n-1$ steps, i.e. $\text{Attr}_{\text{Eve}}^{n-1}(\text{Win}) = \text{Attr}_{\text{Eve}}^n(\text{Win}) = \text{Attr}_{\text{Eve}}(\text{Win})$.

Let us drop the finiteness assumption: if the game is infinite but has finite outdegree, meaning that for any vertex there is a finite number of outgoing edges, then the operator above preserves suprema so thanks to Theorem 4 we have $\text{Attr}_{\text{Eve}}(\text{Win}) = \bigcup_{k \in \mathbb{N}} \text{Attr}_{\text{Eve}}^k(\text{Win})$. In full generality the operator does not preserve suprema and the use of ordinals is necessary: we define the sequence $(\text{Attr}_{\text{Eve}}^\alpha(\text{Win}))$ indexed by ordinals up to the cardinal of $\mathcal{G}$, the case of a limit ordinal $\alpha$ being $\text{Attr}_{\text{Eve}}^\alpha(\text{Win}) =$
$\cup_{\beta<\alpha} \text{Attr}_{\text{Eve}}^{\beta}(\text{Win})$. We then show that $\text{Attr}_{\text{Eve}}(\text{Win})$ is the union of all elements in this sequence. We do not elaborate further this most general case but note that the overhead is mostly technical, the proof below of Lemma 9 can be adapted with little changes using a transfinite induction.

The following lemma shows how the attractor yields a solution to reachability games and directly implies Theorem 12.

**Lemma 9 (Characterisation of the winning region of reachability games using attractors).** Let $\mathcal{G}$ a reachability game. Then $W_{\text{Eve}}(\mathcal{G}) = \text{Attr}_{\text{Eve}}(\text{Win})$, and:

* there exists a uniform positional strategy $\sigma$ for Eve called the attractor strategy defined on $\text{Attr}_{\text{Eve}}(\text{Win})$ which ensures to reach Win from any vertex in $\text{Attr}_{\text{Eve}}(\text{Win})$, with the property that for any $k \in \mathbb{N}$ all plays consistent with $\sigma$ from $\text{Attr}_{\text{Eve}}^k(\text{Win})$ reach Win within $k$ steps and remain in $\text{Attr}_{\text{Eve}}(\text{Win})$ until doing so;

* there exists a uniform positional strategy $\tau$ for Adam called the counter-attractor strategy defined on $V \setminus \text{Attr}_{\text{Eve}}(\text{Win})$ which ensures never to reach Win from any vertex in $V \setminus \text{Attr}_{\text{Eve}}(\text{Win})$, with the property that all plays consistent with $\tau$ remain in $V \setminus \text{Attr}_{\text{Eve}}(\text{Win})$.

The following definition is very important: for $v \in V$, the rank of $v$ is the smallest $k \in \mathbb{N}$ such that $v \in \text{Attr}_{\text{Eve}}^k(\text{Win})$.

*Proof.* We first show that $\text{Attr}_{\text{Eve}}(\text{Win}) \subseteq W_{\text{Eve}}(\mathcal{G})$. We use the rank to define a positional strategy $\sigma$ for Eve. Let $u \in V_{\text{Eve}}$ of rank $k+1$, then $u \in \text{Pre}_{\text{Eve}}(\text{Attr}_{\text{Eve}}^k(\text{Win}))$, so there exists $u \to v \in E$ such that $v \in \text{Attr}_{\text{Eve}}^k(\text{Win})$, define $\sigma(u) = u \to v$. If $u \in V_{\text{Eve}}$ has rank 0, meaning $u \in \text{Win}$, the game is already won.

We argue that $\sigma$ ensures $\text{Reach}(\text{Win})$. By construction in any play consistent with $\sigma$ at each step either we are in $\text{Win}$ or the rank decreases by at least one. Thus any play consistent with $\sigma$ from $\text{Attr}_{\text{Eve}}(\text{Win})$ reaches $\text{Win}$.

We now show that $W_{\text{Eve}}(\mathcal{G}) \subseteq \text{Attr}_{\text{Eve}}(\text{Win})$. For this we actually show

$$V \setminus \text{Attr}_{\text{Eve}}(\text{Win}) \subseteq W_{\text{Adam}}(\mathcal{G}).$$

Indeed, $W_{\text{Adam}}(\mathcal{G}) \subseteq V \setminus W_{\text{Eve}}(\mathcal{G})$, because Eve and Adam cannot have a winning strategy from the same vertex. This property is clear and holds for any game, it should not be confused with determinacy.

We define a positional strategy $\tau$ for Adam from $V \setminus \text{Attr}_{\text{Eve}}(\text{Win})$. Let $u \in V_{\text{Adam}}$ in $V \setminus \text{Attr}_{\text{Eve}}(\text{Win})$, there exists $u \to v \in E$ such that $v \in V \setminus \text{Attr}_{\text{Eve}}(\text{Win})$, define $\tau(u) = u \to v$. Similarly, if $u \in V_{\text{Eve}}$ in $V \setminus \text{Attr}_{\text{Eve}}(\text{Win})$, then for all $u \to v \in E$, we have $v \in V \setminus \text{Attr}_{\text{Eve}}(\text{Win})$. It follows that any play consistent with $\tau$ remain in $V \setminus \text{Attr}_{\text{Eve}}(\text{Win})$ hence never reaches $\text{Win}$, in other words $\tau$ ensures $\text{Safe}(\text{Win})$ from $V \setminus \text{Attr}_{\text{Eve}}(\text{Win})$. $\square$

Let us note that the proof above extends very easily to the edge labelling case. Let $\text{Win}$ a set of edges, we define:

$$\text{Win}' = \{u \in V_{\text{Eve}} : \exists e = u \to v \in E, e \in \text{Win}\} \cup \{u \in V_{\text{Adam}} : \forall e = u \to v \in E, e \in \text{Win}\}.$$
Eve has a winning strategy for Reach(Win) if and only if she has one for Reach(Win'),
which reduces edge labelling to vertex labelling for reachability games. In the pseu-
docode of Algorithm 2.1 we use the (more general) edge labelling convention. Algo-
rithm 2.1 is an efficient implementation of the attractor computation, and more pre-
cisely it computes the ranks of all vertices: it returns a function $\mu: V \to N \cup \{\infty\}$ such
that $\mu(u)$ is the rank of $u$, as stated in the following theorem.

**Theorem 13 (Computing ranks for reachability games).** *There exists an algorithm for computing the ranks of all vertices in reachability games in linear time and space. More precisely the time and space complexity are both $O(m)$.*

In Section 4.5 we will generalise this algorithm to a quantitative setting, considering
the shortest path objective. We invite the reader to compare this algorithm to the generic
value iteration algorithm presented in Algorithm 1.3: it is indeed the instantiation of
this framework for the quantitative shortest path objective with all weights equal to
one.

The correctness of the algorithm hinges on the following invariant: for $i \ge 1$, before
the $i^{th}$ iteration in the *Main* function,

• $\mu$ has correctly computed the ranks of vertices strictly less than $i$,

• *Incorrect* is the set of vertices of rank $i-1$,

• for each $v \in V_{\text{Adam}}$, $\text{Count}(v)$ is the number of outgoing edges of $v$ to vertices of ranks strictly less than $i$.

The function *Init* ensures these properties for *i* = 1. To see that the invariant is preserved, note that each vertex *v* is updated at most once, and therefore each edge *u* → *v* is considered at most once, so *Count* is correctly updated. To get the overall *O*(*m*) complexity, we note that each vertex *v* is updated at most once over the course of the algorithm.

**Remark 7 (RAM versus Turing models of computation).** We note that in the complex-
ity analysis the cost of manipulating (and in particular incrementing) the counters for
the number of edges is constant, which holds in the unit cost RAM model of compu-
tation. The same algorithm analysed in the Turing model of computation would have
an additional $O(\log(n))$ multiplicative factor in the time complexity to take this into
account.

Subgames

Additionally to solving reachability games, the notion of attractors induces a common
way of constructing traps and subgames. This discussion is very closely related to the
notion of traps defined in Section 1.7, but some extra care is required because of the
edge labelling convention.

Let $\mathcal{G}$ a game and $F \subseteq E$ a subset of edges. By definition of the attractor:

• for every $u \in V_{\text{Adam}} \setminus \text{Attr}_{\text{Eve}}(F)$, there exists $u \to v \in E$ which is not in $F$ and $v \in V \setminus \text{Attr}_{\text{Eve}}(F)$, and
• for every $u \in V_{\text{Eve}} \setminus \text{Attr}_{\text{Eve}}(F)$, for all $e = u \to v \in E$, we have $e \notin F$ and $v \in V \setminus \text{Attr}_{\text{Eve}}(F)$.

This means that we can define the subgame $\mathcal{G} \setminus \text{Attr}_{\text{Eve}}(F)$ as follows: the set of vertices is $V \setminus \text{Attr}_{\text{Eve}}(F)$, and the set of edges $\mathcal{G}$ to the subset of $E \setminus F$ where both incoming and outgoing vertices are in $V \setminus \text{Attr}_{\text{Eve}}(F)$. The colouring function and the condition are naturally induced from $\mathcal{G}$ to $\mathcal{G} \setminus \text{Attr}_{\text{Eve}}(F)$.

Let us emphasise a subtlety here: indeed $V \setminus \text{Attr}_{\text{Eve}}(F)$ is a trap for Eve, so we can define the subgame induced by the set of vertices $V \setminus \text{Attr}_{\text{Eve}}(F)$. But it is not the same as $\mathcal{G} \setminus \text{Attr}_{\text{Eve}}(F)$: in the latter we remove the edges in $F$, which may still be present in the induced subgame.

**Lemma 10** (Attractors induce subgames – statement for Adam). Let $\tau$ a strategy for Adam in the subgame $\mathcal{G} \setminus \text{Attr}_{\text{Eve}}(F)$, it induces a strategy $\tau'$ in $\mathcal{G}$ such that plays consistent with $\tau$ in $\mathcal{G} \setminus \text{Attr}_{\text{Eve}}(F)$ are in one-to-one correspondence with plays consistent with $\tau'$ in $\mathcal{G}$, in particular any play consistent with $\tau'$ stays forever in $\mathcal{G} \setminus \text{Attr}_{\text{Eve}}(F)$.

This very useful lemma is very heavily used when decomposing games, and in a small abuse of notations we identify the strategies $\tau$ and $\tau'$.

The analogous statement can be made for the subgame $\mathcal{G} \setminus \text{Attr}_{\text{Adam}}(F)$:

**Lemma 11** (Attractors induce subgames – statement for Eve). Let $\sigma$ a strategy for Eve in the subgame $\mathcal{G} \setminus \text{Attr}_{\text{Adam}}(F)$, it induces a strategy $\sigma'$ in $\mathcal{G}$ such that plays consistent with $\sigma$ in $\mathcal{G} \setminus \text{Attr}_{\text{Adam}}(F)$ or in one-to-one correspondence with plays consistent with $\sigma'$ in $\mathcal{G}$, in particular any play consistent with $\sigma'$ stays forever in $\mathcal{G} \setminus \text{Attr}_{\text{Adam}}(F)$.

## 2.2 Büchi games

Recall that the objective Büchi requires that the colour Win appears infinitely many times and CoBuchi requires that the colour Lose appears finitely many times.

**Theorem 14** (Positional determinacy and complexity of Büchi games). Büchi objectives are uniformly positionally determined<fnref n="1" />. There exists an algorithm for computing the winning regions of Büchi games in quadratic time, more precisely $O(mn)$, and linear space, more precisely $O(m)$.

We present two different yet very similar algorithms.

### A first algorithm

The following lemma implies Theorem 14.

**Lemma 12** (Fixed point characterisation of the winning region for Büchi games). Let $\mathcal{G}$ be a Büchi game.

• If $\text{Attr}_{\text{Eve}}(\text{Win}) = V$, then $W_{\text{Eve}}(\mathcal{G}) = V$.

<footnote n="1">¹See Remark 6 for the case of infinite games.</footnote>
• If $\text{Attr}_{\text{Eve}}(\text{Win}) \neq V$, let $\mathcal{G}' = \mathcal{G} \setminus \text{Attr}_{\text{Adam}}(V \setminus \text{Attr}_{\text{Eve}}(\text{Win}))$, then $W_{\text{Eve}}(\mathcal{G}) = W_{\text{Eve}}(\mathcal{G}')$.

*Proof.* We prove the first item. Let $\sigma$ be an attractor strategy ensuring to reach Win from $\text{Attr}_{\text{Eve}}(\text{Win}) = V$. We argue that $\sigma$ ensures Buchi (Win). Indeed a play consistent with $\sigma$ can be divided into infinitely many finite plays, each of them consistent with $\sigma$ until reaching Win, and starting from scratch from the next vertex onwards. Thus $\sigma$ is winning from V.

We now look at the second item. We first prove that $\text{Attr}_{\text{Adam}}(V \setminus \text{Attr}_{\text{Eve}}(\text{Win})) \subseteq W_{\text{Adam}}(\mathcal{G})$. Let $\tau_a$ denote an attractor strategy ensuring to reach $V \setminus \text{Attr}_{\text{Eve}}(\text{Win})$ from $\text{Attr}_{\text{Adam}}(V \setminus \text{Attr}_{\text{Eve}}(\text{Win}))$, and $\tau_c$ a counter-attractor strategy ensuring to never reach Win from $V \setminus \text{Attr}_{\text{Eve}}(\text{Win})$. We construct the strategy $\tau$ as the disjoint union of $\tau_a$ and $\tau_c$:

$$ \tau(v) = \begin{cases} \tau_a(v) & \text{if } v \in \text{Attr}_{\text{Adam}}(V \setminus \text{Attr}_{\text{Eve}}(\text{Win})) \setminus (V \setminus \text{Attr}_{\text{Eve}}(\text{Win})), \\ \tau_c(v) & \text{if } v \in V \setminus \text{Attr}_{\text{Eve}}(\text{Win}). \end{cases} $$

Any play consistent with $\tau$ is first consistent with $\tau_a$ until reaching $V \setminus \text{Attr}_{\text{Eve}}(\text{Win})$ and then is consistent with $\tau_c$ and stays there forever. In this second phase it does not visit Win, implying that the play visits Win finitely many times, so it is winning. Thus we have proved that $\text{Attr}_{\text{Adam}}(V \setminus \text{Attr}_{\text{Eve}}(\text{Win})) \subseteq W_{\text{Adam}}(\mathcal{G})$, implying $W_{\text{Eve}}(\mathcal{G}) \subseteq V \setminus \text{Attr}_{\text{Adam}}(V \setminus \text{Attr}_{\text{Eve}}(\text{Win}))$.

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}'$, thanks to Lemma 11 it induces a winning strategy in $\mathcal{G}$. $\square$

The algorithm is presented in pseudocode in Algorithm 2.2. For the complexity analysis, the algorithm performs at most $n$ recursive calls and each of them involves two attractor computations, implying the time complexity $O(mn)$.

<caption>**Algorithm 2.2:** The first quadratic time algorithm for solving Büchi games.</caption>

**Data:** A Büchi game.

**Function** Solve $(\mathcal{G})$:
$X \leftarrow \text{Attr}_{\text{Eve}}(\text{Win})$
**if** $X = V$ **then**
  $\lfloor$ **return** $V$
**else**
  Let $\mathcal{G}' = \mathcal{G} \setminus \text{Attr}_{\text{Adam}}(V \setminus X)$
  $\lfloor$ **return** Solve $(\mathcal{G}')$

Let us see how uniform positional determinacy follows from Lemma 12. The shortest proof is by induction on the number of vertices, and remark that in both cases in Lemma 12 this number decreases.

A more instructive proof proceeds by unfolding the fixed point computation. Let $\mathcal{G}_0 = \mathcal{G}$ the original game, and applying the computation yields a sequence of subgames
G₁, G₂, ..., Gₚ. Let us write Vₖ for the set of vertices of Gₖ, we have Attr<sub>Eve</sub><sup>Gₚ</sup>(Win) = Vₚ. Thanks to the lemma, we have W<sub>Eve</sub>(G) = Vₚ. The proof constructs a positional uniform winning strategy in Gₚ from W<sub>Eve</sub>(G), which thanks to Lemma 11 induces a positional uniform winning strategy in G from W<sub>Eve</sub>(G).

The case of Adam is a bit more complicated. For v /∈ Vₖ, the rank of v is the smallest k ∈ N such that v ∈ V \ Vₖ. Equivalently, v ∈ Vₖ₋₁ \ Vₖ.

For each k, let τ<sub>a,k</sub> denote an attractor strategy ensuring to reach Vₖ \ Attr<sub>Eve</sub><sup>Gₖ</sup>(Win) from Attr<sub>Adam</sub><sup>Gₖ</sup>(Vₖ \ Attr<sub>Eve</sub><sup>Gₖ</sup>(Win)), and τ<sub>c,k</sub> a counter-attractor strategy ensuring to never reach Win from Vₖ \ Attr<sub>Eve</sub><sup>Gₖ</sup>(Win). We construct the strategy τ in G as the disjoint union of all τ<sub>a,k</sub> and τ<sub>c,k</sub>:

$$
\tau(v) = \begin{cases} \tau_{a,k}(v) & \text{if } \mathrm{rank}(v) = k \text{ and } v \notin V_k \setminus \mathrm{Attr}_{\mathrm{Eve}}^{G_k}(\mathrm{Win}), \\ \tau_{c,k}(v) & \text{if } \mathrm{rank}(v) = k \text{ and } v \in V_k \setminus \mathrm{Attr}_{\mathrm{Eve}}^{G_k}(\mathrm{Win}). \end{cases}
$$

and argue that it ensures CoBuchi(Win). Note that τ is the disjoint union of positional strategies, it is positional. Consider a play consistent with τ starting from a vertex of rank k. In the first phase, the play is consistent with τ<sub>a,k</sub>. If we were playing in G<sub>k</sub>, this would go on until reaching V \ Attr<sub>Eve</sub><sup>G<sub>k</sub></sup>(Win). But since we are here playing in G, there is another possibility: that Eve chooses an edge leading outside of G<sub>k</sub>. In that case necessarily the next vertex is in G<sub>k-1</sub>, so it has smaller rank. In the second phase, which starts upon reaching V \ Attr<sub>Eve</sub><sup>G<sub>k</sub></sup>(Win), the play is consistent with τ<sub>c,k</sub>, and again two things can happen. Either the play remains in G<sub>k</sub>, so it is consistent with τ<sub>c,k</sub> forever, in which case it never sees Win and therefore satisfies CoBuchi(Win), or it exists G<sub>k</sub>, necessarily to reach G<sub>k-1</sub>, meaning that it reaches a vertex of smaller rank. Along any play consistent with τ the rank never increases, implying that it is eventually consistent with some τ<sub>c,k</sub> hence satisfies CoBuchi(Win).

A second algorithm

The following lemma induces a different algorithm with the same complexity. We
define the operator Pre<sub>Eve</sub><sup>Win</sup> on subsets of vertices: for Y ⊆ V,

$$
\mathrm{Pre}_{\mathrm{Eve}}^{\mathrm{Win}}(Y) = \{ v \in V_E : \exists v \xrightarrow{\mathrm{Win}} v' \in E, v' \in Y \} \cup \{ v \in V_A : \forall v \xrightarrow{\mathrm{Win}} v' \in E, v' \in Y \}.
$$

**Lemma 13** (Second fixed point characterisation of the winning region for Buchi games).
Let $\mathcal{G}$ a Büchi game. Then $W_{\text{Eve}}(\mathcal{G})$ is the greatest fixed point of the monotonic opera-
tor

$$
Y \mapsto \mathrm{Attr}_{\mathrm{Eve}} (\mathrm{Pre}_{\mathrm{Eve}}^{\mathrm{Win}}(Y)).
$$

*Proof.* Thanks to Theorem 4 the greatest fixed point is also the greatest post-fixed
point, so we need to show two properties:

• W<sub>Eve</sub>(G) is a post-fixed point, meaning W<sub>Eve</sub>(G) ⊆ Attr<sub>Eve</sub>(Pre<sub>Eve</sub><sup>Win</sup>(W<sub>Eve</sub>(G))).

• For all *post-fixed points* Y, we have *Y* ⊆ *W<sub>Eve</sub>(G)*.
We first show that $W_{Eve}(\mathscr{G}) \subseteq \text{Attr}_{Eve}(\text{Pre}_{Eve}^{\text{Win}}(W_{Eve}(\mathscr{G})))$. We actually show that $V \setminus \text{Attr}_{Eve}(\text{Pre}_{Eve}^{\text{Win}}(W_{Eve}(\mathscr{G}))) \subseteq W_{Adam}(\mathscr{G})$, implying the inclusion by complementing. Let $\tau$ be a counter-attractor strategy ensuring never to reach $\text{Pre}_{Eve}^{\text{Win}}(W_{Eve}(\mathscr{G}))$ from $V \setminus \text{Attr}_{Eve}(\text{Pre}_{Eve}^{\text{Win}}(W_{Eve}(\mathscr{G})))$. We additionally require that $\tau$ chooses Lose edges over Win edges whenever possible: for each $v \in V_{Adam} \cap (V \setminus \text{Attr}_{Eve}(\text{Pre}_{Eve}^{\text{Win}}(W_{Eve}(\mathscr{G})))$,
if there exists $v \xrightarrow{\text{Lose}} v'$ with $v' \notin \text{Attr}_{Eve}(\text{Pre}_{Eve}^{\text{Win}}(W_{Eve}(\mathscr{G})))$, define $\tau(v) = v \xrightarrow{\text{Lose}} v'$.

Let $\tau'$ a winning strategy from $W_{Adam}(\mathscr{G})$. We play the following strategy: play $\tau'$ from $W_{Adam}(\mathscr{G})$ and $\tau$ otherwise. Let us consider a play consistent with this strategy from $V \setminus \text{Attr}_{Eve}(\text{Pre}_{Eve}^{\text{Win}}(W_{Eve}(\mathscr{G})))$, and assume that it reaches an edge $v \xrightarrow{\text{Win}} v'$. If $v \in V_{Eve}$, since $v \notin \text{Pre}_{Eve}^{\text{Win}}(W_{Eve}(\mathscr{G}))$ this implies that $v' \in W_{Adam}(\mathscr{G})$. If $v \in V_{Adam}$, the additional property of $\tau'$ ensures that $v' \in W_{Adam}(\mathscr{G})$. Hence after reaching Win we switch to a winning strategy, so the strategy is winning from $V \setminus \text{Attr}_{Eve}(\text{Pre}_{Eve}^{\text{Win}}(W_{Eve}(\mathscr{G})))$.

Let $Y$ a post-fixed point, meaning $Y \subseteq \text{Attr}_{Eve}(\text{Pre}_{Eve}^{\text{Win}}(Y))$. We show that $W_{Eve}(\mathscr{G}) \subseteq Y$. Let $\sigma_a$ be an attractor strategy ensuring to reach $\text{Pre}_{Eve}^{\text{Win}}(Y)$ from $Y$. We also define a strategy $\sigma_p$: for $v \in V_{Eve}$, if $v \in \text{Pre}_{Eve}^{\text{Win}}(Y)$ there exists $v \xrightarrow{\text{Win}} v' \in E$ such that $v' \in Y$, let us define $\sigma_p(v) = v \to v'$. We define the strategy $\sigma$ as follows:

$$ \sigma(v) = \begin{cases} \sigma_a(v) & \text{if } v \in \text{Attr}_{Eve}(\text{Pre}_{Eve}^{\text{Win}}(Y)) \setminus \text{Pre}_{Eve}^{\text{Win}}(Y), \\ \sigma_p(v) & \text{if } v \in \text{Pre}_{Eve}^{\text{Win}}(Y). \end{cases} $$

We argue that $\sigma$ ensures Buchi (Win) from $Y$. Indeed a play consistent with $\sigma$ can be divided into infinitely many finite plays, each of them consistent with $\sigma_a$ until reaching $\text{Pre}_{Eve}^{\text{Win}}(Y)$, then one step consistent with $\sigma_p$ reaching Win, before starting from scratch in $Y$. $\square$

Lemma 12 directly transfers to Algorithm 2.3. We could also obtain uniform positional determinacy from Lemma 13, using a similar unfolding as for Lemma 12.

**Algorithm 2.3:** The second quadratic time algorithm for solving Büchi games.

**Data:** A Büchi game.

Y $\leftarrow$ V

repeat

| Y $\leftarrow$ \text{Attr}_{Eve}(\text{Pre}_{Eve}^{\text{Win}}(Y))

until $Y = \text{Attr}_{Eve}(\text{Pre}_{Eve}^{\text{Win}}(Y))$;

return Y

**Remark 8 (Comparison of the two algorithms).** Both algorithms have the same complexity but they are not equivalent: the number of recursive calls of the first algorithm may be strictly smaller than the number of iterations of the repeat loop in the second algorithm. Both can be extended into (different) algorithms for parity games and beyond; in this chapter we will work with the first algorithm.
## 2.3 Parity games

Recall that the *parity* objective extends Büchi and coBüchi objectives:

$$ \text{Parity} = \{ \rho \in [1, d]^\omega \mid \text{the largest priority appearing infinitely often in } \rho \text{ is even} \}. $$

**Theorem 15** (Positional determinacy and complexity of parity games). *Parity objectives are uniformly positionally determined<fnref n="2" />. There exists an algorithm for computing the winning regions of parity games in exponential time, and more precisely of complexity $O(mn^{d-1})$. The space complexity of $O(n)$.

Furthermore, solving parity games is in NP $\cap$ coNP.

To prove Theorem 15 we first construct a recursive algorithm for computing the winning regions of parity games. The algorithm is often called Zielonka's algorithm, or more accurately McNaughton Zielonka's algorithm. We refer to the reference section Section 2.6 for a discussion on this nomenclature. The NP $\cap$ coNP complexity bounds will be discussed at the end of this section.

The following lemma induces (half of) the recursive algorithm. Identifying a colour and its set of vertices we write $d$ for the set of vertices of priority $d$.

**Lemma 14** (Fixed point characterisation of the winning regions for parity games). *Let $\mathcal{G}$ be a parity game with priorities in $[1, d]$, and $d$ even. Let $\mathcal{G}' = \mathcal{G} \setminus \text{Attr}_{\text{Eve}}(d)$.*

* If $W_{\text{Adam}}(\mathcal{G}') = \emptyset$, then $W_{\text{Eve}}(\mathcal{G}) = V$.

* If $W_{\text{Adam}}(\mathcal{G}') \neq \emptyset$, let $\mathcal{G}'' = \mathcal{G} \setminus \text{Attr}_{\text{Adam}}(W_{\text{Adam}}(\mathcal{G}'))$, then $W_{\text{Eve}}(\mathcal{G}) = W_{\text{Eve}}(\mathcal{G}'')$.

Note that $\mathcal{G}'$ has priorities in $[1, d-1]$ and that if $W_{\text{Adam}}(\mathcal{G}') \neq \emptyset$, then $\mathcal{G}''$ has less vertices than $\mathcal{G}$.

*Proof.* We prove the first item. Let $\sigma_d$ be an attractor strategy ensuring to reach $d$ from $\text{Attr}_{\text{Eve}}(d)$. Consider a winning strategy for Eve from $V \setminus \text{Attr}_{\text{Eve}}(d)$ in $\mathcal{G}'$, it induces a strategy $\sigma'$ in $\mathcal{G}$. We construct a strategy $\sigma$ in $\mathcal{G}$ as the disjoint union of $\sigma_d$ on $\text{Attr}_{\text{Eve}}(d)$ and of $\sigma'$ on $V \setminus \text{Attr}_{\text{Eve}}(d)$. Any play consistent with $\sigma$ either enters $\text{Attr}_{\text{Eve}}(d)$ infinitely many times, or eventually remains in $V \setminus \text{Attr}_{\text{Eve}}(d)$ and is eventually consistent with $\sigma'$. In the first case it sees infinitely many times $d$, which is even and maximal, hence satisfies *Parity*, and in the other case since $\sigma'$ is winning the play satisfies *Parity*. Thus $\sigma$ is winning from $V$.

We now look at the second item. Let $\tau_a$ denote an attractor strategy ensuring to reach $W_{\text{Adam}}(\mathcal{G}')$ from $\text{Attr}_{\text{Adam}}(W_{\text{Adam}}(\mathcal{G}'))$. Consider a winning strategy for Adam from $W_{\text{Adam}}(\mathcal{G}')$ in $\mathcal{G}'$, it induces a strategy $\tau'$ in $\mathcal{G}$. Thanks to Lemma 10 $\tau'$ is a winning strategy in $\mathcal{G}$. 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}'))$ is not 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}')) \setminus W_{\text{Adam}}(\mathcal{G}')$, the strategy $\tau'$ on $W_{\text{Adam}}(\mathcal{G}')$ 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}')) \cup W_{\text{Adam}}(\mathcal{G}'')$ in $\mathcal{G}$.

<footnote n="2">²See Remark 6 for the case of infinite games.</footnote>
Indeed, any play consistent with this strategy in $\mathcal{G}$ either stays forever in $W_{Adam}(\mathcal{G}'')$ hence is consistent with $\tau''$ or enters $\text{Attr}_{Adam}(W_{Adam}(\mathcal{G}'))$, hence is eventually consistent with $\tau'$. In both cases this implies that the play is winning. Thus we have proved that $\text{Attr}_{Adam}(W_{Adam}(\mathcal{G}')) \cup W_{Adam}(\mathcal{G}'') \subseteq W_{Adam}(\mathcal{G})$.

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

To get the full algorithm we need the analogous lemma for the case where the maximal priority is odd. We do not prove the following lemma as it is the exact dual of the previous lemma, and the proof is the same swapping the two players.

**Lemma 15** (Dual fixed point characterisation of the winning regions for parity games). Let $\mathcal{G}$ be a parity game with priorities in $[1, d]$, and $d$ odd. Let $\mathcal{G}' = \mathcal{G} \setminus \text{Attr}_{Adam}(d)$.

* If $W_{Eve}(\mathcal{G}') = \emptyset$, then $W_{Adam}(\mathcal{G}) = V$.

* If $W_{Eve}(\mathcal{G}') \neq \emptyset$, let $\mathcal{G}'' = \mathcal{G} \setminus \text{Attr}_{Eve}(W_{Eve}(\mathcal{G}'))$, then $W_{Adam}(\mathcal{G}) = W_{Adam}(\mathcal{G}'')$.

The algorithm is presented in pseudocode in Algorithm 2.4.

The proofs of Lemma 14 and Lemma 15 also imply that parity games are positionally determined. Indeed, winning strategies are defined as disjoint unions of strategies constructed inductively.

We now perform a complexity analysis. Let us write $f(n,d)$ for the number of recursive calls performed by the algorithm on parity games with $n$ vertices and priorities in $[1, d]$. We have $f(n, 1) = f(0, d) = 0$, with the general induction:

$$f(n,d) \leq f(n,d-1) + f(n-1,d) + 2.$$

The term $f(n, d-1)$ corresponds to the recursive call to $\mathcal{G}'$ and the term $f(n-1, d)$ to the recursive call to $\mathcal{G}''$. We obtain $f(n, d) \leq n \cdot f(n, d-1) + 2n$, so $f(n, d) \leq 2n(1 + n + \cdots + n^{d-2}) = O(n^{d-1})$. In each recursive call we perform two attractor computations so the number of operations in one recursive call is $O(m)$. Thus the overall time complexity is $O(mn^{d-1})$.

We finish the proof of Theorem 15 by sketching the argument that solving parity games is in NP $\cap$ coNP. The first observation is that computing the winning regions of the one player variants of parity games can be done in polynomial time through a simple graph analysis that we do not detail here. The NP and coNP algorithms are the following: guess a winning positional strategy, and check whether it is winning by computing the winning regions of the one player game induced by the strategy. Guessing a strategy for Eve is a witness that the answer is yes so it yields an NP algorithm, and guessing a strategy for Adam yields a coNP algorithm.

Chapter 3 is devoted to the study of advanced algorithms for parity games.
**Algorithm 2.4:** A recursive algorithm for computing the winning regions of parity games.

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

**Function** SolveEven($\mathcal{G}$):
    $\mathcal{G}' \leftarrow \mathcal{G} \setminus \text{Attr}_{\text{Eve}}(d)$
    $X \leftarrow \text{SolveOdd}(\mathcal{G}')$ // $\mathcal{G}'$ has one less priority
    **if** $X = \emptyset$ **then**
        $\lfloor$ **return** $V$
    **else**
        $\mathcal{G}'' \leftarrow \mathcal{G} \setminus \text{Attr}_{\text{Adam}}(X)$
        **return** SolveEven($\mathcal{G}'$) // $\mathcal{G}''$ has less vertices

**Function** SolveOdd($\mathcal{G}$):
    **if** $d = 1$ **then**
        $\lfloor$ **return** $V$
    $\mathcal{G}' \leftarrow \mathcal{G} \setminus \text{Attr}_{\text{Adam}}(d)$
    $X \leftarrow \text{SolveEven}(\mathcal{G}')$ // $\mathcal{G}'$ has one less priority
    **if** $X = \emptyset$ **then**
        $\lfloor$ **return** $V$
    **else**
        $\mathcal{G}'' \leftarrow \mathcal{G} \setminus \text{Attr}_{\text{Eve}}(X)$
        **return** SolveOdd($\mathcal{G}'$) // $\mathcal{G}''$ has less vertices

**if** $d$ is even **then**
        $\lfloor$ SolveEven($\mathcal{G}$) $\lfloor$
    **else**
        $\lfloor$ SolveOdd($\mathcal{G}$) $\lfloor$
## 2.4 Proving half-positional determinacy for qualitative games

We define here a generic approach to proving half-positional determinacy results for qualitative objectives. Let us say that an objective $\Omega$ is *submixing* if:

$$ 
\begin{array}{lclclcl}
\text{if} & \rho_1 & = & \rho_1^0 & \rho_1^1 & \dots & \rho_1^\ell & \dots & \notin \Omega \\
\text{and} & \rho_2 & = & \rho_2^0 & \rho_2^1 & \dots & \rho_2^\ell & \dots & \notin \Omega, \\
\text{then:} & \rho_1 \bowtie \rho_2 & = & \rho_1^0 & \rho_2^0 & \rho_1^1 & \rho_2^1 & \dots & \rho_1^\ell & \rho_2^\ell & \notin \Omega.
\end{array}
$$

**Theorem 16** (Submixing property implies uniform half-positional determinacy). *Every prefix independent submixing objective is uniformly half-positionally determined over finite arenas.*

*Proof.* We proceed by induction over the following quantity: total outdegree of vertices controlled by Eve minus number of vertices controller by Eve. Since we assume that every vertex has an outgoing edge, the base case is when each vertex of Eve has only one successor. In that case Eve has only one strategy and it is positional, so the property holds.

In the inductive step, we consider a game $\mathcal{G}$ where Eve has a winning strategy $\sigma$. Let $v \in V_{Eve}$ with at least two successors. We partition the outgoing edges of $v$ in two non-empty subsets which we call $E_1^v$ and $E_2^v$. Let us define two games $\mathcal{G}_1$ and $\mathcal{G}_2$: the game $\mathcal{G}_1$ is obtained from $\mathcal{G}$ by removing the edges from $E_2^v$, and symmetrically for $\mathcal{G}_2$.

We claim that Eve has a winning strategy in either $\mathcal{G}_1$ or $\mathcal{G}_2$. Let us assume towards contradiction that this is not the case: then there exist $\tau_1$ and $\tau_2$ two strategies for Adam which are winning in $\mathcal{G}_1$ and $\mathcal{G}_2$ respectively. We construct a strategy $\tau$ for Adam in $\mathcal{G}$ as follows: it has two modes, 1 and 2. The initial mode is 1, and the strategy simulates $\tau_1$ from the mode 1 and $\tau_2$ from the mode 2. Whenever $v$ is visited, the mode is adjusted: if the outgoing edge is in $E_1^v$ then the new mode is 1, otherwise it is 2. To be more specific: when simulating $\tau_1$ we play ignoring the parts of the play using mode 2, so removing them yields a play consistent with $\tau_1$. The same goes for $\tau_2$.

Consider a play $\pi$ consistent with $\sigma$ and $\tau$. Since $\sigma$ is winning, the play $\pi$ is winning. It can be decomposed following which mode the play is in:

$$ 
\begin{array}{c}
\begin{array}{c}
\text{mode 1} \\
\text{mode 2}
\end{array} \\
\begin{array}{c}
\underbrace{\pi_1^0}_{v_0 \cdots v} \\
\underbrace{\vcenter{\hbox{\strut v \dots v}}}_{\pi_2^0} \\
\underbrace{\pi_1^1}_{v \cdots v} \\
\underbrace{\vcenter{\hbox{\strut v \dots v}}}_{\pi_2^1}
\end{array} \\
\begin{array}{c}
\dots \\
\dots
\end{array}
\end{array}
$$

where $\pi_1 = \pi_1^0 \pi_1^1 \cdots$ is consistent with $\tau_1$ and $\pi_2 = \pi_2^0 \pi_2^1 \cdots$ is consistent with $\tau_2$. Since $\tau_1$ and $\tau_2$ are winning strategies for Adam, $\pi_1$ and $\pi_2$ do not satisfy $\Omega$.

There are two cases: the decomposition is either finite or infinite. If it is finite we get a contradiction: since $\pi$ is winning and $\Omega$ is prefix independent any suffix of $\pi$ is winning as well, contradicting that it is consistent with either $\tau_1$ or $\tau_2$ hence cannot be winning. In the second case, the submixing property directly yields a contradiction: neither $\pi_1$ nor $\pi_2$ satisfy $\Omega$, yet their shuffle $\pi$ does. $\square$
## 2.5 Rabin, Streett, and Muller games

The prefix independent objectives we studied so far are Büchi, CoBüchi, and their joint extension the parity objectives. The definition of the latter may seem a bit arbitrary; the study of Muller objectives will show how parity objectives naturally emerge as a well-behaved class of objectives.

Let us start with a very general class of infinitary objectives, where infinitary means that the objective only considers the set of colours appearing infinitely many times. For a sequence $\rho$, we let $\text{Inf}(\rho)$ denote the set of colours appearing infinitely many times in $\rho$. The Muller objective is over the set of colours $C = [1, d]$ and is parametrised by some $\mathcal{F} \subseteq 2^C$, i.e. a family of subsets of $C$. The objective is defined as follows:

$$ \text{Muller}(\mathcal{F}) = \{\rho \in C^\omega : \text{Inf}(\rho) \in \mathcal{F}\}. $$

Muller objectives include any objective specifying the set of colours appearing infinitely often. There are different possible representations for a Muller objective, for instance using logical formulas or circuits. We will here consider the most natural one which simply consists in listing the elements of $\mathcal{F}$. Note that $\mathcal{F}$ can have size up to $2^{2^d}$, and each element of $\mathcal{F}$ (which is a subset of $C$) requires up to $d$ bits to be identified, so the representation of $\mathcal{F}$ can be very large.

We note that the complement of a Muller objective is another Muller objective: $C^\omega \setminus \text{Muller}(\mathcal{F}) = \text{Muller}(2^C \setminus \mathcal{F})$. In particular if Eve has a Muller objective then Adam also has a Muller objective.

To define subclasses of Muller objectives we make assumptions on $\mathcal{F} \subseteq 2^C$. We say that $\mathcal{F}$ is closed under union if whenever $X, Y \in \mathcal{F}$ then $X \cup Y \in \mathcal{F}$. Let us define Streett objectives as the subclass of Muller objectives given by $\mathcal{F}$ closed under union. The following purely combinatorial lemma gives a nice characterisation of these objectives.

**Lemma 16 (Characterisation of Streett among Muller objectives).** A collection $\mathcal{F} \subseteq 2^C$ is closed under union if and only if there exists a set of pairs $(R_i, G_i)_{i \in [1, d]}$ with $R_i, G_i \subseteq C$ such that $X \in \mathcal{F}$ is equivalent to for all $i \in [1, d]$, if $X \cap R_i \neq \emptyset$ then $X \cap G_i \neq \emptyset$.

We will see in Section 2.6 a natural and optimised way to construct these pairs using the Zielonka tree. In the meantime let us give a direct proof of this result.

*Proof.* Let $\mathcal{F}$ closed under union. We note that for any $S \notin \mathcal{F}$, either no subsets of $S$ are in $\mathcal{F}$ or there exists a maximal subset $S'$ of $S$ in $\mathcal{F}$: indeed it is the union of all subsets of $S$ in $\mathcal{F}$. It directly follows that for a subset $X$ we have the following equivalence: $X \in \mathcal{F}$ if and only if for any $S \notin \mathcal{F}$, if $X \subseteq S$ then $X \subseteq S'$. This is rewritten equivalently as: if $X \cap (C \setminus S') \neq \emptyset$ then $X \cap (C \setminus S) \neq \emptyset$. Hence a suitable set of pairs satisfying the required property is $\{(C \setminus S', C \setminus S) : S \notin \mathcal{F}\}$. $\square$

Thanks to this lemma we can give a direct definition of Streett objectives. The set of colours is $C = [1, d]$, and we consider a family of subsets $G_1, R_1, \dots, G_d, R_d \subseteq C$.

$$ \text{Streett} = \{\rho \in C^\omega : \forall i \in [1, d], R_i \cap \text{Inf}(\rho) \neq \emptyset \implies G_i \cap \text{Inf}(\rho) \neq \emptyset\}. $$
It is customary to call $R_i$ the $i^{th}$ request and $G_i$ the corresponding response; with this terminology the Streett objective requires that every request made infinitely many times must be responded to infinitely many times.

The Rabin objectives are the complement of the Streett objectives:

$$ \mathbf{Rabin} = \{ \rho \in C^\omega : \exists i \in [1, d], R_i \cap \mathrm{Inf}(\rho) \neq \emptyset \wedge G_i \cap \mathrm{Inf}(\rho) = \emptyset \}. $$

## McNaughton algorithm: an exponential time algorithm for Muller games

**Theorem 17** (Finite memory determinacy and complexity for Muller games). *Muller objectives are determined with finite memory strategies of size $d$.$^3$ There exists an algorithm for computing the winning regions of Muller games in exponential time, and more specifically of complexity $O(dm dn^{d-1})$, and in polynomial space, and more specifically $O(dm)$.*

The complexity will be improved later in this chapter. The presentation of the recursive algorithm for computing the winning regions of Muller games follows the exact same lines as for parity games: indeed, the Muller objective extends the parity objective, and specialising the algorithm for Muller games to parity games yields the algorithm we presented above.

The following lemma induces the recursive algorithm for computing the winning regions of Muller games.

**Lemma 17** (Fixed point characterisation of the winning regions for Muller games). *Let $\mathcal{G}$ be a Muller game such that $C \in \mathcal{F}$. For each $c \in C$, let $\mathcal{G}_c = \mathcal{G} \setminus \mathrm{Attr}_{\mathrm{Eve}}(c)$.*

* If for all $c \in C$, we have $W_{\mathrm{Adam}}(\mathcal{G}_c) = \emptyset$, then $W_{\mathrm{Eve}}(\mathcal{G}) = V$.

* If there exists $c \in C$ such that $W_{\mathrm{Adam}}(\mathcal{G}_c) \neq \emptyset$, let $\mathcal{G}' = \mathcal{G} \setminus \mathrm{Attr}_{\mathrm{Adam}}(W_{\mathrm{Adam}}(\mathcal{G}_c))$, then $W_{\mathrm{Eve}}(\mathcal{G}) = W_{\mathrm{Eve}}(\mathcal{G}')$.

*Proof.* We prove the first item.

For each $c \in C$, let $\sigma_c$ be an attractor strategy ensuring to reach $c$ from $\mathrm{Attr}_{\mathrm{Eve}}(c)$, and consider a winning strategy for Eve from $V \setminus \mathrm{Attr}_{\mathrm{Eve}}(c)$ in $\mathcal{G}_c$, it induces a strategy $\sigma'_c$ in $\mathcal{G}$. We construct a strategy $\sigma$ in $\mathcal{G}$ which will simulate the strategies above in turn; to do so it uses $C$ as top-level memory states. (We note that the strategies $\sigma'_c$ may use memory as well, so $\sigma$ may actually use more memory than just $C$.) The strategy $\sigma$ with memory $c$ simulates $\sigma_c$ from $\mathrm{Attr}_{\mathrm{Eve}}(c)$ and $\sigma'_c$ from $V \setminus \mathrm{Attr}_{\mathrm{Eve}}(c)$, and if it ever reaches $c$ it updates its memory state to $c+1$ and $1$ if $c=d$. Any play consistent with $\sigma$ either updates its memory state infinitely many times, or eventually remains in $V \setminus \mathrm{Attr}_{\mathrm{Eve}}(c)$ and is eventually consistent with $\sigma'_c$. In the first case it sees each colour infinitely many times, and since $C \in \mathcal{F}$ the play satisfies Muller($\mathcal{F}$), and in the other case since $\sigma'_c$ is winning the play satisfies Muller($\mathcal{F}$). Thus $\sigma$ is winning from $V$.

We now look at the second item.

Let $\tau_d$ denote an attractor strategy from $\mathrm{Attr}_{\mathrm{Adam}}(W_{\mathrm{Adam}}(\mathcal{G}_c)) \setminus W_{\mathrm{Adam}}(\mathcal{G}_c)$. Consider a winning strategy for Adam from $W_{\mathrm{Adam}}(\mathcal{G}_c)$ in $\mathcal{G}_c$, it induces a strategy $\tau_c$ in

<footnote>$^3$See Remark 6 for the case of infinite games.</footnote>
G. Thanks to Lemma 10, this implies that $\tau_c$ is a winning strategy in $\mathcal{G}$. 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}))$ 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})) \setminus W_{\text{Adam}}(\mathcal{G}_c)$, the strategy $\tau_c$ on $W_{\text{Adam}}(\mathcal{G}_c)$ 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}_c)) \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}_c))$, so it is eventually consistent with $\tau_c$. 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, any play consistent with $\sigma$ stays forever in $W_{\text{Eve}}(\mathcal{G}')$, implying that $\sigma$ is winning from $W_{\text{Eve}}(\mathcal{G}')$ in $\mathcal{G}$. $\square$

To get the full algorithm we need the analogous lemma for the case where $C \notin \mathcal{F}$. We do not prove it as it is the exact dual of the previous lemma, and the proof is the same swapping the two players.

**Lemma 18 (Dual fixed point characterisation of the winning regions for Muller games).**
Let $\mathcal{G}$ be a Muller game such that $C \notin \mathcal{F}$. For each $c \in C$, let $\mathcal{G}_c = \mathcal{G} \setminus \text{Attr}_{\text{Adam}}(c)$.

* If for all $c \in C$, we have $W_{\text{Eve}}(\mathcal{G}_c) = \emptyset$, then $W_{\text{Adam}}(\mathcal{G}) = V$.

* If there exists $c \in C$ such that $W_{\text{Eve}}(\mathcal{G}_c) \neq \emptyset$, let $\mathcal{G}' = \mathcal{G} \setminus \text{Attr}_{\text{Eve}}(W_{\text{Eve}}(\mathcal{G}_c))$, then $W_{\text{Adam}}(\mathcal{G}) = W_{\text{Adam}}(\mathcal{G}')$.

The algorithm is presented in pseudocode in Algorithm 2.5. We only give the case where $C \in \mathcal{F}$, the other case being symmetric. The base case is when there is only one colour $c$, in which case Eve wins everywhere if $\mathcal{F} = \{c\}$ and Adam wins everywhere if $\mathcal{F} = \emptyset$.

We now perform a complexity analysis of the algorithm. Let us write $f(n,d)$ for the number of recursive calls performed by the algorithm on Muller games with $n$ vertices and $d$ colours. We have $f(n, 1) = f(0, d) = 0$, with the general induction:

$$f(n,d) \leq d \cdot f(n,d-1) + f(n-1,d) + d + 1.$$

The term $d \cdot f(n,d-1)$ corresponds to the recursive calls to $\mathcal{G}_c$ for each $c \in C$ and the term $f(n-1,d)$ to the recursive call to $\mathcal{G}'$. We obtain $f(n,d) \leq dn \cdot f(n,d-1) + (d+1)n$, so $f(n,d) \leq (d+1)n(1+dn+(dn)^2+\dots+(dn)^{d-2}) = O((dn)^{d-1})$. In each recursive call we perform $d+1$ attractor computations so the number of operations in one recursive call is $O(dm)$. Thus the overall time complexity is $O(dm dn^{d-1})$.

The proofs of Lemma 17 and Lemma 18 also imply that Muller games are determined with finite memory of size $d!$. We do not make it more precise here because an improved analysis of the memory requirements will be conducted in Section 2.6 using a variant of this algorithm.
**Algorithm 2.5:** A recursive algorithm for computing the winning regions of Muller games.

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

**Function** SolveIn($\mathcal{G}$):

// Assumes $C \in \mathcal{F}$

if $C = \{c\}$ then

return $V$

for $c \in C$ do

$\mathcal{G}_c \leftarrow \mathcal{G} \setminus \text{Attr}_{\text{Eve}}^c(c)$

if $C \setminus \{c\} \in \mathcal{F}$ then

[$W_{\text{Eve}}(\mathcal{G}_c) \leftarrow \text{SolveIn}(\mathcal{G}_c) // \mathcal{G}_c$ has one colour less

else

[$W_{\text{Eve}}(\mathcal{G}_c) \leftarrow \text{SolveOut}(\mathcal{G}_c) // \mathcal{G}_c$ has one colour less

if $\forall c \in C, W_{\text{Adam}}(\mathcal{G}_c) = \emptyset$ then

return $V$

else

Let $c$ such that $W_{\text{Adam}}(\mathcal{G}_c) \neq \emptyset$

$\mathcal{G}' \leftarrow \mathcal{G} \setminus \text{Attr}_{\text{Adam}}^c(W_{\text{Adam}}(\mathcal{G}_c))$

return SolveIn($\mathcal{G}'$) // $\mathcal{G}'$ has less vertices

**Function** SolveOut($\mathcal{G}$):

[$W_{\text{Adam}}(\mathcal{G}) \leftarrow \text{SolveOut}(\mathcal{G})$ // Symmetric to SolveIn, assumes $C \notin \mathcal{F}$

if $C \in \mathcal{F}$ then

SolveIn($\mathcal{G}$)

else

SolveOut($\mathcal{G}$)
## Half-positional determinacy for Rabin games

**Theorem 18 (Half-positional determinacy for Rabin games).** *Rabin games are uniformly half-positionally determined.*

Theorem 18 is a direct corollary of Theorem 16, since the Rabin objective is prefix independent and submixing. Indeed, let $(\rho_1^\ell)_{\ell \in \mathbb{N}}$ and $(\rho_2^\ell)_{\ell \in \mathbb{N}}$ such that:

$$ 
\begin{array}{l @{\qquad} l @{\qquad} l @{\qquad} l @{\qquad} l @{\qquad} l}
\text{and} & \rho_1 & = & \rho_1^0 & \rho_1^1 & \dots & \rho_1^\ell & \dots & \notin \text{Rabin} \\
\text{then:} & \rho_2 & = & \rho_2^0 & \rho_2^1 & \dots & \rho_2^\ell & \dots & \notin \text{Rabin}, \\
& \rho_1 \bowtie \rho_2 & = & \rho_1^0 & \rho_2^0 & \rho_1^1 & \rho_2^1 & \dots & \notin \text{Rabin}.
\end{array}
$$

Since neither $\rho_1$ nor $\rho_2$ satisfy Rabin, in both for all $i \in [1, d]$ if $R_i \cap \text{Inf}(\rho) \neq \emptyset$, then $G_i \cap \text{Inf}(\rho) \neq \emptyset$. Since $\text{Inf}(\rho_1 \bowtie \rho_2) = \text{Inf}(\rho_1) \cup \text{Inf}(\rho_2)$, this implies that $\rho_1 \bowtie \rho_2$ does not satisfy Rabin.

Theorem 18 holds for infinite games. However the proof using the submixing property only applies to finite games and does not easily extend to infinite ones. A different approach is required to obtain the positional determinacy result for infinite games, see Theorem 25.

## The complexity of solving Rabin games

**Theorem 19 (Complexity of solving Rabin games).** *Solving Rabin games is NP-complete.*

*Proof.* The proof that solving Rabin games is in NP follows the same lines as for solving parity games: the algorithm guesses a positional strategy and checks whether it is indeed winning. This requires proving that solving Rabin games where Adam control all vertices can be done in polynomial time, which is indeed true and easy to see so we will not elaborate further on this.

To prove the NP-hardness we reduce the satisfiability problem for boolean formulas in conjunctive normal form (SAT) to solving Rabin games.

Let $\Phi$ be a formula in conjunctive normal form with $n$ variables $x_1...x_n$ and $m$ clauses $C_1...C_m$, where each $C_j$ is of the form $\ell_{j_1} \lor \ell_{j_2} \lor \ell_{j_3}$:

$$ \Phi = \bigwedge_{j=1}^{m} \ell_{j_1} \lor \ell_{j_2} \lor \ell_{j_3}. $$

A literal $\ell$ is either a variable $x$ or its negation $\bar{x}$, and we write $\bar{\ell}$ for the negation of a literal. The question whether $\Phi$ is satisfiable reads: does there exist a valuation $v: \{x_1, ..., x_n\} \to \{0, 1\}$ satisfying $\Phi$.

We construct a Rabin game $\mathcal{G}$ with $m+1$ vertices (one per clause, all controlled by Eve, plus a unique vertex controlled by Adam), $4m$ edges (4 per clause), and $2n$ Rabin pairs (one per literal). We will show that the formula $\Phi$ is satisfiable if and only if Eve has a winning strategy in the Rabin game $\mathcal{G}$.

We first describe the Rabin condition. There is a Rabin pair $(R_\ell, G_\ell)$ for each literal $\ell$, so the Rabin condition requires that there exists a literal $\ell$ such that $R_\ell$ is visited infinitely many times and $G_\ell$ is not. Let us now describe the arena. A play
<figure><img src="image_16.png" /><figcaption>Figure 2.1: The Rabin game for $\Phi = (x \lor y \lor z) \land (x \lor \bar{y} \lor \bar{z}) \land (\bar{x} \lor y \lor \bar{z})$.</figcaption></figure>

consists in an infinite sequence of rounds, where in each round first Adam chooses a clause and second Eve chooses a literal in this clause. When Eve chooses a literal $ℓ$ she visits $R_ℓ$ and $G_{\bar{ℓ}}$. This completes the description of the Rabin game $\mathcal{G}$, it is illustrated in Figure 2.1. Let us now prove that this yields a reduction from SAT to solving Rabin games.

Let us first assume that $\Phi$ is satisfiable, and let $v$ be a satisfying assignment: there is a literal $ℓ$ in each clause satisfied by $v$. Let $\sigma$ be the memoryless strategy choosing such a literal in each clause. We argue that in any play consistent with $\sigma$ there is at least one literal $ℓ$ that Eve chooses infinitely many times without ever choosing $\bar{ℓ}$; this implies that $R_ℓ$ is visited infinitely often and $G_ℓ$ is not. Indeed, some clause is chosen infinitely many times, so the corresponding literal chosen by Eve is also chosen infinitely many times. Since all the literals chosen by Eve satisfy the same assignment $v$ she does not choose both a literal and its negation, so she never chooses $\bar{ℓ}$. It follows that $\sigma$ is a winning strategy for Eve.

Conversely, let us assume that Eve has a winning strategy. Thanks to Theorem 18 she has a positional winning strategy $\sigma$. We argue that $\sigma$ cannot choose some literal $ℓ$ in some clause $C$ and the literal $\bar{ℓ}$ in another clause $C'$. If this would be the case, consider the strategy of Adam alternating between the two clauses $C$ and $C'$ and play it against $\sigma$: both $ℓ$ and $\bar{ℓ}$ are chosen infinitely many times, and no other literals. Hence $R_ℓ, G_ℓ, R_{\bar{ℓ}},$ and $G_{\bar{ℓ}}$ are all visited infinitely many times, implying that this play does not satisfy Rabin, contradicting that $\sigma$ is winning.

There exists a valuation $v$ which satisfies each literal chosen by Eve, implying that it satisfies $\Phi$ which is then satisfiable. $\square$
## The complexity of solving Muller games

**Theorem 20 (Complexity of solving Muller games).** *Solving Muller games is PSPACE-complete.*

As for the previous reduction, in the Muller game constructed in the reduction below we label edges rather than vertices, and some edges have more than one colour. As for Rabin games this can be reduced to the original definition of colouring functions (labelling vertices with exactly one colour each) with a polynomial increase in size.

*Proof.* The PSPACE algorithm was constructed in Theorem 17.

To prove the PSPACE-hardness we reduce the evaluation of quantified boolean formulas in disjunctive normal form (QBF) to solving Muller games.

Let $\Psi$ be a quantified boolean formula in disjunctive normal form with $n$ variables $x_1...x_n$ and $m$ clauses $C_1...C_m$, where each $C_j$ is of the form $\ell_{j_1} \wedge \ell_{j_2} \wedge \ell_{j_3}$:

$$ \Psi = \exists x_1, \forall x_2, \dots, \exists x_n, \Phi(x_1, \dots, x_n) \text{ and } \Phi(x_1, \dots, x_n) = \bigvee_{j=1}^{m} \ell_{j_1} \wedge \ell_{j_2} \wedge \ell_{j_3}. $$

We construct a Muller game $\mathcal{G}$ with $m+1$ vertices (one per clause, all controlled by Adam, plus a unique vertex controlled by Eve), $4m$ edges (4 per clause), and $2n$ colours (one per literal). We will show that the formula $\Psi$ evaluates to true if and only if Eve has a winning strategy in the Muller game $\mathcal{G}$.

We first describe the Muller condition. The set of colours is the set of literals. We let $x$ denote the lowest quantified variable such that $x$ or $\bar{x}$ is visited infinitely many times. The Muller condition requires that:

* either $x$ is existential and only one of $x$ and $\bar{x}$ is visited infinitely many times,

* or $x$ is universal and both $x$ and $\bar{x}$ are visited infinitely many times,

and for all variables $y$ quantified after $x$, both $y$ and $\bar{y}$ are visited infinitely many times. Formally, let $S_{>i} = \{x_q, \bar{x}_q : q > p\}$ and:

$$ \mathcal{F} = \{S_{>p}, \{x_p\} \cup S_{>p}, \{\bar{x}_p\} \cup S_{>p} : x_p \text{ existential}\} \cup \{S_{\ge p} : x_p \text{ universal}\}. $$

Note that $\mathcal{F}$ contains $O(n)$ elements.

Let us now describe the arena. A play consists in an infinite sequence of rounds, where in each round first Eve chooses a clause and second Adam chooses a literal $\ell$ in this clause corresponding to some variable $x_p$, and visits the colour $\ell$ as well as each colour in $S_{>p}$.

The reduction is illustrated in Figure 2.2. Note that the edges from the vertex controlled by Eve to the other ones do not have a colour, which does not fit our definitions. For this reason we introduce a new colour $c$ and colour all these edges by $c$. We define a new Muller objective by adding $c$ to each set in $\mathcal{F}$: since every play in the game visit $c$ infinitely many times, the two games are equivalent. We note that this construction works for this particular game but not in general.
For a valuation $v: \{x_1, \dots, x_n\} \to \{0, 1\}$ and $p \in [1, n]$, we write $\Psi_{v,p}$ for the formula obtained from $\Psi$ by fixing the variables $x_1, \dots, x_{p-1}$ to $v(x_1), \dots, v(x_{p-1})$ and quantifying only over the remaining variables. Let us say that a valuation $v$ is positive if for every $p \in [1, n]$, the formula $\Psi_{v,p}$ evaluates to true, and similarly a valuation is negative if for every $p \in [1, n]$, the formula $\Psi_{v,p}$ evaluates to false.

Let us first assume that $\Psi$ evaluates to true. We construct a winning strategy $\sigma$ for Eve. It uses positive valuations over the variables $x_1, \dots, x_n$ as memory states. Note that the fact that $\Psi$ evaluates to true implies that there exists a positive valuation. Let us choose an arbitrary positive valuation as initial valuation. We first explain what the strategy $\sigma$ does and then how to update its memory.

Assume that the current valuation is $v$, since it is positive there exists a clause satisfying $v$, the strategy $\sigma$ chooses such a clause. Therefore, any literal that Adam chooses is necessarily true under $v$.

The memory is updated as follows: assume that the current valuation is $v$ and that Adam chose a literal corresponding to the variable $x_p$. If $x_p$ is existential the valuation is unchanged. If $x_p$ is universal, we construct a new positive valuation as follows. We swap the value of $x_p$ in $v$ and write $v[x_p]$ for this new valuation. Since $v$ is positive and $x_p$ is universally quantified, the formula $\Psi_{v[x_p],p+1}$ evaluates to true, so there exists a positive valuation $v_{p+1}: \{x_{p+1}, \dots, x_n\} \to \{0, 1\}$ for this formula. The new valuation is defined as follows:

$$ v'(x_q) = \begin{cases} v(x_q) & \text{if } q < p, \\ \overline{v(x_q)} & \text{if } q = p, \\ v_{p+1}(x_q) & \text{if } q > p, \end{cases} $$

it is positive by construction.

Let $\pi$ be a play consistent with $\sigma$ and $x_p$ be the lowest quantified variable chosen infinitely many times by Adam. First, all colours in $S_{>p}$ are visited infinitely many times (when visiting $x$ or $\bar{x}$). Let us look at the sequence $(v_i(x_p))_{i \in \mathbb{N}}$ where $v_i$ is the valuation in the $i^{th}$ round. If $x_p$ is existential, the sequence is ultimately constant as it can only change when a lower quantified variable is visited. If $x_p$ is universal, the value changes each time the variable $x_p$ is chosen. Since any literal that Adam chooses is necessarily true under the current valuation, this implies that in both cases $\pi$ satisfies Muller($\mathcal{F}$).

For the converse implication we show that if $\Psi$ evaluates to false, then there exists a winning strategy $\tau$ for Adam. The construction is similar but using negative valuations. The memory states are negative valuations. The initial valuation is any negative valuation. If the current valuation is $v$ and Eve chose the clause $C$, since the valuation is negative $v$ does not satisfy $C$, the strategy $\tau$ chooses a literal in $C$ witnessing this failure. The memory is updated as follows: assume that the current valuation is $v$ and that the strategy $\tau$ chose a literal corresponding to the variable $x_p$. If $x_p$ is universal the valuation is unchanged. If $x_p$ is existential, we proceed as above to construct another negative valuation where the value of $x_p$ is swapped.

Let $\pi$ be a play consistent with $\tau$ and $x$ be the lowest quantified variable chosen infinitely many times by Adam. As before, we look at the sequence $(v_i(x))_{i \in \mathbb{N}}$ where
<figure><img src="image_17.png" /><figcaption>Figure 2.2: The Muller game for $\Psi = \exists x, \forall y, \exists z, (x \land y \land z) \lor (x \land \bar{y} \land \bar{z}) \lor (\bar{x} \land y \land \bar{z})$. For a variable $v$ we write $S_{>v}$ for the set of literals corresponding to variables quantified after $v$, so for instance $S_{>x} = \{y, \bar{y}, z, \bar{z}\}$.</figcaption></figure>

$v_i$ is the valuation in the $i^{th}$ round. If $x$ is existential, the value changes each time the variable $x$ is chosen. If $x$ is universal, the sequence is ultimately constant. Since any literal that Adam chooses is necessarily false under the current valuation, this implies that in both cases $\pi$ does not satisfy $\text{Muller}(\mathcal{F})$. $\square$

## 2.6 Zielonka tree

The Zielonka tree is a combinatorial structure associated with a Muller objective which very neatly exposes its properties. As a warm-up we first present its predecessor the LAR construction, and then show the properties of Zielonka trees. As we will see, the key feature of the Zielonka tree of a Muller objective $\text{Muller}(\mathcal{F})$ is to characterise its exact memory requirements.

### The latest appearance record

Muller objectives can be reduced to parity objectives, see Section 1.6 for an introduction to reductions between objectives.

**Theorem 21** (Latest Appearance Record (LAR) construction). Let $C = [1, d]$ be a set of colours and $\text{Muller}(\mathcal{F})$ a Muller objective. There exists a deterministic parity automaton $\text{LAR}_{\mathcal{F}}$ over the alphabet $C$ defining $\text{Muller}(\mathcal{F})$. It has $d!$ states and has priorities in $[1, 2d]$.

LAR stands for *Latest Appearance Record*. In the literature the number of states is often $d \cdot d!$ instead of $d!$, the multiplicative factor $d$ is saved since we consider transition-based acceptance conditions for automata.
*Proof.* We define the automaton $\text{LAR}_{\mathcal{F}}$. The set of states is the set of lists of all colours of $C$ without repetitions. We represent a list by $(c_1, \dots, c_d)$. The initial state is irrelevant because $\text{Muller}(\mathcal{F})$ is prefix independent. The transition function is defined as follows: $\delta(\ell, c)$ is $\ell'$ obtained from $\ell$ by pushing $c$ to the first position (hence shifting to the right the elements to the left of $c$). This is best understood on an example:

$$ \delta((4, 1, 2, 3), 2) = (2, 4, 1, 3). $$

Let $j$ be the position of $c$ in $\ell$, the priority of this transition is defined by:

$$ c((\ell, c, \ell')) = \begin{cases} 2j & \text{if } \ell([1, j]) \in \mathcal{F}, \\ 2j-1 & \text{otherwise.} \end{cases} $$

We now show that the automaton $\text{LAR}_{\mathcal{F}}$ defines $\text{Muller}(\mathcal{F})$. Let $\rho = c_0c_1\dots$ be an infinite word over the alphabet $C$. Let us consider the run of $\text{LAR}_{\mathcal{F}}$ over $\rho$:

$$ (\ell_0, c_0, \ell_1)(\ell_1, c_1, \ell_2)\dots $$

Let us write $j_i$ for the position of $c_i$ in $\ell_i$. We consider $\text{Inf}(\rho)$ the set of colours appearing infinitely many times and write $j$ for its cardinal. From some point onwards the lists $\ell_i$ are of the form

$$ \underbrace{(c_1, \dots, c_j)}_{\text{Inf}(\rho)}, \underbrace{c_{j+1}, \dots, c_d)}_{C \setminus \text{Inf}(\rho)}. $$

From this point on $j_i$ is smaller than or equal to $j$, and it reaches $j$ infinitely many times. It follows that the largest priority appearing infinitely many times in the run is $2j$ if $\text{Inf}(\rho) \in \mathcal{F}$ and $2j-1$ if $\text{Inf}(\rho) \notin \mathcal{F}$. Thus $\rho$ is accepted by $\text{LAR}_{\mathcal{F}}$ if and only if $\text{Inf}(\rho) \in \mathcal{F}$, as desired. $\square$

## The Zielonka tree

Theorem 21 implies a reduction from Muller games to parity games as explained in Section 1.6. This yields a small improvement from the complexity results we already obtained for Muller games in Theorem 17, but not for the memory requirements. One weakness of the LAR construction is that its size depends only on the number of colours, and not on the properties of $\mathcal{F}$. The Zielonka tree is an improved take on the LAR.

**Definition 3 (Zielonka tree).** Let $\text{Muller}(\mathcal{F})$ be a Muller objective over the set of colours $C$. The Zielonka tree $T_{\mathcal{F}}$ of $\text{Muller}(\mathcal{F})$ is a rooted tree with nodes labelled by subsets of colours, it is constructed inductively as follows:

* the root is labelled $C$,

* the children of a node labelled $S$ are the maximal subsets $S_1, \dots, S_k$ of $S$ such that $S_i \in \text{Muller}(\mathcal{F}) \iff S \notin \text{Muller}(\mathcal{F})$.
<figure><img src="image_18.png" /><figcaption>Figure 2.3: The Muller tree for Muller($\mathcal{F}$). By convention nodes labelled by a set in $\mathcal{F}$ are represented by a circle and the others by a square. The numbers on the right hand side and the dashed nodes (describing a branch) are both used in the proof of Theorem 22.</figcaption></figure>

<caption>Figure 2.3 represents the Zielonka tree for Muller($\mathcal{F}$) with</caption>

$$ \mathcal{F} = \{\{2\}, \{3\}, \{4\}, \{1,2\}, \{1,3\}, \{1,3,4\}, \{2,3,4\}, \{1,2,3,4\}\}. $$

We note that there are two nodes labelled $\{1\}$; in general there may be several nodes with the same label. Also, not all branches have the same length.

The first use of the Zielonka tree is to induce an improved reduction from Muller to parity objectives. A branch in a tree is a path from the root to a leaf.

**Theorem 22** (Reduction from Muller to parity games using the Zielonka tree automaton). Let $C = [1, d]$ be a set of colours and Muller($\mathcal{F}$) a Muller objective. There exists a deterministic parity automaton Zielonka $\mathcal{F}$ over the alphabet $C$ defining Muller($\mathcal{F}$). Its number of states is the number of branches of $T_{\mathcal{F}}$ and its parity condition uses $d$ priorities.

Here again we take advantage of the fact that the acceptance conditions on automata are transition based; using stated based transitions we would have added a multiplicative factor $d$.

*Proof.* Without loss of generality $C \in \mathcal{F}$: if this is not the case we consider the complement Muller$(2^C \setminus \mathcal{F})$. We number the levels of $T_{\mathcal{F}}$ from the leaves to the root such that nodes labelled by sets in $\mathcal{F}$ are even and the other ones odd (this will be used for defining the parity condition). See Figure 2.3 for a possible numeration of the levels (on the right hand side), the other options being shifts of this numeration by an even number.

The set of states of Zielonka $\mathcal{F}$ is the set of branches of $T_{\mathcal{F}}$. We represent a branch by $(S_1, \dots, S_k)$ where $S_1$ is the set labelling the root and $S_k$ the set labelling a leaf. Note that $k \le d$. For the sake of simplicity we identify nodes with their labels, which is an abuse since two different nodes may have the same label but will be convenient and harmless in our reasoning.
The initial state is irrelevant because Muller($\mathcal{F}$) is prefix independent. We define the support $\text{supp}(b, c)$ of a branch $b$ and a colour $c$ to be the lowest node of $b$ which contains $c$. The transition function is defined as follows: $\delta(b, c)$ is the next branch (in the lexicographic order from left to right and in a cyclic way) which coincides with $b$ up to $\text{supp}(b, c)$. The priority of this transition is given by the level on which $\text{supp}(b, c)$ sits.

This is best understood on an example: on Figure 2.3 consider the branch $b$ represented by dashed nodes, reading the colour 2 we consider branches starting with $(\{1, 2, 3, 4\}, \{1, 2, 3\})$ because $\text{supp}(b, 2) = \{1, 2, 3\}$.

The next branch after $b$ is $(\{1, 2, 3, 4\}, \{1, 2, 3\}, \{1, 2\}, \{1\})$ (because we cycle: the node after $\{1, 3\}$ is $\{1, 2\}$). The priority of this transition is 3 corresponding to the level where $\{1, 2, 3\}$ sits.

We now show that the automaton Zielonka$_{\mathcal{F}}$ defines Muller($\mathcal{F}$). Let $\rho = c_0c_1...$ be an infinite word over the alphabet $C$. Let us consider the run of Zielonka$_{\mathcal{F}}$ over $\rho$:

$$ (b_0, c_0, b_1)(b_1, c_1, b_2)... $$

We consider $\text{Inf}(\rho)$ the set of colours appearing infinitely many times. Let us look at the largest prefix $(S_1, ..., S_p)$ of a branch which is eventually common to all the branches $b_i$. We make two claims:

* $\text{Inf}(\rho)$ is included in $S_p$;

* $\text{Inf}(\rho)$ is not included in any child of $S_p$.

For the first claim, let $c \in \text{Inf}(\rho)$, since eventually the branch $b_i$ starts with $(S_1, ..., S_p)$, the support of $b_i$ and $c$ is lower than or equal to $S_p$, meaning that $c \in S_p$.

For the second claim, we first note that by maximality of $(S_1, ..., S_p)$ the support of $b_i$ and $c_i$ is infinitely many times $S_p$. Indeed from some point onwards it is lower than or equal to $S_p$, and if it would be eventually strictly lower then the corresponding child of $S_p$ would be common to all branches $b_i$ from there on. This implies that all children of $S_p$ appear infinitely many times in the branches $b_i$: each time the support of $b_i$ and $c_i$ is $S_p$, the branch switches to the next child of $S_p$. Now since each child $S_{p+1}$ of $S_p$ is left infinitely many times this implies that there exists $c \in \text{Inf}(\rho)$ with $c \notin S_{p+1}$. Hence $\text{Inf}(\rho)$ is not included in $S_{p+1}$.

By definition of the Zielonka tree, this implies that $\text{Inf}(\rho) \in \mathcal{F}$ if and only if $S_p \in \mathcal{F}$, thus $\rho$ is accepted by Zielonka$_{\mathcal{F}}$ if and only if $\text{Inf}(\rho) \in \mathcal{F}$, as desired. $\square$

Since Theorem 22 is a reduction from Muller to parity objectives, it implies a reduction from Muller games to parity games as explained in Section 1.6, improving over Theorem 21. Since solving parity games is in $\text{NP} \cap \text{coNP}$, if we represent the Muller condition by a Zielonka tree then the automaton constructed in Theorem 22 is of polynomial size, implying the following result.

**Theorem 23 (Complexity of solving Muller games represented by the Zielonka tree).**
Solving Muller games where the condition is represented by a Zielonka tree is in $\text{NP} \cap \text{coNP}$.