Chapter 13

# Multiplayer Games

ROMAIN BRENGUIER, OCAN SANKUR

In two player games seen so far, players had objectives that are opposite to each other's, so we were able to define them giving only Eve's objective. Adam was seen as a purely adversarial player. Such games are called *zero-sum* games since, in a quantitative setting, the sum of the payoffs of the two players would sum up to zero in any outcome. However, the objectives of the players are not entirely conflicting in all games. In particular, in multiplayer games, that is, games with more than two players, the binary view of zero-sum games does not make sense; but there are also interesting examples of non-zero sum games with only two players (we will see one below). In this setting, winning strategies are no longer suitable to describe rational behaviours since the opponents should no longer be seen as purely adversarial. In fact, when the objectives of the players are not opposite, some cooperation becomes possible. Then, rather than assuming that opponents are purely adversarial, it is interesting to study the possible outcomes when they are simply *rational*, that is, follow the best strategy for their own objectives. The notion of equilibria we will study in this chapter aims at describing such rational behaviours.

If one is expecting for sure some specific strategies to be played by the opponents, then the most rational response is to choose the *best response*, that is, the strategy that is optimal for the player against the given strategies of the other players. Thus, if we assign strategies to players, and if the players are all aware of the strategies of the other players, then each player will be willing to change their strategy if theirs does not turn out to be a best response. Such a situation is seen as unstable and is undesirable in many applications of game theory. *Nash equilibrium* is defined simply as a stable situation in such a setting: a strategy profile in which the strategy of each player is a best response to the rest of the strategies. Thus, no player has any incentive to change their strategy.

We will see the formal definition of a Nash equilibrium in the next section. Let us first consider the following example.

The following Hawk-Dove game was first presented by the biologists Smith and
<table><caption>Table 13.1: The Hawk-Dove game. Each column corresponds to a strategy of $P_1$ and each line to a strategy of $P_2$.</caption><thead><tr><th></th><th>Hawk</th><th>Dove</th></tr></thead><tbody><tr><th>Hawk</th><td>0, 0</td><td>1, 4</td></tr><tr><th>Dove</th><td>4, 1</td><td>3, 3</td></tr></tbody></table>

Price, and shown in Table 13.1. Here, two animals are fighting for resources and can choose to either act as a hawk or as a dove. If both player choose hawk they will have to fight for resources, and thus only get payoff 0. If only one chooses hawk, they get a high payoff of 4, because they get all the valuable resources for themselves, while the dove gets 1: they get plenty of resources but gets hunted. When they both choose dove, they both get a payoff of 3: they have to share resources but do not get hunted.

When a player chooses hawk then the best payoff for the opponent is obtained by choosing dove, so as to avoid fighting for resources. So, dove is the best response to hawk. Reciprocally, the best response to dove is to play hawk. There are two ‘equilibria’: (Hawk, Dove) and (Dove, Hawk), where no player has an interest in changing their strategy. Note that the highest payoff a player can ensure (against all adversary strategies) is only 1.

Nash showed the existence of such equilibria in normal-form games<fnref n="1" />, which may require randomized strategies. This result revolutionized the field of economics, where it is used to analyze competitions between firms or government economic policies for example. Game theory and the concept of Nash equilibrium are now applied to diverse fields: in finance to analyse the evolution of market prices, in biology to understand the evolution of some species, in political sciences to explain public choices made by parties.

In this chapter, we will first study the computation of Nash equilibria in multiplayer concurrent games with $\omega$-regular objectives. The algorithms we present here differ from those that were given for normal-form games since ours are infinite-duration with omega-regular objectives. We will then present extensions of this notion such as secure and robust equilibria. The second result we develop is the notion of admissibility: this is a different approach to the study of rational behaviours and consists in eliminating for each player irrational choices of strategies.

## 13.1 Nash Equilibria for games in normal form

The normal form games we consider differ from the matrix games of Chapter 7, in that each player has their own payoff. So for instance, when player 1 chooses column Hawk, and player 2 chooses row Dove, the payoff for player 1 is $f_{P_1}(\text{Hawk}, \text{Dove}) = 4$.

<footnote n="1">¹normal-form games are also called matrix games, see Chapter 7.</footnote>
<table><caption>Table 13.2: A game of medium access.</caption><thead><tr><th></th><th>Emit</th><th>Wait</th></tr></thead><tbody><tr><th>Emit</th><td>-1, -1</td><td>2, 0</td></tr><tr><th>Wait</th><td>0, 2</td><td>0, 0</td></tr></tbody></table>

Let us call a vector of strategies specifying a strategy for each player a *strategy profile*. In normal-form games, each cell of the table $\Delta$ corresponds to a strategy profile.

**Definition 31.** A Nash equilibrium is a stable strategy profile in which strategy is a best response against the other strategies.

Thus a Nash equilibrium is a stable situation in the sense that no player has an incentive in changing their strategy. Nash proved that when players are allowed to randomise among all their strategies, there always exists a Nash equilibrium.

**Theorem 138 (Existence of Nash equilibria).** In every normal-form game with a finite number of players, each having a finite number of pure strategies, there exists a randomised Nash equilibrium.

Note that not all games contain pure Nash equilibria. For example, in the rock-paper-scissors game, the best response to rock is paper, to paper is scissors, and to scissors is rock, so none of these pure strategies can be an equilibrium.

For finding a pure Nash equilibrium in a normal-form game, there is a simple polynomial time algorithm. For each strategy profile, we look for each player whether they have a better response than their current strategy. If no player has a better response, the strategy profile is a Nash equilibrium, otherwise we move to the next one, and if none satisfies the condition then there is no equilibrium.

**Example 29 (Medium Access Control).** Consider a medium access control problem, where several users share access to a wireless channel. A communication over the channel is successful if there are no collisions, that is, if a single user is transmitting their message only. During each slot, each user chooses either to transmit or to idle. Intuitively, the number of packets transmitted without collision decreases with the number of users emitting in the same slot. Furthermore each attempt at transmitting has a cost. An example payoff for two players, is represented in Table 13.2.

We encourage the reader to find the Nash equilibria of the above game.

The game described above corresponds to a single slot of this system. In a practical scenario, there would be a succession of slots and the payoff would be the sum of payoffs over all slots. Normal-form games are thus not sufficient to represent games with repetitions and to study the evolution of the behaviours as the game evolves.

One possibility to model repetition is to use *games in extensive form* which are games played on finite trees. However such games only model a fixed number of repetitions unlike infinite or arbitrary duration games as studied in this book. We thus study, in the rest of this chapter, algorithms for games played on graphs.
<figure><img src="image_114.png" /><figcaption>Figure 13.1: Example of a three-player concurrent arena. The symbol $*$ on edges can be replaced by either a or b.</figcaption></figure>

**13.1.1 Definitions**

**Definition 32.** A multiplayer arena $\mathcal{A}$ with $k$ players is a tuple $(V, A, \Delta, (c_P)_{P \in \mathcal{P}})$, where:

• $V$ is a finite set of vertices;

• $\mathcal{P} = \{1, 2, \dots, k\}$ is the set of players;

• $A$ is a finite set of actions, a tuple $(a_P)_{P \in \mathcal{P}}$ containing one action $a_P$ for each player $A$ is called a move, thus $A^k$ is the set of possible moves;

• $\Delta: V \times A^k \to V$ is the transition function which associates to a pair of vertices and moves the resulting state;

• $(c_P)_{P \in \mathcal{P}}$ is a tuple of colouring functions with $c_P: V \to C$ for each $P \in \mathcal{P}$.

**Example 30.** A simple three-player concurrent game is represented in Figure 13.1. Vertices are $v_0, v_1, v_2, v_3$ and $v_4$. Players are named $P_1, P_2, P_3$. The set of actions is $A = \{a, b\}$. The transition relation is given by the edges in the graph, for instance $\Delta(s_0, (a, b, a)) = v_1$. In our figures, $*$ represents an arbitrary action. The colouring function is represented below vertices as tuples ranging over players. For instance, a vertex labelled by $(1, 1, 0)$ assigns the first two players the colour 1, and the third player the colour 0, In particular, $c_{P_1}(v_2) = 1$, and $c_{P_3}(v_2) = 0$.

A history of the multiplayer arena $\mathcal{A}$ is a finite sequence of states and moves ending with a state, i.e. a word in $(V \cdot A^{\mathcal{P}})^* \cdot V$. Note that unlike for two player games we include actions in the history, because knowing the source and target vertices does not mean you know which player chose which actions.

For a history $\pi$, we write $\pi_i$ the $i$-th vertex of $\pi$, starting from 0, and $move_i(\pi)$ its $i$-th move, thus $\pi = \pi_0 \cdot move_0(\pi \cdot \pi_1 \cdots move_{n-1}(\pi) \cdot \pi_n)$, and with this notation
$move_i(\pi)_P$ is the $i$-th action of player $P$ in $h$. The length $|\pi|$ of such a history is $n+1$. We write last($\pi$) the last vertex of $h$, i.e. $\pi_{|\pi|-1}$. A play $\rho$ is an infinite sequence of vertices and moves, i.e. an element of $(V \cdot A^\mathcal{P})^\omega$.

**Definition 33 (Strategy and coalition).** A strategy is a function which associates an action to each history. We often write $\sigma_A$ for a strategy of player $P$. A coalition $\mathcal{C}$ is a set of players in $\mathcal{P}$, and we write $-\mathcal{C}$ for the remaining players, that is $-\mathcal{C} = \text{Agt} \setminus \mathcal{C}$. Let $\mathcal{C}$ be a coalition, a strategy $\sigma_{\mathcal{C}}$ for $\mathcal{C}$ is a function which associates a strategy $\sigma_P$ to each player $P \in \mathcal{C}$. Given a strategy $\sigma_{\mathcal{C}}$, when it is clear from the context, we simply write $\sigma_P$ for $\sigma_{\mathcal{C}}(P)$.

**Definition 34 (Outcomes).** A history $\pi$ is compatible with the strategy $\sigma_{\mathcal{C}}$ for coalition $\mathcal{C}$ if, for all $k < |\pi| - 1$ and all $P \in \mathcal{C}$, we have $(move_k(\pi))_P = \sigma_P(\pi \le k)$, and $\Delta(\pi_k, move_k(\pi)) = \pi_{k+1}$. A play $\rho$ is compatible with the strategy $\sigma_{\mathcal{C}}$ if all its prefixes are. We write $\text{Out}_{\mathcal{A}}(v_0, \sigma_{\mathcal{C}})$ for the set of plays in $\mathcal{A}$ that are compatible with strategy $\sigma_{\mathcal{C}}$ and have initial vertex $v_0$. Let $\text{Out}_{\mathcal{A}}(\sigma_{\mathcal{C}})$ denote the union of $\text{Out}_{\mathcal{A}}(v_0, \sigma_{\mathcal{C}})$ for all $v_0$, and $\text{Out}_{\mathcal{A}}(v_0)$ the union of all $\text{Out}_{\mathcal{A}}(v_0, \sigma_{\mathcal{C}})$. The subscript $\mathcal{A}$ can be omitted if it is clear from the context. These paths are called outcomes of $\sigma_{\mathcal{C}}$ from $v_0$.

Note that when the coalition $\mathcal{C}$ is composed of all the players the outcome from a given state is unique.

**Example 31.** Consider in the example of Figure 13.1, the following strategies:

* $P_1$ always plays a, i.e. $\sigma_{P_1}(\pi) = a$ for all histories $\pi$;

* $P_2$ plays a in $v_0$ if it is the first state and then always plays b, i.e. $\sigma_{P_2}(v_0) = a$ and $\sigma_{P_2}(\pi) = b$ for all $\pi \ne v_0$;

* $P_3$ always plays b, i.e. $\sigma_{P_3}(\pi) = b$.

The outcome from $v_0$ in that case is

$$ \text{Out}(v_0, \sigma_{\{P_1,P_2,P_3\}}) = v_0 \cdot (a,a,b) \cdot v_2 \cdot (a,b,b) \cdot v_4 \cdot (a,b,b) \cdot \\ (v_0 \cdot (a,b,b) \cdot v_1 \cdot (a,b,b) \cdot v_3 \cdot (a,b,b))^\omega $$

**Definition 35 (Multiplayer game).** A payoff function associates a real number to each outcome. We will be mostly be interested in solving games with qualitative objectives, that is payoffs that take values 0 and 1. A multiplayer game $(\mathcal{A}, (f_P)_{P \in \mathcal{P}})$ is given by a multiplayer arena $\mathcal{A}$, an initial vertex $v_0$ and payoff function $f_P$ for each player $P$. When $f_P$ is qualitative we simply write $\Omega_P$ for the corresponding objective.

### 13.1.2 The Nash equilibrium problem

In this section we will present an algorithm to compute Nash equilibria in multiplayer games. The problem we are interested in is to decide the existence of a Nash equilibrium in which the objectives of a given set of players are satisfied.

**Problem 21 (Existence of a constrained Nash equilibrium).**
**INPUT:** A multiplayer game $(\mathcal{A}, (f_P)_{P \in \mathcal{P}})$, payoff bounds $(b_P)_{P \in \mathcal{P}}$, and an initial vertex $v_0$

**OUTPUT:** Does there exist a Nash equilibrium $\sigma_{\mathcal{P}}$ such that for all $P \in \mathcal{P}$, we have $f_P(\text{Out}(v_0, \sigma_{\mathcal{P}})) \ge b_P$?

The algorithm is based on a reduction to zero-sum two-players games, which allows us to use algorithms presented in the previous chapters of this book. More precisely, we present the *deviator game*, which is a transformation of a concurrent multiplayer game into a turn-based zero-sum game, such that there are strong links between equilibria in the former and winning strategies in the latter. The proofs of this section are independent of the type of objectives we consider.

### 13.1.3 Deviators

A central notion we use is that of *deviators*. These are the players who have played different moves from those prescribed in a given profile, thus causing a deviation from the expected outcome. Formally, a deviator from move $a_{\mathcal{P}}$ to $a'_{\mathcal{P}}$ is a player $D \in \mathcal{P}$ such that $a_D \neq a'_D$. We denote the set of deviators by

$$ \text{Dev}(a_{\mathcal{P}}, a'_{\mathcal{P}}) = \{D \in \mathcal{P} \mid a_D \neq a'_{D}\}. $$

We extend the definition to pairs of histories and strategies by taking the union of deviator sets of each step along the history. Formally,

$$ \text{Dev}(\pi, \sigma_{\mathcal{P}}) = \bigcup_{0 \le i < |h|} \text{Dev}(\text{move}_i(\pi), \sigma_{\mathcal{P}}(\pi_{\le i})). $$

For an infinite play $\rho$, we define $\text{Dev}(\rho, \sigma_{\mathcal{P}}) = \bigcup_{i \in \mathbb{N}} \text{Dev}(\text{move}_i(\rho), \sigma_{\mathcal{P}}(\rho_{\le i}))$. Intuitively, having chosen a strategy profile $\sigma_{\mathcal{P}}$ and observed a play $\rho$, deviators represent the players that must have changed their strategies from $\sigma_{\mathcal{P}}$ in order to generate $\rho$.

**Lemma 145.** *Given a play $\rho$, strategy profile $\sigma_{\mathcal{P}}$, a coalition $\mathcal{C}$ contains $\text{Dev}(\rho)$, if and only if, there exists a strategy $\sigma'_{\mathcal{C}}$ such that $\text{Out}(\rho_1, \sigma_{-\mathcal{C}}, \sigma'_{\mathcal{C}}) = \rho$.*

*Proof.* Assume that coalition $\mathcal{C}$ contains $\text{Dev}(\rho, \sigma_{\mathcal{P}})$. We define the strategy $\sigma_{\mathcal{C}}$ to be such that for all $i \in \mathbb{N}$, $\sigma_{\mathcal{C}}(\rho_{\le i}) = (\text{move}_i(\rho))_{\mathcal{C}}$. By hypothesis, we have, for all indices $i$, $\text{Dev}(\text{move}_i(\rho), \sigma_{\mathcal{P}}(\rho_{\le i})) \subseteq \mathcal{C}$, so for all players $A \notin \mathcal{C}$, $\sigma_A(\rho_{\le i}) = (\text{move}_i(\rho))_A$. Then $\Delta(\rho_i, \sigma'_{\mathcal{C}}(\rho_{\le i}), \sigma_{-\mathcal{C}}(\rho_{\le i})) = \rho_{i+1}$. Hence $\rho$ is the outcome of the profile $(\sigma_{-\mathcal{C}}, \sigma'_{\mathcal{C}})$.

For the other direction, let $\sigma_{\mathcal{P}}$ be a strategy profile, $\sigma'_{\mathcal{C}}$ a strategy for coalition $\mathcal{C}$, and $\rho \in \text{Out}_G(\rho_0, \sigma_{-\mathcal{C}}, \sigma'_{\mathcal{C}})$. For all indices $i$, $\text{move}_i(\rho) = (\sigma_{-\mathcal{C}}(\rho_{\le i}), \sigma'_{\mathcal{C}}(\rho_{\le i}))$. Therefore for all players $A \notin \mathcal{C}$, $(\text{move}_i(\rho))_A = \sigma_A(\rho_{\le i})$. Consequently, this implies that $\text{Dev}(\text{move}_i(\rho), \sigma_{\mathcal{P}}(\rho_{\le i})) \subseteq \mathcal{C}$. Hence $\text{Dev}(\rho, \sigma_{\mathcal{P}}) \subseteq \mathcal{C}$. $\square$

**Example 32.** *In the example of Figure 13.1, we consider again the strategies, such that for all histories $\pi, \sigma_{P_1}(\pi) = a$, $\sigma_{P_2}(v_0) = a$ and if $\pi \neq v_0$, $\sigma_{P_2}(\pi) = b$, and $\sigma_{P_3}(\pi) = b$. Then $\text{Dev}(v_0 \cdot (a, a, b) \cdot v_2 \cdot (a, a, b) \cdot v_1 \cdot (a, b, a) \cdot v_2, \sigma_{\mathcal{P}})$ is the union of:*
$$ \bullet \ Dev(\sigma_{\mathcal{P}}(v_0), (a, a, b)) = Dev((a, a, b), (a, a, b)) = \emptyset $$

$$ \bullet \ Dev(\sigma_{\mathcal{P}}(v_0 \cdot (a, a, b) \cdot v_2), (a, a, b)) = Dev((a, b, b), (a, a, b)) = \{P_2\} $$

$$ \bullet \ Dev(\sigma_{\mathcal{P}}(v_0 \cdot (a, a, b) \cdot v_2 \cdot (a, a, b) \cdot v_1), (a, b, a)) = Dev((a, b, b), (a, b, a)) = \{P_3\}. $$

We obtain $Dev(v_0 \cdot (a, a, b) \cdot v_2 \cdot (a, a, b) \cdot v_1 \cdot (a, b, a) \cdot v_2, \sigma_{\mathcal{P}}) = \{P_2, P_3\}$. This means that both $P_2$ and $P_3$ need to change their strategies from $\sigma_{\mathcal{P}}$ to obtain the given history.

Note that Nash equilibria are defined only with respect to deviations by single players, that is, we require all players to achieve worse or equal payoffs than the prescribed profile when they single-handedly change strategies. Thus, only the outcomes with singleton deviator sets will be of interest for us in the next section where we present the algorithm.

### 13.1.4 Deviator Game

We now present an algorithm to reduce multiplayer games to two-player games using the notion of deviators we just defined. Given a game $\mathcal{G} = (\mathcal{A}, (f_A)_{A \in \mathcal{P}})$, we define the deviator game, denoted DevGame($\mathcal{G}$). Intuitively, in this game, Eve needs to play according to an equilibrium, while Adam tries to find a profitable deviation for any player. The vertices are $V' = V \times 2^{\mathcal{P}}$, where the second component, a subset of $\mathcal{P}$, records the deviators of the current history.

At each step, Eve chooses an action profile, and Adam chooses the move that will apply. Adam can either respect Eve's choice, or pick a different action profile in which case the deviators will be added to the second component of the vertex. The game begins in $(v_0, \emptyset)$ and then proceeds as follows: from a vertex $(v, D)$, Eve chooses an action profile $a_{\mathcal{P}}$, and Adam chooses a possibly different one $a'_{\mathcal{P}}$. The next vertex is $(\Delta(v, a'_{\mathcal{P}}), D \cup Dev(a_{\mathcal{P}}, a'_{\mathcal{P}}))$.

**Example 33.** An example of a partial construction of the deviator game for the example of Figure 13.1, is given in Figure 13.2. We cannot represent the full construction here, as there are 40 vertices.

We define projections $\text{proj}_V$ and $\text{proj}_{\text{Dev}}$ from $V'$ to $V$ and from $V'$ to $2^{\mathcal{P}}$ respectively, as well as $\text{proj}_A$ from $\text{Act}^{\mathcal{P}} \times \text{Act}^{\mathcal{P}}$ to $\text{Act}^{\mathcal{P}}$ which maps to the second component of the product, that is, Adam's action.

For a history or play $\rho$, define $\pi_{\text{Out}}(\rho)$ as the play $\rho'$ for which, $\rho'_i = \text{proj}_V(\rho_i)$ and $\text{move}_i(\rho') = \text{proj}_A(\text{move}_i(\rho))$ for all $i$. This is thus the play induced by Adam's actions. Let us also denote $\text{Dev}(\rho) = \text{proj}_{\text{Dev}}(\text{last}(\rho))$.

We can associate a strategy of Eve to each strategy profile $\sigma_{\mathcal{P}}$ such that she chooses the moves prescribed by $\sigma_{\mathcal{P}}$ at each history of DevGame($\mathcal{G}$). Formally, we write $\kappa(\sigma_{\mathcal{P}})$ for the strategy defined by $\kappa(\sigma_{\mathcal{P}})(\pi) = \sigma_{\mathcal{P}}(\text{proj}_{\text{Out}}(\pi))$ for all histories $\pi$.

The following lemma states the correctness of the construction of the deviator game DevGame($\mathcal{G}$), in the sense that it records the set of deviators in the strategy profile suggested by Adam with respect to the strategy profile suggested by Eve.

**Lemma 146.** Let $\mathcal{G}$ be a multiplayer game, $v$ a vertex, $\sigma_{\mathcal{P}}$ a strategy profile, and $\sigma_{\exists} = \kappa(\sigma_{\mathcal{P}})$ the associated strategy in the deviator game.
<figure><img src="image_115.png" /><figcaption>Figure 13.2: Example a deviator game construction.</figcaption></figure>
1. If $\rho \in \text{Out}_{\text{DevGame}(\mathscr{G})}((v, \emptyset), \sigma_{\mathscr{P}})$, then $\text{Dev}(\text{proj}_{\text{Out}}(\rho), \sigma_{\mathscr{P}}) = \text{Dev}(\rho)$.

2. If $\rho \in \text{Out}_G(v)$ and for all index $i$, $\rho'_i = (\rho_i, \text{Dev}(\rho_{\le i}, \sigma_{\mathscr{P}}))$ and $\text{move}_i(\rho') = (\sigma_{\mathscr{P}}(\rho_{\le i}), \text{move}_i(\rho))$, then $\rho' \in \text{Out}_{\text{DevGame}(\mathscr{G})}((v, \emptyset), \sigma_{\exists})$.

*Proof.* We prove that for all $i$, $\text{Dev}(\text{proj}_{\text{Out}}(\rho_{\le i}, \sigma_{\mathscr{P}})) = \text{proj}_{\text{Dev}}(\rho_{\le i})$, which implies the property. The property holds for $i = 0$, since initially both sets are empty. Assume now that it holds for $i \ge 0$. Then:

$$
\begin{align*}
& \text{Dev}(\text{proj}_{\text{Out}}(\rho_{\le i+1}), \sigma_{\mathscr{P}}) \\
&= \text{Dev}(\text{proj}_{\text{Out}}(\rho_{\le i}), \sigma_{\mathscr{P}}) \cup \text{Dev}(\sigma_{\mathscr{P}}(\text{proj}_{\text{Out}}(\rho_{\le i})), \text{proj}_A(\text{move}_{i+1}(\rho))) \\
& \quad \text{(by definition of deviators)} \\
&= \text{Dev}(\rho_{\le i}) \cup \text{Dev}(\sigma_{\mathscr{P}}(\text{proj}_{\text{Out}}(\rho_{\le i}), \text{proj}_A(\text{move}_{i+1}(\rho)))) \\
& \quad \text{(by induction hypothesis)} \\
&= \text{Dev}(\rho_{\le i}) \cup \text{Dev}(\sigma_{\exists}(\rho_{\le i}), \text{proj}_A(\text{move}_{i+1}(\rho))) \\
& \quad \text{(by definition of } \sigma_{\exists} \text{)} \\
&= \text{Dev}(\rho_{\le i}) \cup \text{Dev}(\text{move}_{i+1}(\rho)) \\
& \quad \text{(by assumption } \rho \in \text{Out}_{\text{DevGame}(\mathscr{G})}((v, \emptyset), \sigma_{\exists})) \\
&= \text{Dev}(\rho_{\le i+1}) \\
& \quad \text{(by construction of DevGame}(\mathscr{G})\text{))}
\end{align*}
$$

Which concludes the induction.

We now prove the second part. The property is shown by induction. It holds for $v_0$. Assume it is true up to index $i > 0$, then

$$
\begin{align*}
& \Delta'(\rho'_i, \sigma_{\exists}(\rho'_{\le i}), \text{move}_i(\rho)) \\
&= \Delta'((\rho_i, \text{Dev}(\rho_{\le i}, \sigma_{\mathscr{P}})), \sigma_{\exists}(\rho'_{\le i}), \text{move}_i(\rho)) \\
& \quad \text{(by definition of } \rho' \text{)} \\
&= \Delta(\rho_i, \text{move}_i(\rho)), \text{Dev}(\rho_{\le i}, \sigma_{\mathscr{P}}) \cup \text{Dev}(\sigma_{\exists}(\rho'_{\le i}), \rho_{i+1})) \\
& \quad \text{(by construction of } \Delta' \text{)} \\
&= (\rho_{i+1}, \text{Dev}(\rho_{\le i}, \sigma_{\mathscr{P}}) \cup \text{Dev}(\sigma_{\exists}(\rho'_{\le i}), \rho_{i+1})) \\
& \quad \text{(since } \rho \text{ is an outcome of the game)} \\
&= (\rho_{i+1}, \text{Dev}(\rho_{\le i}, \sigma_{\mathscr{P}}) \cup \text{Dev}(\sigma_{\mathscr{P}}(\rho_{\le i}), \rho_{i+1})) \\
& \quad \text{(by construction of } \sigma_{\exists} \text{)} \\
&= (\rho_{i+1}, \text{Dev}(\rho_{\le i+1}, \sigma_{\mathscr{P}})) \\
& \quad \text{(by definition of deviators)} \\
&= \rho'_{i+1}.
\end{align*}
$$

□
The objective of Eve in the deviator game is defined so that winning strategies correspond to equilibria of the original game. First, as an intermediary step, given coalition $\mathcal{C}$, player $P$ and bound $b$, we will construct an objective stating that we can ensure that the payoff of $P$ will not exceed $b$ even if players in $\mathcal{C}$ change their strategies. Consider the following objective in DevGame($\mathcal{G}$):

$$ \Omega(\mathcal{C}, P, b) = \{ \rho \in \text{Out}_{\text{DevGame}(\mathcal{G})} \mid \text{Dev}(\rho) \subseteq \mathcal{C} \Rightarrow f_P(\text{proj}_{\text{Out}}(\rho)) \leq b \}. $$

Intuitively, this says that if only players in $\mathcal{C}$ deviated from the strategy suggested by Eve, then the payoff of $P$ is smaller than $b$. We now show that a strategy ensuring bound $b$ for the payoff of $P$ against coalition $\mathcal{C}$ corresponds to a winning strategy for $\Omega(\mathcal{C}, P, b)$ in the deviator game.

**Lemma 147.** Let $\mathcal{C} \subseteq \mathcal{P}$ be a coalition, $\sigma_{\mathcal{P}}$ be a strategy profile, $b \in \mathbb{R}$ a bound, and $P$ a player. For all strategies $\sigma'_c$, vertex $v_0$, and coalition $\mathcal{C}$, the following equivalence holds: $f_P(\text{Out}_{\text{DevGame}(\mathcal{G})}(v_0, \sigma'_c, \sigma'_c)) \leq b$ if, and only if, $\kappa(\sigma_{\mathcal{P}})$ is winning in DevGame($\mathcal{G}$) for objective $\Omega(\mathcal{C}, P, b)$.

*Proof.* Let $\rho$ be an outcome of $\sigma_\exists = \kappa(\sigma_{\mathcal{P}}) \in \text{DevGame}(\mathcal{G})$. By Lemma 146, we have that $\text{Dev}(\rho) = \text{Dev}(\text{proj}_V(\rho), \sigma_{\mathcal{P}})$. By Lemma 145, $\text{proj}_V(\rho)$ is the outcome of $(\sigma_{-\text{Dev}(\rho)}, \sigma'_{\text{Dev}(\rho)})$ for some $\sigma'_{\text{Dev}(\rho)}$. If $\text{Dev}(\rho) \subseteq \mathcal{C}$, then

$$ f_P(\text{proj}_V(\rho)) = f_P(\sigma'_{-\mathcal{C}}, \sigma'_{\mathcal{C}\setminus\text{Dev}(\rho)}, \sigma'_{\text{Dev}(\rho)}) = f_P(\sigma'_{-\mathcal{C}}, \sigma''_{\mathcal{C}}) $$

where $\sigma''_P = \sigma'_P$ if $P \in \text{Dev}(\rho)$ and $\sigma_P$ otherwise. By hypothesis, this payoff is smaller than or equal to $b$. This holds for all outcomes $\rho$ of $\sigma_\exists$, thus $\sigma_\exists$ is a winning strategy for $\Omega(\mathcal{C}, P, b)$.

For the other direction, assume $\sigma_\exists = \kappa(\sigma_{\mathcal{P}})$ is a winning strategy in DevGame($\mathcal{G}$) for $\Omega(\mathcal{C}, P, b)$. Let $\sigma'_c$ be a strategy for $\mathcal{C}$ and $\rho$ the outcome of $(\sigma'_c, \sigma_{-\mathcal{C}})$. By Lemma 145, $\text{Dev}(\rho, \sigma_{\mathcal{P}}) \subseteq \mathcal{C}$. By Lemma 146, $\rho' = (\rho_j, \text{Dev}(\rho_{\le j}, \sigma_{\mathcal{P}}))_{j \in \mathbb{N}}$ is an outcome of $\sigma_\exists$. We have that $\text{Dev}(\rho') = \text{Dev}(\rho, \sigma_{\mathcal{P}}) \subseteq \mathcal{C}$. Since $\sigma_\exists$ is winning, $\rho$ is such that $f_P(\text{proj}_V(\rho)) \leq b$. Since $f_P(\text{proj}_V(\rho')) = f_P(\rho)$, this shows that for all strategies $\sigma'_c$, $f_P(\sigma'_{-\mathcal{C}}, \sigma''_{\mathcal{C}}) \leq b$. $\square$

Now, Eve can show that there is a Nash equilibrium in a given game by proving that whenever there is a single deviator, the deviating player does not gain more than without the deviation, while she does not have to prove anything on plays involving several deviators.

**Theorem 139.** Let $\mathcal{G} = (\mathcal{A}, (f_P)_{P \in \mathcal{P}})$ be a game, $\sigma_{\mathcal{P}}$ a strategy profile in $\mathcal{G}$, vertex $v_0$, and $F = (f_P(\text{Out}_{\mathcal{A}}(v_0, \sigma_{\mathcal{P}})))_{P \in \mathcal{P}}$ the payoff profile of $\sigma_{\mathcal{P}}$ from $v_0$. The strategy profile $\sigma_{\mathcal{P}}$ is a Nash equilibrium if, and only if, strategy $\kappa(\sigma_{\mathcal{P}})$ is winning in DevGame($\mathcal{A}$) for the objective $N(F)$ defined by:

$$ N(F) = \{ \rho \mid |\text{Dev}(\rho)| \neq 1 \} \cup \bigcup_{P \in \mathcal{P}} \{ \rho \mid \text{Dev}(\rho) = \{P\} \wedge f_P(\text{proj}_{\text{Out}}(\rho)) \leq F_P \}. $$

*Proof.* By Lemma 147, $\sigma_{\mathcal{P}}$ is a Nash equilibrium if, and only if, for each player $P$, $\kappa(\sigma_{\mathcal{P}})$ is winning for $\Omega(\{P\}, P, F_P)$. So it is enough to show that for each player $P$, $\kappa(\sigma_{\mathcal{P}})$ is winning for $\Omega(\{P\}, P, F_P)$ if, and only if, $\kappa(\sigma_{\mathcal{P}})$ is winning for $N(F)$.

**Implication** Let $\rho$ be an outcome of $\kappa(\sigma_{\mathcal{P}})$.
* If $|\text{Dev}(\rho)| \neq 1$, then $\rho$ is in $N(F)$ by definition.

* If $|\text{Dev}(\rho)| = 1$, then for $\{P\} = \text{Dev}(\rho)$, $f_P(\text{proj}_{\text{Out}}(\rho)) \le F_P$ because $\kappa(\sigma_{\mathcal{P}})$ is winning for $\Omega(\text{Dev}(\rho), P, F_P)$. Therefore $\rho$ is in $N(F)$.

This holds for all outcomes $\rho$ of $\kappa(\sigma_{\mathcal{P}})$ and shows that $\kappa(\sigma_{\mathcal{P}})$ is winning for $N(F)$.

**Reverse implication** Assume that $\kappa(\sigma_{\mathcal{P}})$ is winning for $N(F)$. We now show that $\kappa(\sigma_{\mathcal{P}})$ is winning for $\Omega(\{P\}, P, F_P)$ for each player $P$. Let $\rho$ be an outcome of $\kappa(\sigma_{\mathcal{P}})$, we have $\rho \in N(F)$. We show that $\rho$ belongs to $\Omega(\{P\}, P, F_P)$:

* If $\text{Dev}(\rho) = \emptyset$ then $\rho = \text{Out}(v_0, \sigma_{\mathcal{P}})$ and $f_P(\rho) = F_P$, so $\rho$ is in $\Omega(\{P\}, P, F_P)$

* If $\text{Dev}(\rho) \not\subseteq \{P\}$, then $\rho \in \Omega(\mathcal{C}, P, F_P)$ by definition.

* Otherwise $\text{Dev}(\rho) = \{P\}$. Since $\rho \in N(F)$, $f_P(\rho) \le F_P$. Hence $\rho \in \Omega(\mathcal{C}, P, F_P)$.

This holds for all outcomes $\rho$ of $\kappa(\sigma_{\mathcal{P}})$ and shows it is winning for $\Omega(\{P\}, P, F_P)$ for each player $P \in \mathcal{P}$, which shows that $\sigma_{\mathcal{P}}$ is a Nash equilibrium. $\square$

**Algorithm for Parity Objectives**

We now focus on the case of Parity objectives. Recall that Each player $P$ has a colouring function $c_P: V \to \mathbb{N}$, inducing the parity objective $\Omega_A$. Thus the payoff $f_P$ assigns 1 to paths belonging to $\Omega_A$ and 0 to the others.

We now give an algorithm for the Nash equilibrium problem with parity objectives. Given a payoff for each player $(F_P)_{P \in \mathcal{P}}$, we can deduce from the previous theorem an algorithm that constructs a Nash equilibrium if there exists one. We construct the deviator game and note that we can reduce the number of vertices as follows: since $\text{Dev}(\rho_{\le k})$ is nondecreasing, we know that Eve wins whenever this set has at least two elements. In the construction, states with at least two deviators can be replaced by a sink vertex that is winning for Eve. This means that the constructed game has at most $n \times (|\mathcal{P}| + 1) + 1$ states.

The objective can be expressed as a Parity condition in the following way:

* for each vertex $v' = (v, \{P\})$, $c'(v') = c_P(v) + 1$ if $F_P = 0$ and $2 \cdot \max_v c_P(v)$ otherwise;

* for each vertex $v' = (v, D)$ with $|D| \neq 1$, $c'(v') = 2 \cdot \max_v c_P(v)$ i.e. it is winning for Eve.

Notice that the colouring function $c'$ inverts the parity in the case where there is a single deviator who is losing in the prescribed strategy profile (that is, $F_P = 0$). In fact, when $F_P = 1$, the player cannot obtain more since they are already winning so the colour is set to $2 \cdot \max_v c_P(v)$ which is winning for Eve.

**Lemma 148.** We have $\maxinf(c'(\rho_i)) \in 2\mathbb{N}$ if, and only if, $\rho \in N(F)$, where $N(F)$ is as defined in Theorem 139.
*Proof.* For the implication, we will prove the contrapositive. Let $\rho$ be a play not in $N(F)$, then since the deviators can only increase along a play, we have that $\text{Dev}(\rho) = \{P\}$ for some player $P$ and $f_P(\rho) > F_P$. This means $F_P = 0$ and $\text{maxinf}(c_P(\rho_i)) \in 2\mathbb{N}$. By definition of $c'$ this implies that $\text{maxinf}(c'(\rho_i)) \in 2\mathbb{N} + 1$ which proves the implication.

For the other implication, let $\rho$ be such that $\text{maxinf}(c'(\rho_i)) \in 2\mathbb{N} + 1$. By definition of $c'$ this means $\rho$ contains infinitely many states of the form $(v, \{P\})$ with $F_P = 0$. Since the deviators only increase along the run, there is a player $P$ such that $\rho$ stays in the component $V \times \{P\}$ after some index $k$. Then for $i \ge k$, $c'(\rho_i) = c_P(\rho_i) + 1$, hence $\text{maxinf}(c'(\rho_i)) = \text{maxinf}(c_P(\rho_i)) + 1$. Therefore $\text{maxinf}(c_P(\rho_i)) \in 2\mathbb{N}$, which means $f_P(\rho) = 1 > F_P$. By definition of $N(F)$, $\rho \notin N(F)$. $\square$

Given that the size of the game is polynomial and that parity games can be decided in quasi-polynomial time (see Chapter 3), the above lemma implies the following theorem.

**Theorem 140.** For parity games, there is a quasi-polynomial algorithm to decide whether there is a Nash equilibrium with a given payoff.

### 13.1.5 Extensions of Nash Equilibria

#### Subgame Perfect Equilibria

Nash equilibria present the disadvantage that once a player has deviated, the others will try to punish him, forgetting everything about their own objectives. If we were to observe the game after this point of deviation, it would not look like the players are playing rationally and in fact it would not correspond to a Nash equilibrium. The concept of *subgame perfect equilibria* refines the concept of Nash equilibrium by imposing that at each step of the history, the strategy behaves like Nash equilibrium if we were to start the game now. Formally, let us write $\sigma_P \circ h$ the strategy which maps all histories $h'$ to $\sigma_P(h \cdot h')$, that is the strategy that behave like $\sigma_P$ after $h$. Then $(\sigma_P)_{P \in \mathcal{P}}$ is a *subgame perfect equilibrium* if for all histories $h$, $(\sigma_P \circ h)_{P \in \mathcal{P}}$ is a Nash equilibrium.

Imposing such a strong restriction is justified by the fact that subgame perfect Nash equilibria exist for a large class of games. In particular subgame perfect equilibria always exist in turn-based games with reachability objectives.

**Example 34.** Consider the example of Figure 13.3. There is a Nash equilibria whose outcome goes through states $v_0 \to v_1 \to \Omega_1$. In this equilibrium, Player 1 should play $b$ in $v_2$, so that the best response of Player 2 is to play $a$ at $v_0$. Intuitively, player 1 is threatening player 2, to make them both lose from $v_2$, but this threat is not credible, and the profile is not a subgame perfect equilibrium. In fact, once $v_2$ is reached it is better for Player 1 to play a so it is unlikely that the player will execute the said threat. The only subgame perfect equilibrium of this game ends in the vertex satisfying both $\Omega_1$ and $\Omega_2$.
<figure><img src="image_116.png" /><figcaption>Figure 13.3: Two-player game with reachability objectives. The goal of player 1 is to reach a state labeled with $\Omega_1$ and that of player 2 is to reach a state labeled with $\Omega_2$.</figcaption></figure>

## Robust equilibria

The notion of robust equilibria refines Nash equilibria in two ways:

* a robust equilibrium is *resilient*, i.e. when a small coalition changes its strategy, none of the players of the coalition improves their payoff;

* it is *immune*, i.e. when a small coalition changes its strategy, it does not decrease the payoffs of the non-deviating players.

The size of small coalitions is determined by parameter *k* for resilience and *t* for immunity. When a strategy is both *k*-resilient and *t*-immune, it is called a (*k*,*t*)-robust equilibrium.

The motivation behind this concept is to address these two weaknesses of Nash equilibria:

* There is no guarantee on payoffs when two (or more) players deviate together. Such a situation can occur in networks if the same person controls several devices (a laptop and a phone for instance) and can then coordinate their behaviours. In this case, the devices would be considered as different players and Nash equilibria can offer no guarantee.

* When a deviation occurs, the strategies of the equilibrium can punish the deviating user without any regard for the payoffs of the others. This can result in a situation where, because of a faulty device, nobody can use the protocol anymore.

By comparison, finding resilient equilibria with $k > 1$, ensures that clients have no interest in forming coalitions (up to size *k*), and finding immune equilibria with
$t > 0$ ensures that other clients will not suffer from some players (up to $t$) behaving differently from what was expected.

The deviator construction can be reused for finding such equilibria. We only need to adapt the objectives. Given a game $G = (\mathcal{A}, (f_P)_{P \in \mathcal{P}})$, a strategy profile $\sigma_{\mathcal{P}}$, and parameters $k, t$, we have

* The strategy profile $\sigma_{\mathcal{P}}$ is $k$-resilient if, and only if, strategy $\kappa(\sigma_{\mathcal{P}})$ is winning in $\text{DevGame}(\mathcal{A})$ for the *resilience objective} \mathcal{R}(k, F)$ where $F = (f_P(\text{Out}_{\mathcal{A}}(v_0, \sigma_{\mathcal{P}})))_{P \in \mathcal{P}}$ is the payoff profile of $\sigma_{\mathcal{P}}$ and $\mathcal{R}(k, F)$ is defined by:

$$ \begin{aligned} \mathcal{R}(k, F) = & \{\rho \in \text{Out}_{\text{DevGame}(\mathcal{A})} \mid |\text{Dev}(\rho)| > k\} \\ & \cup \{\rho \in \text{Out}_{\text{DevGame}(\mathcal{A})} \mid |\text{Dev}(\rho)| = k \land \forall P \in \text{Dev}(\rho). f_P(\text{proj}_{\text{Out}}(\rho)) \le F_P\} \\ & \cup \{\rho \in \text{Out}_{\text{DevGame}(\mathcal{A})} \mid |\text{Dev}(\rho)| < k \land \forall P \in \mathcal{P}. f_P(\text{proj}_{\text{Out}}(\rho)) \le F_P\}. \end{aligned} $$

* The strategy profile $\sigma_{\mathcal{P}}$ is $t$-immune if, and only if, strategy $\kappa(\sigma_{\mathcal{P}})$ is winning for the *immunity objective} \mathcal{I}(t, F)$ where $F = (f(\text{Out}_{\mathcal{A}}(v_0, \sigma_{\mathcal{P}})))_{P \in \mathcal{P}}$ is the payoff profile of $\sigma_{\mathcal{P}}$ and $\mathcal{I}(t, F)$ is defined by:

$$ \begin{aligned} \mathcal{I}(t, F) = & \{\rho \in \text{Out}_{\text{DevGame}(\mathcal{A})} \mid |\text{Dev}(\rho)| > t\} \\ & \cup \{\rho \in \text{Out}_{\text{DevGame}(\mathcal{A})} \mid \forall P \in \mathcal{P} \setminus \text{Dev}(\rho). F_P \le f_P(\text{proj}_{\text{Out}}(\rho))\}. \end{aligned} $$

* The strategy profile $\sigma_{\mathcal{P}}$ is a $(k,t)$-robust profile in $G$ if, and only if, $\kappa(\sigma_{\mathcal{P}})$ is winning for the *robustness objective*

$$ \mathcal{R}(k, t, F) = \mathcal{R}(k, F) \cap \mathcal{I}(t, F), $$

where $F = (f_P(\text{Out}_{\mathcal{A}}(v_0, \sigma_{\mathcal{P}})))_{P \in \mathcal{P}}$ is the payoff profile of $\sigma_{\mathcal{P}}$.

We omit the proof and encourage the reader to do it by themselves.

## Extension to games with hidden actions

In most practical cases, players only have a partial view of the state of the system; so they may not be able, for instance, to detect a deviating player immediately. Studying equilibria in general imperfect information as in Chapter 8 would be well adapted in such situations. Unfortunately, these games are too powerful in general since the existence of Nash equilibria is undecidable in this case.

Nevertheless, the problem is decidable for a restricted form of imperfect information where the players observe the visited states but do not see the played actions; thus the actions are *hidden*.

We will thus consider strategies defined as functions from $V^*$ to Act, which represents the fact that players' decision can only depend on observed sequence of states but not on other players' actions.

In this case, deviators cannot be defined as obviously as before, as it may not always be possible to identify one unique deviator responsible for a deviation. The construction will thus maintain a set of suspects, those players that might have been responsible
<figure><img src="image_117.png" /><figcaption>Figure 13.4: Three-player game with hidden actions. The goal of player *i* is to reach a state labeled with $\Omega_i$.</figcaption></figure>

for the observed deviation. Formally, suspects for an edge $(v, v')$ with respect to a move $(a_P)_{P \in \mathcal{P}}$ are players *P* such that there is $a'_P$ and $\Delta(a'_P, a_{-P}) = (v, v')$. Rather than computing the union of deviators along a history, we now consider the intersection of suspects. That is, if at vertex *v*, the suspect set is *S*, and the strategy profile is $\sigma_{\mathcal{P}}$, and if the next vertex is *v'*, then the suspect set becomes $S \cap \{P \in \mathcal{P} \mid \exists a'_P, \Delta(a'_P, a_{-P}) = (v, v')\}$.

The suspect game can be defined just like the deviator game by replacing the deviators component by the suspects component. The objective for Eve is that no suspect player improves their payoff. In fact, in case of deviation, we know that the deviator belongs to the set of suspects although we cannot know which one has deviated for sure so Eve must ensure this for all suspects.

**Example 35.** Consider the example of Figure 13.4. If actions were visible there would be an equilibrium ending in the state labeled with $\Omega_3$: player 3 simply has to punish the player who would deviate from this path. But if we now consider hidden actions, in case of a deviation, player 3 would observe that the play went arrives in $v_1$ instead of $v_2$ and both Player 1 and Player 2 are suspects. Since Player 3 cannot punish both players at the same time, there is no Nash equilibrium ending satisfying $\Omega_3$.

## 13.2 Admissible strategies

Nash equilibria and their variants seen so far describe stable situations from which players have no incentive to deviate. This however is of limited use in some situations. First, the stability relies on the fact that all players are informed of the strategy profile to be played; that is, some central authority needs to publicly announce the strategies for all players. Second, each equilibrium describes a single possible situation. If there are several equilibria, it is not clear which one is to be chosen.
<table><caption>Table 13.3: A normal form game solvable by iterated elimination.</caption><thead><tr><th></th><th>A</th><th>B</th></tr></thead><tbody><tr><th>C</th><td>3, 3</td><td>4, 1</td></tr><tr><th>D</th><td>0, 4</td><td>0, 0</td></tr></tbody></table>

Rather than concentrating on particular equilibria, game theorists have studied reasons players may follow in order to exclude some strategies that are necessarily worse than others. These worse strategies are called *dominated*. By formalizing dominated and non-dominated strategies for a given player, one can then predict the behaviour of rational players since such a player would never use a dominated strategy but rather always pick the best one available.

In this section, we will formalize dominated strategies and show how these can be computed in games. We then briefly show that this reasoning can be repeated, and present the iterated elimination of dominated strategies.

### 13.2.1 Definition

The notion of *dominance* is used to compare strategies with respect to payoffs they yield against the rest of the players' strategies. Consider the example of Table 13.3. Given a strategy of the second player, playing *B* is always at least as good as playing *A* for the first player. In fact, again *C*, *B* yields a payoff of 4 which is better than 3, the payoff of *A*; and against *D*, both yield 0. The strategy *B* is said to dominate *A*. Intuitively, *B* is either better or as good as *A* in all situations, so playing *B* is the rational choice for Player 1.

Furthermore, by this analysis, Player 2 knows that Player 1 will play *B*. Given this information, the best response of Player 1 is to play *C*. By iterated elimination, we established that (*B*, *C*) should be the only strategy profile to be played by players following this reasoning.

Let us formalize this notion.

**Definition 36 (Dominance).** Let $S \subseteq \mathcal{S}^\mathcal{P}$ be a set of the form $S = S_1 \times S_2 \times \cdots \times S_n$ which we will call a rectangular set. Let $\sigma, \sigma' \in S_i$. Strategy $\sigma$ very weakly dominates strategy $\sigma'$ with respect to $S$, written $\sigma_i \ge_s \sigma'_i$, if from all vertices $v_0$:

$$ \forall \sigma_{-i} \in S_{-i}, f_i(\mathrm{Out}(v_0, \sigma'_i, \sigma_{-i})) \ge f_i(\mathrm{Out}(v_0, \sigma_i, \sigma_{-i})). $$

Strategy $\sigma_i$ weakly dominates strategy $\sigma'_i$ in $S$, written $\sigma >_S \sigma'$, if $\sigma \ge_S \sigma'$ and $-(\sigma' \le_S \sigma)$. A strategy that is not weakly dominated in $S$ is admissible in $S$. The subscripts on $\ge_S$ and $>_S$ are omitted when the sets of strategies are clear from the context.

Algorithms rely on the notion of *optimistic* and *pessimistic value* of a history. The pessimistic value is the maximum payoff that a player can ensure in the worst case
<figure><img src="image_118.png" /><figcaption>Figure 13.5: Example of a three-player turn-based simple safety game. Numbers below states describe the safety objective, for instance -1, -1, 0 is losing for player 1 and 2.</figcaption></figure>

within the strategy set $S$. The optimistic value is the best the player can achieve with the help of other players, given the strategy set $S$.

**Definition 37 (Values).** The pessimistic value of a strategy $\sigma_i$ for a history $h$ with respect to a rectangular set of strategies $S$, is

$$ \bullet \text{ pes}_i(S, h, \sigma_i) = \inf_{\sigma_{-i} \in S_{-i}} f_i(h \cdot \text{Out}(\text{last}(h), \sigma_i, \sigma_{-i})). $$

The pessimistic value of a history $h$ for $A_i$ with respect to a rectangular set of strategies $S$ is given by:

$$ \bullet \text{ pes}_i(S, h) = \sup_{\sigma_i \in S_i} \text{pes}_i(S, s, \sigma_i). $$

The optimistic value of a strategy $\sigma_i$ for a history $h$ with respect to a rectangular set of strategies $S$ is given by:

$$ \bullet \text{ opt}_i(S, h, \sigma_i) = \sup_{\sigma_{-i} \in S_{-i}} f_i(h_{\le |h| - 2} \cdot \text{Out}(\text{last}(h), \sigma_i, \sigma_{-i})). $$

The optimistic value of a history $h$ for $A_i$ with respect to a rectangular set of strategies $S$ is given by:

$$ \bullet \text{ opt}_i(S, h) = \sup_{\sigma_i \in S_i} f_i(\text{opt}_i(S, h, \sigma_i)) $$

We will first consider the case where $S$ is the set of all strategies, and omit $S$ in the above notations.

### 13.2.2 Simple Safety games

Simple safety games, are safety games in which there are no transitions from losing vertices to non-losing ones. Restricting to this particular class of game makes the problem simpler because the objective becomes prefix independent. Any safety game can be converted to an equivalent simple safety game by encoding in the states which players have visited so far a losing state. Note that this translation can be exponential in the number of players.
For simple safety games, the pessimistic and optimistic values do not depend on
the full history but only on the last state: for all histories $pes_i(h) = pes_i(last(h))$ and
$opt_i(h) = opt_i(last(h))$.

Note that in safety games (and any qualitative games) values can be only 1 (for winning) and 0 (for losing) and since the pessimistic value is always less than the optimistic one, the pair ($pes_i, opt_i$) can only take three values: (0,0), (0,1) and (1,1).

Intuitively, players should avoid decreasing this pair of values if they can. In fact, the characterization of admissible strategies we give below will be based on this simple observation.

**Example 36.** An example of a simple safety game is given in Figure 13.5. In this game, player 1 controls $v_1$ where its optimistic value is 0, as it is possible that the outcome will never reach $v_3$ or $v_4$. However $v_3$ has optimistic value -1 for player 1, as it is a losing state for player 1. Going from $v_1$ to $v_3$ is a bad choice for player 1, and it is indeed dominated by the strategy that would always choose to go to $v_2$. In state $v_3$, player 3 has pessimistic value 0 since it can ensure not visiting $v_4$. The winning strategy for player 3 which is to always go to $v_1$ is also the only non-dominated strategy. For player 2, from state $v_0$, both choices lead to a state with values (-1,0) so no choice is particularly better and both strategies are non-dominated.

**Definition 38.** Let $D_i$ be the set of edges $(v, v') \in E$ such that $v \in V_i \text{ pes}_i(v) > \text{pes}_i(v')$ or $opt_i(v) > opt_i(v')$. These are called dominated edges.

**Theorem 141** (Characterisation of admissible strategies). Admissible strategies for player $A_i$ are the strategies that never take actions in $D_i$.

*Proof.* We show that if $A_i$ plays an admissible strategy $\sigma_i$ then the value cannot decrease on a transition controlled by $A_i$. Let $\rho \in \text{Out}(\sigma_i, \sigma_{-i})$, and $k$ an index such that $\rho_k \in V_i$. Let $(v, v') = \sigma_i(\rho_{\le k})$:

* If $pes_i(\rho_k) = 1$, then $\sigma_i$ has to be winning against all strategies $\sigma_{-i}$ of $A_{-i}$, otherwise it would be weakly dominated by such a strategy. Since there is no such strategy from a state with value $pes_i \le 0$, we must have $pes_i(v') = 1$.

* If $opt_i(\rho_k) = 1$, then there is a profile $\sigma'$ such that $\rho = f(\text{Out}(v, \sigma'))$, which is equal to 1. Assume that $opt_i(v') = 0$. Then $\sigma_i$ is dominated by the strategy $\sigma_i''$ obtained from $\sigma_i$ by making it switch to $\sigma'$ at $v$. In fact, $\sigma_i$ is losing against all strategies of $-i$, while $\sigma_i''$ is winning at least against $\sigma_{-i}$.

* If $pes_i(v) = 0$ or $opt_i(s) = 0$, then the value cannot decrease further.

In the other direction, let $\sigma_i, \sigma_i'$ be two strategies of player $A_i$ and assume $\sigma_i' >_S \sigma_i$. We will prove $\sigma_i$ takes a transition in $D_i$ at some point.

Let us fix some objects before developing the proof. There is a vertex $v$ and strategy profile $\sigma_{-i} \in S_{-i}$ such that $f(\text{Out}(v, \sigma_i', \sigma_{-i})) = 1 \wedge f(\text{Out}(v, \sigma_i, \sigma_{-i})) = 0$. Let $\rho = \text{Out}(v, \sigma_i, \sigma_{-i})$ and $\rho' = \text{Out}(v, \sigma_i', \sigma_{-i})$. Consider the first position where these runs differ: write $\rho = w \cdot s' \cdot s_2 \cdot w'$ and $\rho' = w \cdot s' \cdot s_1 \cdot w''$.

The following are simple facts that can be seen easily:
• $s' \in V_i$, because the strategy of the other players are identical in the two runs.

• $\text{opt}_i(s_1) = 1$ because $f(\text{Out}(v, \sigma'_i, \sigma_{-i})) = 1$

• $\text{pes}_i(s_2) = 0$ because $f(\text{Out}(v, \sigma'_i, \sigma_{-i})) = 0$

If $\text{opt}_i(s_2) = 0$ or $\text{pes}_i(s_1) = 1$ then $s' \to s_2 \in D_i$ so $\sigma_i$ takes a transition of $D_i$. The remaining case to complete the proof is $\text{opt}_i(s_2) = 1$ and $\text{pes}_i(s_1) = 0$. Let us assume that $\sigma_i$ does not take any edges from $D_i$. We will show that there is a strategy for $-i$ against which $\sigma_i$ wins and $\sigma'_i$ loses, which contradicts the hypothesis that $\sigma'_i$ weakly dominates $\sigma_i$.

We first construct a profile $\sigma^2_{-i} \in S_{-i}$ such that $f(\text{Out}(s_2, \sigma_i, \sigma^2_{-i})) = 1$. Strategy $\sigma^2_{-i} \in S_{-i}$ never decreases the optimistic value from 1 to 0 since the optimistic value is non-increasing. By assumption, $\sigma_i$ itself does not decrease the value of $A_i$ because it does not take transitions of $D_i$. So the outcome of $(\sigma_i, \sigma^2_{-i})$ never reaches a state of optimistic value 0. Hence it never reaches a state in $\text{Bad}_i$ and therefore it is winning for $A_i$.

Let us now consider a profile $\sigma^1_{-i} \in S_{-i}$ such that $f(\sigma'_i, \sigma^1_{-i}) = 0$ from $s_1$. Such a strategy exists because $\text{pes}_i(s_1) = 0$, so $\sigma'_i$ is not a winning strategy. Then there exists a strategy profile $\sigma^1_{-i}$ such that $\sigma'_i$ loses from $s_1$.

Now consider strategy profile $\sigma'_{-i}$ that plays like $\sigma_{-i}$ if the play does not start with $w$; and otherwise switches to $\sigma^1_{-i}$ at history $w s_1$ and to $\sigma^2_{-i}$ at history $w s_2$. Formally, given a history $h$, $\sigma'_{-i}(h) =$

• $\sigma^1_{-i}(h')$ if $w \cdot s_1$ is a prefix of $h$ and $w \cdot s_1 \cdot h' = h$

• $\sigma^2_{-i}(h')$ if $w \cdot s_2$ is a prefix of $h$ and $w \cdot s_2 \cdot h' = h$

• $\sigma_{-i}(h)$ otherwise

Clearly we have $f_i(\text{Out}_s(\sigma_i, \sigma'_{-i})) = 1 \wedge f_i(\text{Out}_s(\sigma'_i, \sigma'_{-i})) = 0$, which contradicts $\sigma'_i \ge_s \sigma_i$. $\square$

### 13.2.3 Parity games

The characterization given for simple safety game is not enough for parity objectives, as we will see in the following example.

**Example 37.** Consider the example in Figure 13.6. In this example, although the strategy that always stays in $v_0$ does not decrease the value of player 1, it is dominated because it has no chance of winning. By contrast the strategy that always goes to $v_1$ has a chance of being helped by player 2 and actually reaching $\Omega_1$ it therefore dominates the first strategy.

However the fact that an admissible strategy should not decrease its own value still holds. Assuming strategy $\sigma_i$ of player $P_i$ does not decrease its own value, we can classify its outcome in three categories according to their ultimate values.

• either ultimately $\text{opt}_i = 0$, in which case all strategies are losing, and thus any strategy is admissible
<figure><img src="image_119.png" /><figcaption>Figure 13.6: Parity game where the objective for player 1 is to visit $\Omega_1$ infinitely often. Player 1 controls square vertices and player 2 round vertices.</figcaption></figure>

• or ultimately $pes_i = 1$, in which case admissible strategies are exactly the winning ones

• or ultimately $pes_i = 0$ and $opt_i = 1$. We will focus on this case which is more involved.

From a state of value 0, an admissible strategy of $P_i$ should allow a winning play for $P_i$ with the help of other players.

We write $H_i$ for set of vertices $v$ controlled by a player $P_j \neq P_i$ that have at least two successors of optimistic value 1. Formally, the *help-states* $H_i$ of player $P_i$ are defined as:

$$ \bigcup_{P_j \in \mathcal{P} \setminus \{i\}} \{s \in V_j \mid \exists s', s'', s' \neq s'' \wedge s \to s' \wedge s \to s'' \wedge \text{opt}_i(s') = 1 \wedge \text{opt}_i(s'') = 1 \}. $$

Intuitively, admissible strategies in the case satisfying $pes_i = 0$ and $opt_i = 1$ are those that visit infinitely often help states. In fact, letting other players make choices means that the player is allowing the possibility of them helping to achieve the objective. More precisely, we have the following property whose proof is omitted.

**Lemma 149.** Let $v \in V$, $P_i \in \mathcal{P}$ and $\rho$ a play be such that $\exists^\infty k. \text{opt}_i(\rho_k) = 1$. There exists $\sigma_i$ admissible such that $\rho \in \text{Out}(v, \sigma_i)$ if, and only if, $f_i(\rho) = 1$ or $\exists^\infty k. \rho_k \in H_i$.

### 13.2.4 Iterated elimination

Once each player is restricted to use admissible strategies, they can further refine their choices knowing that other players will not be using dominated strategies. We already saw this in the example of Table 13.3. In fact, once player 1 has eliminated strategy A (which is dominated by B), player 2 can use this information since its best response against the remaining strategies is C. In more complex games, this reasoning can be repeated and take several steps before converging. This repeated process is called *iterated elimination of dominated strategies*.

We now define this process formally.
**Definition 39** (Iterated elimination). The sequence of iterative elimination is a sequence of rectangular strategy sets defined as follows. $S^0 = (S_i^0)_{P_i \in \mathcal{P}}$ is the set of all strategies. For $k \ge 0$, if we write $S^k = (S_i)_{P_i \in \mathcal{P}}$, then $S_i^{k+1}$ is the set of strategies in $S_i^k$ that are not dominated in $S^k$.

Thus, the step 1 of the sequence of iterative elimination corresponds to admissible strategies defined above. Let us call them 1-admissible. In step 2, we again compute strategies that are dominated by only considering 1-admissible strategies for all players, and repeat. Strategies that survive all step of elimination are said iteratively admissible.

**Theorem 142.** In parity games, the sequence of iterative elimination converges, and it reaches a non-empty fixed point.

We prove this result only for simple safety games since the case of parity conditions is too complex for the scope of this book.

Intuitively, given a game $G$, Theorem 141 tells us that any strategy for player $P_i$ that avoids using edges $D_i$ is admissible. So if we remove all edges $\cup_{P_i \in \mathcal{P}} D_i$ from the game to obtain a new game called $G_1$, then all strategies of $G_1$ (for all players) are admissible in $G$, and conversely. We can then repeat this process to $G_1$: we construct $G_2$ by eliminating all dominated edges in $G_1$, and get that admissible strategies in $G_1$ are exactly all strategies of $G_2$, which correspond to 2-admissible strategies, and so on.

Since the size of the games decrease at each step, this process necessarily stops. It remains to show that the limit game $G_\infty$ contains strategies. We will show that all vertices have at least one outgoing edge in $G_\infty$. It suffices to show that the sets $D_i$ never contains all edges leaving a vertex. Let us consider any game $G_j$. For a vertex $v \in V_i$ with $\text{pes}_i(v) = 0$ and $\text{opt}_i(v) = 0$, none of the edges are dominated. For a vertex $v \in V_i$ with $\text{pes}_i(v) = 1$ (and necessarily $\text{opt}_i(v) = 1$), there exists a winning strategy in $G_j$ so there must be a successor $v'$ with $\text{pes}_i(v') = 1$ which is not dominated. Last, for a vertex $v \in V_i$ with $\text{pes}_i(v) = 0$ and $\text{opt}_i(v) = 1$, there exists a winning play from $v$ so for some successor $v'$ we must have $\text{opt}_i(v') = 1$ which is an edge that is not dominated.

# Bibliographic references

Most results about equilibria fall into two-categories: they either prove that equilibria always exist for some class of games, or they characterize the complexity of finding a particular one.

## Existence results

Several authors have noticed that Nash equilibria always exist in turn-based game for some classes of objectives, in particular this is true of $\omega$-regular objectives. The most general result of that kind shows that this is true for all objectives for which there exist finite memory optimal strategies [RP18].

The notion of equilibrium we now call Nash equilibrium was defined in the article of Nash [Nas50] in which he proves the existence for a class of normal form game. The Hawk-dove game we presented as an example in the first part of this chapter is
also called game of chicken. The first reference to this game was by Smith and Price
[SP73]. The example of medium of access control we presented as a motivation was
studied from a game theoretic point of view in [MW03].

The notion of subgame perfect equilibria is interesting because in games on trees (or extensive games), for which they were originally introduced, they always exist. This results can be extended to games played on graphs. In particular subgame perfect equilibria always exist in reachability games [BBdPG12].

Algorithms and complexity results

The deviator construction and the algorithm presented in this chapter are based on
[BBMU11, Bre12]. Algorithms on admissible strategies on infinite games and the
complexity of the related problems were studied in [Ber07b, BRS14].

Imperfect information games in the context of multiplayer games are difficult. As soon as there are ‘information forks’ interesting problems are undecidable. Deciding whether two players can ensure an objective against a third player is undecidable. As a corollary the Nash equilibrium problem is also undecidable [PR90]. The problem of Nash equilibrium is also undecidable in stochastic games even with only three players [BMS14].

In the first section we presented a polynomial algorithm for finding pure Nash equi-
libria in normal form games. It is actually also possible to find a mixed Nash equilibria
in polynomial time using linear programming. The same extends to finding memory-
less mixed Nash equilibria in concurrent games, and even resilient equilibria [Bre16].

Action-graphs are succinct representation of matrix games. Indeed, representing
games with matrices can be costly when the number of players increases. The size
of the matrix is in fact exponential in the number of players: when each player has
two strategies there are $2^{|\Sigma|}$ cells in the table. The action-graph representation is more
compact, and the representation can be exponentially smaller. Because of that, the al-
gorithm is no longer polynomial. If there are no constraints on the Nash equilibrium
we are looking for, the complexity of the problem cannot be characterized using clas-
sical classes like NP-completeness because equilibria always exist and thus the answer
to the decision problem would always be true. The characterization of the complexity
was done using the PPAD class [DGP09].

Nash equilibria with LTL objectives is expressible in logics such as strategy logic [CHP10] or ATL\* [AHK02], as well as other extensions of this equilibria. However, satisfiability in these logic is difficult: it is 2EXP-complete for ATL\* and undecidable for strategy logic in general. A decidable fragment of strategy logic has been identified [MMPV12], but remains difficult; it is 2EXP-complete.
# Conclusions

The goal of this book was to give a technical account of the state of affairs on games on graphs. It emerged as a research topic already decades ago, and is now an active field with interactions with many other disciplines. In this conclusion, let us note that it has two appealing features:

* A well defined and small set of fundamental open problems. The most prominent ones are the complexity of solving parity games, mean payoff games, discounted games, and stochastic reachability games. Many others have been discussed in this book.

* A wealth of new models and directions. Let us cite as examples progress towards understanding the memory requirements [Ohl23, BRV23], bidding mechanisms [AHZ21], or distributed games [GMMW22].
Bibliography

[ABd03] Parosh Aziz Abdulla, Ahmed Bouajjani, and Julien d'Orso. Deciding monotonic games. In *Proceedings of the EACSL Annual Conference on Computer Science and Logic*, CSL'03, volume 2803. Springer-Verlag, 2003.

[ABDL18] Natasha Alechina, Nils Bulling, Stéphane Demri, and Brian Logan. On the complexity of resource-bounded logics. *Theoretical Computer Science*, 750, 2018.

[ABGJ14] Xavier Allamigeon, Pascal Benchimol, Stéphane Gaubert, and Michael Joswig. Combinatorial simplex algorithms can solve mean payoff games. *SIAM Journal on Control and Optimization*, 24, 2014.

[AC88] André Arnold and Paul Crubillé. A linear algorithm to solve fixed-point equations on transition systems. *Information Processing Letters*, 29, 1988.

[AČJT00] Parosh Aziz Abdulla, Kārlis Čerāns, Bengt Jonsson, and Yih-Kuen Tsay. Algorithmic analysis of programs with well quasi-ordered domains. *Information and Computation*, 160, 2000.

[ACTDG13] Marianne Akian, Jean Cochet-Terrasson, Sylvie Detournay, and Stéphane Gaubert. Solving multichain stochastic games with mean payoff by policy iteration. In *Proceedings of the IEEE Conference on Decision and Control, CDC'13*. IEEE Computer Society, 2013.

[AD94] Rajeev Alur and David L. Dill. A theory of timed automata. *Theoretical Computer Science*, 126, 1994.

[ADD00] Robert B. Ash and Catherine A. Doléans-Dade. *Probability and Measure Theory*. Academic Press, 2000.

[AdMS21] David Auger, Xavier Badin de Montjoye, and Yann Strozecki. A generic strategy iteration method for simple stochastic games. In *Proceedings of*
the International Symposium on Mathematical Foundations of Computer Science, MFCS'21, volume 202. Schloß Dagstuhl, 2021.

[AG11] Krzysztof R. Apt and Erich Grädel. *Lectures in Game Theory for Computer Scientists*. Cambridge University Press, 2011.

[AGKS22] Xavier Allamigeon, Stéphane Gaubert, Ricardo D. Katz, and Mateusz Skomra. Universal complexity bounds based on value iteration and application to entropy games. In *Proceedings of the International Colloquium on Automata, Languages and Programming, ICALP'22*, volume 229. Schloß Dagstuhl, 2022.

[AHK02] Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time temporal logic. *Journal of the ACM*, 49, 2002.

[AHZ21] Guy Avni, Thomas A. Henzinger, and Dorde Zikelic. Bidding mechanisms in graph games. *Journal of Computer and System Sciences*, 119, 2021.

[AKV16] Shaull Almagor, Orna Kupferman, and Yaron Velner. Minimizing expected cost under hard Boolean constraints, with applications to quantitative synthesis. In *Proceedings of the International Conference on Concurrency Theory, CONCUR'16*, volume 59. Schloß Dagstuhl, 2016.

[AM09] Daniel Andersson and Peter Bro Miltersen. The complexity of solving stochastic games on graphs. In *Proceedings of the International Symposium on Algorithms and Computation, ISAAC'09*, volume 5878. Springer-Verlag, 2009.

[AMPS98] Eugene Asarin, Oded Maler, Amir Pnueli, and Joseph Sifakis. Controller synthesis for timed automata. In *Proceedings of the IFAC Conference on System Structure and Control, SSC'98*. Elsevier, 1998.

[AMSS13] Parosh Aziz Abdulla, Richard Mayr, Arnaud Sangnier, and Jeremy Sproston. Solving parity games on integer vectors. In *Proceedings of the International Conference on Concurrency Theory, CONCUR'13*, volume 8052. Springer-Verlag, 2013.

[AR17] Benjamin Aminof and Sasha Rubin. First-cycle games. *Information and Computation*, 254, 2017.

[Aum64] Robert J. Aumann. Mixed and behavior strategies in infinite extensive games. In *Advances in Game Theory*, volume 52. Princeton University Press, 1964.

[Bar68] Erwin H. Bareiss. Sylvester's identity and multistep integer-preserving Gaussian elimination. *Mathematics of Computation*, 22, 1968.

[BB79] Catriel Beeri and Philip A. Bernstein. Computational problems related to the design of normal form relational schemas. *ACM Transactions on Database Systems*, 4, 1979.
[BBC⁺14] Tomáš Brázdil, Václav Brožek, Krishnendu Chatterjee, Vojtech Forejt, and Antonín Kučera. Markov decision processes with multiple long-run average objectives. *Logical Methods in Computer Science*, 10, 2014.

[BBdPG12] Thomas Brihaye, Véronique Bruyère, Julie de Pril, and Hugo Gimbert. Subgame perfection for equilibria in quantitative reachability games. In *Proceedings of the International Conference on the Foundations of Software Science and Computational Structures, FoSSaCS'12*, 2012.

[BBEK11] Tomáš Brázdil, Václav Brožek, Kousha Etessami, and Antonín Kučera. Approximating the termination value of one-counter MDPs and stochastic games. In *Proceedings of the International Colloquium on Automata, Languages and Programming, ICALP'11*. Springer-Verlag, 2011.

[BBM06] Patricia Bouyer, Thomas Brihaye, and Nicolas Markey. Improved undecidability results on weighted timed automata. *Information Processing Letters*, 98, 2006.

[BBMU11] Patricia Bouyer, Romain Brenguier, Nicolas Markey, and Michael Ummels. Nash Equilibria in Concurrent Games with Büchi Objectives. In *Proceedings of the International Conference on the Foundations of Software Technology and Theoretical Computer Science, FSTTCS'11*, volume 13. Schloß Dagstuhl, 2011.

[BBR05] Thomas Brihaye, Véronique Bruyère, and Jean-François Raskin. On optimal timed strategies. In *Proceedings of the International Conference on Formal Modelling and Analysis of Timed Systems, FORMATS'05*, volume 3829. Springer-Verlag, 2005.

[BC18] Mikołaj Bojańczyk and Wojciech Czerwiński. An automata toolbox, 2018.

[BCD⁺07] Gerd Behrmann, Agnès Cougnard, Alexandre David, Emmanuel Fleury, Kim G. Larsen, and Didier Lime. UPPAAL-Tiga: Time for playing games! In *Proceedings of the International Conference on Computer Aided Verification, CAV'07*, volume 4590. Springer-Verlag, 2007.

[BCD⁺11] Luboš Brim, Jakub Chaloupka, Laurent Doyen, Rafaella Gentilini, and Jean-François Raskin. Faster algorithms for mean-payoff games. *Formal Methods for System Design*, 38, 2011.

[BCFK17] Tomáš Brázdil, Krishnendu Chatterjee, Vojtech Forejt, and Antonín Kučera. Trading performance for stability in Markov decision processes. *Journal of Computer and System Sciences*, 84, 2017.

[BCH⁺16] Romain Brenguier, Lorenzo Clemente, Paul Hunter, Guillermo A. Pérez, Mickael Randour, Jean-François Raskin, Ocan Sankur, and Mathieu Sasolas. Non-zero sum games for reactive synthesis. In *Proceedings of the International Conference on Language and Automata Theory and Applications, LATA'16*, volume 9618. Springer-Verlag, 2016.
[BCH$^{+}$21] Christopher H. Broadbent, Arnaud Carayol, Matthew Hague, Andrzej S. Murawski, C.-H. Luke Ong, and Olivier Serre. Collapsible pushdown parity games. *ACM Transactions on Computational Logic*, 22, 2021.

[BCKN12] Tomáš Brázdil, Krishnendu Chatterjee, Antonín Kučera, and Petr Novotný. Efficient controller synthesis for consumption games with multiple resource types. In *Proceedings of the International Conference on Computer Aided Verification, CAV'12*, volume 7358. Springer, 2012.

[BCNV20] Tomáš Brázdil, Krishnendu Chatterjee, Petr Novotný, and Jiri Vahala. Reinforcement learning of risk-constrained policies in Markov decision processes. In *Proceedings of the AAAI Conference on Artificial Intelligence, AAAI'20*. AAAI Press, 2020.

[BDMP03] Patricia Bouyer, Deepak D'Souza, Parthasarathy Madhusudan, and Antoine Petit. Timed control with partial observability. In *Proceedings of the International Conference on Computer Aided Verification, CAV'03*, volume 2725. Springer-Verlag, 2003.

[BDOR20] Thomas Brihaye, Florent Delgrange, Youssouf Oualhadj, and Mickael Randour. Life is random, time is not: Markov decision processes with window objectives. *Logical Methods in Computer Science*, 16, 2020.

[BEGM19] Endre Boros, Khaled Elbassioni, Vladimir A. Gurvich, and Kazuhisa Makino. A pseudo-polynomial algorithm for mean payoff stochastic games with perfect information and few random positions. *Information and Computation*, 267, 2019.

[Bel57] Richard Bellman. A Markovian decision process. *Journal of Mathematics and Mechanics*, 1957.

[BEM97] Ahmed Bouajjani, Javier Esparza, and Oded Maler. Reachability analysis of pushdown automata: Application to model-checking. In *Proceedings of the International Conference on Concurrency Theory, CONCUR'97*, volume 1243. Springer, 1997.

[Ber07a] Dimitri P. Bertsekas. *Dynamic Programming and Optimal Control*. Athena Scientific, 2007.

[Ber07b] Dietmar Berwanger. Admissibility in infinite games. In *Proceedings of the International Symposium on Theoretical Aspects of Computer Science, STACS'07*, volume 4393. Springer-Verlag, 2007.

[BF68] David Blackwell and Chris Ferguson. The big match. *Annals of Mathematical Statistics*, 1968.

[BFL$^{+}$08] Patricia Bouyer, Uli Fahrenberg, Kim G. Larsen, Nicolas Markey, and Jiří Srba. Infinite runs in weighted timed automata with energy constraints. In *Proceedings of the International Conference on Formal Modelling and Analysis of Timed Systems, FORMATS'08*, volume 5215. Springer-Verlag, 2008.
[BFM15] Patricia Bouyer, Erwin Fang, and Nicolas Markey. Permissive strategies in timed automata and games. In *Proceedings of the International Workshop on Automated Verification of Critical Systems, AVoCS'15*, volume 72. European Association of Software Science and Technology, 2015.

[BFRR17] Véronique Bruyère, Emmanuel Filiot, Mickael Randour, and Jean-François Raskin. Meet your expectations with guarantees: Beyond worst-case synthesis in quantitative games. *Information and Computation*, 254, 2017.

[BG11] Laura Bozzelli and Pierre Ganty. Complexity analysis of the backward coverability algorithm for VASS. In *Proceedings of the International Workshop on Reachability Problems, RP'11*, volume 6945. Springer-Verlag, 2011.

[BGG17] Nathalie Bertrand, Blaise Genest, and Hugo Gimbert. Qualitative determinacy and decidability of stochastic games with signals. *Journal of the ACM*, 64, 2017.

[BGHM17] Thomas Brihaye, Gilles Geeraerts, Axel Haddad, and Benjamin Monmege. Pseudopolynomial iterative algorithm to solve total-payoff games and min-cost reachability games. *Acta Informatica*, 54, 2017.

[BGMR17] Damien Busatto-Gaston, Benjamin Monmege, and Pierre-Alain Reynier. Optimal reachability in divergent weighted timed games. In *Proceedings of the International Conference on the Foundations of Software Science and Computational Structures, FoSSaCS'17*, volume 10203. Springer-Verlag, 2017.

[BGMR18] Patricia Bouyer, Mauricio González, Nicolas Markey, and Mickael Randour. Multi-weighted Markov decision processes with reachability objectives. In *Proceedings of the International Symposium on Games, Automata, Logics, and Formal Verification, GandALF'18*, volume 277, 2018.

[BGR20] Raphaël Berthon, Shibashis Guha, and Jean-François Raskin. Mixing probabilistic and non-probabilistic objectives in Markov decision processes. In *Proceedings of the Annual IEEE Symposium on Logic in Computer Science, LICS'20*. ACM, 2020.

[BHM$^{+}$17] Patricia Bouyer, Piotr Hofman, Nicolas Markey, Mickael Randour, and Martin Zimmermann. Bounding average-energy games. In *Proceedings of the International Conference on the Foundations of Software Science and Computational Structures, FoSSaCS'17*, volume 10203, 2017.

[BHR16a] Véronique Bruyère, Quentin Hautem, and Mickael Randour. Window parity games: an alternative approach toward parity games with time bounds. In *Proceedings of the International Symposium on Games*,
Automata, Logics, and Formal Verification, GandALF'16, volume 226, 2016.

[BHR16b] Véronique Bruyère, Quentin Hautem, and Jean-François Raskin. On the complexity of heterogeneous multidimensional games. In Proceedings of the International Conference on Concurrency Theory, CONCUR'16, volume 59. Schloß Dagstuhl, 2016.

[BHRR19] Véronique Bruyère, Quentin Hautem, Mickael Randour, and Jean-François Raskin. Energy mean-payoff games. In Proceedings of the International Conference on Concurrency Theory, CONCUR'19, volume 140. Schloß Dagstuhl, 2019.

[BHSS12] Béatrice Bérard, Serge Haddad, Mathieu Sassolas, and Nathalie Sznad-jer. Concurrent games on VASS with inhibition. In Proceedings of the International Conference on Concurrency Theory, CONCUR'12, volume 7454. Springer-Verlag, 2012.

[Bil95] Patrick Billingsley. Probability and Measure. John Wiley & Sons, 1995.

[BJK10] Tomáš Brázdil, Petr Jančar, and Antonín Kučera. Reachability games on extended vector addition systems with states. In Proceedings of the International Colloquium on Automata, Languages and Programming, ICALP'10, volume 6199. Springer-Verlag, 2010.

[BJM15] Patricia Bouyer, Samy Jaziri, and Nicolas Markey. On the value problem in weighted timed games. In Proceedings of the International Conference on Concurrency Theory, CONCUR'15, volume 42. Schloß Dagstuhl, 2015.

[BJW02] Julien Bernet, David Janin, and Igor Walukiewicz. Permissive strategies: from parity games to safety games. Theoretical Informatics and Applications, 36, 2002.

[BK08] Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. MIT Press, 2008.

[BK14] James Brotherston and Max I. Kanovich. Undecidability of propositional separation logic and its neighbours. Journal of the ACM, 61, 2014.

[BKN16] Tomáš Brázdil, Antonín Kučera, and Petr Novotný. Optimizing the expected mean payoff in energy Markov decision processes. In Proceedings of the International Symposium on Automated Technology for Verification and Analysis, ATVA'16, volume 9938, 2016.

[BL69] J. Richard Büchi and Lawrence H. Landweber. Solving sequential conditions by finite-state strategies. Transactions of the American Mathematical Society, 138, 1969.
[BM83] Bernard Berthomieu and Miguel Menasche. An enumerative approach for analyzing time Petri nets. In *Proceedings of the IFIP World Computer Congress, WCC'83*. North-Holland/IFIP, 1983.

[BM16] Manuel Bodirsky and Marcello Mamino. Max-closed semilinear constraint satisfaction. In *Proceedings of the International Computer Science Symposium in Russia, CSR'16*, volume 9691. Springer-Verlag, 2016.

[BMR$^{+}$18] Patricia Bouyer, Nicolas Markey, Mickael Randour, Kim G. Larsen, and Simon Laursen. Average-energy games. *Acta Informatica*, 55, 2018.

[BMS14] Patricia Bouyer, Nicolas Markey, and Daniel Stan. Mixed Nash Equilibria in Concurrent Terminal-Reward Games. In *Proceedings of the International Conference on the Foundations of Software Technology and Theoretical Computer Science, FSTTCS'14*, 2014.

[BMS15] Patricia Bouyer, Nicolas Markey, and Ocan Sankur. Robust reachability in timed automata and games: A game-based approach. *Theoretical Computer Science*, 563, 2015.

[BORV21] Patricia Bouyer, Youssouf Oualhadj, Mickael Randour, and Pierre Vandenhove. Arena-independent finite-memory determinacy in stochastic games. In *Proceedings of the International Conference on Concurrency Theory, CONCUR'21*, volume 203. Schloß Dagstuhl, 2021.

[BR15] Romain Brenguier and Jean-François Raskin. Pareto curves of multidimensional mean-payoff games. In *Proceedings of the International Conference on Computer Aided Verification, CAV'15*, volume 9207. Springer-Verlag, 2015.

[Bra79] Gilles Brassard. A note on the complexity of cryptography (corresp.). *ieee Trans. Information Theory*, 25, 1979.

[Bre12] Romain Brenguier. Nash equilibria in concurrent games: applications to timed games. PhD thesis, École Normale Supérieure de Cachan - ENS Cachan, 2012.

[Bre16] Romain Brenguier. Robust equilibria in mean payoff games. In *Proceedings of the International Conference on the Foundations of Software Science and Computational Structures, FoSSaCS'16*, 2016.

[BRO$^{+}$22] Patricia Bouyer, Stéphane Le Roux, Youssouf Oualhadj, Mickael Randour, and Pierre Vandenhove. Games where you can play optimally with arena-independent finite memory. *Logical Methods in Computer Science*, 18, 2022.

[BRR17] Raphaël Berthon, Mickael Randour, and Jean-François Raskin. Threshold constraints with guarantees for parity objectives in Markov decision processes. In *Proceedings of the International Colloquium on Automata,*
*Languages and Programming, ICALP'17*, volume 80. Schloß Dagstuhl, 2017.

[BRS14] Romain Brenguier, Jean-François Raskin, and Mathieu Sassolas. The complexity of admissibility in omega-regular games. In *Proceedings of the Joint Meeting of the EACSL Annual Conference on Computer Science and Logic and the Annual IEEE Symposium on Logic in Computer Science, CSL-LICS'14*. ACM, 2014.

[BRV22] Patricia Bouyer, Mickael Randour, and Pierre Vandenhove. The true colors of memory: A tour of chromatic-memory strategies in zero-sum games on graphs (invited talk). In *Proceedings of the International Conference on the Foundations of Software Technology and Theoretical Computer Science, FSTTCS'22*, volume 250. Schloß Dagstuhl, 2022.

[BRV23] Patricia Bouyer, Mickael Randour, and Pierre Vandenhove. Characterizing omega-regularity through finite-memory determinacy of games on infinite graphs. *TheoretiCS*, 2, 2023.

[BSV03] Henrik Björklund, Sven Sandberg, and Sergei Vorobyov. A discrete subexponential algorithm for parity games. In *Proceedings of the International Symposium on Theoretical Aspects of Computer Science, STACS'03*, volume 2607. Springer-Verlag, 2003.

[BSV04] Henrik Björklund, Sven Sandberg, and Sergei Vorobyov. Memoryless determinacy of parity and mean payoff games: a simple proof. *Theoretical Computer Science*, 310, 2004.

[BSW03] Alexis-Julien Bouquet, Olivier Serre, and Igor Walukiewicz. Pushdown games with unboundedness and regular conditions. In *Proceedings of the International Conference on the Foundations of Software Technology and Theoretical Computer Science, FSTTCS'03*, volume 2914. Springer-Verlag, 2003.

[BT97] Dimitris Bertsimas and John N. Tsitsiklis. *Introduction to linear optimization*, volume 6. Athena Scientific, 1997.

[Büc62] J. Richard Büchi. On a decision method in restricted second-order arithmetic. In *Proceedings of the International Congress of Logic, Methodology, and Philosophy of Science, CLMPS'60*. Stanford University Press, 1962.

[Büc64] J. Richard Büchi. Regular canonical systems. *Archive for Mathematical Logic*, 6, 1964.

[Büc77] J. Richard Büchi. Using determinacy of games to eliminate quantifiers. In *Fundamentals of Computation Theory*77, 1977.
[BV07] Henrik Björklund and Sergei Vorobyov. A combinatorial strongly subexponen- tial strategy improvement algorithm for mean payoff games. *Dis- crete Applied Mathematics*, 155, 2007.

[BY04] Johan Bengtsson and Wang Yi. Timed automata: Semantics, algorithms and tools. In *Lectures on Concurrency and Petri Nets*, volume 2098. Springer-Verlag, 2004.

[Cac02] Thierry Cachat. Two-way tree automata solving pushdown games. In *Automata, Logics, and Infinite Games: A Guide to Current Research*. Springer Berlin Heidelberg, 2002.

[Cac03] Thierry Cachat. *Games on pushdown graphs and extensions*. PhD thesis, RWTH Aachen, 2003.

[Cau88] Didier Caucal. Récritures suffixes de mots. Technical report, INRIA, 1988.

[CD12] Krishnendu Chatterjee and Laurent Doyen. Energy parity games. *Theo- retical Computer Science*, 458, 2012.

[CDF+05] Franck Cassez, Alexandre David, Emmanuel Fleury, Kim G. Larsen, and Didier Lime. Efficient on-the-fly algorithms for the analysis of timed games. In *Proceedings of the International Conference on Concurrency Theory, CONCUR'05*, volume 3653. Springer-Verlag, 2005.

[CDF+19] Wojciech Czerwiński, Laure Daviaud, Nathanaël Fijalkow, Marcin Jur- dziński, Ranko Lazić, and Paweł Parys. Universal trees grow inside sep- arating automata: Quasip polynomial lower bounds for parity games. In *Proceedings of the Symposium on Discrete Algorithms, SODA'19*, 2019.

[CDH10a] Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. Qual- itative analysis of partially-observable markov decision processes. In *Proceedings of the International Symposium on Mathematical Founda- tions of Computer Science, MFCS'10*. Springer-Verlag, 2010.

[CDH10b] Julien Cristau, Alexandre David, and Florian Horn. How do we remem- ber the past in randomised strategies? In *Proceedings of the International Symposium on Games, Automata, Logics, and Formal Verification, GandALF'10*, volume 25, 2010.

[CDHR07] Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, and Jean- François Raskin. Algorithms for omega-regular games of incomplete information. *Logical Methods in Computer Science*, 3, 2007.

[CDHR10] Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, and Jean- François Raskin. Generalized mean payoff and energy games. In *Proceedings of the International Conference on the Foundations of Software Technology and Theoretical Computer Science, FSTTCS'10*, volume 8. Schloß Dagstuhl, 2010.
[CDL+07] Franck Cassez, Alexandre David, Kim G. Larsen, Didier Lime, and Jean-François Raskin. Timed control with observation based and stuttering invariant strategies. In *Proceedings of the International Symposium on Automated Technology for Verification and Analysis, ATVA'07*, volume 4762. Springer-Verlag, 2007.

[CDRR15] Krishnendu Chatterjee, Laurent Doyen, Mickael Randour, and Jean-François Raskin. Looking at mean payoff and total-payoff through windows. *Information and Computation*, 242, 2015.

[CDT02] Thierry Cachat, Jacques Duparc, and Wolfgang Thomas. Solving push-down games with a $\Sigma_3$ winning condition. In *Proceedings of the EACSL Annual Conference on Computer Science and Logic, CSL'02*, volume 2471. Springer-Verlag, 2002.

[CENR18] Krishnendu Chatterjee, Adrián Elgyütt, Petr Novotný, and Owen Rouillé. Expectation optimization with probabilistic guarantees in POMDPs with discounted-sum objectives. In *International Joint Conference on Artificial Intelligence* 18. ijcai.org, 2018.

[CF19] Thomas Colcombet and Nathanaël Fijalkow. Universal graphs and good for games automata: New tools for infinite duration games. In *Proceedings of the International Conference on the Foundations of Software Science and Computational Structures, FoSSaCS'19*, 2019.

[CFGO22] Thomas Colcombet, Nathanaël Fijalkow, Paweł Gawrychowski, and Pierre Ohlmann. The theory of universal graphs for infinite duration games. *Logical Methods in Computer Science*, 18, 2022.

[CH11] Krishnendu Chatterjee and Monika Henzinger. Faster and dynamic algorithms for maximal end-component decomposition and related graph problems in probabilistic verification. In *Proceedings of the Symposium on Discrete Algorithms, SODA'11*. Society for Industrial and Applied Mathematics, 2011.

[CH14] Arnaud Carayol and Matthew Hague. Saturation algorithms for model-checking pushdown systems. In *Proceedings of the International Conference on Automata and Formal Languages, AFL14*, volume 151, 2014.

[Cha13] Jakub Chaloupka. Z-reachability problem for games on 2-dimensional vector addition systems with states is in P. *Fundamenta Informatica*, 123, 2013.

[CHIJ17] Krishnendu Chatterjee, Thomas Dueholm Hansen, and Rasmus Ibsen-Jensen. Strategy complexity of concurrent safety games. In *Proceedings of the International Symposium on Mathematical Foundations of Computer Science, MFCS'17*, 2017.
[CHJ05] Krishnendu Chatterjee, Thomas A. Henzinger, and Marcin Jurdziński. Mean-payoff parity games. In *Proceedings of the Annual IEEE Symposium on Logic in Computer Science, LICS'05*. IEEE Computer Society, 2005.

[CHP08] Krishnendu Chatterjee, Thomas A. Henzinger, and Vinayak S. Prabhu. Trading infinite memory for uniform randomness in timed games. In *Proceedings of the International Conference on Hybrid Systems: Computation and Control, HSCC'08*, volume 4981. Springer-Verlag, 2008.

[CHP10] Krishnendu Chatterjee, Thomas A. Henzinger, and Nir Piterman. Strategy logic. *Information and Computation*, 208, 2010.

[Chu57] Alonzo Church. Applications of recursive arithmetic to the problem of circuit synthesis. In *Summaries of the Summer Institute of Symbolic Logic*, volume I. Cornell University, 1957.

[Chu62] Alonzo Church. Logic, arithmetic, and automata. In *Proceedings of the International Congress of Mathematicians, ICM'62*, 1962.

[CIJ15] Krishnendu Chatterjee and Rasmus Ibsen-Jensen. The value 1 problem under finite-memory strategies for concurrent mean payoff games. In *Proceedings of the Symposium on Discrete Algorithms, SODA'15*. Society for Industrial and Applied Mathematics, 2015.

[CJK+17] Cristian S. Calude, Sanjay Jain, Bakhadyr Khoussainov, Wei Li, and Frank Stephan. Deciding parity games in quasip polynomial time. In *Proceedings of the Annual ACM Symposium on Theory of Computing, STOC'17*, 2017.

[CJL+09] Franck Cassez, Jan J. Jensen, Kim G. Larsen, Jean-François Raskin, and Pierre-Alain Reynier. Automatic synthesis of robust and optimal controllers – an industrial case study. In *Proceedings of the International Conference on Hybrid Systems: Computation and Control, HSCC'09*, volume 5469. Springer-Verlag, 2009.

[CJLS17] Thomas Colcombet, Marcin Jurdziński, Ranko Lazić, and Sylvain Schmitz. Perfect half-space games. In *Proceedings of the Annual IEEE Symposium on Logic in Computer Science, LICS'17*. IEEE Computer Society, 2017.

[CKK17] Krishnendu Chatterjee, Zuzana Kretínská, and Jan Kretínský. Unifying two views on multiple mean-payoff objectives in Markov decision processes. *Logical Methods in Computer Science*, 13, 2017.

[CLL+19] Wojciech Czerwiński, Sławomir Lasota, Ranko Lazić, Jérôme Leroux, and Filip Mazowiecki. The reachability problem for Petri nets is not elementary. In *Proceedings of the Annual ACM Symposium on Theory of Computing, STOC'19*. ACM Press, 2019.
[CLRS09] Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. *Introduction to Algorithms, Third Edition*. MIT Press, 2009.

[Con92] Anne Condon. The complexity of stochastic games. *Information and Computation*, 96, 1992.

[CR15] Lorenzo Clemente and Jean-François Raskin. Multidimensional beyond worst-case and almost-sure problems for mean-payoff objectives. In *Proceedings of the Annual IEEE Symposium on Logic in Computer Science, LICS'15*. IEEE Computer Society, 2015.

[CR17] Carlo Comin and Romeo Rizzi. Improved pseudo-polynomial bound for the value problem and optimal strategy synthesis in mean payoff games. *Algorithmica*, 77, 2017.

[CRR14] Krishnendu Chatterjee, Mickael Randour, and Jean-François Raskin. Strategy synthesis for multi-dimensional quantitative objectives. *Acta Informatica*, 51, 2014.

[CS14] Jean-Baptiste Courtois and Sylvain Schmitz. Alternating vector addition systems with states. In *Proceedings of the International Symposium on Mathematical Foundations of Computer Science, MFCS'14*, volume 8634. Springer-Verlag, 2014.

[CS21] Arnaud Carayol and Olivier Serre. Higher-order recursion schemes and their automata models. In *Handbook of Automata Theory*. European Mathematical Society Publishing House, Zürich, Switzerland, 2021.

[dA97] Luca de Alfaro. *Formal Verification of Probabilistic Systems*. PhD thesis, Stanford University, 1997.

[dAFH+03] Luca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar, and Mariëlle Stoelinga. The element of surprise in timed games. In *Proceedings of the International Conference on Concurrency Theory, CONCUR'03*, volume 2761. Springer-Verlag, 2003.

[dAH00] Luca de Alfaro and Thomas A. Henzinger. Concurrent ω-regular games. In *Proceedings of the Annual IEEE Symposium on Logic in Computer Science, LICS'00*. IEEE Computer Society, 2000.

[dAHK98] Luca de Alfaro, Thomas A. Henzinger, and Orna Kupferman. Concurrent reachability games. In *Proceedings of the Annual Symposium on Foundations of Computer Science, FOCS'98*. IEEE Computer Society, 1998.

[Dan65] George B. Dantzig. *Linear programming and extensions*. Princeton University Press, 1965.

[DGP09] Constantinos Daskalakis, Paul Goldberg, and Christos H. Papadimitriou. The complexity of computing a Nash equilibrium. *SIAM Journal on Computing*, 39, 2009.
[Dic13] Leonard Eugene Dickson. Finiteness of the odd perfect and primitive abundant numbers with *n* distinct prime factors. *American Journal of Mathematics*, 35, 1913.

[Dil90] David L. Dill. Timing assumptions and verification of finite-state concurrent systems. In *Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems*, AVMFSS'89, volume 407. Springer-Verlag, 1990.

[DJL+14] Alexandre David, Jan J. Jensen, Kim G. Larsen, Axel Legay, Didier Lime, Mathias Grund Sørensen, and Jakob Haahr Taankvist. On time with minimal expected cost! In *Proceedings of the International Symposium on Automated Technology for Verification and Analysis, ATVA'14*, volume 8837. Springer-Verlag, 2014.

[DJL+15] Alexandre David, Jan J. Jensen, Kim G. Larsen, Marius Mikučionis, and Jakob Haahr Taankvist. Uppaal stratego. In *Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS'15*, volume 9035. Springer-Verlag, 2015.

[DJL18] Laure Daviaud, Marcin Jurdziński, and Ranko Lazić. A pseudo-quasi-polynomial algorithm for mean payoff parity games. In *Proceedings of the Annual IEEE Symposium on Logic in Computer Science, LICS'18*. ACM Press, 2018.

[DJLL12] Stéphane Demri, Marcin Jurdziński, Oded Lachish, and Ranko Lazić. The covering and boundedness problems for branching vector addition systems. *Journal of Computer and System Sciences*, 79, 2012.

[DJW97] Stefan Dziembowski, Marcin Jurdziński, and Igor Walukiewicz. How much memory is needed to win infinite games? In *Proceedings of the Annual IEEE Symposium on Logic in Computer Science, LICS'97*. IEEE Computer Society, 1997.

[DKQR20] Florent Delgrange, Joost-Pieter Katoen, Tim Quatmann, and Mickael Randour. Simple strategies in multi-objective MDPs. In *Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS'20*, volume 12078. Springer, 2020.

[Ehr61] Andrzej Ehrenfeucht. An application of games to the completeness problem for formalized theories. *Comptes-rendus de l'Académie des Sciences*, 49, 1961.

[EJ88] E. Allen Emerson and Charanjit S. Jutla. The complexity of tree automata and logics of programs. In *Proceedings of the Annual Symposium on Foundations of Computer Science, FOCS'88*. IEEE Computer Society, 1988.
[EJ91] E. Allen Emerson and Charanjit S. Jutla. Tree automata, μ-calculus and determinacy. In *Proceedings of the Annual Symposium on Foundations of Computer Science, FOCS'91*. IEEE Computer Society, 1991.

[EJS93] E. Allen Emerson, Charanjit S. Jutla, and A. Prasad Sistla. On model-checking for fragments of μ-calculus. In *Proceedings of the International Conference on Computer Aided Verification, CAV'93*, volume 697. Springer-Verlag, 1993.

[EKVY08] Kousha Etessami, Marta Z. Kwiatkowska, Moshe Y. Vardi, and Mihalis Yannakakis. Multi-objective model checking of Markov decision processes. *Logical Methods in Computer Science*, 4, 2008.

[EM79] Andrzej Ehrenfeucht and Jan Mycielski. Positional strategies for mean payoff games. *International Journal of Game Theory*, 8, 1979.

[EMP10] Rüdiger Ehlers, Robert Mattmüller, and Hans-Jörg Peter. Combining symbolic representations for solving timed games. In *Proceedings of the International Conference on Formal Modelling and Analysis of Timed Systems, FORMATS'10*, volume 6246. Springer-Verlag, 2010.

[Esp98] Javier Esparza. Decidability and complexity of Petri net problems — an introduction. In *Lectures on Petri Nets I: Basic Models*, volume 1491. Springer-Verlag, 1998.

[Eve57] H. Everett. Recursive games. In *Contributions to the Theory of Games III*, volume 39. Princeton University Press, 1957.

[EY10] Kousha Etessami and Mihalis Yannakakis. On the complexity of Nash equilibria and other fixed points. *SIAM Journal on Computing*, 39, 2010.

[Fea10a] John Fearnley. Exponential lower bounds for policy iteration. In *Proceedings of the International Colloquium on Automata, Languages and Programming, ICALP'10*. Springer-Verlag, 2010.

[Fea10b] John Fearnley. *Strategy Iteration Algorithms for Games and Markov Decision Processes*. PhD thesis, University of Warwick, 2010.

[Fea17] John Fearnley. Efficient parallel strategy improvement for parity games. In *Proceedings of the International Conference on Computer Aided Verification, CAV'17*, 2017.

[FF03] Chris Ferguson and Chris Ferguson. On the borel and von neumann poker models. *Game Theory and Applications*, 9, 2003.

[FGMS20] John Fearnley, Spencer Gordon, Ruta Mehta, and Rahul Savani. Unique end of potential line. *Journal of Computer and System Sciences*, 114, 2020.

[Fij18] Nathanaël Fijalkow. An optimal value iteration algorithm for parity games. *CoRR*, abs/1801.09618, 2018.
[FJLS11] Uli Fahrenberg, Line Juhl, Kim G. Larsen, and Jiří Srba. Energy games in multiweighted automata. In *Proceedings of the International Colloquium on Theoretical Aspects of Computing, ICTAC'11*, volume 6916. Springer-Verlag, 2011.

[FJS$^{+}$17] John Fearnley, Sanjay Jain, Sven Schewe, Frank Stephan, and Dominik Wojtczak. An ordered approach to solving parity games in quasipoly- nomial time and quasilinear space. In *Proceedings of the International SPIN Workshop on Model Checking of Software, SPIN'17*, 2017.

[FKP12] Vojtech Forejt, Marta Z. Kwiatkowska, and David Parker. Pareto curves for probabilistic model checking. In *Proceedings of the International Symposium on Automated Technology for Verification and Analysis, ATVA'12*, volume 7561. Springer, 2012.

[FM13] Søren Kristoffer Stiil Frederiksen and Peter Bro Miltersen. Approximat- ing the value of a concurrent reachability game in the polynomial time hierarchy. In *Proceedings of the International Symposium on Algorithms and Computation, ISAAC*, 2013.

[FMR68] Patrick C. Fischer, Albert R. Meyer, and Dinah Rosenberg. Counter ma- chines and counter languages. *Mathematical Systems Theory*, 2, 1968.

[FNS07] Tomas Feder, Hamid Nazerzadeh, and Amin Saberi. Approximating Nash equilibria using small-support strategies. In *Proceedings of the ACM conference on Electronic Commerce, EC'07*. ACM Press, 2007.

[Fra50] Roland Fraïssé. Sur une nouvelle classification des systèmes de relations. In *Comptes Rendus de l'Académie des Sciences*, volume 230, 1950.

[Fra53] Roland Fraïssé. Sur quelques classifications des systèmes de relations. In *Publications Scientifiques de l'Université d'Alger*, 1953.

[Fri11] Oliver Friedmann. An exponential lower bound for the latest determinis- tic strategy iteration algorithms. *Logical Methods in Computer Science*, 7, 2011.

[FS01] Alain Finkel and PhPhilippe Schnoebelen. Well-structured transition sys- tems everywhere! *Theoretical Computer Science*, 256, 2001.

[FV96] Jerzy Filar and Koos Vrieze. *Competitive Markov Decision Processes*. Springer-Verlag, 1996.

[FWW97] Alain Finkel, Bernard Willems, and Pierre Wolper. A direct symbolic ap- proach to model checking pushdown systems. *Electronic Notes in Theo- retical Computer Science*, 9, 1997.

[Gal58] Tibor Gallai. Maximum-minimum sätze über graphen. *Acta Mathematica Academiae Scientiarum Hungaricae*, 9, 1958.
[Gar07] David J. H. Garling. *Inequalities: A Journey Into Linear Analysis*. Cambridge University Press, 2007.

[GH82] Yuri Gurevich and Leo Harrington. Trees, automata, and games. In *Proceedings of the Annual ACM Symposium on Theory of Computing, STOC'82*. ACM Press, 1982.

[GH08] Hugo Gimbert and Florian Horn. Simple stochastic games with few random vertices are easy to solve. In *Proceedings of the International Conference on the Foundations of Software Science and Computational Structures, FoSSaCS'08*, volume 4962. Springer-Verlag, 2008.

[Gil57] Dean Gillette. Stochastic games with zero stop probability. In *Contributions to the Theory of Games III*, volume 39. Princeton University Press, 1957.

[Gim04] Hugo Gimbert. Parity and exploration games on infinite graphs. In *Proceedings of the EACSL Annual Conference on Computer Science and Logic, CSL'04*, volume 3210. Springer-Verlag, 2004.

[GKK88] Vladimir A. Gurvich, Alexander V. Karzanov, and Leonid G. Khachiyan. Cyclic games and an algorithm to find minimax cycle means in directed graphs. *USSR Computational Mathematics and Mathematical Physics*, 28, 1988.

[GMMW22] Hugo Gimbert, Corto Mascle, Anca Muscholl, and Igor Walukiewicz. Distributed controller synthesis for deadlock avoidance. In *Proceedings of the International Colloquium on Automata, Languages and Programming, ICALP'22*, volume 229. Schloß Dagstuhl, 2022.

[Gon92] Clovis C. Gonzaga. Path-following methods for linear programming. *SIAM Review*, 34, 1992.

[Grä02] Erich Grädel. Model checking games. *Electronic Notes in Theoretical Computer Science*, 67, 2002.

[Gre78] Sheila A. Greibach. Remarks on blind and partially blind one-way multicounter machines. *Theoretical Computer Science*, 7, 1978.

[GS53] David Gale and F.M. Stewart. Infinite games with perfect information. *Annals of Mathematical Studies*, 28, 1953.

[GS09a] Thomas Martin Gawlitza and Helmut Seidl. Games through nested fix-points. In *Proceedings of the International Conference on Computer Aided Verification, CAV'09*, volume 5643. Springer-Verlag, 2009.

[GS09b] Vincent Gripon and Olivier Serre. Qualitative concurrent stochastic games with imperfect information. In *Proceedings of the International Colloquium on Automata, Languages and Programming, ICALP'09*, volume 5556. Springer, 2009.
[GTW02] Erich Grädel, Wolfgang Thomas, and Thomas Wilke. *Automata, Logics, and Infinite Games: A Guide to Current Research (outcome of a Dagstuhl seminar, February 2001)*, volume 2500. Springer-Verlag, 2002.

[GVF+18] Giuseppe De Giacomo, Moshe Y. Vardi, Paolo Felli, Natasha Alechina, and Brian Logan. Synthesis of orchestrations of transducers for manufacturing. In *Proceedings of the AAAI Conference on Artificial Intelligence, AAAI'18*. AAAI Publications, 2018.

[GZ04] Hugo Gimbert and Wiesław Zielonka. When can you play positionally? In *Proceedings of the International Symposium on Mathematical Foundations of Computer Science, MFCS'04*, volume 3153. Springer-Verlag, 2004.

[GZ05] Hugo Gimbert and Wiesław Zielonka. Games where you can play optimally without any memory. In *Proceedings of the International Conference on Concurrency Theory, CONCUR'05*, volume 3653. Springer-Verlag, 2005.

[Hab97] Peter Habermehl. On the complexity of the linear-time $\mu$-calculus for Petri nets. In *Proceedings of the International Conference on Application and Theory of Petri Nets, Petri nets'97*, volume 1248. Springer-Verlag, 1997.

[Hal07] Nir Halman. Simple stochastic games, parity games, mean payoff games and discounted payoff games are all LP-type problems. *Algorithmica*, 49, 2007.

[Hau14] Felix Hausdorff. Grundzüge der Mengenlehre. *Leipzig*, 1914.

[HD05] Paul Hunter and Anuj Dawar. Complexity bounds for regular games. In *Proceedings of the International Symposium on Mathematical Foundations of Computer Science, MFCS'05*, volume 3618. Springer-Verlag, 2005.

[HDJ12] Romain Hollanders, Jean-Charles Delvenne, and Raphaël M. Jungers. The complexity of policy iteration is exponential for discounted Markov decision processes. In *Proceedings of the IEEE Conference on Decision and Control, CDC'12*. IEEE Computer Society, 2012.

[HIJK16] Thomas Dueholm Hansen, Rasmus Ibsen-Jensen, and Michal Koucký. The big match in small space. In *Algorithmic Game Theory*, 2016.

[HIJN18] Thomas Dueholm Hansen, Rasmus Ibsen-Jensen, and Abraham Neyman. The big match with a clock and a bit of memory. In *Proceedings of the ACM conference on Electronic Commerce, EC'18*, 2018.

[HIJPT13] Thomas Dueholm Hansen, Rasmus Ibsen-Jensen, Vladimir V. Podolskii, and Elias Tsigaridas. Patience of matrix games. *Discrete Applied Mathematics*, 2013.
[HK15] Christoph Haase and Stefan Kiefer. The odds of staying on budget. In *Proceedings of the International Colloquium on Automata, Languages and Programming, ICALP'15*, volume 9135. Springer, 2015.

[HKL$^{+}$11] Thomas Dueholm Hansen, Michal Koucký, Niels Lauritzen, Peter Bro Miltersen, and Elias Tsigaridas. Exact algorithms for solving stochastic games: Extended abstract. In *Proceedings of the Annual ACM Symposium on Theory of Computing, STOC'11*, 2011.

[HKM09] Thomas Dueholm Hansen, Michal Koucký, and Peter Bro Miltersen. Winning concurrent reachability games requires doubly-exponential patience. In *Proceedings of the Annual IEEE Symposium on Logic in Computer Science, LICS'09*, 2009.

[HMZ13] Thomas Dueholm Hansen, Peter Bro Miltersen, and Uri Zwick. Strategy iteration is strongly polynomial for 2-player turn-based stochastic games with a constant discount factor. *Journal of the ACM*, 60, 2013.

[HO09] Matthew Hague and C.-H. Luke Ong. Winning regions of pushdown parity games: A saturation method. In *Proceedings of the International Conference on Concurrency Theory, CONCUR'09*, 2009.

[Hod93] Wilfrid Hodges. *Model theory*, volume 42. Cambridge University Press, 1993.

[Hor08] Florian Horn. Explicit muller games are PTIME. In *Proceedings of the International Conference on the Foundations of Software Technology and Theoretical Computer Science, FSTTCS'08*, volume 2. Schloß Dagstuhl, 2008.

[HP79] John E. Hopcroft and Jean-Jacques Panivot. On the reachability problem for 5-dimensional vector addition systems. *Theoretical Computer Science*, 8, 1979.

[HPRV76] C. J. Himmelberg, T. Parthasarathy, T. E. S. Raghavan, and F. S. Van Vleck. Existence of *p*-equilibrium and optimal stationary strategies in stochastic games. *Transactions of the American Mathematical Society*, 1976.

[Hun15] Paul Hunter. Reachability in succinct one-counter games. In *Proceedings of the International Workshop on Reachability Problems, RP'15*, volume 9328. Springer-Verlag, 2015.

[IJ12] Rasmus Ibsen-Jensen. *Strategy complexity of two-player, zero-sum games*. PhD thesis, Aarhus University, 2012.

[IJM12] Rasmus Ibsen-Jensen and Peter Bro Miltersen. Solving simple stochastic games with few coin toss positions. In *Proceedings of the European Symposium on Algorithms, ESA'12*, volume 7501. Springer-Verlag, 2012.
[Jan15] Petr Jančar. On reachability-related games on vector addition systems with states. In *Proceedings of the International Workshop on Reachability Problems, RP'15*, volume 9328. Springer-Verlag, 2015.

[JL17] Marcin Jurdziński and Ranko Lazić. Succinct progress measures for solving parity games. In *Proceedings of the Annual IEEE Symposium on Logic in Computer Science, LICS'17*, 2017.

[JLS08] Marcin Jurdziński, François Laroussinie, and Jeremy Sproston. Model checking probabilistic timed automata with one or two clocks. *Logical Methods in Computer Science*, 4, 2008.

[JLS15] Marcin Jurdziński, Ranko Lazić, and Sylvain Schmitz. Fixed-dimensional energy games are in pseudo-polynomial time. In *Proceedings of the International Colloquium on Automata, Languages and Programming, ICALP'15*, volume 9135. Springer-Verlag, 2015.

[JLSØ13] Jan J. Jensen, Kim G. Larsen, Jiří Srba, and Lars Kærlund Østergaard. Local model checking of weighted CTL with upper-bound constraints. In *Proceedings of the International SPIN Workshop on Model Checking of Software, SPIN'13*, volume 7976. Springer-Verlag, 2013.

[JMT22] Marcin Jurdziński, Rémi Morvan, and K. S. Thejaswini. Universal algorithms for parity games and nested fixpoints. In *Principles of Systems Design - Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday*, volume 13660. Springer-Verlag, 2022.

[JOS18] Petr Jančar, Petr Osička, and Zdeněk Sawa. EXPSPACE-complete variant of countdown games, and simulation on succinct one-counter nets. In *Proceedings of the International Workshop on Reachability Problems, RP'18*, volume 11123. Springer-Verlag, 2018.

[JPZ08] Marcin Jurdziński, Mike Paterson, and Uri Zwick. A deterministic subexponential algorithm for solving parity games. *SIAM Journal on Computing*, 38, 2008.

[Jur00] Marcin Jurdziński. Small progress measures for solving parity games. In *Proceedings of the International Symposium on Theoretical Aspects of Computer Science, STACS'00*, 2000.

[Kan95] Max I. Kanovich. Petri nets, Horn programs, linear logic and vector games. *Annals of Pure and Applied Logic*, 75, 1995.

[Kan16] Max I. Kanovich. The undecidability theorem for the Horn-like fragment of linear logic (revisited). *Mathematical Structures in Computer Science*, 26, 2016.

[Kar78] Richard M. Karp. A characterization of the minimum cycle mean in a digraph. *Discrete Mathematics*, 23, 1978.
[Kar84] Narendra Karmarkar. A new polynomial-time algorithm for linear programming. *combinatorica*, 4, 1984.

[KBB+08] Leonid G. Khachiyan, Endre Boros, Konrad Borys, Khaled Elbassioni, Vladimir A. Gurvich, Gabor Rudolf, and Jihui Zhao. On short paths interdiction problems: Total and node-wise limited interdiction. *Theory of Computing Systems*, 43, 2008.

[Kha79] Leonid G. Khachiyan. A polynomial algorithm in linear programming. *Soviet Mathematics Doklady*, 20, 1979.

[Kie13] Stefan Kiefer. BPA bisimilarity is EXPTIME-hard. *Information Processing Letters*, 113, 2013.

[KL22] Zhuan Khye Koh and Georg Loho. Beyond value iteration for parity games: Strategy iteration with universal trees. In *Proceedings of the International Symposium on Mathematical Foundations of Computer Science*, MFCS'22, volume 241. Schloß Dagstuhl, 2022.

[KM03] Stephen Kwek and Kurt Mehlhorn. Optimal search for rationals. *Information Processing Letters*, 86, 2003.

[KMvS94] Daphne Koller, Nimrod Megiddo, and Bernhard von Stengel. Fast algorithms for finding randomized strategies in game trees. In *Proceedings of the Annual ACM Symposium on Theory of Computing, STOC'94*. ACM Press, 1994.

[Koh74] Elon Kohlberg. Repeated games with absorbing states. *Annals of Mathematical Statistics*, 1974.

[Kön36] Dénes König. *Theorie der endlichen und unendlichen Graphen*. Akademische Verlagsgesellschaft Leipzig, 1936.

[Kop06] Eryk Kopczyński. Half-positional determinacy of infinite games. In *Proceedings of the International Colloquium on Automata, Languages and Programming, ICALP'06*, volume 4052. Springer-Verlag, 2006.

[Kop08] Eryk Kopczyński. *Half-positional Determinacy of Infinite Games*. PhD thesis, University of Warsaw, 2008.

[Kos82] S. Rao Kosaraju. Decidability of reachability in vector addition systems. In *Proceedings of the Annual ACM Symposium on Theory of Computing, STOC'82*. ACM Press, 1982.

[Koz21] Alexander Kozachinskiy. Continuous positional payoffs. In *Proceedings of the International Conference on Concurrency Theory, CONCUR'21*, volume 203. Schloß Dagstuhl, 2021.
[KPR18] Jan Kretínský, Guillermo A. Pérez, and Jean-François Raskin. Learning-based mean-payoff optimization in an unknown MDP under omega-regular constraints. In *Proceedings of the International Conference on Concurrency Theory, CONCUR'18*, volume 118. Schloß Dagstuhl, 2018.

[Kru72] Joseph B. Kruskal. The theory of well-quasi-ordering: A frequently discovered concept. *Journal of Combinatorial Theory, Series A*, 13, 1972.

[KS76] John G. Kemeny and J. Laurie Snell. *Finite Markov Chains*. Springer-Verlag, 1976.

[KS88] S. Rao Kosaraju and Gregory Sullivan. Detecting cycles in dynamic graphs in polynomial time. In *Proceedings of the Annual ACM Symposium on Theory of Computing, STOC'88*. ACM Press, 1988.

[Kuč11] Antonín Kučera. Turn-based stochastic games. In *Lectures in Game Theory for Computer Scientists*. Cambridge University Press, 2011.

[KV00] Orna Kupferman and Moshe Y. Vardi. An automata-theoretic approach to reasoning about infinite-state systems. In *Proceedings of the International Conference on Computer Aided Verification, CAV'00*, volume 1855. Springer, 2000.

[Lad75] Richard E. Ladner. The Circuit Value Problem is Log Space Complete for PTIME. *SIGACT News*, 7, 1975.

[Lam92] Jean-Luc Lambert. A structure to decide reachability in Petri nets. *Theoretical Computer Science*, 99, 1992.

[Lan67] Lawrence H. Landweber. Finite state games—a solvability algorithm for restricted second-order arithmetic. *Notices of the American Mathematical Society*, 14, 1967.

[Leh18] Karoliina Lehtinen. A modal-μ perspective on solving parity games in quasi-polynomial time. In *Proceedings of the Annual IEEE Symposium on Logic in Computer Science, LICS'18*, 2018.

[Ler11] Jérôme Leroux. Vector addition system reachability problem: a short self-contained proof. In *Proceedings of the Annual ACM Symposium on Principles of Programming Languages, POPL'11*. ACM Press, 2011.

[Lip76] Richard J. Lipton. The reachability problem requires exponential space. Technical report, Yale University, 1976.

[LL69] Thomas M. Liggett and Steven A Lippman. Stochastic games with perfect information and time average payoff. *SIAM Review*, 11, 1969.

[LLTW14] Kim G. Larsen, Axel Legay, Louis-Marie Traonouez, and Andrzej Wąsoski. Robust synthesis for real-time systems. *Theoretical Computer Science*, 515, 2014.
[LMSS92] Patrick Lincoln, John Mitchell, Andre Scedrov, and Narayan Shankar. Decision problems for propositional linear logic. *Annals of Pure and Applied Logic*, 56, 1992.

[LP07] Yuri M. Lifshits and Dmitri S. Pavlov. Potential theory for mean payoff games. *Journal of Mathematical Sciences*, 145, 2007.

[LPSW22] Karoliina Lehtinen, Paweł Parys, Sven Schewe, and Dominik Wojtczak. A recursive approach to solving parity games in quasip polynomial time. *Logical Methods in Computer Science*, 18, 2022.

[LS98] Xinxin Liu and Scott A. Smolka. Simple linear-time algorithms for minimal fixed points. In *Proceedings of the International Colloquium on Automata, Languages and Programming, ICALP'98*, volume 1443. Springer-Verlag, 1998.

[LS19] Ranko Lazić and Sylvain Schmitz. The ideal view on Rackoff's coverability technique. *Information and Computation*, 2019.

[LWG13] Dominique Larchey-Wendling and Didier Galmiche. Nondeterministic phase semantics and the undecidability of Boolean BI. *ACM Transactions on Computational Logic*, 14, 2013.

[LY94] Richard J. Lipton and Neal E. Young. Simple strategies for large zero-sum games with applications to complexity theory. In *Proceedings of the Annual ACM Symposium on Theory of Computing, STOC'94*. ACM Press, 1994.

[Mar75] George R.R. Martin. Borel determinacy. *Annals of Mathematics*, 102, 1975.

[Mat07] Jiří Matoušek. *Understanding and Using Linear Programming*. Springer-Verlag, 2007.

[May81] Richard Mayr. An algorithm for the general Petri net reachability problem. In *Proceedings of the Annual ACM Symposium on Theory of Computing, STOC'81*. ACM Press, 1981.

[McN65] Robert McNaughton. Finite-state infinite games. Technical report, Massachusetts Institute of Technology, 1965.

[McN66] Robert McNaughton. Testing and generating infinite sequences by a finite automaton. *Information and Computation*, 9, 1966.

[McN93] Robert McNaughton. Infinite games played on finite graphs. *Annals of Pure and Applied Logic*, 65, 1993.

[Min67] Marvin L. Minsky. *Computation: finite and infinite machines*. Prentice-Hall, 1967.
[MMPV12] Fabio Mogavero, Aniello Murano, Giuseppe Perelli, and Moshe Y. Vardi. What makes ATL* decidable? a decidable fragment of strategy logic. In *Proceedings of the International Conference on Concurrency Theory, CONCUR'12*, 2012.

[MN81] Jean-François Mertens and Abraham Neyman. Stochastic games. *International Journal of Game Theory*, 10, 1981.

[Mos84] Andrzej W. Mostowski. Regular expressions for infinite trees and a standard form of automata. In *Computation Theory*, 1984.

[Mos91] Andrzej W. Mostowski. Games with forbidden positions. Technical report, University of Gdansk, 1991.

[MPS95] Oded Maler, Amir Pnueli, and Joseph Sifakis. On the synthesis of discrete controllers for timed systems (an extended abstract). In *Proceedings of the International Symposium on Theoretical Aspects of Computer Science, STACS'95*, volume 900. Springer-Verlag, 1995.

[MR22] James C. A. Main and Mickael Randour. Different strokes in randomised strategies: Revisiting Kuhn's theorem under finite-memory assumptions. In *Proceedings of the International Conference on Concurrency Theory, CONCUR'22*, volume 243. Schloß Dagstuhl, 2022.

[MRS21] James C. A. Main, Mickael Randour, and Jeremy Sproston. Time flies when looking out of the window: Timed games with window parity objectives. In *Proceedings of the International Conference on Concurrency Theory, CONCUR'21*, volume 203. Schloß Dagstuhl, 2021.

[MS98] Ashok P. Maitra and William D. Sudderth. Finitely additive stochastic games with borel measurable payoffs. *International Journal of Game Theory*, 27, 1998.

[Mul63] David E. Muller. Infinite sequences and finite machines. In *Proceedings of the Fourth Annual Symposium on Switching Circuit Theory and Logical Design*. IEEE Computer Society, 1963.

[MW03] Allen B. MacKenzie and Stephen B. Wicker. Stability of multipacket slotted aloha with selfish users and perfect information. In *INFOCOM 2003. Twenty-Second Annual Joint Conference of the IEEE Computer and Communications. IEEE Societies*, volume 3, 2003.

[Nas50] John F. Nash. Equilibrium points in n-person games. *Proceedings of the national academy of sciences*, 36, 1950.

[Nor98] J.R. Norris. *Markov Chains*, volume 2. Cambridge University Press, 1998.

[Nov15] Petr Novotný. *Controller Synthesis for Resource-Aware Systems*. PhD thesis, Masaryk University, 2015.
[NPR16] Reino Niskanen, Igor Potapov, and Julien Reichert. Undecidability of two-dimensional robot games. In *Proceedings of the International Symposium on Mathematical Foundations of Computer Science*, MFCS'16, volume 58. Schloß Dagstuhl, 2016.

[Ohl21] Pierre Ohlmann. *Monotonic graphs for parity and mean-payoff games*. (Graphes monotones pour jeux de parité et à paiement moyen). PhD thesis, Université Paris Cité, 2021.

[Ohl22] Pierre Ohlmann. The GKK algorithm is the fastest over simple mean-payoff games. In *Proceedings of the International Computer Science Symposium in Russia*, CSR'22, volume 13296. Springer, 2022.

[Ohl23] Pierre Ohlmann. Characterizing positionality in games of infinite duration over infinite graphs. *TheoretiCS*, 2, 2023.

[ORS14] Youssouf Oualhadj, Pierre-Alain Reynier, and Ocan Sankur. Probabilistic robust timed games. In *Proceedings of the International Conference on Concurrency Theory, CONCUR'14*, volume 8704. Springer-Verlag, 2014.

[Par73] T. Parthasarathy. Discounted, positive, and non-cooperative stochastic games. *International Journal of Game Theory*, 1973.

[Par19] Paweł Parys. Parity games: Zielonka's algorithm in quasi-polynomial time. In *Proceedings of the International Symposium on Mathematical Foundations of Computer Science*, MFCS'19, 2019.

[Par20] Paweł Parys. Parity games: Another view on lehtinen's algorithm. In *Proceedings of the EACSL Annual Conference on Computer Science and Logic*, CSL'20, 2020.

[PEM11] Hans-Jörg Peter, Rüdiger Ehlers, and Robert Mattmüller. Synthia: Verification and synthesis for timed automata. In *Proceedings of the International Conference on Computer Aided Verification, CAV'11*, volume 6806. Springer-Verlag, 2011.

[Pet62] Carl Adam Petri. *Kommunikation mit Automaten*. PhD thesis, Universität Bonn, 1962.

[Pin21] Jean-Éric Pin. *Handbook of Automata Theory*. European Mathematical Society Publishing House, Zürich, Switzerland, 2021.

[PR90] Amir Pnueli and Roni Rosner. Distributed reactive systems are hard to synthesize. In *Proceedings of the Annual Symposium on Foundations of Computer Science*, FOCS'31, 1990.

[Pur95] Anuj Puri. *Theory of Hybrid Systems and Discrete Event Systems*. PhD thesis, University of California at Berkeley, 1995.
[Put05] Martin L. Puterman. *Markov Decision Processes: Discrete Stochastic Dynamic Programming*. John Wiley & Sons, 2005.

[Rab69a] Michael O. Rabin. Automata on infinite objects and Church's problem. *Transactions of the American Mathematical Society*, 141, 1969.

[Rab69b] Michael O. Rabin. Decidability of second-order theories and automata on infinite trees. *Transactions of the American Mathematical Society*, 141, 1969.

[Rac78] Charles Rackoff. The covering and boundedness problems for vector addition systems. *Theoretical Computer Science*, 6, 1978.

[Ran14] Mickael Randour. *Synthesis in Multi-Criteria Quantitative Games*. PhD thesis, UMONS – Université de Mons, 2014.

[Rei84] John H. Reif. The complexity of two-player games of incomplete information. *Journal of Computer and System Sciences*, 29, 1984.

[Ren09] Jérôme Renault. Repeated games with incomplete information. In *Encyclopaedia of Complexity and Systems Science*. Springer, 2009.

[Ros06] Jeffrey S. Rosenthal. *A First Look at Rigorous Probability Theory*. World Scientific Publishing, 2006.

[RP18] Stéphane Le Roux and Arno Pauly. Extending finite-memory determinacy to multi-player games. *Information and Computation*, 2018.

[RPR18] Stéphane Le Roux, Arno Pauly, and Mickael Randour. Extending finite-memory determinacy by Boolean combination of winning conditions. In *Proceedings of the International Conference on the Foundations of Software Technology and Theoretical Computer Science, FSTTCS'18*, volume 122. Schloß Dagstuhl, 2018.

[RRS14] Mickael Randour, Jean-François Raskin, and Ocan Sankur. Variations on the stochastic shortest path problem. In *Proceedings of the International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI'15*, volume 8931. Springer-Verlag, 2014.

[RRS17] Mickael Randour, Jean-François Raskin, and Ocan Sankur. Percentile queries in multi-dimensional Markov decision processes. *Formal Methods for System Design*, 50, 2017.

[RSB05] Jean-François Raskin, Mathias Samuelides, and Laurent Van Begin. Games for counting abstractions. In *Proceedings of the International Workshop on Automated Verification of Critical Systems, AVoCS'04*, volume 128. Elsevier, 2005.
[RSV06] Dinah Rosenberg, Eilon Solan, and Nicolas Vieille. Stochastic games with imperfect monitoring. In *Advances in Dynamic Games: Applications to Economics, Management Science, Engineering, and Environmental Management*. Birkhäuser Boston, 2006.

[Sav70] Walter J. Savitch. Relationships between nondeterministic and deterministic tape complexities. *Journal of Computer and System Sciences*, 4, 1970.

[SB18] Richard S. Sutton and Andrew G. Barto. *Reinforcement Learning: An Introduction*. MIT Press, 2018.

[SE84] Robert S. Streett and E. Allen Emerson. The propositional mu-calculus is elementary. In *Proceedings of the International Colloquium on Automata, Languages and Programming, ICALP'84*, 1984.

[SE89] Robert S. Streett and E. Allen Emerson. An automata theoretic decision procedure for the propositional mu-calculus. *Information and Computation*, 81, 1989.

[Ser03] Olivier Serre. Note on winning positions on pushdown games with ω-regular conditions. *Information Processing Letters*, 85, 2003.

[Ser04] Olivier Serre. *Contribution à l'étude des jeux sur des graphes de processus à pile*. PhD thesis, Université Paris 7, 2004.

[Ser06a] Olivier Serre. Games with winning conditions of high borel complexity. *Theoretical Computer Science*, 350, 2006.

[Ser06b] Olivier Serre. Parity games played on transition graphs of one-counter processes. In *Proceedings of the International Conference on the Foundations of Software Science and Computational Structures, FoSSaCS'06*, volume 3921. Springer-Verlag, 2006.

[Sha53] Lloyd S. Shapley. Stochastic games. In *Proceedings of the National Academy of Science*, volume 39, 1953.

[Sko21] Mateusz Skomra. Optimal bounds for bit-sizes of stationary distributions in finite Markov chains. Technical report, ArXiv, 2021.

[SP73] John Maynard Smith and George R. Price. The logic of animal conflict. *Nature*, 246, 1973.

[SS12] Sylvain Schmitz and Philippe Schnoebelen. Algorithmic aspects of wqo theory. Lecture notes, European Summer School on Logic, Language and Information, ESSLLI'12, 2012.

[Str81] Robert S. Streett. A propositional dynamic logic of looping and converse. Technical report, Massachusetts Institute of Technology, 1981.
[SW89] Colin Stirling and David Walker. Local model checking in the modal mu-calculus. In *Proceedings of the International Joint Conference on Theory and Practice of Software Development, TAPSOFT'89*, 1989.

[TA99] Stavros Tripakis and Karine Altisen. On-the-fly controller synthesis for discrete and dense-time systems. In *Proceedings of the World Congress on Formal Methods, FM'99*, volume 1708. Springer-Verlag, 1999.

[Tho95] Wolfgang Thomas. On the synthesis of strategies in infinite games. In *Proceedings of the International Symposium on Theoretical Aspects of Computer Science, STACS'95*, volume 900. Springer-Verlag, 1995.

[Tho97] Wolfgang Thomas. Languages, automata, and logic. In *Handbook of Formal Languages, Volume 3: Beyond Words*. Springer-Verlag, 1997.

[Tho09] Wolfgang Thomas. Facets of synthesis: Revisiting Church's problem. In *Proceedings of the International Conference on the Foundations of Software Science and Computational Structures, FoSSaCS'09*, 2009.

[Tse90] Paul Tseng. Solving H-horizon, stationary Markov decision problems in time proportional to $log(H)$. *Operation Research Letters*, 9, 1990.

[Urq99] Alasdair Urquhart. The complexity of decision procedures in relevance logic II. *Journal of Symbolic Logic*, 64, 1999.

[Var98] Moshe Y. Vardi. Reasoning about the past with two-way automata. In *Proceedings of the International Colloquium on Automata, Languages and Programming, ICALP'98*, volume 1443. Springer, 1998.

[VCD$^{+}$15] Yaron Velner, Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, Alexander Rabinovich, and Jean-François Raskin. The complexity of multi-mean payoff and multi-energy games. *Information and Computation*, 241, 2015.

[Vel15] Yaron Velner. Robust multidimensional mean-payoff games are undecidable. In *Proceedings of the International Conference on the Foundations of Software Science and Computational Structures, FoSSaCS'15*, volume 9034. Springer-Verlag, 2015.

[VJ00] Jens Vöge and Marcin Jurdziński. A discrete strategy improvement algorithm for solving parity games. In *Proceedings of the International Conference on Computer Aided Verification, CAV'00*, 2000.

[vNM44] John von Neumann and O. Morgenstern. *Theory of Games and Economic Behavior*. Princeton University Press, 1944.

[Wag79] Klaus W. Wagner. On omega-regular sets. *Information and Computation*, 43, 1979.
[Wal96] Igor Walukiewicz. Pushdown processes: Games and model checking. In *Proceedings of the International Conference on Computer Aided Verification*, CAV'96, volume 1102. Springer-Verlag, 1996.

[Wal01] Igor Walukiewicz. Pushdown processes: Games and model-checking. *Information and Computation*, 164, 2001.

[Wal02] Igor Walukiewicz. Monadic second-order logic on tree-like structures. *Theoretical Computer Science*, 275, 2002.

[Wil91] David Williams. *Probability with Martingales*. Cambridge University Press, 1991.

[Ye11] Yinyu Ye. The simplex and policy-iteration methods are strongly polynomial for the Markov decision problem with a fixed discount rate. *Mathematics of Operations Research*, 36, 2011.

[Zer13] Ernst Zermelo. Über eine Anwendung der mengenlehre auf die theorie des schachspiels. In *Proceedings of the International Congress of Mathematicians, ICM'13*, volume 2. Cambridge University Press, 1913.

[Zie98] Wiesław Zielonka. Infinite games on finitely coloured graphs with applications to automata on infinite trees. *Theoretical Computer Science*, 200, 1998.

[ZP96] Uri Zwick and Mike Paterson. The complexity of mean payoff games. *Theoretical Computer Science*, 158, 1996.