We consider finite-state Markov decision processes with
the combined Energy-MeanPayoff objective.
The controller tries to avoid running out of energy while simultaneously attaining
a strictly positive mean payoff in a second dimension.

We show that finite memory suffices for almost surely winning strategies for
the Energy-MeanPayoff objective.
This is in contrast to the closely related Energy-Parity objective, where
almost surely winning strategies require infinite memory in general.

We show that exponential memory is sufficient
(even for deterministic strategies)
and necessary
(even for randomized strategies)
almost surely winning Energy-MeanPayoff.
The upper bound holds even
if the strictly positive mean payoff part of the objective
is generalized to multidimensional strictly positive mean payoff.

it is decidable in pseudo-polynomial time whether
an almost surely winning strategy exists.

§ INTRODUCTION

Markov decision processes (MDPs) are a standard model for dynamic systems that
exhibit both stochastic and controlled behavior <cit.>.
MDPs play a prominent role in many domains, e.g., artificial intelligence and machine learning <cit.>, control theory <cit.>, operations research and finance <cit.>, and formal verification <cit.>.

An MDP is a directed graph where states are either controlled or random.
If the current state is controlled then the controller can choose a distribution over all possible successor states.
If the current state is random then the next state is chosen according to a
fixed probability distribution.
One assigns numeric rewards to transitions (and this can be generalized to
multidimensional rewards).
Moreover, priorities (aka colors), encoded by bounded non-negative numbers,
are assigned to states.
By fixing a strategy for the controller and an initial state, one obtains a probability space
of runs of the MDP. The goal of the controller is to optimize the expected value of
some objective function on the runs.

The strategy complexity of a given objective is
the amount of memory (and randomization) needed for an optimal (resp. $\eps$-optimal)
Common cases include memoryless strategies, finite-memory strategies, Markov
strategies (using a discrete clock, aka step counter), and general
infinite-memory strategies.

Related work.

The Parity, MeanPayoff and Energy objectives have been extensively studied in
the formal verification community.
A run satisfies the (min-even) Parity objective iff
the minimal priority that appears infinitely often in the run is even.
It subsumes all $\omega$-regular objectives, and in particular safety,
liveness, fairness, etc.
The MeanPayoff objective requires that the limit average reward per
transition along a run is positive (resp. non-negative in some settings).
MeanPayoff objectives go back to a 1957 paper by Gillette <cit.> and have
been widely studied, due to their relevance for efficient control.
The Energy objective <cit.> requires that the
accumulated reward at any time in a run stays above some finite threshold
(typically $0$).
The intuition is that a controlled system has some finite initial energy level
that must never become depleted.

Combinations of these objectives have also been studied, where the runs need to
satisfy several of the above conditions simultaneously.

The existence of almost surely winning strategies for MeanPayoff-Parity
in MDPs is decidable in polynomial time <cit.>.
These strategies require only finite memory for MeanPayoff $>0$ <cit.>,
but infinite memory for MeanPayoff $\ge 0$ <cit.>.

The existence of almost surely winning strategies for Energy-Parity
in MDPs is decidable in $\NP \cap \coNP$ and in pseudo-polynomial time
<cit.>. (The $\NP \cap \coNP$ upper bound holds even for turn-based
stochastic games <cit.>.)
Almost surely winning strategies in MDPs require only finite memory in the special
case of Energy-Büchi <cit.>, but infinite memory for
Energy-co-Büchi and thus for Energy-Parity <cit.>.
However, $\eps$-optimal strategies for Energy-Parity require only finite
(at most doubly exponential) memory, and the value can be effectively approximated in doubly exponential
time (even for turn-based stochastic games) <cit.>.

The Energy-MeanPayoff objective is similar to Energy-Parity, but
replaces the Parity part by a MeanPayoff objective for a second reward
I.e., one considers an MDP with 2-dimensional transition rewards, where the
Energy condition applies to the first dimension and the MeanPayoff condition
applies to the second dimension. (It can be generalized to higher dimensions $d$,
where the MeanPayoff condition applies to all dimensions $2,3,\dots,d$.)
This might look like a direct generalization of the Energy-Parity objective, since
Parity games are reducible to MeanPayoff games <cit.>.
However, this reduction does not work in the context of these combined
objectives when one considers stochastic systems like MDPs; see below.
Non-stochastic Energy-MeanPayoff games have been studied in <cit.>.

A sightly different objective has been studied in
<cit.> who
consider MDPs with $d$-dimensional rewards, where $d=d_1+d_2$.
The objective requires a strictly positive MeanPayoff
surely in the first $d_1$ dimensions,
and almost surely in the remaining $d_2$ dimensions.
This objective is strictly stronger than Energy-MeanPayoff.
E.g., a MeanPayoff of zero in the first dimension may or may not satisfy the Energy objective,
but it never satisfies the objective in <cit.>.

The objective studied in <cit.> aims to maximize the expected
MeanPayoff (rather than the probability of it being strictly positive)
while satisfying the energy constraint.
However, unlike in our work, the reward function has a single dimension
(i.e., both criteria apply to the same value) and $\eps$-optimal strategies
can require infinite memory.

Our contribution.

We consider the Energy-MeanPayoff objective in MDPs with $d$-dimensional rewards.
The first dimension needs to satisfy the Energy condition (never drop below
$0$), while each other dimension needs to have a strictly positive MeanPayoff.
We show that almost surely winning strategies for Energy-MeanPayoff require
only finite memory.
Our results do not carry over to Energy-MeanPayoff objectives
with non-strict inequalities where
one just requires a MeanPayoff $\ge 0$ almost surely.
This needs infinite memory even for the case of $d=2$,
i.e., one energy-dimension and one MeanPayoff-dimension.
It suffices to modify the counterexample for Energy-co-Büchi from
<cit.> such that a visit to a state with unfavorable color
incurs a reward of $-1$ in the MeanPayoff-dimension.
This is in contrast to the Energy-Parity objective where almost surely winning
strategies require infinite memory in general <cit.>
(even for the simpler Energy-co-Büchi objectives).
This also shows that Energy-Parity is not reducible to Energy-MeanPayoff in
MDPs, unlike the reduction from Parity to MeanPayoff in

We show that almost surely winning strategies for Energy-MeanPayoff,
if they exist, can be chosen as deterministic strategies with
an exponential number of memory modes.
The crucial property is that it suffices to remember the stored energy only up to some
exponential upper bound.
A small counterexample shows the corresponding exponential lower bound.
Even for randomized strategies, an exponential number of memory modes is required,
and this holds even for the case of small transition rewards in $\{-1,0,+1\}$.

Although almost surely winning strategies are `exponentially large'
in this sense,
their existence is still decidable in pseudo-polynomial time; cf. <Ref>.

§ 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$.
$\supp(f) \eqdef$  denotes the support of
$f$ and $\dist(S)$ is the set of all probability distributions over $S$.
Given an alphabet $\Sigma$,
let $\Sigma^{\om}$ and $\Sigma^{*}$ ($\Sigma^+$) denote the set of infinite
and finite (non-empty) sequences over $\Sigma$, respectively.
Elements of $\Sigma^{\om}$ or $\Sigma^*$ are called words.

MDPs and Markov chains.

A Markov Decision Process (MDP) is a controlled stochastic directed graph $\mdp \eqdef \mdptuple$
where the set of vertices $\states$ (also called states) is partitioned into the states $\zstates$ of
the player $\pz$ (Maximizer),
and chance vertices (aka random states) $\rstates$.
Let $\transition \subseteq \states \x \states$ be the transition relation.
We write $\s \movesto \s'$ if $\tuple{\s,\s'} \in \transition$ and
assume that
$\successors{\s} \eqdef \{\s' \mid \s\transition{}\s'\} \neq \emptyset$
for every state $\s$.
The probability function $\probp$
assigns each random state $\s \in \rstates$ a distribution over
its successor states, i.e., $\probp(\s) \in \dist(\successors{\s})$.
We extend the domain of $\probp$ to
$\states^*\rstates$ by $\probp(\partialplay\s) \eqdef \probp(\s)$
for all $\partialplay\s \in \states^+\rstates$.

A Markov chain is an MDP with only random states,
i.e., $\zstates = \emptyset$.
In this paper we consider finite-state MDPs, i.e., the set of states $S$ is finite.

A run is an infinite sequence $\s_0\s_1 \ldots \in \states^{\omega}$
such that $\s_i \movesto \s_{i+1}$ for all $i \ge 0$.
A path is a finite prefix of a run.
Let $\playsof{\mdp} \eqdef \set*{\play = \lrc{q_i}_{i \in \N} \, | q_i \movesto q_{i+1}}$
denote the set of all possible runs.
A strategy of the player $\pz$ is a function
$\zstrat\! : \states^* \zstates \to \dist(\states)$
that assigns to every path
$w\s \in \states^* \zstates$
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 $\pz$ in
$\mdp$ is denoted by $\zallstrats{\mdp}$.
A run/path $\s_0\s_1 \ldots$ is compatible with a strategy
$\zstrat$ if $\s_{i+1} \in \supp(\zstrat(\s_0 \ldots \s_i))$
whenever $\s_i \in \zstates$.

Finite-memory strategies are a subclass of
strategies using a finite set $\memconfset$
of memory modes.
A function $\memsuc : \memconfset \x \zstates \mapsto \dist(\states)$
chooses a (distribution over) successor states based on the current memory
mode and state
$\memup : \memconfset \x \transition \mapsto \dist(\memconfset)$
updates the memory mode upon observing a transition.
Let $\zstrat[\memconf]$ denote the finite-memory strategy $\zstrat$ starting
in memory mode $\memconf$.
The set of all finite-memory strategies in $\mdp$ is denoted by $\zfinstrats{\mdp}$.
Strategies with memory $|\memconfset|=1$ are called memoryless.
Memoryless deterministic (resp. randomized) strategies are called MD (resp. MR).
By fixing some finite-memory strategy $\zstrat$ from some initial state in a finite-state MDP
$\mdp$, we obtain a finite-state Markov chain, denoted by $\mdp^\zstrat$.

An MDP $\mdp$ with initial state $\s_0$ and strategy
$\zstrat$ yields a probability space
$(\s_0\states^{\om},\F_{\s_0}, \Prob[\mdp][\zstrat,\s_0]{})$
where $\F_{\s_0}$ is the $\sigma$-algebra generated by the cylinder sets
$\s_0\s_1\ldots\s_n\states^{\om}$ for $n \ge 0$.

The probability measure $\Prob[\mdp][\zstrat,\s_0]{}$ is
first defined on the cylinder sets.
For $\partialplay = \s_0\ldots\s_n$, let
$\Prob[\mdp][\zstrat,\s_0]{\partialplay} \eqdef 0$ if
$\partialplay$ is not compatible with $\zstrat$ and
$\Prob[\mdp][\zstrat,\s_0]{\partialplay\states^{\om}} \eqdef
\prod_{i=0}^{n-1} \xstrat(\s_0\ldots\s_i)(\s_{i+1}) $ where $\xstrat$
is $\zstrat$ or $\probp$ depending on
whether $\s_i \in \zstates$ or $\rstates$, respectively.
If $\mdp$ is a Markov chain then there is only a single strategy, and we simply
write $\Prob[\mdp][\s_0]{}$.
By Carathéodory's extension
theorem <cit.>, this defines a unique probability
measure on the $\sigma$-algebra.
Given some reward function $v: \s_0\states^{\om} \to \mathbb{R}$,
we write $\expectation[][]{.}$
for the expectation w.r.t. $\probm$ and $v$.

General objectives are defined by real-valued measurable functions.

However, we mostly consider indicator functions of measurable sets.
Hence, our objectives can be described by measurable subsets
$\obj \subseteq \states^{\om}$ of runs starting at a given initial state.
By $\Prob[\mdp][\zstrat,\s]{\obj}$ we denote the
payoff under $\zstrat$, i.e.,
the probability that runs from $\s$ belong to $\obj$.
The value of a state is defined as
$\valueof[\mdp][\obj]{\s} \eqdef \sup_{\zstrat \in \zallstrats{\mdp}} \Prob[\mdp][\zstrat,\s]{\obj}$.
For $\eps > 0$ and state $\s$, a strategy $\zstrat \in \zallstrats{\mdp}$
is $\eps$-optimal iff $\Prob[\mdp][\zstrat,\s]{\obj} \ge \valueof[\mdp][\obj]{\s} - \eps$.
A $0$-optimal strategy is called optimal.
An MD/MR strategy is called uniformly $\eps$-optimal (resp. uniformly optimal)
if it is so from every start state.
An optimal strategy from $\s$ is called almost surely winning if $\valueof[\mdp][\obj]{\s}=1$.
By $\AS\lrc{\obj}$ (resp. $\AS_{\finite}\lrc{\obj}$)
we denote the set of states that have an almost surely winning
strategy (resp. an almost surely winning finite-memory strategy)
for objective $\obj$. For ease of presentation, we drop subscripts and superscripts
wherever possible if they are clear from the context.

We use the syntax and semantics of the LTL operators <cit.>
, $\always$ (always) and $\next$ (next)
to specify some conditions on runs.

A reachability objective is defined by a set of target states
$\reachset \subseteq \states$. A run $\play = \s_0s_1 \ldots$
belongs to $\eventually\,\reachset$ iff $\exists i \in \nat\, \s_i \in \reachset$.
Similarly, $\play$ belongs to $\eventually^{\le n} \reachset$
(resp. $\eventually^{\ge n} \reachset$) iff
$\exists i \le n$ (resp. $i \ge n$) such that $\s_i \in \reachset$.

Dually, the safety objective
$\always\,\reachset$ consists of all runs
which never leave $\reachset$. We have $\always\,\reachset = \neg\eventually\neg\reachset$.

Parity. A parity objective is defined via bounded function
$\coloring: \states \to \nat$ that assigns non-negative priorities
(aka colours) to states. Given an infinite run
$\play = \s_0s_1 \ldots$, let $\text{Inf}(\play)$
denote the set of numbers that occur infinitely often in the sequence
A run $\play$ satisfies even parity
w.r.t. $\coloring$ iff the minimum of $\text{Inf}(\play)$ is even.
Otherwise, $\play$ satisfies odd parity.
The objective even parity is denoted by $\Eparity(\coloring)$
and odd parity is denoted by $\Oparity(\coloring)$.
Most of the time, we implicitly assume that the colouring function is known
and just write $\Eparity$ and $\Oparity$.
Observe that, given any colouring $\coloring$, we have
\complementof{\Eparity} = \Oparity$ and
\Oparity(\coloring) = \Eparity(\coloring + 1)
where $\coloring + 1$ is the function which adds $1$ to the colour 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 \set{-R,\dots,0,\dots,R}$ be a bounded function that assigns rewards
to transitions. Depending on context, the sum of these rewards in a path
can be viewed as energy, cost/profit or a counter.
If $\s \movesto \s'$ and $r((\s,\s')) = c$, we write $\s \energymove{c}
\s'$. Let $\play = \s_0 \energymove{c_0} \s_1 \energymove{c_1} \ldots$ be a run.
We say that $\play$ satisfies

* the $k$-energy objective $\EN{k}$ iff $\lrc{k + \sum_{i=0}^{n-1} c_i} \geq 0$ for all $n \ge 0$.

* the $l$-storage condition $\infix\lrc{l}$ if $l+\sum_{i=m}^{n-1} c_i \ge 0$
holds for every infix $s_m \energymove{c_m} \s_{m+1}\ldots s_n$ of the run.
Let $\ES{k,l}$ denote the set of runs that satisfy both the $k$-energy
and the $l$-storage condition. Let $\ES{k} \eqdef \bigcup_l \ES{k,l}$. Clearly, $\ES{k} \subseteq \EN{k}$.

* Mean payoff $\MP\lrc{\rhd\,c}$ for some constant $c \in \R$
iff $\lrc{\liminf_{n \tendsto \infty}\frac{1}{n}\sum_{i=0}^{n-1} c_i } \rhd\; c$
for $\rhd \in \set{<,\le,=,\ge,>}$.

A different way to consider the energy objective 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 a safety objective.

An objective $\obj$ is called shift-invariant
iff for all finite paths $\partialplay$ and plays $\play' \in \states^{\omega}$,
we have $\partialplay \play' \in \obj \iff \play' \in \obj$.
Mean payoff objectives are shift-invariant, but energy and
storage/infix objectives are not.

Multidimensional reward-based objectives.
Let $\N,\Q,\R$ denote the set of positive integers, rationals and reals respectively. For a $d$-dimensional real vector $\vec{\mu}$, let $\mu_i$
denote the $i^{th}$ component of $\vec{\mu}$ for $1 \leq i \leq d$. Given two vectors $\vec{\mu},\vec{\nu} \in \R^d$, $\sim \in \set{<,\leq,>,\geq,=}$ we say $\vec{\mu} \sim \vec{\nu}$ if $\mu_i
\sim \nu_i$ for every $i$. In particular, $\vec{\mu} > \vec{0}$ means that
every component of $\vec{\mu}$ is strictly greater than $0$.
For a multidimensional reward function
$\vec{r}: \transition \to [-R,R]^d$,
we can consider any boolean combination of reward based objectives using any components of $\vec{r}$. For instance,
$\obj_1 = \en_1(k) \, \cap \MP_2\lrc{> 0}$ denotes the objective that contains all runs that satisfy $\en(k)$ in the $1^{st}$ dimension and $\MP\lrc{> 0}$ in the $2^{nd}$ one.
We denote conjunctions of the same objective across different dimensions in
vectorized form, with the dimension information in the subscript. Therefore,
$\vec{\en_{[a,b]}(\vec{k})} \, \cap \, \vec{\MP_{[c,d]}\lrc{> \vec{x}}}$
denotes the runs where the $\en_i(k_i)$ objective is satisfied for each $i \in [a,b]$
and the $\MP_j\lrc{> x_j}$ objective is satisfied for each $j \in [c,d]$.

Given an infinite run $\play =  \s_0 \energymove{\vec{c_0}} \s_1 \energymove{\vec{c_1}} \ldots$,
let $X_n\lrc{\play} \eqdef \s_n$ denote the $n$-th state.
Let $\vec{Y_n}$ be the sum of the rewards in the first $n$ steps, i.e., $\vec{Y_n}\lrc{\rho} \eqdef \sum_{i=0}^{n-1} \vec{c_i}$.
These become random variables once an initial distribution and a strategy are fixed.

We are concerned with approximating the value for the combined energy-parity
objective $\en(k) \cap \Eparity$ and building $\eps$-optimal strategies.

In our constructions we use some auxiliary objectives.
Following <cit.>, these are defined as
$\Gain \eqdef \LimInf{>}{-\infty}\, \cap\, \Eparity$
$\Loss \eqdef \complementof{\Gain} = \LimInf{=}{-\infty}\, \cup\, \Oparity$.

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

* $\eventually\,\reachset$  <cit.>

* $\LimInf{\rhd}{-\infty}$,
$\MP{>}{0}$  <cit.>

* $\Eparity$  <cit.>

Size of an instance.

Given an MDP $\mdp = \mdptuple$ with reward function
$\vec{r}: \transition \to [-R,R]^d$, its size $|\mdp|$
is the number of bits used to describe it.
Similarly for $|\probp|$.
Transition probabilities and rewards can thus be stored in binary.
We call a size pseudo-polynomial in $|\mdp|$ if it is polynomial for the
case where $R$ is `small', i.e., if $R$ is given in unary.

§ THE MAIN RESULT

Let $\mdp = \mdptuple$ be an MDP with $d$-dimensional rewards on the edges
$\vec{r}: \transition \to [-R,R]^d$.
For the multidimensional Energy-MeanPayoff objective
$\en_1(k)\,\cap\,\vec{\MP_{[2,d]}\lrc{> 0}}$ the following properties hold.

* The existence of an almost-surely winning strategy implies
the existence of an almost-surely winning finite-memory strategy.

* Moreover, a deterministic strategy with an exponential number of memory modes is

* An exponential (in $|P|$) number of memory modes is necessary in general,
even for randomized strategies,
even for
$|\states|=5$, $d=2$ and $R=1$.

In the following three sections we prove items 1.,2.,3. of <Ref>,

Here we sketch the main idea for the upper bound.
Except in a special corner case where the energy fluctuates only in a bounded
region, almost-surely winning strategies for Energy-MeanPayoff
can be chosen among some particular strategies
that alternate between two modes, playing two different memoryless strategies.
This alternation keeps the balance between the Energy-part and the
MeanPayoff-part of the objective.
This is similar to almost-surely winning strategies for the Energy-Parity objective
in <cit.>.
In one mode, one plays a randomized memoryless strategy that almost surely yields a positive
mean payoff in all dimensions (in case of Energy-Parity, instead of mean payoff
it satisfies Parity almost surely). This is called the Gain phase.
Whenever the energy level (the cumulative reward in dimension 1)
gets dangerously close to zero, one switches to the other mode and plays
a different memoryless strategy
that focuses exclusively on getting the energy level up again,
while temporarily neglecting the other part of the objective
(Parity or Mean payoff, respectively). This is called a Bailout.
Once the energy level is sufficiently high, one switches back to the Gain
phase again.
The crucial property is that, except in a null set, only finitely many
Bailouts are required, and thus the temporary neglect of the second part of
the objective does not matter in the long run.
Such a strategy uses infinite memory, because it needs to remember the
unbounded energy level.
For Energy-Parity (and even Energy-co-Büchi) this cannot be avoided
and finite-memory strategies do not work <cit.>.
However, for Energy-MeanPayoff one can relax the requirements somewhat.
Suppose that one records the stored energy only up to a certain bound $b$,
i.e., one forgets about potential excess energy above $b$.
In that case, one might have to do infinitely many Bailouts
with high probability, most of which are unnecessary (but one does not know
which ones). However, for a sufficiently large bound $b$, these superfluous
Bailouts occur so infrequently that they do not compromise the
MeanPayoff-part of the objective.
The critical part of the proof is to show this property and
an upper bound on $b$.
Once this is established, one obtains a finite-memory strategy,
because it suffices to record the energy level only in the
range $[0,b]$ (plus one extra bit of memory to record the current phase, Gain
or Bailout).

Note that the argument above is different from the one that justifies
finite-memory $\eps$-optimal strategies for Energy-Parity in
These also record the energy only in a bounded region, but stop doing Bailouts
after the upper bound has been visited.
I.e., they do too few Bailouts, and thus incur an
$\eps$-chance of losing.
In contrast, our almost-surely winning strategies for
Energy-MeanPayoff rather do too many Bailouts, but sufficiently infrequently
such that they don't compromise the objective.

§ PROOF OF FINITE MEMORY STRATEGY EXISTENCE

W.l.o.g, we assume that every state in
$\mdp$ has an almost surely winning strategy for Energy-MeanPayoff for some
initial energy level. (Otherwise, consider a suitably restricted sub-MDP.)
For conciseness, we denote the objective by
$\obj\lrc{k} \eqdef \en_1(k)\,\cap\,\vec{\MP_{[2,d]}\lrc{> 0}}$.

$$\winset\lrc{\s} \eqdef \setcomp{k}{\s \in \AS\lrc{\obj\lrc{k}}},\quad i_{\s} \eqdef \min\lrc{\winset\lrc{\s}}$$

denote the possible initial energy levels and the minimum initial energy level
such that one can win almost surely from state $\s$.
In particular, $i_{\s}$ is well defined by our assumption on $\mdp$.

Towards a contradiction,
assume that not all configurations are winnable with a finite-memory strategy.
I.e., let $\winset_{\finite}\lrc{\s} \eqdef \setcomp{k}{\s \in
\AS_f\lrc{\obj\lrc{k}}}$ denote the energy levels
from which one can win almost surely with a finite-memory strategy from $\s$,
and assume that there is a state $\s^{\dagger}$ such that
$i_{\s^\dagger} \notin \winset_{\finite}\lrc{\s^{\dagger}}$.
We then construct a finite-memory winning strategy from $\s^{\dagger}$
for $\obj\lrc{i_{\s^\dagger}}$, leading to a contradiction.
Similar to $i_\s$, let $f_\s$ denote the
minimal $k$ such that $k \in \winset_{\finite}\lrc{\s}$ and $\infty$ if there
is no such $k$.

We construct a new MDP $\mdp^\ast$ which abstracts away all the $\winset_{\finite}$ configurations.
At every state $\s$, the player gets the option to enter a
winning sink state if the energy level is sufficiently large to win with
finite memory, i.e., if the current energy level is at least $f_\s$.
The states of the MDP $\mdp^\ast$ will have two copies of each state $\s$ of
$\mdp$, namely $\s$ and $\s^\prime$. Moreover, we add a new state
All states $\s^\prime$ are controlled by $\pz$ and every step
$\s_1 \movesto \s$ in the original MDP $\mdp$ is now mapped to a step
$\s_1 \movesto \s^\prime$ with the same reward
(and the same probability if $\s_1$ was a random state).
In $\s^\prime$, the player has two choices: he can either go to $\s$ with
reward $\vec{0}$ or go to $\s_\textrm{win}$ with reward
$\tuple{-f_\s,\vec{0}}$. The latter choice is only available if $f_\s < \infty$.
$\s_\textrm{win}$ is a winning sink where
$\s_{\textrm{win}} \movesto \s_{\textrm{win}}$ with reward $\vec{1}$, i.e.,
reward $+1$ in all dimensions.

The following lemma shows that the existence of almost surely winning (finite-memory) strategies
coincides in $\mdp^\ast$ and $\mdp$.

Let $\s \in \states$ and $k \in \N$, and consider the objective $\obj\lrc{k}$.
There exists an almost surely winning
strategy $\zstrat^\ast$ from $\s$ in $\mdp^\ast$ if and only if
there exists an almost surely winning
strategy $\zstrat$ from $\s$ in $\mdp$.
Moreover, if $\zstrat^\ast$ is finite-memory then $\zstrat$ can be chosen as
finite-memory, and vice-versa.

Towards the `only if' direction, let $\zstrat^\ast$ be a strategy from $\s$
in $\mdp^\ast$ that is almost surely winning for $\obj\lrc{k}$.
We define a strategy $\zstrat$ from $\s$ in $\mdp$ that plays as follows.
First $\zstrat$ imitates the moves of $\zstrat^\ast$ until (if ever)
$\zstrat^\ast$ chooses a move $\s^\prime_1 \to \s_\textrm{win}$ with non-zero
probability at some state $\s^\prime_1$.
This is possible, since any finite path in $\mdp^\ast$ that does not contain $\s_\textrm{win}$
can be bijectively mapped to a path in $\mdp$. The only difference is that
paths in $\mdp^\ast$ contain extra steps via primed states, which are
skipped in the paths in $\mdp$. Moreover, the transition probabilities at
random states coincide in $\mdp^\ast$ and $\mdp$.
If $\zstrat^\ast$ chooses a move $\s^\prime_1 \to \s_\textrm{win}$ with non-zero
probability at some state $\s^\prime_1$ then the current energy level must
be $\geq f_{\s_1}$, because $\zstrat^\ast$ satisfies the energy objective
almost surely (and thus even surely).
Thus, in $\mdp$, there exists an almost surely winning finite-memory
strategy $\hat{\zstrat}$ for $\obj\lrc{f_{\s_1}}$ from $\s_1$.
In this situation $\zstrat$ continues by playing $\hat{\zstrat}$ from $\s_1$.
Therefore, $\zstrat$ satisfies the energy objective surely.
Moreover, by shift invariance and the properties of $\hat{\zstrat}$,
it also satisfies the Mean payoff objective almost surely.
Thus, $\zstrat$ satisfies $\obj\lrc{k}$ almost surely.
Finally, if $\zstrat^\ast$ is finite-memory then so is $\zstrat$,
because $\hat{\zstrat}$ is also finite-memory.

Towards the `if' direction, let $\zstrat$ be a strategy from $\s$
in $\mdp$ that is almost surely winning for $\obj\lrc{k}$.
We define a strategy $\zstrat^\ast$ from $\s$ in $\mdp^\ast$ that
imitates the moves of $\zstrat$. Moreover, at primed states
$q'$ it always goes to $q$ (and never to $\s_\textrm{win}$).
Since the probabilities at random states coincide in $\mdp^\ast$ and $\mdp$,
also the probabilities of the induced paths coincide.
The only difference is that the runs in $\mdp^\ast$ contain extra steps via
primed states and these extra steps carry reward zero.
Thus, the mean payoff of a run in $\mdp^\ast$ is $1/2$ the mean payoff of the
corresponding run in $\mdp$. However, this does not affect the property that
the mean payoff is $>0$ almost surely in either MDP.
Thus, $\zstrat^\ast$ satisfies $\obj\lrc{k}$ almost surely.
Finally, if $\zstrat$ is finite-memory then so is $\zstrat^\ast$.

The following two technical lemmas establish properties of $\mdp^\ast$
that are used in the proof of <Ref>.

In $\mdp^\ast$, there is no almost surely winning strategy for $\en_1(i_{\s^\dagger}) \, \cap\, \eventually\,\s_{\textrm{win}}$ when starting from $\s^\dagger$.

Recall that $\s^{\dagger}$ has been chosen such that $i_{\s^\dagger} \notin \winset_{\finite}\lrc{\s^{\dagger}}$.
Towards a contradiction, assume that there exists
a strategy $\zstrat_1$ that is almost surely winning for the given objective
in $\mdp^\ast$ from $\s^\dagger$.
We then construct an almost surely winning finite-memory strategy $\zstrat_2$
for $\obj\lrc{i_{\s^\dagger}}$ from $\s^\dagger$ in $\mdp$.
This implies that $i_{\s^\dagger} \in \winset_{\finite}\lrc{\s^{\dagger}}$, a

First we observe that $\zstrat_1$ can be chosen as finite-memory, since even
for the slightly more general Energy- objectives,
almost surely winning strategies can be chosen as finite-memory <cit.>.
Consider the following finite-memory strategy $\zstrat_2$ in $\mdp$ from $\s^{\dagger}$.
It behaves like $\zstrat_1$ until it is just about to enter
$\s_\textrm{win}$ from some state $\s^{\prime}$,
at which point it switches to one of the finite-memory almost surely winning strategies for
$\obj\lrc{f_\s}$ from $\s$.
This is possible, because $\zstrat_1$ is energy safe
and the step to $\s_\textrm{win}$ carries a reward of $-f_\s$.
Thus, $\zstrat_2$ satisfies the Energy objective $\en_1(i_{\s^\dagger})$.
Moreover, the switch almost surely happens, since
$\zstrat_1$ almost surely enters $\s_\textrm{win}$.
By the shift invariance of $\vec{\MP_{[2,d]}\lrc{> 0}}$,
$\zstrat_2$ also satisfies this part of the objective and thus satisfies
$\obj\lrc{i_{\s^\dagger}}$ almost surely.

<Ref> shows that any strategy which satisfies
$\en_1(i_{\s^\dagger})$ almost surely cannot guarantee to visit
$s_{\textrm{win}}$ in $\mdp^{\ast}$.
In other words, looking at it in terms of runs in $\mdp$, when playing an
almost surely winning strategy for $\obj\lrc{i_{\s^\dagger}}$ from $s^\dagger$,
there is always a non-zero chance that one never hits an energy level
$\ge f_\s$ at state $\s$.

The next lemma shows that, in $\mdp^{\ast}$, it is impossible to
satisfy Energy-MeanPayoff from $\s$ with arbitrarily high probability,
unless one also allows arbitrarily large fluctuations in the energy level,
or $f_\s = i_\s$. (Recall that $f_\s, i_\s$ are defined relative to $\mdp$.)

For every state $\s$ with $f_\s > i_\s$ and every
$\ell \in \N$, there exists a $\delta_\ell > 0$ such that
$\valueof[\mdp^\ast][\obj\lrc{i_{\s}} \, \cap \, \infix_1\lrc{\ell}]{\s}
\leq 1 - \delta_\ell$.

Towards a contradiction, assume
that $\valueof[\mdp^\ast][\obj\lrc{i_{\s}} \, \cap \, \infix_1\lrc{\ell}]{\s} = 1$ for some $\ell$.

$\obj\lrc{i_{\s}}\, \cap \, \infix_1\lrc{\ell} =
\en_1(i_{\s})\,\cap\,\vec{\MP_{[2,d]}\lrc{> 0}} \, \cap \, \infix_1\lrc{\ell}
= \ST_1\lrc{i_{\s},\ell}\, \cap \, \vec{\MP_{[2,d]}\lrc{> 0}}$.
Therefore, we have $\valueof[\mdp^\ast][\s]{\ST_1\lrc{i_{\s},\ell}\, \cap \, \vec{\MP_{[2,d]}\lrc{> 0}}} = 1$.
Below we prove that this objective has a finite-memory almost-surely winning strategy $\zstrat$ in $\mdp^\ast$.
Consider a modified MDP $\mdp^\ast_1$ that encodes the
energy level up to $i_\s + \ell$ in the states.
A step exceeding the upper energy bound $i_\s + \ell$ results in a truncation
to $i_\s + \ell$, while a step leading to a negative energy leads to a losing sink.
There exists a memoryless randomized (MR) strategy $\zstrat_1$ in
$\mdp^\ast_1$ from state $(\s, i_\s)$
that wins $\vec{\MP_{[2,d]}\lrc{> 0}}$ almost surely, by <Ref>.
We can then carry $\zstrat_1$ back to $\mdp^\ast$ as a finite-memory strategy $\zstrat$
with $i_\s + \ell + 1$ memory modes such that
$\Prob[\mdp^\ast][\zstrat,\s]{\ST_1\lrc{i_{\s},\ell}\, \cap \, \vec{\MP_{[2,d]}\lrc{> 0}}} = 1$.
By set inclusion, $\Prob[\mdp^\ast][\zstrat,\s]{\obj\lrc{i_{\s}}} = 1$.
By <Ref>, there also exists
a finite-memory strategy from $\s$ in $\mdp$ that is almost surely winning for
This implies $f_\s = i_\s$, a contradiction to our assumption $f_\s > i_\s$.

Hence, we obtain $\delta_{\ell} \eqdef 1-
\valueof[\mdp^\ast][\obj\lrc{i_{\s}} \, \cap \, \infix_1\lrc{\ell}]{\s} > 0$.

The following three lemmas show that almost surely winning strategies for
Energy-MeanPayoff can be found by combining two different
memoryless strategies for the simpler $\Bailout$ and $\Gain$ objectives.

First, we define the objective $\Bailout(k) \eqdef \en_1(k) \, \cap\, \MP_1\lrc{> 0}$.
Let $i^{\Bailout}_{\s}$ denote the minimal energy value $k$ with which one can
almost surely satisfy $\Bailout(k)$ when starting from
state $\s$ (or $\infty$ if it does not exist).

Let $\mdp$ be an MDP.
If $\s \in \AS(\Bailout(k))$ for some $k \in \N$
then $i^{\Bailout}_{\s} \leq 3 \cdot \size{\mdp} \cdot R$.
Moreover, there exists a uniform MD strategy $\optzstrat_{\Bailout}$
which is almost surely winning $\Bailout(k)$
from every state $\s \in \AS(\Bailout(k))$.

We define the $\Gain$ objective as $\MP_{[1,d]}\lrc{> 0}$.
The following lemma shows that an almost surely winning strategy
$\optzstrat_{\Gain}$ for this objective can be chosen as memoryless randomized.

There is a uniform MR strategy $\optzstrat_{\Gain}$ which is almost surely
winning for $\Gain$ (or any subset of dimensions) from
all states $\s \in \AS(\Gain)$.

A difference between $\mdp^\ast$ and $\mdp$ is that if one can
almost surely win Energy-MeanPayoff in $\mdp^\ast$ then one can
also push the energy level arbitrarily high.
This does not always hold in $\mdp$.
(Consider, e.g., a single-state Markov chain with a single loop with reward $0$
in the $1^{st}$ dimension and $+1$ in all other dimensions.)
The difference comes from the loop at state $\s_{\textrm{win}}$ in $\mdp^\ast$
which has a strictly positive reward in all dimensions.
Thus, the following lemma only holds for $\mdp^\ast$.

In $\mdp^{\ast}$,
there are two uniform memoryless strategies
$\optzstrat_{\Bailout}$ and $\optzstrat_{\Gain}$
starting from any state $\s\in \AS(\obj\lrc{k})$,
almost surely satisfy $\Bailout(k)$
and $\Gain$, respectively.

Let $\s\in \AS(\obj\lrc{k})$.
We show that $\s \in \AS(\Bailout(k))$ and
$\s \in \AS\lrc{\Gain}$.
The existence of the memoryless strategies $\optzstrat_{\Bailout}$ and $\optzstrat_{\Gain}$
then follows from <Ref> and
<Ref>, respectively.

We assumed that all states $\s$ in $\mdp$ admit an almost surely winning strategy
for Energy-MeanPayoff.
By <Ref>, this also holds for all states $q$ in
Let $\zstrat^\sharp_q$ denote an almost surely winning strategy from $q$
for $\obj\lrc{i_q}$ in $\mdp^\ast$
(without restrictions on memory).

Recall from <Ref> that the random variable $X_t$ denotes the state
at time $t$, and $Y_t$ denotes the ($d$-dimensional) sum of the rewards until
time $t$.

For every state $q \in \mdp^\ast$ there exists some number of
steps $n_q \in \N$ and a probability $p_q > 0$ such that

\[
\Prob[\mdp^\ast][\zstrat^\sharp_q,q]{\bigcup_{j=0}^{n_q} ((Y_j)_1 > i_{X_j} - i_q)\, \cup\, ((Y_j)_1 \geq f_{X_j} - i_q)} \geq p_q.
\]

Towards a contradiction, assume that for all $m$

\[
\Prob[\mdp^\ast][\zstrat^\sharp_q,q]{\bigcup_{j=0}^{m} ((Y_j)_1 >
i_{X_j} - i_q)\, \cup\, ((Y_j)_1 \geq f_{X_j} - i_q)}=0.
\]

Due to the second part of the union, this implies that never
$(Y_j)_1 + i_q \geq f_{X_j}$.
Since $\zstrat^\sharp_q$ satisfies $\en_1(i_q)$ almost surely, it can
never choose the step to $\s_\textrm{win}$.
This implies $\Prob[\mdp^\ast][\zstrat^\sharp_q,q]{\eventually \s_\textrm{win}}= 0$, i.e., $X_j$ is always different from
(The values $f_\s$ were initially defined with respect to states $\s$ of the original MDP $\mdp$,
but the definition is naturally extended to the MDP $\mdp^\ast$, by
giving the primed states the same value, i.e., $f_{\s'} = f_{\s}$.
The state $\s_\textrm{win}$ does not appear in $\mdp$, but only in $\mdp^\ast$.
We can extend the definition by having $f_{\s_\textrm{win}}=0$.
However, this is not strictly required. The $f_{X_j}$ is already
defined, since $X_j$ is always different from $\s_\textrm{win}$.)

Since $\zstrat^\sharp_q$ satisfies $\en_1(i_q)$ almost surely,
all runs always satisfy $(Y_j)_1 \geq i_{X_j} - i_q$ for all $j$.
On the other hand, our assumption yields
$\Prob[\mdp^\ast][\sigma^\sharp_q,q]{\bigcup_{j=0}^{m} (Y_j)_1 > i_{X_j} - i_q} = 0$.
This implies that $(Y_j)_1 = i_{X_j} - i_q$ for all $j$.
Hence, in all runs the energy fluctuates by at most $\ell \eqdef 2\max_q i_q$.
Thus, $\Prob[\mdp^\ast][\zstrat^\sharp_q,q]{\obj\lrc{i_{q}} \, \cap \, \infix_1\lrc{\ell}}=1$.
Then <Ref> implies that $f_q = i_q$. Since $X_0 = q$ we
have $f_{X_0} = f_q$ and thus $(Y_0)_1 \geq f_{X_0} - i_q = 0$.
This contradicts our assumption, since the second part of the union is
surely satisfied.

For any state $q$, let $n_q$, $p_q$ denote the values from

Now we show that $\s \in \AS(\Bailout(k))$.
Define a strategy $\zstrat_{\Bailout}$ which plays in phases,
separated by resets.
It remembers the number of steps $t \geq 0$ since last reset,
the (under-approximated) sum of rewards $Q_t$
and the current state $X_t$.
The first phase starts at state $\s$ and $\zstrat_{\Bailout}$ plays like $\zstrat^\sharp_\s$
until one of the following events occur.

* There is enough energy such that it is safe to move to
$\s_\textrm{win}$, i.e., $\lrc{Q_t \geq f_{X_t} - i_\s}$, or

* The current energy level is strictly greater than the minimal required
energy level of the current state, i.e., $\lrc{Q_t > i_{X_t} - i_\s}$, or

* $n_\s$ steps have elapsed, i.e., $\lrc{t = n_\s}$.

If at any point <Ref> happens, then the strategy simply goes
to $\s_\textrm{win}$.
If it is the case that <Ref> occurs before $t = n_\s$, let's
say at some time $t'$, then the phase ends at $t'$. The sum of the rewards
in the phase, between the last reset (where $t=0$) and the current time is $\geq i_{X_{t'}}-i_\s + 1$.
If neither <Ref> nor <Ref> occurs before
then the phase ends and we let $t' \eqdef t =n_\s$.
The sum of the rewards in this phase is then exactly $i_{X_{t'}} - i_\s$.
At the end of the phase $\zstrat_{\Bailout}$ resets the number of steps
$\lrc{t = 0}$,
and $Q_t$ to $0$.
In the following phase it moves according to $\zstrat^\sharp_{X_{t'}}$ until the next reset.

$\zstrat_{\Bailout}$ clearly satisfies $\en_1(k)$ as it is a mix of energy
safe strategies $\lrc{\zstrat^{\sharp}_q}_{q \in \states^{\ast}}$
and since we are starting from a safe energy level.
By <Ref>, there is a positive
probability (lower-bounded by $\min_q p_q >0$)
that either <Ref> or <Ref> happens in each phase.

Hence, unless event <Ref> occurs, <Ref> occurs
infinitely often almost surely. Moreover, since the length of phases is
upper bounded by $\max_q n_q$, it occurs frequently.
We obtain $\Prob[\mdp^\ast][\zstrat_{\Bailout},\s]{\MP_1 \geq
\min_{q}\lrc{\frac{p_q}{n_q}} >0 \given \neg\eventually \s_\textrm{win}} = 1$.
On the other hand, if $\s_\textrm{win}$ is reached, then $\MP_1$ holds by
shift invariance and the definition of the positive rewards in the loop at
Therefore, $\Prob[\mdp^\ast][\zstrat_{\Bailout},\s]{\en_1(i_\s) \, \cap \, \MP_1\lrc{> 0}} = 1$.

Now we show that $\s \, \in \, \AS\lrc{\Gain}$.
We make use of the following strategies.

* $\zstrat^\sharp_q$ which satisfies
$\en_1(k)\,\cap\,\vec{\MP_{[2,d]}\lrc{> 0}}$ almost surely from $q$ for every $k \geq i_q$.

* a uniform MD strategy $\optzstrat_{\MP_1}$ which satisfies
$\MP_1\lrc{> 0}$ almost surely from every state. It exists since
$\AS\lrc{\MP_1\lrc{> 0}} = \states^{\ast}$
(where $\states^{\ast}$ is the set of states of $\mdp^\ast$),
because $\Prob[\mdp^\ast][\zstrat_{\Bailout},\s]{\en_1(i_\s) \, \cap \, \MP_1\lrc{> 0}} = 1$.

From the former, we get probabilistic bounds on the achievable mean payoff
in all the dimensions, for all states $\s$, and $0 \leq \eps < 1$,
there is a $d-1$ dimensional vector $\vec{\nu_{\eps}} > \vec{0}$ such that
$\Prob[\mdp^\ast][\zstrat^\sharp_\s,\s]{\vec{\MP_{[2,d]}} \geq \vec{\nu_{\eps}}}
\geq 1-\frac{\eps}{2}$.
This follows from the fact that for any sequence of decreasing vectors
$\vec{\nu_n} \tendsto \vec{0}$ in $\R^{d-1}$, $\vec{\MP_{[2,d]}\lrc{> 0}}
= \bigcup_n \vec{\MP_{[2,d]}\lrc{\geq \vec{\nu_n}}}$ and continuity of
Furthermore, denoting by $\vec{Y_t}$ the sum of rewards in all dimensions
until time $t$,
there exists a sufficiently large bound $n_{\eps} \in \N$
such that $\Prob[\mdp^\ast][\zstrat^\sharp_\s,\s]{\frac{\lrc{Y_t}_j}{t}
\geq \frac{\lrc{\nu_{\eps}}_j}{2}} \geq 1-\eps$
in each of the dimensions $j \in [2,d]$ for all $t \geq n_{\eps}$ steps.
This can be shown by observing that $\MP_j\lrc{\geq \lrc{\nu_{\eps}}_j} =
\bigcap_{k=1}^{\infty}\bigcup_{n=1}^{\infty} \bigcap_{t=n}^{\infty}
\lrc{\frac{\lrc{Y_t}_j}{t} \geq \lrc{\nu_{\eps}}_j \cdot
\lrc{1-\frac{1}{2^k}}}$ and using continuity of measures.

Similarly, there exists a bound $n^*_{\eps} \in \N$ and value $\nu^*_{\eps}>0$
such that $\Prob[][\optzstrat_{\MP_1},\s]{\frac{\lrc{Y_t}_1}{t} \geq
\frac{\nu^*_{\eps}}{2}} \geq 1-\eps$ after $t \geq n^*_{\eps}$ steps for
every state $\s$.

Now consider the following strategy $\zstrat_{\Gain}$, which switches between two phases.

Phase 1: If the current state is $q$, it moves according to
$\zstrat^\sharp_q$ for
some number $\alpha > n_{\eps}$ of steps. Then it switches to phase 2.

Phase 2: It moves according to $\optzstrat_{\MP_1}$ for some
number $\beta > n^*_\eps$ of steps, and then switches back to phase 1.

The strategy $\zstrat_{\Gain}$ is a finite-memory strategy, since the
lengths of the alternating phases are bounded by $\alpha$ and $\beta$,
respectively. (Even if $\zstrat^\sharp_q$ is an infinite-memory strategy,
it can only use bounded memory in each phase.)

We fix $\zstrat_{\Gain}$ from the start state $\s$ and obtain a
finite-state Markov chain. In every BSCC of this Markov chain, the expected mean payoff in the $1^{st}$ dimension will be

$$\geq \frac{-i^\sharp + \beta \cdot \lrc{1-\eps} \cdot \lrc{\frac{\nu^*_{\eps}}{2}} - \beta \cdot \eps \cdot R }{\alpha + \beta}.$$

where $i^\sharp = \max_\s i_\s$ denotes the maximum (over all states) minimal safe energy.

Similarly, in every BSCC, the expected mean payoff in the $j^{th}$ dimension for $j \geq 2$ can be lower-bounded by

$$\geq \frac{\alpha \cdot \lrc{\lrc{1-\eps} \cdot \lrc{\frac{\lrc{\nu_{\eps}}_j}{2}}-\eps \cdot R} - \beta \cdot R}{\alpha + \beta}.$$

By choosing $\eps$ sufficiently small, $\beta$ sufficiently large to make
the first term positive and $\alpha \gg \beta$ sufficiently large to make
the second term positive, we can get positive expected mean payoff in all
dimensions. Since this holds in every BSCC of the induced finite Markov
chain, the objective $\Gain$ is satisfied almost surely.

The following lemma shows the converse of <Ref>.
In $\mdp^{\ast}$, it is always possible to win $\obj\lrc{i_{\s}}$ almost
surely from $\s$ by playing a particular strategy $\optzstrat_{\mathtt{alt,Z_b,Z_g}}$
which combines the two uniform memoryless strategies
$\optzstrat_{\Bailout}$ and $\optzstrat_{\Gain}$.
Let $Z_b$ denote the minimal universally safe energy level for
$\Bailout$, i.e., $Z_b \eqdef \max_\s \min\{k\mid \s \in \AS(\Bailout(k))\}$.
Moreover, let $Z_g > Z_b$ be a larger energy level at which our strategy
switches from $\optzstrat_{\Bailout}$ to $\optzstrat_{\Gain}$.

$\eqdef \memstrattuple$ where

* $\memconfset = \N \x \{0,1\}$ where the first component is the actual energy level and an additional bit which denotes if we are in `$\Gain$-phase' or `$\Bailout$-phase'

* $\initmem = \tuple{k,0}$ if $k < k^{\max} +  R$ else $\tuple{k,1}$

* $\memup\lrc{\tuple{k,y},e} = \tuple{k_{\mathtt{new}},x}$ where

* $k_{\mathtt{new}} = k+\vec{r}^\ast(e)_1$

* $x = \begin{rcases}
k_{\mathtt{new}} \geq Z & \textrm{ if } y=0 \\
k_{\mathtt{new}} \geq k^{\max} + R & \textrm{ if } y = 1
\end{rcases}$

* $\memsuc\lrc{\tuple{k,x},\s} = \optzstrat_{\Bailout}\lrc{\s}$ if $x = 0$, $\optzstrat_{\Gain}\lrc{\s}$ o.w

Similarly to <cit.>, we define an infinite-memory strategy $\optzstrat_{\mathtt{alt,Z_b,Z_g}}$
that always records the current energy level and operates by switching between two phases.
It starts by playing $\optzstrat_{\Gain}$ (Gain-phase)
if our starting energy level is sufficiently high $(\geq Z_b + R)$,
and otherwise starts by playing $\optzstrat_{\Bailout}$ (Bailout-phase).
In the $\Bailout$-phase, the primary goal is to pump the energy level up until
it is $\ge Z_g$, and then it switches to the $\Gain$-phase.
It enters the $\Bailout$-phase again if the energy level drops below $Z_b + R$
(in which case it will still be $\ge Z_b$).

There exists a $Z_g \in \N$ such that for every $\s$ in $\mdp^*$
the strategy $\optzstrat_{\mathtt{alt,Z_b,Z_g}}$ is almost surely
winning for $\obj\lrc{i_{\s}}$ from $\s$.

The parameter $Z_g$ is chosen sufficiently large such that there is a fixed non-zero
probability that after every Bailout-phase one never needs another $\Bailout$.
(Thus, except in a null set there are only finitely many Bailouts.)
The existence of such a finite $Z_g$ is guaranteed by the fact that
$\lim_{k \tendsto \infty} \Prob[][\optzstrat_{\Gain},\s]{\obj\lrc{k}} = 1$. (<Ref>).
Eventually, except in a null set, $\optzstrat_{\mathtt{alt,Z_b,Z_g}}$ plays
$\Gain$ forever, thus satisfying $\obj\lrc{i_{\s}}$ almost
surely from $\s$.

Some combined objectives like Energy-Parity really require infinite
memory for almost surely winning strategies <cit.>.
However, we show that a sufficiently large finite memory is enough to
win Energy-MeanPayoff almost surely.
The idea is to modify the strategy $\optzstrat_{\mathtt{alt,Z_b,Z_g}}$ such
that it remembers the current energy only in the interval $[0,b]$, for some
sufficiently large $b > Z_g$, and ignores any possible excess energy above $b$.
This modified strategy is denoted by $\optzstrat_{\mathtt{alt,Z_b,Z_g,b}}$, and
it has a finite set of memory modes $[0,b] \x \{0,1\}$. The $\{0,1\}$ part
is used to remember the current phase ($\Gain=0$ or $\Bailout=1$).
Then $\optzstrat_{\mathtt{alt,Z_b,Z_g,b}}[(u,x)]$ denotes the strategy
$\optzstrat_{\mathtt{alt,Z_b,Z_g,b}}$ with current memory mode $(u,x) \in [0,b] \x \{0,1\}$.

The finite bound $b$ on the remembered energy has the effect that
$\optzstrat_{\mathtt{alt,Z_b,Z_g,b}}$ can no
longer guarantee a fixed positive probability of not needing another Bailout
after each Bailout-phase. Thus, one might have infinitely many Bailouts with
positive probability. (Most of these are unnecessary, but one cannot be sure
which ones).
Unlike for Energy-Parity, where using infinitely many
$\Bailout$ phases can compromise the objective,
the nature of the $\vec{\MP_{[2,d]}\lrc{> 0}}$ objective allows us to use
infinitely many Bailouts with non-zero probability, provided that they happen
sufficiently infrequently.

By its construction, the strategy $\optzstrat_{\mathtt{alt,Z_b,Z_g,b}}[(i_\s,x)]$ is
energy-safe from every state $\s$, every initial energy $\ge i_s$ and $x \in \{0,1\}$.
It remains to show that it
also satisfies $\vec{\MP_{[2,d]}\lrc{> 0}}$ almost surely.
Since $\optzstrat_{\mathtt{alt,Z_b,Z_g,b}}$ is finite-memory, it suffices to
consider the induced finite Markov chain $\mc$ and show that the expected mean
payoff is strictly positive in every BSCC.
I.e., we prove that
$\expectation[][\optzstrat_{\mathtt{alt,Z_b,Z_g,b}},\s]{\vec{\MP_{[2,d]}}} >\vec{0}$
for a sufficiently large $b$.
To this end, we consider the finite Markov chains
$\mc^{\Gain}$ and $\mc^{\Bailout}$ obtained by fixing the memoryless
strategies $\optzstrat_{\Gain}$ and $\optzstrat_{\Bailout}$ in $\mdp^\ast$,
The application of $\optzstrat_{\mathtt{alt, Z_b, Z_g, b}}$ can then be seen
as alternating between these two Markov chains based on hitting certain energy

Let $T^{\Gain}$ denote the random variable that measures the length of a
Gain-phase, when starting at energy level $Z_g$ and assuming that the energy
it truncated at $b$.
Similarly, $T^{\Bailout}$ is the random variable that measures the length of a
Bailout-phase when starting at energy level $Z_b$.
(Here it does not matter that the energy is truncated at $b$,
since the Bailout-phase ends when the energy reaches $Z_g < b$.)
Since $R$ can be $>1$, the Bailout-phase might actually start at a slightly higher
energy level $u \in [Z_b,Z_b+R-1]$, and thus $T^{\Bailout}$ over-approximates the
actual length of the Bailout-phase, which is conservative for our analysis.
the Gain phase might start with an energy slightly higher than $Z_g$, and
$T^{\Gain}$ under-approximates the length of the Gain-phase, which is again
The random variables $(Y_{T^{\Gain}})_i$ and $(Y_{T^{\Bailout}})_i$
then measure the sum of the rewards the $i^{th}$ dimension obtained during the
Gain and Bailout phases, respectively.

The following lemma shows that the strategy $\optzstrat_{\mathtt{alt, Z_b, Z_g, b}}$
can attain a strictly positive mean payoff in all dimensions $i \in [2,d]$,
provided that the expected reward during the Gain-phase is sufficiently large
(positive) and the expected reward during the Bailout-phase (though possibly
negative) is not too small.

If there are constants $v^1_i>0$ and $v^2_i$ such that, for all $i \in [2,d]$ and
states $q$

\begin{align*}
\expectation[\mdp^\ast][\optzstrat_{\mathtt{alt, Z_b,Z_g,b}}[(Z_g,0)],q]{\lrc{Y_{T^{\Gain}}}_i} &\geq v^1_i\\% R#3: l.434
\expectation[\mdp^\ast][\optzstrat_{\mathtt{alt, Z_b, Z_g, b}}[(Z_b,1)],q]{\lrc{Y_{T^{\Bailout}}}_i} &\geq v^2_i\\% R#3: l.435
v^1_i + v^2_i > 0
\end{align*}

then $\expectation[\mdp^\ast][\optzstrat_{\mathtt{alt, Z_b, Z_g,b}}[\memconf],\s]{\MP_i} > 0$
for all $\s$ and $\memconf \in [i_\s,b] \x \{0,1\}$.

By fixing the finite-memory strategy $\optzstrat_{\mathtt{alt, Z_b,Z_g,b}}$,
we obtain a finite Markov chain. Consider any BSCC in this Markov chain.
In this BSCC, except for a null set of runs, either no Bailouts happen or infinitely many.
In the former case, this BSCC behaves like playing $\optzstrat_{\Gain}$
forever, which attains a strictly positive mean payoff in all dimensions almost
surely, and thus a strictly positive expected mean payoff in each dimension $i$.
In the second case, almost surely there happen infinitely many Bailouts,
each starting at an every level $\ge Z_b$.
Then, by the finiteness of the BSCC, we obtain that
$\expectation[][]{T^{\Gain}} < \infty$.
Moreover, by the definition of $\optzstrat_{\Bailout}$, the expected
duration of the Bailout-phase is always finite, i.e.,
$\expectation[][]{T^{\Bailout}} < \infty$.
Thus, by linearity of expectations,
$\expectation[\mdp^\ast][\optzstrat_{\mathtt{alt, Z_b, Z_g,b}},\s]{\MP_i}
\ge (v^1_i + v^2_i)/(\expectation[][]{T^{\Gain}} +
\expectation[][]{T^{\Bailout}}) > 0$.

The following technical <Ref> (proof in <Ref>) shows that the
constants $v^1_i,v^2_i$ from <Ref> exist.
Recall that the finite Markov chains
$\mc^{\Gain}$ and $\mc^{\Bailout}$ are obtained by fixing the memoryless
strategies $\optzstrat_{\Gain}$ and $\optzstrat_{\Bailout}$ in $\mdp^\ast$,
Let $x_{\min,1}$ and $x_{\min,2}$ denote the minimal occurring
non-zero probabilities in these two Markov chains, respectively.
(They come from solutions of linear programs and can be chosen as only
exponentially small, i.e., described by a polynomial number of bits; cf. <Ref>).
The proof works by applying general results about expected first passage times in
truncated Markov chains
to the induced Markov chains $\mc^{\Gain}$ and $\mc^{\Bailout}$.
The general idea is that in the Gain-phase one has a general up drift in all
dimensions, and in particular in the first (energy) dimension.
It is thus unlikely to go down very far in the energy dimension,
even if the energy is truncated at $b$.
Thus, for a sufficiently large truncation point $b$ (actually $b=Z_g+1$ suffices),
the expected time spent in the Gain-phase is very large relative to the
expected time spent in the Bailout phase.
More exactly, the former increases exponentially in $b$, while the latter
is polynomial in $b$.
For a sufficiently large $b$ (exponential in $|\mdp^\ast|$),
the condition $v^1_i + v^2_i > 0$ is met.

Let $\mu_i > 0$ denote the lower bound on the mean payoff in dimension
$i$ in any BSCC in the Markov chain $\mc^{\Gain}$ with corresponding
computable constants $c_i,\,g_{\Gain},\,h_{\Gain}$
and let $\mu$ denote the
lower bound on the mean payoff in the $1^{st}$ dimension in any BSCC of
$\mc^{\Bailout}$ with the corresponding constants
All the above constants, except $c_i$,
can be chosen as
at most exponential in $\size{\mdp^\ast}$ and
$1/(1-c_i) \in \Ocompl\lrc{\exp\lrc{\exp\lrc{\size{\mdp^\ast}^{\Ocompl\lrc{1}}}}}$.

Then there are constants $0 < C_1 < 1$, $C_2 > 0$, $C_3 > 0$, $C_4 > 0$,
$C_5 > 0$, all exponential in $\size{\mdp^\ast}$
and dependent only on $\mdp$,
such that for  $k \eqdef \frac{2 \cdot
\size{\states^\ast}}{x_{\min,1}^{\size{\states^\ast}}} \in
\Ocompl\lrc{\exp\lrc{\size{\mdp^\ast}^{\Ocompl\lrc{1}}}}$, any
$\delta \in (0,1)$ sufficiently small such that $\lrc{\size{\states^\ast}+1} \cdot \lrc{\frac{1}{\delta}-1} + \ceil{ \lrc{\log_{c_i}(\delta \cdot (1-c_i))}} \geq \frac{h_\Gain}{\mu_i}$ for all $2 \leq i \leq d$, one can choose

$Z_g \eqdef Z_b\, +\, R\, +\, k \cdot R\, +\, \max_{i}\lrc{R \cdot \ceil{\log_{c_i}\lrc{\delta \cdot \lrc{1-c_i}}} - R + 1, h_\Gain}\, \in \Ocompl\lrc{e^{\size{\mdp^\ast}^{\Ocompl\lrc{1}}}\cdot \log\lrc{1/\delta}}$ and $b \eqdef Z_g + 1$ so that

\begin{align*}
\expectation[\mdp^\ast][\optzstrat_{\mathtt{alt, Z_b, Z_g, b}}[(Z_g,0)],q]{\lrc{Y_{T^{\Gain}}}_i} &\geq
C_1 \cdot \frac{1}{\delta} - C_2 \log_2 \lrc{\frac{1}{\delta}} - C_3
& \eqdef v^1_i \\
\expectation[\mdp^\ast][\optzstrat_{\mathtt{alt, Z_b, Z_g,
b}}[(Z_b,1)],q]{\lrc{Y_{T^{\Bailout}}}_i} &\geq - C_4 \log_2
\lrc{\frac{1}{\delta}} - C_5
& \eqdef v^2_i
\end{align*}

In particular, in order to satisfy the condition $v^1_i + v^2_i > 0$,
it suffices to choose
$1/\delta \in \Ocompl\lrc{\max(1/C_1,\max_{2\le j \le 5} C_j)^{\Ocompl\lrc{1}}}$.
Since the constants $C_j$ are exponential in $\size{\mdp^{\ast}}$,
and by the conditions on the other constants above,
the value $Z_g$, and hence the overall bound $b=Z_g+1$, can be chosen such that
$b \in \Ocompl\lrc{\exp\lrc{\size{\mdp^\ast}^{\Ocompl\lrc{1}}}}$.

Now we can prove the first item of our main result.

Towards a contradiction, we assume that there exists
a state $\s^{\dagger}$ such that
there is no finite-memory almost surely winning strategy from $\s^{\dagger}$
for $\obj\lrc{i_{\s^\dagger}}$ in the MDP $\mdp$.

First we consider the MDP $\mdp^\ast$.
The finite-memory strategy $\optzstrat_{\mathtt{alt, Z_b,Z_g,b}}[(i_{\s^\dagger},1)]$ from $\s^{\dagger}$
is energy-safe by construction and satisfies $\en_1(i_{\s^\dagger})$ surely.
Now consider the finite Markov chain induced by fixing this
finite-memory strategy in $\mdp^\ast$.
By <Ref> and <Ref>,
for a sufficiently large (exponential) $b$
it yields a strictly positive expected mean payoff
$v^1_i + v^2_i >0$ in every dimension $i \in [2,d]$ in every BSCC of this
Markov chain.
Since the Markov chain is finite, this implies that the mean payoff in every
dimension $i \in [2,d]$ is strictly positive almost surely.
and thus
So there exists an almost surely winning finite-memory strategy from
$\s^\dagger$ for $\obj\lrc{i_{\s^\dagger}}$ in $\mdp^\ast$.
However, <Ref> then implies that there also exists
an almost surely winning finite-memory strategy from
$\s^\dagger$ for $\obj\lrc{i_{\s^\dagger}}$ in $\mdp$. Contradiction.

If $\optzstrat_{\mathtt{alt, Z_b,Z_g,b}}$ satisfies $\obj\lrc{i_\s}$ almost surely
from some state $\s$ then it also satisfies the stronger objective
$\obj\lrc{i_\s} \cap \infix\lrc{b}$ almost surely.
Consider a winning run induced by $\optzstrat_{\mathtt{alt, Z_b,Z_g,b}}$.
While the true energy might sometimes be higher than $b$, the energy remembered by
$\optzstrat_{\mathtt{alt, Z_b,Z_g,b}}$ is always $\le b$.
Even with this conservative under-approximation of the energy,
the run still satisfies the energy objective.
Therefore, in any winning run induced by $\optzstrat_{\mathtt{alt, Z_b,Z_g,b}}$,
the energy can never decrease by more than $b$. Thus,
also $\infix\lrc{b}$ is satisfied almost surely.

§ PROOF OF MEMORY BOUND

Given some state $\s$, let $\zstrat = \memstrattuple$ be a finite-memory
strategy that is almost surely winning for $\obj\lrc{i_\s}$
(which exists by <Ref>).
We show there exists an almost surely winning strategy
$\zstrat'$ for $\obj\lrc{i_\s}$ such that the energy fluctuations are bounded by some
constant which is exponential in $\size{\mdp}$.

First, inside any BSCC $B$ of $\mdp^\zstrat$, we construct an
almost surely winning strategy $\zstrat_B$ and upper bound the minimal safe energy levels and energy fluctuation
while following $\zstrat_B$.
Using this, we upper bound the energy fluctuations in paths before reaching a BSCC.
We use the fact that the set of states and transitions that occur in any BSCC
of a Markov chain induced by fixing some finite-memory strategy in an MDP
is an end component of this MDP (<cit.>).

Let $B$ be a BSCC of $\mdp^\zstrat$ and let $\mdp\lrc{B}$ be the corresponding end component in $\mdp$ with states $\states_B$ and transitions
$\transition_B$. Then there is a strategy $\zstrat_B$, a bound
$b_B \in \Ocompl\lrc{\exp\lrc{\size{\mdp\lrc{B}}^{\Ocompl\lrc{1}}}}$ such that for any state $q \, \in \, \states_B$, there is a minimal safe energy level $j_q \eqdef i^{\mdp\lrc{B}}_q \leq 3 \cdot \size{\states_B} \cdot R$ such that
$ \Prob[\mdp\lrc{B}][\zstrat_B,q]{\obj\lrc{j_q} \, \cap\, \infix\lrc{b_B}} = 1$.

The idea is that for $\mdp\lrc{B}$ there are two cases.
In the first case it behaves similar to $\mdp^{\ast}$ from
<Ref>, in the sense that
it is possible to win $\Gain$ and $\Bailout$ almost surely, and thus
Energy-MeanPayoff can be won almost surely by switching between the
two strategies for $\Gain$ and $\Bailout$ like in the strategy $\optzstrat_{\mathtt{alt, Z_b,Z_g}}$.
Then one can invoke <Ref>
on $\mdp\lrc{B}$ to get an exponential bound $b_B$ such that $\Prob[\mdp\lrc{B}][\zstrat_B,q]{\obj\lrc{j_q} \, \cap\, \infix\lrc{b_B}} = 1$.

If the first case does not hold then
$\mdp\lrc{B}$ is very restrictive,
and one can show that the energy level fluctuations are bounded by a constant
in $\Ocompl\lrc{\size{\states_B} \cdot R}$.

Since the minimal safe energy levels inside these end components are not too large,
one can then bound the energy fluctuations in paths before they reach any such
end component $\mdp\lrc{B}$.
The following lemma is shown in <Ref>.

Let $T$ denote the union of all $\states_B$ of every BSCC $B$ of
as in <Ref>.
Then one can almost surely reach any state in $T$ with the corresponding minimal
safe energy level with energy fluctuations of at most $5 \cdot \size{\states} \cdot R$.

By <Ref>,
for each state $\s$, one can choose a strategy $\zstrat$ and some constant
$b \in \Ocompl\lrc{\exp\lrc{\size{\mdp}^{\Ocompl\lrc{1}}}}$
such that $\Prob[\mdp][\zstrat,\s]{\obj\lrc{i_\s}\, \cap \, \infix\lrc{b}} = 1$.
This means if one encodes the energy levels between $[0,b]$ into the state space by discarding any excess energy above $b$ and redirecting all the
transitions which result in a negative energy to a losing sink (for
$\vec{\MP}_{[2,d]}\lrc{> 0}$)
and constructs this larger MDP $\mdp[0,b]$,
then there is a strategy $\zstrat'$ such that
$\Prob[\mdp[0,b]][\zstrat',\tuple{\s,k}]{\vec{\MP}_{[2,d]}\lrc{> 0}} =1$
for every $k \in [i_\s,b]$.
Then, by <Ref>,
there also exists a memoryless (MR) strategy
$\optzstrat$ in $\mdp[0,b]$ which is almost surely winning
$\vec{\MP}_{[2,d]}\lrc{> 0}$ from $\tuple{\s,k}$.

We can carry the memoryless strategy $\optzstrat$ in $\mdp[0,b]$ back to $\mdp$
as a finite-memory strategy $\optzstrat_\mdp$ with memory $[0,b]$.
It stores the
encoded under-approximated energy level from $\mdp[0,b]$ in its finite memory instead.
Thus $\optzstrat_\mdp$ is a finite-memory strategy from $\s$ that
satisfies $\obj\lrc{i_\s}$
almost surely, and the size of its memory is bounded by
$b \in \Ocompl\lrc{\exp\lrc{\size{\mdp}^{\Ocompl\lrc{1}}}}$.

The strategy $\optzstrat_\mdp$ uses randomization, because $\optzstrat$
from <Ref> is MR.
However, the MR strategy $\optzstrat$ for the mean payoff objective could
be replaced by a deterministic strategy with an exponential number of
memory modes. Hence the overall number of memory modes in the obtained
deterministic version of $\optzstrat_\mdp$ is still only exponential.

§ THE LOWER BOUND (PROOF OF <REF>)

In the previous sections we have shown that finite memory suffices
for almost surely winning strategies for the Energy-MeanPayoff objective.
However, the required memory depends on the given MDP.
We show that no fixed finite amount of memory is sufficient for all MDPs.
In fact, the required memory is exponential in the transition probabilities
even for an otherwise fixed 5-state MDP with just one controlled state, $R=1$ and $d=2$.

Let $1 > \delta > 0$ and $\mdp_\delta=\mdptuple$ be an MDP with 2-dimensional rewards.
It has just one controlled state $\s$
with transitions $\s \to \s_l$ and $\s \to \s_r$.
From $\s_l$ there are two transitions $e_1 = (\s_l \to \s_l^1)$
and $e_2 = (\s_l \to \s_l^2)$.
Let $\probm(e_1) = (1 + \delta)/2$ and $\probm(e_2) = (1 - \delta)/2$
and $\vec{r}(e_1) = (+1,+1)$ and $\vec{r}(e_2) = (-1,-1)$.
$\s_l^1$ and $\s_l^2$ are random states which each have just one transition
back to $\s$ with probability $1$ and reward $\vec{0}$.
From $s_r$ there is only one transition $e_3$ back to $s$ with
probability $1$ and $\vec{r}(e_3) = (+1,-1)$.

The following lemma directly implies the exponential lower bound
on the number of memory modes in <Ref>(<Ref>).

Consider the Energy-MeanPayoff objective.
For every finite bound $m \in \N$ on the number of memory modes
there exists a $\delta \eqdef 1/(6m) >0$
such that the finite MDP $\mdp_\delta = \mdptuple$ from <Ref>
satisfies the following properties.

* $\exists \sigma'\ \probm^{\mdp_\delta}_{\sigma',\s}(\en_1(0)\,\cap\,\vec{\MP_2}\lrc{> 0})=1$,
i.e., it is possible to win almost surely from $s$ in $\mdp_\delta$,
even with initial energy $0$.

* For every finite-memory strategy $\sigma$ with $\le m$ memory modes we have
$\probm^{\mdp_\delta}_{\sigma,\s}(\en_1(k)\,\cap\,\vec{\MP_2}\lrc{> 0})=0$
for every $k \in \N$, i.e., $\sigma$ attains nothing in $\mdp_\delta$,
regardless of the initial energy $k$.

* For $\mdp_\delta$ we have $|S|=5$, $d=1$ and $R=1$.
The number of memory modes required for an almost-surely winning strategy
in $\mdp_\delta$ is exponential in $|P|$ (and in $|\mdp_\delta|$).

Towards item 1, consider a strategy $\sigma'$ that plays as follows. It keeps
a counter that records the current energy, which is initially $0$.
Whenever the current energy is $0$, it plays $s \to s_r$, otherwise
it plays $s \to s_l$. Thus $\sigma'$ satisfies $\en_1(0)$ surely from $s$.
Since $\delta>0$ it follows from the classic Gambler's ruin problem
(with strictly positive expected gain, here in the first reward dimension)
that $\sigma'$
plays $s \to s_r$ only finitely often, except in a nullset of the runs.
Therefore, the expected mean payoff (in the second dimension) under $\sigma'$ is
$(1+\delta)/2 - (1-\delta)/2 = \delta >0$.
Hence $\probm^{\mdp_\delta}_{\sigma',\s}(\vec{\MP_2}\lrc{> 0})=1$. Since the
energy objective is satisfied surely, we obtain
$\probm^{\mdp_\delta}_{\sigma',\s}(\en_1(0)\,\cap\,\vec{\MP_2}\lrc{> 0})=1$.

Towards item 2, let $\delta \eqdef 1/(6m) >0$ and
let $\sigma$ be a finite-memory strategy with $\le m$ memory modes.
Consider the finite-state Markov chain $\cal C$ that is induced by
playing $\sigma$ from $s$ in $\mdp_\delta$.
This Markov chain has $\le 5m$ states, since $\mdp$
has $5$ states and $\sigma$ has $\le m$ memory modes.
Let $B$ be any BSCC of $\cal C$ that is reachable from $s$ and the initial
memory mode of $\sigma$. In particular, $|B| \le 5m$.
In $B$ there must not exist any loop that does not contain $s_r$, because
otherwise the energy objective cannot be satisfied almost surely.
Thus every path in $B$ of length $\ge 5m$ must contain $s_r$ (and hence a reward
$(+1,-1)$) at least once. Therefore, the expected mean payoff in $B$ (in the
second reward dimension) is $\le 5m\delta - 1 = -1/6 < 0$.
Since this holds in every reachable BSCC, we obtain
$\probm^{\mdp_\delta}_{\sigma,\s}(\vec{\MP_2}\lrc{> 0})=0$ and thus
$\probm^{\mdp_\delta}_{\sigma,\s}(\en_1(k)\,\cap\,\vec{\MP_2}\lrc{> 0})=0$.

Towards item 3, the size of $\mdp_\delta$ follows from <Ref>.
By items 1 and 2,
the required number of memory modes
$m$ for an almost-surely winning strategy
satisfies $m > 1/(6\delta)$.
Since $|P| = \Theta(\log(1/\delta))$
and $|\mdp_\delta| = \Theta(|P|)$, we obtain
$m = \Omega(\exp(|P|))$ and $m = \Omega(\exp(|\mdp_\delta|))$.

The exponential lower bound on the required memory
does not require probabilities encoded in binary like in
One can construct an equivalent example with polynomially
many states where all transition probabilities are $1/2$.
This is because one can encode exponentially small probabilities $2^{-k}$
with a chain of $k$ extra states and transition probabilities $1/2$.

§ COMPUTATIONAL COMPLEXITY

We have shown that the existence of an almost surely winning strategy for the
Energy-MeanPayoff objective for a given state and initial energy level in an MDP
implies the existence of a deterministic such strategy with exponentially many
memory modes (unlike for Energy-Parity which
requires infinite memory in general <cit.>).

A related problem is the decidability of the question whether a given state
in an MDP and a given initial energy level admit an almost surely winning
strategy for Energy-MeanPayoff.
This problem is decidable in pseudo-polynomial time, using an algorithm very
similar to the one for Energy-Parity presented in <cit.>.
I.e., the time is polynomial, provided that the bound $R$ on the rewards
is given in unary. Transition probabilities in the MDP can still be represented
in binary.
The crucial point is that it suffices to witness the mere existence of
an almost surely winning strategy, regardless of its memory.
Basically, it suffices that the algorithm proves that the infinite-memory
strategy $\optzstrat_{\mathtt{alt,Z_b,Z_g}}$ wins almost surely
(plus a small extra argument about a corner case where the energy fluctuates only
in a bounded region). The algorithm
does not need to compute the bound $b$ or to explicitly construct
the finite-memory strategy $\optzstrat_{\mathtt{alt,Z_b,Z_g,b}}$.

Let $\mdp = \mdptuple$ be an MDP with $d$-dimensional rewards on the edges
$\vec{r}: \transition \to [-R,R]^d$.
For any state $\s$ and $k \in \N$, the existence of an almost surely winning
strategy from $\s$ for the multidimensional Energy-MeanPayoff objective
$\en_1(k)\,\cap\,\vec{\MP_{[2,d]}\lrc{> 0}}$ is decidable in pseudo-polynomial
time (i.e., polynomial for $R$ in unary).

The proof is similar to the one for Energy-Parity presented in <cit.>.
We outline the differences below.
First, in the corner case where it is impossible to pump the energy up arbitrarily high almost surely
from some state $q$, the only possible way to win Energy-MeanPayoff
(resp. Energy-Parity) almost surely (if at all) is by using a non-nullset of
runs where the energy only ever fluctuates in a bounded region.
In that case, the size of the energy fluctuations in these runs can safely be restricted
to a region that is polynomial in $|S|\cdot R$, and thus pseudo-polynomial in
$|\mdp|$ <cit.>.
It thus suffices to win multi-dimensional $\MP_{[2,d]}\lrc{> 0}$ almost surely in a
derived MDP $\mdp'$ where the bounded energy is encoded into the states.
Deciding this requires time polynomial in $|\mdp'|$ <cit.> and thus
pseudo-polynomial in $|\mdp|$.
The winning situations of the corner case can then be encoded into $\mdp$,
yielding a derived MDP $\mdp'$ of pseudo-polynomial size, where
Energy-MeanPayoff can be won almost surely if and only if it can be won almost
surely by a combination of $\Gain$ and $\Bailout$ strategies, i.e., by strategy
Therefore it suffices to compute the states (and minimal initial energy levels $k$)
where $\Gain$ and $\Bailout(k)$ can be won almost surely.
The objective $\Bailout(k) \eqdef \en_1(k) \, \cap\, \MP_1\lrc{> 0}$ is
exactly the same as the $\Bailout$ objective analyzed in <cit.>,
and winning it almost surely is decidable in pseudo-polynomial time.
Our objective $\Gain \eqdef \MP_{[1,d]}\lrc{> 0}$ differs from the
$\Gain$ objective considered in <cit.> (which was
$\MP_1\lrc{> 0}\,\cap\, \parity$), but winning it almost surely is
still decidable in polynomial time <cit.>
by solving a linear program.
So overall the algorithm runs in pseudo-polynomial time.