and finally

$$ \ell_{1 \le ? \le m_0 + 1} \xrightarrow{-b_0} \ell_1, $$

$$ \ell_{1 \le ? \le m_0 + 1} \xrightarrow{0} \ell_1, $$

where for all $1 \le d \le p(n)$, $\ell_{1 \le ? \le 2^d}(c)$ allows to reach $\odot(0)$ if and only if $1 \le c \le 2^d$:

$$ \ell_{1 \le ? \le 2^{d+1}} \xrightarrow{-2^d} \ell_{1 \le ? \le 2^d}, $$

$$ \ell_{1 \le ? \le 2^1} \xrightarrow{-1} \ell_1, $$

$$ \ell_{1 \le ? \le 2^{d+1}} \xrightarrow{0} \ell_{1 \le ? \le 2^d}, $$

$$ \ell_{1 \le ? \le 2^1} \xrightarrow{0} \ell_1. $$

The remainder of the reduction is now very similar to the reduction shown in Theorem 11.3. Regarding initialisation, Eve can choose her initial position, which we implement by the actions

$$ \ell_0 \xrightarrow{-1} \ell_0 $$

$$ \ell_0 \xrightarrow{-1} \ell_{(q_{\text{final}}, a)} \quad \text{for } a \in \Gamma. $$

Outside the boundary cases, the game is implemented by the following actions:

$$ \ell_{\gamma} \xrightarrow{-m} \ell_{(\gamma_1, \gamma_2, \gamma_3)} $$

for $\gamma_1, \gamma_2, \gamma_3 \vdash \gamma$,

$$ \ell_{(\gamma_1, \gamma_2, \gamma_3)} \xrightarrow{0} \ell_{\gamma_k}^k $$

$$ \ell_{\gamma_k}^k \xrightarrow{-k} \ell_{\gamma_k} $$

for $k \in \{1, 2, 3\}$.

We handle the endmarker positions via the following actions, where Eve proceeds along the left edge of Figure 11.6 until she reaches the initial left endmarker:

$$ \ell_{\triangleleft} \xrightarrow{-m-2} \ell_{\triangleright}, $$

$$ \ell_{\triangleright} \xrightarrow{-1} \ell_1, $$

$$ \ell_{\triangleleft} \xrightarrow{-m-1} \ell_{\triangleright}. $$

For the positions inside the input word $w = a_1 \cdots a_n$, we use the actions

$$ \ell_{(q_0, a_1)} \xrightarrow{-2} \ell_1, $$

$$ \ell_{a_j} \xrightarrow{-2} \ell_j $$

for $1 < j \le n$.

Finally, for the blank symbols of $C_1$, which should be associated with a counter value $c$ such that $n+3 \le c \le m+3$, i.e., such that $1 \le c-n-2 \le m-n+1 = m_{p(n)}+1$, we use the action

$$ \ell_{\Box} \xrightarrow{-n-2} \ell_{1 \le ? \le m_{p(n)} + 1}. $$

Regarding the given initial credit variant, we add a new location $\ell'_0$ controlled by Eve and let her choose her initial credit when starting from $\ell'_0(0)$ by using the new actions $\ell'_0 \xrightarrow{1} \ell'_0$ and $\ell'_0 \xrightarrow{0} \ell_0$. $\square$

### 11.3.2 Asymmetric Monotone Games

The results on configuration reachability might give the impression that asymmetry does not help much for solving vector games: we obtained in Section 11.3.1 exactly the same results as in the general case. Thankfully, the situation changes drastically if we consider the other types of vector games: coverability, non-termination, and parity become decidable in asymmetric vector games. The main rationale for this comes from order theory, which prompts the following definitions.
**Quasi-orders** A quasi-order $(X, \le)$ is a set $X$ together with a reflexive and transitive relation $\le \subseteq X \times X$. Two elements $x, y \in X$ are incomparable if $x \not\le y$ and $y \not\le x$, and they are equivalent if $x \le y$ and $y \le x$. The associated strict relation $x < y$ holds if $x \le y$ and $y \not\le x$.

The upward closure of a subset $S \subseteq X$ is the set of elements greater or equal to the elements of $S$: $\uparrow S \stackrel{\text{def}}{=} \{x \in X \mid \exists y \in S. y \le x\}$. A subset $U \subseteq X$ is upwards closed if $\uparrow U = U$. When $S = \{x\}$ is a singleton, we write more simply $\uparrow x$ for its upward closure and call the resulting upwards closed set a **principal filter**. Dually, the downward closure of $S$ is $\downarrow S \stackrel{\text{def}}{=} \{x \in X \mid \exists y \in S. x \le y\}$, a **downwards closed** set is a subset $D \subseteq X$ such that $D = \downarrow D$, and $\downarrow x$ is called a **principal ideal**. Note that the complement $X \setminus U$ of an upwards closed set $U$ is downwards closed and vice versa.

**Monotone Games** Let us consider again the natural semantics $\mathcal{A}_{\mathbb{N}}(\mathcal{V})$ of a vector system. The set of vertices $V = \mathcal{L} \times \mathbb{N}^k \cup \{\perp\}$ is naturally equipped with a partial ordering: $v \le v'$ if either $v = v' = \perp$, or $v = \ell(\vec{v})$ and $v' = \ell(\vec{v}')$ are two configurations that share the same location and satisfy $\vec{v}(i) \le \vec{v}'(i)$ for all $1 \le i \le k$, i.e., if $\vec{v} \le \vec{v}'$ for the componentwise ordering.

Consider a set of colours $C$ and a vertex colouring $vcol: V \to C$ of the natural semantics $\mathcal{A}_{\mathbb{N}}(\mathcal{V})$ of a vector system, which defines a colouring $c: E \to C$ where $c(e) \stackrel{\text{def}}{=} vcol(\text{In}(e))$. We say that the colouring $vcol$ is **monotonic** if $C$ is finite and, for every colour $p \in C$, the set $vcol^{-1}(p)$ of vertices coloured by $p$ is upwards closed with respect to $\le$. Clearly, the colourings of coverability, non-termination, and parity vector games are monotonic, whereas those of configuration reachability vector games are not. By extension, we call a vector game **monotonic** if its underlying colouring is monotonic.

**Lemma 132 (Simulation).** In a monotonic asymmetric vector game, if Eve wins from a vertex $v_0$, then she also wins from $v'_0$ for all $v'_0 \ge v_0$.

*Proof.* It suffices for this to check that, for all $v_1 \le v_2$ in $V$,

(colours) $vcol(v_1) = vcol(v_2)$ since $vcol$ is monotonic;

(zig Eve) if $v_1, v_2 \in V_{\text{Eve}}$, $a \in A$, and $\Delta(v_1, a) = v'_1 \neq \perp$ is defined, then $v'_2 \stackrel{\text{def}}{=} \Delta(v_2, a)$ is such that $v'_2 \ge v'_1$: indeed, $v'_1 \neq \perp$ entails that $v_1$ is a configuration $\ell(\vec{v}_1)$ and $v'_1 = \ell'(\vec{v}_1 + \vec{u})$ for the action $a = (\ell \xrightarrow{\vec{u}} \ell') \in A$, but then $v_2 = \ell(\vec{v}_2)$ for some $\vec{v}_2 \ge \vec{v}_1$ and $v'_2 = \ell'(\vec{v}_2 + \vec{u}) \ge v'_1$;

(zig Adam) if $v_1, v_2 \in V_{\text{Adam}}$, $a \in A$, and $\Delta(v_2, a) = v'_2$ is defined, then $v'_1 \stackrel{\text{def}}{=} \Delta(v_1, a) \le v'_2$: indeed, either $v'_2 = \perp$ and then $v'_1 = \perp$, or $v'_2 \neq \perp$, thus $v_2 = \ell(\vec{v}_2)$, $v'_2 = \ell'(\vec{v}_2)$, and $a = (\ell \xrightarrow{\vec{0}} \ell') \in A$ (recall that the game is asymmetric), but then $v_1 = \ell(\vec{v}_1)$ for some $\vec{v}_1 \le \vec{v}_2$ and thus $v'_1 = \ell'(\vec{v}_1) \le v'_2$.

The above conditions show that, if $\sigma: E^* \to A$ is a strategy of Eve that wins from $v_0$, then by *simulating* $\sigma$ starting from $v'_0$—i.e., by applying the same actions when given a pointwise larger or equal history—she will also win. $\square$

Note that Lemma 132 implies that $W_{\text{Eve}}$ is upwards closed: $v_0 \in W_{\text{Eve}}$ and $v_0 \le v'_0$ imply $v'_0 \in W_{\text{Eve}}$. Lemma 132 does not necessarily hold in vector games without the
asymmetry condition. For instance, in both Figures 11.3 and 11.4 on p. 359, $\ell'(0,1) \in W_{\text{Eve}}$ but $\ell'(1,2) \in W_{\text{Adam}}$ for the coverability and non-termination objectives. This is due to the fact that the action $\ell' \xrightarrow{-1,0} \ell$ is available in $\ell'(1,2)$ but not in $\ell'(0,1)$.

**Well-quasi-orders** What makes monotonic vector games so interesting is that the partial order ($V, \le$) associated with the natural semantics of a vector system is a *well-quasi-order*. A quasi-order ($X, \le$) is well (a wqo) if any of the following equivalent characterisations hold [Kru72, SS12]:

* in any infinite sequence $x_0, x_1, \dots$ of elements of $X$, there exists an infinite sequence of indices $n_0 < n_1 < \dots$ such that $x_{n_0} \le x_{n_1} \le \dots$—infinite sequences in $X$ are *good*—,

* any strictly ascending sequence $U_0 \subsetneq U_1 \subsetneq \dots$ of upwards closed sets $U_i \subseteq X$ is finite—$X$ has the *ascending chain condition*—,

* any non-empty upwards closed $U \subseteq X$ has at least one, and at most finitely many minimal elements up to equivalence; therefore any upwards closed $U \subseteq X$ is a finite union $U = \bigcup_{1 \le j \le n} \uparrow x_j$ of finitely many principal filters $\uparrow x_j$—$X$ has the *finite basis property*.

The fact that ($V, \le$) satisfies all of the above is an easy consequence of Dickson's Lemma [Dic13].

**Pareto Limits** By the finite basis property of ($V, \le$) and Lemma 132, in a monotonic asymmetric vector game, $W_{\text{Eve}} = \bigcup_{1 \le j \le n} \uparrow \ell_j(\vec{v}_j)$ is a finite union of principal filters. The set Pareto $\stackrel{\text{def}}{=} \{\ell_1(\vec{v}_1), \dots, \ell_n(\vec{v}_n)\}$ is called the *Pareto limit* or *Pareto frontier* of the game. Both the existential and the given initial credit variants of the game can be reduced to computing this Pareto limit: with existential initial credit and an initial location $\ell_0$, check whether $\ell_0(\vec{v}) \in \text{Pareto}$ for some $\vec{v}$, and with given initial credit and an initial configuration $\ell_0(\vec{v}_0)$, check whether $\ell_0(\vec{v}) \in \text{Pareto}$ for some $\vec{v} \le \vec{v}_0$.

**Example 11** (Pareto limit). Consider the asymmetric vector system from Figure 11.7 on p. 368. For the coverability game with target configuration $\ell(2,2)$, the Pareto limit is Pareto $= \{\ell(2,2), \ell'(3,2), \ell_{2,1}(0,1), \ell_{-1,0}(3,2)\}$, while for the non-termination game, Pareto $= \emptyset$: Eve loses from all the vertices. Observe that this is consistent with Eve's winning region in the coverability energy game shown in Figure 11.12.

**Example 12** (Doubly exponential Pareto limit). Consider the one-player vector system of Figure 11.9, where the meta-decrement from $\ell_0$ to $\ell_1$ can be implemented using $O(n)$ additional counters and a set $\mathcal{L}'$ of $O(n)$ additional locations by the arguments of the forthcoming Theorem 125.

For the coverability game with target configuration $\ell_f(\vec{0})$, if $\ell_0$ is the initial location and we are given initial credit $m \cdot \vec{e}_1$, Eve wins if and only if $m \ge 2^{2^n}$, but with existential initial credit she can start from $\ell_0(\vec{e}_2)$ instead. We have indeed $\text{Pareto} \cap (\{\ell_0, \ell_1, \ell_f\} \times \mathbb{N}^k) = \{\ell_0(\vec{e}_2), \ell_0(2^{2^n} \cdot \vec{e}_1), \ell_1(\vec{0}), \ell_f(\vec{0})\}$. Looking more in-depth into the construction of Theorem 125, there is also an at least double exponential number of distinct minimal configurations in Pareto.
<figure><img src="image_91.png" /><figcaption>Figure 11.9: A one-player vector system with a large Pareto limit.</figcaption></figure>

**Finite Memory** Besides having a finitely represented winning region, Eve also has finite memory strategies in asymmetric vector games with parity objectives; the following argument is straightforward to adapt to the other regular objectives from Chapter 2.

**Lemma 133 (Finite memory suffices in parity asymmetric vector games).** If Eve has a strategy winning from some vertex $v_0$ in a parity asymmetric vector game, then she has a finite-memory one.

*Proof.* Assume $\sigma$ is a winning strategy from $v_0$. Consider the tree of vertices visited by plays consistent with $\sigma$: each branch is an infinite sequence $v_0, v_1, \dots$ of elements of $V$ where the maximal priority occuring infinitely often is some even number $p$. Since $(V, \le)$ is a wqo, this is a good sequence: there exists infinitely many indices $n_0 < n_1 < \dots$ such that $v_{n_0} \le v_{n_1} \le \dots$. There exists $i < j$ such that $p = \max_{n_i \le n < n_j} \text{vcol}(v_n)$ is the maximal priority occurring in some interval $v_{n_i}, v_{n_{i+1}}, \dots, v_{n_{j-1}}$. Then Eve can play in $v_{n_j}$ as if she were in $v_{n_i}$, in $v_{n_{j+1}}$ as if she were in $v_{n_{i+1}}$ and so on, and we prune the tree at index $n_j$ along this branch so that $v_{n_j}$ is a leaf, and we call $v_{n_i}$ the *return node* of that leaf. We therefore obtain a finitely branching tree with finite branches, which by König's Lemma is finite.

The finite tree we obtain this way is sometimes called a *self-covering tree*. It is relatively straightforward to construct a finite memory structure $(M, m_0, \delta)$ (as defined in Section 1.5) from a self-covering tree, using its internal nodes as memory states plus an additional sink memory state $m_\perp$; the initial memory state $m_0$ is the root of the tree. In a node $m$ labelled by $\ell(\vec{v})$, given an edge $e = (\ell(\vec{v}'), \ell'(\vec{v} + \vec{u}))$ arising from an action $\ell \xrightarrow{\vec{u}} \ell' \in A$, if $\vec{v}' \ge \vec{v}$ and $m$ has a child $m'$ labelled by $\ell'(\vec{v} + \vec{u})$ in the self-covering tree, then either $m'$ is a leaf with return node $m''$ and we set $\delta(m,e) \stackrel{\text{def}}{=} m''$, or $m'$ is an internal node and we set $\delta(m,e) \stackrel{\text{def}}{=} m'$; in all the other cases, $\delta(m,e) \stackrel{\text{def}}{=} m_\perp$. $\square$

**Example 13** (doubly exponential memory). Consider the one-player vector system of Figure 11.10, where the meta-decrement from $\ell_1$ to $\ell_0$ can be implemented using $O(n)$ additional counters and $O(n)$ additional locations by the arguments of the forthcoming Theorem 125 on p. 387.

For the parity game with location colouring $\text{lcol}(\ell_0) \stackrel{\text{def}}{=} 2$ and $\text{lcol}(\ell_1) \stackrel{\text{def}}{=} 1$, note that Eve must visit $\ell_0$ infinitely often in order to fulfil the parity requirements. Starting from the initial configuration $\ell_0(\vec{0})$, any winning play of Eve begins by

$$ \ell_0(\vec{0}) \xrightarrow{0} \ell_1(\vec{0}) \xrightarrow{\vec{e}_1} \ell_1(\vec{e}_1) \xrightarrow{\dots} \vec{e}_1 \xrightarrow{\dots} \ell_1(m \cdot \vec{e}_1) \xrightarrow{-2^{2^n}} \ell_0((m - 2^{2^n}) \cdot \vec{e}_1) $$
<figure><img src="image_92.png" /><figcaption>Figure 11.10: A one-player vector system witnessing the need for double exponential memory.</figcaption></figure>

for some $m \ge 2^{2^n}$ before she visits again a configuration—namely $\ell_0((m - 2^{2^n}) \cdot \vec{e}_1)$— greater or equal than a previous configuration—namely $\ell_0(\vec{0})$—and witnesses a max- imal even parity in the meantime. She then has a winning strategy that simply re- peats this sequence of actions, allowing her to visit successively $\ell_0(2(m - 2^{2^n}) \cdot \vec{e}_1)$, $\ell_0(3(m - 2^{2^n}) \cdot \vec{e}_1)$, etc. In this example, she needs at least $2^{2^n}$ memory to remember how many times the $\ell_1 \xrightarrow{\vec{e}_1} \ell_1$ loop should be taken.

## Attractor Computation for Coverability

So far, we have not seen how to compute the Pareto limit derived from Lemma 132 nor the finite memory structure derived from Lemma 133. These objects are not merely finite but also computable. The simplest case is the one of coverability asymmetric monotonic vector games: the fixed point computation of Section 2.1 for reachability objectives can be turned into an algorithm computing the Pareto limit of the game.

**Fact 20 (Computable Pareto limit).** The Pareto limit of a coverability asymmetric vector game is computable.

*Proof.* Let $\ell_f(\vec{v}_f)$ be the target configuration. We define a chain $U_0 \subseteq U_1 \subseteq \dots$ of sets $U_i \subseteq V$ by

$$U_0 \stackrel{\text{def}}{=} \uparrow \ell_f(\vec{v}_f), \qquad U_{i+1} \stackrel{\text{def}}{=} U_i \cup \text{Pre}(U_i).$$

Observe that for all $i$, $U_i$ is upwards closed. This can be checked by induction over $i$: it holds initially in $U_0$, and for the induction step, if $v \in U_{i+1}$ and $v' \ge v$, then either

* $v = \ell(\vec{v}) \in \text{Pre}(U_i) \cap V_{\text{Eve}}$ thanks to some $\ell \xrightarrow{\vec{u}} \ell' \in A$ such that $\ell'(\vec{v} + \vec{u}) \in U_i$; therefore $v' = \ell(\vec{v}')$ for some $\vec{v}' \ge \vec{v}$ is such that $\ell'(\vec{v}' + \vec{u}) \in U_i$ as well, thus $v' \in \text{Pre}(U_i) \subseteq U_{i+1}$, or

* $v = \ell(\vec{v}) \in \text{Pre}(U_i) \cap V_{\text{Adam}}$ because for all $\ell \xrightarrow{\vec{0}} \ell' \in A$, $\ell'(\vec{v}) \in U_i$; therefore $v' = \ell(\vec{v}')$ for some $\vec{v}' \ge \vec{v}$ is such that $\ell'(\vec{v}') \in U_i$ as well, thus $v' \in \text{Pre}(U_i) \subseteq U_{i+1}$, or

* $v \in U_i$ and therefore $v' \in U_i \subseteq U_{i+1}$.

By the ascending chain condition, there is a finite rank $i$ such that $U_{i+1} \subseteq U_i$ and then $W_{\text{Eve}} = U_i$. Thus the Pareto limit is obtained after finitely many steps. In order to turn this idea into an algorithm, we need a way of representing those infinite upwards
closed sets $U_i$. Thankfully, by the finite basis property, each $U_i$ has a finite basis $B_i$ such that $\uparrow B_i = U_i$. We therefore compute the following sequence of sets

$$B_0 \stackrel{\text{def}}{=} \{\ell_f(\vec{v}_f)\} \qquad B_{i+1} \stackrel{\text{def}}{=} B_i \cup \min \text{Pre}(\uparrow B_i).$$

Indeed, given a finite basis $B_i$ for $U_i$, it is straightforward to compute a finite basis for the upwards closed Pre($U_i$). This results in Algorithm 11.1 below. □

<caption>**Algorithm 11.1:** Fixed point algorithm for coverability in asymmetric vector games.</caption>

**Data:** A vector system and a target configuration $\ell_f(\vec{v}_f)$
$B_0 \leftarrow \{\ell_f(\vec{v}_f)\}$;
$i \leftarrow 0$;
**repeat**
| $B_{i+1} \leftarrow B_i \cup \min \text{Pre}(\uparrow B_i)$;
| $i \leftarrow i+1$;
**until** $\uparrow B_i \supset B_{i+1}$;
**return** $\min B_i = \text{Pareto}(\mathcal{G})$

While this algorithm terminates thanks to the ascending chain condition, it may take quite long. For instance, in Example 12, it requires at least $2^{2^n}$ steps before it reaches its fixed point. This is a worst-case instance, as it turns out that this algorithm works in $2\text{EXP}$; see the bibliographic notes at the end of the chapter. Note that such a fixed point computation does not work directly for non-termination or parity vector games, due to the need for greatest fixed points.

## 11.4 Resource-conscious games

Vector games are very well suited for reasoning about systems manipulating discrete resources, modelled as counters. However, in the natural semantics, actions that would deplete some resource, i.e., that would make some counter go negative, are simply inhibited. In models of real-world systems monitoring resources like a gas tank or a battery, a depleted resource would be considered as a system failure. In the energy games of Section 11.4.1, those situations are accordingly considered as winning for Adam. Moreover, if we are modelling systems with a bounded capacity for storing resources, a counter exceeding some bound might also be considered as a failure, which will be considered with bounding games in Section 11.4.2.

These resource-conscious games can be seen as providing alternative semantics for vector systems. They will also be instrumental in establishing complexity upper bounds for monotonic asymmetric vector games later in Section 11.5, and are strongly related to multidimensional mean payoff games, as will be explained in Section 12.2 of Chapter 12.
### 11.4.1 Energy Semantics

Energy games model systems where the depletion of a resource allows Adam to win. This is captured by an energy semantics $\mathcal{A}_E(\mathcal{V}) \stackrel{\text{def}}{=} (V, E_E, V_{\text{Eve}}, V_{\text{Adam}})$ associated with a vector system $\mathcal{V}$: we let as before $V \stackrel{\text{def}}{=} (\mathcal{L} \times \mathbb{N}^k) \uplus \{\perp\}$, but define instead

$$ E_E \stackrel{\text{def}}{=} \left\{ \begin{array}{l} \left( \ell(\vec{v}), \ell'(\vec{v} + \vec{u}) \mid \ell \xrightarrow{\vec{u}} \ell' \in A \text{ and } \vec{v} + \vec{u} \ge \vec{0} \right) \\ \cup \left( \ell(\vec{v}), \perp \mid \forall \ell \xrightarrow{\vec{u}} \ell' \in A. \vec{v} + \vec{u} \not\ge \vec{0} \right) \cup \left( \perp, \perp \mid \forall \ell \xrightarrow{\vec{u}} \ell' \in A. \vec{v} + \vec{u} \not\ge \vec{0} \right) \end{array} \right\}. $$

In the energy semantics, moves that would result in a negative component lead to the sink instead of being inhibited.

**Example 14 (Energy semantics).** Figure 11.11 illustrates the energy semantics of the vector system depicted in Figure 11.1 on p. 356. Observe that, by contrast with the natural semantics of the same system depicted in Figure 11.2, all the configurations $\ell'(0, n)$ controlled by Adam can now move to the sink.

<figure><img src="image_93.png" /><figcaption>Figure 11.11: The energy semantics of the vector system of Figure 11.1: a circle (resp. a square) at position $(i, j)$ of the grid denotes a configuration $\ell(i, j)$ (resp. $\ell'(i, j)$) controlled by Eve (resp. Adam).</figcaption></figure>

Given a colouring $c: E \to C$ and an objective $\Omega$, we call the resulting game $(\mathcal{A}_E(\mathcal{V}), c, \Omega)$ an energy game. In particular, we shall speak of configuration reachability, coverability, non-termination, and parity energy games when replacing $\mathcal{A}_N(\mathcal{V})$ by $\mathcal{A}_E(\mathcal{V})$ in Problems 13 to 16; the existential initial credit variants are defined similarly.

**Example 15 (Energy games).** Consider the target configuration $\ell(2, 2)$ in Figures 11.1 and 11.11. Eve's winning region in the configuration reachability energy game is $W_{\text{Eve}} = \{\ell(n+2, n+2) \mid n \in \mathbb{N}\}$, displayed on the left in Figure 11.12. In the coverage energy game, Eve's winning region is $W_{\text{Eve}} = \{\ell(m+2, n+2), \ell'(m+3, n+2) \mid m, n \in \mathbb{N}\}$ displayed on the right in Figure 11.12.

The reader might have noticed that the natural semantics of the asymmetric system of Figure 11.7 and the energy semantics of the system of Figure 11.1 are essentially the same. This correspondence is quite general.

**Lemma 134 (Energy vs. asymmetric vector games).** Energy games and asymmetric vector games are LOGSPACE-equivalent for configuration reachability, coverability, non-termination, and parity, both with given and with existential initial credit.
<figure><img src="image_94.png" /><figcaption>Figure 11.12: The winning regions of Eve in the configuration reachability energy game (left) and the coverability energy game (right) on the graphs of Figures 11.1 and 11.11 with target configuration $ℓ(2, 2)$. The winning vertices are in filled in green, while the losing ones are filled with white with a red border; the sink is always losing.</figcaption></figure>

*Proof.* Let us first reduce asymmetric vector games to energy games. Given $\mathcal{V}$, $c$, and $\Omega$ where $\mathcal{V}$ is asymmetric and Eve loses if the play ever visits the sink $\perp$, we see that Eve wins $(\mathcal{A}_N(\mathcal{V}), c, \Omega)$ from some $v \in V$ if and only if she wins $(\mathcal{A}_E(\mathcal{V}), c, \Omega)$ from $v$. Of course, this might not be true if $\mathcal{V}$ is not asymmetric, as seen for instance in Examples 9 and 15.

Conversely, let us reduce energy games to asymmetric vector games. Consider $\mathcal{V} = (\mathcal{L}, A, \mathcal{L}_{Eve}, \mathcal{L}_{Adam}, k)$, a colouring $c$ defined from a vertex colouring vcol by $c(e) \stackrel{\text{def}}{=} \text{vcol}(\text{In}(e))$, and an objective $\Omega$, where vcol and $\Omega$ are such that Eve loses if the play ever visits the sink $\perp$ and such that, for all $\pi \in C^*$, $p \in C$, and $\pi' \in C^\omega$, $\pi p \pi' \in \Omega$ if and only if $\pi p \pi' \in \Omega$ (we shall call $\Omega$ *stutter-invariant*, and the objectives in the statement are indeed *stutter-invariant*). We construct an asymmetric vector system $\mathcal{V}' \stackrel{\text{def}}{=} (\mathcal{L} \uplus \mathcal{L}_A, A', \mathcal{L}_{Eve} \uplus \mathcal{L}_A, \mathcal{L}_{Adam}, k)$ where we add the following locations controlled by Eve:

$$ \mathcal{L}_A \stackrel{\text{def}}{=} \{ \ell_a | a = (\ell \xrightarrow{\vec{u}} \ell') \in A \text{ and } \ell \in \mathcal{L}_{Adam} \}. $$

We also modify the set of actions:

$$ A' \stackrel{\text{def}}{=} \{ \ell \xrightarrow{\vec{u}} \ell' | \ell \xrightarrow{\vec{u}} \ell' \in A \text{ and } \ell \in \mathcal{L}_{Eve} \} \\ \cup \{ \ell \xrightarrow{\vec{0}} \ell_a, \ell_a \xrightarrow{\vec{u}} \ell' | a = (\ell \xrightarrow{\vec{u}} \ell') \in A \text{ and } \ell \in \mathcal{L}_{Adam} \}. $$

Figure 11.7 presents the result of this reduction on the system of Figure 11.1. We define a vertex colouring vcol' of $\mathcal{A}_N(\mathcal{V}')$ with vcol'(v) $\stackrel{\text{def}}{=} \text{vcol}(v)$ for all $v \in \mathcal{L} \times \mathbb{N}^k \uplus \{\perp\}$ and vcol'(l(a(\vec{v}))) $\stackrel{\text{def}}{=} \text{vcol}(l(\vec{v}))$ if $a = (\ell \xrightarrow{\vec{u}} \ell') \in A$. Then, for all vertices $v \in V$, Eve wins from $v$ in the energy game $(\mathcal{A}_E(\mathcal{V}), c, \Omega)$ if and only if she wins from $v$ in the vector game $(\mathcal{A}_N(\mathcal{V}'), c', \Omega)$. The crux of the argument is that, in a configuration $\ell(\vec{v})$ where $\ell \in \mathcal{L}_{Adam}$, if $a = (\ell \xrightarrow{\vec{u}} \ell') \in A$ is an action with $\vec{v} + \vec{u} \ge \vec{0}$, in the energy semantics, Adam can force the play into the sink by playing $a$; the same occurs in $\mathcal{V}'$ with the natural semantics, as Adam can now choose to play $\ell \xrightarrow{\vec{0}} \ell_a$ where Eve has only $\ell_a \xrightarrow{\vec{u}} \ell'$ at her disposal, which leads to the sink. $\square$

In turn, energy games with existential initial credit are related to the multi-dimensional mean payoff games of Chapter 12.
## 11.4.2 Bounded Semantics

While Adam wins immediately in an energy game if a resource gets depleted, he also wins in a bounding game if a resource reaches a certain bound $B$. This is a *hard upper bound*, allowing to model systems where exceeding a capacity results in failure, like a dam that overflows and floods the area. We define for a bound $B \in \mathbb{N}$ the *bounded semantics* $\mathcal{A}_B(\mathcal{V}) = (V^B, E^B, V_{\text{Eve}}^B, V_{\text{Adam}}^B)$ of a vector system $\mathcal{V}$ by

$$ 
\begin{align*}
V^B &\stackrel{\text{def}}{=} \{ \ell(\vec{v}) \mid \ell \in \mathcal{L} \text{ and } \|\vec{v}\| < B \}, \\
E^B &\stackrel{\text{def}}{=} \{ (\ell(\vec{v}), \ell'(\vec{v}+\vec{u})) \mid \ell \xrightarrow{\vec{u}} \ell' \in A, \vec{v}+\vec{u} \ge \vec{0}, \text{ and } \|\vec{v}+\vec{u}\| < B \} \\
&\phantom{=} \cup \{ (\ell(\vec{v}), \perp) \mid \forall \ell \xrightarrow{\vec{u}} \ell' \in A, \vec{v}+\vec{u} \not\ge \vec{0} \text{ or } \|\vec{v}+\vec{u}\| \ge B \} \cup \{ (\perp, \perp) \}.
\end{align*}
$$

As usual, $V_{\text{Eve}}^B \stackrel{\text{def}}{=} V^B \cap \mathcal{L}_{\text{Eve}} \times \mathbb{N}^k$ and $V_{\text{Adam}}^B \stackrel{\text{def}}{=} V^B \cap \mathcal{L}_{\text{Adam}} \times \mathbb{N}^k$. Any edge from the energy semantics that would bring to a configuration $\ell(\vec{v})$ with $\vec{v}(i) \ge B$ for some $1 \le i \le k$ leads instead to the sink. All the configurations in this arena have norm less than $B$, thus $|V^B| = |\mathcal{L}|B^k + 1$, and the qualitative games of Chapter 2 are decidable over this arena.

Our focus here is on non-termination games played on the bounded semantics where $B$ is not given as part of the input, but quantified existentially. As usual, the existential initial credit variant of Problem 18 is obtained by quantifying $\vec{v}_0$ existentially in the question.

**Problem 18 (bounding game with given initial credit).**

**INPUT:** A vector system $\mathcal{V} = (\mathcal{L}, A, \mathcal{L}_{\text{Eve}}, \mathcal{L}_{\text{Adam}}, k)$, an initial location $\ell_0 \in \mathcal{L}$, and an initial credit $\vec{v}_0 \in \mathbb{N}^k$.

**OUTPUT:** Does there exist $B \in \mathbb{N}$ such that Eve has a strategy to avoid the sink $\perp$ from $\ell_0(\vec{v}_0)$ in the bounded semantics? That is, does there exist $B \in \mathbb{N}$ such that she wins the bounding game $(\mathcal{A}_B(\mathcal{V}), c, \text{Safe})$ from $\ell_0(\vec{v}_0)$, where $c(e) \stackrel{\text{def}}{=} \text{ Lose if and only if } \text{In}(e) = \perp$?

**Lemma 135.** *There is a LOGSPACE reduction from parity asymmetric vector games to bounding games, both with given and with existential initial credit.*

*Proof.* Given an asymmetric vector system $\mathcal{V} = (\mathcal{L}, A, \mathcal{L}_{\text{Eve}}, \mathcal{L}_{\text{Adam}}, k)$, a location colouring lcol: $\mathcal{L} \to \{1, \dots, 2d\}$, and an initial location $\ell_0 \in \mathcal{L}$, we construct a vector system $\mathcal{V}'$ of dimension $k' \stackrel{\text{def}}{=} k+d$ as described in Figure 11.13, where the priorities in $\mathcal{V}$ for $p \in \{1, \dots, d\}$ are indicated above the corresponding locations.

If Eve wins the bounding game played over $\mathcal{V}'$ from some configuration $\ell_0(\vec{v}_0)$, then she also wins the parity vector game played over $\mathcal{V}$ from the configuration $\ell_0(\vec{v}'_0)$ where $\vec{v}'_0$ is the projection of $\vec{v}_0$ to $\mathbb{N}^k$. Indeed, she can play essentially the same strategy: by Lemma 132 she can simply ignore the new decrement self loops, while the actions on the components in $\{k+1, \dots, k+d\}$ ensure that the maximal priority visited infinitely often is even—otherwise some decrement $-\vec{e}_{k+p}$ would be played infinitely often but the increment $\vec{e}_{k+p}$ only finitely often.
<figure><img src="image_95.png" /><figcaption>Figure 11.13: Schema of the reduction to bounding games in the proof of Lemma 135.</figcaption></figure>

Conversely, consider the parity game $\mathcal{G}$ played over $\mathcal{A}_{\mathbb{N}}(\mathcal{Y})$ with the colouring defined by $lcol$. Then the Pareto limit of the game is finite, thus there exists a natural number

$$B_0 \stackrel{\text{def}}{=} 1 + \max_{\ell_0(\vec{v}_0) \in \text{Pareto}(\mathcal{G})} \|\vec{v}_0\| \quad (11.1)$$

bounding the norms of the minimal winning configurations. For a vector $\vec{v}$ in $\mathbb{N}^k$, let us write $\overline{\vec{v}}^{B_0}$ for the vector ‘capped’ at $B$: for all $1 \le i \le k$, $\overline{\vec{v}}^{B_0}(i) \stackrel{\text{def}}{=} \vec{v}(i)$ if $\vec{v}(i) < B_0$ and $\overline{\vec{v}}^{B_0} \stackrel{\text{def}}{=} B_0$ if $\vec{v}(i) \ge B_0$.

Consider now some configuration $\ell_0(\vec{v}_0) \in \text{Pareto}(\mathcal{G})$. As seen in Lemma 133, since $\ell_0(\vec{v}_0) \in W_{\text{Eve}}(\mathcal{G})$, there is a finite self-covering tree witnessing the fact, and an associated winning strategy. Let $H(\ell_0(\vec{v}_0))$ denote the height of this self-covering tree and observe that all the configurations in this tree have norm bounded by $\|\vec{v}_0\| + \|A\| \cdot H(\ell_0(\vec{v}_0))$. Let us define

$$B \stackrel{\text{def}}{=} B_0 + (\|A\| + 1) \cdot \max_{\ell_0(\vec{v}_0) \in \text{Pareto}(\mathcal{G})} H(\ell_0(\vec{v}_0)). \quad (11.2)$$

This is a bound on the norm of the configurations appearing on the (finitely many) self-covering trees spawned by the elements of $\text{Pareto}(\mathcal{G})$. Note that $B \ge B_0 + (\|A\| + 1)$ since a self-covering tree has height at least one.

Consider the non-termination game $\mathcal{G}_B \stackrel{\text{def}}{=} (\mathcal{A}_B(\mathcal{Y}'), c', \text{Safe})$ played over the bounded semantics defined by $B$, where $c'(e) = \text{ Lose if and only if } \text{In}(e) = \perp$. Let $\vec{b} \stackrel{\text{def}}{=} \sum_{1 \le p \le d} (B-1) \cdot \vec{e}_{k+p}$.

**Claim 3.** If $\ell_0(\vec{v}) \in W_{\text{Eve}}(\mathcal{G})$, then $\ell_0(\vec{v}^{B_0} + \vec{b}) \in W_{\text{Eve}}(\mathcal{G}_B)$.

Indeed, by definition of the Pareto limit $\text{Pareto}(\mathcal{G})$, if $\ell_0(\vec{v}) \in W_{\text{Eve}}(\mathcal{G})$, then there exists $\vec{v}_0 \le \vec{v}$ such that $\ell_0(\vec{v}_0) \in \text{Pareto}(\mathcal{G})$. By definition of the bound $B_0$, $\|\vec{v}_0\| < B_0$,
thus $\vec{v}_0 \le \vec{v}^{B_0}$. Consider the self-covering tree of height $H(\ell_0(\vec{v}_0))$ associated to $\ell_0(\vec{v}_0)$, and the strategy $\sigma'$ defined by the memory structure from the proof of Lemma 133. This is a winning strategy for Eve in $\mathscr{G}$ starting from $\ell_0(\vec{v}_0)$, and by Lemma 132, it is also winning from $\ell_0(\vec{v}^{B_0})$.

Here is how Eve wins $\mathscr{G}_B$ from $\ell_0(\vec{v}^{B_0} + \vec{b})$. She essentially follows the strategy $\sigma'$, with two modifications. First, whenever $\sigma'$ goes to a return node $\ell(\vec{v})$ instead of a leaf $\ell(\vec{v}')$—thus $\vec{v} \le \vec{v}'$—, the next time Eve has the control, she uses the self loops to decrement the current configuration by $\vec{v}' - \vec{v}$. This ensures that any play consistent with the modified strategy remains between zero and $B-1$ on the components in $\{1, \dots, k\}$. (Note that if she never regains the control, the current vector never changes any more since $\mathscr{V}$ is asymmetric.)

Second, whenever a play in $\mathscr{G}$ visits a location with even parity $2p$ for some $p$ in $\{1, \dots, d\}$, Eve has the opportunity to increase the coordinates in $\{k+1, \dots, k+p\}$ in $\mathscr{G}_B$. She does so and increments until all these components reach $B-1$. This ensures that any play consistent with the modified strategy remains between zero and $B-1$ on the components in $\{k+1, \dots, k+p\}$. Indeed, $\sigma'$ guarantees that the longest sequence of moves before a play visits a location with maximal even priority is bounded by $H(\ell_0(\vec{v}_0))$, thus the decrements $-\vec{e}_{k+p}$ introduced in $\mathscr{G}_B$ by the locations from $\mathscr{G}$ with odd parity $2p-1$ will never force the play to go negative. $\square$

The bound $B$ defined in Equation (11.2) in the previous proof is not constructive, and possibly much larger than really required. Nevertheless, one can sometimes show that an explicit $B$ suffices in a bounding game. A simple example is provided by the coverability asymmetric vector games with existential initial credit arising from Remark 22, i.e., where the objective is to reach some location $\ell_f$. Indeed, it is rather straightforward that there exists a suitable initial credit such that Eve wins the game if and only if she wins the finite reachability game played over the underlying directed graph over $\mathcal{L}$ where we ignore the counters. Thus, for an initial location $\ell_0$, $B_0 = |\mathcal{L}| \cdot \|A\| + 1$ bounds the norm of the necessary initial credit, while a simple path may visit at most $|\mathcal{L}|$ locations, thus $B = B_0 + |\mathcal{L}| \cdot \|A\|$ suffices for Eve to win the constructed bounding game.

In the general case of bounding games with existential initial credit, an explicit bound can be established. The proof goes along very different lines and is too involved to fit in this chapter, but we refer the reader to [JLS15, CJLS17] for details.

**Theorem 119 (Bounds on bounding).** If Eve wins a bounding game with existential initial credit defined by a vector system $\mathscr{V} = (\mathcal{L}, A, \mathcal{L}_{Eve}, \mathcal{L}_{Adam}, k)$, then an initial credit $\vec{v}_0$ with $\|\vec{v}_0\| = (4|\mathcal{L}| \cdot \|A\|)^{2(k+2)^3}$ and a bound $B = 2(4|\mathcal{L}| \cdot \|A\|)^{2(k+2)^3} + 1$ suffice for this.

Theorem 119 also yields a way of handling bounding games with given initial credit.
# 11.5 The complexity of asymmetric monotone games

Unlike general vector games and configuration reachability asymmetric ones, coverability, non-termination, and parity asymmetric vector games are decidable. We survey in this section the best known complexity bounds for every case; see Table 11.1 at the end of the chapter for a summary.

## 11.5.1 Upper Bounds

We begin with complexity upper bounds. The main results are that parity games with existential initial credit can be solved in coNP, but are in 2EXP with given initial credit. In both cases however, the complexity is pseudo-polynomial if both the dimension $k$ and the number of priorities $d$ are fixed, which is rather good news: one can hope that, in practice, both the number of different resources (encoded by the counters) and the complexity of the functional specification (encoded by the parity condition) are tiny compared to the size of the system.

### Existential Initial Credit

**Counterless Strategies** Consider a strategy $\tau$ of Adam in a vector game. In all the games we consider, uniform positional strategies suffice over the infinite arena $\mathcal{A}_{\mathbb{N}}(\mathcal{Y}) = (V, E, V_{\text{Eve}}, V_{\text{Adam}})$: $\tau$ maps vertices in $V$ to edges in $E$. We call $\tau$ counterless if, for all locations $\ell \in \mathcal{L}_{\text{Adam}}$ and all vectors $\vec{v}, \vec{v}' \in \mathbb{N}^k$, $\tau(\ell(\vec{v})) = \tau(\ell(\vec{v}'))$. A counterless strategy thus only considers the current location of the play.

**Lemma 136 (Counterless strategies).** Let $\mathcal{Y} = (\mathcal{L}, A, \mathcal{L}_{\text{Eve}}, \mathcal{L}_{\text{Adam}}, k)$ be an asymmetric vector system, $\ell_0 \in \mathcal{L}$ be a location, and lcol: $\mathcal{L} \to \{1, \dots, d\}$ be a location colouring. If Adam wins from $\ell_0(\vec{v})$ for every initial credit $\vec{v}$ in the parity game played over $\mathcal{Y}$ with lcol, then he has a single counterless strategy such that he wins from $\ell_0(\vec{v})$ for every initial credit $\vec{v}$.

*Proof.* Let $A_{\text{Adam}} \stackrel{\text{def}}{=} \{(\ell \xrightarrow{\vec{u}} \ell') \in A \mid \ell \in \mathcal{L}_{\text{Adam}}\}$ be the set of actions controlled by Adam. We assume without loss of generality that every location $\ell \in \mathcal{L}_{\text{Adam}}$ has either one or two outgoing actions, thus $|\mathcal{L}_{\text{Adam}}| \le |A_{\text{Adam}}| \le 2|\mathcal{L}_{\text{Adam}}|$. We proceed by induction over $|A_{\text{Adam}}|$. For the base case, if $|A_{\text{Adam}}| = |\mathcal{L}_{\text{Adam}}|$ then every location controlled by Adam has a single outgoing action, thus any strategy for Adam is trivially counterless.

For the induction step, consider some location $\hat{\ell} \in \mathcal{L}_{\text{Adam}}$ with two outgoing actions $a_l \stackrel{\text{def}}{=} \hat{\ell} \xrightarrow{0} \ell_l$ and $a_r \stackrel{\text{def}}{=} \hat{\ell} \xrightarrow{0} \ell_r$. Let $\mathcal{Y}_l$ and $\mathcal{Y}_r$ be the vector systems obtained from $\mathcal{Y}$ by removing respectively $a_r$ and $a_l$ from $A$, i.e., by using $A_l \stackrel{\text{def}}{=} A \setminus \{a_r\}$ and $A_r \stackrel{\text{def}}{=} A \setminus \{a_l\}$. If Adam wins the parity game from $\ell(\vec{v})$ for every initial credit $\vec{v}$ in either $\mathcal{Y}_l$ or $\mathcal{Y}_r$, then by induction hypothesis he has a counterless winning strategy winning from $\ell(\vec{v})$ for every initial credit $\vec{v}$, and the same strategy is winning in $\mathcal{Y}$ from $\ell(\vec{v})$ for every initial credit $\vec{v}$.

In order to conclude the proof, we show that, if Adam loses in $\mathcal{Y}_l$ from $\ell_0(\vec{v}_l)$ for some $\vec{v}_l \in \mathbb{N}^k$ and in $\mathcal{Y}_r$ from $\ell_0(\vec{v}_r)$ for some $\vec{v}_r \in \mathbb{N}^k$, then there exists $\vec{v}_0 \in \mathbb{N}^k$ such that Eve wins from $\ell_0(\vec{v}_0)$ in $\mathcal{Y}$. Let $\sigma_l$ and $\sigma_r$ denote Eve's winning strategies in the two
games. By a slight abuse of notations (justified by the fact that we are only interested
in a few initial vertices), we see plays as sequences of actions and strategies as maps
$A^* \to A$. Consider the set of plays consistent with $\sigma_r$ starting from $\ell_0(\vec{v}_r)$. If none of
those plays visits $\ell$, then Eve wins in $\mathcal{Y}$ from $\ell_0(\vec{v}_r)$ and we conclude. Otherwise, there
is some finite prefix $\hat{\pi}$ of a play that visits $\ell(\hat{v})$ for some vector $\hat{v} = \vec{v}_r + w(\hat{\pi})$. We let
$\vec{v}_0 \stackrel{\text{def}}{=} \vec{v}_l + \hat{v}$ and show that Eve wins from $\ell_0(\vec{v}_0)$.

We define now a strategy $\sigma$ for Eve over $\mathcal{Y}$ that switches between applying $\sigma_l$
and $\sigma_r$ each time $a_r$ is used and switches back each time $a_l$ is used. More precisely,
given a finite or infinite sequence $\pi$ of actions, we decompose $\pi$ as $\pi_1 a_1 \pi_2 a_2 \pi_3 \cdots$
where each segment $\pi_j \in (A \setminus \{a_l, a_r\})^*$ does not use either $a_l$ nor $a_r$ and each $a_j \in$
$\{a_l, a_r\}$. The associated mode $m(j) \in \{l, r\}$ of a segment $\pi_j$ is $m(1) \stackrel{\text{def}}{=} l$ for the ini-
tial segment and otherwise $m(j) \stackrel{\text{def}}{=} l$ if $e_{j-1} = a_l$ and $m(j) \stackrel{\text{def}}{=} r$ otherwise. The $l$-
subsequence associated with $\pi$ is the sequence of segments $\pi(l) \stackrel{\text{def}}{=} \pi_1 a_{l_2-1} \pi_{l_2} a_{l_3-1} \pi_{l_3} \cdots$
with mode $m(l_i) = l$, while the $r$-subsequence is the sequence $\pi(r) \stackrel{\text{def}}{=} \hat{\pi} a_{r_1-1} \pi_{r_1} a_{r_2-1} \pi_{r_2} \cdots$
with mode $m(r_i) = r$ prefixed by $\hat{\pi}$. Then we let $\sigma(\pi) \stackrel{\text{def}}{=} \sigma_m(\pi(m))$ where $m \in \{l, r\}$ is
the mode of the last segment of $\pi$.

Consider an infinite play $\pi$ consistent with $\sigma$ starting from $\ell_0(\vec{v}_0)$. Since $\vec{v}_0 \ge \vec{v}_l$ and $\vec{v}_0 \ge \vec{v}_r + w(\hat{\pi})$, $\pi(l)$ and $\pi(r)$ starting from $\ell_0(\vec{v}_0)$ are consistent with simulating—in the sense of Lemma 132—$\sigma_l$ from $\ell_0(\vec{v}_l)$ and $\sigma_r$ from $\ell_0(\vec{v}_r)$. Let $\pi'$ be a finite prefix of $\pi$. Then $w(\pi') = w(\pi'(l)) + w(\pi'(r))$ where $\pi'(l)$ is a prefix of $\pi(l)$ and $\pi'(r)$ of $\pi(r)$, thus $w(\pi'(l)) \le \vec{v}_l$ and $w(\pi'(r)) \le \vec{v}_r + w(\hat{\pi})$, thus $w(\pi') \le \vec{v}_0$: the play $\pi$ avoids the sink. Furthermore, the maximal priority seen infinitely often along $\pi(l)$ and $\pi(r)$ is even (note that one of $\pi(l)$ and $\pi(r)$ might not be infinite), thus the maximal priority seen infinitely often along $\pi$ is also even. This shows that $\sigma$ is winning for Eve from $\ell_0(\vec{v}_0)$. $\square$

We are going to exploit Lemma 136 in Theorem 122 in order to prove a coNP upper bound for asymmetric games with existential initial credit: it suffices in order to decide those games to guess a counterless winning strategy $\tau$ for Adam and check that it is indeed winning by checking that Eve loses the one-player game arising from $\tau$. This last step requires an algorithmic result of independent interest.

**One-player Case** Let $\mathcal{Y} = (\mathcal{L}, A, k)$ be a vector addition system with states, lcol: $\mathcal{L} \to \{1, \dots, d\}$ a location colouring, and $\ell_0 \in \mathcal{L}$ an initial location. Then Eve wins the parity one-player game from $\ell_0(\vec{v}_0)$ for some initial credit $\vec{v}_0$ if and only if there exists some location such that

• $\ell$ is reachable from $\ell_0$ in the directed graph underlying $\mathcal{Y}$ and

• there is a cycle $\pi \in A^*$ from $\ell$ to itself such that $w(\pi) \ge 0$ and the maximal priority occurring along $\pi$ is even.

Indeed, assume we can find such a location $\ell$. Let $\hat{\pi} \in A^*$ be a path from $\ell_0$ to $\ell$ and $\vec{v}_0(i) \stackrel{\text{def}}{=} \max\{\|w(\pi')\| \mid \pi'$ is a prefix of $\hat{\pi}\pi\}$ for all $1 \le i \le k$. Then $\ell_0(\vec{v}_0)$ can reach $\ell(\vec{v}_0 + w(\hat{\pi}))$ in the natural semantics of $\mathcal{Y}$ by following $\hat{\pi}$, and then $\ell(\vec{v}_0 + \tilde{W}(\hat{\pi}) + nw(\pi)) \ge \ell(\vec{v}_0 + w(\hat{\pi}))$ after $n$ repetitions of the cycle $\pi$. The infinite play arising from this strategy has an even maximal priority.
Conversely, if Eve wins, then there is a winning play $\pi \in A^\omega$ from $\ell_0(\vec{v}_0)$ for some $\vec{v}_0$. Recall that $(V, \leq)$ is a wqo, and we argue as in Lemma 133 that there is indeed such a location $\ell$.

Therefore, solving one-player parity vector games boils down to determining the existence of a cycle with non-negative effect and even maximal priority. We shall use linear programming techniques in order to check the existence of such a cycle in polynomial time [KS88].

Let us start with a relaxed problem: we call a *multi-cycle* a non-empty finite set of cycles $\Pi$ and let $w(\Pi) \stackrel{\text{def}}{=} \sum_{\pi \in \Pi} w(\pi)$ be its weight; we write $t \in \Pi$ if $t \in \pi$ for some $\pi \in \Pi$. Let $M \in 2^A$ be a set of 'mandatory' subsets of actions and $F \subseteq A$ a set of 'forbidden' actions. Then we say that $\Pi$ is *non-negative* if $w(\Pi) \ge \vec{0}$, and that it is *suitable* for $(M, F)$ if for all $A' \in M$ there exists $t \in A'$ such that $t \in \Pi$, and if for all $t \in F, t \notin \Pi$. We use the same terminology for a single cycle $\pi$.

**Lemma 137 (Linear programs for suitable non-negative multi-cycles).** Let $\mathcal{V}$ be a vector addition system with states, $M \in 2^A$, and $F \subseteq A$. We can check in polynomial time whether $\mathcal{V}$ contains a non-negative multi-cycle $\Pi$ suitable for $(M, F)$.

*Proof.* We reduce the problem to solving a linear program. For a location $\ell$, let $\text{in}(\ell) \stackrel{\text{def}}{=} \{(\ell' \xrightarrow{\vec{u}} \ell) \in A \mid \ell' \in \mathcal{L}\}$ and $\text{out}(\ell) \stackrel{\text{def}}{=} \{(\ell' \xrightarrow{\vec{u}} \ell') \in A \mid \ell' \in \mathcal{L}\}$ be its sets of incoming and outgoing actions. The linear program has a variable $x_a$ for each action $a \in A$, which represents the number of times the action $a$ occurs in the multi-cycle. It consists of the following constraints:

$$ \forall \ell \in \mathcal{L}, \qquad \sum_{a \in \text{in}(\ell)} x_a = \sum_{a \in \text{out}(\ell)} x_a, \qquad (\text{multi-cycle}) $$

$$ \forall a \in A, \qquad x_a \ge 0, \qquad (\text{non-negative uses}) $$

$$ \forall i \in \{1, \dots, k\}, \qquad \sum_{a \in A} x_a \cdot w(t)(i) \ge 0, \qquad (\text{non-negative weight}) $$

$$ \forall A' \in M, \qquad \sum_{a \in A} x_a \ge 0 \qquad (\text{non empty}) $$

$$ \forall a \in F, \qquad \sum_{a \in A'} x_a \ge 0, \qquad (\text{every subset in } M \text{ is used}) $$

$$ \forall a \in F, \qquad x_a = 0. \qquad (\text{no forbidden actions}) $$

As solving a linear program is in polynomial time Theorem 2, the result follows. $\square$

Of course, what we are aiming for is finding a non-negative *cycle* suitable for $(M, F)$ rather than a multi-cycle. Let us define for this the relation $\ell \sim \ell'$ over $\mathcal{L}$ if $\ell = \ell'$ or if there exists a non-negative multi-cycle $\Pi$ suitable for $(M, F)$ such that $\ell$ and $\ell'$ belong to some cycle $\pi \in \Pi$.

**Fact 21.** The relation $\sim$ is an equivalence relation.

*Proof.* Symmetry and reflexivity are trivial, and if $\ell \sim \ell'$ and $\ell' \sim \ell''$ because $\ell$ and $\ell'$ appear in some cycle $\pi \in \Pi$ and $\ell'$ and $\ell''$ in some cycle $\pi' \in \Pi'$ for two non-negative
multi-cycles $\Pi$ and $\Pi'$ suitable for $(M, F)$, then up to a circular shift $\pi$ and $\pi'$ can be assumed to start and end with $\ell'$, and then $(\Pi \setminus \{\pi\}) \cup (\Pi' \setminus \{\pi'\}) \cup \{\pi\pi'\}$ is also a non-negative multi-cycle suitable for $(M, F)$. $\square$

Thus $\sim$ defines a partition $\mathcal{L}/\sim$ of $\mathcal{L}$. In order to find a non-negative cycle $\pi$ suitable for $(M, F)$, we are going to compute the partition $\mathcal{L}/\sim$ of $\mathcal{L}$ according to $\sim$. If we obtain a partition with a single equivalence class, we are done: there exists such a cycle. Otherwise, such a cycle if it exists must be included in one of the subsystems $(P, A \cap (P \times \mathbb{Z}^k \times P), k)$ induced by the equivalence classes $P \in \mathcal{L}/\sim$. This yields Algorithm 11.2, which assumes that we know how to compute the partition $\mathcal{L}/\sim$. Note that the depth of the recursion in Algorithm 11.2 is bounded by $|\mathcal{L}|$ and that recursive calls operate over disjoint subsets of $\mathcal{L}$, thus assuming that we can compute the partition in polynomial time, then Algorithm 11.2 also works in polynomial time.

<caption>**Algorithm 11.2:** cycle($\mathcal{V}, M, F$)</caption>

**Data:** A vector addition system with states $\mathcal{V} = (\mathcal{L}, A, k), M \in 2^A, F \subseteq A$
**if** $|\mathcal{L}| = 1$ **then**
  **if** $\mathcal{V}$ has a non-negative multi-cycle suitable for $(M, F)$ **then**
    **return true**
  **else**
    $\mathcal{L}/\sim$ ← partition($\mathcal{V}, M, F$);
**if** $|\mathcal{L}/\sim| = 1$ **then**
  **return true**
**else**
  **foreach** $P \in \mathcal{L}/\sim$ **do**
    **if** cycle((P, A ∩ (P × $\mathbb{Z}^k$ × P), k), M, F) **then**
      **return true**
    **else**
      **return false**

It remains to see how to compute the partition $\mathcal{L}/\sim$. Consider for this the set of actions $A' \stackrel{\text{def}}{=} \{a \mid \exists \Pi \text{ a non-negative multi-cycle suitable for } (M, F) \text{ with } a \in \Pi\}$ and $\mathcal{V}' = (\mathcal{L}', A', k)$ the subsystem induced by $A'$.

**Claim 4.** There exists a path from $\ell$ to $\ell'$ in $\mathcal{V}'$ if and only if $\ell \sim \ell'$.

*Proof.* If $\ell \sim \ell'$, then either $\ell = \ell'$ and there is an empty path, or there exist $\Pi$ and $\pi \in \Pi$ such that $\ell$ and $\ell'$ belong to $\pi$ and $\Pi$ is a non-negative multi-cycle suitable for $(M, F)$, thus every action of $\pi$ is in $A'$ and there is a path in $\mathcal{V}'$.

Conversely, if there is a path $\pi \in A'^*$ from $\ell$ to $\ell'$, then $\ell \sim \ell'$ by induction on $\pi$. Indeed, if $|\pi| = 0$ then $\ell = \ell'$. For the induction step, $\pi = \pi'a$ with $\pi' \in A'^*$ a path from $\ell$ to $\ell''$ and $a = (\ell'' \xrightarrow{\vec{u}} \ell') \in A'$ for some $\vec{u}$. By induction hypothesis, $\ell \sim \ell''$ and since $a \in A'$, $\ell'' \sim \ell'$, thus $\ell \sim \ell'$ by transitivity shown in Fact 21. $\square$

By Claim 4, the equivalence classes of $\sim$ are the strongly connected components of $\mathcal{V}'$. This yields the following polynomial time algorithm for computing $\mathcal{L}/\sim$.

Together, Lemma 137 and Algorithms 11.2 and 11.3 yield the following.
<caption>**Algorithm 11.3:** partition($V, M, F$)</caption>

**Data:** A vector addition system with states $V = (\mathcal{L}, A, k)$, $M \in 2^A$, $F \subseteq A$
$A' \leftarrow \emptyset$;
**foreach** $a \in A$ **do**
    if $V$ has a non-negative multi-cycle suitable for $(M \cup \{{a}\}, F)$ **then**
        $A' \leftarrow A' \cup \{a\}$
    $V' \leftarrow$ subsystem induced by $A'$;
**return** SCC($V'$)

**Lemma 138 (Polynomial-time detection of suitable non-negative cycles).** Let $V$ be a vector addition system with states, $M \in 2^A$, and $F \subseteq A$. We can check in polynomial time whether $V$ contains a non-negative cycle $\pi$ suitable for $(M, F)$.

Finally, we obtain the desired polynomial time upper bound for parity in vector
addition systems with states.

**Theorem 120 (Existential one-player parity vector games are in P).** *Whether Eve wins a one-player parity vector game with existential initial credit is in P.*

*Proof.* Let $V = (\mathcal{L}, A, k)$ be a vector addition system with states, lcol: $\mathcal{L} \to \{1, \dots, d\}$ a location colouring, and $\ell_0 \in \mathcal{L}$ an initial location. We start by trimming $V$ to only keep the locations reachable from $\ell_0$ in the underlying directed graph. Then, for every even priority $p \in \{1, \dots, d\}$, we use Lemma 138 to check for the existence of a non-negative cycle with maximal priority $p$: it suffices for this to set $M \stackrel{\text{def}}{=} \{\text{lcol}^{-1}(p)\}$ and $F \stackrel{\text{def}}{=} \text{lcol}^{-1}(\{p+1, \dots, d\})$. $\square$

**Upper Bounds** We are now equipped to prove our upper bounds. We begin with a nearly trivial case. In a coverability asymmetric vector game with existential initial credit, the counters play no role at all: Eve has a winning strategy for some initial credit in the vector game if and only if she has one to reach the target location $\ell_f$ in the finite game played over $\mathcal{L}$ and edges $(\ell, \ell')$ whenever $\ell \xrightarrow{\vec{u}} \ell' \in A$ for some $\vec{u}$. This entails that coverability asymmetric vector games are quite easy to solve.

**Theorem 121 (Existential coverability asymmetric vector games are in P).** *Coverability asymmetric vector games with existential initial credit are P-complete.*

Regarding non-termination and parity, we exploit Lemma 136 and thm. 120.

**Theorem 122 (Existential parity asymmetric vector games are in coNP).** *Non-termination and parity asymmetric vector games with existential initial credit are in coNP.*

*Proof.* By Remark 21, it suffices to prove the statement for parity games. By Lemma 136, if Adam wins the game, we can guess a counterless winning strategy $\tau$ telling which action to choose for every location. This strategy yields a one-player game, and by Theorem 120 we can check in polynomial time that $\tau$ was indeed winning for Adam. $\square$
Finally, in fixed dimension and with a fixed number of priorities, we can simply
apply the results of Section 11.4.2.

**Corollary 21** (Existential fixed-dimensional parity asymmetric vector games are pseudo-polynomial). *Parity asymmetric vector games with existential initial credit are in pseudo-polynomial time if the dimension and the number of priorities are fixed.*

*Proof.* Consider an asymmetric vector system $\mathcal{V} = (\mathcal{L}, A, \mathcal{L}_{\text{Eve}}, \mathcal{L}_{\text{Adam}}, k)$ and a location colouring lcol: $\mathcal{L} \to \{1, \dots, 2d\}$. By Lemma 135, the parity vector game with existential initial credit over $\mathcal{V}$ problem reduces to a bounding game with existential initial credit over a vector system $\mathcal{V}' = (\mathcal{L}', A', \mathcal{L}'_{\text{Eve}}, \mathcal{L}'_{\text{Adam}}, k+d)$ where $\mathcal{L}' \in O(|\mathcal{L}|)$ and $\|A'\| = \|A\|$. By Theorem 119, it suffices to consider the case of a non-termination game with existential initial credit played over the bounded semantics $\mathcal{A}_B(\mathcal{V}')$ where $B$ is in $(|\mathcal{L}'| \cdot \|A'\|)^{O(k+d)^3}$. Such a game can be solved in linear time in the size of the bounded arena using attractor techniques, thus in $O(|\mathcal{L}| \cdot B)^{k+d}$, which is in $(|\mathcal{L}| \cdot \|A\|)^{O(k+d)^4}$ in terms of the original instance. $\square$

Given Initial Credit

**Theorem 123** (Upper bounds for asymmetric vector games). *Coverability, non-termination, and parity asymmetric vector games with given initial credit are in 2EXP. If the dimension is fixed, they are in EXP, and if the number of priorities is also fixed, they are in pseudo-polynomial time.*

11.5.2 Lower Bounds

Let us turn our attention to complexity lower bounds for monotonic asymmetric vector
games. It turns out that most of the upper bounds shown in Section 11.5.1 are tight.

Existential Initial Credit

In the existential initial credit variant of our games, we have the following lower bound matching Theorem 122, already with a unary encoding.

**Theorem 124** (Existential non-termination asymmetric vector games are coNP-hard). *Non-termination, and parity asymmetric vector games with existential initial credit are coNP-hard.*

*Proof.* By Remark 21, it suffices to show hardness for non-termination games. We reduce from the 3SAT problem: given a formula $\varphi = \bigwedge_{1 \le i \le m} C_i$ where each clause $C_i$ is a disjunction of the form $\ell_{i,1} \lor \ell_{i,2} \lor \ell_{i,3}$ of literals taken from $X = \{x_1, \neg x_1, x_2, \neg x_2, \dots, x_k, \neg x_k\}$, we construct an asymmetric vector system $\mathcal{V}$ where Eve wins the non-termination game with existential initial credit if and only if $\varphi$ is not satisfiable; since the game is determined, we actually show that Adam wins the game if and only if $\varphi$ is satisfiable.

Our vector system has dimension 2k, and for a literal $\ell \in X$, we define the vector

$$
\vec{u}_{\ell} \stackrel{\text{def}}{=} \begin{cases} \vec{e}_{2n-1} - \vec{e}_{2n} & \text{if } \ell = x_n, \\ \vec{e}_{2n} - \vec{e}_{2n-1} & \text{if } \ell = \neg x_n. \end{cases}
$$
We define $\mathcal{V} \stackrel{\text{def}}{=} (\mathcal{L}, A, \mathcal{L}_{\text{Eve}}, \mathcal{L}_{\text{Adam}}, 2k)$ where

$$ \mathcal{L}_{\text{Eve}} \stackrel{\text{def}}{=} \{\varphi\} \cup \{\ell_{i,j} \mid 1 \le i \le m, 1 \le j \le 3\}, $$

$$ \mathcal{L}_{\text{Adam}} \stackrel{\text{def}}{=} \{C_i \mid 1 \le i \le m\}, $$

$$ A \stackrel{\text{def}}{=} \{ \varphi \xrightarrow{\vec{0}} C_i \mid 1 \le i \le m \} \cup \{ C_i \xrightarrow{\vec{0}} \ell_{i,j}, \ell_{i,j} \xrightarrow{\vec{\bar{\ell}}_{\ell_{i,j}}} \varphi \mid 1 \le i \le m, 1 \le j \le 3 \}. $$

We use $\varphi$ as our initial location. Let us call a map $v: X \to \{0, 1\}$ a *literal assignment*; we call it *conflicting* if there exists $1 \le n \le k$ such that $v(x_n) = v(\neg x_n)$.

Assume that $\varphi$ is satisfiable. Then there exists a non-conflicting literal assignment $v$ that satisfies all the clauses: for each $1 \le i \le m$, there exists $1 \le j \le 3$ such that $v(\ell_{i,j}) = 1$; this yields a counterless strategy for Adam, which selects $(C_i, \ell_{i,j})$ for each $1 \le i \le m$. Consider any infinite play consistent with this strategy. This play only visits literals $\ell$ where $v(\ell) = 1$. There exists a literal $\ell \in X$ that is visited infinitely often along the play, say $\ell = x_n$. Because $v$ is non-conflicting, $v(\neg x_n) = 0$, thus the location $\neg x_n$ is never visited. Thus the play uses the action $\ell \xrightarrow{\vec{e}_{2n-1}} \varphi$ infinitely often, and never uses any action with a positive effect on component $2n$. Hence the play is losing from any initial credit.

Conversely, assume that $\varphi$ is not satisfiable. By contradiction, assume that Adam wins the game for all initial credits. By Lemma 136, he has a counterless winning strategy $\tau$ that selects a literal in every clause. Consider a literal assignment that maps each one of the selected literals to 1 and the remaining ones in a non-conflicting manner. By definition, this literal assignment satisfies all the clauses, but because $\varphi$ is not satisfiable, it is conflicting: necessarily, there exist $1 \le n \le k$ and $1 \le i, i' \le m$, such that $\tau$ selects $x_n$ in $C_i$ and $\neg x_n$ in $C_{i'}$. But this yields a winning strategy for Eve, which alternates in the initial location $\varphi$ between $C_i$ and $C_{i'}$, and for which an initial credit $\vec{e}_{2n-1} + \vec{e}_{2n}$ suffices: a contradiction. $\square$

Note that Theorem 124 does not apply to fixed dimensions $k \ge 2$. We know by Corollary 21 that those games can be solved in pseudo-polynomial time if the number of priorities is fixed, and by Theorem 122 that they are in coNP.

## Given Initial Credit

With given initial credit, we have a lower bound matching the 2EXP upper bound of Theorem 123, already with a unary encoding. The proof itself is an adaptation of the proof by Lipton [Lip76] of EXPSPACE-hardness of coverability in the one-player case.

**Theorem 125 (Coverability and non-termination asymmetric vector games are 2EXP-hard).**
Coverability, non-termination, and parity asymmetric vector games with given initial credit are 2EXP-hard.

*Proof.* We reduce from the halting problem of an alternating Minsky machine $\mathcal{M} = (\mathcal{L}, A, \mathcal{L}_{\text{Eve}}, \mathcal{L}_{\text{Adam}}, k)$ with counters bounded by $B \stackrel{\text{def}}{=} 2^{2n}$ for $n \stackrel{\text{def}}{=} \lfloor \mathcal{M} \rfloor$. Such a machine is similar to an asymmetric vector system with increments $\ell \xrightarrow{\vec{e}_i} \ell'$, decrements $\ell \xrightarrow{\vec{-e}_i} \ell'$, and zero test actions $\ell \xrightarrow{\vec{i}} \ell'$, all restricted to locations $\ell \in \mathcal{L}_{\text{Eve}}$; the only actions available to Adam are actions $\ell \xrightarrow{\vec{0}} \ell'$. The set of locations contains a distinguished 'halt' location $\ell_{\text{halt}} \in \mathcal{L}$ with no outgoing action. The machine comes with
the promise that, along any play, the norm of all the visited configurations $\ell(\vec{v})$ satisfies $\|\vec{v}\| < B$. The halting problem asks, given an initial location $\ell_0 \in \mathcal{L}$, whether Eve has a winning strategy to visit $\ell_{halt}(\vec{v})$ for some $\vec{v} \in \mathbb{N}^k$ from the initial configuration $\ell_0(\vec{0})$. This problem is 2EXP-complete if $k \ge 3$ by standard arguments [FMR68].

Let us start by a quick refresher on Lipton's construction [Lip76]; see also [Esp98] for a nice exposition. At the heart of the construction lies a collection of one-player gadgets implementing level $j$ meta-increments $\ell \xrightarrow{2^{2^j} \cdot \vec{c}} \ell'$ and level $j$ meta-decrements $\ell \xrightarrow{-2^{2^j} \cdot \vec{c}} \ell'$ for some unit vector $\vec{c}$ using $O(j)$ auxiliary counters and $\text{poly}(j)$ actions, with precondition that the auxiliary counters are initially empty in $\ell$ and post relation that they are empty again in $\ell'$. The construction is by induction over $j$; let us first see a naive implementation for meta-increments. For the base case $j=0$, this is just a standard action $\ell \xrightarrow{2\vec{c}} \ell'$. For the induction step $j+1$, we use the gadget of Figure 11.14 below, where $\vec{x}_j, \bar{x}_j, \vec{z}_j, \bar{z}_j$ are distinct fresh unit vectors: the gadget performs two nested loops, each of $2^{2^j}$ iterations, thus iterates the unit increment of $\vec{c}$ a total of $(2^{2^j})^2 = 2^{2^{j+1}}$ times. A meta-decrement is obtained similarly.

<figure><img src="image_96.png" /><figcaption>Figure 11.14: A naive implementation of the meta-increment $\ell \xrightarrow{2^{2^{j+1}} \cdot \vec{c}} \ell'$.</figcaption></figure>

Note that this level ($j+1$) gadget contains two copies of the level $j$ meta-increment and two of the level $j$ meta-decrement, hence this naive implementation has size $\exp(j)$. In order to obtain a polynomial size, we would like to use a single shared level $j$ gad- get for each $j$, instead of hard-wiring multiple copies. The idea is to use a ‘dispatch mechanism,’ using extra counters, to encode the choice of unit vector $\vec{c}$ and of return location $\ell'$. Let us see how to do this in the case of the return location $\ell'$; the mech- anism for the vector $\vec{c}$ is similar. We enumerate the (finitely many) possible return locations $\ell_0, \dots, \ell_{m-1}$ of the gadget implementing $\ell \xrightarrow{2^{2^{j+1}} \cdot \vec{c}} \ell'$. We use two auxil- iary counters with unit vectors $\vec{r}_j$ and $\bar{\vec{r}}_j$ to encode the return location. Assume $\ell'$ is the $i$th possible return location, i.e., $\ell' = \ell_i$ in our enumeration: before entering the shared gadget implementation, we initialise $\vec{r}_j$ and $\bar{\vec{r}}_j$ by performing the action $\ell \xrightarrow{i \cdot \vec{r}_j + (m-i) \cdot \bar{\vec{r}}_j} \dots$. Then, where we would simply go to $\ell'$ in Figure 11.14 at the end of the gadget, the shared gadget has a final action $\dots \xrightarrow{\vec{0}} \ell_{\text{return}} \xrightarrow{-i \cdot \vec{r}_j - (m-i) \cdot \bar{\vec{r}}_j} \ell_i$ leading to a dispatch location for returns: for all $0 \le i < m$, we have an action $\ell_{\text{return}}$ that leads to the desired return location.

Let us return to the proof. Consider an instance of the halting problem. We first exhibit a reduction to coverability; by Remark 22, this will also entail the 2EXP-hardness of parity asymmetric vector games. We build an asymmetric vector system $\mathcal{V} = (\mathcal{L}', A', \mathcal{L}'_{\text{Eve}}, \mathcal{L}_{\text{Adam}}, k')$ with $k' = 2k + O(n)$. Each of the counters $c_i$ of $\mathcal{M}$ is paired with a complementary counter $\tilde{c}_i$ such that their sum is $B$ throughout the sim-
ulation of $\mathcal{M}$. We denote by $\vec{c}_i$ and $\bar{\vec{c}}_i$ the corresponding unit vectors for $1 \le i \le k$. The vector system $\mathcal{V}$ starts by initialising the counters $\bar{c}_i$ to $B$ by a sequence of meta-increments $\ell'_{i-1} \xrightarrow{2^{2^n} \cdot \bar{\vec{c}}_i} \ell'_i$ for $1 \le i \le k$, before starting the simulation by an action $\ell'_k \xrightarrow{0} \ell_0$. The simulation of $\mathcal{M}$ uses the actions depicted in Figure 11.15. Those maintain the invariant on the complement counters. Regarding zero tests, Eve yields the control to Adam, who has a choice between performing a meta-decrement that will fail if $\bar{c}_i < 2^{2^n}$, which by the invariant is if and only if $c_i > 0$, or going to $\ell'$.

<figure><img src="image_97.png" /><figcaption>Figure 11.15: Schema of the reduction to coverability in the proof of Theorem 125.</figcaption></figure>

It is hopefully clear that Eve wins the coverability game played on $\mathcal{V}$ starting from $\ell'_0(\vec{0})$ and with target configuration $\ell_{halt}(\vec{0})$ if and only if the alternating Minsky machine halts.

Regarding non-termination games, we use essentially the same reduction. First observe that, if Eve can ensure reaching $\ell_{halt}$ in the alternating Minsky machine, then she can do so after at most $|\mathcal{L}|B^k$ steps. We therefore use a ‘time budget’: this is an additional component in $\mathcal{V}$ with associated unit vector $\vec{t}$. This component is initialised to $|\mathcal{L}|B^k = |\mathcal{L}|2^{k2^n}$ before the simulation, and decreases by one at every step; see Figure 11.16. We also add a self loop $\ell_{halt} \xrightarrow{0} \ell_{halt}$. Then the only way to avoid the sink and thus to win the non-termination game is to reach $\ell_{halt}$.

We still need to extend our initialisation phase. It suffices for this to implement a gadget for $k$-meta-increments $\ell \xrightarrow{2^{k2^j} \cdot \vec{c}} \ell'$ and $k$-meta-decrements $\ell \xrightarrow{-2^{k2^j} \cdot \vec{c}} \ell'$; this is the same argument as in Lipton's construction, with a base case $\ell \xrightarrow{2^k} \ell'$ for $j=0$. Then we initialise our time budget through $|\mathcal{L}|$ successive $k$-meta-increments $\ell \xrightarrow{2^{k2^n} \cdot \vec{t}} \ell'$. $\square$

The proof of Theorem 125 relies crucially on the fact that the dimension is not fixed: although $k \ge 3$ suffices in the alternating Minsky machine, we need $O(|\mathcal{M}|)$ additional counters to carry out the reduction. A separate argument is thus needed in order to match the EXP upper bound of Theorem 123 in fixed dimension.
<figure><img src="image_98.png" /><figcaption>Figure 11.16: Schema of the reduction to non-termination in the proof of Theorem 125.</figcaption></figure>

**Theorem 126** (Fixed-dimensional coverability and non-termination asymmetric vector games are EXP-hard). *Coverability, non-termination, and parity asymmetric vector games with given initial credit are EXP-hard in dimension $k \ge 2$.*

*Proof.* We exhibit a reduction from countdown games with given initial credit, which are EXP-complete by Theorem 113. Consider an instance of a configuration reachability countdown game: a countdown system $\mathcal{V} = (\mathcal{L}, A, \mathcal{L}_{Eve}, \mathcal{L}_{Adam}, 1)$ with initial configuration $\ell_0(n_0)$ and target configuration $\odot(0)$—as seen in the proof of Theorem 113, we can indeed assume that the target credit is zero; we will also assume that Eve controls $\odot$ and that the only action available in $\odot$ is $\odot \stackrel{-1}{\longrightarrow} \odot$. We construct an asymmetric vector system $\mathcal{V}'$ of dimension 2 such that Eve can ensure reaching $\odot(0, n_0)$ from $\ell_0(n_0, 0)$ in $\mathcal{V}'$ if and only if she could ensure reaching $\odot(0)$ from $\ell_0(n_0)$ in $\mathcal{V}$. The translation is depicted in Figure 11.17.

<figure><img src="image_99.png" /><figcaption>Figure 11.17: Schema of the reduction in the proof of Theorem 126.</figcaption></figure>

The idea behind this translation is that a configuration $\ell(c)$ of $\mathcal{V}$ is simulated by a configuration $\ell(c, n_0 - c)$ in $\mathcal{V}'$. The crucial point is how to handle Adam's moves. In a configuration $\ell(c, n_0 - c)$ with $c \in \mathcal{L}_{Adam}$, according to the natural semantics of
V, Adam should be able to simulate an action $\ell \xrightarrow{-n} \ell'$ if and only if $c \ge n$. Observe that otherwise if $c < n$ and thus $n_0 - c > n_0 - n$, Eve can play to reach $\odot$ and win immediately. An exception to the above is if $n$ is minimal among the decrements in $\ell$, because according to the natural semantics of V, if $c < n$ there should be an edge to the sink, and this is handled in the second line of Figure 11.17.

Then Eve can reach $\odot(0, n_0)$ if and only if she can cover $\odot(0, n_0)$, if and only if she can avoid the sink thanks to the self loop $\xrightarrow{0,0} \odot$. This shows the EXP-hardness of coverability and non-termination asymmetric vector games in dimension two; the hardness of parity follows from Remarks 21 and 22. □

### 11.5.3 Dimension One

#### Bibliographic references

**Vector Addition Systems with States** In their one-player version, i.e. in vector addition systems with states, all the games presented in Section 11.1 are decidable. With given initial credit, configuration reachability is simply called ‘reachability’ and was first shown decidable by Mayr [May81] (with simpler proofs in [Kos82, Lam92, Ler11]) and recently shown to be of non-elementary complexity $[CLL^+19]$. Coverability and non-termination are considerably easier, as they are EXPSPACE-complete [Lip76, Rac78] and so is parity [Hab97]. With existential initial credit, the problems are markedly simpler: configuration reachability becomes EXPSPACE-complete, while coverability is in NL and non-termination and parity can be solved in polynomial time by Theorem 120 using linear programming techniques [KS88].

**Undecidability of Vector Games** The undecidability results of Section 11.1.2 are folklore. One can find undecidability proofs in [ABd03, RSB05]; non-termination was called ‘deadlock-freedom’ by Raskin et al. [RSB05]. Configuration reachability is undecidable even in very restricted cases, like the *robot games* of [NPR16].

**Succinct One-Counter Games** One-dimensional vector systems are often called *one-counter nets* in the literature, by contrast with *one-counter automata* where zero tests are allowed. The EXPSPACE-completeness of succinct one-counter games was shown by Hunter [Hun15]. Countdown games were originally defined with given initial credit and a zero reachability objective, and shown EXP-complete in [JLS08]; see also [Kie13] for a variant called *hit-or-run games*. The hardness proofs for Theorems 113 and 114 are adapted from [JOS18], where countdown games with existential initial credit were first introduced.

**Asymmetric Vector Games** The asymmetric vector games of Section 11.3 appear under many guises in the literature: as ‘and-branching’ vector addition systems with states in [LMSS92], as ‘vector games’ in [Kan95], as ‘B-games’ in [RSB05], as ‘single sided’ vector addition games in [AMSS13], and as ‘alternating’ vector addition systems with states in [CS14].
The undecidability of configuration reachability shown in Section 11.3.1 was already proven by Lincoln et al. [LMSS92] and used to show the undecidability of propositional linear logic; Kanovich [Kan95, Kan16] refines this result to show the undecidability of the (!, ⊕)-Horn fragment of linear logic. Similar proof ideas are used for Boolean BI and separation logic in [LWG13, BK14].

**Asymmetric Monotone Vector Games** The notion of asymmetric infinite games over a well-quasi-ordered arena constitutes a natural extension of the notion of *well-structured systems* of [AČJT00] and [FS01], and was undertaken in [ABd03, RSB05]. The decidability of coverability and non-termination through wqo arguments like those of Fact 20 was shown by Raskin et al. [RSB05]. More advanced wqo techniques were needed for the first decidability proof of parity in [AMSS13]. See also [SS12] for more on the algorithmic uses of wqos.

By analysing the attractor computation of Section 11.3.2, one can show that Algorithm 11.1 works in 2EXP, thus matching the optimal upper bound from Theorem 123: this can be done using the Rackoff-style argument of [CS14] and the analysis of [BG11], or by a direct analysis of the attractor computation algorithm [LS19].

**Energy Games** An alternative take on energy games is to see a vector system $\mathcal{V} = (\mathcal{L}, A, \mathcal{L}_{Eve}, \mathcal{L}_{Adam}, k)$ as a finite arena with edges $\ell \xrightarrow{\vec{u}} \ell'$ coloured by $\vec{u}$, thus with set of colours $C \stackrel{\text{def}}{=} \mathbb{Z}^k$. For an initial credit $\vec{v}_0 \in \mathbb{N}^k$ and $1 \le i \le k$, the associated energy objective is then defined as

$$ \text{Energy}_{\vec{v}_0}(i) \stackrel{\text{def}}{=} \left\{ \pi \in E^{\omega} \mid \forall n \in \mathbb{N} \cdot \left( \vec{v}_0(i) + \sum_{0 \le j \le n} c(\pi)(i) \right) \ge 0 \right\} $$

that is, $\pi$ is winning if the successive sums of weights on coordinate $i$ are always non-negative. The *multi-energy objective* then asks for the play $\pi$ to belong simultaneously to $\text{Energy}_{\vec{v}_0}(i)$ for all $1 \le i \le k$. This is a multiobjective in the sense of the forthcoming Chapter 12. Multi-energy games are equivalent to non-termination games played on the arena $A_{\mathcal{E}}(\mathcal{V})$ defined by the energy semantics.

The relationship with energy games was first observed in [AMSS13]. The equivalence with mean payoff games in dimension one was first noticed by Bouyer et al. [BFL$^{+}$08]. A similar connection in the multi-dimensional case was established in [CDHR10, VCD$^{+}$15] and will be discussed in Chapter 12.

**Complexity** Table 11.1 summarises the complexity results for asymmetric vector games. For the upper bounds with existential initial credit of Section 11.5.1, the existence of counterless winning strategies for Adam was originally shown by Brázdil et al. [BJK10] in the case of non-termination games; the proof of Lemma 136 is a straightforward adaptation using ideas from [CD12] to handle parities. An alternative proof through bounding games is presented in [CJLS17].

The coNP upper of Theorem 122 was shown soon after Brázdil et al.'s work by Chatterjee et al. [CDHR10] in the case of non-termination games. The extension of
Theorem 122 to parity was shown by [CRR14] by a reduction from parity to non-termination games somewhat reminiscent of ?. The proof of Theorem 122 takes a slightly different approach using Lemma 138 for finding non-negative cycles, which is a trivial adaptation of a result by Kosaraju and Sullivan [KS88]. The pseudo-polynomial bound of Corollary 21 is taken from [CJLS17].

For the upper bounds with given initial credit of Section 11.5.1, regarding coverability, the 2EXP upper bound of Theorem 123 was first shown by Courtois and Schmitz [CS14] by adapting Rackoff's technique for vector addition systems with states [Rac78]. Regarding non-termination, the first complexity upper bounds were shown by Brázdil et al. [BJK10] and were in $k$EXP, thus non-elementary in the size of the input. Very roughly, their argument went as follows: one can extract a pseudo-polynomial existential Pareto bound $B$ in the one-player case from the proof of Theorem 120, from which the proof of Lemma 136 yields a $2^{|A|}(B + |\mathcal{L}|)$ existential Pareto bound in the two-player case, and finally by arguments similar to ? a tower of $k$ exponentials on the given initial credit problem. The two-dimensional case with a unary encoding was shown a bit later to be in P by Chaloupka [Cha13]. Finally, a matching 2EXP upper bound (and pseudo-polynomial in any fixed dimension) was obtained by Jurdziński et al. [JLS15]. Regarding parity, Jančar [Jan15] showed how to obtain non-elementary upper bounds by reducing to the case of [BJK10], before a tight 2EXP upper bound (and pseudo-polynomial in fixed dimension with a fixed number of priorities) was shown in [CJLS17].

The coNP hardness with existential initial credit in Theorem 124 originates from [CDHR10]. The 2EXP-hardness of both coverability and non-termination games with given initial credit from Theorem 125 was shown in [CS14] by adapting Lipton's construction for vector addition systems with states [Lip76]; similar proofs can be found for instance in [DJLL12, BHSS12]. The hardness for EXP-hardness in dimension two was first shown by [FJLS11].

The NP $\cap$ coNP upper bounds in dimension one from Section 11.5.3 are due to Bouyer et al. [BFL$^+$08] for given initial credit and Chatterjee and Doyen [CD12] for existential initial credit.

**Some Applications** Besides their many algorithmic applications for solving various types of games, vector games have been employed in several fields to prove decidability and complexity results, for instance for linear, relevance, or separation logics [LMSS92, Kan95, Urq99, LWG13, BK14, Kan16], simulation and bisimulation problems [Kie13, AMSS13, CS14, JOS18], resource-bounded logics [ABDL18], orchestration synthesis [GVF$^+$18], as well as model-checking probabilistic timed automata [JLS08].
<table><caption>Table 11.1: The complexity of asymmetric vector games.</caption><thead><tr><th rowspan="2">Game</th><th rowspan="2">Initial credit</th><th colspan="3">Dimension</th></tr><tr><th>Fixed k = 1</th><th>Fixed k ≥ 2</th><th>Arbitrary</th></tr></thead><tbody><tr><td>configuration reachability</td><td>-</td><td>EXPSPACE-complete<br/>Theorem 118</td><td></td><td>undecidable<br/>Theorem 117 [LMSS92]</td></tr><tr><td rowspan="2">coverability</td><td>existential</td><td></td><td>P-complete<br/>Theorem 121</td><td></td></tr><tr><td>given</td><td>in NP ∩ coNP</td><td>EXP-complete<br/>Theorems 123 and 126 [FJLS11, CS14]</td><td>2EXP-complete<br/>Theorems 123 and 125 [CS14]</td></tr><tr><td rowspan="2">non-termination</td><td>existential</td><td>in NP ∩ coNP<br/>[CD12]</td><td>in coNP</td><td>coNP-complete<br/>Theorems 122 and 124 [CDHR10]</td></tr><tr><td>given</td><td>in NP ∩ coNP<br/>[BFL+08]</td><td>EXP-complete<br/>Theorems 123 and 126 [FJLS11, JLS15]</td><td>2EXP-complete<br/>Theorems 123 and 125 [CS14, JLS15]</td></tr><tr><td rowspan="2">parity</td><td>existential</td><td>in NP ∩ coNP<br/>[CD12]</td><td>in coNP</td><td>coNP-complete<br/>Theorems 122 and 124 [CDHR10, CRR14]</td></tr><tr><td>given</td><td></td><td>EXP-complete<br/>Theorems 123 and 126 [FJLS11, CJLS17]</td><td>2EXP-complete<br/>Theorems 123 and 125 [CS14, CJLS17]</td></tr></tbody></table>
# Part V

## Multi
<figure><img src="image_100.png" /></figure>
# GAMES WITH MULTIPLE OBJECTIVES

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

<figure><img src="image_102.png" /></figure>
Chapter 12

# Games with multiple objectives

MICKAEL RANDOUR

Up to this chapter, we have mostly been interested in finding strategies that achieve a *single* objective or optimise a *single* payoff function. Our goal here is to discuss what happens when one goes further and wants to build strategies that (i) ensure *several objectives*, or (ii) provide *richer guarantees* than the simple worst-case or expectation ones used respectively in zero-sum games and Markov decision processes (MDPs).

Consider case (i). Such requirements arise naturally in applications: for instance, one may want to define a trade-off between the performance of a system and its energy consumption. A model of choice for this is the natural *multidimensional* extension of the games of Chapter 4, where we consider weight vectors on edges and combinations of objectives.

In case (ii), we base our study on stochastic models such as MDPs (Chapter 5). We will notably present how to devise controllers that provide strong guarantees in a worst-case scenario while behaving efficiently on average (based on a stochastic model of its environment built through statistical observations); effectively reconciling the rational antagonistic behaviour of Adam, used in games, with the stochastic interpretation of uncontrollable interaction at the core of MDPs.

Stepping into the *multi-objective* world is like entering a jungle: the sights are amazing but the wildlife is overwhelming. Providing an exhaustive account of existing multi-objective models and the latest developments in their study is a task doomed to fail: simply consider the combinatorial explosion of all the possible combinations based on the already non-exhaustive set of games studied in the previous chapters. Hence, our goal here is to guide the reader through their first steps in the jungle, highlighting the specific dangers and challenges of the multi-objective landscape, and displaying some techniques to deal with them. To that end, we focus on models studied in Chapter 2, Chapter 4, Chapter 5 and Chapter 11, and multi-objective settings that extend them. We favour simple, natural classes of problems, that already suffice to grasp the cornerstones of multi-objective reasoning.
**Chapter outline** In Section 12.1, we illustrate the additional complexity of multi-objective games and how relations between different classes of games that hold in the single-objective case often break as soon as we consider combinations of objectives.

The next two sections are devoted to the simplest form of multi-objective games: games with conjunctions of classical objectives. In Section 12.2, we present the classical case of multidimensional mean payoff and energy games, which preserve relatively nice properties with regard to their single-objective counterparts. In Section 12.3, we discuss the opposite situation of total payoff and shortest path games: their nice single-objective behaviour vanishes here.

In the last two sections, we explore a different meaning of *multi-objective* through so-called *rich behavioural models*. Our quest here is to find strategies that provide several types of guarantees, of different nature, for the same quantitative objective. In Section 12.4, we address the problem of *beyond worst-case synthesis*, which combines the rational antagonistic interpretation of two-player zero-sum games with the stochastic nature of MDPs. We will study the mean payoff setting and see how to construct strategies that ensure a strict worst-case constraint while providing the highest expected value possible. In Section 12.5, we briefly present *percentile queries*, which extend *probability threshold problems* in MDPs to their multidimensional counterparts. Interestingly, *randomised strategies* become needed in this context, whereas up to Section 12.5, we only consider deterministic strategies as they suffice.

We close the chapter with the usual bibliographic discussion and pointers towards some of the many recent advances in multi-objective reasoning.

## 12.1 From one to multiple dimensions

For the first part of this chapter, we consider *multidimensional quantitative games*. With regard to the formalism of Chapter 4, the only change to the arena is the set of colours associated with edges: we now have vectors in $\mathbb{R}^k$ where $k \in \mathbb{N}_{>0}$ is the dimension of the game. As before, for computational purposes, it makes sense to restrict our colouring to rational numbers, and for the sake of simplicity, we even consider *integers only* without loss of generality. Hence, $c: E \to \mathbb{Z}^k$.

For the weighted games of Chapter 4, where a single quantitative objective $f$ is considered, we know that the value of the game exists. In most cases, optimal strategies do too, which makes the problems of computing the value and solving the game for a given threshold morally equivalent. In our simple multidimensional setting, we focus on *conjunctions* of objectives. Similarly to what we did in the one-dimension case, we will write $f_{\ge \vec{x}}$ with $\vec{x} \in \mathbb{Q}^k$ to define the (qualitative) winning condition

$$f_{\ge \vec{x}} = \bigcap_{i=1}^{k} \{ \pi \in \text{Paths}_{\omega}(G) \mid f_i(\pi) \ge \vec{x}_i \}$$

where $f_i(\pi)$ represents the evaluation of $f$ on the sequence of colours in the $i$-th dimension and $\vec{x}_i$ represents the $i$-th component of vector $\vec{x}$. Hence we consider the natural semantics where we want to satisfy the original objective $f$ component-wise.
<figure><img src="image_103.png" /><figcaption>Figure 12.1: A simple multidimensional mean payoff game where Eve needs infinite memory to play (Pareto-)optimally.</figcaption></figure>

**Example 16.** Consider the simple one-player game in Figure 12.1 fitted with the mean payoff objective $\text{MeanPayoff}^{-}$ (recall that two variants exist depending on the use of lim-sup or lim-inf). Let us first recall that in the single-objective case, memoryless strategies suffice to play optimally (Corollary 6). In this game, such strategies permit to achieve payoffs $(1, -1)$, $(-1, -1)$ and $(-1, 1)$. Intuitively, $(-1, -1)$ is not interesting since we can do better with $(1, -1)$ or $(-1, 1)$. On the other hand, these two other payoffs are incomparable and thus should not be discriminated a priori. In the multi-objective world, there is usually no total order between the outcomes of a game — fixing a total order would actually boil down to transforming the game into a one-dimension game — which is why there is in general no optimal strategy but rather Pareto-optimal ones. Intuitively, a strategy is Pareto-optimal if there exists no other strategy yielding a payoff which is as good in all dimensions and strictly better in at least one dimension.

**Definition 30 (Pareto-optimal strategy).** Given a k-dimension game $\mathcal{G}$ based on the conjunction of $k$ maximising (w.l.o.g.) quantitative objectives $(f_i)_{i=1}^k$, a strategy $\sigma$ for Eve is said to be Pareto-optimal if it guarantees a payoff $\vec{x} \in \mathbb{R}^k$ such that for all other strategy $\sigma'$ of Eve ensuring payoff $\vec{x}' \neq \vec{x}$, it holds that $\vec{x}_i > \vec{x}'_i$ for some dimension $i \in \{1, \dots, k\}$.

The concept of Pareto-optimality has an important consequence on multi-objective problems: the correspondence between solving a value problem and computing an optimal strategy that holds in the single-objective case does not carry over. Indeed, one may now be interested in computing the *Pareto frontier* consisting of all Pareto vectors achievable by Eve. This comes at great cost complexity-wise as this frontier may include many points, and in some settings, even an *infinite number of Pareto vectors* (see Section 12.5 for examples), sometimes forcing us to resort to approximation. This requires specific techniques that go beyond the focus of this chapter, hence in the following we mostly discuss the *value problem*, also referred to as ‘solving the game’ for a given threshold vector.

**Example 17.** Let us go back to Example 16 and fix objective $\text{MeanPayoff}^{-}_{\ge \vec{x}}$ where $\vec{x} = (0, 0)$. As discussed before, this threshold cannot be achieved by a memoryless strategy. Actually, this is also the case for any finite-memory strategy. Indeed, any finite-memory strategy induces an ultimately periodic play, where either (a) the periodic part only visits $v_0$ (resp. $v_1$), yielding payoff $(1, -1)$ (resp. $(-1, 1)$) thanks to prefix independence of the mean payoff (Chapter 4), or (b) it visits both, in which case the mean payoff is of
the form

$$ \vec{y} = \text{MeanPayoff}^{-}(\pi) = \frac{a \cdot (1, -1) + 2 \cdot b \cdot (-1, -1) + c \cdot (-1, 1)}{a + 2 \cdot b + c} $$

where $a, c \in \mathbb{N}$ and $b \in \mathbb{N}_{>0}$. Observe that $\vec{y}_1 + \vec{y}_2 = -4 \cdot b/(a + 2 \cdot b + c)$, which is strictly less than zero for any value of the parameters. Hence $\vec{x} = (0,0)$ is not achievable. Now consider what happens with infinite memory: let $\sigma$ be the strategy of Eve that visits $\ell$ times $v_0$, then $\ell$ times $v_1$, and then repeats forever with increasing values of $\ell$. The mean payoff of the resulting play is the limit of the previous equation when $a=c=\ell$ tends to infinity, with $b=1$: intuitively, the switch between $v_0$ and $v_1$ becomes negligible in the long run and the mean payoff is $\frac{1}{2} \cdot (1, -1) + \frac{1}{2} \cdot (-1, 1) = (0,0)$.

**Remark 23.** While Eve cannot achieve $(0,0)$ with finite memory, she can achieve (i.e., ensure at least) any payoff $(-\epsilon, -\epsilon)$ for $0 < \epsilon < 1$, using sufficient memory: for instance, by taking $b=1$ and $a=c = [\frac{1}{\epsilon} - 1]$. In that sense, the payoff $\vec{x} = (0,0)$ achievable by an infinite-memory strategy can be seen as the supremum of payoffs achievable by finite-memory strategies. Actually, this is exactly how we defined strategy $\sigma$: Eve plays according to an infinite sequence of finite-memory strategies parametrised by $\ell$, such that each strategy of the sequence ensures mean payoff $(-\epsilon, -\epsilon)$, with $\epsilon \to 0$ when $\ell \to \infty$.

**Example 18.** The reasoning above holds similarly for MeanPayoff$^+$. With finite-memory, the lim-sup variant coincides with the lim-inf one: because the play is ultimately periodic, the limit exists. With infinite-memory, Eve can actually achieve the payoff $\vec{x}' = (1,1)$, witnessing a gap with the lim-inf variant. To do so, she has to play a strategy that alternates between $v_0$ and $v_1$ while staying in each vertex for a sufficiently long period such that the current mean over the corresponding dimension gets close to 1. Getting these means closer and closer to 1 and using the lim-sup component-wise then suffices to achieve payoff $\vec{x}'$. This is in stark contrast to the lim-inf variant, which cannot achieve any payoff $(\epsilon, \epsilon)$ for $\epsilon > 0$ (the Pareto vectors correspond to linear combinations of simple cycles, as hinted before).

**Theorem 127.** Multidimensional mean payoff games require infinite-memory strategies for Eve. Furthermore, the lim-inf and lim-sup variants are not equivalent, i.e., their winning regions are in general not identical.

This theorem already shows the first signs of our single-objective assumptions crumbling in the multi-objective world: we jump from memoryless determinacy to needing infinite memory, and objectives that were equivalent both in games and MDPs turn out to be different here. Buckle up, as this was only our first step.

## 12.2 Mean payoff and energy

Another well-known equivalence in one-dimension is the one between mean payoff and energy games (in the existential initial credit form), mentioned in Chapter 4. The reduction is trivial: Eve has a winning strategy (and an initial credit) in the energy game
if and only if she has a strategy to ensure mean payoff at least equal to zero in the mean payoff game played over the same arena. Intuitively, the mean payoff strategy of Eve has to reach a subgame where she can ensure that all cycles formed are non-negative (see cycle games in Chapter 4). The initial credit (which can be as high as Eve wants) offsets the cost of reaching such a subgame as well as the low point of cycles in it (which can be negative but is bounded).

How does it fare in multiple dimensions? The study of vector games with energy semantics in Chapter 11 gives the following result.

**Theorem 128.** *Solving multidimensional energy games is coNP-complete. Exponential-memory strategies suffice and are required for Eve, and memoryless ones suffice for Adam.*

Based on Theorem 127 and Example 17, it is clear that the aforementioned equivalence holds no more, as mean payoff games benefit from infinite memory while energy games do not. In Example 17, the strategy that achieves $\vec{x} = (0,0)$ for the mean payoff does so by switching infinitely often but with decreasing frequency between $v_0$ and $v_1$: the switch becomes negligible in the limit which is fine for the mean payoff. Still, this would lead the energy to drop below zero eventually, whatever the initial credit chosen by Eve, hence showing why the reduction does not carry over.

### 12.2.1 Finite memory

Game-theoretic models are generally used in applications, such as controller synthesis, where one actually wants to implement a winning strategy when it exists. This is why finite-memory strategies have a particular appeal. Hence it is interesting to study what happens when we restrict Eve to finite-memory strategies in multidimensional mean payoff games.

We first observe that when both players use finite-memory strategies, the resulting play is ultimately periodic, hence the lim-inf and lim-sup variants coincide (the limit exists) and take the value of the mean over the periodic part.

**Proposition 11.** *The lim-sup and lim-inf variants of multidimensional mean payoff games coincide under finite memory, i.e., their winning regions are identical in all games.*

We now go back to the relationship with energy games. In the following, we write $\vec{0}$ for the $k$-dimension vector $(0, \dots, 0)$. When restricting both players to finite memory, we regain the equivalence between mean payoff and energy games by a natural extension of the argument sketched above for one-dimension games.

**Theorem 129.** *For all arena and initial vertex, Eve has a winning strategy for the existential initial credit multidimensional energy game if and only if she has a finite-memory winning strategy for the multidimensional (lim-inf or lim-sup) mean payoff game with threshold $\vec{0}$.*

*Proof.* Let $\mathcal{A}$ be an arena coloured by integer vectors of dimension $k$ and $v_0$ be the initial vertex. We first consider the left-to-right implication. Assume that Eve has a
strategy $\sigma$ and some initial credit $\vec{c}_0 \in \mathbb{N}^k$ such that she wins the energy objective over $\mathcal{A}$. By Theorem 128, we may assume $\sigma$ to be finite-memory and $\mathcal{M} = (M, m_0, \delta)$ to be its memory structure. Let $\mathcal{A}_\sigma$ be the classical product of the arena with this memory structure $(\mathcal{A} \times \mathcal{M})$ restricted to the choices made by $\sigma$. We claim that any cycle in $\mathcal{A}_\sigma$ is non-negative in all dimensions (we simply project paths of $\mathcal{A}_\sigma$ to $C^\omega$ to interpret them as we do for paths in $\mathcal{A}$). By contradiction, assume that there exists a cycle whose sum of weights is strictly negative in some dimension. Then the play reaching this cycle and looping in it forever is a play consistent with $\sigma$ that is losing for the energy objective, contradicting the hypothesis. Hence, it is indeed the case that all reachable cycles in $\mathcal{A}_\sigma$ are non-negative in all dimensions. Thus, $\sigma$ ensures mean payoff at least equal to zero in all dimensions (for lim-inf and lim-sup variants).

In the opposite direction, assume that $\sigma$ is a finite-memory winning strategy for $\text{MeanPayoff}_{\ge 0}^-$ (or equivalently $\text{MeanPayoff}_{\ge 0}^+$). Using the same argument as before, we have that all cycles in $\mathcal{A}_\sigma$ are non-negative. Therefore there exists some initial credit $\vec{c}_0 \in \mathbb{N}^k$ such that $\sigma$ satisfies the energy objective. As a trivial bound, one may take initial credit $|V| \cdot |M| \cdot W$ in all dimensions, where $|V|$ is the number of vertices of $\mathcal{A}$, $|M|$ the number of memory states of $\mathcal{M}$, and $W$ is the largest absolute weight appearing in the arena: this quantity bounds the lowest sum of weights achievable under an acyclic path. $\square$

Observe that the finite-memory assumption is crucial to lift mean payoff winning strategies to the energy game. Intuitively, the reasoning would break for a strategy like the one used in Example 17 because the memory structure would need to be infinite and $\mathcal{A}_\sigma$ would actually not contain any cycle but an infinite path of ever-decreasing energy such that no bound on the initial credit could be established.

Also, note that Theorem 129 makes no mention of the specific variant of mean payoff used. This is because both players play using finite-memory: Eve by hypothesis and Adam thanks to the equivalence and Theorem 128. Hence, Proposition 11 applies. To sum up, we obtain the following.

**Corollary 22.** *Solving multidimensional mean payoff games under finite-memory is coNP-complete. Exponential-memory strategies suffice and are required for Eve, and memoryless ones suffice for Adam.*

### 12.2.2 Infinite memory

We now turn to the general case, where Eve is allowed to use infinite memory. By Example 18, we already know that lim-sup and lim-inf variants are not equivalent. We will cover the lim-sup case in details and end with a brief overview of the lim-inf one.

#### Lim-sup variant

Without loss of generality, we fix the objective $\text{MeanPayoff}_{\ge 0}^+$ (one can always modify the weights in the arena and consider the shifted-game with threshold zero). We have seen in Example 18 that Eve could focus on each dimension independently and alternatively in such a way that in the limit, she obtains the supremum in each dimension. This is the core idea that we will exploit.
**Lemma 139.** Let $\mathcal{A}$ be an arena such that from all vertex $v \in V$ and for all dimension $i$, $1 \le i \le k$, Eve has a winning strategy for $\{\pi \in \text{Paths}_\omega(G) \mid \text{MeanPayoff}_i^+(\pi) \ge 0\}$. Then, from all vertex $v \in V$, she has a winning strategy for $\text{MeanPayoff}_{\ge 0}^+(\pi)$.

Hence, being able to win in each dimension separately suffices to guarantee winning in all dimensions simultaneously. Note that the converse is obvious.

*Proof.* For each vertex $v \in V$ and dimension $i$, $1 \le i \le k$, let $\sigma_i^v$ be a winning strategy for Eve from $v$ for $\{\pi \in \text{Paths}_\omega(G) \mid \text{MeanPayoff}_i^+(\pi) \ge 0\}$.

Let $T_{\sigma_i^v}$ be the infinite tree obtained by unfolding $\sigma_i^v$: it represents all plays consistent with this strategy. Formally, such a tree is obtained inductively as follows:

* The root of the tree represents $v$.

* Given a node<fnref n="1" /> $\eta$ representing the branch (i.e., prefix of play) $\rho$ starting in vertex $v$ and ending in vertex $v_\eta$, we add children as follows:

- if $v_\eta \in V_{\text{Eve}}$, $\eta$ has a unique child representing the vertex $\text{Out}(e)$ reached through edge $e = \sigma_i^v(\rho)$;

- otherwise $\eta$ has one child for each possible successor of $v_\eta$, i.e., for each $\text{Out}(e)$ such that $e \in E$ and $\text{In}(e) = v_\eta$.

For $\varepsilon > 0$, we declare a node $\eta$ of $T_{\sigma_i^v}$ to be $\varepsilon$-good if the mean over dimension $i$ on the path from the root to $\eta$ is at least $-\varepsilon$ (as usual, we project this path to $C^\omega$ to evaluate it). For $\ell \in \mathbb{N}$, let $\hat{T}_{v,\varepsilon}^{\ell}$ be the tree obtained from $T_{\sigma_i^v}$ by removing all descendants of $\varepsilon$-good nodes that are at depth at least $\ell$: hence, all branches of $\hat{T}_{v,\varepsilon}^{\ell}$ have length at least $\ell$ and their leaves are $\varepsilon$-good.

We first show that $\hat{T}_{v,\varepsilon}^{\ell}$ is a finite tree. By König's Lemma [Kön36], we only need to show that every branch is finite. By contradiction, assume it is not the case and there exists some infinite branch. By construction, it implies that this branch contains no $\varepsilon$-good node after depth $\ell$. Thus, the corresponding play $\pi$, which is consistent with $\sigma_i^v$, necessarily has $\text{MeanPayoff}_i^+(\pi) \le -\varepsilon$. This contradicts the hypothesis that $\sigma_i^v$ is winning for dimension $i$. Hence the tree is indeed finite.

Based on these finite trees, we now build an infinite-memory strategy for Eve that will be winning for the conjunct objective $\text{MeanPayoff}_{\ge 0}^+(\pi)$: it is presented as Algorithm 12.1.

Recall that $W$ is the largest absolute weight in the game. Consider the situation whenever an iteration of the for-loop ends. Let $M$ be the number of steps the play followed $\sigma_i^v$ during this loop execution. Then, the mean payoff in dimension $i$ is at least $\frac{-LW-M\cdot\varepsilon}{L+M} \ge \frac{-LW-M\cdot\varepsilon}{M}$. Since $M \ge \frac{LW}{\varepsilon}$ by definition, we obtain that the mean payoff in dimension $i$ is at least $-2\cdot\varepsilon$.

Observe that since all trees are finite, we always exit the for-loop eventually, hence $\varepsilon$ tends to zero. Therefore, the supremum mean payoff is at least zero in all dimensions, which makes this strategy winning for $\text{MeanPayoff}_{\ge 0}^+(\pi)$. $\square$

<footnote n="1">¹Nodes refer to the tree, vertices to the arena.</footnote>
<table><caption>**Algorithm 12.1:** Winning strategy $\sigma$ for MeanPayoff$^{+}_{\ge 0}$</caption><tr><td>ε</td><td>←</td><td>1</td></tr><tr><td colspan="3">loop</td></tr><tr><td colspan="3">for i = 1 to k do</td></tr><tr><td colspan="3">Let v be the current vertex, L the length of the play so far</td></tr><tr><td colspan="3">l ← ⌊ L/W ⌋</td></tr><tr><td colspan="3">Play according to σ<sup>v</sup><sub>i</sub> until a leaf of T̂<sup>i,l</sup><sub>v,ε</sub> is reached</td></tr><tr><td colspan="3">ε ← ε/2</td></tr></table>

This construction is tight in the sense that infinite memory is needed for Eve, as previously proved. For Adam, we show a better situation. The proof scheme will also be the base of the upcoming algorithm.

**Lemma 140.** *Memoryless strategies suffice for Adam in multidimensional lim-sup mean payoff games.*

*Proof.* The proof works by induction on the number of vertices of the arena. The base case $|V| = 1$ is trivial. Assume the only vertex belongs to Adam. If there exists a self loop (recall we allow several edges per pair of vertices) which has a negative weight on some dimension, Adam wins by looping on it forever. In the opposite case, he cannot win.

Now assume $|V| \ge 2$. For $i \in \{1, \dots, k\}$, let $W^i_{Adam}$ be the winning region of Adam for the complement of $\{\pi \in \text{Paths}_\omega(G) \mid \text{MeanPayoff}_i^+(\pi) \ge 0\}$, i.e., the region where Adam has a strategy to force a strictly negative mean payoff in dimension $i$ (as studied in Chapter 4). Let $W^{\text{disj}}_{Adam} = \cup_{i=1}^k W^i_{Adam}$. We have two cases.

First, $W^{\text{disj}}_{Adam} = \emptyset$. Then, Eve can win all one-dimension games from everywhere and by Lemma 139, she can also win for $\text{MeanPayoff}_{\ge 0}^+$. Thus, Adam has no winning strategy.

Second, $W^{\text{disj}}_{Adam} \neq \emptyset$. Then, there exists $i \in \{1, \dots, k\}$ such that $W^i_{Adam} \neq \emptyset$. In this set, Adam has a memoryless winning strategy $\tau_i$ to falsify the winning condition $\{\pi \in \text{Paths}_\omega(G) \mid \text{MeanPayoff}_i^+(\pi) \ge 0\}$ (because one-dimension mean payoff games are memoryless determined, as proved in Corollary 6). This strategy also falsifies $\text{MeanPayoff}_{\ge 0}^+$, hence $W^i_{Adam}$ is part of the winning region for Adam — we denote it $W_{Adam}$, as usual. By prefix independence of the mean payoff, the attractor $W^i_{Adam} = \text{Attr}_{Adam}(W^i_{Adam})$ is also part of $W_{Adam}$. We denote by $\tau_{\text{Pre}}$ the corresponding attractor strategy of Adam. Moreover, the graph restricted to $V \setminus W^i_{Adam}^{\text{Pre}}$ constitutes a proper arena $\mathcal{A}'$.

Let $W'_{Adam}$ be the winning region of Adam in $\mathcal{A}'$ for the original winning condition $\text{MeanPayoff}_{\ge 0}^+$. The arena $\mathcal{A}'$ has strictly less vertices than $\mathcal{A}$ since we removed the non-empty region $W^i_{Adam}$. Hence we can apply the induction hypothesis: Adam has a memoryless winning strategy $\tau'$ in $W'_{Adam}$. The region $V \setminus (W^i_{Adam}^{\text{Pre}} \cup W'_{Adam})$ is winning for Eve in $\mathcal{A}'$ by determinacy. But it is also winning in $\mathcal{A}$, i.e., the original game, since
Adam cannot force the play to go in $W_{Adam}^{i,Pre}$ from there (otherwise it would be part of the attractor too).

We define the following memoryless strategy for Adam, which we claim is winning from $W_{Adam} = W_{Adam}^{i,Pre} \cup W'_{Adam}$:

$$ \tau(v) = \begin{cases} \tau_{Pre}(v) & \text{if } v \in W_{Adam}^{i,Pre} \setminus W_{Adam}^{i} \\ \tau_{i}(v) & \text{if } v \in W_{Adam}^{i} \\ \tau'(v) & \text{if } v \in W'_{Adam} \end{cases} $$

Since we already know that Eve wins from $V \setminus W_{Adam}$, it remains to prove that $\tau$ is winning from $W_{Adam}$ to conclude. Consider any play $\pi$ consistent with $\tau$ and starting in $W_{Adam}$. Two cases are possible. First, the play eventually reaches $W_{Adam}^{i}$ and Adam switches to $\tau_{i}$: then prefix independence of the mean payoff guarantees that Adam wins. Second, the play never reaches $W_{Adam}^{i}$: then $\pi$ necessarily stays in $\mathcal{A}'$, and $\tau'$ is winning from $W'_{Adam}$ in $\mathcal{A}'$. Therefore, $\tau$ does win from everywhere in $W_{Adam}$, while being memoryless, which ends the proof. $\square$

We use the core reasoning of this proof to build an algorithm solving multidimensional lim-sup mean payoff games (Algorithm 12.2). It uses as a black box a routine that computes (in pseudo-polynomial time) the winning vertices for Eve in one-dimension mean payoff games. This subalgorithm, presented in Section 4.3, is here dubbed SolveOneDimMeanPayoff, and takes as parameters the arena and the considered dimension.

<caption>**Algorithm 12.2:** Solver for multidimensional lim-sup mean payoff games</caption>

**Data:** Arena $\mathcal{A}$ with vertices $V$
**Result:** $W_{Eve}$, the winning region of Eve for MeanPayoff$_{\ge 0}^{+}$
$\mathcal{A}' \leftarrow \mathcal{A}$; $V' \leftarrow V$
**repeat**
| LosingVertices $\leftarrow$ false
| **for** $i = 1$ to $k$ **do**
| | $W_{Adam}^{i} \leftarrow V' \setminus SolveOneDimMeanPayoff(\mathcal{A}', i)$
| | **if** $W'_{Adam} \neq \emptyset$ **then**
| | | $V' \leftarrow V' \setminus W_{Adam}^{i}$
| | | $\mathcal{A}' \leftarrow \mathcal{A}'[V']$ /* Restriction of $\mathcal{A}'$ to $V'$ */
| | | LosingVertices $\leftarrow$ true
| | **until** LosingVertices = false
| | **return** $V'$

Intuitively, we iteratively remove vertices that are declared losing for Eve because Adam can win on some dimension from them. Since removing vertices based on some dimension $i$ may decrease the power of Eve and her ability to win for another dimension $i'$, we need the outer loop: in the end, we ensure that $V'$ contains exactly all the vertices from which Eve has a winning strategy for each dimension. By Lemma 139 and the proof of Lemma 140, we know that this is equal to $W_{Eve}$.
We recall (Section 1.7) that, given an arena $\mathcal{A}$ and a set of vertices $X$, $\mathcal{A}[X]$ denotes the subarena induced by $X$.

**Remark 24.** The restriction $\mathcal{A}'[V']$ induces a proper subarena. Indeed, we have that $W_{\text{Adam}}^i = \text{Attr}_{\text{Adam}}(W_{\text{Adam}}^i)$ since any vertex $v$ from which Adam can force to reach $W_{\text{Adam}}^i$ also belongs to $W_{\text{Adam}}^i$ by prefix independence of the mean payoff.

We wrap up with the following theorem.

**Theorem 130.** Solving multidimensional lim-sup mean payoff game is in NP $\cap$ coNP. Infinite-memory strategies are required for Eve and memoryless ones suffice for Adam. Furthermore, the winning regions can be computed in pseudo-polynomial time, through at most $|V| \cdot k$ calls to an algorithm solving one-dimension mean payoff games.

*Proof.* The correctness of Algorithm 12.2 follows from Lemma 139 and Lemma 140, and its complexity is trivial to assess, using SolveOneDimMeanPayoff as a pseudo-polynomial black-box. The memory bounds follow from Lemma 139, Lemma 140 and Theorem 127. Hence, only the NP $\cap$ coNP membership remains. Recall that the decision problem under study is: given an arena $\mathcal{A}$ and an initial vertex $v_0$, does $v_0$ belong to $W_{\text{Eve}}$ or not?

We first prove that the problem is in NP. A non-deterministic algorithm guesses the winning region $W_{\text{Eve}}$ containing $v_0$ and witness memoryless strategies $\sigma_i$ for all dimensions (we know that memoryless strategies suffice by Corollary 6). Then, it checks for every dimension $i$, for every vertex $v \in W_{\text{Eve}}$, that $\sigma_i$ is winning. This boils down to solving a polynomial number of one-player one-dimension mean payoff games for Adam over the arenas $\mathcal{A}_{\sigma_i}$ obtained by fixing $\sigma_i$.<fnref n="2" /> As noted in Section 4.3, it can be done in polynomial time using Karp's algorithm for finding the minimum cycle mean in a weighted digraph [Kar78]. By Lemma 139, we know that if the verification checks out, Eve has a winning strategy in $W_{\text{Eve}}$ for objective $\text{MeanPayoff}_{\ge 0}^+$.

Finally, we prove coNP membership. The algorithm guesses a memoryless winning strategy $\tau$ for Adam (from $v_0$). The verification then consists in checking that Eve has no winning strategy in the arena $\mathcal{A}_\tau$. This can be done using Algorithm 12.2, through $|V| \cdot k$ calls to SolveOneDimMeanPayoff. In this case however, such calls only need to solve one-player one-dimension mean payoff games for Eve, which again can be done in polynomial time, resorting to Karp's algorithm. Thus, the verification takes polynomial time in total, and coNP membership follows. $\square$

## Lim-inf variant

For the sake of conciseness, we give only a brief sketch. Without loss of generality, we fix the objective $\text{MeanPayoff}_{\ge 0}^-$.

**Lemma 141.** Memoryless strategies suffice for Adam in multidimensional lim-inf mean payoff games.

<footnote n="2">²The arena $\mathcal{A}_\sigma$ induced by applying a strategy $\sigma$ on arena $\mathcal{A}$ can be obtained through the product $\mathcal{A} \times \mathcal{M}$, with $\mathcal{M}$ the memory structure of $\sigma$, as presented in Section 1.6.</footnote>
Sketch. We mention the sketch as it is interesting in its own right. Recall that Chap-
ter 4 presented a general recipe, due to Gimbert and Zielonka [GZ04, GZ05], to prove
memoryless determinacy. Clearly, such a recipe cannot work here due to Theorem 127.
Still, a similar result by Kopczyński deals with half-positional determinacy [Kop06].
This new recipe states that if the objective of Eve is both prefix independent and convex,
then memoryless strategies suffice for Adam. We already know that $\text{MeanPayoff}_{\ge 0}^-$ is
prefix independent. An objective is said to be convex if it is closed under combinations
(shuffling): if two infinite sequences of colours $\pi = \rho_1\rho_2\dots$ and $\pi' = \rho'_1\rho'_2\dots$, with all
$\rho_i$, $\rho'_i$ being finite prefixes, belong to the objective, then $\pi'' = \rho_1\rho'_1\rho_2\rho'_2\dots$ does too.
Conjunctions of lim-inf mean payoff are convex, hence the result applies here. Note
that this approach corresponds to the one presented in Theorem 16: submixing objec-
tives are also called concave, and Eve's objective being convex implies that Adam's
objective is concave; hence the reasoning above.
□

**Remark 25.** Lim-sup mean payoff objectives are not convex, hence the ad-hoc proof in Lemma 140. Consider the integer sequence $\pi = (2)^{50}(-4)^{51}(2)^{52}(-4)^{53}\dots$ where the length of the i-th sequence of numbers is $5^{i-1}$. One can prove that at the end of each sequence of 2's (resp. $-4$'s), the mean is above (and tends to) 1 (resp. is exactly $-3$). Let $\pi'$ be the sequence obtained by swapping all 2's and $-4$'s. We have $\text{MeanPayoff}^{+}(\pi) = \text{MeanPayoff}^{+}(\pi') \ge 1$, hence $\pi, \pi' \in \text{MeanPayoff}_{\ge 0}^{+}$.

Still, by shuffling $\pi$ and $\pi'$ in one-one alternation, we build $\pi'' = 2, -4, 2, -4, \dots$, which is such that $\text{MeanPayoff}^{+}(\pi'') = -1$, hence $\pi'' \notin \text{MeanPayoff}_{\ge 0}^{+}$. Hence lim-sup mean payoff is not convex.

Complexity-wise, multidimensional lim-inf mean payoff games look a lot like mul-
tidimensional energy games, even though we proved they are not equivalent without
memory restrictions.

**Theorem 131.** *Solving multidimensional lim-inf mean payoff games is coNP-complete. Infinite-memory strategies are required for Eve and memoryless ones suffice for Adam.*

We discussed memory through Example 17 and Lemma 141. The coNP-hardness
can be shown through a reduction from 3UNSAT similar to the one used for existen-
tial initial credit multidimensional energy games in Section 11.5. The matching upper
bound relies on memoryless strategies being sufficient for Adam, and the capacity to
solve one-player instances of multidimensional lim-inf mean payoff games in poly-
nomial time. The latter problem is addressed by reduction to detecting non-negative
multi-cycles in graphs (which can be done in polynomial time based on [KS88]).

Wrap-up

We have seen that multidimensional mean payoff games and multidimensional energy
games behave relatively well. Sure, infinite memory is needed for Eve in general for
the former, but complexity-wise, the gap with one-dimension games is small and even
non-existent for the lim-sup variant. Furthermore, if we are interested in finite-memory
strategies, the equivalence with energy games is preserved. Hence, we may say that
both mean payoff and energy games hold up nicely in the multidimensional world.
12.3 Total payoff and shortest path

In this section, we turn to two other objectives deeply studied in Chapter 4: we study
total payoff and shortest path games. We will see that the multidimensional setting has
dire consequences for both.

12.3.1 Total payoff vs. mean payoff

We start with total payoff games. As for the mean payoff, we explicitly consider the two
variants, TotalPayoff⁺ and TotalPayoff⁻, for the lim-sup and lim-inf definitions
respectively. While Chapter 4 was written using the lim-sup variant, all results are
identical for the lim-inf one in one-dimension games [GS09a].

Recall that one-dimension total payoff games are memoryless determined and solving them is in NP ∩ coNP (even in UP ∩ coUP [GS09a]). Furthermore, Chapter 4 taught us that total payoff can be seen as a *refinement* of mean payoff, as it permits to reason about low (using the lim-inf variant) and high (using the lim-sup one) points of partial sums along a play when the mean payoff is zero. We formalize this relationship in the next lemma, and study what happens in multiple dimensions.

**Lemma 142.** *Fix an arena *A* and an initial vertex *v*₀ ∈ *V*. Let *A*, *B*, *C* and *D* denote the following assertions.*

A. Eve has a winning strategy for MeanPayoff_{≥0}⁺.

B. Eve has a winning strategy for $\text{MeanPayoff}_{\ge 0}^{-}$.

C. There exists $\vec{x} \in \mathbb{Q}^k$ such that Eve has a winning strategy for $\text{TotalPayoff}_{\ge \vec{x}}^{-}$.

D. There exists $\vec{x} \in \mathbb{Q}^k$ such that Eve has a winning strategy for $\text{TotalPayoff}_{\ge \vec{x}}^+$.

In one-dimension games ($k = 1$), all four assertions are equivalent. In multidimensional ones ($k > 1$), the only implications that hold are: $C \implies D \implies A$ and $C \implies B \implies A$. All other implications are false in general.

Lemma 142 is depicted in Figure 12.2: the only implications that carry over to
multiple dimensions are depicted by solid arrows.

<figure><img src="image_104.png" /><figcaption>Figure 12.2: Equivalence between mean payoff and total payoff games. Dashed implications are only valid in one-dimension games. We use $\sigma \models \Omega$ as a shortcut for '$\sigma$ is winning from $v_0$ for $\Omega$'.</figcaption></figure>
*Proof.* The implications that remain true in multiple dimensions are the trivial ones. First, satisfaction of the lim-inf version of a given objective clearly implies satisfaction of its lim-sup version by definition. Hence, $B \implies A$ and $C \implies D$. Second, consider a play $\pi \in \text{TotalPayoff}_{\ge \vec{x}}^{-}$ (resp. $\text{TotalPayoff}_{\ge \vec{x}}^{+}$) for some $\vec{x} \in \mathbb{Q}^{k}$. For all dimension $i \in \{1, \dots, k\}$, the corresponding sequence of mean payoff infima (resp. suprema) over prefixes can be *lower-bounded* by a sequence of elements of the form $\frac{\vec{x}_i}{\ell}$ with $\ell$ the length of the prefix. We can do this because the sequence of total payoffs over prefixes is a sequence of integers: it always achieves the value of its limit $\vec{x}_i$ instead of only tending to it asymptotically as could a sequence of rationals (such as the mean pay-offs). Since $\frac{\vec{x}_i}{\ell}$ tends to zero over an infinite play, we do have that $\pi \in \text{MeanPayoff}_{\ge 0}^{-}$ (resp. $\text{MeanPayoff}_{\ge 0}^{+}$). Thus, $C \implies B$ and $D \implies A$. Along with the transitive closure $C \implies A$, these are all the implications preserved in multidimensional games.

In one-dimension games, all assertions are equivalent. As seen before, lim-inf and lim-sup mean payoff games coincide as memoryless strategies suffice for both players. Thus, we add $A \implies B$ and $D \implies B$ by transitivity. Second, consider a memoryless (w.l.o.g.) strategy $\sigma_B$ for Eve for $\text{MeanPayoff}_{\ge 0}^{-}$. Let $\pi$ be any consistent play. Then all cycles in $\pi$ are non-negative, otherwise Eve cannot ensure winning with $\sigma_B$ (because Adam could pump the negative cycle). Thus, the sum of weights along $\pi$ is at all times bounded from below by $-(|V|-1) \cdot W$ (for the longest acyclic prefix), with $W$ the largest absolute weight, as usual. Therefore, we have $B \implies C$, and we obtain all other implications by transitive closure.

For multidimensional games, all dashed implications are false.

1. To show that implication $D \implies B$ does not hold, consider the Eve-owned one-player game where $V = \{v\}$ and the only edges are two self loops of weights $(1, -2)$ and $(-2, 1)$. Clearly, any finite vector $\vec{x} \in \mathbb{Q}^2$ for $\text{TotalPayoff}_{\ge \vec{x}}^{+}$ can be achieved by an infinite-memory strategy consisting in playing both loops successively for longer and longer periods, each time switching after getting back above threshold $\vec{x}$ in the considered dimension. However, it is impossible to build any strategy, even with infinite memory, that satisfies $\text{MeanPayoff}_{\ge 0}^{-}$ as the lim-inf mean payoff would be at best a linear combination of the two cycle values, i.e., strictly less than zero in at least one dimension in any case.

2. Lastly, consider the game in Figure 12.1 where we modify the weights to add a third dimension with value 0 on the self loops and -1 on the other edges. As already proved, the strategy that plays for $\ell$ steps in the left cycle, then goes for $\ell$ steps in the right one, then repeats for $\ell' > \ell$ and so on, is a winning strategy for $\text{MeanPayoff}_{\ge 0}^{-}$. Nevertheless, for any strategy of Eve, the play is such that either (i) it only switches between $v_0$ and $v_1$ a finite number of times, in which case the sum in dimension 1 or 2 decreases to infinity from some point on; or (ii) it switches infinitely often and the sum in dimension 3 decreases to infinity. In both cases, objective $\text{TotalPayoff}_{\ge \vec{x}}^{+}$ is not satisfied for any vector $\vec{x} \in \mathbb{Q}^3$. Hence, $B \implies D$ is falsified.

We only need to consider these two cases: all other dashed implications are false as they would otherwise contradict the last two cases by transitivity. $\square$
We see that the relationship between mean payoff and total payoff games breaks in multiple dimensions. Nonetheless, one may still hope for good properties for the latter, as one-dimension total payoff games are in NP∩coNP (Section 4.6). This hope, however, will not last long.

### 12.3.2 Undecidability

In contrast to mean payoff games, total payoff ones become undecidable in multiple dimensions.

**Theorem 132.** Total payoff games are undecidable in any dimension $k \ge 5$.

*Proof.* We use a reduction from two-dimensional robot games [NPR16], which were mentioned in Chapter 11. They are a restricted case of configuration reachability vector games, recently proved to be already undecidable. Using the formalism of Chapter 11, they are expressible as follows: $\mathcal{V} = (\mathcal{L} = \{\ell_0, \ell_1\}, A, \mathcal{L}_{\text{Eve}} = \{\ell_0\}, \mathcal{L}_{\text{Adam}} = \{\ell_1\})$ and $A \subseteq \mathcal{L} \times [-M, M]^2 \times \mathcal{L}$ for some $M \in \mathbb{N}$. The game starts in configuration $\ell_0(x_0, y_0)$ for some $x_0, y_0 \in \mathbb{Z}$ and the goal of Eve is to reach configuration $\ell_0(0, 0)$: solving such a game is undecidable.

The reduction is as follows. Given a robot game $\mathcal{V}$, we build a five-dimension total payoff game $\mathcal{G}$ such that Eve wins in $\mathcal{G}$ if and only if she wins in $\mathcal{V}$. Let $\mathcal{G} = (\mathcal{A}, \text{TotalPayoff}^{+}_{\ge 0})$ (we will discuss the lim-inf case later), where arena $\mathcal{A}$ has vertices $V = V_{\text{Eve}} \uplus V_{\text{Adam}}$ with $V_{\text{Eve}} = \{v_{\text{init}}, v_0, v_{\text{stop}}\}$ and $V_{\text{Adam}} = \{v_1\}$, and $E$ is built as follows:

* if $(\ell_i, (a, b), \ell_j) \in A$, then $(v_i, (a, -a, b, -b, 0), v_j) \in E$,

* $(v_0, (0, 0, 0, 0, 1), v_{\text{stop}}) \in E$ and $(v_{\text{stop}}, (0, 0, 0, 0, 0), v_{\text{stop}}) \in E$,

* $(v_{\text{init}}, (x_0, -x_0, y_0, -y_0, -1), v_0) \in E$ (where $(x_0, y_0)$ is the initial credit in $\mathcal{V}$).

The initial vertex is $v_{\text{init}}$. Intuitively, dimensions 1 and 2 (resp. 3 and 4) encode the value of the first counter (resp. second counter) and its opposite at all times. The initial credit is encoded thanks to the initial edge, then the game is played as in the vector game, with the exception that Eve may branch from $v_0$ to the absorbing vertex $v_{\text{stop}}$, which has a zero self loop. The role of the last dimension is to force Eve to branch eventually (if she aims to win).

We proceed to prove the correctness of the reduction. First, let $\sigma_g$ be a winning strategy of Eve in $\mathcal{G}$. We claim that Eve can also win in $\mathcal{V}$. Any play $\pi$ consistent with $\sigma_g$ necessarily ends in $v_{\text{stop}}$: otherwise its lim-sup total payoff on the last dimension would be $-1$ (as the sum always stays at $-1$). Due to the branching edge and the self loop having weight zero in all first four dimensions, we also have that the current sum on these dimensions must be non-negative when branching, otherwise the total payoff objective would be falsified. By construction of $\mathcal{A}$, the only way to achieve this is to have a sum exactly equal to zero in all first four dimensions (as dimensions 1 and 2 are opposite at all times and so are 3 and 4). Finally, observe that obtaining a partial sum of $(0, 0, 0, 0, -1)$ in $v_0$ is equivalent to reaching configuration $\ell_0(0, 0)$ in $\mathcal{V}$. Hence, we can easily build a strategy $\sigma_\mathcal{V}$ in $\mathcal{V}$ that mimics $\sigma_g$ in order to win
the robot game. This strategy $\sigma_Y$ could in general use arbitrary memory (since we start with an arbitrary winning strategy $\sigma_Q$) while formally robot games as defined in [NPR16] only allow strategies to look at the current configuration. Still, from $\sigma_Y$, one can easily build a corresponding strategy that meets this restriction ($\mathcal{V}$ being a configuration reachability game, there is no reason to choose different actions in two visits of the same configuration). Hence, if Eve wins in $\mathcal{G}$, she also wins in $\mathcal{V}$.

For the other direction, from a winning strategy $\sigma_Y$ in $\mathcal{V}$, we can similarly define a strategy $\sigma_Q$ that mimics it in $\mathcal{G}$ to reach $v_0$ with partial sum $(0,0,0,0,-1)$, and at that point, branches to $v_{\text{stop}}$. Such a strategy ensures reaching the absorbing vertex with a total payoff of zero in all dimensions, hence is winning in $\mathcal{G}$.

Thus, the reduction holds for lim-sup total payoff. Observe that the exact same reasoning holds for the lim-inf variant. Indeed, the last dimension is always $-1$ outside of $v_{\text{stop}}$, hence any play not entering $v_{\text{stop}}$ also has its lim-inf below zero in this dimension. Furthermore, once $v_{\text{stop}}$ is entered, the sum in all dimensions stays constant, hence the limit exists and both variants coincide. $\square$

An almost identical reduction can be used for shortest path games.

**Theorem 133.** Shortest path games are undecidable in any dimension $k \ge 4$.

**Remark 26.** For the sake of consistency, we use the convention established in Section 4.5: the shortest path payoff takes the opposite of the sum of weights along a path and Eve aims to maximise it (which is equivalent to minimising this sum in the natural interpretation of the shortest path objective). Hence, paths not reaching the target are assigned payoff $-\infty$.

*Proof.* The proof is almost identical to the last one. We use objective ShortestPath$_{\ge 0}$ with target edge $(v_{\text{stop}}, (0,0,0,0), v_{\text{stop}})$ and drop the last dimension in arena $\mathcal{A}$: it is now unnecessary as the shortest path objective by definition will force Eve to branch to $v_{\text{stop}}$, as otherwise the value of the play would be $-\infty$ in all dimensions. The rest of the reasoning is the same as before. $\square$

**Remark 27.** The decidability of total payoff games with $k \in \{2,3,4\}$ dimensions and shortest path games with $k \in \{2,3\}$ dimensions remains an open question. Furthermore, our undecidability results crucially rely on weights being in $\mathbb{Z}$: they do not hold when we restrict weights to $\mathbb{N}$.

## Memory

Let us go back to the game used in Item 1 in the proof of Lemma 142: we have seen that for any threshold $\vec{x} \in \mathbb{Q}^2$, Eve has an infinite-memory strategy that is winning for TotalPayoff$_{\ge \vec{x}}$. In other words, she can ensure an arbitrarily high total payoff with infinite memory. Yet, it is easy to check that there exists no finite-memory strategy of Eve that can achieve a finite threshold vector in the very same game: alternating would still be needed, but the negative amount to compensate grows boundlessly with each alternation, thus no amount of finite memory can ensure to go above the threshold infinitely often. This simple game highlights a huge gap between finite and infinite memory: with finite memory, the total payoff on at least one dimension is $-\infty$; with
infinite memory, the total payoff in both dimensions may be as high as Eve wants. This further highlights the untameable behaviour of multidimensional total payoff games.

### Wrap-up

Multiple dimensions are a curse for total payoff and shortest path games as both become undecidable. This is in stark contrast to mean payoff and energy games, which remain tractable, as seen in Section 12.2. The bottom line is that most of the equiva- lences, relationships, and well-known behaviours of one-dimension games simply fall apart when lifting them to multiple dimensions.

## 12.4 Beyond worst-case synthesis

We now turn to a completely different meaning of *multi-objective*. Let us take a few steps back. Throughout this book, we have studied two types of interaction between players: rational, antagonistic interaction between Eve and Adam; and stochastic inter- action with a random player. Consider the quantitative settings of Chapter 4 and Chap- ter 5. In the zero-sum two-player games of the former, Adam is seen as a *purely antagonistic adversary*, so the goal of Eve is to ensure strict *worst-case guarantees*, i.e., a minimal performance level against all possible strategies of Adam. In the MDPs of the latter, Eve interacts with randomness (through actions or random vertices) and she wants to ensure a good *expected value* for the considered payoff.

For most objectives, these two paradigms yield elegant and simple solutions: e.g., memoryless strategies suffice for both games and MDPs with a mean payoff objective. Nevertheless, the corresponding strategies have clear weaknesses: strategies that are good for the worst-case may exhibit suboptimal behaviours in probable situations while strategies that are good for the expected value may be terrible in some unlikely but possible situations. A natural question, of theoretical and practical interest, is to build — * synthesize* — strategies that combine both paradigms: strategies that both ensure (a) some worst-case threshold no matter how the adversary behaves (i.e., against any arbitrary strategy) and (b) a good expectation against the expected behaviour of the adversary (given as a stochastic model). We call this task *beyond worst-case synthesis*.

The goal of this section is to illustrate the complexity of beyond worst-case synthesis and how it requires fine-tuned interaction between the worst-case and average-case aspects. To that end, we focus on a specific case: the synthesis of *finite-memory strategies* for beyond worst-case *mean payoff* objectives. Due to the highly technical nature of this approach, we will not present all its details, but rather paint in broad strokes its cornerstones. We hope to give the reader sufficient intuition and understanding to develop a clear view of the challenges arising from rich behavioural models, and some of the techniques that come to the rescue.

### 12.4.1 The decision problem

Our goal is to mix the games of Chapter 4 and the MDPs of Chapter 5, so we need to go back and forth between these models.
**Two-player game.** As before, we start with an arena $\mathcal{A} = (G = (V, E), V_{\text{Eve}}, V_{\text{Adam}})$, where the vertices are split between Eve's and Adam's. This arena represents the antagonistic interaction between Eve and Adam, so we consider a worst-case constraint on the corresponding game. We study a single mean payoff function, so our colouring is $c: E \to \mathbb{Z}$. Let $\alpha \in \mathbb{Q}$ be the worst-case threshold: we are looking for a strategy of Eve that is winning for objective $\text{MeanPayoff}_{>\alpha}^-$. Two things to note: first, we consider the lim-inf variant w.l.o.g. as we focus on *finite-memory* strategies (recall Proposition 11); second, we use a strict inequality as it will ease the formulation of the upcoming results.

**Markov decision process.** To make the connection with MDPs, we fix a finite-memory randomised strategy for Adam in the arena $\mathcal{A}$, $\tau^{\text{st}}$. Recall that a randomised strategy is a function $\text{Paths}(G) \to \mathcal{D}(E)$, where $\mathcal{D}(E)$ denotes the set of all probability distributions over $E$. As usual, we may build $\mathcal{A}_{\tau^{\text{st}}}$, the product of the arena $\mathcal{A}$ with the memory structure of $\tau^{\text{st}}$, restricted to the choices made by $\tau^{\text{st}}$. Since $\tau^{\text{st}}$ is assumed to be stochastic, what we obtain is not a one-player game for Eve, but an MDP.

To understand this relationship, it is easier to consider the alternative — and equivalent — formalism of MDPs, based on random vertices (as used for stochastic games in Chapter 6). Assume for instance that $\tau^{\text{st}}$ is a randomised memoryless strategy, i.e., a function $V_{\text{Adam}} \to \mathcal{D}(E)$. Then, the MDP $\mathcal{A}_{\tau^{\text{st}}}$ is immediately obtained by replacing each Adam's vertex $v$ by a random vertex such that $\delta(v) = \tau^{\text{st}}(v)$, i.e., the probabilistic transition function uses the same probability distributions as Adam's strategy. For example, we build the MDP $\mathcal{P} = \mathcal{A}_{\tau^{\text{st}}} = (G, V_{\text{Eve}}, V_{\text{Rand}} = V_{\text{Adam}}, \delta = \tau^{\text{st}})$.

In contrast to Chapter 6, we explicitly allow the transition function to assign probability zero to some edges of the underlying graph $G$, i.e., the support of $\delta(v)$ in some vertex $v \in V_{\text{Rand}}$ might not include all edges $e \in E$ such that $\text{In}(e) = v$. This is important as far as modelling is concerned, as in our context, transition functions will be defined according to a stochastic model for Adam, and we cannot reasonably assume that such a model always involves all the possible actions of Adam. Consequently, given the MDP $\mathcal{P}$, we define the subset of edges $E_{\delta} = \{e \in E \mid \text{In}(e) \in V_{\text{Rand}} \implies \delta(\text{In}(e))(e) > 0\}$, representing all edges that either start in a vertex of Eve, or are chosen with non-zero probability by the transition function $\delta$. Edges in $E \setminus E_{\delta}$ will only matter in the two-player game interpretation, whereas all MDP-related concepts, such as end-components, are defined with regard to edges in $E_{\delta}$ exclusively.

**Beyond worst-case problem.** Let us sum up the situation: we have a two-player arena $\mathcal{A}$ with a mean payoff objective $\text{MeanPayoff}_{>\alpha}^-$ and a finite-memory stochastic model for Adam yielding the MDP $\mathcal{A}_{\tau^{\text{st}}}$. Now, let $\beta \in \mathbb{Q}$ be the expected value threshold we want to ensure in the MDP (i.e., on average against the stochastic model of Adam).

**Problem 19 (Beyond worst-case mean payoff problem).**

**INPUT:** An arena $\mathcal{A}$, a finite-memory stochastic model $\tau^{\text{st}}$, an initial vertex $v_0$, two thresholds $\alpha, \beta \in \mathbb{Q}$

**OUTPUT:** Does Eve have a finite-memory strategy $\sigma$ such that $\sigma$ is winning for objective $\text{MeanPayoff}_{>\alpha}^-$ from $v_0$ in $\mathcal{A}$ and $\mathbb{E}_{\mathcal{A}_{\tau^{\text{st}}}, v_0}^\sigma[\text{MeanPayoff}^-] > \beta$?
We assume $\beta > \alpha$, otherwise the problem trivially reduces to the classical worst-case analysis: if all plays consistent with $\sigma$ have mean payoff greater than $\alpha \ge \beta$ then the expected value is also greater than $\alpha$ — and thus greater than $\beta$ — regardless of the stochastic model.

## 12.4.2 The approach in a nutshell

We present our solution to the beyond worst-case (BWC) problem in Algorithm 12.3. We give an intuitive sketch of its functioning in the following, and illustrate it on a toy example.

### Inputs and outputs

The algorithm takes as input: an arena $\mathcal{A}^\text{in}$ and its (integer) colouring $c^\text{in}$, a finite-memory stochastic model of Adam $\tau^\text{in}$, a worst-case threshold $\alpha^\text{in}$, an expected value threshold $\beta^\text{in}$, and an initial vertex $v_0^\text{in}$. Its output is YES if and only if there exists a finite-memory strategy of Eve satisfying the BWC problem.

The output as described in Algorithm 12.3 is Boolean: the algorithm answers whether a satisfying strategy exists or not, but does not explicitly construct it (to avoid tedious formalization within the pseudocode). Nevertheless, we sketch the synthesis process in the following and we highlight the role of each step of the algorithm in the construction of a winning strategy, as producing a witness winning strategy is a straightforward by-product of the process we apply to decide satisfaction of the BWC problem.

### Preprocessing

The first part of the algorithm is dedicated to the preprocessing of the arena $\mathcal{A}^\text{in}$ and the stochastic model $\tau^\text{in}$ given as inputs in order to apply the second part of the algorithm on a modified arena $\mathcal{A}$ and stochastic model $\tau^\text{st}$, simpler to manipulate. We show in the following that the answer to the BWC problem on the modified arena is YES if and only if it is also YES on the input arena, and we present how a winning strategy of Eve in $\mathcal{A}$ can be transferred to a winning strategy in $\mathcal{A}^\text{in}$.

The preprocessing is composed of four main steps. First, we modify the colouring function $c^\text{in}$ in order to consider the equivalent BWC problem with thresholds $(0, \beta)$ instead of $(\alpha^\text{in}, \beta^\text{in})$. This classical trick is used to get rid of explicitly considering the worst-case threshold in the following, as it is equal to zero.

Second, observe that any strategy that is winning for the BWC problem must also be winning for the classical worst-case problem, as solved in the two-player games of Chapter 4. Such a strategy cannot allow visits of any vertex from which Eve cannot ensure winning against an antagonistic adversary because mean payoff is a prefix independent objective (hence it is not possible to 'win' it over the finite prefix up to such a vertex). Thus, we reduce our study to $\mathcal{A}^\text{w}$, the subarena induced by Eve's worst-case winning vertices — which we compute in pseudo-polynomial time thanks to SolveWorstCaseMeanPayoff($\mathcal{A}^\text{in}, c^\text{P}$) (implementing the algorithm of Section 4.3). Note that we use the modified colouring and that $\mathcal{A}^\text{w}$ is a proper arena (same argument
<caption>**Algorithm 12.3:** Solver for the beyond worst-case mean payoff problem</caption>

**Data:** Arena $\mathcal{A}^{\text{in}} = (G^{\text{in}} = (V^{\text{in}}, E^{\text{in}}), V_{\text{Eve}}^{\text{in}}, V_{\text{Adam}}^{\text{in}})$, colouring $c^{\text{in}}: E^{\text{in}} \to \mathbb{Z}$, finite-memory stochastic model $\tau^{\text{in}}$ for Adam with memory structure $\mathcal{M}$ and initial memory state $m_0$, worst-case and expected value thresholds $\alpha^{\text{in}} = a/b, \beta^{\text{in}} \in \mathbb{Q}, \alpha^{\text{in}} < \beta^{\text{in}}$, initial vertex $v_0^{\text{in}} \in V^{\text{in}}$

**Result:** YES if and only if Eve has a finite-memory strategy $\sigma$ for the BWC problem from $v_0^{\text{in}}$ for thresholds pair $(\alpha^{\text{in}}, \beta^{\text{in}})$

/* Preprocessing */
if $\alpha^{\text{in}} \neq 0$ then
  Modify the colouring: $\forall e \in E^{\text{in}}, c^{\text{P}}(e) \leftarrow b \cdot c^{\text{in}}(e) - a$
  Consider the new thresholds pair $(0, \beta \leftarrow b \cdot \beta^{\text{in}} - a)$
else
  $c^{\text{P}} \leftarrow c^{\text{in}}$
  $V_{\text{wc}} \leftarrow \text{SolveWorstCaseMeanPayoff}(\mathcal{A}^{\text{in}}, c^{\text{P}})$
  if $v_0^{\text{in}} \notin V_{\text{wc}}$ then
    $\text{return}$ NO
else
  $\mathcal{A}^{\text{w}} \leftarrow \mathcal{A}^{\text{in}}[V_{\text{wc}}]$ /* Restriction of $\mathcal{A}^{\text{in}}$ to $V_{\text{wc}}$ */
  Let $\mathcal{A} \leftarrow \mathcal{A}^{\text{w}} \times \mathcal{M} = (G = (V, E), V_{\text{Eve}}, V_{\text{Adam}})$ be the arena obtained by product with the memory structure of Adam's stochastic model $\tau^{\text{in}}$
  Let $v_0 \leftarrow (v_0^{\text{in}}, m_0)$ be the corresponding initial vertex in $\mathcal{A}$
  Let $c$ be the transcription of $c^{\text{P}}$ in $\mathcal{A}$ such that $e = (v, m) \to (v', m')$ has colour $c(e) = c$ iff $v \xrightarrow{c} v'$ in $\mathcal{A}^{\text{w}}$ according to $c^{\text{P}}$
  Let $\tau^{\text{st}}$ be the memoryless transcription of $\tau^{\text{in}}$ on $\mathcal{A}$
  Let $\mathcal{P} \leftarrow \mathcal{A}_{\tau^{\text{st}}} = (G, V_{\text{Eve}}, V_{\text{Rand}} = V_{\text{Adam}}, \delta = \tau^{\text{st}})$ be the corresponding MDP
  /* Random vertices formalism */
/* Main algorithm */
Compute $\mathcal{U}_w$ the set of maximal winning end components of $\mathcal{P}$
Modify the colouring:
  $\forall e \in E, c'(e) \leftarrow \begin{cases} c(e) & \text{if } \exists U \in \mathcal{U}_w \text{ s.t. } \{\text{In}(e), \text{Out}(e)\} \subseteq U \\ 0 & \text{otherwise} \end{cases}$
Compute the maximal expected value $\beta^*$ from $v_0$ in $\mathcal{P}$ using $c'$
if $\beta^* > \beta$ then
  $\text{return}$ YES
else
  $\text{return}$ NO

as Remark 24). Obviously, if from the initial vertex $v_0^{\text{in}}$, Eve cannot win the worst-case problem, then the answer to the BWC problem is NO.

Third, we build arena $\mathcal{A}$, the product of $\mathcal{A}^{\text{w}}$ and the memory structure of Adam's stochastic model $\tau^{\text{in}}$. Intuitively, we expand the initial arena by integrating the memory
elements in the graph. Note that this does not modify the power of Adam in the two-
player interpretation of the arena.

Fourth, the finite-memory stochastic model $\tau^{\text{in}}$ on $\mathcal{A}^{\text{in}}$ clearly translates to a memoryless stochastic model $\tau^{\text{st}}$ on $\mathcal{A}$. This will help us obtain elegant proofs for the second part of the algorithm.

<figure><img src="image_105.png" /><figcaption>Figure 12.3: Beyond worst-case mean payoff problem: $U_2$ and $U_3$ are maximal winning end components, $U_1$ is losing.</figcaption></figure>

**Example 19.** In order to illustrate several notions and strategies, we will consider the arena depicted in Figure 12.3 throughout our presentation. The stochastic model of Adam is memoryless and is described by the probabilities written close to the start of outgoing edges. The colouring (weights) is written besides them.

We consider the BWC problem with the worst-case threshold $\alpha = 0$. Observe that this arena satisfies the assumptions guaranteed at the end of the preprocessing part of the algorithm. That is, the worst-case threshold is zero, a worst-case winning strategy of Eve exists in all vertices (e.g., the memoryless strategy choosing edges $(v_1, v_9)$, $(v_3, v_5)$, $(v_6, v_9)$, $(v_9, v_{10})$ and $(v_{10}, v_9)$ in their respective starting vertices), and the stochastic model is memoryless, as explained above.

Analysis of end components

The second part hence operates on an arena $\mathcal{A}$ such that from all vertices, Eve has a strategy to achieve a strictly positive mean payoff value (recall that $\alpha = 0$). We consider the MDP $\mathcal{P} = \mathcal{A}_{\tau^{\text{st}}}$ and notice that the underlying graphs of $\mathcal{A}$ and $\mathcal{P}$ are the same thanks to $\tau^{\text{st}}$ being memoryless. The following steps rely on the analysis of end components (ECs) in the MDP, i.e., strongly connected subgraphs in which Eve can ensure to stay when playing against Adam's stochastic model (Definition 14).
The motivation to the analysis of ECs is the following. It is well-known that under any arbitrary strategy $\sigma$ of Eve in $\mathcal{P}$, the probability that vertices visited infinitely often along a play constitute an EC is one (Lemma 69). Recall that the mean payoff is prefix independent, therefore the value of any play only depends on those colours that are seen infinitely often. Hence, the expected mean payoff $\mathbb{E}_{\mathcal{P},v_0} [\text{MeanPayoff}^-]$ depends uniquely on the value obtained in the ECs. Inside an EC, we can compute the maximal expected value that can be achieved by Eve, and this value is the same in all vertices of the EC, as established in Theorem 63.

Consequently, in order to satisfy the expected value requirement, an acceptable strategy for the BWC problem has to favor reaching ECs with a sufficient expectation, but under the constraint that it should also ensure satisfaction of the worst-case requirement. As we show in the following, this constraint implies that some ECs with high expected values may still need to be avoided because they do not permit to guarantee the worst-case requirement. This is the cornerstone of the classification of ECs that follows.

## Classification of end components

Let $\mathcal{E} \subseteq 2^V$ denote the set of all ECs in $\mathcal{P}$. Notice that by definition, only edges in $E_\delta$, as defined earlier, are involved to determine which sets of vertices form an EC in $\mathcal{P}$. As such, for any EC $U \in \mathcal{E}$, there may exist edges from $E \setminus E_\delta$ starting in $U$, such that Adam can force leaving $U$ when using an arbitrary strategy in $\mathcal{A}$. Still these edges will never be used by the stochastic model $\tau^{\text{st}}$. This remark will be important to the definition of strategies of Eve that guarantee the worst-case requirement, as Eve needs to be able to react to the hypothetical use of such an edge. We will see that it is also the case inside an EC.

Now, we want to consider the ECs in which Eve can ensure that the worst-case requirement will be fulfilled (i.e., without having to leave the EC): we call them *winning* ECs (WECs). The others will need to be eventually avoided, hence will have zero impact on the expectation of a finite-memory strategy satisfying the BWC problem. So we call the latter *losing* ECs (LECs). The subtlety of this classification is that it involves considering the ECs both in the MDP $\mathcal{P}$, and in the arena $\mathcal{A}$.

Formally, let $U \in \mathcal{E}$ be an EC. It is *winning* if, in the subarena induced by $U$, from all vertices, Eve has a strategy to ensure a *strictly positive* mean payoff against any strategy of Adam *that only chooses edges which are assigned non-zero probability by* $\tau^{\text{st}}$, or equivalently, edges in $E_\delta$. This can be interpreted as looking at arena $\mathcal{A}_\delta$, which is the restriction of $\mathcal{A}$ to edges in $E_\delta$.

We denote $\mathcal{W} \subseteq \mathcal{E}$ the set of such ECs. Non-winning ECs are *losing*: in those, whatever the strategy of Eve played against the stochastic model $\tau^{\text{st}}$ (or any strategy with the same support), there exists at least one play for which the mean payoff is not strictly positive (even if its probability is zero, its mere existence is not acceptable for the worst-case requirement).

**Example 20.** Note that an EC is *winning* if Eve has a worst-case winning strategy from all vertices. This point is important as it may well be the case that winning strategies exist in a strict subset of vertices of the EC. This does not contradict the definition of
<figure><img src="image_106.png" /><figcaption>Figure 12.4: End component $U_2$ is losing. The set of maximal winning end components is $\mathcal{W} = \mathcal{W} = \{U_1, U_3\}$.</figcaption></figure>

ECs as strongly connected subgraphs, as the latter only guarantees that every vertex can be reached with probability one, and not necessarily surely. Hence one cannot call upon the prefix independence of the mean payoff to extend the existence of a winning strategy to all vertices.

Such a situation can be observed on the arena of Figure 12.4, where the EC $U_2$ is losing (because from $v_1$, the play $(v_1v_3v_4)^\omega$ can be forced by Adam, yielding mean payoff $-1/3 \le 0$), while its sub-EC $U_3$ is winning. From $v_1$, Eve can ensure to reach $U_3$ almost-surely, but not surely, which is critical in this case.

## Maximal winning end components

Based on these definitions, observe that Algorithm 12.3 does not actually compute the set $\mathcal{W}$ containing all WECs, but rather the set $\mathcal{W}_w \subseteq \mathcal{W}$, defined as $\mathcal{W}_w = \{U \in \mathcal{W} \mid \forall U' \in \mathcal{W}, U \subseteq U' \implies U = U'\}$, i.e., the set of maximal WECs (MWECs).

The intuition on *why we can* restrict our study to this subset is as follows. If an EC $U_1 \in \mathcal{W}$ is included in another EC $U_2 \in \mathcal{W}$, i.e., $U_1 \subseteq U_2$, we have that the maximal expected value achievable in $U_2$ is at least equal to the one achievable in $U_1$. Indeed, Eve can reach $U_1$ with probability one (by virtue of $U_2$ being an EC and $U_1 \subseteq U_2$) and stay in it forever with probability one (by virtue of $U_1$ being an EC): hence the expectation of such a strategy would be equal to what can be obtained in $U_1$ thanks to the prefix independence of the mean payoff. This property implies that it is sufficient to consider MWECs in our computations.

As for *why we do it*, observe that the complexity gain is critical. The number of WECs can be as large as $|\mathcal{W}| \le |\mathcal{E}| \le 2^{|V|}$, that is, exponential in the size of the input. Yet, the number of MWECs is bounded by $|\mathcal{W}_w| \le |V|$ as they are disjoint by definition: for any two WECs with a non-empty intersection, their union also constitutes an EC, and is still winning because Eve can essentially stick to the EC of her choice.

The computation of the set $\mathcal{W}_w$ is executed by a recursive subalgorithm calling polynomially-many times an oracle solving the worst-case problem (e.g., following the pseudo-polynomial-time algorithm of Section 4.3). Roughly sketched, this algorithm computes the maximal EC decomposition of an MDP (in polynomial time by Theorem 66), then checks for each EC $U$ in the decomposition (their number is polynomial) if $U$ is winning or not, which requires a call to an oracle solving the worst-case threshold problem on the corresponding subgame. If $U$ is losing, it may still be the case that a sub-EC $U' \subsetneq U$ is winning. Therefore we recurse on the MDP reduced to $U$, where
vertices from which Adam can win in $U$ have been removed (they are a no-go for Eve). Hence the stack of calls is also at most polynomial.

**Lemma 143.** The set $\mathcal{U}_w$ of MWECs can be computed in pseudo-polynomial time, and deciding if a set of vertices $U \subseteq V$ belongs to $\mathcal{U}_w$ is in NP $\cap$ coNP.

The complexity follows from Theorem 39 and $P^{NP \cap coNP} = NP \cap coNP$ [Bra79].

**Example 21.** Consider the running example in Figure 12.3. Note that vertices $v_1, v_2$ and $v_5$ do not belong to any EC: given any strategy of Eve in $\mathcal{P}$, with probability one, any consistent play will only visit these vertices a finite number of times (Lemma 69). The set of MWECs is $\mathcal{U}_w = \{U_2, U_3\}$. Obviously, these ECs are disjoint. The set of WECs is larger, $\mathcal{W} = \mathcal{U}_w \cup \{\{v_9, v_{10}\}, \{v_6, v_7\}\}$.

End component $U_1$ is losing: in the subarena $A_\delta[U_1]$, Adam's strategy consisting in always picking the $-1$ edge guarantees a negative mean payoff. Note that this edge is present in $E_\delta$ as it is assigned probability $1/2$ by the stochastic model $\tau^\text{st}$. Here, we witness why it is important to base our definition of WECs on $A_\delta$ rather than $\mathcal{A}$. Indeed, in $A[U_2]$, it is also possible for Adam to guarantee a negative mean payoff by always choosing edges with weight $-1$. However, to achieve this, Adam has to pick edges that are not in $E_\delta$: this will never happen against the stochastic model and as such, this can be watched by Eve to see if Adam uses an arbitrary antagonistic strategy, and dealt with. If Adam conforms to $E_\delta$, i.e., if he plays in $A_\delta$, he has to pick the edge of weight 1 in $v_7$ and Eve has a worst-case winning strategy consisting in always choosing to go in $v_7$. This EC is thus classified as winning. Note that for $U_3$, in both subarenas $A[U_3]$ and $A_\delta[U_3]$, Eve can guarantee a strictly positive mean payoff by playing $(v_9 v_{10})^\omega$: even arbitrary strategies of Adam cannot endanger Eve in this case.

Lastly, consider the arena depicted in Figure 12.4. While $U_2$ is a strict superset of $U_3$, the former is losing whereas the latter is winning, as explained above. Hence, the set $\mathcal{U}_w$ is equal to $\{U_1, U_3\}$.

## Ensure reaching winning end components

As discussed, under any arbitrary strategy of Eve, vertices visited infinitely often form an EC with probability one (Lemma 69). Now, if we take a *finite-memory* strategy that satisfies the BWC problem, we can refine this result and state that they form a *winning* EC with probability one. Equivalently, let $\text{Inf}(\pi)$ denote the set of vertices visited infinitely often along a play $\pi$: we have that the probability that a play $\pi$ is such that $\text{Inf}(\pi) = U$ for some $U \in \mathcal{E} \setminus \mathcal{W}$ is zero. The equality is crucial. It may be the case, with non-zero probability, that $\text{Inf}(\pi) = U' \subseteq U$, for some $U' \in \mathcal{W}$, and $U \in \mathcal{E} \setminus \mathcal{W}$ (hence the recursive algorithm to compute $\mathcal{U}_w$). It is clear that Eve should not visit all the vertices of a LEC forever, as then she would not be able to guarantee the worst-case threshold inside the corresponding subarena.<fnref n="3" />

**Lemma 144.** For any initial vertex $v_0$ and finite-memory strategy $\sigma$ that satisfies the BWC problem, it holds that $\mathbb{P}_{\mathcal{P},v_0}^{\sigma}[\{\pi \mid \text{Inf}(\pi) \in \mathcal{W}\}] = 1$.

<footnote n="3">³This is no longer true if Eve may use infinite memory: there may still be some incentive to stay in a LEC. But this goes beyond the scope of our overview.</footnote>
We denote $V_{\text{neg}} = V \setminus \bigcup_{U \in \mathcal{U}_w} U$ the set of vertices that, with probability one, are only seen a finite number of times when a (finite-memory) BWC satisfying strategy is played, and call them *negligible vertices*.

Our ultimate goal here is to modify the colouring of $\mathcal{P}$ from $c$ to $c'$, such that a classical optimal strategy for the expected value problem (Theorem 70) using this new colouring $c'$ will naturally avoid LECs and prescribe which WECs are the most interesting to reach for a BWC strategy on the initial arena $\mathcal{A}$ and MDP $\mathcal{P}$ with colouring $c$. For the sake of readability, let us simply use $\mathcal{P}$ and $\mathcal{P}'$ to refer to MDP $\mathcal{P}$ with respective colourings $c$ and $c'$.

Observe that the expected value obtained in $\mathcal{P}$ by any BWC satisfying strategy of Eve only depends on the weights of edges involved in WECs, or equivalently, in MWECs (as the set of plays that are not eventually trapped in them has measure zero). Consequently, we define colouring $c'$ as follows: we keep the weights unchanged in edges that belong to some $U \in \mathcal{U}_w$, and we put them to zero everywhere else, i.e., on any edge involving a negligible vertex. Weight zero is taken because it is lower than the expectation granted by WECs, which is *strictly* greater than zero by definition (as $\alpha = 0$).

**Example 22.** Consider $U_1$ in Figure 12.3. This EC is losing as argued before. The optimal expectation achievable in $\mathcal{P}[U_1]$ by Eve is 4: this is higher than what is achievable in both $U_2$ and $U_3$. Note that there exists no WEC included in $U_1$. By Chapter 5, we know that, from $v_1$, any strategy of Eve will see its expectation bounded by the maximum between the optimal expectations of the ECs $U_1$, $U_2$ and $U_3$. Our previous arguments further refine this bound by restricting it to the maximum between the expectations of $U_2$ and $U_3$. Indeed, Eve cannot benefit from the expected value of $U_1$ while using finite memory, as being trapped in $U_1$ induces the existence of plays losing for the worst-case constraint. Hence there is no point in playing inside $U_1$ and Eve may as well cross it directly and try to maximise its expectation using the WECs, $U_2$ and $U_3$. The set of negligible vertices in $\mathcal{P}$ is $V_{\text{neg}} = V \setminus (U_2 \cup U_3) = \{v_1, v_2, v_3, v_4, v_5\}$. We depict $\mathcal{P}'$ in Figure 12.5.

In the arena depicted in Figure 12.4, we already observed that $\mathcal{E} = \{U_1, U_2, U_3\}$ and $\mathcal{W} = \mathcal{U}_w = \{U_1, U_3\}$. Consider the negligible vertex $v_1 \in V_{\text{neg}} = U_2 \setminus U_3$. A finite-memory strategy of Eve may only take the edge $(v_1, v_3)$ finitely often in order to ensure the worst-case requirement. If Eve were to play this edge repeatedly, the losing play $(v_1 v_3 v_4)^\omega$ would exist (while of probability zero). Therefore, Eve can only ensure that $U_3$ is reached with a probability arbitrarily close to one, and not equal to one, because at some point, she has to switch to edge $(v_1, v_2)$ (after a bounded time since Eve uses a finite-memory strategy).

## Reach the highest valued winning end components

We compute the maximal expected mean payoff $\beta^*$ that can be achieved by Eve in $\mathcal{P}'$, from $v_0$. This computation takes polynomial time and memoryless strategies suffice to achieve the maximal value, as established in Theorem 70. As seen before, such a strategy reaches an EC of $\mathcal{P}'$ with probability one. Basically, we build a strategy that favours reaching ECs with high associated expectations in $\mathcal{P}'$.
<figure><img src="image_107.png" /><figcaption>Figure 12.5: Putting all weights outside MWECs to zero naturally drives the optimal expectation strategy in $\mathcal{P}'$, depicted by the thick edges, toward the highest valued MWECs. ECs are annotated with their corresponding optimal expectations in the original MDP $\mathcal{P}$ and the modified MDP $\mathcal{P}'$.</figcaption></figure>

We argue that the ECs reached with probability one by this strategy are necessarily WECs in $\mathcal{P}$. Clearly, if a WEC is reachable instead of a losing one, it will be favoured because of the weights definition in $\mathcal{P}'$ (expectation is strictly higher in WECs). Thus it remains to check if the set of WECs is reachable with probability one from any vertex in $V$. That is the case because of the preprocessing: we know that all vertices are winning for the worst-case requirement. Clearly, from any vertex in $A = V \setminus \bigcup_{U \in \mathcal{E}} U$, Eve cannot ensure to stay in $A$ (otherwise it would form an EC) and thus must be able to win the worst-case requirement from reached ECs. Now for any vertex in $B = \bigcup_{U \in \mathcal{E}} U \setminus \bigcup_{U \in \mathcal{U}_w} U$, i.e., vertices in LECs and not in any winning sub-EC, Eve cannot win the worst-case by staying in $B$, by definition of LEC. Since we know Eve can ensure the worst-case by hypothesis, it is clear that she must be able to reach $C = \bigcup_{U \in \mathcal{U}_w} U$ from any vertex in $B$, as claimed.

## Inside winning end components

Based on that, we know that WECs of $\mathcal{P}$ will be reached with probability one when maximizing the expected value in $\mathcal{P}'$. Let us first consider what we can say about such ECs if we assume that $E_\delta = E$, i.e., if the stochastic model $\tau$^st maps all possible edges to non-zero probabilities. We establish a finite-memory combined strategy $\sigma^{\text{cmb}}$ of Eve that ensures (i) worst-case satisfaction while yielding (ii) an expected value $\varepsilon$-close to the maximal expectation inside the EC.

For two well-chosen parameters $K, L \in \mathbb{N}$, it is informally defined as follows: in
phase (a), play a memoryless expected value optimal strategy $\sigma^e$ for $K$ steps and memorise $\text{Sum} \in \mathbb{Z}$, the sum of weights along these steps; in phase (b), if $\text{Sum} > 0$, go to (a), otherwise play a memoryless worst-case optimal strategy $\sigma^{wc}$ for $L$ steps, then go to (a). In (a), Eve tries to increase her expectation and approach the optimal one, while in (b), she compensates, if needed, losses that occurred in (a).

The two memoryless strategies exist on the subarena induced by the EC: by definition of ECs, based on $E_\delta$, the stochastic model of Adam will never be able to force leaving the EC against the combined strategy.

A key result to our approach is the existence of values for $K$ and $L$ such that (i) and (ii) are verified. We see plays as sequences of periods, each starting with phase (a).

First, for any $K$, it is possible to define $L(K)$ such that any period composed of phases $(a) + (b)$ ensures a mean payoff at least $1/(K+L) > 0$. Periods containing only phase $(a)$ trivially induce a mean payoff at least $1/K$ as they are not followed by phase $(b)$. Both rely on the weights being integers. As the length of any period is bounded by $(K+L)$, the inequality remains strict for the mean payoff of any play, granting (i).

Now, consider parameter $K$. Clearly, when $K \to \infty$, the expectation over phase (a) tends to the optimal one. Nevertheless, phases (b) also contribute to the overall expectation of the combined strategy, and (in general) lower it so that it is strictly less than the optimal for any $K, L \in \mathbb{N}$. Hence to prove (ii), we not only need that the probability of playing phase (b) decreases when $K$ increases, but also that it decreases faster than the increase of $L$, needed to ensure (i), so that overall, the contribution of phases (b) tends to zero when $K \to \infty$. This is indeed the case and is proved using (rather technical) results bounding the probability of observing a mean payoff significantly (more than some $\varepsilon$) different than the optimal expectation along a phase (a) of length $K \in \mathbb{N}$: this probability decreases exponentially when $K$ increases, while $L$ only needs to be polynomial in $K$.

**Theorem 134.** Let $U \in \mathcal{W}$ be a WEC, $\tau^{\text{st}}$ be such that $E_\delta = E$, $v_0 \in U$ be the initial vertex, and let $\beta^* \in \mathbb{Q}$ be the maximal expected value achievable by Eve in EC $U$. Then, for all $\varepsilon > 0$, there exists a finite-memory strategy of Eve that satisfies the BWC problem for the thresholds pair $(0, \beta^* - \varepsilon)$.

**Example 23.** Consider the subarena $\mathcal{A}_\delta[U_3] = \mathcal{A}[U_3]$ from Figure 12.3 and the initial vertex $v_{10}$. Clearly, the worst-case requirement can be satisfied, that is why the EC is classified as winning. Always choosing to go to $v_9$ when in $v_{10}$ is an optimal memoryless worst-case strategy $\sigma^{wc}$ that guarantees a mean payoff $\alpha^* = 1$. Its expectation is $\mathbb{E}_{(\mathcal{A}[U_3])_{\tau^{\text{st}}, v_{10}}}[\text{MeanPayoff}^{-}] = 1$. On the other hand, the strategy $\sigma^e$ that always selects the edge going to $v_{11}$ is optimal regarding the expected value criterion: it induces expectation $\beta^* = (0 + (1/2 \cdot 9 + 1/2 \cdot (-1))/2 = 2$ against the stochastic model $\tau^{\text{st}}$. However, it can only guarantee a mean payoff of value $-1/2$ in the worst-case.

By the reasoning above, we know that it is possible to find finite-memory strategies satisfying the BWC problem for any thresholds pair $(0, 2 - \varepsilon)$, $\varepsilon > 0$. In particular, consider the thresholds pair $(0, 3/2)$. We build a combined strategy $\sigma^{\text{cmb}}$ as sketched before. Let $K = L = 2$: the strategy plays the edge $(v_{10}, v_{11})$ once, then if the edge of value 9 has been chosen by Adam, it chooses $(v_{10}, v_{11})$ again; otherwise it chooses the edge $(v_{10}, v_9)$ once and then resumes choosing $(v_{10}, v_{11})$. This
strategy satisfies the BWC problem. In the worst-case, Adam always chooses the $-1$ edge, but each time he does so, the $-1$ is followed by two $+1$ thanks to the cycle $v_{10}v_9v_{10}$. Strategy $\sigma^{\text{cmb}}$ hence guarantees a mean payoff equal to $(0-1+1+1)/4 = 1/4 > 0$ in the worst-case. For the expected value requirement, we can build the induced Markov chain $(\mathcal{A}[U_3])_{\sigma^{\text{cmb}}, \tau^{\text{st}}}$ (Figure 12.6) and check that its expectation is

$$ \mathbb{E}_{(\mathcal{A}[U_3])_{\tau^{\text{st}}, v_{10}}}^{\sigma^{\text{cmb}}} [\text{MeanPayoff}^{-}] = 5/3 > 3/2 \text{ (Chapter 4).} $$

<figure><img src="image_108.png" /><figcaption>Figure 12.6: Markov chain induced by the combined strategy $\sigma^{\text{cmb}}$ and the stochastic model $\tau^{\text{st}}$ over the WEC $U_3$ of $\mathcal{A}$.</figcaption></figure>

**Remark 28.** Memoryless strategies do not suffice for the BWC problem, even with randomisation. Indeed, the edge $(v_{10}, v_{11})$ cannot be assigned a non-zero probability as it would endanger the worst-case requirement (since the play $(v_{10}v_{11})^\omega$ cycling on the edge of weight $-1$ would exist and have a negative mean payoff). Hence, the only acceptable memoryless strategy is $\sigma^{\text{wc}}$, which has only an expectation of 1.

Now, consider what happens if $E_\delta \subsetneq E$. Then, if Adam uses an arbitrary strategy, he can take edges of probability zero, i.e., in $E \setminus E_\delta$, either staying in the EC, or leaving it. In both cases, this must be taken into account in order to satisfy the worst-case constraint as it may involve dangerous weights (recall that zero-probability edges are not considered when an EC is classified as winning or not). Fortunately, if this were to occur, Eve could switch to a worst-case winning memoryless strategy $\sigma^{\text{sec}}$, which exists in all vertices thanks to the preprocessing, to preserve the worst-case requirement. Regarding the expected value, this has no impact as it occurs with probability zero against $\tau^{\text{st}}$. The strategy to follow in WECs hence adds this reaction procedure to the combined strategy: we call it the witness-and-secure strategy $\sigma^{\text{wns}}$.

**Theorem 135.** Let $U \in \mathcal{W}$ be a WEC, $v_0 \in U$ be the initial vertex, and $\beta^* \in \mathbb{Q}$ be the maximal expected value achievable by Eve in EC $U$. Then, for all $\varepsilon > 0$, there exists a finite-memory strategy of Eve that satisfies the BWC problem for the thresholds pair $(0, \beta^* - \varepsilon)$.

**Example 24.** Consider the WEC $U_2$ in Figure 12.3 and the initial vertex $v_6 \in U_2$. Eve can ensure a strictly positive mean payoff in the subarena $\mathcal{A}_\delta[U_2]$, but not in $\mathcal{A}[U_2]$.
Indeed, it is easy to see that by always choosing the $-1$ edges (which requires an edge $(v_7, v_6) \in E \setminus E_\delta$), Adam can ensure a negative mean payoff whatever the strategy of Eve. However, there exists a strategy that ensures the worst-case constraint, i.e., that yields a strictly positive mean payoff against any strategy of Adam, by leaving the EC. Let $\sigma^{\text{sec}}$ be the memoryless strategy that takes the edge $(v_6, v_9)$ and then cycle on $(v_{10}v_9)^\omega$ forever: it guarantees a mean payoff of $1 > 0$.

For a moment, consider the EC $U_2$ in $\mathcal{A}_\delta$. Graphically, it means that the $-1$ edge from $v_7$ to $v_6$ disappears. In the subarena $\mathcal{A}_\delta[U_2]$, there are two particular memoryless strategies. The optimal worst-case strategy $\sigma^{\text{wc}}$ guarantees a mean payoff of $1/2 > 0$ by choosing to go to $v_7$. The optimal expectation strategy $\sigma^e$ yields an expected mean payoff of 3 by choosing to go to $v_8$ (naturally this strategy yields the same expectation whether we consider edges in $E_\delta$ or in E). Based on them, we build the combined strategy $\sigma^{\text{cmb}}$ of Eve as defined earlier and by Theorem 134, for any $\epsilon > 0$, there are values of K and L such that it satisfies the BWC problem for thresholds $(0, 3 - \epsilon)$ in $\mathcal{A}_\delta[U_2]$. For instance, for $K = L = 2$, we have $E_{(\mathcal{A}[U_2])_{\tau^{\text{st}}, v_6}^{\sigma^{\text{cmb}}}[\text{MeanPayoff}^{-}]} = 13/6$.

We construct the witness-and-secure strategy $\sigma^{\text{wns}}$ based on $\sigma^{\text{cmb}}$ and $\sigma^{\text{sec}}$ as described above. In this case, that means playing as $\sigma^{\text{cmb}}$ until the $-1$ edge from $v_7$ to $v_6$ is taken by Adam. This strategy ensures a worst-case mean payoff equal to $1 > 0$ thanks to $\sigma^{\text{sec}}$ and yields expectation $E_{(\mathcal{A}[U_2])_{\tau^{\text{st}}, v_6}^{\sigma^{\text{wns}}}[\text{MeanPayoff}^{-}]} = 13/6$ for $K = L = 2$.

Finally, notice that securing the mean payoff by switching to $\sigma^{\text{sec}}$ is needed to satisfy the worst-case requirement if Adam plays in $E \setminus E_\delta$. Also, observe that it is still necessary to alternate according to $\sigma^{\text{cmb}}$ in $\mathcal{A}_\delta[U_2]$ and that playing $\sigma^e$ is not sufficient to ensure the worst-case (because Eve has to deal with the $-1$ edge from $v_8$ to $v_6$ that remains in $E_\delta$).

## Global strategy synthesis

In summary, (a) LECs should be avoided and will be by a strategy that optimises the expectation on the MDP $\mathcal{P}';$ (b) in WECs, Eve can obtain $(\epsilon$-closely) the expectation of the EC and ensure the worst-case threshold.

Hence, we finally compare the value $\beta^*$ computed by Algorithm 12.3 with the expected value threshold $\beta$: (i) if it is strictly higher, we conclude that there exists a finite-memory strategy satisfying the BWC problem, and (ii) if it is not, we conclude that there does not exist such a strategy.

To prove (i), we establish a finite-memory strategy in $\mathcal{A}$, called global strategy $\sigma^{\text{glb}}$, of Eve that ensures a strictly positive mean payoff against an antagonistic adversary, and ensures an expected mean payoff $\epsilon$-close to $\beta^*$ (hence, strictly greater than $\beta$) against the stochastic adversary modeled by $\tau^{\text{st}}$ (i.e., in $\mathcal{P}$). The intuition is as follows. We play the memoryless optimal strategy of $\mathcal{P}'$ for a sufficiently long time, defined by a parameter $N \in \mathbb{N}$, in order to be with probability close to one in a WEC (the convergence is exponential by results on absorption times in Markov chains). Then, if we are inside a WEC, we switch to the corresponding witness-and-secure strategy (there is a different one for each MWEC) which, as sketched in the previous paragraph, ensures the worst-case and the expectation thresholds. If we are not yet in a WEC, then we
switch to a worst-case winning strategy, which always exists thanks to the preprocess-
ing. Thus the mean payoff of plays that do not reach WECs is strictly positive. Since
in WECs we are $\epsilon$-close to the maximal expected value of the EC, we can conclude
that it is possible to play the optimal expectation strategy of $\mathcal{P}'$ for sufficiently long to
obtain an overall expected value which is arbitrarily close to $\beta^*$, and still guarantee the
worst-case threshold in all consistent plays.

To prove (ii), it suffices to understand that only ECs have an impact on the ex-
pectation, and that LECs cannot be used forever without endangering the worst-case
requirement.

Note that given a winning strategy on $\mathcal{A}$, it is possible to build a corresponding winning strategy on $\mathcal{A}^{\text{in}}$ by reintegrating the memory states of $\tau^{\text{in}}$ in the memory structure of the winning strategy of Eve. Hence Algorithm 12.3 is correct and complete.

**Theorem 136.** If Algorithm 12.3 answers YES, then there exist values of the parameters such that the pure finite-memory global strategy $\sigma^{\text{glb}}$ satisfies the BWC mean payoff problem. In the opposite case, there exists no finite-memory strategy that satisfies the BWC mean payoff problem.

**Example 25.** Consider the arena in Figure 12.3 and the associated MDP $\mathcal{P}$. Following Chapter 5, analysis of the maximal ECs $U_1, U_2$ and $U_3$ reveals that the maximal expected mean payoff achievable in $\mathcal{P}$ is 4. It is for instance obtained by the memoryless strategy that chooses to go to $v_2$ from $v_1$ and to $v_4$ from $v_3$. Observe that playing in $U_1$ forever is needed to achieve this expectation. By Lemma 144, this should not be allowed as the worst-case cannot be ensured if it is. Indeed, Adam can produce worst-case losing plays by playing the $-1$ edge. Clearly, the maximal expected value that Eve can ensure while guaranteeing the worst-case requirement is thus bounded by the maximal expectation in $\mathcal{P}'$, i.e., by 3, as depicted in Figure 12.5. Let $\sigma^e$ denote an optimal memoryless expectation strategy in $\mathcal{P}'$ that tries to enter $U_2$ by playing $(v_1, v_2)$ and $(v_3, v_5)$, and then plays edge $(v_6, v_8)$ forever (thick edges in Figure 12.5).

Observe that Algorithm 12.3 answers YES for any thresholds pair $(0, \beta)$ such that $\beta < 3$. For the sake of illustration, we construct the global strategy $\sigma^{\text{glb}}$ as presented earlier, with $N=6$ and $K=L=2$. For the first six steps, it behaves exactly as $\sigma^e$. Note that after the six steps, the probability of being in $U_2$ is $1/4 + 1/8 = 3/8$. Then, $\sigma^{\text{glb}}$ switches to another strategy depending on the current vertex ($\sigma^{\text{wns}}$ or $\sigma^{\text{wc}}$) and sticks to this strategy forever. In particular, if the current vertex belongs to $U_2$, it switches to $\sigma^{\text{wns}}$ for $K=L=2$, which guarantees the worst-case threshold and induces an expectation of $13/6$. By definition of $\sigma^{\text{glb}}$, if the current vertex after six steps is not in $U_2$, then $\sigma^{\text{glb}}$ switches to $\sigma^{\text{wc}}$ which guarantees a mean payoff of 1 by reaching vertex $v_9$ and then playing $(v_9, v_{10})^\omega$. Overall, the expected mean payoff of $\sigma^{\text{glb}}$ against $\tau^{\text{st}}$ is

$$
\mathbb{E}_{\sigma^{\text{glb}}|\tau^{\text{st}},v_1}[\text{MeanPayoff}^{-}] \geq \frac{3}{8} \cdot \frac{13}{6} + \frac{5}{8} \cdot 1 = \frac{23}{16}.
$$

Notice that by taking $N$, $K$ and $L$ large enough, it is possible to satisfy the BWC problem for any $\beta < 3$ with the strategy $\sigma^{\text{glb}}$. Also, observe that the WEC $U_2$ is crucial to achieve expectations strictly greater than 2, which is the upper bound when limited to EC $U_3$. For instance, $N = 25$ and $K = L = 2$ implies an expectation strictly greater than 2 for the global strategy.
Lastly, note that in general, the maximal expectation achievable in $\mathcal{P}^1$ (and thus in $\mathcal{P}$ when limited to strategies that respect the worst-case requirement) may depend on a combination of ECs instead of a unique one. This is transparent through the solving of the expected value problem in the MDP $\mathcal{P}^1$.

## Complexity bounds

The input size of the algorithm depends on the size of the arena, the size of the memory structure for the stochastic model, and the encodings of probabilities, weights and thresholds. We can prove that all computing steps require (deterministic) polynomial time except for calls to an algorithm solving the worst-case threshold problem, which is in $NP \cap coNP$ and not known to be in P (Theorem 39). Hence, the overall complexity of the BWC problem is in $NP \cap coNP$ (using $P^{NP \cap coNP} = NP \cap coNP$ [Bra79]) and may collapse to P if the worst-case problem were to be proved in P.

The BWC problem is at least as difficult as the worst-case problem thanks to a trivial polynomial-time reduction from the latter to the former. Thus, membership to $NP \cap coNP$ can be seen as optimal regarding our current knowledge of mean payoff games.

**Theorem 137.** The BWC mean payoff problem is in $NP \cap coNP$ and at least as hard as solving mean payoff games. Moreover, pseudo-polynomial-memory strategies may be necessary for Eve and are always sufficient.

The memory bounds follow from the (involved) probability results used to determine the values of parameters *K*, *L* and *N* in the aforementioned strategies: such parameters need to be polynomial in the size of the arena but also in the probabilities, weights and thresholds.

Thanks to the pseudo-polynomial-time algorithm of Section 4.3 for mean payoff games, we obtain the following corollary.

**Corollary 23** (Beyond worst-case for mean payoff games). *Algorithm 12.3 solves the BWC mean payoff problem in pseudo-polynomial time.*

## Wrap-up

As witnessed by our long overview, solving the beyond worst-case problem requires much more involved techniques than solving the two individual problems, worst-case and expected value, separately. Complexity-wise, it is fortunate that the problem stays in $NP \cap coNP$, and is no more complex that simple mean payoff games. The multi-objective nature of the problem still incurs a cost with regard to strategies: whereas memoryless strategies suffice both in mean payoff games and mean payoff MDPs, we here need pseudo-polynomial memory. Finally, note that Eve does not need to use randomness: pure strategies still suffice.
## 12.5 Percentile queries

We close this chapter by a quick detour to multidimensional MDPs. When considering single-dimension MDPs with payoffs, as in Chapter 5, there are two different (yet both natural) settings that arise depending on how one decides to aggregate play values through the probability measure. Let $\mathcal{P}$ be an MDP, $v$ an initial vertex, and $f$ the payoff function. In the first setting, Eve's goal is to optimise the expected value of the payoff function, that is, to find a strategy $\sigma$ that maximises $E_{\mathcal{P},v}^{\sigma}[f]$. In the second setting, we set a performance threshold to achieve for the payoff function, say $\alpha \in \mathbb{Q}$, essentially creating the qualitative objective $f \ge \alpha$, and Eve aims to maximise the probability to achieve this objective, i.e., she is looking for a strategy $\sigma$ that maximises $P_{\mathcal{P},v}^{\sigma}[f \ge \alpha]$. The concept of percentile query extends the latter problem to multidimensional payoffs.

From now on, assume we have an MDP $\mathcal{P}$ with a multidimensional colouring function $c: E \to \mathbb{Z}^k$. Whether $\mathcal{P}$ uses actions as in Chapter 5 or random vertices as in Chapter 6 does not matter for our discussion — both are equivalent modulo slight modifications of the MDP. Recall that we denote by $f_i, 1 \le i \le k$, the projection of $f$ to its $i$-th component.

**Problem 20 (Percentile query problem).**

**INPUT:** An MDP $\mathcal{P}$, an initial vertex $v_0$, a payoff function $f$, $q \ge 1$ the number of percentile constraints in the query, $q$ dimensions $l_i \in \{1, \dots, k\}$, $q$ value thresholds $\alpha_i \in \mathbb{Q}$, $q$ probability thresholds $\mu_i \in \mathbb{Q} \cap [0, 1]$.

**OUTPUT:** Does Eve have a strategy $\sigma$ such that $\sigma$ is winning for the conjunction of $q$ constraints, called percentile query,

$$ \mathcal{Q} = \bigwedge_{i=1}^{q} \mathbb{P}_{\mathcal{P},v_0}^{\sigma} [f_{l_i} \ge \alpha_i] \ge \mu_i? $$

As usual, we also want to synthesize such a strategy $\sigma$ if one exists. Note that this percentile query framework permits to express rich properties, as each of the $q$ constraint can use a different dimension, value threshold and probability threshold. It is also possible to have different constraints related to the same dimension, for example to enforce different value thresholds for different quantiles.

The percentile query problem has been studied for a variety of payoff functions. Our aim here is not to give an exhaustive account of the corresponding results and techniques, but to highlight some new phenomena that arise in this setting, in comparison to what we have seen up to now.

### 12.5.1 An additional leap in complexity

The expressiveness of percentile queries asks for richer classes of strategies, even in very simple MDPs.

**Example 26.** Consider the single-player game depicted in Figure 12.7. Note that it is an MDP (using only Dirac distributions). Consider the payoff function MeanPayoff⁻.
<figure><img src="image_109.png" /><figcaption>Figure 12.7: Randomised strategies are needed to achieve any percentile query of the form $\mathbb{P}_{\mathcal{P},v_0}^{\sigma}[\text{MeanPayoff}_1^{-} \ge 1] \ge \mu_1 \wedge \mathbb{P}_{\mathcal{P},v_0}^{\sigma}[\text{MeanPayoff}_2^{-} \ge 1] \ge \mu_2$ with $\mu_1, \mu_2 > 0$.</figcaption></figure>

It is clear that due to its prefix independence, any play $\pi$ ending in $v_1$ (resp. $v_2$) will yield $\text{MeanPayoff}^{-}(\pi) = (1,0)$ (resp. $(0,1)$). Hence to achieve a percentile query

$$ \mathcal{Q} = \bigwedge_{i=1}^{2} \mathbb{P}_{\mathcal{P},v_0}^{\sigma} [\text{MeanPayoff}_i^{-} \ge 1] \ge \mu_i, $$

Eve must go toward $v_i$ with probability at least $\mu_i$. If both probability thresholds are non-zero, then this is only achievable by using randomness within Eve's strategy.

Example 26 uses the mean payoff for the sake of consistency with the previous sections, but observe that it can be emulated with virtually all objectives considered in this book. In particular, using reachability with two target sets (corresponding to the edges (1,0) and (0,1)) is sufficient.

While pure strategies were used in most chapters<fnref n="4" /> of this book, randomised strategies have already been considered in specific settings, such as in Chapter 7, usually to break some kind of symmetry and/or make one's strategy hard to predict. In our setting of percentile queries, we are still dealing with relatively simple models of games: we consider turn-based, perfect information games. Yet, the need for randomness arises from the expressiveness of our class of objectives, which in general require careful balance between different stochastic options.

**Example 27.** Let us have another look at the MDP in Figure 12.7. Consider now that the probability thresholds $\mu_1$ and $\mu_2$ in query $\mathcal{Q}$ are not fixed a priori. Instead, we are interested in the set of vectors $(\mu_1, \mu_2)$ that Eve can achieve. In particular, we want to determine the Pareto frontier<fnref n="5" /> and the corresponding Pareto-optimal strategies. What is interesting here is that, in our simple example, there is already an infinite, non-countable, number of Pareto vectors. Indeed, Eve can ensure any vector $(\mu_1, \mu_2)$ such that $\mu_1, \mu_2 \ge 0$ and $\mu_1 + \mu_2 = 1$ by simply taking the edge leading to $v_i$ with probability $\mu_i$.

Although the Pareto frontier consists of an infinite number of points in Example 27, it can be represented in a finite way, as it is essentially obtained through linear combinations of two extreme vectors: (1,0) and (0,1). Interestingly, these two vectors correspond to what can be achieved with pure strategies, and their convex hull yields the Pareto frontier. So, the Pareto frontier can be represented as a convex polytope whose vertex representation is given by the vectors achievable by pure strategies. This

<footnote n="4">⁴Without loss of generality as they suffice in the respective contexts of these chapters.</footnote>

<footnote n="5">⁵One can easily adapt Definition 30 to this context.</footnote>
<figure><img src="image_110.png" /><figcaption>Figure 12.8: When restricted to pure strategies, there are still infinitely many Pareto vectors for the query $P_{\mathcal{D},v_0}^{\sigma}$ [$\text{MeanPayoff}_1^{-} \ge 1$] $\ge \mu_1$ $\wedge$ $P_{\mathcal{D},v_0}^{\sigma}$ [$\text{MeanPayoff}_2^{-} \ge 1$] $\ge \mu_2$. For example, (1,0), (0,1), (1/2, 1/2), (3/4, 1/4), (1/4, 3/4)...</figcaption></figure>

is not merely an artefact resulting from the simplicity of our example; similar phenomena occur in many settings mixing MDPs and multiple objectives.

While the continuous aspect of the Pareto frontier stems from the possibility to use randomness in strategies, complex Pareto frontiers are also to be expected when restricting Eve to pure strategies.

**Example 28.** Consider the MDP in Figure 12.8. It uses the random vertices formalism as in Section 12.4. This MDP is a slight adaptation of the one in Figure 12.7, the crux being that when Eve tries to go to $v_i$ now, she has to cross $r_i$, which has probability $1/2$ to send her back to $v_0$. In the long run, it does not really matter, as Eve will almost surely end up in $v_1$ or $v_2$ (Chapter 5). And if Eve is allowed to use randomness, we obtain the same Pareto frontier as in the previous example. Yet, these random vertices serve a purpose.

When restricted to pure strategies, Eve cannot use the inherent randomness of her strategy to achieve any given vector $(\mu_1, \mu_2)$, as she could in Example 27. Nonetheless, by using memory, Eve is still able to achieve infinitely many Pareto vectors. For example, by first choosing to go to $r_1$, then $r_2$ (if the play comes back to $v_0$), then $r_1$ again (and then every time the play goes back to $v_0$), Eve will achieve vector $(3/4, 1/4)$.

It is relatively easy to see that infinitely many Pareto vectors can be generated with memory and no randomness in Example 28; for example all vectors of the form $(1-p, p)$ where $p = 1/2^n$ for $n \in \mathbb{N}$. Still, all such vectors could already be generated via randomised memoryless strategies as sketched before.

In particular, all vectors achievable by using memory and no randomness are of the form $(\mu_1, \mu_2)$, with $\mu_1, \mu_2 \ge 0$ and $\mu_1 + \mu_2 = 1$ — but not all such vectors can be achieved that way! Hence, by restricting the use of randomness, we have effectively created ‘gaps’ in the Pareto frontier, and rendered its description much more difficult. In full generality, it is usually necessary to use both randomness and memory to satisfy percentile queries.

**Proposition 12.** Pareto-optimal strategies for the percentile query problem may require randomness and memory (possibly infinite depending on the payoff function).
### 12.5.2 Complexity overview

We close our discussion of percentile queries with an overview of their complexity for various payoffs studied in Chapter 2, Chapter 4, and Chapter 5. We sum up the situation in Table 12.1. Some of these results are quite technical to establish, so our goal here is only to highlight interesting elements with respect to everything that has been discussed in the previous chapters and in our own.

<table><caption>Table 12.1: Complexity of percentile query problems for various payoffs. Here $F = \{Inf, Sup, LimInf, LimSup\}$. Parameters $P$ and $Q$ respectively represent the size of the MDP, and the size of the query; $P(x)$, $E(x)$ and $P_{ps}(x)$ respectively denote polynomial, exponential and pseudo-polynomial time in parameter $x$. For the shortest path, only non-negative weights can be used, as otherwise the problem is undecidable.</caption><thead><tr><th></th><th>Single-constraint</th><th>Single-dim.<br>Multi-constraint</th><th>Multi-dim.<br>Multi-constraint</th></tr></thead><tbody><tr><td>Reach</td><td>P</td><td>P(P)·E(Q), PSPACE-h</td><td>—</td></tr><tr><td>f ∈ F</td><td>P</td><td>P</td><td>P(P)·E(Q)<br>PSPACE-h.</td></tr><tr><td>MeanPayoff<sup>+</sup></td><td>P</td><td>P</td><td>P</td></tr><tr><td>MeanPayoff<sup>-</sup></td><td>P</td><td>P(P)·E(Q)</td><td>P(P)·E(Q)</td></tr><tr><td>ShortestPath</td><td>P(P)·P<sub>ps</sub>(Q)<br>PSPACE-h.</td><td>P(P)·P<sub>ps</sub>(Q) (one target)<br>PSPACE-h.</td><td>P(P)·E(Q)<br>PSPACE-h.</td></tr><tr><td>ε-gap DiscountedPayoff</td><td>P<sub>ps</sub>(P, Q, ε)<br>NP-h.</td><td>P<sub>ps</sub>(P, ε)·E(Q)<br>NP-h.</td><td>P<sub>ps</sub>(P, ε)·E(Q)<br>PSPACE-h.</td></tr></tbody></table>

Let us take a moment to appreciate Table 12.1. First, the payoffs present in the left column have all been discussed before; the only oddity being the notion of $\epsilon$-gap attached to the discounted payoff. Its presence is merely technical: we do not know if percentile queries using the discounted payoff can be solved exactly (and it is linked to long-standing open questions), but a slight relaxation of the problem, called $\epsilon$-gap problem, can be solved. Intuitively, this relaxation consists in allowing an $\epsilon$-wide uncertainty area around the value thresholds ($\alpha_i$) of the query. Second, some of the expressiveness of the queries is hidden in the table. For example, when using Reach or ShortestPath, one may consider different target sets in each constraint. Similarly, when using DiscountedPayoff, the discount factors may vary across constraints. Finally, when meaningful, the complexity is broken down into two parts, representing the relative dependency toward the size of the MDP, and the size of the query. The interest of this approach is that, in general and for practical applications, the model size is large whereas the query, encoding a specification, is comparatively much smaller. With that in mind, the polynomial dependency in the size of the MDP for most cases can be seen as good news.

Now, let us compare to what we know outside of percentile queries. Note that single-constraint queries correspond to the probability threshold problems in MDPs, studied in Chapter 5. We see that in most cases, the jump to multiple dimensions induces an exponential blow-up (in the number of constraints). If we compare to two-player (non-stochastic) games, as studied in Section 12.1, Section 12.2, and Sec-
tion 12.3, we see that the undecidability of shortest path objectives holds up if we replace the antagonistic player Adam by stochasticity. On the complexity side, the situation varies from payoff to payoff with, again, an interesting lack of symmetry between the two variants of mean payoff, in stark contrast to the single-dimension case.

## Bibliographic references

As discussed in the introduction, the literature on multi-objective models is too vast to provide a full account here. We therefore limit ourselves to some directions particularly relevant to our focus.

**Multidimensional games.** Our presentation of mean payoff games is inspired by Velner et al. [VCD+15]. Brenguier and Raskin studied the Pareto frontiers of these games in [BR15]. While we considered *conjunctions* of mean payoff objectives, Velner proved that Boolean combinations lead to undecidability [Vel15].

Energy games were discussed — through the prism of vector games — in Chapter 11. The link between energy games and mean payoff games under finite memory was established in [VCD+15]. While triple-exponential bounds on memory for Eve's strategies could be derived from [BJK10], the first exponential upper bounds were proved by Chatterjee et al. [CRR14], also encompassing conjunctions with *parity* objectives. These bounds have since been refined [JLS15] but remain exponential; indeed, it is known that exponential memory is necessary for Eve [CRR14].

The undecidability of total payoff games was first established by Chatterjee et al. in [CDRR15] via reduction from the halting problem for two-counter machines: we provided here a new, simpler proof based on robot games [NPR16]. This undecidability result, along with the complexity barriers of mean payoff and total payoff games, motivated the introduction of (multidimensional) *window objectives*: conservative variants of mean payoff and total payoff objectives that benefit from increased tractability and permit to reason about time bounds [CDRR15]. They have since been studied in a variety of contexts: variants of parity objectives [BHR16a], Markov decision processes [BDOR20], timed games [MRS21], etc.

The undecidability of shortest path games is formally new, but the result was already established for MDPs by Randour et al. in [RRS17]. Here, we use the aforementioned new approach based on robot games.

Consumption games were studied by Brázdil et al. [BCKN12]: they have the flavor of energy games but are actually incomparable. In such games, only negative weights are used, and gaining energy can only be done through particular 'reload edges' that refill the energy up to a predefined capacity.

Parts of our presentation of multidimensional games are inspired by [Ran14].

**Combinations of different objectives.** We focused on multidimensional games obtained by conjunction of *identical* objectives. Conjunctions of *heterogeneous* objectives have been studied in numerous different contexts, including mean payoff parity games [CHJ05, DJL18], energy parity games [CD12, CRR14], average-energy games
with energy constraints [BMR$^+$18, BHM$^+$17], energy mean payoff games [BHRR19], or Boolean combinations of simple quantitative objectives [BHR16b]. While similarities often exist across these different settings, ad hoc techniques are still needed and complexity results may vary greatly. Developing a general framework encompassing large classes of multi-objective problems is still a vastly unexplored challenge. Some progress has been achieved recently with a focus on strategy complexity; we discuss it further below.

**Beyond worst-case synthesis.** Our presentation is mostly inspired by Bruyère et al. in [BFRR17], which introduced the BWC synthesis problem, and where all technical details can be found. As noted in [BFRR17], allowing large inequalities in the BWC problem may require infinite-memory strategies. The case of infinite-memory strategies was studied in [CR15] along with multidimensional BWC mean payoff problems.

BWC problems were studied for other objectives, such as shortest path [BFRR17] or parity [BRR17]; and on other related models (e.g., [BKN16, AKV16]). BWC principles have been implemented in the tool UPPAAL [DJL$^+$14]. Boolean combinations of objectives akin to the BWC problem have been considered in MDPs [BGR20].

The BWC framework aims to provide strategies that exhibit high performance in normal operating conditions while offering a high-level of resilience in extreme conditions. A kindred — but softer — approach is the study of strategies in MDPs that achieve a trade-off between the expectation and the variance over the outcomes, giving a statistical measure of the stability of the performance. Brázdil et al. have considered the mean payoff with this philosophy in [BCFK17].

**Percentile queries.** The framework of percentile queries was introduced by Randour et al. in [RRS17], where they studied a variety of payoffs: all results mentioned in this chapter are from [RRS17]. As mentioned in Section 12.5.2, the percentile query problem was established to be undecidable for the shortest path payoff when both positive and negative weights are allowed. The theory of percentile queries can be seen as a quantitative follow-up to the work of Etessami et al. on reachability objectives, in [EKVY08].

Several other problems have been considered on multidimensional MDPs. For example, in [BBC$^+$14], Brázdil et al. study two different problems based on the mean payoff. On the one hand, they consider the optimisation of the expected value vector. On the other hand, they show how to optimise the probability that the payoff vector is above a threshold vector. Observe that, in comparison to percentile queries, the latter problem asks for a bound on the joint probability of the thresholds, that is, the probability of satisfying all constraints simultaneously. In contrast, percentile queries bound the marginal probabilities separately, which may allow for more modeling flexibility. Another complementary approach was considered by Haase and Kiefer in [HK15]: whereas percentile queries allow for conjunctions between probability constraints on simple value inequalities, they consider only one probability constraint but allow for conjunctions of value constraints within this single probability constraint. Hence, both frameworks are incomparable.
Various frameworks mixing concepts from beyond worst-case synthesis and per-
centile queries have been developed in the recent years, both in exact, formal ap-
proaches (e.g., [BGMR18, CKK17]), and in reinforcement learning (e.g., [KPR18,
CENR18, BCNV20]). Comparisons between percentile queries, beyond worst-case
synthesis, and other rich behavioural models can be found in [RRS14, BCH<sup>+</sup>16].

**Pareto frontiers.** As hinted throughout this chapter, the first step in understanding multi-objective settings is often to fix acceptable performance thresholds and to focus on the corresponding decision problem, asking if there exists a strategy to ensure these thresholds. Yet, to fully embrace the complexity of multi-objective frameworks, to be able to visualise the interplay between different (qualitative and quantitative) aspects and the corresponding trade-offs, we have to look at Pareto frontiers. This endeavour is generally difficult and one requires specific techniques to provide efficient approximations of Pareto frontiers — due to their complexity, exact computation is often out of reach.

We already mentioned [BR15], which deals with Pareto frontiers in multidimen-
sional mean payoff games. A seminal approach in the case of MDPs was developed
by Forejt et al. in [FKP12]. In a nutshell, it consists in obtaining successive approx-
imations of the Pareto frontier by solving many one-dimension problems. Each of
these is obtained by reinterpreting the original *k*-objective problem as a weighted sum
of each individual objective. Having the weight assignment vary yields different one-
dimension problems, but also permits to approximate the real Pareto frontier from a
different angle, as each weight assignment morally corresponds to looking in a dif-
ferent direction within the *k*-dimension space. The crux is then to explore this space
efficiently by a clever choice of weights at each iteration.

**Complex strategies.** The additional expressive power of multi-objective games and MDPs comes at a cost in terms of algorithmic complexity, but also with regard to the classes of strategies that are necessary to play (Pareto-)optimally. We have seen various examples in this chapter were Eve had to resort to strategies with (finite or infinite) memory and/or randomness. In a similar spirit to the characterisations of memoryless-determined objectives discussed in the early chapters of this book, recent research has striven to characterise the need for complex strategies in broad classes of multi-objective settings.

Recently, there has been a lot of progress on understanding the power of finite-
memory strategies, both in games [BRO+22, BRV23] and in MDPs [BORV21]. An
overview by Bouyer et al. is given in [BRV22]. With a particular focus on multi-
objective games, Le Roux et al. studied general conditions under which finite-memory
determinacy can be maintained through combinations of finite-memory determined ob-
jectives [RPR18].

With regard to randomness — which we have seen to be necessary in the most
general multi-objective settings, it is interesting to see that not all forms of random-
ness were created equal: when considering finite-memory (Section 1.5) randomised
strategies, one can put randomness in different parts of the memory structure (initial
state, update function, and/or ‘next-action’ function that exploits the memory to take a
decision), with differences in terms of resulting power [MR22]. This is in contrast to the celebrated Kuhn's theorem in classical game theory, which crucially relies on the availability of infinite memory.

Finally, as complex strategies are often prohibitive in practical applications, it is sometimes interesting to consider multi-objective problems where one looks for strategies of limited complexity. That is, even if the problem requires complex strategies for (Pareto-)optimality, one may be interested in how good simple strategies can be. For example, [DKQR20] develops techniques to explore the Pareto frontier of multi-objective MDPs under the constraint that only pure (i.e., without randomness) and limited-memory strategies should be considered. As seen in Example 28, such constraints often break the nice structure of (unrestricted) Pareto frontiers, which renders their exploration (and representation) more difficult.
<figure><img src="image_111.png" /></figure>

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

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