as $\gamma$ and $\delta$ in $\mathcal{M}$, but the decrease in the accumulated
weight is explicitly encoded into the state space. Namely, for
$n\in\mathbb{N}$ and $0<i\leq k$, we have

$\displaystyle e(t,nk+i)=\sum_{j=1}^{k}$
$\displaystyle\big{(}\mathrm{Pr}_{\mathcal{C},t_{+i}}(\lozenge t_{-k+j})\cdot
e(t,(n{-}1)k+j)+\mathrm{Pr}_{\mathcal{C},t_{+i}}(\lozenge s_{-k+j})\cdot
e(s,(n{-}1)k+j)\big{)}$ $\displaystyle+\sum_{j=1}^{k}$
$\displaystyle\mathrm{Pr}_{\mathcal{C},t_{+i}}(\lozenge\mathit{goal}_{+j})\cdot(nk+j)$
($\ast\ast$)

and analogously for $e(s,nk+i)$. We now group the optimal values together in
the following column vectors

$v_{n}=(e(t,nk+k),e(t,nk+k-1),\ldots,e(t,nk+1),e(s,nk+k),\ldots,e(s,nk+1))^{\top}$

for $n\in\mathbb{N}$. In other words, this vector contains the optimal values
for the partial expectation when starting in $t$ or $s$ with an accumulated
weight from $\\{nk+1,\dots,nk+k\\}$. Further, we define the vector containing
the optimal values for weights in $\\{-k+1,\dots,0\\}$ which are the least
values of accumulated weight reachable under scheduler $\mathfrak{S}$.

$v_{-1}=(e(t,0),e(t,-1),\ldots,e(t,-k+1),e(s,0),e(s,-1),\ldots,e(s,-k+1))^{\top}.$

As we have seen, these values are given as follows:

$e(t,-k+1+j)=\frac{1}{2k^{2(k-j)}}+\beta_{j}\text{ and
}e(s,-k+1+j)=\frac{1}{2k^{2(k-j)}}$

for $0\leq j\leq k-1$.

As the reachability probabilities in $\mathcal{C}$ are rational and computable
in polynomial time, we conclude from (4.2) that there are a matrix
$A\in\mathbb{Q}^{2k\times 2k}$, and vectors $a$ and $b$ in $\mathbb{Q}^{2k}$
computable in polynomial time such that

$v_{n}=Av_{n-1}+na+b,$

for all $n\in\mathbb{N}$. We claim that the following explicit representation
for $n\geq-1$ satisfies this recursion:

$v_{n}=A^{n+1}v_{-1}+\sum_{i=0}^{n}(n-i)A^{i}a+\sum_{i=0}^{n}A^{i}b.$

We show this by induction: Clearly, this representation yields the correct
value for $v_{-1}$. So, assume
$v_{n}=A^{n+1}v_{-1}+\sum_{i=0}^{n}(n-i)A^{i}a+\sum_{i=0}^{n}A^{i}b$. Then,

$\displaystyle v_{n+1}$
$\displaystyle=A(A^{n+1}v_{-1}+\sum_{i=0}^{n}(n-i)A^{i}a+\sum_{i=0}^{n}A^{i}b)+(n+1)a+b$
$\displaystyle=A^{n+2}v_{-1}+\left(\sum_{i=0}^{n}(n-i)A^{i+1}a\right)+(n+1)A^{0}a+\left(\sum_{i=1}^{n+1}A^{i}b\right)+A^{0}b$
$\displaystyle=A^{n+2}v_{-1}+\sum_{i=0}^{n+1}(n+1-i)A^{i}a+\sum_{i=0}^{n+1}A^{i}b.$

So, we have an explicit representation for $v_{n}$. The value we are
interested in is

$\mathbb{PE}^{\mathfrak{S}}_{\mathcal{M}}=\sum_{\ell=1}^{\infty}(1/2)^{\ell}e(t,\ell).$

Let $c=(\frac{1}{2^{k}},\frac{1}{2^{k-1}},\dots,\frac{1}{2^{1}},0,\dots,0)$.
Then,

$(\frac{1}{2^{k}})^{n}c\cdot v_{n}=\sum_{i=1}^{k}\frac{1}{2^{nk+i}}e(t,nk+i).$

Hence, we can write

$\displaystyle\mathbb{PE}^{\mathfrak{S}}_{\mathcal{M}}=\sum_{n=0}^{\infty}(\frac{1}{2^{k}})^{n}c\cdot
v_{n}=c\cdot\sum_{n=0}^{\infty}(\frac{1}{2^{k}})^{n}v_{n}$ $\displaystyle={}$
$\displaystyle
c\cdot\sum_{n=0}^{\infty}(\frac{1}{2^{k}})^{n}(A^{n+1}v_{-1}+\sum_{i=0}^{n}(n-i)A^{i}a+\sum_{i=0}^{n}A^{i}b)$
$\displaystyle={}$ $\displaystyle
c\cdot\big{(}(\sum_{n=0}^{\infty}(\frac{1}{2^{k}})^{n}A^{n+1})v_{-1}+(\sum_{n=0}^{\infty}(\frac{1}{2^{k}})^{n}\sum_{i=0}^{n}(n-i)A^{i})a+(\sum_{n=0}^{\infty}(\frac{1}{2^{k}})^{n}\sum_{i=0}^{n}A^{i})b\big{)}.$

We claim that all of the matrix series involved converge to rational matrices.
As in the proof of Lemma 4.4, we observe that the maximal row sum in $A$ is at
most $|\alpha_{1}|{+}\ldots{+}|\alpha_{k}|<1$ because the rows of the matrix
contain exactly the probabilities to reach $t_{0}$, …$t_{-k+1}$, $s_{0}$, …,
and $s_{-k+1}$ from a state $t_{+i}$ or $s_{+i}$ in $\mathcal{C}$ for $1\leq
i\leq k$. But the probability to reach $\mathit{goal}_{+i}$ from these states
is already $1{-}|\alpha_{1}|{-}\ldots{-}|\alpha_{k}|$. Hence,
$\|A\|_{\infty}$, the operator norm induced by the maximum norm
$\|\cdot\|_{\infty}$, which equals $\max_{i}\sum_{j=1}^{2k}|A_{ij}|$, is less
than $1$. So, of course also $\|\frac{1}{2^{k}}A\|_{\infty}<1$ and hence the
Neumann series $\sum_{n=0}^{\infty}(\frac{1}{2^{k}}A)^{n}$ converges to
$(I_{2k}-\frac{1}{2^{k}}A)^{-1}$ where $I_{2k}$ is the identity matrix of size
$2k{\times}2k$. So,

$\displaystyle\sum_{n=0}^{\infty}(\frac{1}{2^{k}})^{n}A^{n+1}=A\sum_{n=0}^{\infty}(\frac{1}{2^{k}}A)^{n}=A(I_{2k}-\frac{1}{2^{k}}A)^{-1}.$

Note that $\|A\|_{\infty}<1$ also implies that $I_{2k}-A$ is invertible. We
observe that for all $n$,

$\sum_{i=0}^{n}A^{i}=(I_{2k}-A)^{-1}(I_{2k}-A^{n+1})$

which is shown by straight-forward induction. Therefore,

$\displaystyle\sum_{n=0}^{\infty}(\frac{1}{2^{k}})^{n}\sum_{i=0}^{n}A^{i}$
$\displaystyle=(I_{2k}-A)^{-1}\left(\sum_{n=0}^{\infty}(\frac{1}{2^{k}})^{n}I_{2k}-A\sum_{n=0}^{\infty}(\frac{1}{2^{k}}A)^{n}\right)$
$\displaystyle=(I_{2k}-A)^{-1}\left(\frac{2^{k}}{2^{k}{-}1}I_{2k}-A(I_{2k}-\frac{1}{2^{k}}A)^{-1}\right).$

Finally, we show by induction that

$\sum_{i=0}^{n}(n-i)A^{i}=(I_{2k}-A)^{-2}(A^{n+1}-A+n(I_{2k}-A)).$

This is equivalent to

$(I_{2k}-A)^{2}\sum_{i=0}^{n}(n-i)A^{i}=A^{n+1}-A+n(I_{2k}-A).$

For $n=0$, both sides evaluate to $0$. So, we assume the claim holds for $n$.

$\displaystyle(I_{2k}-A)^{2}\sum_{i=0}^{n+1}(n+1-i)A^{i}={}$
$\displaystyle(I_{2k}-A)^{2}\sum_{i=0}^{n}(n-i)A^{i}+(I_{2k}-A)^{2}\sum_{i=0}^{n}A^{i}$
$\displaystyle\overset{\mathrm{IH}}{=}{}$ $\displaystyle
A^{n+1}-A+n(I_{2k}-A)+(I_{2k}-A)^{2}\sum_{i=0}^{n}A^{i}$ $\displaystyle={}$
$\displaystyle
A-A^{n+1}+n(I_{2k}-A)+(I_{2k}-A)^{2}(I_{2k}-A)^{-1}(I_{2k}-A^{n+1})$
$\displaystyle={}$ $\displaystyle
A-A^{n+1}+n(I_{2k}-A)+I_{2k}-A-A^{n+1}+A^{n+2}$ $\displaystyle={}$
$\displaystyle A^{n+2}-A+(n+1)(I_{2k}-A).$

The remaining series is the following:

$\displaystyle\sum_{n=0}^{\infty}(\frac{1}{2^{k}})^{n}\sum_{i=0}^{n}(n-i)A^{i}={}$
$\displaystyle\sum_{n=0}^{\infty}(\frac{1}{2^{k}})^{n}(I_{2k}-A)^{-2}(A^{n+1}-A+n(I_{2k}-A))$
$\displaystyle={}$
$\displaystyle(I_{2k}-A)^{-2}\left(\sum_{n=0}^{\infty}(\frac{1}{2^{k}})^{n}A^{n+1}-\sum_{n=0}^{\infty}(\frac{1}{2^{k}})^{n}A+\sum_{n=0}^{\infty}(\frac{1}{2^{k}})^{n}n(I_{2k}-A)\right)$
$\displaystyle={}$
$\displaystyle(I_{2k}-A)^{-2}\left(A(I_{2k}-\frac{1}{2^{k}}A)^{-1}-\frac{2^{k}}{2^{k}{-}1}A+\frac{2^{k}}{(2^{k}{-}1)^{2}}(I_{2k}-A)\right).$

We conclude that all expressions in the representation of
${\mathbb{PE}}^{\mathfrak{S}}_{\mathcal{M}}$ above are rational and computable
in polynomial time. ∎

As we have seen, the originally given linear recurrence sequence contains a
negative member if and only if the scheduler $\mathfrak{S}$ is not optimal.
This is the case if and only if
${\mathbb{PE}}^{\max}_{\mathcal{M}}>{\mathbb{PE}}^{\mathfrak{S}}_{\mathcal{M}}$
for the MDP $\mathcal{M}$ constructed from the linear recurrence sequence in
polynomial time above. This finishes the proof of Theorem 4.10.

Conditional SSPP. For the Positivity-hardness of the threshold problem for
conditional expectations, we provide a reduction from the threshold problem
for partial expectations in the following lemma. Note that a reduction in the
other direction is provided in [PB19] rendering the two problems polynomial-
time inter-reducible.

######  Lemma 4.14.

The threshold problems for the partial SSPP is polynomial-time reducible to
the threshold problem of the conditional SSPP.

###### Proof.

Let $\mathcal{M}$ be an MDP with a designated terminal target state
$\mathit{goal}$ and let $\vartheta$ be a rational number. We construct an MDP
$\mathcal{N}$ such that ${\mathbb{PE}}^{\max}_{\mathcal{M}}>\vartheta$ if and
only if ${\mathbb{CE}}^{\max}_{\mathcal{N}}>\vartheta$. We obtain
$\mathcal{N}$ by adding a new initial state $s_{\mathit{\scriptscriptstyle
init}}^{\prime}$, renaming the state $\mathit{goal}$ to
$\mathit{goal}^{\prime}$, and adding a new state $\mathit{goal}$ to
$\mathcal{M}$. In $s_{\mathit{\scriptscriptstyle init}}^{\prime}$, one action
with weight $0$ is enabled leading to the old initial state
$s_{\mathit{\scriptscriptstyle init}}$ and to $\mathit{goal}$ with probability
$1/2$ each. From $\mathit{goal}^{\prime}$ there is one new action leading to
$\mathit{goal}$ with probability $1$ and weight $+\vartheta$.

Each scheduler $\mathfrak{S}$ for $\mathcal{M}$ can be seen as a scheduler for
$\mathcal{N}$ and vice versa. Now, we observe that for any scheduler
$\mathfrak{S}$,

$\mathbb{CE}^{\mathfrak{S}}_{\mathcal{N}}=\frac{1/2(\mathbb{PE}^{\mathfrak{S}}_{\mathcal{M}}+\mathrm{Pr}_{\mathcal{M}}^{\mathfrak{S}}(\lozenge\mathit{goal})\vartheta)}{1/2+1/2\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\lozenge\mathit{goal})}=\frac{\mathbb{PE}^{\mathfrak{S}}_{\mathcal{M}}+\mathrm{Pr}_{\mathcal{M}}^{\mathfrak{S}}(\lozenge\mathit{goal})\vartheta}{1+\mathrm{Pr}_{\mathcal{M}}^{\mathfrak{S}}(\lozenge\mathit{goal})}.$

Hence, ${\mathbb{PE}}^{\max}_{\mathcal{M}}>\vartheta$ if and only if
${\mathbb{CE}}^{\max}_{\mathcal{N}}>\vartheta$. ∎

Together with the Positivity-hardness of the threshold problem for partial
expectations (Theorem 4.10), we conclude:

######  Theorem 4.15.

The Positivity problem is reducible in polynomial time to the following
problem: Given an MDP $\mathcal{M}$ and a rational $\vartheta$, decide whether
${\mathbb{CE}}^{\max}_{\mathcal{M}}>\vartheta$.

#### Two-sided partial SSPP

To conclude this section, we prove the Positivity-hardness of a two sided
version of the partial SSPP with two non-negative weight functions. This
result will form the basis to further Positivity-hardness results in the
subsequent section. The key idea is that, instead of using arbitrary integer
weights, we can simulate the non-monotonic behavior of the accumulated weight
along a path in the partial SSPP with arbitrary weights with two non-negative
weight functions. In the definition of the random variable
$\oplus\mathit{Goal}$, we can replace the choice that paths not reaching
$\mathit{Goal}$ are assigned weight $0$ by a second weight function. Let
$\mathcal{M}=(S,\mathit{Act},\mathrm{Pr},s_{\mathit{\scriptscriptstyle
init}},\mathit{wgt}_{\mathit{goal}},\mathit{wgt}_{\mathit{fail}},\mathit{goal},\mathit{fail})$
be an MDP with two designated terminal states $\mathit{goal}$ and
$\mathit{fail}$ and two non-negative weight functions
$\mathit{wgt}_{\mathit{goal}}\colon S\times\mathit{Act}\to\mathbb{N}$ and
$\mathit{wgt}_{\mathit{fail}}\colon S\times\mathit{Act}\to\mathbb{N}$. Assume
that the probability $\mathrm{Pr}_{\mathcal{M},s_{\mathit{\scriptscriptstyle
init}}}^{\min}(\lozenge\\{\mathit{goal},\mathit{fail}\\})=1$. Define the
following random variable $X$ on maximal paths $\zeta$:

$X(\zeta)=\begin{cases}\mathit{wgt}_{\mathit{goal}}(\zeta)&\text{if
$\zeta\vDash\lozenge\mathit{goal}$,}\\\
\mathit{wgt}_{\mathit{fail}}(\zeta)&\text{if
$\zeta\vDash\lozenge\mathit{fail}$.}\end{cases}$

Due to the assumption that $\mathit{goal}$ or $\mathit{fail}$ is reached
almost surely under any scheduler, the expected value
$\mathbb{E}^{\mathfrak{S}}_{\mathcal{M},s_{\mathit{\scriptscriptstyle
init}}}(X)$ is well-defined for all schedulers $\mathfrak{S}$ for
$\mathcal{M}$. We call the value
$\mathbb{E}^{\max}_{\mathcal{M},s_{\mathit{\scriptscriptstyle
init}}}(X)=\sup_{\mathfrak{S}}\mathbb{E}^{\mathfrak{S}}_{\mathcal{M},s_{\mathit{\scriptscriptstyle
init}}}(X)$ the optimal _two-sided partial expectation_. We can show that the
threshold problem for the two-sided partial expectation is Positivity-hard as
well by a small adjustment of the construction above.

######  Theorem 4.16.

The Positivity problem is polynomial-time reducible to the following problem:
Given an MDP
$\mathcal{M}=(S,\mathit{Act},\mathrm{Pr},s_{\mathit{\scriptscriptstyle
init}},\mathit{wgt}_{\mathit{goal}},\mathit{wgt}_{\mathit{fail}},\mathit{goal},\mathit{fail})$
as above and a rational $\vartheta$, decide whether
$\mathbb{E}^{\max}_{\mathcal{M},s_{\mathit{\scriptscriptstyle
init}}}(X)>\vartheta$.

$t$$x_{j}$$\mathit{goal}$$s$$y_{j}$$\mathit{fail}$$x_{j}^{\prime}$$y_{j}^{\prime}$$p_{2}$$p_{1}$$\gamma_{j}|\mathit{wgt}:+k-j$$\alpha$$p_{2}$$p_{1}$$\alpha$$q_{2}$$q_{1}$$\delta_{j}|\mathit{wgt}:+k-j$$\alpha$$q_{2}$$q_{1}$$\alpha$

Figure 12: The gadget $\mathcal{T}_{\bar{\beta}}$ encoding initial values in
terms of two-sided partial expectations.

###### Proof.

Given the parameters $\alpha_{1},\dots,\alpha_{k}$ and
$\beta_{0},\dots,\beta_{k-1}$ of a rational linear recurrence sequence, we can
construct an MDP
$\mathcal{M}^{\prime}=(S,\mathit{Act},\mathrm{Pr},s_{\mathit{\scriptscriptstyle
init}},\mathit{wgt},\mathit{goal},\mathit{fail})$ with one weight function
$\mathit{wgt}\colon S\times\mathit{Act}\to\mathbb{Z}$ similar to the MDP
$\mathcal{M}$ depicted in Figure 11. W.l.o.g., we again assume that
$\sum_{i}|\alpha_{i}|<\frac{1}{4}$ and that
$0\leq\beta_{j}<\frac{1}{4k^{2k+2}}$ for all $j$. The initial gadget and the
gadget $\mathcal{G}_{\bar{\alpha}}$ are as before. The gadget
$\mathcal{P}_{\bar{\beta}}$, however, is slightly modified and replaced by the
gadget $\mathcal{T}_{\bar{\beta}}$ depicted in Figure 12. For this gadget, we
define $\alpha=\sum_{i=1}^{k}|\alpha_{i}|$,
$p_{1}=(1-\alpha)(\frac{1}{2k^{2(k-j)}}+\beta_{j})$,
$p_{2}=(1-\alpha)(1-(\frac{1}{2k^{2(k-j)}}+\beta_{j}))$,
$q_{1}=(1-\alpha)\frac{1}{2k^{2(k-j)}}$, and
$q_{2}=(1-\alpha)(1-\frac{1}{2k^{2(k-j)}})$. With the transitions as in the
figure, the probability to reach $\mathit{goal}$ or $\mathit{fail}$ and the
weight accumulated does not change when choosing action $\gamma_{j}$ or
$\delta_{j}$ compared to the gadget $\mathcal{P}_{\bar{\beta}}$. The only
difference is that the expected time to reach $\mathit{goal}$ or
$\mathit{fail}$ changes. The steps alternate between probability $\alpha$ and
probability $0$ to reach $\mathit{goal}$ or $\mathit{fail}$ – just as in the
gadget $\mathcal{G}_{\bar{\alpha}}$. In this way, it makes no difference for
the expected time before reaching $\mathit{goal}$ or $\mathit{fail}$ when a
scheduler stops choosing $\gamma$ and $\delta$. We can, in fact, compute the
expected time $T$ to reach $\mathit{goal}$ or $\mathit{fail}$ from
$s_{\mathit{\scriptscriptstyle init}}$ under any scheduler quite easily:
Reaching $t$ or $s$ takes $3$ steps in expectation. Afterwards, two further
steps are taken $1/\alpha$-many times in expectation. So,

$T=3+\frac{2}{\alpha}.$

The optimal scheduler $\mathfrak{S}$ for the partial expectation in
$\mathcal{M}^{\prime}$ is the same as in the MDP $\mathcal{M}$ above. Also the
value $\vartheta$ of this scheduler can be computed as in Theorem 4.13. So,
$\mathbb{PE}^{\max}_{\mathcal{M}^{\prime},s_{\mathit{\scriptscriptstyle
init}}}>\vartheta$ if and only if the given linear recurrence sequence is
eventually negative.

Note that all weights in $\mathcal{M}^{\prime}$ are $\geq-k$. We define two
new weight functions to obtain an MDP $\mathcal{N}$ from
$\mathcal{M}^{\prime}$: We let
$\mathit{wgt}_{\mathit{goal}}(s,\alpha)=\mathit{wgt}(s,\alpha)+k$ and
$\mathit{wgt}_{\mathit{fail}}(s,\alpha)=+k$ for all $(s,\alpha)\in
S\times\mathit{Act}$. Both weight functions take only non-negative integer
values.

Any scheduler $\mathfrak{S}$ for $\mathcal{M}^{\prime}$ can be viewed as a
scheduler for $\mathcal{N}$, and vice versa, as the two MDPs only differ in
the weight functions. Further, we observe that for each maximal path $\zeta$
ending in $\mathit{goal}$ or $\mathit{fail}$ in $\mathcal{M}^{\prime}$ and at
the same time in $\mathcal{N}$, we have
$X(\zeta)=\oplus\mathit{goal}(\zeta)+k\cdot\mathit{length}(\zeta)$. (Recall
that $\oplus\mathit{goal}(\zeta)$ equals $\mathit{wgt}(\zeta)$ if $\zeta$
reaches $\mathit{goal}$ and $0$ if $\zeta$ reaches $\mathit{fail}$.) As the
expected time before $\mathit{goal}$ or $\mathit{fail}$ is reached is
constant, namely $T$ under any scheduler, it follows that for all schedulers
$\mathfrak{T}$ we have

$\mathbb{E}^{\mathfrak{T}}_{\mathcal{N},s_{\mathit{\scriptscriptstyle
init}}}(X)=\mathbb{PE}^{\mathfrak{T}}_{\mathcal{M}^{\prime},s_{\mathit{\scriptscriptstyle
init}}}+k\cdot T.$

Therefore, $\mathbb{E}^{\max}_{\mathcal{N},s_{\mathit{\scriptscriptstyle
init}}}(X)>\vartheta+k\cdot T$ if and only if the given linear recurrence
sequence eventually becomes negative. ∎

While the two-sided partial expectation is certainly interesting in its own
right, it will also play an important role in the proof of the Positivity-
hardness of the threshold problem for the optimal long-run probability of a
regular co-safety property in the next section.

###  4.3 Long-run probabilities and frequency-LTL

We now turn our attention to problems concerning the long-run satisfaction of
path properties. On first sight, these problems seem to be of quite a
different nature compared to the problems addressed so far. Long-run
probabilities are an average of the probability after each step that a
property $\varphi$ is satisfied on the suffix of an execution starting after
that step. Similarly, frequency-LTL allows us to express that the long-run
fraction of suffixes of an execution satisfying $\varphi$ lies above a
threshold. Nevertheless, upon closer inspection, the two-sided version of
partial expectations considered at the end of the previous section actually
shares similarities with these long-run satisfaction problems. This allows us
to provide a reduction from the threshold problem for two-sided partial
expectations to the threshold problem for long-run probabilities of a simple
fixed co-safety property. We begin by formally defining long-run
probabilities.

#### Long-run probability.

Let $\mathcal{M}=(S,\mathit{Act},P,s_{\mathit{\scriptscriptstyle
init}},\mathsf{AP},\mathsf{L})$ be an MDP and let $\varphi$ be a path
property. The _long-run probability_ of $\varphi$ on an infinite path $\zeta$
under a scheduler $\mathfrak{S}$ for $\mathcal{M}$ is defined as as the long-
run average of the probabilities for $\varphi$ in all positions of $\zeta$
with respect to the residual schedulers $\mathfrak{S}{\uparrow}{\zeta[0\dots
i]}$ defined by

$\mathfrak{S}{\uparrow}{\zeta[0\dots i]}(\pi)=\mathfrak{S}(\zeta{[0\dots
i]}\cdot\pi)$

for finite paths $\pi$ starting in $\zeta[i]$:

$\mathit{lrp}^{\mathfrak{S}}_{\scriptscriptstyle\varphi}(\zeta)\quad=\quad\liminf_{n\to\infty}\
\frac{1}{n{+}1}\cdot\sum_{i=0}^{n}\mathrm{Pr}^{\mathfrak{S}{\uparrow}{\zeta[0\dots
i]}}_{\mathcal{M},{\zeta}[i]}(\varphi)\enspace.$

The long-run probability of property $\varphi$ under scheduler $\mathfrak{S}$
from state $s$, denoted $\mathbb{LP}^{\mathfrak{S}}_{\mathcal{M},s}(\varphi)$,
is defined as the expectation of the random variable
$\zeta\mapsto\mathit{lrp}^{\mathfrak{S}}_{\scriptscriptstyle\varphi}(\zeta)$
under $\mathfrak{S}$ with starting state $s$:

$\mathbb{LP}^{\mathfrak{S}}_{\mathcal{M},s}(\varphi)=\mathbb{E}^{\mathfrak{S}}_{\mathcal{M},s_{\mathit{\scriptscriptstyle
init}}}(\mathit{lrp}^{\mathfrak{S}}_{\scriptscriptstyle\varphi}).$

We now address the task to compute the extremal long-run probabilities for
$\varphi$:

$\begin{array}[]{lcc@{\hspace*{0.15cm}}l}\mathbb{LP}^{\max}_{\mathcal{M},s}(\varphi)&=&\sup\limits_{\mathfrak{S}}\hfil\hskip
4.26773pt&\mathbb{LP}^{\mathfrak{S}}_{\mathcal{M},s}(\varphi)\text{ and}\\\
\mathbb{LP}^{\min}_{\mathcal{M},s}(\varphi)&=&\inf\limits_{\mathfrak{S}}\hfil\hskip
4.26773pt&\mathbb{LP}^{\mathfrak{S}}_{\mathcal{M},s}(\varphi)\end{array}$

where $\mathfrak{S}$ ranges over all schedulers for $\mathcal{M}$. In contrast
to classical optimization problems for MDPs, the random variable whose
expectation we aim to optimize, namely
$\mathit{lrp}^{\mathfrak{S}}_{\scriptscriptstyle\varphi}$, depends on the
scheduler $\mathfrak{S}$ itself.

######  Example 4.17.

To illustrate the notion of long-run probability, consider the following
example, which is a simplification of an example from [BBPS19]. Let
$\mathcal{N}$ be the MDP shown in Fig. 13. The only non-deterministic choice
is the choice between actions $\alpha$ and $\beta$ in state $a$. Action
$\alpha$ yields a uniform distribution over the three successors.

$a$$b_{1}$$c_{1}$$b_{2}$$c_{2}$$\alpha$$\beta$$\frac{1}{2}$$\frac{1}{2}$

Figure 13: MDP with labels indicated by the state names requiring counting to
maximize the long-run probability of $a{\mathrm{U}}b$.

We want to determine the maximal long-run probability of $a{\mathrm{U}}b$.
Under the memoryless scheduler $\mathfrak{S}_{\alpha}$ that always picks
action $\alpha$, the probability of $a{\mathrm{U}}b$ in the $a$-state is
$\frac{1}{2}$ under this scheduler. The states $b_{1}$ and $c_{1}$ appear
equally often. The probability of $a{\mathrm{U}}b$ is $1$ in state $b_{1}$ and
$0$ in state $c_{1}$. We thus conclude that the long-run probability under
$\mathfrak{S}_{\alpha}$ is $\frac{1}{2}$. Similarly, the steady-state
probability of the states $a$ and $b_{2}$ under the memoryless scheduler
$\mathfrak{S}_{\beta}$ are $\frac{1}{4}$, and the probability that
$a{\mathrm{U}}b$ holds from there is $1$. The long-run probability of
$a{\mathrm{U}}b$ under $\mathfrak{S}_{\beta}$ equals $\frac{1}{2}$ as well.
Interestingly, these two memoryless schedulers are not optimal. Consider the
scheduler $\mathfrak{S}$ that chooses $\alpha$ first and, if it returns to $a$
directly, chooses $\beta$ afterwards. In the first visit to the $a$ state, the
probability for $a{\mathrm{U}}b$ is $\frac{2}{3}$. States $b_{1}$ and $c_{1}$
are reached with probability $1/3$ afterwards. If state $a$ is reached again
directly, the probability of $a{\mathrm{U}}b$ is now $1$. Also state $b_{2}$
is reached with probability $1/3$ before returning to $a$ from $b_{1}$,
$c_{1}$, or $c_{2}$. Tho compute the long-run probability under this
scheduler, we sum up the satisfaction probabilities for all states that can be
visited before returning to $a$ from $b_{1}$, $c_{1}$, or $c_{2}$ multiplied
with the probabilities of the visits. We divide the result by the expected
number of steps before returning. Note that we sum up probability
$2/3+1/3\cdot 1$ for the two possible visits to state $a$. We obtain a long-
run probability of

$\frac{2/3+1/3+1/3+1/3}{2/3\cdot 2+1/3\cdot 5}=\frac{5}{9}.$

#### Preliminary results.

Before we prove the Positivity-hardness result for long-run probabilities, we
need some results on the connection between long-run probabilities and mean
payoffs. The results are presented in [Pir21] and we briefly state the
necessary results in the sequel.

We will prove that the threshold problem for the maximal long-run probability
is Positivity-hard already for very simple co-safety properties $\varphi$. To
represent regular co-safety properties, we will use deterministic finite-
automata (DFA). A run $\zeta$ satisfies the represented co-safety property if
some prefix of $L(\zeta)$ is accepted by the DFA.

In [Pir21], a construction is provided that allows us to express the optimal
long-run probability of regular co-safety properties in terms of expected mean
payoffs. We briefly present this reduction and the corresponding results here:
The main idea is to construct an MDP with extended state space that keeps
track of the number of runs currently in each state of the automaton. We can
then assign a weight to each step of the MDP depending on how many runs of the
DFA enter an accepting state during that step. The optimal mean payoff in the
constructed MDP then coincides with the optimal long-run probability in the
original MDP. However, there is no bound on the number of runs we have to
store in the state space for this construction. Therefore, the constructed MDP
will have an infinite state space.

Let $\mathcal{M}=(S,\mathit{Act},P,s_{\mathit{\scriptscriptstyle
init}},\mathsf{AP},L)$ be a strongly connected MDP and let
$\mathcal{D}=(Q,2^{\mathsf{AP}},\delta,q_{0},F)$ be a DFA over $\mathsf{AP}$.
As we are interested in the co-safety property given by $\mathcal{D}$, only
runs of $\mathcal{D}$ up to the first accepting state are relevant. Hence, we
can collapse all accepting states of $\mathcal{D}$ to one absorbing state
$\mathit{accept}$ and all states form which $\mathit{accept}$ is not reachable
to one state $\mathit{reject}$. Let the set of states
$Q=\\{q_{0},q_{1},\dots,q_{\ell},\mathit{accept},\mathit{reject}\\}$ for some
$\ell\in\mathbb{N}$.

We construct a weighted infinite-state MDP
$\mathcal{M}_{\mathcal{D}}=(S^{\prime},\mathit{Act},P^{\prime},s_{\mathit{\scriptscriptstyle
init}}^{\prime},\mathit{wgt})$ in the sequel. The state space is

$S^{\prime}=S\times\mathbb{N}^{\ell+1}.$

The $\ell+1$ natural numbers in a state store the number of runs of
$\mathcal{D}$ on suffixes of the path produced by the MDP so far that are in
the respective state of $\mathcal{D}$. The actions $\mathit{Act}$ are the same
as in $\mathcal{M}$. For the transition probability function $P^{\prime}$ we
define the following: Let $s^{\prime}=(s,n_{0},\dots,n_{\ell})$ and
$t^{\prime}=(t,m_{0},\dots,m_{\ell})$ be states such that for all $i$,

$m_{i}=\iota_{i}+\sum_{j:\delta(q_{j},L(t))=q_{i}}n_{j}$

where $\iota_{i}=1$ if $i=0$ and $\iota_{i}=0$ otherwise. For such states, we
set

$P^{\prime}(s^{\prime},\alpha,t^{\prime})=P(s,\alpha,t).$

All other transition probabilities are $0$. The weight function does not work
on state-weight pairs as usual, but on single transitions in
$S^{\prime}\times\mathit{Act}\times S^{\prime}$. For a transition
$(s^{\prime},\alpha,t^{\prime})$ with $s^{\prime}=(s,n_{0},\dots,n_{\ell})$
and $t^{\prime}=(t,m_{0},\dots,m_{\ell})$, the weight is defined by

$\mathit{wgt}(s^{\prime},\alpha,t^{\prime})=\sum_{j:\delta(q_{j},L(t))=\mathit{accept}}n_{j}.$

To obtain a weight function on state-weight pairs, one could now take the
weighted average over all possible transitions that can be taken via a state
action-pair. As we will be interested in the mean payoff under this weight
function, this change would not influence the subsequent considerations. The
initial state $s_{\mathit{\scriptscriptstyle init}}^{\prime}$ is
$(s_{\mathit{\scriptscriptstyle init}},1,0,\dots,0)$.

We observe that the sum of the entries in the last $\ell+1$ components
increases by at most $1$ in each step. Hence, the total accumulated weight
after $n$ steps along any path is bounded by $n$ and we can already conclude
that the mean payoff in $\mathcal{M}_{\mathcal{D}}$ is bounded by $1$ along
each path.

A scheduler for $\mathcal{M}$ can be used as a scheduler for
$\mathcal{M}_{\mathcal{D}}$ and vice versa as transitions in
$\mathcal{M}_{\mathcal{D}}$ are uniquely defined by the transitions in the
$\mathcal{M}$ component. If we consider a scheduler $\mathfrak{S}$ for both
$\mathcal{M}$ and $\mathcal{M}_{\mathcal{D}}$, there is, however, one caveat:
If $\mathfrak{S}$ is a finite memory-scheduler for
$\mathcal{M}_{\mathcal{D}}$, the same scheduler is not necessarily a finite-
memory scheduler for $\mathcal{M}$. So, we want to emphasize that the
following lemma states that the maximal mean payoff in
$\mathcal{M}_{\mathcal{D}}$ can be approximated by schedulers that are still
finite-memory schedulers when considered as schedulers for $\mathcal{M}$.

######  Lemma 4.18 ([Pir21]).

Let $\mathcal{M}$ and $\mathcal{D}$ be given as above and let
$\mathcal{M}_{\mathcal{D}}$ be the constructed MDP. For each scheduler
$\mathfrak{T}$ for $\mathcal{M}_{\mathcal{D}}$ and each $\varepsilon>0$, there
is a finite-memory scheduler $\mathfrak{F}$ for $\mathcal{M}$ such that, if
$\mathfrak{F}$ is seen as a scheduler for $\mathcal{M}_{\mathcal{D}}$:

$\mathbb{E}^{\mathfrak{F}}_{\mathcal{M}_{\mathcal{D}},s_{\mathit{\scriptscriptstyle
init}}^{\prime}}(\mathit{MP})\geq\mathbb{E}^{\mathfrak{T}}_{\mathcal{M}_{\mathcal{D}},s_{\mathit{\scriptscriptstyle
init}}^{\prime}}(\mathit{MP})-\varepsilon.$

For finite-memory schedulers, the mean-payoff in $\mathcal{M}_{\mathcal{D}}$
and the long-run probability of the co-safety property given by $\mathcal{D}$
in $\mathcal{M}$ coincide:

######  Lemma 4.19 ([Pir21]).

Let $\mathcal{M}$ and $\mathcal{D}$ be given as above and let
$\mathcal{M}_{\mathcal{D}}$ be the constructed MDP. Then, for each finite-
memory scheduler $\mathfrak{S}$ for $\mathcal{M}$ (also viewed as a scheduler
for $\mathcal{M}_{\mathcal{D}}$), we have
$\mathbb{LP}^{\mathfrak{S}}_{\mathcal{M},s_{\mathit{\scriptscriptstyle
init}}}(\mathcal{D})=\mathbb{E}^{\mathfrak{S}}_{\mathcal{M}_{\mathcal{D}},s_{\mathit{\scriptscriptstyle
init}}^{\prime}}(\mathit{MP)}$.

As shown in [Pir21], using Fatou’s lemma, one can show that also the optimal
long-run probability can be approximated by finite-memory schedulers:

######  Lemma 4.20 ([Pir21]).

Let $\mathcal{M}$ and $\varphi$ be given as above. For each scheduler
$\mathfrak{T}$ for $\mathcal{M}$ and each $\varepsilon>0$, there is a finite-
memory scheduler $\mathfrak{F}$ for $\mathcal{M}$ such that:

$\mathbb{LP}^{\mathfrak{F}}_{\mathcal{M},s_{\mathit{\scriptscriptstyle
init}}}(\varphi)\geq\mathbb{LP}^{\mathfrak{T}}_{\mathcal{M},s_{\mathit{\scriptscriptstyle
init}}}(\varphi)-\varepsilon.$

It follows that indeed, the optimal long-run probability can be expressed as
an optimal expected mean payoff via the provided reduction.

######  Theorem 4.21 ([Pir21]).

Let $\mathcal{M}$ and $\mathcal{D}$ be as above. Let
$\mathcal{M}_{\mathcal{D}}$ be the infinite-state MDP constructed from
$\mathcal{M}$ and $\mathcal{D}$ as described above. Then,

$\mathbb{LP}^{\max}_{\mathcal{M},s_{\mathit{\scriptscriptstyle
init}}}(\mathcal{D})=\mathbb{E}^{\max}_{\mathcal{M}_{\mathcal{D}},s_{\mathit{\scriptscriptstyle
init}}^{\prime}}(\mathit{MP}).$

#### Positivity-hardness.

So far, we have seen that the optimal long-run probability of a regular co-
safety can be expressed in terms of an optimal expected mean-payoff. This
insight allows us to draw a connection between long-run probabilities and two
sided-partial expectations that we just discussed. Recall that for an MDP
$\mathcal{M}=(S,\mathit{Act},\mathrm{Pr},s_{\mathit{\scriptscriptstyle
init}},\mathit{wgt}_{\mathit{goal}},\mathit{wgt}_{\mathit{fail}},\mathit{goal},\mathit{fail})$
with two designated absorbing states $\mathit{goal}$ and $\mathit{fail}$ and
two non-negative weight functions $\mathit{wgt}_{\mathit{goal}}\colon
S\times\mathit{Act}\to\mathbb{N}$ and $\mathit{wgt}_{\mathit{fail}}\colon
S\times\mathit{Act}\to\mathbb{N}$, the two-sided partial expectation was
defined as the expectation of the following random variable $X$ on maximal
paths $\zeta$:

$X(\zeta)=\begin{cases}\mathit{wgt}_{\mathit{goal}}(\zeta)&\text{if
$\zeta\vDash\lozenge\mathit{goal}$,}\\\
\mathit{wgt}_{\mathit{fail}}(\zeta)&\text{if
$\zeta\vDash\lozenge\mathit{fail}$.}\end{cases}$

We now exploit the construction of $\mathcal{M}_{\mathcal{D}}$ provided above
to mimic a behavior similar to the payoff according to the random variable
$X$. Consider the DFA $\mathcal{D}$ depicted in Figure 14. The state space is
$Q=\\{q_{{\mathit{\scriptscriptstyle
init}}},q_{1},q_{2},\mathit{accept},\mathit{reject}\\}$. The alphabet is
$2^{\\{a,b,c,\mathit{goal},\mathit{fail}\\}}$. From the initial state letters
satisfying $a\land b\land\neg c$ lead to $q_{1}$, letters satisfying $a\land
c\land\neg b$ to $q_{2}$ and all remaining letters to $\mathit{reject}$. From
$q_{1}$, letters satisfying $a\land\neg\mathit{goal}$ lead back to $q_{1}$,
letters with $\mathit{goal}\land\neg a$ to $\mathit{accept}$, and all
remaining letters lead to $\mathit{reject}$. Transitions from $q_{2}$ are
defined analogously with $\mathit{goal}$ replaced by $\mathit{fail}$.

$q_{{\mathit{\scriptscriptstyle init}}}$$q_{1}$$q_{2}$$a\land b\land\neg
c$$\mathit{goal}\land\neg a$$a\land c\land\neg b$$\mathit{fail}\land\neg
a$$a\land\neg\mathit{goal}$$a\land\neg\mathit{fail}$

Figure 14: The DFA $\mathcal{D}$ mimicking two-sided partial expectations. All
transitions on letters not satisfying one of the labels lead to a rejecting
sink that is not depicted.

Consider a run $\rho$ of an MDP $\mathcal{M}$ labeled with
$\\{a,b,c,\mathit{goal},\mathit{fail}\\}$ for which we keep counters of the
number of runs on suffixes of $\rho$ in each of the states of $\mathcal{D}$:
We only need counters $c_{1}$ and $c_{2}$ for states $q_{1}$ and $q_{2}$ as
these are the only states multiple runs can be in before being accepted or
rejected. The update of the counters in the MDP $\mathcal{M}_{\mathcal{D}}$
can directly be determined from the DFA $\mathcal{D}$: E.g., if $\\{a,b\\}$ is
read, counter $c_{1}$ is increased; if $\\{a,c\\}$ is read, counter $c_{2}$ is
increased. On $\\{a\\}$, both counters stay the same. If no $a$ is read, the
counters are reset to $0$. If at the same time $\mathit{goal}$ is read, the
value of $c_{1}$ is received as weight. If $\mathit{fail}$ is read, the value
of $c_{2}$ is received as weight. So, the behavior of the counters is very
similar to the accumulation of two non-negative weight functions. Which of the
two weight functions or the two counters is used to determine the payoff
depends on whether $\mathit{goal}$ or $\mathit{fail}$ is reached next. In the
sequel, we will show that indeed already the fixed co-safety property of this
simple DFA $\mathcal{D}$ suffices to prove Positivity-hardness of the
threshold problem for long-run probabilities.

The proof of the Positivity-hardness of the threshold problem for the two-
sided partial expectation with non-negative weights contains most of the
necessary ingredients we need: Let $(u_{n})_{n\geq 0}$ be a rational linear
recurrence sequence given by initial values $\beta_{0},\dots,\beta_{k-1}$ and
the coefficients $\alpha_{1},\dots,\alpha_{k}$ of the recurrence. In the proof
of Theorem 4.16, we showed that we can construct an MDP
$\mathcal{M}=(S,\mathit{Act},\mathrm{Pr},s_{\mathit{\scriptscriptstyle
init}},\mathit{wgt}_{\mathit{goal}},\mathit{wgt}_{\mathit{fail}},\mathit{goal},\mathit{fail})$
and rationals $\vartheta$, $T$ with the following properties from the given
parameters:

  * •

For the two designated states $\mathit{goal}$ and $\mathit{fail}$, we have
$\mathrm{Pr}_{\mathcal{M},s_{\mathit{\scriptscriptstyle
init}}}^{\min}(\lozenge\\{\mathit{goal},\mathit{fail}\\})=1$.

  * •

The expected number of steps until $\mathit{goal}$ or $\mathit{fail}$ is
reached is $T$ under any scheduler.

  * •

The weight functions $\mathit{wgt}_{\mathit{goal}}$ and
$\mathit{wgt}_{\mathit{fail}}$ assign a weight between $0$ and $2k$ to each
state-action pair.

  * •

$\mathbb{E}^{\max}_{\mathcal{M},s_{\mathit{\scriptscriptstyle
init}}}(X)>\vartheta$ if and only if there is an $n$ with $u_{n}<0$.

$s$$t$$v$$s$$r_{s,\alpha}^{1}$$\dots$$r_{s,\alpha}^{4k}$$t$$v$$p_{1}$$\alpha$$p_{2}$$\alpha$$p_{1}$$p_{2}$

Figure 15: Construction of $\mathcal{K}$.

From this MDP $\mathcal{M}$, we now construct a labeled MDP $\mathcal{K}$. For
each state-action pair $(s,\alpha)$ of $\mathcal{M}$ with
$s\not\in\\{\mathit{goal},\mathit{fail}\\}$, we add a chain
$r_{s,\alpha}^{1},\dots,r_{s,\alpha}^{4k}$ of new states as depicted in Figure
15: We redirect the transition from $s$ when choosing $\alpha$ to this chain
by setting $P_{\mathcal{K}}(s,\alpha,r_{s,\alpha}^{1})$. In the states of the
chain only one action $\tau$ is enabled. The process moves through the chain
with probability $1$ via this action, i.e.,
$P_{\mathcal{K}}(r_{s,\alpha}^{i},\tau,r_{s,\alpha}^{i+1})=1$ for all $i<4k$.
Then, the original transition is taken from the state $r_{s,\alpha}^{4k}$ by
setting $P_{\mathcal{K}}(r_{s,\alpha}^{4k},\tau,t)=P(s,\alpha,t)$ for all
states $t$ of $\mathcal{M}$. Instead of making $\mathit{goal}$ and
$\mathit{fail}$ absorbing, we furthermore add transitions back to the initial
state $s_{\mathit{\scriptscriptstyle init}}$ from $\mathit{goal}$ and
$\mathit{fail}$ with probability $1$. Note that the expected time from
$s_{\mathit{\scriptscriptstyle init}}$ until $s_{\mathit{\scriptscriptstyle
init}}$ is reached again from $\mathit{goal}$ or $\mathit{fail}$ is now
$T^{\prime}=T(4k+1)+1$ in $\mathcal{K}$ under any scheduler.

The labeling is defined as follows: All states except for $\mathit{goal}$ and
$\mathit{fail}$ are labeled with $a$. States $\mathit{goal}$ and
$\mathit{fail}$ are labeled with their names. Furthermore, in each of the
chains $r_{s,\alpha}^{1},\dots,r_{s,\alpha}^{4k}$, the first
$\mathit{wgt}_{\mathit{goal}}(s,\alpha)$ of the states are labeled with $b$ in
addition to the label $a$. The next $\mathit{wgt}_{\mathit{fail}}(s,\alpha)$
states are labeled with $c$ in addition to the $a$. As
$\mathit{wgt}_{\mathit{goal}}(s,\alpha)+\mathit{wgt}_{\mathit{fail}}(s,\alpha)\leq
4k$, this is always possible.

Consider now a path $\pi$ of $\mathcal{M}$ from $s_{\mathit{\scriptscriptstyle
init}}$ to $\mathit{goal}$ or $\mathit{fail}$. There is a unique corresponding
path $\hat{\pi}$ in $\mathcal{K}$. The counters induced by the DFA
$\mathcal{D}$ as described above now behave exactly like the accumulation
weight functions $\mathit{wgt}_{\mathit{goal}}$ and
$\mathit{wgt}_{\mathit{fail}}$. The value $c_{1}$ counting the number of runs
in state $q_{1}$ of $\mathcal{D}$ is precisely
$\mathit{wgt}_{\mathit{goal}}(\pi)$ when entering $\mathit{goal}$ or
$\mathit{fail}$ as in each chain of states
$r_{s,\alpha}^{1},\dots,r_{s,\alpha}^{4k}$ exactly
$\mathit{wgt}_{\mathit{goal}}(s,\alpha)$-many runs of $\mathcal{D}$ enter
state $q_{1}$. The counter $c_{2}$ behaves analogously in terms of the weight
function $\mathit{wgt}_{\mathit{fail}}$. As all states not in
$\\{\mathit{goal},\mathit{fail}\\}$ are labeled with $a$, the counters are
also not reset. When entering $\mathit{goal}$, the random variable $X$ assigns
weight $\mathit{wgt}_{\mathit{goal}}(\pi)$ to the path $\pi$. The same weight
is received from the counter $c_{1}$ in this case. When entering
$\mathit{fail}$, weight $\mathit{wgt}_{\mathit{fail}}(\pi)$ is assigned by $X$
and received from the counters.

As the time required to reach $s_{\mathit{\scriptscriptstyle init}}$ again
from $\mathit{goal}$ or $\mathit{fail}$ in $\mathcal{K}$ in expectation is
$T^{\prime}$ under any scheduler, a scheduler maximizing the expected mean
payoff in $\mathcal{K}_{\mathcal{D}}$, i.e., according to the weight function
induced by the counter for $\mathcal{D}$, hence has to maximize the expected
value of $X$ when considered as a scheduler for $\mathcal{M}$. By Theorem
4.21, the maximal mean payoff in $\mathcal{K}_{\mathcal{D}}$ equals the
maximal long-run probability
$\mathbb{LP}^{\max}_{\mathcal{K},s_{\mathit{\scriptscriptstyle
init}}}(\mathcal{D})$. Putting these results together, we obtain that

$\mathbb{LP}^{\max}_{\mathcal{K},s_{\mathit{\scriptscriptstyle
init}}}(\mathcal{D})>\frac{\vartheta}{T^{\prime}}$

if and only if the given linear recurrence sequence is eventually negative. We
conclude the Positivity-hardness result for long-run probabilities. Note that
the Positivity-hardness holds for the fixed simple DFA $\mathcal{D}$.

######  Theorem 4.22.

There is a fixed DFA $\mathcal{D}$ such that the Positivity problem is
polynomial-time reducible to the following problem: Given an MDP $\mathcal{M}$
and a rational $\chi$, decide whether
$\mathbb{LP}^{\max}_{\mathcal{M}}(\mathcal{D})>\chi$.

#### Frequency-LTL.

A consequence of this result is that model checking of frequency-LTL in MDPs
is at least as hard as the Positivity problem. Whether the model-checking
problem for the full logic frequency-LTL is decidable has been raised as an
open question in [FK15, FKK15]. Our result now shows that proving decidability
of this model-checking problem would render the Positivity problem decidable
as well. The frequency-globally modality $G^{>\vartheta}_{\inf}(\varphi)$ of
frequency-LTL is defined to hold on a path $\pi$ iff

$\liminf_{n\to\infty}\frac{1}{n+1}\sum_{i=0}^{n}\mathds{1}_{\pi[i\dots]\vDash\varphi}>\vartheta,$

i.e. iff the long-run frequency of $\varphi$ exceeds $\vartheta$.

######  Theorem 4.23.

There is a polynomial-time reduction from the Positivity problem to the
following qualitative model checking problem for frequency-LTL for a fixed
LTL-formula $\varphi$: Given an MDP $\mathcal{M}$ and a rational $\vartheta$,
is $\mathrm{Pr}^{\max}_{\mathcal{M}}(G^{>\vartheta}_{\inf}(\varphi))=1$?

###### Proof.

Consider the MDP $\mathcal{K}$, the DFA $\mathcal{D}$, and the threshold
$\vartheta^{\prime}={\vartheta}/{T^{\prime}}$ constructed above. As the sets
of states labeled with $b$ and with $c$ are disjoint and included in the set
of states labeled with $a$, and likewise the sets of states labeled with $a$,
$\mathit{goal}$, and $\mathit{fail}$ are pairwise disjoint in $\mathcal{K}$, a
path of $\mathcal{K}$ has a prefix accepted by $\mathcal{D}$ if and only if
the path satisfies

$\varphi=(b\land(a{\mathrm{U}}\mathit{goal}))\lor(c\land(a{\mathrm{U}}\mathit{fail}).$

We claim that there is a scheduler $\mathfrak{S}$ with
$\mathbb{LP}^{\mathfrak{S}}_{\mathcal{K},s_{\mathit{\scriptscriptstyle
init}}}(\mathcal{D})>\vartheta^{\prime}$ if and only if there is a scheduler
$\mathfrak{T}$ such that $G^{>\vartheta}_{\inf}(\varphi)$ holds with
probability $1$ under $\mathfrak{T}$ in $\mathcal{K}$.

Suppose there is a scheduler with $\mathfrak{S}$ with
$\mathbb{LP}_{\mathcal{K}}^{\mathfrak{S}}(\mathcal{D})>\vartheta^{\prime}$. By
Lemma 4.20, we can assume that $\mathfrak{S}$ is a finite-memory scheduler as
the maximal long-run probability can be approximated by finite-memory
schedulers. As $\mathcal{K}$ is strongly connected, we can further assume that
$\mathfrak{S}$ induces only one BSCC. We claim that under this scheduler
$\mathfrak{S}$ also $G^{>\vartheta}_{\inf}(\varphi)$ holds with probability
$1$. For finite-memory schedulers, it is easy to check that the expected long-
run probability equals the expected long-run frequency as we obtain a finite-
state Markov chain: Let $x_{\mathfrak{s}}$ be the steady state probability of
states $\mathfrak{s}$ enriched with memory modes in the single BSCC
$\mathcal{B}^{\mathfrak{S}}$ induced by $\mathfrak{S}$. Further, let
$p_{\mathfrak{s}}$ be the probability that a run starting in $\mathfrak{s}$
under $\mathfrak{S}$ satisfies $\varphi$. Then,
$\mathbb{LP}_{\mathcal{K}}^{\mathfrak{S}}(\mathcal{D})=\sum_{\mathfrak{s}\in\mathcal{B}^{\mathfrak{S}}}x_{\mathfrak{s}}\cdot
p_{\mathfrak{s}}$. But the same expression also computes the expected
frequency with which $\varphi$ holds on suffixes as shown in [FK15].
Furthermore, in a strongly connected Markov chain, the frequency of $\varphi$
along almost all paths agrees with the expected frequency (see [FK15]). So,

$\liminf_{n\to\infty}\frac{1}{n+1}\sum_{i=0}^{n}\mathds{1}_{\zeta[i\dots]\vDash\varphi}>\vartheta$

holds on almost all paths $\zeta$.

Conversely, if there is a scheduler $\mathfrak{T}$ such that
$G^{>\vartheta}_{\inf}(\varphi)$ holds with probability $1$ under
$\mathfrak{T}$ in $\mathcal{K}$, the expected value
$\mathbb{E}_{\mathcal{K}}^{\mathfrak{S}}(\liminf_{n\to\infty}\frac{1}{n+1}\sum_{i=0}^{n}\mathds{1}_{\varsigma[i\dots]\vDash\varphi})>\vartheta$.
By an argument using Fatou’s lemma analogously to the proof of Lemma 4.20 in
[Pir21], we can find a finite memory scheduler with expected long-run
frequency, and hence long-run probability, greater than $\vartheta$. ∎

###  4.4 Conditional value-at-risk for accumulated weights

Lastly, we aim to prove the Positivity-hardness of the threshold problem for
the CVaR in this section. To this end, we provide a further direct reduction
from the Positivity-problem to the threshold problem for the expected value of
an auxiliary random variable closely related to the CVaR using our MDP-
gadgets.

#### Conditional Value-at-Risk.

Given an MDP $\mathcal{M}=(S,\mathit{Act},P,s_{\mathit{\scriptscriptstyle
init}},\mathit{wgt},\mathit{Goal})$ with a scheduler $\mathfrak{S}$, a random
variable $X$ defined on runs of the MDP with values in $\mathbb{R}$ and a
value $p\in[0,1]$, we define the value-at-risk as
$\mathit{VaR}^{\mathfrak{S}}_{p}(X)=\sup\\{r\in\mathbb{R}|\mathrm{Pr}_{\mathcal{M}}^{\mathfrak{S}}(X\leq
r)\leq p\\}$. So, the value-at-risk is the point at which the cumulative
distribution function of $X$ reaches or exceeds $p$. The conditional value-at-
risk is now the expectation of $X$ under the condition that the outcome
belongs to the $p$ worst outcomes – in this case, the $p$ lowest outcomes.
Denote $\mathit{VaR}_{p}^{\mathfrak{S}}(X)$ by $v$. Following the treatment of
random variables that are not continuous in general in [KM18], we define the
conditional value-at-risk as follows:

$\mathit{CVaR}_{p}^{\mathfrak{S}}(X)=1/p(\mathrm{Pr}_{\mathcal{M}}^{\mathfrak{S}}(X<v)\cdot\mathbb{E}_{\mathcal{M}}^{\mathfrak{S}}(X|X<v)+(p-\mathrm{Pr}_{\mathcal{M}}^{\mathfrak{S}}(X<v))\cdot
v).$

Outcomes of $X$ which are less than $v$ are treated differently to outcomes
equal to $v$ as it is possible that the outcome $v$ has positive probability
and we only want to account exactly for the $p$ worst outcomes. Hence, we take
only $p-\mathrm{Pr}_{\mathcal{M}}^{\mathfrak{S}}(X<v)$ of the outcomes which
are exactly $v$ into account as well. To provide worst-case guarantees or to
find risk-averse policies, we are interested in the maximal and minimal
conditional value-at-risk

$\mathit{CVaR}_{p}^{\max}(X)=\sup_{\mathfrak{S}}\mathit{CVaR}_{p}^{\mathfrak{S}}(X)\text{
and
}\mathit{CVaR}_{p}^{\min}(X)=\inf_{\mathfrak{S}}\mathit{CVaR}_{p}^{\mathfrak{S}}(X).$

In our formulation here, low outcomes are considered to be bad. Completely
analogously, one can define the conditional value-at-risk for the highest $p$
outcomes.

The main result of the section is the following:

######  Theorem 4.24.

The Positivity problem is polynomial-time reducible to the following problem:
Given an MDP $\mathcal{M}$ and rationals $\vartheta$ and $p\in(0,1)$, decide
whether

$\mathit{CVaR}^{\max}_{p}(\leavevmode\hbox to12.69pt{\vbox
to14.42pt{\pgfpicture\makeatletter\hbox{\hskip 6.3469pt\lower-7.208pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {}{{}}{}{}{}{}{{}}{}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.01389pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.01385pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-3.87498pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{3.87495pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{{}}{}{
{}{}{}} {}{}{ {}{}{}} {}{}{ {}{}{}} {}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{0.0pt}{3.87495pt}\pgfsys@lineto{3.01385pt}{0.0pt}\pgfsys@lineto{0.0pt}{-3.87498pt}\pgfsys@lineto{-3.01389pt}{0.0pt}\pgfsys@lineto{0.0pt}{3.87495pt}\pgfsys@stroke\pgfsys@invoke{
} { {}{}{}}{}{{}}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{0.0pt}{3.87495pt}\pgfsys@lineto{0.0pt}{-3.87498pt}\pgfsys@stroke\pgfsys@invoke{
} { {}{}{}}{}{{}}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{3.01385pt}{0.0pt}\pgfsys@lineto{-3.01389pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\mathit{goal})>\vartheta.$

We will use an auxiliary optimization problem to prove this result. We begin
with the following consideration: Given an MDP $\mathcal{M}$ with initial
state $s_{\mathit{\scriptscriptstyle init}}$, we construct a new MDP
$\mathcal{N}$. We add a new initial state $s_{\mathit{\scriptscriptstyle
init}}^{\prime}$. In $s_{\mathit{\scriptscriptstyle init}}^{\prime}$, there is
only one action with weight $0$ enabled leading to
$s_{\mathit{\scriptscriptstyle init}}$ with probability $\frac{1}{3}$ and to
$\mathit{goal}$ with probability $\frac{2}{3}$. So, at least two thirds of the
paths accumulate weight $0$ before reaching the goal. Hence, we can already
say that $\mathit{VaR}^{\mathfrak{S}}_{1/2}(\leavevmode\hbox to12.69pt{\vbox
to14.42pt{\pgfpicture\makeatletter\hbox{\hskip 6.3469pt\lower-7.208pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {}{{}}{}{}{}{}{{}}{}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.01389pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.01385pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-3.87498pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{3.87495pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{{}}{}{
{}{}{}} {}{}{ {}{}{}} {}{}{ {}{}{}} {}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{0.0pt}{3.87495pt}\pgfsys@lineto{3.01385pt}{0.0pt}\pgfsys@lineto{0.0pt}{-3.87498pt}\pgfsys@lineto{-3.01389pt}{0.0pt}\pgfsys@lineto{0.0pt}{3.87495pt}\pgfsys@stroke\pgfsys@invoke{
} { {}{}{}}{}{{}}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{0.0pt}{3.87495pt}\pgfsys@lineto{0.0pt}{-3.87498pt}\pgfsys@stroke\pgfsys@invoke{
} { {}{}{}}{}{{}}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{3.01385pt}{0.0pt}\pgfsys@lineto{-3.01389pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\mathit{goal})=0$ in
$\mathcal{N}$ under any scheduler $\mathfrak{S}$. Note that schedulers for
$\mathcal{M}$ can be seen as schedulers for $\mathcal{N}$ and vice versa. This
considerably simplifies the computation of the conditional value-at-risk in
$\mathcal{N}$. Define the random variable $\leavevmode\hbox to12.69pt{\vbox
to14.42pt{\pgfpicture\makeatletter\hbox{\hskip 6.3469pt\lower-7.208pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {}{{}}{}{}{}{}{{}}{}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.01389pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.01385pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-3.87498pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{3.87495pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{{}}{}{
{}{}{}} {}{}{ {}{}{}} {}{}{ {}{}{}} {}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{0.0pt}{3.87495pt}\pgfsys@lineto{3.01385pt}{0.0pt}\pgfsys@lineto{0.0pt}{-3.87498pt}\pgfsys@lineto{-3.01389pt}{0.0pt}\pgfsys@lineto{0.0pt}{3.87495pt}\pgfsys@stroke\pgfsys@invoke{
} { {}{}{}}{}{{}}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{3.01385pt}{0.0pt}\pgfsys@lineto{-3.01389pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\mathit{goal}$ on
paths $\zeta$ by

$\leavevmode\hbox to12.69pt{\vbox
to14.42pt{\pgfpicture\makeatletter\hbox{\hskip 6.3469pt\lower-7.208pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {}{{}}{}{}{}{}{{}}{}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.01389pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.01385pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-3.87498pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{3.87495pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{{}}{}{
{}{}{}} {}{}{ {}{}{}} {}{}{ {}{}{}} {}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{0.0pt}{3.87495pt}\pgfsys@lineto{3.01385pt}{0.0pt}\pgfsys@lineto{0.0pt}{-3.87498pt}\pgfsys@lineto{-3.01389pt}{0.0pt}\pgfsys@lineto{0.0pt}{3.87495pt}\pgfsys@stroke\pgfsys@invoke{
} { {}{}{}}{}{{}}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{3.01385pt}{0.0pt}\pgfsys@lineto{-3.01389pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\mathit{goal}(\zeta)=\min(\leavevmode\hbox
to12.69pt{\vbox to14.42pt{\pgfpicture\makeatletter\hbox{\hskip
6.3469pt\lower-7.208pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {}{{}}{}{}{}{}{{}}{}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.01389pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.01385pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-3.87498pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{3.87495pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{{}}{}{
{}{}{}} {}{}{ {}{}{}} {}{}{ {}{}{}} {}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{0.0pt}{3.87495pt}\pgfsys@lineto{3.01385pt}{0.0pt}\pgfsys@lineto{0.0pt}{-3.87498pt}\pgfsys@lineto{-3.01389pt}{0.0pt}\pgfsys@lineto{0.0pt}{3.87495pt}\pgfsys@stroke\pgfsys@invoke{
} { {}{}{}}{}{{}}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{0.0pt}{3.87495pt}\pgfsys@lineto{0.0pt}{-3.87498pt}\pgfsys@stroke\pgfsys@invoke{
} { {}{}{}}{}{{}}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{3.01385pt}{0.0pt}\pgfsys@lineto{-3.01389pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\mathit{goal}(\zeta),0).$

Now, the conditional value-at-risk for the probability value $1/2$ under a
scheduler $\mathfrak{S}$ in $\mathcal{N}$ is given by
$\mathit{CVaR}^{\mathfrak{S}}_{1/2}(\leavevmode\hbox to12.69pt{\vbox
to14.42pt{\pgfpicture\makeatletter\hbox{\hskip 6.3469pt\lower-7.208pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {}{{}}{}{}{}{}{{}}{}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.01389pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.01385pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-3.87498pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{3.87495pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{{}}{}{
{}{}{}} {}{}{ {}{}{}} {}{}{ {}{}{}} {}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{0.0pt}{3.87495pt}\pgfsys@lineto{3.01385pt}{0.0pt}\pgfsys@lineto{0.0pt}{-3.87498pt}\pgfsys@lineto{-3.01389pt}{0.0pt}\pgfsys@lineto{0.0pt}{3.87495pt}\pgfsys@stroke\pgfsys@invoke{
} { {}{}{}}{}{{}}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{0.0pt}{3.87495pt}\pgfsys@lineto{0.0pt}{-3.87498pt}\pgfsys@stroke\pgfsys@invoke{
} { {}{}{}}{}{{}}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{3.01385pt}{0.0pt}\pgfsys@lineto{-3.01389pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\mathit{goal})=2\cdot\mathbb{E}^{\mathfrak{S}}_{\mathcal{N},s_{\mathit{\scriptscriptstyle
init}}}(\leavevmode\hbox to12.69pt{\vbox
to14.42pt{\pgfpicture\makeatletter\hbox{\hskip 6.3469pt\lower-7.208pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {}{{}}{}{}{}{}{{}}{}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.01389pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.01385pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-3.87498pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{3.87495pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{{}}{}{
{}{}{}} {}{}{ {}{}{}} {}{}{ {}{}{}} {}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{0.0pt}{3.87495pt}\pgfsys@lineto{3.01385pt}{0.0pt}\pgfsys@lineto{0.0pt}{-3.87498pt}\pgfsys@lineto{-3.01389pt}{0.0pt}\pgfsys@lineto{0.0pt}{3.87495pt}\pgfsys@stroke\pgfsys@invoke{
} { {}{}{}}{}{{}}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{3.01385pt}{0.0pt}\pgfsys@lineto{-3.01389pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\mathit{goal})=\frac{2}{3}\cdot\mathbb{E}^{\mathfrak{S}}_{\mathcal{M},s_{\mathit{\scriptscriptstyle
init}}}(\leavevmode\hbox to12.69pt{\vbox
to14.42pt{\pgfpicture\makeatletter\hbox{\hskip 6.3469pt\lower-7.208pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {}{{}}{}{}{}{}{{}}{}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.01389pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.01385pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-3.87498pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{3.87495pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{{}}{}{
{}{}{}} {}{}{ {}{}{}} {}{}{ {}{}{}} {}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{0.0pt}{3.87495pt}\pgfsys@lineto{3.01385pt}{0.0pt}\pgfsys@lineto{0.0pt}{-3.87498pt}\pgfsys@lineto{-3.01389pt}{0.0pt}\pgfsys@lineto{0.0pt}{3.87495pt}\pgfsys@stroke\pgfsys@invoke{
} { {}{}{}}{}{{}}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{3.01385pt}{0.0pt}\pgfsys@lineto{-3.01389pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\mathit{goal})$. So,
the result follows from the following lemma:

######  Lemma 4.25.

The Positivity problem is polynomial-time reducible to the following problem:
Given an MDP $\mathcal{M}$ and a rational $\vartheta$, decide whether
$\mathbb{E}^{\max}_{\mathcal{M},s_{\mathit{\scriptscriptstyle
init}}}(\leavevmode\hbox to12.69pt{\vbox
to14.42pt{\pgfpicture\makeatletter\hbox{\hskip 6.3469pt\lower-7.208pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {}{{}}{}{}{}{}{{}}{}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.01389pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.01385pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-3.87498pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{3.87495pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{{}}{}{
{}{}{}} {}{}{ {}{}{}} {}{}{ {}{}{}} {}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{0.0pt}{3.87495pt}\pgfsys@lineto{3.01385pt}{0.0pt}\pgfsys@lineto{0.0pt}{-3.87498pt}\pgfsys@lineto{-3.01389pt}{0.0pt}\pgfsys@lineto{0.0pt}{3.87495pt}\pgfsys@stroke\pgfsys@invoke{
} { {}{}{}}{}{{}}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{3.01385pt}{0.0pt}\pgfsys@lineto{-3.01389pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\mathit{goal})>\vartheta$.

###### Proof.

The first important observation is that the optimal expectation $e(q,w)$ of
$\leavevmode\hbox to12.69pt{\vbox
to14.42pt{\pgfpicture\makeatletter\hbox{\hskip 6.3469pt\lower-7.208pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {}{{}}{}{}{}{}{{}}{}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.01389pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.01385pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-3.87498pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{3.87495pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{{}}{}{
{}{}{}} {}{}{ {}{}{}} {}{}{ {}{}{}} {}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{0.0pt}{3.87495pt}\pgfsys@lineto{3.01385pt}{0.0pt}\pgfsys@lineto{0.0pt}{-3.87498pt}\pgfsys@lineto{-3.01389pt}{0.0pt}\pgfsys@lineto{0.0pt}{3.87495pt}\pgfsys@stroke\pgfsys@invoke{
} { {}{}{}}{}{{}}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{3.01385pt}{0.0pt}\pgfsys@lineto{-3.01389pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\mathit{goal}$ for
different starting states $q$ and starting weights $w$ satisfies equation
($\ast$) from Section 3.2, i.e., $e(q,w)=\sum_{r\in S}P(q,\alpha,r)\cdot
e(r,w{+}\mathit{wgt}(q,\alpha))$ if an optimal scheduler chooses actions
$\alpha$ in state $q\not=\mathit{goal}$ when the accumulated weight is $w$.
The value $e(\mathit{goal},w)$ is $w$ if $w\leq 0$ and $0$ otherwise. This
allows us to reuse the gadget $\mathcal{G}_{\bar{\alpha}}$ to encode a linear
recurrence relation.

We again adjust the gadget encoding the initial values of a linear recurrence
sequence. So, let $k$ be a natural number, $\alpha_{1},\dots,\alpha_{k}$ be
rational coefficients of a linear recurrence sequence, and
$\beta_{0},\dots,\beta_{k-1}\geq 0$ the rational initial values. W.l.o.g. we
again assume these values to be small using Assumption 3.1, namely:
$\sum_{1\leq i\leq k}|\alpha_{i}|\leq\frac{1}{5(k+1)}$ and for all $j$,
$\beta_{j}\leq\frac{1}{3}\alpha$ where $\alpha=\sum_{1\leq i\leq
k}|\alpha_{i}|$.

The new gadget that encodes the initial values of a linear recurrence sequence
is depicted in Figure 16. In states $t$ and $s$, there is a choice between
actions $\gamma_{j}$ and $\delta_{j}$, respectively, for $0\leq j\leq k-1$.
After glueing together this gadget with the gadget
$\mathcal{G}_{\bar{\alpha}}$ at states $t$, $s$, and $\mathit{goal}$, we prove
that the interplay between the gadgets is correct: Let $0\leq j\leq k-1$.
Starting with accumulated weight ${-}k{+}j$ in state $t$, the action
$\gamma_{j}$ maximizes the partial expectation among the actions
$\gamma_{0},\dots,\gamma_{k-1}$. Likewise, $\delta_{j}$ is optimal when
starting in $s$ with weight ${-}k{+}j$. If the accumulated weight is non-
negative in state $s$ or $t$, then $\gamma$ or $\delta$ are optimal. The idea
is that for positive starting weights, the tail loss of $\gamma_{i}$ and
$\delta_{i}$ is relatively high while for weights just below $0$, the chance
to reach $\mathit{goal}$ with positive weight again outweighs this tail loss.

$t$$x_{j}$$z_{j}$$\mathit{goal}$$y_{j}$$s$$y_{j}^{\prime}$$\mathit{wgt}:{-}k$$\frac{1}{k+1}$$\frac{k}{k{+}1}$$\alpha$$1{-}\alpha$$\gamma_{j}|\mathit{wgt}:{-}2k{+}j$$\mathit{wgt}:+k$$1-\beta_{j}/\alpha$$\mathit{wgt}:+k$$\beta_{j}/\alpha$$\mathit{wgt}:+k$$\alpha$$1{-}\alpha$$\delta_{j}|\mathit{wgt}:{-}2k{+}j$$\mathit{wgt}:{-}k$$\frac{1}{k{+}1}$$\frac{k}{k{+}1}$$\mathit{wgt}:{-}2k$$\frac{1}{k{+}1}$$\frac{k}{k{+}1}$$\mathit{wgt}:{+}3k{-}2j$

Figure 16: The gadget encoding initial values for the reduction to the
threshold problem for the conditional value-at-risk. The gadget contains the
depicted states and actions for each $0\leq j\leq k-1$. The probability
$\alpha$ is $\sum_{1\leq i\leq k}|\alpha_{i}|$.

First, we estimate the expectation of $\leavevmode\hbox to12.69pt{\vbox
to14.42pt{\pgfpicture\makeatletter\hbox{\hskip 6.3469pt\lower-7.208pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {}{{}}{}{}{}{}{{}}{}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.01389pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.01385pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-3.87498pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{3.87495pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{{}}{}{
{}{}{}} {}{}{ {}{}{}} {}{}{ {}{}{}} {}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{0.0pt}{3.87495pt}\pgfsys@lineto{3.01385pt}{0.0pt}\pgfsys@lineto{0.0pt}{-3.87498pt}\pgfsys@lineto{-3.01389pt}{0.0pt}\pgfsys@lineto{0.0pt}{3.87495pt}\pgfsys@stroke\pgfsys@invoke{
} { {}{}{}}{}{{}}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{3.01385pt}{0.0pt}\pgfsys@lineto{-3.01389pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\mathit{goal}$ when
choosing $\delta_{i}$ and $\delta$ while the accumulated weight is ${-}k{+}j$
in $s$. If $i>j$, then $\delta_{i}$ and $\delta$ lead to $\mathit{goal}$
directly with probability $1{-}\alpha$ and weight $\leq-1$. So, the
expectation is less than ${-}(1-\alpha)\leq{-}1{+}\frac{1}{5(k{+}1)}$.

If $i\leq j$, then with probability $1{-}\alpha$ $\mathit{goal}$ is reached
with positive weight, hence $\leavevmode\hbox to12.69pt{\vbox
to14.42pt{\pgfpicture\makeatletter\hbox{\hskip 6.3469pt\lower-7.208pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {}{{}}{}{}{}{}{{}}{}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.01389pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.01385pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-3.87498pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{3.87495pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{{}}{}{
{}{}{}} {}{}{ {}{}{}} {}{}{ {}{}{}} {}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{0.0pt}{3.87495pt}\pgfsys@lineto{3.01385pt}{0.0pt}\pgfsys@lineto{0.0pt}{-3.87498pt}\pgfsys@lineto{-3.01389pt}{0.0pt}\pgfsys@lineto{0.0pt}{3.87495pt}\pgfsys@stroke\pgfsys@invoke{
} { {}{}{}}{}{{}}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{3.01385pt}{0.0pt}\pgfsys@lineto{-3.01389pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\mathit{goal}$ is $0$
on these paths. With probability $\beta_{i}$, goal is reached via
$y_{j}^{\prime}$. In this case all runs reach $\mathit{goal}$ with negative
weight. On the way to $y_{j}^{\prime}$ weight $2k$ is added, but afterwards
subtracted again at least once. In expectation weight $2k$ is subtracted
$\frac{k{+}1}{k}$ many times. Furthermore, ${-}2k{+}i$ is added to the
starting weight of ${-}k{+}j$. So, these paths contribute
$\beta_{i}\cdot(2k-2k\frac{k{+}1}{k}{-}3k{+}j{+}i)=({-}3k{+}j{+}i{-}2)\cdot\beta_{i}$
to the expectation of $\leavevmode\hbox to12.69pt{\vbox
to14.42pt{\pgfpicture\makeatletter\hbox{\hskip 6.3469pt\lower-7.208pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {}{{}}{}{}{}{}{{}}{}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.01389pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.01385pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-3.87498pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{3.87495pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{{}}{}{
{}{}{}} {}{}{ {}{}{}} {}{}{ {}{}{}} {}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{0.0pt}{3.87495pt}\pgfsys@lineto{3.01385pt}{0.0pt}\pgfsys@lineto{0.0pt}{-3.87498pt}\pgfsys@lineto{-3.01389pt}{0.0pt}\pgfsys@lineto{0.0pt}{3.87495pt}\pgfsys@stroke\pgfsys@invoke{
} { {}{}{}}{}{{}}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{3.01385pt}{0.0pt}\pgfsys@lineto{-3.01389pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\mathit{goal}$. With
analogous reasoning, we see that the remaining paths contribute
$({-}3k{+}j{+}i{-}1)\cdot(\alpha-\beta_{i})$. So, all in all the expectation
of $\leavevmode\hbox to12.69pt{\vbox
to14.42pt{\pgfpicture\makeatletter\hbox{\hskip 6.3469pt\lower-7.208pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {}{{}}{}{}{}{}{{}}{}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.01389pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.01385pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-3.87498pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{3.87495pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{{}}{}{
{}{}{}} {}{}{ {}{}{}} {}{}{ {}{}{}} {}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{0.0pt}{3.87495pt}\pgfsys@lineto{3.01385pt}{0.0pt}\pgfsys@lineto{0.0pt}{-3.87498pt}\pgfsys@lineto{-3.01389pt}{0.0pt}\pgfsys@lineto{0.0pt}{3.87495pt}\pgfsys@stroke\pgfsys@invoke{
} { {}{}{}}{}{{}}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{3.01385pt}{0.0pt}\pgfsys@lineto{-3.01389pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\mathit{goal}$ in this
situation is $\alpha{\cdot}({-}3k{+}j{+}i{-}1){-}\beta_{i}$. Now, as
$\alpha\leq\frac{1}{5(k{+}1)}$ and $\beta_{i}\leq\frac{\alpha}{3}$ for all
$i$, we see that
$\alpha{\cdot}({-}3k{+}j{+}i{-}1){-}\beta_{i}\geq{-}(3k+2)\alpha\geq{-}1{+}\frac{1}{5(k{+}1)}$.
The optimum with $i\leq j$ is obtained for $i=j$ as $\beta_{i}\leq\alpha/3$
for all $i$. Hence indeed $\delta_{j}$ is the optimal action. For $\gamma_{j}$
the same proof with $\beta_{i}=0$ for all $i$ leads to the same result.

Now assume that the accumulated weight in $t$ or $s$ is $\ell\geq 0$. Then,
all actions lead to $\mathit{goal}$ with a positive weight with probability
$1-\alpha$. In this case $\leavevmode\hbox to12.69pt{\vbox
to14.42pt{\pgfpicture\makeatletter\hbox{\hskip 6.3469pt\lower-7.208pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {}{{}}{}{}{}{}{{}}{}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.01389pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.01385pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-3.87498pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{3.87495pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{{}}{}{
{}{}{}} {}{}{ {}{}{}} {}{}{ {}{}{}} {}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{0.0pt}{3.87495pt}\pgfsys@lineto{3.01385pt}{0.0pt}\pgfsys@lineto{0.0pt}{-3.87498pt}\pgfsys@lineto{-3.01389pt}{0.0pt}\pgfsys@lineto{0.0pt}{3.87495pt}\pgfsys@stroke\pgfsys@invoke{
} { {}{}{}}{}{{}}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{3.01385pt}{0.0pt}\pgfsys@lineto{-3.01389pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\mathit{goal}$ is $0$.
However, a scheduler $\mathfrak{S}$ which always chooses $\gamma$ and $\delta$
is better than a scheduler choosing $\gamma_{j}$ or $\delta_{j}$ for any
$j\leq k{-}1$. Under scheduler $\mathfrak{S}$ starting from $s$ or $t$ a run
returns to $\\{s,t\\}$ with probability $\alpha$ while accumulating weight
$\geq{-}k$ and the process is repeated. After choosing $\gamma_{j}$ or
$\delta_{j}$ the run moves to $x_{j}$, $y_{j}$ or $y_{j}^{\prime}$ while
accumulating a negative weight. From then on, in each step it will stay in
that state with probability greater than $\alpha$ and accumulate weight
$\leq{-}k$. Hence, the expectation of $\leavevmode\hbox to12.69pt{\vbox
to14.42pt{\pgfpicture\makeatletter\hbox{\hskip 6.3469pt\lower-7.208pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {}{{}}{}{}{}{}{{}}{}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.01389pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.01385pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-3.87498pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{3.87495pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{{}}{}{
{}{}{}} {}{}{ {}{}{}} {}{}{ {}{}{}} {}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{0.0pt}{3.87495pt}\pgfsys@lineto{3.01385pt}{0.0pt}\pgfsys@lineto{0.0pt}{-3.87498pt}\pgfsys@lineto{-3.01389pt}{0.0pt}\pgfsys@lineto{0.0pt}{3.87495pt}\pgfsys@stroke\pgfsys@invoke{
} { {}{}{}}{}{{}}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{3.01385pt}{0.0pt}\pgfsys@lineto{-3.01389pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\mathit{goal}$ is
lower under $\gamma_{j}$ or $\delta_{j}$ than under $\mathfrak{S}$. Therefore
indeed $\gamma$ and $\delta$ are the best actions for non-negative accumulated
weight in states $s$ and $t$.

Let now $e(t,w)$ and $e(s,w)$ denote the optimal expectations of
$\leavevmode\hbox to12.69pt{\vbox
to14.42pt{\pgfpicture\makeatletter\hbox{\hskip 6.3469pt\lower-7.208pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {}{{}}{}{}{}{}{{}}{}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.01389pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.01385pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-3.87498pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{3.87495pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{{}}{}{
{}{}{}} {}{}{ {}{}{}} {}{}{ {}{}{}} {}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{0.0pt}{3.87495pt}\pgfsys@lineto{3.01385pt}{0.0pt}\pgfsys@lineto{0.0pt}{-3.87498pt}\pgfsys@lineto{-3.01389pt}{0.0pt}\pgfsys@lineto{0.0pt}{3.87495pt}\pgfsys@stroke\pgfsys@invoke{
} { {}{}{}}{}{{}}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{3.01385pt}{0.0pt}\pgfsys@lineto{-3.01389pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\mathit{goal}$ when
starting in $t$ or $s$ with weight $w$. Further, let $d(w)=e(t,w)-e(s,w)$.
From the argument above, we also learn that the difference $d(-k{+}j)$ is
equal to $\beta_{j}$, for $0\leq j\leq k-1$ . Put together with the linear
recurrence encoded in $\mathcal{G}_{\bar{\alpha}}$ this shows that
$d({-k}+w)=u_{w}$ for all $w$ where $(u_{n})_{n\in\mathbb{N}}$ is the linear
recurrence sequence specified by the $\alpha_{i}$, $\beta_{j}$, $1\leq i\leq
k$, and $0\leq j\leq k{-}1$.

Finally, we add the same initial component as in the previous section to
obtain an MDP $\mathcal{M}$. Let $\mathfrak{S}$ be the scheduler always
choosing $\tau$ in state $c$ and afterwards following the optimal actions as
described above is optimal iff the linear recurrence sequence stays non-
negative. The remaining argument goes completely analogously to the proof of
Theorem 4.1. Grouping together the optimal values in vectors $v_{n}$ with $2k$
entries as done there, we can use the same Markov chain as in that proof to
obtain a matrix $A$ such that $v_{n+1}=Av_{n}$. This allows us to compute the
rational value
$\vartheta=\mathbb{E}_{\mathcal{M},s_{\mathit{\scriptscriptstyle
init}}}^{\mathfrak{S}}(\leavevmode\hbox to12.69pt{\vbox
to14.42pt{\pgfpicture\makeatletter\hbox{\hskip 6.3469pt\lower-7.208pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {}{{}}{}{}{}{}{{}}{}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.01389pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.01385pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-3.87498pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{3.87495pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{{}}{}{
{}{}{}} {}{}{ {}{}{}} {}{}{ {}{}{}} {}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{0.0pt}{3.87495pt}\pgfsys@lineto{3.01385pt}{0.0pt}\pgfsys@lineto{0.0pt}{-3.87498pt}\pgfsys@lineto{-3.01389pt}{0.0pt}\pgfsys@lineto{0.0pt}{3.87495pt}\pgfsys@stroke\pgfsys@invoke{
} { {}{}{}}{}{{}}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{3.01385pt}{0.0pt}\pgfsys@lineto{-3.01389pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\mathit{goal})$ via a
matrix series in polynomial time and
$\mathbb{E}_{\mathcal{M},s_{\mathit{\scriptscriptstyle
init}}}^{\max}(\leavevmode\hbox to12.69pt{\vbox
to14.42pt{\pgfpicture\makeatletter\hbox{\hskip 6.3469pt\lower-7.208pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {}{{}}{}{}{}{}{{}}{}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.01389pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.01385pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-3.87498pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{3.87495pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{{}}{}{
{}{}{}} {}{}{ {}{}{}} {}{}{ {}{}{}} {}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{0.0pt}{3.87495pt}\pgfsys@lineto{3.01385pt}{0.0pt}\pgfsys@lineto{0.0pt}{-3.87498pt}\pgfsys@lineto{-3.01389pt}{0.0pt}\pgfsys@lineto{0.0pt}{3.87495pt}\pgfsys@stroke\pgfsys@invoke{
} { {}{}{}}{}{{}}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{3.01385pt}{0.0pt}\pgfsys@lineto{-3.01389pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\mathit{goal})>\vartheta$
if and only if the given linear recurrence sequence is eventually negative. ∎

By the discussion above, this lemma directly implies Theorem 4.24. With
adaptions similar to the previous section, it is possible to obtain the
analogous result for the minimal expectation of $\leavevmode\hbox
to12.69pt{\vbox to14.42pt{\pgfpicture\makeatletter\hbox{\hskip
6.3469pt\lower-7.208pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {}{{}}{}{}{}{}{{}}{}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.01389pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.01385pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-3.87498pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{3.87495pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{{}}{}{
{}{}{}} {}{}{ {}{}{}} {}{}{ {}{}{}} {}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{0.0pt}{3.87495pt}\pgfsys@lineto{3.01385pt}{0.0pt}\pgfsys@lineto{0.0pt}{-3.87498pt}\pgfsys@lineto{-3.01389pt}{0.0pt}\pgfsys@lineto{0.0pt}{3.87495pt}\pgfsys@stroke\pgfsys@invoke{
} { {}{}{}}{}{{}}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{3.01385pt}{0.0pt}\pgfsys@lineto{-3.01389pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\mathit{goal}$. This
implies that also the threshold problem whether the minimal conditional value-
at-risk is less than a threshold $\vartheta$,
$\mathit{CVaR}^{\min}_{p}(\leavevmode\hbox to12.69pt{\vbox
to14.42pt{\pgfpicture\makeatletter\hbox{\hskip 6.3469pt\lower-7.208pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {}{{}}{}{}{}{}{{}}{}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.01389pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.01385pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-3.87498pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{{}{}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{3.87495pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{{}}{}{
{}{}{}} {}{}{ {}{}{}} {}{}{ {}{}{}} {}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{0.0pt}{3.87495pt}\pgfsys@lineto{3.01385pt}{0.0pt}\pgfsys@lineto{0.0pt}{-3.87498pt}\pgfsys@lineto{-3.01389pt}{0.0pt}\pgfsys@lineto{0.0pt}{3.87495pt}\pgfsys@stroke\pgfsys@invoke{
} { {}{}{}}{}{{}}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{0.0pt}{3.87495pt}\pgfsys@lineto{0.0pt}{-3.87498pt}\pgfsys@stroke\pgfsys@invoke{
} { {}{}{}}{}{{}}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{3.01385pt}{0.0pt}\pgfsys@lineto{-3.01389pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\mathit{goal})<\vartheta$,
is Positivity-hard.

##  5 Conclusion

The Positivity-hardness results established in this paper show that a series
of problems on finite-state MDPs that have been studied and left open in the
literature exhibit an inherent mathematical difficulty. A decidability result
for any of these problems would imply a major break-through in analytic number
theory. At the heart of our Positivity-hardness proofs lies the construction
of modular MDPs consisting of three gadgets. This construction provides a
versatile proof strategy to establish Positivity-hardness results: It allowed
us to provide three direct reductions from the Positivity problem by
constructing structurally identical MDPs that only differ in the gadget
encoding the initial values. The further chains of reductions depicted in
Figure 1 established Positivity-hardness for a landscape of different
problems. These problems range from problems on one-counter MDPs and integer-
weighted MDPs also to problems concerning the long-run satisfaction of path
properties, namely the threshold problem for long-run probabilities and the
model-checking problem of frequency-LTL, which are on first sight of a rather
different nature compared to the other problems.

The proof technique might be applicable to further threshold problems
associated to optimization problems on MDPs. A main requirement for the direct
applicability of the technique is that the optimal values $V(s,w)$ in terms of
the current state $s$ and the weight $w$ accumulated so far, or a similar
quantity that can be increased and decreased, satisfy an optimality equation
of the form

$V(s,w)=\max_{\alpha\in\mathit{Act}(s)}\sum_{t\in S}P(s,\alpha,t)\cdot
V(t,w+\mathit{wgt}(s,\alpha)).$

In addition, the optimum must not be achievable with memoryless schedulers,
but the optimal decisions have to depend on the accumulated weight to make it
possible to encode initial values of a linear recurrence sequence. This
combination of conditions is quite common as we have seen. Furthermore, our
and possible future Positivity-hardness results might be transferrable to
further notions resulting from taking long-run averages (as in the case of
long-run probabilities and frequency-LTL) or conditioning (as in the case of
conditional expectations and conditional values-at-risk).

In the special case of Markov chains, several of the investigated problems are
decidable: In Markov chains, partial and conditional expectations and long-run
probabilities and frequencies can easily be computed. Furthermore, one-counter
Markov chains constitute a special case of recursive Markov chains, for which
the threshold problem for the termination probability can be decided in
polynomial space [EY09]. Remarkably however, the threshold problem for the
probability that the accumulated cost satisfies a Boolean combination of
inequality constraints in finite-state Markov chains is open [HKL17].

Finally, the Positivity-hardness results of course leave the possibility open
that some or all of the problems we studied are in fact harder than the
Positivity problem. In particular, it could be the case that the problems are
undecidable and that a proof of the undecidability would yield no implications
for the Positivity problem. For this reason, investigating whether some or all
of the threshold problems are reducible to the Positivity problem constitutes
a very interesting – and challenging – direction for future work. Such an
inter-reducibility result would show that studying any of the discussed
optimization problems on MDPs could be a worthwhile direction of research to
settle the decidability status of the Positivity-problem. Some hope for an
inter-reducibility result can be drawn from the fact that the optimal values
are approximable for several of the problems – for termination probabilities
and expected termination times of one-counter MDPs, this was shown in [BBEK11,
BKNW12] and for partial and conditional expectations in [PB19]. This indicates
that there is at least a major difference to undecidable problems in a similar
context such as the emptiness problem for probabilistic finite automata where
the optimal value cannot be approximated [Paz71, CL89].

## References

  * [AAGT15] Manindra Agrawal, Sundararaman Akshay, Blaise Genest, and P. S. Thiagarajan.  Approximate verification of the symbolic dynamics of Markov chains.  Journal of the ACM, 62(1):1–34, 2015.
  * [AAOW15] S. Akshay, Timos Antonopoulos, Joël Ouaknine, and James Worrell.  Reachability problems for Markov chains.  Information Processing Letters, 115(2):155–158, 2015.
  * [ADBA21] Mohamadreza Ahmadi, Anushri Dixit, Joel W Burdick, and Aaron D Ames.  Risk-averse stochastic shortest path planning.  arXiv:2103.14727, 2021.
  * [AT02] Carlo Acerbi and Dirk Tasche.  Expected shortfall: A natural coherent alternative to value at risk.  Economic Notes, 31(2):379–388, 2002.
  * [BAGM12] Amir M. Ben-Amram, Samir Genaim, and Abu Naser Masud.  On the termination of integer loops.  ACM Transactions on Programming Languages and Systems, 34(4):1–24, 2012.
  * [BBD+18] Christel Baier, Nathalie Bertrand, Clemens Dubslaff, Daniel Gburek, and Ocan Sankur.  Stochastic shortest paths and weight-bounded properties in Markov decision processes.  In 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 86–94. ACM, 2018.
  * [BBE+10] Tomás Brázdil, Václav Brožek, Kousha Etessami, Antonín Kučera, and Dominik Wojtczak.  One-counter Markov decision processes.  In 21st Annual ACM-SIAM Symposium on Discrete Algorithms (SODA), pages 863–874. SIAM, 2010.
  * [BBEK11] Tomáš Brázdil, Václav Brožek, Kousha Etessami, and Antonín Kučera.  Approximating the termination value of one-counter MDPs and stochastic games.  In Luca Aceto, Monika Henzinger, and Jiří Sgall, editors, 38th International Colloquium on Automata, Languages, and Programming (ICALP), volume 6755 of Theoretical Computer Science and General Issues, pages 332–343. Springer, 2011.
  * [BBPS19] Christel Baier, Nathalie Bertrand, Jakob Piribauer, and Ocan Sankur.  Long-run satisfaction of path properties.  In 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–14. IEEE, 2019.
  * [BDD+14] Christel Baier, Marcus Daum, Clemens Dubslaff, Joachim Klein, and Sascha Klüppelholz.  Energy-utility quantiles.  In Julia M. Badger and Kristin Yvonne Rozier, editors, 6th NASA Formal Methods Symposium (NFM), volume 8430 of Programming and Software Engineering, pages 285–299. Springer, 2014.
  * [BDK+14] Christel Baier, Clemens Dubslaff, Joachim Klein, Sascha Klüppelholz, and Sascha Wunderlich.  Probabilistic model checking for energy-utility analysis.  In Franck van Breugel, Elham Kashefi, Catuscia Palamidessi, and Jan Rutten, editors, Horizons of the Mind. A Tribute to Prakash Panangaden, volume 8464 of Lecture Notes in Computer Science, pages 96–123. Springer, 2014.
  * [BDL12] Benedikt Bollig, Normann Decker, and Martin Leucker.  Frequency linear-time temporal logic.  In 6th International Symposium on Theoretical Aspects of Software Engineering (TASE), pages 85–92. IEEE, 2012.
  * [BEFH16] Gilles Barthe, Thomas Espitau, Luis María Ferrer Fioriti, and Justin Hsu.  Synthesizing probabilistic invariants via Doob’s decomposition.  In Swarat Chaudhuri and Azadeh Farzan, editors, 28th International Conference on Computer Aided Verification (CAV), Part I, volume 9779 of Lecture Notes in Computer Science, pages 43–61. Springer, 2016.
  * [BGB12] Christel Baier, Marcus Größer, and Nathalie Bertrand.  Probabilistic $\omega$-automata.  Journal of the ACM, 59(1):1:1–1:52, 2012.
  * [BK08] Christel Baier and Joost-Pieter Katoen.  Principles of Model Checking.  MIT Press, 2008.
  * [BKKW14] Christel Baier, Joachim Klein, Sascha Klüppelholz, and Sascha Wunderlich.  Weight monitoring with linear temporal logic: Complexity and decidability.  In 29th Symposium on Logic In Computer Science (LICS), pages 11:1–11:10. ACM, 2014.
  * [BKKW17] Christel Baier, Joachim Klein, Sascha Klüppelholz, and Sascha Wunderlich.  Maximizing the conditional expected reward for reaching the goal.  In Axel Legay and Tiziana Margaria, editors, 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 10206 of Lecture Notes in Computer Science, pages 269–285. Springer, 2017.
  * [BKN16] Tomás Brázdil, Antonín Kucera, and Petr Novotný.  Optimizing the expected mean payoff in energy Markov decision processes.  In Cyrille Artho, Axel Legay, and Doron Peled, editors, 14th International Symposium on Automated Technology for Verification and Analysis (ATVA), volume 9938 of Lecture Notes in Computer Science, pages 32–49. Springer, 2016.
  * [BKNW12] Tomáš Brázdil, Antonín Kučera, Petr Novotnỳ, and Dominik Wojtczak.  Minimizing expected termination time in one-counter Markov decision processes.  In Artur Czumaj, Kurt Mehlhorn, Andrew Pitts, and Roger Wattenhofer, editors, 39th International Colloquium on Automata, Languages, and Programming (ICALP), volume 7392 of Theoretical Computer Science and General Issues, pages 141–152. Springer, 2012.
  * [Bra06] Mark Braverman.  Termination of integer linear programs.  In Thomas Ball and Robert B. Jones, editors, 18th International Conference on Computer Aided Verification (CAV), volume 4144 of Theoretical Computer Science and General Issues, pages 372–385. Springer, 2006\.
  * [BRS06] Daniele Beauquier, Alexander Rabinovich, and Anatol Slissenko.  A logic of probability with decidable model checking.  Journal of Logic and Computation, 16(4):461–487, 2006.
  * [BT91] Dimitri P. Bertsekas and John N. Tsitsiklis.  An analysis of stochastic shortest path problems.  Mathematics of Operations Research, 16(3):580–595, 1991.
  * [Can88] John Canny.  Some algebraic and geometric computations in pspace.  In 20th Annual ACM Symposium on Theory of Computing (STOC), pages 460–467. ACM, 1988.
  * [CD11] Krishnendu Chatterjee and Laurent Doyen.  Energy and mean-payoff parity Markov decision processes.  In Filip Murlak and Piotr Sankowski, editors, 36th International Symposium on Mathematical Foundations of Computer Science (MFCS), volume 6907 of Lecture Notes in Computer Science, pages 206–218. Springer, 2011\.
  * [CFG16] Krishnendu Chatterjee, Hongfei Fu, and Amir Kafshdar Goharshady.  Termination analysis of probabilistic programs through Positivstellensatz’s.  In Swarat Chaudhuri and Azadeh Farzan, editors, 28th International Conference on Computer Aided Verification (CAV), Part I, volume 9779 of Lecture Notes in Computer Science, pages 3–22. Springer, 2016.
  * [CFK+13a] Taolue Chen, Vojtěch Forejt, Marta Kwiatkowska, David Parker, and Aistis Simaitis.  Automatic verification of competitive stochastic systems.  Formal Methods in System Design, 43(1):61–92, 2013.
  * [CFK+13b] Taolue Chen, Vojtěch Forejt, Marta Kwiatkowska, David Parker, and Aistis Simaitis.  Prism-games: A model checker for stochastic multi-player games.  In Nir Piterman and Scott A. Smolka, editors, 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 7795 of Lecture Notes in Computer Science, pages 185–191. Springer, 2013.