CNRS & LMF, ENS Paris-Saclay, Gif-sur-Yvette,
Francehttps://orcid.org/0000-0003-3714-6145 Tata Institute of Fundamental
Research, Mumbai, Indiahttps://orcid.org/0009-0000-8012-780X Tata Institute of
Fundamental Research, Mumbai, Indiahttps://orcid.org/0000-0002-9814-6651
[100]Mathematics of computing Probability and statistics Stochastic processes

###### Acknowledgements.

We thank Mickael Randour for pointing out reference [7], making us aware of
the bugs in the algorithms of [9] and the correct version of these algorithms
as presented here.

# Stochastic Window Mean-payoff Games

Laurent Doyen  Pranshu Gaba  Shibashis Guha

###### Abstract

Stochastic two-player games model systems with an environment that is both
adversarial and stochastic. The environment is modeled by a player
($\textrm{Player}\leavevmode\nobreak\ {2}$) who tries to prevent the system
($\textrm{Player}\leavevmode\nobreak\ {1}$) from achieving its objective. We
consider finitary versions of the traditional mean-payoff objective, replacing
the long-run average of the payoffs by payoff average computed over a finite
sliding window. Two variants have been considered: in one variant, the maximum
window length is fixed and given, while in the other, it is not fixed but is
required to be bounded. For both variants, we present complexity bounds and
algorithmic solutions for computing strategies for
$\textrm{Player}\leavevmode\nobreak\ {1}$ to ensure that the objective is
satisfied with positive probability, with probability $1$, or with probability
at least $p$, regardless of the strategy of
$\textrm{Player}\leavevmode\nobreak\ {2}$. The solution crucially relies on a
reduction to the special case of non-stochastic two-player games. We give a
general characterization of prefix-independent objectives for which this
reduction holds. The memory requirement for both players in stochastic games
is also the same as in non-stochastic games by our reduction. Moreover, for
non-stochastic games, we improve upon the upper bound for the memory
requirement of $\textrm{Player}\leavevmode\nobreak\ {1}$ and upon the lower
bound for the memory requirement of $\textrm{Player}\leavevmode\nobreak\ {2}$.

###### keywords:

stochastic games, finitary objectives, mean-payoff, reactive synthesis

###### category:

##  1 Introduction

We consider two-player turn-based stochastic games played on graphs. Games are
a central model in computer science, in particular for the verification and
synthesis of reactive systems [19, 12, 18]. A stochastic game is played by two
players on a graph with stochastic transitions, where the players represent
the system and the adversarial environment, while the objective represents the
functional requirement that the synthesized system aims to satisfy with a
probability $p$ as large as possible. The vertices of the graph are
partitioned into system, environment, and probabilistic vertices. A stochastic
game is played in infinitely many rounds, starting by initially placing a
token on some vertex. In every round, if the token is on a system or an
environment vertex, then the owner of the vertex chooses a successor vertex;
if the token is on a probabilistic vertex, then the successor vertex is chosen
according to a given probability distribution. The token moves to the
successor vertex, from where the next round starts. The outcome is an infinite
sequence of vertices, which is winning for the system if it satisfies the
given objective. The associated _quantitative satisfaction problem_ is to
decide, given a threshold $p$, whether the system can win with probability at
least $p$. The _almost-sure problem_ is the special case where $p=1$, and the
_positive problem_ is to decide whether the system can win with positive
probability. The almost-sure and the positive problems are referred to as the
_qualitative satisfaction problems_. When the answer to these decision
problems is ${\sf Yes}$, it is useful to construct a winning strategy for the
system that can be used as a model for an implementation that ensures the
objective be satisfied with the given probability.

Traditional objectives in stochastic games are $\omega$-regular such as
reachability, safety, and parity objectives [12], or quantitative such as
mean-payoff objectives [17, 29]. For example, a parity objective may specify
that every request of the environment is eventually granted by the system, and
a mean-payoff objective may specify the long-run average power consumption of
the system. A well-known drawback of parity and mean-payoff objectives is that
only the long-run behaviour of the system may be specified [1, 10, 22],
allowing weird transient behaviour: for example, a system may grant all its
requests but with an unbounded response time; or a system with long-run
average power consumption below some threshold may exhibit arbitrarily long
(but finite) sequences with average power consumption above the threshold.
This limitation has led to considering finitary versions of those objectives
[10, 24, 9], where the sequences of undesired transient behaviours must be of
fixed or bounded length. Window mean-payoff objectives [9] are quantitative
finitary objectives that strengthen the traditional mean-payoff objective: the
satisfaction of a window mean-payoff objective implies the satisfaction of the
standard mean-payoff objective. Given a length $\ell\geq 1$, the fixed window
mean-payoff objective ($\mathsf{FWMP}(\ell)$) is satisfied if there exists a
time $T$, such that for every time $t\geq T$ in the execution, there exists a
window $W$ of length at most $\ell$ starting from $t$ and the mean payoff over
$W$ is non-negative. In the bounded window mean-payoff objective
($\mathsf{BWMP}$), it is sufficient that there exists some length $\ell$ for
which the $\mathsf{FWMP}(\ell)$ objective is satisfied.

#### Contributions.

We present algorithmic solutions for stochastic games with window mean-payoff
objectives, and show that the positive and almost-sure problems are solvable
in polynomial time for $\mathsf{FWMP}(\ell)$ (Theorem 6.5), and in
$\mathsf{NP}\cap\mathsf{coNP}$ for $\mathsf{BWMP}$ (Theorem 6.10). The
complexity result for the almost-sure problem entails that the quantitative
satisfaction problem is in $\mathsf{NP}\cap\mathsf{coNP}$ (for both the fixed
and bounded version), using standard techniques for solving stochastic games
with prefix-independent objectives [14]. Note that the
$\mathsf{NP}\cap\mathsf{coNP}$ bound for the quantitative satisfaction problem
matches the special case of reachability objectives in simple stochastic games
[15], and thus would require a major breakthrough to be improved.

As a consequence, using the $\mathsf{FWMP}(\ell)$ objective instead of the
standard mean-payoff objective provides a stronger guarantee on the system,
and even with a polynomial complexity for the positive and the almost-sure
problems (which is not known for mean-payoff objectives), and at no additional
computational cost for the quantitative satisfaction problem. The solution
relies on a reduction to non-stochastic two-player games (stochastic games
without probabilistic vertices). The key result is to show that in order to
win positively from some vertex of the game graph, it is necessary to win from
some vertex of the non-stochastic game obtained by transforming all
probabilistic vertices into adversarial vertices. While this condition, that
we call the sure-almost-sure (SAS) property (Definition 5.1), was used to
solve finitary Streett objectives [14], we follow a similar approach and
generalize it to arbitrary prefix-independent objectives (Theorem 5.2). The
bounds on the memory requirement of optimal strategies of
$\textrm{Player}\leavevmode\nobreak\ {1}$ can also be derived from the key
result, and are the same as optimal bounds for non-stochastic games. For
$\mathsf{FWMP}(\ell)$ and $\mathsf{BWMP}$ objectives in particular, we show
that the memory requirement of $\textrm{Player}\leavevmode\nobreak\ {2}$ is
also no more than the optimal memory required by winning strategies in non-
stochastic games.

As solving a stochastic game with a prefix-independent objective $\varphi$
reduces to solving non-stochastic games with objective $\varphi$ and showing
that $\varphi$ satisfies the $\mathsf{SAS}$ property, we show that the
$\mathsf{FWMP}(\ell)$ and $\mathsf{BWMP}$ objectives satisfy the
$\mathsf{SAS}$ property (Lemma 6.1, Lemma 6.8) and rely on the solution of
non-stochastic games with these objectives [9] to complete the reduction.

We improve the memory bounds for optimal strategies of both players in non-
stochastic games. It is stated in [9] that $\lvert V\rvert\cdot\ell$ memory
suffices for both players, where $|V|$ and $\ell$ are the number of vertices
and the window length respectively. In [7, Theorem 2], the bound is loosened
to $\mathcal{O}(w_{\max}\cdot\ell^{2})$ and
$\mathcal{O}(w_{\max}\cdot\ell^{2}\cdot\lvert V\rvert)$ for
$\textrm{Player}\leavevmode\nobreak\ {1}$ and
$\textrm{Player}\leavevmode\nobreak\ {2}$ respectively, where $w_{\max}$ is
the maximum absolute payoff in the graph, as the original tighter bounds [9]
were stated without proof. Since the payoffs are given in binary, this is
exponential in the size of the input. In contrast, we tighten the bounds
stated in [9]. We show that for $\textrm{Player}\leavevmode\nobreak\ {1}$,
memory $\ell$ suffices (Theorem 4.5), and improve the bound on memory of
$\textrm{Player}\leavevmode\nobreak\ {2}$ strategies as follows. We compute
the set $W$ of vertices from which $\textrm{Player}\leavevmode\nobreak\ {2}$
can ensure that the mean payoff remains negative for $\ell$ steps, as well as
the vertices from which $\textrm{Player}\leavevmode\nobreak\ {2}$ can ensure
that the game reaches $W$. These vertices are identified recursively on
successive subgames of the original input game. If $k$ be the number of
recursive calls, then we show that $k\cdot\ell$ memory suffices for
$\textrm{Player}\leavevmode\nobreak\ {2}$ to play optimally (Theorem 4.9).
Note that $k\leq\lvert V\rvert$. We also provide a lower bound on the memory
size for $\textrm{Player}\leavevmode\nobreak\ {2}$. Given $\ell\geq 2$, for
every $k\geq 1$, we construct a graph with a set $V$ of vertices such that
$\textrm{Player}\leavevmode\nobreak\ {2}$ requires at least
$k+1=\frac{1}{2}(|V|-\ell+3)$ memory to play optimally (Theorem 4.14). This is
an improvement over the result in [9] which showed that memoryless strategies
do not suffice for $\textrm{Player}\leavevmode\nobreak\ {2}$. Our result is
quite counterintuitive since given an open window (a window in which every
prefix has a total weight less than $0$) that needs to be kept open for
another $j\leq\ell$ steps from a vertex $v$, one would conjecture that it is
sufficient for a $\textrm{Player}\leavevmode\nobreak\ {2}$ winning strategy to
choose an edge from $v$ that leads to the minimum payoff over paths of length
$j$. Thus for every $j$, $\textrm{Player}\leavevmode\nobreak\ {2}$ should
choose a fixed edge and hence memory of size $\ell$ should suffice. However,
we show that this is not the case.

To the best of our knowledge, this work leads to the first study of stochastic
games with finitary quantitative objectives.

#### Related work.

Window mean-payoff objectives were first introduced in [9] for non-stochastic
games, where solving $\mathsf{FWMP}(\ell)$ was shown to be in $\mathsf{PTIME}$
and $\mathsf{BWMP}$ in $\mathsf{NP}\cap\mathsf{coNP}$. These have also been
studied for Markov decision processes (MDPs) in [5, 4]. In [5], a threshold
probability problem has been studied, while in [4], the authors studied the
problem of maximising the expected value of the window mean-payoff. Positive,
almost-sure, and quantitative satisfaction of $\mathsf{BWMP}$ in MDPs are in
$\mathsf{NP}\cap\mathsf{coNP}$ [5], the same as in non-stochastic games.

Parity objectives can be viewed as a special case of mean-payoff [23]. A
bounded-window parity objective has been studied in [10, 21, 13] where a play
satisfies the objective if from some point on, there exists a bound $\ell$
such that from every state with an odd priority a smaller even priority occurs
within at most $\ell$ steps. Non-stochastic games with bounded window parity
objectives can be solved in $\mathsf{PTIME}$ [21, 13]. Stochastic games with
bounded window parity objectives have been studied in [14] where the positive
and almost-sure problems are in $\mathsf{PTIME}$ while the quantitative
satisfaction problem is in $\mathsf{NP}\cap\mathsf{coNP}$. A fixed version of
the window parity objective has been studied for two-player games and shown to
be $\mathsf{PSPACE}$-complete [28]. Another window parity objective has been
studied in [6] for which both the fixed and the bounded variants have been
shown to be in $\mathsf{PTIME}$ for non-stochastic games. The threshold
problem for this objective has also been studied in the context of MDPs, and
both fixed and bounded variants are in $\mathsf{PTIME}$ [5]. Finally,
synthesis for _bounded_ eventuality properties in LTL is
2-$\mathsf{EXPTIME}$-complete [24].

#### Outline

In Section 2, we provide the necessary technical preliminaries. In Section 3,
we define window mean-payoff objectives and state relevant decision problems
for stochastic games. In Section 4, we give improved bounds on the memory
requirements of the players’ strategies for non-stochastic games with window
mean-payoff objectives. In Section 5, we define a property of prefix-
independent objectives that allows one to solve stochastic games by reducing
them to non-stochastic games. Finally, as an application, in Section 6, we
provide solutions to problems in stochastic games with window mean-payoff
objectives.

##  2 Preliminaries

#### Probability distributions.

A _probability distribution_ over a finite nonempty set $A$ is a function
$\mathsf{Pr}\colon A\to[0,1]$ such that $\sum_{a\in A}\mathsf{Pr}(a)=1$. We
denote by $\mathcal{D}(A)$ the set of all probability distributions over $A$.
For the algorithmic and complexity results, we assume that probabilities are
given as rational numbers.

#### Stochastic games.

We consider two-player turn-based zero-sum stochastic games (or simply,
stochastic games in the sequel). The two players are referred to as
$\textrm{Player}\leavevmode\nobreak\ {1}$ and
$\textrm{Player}\leavevmode\nobreak\ {2}$. A _stochastic game_ is a weighted
directed graph $\mathcal{G}=((V,E),(V_{1},V_{2},V_{\Diamond}),\mathbb{P},w)$,
where:

  * •

$(V,E)$ is a directed graph with a set $V$ of vertices and a set $E\subseteq
V\times V$ of directed edges such that for all vertices $v\in V$, the set
$E(v)=\\{v^{\prime}\in V\mid(v,v^{\prime})\in E\\}$ of out-neighbours of $v$
is nonempty, i.e., $E(v)\neq\varnothing$ (no deadlocks). A stochastic game is
said to be finite if $V$ is a finite set, and infinite otherwise. Unless
mentioned otherwise, stochastic games considered in this paper are finite;

  * •

$(V_{1},V_{2},V_{\Diamond})$ is a partition of $V$. The vertices in $V_{1}$
belong to $\textrm{Player}\leavevmode\nobreak\ {1}$, the vertices in $V_{2}$
belong to $\textrm{Player}\leavevmode\nobreak\ {2}$, and the vertices in
$V_{\Diamond}$ are called probabilistic vertices;

  * •

$\mathbb{P}\colon V_{\Diamond}\to\mathcal{D}(V)$ is a _probability function_
that describes the behaviour of probabilistic vertices in the game. It maps
the probabilistic vertices $v\in V_{\Diamond}$ to a probability distribution
$\mathbb{P}(v)$ over the set $E(v)$ of out-neighbours of $v$ such that
$\mathbb{P}(v)(v^{\prime})>0$ for all $v^{\prime}\in E(v)$ (i.e., all
neighbours have nonzero probability);

  * •

$w\colon E\to\mathbb{Q}$ is a _payoff function_ assigning a rational payoff to
every edge in the game.

Stochastic games are played in rounds. The game starts by initially placing a
token on some vertex. At the beginning of a round, if the token is on a vertex
$v$, and $v\in V_{i}$ for $i\in\\{1,2\\}$, then
$\textrm{Player}\leavevmode\nobreak\ {i}$ chooses an out-neighbour
$v^{\prime}\in E(v)$; otherwise $v\in V_{\Diamond}$, and an out-neighbour
$v^{\prime}\in E(v)$ is chosen with probability $\mathbb{P}(v)(v^{\prime})$.
$\textrm{Player}\leavevmode\nobreak\ {1}$ receives from
$\textrm{Player}\leavevmode\nobreak\ {2}$ the amount $w(v,v^{\prime})$ given
by the payoff function, and the token moves to $v^{\prime}$ for the next
round. This continues ad infinitum resulting in an infinite sequence
$\pi=v_{0}v_{1}v_{2}\dotsm\in V^{\omega}$ such that $(v_{i},v_{i+1})\in E$ for
all $i\geq 0$.

A stochastic game with $V_{\Diamond}=\varnothing$ is called a non-stochastic
two-player game, a stochastic game with $V_{2}=\varnothing$ is called a Markov
decision process (MDP), a stochastic game with
$V_{2}=V_{\Diamond}=\varnothing$ is called a one-player game, and a stochastic
game with $V_{1}=V_{2}=\varnothing$ is called a Markov chain. We use pronouns
“she/her” for $\textrm{Player}\leavevmode\nobreak\ {1}$ and “he/him” for
$\textrm{Player}\leavevmode\nobreak\ {2}$. Figure 1 shows an example of a
stochastic game. In figures, $\textrm{Player}\leavevmode\nobreak\ {1}$
vertices are shown as circles, $\textrm{Player}\leavevmode\nobreak\ {2}$
vertices as boxes, and probabilistic vertices as diamonds.

$v_{1}$$v_{2}$$v_{3}$$v_{4}$$v_{5}$$v_{6}$$v_{7}$$v_{8}$$v_{9}$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}.3}$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}.7}$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}.1}$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}.9}$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}.2}$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}.8}$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0}$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}-1}$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}-1}$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0}$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0}$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0}$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}-1}$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0}$
Figure 1: A stochastic game. $\textrm{Player}\leavevmode\nobreak\ {1}$
vertices are denoted by circles, $\textrm{Player}\leavevmode\nobreak\ {2}$
vertices are denoted by boxes, and probabilistic vertices are denoted by
diamonds. The payoff for each edge is shown in red and probability
distribution out of probabilistic vertices is shown in blue.

#### Plays and prefixes.

A _play_ in $\mathcal{G}$ is an infinite sequence $\pi=v_{0}v_{1}\cdots\in
V^{\omega}$ of vertices such that $(v_{i},v_{i+1})\in E$ for all $i\geq 0$. We
denote by $\textrm{occ}(\pi)$ the set of vertices in $V$ that occur at least
once in $\pi$, and by $\inf(\pi)$ the set of vertices in $V$ that occur
infinitely often in $\pi$. For $i<j$, we denote by $\pi(i,j)$ the _infix_
$v_{i}v_{i+1}\dotsm v_{j}$ of $\pi$. Its length is $\lvert\pi(i,j)\rvert=j-i$,
the number of edges. We denote by $\pi(0,j)$ the finite _prefix_
$v_{0}v_{1}\dotsm v_{j}$ of $\pi$, and by $\pi(i,\infty)$ the infinite
_suffix_ $v_{i}v_{i+1}\ldots$ of $\pi$. We denote by
$\mathsf{Plays}_{\mathcal{G}}$ and $\mathsf{Prefs}_{\mathcal{G}}$ the set of
all plays and the set of all prefixes in $\mathcal{G}$ respectively; the
symbol $\mathcal{G}$ is omitted when it can easily be derived from the
context. We denote by $\mathsf{First}(\rho)$ and $\mathsf{Last}(\rho)$ the
first vertex and the last vertex of a prefix
$\rho\in\mathsf{Prefs}_{\mathcal{G}}$ respectively. We denote by
$\mathsf{Prefs}^{i}_{\mathcal{G}}$ ($i\in\\{1,2\\}$) the set of all prefixes
$\rho$ such that $\mathsf{Last}(\rho)\in V_{i}$. The _cone_ at $\rho$ is the
set $\mathsf{Cone}(\rho)=\\{\pi\in\mathsf{Plays}_{\mathcal{G}}\mid\rho\text{
is a prefix of }\pi\\}$, the set of all plays having $\rho$ as a prefix.

#### Objectives.

An _objective_ $\varphi$ is a Borel-measurable subset of
$\mathsf{Plays}_{\mathcal{G}}$ [2]. A play
$\pi\in\mathsf{Plays}_{\mathcal{G}}$ _satisfies_ an objective $\varphi$ if
$\pi\in\varphi$. In a (zero-sum) stochastic game $\mathcal{G}$ with objective
$\varphi$, the objective of $\textrm{Player}\leavevmode\nobreak\ {1}$ is
$\varphi$, and the objective of $\textrm{Player}\leavevmode\nobreak\ {2}$ is
the complement set
$\overline{\varphi}=\mathsf{Plays}_{\mathcal{G}}\setminus\varphi$. Given
$T\subseteq V$, define the following objectives:

  * •

the _reachability_ objective
$\mathsf{Reach}_{\mathcal{G}}(T)=\\{\pi\in\mathsf{Plays}_{\mathcal{G}}\mid
T\cap\textrm{occ}(\pi)\neq\varnothing\\}$, the set of all plays that visit a
vertex in $T$,

  * •

the dual _safety_ objective
$\mathsf{Safe}_{\mathcal{G}}(T)=\\{\pi\in\mathsf{Plays}_{\mathcal{G}}\mid\textrm{occ}(\pi)\subseteq
T\\}$, the set of all plays that never visit a vertex outside $T$,

  * •

the _Büchi_ objective
$\textsf{B\"{u}chi}_{\mathcal{G}}(T)=\\{\pi\in\mathsf{Plays}_{\mathcal{G}}\mid
T\cap\inf(\pi)\neq\varnothing\\}$, the set of all plays that visit a vertex in
$T$ infinitely often, and

  * •

the dual _coBüchi_ objective
$\textsf{coB\"{u}chi}_{\mathcal{G}}(T)=\\{\pi\in\mathsf{Plays}_{\mathcal{G}}\mid\inf(\pi)\subseteq
T\\}$, the set of all plays that eventually only visit vertices in $T$.

An objective $\varphi$ is _closed under suffixes_ if for all plays $\pi$
satisfying $\varphi$, all suffixes of $\pi$ also satisfy $\varphi$, that is,
$\pi(j,\infty)\in\varphi$ for all $j\geq 0$. An objective $\varphi$ is _closed
under prefixes_ if for all plays $\pi$ satisfying $\varphi$, for all prefixes
$\rho$ such that $\rho\cdot\pi\in\mathsf{Plays}_{\mathcal{G}}$, we have that
$\rho\cdot\pi\in\varphi$. An objective $\varphi$ is _prefix-independent_ if it
is closed under both prefixes and suffixes. An objective $\varphi$ is closed
under suffixes if and only if the complement objective $\overline{\varphi}$ is
closed under prefixes. Thus, an objective $\varphi$ is prefix-independent if
and only if its complement $\overline{\varphi}$ is prefix-independent. The
reachability objective is closed under prefixes, the safety objective is
closed under suffixes, and the Büchi and coBüchi objectives are closed under
both prefixes and suffixes.

#### Strategies.

A (deterministic or pure) _strategy_ 111In general, strategies may be
randomised, but deterministic strategies are sufficient for the objectives
considered in this work. for Player $i\in\\{1,2\\}$ in a game $\mathcal{G}$ is
a function $\sigma_{i}:\mathsf{Prefs}^{i}_{\mathcal{G}}\to V$ that maps
prefixes ending in a vertex $v\in V_{i}$ to a successor of $v$. The set of all
strategies of Player $i\in\\{1,2\\}$ in the game $\mathcal{G}$ is denoted by
$\Lambda_{i}(\mathcal{G})$, or $\Lambda_{i}$ when $\mathcal{G}$ is clear from
the context. Strategies can be realised as the output of a (possibly infinite-
state) Mealy machine. A _Mealy machine_ is a transition system with
transitions labelled by a pair of symbols: one from the input alphabet and one
from an output alphabet. For each state $q$ of the Mealy machine and every
letter $a$ of the input alphabet, there is exactly one transition defined from
state $q$ on reading the letter $a$. Formally, a Mealy machine $M$ is a tuple
$(Q,q_{0},\Sigma_{i},\Sigma_{o},\Delta,\delta)$ where $Q$ is the set of states
of $M$ (the memory of the induced strategy), $q_{0}\in Q$ is the initial
state, $\Sigma_{i}$ is the input alphabet, $\Sigma_{o}$ is the output
alphabet, $\Delta\colon Q\times\Sigma_{i}\to Q$ is a transition function that
reads the current state of $M$ and an input letter and returns the next state
of $M$, and $\delta\colon Q\times\Sigma_{i}\to\Sigma_{o}$ is an output
function that reads the current state of $M$ and an input letter and returns
an output letter.

The transition function $\Delta$ can be extended to a function
$\hat{\Delta}\colon Q\times\Sigma_{i}^{+}\to Q$ that reads words and can be
defined inductively by $\hat{\Delta}(q,a)=\Delta(q,a)$ and
$\hat{\Delta}(q,x\cdot a)=\Delta(\hat{\Delta}(q,x),a)$, for $q\in Q$,
$x\in\Sigma_{i}^{+}$, and $a\in\Sigma_{i}$. The output function $\delta$ can
be also be similarly extended to a function $\hat{\delta}\colon
Q\times\Sigma_{i}^{+}\to\Sigma_{o}$ on words and can be defined inductively by
$\hat{\delta}(q,a)=\delta(q,a)$ and $\hat{\delta}(q,x\cdot
a)=\delta(\hat{\Delta}(q,x),a)$, for $q\in Q$, $x\in\Sigma_{i}^{+}$, and
$a\in\Sigma_{i}$.

A player’s strategy can be defined by a Mealy machine whose input and output
alphabets are $V$ and $V\cup\\{\epsilon\\}$ respectively. For $i\in\\{1,2\\}$,
a strategy $\sigma_{i}$ of $\text{Player\leavevmode\nobreak\ }i$ can be
defined by a Mealy machine $(Q,q_{0},V,V\cup\\{\epsilon\\},\Delta,\delta)$ as
follows: Given a prefix $\rho\in\mathsf{Prefs}^{i}_{\mathcal{G}}$ ending in a
$\text{Player\leavevmode\nobreak\ }i$ vertex, the strategy $\sigma_{i}$
defined by a Mealy machine is $\sigma_{i}(\rho)=\hat{\delta}(q_{0},\rho)$.
Intuitively, in each turn, if the token is on a vertex $v$ that belongs to
$\text{Player\leavevmode\nobreak\ }i$ for $i\in\\{1,2\\}$, then $v$ is given
as input to the Mealy machine, and the Mealy machine outputs the successor
vertex of $v$ that $\text{Player\leavevmode\nobreak\ }i$ must choose.
Otherwise, the token is on a vertex $v$ that either belongs to
$\text{Player\leavevmode\nobreak\ }i$’s opponent or is a probabilistic vertex,
in which case, the Mealy machine outputs the symbol $\epsilon$ to denote that
$\text{Player\leavevmode\nobreak\ }i$ cannot decide the successor vertex of
$v$. The _memory size_ of a strategy $\sigma_{i}$ is the smallest number of
states a Mealy machine defining $\sigma_{i}$ can have. A strategy $\sigma_{i}$
is _memoryless_ if $\sigma_{i}(\rho)$ only depends on the last element of the
prefix $\rho$, that is for all prefixes
$\rho,\rho^{\prime}\in\mathsf{Prefs}^{i}_{\mathcal{G}}$ if
$\mathsf{Last}(\rho)=\mathsf{Last}(\rho^{\prime})$, then
$\sigma_{i}(\rho)=\sigma_{i}(\rho^{\prime})$. Memoryless strategies can be
defined by Mealy machines with only one state.

A strategy _profile_ $\overline{\sigma}=(\sigma_{1},\sigma_{2})$ is a pair of
strategies $\sigma_{1}\in\Lambda_{1}(\mathcal{G})$ and
$\sigma_{2}\in\Lambda_{2}(\mathcal{G})$. A play $\pi=v_{0}v_{1}\dotsm$ is
_consistent_ with a strategy $\sigma_{i}\in\Lambda_{i}$ ($i\in\\{1,2\\}$) if
for all $j\geq 0$, we have that if $v_{j}\in V_{i}$, then
$v_{j+1}=\sigma_{i}(\pi(0,j))$. A play $\pi$ is an _outcome_ of a profile
$\overline{\sigma}=(\sigma_{1},\sigma_{2})$ if it is consistent with both
$\sigma_{1}$ and $\sigma_{2}$. We denote by
$\mathsf{Pr}^{\sigma_{1},\sigma_{2}}_{\mathcal{G},v}(\varphi)$ the probability
that an outcome of the profile $(\sigma_{1},\sigma_{2})$ in $\mathcal{G}$ with
initial vertex $v$ satisfies $\varphi$. First, we define this probability
measure over cones inductively as follows. If $\lvert\rho\rvert=0$, then
$\rho$ is just a vertex $v_{0}$, and
$\mathsf{Pr}^{\sigma_{1},\sigma_{2}}_{\mathcal{G},v}(\mathsf{Cone}(\rho))$ is
$1$ if $v=v_{0}$, and $0$ otherwise. For the inductive case
$\lvert\rho\rvert>0$, there exist
$\rho^{\prime}\in\mathsf{Prefs}_{\mathcal{G}}$ and $v^{\prime}\in V$ such that
$\rho=\rho^{\prime}\cdot v^{\prime}$, and we have

$\mathsf{Pr}^{\sigma_{1},\sigma_{2}}_{\mathcal{G},v}(\mathsf{Cone}(\rho^{\prime}\cdot
v^{\prime}))=\begin{cases}\mathsf{Pr}^{\sigma_{1},\sigma_{2}}_{\mathcal{G},v}(\mathsf{Cone}(\rho^{\prime}))\cdot\mathbb{P}(\mathsf{Last}(\rho^{\prime}))(v^{\prime})&\text{if
}\mathsf{Last}(\rho^{\prime})\in V_{\Diamond},\\\
\mathsf{Pr}^{\sigma_{1},\sigma_{2}}_{\mathcal{G},v}(\mathsf{Cone}(\rho^{\prime}))&\text{if
}\mathsf{Last}(\rho^{\prime})\in V_{i}\text{ and
}\sigma_{i}(\rho^{\prime})=v^{\prime},\\\ 0&\text{otherwise.}\\\ \end{cases}$

It is sufficient to define
$\mathsf{Pr}^{\sigma_{1},\sigma_{2}}_{\mathcal{G},v}(\varphi)$ on cones in
$\mathcal{G}$ since a measure defined on cones extends to a unique measure on
$\mathsf{Plays}_{\mathcal{G}}$ by Carathéodory’s extension theorem [3].

#### Non-stochastic two-player games.

A stochastic game without probabilistic vertices (that is, with
$V_{\Diamond}=\varnothing$) is called a _non-stochastic two-player game_ (or
simply, non-stochastic game in the sequel). In a non-stochastic game $G$ with
objective $\varphi$, a strategy $\sigma_{i}$ is _winning_ for
$\text{Player\leavevmode\nobreak\ }i$ ($i\in\\{1,2\\}$) if every play in $G$
consistent with $\sigma_{i}$ satisfies the objective $\varphi$. A vertex $v\in
V$ is _winning_ for $\textrm{Player}\leavevmode\nobreak\ {i}$ in $G$ if
$\textrm{Player}\leavevmode\nobreak\ {i}$ has a winning strategy in $G$ when
the initial vertex is $v$. The set of vertices in $V$ that are winning for
$\textrm{Player}\leavevmode\nobreak\ {i}$ in $G$ is the _winning region_ of
$\textrm{Player}\leavevmode\nobreak\ {i}$ in $G$, denoted $\langle\\!\langle
i\rangle\\!\rangle^{\mathsf{}}_{G}(\varphi)$. If a vertex $v$ belongs to the
winning region of Player $i$ ($i\in\\{1,2\\}$), then Player $i$ is said to
play _optimally_ from $v$ if they follow a winning strategy. By fixing a
strategy $\sigma_{i}$ of $\textrm{Player}\leavevmode\nobreak\ {i}$ in a non-
stochastic game $G$ we obtain a (possibly infinite) one-player game
$G^{\sigma_{i}}$ with vertices $V\times Q$, where $Q$ is the set of states of
a Mealy machine defining $\sigma_{i}$.

#### Subgames.

Given a stochastic game
$\mathcal{G}=((V,E),(V_{1},V_{2},V_{\Diamond}),\mathbb{P},w)$, a subset
$V^{\prime}\subseteq V$ of vertices _induces_ a subgame if $(i)$ every vertex
$v^{\prime}\in V^{\prime}$ has an outgoing edge in $V^{\prime}$, that is
$E(v^{\prime})\cap V^{\prime}\neq\varnothing$, and $(ii)$ every probabilistic
vertex $v^{\prime}\in V_{\Diamond}\cap V^{\prime}$ has all outgoing edges in
$V^{\prime}$, that is $E(v^{\prime})\subseteq V^{\prime}$. The induced
_subgame_ is $((V^{\prime},E^{\prime}),(V_{1}\cap V^{\prime},V_{2}\cap
V^{\prime},V_{\Diamond}\cap V^{\prime}),\mathbb{P}^{\prime},w^{\prime})$,
where $E^{\prime}=E\cap(V^{\prime}\times V^{\prime})$, and
$\mathbb{P}^{\prime}$ and $w^{\prime}$ are restrictions of $\mathbb{P}$ and
$w$ respectively to $(V^{\prime},E^{\prime})$. We denote this subgame by
$\mathcal{G}\upharpoonright V^{\prime}$. Let $\varphi$ be an objective in the
stochastic game $\mathcal{G}$. We define the restriction of $\varphi$ to a
subgame $\mathcal{G}^{\prime}$ of $\mathcal{G}$ to be the set of all plays in
$\mathcal{G}^{\prime}$ satisfying $\varphi$, that is, the set
$\mathsf{Plays}_{\mathcal{G}^{\prime}}\cap\varphi$.

#### Satisfaction probability.

A strategy $\sigma_{1}$ of $\textrm{Player}\leavevmode\nobreak\ {1}$ is
_winning_ with probability $p$ from an initial vertex $v$ in $\mathcal{G}$ for
objective $\varphi$ if
$\mathsf{Pr}^{\sigma_{1},\sigma_{2}}_{\mathcal{G},v}(\varphi)\geq p$ for all
strategies $\sigma_{2}$ of $\textrm{Player}\leavevmode\nobreak\ {2}$. A
strategy $\sigma_{1}$ of $\textrm{Player}\leavevmode\nobreak\ {1}$ is
_positive_ winning (resp., _almost-sure_ winning) from $v$ for
$\textrm{Player}\leavevmode\nobreak\ {1}$ in $\mathcal{G}$ with objective
$\varphi$ if $\mathsf{Pr}^{\sigma_{1},\sigma_{2}}_{\mathcal{G},v}(\varphi)>0$
(resp., $\mathsf{Pr}^{\sigma_{1},\sigma_{2}}_{\mathcal{G},v}(\varphi)=1$) for
all strategies $\sigma_{2}$ of $\textrm{Player}\leavevmode\nobreak\ {2}$. We
refer to positive and almost-sure winning as _qualitative_ satisfaction of
$\varphi$, while for arbitrary $p\in[0,1]$, we call it _quantitative_
satisfaction. We denote by $\langle\\!\langle
1\rangle\\!\rangle^{\mathsf{Pos}}_{\mathcal{G}}(\varphi)$ (resp., by
$\langle\\!\langle 1\rangle\\!\rangle^{\mathsf{AS}}_{\mathcal{G}}(\varphi)$)
the positive (resp., almost-sure) winning region of
$\textrm{Player}\leavevmode\nobreak\ {1}$, i.e., the set of all vertices in
$\mathcal{G}$ from which $\textrm{Player}\leavevmode\nobreak\ {1}$ has a
positive (resp., almost-sure) winning strategy for $\mathcal{G}$ with
objective $\varphi$. If a vertex $v$ belongs to the positive (resp., almost-
sure) winning region of $\textrm{Player}\leavevmode\nobreak\ {1}$, then
$\textrm{Player}\leavevmode\nobreak\ {1}$ is said to play _optimally_ from $v$
if she follows a positive (resp., almost-sure) winning strategy from $v$. We
omit analogous definitions for $\textrm{Player}\leavevmode\nobreak\ {2}$.

#### Positive attractors and traps.

The $\text{Player\leavevmode\nobreak\ }i$  _positive attractor_
($i\in\\{1,2\\}$) to $T\subseteq V$, denoted $\mathsf{PosAttr}_{i}(T)$, is the
set $\langle\\!\langle
i\rangle\\!\rangle^{\mathsf{Pos}}_{\mathcal{G}}(\mathsf{Reach}(T))$ of
vertices in $V$ from which $\text{Player\leavevmode\nobreak\ }i$ can ensure
that the token reaches a vertex in $T$ with positive probability. It can be
computed as the least fixed point of the operator $\lambda x.{\sf
PosPre}_{i}(x)\cup T$ where ${\sf PosPre}_{1}(x)=\\{v\in V_{1}\cup
V_{\Diamond}\mid E(v)\cap x\neq\varnothing\\}\cup\\{v\in V_{2}\mid
E(v)\subseteq x\\}$ is the positive predecessor operator for
$\textrm{Player}\leavevmode\nobreak\ {1}$, and ${\sf PosPre}_{2}$ is defined
analogously for $\textrm{Player}\leavevmode\nobreak\ {2}$. Intuitively ${\sf
PosPre}_{i}(x)$ is the set of vertices from which
$\text{Player\leavevmode\nobreak\ }i$ has a strategy to ensure with positive
probability that the vertex in the next round is in $x$. It is possible to
compute the positive attractor in $\mathcal{O}(\lvert E\rvert)$ time [11]. In
non-stochastic games, a positive-attractor to a set $T$ is the same as an
attractor to the set $T$, which we denote this by $\mathsf{Attr}_{i}(T)$. It
is easy to derive from the computation of $\mathsf{PosAttr}_{i}(T)$ a
memoryless strategy for $\textrm{Player}\leavevmode\nobreak\ {i}$ that ensures
the positive satisfaction of $\mathsf{Reach}(T)$. We call such a strategy a
_positive-attractor strategy_ of $\textrm{Player}\leavevmode\nobreak\ {i}$.

A _trap_ for $\textrm{Player}\leavevmode\nobreak\ {1}$ is a set $T\subseteq V$
such that for every vertex $v\in T$, if $v\in V_{1}\cup V_{\Diamond}$, then
$E(v)\subseteq T$, and if $v\in V_{2}$, then $E(v)\cap T\neq\varnothing$. that
is ${\sf PosPre}_{1}(V\setminus T)=\varnothing$. In other words, from every
vertex $v\in T$, $\textrm{Player}\leavevmode\nobreak\ {2}$ can ensure (with
probability $1$) that the game never leaves $T$, moreover using a memoryless
strategy. A trap for $\textrm{Player}\leavevmode\nobreak\ {2}$ can be defined
analogously.

######  Remark 2.1.

Let $G$ be a non-stochastic game with objective $\varphi$ for
$\textrm{Player}\leavevmode\nobreak\ {1}$. If $\varphi$ is closed under
suffixes, then the winning region of $\textrm{Player}\leavevmode\nobreak\ {1}$
is a trap for $\textrm{Player}\leavevmode\nobreak\ {2}$. As a corollary, if
$\varphi$ is prefix-independent, then the winning region of
$\textrm{Player}\leavevmode\nobreak\ {1}$ is a trap for
$\textrm{Player}\leavevmode\nobreak\ {2}$ and the winning region of
$\textrm{Player}\leavevmode\nobreak\ {2}$ is a trap for
$\textrm{Player}\leavevmode\nobreak\ {1}$.

##  3 Window mean payoff

We consider two types of window mean-payoff objectives, introduced in [9]:
$(i)$ _fixed window mean-payoff_ objective ($\mathsf{FWMP}(\ell)$) in which a
window length $\ell\geq 1$ is given, and $(ii)$ _bounded window mean-payoff_
objective ($\mathsf{BWMP}$) in which for every play, we need a bound on window
lengths. We define these objectives below.

For a play $\pi$ in a stochastic game $\mathcal{G}$, the _total payoff_ of an
infix $\pi(i,i+n)=v_{i}v_{i+1}\dotsm v_{i+n}$ is the sum of the payoffs of the
edges in the infix and is defined as
$\mathsf{TP}(\pi(i,i+n))=\sum_{k=i}^{i+n-1}w(v_{k},v_{k+1})$. The _mean
payoff_ of an infix $\pi(i,i+n)$ is the average of the payoffs of the edges in
the infix and is defined as
$\mathsf{MP}(\pi(i,i+n))=\frac{1}{n}\mathsf{TP}(\pi(i,i+n))=\sum_{k=i}^{i+n-1}\frac{1}{n}w(v_{k},v_{k+1})$.
The mean payoff of a play $\pi$ is defined as
$\mathsf{MP}(\pi)=\displaystyle{\liminf_{n\rightarrow\infty}}\;\mathsf{MP}(\pi(0,n))$.

Given a window length $\ell\geq 1$, a play $\pi=v_{0}v_{1}\dotsm$ in
$\mathcal{G}$ satisfies the _fixed window mean-payoff objective_
$\mathsf{FWMP}_{\mathcal{G}}(\ell)$ if from every position after some point,
it is possible to start an infix of length at most $\ell$ with a nonnegative
mean payoff. Formally,

$\mathsf{FWMP}_{\mathcal{G}}(\ell)=\\{\pi\in\mathsf{Plays}_{\mathcal{G}}\mid\exists
k\geq 0\cdot\forall i\geq k\cdot\exists
j\in\\{1,\ldots,\ell\\}:\mathsf{MP}(\pi(i,i+j))\geq 0\\}.$

We omit the subscript $\mathcal{G}$ when it is clear from the context. In this
definition, there is no loss of generality in considering mean-payoff
threshold $0$ rather than some $\lambda\in\mathbb{Q}$: consider the game
$\mathcal{G}^{\prime}$ obtained by subtracting $\lambda$ from every edge
payoff in $\mathcal{G}$, and the mean payoff of any infix of a play in
$\mathcal{G}$ is at least $\lambda$ if and only if its mean payoff in
$\mathcal{G}^{\prime}$ is nonnegative. Moreover, observe that the mean payoff
of an infix is nonnegative if and only if the total-payoff of the infix is
nonnegative.

Note that when $\ell=1$, the $\mathsf{FWMP}(1)$ and
$\overline{\mathsf{FWMP}(1)}$ (i.e., the complement of $\mathsf{FWMP}(1)$)
objectives reduce to coBüchi and Büchi objectives respectively. To see this,
let $T$ be the set of all vertices $v\in V$ such that either $v\in V_{1}$ and
all out-edges of $v$ have a negative payoff, or $v\in V_{2}$ and at least one
out-edge of $v$ has a negative payoff. Then, a play satisfies the
$\overline{\mathsf{FWMP}(1)}$ objective if and only if it satisfies the
Büchi$(T)$ objective. The following properties of $\mathsf{FWMP}(\ell)$ have
been observed in [9]. The fixed window mean-payoff objective provides a robust
and conservative approximation of the traditional mean-payoff objective,
defined as the set of plays with nonnegative mean payoff: for all window
lengths $\ell$, if a play $\pi$ satisfies $\mathsf{FWMP}_{\mathcal{G}}(\ell)$,
then it has a nonnegative mean payoff. Since $\ell\leq\ell^{\prime}$ implies
$\mathsf{FWMP}_{\mathcal{G}}(\ell)\subseteq\mathsf{FWMP}_{\mathcal{G}}(\ell^{\prime})$,
more precise approximations of mean payoff can be obtained by increasing the
window length. In all plays satisfying $\mathsf{FWMP}(\ell)$, there exists a
suffix that can be decomposed into infixes of length at most $\ell$, each with
a nonnegative mean payoff. Such a desirable robust property is not guaranteed
by the classical mean-payoff objective, where infixes of unbounded lengths may
have negative mean payoff.

As defined in [9], given a play $\pi=v_{0}v_{1}\cdots$ and $0\leq i<j$, we say
that the window $\pi(i,j)$ is _open_ if the total-payoff of $\pi(i,k)$ is
negative for all $i<k\leq j$. Otherwise, the window is _closed_. Given $j>0$,
we say a window is open at $j$ if there exists an open window $\pi(i,j)$ for
some $i<j$. The window starting at position $i$ _closes_ at position $j$ if
$j$ is the first position after $i$ such that the total payoff of $\pi(i,j)$
is nonnegative. If the window starting at $i$ closes at $j$, then for all
$i\leq k<j$, the windows $\pi(k,j)$ are closed. This property is called the
_inductive property of windows_. A play $\pi$ satisfies $\mathsf{FWMP}(\ell)$
if and only if, from some point on, every window in $\pi$ closes within at
most $\ell$ steps.

We also consider the bounded window mean payoff objective
$\mathsf{BWMP}_{\mathcal{G}}$. We omit the subscript $\mathcal{G}$ when it is
clear from the context. A play $\pi$ satisfies the $\mathsf{BWMP}$ objective
if there exists a window length $\ell\geq 1$ for which $\pi$ satisfies
$\mathsf{FWMP}(\ell)$. Formally,

$\displaystyle\mathsf{BWMP}_{\mathcal{G}}$
$\displaystyle=\\{\pi\in\mathsf{Plays}_{\mathcal{G}}\mid\exists\ell\geq
1:\pi\in\mathsf{FWMP}(\ell)\\}.$

Equivalently, a play $\pi$ does not satisfy $\mathsf{BWMP}$ if and only if for
every suffix of $\pi$, for all $\ell\geq 1$, the suffix contains an open
window of length $\ell$. Note that both $\mathsf{FWMP}(\ell)$ for all
$\ell\geq 1$ and $\mathsf{BWMP}$ are prefix-independent objectives.

#### Decision problems.

Given a game $\mathcal{G}$, an initial vertex $v\in V$, a rational threshold
$p\in[0,1]$, and an objective $\varphi$ (that is either $\mathsf{FWMP}(\ell)$
for a given window length $\ell\geq 1$, or $\mathsf{BWMP}$), consider the
problem of deciding:

  * •

_Positive satisfaction of $\varphi$_: if $\textrm{Player}\leavevmode\nobreak\
{1}$ positively wins $\varphi$ from $v$, i.e., if $v\in\langle\\!\langle
1\rangle\\!\rangle^{\mathsf{Pos}}_{\mathcal{G}}(\varphi)$.

  * •

_Almost-sure satisfaction of $\varphi$_: if
$\textrm{Player}\leavevmode\nobreak\ {1}$ almost-surely wins $\varphi$ from
$v$, i.e., if $v\in\langle\\!\langle
1\rangle\\!\rangle^{\mathsf{AS}}_{\mathcal{G}}(\varphi)$.

  * •

_Quantitative satisfaction of $\varphi$_ (also known as _quantitative value
problem_ [14]): if $\textrm{Player}\leavevmode\nobreak\ {1}$ wins $\varphi$
from $v$ with probability at least $p$, i.e., if
$\sup_{\sigma_{1}\in\Lambda_{1}}\inf_{\sigma_{2}\in\Lambda_{2}}\mathsf{Pr}^{\sigma_{1},\sigma_{2}}_{\mathcal{G},v}(\varphi)\geq
p$.

Note that these three problems coincide for non-stochastic games. As
considered in previous works [9, 4, 5], the window length $\ell$ is usually
small (typically $\ell\leq\lvert V\rvert$), and therefore we assume that
$\ell$ is given in unary (while the payoff on the edges is given in binary).

#### Determinacy.

From determinacy of Blackwell games [25], stochastic games with window mean-
payoff objectives as defined above are determined, i.e., the largest
probability with which $\textrm{Player}\leavevmode\nobreak\ {1}$ is winning
and the largest probability with which $\textrm{Player}\leavevmode\nobreak\
{2}$ is winning add up to $1$.

#### Algorithms for non-stochastic window mean-payoff games.

To compute the positive and almost-sure winning regions for
$\textrm{Player}\leavevmode\nobreak\ {1}$ for $\mathsf{FWMP}(\ell)$, we recall
intermediate objectives defined in [9]. The _good window_ objective
$\mathsf{GW}_{\mathcal{G}}(\ell)$ consists of all plays $\pi$ in $\mathcal{G}$
such that the window opened at the first position in the play closes in at
most $\ell$ steps:

$\mathsf{GW}_{\mathcal{G}}(\ell)=\\{\pi\in\mathsf{Plays}_{\mathcal{G}}\mid\exists
j\in\\{1,\ldots,\ell\\}:\mathsf{MP}(\pi(0,j))\geq 0\\}.$

The _direct fixed window mean-payoff_ objective
$\mathsf{DirFWMP}_{\mathcal{G}}(\ell)$ consists of all plays $\pi$ in
$\mathcal{G}$ such that from every position in $\pi$, the window closes in at
most $\ell$ steps:

$\mathsf{DirFWMP}_{\mathcal{G}}(\ell)=\\{\pi\in\mathsf{Plays}_{\mathcal{G}}\mid\forall
i\geq 0:\pi(i,\infty)\in\mathsf{GW}_{\mathcal{G}}(\ell)\\}.$

The $\mathsf{FWMP}_{\mathcal{G}}(\ell)$ objective can be expressed in terms of
$\mathsf{DirFWMP}_{\mathcal{G}}(\ell)$:

$\mathsf{FWMP}_{\mathcal{G}}(\ell)=\\{\pi\in\mathsf{Plays}_{\mathcal{G}}\mid\exists
k\geq 0:\pi(k,\infty)\in\mathsf{DirFWMP}_{\mathcal{G}}(\ell)\\}.$

We refer to Algorithm 1, 2, and 3 from [9] shown below with the same
numbering. They compute the winning regions for
$\textrm{Player}\leavevmode\nobreak\ {1}$ for the $\mathsf{FWMP}(\ell)$,
$\mathsf{DirFWMP}(\ell)$, and $\mathsf{GW}(\ell)$ objectives in non-stochastic
games respectively. [9, Algorithm 2 and Algorithm 3] contain subtle errors for
which the fixes are known [7, 20]. In fact, a related objective that is a
combination of the good window and reachability objectives was studied in [20]
and [7] from which the correct algorithms can be derived. For completeness, we
include below counterexamples for the versions in [9], along with the correct
algorithms and brief explanations of correctness.

Algorithm 1 $\textup{{NonStocFWMP}}(G,\ell)$ [9, Algorithm 1]

1: $G=((V,E),(V_{1},V_{2},\varnothing),w)$, the non-stochastic game, and
$\ell\geq 1$, the window length

2: The set of vertices in $V$ from which $\textrm{Player}\leavevmode\nobreak\
{1}$ wins $\mathsf{FWMP}(\ell)$

3: $W_{d}\leftarrow\textup{{NonStocDirFWMP}}(G,\ell)$

4: $W_{d}\leftarrow\textup{{NonStocDirFWMP}}(G,\ell)$ if $W_{d}=\varnothing$
then

5: return $\varnothing$

6: return $\varnothing$ return $\varnothing$ else

7: $A\leftarrow\mathsf{Attr}_{1}(W_{d})$

8: return $A\cup\textup{{NonStocFWMP}}(G\upharpoonright(V\setminus A),\ell)$
return $A\cup\textup{{NonStocFWMP}}(G\upharpoonright(V\setminus A),\ell)$

Algorithm 2 $\textup{{NonStocDirFWMP}}(G,\ell)$

1: $G=((V,E),(V_{1},V_{2},\varnothing),w)$ the non-stochastic game, and
$\ell\geq 1$, the window length

2: The set of vertices in $V$ from which $\textrm{Player}\leavevmode\nobreak\
{1}$ wins $\mathsf{DirFWMP}(\ell)$

3: $W_{gw}\leftarrow\textup{{GoodWin}}(G,\ell)$

4: $W_{gw}\leftarrow\textup{{GoodWin}}(G,\ell)$ if $W_{gw}=V$ or
$W_{gw}=\varnothing$ then

5: return $W_{gw}$

6: return $W_{gw}$ return $W_{gw}$ else

7: $A\leftarrow\mathsf{Attr}_{2}(V\setminus W_{gw})$

8: return $\textup{{NonStocDirFWMP}}(G\restriction(W_{gw}\setminus A),\ell)$
return $\textup{{NonStocDirFWMP}}(G\restriction(W_{gw}\setminus A),\ell)$

Algorithm 3 $\textup{{GoodWin}}(G,\ell)$

1: $G=((V,E),(V_{1},V_{2},\varnothing),w)$ the non-stochastic game, and
$\ell\geq 1$, the window length

2: The set of vertices in $V$ from which $\textrm{Player}\leavevmode\nobreak\
{1}$ wins $\mathsf{GW}(\ell)$

3: The set of vertices in $V$ from which $\textrm{Player}\leavevmode\nobreak\
{1}$ wins $\mathsf{GW}(\ell)$ for all $v\in V$ do

4: $C_{0}(v)\leftarrow 0$

5: $C_{0}(v)\leftarrow 0$ for all $i\in\\{1,\ldots,\ell\\}$ do

6: $C_{i}(v)\leftarrow-\infty$ $C_{i}(v)\leftarrow-\infty$
$C_{i}(v)\leftarrow-\infty$ $C_{i}(v)\leftarrow-\infty$

7: $C_{i}(v)\leftarrow-\infty$ for all $i\in\\{1,\ldots,\ell\\}$ do

8: for all $i\in\\{1,\ldots,\ell\\}$ do for all $v\in V_{1}$ do

9: $C_{i}(v)\leftarrow\max_{(v,v^{\prime})\in
E}\\{\max\\{w(v,v^{\prime}),w(v,v^{\prime})+C_{i-1}(v^{\prime})\\}\\}$
$\triangleright$ In [9], $w(v,v^{\prime})+C_{i-1}(v^{\prime})$ was used
instead of $\max\\{w(v,v^{\prime}),w(v,v^{\prime})+C_{i-1}(v^{\prime})\\}$.
$C_{i}(v)\leftarrow\max_{(v,v^{\prime})\in
E}\\{\max\\{w(v,v^{\prime}),w(v,v^{\prime})+C_{i-1}(v^{\prime})\\}\\}$
$\triangleright$ In [9], $w(v,v^{\prime})+C_{i-1}(v^{\prime})$ was used
instead of $\max\\{w(v,v^{\prime}),w(v,v^{\prime})+C_{i-1}(v^{\prime})\\}$.

10: $C_{i}(v)\leftarrow\max_{(v,v^{\prime})\in
E}\\{\max\\{w(v,v^{\prime}),w(v,v^{\prime})+C_{i-1}(v^{\prime})\\}\\}$
$\triangleright$ In [9], $w(v,v^{\prime})+C_{i-1}(v^{\prime})$ was used
instead of $\max\\{w(v,v^{\prime}),w(v,v^{\prime})+C_{i-1}(v^{\prime})\\}$.
for all $v\in V_{2}$ do

11: $C_{i}(v)\leftarrow\min_{(v,v^{\prime})\in
E}\\{\max\\{w(v,v^{\prime}),w(v,v^{\prime})+C_{i-1}(v^{\prime})\\}\\}$
$\triangleright$ In [9], $w(v,v^{\prime})+C_{i-1}(v^{\prime})$ was used
instead of $\max\\{w(v,v^{\prime}),w(v,v^{\prime})+C_{i-1}(v^{\prime})\\}$.
$C_{i}(v)\leftarrow\min_{(v,v^{\prime})\in
E}\\{\max\\{w(v,v^{\prime}),w(v,v^{\prime})+C_{i-1}(v^{\prime})\\}\\}$
$\triangleright$ In [9], $w(v,v^{\prime})+C_{i-1}(v^{\prime})$ was used
instead of $\max\\{w(v,v^{\prime}),w(v,v^{\prime})+C_{i-1}(v^{\prime})\\}$.
$C_{i}(v)\leftarrow\min_{(v,v^{\prime})\in
E}\\{\max\\{w(v,v^{\prime}),w(v,v^{\prime})+C_{i-1}(v^{\prime})\\}\\}$
$\triangleright$ In [9], $w(v,v^{\prime})+C_{i-1}(v^{\prime})$ was used
instead of $\max\\{w(v,v^{\prime}),w(v,v^{\prime})+C_{i-1}(v^{\prime})\\}$.
$C_{i}(v)\leftarrow\min_{(v,v^{\prime})\in
E}\\{\max\\{w(v,v^{\prime}),w(v,v^{\prime})+C_{i-1}(v^{\prime})\\}\\}$
$\triangleright$ In [9], $w(v,v^{\prime})+C_{i-1}(v^{\prime})$ was used
instead of $\max\\{w(v,v^{\prime}),w(v,v^{\prime})+C_{i-1}(v^{\prime})\\}$.

12: $W_{gw}\leftarrow\\{v\in V\mid C_{\ell}(v)\geq 0\\}$ $\triangleright$ In
[9], $W_{gw}$ was defined as $\\{v\in V\mid\exists i\in\\{1,2,\ldots\ell\\},\
C_{i}(v)\geq 0\\}$ instead because $C_{i}(v)$ had a different definition in
[9].

13: return $W_{gw}$

$v_{1}$$v_{2}$$v_{3}$$v_{4}$$v_{5}$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}-1}$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}-1}$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}-1}$

(a) A counterexample for computing winning region for $\mathsf{DirFWMP}(\ell)$
[9, Algorithm 2] with $\ell=2$.

$v_{1}$$v_{2}$$v_{3}$$v_{4}$$v_{5}$$v_{6}$$v_{7}$$v_{8}$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}-1}$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}-1}$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}2}$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}3}$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0}$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}-2}$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0}$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}2}$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0}$

(b) A counterexample for computing winning region for $\mathsf{GW}(\ell)$ [9,
Algorithm 3] with $\ell=3$.

Figure 2: Counterexamples for algorithms in [9]

#### Description of algorithms from [9].

Algorithm 1 [9, Algorithm 1] computes the winning region of
$\textrm{Player}\leavevmode\nobreak\ {1}$ for the $\mathsf{FWMP}(\ell)$
objective. First (Line 4) it computes the winning region $W_{d}$ for
$\textrm{Player}\leavevmode\nobreak\ {1}$ for the $\mathsf{DirFWMP}(\ell)$
objective (using Algorithm 2). All vertices in the
$\text{Player\leavevmode\nobreak\ }1$ attractor of $W_{d}$ (Line 7) are also
winning, as $\mathsf{FWMP}(\ell)$ is closed under prefixes. If the attractor
is empty, then it is easy to show that the winning region for
$\textrm{Player}\leavevmode\nobreak\ {1}$ for objective $\mathsf{FWMP}(\ell)$
is also empty, and the algorithm terminates (Line 6). Otherwise, the remaining
states (i.e., the complement of the attractor) induce a smaller subgame, which
can be solved (recursively) by the same algorithm.

Algorithm 2 computes the winning region of
$\textrm{Player}\leavevmode\nobreak\ {1}$ for the $\mathsf{DirFWMP}(\ell)$
objective. It does so by first computing the region $V\setminus W_{gw}$ from
which $\textrm{Player}\leavevmode\nobreak\ {1}$ cannot win the good window
objective $\mathsf{GW}(\ell)$ (Line 6). If
$\textrm{Player}\leavevmode\nobreak\ {1}$ does not win the $\mathsf{GW}(\ell)$
objective, then she does not win the $\mathsf{DirFWMP}(\ell)$ objective
either, and thus, all vertices in $V\setminus W_{gw}$ are losing for
$\textrm{Player}\leavevmode\nobreak\ {1}$. If $V\setminus W_{gw}$ is empty,
that is, if $W_{gw}=V$, then $\textrm{Player}\leavevmode\nobreak\ {1}$ wins
the $\mathsf{GW}(\ell)$ objective from every vertex, and it is easy to see
that $\textrm{Player}\leavevmode\nobreak\ {1}$ also wins the
$\mathsf{DirFWMP}(\ell)$ objective from every vertex. Otherwise, the
$\text{Player\leavevmode\nobreak\ }2$ attractor to $V\setminus W_{gw}$ is also
losing for $\textrm{Player}\leavevmode\nobreak\ {1}$. The remaining states
(i.e., the complement of $A$) induce a smaller subgame, which can be solved
(recursively) by the same algorithm.

Algorithm 3 computes the winning region of
$\textrm{Player}\leavevmode\nobreak\ {1}$ for the good window objective
$\mathsf{GW}(\ell)$, that is, the set of vertices from which
$\textrm{Player}\leavevmode\nobreak\ {1}$ can close the window within at most
$\ell$ steps. The algorithm uses dynamic programming to compute, for all $v\in
V$ and all lengths $i\in\\{1,\ldots,\ell\\}$, the largest payoff $C_{i}(v)$
that $\textrm{Player}\leavevmode\nobreak\ {1}$ can ensure from $v$ within at
most $i$ steps. The winning region for $\mathsf{GW}(\ell)$ for
$\textrm{Player}\leavevmode\nobreak\ {1}$ consists of all vertices $v$ such
that $C_{\ell}(v)\geq 0$.

#### Correctness of Algorithm 2.

We show the correctness of Algorithm 2, that is, we show that this algorithm
correctly computes $\langle\\!\langle
1\rangle\\!\rangle^{\mathsf{}}_{G}(\mathsf{DirFWMP}(\ell))$, the winning
region for $\textrm{Player}\leavevmode\nobreak\ {1}$ for the
$\mathsf{DirFWMP}(\ell)$ objective. The proof makes use of the fact that
$\mathsf{DirFWMP}(\ell)\subseteq\mathsf{GW}(\ell)$, that is, if
$\textrm{Player}\leavevmode\nobreak\ {1}$ does not win $\mathsf{GW}(\ell)$
from a vertex $v\in V$, then she also does not win $\mathsf{DirFWMP}(\ell)$
from $v$.

The algorithm successively finds vertices that are losing for
$\textrm{Player}\leavevmode\nobreak\ {1}$ for the $\mathsf{GW}(\ell)$
objective, removes them, and recurses on the rest of the game graph. In Line
4, we have $W_{gw}=\langle\\!\langle
1\rangle\\!\rangle^{\mathsf{}}_{G}(\mathsf{GW}(\ell))$, the winning region for
$\textrm{Player}\leavevmode\nobreak\ {1}$ for the $\mathsf{GW}(\ell)$
objective.

  * •

If $W_{gw}=\varnothing$, then $\textrm{Player}\leavevmode\nobreak\ {2}$ wins
$\overline{\mathsf{GW}(\ell)}$ from all vertices in $V$, and therefore,
$\textrm{Player}\leavevmode\nobreak\ {2}$ also wins
$\overline{\mathsf{DirFWMP}(\ell)}$ from all vertices in $V$. Hence,
$\langle\\!\langle
1\rangle\\!\rangle^{\mathsf{}}_{G}(\mathsf{DirFWMP}(\ell))=\varnothing$.

  * •

Otherwise, if $W_{gw}=V$, then $\textrm{Player}\leavevmode\nobreak\ {1}$ wins
$\mathsf{GW}(\ell)$ from all vertices in $G$. For all vertices $v\in V$,
starting from $v$, $\textrm{Player}\leavevmode\nobreak\ {1}$ can ensure that
the window starting at $v$ closes in at most $\ell$ steps. When the window
starting at $v$ closes, suppose the token is on a vertex $v^{\prime}$. By the
inductive property of windows, all windows that opened after $v$ are also
closed by the time the token reaches $v^{\prime}$. Now, since
$v^{\prime}\in\langle\\!\langle
1\rangle\\!\rangle^{\mathsf{}}_{G}(\mathsf{GW}(\ell))$,
$\textrm{Player}\leavevmode\nobreak\ {1}$ can ensure that the window starting
at $v^{\prime}$ also closes in at most $\ell$ steps. In this manner,
$\textrm{Player}\leavevmode\nobreak\ {1}$ closes every window in at most
$\ell$ steps, resulting in an outcome that is winning for the
$\mathsf{DirFWMP}(\ell)$ objective. We get that $\langle\\!\langle
1\rangle\\!\rangle^{\mathsf{}}_{G}(\mathsf{DirFWMP}(\ell))=V$.

  * •

Finally, suppose $\varnothing\subsetneq W_{gw}\subsetneq V$. Starting from
$V\setminus W_{gw}$, $\textrm{Player}\leavevmode\nobreak\ {2}$ wins the
$\overline{\mathsf{GW}(\ell)}$ objective, and hence, also the
$\overline{\mathsf{DirFWMP}(\ell)}$ objective. Therefore, no vertex in
$V\setminus W_{gw}$ belongs to $\langle\\!\langle
1\rangle\\!\rangle^{\mathsf{}}_{G}(\mathsf{DirFWMP}(\ell))$. Moreover,
consider the $\textrm{Player}\leavevmode\nobreak\ {2}$ attractor $A$ to
$V\setminus W_{gw}$ (Line 7). Starting from a vertex in this attractor,
$\textrm{Player}\leavevmode\nobreak\ {2}$ can follow a memoryless strategy to
eventually reach $V\setminus W_{gw}$. Once the token reaches $V\setminus
W_{gw}$, $\textrm{Player}\leavevmode\nobreak\ {2}$ can ensure that a window
remains open for $\ell$ steps, resulting in
$\textrm{Player}\leavevmode\nobreak\ {1}$ losing. Hence, no vertex in the
attractor belongs to $\langle\\!\langle
1\rangle\\!\rangle^{\mathsf{}}_{G}(\mathsf{DirFWMP}(\ell))$ either. The
complement of this $\textrm{Player}\leavevmode\nobreak\ {2}$ attractor is a
trap for $\textrm{Player}\leavevmode\nobreak\ {2}$ and induces a subgame. For
all vertices $v$ in this subgame, if $\textrm{Player}\leavevmode\nobreak\ {1}$
wins from $v$ in the subgame, then she also wins from $v$ in the original game
as she can mimic a winning strategy from the subgame while also ensuring that
the token never leaves the subgame. Conversely, for all vertices $v$ in the
subgame, if $\textrm{Player}\leavevmode\nobreak\ {1}$ does not win from $v$ in
the subgame, then she also does not win from $v$ in the original game. This is
because if the token remains in the subgame forever, then
$\textrm{Player}\leavevmode\nobreak\ {2}$ wins, and if the token ever leaves
the subgame, then as discussed above, the token enters the
$\textrm{Player}\leavevmode\nobreak\ {2}$ attractor, and
$\textrm{Player}\leavevmode\nobreak\ {2}$ wins. Thus, for all vertices $v$ in
the subgame, $\textrm{Player}\leavevmode\nobreak\ {1}$ wins from $v$ in the
subgame if and only if she wins from $v$ in the original game. Hence, the
winning region for $\textrm{Player}\leavevmode\nobreak\ {1}$ in the subgame is
equal to the winning region for $\textrm{Player}\leavevmode\nobreak\ {1}$ in
the original game, and hence, the algorithm recurses on this subgame.

#### Correctness of Algorithm 3.

The following characterization of $C_{i}(v)$ holds:

  * •

There exists a strategy $\sigma_{1}$ of $\textrm{Player}\leavevmode\nobreak\
{1}$ such that for all strategies $\sigma_{2}$ of
$\textrm{Player}\leavevmode\nobreak\ {2}$, there exists $1\leq j\leq i$ such
that in the outcome of the strategy profile $(\sigma_{1},\sigma_{2})$ with
initial vertex $v$, the total payoff in the first $j$ steps of the outcome is
at least $C_{i}(v)$;

  * •

For all strategies $\sigma_{1}$ of $\textrm{Player}\leavevmode\nobreak\ {1}$,
there exists a strategy $\sigma_{2}$ of $\textrm{Player}\leavevmode\nobreak\
{2}$ such that for all $1\leq j\leq i$, the total payoff of the first $j$
steps in the outcome of $(\sigma_{1},\sigma_{2})$ with initial vertex $v$ is
at most $C_{i}(v)$.

A monotonicity property follows from the above characterization, namely that
for all $v\in V$, if $1\leq i\leq j\leq\ell$, then $C_{i}(v)\leq C_{j}(v)$,
which can also easily be established from Algorithm 3. Note that monotonicity
does not hold for $i=0$ as $C_{0}(v)=0$ for all $v\in V$, but we may have
$C_{1}(v)<0$ (e.g., if all outgoing edges from $v$ have negative weight). It
also follows from this characterization that $C_{i}(v)\geq 0$ if
$\textrm{Player}\leavevmode\nobreak\ {1}$ wins from $v$ for objective
$\mathsf{GW}(i)$.

We now show the correctness of Algorithm 3 to compute $C_{i}(\cdot)$, by
induction on $i\in\\{1,\ldots,\ell\\}$. The base case $i=1$ holds since
$C_{0}(v)=0$ for all $v\in V$ and the maximum possible payoff from $v$ in one
step is $C_{1}(v)=\max_{(v,v^{\prime})\in E}\\{w(v,v^{\prime})\\}$ if $v\in
V_{1}$ is a vertex of $\textrm{Player}\leavevmode\nobreak\ {1}$, and
$C_{1}(v)=\min_{(v,v^{\prime})\in E}\\{w(v,v^{\prime})\\}$ if $v\in V_{2}$ is
a vertex of $\textrm{Player}\leavevmode\nobreak\ {2}$. For the induction step
$i\geq 2$, assume that $C_{i-1}(v)$ is correctly computed by the algorithm for
all $v\in V$, as the maximum payoff that $\textrm{Player}\leavevmode\nobreak\
{1}$ can ensure from $v$ in at least $1$ and at most $i-1$ steps. Then, from a
vertex $v$ and if the edge $(v,v^{\prime})$ is chosen (either by
$\textrm{Player}\leavevmode\nobreak\ {1}$ or by
$\textrm{Player}\leavevmode\nobreak\ {2}$), the maximum payoff that
$\textrm{Player}\leavevmode\nobreak\ {1}$ can ensure in at least $1$ and at
most $i$ steps is either $w(v,v^{\prime})$ (in $1$ step) or
$w(v,v^{\prime})+C_{i-1}(v^{\prime})$ (in at least $1+1=2$ steps and at most
$1+i-1=i$ steps), whichever is greater. Hence if $v\in V_{1}$ is a vertex of
$\textrm{Player}\leavevmode\nobreak\ {1}$, then $C_{i}(v)$ is the maximum such
value across the out-neighbours $v^{\prime}$ of $v$, and if $v\in V_{2}$ is a
vertex of $\textrm{Player}\leavevmode\nobreak\ {2}$, then $C_{i}(v)$ is the
minimum, as in Line 10 and Line 11 of the algorithm. Finally by the
characterization of $C_{i}(v)$, $\textrm{Player}\leavevmode\nobreak\ {1}$ wins
from $v$ for the $\mathsf{GW}(\ell)$ objective if $C_{\ell}(v)\geq 0$ (Line
12), which by the monotonicity property, is equivalent to the condition
$\exists 1\leq i\leq\ell:C_{i}(v)\geq 0$ used in [9].

#### Counterexample for [9, Algorithm 2].

The version of Algorithm 2 in [9] does not compute (and does not remove) the
$\text{Player\leavevmode\nobreak\ }2$ attractor $\mathsf{Attr}_{2}(V\setminus
W_{gw})$ to the winning region of $\textrm{Player}\leavevmode\nobreak\ {2}$
for the good-window objective (Line 7). However, it is easy to see that
$\textrm{Player}\leavevmode\nobreak\ {2}$ can spoil the good-window objective
from $A$, not only from $V\setminus W_{gw}$. This may lead to incorrectly
classifying some losing states as being winning (for
$\textrm{Player}\leavevmode\nobreak\ {1}$). Consider the non-stochastic game
shown in Figure 2(a) with $\ell=2$. The vertices $v_{4}$ and $v_{5}$ are
losing for $\textrm{Player}\leavevmode\nobreak\ {1}$ for
$\mathsf{DirFWMP}(\ell)$, and since $v_{1}\in V_{2}$, the vertex $v_{1}$ is
also losing for $\textrm{Player}\leavevmode\nobreak\ {1}$. The remaining
vertices $\\{v_{2},v_{3}\\}$ are winning for
$\textrm{Player}\leavevmode\nobreak\ {1}$. After computing the winning region
of $\textrm{Player}\leavevmode\nobreak\ {2}$ for the good-window objective,
which is $\\{v_{4},v_{5}\\}$, the winning region in the subgame induced by
$V\setminus\\{v_{4},v_{5}\\}=\\{v_{1},v_{2},v_{3}\\}$ is
$\\{v_{1},v_{2},v_{3}\\}$, which is returned as the winning region for
$\mathsf{DirFWMP}(\ell)$, instead of $\\{v_{2},v_{3}\\}$.

#### Counterexample for [9, Algorithm 3].

The version of Algorithm 3 in [9] differs at Line 10 and Line 11, and we show
that it does not compute the winning region for the good-window objective.

Consider the non-stochastic game $G$ shown in Figure 2(b) with $\ell=3$. The
vertex $v_{1}$ is winning for $\mathsf{GW}(3)$ since the window closes in
three steps irrespective of the successor chosen by
$\textrm{Player}\leavevmode\nobreak\ {2}$ from $v_{2}$. If
$\textrm{Player}\leavevmode\nobreak\ {2}$ chooses $v_{3}$ from $v_{2}$, the
window closes in three steps, whereas if $\textrm{Player}\leavevmode\nobreak\
{2}$ chooses $v_{5}$ from $v_{2}$, the window closes in two steps. However,
Algorithm 3 in [9] does not include $v_{1}$ in the winning region for
$\mathsf{GW}(3)$. This is because for every vertex $v$ in the game, it
computes for all $1\leq i\leq\ell$, the value $C_{i}(v)$ as the best payoff
that $\textrm{Player}\leavevmode\nobreak\ {1}$ can ensure from $v$ in
_exactly_ $i$ steps, instead of at most $i$ steps. The algorithm includes a
vertex $v$ in the winning region for $\mathsf{GW}(\ell)$ if at least one of
the $C_{i}(v)$ is nonnegative. In our example, the best payoff that
$\textrm{Player}\leavevmode\nobreak\ {1}$ can ensure from $v_{1}$ in exactly
one step is $-1$, in exactly two steps is $-2$ (corresponding to the prefix
$v_{1}v_{2}v_{3})$, and in exactly three steps is $-1$ (corresponding to the
prefix $v_{1}v_{2}v_{5}v_{6})$. Thus, for all $1\leq i\leq 3$, the value
$C_{i}(v_{1})$ is negative. This example shows that it is possible for
$\textrm{Player}\leavevmode\nobreak\ {1}$ to ensure a nonnegative payoff in at
most $\ell$ steps despite the worst payoff in exactly $i$ steps being negative
for all $i\in\\{1,\ldots,\ell\\}$.

##  4 Memory requirement for non-stochastic window mean-payoff games

The memory requirement for winning strategies of both
$\textrm{Player}\leavevmode\nobreak\ {1}$ and
$\textrm{Player}\leavevmode\nobreak\ {2}$ in non-stochastic games with
objective $\mathsf{FWMP}(\ell)$ is claimed to be $\mathcal{O}(\lvert
V\rvert\cdot\ell)$ without proof [9, Lemma 7]. Further, the bounds are
“correctly stated” as $\mathcal{O}(w_{\max}\cdot\ell^{2})$ and
$\mathcal{O}(w_{\max}\cdot\ell^{2}\cdot\lvert V\rvert)$ for
$\textrm{Player}\leavevmode\nobreak\ {1}$ and
$\textrm{Player}\leavevmode\nobreak\ {2}$ respectively, where $w_{\max}$ is
the maximum absolute payoff in the graph [7, Theorem 2]. We improve upon these
bounds and show that memory of size $\ell$ suffices for a winning strategy of
$\textrm{Player}\leavevmode\nobreak\ {1}$. Furthermore, a formal argument for
memory requirement for $\textrm{Player}\leavevmode\nobreak\ {2}$ strategies is
missing in [9] which we provide here.

We show constructions of Mealy machines $M_{1}^{\mathsf{NS}}$ and
$M_{2}^{\mathsf{NS}}$ (with at most $\ell$ and $\lvert V\rvert\cdot\ell$
states respectively) that define winning strategies $\sigma_{1}^{\mathsf{NS}}$
and $\sigma_{2}^{\mathsf{NS}}$ of $\textrm{Player}\leavevmode\nobreak\ {1}$
and $\textrm{Player}\leavevmode\nobreak\ {2}$ respectively, showing upper
bounds on the memory requirements for both players. We also present a family
of games with arbitrarily large state space where
$\textrm{Player}\leavevmode\nobreak\ {2}$ is winning and all his winning
strategies require at least $\frac{1}{2}(\lvert V\rvert-\ell)+3$ memory, while
it was only known that memoryless strategies are not sufficient for
$\textrm{Player}\leavevmode\nobreak\ {2}$ [9].

The paper [9] also has results on the analysis of the $\mathsf{BWMP}$
objective. It has been shown that solving $\mathsf{BWMP}$ for non-stochastic
games is in $\mathsf{NP}\cap\mathsf{coNP}$, and memoryless strategies suffice
for $\textrm{Player}\leavevmode\nobreak\ {1}$, whereas
$\textrm{Player}\leavevmode\nobreak\ {2}$ may need infinite memory strategies
to play optimally.

###  4.1 Memory requirement for Player 1 for FWMP objective

#### Upper bound on memory requirement for Player 1.

We show that memory of size $\ell$ suffices for winning strategies of
$\textrm{Player}\leavevmode\nobreak\ {1}$ for the $\mathsf{DirFWMP}(\ell)$
objective (Lemma 4.1), which is in turn used to show that the same memory also
works for the $\mathsf{FWMP}(\ell)$ objective (Theorem 4.5).

######  Lemma 4.1.

If $\textrm{Player}\leavevmode\nobreak\ {1}$ wins in a non-stochastic game
with objective $\mathsf{DirFWMP}(\ell)$, then
$\textrm{Player}\leavevmode\nobreak\ {1}$ has a winning strategy with memory
of size $\ell$.

######  Proof 4.2.

Given a game $G$, let $W_{d}$ be the winning region of
$\textrm{Player}\leavevmode\nobreak\ {1}$ in $G$ for objective
$\mathsf{DirFWMP}(\ell)$. Note that the region $W_{d}$ is a trap for
$\textrm{Player}\leavevmode\nobreak\ {2}$ in $G$, as the objective
$\mathsf{DirFWMP}(\ell)$ is closed under suffixes. Every vertex in $W_{d}$ is
moreover winning for $\textrm{Player}\leavevmode\nobreak\ {1}$ with objective
$\mathsf{GW}(\ell)$, by definition.

A winning strategy of $\textrm{Player}\leavevmode\nobreak\ {1}$ is to play for
the objective $\mathsf{GW}(\ell)$ until the window closes (which
$\textrm{Player}\leavevmode\nobreak\ {1}$ can ensure within at most $\ell$
steps), and then to restart with the same strategy, playing for
$\mathsf{GW}(\ell)$ and so on. Using memory space $Q=\\{1,\ldots,\ell\\}$, we
may store the number of steps remaining before the window must close to
satisfy $\mathsf{GW}(\ell)$, and reset the memory to $q_{0}=\ell$ whenever the
window closes. However, the window may close any time within $\ell$ steps, and
the difficulty is to detect when this happens: how to update the memory $q=i$,
given the next visited vertex $v$, but independently of the history?
Intuitively, the memory should be updated to $q=i-1$ if the window did not
close yet upon reaching $v$, and to $q=\ell$ if it did, but that depends on
which path was followed to reach $v$ (not just on $v$), which is not stored in
the memory space.

The crux is to show that it is not always necessary for
$\textrm{Player}\leavevmode\nobreak\ {1}$ to be able to infer when the window
closes. Given the current memory state $q=i$, and the next visited vertex $v$,
the memory update is as follows: if $C_{i}(v)\geq 0$ (that is,
$\textrm{Player}\leavevmode\nobreak\ {1}$ can ensure the window from $v$ will
close within $i$ steps), then we update to $q=i-1$ (decrement) although the
window may or may not have closed upon reaching $v$; otherwise $C_{i}(v)<0$
and we update to $q=\ell-1$ (reset to $\ell$ and decrement) and we show that
in this case the window did close. Intuitively, updating to $q=i-1$ is safe
even if the window did close, because the strategy of
$\textrm{Player}\leavevmode\nobreak\ {1}$ will anyway ensure the (upcoming)
window is closed within $i-1<\ell$ steps. For the case $C_{i}(v)<0$, we want
the Mealy machine to be in state $\ell$ when $v$ is being read. However, there
is an additional difficulty to this. Assume that vertex $v^{\prime}$ is read
by the Mealy machine before reading $v$. The Mealy machine is thus in state
$i+1$ and $C_{i+1}(v^{\prime})\geq 0$. Now $C_{i}(v)<0$ denotes that an open
window is closed on the edge $(v^{\prime},v)$, and the state of the Mealy
machine should be reset to $\ell$. However, if $v^{\prime}$ is a
$\textrm{Player}\leavevmode\nobreak\ {2}$ vertex, since the vertex chosen by a
$\textrm{Player}\leavevmode\nobreak\ {2}$ strategy from $v^{\prime}$ is not
known to $\textrm{Player}\leavevmode\nobreak\ {1}$ (the output on the
transition of the Mealy machine is thus $\epsilon$), the state of the Mealy
machine is updated from $i+1$ to $i$ while reading $v^{\prime}$. The state is
then updated to $\ell-1$ after reading $v$ to simulate that the window was
already closed upon reaching $v$.

For $v\in V_{1}$, we define the next vertex chosen by the strategy as

$D_{i}(v)=\arg\max_{(v,v^{\prime})\in
E}\\{\max\\{w(v,v^{\prime}),w(v,v^{\prime})+C_{i-1}(v^{\prime})\\}\\},$

the out-neighbour from $v$ that maximizes the expression of Algorithm 3 for
the $\mathsf{GW}(\ell)$ objective, Line 10. If there is more than one such
out-neighbour, we choose one arbitrarily. Example 4.3 illustrates how
computing $C_{i}(v)$ and checking if it is nonnegative is useful in
constructing a winning strategy for $\textrm{Player}\leavevmode\nobreak\ {1}$.
We see in Construction 4.4 a formal description of a Mealy machine with $\ell$
states defining a winning strategy of $\textrm{Player}\leavevmode\nobreak\
{1}$ for the $\mathsf{DirFWMP}(\ell)$ objective. This concludes the proof of
Lemma 4.1.

######  Example 4.3.

In this example, we show why checking if $C_{i}(v)$ is negative or not is
sometimes necessary. Figure 3 shows a fragment of a game where if
$\textrm{Player}\leavevmode\nobreak\ {1}$ does not know if the window has
closed, then she may choose a vertex that causes her to lose the
$\mathsf{DirFWMP}(\ell)$ objective for $\ell=4$.

$v$$u_{5}$$u_{4}$$u_{3}$$u_{1}$$u_{2}$$u_{6}$$v_{1}$$v_{2}$$v_{3}$$v_{4}$$v_{5}$$v_{6}$$+5$$+5$$-2$$0$$-2$$+3$$+1$$-4$$0$$0$$+4$$+3$$0$$0$

Figure 3:  The successor of $v$ that $\textrm{Player}\leavevmode\nobreak\ {1}$
should choose depends on how many more steps she has to close the window. If
$\textrm{Player}\leavevmode\nobreak\ {1}$ does not detect that the window is
closed on $(u_{4},u_{5})$, then she chooses $v_{4}$ from $v$. Otherwise, she
chooses $v_{1}$ from $v$. Computing $C_{2}(u_{5})$ shows that it is negative
and this implies that the window starting at $u_{3}$ must have closed at
$u_{5}$.

Suppose it is the case that all windows in the play have closed when the token
reaches $u_{1}$ and $u_{3}$. If the token reaches $v$ along $u_{1}u_{2}$, then
$\textrm{Player}\leavevmode\nobreak\ {1}$ must move the token from $v$ to
$D_{2}(v)=v_{4}$ as this closes the window starting at $u_{1}$. If
$\textrm{Player}\leavevmode\nobreak\ {1}$ moves the token from $v$ to $v_{1}$
instead, then this results in an open window $u_{1}u_{2}vv_{1}v_{2}$ of length
$4$ which is not desirable for $\textrm{Player}\leavevmode\nobreak\ {1}$.

On the other hand, if the token reaches $v$ along $u_{3}u_{4}u_{5}$, then
since the window starting at $u_{3}$ closes at $u_{5}$, we have that
$\textrm{Player}\leavevmode\nobreak\ {1}$ must choose a successor of $v$ such
that the window starting at $u_{5}$ closes in at most three steps from $v$.
Hence, if $\textrm{Player}\leavevmode\nobreak\ {1}$ moves the token from $v$
to $D_{3}(v)$, that is, $v_{1}$, then the window starting at $u_{5}$ closes in
at most $4$ steps. However, suppose $\textrm{Player}\leavevmode\nobreak\ {1}$
does not detect that the window starting at $u_{3}$ closes at $u_{5}$.
Although the total payoff along $u_{3}u_{4}u_{5}vv_{4}$ is nonnegative (which
implies that the window starting at $u_{3}$ is closed at $v_{4}$), one cannot
use the inductive property of windows to claim that all subsequent windows are
closed at $v_{4}$. The inductive property of windows does not hold since the
window starting at $u_{3}$ closes at $u_{5}$ and this gives no information
about when the window starting at $u_{5}$ closes. If
$\textrm{Player}\leavevmode\nobreak\ {1}$ plays from $v$ as if she has only
one more step to close the window, then she moves the token to
$D_{1}(v)=v_{4}$ and this results in an open window $u_{5}vv_{4}v_{5}v_{6}$ of
length $4$ which is undesirable for $\textrm{Player}\leavevmode\nobreak\ {1}$.

Thus, if $\textrm{Player}\leavevmode\nobreak\ {1}$ never detects window
closings, then this may result in open windows of length $\ell$ in the
outcome. Since $C_{2}(u_{5})$ is negative and $u_{5}$ belongs to the winning
region for $\mathsf{DirFWMP}(\ell)$, this implies that the window starting at
$u_{3}$ must have closed at $u_{5}$ and $\textrm{Player}\leavevmode\nobreak\
{1}$ cannot continue playing as if the window did not close at $u_{5}$.
Computing $C_{i}(v)$ in general helps detect those window closings where
$\textrm{Player}\leavevmode\nobreak\ {1}$ cannot continue on as if the window
did not close. If $C_{i}(v)\geq 0$, then even if a window closes along a path
when $v$ is reached, it is safe not to detect it, and we can still construct a
winning strategy if one exists. ∎

######  Construction 4.4.

We construct a Mealy machine $M_{{\sf d}}=(Q_{{\sf
d}},q_{0},V,V\cup\\{\epsilon\\},\Delta_{{\sf d}},\delta_{{\sf d}})$ with
$\ell$ states that defines a winning strategy $\sigma_{{\sf d}}$ of
$\textrm{Player}\leavevmode\nobreak\ {1}$ for the $\mathsf{DirFWMP}(\ell)$
objective, where:

  * •

the memory $Q_{{\sf d}}=\\{1,\ldots,\ell\\}$ stores a counter (modulo $\ell$),
and we assume arithmetic modulo $\ell$ (that is, $\ell+1=1$, $1-1=\ell$,
etc.);

  * •

the initial state is $q_{0}=\ell$ (although we show that an arbitrary initial
state also induces a winning strategy);

  * •

the input alphabet is $V$, as the Mealy machine reads vertices of the game,

  * •

the output alphabet is $V\cup\\{\epsilon\\}$, as the Mealy machine either
outputs a vertex (upon reading a vertex of
$\textrm{Player}\leavevmode\nobreak\ {1}$) or $\epsilon$ (upon reading a
vertex of $\textrm{Player}\leavevmode\nobreak\ {2}$);

  * •

The transition function $\Delta_{{\sf d}}\colon Q_{{\sf d}}\times V\to Q_{{\sf
d}}$ is defined as follows:

$\Delta_{{\sf d}}(i,v)=\begin{cases}i-1\pmod{\ell}&\text{ if }C_{i}(v)\geq
0\quad(\emph{decrement})\\\ \ell-1&\text{ if }C_{i}(v)<0\quad(\emph{reset and
decrement})\\\ \end{cases}$

  * •

The output function $\delta_{{\sf d}}\colon\\{1,\ldots,\ell\\}\times V\to
V\cup\\{\epsilon\\}$ is defined as follows:

$\delta_{{\sf d}}(i,v)=\begin{cases}\epsilon&\text{ if }v\in V_{2}\\\
D_{i}(v)&\text{ if }v\in V_{1}\text{ and }C_{i}(v)\geq 0\\\ D_{\ell}(v)&\text{
if }v\in V_{1}\text{ and }C_{i}(v)<0\\\ \end{cases}$

Note that if $C_{i}(v)<0$, then $\delta_{{\sf d}}(i,v)=\delta_{{\sf
d}}(\ell,v)$, that is, on a reset the strategy plays as if the counter was
equal to $\ell$.

We establish the correctness of the construction as follows. We show that the
strategy $\sigma_{{\sf d}}$ of $\textrm{Player}\leavevmode\nobreak\ {1}$
defined by $M_{{\sf d}}$ is winning, that is for all strategies $\sigma_{2}$
of $\textrm{Player}\leavevmode\nobreak\ {2}$, the outcome $\pi$ of the
strategy profile $(\sigma_{{\sf d}},\sigma_{2})$ satisfies the objective
$\mathsf{DirFWMP}(\ell)$.

We show that every window in $\pi$ closes within at most $\ell$ steps. We
split the outcome $\pi$ into segments (where the last vertex of each segment
is the same as the first vertex of the next segment) such that for each
segment, the state of the Mealy machine is updated to $\ell-1$ upon reading
the last vertex of the segment (thus also upon reading the first vertex of
each segment), but the Mealy machine is never in state $\ell-1$ in between.
Note that the initial memory state of the Mealy machine is $\ell$, thus the
first segment starts at the beginning of the outcome, and the segments cover
the whole outcome. Note also that the length of each segment (i.e., the number
of transitions) is at most $\ell$ since either the memory state is either
updated to $\ell-1$, or decreased by $1$ (modulo $\ell$).

For all segments in the outcome $\pi$, we show that all windows that open in
the segment are closed by (or before) the end of the segment, from which we
can conclude that the objective $\mathsf{DirFWMP}(\ell)$ is satisfied.

Consider a segment $v_{\ell}v_{\ell-1}v_{\ell-2}\cdots v_{p+1}v_{p}$ (where
$p\geq 0$ since each segment has at most $\ell$ transitions), and the sequence
of memory states along the segment:

$q_{\ell}\xrightarrow{v_{\ell}}q_{\ell-1}\xrightarrow{v_{\ell-1}}q_{\ell-2}\
\cdots\ q_{p+1}\xrightarrow{v_{p+1}}q_{p}\xrightarrow{v_{p}}q_{p-1}$

which can be written as:

$x\xrightarrow{v_{\ell}}\ell-1\xrightarrow{v_{\ell-1}}\ell-2\ \cdots\
p+1\xrightarrow{v_{p+1}}y\xrightarrow{v_{p}}\ell-1$

where $q_{\ell-1}=\ell-1$ and $q_{p-1}=\ell-1$ by the definition of segments,
and $q_{i}=i$ for $i=p+1,\ldots,\ell-2$ since the counter is decremented
whenever it is not reset to $\ell-1$ (and thus we also have $C_{i}(v_{i})\geq
0$ for $i=p+1,\ldots,\ell-1$). We discuss the possible values of $q_{p}=y$
(and $q_{\ell}=x$ for which the situation is similar). There are two
possibilities: either $y=\ell$ and the counter is decremented upon reading
$v_{p}$ (and thus $p=0$ and $C_{p}(v_{p})=0$), or $y=p<\ell$ and the counter
is reset upon reading $v_{p}$ (and thus $C_{p}(v_{p})<0$). It follows that in
both cases $C_{p}(v_{p})\leq 0$.

Moreover at the beginning of the segment (considering $q_{\ell}=x$), the
strategy chooses $D_{\ell}(v_{\ell})$ upon reading $v_{\ell}$ (if $v_{\ell}\in
V_{1}$ is a player-1 vertex), as either $x=\ell$ and the output on a decrement
is $D_{x}(v_{\ell})=D_{\ell}(v_{\ell})$, or $x<\ell$ and $C_{x}(v_{\ell})<0$
(and the output on a reset is $D_{\ell}(v_{\ell})$ by definition). Hence we
have $v_{i-1}=D_{i}(v_{i})$ whenever $v_{i}\in V_{1}$ is a player-1 vertex,
for all $i=p+1,\dots,\ell$.

We now show by induction on $i$ that $C_{i}(v_{i})\leq\mathsf{TP}(v_{i}\cdots
v_{p+1}v_{p})$ for all $i\in\\{p+1,\ldots,\ell-1\\}$, which implies, since
$C_{i}(v_{i})\geq 0$, that $\mathsf{TP}(v_{i}\cdots v_{p+1}v_{p})\geq 0$, and
thus all windows in the segment close within $\ell$ steps.

For the base case $i=p+1$, since $C_{p}(v_{p})\leq 0$, the $\max$
subexpression at Line 10 and Line 11 of Algorithm 3 simplifies to
$w(v_{p+1},v_{p})$, and accordingly we get either
$C_{p+1}(v_{p+1})=w(v_{p+1},v_{p})$ if $v_{p+1}\in V_{1}$ is a player-1
vertex, or $C_{p+1}(v_{p+1})\leq w(v_{p+1},v_{p})$ if $v_{p+1}\in V_{2}$ is a
player-2 vertex, which establishes the base case $C_{p+1}(v_{p+1})\leq
w(v_{p+1},v_{p})=\mathsf{TP}(v_{p+1}v_{p})$.

For the induction step, let $i\in\\{p+2,\ldots,\ell-1\\}$. Since
$C_{i-1}(v_{i-1})\geq 0$, we have $C_{i}(v_{i})\leq
w(v_{i},v_{i-1})+C_{i-1}(v_{i-1})$ by a similar argument as in the base case.
By the induction hypothesis, we get $C_{i}(v_{i})\leq
w(v_{i},v_{i-1})+\mathsf{TP}(v_{i-1}\cdots v_{p})=\mathsf{TP}(v_{i}\cdots
v_{p})$.

We show that the result holds no matter which is the initial memory state of
the Mealy machine. It suffices to remark that with initial state $q_{0}=i$
instead of $q_{0}=\ell$, the prefix of the outcome until the first reset
occurs (and the first segment starts) can be considered as a truncated segment
(thus of length at most $i\leq\ell$) where the same argument can be used to
show that all windows close within the length of the segment. ∎

######  Theorem 4.5.

If $\textrm{Player}\leavevmode\nobreak\ {1}$ wins in a non-stochastic game $G$
with objective $\mathsf{FWMP}(\ell)$, then
$\textrm{Player}\leavevmode\nobreak\ {1}$ has a winning strategy with memory
of size $\ell$.

######  Proof 4.6.

Since $\mathsf{FWMP}(\ell)$ is a prefix-independent objective, we have that
the winning region $\langle\\!\langle
1\rangle\\!\rangle^{\mathsf{}}_{G}(\mathsf{FWMP}(\ell))$ of
$\textrm{Player}\leavevmode\nobreak\ {1}$ is a trap for
$\textrm{Player}\leavevmode\nobreak\ {2}$ (Remark 2.1), and induces a subgame,
say $G_{0}$. We construct a winning strategy $\sigma_{1}^{\mathsf{NS}}$ for
$\textrm{Player}\leavevmode\nobreak\ {1}$ in $G_{0}$, with memory of size
$\ell$. Let there be $k+1$ calls to the subroutine NonStocDirFWMP from
Algorithm 1. We denote by $(W_{i})_{i\in\\{1,\dots,k\\}}$ the nonempty $W_{d}$
returned by the $i^{\text{th}}$ call to the subroutine, and let
$A_{i}=\mathsf{Attr}_{1}(W_{i})$. The $A_{i}$’s are pairwise disjoint, and
their union is $\bigcup_{i=1}^{k}A_{i}=\langle\\!\langle
1\rangle\\!\rangle^{\mathsf{}}_{G}(\mathsf{FWMP}(\ell))$. For
$i\in\\{1,\ldots,k\\}$, inductively define $G_{i}$ to be the subgame induced
by the complement of $A_{i}$ in $G_{i-1}$. Since $\mathsf{DirFWMP}(\ell)$ is
closed under suffixes, for all $i\in\\{1,\ldots,k\\}$, we have that $W_{i}$ is
a trap for $\textrm{Player}\leavevmode\nobreak\ {2}$ in $G_{i}$ (Remark 2.1).

Let $W=\bigcup_{i=1}^{k}W_{i}$ be the union of the regions $W_{i}$ over all
subgames $G_{i}$, and let $A=\bigcup_{i=1}^{k}(A_{i}\setminus W_{i})$ be the
union of the regions $A_{i}\setminus W_{i}$ over all subgames $G_{i}$, for
$i\in\\{1,\ldots,k\\}$. Note that $W\cap A=\varnothing$ and $W\cup A=W_{0}$.

We construct a strategy $\sigma_{1}^{\mathsf{NS}}$ that plays according to the
(memoryless) attractor strategy in $A$, and according to the winning strategy
$\sigma_{{\sf d}}$ for $\mathsf{DirFWMP}(\ell)$ objective (defined in the
proof of Lemma 4.1) in $W$. Formally, define the Mealy machine
$M_{1}^{\mathsf{NS}}$ with $\ell$ states that defines
$\sigma_{1}^{\mathsf{NS}}$. The Mealy machine $M_{1}^{\mathsf{NS}}$ is given
by the tuple
$(Q_{1}^{\mathsf{NS}},\ell,V,V\cup\\{\epsilon\\},\Delta_{1}^{\mathsf{NS}},\delta_{1}^{\mathsf{NS}})$,
where

  * •

the memory $Q_{1}^{\mathsf{NS}}=\\{1,\ldots,\ell\\}$ of the Mealy machine
stores a counter (modulo $\ell$);

  * •

the initial state is $q_{0}=\ell$;

  * •

the input alphabet is $V$, as the Mealy machine reads vertices of the game,

  * •

the output alphabet is $V\cup\\{\epsilon\\}$, as the Mealy machine either
outputs a vertex (upon reading a vertex of
$\textrm{Player}\leavevmode\nobreak\ {1}$) or $\epsilon$ (upon reading a
vertex of $\textrm{Player}\leavevmode\nobreak\ {2}$);

  * •

The transition function $\Delta_{1}^{\mathsf{NS}}\colon
Q_{1}^{\mathsf{NS}}\times V\to Q_{1}^{\mathsf{NS}}$ is defined as:

$\Delta_{1}^{\mathsf{NS}}(i,v)=\begin{cases}\ell&\text{ if }v\in
A\,\,\quad(\text{follow attractor strategy})\\\ \Delta_{d}(i,v)&\text{ if
}v\in W\quad(\text{follow $\sigma_{{\sf d}}$ for objective
$\mathsf{DirFWMP}(\ell)$})\\\ \end{cases}$

  * •

The output function $\delta_{1}^{\mathsf{NS}}\colon\\{1,\ldots,\ell\\}\times
V\to V\cup\\{\epsilon\\}$ is defined as follows:

$\delta_{1}^{\mathsf{NS}}(i,v)=\begin{cases}\epsilon&\text{ if }v\in V_{2}\\\
A(v)&\text{ if }v\in A\cap V_{1}\\\ \delta_{d}(i,v)&\text{ if }v\in W\cap
V_{1}\\\ \end{cases}$

We establish the correctness of the construction as follows. We show that the
strategy $\sigma_{1}^{\mathsf{NS}}$ of $\textrm{Player}\leavevmode\nobreak\
{1}$ defined by $M_{1}^{\mathsf{NS}}$ is winning, that is for all strategies
$\sigma_{2}$ of $\textrm{Player}\leavevmode\nobreak\ {2}$, the outcome $\pi$
of the strategy profile $(\sigma_{1}^{\mathsf{NS}},\sigma_{2})$ satisfies the
objective $\mathsf{FWMP}(\ell)$.

The crux is to show that one of the sets $W_{i}$ for some
$i\in\\{1,\ldots,k\\}$ is never left from some point on. Intuitively, given
the token is in $A_{i}$ for some $i\in\\{1,\ldots,k\\}$ (thus in $G_{i}$),
following $\sigma_{1}^{\mathsf{NS}}$ the token will either remain in $A_{i}$,
or leave the subgame $G_{i}$, thus entering $A_{j}$ for a smaller index $j<i$.
Repeating this argument (at most $k$ times, as the index is decreasing) shows
that the token eventually remains in some $W_{i}$ ($i\in\\{1,\ldots,k\\}$).
From that point on, the strategy plays like $\sigma_{{\sf d}}$ (with some
initial memory state $i\in\\{1,\ldots,\ell\\}$) that ensures objective
$\mathsf{DirFWMP}(\ell)$ (proof of Lemma 4.1), and thus from the initial state
the objective $\mathsf{FWMP}(\ell)$ is satisfied.

#### Lower bound on memory requirement for Player 1.

In [9], the authors show an example of game with $\ell=4$ where
$\textrm{Player}\leavevmode\nobreak\ {1}$ requires memory at least 3. While it
is not difficult to generalize this to arbitrary $\ell$, we state it here for
completion.

######  Theorem 4.7.

There exists a family of games $\\{G_{\ell}\\}_{\ell\geq 2}$ with objective
$\mathsf{FWMP}(\ell)$ for $\textrm{Player}\leavevmode\nobreak\ {1}$ such that
every winning strategy of $\textrm{Player}\leavevmode\nobreak\ {1}$ in
$G_{\ell}$ requires at least $\ell-1$ memory.

######  Proof 4.8.

We describe the game $G_{\ell}$ with objective $\mathsf{FWMP}(\ell)$ in Figure
4.

$u_{0}$$u_{1}$$u_{2}$$u_{\ell-2}$$u_{\ell-1}$$v$$-1$$0$$0$$-2$$-(\ell-2)$$-(\ell-1)$$+1$$0$$0$$0$$0$$+2$$0$$0$$0$$0$$0$$+(\ell-1)$$0$

Figure 4: Memory $\ell-1$ is necessary for
$\textrm{Player}\leavevmode\nobreak\ {1}$.

The vertex $u_{0}$ belongs to $\textrm{Player}\leavevmode\nobreak\ {2}$. All
other vertices in the game belong to $\textrm{Player}\leavevmode\nobreak\
{1}$. For each $i\in\\{1,\ldots,\ell\\}$, there is an edge from
$(u_{0},u_{i})$ with payoff $-i$. For all $i\in\\{1,\ldots,\ell-2\\}$, there
is an edge $(u_{i},u_{i+1})$ with payoff $0$. There are $\ell-1$ disjoint
paths from $u_{\ell-1}$ to $v$, each of length $\ell-1$. The $i^{\text{th}}$
edge on the $i^{\text{th}}$ path has payoff $+i$. All other edges in all paths
from $u_{\ell-1}$ to $v$ have payoff $0$. Finally, there is an edge
$(v,u_{0})$ with payoff $0$.

If $\textrm{Player}\leavevmode\nobreak\ {2}$ moves the token from $u_{0}$ to
$u_{i}$ for $i\in\\{1,\ldots,\ell-1\\}$, then
$\textrm{Player}\leavevmode\nobreak\ {1}$ needs to ensure a payoff of at least
$+i$ from $u_{\ell-1}$ in at most $i$ steps to ensure that the window starting
at $u_{0}$ closes in at most $\ell$ steps. When
$\textrm{Player}\leavevmode\nobreak\ {2}$ moves the token from $u_{0}$ to
$u_{i}$, we have that $\textrm{Player}\leavevmode\nobreak\ {1}$ must take the
$i^{\text{th}}$ path from $u_{\ell-1}$ so the window starting at $u_{0}$
closes in at most $\ell$ steps. If $\textrm{Player}\leavevmode\nobreak\ {1}$
chooses any other successor of $u_{\ell-1}$, then the window starting at
$u_{0}$ remains open for more than $\ell$ steps. Since there are $\ell-1$
different choices for $\textrm{Player}\leavevmode\nobreak\ {1}$ from
$u_{\ell-1}$, a Mealy machine defining a winning strategy of
$\textrm{Player}\leavevmode\nobreak\ {1}$ requires at least $\ell-1$ distinct
states. Thus, a winning strategy of $\textrm{Player}\leavevmode\nobreak\ {1}$
in the game $G_{\ell}$ requires at least $\ell-1$ memory.

###  4.2 Memory requirement for Player 2 for FWMP objective

#### Upper bound on memory requirement for Player 2.

Now we show that for $\overline{\mathsf{FWMP}(\ell)}$ objective,
$\textrm{Player}\leavevmode\nobreak\ {2}$ has a winning strategy that requires
at most $|V|\cdot\ell$ memory. This has been loosely stated in [9] without a
formal proof. We use this result to show in Section 6 that the same memory
bound for $\textrm{Player}\leavevmode\nobreak\ {2}$ also suffices in
stochastic games. In fact, we show a stronger result that the memory required
in the stochastic window mean-payoff games is no more than the optimal memory
bounds for non-stochastic games.

######  Theorem 4.9.

Let $G$ be a non-stochastic game with objective
$\overline{\mathsf{FWMP}(\ell)}$ for $\textrm{Player}\leavevmode\nobreak\
{2}$. Then, $\textrm{Player}\leavevmode\nobreak\ {2}$ has a winning strategy
with memory size at most $\lvert V\rvert\cdot\ell$.

######  Proof 4.10.

Since $\mathsf{FWMP}(\ell)$ is a prefix-independent objective, so is
$\overline{\mathsf{FWMP}(\ell)}$. We have that $\langle\\!\langle
2\rangle\\!\rangle^{\mathsf{}}_{G}(\overline{\mathsf{FWMP}(\ell)})$ is a trap
for $\textrm{Player}\leavevmode\nobreak\ {1}$ (Remark 2.1) and induces a
subgame, say $H_{0}$, of $G$. Let there be $k+1$ calls to the subroutine
GoodWin from Algorithm 2, and let $H_{i}$ be the subgame corresponding to the
$i^{\text{th}}$ call of the subroutine. We denote by $(W_{i})_{i=1}^{k}$ the
complement of $W_{gw}$ in $H_{i}$, where $W_{gw}$ is returned by the
$i^{\text{th}}$ call to the subroutine, and let
$A_{i}=\mathsf{Attr}_{2}(W_{i})$. The $A_{i}$’s are pairwise disjoint, and
their union is $\bigcup_{i=1}^{k}A_{i}=\langle\\!\langle
2\rangle\\!\rangle^{\mathsf{}}_{G}(\overline{\mathsf{FWMP}(\ell)})$.

We describe a winning strategy for the $\overline{\mathsf{FWMP}(\ell)}$
objective with memory $k\cdot\ell$, which is at most $\lvert
V\rvert\cdot\ell$. The strategy is always in either attractor mode or window-
open mode. When the game begins, it is in attractor mode. If the strategy is
in attractor mode and the token is on a vertex $v\in A_{i}\setminus W_{i}$ for
some $i\in\\{1,\ldots,k\\}$, then the attractor strategy is to eventually
reach $W_{i}$. If the token reaches $W_{i}$, then the strategy switches to
window-open mode. Since all vertices in $W_{i}$ are winning for
$\textrm{Player}\leavevmode\nobreak\ {2}$ for the
$\overline{\mathsf{GW}(\ell)}$ objective, he can keep the window open for
$\ell$ more steps, provided that $\textrm{Player}\leavevmode\nobreak\ {1}$
does not move the token out of the subgame $H_{i}$. If, at some point,
$\textrm{Player}\leavevmode\nobreak\ {1}$ moves the token out of the subgame
$H_{i}$ to $A_{j}$ for a smaller index $j<i$, then the strategy switches back
to attractor mode, this time trying to reach $W_{j}$ in the bigger subgame
$H_{j}$. Otherwise, if $\textrm{Player}\leavevmode\nobreak\ {2}$ keeps the
window open for $\ell$ steps, then the strategy switches back to attractor
mode until the token reaches a vertex in $\bigcup_{i=1}^{k}W_{i}$. This
strategy can be defined by a Mealy machine $M_{2}^{\mathsf{NS}}$ with states
$\\{1,\ldots,k\\}\times\\{1,\ldots,\ell\\}$, where the first component tracks
the smallest subgame $H_{i}$ in which the window started to remain open, and
the second component indicates how many more steps the window needs to be kept
open for. A formal description of $M_{2}^{\mathsf{NS}}$ is given in
Construction 4.11.

######  Construction 4.11.

Let $W=\bigcup_{i=1}^{k}W_{i}$, and $A=\bigcup_{i=1}^{k}(A_{i}\setminus
W_{i})$. For all $v\in V$, let $\Gamma(v)$ denote the largest $j\geq 1$ such
that $v\in H_{j}$. That is, $H_{\Gamma(v)}$ is the smallest subgame that $v$
belongs to. Given $j\geq 1$ and $v\in A\cap V_{2}\cap(H_{j}\setminus
H_{j+1})$, let $A^{j}(v)$ denote the successor vertex that
$\textrm{Player}\leavevmode\nobreak\ {2}$ must choose to eventually reach the
$W_{j}$ region in $W\cap(H_{j}\setminus H_{j+1})$. This is given by a
memoryless attractor strategy. Given $i\in\\{1,\ldots,\ell\\}$, $j\geq 1$ and
$v\in V_{2}\cap H_{j}$, let $D_{i}^{j}(v)$ denote the best successor that
$\textrm{Player}\leavevmode\nobreak\ {2}$ should choose from $v$ to ensure
that the window remains open for $i$ more steps. These values can be computed
for all $i\in\\{1,\ldots,\ell\\}$ and for all $v\in H_{j}$ by running the
GoodWin algorithm on the subgame $H_{j}$. Recall from Line 11 in Algorithm 3
that $C_{i}(v)=\min_{(v,v^{\prime})\in
E}\\{\max\\{w(v,v^{\prime}),w(v,v^{\prime})+C_{i-1}(v^{\prime})\\}\\}$. We let
$D^{j}_{i}(v)$ be the successor vertex $v^{\prime}\in E(v)$ of $v$ such that
the value of
$\\{\max\\{w(v,v^{\prime}),w(v,v^{\prime})+C_{i-1}(v^{\prime})\\}\\}$ is
minimized. If there is more than one such $v^{\prime}$, we choose one
arbitrarily.

We construct a Mealy machine $M_{2}^{\mathsf{NS}}$ that defines
$\sigma_{2}^{\mathsf{NS}}$, a winning strategy of
$\textrm{Player}\leavevmode\nobreak\ {2}$. The Mealy machine
$M_{2}^{\mathsf{NS}}$ is a tuple
$(Q^{\mathsf{NS}}_{2},(1,\ell),V,V\cup\\{\epsilon\\},\Delta_{2}^{\mathsf{NS}},\delta_{2}^{\mathsf{NS}})$
where

  * •

the set of states $Q_{2}^{\mathsf{NS}}$ is the set
$\\{1,\ldots,k\\}\times\\{1,\ldots,\ell\\}$,

  * •

the initial state of the Mealy machine is $(1,\ell)$ irrespective of where the
game begins in $H_{1}$. We could also instead have set the initial state of
the Mealy machine as $(\Gamma(v_{\mathsf{init}}),\ell)$, where
$v_{\mathsf{init}}$ is the initial vertex of the game. However, to keep the
initial state of the Mealy machine independent of the initial vertex of the
game, we have the initial state of the Mealy machine as $(1,\ell)$. The
transitions are defined such that the state of the Mealy machine is changed to
$\Gamma(v)$ in the very next step.

  * •

the input alphabet is $V$, same as in $M_{1}^{\mathsf{NS}}$,

  * •

the output alphabet is $V\cup\\{\epsilon\\}$, same as in
$M_{1}^{\mathsf{NS}}$.

The transition function $\Delta_{2}^{\mathsf{NS}}\colon
Q_{2}^{\mathsf{NS}}\times V\to Q_{2}^{\mathsf{NS}}$ is defined as follows:

$\Delta_{2}^{\mathsf{NS}}(q,v)=\begin{cases}\Delta_{2}^{\mathsf{NS}}((1,\ell),v)&q=(j,i),v\in
H_{1}\setminus H_{j},\text{for all
}i\in\\{1,\ldots,\ell\\},j\in\\{2,\ldots,k\\}\\\
(\Gamma(v),\ell)&q=(j,\ell),v\in A\cap H_{j},\text{for all
}j\in\\{1,\ldots,k\\}\\\ (\Gamma(v),\ell-1)&q=(j,\ell),v\in W\cap
H_{j},\text{for all }j\in\\{1,\ldots,k\\}\\\ (j,i-1)&q=(j,i),v\in
H_{j},\text{for all }i\in\\{2,\ldots,\ell-1\\},j\in\\{1,\ldots,k\\}\\\
(1,\ell)&q=(j,1),v\in H_{j},\text{for all }j\in\\{1,\ldots,k\\}\\\
\end{cases}$

Suppose the Mealy machine is in state $q\in Q_{2}^{\mathsf{NS}}$ and the token
is in vertex $v\in V$. We describe the definition of
$\Delta_{2}^{\mathsf{NS}}(q,v)$.

  * •

If $q=(j,i)$ for $i\in\\{1,\ldots,\ell\\}$ and $j\in\\{2,\ldots,k\\}$, but
$v\in H_{1}\setminus H_{j}$, then this means that
$\textrm{Player}\leavevmode\nobreak\ {1}$ must have moved the token out of the
subgame $H_{j}$. $\textrm{Player}\leavevmode\nobreak\ {2}$ may have been in
the process of keeping the window open for $\ell$ steps in $H_{j}$, but the
move by $\textrm{Player}\leavevmode\nobreak\ {1}$ may have closed the window.
The strategy switches to attractor mode, and the state of the Mealy machine
changes to $\Delta_{2}^{\mathsf{NS}}((1,\ell),v)$. Note that
$\textrm{Player}\leavevmode\nobreak\ {1}$ can only move the token out of a
subgame finitely many times, and once the token is in $H_{1}\setminus H_{2}$,
then $\textrm{Player}\leavevmode\nobreak\ {1}$ can no longer move the token
out of $H_{1}$, and $\textrm{Player}\leavevmode\nobreak\ {2}$ will be able to
keep the window open for $\ell$ steps without resetting the strategy. Now, for
the remaining cases, suppose that if $q=(j,i)$, then $v\in H_{j}$.

  * •

If $q=(j,\ell)$ for $j\in\\{1,\ldots,k\\}$ and $v\in A\cap H_{j}$, then the
strategy is in attractor mode. Since $v\in H_{j}$, we have that $\Gamma(v)\geq
j$, i.e. $H_{\Gamma(v)}$ is a subgame of $H_{j}$. When the game begins, or
when $\textrm{Player}\leavevmode\nobreak\ {2}$ manages to keep the window open
for $\ell$ steps, the first component resets to 1 according to the fifth type
of transition in the definition of $\Delta_{2}^{\mathsf{NS}}(q,v)$. In such
cases, it may happen that $\Gamma(v)>j$. Another possibility is that, at some
point, the Mealy machine is in state $(j^{\prime},i)$ for
$j^{\prime}\in\\{2,\ldots,k\\}$ and $i\in\\{1,\ldots,\ell\\}$, and the token
is in a vertex $u\in H_{j^{\prime}}$. If $u$ belongs to
$\textrm{Player}\leavevmode\nobreak\ {1}$ and she moves the token from $u$ to
a vertex $u^{\prime}$ that is outside $H_{j^{\prime}}$, then in the next turn,
the first kind of transition of $\Delta_{2}^{\mathsf{NS}}$ occurs, that is,
$\Delta_{2}^{\mathsf{NS}}((1,\ell),u^{\prime})$. In this case, it is possible
that $\Gamma(u^{\prime})>1$. For such scenarios, the first component of the
state of the Mealy machine updates to $\Gamma(v)$ to be an indicator of the
smallest subgame that $v$ belongs to. The second component remains equal to
$\ell$.

  * •

If $q=(j,\ell)$ for $j\in\\{1,\ldots,k\\}$ and $v\in W\cap H_{j}$, then the
strategy was in attractor mode, but switches to window-open mode in this step.
Again, if the game begins, or if $\textrm{Player}\leavevmode\nobreak\ {2}$
manages to keep the window open for $\ell$ steps, or if
$\textrm{Player}\leavevmode\nobreak\ {1}$ moves the token out of a subgame to
a $W$-vertex, it may be the case that $\Gamma(v)>j$. Thus, the first component
of the state of the Mealy machine updates to $\Gamma(v)$ to correctly reflect
the smallest subgame that $\textrm{Player}\leavevmode\nobreak\ {2}$ begins to
keep the window open in. The second component decreases by one, since
$\textrm{Player}\leavevmode\nobreak\ {2}$ has begun to keep the window open
from $v$ and only needs to keep the window open for $\ell-1$ steps after this.

  * •

If $q=(j,i)$ for $j\in\\{1,\ldots,k\\}$ and $i\in\\{2,\ldots,\ell-1\\}$, and
$v\in H_{j}$, then the strategy is in window-open mode. The state of the Mealy
machine changes to $(j,i-1)$. The first component of the state of the Mealy
machine keeps track of the smallest subgame in which
$\textrm{Player}\leavevmode\nobreak\ {2}$ began to keep the window open in
order to decide the optimal successor vertex $D_{i}^{j}(v)$, so it remains
unchanged. The second component decreases to $i-1$, and we now describe why.
If $v$ belongs to $\textrm{Player}\leavevmode\nobreak\ {2}$, and since $H_{j}$
is a trap for $\textrm{Player}\leavevmode\nobreak\ {2}$, the successor
$v^{\prime}$ of $v$ chosen by $\textrm{Player}\leavevmode\nobreak\ {2}$ also
belongs to $H_{j}$, and $\textrm{Player}\leavevmode\nobreak\ {2}$ chooses the
successor that lets him keep the window open for $i-1$ more steps after
$v^{\prime}$. On the other hand, if $v$ belongs to
$\textrm{Player}\leavevmode\nobreak\ {1}$, then the successor $v^{\prime}$ of
$v$ chosen by $\textrm{Player}\leavevmode\nobreak\ {1}$ may or may not belong
to $H_{j}$. If $v^{\prime}$ belongs to $H_{j}$, then
$\textrm{Player}\leavevmode\nobreak\ {2}$ can still keep the window open for
$i-1$ more steps after $v^{\prime}$, since
$\textrm{Player}\leavevmode\nobreak\ {2}$ has been playing optimally for the
objective $\overline{\mathsf{GW}(\ell)}$ restricted to the subgame $H_{j}$.
However, if $\textrm{Player}\leavevmode\nobreak\ {1}$ moves the token out of
$H_{j}$, then the window may have closed, but we let the state of the Mealy
machine change to $(j,i-1)$ regardless. In the next turn, the Mealy machine
will be in state $(j,i-1)$, but $v^{\prime}$ will not belong to $H_{j}$. Thus,
by the first kind of transition of $\Delta_{2}^{\mathsf{NS}}$, after the next
step, the state of the Mealy machine will change to
$\Delta_{2}^{\mathsf{NS}}((1,\ell),v^{\prime})$. The Mealy machine will behave
as if its state had changed to $(1,\ell)$ (instead of $(j,i-1)$) after reading
$v$.

  * •

If $q=(j,1)$ for $j\in\\{1,\ldots,k\\}$ and $v\in H_{j}$, then the strategy is
in window-open mode. After this step, $\textrm{Player}\leavevmode\nobreak\
{2}$ has successfully kept the window open for $\ell$ steps, and the strategy
switches to attractor mode. The second component resets to $\ell$ to indicate
that the strategy switches to attractor mode. The first component of the state
of the Mealy machine resets to 1, the way it was at the beginning of the game.
Since $\Gamma(v)\geq 1$, the first component will correctly change to
$\Gamma(v)$ in the next step by the second or third type of transition in the
definition of $\Delta_{2}^{\mathsf{NS}}(q,v)$.

The output function $\delta_{2}^{\mathsf{NS}}\colon Q_{2}^{\mathsf{NS}}\times
V\to V\cup\\{\epsilon\\}$ is defined as follows:

$\delta_{2}^{\mathsf{NS}}(q,v)=\begin{cases}\epsilon&q\in
Q_{2}^{\mathsf{NS}},v\in V_{1}\\\
\delta_{2}^{\mathsf{NS}}((1,\ell),v)&q=(j,i),v\in V_{2}\cap H_{1}\setminus
H_{j},\text{for all }i\in\\{1,\ldots,\ell\\},j\in\\{2,\ldots,k\\}\\\
A^{\Gamma(v)}(v)&q=(j,\ell),v\in A\cap V_{2}\cap H_{j},\text{for all
}j\in\\{1,\ldots,k\\},\\\ D^{\Gamma(v)}_{\ell}(v)&q=(j,\ell),v\in W\cap
V_{2}\cap H_{j},\text{for all }j\in\\{1,\ldots,k\\},\\\
D_{i}^{j}(v)&q=(j,i),v\in V_{2}\cap H_{j},\text{for all
}i\in\\{1,\ldots,\ell-1\\},j\in\\{1,\ldots,k\\}\\\ \end{cases}$

Suppose the Mealy machine is in state $q\in Q_{2}^{\mathsf{NS}}$ and the token
is in vertex $v\in V$. We describe the definition of
$\delta_{2}^{\mathsf{NS}}(q,v)$.

  * •

If $v\in V_{1}$, then the Mealy machine outputs $\epsilon$ since a strategy of
$\textrm{Player}\leavevmode\nobreak\ {2}$ is not defined for prefixes ending
with a $\textrm{Player}\leavevmode\nobreak\ {1}$ vertex.

  * •

If $q=(j,i)$ for some $i\in\\{1,\ldots,\ell\\}$ and $j\in\\{2,\ldots,k\\}$,
but $v\in H_{1}\setminus H_{j}$, then as described in the definition of the
transition function $\Delta_{2}^{\mathsf{NS}}(q,v)$, this means that
$\textrm{Player}\leavevmode\nobreak\ {1}$ must have moved the token out of the
subgame $H_{j}$ when the last vertex before $v$ was read. The Mealy machine
behaves as if it was in state $(1,\ell)$, and outputs
$\delta_{2}^{\mathsf{NS}}((1,\ell),v)$.

  * •

If $q=(j,\ell)$ and $v\in A\cap V_{2}\cap H_{j}$ for $j\in\\{1,\ldots,k\\}$,
then the strategy is in attractor mode. $\textrm{Player}\leavevmode\nobreak\
{2}$ must move the token by following the attractor strategy to reach
$W_{\Gamma(v)}$. The vertex given by the attractor strategy is
$A^{\Gamma(v)}(v)$.

  * •

If $q=(j,\ell)$ and $v\in W\cap V_{2}\cap H_{j}$ for $j\in\\{1,\ldots,k\\}$,
then the strategy switches to window-open mode.
$\textrm{Player}\leavevmode\nobreak\ {2}$ has not started to keep to window
open, but can now begin to keep the window open for $\ell$ steps. The best
vertex to choose for this is given by the successor $D_{\ell}^{\Gamma(v)}(v)$.

  * •

Finally, if $q=(j,i)$ and $v\in V_{2}\cap H_{j}$ for
$i\in\\{1,\ldots,\ell-1\\}$ and $j\in\\{1,\ldots,k\\}$, then the strategy is
in window-open mode. $\textrm{Player}\leavevmode\nobreak\ {2}$ has kept the
window open for $\ell-i$ steps already, with the first vertex in the window
from $H_{j}\setminus H_{j+1}$. He must keep the window open for $i$ more
steps, and hence chooses $D_{i}^{j}(v)$ as the successor vertex.

This concludes the construction of a Mealy machine defining a winning strategy
of $\textrm{Player}\leavevmode\nobreak\ {2}$. ∎

######  Remark 4.12.

The definitions $\Delta_{2}^{\mathsf{NS}}(q,v)$ and
$\delta_{2}^{\mathsf{NS}}(q,v)$ are recursive definitions when $q=(j,i)$ and
$v\in H_{1}\setminus H_{j}$. Recall that when this is the case, we have
$\Delta_{2}^{\mathsf{NS}}(q,v)=\Delta_{2}^{\mathsf{NS}}((1,\ell),v)$ and
$\delta_{2}^{\mathsf{NS}}(q,v)=\delta_{2}^{\mathsf{NS}}((1,\ell),v)$. The
output and the transition of the Mealy machine $M_{2}^{\mathsf{NS}}$ from the
state $(j,i)$ are as if the Mealy machine is actually in state $(1,\ell)$. If
the Mealy machine is in state $(1,\ell)$, then since $j=1$, and it is not
possible for $v$ to belong to $H_{1}\setminus H_{1}$ because it is an empty
set. Thus, when $j=1$, the transition and output functions do not make
recursive calls to themselves. Hence, the depth of recursion in both
$\Delta_{2}^{\mathsf{NS}}$ and $\delta_{2}^{\mathsf{NS}}$ is never greater
than 1.

######  Remark 4.13.

Note that the memory required for $\textrm{Player}\leavevmode\nobreak\ {2}$ to
play optimally is $k\cdot\ell$, where $k$ is the number of recursive calls to
the GoodWin algorithm. This gives a tighter bound than that claimed in [9]
since $k\leq|V|$.

#### Lower bound on memory requirement for Player 2.

In [9], it was shown that memoryless strategies do not suffice for
$\textrm{Player}\leavevmode\nobreak\ {2}$. We improve upon this lower bound.
Given a window length $\ell\geq 2$, for every $k\geq 1$, we construct a graph
$\\{G_{k,\ell}\\}$ with $2k+\ell-1$ vertices such that every winning strategy
of $\textrm{Player}\leavevmode\nobreak\ {2}$ in $\\{G_{k,\ell}\\}$ requires at
least $k+1$ memory.

######  Theorem 4.14.

There exists a family of non-stochastic games $\\{G_{k,\ell}\\}_{k\geq
1,\ell\geq 2}$ with objective $\mathsf{FWMP}(\ell)$ for
$\textrm{Player}\leavevmode\nobreak\ {1}$ and edge weights $-1,0,+1$ such that
every winning strategy of $\textrm{Player}\leavevmode\nobreak\ {2}$ requires
at least $\frac{1}{2}(\lvert V\rvert-\ell+1)+1$ memory, where $|V|=2k+\ell-1$.

######  Proof 4.15.

Let $A=\\{a_{1},\ldots,a_{k}\\}$, $B=\\{b_{1},\ldots,b_{k}\\}$, and
$C=\\{c_{1},\ldots,c_{\ell-1}\\}$ be pairwise disjoint sets. The vertices of
$G_{k,\ell}$ are $A\cup B\cup C$ with $V_{1}=A\cup C$ and $V_{2}=B$. Now we
list the edges in $G_{k,\ell}$:

  1. 1.

For all $p\in\\{1,\ldots,k\\}$ and $r\in\\{1,\ldots,k\\}$ such that $p\leq r$,
we have an edge $(a_{p},b_{r})$ with payoff $-1$.

  2. 2.

For all $p\in\\{2,\ldots,k\\}$, we have an edge $(a_{p},a_{p-1})$ with payoff
$+1$.

  3. 3.

For all $p\in\\{2,\ldots,k\\}$, we have an edge $(a_{p},b_{p-1})$ with payoff
$+1$.

  4. 4.

For all $p\in\\{1,\ldots,k\\}$, we have an edge $(b_{p},c_{\ell-1})$ with
payoff $0$.

  5. 5.

For all $p\in\\{1,\ldots,k\\}$, we have an edge $(b_{p},a_{p})$ with payoff
$+1$.

  6. 6.

For all $p\in\\{2,\ldots,\ell-1\\}$, we have an edge $(c_{p},c_{p-1})$ with
payoff $0$.

  7. 7.

We have edges $(c_{1},a_{k})$ and $(c_{1},b_{k})$ with payoff $+1$ each.

Figure 5 shows the game $G_{4,3}$.

$a_{1}$$b_{1}$$a_{2}$$b_{2}$$a_{3}$$b_{3}$$a_{4}$$b_{4}$$c_{1}$$c_{2}$

Figure 5: The game $G_{4,3}$ with parameter $k=4$ and window length $\ell=3$.
Red edges have payoff $-1$, black edges have payoff $0$, and blue edges have
payoff $+1$. Memory of size at least $k=4$ is needed to define a winning
strategy for the $\overline{\mathsf{FWMP}(\ell)}$ objective for
$\textrm{Player}\leavevmode\nobreak\ {2}$ in this game.

Observe that the only open windows of length $\ell$ in the game $G_{k,\ell}$
are sequences of the form $a_{p}b_{r}c_{\ell-1}\cdots c_{1}$ for all $p\leq
r$. Also note that $\textrm{Player}\leavevmode\nobreak\ {2}$ has a winning
strategy that wins starting from every vertex in the game:

  * •

If the token is in $C$, then it eventually reaches $c_{1}$. From $c_{1}$, the
token can move to either $a_{k}$ or $b_{k}$. In the latter case,
$\textrm{Player}\leavevmode\nobreak\ {2}$ moves the token from $b_{k}$ to
$a_{k}$. In both cases, the token reaches $A$.

  * •

If the token is in $A$, then it cannot remain in $A$ forever; it must
eventually move to $B$. Moreover, $\textrm{Player}\leavevmode\nobreak\ {2}$
can ensure that the token eventually moves from $A$ to $B$ along an edge with
negative payoff. Suppose whenever the token moves from $A$ to $B$, it moves an
edge with positive payoff, i.e., from $a_{p}\in A$ to $b_{p-1}\in B$ for some
$p\in\\{2,\ldots,k\\}$. Then, $\textrm{Player}\leavevmode\nobreak\ {2}$ moves
the token from $b_{p-1}$ back to $a_{p-1}\in A$. The token then eventually
reaches $a_{1}$ from which all out-edges have negative payoff, and must
necessarily move to $B$ along an edge with negative payoff.

  * •

Eventually, the token moves from $a_{p}$ to $b_{r}$ for some $p\leq r$. In
this case, $\textrm{Player}\leavevmode\nobreak\ {2}$ moves the token from
$b_{r}$ to $c_{\ell-1}$ and eventually to $c_{1}$. The edge $(a_{p},b_{r})$
has a negative payoff and the $\ell-1$ edges on the path from $b_{r}$ to
$c_{1}$ have payoff $0$ each. Hence, the window starting at $a_{p}$ remains
open for $\ell$ steps.

  * •

Now, the token is on $c_{1}$ again and $\textrm{Player}\leavevmode\nobreak\
{2}$ can eventually keep the window open for $\ell$ steps again.

In this manner, $\textrm{Player}\leavevmode\nobreak\ {2}$ can ensure that open
windows of length $\ell$ occur infinitely often in the play.

#### Good choices.

When the token reaches a vertex $b_{r}\in B$,
$\textrm{Player}\leavevmode\nobreak\ {2}$ can either move the token to
$a_{r}\in A$ or to $c_{\ell-1}\in C$. Depending on which vertex the token was
on before reaching $b_{r}$, one of the two choices is _good_ for
$\textrm{Player}\leavevmode\nobreak\ {2}$. If the token reaches $b_{r}$ from
the left or above, i.e., from $a_{p}$ for $p\leq r$, then the edge
$(a_{p},b_{r})$ has negative payoff. In this case, it is good for
$\textrm{Player}\leavevmode\nobreak\ {2}$ to move the token to $c_{\ell-1}\in
C$ so that the window starting at $a_{p}$ remains open for $\ell$ steps.
Otherwise, if the token reaches $b_{r}$ from the right, i.e., from $a_{r+1}$,
then it is good for $\textrm{Player}\leavevmode\nobreak\ {2}$ to move the
token to $a_{r}$ so that an edge with negative payoff may eventually be taken.

For all $u\in A\cup\\{c_{1}\\}$, for all $b_{r}\in B$ such that $(u,b_{r})$ is
an edge in $G_{k,\ell}$, we denote by $\chi(u,b_{r})$ the vertex $a_{r}$ or
$c_{\ell-1}$ that is good for $\textrm{Player}\leavevmode\nobreak\ {2}$. We
list the good choices in the game $G_{4,3}$ in Table 1. The columns are
indexed by $u\in A\cup\\{c_{1}\\}$ and the rows are indexed by $b_{r}\in B$.
If the edge $(u,b_{r})$ does not exist in the game, then the cell
corresponding to this edge is left empty in the table.

$a_{1}b_{1}\to c_{2}$ | $a_{2}b_{1}\to a_{1}$ |  |  |
---|---|---|---|---
$a_{1}b_{2}\to c_{2}$ | $a_{2}b_{2}\to c_{2}$ | $a_{3}b_{2}\to a_{2}$ |  |
$a_{1}b_{3}\to c_{2}$ | $a_{2}b_{3}\to c_{2}$ | $a_{3}b_{3}\to c_{2}$ | $a_{4}b_{3}\to a_{3}$ |
$a_{1}b_{4}\to c_{2}$ | $a_{2}b_{4}\to c_{2}$ | $a_{3}b_{4}\to c_{2}$ | $a_{4}b_{4}\to c_{2}$ | $c_{1}b_{4}\to a_{4}$
Table 1: Good choices $\chi(u,b_{r})$ for all $u\in A\cup\\{c_{1}\\}$ and
$b_{r}\in B$ in the game $G_{4,3}$.

In Lemma 4.16, we show that for each column in the table, there exists a
distinct memory state in every Mealy machine defining a winning strategy of
$\textrm{Player}\leavevmode\nobreak\ {2}$. This gives a lower bound of $k+1$
on the number of states of such a Mealy machine. Since $G_{k,\ell}$ has
$2k+\ell-1$ vertices, the memory requirement of a winning strategy of
$\textrm{Player}\leavevmode\nobreak\ {2}$ is at least $\frac{1}{2}(\lvert
V\rvert-\ell+1)+1$. This concludes the proof of Theorem 4.14.

#### Constructing Mealy machines.

We show that every winning strategy of $\textrm{Player}\leavevmode\nobreak\
{2}$ in $G_{k,\ell}$ requires at least $k$ memory. Let
$\sigma_{2}^{\mathsf{NS}}$ be a winning strategy of
$\textrm{Player}\leavevmode\nobreak\ {2}$ in $G_{k,\ell}$, and let
$M_{2}^{\mathsf{NS}}=(Q_{2}^{\mathsf{NS}},q_{0},V,V\cup\\{\epsilon\\},\Delta_{2}^{\mathsf{NS}},\delta_{2}^{\mathsf{NS}})$
be a Mealy machine defining $\sigma_{2}^{\mathsf{NS}}$.

For all $u\in A\cup\\{c_{1}\\}$, let $Q_{u}$ denote the set of all states that
$M_{2}^{\mathsf{NS}}$ could be in after reading a prefix ending in $u$, i.e.,
$Q_{u}=\\{q\in
Q_{2}^{\mathsf{NS}}\mid\exists\rho\in\mathsf{Prefs}:\hat{\Delta}_{2}^{\mathsf{NS}}(q_{0},\rho\cdot
u)=q\\}$. Lemma 4.16 gives a lower bound on the number of states in
$M_{2}^{\mathsf{NS}}$.

######  Lemma 4.16.

Let $\sigma_{2}^{\mathsf{NS}}$ be a winning strategy for
$\textrm{Player}\leavevmode\nobreak\ {2}$ for the
$\overline{\mathsf{FWMP}(\ell)}$ objective, and let $M_{2}^{\mathsf{NS}}$ be a
Mealy machine defining $\sigma_{2}^{\mathsf{NS}}$. Then, for all vertices
$u\in A\cup\\{c_{1}\\}$, there exists a state $q_{u}\in Q_{u}$ such that for
all $b_{r}\in B\cap E(u)$, we have that
$\delta_{2}^{\mathsf{NS}}(q_{u},b_{r})=\chi(u,b_{r})$. Moreover, the Mealy
machine $M_{2}^{\mathsf{NS}}$ has $k+1$ distinct states.

######  Proof 4.17.

We prove the contrapositive. Suppose there exists a vertex $u\in
A\cup\\{c_{1}\\}$ such that for all $q_{u}\in Q_{u}$, there exists a vertex
$b_{r}\in B\cap E(u)$ such that
$\delta_{2}^{\mathsf{NS}}(q_{u},b_{r})\neq\chi(u,b_{r})$. Then, we show that
$\sigma_{2}^{\mathsf{NS}}$ is not winning for
$\textrm{Player}\leavevmode\nobreak\ {2}$. We show this by constructing a
strategy $\sigma_{1}$ of $\textrm{Player}\leavevmode\nobreak\ {1}$ such that
the outcome $(\sigma_{1},\sigma_{2}^{\mathsf{NS}})$ satisfies
$\mathsf{FWMP}(\ell)$ and is thus losing for
$\textrm{Player}\leavevmode\nobreak\ {2}$. We have that either $u\in A$ or
$u=c_{1}$.

  * •

Suppose $u=c_{1}$.
Irrespective of which vertex the game begins from, the strategy $\sigma_{1}$
tries to eventually move the token to $c_{1}$. If the token never reaches
$c_{1}$, then this implies that the token never reaches $c_{\ell-1}$, and
therefore, this implies that every time the token reaches $B$,
$\textrm{Player}\leavevmode\nobreak\ {1}$ moves it to $A$ and not $C$. Thus,
no windows remain open for $\ell$ steps. Otherwise, the token eventually
reaches $c_{1}$ after having seen at most one open window of length $\ell$.
After the token reaches $c_{1}$ for the first time, we show that under the
assumption that for all $q_{c_{1}}\in Q_{c_{1}}$, there exists a vertex
$b_{r}\in B\cap E(c_{1})$ such that
$\delta_{2}^{\mathsf{NS}}(q_{c_{1}},b_{r})\neq\chi(c_{1},b_{r})$, that
subsequently there are no more open windows of size $\ell$ in the outcome.

To see this, observe that $B\cap E(c_{1})=\\{b_{k}\\}$ and
$\chi(c_{1},b_{k})=a_{k}$. Since for all $q_{c_{1}}\in Q_{c_{1}}$ we have that
$\delta_{2}^{\mathsf{NS}}(q_{c_{1}},b_{k})\neq\chi(c_{1},b_{k})$, we have that
$\delta_{2}^{\mathsf{NS}}(q_{c_{1}},b_{k})=c_{\ell-1}$. That is, each time the
token reaches $b_{k}$ from $c_{1}$, the strategy $\sigma_{2}^{\mathsf{NS}}$
moves the token to $c_{\ell-1}$. Hence, the token is stuck in the cycle
$(b_{k}c_{\ell-1}\cdots c_{1})$ where every edge has nonnegative payoff, and
no windows open.

  * •

Otherwise, suppose $u=a_{j}\in A$ for some $j\in\\{1,\ldots,k\\}$.
Irrespective of which vertex the game begins from, the strategy $\sigma_{1}$
eventually moves the token to $a_{j}$ encountering at most one open window of
length $\ell$. Under the assumption in the contrapositive statement, we have
that each time the token reaches $a_{j}$, there exists a successor $b_{r}$ of
$a_{j}$ such that $\sigma_{2}^{\mathsf{NS}}$ does not play according to
$\chi(u,b_{r})$ from $b_{r}$. Specifically, at least one of the following
hold:

    * –

If $\sigma_{1}$ moves the token from $a_{j}$ to $b_{j-1}$, then
$\sigma_{2}^{\mathsf{NS}}$ moves the token from $b_{j-1}$ to $c_{\ell-1}$.

    * –

There exists $r\geq j$ such that if $\sigma_{1}$ moves the token from $a_{j}$
to $b_{r}$, then $\sigma_{2}^{\mathsf{NS}}$ moves the token from $b_{r}$ to
$a_{r}$.

To see this, suppose that when the token reaches $a_{j}$, the state of the
Mealy machine $M_{2}^{\mathsf{NS}}$ becomes $q^{\prime}$. When the token moves
from $a_{j}$ to a successor of $a_{j}$, suppose that the state of
$M_{2}^{\mathsf{NS}}$ becomes $q\in Q_{a_{j}}$, i.e., we have that
$\delta_{2}^{\mathsf{NS}}(q^{\prime},a_{j})=q$. Now, there exists $b_{r}\in
B\cap E(a_{j})$ such that
$\delta_{2}^{\mathsf{NS}}(q,b_{r})\neq\chi(a_{j},b_{r})$. Recall that $B\cap
E(a_{j})=\\{b_{j-1},b_{j},\ldots,b_{k}\\}$, and that
$\chi(a_{j},b_{j-1})=a_{j-1}$, and $\chi(a_{j},b_{r})=c_{\ell-1}$ for all
$r\geq j$. Therefore, we have that at least one of the following holds:
$\delta_{2}^{\mathsf{NS}}(q,b_{j-1})\neq a_{j-1}$ or there exists $r\geq j$
such that $\delta_{2}^{\mathsf{NS}}(q,b_{r})\neq c_{\ell-1}$. Equivalently, at
least one of the following holds:
$\delta_{2}^{\mathsf{NS}}(q,b_{j-1})=c_{\ell-1}$ or there exists $r\geq j$
such that $\delta_{2}^{\mathsf{NS}}(q,b_{r})=a_{r}$.

In the first case, the window does not open at $a_{j}$. When the token reaches
$c_{\ell-1}$, the strategy $\sigma_{1}$ eventually moves the token back to
$a_{j}$ without opening any new windows. In the second case, since the edge
$(a_{j},b_{r})$ has payoff $-1$, a window opens at $a_{j}$. However, since the
edge $(b_{r},a_{r})$ has payoff $+1$, this window closes in the next step and
does not remain open for $\ell$ steps. The strategy $\sigma_{1}$ eventually
moves the token back to $a_{j}$ along vertices in $A$.

Therefore, each time the token reaches $a_{j}$, the strategy $\sigma_{1}$
moves the token to a successor $b_{r}$ of $a_{j}$ from which
$\sigma_{2}^{\mathsf{NS}}$ does not play according to $\chi(a_{j},b_{r})$.
This way there are subsequently no open windows of length $\ell$ in the
outcome.

This completes the proof of the contrapositive. We now show that such a Mealy
machine $M_{2}^{\mathsf{NS}}$ has at least $k+1$ distinct states. For all
$u\in A\cup\\{c_{1}\\}$, let $q_{u}$ denote a state in $Q_{u}$ that plays in
accordance with the good choices, i.e., for all $b_{r}\in B\cap E(u)$, we have
that $\delta_{2}^{\mathsf{NS}}(q_{u},b_{r})=\chi(u,b_{r})$. Then, for all
$i,j$ such that $0\leq i<j<k$, we have that $q_{a_{i}}$ and $q_{a_{j}}$ are
distinct states since $\delta_{2}^{\mathsf{NS}}(q_{a_{i}},b_{j-1})=c_{\ell-1}$
but $\delta_{2}^{\mathsf{NS}}(q_{a_{j}},b_{j-1})=a_{j-1}$. This gives $k$
distinct states in $M_{2}^{\mathsf{NS}}$. In addition to this, since
$\delta_{2}^{\mathsf{NS}}(q_{c_{1}},b_{k})=a_{k}$ but
$\delta_{2}^{\mathsf{NS}}(q_{a_{j}},b_{k})=c_{\ell-1}$ for all
$j\in\\{1,\ldots,k\\}$, we have that $q_{c_{1}}$ is distinct from each of the
$k$ distinct states found before. Thus $M_{2}^{\mathsf{NS}}$ has at least
$k+1$ distinct states.

Given a winning strategy $\sigma_{2}^{\mathsf{NS}}$ of
$\textrm{Player}\leavevmode\nobreak\ {2}$ for the
$\overline{\mathsf{FWMP}(\ell)}$ objective, the following lemma gives an upper
bound on the number of steps between consecutive open windows of length $\ell$
in any play consistent with $\sigma_{2}^{\mathsf{NS}}$. This lemma is used in
Section 6, where we construct an almost-sure winning strategy of
$\textrm{Player}\leavevmode\nobreak\ {2}$ for the
$\overline{\mathsf{FWMP}(\ell)}$ objective.

######  Lemma 4.18.

Let $G$ be a non-stochastic game such that all vertices in $G$ are winning for
$\textrm{Player}\leavevmode\nobreak\ {2}$, that is, $\langle\\!\langle
2\rangle\\!\rangle^{\mathsf{}}_{G}(\overline{\mathsf{FWMP}(\ell)})=V$. Let
$\sigma_{2}^{\mathsf{NS}}$ be a finite-memory strategy of
$\textrm{Player}\leavevmode\nobreak\ {2}$ of memory size $\mathsf{M}$ that is
winning for $\overline{\mathsf{FWMP}(\ell)}$ from all vertices in $G$. Then,
for every play $\pi$ of $G$ consistent with $\sigma_{2}^{\mathsf{NS}}$, every
infix of $\pi$ of length $\mathsf{M}\cdot\lvert V\rvert\cdot\ell$ contains an
open window of length $\ell$.

######  Proof 4.19.

Since $\sigma_{2}^{\mathsf{NS}}$ has memory of size $\mathsf{M}$, fixing this
strategy in $G$ gives a one-player game $G^{\sigma_{2}^{\mathsf{NS}}}$ with
$\mathsf{M}\cdot\lvert V\rvert$ vertices. Then, the claim is that every path
of length $\mathsf{M}\cdot\lvert V\rvert\cdot\ell$ in
$G^{\sigma_{2}^{\mathsf{NS}}}$ contains an open window of length $\ell$.
Suppose towards a contradiction that there exists a path of length
$\mathsf{M}\cdot\lvert V\rvert\cdot\ell$ in the one-player game that does not
contain an open window of length $\ell$. Since every window is closed in no
more than $\ell$ steps, and the window is closed at the initial vertex to
begin with, there are at least $\mathsf{M}\cdot\lvert V\rvert+1$ vertices in
this path where a window closes. Since there are only $\mathsf{M}\cdot\lvert
V\rvert$ vertices in $G^{\sigma_{2}^{\mathsf{NS}}}$, by the pigeonhole
principle, there exists a vertex $u$ that is visited twice in this path, both
times with the window closed. Thus, the path contains a cycle without open
windows of length $\ell$. Since $\textrm{Player}\leavevmode\nobreak\ {1}$ can
reach this cycle and loop in it forever, it gives an outcome that is winning
for $\textrm{Player}\leavevmode\nobreak\ {1}$ in $G$, which is a
contradiction.

##  5 Reducing stochastic games to non-stochastic games

In this section, we recall a sufficient condition that allows to solve
stochastic games by solving, as a subroutine, a non-stochastic game with the
same objective. The sufficient condition was presented in [14] for solving
finitary Streett objectives and can be generalized to arbitrary prefix-
independent objectives. Under this condition, the qualitative problems for
stochastic games can be solved as efficiently (up to a factor of $\lvert
V\rvert^{2}$) as non-stochastic games with the same objective. Also, it
follows that the memory requirement for $\textrm{Player}\leavevmode\nobreak\
{1}$ to play optimally in stochastic games is the same as in non-stochastic
games with the same objective.

We now describe the sufficient condition that we call the sure-almost-sure
property. Given a stochastic game $\mathcal{G}$, let
$\mathcal{G}_{\mathsf{NS}}=((V,E),(V_{1},V_{2}\cup
V_{\Diamond},\varnothing),w)$ be the _(adversarial) non-stochastic game
corresponding to $\mathcal{G}$_, obtained by changing all probabilistic
vertices to $\text{Player\leavevmode\nobreak\ }2$ vertices. We omit the
probability function in the tuple since there are no more probabilistic
vertices.

######  Definition 5.1 (Sure-almost-sure ($\mathsf{SAS}$) property).

A prefix-independent objective $\varphi$ in a game $\mathcal{G}$ satisfies the
$\mathsf{SAS}$ property if $\langle\\!\langle
2\rangle\\!\rangle^{\mathsf{}}_{\mathcal{G}_{\mathsf{NS}}}(\overline{\varphi})=V$
implies $\langle\\!\langle
2\rangle\\!\rangle^{\mathsf{AS}}_{\mathcal{G}}(\overline{\varphi})=V$, that
is, if $\textrm{Player}\leavevmode\nobreak\ {2}$ wins the objective
$\overline{\varphi}$ from every vertex in $\mathcal{G}_{\mathsf{NS}}$, then
$\textrm{Player}\leavevmode\nobreak\ {2}$ almost-surely wins the same
objective $\overline{\varphi}$ from every vertex in $\mathcal{G}$.

The definition of the $\mathsf{SAS}$ property implies that if there exists a
vertex from which $\textrm{Player}\leavevmode\nobreak\ {1}$ wins the objective
$\varphi$ positively in the stochastic game $\mathcal{G}$, then there exists a
vertex from which $\textrm{Player}\leavevmode\nobreak\ {1}$ wins the same
objective $\varphi$ in the non-stochastic game $\mathcal{G}_{\mathsf{NS}}$.
Note that every prefix-independent objective satisfies the converse of the
$\mathsf{SAS}$ property since if $\textrm{Player}\leavevmode\nobreak\ {2}$
even wins positively from all vertices in $\mathcal{G}$, then since he
controls all probabilistic vertices in $\mathcal{G}_{\mathsf{NS}}$, he wins
from all vertices in $\mathcal{G}_{\mathsf{NS}}$ by choosing optimal
successors of probabilistic vertices.

We show in Section 6 that for all stochastic games $\mathcal{G}$, the
objectives $\mathsf{FWMP}_{\mathcal{G}}(\ell)$ and
$\mathsf{BWMP}_{\mathcal{G}}$ satisfy the $\mathsf{SAS}$ property. Now, we
present an example of objective that _does not_ satisfy the $\mathsf{SAS}$
property. Consider the example in Figure 6. The objective $\varphi$ in this
game is a Büchi objective: a play $\pi$ satisfies the Büchi objective if $\pi$
visits vertex ${v}_{1}$ infinitely often. Although from every vertex, with
positive probability (in fact, with probability $1$), a play visits ${v}_{1}$
infinitely often, from none of the vertices,
$\textrm{Player}\leavevmode\nobreak\ {1}$ can ensure the Büchi objective in
the non-stochastic game $\mathcal{G}_{\mathsf{NS}}$.

$v_{1}$$v_{2}$$v_{3}$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}.5}$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}.5}$
Figure 6: Büchi objective does not satisfy the $\mathsf{SAS}$ property in this
game.

The following theorem states that if an objective $\varphi$ satisfies the
$\mathsf{SAS}$ property, then solving the positive (resp., almost-sure)
satisfaction problem can be done within a linear (resp., quadratic) factor of
the time needed to solve non-stochastic games with the same objective.

######  Theorem 5.2.

Given $\mathcal{G}$ and $\varphi$, suppose in every subgame
$\mathcal{G}^{\prime}$ of $\mathcal{G}$, the objective $\varphi$ restricted to
$\mathcal{G}^{\prime}$ satisfies the $\mathsf{SAS}$ property. Let
$\textup{{NonStocWin}}_{\varphi}(\mathcal{G}_{\mathsf{NS}})$ be an algorithm
computing $\langle\\!\langle
1\rangle\\!\rangle^{\mathsf{}}_{\mathcal{G}_{\mathsf{NS}}}(\varphi)$ in
$\mathcal{G}_{\mathsf{NS}}$ in time $\mathbb{C}$. Then, the positive and
almost-sure satisfaction of $\varphi$ can be decided in time
$\mathcal{O}(\lvert V\rvert\cdot(\mathbb{C}+\lvert E\rvert))$ and
$\mathcal{O}(\lvert V\rvert^{2}\cdot(\mathbb{C}+\lvert E\rvert))$
respectively.

Moreover, for positive and almost-sure satisfaction of $\varphi$, the memory
requirement for $\textrm{Player}\leavevmode\nobreak\ {1}$ to play optimally in
stochastic games is no more than that for non-stochastic games.

Theorem 5.2 does not give bounds on memory requirement for winning
$\textrm{Player}\leavevmode\nobreak\ {2}$ strategies for objective $\varphi$
in the stochastic game, but we provide such bounds specifically for
$\mathsf{FWMP}(\ell)$ and $\mathsf{BWMP}$ in Section 6. The proof of the
theorem appears shortly after Corollary 5.3.

Finally, we look at the quantitative decision problem. The quantitative
satisfaction for $\varphi$ can be decided in $\mathsf{NP}^{B}$ ([14, Theorem
6]), where $B$ is an oracle deciding positive and almost-sure satisfaction
problems for $\varphi$. It is not difficult to see that the quantitative
satisfaction for $\varphi$ can be decided in
$\mathsf{NP}^{B}\cap\mathsf{coNP}^{B}$. Moreover, from the proof of [14,
Theorem 6], it follows that the memory requirement of winning strategies for
both players for the quantitative decision problem is no greater than that for
the qualitative decision problem.

As stated in [14, Definition 2], the vertices of a stochastic game can be
partitioned into classes from which $\textrm{Player}\leavevmode\nobreak\ {1}$
wins $\varphi$ with the same maximal probability. From [14, Lemma 7], a
strategy of $\textrm{Player}\leavevmode\nobreak\ {1}$ that is almost-sure
winning in every class for the objective $\varphi\cup\mathsf{Reach}(Z)$ for
some suitable subset $Z$ of the class is a winning strategy of
$\textrm{Player}\leavevmode\nobreak\ {1}$ for the quantitative satisfaction of
$\varphi$. Analogously, a strategy of $\textrm{Player}\leavevmode\nobreak\
{2}$ that is positive winning in every class for objective
$\overline{\varphi}\cap\mathsf{Safe}(\overline{Z})$, where $\overline{Z}$ is
the complement of $Z$ in the class, is a winning strategy for
$\textrm{Player}\leavevmode\nobreak\ {2}$. Thus, the memory requirement of
winning strategies for both players for the quantitative decision problem is
no greater than that for the qualitative decision problem.

######  Corollary 5.3.

Given $\mathcal{G}$ and $\varphi$ as described in Theorem 5.2, let $B$ be an
oracle deciding the qualitative satisfaction of $\varphi$. Then, the
quantitative satisfaction of $\varphi$ is in
$\mathsf{NP}^{B}\cap\mathsf{coNP}^{B}$. Moreover, the memory requirement of
optimal strategies for both players is no greater than that for the positive
and almost-sure satisfaction of $\varphi$.

Now, we describe an algorithm $\textup{{PosWin}}_{\varphi}$ to compute the
positive winning region of $\textrm{Player}\leavevmode\nobreak\ {1}$ in
$\mathcal{G}$ with objective $\varphi$. The algorithm uses
$\textup{{NonStocWin}}_{\varphi}$ as a subroutine. Then, we describe an