text:
\section{Appendix}

\subsection{Properties of the CVaR operator} \label{sec:app:cvar_prop}

\subsubsection{Details of the VaR definition}

In the main body, we mentioned a possible alternative definition of VaR, namely $\VaR_p := \inf \{r \in \mathbb{R} \mid F_X(r) \geq p\}$, which is quite symmetric our chosen definition $\VaR_p :=  \sup \{r \in \mathbb{R} \mid F_X(r) \leq p\}$.
Indeed, these definitions mostly are equivalent, especially on continuous random variables.
A subtle difference arises for discrete random variables, which we explain in the following.

Recall that in the proof of correctness for the LP in Fig.~\ref{fig:reach_lp}, we mentioned that under particular circumstances, namely $\underline{x}_s = x_s$ for all $s \in T_\leq$, we have $\VaR_p > t$, $\VaR_p = \min \{r \in \mathbf{r}(S) \mid r > t\}$ to be precise.
As we are only dealing with lower bound constraints, this doesn't matter in our case.

Essentially, the problem arises if there is an interval $I$ such that $F(r) = p$ for all $r \in I$.
The $\sup$-based definition of $\VaR_p$ now yields the upper bound of the interval, i.e. $\sup I$, while the $\inf$-based definition yields the lower bound $\inf I$.
This in turn complicates the decision procedure slightly, since we have to exclude the case $\underline{x}_s = 0$ for all $s \in T_=$ for the guessed VaR bound $t = \mathsf{v}$.

\subsubsection{Event-based definition}

Intuitively, one might think of defining $\CVaR$ in terms of the \enquote{worst $p$-quantile events}, i.e., in this setting, the set of worst runs in the system.
Formally, we would be interested in some set $\Omega_p \in \mathcal{F}$ such that $\mu(\Omega_p) = p$ and $X(\omega) \leq \VaR_p(X)$ for all events $\omega \in \Omega_p$.
Clearly, this set may not be uniquely defined.
Consider, for example, a system and random variable where all runs attains the same value $v$.
Then, we could choose \emph{any} appropriately sized set of runs as $\Omega_p$.

But, this interpretation has another, more immediate problem.
The amount of distinct runs in a system may easily be finite or even a singleton, for example any single-state system.
Then, no set of runs actually satisfies this condition.
Yet, when interpreting $\CVaR$ as a measure of risk, it may still make sense to include a \enquote{fraction} of some run into this set, or equivalently, give less weight to it.

To fix this problem, one can consider a slight modification of the probability space of the system.
Informally, we attach some uniformly chosen value between $0$ and $1$ to any run of the system.
This ensures that no run has positive weight, yet the probability of any particular sequence of visited states remains unchanged.

\subsubsection{Further insight into the non-linearity} \label{sec:app:cvar:nonlinear}

\begin{example}
	Recall Ex.~\ref{ex:mdp_cvar_hard} and again set $p = 0.2$.
	We claim that any mixed strategy $\sigma_\lambda = \lambda \sigma_a + (1-\lambda) \sigma_b$ for $\lambda \in (0, 1)$ yields a CVaR strictly less than $5$.
	Fix any such lambda.
	Under the mixed strategy $\sigma_\lambda$, a value of $0$ is obtained with probability $(1-\lambda) 0.1$, $5$ with $\lambda$, and $10$ with $(1-\lambda) 0.9$, respectively.
	Together, we have that $\VaR_p = 5$ iff $p < 0.1 (1-\lambda) + \lambda$, i.e. $\lambda > \frac{1}{9}$, and $\VaR_p = 10$ otherwise.
	We handle these two cases separately.
	In the former case, the $\CVaR_p$ is
	\begin{multline*}
		\tfrac{1}{p} \left((1-\lambda) 0.1 \cdot 0 + (p - 0.1 (1-\lambda)) \cdot 5\right) = 5 - 2.5 (1-\lambda) = \\
		= 2.5 (1 + \lambda).
	\end{multline*}
	On the other hand, in the latter we have
	\begin{multline*}
		\tfrac{1}{p} \left((1-\lambda) 0.1 \cdot 0 + \lambda \cdot 5 + (p - ((1-\lambda) 0.1 + \lambda)) \cdot 10 \right) = \\
		= \ldots = 5 (1 - 4 \lambda).
	\end{multline*}
	Together, we get the graph in Fig.~\ref{fig:cvar_nonlinear_graph}.

	\begin{figure}[h]
		\begin{tikzpicture}[auto]
		\begin{axis}[axis x line=bottom,
		x axis line style={-},
		x label style={at={(axis description cs:0.5,0)},anchor=north},
		y axis line style={->},
		y label style={at={(axis description cs:0,0)},anchor=south west},
		height=3cm,width={0.5\columnwidth},
		xmin=0,xmax=1,xtick={0,1},xmajorticks=true,xlabel={$\lambda$},
		ymin=0,ymax=6,ytick={0,2.5,5},ylabel={}]
		\draw (axis cs:0,5) -- (axis cs:1/9,2.5) -- (axis cs:1,5);
		\end{axis}
		\end{tikzpicture}
		\caption{Graph of $\CVaR_p(X_\lambda)$ for $X_\lambda$ as in Ex.~\ref{ex:mdp_cvar_hard}.}
		\label{fig:cvar_nonlinear_graph}
	\end{figure}

\end{example}

\subsubsection{Monotonicity}

\begin{proposition} \label{stm:cvar_monotone}
	Let $p \in (0, 1)$ and $X_1, X_2$ two random variables with CDF $F_1$ and $F_2$, respectively.
	Assume that $F_1$ is point-wise larger than $F_2$ up until $t = \VaR_p(X_1)$, i.e.\ the CDFs satisfy $F_1(r) \geq F_2(r)$ for all $r \in (-\infty, t]$.
	Then we have that $\CVaR_p(X_1) \leq \CVaR_p(X_2)$.
\end{proposition}
\begin{proof}[Proof sketch]
	Let $X_1$ and $X_2$ be random variables and $p \in (0, 1)$ as in the theorem statement.
	Further, assume for now that $X_1$ and $X_2$ are continuous.
	This allows us to choose a measurable, strictly monotone $u : (-\infty, t] \to \mathbb{R}$ such that $F_1 \circ u = F_2$.
	Note that necessarily $u(x) \geq x$, since $F_1(x) \geq F_2(x)$ for all $x \leq t$.
	Define $V_i = (-\infty, \VaR_p(X_i)]$ the domain of integration for $\CVaR$.
	Then, by substitution, we get
	\begin{multline*}
		\CVaR_p(X_1) = \int_{V_1} x \ dF_1 = \int_{V_1} u^{-1} \circ u \ dF_1 = \\
		= \int_{u(V_1)} u^{-1} \ dF_1(u) = \int_{V_2} u^{-1} \ dF_2 \leq \int_{V_2} x \ dF_2,
	\end{multline*}
	concluding the proof.

	The general case can be proven analogously, only that one has to slightly relax the conditions on $u$ and deal with the previously mentioned corner cases.
\end{proof}

\begin{corollary}
	Let $p \in (0, 1)$ and $X_1, X_2$ two real valued random variables where $X_2$ stochastically dominates $X_1$.
	Then $\mathbb{E}[X_1] \leq \mathbb{E}[X_2]$, $\VaR_p(X_1) \leq \VaR_p(X_2)$, and $\CVaR_p(X_1) \leq \CVaR_p(X_2)$.
\end{corollary}

\begin{proof}
	For $\mathbb{E}$ and $\VaR$, this immediately follows from the respective definition, for $\CVaR$ the statement follows from Prop.~\ref{stm:cvar_monotone}.
\end{proof}

\subsubsection{CVaR of conditioned variables}

In the proof of Lem.~\ref{stm:mean_multi_mec_constant_strategies}, we applied $\CVaR$ on a random variable together with a conditioning, i.e. $\CVaR_p(X \mid W)$, where $W \in \mathcal{F}$ is a measurable, non-zero measure event.
Formally, this refers to the CVaR of $X$ on a slightly modified probability space, where $\mathbb{P}'$ equals $\mathbb{P}$ conditioned on $W$.

For, e.g., expectation, it is known that conditioning on a partitioning of the probability space preserves the total value, i.e. for a finite set $\{ W_i \} \subseteq \mathcal{F}$ which partitions $\Omega$, we have $\mathbb{E}[X] = \sum \mathbb{P}[W_i] \cdot \mathbb{E}[X \mid W_i]$.
This does not hold for CVaR, see Sec.~\ref{sec:app:cvar:nonlinear}.
We instead show a weaker statement, used in the proof of Lem.~\ref{stm:mean_multi_mec_constant_strategies}.

\begin{theorem} \label{stm:cvar_partitioning}
	Fix a probability space $(\Omega, \mathcal{F}, \mathbb{P})$, a random variable $X$ and $p \in [0, 1]$.
	Further, let $W = \{W_i\} \subseteq \mathcal{F}$ be a partitioning of $\Omega$, where all $W_i$ are measurable and have non-zero measure.
	Then, there exist $p_i$ and a set $W' \subseteq W$ such that
	\begin{equation*}
		\CVaR_p(X) = \frac{1}{\mathbb{P}[\UnionSym_{W_i \in W'} W']}\sum_{W_i \in W'} \mathbb{P}[W_i] \CVaR_{p_i}(X \mid W_i)
	\end{equation*}
\end{theorem}

\begin{proof}
	Recall that $\CVaR_1 = \mathbb{E}$ and $\CVaR_0 = \VaR$.
	In these cases, the statement immediately follows:
	For expectation, choose $W' = W$ and $p_i = 1$; for $\VaR$, choose $W' = \{W_i\}$ where $W_i$ is a witness of the worst case and set $p_i = 0$.

	Now, let $p \in (0, 1)$.
	Let $W' = \{W_i \mid \mathbb{P}[X \leq v \mid W_i] > 0\}$ be all sets relevant for the CVaR, i.e. which contain \enquote{bad} events.
	Then, we can simply set $p_i = \mathbb{P}[X \leq v \mid W_i]$, taking care of potential discrete jumps of $X$ in the respective $W_i$.
\end{proof}

\subsection{The general case for weighted reachability} \label{sec:app:cvar:weighted_reach}

\subsubsection{Proof of Thm.~\ref{stm:mdp_exp_reach_strategies_general}}

In the main body, we assumed that the set of target states $T$ is reached almost surely.
Thm.~\ref{stm:mdp_exp_reach_strategies} shows that in this case memoryless randomizing strategies are sufficient for $\mathsf{MDP}_{\mathsf{r},\mathsf{single}}^{\{\Expectation, \VaR, \CVaR\}}$.
If we drop this assumption, the involved strategies may become more complex.
Intuitively, this is the case since it might pay off to not move to the target set at all, e.g., if $\mathbf{r}(s) < 0$ for all $s \in T$.
We show this with a simple variation of the MDP in Fig.~\ref{fig:mean_payoff_memory} and prove that 2-memory strategies are sufficient.
Recall that this is the same type of strategy required for mean payoff, see Thm.~\ref{stm:mdp_exp_mean_strategies}.

\begin{figure}[!h]
	\begin{tikzpicture}[auto,initial text={},node distance=0.5cm]
		\node[initial above,state] (s0) {};
		\node[actionnode,right=of s0] (s0b) {};
		\node[state,above right=0.2cm and 0.75cm of s0b] (s2) {$5$};
		\node[state,below right=0.2cm and 0.75cm of s0b] (s3) {$-5$};

		\path[->]
			(s0) edge[directedge,loop left]    node[action] {$a$} (s0)
			(s0) edge[actionedge]         node[action] {$b$} (s0b)
			(s0b) edge[probedge]          node[prob] {$0.9$} (s2)
			(s0b) edge[probedge,swap]     node[prob] {$0.1$} (s3)
			(s2) edge[directedge,loop right] (s2)
			(s3) edge[directedge,loop right] (s3);
	\end{tikzpicture}
	\caption{Memory is necessary for general weighted reachability}
	\label{fig:reach_general_memory}
\end{figure} %
\begin{example}
	Consider the MDP presented in Fig.~\ref{fig:reach_general_memory} together with the constraints $\mathsf{q} = \mathsf{p} = 0.05$, $\mathsf{e} = 1$, and $\mathsf{c} = -3$ (or $\mathsf{v} = 0$).
	Using the reasoning of Ex.~\ref{ex:mdp_exp_reach_memory} immediately yields the result, namely that any satisfying strategy needs memory. \QEE
\end{example}

\begin{proof}[Proof of Thm.~\ref{stm:mdp_exp_reach_strategies_general}]
	Since we assumed that all states in $T$ are absorbing, we can trivially convert this problem to an instance of mean payoff by assigning $\mathbf{r}(s) = 0$ to all $s \in S \setminus T$.
	Applying Thm.~\ref{stm:mdp_exp_mean_strategies} yields the result.
\end{proof}

\subsubsection{Assumptions in Thm.~\ref{stm:mdp_exp_reach_lp_correct}} \label{sec:app:reach_lp_assumptions}

For the LP in Fig.~\ref{fig:reach_lp}, we made several assumptions, namely:
\begin{enumerate}
	\item All MECs consist of a single state and we identify each MEC with the corresponding state, \label{stm:mdp_exp_reach_lp_correct:assumption:mec}
	\item all MECs $m_i$ from which $T$ is not reachable are considered part of $T$ and have $\mathbf{r}(m_i) = 0$, and \label{stm:mdp_exp_reach_lp_correct:assumption:all_reach}
	\item quantile-probabilities are equal, i.e.\ $\mathsf{p} = \mathsf{q}$. \label{stm:mdp_exp_reach_lp_correct:assumption:quantile}
\end{enumerate}

In the following, we present the general procedure to obtain a solution to $\mathsf{MDP}_{\mathsf{r},\mathsf{single}}^{\{\Expectation,\VaR,\CVaR\}}$ queries.
In particular, we
\begin{enumerate}
	\item prove that assumption~\ref{stm:mdp_exp_reach_lp_correct:assumption:mec} and \ref{stm:mdp_exp_reach_lp_correct:assumption:all_reach} can be made w.l.o.g.,
	\item derive a modification of the LP from Fig.~\ref{fig:reach_lp} in Fig.~\ref{fig:reach_lp_ext} which deals with assumption~\ref{stm:mdp_exp_reach_lp_correct:assumption:quantile}, and
	\item show that the combined procedure is correct.
\end{enumerate}

Assumption~\ref{stm:mdp_exp_reach_lp_correct:assumption:all_reach} directly follows from the definition of weighted reachability.
Once a run enters a MEC from which the target set $T$ is not reachable, the run is guaranteed to achieve a reward of zero.
To resolve the single-state MEC assumption we can lift the problem to the \emph{MEC quotient}~\cite{dA97a}, which satisfies the criterion.
This construction intuitively collapses each MEC into a single representative state and adapts the transitions accordingly.
Since in each MEC every state can be reached from any other with probability $1$, the MEC quotient preserves many infinite horizon properties like (weighted) reachability~\cite{dA97a,Puterman-book,DBLP:conf/cav/AshokCDKM17}.
More precisely, queries can easily be transformed so that they are satisfiable on the MEC quotient if and only if the original query is satisfiable.

\begin{figure}
	\begin{enumerate}
		\renewcommand{\labelenumi}{(\arabic{enumi}) }
		\item \label{fig:reach_lp_ext:non-neg}
		All variables $y_a$, $x_s$, $\underline{x}_s^c$, $\underline{x}_s^v$ are non-negative.
		\item \label{fig:reach_lp_ext:flow}
		Flow for $s \in S$:
		\begin{equation*}
			\mathbbm{1}_{s_0}(s) + {\sum}_{a \in \mathsf{A}} y_a \Delta(a, s) = {\sum}_{a \in \mathsf{Av}(s)} y_a + x_s
		\end{equation*}
		\item \label{fig:reach_lp_ext:switching}
		Switching to recurrent behaviour:
		\begin{equation*}
			{\sum}_{s \in M_i} y_s = x_i
		\end{equation*}
		\item \label{fig:reach_lp_ext:var_split}
		$\VaR$-consistent split:
		\begin{align*}
			\underline{x}_s^c & = x_s \text{ for $s \in T_{<c}$} & \underline{x}_s^c & \leq x_s \text{ for $s \in T_{=c}$} \\
			\underline{x}_s^v & = x_s \text{ for $s \in T_{<v}$} & \underline{x}_s^v & \leq x_s \text{ for $s \in T_{=v}$}
		\end{align*}
		\item \label{fig:reach_lp_ext:consistent_split}
		Probability-consistent split:
		\begin{align*}
			\sum_{s \in T_{\leq c}} \underline{x}_s^c & = \mathsf{p} & \sum_{s \in T_{\leq v}} \underline{x}_s^v & = \mathsf{q}
		\end{align*}
		\item \label{fig:reach_lp_ext:satisfaction}
		CVaR and expectation satisfaction:
		\begin{align*}
			\sum_{s \in T_{\leq c}} \underline{x}_s^c \cdot \mathbf{r}(s) & \geq \mathsf{p} \cdot \mathsf{c} &
			\sum_{s \in T} x_s \cdot \mathbf{r}(s) & \geq \mathsf{e}
		\end{align*}
	\end{enumerate}
	\caption{LP used to decide weighted reachability queries given guesses $t_c$ and $t_v$ of $\VaR_\mathsf{p}$ and $\VaR_\mathsf{q}$, respectively.
	$T_{\sim c}$ is defined as $T_{\sim c} := \{s \in T \mid s \sim t_c\}$ for $\sim~\in \{<, =, \leq\}$, analogous for $T_{\sim v}$.}
	\label{fig:reach_lp_ext}
	\vspace{-0.5em}
\end{figure}

In order to handle assumption~\ref{stm:mdp_exp_reach_lp_correct:assumption:quantile}, we present the adaptation of the LP from Fig.~\ref{fig:reach_lp} in Fig.~\ref{fig:reach_lp_ext}.
Essentially, only an additional type of variable, namely $\underline{x}_s^v$, has been added, verifying the $\VaR_\mathsf{q}$ constraint.
To prove Thm.~\ref{stm:mdp_exp_reach_lp_correct} for this adapted LP, the exact same reasoning as in the original proof can be applied.

\subsection{Proof of Lem.~\ref{stm:cvar_quasiconvex}} \label{sec:app:quasiconvex}

\begin{proof}
	Let $X_1$, $X_2$, $p$, and $\lambda$ be as in the statement and define $X_\lambda = \lambda X_1 + (1-\lambda) X_2$.
	Further, for $\circ \in \{1, 2, \lambda\}$, set $v_\circ = \VaR_p(X_\circ)$ and $c_\circ = \CVaR_p(X_\circ)$, and let $F_\circ$ denote the CDF of $X_\circ$.
	W.l.o.g., let $v_1 \leq v_2$.
	Observe that $F_\lambda = \lambda F_1 + (1-\lambda) F_2$ and, since CDF are non-decreasing, $F_2(v_1) \leq F_1(v_1) \leq F_1(v_2)$.
	Together, $F_\lambda(v_1) \leq F_\lambda(v_\lambda) \leq F_\lambda(v_2)$, which in turn yields $v_1 \leq v_\lambda \leq v_2$.

	Moreover, we can rearrange the definition of $F_\lambda$ to
	\begin{equation*}
		\lambda (F_1(v_\lambda) - p) = (1-\lambda) (p - F_2(v_\lambda)),
	\end{equation*}
	and thus
	\begin{equation*}
		\lambda \int_{v_1}^{v_\lambda} dF_1 = (1-\lambda) \int_{v_\lambda}^{v_2} dF_2.
	\end{equation*}
	Rearranging $c_\lambda$ and splitting the integration domain, we get
	\begin{multline*}
		c_\lambda = \int_{-\infty}^{v_\lambda} v\ dF_\lambda = \lambda \int_{-\infty}^{v_\lambda} v\ dF_1 + (1-\lambda) \int_{-\infty}^{v_\lambda} v\ dF_2 = \\
			= \lambda \left(c_1 + \int_{v_1}^{v_\lambda} v\ dF_1\right) + (1-\lambda) \left(c_2 - \int_{v_\lambda}^{v_2} v\ dF_2\right) \leq \\
			\leq \lambda c_1 + (1-\lambda) c_2 + \left( \lambda v_\lambda \int_{v_1}^{v_\lambda} dF_1 - (1-\lambda) v_\lambda \int_{v_\lambda}^{v_2} dF_2 \right),
	\end{multline*}
	and thus, by the previous equality, $c_\lambda \leq \lambda c_1 + (1-\lambda) c_2$.
\end{proof}

\section{Introducing the Conditional Value-at-risk}

In order to define our problem, we first introduce the general concept of \emph{conditional value-at-risk} (CVaR), also known as \emph{average value-at-risk}, \emph{expected shortfall}, and \emph{expected tail loss}.
As already hinted, the CVaR of some real-valued random variable $X$ and probability $p \in [0, 1]$ intuitively is the expectation below the worst $p$-quantile of $X$.

Let $X : \Omega \to \mathbb{R}$ be a random variable over the probability space $(\Omega, \mathcal{F}, \mathbb{P})$.
The associated \emph{cumulative density function} (CDF) $F_X : \mathbb{R} \to [0, 1]$ of $X$ yields the probability of $X$ being less than or equal to the given value $r$, i.e. $F_X(r) = \mathbb{P}(\{X(\omega) \leq r\})$.
$F$ is non-decreasing and right continuous with left limits (\emph{càdlàg}).

The \emph{value-at-risk} $\VaR_p$ is the worst $p$-quantile, i.e.\ a value $v$ s.t. the probability of $X$ attaining a value less than or equal to $v$ is $p$:\footnote{An often used, mostly equivalent definition is $\inf \{r \in \mathbb{R} \mid F_X(r) \geq p\}$.
Unfortunately, this would lead to some complications later on.
See Sec.~\ref{sec:app:cvar_prop} for details.}
\begin{equation*}
	\VaR_p(X) := \sup \{r \in \mathbb{R} \mid F_X(r) \leq p\} \quad (\VaR_1(X) = \infty)
\end{equation*}
Then, with $v = \VaR_p(X)$, $\CVaR$ can be defined as~\cite{Rockafellar00optimizationof}
\begin{equation*}
	\CVaR_p(X) := \mathbb{E}[X \mid X \leq v] = \frac{1}{p} \int_{(-\infty, v]} x \ dF_X,
\end{equation*}
with the corner cases $\CVaR_0 := \VaR_0$ and $\CVaR_1 = \mathbb{E}$.

Unfortunately, this definition only works as intended for continuous $X$, as shown by the following example.

\begin{figure}
	\begin{subfigure}[!t]{0.49\columnwidth}
		\begin{tikzpicture}
			\begin{axis}[axis x line=middle, axis y line=middle,
					height=3cm, width=1.2\textwidth,
					x label style={at={(axis description cs:0,0)},anchor=north west},
					y label style={at={(axis description cs:0,0)},rotate=90,anchor=south west},
					xmin=-0.4,xmax=2.5,xtick={1,2},xlabel={value},
					ymin=-0.05,ymax=1.2,ytick={0.5,1},yticklabels={$\tfrac{1}{2}$, $1$},ylabel={density $f$}]

				\draw[thick] (axis cs:-1,0) -- (axis cs:0,0) node[discontinuity-limit] {};
				\draw[thick] (axis cs:0,0.5) node[discontinuity-value] {} -- (axis cs:1,0.5) node[discontinuity-value] {};
				\draw[thick] (axis cs:1,0) node[discontinuity-limit] {} -- (axis cs:3,0);
				\draw[thick] (axis cs:2,0) -- (axis cs:2,0.9);
				\draw[thick,densely dotted] (axis cs:2,0.9) -- (axis cs:2,1.2);
,			\end{axis}
		\end{tikzpicture}
	\end{subfigure}
	\begin{subfigure}[!t]{0.49\columnwidth}
		\begin{tikzpicture}
			\begin{axis}[axis x line=middle, axis y line=middle,
					height=3cm, width=1.2\textwidth,
					x label style={at={(axis description cs:0,0)},anchor=north west},
					y label style={at={(axis description cs:0,0)},rotate=90,anchor=south west},
					xmin=-0.4,xmax=2.5,xtick={1,2},xlabel={value},
					ymin=-0.05,ymax=1.2,ytick={0.5,1},yticklabels={$\tfrac{1}{2}$, $1$},ylabel={CDF $F$}]

				\draw[thick] (axis cs:-1,0) -- (axis cs:0,0) -- (axis cs:1,0.5) -- (axis cs:2,0.5) node[discontinuity-limit] {};
				\draw[thick] (axis cs:2,1) node[discontinuity-value] {} -- (axis cs:2.2,1);
				\draw[thick,densely dotted] (axis cs:2.2,1) -- (axis cs:2.5,1);

			\end{axis}
		\end{tikzpicture}
	\end{subfigure}
	\caption{Distribution showing peculiarities of $\CVaR$}
	\label{fig:cvar_difficult}
\end{figure} %
\begin{example} \label{ex:cvar_intuition_wrong}
	Consider a random variable $X$ with a distribution as outlined in Fig.~\ref{fig:cvar_difficult}.
	For $p < \frac{1}{2}$, we certainly have $\VaR_p = 2p$.
	On the other hand, for any $p \in (\frac{1}{2}, 1)$, we get $\VaR_p = 2$.
	Consequently, the integral remains constant and $\CVaR_p$ would actually \emph{decrease} for increasing $p$, not matching the intuition. \QEE
\end{example}

\paragraph{General definition.}
As seen in Ex.~\ref{ex:cvar_intuition_wrong}, the previous definition breaks down when $F_X$ is not continuous at the $p$-quantile and consequently $F_X(\VaR_p(X)) > p$.
Thus, we handle the values at the threshold separately, similar to~\cite{rockafellar2002conditional}.

\begin{definition}
	Let $X$ be some random variable and $p \in [0, 1]$.
	With $v = \VaR_p(X)$, the $\CVaR$ of $X$ is defined as
	\begin{equation*}
		\CVaR_p(X) := \frac{1}{p} \left( \int_{(-\infty, v)} x \, dF_X + (p - \mathbb{P}[X < v]) \cdot v \right),
	\end{equation*}
	which can be rewritten as
	\begin{equation*}
		\CVaR_p(X) = \tfrac{1}{p} \big( \mathbb{P}[X < v] \cdot \mathbb{E}[X \mid X < v] + (p - \mathbb{P}[X < v]) \cdot v \big).
	\end{equation*}
	The corner cases again are $\CVaR_0 := \VaR_0$, and $\CVaR_1 = \mathbb{E}$.
\end{definition}
Since the degenerate cases of $p = 0$ and $p = 1$ reduce to already known problems, we exclude them in the following.

We demonstrate this definition on the previous example.
\begin{example}
	Again, consider the random variable $X$ from Ex.~\ref{ex:cvar_intuition_wrong}.
	For $\frac{1}{2} < p < 1$ we have that $\mathbb{P}[X < \VaR_p(X)] = \mathbb{P}[X < 2] = \frac{1}{2}$.
	The right hand side of the definition $(p - \mathbb{P}[X < \VaR_p(X)]) = p - \frac{1}{2}$ captures the remaining discrete probability mass which we have to handle separately.
	Together with  $\int_{(-\infty, 2)} x \, dF_X = \frac{1}{4}$ we get $\CVaR_p(X) = \frac{1}{p} (\frac{1}{4} + (p - \frac{1}{2}) \cdot 2) = 2 - \frac{3}{4p}$.
	For example, with $p = \frac{3}{4}$, this yields the expected result $\CVaR_p(X) = 1$. \QEE
\end{example}
\begin{remark}
	Recall that $\mathbb{P}[X < r]$ can be expressed as the left limit of $F_X$, namely $\mathbb{P}[X < r] = \lim_{r' \to^{-} r} F_X(r')$.
	Hence, $\CVaR_p(X)$ solely depends on the CDF of $X$ and thus random variables with the same CDF also have the same CVaR.
\end{remark}

We say that \emph{$F_1$ stochastically dominates $F_2$} for two CDF $F_1$ and $F_2$, if $F_1(r) \leq F_2(r)$ for all $r$.
Intuitively, this means that a sample drawn from $F_2$ is likely to be larger or equal to a sample from $F_1$.
All three investigated operators ($\mathbb{E}$, $\CVaR$, and $\VaR$) are monotone w.r.t. stochastic dominance, see Sec.~\ref{sec:app:cvar_prop}.
\section{Introduction}

\paragraph{Markov decision processes (MDP)} are a standard formalism for modelling stochastic systems featuring non-determinism.
The fundamental problem is to design a strategy resolving the non-determi\-nistic choices so that the systems' behaviour is optimized with respect to a given objective function, or, in the case of multi-objective optimization, to obtain the desired trade-off.
The objective function (in the optimization phrasing) or the query (in the decision-problem phrasing) consists of two parts.
First, a payoff is a measurable function assigning an outcome to each run of the system.
It can be real-valued, such as the \emph{long-run average reward} (also called \emph{mean payoff}), or a two-valued predicate, such as \emph{reachability}.
Second, the payoffs for single runs are combined into an overall outcome of the strategy, typically in terms of \emph{expectation}.
The resulting objective function is then for instance the expected long-run average reward, or the probability to reach a given target state.

\paragraph{Risk-averse control} aims to overcome one of the main disadvantages of the expectation operator, namely its ignorance towards the incurred risks, intuitively phrased as a question \emph{\enquote{How bad are the bad cases?}}
While the standard deviation (or variance) quantifies the spread of the distribution, it does not focus on the bad cases and thus fails to capture the risk.
There are a number of quantities used to deal with this issue:
\begin{itemize}
	\item The \emph{worst-case} analysis (in the financial context known as discounted maximum loss) looks at the payoff of the worst possible run.
	While this makes sense in a fully non-deterministic environment and lies at the heart of verification, in the probabilistic setting it is typically unreasonably pessimistic, taking into account events happening with probability $0$, e.g., never tossing head on a fair coin.
	\item The \emph{value-at-risk} ($\VaR$) denotes the worst $p$-quantile for some $p \in [0,1]$.
	For instance, the value at the $0.5$-quantile is the median, the $0.05$-quantile (the \emph{vigintile} or \emph{ventile}) is the value of the best run among the $5\%$ worst ones.
	As such it captures the \enquote{reasonably possible} worst-case.
	See Fig.~\ref{fig:cvar_explain} for an example of VaR for two given probability density functions.
	There has been an extensive effort spent recently on the analysis of MDP with respect to VaR and the re-formulated notions of quantiles, percentiles, thresholds, satisfaction view etc., see below.
	Although VaR is more realistic, it tends to ignore outliers too much, as seen in Fig.~\ref{fig:cvar_explain} on the right.
	VaR has been characterized as \emph{\enquote{seductive, but dangerous}} and \emph{\enquote{not sufficient to control risk}} \cite{seductive}.
	\item The \emph{conditional value-at-risk} (average value-at-risk, expected shortfall, expected tail loss) answers the question \emph{\enquote{What to expect in the bad cases?}}
	It is defined as the expectation over all events worse than the value-at-risk, see Fig.~\ref{fig:cvar_explain}.
	As such it describes the lossy tail, taking outliers into account, weighted respectively.
	In the degenerate cases, CVaR for $p = 1$ is the expectation and for $p = 0$ the (probabilistic) worst case.
	It is an established risk metric in finance, optimization and operations research, e.g. \cite{MAFI:MAFI068,Rockafellar00optimizationof}, and \emph{\enquote{is considered to be a more consistent measure of risk}} \cite{Rockafellar00optimizationof}.
	Recently, it started permeating to areas closer to verification, e.g. robotics \cite{DBLP:conf/icra/CarpinCP16}.
\end{itemize}

\begin{figure}
	\begin{subfigure}[!t]{0.49\columnwidth}
		\begin{tikzpicture}
			\begin{axis}[axis x line=middle, axis y line=middle,
					axis line style={->},
					x label style={at={(axis description cs:0,0)},anchor=north west},
					y label style={at={(axis description cs:0,0)},rotate=90,anchor=south west},
					ymajorticks=false,
					height=2.8cm,width={1.2\textwidth},
					xmin=0,xmax=2.2,xtick={0,1,2},xlabel={value},
					ymin=0,ymax=0.5,ytick style={draw=none},ylabel={density},
					samples=50]
				\addplot[domain=0:0.55, smooth, fill=lightgray, draw=none]{(e^(1 - (x - 1)^2) - 1)^4 / (20)} \closedcycle;
				\addplot[domain=0:2, smooth]{(e^(1 - (x - 1)^2) - 1)^4 / (20)};

				\draw [dashed] (axis cs:0.45,0) -- (axis cs:0.45,0.32) node[rotate=90,anchor=south] {$\CVaR$} -- (axis cs:0.45,0.47);
				\draw [dashed] (axis cs:0.55,0) -- (axis cs:0.55,0.38) node[rotate=90,anchor=north] {$\VaR$} -- (axis cs:0.55,0.47);

				\draw (axis cs:0,0) -- (axis cs:1,0);
			\end{axis}
		\end{tikzpicture}
	\end{subfigure} %
	\begin{subfigure}[!t]{0.49\columnwidth}
		\begin{tikzpicture}
			\begin{axis}[axis x line=middle, axis y line=middle,
					axis line style={->},
					x label style={at={(axis description cs:0,0)},anchor=north west},
					y label style={at={(axis description cs:0,0)},rotate=90,anchor=south west},
					ymajorticks=false,
					height=2.8cm,width={1.2\textwidth},
					xmin=0,xmax=2.2,xtick={0,1,2},xlabel={value},
					ymin=0,ymax=0.5,ytick style={draw=none},ylabel={density},
					samples=50,]
				\addplot[domain=0:0.25, smooth, fill=lightgray, draw]{sin(x*720)^2 / 4};

				\addplot[domain=1:1.1, smooth, fill=lightgray, draw=none]{(e^(-(x - 1.5)^2) - e^(-0.25))^2 * 7.5} \closedcycle;
				\addplot[domain=1:2, smooth]{(e^(-(x - 1.5)^2) - e^(-0.25))^2 * 7.5};

				\draw [dashed] (axis cs:0.3,0) -- (axis cs:0.3,0.32) node[rotate=90,anchor=north] {$\CVaR$} -- (axis cs:0.3,0.47);
				\draw [dashed] (axis cs:1.1,0) -- (axis cs:1.1,0.38) node[rotate=90,anchor=south] {$\VaR$} -- (axis cs:1.1,0.47);

				\draw (axis cs:0,0) -- (axis cs:2,0);
			\end{axis}
		\end{tikzpicture}
	\end{subfigure}
	\caption{Illustration of VaR and CVaR for some random variables.}
	\label{fig:cvar_explain}
\end{figure}

\paragraph{Our contribution}

In this paper, we investigate optimization of MDP with respect to CVaR as well as the respective trade-offs with expectation and VaR.
We study the VaR and CVaR operators for the first time with the payoff functions of weighted reachability and mean payoff, which are fundamental in verification.
Moreover, we cover both the single-dimensional and the multi-dimensional case.

Particularly, we define CVaR for MDP and show the peculiarities of the concept.
Then we study the computational complexity and the strategy complexity for various settings, proving the following:
\begin{itemize}
	\item
	The single dimensional case can be solved in polynomial time through linear programming, see Section~\ref{sec:single}.
	\item
	The multi-dimensional case is NP-hard, even for CVaR-only constraints.
	Weighted reachability is NP-complete and we give PSPACE and EXPSPACE upper bounds for mean payoff with CVaR and expectation constraints, and with additional VaR constraints, respectively, see Section~\ref{sec:multi}.
	(Note that already for the sole VaR constraints only an exponential algorithm is known; the complexity is an open question and not even NP-hardness is known~\cite{DBLP:journals/fmsd/RandourRS17,DBLP:conf/lics/ChatterjeeKK15}.)
	\item We characterize the strategy requirements, both in terms of memory, ranging from memoryless, over constant-size to infinite memory, and the required degree of randomization, ranging from fully deterministic strategies to randomizing strategies with stochastic memory update.
\end{itemize}

While dealing with the CVaR operator, we encountered surprising behaviour, preventing us to trivially adapt the solutions to the expectation and VaR problems:
\begin{itemize}
	\item Compared to, e.g., expectation and VaR, CVaR does not behave linearly w.r.t. stochastic combination of strategies.

	\item A conjunction of CVaR constraints already is NP-hard, since it can force a strategy to play deterministically.
\end{itemize}

\subsection{Related work}

\paragraph{Worst case}
Risk-averse approaches optimizing the worst case together with expectation have been considered in beyond-worst-case and beyond-almost-sure analysis investigated in both the single-dimensional~\cite{DBLP:journals/iandc/BruyereFRR17}
and in the multi-dimensional~\cite{DBLP:conf/lics/ClementeR15} setup.

\paragraph{Quantiles}
The decision problem related to VaR has been phrased in probabilistic verification mostly in the form \emph{\enquote{Is the probability that the payoff is higher than a given value threshold more than a given probability threshold?}}
The total reward gained attention both in the verification community~\cite{DBLP:conf/fossacs/UmmelsB13,DBLP:conf/icalp/HaaseK15,DBLP:conf/tacas/Baier0KW17} and recently in the AI community~\cite{DBLP:conf/aaai/GilbertWX17,DBLP:journals/corr/abs-1711-05788}.
Multi-dimensional percentile queries are considered for various objectives, such as mean-payoff, limsup, liminf, shortest path in~\cite{DBLP:journals/fmsd/RandourRS17}; for the specifics of two-dimensional case and their interplay, see~\cite{DBLP:conf/nfm/BaierDDKK14}.
Quantile queries for more complex constraints have also been considered, namely their conjunctions~\cite{FKR95,DBLP:journals/corr/abs-1104-3489}, conjunctions with expectations~\cite{DBLP:conf/lics/ChatterjeeKK15} or generally Boolean expressions~\cite{DBLP:conf/lics/HaaseKL17}.
Some of these approaches have already been practically applied and found useful by domain experts~\cite{DBLP:conf/fase/BaierDKDKMW14,DBLP:conf/csl/BaierDK14}.

\paragraph{CVaR}

There is a body of work that optimizes CVaR in MDP.
However, to the best of our knowledge, all the approaches (1) focus on the single-dimensional case, (2) disregard the expectation, and (3) treat neither reachability nor mean payoff.
They focus on the discounted~\cite{DBLP:journals/mmor/BauerleO11}, total~\cite{DBLP:conf/icra/CarpinCP16}, or immediate~\cite{DBLP:journals/ajcm/KageyamaFKT11} reward, as well as extend the results to continuous-time models~\cite{DBLP:journals/siamjo/HuangG16,DBLP:journals/siamco/MillerY17}.
This work comes from the area of optimization and operations research, with the notable exception of~\cite{DBLP:conf/icra/CarpinCP16}, which focuses on the total reward.
Since the total reward generalizes weighted reachability, \cite{DBLP:conf/icra/CarpinCP16} is related to our work the most.
However, it provides only an approximation solution for the one-dimensional case, neglecting expectation and the respective trade-offs.

Further, CVaR is a topic of high interest in finance, e.g., \cite{Rockafellar00optimizationof,seductive}.
The central difference is that there variations of portfolios (i.e. the objective functions) are considered while leaving the underlying random process (the market) unchanged.
This is dual to our problem, since we fix the objective function and now search for an optimal random process (or the respective strategy).

\paragraph{Multi-objective expectation}

In the last decade, MDP have been extensively studied generally in the setting of multiple objectives, which provides some of the necessary tools for our trade-off analysis.
Multiple objectives have been considered for both qualitative payoffs, such as reachability and LTL~\cite{DBLP:journals/lmcs/EtessamiKVY08}, as well as quantitative payoffs, such as mean payoff~\cite{DBLP:journals/corr/abs-1104-3489}, discounted sum~\cite{DBLP:conf/lpar/ChatterjeeFW13}, or total reward~\cite{DBLP:conf/tacas/ForejtKNPQ11}.
Variance has been introduced to the landscape in~ \cite{DBLP:conf/lics/BrazdilCFK13}.

\section{Multiple Dimensions} \label{sec:multi}

In this section, we deal with multi-dimensional queries.
We continue to use $i$ for indices related to MECs and further use $j$ for dimension indices.
First, we show that the Markov Chain case does not significantly change.

\begin{theorem}
	For any $\mathbf{obj}\in\{\mathsf{r},\mathsf{m}\}$, $\mathsf{MC}^{\{\Expectation, \VaR, \CVaR\}}_{\mathbf{obj}, \mathsf{multi}}$ is in P.
\end{theorem}

\begin{proof}
	Similarly to the single-dimensional case, we decide each constraint in each dimension separately, using our previous results.
	The query is satisfied iff each of the constraints is satisfied.
\end{proof}

\subsection{NP-Hardness of reachability and mean payoff}

For the MDP on the other hand, multiple dimensions add significant complexity.
In the following, we show that already the weighted reachability problem with multiple dimensions and only $\CVaR$ constraints, i.e.\ $\mathsf{MDP}_{\mathsf{r}, \mathsf{multi}}^{\{\CVaR\}}$, is NP-hard.
This result directly transfers to mean payoff, i.e.\ $\mathbf{obj} = \mathsf{m}$.
Recall that in contrast $\mathsf{MDP}_{\mathsf{r}, \mathsf{multi}}^{\{\Expectation\}}$ and even $\mathsf{MDP}_{\mathsf{r}, \mathsf{multi}}^{\{\Expectation,\VaR_0\}}$, i.e. constraints on the expectation and ensuring that almost all runs achieve a given threshold, are in P~\cite{DBLP:conf/lics/ChatterjeeKK15}.

\begin{theorem} \label{stm:reach_multi_np_hard}
	For any $\mathbf{obj} \in \{\mathsf{r}, \mathsf{m}\}$, $\mathsf{MDP}_{\mathbf{obj}, \mathsf{multi}}^{\{\CVaR\}}$ is NP-hard (when the dimension $d$ is a part of the input).
\end{theorem}

\begin{figure}
	\begin{tikzpicture}[auto,initial text=,node distance=0.5cm]
		\node[initial,state] (s0) {$s_0$};

		\node[actionnode,right=0.25cm of s0] (s0a) {};

		\node[state,right=0.5cm of s0a] (x) {$\texttt{?}_m$};
		\node[draw=none,above=1.25cm of x] (xdotsabove) {$\vdots$};
		\node[draw=none,below=1.25cm of x] (xdotsbelow) {$\vdots$};

		\node[actionnode,above right=0.25cm and 0.5cm of x] (xt) {};
		\node[actionnode,below right=0.25cm and 0.5cm of x] (xf) {};

		\node[above right=1cm and 1cm of xt] (xt_commit_mid) {};
		\node[state,left=0.2cm of xt_commit_mid,fill=lightgray!50] (xt_commit_above) {\scriptsize $10_m$};
		\node[state,right=0.2cm of xt_commit_mid,fill=lightgray!50] (xt_commit_below) {\scriptsize $0_m$};
		\node[state,below right=1cm and 0.75cm of xf,fill=lightgray!50] (xf_commit) {\scriptsize $5_m$};

		\node[state,right=2cm of xt] (xt_commit_node) {$x_m$};
		\node[state,right=2cm of xf] (xf_commit_node) {$\overline{x}_m$};

		\node[actionnode,right=0.25cm of xt_commit_node] (xt_action) {};
		\node[actionnode,right=0.25cm of xf_commit_node] (xf_action) {};

		\node (clause_anchor) at ($(xt_action)!0.5!(xf_action)$) {};
		\node[right=0.5cm of clause_anchor,state] (c2) {$c_{n_2}$};
		\node[above=of c2,state]       (c1) {$c_{n_1}$};
		\node[below=of c2,state]       (c3) {$c_{n_3}$};

		\node[above=0.1cm of c1] {$\vdots$};
		\node[below=0cm of c3] {$\vdots$};

		\path[->]
			(s0) edge[actionedge]              node[action] {} (s0a)

			(s0a) edge[probedge,pos=0.75]      node[prob] {} (x)
			(s0a) edge[probedge,pos=0.75]      node[prob] {} (xdotsabove)
			(s0a) edge[probedge,pos=0.75,swap] node[prob] {} (xdotsbelow)

			(x) edge[actionedge,pos=0.9,looseness=0.75,bend left]       node[action,anchor=south east] {$x_m = \texttt{tt}$} (xt)
			(x) edge[actionedge,pos=0.9,looseness=0.75,bend right,swap] node[action,anchor=north east] {$x_m = \texttt{ff}$} (xf)

			(xt) edge[probedge,looseness=1.25,out=0,in=-90,pos=0.75]   node[prob] {$0.45$} (xt_commit_above)
			(xt) edge[probedge,looseness=1,out=0,in=-100,pos=0.75]     node[prob] {$0.05$} (xt_commit_below)
			(xt) edge[probedge,pos=0.75,swap]                          node[prob] {$0.5$}  (xt_commit_node)
			(xf) edge[probedge,looseness=1,out=1,in=90,swap,pos=0.75]  node[prob] {$0.5$}  (xf_commit)
			(xf) edge[probedge,pos=0.75]                               node[prob] {$0.5$}  (xf_commit_node)

			(xt_commit_above) edge[directedge,loop left] (xt_commit_above)
			(xt_commit_below) edge[directedge,loop right] (xt_commit_below)
			(xf_commit) edge[directedge,loop right] (xf_commit)

			(xf_commit_node) edge[actionedge] (xf_action)
			(xt_commit_node) edge[actionedge] (xt_action)

			(xt_action) edge[probedge] (c1)
			(xt_action) edge[probedge] (c2)
			(xf_action) edge[probedge] (c3)

			(c1) edge[directedge,loop right] (c1)
			(c2) edge[directedge,loop right] (c2)
			(c3) edge[directedge,loop right] (c3)
		;

	\end{tikzpicture}
	\caption{Gadget for variable $x_m$.
	Uniform transition probabilities are omitted for readability.}
	\label{fig:reach_np_hard_gadget}
\end{figure}

\begin{proof
	We prove hardness by reduction from 3-SAT.
	The core idea is to utilize observations from Fig.~\ref{fig:mdp_cvar_hard} and Ex.~\ref{ex:mdp_cvar_hard}, namely that CVaR constraints can be used to enforce a deterministic choice.

	Let $\{C_n\}$ be a set of $N$ clauses with $M$ variables $x_m$ and set the dimensions $d = N + M$.
	By abuse of notation, $n$ refers to the dimension of clause $C_n$ and $m$ to the one of variable $x_m$, respectively.

	The gadget for the reduction is outlined in Fig.~\ref{fig:reach_np_hard_gadget}.
	Observe that, due to the structure of the MDP, we have that $R^\mathsf{r} = R^\mathsf{m}$.

	Overall, the reduction works as follows.
	Initially, a state $\texttt{?}_m$, representing the variable $x_m$, is chosen uniformly.
	In this state, the strategy is asked to give the valuation of $x_m$ through the actions \enquote{$x_m = \texttt{tt}$} or \enquote{$x_m = \texttt{ff}$}.
	As seen in Ex.~\ref{ex:mdp_cvar_hard}, the structure of the shaded states can be used to enforces a deterministic choice between the two actions.
	Particularly, in dimension $m$ we require $\CVaR_p \geq 5$ for $p = \frac{M-1}{M} + \frac{1}{M} \cdot 0.5 \cdot 0.2$.
	Since all other gadgets yield 0 in dimension $m$ and only half of the runs going through $\texttt{?}_m$ end up in the shaded area, this corresponds to Ex.~\ref{ex:mdp_cvar_hard}, where $p = 0.2$.

	Once in either state $x_m$ or $\overline{x}_m$, a state $c_n$ corresponding to a clause $C_n$ satisfied by this assignment is chosen uniformly.
	In the example gadget, we would have $x_m \in C_{n_1} \intersectionBin C_{n_2}$, and $\overline{x}_m \in C_{n_3}$.
	We set the reward of $c_n$ to $1_n$.
	Then a clause $c_n$ is satisfied under the assignment if the state $c_n$ is visited with positive probability, e.g. if $\CVaR_1 \geq \frac{1}{M} \cdot 0.5 \cdot \frac{1}{N}$.
	Clearly, a satisfying assignment exists iff a strategy satisfying these constraints exists.
\end{proof}

\subsection{NP-completeness and strategies for reachability}

For weighted reachability, we prove that the previously presented bound is tight, i.e.\ that the weighted reachability problem with multiple dimensions and $\CVaR$ constraints is NP-complete when $d$ is part of the input and $P$ otherwise.
First, we show that the strategy bounds of the single dimensional case directly transfer.
Intuitively, this is the case since only the steady state distribution over the target set $T$ is relevant, independent of the dimensionality.

\begin{theorem}
	Two-memory stochastic strategies (i.e.\ with both randomization and stochastic update) are sufficient for $\mathsf{MDP}_{\mathsf{r}, \mathsf{multi}}^{\{\Expectation, \VaR, \CVaR\}}$.
	Moreover, if $\mathbf{r}_j(s) \geq 0$ for all $s \in T$ and $j \in [d]$, then memoryless randomizing strategies are sufficient.
\end{theorem}

\begin{proof}
	Follows directly from the reasoning used in the proofs of Thm.~\ref{stm:mdp_exp_mean_strategies} and Thm.~\ref{stm:mdp_exp_reach_strategies}.
\end{proof}

\begin{figure}
	\begin{enumerate}
		\renewcommand{\labelenumi}{(\arabic{enumi}) }
		\item \label{fig:reach_lp_multi:non-neg}
		All variables $y_a$, $x_s$, $\underline{x}_s^j$ are non-negative.
		\setcounter{enumi}{3}
		\item \label{fig:reach_lp_multi:var_split}
		$\VaR$-consistent split for $j \in [d]$:
		\begin{align*}
			\underline{x}_s^j & = x_s \text{ for $s \in T_<^j$} & \underline{x}_s^j & \leq x_s \text{ for $s \in T_=^j$}
		\end{align*}
		\item \label{fig:reach_lp_multi:probability_split}
		Probability-consistent split for $j \in [d]$:
		\begin{equation*}
			{\sum}_{s \in T_\leq^j} \underline{x}_s^j = \mathsf{\mathbf{p}}_j
		\end{equation*}
		\item \label{fig:reach_lp_multi:satisfaction}
		CVaR and expectation satisfaction for $j \in [d]$:
		\begin{align*}
			{\sum}_{s \in T_\leq^j} \underline{x}_s \cdot \mathbf{r}(s) & \geq \mathsf{p}_j \cdot \mathsf{\mathbf{c}}_j &
			{\sum}_{s \in T} x_s \cdot \mathbf{r}_j(s) & \geq \mathsf{\mathbf{e}}_j
		\end{align*}
	\end{enumerate}
	\caption{LP used to decide multi-dimensional weighted reachability queries given a guess $\textbf{t}$ of $\VaR_{\mathsf{p}_j}$.
		Equalities~\eqref{fig:reach_lp:flow} and \eqref{fig:reach_lp:recurrent_switch} are as in Fig.~\ref{fig:reach_lp}, $T_\sim^j := \{s \in T \mid \mathbf{r}_j(s) \sim \textbf{t}_j\}$, $\sim \in \{<, =, \leq\}$.}
	\label{fig:reach_lp_multi}
\end{figure}

\begin{theorem}
	$\mathsf{MDP}_{\mathsf{r}, \mathsf{multi}}^{ \{\Expectation, \VaR, \CVaR\}}$ is in NP if $d$ is a part of the input; moreover, it is in P for any fixed $d$.
\end{theorem}

\begin{proof}[Proof sketch]
	To prove containment, we guess the VaR threshold vector $\mathbf{t}$ out of the set of potential ones, namely $\{r \mid \exists i \in [d], s \in T. \mathbf{r}_i(s) = r\}^d$ and use an LP to verify the solution.
	We again assume that each MEC can reach the target set and is single-state, as we did for Fig.~\ref{fig:reach_lp}.
	The arguments used to resolve this assumption are still applicable in the multi-dimensional setting.
	The LP consists of the flow Equalities~\eqref{fig:reach_lp:flow} and \eqref{fig:reach_lp:recurrent_switch} from the LP in Fig.~\ref{fig:reach_lp} together with the modified (In)Equalities~\eqref{fig:reach_lp_multi:var_split}-\eqref{fig:reach_lp_multi:satisfaction} as shown in Fig.~\ref{fig:reach_lp_multi}.

	The difference is that we extract the worst fraction of the flow \emph{in each dimension}.
	Consequently, we have $d$ instances of each $\underline{x}_s$ variable, namely $\underline{x}_s^j$.
	The number of possible guesses $\mathbf{t}$ is bounded by $\cardinality{T}^d$ and thus the guess is of polynomial length.
	For a fixed $d$ the bound itself is polynomial and hence, as previously, we can try out all vectors.
\end{proof}

\subsection{Upper bounds of mean payoff}

In this section, we provide an upper bound on the complexity of mean-payoff queries.
Strategies in this context are known to have higher complexity.

\begin{proposition}[\cite{DBLP:journals/corr/abs-1104-3489}]
	Infinite memory is necessary for $\mathsf{MDP}^{\{\Expectation\}}_{\mathsf{m}, \mathsf{multi}}$.
\end{proposition} %
Note that this directly transfers to $\mathsf{MDP}^{\{\CVaR\}}_{\mathsf{m}, \mathsf{multi}}$, as $\CVaR_1 = \mathbb{E}$.
However, closing gaps between lower and upper bounds for the mean payoff objective is notoriously more difficult.
For instance, $\mathsf{MDP}_{\mathsf{m},\mathsf{multi}}^{\{\VaR\}}$ is known to be in EXP, but not even known to be NP-hard, neither is $\mathsf{MDP}_{\mathsf{m},\mathsf{multi}}^{\{\Expectation,\VaR\}}$.
Since we have proven that $\mathsf{MDP}_{\mathsf{m},\mathsf{multi}}^{\{\CVaR\}}$ is NP-hard, we can expect that obtaining the matching NP upper bound will be yet more difficult.
The fundamental difference of the multi-dimensional mean-payoff case is that the solutions within MECs cannot be pre-computed, rather non-trivial trade-offs must be considered.
Moreover, the trade-offs are not \enquote{local} and must be synchronized over all the MECs, see~\cite{DBLP:conf/lics/ChatterjeeKK15} for details.

We now observe that, as opposed to quantile queries, i.e. $\VaR$ constraints, the behaviour inside each MEC can be assumed to be quite simple.
Our results primarily rely on \cite{DBLP:journals/lmcs/ChatterjeeKK17} and use a similar notation.
In particular, given a run $\rho$, $\mathrm{Freq}_a(\rho)$ yields the average frequency of action $a$, i.e. $\mathrm{Freq}_a(\rho) := \liminf_{n \to \infty} \frac{1}{n} \sum_{t = 1}^n \mathbbm{1}_a(a_t)$, where $a_t$ refers to the action taken by $\rho$ in step $t$.

\begin{definition}
	A strategy $\sigma$ is \emph{MEC-constant} if for all $M_i \in \mathsf{MEC}$ with $\mathbb{P}^\sigma[\diamondsuit\Box M_i] > 0$ and all $j \in [d]$ there is a $v \in \mathbb{R}$ such that
	$\mathbb{P}^\sigma[R^\mathsf{m}_j = v \mid \diamondsuit\Box M_i] = 1$.
\end{definition}

\begin{lemma} \label{stm:mean_multi_mec_constant_strategies}
	MEC-constant strategies are sufficient for $\mathsf{MDP}^{\{\Expectation, \CVaR\}}_{\mathsf{m}, \mathsf{multi}}$.
\end{lemma}
\begin{proof}
	Fix an MDP $\mathcal{M}$ with MECs $\mathsf{MEC} = \{M_1, \dots, M_n\}$, reward function $\mathbf{r}$ and a strategy $\sigma$.
	Further, define $p_i = \mathbb{P}^\sigma[\diamondsuit\Box M_i]$.
	We construct a strategy $\sigma'$ so that (i)~$\mathbb{P}^{\sigma'}[\diamondsuit\Box M_i] = p_i$ for all $M_i$, and (ii)~all behaviours of $\sigma$ on a MEC $M_i$ are \enquote{mixed} into each run on $M_i$, making it MEC-constant.

	We first define the mixing strategies $\sigma_i$, achieving point (ii).
	By \cite[Sec.~4.1]{DBLP:journals/lmcs/ChatterjeeKK17}, there are frequencies $(x_a)_{a \in \mathsf{A}}$ which
	\begin{itemize}
		\item satisfy $\sum_{a \in A} x_a \cdot \Delta(a, s) = \sum_{a \in \mathsf{Av}(s)} x_a$ for all $s \in S$,
		\item for each action $a$ we have $\mathbb{E}^\sigma[\mathrm{Freq}_a] \leq x_a$, and
		\item $\sum_{a \in \mathsf{A} \intersectionBin M_i} x_a = p_i$.
	\end{itemize}
	By \cite[Cor.~5.5]{DBLP:journals/lmcs/ChatterjeeKK17}, there is a (Markov) strategy $\sigma_i$ on $M_i$ where
	\begin{equation*}
		\mathbb{P}^{\sigma_i}\left[\mathrm{Freq}_a = x_a / p_i \right] = 1.
	\end{equation*}
	Consequently, $\sigma_i$ is almost surely constant on $M_i$ w.r.t. $R^\mathsf{m}$.
	We apply the reasoning used in the proof of Thm.~\ref{stm:mdp_exp_mean_strategies} to obtain the combined strategy $\sigma'$ which achieves point (i) and switches to $\sigma_i$ upon remaining in $M_i$.

	Now, fix any  $j \in [d]$, $M_i \in \mathsf{MEC}$, and $p, q \in (0, 1)$.
	We have that $\mathbb{E}^{\sigma_i}[\mathrm{Freq}_a \mid \diamondsuit\Box M_i] \geq \mathbb{E}^\sigma[\mathrm{Freq}_a \mid \diamondsuit\Box M_i]$ by construction.
	Consequently, $\mathbb{E}^{\sigma'}(R^\mathsf{m}_j) \geq \mathbb{E}^{\sigma}(R^\mathsf{m}_j)$.

	Since $\sigma'$ is MEC-constant, we have $\CVaR_p^{\sigma'}(R^\mathsf{m}_j \mid \diamondsuit\Box M_i) = \mathbb{E}^{\sigma'}[R^\mathsf{m}_j \mid \diamondsuit\Box M_i]$.
	Further, by $\mathbb{E}^\sigma[\mathrm{Freq}_a \mid \diamondsuit\Box M_i] \cdot p_i \leq \mathbb{E}^{\sigma_i}[\mathrm{Freq}_a]$ for all $a$, we get $\mathbb{E}^\sigma[R^\mathsf{m}_j \mid \diamondsuit\Box M_i] \leq \mathbb{E}^{\sigma_i}[R^\mathsf{m}_j]$.
	So, $\CVaR_p^{\sigma_i}(R^\mathsf{m}_j) = \mathbb{E}^{\sigma_i}[R^\mathsf{m}_j] \geq \mathbb{E}^\sigma[R^\mathsf{m}_j \mid \diamondsuit\Box M_i] \geq \CVaR_q^{\sigma}(R^\mathsf{m}_j \mid \diamondsuit\Box M_i)$, as $\CVaR \leq \mathbb{E}$.

	Finally, we apply this inequality together with property (i), obtaining $\CVaR_p^{\sigma}(R^\mathsf{m}_j) \leq \CVaR_p^{\sigma'}(R^\mathsf{m}_j)$ by Thm.~\ref{stm:cvar_partitioning}.
\end{proof}

We utilize this structural property to design a linear program for these constraints.
However, similarly to the previously considered LPs, it relies on knowing the $\VaR$ for each $\CVaR_\mathsf{p}$ constraint.
Due to the non-linear behaviour of $\CVaR$, the classical techniques do not allow us to conclude that $\VaR$ is polynomially sized and thus we do not present the \enquote{matching} NP upper bound, but a PSPACE upper bound, which we achieve as follows.

\begin{figure}
	\renewcommand{\labelenumi}{(\arabic{enumi}) }
	\begin{enumerate}
		\item \label{fig:mean_lp_multi:non-neg}
		All variables $y_a$, $y_s$, $x_a$, $x_s$ are non-negative.
		\item \label{fig:mean_lp_multi:transient}
		Transient flow for $s \in S$:
		\begin{equation*}
			\mathbbm{1}_{s_0}(s) + {\sum}_{a \in \mathsf{A}} y_a \cdot \Delta(a, s) = {\sum}_{a \in \mathsf{Av}(s)} y_a + y_s
		\end{equation*}
		\item \label{fig:mean_lp_multi:switching}
		Probability of switching in a MEC is the frequency of using its actions for $M_i \in \mathsf{MEC}$:
		\begin{equation*}
			{\sum}_{s \in M_i} y_s = {\sum}_{a \in M_i} x_a
		\end{equation*}
		\item \label{fig:mean_lp_multi:recurrent}
		Recurrent flow for $s \in S$:
		\begin{equation*}
			x_s = {\sum}_{a \in \mathsf{A}} x_a \cdot \Delta(a, s) = {\sum}_{a \in \mathsf{Av}(s)} x_a
		\end{equation*}
		\item \label{fig:mean_lp_multi:satisfaction}
		$\CVaR$ and expectation satisfaction for $j \in [d]$:
		\begin{gather*}
			{\sum}_{s \in S^j_\leq} x_s \cdot \mathbf{r}_j(s) + \left(\mathsf{\mathbf{p}}_j  - {\sum}_{s \in S^j_\leq} x_s\right) \cdot \textbf{t}_j \geq \mathsf{\mathbf{p}}_j \cdot \mathsf{\mathbf{c}}_j \\
			{\sum}_{s \in S} x_s \cdot \mathbf{r}_j(s) \geq \mathsf{\mathbf{e}}_j
		\end{gather*}
		\item \label{fig:mean_lp_multi:verify_mec}
		Verify MEC classification guess for $j \in [d]$:
		\begin{align*}
			{\sum}_{s \in M^j_\leq} x_s \cdot \mathbf{r}_j(s) & \leq \textbf{t}_j \quad \text{ for $M^j_\leq \in \mathsf{MEC}^j_\leq \unionBin \{M^j_=\}$} \\
			{\sum}_{s \in M^j_\geq} x_s \cdot \mathbf{r}_j(s) & \geq \textbf{t}_j \quad \text{ for $M^j_\geq \in \mathsf{MEC}^j_> \unionBin \{M^j_=\}$}
		\end{align*}
		\item \label{fig:mean_lp_multi:verify_var}
		Verify VaR guess for $j \in [d]$:
		\begin{align*}
			{\sum}_{s \in S^j_\leq} x_s & \leq \mathsf{\mathbf{p}}_j &
			{\sum}_{s \in S^j_\leq \unionBin M^j_=} x_s & \geq \mathsf{\mathbf{p}}_j
		\end{align*}
	\end{enumerate}

	\caption{LP used to decide multi-dimensional mean-payoff queries given a guess \textbf{t} of $\VaR_{\mathsf{p}_j}$ and MEC classification $\mathsf{MEC}_\leq^j$, $M_=^j$, and $\mathsf{MEC}_>^j$.
		$S_\sim^j := \{s \in S \mid s \in M \text{ and } M \in \mathsf{MEC}_\sim^j\}$, $\sim \in \{\leq, >\}$.} \label{fig:mean_lp_multi}
\end{figure}

\begin{theorem}
	$\mathsf{MDP}^{\{\Expectation, \CVaR\}}_{\mathsf{m}, \mathsf{multi}}$ is in PSPACE.
\end{theorem}

\begin{proof}[Proof sketch]
	We use the existential theory of the reals, which is NP-hard and in PSPACE \cite{DBLP:conf/stoc/Canny88}, to encode our problem.
	The VaR vector \textbf{t} is existentially quantified and the formula is a polynomially sized program with constraints linear in VaR's and linear in the remaining variables.
	This shows the complexity result.

	The details of the procedure are as follows.
	For each $j \in [d]$, we use the existential theory of reals to guess the achieved VaR $\textbf{t} = \VaR_{\mathsf{\mathbf{p}}_j}$.
	Further, we non-deterministically obtain the following polynomially-sized information (or deterministically try out all options in PSPACE).
	For each $j \in [d]$ and for each MEC $M_i$, we guess if the value achieved in $M_i$ is at most (denoted $M_i \in \mathsf{MEC}_\leq^j$) or above (denoted $M_i \in \mathsf{MEC}_>^j$) the respective $\textbf{t}_j$, and exactly one MEC $M^j_=$, which achieves a value equal to it.
	Given these guesses, we check whether the LP in Fig.~\ref{fig:mean_lp_multi} has a solution.

	Equations~\eqref{fig:mean_lp_multi:non-neg}-\eqref{fig:mean_lp_multi:recurrent} describe the transient flow like the previous LP's and, additionally, the recurrent flow like in \cite[Sec.~9.3]{Puterman-book} or \cite{DBLP:journals/lmcs/EtessamiKVY08,DBLP:journals/corr/abs-1104-3489,DBLP:journals/lmcs/ChatterjeeKK17}.
	This addition is needed, since now our MECs are not trivial, i.e. single state.
	Again, Inequalities~\eqref{fig:mean_lp_multi:satisfaction} verify that the CVaR and expectation constraints are satisfied.
	Finally, Inequalities~\eqref{fig:mean_lp_multi:verify_mec} and \eqref{fig:mean_lp_multi:verify_var} verify the previously guessed information, i.e. the VaR vector and the MEC classification.

	Using the very same techniques, it is easy to prove that solutions to the LP correspond to satisfying strategies and vice versa.
	In particular, Inequalities~\eqref{fig:mean_lp_multi:verify_mec} and \eqref{fig:mean_lp_multi:verify_var} directly make use of the MEC-constant property of Lem.~\ref{stm:mean_multi_mec_constant_strategies}.
\end{proof}

While MEC-constant strategies are sufficient for $\Expectation$ with $\CVaR$, in contrast, they are not even for just $\mathsf{MDP}^{\{\VaR\}}_{\mathsf{m}, \mathsf{multi}}$ \cite[Ex.22]{DBLP:conf/lics/ChatterjeeKK15}.
Consequently, only an exponentially large LP is known for $\mathsf{MDP}^{\{\VaR\}}_{\mathsf{m}, \mathsf{multi}}$.
We can combine all the objective functions together as follows:

\begin{theorem}
	$\mathsf{MDP}^{\{\Expectation, \VaR, \CVaR\}}_{\mathsf{m}, \mathsf{multi}}$ is in EXPSPACE.
\end{theorem}
\begin{proof}[Proof sketch]
	We proceed exactly as in the previous case, but now the flows in Equality~\eqref{fig:mean_lp_multi:recurrent} are split into exponentially many flows, depending on the set of dimensions where they achieve the given VaR threshold, see LP $L$ in \cite[Fig.~4]{DBLP:conf/lics/ChatterjeeKK15}.
	The resulting size of the program is polynomial in the size of the system and exponential in $d$.
	Hence the call to the decision procedure of the existential theory of reals results in the EXPSPACE upper bound.
\end{proof}

\begin{table*}
	\caption{
	Schematic summary of known and new results.
	Strategies are abbreviated by \enquote{C/$n$-M}, where C is either \emph{D}eterministic or \emph{R}andomizing, $n$ is the size of the memory, and M is either \emph{D}etereministic or \emph{S}tochastic \emph{MEM}ory.
	} %
	\small %
	\begin{tabular}{c|cc||c|cccc}
		$\mathbf{dim}$  &              \multicolumn{2}{c||}{$\mathsf{single}$}               &                                                            \multicolumn{5}{c}{$\mathsf{multi}$}                                                             \\
		$\mathbf{obj}$  &                 \multicolumn{2}{c||}{\textsf{any}}                 &    $\mathsf{r}$    &                                                \multicolumn{4}{c}{$\mathsf{m}$}                                                 \\
		$\mathbf{crit}$ & $\cardinality{\mathbf{crit}} = 1$ & $\cardinality{\mathbf{crit}} \geq 2$ & $\CVaR \in \mathbf{crit}$ & $\{\Expectation,\VaR_0\}$ & $\{\VaR\}$ & $\{\CVaR\}, \{\CVaR, \mathbb{E}\}$ & $\{\mathbb{E}, \CVaR, \VaR\}$ \\ \midrule
		  Complex.   &                      \multicolumn{2}{c||}{P}                       & NP-c., P for fixed $d$ &                  P                  &         EXP         &            NP-h., PSPACE             &         NP-h., EXPSPACE         \\
		   Strat.    &            D/1-MEM             &             R/2-SMEM              &        R/2-SMEM        &                                            \multicolumn{4}{c}{ \rule[0.5\parskip]{2cm}{0.1pt} \quad R/$\infty$-DMEM \quad \rule[0.5\parskip]{2cm}{0.1pt}}

	\end{tabular} \label{tbl:results} %
\end{table*}

\section{Conclusion}

We introduced the conditional value-at-risk for Markov decision processes in the setting of classical verification objectives of reachability and mean payoff.
We observed that in the single dimensional case the additional CVaR constraints do not increase the computational complexity of the problems.
As such they provide a useful means for designing risk-averse strategies, at no additional cost.
In the multidimensional case, the problems become NP-hard.
Nevertheless, this may not necessarily hinder the practical usability.
Our results are summarized in Table~\ref{tbl:results}.

We conjecture that the VaR's for given CVaR constraints are polynomially large numbers.
In that case, the provided algorithms would yield NP-completeness for $\mathsf{MDP}^{\{\CVaR\}}_{\mathsf{m}, \mathsf{multi}}$ and EXPTIME containment for $\mathsf{MDP}^{\{\Expectation,\VaR, \CVaR\}}_{\mathsf{m}, \mathsf{multi}}$, where the exponential dependency is only on the dimension.

\section{Preliminaries}

Due to space constraints, some proofs and explanations are shortened or omitted when clear and can be found in the appendix.

\subsection{Basic definitions}

We mostly follow the definitions of \cite{DBLP:conf/lics/ChatterjeeKK15,DBLP:journals/corr/abs-1104-3489}.
$\mathbb{N}, \mathbb{Q}, \mathbb{R}$ are used to denote the sets of positive integers, rational and real numbers, respectively.
For $n \in \mathbb{N}$, let $[n]=\{1, \ldots, n\}$.
Further, $k_j$ refers to $k \cdot e_j$, where $e_j$ is the unit vector in dimension $j$.

We assume familiarity with basic notions of probability theory, e.g., \emph{probability space} $(\Omega, \mathcal{F}, \mu)$, \emph{random variable} $F$, or \emph{expected value} $\mathbb{E}$.
The set of all distributions over a countable set $C$ is denoted by $\mathcal{D}(C)$.
Further, $d \in \mathcal{D}(C)$ is Dirac if $d(c) = 1$ for some $c \in C$.
To ease notation, for functions yielding a distribution over some set $C$, we may write $f(\cdot, c)$ instead of $f(\cdot)(c)$ for $c \in C$.

\paragraph{Markov chains}
A \emph{Markov chain} (MC) is a tuple $\mathsf{M} = (S, \delta, \mu_0)$, where
	$S$ is a countable set of states\footnote{We allow the state set to be countable for the formal definition of strategies on MDP.
		When dealing with Markov Chains in queries, we only consider finite state sets.},
	$\delta : S \to \mathcal{D}(S)$ is a probabilistic transition function, and
	$\mu_0 \in \mathcal{D}(S)$ is the initial probability distribution.
The SCCs and BSCCs of a MC are denoted by $\mathsf{SCC}$ and $\mathsf{BSCC}$, respectively~\cite{Puterman-book}.

A \emph{run} in $\mathsf{M}$ is an infinite sequence $\rho = s_1 s_2 \cdots$ of states, we write $\rho_i$ to refer to the $i$-th state $s_i$.
A \emph{path} $\varrho$ in $\mathsf{M}$ is a finite prefix of a run $\rho$.
Each path $\varrho$ in $\mathsf{M}$ determines the set $\mathsf{Cone}(\varrho)$ consisting of all runs that start with $\varrho$.
To $\mathsf{M}$, we associate the usual probability space $(\varOmega, \mathcal{F}, \mathbb{P})$, where $\varOmega$ is the set of all runs in $\mathsf{M}$, $\mathcal{F}$ is the $\sigma$-field generated by all $\mathsf{Cone}(\varrho)$, and $\mathbb{P}$ is the unique probability measure such that $\mathbb{P}(\mathsf{Cone}(s_1 \cdots s_k)) = \mu_0(s_1) \cdot \prod_{i=1}^{k-1} \delta(s_i, s_{i+1})$.
Furthermore, $\diamondsuit B$ ($\diamondsuit \Box B$) denotes the set of runs which eventually reach (eventually remain in) the set $B \subseteq S$, i.e.\ all runs where $\rho_i \in B$ for some $i$ (there exists an $i_0$ such that $\rho_i \in B$ for all $i \geq i_0$).

\paragraph{Markov decision processes}
A \emph{Markov decision process} (MDP) is a tuple $\mathcal{M} = (S, \mathsf{A}, \mathsf{Av}, \Delta, s_0)$ where
	$S$ is a finite set of states,
	$\mathsf{A}$ is a finite set of actions,
	$\mathsf{Av} : S \rightarrow 2^\mathsf{A} \setminus \{\emptyset\}$ assigns to each state $s$ the set $\mathsf{Av}(s)$ of actions enabled in $s$ so that $\{\mathsf{Av}(s) \mid s \in S\}$ is a partitioning of $\mathsf{A}$\footnote{In other words, each action is associated with exactly one state.},
	$\Delta : \mathsf{A} \rightarrow \mathcal{D}(S)$ is a probabilistic transition function that given an action $a$ yields a probability distribution over the successor states, and
	$s_0$ is the initial state of the system.

A \emph{run} $\rho$ of $\mathcal{M}$ is an infinite alternating sequence of states and actions $\rho = s_1 a_1 s_2 a_2 \cdots$ such that for all $i \geq 1$, we have $a_i \in \mathsf{Av}(s_i)$ and $\Delta(a_i, s_{i+1}) > 0$.
Again, $\rho_i$ refers to the $i$-th state visited by this particular run.
A \emph{path} of length $k$ in $\mathcal{M}$ is a finite prefix $\varrho = s_1 a_1 \cdots a_{k-1} s_k$ of a run in $G$.

\paragraph{Strategies and plays.}
Intuitively, a strategy in an MDP $\mathcal{M}$ is a \enquote{recipe} to choose actions based on the observed events.
Usually, a strategy is defined as a function $\sigma : (S \mathsf{A})^*S \to \mathcal{D}(\mathsf{A})$ that given a finite path $\varrho$, representing the history of a play, gives a probability distribution over the actions enabled in the last state.
We adopt the slightly different, though equivalent~\cite[Sec.~6]{DBLP:journals/corr/abs-1104-3489} definition from~\cite{DBLP:conf/lics/ChatterjeeKK15}, which is more convenient for our setting.

Let $\mathsf{M}$ be a countable set of \emph{memory elements}.
A \emph{strategy} is a triple $\sigma = (\sigma_u, \sigma_n, \alpha)$, where
	$\sigma_u: \mathsf{A} \times S \times \mathsf{M} \to \mathcal{D}(\mathsf{M})$ and
	$\sigma_n: S \times \mathsf{M} \to \mathcal{D}(\mathsf{A})$ are \emph{memory update} and \emph{next move} functions, respectively, and
	$\alpha \in \mathcal{D}(\mathsf{M})$ is the initial memory distribution.
We require that, for all $(s, m) \in S \times \mathsf{M}$, the distribution $\sigma_n(s,m)$ assigns positive values only to actions available at $s$, i.e.\ $\supp \sigma_n(s,m) \subseteq \mathsf{Av}(s)$.

A \emph{play} of $\mathcal{M}$ determined by a strategy $\sigma$ is a Markov chain $\mathcal{M}^\sigma = (S^\sigma, \delta^\sigma, \mu_0^\sigma)$, where
	the set of states is $S^\sigma = S \times \mathsf{M} \times \mathsf{A}$,
	the initial distribution $\mu_0$ is zero except for $\mu_0^\sigma(s_0, m, a) = \alpha(m) \cdot \sigma_n(s_0, m, a)$, and
	the transition probability from $s^\sigma = (s, m, a)$ to ${s'}^\sigma = (s', m', a')$ is $\delta^\sigma(s^\sigma, {s'}^\sigma) = \Delta(a, s') \cdot \sigma_u(a, s', m, m') \cdot  \sigma_n(s',m', a')$.
Hence, $\mathcal{M}^\sigma$ starts in a location chosen randomly according to $\alpha$ and $\sigma_n$.
In state $(s, m, a)$ the next action to be performed is $a$, hence the probability of entering $s'$ is $\Delta(a, s')$.
The probability of updating the memory to $m'$ is $\sigma_u(a, s', m, m')$, and the probability of selecting $a'$ as the next action is $\sigma_n(s',m', a')$. Since these choices are independent, and thus we obtain the product above.

Technically, $\mathcal{M}^\sigma$ induces a probability measure $\mathbb{P}^\sigma$ on $S^\sigma$.
Since we mostly work with the corresponding runs in the original MDP, we overload $\mathbb{P}^\sigma$ to also refer to the probability measure obtained by projecting onto $S$.
Further, \enquote{almost surely} etc. refers to happening with probability 1 according to $\mathbb{P}^\sigma$.
The expected value of a random variable $X : \varOmega \to \mathbb{R}$ is $\mathbb{E}^\sigma[X] = \int_\varOmega X \ d\mathbb{P}^\sigma$.

A convex combinations of two strategies $\sigma_1$ and $\sigma_2$, written as $\sigma_\lambda = \lambda \sigma_1 + (1-\lambda) \sigma_2$, can be obtained by defining the memory as $\mathsf{M}_\lambda = \{1\} \times \mathsf{M}_1 \unionBin \{2\} \times \mathsf{M}_2$, randomly choosing one of the two strategies via the initial memory distribution $\alpha_\lambda$ and then following the chosen strategy.
Clearly, we have that $\mathbb{P}^{\sigma_\lambda} = \lambda \mathbb{P}^{\sigma_1} + (1-\lambda) \mathbb{P}^{\sigma_2}$.

\paragraph{Strategy types.}
A strategy $\sigma$ may use infinite memory $\mathsf{M}$, and both $\sigma_u$ and $\sigma_n$ may randomize.
The strategy $\sigma$ is
\begin{itemize}
	\item \emph{deterministic-update}, if $\alpha$ is Dirac and the memory update function $\sigma_u$ gives a Dirac distribution for every argument;
	\item \emph{deterministic}, if it is deterministic-update and the next move function $\sigma_n$ gives a Dirac distribution for every argument.
\end{itemize}
A \emph{stochastic-update} strategy is a strategy that is not necessarily deterministic-update and \emph{randomized} strategy is a strategy that is not necessarily deterministic.
We also classify the strategies according to the size of memory they use.
Important subclasses are
	\emph{memoryless} strategies, in which $\mathsf{M}$ is a singleton,
	\emph{$n$-memory} strategies, in which $\mathsf{M}$ has exactly $n$~elements, and
	\emph{finite-memory} strategies, in which $\mathsf{M}$ is finite.

\paragraph{End components.}
A tuple $(T, B)$ where $\emptyset \neq T \subseteq S$ and $\emptyset \neq B \subseteq \bigcup_{t\in T} \mathsf{Av}(t)$ is an \emph{end component} of the MDP $\mathcal{M}$ if
	(i)~for all actions $a \in B$, $\Delta(a, s') > 0$ implies $s'\in T$; and
	(ii)~for all states $s, t \in T$ there is a path $\varrho = s_1 a_1\cdots a_{k-1} s_k \in (TB)^{k-1}T$ with $s_1 = s$, $s_k = t$.
An end component $(T, B)$ is a \emph{maximal end component (MEC)} if $T$ and $B$ are maximal with respect to subset ordering.
Given an MDP, the set of MECs is denoted by $\mathsf{MEC}$.
By abuse of notation, $s \in M$ refers to all states of a MEC $M$, while $a \in M$ refers to the actions.

\begin{remark} \label{rem:mec_decomposition_ptime}
	Computing the maximal end component (MEC) decomposition of an MDP, i.e.\ the computation of $\mathsf{MEC}$, is in P~\cite{DBLP:journals/jacm/CourcoubetisY95}.
\end{remark}

\begin{remark} \label{rem:mec_almost_sure}
	For any MDP $\mathcal{M}$ and strategy $\sigma$, a run almost surely eventually stays in one MEC, i.e.\ $\mathbb{P}^\sigma[\UnionSym_{M_i \in \mathsf{MEC}} \diamondsuit\Box M_i] = 1$~\cite{Puterman-book}.
\end{remark}

\subsection{Random variables on Runs}

We introduce two standard random variables, assigning a value to each run of a Markov Chain or Markov Decision Process.

\paragraph{Weighted reachability.}
Let $T \subseteq S$ be a set of target states and $\mathbf{r} : T \mapsto \mathbb{Q}$ be a reward function.
Define the random variable $R^\mathsf{r}$ as $R^\mathsf{r}(\rho) = \mathbf{r}(\min_i \{\rho_i \mid \rho_i \in T\})$, if such an $i$ exists, and $0$ otherwise.
Informally, $R^\mathsf{r}$ assigns to each run the value of the first visited target state, or $0$ if none.
$R^\mathsf{r}$ is measurable and discrete, as $S$ is finite~\cite{Puterman-book}.
Whenever we are dealing with weighted reachability, we assume w.l.o.g. that all target states are absorbing, i.e.\ for any $s \in T$ we have $\delta(s, s) = 1$ for MC and $\Delta(a, s) = 1$ for all $a \in \mathsf{Av}(s)$ for MDP.

\paragraph{Mean payoff} (also known as \emph{long-run average reward}, and \emph{limit average reward}).
Again, let $\mathbf{r} : S \mapsto \mathbb{Q}$ be a reward function.
The mean payoff of a run $\rho$ is the average reward obtained per step, i.e. $R^\mathsf{m}(\rho) = \liminf_{n \to \infty} \frac{1}{n} \sum_{i = 1}^n \mathbf{r}(\rho_i).$
The $\liminf$ is necessary, since $\lim$ may not be defined in general.
Further, $R^\mathsf{m}$ is measurable~\cite{Puterman-book}.

\begin{remark}
	There are several distinct definitions of \enquote{weighted reachability}.
	The one chosen here primarily serves as foundation for the more general mean payoff.
\end{remark}

\section{CVaR in MC and MDP: Problem statement}

Now, we are ready to define our problem framework.
First, we explain the types of building blocks for our queries, namely lower bounds on expectation, CVaR, and VaR.
Formally, we consider the following types of constraints.
\begin{align*}
	\mathsf{e} & \leq \mathbb{E}(X) & \mathsf{c} & \leq \CVaR_\mathsf{p}(X) & \mathsf{v} & \leq \VaR_\mathsf{q}(X)
\end{align*}
$X$ is some real-valued random variable, assigning a payoff to each run.
With these constraints, the classes of queries are denoted by
\begin{equation*}
	\mathsf{MDP}^{\mathbf{crit}}_{\mathbf{obj}, \mathbf{dim}}
\end{equation*}
\begin{itemize}
	\item $\mathbf{crit} \subseteq \{\Expectation, \CVaR, \VaR\}$ are the types of constraints,
	\item $\mathbf{obj} \in \{\mathsf{r}, \mathsf{m}\}$ is the type of the objective function, either weighted reachability $\mathsf{r}$ or mean payoff $\mathsf{m}$, and
	\item $\mathbf{dim} \in \{\mathsf{single}, \mathsf{multi}\}$ is the dimensionality of the query.
\end{itemize}
We use $d$ to denote the dimensions of the problem, $d = 1$ iff $\mathbf{dim} = \mathsf{single}$.
As usual, we assume that all quantities of the input, e.g., probabilities of distributions, are rational.

An instance of these queries is specified by an MDP $\mathcal{M}$, a $d$-dimensional reward function $\mathbf{r} : S \to \mathbb{Q}^d$, and constraints from $\mathbf{crit}$, given by vectors $\mathsf{\mathbf{e}}, \mathsf{\mathbf{c}}, \mathsf{\mathbf{v}} \in (\mathbb{Q} \unionBin \{ \bot \})^d$ and $\mathsf{\mathbf{p}}, \mathsf{\mathbf{q}} \in (0, 1)^d$.
This implies that in each dimension there is at most one constraint per type.
The presented methods can easily be extended to the more general setting of multiple constraints of a particular type in one dimension.
The decision problem is to determine whether there exists a strategy $\sigma$ such that \emph{all} constraints are met.

Technically, this is defined as follows.
Let $X$ be the $d$-dimensional random variable induced by the objective $\mathbf{obj}$ and reward function $\mathbf{r}$, operating on the probability space of $\mathcal{M}^\sigma$.
The strategy $\sigma$ is a witness to the query iff for each dimension $j \in [d]$ we have that $\mathbb{E}[X_j] \geq \QueryVec{e}_j$, $\CVaR_{\mathsf{\mathbf{p}}_j}(X_j) \geq \mathsf{\mathbf{c}}_j$, and $\VaR_{\mathsf{\mathbf{q}}_j}(X_j) \geq \mathsf{\mathbf{v}}_j$.
Moreover, $\bot$ constraints are trivially satisfied.

For completeness sake, we also consider $\mathsf{MC}^{\mathbf{crit}}_{\mathbf{obj}, \mathbf{dim}}$ queries, i.e. the corresponding problem on (finite state) Markov chains.

\paragraph{Notation.}
We introduce the following abbreviations.
When dealing with an MDP $\mathcal{M}$, $\CVaR^\sigma_p$ denotes $\CVaR_p$ relative to the probability space over runs induced by the strategy $\sigma$.
When additionally the random variable $X$ (e.g., mean payoff) is clear from the context, we may write $\CVaR_p$ and $\CVaR_p^\sigma$ instead of $\CVaR_p(X)$ and $\CVaR^\sigma_p(X)$, respectively.
We also define analogous abbreviations for $\VaR$.

\section{Single dimension} \label{sec:single}

We show that all queries in one dimension are in P.
Furthermore, our LP-based decision procedures directly yield a description of a witness strategy and allow for optimization objectives.
We refer to the input constraints by $\mathsf{e}$ for expectation, $(\mathsf{p}, \mathsf{c})$ for CVaR, and $(\mathsf{q}, \mathsf{v})$ for VaR.
Further, we use $i$ for indices related to SCCs / MECs.

\subsection{Weighted reachability}

First, we show the simple result for Markov Chains, providing some insight in the techniques used in the MDP case.

\begin{theorem} \label{stm:mc_single_ptime}
	$\mathsf{MC}^{\{\Expectation, \CVaR, \VaR\}}_{\mathsf{r}, \mathsf{single}}$ is in P.
\end{theorem}
\begin{proof}
	Let $\mathsf{M}$ be a \emph{finite-state} Markov chain, $\mathbf{r}$ a reward function, and $T = \{b_1, \dots, b_n\}$ the target set.
	Recall that all $b_i$ are absorbing, hence single-state BSCCs.
	We obtain the stationary distribution $p$ of $\mathsf{M}$ in polynomial time by, e.g., solving a linear equation system~\cite{Puterman-book}.
	With $p$, we can directly compute the CDF of $R^\mathsf{r}$ as $F_{R^\mathsf{r}}(v) = \sum_{b_i : \mathbf{r}(b_i) \leq v} p(b_i)$ and immediately decide the query.

\end{proof}

Let us consider the more complex case of MDP.
We show a lower bound on the type of strategies necessary to realize $\mathbf{obj} = \mathsf{r}$ queries with constraints on expectation and one of VaR or CVaR.
We then continue to prove that this class of strategies is optimal.
This characterization is used to derive a polynomial time decision procedure based on a linear program (LP) which immediately yields a witness strategy.
Finally, when we deal with the mean payoff case in Sec.~\ref{sec:single:mean}, we make use of the reasoning presented in this section.

\paragraph{Randomization is necessary for weighted reachability.}
In the following example, we present a simple MDP on which all deterministic strategies fail to satisfy specific constraints, while a straightforward randomizing one succeeds in doing so.

\begin{figure}
	\begin{tikzpicture}[auto,initial text={},node distance=0.5cm]
		\node[initial above,state] (s0) {};
		\node[state,left=0.5cm of s0] (s1) {$5$};
		\node[actionnode,right=of s0] (s0b) {};
		\node[state,above right=0.2cm and 0.75cm of s0b] (s2) {$10$};
		\node[state,below right=0.2cm and 0.75cm of s0b] (s3) {$0$};

		\path[->]
			(s0) edge[directedge,swap]    node[action] {$a$} (s1)
			(s0) edge[actionedge]         node[action] {$b$} (s0b)
			(s0b) edge[probedge]          node[prob] {$0.9$} (s2)
			(s0b) edge[probedge,swap]     node[prob] {$0.1$} (s3)
			(s1) edge[directedge,loop left] (s1)
			(s2) edge[directedge,loop right] (s2)
			(s3) edge[directedge,loop right] (s3);
	\end{tikzpicture}
	\caption{MDP used to show various difficulties of $\CVaR$}
	\label{fig:mdp_cvar_hard}
\end{figure}

\begin{example} \label{ex:weighted_reachability_randomization}
	Consider the MDP outlined in Fig.~\ref{fig:mdp_cvar_hard}.
	The only non-determinism is given by the choice in the initial state $s_0$.
	Hence, any strategy is characterised by the choice in that particular state.
	Let now $\sigma_a$ and $\sigma_b$ denote the deterministic strategies playing $a$ and $b$ in $s_0$, respectively.
	Clearly, $\sigma_a$ achieves an expectation, $\CVaR_{0.05}^{\sigma_a}$, and $\VaR_{0.05}^{\sigma_a}$ of $5$.
	On the other hand, $\sigma_b$ obtains an expectation of $9$ with $\CVaR_{0.05}^{\sigma_b}$ and $\VaR_{0.05}^{\sigma_b}$ equal to $0$.

	Thus, neither strategy satisfies the constraints $\mathsf{q} = \mathsf{p} = 0.05$, $\mathsf{e} = 6$, and $\mathsf{c} = 2$ (or $\mathsf{v} = 5$).
	This is the case even when the strategy has arbitrary (deterministic) memory at its disposal, since in the first step there is nothing to remember.
	Yet, $\sigma = \frac{3}{4}\sigma_a + \frac{1}{4}\sigma_b$ achieves $\mathbb{E} = \frac{3}{4}5 + \frac{1}{4}9 = 6 \geq \mathsf{e}$, $\CVaR_\mathsf{p} = 2.5 \geq \mathsf{c}$, and $\VaR_\mathsf{q} = 5 \geq \mathsf{v}$. \QEE
\end{example}

Hence strategies satisfying an expectation constraint together with either a CVaR \emph{or} VaR constraint may necessarily involve randomization in general.
We prove that (i)~under mild assumptions randomization actually is sufficient, i.e. no memory is required, and (ii)~fixed memory may additionally be required in general.

\begin{definition} \label{def:attraction_assumption}
	Let $\mathcal{M}$ be an MDP with target set $T$ and reward function $\mathbf{r}$.
	We say that $\mathcal{M}$ satisfies the \emph{attraction assumption} if \textbf{A1})~the target set $T$ is reached almost surely for any strategy, or \textbf{A2})~for all target state $s \in T$ we have $\mathbf{r}(s) \geq 0$.
\end{definition}

Essentially, this definition implies that an optimal strategy never remains in a non-target MEC.
This allows us to design memoryless strategies for the weighted reachability problem.

\begin{theorem} \label{stm:mdp_exp_reach_strategies}
	Memoryless randomizing strategies are sufficient for $\mathsf{MDP}_{\mathsf{r}, \mathsf{single}}^{\{\Expectation, \VaR, \CVaR\}}$ under the attraction assumption.
\end{theorem}

\begin{proof}
	Fix an MDP $\mathcal{M}$ and reward function $\mathbf{r}$.
	We prove that for any strategy $\sigma$ there exists a memoryless, randomizing strategy $\sigma'$ achieving at least the expectation, VaR, and CVaR of $\sigma$.

	All target states $t_i \in T$ form single-state MECs, as we assumed that all target states are absorbing.
	Consequently, $\sigma$ naturally induces a distribution over these $s_i$.
	Now, we apply \cite[Theorem 3.2]{DBLP:journals/lmcs/EtessamiKVY08} to obtain a strategy $\sigma'$ with $\mathbb{P}^{\sigma'}[\diamondsuit s_i] \geq \mathbb{P}^\sigma[\diamondsuit s_i]$ for all $i$.

	With \textbf{A1}), we have $\sum p_i = 1$ and thus $\mathbb{P}^{\sigma'}[\diamondsuit t_i] = \mathbb{P}^\sigma[\diamondsuit t_i]$.
	Hence, $\sigma'$ obtains the same CDF for the weighted reachability objective.
	Under \textbf{A2}), the CDF $F'$ of strategy $\sigma'$ stochastically dominates the CDF $F$ of the original strategy $\sigma$, concluding the proof.
\end{proof}

\begin{theorem} \label{stm:mdp_exp_reach_strategies_general}
	Two-memory stochastic strategies (i.e.\ with both randomization and stochastic update) are sufficient for $\mathsf{MDP}_{\mathsf{r}, \mathsf{single}}^{\{\Expectation, \VaR, \CVaR\}}$.
\end{theorem}

The proof is a simple application of the following Thm.~\ref{stm:mdp_exp_mean_strategies}, as weighted reachability is a special case of mean payoff.
Together with an example for the lower bound it can be found in Sec~\ref{sec:app:cvar:weighted_reach}.

\begin{figure}
	\begin{enumerate}
		\renewcommand{\labelenumi}{(\arabic{enumi}) }
		\item \label{fig:reach_lp:non-neg}
		All variables $y_a$, $x_s$, $\underline{x}_s$ are non-negative.
		\item \label{fig:reach_lp:flow}
		Transient flow for $s \in S$:
		\begin{equation*}
			\mathbbm{1}_{s_0}(s) + {\sum}_{a \in \mathsf{A}} y_a \Delta(a, s) = {\sum}_{a \in \mathsf{Av}(s)} y_a + x_s
		\end{equation*}
		\item \label{fig:reach_lp:recurrent_switch}
		Switching to recurrent behaviour:
		\begin{equation*}
			{\sum}_{s \in T} x_s = 1
		\end{equation*}
		\item \label{fig:reach_lp:var_split}
		$\VaR$-consistent split:
		\begin{align*}
			\underline{x}_s & = x_s \text{ for $s \in T_<$} & \underline{x}_s & \leq x_s \text{ for $s \in T_=$}
		\end{align*}
		\item \label{fig:reach_lp:probability_split}
		Probability-consistent split:
		\begin{equation*}
			{\sum}_{s \in T_\leq} \underline{x}_s = \mathsf{p}
		\end{equation*}
		\item \label{fig:reach_lp:satisfaction}
		CVaR and expectation satisfaction:
		\begin{align*}
			{\sum}_{s \in T_\leq} \underline{x}_s \cdot \mathbf{r}(s) & \geq \mathsf{p} \cdot \mathsf{c} &
			{\sum}_{s \in T} x_s \cdot \mathbf{r}(s) & \geq \mathsf{e}
		\end{align*}
	\end{enumerate} %
	\caption{LP used to decide weighted reachability queries given a guess $t$ of $\VaR_\mathsf{p}$.
		$T_\sim := \{s \in T \mid \mathbf{r}(s) \sim t\}$, $\sim \in \{<, =, \leq\}$.} %
	\label{fig:reach_lp} %
\end{figure} %
Inspired by~\cite[Fig.~3]{DBLP:conf/lics/ChatterjeeKK15}, we use the optimality result from Thm.~\ref{stm:mdp_exp_reach_strategies} to derive a decision procedure for weighted reachability queries under the attraction assumptions based on the LP in Fig.~\ref{fig:reach_lp}.

To simplify the LP, we make further assumptions -- see Sec~\ref{sec:app:reach_lp_assumptions} for details.
First, all MECs, including non-target ones, consist of a single state.
Second, all MECs from which $T$ is not reachable are considered part of $T$ and have $\mathbf{r} = 0$ (similar to the \enquote{cleaned-up MDP} from \cite{DBLP:journals/lmcs/EtessamiKVY08}).
Finally, we assume that the quantile-probabilities are equal, i.e.\ $\mathsf{p} = \mathsf{q}$.
The LP can easily be extended to account for different values by duplicating the $\underline{x}_s$ variables and adding according constraints.

The central idea is to characterize randomizing strategies by the \enquote{flow} they achieve.
To this end, Equality~\eqref{fig:reach_lp:flow} essentially models Kirchhoff's law, i.e.\ inflow and outflow of a state have to be equal.
In particular, $y_a$ expresses the transient flow of the strategy as the expected total number of uses of action $a$.
Similarly, $x_s$ models the recurrent flow, which under our absorption assumption equals the probability of reaching $s$.
Equality~\eqref{fig:reach_lp:recurrent_switch} ensures that all transient behaviour eventually changes into recurrent one.

In order to deal with our query constraints, Constraints~\eqref{fig:reach_lp:var_split} and \eqref{fig:reach_lp:probability_split} extract the worst $\mathsf{p}$ fraction of the recurrent flow, ensuring that the $\VaR_\mathsf{p}$ is at least $t$.
Note that equality is not guaranteed by the LP; if $\underline{x}_s = x_s$ for all $s \in T_\leq$, we have $\VaR_\mathsf{p} > t$.
Finally, Inequality~\eqref{fig:reach_lp:satisfaction} enforces satisfaction of the constraints.

\begin{theorem} \label{stm:mdp_exp_reach_lp_correct}
	Let $\mathcal{M}$ be an MDP with target states $T$ and reward function $\mathbf{r}$, satisfying the attraction assumption.
	Fix the constraint probability $\mathsf{p} \in (0, 1)$ and thresholds $\mathsf{e}, \mathsf{c} \in \mathbb{Q}$.
	Then, we have that
	\begin{enumerate}
		\item
		for any strategy $\sigma$ satisfying the constraints, there is a $t \in \mathbf{r}(S)$ such that the LP in Fig.~\ref{fig:reach_lp} is feasible, and
		\item \label{stm:mdp_exp_reach_lp_correct:strategy}
		for any threshold $t \in \mathbf{r}(S)$, a solution of the LP in Fig.~\ref{fig:reach_lp} induces a memoryless, randomizing strategy $\sigma$ satisfying the constraints and $\VaR^\sigma_\mathsf{p} \geq t$.
	\end{enumerate}
\end{theorem}

\begin{proof}
	First, we prove for a strategy $\sigma$ satisfying the constraints that there exists a $t \in \mathbf{r}(S)$ such that the LP is feasible.
	By Thm.~\ref{stm:mdp_exp_reach_strategies}, we may assume that $\sigma$ is a memoryless randomizing strategy.
	From \cite[Theorem 3.2]{DBLP:journals/lmcs/EtessamiKVY08}, we get an assignment to the $y_a$'s and $x_s$'s satisfying Equalities~\eqref{fig:reach_lp:non-neg}, \eqref{fig:reach_lp:flow}, and~\eqref{fig:reach_lp:recurrent_switch} such that $\mathbb{P}^\sigma[\diamondsuit s] = x_s$ for all target states $s \in T$.
	Further, let $v = \VaR^\sigma_\mathsf{p}$ be the value-at-risk of the strategy.
	By definition of $\VaR$, we have that $\mathbb{P}^\sigma[X < v] \leq p$.

	Assume for now that $\mathbb{P}^\sigma[X < v] = p$, i.e. the probability of obtaining a value strictly smaller than $v$ is exactly $p$.
	In this case, choose $t$ to be the next smaller reward, i.e.\ $t = \max \{\mathbf{r}(s) < v\}$.
	We set $\underline{x}_s = x_s$ for all $s \in T_\leq$, satisfying Constraints~\eqref{fig:reach_lp:var_split} and \eqref{fig:reach_lp:probability_split}.

	Otherwise, we have $\mathbb{P}^\sigma[X < v] < p$.
	Now, some non-zero fraction of the probability mass at $v$ contributes to the $\CVaR$.
	Again, we set the values for $\underline{x}_s$ according to Constraint~\eqref{fig:reach_lp:var_split}.
	The only degree of freedom are the values of $\underline{x}_s$ where $\mathbf{r}(s) = t$.
	There, we assign the values so that $\sum_{s \in T_=} \underline{x}_s = p - \sum_{s \in T_<} \underline{x}_s$, satisfying Equality~\eqref{fig:reach_lp:probability_split}.

	It remains to check Inequality~\eqref{fig:reach_lp:satisfaction}.
	For expectation, we have $\sum_{s \in T} x_s \cdot \mathbf{r}(s) = \sum_{s \in T} \mathbb{P}^\sigma[\diamondsuit s] \cdot \mathbf{r}(s) = \mathbb{E}^\sigma[R^\mathsf{r}] \geq \mathsf{e}$.
	For CVaR, notice that, due to the already proven Constraints~\eqref{fig:reach_lp:var_split} and \eqref{fig:reach_lp:probability_split}, the side of Inequality~\eqref{fig:reach_lp:satisfaction} is equal to $\CVaR_\mathsf{p}^\sigma$ and thus at least $\mathsf{c}$.

	Second, we prove that a solution to the LP induces the desired strategy $\sigma$.
	Again by \cite[Theorem 3.2]{DBLP:journals/lmcs/EtessamiKVY08}, we get a memoryless randomizing strategy $\sigma$ such that $\mathbb{P}^\sigma[\diamondsuit s] = x_s$ for all states $s \in T$.
	Then $\mathbb{E}^\sigma[R^\mathsf{r}] = \sum_{s \in T} \mathbb{P}^\sigma[\diamondsuit s] \cdot \mathbf{r}(s) = \sum_{s \in T} x_s \cdot \mathbf{r}(s) \geq \mathsf{e}$.
	Further,
	\begin{equation*}
		\CVaR_p(R^\mathsf{r}) = \frac{1}{\mathsf{p}} \left( {\sum}_{s : \mathbf{r}(s) < v} x_s \cdot \mathbf{r}(s) + (\mathsf{p} - {\sum}_{s : \mathbf{r}(s) < v} x_s) \cdot v \right)
	\end{equation*}
	by definition.
	Now, we make a case distinction on $\underline{x}_s = x_s$ for all $s \in T_=$.
	If this is true, we have $v = \VaR_\mathsf{p}^\sigma = \min\{r \in \mathbf{r}(S) \mid r > t\}$, but $\mathbb{P}^\sigma[X < v] = p$.
	Consequently, $T_\leq = \{s \in T : \mathbf{r}(s) < v\}$ and ${\sum}_{s : \mathbf{r}(s) < v} x_s = p$.
	Otherwise, we have $v = t$ and consequently $T_< = \{s \mid \mathbf{r}(s) < v\}$.
	Inserting in the above equation immediately gives the result $\CVaR_p(R^\mathsf{r}) = \tfrac{1}{\mathsf{p}} {\sum}_{s \in T_\leq} \mathbf{r}(s) \cdot \underline{x}_s$.
\end{proof}

The linear program requires to know the $\VaR_p^\sigma$ beforehand, which in turn clearly depends on the chosen strategy.
Yet, there are only linearly many values the random variable $R^\mathsf{r}$ attains.
Thus we can simply try to find a solution for all potential values of $\VaR_p^\sigma$, i.e.\ $\{r \in \mathbf{r}(S)\}$, yielding a polynomial time solution.

\begin{corollary} \label{stm:mdp_exp_reach_ptime}
	$\mathsf{MDP}^{\{\Expectation, \VaR, \CVaR\}}_{\mathsf{r},\mathsf{single}}$ is in P.
\end{corollary}

\begin{proof}
	Under the attraction assumption, this follows directly from Thm.~\ref{stm:mdp_exp_reach_lp_correct}.
	In general, the reduction to mean payoff used by Thm.~\ref{stm:mdp_exp_reach_strategies_general} and the respective result from Cor.~\ref{stm:mdp_mean_ptime} show the result.

\end{proof}

\subsection{Mean payoff} \label{sec:single:mean}

In this section, we investigate the case of $\mathbf{obj} = \mathsf{m}$.
Again, the construction for MC is considerably simple, yet instructive for the following MDP case.
\begin{theorem}
	$\mathsf{MC}^{\{\Expectation, \VaR, \CVaR\}}_{\mathsf{m},\mathsf{single}}$ is in P.
\end{theorem}
\begin{proof}[Proof sketch]
	For each BSCC $B_i$, we obtain its expected mean payoff $r_i = \mathbb{E}[R^\mathsf{m} \mid B_i]$ through, e.g., a linear equation system~\cite{Puterman-book}.
	Almost all runs in $B_i$ achieve this mean payoff and thus the corresponding random variable is discrete.
	We reduce the problem to weighted reachability by using the known reformulation
	%
	\begin{equation*}
		\mathbb{P}[R^\mathsf{m} = c] = {\sum}_{B_i : r_i = c} P[\diamondsuit B_i].
	\end{equation*}

	We replace each of these BSCCs by a representative $b_i$ to obtain $\mathsf{M}'$.
	Define the set of target states $T = \{b_i\}$ and the reachability reward function $\mathbf{r}'(b_i) = r_i$.
	By applying the approach of Thm.~\ref{stm:mc_single_ptime}, we obtain the expectation, $\VaR$, and $\CVaR$ for reachability in $\mathsf{M}'$ which by construction coincides with the respective values for mean payoff in $\mathsf{M}$.
\end{proof}

For the MDP case, recall that simple expectation maximization of mean payoff can be reduced to weighted reachability~\cite{DBLP:conf/cav/AshokCDKM17} and deterministic, memoryless strategies are optimal~\cite{Puterman-book}.
Yet, solving a conjunctive query involving either VaR or CVaR needs more powerful strategies than in the weighted reachability case of Thm.~\ref{stm:mdp_exp_reach_strategies}.
Nevertheless, we show how to decide these queries in P.

\paragraph{Randomization and memory is necessary for mean payoff.}
A simple modification of the MDP in Fig.~\ref{fig:mdp_cvar_hard} yields an MDP where both randomization and memory is required to satisfy the constraints of the following example.

\begin{figure}
	\begin{tikzpicture}[auto,initial text={},node distance=0.5cm]
		\node[initial above,state] (s0) {$5$};
		\node[actionnode,right=of s0] (s0b) {};
		\node[state,above right=0.2cm and 0.75cm of s0b] (s2) {$10$};
		\node[state,below right=0.2cm and 0.75cm of s0b] (s3) {$0$};

		\path[->]
			(s0) edge[directedge,loop left] node[action] {$a$} (s0)
			(s0) edge[actionedge]         node[action] {$b$} (s0b)
			(s0b) edge[probedge]          node[prob] {$0.9$} (s2)
			(s0b) edge[probedge,swap]     node[prob] {$0.1$} (s3)
			(s2) edge[directedge,loop right] (s2)
			(s3) edge[directedge,loop right] (s3);
	\end{tikzpicture}
	\caption{Memory is necessary for mean payoff queries}
	\label{fig:mean_payoff_memory}
\end{figure} %

\begin{example} \label{ex:mdp_exp_reach_memory}
	Consider the MDP presented in Fig.~\ref{fig:mean_payoff_memory}.
	There, the same constraints as before, i.e.\ $\mathsf{q} = \mathsf{p} = 0.05$, $\mathsf{e} = 6$, and $\mathsf{c} = 2$ (or $\mathsf{v} = 5$), can only be satisfied by strategies with both memory and randomization.
	Clearly, a pure strategy can only satisfy either of the two constraints again.
	But now a memoryless randomizing strategy also is insufficient, too, since any non-zero probability on action $b$ leads to almost all runs ending up on the right side of the MDP, hence yielding a $\CVaR_\mathsf{p}$ and $\VaR_\mathsf{q}$ of $0$.
	Instead, a stochastic strategy with $\mathsf{M} = \{a, b\}$ can simply choose $\alpha = \{a \mapsto \frac{3}{4}, b \mapsto \frac{1}{4}\}$ and play the corresponding action indefinitely, satisfying the constraints. \QEE
\end{example}

We prove that this bound actually is tight, i.e.\ that, given stochastic memory update, two memory elements
are sufficient.

\begin{theorem} \label{stm:mdp_exp_mean_strategies}
	Two-memory stochastic strategies (i.e.\ with both randomization and stochastic update) are sufficient for $\mathsf{MDP}_{\mathsf{m},\mathsf{single}}^{\{\Expectation, \VaR, \CVaR\}}$.
\end{theorem}

\begin{proof}

	Let $\sigma$ be a strategy on an MDP $\mathcal{M}$ with reward function $\mathbf{r}$.
	We construct a two-memory stochastic strategy $\sigma'$ achieving at least the expectation, VaR, and CVaR of $\sigma$.

	First, we obtain a memoryless deterministic strategy $\sigma_\text{opt}$ which obtains the maximal possible mean payoff in each MEC~\cite{Puterman-book}.
	We then apply the construction of \cite[Proposition 4.2]{DBLP:journals/corr/abs-1104-3489} (see also \cite[Lemma 5.7]{DBLP:conf/lics/ChatterjeeKK15}), where the $\xi$ is our $\sigma_\text{opt}$.
	(Technically, this can be ensured by choosing the constraints of the LP $L$ according to $\sigma_\text{opt}$.)

	Intuitively, this constructs a two-memory strategy $\sigma'$ on $\mathcal{M}$ behaving as follows.
	Initially, $\sigma'$ remains in each MEC with the same probability as $\sigma$, i.e. $\mathbb{P}^{\sigma'}[\diamondsuit \Box M_i] = \mathbb{P}^{\sigma}[\diamondsuit \Box M_i]$ by following a memoryless \enquote{searching} strategy and stochastically switching its memory state to \enquote{remain}.
	Once in the \enquote{remain} state, the behaviour of the optimal strategy $\sigma_\text{opt}$ is implemented.

	Clearly, (i)~both strategies remain in a particular MEC with the same probability, and (ii)~$\sigma'$ obtains as least as much value in each MEC as $\sigma$.
	Hence the CDF induced by $\sigma'$ stochastically dominates the one of $\sigma$, concluding the proof.
\end{proof}

This immediately gives us a polynomial time decision procedure.

\begin{corollary} \label{stm:mdp_mean_ptime}
	$\mathsf{MDP}^{\{\Expectation, \VaR, \CVaR\}}_{\mathsf{m}, \mathsf{single}}$ is in P.
\end{corollary}

Furthermore, we can use results of \cite[Lemma 16]{DBLP:conf/lics/ChatterjeeKK15} to trade the stochastic update for more memory.

\begin{corollary}
	Stochastic strategies with finite, deterministic memory are sufficient for $\mathsf{MDP}_{\mathsf{m},\mathsf{single}}^{\{\Expectation, \VaR, \CVaR\}}$.
\end{corollary}

\paragraph{Deterministic strategies may require exponential memory.}
As sources of randomness are not always available, one might ask what can be hoped for when only determinism is allowed.
As already shown in Ex.~\ref{ex:weighted_reachability_randomization}, randomization is required in general.
But even if some deterministic strategy is sufficient, it may require memory exponential in the size of the input, even in an MDP with only 3 states.
We show this in the following example.

\begin{figure}
	\begin{tikzpicture}[auto,initial text={},node distance=0.5cm]
		\node[initial above,state] (s0) {$5$};
		\node[actionnode,right=1cm of s0] (s0b) {};
		\node[state,above right=0.2cm and 1cm of s0b] (s2) {$10$};
		\node[state,below right=0.2cm and 1cm of s0b] (s3) {$0$};

		\path[->]
			(s0) edge[directedge,loop left] node[action] {$a$} (s0)
			(s0) edge[actionedge]         node[action] {$b$} (s0b)
			(s0b) edge[probedge]          node[prob] {$0.9 \varepsilon$} (s2)
			(s0b) edge[probedge,swap]     node[prob] {$0.1 \varepsilon$} (s3)
			(s0b) edge[probedge,bend left] node[prob,pos=.6] {$1-\varepsilon$} (s0)
			(s2) edge[directedge,loop right] (s2)
			(s3) edge[directedge,loop right] (s3);
	\end{tikzpicture}
	\caption{Exponential memory is necessary for mean payoff when only deterministic update is allowed.}
	\label{fig:mean_payoff_deterministic_memory}
\end{figure}

\begin{example}
	Consider the MDP outlined in Fig.~\ref{fig:mean_payoff_deterministic_memory} together with the constraints $\mathsf{q} = \mathsf{p} = 0.05$, $\mathsf{e} = 6$, and $\mathsf{c} = 2$ (or $\mathsf{v} = 5$).
	Again, any optimal strategy needs a significant part of runs to go to the right side in order to satisfy the expectation constraint.
	Yet, any strategy can only \enquote{move} a small fraction of the runs there in each step.
	In particular, after $k$ steps, the right side is only reached with probability at most $1 - (1 - \varepsilon)^k$.
	When choosing $\varepsilon = 2^{-n}$, which needs $\Theta(n)$ bits to encode, a deterministic strategy requires $k \geq c / \log(1-2^{-n}) \in O(2^n)$ memory elements to count the number of steps.
	The same holds true for any deterministic-update strategy.

	On the other hand, a strategy with stochastic memory update can encode this counting by switching its state with a small probability after each step.
	For example, a strategy switching with probability $p = 3 \varepsilon$ from \enquote{play $b$} to \enquote{play $a$} satisfies the constraint. \QEE
\end{example}

\subsection{Single constraint queries}

In this section, we discuss an important sub-case of the single-dimensional case, namely queries with only a single constraint, i.e. $\cardinality{\mathbf{crit}} = 1$.
We show that deterministic memoryless strategies are sufficient in this case.

One might be tempted to use standard arguments and directly conclude this from the results of Thm.~\ref{stm:mdp_exp_reach_strategies} as follows.
Recall that this theorem shows that memoryless, randomizing strategies are sufficient; and that any such strategy can be written as finite convex combination of memoryless, deterministic strategies.
Most constraints, for example expectation or reachability, behave linearly under convex combination of strategies, e.g., $\mathbb{E}^{\sigma_\lambda}(X) = \lambda \mathbb{E}^{\sigma_1}[X] + (1-\lambda) \mathbb{E}^{\sigma_2}[X]$.
Consequently, for an optimal memoryless strategy, there is a deterministic witness, which in turn also is optimal.

Surprisingly, this assumption is not true for $\CVaR$.
On the contrary, the $\CVaR$ of a convex combination of strategies might be strictly worse than the $\CVaR$s of either strategy, as shown in the following example.
We prove a slightly weaker property of $\CVaR$ which eventually allows us to apply similar reasoning.

\begin{example} \label{ex:mdp_cvar_hard}

	Recall the MDP in Fig.~\ref{fig:mdp_cvar_hard} and let $p = 0.05$.
	As previously shown, $\CVaR_p^{\sigma_a} = 5$ and $\CVaR_p^{\sigma_b} = 0$, but the mixed strategy $\sigma_\lambda = \frac{1}{2}\sigma_a + \frac{1}{2}\sigma_b$ achieves $\CVaR_p^{\sigma_\lambda} = 0$ instead of the convex combination $\frac{1}{2}5 + \frac{1}{2}0 = 2.5$.

	For $p = 0.2$, we have $\CVaR_p^{\sigma_a} = \CVaR_p^{\sigma_b} = 5$.
	Yet, \emph{any} non-trivial convex combination of the two strategies yields a $\CVaR_p$ less than $5$.
	See Sec.~\ref{sec:app:cvar:nonlinear} for more details.
	With according constraints, this effectively can force an optimal strategy to choose between $a$ or $b$.
	This observation is further exploited in the NP-hardness proof of the multi-dimensional case in Sec.~\ref{sec:multi}.
	\qee
\end{example}

Since CVaR considers the worst events, the CVaR of a combination intuitively cannot be better than the combination of the respective CVaRs.
We prove this intuition in the general setting, where instead of a convex combination of strategies we consider a mixture of two random variables.

\begin{lemma} \label{stm:cvar_quasiconvex}
	$\CVaR_p(X)$ is convex in $X$ for fixed $p \in (0, 1)$, i.e.\ for random variables $X_1, X_2$ and $\lambda \in [0, 1]$
	\begin{equation*}
		\CVaR_p(\lambda X_1 + (1-\lambda) X_2) \leq \lambda \CVaR_p(X_1) + (1-\lambda) \CVaR_p(X_2).
	\end{equation*}
\end{lemma}

The proof can be found in Sec.~\ref{sec:app:quasiconvex}.
This result allows us to apply the ideas outlined in the beginning of the section.

\begin{theorem}
	For any $\mathbf{obj}\in\{\mathsf{r},\mathsf{m}\}$, deterministic memoryless strategies are sufficient for $\mathsf{MDP}^{\mathbf{crit}}_{\mathbf{obj}, \mathsf{single}}$ when $\cardinality{\mathbf{crit}} = 1$.
\end{theorem}

\begin{proof}
	This is known for $\mathbf{crit} = \{\Expectation\}$~\cite{Puterman-book} and $\mathbf{crit} = \{\VaR\}$~\cite{CIS-125853}.

	For CVaR, observe that the convex combination of deterministic strategies cannot achieve a better CVaR than the best strategy involved in the combination (see Lem.~\ref{stm:cvar_quasiconvex}).
	This immediately yields the result for $\mathbf{obj} = \mathsf{r}$ through Thm.~\ref{stm:mdp_exp_reach_strategies}.
	For $\mathbf{obj} = \mathsf{m}$, we exploit the approach of Thm.~\ref{stm:mdp_exp_mean_strategies}.
	Recall that there we obtained a two-memory strategy $\sigma'$.
	Both randomization and stochastic update are used solely to distribute the runs over all MECs accordingly.
	By the above reasoning, for each MEC it is sufficient to either almost surely remain there or leave it.
	This behaviour can be implemented by a deterministic memoryless strategy on the original MDP.
\end{proof}

redpajama_set_name: RedPajamaArXiv