# From Local To Global Optimality in Concurrent Parity Games

Benjamin Bordais  Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMF, 91190
Gif-sur-Yvette, France  TU Dortmund University, Dortmund, Germany  Center for
Trustworthy Data Science and Security, University Alliance Ruhr, Dortmund,
Germany  Patricia Bouyer  Université Paris-Saclay, CNRS, ENS Paris-Saclay,
LMF, 91190 Gif-sur-Yvette, France  Stéphane Le Roux  Université Paris-Saclay,
CNRS, ENS Paris-Saclay, LMF, 91190 Gif-sur-Yvette, France

###### Abstract

We study two-player games on finite graphs. Turn-based games have many nice
properties, but concurrent games are harder to tame: e.g. turn-based
stochastic parity games have positional optimal strategies, whereas even basic
concurrent reachability games may fail to have optimal strategies. We study
concurrent stochastic parity games, and identify a local structural condition
that, when satisfied at each state, guarantees existence of positional optimal
strategies for both players.

##  1 Introduction

Two-player games played on finite graphs have been a helpful model in areas of
computer science. In such games, states/vertices of the graph are colored; the
actions of the players induce an infinite path in the graph, thus inducing an
infinite sequence of colors. Who wins depends on the color sequence. These
games can be turn-based, i.e. at each state a unique player chooses an
outgoing edge leading to a probability distribution over successor states, or
concurrent, i.e. at each state, the combination of one action per player
determines the probability distribution over successor states. In such a
stochastic setting, Player $\mathsf{A}$ wants to maximize her probability to
win, and Player $\mathsf{B}$ to minimize the very same probability.

We study the above games in the case of parity objective: colors are natural
numbers, and a sequence is winning for Player $\mathsf{A}$ iff the maximal
color seen infinitely often is even. This objective has been well-studied in
connection with model-checking. The turn-based version of these games has nice
properties involving deterministic positional strategies, where ”positional”
means that the played action depends only on the current state: with only
deterministic probability distributions over successor states, either of the
players has a winning such strategy [17]; with arbitrary probability
distributions over successor states, both players have optimal such strategies
[18, 7]. Note that in concurrent parity games, positional optimal strategies
for distinct starting states yield one positional strategy optimal for all
states uniformly. So we omit the word ”uniform” in this paper.

The above properties and others break in basic concurrent games but for safety
games, as recorded in the table below, where safety and reachability are
special cases of (co-)Büchi, and parity subsumes (co-)Büchi. Büchi games may
not have optimal strategies but when they have, they have positional ones; co-
Büchi games may not have optimal strategies, and they may have only infinite-
memory ones; and the other way around for $\varepsilon$-optimal strategies,
hence incomparable difficulty between Büchi and co-Büchi. This shows that
concurrent parity is strictly harder than (co-)Büchi, since parity games may
have only infinite-memory ($\varepsilon$-)optimal strategies. (See also the
column on subgame optimal strategies or Appendix A.)

|  $\exists$ opt strat? | opt |  $\varepsilon$-opt | SubG-opt
---|---|---|---|---
Safety | always [9] | pos. [9] | pos. [9] | pos. [9]
Reach. | not always [11] | pos. [3] | pos. [10] | pos. [3]
Büchi | not always | pos. [4] |  $\infty$ [8] | pos. [4]
Co-B. | not always |  $\infty$ [4] | pos. [6] | pos. [1]
Parity | not always |  $\infty$ [8] |  $\infty$ [8] |  $\infty$ [8]
Table 1: The summary of the situation in concurrent parity games in terms of
existence and nature of (subgame) (almost-)optimal strategies.

Nevertheless, concurrent games’ poor behavior in general should not deter us
from studying them, as many complex systems are inherently concurrent. See
[12] for further arguments. Continuing a recent line of research [2, 3, 4] we
seek local structural good behaviors that scale up to the whole game.

The following key property still holds in parity concurrent games, by
determinacy of Blackwell games [13]: each state has a value $u\in[0,1]$, i.e.
for all $\varepsilon>0$ Player $\mathsf{A}$ has an $\varepsilon$-optimal
strategy for plays starting in the state, i.e. guaranteeing probability at
least $u-\varepsilon$ to win, regardless of Player $\mathsf{B}$’s strategy;
and likewise Player $\mathsf{B}$ can guarantee that Player $\mathsf{A}$ wins
with probability at most $u+\varepsilon$. Here we are interested in strategies
that are optimal, i.e. that realize exactly the value $u$, and that are
positional. They do not exist in general (see [3, Figure 2]), but our result
below is a transfer from local to global positional optimality, and the
terminology that it uses is explained afterwards.

######  Theorem 1.

If at every state the induced game form is positionally optimizable, both
players have positional optimal strategies in the game.

A game form is a map from pairs of actions to a probability distribution over
successor states, see Figure 1 to the left, or [2] page 5 forcmore. So each
state induces a game form. Given a game form $\mathcal{F}$, an
$\mathcal{F}$-game has a unique non-trivial state which induces $\mathcal{F}$
and the other player states are of two kinds: first colored kind, they loop
back to the non-trivial state; second uncolored kind, they have an explicit
value in $[0,1]$, and the game stops there. Moreover Player $\mathsf{A}$
prefers higher explicit values. See Figure 1 or Figure 6 for examples of such
a construction. For all $n\in\mathbb{N}$, we say that $\mathcal{F}$ is called
_positionally optimizable up to $n$_ if both players have positional optimal
strategies in all $\mathcal{F}$-games with at most $n+1$ different colors. We
say that $\mathcal{F}$ is positionally optimizable if it positionally
optimizable up to $n$ for all $n\in\mathbb{N}$. An overview of the proof of
Theorem 1 is given in Subsection 6.1, after having introduced the relevant
definitions.

As a corollary of Theorem 1, we recover the known result that positional
strategies are sufficient to play optimally in turn-based stochastic games
[18, 7].

The version of Theorem 1 that we show in this paper (i.e. Theorem 25) is
actually a little more precise. Indeed, for Theorem 1 to hold, it is actually
sufficient that all the game forms appearing in the game are positionally
optimizable up to $n$ where $n$ denotes the different between the highest and
least color appearing in the game. After having proved Theorem 25, we show
that it is decidable if a game form is positionally optimizable (resp.
positionally optimizable up to $n$), see Proposition 58. Furthermore, we also
show that, for all $n\in\mathbb{N}$, the set of game forms positionally
optimizable up to $n$ is strictly larger that the set of game forms up to
$n+1$, see Theorem 59.

Finally, note that the results presented in this paper appear in the PhD
thesis of one of the authors, which will soon be available online.

##  2 Preliminaries and Game Forms

Consider a non-empty set $Q$. We denote by $Q^{*}$, $Q^{+}$ and $Q^{\omega}$
the set of finite sequences, non-empty finite sequences and infinite sequences
of elements of $Q$ respectively.

For all subsets $S\subseteq Q$, we let $\mathbbm{1}_{S}:Q\rightarrow\\{0,1\\}$
be the indicator function of the set $S$ defined by, for all $q\in Q$, we have
$\mathbbm{1}_{S}(q)=1$ if and only if $q\in S$. When $S=\\{q\\}$ for any $q\in
Q$, we write $\mathbbm{1}_{q}$ for $\mathbbm{1}_{S}$.

A _discrete probability distribution_ over a non-empty finite set $Q$ is a
function $\mu:Q\rightarrow[0,1]$ such that $\sum_{x\in Q}\mu(x)=1$. The
distribution $\mu$ is _deterministic_ if $\mu(q)=1$ for some $q\in Q$. For all
$S\subseteq Q$, we let $\mu[S]:=\sum_{q\in S}\mu(q)$. The set of distributions
over the set $Q$ is denoted $\mathcal{D}(Q)$.

For all $i\leq j\in\mathbb{N}$, we denote by $\llbracket i,j\rrbracket$ the
set of integers between $i$ and $j$: $\llbracket
i,j\rrbracket:=\\{k\in\mathbb{N}\mid i\leq k\leq j\\}$. This set is typed in
the sense that these are seen as integers and not reals numbers: $\llbracket
0,1\rrbracket\cap[0,1]=\emptyset$111This is done because, in parity games, the
integers refer to the colors appearing in the game whereas the real numbers
between in $[0,1]$ refer to the values of the states in the game. These are
disjoint.. For all finite sets $S\subseteq\mathbb{N}$, we let
$\mathsf{Even}(S)$ (resp. $\mathsf{Odd}(S)$) be the smallest even (resp. odd)
integer that is greater than or equal to all elements in $S$.

We recall the definition of game forms, which informally are finite two-
dimensional tables with variables, and of games in normal forms which are game
forms whose outcomes are values between $0$ and $1$.

######  Definition 2 (Game form and game in normal form).

Consider a non-empty set of outcomes $\mathsf{O}$. A _game form_
($\mathsf{GF}$ for short) on $\mathsf{O}$ is a tuple
$\mathcal{F}=\langle\mathsf{Act}_{\mathsf{A}},\mathsf{Act}_{\mathsf{B}},\mathsf{O},\varrho\rangle$
where $\mathsf{Act}_{\mathsf{A}}$ (resp. $\mathsf{Act}_{\mathsf{B}}$) is the
non-empty finite set of actions available to Player $\mathsf{A}$ (resp.
$\mathsf{B}$) and
$\varrho:\mathsf{Act}_{\mathsf{A}}\times\mathsf{Act}_{\mathsf{B}}\rightarrow\mathcal{D}(\mathsf{O})$
is a function that associates a distribution over the outcomes to each pair of
actions. We denote by $\mathsf{Form}(\mathsf{O})$ the set of all game forms on
$\mathsf{O}$.

When the set of outcomes $\mathsf{O}$ is equal to $[0,1]$, we say that
$\mathcal{F}$ is a _game in normal form_. For a valuation
$v:\mathsf{O}\rightarrow[0,1]$ of the outcomes, the notation
$\langle\mathcal{F},v\rangle$ refers to the game in normal form
$\langle\mathsf{Act}_{\mathsf{A}},\mathsf{Act}_{\mathsf{B}},[0,1],v\circ\varrho\rangle$
induced from $\mathcal{F}$ by $v$.

Finally, a Player-$\mathsf{A}$ (resp. Player-$\mathsf{B}$) game form
$\mathcal{F}$ is such that $|\mathsf{Act}_{\mathsf{B}}|=1$ (resp.
$|\mathsf{Act}_{\mathsf{A}}|=1$). The only Player-$\mathsf{B}$ (resp.
Player-$\mathsf{A}$) action is denoted $*$. Such a game form is denoted
$\mathcal{F}=\langle\mathsf{A}:\varrho(\mathsf{Act}_{\mathsf{A}},*)\rangle$
(resp.
$\mathcal{F}=\langle\mathsf{B}:\varrho(*,\mathsf{Act}_{\mathsf{B}})\rangle$).
When $\mathcal{F}$ is both a Player-$\mathsf{A}$ and a Player-$\mathsf{B}$
game form, it is called a _trivial_ game form. Such a game form is denoted
$\mathcal{F}=\\{\varrho(*,*)\\}$.

An example of a game form is depicted on the left of Figure 1 where the
actions available to Player $\mathsf{A}$ are the rows and the actions
available to Player $\mathsf{B}$ are the columns. Strategies available to
Player-$\mathsf{A}$ (resp. $\mathsf{B}$) are then the probability
distributions over their respective sets of actions. In a game in normal form,
Player $\mathsf{A}$ tries to maximize the outcome, whereas Player $\mathsf{B}$
tries to minimize it.

######  Definition 3 (Outcome and value of a game in normal form).

Consider a game in normal form
$\mathcal{F}=\langle\mathsf{Act}_{\mathsf{A}},\mathsf{Act}_{\mathsf{B}},[0,1],\varrho\rangle$.
The set $\mathcal{D}(\mathsf{Act}_{\mathsf{A}})$ (resp.
$\mathcal{D}(\mathsf{Act}_{\mathsf{B}})$) corresponds to the set of strategies
available to Player $\mathsf{A}$ (resp. $\mathsf{B}$), it is denoted
$\Sigma_{\mathsf{A}}(\mathcal{F})$ (resp. $\Sigma_{\mathsf{B}}(\mathcal{F})$).
For a pair of strategies
$(\sigma_{\mathsf{A}},\sigma_{\mathsf{B}})\in\Sigma_{\mathsf{A}}(\mathcal{F})\times\Sigma_{\mathsf{B}}(\mathcal{F})$,
the outcome
$\mathsf{out}_{\mathcal{F}}(\sigma_{\mathsf{A}},\sigma_{\mathsf{B}})$ in
$\mathcal{F}$ of the strategies $(\sigma_{\mathsf{A}},\sigma_{\mathsf{B}})$ is
defined as:
$\mathsf{out}_{\mathcal{F}}(\sigma_{\mathsf{A}},\sigma_{\mathsf{B}}):=\sum_{a\in\mathsf{Act}_{\mathsf{A}}}\sum_{b\in\mathsf{Act}_{\mathsf{B}}}\sigma_{\mathsf{A}}(a)\cdot\sigma_{\mathsf{B}}(b)\cdot\varrho(a,b)\in[0,1]$.

Consider a Player-$\mathsf{A}$ strategy
$\sigma_{\mathsf{A}}\in\Sigma_{\mathsf{A}}(\mathcal{F})$. The _value_ of
strategy $\sigma_{\mathsf{A}}$, denoted
$\mathsf{val}_{\mathcal{F}}(\sigma_{\mathsf{A}})$ is equal to:
$\mathsf{val}_{\mathcal{F}}(\sigma_{\mathsf{A}}):=\inf_{\sigma_{\mathsf{B}}\in\Sigma_{\mathsf{B}}(\mathcal{F})}\mathsf{out}_{\mathcal{F}}(\sigma_{\mathsf{A}},\sigma_{\mathsf{B}})$,
and dually for Player $\mathsf{B}$. When
$\sup_{\sigma_{\mathsf{A}}\in\Sigma_{\mathsf{A}}(\mathcal{F})}\mathsf{val}_{\mathcal{F}}(\sigma_{\mathsf{A}})=\inf_{\sigma_{\mathsf{B}}\in\Sigma_{\mathsf{B}}(\mathcal{F})}\mathsf{val}_{\mathcal{F}}(\sigma_{\mathsf{B}})$,
it defines the _value_ of the game $\mathcal{F}$, denoted
$\mathsf{val}_{\mathcal{F}}$. If
$\mathsf{val}_{\mathcal{F}}(\sigma_{\mathsf{A}})=\mathsf{val}_{\mathcal{F}}$,
the strategy $\sigma_{\mathsf{A}}$ is said to be _optimal_ for Player
$\mathsf{A}$. This is defined analogously for Player $\mathsf{B}$. Since the
sets of actions is finite, Von Neumann’s minimax theorem [16] ensures the
existence of a value and of optimal strategies for both players.

In the following, strategies in game forms will be called
$\mathsf{GF}$-strategies in order not to confuse them with strategies in
concurrent games (on graphs).

##  3 Concurrent games, local interactions

###  3.1 Concurrent arenas and games

######  Definition 4 (Finite stochastic concurrent arena).

A finite _concurrent arena_ $\mathcal{C}$ is a tuple $\langle
Q,\mathsf{F}\rangle$ where $Q$ is a non-empty finite set of states and
$\mathsf{F}:Q\rightarrow\mathsf{Form}(Q)$ maps each state to its induced game
form, which describes the interaction of the players at this state.

In the following, the arena $\mathcal{C}$ will refer to the tuple $\langle
Q,\mathsf{F}\rangle$, unless otherwise stated. Furthermore, for all $q\in Q$,
we denote by $\mathsf{Act}_{\mathsf{A}}^{q}$ and
$\mathsf{Act}_{\mathsf{B}}^{q}$ the sets of actions available to both players
in the local interaction $\mathsf{F}(q)$, unless otherwise stated. In this
paper, we focus on (max) parity objectives: the goal of Player $\mathsf{A}$ is
that the maximum of the colors (i.e. label on states) visited infinitely often
is even.

######  Definition 5 (Parity game).

Consider a finite set of states $Q$ and a coloring function
$\mathsf{col}:Q\rightarrow\mathbb{N}$. This coloring function induces the
_parity objective_ $W(\mathsf{col})\subseteq Q^{\omega}$ defined by
$W(\mathsf{col}):=\\{\rho\in
Q^{\omega}\mid\max(\mathsf{col}(\rho)_{\infty})\text{ is even }\\}$ where
$\mathsf{col}(\rho)_{\infty}:=\\{k\in\mathbb{N}\mid\forall
i\in\mathbb{N},\;\exists j\geq i,\;\mathsf{col}(\rho)_{j}=k\\}\neq\emptyset$
(since $Q$ is finite) denotes the set of colors seen infinitely often in
$\mathsf{col}(\rho)$.

A _parity game_ $\mathcal{G}=\langle\mathcal{C},\mathsf{col}\rangle$ is a pair
formed of a concurrent arena $\mathcal{C}$ and a coloring function
$\mathsf{col}:Q\rightarrow\mathbb{N}$.

In such a game, strategies map the history of the game (i.e. the finite
sequence of states visited so far) to a $\mathsf{GF}$-strategy in the game
form corresponding to the current state of the game.

######  Definition 6 (Strategies).

Consider a concurrent arena $\mathcal{C}$. A _strategy_ for Player
$\mathsf{A}$ is a function $\mathsf{s}_{\mathsf{A}}:\cup_{q\in Q}(Q^{*}\cdot
q\rightarrow\Sigma_{\mathsf{A}}(\mathsf{F}(q)))$. It is _positional_ if for
all $q\in Q$, there is a $\mathsf{GF}$-strategy
$\sigma_{\mathsf{A}}^{q}\in\Sigma_{\mathsf{A}}(\mathsf{F}(q))$ such that, for
all $\pi=\rho\cdot q\in Q^{+}$: $\mathsf{s}_{\mathsf{A}}(\pi)=\sigma_{A}^{q}$.
In that case, the strategy $\mathsf{s}_{\mathsf{A}}$ is said to be _defined_
by $(\sigma_{\mathsf{A}}^{q})_{q\in Q}$.

We denote by $\mathsf{S}_{\mathcal{C}}^{\mathsf{A}}$ and
$\mathsf{PS}_{\mathcal{C}}^{\mathsf{A}}$ the set of all strategies and
positional strategies respectively in arena $\mathcal{C}$ for Player
$\mathsf{A}$. A strategy $\mathsf{s}_{\mathsf{A}}$ is _deterministic_ if, for
all $\rho\in Q^{+}$, $\mathsf{s}_{\mathsf{A}}(\rho)$ is deterministic. The
definitions are analogous for Player $\mathsf{B}$.

Unlike deterministic games with deterministic strategies, the outcome of a
game, given two strategies (one for each Player), is not a single play but
rather a distribution over plays. To formalize this, we first define the
probability to go from a state $q$ to a state $q^{\prime}$ given two
$\mathsf{GF}$-strategies in $\mathsf{F}(q)$.

######  Definition 7 (Probability transition given two strategies).

Consider a concurrent arena $\mathcal{C}$, a state $q\in Q$ and two strategies
$(\sigma_{\mathsf{A}},\sigma_{\mathsf{B}})\in\Sigma_{\mathsf{A}}(\mathsf{F}(q))\times\Sigma_{\mathsf{B}}(\mathsf{F}(q))$.
Let $q^{\prime}\in Q$. The probability to go from $q$ to $q^{\prime}$ if the
players plays, in q, $\sigma_{\mathsf{A}}$ and $\sigma_{\mathsf{B}}$, denoted
$\mathbb{P}^{\sigma_{\mathsf{A}},\sigma_{\mathsf{B}}}{}(q,q^{\prime})$, is
equal to:

$\mathbb{P}^{\sigma_{\mathsf{A}},\sigma_{\mathsf{B}}}{}(q,q^{\prime}):=\mathsf{out}_{\langle\mathsf{F}(q),\mathbbm{1}_{q^{\prime}}\rangle}(\sigma_{\mathsf{A}},\sigma_{\mathsf{B}})$

We now define the probability of occurrence of finite paths, and consequently
of any Borel set, given a strategy per player.

######  Definition 8 (Probability distribution given two strategies).

Consider a concurrent arena $\mathcal{C}$ and two arbitrary strategies
$(\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}})\in\mathsf{S}_{\mathcal{C}}^{\mathsf{A}}\times\mathsf{S}_{\mathcal{C}}^{\mathsf{B}}$.
We denote by
$\mathbb{P}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}:Q^{+}\rightarrow\mathcal{D}(Q)$
the function giving the probability distribution over the next state of the
arena given the sequence of states already seen. That is, for all finite path
$\pi=\pi_{0}\ldots\pi_{n}\in Q^{+}$ and $q\in Q$, we have:

$\mathbb{P}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}(\pi)[q]=\mathbb{P}^{\mathsf{s}_{\mathsf{A}}(\pi),\mathsf{s}_{\mathsf{B}}(\pi)}{}(\pi_{n},q)$

The probability of a finite path $\pi=\pi_{0}\cdots\pi_{n}\in Q^{+}$ from a
state $q_{0}\in Q$ with the pair of strategies
$(\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}})$ is then equal to
$\mathbb{P}^{\mathcal{C},q_{0}}_{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}(\pi):=\Pi_{i=0}^{n-1}\mathbb{P}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}(\pi_{\leq
i})[\pi_{i+1}]$ if $\pi_{0}=q_{0}$ and $0$ otherwise. The probability of a
cylinder set $\mathsf{Cyl}(\pi):=\\{\pi\cdot\rho\mid\rho\in Q^{\omega}\\}$ is
$\mathbb{P}^{\mathcal{C},q_{0}}_{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}[\mathsf{Cyl}(\pi)]:=\mathbb{P}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}(\pi)$
for any finite path $\pi\in Q^{*}$. This induces the probability measure over
Borel sets in the usual way. We denote by
$\mathbb{P}^{\mathcal{C},q_{0}}_{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}$
this probability measure. mapping each Borel set to a value in $[0,1]$

The values of strategies and of the game follow.

######  Definition 9 (Value of strategies and of the game).

Let $\mathcal{G}=\langle\mathcal{C},\mathsf{col}\rangle$ be a parity game and
$\mathsf{s}_{\mathsf{A}}\in\mathsf{S}_{\mathcal{C}}^{\mathsf{A}}$ be a
Player-$\mathsf{A}$ strategy. The vector
$\chi_{\mathcal{G}}[\mathsf{s}_{\mathsf{A}}]:Q\rightarrow[0,1]$ giving the
value of the strategy $\mathsf{s}_{\mathsf{A}}$ is such that, for all
$q_{0}\in Q$, we have
$\chi_{\mathcal{G}}[\mathsf{s}_{\mathsf{A}}](q_{0}):=\inf_{\mathsf{s}_{\mathsf{B}}\in\mathsf{S}_{\mathcal{C}}^{\mathsf{B}}}\mathbb{P}^{\mathcal{C},q_{0}}_{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}[W(\mathsf{col})]$.
The vector $\chi_{\mathcal{G}}[\mathsf{A}]:Q\rightarrow[0,1]$ giving the value
for Player $\mathsf{A}$ is such that, for all $q_{0}\in Q$, we have
$\chi_{\mathcal{G}}[\mathsf{A}](q_{0}):=\sup_{\mathsf{s}_{\mathsf{A}}\in\mathsf{S}_{\mathcal{C}}^{\mathsf{A}}}\chi_{\mathcal{G}}[\mathsf{s}_{\mathsf{A}}](q_{0})$.
The vector $\chi_{\mathcal{G}}[\mathsf{B}]:Q\rightarrow[0,1]$ giving the value
of the game for Player $\mathsf{B}$ is defined similarly by reversing $\inf$
and $\sup$.

By Martin’s result on the determinacy of Blackwell games [13]:
$\chi_{\mathcal{G}}[\mathsf{A}]=\chi_{\mathcal{G}}[\mathsf{B}]$, which defines
the _value_ of the game:
$\chi_{\mathcal{G}}:=\chi_{\mathcal{G}}[\mathsf{A}]=\chi_{\mathcal{G}}[\mathsf{B}]$.
A Player-$\mathsf{A}$ strategy $\mathsf{s}_{\mathsf{A}}$ such that
$\chi_{\mathcal{G}}:=\chi_{\mathcal{G}}[\mathsf{s}_{\mathsf{A}}]$ is _optimal_
(and similarly for Player $\mathsf{B}$).

Note that optimal strategies may not exist in general; when they exist they
can be arbitrarily complex; see the table page 1.

Finally, we extend our formalism by considering stopping states with output
value, i.e. states that, when visited, immediately stop the game and induce a
specific value in $[0,1]$. The fact that the value of a stopping state $q$ is
set to be $u$ is denoted $\mathsf{val}(q)\leftarrow u$. Note that such
stopping states can be encoded in our formalism (see Appendix C.1). They will
be depicted as dashed states.

###  3.2 Markov chains and sufficient condition for optimality

In this subsection, we give a condition on positional strategies to be optimal
in a concurrent parity game. First, we need to introduce the notions of Markov
chain and bottom strongly connected component.

######  Definition 10 (Markov chain, BSCC).

A _Markov chain_ $\mathcal{M}$ is a pair $\mathcal{M}=\langle
Q,\mathbb{P}\rangle$ where $Q$ is a finite set of states and
$\mathbb{P}:Q\rightarrow\mathcal{D}(Q)$. A _bottom strongly connected
component_ (BSCC for short) $H\subseteq Q$ is a subset of states such that the
underlying graph of $H$ is strongly connected (w.r.t. edges given by positive
probability transitions from states to states) and $H$ cannot be exited: for
all $q\in H$ and $q^{\prime}\in Q$, $\mathbb{P}(q)(q^{\prime})>0$ implies
$q^{\prime}\in H$.

We say that a subset of states $S\subseteq Q$ _occurs_ in $H$ if $S\cap
H\neq\emptyset$. We say that a state $q\in Q$ _occurs_ in $H$ if $q\in H$.

Two positional strategies (one per player) in a concurrent arena not only
induce a probability measure on infinite sequences of states (recall
Definition 8), but also a Markov chain, whose graph is a subgraph of the
arena. (This is done formally in Appendix C.2.) If we only fix a strategy, we
can consider the BSCCs that are compatible with that strategy as follows.

######  Definition 11 (Induced Markov chains, BSCCs compatible with a
strategy).

Consider a parity game $\mathcal{G}=\langle\mathcal{C},\mathsf{col}\rangle$.
Let $\mathsf{s}$ be a positional strategy for one of the players. For every
positional and deterministic strategy $\mathsf{s}^{\prime}$ for the other
player, we denote by $\mathcal{M}_{\mathsf{s},\mathsf{s}^{\prime}}=\langle
Q,\mathbb{P}^{\mathsf{s},\mathsf{s}^{\prime}}\rangle$ the Markov chain
_induced_ by $\mathsf{s}$ and $\mathsf{s}^{\prime}$.

We let $H_{\mathsf{s}}$ denote the set of BSCCs _compatible_ with
$\mathsf{s}$, i.e. the BSCCs of some Markov chain
$\mathcal{M}_{\mathsf{s},\mathsf{s}^{\prime}}$, where $\mathsf{s}^{\prime}$
ranges over ther other player’s positional deterministic strategies. A BSCC
$H\in H_{\mathsf{s}}$ is _even-colored_ if $\max\mathsf{col}[H]$ is even.
Otherwise, it is _odd-colored_.

We now define several properties relating a positional strategy and a
valuation of the states.

######  Definition 12.

Let $\mathcal{G}=\langle\mathcal{C},\mathsf{col}\rangle$ be a game and
$v:Q\rightarrow[0,1]$ be a valuation over its states. Consider a positional
Player-$\mathsf{A}$ strategy $\mathsf{s}_{\mathsf{A}}$ (resp.
Player-$\mathsf{B}$ strategy $\mathsf{s}_{\mathsf{B}}$). The strategy
$\mathsf{s}_{\mathsf{A}}$ (resp. $\mathsf{s}_{\mathsf{B}}$):

  * •

_dominates_ the valuation $v$ if for all $q\in Q$, it holds that
$v(q)\leq\mathsf{val}_{\langle\mathsf{F}(q),v\rangle}(\mathsf{s}_{\mathsf{A}}(q))$
(resp.
$v(q)\geq\mathsf{val}_{\langle\mathsf{F}(q),v\rangle}(\mathsf{s}_{\mathsf{B}}(q))$);

  * •

_parity dominates_ the valuation $v$ if it dominates $v$ and all BSCCs $H$
compatible with $\mathsf{s}_{\mathsf{A}}$ (resp. $\mathsf{s}_{\mathsf{B}}$)
such that $\min v[H]>0$ (resp. $\max v[H]<1$) are even-colored (resp. odd-
colored);

  * •

_guarantees_ the valuation $v$ if, for all $q\in Q$, it holds
$v(q)\leq\chi_{\mathcal{G}}[\mathsf{s}_{\mathsf{A}}](q)$ (resp.
$v(q)\geq\chi_{\mathcal{G}}[\mathsf{s}_{\mathsf{B}}](q)$).

Parity dominating a valuation implies guaranteeing it (the theorem below can
be deduced from [5, Lemma 34]).

######  Theorem 13 (Proof C.3).

Consider a parity game $\mathcal{G}=\langle\mathcal{C},\mathsf{col}\rangle$, a
Player-$\mathsf{A}$ positional strategy
$\mathsf{s}_{\mathsf{A}}\in\mathsf{PS}_{\mathcal{C}}^{\mathsf{A}}$ and a
valuation of the states $v:Q\rightarrow[0,1]$. If the strategy
$\mathsf{s}_{\mathsf{A}}$ dominates the valuation $v$, then for all BSCCs
$H\in H_{\mathsf{s}_{\mathsf{A}}}$, there is some $v_{H}\in[0,1]$ such that
$v[H]=\\{v_{H}\\}$.If in addition $\mathsf{s}_{\mathsf{A}}$ parity dominates
$v$, it also guarantees $v$.

##  4 Local Environment

The goal of this section is to define simple parity games with a single non-
trivial local interaction. This will allow us to define exactly the game forms
that should be used in parity games if one requires positional optimal
strategies for both players. We first define what a (parity) environment on a
given set of outcomes is. We can then define the parity game induced by such
an environment (along with a game form).

######  Definition 14 (Parity environment).

Consider a non-empty finite set of outcomes $\mathsf{O}$. An _environment_ $E$
on $\mathsf{O}$ is a tuple $E:=\langle c,e,p\rangle$ where $c,e\in\mathbb{N}$
with $c\leq e$ and $p:\mathsf{O}\rightarrow\\{q_{\mathsf{init}}\\}\uplus
K_{e}\uplus[0,1]$. We let $p_{[0,1]}:=p[\mathsf{O}]\cap[0,1]$. The _size_
w.r.t. Player $\mathsf{A}$ (resp. $\mathsf{B}$) $\mathsf{Sz}_{\mathsf{A}}(E)$
(resp. $\mathsf{Sz}_{\mathsf{B}}(E)$) of the environment $E$ is equal to
$\mathsf{Sz}_{\mathsf{A}}(E):=\mathsf{Even}(e)-c$ (resp.
$\mathsf{Sz}_{\mathsf{B}}(E):=\mathsf{Odd}(e)-c$). We denote by
$\mathsf{Env}(\mathsf{O})$ the set of all environments on the set of outcomes
$\mathsf{O}$.

######  Remark 15.

A quick note on the size of an environment. From Player $\mathsf{A}$’s
perspective, the size of an environment $E:=\langle c,e,p\rangle$, assuming
that $c=0$, is equal to: 0 if $e=0$, 2 if $e=1$ or $e=2$, etc. Informally,
when $c=0$, if $e=0$ this corresponds to safety game, if $e=1$ this
corresponds to a co-Büchi game, etc. This will become more apparent with
Definition 16 below.

We can then define the simple parity game corresponding to a parity
environment.

######  Definition 16 (Parity game induced by an environment).

Consider a non-empty finite set of outcomes $\mathsf{O}$, a game form
$\mathcal{F}\in\mathsf{Form}(\mathsf{O})$ and an environment $E=\langle
c,e,p\rangle\in\mathsf{Env}(\mathsf{O})$. Let $Y:=(\mathcal{F},E)$. The local
arena $\mathcal{C}_{Y}=\langle Q,\mathsf{F}\rangle$ and the coloring function
$\mathsf{col}_{Y}$ induced by $Y$ is such that:

  * •

$Q:=\\{q_{\mathsf{init}}\\}\cup K_{e}\cup p_{[0,1]}$,
$Q_{\mathsf{s}}:=p_{[0,1]}$, and for all $u\in p_{[0,1]}$, we set the value of
the stopping state $u$ to be $u$ itself: $\mathsf{val}(u)\leftarrow u$;

  * •

$\mathsf{F}(q_{\mathsf{init}}):=\mathcal{F}^{p}=\langle\mathsf{Act}_{\mathsf{A}},\mathsf{Act}_{\mathsf{B}},Q,\varrho_{p}\rangle$
where, for all $\sigma_{\mathsf{A}}\in\mathcal{D}(\mathsf{Act}_{\mathsf{A}})$,
$\sigma_{\mathsf{B}}\in\mathcal{D}(\mathsf{Act}_{\mathsf{B}})$, and $q\in Q$,
we have
$\varrho_{p}(\sigma_{\mathsf{A}},\sigma_{\mathsf{B}})(q):=\varrho(\sigma_{\mathsf{A}},\sigma_{\mathsf{B}})[p^{-1}[q]]$;

  * •

for all $i\in\llbracket 0,e\rrbracket$, the set $k_{i}$ is trivial, its only
outcome is the state $q_{\mathsf{init}}$;

  * •

$\mathsf{col}_{Y}(q_{\mathsf{init}}):=c$ and for all $i\in\llbracket
0,e\rrbracket$, we have $\mathsf{col}_{Y}(k_{i}):=i$.

For all $u\in[0,1]$, we denote by $v_{Y}^{u}:Q\rightarrow[0,1]$ the valuation
such that: $v_{Y}^{u}(q_{\mathsf{init}})=v_{Y}^{u}(k_{i}):=u$ for all
$i\in\llbracket 0,e\rrbracket$ and $v_{Y}^{u}(x):=x$ for all $x\in p_{[0,1]}$.
Furthermore, for all Player-$\mathsf{A}$ $\mathsf{GF}$-strategies
$\sigma_{\mathsf{A}}\in\Sigma_{\mathsf{A}}(\mathcal{F})$, we denote by
$\mathsf{s}_{\mathsf{A}}^{Y}(\sigma_{\mathsf{A}})\in\mathsf{S}_{\mathsf{A}}^{\mathcal{C}_{Y}}$
the Player-$\mathsf{A}$ positional strategy defined by $\sigma_{\mathsf{A}}$
in the arena $\mathcal{C}_{Y}$.

The game $\mathcal{G}_{Y}$ is then equal to
$\mathcal{G}_{Y}:=\langle\mathcal{C}_{Y},\mathsf{col}_{Y}\rangle$.

######  Example 17.

Definition 16 above is illustrated in Figure 1. Note that the colors of the
non-stopping states are depicted in red next to the states.

As in the previous chapter, we can define the notion of Player-$\mathsf{A}$
$\mathsf{GF}$-strategy being optimal in a parity environment.

######  Definition 18 (Optimal $\mathsf{GF}$-strategies).

Consider a non-empty finite set of outcomes $\mathsf{O}$, a game form
$\mathcal{F}\in\mathsf{Form}(\mathsf{O})$, an environment $E=\langle
c,e,p\rangle\in\mathsf{Env}(\mathsf{O})$, and let $Y:=(\mathcal{F},E)$. A
Player-$\mathsf{A}$ $\mathsf{GF}$-strategy
$\sigma_{\mathsf{A}}\in\Sigma_{\mathsf{A}}(\mathcal{F})$ is said to be
_optimal_ w.r.t. $Y$ if the Player-$\mathsf{A}$ positional strategy
$\mathsf{s}_{\mathsf{A}}^{Y}(\sigma_{\mathsf{A}})$ is optimal in
$\mathcal{G}_{Y}$. The definition is analogous for Player $\mathsf{B}$.

Given a finite set of outcomes $\mathsf{O}$, we can now define the game forms
on $\mathsf{O}$ ensuring the existence of optimal strategies w.r.t. all
environments.

######  Definition 19 (Game forms with optimal strategies).

Consider a non-empty finite set of outcomes $\mathsf{O}$, a game form
$\mathcal{F}\in\mathsf{Form}(\mathsf{O})$ and some $n\in\mathbb{N}$.

Consider a Player $\mathsf{C}\in\\{\mathsf{A},\mathsf{B}\\}$. The game form
$\mathcal{F}$ is said to be _positionally maximizable up to_ $n$ w.r.t. Player
$\mathsf{C}$ if, for each environment $E\in\mathsf{Env}(\mathsf{O})$ with
$\mathsf{Sz}_{\mathsf{C}}(E)\leq n$, there is an optimal
$\mathsf{GF}$-strategy for Player $\mathsf{C}$ w.r.t. $(\mathcal{F},E)$.

When this holds for both Players, $\mathcal{F}$ is said to be _positionally
optimizable up to $n$_. The corresponding set of game forms is denoted
$\mathsf{ParO}(n)$. If this holds for all $n\in\mathbb{N}$, $\mathcal{F}$ is
simply said to be _positionally optimizable_ , and the corresponding set of
game forms is denoted $\mathsf{ParO}$.

######  Remark 20.

First, note that all game forms are positionally optimizable up to 0. This is
because environement of size 0 induce safety games. However, there are some
game forms that are not positionally maximizable w.r.t. any player up to 1.

Furthermore, by definition, from a game form
$\mathcal{F}\in\mathsf{Form}(\mathsf{O})$ that is not positionally optimizable
up to some $n\in\mathbb{N}$, there exists an environment
$E\in\mathsf{Env}(\mathsf{O})$ such that either of the players has no
positional optimal strategy in the simple parity game
$\mathcal{G}_{(\mathcal{F},E)}$ where the difference between
$\mathsf{col}(q_{\mathsf{init}})$ and the maximum of the colors appearing in
$\mathcal{G}_{(\mathcal{F},E)}$ is at most $n$.

In the game $\mathcal{G}_{(\mathcal{F},E)}$ depicted on the right of Figure 1,
Player $\mathsf{A}$ has positional optimal strategies: it suffices to play
both rows with positive probability. (This is similar for Player
$\mathsf{B}$.) As a side remark, the game form in the left of Figure 1 is
positionally optimizable.

In Lemma 21 below, we formulate more explicitly (using the notion of parity
domination from Definition 12) what optimal $\mathsf{GF}$-strategies are.

######  Lemma 21 (Proof C.4).

Consider a non-empty finite set of outcomes $\mathsf{O}$, a game form
$\mathcal{F}\in\mathsf{Form}(\mathsf{O})$, an environment $E=\langle
c,e,p\rangle\in\mathsf{Env}(\mathsf{O})$ and $Y:=(\mathcal{F},E)$. A
Player-$\mathsf{A}$ $\mathsf{GF}$-strategy
$\sigma_{\mathsf{A}}\in\Sigma_{\mathsf{A}}(\mathcal{F})$ is _optimal_ w.r.t.
$Y$ if and only if, letting $u:=\chi_{\mathcal{G}_{Y}}(q_{\mathsf{init}})$,
either (i) $u=0$, or (ii) the positional Player-$\mathsf{A}$ strategy
$\mathsf{s}^{Y}_{\mathsf{A}}(\sigma_{\mathsf{A}})$ parity dominates the
valuation $v_{Y}^{u}$.

Furthermore (ii) is equivalent to:

  * •

(1) the Player-$\mathsf{A}$ positional strategy
$\mathsf{s}^{Y}_{\mathsf{A}}(\sigma_{\mathsf{A}})$ dominates the valuation
$v_{Y}^{u}$, i.e. $\sigma_{\mathsf{A}}$ is optimal in the game in normal form
$\langle\mathcal{F},v^{u}_{Y}\circ p\rangle$; and

  * •

(2) for all $b\in\mathsf{Act}_{\mathsf{B}}$, if
$\mathsf{out}_{\langle\mathcal{F},\mathbbm{1}_{p^{-1}[0,1]}\rangle}(\sigma_{\mathsf{A}},b)=0$
(i.e. the probability under $\sigma_{\mathsf{A}}$ and $b$ to reach a stopping
state is null), then
$\max(\mathsf{Color}(\mathcal{F},p,\sigma_{\mathsf{A}},b)\cup\\{c\\})$ is even
where $\mathsf{Color}(\mathcal{F},p,\sigma_{\mathsf{A}},b):=\\{i\in\llbracket
0,e\rrbracket\mid\mathsf{out}_{\langle\mathcal{F},\mathbbm{1}_{p^{-1}[k_{i}]}\rangle}(\sigma_{\mathsf{A}},b)>0\\}$
is the set of colors that can be seen with positive probability under
$\sigma_{\mathsf{A}}$ and $b$.

This is symmetrical for Player $\mathsf{B}$.

######  Remark 22.

Informally, this proposition states that for a Player-$\mathsf{A}$
$\mathsf{GF}$-strategy $\sigma_{\mathsf{A}}$ to be optimal in a simple game
$\mathcal{G}_{Y}$ with positive value, it must be the case that for every
Player-$\mathsf{B}$ action $b$: either there is a positive probability (w.r.t.
$\sigma_{\mathsf{A}}$ and $b$) to exit $q_{\mathsf{init}}$ and the expected
value of the stopping states visited is at least $u$; or the game loops on
$q_{\mathsf{init}}$ with probability $1$, and the maximum of the colors that
can be seen with positive probability (w.r.t. $\sigma_{\mathsf{A}}$ and $b$)
is even. In particular, if
$c\leq\max\mathsf{Color}(\mathcal{F},p,\sigma_{\mathsf{A}},b)$ or if $c$ is
odd, then $\max\mathsf{Color}(\mathcal{F},p,\sigma_{\mathsf{A}},b)$ is even.

##  5 The main theorem

$\mathcal{F}:=\begin{bmatrix}y&x\\\ x&y\end{bmatrix}$

  * $\bullet$

$E:=\langle 2,4,p\rangle$;

  * $\bullet$

$p(x):=1/2$;

  * $\bullet$

$p(y):=k_{3}$.

2$q_{\mathsf{init}}$,$\begin{bmatrix}k_{3}&1/2\\\
1/2&k_{3}\end{bmatrix}$0$k_{0}$1$k_{1}$2$k_{2}$3$k_{3}$4$k_{4}$$1/2$

Figure 1: On the left, a game form on the set of outcomes
$\mathsf{O}:=\\{x,y\\}$, in the middle the description of an environment on
$\mathsf{O}$ and on the right the parity game $\mathcal{G}_{(\mathcal{F},E)}$
obtained from what is depicted on the left. The dashed state is a stopping of
value $1/2$.

The goal of this section is to formally state the main theorem of this paper,
Theorem 25 below. Informally, this theorem consists in extracting, for every
state of a game and for each Player, a local environment which will summarize
the context of the state to the Player, and tell her how to play optimally
(and positionally).

Before stating this theorem, let us recall and define below some useful
notations, in particular we recall the notation for value slices.

######  Definition 23 (Value slice).

Consider a parity game $\mathcal{G}$. For all subsets of states $S\subseteq
Q$, we denote by $V_{S}:=\\{u\in[0,1]\mid\exists q\in
S,\;\chi_{\mathcal{G}}(q)=u\\}$ the finite set of values of states in $S$.
Furthermore, for all $u\in V_{Q}$, we let $Q_{u}:=\\{q\in
Q\mid\chi_{\mathcal{G}}(q)=u\\}$ be the set of states whose value is $u$: it
is the $u$-slice of $\mathcal{G}$. Finally, for all $u\in V_{Q}$, we let
$e_{u}:=\mathsf{Even}(\mathsf{col}[Q_{u}])$ and
$o_{u}:=\mathsf{Odd}(\mathsf{col}[Q_{u}])$.

We also introduce the notion of positional strategies generated by an
environment function: this is a strategy that, at each state, plays a
$\mathsf{GF}$-strategy that is optimal in the corresponding environment.

######  Definition 24 (Positional strategy generated by an environment
function).

For all environment functions
$\mathsf{Ev}:Q\rightarrow\mathsf{Env}(\mathsf{O})$, a Player-$\mathsf{A}$
positional strategy $\mathsf{s}_{\mathsf{A}}$ is _generated_ by $\mathsf{Ev}$
if for all $q\in Q$, the $\mathsf{GF}$-strategy $\mathsf{s}_{\mathsf{A}}(q)$
is optimal w.r.t. $(\mathsf{F}(q),\mathsf{Ev}(q))$.

This is similar for Player $\mathsf{B}$.

We can now state the main result of this chapter: Theorem 25.

######  Theorem 25.

Let $\mathcal{G}=\langle\mathcal{C},\mathsf{col}\rangle$ be a parity game.
Assume that for all $q\in Q$, letting $u:=\chi_{\mathcal{G}}(q)\in[0,1]$, the
game form $\mathsf{F}(q)$ is:

  * •

positionally maximizable up to $e_{u}-\mathsf{col}(q)$ w.r.t. Player
$\mathsf{A}$; and

  * •

positionally maximizable up to $o_{u}-\mathsf{col}(q)$ w.r.t. Player
$\mathsf{B}$.

Then, there is a function
$\mathsf{Ev}_{\mathsf{A}}:Q\rightarrow\mathsf{Env}(\mathsf{O})$ (resp.
$\mathsf{Ev}_{\mathsf{B}}$) such that all Player-$\mathsf{A}$ (resp.
Player-$\mathsf{B}$) positional strategies $\mathsf{s}_{\mathsf{A}}$ (resp.
$\mathsf{s}_{\mathsf{B}}$) generated by $\mathsf{Ev}_{\mathsf{A}}$ (resp.
$\mathsf{Ev}_{\mathsf{B}}$) are optimal in $\mathcal{G}$; and such strategies
exist.

######  Remark 26.

Given some $u\in V_{Q}$, one can realize that the requirement at states
$q,q^{\prime}\in Q_{u}$ changes depending on the color of $q$ and
$q^{\prime}$. More specifically, if
$\mathsf{col}(q)<\mathsf{col}(q^{\prime})$, then the requirement at state $q$
is (a priori) stronger than the requirement at state $q^{\prime}$ since the
game form $\mathsf{F}(q)$ should behave well for environments of larger size
than the game form $\mathsf{F}(q^{\prime})$.

The remainder of this section and the entirety of the next is devoted to the
explanation of the construction of the environment function
$\mathsf{Ev}_{\mathsf{A}}$ (the construction being similar for Player
$\mathsf{B}$), hence we are taking the point of view of Player $\mathsf{A}$.
First, let us argue that we can restrict ourselves to a specific $u$-slice
$Q_{u}$ for some $u\in V_{Q}$. Such a restriction is properly defined (using
stopping states) in Definition 27 below.

######  Definition 27 (Game restricted to a $u$-slice).

For all $u\in V_{Q}$, we let $\mathcal{G}^{u}$ be the concurrent game
$\mathcal{G}$ where all states outside $Q_{u}$ are made stopping states: for
every $q\in Q\setminus Q_{u}$, we set
$\mathsf{val}(q)\leftarrow\chi_{\mathcal{G}}(q)$. The states, game forms and
coloring function on $Q_{u}$ are left unchanged.

Interestingly, a Player-$\mathsf{A}$ positional strategy optimal in
$\mathcal{G}$ can be obtained by merging appropriate positional strategies
$\mathsf{s}_{\mathsf{A}}^{u}$ in the games $\mathcal{G}^{u}$ for all $u\in
V_{Q}\setminus\\{0\\}$, which is actually a straightforward consequence of
Theorem 13.

######  Lemma 28 (Proof C.5).

Consider a parity game $\mathcal{G}$. For all $u\in V_{Q}\setminus\\{0\\}$,
consider a positional Player-$\mathsf{A}$ strategy
$\mathsf{s}_{\mathsf{A}}^{u}$ that parity dominates the valuation
$\chi_{\mathcal{G}}$ in $\mathcal{G}^{u}$. Then, the Player-$\mathsf{A}$
positional strategy $\mathsf{s}_{\mathsf{A}}$ such that
$\mathsf{s}_{\mathsf{A}}(q):=\mathsf{s}_{\mathsf{A}}^{u}(q)$ for all $u\in
V_{Q}\setminus\\{0\\}$ and $q\in Q_{u}$ guarantees the valuation
$\chi_{\mathcal{G}}$ in $\mathcal{G}$ (i.e. it is optimal).

##  6 The proof

In Appendix D, we give a quick overview of the technical properties and lemmas
that we show in the appendix and that we will use to prove the lemmas (we will
state later in this chapter) leading to the proof of Theorem 25.

In this section, we fix a parity game
$\mathcal{G}=\langle\mathcal{C},\mathsf{col}\rangle$. In particular, the set
of states $Q$ is fixed: r ecall that $Q$ is also the set of outcomes of all
game forms occurring in $\mathcal{G}$. Also, Lemma 28 above justifies that we
focus on a given $u$-slice $Q_{u}$ for some positive $u\in(0,1]$. We also let
$e:=e_{u}$, $o:=o_{u}$ and $K:=\\{k_{i}\mid i\in\llbracket 0,e\rrbracket\\}$
and for all $n\in\llbracket 0,e\rrbracket$, we let $K^{n}:=\\{k_{i}^{n}\mid
i\in\llbracket 0,e\rrbracket\\}$.

###  6.1 Big picture of the proof

In order to give an idea of the steps that we take to prove Theorem 25, let us
first consider the very simple case of finite turn-based deterministic
reachability games. In this setting, computing the area $L_{\mathsf{A}}$ from
which Player $\mathsf{A}$ has a winning strategy can be done inductively. That
is, initially we set $L_{\mathsf{A}}:=T$ where $T$ denotes the target that
Player $\mathsf{A}$ wants to reach. Then, the inductive step is handled with a
(deterministic) attractor: we add to $L_{\mathsf{A}}$ any Player-$\mathsf{A}$
state with a successor in $L_{\mathsf{A}}$ and any Player-$\mathsf{B}$ state
with all successors in $L_{\mathsf{A}}$. After finitely many steps, there is
no more state to add in $L_{\mathsf{A}}$: this exactly corresponds to the
states from which Player $\mathsf{A}$ has a winning strategy.

Computing a single attractor is not merely enough to take into account the
intricate behavior of parity objectives, which is what Theorem 25 deals with.
Therefore, we are going to iteratively compute several layers of (virtual)
colors, with a local update to change the (virtual) color (and therefore the
layer it belongs to) of a state. This local update can be seen as an attractor
except in a concurrent stochastic setting. Hence, when we update the (virtual)
color of a state, we take into account the concurrent interaction of the
players at each state along with the probability to see stopping states or
states with different (virtual) colors. We define this local update in
Subsection 6.3. Let us describe below the steps that we take to capture the
behavior of the parity objective.

We compute layers of successive probabilistic attractors with leaks towards
the stopping states. Although we compute a strategy, e.g., for Player
$\mathsf{A}$, we alternate players to build layers, then move the last non-
empty layer into the closest layer with same parity, then backtrack the
attractor computation from this layer downwards, and start over again the full
attractor computation on the new layer structure. In a more concrete way, let
us assume below that the highest color in the $u$-slice is $6$. We proceed as
follows:

$q_{3}$3$q_{2}$2$q_{4}$4$q_{1}$1

Figure 2: A (deterministic turn-based) game.

  1. 1.

Add the states colored with $6$ to layer $L_{6}$.

  2. 2.

Recursively add to $L_{6}$ the states where Player $\mathsf{A}$ can guarantee
that with positive probability (pp) either a leak towards stopping states
occurs now and its expected explicit value is $u$ or more
($\mathsf{Leak}_{\geq u}$), or with pp the next state is in $L_{6}$, i.e. with
pp color $6$ or $\mathsf{Leak}_{\geq u}$ will occur.

  3. 3.

Add the remaining states colored with $5$ to layer $L_{5}$.

  4. 4.

Recursively add to $L_{5}$ the states where Player $\mathsf{B}$ can guarantee
that either $\mathsf{Leak}_{<u}$ occurs now with pp, or the next state is
surely not in $L_{6}$ and with pp in $L_{5}$; i.e. if $\mathsf{Leak}_{<u}$
occurs with probability $0$, then color $6$ will not occur but color $5$ will
eventually occur with pp.

  5. 5.

Add the remaining states colored with $4$ to layer $L_{4}$.

  6. 6.

Recursively add to $L_{4}$ the states where Player $\mathsf{A}$ can guarantee
that either $\mathsf{Leak}_{\geq u}$ will occur with pp, or the maximal layer
index of the next states seen with pp is $4$ or $6$, i.e. even and at least
$4$.

  7. 7.

And so on, from color $3$ to $0$. The layers so far only give information
about what can happen at finite horizon.

  8. 8.

For instance, from $L_{2}$, Player $\mathsf{A}$ can guarantee that either
$\mathsf{Leak}_{\geq u}$ will occur with pp, or the maximal color that will be
seen with pp is in $\\{2,4,6\\}$. Now, if e.g. $L_{0}=L_{1}=\emptyset$, we
merge $L_{2}$ into $L_{4}$. This is, arguably, the most surprising step, let
us try to give a conceptual intuition behind this step, we will then
illustrate it on a concrete example. Consider what happens in the $L_{2}$
layer, assuming $L_{0}=L_{1}=\emptyset$. From states in that layer, either:

     * •

$\mathsf{Leak}_{\geq u}$ occurs with pp;

     * •

otherwise, $L_{3}\cup L_{4}\cup L_{5}\cup L_{6}$ occurs with pp, and the
maximum index seen with pp is even;

     * •

otherwise, the game loops surely in $L_{2}$, and with pp the maximum color
seen is $2$. In that case, Player $\mathsf{A}$ wins the (real) parity game
almost-surely.

In other words, either the game loops in $L_{2}$ and Player $\mathsf{A}$ wins,
or what happens is alike to what happens in the layer $L_{4}$. In Figure 2
without dotted state $q_{1}$ where Player $\mathsf{B}$ plays alone,
$L_{4}=\\{q_{4}\\}$, then $L_{3}=\\{q_{3}\\}$, then $L_{2}=\\{q_{2}\\}$, but
if the play stays in $L_{2}$, Player $\mathsf{A}$ wins, so Player $\mathsf{B}$
may just as well go to $q_{4}$ since there is no $L_{0},L_{1}$ below to
escape. However, in Figure 2 with dotted state $q_{1}$, Player $\mathsf{B}$
can leave $L_{2}$ via $L_{1}\neq\emptyset$, avoid color $4$, and win. There
$L_{2}$ and $L_{4}$ are not alike. Hence, we do not merge them.

  9. 9.

Earlier, some states of color $1$ may have been added to $L_{3}$ since $L_{3}$
”overruled” $L_{2}$ w.r.t indices, but since $L_{2}$ has just been merged into
$L_{4}$, it now overrules $L_{3}$, so some states from $L_{3}$ may have to go
back to $L_{1}$. Therefore we reset the layers below $L_{4}$ and repeat the
above attractor alternation all over again, until all the states are
eventually in $L_{6}$ as we shall prove.

The key property that is growing throughout the above computation and will
hold in the final $L_{6}$ involves layer games: the $L_{n}$-game is derived
from the $u$-slice by abstracting each $L_{i}$ with $i\neq n$ via one state
$k_{i}^{n}$ from which the player who dislikes the parity of $n$ chooses any
next state in $L_{n}$, making it harder for the other to win. If $i>n$ then
$k_{i}^{n}$ is $i$-colored, else $(n-1)$-colored, also making it harder for
the other to win. And states in $L_{n}$ bear their true colors. See for
instance Figure 5. The $L_{n}$-game is only seemingly harder to win: it is
actually equivalently hard, but its useful properties are easier to prove.

The key growing property is as follows: between two merges, the attractor
computation from the top layer down to $L_{n}$ ensures that Player
$\mathsf{A}$ has a positional strategy of value at least $u$ in each $L_{i}$
for even $i\geq n$, and Player $\mathsf{B}$ less than $u$ for odd $i\geq n$.
In the very end, there is only one even layer with all states bearing their
true colors, and no abstract states, so the last layer game equals the
$u$-slice game, for which we have thus computed a positional optimal strategy.

Let us hint at how to show positional optimality in the $L_{n}$-games when it
holds: we break $L_{n}$ each into one simple parity game built on
$\mathsf{F}(q)$ per state $q$ in $L_{n}$, abstracting the other states in
$L_{n}$ into one. Our theorem assumption yields an optimal
$\mathsf{GF}$-strategy for Player $\mathsf{A}$ or $\mathsf{B}$ in the simple
parity game. Gluing them does the job.

Now recall the above example of computation, where Player $\mathsf{A}$ for
even indices, and Player $\mathsf{B}$ for odd ones, guarantees (assuming
neither $\mathsf{Leak}_{\geq u}$ nor $\mathsf{Leak}_{<u}$ occurs):

  * •

in $L_{6}$, that a next state is of color 6 with pp;

  * •

in $L_{5}$, that the next state is surely not of color 6, and with pp a next
state is of color 5;

  * •

in $L_{4}$, that a next state is of color 6 with pp or surely the next state
is not of color 5, and with pp a next state is of color 4;

  * •

in $L_{3}$, that the next state is surely not of color 6 and that the next
state is of color 5 with pp or surely the next state is not of color 4, and
with pp a next state is of color 3; etc.

One can realize that the furthest the layer is from the maximal color (that is
6), the more complex the requirement is at that layer. That is why the
strength of our assumption on the game form induced at some state increases
with the difference between maximal true color in the $u$-slice and the true
color (at most $n$) of the state, as stated in Remark 26. We will discuss this
further in the next chapter. In particular, we will show that there is an
infinite strict hierarchy between these assumptions.

###  6.2 Extracting an environment function from a parity game

Once restricted to the game $\mathcal{G}^{u}$, the method that we use to prove
Theorem 25 consists in iteratively building a pair of (virtual) coloring and
environment functions ensuring a nice property (namely _faithfulness_ ,
defined below in Definition 42). For the remainder of this section, we
illustrate the definitions and lemmas on the game depicted in Figures 4 and 4.

Figure 3: The depiction of a game restricted to the $1/2$-slice $Q_{1/2}$ with
the initial coloring function $\mathsf{col}$.

Figure 4: The same game restricted to $Q_{1/2}$ with a different coloring
function $\mathsf{vcol}$.

######  Example 29.

We explain the notations used to depict this game (it is in fact the same
arena in both Figures 4 and 4, with different coloring functions – real or
virtual). On the sides in green are the slices $Q_{0},Q_{1/4},Q_{3/4}$ and
$Q_{1}$ from left to right. We focus on the central slice $Q_{1/2}$. In
$Q_{1/2}$, there are seven states, five of which (the square-shaped ones) are
turn-based for Player $\mathsf{B}$, that is, Player $\mathsf{A}$ has only one
available action. On the other hand, the two circled-shaped states ${q}_{0}$
and ${q}_{5}$ are “truly” concurrent in the sense that both players have
several actions available. Furthermore, note that only one stochastic outcome
(of a local interaction) is drafted as a black dot: from ${q}_{4}$, Player
$\mathsf{B}$ may either loop on ${q}_{4}$ or go with equal probability to
${q}_{0}$ and ${q}_{6}$. The other arrows lead to a single state and the
outcomes of the game forms in ${q}_{0}$ or ${q}_{5}$ is a single state or a
value: $1$ or $1/2$. These formally refer to a (distribution over) stopping
states outside of the $1/2$-slice $Q_{1/2}$. The horizontal layers depict the
colors of the states. In Figure 4, the coloring function considered is the
initial one $\mathsf{col}$ whereas in Figure 4 we have depicted a (virtual)
coloring function $\mathsf{vcol}$. For instance, $\mathsf{col}({q}_{6})=3$
whereas $\mathsf{col}({q}_{5})=2$. Similarly, $\mathsf{vcol}({q}_{6})=3$
whereas $\mathsf{vcol}({q}_{5})=4$. Note that, in Figure 4, the real colors
(given by $\mathsf{col}$) are reminded next to some states with circled
numbers. Finally, note that $e:=e_{1/2}=4$.

Given a (virtual) coloring function, we need to extract local environments
from the parity game $\mathcal{G}$, which summarize how the Players see their
neighboring states via the virtual coloring function. This is (partly) done in
Definition 30.

######  Definition 30 (Probability function extracted from an arena and a
(virtual) coloring function).

Consider a virtual coloring function $\mathsf{vcol}:Q_{u}\rightarrow\llbracket
0,e\rrbracket$. For all $n\in\llbracket 0,e\rrbracket$, we let
$Q_{n}:=\mathsf{vcol}^{-1}[n]$. We then define the map
$p_{n,\mathsf{vcol}}:Q\rightarrow Q_{n}\uplus K^{n}\uplus V_{Q\setminus
Q_{u}}$ such that, for all $q\in Q$:

  * •

if $q\in Q_{n}$, $p_{n,\mathsf{vcol}}(q):=q\in Q$;

  * •

if $q\in Q_{u}\setminus Q_{n}$,
$p_{n,\mathsf{vcol}}(q):=k^{n}_{\mathsf{vcol}(q)}\in K^{n}$;

  * •

if $q\in Q\setminus Q_{u}$, $p_{n,\mathsf{vcol}}(q):=\chi_{\mathcal{G}}(q)\in
V_{Q\setminus Q_{u}}$.

Given a (virtual) coloring function $\mathsf{vcol}:Q_{u}\rightarrow\llbracket
0,e\rrbracket$ and a color $n\in\llbracket 0,e\rrbracket$, we can now extract
a smaller parity game from $\mathcal{G}$ where the states with non-trivial
game forms are the states in $\mathsf{vcol}^{-1}[n]$, the states in
$Q\setminus Q_{u}$ are stopping states and the arena loops back to
$\mathsf{vcol}^{-1}[n]$ when a state in $Q_{u}\setminus\mathsf{vcol}^{-1}[n]$
is seen. This is done below in Definition 31.

######  Definition 31 (Parity game extracted from the $u$-slice).

Consider a virtual coloring function $\mathsf{vcol}:Q_{u}\rightarrow\llbracket
0,e\rrbracket$ and a color $n\in\llbracket 0,e\rrbracket$. Let
$\mathsf{C}\in\\{\mathsf{A},\mathsf{B}\\}$ be a Player: $\mathsf{A}$ if $n$ is
odd and $\mathsf{B}$ if $n$ is even. The arena
$\mathcal{C}_{\mathsf{vcol}}^{n}=\langle
Q^{\prime},\mathsf{F}^{\prime}\rangle$ along with the coloring function
$\mathsf{vcol}_{n}:Q^{\prime}\rightarrow\mathbb{N}$ are such that, denoting
$Q_{n}:=\mathsf{vcol}^{-1}[n]$:

  * •

$Q^{\prime}:=Q_{n}\cup K^{n}\cup V_{Q\setminus Q_{u}}$ where all $x\in
V_{Q\setminus Q_{u}}$ are stopping states with $\mathsf{val}(x)\leftarrow x$;

  * •

for all $q\in Q_{n}$,
$\mathsf{F}^{\prime}(q):=\mathsf{F}(q)^{p_{n,\mathsf{vcol}}}=\langle\mathsf{Act}_{\mathsf{A}}^{q},\mathsf{Act}_{\mathsf{B}}^{q},Q^{\prime},\varrho_{p_{n,\mathsf{vcol}}}\rangle$
where, for all $\sigma_{\mathsf{A}}\in\mathsf{Act}_{\mathsf{A}}^{q}$,
$\sigma_{\mathsf{B}}\in\mathsf{Act}_{\mathsf{B}}^{q}$, and $q\in Q$, we have
$\varrho_{p_{n,\mathsf{vcol}}}(\sigma_{\mathsf{A}},\sigma_{\mathsf{B}})(q):=\varrho(\sigma_{\mathsf{A}},\sigma_{\mathsf{B}})[p_{n,\mathsf{vcol}}^{-1}[q]]$;

  * •

for all $k\in K^{n}$, we set $\mathsf{F}^{\prime}(k)$ as a Player-$\mathsf{C}$
state whose outcomes are all the states in $Q_{n}$;

  * •

for all $q\in Q_{n}$, we let $\mathsf{vcol}_{n}(q):=\mathsf{col}(q)$ and for
all $i\in\llbracket 0,e\rrbracket$, we have
$\mathsf{vcol}_{n}(k_{i}^{n}):=\max(i,n-1)$.

For $t\in[0,1]$, we define the valuation
$v_{n,\mathsf{vcol}}^{t}:Q^{\prime}\rightarrow[0,1]$:
$v_{n,\mathsf{vcol}}^{t}[Q_{n}\cup K^{n}]:=\\{t\\}$ and for all $x\in
V_{Q\setminus Q_{u}}$, $v_{n,\mathsf{vcol}}^{t}(x):=x$.

The game $\mathcal{L}_{\mathsf{vcol}}^{n}$ is then equal to
$\mathcal{L}_{\mathsf{vcol}}^{n}=\langle\mathcal{C}^{n}_{\mathsf{vcol}},\mathsf{vcol}_{n}\rangle$.

######  Remark 32.

First, the notation $\mathcal{L}^{n}_{\mathsf{vcol}}$ comes from the fact that
the game is extracted for the $n$-colored layer w.r.t. the coloring function
$\mathsf{vcol}$. The idea behind Definition 31 is the following: the states of
interest are those of $Q_{n}$, that is, those for which the virtual color
given by $\mathsf{vcol}$ is $n$. Note however that the colors of these states
in $\mathcal{L}^{n}_{\mathsf{vcol}}$ are given by the real coloring function
$\mathsf{col}$. On the other hand, for all $i\in\llbracket 0,e\rrbracket$, the
state $k_{i}^{n}$ in $\mathcal{L}^{n}_{\mathsf{vcol}}$ corresponds to the
states in $\mathcal{G}^{u}$ colored with $i$ w.r.t. $\mathsf{vcol}$. In the
case where $n$ is even, as formally defined later in Definition 40, we will
require that any Player-$\mathsf{A}$ positional strategy generated by a given
environment has value at least $u$, in the game
$\mathcal{L}^{n}_{\mathsf{vcol}}$, from all states in $Q_{n}$. However, all
states $k^{n}_{i}$ for $i\in\llbracket 0,e\rrbracket$ are
Player-$\mathsf{B}$’s, who can then choose to loop back to any state in
$Q_{n}$. Therefore, given a Player-$\mathsf{A}$ positional strategy
$\mathsf{s}_{\mathsf{A}}$, if the game cannot exit to any stopping state, for
the strategy $\mathsf{s}_{\mathsf{A}}$ not to have value 0, the game may loop
on some $k_{i}^{n}$ only at the condition that the highest color seen with
positive probability is even. In addition, note that the color of the state
$k^{n}_{i}$ for $i\in\llbracket 0,n-1\rrbracket$ is $n-1$ (which is odd).
Hence, all other things being equal, the game is harder for Player
$\mathsf{A}$ when $n=4$ than when $n=2$ or $0$. Finally, note that, when $n$
is odd, we will require that any Player-$\mathsf{B}$ positional strategy
generated by a given environment has value less than $u$.

3$k_{3}^{3}$4$k_{4}^{3}$$q_{4}$2$q_{6}$32$k_{0}^{3}$2$k_{1}^{3}$2$k_{2}^{3}$

Figure 5: The game $\mathcal{L}^{3}_{\mathsf{vcol}}$. For readability, exiting
arrows from $k_{0}^{3},k_{1}^{3},k_{2}^{3},k_{3}^{3}$ and $k_{4}^{3}$ are not
depicted: they would all loop back to both ${q}_{4}$ and ${q}_{6}$.

0$q_{\mathsf{init}}$,$\begin{bmatrix}k_{3}&k_{0}&1\\\
k_{4}&k_{0}&k_{3}\end{bmatrix}$0$k_{0}$1$k_{1}$2$k_{2}$3$k_{3}$4$k_{4}$$1$

Figure 6: The game $\mathcal{G}_{q_{0},\mathsf{vcol}}^{0}$ with
$\mathsf{vcol}$ the coloring function depicted in Figure 4.

######  Example 33.

The game $\mathcal{L}^{3}_{\mathsf{vcol}}$ is partly depicted in Figure 5 (the
virtual coloring function $\mathsf{vcol}$ being the one depicted in Figure 4).
The colors of the states are depicted in red. Although the arrows are not
depicted, from all states $k_{0}^{3},k_{1}^{3},k_{2}^{3},k_{3}^{3}$ and
$k_{4}^{3}$ Player $\mathsf{A}$ can decide to which state among
$\\{q_{4},q_{6}\\}$ to loop back (since $n=3$ is odd). In an even-colored
layer, it would have been Player $\mathsf{B}$ to decide.

Given a virtual coloring function, we also associate a local environment with
each state.

######  Definition 34 (Local environment induced by a virtual coloring
function and a color).

Consider a state $q\in Q_{u}$ and a coloring function
$\mathsf{vcol}:Q_{u}\rightarrow\llbracket 0,e\rrbracket$. We define
$p_{q,\mathsf{vcol}}:Q\rightarrow\\{q_{\mathsf{init}}\\}\cup K_{e}\cup[0,1]$
similarly to how we define $p_{n,\mathsf{vcol}}$ in Definition 30. That is,
for all $q^{\prime}\in Q$, we have:

  * •

if $q^{\prime}=q$, $p_{q,\mathsf{vcol}}:=q_{\mathsf{init}}$;

  * •

if $q^{\prime}\in Q_{u}\setminus\\{q\\}$,
$p_{q,\mathsf{vcol}}:=k_{\mathsf{vcol}(q^{\prime})}\in K_{e}$;

  * •

if $q^{\prime}\in Q\setminus Q_{u}$,
$p_{q,\mathsf{vcol}}(q):=\chi_{\mathcal{G}}(q)\in[0,1]$.

Then, for all $n\in\llbracket 0,e\rrbracket$, the environment
$E^{n}_{q,\mathsf{vcol}}$ associated with state $q$ w.r.t. $\mathsf{vcol}$ and
$n$ is such that
$E^{n}_{q,\mathsf{vcol}}:=\langle\max(c_{n},\mathsf{vcol}(q)),e,p_{q,\mathsf{vcol}}\rangle$
where $c_{n}=n+1$ if $n$ is odd and $c_{n}:=n-1$ if $n$ is even. We say that
the coloring function $\mathsf{vcol}$ is _associated_ with the environment
$E^{n}_{q,\mathsf{vcol}}$.

The corresponding (local) game
$\mathcal{G}_{(\mathsf{F}(q),E^{n}_{q,\mathsf{vcol}})}$ (see Definition 16) is
denoted $\mathcal{G}_{q,\mathsf{vcol}}^{n}$. For all $x\in[0,1]$, we set
$v_{q,\mathsf{vcol}}^{x}:=v^{x}_{(\mathsf{F}(q),E^{0}_{q,\mathsf{vcol}})}$
(see Definition 16).

The definition of $c_{n}$ may seem ad hoc. We give an explanation of this
definition below in the next subsection.

######  Example 35.

The game $\mathcal{G}^{n}_{q_{5},\mathsf{col}}$ is depicted on the right of
Figure 1 for $n=0,1,2$. However, if $n=3$, the color of $q_{\mathsf{init}}$
would be 4, and if $n=4$, it would be 3. The game
$\mathcal{G}^{n}_{q_{0},\mathsf{vcol}}$ is depicted in Figure 6 for $n=0$.
However, if $n=1$, the color of $q_{\mathsf{init}}$ would be 2, if $n=2$, the
color would be 1, if $n=3$, the color would be 4 and if $n=4$ the color would
be 3.

###  6.3 Local Operator

We want to define a way to update a (virtual) coloring function
$\mathsf{vcol}$. This will be done via a local operator mapping a given state
$q$ to the best color $k$ for which Player $\mathsf{A}$ can achieve the value
$u$ in the corresponding local parity game
$\mathcal{G}^{k}_{q,\mathsf{vcol}}$. Note that “best” is to be understood
considering an ordering compatible with the parity objective. Specifically,
taking the point-of-view of Player $\mathsf{A}$, any even number is better
than any odd number, and when they increase, odd numbers get worse whereas
even numbers get better. This induces a new ordering.

######  Definition 36 (Parity order).

We define a total strict order relation $\prec_{\mathsf{par}}$ on $\mathbb{N}$
such that, for all $m,n\in\mathbb{N}$, we have $m\prec_{\mathsf{par}}n$ if:
$m$ is odd and $n$ is even; or $m>n$ and $m$ and $n$ are odd; or $m<n$ and $m$
and $n$ are even.

######  Definition 37 (Local operator).

Consider a state $q\in Q_{u}$ and a (possibly virtual) coloring function
$\mathsf{vcol}:Q_{u}\rightarrow\llbracket 0,e\rrbracket$. The color
$\mathsf{NewCol}(q,\mathsf{vcol})\in\mathbb{N}$ induced by $\mathsf{vcol}$ at
$q$ is defined by:

$\mathsf{NewCol}(q,\mathsf{vcol}):=\max_{\prec_{\mathsf{par}}}\\{n\in\llbracket
0,e\rrbracket\mid\chi_{\mathcal{G}_{q,\mathsf{vcol}}^{n}}(q_{\mathsf{init}})\geq
u\\}$

The meaning of a new virtual color $n$ assigned to a state $q$ via
$\mathsf{NewCol}$ is the following: in the game $\mathcal{G}^{u}$ with the
coloring function $\mathsf{vcol}$, from state $q$ and in at most one step, the
highest color w.r.t. $\mathsf{vcol}$ seen with positive probability when both
players play optimally is $n$ (and no stopping state is seen).

Let us now explain the choice of $c_{n}$ in Definition 34. In a local
environment parameterized by $n$, the integer $n$ induces a shifted parity
objective for Player $\mathsf{A}$: her objective is that the maximal color
seen infinitely often is at least $n$ w.r.t. $\prec_{\mathsf{par}}$; in
particular $n=0$ induces the usual parity objective. The value $c_{n}$ encodes
that winning condition. For instance, if $n=2$, assuming $\mathsf{vcol}(q)=0$
for simplicity, then $c_{n}=1$, which implies that seeing $0$ infinitely often
is not enough, but seeing $2$ infinitely often is enough to win. Similarly, if
$n=1$, $c_{n}=2$, which implies that seeing $1$ infinitely often is now enough
to win, but seeing $3$ infinitely often is still losing.

######  Remark 38.

Assume for instance that $\mathsf{NewCol}(q,\mathsf{vcol})=2$ for some state
$q\in Q$ and some (virtual) coloring function $\mathsf{vcol}$222In particular,
it must be the case that $\mathsf{vcol}(q)\leq 2$, see Proposition 66.. In
particular, Player $\mathsf{A}$ has a $\mathsf{GF}$-strategy
$\sigma_{\mathsf{A}}$ optimal w.r.t. $(\mathcal{F},E^{2}_{q,\mathsf{vcol}})$,
which yields a value at least $u$, and Player $\mathsf{B}$ has a
$\mathsf{GF}$-strategy $\sigma_{\mathsf{B}}$ optimal w.r.t.
$(\mathcal{F},E^{4}_{q,\mathsf{vcol}})$, which yields a value less than $u$.
Remember that all games $\mathcal{G}^{k}_{q,\mathsf{vcol}}$ (where $k$ ranges
over $\llbracket 0,e\rrbracket$) share the same structure and that only the
color of $q_{\mathsf{init}}$ changes. Consider what happens in the game
$\mathcal{G}^{0}_{q,\mathsf{vcol}}$ (where the state $q_{\mathsf{init}}$ is
colored by $\mathsf{vcol}(q)$) when playing strategies $\sigma_{\mathsf{A}}$
and $\sigma_{\mathsf{B}}$. Recalling Remark 22, the game cannot exit to any
stopping state since the expected value of the stopping states reached would
be both at least $u$ (since $\sigma_{\mathsf{A}}$ is optimal in
$\mathcal{G}^{2}_{q,\mathsf{vcol}}$) and less than $u$ (since
$\sigma_{\mathsf{B}}$ is optimal in $\mathcal{G}^{4}_{q,\mathsf{vcol}}$);
hence this cannot happen. Furthermore, if some color of value at least $3$ is
seen with positive probability, then the highest such color must be both even
(since $\sigma_{\mathsf{A}}$ is optimal in
$\mathcal{G}^{2}_{q,\mathsf{vcol}}$) and odd (since $\sigma_{\mathsf{B}}$ is
optimal in $\mathcal{G}^{4}_{q,\mathsf{vcol}}$). In fact, the highest color
seen with positive probability in $\mathcal{G}^{0}_{q,\mathsf{vcol}}$ under
$\sigma_{\mathsf{A}}$ and $\sigma_{\mathsf{B}}$ is $2$ and neither of the
players can do better (w.r.t. the ordering $\prec_{\mathsf{par}}$). From this,
we can infer the semantics of a virtual color $n$ assigned to a state $q$ via
operator $\mathsf{NewCol}$ (i.e. a color given by a virtual coloring
function): in the game $\mathcal{G}^{u}$ with coloring function
$\mathsf{vcol}$, from state $q$ and in at most one step, the highest color
w.r.t. $\mathsf{vcol}$ seen with positive probability is $n$ (and no stopping
state can be seen).

Let us exemplify this operator on an example.

######  Example 39.

First, consider Figure 1 and let us compute
$\mathsf{NewCol}(q_{5},\mathsf{col})$. We can realize that, regardless of the
color of state $q_{\mathsf{init}}$, Player $\mathsf{A}$ can (positionally)
play both rows with positive probability and ensure reaching (almost-surely)
the stopping state $1/2$. In fact, for all $n\in\llbracket 0,4\rrbracket$, we
have $\chi_{\mathcal{G}_{q_{5},\mathsf{col}}^{n}}(q_{\mathsf{init}})=1/2$.
Hence, $\mathsf{NewCol}(q_{5},\mathsf{col})=4$.

Consider now Figure 6 and let us compute
$\mathsf{NewCol}(q_{0},\mathsf{vcol})$. As mentioned in Example 35, the game
$\mathcal{G}^{4}_{q_{0},\mathsf{vcol}}$ corresponds to the game depicted in
Figure 6 except that $q_{\mathsf{init}}$ is colored with 3. One can realize
that, with this choice (of coloring of the state $q_{\mathsf{init}}$), if the
highest color $i\in\llbracket 0,4\rrbracket$ such that $k_{i}$ is seen
infinitely often is such that $i\prec_{\mathsf{par}}4$, then Player
$\mathsf{A}$ loses. The value of this game is 0 as Player $\mathsf{B}$ can
ensure looping on $k_{0}$ and $q_{\mathsf{init}}$ (by playing, positionally
and deterministically, the middle column) thus ensuring that the highest color
seen infinitely often is 3. Thus,
$\mathsf{NewCol}(q_{0},\mathsf{vcol})\prec_{\mathsf{par}}4$. In the game
$\mathcal{G}^{2}_{q_{0},\mathsf{vcol}}$, $q_{\mathsf{init}}$ is colored with
1. Again, with this choice (of coloring of the state $q_{\mathsf{init}}$), if
the highest color $i\in\llbracket 0,4\rrbracket$ such that $k_{i}$ is seen
infinitely often is such that $i\prec_{\mathsf{par}}2$, then Player
$\mathsf{A}$ loses. The value of this game is also 0 as Player $\mathsf{B}$
can still play the middle column ensuring that the highest color seen
infinitely often is 1. Thus,
$\mathsf{NewCol}(q_{0},\mathsf{vcol})\prec_{\mathsf{par}}2$. Consider now the
game $\mathcal{G}^{0}_{q_{0},\mathsf{vcol}}$, the one depicted in Figure 6.
The value of the state $q_{\mathsf{init}}$ is now 1. Indeed, if Player
$\mathsf{A}$ plays the two rows with equal probability, one can see that this
strategy parity dominates (see Definition 12) the valuation
$v_{q_{0},\mathsf{vcol}}^{1}$ (recall Definition 34). Indeed, the BSCCs
compatible with this strategy are $\\{q_{\mathsf{init}},k_{3},k_{4}\\}$ and
$\\{q_{\mathsf{init}},k_{0}\\}$ and they are even-colored. Hence, by Theorem
13, $\chi_{\mathcal{G}_{q_{1},\mathsf{col}}^{0}}(q_{\mathsf{init}})=1\geq 1/2$
and $\mathsf{NewCol}(q_{0},\mathsf{vcol})\succeq_{\mathsf{par}}0$. That is,
$\mathsf{NewCol}(q_{0},\mathsf{vcol})=0$.

Some of the properties enjoyed by the local operator $\mathsf{NewCol}$ are
given in the appendix in Page D.1.

###  6.4 Faithful coloring function

To prove Theorem 25, we iteratively build a (virtual) coloring function and a
local environment. We want to define the desirable property that the pair of
coloring and environment functions should satisfy that will be preserved step
by step. First, we need to define the notion of an environment function
witnessing a color.

######  Definition 40 (Environment witnessing a color).

Consider a coloring function $\mathsf{vcol}:Q_{u}\rightarrow\llbracket
0,e\rrbracket$, a color $n\in\llbracket 0,e\rrbracket$ and an environment
function $\mathsf{Ev}:Q_{n}\rightarrow\mathsf{Env}(Q)$ with
$Q_{n}:=\mathsf{vcol}^{-1}[n]$.

Assume that $n$ is even. We say that the pair $(\mathsf{vcol},\mathsf{Ev})$
_witnesses_ the color $n$ if for all $q\in Q_{n}$,
$\mathsf{Sz}_{\mathsf{A}}(\mathsf{Ev}(q))\leq e-\mathsf{col}(q)$ and all
positional Player-$\mathsf{A}$ strategies
$\mathsf{s}_{\mathsf{A}}\in\mathsf{S}_{\mathsf{A}}^{\mathcal{C}}$ generated by
$\mathsf{Ev}$ (recall Definition 24) in the game
$\mathcal{L}^{n}_{\mathsf{vcol}}$ parity dominate the valuation
$v_{n,\mathsf{vcol}}^{u}$ (recall Definition 31).

Assume that $n$ is odd. We say that the pair $(\mathsf{vcol},\mathsf{Ev})$
witnesses the color $n$, if for all $q\in Q_{n}$,
$\mathsf{Sz}_{\mathsf{B}}(\mathsf{Ev}(q))\leq o-\mathsf{col}(q)$ and for all
positional Player-$\mathsf{B}$ strategies
$\mathsf{s}_{\mathsf{B}}\in\mathsf{S}_{\mathsf{B}}^{\mathcal{C}}$ generated by
$\mathsf{Ev}$ in the game $\mathcal{L}^{n}_{\mathsf{vcol}}$, there is some
$u^{\prime}<u$, such that $\mathsf{s}_{\mathsf{B}}$ parity dominates the
valuation $v_{n,\mathsf{vcol}}^{u^{\prime}}$.

######  Remark 41.

The condition on the size of the environments considered along with the
assumptions of Theorem 25 ensures that the quantification over the strategies
generated by the environment function are not over the empty set.

This definition was hinted in Remark 32. Informally, it means that, in the
(virtual) games given by $\mathsf{vcol}$, in the even-colored layers, Player
$\mathsf{A}$ can achieve at least what she should be able to achieve in this
$u$-slice (i.e. the value of the states is at least $u$). Whereas, in the odd-
colored layers, Player $\mathsf{B}$ can prevent Player $\mathsf{A}$ from
achieving this.

We can now define the notion of faithful pair of coloring and environment
functions.

######  Definition 42 (Faithful pair of coloring and environment functions).

Consider a coloring function $\mathsf{vcol}:Q_{u}\rightarrow\llbracket
0,e\rrbracket$, some $n\in\llbracket 0,e+1\rrbracket$ and a partial
environment function $\mathsf{Ev}:Q_{u}\rightarrow\mathsf{Env}(Q)$ defined on
$\mathsf{vcol}^{-1}[\llbracket n,e\rrbracket]$. We say that
$(\mathsf{vcol},\mathsf{Ev})$ is _faithful down to_ $n$ if:

  * •

for all $k\in\llbracket n,e\rrbracket$, the pair $(\mathsf{vcol},\mathsf{Ev})$
witnesses color $k$;

  * •

for all $q\in Q_{u}$, if $\mathsf{vcol}(q)<n$, then
$\mathsf{col}(q)=\mathsf{vcol}(q)$ and $\mathsf{NewCol}(q,\mathsf{vcol})<n$;

If $n=0$, we say that the pair $(\mathsf{vcol},\mathsf{Ev})$ is _completely
faithful_.

Only the first condition for faithfulness is really of interest to us. For
instance, this first condition suffices to show the crucial proposition below.
However, the second condition is used in the proofs. (It is also helpful as it
guides us in how to build a completely faithful pair, as discussed below.)
Note that, in the proofs, we use an even stronger notion of faithfulness with
a third condition. However, we do not present it here in order not to
complexify too much the approach, and the two first conditions are sufficient
for the (informal) explanation of Theorem 25. It can however be found in
Appendix D.2.

The benefit of faithful environments and coloring functions lies in the
proposition below: if all states are mapped w.r.t. the coloring function to
$e$, then the environment function guarantees the value $u$ in the whole
$u$-slice $Q_{u}$.

######  Proposition 43.

For a coloring function $\mathsf{vcol}:Q_{u}\rightarrow\llbracket
0,e\rrbracket$ and an environment function
$\mathsf{Ev}:Q_{u}\rightarrow\mathsf{Env}(Q)$, assume that
$(\mathsf{vcol},\mathsf{Ev})$ is completely faithful and that
$\mathsf{col}_{u}[Q_{u}]=\\{e\\}$. Then, all Player-$\mathsf{A}$ positional
strategies generated by the environment function $\mathsf{Ev}$ parity dominate
the valuation $\chi_{\mathcal{G}}$ in the game $\mathcal{G}^{u}$.

######  Proof.

This is direct from the definitions. Indeed, as $(\mathsf{vcol},\mathsf{Ev})$
is completely faithful, it follows that $(\mathsf{vcol},\mathsf{Ev})$
witnesses the color $e$ (see Definition 42). That is, all Player-$\mathsf{A}$
positional strategies $\mathsf{s}_{\mathsf{A}}$ generated by $\mathsf{Ev}$ in
the game $\mathcal{L}^{e}_{\mathsf{vcol}}$ parity dominate the valuation
$v_{e,\mathsf{vcol}}^{u}$ (see Definition 40). Since
$\mathsf{vcol}[Q_{u}]=\\{e\\}$, both games $\mathcal{L}^{e}_{\mathsf{vcol}}$
and $\mathcal{G}^{u}$ are identical (see Definitions 27 and 31). Similarly,
the valuation $v_{e,\mathsf{vcol}}^{u}$ is equal to the valuation
$\chi_{\mathcal{G}}$ in the game $\mathcal{G}^{u}$ (also see Definition 40).

###  6.5 Computing a completely faithful pair

Given Lemma 43, our goal is to come up with a pair of an environment function
and a coloring function completely faithful such that all states are colored
with $e$. Let us first consider how to obtain a completely faithful pair from
the initial coloring function and the empty environment function (i.e. no
state is mapped to an environment). Note that this initial pair of coloring
and environment functions is faithful down to $e+1$. Hence, our goal is, given
a pair $(\mathsf{vcol},\mathsf{Ev})$ faithful down to some $n\in\llbracket
1,e+1\rrbracket$, to build a new pair that is faithful down to $n-1$. To do
so, let us be guided by the second property for faithfulness: to be faithful
down to $n-1$, no state $q\in Q_{u}$ such that $\mathsf{vcol}(q)\leq n-2$
should be such that $\mathsf{NewCol}(q,\mathsf{vcol})=n-1$. Hence, the idea
is, for all such states $q\in Q_{u}$, to change their colors to $n-1$ until no
state $q\in Q_{u}$ with $\mathsf{vcol}(q)\leq n-2$ satisfies333This can seen
as computing the “probabilistic attractor with leaks towards the stopping
states” that we mentioned above. $\mathsf{NewCol}(q,\mathsf{vcol})=n-1$. The
environment associated to each such state $q$ newly colored by $n-1$ will be
given by the coloring function $\mathsf{vcol}$ for which
$\mathsf{NewCol}(q,\mathsf{vcol})=n-1$ for the first time (crucially, this is
done before the color of $q$ is updated to $n-1$). The procedure we have
described is formally given in the Appendix as Algorithm 15. Interestingly,
the update done in the algorithm preserves the faithfulness of environment and
coloring functions.

######  Lemma 44 (Proof Appendix D.4, Page D.4).

Consider a coloring function $\mathsf{vcol}:Q_{u}\rightarrow\llbracket
0,e\rrbracket$, $n\in\llbracket 1,e+1\rrbracket$, and a partial environment
function $\mathsf{Ev}:Q_{u}\rightarrow\mathsf{Env}(Q)$ defined on
$\mathsf{vcol}^{-1}[\llbracket n,e\rrbracket]$. Assume that
$(\mathsf{vcol},\mathsf{Ev})$ is faithful down to $n$. Let
$(\mathsf{vcol}^{\prime},\mathsf{Ev}^{\prime})\leftarrow\mathsf{UpdateColEnv}(n-1,\mathsf{vcol},\mathsf{Ev})$
be the pair computed by Algorithm 15 for index $n-1$. (Only states $q$ such
that $\mathsf{vcol}^{\prime}(q)=n-1$ may have changed their colors and be
newly mapped to an environment.) Then,
$(\mathsf{vcol}^{\prime},\mathsf{Ev}^{\prime})$ is faithful down to $n-1$.

Before giving a proof sketch of this lemma, let us illustrate it on an
example.

######  Example 45.

Let us illustrate this algorithm on Figures 4 and 4. The first step is to
build a pair that is faithful down to $e=4$. As mentioned above in Example 39,
we have $\mathsf{NewCol}(q_{5},\mathsf{col})=4$. Hence, the color of this
state is changed to $4$ (we obtain a virtual coloring function
$\mathsf{vcol}^{q_{5}}$) and we set
$\mathsf{Ev}(q_{5}):=E^{4}_{q_{5},\mathsf{col}}$. Note that a
Player-$\mathsf{A}$ $\mathsf{GF}$-strategy $\sigma_{\mathsf{A}}$ is optimal in
this environment if and only if it plays both rows with positive probability.
Furthermore, note that, in the extracted game
$\mathcal{L}^{4}_{\mathsf{vcol}^{q_{5}}}$, a Player-$\mathsf{A}$ positional
strategy playing such a $\mathsf{GF}$-strategy $\sigma_{\mathsf{A}}$ in
$q_{5}$ parity dominates the valuation $v_{Q_{4},\mathsf{col}^{q_{5}}}^{1/2}$.
Hence, the pair $(\mathsf{vcol}^{q_{5}},\mathsf{Ev})$ is faithful down to $4$.

Consider now the layer $3$. First, the state $q_{6}$ already has color $3$, so
it only remains to set its environment:
$\mathsf{Ev}(q_{6}):=E^{3}_{q_{6},\mathsf{vcol}^{q_{5}}}$. We then realize
that $\mathsf{NewCol}(q_{4},\mathsf{vcol}^{q_{5}})=3$. Indeed, $q_{4}$ is
colored with $2$ and may go with equal probability to a state colored with $0$
and to a state colored with $3$. The color of this state is therefore changed,
thus obtaining a new virtual coloring function
$\mathsf{vcol}^{q_{5},q_{6},q_{4}}$. We set its environment:
$\mathsf{Ev}(q_{4}):=E^{3}_{q_{4},\mathsf{vcol}^{q_{5}}}$. One can realize
that the pair $(\mathsf{vcol}^{q_{5},q_{6},q_{4}},\mathsf{Ev})$ witnesses the
color $3$ : a positional Player-$\mathsf{B}$ strategy generated by this
environment would be so that (i) from $q_{6}$, it goes to $q_{4}$ with
probability $1$ (to avoid $k_{4}$ that is colored with $4$) and (ii) from
$q_{5}$, it goes to $q_{6}$ with positive probability (to see the color $3$
with positive probability). Such a strategy has value $0$ in the game
$\mathcal{L}^{3}_{\mathsf{vcol}^{q_{5}}}=\mathcal{L}^{3}_{\mathsf{vcol}}$ from
Figure 5, hence the pair $(\mathsf{vcol}^{q_{5},q_{6},q_{4}},\mathsf{Ev})$
witnesses the color $3$.

We illustrate on this step why the environment needs to be set before changing
the new color and not after. That is, we explain why it would not be correct
to set $\mathsf{Ev}(q_{4}):=E^{3}_{q_{4},\mathsf{col}^{q_{5},q_{6},q_{4}}}$
instead of what we do above. In this environment, the state $q_{4}$ has color
$3$. Hence, looping with probability $1$ on $q_{4}$ is an optimal
$\mathsf{GF}$-strategy for Player $\mathsf{B}$ w.r.t.
$(\mathsf{F}(q_{4}),\mathsf{Ev}(q_{4}))$. Then, the corresponding pair of
coloring and environment functions would not witness the color $3$. Indeed, a
Player $\mathsf{B}$ strategy that loops with probability $1$ on $q_{4}$ is
generated by this environment, and it has value $1\geq u$ (because the real
color of this state is $2$, and not $3$).

This process is then repeated down to $0$. In Figure 4, the depicted coloring
function (with the appropriate environment function that is not shown in
Figure 4) are in fact completely faithful (this is what outputs Algorithm 15
on the coloring function of Figure 4).

We give a proof sketch of Lemma 44, which explains the ideas for the first
phase of the procedure for computing a first completely faithful pair, before
Algorithm 16 is called – which we will discuss right after.

######  Proof (Proof sketch).

We want to prove that the pair $(\mathsf{vcol}^{\prime},\mathsf{Ev}^{\prime})$
witnesses the color $n-1$ (the other condition for faithfulness is ensured by
the construction). We consider the case where $n-1$ is even, the other case is
similar (but one needs to take the point-of-view of Player $\mathsf{B}$).
Consider a Player-$\mathsf{A}$ positional strategy $\mathsf{s}_{\mathsf{A}}$
generated by the environment function $\mathsf{Ev}^{\prime}$ in the game
$\mathcal{L}^{n-1}_{{\mathsf{vcol}^{\prime}}}$. Let
$Q_{n-1}:=\mathsf{vcol}^{\prime-1}[n-1]$ and let
$v:=v_{n-1,{\mathsf{vcol}^{\prime}}}^{u}$. For every $q\in Q_{n-1}$, let
$Y_{q}:=(\mathsf{F}(q),\mathsf{Ev}^{\prime}(q))$ be the local environment at
state $q$ and let us denote $\mathsf{Ev}^{\prime}(q)$ by
$\mathsf{Ev}^{\prime}(q)=\langle c_{q},e,p_{q}\rangle$. From the
characterization of Lemma 21 (item (ii.1)), by carefully analyzing the links
between the local games $\mathcal{G}_{Y_{q}}$ for all $q\in Q_{n-1}$ and the
game $\mathcal{L}^{n-1}_{{\mathsf{vcol}^{\prime}}}$, we deduce that the
strategy $\mathsf{s}_{\mathsf{A}}$ dominates the valuation $v$.

It remains to show that all BSCCs (that are not reduced to a stopping state
and are) compatible with $s_{\mathsf{A}}$ are even-colored. Consider such a
BSCC $H$ and a Player-$\mathsf{B}$ deterministic positional strategy
$\mathsf{s}_{\mathsf{B}}$ which induces $H$. For every state $q\in H$, since
no stopping state occurs in $H$, it must be that the probability to reach a
stopping state is $0$. That is, it amounts to have
$\mathsf{out}_{\langle\mathsf{F}(q),\mathbbm{1}_{Q\setminus
Q_{u}}\rangle}(\sigma_{\mathsf{A}},b)=0$. For every state $q\in Q_{n-1}$, the
coloring function $\mathsf{vcol}_{q}$ associated with environment
$\mathsf{Ev}^{\prime}(q)$ is such that $\mathsf{vcol}_{q}(q)\leq n-1$.444This
is because all states $q\in Q_{n-1}$ satisfy $\mathsf{col}(q)\leq n-1$. This
is one of the additional conditions for faithfulness that we did mention, but
that is used in the Appendix in Definition 71. Hence, the color $c_{q}$ is
such that $c_{q}=\max(n-2,\mathsf{vcol}_{q}(q))\leq n-1$. Now, assume that
some state $k_{i}$ is in $H$ for some $i>n-1\geq c_{q}$. In that case, as
explained in Remark 22, the highest $i$ such that $k_{i}$ is in $H$ must be
even. Hence, $H$ is even-colored. Assume now that no state $k_{i}$ in $H$ is
such that $i>n-1$. In that case, if a state in $H$ has color $n-1$ (like the
state $q_{6}$ in Figure 4 in the case where $n-1=3$), then $n-1$ is the
highest color in $H$ and $H$ is even-colored. Consider the first state $q$
whose color is now $n-1$ (w.r.t. ${\mathsf{vcol}^{\prime}}$) but whose
previous color was not $n-1$. In that case, we have
$c_{q}=\max(n-2,\mathsf{vcol}_{q}(q))=n-2$ is odd. Furthermore, the state $q$
has changed its color because $\mathsf{NewCol}(q,\mathsf{vcol}_{q})=n-1$. With
Remark 22, since $\mathsf{s}_{\mathsf{A}}(q)$ is optimal w.r.t. $Y_{q}$, it
follows that there is a positive probability to reach, in the game
$\mathcal{G}_{Y_{q}}$ the state $k_{n-1}$. In the game
$\mathcal{L}^{n-1}_{{\mathsf{vcol}^{\prime}}}$, this corresponds to a positive
probability to reach a state $q^{\prime}\in H$ colored with $n-1$ w.r.t.
$\mathsf{vcol}_{q}$ (recall Definition 30). Since $q$ is the first state to
have changed its color, we can deduce that $q^{\prime}$ already had color
$n-1$ w.r.t. $\mathsf{vcol}$. Furthermore, one can show that $q^{\prime}$ is
colored with $n-1$ w.r.t. the real coloring function $\mathsf{col}$. Overall,
in the game $\mathcal{L}^{n-1}_{{\mathsf{vcol}^{\prime}}}$, with the
$\mathsf{GF}$-strategy $\mathsf{s}_{\mathsf{A}}(q)$, there is a positive
probability to reach in one step a state $q^{\prime}$ colored with $n-1$.
Iteratively, we obtain that, considering the $k$-th state whose color is now
$n-1$ (i.e. w.r.t. ${\mathsf{vcol}^{\prime}}$) but whose initial color was not
$n-1$, there is a positive probability to reach (in at most $k$ steps) a state
colored with $n-1$. Hence, the highest color appearing in $H$ is $n-1$, which
is even. We obtain that $\mathsf{s}_{\mathsf{A}}$ parity dominates the
valuation $v$.

Overall, applying iteratively Algorithm 15 on all colors from $e$ down to $0$
starting with the initial coloring function induces a completely faithful pair
$(\mathsf{vcol},\mathsf{Ev})$. However, it may be the case that some states
are mapped to an odd number, which does not allow to apply Lemma 43. The
question is then: from that completely faithful configuration, how can one
make some progress towards a situation where Lemma 43 can be applied?

######  Example 46.

Consider the coloring function of Figure 4. As mentioned in Example 45, with
an appropriate environment function (that is not shown in Figure 4), we can
have a pair which is completely faithful. To gain some intuition on what
should be done next, let us focus only on the states $q_{1},q_{2},q_{3}$. A
simplified version is presented in Figure 7 (with a slight modification:
instead of going to $q_{0}$, $q_{1}$ loops on itself): the initial (and true)
colors of the states are in circles next to them and their color w.r.t. the
current (virtual) coloring function (that is completely faithful with an
appropriate environment function) is written in red. In this game, Player
$\mathsf{B}$ plays alone, but it is obvious that Player $\mathsf{A}$ wins
surely from $q_{2}$: indeed, either the game stays indefinitely in $q_{2}$, or
it eventually reaches and settles in $q_{1}$.

The current virtual color $1$ assigned to both $q_{2}$ and $q_{3}$ does not
properly reflect the fact that if the game reaches $q_{3}$, even though Player
$\mathsf{B}$ plays optimally according to the local game associated with
$q_{2}$, it will end up looping in $q_{1}$, which will be losing for Player
$\mathsf{B}$. In a way, we would like to propagate the information that
reaching $q_{1}$ is bad for Player $\mathsf{B}$. Since $0$ is the smallest
color, there is no harm in increasing it to $2$, the game from $q_{1}$ will be
the same: it will be won by Player $\mathsf{A}$ by looping. Player
$\mathsf{B}$ will now be able to know that going to $q_{1}$ is dangerous for
him, which will be obtained by applying the previous iterative process.

In a more general concurrent game, the next step of the process when we have a
completely faithful configuration not satisfying the assumptions of Lemma 43
consists in changing all the states with the least (virtual) color $n$ to the
color $n+2$. However, note that there is a (very important) second step: the
colors of all states (virtually) colored with $n+1$ should be reset to their
initial colors. The reason why can be seen again in Figure 7. After the color
of $q_{1}$ becomes $2$, the color of $q_{3}$ will also become $2$. However, if
the color of the state $q_{2}$ is not reset, then it is not going to change
since Player $\mathsf{B}$ can choose to loop to $q_{2}$ and see the color $1$
for ever (in game $\mathcal{G}^{0}_{q_{2},\mathsf{vcol}}$). That is, from
Player $\mathsf{B}$’s perspective, looping indefinitely on $q_{2}$ is winning,
which is not what happens in the real game (i.e. the coloring function does
not faithfully describes what happens in the game). The changes made to the
coloring function $\mathsf{vcol}$ from Figure 4 can be seen in Figure 8. Note
that the process of increasing the colors of some states by $2$ can only be
done with the _least_ color (otherwise faithfulness will not be preserved).

0$0$$q_{1}$1$0$$q_{2}$1$1$$q_{3}$ Figure 7: A (deterministic turn-based) game
with only three states. Figure 8: The same arena as in Figures 4,4 but with a
different coloring function.

The process described in Example 46 is implemented as Algorithm 16 in the
Appendix, it ensures the lemma below.

######  Lemma 47 (Proof Appendix D.5, Page D.5).

Let $\mathsf{vcol}:Q_{u}\rightarrow\llbracket 0,e\rrbracket$,
$\mathsf{Ev}:Q_{u}\rightarrow\mathsf{Env}(Q)$ be a coloring and an environment
functions. Let $n:=\min\mathsf{vcol}[Q]$. Assume that $n\leq e-2$ and the pair
$(\mathsf{vcol},\mathsf{Ev})$ is completely faithful. If
$(\mathsf{vcol}^{\prime},\mathsf{Ev}^{\prime})\leftarrow\mathsf{IncLeast}(\mathsf{vcol},\mathsf{Ev})$
is the result of increasing the least-colored layer by 2 and resetting the
environment of the last but least-colored layer (Algorithm 16), then
$(\mathsf{vcol}^{\prime},\mathsf{Ev}^{\prime})$ is faithful down to $n+2$.

######  Proof (Proof sketch).

Let $Q_{n}:=\mathsf{vcol}^{-1}[n]$ and $Q_{n+2}:=\mathsf{vcol}^{-1}[n+2]$. The
algorithm has three steps: first, it increases the least color by $2$; then it
resets the environments of the $(n+1)$-colored states; finally it applies
Algorithm 14 to these reset states. Let us argue that
$(\mathsf{vcol}^{\prime\prime},\mathsf{Ev})$ (obtained after the first step)
witnesses the color $n+2$.

Consider a Player-$\mathsf{A}$ positional strategy $\mathsf{s}_{\mathsf{A}}$
generated by the environment $\mathsf{Ev}$ in the game
$\mathcal{L}^{n+2}_{{\mathsf{vcol}^{\prime\prime}}}$. Let
$v:=v^{u}_{n+1,\mathsf{vcol}^{\prime\prime}}$. Similarly to the proof of Lemma
44, $\mathsf{s}_{\mathsf{A}}$ dominates the valuation $v$. Consider a BSCC $H$
compatible with $\mathsf{s}_{\mathsf{A}}$. If $H\cap Q_{n+2}=\emptyset$, then
$H$ is even-colored. Indeed, $(\mathsf{vcol},\mathsf{Ev})$ witnesses the color
$n$. In addition, the probability to go to a state $k_{i}^{n+2}$ that is
$(n+1)$-colored in the game
$\mathcal{L}^{n+2}_{{\mathsf{vcol}^{\prime\prime}}}$ is exactly the
probability to go to a state $k_{i}^{n}$ that is $(n+1)$-colored in the game
$\mathcal{L}^{n}_{\mathsf{vcol}}$ (since $n$ is the least color). Furthermore,
$H$ is also even-colored as soon as $H\cap Q_{n}=\emptyset$ since
$(\mathsf{vcol},\mathsf{Ev})$ witnesses the color $n+2$. Now, assume that none
of these cases occur. Then, one can show that: either a state $k_{i}$ is seen
for some $i\geq n+2$, and $H$ is even-colored; or, from some states in
$Q_{n+2}$, there is a positive probability to exit $Q_{n+2}$ and no state
$k_{i}$ is seen for $i\geq n+2$. Now, looking at what happens in game
$\mathcal{L}^{n+2}_{{\mathsf{vcol}}}$, some states $k_{i}$ are seen for $i\leq
n+1$, and such states are colored with $n+1$. Hence, since
$(\mathsf{vcol},\mathsf{Ev})$ witnesses the color $n+2$, it must be that the
highest color in $H$ is $n+2$, which is even. Therefore it is also the case in
the game $\mathcal{L}^{n+2}_{{\mathsf{vcol}^{\prime\prime}}}$. In all the
cases, $H$ is even-colored.

As stated in Lemma 47, the update of colors described in Example 46 can be
done only if, for a completely faithful pair, the least (virtual) color $n$
appearing is at most $e-2$. If $n=e$, we are actually in the scope of Lemma 43
since in that case all states have (virtual) color $e$. However, there remains
the case where we have $n=e-1$. In fact, this case cannot happen.

######  Lemma 48 (Proof Appendix D.6, Page D.6).

Consider a coloring function $\mathsf{vcol}:Q_{u}\rightarrow\llbracket
0,e\rrbracket$, an environment function
$\mathsf{Ev}:Q_{u}\rightarrow\mathsf{Env}(Q)$. Assume that
$(\mathsf{vcol},\mathsf{Ev})$ is completely faithful. Then, for
$C:=\mathsf{vcol}[Q]$, we have $\min C\neq e-1$.

######  Proof (Proof sketch).

Let $Q_{e-1}:=\mathsf{vcol}^{-1}[e-1]$. Towards a contradiction, let
$\mathsf{s}_{\mathsf{B}}$ be a Player-$\mathsf{B}$ positional strategy
generated by $\mathsf{Ev}$ in the game $\mathcal{L}^{e-1}_{\mathsf{vcol}}$. It
parity dominates the valuation $v_{e-1,\mathsf{vcol}}^{u^{\prime}}$ for some
$u^{\prime}<u$. Hence, all BSCCs compatible with $\mathsf{s}_{\mathsf{B}}$ are
odd-colored: they all stay in the layer $Q_{e-1}$. Indeed, since $e-1=\min C$,
exiting $Q_{e-1}$ while staying in $Q_{u}$ means seeing
$Q_{e}:=\mathsf{vcol}^{-1}[e]$ with $e$ even and the highest color in the
game. Hence, either the game stays indefinitely in $Q_{e-1}$ and Player
$\mathsf{B}$ wins almost surely, or there is some positive probability to
visit stopping states, and in that case their expected values is at most
$u^{\prime}$. Hence, in the game $\mathcal{G}^{u}$, the strategy
$\mathsf{s}_{\mathsf{B}}$ has values less than $u$ from the states
$Q_{e-1}\subseteq Q_{u}$, which is a contradiction.

Finally, all these pieces are put together in Algorithm 17 in the Appendix,
whose output is a completely faithful pair where all states are mapped to $e$.
The only remaining step is to prove the termination of this algorithm. Let us
consider the (virtual) coloring functions as vectors in $\mathbb{N}^{e+1}$
indicating the number of states mapped to each color. Then, one can realize
that each step of Algorithm 17 increases this vector for a lexicographic order
(i.e. we first compare the number of states mapped to $e$, then the number of
states mapped to $e-1$, etc). Hence, Algorithm 17 does terminate in finitely
many steps.

######  Lemma 49 (Proof Appendix D.7, Page D.7).

Algorithm 17 computes a completely faithful pair of environment and coloring
functions mapping each state to $e$ in finitely many steps.

We can now proceed to the proof of Theorem 25.

######  Proof.

Let us prove Theorem 25 for Player $\mathsf{A}$. Consider some $u\in
V_{Q}\setminus\\{0\\}$. By Lemma 49, there is a completely faithful pair of
environment and coloring functions
$(\mathsf{vcol}_{u},\mathsf{Ev}_{\mathsf{A}}^{u})$ mapping each state in
$Q_{u}$ to $e_{u}$. Hence, by Lemma 43, all Player-$\mathsf{A}$ positional
strategies generated by the environment function
$\mathsf{Ev}_{\mathsf{A}}^{u}$ parity dominate the valuation
$\chi_{\mathcal{G}}$ in the game $\mathcal{G}^{u}$. Since we assume that all
game forms occurring in $Q_{u}$ are positionally maximizable up to
$e_{u}-\mathsf{col}(q)$ w.r.t. Player $\mathsf{A}$, such positional strategies
generated by $\mathsf{Ev}_{\mathsf{A}}^{u}$ do exist. Then, considering the
environment function
$\mathsf{Ev}_{\mathsf{A}}:Q\rightarrow\mathsf{Ev}(\mathsf{D})$ that merges all
the environment functions $(\mathsf{Ev}_{\mathsf{A}}^{u})_{u\in
V_{\mathcal{G}}\setminus\\{0\\}}$ together (and that is defined arbitrarily on
$Q_{0}$), it follows by Lemma 28, that all Player-$\mathsf{A}$ positional
strategies generated by that environment function $\mathsf{Ev}$ are optimal.
(And such strategies exist.)

##  7 Positionally optimizable game forms

In this section, we state some properties that are ensured by positionally
optimizable game forms. We begin by giving some notations for positionally
optimizable game forms (and the corresponding decision problems).

######  Notation 50.

For $n\in\mathbb{N}$, we let $\mathsf{ParO}(n)$ be the set of all game forms
positionally optimizable up to $n$ and we let $\mathsf{IsO}(n)$ be the problem
of deciding whether a game form is in $\mathsf{ParO}(n)$. Furthermore, we let
$\mathsf{ParO}:=\cap_{n\in\mathbb{N}}\mathsf{ParO}(n)$ and we denote by
$\mathsf{IsO}$ the problem of deciding whether a game form is in
$\mathsf{ParO}$.

###  7.1 Some positionally optimizable game forms

Let us first exhibit some positionally maximizable game forms. Given the
distance to the highest color in the game, Theorem 25 and Remark 20 give
exactly the game forms that should be used in parity games to ensure the
existence of positional optimal strategies for both players. The game forms in
$\mathsf{ParO}$ are the ones that can be used in all parity games, regardless
of the number of colors involved, while ensuring the existence of positional
optimal strategies (for both players). Such game forms do exist. For instance,
, turn-based game forms are positionally optimizable (straightforwardly). In
fact, all _determined_ [2] game forms are positionally optimizable. A
deterministic (i.e. where all distributions over are the outcomes are
deterministic) game form $\mathcal{F}\in\mathsf{Form}(\mathsf{O})$ is
determined if it satisfies the following property: for all
$\\{0,1\\}$-valuations of the outcomes $v:\mathsf{O}\rightarrow\\{0,1\\}$, in
the game in normal form $\langle\mathcal{F},v\rangle$, there is either a row
of $1$ or a column of $0$. In particular, all turn-based game forms are
determined. Furthermore, all game forms with at most two outcomes are in
$\mathsf{ParO}$. This is stated formally in the lemma below.

######  Proposition 51 (Proof E.1, Page E.1).

Consider a set of outcomes $\mathsf{O}$ and a game form
$\mathcal{F}=\langle\mathsf{Act}_{\mathsf{A}},\mathsf{Act}_{\mathsf{B}},\mathsf{D},\varrho\rangle\in\mathsf{Form}(\mathsf{D})$.
Assume that $\mathcal{F}$ is either determined (in particular, it may be turn-
based), or such that $\mathsf{O}\leq 2$. In that case,
$\mathcal{F}\in\mathsf{ParO}$.

###  7.2 Deciding if a game form is positionally optimizable

Now, we want to show that it is decidable if a game form if positionally
optimizable. To do so, we are going to encode this problem in the first order
of the reals, that we introduce in the subsection below.

####  7.2.1 First-order theory of the reals

Informally, first order theory of the reals formulas use (existential or
universal) quantification over real variables, classical logical connectors
and (in)equalities between multi-variate polynomials. We formally define them
below.

######  Definition 52 (First-order theory of the reals).

In the first order theory of the reals ($\mathsf{FO}$-$\mathbb{R}$ for short),
we consider formulas $\Phi$ of the shape:

$\Phi=Q_{1}\;x_{1}\in\mathbb{R},\ldots,Q_{n}\;x_{n}\in\mathbb{R},\varphi(x_{1},\ldots,x_{n})$

where $n\in\mathbb{N}$ and

  * •

for all $i\in\llbracket 1,n\rrbracket$, $Q_{i}\in\\{\exists,\forall\\}$. That
is, it is either an existential or a universal quantifier;

  * •

$\varphi(x_{1},\ldots,x_{n})$ is a classical formula without quantifiers, with
$\wedge$ (and), $\lor$ (or) and $\lnot$ (negation) as logical connectors. The
atomic propositions considered in $\varphi(x_{1},\ldots,x_{n})$ are of the
shape:

$P(x_{1},\ldots,x_{n})\bowtie 0$

where $\bowtie\;\in\\{=,\neq,\geq,>,\leq,<\\}$ and
$P:\mathbb{R}^{n}\rightarrow\mathbb{R}$ is a real multi-variate polynomial
with integer coefficients.

The semantics behind the first order theory of the reals is quite intuitive,
though it would take some space to formally define. Instead, let us illustrate
it on a couple of examples.

######  Example 53.

Consider the $\mathsf{FO}$-$\mathbb{R}$ formula below.

$\forall x\in\mathbb{R},\;\exists y\in\mathbb{R},\;x+y\geq 0$

This $\mathsf{FO}$-$\mathbb{R}$ formula is true since it does hold that, for
all $x\in\mathbb{R}$, taking $y:=-x\in\mathbb{R}$, we have $x+y=0$. However,
the $\mathsf{FO}$-$\mathbb{R}$ formula

$\exists x\in\mathbb{R},\;\forall y\in\mathbb{R},\;x+y\geq 0$

is false in $\mathsf{FO}$-$\mathbb{R}$ since there is no $x\in\mathbb{R}$,
such that, for all $y\in\mathbb{R}$, we have $x+y\geq 0$.

Let us now consider the decision problem associated with
$\mathsf{FO}$-$\mathbb{R}$ formulas.

######  Definition 54.

We denote by $\mathsf{True}_{\mathsf{FO}-\mathbb{R}}$ the set of all first-
order theory of the reals formulas that evaluate to true. The decision problem
$\mathsf{Is}_{\mathsf{FO}-\mathbb{R}}$ is as follows:

  * •

Input: an $\mathsf{FO}$-$\mathbb{R}$ formula $\Phi$;

  * •

Output: yes if and only if the formula $\Phi$ is in
$\mathsf{True}_{\mathsf{FO}-\mathbb{R}}$.

######  Theorem 55.

The decision problem $\mathsf{Is}_{\mathsf{Fo}-\mathbb{R}}$ is decidable.

This result was first shown in [15]. It was then improved in [14, Theorem 1.1]
it as it was shown that $\mathsf{Is}_{\mathsf{FO}-\mathbb{R}}$ could be
decided in doubly-exponential time via a quantifier elimination procedure.

####  7.2.2 Encoding in the first order theory of the reals

Let us come back to the problem of interest of us: deciding if a game form is
positionally optimizable. To tackle this issue, we first realize that a game
form is positionally optimizable if and only if there are optimal
$\mathsf{GF}$-strategies w.r.t. all _relevant_ environments, defined below.

######  Definition 56 (Relevant environments).

For a set of outcomes $\mathsf{O}$, an environment $E=\langle
c,e,p\rangle\in\mathsf{Env}(\mathsf{O})$ is _relevant_ if $c\in\\{0,1\\}$,
$p^{-1}[\\{c-1\\}]=p^{-1}[\\{q_{\mathsf{init}}\\}]=\emptyset$ and, for all
$i\in\llbracket c,e\rrbracket$, there is $o\in\mathsf{O}$ such that
$p(o)=k_{i}$. The _size_ of a relevant environment $E$ is equal to
$\mathsf{Sz}(E):=e-c$.

As mentioned above, we may only consider relevant environment to decide if a
game form is positionally maximizable.

######  Proposition 57 (Proof Appendix E.2, Page E.2).

Consider a set of outcomes $\mathsf{O}$ and a game form
$\mathcal{F}\in\mathsf{Form}(\mathsf{O})$. Consider a Player
$\mathsf{C}\in\\{\mathsf{A},\mathsf{B}\\}$. For all $n\in\mathbb{N}$, the game
form $\mathcal{F}$ is positionally maximizable w.r.t. Player $\mathsf{C}$ up
to $n$ if and only if, for all relevant environments $E$ with
$\mathsf{Sz}(E)\leq n-1$, there is an optimal $\mathsf{GF}$-strategy in
$\mathcal{F}$ for Player $\mathsf{C}$ w.r.t. $(\mathcal{F},E)$.

The proof of this proposition is quite long and actually uses a result that is
not published yet, but that is in the PhD thesis of one of the authors, which
will soon be available online.

The benefit of considering only relevant environment is that, given any
$l\in\mathbb{N}$, deciding if a game form is positionally optimizable up to
$l$ can be done by considering environments where all the outcomes are mapped
to integers at most $l$. Then, the fact that a game form is positionally
optimizable can be encoded in the first-order theory of the reals.

######  Proposition 58.

Consider a deterministic game form $\mathcal{F}$. The fact that
$\mathcal{F}\in\mathsf{ParO}$ (resp. $\mathcal{F}\in\mathsf{ParO}(n)$, for
some $n\in\mathbb{N}$) can be encoded, with formula of size polynomial in
$|\mathcal{F}|$ (resp. and $n$), in $\mathsf{FO}$-$\mathbb{R}$.

###### Proof.

Consider some $l\in\mathbb{N}$. We encode the fact that a standard finite
deterministic game form
$\mathcal{F}=\langle\mathsf{Act}_{\mathsf{A}},\mathsf{Act}_{\mathsf{B}},\mathsf{O},\varrho\rangle$
is positionally optimizable up to $l$. Without loss of generality, since the
game form $\mathcal{F}$ is deterministic, we assume that
$\mathsf{O}=\varrho(\mathsf{Act}_{\mathsf{A}},\mathsf{Act}_{\mathsf{B}})$. To
do so, we use the characterization of Proposition 57 and we express in
$\mathsf{FO}$-$\mathbb{R}$ the fact that, for all relevant environments
$E=\langle c,e,p\rangle$ of size at most $l-1$, both players have an optimal
$\mathsf{GF}$-strategy. We use the characterization given by Lemma 21. We
assume that $\mathsf{Act}_{\mathsf{A}}=\llbracket 1,n\rrbracket$,
$\mathsf{Act}_{\mathsf{B}}=\llbracket 1,m\rrbracket$ and we consider the
formula $\Phi_{\mathcal{F}}^{\mathsf{ParO}(l)}$ below, that we will explain
line by line in the following.

$\displaystyle\Phi_{\mathcal{F}}^{\mathsf{ParO}(l)}:=\forall c,$
$\displaystyle\;\mathsf{ZeroOrOne}(c)\;\wedge$
$\displaystyle\forall\alpha=(\alpha_{o})_{o\in\mathsf{O}},$
$\displaystyle\;\mathsf{ZeroOrOne}(\alpha)\;\wedge$ $\displaystyle\forall
v=(v_{o})_{o\in\mathsf{O}},$
$\displaystyle\;\mathsf{RealBetweenZeroOne}(v)\;\wedge$ $\displaystyle\forall
k=(k_{o})_{o\in\mathsf{O}},$
$\displaystyle\;\mathsf{IntBetweenZeroL}(k,c)\;\wedge$ $\displaystyle\exists
u,$ $\displaystyle\;(0\leq u\leq 1)\;\wedge$ $\displaystyle\exists
S_{\mathsf{A}}=S_{\mathsf{A}}^{1},\ldots,S_{\mathsf{A}}^{n},\;$
$\displaystyle\exists\sigma_{\mathsf{A}}=\sigma_{\mathsf{A}}^{1},\ldots,\sigma_{\mathsf{A}}^{n},\;$
$\displaystyle\mathsf{IsIndicator}(S_{\mathsf{A}})\wedge\mathsf{IsStrategy}_{\mathsf{A}}(\sigma_{\mathsf{A}})\wedge\mathsf{IsSupp}(\sigma_{\mathsf{A}},S_{\mathsf{A}})\wedge\mathsf{Val}_{\mathsf{A}}(\sigma_{\mathsf{A}},\alpha,v,u)\wedge$
$\displaystyle\bigwedge_{1\leq j\leq
m}\mathsf{MaxIntegerEven}(S_{\mathsf{A}},k,j,c)\;\wedge$ $\displaystyle\exists
S_{\mathsf{B}}=S_{\mathsf{B}}^{1},\ldots,S_{\mathsf{B}}^{m},\;$
$\displaystyle\exists\sigma_{\mathsf{B}}=\sigma_{\mathsf{B}}^{1},\ldots,\sigma_{\mathsf{B}}^{n},\;$
$\displaystyle\mathsf{IsIndicator}(S_{\mathsf{B}})\wedge\mathsf{IsStrategy}_{\mathsf{B}}(\sigma_{\mathsf{B}})\wedge\mathsf{IsSupp}(\sigma_{\mathsf{B}},S_{\mathsf{B}})\wedge\mathsf{Val}_{\mathsf{B}}(\sigma_{\mathsf{B}},\alpha,v,u)\wedge$
$\displaystyle\bigwedge_{1\leq i\leq
n}\mathsf{MaxIntegerOdd}(S_{\mathsf{B}},k,i,c)$

The formula $\Phi_{\mathcal{F}}^{\mathsf{ParO}(l)}$ does not fit exactly the
formalism of Definition 52, since all the quantifiers are not at the beginning
of the formula. However, the semantics is unchanged if these quantifiers are
moved at the beginning of the formula. We presented
$\Phi_{\mathcal{F}}^{\mathsf{ParO}(l)}$ in that way for readability.

The first four lines encode the relevant environment $E$. Specifically:

$\mathsf{ZeroOrOne}(c):=(c=0)\lor(c=0)\;$

Since the environment $E$ is relevant, $c$ is equal to either 0 or 1.
Furthermore:

$\mathsf{ZeroOrOne}(\alpha):=\bigwedge_{o\in\mathsf{O}}((\alpha_{o}=0)\lor(\alpha_{o}=1))$

where, for all $o\in\mathsf{O}$, $\alpha_{o}=1$ means that $p(o)\in[0,1]$ and
$\alpha_{o}=0$ means that $p(o)\in K_{l}$. Furthermore:

$\mathsf{RealBetweenZeroOne}(v):=\bigwedge_{o\in\mathsf{O}}(0\leq v_{o}\leq
1)$

where, for all $o\in\mathsf{O}$, $v_{o}\in[0,1]$ corresponds to the value of
$o$ w.r.t. $p$ (assuming $p(o)\in[0,1]$). Furthermore:

$\mathsf{IntBetweenZeroL}(k,c):=\bigwedge_{o\in\mathsf{O}}(\bigvee_{0\leq
p\leq l}k_{o}=p)\wedge((c=0)\Rightarrow(k_{o}\leq l-1))$

where, for all $o\in\mathsf{O}$, $k_{o}\in\llbracket 0,l\rrbracket$ is the
index of $o$ given by $p$ (assuming that $p(o)\in K_{l}$). Furthermore, since
the size of $E$ is at most $l-1$, if $c=0$, then the maximum of the colors
should be at most $l-1$.

Then, $u$ is the value of the game $\mathcal{G}_{(\mathcal{F},E)}$ from the
state $q_{\mathsf{init}}$. This is ensured by the remainder of the formula: it
exhibits a $\mathsf{GF}$-strategy per player whose corresponding positional
strategy parity dominates the valuation $v_{Y}^{u}$ for $Y:=(\mathcal{F},E)$.
The predicates are used for both players, we give them only for Player
$\mathsf{A}$, the case of Player $\mathsf{B}$ being analogous.

$\mathsf{IsIndicator}(S_{\mathsf{A}}):=\bigwedge_{1\leq i\leq
n}((S_{\mathsf{A}}^{i}=0)\lor(S_{\mathsf{A}}^{i}=1))$

where $S_{\mathsf{A}}$ encodes the support of the $\mathsf{GF}$-strategy
$\sigma_{\mathsf{A}}$. The fact that it is indeed a Player-$\mathsf{A}$
$\mathsf{GF}$-strategy is ensured by the predicates below:

$\mathsf{IsStrategy}_{\mathsf{A}}(\sigma_{\mathsf{A}}):=\bigwedge_{1\leq i\leq
n}((0\leq\sigma_{\mathsf{A}}^{i}\leq
1)\wedge(\sum_{i=1}^{n}\sigma_{\mathsf{A}}^{i}=1))$

In addition, we have:

$\mathsf{IsSupp}(\sigma_{\mathsf{A}},S_{\mathsf{A}}):=\bigwedge_{1\leq i\leq
n}((\sigma_{\mathsf{A}}^{i}>0)\Leftrightarrow(S_{\mathsf{A}}^{i}=1))$

This predicate ensures that $S_{\mathsf{A}}$ does indeed correspond to the
support of the $\mathsf{GF}$-strategy $\sigma_{\mathsf{A}}$. Furthermore:

$\mathsf{Val}_{\mathsf{A}}(\sigma_{\mathsf{A}},\alpha,v,u):=\bigwedge_{1\leq
j\leq k}(\sum_{i=1}^{n}\sigma_{\mathsf{A}}^{i}\cdot(\alpha_{\varrho(i,j)}\cdot
v_{\varrho(i,j)}+(1-\alpha_{\varrho(i,j)})\cdot u)\geq u)$

This predicates encodes the fact that the Player-$\mathsf{A}$
$\mathsf{GF}$-strategy $\sigma_{\mathsf{A}}$ dominates the valuation
$v_{Y}^{u}$. Indeed, note that for all $o\in\mathsf{O}$, if $\alpha_{o}=1$,
then $p(o)\in[0,1]$, and therefore $v_{Y}^{u}(o)=p(o)=v_{o}$. Similarly, if
$\alpha_{o}=0$, then $p(o)\in K_{l}$, and therefore $v_{Y}^{u}(o)=u$. Finally,
when $l$ is even, denoting $l=2\cdot x$ with $x\in\mathbb{N}$:

$\displaystyle\mathsf{MaxIntegerEven}(S_{\mathsf{A}},k,j,c):=$
$\displaystyle\bigvee_{1\leq i\leq
n}(S_{\mathsf{A}}^{i}=1\wedge\alpha_{\varrho(i,j)}=1)\lor$
$\displaystyle\bigvee_{0\leq e\leq x}(2e\geq c)\wedge((\bigvee_{1\leq i\leq
n}(S_{\mathsf{A}}^{i}=1)\wedge(k_{\varrho(i,j)}=2e))\;\wedge$
$\displaystyle(\bigwedge_{1\leq i\leq
n}(S_{\mathsf{A}}^{i}=1)\Rightarrow(k_{\varrho(i,j)}\leq 2\cdot e)))$

It is similar if $l$ is odd, up to small changes. This predicate encodes item
$(ii.2)$ of Lemma 21: for all columns $j\in\mathsf{Act}_{\mathsf{B}}$, either
there is positive probability to see an outcome mapped to a value in $[0,1]$
(i.e.
$\mathsf{out}{\langle\mathcal{F},\mathbbm{1}_{p^{-1}[0,1]}\rangle}(\sigma_{\mathsf{A}},j)>0$)
or the maximum of the colors in the support of the strategy
$\sigma_{\mathsf{A}}$ is even (i.e.
$\max(\mathsf{Color}(\mathcal{F},p,\sigma_{\mathsf{A}},j)\cup\\{c\\})$ is
even).

By Lemma 21 and Proposition 57, we have that $\mathcal{F}\in\mathsf{ParO}(l)$
if and only if
$\Phi_{\mathcal{F}}^{\mathsf{ParO}(l)}\in\mathsf{True}_{\mathsf{FO}-\mathbb{R}}$.
Furthermore, the size of $\Phi_{\mathcal{F}}^{\mathsf{ParO}(l)}$ is polynomial
in the size of $\mathcal{F}$ (and in $l$).

Finally, since given an environment, an outcome is mapped to at most one
integer, and since in relevant environments of size $n\in\mathbb{N}$, the
outcomes are mapped to at least $n-1$ different integers, we have
$\mathcal{F}\in\mathsf{ParO}\Leftrightarrow\mathcal{F}\in\mathsf{ParO}(n+2)$
for $n:=|\mathsf{O}|$. The proposition follows. ∎

###  7.3 Hierarchy

For all $n\in\mathbb{N}$, the game forms in $\mathsf{ParO}(n)$ are the ones to
be used — to ensure the existence of positional optimal strategies for both
players — in parity games at states where the gap between the color of the
state and the maximum color in the game is at most $n$. Straightforwardly,
$\mathsf{ParO}(n)\subseteq\mathsf{ParO}(n+1)$. In fact, this inclusion is
strict for all $n\in\mathbb{N}$. This defines an infinite hierarchy of game
forms.

######  Proposition 59.

For all $n\in\mathbb{N}$, the set of game forms positionally optimizable up to
$n$ (i.e. $\mathsf{ParO}(n)$) strictly contains the set of game forms
optimizable up to $n+1$ (i.e. $\mathsf{ParO}(n+1)$). That is, we have
$\mathsf{ParO}(n)\supsetneq\mathsf{ParO}(n+1)$.

For all $n\geq 1$, we exhibit a standard finite game form $\mathcal{F}_{n}$
that is in $\mathsf{ParO}(n-1)$ but not in $\mathsf{ParO}(n)$. This is done in
Definition 60 below, where we describe a game form that is $\mathsf{ParO}(n)$
but not in $\mathsf{ParO}(n-1)$ in the case where $n$ is even.

######  Definition 60.

Consider some even integer $n\geq 2$. We consider the set of outcomes
$\mathsf{O}_{n}:=\\{x_{0},x_{1},\ldots,x_{n-1},y,z\\}$ and we consider the
game form
$\mathcal{F}_{n}=\langle\mathsf{Act}_{\mathsf{A}}^{n},\mathsf{Act}_{\mathsf{B}}^{n},\mathsf{O}_{n},\varrho_{n}\rangle_{\mathsf{s}}$
depicted in Figure 9. Let us describe the set of actions of the players.We
set:

  * •

$\mathsf{Act}_{\mathsf{A}}^{n}:=\\{a_{\mathsf{t}},a_{\mathsf{b}},a_{1},\ldots,a_{n-1},a_{1,0},\ldots,a_{n-1,n-2},a_{\mathsf{Ex}}\\}$;
and

  * •

$\mathsf{Act}_{\mathsf{B}}^{n}:=\\{b_{\mathsf{l}},b_{\mathsf{r}},b_{0},\ldots,b_{n-2},b_{2,1},\ldots,b_{n-2,n-3},b_{\mathsf{Ex}}\\}$.

The actions $a_{\mathsf{t}},a_{\mathsf{b}}$ (resp.
$b_{\mathsf{l}},b_{\mathsf{r}}$) refer to the two topmost rows (resp. leftmost
columns): $a_{\mathsf{t}}$ (resp. $b_{\mathsf{l}}$) leads to
$\frac{x_{0}+\ldots+x_{n-1}}{n},\frac{3y+z}{4}$ whereas $a_{\mathsf{b}}$
(resp. $b_{\mathsf{r}}$) leads to $\frac{3y+z}{4},\frac{y+3z}{4}$. Then, for
all odd $i\leq n-1$ (resp. even $j\leq n-2$) $a_{i}$ and $a_{i,i-1}$ (resp.
$b_{j}$ and $b_{j,j-1}$ — only if $j\geq 2$) correspond to the rows leading to
$x_{i}$ and $\frac{x_{i}+x_{i-1}}{2}$ (resp. columns leading to $x_{j}$ and
$\frac{x_{j}+x_{j-1}}{2}$) respectively. Finally, action $a_{\mathsf{Ex}}$
(resp. $b_{\mathsf{Ex}}$) correspond to the bottommost row (resp. rightmost
column).

Figure 9: The game form $\mathcal{F}_{n}$. Due to a lack of space, $h$ refers
to $n-1$ and $h^{\prime}$ to $n-2$.

The game forms described in Definition 60 satisfies the lemma below.

######  Lemma 61 (Proof E.3, Page E.3).

Consider some even $n\geq 2$. The game form of $\mathcal{F}_{n}$ Definition 60
is:

  * •

positionally maximizable w.r.t. Player $\mathsf{B}$;

  * •

positionally maximizable w.r.t. Player $\mathsf{A}$ up to $n-1$ but not up to
$n$.

That is: $\mathcal{F}_{n}\in\mathsf{ParO}(n)\setminus\mathsf{ParO}(n-1)$.

The proof of this lemma is very tedious since it requires to consider a lot of
different possibilities in terms of which outcome is mapped to which value or
color. We give here an informal proof of this lemma in the case where $n=2$.
The game form $\mathcal{F}_{2}$ is depicted in Figure 11.

Figure 10: The game form $\mathcal{F}_{2}$.

Figure 11: The game form $\mathcal{F}_{2}$ in a specific environment.

###### Proof sketch.

Consider a relevant environment $E=\langle
c,e,p\rangle\in\mathsf{Env}(\mathsf{O})$ and the corresponding parity game
$\mathcal{G}_{(\mathcal{F}_{2},E)}$ (recall Definition 16). We let
$u:=\chi_{\mathcal{G}_{(\mathcal{F}_{2},E)}}(q_{\mathsf{init}})$. For all
$t\in\mathsf{O}_{2}$, if $p(t)\notin[0,1]$, we let $n_{t}\in\llbracket
0,e\rrbracket$ denote the integer that $t$ is mapped to w.r.t. $p$, i.e. the
integer ensuring $p(t)=k_{n_{t}}$. We want to show that, in any case, Player
$\mathsf{B}$ has a $\mathsf{GF}$-strategy that is optimal w.r.t.
$(\mathcal{F}_{2},E)$ and that this also holds for Player $\mathsf{A}$ as long
as $c=e$ (i.e. if $\mathsf{Sz}(E)=0=n-2$). However, there is a relevant
environment $E$ with $\mathsf{Sz}(E)=1$ such that Player $\mathsf{A}$ has no
$\mathsf{GF}$-strategy optimal w.r.t. $(\mathcal{F}_{2},E)$. There are several
cases, we detail some of them.

  * •

Assume that $p(y),p(z)\notin[0,1]$. This implies $u\in\\{0,1\\}$ and playing
action $a_{\mathsf{Ex}}$ for Player $\mathsf{A}$ and action $b_{\mathsf{Ex}}$
for Player $\mathsf{B}$ is optimal w.r.t. $(\mathcal{F}_{2},E)$.

  * •

Assume now that $p(y)\in[0,1]$ and $p(z)\notin[0,1]$. Then, we have $u=p(y)$.
The reason is that, by playing action $a_{\mathsf{Ex}}$, Player $\mathsf{A}$
ensures that almost surely a stopping state of value $p(y)$ is reached.
Furthermore, Player $\mathsf{B}$ can ensure the same thing by playing action
$b_{\mathsf{Ex}}$. Then, playing action $a_{\mathsf{Ex}}$ for Player
$\mathsf{A}$ and action $b_{\mathsf{Ex}}$ for Player $\mathsf{B}$ is optimal
w.r.t. $(\mathcal{F}_{2},E)$. This is similar if $p(y)\notin[0,1]$ and
$p(z)\in[0,1]$.

  * •

Assume now $p(y),p(z)\in[0,1]$. If $p(y)<p(z)$, then we have
$u=\frac{3p(y)+p(z)}{4}$, and as before playing action $a_{\mathsf{Ex}}$ for
Player $\mathsf{A}$ and action $b_{\mathsf{Ex}}$ for Player $\mathsf{B}$ is
optimal w.r.t. $(\mathcal{F}_{2},E)$.

  * •

Assume now that $p(y),p(z)\in[0,1]$ and $p(y)\geq p(z)$. If $p(x_{0})\in[0,1]$
or $p(x_{1})\in[0,1]$, we can also exhibit an optimal $\mathsf{GF}$-strategy
for both players.

  * •

Let us now assume that $p(y),p(z)\in[0,1]$ with $p(y)\geq p(z)$. For
simplicity, we assume that $p(y)=1$ and $p(z)=0$. In that case, we have:

$\frac{1}{4}=\frac{3p(z)+p(y)}{4}\leq u\leq\frac{p(z)+3p(y)}{4}=\frac{3}{4}$

Assume also that $p(x_{0}),p(x_{1})\notin[0,1]$. Assume first that $n_{x_{0}}$
is odd. In that case, $u=\frac{1}{4}$. A Player-$\mathsf{B}$ strategy playing
positionally action $b_{0}$ achieves this value in the game
$\mathcal{G}_{(\mathcal{F}_{2},E)}$. Thus, the Player-$\mathsf{A}$
$\mathsf{GF}$-strategy $a_{\mathsf{Ex}}$ is optimal w.r.t.
$(\mathcal{F}_{2},E)$.

Assume now that $n_{x_{0}}$ is even. Then, we have $u=\frac{3}{4}$: Indeed,
for all $\varepsilon>0$, a Player-$\mathsf{A}$ positional strategy playing
action $a_{\mathsf{t}}$ with probability $1-\varepsilon$ and action
$a_{\mathsf{b}}$ with probability $\varepsilon$ has value at least
$\frac{3}{4}-\varepsilon$ in the game $\mathcal{G}_{(\mathcal{F}_{2},E)}$.
Therefore, playing action $b_{\mathsf{Ex}}$ is always optimal for Player
$\mathsf{B}$. It will also be the case for Player $\mathsf{A}$ if
$\mathsf{Sz}(E)=0$, i.e. if $c=e$. Indeed, in that case, we have either
$n_{x_{0}}=n_{x_{1}}=0$, in which case $u=\frac{3}{4}$ and the
Player-$\mathsf{A}$ $\mathsf{GF}$-strategy $a_{1}$ is optimal w.r.t.
$(\mathcal{F}_{2},E)$; or $n_{x_{0}}=n_{x_{1}}=1$, in which case we are in the
scope of the previous case of this item since $n_{x_{0}}$ is odd. However, if
$\mathsf{Sz}(E)=1$, there may be an issue for Player $\mathsf{A}$, as we show
below.

Consider now a relevant environment $E=\langle c,e,p\rangle$ of size 1 such
that $c:=0$, $p(y):=1$, $p(z):=0$, $p(x_{0})=k_{0}$ and $p(x_{1})=k_{1}$. We
do have $\mathsf{Sz}(E)=1$. What we obtain is depicted in Figure 11. In that
case, we have
$u:=\chi_{\mathcal{G}_{\mathcal{F}_{2},E}}(q_{\mathsf{init}})=\frac{3}{4}$, as
argued above in the last item. Consider any Player-$\mathsf{A}$
$\mathsf{GF}$-strategy
$\sigma_{\mathsf{A}}\in\Sigma_{\mathsf{A}}(\mathcal{F}_{2})$. If it plays
action $a_{\mathsf{b}}$ or action $a_{\mathsf{Ex}}$ with positive probability,
then the strategy
$\mathsf{s}_{\mathsf{A}}^{(\mathcal{F}_{2},E)}(\sigma_{\mathsf{A}})$ does not
dominate the valuation $v^{u}_{(\mathcal{F}_{2},E)}$. However, if it does not
play these actions with positive probability, the strategy
$\mathsf{s}_{\mathsf{A}}^{(\mathcal{F}_{2},E)}(\sigma_{\mathsf{A}})$ has value
0 in $\chi_{\mathcal{G}_{(\mathcal{F}_{2},E)}}$ from $q_{\mathsf{init}}$.
Indeed, by positionally playing action $b_{\mathsf{l}}$, Player $\mathsf{B}$
ensures that: 1) surely, no stopping state is seen, and 2) almost surely, the
state $k_{1}$ (of color 1) is seen infinitely often, while $c=0$. ∎

Let us now consider the proof of Proposition 59.

###### Proof.

Let $n\geq 1$. The inclusion $\mathsf{ParO}(n-1)\supseteq\mathsf{ParO}(n)$ is
direct. Lemma 61 ensures that these two sets are not equal when $n$ is even. A
similar lemma could be stated in the case where $n$ is odd. ∎

## References

  * [1] Benjamin Bordais, Patricia Bouyer, and Stéphane Le Roux.  Playing subgame optimally in concurrent games with prefix-independent objectives.  Accepted FoSSaCs 2023.
  * [2] Benjamin Bordais, Patricia Bouyer, and Stéphane Le Roux.  From local to global determinacy in concurrent graph games.  In Mikolaj Bojanczyk and Chandra Chekuri, editors, 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2021, December 15-17, 2021, Virtual Conference, volume 213 of LIPIcs, pages 41:1–41:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021.
  * [3] Benjamin Bordais, Patricia Bouyer, and Stéphane Le Roux.  Optimal strategies in concurrent reachability games.  In Florin Manea and Alex Simpson, editors, 30th EACSL Annual Conference on Computer Science Logic, CSL 2022, February 14-19, 2022, Göttingen, Germany (Virtual Conference), volume 216 of LIPIcs, pages 7:1–7:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022\.
  * [4] Benjamin Bordais, Patricia Bouyer, and Stéphane Le Roux.  Playing (almost-)optimally in concurrent büchi and co-büchi games.  In Anuj Dawar and Venkatesan Guruswami, editors, 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2022, December 18-20, 2022, IIT Madras, Chennai, India, volume 250 of LIPIcs, pages 33:1–33:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.
  * [5] Benjamin Bordais, Patricia Bouyer, and Stéphane Le Roux.  Playing (almost-)optimally in concurrent büchi and co-büchi games.  CoRR, abs/2203.06966, 2022.
  * [6] Krishnendu Chatterjee, Luca de Alfaro, and Thomas A. Henzinger.  The complexity of quantitative concurrent parity games.  In Proceedings of the Seventeenth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2006, Miami, Florida, USA, January 22-26, 2006, pages 678–687. ACM Press, 2006.
  * [7] Krishnendu Chatterjee, Marcin Jurdzinski, and Thomas A. Henzinger.  Quantitative stochastic parity games.  In Proceedings of the Fifteenth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2004, New Orleans, Louisiana, USA, January 11-14, 2004, pages 121–130. SIAM, 2004.
  * [8] Luca de Alfaro and Thomas A. Henzinger.  Concurrent omega-regular games.  In 15th Annual IEEE Symposium on Logic in Computer Science, Santa Barbara, California, USA, June 26-29, 2000, pages 141–154. IEEE Computer Society, 2000.
  * [9] Luca de Alfaro and Rupak Majumdar.  Quantitative solution of omega-regular games.  Journal of Computer and System Sciences, 68:374–397, 2004.
  * [10] Hugh Everett.  Recursive games.  Annals of Mathematics Studies – Contributions to the Theory of Games, 3:67–78, 1957.
  * [11] Panganamala R Kumar and Tzong-Huei Shiau.  Existence of value and randomized strategies in zero-sum discrete-time stochastic dynamic games.  SIAM Journal on Control and Optimization, 19(5):617–634, 1981.
  * [12] Marta Kwiatkowska, Gethin Norman, David Parker, Gabriel Santos, and Rui Yan.  Probabilistic model checking for strategic equilibria-based decision making.  LIPIcs. Leibniz-Zentrum für Informatik, 2022.  To appear; Available as arXiv:2206.15148.
  * [13] Donald A. Martin.  The determinacy of blackwell games.  The Journal of Symbolic Logic, 63(4):1565–1581, 1998.
  * [14] James Renegar.  On the computational complexity and geometry of the first-order theory of the reals, part III: quantifier elimination.  J. Symb. Comput., 13(3):329–352, 1992.
  * [15] Alfred Tarski.  A decision method for elementary algebra and geometry.  Springer, 1998.
  * [16] John von Neumann and Oskar Morgenstern.  Theory of Games and Economic Behavior.  Princeton Univ. Press, Princeton, 1944.
  * [17] Wieslaw Zielonka.  Infinite games on finitely coloured graphs with applications to automata on infinite trees.  Theoretical Computer Science, 200(1–2):135–183, 1998.
  * [18] Wiesław Zielonka.  Perfect-information stochastic parity games.  In Proc. 7th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS’04), volume 2987 of Lecture Notes in Computer Science, pages 499–513. Springer, 2004.

##  Appendix A Explanations on Table 1 from the introduction

Let us describe exactly what the rows and columns of the table refer to.
First, the rows correspond to the objectives considered in a finite concurrent
arena:

  * •

Safety: Player $\mathsf{A}$ wants to avoid a target (i.e. a set of states);

  * •

Reach: stands for reachability, Player $\mathsf{A}$ wants to reach a target;

  * •

Büchi: Player $\mathsf{A}$ wants to reach a target infinitely often, it
corresponds to a parity objective with colors $1$ and $2$;

  * •

co-B: stands for co-Büchi, Player $\mathsf{A}$ wants to reach a target only
finitely often, it corresponds to a parity objective with colors $0$ and $1$;

  * •

Parity: arbitrary parity objective.

Consider now the columns.

  * •

The first column on the left, $\exists$ opt strat?, tells if there always
exist optimal strategies in finite games for these objectives. This holds for
the safety objective, but it does not for reachability, therefore it does not
either for Büchi, co-Büchi and parity as they are more involved than the
reachability objective.

  * •

The second column, opt, tells the simpler kind of strategies that allow to
play optimally, assuming it is possible. In any cell, pos stands for
positional whereas $\infty$ stands for infinite memory, i.e. strategies that
cannot be described with a finite automaton.

  * •

The third column, $\varepsilon$-opt, tells the simpler kind of strategies that
allow to play $\varepsilon$-optimally. Note that such strategies always exist
by definition of the value of the game.

  * •

Finally, the forth column, SubG-opt, tells the simpler kind of strategies that
allow to play subgame optimally, assuming it is possible. A strategy is
subgame optimal if all of its residual strategies are optimal. (See e.g. [1]
for more details.) Note that being subgame is stronger than being optimal,
however both notions coincide on positional strategies. Note that the need for
infinite-memory strategies for arbitrary parity objectives already occurs with
3 colors.

##  Appendix B Algorithms

1:procedure CreateEnv($k,q,\mathsf{vcol}$)

2: if $k$ is even then

3: return $E_{q,\mathsf{vcol}}^{k}$

4: end if

5: if $k$ is odd then

6: $m\leftarrow\max(k-2,0)$

7: return $E_{q,\mathsf{vcol}}^{m}$

8: end if

9:end procedure

Figure 12: Build an environment from a state, a color and a coloring function

1:procedure UpdCurSta($k,\mathsf{vcol},\mathsf{Ev}$)

2: for $q\in Q_{u}$ do

3: if $\mathsf{vcol}(q)=k$ then

4: $\mathsf{Ev}[q]\leftarrow\mathsf{CreateEnv}(k,q,\mathsf{vcol})$

5: end if

6: end for

7: return $\mathsf{Ev}$

8:end procedure

Figure 13: Updates the Environment for the states of the current color

1:procedure UpdNewSta($k,\mathsf{vcol},\mathsf{Ev}^{\prime}$)

2: $\mathsf{change}\leftarrow\mathsf{True}$

3: while change do

4: $\mathsf{change}\leftarrow\mathsf{False}$

5: for $q\in Q_{u}$ do

6: if $\mathsf{NewCol}(q,\mathsf{vcol})=k$ then

7: $\mathsf{Ev}^{\prime}[q]\leftarrow\mathsf{CreateEnv}(k,q,\mathsf{vcol})$;
$\mathsf{vcol}[q]\leftarrow k$

8: $\mathsf{change}\leftarrow\mathsf{True}$; break;

9: end if

10: end for

11: end while

12: return $(\mathsf{vcol},\mathsf{Ev}^{\prime})$

13:end procedure

Figure 14: Updates the Environment and Coloring Functions for new states of a
specific color

1:procedure UpdateColEnv($k,\mathsf{vcol},\mathsf{Ev}^{\prime}$)

2:
$\mathsf{Ev}^{\prime}\leftarrow\mathsf{UpdCurSta}(k,\mathsf{vcol},\mathsf{Ev}^{\prime})$

3: $\mathsf{UpdNewSta}(k,\mathsf{vcol},\mathsf{Ev}^{\prime})$

4:end procedure

Figure 15: Updates the Environment and Coloring Functions for a specific color

1:procedure IncLeast($\mathsf{col}^{\prime},\mathsf{Ev}^{\prime}$)

2: $c_{\mathsf{min}}\leftarrow\min\mathsf{vcol}$

3: for $q\in Q_{u}$ do

4: if $\mathsf{vcol}(q)=c_{\mathsf{min}}$ then

5: $\mathsf{vcol}(q)\leftarrow c_{\mathsf{min}}+2$;

6: end if

7: if $\mathsf{vcol}(q)=c_{\mathsf{min}}+1$ then

8: $\mathsf{vcol}(q)\leftarrow\mathsf{col}(q)$;

9: $\mathsf{Ev}^{\prime}[q]\leftarrow\mathsf{NoEnv}$;

10: end if

11: end for

12:
$\mathsf{UpdNewSta}(c_{\mathsf{min}}+2,\mathsf{vcol},\mathsf{Ev}^{\prime})$

13:end procedure

Figure 16: Increases the least color, resets the last but least layer

1:procedure ComputeEnv($u,\mathsf{col}$)

2: $\mathsf{vcol}\leftarrow\mathsf{col}$

3: $\mathsf{Ev}\leftarrow\mathsf{EmptyEnv}$

4: for $k=e\textsf{ down to }0$ do

5:
$(\mathsf{vcol},\mathsf{Ev})\leftarrow\mathsf{UpdateColEnv}(k,\mathsf{vcol},\mathsf{Ev})$

6: end for

7: while $\mathsf{vcol}[Q_{u}]\neq\\{e\\}$ do

8:
$(\mathsf{vcol},\mathsf{Ev})\leftarrow\mathsf{IncLeast}(\mathsf{vcol},\mathsf{Ev})$

9: for $k=e\textsf{ down to }0$ do

10:
$(\mathsf{vcol},\mathsf{Ev})\leftarrow\mathsf{UpdateColEnv}(k,\mathsf{vcol},\mathsf{Ev})$

11: end for

12: end while

13: return $(\mathsf{vcol},\mathsf{Ev})$

14:end procedure

Figure 17: Computes an environment function guaranteeing $u$ for Player
$\mathsf{A}$ in $Q_{u}$

##  Appendix C Complements on strategies and valuations

###  C.1 How to implement stopping states

This can be done in a straightforward manner: given a stopping state of value
$u\in[0,1]$, we consider a probability distribution that goes with probability
$u$ to a (self-looping) state $q_{\mathsf{A}}$ of value 1 and that goes to a
(self-looping) state $q_{\mathsf{B}}$ of value 0 with probability $1-u$.
Furthermore, note that the two corresponding BSCCs $\\{q_{\mathsf{A}}\\}$ and
$\\{q_{\mathsf{B}}\\}$ (which exists regardless of the strategies of the
players) behave properly w.r.t. the conditions for parity dominating a
valuation (again, regardless of the strategies).

###  C.2 Markov chain induced by a pair of strategies

######  Definition 62 (Markov chain induced by a pair of positional
strategies).

Consider a concurrent arena $\mathcal{C}$ and two positional strategies
$\mathsf{s}_{\mathsf{A}}$ (for Player $\mathsf{A}$) and
$\mathsf{s}_{\mathsf{B}}$ (for Player $\mathsf{B}$). The Markov chain
$\mathcal{M}_{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}=\langle
Q,\mathbb{P}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}\rangle$
_induced_ by $\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}$ is such that,
for all $q\in Q$:

$\forall q^{\prime}\in
Q,\;\mathbb{P}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}(q)(q^{\prime}):=\mathsf{out}_{\langle\mathsf{F}(q),\mathbbm{1}_{q^{\prime}}\rangle}(\mathsf{s}_{\mathsf{A}}(q),\mathsf{s}_{\mathsf{B}}(q))$

###  C.3 Proof of Theorem 13

This theorem is straightforwardly deduced from already existing work,
specifically, [3] and [5]. In particular, in this paper, results are stated by
using the notion of MDPs and End Component. Informally, MDPs are games where
only one Player plays. In particular, one obtains an MDP from a concurrent
game by fixing the (positional) strategy of a player. An End Component $H$ (EC
for short) in an MDP is a set of states $Q_{H}\subseteq Q$ such that one can
ensure to stay in $Q^{\prime}$ while the underlying graph of $H$ if strongly
connected. In particular, BSCCs are special cases of end components.

######  Proof.

The first part of the theorem is given by [3, Proposition 18]. As for the
second part, we apply [5, Lemma 17]. Indeed, the first condition is ensured by
assumption. As for the second, consider a End Component $H$ with $v_{H}>0$.
This can be seen as a finite MDP — where only Player $\mathsf{B}$ plays — with
a parity objective. From [7], Player $\mathsf{B}$ has an optimal strategy
$\mathsf{s}_{\mathsf{B}}$ that is positional and deterministic. Then, we
obtain a Markov chain $H_{\mathsf{s}_{\mathsf{B}}}$ where all BSCCs are