\begin{document}

	\author{Benjamin Bordais, Patricia Bouyer and Stéphane Le Roux}
	
	\title{Sub-game optimal strategies in concurrent games with prefix-independent objectives}
	\maketitle
	
	\begin{abstract}
		We investigate concurrent two-player win/lose stochastic games on
		finite graphs with prefix-independent objectives. We characterize
		subgame optimal strategies and use this characterization to show
		various memory transfer results: 1) For a given (prefix-independent)
		objective, if every game that has a subgame \emph{almost-surely
			winning} strategy also has a positional one, then every game that
		has a subgame \emph{optimal} strategy also has a positional one;

		2) Assume that the (prefix-independent) objective has a neutral
		color. If every \emph{turn-based} game that has a subgame
		almost-surely winning strategy also has a positional one, then every
		game that has a \emph{finite-choice} (notion to be defined)

		subgame optimal strategy also has a positional one.
		
		We collect or design examples to show that our results are tight in
		several ways. We also apply our results to Büchi, co-Büchi, parity,
		mean-payoff objectives, thus yielding simpler statements.
	\end{abstract}
	
	\ensuremath{\mathsf{s}}ection{Introduction}
	
	Turn-based two-player win/lose (stochastic) games on finite graphs have been
	intensively studied in the context of model checking in a broad
	sense~\cite{thomas02,BCJ18}.

	These games behave well regarding optimality in various settings. Most
	importantly for this paper, \cite{GIH10} proved the following results
	for finite turn-based stochastic games with prefix-independent
	objectives: (1) every game has deterministic optimal strategies; (2)
	from every value-$1$ state, there is an optimal, i.e. almost-surely
	winning, strategy; (3) if from every value-$1$ state of every game
	there is an optimal strategy using some fixed amount of memory, every
	game has an optimal strategy using this amount of memory. These
	results are of either of the following generic forms:
	\begin{itemize}
		\item In all games, (from all nice states) there is a nice strategy.
		
		\item If from all \emph{nice states} of all games there is a nice
		strategy, so it is from all \emph{states}.
	\end{itemize}
	

	The concurrent version of these turn-based (stochastic) games has a
	higher modeling power than the turn-based version: this is really
	useful in practice since real-world systems are intrinsically
	concurrent~\cite{KNPS21}. They are played on a finite graph as
	follows: at each player state, 
	the two players stochastically and independently choose one among
	finitely many actions. This yields a Nature state, which
	stochastically draws a next player state, from where each player
	chooses one action again, and so on.  Each player state is labelled by
	a color, and who wins depends on the infinite sequence of colors
	underlying the (stochastically) generated infinite sequence of player
	states.

	Unfortunately, these concurrent games do
	not behave well in general even for simple winning conditions and
	simple graph structures, like finite graphs:
	\begin{itemize}
		\item Reachability objectives: there is a game without optimal
		strategies \cite{everett57};
		\item B\"uchi objectives: there is a game with value $1$ while all
		finite-memory strategies have value $0$ \cite{AH00};
		\item Co-B\"uchi objectives: although there are always positional
		$\ensuremath{\mathsf{val}}repsilon$-optimal strategies \cite{AH06}, there is a game with optimal
		strategies but without finite-memory optimal strategies \cite{BBSArXivICALP}; 
		\item Parity \cite{AH00} and mean-payoff
		\cite{DBLP:journals/iandc/ChatterjeeI15} objectives: there is a game
		with subgame almost-surely-winning strategies, but where all
		finite-memory strategies have value $0$.
	\end{itemize}
	
	In this paper, we focus on concurrent stochastic finite
	games. Therefore, the generic forms of our results will be more
	complex, in order to take into account the above-mentioned
	discrepancies. They will somehow 
	be given as generic statements as follows:

	\begin{itemize}
		\item Every game that has a \emph{nice} strategy also has a
		\emph{nicer} one.		
		\item If all \emph{special games} that have a nice strategy have a
		nicer one, so it is for all \emph{games}.
	\end{itemize}
	Much of the difficulty consists in fine-tuning the strength of
	``nice'', ``nicer'' and ``special'' above. We present below our main
	contributions on finite two-player win/lose concurrent stochastic
	games with prefix-independent objectives:
	\begin{enumerate}
		\item\label{main1} We provide a characterization of subgame optimal
		strategies, which are strategies that are optimal after every
		history (Theorem~\ref{thm:subgame_optimal_arbitrary_strategy}): a Player $\mathsf{A} $
		strategy is subgame optimal iff 1) it is
		locally optimal and 2) for every Player $\mathsf{B} $ deterministic strategy,
		after every history, if the visited states have the same positive
		value, Player $\mathsf{A} $ wins with probability $1$. This characterization is 
		used to prove all the results below.
		
		\item\label{main2} We prove memory transfer results from subgame
		almost-surely winning strategies to subgame optimal strategies:
		\begin{enumerate}
			\item\label{main21} Theorem~\ref{thm:transfer_memory}: If every game that has
			a subgame
			\emph{almost-surely winning} strategy also has a positional one,
			then every game that has a subgame \emph{optimal} strategy also
			has a positional one.
			
			\item Corollary~\ref{coro:application_buchi_cobuchi}: every Büchi or co-Büchi
			game that has a subgame
			optimal strategy has a positional one. (Whereas parity games may
			require infinite memory \cite{AH00}.)
		\end{enumerate}
		Note that the transfer result~{\bfseries\ensuremath{\mathsf{s}}ffamily
			\color{darkgray}\ref{main21}} is generalized from positional to
		finite memory in appendix.
		

		
		\item We say that a strategy has finite-choice, if it uses only
		finitely many action distributions. Note that finite-memory
		(resp. deterministic) strategies clearly have finite choice.
		\begin{enumerate}
			\item\label{main31} Theorem~\ref{thm:fair_strategy_uniformly_optimal}: In a
			given game, if there is a finite-choice
			optimal strategy, there is a finite-choice \emph{subgame} optimal
			strategy.
			
			\item\label{main32} Theorem~\ref{thm:transfer_memory_finite_choice}: Assume
			that the objective has a neutral
			color. If every \emph{turn-based} game that has a subgame
			almost-surely winning strategy also has a positional one, then
			every game that has a \emph{finite-choice} subgame optimal
			strategy also has a positional one.
			
			\item\label{main33} Corollary~\ref{coro:transfer_memory_finite_choice}: every
			parity or mean-payoff game that
			has a finite-memory subgame optimal strategy also has a
			positional one.
		\end{enumerate}
		Note

		that {\bfseries\ensuremath{\mathsf{s}}ffamily \color{darkgray}\ref{main31}} and
		{\bfseries\ensuremath{\mathsf{s}}ffamily \color{darkgray}\ref{main32}} are false if the
		word finite-choice is removed \cite{BBSArXivICALP}. The proof of
		{\bfseries\ensuremath{\mathsf{s}}ffamily \color{darkgray}\ref{main32}} invokes
		{\bfseries\ensuremath{\mathsf{s}}ffamily \color{darkgray}\ref{main31}}. Flavor (and
		proofs) of {\bfseries\ensuremath{\mathsf{s}}ffamily \color{darkgray}\ref{main32}} and
		{\bfseries\ensuremath{\mathsf{s}}ffamily \color{darkgray}\ref{main21}} are similar, but
		both premises and conclusions are weakened in {\bfseries\ensuremath{\mathsf{s}}ffamily
			\color{darkgray}\ref{main32}}, as emphasized.
	\end{enumerate}
	

	\

	
	\textbf{Related works.}  A large part of this paper is
	dedicated to the extension to concurrent games of the results from
	\cite{GIH10} regarding the transfer of memory from almost-surely
	winning strategies to optimal strategies in turn-based games. Note
	that the proof technique used in \cite{GIH10} is different 
	and could
	not be adapted to our more general setting. In their proof, both
	players agree on a preference over Nature states and play
	according to this preference. 

	In our proof, we slice the graph into value areas (that is, sets of
	states with the same value), and show that it is sufficient to play an
	almost-sure winning strategy in each slice; we then glue these (partial)
	strategies together to get a subgame-optimal strategy over the whole
	graph.
	

	

	The slicing technique was already used in the context of concurrent
	games in~\cite{AH06}. The authors focus on parity objectives and
	establishes a memory transfer result from limit-sure winning
	strategies to almost-optimal strategies. As an application, they show
	that, for co-Büchi objectives, since positional strategies are
	sufficient to win limit-surely, they also are to win
	almost-optimally. Their construction made heavy use of the specific
	nature of parity objectives.
	
	

	
	We also mention \cite{CH07}, where the focus is also on concurrent
	games with prefix-independent objectives. In particular, the authors
	establish a (very useful) result: if all states have positive
	values, then they all have value 1. (Note that a strengthening of
	this result is presented in this paper
	(Theorem~\ref{thm:all_not_zero_implies_almost_sure}), which also
	appears as an adaptation of a result proved in \cite{GIH10}). 
	This result is then used in another context with non-zero-sum
	games. 

	

	Finally, some recent works on concurrent games have been done in
	\cite{BBSFSTTCS21,BBSCSL22,BBSArXivICALP}, where the goal is the
	following: local interactions of the two players in the player
	state are given by bi-dimensional tables; those tables can be
	abstracted as \emph{game forms}, where (output) variables are
	issues of the local interaction (possibly several issues are
	labelled by the same variable). The goal of this series of works
	is to give (intrinsic) properties of these game forms, so that,
	when used in a graph game, the existence of optimal strategies is
	ensured. For instance, in~\cite{BBSCSL22}, a property of games
	forms, called RM, is given, which ensures that, if one only uses
	RM game forms in a graph, then for every reachability objective,
	Player $\mathsf{A} $ will always have an optimal strategy for that
	objective. This property is a characterization of well-behaved
	game forms regarding reachability objectives since every game form
	which is not RM can be embedded into a (small) graph game in such
	a way that Player $\mathsf{A} $ does not have an optimal strategy. This
	line of works really differs from the target of the current
	paper.
	

	

	

	

	
	\textbf{Structure of the paper.}  Section~\ref{sec:prelim}
	presents notations, Section~\ref{sec:gf} recalls the notion of game
	forms, Section~\ref{sec:games} introduces our formalism,
	Section~\ref{sec:conditions_subgame_optimal} exhibits a necessary and
	sufficient pair of conditions for subgame optimality,
	Section~\ref{sec:transfer} shows a memory transfer from subgame
	almost-surely winning to subgame optimal in concurrent games, and
	Section~\ref{sec:fair_strategies} adapts the results of the previous
	section to the case of the existence of a subgame finite-choice
	strategy.
	
	\ensuremath{\mathsf{s}}ection{Preliminaries}
	\label{sec:prelim}
	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 $n \in \ensuremath{\mathbb{N}}$, we denote by $Q^n$ (resp. $Q^{\leq
		n}$) the set of sequences of (resp. at most) $n$ elements of $Q$. For all $\rho
	= q_1 \cdots q_n \in Q^n$ and $i \leq n$, we denote by $\rho_i$ the element $q_i
	\in Q$ and by $\rho_{\leq i} \in Q^i$ the finite sequence $q_1 \cdots q_i$. 

	For a subset $S \ensuremath{\mathsf{s}}ubseteq Q$, we denote by $Q^* \cdot S^\omega \ensuremath{\mathsf{s}}ubseteq
	Q^\omega$ the set of infinite paths that eventually settle in $S$ and by $(Q^*
	\cdot S)^\omega \ensuremath{\mathsf{s}}ubseteq Q^\omega$ the set of infinite paths visiting
	infinitely often the set $S$.
	
	A \emph{discrete probability distribution} over a non-empty finite set $Q$ is a function $\mu: Q \rightarrow [0,1]$ such that $\ensuremath{\mathsf{s}}um_{x \in Q} \mu(x) = 1$. The	\emph{support} $\mathsf{Supp} (\mu)$ of a probability distribution $\mu: Q \rightarrow [0,1]$ is the	set of non-zeros of the distribution: $\mathsf{Supp} (\mu) = \{ q \in Q \mid \mu(q) \in
	(0,1] \}$. 

	The set of all distributions over 
	$Q$ is denoted $\mathcal{D} (Q)$.

	
	\ensuremath{\mathsf{s}}ection{Game forms}
	\label{sec:gf}
	

	We recall the definition of game forms -- 
	informally, bi-dimensional tables with variables -- and of games in normal
	forms -- game forms whose outcomes are values between $0$ and $1$.
	\begin{definition}[Game form and game in normal form]
		\label{def:arena_game_nf}
		A \emph{game form} (GF for short) is a tuple
		$\mathcal{F} = \langle \mathsf{Act}_\mathsf{A} ,\mathsf{Act}_\mathsf{B} ,\mathsf{O},\ensuremath{\mathsf{val}}rrho \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} $), $\mathsf{O}$
		is a non-empty set of outcomes, and
		$\ensuremath{\mathsf{val}}rrho: \mathsf{Act}_\mathsf{A}  \times \mathsf{Act}_\mathsf{B}  \rightarrow \mathsf{O}$ is a
		function that associates an outcome to each pair of
		actions. When the set of outcomes $\mathsf{O}$ is equal to
		$[0,1]$, we say that $\mathcal{F}$ is a \emph{game in normal
			form}. For a valuation $v \in [0,1]^\mathsf{O}$ of the
		outcomes, the notation $\gameNF{\mathcal{F}}{v}$ refers to the
		game in normal form
		$\langle \mathsf{Act}_\mathsf{A} ,\mathsf{Act}_\mathsf{B} ,[0,1],v \circ \ensuremath{\mathsf{val}}rrho \rangle$.
	\end{definition}

	We use 
	game forms to represent interactions between two
	players. The strategies available to Player $\mathsf{A} $ (resp. $\mathsf{B} $) are
	convex combinations of actions given as the rows
	(resp. columns) of the table. In a game in normal form, Player $\mathsf{A} $
	tries to maximize the outcome, whereas Player $\mathsf{B} $ tries to minimize
	it.
	\begin{definition}[Outcome of a game in normal form]
		\label{def:outcome_game_form}
		Consider a game in normal form
		$\mathcal{F} = \langle \mathsf{Act}_\mathsf{A} ,\mathsf{Act}_\mathsf{B} ,[0,1],\ensuremath{\mathsf{val}}rrho \rangle$. The
		set $\mathcal{D} (\mathsf{Act}_\mathsf{A} )$ (resp. $\mathcal{D} (\mathsf{Act}_\mathsf{B} )$) is the
		set of strategies available to Player $\mathsf{A} $
		(resp. $\mathsf{B} $). For a pair of strategies
		$(\ensuremath{\mathsf{s}}igma_\mathsf{A} ,\ensuremath{\mathsf{s}}igma_\mathsf{B} ) \in \mathcal{D} (\mathsf{Act}_\mathsf{A} ) \times
		\mathcal{D} (\mathsf{Act}_\mathsf{B} )$, the outcome
		$\ensuremath{\mathsf{out}}_\mathcal{F}(\ensuremath{\mathsf{s}}igma_\mathsf{A} ,\ensuremath{\mathsf{s}}igma_\mathsf{B} )$ in $\mathcal{F}$ of the
		strategies $(\ensuremath{\mathsf{s}}igma_\mathsf{A} ,\ensuremath{\mathsf{s}}igma_\mathsf{B} )$ is defined as:
		\begin{equation*}
			\ensuremath{\mathsf{out}}_\mathcal{F}(\ensuremath{\mathsf{s}}igma_\mathsf{A} ,\ensuremath{\mathsf{s}}igma_\mathsf{B} ) := \ensuremath{\mathsf{s}}um_{a \in \mathsf{Act}_\mathsf{A} }
			\ensuremath{\mathsf{s}}um_{b \in \mathsf{Act}_\mathsf{B} } \ensuremath{\mathsf{s}}igma_\mathsf{A} (a) \cdot \ensuremath{\mathsf{s}}igma_\mathsf{B} (b) \cdot
			\ensuremath{\mathsf{val}}rrho(a,b) \in [0,1]
		\end{equation*}
	\end{definition}	
	

	\begin{definition}[Value of a game in normal form and optimal strategies]
		\label{def:alternative_value_game_normal_form}
		Consider a game in normal form
		$\mathcal{F} = \langle \mathsf{Act}_\mathsf{A} ,\mathsf{Act}_\mathsf{B} ,[0,1],\ensuremath{\mathsf{val}}rrho \rangle$ and
		a
		strategy $\ensuremath{\mathsf{s}}igma_\mathsf{A}  \in \mathcal{D} (\mathsf{Act}_\mathsf{A} )$ for Player $\mathsf{A} $.  The
		\emph{value} of the strategy $\ensuremath{\mathsf{s}}igma_\mathsf{A} $, denoted
		$\ensuremath{\mathsf{val}}_\mathcal{F}(\ensuremath{\mathsf{s}}igma_\mathsf{A} )$ is equal to:
		$\ensuremath{\mathsf{val}}_\mathcal{F}(\ensuremath{\mathsf{s}}igma_\mathsf{A} ) := \inf_{\ensuremath{\mathsf{s}}igma_\mathsf{B}  \in \mathcal{D} (\mathsf{Act}_\mathsf{B} )}
		\ensuremath{\mathsf{out}}_{\mathcal{F}}(\ensuremath{\mathsf{s}}igma_\mathsf{A} ,\ensuremath{\mathsf{s}}igma_\mathsf{B} )$, and analogously for Player
		$\mathsf{B} $, with a $\ensuremath{\mathsf{s}}up$ instead of an $\inf$. When
		$\ensuremath{\mathsf{s}}up_{\ensuremath{\mathsf{s}}igma_\mathsf{A}  \in \mathcal{D} (\mathsf{Act}_\mathsf{A} )} \ensuremath{\mathsf{val}}_\mathcal{F}(\ensuremath{\mathsf{s}}igma_\mathsf{A} ) =
		\inf_{\ensuremath{\mathsf{s}}igma_\mathsf{B}  \in \mathcal{D} (\mathsf{Act}_\mathsf{B} )} \ensuremath{\mathsf{val}}_\mathcal{F}(\ensuremath{\mathsf{s}}igma_\mathsf{B} )$, it
		defines the \emph{value} of the game $\mathcal{F}$, denoted
		$\ensuremath{\mathsf{val}}_\mathcal{F}$.
		

		A strategy $\ensuremath{\mathsf{s}}igma_\mathsf{A}  \in \mathcal{D} (\mathsf{Act}_\mathsf{A} )$ ensuring
		$\ensuremath{\mathsf{val}}_\mathcal{F} = \ensuremath{\mathsf{val}}_\mathcal{F}(\ensuremath{\mathsf{s}}igma_\mathsf{A} )$ is called \emph{optimal}. The
		set of all optimal strategies for Player $\mathsf{A} $ is denoted
		$\ensuremath{\mathsf{Opt}}_\mathsf{A} (\mathcal{F}) \ensuremath{\mathsf{s}}ubseteq \mathcal{D} (\mathsf{Act}_\mathsf{A} )$, and analogously for
		Player $\mathsf{B} $. Von Neuman's minimax theorem~\cite{vonNeuman} ensures the
		existence of
		optimal strategies (for both players). 
	\end{definition}
	In the following, strategies in games in normal forms will be called
	$\mathsf{GF}$-strategies, in order not to confuse them with strategies in
	concurrent (graph) games.
	
	\ensuremath{\mathsf{s}}ection{Concurrent games and optimal strategies}
	\label{sec:games}
	\ensuremath{\mathsf{s}}ubsection{Concurrent arenas and strategies}
	We introduce the definition of concurrent arenas played on a finite graph.
	\begin{definition}[Finite stochastic concurrent arena]
		A \emph{colored concurrent arena} $\mathsf{A} conc$ is a tuple 
		$\mathsf{A} paramConc$ where $Q$ is the non-empty finite set of states, for all $q \in
		Q$, $A_q$ (resp. $B_q$) is the non-empty finite set of 
		actions available to Player $\mathsf{A} $ (resp. $\mathsf{B} $) at state $q$

		, $\mathsf{D} $ is the finite set of Nature states, $\delta: \bigcup_{q \in Q}
		(\{ q \} \times A_q \times B_q) \rightarrow \mathsf{D} $ is the
		transition function, $\mathsf{dist} : \mathsf{D}  \rightarrow \mathcal{D} (Q)$ is the
		distribution function. Furthermore, $\mathsf{K} $ is the non-empty finite set of
		colors and $\mathsf{col} : Q \rightarrow \mathsf{K} $ is the coloring function.

	\end{definition}
	
	In the following, the arena $\mathsf{A} conc$ will refer to the tuple $\mathsf{A} paramConc$,
	unless otherwise stated. A concurrent game is obtained from a concurrent arena
	by adding a winning condition: the set of infinite paths winning for Player $\mathsf{A} $
	(and losing for Player $\mathsf{B} $).
	\begin{definition}[Finite stochastic concurrent game]
		A finite \emph{concurrent game} 
		is 
		a pair $\mathcal{G} ames{\mathsf{A} conc}{W}$ where $\mathsf{A} conc$ is a finite concurrent colored arena
		and $W \ensuremath{\mathsf{s}}ubseteq \mathsf{K} ^\omega$ is Borel. The set $W$ is called the
		\emph{objective}, as it corresponds to the set of colored paths winning for
		Player $\mathsf{A} $.
	\end{definition}
	
	In this paper, we only consider a specific kind of objectives:
	prefix-independent ones. Informally, they correspond to objectives $W$ such that
	an infinite path $\rho$ is in $W$ if and only if 

	any of its suffixes is in $W$. More formally:
	\begin{definition}[Prefix-independent objectives]
		For a non-empty finite set of colors $\mathsf{K} $ and 
		$W \ensuremath{\mathsf{s}}ubseteq \mathsf{K} ^\omega$, 
		$W$ is said to be \emph{prefix-independent} (PI for short) if, for all $\rho
		\in \mathsf{K} ^\omega$ and $i \geq 0$, $\rho \in W \Leftrightarrow \rho_{\geq i}
		\in W$. 
	\end{definition}
	In the following, we refer to concurrent games with prefix-independent
	objectives as PI concurrent games. Our main results will be stated for arbitrary prefix-independent objectives, but we will apply them to specific objectives, namely parity, and relevant special cases Büchi and co-Büchi.	
	\begin{definition}[Parity, Büchi, co-Büchi objectives]
		\label{def:parity_buchi_cobuchi}
		Let $\mathsf{K}  \ensuremath{\mathsf{s}}ubset \ensuremath{\mathbb{N}}$ be a finite non-empty set of integers. Consider a
		concurrent arena $\mathsf{A} conc$ with $\mathsf{K} $ as set of colors. For an infinite path
		$\rho \in Q^\omega$, we denote by $\mathsf{col} (\rho)_\infty \ensuremath{\mathsf{s}}ubseteq \ensuremath{\mathbb{N}}$ the set
		of colors seen infinitely often in $\rho$: $\mathsf{col} (\rho)_\infty := \{ n \in \ensuremath{\mathbb{N}}
		\mid \forall i \in \ensuremath{\mathbb{N}},\; \exists j \geq i,\; \mathsf{col} (\rho_j) = n \}$. Then, the
		\emph{parity objective} w.r.t. $\mathsf{col} $ is the set
		$W^{\mathsf{Parity}}(\mathsf{col} ) := \{ \rho \in Q^\omega \mid \max
		\mathsf{col} (\rho)_\infty \text{ is even } \}$. The Büchi (resp. co-Büchi) objective
		correspond to the parity objective with $\mathsf{K}  := \{ 1,2 \}$ (resp. $\mathsf{K} 
		:= \{ 0,1 \}$).
	\end{definition}
	
	Strategies are then defined as functions that, given the history of the game
	(i.e. the sequence of states already seen) associate 

	a distribution on the actions available to the Player.
	\begin{definition}[Strategies]
		Consider a concurrent game $\mathsf{A} conc
		$. A strategy for Player $\mathsf{A} $  is a function $\ensuremath{\mathsf{s}}_\mathsf{A} : Q^+ \rightarrow \mathcal{D} (A)$
		with $A := \bigcup_{q \in Q} A_q$ such that, for all $\rho = q_0 \cdots q_n \in
		Q^+$, we have $\ensuremath{\mathsf{s}}_\mathsf{A} (\rho) \in \mathcal{D} (A_{q_n})$.		We denote by
		$\SetStrat{\mathsf{A} conc}{\mathsf{A} }$ the set of all strategies in arena $\mathsf{A} conc$ for Player
		$\mathsf{A} $. This is analogous for Player $\mathsf{B} $.

	\end{definition}
	
		
	We would like to define the outcome of the game given two strategies (one for
	each Player). First, we define the probability to go from a state $q$ to another
	state $q'$ given two $\mathsf{GF}$-strategies at a given state.

	\begin{definition}[Probability Transition]
		\label{def:mu_state}
		Consider a concurrent arena $\mathsf{A} conc
		$, a state $q \in Q$ and two strategies $(\ensuremath{\mathsf{s}}igma_\mathsf{A} ,\ensuremath{\mathsf{s}}igma_\mathsf{B} ) \in \mathcal{D} (A_q)
		\times \mathcal{D} (B_q)$
		. Consider another state $q' \in Q$. The probability to go from $q$ to $q'$ if
		the players plays, in q, $\ensuremath{\mathsf{s}}igma_\mathsf{A} $ and $\ensuremath{\mathsf{s}}igma_\mathsf{B} $, denoted
		$\prob{q,q'}{}{}(\ensuremath{\mathsf{s}}igma_\mathsf{A} ,\ensuremath{\mathsf{s}}igma_\mathsf{B} )$, is equal to:
		\begin{displaymath}
		\prob{q,q'}{}{}(\ensuremath{\mathsf{s}}igma_\mathsf{A} ,\ensuremath{\mathsf{s}}igma_\mathsf{B} ) = \ensuremath{\mathsf{s}}um_{a \in A_q} \ensuremath{\mathsf{s}}um_{b \in B_q}
		\ensuremath{\mathsf{s}}igma_\mathsf{A} (a) \cdot \ensuremath{\mathsf{s}}igma_\mathsf{B} (b) \cdot \mathsf{dist}  \circ \delta(q,a,b)(q')
		\end{displaymath}

	\end{definition}
	
	Let us now define the probability of occurrence of any finite path, and
	consequently of any Borel set, given two strategies.
	\begin{definition}[Probability distribution given two strategies]
		Let us consider a concurrent arena $\mathsf{A} conc
		$ and $\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B}  \in \SetStrat{\mathsf{A} conc}{\mathsf{A} } \times \SetStrat{\mathsf{A} conc}{\mathsf{B} }$ two
		arbitrary strategies for Player $\mathsf{A} $ and $\mathsf{B} $. We denote by
		$\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\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:
		\begin{displaymath}
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(\pi)[q] = \prob{\pi_n,q}{}{}(\ensuremath{\mathsf{s}}_\mathsf{A} (\pi),\ensuremath{\mathsf{s}}_\mathsf{B} (\pi))
		\end{displaymath}
		
		Then, the probability of occurrence of a finite path $\pi = \pi_0 \cdots \pi_n
		\in Q^+$ from a state $q_0 \in Q$ with the pair of strategies $(\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} )$ is
		equal to $\prob{\mathsf{A} conc,q_0}{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(\pi) = \Pi_{i = 0}^{n-1}
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(\pi_{\leq i})[\pi_{i+1}]$ if $\pi_0 = q_0$ and $0$
		otherwise. 

		The probability of a cylinder set $\ensuremath{\mathsf{Cyl}}(\pi)$ is
		$\prob{\mathsf{A} conc,q_0}{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }[\ensuremath{\mathsf{Cyl}}(\pi)] = \prob{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }{}(\pi)$ for any
		finite path $\pi \in Q^*$. This induces the probability of any Borel set in the
		usual way, 
		we denote by $\prob{\mathsf{A} conc,q_0}{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }: \mathsf{B} orel(Q) \rightarrow [0,1]$ the
		corresponding probability measure. Note that the set of infinite paths in
		$Q^\omega$ whose sequence of colors correspond to a Borel set $W \ensuremath{\mathsf{s}}ubseteq
		\mathsf{K} ^\omega$ is also a Borel set (as the preimage of a Borel set by a
		continuous function).
	\end{definition}
	

	Values of strategies and of the game follow and	are defined below.
	\begin{definition}[Value of strategies and of the game]
		Let $\mathcal{G} = \mathcal{G} ames{\mathsf{A} conc}{W}$ be a PI concurrent
		game 
		and consider a strategy $\ensuremath{\mathsf{s}}_\mathsf{A}  \in \SetStrat{\mathsf{A} conc}{\mathsf{A} }$
		for Player $\mathsf{A} $. The function
		$\MarVal{\mathcal{G} }[\ensuremath{\mathsf{s}}_\mathsf{A} ]: Q \rightarrow [0,1]$ giving the value
		of the strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $ is such that, for all $q_0 \in Q$,
		we have
		$\MarVal{\mathcal{G} }[\ensuremath{\mathsf{s}}_\mathsf{A} ](q_0) := \inf_{\ensuremath{\mathsf{s}}_\mathsf{B}  \in \SetStrat{\mathsf{A} conc}{\mathsf{B} }}
		\prob{\mathsf{A} conc,q_0}{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }[W]$. The function
		$\MarVal{\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
		$\MarVal{\mathcal{G} }[\mathsf{A} ](q_0) := \ensuremath{\mathsf{s}}up_{\ensuremath{\mathsf{s}}_\mathsf{A}  \in
			\SetStrat{\mathsf{A} conc}{\mathsf{A} }} \MarVal{\mathcal{G} }[\ensuremath{\mathsf{s}}_\mathsf{A} ](q_0)$. The
		function $\MarVal{\mathcal{G} }[\mathsf{B} ]: Q \rightarrow [0,1]$ giving the
		value of the game for Player $\mathsf{B} $ is defined similarly by
		reversing the supremum and infimum.
		
		By Martin's result on the determinacy of Blackwell games \cite{martin98}, for
		all concurrent games $\mathcal{G}  = \mathcal{G} ames{\mathsf{A} conc}{W}$, the value functions for both
		Players are equal, this defines the value function $\MarVal{\mathcal{G} }: Q \rightarrow
		[0,1]$ of the game: $\MarVal{\mathcal{G} } := \MarVal{\mathcal{G} }[\mathsf{A} ] = \MarVal{\mathcal{G} }[\mathsf{B} ]$.

		\label{def:determinacy}
	\end{definition}
	
	We define value areas: subsets of states 
	whose values are the same.
	\begin{definition}[Value area]
		In a PI concurrent game $\mathcal{G}
		$, 
		$V_\mathcal{G}$ refers to the set of values appearing in the game

		: $V_\mathcal{G} := \{ \MarVal{\mathcal{G} }[q] \mid q \in Q \}$. Furthermore, for all 

		$u \in V_\mathcal{G}$, $Q_u \ensuremath{\mathsf{s}}ubseteq Q$ refers to the set of states whose
		values are $u$ w.r.t. $\MarVal{\mathcal{G} }$: $Q_u := \{ q \in Q \mid \MarVal{\mathcal{G} }(q) = u
		\}$.
		\label{def:slice_of_game}
	\end{definition}
	
	In concurrent games, game forms appear at each state and describe the
	interactions of the players at that state. Furthermore, the valuation mapping
	each state to its value in the game can be lifted, via a convex combination,
	into a valuation of the Nature states. This, in turn, induces a natural way to
	define the game in normal form appearing at each state.
	\begin{definition}[Local interactions, Lifting valuations
		]
		In a PI concurrent game $\mathcal{G} $ where the valuation $\MarVal{\mathcal{G} }: Q \rightarrow
		[0,1]$ gives the values of the game, the lift $\LiftVal{\mathcal{G} }: \mathsf{D} 
		\rightarrow [0,1]$ is such that, for all 
		$d \in \mathsf{D} $, we have $\LiftVal{\mathcal{G} }(d) := \ensuremath{\mathsf{s}}um_{q \in Q} \MarVal{\mathcal{G} }(q)
		\cdot \mathsf{dist} (d)(q)$ (recall that $\mathsf{dist} : \mathsf{D}  \rightarrow
		\mathcal{D} (Q)$ is the distribution function).
		

		Let $q \in Q$. The \emph{local interaction} at state $q$ is the game form
		$\mathcal{F}_q = \langle A_q,B_q,\mathsf{D} ,\delta(q,\cdot,\cdot)
		\rangle$. 

		The game in normal form at state $q$ is then $\mathcal{F}^\mathsf{nf}_q :=
		\mathcal{G} ames{\mathcal{F}_q}{\LiftVal{\mathcal{G} }}$.
	\end{definition}
	

	

	
	Note that, the values of the game in normal form $\mathcal{F}^\mathsf{nf}_q$ 
	and of the state $q$ are equal.
	\begin{proposition}
		\label{prop:gnf}
		In a PI concurrent game $\mathcal{G} $, for all states $q \in Q$, we have
		$\MarVal{\mathcal{G} }(q) = \ensuremath{\mathsf{out}}_{\mathcal{F}^\mathsf{nf}_q}$.
	\end{proposition}
	

	
	\ensuremath{\mathsf{s}}ubsection{More on strategies}
	\label{subsec:definition_strategies}
	In this subsection, we define several kinds of strategies we will be
	interested in later on. Let us fix a PI concurrent game $\mathcal{G} $ for the rest of this section.

	First, we consider optimal strategies, i.e. strategies realizing the value of
	the game. We also consider positively-optimal strategies, i.e. strategies whose values are positive from all states where it is possible. This is defined formally below in Definition~\ref{def:positively_optimal_strat}.

	\begin{definition}[(Positively-) optimal strategies]
		\label{def:positively_optimal_strat}
		A Player $\mathsf{A} $ strategy $\ensuremath{\mathsf{s}}_\mathsf{A}  \in \SetStrat{\mathsf{A} conc}{\mathsf{A} }$ is (resp.
		\emph{positively}-)\emph{optimal} from a state $q \in Q$ if $\MarVal{\mathcal{G} }(q) =
		\MarVal{\mathcal{G} }[\ensuremath{\mathsf{s}}_\mathsf{A} ](q)$ (resp. if $\MarVal{\mathcal{G} }(q) > 0 \ensuremath{\mathbb{R}}ightarrow
		\MarVal{\mathcal{G} }[\ensuremath{\mathsf{s}}_\mathsf{A} ](q) > 0$). It is (resp. positively-)optimal if this 
		holds from all states $q \in Q$.

	\end{definition}
	Note that the definition of optimal strategies we consider is sometimes
	referred to as uniform optimality, as it holds from every state of the game. 

	However, it does not say anything about what happens once some sequence of
	states have been seen. We would like now to define a notion of strategy that is
	optimal from any point that can occur after any finite sequence of states has
	been seen. This correspond to subgame optimal strategies. To define them, we
	need to introduce 
	the notion of residual strategy.
	
	\begin{definition}[Residual and Subgame Optimal Strategies]
		Consider a Player $\mathsf{A} $ strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $. For all finite sequences $\rho \in Q^+$, the \emph{residual strategy}
		$\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho$ of a the strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $ 
		is the strategy $\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho: Q^+ \rightarrow \mathcal{D} (A)$ such that, for all $\pi \in Q^+$, we have $\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho(\pi) := \ensuremath{\mathsf{s}}_\mathsf{A} (\rho \cdot \pi)$.
		
		The Player $\mathsf{A} $ strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $ is \emph{subgame optimal} if, for all $\rho =	\rho' \cdot q \in Q^+$, the residual strategy $\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho$ is optimal from $q$, i.e. $\MarVal{\mathcal{G} }[\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho](q) = \MarVal{\mathcal{G} }(q)$.
	\end{definition}
	

	Note that, in particular, subgame optimal strategies are 
	optimal strategies. 

	When such strategies do exist, we want them to be as simple as possible, for
	instance we want them to be positional

	, that is that they only depend on the current state of the game.
	
	Furthermore, once a Player $\mathsf{A} $ strategy is fixed we obtain an (infinite)
	MDP. In such a context, $\ensuremath{\mathsf{val}}repsilon$-optimal strategies can
	be chosen among deterministic strategies (see for instance the
	explanation in~\cite[Thm. 1]{DBLP:journals/iandc/Chatterjee0GH15}) where deterministic strategies are such that, after any finite sequence of states, a specific action is played with probability 1. 
	Both of these notions are defined formally below in Definition~\ref{def:positional_deterministic_strategies}. 
	\begin{definition}[Positional, Deterministic strategies]
		\label{def:positional_deterministic_strategies}
		A Player $\mathsf{A} $ strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $ is \emph{positional} if, for all states $q \in Q$ and 
		paths $\rho \in Q^+$ we have $\ensuremath{\mathsf{s}}_\mathsf{A} (\rho \cdot q) = \ensuremath{\mathsf{s}}_\mathsf{A} (q)$. 
		
		A Player $\mathsf{B} $ strategy $\ensuremath{\mathsf{s}}_\mathsf{B} $ is \emph{deterministic} if, for all finite sequences $\rho \cdot q \in Q^+$, there exists $b \in B_q$ such that $\ensuremath{\mathsf{s}}_\mathsf{B} (\rho \cdot q)(b) = 1$.
	\end{definition}

	

	
	\ensuremath{\mathsf{s}}ection{Necessary and sufficient condition for subgame optimality}
	\label{sec:conditions_subgame_optimal}
	In this section, we present a necessary and sufficient pair of
	conditions for a Player $\mathsf{A} $ strategy to be subgame optimal, formally stated in
	Theorem~\ref{thm:subgame_optimal_arbitrary_strategy}. 

	The arguments given 
	here are somewhat similar to the ones given in Section 4 of
	\cite{BBSArXivICALP}, which deals with the same question restricted to
	positional strategies.
	

	The first 
	condition is local: it specifies how a strategy behaves in the
	games in normal form at each local interaction of the game. As mentioned in
	Proposition~\ref{prop:gnf}, at each state $q$, the value of the game in normal
	form $\mathcal{F}^\mathsf{nf}_q$ is equal to the value of the state $q$ (given by the valuation
	$\MarVal{\mathcal{G} } \in [0,1]^Q$). This suggests that, for all finite sequences of
	states $\rho \in Q^+$ 
	ending at that state $q$, the $\mathsf{GF}$-strategy $\ensuremath{\mathsf{s}}_\mathsf{A} (\rho)$ 

	needs to be optimal in the game in normal form $\mathcal{F}^\mathsf{nf}_q$ for the residual
	strategy $\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho$ to be optimal from $q$. Strategies with such a property
	are called locally optimal.

	This is 
	a necessary condition for subgame optimality. (However,

	it is neither a necessary nor a sufficient
	condition for optimality, as argued in Section~\ref{sec:transfer}

	.)
	\begin{definition}[Locally optimal strategies]
		Consider a PI concurrent game $\mathcal{G} $. 

		A Player $\mathsf{A} $ strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $ is locally optimal if, for all $\rho = \rho'
		\cdot q \in Q^+$, the $\mathsf{GF}$-strategy $\ensuremath{\mathsf{s}}_\mathsf{A} (\rho)$ is optimal in the game in
		normal form $\mathcal{F}^\mathsf{nf}_q$. That is -- recalling that $\LiftVal{\mathcal{G} } \in
		[0,1]^\mathsf{D} $ lifts the valuation $\MarVal{\mathcal{G} } \in [0,1]^Q$ to the Nature
		states -- for all $b \in B_q$: 
		\begin{displaymath}
		\MarVal{\mathcal{G} }(q) \leq \ensuremath{\mathsf{out}}_{\mathcal{F}^\mathsf{nf}_q}(\ensuremath{\mathsf{s}}_\mathsf{A} (\rho),b) = \ensuremath{\mathsf{s}}um_{a \in A_q} \ensuremath{\mathsf{s}}_\mathsf{A} (\rho)(a) \cdot \LiftVal{\mathcal{G} } \circ
		\delta(q,a,b)
		\end{displaymath}
		\label{def:locally_optimal}
	\end{definition}
	
	\begin{lemma}[Proof in
		Appendix~\ref{proof:prop_sub_game_opt_implies_locally_opt}]
		\label{prop:sub_game_opt_implies_locally_opt}
		In a PI concurrent game,

		subgame optimal strategies are locally optimal.
	\end{lemma}
	Note that this was already shown for positional strategies in
	\cite{BBSArXivICALP}.
	
	Local optimality does not ensure subgame optimality in general. However, it
	does ensure that, for all Player $\mathsf{B} $ deterministic strategies, the game
	almost-surely eventually settles in a value area, 

	i.e. in some $Q_u$ for some $u \in V_\mathcal{G} $.
	\begin{lemma}[Proof in Appendix~\ref{proof:lem_locally_opt_implies_same_value}]
		\label{lem:locally_opt_implies_same_value}
		Consider a PI concurrent game $\mathcal{G} 
		$ 

		and a Player $\mathsf{A} $ locally optimal strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $. For all Player $\mathsf{B} $
		deterministic strategies, almost surely the states seen infinitely often have
		the same value
		. That is: 
		\begin{displaymath}
			\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }[\bigcup_{u \in V_{\mathcal{G} }} Q^* \cdot
			(Q_u)^\omega] = 1
		\end{displaymath}
	\end{lemma}
	\begin{proof}[Sketch]
		First, if a state of value 1 is reached (i.e. a state in $Q_1$), then all
		states that can be seen with positive probability have value 1 (i.e. are in
		$Q_1$), since the strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $ is locally optimal. Let now $u \in V_{\mathcal{G} }$ be
		the highest value in $V_{\mathcal{G} }$ that is not 1 and consider the set of infinite
		paths such that the set $Q_u$ is seen infinitely often but the game does not
		settle in it, i.e. the set $(Q^* \cdot (Q \ensuremath{\mathsf{s}}etminus Q_u))^\omega \cap (Q^* \cdot
		Q_u)^\omega \ensuremath{\mathsf{s}}ubseteq Q^\omega$. Since the strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $ is locally optimal
		(and since $V_{\mathcal{G} }$ is finite), one can show that there is a positive
		probability $p > 0$ such that, the conditional probability of reaching $Q_1$
		knowing that $Q_u$ is left is at least $p$. 

		Hence, if $Q_u$ is left infinitely often, almost-surely the set $Q_1$ is seen

		(and never left). It follows that the probability of the event $(Q^* \cdot (Q
		\ensuremath{\mathsf{s}}etminus Q_u))^\omega \cap (Q^* \cdot Q_u)^\omega$ is 0. This implies that,
		almost-surely, if the set $Q_u$ is seen infinitely often, then at some point it
		is never left. The same arguments can then be used with the highest value in
		$V_{\mathcal{G} }$ that is less than $u$, etc. Overall, we obtain that, for all $u \in
		V_{\mathcal{G} }$, if a set $Q_u$ is seen infinitely often, it is eventually never left
		almost-surely. 
	\end{proof}
	
	Local optimality ensures that, at each step, the 
	expected values of the states reached 
	does not worsen (and may even improve if Player $\mathsf{B} $ does not play optimally). 

	By propagating this property, we obtain that, given a Player $\mathsf{A} $ locally
	optimal strategy and a Player $\mathsf{B} $ deterministic strategy, the convex
	combination of the values $u$ in $V_\mathcal{G} $ weighted by the probability of settling
	in the 
	value area $Q_u$, from a state $q$ is at least equal to its 
	value $\MarVal{\mathcal{G} }(q)$. 
	This is stated in Lemma~\ref{lem:locally_opt_implies_convex_comb} below.
	\begin{lemma}[Proof in
		Appendix~\ref{proof:lem_locally_opt_implies_convex_comb_ok}]
		\label{lem:locally_opt_implies_convex_comb}
		For a PI concurrent game $\mathcal{G} 
		$, 

		a Player $\mathsf{A} $ locally optimal strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $, a Player $\mathsf{B} $ deterministic
		strategy $\ensuremath{\mathsf{s}}_\mathsf{B} $ 
		and a state $q \in Q$: 

		\begin{displaymath}
			\MarVal{\mathcal{G} }(q) \leq \ensuremath{\mathsf{s}}um_{u \in V_{\mathcal{G} }} u \cdot
			\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }_q[Q^* \cdot (Q_u)^\omega]
		\end{displaymath}
	\end{lemma}
	Note that if Player $\mathsf{B} $ plays subgame optimally, 

	then this inequality is an equality.
	\begin{proof}[Sketch]
		First, let us denote $\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }_q$ by $\mathbb{P}$. 

		It can be shown by induction that, for all $i \in \ensuremath{\mathbb{N}}^*$, we have the property
		$\mathcal{P}(i): \MarVal{\mathcal{G} }(q) \leq \ensuremath{\mathsf{s}}um_{\pi \cdot q' \in q \cdot Q^i}
		\MarVal{\mathcal{G} }(q') \cdot \mathbb{P}(\pi \cdot q') =  \ensuremath{\mathsf{s}}um_{u \in V_\mathcal{G}  \ensuremath{\mathsf{s}}etminus \{
			0 \}} u \cdot \mathbb{P}[q \cdot Q^{i-1} \cdot Q_u]$. Furthermore, since by
		Lemma~\ref{lem:locally_opt_implies_same_value}, the game almost-surely settles
		in a value area, it can be shown that for $n$ large enough, the probability of
		being in $Q_u$ after $n$ steps (i.e. $\mathbb{P}[q \cdot Q^{n-1} \cdot Q_u]$) is
		arbitrarily close to the probability of eventually settling in $Q_u$ (i.e.
		$\mathbb{P}
		[Q^* \cdot (Q_u)^\omega]$). We can then apply $\mathcal{P}(n)$ to obtain the
		desired inequality.

	\end{proof}
	
	Recall that we are considering a pair of conditions to
	characterize that a strategy is subgame optimal. The first
	condition is local optimality. To summarize, we have seen that	
	the fact that a strategy is locally optimal ensures that, from
	any state $q$, the expected values of the value areas where the game settles 
	is at least $\MarVal{\mathcal{G} }(q)$. However, local
	optimality does not ensure anything as to the probability of
	$W$ given that the game settles in a specific value area, as
	witnessed in
	Appendix~\ref{appen:exemple_opt_loc_opt_not_sub_game_opt}. This
	is where the second condition comes into play. For the
	explanations regarding this condition, we will need
	Lemma~\ref{lem:chaterjee_value_0_1} below: a
	consequence of Levy's 0-1 Law.
	\begin{lemma}[See Appendix~\ref{appen:levy}]
		\label{lem:chaterjee_value_0_1}
		Let $\mathcal{M}$ be a countable Markov chain with a PI objective. If there is
		a $q \in Q$ such that $\MarVal{\mathcal{M}}(q) < 1$, then $\inf_{q' \in Q}
		\MarVal{\mathcal{M}}(q') = 0$.
	\end{lemma}
	Consider now 

	a Player $\mathsf{A} $ subgame optimal strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $ and a Player $\mathsf{B} $ deterministic
	strategy. Let us consider what happens if the game eventually settles in $Q_u$
	for some $u \in V_\mathcal{G}  \ensuremath{\mathsf{s}}etminus \{ 0 \}$. Assume towards a contradiction that
	there is a finite path after which the probability of $W$ given that the play
	eventually settles in $Q_u$ is less than 1. Then, there is a continuation of
	this path ending in $Q_u$ for which this probability of $W$ is less than $u$.
	Indeed, it was shown that, for a PI objective, in a countable Markov chain
	(which is what we obtain once strategies for both players are fixed), if there
	is a state with a value less than 1, then the infimum of the values in the
	Markov chain is 0 (this is what is stated in
	Lemma~\ref{lem:chaterjee_value_0_1}). Following our above
	towards-a-contradiction-assumption, there would be a finite path from which the
	Player $\mathsf{A} $ strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $ is not optimal. This is in contradiction with the
	fact that it is subgame optimal. Hence, a second necessary condition -- 

	in addition to the local optimality assumption -- for subgame optimality is:
	from all finite paths, for all Player $\mathsf{B} $ deterministic strategies, for all
	positive values $u \in V_{\mathcal{G} } \ensuremath{\mathsf{s}}etminus \{ 0 \}$, the probability of $W$ and
	eventually settling in $Q_u$ is equal to the probability of eventually settling
	in $Q_u$. We obtain the theorem below.
	

	
	\begin{theorem}[Proof in Appendix~\ref{proof:lem_optimal_arbitrary_strategy}]
		Consider a concurrent game $\mathcal{G} $ with a PI objective $W$ 

		and a Player $\mathsf{A} $ strategy $\ensuremath{\mathsf{s}}_\mathsf{A}  \in \SetStrat{\mathsf{A} conc}{\mathsf{A} }$. The strategy
		$\ensuremath{\mathsf{s}}_\mathsf{A} $ is subgame optimal if and only if:
		\begin{itemize}
			\item it is locally optimal;
			\item for all $\rho \in Q^+$, for all Player $\mathsf{B} $ deterministic strategies
			$\ensuremath{\mathsf{s}}_\mathsf{B} $, for all values $u \in V_\mathcal{G}  \ensuremath{\mathsf{s}}etminus \{ 0 \}$, we have
			$\mathbb{P}_\rho^{\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[W \cap Q^* \cdot (Q_u)^\omega] =
			\mathbb{P}_\rho^{\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[Q^* \cdot (Q_u)^\omega]$.
		\end{itemize}

		\label{thm:subgame_optimal_arbitrary_strategy}
	\end{theorem}
	\begin{proof}[Sketch]
		Lemma~\ref{prop:sub_game_opt_implies_locally_opt} states that local optimality
		is necessary and we have informally argued above why the second condition is
		also necessary for subgame optimality. As for the fact that they are sufficient
		conditions, this is a direct consequence of
		Lemmas~\ref{lem:locally_opt_implies_same_value}
		and~\ref{lem:locally_opt_implies_convex_comb} and the fact that deterministic
		strategies can achieve the same values as arbitrary strategies in MDPs (which we
		obtain once a Player $\mathsf{A} $ strategy is fixed), as cited in
		Subsection~\ref{subsec:definition_strategies}

		.
	\end{proof}
	

	One may ask what happens in the special case where the strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $
	considered is positional. 

	As mentioned above, such a characterization was already presented in
	\cite{BBSArXivICALP}\footnote{The proof was only presented for a
		specific class of objectives.

	}. Overall, we obtain a similar result except that the second condition is
	replaced by what happens in the game restricted to the End Components in the
	Markov Decision Process induced by the positional strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $. 

	
	\ensuremath{\mathsf{s}}ection{From subgame almost-surely winning to subgame optimality}
	\label{sec:transfer}
	
	\begin{figure}
\caption{A co-Büchi game.}
\label{fig:co_buchi_unfair}

\caption{A parity game.}
\label{fig:parity_unfair}
\end{figure}
	
	In \cite[Thm. 4.5]{GIH10}, the authors have proved a transfer result in PI
	turn-based games
	: the amount of memory sufficient to play optimally in every state of value 1
	of every game is also sufficient to play optimally in every game. 

	This result does not hold on concurrent games as is. First, although there are
	always optimal strategies in PI turn-based games (as proved in the same paper
	\cite[Thm. 4.3]{GIH10}), there are PI concurrent games without optimal
	strategies. 

	Second, infinite memory may be required to play optimally in co-Büchi
	concurrent games whereas almost-surely  winning strategies can be found among
	positional strategies in a turn-based setting. This can be seen in the game of
	Figure~\ref{fig:co_buchi_unfair} with $\mathsf{col} (q_0) = 0$ and $\mathsf{col} (q_1) =
	\mathsf{col} (q_1') = 1$. The green values in the local interaction at state $q_0$
	are the values of the game if they are reached (the game ends immediately). If a
	green value is not reached, the objective of Player $\mathsf{A} $ is to see only finitely
	often states $q_1$ and $q_1'$. It has already been argued in
	\cite{BBSArXivICALP} that the value of this game is $1/2$ and that there is an
	optimal strategy for Player $\mathsf{A} $ but it requires infinite memory. 

	To play optimally, Player $\mathsf{A} $ must play the top row with probability $1 -
	\ensuremath{\mathsf{val}}repsilon_k$ and the middle row with probability $\ensuremath{\mathsf{val}}repsilon_k$ for
	$\ensuremath{\mathsf{val}}repsilon_k > 0$ that goes (fast) to 0 when $k$ goes to $\infty$ (where $k$
	denotes the number of steps). The $\ensuremath{\mathsf{val}}repsilon_k$ must be chosen so that, if
	Player $\mathsf{B} $ always plays the left column with probability 1, then the state
	$q_1$ is seen finitely often with probability 1. Furthermore, as soon as the
	state $q_1'$ is visited, Player $\mathsf{A} $ switches to a positional strategy playing
	the bottom row with probability $\ensuremath{\mathsf{val}}repsilon_k'$ small enough (where $k$ denotes
	the number of steps before the state $q_1'$ was seen) and the two top rows with
	probability $(1 - \ensuremath{\mathsf{val}}repsilon_k')/2$. 
	
	Hence, the transfer of memory from almost-surely winning to
	optimal does not hold in concurrent games even if it is
	assumed that optimal strategies
	exist

	. However, one can note that although the strategy described
	above is 
	optimal, it is not subgame optimal. Indeed, when the strategy
	switches, the value of the residual strategy is
	$1/2 - \ensuremath{\mathsf{val}}repsilon_k' <
	1/2$. 

	In fact, there is no subgame optimal strategy in that
	game. Actually, if we assume that, not only optimal but
	subgame optimal strategies exist, then the transfer of memory
	will hold.

	
	The aim of this section is twofold: first, we identify a necessary and
	sufficient condition for the existence of subgame optimal
	strategies\footnote{Note that this is 
		different from what we did in the previous section: there, we established a
		necessary and sufficient condition for a specific strategy to be subgame
		optimal. Here, given a game, we consider necessary and sufficient conditions on
		the game for the existence of a subgame optimal strategy.}. Second, we establish
	the above-mentioned memory transfer that relates the amount of memory to play
	subgame optimally 
	and to be almost-surely winning. Before stating the main theorem of this
	section
	, let us first introduce the definition of positionally subgame almost-surely
	winnable objective, i.e. objectives for which subgame almost-surely winning
	strategies can be found among positional strategies.
	\begin{definition}[Positionally subgame almost-surely winnable objective]
		Consider a PI objective $W \ensuremath{\mathsf{s}}ubseteq \mathsf{K} ^\omega$. It is said to be a
		positionally subgame almost-surely winnable objective (\textsf{PSAW} for short)
		if the following holds: in all concurrent games $\mathcal{G}  = \mathcal{G} ames{\mathsf{A} conc}{W}$ where
		there is a subgame almost-surely winning strategy, there is a positional one. 
	\end{definition}
	

	

	

	

	\begin{theorem}
		Consider a non-empty finite set of colors $K$ and a PI objective $\emptyset
		\ensuremath{\mathsf{s}}ubsetneq W \ensuremath{\mathsf{s}}ubseteq \mathsf{K} ^\omega$. Consider a concurrent game $\mathcal{G} $ with
		objective $W$. Then, the three following assertions are equivalent:
		\begin{itemize}
			\item[a.] there exists a subgame optimal strategy;
			\item[b.] there exists an 
			optimal strategy that is locally optimal;
			\item[c.] there exists a 
			positively-optimal strategy that is locally optimal.
		\end{itemize}

		Furthermore, if this holds and if the objective $W$ is \textsf{PSAW}, then
		there exists a subgame optimal positional strategy.
		\label{thm:transfer_memory}
	\end{theorem}
	First, note that the equivalence is stated in terms of existence of strategies,
	not on the strategies themselves. In particular, any subgame optimal strategy is
	both 
	optimal and locally optimal, however, an 
	optimal strategy that is locally optimal is not necessarily a subgame optimal
	strategy. An example is provided in
	Appendix~\ref{appen:exemple_opt_loc_opt_not_sub_game_opt}. Second, it is
	straightforward that point \textit{a} implies point \textit{b} (from
	Theorem~\ref{thm:subgame_optimal_arbitrary_strategy}) and that point \textit{b}
	implies point \textit{c} (by definition of positively-optimal strategies). In
	the remainder of this section, we explain informally the constructions 

	leading to the proof of this theorem, i.e. to the proof that point \textit{c}
	implies point \textit{a}. The transfer of memory 
	is a direct consequence of the way this theorem is proven. The
	full proof is given in Appendix
	~\ref{proof:thm_transfer_almost_sure_optimal}. We fix a PI concurrent game
	$\mathcal{G}  = \mathcal{G} ames{\mathsf{A} conc}{W}$ for the rest of the section.

	
	The idea is as follows. As stated in
	Theorem~\ref{thm:subgame_optimal_arbitrary_strategy}, subgame optimal strategies
	are locally optimal and win the game almost-surely if the game settles in a
	value area $Q_u$ for some positive $u \in V_{\mathcal{G} } \ensuremath{\mathsf{s}}etminus \{ 0 \}$. Our idea is
	therefore to consider subgame almost-surely winning strategies in the derived
	game $\mathcal{G} _u$: a \textquotedblleft restriction\textquotedblright \ of the game
	$\mathcal{G} $ to $Q_u$ (more details will be given later). We can 
	then glue together these subgame almost-surely winning strategies -- defined
	for all $u \in V_{\mathcal{G} } \ensuremath{\mathsf{s}}etminus \{ 0 \}$ -- 
	into a subgame optimal strategy.

	However, there are some issues:
	\begin{enumerate}
		\item the state values in the game $\mathcal{G} _u$ should be all equal to 1;
		\item furthermore, there must exist a subgame almost-surely winning strategy
		in $\mathcal{G} _u$;
		\item this subgame almost-surely winning strategy in $\mathcal{G} _u$ should be locally
		optimal when considered in the whole game $\mathcal{G} $.
	\end{enumerate}

	Note that the method we use here is different from what the authors of
	\cite{GIH10} did to prove the transfer of memory in turn-based
	games

	. 
	
	Let us first deal with issue {\bfseries\ensuremath{\mathsf{s}}ffamily
		\color{darkgray} 3}. One can ensure that the almost-surely winning strategies
	in the game $\mathcal{G} _u$ are all locally optimal in $\mathcal{G} $ by properly defining the game
	$\mathcal{G} _u$. More specifically, 
	this is done by enforcing that the only Player $\mathsf{A} $ possible strategies in
	$\mathcal{G} _u$ are locally optimal in the game $\mathcal{G} $. To do so, we construct the game
	$\mathcal{G} _u$ whose state space is $Q_u$ 

	(plus gadget states) but whose set of actions $A_{\mathcal{F}^\mathsf{nf}_q}$, at a state $q \in
	Q_u$, is such that the set of strategies $\mathcal{D} (A_{\mathcal{F}^\mathsf{nf}_q})$ corresponds
	exactly to the set of optimal strategies in the original game in normal form
	$\mathcal{F}^\mathsf{nf}_q$, while keeping the set of actions $A_{\mathcal{F}^\mathsf{nf}_q}$ for Player $\mathsf{A} $
	finite. This is possible thanks to
	Proposition~\ref{prop:finite_set_optimal_start_gnf} below: in every game in
	normal form $\mathcal{F}^\mathsf{nf}_q$ at state $q \in Q_u$, there exists a finite set
	$A_{\mathcal{F}^\mathsf{nf}_q}$ of optimal strategies such that the optimal strategies in
	$\mathcal{F}^\mathsf{nf}_q$ are exactly the convex combinations of strategies in $A_{\mathcal{F}^\mathsf{nf}_q}$.
	This is a well known result, argued for instance in \cite{shapley1950basic}.	

	\begin{proposition}
		\label{prop:finite_set_optimal_start_gnf}
		Consider a game in normal form $\mathcal{F}^\mathsf{nf} = \langle \mathsf{Act}_\mathsf{A} ,\mathsf{Act}_\mathsf{B} ,[0,1],\delta \rangle$
		with $|\mathsf{Act}_\mathsf{A} | = n$ and $|\mathsf{Act}_\mathsf{B} | = k$. There exists a set $A_{\mathcal{F}^\mathsf{nf}} \ensuremath{\mathsf{s}}ubseteq
		\ensuremath{\mathsf{Opt}}_\mathsf{A} (\mathcal{F}^\mathsf{nf})$ of optimal strategies such that $|A_{\mathcal{F}^\mathsf{nf}}| \leq n+k$ and
		$\mathcal{D} (A_{\mathcal{F}^\mathsf{nf}}) = \ensuremath{\mathsf{Opt}}_\mathsf{A} (\mathcal{F}^\mathsf{nf})$.

	\end{proposition}
	\begin{proof}[Sketch]
		One can write a system of $n+k$ inequalities (with some
		additional equalities) whose set of solutions is exactly the
		set of optimal $\mathsf{GF}$-strategies $\ensuremath{\mathsf{Opt}}_\mathsf{A} (\mathcal{F}^\mathsf{nf})$.

		The result then follows from standard system of inequalities
		arguments as the space of solutions is in fact a polytope
		with at most $n+k$ vertices.
	\end{proof}
	
	We illustrate this construction: a part of a concurrent game
	is depicted in Figure \ref{fig:local_optimal_necessary} and
	the change of the interaction of the players at state $q_0$ is
	depicted in Figures~\ref{fig:FormOriginal},~\ref{fig:FormOriginalValued},~\ref{fig:FormOriginalValuedOnlyOpt} and~\ref{fig:FormOnlyOpt}.
	\begin{figure}
\caption{A concurrent game with $A_{q_0}
\label{fig:local_optimal_necessary}

\caption{The local interaction $\mathcal{F}
\label{fig:FormOriginal}

\caption{The game in normal form $\mathcal{F}
\label{fig:FormOriginalValued}

\caption{The game $\mathcal{F}
\label{fig:FormOriginalValuedOnlyOpt}

\caption{The game form $\mathcal{F}
\label{fig:FormOnlyOpt}
\end{figure}
	
	The game $\mathcal{G} _u$ has the same objective $W$ as the game 

	$\mathcal{G} $.

	Since we want all the states to have value 1 in $\mathcal{G} _u$ (recall issue
	{\bfseries\ensuremath{\mathsf{s}}ffamily
		\color{darkgray} 1}),

	we will build the game $\mathcal{G} _u$ such that any edge leading to a state not in
	$Q_u$ in $\mathcal{G} $ now leads to a PI concurrent game $\mathcal{G} _W$ (with the same objective
	$W$) where all states have value~1. 

	The game $\mathcal{G} _W$ is (for instance) a clique with all colors in $\mathsf{K} $ where
	Player $\mathsf{A} $ plays alone. The formal definitions of the game $\mathcal{G} _W =
	\mathcal{G} ames{\mathsf{A} conc_W}{W}$ and of the game $\mathcal{G} _u$ can be found in
	Appendix~\ref{subsec:game_value_one_everywhere}. 

	
	An illustration of this construction can be found in
	Figures~\ref{fig:decompositionGame1} and~\ref{fig:decompositionGame2}. The blue
	dotted arrows are the ones that need to be redirected when the game is changed.
	\begin{figure}
\caption{The depiction of a PI concurrent game with its value areas.}
\label{fig:decompositionGame1}

\caption{The PI concurrent game after the modifications described above.}
\label{fig:decompositionGame2}
\end{figure}

	With such a definition, we have made some progress w.r.t. the issue
	{\bfseries\ensuremath{\mathsf{s}}ffamily
		\color{darkgray} 1} cited previously (regarding the values being equal to 1):

	the values of all states of the game $\mathcal{G} _u$ are positive (for positive $u$).
	\begin{lemma}[Proof in Appendix~\ref{proof:lem_value_one_Gu}]
		Consider the game $\mathcal{G} _u$ for some positive $u \in V_{\mathcal{G} } \ensuremath{\mathsf{s}}etminus \{ 0 \}$
		and assume that, in $\mathcal{G} $, there exists a 
		positively-optimal strategy that is locally optimal. 

		Then, for all states $q$ in $\mathcal{G} _u$, the value of the state $q$ in $\mathcal{G} _u$ is
		positive: $\MarVal{\mathcal{G} _u}(q) > 0$.
		\label{lem:value_one_Gu}
	\end{lemma}
	\begin{proof}[Sketch]
		Consider a state $q \in Q_u$ and a Player $\mathsf{A} $ locally optimal strategy
		$\ensuremath{\mathsf{s}}_\mathsf{A} $ in $\mathcal{G} $ that is positively-optimal from $q$

		. Then, the strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $ (restricted to $Q_u^+$) can be seen as a strategy
		in $\mathcal{G} _u$ (it has to be defined in $\mathcal{G} _W$, but this can done straightforwardly).
		Note that this is only possible because the strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $ is locally optimal
		(due to the definition of $\mathcal{G} _u$). 

		For a Player $\mathsf{B} $ strategy $\ensuremath{\mathsf{s}}_\mathsf{B} $ in $\mathcal{G} _u$, consider what happens with
		strategies $\ensuremath{\mathsf{s}}_\mathsf{A} $ and $\ensuremath{\mathsf{s}}_\mathsf{B} $ in both games $\mathcal{G} _u$ and $\mathcal{G} $. Either the game
		stays indefinitely in $Q_u$, and what happens in $\mathcal{G} _u$ and $\mathcal{G} $ is identical.
		Or it eventually leaves $Q_u$, leading to states of value 1 in $\mathcal{G} _u$. Hence,
		the value of the game $\mathcal{G} _u$ from $q$ with strategies $\ensuremath{\mathsf{s}}_\mathsf{A} $ and $\ensuremath{\mathsf{s}}_\mathsf{B} $ is at
		least the value of the game $\mathcal{G} $ from $q$ with the same strategies. Thus, the
		value of the state $q$ is positive in $\mathcal{G} _u$.

	\end{proof}

	
	As it turns out, Lemma~\ref{lem:value_one_Gu} suffices 
	to deal with both 
	issues {\bfseries\ensuremath{\mathsf{s}}ffamily \color{darkgray} 1} and
	{\bfseries\ensuremath{\mathsf{s}}ffamily \color{darkgray} 2} at the same
	time. Indeed, as stated in
	Theorem~\ref{thm:all_not_zero_implies_almost_sure} below, it
	is a general result that in a PI concurrent game, if all
	states have positive values, then all states have value 1 and
	there is a subgame almost-surely winning strategy.

	\begin{theorem}[Proof in
		Appendix~\ref{proof:thm_all_not_zero_implies_almost_sure}]
		\label{thm:all_not_zero_implies_almost_sure}
		Consider a PI concurrent game $\mathcal{G} $ and assume that all state values are
		greater than or equal to 
		$c > 0$, i.e. for all $q \in Q$, $\MarVal{\mathcal{G} }(q) \geq c$. Then, there is a
		subgame almost-surely winning strategy in $\mathcal{G} $.
	\end{theorem}
	\begin{remark}
		This theorem can be seen as a strengthening of Theorem
		1 from \cite{CH07}. Indeed, this Theorem 1 states that
		if all states have positive values, then they all have
		value 1 (this is then generalized to games with
		countably-many states). Theorem~\ref{thm:all_not_zero_implies_almost_sure}
		is stronger since it ensures the existence of
		(subgame) almost-surely winning strategies. Although a
		detailed proof is provided in
		Appendix~\ref{proof:thm_all_not_zero_implies_almost_sure},
		note that this theorem was already stated and proven
		in \cite{GIH10} in the context of PI turn-based
		games. Nevertheless their arguments could have been
		used \textit{verbatim} for concurrent games as well.

		In the Appendix, we give a proof using the same
		construction (namely, reset strategies) but we argue
		differently 
		why the construction proves the theorem.
	\end{remark}
	

	We can now glue together pieces of strategies $\ensuremath{\mathsf{s}}_\mathsf{A} ^u$ defined in all games
	$\mathcal{G} _u$ into a single strategy $\ensuremath{\mathsf{s}}_\mathsf{A} [(\ensuremath{\mathsf{s}}_\mathsf{A} ^u)_{u \in V_{\mathcal{G} } \ensuremath{\mathsf{s}}etminus \{ 0
		\}}]$. Informally, the glued strategy mimics the strategy on $Q_u^+$ and
	switches strategy when a value area is left and another one is reached.
	\begin{definition}[Gluing strategies]
		Consider a PI concurrent game $\mathcal{G} $ 
		and for all values $u \in V_{\mathcal{G} } \ensuremath{\mathsf{s}}etminus \{ 0 \}$, a strategy $\ensuremath{\mathsf{s}}_\mathsf{A} ^u$ in
		the game $\mathcal{G} _u$. Then, we glue these strategies into the strategy
		$\ensuremath{\mathsf{s}}_\mathsf{A} [(\ensuremath{\mathsf{s}}_\mathsf{A} ^u)_{u \in V_{\mathcal{G} } \ensuremath{\mathsf{s}}etminus \{ 0 \}}]: Q^+ \rightarrow \mathcal{D} (A)$
		simply written $\ensuremath{\mathsf{s}}_\mathsf{A} $ such that, for all $\rho$ ending at state $q \in Q$:
		\begin{displaymath}
		\ensuremath{\mathsf{s}}_\mathsf{A} (\rho) := 
		\begin{cases}
		\ensuremath{\mathsf{s}}_\mathsf{A} ^u(\pi) & \text{ if } u = \MarVal{\mathcal{G} }(q) > 0 \text{ for } \pi \text{ the
			longest suffix of } \rho \text{ in } Q_u^+ \\ 

		\text{is arbitrary } & \text{ if } \MarVal{\mathcal{G} }(q) = 0\\
		\end{cases}
		\end{displaymath}
		\label{def:glued_strat}
	\end{definition}
	As stated in Lemma~\ref{prop:glued_strategy} below, the construction described
	in Definition~\ref{def:glued_strat} transfers almost-surely winning strategies
	in $\mathcal{G} _u$ into a subgame optimal strategy in $\mathcal{G} $.

	\begin{lemma}[Proof in Appendix~\ref{proof:prop_glued_strategy}]
		\label{prop:glued_strategy}

		For all $u \in V_{\mathcal{G} } \ensuremath{\mathsf{s}}etminus \{ 0 \}$, let $\ensuremath{\mathsf{s}}_\mathsf{A} ^u$ be a subgame
		almost-surely winning strategy in $\mathcal{G} _u$. 

		The glued strategy $\ensuremath{\mathsf{s}}_\mathsf{A} [(\ensuremath{\mathsf{s}}_\mathsf{A} ^u)_{u \in V_\mathcal{G}  \ensuremath{\mathsf{s}}etminus \{ 0 \}}]$, denoted
		$\ensuremath{\mathsf{s}}_\mathsf{A} $, is subgame optimal in $\mathcal{G} $.
	\end{lemma}
	\begin{proof}[Sketch]
		We apply Theorem~\ref{thm:subgame_optimal_arbitrary_strategy}. First, the
		strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $ is locally optimal in all $Q_u$ for $u > 0$ by the strategy
		restriction done to define the game $\mathcal{G} _u$ (only optimal strategies are
		considered at each game in normal form $\mathcal{F}^\mathsf{nf}_q$ at states $q \in Q_u$

		). Furthermore, any strategy is optimal in a game in normal form of value 0
		(which is the case of the game in normal forms of states in $Q_0$). 

		Second, if the game eventually settles in a value area $Q_u$ for some $u > 0$,
		from then on the strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $ mimics the strategy $\ensuremath{\mathsf{s}}_\mathsf{A} ^u$, which is
		subgame almost-surely winning in $\mathcal{G} _u$. Hence, the probability of $W$ given
		that the game eventually settles in $Q_u$ is 1. This holds for all $u \in V_{\mathcal{G} }
		\ensuremath{\mathsf{s}}etminus \{ 0 \}$, so the second condition of
		Theorem~\ref{thm:subgame_optimal_arbitrary_strategy} holds.
	\end{proof}
	
	We now have all the ingredients to prove Theorem~\ref{thm:transfer_memory}. 
	\begin{proof}[Of Theorem~\ref{thm:transfer_memory}]
		We consider the PI concurrent game $\mathcal{G} $ and assume that there is a 
		positively-optimal strategy that is locally optimal. Then, by
		Lemma~\ref{lem:value_one_Gu}, for all positive values $u \in V_{\mathcal{G} } \ensuremath{\mathsf{s}}etminus \{
		0 \}$, all states in $\mathcal{G} _u$ have positive values. It follows, by
		Theorem~\ref{thm:all_not_zero_implies_almost_sure}, that there exists a subgame
		almost-surely winning strategy in every game $\mathcal{G} _u$ for $u \in V_{\mathcal{G} } \ensuremath{\mathsf{s}}etminus
		\{ 0 \}$. We then obtain a subgame optimal strategy by gluing these strategies
		together, 
		given by Lemma~\ref{prop:glued_strategy}.
		
		The second part of the theorem, dealing with transfer of positionality from
		subgame almost-surely winning to subgame optimal follows from the fact that if
		all strategies $\ensuremath{\mathsf{s}}_\mathsf{A} ^u$ are positional for all $u \in V_{\mathcal{G} } \ensuremath{\mathsf{s}}etminus \{ 0
		\}$, then so is the glued strategy $\ensuremath{\mathsf{s}}_\mathsf{A} [(\ensuremath{\mathsf{s}}_\mathsf{A} ^u)_{u \in V_{\mathcal{G} } \ensuremath{\mathsf{s}}etminus \{ 0
			\}}]$. 		

	\end{proof}

	
	We now apply the result of Theorem~\ref{thm:transfer_memory}
	to two specific classes of objectives: Büchi and co-Büchi
	objectives. Note that this result is already known for
	Büchi objectives, proven in \cite{BBSArXivICALP}.
	\begin{corollary}
		\label{coro:application_buchi_cobuchi}
		Consider a concurrent game with a Büchi (resp. co-Büchi)
		objective and assume that there is a 
		positively-optimal strategy that is locally optimal. Then there is a subgame
		optimal
		positional strategy.
	\end{corollary}
	Note that it is also possible to prove a memory transfer from
	subgame almost-surely winning to subgame optimal for an
	arbitrary memory skeleton, instead of only positional
	strategies. This adds only a few minor difficulties. This is
	dealt with in Appendix~\ref{appen:extension_finite_memory}.
	

	
	

	

	

	
	\textbf{Application to the turn-based setting.}
	The aim of Section~\ref{sec:transfer} was to extend an already existing result
	on turn-based games in the context of concurrent games. This required an
	adaptation of the assumptions. However, it is in fact possible to retrieve the
	original result on turn-based games from Theorem~\ref{thm:transfer_memory} in a
	fairly straightforward manner. It amounts to show that, in all finite turn-based
	games $\mathcal{G} $, for all values $u \in V_{\mathcal{G} } \ensuremath{\mathsf{s}}etminus \{ 0 \}$, there is a locally
	optimal strategy that is positively-optimal from all states in $Q_u$. This is
	done in Appendix~\ref{appen:retrieve_result_turn_based}. 

	

	\ensuremath{\mathsf{s}}ection{Finite-choice strategies}
	\label{sec:fair_strategies}
	

	

	
	In this section, we introduce a new kind of strategies, namely finite-choice
	strategies. Let us first motivate why we consider such strategies. Consider
	again the co-Büchi game of Figure~\ref{fig:co_buchi_unfair}. Recall that the
	optimal strategy we described first plays the top row with increasing
	probability and the middle row with decreasing probability and then, once Player
	$\mathsf{B} $ plays the second column, switches to a positional strategy playing the
	bottom row with positive, yet small enough probability. Note that switching
	strategy is essential. Indeed, if Player $\mathsf{A} $ does not switch

	, Player $\mathsf{B} $ could at some point opt for the middle column and see
	indefinitely the state $q_1'$ with very high probability

	. In fact, what happens in that case is rather counter-intuitive: once Player
	$\mathsf{B} $ switches, there is infinitely often a positive probability to reach the
	outcome of value 1. However, the probability to ever reaching this outcome can
	be arbitrarily small, if Player $\mathsf{B} $ waits long enough before playing the middle
	row. This happens because the probability $\ensuremath{\mathsf{val}}repsilon_k$ to visit that outcome
	goes (fast) to 0 when $k$ goes to $\infty$. In fact, such an optimal strategy
	has \textquotedblleft infinite choice\textquotedblright \ in the sense that it
	may prescribe 
	infinitely many different 
	probability distribution. 
	
	In this section, we consider \emph{finite-choice strategies}, i.e. strategies
	that can use only finitely many 
	$\mathsf{GF}$-strategies at each state.
	

	\begin{definition}[Finite-choice strategy]
		\label{def:finite_choice_strategies}
		Let $\mathcal{G} $ be a concurrent game. A Player $\mathsf{A} $ strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $ in $\mathcal{G} $ has
		\emph{finite choice} if, for all $q \in Q$, the set $S^{\ensuremath{\mathsf{s}}_\mathsf{A} }_q := \{ 
		\ensuremath{\mathsf{s}}_\mathsf{A} (\rho \cdot q) \mid \rho \in Q^+ \} \ensuremath{\mathsf{s}}ubseteq \mathcal{D} (A_q)$ 

		is finite.

	\end{definition}
	Note that positional (even finite-memory) and deterministic strategies are
	examples of finite-choice strategies.
	
	Interestingly, we can link finite-choice strategies with the existence of
	subgame optimal strategies. In general it does not hold that if there are

	optimal strategies, then there exists subgame optimal strategies (as
	exemplified in the game of Figure~\ref{fig:co_buchi_unfair}). However, in
	Theorem~\ref{thm:fair_strategy_uniformly_optimal} below, we state that if we
	additionally assume that the 
	optimal strategy considered has finite choice, then there is a
	subgame optimal strategy (that has also finite choice).

	\begin{theorem}[Proof in
		Appendix~\ref{proof:thm_fair_strategy_uniformly_optimal}]
		\label{thm:fair_strategy_uniformly_optimal}
		Consider a PI concurrent game $\mathcal{G} $. If there is a finite-choice 
		optimal strategy, 
		then there is a finite-choice subgame optimal
		strategy. 

	\end{theorem}
	\begin{proof}[Sketch]
		Consider such an 
		optimal finite-choice strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $. In particular, note that there is a
		constant $c > 0$ such that for all $\rho \cdot q \in Q^+$, for all $a \in A_q$
		we have: $\ensuremath{\mathsf{s}}_\mathsf{A} (\rho \cdot q)(q) > 0 \ensuremath{\mathbb{R}}ightarrow \ensuremath{\mathsf{s}}_\mathsf{A} (\rho \cdot q)(q) \geq c$.
		We build a subgame optimal strategy $\ensuremath{\mathsf{s}}_\mathsf{A} '$ in the following way: for all $\rho
		= \rho' \cdot q \in Q^+$, if the residual strategy $\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho$ is optimal, then
		$\ensuremath{\mathsf{s}}_\mathsf{A} '(\rho) := \ensuremath{\mathsf{s}}_\mathsf{A} (\rho)$, otherwise $\ensuremath{\mathsf{s}}_\mathsf{A} '(\rho) := \ensuremath{\mathsf{s}}_\mathsf{A} (q)$ (i.e. we
		reset the strategy). Straightforwardly, the strategy $\ensuremath{\mathsf{s}}_\mathsf{A} '$ has finite choice.
		We want to apply Theorem~\ref{thm:subgame_optimal_arbitrary_strategy} to prove
		that it is subgame optimal. One can see that it is locally optimal (by the
		criterion chosen for resetting the strategy). Consider now some $\rho \in Q^+$
		ending at state $q \in Q$ and another state $q' \in Q$. Assume that the residual
		strategy $\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho$ is optimal but that the residual strategy $\ensuremath{\mathsf{s}}_\mathsf{A} ^{\rho
			\cdot q'}$ is not. Then, similarly to why local optimality is necessary for
		subgame optimality (see
		Proposition~\ref{prop:sub_game_opt_implies_locally_opt}), 

		one can show that any Player $\mathsf{B} $ action $b \in B_q$ leading to $q'$ from $\rho$ with
		positive probability is such that $\MarVal{\mathcal{G} }(q) <
		\ensuremath{\mathsf{out}}_{\mathcal{F}^\mathsf{nf}_q}(\ensuremath{\mathsf{s}}_\mathsf{A} (\rho),b)$. Hence, there is positive probability from
		$\rho$, if Player $\mathsf{B} $ opts for the action $b$, to reach a state of value
		different from $u = \MarVal{\mathcal{G} }(q)$. And if this happens infinitely often, 

		a state of value different from $u$ will be reached
		almost-surely\footnote{This holds because the strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $ has finite
			choice: the probability to see a state of different value is bounded below by
			the product of $c$ and the smallest positive probability among all Nature
			states.}. In other words, if a value area is never left, almost-surely, the
		strategy $\ensuremath{\mathsf{s}}_\mathsf{A} '$ only resets finitely often.
		
		Consider now some $\rho \in Q^+$, a Player $\mathsf{B} $ deterministic strategy $\ensuremath{\mathsf{s}}_\mathsf{B} $
		and a value $u \in V_\mathcal{G}  \ensuremath{\mathsf{s}}etminus \{ 0 \}$. From what we argued above, the
		probability of the event $Q^* \cdot (Q_u)^\omega$ (resp. $W \cap Q^* \cdot
		(Q_u)^\omega$) is the same if we intersect it with the fact that the strategy
		$\ensuremath{\mathsf{s}}_\mathsf{A} '$ only resets finitely often. Furthermore, if the strategy does not reset
		anymore from some point on, and all states have the same value $u > 0$, then it
		follows that the probability of $W$ is 1 (since $W$ is PI). We can then conclude
		by applying Theorem~\ref{thm:subgame_optimal_arbitrary_strategy}.
	\end{proof}
	
	Finite-choice strategies are interesting for another reason. In the previous
	section, we applied the memory transfer from Theorem~\ref{thm:transfer_memory}
	to the Büchi and co-Büchi objectives. We did not apply it to other objectives --
	in particular to the parity objective. Indeed, in general, contrary to the case
	of turn-based games, infinite-memory is necessary to be almost-surely winning in
	parity games. This happens in Figure~\ref{fig:parity_unfair} (already described
	in \cite{AH00}) where the objective of Player $\mathsf{A} $ is to see $q_1$ infinitely
	often, while seeing $q_2$ only finitely often. Let us describe a Player $\mathsf{A} $
	subgame almost-surely winning strategy. 

	The top row is played with probability $1 - \ensuremath{\mathsf{val}}repsilon_k$ and the bottom row
	is played with probability $\ensuremath{\mathsf{val}}repsilon_k > 0$ with $\ensuremath{\mathsf{val}}repsilon_k$ going to 0
	when $k$ goes to $\infty$ (the ($\ensuremath{\mathsf{val}}repsilon_k$) used in the game in
	Figure~\ref{fig:co_buchi_unfair} works here as well) where $k$ denotes the
	number of times the state $q_0$ is seen. Such a strategy is subgame
	almost-surely winning and does not have finite choice. In fact, it can be shown
	that all Player $\mathsf{A} $ finite-choice strategies have value 0 in that game. 
	
	Interestingly, the transfer of memory of Theorem~\ref{thm:transfer_memory} is
	adapted in Theorem~\ref{thm:transfer_memory_finite_choice} with the memory that
	is sufficient in turn-based games -- for those PI objectives that have a
	\textquotedblleft neutral color\textquotedblright 
	-- if we additionally assume that the subgame optimal strategy considered has
	finite choice. First, let us define what is meant by 
	\textquotedblleft neutral color\textquotedblright
	, then we define the turn-based version of \textsf{PSAW}.

	\begin{definition}[Objective with a neutral color]
		Consider a set of colors $\mathsf{K} $ and a PI objective $W \ensuremath{\mathsf{s}}ubseteq
		\mathsf{K} ^\omega$. It has a \emph{neutral color} if there is some (neutral) color
		$k \in \mathsf{K} $ such that, for all $\rho = \rho_0 \cdot \rho_1 \cdots \in
		\mathsf{K} ^\omega$, we have $\rho \in W \Leftrightarrow \rho_0 \cdot k \cdot \rho_1
		\cdot k \cdots \in W$. 

	\end{definition}

	
	\begin{definition}[\textsf{PASW} objective in turn-based games]
		Consider a PI objective $W \ensuremath{\mathsf{s}}ubseteq \mathsf{K} ^\omega$. It is \emph{positionally
			subgame almost-surely winnable in turn-based games} (\textsf{PSAWT} for short)
		if in all turn-based games $\mathcal{G}  = \mathcal{G} ames{\mathsf{A} conc}{W}$ where there is a subgame
		almost-surely winning strategy, there is a positional one. 
	\end{definition}

	\begin{theorem}[Proof in
		Appendix~\ref{proof:thm_transfer_memory_finite_choice}]
		Consider a \textsf{PSAWT} PI objective $W \ensuremath{\mathsf{s}}ubseteq \mathsf{K} ^\omega$ with a
		neutral color 

		and a  concurrent game $\mathcal{G} $ with objective $W$. Assume  there
		is a subgame optimal strategy that has finite choice. Then, there is a
		positional one.
		\label{thm:transfer_memory_finite_choice}
	\end{theorem}
	\begin{proof}[Sketch]
		A finite-choice strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $ 
		plays only among a finite number of $\mathsf{GF}$-strategies at each state. The idea
		is therefore to modify the game $\mathcal{G} _u$ of the previous subsection into a game
		$\mathcal{G} '_u$ by transforming it into a (finite) turn-based game. At each state,
		Player $\mathsf{A} $ chooses first her $\mathsf{GF}$-strategy. She can choose among only a finite
		number of them: she has at her disposal, at a state $q$, only optimal
		$\mathsf{GF}$-strategies in $S^{\ensuremath{\mathsf{s}}_\mathsf{A} }_q$ (recall
		Definition~\ref{def:finite_choice_strategies})

		. We consider the objective $W$ in that new arena where Player $\mathsf{B} $ states are
		colored with a neutral color. The existence, in $\mathcal{G} $, of a subgame optimal
		strategy that has finite choice ensures that all states in $\mathcal{G} _u'$ have positive
		values. We can then conclude as for Theorem~\ref{thm:transfer_memory}: a subgame
		optimal strategy can be obtained by gluing together subgame almost-surely
		winning strategies in the (turn-based) games $\mathcal{G} _u'$ (that can be chosen
		positional by assumption).

	\end{proof}
	
	As an application, one can realize that the parity, mean-payoff and generalized
	Büchi objectives have a neutral color and are \textsf{PSAWT}
	(\cite{DBLP:conf/soda/ChatterjeeJH04,liggett1969stochastic,DBLP:conf/qest/ChatterjeeAH04}).
	Hence, for these objectives, if there exists an 
	optimal strategy that has finite choice, then there is one that is positional.
	\begin{corollary}[Proof in
		Appendix~\ref{proof:coro_transfer_memory_finite_choice}]
		Consider a concurrent game $\mathcal{G} $ with a parity (resp. mean-payoff, resp.
		generalized Büchi) objective. Assume that there is an 
		optimal strategy that has finite choice in $\mathcal{G} $. Then, there is a positional
		one.
		\label{coro:transfer_memory_finite_choice}
	\end{corollary}
	
	
	

	

	
	

	\appendix	
	\ensuremath{\mathsf{s}}ection{Additional preliminaries}

	For a set $Q$ and a subset $S \ensuremath{\mathsf{s}}ubseteq Q^+$ of finite sequences of elements of
	$Q$, we denote by $S^\omega \ensuremath{\mathsf{s}}ubseteq Q^\omega$ the set of infinite sequences of
	elements of $Q$ with infinitely many prefixes in $S$: $S^\omega := \{ \pi \in
	Q^\omega \mid \forall i \in \ensuremath{\mathbb{N}},\; \exists j \geq i,\; \pi_{\leq j} \in S \}$.
	
	Let us also define the notion of (countable) Markov chain. A Markov chain is a
	pair $(Q,\mathbb{P})$ where $Q$ is the set of states and $\mathbb{P}: Q \times Q
	\rightarrow [0,1]$ is the probability function such that, for all states $q \in
	Q$, we have $\ensuremath{\mathsf{s}}um_{q' \in Q} \mathbb{P}(q,q') = 1$.
		
	\ensuremath{\mathsf{s}}ection{Proofs from
		Section~\ref{sec:conditions_subgame_optimal}}
	\label{app:conditions_subgame_optimal}
	We recall a proposition from \cite{BBSCSLarXiv} (specifically, Proposition 42
	in \cite{BBSCSLarXiv}) that we use in this section.
	\begin{proposition}
		\label{prop:outcome_valuation}
		Consider a PI concurrent game $\mathcal{G}  = \mathcal{G} ames{\mathsf{A} conc}{W}$

		, a state $q \in Q$ and strategies $\ensuremath{\mathsf{s}}igma_\mathsf{A} ,\ensuremath{\mathsf{s}}igma_\mathsf{B}  \in \mathcal{D} (A) \times
		\mathcal{D} (B)$ for both players in the game in normal form $\mathcal{F}_q$. We have the
		following relation:
		\[\ensuremath{\mathsf{s}}um_{q' \in Q} \mathbb{P}^{q,q'}(\ensuremath{\mathsf{s}}igma_\mathsf{A} ,\ensuremath{\mathsf{s}}igma_\mathsf{B} )
		\cdot \MarVal{\mathcal{G} }(q') = \ensuremath{\mathsf{out}}_{\mathcal{F}_q}(\ensuremath{\mathsf{s}}igma_\mathsf{A} ,\ensuremath{\mathsf{s}}igma_\mathsf{B} )\]
	\end{proposition}
	
	\ensuremath{\mathsf{s}}ubsection{Proof of Lemma~\ref{prop:sub_game_opt_implies_locally_opt}}
	\label{proof:prop_sub_game_opt_implies_locally_opt}
	We show the proposition below.
	\begin{proposition}
		\label{prop:optimal_implies_locally_optimal}
		Consider a PI concurrent game $\mathcal{G} $ and a Player $\mathsf{A} $ optimal strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $
		from a state $q \in Q$. Then, for all Player $\mathsf{B} $ actions $b \in B_q$, we have
		$\ensuremath{\mathsf{out}}_{\mathcal{F}_q}(\ensuremath{\mathsf{s}}_\mathsf{A} (q),b) \geq \MarVal{\mathcal{G} }(q)$.
	\end{proposition}
	The proof is identical to the proof of Lemma 17 in \cite{BBSArXivICALP} in the
	case of positional strategies.
	\begin{proof}
		Assume towards a contradiction that 
		it is not the case, i.e. there is a Player $\mathsf{B} $ action $b \in B_q$ such that
		$\ensuremath{\mathsf{out}}_{\mathcal{F}_q}(\ensuremath{\mathsf{s}}_\mathsf{A} (q),b) \leq \MarVal{\mathcal{G} }(q) - \ensuremath{\mathsf{val}}repsilon$ for some
		$\ensuremath{\mathsf{val}}repsilon > 0$. Let us show that the strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $ is then not optimal
		from $q$. Consider a Player $\mathsf{B} $ strategy $\ensuremath{\mathsf{s}}_\mathsf{B} '$ such that for all $q' \in Q$,
		the value of the strategy at state $q'$ is at most $\MarVal{\mathcal{G} }(q') +
		\ensuremath{\mathsf{val}}repsilon/2$: $\MarVal{\mathcal{G} }[\ensuremath{\mathsf{s}}_\mathsf{B} ](q') \leq \MarVal{\mathcal{G} }(q') + \ensuremath{\mathsf{val}}repsilon/2$.
		We then define a Player $\mathsf{B} $ strategy $\ensuremath{\mathsf{s}}_\mathsf{B} $ as follows: $\ensuremath{\mathsf{s}}_\mathsf{B} (q) := b$ and,
		for all $q' \in Q$, we have $\ensuremath{\mathsf{s}}_\mathsf{B} (q \cdot q') := \ensuremath{\mathsf{s}}_\mathsf{B} (q')$. Then, as $W$ is
		prefix-independent and by  Proposition~\ref{prop:outcome_valuation}, we obtain:
		\begin{align*}
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }_q[W] & = \ensuremath{\mathsf{s}}um_{q' \in Q}
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(q)[q'] \cdot \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ^{q \cdot q'},\ensuremath{\mathsf{s}}_\mathsf{B} ^{q
				\cdot q'}}_{q'}[W] \\
		& \leq \ensuremath{\mathsf{s}}um_{q' \in Q} \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(q)[q'] \cdot (\MarVal{\mathcal{G} }(q')
		+ \ensuremath{\mathsf{val}}repsilon/2) \\
		& = \ensuremath{\mathsf{s}}um_{q' \in Q} \mathbb{P}^{q,q'}(\ensuremath{\mathsf{s}}_\mathsf{A} (\rho),\ensuremath{\mathsf{s}}_\mathsf{B} (\rho)) \cdot
		\MarVal{\mathcal{G} }(q') + \ensuremath{\mathsf{val}}repsilon/2 \\
		& = \ensuremath{\mathsf{out}}_{\mathcal{F}_q}(\ensuremath{\mathsf{s}}_\mathsf{A} (q),b) + \ensuremath{\mathsf{val}}repsilon/2 \\
		& \leq \MarVal{\mathcal{G} }[q] - \ensuremath{\mathsf{val}}repsilon + \ensuremath{\mathsf{val}}repsilon/2 = \MarVal{\mathcal{G} }[q] -
		\ensuremath{\mathsf{val}}repsilon/2
		\end{align*}
		That is, the strategy $\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho$ is not optimal from $q$.	
	\end{proof}
	
	The proof of Lemma~\ref{prop:sub_game_opt_implies_locally_opt} is then a direct
	consequence.
	\begin{proof}
		Assume towards a contradiction that $\ensuremath{\mathsf{s}}_\mathsf{A} $ is not locally optimal. That is,
		there is some $\rho = \rho' \cdot q \in Q^+$ and a Player $\mathsf{B} $ action $b \in
		B_q$ such that $\ensuremath{\mathsf{out}}_{\mathcal{F}_q}(\ensuremath{\mathsf{s}}_\mathsf{A} (\rho),b) \leq \MarVal{\mathcal{G} }(q) -
		\ensuremath{\mathsf{val}}repsilon$ for some $\ensuremath{\mathsf{val}}repsilon > 0$. It follows by
		Proposition~\ref{prop:optimal_implies_locally_optimal} that the residual
		strategy $\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho$ is not optimal from $\rho$, hence the contradiction.
	\end{proof}
	
	\ensuremath{\mathsf{s}}ubsection{Proof of Lemma~\ref{lem:locally_opt_implies_same_value}}
	\label{proof:lem_locally_opt_implies_same_value}
	First, let us state a straightforward proposition about locally optimal
	strategies.
	\begin{proposition}
		\label{prop:locally_opt_next}
		In a PI concurrent game $\mathcal{G} $, for a Player $\mathsf{A} $ locally optimal strategy
		$\ensuremath{\mathsf{s}}_\mathsf{A} $ and a deterministic Player $\mathsf{B} $ strategy, for all finite paths $\rho =
		\rho' \cdot q \in Q^+$, we have
		$\MarVal{\mathcal{G} }(q) \leq \ensuremath{\mathsf{s}}um_{u \in V_{\mathcal{G} }} u \cdot
		\mathbb{P}_\rho^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }[Q_u]$.
	\end{proposition}
	\begin{proof}
		We let $b := \ensuremath{\mathsf{s}}_\mathsf{B} (\rho) \in B_q$. We have:
		\begin{align*}
		\MarVal{\mathcal{G} }(q) & \leq \ensuremath{\mathsf{s}}um_{a \in A} \ensuremath{\mathsf{s}}_\mathsf{A} (\rho)(a) \cdot \LiftVal{\mathcal{G} } \circ
		\delta(q,a,b) = \ensuremath{\mathsf{s}}um_{a \in A} \ensuremath{\mathsf{s}}_\mathsf{A} (\rho)(a) \cdot (\ensuremath{\mathsf{s}}um_{q' \in Q}
		\mathsf{dist}  \circ \delta(q,a,b)(q') \cdot \MarVal{\mathcal{G} }(q')) \\
		& = \ensuremath{\mathsf{s}}um_{u \in V_{\mathcal{G} }} \ensuremath{\mathsf{s}}um_{a \in A} \ensuremath{\mathsf{s}}_\mathsf{A} (\rho)(a) \cdot (\ensuremath{\mathsf{s}}um_{q' \in Q_u}
		\mathsf{dist}  \circ \delta(q,a,b)(q') \cdot \MarVal{\mathcal{G} }(q')) \\
		& = \ensuremath{\mathsf{s}}um_{u \in V_{\mathcal{G} }} u \cdot \left(\ensuremath{\mathsf{s}}um_{q' \in Q_u} \ensuremath{\mathsf{s}}um_{a \in A}
		\ensuremath{\mathsf{s}}_\mathsf{A} (\rho)(a) \cdot \mathsf{dist}  \circ \delta(q,a,b) \right) = \ensuremath{\mathsf{s}}um_{u \in
			V_{\mathcal{G} }} u \cdot \mathbb{P}_\rho^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }[Q_u]
		\end{align*}
	\end{proof}
	
	We can now proceed to the proof of
	Lemma~\ref{lem:locally_opt_implies_same_value}.
	\begin{proof}
		We denote by $v$ the valuation $\MarVal{\mathcal{G} }$. We extend the valuation $v$ to
		finite paths: $v^+: Q^+ \rightarrow [0,1]$ such that, for all $\rho \cdot q \in
		Q^+$, we have $v^+(\rho \cdot q) := v(q)$. If all states have value 0 or 1, the
		lemma straightforwardly holds. Let us now assume that there are some states of
		value between 0 and 1. Let us denote by $0 = u_0 < u_1 < \ldots < u_n = 1$ the
		states values in $V_{\mathcal{G} }$
		, i.e. $|V_{\mathcal{G} }| = n+1$. For all $i \leq n+1$, we denote by $Q_{\leq i}$ the
		set $Q_{\leq i} := v^{-1}[\{ u_0,\ldots,u_i \}]$

		. We show by induction on $k \leq n$ the following property $\mathcal{P}(k)$:

		\begin{displaymath}
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(\bigcup_{0 \leq i \leq k} Q^* \cdot (Q_{u_i})^\omega
		\cap Q^* \cdot (Q_{\leq k})^\omega) = \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(Q^* \cdot
		(Q_{\leq k})^\omega)
		\end{displaymath}
		This straightforwardly holds for $k = 0$. Consider now some $k \leq n$ and
		assume that $\mathcal{P}(k)$ holds. 

		We have:
		\begin{align*}
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(Q^* \cdot (Q_{\leq k+1})^\omega ) & =
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(Q^* \cdot (Q_{k+1})^\omega \cap Q^* \cdot (Q_{\leq
			k+1})^\omega ) \\
		& + \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(Q^* \cdot (Q_{\leq k})^\omega \cap Q^* \cdot
		(Q_{\leq k+1})^\omega ) \\
		& + \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }((Q^* \cdot Q_{\leq k})^\omega \cap (Q^* \cdot
		Q_{k+1})^\omega \cap Q^* \cdot (Q_{\leq k+1})^\omega) 
		\end{align*}
		Let us show that the term $\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }((Q^* \cdot Q_{\leq
			k})^\omega \cap (Q^* \cdot Q_{k+1})^\omega \cap Q^* \cdot (Q_{\leq k+1})^\omega)
		= 0$. This holds if $k = n$ since then, $u_{k+1} = 1$ and being locally optimal
		means that all states seen with positive probability have value 1. Assume now
		that $k < n$ and $u_{k+1} < 1$. For all $l \in \ensuremath{\mathbb{N}}$, we denote by $E_{\leq k}^l$
		the event $E_{\leq k}^l := Q^l \cdot (Q_{k+1} \cap Q \cdot Q_{\leq k})$ and by
		$E_{\geq k+2}^l$ the event $E_{\geq k+2}^l := Q^l \cdot (Q_{k+1} \cap Q \cdot
		Q_{\geq k+2})$. Let also $E^l := E_{\leq k}^l \cup E_{\geq k+2}^l$. We also
		denote by $E_{\leq k}^\infty := \cap_{d \in \ensuremath{\mathbb{N}}} \cup_{l \geq d} E_{\leq k}^l$,
		$E_{\geq k+2}^\infty := \cap_{d \in \ensuremath{\mathbb{N}}} \cup_{l \geq d} E_{\geq k+2}^l$ and
		$E^\infty := \cap_{d \in \ensuremath{\mathbb{N}}} \cup_{l \geq d} E^l$. If $
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(E^\infty) = 0$ then $\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }((Q^*
		\cdot Q_{\leq k})^\omega \cap (Q^* \cdot Q_{k+1})^\omega \cap Q^* \cdot (Q_{\leq
			k+1})^\omega) = 0$ since $(Q^* \cdot Q_{\leq k})^\omega \cap (Q^* \cdot
		Q_{k+1})^\omega \cap Q^* \cdot (Q_{\leq k+1})^\omega \ensuremath{\mathsf{s}}ubseteq E^\infty_{\leq k}
		\ensuremath{\mathsf{s}}ubseteq E^\infty$. Let us now assume that $ \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(E^\infty)
		> 0$.
		
		Consider some $\rho = \rho' \cdot q \in Q^+ \cdot Q_{k+1}$. Since $\ensuremath{\mathsf{s}}_\mathsf{A} $ is
		locally optimal and by Proposition~\ref{prop:locally_opt_next}, we have:
		\begin{align*}
		u_{k+1} \leq \ensuremath{\mathsf{s}}um_{u \in V_{\mathcal{G} }} u \cdot \mathbb{P}_\rho^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }[Q_u] &
		= u_{k+1} \cdot \mathbb{P}_\rho^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }[Q_{u_{k+1}}] + \ensuremath{\mathsf{s}}um_{u \leq u_k} u
		\cdot \mathbb{P}_\rho^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }[Q_{u}] + \ensuremath{\mathsf{s}}um_{u \geq u_{k+2}} u \cdot
		\mathbb{P}_\rho^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }[Q_{u}] \\
		& \leq u_{k+1} \cdot \mathbb{P}_\rho^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }[Q_{u_{k+1}}] + \ensuremath{\mathsf{s}}um_{u \leq
			u_k} u_k \cdot \mathbb{P}_\rho^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }[Q_{u}] + \ensuremath{\mathsf{s}}um_{u \geq u_{k+2}}
		\mathbb{P}_\rho^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }[Q_{u}] \\
		& = u_{k+1} \cdot \mathbb{P}_\rho^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }[Q_{u_{k+1}}] + u_k \cdot
		\mathbb{P}_\rho^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }[Q_{\leq k}] +
		\mathbb{P}_\rho^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }[Q_{\geq k+2}] \\
		\end{align*}
		Denoting $\mathbb{P}_\rho^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }[Q_{\leq k}]$ by $p_k$ and
		$\mathbb{P}_\rho^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }[Q_{\geq k+2}]$ by $p_{k+2}$, we obtain:
		\begin{align*}
		& u_{k} \cdot p_k + p_{k+2} \geq u_{k+1} \cdot (p_k+p_{k+2}) \\
		\Leftrightarrow \; & p_{k+2} \cdot (1 - u_{k+1}) \geq p_k \cdot (u_{k+1} -
		u_k) \\
		\Leftrightarrow \; & p_{k+2} \geq p_k \cdot \frac{u_{k+1} - u_k}{1 - u_{k+1}}
		= p_{k+2} \cdot x
		\end{align*}
		for $x := \frac{u_{k+1} - u_k}{1 - u_{k+1}} \geq 0$. Hence, setting $c :=
		\frac{x}{1 + x} \in ]0,1[$, we have $\frac{p_{k+2}}{p_k + p_{k+2}} \geq c$. That
		is, for $l = |\rho|$, we have: 
		\begin{displaymath}
		\mathbb{P}_\rho^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(\lnot E^l_{\geq k+2} \cap E^l) \leq (1 - c)
		\cdot \mathbb{P}_\rho^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(E^l) 
		\end{displaymath}
		Then, consider the probability $\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(\lnot E^\infty_{\geq
			k+2} \mid E^\infty)$ (recall that $\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(E^\infty) > 0$).
		This is equal to:
		\begin{displaymath}
		\lim\limits_{d \rightarrow \infty} \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(\bigcap_{l \geq d}
		(\lnot E^l_{\geq k+2}) \mid E^\infty) \leq \lim\limits_{d \rightarrow \infty}
		(\lim\limits_{t \rightarrow \infty} (1-c)^t) = 0
		\end{displaymath}
		
		Furthermore:
		\begin{displaymath}
		(Q^* \cdot Q_{\leq k})^\omega \cap (Q^* \cdot Q_{k+1})^\omega \cap Q^* \cdot
		(Q_{\leq k+1})^\omega \ensuremath{\mathsf{s}}ubseteq (Q^\omega \ensuremath{\mathsf{s}}etminus E^\infty_{\geq k+2}) \cap
		E^\infty
		\end{displaymath}
		
		It follows that:
		\begin{displaymath}
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }((Q^* \cdot Q_{\leq k})^\omega \cap (Q^* \cdot
		Q_{k+1})^\omega \cap Q^* \cdot (Q_{\leq k+1})^\omega) \leq
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(\lnot E^\infty_{\geq k+2} \cap E^\infty) =
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(\lnot E^\infty_{\geq k+2} \mid E^\infty) \cdot
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(E^\infty) = 0
		\end{displaymath}
		

		Overall:
		\begin{align*}
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(Q^* \cdot (Q_{\leq k+1})^\omega ) & =
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(Q^* \cdot (Q_{k+1})^\omega \cap Q^* \cdot (Q_{\leq
			k+1})^\omega ) + \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(Q^* \cdot (Q_{\leq k})^\omega \cap Q^*
		\cdot (Q_{\leq k+1})^\omega ) \\
		& = \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(Q^* \cdot (Q_{k+1})^\omega ) +
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(Q^* \cdot (Q_{\leq k})^\omega ) \\
		& = \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(Q^* \cdot (Q_{k+1})^\omega ) +
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(\bigcup_{0 \leq i \leq k} Q^* \cdot (Q_{u_i})^\omega
		\cap Q^* \cdot (Q_{\leq k})^\omega) \\
		& = \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(\bigcup_{0 \leq i \leq k+1} Q^* \cdot
		Q_{u_i}^\omega \cap Q^* \cdot (Q_{\leq k+1})^\omega )
		\end{align*}
		Hence, $\mathcal{P}(k+1)$ holds. In fact, it does for all $k \leq n$. 	Then,
		the lemma exactly corresponds to $\mathcal{P}(n)$ since $Q_{\leq n} = Q$.
	\end{proof}
	
	\ensuremath{\mathsf{s}}ubsection{Proof of Lemma~\ref{lem:locally_opt_implies_convex_comb}}
	\label{proof:lem_locally_opt_implies_convex_comb_ok}

	In fact, we prove the more general lemma below.
	\begin{lemma}[Proof~\ref{proof:lem_locally_opt_implies_convex_comb_ok}]
		\label{lem:locally_opt_implies_convex_comb_ok}
		Consider an PI concurrent game $\mathcal{G} 
		$

		, a Player $\mathsf{A} $ locally optimal strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $ and a Player $\mathsf{B} $
		deterministic strategy $\ensuremath{\mathsf{s}}_\mathsf{B} $. For a finite sequence $\rho = \rho' \cdot q \in
		Q^+$
		:

		\begin{displaymath}
		\MarVal{\mathcal{G} }(q) \leq \ensuremath{\mathsf{s}}um_{u \in V_{\mathcal{G} }} u \cdot
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}_\rho[Q^* \cdot (Q_u)^\omega]
		\end{displaymath}
	\end{lemma}
	\begin{proof}
		We consider the locally optimal strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $, a deterministic Player $\mathsf{B} $
		strategy $\ensuremath{\mathsf{s}}_\mathsf{B} $ and the finite path $\rho \in Q^+$.	

		Let us consider the infinite Markov chain $\mathcal{M} = (\rho \cdot
		Q^+,\mathbb{P})$ with $\mathbb{P}: \rho \cdot Q^+ \times \rho \cdot Q^+
		\rightarrow [0,1]$ where, for all $\pi \in Q^+$

		, we have $\mathbb{P}(\rho \cdot \pi,\rho \cdot \pi \cdot q) :=
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(\rho \cdot \pi,q)$. All other probabilities are equal
		to 0. 
		The probability measure $\mathbb{P}$ is extended to finite paths starting at
		$\rho$, cylinders and arbitrary Borel sets (in particular, to $W$). 

		

		
		We additionally define inductively the function $f: \rho \cdot Q^+ \rightarrow
		\ensuremath{\mathbb{N}}$ in the following way: $f(\rho) := 0$ and for all $\pi \cdot q \cdot q' \in
		Q^+$, we set $f(\rho \cdot \pi \cdot q \cdot q') := f(\rho \cdot \pi \cdot q)$
		if $\MarVal{\mathcal{G} }(q) = \MarVal{\mathcal{G} }(q')$ 

		and $f(\rho \cdot q \cdot q') := f(\rho \cdot q) + 1$ otherwise. 

		This function counts the number of changes of values.
		
		Let $\ensuremath{\mathsf{val}}repsilon > 0$

		. By Lemma~\ref{lem:locally_opt_implies_same_value}, we have 
		\begin{displaymath}
		\lim\limits_{n \rightarrow \infty}  \mathbb{P}(Q^+ \cdot f^{-1}[\{n\}]) = 0	
		\end{displaymath}
		Consider some $N \in \ensuremath{\mathbb{N}}$ such that $\mathbb{P}(Q^+ \cdot f^{-1}[N+1]) \leq
		\ensuremath{\mathsf{val}}repsilon/2$. For all $0 \leq k \leq N$ and values $u \in V_{\mathcal{G} }$, we denote
		by $(Q_u,k) \ensuremath{\mathsf{s}}ubseteq \rho \cdot Q^+$ the set of finite paths ending in $Q_u$
		and whose values w.r.t. the function $f$ are $k$: $(Q_u,k) := \{ \rho \cdot \pi
		\cdot q \in Q^+ \mid q \in Q_u,\; f(\rho \cdot \pi \cdot q) = k \}$. For all $n
		\in \ensuremath{\mathbb{N}}$, we denote by $(Q_u,k)_n := \rho \cdot Q^n \cap (Q_u,k)$.

		
		For all $0 \leq k \leq N$, we denote by $n_k \in \ensuremath{\mathbb{N}}$ an index such that:
		\begin{displaymath}
		\mathbb{P}(Q^+ \cdot f^{-1}[k]) \leq \mathbb{P}(Q^{\leq n_k} \cdot f^{-1}[k])
		+ \frac{\ensuremath{\mathsf{val}}repsilon}{2 \cdot (N+1) \cdot N_{V_{\mathcal{G} }}}
		\end{displaymath} 
		where $N_{V_{\mathcal{G} }} := |V_{\mathcal{G} }|$ (this exists since $\mathbb{P}(Q^+ \cdot S) =
		\lim_{n \rightarrow \infty} \mathbb{P}(Q^{\leq n} \cdot S)$

		). In particular, this implies $\mathbb{P}(Q^{> n_k} \cdot f^{-1}[k]) =
		\mathbb{P}(Q^+ \cdot f^{-1}[k]) - \mathbb{P}(Q^{\leq n_k} \cdot f^{-1}[k]) \leq
		\ensuremath{\mathsf{val}}repsilon/(2 \cdot (N+1) \cdot N_V)$. 

		Now, let $n := \max_{0 \leq k \leq N} n_k$. 

		Let us show that, for all $0 \leq k \leq N$ and $u \in V_{\mathcal{G} }$, we have:
		\begin{equation}
		\label{eqn:close_always_value}

		\mathbb{P}[(Q_u,k)_n] = \ensuremath{\mathsf{s}}um_{\pi \in (Q_u,k)_n} \mathbb{P}(\pi) \leq
		\mathbb{P}(Q^+ \cdot (Q_u,k)^\omega) + \frac{\ensuremath{\mathsf{val}}repsilon}{2 \cdot (N+1) \cdot
			N_V}
		\end{equation}
		
		Indeed, since $n \geq n_k$, we have:
		\begin{align*}
		\mathbb{P}(Q^+ \cdot (Q_u,k)^\omega) & \geq \mathbb{P}(Q^{\leq n} \cdot
		(Q_u,k)^\omega) \\
		& = \ensuremath{\mathsf{s}}um_{\pi \in (Q_u,k)_n} \mathbb{P}(\pi) \cdot
		\mathbb{P}_\pi((Q_u,k)^\omega) \\
		& = \ensuremath{\mathsf{s}}um_{\pi \in (Q_u,k)_n} \mathbb{P}(\pi) \cdot (1 - \mathbb{P}_\pi(Q^+
		\cdot f^{-1}[k+1])) \\
		& = \ensuremath{\mathsf{s}}um_{\pi \in (Q_u,k)_n} \mathbb{P}(\pi) - \ensuremath{\mathsf{s}}um_{\pi \in (Q_u,k)_n}
		\mathbb{P}(\pi) \cdot \mathbb{P}_\pi(Q^+ \cdot  f^{-1}[k+1])) \\
		& \geq \ensuremath{\mathsf{s}}um_{\pi \in (Q_u,k)_n} \mathbb{P}(\pi) - \mathbb{P}_{> n}(Q^+ \cdot
		f^{-1}[k+1])) \\
		& \geq \ensuremath{\mathsf{s}}um_{\pi \in (Q_u,k)_n} \mathbb{P}(\pi) - \frac{\ensuremath{\mathsf{val}}repsilon}{2 \cdot
			(N+1) \cdot N_V} \\

		\end{align*}

		
		
		We obtain Equation~(\ref{eqn:close_always_value}). In the following, we denote
		the valuation $\MarVal{\mathcal{G} }$ by $v: Q \rightarrow [0,1]$. Let us show by
		induction on $i$ the following property $\mathcal{P}(i)$: \textquotedblleft
		$\ensuremath{\mathsf{s}}um_{\pi \in \rho \cdot Q^i} \mathbb{P}(\pi) \cdot v(\pi) \geq
		v(\rho)$\textquotedblright where $v(\pi) \in [0,1]$ refers to $v(q)$ for $q \in
		Q$ the last state of $\pi$
		. The property $\mathcal{P}(0)$ straightforwardly holds. Assume now that this
		property holds for some $i \in \ensuremath{\mathbb{N}}$. We have, by
		Proposition~\ref{prop:outcome_valuation} and since $\ensuremath{\mathsf{s}}_\mathsf{A} $ is locally optimal:
		\begin{align*}
		\ensuremath{\mathsf{s}}um_{\pi \in \rho \cdot Q^{i+1}} \mathbb{P}(\pi) \cdot v(\pi) & = \ensuremath{\mathsf{s}}um_{\pi =
			\rho \cdot q_1 \cdots q_i \cdot q_{i+1} \in \rho \cdot Q^{i+1}} \mathbb{P}(\pi)
		\cdot v(q_{i+1}) \\
		& = \ensuremath{\mathsf{s}}um_{\pi' = \rho \cdot q_0 \cdots q_i \in \rho \cdot Q^{i}} \ensuremath{\mathsf{s}}um_{q_{i+1}
			\in Q} \mathbb{P}(\pi' \cdot q_{i+1}) \cdot v(q_{i+1}) \\
		& = \ensuremath{\mathsf{s}}um_{\pi' = \rho \cdot q_1 \cdots q_i \in \rho \cdot Q^{i}} \ensuremath{\mathsf{s}}um_{q_{i+1}
			\in Q} \mathbb{P}(\pi') \cdot \mathbb{P}(\pi',\pi' \cdot q_{i+1}) \cdot
		v(q_{i+1}) \\
		& = \ensuremath{\mathsf{s}}um_{\pi' = \rho \cdot q_0 \cdots q_i \in \rho \cdot Q^{i}}
		\mathbb{P}(\pi') \cdot \ensuremath{\mathsf{s}}um_{q_{i+1} \in Q} \mathbb{P}(\pi',\pi' \cdot q_{i+1})
		\cdot v(q_{i+1}) \\
		& = \ensuremath{\mathsf{s}}um_{\pi' = \rho \cdot q_1 \cdots q_i \in \rho \cdot Q^{i}}
		\mathbb{P}(\pi') \cdot \ensuremath{\mathsf{s}}um_{q_{i+1} \in Q}
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(\pi')[q_{i+1}] \cdot v(q_{i+1}) \\
		& = \ensuremath{\mathsf{s}}um_{\pi' = \rho \cdot q_1 \cdots q_i \in \rho \cdot Q^{i}}
		\mathbb{P}(\pi') \cdot \ensuremath{\mathsf{s}}um_{q_{i+1} \in Q}
		\mathbb{P}^{q_i,q_{i+1}}(\ensuremath{\mathsf{s}}_\mathsf{A} (\pi'),\ensuremath{\mathsf{s}}_\mathsf{B} (\pi')) \cdot v(q_{i+1}) \\
		& = \ensuremath{\mathsf{s}}um_{\pi' = \rho \cdot q_1 \cdots q_i \in \rho \cdot Q^{i}}
		\mathbb{P}(\pi') \cdot \ensuremath{\mathsf{out}}_{\mathcal{F}_{q_i}}(\ensuremath{\mathsf{s}}_\mathsf{A} (\pi'),\ensuremath{\mathsf{s}}_\mathsf{B} (\pi')) \\

		& \geq \ensuremath{\mathsf{s}}um_{\pi' = \rho \cdot q_1 \cdots q_i \in \rho \cdot Q^{i}}
		\mathbb{P}(\pi') \cdot v(q_i) \\
		& \geq v(\rho)
		\end{align*}
		Hence, the property $\mathcal{P}(i)$ is ensured for all $i \in \mathbb{N}$, in
		particular $\mathcal{P}(n)$ holds. It follows that:
		
		\begin{align*}
		\hspace*{-1.3cm}
		\ensuremath{\mathsf{s}}um_{u \in V_{\mathcal{G} }} u \cdot \mathbb{P}(Q^+ \cdot (Q_u)^\omega) & \geq \ensuremath{\mathsf{s}}um_{u
			\in V_{\mathcal{G} }} u \cdot \mathbb{P}(\bigcup_{k = 0}^N Q^+ \cdot (Q_u,k)^\omega) &
		\text{ since }\bigcup_{k = 0}^N Q^+ \cdot (Q_u,k)^\omega \ensuremath{\mathsf{s}}ubseteq Q^+ \cdot
		Q_u^\omega\\
		& \geq \ensuremath{\mathsf{s}}um_{k = 0}^N \ensuremath{\mathsf{s}}um_{u \in V_{\mathcal{G} }} u \cdot \mathbb{P}(Q^+ \cdot
		(Q_u,k)^\omega) & \text{ since } (Q_u,k)^\omega \cap (Q_u,j)^\omega = \emptyset
		\text{ if }k \neq j\\
		& \geq \ensuremath{\mathsf{s}}um_{k = 0}^N \ensuremath{\mathsf{s}}um_{u \in V_{\mathcal{G} }} u \cdot (\ensuremath{\mathsf{s}}um_{\pi \in (Q_u,k)_n}
		\mathbb{P}(\pi) - \frac{\ensuremath{\mathsf{val}}repsilon}{2 \cdot (N+1) \cdot N_{V_\mathcal{G} }}) & \text{ by
			Equation~(\ref{eqn:close_always_value}) }\\
		& \geq \ensuremath{\mathsf{s}}um_{k = 0}^N \ensuremath{\mathsf{s}}um_{u \in V} \ensuremath{\mathsf{s}}um_{\pi \in (Q_u,k)_n} \mathbb{P}(\pi)
		\cdot v(\pi) - \frac{\ensuremath{\mathsf{val}}repsilon}{2} & \text{ since }u = v(\pi), \forall \pi \in
		(Q_u,k)_n \\
		& = \ensuremath{\mathsf{s}}um_{k = 0}^N \ensuremath{\mathsf{s}}um_{\pi \in \rho \cdot Q^n \cap f^{-1}[k]}
		\mathbb{P}(\pi) \cdot v(\pi) - \frac{\ensuremath{\mathsf{val}}repsilon}{2} & \text{ since }\rho \cdot
		Q^n \cap f^{-1}[k] = \uplus_{u \in V_{\mathcal{G} }} (Q_u,k)_n \\
		& \geq \ensuremath{\mathsf{s}}um_{\pi \in \rho \cdot Q^n} \mathbb{P}(\pi) \cdot v(\pi) -
		\ensuremath{\mathsf{val}}repsilon & \text{ since }\mathbb{P}(Q^+ \cdot f^{-1}[N+1]) \leq
		\frac{\ensuremath{\mathsf{val}}repsilon}{2}\\
		& \geq v(\rho) - \ensuremath{\mathsf{val}}repsilon & \text{ by }\mathcal{P}(n)
		\end{align*}
		As this holds for all $\ensuremath{\mathsf{val}}repsilon > 0$, we obtain: $\ensuremath{\mathsf{s}}um_{u \in V_{\mathcal{G} }} u
		\cdot \mathbb{P}(Q^+ \cdot (Q_u)^\omega) \geq v(\rho) = \MarVal{\mathcal{G} }(q)$ (for $q$
		the last state of $\rho$).
	\end{proof}
	Lemma~\ref{lem:locally_opt_implies_convex_comb} is then a direct consequence.
	
	\ensuremath{\mathsf{s}}ubsection{Levy's 0-1 Law on Markov chains}
	\label{appen:levy}
	Let us state an adaptation of Levy's 0-1 Law to the context of infinite Markov
	chains to prefix-independent objectives. This comes from Theorem 5  in
	\cite{DBLP:conf/icalp/KieferMSTW20}:
	\begin{theorem}[Levy's 0-1 Law for prefix-independent objectives]
		Consider a countable Markov chain $\mathcal{M}$ on a set of states $Q$ with a
		probability $\mathbb{P}$. For all prefix-independent objectives $W \ensuremath{\mathsf{s}}ubseteq
		Q^\omega$, the sets $W$ and $\{ \rho \in Q^\omega \mid \lim_{n \rightarrow
			\infty} \mathbb{P}_{\rho_n}(W) = 1 \}$ are equal up to a null set. This also
		holds for $Q^\omega \ensuremath{\mathsf{s}}etminus W$: the sets $Q^\omega \ensuremath{\mathsf{s}}etminus W$ and $\{ \rho
		\in Q^\omega \mid \lim_{n \rightarrow \infty} \mathbb{P}_{\rho_n}(W) = 0 \}$ are
		equal up to a null set.
		\label{thm:levy}
	\end{theorem}
	
	Lemma~\ref{lem:chaterjee_value_0_1} is then a direct consequence of this
	theorem. Note that Lemma~\ref{lem:chaterjee_value_0_1} also comes from Lemma 2
	in \cite{CH07}.
	
	\ensuremath{\mathsf{s}}ubsection{Proof of Theorem~\ref{thm:subgame_optimal_arbitrary_strategy}}
	\label{proof:lem_optimal_arbitrary_strategy}

	\begin{proof}
		The first property is necessary by
		Lemma~\ref{prop:sub_game_opt_implies_locally_opt}. Let us show that the second
		one is also necessary. Consider a Player $\mathsf{A} $ strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $ such that there
		is a finite paths $\rho \in Q^+$, a deterministic Player $\mathsf{B} $ strategy $\ensuremath{\mathsf{s}}_\mathsf{B} $
		and a positive value $u \in V_{\mathcal{G} } \ensuremath{\mathsf{s}}etminus \{ 0 \}$ such that
		$\mathbb{P}_\rho^{\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[W \cap Q^* \cdot (Q_u)^\omega] <
		\mathbb{P}_\rho^{\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[Q^* \cdot (Q_u)^\omega]$. Consider the
		countable Markov chain induced by both strategies $\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho$ and $\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho$
		whose initial state in $\rho$. We denote by $\mathbb{P}$ the probability
		function in that Markov chain. Consider the prefix-independent objective $W_u :=
		W \cup (Q^* \cdot (Q \ensuremath{\mathsf{s}}etminus Q_u))^\omega$. We have:
		\begin{align*}
		\mathbb{P}[W_u] & = \mathbb{P}[W_u \cap Q^* \cdot (Q_u)^\omega] +
		\mathbb{P}[W_u \cap (Q^* \cdot (Q \ensuremath{\mathsf{s}}etminus Q_u))^\omega] \\
		& = \mathbb{P}[W \cap Q^* \cdot (Q_u)^\omega] + \mathbb{P}[(Q^* \cdot (Q
		\ensuremath{\mathsf{s}}etminus Q_u))^\omega] \\
		& < \mathbb{P}[Q^* \cdot (Q_u)^\omega] + \mathbb{P}[(Q^* \cdot (Q \ensuremath{\mathsf{s}}etminus
		Q_u))^\omega] \\
		& = 1
		\end{align*}
		Let us now show that there is a finite paths whose last state is in $Q_u$ and
		from which the probability of $W_u$ is less than $u/2$. By
		Lemma~\ref{lem:chaterjee_value_0_1}, there is state $\pi \in Q^*$ (which
		corresponds to a finite path) in the Markov chain such that $\mathbb{P}_\pi[W_u]
		< u/2$. If $\pi \in Q^* \cdot Q_u$, we have shown what we want.	Assume now
		towards a contradiction that it is not the case and that for all paths $\pi' \in
		Q^* \cdot Q_u$, we have $\mathbb{P}_{\pi \cdot \pi'}[W_u] \geq u/2$. Then:
		\begin{align*}
		\mathbb{P}_\pi[W_u] & = \mathbb{P}_\pi[W_u \cap (Q \ensuremath{\mathsf{s}}etminus Q_u)^* \cdot Q_u
		\cdot Q^\omega] + \mathbb{P}_\pi[W_u \cap (Q \ensuremath{\mathsf{s}}etminus Q_u)^\omega] \\
		& = \ensuremath{\mathsf{s}}um_{\pi' \in (Q \ensuremath{\mathsf{s}}etminus Q_u)^* \cdot Q_u} \mathbb{P}_{\pi}(\pi') \cdot
		\mathbb{P}_{\pi \cdot \pi'}[W_u] + \mathbb{P}_\pi[(Q \ensuremath{\mathsf{s}}etminus Q_u)^\omega] \\
		& \geq \ensuremath{\mathsf{s}}um_{\pi' \in (Q \ensuremath{\mathsf{s}}etminus Q_u)^* \cdot Q_u} \mathbb{P}_{\pi}(\pi')
		\cdot \frac{u}{2} + \mathbb{P}_\pi[(Q \ensuremath{\mathsf{s}}etminus Q_u)^\omega] \\
		& = \mathbb{P}_\pi[(Q \ensuremath{\mathsf{s}}etminus Q_u)^* \cdot Q_u \cdot Q^\omega] \cdot
		\frac{u}{2} + \mathbb{P}_\pi[(Q \ensuremath{\mathsf{s}}etminus Q_u)^\omega] \\
		& \geq \frac{u}{2}
		\end{align*}
		This is a contradiction since $\mathbb{P}_\pi[W_u] < u/2$. Hence, there exists
		some path $\pi \in Q^* \cdot Q_u$ such that $\mathbb{P}_\pi[W_u] < u/2$. Since
		$W \ensuremath{\mathsf{s}}ubseteq W_u$, it follows that $\mathbb{P}_\pi[W] \leq \mathbb{P}_\pi[W_u] <
		u/2$. That is, the residual strategy $\ensuremath{\mathsf{s}}_\mathsf{A} ^{\rho \cdot \pi}$ is not optimal
		from the last state of $\rho \cdot \pi$, that is the Player $\mathsf{A} $ strategy
		$\ensuremath{\mathsf{s}}_\mathsf{A} $ is not subgame optimal.
		
		Let us now show that these conditions are sufficient. Let $\rho \in Q^+$. Let
		us show that the residual strategy $\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho$ is optimal from $\rho$. Consider
		a Player $\mathsf{B} $ deterministic strategy $\ensuremath{\mathsf{s}}_\mathsf{B} $. We have, by
		Lemma~\ref{lem:locally_opt_implies_same_value}:
		\begin{align*}
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}_\rho[W] & =
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}_\rho[W \cap ( \bigcup_{u \in V_{\mathcal{G} }} Q^+
		\cdot (Q_u)^\omega)] = \ensuremath{\mathsf{s}}um_{u \in V_{\mathcal{G} }}
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}_\rho[W \cap Q^+ \cdot (Q_u)^\omega] \\
		& \geq \ensuremath{\mathsf{s}}um_{u \in V_{\mathcal{G} } \ensuremath{\mathsf{s}}etminus \{ 0 \}} u \cdot
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}_\rho[W \cap Q^+ \cdot (Q_u)^\omega] 

		\\
		& \geq \ensuremath{\mathsf{s}}um_{u \in V_{\mathcal{G} } \ensuremath{\mathsf{s}}etminus \{ 0 \}} u \cdot
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}_\rho[Q^+ \cdot (Q_u)^\omega] + 0 \cdot
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}_\rho[Q^+ \cdot (Q_0)^\omega]\\
		& = \ensuremath{\mathsf{s}}um_{u \in V_{\mathcal{G} }} u \cdot \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}_\rho[Q^+
		\cdot (Q_u)^\omega]  \geq \MarVal{\mathcal{G} }(q)					
		\end{align*}
		Where the last inequality comes from
		Lemma~\ref{lem:locally_opt_implies_convex_comb_ok}.	It follows that the Player
		$\mathsf{A} $ residual strategy $\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho$ is optimal from $\rho$

		.

	\end{proof}
	
	\ensuremath{\mathsf{s}}ection{Proof from Section~\ref{sec:transfer}}
	\label{proof:thm_transfer_almost_sure_optimal}
	
	\ensuremath{\mathsf{s}}ubsection{(Positively) optimal strategy that is locally optimal but not
		subgame optimal}
	\label{appen:exemple_opt_loc_opt_not_sub_game_opt}

	\begin{figure}
\caption{A reachability game.}
\label{fig:reach_opt_not_sub_game_opt}
\end{figure}
	
	Consider the game of Figure~\ref{fig:reach_opt_not_sub_game_opt}: it is a
	reachability game, that is if it loops indefinitely on $q_0$, the value is 0.
	The value of the state $q_0$ is $1/2$, it is achieved by a Player $\mathsf{A} $
	positional strategy playing the two top rows with probability $1/2$ and by a
	Player $\mathsf{B} $ positional strategy playing the two columns with probability $1/2$. 
	
	However, denoting $a_1,a_2$ and $a_3$ the three actions available to Player
	$\mathsf{A} $ at state $q_0$ from top to bottom, consider the following Player $\mathsf{A} $
	strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $ such that $\ensuremath{\mathsf{s}}_\mathsf{A} (q_0)(a_1) = \ensuremath{\mathsf{s}}_\mathsf{A} (q_0)(a_2) := 1/2$ and
	$\ensuremath{\mathsf{s}}_\mathsf{A} (q_0^{n+1})(a_3) := 1$ for all $n \geq 1$. Then, this strategy is locally
	optimal and it is optimal. Indeed, if the game loops at least once on $q_0$,
	then there was the same probability to loop on $q_0$ and to reach outcome 1.
	Hence, the mean of the values is at least $1/2$ which is the value of the state
	$q_0$. However, it is not subgame optimal since after the game loops once on
	$q_0$, then Player $\mathsf{B} $ can ensure value 0 by playing indefinitely the left
	column with probability 1. 
	
	Similarly, consider a Player $\mathsf{A} $ strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $ such that $\ensuremath{\mathsf{s}}_\mathsf{A} (q_0)(a_1) =
	\ensuremath{\mathsf{s}}_\mathsf{A} (q_0)(a_2) := 1/4$, $\ensuremath{\mathsf{s}}_\mathsf{A} (q_0)(a_3) := 1/2$ and $\ensuremath{\mathsf{s}}_\mathsf{A} (q_0^{n+1})(a_3) :=
	1$ for all $n \geq 1$. Then, this strategy is locally optimal and
	positively-optimal, however it is not optimal since the value of this strategy
	is $1/4$, which can be enforced by Player $\mathsf{B} $ by playing indefinitely the left
	column with probability 1.
	
	\ensuremath{\mathsf{s}}ubsection{Formal definition of the new games}
	\label{subsec:game_value_one_everywhere}
	\ensuremath{\mathsf{s}}ubsubsection{Game where all states have value 1}
	\begin{proposition}
		\label{prop:G_W}
		Consider a PI objective $\emptyset \ensuremath{\mathsf{s}}ubsetneq W \ensuremath{\mathsf{s}}ubseteq \mathsf{K} ^\omega$

		. Then, there is a concurrent game $\mathcal{G} _W = \langle \mathsf{A} conc_W,W \rangle$ where
		all states have value $1$.
	\end{proposition}
	\begin{proof}
		We consider the concurrent arena $\mathsf{A} conc_W = \mathsf{A} paramConc$ where Player $\mathsf{A} $
		can choose alone the sequence of states seen among states of colors in
		$\mathsf{K} $, that is:
		\begin{itemize}
			\item $Q := \mathsf{K} $, for all $q \in Q$, we have $A_q := \mathsf{K} $ and $B_q :=
			\{ b \}$;
			\item $\mathsf{D}  := \{ d_q \mid q \in Q \}$ and for all $q \in Q$, we have
			$\mathsf{dist} (d_q)(q) = 1$;
			\item For all $q \in Q$ and $q' \in A_q = \mathsf{K} $, we have $\delta(q,q',b)
			:= d_{q'}$;
			\item for all $q \in Q$, we have $\mathsf{col} (q) := q$.
		\end{itemize}
		This game is in fact turn-based since only Player $\mathsf{A} $'s actions affect the
		sequence of states. She can decide exactly the sequence of states -- and colors
		-- that is seen. Hence, she can follow exactly a path $\rho \in W$ (except for
		the first color, which does not matter since $W$ is prefix-independent), hence
		the values of states are 1.
	\end{proof}
	
	\ensuremath{\mathsf{s}}ubsubsection{The definition of the game $\mathcal{G} _u$}
	\begin{definition}
		\label{def:game_g_u}

		For a positive value $u \in V_{\mathcal{G} } \ensuremath{\mathsf{s}}etminus \{ 0 \}$, we define the game
		$\mathcal{G} _u = \mathcal{G} ames{\mathsf{A} conc_u}{W}$ with $\mathsf{A} conc_u = \langle Q'_u,(A'_q)_{q \in
			Q'_u},(B'_q)_{q \in Q'_u},\mathsf{D} ,\delta',\mathsf{dist} ',\mathsf{K} ,\mathsf{col} 
		\rangle$ where we refer to the arena $\mathsf{A} conc_W$ as a sink state to which there
		are some transitions:
		\begin{itemize}
			\item $Q := Q_u \cup \mathsf{A} conc_W$;
			\item For all $q \in Q_u$, we have $A'_q := A_{\mathcal{F}^\mathsf{nf}_q}$ and $B'_q := B_q$;
			\item $\mathsf{D} ' := \{ d_{q,\ensuremath{\mathsf{s}}igma_q,b} \mid q \in Q_u,\; \ensuremath{\mathsf{s}}igma_q \in
			A_q, b \in B \}$;
			\item For all $q \in Q_u$ and $\ensuremath{\mathsf{s}}igma_q \in A_q = S_{\mathcal{F}^\mathsf{nf}_q}$ we have:
			$\delta'(q,\ensuremath{\mathsf{s}}igma_q,b) := d_{q,\ensuremath{\mathsf{s}}igma_q,b}$;
			\item For all $q \in Q_u,\; \ensuremath{\mathsf{s}}igma_q = \ensuremath{\mathsf{s}}um_{a \in A} \ensuremath{\mathsf{s}}igma_q(a) \cdot
			\mathds{1}_{\{ a \}} \in A'_q$, $b \in B'_q$ and $q' \in Q$, we have:
			\begin{displaymath}
			\mathsf{dist} '(d_{q,\ensuremath{\mathsf{s}}igma_q,b})(q') := 
			\begin{cases}
			\ensuremath{\mathsf{s}}um_{a \in A} \ensuremath{\mathsf{s}}igma_q(a) \cdot \mathsf{dist} (\delta(q,a,b))(q') & \text{ if
			} q' \in Q_u\\
			\ensuremath{\mathsf{s}}um_{a \in A} \ensuremath{\mathsf{s}}igma_q(a) \cdot \mathsf{dist} (\delta(q,a,b))[Q \ensuremath{\mathsf{s}}etminus Q_u]
			& \text{ if } q' = \mathsf{A} conc_W\\
			\end{cases}
			\end{displaymath}
		\end{itemize}

	\end{definition}

	
	

	

	
	

	
	\ensuremath{\mathsf{s}}ubsection{Proof of Lemma~\ref{lem:value_one_Gu}}
	\label{proof:lem_value_one_Gu}

	In fact we show a stronger result.
	\begin{lemma}
		Consider some $u \in V_{\mathcal{G} } \ensuremath{\mathsf{s}}etminus \{ 0 \}$ and the game $\mathcal{G} _u$. Consider
		also the objective (that is not prefix-independent) $W_u := W \cup Q^* \cdot (Q
		\ensuremath{\mathsf{s}}etminus Q_u) \cdot Q^\omega \ensuremath{\mathsf{s}}ubseteq Q^\omega$ and assume that there exists,
		in $\mathcal{G} $ a locally optimal strategy that is positively-optimal w.r.t. the
		objective $W_u$ from all states in $Q_u$. Then, the values of all states in
		$\mathcal{G} _u$ is positive: $\MarVal{\mathcal{G} _u}(q) > 0$, for all $q$ in $\mathcal{G} _u$.
		\label{lem:value_one_qualitatively_Gu}
	\end{lemma}
	The proof of this lemma is quite straightforward but it is quite long. It is
	due to how the game $\mathcal{G} _u$ is formally defined.
	\begin{proof}
		First, note that all the values of all states in $\mathcal{G} _u$ w.r.t. the objective
		$W_u$ are at least $u$ since $W \ensuremath{\mathsf{s}}ubseteq W_u$. Let us now consider such a
		locally optimal strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $ that is positively-optimal w.r.t. the objective
		$W_u$ from all states in $Q_u$ and let $r = \min_{q \in Q_u}
		\MarVal{\mathcal{G} ames{\mathsf{A} conc}{W_u}}[\ensuremath{\mathsf{s}}_\mathsf{A} ](q) > 0$ be the minimum of the values of the
		strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $ in $Q_u$ w.r.t. the objective $Q_u$. 
		Let us assume that one state $q \in Q_u$ has value 0 in the game $\mathcal{G} _u$
		(w.r.t. to the objective $W$) and consider a Player $\mathsf{B} $ strategy $\ensuremath{\mathsf{s}}_\mathsf{B} $ whose
		value in the game $\mathcal{G} _u$ is at most $r/2 > 0$ from the state $q$: i.e.
		$\MarVal{\mathcal{G} _u}[\ensuremath{\mathsf{s}}_\mathsf{B} ](q) \leq r/2$ w.r.t. $W$. Note that the Player $\mathsf{B} $
		strategy $\ensuremath{\mathsf{s}}_\mathsf{B} $ is a strategy in $\mathsf{A} conc$ and in $\mathsf{A} conc_u$. 

		For all $\rho = \rho' \cdot q \in (Q_u)^+$, we can write $\ensuremath{\mathsf{s}}_\mathsf{A} (\rho)$ as a
		convex combination of elements in $A'_q$: $\ensuremath{\mathsf{s}}_\mathsf{A} (\rho) = \ensuremath{\mathsf{s}}um_{\ensuremath{\mathsf{s}}igma \in A'_q}
		\mu_{\ensuremath{\mathsf{s}}igma}(\rho) \cdot \ensuremath{\mathsf{s}}igma$. Let us now define the Player $\mathsf{A} $ strategy
		$\ensuremath{\mathsf{s}}_\mathsf{A} '$ in the game $\mathcal{G} _u$ that mimics the strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $, i.e. for all $\rho
		= \rho' \cdot q \in (Q_u)^+$ and $\ensuremath{\mathsf{s}}igma \in A'_q$, we set:
		$\ensuremath{\mathsf{s}}_\mathsf{A} '(\rho)(\ensuremath{\mathsf{s}}igma) := \mu_{\ensuremath{\mathsf{s}}igma}(\rho)$. When the game enters $\mathsf{A} conc_W$,
		the strategy $\ensuremath{\mathsf{s}}_\mathsf{A} '$ switches to a sure strategy. Hence, since the objective
		$W$ is prefix-independent, for all $\rho \in (Q_u)^* \cdot \mathsf{A} conc_W$, we have
		$\MarVal{\mathcal{G} _u}(\ensuremath{\mathsf{s}}_\mathsf{A} ')(\rho) = 1$. We denote by $\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }$ the
		probability measure induced by strategies $\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} $ in $\mathcal{G} $ from state $q$
		and by $\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ',\ensuremath{\mathsf{s}}_\mathsf{B} ,u}$ the probability measure induced by
		$\ensuremath{\mathsf{s}}_\mathsf{A} ',\ensuremath{\mathsf{s}}_\mathsf{B} $ in $\mathcal{G} _u$ from state $q$. 
		
		Let us now show by induction on $n$ the property $\mathcal{P}(n)$:

		for all $\rho \in (Q_u)^n$, we have $\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(\rho) =
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ',\ensuremath{\mathsf{s}}_\mathsf{B} ,u}(\rho)$ and $\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(Q_u^{\leq n}
		\cdot (Q \ensuremath{\mathsf{s}}etminus Q_u)) = \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ',\ensuremath{\mathsf{s}}_\mathsf{B} ,u}(Q_u^{\leq n} \cdot
		\mathsf{A} conc_W)$. This straightforwardly holds for $n = 1$. Assume now that this holds
		for some $n-1 \geq 0$. Consider some $\rho = \rho' \cdot q = \rho'' \cdot q'
		\cdot q \in (Q_u)^n \cdot Q$. We have:
		\begin{align*}
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(\rho) & = \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(\rho') \cdot
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }_{\rho'}(q) \\
		& = \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} ,u}(\rho') \cdot \left( \ensuremath{\mathsf{s}}um_{a \in A} \ensuremath{\mathsf{s}}um_{b \in
			B} \ensuremath{\mathsf{s}}_\mathsf{A} (\rho')(a) \cdot \ensuremath{\mathsf{s}}_\mathsf{B} (\rho')(b) \cdot \mathsf{dist} (\delta(q',a,b))(q)
		\right) \\
		& = \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} ,u}(\rho') \cdot \ensuremath{\mathsf{s}}um_{b \in B}  \ensuremath{\mathsf{s}}_\mathsf{B} (\rho')(b)
		\cdot \left( \ensuremath{\mathsf{s}}um_{a \in A} \ensuremath{\mathsf{s}}_\mathsf{A} (\rho')(a) \cdot 
		\mathsf{dist} (\delta(q',a,b))(q) \right) \\
		& = \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} ,u}(\rho') \cdot \ensuremath{\mathsf{s}}um_{b \in B}  \ensuremath{\mathsf{s}}_\mathsf{B} (\rho')(b)
		\cdot \left( \ensuremath{\mathsf{s}}um_{a \in A} \ensuremath{\mathsf{s}}um_{\ensuremath{\mathsf{s}}igma \in A'_q} \mu_{\ensuremath{\mathsf{s}}igma}(\rho') \cdot
		\ensuremath{\mathsf{s}}igma(a) \cdot  \mathsf{dist} (\delta(q',a,b))(q) \right) \\
		& = \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} ,u}(\rho') \cdot \ensuremath{\mathsf{s}}um_{b \in B}  \ensuremath{\mathsf{s}}_\mathsf{B} (\rho')(b)
		\cdot \left( \ensuremath{\mathsf{s}}um_{\ensuremath{\mathsf{s}}igma \in A'_q} \mu_{\ensuremath{\mathsf{s}}igma}(\rho') \cdot \ensuremath{\mathsf{s}}um_{a \in A}
		\ensuremath{\mathsf{s}}igma(a) \cdot  \mathsf{dist} (\delta(q',a,b))(q) \right) 
		\end{align*}
		If $q \in Q_u$, we obtain:
		\begin{align*}
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(\rho) & = \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} ,u}(\rho') \cdot
		\ensuremath{\mathsf{s}}um_{b \in B}  \ensuremath{\mathsf{s}}_\mathsf{B} (\rho')(b) \cdot \ensuremath{\mathsf{s}}um_{\ensuremath{\mathsf{s}}igma \in A'_q} \mu_{\ensuremath{\mathsf{s}}igma}(\rho')
		\cdot \mathsf{dist} '(d_{q'},\ensuremath{\mathsf{s}}igma_q,b)(q) \\
		& = \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} ,u}(\rho') \cdot \ensuremath{\mathsf{s}}um_{b \in B}  \ensuremath{\mathsf{s}}_\mathsf{B} (\rho')(b)
		\cdot \ensuremath{\mathsf{s}}um_{\ensuremath{\mathsf{s}}igma \in A'_q} \ensuremath{\mathsf{s}}_\mathsf{A} '(\rho')(\ensuremath{\mathsf{s}}igma) \cdot
		\mathsf{dist} '(d_{q'},\ensuremath{\mathsf{s}}igma,b)(q) \\
		& = \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} ,u}(\rho') \cdot \ensuremath{\mathsf{s}}um_{\ensuremath{\mathsf{s}}igma \in A'_q}  \ensuremath{\mathsf{s}}um_{b
			\in B} \ensuremath{\mathsf{s}}_\mathsf{A} '(\rho')(\ensuremath{\mathsf{s}}igma) \cdot \ensuremath{\mathsf{s}}_\mathsf{B} (\rho')(b) \cdot
		\mathsf{dist} '(\delta'(q',\ensuremath{\mathsf{s}}igma,b))(q) \\
		& = \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} ,u}(\rho') \cdot
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ',\ensuremath{\mathsf{s}}_\mathsf{B} ,u}_{\rho'}(q) \\
		& = \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ',\ensuremath{\mathsf{s}}_\mathsf{B} ,u}(\rho)
		\end{align*}
		Furthermore, we have:
		\begin{align*}
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }[Q_u^n \cdot (Q \ensuremath{\mathsf{s}}etminus Q_u)] & = \ensuremath{\mathsf{s}}um_{\rho' \in
			(Q_u)^n} \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(\rho') \cdot
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }_{\rho'}[Q \ensuremath{\mathsf{s}}etminus Q_u] \\
		& = \ensuremath{\mathsf{s}}um_{\rho' \in (Q_u)^n} \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(\rho') \cdot \ensuremath{\mathsf{s}}um_{q \in
			Q \ensuremath{\mathsf{s}}etminus Q_u} \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }_{\rho'}(q) \\
		& = \ensuremath{\mathsf{s}}um_{\rho' \in (Q_u)^n} \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(\rho') \cdot \ensuremath{\mathsf{s}}um_{q \in
			Q \ensuremath{\mathsf{s}}etminus Q_u} \ensuremath{\mathsf{s}}um_{b \in B}  \ensuremath{\mathsf{s}}_\mathsf{B} (\rho')(b) \cdot \left( \ensuremath{\mathsf{s}}um_{\ensuremath{\mathsf{s}}igma \in
			A_q} \mu_{\ensuremath{\mathsf{s}}igma}(\rho') \cdot \ensuremath{\mathsf{s}}um_{a \in A} \ensuremath{\mathsf{s}}igma(a) \cdot 
		\mathsf{dist} (\delta(q',a,b))(q) \right) \\
		& = \ensuremath{\mathsf{s}}um_{\rho' \in (Q_u)^n} \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(\rho') \cdot \ensuremath{\mathsf{s}}um_{b \in
			B}  \ensuremath{\mathsf{s}}_\mathsf{B} (\rho')(b) \cdot \left( \ensuremath{\mathsf{s}}um_{\ensuremath{\mathsf{s}}igma \in A_q} \mu_{\ensuremath{\mathsf{s}}igma}(\rho') \cdot
		\ensuremath{\mathsf{s}}um_{a \in A} \ensuremath{\mathsf{s}}igma(a) \cdot  \ensuremath{\mathsf{s}}um_{q \in Q \ensuremath{\mathsf{s}}etminus Q_u} 
		\mathsf{dist} (\delta(q',a,b))(q) \right) \\
		& = \ensuremath{\mathsf{s}}um_{\rho' \in (Q_u)^n} \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(\rho') \cdot \ensuremath{\mathsf{s}}um_{b \in
			B}  \ensuremath{\mathsf{s}}_\mathsf{B} (\rho')(b) \cdot \left( \ensuremath{\mathsf{s}}um_{\ensuremath{\mathsf{s}}igma \in A_q} \mu_{\ensuremath{\mathsf{s}}igma}(\rho') \cdot
		\ensuremath{\mathsf{s}}um_{a \in A} \ensuremath{\mathsf{s}}igma(a) \cdot \mathsf{dist} (\delta(q',a,b))[Q \ensuremath{\mathsf{s}}etminus Q_u]
		\right) \\
		& = \ensuremath{\mathsf{s}}um_{\rho' \in (Q_u)^n} \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(\rho') \cdot \ensuremath{\mathsf{s}}um_{b \in
			B}  \ensuremath{\mathsf{s}}_\mathsf{B} (\rho')(b) \cdot \left( \ensuremath{\mathsf{s}}um_{\ensuremath{\mathsf{s}}igma \in A_q} \mu_{\ensuremath{\mathsf{s}}igma}(\rho') \cdot
		\mathsf{dist} '(d_{q',\ensuremath{\mathsf{s}}igma,b})[\mathsf{A} conc_W] \right) \\
		& = \ensuremath{\mathsf{s}}um_{\rho' \in (Q_u)^n} \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(\rho') \cdot
		\ensuremath{\mathsf{s}}um_{\ensuremath{\mathsf{s}}igma \in A'_q} \ensuremath{\mathsf{s}}um_{b \in B} \ensuremath{\mathsf{s}}_\mathsf{A} '(\rho')(\ensuremath{\mathsf{s}}igma) \cdot
		\ensuremath{\mathsf{s}}_\mathsf{B} (\rho')(b) \cdot \mathsf{dist} '(\delta(q',\ensuremath{\mathsf{s}}igma,b))[\mathsf{A} conc_W]  \\
		& = \ensuremath{\mathsf{s}}um_{\rho' \in (Q_u)^n} \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(\rho') \cdot
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ',\ensuremath{\mathsf{s}}_\mathsf{B} ,u}_{\rho'}[\mathsf{A} conc_W]  \\
		& = \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ',\ensuremath{\mathsf{s}}_\mathsf{B} ,u}[Q_u^n \cdot \mathsf{A} conc_W]
		\end{align*}
		
		It follows that:
		\begin{align*}
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }[(Q_u)^{\leq n} \cdot (Q \ensuremath{\mathsf{s}}etminus Q_u)] & =
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }[(Q_u)^{\leq n-1} \cdot (Q \ensuremath{\mathsf{s}}etminus Q_u)] +
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }[(Q_u)^n \cdot (Q \ensuremath{\mathsf{s}}etminus Q_u)] \\
		& = \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ',\ensuremath{\mathsf{s}}_\mathsf{B} ,u}[(Q_u)^{\leq n-1} \mathsf{A} conc_W] +
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ',\ensuremath{\mathsf{s}}_\mathsf{B} ,u}[(Q_u)^n \cdot \mathsf{A} conc_W] \\
		& = \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ',\ensuremath{\mathsf{s}}_\mathsf{B} ,u}[(Q_u)^{\leq n} \cdot \mathsf{A} conc_W]
		\end{align*}	
		Hence, $\mathcal{P}(n)$ holds. In fact, this property holds for all $n \in
		\ensuremath{\mathbb{N}}$. From this, we obtain:
		\begin{itemize}
			\item $\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }[(Q_u)^* \cdot (Q \ensuremath{\mathsf{s}}etminus Q_u)] =
			\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ',\ensuremath{\mathsf{s}}_\mathsf{B} ,u}[(Q_u)^* \cdot \mathsf{A} conc_W]$;
			\item $\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }[W \cap (Q_u)^\omega] =
			\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ',\ensuremath{\mathsf{s}}_\mathsf{B} ,u}[W \cap (Q_u)^\omega]$.
		\end{itemize}
		That is:
		\begin{align*}
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }[W_u] & = \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }[W_u \cap
		(Q_u)^\omega] + \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }[W_u \cap (Q_u)^* \cdot (Q \ensuremath{\mathsf{s}}etminus
		Q_u)] \\ 
		& = \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }[W \cap (Q_u)^\omega] +
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }[(Q_u)^* \cdot (Q \ensuremath{\mathsf{s}}etminus Q_u)] \\ 

		& = \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ',\ensuremath{\mathsf{s}}_\mathsf{B} ,u}[W \cap (Q_u)^\omega] +
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ',\ensuremath{\mathsf{s}}_\mathsf{B} ,u}[(Q_u)^* \cdot \mathsf{A} conc_W] \\
		& = \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ',\ensuremath{\mathsf{s}}_\mathsf{B} ,u}[W \cap (Q_u)^\omega] +
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ',\ensuremath{\mathsf{s}}_\mathsf{B} ,u}[W \cap (Q_u)^* \cdot \mathsf{A} conc_W] \\
		& = \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ',\ensuremath{\mathsf{s}}_\mathsf{B} ,u}[W] \leq r/2 < r
		\end{align*}
		The inequality follow by the choice of the Player $\mathsf{B} $ strategy $\ensuremath{\mathsf{s}}_\mathsf{B} $. This
		result is in contradiction with the definition of $r$: the minimum of the values
		of the states in $Q_u$ w.r.t. the strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $ and the objective $W_u$. In
		fact, there is no such state $q \in Q_u$ whose value in $\mathcal{G} _u$ is 0. 

		The lemma follows.
	\end{proof}
	
	\ensuremath{\mathsf{s}}ubsection{Proof of Lemma~\ref{prop:glued_strategy}}
	\label{proof:prop_glued_strategy}
	\begin{proof}
		We denote the strategy $\ensuremath{\mathsf{s}}_\mathsf{A} [(\ensuremath{\mathsf{s}}_\mathsf{A} ^u)_{u \in V_{\mathcal{G} } \ensuremath{\mathsf{s}}etminus \{ 0 \}}]$ by
		$\ensuremath{\mathsf{s}}_\mathsf{A} $ and we apply Theorem~\ref{thm:subgame_optimal_arbitrary_strategy} to
		show that it is subgame optimal. The strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $ is locally optimal at all
		states in $Q_u$ for all positive $u \in V_{\mathcal{G} } \ensuremath{\mathsf{s}}etminus \{ 0 \}$, by definition
		of the games $\mathcal{G} _u$. Furthermore, since the values of all states $q \in Q_0$ is
		0, the values of the game in normal form in $Q_0$ are 0. Hence, for all state $q
		\in Q_0$, any strategy in the game in normal form $\mathcal{F}_q$ is optimal in game
		in normal form $\mathcal{F}_q$. That is, the strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $ is locally optimal.
		
		Let us now show that it ensures the second property of
		Theorem~\ref{thm:subgame_optimal_arbitrary_strategy}. Let $u \in V_{\mathcal{G} }
		\ensuremath{\mathsf{s}}etminus \{ 0 \}$. Consider a deterministic Player $\mathsf{B} $ strategy $\ensuremath{\mathsf{s}}_\mathsf{B} $.
		Consider a finite path $\rho \in Q^+$ and $\pi = \pi' \cdot q \in Q^* \cdot
		Q_u$. Assume that $\mathbb{P}_{\rho \cdot \pi}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }((Q_u)^\omega) > 0$.
		Then, we have $\mathbb{P}_{\rho \cdot \pi}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(W \mid (Q_u)^\omega) =
		1$ since the strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $ then behaves like $\ensuremath{\mathsf{s}}_\mathsf{A} ^u$ and this holds for
		$\ensuremath{\mathsf{s}}_\mathsf{A} ^u$ (as it is subgame almost-surely winning in $\mathcal{G} _u$ and the objective
		$W$ is prefix-independent). That is, $\mathbb{P}_{\rho \cdot
			\pi}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(W \cap (Q_u)^\omega) = \mathbb{P}_{\rho \cdot
			\pi}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }((Q_u)^\omega)$. As this holds for all $\pi \in Q^* \cdot
		Q_u$, it follows that $\mathbb{P}_{\rho}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(W \cap Q^* \cdot
		(Q_u)^\omega) = \mathbb{P}_{\rho}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(Q^* \cdot (Q_u)^\omega)$. 
		
		We can then apply Theorem~\ref{thm:subgame_optimal_arbitrary_strategy} to
		obtain the theorem.
	\end{proof}
	
	
	\ensuremath{\mathsf{s}}ubsection{Extension to finite memory}
	\label{appen:extension_finite_memory}
	We first recall what is a memory skeleton (see, for
	instance,~\cite{DBLP:conf/concur/Bouyer0ORV20}) and we see how it
	can implement finite-memory strategies. For a set of colors $\mathsf{K} $
	and a set of states $Q$, a memory skeleton on $\mathsf{K} $ is a triple
	$\mathcal{M} = \langle M,m_{\text{\upshape init}},\mu \rangle$, where $M$ is a non-empty
	set called the memory, $m_{\text{\upshape init}} \in M$ is the initial state of the
	memory and $\mu: M \times \mathsf{K}  \rightarrow M$ is the update
	function. Note that the update function $\mu$ can be extended inductively into
	a function $\mu^*: M \times \mathsf{K} ^* \rightarrow M$ in the following way: for
	all $m \in M$, $\mu^*(m,\epsilon) := m$ and for all $\rho \cdot k \in
	\mathsf{K} ^+$, $\mu^*(m,\rho \cdot k) := \mu(\mu^*(m,\rho),k)$. Given some set of
	actions $A_q$ for each $q \in Q$, an action map with memory $M$ is a function
	$\lambda: M \times Q \rightarrow \mathcal{D} (\cup_{q \in Q} A_q)$  such that for all
	$q \in Q$ and $m \in M$ we have $\lambda(m,q) \in \mathcal{D} (A_q)$. In fact, a memory
	skeleton and an action map implement a strategy.
	
	\begin{definition}[Implementation of finite memory strategies]
		Consider a concurrent arena $\mathsf{A} conc$ on a set of colors $\mathsf{K} $. A memory
		skeleton	$\mathcal{M} = \langle M,m_{\text{\upshape init}},\mu \rangle$ on $\mathsf{K} $ and an action
		map $\lambda: M \times Q \rightarrow \mathcal{D} (\cup_{q \in Q} A_q)$ implement the
		strategy $\ensuremath{\mathsf{s}}_\mathsf{A} : Q^+ \rightarrow \mathcal{D} (\cup_{q \in A_q} A_q)$ that is
		defined by, for all $\rho = \rho' \cdot q \in Q^+$, $\ensuremath{\mathsf{s}}_\mathsf{A} (\rho) :=
		\lambda(\mu^*(m_{\text{\upshape init}},\mathsf{col} (\rho)),q) \in \mathcal{D} (A_q)$.
		
		A strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $ is \emph{finite memory} if there exists a memory
		skeleton $\mathcal{M} = \langle M,m_{\text{\upshape init}},\mu \rangle$, with $M$
		finite, and an action map $\lambda$ implementing $\ensuremath{\mathsf{s}}_\mathsf{A} $. If $M$ is a
		singleton, we retrieve the definition of positional strategies.
	\end{definition}
	
	We can extend the definition positionaly almost-surely winnable objective to
	objective winnable with a fixed memory skeleton.
	\begin{definition}[$\mathcal{M}$-almost-surely winnable objective]
		Consider an Borel prefix-independent objective $W \ensuremath{\mathsf{s}}ubseteq \mathsf{K} ^\omega$ on
		a set of colors $\mathsf{K} $ and a memory skeleton $\mathcal{M}$. It is
		$\mathcal{M}$-\emph{almost-surely winnable} ($\mathcal{M}$-\textsf{ASW} for
		short) if in all finite games $\mathcal{G}  = \mathcal{G} ames{\mathsf{A} conc}{W}$ on the set of colors
		$\mathsf{K} $, if there is a subgame almost-surely winning strategy, then there is
		one that can be implemented with $\mathcal{M}$.
	\end{definition}
	
	We now adapt Theorem~\ref{thm:transfer_memory} to the transfer of
	finite-memory.
	\begin{theorem}
		Consider a non-empty finite set of colors $K$ and a PI objective $\emptyset
		\ensuremath{\mathsf{s}}ubsetneq W \ensuremath{\mathsf{s}}ubseteq \mathsf{K} ^\omega$. Consider a PI concurrent game $\mathcal{G} $ with
		objective $W$. For some memory skeleton $\mathcal{M}$, if the objective $W$ is
		$\mathcal{M}$-\textsf{ASW} and if there is a subgame optimal strategy in $\mathcal{G} $
		then there is one that can be implemented by $\mathcal{M}$.
		\label{thm:transfer_finite_memory}
	\end{theorem}
	
	Let us define the set of relevant memory states of a given memory skeleton
	$\mathcal{M}$, that is the subset of memory states that could occur from
	$m_{\text{\upshape init}}$ given any finite sequence of colors. That is:
	\begin{definition}[Relevant memory states]
		Consider a memory skeleton $\mathcal{M} = \langle M,m_{\text{\upshape init}},\mu \rangle$ on a
		set of colors $\mathsf{K} $. The set of \emph{relevant memory states} $M_r \ensuremath{\mathsf{s}}ubseteq
		M$ is defined as $M_r := \{ m \in M \mid \exists \rho \in \mathsf{K} ^*,\; m =
		\mu^*(m_{\text{\upshape init}},\rho) \}$. For all such relevant states $m \in M_r$, we denote by
		$\mathcal{M}^m$ the memory skeleton $\mathcal{M}^m := \langle M,m,\mu \rangle$.
	\end{definition}
	
	Then, we have the following proposition:
	\begin{proposition}
		Consider a set of colors $\mathsf{K} $, a memory skeleton $\mathcal{M} = \langle
		M,m_{\text{\upshape init}},\mu \rangle$ on $\mathsf{K} $ and the corresponding set of relevant memory
		states $M_r$. Consider also a $\mathcal{M}$-\textsf{ASW} objective $W \ensuremath{\mathsf{s}}ubseteq
		K^\omega$. Then, for all finite games $\mathcal{G}  = \mathcal{G} ames{\mathsf{A} conc}{W}$ on the set of
		colors $\mathsf{K} $ where there is a subgame almost-surely winning strategy, there
		is an action map $\lambda: M \times Q \rightarrow \mathcal{D} (\cup_{q \in Q} A_q)$
		such that, for all relevant states $m \in M_r$, the strategy implemented by
		$\mathcal{M}^m$ and $\lambda$ is subgame almost-surely winning in $\mathcal{G} $.
		\label{prop:sub_game_optimal_from_every_memory_state}
	\end{proposition}
	\begin{proof}
		Consider a set of colors $\mathsf{K} $, a memory skeleton $\mathcal{M} = \langle
		M,m_{\text{\upshape init}},\mu \rangle$ on $\mathsf{K} $ and the corresponding set of relevant memory
		states $M_r$. Consider also a $\mathcal{M}$-\textsf{ASW} objectives $W \ensuremath{\mathsf{s}}ubseteq
		K^\omega$. Consider also a finite game $\mathcal{G}  = \mathcal{G} ames{\mathsf{A} conc}{W}$ on the set of
		colors $\mathsf{K} $ where there is a subgame almost-surely winning strategy. Let us
		build a game $\mathcal{G} ^\mathsf{B} $ where Player $\mathsf{B} $ first plays for finite number of rounds
		to 'choose' the memory state of the Player $\mathsf{A} $ strategy, and then the game
		proceeds as in $\mathcal{G} $. More specifically, for $n := |M_r|$ and denoting $Q$ the
		set of states in $\mathcal{G} $, we consider the finite arena $\mathsf{A} conc^\mathsf{B}  = \langle
		Q^\mathsf{B} ,(A_q)_{q \in Q^\mathsf{B} },(B_q)_{q \in
			Q^\mathsf{B} },\mathsf{D} ,\delta,\mathsf{dist} ,\mathsf{K} ,\mathsf{col}  \rangle$ defined in the
		following way:
		\begin{itemize}
			\item $Q^\mathsf{B}  := \mathsf{K}  \times \{ 0,\ldots,n \}$ the set of states where only
			Player $\mathsf{B} $ will play;
			\item For all $q = (k,i) \in Q^\mathsf{B} $, we have $A'_q := \{ a \}$ for an
			arbitrary action $a$ and $B_q := \mathsf{Cont}_q \uplus \mathsf{Exit}_q$ with
			$\mathsf{Cont}_q := \{ b_{k,i+1} \mid k \in \mathsf{K}  \}$ if $i < n$ and
			$\mathsf{Cont}_q := \emptyset$ otherwise. Furthermore, $\mathsf{Exit}_q := \{
			b_{q'} \mid q' \in Q \}$;
			\item $\mathsf{D}  := \{ d_{k,i+1} \mid k \in \mathsf{K} ,\; 0 \leq i \leq n-1 \}
			\uplus \{ d_{q'} \mid q' \in Q \}$;
			\item For all $q = (k,i) \in Q^\mathsf{B} $ and $k \in \mathsf{K} $ we have:
			$\delta(q,a,b_{k,i+1}) := d_{k,i+1}$ and for all $q' \in Q$, we have
			$\delta(q,a,b_{q'}) := d_{q'}$;
			\item For all $k \in \mathsf{K} $ and $0 \leq i \leq n-1$, we have
			$\mathsf{dist} (d_{k,i+1})((k,i+1)) := 1$ and for all $q \in Q$
			$\mathsf{dist} (d_{q})(q) := 1$;
			\item For all $k \in \mathsf{K} $ and $0 \leq i \leq n$, we have $\mathsf{col} ((k,i))
			:= k$.
		\end{itemize}
		The arena $\mathsf{A} conc^\mathsf{B} $ is plugged in before the arena $\mathsf{A} conc$ (thus obtaining
		the arena $\mathsf{A} conc^\mathsf{B}  \cdot \mathsf{A} conc$) and eventually enters this arena $\mathsf{A} conc$
		via the Nature states $d_{q}$ for $q \in Q$ (which have to be chosen at some
		point: there are the only successors of the states $(k,n)$ for all $k \in
		\mathsf{K} $). We claim that there is still a subgame almost-surely winning strategy
		in the game $\mathcal{G} ^\mathsf{B}  := \langle \mathsf{A} conc^\mathsf{B}  \cdot \mathsf{A} conc,W \rangle$. This is due to
		the fact that it was the case of the game $\mathcal{G} $,that the objective $W$ is
		prefix-independent and that the gae can only stay in $\mathsf{A} conc^\mathsf{B} $ for a finite
		number of rounds. Hence, since the objective $W$ is
		$\mathcal{M}$-$\mathsf{ASW}$, there is an action map $\lambda: M \times Q^\mathsf{B} 
		\cup Q \rightarrow \mathcal{D} (\cup_{q \in Q^\mathsf{B}  \cup Q} A_q)$ such that the strategy
		$\ensuremath{\mathsf{s}}_\mathsf{A} $ implemented by $\mathsf{M}$ and $\lambda$ is subgame almost-surely
		winning in $\mathcal{G} ^B$. In particular, Player $\mathsf{B} $ can play in the arena $\mathsf{A} conc^\mathsf{B} $
		such that, when she leaves it to 'start the game $\mathcal{G} $', it can be done with the
		memory state of the Player $\mathsf{A} $ strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $ is an arbitrary relevant memory
		state $m \in M_r$. (Note that indeed Player $\mathsf{B} $ can reach any relevant memory
		state because the memory skeleton $\langle M_r,m_{\text{\upshape init}},\mu \rangle$ can be seen
		as a strongly connected graph of size $|M_r| = n$.) That is, for all relevant
		memory states $m \in M_r$ such that there exists a finite sequence $\rho \in
		\mathsf{K} ^k$ for $k \leq n+1$ of colors such that $m = \mu^*(m_{\text{\upshape init}},\rho)$, the
		strategy implemented by $\mathcal{M}^m$ and $\lambda$ is in fact the residual
		strategy $\ensuremath{\mathsf{s}}_\mathsf{A} ^{(\rho_0,0) \cdots (\rho_k,k)}$, and it is also subgame optimal.
		
	\end{proof}
	
	We can now proceed to the proof of Theorem~\ref{thm:transfer_finite_memory}.
	\begin{proof}
		Consider a non-empty finite set of colors $K$ and a PI objective $\emptyset
		\ensuremath{\mathsf{s}}ubsetneq W \ensuremath{\mathsf{s}}ubseteq \mathsf{K} ^\omega$. Consider a concurrent game $\mathcal{G} $ with
		objective $W$. Assume that the objective $W$ is $\mathcal{M}$-\textsf{ASW} for
		some memory skeleton $\mathcal{M}$ and that there is a subgame optimal strategy
		in $\mathcal{G} $.
		We consider the same construction than for the proof of
		Theorem~\ref{thm:transfer_memory}. However, for all $u \in V_{\mathcal{G} } \ensuremath{\mathsf{s}}etminus \{ 0
		\}$, since there is a subgame almost-surely winning strategy in the game $\mathcal{G} _u$,
		by Proposition~\ref{prop:sub_game_optimal_from_every_memory_state}, there is an
		action map $\lambda_u: M \times Q_u \rightarrow \mathcal{D} (\cup_{q \in Q_u} A_q)$
		such that, for all relevant states $m \in M_r$, the strategy implemented by
		$\mathcal{M}^m$ and $\lambda$ is subgame almost-surely winning in $\mathcal{G} _u$. We
		then glue these strategies into the an action map $\lambda: M \times Q
		\rightarrow \mathcal{D} (\cup_{q \in Q} A_q)$ such that, for all $\rho = \rho' \cdot q
		\in Q^+$, $\lambda(m,q) := \lambda_{\MarVal{\mathcal{G} }(q)}(m,q)$, i.e. the action map
		chosen depends on the value area. We then claim that the strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $
		implemented by the memory skeleton $\mathcal{M}$ and the action map $\lambda$ is
		subgame optimal. As for the proof of Lemma~\ref{prop:glued_strategy}, this
		strategy is locally optimal. Furthermore, again as for the proof of
		Lemma~\ref{prop:glued_strategy}, let us show that it ensures the second property
		of Theorem~\ref{thm:subgame_optimal_arbitrary_strategy}. Let $u \in V_{\mathcal{G} }
		\ensuremath{\mathsf{s}}etminus \{ 0 \}$. Consider a deterministic Player $\mathsf{B} $ strategy $\ensuremath{\mathsf{s}}_\mathsf{B} $.
		Consider a finite path $\rho \in Q^+$ and $\pi = \pi' \cdot q \in Q^* \cdot
		Q_u$. Assume that $\mathbb{P}_{\rho \cdot \pi}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }((Q_u)^\omega) > 0$.
		Then, we have $\mathbb{P}_{\rho \cdot \pi}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }(W \mid (Q_u)^\omega) =
		1$ since the strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $ then behaves like $\ensuremath{\mathsf{s}}_\mathsf{A} ^u$ (implemented by
		$\mathcal{M}$ and $\lambda_u$) and this holds for $\ensuremath{\mathsf{s}}_\mathsf{A} ^u$ (as it is subgame
		almost-surely winning in $\mathcal{G} _u$ regardless of the starting relevant memory state
		and since the objective $W$ is prefix-independent). 

	\end{proof}
	
	\ensuremath{\mathsf{s}}ubsection{Retrieving the original result from \cite{GIH10}}
	\label{appen:retrieve_result_turn_based}

	

	

	
	Let us first show that 
	positively-optimal strategies that are locally optimal always exists (for a
	slightly modified objective) in a turn-based setting.
	\begin{proposition}
		Consider a turn-based game $\mathcal{G} $ (i.e. it is such that the set of states can be
		partitioned into Player $\mathsf{A} $ states $q$ where $B_q$ is a singleton and Player
		$\mathsf{B} $ states $q$ where $A_q$ is a singleton). Consider the valuation $v: Q
		\rightarrow [0,1]$ giving the value of the game from all states w.r.t. action
		strategies. Consider some value $u \in V_\mathcal{G}  \ensuremath{\mathsf{s}}etminus \{ 0 \}$ (w.r.t. the
		valuation $v$) and consider the objective (first defined in
		Lemma~\ref{lem:value_one_qualitatively_Gu}) $W_u := W \cup Q^* \cdot (Q
		\ensuremath{\mathsf{s}}etminus Q_u) \cdot Q^\omega \ensuremath{\mathsf{s}}ubseteq Q^\omega$ (where $Q_u$ is defined w.r.t.
		the valuation $v$). Then, there is a locally optimal action strategy whose value
		is positive from all states in $Q_u$.
	\end{proposition}
	\begin{proof}
		Consider a turn-based game $\mathcal{G} $ and let $Q = Q_\mathsf{A}  \uplus Q_\mathsf{B} $ where for all
		$q \in Q_\mathsf{A} $ (resp. $Q_\mathsf{B} $) we have $B_q$ (resp. $A_q$) a singleton. Consider
		some value $u \in V_\mathcal{G}  \ensuremath{\mathsf{s}}etminus \{ 0 \}$ and assume towards a contradiction
		that there is a state $q \in Q_u$ from which there is no locally optimal action
		strategy whose value is positive from $q$. Let $\mathsf{D} _{< u} \ensuremath{\mathsf{s}}ubseteq
		\mathsf{D} $ be the set of Nature states whose values is less than $u$ and let
		$x < u$ be the highest values of these Nature states. Consider the game $\mathcal{G} ' =
		\langle \mathsf{A} conc',W_u \rangle$ where the arena $\mathsf{A} conc'$ is a restriction of the
		arena $\mathsf{A} conc$ where the Player $\mathsf{A} $ actions leading to Nature states in
		$\mathsf{D} _{< u}$ are removed (i.e. Player $\mathsf{A} $ can only play locally optimal
		strategies at states in $Q_u$). By assumption, there is a state $q \in Q_u$
		whose value is 0 in that game $\mathcal{G} '$. Let $\ensuremath{\mathsf{s}}_\mathsf{B} $ be a Player $\mathsf{B} $ strategy in
		that game $\mathcal{G} '$ whose value is $(u-x)/4 > 0$ from $q$. Now consider a Player
		$\mathsf{A} $ deterministic strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $ (recall that in turn-based games
		deterministic strategies acheive the same values than arbitrary strategies, see
		for instance the explanations in Theorem 1 from
		\cite{DBLP:journals/iandc/Chatterjee0GH15}). Let us denote by $\mathsf{NLO}$
		(for non-locally-optimal) the set of finite paths ending in $Q_u$ after which
		the Player $\mathsf{A} $ deterministic strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $ is not locally optimal:
		$\mathsf{NLO} := \{ \rho = \rho' \cdot q' \in Q^* \cdot Q_u \mid
		\delta(q,\ensuremath{\mathsf{s}}_\mathsf{A} (\rho),b) \in \mathsf{D} _{< u} \}$ for $b$ the only Player $\mathsf{B} $
		action in $B_{q'}$. We can now define the Player $\mathsf{B} $ strategy $\ensuremath{\mathsf{s}}_\mathsf{B} '$ in the
		following way: it mimics the strategy $\ensuremath{\mathsf{s}}_\mathsf{B} $ while the play stays in $Q_u$ and
		no finite paths in $\mathsf{NLO}$ has been reached, when such a path is reached,

		$\ensuremath{\mathsf{s}}_\mathsf{B} '$ switches to strategy of value $(x + u)/2$ (which is possible by
		definition of $\mathsf{NLO}$). Consider now a Player $\mathsf{A} $ strategy that does
		exactly $\ensuremath{\mathsf{s}}_\mathsf{A} $ until a finite paths in $\mathsf{NLO} \cup Q^* \cdot (Q
		\ensuremath{\mathsf{s}}etminus Q_u)$ is reached and in that case, it switches to an arbitrary locally
		optimal strategy (it is therefore a strategy in the game $\mathcal{G} '$). With these
		choices, $\ensuremath{\mathsf{s}}_\mathsf{A} $ and $\ensuremath{\mathsf{s}}_\mathsf{A} '$ coincide on paths in $(Q_u \ensuremath{\mathsf{s}}etminus
		\mathsf{NLO})^*$. The strategies $\ensuremath{\mathsf{s}}_\mathsf{B} $ and $\ensuremath{\mathsf{s}}_\mathsf{B} '$ also coincide on these
		paths. Considering what happens with strategies $\ensuremath{\mathsf{s}}_\mathsf{A} '$ and $\ensuremath{\mathsf{s}}_\mathsf{B} $ -- recall
		$\ensuremath{\mathsf{s}}_\mathsf{B} $ has value at most $u-x/4$ against locally optimal strategies for the
		objective $W_u$:
		\begin{align*}
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ',\ensuremath{\mathsf{s}}_\mathsf{B} }_q[W_u] & = \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }_q[W_u \cap (Q_u
		\ensuremath{\mathsf{s}}etminus \mathsf{NLO})^\omega] + \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ',\ensuremath{\mathsf{s}}_\mathsf{B} }_q[W_u \cap (Q_u
		\ensuremath{\mathsf{s}}etminus \mathsf{NLO})^* \cdot (Q \ensuremath{\mathsf{s}}etminus Q_u)] +
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ',\ensuremath{\mathsf{s}}_\mathsf{B} }_q[W_u \cap Q_u^* \cdot \mathsf{NLO}] \\
		& = \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ',\ensuremath{\mathsf{s}}_\mathsf{B} }_q[W \cap (Q_u \ensuremath{\mathsf{s}}etminus \mathsf{NLO})^\omega] +
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ',\ensuremath{\mathsf{s}}_\mathsf{B} }_q[(Q_u \ensuremath{\mathsf{s}}etminus \mathsf{NLO})^* \cdot (Q \ensuremath{\mathsf{s}}etminus
		Q_u)] + \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ',\ensuremath{\mathsf{s}}_\mathsf{B} }_q[W_u \cap Q_u^* \cdot \mathsf{NLO}] \\
		& = \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} '}_q[W \cap (Q_u \ensuremath{\mathsf{s}}etminus \mathsf{NLO})^\omega] +
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} '}_q[(Q_u \ensuremath{\mathsf{s}}etminus \mathsf{NLO})^* \cdot (Q \ensuremath{\mathsf{s}}etminus
		Q_u)] + \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ',\ensuremath{\mathsf{s}}_\mathsf{B} }_q[W_u \cap Q_u^* \cdot \mathsf{NLO}] \\
		& \leq \frac{u-x}{4}
		\end{align*}
		It follows that $\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} '}_q[W \cap (Q_u \ensuremath{\mathsf{s}}etminus
		\mathsf{NLO})^\omega] + \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} '}_q[(Q_u \ensuremath{\mathsf{s}}etminus
		\mathsf{NLO})^* \cdot (Q \ensuremath{\mathsf{s}}etminus Q_u)] \leq \frac{u-x}{4}$. Furthermore,by
		choice of the strategy $\ensuremath{\mathsf{s}}_\mathsf{B} '$, we have $\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} '}_q[W \cap
		Q_u^* \cdot \mathsf{NLO}] \leq \frac{u+x}{2}$. We obtain:
		\begin{align*}
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} '}_q[W] & = \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }_q[W \cap (Q_u
		\ensuremath{\mathsf{s}}etminus \mathsf{NLO})^\omega] + \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} '}_q[W \cap (Q_u
		\ensuremath{\mathsf{s}}etminus \mathsf{NLO})^* \cdot (Q \ensuremath{\mathsf{s}}etminus Q_u)] +
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} '}_q[W \cap Q_u^* \cdot \mathsf{NLO}] \\
		& \leq \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }_q[W \cap (Q_u \ensuremath{\mathsf{s}}etminus \mathsf{NLO})^\omega]
		+ \mathbb{P}^{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} '}_q[(Q_u \ensuremath{\mathsf{s}}etminus \mathsf{NLO})^* \cdot (Q \ensuremath{\mathsf{s}}etminus
		Q_u)] + \frac{u+x}{2} \\
		& \leq \frac{u-x}{4} + \frac{u+x}{2} \\
		& = u - \frac{u-x}{4} < u
		\end{align*}
		Hence, all Player $\mathsf{A} $ deterministic strategies have values at most $u -
		\frac{u-x}{4} < u$. This is a contradiction with the fact that the state $q$ has
		value $u$. 
	\end{proof}
	
	We can now deduce that subgame optimal strategies always exist in turn-based
	games. Indeed, it was shown in Lemma~\ref{lem:value_one_qualitatively_Gu} that
	if, for all values $u \in V_{\mathcal{G} } \ensuremath{\mathsf{s}}etminus \{ 0 \}$, there are locally optimal
	strategies whose value is positive from all states in $Q_u$ w.r.t. the objective
	$W_u$ (which we will call assumption $H_u$), then all the states in the games
	$\mathcal{G} _u$ (from the proof of Theorem~\ref{thm:transfer_memory}) is positive. Hence,
	with a straightforward adaptation of the proof of
	Theorem~\ref{thm:transfer_memory}, one can show that this assumption $H_u$
	implies the existence of subgame optimal strategy. It follows that there always
	are subgame optimal strategies in turn-based games. 
	
	Furthermore, note that in that case there are subgame optimal deterministic
	strategies. This is due to fact that
	Theorem~\ref{thm:all_not_zero_implies_almost_sure}, when stated in turn-based
	games, ensures the existence of subgame almost-surely winning deterministic
	strategies. This is already proved in \cite{GIH10}. Our adaptation of the proof
	(which can be found in
	Appendix~\ref{proof:thm_all_not_zero_implies_almost_sure}) could also show it,
	one has just to realize that $\ensuremath{\mathsf{val}}repsilon$-optimal strategies can be found among
	deterministic strategies in turn-based games.
	
	\ensuremath{\mathsf{s}}ection{Proof of Theorem~\ref{thm:all_not_zero_implies_almost_sure}}
	\label{proof:thm_all_not_zero_implies_almost_sure}

	

	

	
	Before proceeding to the proof of
	Theorem~\ref{thm:all_not_zero_implies_almost_sure}, we need some additional
	notations and a very useful theorem. 
	
	\paragraph{Additional Notations}
	Consider a finite set $Q$. For all $\rho \in Q^*$, we denote by $\ensuremath{\mathsf{Cyl}}(\rho)
	\ensuremath{\mathsf{s}}ubseteq Q$ the set $\ensuremath{\mathsf{Cyl}}(\rho) := \{ \rho \cdot \pi \mid \pi \in Q^* \}$.
	Then, for a subset $S$ of $Q^*$, we denote by $\mathsf{Suff}(S) \ensuremath{\mathsf{s}}ubseteq Q^*$
	the set of suffixes of element of $S$,
	that is $\mathsf{Suff}(S) := \cup_{\rho \in S} \ensuremath{\mathsf{Cyl}}(\rho)$. 

	We say that a set $S \in Q^*$ is \emph{suffix-closed} if $S =
	\mathsf{Suff}(S)$. Furthermore, for all suffix-closed sets $S$ of $Q^+$, there
	is a unique set $\prefUniq{S} \ensuremath{\mathsf{s}}ubseteq S$ such that $S$ can be written as the
	following disjoint union: $S = \uplus_{\rho \in \prefUniq{S}} \ensuremath{\mathsf{Cyl}}(\rho)$ (the
	set $\prefUniq{S}$ can be defined as $\prefUniq{S} := \{ \rho \in S \mid \rho
	\text{ has no prefix in } S\}$). 

	Finally, for all finite paths $\rho = q_0 \cdots q_n \in Q^+$, we denote by
	$\ensuremath{\mathsf{head}}(\rho) \in Q$ the last state of $\rho$, i.e. $\ensuremath{\mathsf{head}}(\rho) := q_n$.
	
	Consider an PI concurrent game $\mathcal{G}  = \mathcal{G} ames{\mathsf{A} conc}{W}$, and a Player $\mathsf{A} $
	strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $. 

	Let us now define, for $u \in [0,1]$, an operator $\mathsf{ValInf}_{u}:
	\SetStrat{\mathsf{A} conc}{\mathsf{A} } \times \mathcal{P}(Q^+) \rightarrow \mathcal{P}(Q^+)$  on
	strategies that, given a strategy $\ensuremath{\mathsf{s}} \in \SetStrat{\mathsf{A} conc}{\mathsf{A} }$ and a set of
	finite paths of interest that is prefix-closed $S \in \mathcal{P}(Q^+)$,

	associates the set of finite paths $\rho$ whose value, w.r.t. the residual
	strategy $\ensuremath{\mathsf{s}}^{\rho}$ is less than $\frac{1}{2}$. That is,
	$\mathsf{ValInf}_{u}(\ensuremath{\mathsf{s}},S) := \{ \rho \in S \mid \MarVal{\mathcal{G} }[\ensuremath{\mathsf{s}}^\rho](\rho) < u
	\}$. 
	

	
	\begin{proof}
		For all states $q \in Q$, we denote by $\ensuremath{\mathsf{s}}_q: Q^+ \rightarrow \mathcal{D} (A) \in
		\SetStrat{\mathsf{A} conc}{\mathsf{A} }$ a Player $\mathsf{A} $ strategy whose value from the state $q$ is
		at least $c \cdot (1 - c/4)$ (i.e. 
		$\MarVal{\mathcal{G} }[\ensuremath{\mathsf{s}}_q](q) \geq c \cdot (1 - c/4)$). Now, let $q_0 \in Q$ be a
		state and let us exhibit an almost-surely winning strategy from $q_0$. We build
		inductively a sequence of strategies $(\ensuremath{\mathsf{s}}_n)_{n \in \ensuremath{\mathbb{N}}} \in
		(\SetStrat{\mathsf{A} conc}{\mathsf{A} })^\ensuremath{\mathbb{N}}$ and a sequence of sets of finite paths $(S_n)_{n \in
			\ensuremath{\mathbb{N}}} \in (\mathcal{P}(Q^+))^\ensuremath{\mathbb{N}}$ ensuring the following properties, for all $n \in
		\ensuremath{\mathbb{N}}$:
		\begin{itemize}
			\item[(a)] $S_{n}$ is suffix-closed;
			\item[(b)] $S_{n} \ensuremath{\mathsf{s}}ubseteq S_{n-1}$ and $S_n \cap \prefUniq{S_{n-1}} =
			\emptyset$;

			\item[(c)] for all $k < n$, $\ensuremath{\mathsf{s}}_n$ coincides with $\ensuremath{\mathsf{s}}_k$ on $Q^+ \ensuremath{\mathsf{s}}etminus
			S_{k+1}$;
			\item[(d)] for all $\rho \in \prefUniq{S_n}$, the value of the residual
			strategy $\ensuremath{\mathsf{s}}_n$ in $\rho$ is at least $c \cdot (1 - c/4)$, i.e.
			$\MarVal{\mathcal{G} }[\ensuremath{\mathsf{s}}_n^\rho](\rho) \geq c \cdot (1 - c/4)$

		\end{itemize}
		

		
		Initially, we set $\ensuremath{\mathsf{s}}_0 := \ensuremath{\mathsf{s}}_{q_0}$ and $S_0 := q_0 \cdot Q^+$. Note that it
		is indeed suffix-closed, thus satisfying property $(a)$ and, since
		$\prefUniq{S_0} = \{ q_0 \}$, property $(d)$ is also ensured. Then, assume that
		for some $n \geq 1$, for all $k \leq n-1$, $s_k \in \SetStrat{\mathsf{A} conc}{\mathsf{A} }$ and
		$S_k \ensuremath{\mathsf{s}}ubseteq Q^+$ are defined and properties $(a)-(d)$ hold. Let us define
		$s_{n}$ and $S_{n}$. If $S_{n-1} = \emptyset$, then $S_{n} := S_{n-1}$ and
		$\ensuremath{\mathsf{s}}_{n} := \ensuremath{\mathsf{s}}_{n-1}$ (and properties $(a)-(d)$ are ensured). 
		
		Now assume that $S_{n-1} \neq \emptyset$. Let us first define $S_n \ensuremath{\mathsf{s}}ubseteq
		Q^*$ and show that it satisfies properties $(a)-(b)$. Let $V_{n-1} =
		\mathsf{ValInf}_{c \cdot \frac{1}{2}}(\ensuremath{\mathsf{s}}_{n-1},S_{n-1}) \ensuremath{\mathsf{s}}ubseteq S_{n-1}$ be
		the set of finite paths of $S_{n-1}$ where the value of the residual strategy of
		$s_{n-1}$ is less than $c \cdot \frac{1}{2}$. Then, we define $S_{n} \ensuremath{\mathsf{s}}ubseteq
		Q^+$ as the set of suffixes of $V_{n-1}$: $S_{n} := \mathsf{Suff}(V_{n-1})$. In
		particular, note that $\prefUniq{S_{n}} = \prefUniq{V_{n-1}}$. 

		Clearly, $S_n$ is suffix-closed, hence property $(a)$ is ensured. 
		
		Consider now property $(b)$. We have $S_n = \mathsf{Suff}(V_{n-1}) \ensuremath{\mathsf{s}}ubseteq
		\mathsf{Suff}(S_{n-1}) = S_{n-1}$ since $V_{n-1} \ensuremath{\mathsf{s}}ubseteq S_{n-1}$ and
		$S_{n-1}$ is suffix-closed. 

		In addition, consider a path $\rho \in \prefUniq{S_{n-1}} \neq \emptyset$

		. Assume towards a contradiction that $\rho \in S_{n} =
		\mathsf{Suff}(V_{n-1})$. Then, there is some $\rho' \in V_{n-1} \ensuremath{\mathsf{s}}ubseteq
		S_{n-1}$ such that $\rho \in \ensuremath{\mathsf{Cyl}}(\rho')$. Since $\rho' \in S_{n-1}$, there
		would be some $\rho'' \in \prefUniq{S_{n-1}}$ such that $\rho' \in
		\ensuremath{\mathsf{Cyl}}(\rho'')$, and hence $\rho \in \ensuremath{\mathsf{Cyl}}(\rho'')$. We obtain that $\rho \in
		\ensuremath{\mathsf{Cyl}}(\rho) \cap \ensuremath{\mathsf{Cyl}}(\rho'')$ with $\rho,\rho'' \in \prefUniq{S_{n-1}}$. By
		definition, this implies $\rho = \rho'' $ and $\rho' \in \ensuremath{\mathsf{Cyl}}(\rho)$. That is,
		$\rho = \rho' \in V_{n-1}$. However, by property $(d)$ at index $n-1$, we have
		$\MarVal{\mathcal{G} }[\ensuremath{\mathsf{s}}_{n-1}^\rho](\ensuremath{\mathsf{head}}(\rho)) \geq c \cdot (1 - c/4) > c/2$ and hence
		$\rho \notin V_{n-1}$. Hence the contradiction. In fact, $\rho \notin S_{n}$ and
		property $(b)$ is ensured.
		

		

		
		Let us now define the strategy $\ensuremath{\mathsf{s}}_n: Q^+ \rightarrow \mathcal{D} (A)$. We set:
		\begin{itemize}
			\item $\restr{\ensuremath{\mathsf{s}}_n}{Q^+ \ensuremath{\mathsf{s}}etminus S_n} := \ensuremath{\mathsf{s}}_{n-1}$;
			\item for all $\rho \in \prefUniq{V_{n-1}} = \prefUniq{S_n}$, we have
			$\ensuremath{\mathsf{s}}_n^\rho := \ensuremath{\mathsf{s}}_\mathsf{head(\rho)}$.
		\end{itemize} 
		Let us show that this definition ensures properties $(c)-(d)$. Let $k \leq
		n-1$. Then, $\ensuremath{\mathsf{s}}_k$ coincides with $\ensuremath{\mathsf{s}}_{n-1}$ on $Q^+ \ensuremath{\mathsf{s}}etminus S_{k+1} \ensuremath{\mathsf{s}}ubseteq
		Q^+ \ensuremath{\mathsf{s}}etminus S_n$. Hence, $\ensuremath{\mathsf{s}}_k$ also coincides with $\ensuremath{\mathsf{s}}_n$ on $Q^+ \ensuremath{\mathsf{s}}etminus
		S_{k+1}$. Furthermore, $\ensuremath{\mathsf{s}}_{n-1}$ coincides with $\ensuremath{\mathsf{s}}_{n}$ on $Q^+ \ensuremath{\mathsf{s}}etminus
		S_{n}$. Hence, property $(c)$ holds. Finally, since $W$ is a prefix-independent
		objective, for all $\rho \in \prefUniq{S_n}$ and $q := \ensuremath{\mathsf{head}}(\rho) \in Q$, we
		have  $\MarVal{\mathcal{G} }[\ensuremath{\mathsf{s}}_n^\rho](\ensuremath{\mathsf{head}}(\rho)) = \MarVal{\mathcal{G} }[\ensuremath{\mathsf{s}}_q](q) \geq c \cdot
		(1 - c/4)$. That is, property $(d)$ holds. 
		

		

		
		This concludes the inductive definitions of the sequences $(\ensuremath{\mathsf{s}}_n)_{n \in \ensuremath{\mathbb{N}}}
		\in (\SetStrat{\mathsf{A} conc}{\mathsf{A} })^\ensuremath{\mathbb{N}}$ and $(S_n)_{n \in \ensuremath{\mathbb{N}}} \in
		(\mathcal{P}(Q^+))^\ensuremath{\mathbb{N}}$. We can then define the strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $ as the limit of
		the strategies $\ensuremath{\mathsf{s}}_n$. That is, if at some point $S_n = \emptyset$  and $\ensuremath{\mathsf{s}}_n =
		\ensuremath{\mathsf{s}}_{n + k}$ for all $k \geq 0$, then we set $\ensuremath{\mathsf{s}}_\mathsf{A}  := \ensuremath{\mathsf{s}}_n$. Otherwise, note
		that by property $(b)$ we have $\cap_{n \in \ensuremath{\mathbb{N}}} S_n = \emptyset$. Indeed,
		consider a finite path $\rho \in \cap_{n \in \ensuremath{\mathbb{N}}} S_n \ensuremath{\mathsf{s}}ubseteq Q^*$. For all $n
		\in \ensuremath{\mathbb{N}}$, there a unique finite path $\rho_n \in \prefUniq{S_n}$ such that $\rho
		\in \ensuremath{\mathsf{Cyl}}(\rho_n)$. Furthermore, for all $k < l \in \ensuremath{\mathbb{N}}$, we have $\rho_k \neq
		\rho_{l}$, otherwise we would have $\prefUniq{S_k} \ni \rho_k \in \prefUniq{S_l}
		\ensuremath{\mathsf{s}}ubseteq S_l \ensuremath{\mathsf{s}}ubseteq S_{k+1}$ (since $l \geq k+1$) which does not hold.
		Hence, $\rho$ has infinitely many different finite prefixes, which is not
		possible. 
		It follows that, for all $\rho \in Q^+$, there is exactly one index $n \in \ensuremath{\mathbb{N}}$
		such that $\rho \in S_n \ensuremath{\mathsf{s}}etminus S_{n-1}$.

		We then define the strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $ in the following way:
		\begin{displaymath}
		\forall n \in \ensuremath{\mathbb{N}},\; \restr{\ensuremath{\mathsf{s}}_\mathsf{A} }{S_n \ensuremath{\mathsf{s}}etminus S_{n-1}} := \ensuremath{\mathsf{s}}_n
		\end{displaymath}
		
		With property $(c)$, this definition ensures that:
		\begin{equation}
		\forall n \in \ensuremath{\mathbb{N}},\; \restr{\ensuremath{\mathsf{s}}_\mathsf{A} }{Q^+ \ensuremath{\mathsf{s}}etminus S_{n+1}} = \ensuremath{\mathsf{s}}_n
		\label{eqn:s_as_sn}
		\end{equation}
		Note that this also holds in the first case where $S_n = \emptyset$ for some
		$n \in \ensuremath{\mathbb{N}}$.
		
		We claim that this Player $\mathsf{A} $ strategy is almost-sure. Consider a Player $\mathsf{B} $
		strategy $\ensuremath{\mathsf{s}}_\mathsf{B} $. Define the concurrent game $\mathcal{G} '$ that is obtained from $\mathcal{G} $ by
		unfolding the state space, thus obtaining the countable state space $q_0 \cdot
		Q^*$ (the set of strategies is unchanged). 

		Let us show that the value of the game $\mathcal{G} '$ with strategies $\ensuremath{\mathsf{s}}_\mathsf{A} $ and
		$\ensuremath{\mathsf{s}}_\mathsf{B} $ from all states (which corresponds to finite paths in $\mathcal{G} $) is at least
		$c \cdot \frac{1}{2} > 0$. This would imply that it is in fact $1$ from all
		states, by Lemma~\ref{lem:chaterjee_value_0_1}.
		
		For all sets $S \ensuremath{\mathsf{s}}ubseteq q_0 \cdot Q^*$, we denote by $\diamondsuit S$ the
		event specifying that the set $S$ is reached.
		
		Let $n \in \ensuremath{\mathbb{N}}$ and $\rho \in S_n \ensuremath{\mathsf{s}}etminus S_{n+1}$. 

		First, let us consider a Player $\mathsf{B} $ strategy $\tilde{\ensuremath{\mathsf{s}}}_\mathsf{B} $ that coincides
		with $\ensuremath{\mathsf{s}}_\mathsf{B} $ on $Q^+ \ensuremath{\mathsf{s}}etminus S_{n+1}$ and such that, for all paths $\rho' \in
		\prefUniq{S_{n+1}} \cap \ensuremath{\mathsf{Cyl}}(\rho)$
		, we have $\prob{\rho'}{\ensuremath{\mathsf{s}}_n^{\rho'},\ensuremath{\mathsf{s}}_\mathsf{B} ^{\rho'}}[W] \leq c \cdot
		\frac{1}{2}$. Note that this is possible since $\rho' \in \prefUniq{S_{n+1}} =
		\prefUniq{V_n} \ensuremath{\mathsf{s}}ubseteq V_n = \mathsf{ValInf}_{c \cdot
			\frac{1}{2}}(\ensuremath{\mathsf{s}}_{n},S_{n})$, which means that $\MarVal{\mathcal{G} }[\ensuremath{\mathsf{s}}_n^\rho](\rho') < c
		\cdot \frac{1}{2}$. With this definition, if
		$\mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_n^\rho,\tilde{\ensuremath{\mathsf{s}}}_\mathsf{B} ^\rho}[\diamondsuit S_{n+1}] > 0$, we
		have:
		\begin{align*}
		\mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_n^\rho,\tilde{\ensuremath{\mathsf{s}}}_\mathsf{B} ^\rho}[W \mid \diamondsuit S_{n+1}] &
		= \frac{\ensuremath{\mathsf{s}}um_{\pi \in \ensuremath{\mathsf{Cyl}}(\rho) \cap \prefUniq{S_{n+1}}}
			\mathbb{P}^{\pi}_{\ensuremath{\mathsf{s}}_n^{\pi},\tilde{\ensuremath{\mathsf{s}}}_\mathsf{B} ^{\pi}}[W] \cdot
			\mathbb{P}^{\rho}_{\ensuremath{\mathsf{s}}_n^{\rho},\tilde{\ensuremath{\mathsf{s}}}_\mathsf{B} ^{\rho}}[
			\pi]}{\mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_n^\rho,\tilde{\ensuremath{\mathsf{s}}}_\mathsf{B} ^\rho}[\diamondsuit S_{n+1}]} \\ &
		\leq c \cdot \frac{1}{2} \frac{\ensuremath{\mathsf{s}}um_{\pi \in \ensuremath{\mathsf{Cyl}}(\rho) \cap \prefUniq{S_{n+1}}}			
			\mathbb{P}^{\rho}_{\ensuremath{\mathsf{s}}_n^{\rho},\tilde{\ensuremath{\mathsf{s}}}_\mathsf{B} ^{\rho}}[\pi]}{\mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_n^\rho,\tilde{\ensuremath{\mathsf{s}}}_\mathsf{B} ^\rho}[\diamondsuit
			S_{n+1}]} \\
		& = c \cdot \frac{1}{2} \cdot
		\frac{\mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_n^\rho,\tilde{\ensuremath{\mathsf{s}}}_\mathsf{B} ^\rho}[\diamondsuit
			S_{n+1}]}{\mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_n^\rho,\tilde{\ensuremath{\mathsf{s}}}_\mathsf{B} ^\rho}[\diamondsuit S_{n+1}]}
		= c \cdot \frac{1}{2}
		\end{align*}

		Furthermore, since $\tilde{\ensuremath{\mathsf{s}}}_\mathsf{B} $ and $\ensuremath{\mathsf{s}}_\mathsf{B} $ coincide on $Q^+ \ensuremath{\mathsf{s}}etminus
		S_{n+1}$:
		\begin{align*}
		\mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_n^\rho,\tilde{\ensuremath{\mathsf{s}}}_\mathsf{B} ^\rho}[W] & =
		\mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_n^\rho,\tilde{\ensuremath{\mathsf{s}}}_\mathsf{B} ^\rho}[W \mid \diamondsuit S_{n+1}]
		\cdot \mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_n^\rho,\tilde{\ensuremath{\mathsf{s}}}_\mathsf{B} ^\rho}[\diamondsuit S_{n+1}] +
		\mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_n^\rho,\tilde{\ensuremath{\mathsf{s}}}_\mathsf{B} ^\rho}[W \mid \lnot \diamondsuit
		S_{n+1}] \cdot \mathbb{P}^q_{\ensuremath{\mathsf{s}}_n^\rho,\tilde{\ensuremath{\mathsf{s}}}_\mathsf{B} ^\rho}[\lnot \diamondsuit
		S_{n+1}] \\
		& \leq c \cdot \frac{1}{2} \cdot
		\mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_n^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[\diamondsuit S_{n+1}] +
		\mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_n^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[W \mid \lnot \diamondsuit S_{n+1}] \cdot
		\mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_n^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[\lnot \diamondsuit S_{n+1}] \\
		& = c \cdot \frac{1}{2} \cdot p_1 + p_2 \cdot (1-p_1)
		\end{align*}
		for $p_1 := \mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_n^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[\diamondsuit S_{n+1}]$ and
		$p_2 := \mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_n^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[W \mid \lnot \diamondsuit
		S_{n+1}]$. We obtain:
		\begin{equation}
		\mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_n^\rho,\tilde{\ensuremath{\mathsf{s}}}_\mathsf{B} ^\rho}[W] \leq \frac{c}{2} \cdot p_1 +
		p_2 \cdot (1-p_1)
		\label{eqn:ineq}
		\end{equation}
		
		This inequality holds for all $\rho \in S_n \ensuremath{\mathsf{s}}etminus S_{n+1}$ and $n \in \ensuremath{\mathbb{N}}$.
		
		
		Now, in the case where $\rho \in \prefUniq{S_n}$, let us show that
		$\mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[W] \geq c \cdot \frac{1}{2}$. Indeed,

		we have by property $(d)$: $\MarVal{\mathcal{G} }[\ensuremath{\mathsf{s}}_n^\rho](\rho) \geq c \cdot (1 -
		c/4)$. This implies $\mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_n^\rho,\tilde{\ensuremath{\mathsf{s}}}_\mathsf{B} ^\rho}[W] \geq c
		\cdot (1 - c/4)$. Therefore:
		\begin{align*}
		c \cdot (1 - \frac{c}{4}) \leq \frac{c}{2} \cdot p_1 + p_2 \cdot (1 - p_1)

		\end{align*}
		Hence, $p_2 > \frac{c}{2}$ (since $1/2 < 1 - c/4$) and:
		\begin{align*}
		p_1 \leq \frac{p_2 - c \cdot (1 - \frac{c}{4})}{p_2 - \frac{c}{2}} 

		\end{align*}
		That is:
		\begin{align*}
		p_2 \cdot (1 - p_1) \geq p_2 \cdot \frac{p_2 - \frac{c}{2} - p_2 + c \cdot (1
			- \frac{c}{4})}{p_2 - \frac{c}{2}} = p_2 \cdot \frac{c \cdot (\frac{1}{2} -
			\frac{c}{4})}{p_2 - \frac{c}{2}} = \frac{c}{2} \cdot \frac{p_2 - p_2 \cdot
			\frac{c}{2}}{p_2 - \frac{c}{2}} \geq \frac{c}{2}
		\end{align*}
		

		
		We can now consider the probability
		$\mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[W]$ of satisfying $W$ given strategies
		$\ensuremath{\mathsf{s}}_\mathsf{A} $ and $\tilde{\ensuremath{\mathsf{s}}}_\mathsf{B} $. Note that $\ensuremath{\mathsf{s}}_\mathsf{A} $ coincides with $\ensuremath{\mathsf{s}}_n$ on $S_n
		\ensuremath{\mathsf{s}}etminus S_{n+1}$ and in particular on $\ensuremath{\mathsf{Cyl}}(\rho) \ensuremath{\mathsf{s}}etminus S_{n+1}$. Hence,
		we have:
		\begin{align*}
		\mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[W] & =
		\mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[W \mid \diamondsuit S_{n+1}] \cdot
		\mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[\diamondsuit S_{n+1}] +
		\mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[W \mid \lnot \diamondsuit S_{n+1}] \cdot
		\mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[\lnot \diamondsuit S_{n+1}] \\
		& \geq \mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[W \mid \lnot \diamondsuit
		S_{n+1}] \cdot \mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[\lnot \diamondsuit
		S_{n+1}] \\
		& = \mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_n^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[W \mid \lnot \diamondsuit S_{n+1}]
		\cdot \mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_n^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[\lnot \diamondsuit S_{n+1}] \\ & =
		p_2 \cdot (1 - p_1) \geq \frac{c}{2}
		\end{align*}
		This holds for all $\rho \in \prefUniq{S_n}$ and for all $n \in \ensuremath{\mathbb{N}}$. 
		
		Consider now some arbitrary $\rho \in S_n \ensuremath{\mathsf{s}}etminus S_{n+1}$. In this case,
		since $\rho \notin \mathsf{ValInf}_{c \cdot \frac{1}{2}}(\ensuremath{\mathsf{s}}_{n},S_{n}) = V_{n}
		\ensuremath{\mathsf{s}}ubseteq S_{n+1}$, we have $\MarVal{\mathcal{G} }[\ensuremath{\mathsf{s}}_n^\rho](\rho) \geq \frac{c}{2}$ and
		$\mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_n^\rho,\tilde{\ensuremath{\mathsf{s}}}_\mathsf{B} ^\rho}[W] \geq \frac{c}{2}$. Hence,
		with Equation~\ref{eqn:ineq} we have:
		\begin{displaymath}
		\frac{c}{2} \leq \mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_n^\rho,\tilde{\ensuremath{\mathsf{s}}}_\mathsf{B} ^\rho}[W] \leq
		\frac{c}{2} \cdot p_1 + p_2 \cdot (1-p_1)
		\end{displaymath}
		Hence, assuming $1 - p_1 = \mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_n^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[\lnot
		\diamondsuit S_{n+1}] > 0$, we obtain that $p_2  =
		\mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_n^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[W \mid \lnot \diamondsuit S_{n+1}] \geq
		\frac{c}{2}$. Furthermore, we have shown that for all $\rho' \in
		\prefUniq{S_{n+1}}$, we have 
		$\mathbb{P}^{\rho'}_{\ensuremath{\mathsf{s}}_\mathsf{A} ^{\rho'},\ensuremath{\mathsf{s}}_\mathsf{B} ^{\rho'}}[W] \geq \frac{c}{2}$. Hence,
		assuming that $\mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[\diamondsuit S_{n+1}]
		\neq 0$, we have: 
		\begin{align*}
		\mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[W \mid \diamondsuit S_{n+1}] & =
		\frac{1}{\mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[\diamondsuit S_{n+1}]} \cdot
		\ensuremath{\mathsf{s}}um_{\rho' \in \prefUniq{S_{n+1}}}
		\mathbb{P}^{\rho'}_{\ensuremath{\mathsf{s}}_\mathsf{A} ^{\rho'},\ensuremath{\mathsf{s}}_\mathsf{B} ^{\rho'}}[W] \cdot
		\mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[\rho'] \\
		& \geq \frac{1}{\mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[\diamondsuit S_{n+1}]}
		\cdot \ensuremath{\mathsf{s}}um_{\rho' \in \prefUniq{S_{n+1}}} \frac{c}{2} \cdot
		\mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[\rho'] \\
		& = \frac{c}{2} \cdot
		\frac{1}{\mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[\diamondsuit S_{n+1}]} \cdot
		\ensuremath{\mathsf{s}}um_{\rho' \in \prefUniq{S_{n+1}}} \cdot
		\mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[\rho'] \\
		& = \frac{c}{2} \cdot
		\frac{1}{\mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[\diamondsuit S_{n+1}]} \cdot
		\mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[\diamondsuit S_{n+1}] \\
		& = \frac{c}{2}
		\end{align*}
		
		Then, assuming that $0<  \mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[\diamondsuit
		S_{n+1}] < 1$, we have:
		\begin{align*}
		\mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[W] & =
		\mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[W \mid \diamondsuit S_{n+1}] \cdot
		\mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[\diamondsuit S_{n+1}] +
		\mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[W \mid \lnot \diamondsuit S_{n+1}] \cdot
		\mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[\lnot \diamondsuit S_{n+1}] \\
		& \geq \frac{c}{2} \cdot \mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[\diamondsuit
		S_{n+1}] + \mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[W \mid \lnot \diamondsuit
		S_{n+1}] \cdot \mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[\lnot \diamondsuit
		S_{n+1}] \\
		& = \frac{c}{2} \cdot \mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_n^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[\diamondsuit
		S_{n+1}] + \mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_n^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[W \mid \lnot \diamondsuit
		S_{n+1}] \cdot \mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_n^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[\lnot \diamondsuit
		S_{n+1}] \\
		& = \frac{c}{2} \cdot \mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_n^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[\diamondsuit
		S_{n+1}] + p_2 \cdot \mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_n^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[\lnot \diamondsuit
		S_{n+1}] \\
		& \geq \frac{c}{2} \cdot \mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_n^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[\diamondsuit
		S_{n+1}] + \frac{c}{2} \cdot \mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_n^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[\lnot
		\diamondsuit S_{n+1}] \\
		& = \frac{c}{2}
		\end{align*}
		Note that this also holds if the probability
		$\mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[\diamondsuit S_{n+1}]
		=\mathbb{P}^\rho_{\ensuremath{\mathsf{s}}_n^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[\diamondsuit S_{n+1}]$ is either equal
		to 0 or to 1.
		
		Overall, we obtain that for all $\rho \in Q^+$, we have $\MarVal{\mathcal{G} '}(\rho) =
		\mathbb{P}^{\rho}_{\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[W] \geq \frac{1}{2}$. Hence, $\inf_{q
			\in Q} \MarVal{\mathcal{G} '}(q) \geq \frac{1}{2}$, which implies, by
		Lemma~\ref{lem:chaterjee_value_0_1}, that, for all $\rho \in q_0 \cdot Q^*$, we
		have $1 = \MarVal{\mathcal{G} '}(q) = \mathbb{P}^{\mathcal{G} ,\rho}_{\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\rho}[W]$. in
		particular, $\mathbb{P}^{\mathcal{G} }_{\ensuremath{\mathsf{s}}_\mathsf{A} ,\ensuremath{\mathsf{s}}_\mathsf{B} }[W] = 1$. As this holds for all Player
		$\mathsf{B} $ strategy $\ensuremath{\mathsf{s}}_\mathsf{B} $, it follows that the strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $ is almost-sure. We
		can then do the same from all states $q \in Q$ to obtain a strategy 
		almost-sure. Furthermore, we have shown that the value of the strategy from
		all finite paths is at least $c/2 > 0$. In fact, this implies that the strategy
		is subgame almost-sure. 

	\end{proof}
	
	\ensuremath{\mathsf{s}}ection{Finite-choice strategies}

	

	
	\ensuremath{\mathsf{s}}ubsection{Proof of Theorem~\ref{thm:fair_strategy_uniformly_optimal}}
	\label{proof:thm_fair_strategy_uniformly_optimal}	
	We show Theorem~\ref{thm:fair_strategy_uniformly_optimal} for more general
	strategies, namely, positively bounded strategies. 
	\begin{definition}[Positively bounded strategy]
		A Player $\mathsf{A} $ strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $ is \emph{positively bounded} (p.b. for short)
		if there is a constant $c > 0$ such that, for all $\rho \cdot q \in Q^+$, for
		all $a \in A_q$ we have: $\ensuremath{\mathsf{s}}_\mathsf{A} (\rho \cdot q)(q) > 0 \ensuremath{\mathbb{R}}ightarrow \ensuremath{\mathsf{s}}_\mathsf{A} (\rho
		\cdot q)(q) \geq c$.
	\end{definition}
	
	We show the theorem below.
	\begin{theorem}
		\label{thm:positively_bounded_strategy_uniformly_optimal}
		Consider a PI concurrent game $\mathcal{G} $. Assume that there is an 
		optimal strategy that is positively bounded. Then, there is a subgame optimal
		strategy that is positively bounded.
	\end{theorem}
	\begin{proof}
		Let us denote by $\ensuremath{\mathsf{s}}_\mathsf{pb}$ an 
		optimal 
		positively bounded Player $\mathsf{A} $ strategy. Let us build inductively a Player
		$\mathsf{A} $ subgame optimal strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $. It is defined as follows: for all finite
		paths $\rho = \rho' \cdot q \in Q^+$, we set $\ensuremath{\mathsf{s}}_\mathsf{A} (\rho)$ to:
		\begin{displaymath}
		\ensuremath{\mathsf{s}}_\mathsf{A} (\rho) := \begin{cases}
		\ensuremath{\mathsf{s}}_{\mathsf{pb}}(\rho) & \text{ if }\ensuremath{\mathsf{s}}_{\mathsf{pb}} \text{ is optimal from
		}\rho\text{, i.e. } \MarVal{\mathcal{G} }(\ensuremath{\mathsf{s}}_{\mathsf{pb}}^\rho)[q] = \MarVal{\mathcal{G} }[q]\\
		\ensuremath{\mathsf{s}}_{\mathsf{pb}}(q) & \text{ otherwise }\\
		\end{cases}
		\end{displaymath}
		Since the strategy $\ensuremath{\mathsf{s}}_{\mathsf{pb}}$ is p.b.
		, it follows that the strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $ also is.	Let us show that it is subgame
		optimal by applying Theorem~\ref{thm:subgame_optimal_arbitrary_strategy}. 
		
		Let $\rho = \rho' \cdot q \in Q^+$. In all cases, the strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $
		coincides with the strategy $\ensuremath{\mathsf{s}}_{\mathsf{pb}}$ (either at $\rho$ or $q$) which
		is optimal from $q$, hence, by
		Proposition~\ref{prop:optimal_implies_locally_optimal}, we have that, for all
		Player $\mathsf{B} $ action $b \in B_q$: $\ensuremath{\mathsf{out}}_{\mathcal{F}_q}(\ensuremath{\mathsf{s}}_\mathsf{A} (q),b) \geq
		\MarVal{\mathcal{G} }(q)$. It follows that the strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $ is locally optimal. 
		
		Let us now show that it ensures the second property. Let $\rho \in Q^+$ and
		let us denote by $\ensuremath{\mathsf{s}}_\rho$ the residual strategy $\ensuremath{\mathsf{s}}_\mathsf{A} ^\rho$. Consider a Player
		$\mathsf{B} $ deterministic strategy $\ensuremath{\mathsf{s}}_\mathsf{B} $ and some value $u \in V_{\mathcal{G} } \ensuremath{\mathsf{s}}etminus \{ 0
		\}$. We introduce two notations:
		\begin{itemize}
			\item we denote by $\mathsf{Exit}_u \ensuremath{\mathsf{s}}ubseteq Q^+$ the set of finite paths
			ending in $Q_u$ with a positive probability to exit this value area:
			$\mathsf{Exit}_u := \{ \pi \cdot Q^* \cdot Q_u \mid
			\mathbb{P}^{\ensuremath{\mathsf{s}}_\rho,\ensuremath{\mathsf{s}}_\mathsf{B} }_{\pi}[Q \ensuremath{\mathsf{s}}etminus Q_u] > 0\}$. 

			\item we also denote by $\mathsf{Deviate} \ensuremath{\mathsf{s}}ubseteq Q^+$ the set of finite
			paths where the strategies $\ensuremath{\mathsf{s}}_\mathsf{A} ^\mathsf{pb}$ is not optimal: $\mathsf{Deviate}
			:= \{ \pi = \pi' \cdot q \in Q^+ \mid \MarVal{\mathcal{G} }[\ensuremath{\mathsf{s}}_{\mathsf{pb}}^{\rho \cdot
				\pi}](q) <  \MarVal{\mathcal{G} }(q) \}$.
		\end{itemize}
		Let us show the following facts:
		\begin{itemize}
			\item[(a).] $\mathbb{P}^{\ensuremath{\mathsf{s}}_\rho,\ensuremath{\mathsf{s}}_\mathsf{B} }_{\rho}[Q^* \cdot (Q_u)^\omega \cap
			(Q^* \cdot \mathsf{Exit}_u)^\omega]

			= 0$;
			\item[(b).] $\mathbb{P}^{\ensuremath{\mathsf{s}}_\rho,\ensuremath{\mathsf{s}}_\mathsf{B} }[Q^* \cdot (Q_u)^\omega \cap Q^* \cdot
			(Q \ensuremath{\mathsf{s}}etminus \mathsf{Exit}_u)^\omega] \leq \mathbb{P}^{\ensuremath{\mathsf{s}}_\rho,\ensuremath{\mathsf{s}}_\mathsf{B} }[Q^* \cdot
			(Q_u)^\omega 
			\cap Q^* \cdot (Q \ensuremath{\mathsf{s}}etminus \mathsf{Deviate})^\omega]$

			;
			\item[(c).] $\mathbb{P}^{\ensuremath{\mathsf{s}}_\rho,\ensuremath{\mathsf{s}}_\mathsf{B} }_{\rho}[Q^* \cdot (Q_u \ensuremath{\mathsf{s}}etminus
			\mathsf{Deviate})^\omega] = \mathbb{P}^{\ensuremath{\mathsf{s}}_\rho,\ensuremath{\mathsf{s}}_\mathsf{B} }_{\rho}[W \cap Q^* \cdot
			(Q_u \ensuremath{\mathsf{s}}etminus \mathsf{Deviate})^\omega]$.

		\end{itemize}
		If we assume that all these facts hold, then we obtain:
		\begin{align*}
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\rho,\ensuremath{\mathsf{s}}_\mathsf{B} }_{\rho}[Q^* \cdot (Q_u)^\omega] & =
		\mathbb{P}^{\ensuremath{\mathsf{s}}_\rho,\ensuremath{\mathsf{s}}_\mathsf{B} }_{\rho}[Q^* \cdot (Q_u)^\omega \cap Q^* \cdot (Q
		\ensuremath{\mathsf{s}}etminus \mathsf{Exit}_u)^\omega] & \text{ by fact (a)} \\
		& \leq \mathbb{P}^{\ensuremath{\mathsf{s}}_\rho,\ensuremath{\mathsf{s}}_\mathsf{B} }_{\rho}[Q^* \cdot (Q_u)^\omega \cap Q^* \cdot
		(Q \ensuremath{\mathsf{s}}etminus \mathsf{Deviate})^\omega] & \text{ by fact (b)} \\
		& = \mathbb{P}^{\ensuremath{\mathsf{s}}_\rho,\ensuremath{\mathsf{s}}_\mathsf{B} }_{\rho}[Q^* \cdot (Q_u \ensuremath{\mathsf{s}}etminus
		\mathsf{Deviate})^\omega]  \\
		& = \mathbb{P}^{\ensuremath{\mathsf{s}}_\rho,\ensuremath{\mathsf{s}}_\mathsf{B} }_{\rho}[W \cap Q^* \cdot (Q_u \ensuremath{\mathsf{s}}etminus
		\mathsf{Deviate})^\omega] & \text{ by fact (c)} \\
		& \leq \mathbb{P}^{\ensuremath{\mathsf{s}}_\rho,\ensuremath{\mathsf{s}}_\mathsf{B} }_{\rho}[W \cap Q^* \cdot (Q_u)^\omega]  \\
		& \leq \mathbb{P}^{\ensuremath{\mathsf{s}}_{\rho},\ensuremath{\mathsf{s}}_\mathsf{B} }_{\rho}[Q^* \cdot (Q_u)^\omega] 

		\end{align*}

		In fact, all these inequalities are equalities. We can then apply
		Theorem~\ref{thm:subgame_optimal_arbitrary_strategy} to conclude. 
		Let us now show all these facts one by one. 
		\begin{itemize}
			\item[(a).] 

			Consider some $\pi = \pi' \cdot q \in \mathsf{Exit}_u$. We have
			$\mathbb{P}^{\ensuremath{\mathsf{s}}^\pi_\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\pi}_{\rho \cdot \pi}[Q \ensuremath{\mathsf{s}}etminus Q_u] > 0$. Let
			$b := \ensuremath{\mathsf{s}}_\mathsf{B} (\pi)$ (recall that $\ensuremath{\mathsf{s}}_\mathsf{B} $ is a deterministic strategy) and let
			$A_{Q \ensuremath{\mathsf{s}}etminus Q_u} := \{ a \in A_q \mid \mathsf{dist}  \circ \delta(q,a,b)[Q
			\ensuremath{\mathsf{s}}etminus Q_u] > 0 \}$. Then, $\ensuremath{\mathsf{s}}^\pi_\rho[A_{Q \ensuremath{\mathsf{s}}etminus Q_u}] > 0$ hence
			$\ensuremath{\mathsf{s}}^\pi_\rho[A_{Q \ensuremath{\mathsf{s}}etminus Q_u}] \geq c$ for some fixed $c > 0$ (since
			$\ensuremath{\mathsf{s}}_\rho$ is p.b.). Furthermore, let $x := \min_{d \in \mathsf{D} } \min_{q \in
				\mathsf{Supp} (\mathsf{dist} (d))} \mathsf{dist} (d)(q) > 0$. It follows that
			$\mathbb{P}^{\ensuremath{\mathsf{s}}^\pi_\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\pi}_{\rho \cdot \pi}[Q \ensuremath{\mathsf{s}}etminus Q_u] \geq c
			\cdot x$. In fact, this holds for all $\pi \in \mathsf{Exit}_u$. Hence, for all
			$\pi \in Q^*$, we have $\mathbb{P}^{\ensuremath{\mathsf{s}}^\pi_\rho,\ensuremath{\mathsf{s}}_\mathsf{B} ^\pi}_{\rho \cdot
				\pi}[(Q_u)^\omega \mid (Q^* \cdot \mathsf{Exit}_u)^\omega] \leq \lim_{n
				\rightarrow \infty} (1 - c \cdot x)^n = 0$. It follows that
			$\mathbb{P}^{\ensuremath{\mathsf{s}}_\rho,\ensuremath{\mathsf{s}}_\mathsf{B} }_{\rho}[Q^* \cdot (Q_u)^\omega \cap (Q^* \cdot
			\mathsf{Exit}_u)^\omega] = 0$.
			\item[(b).] Let us show that $\mathbb{P}^{\ensuremath{\mathsf{s}}_\rho,\ensuremath{\mathsf{s}}_\mathsf{B} }[Q^* \cdot
			(Q_u)^\omega \cap Q^* \cdot (Q \ensuremath{\mathsf{s}}etminus \mathsf{Exit}_u)^\omega \cap (Q^* \cdot
			\mathsf{Deviate})^\omega] = 0$.	Let $\theta \in Q^* \cdot (Q_u)^\omega \cap Q^*
			\cdot (Q \ensuremath{\mathsf{s}}etminus \mathsf{Exit}_u)^\omega$. Let $n \in \mathbb{N}$ be an index
			such that $\theta_{\geq n} \in (Q_u \ensuremath{\mathsf{s}}etminus \mathsf{Exit}_u)^\omega$. 

			Consider, assuming it exists, the least index $i \geq n+1$ such that
			$\theta_i \in \mathsf{Deviate}$. That is, $\MarVal{\mathcal{G} }[\ensuremath{\mathsf{s}}_{\mathsf{pb}}^{\rho
				\cdot \theta_{\leq i}}](\theta_i) < \MarVal{\mathcal{G} }(\theta_i)$ and
			$\MarVal{\mathcal{G} }[\ensuremath{\mathsf{s}}_{\mathsf{pb}}^{\rho \cdot \theta_{\leq i-1}}](\theta_{i-1}) =
			\MarVal{\mathcal{G} }(\theta_{i-1})$. With a straightforward adaptation of
			Proposition~\ref{prop:optimal_implies_locally_optimal}, if
			$\mathbb{P}^{\ensuremath{\mathsf{s}}_\rho,\ensuremath{\mathsf{s}}_\mathsf{B} }_{\theta_{\leq i-1}}[\theta_i] > 0$, for $b :=
			\ensuremath{\mathsf{s}}_\mathsf{B} (\rho \cdot \theta_{\leq i-1})$ (recall that $\ensuremath{\mathsf{s}}_\mathsf{B} $ is deterministic), we
			have $\ensuremath{\mathsf{out}}_{\mathcal{F}_{\theta_{i-1}}}(\ensuremath{\mathsf{s}}_\rho(\theta_{\leq i-1}),b) >
			\MarVal{\mathcal{G} }(\theta_{i-1}) = u$. Hence, at $\theta_{\leq i-1}$, there is a
			non-zero probability to reach a state of value different from $u$, i.e.
			$\mathbb{P}^{\ensuremath{\mathsf{s}}_\rho,\ensuremath{\mathsf{s}}_\mathsf{B} }_{\theta_{\leq i-1}}[Q \ensuremath{\mathsf{s}}etminus Q_u] > 0$. That is,
			$\theta_{i-1} \in \mathsf{Exit}_u$.

			That is a path -- with a positive probability to occur -- that does not visit
			$\mathsf{Exit}_u$ does not visit $\mathsf{Deviate}$ as well. Hence,
			almost-surely, a path visiting $\mathsf{Exit}_u$ only finitely often visits
			$\mathsf{Deviate}$ only finitely often. It follows that
			$\mathbb{P}^{\ensuremath{\mathsf{s}}_\rho,\ensuremath{\mathsf{s}}_\mathsf{B} }[Q^* \cdot (Q_u)^\omega \cap Q^* \cdot (Q \ensuremath{\mathsf{s}}etminus
			\mathsf{Exit}_u)^\omega \cap (Q^* \cdot \mathsf{Deviate})^\omega] = 0$. That is:
			$\mathbb{P}^{\ensuremath{\mathsf{s}}_\rho,\ensuremath{\mathsf{s}}_\mathsf{B} }[Q^* \cdot (Q_u)^\omega \cap Q^* \cdot (Q \ensuremath{\mathsf{s}}etminus
			\mathsf{Exit}_u)^\omega] = \mathbb{P}^{\ensuremath{\mathsf{s}}_\rho,\ensuremath{\mathsf{s}}_\mathsf{B} }[Q^* \cdot (Q_u)^\omega
			\cap Q^* \cdot (Q \ensuremath{\mathsf{s}}etminus \mathsf{Exit}_u)^\omega \cap Q^* \cdot (Q \ensuremath{\mathsf{s}}etminus
			\mathsf{Deviate})^\omega] \leq \mathbb{P}^{\ensuremath{\mathsf{s}}_\rho,\ensuremath{\mathsf{s}}_\mathsf{B} }[Q^* \cdot (Q_u)^\omega
			\cap Q^* \cdot (Q \ensuremath{\mathsf{s}}etminus \mathsf{Deviate})^\omega]$.
			\item[(c).] We proceed similarly to how we proved the necessary conditions of
			Theorem~\ref{thm:subgame_optimal_arbitrary_strategy} with an additional
			difficulty to conclude. Indeed, assume towards a contradiction that
			$\mathbb{P}^{\ensuremath{\mathsf{s}}_\rho,\ensuremath{\mathsf{s}}_\mathsf{B} }_{\rho}[Q^* \cdot (Q_u \ensuremath{\mathsf{s}}etminus
			\mathsf{Deviate})^\omega] > \mathbb{P}^{\ensuremath{\mathsf{s}}_\rho,\ensuremath{\mathsf{s}}_\mathsf{B} }_{\rho}[W \cap Q^* \cdot
			(Q_u \ensuremath{\mathsf{s}}etminus \mathsf{Deviate})^\omega]$. Consider the countable Markov chain
			induced by both strategies $\ensuremath{\mathsf{s}}_\rho$ and $\ensuremath{\mathsf{s}}_\mathsf{B} $ whose initial state is $\rho$.
			We denote by $\mathbb{P}$ the probability function in that Markov chain.
			Consider the prefix-independent objective $W_u := W \cup (Q^* \cdot (Q \ensuremath{\mathsf{s}}etminus
			Q_u \cup \mathsf{Deviate}))^\omega$. We have:
			\begin{align*}
			\mathbb{P}[W_u] & = \mathbb{P}[W_u \cap Q^* \cdot (Q_u \ensuremath{\mathsf{s}}etminus
			\mathsf{Deviate})^\omega] + \mathbb{P}[W_u \cap (Q^* \cdot (Q \ensuremath{\mathsf{s}}etminus Q_u \cup
			\mathsf{Deviate})^\omega] \\
			& = \mathbb{P}[W \cap Q^* \cdot (Q_u \ensuremath{\mathsf{s}}etminus \mathsf{Deviate})^\omega] +
			\mathbb{P}[(Q^* \cdot (Q \ensuremath{\mathsf{s}}etminus Q_u \cup \mathsf{Deviate}))^\omega] \\
			& < \mathbb{P}[Q^* \cdot (Q_u \ensuremath{\mathsf{s}}etminus \mathsf{Deviate})^\omega] +
			\mathbb{P}[(Q^* \cdot (Q \ensuremath{\mathsf{s}}etminus Q_u \cup \mathsf{Deviate}))^\omega] \\
			& = 1
			\end{align*}
			Let us now show that there is a finite paths whose last state is in $Q_u
			\ensuremath{\mathsf{s}}etminus \mathsf{Deviate}$ and from which the probability of $W_u$ is less than
			$u/2$. By Lemma~\ref{lem:chaterjee_value_0_1}, since $W_u$ is prefix
			independent, there is state $\pi \in Q^*$ (which corresponds to a finite path)
			in the Markov chain such that $\mathbb{P}_\pi[W_u] < u/2$. 
			
			Now, assume towards a contradiction that, for all $\pi' \in \pi \cdot Q^*
			\cdot (Q_u \ensuremath{\mathsf{s}}etminus \mathsf{Deviate})$, we have either $\mathbb{P}_{\pi'}[W_u]
			\geq \frac{u}{2}$ or $\mathbb{P}_{\pi'}[Q^* \cdot (Q \ensuremath{\mathsf{s}}etminus Q_u \cup
			\mathsf{Deviate})] > \frac{u}{2}$. Let us denote by $Q_1 := \{ \pi' \in \pi
			\cdot Q^* \cdot (Q_u \ensuremath{\mathsf{s}}etminus \mathsf{Deviate}) \mid \mathbb{P}_{\pi'}[W_u]
			\geq \frac{u}{2} \}$ and by $Q_2 := \pi \cdot Q^* \cdot (Q_u \ensuremath{\mathsf{s}}etminus
			\mathsf{Deviate}) \ensuremath{\mathsf{s}}etminus Q_1$. By definition, $ \pi \cdot Q^* \cdot (Q_u
			\ensuremath{\mathsf{s}}etminus \mathsf{Deviate}) = Q_1 \uplus Q_2$ and by assumption, for all $\pi'
			\in Q_2$, we have $\mathbb{P}_{\pi'}[Q^* \cdot (Q \ensuremath{\mathsf{s}}etminus Q_u \cup
			\mathsf{Deviate})] > u/2$. It follows that $\mathbb{P}_{\pi}[Q^* \cdot (Q_u
			\ensuremath{\mathsf{s}}etminus \mathsf{Deviate})^\omega \cap (Q^* \cdot Q_2)^\omega] = 0$. That is,
			$\mathbb{P}_{\pi}[Q^* \cdot (Q_u \ensuremath{\mathsf{s}}etminus \mathsf{Deviate})^\omega] =
			\mathbb{P}_{\pi}[Q^* \cdot (Q_1 \uplus Q_2)^\omega] = \mathbb{P}_{\pi}[Q^* \cdot
			(Q_1)^\omega]$. Furthermore, $\mathbb{P}_\pi[W_u \cap Q^* \cdot (Q_1)^\omega] =
			\mathbb{P}_\pi[Q^* \cdot (Q_1)^\omega]$ by definition of $Q_1$ (since at some
			point, only states of with probability at least $u/2$ of $W_u$ are seen) and
			Theorem~\ref{thm:levy}. Then:
			\begin{align*}
			\mathbb{P}_\pi[W_u] & = \mathbb{P}_\pi[W_u \cap Q^* \cdot (Q_u \ensuremath{\mathsf{s}}etminus
			\mathsf{Deviate})^\omega] + \mathbb{P}_\pi[W_u \cap (Q^* \cdot (Q \ensuremath{\mathsf{s}}etminus Q_u
			\cup \mathsf{Deviate}))^\omega] \\
			& = \mathbb{P}_\pi[W_u \cap Q^* \cdot (Q_1)^\omega] + \mathbb{P}_\pi[(Q^*
			\cdot (Q \ensuremath{\mathsf{s}}etminus Q_u \cup \mathsf{Deviate}))^\omega] \\
			& = \mathbb{P}_\pi[Q^* \cdot (Q_1)^\omega] + \mathbb{P}_\pi[(Q^* \cdot (Q
			\ensuremath{\mathsf{s}}etminus Q_u \cup \mathsf{Deviate}))^\omega] \\
			& = \mathbb{P}_\pi[Q^* \cdot (Q_u \ensuremath{\mathsf{s}}etminus \mathsf{Deviate})^\omega] +
			\mathbb{P}_\pi[(Q^* \cdot (Q \ensuremath{\mathsf{s}}etminus Q_u \cup \mathsf{Deviate}))^\omega] \\
			& = 1
			\end{align*}
			This is a contradiction with the fact that $\mathbb{P}_\pi[W_u] \leq u/2$. In
			fact, there is some $\pi' \in \pi \cdot Q^* \cdot (Q_u \ensuremath{\mathsf{s}}etminus
			\mathsf{Deviate})$ such that we have $\mathbb{P}_{\pi'}[W_u] < \frac{u}{2}$ and
			$\mathbb{P}_{\pi'}[Q^* \cdot (Q \ensuremath{\mathsf{s}}etminus Q_u \cup \mathsf{Deviate})] \leq u/2$.
			Let $\pi' = \pi'' \cdot q$. Since $\pi' \notin \mathsf{Deviate}$, we have
			$\MarVal{\mathcal{G} }[\ensuremath{\mathsf{s}}_{\mathsf{pb}}^{\rho \cdot \pi'}](q) = \MarVal{\mathcal{G} }(q) = u$. It
			follows that:
			\begin{align*}
			u \leq \mathbb{P}_{\rho \cdot \pi'}^{\ensuremath{\mathsf{s}}_{\mathsf{pb}}^{\rho \cdot
					\pi'},\ensuremath{\mathsf{s}}_\mathsf{B} }[W] & \leq \mathbb{P}_{\rho \cdot \pi'}^{\ensuremath{\mathsf{s}}_{\mathsf{pb}}^{\rho
					\cdot \pi'},\ensuremath{\mathsf{s}}_\mathsf{B} }[W \mid (Q_u \ensuremath{\mathsf{s}}etminus \mathsf{Deviate})^\omega] \cdot
			\mathbb{P}_{\rho \cdot \pi'}^{\ensuremath{\mathsf{s}}_{\mathsf{pb}}^{\rho \cdot \pi'},\ensuremath{\mathsf{s}}_\mathsf{B} }[(Q_u
			\ensuremath{\mathsf{s}}etminus \mathsf{Deviate})^\omega] \\
			& + \mathbb{P}_{\rho \cdot \pi'}^{\ensuremath{\mathsf{s}}_{\mathsf{pb}}^{\rho \cdot
					\pi'},\ensuremath{\mathsf{s}}_\mathsf{B} }[Q^* \cdot (Q \ensuremath{\mathsf{s}}etminus Q_u \cup \mathsf{Deviate})] \\
			& \leq \mathbb{P}_{\rho \cdot \pi'}^{\ensuremath{\mathsf{s}}_{\mathsf{pb}}^{\rho \cdot
					\pi'},\ensuremath{\mathsf{s}}_\mathsf{B} }[W \mid (Q_u \ensuremath{\mathsf{s}}etminus \mathsf{Deviate})^\omega] \cdot (1 -
			\frac{u}{2}) + \frac{u}{2}
			\end{align*}
			Note that we can indeed relate these probabilities with the previous ones
			(expressed with $\mathbb{P}$) with the strategy $\ensuremath{\mathsf{s}}_\rho$ -- instead of
			$\ensuremath{\mathsf{s}}_{\mathsf{pb}}^{\rho \cdot \pi'}$ -- since these two strategies coincide
			outside of $\mathsf{Deviate}$. We obtain:
			\begin{displaymath}
			\mathbb{P}_{\rho \cdot \pi'}^{\ensuremath{\mathsf{s}}_{\mathsf{pb}}^{\rho \cdot \pi'},\ensuremath{\mathsf{s}}_\mathsf{B} }[W
			\mid (Q_u \ensuremath{\mathsf{s}}etminus \mathsf{Deviate})^\omega] = \mathbb{P}_{\pi'}[W \mid (Q_u
			\ensuremath{\mathsf{s}}etminus \mathsf{Deviate})^\omega] \geq \frac{u}{2 - u}
			\end{displaymath}
			We can then conclude that:
			\begin{align*}
			\mathbb{P}_{\pi'}[W_u] & \geq \mathbb{P}_{\pi'}[W_u \cap (Q_u \ensuremath{\mathsf{s}}etminus
			\mathsf{Deviate})^\omega] \\
			& = \mathbb{P}_{\pi'}[W \mid (Q_u \ensuremath{\mathsf{s}}etminus \mathsf{Deviate})^\omega] \cdot
			\mathbb{P}_{\pi'}[(Q_u \ensuremath{\mathsf{s}}etminus \mathsf{Deviate})^\omega] \\
			& \geq \frac{u}{2 - u} \cdot (1 - \frac{u}{2}) \\
			& = \frac{u}{2}
			\end{align*}
			This is a contradiction with the fact that $\mathbb{P}_{\pi'}[W_u] <
			\frac{u}{2}$. In fact, our assumption $\mathbb{P}^{\ensuremath{\mathsf{s}}_\rho,\ensuremath{\mathsf{s}}_\mathsf{B} }_{\rho}[Q^*
			\cdot (Q_u \ensuremath{\mathsf{s}}etminus \mathsf{Deviate})^\omega] >
			\mathbb{P}^{\ensuremath{\mathsf{s}}_\rho,\ensuremath{\mathsf{s}}_\mathsf{B} }_{\rho}[W \cap Q^* \cdot (Q_u \ensuremath{\mathsf{s}}etminus
			\mathsf{Deviate})^\omega]$ does not hold. That is, we have
			$\mathbb{P}^{\ensuremath{\mathsf{s}}_\rho,\ensuremath{\mathsf{s}}_\mathsf{B} }_{\rho}[Q^* \cdot (Q_u \ensuremath{\mathsf{s}}etminus
			\mathsf{Deviate})^\omega] = \mathbb{P}^{\ensuremath{\mathsf{s}}_\rho,\ensuremath{\mathsf{s}}_\mathsf{B} }_{\rho}[W \cap Q^* \cdot
			(Q_u \ensuremath{\mathsf{s}}etminus \mathsf{Deviate})^\omega]$.

		\end{itemize}
	\end{proof}
	The proof of Theorem~\ref{thm:fair_strategy_uniformly_optimal} can then be done
	in a similar way with the additional remark that if $\ensuremath{\mathsf{s}}_{\mathsf{fc}}$ is a
	finite-choice strategy, then the strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $ defined in this proof also is.
	
	\ensuremath{\mathsf{s}}ubsection{Proof of Theorem~\ref{thm:transfer_memory_finite_choice}}
	\label{proof:thm_transfer_memory_finite_choice}
	First note that $W_\mathsf{proj}$ is prefix-independent. Indeed, for $\rho \in
	W_\mathsf{proj}$. We have $\rho = k^n \cdot \pi_0 \cdot k \cdot \pi_1 \cdots$
	for $n \in \{ 0,1 \}$ and $\pi \in W$. Then, for all $i \in \ensuremath{\mathbb{N}}$, we have
	$\rho_{\geq i} = k^{n'} \cdot \pi_j \cdot k \cdot \pi_{j+1} \cdots$ for some $n'
	\in \{ 0,1 \}$ and $j \in \ensuremath{\mathbb{N}}$. Then, since $W$ is prfix independent, then
	$\pi_{\geq j} \in W$.
	
	Now, for a finite choice strategy $\ensuremath{\mathsf{s}}_\mathsf{A} $ and a value $u \in V_{\mathcal{G} } \ensuremath{\mathsf{s}}etminus
	\{ 0 \}$, let us define the game $\mathcal{G} ^{\mathsf{tb}}_u$:
	\begin{definition}
		\label{def:game_g_u_tb}

		For a positive value $u \in V_{\mathcal{G} } \ensuremath{\mathsf{s}}etminus \{ 0 \}$, we define the game
		$\mathcal{G} ^\mathsf{tb}_u = \mathcal{G} ames{\mathsf{A} conc_u}{W_{\mathsf{proj}}}$ with
		$\mathsf{A} conc^\mathsf{tb}_u = \langle Q^\mathsf{A} _u \uplus Q^\mathsf{B} _u \uplus \mathsf{A} conc_W,(A'_q)_{q
			\in Q'_u},(B'_q)_{q \in
			Q'_u},\mathsf{D} ,\delta',\mathsf{dist} ',\mathsf{K} ,\mathsf{col} ' \rangle$ where we
		refer to the arena $\mathsf{A} conc_W$ as a sink state to which there are some
		transitions:
		\begin{itemize}
			\item $Q_u^\mathsf{A}  := Q_u$ the set of Player $\mathsf{A} $'s states;
			\item For all $q \in Q^\mathsf{A} _u$, we have $A'_q := S_q$ and $B'_q := \{
			b_{\mathsf{id}} \}$ for a new fresh action $b_{\mathsf{id}}$;
			\item $Q_u^\mathsf{B}  := \{ (q,\ensuremath{\mathsf{s}}igma) \mid q \in Q_u,\; \ensuremath{\mathsf{s}}igma \in A'_q \}$ the set
			of Player $\mathsf{B} $'s states;
			\item For all $q \in Q^\mathsf{B} _u$, we have $A'_q := \{ a_{\mathsf{id}} \}$ for a
			new fresh action $a_{\mathsf{id}}$ and $B'_q := B_q$;
			\item $\mathsf{D} ' := \{ d_{q,\ensuremath{\mathsf{s}}igma} \mid q \in Q_u,\; \ensuremath{\mathsf{s}}igma \in A'_q \}
			\uplus \{ d_{q,\ensuremath{\mathsf{s}}igma,b} \mid q \in Q_u,\; \ensuremath{\mathsf{s}}igma_q \in A'_q, b \in B \}$;
			\item For all $q \in Q_u$ and $\ensuremath{\mathsf{s}}igma \in A'_q$ we have:
			$\delta'(q,\ensuremath{\mathsf{s}}igma,b_{\mathsf{id}}) := d_{q,\ensuremath{\mathsf{s}}igma_q}$;
			\item For all $q \in Q_u$, $\ensuremath{\mathsf{s}}igma \in A'_q$ and $b \in B_q$, we have:
			$\delta'((q,\ensuremath{\mathsf{s}}igma),a_\mathsf{id},b) := d_{q,\ensuremath{\mathsf{s}}igma,b}$;
			\item For all $q \in Q_u,\; \ensuremath{\mathsf{s}}igma \in A'_q$, we have
			$\mathsf{dist} '(d_{q,\ensuremath{\mathsf{s}}igma})((q,\ensuremath{\mathsf{s}}igma)) := 1$. Furthermore, for all $b \in
			B'_q$ and $q' \in Q$, we have:
			\begin{displaymath}
			\mathsf{dist} '(d_{q,\ensuremath{\mathsf{s}}igma_q,b})(q') := 
			\begin{cases}
			\ensuremath{\mathsf{s}}um_{a \in A} \ensuremath{\mathsf{s}}igma_q(a) \cdot \mathsf{dist} (\delta(q,a,b))(q') & \text{ if
			} q' \in Q_u\\
			\ensuremath{\mathsf{s}}um_{a \in A} \ensuremath{\mathsf{s}}igma_q(a) \cdot \mathsf{dist} (\delta(q,a,b))[Q \ensuremath{\mathsf{s}}etminus Q_u]
			& \text{ if } q' = \mathsf{A} conc_W\\
			\end{cases}
			\end{displaymath}
			\item Finally, for all $q \in Q_u$, we have $\mathsf{col} '(q) := \mathsf{col} (q)$ and
			for all $\ensuremath{\mathsf{s}}igma \in A'_q$: $\mathsf{col} '(q,\ensuremath{\mathsf{s}}igma) := k$ for some arbitrary color
			$k \in \mathsf{K} $.
		\end{itemize}
	\end{definition}	
	
	Let us now proceed to the proof of
	Theorem~\ref{thm:transfer_memory_finite_choice}. 
	\begin{proof}
		As for the proof of Lemma~\ref{lem:value_one_Gu}, we can show that if there is
		a subgame optimal strategy that has finite choice, then for all $u \in V_{\mathcal{G} }
		\ensuremath{\mathsf{s}}etminus \{ 0 \}$, all the states in the game $\mathcal{G} ^\mathsf{tb}_u$ have a
		positive value. Indeed, if Player $\mathsf{A} $ plays the subgame optimal strategy that
		has finite choice in the turn-based game $\mathcal{G} _u^\mathsf{tb}$, we obtain the same
		MDPs (modulo intermediate states colored with $k$) than the MDPs obtained in the
		concurrent game $\mathcal{G} $ (restricted to $Q_u$) where Player $\mathsf{A} $ plays the same
		subgame optimal strategy that has finite choice. Furthermore, all the games
		$\mathcal{G} ^\mathsf{tb}_u$ are finite and turn-based. We can then apply the same proof
		than for Theorem~\ref{thm:transfer_memory}: by
		Theorem~\ref{thm:all_not_zero_implies_almost_sure}, there exists a subgame
		almost-surely winning strategy in all games $\mathcal{G} _u$ for $u \in V_{\mathcal{G} } \ensuremath{\mathsf{s}}etminus
		\{ 0 \}$. We then obtain a subgame optimal strategy by gluing these strategies
		into one, this is given by Lemma~\ref{prop:glued_strategy}. Then again, if all
		strategies $\ensuremath{\mathsf{s}}_\mathsf{A} ^u$ are positional for all $u \in V_{\mathcal{G} } \ensuremath{\mathsf{s}}etminus \{ 0 \}$,
		then so is the glued strategy $\ensuremath{\mathsf{s}}_\mathsf{A} [(\ensuremath{\mathsf{s}}_\mathsf{A} ^u)_{u \in V_{\mathcal{G} } \ensuremath{\mathsf{s}}etminus \{ 0
			\}}]$. 		
	\end{proof}
	
	\ensuremath{\mathsf{s}}ubsection{Proof of Corollary~\ref{coro:transfer_memory_finite_choice}}
	\label{proof:coro_transfer_memory_finite_choice}
	Let us formally define these objectives and argue that they have aneutral color
	and that they are \textsf{PSAWT}. 
	
	Consider first the parity objective. It is formally defined in
	Definition~\ref{def:parity_buchi_cobuchi}. The least color (which is an integer
	for the parity objective) in $\mathsf{K} $ is straightforwardly a neutral color
	(since we consider the maximum of the colors seen infinitely often).
	Furthermore, the parity objective is \textsf{PSAWT}, as shown for instance in
	\cite{DBLP:conf/soda/ChatterjeeJH04,DBLP:conf/fossacs/Zielonka04}.
	
	Let us now define the mean-payoff objective. 
	\begin{definition}[Mean-payoff]
		Let $\mathsf{K}  := Q \cap [0,1]$ and $m \in \mathsf{K} $. The \emph{mean-payoff}
		objective $W_\mathsf{MP(m)}$ w.r.t. $m$ is $W_\mathsf{MP(m)} := \{ \rho \in
		\mathsf{K} ^\omega \mid \limsup_{n \rightarrow \infty} \frac{1}{n+1} \ensuremath{\mathsf{s}}um_{i = 0}^n
		\rho_i \geq m \}$.
	\end{definition}
	Given a mean-payoff objective $W_\mathsf{MP(m)}$ for some $m \in Q \cap [0,1]$,
	one can see that $m$ is in fact a neutral color for $W_\mathsf{MP(m)}$.
	Furthermore, it is also \textsf{PSAWT}, as proved in
	\cite{liggett1969stochastic}. 
	
	Finally, consider the generalized Büchi objective. 
	\begin{definition}[Generalized Büchi]
		Let $\mathsf{K}  \ensuremath{\mathsf{s}}ubseteq \ensuremath{\mathbb{N}}$ be a finite subset of integers. A \emph{generalized
			Büchi} objective is an intersection of Büchi objectives on $\mathsf{K} $. 
	\end{definition}
	This objective has a neutral color, up to adding a fresh color that does not
	appear in any of the intersected Büchi objectives. Furthermore, it is also
	\textsf{PSAWT}, as proved in \cite{DBLP:conf/qest/ChatterjeeAH04} as a sub-class
	of upward-closed Muller objectives. 
	
	The proof of Corollary~\ref{coro:transfer_memory_finite_choice} is then direct.
	\begin{proof}
		By Theorem~\ref{thm:fair_strategy_uniformly_optimal}, there is subgame optimal
		strategy in $\mathcal{G} $ that is finite choice. Since the objective considered has a
		neutral color and is \textsf{PSAWT}, it follows that there is a positional
		subgame optimal strategy by Theorem~\ref{thm:transfer_memory_finite_choice}.
	\end{proof}

\end{document}