School of Informatics, University of Edinburgh, UK School of Informatics,
University of Edinburgh, UK Mohan Dantam and Richard Mayr Computing
methodologies Stochastic games Full version of a paper presented at MFCS 2023.
Jérôme Leroux, Sylvain Lombardy, and David Peleg 3 48th International
Symposium on Mathematical Foundations of Computer Science (MFCS 2023) MFCS
2023 MFCS 2023 August 28 to September 1, 2023 Bordeaux, France 272 36

# Approximating the Value of Energy-Parity Objectives in Simple Stochastic
Games

Mohan Dantam  Richard Mayr

###### Abstract

We consider simple stochastic games ${\mathcal{G}}$ with energy-parity
objectives, a combination of quantitative rewards with a qualitative parity
condition. The Maximizer tries to avoid running out of energy while
simultaneously satisfying a parity condition.

We present an algorithm to approximate the value of a given configuration in
2-$\mathsf{NEXPTIME}$. Moreover, $\varepsilon$-optimal strategies for either
player require at most
${\mathcal{O}}\left(2\textrm{-}\mathsf{EXP}\left(\lvert{\mathcal{G}}\rvert\right)\cdot\log\left(\frac{1}{\varepsilon}\right)\right)$
memory modes.

###### keywords:

Energy-Parity Games, Simple Stochastic Games, Parity, Energy

##  1 Introduction

Background. _Simple stochastic games_ (SSGs) are 2-player turn-based perfect
information stochastic games played on finite graphs. They are also called
_competitive Markov decision processes_ [20], or _$2\frac{1}{2}$ -player
games_ [13, 12]. Introduced by Shapley [36] in 1953, they have since played a
central role in the solution of many problems, e.g., synthesis of reactive
systems [35, 34] and formal specification and verification [17, 18, 1]. Every
state either belongs to one of the players (Maximizer or Minimizer) or is a
random state. In each round of the game the player who owns the current state
gets to choose the successor state along the game graph. For random states the
successor is chosen according to a predefined distribution. Given a start
state and strategies of Maximizer and Minimizer, this yields a distribution
over induced infinite plays. We consider objectives $\mathtt{O}$ that are
measurable subsets of the set of possible plays, and the players try to
maximize (resp. minimize) the probability of $\mathtt{O}$.

Many different objectives for SSGs have been studied in the literature. Here
we focus on parity, mean-payoff and energy objectives. We assign numeric
rewards to transitions and priorities (aka colors), encoded by bounded non-
negative numbers, to states. A play satisfies the (min-even) parity objective
iff the minimal priority that appears infinitely often in a play is even. It
subsumes all $\omega$-regular objectives, and in particular safety, liveness,
fairness, etc. On finite SSGs, the parity objective can be seen as a special
case of the mean-payoff objective which requires the limit average reward per
transition along a play to be positive (or non-negative). Mean-payoff
objectives in SSGs go back to a 1957 paper by Gillette [21] and have been
widely studied, due to their relevance for efficient control. The energy
objective [6] requires that the accumulated reward at any time in a play stays
above some finite threshold. The intuition is that a controlled system has
some finite initial energy level that must never become depleted. Since the
accumulated reward is not bounded a-priori, this essentially turns a finite-
state game into an infinite-state one.

Energy-parity. We consider SSGs with _energy-parity_ objectives, where plays
need to satisfy both an energy and a parity objective. The parity objective
specifies functional correctness, while the energy condition can encode
efficiency or risk considerations, e.g., the system should not run out of
energy since manually recharging would be costly or risky.

Previous work. Much work on combined objectives for stochastic systems is
restricted to Markov decision processes (MDPs) [8, 9, 4, 28].

For (stochastic) games, the computational complexity of single objectives is
often in $\mathsf{NP}\cap\mathsf{coNP}$, e.g., for parity or mean-payoff
objectives [25]. Multi-objective games can be harder, e.g., satisfying _two
different_ parity objectives leads to $\mathsf{coNP}$ completeness [11].

Stochastic mean-payoff parity games can be solved in
$\mathsf{NP}\cap\mathsf{coNP}$ [10]. However, this does not imply a solution
for stochastic energy-parity games, since, unlike in the non-stochastic case
[7], there is no known reduction from energy-parity to mean-payoff parity in
stochastic games. The reduction in [7] relies on the fact that Maximizer has a
winning _finite-memory_ strategy for energy-parity, which does not generally
hold for stochastic games, or even MDPs [28]. For the same reason, the direct
reduction from stochastic energy-parity to ordinary energy games proposed in
[8, 9] does not work for general energy-parity but only for energy-Büchi; cf.
[28].

Non-stochastic energy-parity games can be solved in
$\mathsf{NP}\cap\mathsf{coNP}$ (and even in pseudo-quasi-polynomial time [16])
and Maximizer strategies require only finite (but exponential) memory [7].

Stochastic energy-parity games have been studied in [29], where it was shown
that the almost-sure problem is decidable and in
$\mathsf{NP}\cap\mathsf{coNP}$. That is, given an initial configuration
(control-state plus current energy level), does Maximizer have a strategy to
ensure that energy-parity is satisfied with probability $1$ against any
Minimizer strategy? Unlike in many single-objective games, such an almost-
surely winning Maximizer strategy (if it exists) requires infinite memory in
general. This holds even in MDPs and for energy-coBüchi objectives [28].

However, [29] did not address quantitative questions about energy-parity
objectives, such as computing/approximating the value of a given
configuration, or the decidability of exact questions like “Is the value of
this configuration $\geq k$ ?” for some constant $k$ (e.g., $k=1/2$).

The decidability of the latter type of exact question about the energy-parity
value is open, but there are strong indications that it is very hard. In fact,
even simpler subproblems are already at least as hard as the _positivity
problem for linear recurrence sequences_ , which in turn is at least as hard
as the _Skolem problem_ [19]. (The decidability of these problems has been
open for decades; see [30] for an overview.) Given an SSG with an energy-
parity objective, suppose we remove the parity condition (assume it is always
true) and also suppose that Maximizer is passive (does not get to make any
decisions). Then we obtain an MDP where the only active player (the Minimizer
in the SSG) has a _termination objective_ , i.e., to reach a configuration
where the energy level is $\leq 0$. Exact questions about the value of the
termination objective in MDPs are already at least as hard as the positivity
problem [31, Section 5.2.3] (see also [32, 33]). Thus exact questions about
the energy-parity value in SSGs are also at least as hard as the positivity
problem.

Our contributions. Since exact questions about the energy-parity value in SSGs
are positivity-hard, we consider the problem of computing approximations of
the value. We present an algorithm that, given an SSG ${\mathcal{G}}$ and
error $\varepsilon$, computes $\varepsilon$-close approximations of the
energy-parity value of any given configuration in 2-$\mathsf{NEXPTIME}$.
Moreover, we show that $\varepsilon$-optimal Maximizer (resp. Minimizer)
strategies can be chosen as deterministic and using only finite memory with
${\mathcal{O}}\left(2\textrm{-}\mathsf{EXP}\left(\lvert{\mathcal{G}}\rvert\right)\cdot\log\left(\frac{1}{\varepsilon}\right)\right)$
memory modes. One can understand the idea as a constructive upper bound on the
accuracy with which the players need to remember the current energy level in
the game. (This is in contrast to the result in [28] that almost-surely
winning Maximizer strategies require infinite memory in general.) Once the
upper bound on Maximizer’s memory for $\varepsilon$-optimal strategies is
established, one might attempt a reduction from energy-parity to mean-payoff
parity, along similar lines as for non-stochastic games in [7]. However,
instead we use a more direct reduction from energy-parity to parity in a
derived SSG for our approximation algorithm.

##  2 Preliminaries

A probability distribution over a countable set $S$ is a function
$f:S\to[0,1]$ with $\sum_{s\in S}f(s)=1$. ${\sf
supp}(f)\stackrel{{\scriptstyle\text{{\tiny{def}}}}}{{=}}$
$\\{{s}|\;{f(s)>0}\\}$ denotes the support of $f$ and $\mathcal{D}(S)$ is the
set of all probability distributions over $S$. Given an alphabet $\Sigma$, let
$\Sigma^{\omega}$ and $\Sigma^{*}$ ($\Sigma^{+}$) denote the set of infinite
and finite (non-empty) sequences over $\Sigma$, respectively. Elements of
$\Sigma^{\omega}$ or $\Sigma^{*}$ are called words.

Games, MDPs and Markov chains. A _Simple Stochastic Game_ (SSG) is a finite-
state 2-player turn-based perfect-information stochastic game
${\mathcal{G}}=\left(S,(S_{\Box},S_{\Diamond},S_{\ocircle}),{E},P\right)$
where the finite set of states $S$ is partitioned into the states $S_{\Box}$
of the player $\Box$ (_Maximizer_), states $S_{\Diamond}$ of player $\Diamond$
(_Minimizer_), and chance vertices (aka random states) $S_{\ocircle}$. Let
${E}\subseteq S\times S$ be the transition relation. We write
$s{\longrightarrow}s^{\prime}$ if $\left(s,s^{\prime}\right)\in{E}$ and assume
that
$\mathsf{Succ}({s})\stackrel{{\scriptstyle\text{{\tiny{def}}}}}{{=}}\\{s^{\prime}\mid
s{E}{}s^{\prime}\\}\neq\emptyset$ for every state $s$. The _probability
function_ $P$ assigns each random state $s\in S_{\ocircle}$ a distribution
over its successor states, i.e., $P(s)\in\mathcal{D}(\mathsf{Succ}({s}))$. For
ease of presentation, we extend the domain of $P$ to $S^{*}S_{\ocircle}$ by
$P(\rho s)\stackrel{{\scriptstyle\text{{\tiny{def}}}}}{{=}}P(s)$ for all $\rho
s\in S^{+}S_{\ocircle}$. An _MDP_ is a game where one of the two players does
not control any states. An MDP is _maximizing_ (resp.  _minimizing_) iff
$S_{\Diamond}=\emptyset$ (resp. $S_{\Box}=\emptyset$). A _Markov chain_ is a
game with only random states, i.e., $S_{\Box}=S_{\Diamond}=\emptyset$.

Strategies. A play is an infinite sequence $s_{0}s_{1}\ldots\in S^{\omega}$
such that $s_{i}{\longrightarrow}s_{i+1}$ for all $i\geq 0$. A path is a
finite prefix of a play. Let ${\it
Plays}\left({\mathcal{G}}\right)\stackrel{{\scriptstyle\text{{\tiny{def}}}}}{{=}}\left\\{\rho=\left(q_{i}\right)_{i\in\mathbb{N}}\,|q_{i}{\longrightarrow}q_{i+1}\right\\}$
denote the set of all possible plays. A strategy of the player $\Box$
($\Diamond$) is a function $\sigma:S^{*}S_{\Box}\to\mathcal{D}(S)$
($\pi:S^{*}S_{\Diamond}\to\mathcal{D}(S)$) that assigns to every path $ws\in
S^{*}S_{\Box}$ ($\in S^{*}S_{\Diamond}$) a probability distribution over the
successors of $s$. If these distributions are always Dirac then the strategy
is called _deterministic_ (aka pure), otherwise it is called _randomized_ (aka
mixed). The set of all strategies of player $\Box$ and $\Diamond$ in
${\mathcal{G}}$ is denoted by $\Sigma_{{{\mathcal{G}}}}$ and
$\Pi_{{{\mathcal{G}}}}$, respectively. A play/path $s_{0}s_{1}\ldots$ is
compatible with a pair of strategies $(\sigma,\pi)$ if $s_{i+1}\in{\sf
supp}(\sigma(s_{0}\ldots s_{i}))$ whenever $s_{i}\in S_{\Box}$ and
$s_{i+1}\in{\sf supp}(\pi(s_{0}\ldots s_{i}))$ whenever $s_{i}\in
S_{\Diamond}$.

Finite-memory deterministic (FD) strategies are a subclass of strategies
described by deterministic transducers ${\sf T}=\left({\sf M},{\sf m}_{0},{\sf
upd},{\sf nxt}\right)$ where ${\sf M}$ is a finite set of memory modes with
initial mode ${\sf m}_{0}$, ${\sf upd}:{\sf M}\times{E}\mapsto{\sf M}$ updates
the memory mode upon observing a transition and ${\sf nxt}:{\sf M}\times
S_{\odot}\mapsto S$ chooses the successor state based on the current memory
mode and state. FD strategies without memory ($|{\sf M}|=1$) are called
memoryless deterministic (MD). For deterministic strategies, there is no
difference between public memory (observable by the other player) and private
memory.

Measure. A game ${\mathcal{G}}$ with initial state $s_{0}$ and strategies
$(\sigma,\pi)$ yields a probability space
$(s_{0}S^{\omega},{\mathcal{F}}_{s_{0}},\mathcal{P}^{{\mathcal{G}}}_{\sigma,\pi,s_{0}})$
where ${\mathcal{F}}_{s_{0}}$ is the $\sigma$-algebra generated by the
cylinder sets $s_{0}s_{1}\ldots s_{n}S^{\omega}$ for $n\geq 0$. The
probability measure $\mathcal{P}^{{\mathcal{G}}}_{\sigma,\pi,s_{0}}$ is first
defined on the cylinder sets. For $\rho=s_{0}\ldots s_{n}$, let
$\mathcal{P}^{{\mathcal{G}}}_{\sigma,\pi,s_{0}}(\rho)\stackrel{{\scriptstyle\text{{\tiny{def}}}}}{{=}}0$
if $\rho$ is not compatible with $\sigma,\pi$ and otherwise
$\mathcal{P}^{{\mathcal{G}}}_{\sigma,\pi,s_{0}}(\rho
S^{\omega})\stackrel{{\scriptstyle\text{{\tiny{def}}}}}{{=}}\prod_{i=0}^{n-1}\tau(s_{0}\ldots
s_{i})(s_{i+1})$ where $\tau$ is $\sigma$ or $\pi$ or $P$ depending on whether
$s_{i}\in S_{\Box}$ or $S_{\Diamond}$ or $S_{\ocircle}$, respectively. By
Carathéodory’s extension theorem [2], this defines a unique probability
measure on the $\sigma$-algebra.

Objectives and Payoff functions. General objectives are defined by real-valued
measurable functions. However, we only consider indicator functions of
measurable sets. Hence our objectives can be described by measurable subsets
$\mathtt{O}\subseteq S^{\omega}$ of plays. The payoff, under strategies
$(\sigma,\pi)$, is the probability that plays belong to $\mathtt{O}$.

We use the syntax and semantics of the LTL operators [14] ${\sf F}$
(eventually), ${\sf G}$ (always) and ${\sf X}$ (next) to specify some
conditions on plays.

Reachability & Safety. A reachability objective is defined by a set of target
states $T\subseteq S$. A play $\rho=s_{0}s_{1}\ldots$ belongs to ${\sf F}\,T$
iff $\exists i\in{\rm Nature}\,s_{i}\in T$. Similarly, $\rho$ belongs to ${\sf
F}^{\leq n}T$ (resp. ${\sf F}^{\geq n}T$) iff $\exists i\leq n$ (resp. $i\geq
n$) such that $s_{i}\in T$. Dually, the safety objective ${\sf G}\,T$ consists
of all plays which never leave $T$. We have ${\sf G}\,T=\neg{\sf F}\neg T$.

Parity. A parity objective is defined via bounded function
${\mathit{C}ol}:S\to{\rm Nature}$ that assigns non-negative priorities (aka
colors) to states. Given an infinite play $\rho=s_{0}s_{1}\ldots$, let
$\text{Inf}(\rho)$ denote the set of numbers that occur infinitely often in
the sequence ${\mathit{C}ol}(s_{0}){\mathit{C}ol}(s_{1})\ldots$. A play $\rho$
satisfies even parity w.r.t. ${\mathit{C}ol}$ iff the minimum of
$\text{Inf}(\rho)$ is even. Otherwise, $\rho$ satisfies odd parity. The
objective even parity is denoted by $\mathtt{EPAR}({\mathit{C}ol})$ and odd
parity is denoted by $\mathtt{OPAR}({\mathit{C}ol})$. Most of the time, we
implicitly assume that the coloring function is known and just write
$\mathtt{EPAR}$ and $\mathtt{OPAR}$. Observe that, given any coloring
${\mathit{C}ol}$, we have $\overline{\mathtt{EPAR}}=\mathtt{OPAR}$ and
$\mathtt{OPAR}({\mathit{C}ol})=\mathtt{EPAR}({\mathit{C}ol}+1)$ where
${\mathit{C}ol}+1$ is the function which adds $1$ to the color of every state.
This justifies to consider only one of the even/odd parity objectives, but,
for the sake of clarity, we distinguish these objectives wherever necessary.

Energy/Reward/Counter based objectives. Let $r:E\to\\{-R,\dots,0,\dots,R\\}$
be a bounded function that assigns weights to transitions. Depending on
context, the sum of these weights in a path can be viewed as energy,
cost/reward or a counter. If $s{\longrightarrow}s^{\prime}$ and
$r((s,s^{\prime}))=c$, we write $s\stackrel{{\scriptstyle
c}}{{{\longrightarrow}}}s^{\prime}$. Let $\rho=s_{0}\stackrel{{\scriptstyle
c_{0}}}{{{\longrightarrow}}}s_{1}\stackrel{{\scriptstyle
c_{1}}}{{{\longrightarrow}}}\ldots$ be a play. We say that $\rho$ satisfies

  1. 1.

the $k$-energy objective $\mathsf{EN}(k)$ iff
$\left(k+\sum_{i=0}^{n-1}c_{i}\right)>0$ for all $n\geq 0$.

  2. 2.

the _$l$ -storage condition_ if $l+\sum_{i=m}^{n-1}c_{i}\geq 0$ holds for
every infix $s_{m}\stackrel{{\scriptstyle
c_{m}}}{{{\longrightarrow}}}s_{m+1}\ldots s_{n}$ of the play. Let
$\mathsf{ST}(k,l)$ denote the set of plays that satisfy both the $k$-energy
and the $l$-storage condition. Let
$\mathsf{ST}(k)\stackrel{{\scriptstyle\text{{\tiny{def}}}}}{{=}}\bigcup_{l}\mathsf{ST}(k,l)$.
Clearly, $\mathsf{ST}(k)\subseteq\mathsf{EN}(k)$.

  3. 3.

$k$-Termination $\operatorname{\mathtt{Term}}(k)$ iff there exists $n\geq 0$
such that $\left(k+\sum_{i=0}^{n-1}c_{i}\right)\leq 0$.

  4. 4.

Limit objective $\mathtt{LimInf}(\rhd z)$ iff
$\left(\liminf_{n\rightarrow\infty}\sum_{i=0}^{n-1}c_{i}\right)\rhd\;z$ for
$\rhd\in\\{<,\leq,=,\geq,>\\}$ and $z\in\mathbb{R}\cup\\{\infty,-\infty\\}$
and similarly for $\mathtt{LimSup}(\rhd z)$.

  5. 5.

Mean payoff $\mathtt{MP}(\rhd\,c)$ for some constant $c\in\mathbb{R}$ iff
$\left(\liminf_{n\rightarrow\infty}\frac{1}{n}\sum_{i=0}^{n-1}c_{i}\right)\rhd\;c$.

Observe that the objectives $k$-energy and $k$-termination are mutually
exclusive and cover all of the plays. A different way to consider these
objectives is to encode the energy level (the sum of the transition weights so
far) into the state space and then consider the obtained infinite-state game
with safety/reachability objective, respectively.

An objective $\mathtt{O}$ is called shift-invariant iff for all finite paths
$\rho$ and plays $\rho^{\prime}\in S^{\omega}$, we have
$\rho\rho^{\prime}\in\mathtt{O}\iff\rho^{\prime}\in\mathtt{O}$. Parity and
mean payoff objectives are shift-invariant, but energy and termination
objectives are not. Objective $\mathtt{O}$ is called submixing iff for all
sequences of finite non-empty words $u_{0}$, $v_{0}$, $u_{1}$, $v_{1}\ldots$
we have
$u_{0}v_{0}u_{1}v_{1}\ldots\in\mathtt{O}\implies\left((u_{0}u_{1}\ldots\in\mathtt{O})\vee(v_{0}v_{1}\ldots\in\mathtt{O})\right)$.

Determinacy. Given an objective $\mathtt{O}$ and a game ${\mathcal{G}}$, state
$s$ has value (w.r.t to $\mathtt{O}$) iff

$\sup_{\sigma\in\Sigma_{{{\mathcal{G}}}}}\inf_{\pi\in\Pi_{{{\mathcal{G}}}}}\mathcal{P}^{{\mathcal{G}}}_{\sigma,\pi,s}(\mathtt{O})=\inf_{\pi\in\Pi_{{{\mathcal{G}}}}}\sup_{\sigma\in\Sigma_{{{\mathcal{G}}}}}\mathcal{P}^{{\mathcal{G}}}_{\sigma,\pi,s}(\mathtt{O}).$

If $s$ has value then
${\mathtt{val}^{{\mathcal{G}}}_{\mathtt{O}}\left(s\right)}$ denotes the value
of $s$ defined by the above equality. A game with an objective is called
weakly determined if every state has value. Stochastic games with Borel
objectives are weakly determined [26, 27]. Our objectives above are Borel,
hence any boolean combination of them is also weakly determined. For
$\varepsilon>0$ and state $s$, a strategy

  1. 1.

$\sigma\in\Sigma_{{{\mathcal{G}}}}$ is $\varepsilon$-optimal (maximizing) iff
$\mathcal{P}^{{\mathcal{G}}}_{\sigma,\pi,s}(\mathtt{O})\geq{\mathtt{val}^{{\mathcal{G}}}_{\mathtt{O}}\left(s\right)}-\varepsilon$
for all $\pi\in\Pi_{{{\mathcal{G}}}}$.

  2. 2.

$\pi\in\Pi_{{{\mathcal{G}}}}$ is $\varepsilon$-optimal (minimizing) iff
$\mathcal{P}^{{\mathcal{G}}}_{\sigma,\pi,s}(\mathtt{O})\leq{\mathtt{val}^{{\mathcal{G}}}_{\mathtt{O}}\left(s\right)}+\varepsilon$
for all $\sigma\in\Sigma_{{{\mathcal{G}}}}$.

A $0$-optimal strategy is called _optimal_. An MD strategy is called
_uniformly_ $\varepsilon$-optimal (resp. uniformly optimal) if it is so from
every start state. An optimal strategy for player $\Box$ from state $s$ is
_almost surely_ winning if
${\mathtt{val}^{{\mathcal{G}}}_{\mathtt{O}}\left(s\right)}=1$. By
$\mathsf{AS}\left(\mathtt{O}\right)$ we denote the set of states that have an
almost surely winning strategy for objective $\mathtt{O}$. For ease of
presentation, we drop subscripts and superscripts wherever possible if they
are clear from the context.

Energy-parity. We are concerned with approximating the value for the combined
energy-parity objective $\mathtt{EN}(k)\cap\mathtt{EPAR}$ and building
$\varepsilon$-optimal strategies.

In our constructions we use some auxiliary objectives. Following [29], these
are defined as
$\operatorname{\mathtt{Gain}}\stackrel{{\scriptstyle\text{{\tiny{def}}}}}{{=}}\mathtt{LimInf}(>-\infty)\,\cap\,\mathtt{EPAR}$
and
$\operatorname{\mathtt{Loss}}\stackrel{{\scriptstyle\text{{\tiny{def}}}}}{{=}}\overline{\operatorname{\mathtt{Gain}}}=\mathtt{LimInf}(=-\infty)\,\cup\,\mathtt{OPAR}$.

######  Remark 2.1.

For finite-state SSGs and the following objectives there exist optimal MD
strategies for both players. Moreover, if the SSG is just a maximizing MDP
then the set of states that are almost surely winning for Maximizer can be
computed in polynomial time.

  1. 1.

${\sf F}\,T$ [15]

  2. 2.

$\mathtt{LimInf}(\rhd-\infty)$, $\mathtt{LimInf}(\rhd\infty)$,
$\mathtt{LimSup}(\rhd-\infty)$, $\mathtt{LimSup}(\rhd\infty)$,
$\mathtt{MP}(>\,0)$ [5, Prop. 1]

  3. 3.

$\mathtt{EPAR}$ [37]

##  3 The Main Result

The following theorem states our main result.

######  Theorem 3.1.

Let ${\mathcal{G}}=\left(S,(S_{\Box},S_{\Diamond},S_{\ocircle}),{E},P\right)$
be an SSG with transition rewards in unary assigned by function $r$ and colors
assigned to states by function ${\mathit{C}ol}$. For every state $s\in S$,
initial energy level $i\geq 0$ and error margin $\varepsilon>0$, one can
compute

  1. 1.

a rational number $v^{\prime}$ such that $0\leq
v^{\prime}-{\mathtt{val}^{{\mathcal{G}}}_{\mathtt{EN}(i)\,\cap\mathtt{EPAR}}\left(s\right)}\leq\varepsilon$
in 2-$\mathsf{NEXPTIME}$. 111We write “computing a number $v^{\prime}$ in
2-$\mathsf{NEXPTIME}$” as a shorthand for the property that questions like
$v^{\prime}\leq c$ for constants $c$ are decidable in 2-$\mathsf{NEXPTIME}$.

  2. 2.

$\varepsilon$-optimal FD strategies $\sigma_{\varepsilon}$ and
$\pi_{\varepsilon}$ for Maximizer and Minimizer, resp., in
2-$\mathsf{NEXPTIME}$. These strategies use
${\mathcal{O}}\left(2\textrm{-}\mathsf{EXP}\left(\lvert{\mathcal{G}}\rvert\right)\cdot\log\left(\frac{1}{\varepsilon}\right)\right)$
memory modes.

For rewards in binary, the bounds above increase by one exponential.

We outline the main steps of the proof; details in the following sections. We
begin with the observation that $\mathtt{EN}(i)\subseteq\mathtt{EN}(j)$ for
$i\leq j$, and thus for all states $s$ we have
${\mathtt{val}^{{\mathcal{G}}}_{\mathtt{EN}(i)\,\cap\,\mathtt{EPAR}}\left(s\right)}\leq{\mathtt{val}^{{\mathcal{G}}}_{\mathtt{EN}(j)\,\cap\,\mathtt{EPAR}}\left(s\right)}\leq
1.$ So
$\lim_{n\rightarrow\infty}{\mathtt{val}^{{\mathcal{G}}}_{\mathtt{EN}(n)\,\cap\,\mathtt{EPAR}}\left(s\right)}$
exists. We define

$\displaystyle{\mathtt{Lval}^{{\mathcal{G}}}\left(s\right)}$
$\displaystyle\stackrel{{\scriptstyle\text{{\tiny{def}}}}}{{=}}\lim_{n\rightarrow\infty}{\mathtt{val}^{{\mathcal{G}}}_{\mathtt{EN}(n)\,\cap\,\mathtt{EPAR}}\left(s\right)}.$
(1)

We will see that ${\mathtt{Lval}^{{\mathcal{G}}}\left(s\right)}$ and
${\mathtt{val}^{{\mathcal{G}}}_{\operatorname{\mathtt{Gain}}}\left(s\right)}$
are in fact equal (a consequence of Lemma 5.6) and
${\mathtt{val}^{{\mathcal{G}}}_{\operatorname{\mathtt{Gain}}}\left(s\right)}$
can be computed in nondeterministic polynomial time (Theorem 4.4).
Intuitively, for high energy levels, the precise energy level does not matter
much for the value.

The main steps of the approximation algorithm are as follows.

  1. 1.

Compute FD strategies $\sigma^{*}(s)$ that are optimal maximizing for the
objective $\operatorname{\mathtt{Gain}}$ starting from state $s$ in
${\mathcal{G}}$. Compute an MD strategy $\pi^{*}$ that is uniformly optimal
minimizing for the objective $\operatorname{\mathtt{Gain}}$. Compute the value
${\mathtt{val}^{{\mathcal{G}}}_{\operatorname{\mathtt{Gain}}}\left(s\right)}$
for every $s\in S$. See Section 4.

  2. 2.

Compute a natural number $N$ such that for all $s\in S$ and all $i\geq N$ we
have

$0\leq{\mathtt{val}^{{\mathcal{G}}}_{\operatorname{\mathtt{Gain}}}\left(s\right)}-{\mathtt{val}^{{\mathcal{G}}}_{\mathtt{EN}(i)\,\cap\,\mathtt{EPAR}}\left(s\right)}\leq\varepsilon.$

$N$ will be doubly exponential. See Section 5.

  3. 3.

Consider the finite-state parity game ${\mathcal{G}}^{\prime}$ derived from
${\mathcal{G}}$ by encoding the energy level up-to $N$ into the states, i.e.,
the states of ${\mathcal{G}}^{\prime}$ are of the form $(s,k)$ for $s\in S$
and $0\leq k\leq N$, and colors are inherited from $s$. Moreover, we add
gadgets that ensure that states $(s,N)$ at the upper end win with probability
${\mathtt{val}^{{\mathcal{G}}}_{\operatorname{\mathtt{Gain}}}\left(s\right)}$
and states $(s,0)$ at the lower end lose. By the previous item,
${\mathtt{val}^{{\mathcal{G}}}_{\operatorname{\mathtt{Gain}}}\left(s\right)}$
is $\varepsilon$-close to
${\mathtt{val}^{{\mathcal{G}}}_{\mathtt{EN}(N)\,\cap\,\mathtt{EPAR}}\left(s\right)}$.
Thus, for $k<N$ we can $\varepsilon$-approximate the value
$v={\mathtt{val}^{{\mathcal{G}}}_{\mathtt{EN}(k)\,\cap\,\mathtt{EPAR}}\left(s\right)}$
by
$v^{\prime}\stackrel{{\scriptstyle\text{{\tiny{def}}}}}{{=}}{\mathtt{val}^{{\mathcal{G}}^{\prime}}_{\mathtt{EPAR}}\left((s,k)\right)}$.
If $k\geq N$ we can $\varepsilon$-approximate $v$ by
$v^{\prime}\stackrel{{\scriptstyle\text{{\tiny{def}}}}}{{=}}{\mathtt{val}^{{\mathcal{G}}}_{\operatorname{\mathtt{Gain}}}\left(s\right)}$.

Moreover, we obtain $\varepsilon$-optimal FD strategies $\sigma_{\varepsilon}$
for Maximizer (resp. $\pi_{\varepsilon}$ for Minimizer) for
$\mathtt{EN}(k)\,\cap\,\mathtt{EPAR}$ in ${\mathcal{G}}$. Let $\hat{\sigma}$
(resp. $\hat{\pi}$) be optimal MD strategies for Maximizer (resp. Minimizer)
for the objective $\mathtt{EPAR}$ in ${\mathcal{G}}^{\prime}$. Then
$\sigma_{\varepsilon}$ plays as follows. While the current energy level $j$
($k$ plus the sum of the rewards so far) stays $<N$, then, at any state
$s^{\prime}$, play like $\hat{\sigma}$ at state $(s^{\prime},j)$ in
${\mathcal{G}}^{\prime}$. Once the energy level reaches a value $\geq N$ at
some state $s^{\prime}$ for the first time, then play like
$\sigma^{*}(s^{\prime})$ forever. Similarly, $\pi_{\varepsilon}$ plays as
follows. While the current energy level $j$ ($k$ plus the sum of the rewards
so far) stays $<N$, then, at any state $s^{\prime}$, play like $\hat{\pi}$ at
state $(s^{\prime},j)$ in ${\mathcal{G}}^{\prime}$. Once the energy level
reaches a value $\geq N$ (at any state) for the first time, then play like
$\pi^{*}$ forever. See Section 6.

As a technical tool, we sometimes consider the dual of a game ${\mathcal{G}}$
(resp. the dual maximizing MDP of some minimizing MDP). Consider
${\mathcal{G}}^{d}\stackrel{{\scriptstyle\text{{\tiny{def}}}}}{{=}}\left(S^{\prime},(S_{\Box}^{\prime},S_{\Diamond}^{\prime},S_{\ocircle}^{\prime}),{E}^{\prime},P^{\prime}\right)$
with the complement objective
$\overline{\mathtt{EN}(k)\,\cap\,\mathtt{EPAR}}=\operatorname{\mathtt{Term}}(k)\cup\mathtt{OPAR}$,
where ${\mathcal{G}}^{d}$ is simply the game with the roles of Maximizer and
Minimizer reversed, i.e.,

$\displaystyle S^{\prime}$ $\displaystyle=S$ $\displaystyle S_{\Box}^{\prime}$
$\displaystyle=S_{\Diamond}$ $\displaystyle S_{\Diamond}^{\prime}$
$\displaystyle=S_{\Box}$ $\displaystyle S_{\ocircle}^{\prime}$
$\displaystyle=S_{\ocircle}$ $\displaystyle{E}^{\prime}$ $\displaystyle={E}$
$\displaystyle P^{\prime}$ $\displaystyle=P$

Hence $\Sigma_{{{\mathcal{G}}^{d}}}=\Pi_{{{\mathcal{G}}}}$ and
$\Pi_{{{\mathcal{G}}^{d}}}=\Sigma_{{{\mathcal{G}}}}$. It is easy to see that
for any objective $\mathtt{O}$ and start state $s$

  1. 1.

${\mathtt{val}^{{\mathcal{G}}}_{\mathtt{O}}\left(s\right)}+{\mathtt{val}^{{\mathcal{G}}^{d}}_{\overline{\mathtt{O}}}\left(s\right)}=1$.

  2. 2.

$\sigma$ is $\varepsilon$-optimal maximizing for $\mathtt{O}$ in
${\mathcal{G}}$ iff it is $\varepsilon$-optimal minimizing for
$\overline{\mathtt{O}}$ in ${\mathcal{G}}^{d}$.

  3. 3.

$\pi$ is $\varepsilon$-optimal minimizing for $\mathtt{O}$ in ${\mathcal{G}}$
iff it is $\varepsilon$-optimal maximizing for $\overline{\mathtt{O}}$ in
${\mathcal{G}}^{d}$.

So approximating the value of $\mathtt{EN}(k)\,\cap\,\mathtt{EPAR}$ in
${\mathcal{G}}$ can be reduced in linear time to approximating the value of
$\operatorname{\mathtt{Term}}(k)\,\cup\,\mathtt{OPAR}$ in ${\mathcal{G}}^{d}$.

##  4 Computing
${\mathtt{val}^{{\mathcal{G}}}_{\operatorname{\mathtt{Gain}}}\left(s\right)}$

Given an SSG
${\mathcal{G}}=\left(S,(S_{\Box},S_{\Diamond},S_{\ocircle}),{E},P\right)$ and
a start state $s$, we will show how to compute
${\mathtt{val}^{{\mathcal{G}}}_{\operatorname{\mathtt{Gain}}}\left(s\right)}$
and the optimal strategies for both players.

We start with the case of maximizing MDPs. The following lemma summarizes some
previous results ([29, Lemmas 30,16], [28, Lemma 26], [24, Proposition 4]).

######  Lemma 4.1.

Let ${\mathcal{M}}$ be a maximizing MDP.

  1. 1.

${\mathtt{Lval}^{{\mathcal{M}}}\left(s\right)}={\mathtt{val}^{{\mathcal{M}}}_{\operatorname{\mathtt{Gain}}}\left(s\right)}$
for all states $s\in S$.

  2. 2.

Optimal strategies for $\operatorname{\mathtt{Gain}}$ in ${\mathcal{M}}$ exist
and can be chosen FD, with
$\mathcal{O}(\exp(|{\mathcal{M}}|^{\mathcal{O}(1)}))$ memory modes, and
exponential memory is also necessary.

  3. 3.

For any state $s\in S$, ${\mathtt{Lval}^{{\mathcal{M}}}\left(s\right)}$ is
rational and can be computed in $\mathcal{O}(|{\mathcal{M}}|^{8})$
deterministic polynomial time if rewards are in unary, and in $\mathsf{NP}$
and $\mathsf{coNP}$ if rewards are in binary.

######  Proof 4.2.

Item 1 holds by [29, Lemma 30].

Towards Item 2, we follow the proof of [29, Lemma 16]. Since
$\operatorname{\mathtt{Gain}}=\mathtt{LimInf}(>-\infty)\,\cap\,\mathtt{EPAR}$
is shift-invariant, there exist optimal strategies by [22]. By [28, Theorem
18] and Item 1, an optimal strategy for $\operatorname{\mathtt{Gain}}$ can be
constructed as follows. Let
$A\stackrel{{\scriptstyle\text{{\tiny{def}}}}}{{=}}\bigcup_{k\in\mathbb{N}}\mathsf{AS}\left(\mathsf{ST}(k)\cap\mathtt{EPAR}\right)$
and
$B\stackrel{{\scriptstyle\text{{\tiny{def}}}}}{{=}}\mathsf{AS}\left(\mathtt{LimInf}(=\infty)\cap\mathtt{EPAR}\right)$
be the subsets of states from which there exist almost surely winning
strategies for the objectives $\mathsf{ST}(k)\cap\mathtt{EPAR}$ and
$\mathtt{LimInf}(=\infty)\cap\mathtt{EPAR}$, respectively. By [28, Theorem 8],
we can restrict the values $k$ in the definition of $A$ by some
$k^{\prime}=\mathcal{O}(|S|\cdot R)$, i.e., $A=\bigcup_{k\leq
k^{\prime}}\mathsf{AS}\left(\mathsf{ST}(k)\cap\mathtt{EPAR}\right)$. An
optimal strategy $\sigma$ for $\operatorname{\mathtt{Gain}}$ works in two
phases. First it plays an optimal strategy $\sigma_{R}$ towards reaching the
set $A\cup B$, where $\sigma_{R}$ can be chosen MD by Remark 2.1. Then, upon
reaching $A$ (resp. $B$), it plays an almost surely winning strategy
$\sigma_{A}$ for the objective $\mathsf{ST}(k)\cap\mathtt{EPAR}$ (resp.
$\sigma_{B}$ for the objective $\mathtt{LimInf}(=\infty)\cap\mathtt{EPAR}$).
By [28, Theorem 8], the strategy $\sigma_{A}$ requires
$\mathcal{O}(k\cdot|S|)$ memory modes for a given $k$ and thus at most
$\mathcal{O}(|S|^{2}\cdot R)$, since we can assume that $k\leq k^{\prime}$.
Towards the strategy $\sigma_{B}$, we first observe that in finite MDPs a
strategy is almost-surely winning for
$\mathtt{LimInf}(=\infty)\cap\mathtt{EPAR}$ iff it is almost-surely winning
for $\mathtt{MP}(>\,0)\cap\mathtt{EPAR}$. By [24, Proposition 4], there exist
optimal deterministic strategies for $\mathtt{MP}(>\,0)\cap\mathtt{EPAR}$ that
use exponential memory, i.e.,
$\mathcal{O}(\exp(|{\mathcal{M}}|^{\mathcal{O}(1)}))$ memory modes. The memory
required for $\sigma_{B}$ exceeds that of $\sigma_{R}$ and $\sigma_{A}$ (even
when $R$ is given in binary), and the one extra memory mode to record the
switch from $\sigma_{R}$ to $\sigma_{A}$ (resp. $\sigma_{B}$) is negligible in
comparison. Thus we can conclude that $\sigma$ uses
$\mathcal{O}(\exp(|{\mathcal{M}}|^{\mathcal{O}(1)}))$ memory modes. [24, Fig.
1 and Prop. 4] shows that exponential memory is necessary.

Towards Item 3, let
$d\stackrel{{\scriptstyle\text{{\tiny{def}}}}}{{=}}|{\mathit{C}ol}(S)|$ be the
number of priorities in the parity condition. By [28, Lemma 26], for each
$s\in S$, ${\mathtt{Lval}^{{\mathcal{M}}}\left(s\right)}$ is rational and can
be computed in deterministic time $\tilde{\mathcal{O}}(|E|\cdot
d\cdot|S|^{4}\cdot R+d\cdot|S|^{3.5}\cdot(|P|+|r|)^{2})$ (and still in
$\mathsf{NP}$ and $\mathsf{coNP}$ if $R$ is given in binary). So
${\mathtt{Lval}^{{\mathcal{M}}}\left(s\right)}$ can be computed in
$\mathcal{O}(|{\mathcal{M}}|^{8})$ deterministic polynomial time if weights
are given in unary, and in $\mathsf{NP}$ and $\mathsf{coNP}$ if weights are
given in binary.

In order to extend Lemma 4.1 from MDPs to games, we need the notion of derived
MDPs, obtained by fixing the choices of one player according to some FD
strategy. Given an SSG
${\mathcal{G}}=\left(S,(S_{\Box},S_{\Diamond},S_{\ocircle}),{E},P\right)$ and
a finite memory deterministic (FD) strategy $\pi$ for Minimizer (resp.
$\sigma$ for Maximizer) from a state $s$, described by $\left({\sf M},{\sf
m}_{0},{\sf upd},{\sf nxt}\right)$, let ${\mathcal{G}}_{\pi}$ (resp.
${\mathcal{G}}^{\sigma}$) be the maximizing (resp. minimizing) MDP with state
space ${\sf M}\times S$ obtained by fixing Minimizer’s (resp. Maximizer’s)
choices according to $\pi$ (resp. $\sigma$).

######  Lemma 4.3.

For every SSG ${\mathcal{G}}$, objective $\mathtt{O}$ and Minimizer (resp.
Maximizer) FD strategy $\pi=\left({\sf M},{\sf m}_{0},{\sf upd},{\sf
nxt}\right)$ (resp. $\sigma$), from state $s$ we get
${\mathtt{val}^{{\mathcal{G}}^{\sigma}}_{\mathtt{O}}\left(\left({\sf
m}_{0},s\right)\right)}\leq{\mathtt{val}^{{\mathcal{G}}}_{\mathtt{O}}\left(s\right)}\leq{\mathtt{val}^{{\mathcal{G}}_{\pi}}_{\mathtt{O}}\left(\left({\sf
m}_{0},s\right)\right)}$ and equality holds if $\pi$ (resp. $\sigma$) is
optimal from state $s$.

######  Theorem 4.4.

Consider an SSG
${\mathcal{G}}=\left(S,(S_{\Box},S_{\Diamond},S_{\ocircle}),{E},P\right)$ with
the $\operatorname{\mathtt{Gain}}$ objective.

  1. 1.

Optimal Minimizer strategies exist and can be chosen uniform MD.

  2. 2.

${\mathtt{val}^{{\mathcal{G}}}_{\operatorname{\mathtt{Gain}}}\left(s\right)}$
is rational and questions about it, i.e.,
${\mathtt{val}^{{\mathcal{G}}}_{\operatorname{\mathtt{Gain}}}\left(s\right)}\leq
c$ for constants $c$, are decidable in $\mathsf{NP}$.

  3. 3.

Optimal Maximizer strategies exist and can be chosen FD, with
$\mathcal{O}(\exp(|{\mathcal{G}}|^{\mathcal{O}(1)}))$ memory modes. Moreover,
exponential memory is also necessary.

######  Proof 4.5.

Towards Item 1, observe that since both the objectives
$\mathtt{LimInf}(=-\infty)$ and $\mathtt{OPAR}$ are shift-invariant and
submixing, so is their union, i.e., $\overline{\operatorname{\mathtt{Gain}}}$
is shift-invariant and submixing. Hence, by [23, Theorem 1.1], an optimal MD
strategy $\pi^{*}_{s}$ for Minimizer exists from any state $s\in S$. Since $S$
is finite and $\operatorname{\mathtt{Gain}}$ is shift-invariant, we can also
obtain a uniformly optimal MD strategy $\pi^{*}$, i.e., $\pi^{*}$ is optimal
from every state.

Towards Item 2, consider the maximizing MDP ${\mathcal{G}}_{\pi^{*}}$ obtained
from ${\mathcal{G}}$ by fixing $\pi^{*}$ (cf. Definition A.1). Since $\pi^{*}$
is MD, the states of ${\mathcal{G}}_{\pi^{*}}$ are the same as the states as
${\mathcal{G}}$. Since $\pi^{*}$ is optimal for Minimizer from every state
$s$, we obtain that
${\mathtt{val}^{{\mathcal{G}}}_{\operatorname{\mathtt{Gain}}}\left(s\right)}={\mathtt{val}^{{\mathcal{G}}_{\pi^{*}}}_{\operatorname{\mathtt{Gain}}}\left(s\right)}$
for every state $s$ by Lemma 4.3. By Lemma 4.1, the latter is rational and can
be computed in polynomial time for weights in unary (resp. in $\mathsf{NP}$
and $\mathsf{coNP}$ for weights in binary). Thus, by guessing $\pi^{*}$, we
can decide questions
${\mathtt{val}^{{\mathcal{G}}}_{\operatorname{\mathtt{Gain}}}\left(s\right)}\leq
c$ in $\mathsf{NP}$.

Towards Item 3, we again use the property that
$\overline{\operatorname{\mathtt{Gain}}}$ is shift-invariant and submixing
(see above). By [29, Theorem 6, Def. 24], optimal FD Maximizer strategies for
$\operatorname{\mathtt{Gain}}$ in an SSG require only
$|S_{\Diamond}|\cdot\lceil\log(|E|)\rceil$ many extra bits of memory above the
memory required for optimal Maximizer strategies in any derived MDP
${\mathcal{M}}$ where Minimizer’s choices are fixed. Hence, by Lemma 4.1, one
can obtain optimal FD Maximizer strategies in ${\mathcal{G}}$ that use at most
$2^{|S_{\Diamond}|\cdot\lceil\log(|E|)\rceil}\cdot\mathcal{O}(\exp(|{\mathcal{M}}|^{\mathcal{O}(1)}))=\mathcal{O}(\exp(|{\mathcal{G}}|^{\mathcal{O}(1)}))$
memory modes. The corresponding exponential lower bound on the memory holds
already for MDPs by Lemma 4.1.

##  5 Computing the Upper Bound $N$

We show how to compute the upper bound $N$, up-to which Maximizer needs to
remember the energy level, for any given error margin $\varepsilon>0$.
Similarly as in Section 4, we first solve the problem for maximizing MDPs and
then extend the solution to SSGs.

###  5.1 Computing $N$ for maximizing MDPs

Given a maximizing MDP
${\mathcal{M}}=\left(S,S_{\Box},S_{\ocircle},{E},P\right)$ and
$\varepsilon>0$, we will compute an $N\in\mathbb{N}$ such that for all $s\in
S$ and all $j\geq N$

$0\leq{\mathtt{val}^{{\mathcal{M}}}_{\operatorname{\mathtt{Term}}(j)\,\cup\,\mathtt{OPAR}}\left(s\right)}-{\mathtt{val}^{{\mathcal{M}}}_{\operatorname{\mathtt{Loss}}}\left(s\right)}\leq\varepsilon.$

Recall that
$\operatorname{\mathtt{Loss}}=\mathtt{LimInf}(=-\infty)\,\cup\,\mathtt{OPAR}$.
We now define the sets of states
$W_{0}\stackrel{{\scriptstyle\text{{\tiny{def}}}}}{{=}}\mathsf{AS}\left(\operatorname{\mathtt{Loss}}\right)$,
$W_{1}\stackrel{{\scriptstyle\text{{\tiny{def}}}}}{{=}}\mathsf{AS}\left(\mathtt{LimInf}(=-\infty)\right)$
and
$W_{2}\stackrel{{\scriptstyle\text{{\tiny{def}}}}}{{=}}\mathsf{AS}\left(\mathtt{OPAR}\right)$.
By Remark 2.1, there exist optimal MD strategies for
$\mathtt{LimInf}(=-\infty)$ and $\mathtt{OPAR}$. Since
$\operatorname{\mathtt{Loss}}$ is shift-invariant and submixing, there exists
an optimal MD strategy for it by [23, Theorem 1.1].

######  Lemma 5.1.

For every state $s$ in the MDP ${\mathcal{M}}$ we have

  1. 1.

$W_{1}\cup W_{2}\subseteq W_{0}$

  2. 2.

${\mathtt{val}_{{\sf
F}\,{W_{0}}}\left(s\right)}\leq{\mathtt{val}_{\operatorname{\mathtt{Loss}}}\left(s\right)}$

  3. 3.

${\mathtt{val}_{\mathtt{OPAR}\,\cap\,\overline{{\sf
F}\,{W_{2}}}}\left(s\right)}=0$

  4. 4.

for every initial energy level $j\geq 0$

$\displaystyle{\mathtt{val}_{\left(\operatorname{\mathtt{Term}}(j)\,\cup\,\mathtt{OPAR}\right)\,\cap\,{\sf
F}\,W_{0}}\left(s\right)}={\mathtt{val}_{{\sf F}\,W_{0}}\left(s\right)}$ (2)
$\displaystyle{\mathtt{val}_{\operatorname{\mathtt{Loss}}}\left(s\right)}\leq{\mathtt{val}_{\operatorname{\mathtt{Term}}(j)\,\cup\,\mathtt{OPAR}}\left(s\right)}\leq{\mathtt{val}_{\operatorname{\mathtt{Loss}}}\left(s\right)}+\sup_{\sigma}\mathcal{P}_{\sigma,s}\left(\operatorname{\mathtt{Term}}(j)\,\cap\,\overline{{\sf
F}\,{W_{1}}}\right)$ (3)

######  Proof 5.2.

  1. 1.

This follows directly from the definitions of $W_{0},W_{1},W_{2}$.

  2. 2.

Let $\sigma^{\prime}$ be an optimal MD strategy for ${\sf F}\,{W_{0}}$ from
$s$ and $\sigma^{\prime\prime}$ be an almost surely winning MD strategy for
$\operatorname{\mathtt{Loss}}$ from any state in $W_{0}$. Let $\sigma$ be the
strategy that plays $\sigma^{\prime}$ until reaching $W_{0}$ and then switches
to $\sigma^{\prime\prime}$. We have
${\mathtt{val}_{\operatorname{\mathtt{Loss}}}\left(s\right)}\geq\mathcal{P}_{\sigma,s}(\operatorname{\mathtt{Loss}})\geq\mathcal{P}_{\sigma^{\prime},s}({\sf
F}\,W_{0})={\mathtt{val}_{{\sf F}\,W_{0}}\left(s\right)}$.

  3. 3.

For $s\in W_{2}$ the statement is obvious. So let $s\notin W_{2}$ and consider
the modified MDP
${\mathcal{M}}^{\prime}=\left(S^{\prime},S_{\Box}^{\prime},S_{\ocircle}^{\prime},{E}^{\prime},P^{\prime}\right)$
where all states in $W_{2}$ are collapsed into a losing sink. I.e.,
$S^{\prime}\stackrel{{\scriptstyle\text{{\tiny{def}}}}}{{=}}(S\setminus
W_{2})\uplus\left\\{\mathit{trap}\right\\}$, with $\mathit{trap}$ a new random
sink state having color $0$ (thus losing for objective $\mathtt{OPAR}$),
${E}^{\prime}$ contains all of $\left({E}\cap\left\\{(S\setminus
W_{2})\times(S\setminus
W_{2})\right\\}\cup(\mathit{trap},\mathit{trap})\right)$ and all transitions
to $W_{2}$ are redirected to $\mathit{trap}$ and $P^{\prime}$ is derived
accordingly from $P$. Then
${\mathtt{val}^{{\mathcal{M}}^{\prime}}_{\mathtt{OPAR}}\left(\hat{s}\right)}={\mathtt{val}^{{\mathcal{M}}}_{\mathtt{OPAR}\,\cap\,\overline{{\sf
F}{W_{2}}}}\left(\hat{s}\right)}$ for all states $\hat{s}\in S\setminus
W_{2}$. Towards a contradiction, assume that
${\mathtt{val}^{{\mathcal{M}}}_{\mathtt{OPAR}\,\cap\,\overline{{\sf
F}{W_{2}}}}\left(s\right)}>0$. Hence
${\mathtt{val}^{{\mathcal{M}}^{\prime}}_{\mathtt{OPAR}}\left(s\right)}>0$.
Then, by [22, Theorem 3.2], there exists a state $s^{\prime}\in S^{\prime}$
such that
${\mathtt{val}^{{\mathcal{M}}^{\prime}}_{\mathtt{OPAR}}\left(s^{\prime}\right)}=1$,
and it is easy to see that $s^{\prime}\neq\mathit{trap}$ and thus
$s^{\prime}\in S\setminus W_{2}$. But this implies that
${\mathtt{val}^{{\mathcal{M}}}_{\mathtt{OPAR}}\left(s^{\prime}\right)}=1$ and
thus $s^{\prime}\in W_{2}$, a contradiction.

  4. 4.

Let
$\mathtt{O}\stackrel{{\scriptstyle\text{{\tiny{def}}}}}{{=}}\operatorname{\mathtt{Term}}(j)\,\cup\,\mathtt{OPAR}$.
For Equation 2, the first inequality ${\mathtt{val}_{\mathtt{O}\,\cap\,{\sf
F}W_{0}}\left(s\right)}\leq{\mathtt{val}_{{\sf F}W_{0}}\left(s\right)}$ is
trivial, since $\mathtt{O}\,\cap\,{\sf F}\,W_{0}\subseteq{\sf F}W_{0}$. To
show the reverse inequality, consider the strategy $\sigma$ that first plays
like an optimal MD strategy $\sigma^{\prime}$ for the objective ${\sf
F}\,W_{0}$ and after reaching $W_{0}$ switches to an almost surely winning MD
strategy $\sigma^{\prime\prime}$ for the objective
$\operatorname{\mathtt{Loss}}$. Then ${\mathtt{val}_{\mathtt{O}\,\cap\,{\sf
F}W_{0}}\left(s\right)}\geq\mathcal{P}_{\sigma,s}(\mathtt{O}\,\cap\,{\sf
F}\,W_{0})\geq\mathcal{P}_{\sigma,s}(\operatorname{\mathtt{Loss}}\,\cap\,{\sf
F}\,W_{0})=\mathcal{P}_{\sigma^{\prime},s}({\sf F}\,W_{0})={\mathtt{val}_{{\sf
F}W_{0}}\left(s\right)}$, where the second inequality is due to
$\mathtt{LimInf}(=-\infty)\subseteq\operatorname{\mathtt{Term}}(j)$.

For Equation 3, the first inequality is again due to the fact that
$\mathtt{LimInf}(=-\infty)\subseteq\operatorname{\mathtt{Term}}(j)$ for all
$j\geq 0$. Towards the second inequality of Equation 3 we have

$\displaystyle{\mathtt{val}_{\mathtt{O}}\left(s\right)}$
$\displaystyle=\sup_{\sigma}\mathcal{P}_{\sigma,s}(\mathtt{O})$
$\displaystyle=\sup_{\sigma}\left(\mathcal{P}_{\sigma,s}\left(\mathtt{O}\,\cap\,{\sf
F}\,{W_{0}}\right)+\mathcal{P}_{\sigma,s}\left(\mathtt{O}\,\cap\,\overline{{\sf
F}\,{W_{0}}}\right)\right)$ $\displaystyle\left(\textrm{Law of total
probability}\right)$
$\displaystyle\leq\sup_{\sigma}\mathcal{P}_{\sigma,s}\left(\mathtt{O}\,\cap\,{\sf
F}\,{W_{0}}\right)+\sup_{\sigma}\mathcal{P}_{\sigma,s}\left(\mathtt{O}\,\cap\,\overline{{\sf
F}\,{W_{0}}}\right)$ $\displaystyle\left(\sup\left(f+g\right)\leq\sup f+\sup
g\right)$ $\displaystyle=\sup_{\sigma}\mathcal{P}_{\sigma,s}\left({\sf
F}\,{W_{0}}\right)+\sup_{\sigma}\mathcal{P}_{\sigma,s}\left(\mathtt{O}\,\cap\,\overline{{\sf
F}\,{W_{0}}}\right)$
$\displaystyle\left(\lx@cref{creftype~refnum}{eq:valTermcapFW = valFW}\right)$
$\displaystyle\leq{\mathtt{val}_{\operatorname{\mathtt{Loss}}}\left(s\right)}+\sup_{\sigma}\mathcal{P}_{\sigma,s}\left(\mathtt{O}\,\cap\,\overline{{\sf
F}\,{W_{0}}}\right)$ $\displaystyle\left(\lx@cref{creftype~refnum}{itm:Fw
lessequal nus}\right)$

We can upper-bound the second summand above as follows.

$\displaystyle\sup_{\sigma}\mathcal{P}_{\sigma,s}(\mathtt{O}\,\cap\,\overline{{\sf
F}\,{W_{0}}})$
$\displaystyle=\sup_{\sigma}\mathcal{P}_{\sigma,s}\left((\operatorname{\mathtt{Term}}(j)\,\cup\,\mathtt{OPAR})\,\cap\,\overline{{\sf
F}\,{W_{0}}}\right)$
$\displaystyle\leq\sup_{\sigma}\mathcal{P}_{\sigma,s}\left(\operatorname{\mathtt{Term}}(j)\,\cap\,\overline{{\sf
F}\,{W_{0}}}\right)+\sup_{\sigma}\mathcal{P}_{\sigma,s}\left(\mathtt{OPAR}\,\cap\,\overline{{\sf
F}\,{W_{0}}}\right)$ $\displaystyle\left(\textrm{Union bound}\right)$
$\displaystyle\leq\sup_{\sigma}\mathcal{P}_{\sigma,s}\left(\operatorname{\mathtt{Term}}(j)\,\cap\,\overline{{\sf
F}\,{W_{1}}}\right)+\sup_{\sigma}\mathcal{P}_{\sigma,s}\left(\mathtt{OPAR}\,\cap\,\overline{{\sf
F}\,{W_{2}}}\right)$ $\displaystyle\left(\lx@cref{creftype~refnum}{itm:Wi sub
W}\right)\quad\quad$
$\displaystyle=\sup_{\sigma}\mathcal{P}_{\sigma,s}\left(\operatorname{\mathtt{Term}}(j)\,\cap\,\overline{{\sf
F}\,{W_{1}}}\right)$
$\displaystyle\left(\lx@cref{creftype~refnum}{itm:val_parcapcompW2 =
0}\right)\quad\quad$

We show that the term
$\sup_{\sigma}\mathcal{P}_{\sigma,s}\left(\operatorname{\mathtt{Term}}(j)\,\cap\,\overline{{\sf
F}\,{W_{1}}}\right)$ in Equation 3 can be made arbitrarily small for large
$j$. To this end, we use [3, Lemma 3.9] (adapted to our notation).

######  Lemma 5.3.

[3, Lemma 3.9 and Claim 6] Let
${\mathcal{M}}=\left(S,S_{\Box},S_{\ocircle},{E},P\right)$ be a maximizing
finite MDP with rewards in unary and
$W_{1}\stackrel{{\scriptstyle\text{{\tiny{def}}}}}{{=}}\mathsf{AS}\left(\mathtt{LimInf}(=-\infty)\right)$.
One can compute, in polynomial time, a rational constant $c<1$, and an integer
$h\geq 0$ such that for all $j\geq h$ and $s\in S$

$\sup_{\sigma}\mathcal{P}_{\sigma,s}\left(\operatorname{\mathtt{Term}}(j)\,\cap\,\overline{{\sf
F}\,W_{1}}\right)\leq\frac{c^{j}}{1-c}.$

Moreover,
$1/(1-c)\in{\mathcal{O}}\left(\exp(\lvert{\mathcal{M}}\rvert^{\mathcal{O}(1)})\right)$
and
$h\in{\mathcal{O}}(\exp\left(\lvert{\mathcal{M}}\rvert^{{\mathcal{O}}(1)}\right))$.

######  Lemma 5.4.

Consider a maximizing MDP
${\mathcal{M}}=\left(S,S_{\Box},S_{\ocircle},{E},P\right)$, $\varepsilon>0$
and the constants $c,h$ from Lemma 5.3. For rewards in unary and $i\geq N$ we
have
${\mathtt{val}^{{\mathcal{M}}}_{\operatorname{\mathtt{Term}}(i)\,\cup\,\mathtt{OPAR}}\left(s\right)}-{\mathtt{val}^{{\mathcal{M}}}_{\operatorname{\mathtt{Loss}}}\left(s\right)}\leq\varepsilon$
where
$N\stackrel{{\scriptstyle\text{{\tiny{def}}}}}{{=}}\max\left(h,\lceil\log_{c}\left(\varepsilon\cdot\left(1-c\right)\right)\rceil\right)\in{\mathcal{O}}\left(\exp(\lvert{\mathcal{M}}\rvert^{\mathcal{O}(1)})\cdot\log\left(1/\varepsilon\right)\right)$.

For rewards in binary we have
$N\in{\mathcal{O}}\left(\exp(\exp(\lvert{\mathcal{M}}\rvert^{\mathcal{O}(1)}))\cdot\log\left(1/\varepsilon\right)\right)$,
i.e., the size of $N$ increases by one exponential.

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

For rewards in unary, the result follows from Lemma 5.1(Equation 3) and Lemma
5.3. For rewards in binary, the constants increase by one exponential via
encoding binary rewards into unary rewards in a modified MDP.

###  5.2 Computing $N$ for SSGs

In order to compute the bound $N$ for an SSG ${\mathcal{G}}$, we first
consider bounds $N(s)$ for individual states $s$ and then take their maximum.
Given a state $s$, we can use Theorem 4.4(Item 3) to obtain an optimal FD
strategy (with $\mathcal{O}(\exp(|{\mathcal{G}}|^{\mathcal{O}(1)}))$ memory
modes) $\sigma^{*}(s)=\left({\sf M},{\sf m}_{0},{\sf upd},{\sf nxt}\right)$
for Maximizer from state $s$ w.r.t. the $\operatorname{\mathtt{Gain}}$
objective. Theorem 4.4(Item 1) yields a uniform MD strategy $\pi^{*}$ that is
optimal for Minimizer from all states $s$ w.r.t. the
$\operatorname{\mathtt{Gain}}$ objective.

######  Lemma 5.6.

Given an SSG
${\mathcal{G}}=\left(S,(S_{\Box},S_{\Diamond},S_{\ocircle}),{E},P\right)$ and
$\varepsilon>0$, we can compute a number $N\in\mathbb{N}$ such that for all
$i\geq N$ and states $s\in S$ we have

${\mathtt{val}^{{\mathcal{G}}}_{\mathtt{EN}(i)\,\cap\,\mathtt{EPAR}}\left(s\right)}-\varepsilon\leq{\mathtt{val}^{{\mathcal{G}}}_{\operatorname{\mathtt{Gain}}}\left(s\right)}-\varepsilon\leq\inf_{\pi}\mathcal{P}^{{\mathcal{G}}}_{\sigma^{*}(s),\pi,s}\left(\mathtt{EN}(i)\,\cap\,\mathtt{EPAR}\right)\leq{\mathtt{val}^{{\mathcal{G}}}_{\mathtt{EN}(i)\,\cap\,\mathtt{EPAR}}\left(s\right)}$
(4)

i.e., $\sigma^{*}(s)$ is $\varepsilon$-optimal for Maximizer for
$\mathtt{EN}(i)\,\cap\,\mathtt{EPAR}$ for all $i\geq N$. In particular,
$0\leq{\mathtt{val}^{{\mathcal{G}}}_{\operatorname{\mathtt{Gain}}}\left(s\right)}-{\mathtt{val}^{{\mathcal{G}}}_{\mathtt{EN}(i)\,\cap\,\mathtt{EPAR}}\left(s\right)}\leq\varepsilon$.

Moreover, $\pi^{*}$ is $\varepsilon$-optimal for Minimizer from any state $s$
for $i\geq N$.

$\sup_{\sigma}\mathcal{P}^{{\mathcal{G}}}_{\sigma,\pi^{*},s}\left(\mathtt{EN}(i)\,\cap\,\mathtt{EPAR}\right)\leq\sup_{\sigma}\mathcal{P}^{{\mathcal{G}}}_{\sigma,\pi^{*},s}\left(\operatorname{\mathtt{Gain}}\right)={\mathtt{val}^{{\mathcal{G}}}_{\operatorname{\mathtt{Gain}}}\left(s\right)}\leq{\mathtt{val}^{{\mathcal{G}}}_{\mathtt{EN}(i)\,\cap\,\mathtt{EPAR}}\left(s\right)}+\varepsilon$
(5)

For rewards in unary, $N$ is doubly exponential, i.e.,
$N\in{\mathcal{O}}\left(\exp(\exp(\lvert{\mathcal{G}}\rvert^{\mathcal{O}(1)}))\cdot\log\left(1/\varepsilon\right)\right)$
and it can be computed in exponential time. For rewards in binary, the size of
$N$ and its computation time increase by one exponential, respectively.

######  Proof 5.7.

Assume that rewards are in unary. The first inequality of (4) holds because
$\mathtt{EN}(i)\,\cap\,\mathtt{EPAR}\subseteq\operatorname{\mathtt{Gain}}$ for
any $i$. The third inequality of (4) follows from the definition of the value.
Towards the second inequality of (4), we consider the minimizing MDP
${\mathcal{M}}(s)\stackrel{{\scriptstyle\text{{\tiny{def}}}}}{{=}}{\mathcal{G}}^{\sigma^{*}(s)}$
obtained by fixing the Maximizer strategy $\sigma^{*}(s)$. Since
$\sigma^{*}(s)$ is optimal for Maximizer from state $s$ wrt. the objective
$\operatorname{\mathtt{Gain}}$, Lemma 4.3 yields that

${\mathtt{val}^{{\mathcal{G}}}_{\operatorname{\mathtt{Gain}}}\left(s\right)}={\mathtt{val}^{{\mathcal{M}}(s)}_{\operatorname{\mathtt{Gain}}}\left(\left({\sf
m}_{0},s\right)\right)}.$ (6)

Since $\sigma^{*}(s)$ has
$\mathcal{O}(\exp(|{\mathcal{G}}|^{\mathcal{O}(1)}))$ memory modes, the size
of ${\mathcal{M}}(s)$ is exponential in $|{\mathcal{G}}|$ and
${\mathcal{M}}(s)$ can be computed in exponential time.

Now we consider the dual maximizing MDP ${\mathcal{M}}(s)^{d}$ and the
objectives $\operatorname{\mathtt{Term}}(i)\,\cup\,\mathtt{OPAR}$ and
$\operatorname{\mathtt{Loss}}$. (Note that ${\mathcal{M}}(s)^{d}$ has the same
size as ${\mathcal{M}}(s)$.) From Lemma 5.4, we obtain a bound
$N(s)\in\mathbb{N}$ such that for all $i\geq N(s)$

$0\leq{\mathtt{val}^{{\mathcal{M}}(s)^{d}}_{\operatorname{\mathtt{Term}}(i)\,\cup\,\mathtt{OPAR}}\left(\left({\sf
m}_{0},s\right)\right)}-{\mathtt{val}^{{\mathcal{M}}(s)^{d}}_{\operatorname{\mathtt{Loss}}}\left(\left({\sf
m}_{0},s\right)\right)}\leq\varepsilon.$ (7)

By Lemma 5.4 and Lemma 5.3, $N(s)$ is exponential in $|{\mathcal{M}}(s)^{d}|$
and thus doubly exponential in $|{\mathcal{G}}|$, i.e.,
$N(s)\in{\mathcal{O}}\left(\exp(\exp(\lvert{\mathcal{G}}\rvert^{\mathcal{O}(1)}))\cdot\log\left(1/\varepsilon\right)\right)$.
Moreover, $N(s)$ can be computed in time polynomial in
$|{\mathcal{M}}(s)^{d}|$ and thus in time exponential in $|{\mathcal{G}}|$. By
duality, we can rewrite Equation 7 for ${\mathcal{M}}(s)$ as follows. For all
$i\geq N(s)$

$0\leq{\mathtt{val}^{{\mathcal{M}}(s)}_{\operatorname{\mathtt{Gain}}}\left(\left({\sf
m}_{0},s\right)\right)}-{\mathtt{val}^{{\mathcal{M}}(s)}_{\mathtt{EN}(i)\,\cap\,\mathtt{EPAR}}\left(\left({\sf
m}_{0},s\right)\right)}\leq\varepsilon.$ (8)

In order to get a uniform upper bound that holds for all states, let
$N\stackrel{{\scriptstyle\text{{\tiny{def}}}}}{{=}}\max_{s\in S}N(s)$. Since
$|S|$ is linear, we still have
$N\in{\mathcal{O}}\left(\exp(\exp(\lvert{\mathcal{G}}\rvert^{\mathcal{O}(1)}))\cdot\log\left(1/\varepsilon\right)\right)$
and it can be computed in exponential time in $|{\mathcal{G}}|$. Finally, we
can show the second inequality of (4).

$\displaystyle\inf_{\pi}\mathcal{P}^{{\mathcal{G}}}_{\sigma^{*}(s),\pi,s}\left(\mathtt{EN}(i)\,\cap\,\mathtt{EPAR}\right)$
$\displaystyle=\inf_{\pi}\mathcal{P}^{{\mathcal{M}}(s)}_{\pi,\left({\sf
m}_{0},s\right)}\left(\mathtt{EN}(i)\,\cap\,\mathtt{EPAR}\right)$
$\displaystyle={\mathtt{val}^{{\mathcal{M}}(s)}_{\mathtt{EN}(i)\,\cap\,\mathtt{EPAR}}\left(\left({\sf
m}_{0},s\right)\right)}$
$\displaystyle\geq{\mathtt{val}^{{\mathcal{M}}(s)}_{\operatorname{\mathtt{Gain}}}\left(\left({\sf
m}_{0},s\right)\right)}-\varepsilon$ by $i\geq N\geq N(s)$ and Equation 8
$\displaystyle={\mathtt{val}^{{\mathcal{G}}}_{\operatorname{\mathtt{Gain}}}\left(s\right)}-\varepsilon$
by (6)

The first inequality of (5) holds because
$\mathtt{EN}(i)\,\cap\,\mathtt{EPAR}\subseteq\operatorname{\mathtt{Gain}}$ for
any $i$. The equality in (5) holds by the optimality of $\pi^{*}$. The second
inequality of (5) follows from the previously stated consequence of (4).

For rewards in binary, the sizes of the numbers $N(s)$ (and hence $N$) and the
time to compute it increase by one exponential by Lemma 5.4.

##  6 Unfolding the Game to Energy Level $N$

Given an SSG
${\mathcal{G}}=\left(S,(S_{\Box},S_{\Diamond},S_{\ocircle}),{E},P\right)$ and
error tolerance $\varepsilon>0$, for each state $s\in S$ and energy level
$i\geq 0$, we want to compute a rational number $v^{\prime}$ which satisfies
$0\leq
v^{\prime}-{\mathtt{val}^{{\mathcal{G}}}_{\mathtt{EN}(i)\,\cap\,\mathtt{EPAR}}\left(s\right)}\leq\varepsilon$,
and $\varepsilon$-optimal FD strategies $\sigma_{\varepsilon}$ and
$\pi_{\varepsilon}$ for Maximizer and Minimizer, resp. We achieve this by
constructing a finite-state parity game ${\mathcal{G}}^{\prime}$ that closely
approximates the original game ${\mathcal{G}}$, as described in Section 3(Item
3).

For clarity, we explain the construction in two steps. In the first step, we
consider a finite-state parity game ${\mathcal{G}}\left[N\right]$. (Unlike
${\mathcal{G}}^{\prime}$, the game ${\mathcal{G}}\left[N\right]$ is not
actually constructed. It just serves as a part of the correctness proof.)
${\mathcal{G}}\left[N\right]$ encodes the energy level up-to $N+R$ (where $R$
is the maximal transition reward) into the states, i.e., it has states of the
form $(s,k)$ with $k\leq N+R$. It imitates the original game ${\mathcal{G}}$
till energy level $N+R$, but at any state $\left(s,i\right)$ with energy level
$i\geq N$ it jumps to a winning state with probability
${\mathtt{val}^{{\mathcal{G}}}_{\mathtt{EN}(i)\,\cap\,\mathtt{EPAR}}\left(s\right)}$
and to a losing state with probability
$1-{\mathtt{val}^{{\mathcal{G}}}_{\mathtt{EN}(i)\,\cap\,\mathtt{EPAR}}\left(s\right)}$.
(We need the margin up-to $N+R$, because transitions can have rewards $>1$, so
the level $N$ might not be hit exactly.) Similarly, at states
$\left(s,0\right)$ with energy level $0$, we jump to a losing state. The
coloring function in the new game ${\mathcal{G}}\left[N\right]$ derives its
colors from the colors in the original game ${\mathcal{G}}$, i.e., all states
$\left(s,i\right)$ have the same color as $s$ in ${\mathcal{G}}$.

By construction of ${\mathcal{G}}\left[N\right]$, for $i\leq N$, the
$\mathtt{EPAR}$ value of $\left(s,i\right)$ in ${\mathcal{G}}\left[N\right]$
coincides with
${\mathtt{val}^{{\mathcal{G}}}_{\mathtt{EN}(i)\,\cap\,\mathtt{EPAR}}\left(s\right)}$.

In the second step, since we do not know the exact values
${\mathtt{val}^{{\mathcal{G}}}_{\mathtt{EN}(i)\,\cap\,\mathtt{EPAR}}\left(s\right)}$
for $N+R\geq i>N$, we approximate these by the slightly larger
${\mathtt{val}^{{\mathcal{G}}}_{\operatorname{\mathtt{Gain}}}\left(s\right)}$.
I.e., we modify ${\mathcal{G}}\left[N\right]$ by replacing the probability
values
${\mathtt{val}^{{\mathcal{G}}}_{\mathtt{EN}(i)\,\cap\,\mathtt{EPAR}}\left(s\right)}$
for the jumps to the winning state by
${\mathtt{val}^{{\mathcal{G}}}_{\operatorname{\mathtt{Gain}}}\left(s\right)}$.
Let ${\mathcal{G}}^{\prime}$ be the resulting finite-state parity game. It
follows from Lemma 5.6 that
$0\leq{\mathtt{val}^{{\mathcal{G}}}_{\operatorname{\mathtt{Gain}}}\left(s\right)}-{\mathtt{val}^{{\mathcal{G}}}_{\mathtt{EN}(i)\,\cap\,\mathtt{EPAR}}\left(s\right)}\leq\varepsilon$
for $i\geq N$ and
${\mathtt{Lval}^{{\mathcal{G}}}_{\mathtt{EN}\,\cap\,\mathtt{EPAR}}\left(s\right)}={\mathtt{val}^{{\mathcal{G}}}_{\operatorname{\mathtt{Gain}}}\left(s\right)}$.
Thus ${\mathcal{G}}^{\prime}$ $\varepsilon$-over-approximates
${\mathcal{G}}\left[N\right]$ and ${\mathcal{G}}$, and we obtain the following
lemma.

######  Lemma 6.1.

For all states $s$ and all $0\leq i\leq N$

$\displaystyle{\mathtt{val}^{{\mathcal{G}}\left[N\right]}_{\mathtt{EPAR}}\left(\left(s,i\right)\right)}={\mathtt{val}^{{\mathcal{G}}}_{\mathtt{EN}(i)\,\cap\,\mathtt{EPAR}}\left(s\right)},\mbox{and}$
$\displaystyle
0\leq{\mathtt{val}^{{\mathcal{G}}^{\prime}}_{\mathtt{EPAR}}\left(\left(s,i\right)\right)}-{\mathtt{val}^{{\mathcal{G}}\left[N\right]}_{\mathtt{EPAR}}\left(\left(s,i\right)\right)}\leq\varepsilon.$

Now we are ready to prove the main theorem.

See 3.1

######  Proof 6.2.

For $i>N$ we output
$v^{\prime}={\mathtt{val}^{{\mathcal{G}}}_{\operatorname{\mathtt{Gain}}}\left(s\right)}$,
which satisfies the condition by Lemma 5.6. For $i\leq N$ we output
$v^{\prime}={\mathtt{val}^{{\mathcal{G}}^{\prime}}_{\mathtt{EPAR}}\left(\left(s,i\right)\right)}$,
which satisfies the condition by Lemma 6.1. By Theorem 4.4, the values
${\mathtt{val}^{{\mathcal{G}}}_{\operatorname{\mathtt{Gain}}}\left(s\right)}$
are rational for all states $s$. Therefore all probability values in
${\mathcal{G}}^{\prime}$ are rational and thus the $\mathtt{EPAR}$ values of
all states in ${\mathcal{G}}^{\prime}$ are rational. Hence our numbers
$v^{\prime}$ are always rational.

By Theorem 4.4, the values
${\mathtt{val}^{{\mathcal{G}}}_{\operatorname{\mathtt{Gain}}}\left(s\right)}$
for all states $s\in S$ can be computed in exponential time. By Lemma 5.6,
$N\in{\mathcal{O}}\left(\exp(\exp(\lvert{\mathcal{G}}\rvert^{\mathcal{O}(1)}))\cdot\log\left(1/\varepsilon\right)\right)$
is doubly exponential. Therefore, we can construct ${\mathcal{G}}^{\prime}$ in
${\mathcal{O}}\left(\exp(\exp(\lvert{\mathcal{G}}\rvert^{\mathcal{O}(1)}))\cdot\log\left(1/\varepsilon\right)\right)$
time and space. Questions about the parity values of states in
${\mathcal{G}}^{\prime}$ can be decided in nondeterministic time polynomial in
$|{\mathcal{G}}^{\prime}|$. Thus the numbers $v^{\prime}$ are computed in
2-$\mathsf{NEXPTIME}$.

Towards Item 2, we construct $\varepsilon$-optimal FD strategies
$\sigma_{\varepsilon}$ for Maximizer (resp. $\pi_{\varepsilon}$ for Minimizer)
for $\mathtt{EN}(i)\,\cap\,\mathtt{EPAR}$ in ${\mathcal{G}}$. Let
$\hat{\sigma}$ (resp. $\hat{\pi}$) be optimal MD strategies for Maximizer
(resp. Minimizer) for the objective $\mathtt{EPAR}$ in
${\mathcal{G}}^{\prime}$, which exist by Remark 2.1. Since these strategies
are MD, they can be guessed in nondeterministic time polynomial in the size
$|{\mathcal{G}}^{\prime}|$, and thus in
${\mathcal{O}}\left(\exp(\exp(\lvert{\mathcal{G}}\rvert^{\mathcal{O}(1)}))\cdot\log\left(1/\varepsilon\right)\right)$
nondeterministic time.

Then $\sigma_{\varepsilon}$ plays as follows. While the current energy level
$j$ ($i$ plus the sum of the rewards so far) stays $<N$, then, at any state
$s^{\prime}$, play like $\hat{\sigma}$ at state $(s^{\prime},j)$ in
${\mathcal{G}}^{\prime}$. Once the energy level reaches a value $\geq N$ at
some state $s^{\prime}$ for the first time, then play like
$\sigma^{*}(s^{\prime})$ forever. (Recall that $\sigma^{*}(s^{\prime})$ is the
optimal FD Maximizer strategy for $\operatorname{\mathtt{Gain}}$ from state
$s^{\prime}$ from Section 5.2.) $\sigma_{\varepsilon}$ is
$\varepsilon$-optimal by Lemma 6.1 and Lemma 5.6. It needs to remember the
energy level up-to $N$ while simulating $\hat{\sigma}$. Moreover,
$\sigma^{*}(s^{\prime})$ needs
$\mathcal{O}(\exp(|{\mathcal{G}}|^{\mathcal{O}(1)}))$ memory modes by Theorem
4.4. Finally, it needs to remember the switch from $\hat{\sigma}$ to
$\sigma^{*}(s^{\prime})$. Since
$N\in{\mathcal{O}}\left(\exp(\exp(\lvert{\mathcal{G}}\rvert^{\mathcal{O}(1)}))\cdot\log\left(1/\varepsilon\right)\right)$
dominates the rest, $\sigma_{\varepsilon}$ uses
${\mathcal{O}}\left(\exp(\exp(\lvert{\mathcal{G}}\rvert^{\mathcal{O}(1)}))\cdot\log\left(1/\varepsilon\right)\right)$
memory modes.

Similarly, $\pi_{\varepsilon}$ plays as follows. While the current energy
level $j$ stays $<N$, at any state $s^{\prime}$, play like $\hat{\pi}$ at
state $(s^{\prime},j)$ in ${\mathcal{G}}^{\prime}$. Once the energy level
reaches a value $\geq N$ (at any state) for the first time, then play like
$\pi^{*}$ forever (where $\pi^{*}$ is the uniform optimal MD Minimizer
strategy for $\operatorname{\mathtt{Gain}}$ from Section 5.2.)
$\pi_{\varepsilon}$ is $\varepsilon$-optimal by Lemma 6.1 and Lemma 5.6. While
$\pi^{*}$ is MD and does not use any memory, $\pi_{\varepsilon}$ still needs
to remember the energy level up-to $N$ while simulating $\hat{\pi}$, and thus
it uses
${\mathcal{O}}\left(\exp(\exp(\lvert{\mathcal{G}}\rvert^{\mathcal{O}(1)}))\cdot\log\left(1/\varepsilon\right)\right)$
memory modes.

For rewards in binary, all bounds increase by one exponential via an encoding
of ${\mathcal{G}}$ into an exponentially larger but equivalent game with
rewards in unary.

No nontrivial lower bounds are known on the computational complexity of
approximating
${\mathtt{val}^{{\mathcal{G}}}_{\mathtt{EN}(i)\,\cap\mathtt{EPAR}}\left(s\right)}$.
However, even without the parity part, the problem appears to be hard. The
best known algorithm for approximating the value of the energy objective
(resp. the dual termination objective) runs in $\mathsf{NEXPTIME}$ for SSGs
with rewards in unary [3].

As for lower bounds on the strategy complexity, $\varepsilon$-optimal
Maximizer strategies need at least an exponential number of memory modes (for
any $0<\varepsilon<1$) even in maximizing MDPs. This can easily be shown by
extending the example in Lemma 4.1(Item 2) and [24, Fig. 1 and Prop. 4] that
shows the lower bound for the $\operatorname{\mathtt{Gain}}$ objective. First
loop in a state with an unfavorable color to accumulate a sufficiently large
reward (depending on $\varepsilon$) and then switch to the MDP in [24, Fig. 1
and Prop. 4] to play for $\operatorname{\mathtt{Gain}}$ (since
$\mathtt{EN}(i)\,\cap\,\mathtt{EPAR}$ will be very close to
$\operatorname{\mathtt{Gain}}$ then). Even the latter part requires
exponentially many memory modes.

##  7 Conclusion & Extensions

We gave a procedure to compute $\varepsilon$-approximations of the value of
combined energy-parity objectives in SSGs. The decidability of questions about
the exact values is open, but the problem is at least as hard as the
positivity problem for linear recurrence sequences [31, Section 5.2.3]. Unlike
almost surely winning Maximizer strategies which require infinite memory in
general [28, 29], $\varepsilon$-optimal strategies for either player require
only finite memory with at most doubly exponentially many memory modes.

An interesting topic for further study is whether these results can be
extended to other combined objectives where the parity part is replaced by
something else, i.e., energy-X for some objective X (e.g., some other color-
based condition like Rabin/Streett, or a quantitative objective about multi-
dimensional transition rewards). While our proofs are not completely specific
to parity, they do use many strong properties that parity satisfies.

  * •

Shift-invariance of $\mathtt{EPAR}$ is used in several places, e.g. in Lemma
5.1 (and thus its consequences) and for the correctness of the constructions
in Section 6.

  * •

We use the fact that $\mathtt{EPAR}$ goes well together with
$\mathtt{LimInf}(>-\infty)$, i.e., the objective
$\operatorname{\mathtt{Gain}}=\mathtt{LimInf}(>-\infty)\,\cap\,\mathtt{EPAR}$
allows optimal FD strategies for Maximizer in MDPs; cf. Lemma 4.1.

  * •

The submixing property of $\mathtt{OPAR}=\overline{\mathtt{EPAR}}$ is used in
Theorem 4.4 to lift Lemma 4.1 from MDPs to SSGs.

## References

  * [1] Rajeev Alur, Thomas A Henzinger, and Orna Kupferman.  Alternating-time temporal logic.  Journal of the ACM, 49(5):672–713, 2002.
  * [2] Patrick Billingsley.  Probability and measure.  John Wiley & Sons, 2008.
  * [3] T. Brázdil, V. Brožek, K. Etessami, and A. Kučera.  Approximating the Termination Value of One-Counter MDPs and Stochastic Games.  Information and Computation, 222:121–138, 2013.  URL: https://arxiv.org/abs/1104.4978.
  * [4] T. Brázdil, A. Kučera, and P. Novotný.  Optimizing the expected mean payoff in energy Markov decision processes.  In International Symposium on Automated Technology for Verification and Analysis (ATVA), volume 9938 of LNCS, pages 32–49, 2016\.
  * [5] Tomás Brázdil, Václav Brozek, and Kousha Etessami.  One-Counter Stochastic Games.  In Kamal Lodaya and Meena Mahajan, editors, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010), volume 8 of Leibniz International Proceedings in Informatics (LIPIcs), pages 108–119, Dagstuhl, Germany, 2010. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik.  Full version at http://arxiv.org/abs/1009.5636.  URL: http://drops.dagstuhl.de/opus/volltexte/2010/2857, doi:10.4230/LIPIcs.FSTTCS.2010.108.
  * [6] Arindam Chakrabarti, Luca De Alfaro, Thomas A Henzinger, and Mariëlle Stoelinga.  Resource interfaces.  In International Workshop on Embedded Software, pages 117–133, 2003\.
  * [7] Krishnendu Chatterjee and Laurent Doyen.  Energy parity games.  In International Colloquium on Automata, Languages and Programming (ICALP), volume 6199 of LNCS, pages 599–610, 2010.
  * [8] Krishnendu Chatterjee and Laurent Doyen.  Energy and mean-payoff parity Markov decision processes.  In International Symposium on Mathematical Foundations of Computer Science (MFCS), volume 6907, pages 206–218, 2011.
  * [9] Krishnendu Chatterjee and Laurent Doyen.  Games and Markov decision processes with mean-payoff parity and energy parity objectives.  In Mathematical and Engineering Methods in Computer Science (MEMICS), volume 7119 of LNCS, pages 37–46. Springer, 2011.
  * [10] Krishnendu Chatterjee, Laurent Doyen, Hugo Gimbert, and Youssouf Oualhadj.  Perfect-information stochastic mean-payoff parity games.  In International Conference on Foundations of Software Science and Computational Structures (FoSSaCS), volume 8412 of LNCS, 2014.
  * [11] Krishnendu Chatterjee, Thomas A. Henzinger, and Nir Piterman.  Generalized parity games.  In Helmut Seidl, editor, International Conference on Foundations of Software Science and Computational Structures (FoSSaCS), volume 4423 of LNCS, pages 153–167. Springer, 2007.  URL: https://doi.org/10.1007/978-3-540-71389-0_12, doi:10.1007/978-3-540-71389-0\\_12.
  * [12] Krishnendu Chatterjee, Marcin Jurdziński, and Thomas A. Henzinger.  Simple stochastic parity games.  In Computer Science Logic (CSL), volume 2803 of LNCS, pages 100–113. Springer, 2003.
  * [13] Krishnendu Chatterjee, Marcin Jurdziński, and Thomas A. Henzinger.  Quantitative stochastic parity games.  In ACM-SIAM Symposium on Discrete Algorithms (SODA), pages 121–130. SIAM, 2004.
  * [14] E.M. Clarke, O. Grumberg, and D. Peled.  Model Checking.  MIT Press, Dec. 1999.
  * [15] Anne Condon.  The complexity of stochastic games.  Information and Computation, 96(2):203–224, 1992.  doi:https://doi.org/10.1016/0890-5401(92)90048-K.
  * [16] Laure Daviaud, Martin Jurdziński, and Ranko Lazić.  A pseudo-quasi-polynomial algorithm for mean-payoff parity games.  In Logic in Computer Science (LICS), pages 325–334, 2018.
  * [17] Luca De Alfaro and Thomas A Henzinger.  Interface automata.  ACM SIGSOFT Software Engineering Notes, 26(5):109–120, 2001.
  * [18] David L. Dill.  Trace theory for automatic hierarchical verification of speed-independent circuits, volume 24.  MIT press Cambridge, 1989.
  * [19] Graham Everest, Alfred Jacobus van der Poorten, Igor Shparlinski, and Thomas Ward.  Recurrence sequences.  ACM, 2003.
  * [20] J. Filar and K. Vrieze.  Competitive Markov Decision Processes.  Springer, 1997.
  * [21] Dean Gillette.  Stochastic games with zero stop probabilities.  Contributions to the Theory of Games, 3:179–187, 1957.
  * [22] Hugo Gimbert and Florian Horn.  Solving simple stochastic tail games.  In ACM-SIAM Symposium on Discrete Algorithms (SODA), pages 847–862, 2010.  URL: http://epubs.siam.org/doi/abs/10.1137/1.9781611973075.69.
  * [23] Hugo Gimbert and Edon Kelmendi.  Submixing and shift-invariant stochastic games.  2022\.  URL: https://arxiv.org/abs/1401.6575.
  * [24] Hugo Gimbert, Youssouf Oualhadj, and Soumya Paul.  Computing optimal strategies for Markov decision processes with parity and positive-average conditions.  2011\.  URL: https://hal.science/hal-00559173/en/.
  * [25] Marcin Jurdziński.  Deciding the winner in parity games is in UP $\cap$ co-UP.  Information Processing Letters, 68(3):119–124, 1998.
  * [26] A. Maitra and W. Sudderth.  Stochastic games with Borel payoffs.  In Stochastic Games and Applications, pages 367–373. Kluwer, Dordrecht, 2003.
  * [27] Donald A. Martin.  The determinacy of Blackwell games.  Journal of Symbolic Logic, 63(4):1565–1581, 1998.
  * [28] Richard Mayr, Sven Schewe, Patrick Totzke, and Dominik Wojtczak.  MDPs with Energy-Parity Objectives.  In Logic in Computer Science (LICS). IEEE, 2017.  URL: https://arxiv.org/abs/1701.02546.
  * [29] Richard Mayr, Sven Schewe, Patrick Totzke, and Dominik Wojtczak.  Simple stochastic games with almost-sure energy-parity objectives are in NP and coNP.  In Proc. of Fossacs, volume 12650 of LNCS, 2021.  Extended version on arXiv.  URL: https://arxiv.org/abs/2101.06989.
  * [30] Joël Ouaknine and James Worrell.  On linear recurrence sequences and loop termination.  ACM SIGLOG News, 2(2):4–13, 2015.
  * [31] Jakob Piribauer.  On non-classical stochastic shortest path problems.  PhD thesis, Technische Universität Dresden, Germany, 2021.  URL: https://nbn-resolving.org/urn:nbn:de:bsz:14-qucosa2-762812.
  * [32] Jakob Piribauer and Christel Baier.  On Skolem-Hardness and Saturation Points in Markov Decision Processes.  In Artur Czumaj, Anuj Dawar, and Emanuela Merelli, editors, Proc. of ICALP, volume 168 of LIPIcs, pages 138:1–138:17, Dagstuhl, Germany, 2020. Schloss Dagstuhl–Leibniz-Zentrum für Informatik.  URL: https://drops.dagstuhl.de/opus/volltexte/2020/12545, doi:10.4230/LIPIcs.ICALP.2020.138.
  * [33] Jakob Piribauer and Christel Baier.  Positivity-hardness results on Markov decision processes.  2023\.  URL: https://arxiv.org/abs/2302.13675v1.
  * [34] Amir Pnueli and Roni Rosner.  On the synthesis of a reactive module.  In Annual Symposium on Principles of Programming Languages (POPL), pages 179–190, 1989.
  * [35] Peter J. Ramadge and W. Murray Wonham.  Supervisory control of a class of discrete event processes.  SIAM journal on control and optimization, 25(1):206–230, 1987.
  * [36] Lloyd S. Shapley.  Stochastic games.  Proceedings of the national academy of sciences, 39(10):1095–1100, 1953.
  * [37] W. Zielonka.  Infinite games on finitely coloured graphs with applications to automata on infinite trees.  Theoretical Computer Science, 200(1-2):135–183, 1998.

##  Appendix A Appendix for Section 4

######  Definition A.1.

Given an SSG
${\mathcal{G}}=\left(S,(S_{\Box},S_{\Diamond},S_{\ocircle}),{E},P\right)$ and
a finite memory deterministic (FD) strategy $\pi=\left({\sf M},{\sf
m}_{0},{\sf upd},{\sf nxt}\right)$ for Minimizer let ${\mathcal{G}}_{\pi}$ be
the maximizing MDP with state space ${\sf M}\times S$ obtained by fixing
Minimizer’s choices according to $\pi$. The transition rules
${\longrightarrow}^{\prime}$ in the derived MDP ${\mathcal{G}}_{\pi}$ are
given as follows.

  1. 1.

If $s\in S_{\Box}$ for every $(s,s^{\prime})\in{E}$, ${\sf m}\in{\sf M}$, we
have $({\sf m},s)\,{\longrightarrow}^{\prime}\,({\sf upd}({\sf
m},(s,s^{\prime})),s^{\prime})$, i.e., Maximizer determines the successor
state and Minimizer updates its memory according to the observed transition.

  2. 2.

Similarly if $s\in S_{\ocircle}$ for every $(s,s^{\prime})\in{E}$, ${\sf
m}\in{\sf M}$ we have $({\sf m},s)\,{\longrightarrow}^{\prime}\,({\sf
upd}({\sf m},(s,s^{\prime})),s^{\prime})$ and $P(({\sf m},s))(({\sf upd}({\sf
m},(s,s^{\prime})),s^{\prime}))=P(s)(s^{\prime})$, i.e., transition
probabilities are inherited and Minimizer’s memory is updated according to the
observed transition.

  3. 3.

If $s\in S_{\Diamond}$ then $({\sf m},s)\,{\longrightarrow}^{\prime}\,({\sf
upd}({\sf m},(s,s^{\prime})),s^{\prime})$ where $s^{\prime}={\sf nxt}({\sf
m},s)$, i.e., Minimizer chooses the successor state according to the strategy
$\pi$ and updates its memory accordingly.

The reward of each transition is the same as the reward of the transition in
${\mathcal{G}}$ from which it is derived. Similarly for the priorities (aka
coloring) of the states. The ownership of the vertices $({\sf m},s)$ in
${\mathcal{G}}_{\pi}$ is as follows. If $s\in S_{\Box}$ then $({\sf m},s)$
belongs to Maximizer. If $s\in S_{\ocircle}$ then $({\sf m},s)$ is also a
chance vertex. If $s\in S_{\Diamond}$ then $({\sf m},s)$ also becomes a chance
vertex (with exactly one successor), since Minimizer’s choice has been fixed.

In the dual case where a FD strategy $\sigma$ for Maximizer is fixed, we
obtain a minimizing MDP ${\mathcal{G}}^{\sigma}$. The construction is the same
as above, with the roles of Minimizer and Maximizer swapped.

##  Appendix B Appendix for Section 5

See 5.4

######  Proof B.1.

By Lemma 5.1(Equation 3) and Lemma 5.3, we have

${\mathtt{val}^{{\mathcal{M}}}_{\operatorname{\mathtt{Term}}(i)\,\cup\,\mathtt{OPAR}}\left(s\right)}-{\mathtt{val}^{{\mathcal{M}}}_{\operatorname{\mathtt{Loss}}}\left(s\right)}\leq\sup_{\sigma}\mathcal{P}_{\sigma,s}\left(\operatorname{\mathtt{Term}}(i)\,\cap\,\overline{{\sf
F}\,W_{1}}\right)\leq\frac{c^{i}}{1-c}$

for all $i\geq h$ and $s\in S$. To obtain a bound $N\geq h$ with
$\frac{c^{N}}{1-c}\leq\varepsilon$, it suffices to choose

$N\stackrel{{\scriptstyle\text{{\tiny{def}}}}}{{=}}\max\left(h,\lceil\log_{c}\left(\varepsilon\cdot\left(1-c\right)\right)\rceil\right).$

We observe that
$\log_{c}\left(\varepsilon\cdot\left(1-c\right)\right)=-\ln\left(\varepsilon\cdot\left(1-c\right)\right)\cdot(-\ln(c)^{-1})$.
However, $-\ln(c)=-\ln(1-(1-c))\geq(1-c)$. Thus
$\log_{c}\left(\varepsilon\cdot\left(1-c\right)\right)\leq\ln\left(\frac{1}{\varepsilon}\cdot\frac{1}{1-c}\right)\cdot\frac{1}{1-c}$.
For rewards in unary, by Lemma 5.3, we have
$1/(1-c)\in{\mathcal{O}}\left(\exp(\lvert{\mathcal{M}}\rvert^{\mathcal{O}(1)})\right)$
and $h$ is only
${\mathcal{O}}(\exp\left(\lvert{\mathcal{M}}\rvert^{{\mathcal{O}}(1)}\right))$.
Thus
$N\in{\mathcal{O}}\left(\exp(\lvert{\mathcal{M}}\rvert^{\mathcal{O}(1)})\cdot\log\left(1/\varepsilon\right)\right)$.

Now consider the case where rewards are given in binary. Following the proof
of [3, Lemma 3.9], the bounds are derived from the size of solutions of the
constructed linear program. While the MDPs in [3] only consider unary rewards
from $\left\\{-1,0,1\right\\}$, one can extend it to the case where the
rewards come from the set $\left\\{-R,\dots,0,\dots,R\right\\}$ in a natural
way. This affects the complexity of the above computed constants and thereby
size of $N$. More precisely, the proof of Lemma 5.3 can be split into three
steps. Firstly, given an MDP ${\mathcal{M}}$ construct a new “rising” MDP
${\mathcal{M}}^{\prime}$. Then from this derived ${\mathcal{M}}^{\prime}$,
construct a linear program. From the solutions of constructed LP, compute the
required $c$ and $h$. We evaluate the effect of having non-unary rewards in
each of these steps.

When rewards are given in unary, the resulting ${\mathcal{M}}^{\prime}$ has
overall size $\lvert{\mathcal{M}}^{\prime}\rvert\leq
10\lvert{\mathcal{M}}\rvert^{4}$. More exactly, $\lvert S^{\prime}\rvert\leq
10*\lvert S\rvert^{3}*\left(\lvert S\rvert+\lvert{E}\rvert\right)$ and
similarly for $\lvert{E}^{\prime}\rvert$. When the rewards are given in
binary, the construction results in an additional $R^{2}$ factor. So the
resulting ${\mathcal{M}}^{\prime}$ is pseudo-polynomially big when compared to
${\mathcal{M}}$ in our case.

The constructed LP (cf. [3, Fig.1]) has $S^{\prime}+2$ variables ($z_{s}$ for
each state, $x$ for the mean payoff and $\xi$ for converting the constraint
$x>0$ to $x\geq\xi$). Moreover all variables can be assumed non-negative. The
number of constraints is bounded by ${E}^{\prime}+1$. Furthermore all the
constants appearing in the constraints are either constants in the original
MDP ${\mathcal{M}}$ or 1 or 0.

Finally, from an optimal solution of the LP $\left(z_{s},x,\xi\right)$ one can
compute $\exp\left(\frac{-x^{2}}{2\cdot(z_{\max}+x+R)^{2}}\right)$ and to get
$c$, then take a rational over-approximation and also take $h$ as $\lceil
z_{\max}\rceil$ where
$z_{\max}\stackrel{{\scriptstyle\text{{\tiny{def}}}}}{{=}}\max_{s\in
S^{\prime}}z_{s}-\min_{s\in S^{\prime}}z_{s}$. The only difference compared to
the unary rewards case here is that the one step change of the submartingale
is bounded by $z_{\max}+x+R$ instead of $z_{\max}+x+1$.

From the complexity point of view, both the construction of the LP and the
computation from its optimal solutions aren’t affected by changes in the
rewards, i.e., the previous bounds for $c$, $h$ and $N$ in terms of
$\lvert{\mathcal{M}}^{\prime}\rvert$ still hold. In particular,
$c\in{\mathcal{O}}\left(\exp\left(1/2^{\lvert{\mathcal{M}}^{\prime}\rvert^{{\mathcal{O}}(1)}}\right)\right)$,
$h\in{\mathcal{O}}(\exp\left(\lvert{\mathcal{M}}^{\prime}\rvert^{{\mathcal{O}}(1)}\right))$
and thus
$N\in{\mathcal{O}}\left(\exp\left(\lvert{\mathcal{M}}^{\prime}\rvert^{{\mathcal{O}}(1)}\right)\cdot\log\left(1/\varepsilon\right)\right)$
by [3, Claim 6].

While previously, ${\mathcal{M}}^{\prime}$ is only polynomially larger than
${\mathcal{M}}$, introducing binary rewards blows up the construction (cf. [3,
Appendix A.2]). As a result we have that
$\lvert{\mathcal{M}}^{\prime}\rvert\in{\mathcal{O}}\left(2^{\lvert{\mathcal{M}}\rvert^{{\mathcal{O}}(1)}}\right)$.
Therefore $N$ can be doubly exponential in the size of the original MDP
${\mathcal{M}}$, i.e.,
$N\in{\mathcal{O}}\left(\exp(\exp(\lvert{\mathcal{M}}\rvert^{\mathcal{O}(1)}))\cdot\log\left(1/\varepsilon\right)\right)$.

##  Appendix C Appendix for Section 6

######  Definition C.1 (Definition of ${\mathcal{G}}\left[N\right]$).

We present formally the definition of the game ${\mathcal{G}}\left[N\right]$,
which unfolds the energy level in ${\mathcal{G}}$ till $N$

${\mathcal{G}}\left[N\right]=\left(S\left[N\right],\left(S_{\Box}\left[N\right],S_{\Diamond}\left[N\right],S_{\ocircle}\left[N\right]\right),{E}\left[N\right],P\left[N\right]\right)$

where

  1. 1.

$S\left[N\right]\stackrel{{\scriptstyle\text{{\tiny{def}}}}}{{=}}S\times\left\\{0,\ldots,N+R\right\\}\uplus\left\\{s_{\mathrm{win}},s_{\mathrm{lose}}\right\\}$,
the set of states is the tuple with the game state and energy level until
$N+R$ as the maximum change in a single step is $R$ and since we are only
interested in energy levels $\leq N$, it suffices to consider till $N+R$.

  2. 2.

$S_{\odot}\left[N\right]\stackrel{{\scriptstyle\text{{\tiny{def}}}}}{{=}}S_{\odot}\times\left\\{1,\ldots,N\right\\}$,
both players control their respective states until energy level $N$. Every
state with energy $>N$ becomes a chance node. Consequently,

  3. 3.

$S_{\ocircle}\left[N\right]\stackrel{{\scriptstyle\text{{\tiny{def}}}}}{{=}}S_{\ocircle}\times\left\\{1,\ldots,N\right\\}\cup
S\times\left\\{0,N+1,\dots,N+R\right\\}\cup\left\\{s_{\mathrm{win}},s_{\mathrm{lose}}\right\\}$,
since the Maximizer loses when the energy level becomes $\leq 0$, we make
these states as a chance vertex which go to a losing loop.

  4. 4.

${E}\left[N\right]$, $P\left[N\right]$

    1. (a)

For $0<i\leq N$,
$\left(s,i\right){\longrightarrow}\left(s^{\prime},\max(0,j)\right)$ iff
$s\stackrel{{\scriptstyle j-i}}{{{\longrightarrow}}}s^{\prime}\in{E}$, this is
just simulating the transitions of the game until energy level $N$ and taking
care of border cases. When energy drops below $0$, we move to level $0$ as
there is no difference. When it shoots above $N$, it cannot go beyond $N+R$
and thus the transition is well defined.

    2. (b)

If $s\in S_{\ocircle}$ above, then the probability is carried over.

    3. (c)

$\left(s,0\right){\longrightarrow}s_{\mathrm{lose}}$ with probability 1.

    4. (d)

$\left(s,N+k\right){\longrightarrow}s_{\mathrm{win}}$ with probability
${\mathtt{val}^{{\mathcal{G}}}_{\mathtt{EN}(N+k)\,\cap\,\mathtt{EPAR}}\left(s\right)}$
and with remaining probability moves to $s_{\mathrm{lose}}$ for $1\leq k\leq
R$

    5. (e)

$s_{\mathrm{lose}}{\longrightarrow}s_{\mathrm{lose}}$ with probability 1.
Similarly for $s_{\mathrm{win}}$.