\(\mathcal {G}\)  is stopping under fairness iff
\(\exists \mathit {Pre}_f^*(V \setminus \forall \mathit {Pre}_f^*(T)) = \emptyset \) .
It is direct to see that \(\exists \mathit {Pre}_f\)  and \(\forall \mathit {Pre}_f\)  can be computed using standard graph algorithms which are polynomial in time w.r.t. the size of the game, thus we obtain the following theorem.
Checking whether the stochastic game \(\mathcal {G}\)  is stopping under
fairness or not is in \(O(\mathit {poly}(\mathit {size}(\mathcal {G})))\) .
Determinacy of Stopping Games under Fairness.
The determinacy of stochastic games with Borel and bounded payoff functions follows from Martin's results [1]}. The function \(\textit {rew}\)  is unbounded, so Martin's theorems do not apply to it. In [2]}, the determinacy of a general class of stopping stochastic games (called transient) with total rewards is proven. However, note that we restrict Player 2 to only play with fair strategies and hence, the last result does not apply either.
In [3]} the authors classify Player 2's strategies into proper (those ensuring termination) and improper (those prolonging the game indefinitely). For proving determinacy, the authors assume that the value of the game for Player 2's improper strategies is \(\infty \) . It is worth noting that, for proving the results below, we do not make any assumption about unfair strategies.
In the following we prove that the restriction to fair plays does not affect the determinacy of the games.
The notion of semi-Markov strategies [2]} will be important for the theorems in this section. Intuitively, a semi-Markov strategy only takes into account the length of a play, the initial state, and the current state to select the next step in the play.
Let \(\mathcal {G}= (V, (V_1, V_2, V_\mathsf {P}), \delta )\)  be a stochastic game. A strategy \(\pi _{i} \in \Pi _{i}\)  is called semi-Markov if: \(\pi _{i}(v \hat{\omega }v^{\prime }) = \pi _{i}(v \hat{\omega }^{\prime }v^{\prime })\) , for every \(v \in V\)  and \(\hat{\omega }, \hat{\omega }^{\prime } \in V^*\)  such that \(|\hat{\omega }|=|\hat{\omega }^{\prime }|\) .
The set of all semi-Markov (resp. semi-Markov fair) strategies for player \(i\)  is denoted \(\Pi ^{S}_{i}\)  (resp. \(\Pi ^{S\mathcal {F}}_{i}\) ). The importance of semi-Markov strategies lies in the fact that, when Player 2 plays a semi-Markov strategy, any Player 1's strategy can be mimicked by a semi-Markov strategy as stated in the following theorem.
Let \(\mathcal {G}\)  be a stopping under fairness stochastic game, and let
\(\pi _{2} \in \Pi ^{S\mathcal {F}}_{2}\)  be a fair and semi-Markov
strategy. Then, for any \(\pi _{1} \in \Pi _{1}\) , there is a
semi-Markov strategy \(\pi ^*_{1} \in \Pi ^{S}_{1}\) 
such that
\(\mathbb {E}^{\pi _{1}, \pi _{2}}_{\mathcal {G}, v}[\textit {rew}] =\mathbb {E}^{\pi ^*_{1}, \pi _{2}}_{\mathcal {G}, v}[\textit {rew}]\) .

[Sketch]
The proof follows the arguments of Theorem 4.2.7 in [2]}
adapted to our setting.
Consider the event \(\Diamond ^{k} v^{\prime } = \lbrace  \omega \in \mathit {Paths}_\mathcal {G}\mid \omega _k = v^{\prime }\rbrace \) , for \(k\ge 0\) . That is,
the set of runs in which \(v^{\prime }\)  is reached after exactly \(k\)  steps.
We define \(\pi ^*_{1}\)  as follows.
\(\pi ^*_{1}(\hat{\omega }v^{\prime })(v^{\prime \prime }) = \mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\Diamond ^{k+1} v^{\prime \prime } \mid \Diamond ^k v^{\prime })\) 
for every \(\hat{\omega }\)  such that \(\mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\hat{\omega }v^{\prime }) > 0\)  and \(|\hat{\omega }v^{\prime }| = k\) . For those \(\hat{\omega }\) 's with \(\mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\hat{\omega }v^{\prime }) = 0\)  we define \(\pi ^*_{1}(\hat{\omega }v^{\prime })\)  to be any arbitrary distribution. We prove that this strategy satisfies the conditions of the theorem.
For this, we prove that \(\mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\Diamond ^{k} v^{\prime }) = \mathit {Prob}^{\pi ^*_{1}, \pi _{2}}_{\mathcal {G},v}(\Diamond ^{k} v^{\prime })\)  by induction on \(k\) .
Hence:
\(\mathbb {E}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}] & = \sum ^\infty _{N=0} \sum _{\hat{\omega } \in V^{N+1}} \mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\hat{\omega })\mathit {r}(\hat{\omega }_N)\\& = \sum ^\infty _{N=0} \sum _{v \in V} \mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\Diamond ^N v)\mathit {r}(v) \\& = \sum ^\infty _{N=0} \sum _{v \in V} \mathit {Prob}^{\pi ^*_{1}, \pi _{2}}_{\mathcal {G},v}(\Diamond ^N v)\mathit {r}(v) \\& = \mathbb {E}^{\pi ^*_{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}]\) 

\(\Box \)
The results below relate the games presented in this paper with
transient games [2]}, [7]}. Roughly speaking, the
following property states that, in games that stop under fairness, the
expected time that both players spend in non-terminal states is
finite, given that the two players play memoryless strategies.
Let \(\mathcal {G}= (V, (V_1, V_2, V_\mathsf {P}), \delta )\)  be a
stochastic game that is stopping under fairness with \(T\)  being the
set of terminal states.
Let \(\pi _{1} \in \Pi ^{M}_{1}\)  be a memoryless strategy
for Player 1 and \(\pi _{2} \in \Pi ^{M\mathcal {F}}_{2}\)  a
memoryless fair strategy for Player 2. Then
\(\sum ^\infty _{N=1} \sum _{\hat{\omega } \in (V \setminus T)^{N}} \mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\hat{\omega }) < \infty \) .
This result can be extended to all the strategies of Player 1. The
main idea behind the proof is to fix a stationary fair strategy for
Player 2 (e.g., a uniform distributed strategy). This yields an MDP
that stops for every strategy of Player 1, and furthermore, it can be
seen as a one-player transient game (as defined in
[2]}). Hence, the result follows from Lemma
REF  and Theorem 4.2.12 in
[2]}.
Let \(\mathcal {G}\)  be a stochastic game that is stopping under fairness
and let \(T\)  be the set of terminal states. In addition, let
\(\pi _{1} \in \Pi _{1}\)  be a strategy for Player 1 and
\(\pi _{2} \in \Pi ^{M\mathcal {F}}_{2}\)  be a fair and memoryless
strategy for Player 2. Then
\(\sum ^\infty _{N=0} \sum _{\hat{\omega } \in v(V \setminus T)^N} \mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\hat{\omega }) < \infty \) .
Using the previous theorem, some fairly simple calculations lead to
the fact that the value of the total accumulated reward payoff game is
well-defined for any strategy of the players. This is stated in the
next theorem.
Let \(\mathcal {G}= (V, (V_1, V_2, V_\mathsf {P}), \delta )\)  be a
stochastic game that is stopping under fairness,
\(\pi _{1} \in \Pi _{1}\)  a strategy for Player 1, and
\(\pi _{2} \in \Pi ^{\mathcal {F}}_{2}\)  a fair strategy for Player 2.
Then, for all \(v \in V\) ,
\(\mathbb {E}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}] < \infty \) .
As a consequence of this theorem, the value of the game is bounded
from above for any Player 1's strategy.

Let \(\mathcal {G}= (V, (V_1, V_2, V_\mathsf {P}), \delta )\)  be a
stochastic game that is stopping under fairness and
\(\pi _{1} \in \Pi _{1}\)  a strategy for Player 1.
Then, for every vertex \(v \in V\) ,
\(\inf _{\pi _{2} \in \Pi ^{\mathcal {F}}_{2}} \mathbb {E}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}] < \infty \) .
Consider any fair strategy \(\pi _{2}^{\prime } \in \Pi ^{\mathcal {F}}_{2}\) .
Then,
\(\inf _{\pi _{2} \in \Pi ^{\mathcal {F}}_{2}} \mathbb {E}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}]\le \mathbb {E}^{\pi _{1}, \pi ^{\mathrm {u}}_{2}}_{\mathcal {G},v}[\textit {rew}] < \infty \) ,
where the last inequality follows from
Theorem REF .
\(\Box \)
The following theorem plays an important role in the rest of the
paper. Intuitively, it states that, when Player 1 plays with a
memoryless strategy, Player 2 has an optimal deterministic
memoryless fair strategy.
Let \(\mathcal {G}= (V, (V_1, V_2, V_\mathsf {P}), \delta )\)  be a
stochastic game that is stopping under fairness and let
\(\pi _{1} \in \Pi ^{M}_{1}\)  be a memoryless strategy for
Player 1. There exists a deterministic memoryless fair strategy
\(\pi ^*_{2}\in \Pi ^{M\mathcal {F}}_{2}\)  such that
\(\inf _{\pi _{2} \in \Pi ^{\mathcal {F}}_{2}} \mathbb {E}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}]=\mathbb {E}^{\pi _{1}, \pi ^*_{2}}_{\mathcal {G},v}[\textit {rew}]\) , for every \(v \in V\) .
As an immediate consequence of Theorem REF , we have
that, if Player 1 plays with a memoryless strategy, it suffices that
Player 2 considers only memoryless fair strategies to find its
optimal value:
Let \(\mathcal {G}= (V, (V_1, V_2, V_\mathsf {P}), \delta )\)  be a stochastic game that is stopping under fairness
and let \(\pi _{1} \in \Pi ^{M}_{1}\)  be a memoryless
strategy for Player 1. Then,
\(\inf _{\pi _{2} \in \Pi ^{\mathcal {F}}_{2}} \mathbb {E}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}]=\inf _{\pi _{2} \in \Pi ^{M\mathcal {F}}_{2}} \mathbb {E}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}]\) , for every \(v \in V\) .
Semi-Markov strategies can be thought of as sequences of memoryless strategies. The next theorem uses this fact to show that, when Player 2 plays a memoryless and fair strategy, semi-Markov strategies do not improve the value that Player 1 can obtain via memoryless strategies. The proof of the following theorem adapts the ideas of Theorem 4.2.9 in [2]} to our games.
For any stochastic game \(\mathcal {G}\)  that is stopping under fairness, and vertex \(v\) , it holds that:
\(\sup _{\pi _{1} \in \Pi ^{S}_{1}} \inf _{\pi _{2} \in \Pi ^{M\mathcal {F}}_{2}} \mathbb {E}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}]= \sup _{\pi _{1} \in \Pi ^{M}_{1}} \inf _{\pi _{2} \in \Pi ^{M\mathcal {F}}_{2}} \mathbb {E}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}]\) 
Using the previous theorem, we can prove the following
useful property.

For any stochastic game \(\mathcal {G}\)  that is stopping under fairness we have:
\(\sup _{\pi _{1} \in \Pi _{1}} \inf _{\pi _{2} \in \Pi ^{\mathcal {F}}_{2}} \mathbb {E}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}]=\sup _{\pi _{1} \in \Pi ^{M}_{1}} \inf _{\pi _{2} \in \Pi ^{M\mathcal {F}}_{2}} \mathbb {E}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}]\) 


First, we prove that the left-hand term is smaller or equal to the right-hand one:
\(\sup _{\pi _{1} \in \Pi _{1}} \inf _{\pi _{2} \in \Pi ^{\mathcal {F}}_{2}} \mathbb {E}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}]&{} \le \sup _{\pi _{1} \in \Pi _{1}} \inf _{\pi _{2} \in \Pi ^{M\mathcal {F}}_{2}} \mathbb {E}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}]\\&{} \le \sup _{\pi _{1} \in \Pi ^{S}_{1}} \inf _{\pi _{2} \in \Pi ^{M\mathcal {F}}_{2}} \mathbb {E}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}]\le \sup _{\pi _{1} \in \Pi ^{M}_{1}} \inf _{\pi _{2} \in \Pi ^{M\mathcal {F}}_{2}} \mathbb {E}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}]\) 

The first inequality follows from \(\Pi ^{M\mathcal {F}}_{2} \subseteq \Pi ^{\mathcal {F}}_{2}\) , the second inequality is due to Theorem REF  and the fact that memoryless strategies are semi-Markov, and the last inequality is obtained by applying Theorem REF .
To prove the other inequality, we calculate:
\(\sup _{\pi _{1} \in \Pi ^{M}_{1}} \inf _{\pi _{2} \in \Pi ^{M\mathcal {F}}_{2}} \mathbb {E}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}]= \sup _{\pi _{1} \in \Pi ^{M}_{1}} \inf _{\pi _{2} \in \Pi ^{\mathcal {F}}_{2}} \mathbb {E}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}]\le \sup _{\pi _{1} \in \Pi _{1}} \inf _{\pi _{2} \in \Pi ^{\mathcal {F}}_{2}} \mathbb {E}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}].\) 
The first equality follows from Corollary REF , and the second inequality is due to suprema properties.
\(\Box \) 
Furthermore, since the values obtained via randomized memoryless strategies are convex combinations of values
obtained via deterministic memoryless strategies, we obtain the following corollary.
For any stochastic game \(\mathcal {G}\)  that is stopping under fairness we have:
\(\sup _{\pi _{1} \in \Pi _{1}} \inf _{\pi _{2} \in \Pi ^{\mathcal {F}}_{2}} \mathbb {E}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}]= \sup _{\pi _{1} \in \Pi ^{MD}_{1}} \inf _{\pi _{2} \in \Pi ^{MD\mathcal {F}}_{2}} \mathbb {E}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}]\) 
Summing up, we can compute the value \(\sup _{\pi _{1} \in \Pi _{1}} \inf _{\pi _{2} \in \Pi ^{\mathcal {F}}_{2}} \mathbb {E}^{\pi _{1}, \pi _{2}}[\textit {rew}]\) , for any vertex \(v\) , by restricting ourselves to deterministic memoryless strategies.
It is worth noting that, by Theorem REF , the value \(\mathbb {E}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}]\)  is finite
for every stopping game under fairness \(\mathcal {G}\)  and strategies \(\pi _{1} \in \Pi ^{MD}_{1}\) , \(\pi _{2} \in \Pi ^{MD\mathcal {F}}_{2}\) .
Furthermore, because the number of deterministic memoryless strategies is finite we have that the number
\(\mathbf {U}= \max \lbrace  \inf _{\pi _{2} \in \Pi ^{MD\mathcal {F}}_{2}} \sup _{\pi _{1} \in \Pi ^{MD}_{1}} \mathbb {E}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}] \mid v \in V \rbrace \)  is well defined. Consider the functional:
\(\Gamma : [0,\mathbf {U}]^V \rightarrow [0,\mathbf {U}]^V\) , defined by the following set of equations.
\(\Gamma (f)(v) ={\left\lbrace \begin{array}{ll}\end{array}\sum _{v^{\prime } \in \mathit {post}(v)} \delta (v,v^{\prime }) f(v^{\prime }) & \text{ if } v \in V_\mathsf {P}\\\max \lbrace \mathit {r}(v) + f(v^{\prime }) \mid v^{\prime } \in \mathit {post}(v) \rbrace  & \text{ if } v \in V_1 \setminus T, \\\min \lbrace \mathit {r}(v) + f(v^{\prime }) \mid v^{\prime } \in \mathit {post}(v) \rbrace  & \text{ if } v \in V_2 \setminus T, \\0 & \text{ if } v \in T.\right.}\) 
Since \(([0,\mathbf {U}]^V, \le )\)  is a complete lattice and \(\Gamma \)  is monotonic, by the Knaster-Tarski theorems, the (non-empty) set of fixed points of \(\Gamma \)  forms a complete lattice. From now on, we denote by
\(\nu \Gamma \)  the greatest fixed point of \(\Gamma \) .
The following theorem states that game determinacy is preserved when Player 2 is restricted to play fair strategies. Furthermore, the value of the game is given by the greatest fixed point of \(\Gamma \) .
 Let \(\mathcal {G}\)  be a stochastic game stopping under fair strategies. It holds that:
\(\inf _{\pi _{2} \in \Pi ^{\mathcal {F}}_{2}} \sup _{\pi _{1} \in \Pi _{1}} \mathbb {E}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}] = \sup _{\pi _{1} \in \Pi _{1}} \inf _{\pi _{2} \in \Pi ^{\mathcal {F}}_{2}} \mathbb {E}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}] = \nu \Gamma (v)\) 


First, note that \(\inf _{\pi _{2} \in \Pi ^{MD\mathcal {F}}_{2}} \sup _{\pi _{1} \in \Pi ^{MD}_{1}} \mathbb {E}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}]\) 
is a fixed point of \(\Gamma \) . Thus we have:
\( \sup _{\pi _{1} \in \Pi _{1}} \inf _{\pi _{2} \in \Pi ^{\mathcal {F}}_{2}} \mathbb {E}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}]& \le \inf _{\pi _{2} \in \Pi ^{\mathcal {F}}_{2}} \sup _{\pi _{1} \in \Pi _{1}} \mathbb {E}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}] \\& \le \inf _{\pi _{2} \in \Pi ^{MD\mathcal {F}}_{2}} \sup _{\pi _{1} \in \Pi ^{MD}_{1}} \mathbb {E}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}]\le \nu \Gamma (v)\) 

for any \(v\) . The first inequality is a standard property of suprema and infima [11]}, the second inequality holds because
\(\Pi ^{MD\mathcal {F}}_{2} \subseteq \Pi ^{\mathcal {F}}_{2}\)  and standard properties of MDPs: by fixing a deterministic memoryless
fair strategy for Player 2 we obtain a transient MDP, the optimal strategy for Player 1 in this MDP is obtained via a deterministic memoryless strategy [12]},
the last inequality holds because \(\inf _{\pi _{2} \in \Pi ^{MD\mathcal {F}}_{2}} \sup _{\pi _{1} \in \Pi ^{MD}_{1}} \mathbb {E}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}]\)  is
a fixed point of \(\Gamma \) .
Rest to prove that \(\sup _{\pi _{1} \in \Pi _{1}} \inf _{\pi _{2} \in \Pi ^{\mathcal {F}}_{2}} \mathbb {E}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}] \ge \nu \Gamma (v)\) . Note that, if there is \(\pi _{1} \in \Pi _{1}\)  such that
\(\inf _{\pi _{2} \in \Pi ^{\mathcal {F}}_{2}} \mathbb {E}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}] \ge \nu \Gamma (v)\)  the property above follows by properties of supremum. Consider the strategy \(\pi ^*_{1}\)  defined as follows:
\(\pi ^*_{1}(v) \in \operatornamewithlimits{argmax}\lbrace \nu \Gamma (v^{\prime }) + \mathit {r}(v) \mid v^{\prime } \in \mathit {post}(v) \rbrace \) . Note that \(\pi ^*_{1}\)  is a memoryless strategy. For any memoryless and fair strategy \(\pi _{2} \in \Pi ^{M\mathcal {F}}_{2}\)  we have
\(\nu \Gamma (v) \le \mathbb {E}^{\pi ^*_{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}]\)  (by definition of \(\Gamma \) ). Thus,
\(\nu \Gamma (v) \le \inf _{\pi _{2} \in \Pi ^{M\mathcal {F}}_{2}} \mathbb {E}^{\pi ^*_{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}]\) 
and therefore:
\(\nu \Gamma (v) \le \sup _{\pi _{1} \in \Pi ^{M}_{1}} \inf _{\pi _{2} \in \Pi ^{M\mathcal {F}}_{1}} \mathbb {E}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}]\) .
Finally, by Theorem REF  we get:
\(\nu \Gamma (v) \le \sup _{\pi _{1} \in \Pi _{1}} \inf _{\pi _{2} \in \Pi ^{\mathcal {F}}_{2}} \mathbb {E}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}]\) .
\(\Box \)

Considerations for an algorithmic solution.
Value iteration [13]} has been used to compute maximum/minimum expected accumulated reward in MDPs, e.g. in the Prism model checker. Usually, the value is computed by approximating the least fixed point from below using the Bellman equations [13]}. In [15]}, the authors propose to approach these values from both a lower and an upper bound (known as interval iteration [16]}). To do so, [15]} shows a technique for computing upper bounds for the expected total rewards for MDPs.
The above defined functional \(\Gamma \)  presents a form of Bellman equations that enables a value iteration algorithm to solve our games. As we are looking for the greatest fixed point, we need to start with some value vector larger than such a fixed point.
If we take our game and fix a fair strategy for the environment, we obtain an MDP. We can then use the techniques presented in [15]} to find an upper bound in this MDP, which in turn is an upper bound in the original game. The obvious fair strategy to use is the one based on the uniform distribution (as in Theorem REF ). We have implemented these ideas in a prototype tool as described in the next section.

Experimental Evaluation
In order to evaluate the viability of our approach we have implemented a prototype tool named SynthFairy (available at [19]})
and run it on two different sets of examples. The tool takes as input a model describing the game and the state rewards and returns as output
the optimal expected total reward for a given initial state as well as the synthesized optimal controller strategy (under fairness assumptions).
The input models are specified using a language resembling Prism notation [20]}. The experimental evaluation shows that our approach can cope with case studies of reasonable complexity. For computing these values we set a relative error of at most \(\varepsilon = 10^{-6}\) .
Roborta vs. the Fair Light.
Table REF  shows the results of the example introduced in Sec. 
for multiple configurations.
We considered three variants of the case study: version A (the light does not fail), version B (the light can only fail when trying to signal a green light), and version C (the light can fail when trying to signal any kind of light).
We assumed that, when Roborta fails, she cannot move (this is beneficial to Roborta since she can re-collect the reward);
when the light fails, the robot can freely move into any allowed direction.
The grid configuration (movement restrictions and rewards) are randomly generated. For each setting, Table REF  describes the results for three different scenarios generated starting at different seeds. For the grid configuration shown in Sec.  with parameters \(P=0.1\)  and \(Q=0\) , the tool derived the optimal strategy depicted in Fig. REF  and reports an expected total reward of \(5.55\) .

Autonomous UAV vs. Human Operator.
We adapted the case study analyzed in [21]}. A remotely controlled Unmanned Aerial Vehicle (UAV) is used to perform intelligence, surveillance, and reconnaissance (ISR) missions over a road network. The UAV performs piloting functions autonomously (selecting a path to fly between waypoints). The human operator (environment) controls the onboard sensor to capture imagery at a waypoint as well as the piloting functions on certain waypoints (called checkpoints). Note that an operator can continuously try to get a better image by making the UAV loiter around a certain waypoint, this may lead to an unfair behavior.
Each successful capture from an unvisited waypoint grants a reward.
<FIGURE>Fig. REF  shows an example of road network consisting of six surveillance waypoints labeled \(w_0,w_2,...,w_5\) , the edges represent connecting paths, a red-dashed line means that the path is dangerous enough to make the UAV stop working with probability 1, while on any other path, this probability is \(S\) . Checkpoints are depicted as pink nodes, therein the operator can still delegate the piloting task to the UAV with probability \(D\) . Each node is annotated with three possible rewards. For instance, for \(S=0.3\)  and \(D=0.5\)  and the leftmost reward values in each triple, the synthesized strategy for the UAV tries to follow the optimal circuit \(w_0,w_1,w_2,w_3,w_4,w_5\) . While for the middle and rightmost reward values, the optimal circuits to follow are \(w_0,w_5,w_0,w_1,w_2,w_3,w_4\)  and \(w_0,w_5,w_4,w_1,w_2,w_3\) , respectively. Table REF  shows the results obtained for this game for several randomly generated road networks.
All the experiments were run on a MacBook Air with Intel Core i5 at 1.3 GHz and 4 Gb of RAM. The tool and case studies are available in the tool repository.
<TABLE><TABLE>
Related Work
Stochastic games with payoff functions have been extensively investigated in the literature. In [2]}, several results are presented about transient games,
a generalized version of stopping stochastic games with total reward payoff.
In transient games, both players possess optimal (memoryless and deterministic) strategies.
Most importantly, the games are determined and their value can be computed as the least fixed point of a set of equations.
Most of these results are based on the fact that the \(\Gamma \)  functional (see Section ) for transient games has a unique fixed point.
Notice that in this paper we have dealt with games that are stopping only under fairness assumptions. Thus, the corresponding functional
may have several fixed points. Hence, the main results presented in [2]} do not apply to our setting.
[24]} and [25]} present logical frameworks for the verification and synthesis of systems. While [24]} provides a solution for a probabilistic branching temporal logic extended with expected total, discounted, and average reward objective functions, [25]} does the same in a similar extension of a probabilistic linear temporal logic. Both frameworks were implemented in the tool Prism [20]}. Although a vast class of properties can be expressed in these frameworks, none of them are presented under fair environments. In fact, these works are on stochastic multiplayer games in which each player is treated equally.
Stochastic shortest path games [3]} are two-player stochastic games with (negative or positive) rewards in which the minimizer's strategies are classified into proper and improper,
proper strategies are those ensuring termination. As proven in [3]}, these games are determined, and both players posses memoryless optimal strategies. To prove these results, the authors assume that the expected game value for improper strategies is \(\infty \) , this ensures that the corresponding functional is a contraction and thus it has a unique fixpoint. In contrast, we restrict ourselves to non-negative rewards but we do not make any assumptions over unfair strategies, as mentioned above the corresponding functional for our games may have several fixpoints. Furthermore, we proved that the value of the game is given by the greatest fixpoint of \(\Gamma \) . In recent years, several authors have investigated stochastic shortest path problems for MDPs (i.e, one-player games), where the assumption over improper strategies is relaxed (e.g., [31]}); to the best of our knowledge, these results have not be extended to two-player games.
In [32]} the authors tackle the problem of synthesizing a controller that maximizes the probability of satisfying an LTL property. Fairness strategies are used to reduce this problem to the synthesis of a controller maximizing a PCTL property over a product game. However, this article does not address expected rewards and game determinacy under fairness assumptions.
Interestingly, in [33]} the authors consider the problem of winning a (non-stochastic) two-player games with fairness assumptions over the environment. The objective of the system is to guarantee an \(\omega \) -regular property. The authors show that winning in these games is equivalent to almost-sure winning in a Markov decision process. It must be noted that this work only considers non-stochastic games. Furthermore, payoff functions are not considered therein.

Concluding remarks
In this paper, we have investigated the properties of stochastic games with total reward payoff under the assumption that the minimizer (i.e., the environment) plays only with fair strategies. We have shown that, in this scenario, determinacy is preserved and both players have optimal memoryless and deterministic strategies; furthermore, the value of the game can be calculated by approximating a greatest fixed point of a Bellman operator. We have only considered non-negative rewards in this paper. A possible way of extending the results presented here to games with negative rewards is to adapt the techniques presented in [31]} for MDPs with negative costs, we leave this as a further work.
In order to show the applicability of our technique, we have presented two examples of applications and an experimental evaluation over diverse instances of these case studies using our prototype tool. We believe that fairness assumptions allow one to consider more realistic behavior of the environment.
As future work, we plan to build a more robust tool and thus model and evaluate other case studies.
We have not investigated other common payoff functions such as discounted payoff or limiting-average payoff. A benefit of these classes of functions is that the value of games are well-defined even when the games are not stopping.
At first sight, the notion of fairness is little relevant for games with discounted payoff, since these kinds of payoff functions take most of their value from the initial parts of runs. For limiting-average the situation is different, and fairness assumptions may be relevant as they could change the value of games, we leave this as further work.
*proofofclaimProof of claim

Proofs
Fix strategies \(\pi _{1} \in \Pi _{1}\) , \(\pi _{2} \in \Pi ^{\mathcal {F}}_{2}\)  and a vertex \(v \in V\)  such that
\(\mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G}, v}(\Diamond T) < 1\) .
Note that we can define an MDP (named \(\mathcal {G}^{V_1{+}V_2}\) ) from
\(\mathcal {G}\)  by considering that \(V_1\)  and \(V_2\)  belong to the same
player. For this MDP consider the set \(U = \lbrace  (V^{\prime },\delta ^{\prime })\mid (V^{\prime },\delta ^{\prime }) \in \mathit {EC}(\mathcal {G}^{V_1{+}V_2}) \text{ and }V^{\prime }\cap T = \emptyset \rbrace \)  of end components not containing terminal
vertices. So, we define a strategy for this player combining
\(\pi _{1}\)  and \(\pi _{2}\)  (named \(\pi _{1}{+}\pi _{2}\) ) as
follows: it behaves as \(\pi _{1}\)  in finite paths ending in a state
of \(V_1\) , and behaves as \(\pi _{2}\)  in finite paths ending in a
state of \(V_2\) . Note that we have
\(\mathit {Prob}^{\pi _{1}{+}\pi _{2}}_{\mathcal {G}^{V_1+V_2},v}(\Diamond T) <1\) . By the limit properties of MDPs (Theorem 10.120 [35]})
we have that:
\(\mathit {Prob}^{\pi _{1}{+}\pi _{2}}_{\mathcal {G}^{V_1+V_2},v} \left(\lbrace  \omega \in \mathit {Paths}^{\pi _{1}{+}\pi _{2}}_{\mathcal {G}^{V_1+V_2},v} \mid \mathit {limit}(\omega ) \in U \rbrace \right) > 0,\) 
where \(\mathit {limit}(\omega )\)  denotes the end-component that is repeated
infinitely often in \(\omega \) , as defined in [35]}. Note
that, the fairness of \(\pi _{2}\)  and
(REF ) imply that there is a reachable
end component \(\mathcal {C}= (V^{\prime },\delta ^{\prime }) \in U\)  such that, for all
\(v^{\prime } \in V_2 \cap V^{\prime }\) , \(\mathit {post}^\delta (v^{\prime }) \subseteq V^{\prime }\)  \((\dag )\) .
This
can be proven by contradiction: if \((\dag )\)  does not hold we have
that for every end component in \(U\)  there must be some vertex in
\(V_2\)  such that some of its successors is not in the component; but,
since \(\pi _{2}\)  is fair, we should have
\(\mathit {Prob}^{\pi _{1}{+}\pi _{2}}_{\mathcal {G}^{V_1+V_2},v} \left( \lbrace  \omega \in \mathit {Paths}^{\pi _{1}{+}\pi _{2}}_{\mathcal {G}^{V_1+V_2},v} \mid \mathit {limit}(\omega ) \in U \rbrace \right) = 0\) 
contradicting (REF ). Thus \((\dag )\)  must hold.
Hence, there is some finite path \(\hat{\omega } = v_0 v_1 v_2 \dots v_k\) 
in this MDP such that \(v_i \notin T\)  for every \(i\) , \(v_k \in V^{\prime }\) , and
\(\mathit {Prob}^{\pi _{1}{+}\pi _{2}}_{\mathcal {G}^{V_1+V_2},v}(v_0\dots v_k) > 0\) .
Now, we define \(\pi _{1}^{\prime }\)  as follows:
\(\pi _{1}^{\prime }(v^{\prime }) = \hat{\omega }_{i+1}\) , if \(i < k\)  is the largest
index such that \(v^{\prime } = \hat{\omega }_{i}\) ;
\(\pi _{1}^{\prime }(v^{\prime }) = v^{\prime \prime }\)  for some arbitrary \(v^{\prime \prime } \in V^{\prime }\cap \mathit {post}^\delta (v)\) , if \(v^{\prime } \in V^{\prime }\) ;
otherwise \(\pi _{1}^{\prime }(v^{\prime }) = v^{\prime \prime }\)  for some arbitrary
\(v^{\prime \prime } \in \mathit {post}^\delta (v^{\prime })\) .
\(\pi _{2}^{\prime }\)  is defined as the uniform strategy, that is:
\(\pi _{2}^{\prime }(v^{\prime })(v^{\prime \prime }) = \frac{1}{\# \mathit {post}^\delta (v^{\prime })}\) , for every \(v^{\prime }\in V_2\)  and \(v^{\prime \prime } \in \mathit {post}^\delta (v^{\prime })\) .
\(\pi _{1}^{\prime }\)  is defined such that it jumps ahead on \(\hat{\omega }\) 
skipping all possible loops introduced by \(\pi _{1}\) . Let
\(\hat{\omega }{\downharpoonleft }_{\pi _{1}^{\prime }}\)  be the finite path
obtained by following \(\hat{\omega }\)  skipping all loops according
to \(\pi _{1}^{\prime }\) .
Note that \(\hat{\omega }{\downharpoonleft }_{\pi _{1}^{\prime }}\)  is a valid
path in \(\mathcal {G}\) , that it still ends in state \(v_k\) , and that
\(\mathit {Prob}^{\pi _{1}^{\prime },\pi _{2}^{\prime }}_{\mathcal {G},v}({\hat{\omega }{\downharpoonleft }_{\pi _{1}^{\prime }}})>0\) .
Moreover, by (\(\dag \) ) and the definition of \(\pi _{1}^{\prime }\) , we have
that \(\mathit {Prob}^{\pi _{1}^{\prime },\pi _{2}^{\prime }}_{\mathcal {G}, v_k}(\Box V^{\prime }) = 1\) .
Thus \(\mathit {Prob}^{\pi _{1}^{\prime },\pi _{2}^{\prime }}_{\mathcal {G}, v}(\Diamond T) < 1\) .
Furthermore, note that \(\pi _{1}^{\prime }\)  is memoryless and \(\pi _{2}^{\prime }\) 
is fair.
\(\Box \)
“If”: Suppose that \(\mathit {Prob}^{\pi _{1}, \pi ^{\mathrm {u}}_{2}}_{\mathcal {G},v}(\Diamond T)=1\)  for every Player 1's strategy \(\pi _{1}\) . Moreover,
assume, for the sake of contradiction, that
\(\mathit {Prob}^{\pi _{1}^{\prime }, \pi _{2}^{\prime }}_{\mathcal {G},v}(\Diamond T) < 1\)  for some \(\pi _{1}^{\prime }\in \Pi _{1}\)  and \(\pi _{2}^{\prime }\in \Pi ^{\mathcal {F}}_{2}\) .
By Lemma REF , we can safely assume that \(\pi _{1}^{\prime }\)  is memoryless and deterministic.
Thus, by fixing \(\pi _{1}^{\prime }\) , we obtain a (finite) Markov decision process denoted \(\mathcal {G}^{\pi _{1}^{\prime }}\) .
By assumption, we have that
\(\inf _{\pi _{2} \in \Pi ^{\mathcal {F}}_{2}} \mathit {Prob}^{\pi _{2}}_{\mathcal {G}^{\pi _{1}^{\prime }},v}(\Diamond T) < 1 \) . In addition, by Theorem 10.133 in [35]}, we have that \(\inf _{ \pi _{2} \in \Pi ^{\mathcal {F}}_{2}}\mathit {Prob}^{\pi _{2}}_{\mathcal {G}^{\pi _{1}^{\prime }},v}(\Diamond T) = 1 - \sup _{\pi _{2} \in \Pi ^{\mathcal {F}}_{2}} \mathit {Prob}^{\pi _{2}}_{\mathcal {G}^{\pi _{1}^{\prime }},v}(\lnot T \mathbin {\textsf {U}}U)\) , where \(T\)  is the set of terminal states, \(\lnot T\)  is its complement, and
\(U = \bigcup \lbrace  V^{\prime } \mid (V^{\prime }, \delta ^{\prime }) \in \mathit {EC}(\mathcal {G}^{\pi _{1}^{\prime }}) \text{ and } T \cap V^{\prime } = \emptyset \rbrace \) .
Let \(\pi _{2}^{\prime \prime }\)  be the fair strategy that maximizes the value of \(\mathit {Prob}^{\pi _{2}^{\prime \prime }}_{\mathcal {G}^{\pi _{1}^{\prime }},v}(\lnot T \mathbin {\textsf {U}}U)\) , which exists as shown in the proof of Theorem 10.133 in [35]}.
Then we have that \(\mathit {Prob}^{\pi _{2}^{\prime \prime }}_{\mathcal {G}^{\pi _{1}^{\prime }},v}(\lnot T \mathbin {\textsf {U}}U) > 0\)  and hence
there is a path \(v_0 v_1 \dots v_n\)  with positive probability such that \(v_i \notin T\)  and \(v_n\)  belongs to an end-component \(\mathcal {C} = (V^{\prime \prime }, \delta ^{\prime \prime })\) 
such that \(T \cap V^{\prime \prime } = \emptyset \) . Since \(\pi _{2}^{\prime \prime }\)  is fair, by our definition of fair strategy, the end component \(\mathcal {C}\)  contains all the
transitions in \(\mathcal {G}^{\pi _{1}^{\prime }}\)  when restricted to \(V^{\prime \prime }\) .
Therefore, \(\mathit {Prob}^{\pi ^{\mathrm {u}}_{2}}_{\mathcal {G}^{\pi _{1}^{\prime }},v}(\Diamond V^{\prime \prime }) > 0\) , and
\(\mathit {Prob}^{\pi ^{\mathrm {u}}_{2}}_{\mathcal {G}^{\pi _{1}^{\prime }},v^{\prime \prime }}(\Box V^{\prime \prime }) = 1 \) 
from any state in \(v^{\prime \prime } \in V^{\prime \prime }\) , which implies that \(\mathit {Prob}^{\pi ^{\mathrm {u}}_{2}}_{\mathcal {G}{\pi _{1}^{\prime }},v}(\lnot T \mathbin {\textsf {U}}V^{\prime \prime }) > 0\) .
Hence, \(\mathit {Prob}^{\pi ^{\mathrm {u}}_{2}}_{\mathcal {G}^{\pi _{1}^{\prime }},v}(\Diamond T) < 1\) , which contradicts our initial assumption.
“Only If”: This part is direct since \(\pi ^{\mathrm {u}}_{2}\)  is a fair strategy.
\(\Box \)
(2) is an immediate consequence of (1). So, we only prove the first
statement.
Notice that
\(\mathcal {G}^{\pi ^{\mathrm {u}}_{2}} = (V, (V_1, \emptyset , {V_2 \cup V_\mathsf {P}}), \delta ^{\prime })\) ,
where \(\delta ^{\prime }(v,\cdot )=\delta (v,\cdot )\)  if \(v\in V_1\cup V_\mathsf {P}\) 
and \(\delta ^{\prime }(v,\cdot )=\pi ^{\mathrm {u}}_{2}(v)\)  if \(v\in V_2\) .
On this MDP, operators \(\forall \mathit {Pre}\)  and \(\exists \mathit {Pre}\)  are defined by
\(\exists \mathit {Pre}(C) \ = \ {}&\lbrace  v \in V \mid \delta ^{\prime }(v,C) > 0\rbrace  \\\forall \mathit {Pre}(C) \ = \ {}&\lbrace  v \in V_2\cup V_\mathsf {P}\mid \delta ^{\prime }(v,C) > 0\rbrace  \\&\cup \ \lbrace  v \in V_1 \mid \forall v^{\prime } \in V : \delta ^{\prime }(v,v^{\prime }) > 0 \Rightarrow v^{\prime } \in C \rbrace \) 

It is straightforward to verify that \(\exists \mathit {Pre}_f(C)=\exists \mathit {Pre}(C)\)  and
\(\forall \mathit {Pre}_f(C)=\forall \mathit {Pre}(C)\)  for any \(C\subseteq V\) .
As a consequence of this observation and
Theorem REF , it suffices to check that
\(\mathit {Prob}^{\pi _{1}}_{\mathcal {G}^{\pi ^{\mathrm {u}}_{2}},v}(\Diamond T)=1\)  for every
strategy \(\pi _{1}\)  iff
\(v \in V\setminus \exists \mathit {Pre}^*(V \setminus \forall \mathit {Pre}^*(T))\)  \((\ddag )\) .
By Lemma 10.110 [35]}, \(v\in V \setminus \forall \mathit {Pre}^*(T))\)  iff
\(\exists \pi _{1}\colon \mathit {Prob}^{\pi _{1}}_{\mathcal {G}^{\pi ^{\mathrm {u}}_{2}},v}(\Diamond T) = 0\) .
Therefore, \(v\in V \setminus \forall \mathit {Pre}^*(T))\)  iff
\(\exists \pi _{1}\colon \mathit {Prob}^{\pi _{1}}_{\mathcal {G}^{\pi ^{\mathrm {u}}_{2}},v}(\Box \lnot T) = 1\) .
Taking into account that all terminal states are absorbing, from Lemma 10.111 [35]}, \(v\in \exists \mathit {Pre}^*(V \setminus \forall \mathit {Pre}^*(T)))\)  iff
\(\exists \pi _{1}\colon \mathit {Prob}^{\pi _{1}}_{\mathcal {G}^{\pi ^{\mathrm {u}}_{2}},v}(\Diamond T) < 1\) 
from which \((\ddag )\)  follows.
\(\Box \)
Consider the event \(\Diamond ^{k} v^{\prime } = \lbrace  \omega \in \mathit {Paths}_\mathcal {G}\mid \omega _k = v^{\prime }\rbrace \) , for \(k\ge 0\) . That is,
the set of runs in which \(v^{\prime }\)  is reached in exactly \(k\)  steps.
We define \(\pi ^*_{1}\)  as follows:
\(\pi ^*_{1}(\hat{\omega }v^{\prime })(v^{\prime \prime }) = \mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\Diamond ^{k+1} v^{\prime \prime } \mid \Diamond ^k v^{\prime })\) 
for every \(\hat{\omega }\)  such that
\(\mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\hat{\omega }v^{\prime }) > 0\)  and
\(|\hat{\omega }v^{\prime }| = k\) . For \(\hat{\omega }\)  with
\(\mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\hat{\omega }v^{\prime }) = 0\)  we
define \(\pi ^*_{1}(\hat{\omega }v^{\prime })\)  to be any arbitrary
distribution.
We prove that this strategy satisfies the conditions of the theorem.
First, we prove that
\(\mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\Diamond ^{k} v^{\prime }) =\mathit {Prob}^{\pi ^*_{1}, \pi _{2}}_{\mathcal {G},v}(\Diamond ^{k} v^{\prime }).\) 
Notice that for \(k=0\)  we have that,
\(\mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\Diamond ^{0} v^{\prime }) =\mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(v^{\prime }) = \Delta _v(v^{\prime }) =\mathit {Prob}^{\pi ^*_{1}, \pi _{2}}_{\mathcal {G},v}(v^{\prime })=\mathit {Prob}^{\pi ^*_{1}, \pi _{2}}_{\mathcal {G},v}(\Diamond ^{0} v^{\prime }).\) 
For \(k + 1 > 0\) , we note that
\(\mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\Diamond ^{k+1} v^{\prime }) = \sum _{\hat{\omega } \in V^{k+1}} \mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\hat{\omega }v^{\prime }) = \sum _{v^{\prime \prime } \in \mathit {pre}(v^{\prime })}\sum _{\hat{\omega } \in V^k} \mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\hat{\omega }v^{\prime \prime }v^{\prime }),\) 
and hence, for this case, it sufficies to show that, for all
\(v^{\prime \prime }\in \mathit {pre}(v)\) ,
\(\sum _{\hat{\omega } \in V^k} \mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\hat{\omega }v^{\prime \prime }v^{\prime }) = \sum _{\hat{\omega } \in V^k} \mathit {Prob}^{\pi ^*_{1}, \pi _{2}}_{\mathcal {G},v}(\hat{\omega }v^{\prime \prime }v^{\prime }).\) 
The proof uses induction on \(k\)  doing case analysis. We observe that
the base case follows similarly to the inductive case and we
properly point it out when it corresponds.
If \(v^{\prime \prime } \in V_2\) , we proceed as follows.
\( \sum _{\hat{\omega } \in V^k}\mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\hat{\omega }v^{\prime \prime }v^{\prime })& = \sum _{\hat{\omega } \in V^k}\mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\hat{\omega }v^{\prime \prime }) \pi _{2}(\hat{\omega }v^{\prime \prime })(v^{\prime })\\& = \alpha \sum _{\hat{\omega } \in V^k}\mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\hat{\omega }v^{\prime \prime }) \\& = \alpha \sum _{\hat{\omega } \in V^k}\mathit {Prob}^{\pi ^*_{1}, \pi _{2}}_{\mathcal {G},v}(\hat{\omega }v^{\prime \prime }) \\& = \sum _{\hat{\omega } \in V^k}\mathit {Prob}^{\pi ^*_{1}, \pi _{2}}_{\mathcal {G},v}(\hat{\omega }v^{\prime \prime }v^{\prime })\) 

(REF ) follows by definition.
For (), we define \(\alpha =\pi _{2}(\hat{\omega }v^{\prime \prime })(v^{\prime })\)  if \(\hat{\omega }\)  starts at \(v\) . By
recalling that the semi-Markov nature of \(\pi _{2}\)  defines the
same \(\alpha \)  for any \(\hat{\omega }\in V^k\)  starting at \(v\) , and that
\(\mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\hat{\omega }v^{\prime \prime }) = 0\)  if
\(\hat{\omega }\)  does not start at \(v\) , \(\alpha \)  results to be common
factor.
() follows either by induction
hypothesis, or, in the base case, by observing that
\(\mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(v^{\prime \prime }) =\Delta _v(v^{\prime \prime })=\mathit {Prob}^{\pi ^*_{1}, \pi _{2}}_{\mathcal {G},v}(v^{\prime \prime })\) .
() resolves just like
().
For the case in which \(v^{\prime \prime } \in V_1\) , we proceed as follows.
\( \sum _{\hat{\omega } \in V^k}\mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\hat{\omega }v^{\prime \prime }v^{\prime }) \hspace{-60.0pt} & \\& = \sum _{\hat{\omega } \in V^k}\mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\hat{\omega }v^{\prime \prime }) \pi _{1}(\hat{\omega }v^{\prime \prime })(v^{\prime })\\& = \left( \sum _{\hat{\omega } \in V^k}\mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\hat{\omega }v^{\prime \prime }) \right) \frac{\displaystyle \sum _{\hat{\omega } \in V^k}\mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\hat{\omega }v^{\prime \prime }) \pi _{1}(\hat{\omega }v^{\prime \prime })(v^{\prime })}{\displaystyle \sum _{\hat{\omega } \in V^k}\mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\hat{\omega }v^{\prime \prime })} \\& = \sum _{\hat{\omega } \in V^k}\mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\hat{\omega }v^{\prime \prime }) \mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\Diamond ^{k+1} v^{\prime } \mid \Diamond ^k v^{\prime \prime }) \\& = \sum _{\hat{\omega } \in V^k}\mathit {Prob}^{\pi ^*_{1}, \pi _{2}}_{\mathcal {G},v}(\hat{\omega }v^{\prime \prime }) \pi ^*_{1}(\hat{\omega }v^{\prime \prime })(v)\\& = \sum _{\hat{\omega } \in V^k}\mathit {Prob}^{\pi ^*_{1}, \pi _{2}}_{\mathcal {G},v}(\hat{\omega }v^{\prime \prime }v^{\prime })\) 

(REF ) follows by definition.
() is obtained by multiplying and
dividing the term by
\(\sum _{\hat{\omega }v^{\prime \prime } \in V^k}\mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\hat{\omega }v^{\prime \prime })\) .
() follows from the definition of
conditional probability by noting that
\(\mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}({\Diamond ^{k+1} v^{\prime }} \cap {\Diamond ^k v^{\prime \prime }}) =\sum _{\hat{\omega } \in V^k}\mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\hat{\omega }v^{\prime \prime }) \pi _{1}(\hat{\omega }v^{\prime \prime })(v^{\prime })\) 
and
\(\mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\Diamond ^{k} v^{\prime \prime }) =\sum _{\hat{\omega } \in V^k}\mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\hat{\omega }v^{\prime \prime })\) .
Finally, () follows by the definition of
\(\pi ^*_{1}\)  and () by the
definition of \(\mathit {Prob}^{\pi ^*_{1}, \pi _{2}}_{\mathcal {G},v}\) .
The proof for case \(v^{\prime \prime } \in V_\mathsf {P}\)  follows just like for
the case first case, with the difference that instead of considering
\(\pi _{2}(\hat{\omega }v^{\prime \prime })(v^{\prime })\)  we need to consider
\(\delta (v^{\prime \prime },v^{\prime })\) .
Now, we have:
\(\mathbb {E}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}] & = \sum ^\infty _{N=0} \sum _{\hat{\omega } \in V^{N+1}} \mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\hat{\omega })\mathit {r}(\hat{\omega }_N)\\& = \sum ^\infty _{N=0} \sum _{v \in V} \mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\Diamond ^N v)\mathit {r}(v) \\& = \sum ^\infty _{N=0} \sum _{v \in V} \mathit {Prob}^{\pi ^*_{1}, \pi _{2}}_{\mathcal {G},v}(\Diamond ^N v)\mathit {r}(v) \\& = \mathbb {E}^{\pi ^*_{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}]\) 

\(\Box \)
Since \(\pi _{1}\)  and \(\pi _{2}\)  are memoryless, we can fix these
strategies and obtain an absorbing finite Markov chain
\(\mathcal {G}^{\pi _{1},\pi _{2}} = (V, (\emptyset ,\emptyset , V_1 \cup V_2 \cup V_P), \delta ^{\pi _{1}, \pi _{2}})\) ,
then the result follows from basic properties of Markov chains. For
the sake of completeness, we provide a proof.
Let \(|V|\)  be the number of states of the MC
\(\mathcal {G}^{\pi _{1},\pi _{2}}\)  and \(T\)  its set of terminal
vertices.
Because \(\mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\Diamond T) = 1\) 
and the MC is finite, from any vertex, we have a path of length \(k\) 
with \(k \le |V|\)  to a terminal vertex.
Furthermore, let
\(\lambda = \min \lbrace  \delta ^{\pi _{1},\pi _{2}}(v,v^{\prime }) > 0 \mid v,v^{\prime } \in V \rbrace \) ,
which is well-defined since \(\mathcal {G}^{\pi _{1},\pi _{2}}\)  has a finite
number of states. Thus for any \(N\ge 0\)  we have:
\(\sum _{\hat{\omega } \in (V \setminus T)^{N+1}} \mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\hat{\omega }) \le (1 - \lambda ^{|V|})^{\left\lfloor {\frac{N}{|V|}}\right\rfloor }\) 
Thus, if \(\lambda <1\) ,
\(\sum ^\infty _{N=0}\sum _{\hat{\omega } \in (V \setminus T)^{N+1}} \mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\hat{\omega }) & \ \le \ \sum ^{\infty }_{N=0}(1 - \lambda ^{|V|})^{\left\lfloor {\frac{N}{|V|}}\right\rfloor } \\& \ = \ {|V|}\sum ^{\infty }_{i=0}(1 - \lambda ^{|V|})^i \ = \ \frac{|V|}{1 - \lambda ^{|V|}}.\) 

If \(\lambda = 1\) , it is easy to check that
\(\sum ^\infty _{N=0}\sum _{\hat{\omega } \in (V \setminus T)^{N+1}} \mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\hat{\omega }) \le {|V|}\) .
\(\Box \)
Rather than prooducing the approriate reductions to apply Theorem
4.2.12 in [2]}, we produce a direct proof based
on the ideas of the proof of that Theorem.
Fix a fair strategy \(\pi _{2} \in \Pi ^{M\mathcal {F}}_{2}\)  and
consider the MDP
\(\mathcal {G}^\pi _{2} = (V, (V_1, \emptyset , V_2 \cup V_\mathsf {P}), \delta ^{\pi _{2}})\) .
Define the following functional:
\(\Gamma ^{\prime }(f)(v) ={\left\lbrace \begin{array}{ll}\sum _{v^{\prime } \in \mathit {post}(v)} \delta ^\pi _{2}(v,v^{\prime }) f(v^{\prime }) & \text{ if } v \in V_2 \cup V_\mathsf {P}\\\max \lbrace 1 + f(v^{\prime }) \mid v^{\prime } \in \mathit {post}(v) \rbrace  & \text{ if } v \in V_1 \setminus T \\0 & \text{ if } v \in T.\end{array}\right.}\) 
It is well-known that, since \(\mathcal {G}^{\pi _{2}}\)  is stopping, this
functional is a contraction mapping and then it has a unique
fixpoint (see, e.g., proof of Theorem 4.2.2 in [2]}),
which gives us the optimal value for Player 1 in MDP
\(\mathcal {G}^{\pi _{2}}\) . Let \(\nu \)  denote the fixpoint of \(\Gamma ^{\prime }\) .
Since \(\nu (v_n)\)  is the optimal value for a given vertex \(v_{n}\) ,
we have that
\(\nu (v_n) \ge 1 + \sum _{v_{n+1} \in \mathit {post}(v_n)} \delta ^{\pi _{1}^n, \pi _{2}}(v_n, v_{n+1}) \nu (v_{n+1})\) 
for any memoryless strategy \(\pi _{1}^n\)  (the value obtained by the
fixpoint is optimal among memoryless strategies, thus it cannot be
improved by \(\pi _{1}^n\) ).
Take any sequence \(\hat{\omega } = v_0 \dots v_n\)  with
\(\hat{\omega }_n = v_n\)  and multiply
(REF ) by
\(\prod ^{n-1}_{i=0} \delta ^{\pi _{1}^i, \pi _{2}}(\hat{\omega }_i, \hat{\omega }_{i+1})\) 
on both sides. This yields
\(\prod ^{n-1}_{i=0} \delta ^{\pi _{1}^i, \pi _{2}}(\hat{\omega }_i, \hat{\omega }_{i+1}) \nu (\hat{\omega }_n) \hspace{-65.0pt}& \\\ge \ & \prod ^{n-1}_{i=0} \delta ^{\pi _{1}^i, \pi _{2}}(\hat{\omega }_i, \hat{\omega }_{i+1})  \\& + \ \prod ^{n-1}_{i=0} \delta ^{\pi _{1}^i, \pi _{2}}(\hat{\omega }_i, \hat{\omega }_{i+1})\sum _{v_{n+1} \in \mathit {post}(v_n)} \delta ^{\pi _{1}^n, \pi _{2}}(v_n, v_{n+1}) \nu (v_{n+1}) \) 

In the equation above, we assume
\(\prod ^{-1}_{i=0} \delta ^{\pi _{1}^i, \pi _{2}}(\hat{\omega }_i, \hat{\omega }_{i+1}) = 1\) 
for the case in which \(n=0\) .
Considering all sequences of length \(n+1\)  in \(v(V \setminus T)^n\) ,
from (REF ), and rewriting the last
line of the inequality, we get
\(\sum _{\hat{\omega } \in v(V \setminus T)^n}\prod ^{n-1}_{i=0} \delta ^{\pi _{1}^i, \pi _{2}}(\hat{\omega }_i, \hat{\omega }_{i+1}) \nu (\hat{\omega }_n) \hspace{-55.0pt}& \\\ge \ & \sum _{\hat{\omega } \in v(V \setminus T)^n}\prod ^{n-1}_{i=0} \delta ^{\pi _{1}^i, \pi _{2}}(\hat{\omega }_i, \hat{\omega }_{i+1}) \\& + \ \sum _{\hat{\omega } \in v(V \setminus T)^{n+1}}(\prod ^{n}_{i=0} \delta ^{\pi _{1}^i, \pi _{2}}(\hat{\omega }_i, \hat{\omega }_{i+1}) \nu (\hat{\omega }_{n+1})) \) 

Summing all the possible sequences up to \(N\)  we obtain
\(\sum ^{N}_{n=0}\sum _{\hat{\omega } \in v(V \setminus T)^n}\prod ^{n-1}_{i=0} \delta ^{\pi _{1}^i, \pi _{2}}(\hat{\omega }_i, \hat{\omega }_{i+1}) \nu (\hat{\omega }_n) \hspace{-65.0pt}& \\\ge \ & \sum ^{N}_{n=0} \sum _{\hat{\omega } \in v(V \setminus T)^n}\prod ^{n-1}_{i=0} \delta ^{\pi _{1}^i, \pi _{2}}(\hat{\omega }_i, \hat{\omega }_{i+1})  \\& + \ \sum ^{N}_{n=0} \sum _{\hat{\omega } \in v(V \setminus T)^{n+1}}(\prod ^{n}_{i=0} \delta ^{\pi _{1}^i, \pi _{2}}(\hat{\omega }_i, \hat{\omega }_{i+1}) \nu (\hat{\omega }_{n+1})) \) 

(REF ) can be equivalently rewritten
as
\(\sum ^{N}_{n=0}\sum _{\hat{\omega } \in v(V \setminus T)^n}\prod ^{n-1}_{i=0} \delta ^{\pi _{1}^i, \pi _{2}}(\hat{\omega }_i, \hat{\omega }_{i+1}) \nu (\hat{\omega }_n) \hspace{-65.0pt}& \\\ge \ & \sum ^{N}_{n=0} \sum _{\hat{\omega } \in v(V \setminus T)^n}\prod ^{n-1}_{i=0} \delta ^{\pi _{1}^i, \pi _{2}}(\hat{\omega }_i, \hat{\omega }_{i+1}) \\& + \ \sum ^{N+1}_{n=1} \sum _{\hat{\omega } \in v(V \setminus T)^{n}}(\prod ^{n-1}_{i=0} \delta ^{\pi _{1}^i, \pi _{2}}(\hat{\omega }_i, \hat{\omega }_{i+1}) \nu (\hat{\omega }_{n})) \) 

By subtracting
\(\sum ^{N+1}_{n=1} \sum _{\hat{\omega } \in v(V \setminus T)^{n}}(\prod ^{n-1}_{i=0} \delta ^{\pi _{1}^i, \pi _{2}}(\hat{\omega }_i, \hat{\omega }_{i+1}) \nu (v_{n}))\) 
from both sides of the inequality
(REF ), we get
\(\nu (v) - \sum _{\hat{\omega } \in v(V \setminus T)^{N+1}}\prod ^{N}_{i=0} \delta ^{\pi _{1}^i, \pi _{2}}(\hat{\omega }_i,\hat{\omega }_{i+1}) \nu (\hat{\omega }_{N+1}) \hspace{-65.0pt}& \\\ge \ & \sum ^{N}_{n=0} \sum _{\hat{\omega } \in v(V \setminus T)^n}\prod ^{n-1}_{i=0} \delta ^{\pi _{1}^i, \pi _{2}}(\hat{\omega }_i, \hat{\omega }_{i+1}) \) 

Applying limits to both sides of the inequality
(REF ) we obtain
\(\nu (v) - \lim _{N \rightarrow \infty } \sum _{\hat{\omega } \in v(V \setminus T)^{N+1}}\prod ^{N}_{i=0} \delta ^{\pi _{1}^i, \pi _{2}}(\hat{\omega }_i,\hat{\omega }_{i+1}) \mathit {val}(\hat{\omega }_{N+1}) \hspace{-85.0pt}& \\\ge \ & \lim _{N \rightarrow \infty } \sum ^{N}_{n=0} \sum _{\hat{\omega } \in v(V \setminus T)^n}\prod ^{n-1}_{i=0} \delta ^{\pi _{1}^i, \pi _{2}}(\hat{\omega }_i, \hat{\omega }_{i+1}) \) 

Now, by Lemma REF , \(\nu (v)\)  is
bounded for every \(v\) . In addition,
\(\lim _{N \rightarrow \infty }\sum _{\hat{\omega } \in v(V \setminus T)^{N+1}}\prod ^{N}_{i=0} \delta ^{\pi _{1}^i, \pi _{2}}(v_i,v_{i+1}) \nu (v_{N+1}) = 0,\) 
Thus, the right term of the inequality
(REF ) is a finite number. That means
that for every sequence of memoryless strategies
\(\pi _{1}^0,\pi _{1}^1, \dots \)  we get
\(\lim _{N \rightarrow \infty } \sum ^{N}_{n=0} \sum _{\hat{\omega } \in v(V \setminus T)^n}\prod ^{n-1}_{i=0} \delta ^{\pi _{1}^i, \pi _{2}}(\hat{\omega }_i, \hat{\omega }_{i+1}) < \infty ,\) 
Noting that any semi-Markov strategy \(\pi _{1}^{\prime }\)  can be seen as a
sequence of memoryless strategies, it follows that
\(\lim _{N \rightarrow \infty } \sum ^{N}_{n=0} \sum _{\hat{\omega } \in v(V \setminus T)^n} \mathit {Prob}^{\pi _{1}^{\prime }}_{\mathcal {G}^{\pi _{2}}, v}(\hat{\omega }) < \infty ,\) 
for any \(\pi _{1}^{\prime }\)  semi-Markovian. Furthermore, since every
strategy \(\pi _{1}\)  has an equivalent semi-Markov strategy (see
proof of Theorem REF ), the result follows.
\(\Box \)
Take \(M = \max \lbrace r(v) \mid v \in V\rbrace \) . This number is well defined
since the number of vertices is finite.
The expected value of the game under strategies
\(\pi _{1} \in \Pi _{1}\)  and \(\pi _{2} \in \Pi ^{\mathcal {F}}_{2}\) 
is given by
\( \mathbb {E}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}]& = \sum ^{\infty }_{N=0} \sum _{\hat{\omega } \in V^{N+1}} \mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\hat{\omega })\mathit {r}(\hat{\omega }_N) \\ & = \sum ^{\infty }_{N=0} \ \ \sum _{\hat{\omega } \in (V^{N+1} \cap (V \setminus T)^*T)} \mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\hat{\omega }) \mathit {r}(\hat{\omega }_N) \ \ + \\&\hspace*{40.0pt} \sum _{\hat{\omega } \in (V^{N+1} \cap (V \setminus T)^*)} \mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\hat{\omega }) \mathit {r}(\hat{\omega }_N) \\& = \sum ^{\infty }_{N=0} (\sum _{\hat{\omega } \in V^{N+1} \cap (V \setminus T)^*} \mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\hat{\omega }) \mathit {r}(\hat{\omega }_N) ) \\& \le M \sum ^{\infty }_{N=0} \sum _{\hat{\omega } \in V^{N+1} \cap (V \setminus T)^*} \mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\hat{\omega }) \\& < \infty \) 

(REF ) is the
definition of the expected value.
The fact that \(V^{N+1} \cap (V \setminus T)^*T\)  and
\(V^{N+1} \cap (V \setminus T)^*\)  are disjoint justifies
().
() follows
from the assumption that \(\mathit {r}(v) = 0\)  for all \(v \in T\)  and
() from the
definition of \(M\) .
Finally, ()
is a consequence of Theorem REF .
\(\Box \)
By fixing strategy \(\pi _{1}\)  on \(\mathcal {G}\)  we obtain the MDP
\(\mathcal {G}^{\pi _{1}} = (V, (\emptyset ,V_2,V_1\cup V_\mathsf {P}),\delta ^{\pi _{1}})\) 
where \(\delta ^{\pi _{1}}(v,\cdot )=\pi _{1}(v)\)  if \(v\in V_1\) , and
\(\delta ^{\pi _{1}}(v,\cdot )=\delta (v,\cdot )\)  if \(v\in V_2\cup V_\mathsf {P}\) .
Notice that the set \(V_1\)  of Player 1 vertices in \(\mathcal {G}\)  became
part of the probabilistic vertices of \(\mathcal {G}^{\pi _{1}}\) . Thus,
non-deterministic choices can only be present at vertices in \(V_2\) .
By definition,
\(\inf _{\pi _{2} \in \Pi ^{\mathcal {F}}_{2}} \mathbb {E}^{\pi _{2}}_{\mathcal {G}^{\pi _{1}},v}[\textit {rew}] =\inf _{\pi _{2} \in \Pi ^{\mathcal {F}}_{2}} \mathbb {E}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}]\) 
for all \(v\in V\) .
Though the proof in general differs, the basic strategy is inspired
by the proof of Lemma 10.102 in [35]}: We first construct
a reduced MDP \(\mathcal {G}^{\pi _{1}}_{\min }\)  which preserves the
optimizing values of \(\mathcal {G}^{\pi _{1}}\)  at each vertex, and then
use the structure of \(\mathcal {G}^{\pi _{1}}_{\min }\)  to derive an
optimal deterministic memoryless strategy.
For all \(v\in V\) ,
let \(x_v = \inf _{\pi _{2} \in \Pi ^{\mathcal {F}}_{2}} \mathbb {E}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}]\)  (by Corollary REF  this value is well-defined) and,
for all \(v\in V_2\) , let
\(\mathit {post}^{\min }(v) = \lbrace {v^{\prime }\in V} \mid {\delta ^{\pi _{1}}(v,v^{\prime })=1} \wedge {x_v=\mathit {r}(v)+x_{v^{\prime }}}\rbrace .\) 
We define the MDP
\(\mathcal {G}^{\pi _{1}}_{\min } = (V, (\emptyset ,V_2,V_1\cup V_\mathsf {P}),\delta ^{\pi _{1}}_{\min })\) 
where \(\delta ^{\pi _{1}}_{\min }(v,v^{\prime })=\delta ^{\pi _{1}}(v,v^{\prime })\)  if \(v\in V_1\cup V_\mathsf {P}\) , or \(v\in V_2\)  and \(v^{\prime }\in \mathit {post}^{\min }(v)\) . Otherwise
\(\delta ^{\pi _{1}}_{\min }(v,v^{\prime })=0\) .
Thus, \(\mathcal {G}^{\pi _{1}}_{\min }\)  is the same as \(\mathcal {G}^{\pi _{1}}\)  except that all
transitions \(\delta ^{\pi _{1}}(v,v^{\prime })=1\)  where \(v\in V_2\)  and
\(x_v < \mathit {r}(v)+x_{v^{\prime }}\)  have been removed.
Notice that
\(\inf _{\pi _{2} \in \Pi ^{\mathcal {F}}_{2}} \mathbb {E}^{\pi _{2}}_{\mathcal {G}^{\pi _{1}}_{\min },v}[\textit {rew}] =\inf _{\pi _{2} \in \Pi ^{\mathcal {F}}_{2}} \mathbb {E}^{\pi _{2}}_{\mathcal {G}^{\pi _{1}},v}[\textit {rew}] =x_v\) 
for all \(v\in V\) .
Before continuing, we prove the following claim

\(\mathcal {G}^{\pi _{1}}_{\min }\)  is stopping under fairness.


We proceed by contradiction. Suppose that there is a fair
strategy \(\pi _{2}^{\prime }\)  such that, for some node \(v \in V\)  we have
\(\mathit {Prob}^{\pi _{2}^{\prime }}_{\mathcal {G}_{\min }^{\pi _{1}},v}(\Diamond T) < 1\) .
Hence, \(\mathit {Prob}^{\pi _{2}^{\prime }}_{\mathcal {G}_{\min }^{\pi _{1}},v}(\Box \lnot T) > 0\) .
This implies that there is an end component \(\mathcal {C} = (V^{\prime },\delta ^{\prime })\)  in the MDP \(\mathcal {G}_{\min }^{\pi _{1}}\)  such that
\(T \cap V^{\prime } = \emptyset \)  and
\(\mathit {Prob}^{\pi _{2}^{\prime }}_{\mathcal {G}_{\min }^{\pi _{1}},v}(\Diamond V^{\prime }) > 0\) 
(Theorem 10.133 [35]}).
Since \(\mathcal {G}_{\min }^{\pi _{1}}\)  is a sub-MDP of
\(\mathcal {G}^{\pi _{1}}\) , \(\mathcal {C}\)  is also an end component of
\(\mathcal {G}^{\pi _{1}}\) .
Also, note that \(\mathcal {C}\)  cannot be a maximal end component in
\(\mathcal {G}^{\pi _{1}}\) , otherwise we have found a fair strategy
reaching a maximal end component and not reaching \(T\) , thus
violating the assumption that \(\mathcal {G}\)  is stopping under
fairness.
Let \(m = \min \lbrace  x_{v^{\prime }} \mid v^{\prime } \in V^{\prime } \rbrace \)  and
\(\hat{v} \in \operatornamewithlimits{argmin}\lbrace  x_{v^{\prime }} \mid v^{\prime } \in V^{\prime } \rbrace \) .
If \(\hat{v}\in V_2\) , by definition of \(\mathit {post}^{\min }(v)\) ,
\(x_{\hat{v}} = \mathit {r}(\hat{v}) + x_{v^{\prime }}\) , for all
\(v^{\prime } \in \mathit {post}^{\min }(v)\) , and hence, necesaryly \(\mathit {r}(\hat{v})=0\) 
and \(x_{\hat{v}} = x_{v^{\prime }}\)  since all values are non-negative.
The same holds in case \(\hat{v}\)  is a probabilistic vertex,
because \(x_{\hat{v}}\)  depends on the convex combination of the
values of its successors.
Thus, inductively, \(x_{\hat{v}} = x_{v^{\prime }}\)  and \(\mathit {r}(v^{\prime })=0\)  for
all \(v^{\prime }\in V^{\prime }\) .
Now, let
\(M = \min \lbrace  \inf _{\pi _{2} \in \Pi ^{\mathcal {F}}_{2}} \mathbb {E}^{\pi _{2}}_{\mathcal {G}^{\pi _{1}},v^{\prime }}[\textit {rew}] \mid v^{\prime } \in (\mathit {post}(V^{\prime }) \setminus V^{\prime })\rbrace \) 
and
\(F=\lbrace v \in V \mid v \in (\mathit {post}(V^{\prime }) \setminus V^{\prime })\rbrace \) .
Note that, by definition of \(\mathcal {G}_{min}^{\pi _{1}}\) , we have that \(M > m\) .
Set \(\epsilon = \frac{M -m}{2}\)  and consider an \(\epsilon \) -optimal
strategy \(\hat{\pi _{2}}\)  for vertex \(\hat{v}\) , i.e.,
\(\mathbb {E}^{\hat{\pi _{2}}}_{\mathcal {G}^{\pi _{1}},\hat{v}}[\textit {rew}] \le x_{\hat{v}} + \epsilon \) .
Note that, since \(\mathcal {G}^{\pi _{1}}\)  is stopping under fairness,
when using strategy \(\hat{\pi _{2}}\) , any play almost surely
leaves \(\mathcal {C}\)  (recall that \(V^{\prime } \cap T = \emptyset \) ) and hence
\(\mathit {Prob}^{\hat{\pi _{2}}}_{\mathcal {G}^{\pi _{1}},\hat{v}} (\Diamond F) = 1\) .
Since all the rewards of the vertices in \(\mathcal {C}\)  are 0 (as
proven above) we can show that
\(\mathbb {E}^{\hat{\pi _{2}}}_{\mathcal {G}^{\pi _{1}},\hat{v}}[\textit {rew}]\ge M\)  as follows:
\( \mathbb {E}^{\hat{\pi _{2}}}_{\mathcal {G}^{\pi _{1}},\hat{v}}[\textit {rew}] \hspace{-40.0pt} & \\&= \sum _{\hat{\omega } \in (V \setminus T)^*T} \mathit {Prob}^{\hat{\pi _{2}}}_{\mathcal {G}^{\pi _{1}},\hat{v}}(\hat{\omega })\ \textit {rew}(\hat{\omega }) \\&=\sum _{\hat{\omega } \in \hat{v}{V^{\prime }}^*F(V \setminus T)^*T} \mathit {Prob}^{\hat{\pi _{2}}}_{\mathcal {G}^{\pi _{1}},\hat{v}}(\hat{\omega })\ \textit {rew}(\hat{\omega }) \\&= \sum _{v^{\prime } \in F} \sum _{\hat{\omega } \in \hat{v}{V^{\prime }}^*v^{\prime }} \mathit {Prob}^{\hat{\pi _{2}}}_{\mathcal {G}^{\pi _{1}},\hat{v}}(\hat{\omega }) \sum _{\hat{\omega }^{\prime } \in v^{\prime } (V \setminus T)^*T} \mathit {Prob}^{\hat{\pi _{2}}}_{\mathcal {G}^{\pi _{1}},v^{\prime }}(\hat{\omega }^{\prime })\ \textit {rew}(\hat{\omega }^{\prime })\\&\ge \sum _{v^{\prime } \in F} \sum _{\hat{\omega } \in \hat{v}{V^{\prime }}^*v^{\prime }} \mathit {Prob}^{\hat{\pi _{2}}}_{\mathcal {G}^{\pi _{1}},\hat{v}}(\hat{\omega })\ x_{v^{\prime }} \\&\ge \sum _{v^{\prime } \in F} \sum _{\hat{\omega } \in \hat{v}{V^{\prime }}^*v^{\prime }} \mathit {Prob}^{\hat{\pi _{2}}}_{\mathcal {G}^{\pi _{1}},\hat{v}}(\hat{\omega })\ M \\&= M \sum _{v^{\prime } \in F} \sum _{\hat{\omega } \in \hat{v}{V^{\prime }}^*v^{\prime }} \mathit {Prob}^{\hat{\pi _{2}}}_{\mathcal {G}^{\pi _{1}},\hat{v}}(\hat{\omega }) \\&= M\) 

(REF ) is the definition of expectation.
() follows by the observation that
any path \(\hat{\omega } \in (V \setminus T)^*T\)  needs to start in
\(\hat{v}\in V^{\prime }\)  and needs to pass through the frontier \(F\)  to
leave \(\mathcal {C}\)  and reach some terminal state in \(T\) .
() is obtained by taking into account
that \(\mathit {r}(v) = 0\)  for any \(v \in V^{\prime }\) .
() follows from the fact that
\(x_{v^{\prime }} \le \sum _{\hat{\omega }^{\prime } \in v^{\prime } (V \setminus T)^*T} \mathit {Prob}^{\hat{\pi _{2}}}_{\mathcal {G}^{\pi _{1}},v^{\prime }}(\hat{\omega }^{\prime })\ \textit {rew}(\hat{\omega }^{\prime })\) .
() follows by the definition of \(M\)  and
() by factorizing \(M\) .
Finally, () follows from the fact
\(\sum _{v^{\prime } \in F} \sum _{\hat{\omega } \in \hat{v}{V^{\prime }}^*v^{\prime }} \mathit {Prob}^{\hat{\pi _{2}}}_{\mathcal {G}^{\pi _{1}},\hat{v}}(\hat{\omega }) =\mathit {Prob}^{\hat{\pi _{2}}}_{\mathcal {G}^{\pi _{1}},\hat{v}} (\Diamond F) = 1\) .
Thus we have that
\(x_{\hat{v}} + \epsilon \ge \mathbb {E}^{\hat{\pi _{2}}}_{\mathcal {G}^{\pi _{1}},\hat{v}}[\textit {rew}] \ge M\) .
Since also \(M > x_{\hat{v}} + \epsilon \) , we reach a contradiction.
Hence \(\mathcal {G}^{\pi _{1}}_{\min }\)  must be stopping under fairness.
(End of claim)\(\Box \)
For every \(v\in V\) , let \({\Vert {v}\Vert }\)  be the length of the shortest
path fragment to some terminal vertex in \(T\)  in the MDP
\(\mathcal {G}^{\pi _{1}}_{\min }\) . In
particular, \({\Vert {v}\Vert }=0\)  for all \(v\in T\) . Notice that \({\Vert {v}\Vert }\)  is defined for all
\(v\in V\)  because \(\mathcal {G}^{\pi _{1}}_{\min }\)  inherits from \(\mathcal {G}\)  the
property of being stopping under fair strategies (and hence almost
surely reaches \(T\)  for any fair strategy in \(\Pi ^{\mathcal {F}}_{2}\) ).
Now, for every \(v\in V_2\) 
such that \({\Vert {v}\Vert } \ge 1\) , define \(\pi ^*_{2}(v)(v^{\prime })=1\) 
for some \(v^{\prime }\)  such that \(\delta ^{\pi _{1}}_{\min }(v,v^{\prime })=1\)  and
\({\Vert {v}\Vert }={\Vert {v^{\prime }}\Vert }+1\) ; and \(\pi ^*_{2}(v)(v^{\prime \prime })=0\)  for \(v^{\prime \prime }\ne v^{\prime }\) . Notice that such \(v^{\prime }\)  always exists,
and that \(\pi ^*_{2}\)  is a memoryless and deterministic
strategy.
\(\pi ^*_{2}\)  induces the (finite) Markov chain
\(\mathcal {G}^{\pi _{1},\pi ^*_{2}} = (V, (\emptyset ,\emptyset ,V_1\cup V_2\cup V_\mathsf {P}),\delta ^{\pi _{1},\pi ^*_{2}})\) ,
where
\(\delta ^{\pi _{1},\pi ^*_{2}}(v,v^{\prime }) ={\left\lbrace \begin{array}{ll}\delta (v,v^{\prime }) & \text{ if } v\in V_\mathsf {P}\\\pi _{1}(v)(v^{\prime }) & \text{ if } v\in V_1 \\\pi ^*_{2}(v)(v^{\prime }) & \text{ if } v\in V_2.\end{array}\right.}\) 
Taking into account the definition of \(\delta ^{\pi _{1},\pi ^*_{2}}\) ,
the expected reward values
\(\mathbb {E}^{}_{\mathcal {G}^{\pi _{1},\pi ^*_{2}},v}[\textit {rew}]\)  are obtained
by the unique solution of the following linear equation system:
\(y_v = {} & 0 && \text{ if } v\in T \\y_v = {} &\textstyle \mathit {r}(v) + \sum _{v\in V} \delta (v,v^{\prime }) \cdot y_{v^{\prime }} && \text{ if } v\in V_\mathsf {P}\setminus T\\y_v = {} &\textstyle \mathit {r}(v) + \sum _{v\in V} \pi _{1}(v)(v^{\prime }) \cdot y_{v^{\prime }} && \text{ if } v\in V_1 \setminus T\\y_v = {} & \mathit {r}(v) + y_{v^{\prime }} && \text{ if } v\in V_2 \setminus T \text{ and } \pi ^*_{2}(v)(v^{\prime }) = 1\) 

To see that this equation system has a unique solution, consider its
matrix form \(y = Ay+ r\) , wherein \(A\)  is a matrix defined by
\(A_{i,j} = \delta ^{\pi _1,\pi ^*_2}(v_i,v_j)\)  if \(v_i \notin T\)  and
\(A_{i,j} = 0\)  if \(v_i \in T\) , and \(r\)  is the reward vector where
\(r_i = \mathit {r}(v_i)\) .
\(A\)  is a square substochastic matrix
[45]} in which there is a path from
any vertex to a terminal vertex.
Thus, by Corollary 2.6 in [45]},
\((I-A)^{-1}\)  exists and hence \((I-A)^{-1} r\)  is the unique solution
to the equation system given above.
Since \(\pi ^*_{2}(v)(v^{\prime }) = 1\)  implies that \(v^{\prime }\in \mathit {post}^{\min }(v)\) ,
it follows that \((x_v)_{v\in V}\)  also solves the equation system
above. By uniqueness of the solution we get
\(\mathbb {E}^{\pi _{1}, \pi ^*_{2}}_{\mathcal {G},v}[\textit {rew}] =\mathbb {E}^{}_{\mathcal {G}^{\pi _{1},\pi ^*_{2}},v}[\textit {rew}] =y_v = x_v =\inf _{\pi _{2} \in \Pi ^{\mathcal {F}}_{2}} \mathbb {E}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}].\) 
In the last step of the proof we show \(\pi ^*_{2}\)  is fair.
By contradiction, suppose this is not the case. Hence,
\(\mathit {Prob}^{\pi _{1}, \pi ^*_{2}}_{\mathcal {G},v}(\mathit {FP}^2) < 1\)  for some
\(v\in V\) . Thus, there must exist vertices \(\hat{v}\in V_2\) 
and \(\hat{v}^{\prime }\in \mathit {post}(\hat{v})\)  such that
\(\mathit {Prob}^{\pi _{1}, \pi ^*_{2}}_{\mathcal {G},v}({\Box \Diamond \hat{v}}\wedge {\Diamond \Box \lnot \hat{v}^{\prime }})>0\) ,
where
\({\Box \Diamond \hat{v}}\wedge {\Diamond \Box \lnot \hat{v}^{\prime }} =\lbrace  {\omega \in \mathit {Paths}_{\mathcal {G}}} \mid {\hat{v} \in \inf (\omega )} \wedge {\hat{v}^{\prime } \notin \inf (\omega )} \rbrace \) .
By Theorem 10.56 in [35]}, there is a BSCC
\(B\)  in \(\mathcal {G}^{\pi _{1},\pi ^*_{2}}\)  satisfying \(\hat{v}\in B\)  and \(\hat{v}^{\prime }\notin B\) , such that
\(\mathit {Prob}^{\pi _{1}, \pi ^*_{2}}_{\mathcal {G},v}({\Box \Diamond \hat{v}}\wedge {\Diamond \Box \lnot \hat{v}^{\prime }})= \mathit {Prob}^{\pi _{1}, \pi ^*_{2}}_{\mathcal {G},v}({\Diamond B})\) .
(A bottom strongly connected component (BSCC) is a strongly
connected component \(B\subseteq V\)  that cannot reach any vertex
outside \(B\) , that is \(\delta ^{\pi _{1},\pi ^*_{2}}(v,B)=1\) 
for all \(v\in B\) .)
Take \(v^*\in B\)  with minimal distance in
\(\mathcal {G}^{\pi _{1}}_{\min }\)  to a terminal state in \(T\) , that is
\({\Vert {v^*}\Vert }\le {\Vert {v}\Vert }\)  for all \(v\in B\) . Since terminal
vertices are absorbing, we have that \(\hat{v}\notin T\) , and hence
\(T\cap B=\emptyset \) . Therefore \({\Vert {v^*}\Vert }>0\) .
If \(v^*\in V_1 \cup V_\mathsf {P}\) , by definition of
\({\Vert {v^*}\Vert }\) , \(\delta ^{\pi _{1}}_{\min }(v^*,v^{\prime })>0\) 
for some \(v^{\prime }\)  such that \({\Vert {v^{\prime }}\Vert }+1={\Vert {v^*}\Vert }\) . Then
\(v^{\prime }\notin B\) , contradicting the fact that
\(\delta ^{\pi _{1}}_{\min }(v^*,B)=\delta ^{\pi _{1},\pi ^*_{2}}(v^*,B)=1\) .
Hence, \(v^*\notin V_1 \cup V_\mathsf {P}\)  \((\dagger )\) .
If \(v^*\in V_2\) , by definition,
\(\pi ^*_{2}(v^*)(v^{\prime })=1\)  if and only if
\(\delta ^{\pi _{1}}_{\min }(v^*,v^{\prime })=1\)  and
\({\Vert {v^*}\Vert }={\Vert {v^{\prime }}\Vert }+1\) . Again \(v^{\prime }\notin B\) ,
which contradicts the fact that
\(\pi ^*_{2}(v^*)(B)=\delta ^{\pi _{1},\pi ^*_{2}}(v^*,B)=1\) .
Therefore \(v^*\notin V_2\)  \((\ddagger )\) .
By \((\dagger )\)  and \((\ddagger )\) , \(v^*\notin V \supseteq B\) 
contradicting our assumption that \(v^*\in B\) . Therefore,
\(\pi ^*_{2}\)  is fair.
\(\Box \)
To prove Theorem REF , we need the following lemma.
Let \(\mathcal {G}\)  a stochastic game that is stopping under fairness.
Then for any \(\pi _{1} \in \Pi _{1}\) ,
\(\pi _{2} \in \Pi ^{\mathcal {F}}_{2}\) , and \(v \in V\)  it holds:
\(\lim _{N \rightarrow \infty } \sum _{\hat{\omega } \in (V \setminus T)^N} \mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\hat{\omega }) = 0\) 
where \(T\)  is the set of terminal nodes of \(\mathcal {G}\) .


First notice that the complement of \((V \setminus T)^N\)  is
\(\Diamond ^{\le N} T = \cup ^N_{i=0} \Diamond ^i T\) .
Moreover, \(\Diamond ^{\le N} T \subseteq \Diamond ^{\le N+1} T\) , for all \(N\ge 0\) ,
and \(\lim _{N \rightarrow \infty } \Diamond ^{\le N} T = \Diamond T\) .
Then,
\(\lim _{N \rightarrow \infty } \sum _{\hat{\omega } \in (V \setminus T)^N} \mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\hat{\omega }) \ & = \lim _{N \rightarrow \infty } \mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}((V \setminus T)^N) \\& = \lim _{N \rightarrow \infty } 1 - \mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\Diamond ^{\le N} T ) \\& = 1 - \lim _{N \rightarrow \infty } \mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\Diamond ^{\le N} T ) \\& = 1 - \mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\Diamond T ) \\& = 0\) 

The last equality is due to stopping under fairness, and all the
previous ones, to standard measure theory results.
\(\Box \)
Consider a stochastic game \(\mathcal {G}\)  that is stopping under fairness, and a vertex \(v\) . First, note that any semi-Markov strategy \(\pi _{1}\)  can be thought of as a sequence of memoryless strategies: \(\pi _{1}^{0},\pi _{1}^{1},\pi _{1}^{2}, \dots \) , defined as follows:
\(\pi _{1}^{n}(\hat{\omega }v)(v^{\prime }) = \pi _{1}(v_0 \dots v_n)(v^{\prime }), \text{ for any $\hat{\omega }$ and $v_0 \dots v_n$ with $v_n = v$}\) 
Now, for any strategies \(\pi _{1} \in \Pi ^{S}_{1}\)  and \(\pi _{2} \in \Pi ^{M\mathcal {F}}_{2}\) , we have that:
\(\mathbb {E}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}] =\sum ^\infty _{n=0} \sum _{\hat{\omega } \in vV^n} \prod ^{n-1}_{i=0} \delta ^{\pi _{1}^i,\pi _{2}}(\hat{\omega }_i, \hat{\omega }_{i+1}) \mathit {r}(\hat{\omega }_n),\) 
where \(\delta ^{\pi _{1}^i,\pi _{2}}\)  is the probability transition function of the Markov chain \(\mathcal {G}^{\pi _{1}^i,\pi _{2}}\) . We assume that \(\prod ^{-1}_{i=0} \delta ^{\pi _{1}^i,\pi _{2}}(\hat{\omega }_i, \hat{\omega }_{i+1}) = 1\) .
Fix a \(\pi _{2} \in \Pi ^{M\mathcal {F}}_{2}\) , and let \(\pi ^*_{1} \in \Pi ^{M}_{1}\)  be an optimal memoryless strategy for Player 1 for strategy \(\pi _{2}\) . We will prove that no semi-Markov strategy improves the value obtained by \(\pi ^*_{1}\) . Let \(\pi _{1}\)  be an arbitrary and fixed semi-Markov strategy for Player 1. First, note that, since \(\pi ^*_{1}\)  is optimal for memoryless strategies, we have:
\(\mathit {r}(v_n) + \sum _{v_{n+1} \in \mathit {post}(v_n)} \delta ^{\pi _{1}^n,\pi _{2}}(v_n, v_{n+1}) \mathbb {E}^{\pi ^*_{1}, \pi _{2}}_{\mathcal {G},v_{n+1}}[\textit {rew}] \le \mathbb {E}^{\pi ^*_{1}, \pi _{2}}_{\mathcal {G},v_n}[\textit {rew}]\) 
for any vertex \(v_n\)  and memoryless strategy \(\pi _{1}^n\)  as defined in (REF ). Now, let \(\hat{\omega }\)  be any sequence such that
\(\hat{\omega }_n = v_n\) , we multiply both sides of (REF ) by \(\prod ^{n-1}_{i=0} \delta ^{\pi _{1}^i,\pi _{2}}(\hat{\omega }_i,\hat{\omega }_{i+1})\) ,
and get:
\(& \prod ^{n-1}_{i=0}\delta ^{\pi _{1}^i, \pi _{2}}_{\mathcal {G},v}(\hat{\omega }_i, \hat{\omega }_{i+1}) \mathit {r}(v_n) \\& \quad + \ \prod ^{n-1}_{i=0}\delta ^{\pi _{1}^i,\pi _{2}}(\hat{\omega }_i, \hat{\omega }_{i+1}) \sum _{v_{n+1} \in \mathit {post}(\hat{\omega }_n)} \delta ^{\pi _{1}^n,\pi _{2}}(\hat{\omega }_n, v_{n+1}) \mathbb {E}^{\pi ^*_{1}, \pi _{2}}_{\mathcal {G},v_{n+1}}[\textit {rew}] \\& \hspace{180.0pt} \le \prod ^{n-1}_{i=0}\delta ^{\pi _{1}^i,\pi _{2}}(\hat{\omega }_i,\hat{\omega }_{i+1}) \mathbb {E}^{\pi ^*_{1}, \pi _{2}}_{\mathcal {G},v_n}[\textit {rew}]\) 

Thus, considering all the sequences \(\hat{\omega }\)  of length \(n+1\)  we obtain:
\(& \sum _{\hat{\omega } \in vV^{n}} \prod ^{n-1}_{i=0}\delta ^{\pi _{1}^i,\pi _{2}}(\hat{\omega }_i, \hat{\omega }_{i+1}) \mathit {r}(\omega _n) \\& \quad + \ \sum _{\hat{\omega } \in vV^{n+1}} \prod ^{n}_{i=0}\delta ^{\pi _{1}^i,\pi _{2}}(\hat{\omega }_i,\hat{\omega }_{i+1}) \mathbb {E}^{\pi ^*_{1}, \pi _{2}}_{\mathcal {G},\hat{\omega }_{n+1}}[\textit {rew}]\\& \hspace{130.0pt} \le \sum _{\hat{\omega } \in vV^{n}} \prod ^{n-1}_{i=0}\delta ^{\pi _{1}^i,\pi _{2}}(\hat{\omega }_i, \hat{\omega }_{i+1}) \mathbb {E}^{\pi ^*_{1}, \pi _{2}}_{\mathcal {G},\hat{\omega }_n}[\textit {rew}]\) 

Summing up from \(n=0\)  to \(N\) :
\(& \sum ^{N}_{n=0}\sum _{\hat{\omega } \in vV^{n}} \prod ^{n-1}_{i=0}\delta ^{\pi _{1}^i,\pi _{2}}(\hat{\omega }_i,\hat{\omega }_{i+1}) \mathit {r}(\hat{\omega }_n) \\& \quad + \ \sum ^{N}_{n=0} \sum _{\hat{\omega } \in vV^{n+1}} \prod ^{n}_{i=0}\delta ^{\pi _{1}^i,\pi _{2}}(\hat{\omega }_i,\hat{\omega }_{i+1}) \mathbb {E}^{\pi ^*_{1}, \pi _{2}}_{\mathcal {G},\hat{\omega }_{n+1}}[\textit {rew}] \\& \hspace{150.0pt} \le \sum ^{N}_{n=0}\sum _{\hat{\omega } \in vV^{n}} \prod ^{n-1}_{i=0}\delta ^{\pi _{1}^i,\pi _{2}}(\hat{\omega }_i, \hat{\omega }_{i+1}) \mathbb {E}^{\pi ^*_{1}, \pi _{2}}_{\mathcal {G},\hat{\omega }_n}[\textit {rew}],\) 

This is the same as:
\(& \sum ^{N}_{n=0}\sum _{\hat{\omega } \in vV^{n}} \prod ^{n-1}_{i=0}\delta ^{\pi _{1}^i,\pi _{2}}(\hat{\omega }_i,\hat{\omega }_{i+1}) \mathit {r}(\hat{\omega }_n) \\& \quad + \ \sum ^{N+1}_{n=1} \sum _{\hat{\omega } \in vV^{n}} \prod ^{n-1}_{i=0}\delta ^{\pi _{1}^i,\pi _{2}}_{\mathcal {G},v}(\hat{\omega }_i,\hat{\omega }_{i+1}) \mathbb {E}^{\pi ^*_{1}, \pi _{2}}_{\mathcal {G},\hat{\omega }_{n}}[\textit {rew}] \\& \hspace{130.0pt} \le \sum ^{N}_{n=0}\sum _{\hat{\omega } \in vV^{n}} \prod ^{n-1}_{i=0}\delta ^{\pi _{1}^i,\pi _{2}}(\hat{\omega }_i, \hat{\omega }_{i+1}) \mathbb {E}^{\pi ^*_{1}, \pi _{2}}_{\mathcal {G},\hat{\omega }_n}[\textit {rew}]\) 

Thus, subtracting \(\sum ^{N+1}_{n=1} \sum _{\hat{\omega } \in vV^{n}} \prod ^{n-1}_{i=0}\delta ^{\pi _{1}^i,\pi _{2}}(\hat{\omega }_i,\hat{\omega }_{i+1}) \mathbb {E}^{\pi ^*_{1}, \pi _{2}}_{\mathcal {G},\hat{\omega }_{n}}[\textit {rew}]\)  from both sides we get:
\(& \sum ^{N}_{n=0}\sum _{\hat{\omega } \in vV^{n}} \prod ^{n-1}_{i=0}\delta ^{\pi _{1}^i,\pi _{2}}(\hat{\omega }_i, \hat{\omega }_{i+1}) \mathit {r}(v_n)\\& \hspace{70.0pt} \le \mathbb {E}^{\pi ^*_{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}] \ - \sum _{\hat{\omega } \in vV^{N+1}}\prod ^{N}_{n=1}\delta ^{\pi _{1}^n,\pi _{2}}(\hat{\omega }_i,\hat{\omega }_{i+1}) \mathbb {E}^{\pi ^*_{1}, \pi _{2}}_{\mathcal {G}, \hat{\omega }_{N+1}}[\textit {rew}]\) 

Applying limits on both sides, we obtain
\(& \lim _{N \rightarrow \infty } \sum ^{N}_{n=0}\sum _{\hat{\omega } \in vV^{n}} \prod ^{n-1}_{i=0}\delta ^{\pi _{1}^i,\pi _{2}}(\hat{\omega }_i, \hat{\omega }_{i+1}) \mathit {r}(v_n) \\& \hspace{50.0pt} \le \mathbb {E}^{\pi ^*_{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}] \ - \lim _{N \rightarrow \infty } \sum _{\hat{\omega } \in vV^{N+1}}\prod ^{N}_{n=1}\delta ^{\pi _{1}^n,\pi _{2}}(\hat{\omega }_i,\hat{\omega }_{i+1}) \mathbb {E}^{\pi ^*_{1}, \pi _{2}}_{\mathcal {G}, \hat{\omega }_{N+1}}[\textit {rew}] \) 
Observe that
\(\lim _{N \rightarrow \infty } \sum _{\hat{\omega } \in vV^{N+1}}\prod ^{N}_{n=1}\delta ^{\pi _{1}^n,\pi _{2}}(\hat{\omega }_i,\hat{\omega }_{i+1}) \mathbb {E}^{\pi ^*_{1}, \pi _{2}}_{\mathcal {G}, \hat{\omega }_{N+1}}[\textit {rew}] \hspace{-160.0pt} & \\= \ & \lim _{N \rightarrow \infty } \sum _{\hat{\omega } \in v(V\setminus T)^{N+1}}\prod ^{N}_{n=1}\delta ^{\pi _{1}^n,\pi _{2}}(\hat{\omega }_i,\hat{\omega }_{i+1}) \mathbb {E}^{\pi ^*_{1}, \pi _{2}}_{\mathcal {G}, \hat{\omega }_{N+1}}[\textit {rew}] \\& \phantom{\lim _{N \rightarrow \infty }} + \ \sum _{\hat{\omega } \in v\bigcup _{i=0}^N(V\setminus T)^iT^{N+1-i}}\prod ^{N}_{n=1}\delta ^{\pi _{1}^n,\pi _{2}}(\hat{\omega }_i,\hat{\omega }_{i+1}) \mathbb {E}^{\pi ^*_{1}, \pi _{2}}_{\mathcal {G}, \hat{\omega }_{N+1}}[\textit {rew}] \\= \ & \lim _{N \rightarrow \infty } \sum _{\hat{\omega } \in v(V\setminus T)^{N+1}}\prod ^{N}_{n=1}\delta ^{\pi _{1}^n,\pi _{2}}(\hat{\omega }_i,\hat{\omega }_{i+1}) \mathbb {E}^{\pi ^*_{1}, \pi _{2}}_{\mathcal {G}, \hat{\omega }_{N+1}}[\textit {rew}] \\\le \ & \lim _{N \rightarrow \infty } \sum _{\hat{\omega } \in v(V\setminus T)^{N+1}}\prod ^{N}_{n=1}\delta ^{\pi _{1}^n,\pi _{2}}(\hat{\omega }_i,\hat{\omega }_{i+1}) \ M \\= \ & M \ \lim _{N \rightarrow \infty } \sum _{\hat{\omega } \in v(V\setminus T)^{N+1}} \mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\hat{\omega }) \\= \ & 0 \) 

(REF ) folows by noticing that,
since terminal states in set \(T\)  are absorving,
\(V^{N+1}=(V\setminus T)^{N+1}\cup \bigcup _{i=0}^N(V\setminus T)^iT^{N+1-i}\) .
Since
\(\mathbb {E}^{\pi ^*_{1}, \pi _{2}}_{\mathcal {G}, \hat{\omega }_{N+1}}[\textit {rew}]=0\) 
for all \(\hat{\omega }_{N+1}\in T\) , ()
folows.
By taking
\(M = \max _{v\in V} \mathbb {E}^{\pi ^*_{1}, \pi _{2}}_{\mathcal {G}, v}[\textit {rew}]\) ,
which we know it exists because of
Theorem REF , we can conclude
().
() follows by definition of
\(\mathit {Prob}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}(\hat{\omega })\)  and we
conclude () using
Lemma .
Considering this last observation, from
(REF ), we obtain
\(\lim _{N \rightarrow \infty } \sum ^{N}_{n=0}\sum _{\hat{\omega } \in vV^{n}} \prod ^{n-1}_{i=0}\delta ^{\pi _{1}^i,\pi _{2}}(\hat{\omega }_i, \hat{\omega }_{i+1}) \mathit {r}(v_n) \ \le \ \mathbb {E}^{\pi ^*_{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}]\) 
which is equivalent to:
\(\mathbb {E}^{\pi _{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}] \le \mathbb {E}^{\pi ^*_{1}, \pi _{2}}_{\mathcal {G},v}[\textit {rew}].\) 
Hence, the arbitrary semi-Markov strategy \(\pi _{1}\)  does not improve on \(\pi ^*_{1}\) .
\(\Box \)
