Now suppose $\gamma = 0$, so we have $\SM^\top \vect{y} = 0$. Suppose $\vect{y} = 0$, then we get $\TM^\top \vect{y} = 0 \geq \vect{1} \cdot \varepsilon > 0$. Hence $\vect{y} = 0$ cannot hold. Suppose $\vect{y} \neq 0$. The following observation is from the proof of Lemma 3.8 in <cit.>. Since we have $\SM^\top \vect{y} = 0$, we also have $\vect{1}^\top\SM^\top \vect{y} = 0$. Observe that $\vect{1}^\top \SM^\top$ corresponds to $1 - \sum_{\state' \in \states} \transMat(\state, \action, \state')$ for every $(\state, \action) \in \SA$. From $\vect{1}^\top\SM^\top \vect{y} = 0$ we have for all $\vect{y}(\state, \action) > 0$ that $\sum_{\state' \in \states} \transMat(\state, \action, \state') = 1$ and $\transMat(\state, \action, \targets) = 0$. This implies $\TM^\top \vect{y} = 0$, again yielding a contradiction and $\gamma \neq 0$ has to hold. Thus we have:

\begin{align*}
&\phantom{\iff} \neg \exists \varepsilon \in \reals_{>0} \centerdot \exists \vect{y} \in \realsnn^{\SA} \centerdot \SM^\top \vect{y} = \initDistr \land \TM^\top \vect{y} \geq \pmb{\lambda} + \vect{1} \cdot \varepsilon \\
& \iff \neg \exists \gamma \in \realsnn \centerdot \exists \varepsilon \in \reals_{>0} \centerdot \exists \vect{y} \in \realsnn^{\SA} \centerdot \SM^\top \vect{y} = \initDistr \cdot \gamma \land \TM^\top \vect{y} \geq \pmb{\lambda} \cdot \gamma + \vect{1} \cdot \varepsilon \\
& \iff \neg \exists \gamma, \varepsilon \in \realsnn \centerdot \exists \vect{y} \in \realsnn^{\SA} \centerdot \begin{pmatrix} \SM^\top & -\initDistr & \vect{0} \\ -\SM^\top & \initDistr & \vect{0} \\ \TM^\top & -\pmb{\lambda} & -\vect{1} \end{pmatrix}
\begin{pmatrix}
\vect{y} \\
\gamma \\
\varepsilon
\end{pmatrix}
\geq 0 \ \land -\varepsilon < 0 \\
\overset{\text{\Cref{lemma:farkas} \ref{lemma:farkas-1}}}&{\iff}
\exists \vect{x}_1, \vect{x}_2 \in \realsnn^{\states} \centerdot \exists \vect{z} \in \realsnn^{[k]} \centerdot \begin{pmatrix} \SM & -\SM & \TM \\ -\initDistr^\top & \initDistr^\top & -\pmb{\lambda}^\top \\ \vect{0}^\top & \vect{0}^\top & -\vect{1}^\top \end{pmatrix} \begin{pmatrix}
\vect{x}_1 \\
\vect{x}_2 \\
\vect{z}
\end{pmatrix} \leq \begin{pmatrix}
\vect{0} \\
0 \\
\end{pmatrix}\\
& \iff \exists \vect{x} \in \reals^{\states} \centerdot \exists \vect{z} \in \realsnn^{[k]} \centerdot \SM \vect{x} \leq - \TM \vect{z} \land - \initDistr^\top \vect{x} \leq \pmb{\lambda}^\top \vect{z} \land \vect{1}^\top\vect{z} \geq 1\\
& \iff \exists \vect{x} \in \reals^{\states} \centerdot \exists \vect{z} \in \realsnn^{[k]} \centerdot \SM \vect{x} \geq \TM \vect{z} \land \initDistr^\top \vect{x} \leq \pmb{\lambda}^\top \vect{z} \land \vect{1}^\top\vect{z} \geq 1
\end{align*}

We claim that $\SM \vect{x} \geq \TM \vect{z} \land \initDistr^\top \vect{x} \leq \pmb{\lambda}^\top \vect{z} \land \vect{1}^\top\vect{z} \geq 1$ has a solution if and only if $\SM \vect{x} \geq \TM \vect{z} \land \initDistr^\top \vect{x} \leq \pmb{\lambda}^\top \vect{z} \land \vect{z} \neq 0$ does. Firstly, the solution to the former is a solution to the latter, since $\vect{1}^\top\vect{z} \geq 1$ implies $\vect{z} \neq 0$. Now let $\vect{x}$ and $\vect{z}$ be a solution of the latter. Since $\vect{z} \neq 0$ and $\vect{z} \geq 0$ there exists $\beta \in \realsnn$ such that $\beta \cdot \vect{1}^\top \vect{z} \geq 1$. Let $\vect{x}' = \vect{x} \cdot \beta$ and $\vect{z}' = \vect{z} \cdot \beta$. Then we get $\SM \vect{x}' = \SM \vect{x} \cdot \beta \geq \TM \vect{z} \cdot \beta = \TM \vect{z}'$ and $\initDistr^\top \vect{x}' = \initDistr^\top \vect{x} \cdot \beta \leq \pmb{\lambda}^\top \vect{z} \cdot \beta = \pmb{\lambda}^\top \vect{z}'$ and by construction $\vect{1}^\top \vect{z} \geq 1$. Hence $\vect{x}'$ and $\vect{z}'$ are a solution to the former system. Altogether this shows the equivalence. Since $\initDistr^\top \vect{x} = \vect{x}(\init)$, this completes the proof.

Again, for lower bounds we assume $\mdp$ to be EC-free. Then the proof is analogous and we apply <Ref> <ref> instead of <Ref> <ref>.

Directly follows from <Ref> and <Ref>.

Let us now briefly show how the certificates for -queries and -queries can be derived. To this end, let $\vect{t}_i$ denote the $i$th column of $\vect{T}$ and $\compBowtie \ = \ \leq$ if $\bowtie \ \in \{\geq, > \}$ and $\compBowtie \ = \ \geq$ if $\bowtie \ \in \{\leq, <\}$.

Let $\mdp = \mdpRF$ be an MDP in reachability form without ECs and let $\targetSet_1, \dots, \targetSet_k$ be target sets. Let $\lambda_i \in [0, 1]$ for all $i \in [k]$ and $\bowtie \ \in \{<, \leq, >, \geq\}$. Then we have:

\[
\exists \scheduler \in \schedulers \centerdot \Disj_{i=1}^{k} \prob_{\mdp}^\scheduler(\eventually  \targetSet_i ) \bowtie \lambda_i
\iff \exists \vect{y} \in \reals^\states \centerdot \Disj_{i=1}^{k} \SM^\top \vect{y} \compBowtie \initDistr \land \vect{t}_i^\top \vect{y} \bowtie \lambda_i
\]

Observe that we have:

\begin{align*}
\exists \scheduler \in \schedulers \centerdot \Disj_{i=1}^{k} \prob_{\mdp}^\scheduler(\eventually \targetSet_i ) \bowtie \lambda_i \iff \Disj_{i=1}^{k} \exists \scheduler \in \schedulers \centerdot \prob_{\mdp, \init}^\scheduler(\eventually \targetSet_i ) \bowtie \lambda_i
\end{align*}

We can then directly apply the results from the single-objective case <cit.> to each disjunct, thereby yielding the statement.

Let $\mdp = \mdpRF$ be an MDP in reachability form without ECs and let $\targetSet_1, \dots, \targetSet_k$ be target sets. Let $\lambda_i \in [0, 1]$ for all $i \in [k]$ and $\bowtie \ \in \{<, \leq, >, \geq\}$. Then we have:

\[
\forall \scheduler \in \schedulers \centerdot \Conj_{i=1}^{k} \prob_{\mdp}^\scheduler(\eventually  \targetSet_i ) \bowtie \lambda_i \iff
\exists \vect{x}_1, \dots, \vect{x}_k \in \reals^\states \centerdot \Conj_{i=1}^{k} \SM \vect{x} \compBowtie \vect{t}_i \land \initDistr^\top \vect{x} \bowtie \lambda_i
\]

\begin{align*}
\forall \scheduler \in \schedulers \centerdot \Conj_{i=1}^{k} \prob_{\mdp}^\scheduler(\eventually \targetSet_i) \bowtie \lambda_i &\iff \Conj_{i=1}^{k} \forall \scheduler \in \schedulers \centerdot \prob_{\mdp, \init}^\scheduler(\eventually \targetSet_i ) \bowtie \lambda_i
\end{align*}

We then obtain certificate conditions for each conjunct by using results from the single-objective case <cit.>, yielding the statement.

2c|     Certificate     Condition

2*$\exists$     $\land$     $\vect{y} \in \realsnn^\SA$     $\SM^\top \vect{y} \compBowtie \initDistr, \TM^\top \vect{y} \bowtie \pmb{\lambda}$     <cit.>

$\lor$      $\vect{y} \in \realsnn^\SA$
$\Disj_{i=1}^k \SM^\top \vect{y} \compBowtie \initDistr \land \vect{t}_i^\top \vect{y} \bowtie \lambda_i$     <cit.>

2*$\forall$     $\land$     $\vect{x}_1, \dots, \vect{x}_k \in \reals^\states$     $\Conj_{i=1}^k \SM \vect{x} \compBowtie \vect{t}_i \land \initDistr^\top \vect{x} \bowtie \lambda_i$     <cit.>

$\lor$      $\vect{x} \in \reals^\states, \ \begin{aligned}\vect{z} \in \begin{cases}
\realsnn^{[k]} \setminus \{\vect{0}\}, & \text{if } \bowtie \ \in \{\leq, \geq\}\\
\realsnn^{[k]}, & \text{else} \\
\end{cases} \\
\end{aligned}$    $\SM \vect{x} \compBowtie \TM \vect{z} \land \vect{x}(\init) \bowtie \pmb{\lambda}^\top \vect{z}$     <Ref>

Farkas certificates and conditions for EC-free MDPs. $\compBowtie =\ \leq$ if $\bowtie \ \in \{\geq, >\}$ and $\compBowtie =\ \geq$ otherwise.

An overview of the certificates and their conditions for EC-free MDPs in reachability form is shown in <Ref>.

§.§.§ Farkas certificates and witnessing subsystems
In this section we provide proofs for <Ref> and <Ref>.

Let $\mathcal{N} = (\states, \actions, \init, \transMat)$ be an MDP. Let $\targets_1, \dots, \targets_k \subseteq \states$ and $\targetSet_1, \dots,\allowbreak \targetSet_\ell \subseteq \states$. Further, let $\vect{r}_1, \dots, \vect{r}_p \in \rationals^\SA$ be reward vectors. Let $\mathcal{N}' = (\states' \union \{\exit\}, \actions, \init, \transMat')$ be a subsystem of $\mathcal{N}$.

* For every scheduler in $\scheduler \in \schedulers^\mathcal{N}$ there exists a scheduler $\scheduler' \in \schedulers^{\mathcal{N}'}$ such that for all $i \in [k]$ we have $\prob_{\mathcal{N}'}^{\scheduler'}(\eventually \targets_i) \leq \prob_{\mathcal{N}}^\scheduler(\eventually \targets_i)$, for all $j \in [\ell]$ we have $\prob_{\mathcal{N}'}^{\scheduler'}(\globally \targetSet_j) \leq \prob_{\mathcal{N}}^\scheduler(\globally \targetSet_j)$ and for all $h \in [p]$ we have $\expectation[\mathcal{N}']{\scheduler'}{\lrInf{\vect{r'}_h}} \leq \expectation[\mathcal{N}]{\scheduler}{\lrInf{\vect{r}_h}}$ ($\expectation[\mathcal{N}']{\scheduler'}{\lrSup{\vect{r'}_h}} \leq \expectation[\mathcal{N}]{\scheduler}{\lrSup{\vect{r}_h}}$)

* Vice versa, for every scheduler $\scheduler' \in \schedulers^{\mathcal{N}'}$ there exists a scheduler in $\scheduler \in \schedulers^\mathcal{N}$ such that for all $i \in [k]$ we have $\prob_{\mathcal{N}'}^{\scheduler'}(\eventually \targetSet_i) \leq \prob_{\mathcal{N}}^\scheduler(\eventually \targetSet_i)$, for all $j \in [\ell]$ we have $\prob_{\mathcal{N}'}^{\scheduler'}(\globally \targetSet_j) \leq \prob_{\mathcal{N}}^\scheduler(\globally \targetSet_j)$ and for all $h \in [p]$ we have $\expectation[\mathcal{N}']{\scheduler'}{\lrInf{\vect{r'}_h}} \leq \expectation[\mathcal{N}]{\scheduler}{\lrInf{\vect{r}_h}}$ ($ \expectation[\mathcal{N}']{\scheduler'}{\lrSup{\vect{r'}_h}} \leq \expectation[\mathcal{N}]{\scheduler}{\lrSup{\vect{r}_h}}$)

The proof follows the ideas from <cit.>. The set of paths in $\mathcal{N}'$ never visiting $\exit$ are a subset of paths in $\mathcal{N}$, i.e.

\[
\{\Path' \in \paths(\mathcal{N}') \mid \Path' \text{ never visits } \exit \} \subseteq \paths(\mathcal{N})
\]

Further, for all paths $\Path_\exit \in \{\Path' \in \paths(\mathcal{N}') \mid \Path' \text{ visits } \exit \}$, i.e. paths in $\mathcal{N}'$ that visit $\exit$ (and hence stay in $\exit$ forever, as $\exit$ cannot be left), and $\Path \in \paths(\mathcal{N})$ we have $\lrInf{\vect{r}_h'}(\Path_\exit) \leq \lrInf{\vect{r}_h}(\Path)$ ($\lrSup{\vect{r}_h'}(\Path_\exit) \leq \lrSup{\vect{r}_h}(\Path)$) for all $h \in [p]$. Intuitively, by construction of $\vect{r}_h'$, the smallest possible reward is collected in $\exit$ and a path in $\mathcal{N}'$ visiting $\exit$ cannot achieve a higher mean-payoff than any path in $\mathcal{N}$.

Let us prove <ref> first. Given a scheduler $\scheduler \in \schedulers^\mathcal{N}$, we choose a scheduler $\scheduler' \in \schedulers^{\mathcal{N}'}$ that behaves like $\scheduler$ in $\states'$ (in $\exit$ the choice does not matter). Recall that the set of actions that are enabled in a state $\state$ in $\mathcal{N}$ and $\mathcal{N}'$ coincide by definition and that once $\exit$ is entered in the subsystem the smallest possible reward is collected. Because the paths in $\mathcal{N}$ under $\scheduler$ and $\mathcal{N}'$ under $\scheduler'$ carry the same probability and the state-action pairs in $\states'$ have the same reward, the statement follows with the observations above.

For <ref>, let  $\scheduler' \in \schedulers^{\mathcal{N}'}$ be given. We choose a scheduler $\scheduler$ that behaves like $\scheduler'$ for paths $\Path \in \pathsFin(\mathcal{N})$ that only visit $\states'$. Otherwise, $\scheduler$ is allowed to play any available action. Similarly, the statement then follows.

For <ref>, we can directly apply <Ref> <ref>. For <ref> we prove via contraposition, i.e. we show:

\[
\exists \scheduler \in \schedulers^\mdp \centerdot \propAlt{\lesssim}{\scheduler}(\boldLambda) \implies \exists \scheduler' \in \schedulers^{\mdp'} \centerdot \propAlt{\lesssim}{\scheduler'}(\boldLambda)
\]

where $\propAlt{\lesssim}{\scheduler}(\boldLambda)$ is a corresponding conjunctive query if $\prop{\gtrsim}{\scheduler}(\boldLambda)$ is a disjunctive query and $\propAlt{\lesssim}{\scheduler}(\boldLambda)$ is a corresponding disjunctive query if $\prop{\gtrsim}{\scheduler}(\boldLambda)$ is a conjunctive query. Further, we choose $\lesssim \ = \ <$ if $\gtrsim \ = \ \geq$ and $\lesssim \ = \ \leq$ if $\gtrsim \ = \ >$. The statement then follows from <Ref> <ref>.

Let $\SM' = \SM\vert_{\SA'\times\states'} =  \SM_{\mdp_{\states'}}$ and $\TM' = \TM\vert_{\SA'\times [k]} = \TM_{\mdp_{\states'}}$ where $\SA' = \{(\state, \action) \in \SA \mid \state \in \states'\} = \SA_{\mdp_{\states'}}$. Let us prove <ref> first. We first note that if there exists $(\vect{x}', \vect{z}') \in \dqPoly{\mdp}{\gtrsim}(\pmb{\lambda})$, then there also exist $(\vect{x}, \vect{z}) \in \dqPoly{\mdp}{\gtrsim}(\pmb{\lambda})$ with $\vect{x} \geq 0$, namely $\vect{x}(\state) = \max\{0, \vect{x}'(\state)\}$ for all $\state \in \states$ and $\vect{z} = \vect{z}'$.

$\Rightarrow$: Let $(\vect{x}, \vect{z}) \in \dqPoly{\mdp}{\gtrsim}(\pmb{\lambda})$ with $\vect{x} \geq 0$. Then we have $\SM \vect{x} \leq \TM \vect{z} \land \vect{x}(\init) \gtrsim \pmb{\lambda}^\top \vect{z}$ (and additionally $\vect{z} \neq 0$ if we have non-strict inequalities). Let $\vect{x}' = \vect{x} \vert_{\states'}$ (i.e. $\vect{x}$ restricted to $\states'$). From Lemma 4.22 in <cit.> we know that $\SM' \vect{x}' \leq \TM' \vect{z}$ and $\vect{x}'(\init) \gtrsim \pmb{\lambda}^\top \vect{z}$ hold. Intuitively, by omitting columns in $\SA$ (that is columns corresponding to states in $\states\setminus\states'$ and which are thus not in the support of $\vect{x}$) where the corresponding value of $\vect{x}$ is zero does not change the value of the left-hand side. Additionally, omitting rows on both sides also preserves the satisfaction of the inequalities. Consequently, $\vect{x}'$ and $\vect{z}$ are Farkas certificates for the satisfaction of the query in $\mdp_{\states'}$. Using <Ref> we can conclude $\forall \scheduler \in \schedulers \centerdot \Disj_{i=1}^{k} \prob_{\mdp_{\states'}, \init}^\scheduler(\eventually  \targetSet_i ) \gtrsim \lambda_i$.

$\Leftarrow$: Because $\forall \scheduler \in \schedulers \centerdot \Disj_{i=1}^{k} \prob_{\mdp_{\states'}, \init}^\scheduler(\eventually \targetSet_i) \gtrsim \lambda_i$ holds, we know by <Ref> that there exists $\vect{x}' \in \realsnn^{\states'}$ and $\vect{z} \in \realsnn^{[k]}$ such that $(\vect{x'}, \vect{z}) \in \dqPoly{\mdp_{\states'}}{\gtrsim}(\pmb{\lambda})$, i.e. $\SM' \vect{x}' \leq \TM' \vect{z}$,  $\vect{x}'(\init) \gtrsim \pmb{\lambda}^\top \vect{z}$ and $\vect{1}^\top \vect{z} \leq 1$ (or $\vect{1}^\top \vect{z} = 1$ if we have non-strict inequalities). Let $\vect{x} \in \realsnn^\states$ with $\vect{x}(\state) = \vect{x}'(\state)$ if $\state \in \states'$ and $\vect{x}(\state) = 0$ otherwise. Clearly, we have $\supp{\vect{x}} \subseteq \states'$. Again, applying Lemma 4.22 from <cit.> we know that  $\SM \vect{x} \leq \TM \vect{z}$ and  $\vect{x}(\init) \geq \pmb{\lambda}^\top \vect{z}$ hold. Intuitively, adding columns corresponding to states where $\vect{x}$ is zero does not change the left-hand side of the inequalities. Rows corresponding to $(\state, \action) \in \SA$ with $\state \in \states\setminus\states'$ are of the form $- \sum_{\state' \in \states} \transMat(\state, \action, \state') \cdot \vect{x}(\state') \leq \sum_{i=1}^k \sum_{\target \in \targetSet_i} \transMat(\state, \action, \target) \cdot \vect{z}(\targetSet_i)$ because $\vect{x}(\state) = 0$. Since $\vect{x} \geq 0$ and the right-hand side is non-negative, such rows are also satisfied. Thus we have $(\vect{x}, \vect{z}) \in \dqPoly{\mdp}{\gtrsim}(\pmb{\lambda})$.

The proof for <ref> is analogous.

$\Rightarrow$: Let $\vect{y} \in \cqPoly{\mdp}{\gtrsim}(\boldLambda)$ with $\states' = \stateSupp{\vect{y}}$. For such $\vect{y}$ we have $\SM^\top\vect{y} \leq \initDistr \land \TM^\top \vect{y} \gtrsim \boldLambda$. Now we consider the restriction of $\vect{y}$ to the state action pairs in $\SA'$, i.e. $\vect{y}' = \vect{y} \vert_{\SA'}$. Again, following the reasoning of Lemma 4.22 from <cit.> we have that omitting columns of $\SM^\top$ where $\vect{y}$ is zero does not change the value. Similarly, omitting rows preserves the satisfaction of the inequality. Because $\TM^\top \vect{y} = (\TM')^\top \vect{y'}$, we then have $(\SM')^\top\vect{y}' \leq \initDistr \land (\TM')^\top \vect{y}' \gtrsim \boldLambda$. Applying <Ref> then concludes the proof.

$\Leftarrow$: Now suppose we have $\states' \subseteq \states$ such that $ \exists \scheduler' \in \schedulers^{\mdp_{\states'}} \centerdot \propAlt{\gtrsim}{\scheduler'}(\boldLambda)$. By <Ref> we have that there exists $\vect{y}' \in \realsnn^{\SA'}$ such that $(\SM')^\top\vect{y}' \leq \initDistr \land (\TM')^\top \vect{y}' \gtrsim \boldLambda$. Now let $\vect{y} \in \realsnn^\SA$ and we set $\vect{y}(\state, \action) = \vect{y}'(\state, \action)$ if $(\state, \action) \in \SA'$ and $\vect{y}(\state, \action) = 0$ otherwise. Observe that $\stateSupp{\vect{y}} \subseteq \states'$ and for every state $\state \in \states \setminus \states'$ we have $\sum_{\action \in \actions(\state)} \vect{y}(\state, \action) - \sum_{(t, \action)} \transMat(t, \action, \state) \cdot \vect{y}(\state, \action) - \initDistr(\state) \leq 0$, because we have $\sum_{\action \in \actions(\state)} \vect{y}(\state, \action) = 0$. By construction we have $\TM^\top \vect{y} = (\TM')^\top \vect{y'}$. In total, we then have $\SM^\top\vect{y} \leq \initDistr \land \TM^\top \vect{y} \gtrsim \boldLambda$ because adding rows corresponding to $\state \in \states \setminus \states'$ preserves the satisfaction, as well as adding columns where $\vect{y}$ is zero.

§.§ Proofs for <Ref>

§.§.§ Reduction and transfer of subsystems

Let us discuss the reduction described in <Ref> and shown in the upper part of <Ref> in detail.
Recall that $\mathcal{N} = (\states_\mathcal{N}, \actions, \bar{\state}, \transMat_\mathcal{N})$ is an arbitrary MDP and $\query_\mathcal{N}$ is a -query containing lower-bounded predicates $\prob_\mathcal{N}^\scheduler(\eventually T_1) \gtrsim \lambda_1, \dots, \prob_\mathcal{N}^\scheduler(\eventually T_k) \gtrsim \lambda_k$ and $\prob_\mathcal{N}^\scheduler(\globally G_1) \gtrsim \xi_1, \dots, \prob_\mathcal{N}^\scheduler(\globally G_\ell) \gtrsim \xi_\ell$.
We follow the construction from <cit.> for the product MDP $\mdp$. Let $\mdp = (\states, \actions, \init, \transMat)$ where $\states = \states_\mathcal{N} \times 2^{[k]} \times 2^{[\ell]}$, $\init = (\bar{\state}, \emptyset)$ and:

\[
\transMat((\state, u, v), \action, (\state', u', v')) =
\begin{cases}
\transMat_{\mathcal{N}}(\state, \action, \state'),& \text{if } u' = u \union \{i \in [k] \mid \state \in T_i \} \text{ and} \\
& v' = v \union \{j \in [\ell] \mid \state \in \states\setminus G_j \} \\
0,              & \text{otherwise.}
\end{cases}
\]

Intuitively, $u$ keeps track of the “good” and $v$ the “bad” states that have been visited. The predicates can be easily rephrased, i.e. $\prob_\mathcal{N}^\scheduler(\eventually T)$ to $\prob_{\mdp}^\scheduler(\eventually (T \times 2^{[k]} \times 2^{[\ell]}))$ and analogously for invariant probabilities. For brevity, we write $\prob_{\mdp}^\scheduler(\eventually T)$ instead.
Because almost all paths eventually stay in a MEC <cit.>, instead of considering $\prob_{\mdp}^\scheduler(\eventually T_i)$, we can consider the probability of eventually staying in a MEC $\mec \in \MECS(\mdp)$ where $T_i$ has already been visited, that is there exists a $(\state, u, v) \in \states(\mec)$ with $i \in u$. Analogously, for $\prob_{\mdp}^\scheduler(\globally \targetSet_j)$ we consider MECs $\mec$ where there exists $(\state, u, v) \in \states(\mec)$ with $j \notin v$. Note that inside MECs, the $u$ and $v$ component of the states are identical. Let $A_i \subseteq \MECS(\mdp)$ denote the set of these MECs for predicates $\prob_{\mdp}^\scheduler(\eventually \targetSet_i)$ and analogously $B_j \subseteq \MECS(\mdp)$ for predicates $\prob_{\mdp}^\scheduler(\globally \targetSet_j)$. We then consider the quotient $\hat{\mdp}$, where reaching $\bot_\mec$ corresponds to staying in MEC $\mec$ forever <cit.>. Clearly, we can then consider corresponding predicates of the form $\prob_{\hat{\mdp}}^{\hat{\scheduler}}(\eventually \{\bot_\mec \mid \mec \in A_i \})$ and $\prob_{\hat{\mdp}}^{\hat{\scheduler}}(\eventually \{\bot_\mec \mid \mec \in B_j \})$.

Recall that $\iota \colon \states \to \hat{\states}$ maps a state of the product MDP $\mdp$ to the corresponding state in $\hat{\mdp}$.
Given a set of states $\hat{\states}'$ of the MEC quotient, the corresponding set of states in $\mdp$ and $\mathcal{N}$ is given by $\states' = \{(\state, u, v) \in \states \mid \iota((\state, u, v)) \in \hat{\states}' \}$ and $\states_{\mathcal{N}}' = \{\state \in \states_\mathcal{N} \mid \exists u, v \centerdot \iota((\state, u, v)) \in \hat{\states} \}$, respectively.

Let $\hat{\mdp}'$ be the subsystem of $\hat{\mdp}$ induced by a set $\hat{\states}'$ that satisfies $\query_{\hat{\mdp}}$. Let $\mdp'$ be the corresponding subsystem for $\mdp$ induced by $\states'$ and $\mathcal{N}'$ the subsystem of $\mathcal{N}$ induced by $\states_\mathcal{N}'$. Observe that $\hat{\mdp}'$ corresponds to the MEC quotient of $\mdp'$. From <cit.> we then have that for any scheduler $\hat{\scheduler} \in \schedulers^{\hat{\mdp}'}$, there exists a scheduler $\scheduler \in \schedulers^{\mdp'}$ such that for all $i \in [k]$ and $j \in [\ell]$ we have

* $\prob_{\hat{\mdp}'}^{\hat{\scheduler}}(\eventually \{\bot_\mec \mid \mec \in A_i \}) = \prob_{\mdp'}^{\scheduler}(\eventually\globally \union_{\mec \in A_i} \states(\mec))$

* $\prob_{\hat{\mdp}'}^{\hat{\scheduler}}(\eventually \{\bot_\mec \mid \mec \in B_j \}) = \prob_{\mdp'}^\scheduler(\eventually\globally \union_{\mec \in B_j} \states(\mec))$

and vice versa. Additionally, for any scheduler $\scheduler \in \schedulers^{\mdp'}$ there exists a scheduler $\scheduler' \in \schedulers^{\mathcal{N}'}$ such that for all $i \in [k]$ and $j \in [\ell]$ we have

* $\prob_{\mdp'}^{\scheduler}(\eventually\globally \union_{\mec \in A_i} \states(\mec)) = \prob_{\mathcal{N}'}^{\scheduler'}(\eventually T_i)$

* $\prob_{\mdp'}^\scheduler(\eventually\globally \union_{\mec \in B_j} \states(\mec)) = \prob_{\mathcal{N}'}^{\scheduler'}(\globally G_j)$

and vice versa. This follows from the fact there is a one-to-one correspondence between schedulers of the MDP and its product and that almost all paths stay in an MEC forever <cit.>. The statement then follows.

§.§.§ Transferring witnessing schedulers

Let $\vect{x} \in \reals^\states$. We consider the linear equation system with $\state \in \states$:

\begin{align*}
\vect{x}(\state) &= \boldDelta(\state) + \sum_{u \in \states} (\vect{x}(u) - \boldMu(u)) \cdot \transMat(u, \state) \\
&= \boldDelta(\state) + \sum_{u \in \states} \vect{x}(u) \cdot \transMat(u, \state) - \sum_{u \in \states} \boldMu(u) \cdot \transMat(u, \state)
\end{align*}

Intuitively, the equations describe the expected frequencies of state $\state$ subtracted by the frequencies that are redirected to the copies of the states. Equivalently, the system can be written in vector-matrix notation as follows:

\begin{equation}
\label{eq:frequencies}
\vect{x} (\vect{I} - \transMat) = \boldDelta - \boldMu \cdot \transMat
\end{equation}

Observe that the steady-state distribution $\boldGamma$ of $\dtmc$ satisfies $\boldGamma (\vect{I} - \transMat) = 0$ and also $\boldGamma > \vect{0}$ since $\dtmc$ is strongly connected. Given a solution $\vect{x}^*$ to (<ref>), we know that $\vect{x}^* + r \cdot \boldGamma$ is also a solution to (<ref>) for all $r \in \reals$. Thus, if there exists a solution, there also exists a solution $\vect{x}^*$ such that $\vect{x}^*(\state) > \boldMu(\state)$ for all states $\state$. Let $\boldLambda(\state) = \frac{\boldMu(\state)}{\vect{x}^*(s)}$, then $\boldLambda(\state) \in [0, 1]$. Setting $\boldMu(\state) = \boldLambda(\state) \cdot \vect{x}^*(\state)$ in (<ref>) yields for all states $\state$:

\[
\vect{x}^*(\state) = \boldDelta(\state) + \sum_{u \in \states} \vect{x}^*(u) \cdot (1 - \boldLambda(u)) \cdot \transMat(u, \state) = \boldDelta(\state) + \sum_{u \in \states} \vect{x}^*(u) \cdot \transMat_{\dtmc_{\boldLambda}}(u, \state)
\]

Considering the DTMC $\dtmc_{\boldLambda}$, the expected frequencies $\freq_{\dtmc_{\boldLambda}}(\state)$ are the unique solution of the following system with variables $\vect{z} \in \reals^\states$ and for all states $\state$:

\begin{align*}
\vect{z}(\state) &= \boldDelta(\state) + \sum_{u \in \states} \vect{z}(u) \cdot (1 - \boldLambda(u)) \cdot \transMat(u, \state)\\
\vect{z}(\state') &= \boldLambda(\state) \cdot \vect{z}(\state)
\end{align*}

Thus, $\vect{x}^*(\state) = \freq_{\dtmc_{\boldLambda}}(\state)$ and $\prob_{\dtmc_{\boldLambda}}(\eventually \state') = \freq_{\dtmc_{\boldLambda}}(\state') = \boldLambda(\state) \cdot \vect{x}^*(\state) = \boldMu(\state)$. Hence it remains to be shown that (<ref>) has a solution. We apply Farkas' lemma (<Ref> <ref>) on (<ref>) and show that the resulting system (shown below) cannot have a solution.

\begin{equation}
\label{eq:frequencies-farkas}
(\vect{I} - \transMat) \vect{y} = 0 \qquad \text{and} \qquad (\boldDelta - \boldMu \transMat)^\top \vect{y} \neq 0
\end{equation}

Since $\transMat$ is a stochastic matrix (all rows sum up to $1$), we have $(\vect{I} - \transMat) \vect{1} = 0$. Because $\dtmc$ is strongly connected, $\vect{I} - \transMat$ has rank $\card{\states} - 1$ and thus all solutions of $(\vect{I} - \transMat) \vect{y} = 0$ are multiples of $\vect{1}$. Let $\vect{y} = r \cdot \vect{1}$ for some $r \in \reals$. For all distributions $\boldGamma$ we have $\boldGamma^\top \vect{y} = r \cdot \boldGamma^\top \vect{1} = r$. In particular, we have $\boldDelta^\top \vect{y} = r$. Observe that $\boldMu \transMat$ is again a distribution and thus $\transMat^\top \boldMu^\top \vect{y} = r$. We then get $(\boldDelta - \boldMu \transMat)^\top \vect{y} = 0$ contradicting (<ref>). Thus, we can conclude that (<ref>) has a solution.

§ PROOFS FOR <REF>

$\Rightarrow$: Directly follows from <cit.> and <cit.>.

$\Leftarrow$: Let MDP $\mdp' = (\states \union \{\exit\}, \actions \union \{\tau\}, \init, \transMat')$ be the MDP obtained from $\mdp$ by adding a fresh state $\exit$ and transitions to $\exit$ under a fresh action $\tau$ in all states. Let $\states' = \states \union \{\exit\}$. In particular the enabled state action pairs in $\mdp'$ are $\SA' = \SA \union (\states' \times \{\tau\})$. For all $i \in [k]$ we define $\vect{r}_i' \in \rationals_{\geq0}^{\SA'}$ and set $\vect{r}_i'(\state, \action) = \vect{r}_i(\state, \action)$ if $(\state, \action) \in \SA$ and $\vect{r}_i'(\exit, \tau) = \min_{(\state, \action)} \vect{r}_i(\state, \action)$. Because the added transitions under action $\tau$ have lowest possible reward for each reward function, the existence of a strategy $\scheduler'$ for $\mdp'$ that satisfies the mean-payoff constraints implies the existence of satisfying strategy $\scheduler$ for $\mdp$.

Suppose we have $\vect{x}, \vect{y} \in \realsnn^\SA$ and $\vect{z} \in \realsnn^\states$ that satisfy the constraints. Then for all states $\state \in \states$ let:
We define $\vect{y}', \vect{x}' \in \realsnn^{\SA'}$ for all $(\state, \action) \in \SA'$ as follows:

\[
\vect{y}'(\state, \action) =
\begin{cases}
0, &\text{if } \state = \exit\\
\vect{z}(\state),& \text{if } \state \neq \exit \land \action = \tau \\
\vect{y}(\state, \action),              & \text{otherwise}
\end{cases}
\]

\[
\vect{x}'(\state, \action) =
\begin{cases}
\sum_{\state' \in \states} \vect{z}(\state'),& \text{if } \state = \exit \\
0, & \text{if } \state \neq \exit \land \action = \tau\\
\vect{x}(\state, \action),              & \text{otherwise}
\end{cases}
\]

We then have for all $\state \in \states$:

\begin{align*}
\initDistr(\state) + \sum_{(\state', \action') \in \SA'} \transMat'(\state', \action', \state) \cdot \vect{y}'(\state', \action') &= \initDistr(\state) + \sum_{(\state', \action') \in \SA} \transMat(\state', \action', \state) \cdot \vect{y}(\state', \action') \\
&= \sum_{\action \in \actions(\state)} \vect{y}(\state, \action) + \vect{x}(\state, \action) + \vect{z}(\state)\\
&= \sum_{\action \in \actions(\state) \union \{\tau\}} \vect{y}'(\state, \action) + \vect{x}'(\state, \action)
\end{align*}

Further, we have $\initDistr(\exit) + \sum_{(\state', \action') \in \SA'} \transMat'(\state', \action', \exit) \cdot \vect{y}'(\state', \action') = \sum_{\state \in \states} \vect{z}(\state) = \vect{x}'(\exit, \tau)$. Further, we also have for all $\state \in \states$:

\begin{align*}
\sum_{(\state', \action') \in \SA'} \transMat'(\state', \action', \state) \cdot \vect{x}'(\state', \action') &= \sum_{(\state', \action') \in \SA} \transMat(\state', \action', \state) \cdot \vect{x}(\state', \action') \\
&= \sum_{\action \in \actions(\state)} \vect{x}(\state, \action)\\
&= \sum_{\action \in \actions(\state) \union \{\tau\}} \vect{x}'(\state, \action)
\end{align*}

Analogously, we have $\sum_{(\state', \action') \in \SA'} \transMat'(\state', \action', \exit) \cdot \vect{x}'(\state', \action') = \sum_{\state \in \states} \vect{z}(\state) = \vect{x}'(\exit, \tau)$. Lastly, for all $i \in [k]$ we have:

\[
\sum_{(\state, \action) \in \SA'} \vect{x}'(\state, \action) \cdot {\vect{r}_i}'(\state,\action) = \sum_{(\state, \action) \in \SA} \vect{x}(\state, \action) \cdot \vect{r}_i(\state,\action) + \sum_{\state \in \states} \vect{z}(\state) \cdot {\vect{r}_{\min}}(i, \state) \geq \lambda_i
\]

From <cit.> and <cit.> we then know that there exists a scheduler $\scheduler' \in \schedulers^{\mdp'}$ such that $\Conj_{i=1}^k \expectation[\mdp', \init]{\scheduler'}{\lrInf{\vect{r}'_i}} \geq \lambda_i$. However, as mentioned above, this also implies the existence of a scheduler $\scheduler \in \schedulers^{\mdp}$ such that $\Conj_{i=1}^k \expectation[\mdp, \init]{\scheduler}{\lrInf{\vect{r}_i}} \geq \lambda_i$.

The variables $y_s$, constraint 2 and 3 in <cit.> are redundant (as also noted in the work). Let us briefly comment on this redundancy. Consider an MDP where each state has a copy state $\state'$.
Then $y_s$ describes the probability of reaching this copy state $\state'$ <cit.>. The sum $\sum_{s \in S} y_s$ equals $1$ because of the fact that $y_a$ corresponds to the expected frequencies of a scheduler that reaches the absorbing states almost surely <cit.> (also see <cit.>). From <cit.> it follows that $x_a$ is $0$ for state-action pairs not contained in MECs. Altogether, this makes $y_s$ and constraints 2 and 3 redundant.

We prove the statement via application of Farkas' lemma to the linear system given in <cit.>. Observe that we have $\expectation[\mdp, \init]{\scheduler}{\lrSup{\vect{r}_i}} = -\expectation[\mdp, \init]{\scheduler}{\lrInf{-\vect{r}_i}}$ for all schedulers $\scheduler \in \schedulers^\mdp$. The statement can then be shown as follows:

\begin{align*}
\forall \scheduler \in \schedulers \centerdot \Disj_{i=1}^k \expectation{\scheduler}{\lrSup{\vect{r}_i}} \geq \lambda_i
&\iff \neg \exists \scheduler \in \schedulers \centerdot \Conj_{i=1}^k \expectation{\scheduler}{\lrSup{\vect{r}_i}} < \lambda_i\\
&\iff \neg \exists \scheduler \in \schedulers \centerdot \Conj_{i=1}^k -\expectation{\scheduler}{\lrInf{-\vect{r}_i}} < \lambda_i\\
&\iff \neg \exists \scheduler \in \schedulers \centerdot \Conj_{i=1}^k \expectation{\scheduler}{\lrInf{-\vect{r}_i}} > -\lambda_i
\end{align*}

By <cit.> and the remark that in <cit.> that the constraints in <cit.> are partly redundant, the existence of a scheduler $\scheduler \in \schedulers$ that satisfies $\Conj_{i=1}^k \expectation{\scheduler}{\lrInf{-\vect{r}_i}} > -\lambda_i$ is equivalent of the satisfiability of the following system of linear equations:

\begin{align*}
\initDistr(\state) + \sum_{(\state', \action') \in \SA} \transMat(\state', \action', \state) \cdot \vect{y}(\state', \action') &= \sum_{\action \in \actions(\state)} \vect{y}(\state, \action) + \vect{x}(\state, \action) &\text{for all } \state \in \states\\
\sum_{(\state', \action') \in \SA} \transMat(\state', \action', \state) \cdot \vect{x}(\state', \action') &= \sum_{\action \in \actions(\state)} \vect{x}(\state, \action) &\text{for all } \state \in \states\\
\sum_{(\state, \action) \in \SA} \vect{x}(\state, \action) \cdot \bigl(- \vect{r}_i(\state,\action) \bigr)&\geq - \lambda_i + \varepsilon &\text{for all } i \in [k]
\end{align*}

where $\vect{x}, \vect{y} \in \realsnn^\SA$ and $\varepsilon > 0$. Equivalently, we can write the system in matrix vector notation as follows:

\begin{equation}
\begin{aligned}
(\vect{D} - \transMat)^\top \vect{y} + \vect{D}^\top \vect{x} &= \initDistr \\
(\vect{D} - \transMat)^\top\vect{x} &= \vect{0}\\
\vect{R}^\top \vect{x} + \vect{1} \cdot \varepsilon &\leq \boldLambda
\end{aligned}
\label{eq:non-scaled-exists}
\end{equation}

Here, $\vect{D} \in \{0, 1\}^{\SA \times \states}$ is defined as $\vect{D}((\state, \action), \state) = 1$ for all $(\state, \action) \in \SA$ and $0$ otherwise. In order to derive certificates and conditions for the universally quantified queries, we instead consider the following system:

\begin{equation}
\begin{aligned}
(\vect{D} - \transMat)^\top \vect{y} + \vect{D}^\top \vect{x} &= \initDistr \cdot \gamma \\
(\vect{D} - \transMat)^\top\vect{x} &= \vect{0}\\
\vect{R}^\top \vect{x} + \vect{1} \cdot \varepsilon &\leq \boldLambda \cdot \gamma\\
\gamma &\geq \varepsilon
\end{aligned}
\label{eq:scaled-exists}
\end{equation}

where again $\vect{x}, \vect{y} \in \realsnn^\SA$ and $\gamma, \varepsilon > 0$. Let us now show the equivalence in terms of satisfiability of those two systems.

(<ref>) $\Rightarrow$ (<ref>): Let $\vect{x}, \vect{y} \in \realsnn^\SA$ and $\varepsilon > 0$ be a solution of (<ref>). We can simply choose $\gamma = 1$ and choose $\varepsilon' = \min\{\gamma, \varepsilon\}$. Then $\vect{x}, \vect{y}$, $\varepsilon'$ and $\gamma$ are a solution to (<ref>).

(<ref>) $\Leftarrow$ (<ref>): Let $\vect{x}, \vect{y} \in \realsnn^\SA$ and $\gamma, \varepsilon > 0$ be a solution of (<ref>). Let $\vect{x}' = \vect{x} \cdot 1 / \gamma$, $\vect{y}' = \vect{y} \cdot 1 / \gamma$ and $\varepsilon' = \varepsilon \cdot 1 / \gamma$. Clearly, we have $(\vect{D} - \transMat)^\top\vect{x}' = \vect{0}$. Further, we have

\[
(\vect{D} - \transMat)^\top \vect{y}' + \vect{D}^\top\vect{x}' = \frac{1}{\gamma} \bigl((\vect{D} - \transMat)^\top \vect{y} + \vect{D}^\top\vect{x} \bigr) = \frac{1}{\gamma} \cdot \initDistr \cdot \gamma = \initDistr,
\]

\[
\vect{R}^\top \vect{x'} + \vect{1} \cdot \varepsilon' = \frac{1}{\gamma} \bigl( \vect{R}^\top \vect{x} + \vect{1} \cdot \varepsilon \bigr) \leq \frac{1}{\gamma} \bigl( \boldLambda \cdot \gamma \bigr) \leq \boldLambda
\]

Hence $\vect{x}', \vect{y}'$ and $\varepsilon'$ are a solution to (<ref>).

We are concerned with the non-existence of a scheduler and thus equivalently the unsatisfiability of (<ref>). We can write (<ref>) as follows:

\begin{equation*}
\setlength{\arraycolsep}{4pt}
\begin{pmatrix}
(\vect{D} - \transMat)^\top & \vect{D}^\top & -\initDistr & \vect{0}\\
-(\vect{D} - \transMat)^\top & -\vect{D}^\top & \initDistr & \vect{0}\\
\vect{0} & (\vect{D} - \transMat)^\top & \vect{0} & \vect{0}\\
\vect{0} & -(\vect{D} - \transMat)^\top & \vect{0} & \vect{0}\\
\vect{0} & - \vect{R}^\top & \boldLambda & -\vect{1}\\
0 & 0 & 1 & -1
\end{pmatrix}
\begin{pmatrix}
\vect{y}\\
\vect{x}\\
\gamma\\
\varepsilon
\end{pmatrix}
\geq
\begin{pmatrix}
\vect{0}\\
\vect{0}\\
\vect{0}\\
\vect{0}\\
\vect{0}\\
\end{pmatrix},
\qquad
\begin{pmatrix}
\vect{0}\\
\vect{0}\\
\vect{0}\\
\end{pmatrix}^\top
\begin{pmatrix}
\vect{y}\\
\vect{x}\\
\gamma\\
\varepsilon
\end{pmatrix}
\end{equation*}

We then apply Farkas' lemma (<Ref> <ref>), yielding the following system:

\begin{equation*}
\setlength{\arraycolsep}{4pt}
\begin{pmatrix}
\vect{D} - \transMat & -(\vect{D} - \transMat) & \vect{0} & \vect{0} & \vect{0} & 0 \\
\vect{D} & -\vect{D} & \vect{D} - \transMat & -(\vect{D} - \transMat) & - \vect{R} & 0 \\
- \initDistr^\top & \initDistr^\top & \vect{0} & \vect{0} & \boldLambda^\top & 1\\
\vect{0} & \vect{0} & \vect{0} & \vect{0} & -\vect{1}^\top & 1
\end{pmatrix}
\begin{pmatrix}
\vect{g}_{+}\\
\vect{g}_{-}\\
\vect{b}_{+}\\
\vect{b}_{-}\\
\vect{z}\\
\beta
\end{pmatrix}
\leq
\begin{pmatrix}
\vect{0}\\
\vect{0}\\
\end{pmatrix}
\end{equation*}

where $\vect{g}_{+}, \vect{g}_{-}, \vect{b}_{+}, \vect{b}_{-} \in \realsnn^\states$, $\vect{z} \in \realsnn^{[k]}$ and $\beta \in \realsnn$. We can further simplify inequalities by defining $\vect{g} \coloneqq \vect{g}_{+} - \vect{g}_{-}$ and $\vect{b} \coloneqq \vect{b}_{+} - \vect{b}_{-}$, yielding:

\begin{equation}
\begin{aligned}
(\vect{D} - \transMat) \vect{g} &\leq \vect{0} \\
\vect{D} \vect{g} + (\vect{D} - \transMat) \vect{b} &\leq \vect{R} \vect{z}\\
\initDistr^\top \vect{g} &\geq \boldLambda^\top \vect{z} + \beta\\
\vect{1}^\top \vect{z} &\geq 1 + \beta
\end{aligned}
\label{eq:farkas-results}
\end{equation}

Observe that any solution of (<ref>) where $\beta > 0$ is also a solution to (<ref>) when setting $\beta = 0$ because $\boldLambda^\top \vect{z} + \beta \geq \boldLambda^\top \vect{z}$ and $1 + \beta \geq 1$. Hence we can assume $\beta = 0$ and obtain the following conditions:

\begin{align*}
(\vect{D} - \transMat) \vect{g} &\leq \vect{0} \\
\vect{D} \vect{g} + (\vect{D} - \transMat) \vect{b} &\leq \vect{R} \vect{z}\\
\initDistr^\top \vect{g} &\geq \boldLambda^\top \vect{z}\\
\vect{1}^\top \vect{z} &\geq 1
\end{align*}

or equivalently written out explicitly:

\begin{align*}
\vect{g}(\state) &\leq \sum_{\state' \in \states} \transMat(\state, \action, \state') \cdot \vect{g}(\state') &\text{for all } (\state, \action) \in \SA\\
\vect{g}(\state) + \vect{b}(\state) &\leq \sum_{\state' \in \states} \transMat(\state, \action, \state') \cdot \vect{b}(\state') + \sum_{i=1}^k \vect{r}_i(\state, \action) \cdot \vect{z}(i) &\text{for all } (\state, \action) \in \SA\\
\vect{g}(\init) &\geq \sum_{i=1}^k \lambda_i \cdot \vect{z}(i) \qquad \sum_{i=1}^k \vect{z}(i) \geq 1 &
\end{align*}

Observe that if $\sum_{i=1}^k \vect{z}(i) > 1$, then we can simply rescale $\vect{x}$, $\vect{y}$ and $\vect{z}$ by $1 / \sum_{i=1}^k \vect{z}(i)$. Hence, we replace the constraint $\sum_{i=1}^k \vect{z}(i) \geq 1$ with $\sum_{i=1}^k \vect{z}(i) = 1$. Lastly, from <cit.> we can conclude that imposing $\vect{g}(\state) \geq \sum_{i=1}^k \vect{z}(i) \cdot \vect{r}_{\min}(i)$ does not change the satisfaction of the system.

Let $\mdp =  (\states, \actions, \init, \transMat)$ be an MDP and $\mdp' = (\states' \union \{\exit\}, \actions, \init, \transMat')$ be an induced subsystem of $\mdp$.

* If $(\vect{x}', \vect{y}', \vect{z}') \in \mathcal{H}_{\mdp'}^{\mathsf{MP}}(\boldLambda)$, then there exists $(\vect{x}, \vect{y}, \vect{z}) \in \mathcal{H}_{\mdp}^{\mathsf{MP}}(\boldLambda)$ such that $\stateSupp{\vect{x}, \vect{y}} \subseteq \stateSupp{\vect{x}', \vect{y}'}$.

* If $(\vect{g}', \vect{b}', \vect{z}') \in \mathcal{F}_{\mdp'}^{\mathsf{MP}}(\boldLambda)$, then there exists $(\vect{g}, \vect{b}, \vect{z}) \in \mathcal{F}_{\mdp}^{\mathsf{MP}}(\boldLambda)$ such that $\supp{\vect{g} - {\vect{R}_{\min}}\vect{z}} \subseteq \supp{\vect{g}' - {{\vect{R}'}_{\min}}\vect{z}'}$.

Proof of <ref>:
Let $\gamma_i \coloneqq \min_{(\state, \action) \in \SA} \vect{r}_i(\state, \action)$ for all $i \in [k]$. Suppose we have $(\vect{x}', \vect{y}', \vect{z}') \in \mathcal{H}_{\mdp'}^{\mathsf{MP}}$. Then for all $\state \in \states' \union \{\exit\}$ we have:

\begin{align}
\initDistr'(\state) + \sum_{(\state', \action') \in \SA'} \transMat'(\state', \action', \state) \cdot \vect{y}'(\state', \action') &= \sum_{\action \in \actions'(\state)} \vect{y}'(\state, \action) + \vect{x}'(\state, \action) + \vect{z}'(\state) \label{eq:monotonicity-proof-transient}\\
\sum_{(\state', \action') \in \SA'} \transMat'(\state', \action', \state) \cdot \vect{x}'(\state', \action') &= \sum_{\action \in \actions'(\state)} \vect{x}'(\state, \action) \label{eq:monotonicity-proof-recurrent}
\end{align}

and for all $i \in [k]$ we have:

\begin{align}
\sum_{(\state, \action) \in \SA'} \vect{x}'(\state, \action) \cdot \vect{r}'_i(\state,\action) + \sum_{\state \in \states' \union \{\exit\}} \vect{z}'(\state) \cdot \gamma_i &\geq \lambda_i \label{eq:monotonicity-proof-spec}
\end{align}

Let us define $\vect{x}, \vect{y} \in \realsnn^\SA$ as follows:

\[
\vect{x}(\state, \action) =
\begin{cases}
\vect{x}'(\state, \action),& \text{if } \state \in \states' \\
0,              & \text{otherwise}
\end{cases}
\qquad
\vect{y}(\state, \action) =
\begin{cases}
\vect{y}'(\state, \action),& \text{if } \state \in \states' \\
0,              & \text{otherwise}
\end{cases}
\]

Further, we define $\vect{z} \in \reals^\states$ for all $\state \in \states$ as follows:

\[
\vect{z}(\state) =
\begin{cases}
\vect{z}'(\state), & \text{if } \state \in \states' \\
\sum_{\state' \in \states'} \sum_{\action' \in \actions(\state')} \transMat(\state', \action' , \state) \cdot \vect{y}(\state', \action'),              & \text{otherwise}
\end{cases}
\]

By construction, we have $\stateSupp{\vect{x}} \union \stateSupp{\vect{y}} \subseteq \stateSupp{\vect{x}'} \union \stateSupp{\vect{y}'}$. Now it remains to be shown that $(\vect{x}, \vect{y}, \vect{z}) \in \mathcal{H}_{\mdp}^{\mathsf{MP}}$. To this end, we observe that $\vect{x}'(\state, \action) = 0$ for all states $\state \in \states'$ and $\action \in \actions(\state)$ if $\transMat'(\state, \action, \exit) > 0$ because otherwise (<ref>) would not be satisfied. Hence $\vect{x}(\state, \action) = 0$ if $\transMat(\state, \action, \state') > \transMat'(\state, \action, \state')$ for some $\state' \in \states$. We then get for all states $\state \in \states \setminus \states'$:

\begin{align*}
\sum_{(\state', \action') \in \SA} \transMat(\state', \action', \state) \cdot \vect{x}(\state', \action') = 0 = \sum_{\action \in \actions(\state)} \vect{x}(\state, \action)
\end{align*}

For all states $\state \in \states'$ we have:

\begin{align*}
\sum_{(\state', \action') \in \SA} \transMat(\state', \action', \state) \cdot \vect{x}(\state', \action') &= \sum_{(\state', \action') \in \SA'} \transMat(\state', \action', \state) \cdot \vect{x}(\state', \action')\\
&= \sum_{(\state', \action') \in \SA'} \transMat'(\state', \action', \state) \cdot \vect{x}(\state', \action')\\
\overset{\eqref{eq:monotonicity-proof-recurrent}}&{=} \sum_{\action \in \actions(\state)} \vect{x}(\state, \action)
\end{align*}

So in total, we have $\sum_{(\state', \action') \in \SA} \transMat(\state', \action', \state) = \sum_{\action \in \actions(\state)} \vect{x}(\state, \action)$ for all $\state \in \states$. Further, for all $\state \in \states'$ we have:

\begin{align*}
&\initDistr(\state) + \sum_{(\state', \action') \in \SA} \transMat(\state', \action', \state) \cdot \vect{y}(\state', \action')\\
={}&\initDistr(\state) + \sum_{(\state', \action') \in \SA'} \transMat'(\state', \action', \state) \cdot \vect{y}'(\state', \action')\\
\overset{\eqref{eq:monotonicity-proof-transient}}{=}{}&\sum_{\action \in \actions(\state)} \vect{y}'(\state, \action) + \vect{x}'(\state, \action) + \vect{z}'(\state)\\
={}&\sum_{\action \in \actions(\state)} \vect{y}(\state, \action) + \vect{x}(\state, \action) + \vect{z}(\state)
\end{align*}

For all $\state \in \states \setminus \states'$ we have:

\begin{align*}
&\initDistr(\state) + \sum_{(\state', \action') \in \SA} \transMat(\state', \action', \state) \cdot \vect{y}(\state', \action')\\
={}&\initDistr(\state) + \sum_{\state' \in \states'} \sum_{\action' \in \actions(\state')} \transMat(\state', \action', \state) \cdot \vect{y}(\state', \action')\\
={}&\sum_{\action \in \actions(\state)} \vect{y}(\state, \action) + \vect{x}(\state, \action) + \vect{z}(\state)
\end{align*}

Lastly, for all $i \in [k]$ we have:

\begin{align*}
&\sum_{(\state, \action) \in \SA} \vect{x}(\state, \action) \cdot \vect{r}_i(\state,\action) + \sum_{\state \in \states} \vect{z}(\state) \cdot \gamma_i\\
={}&\sum_{\state \in \states'} \sum_{\action \in \actions(\state)} \vect{x}'(\state, \action) \cdot \vect{r}_i'(\state, \action) + \\
&\sum_{\state \in \states \setminus \states'}\sum_{\state' \in \states'} \sum_{\action' \in \actions(\state')} \transMat(\state', \action' , \state) \cdot \vect{y}(\state', \action') \cdot \gamma_i +\\
&\sum_{\state \in \states'} \vect{z}'(\state) \cdot \gamma_i\\
={}&\sum_{\state \in \states'} \sum_{\action \in \actions(\state)} \vect{x}'(\state, \action) \cdot \vect{r}_i'(\state, \action) + \\
&\sum_{\state' \in \states'} \sum_{\action' \in \actions(\state')} \transMat'(\state', \action' , \exit) \cdot \vect{y}(\state', \action') \cdot \gamma_i +\\
&\sum_{\state \in \states'} \vect{z}'(\state) \cdot \gamma_i\\
={}&\sum_{(\state, \action) \in \SA'} \vect{x}'(\state, \action) \cdot \vect{r}_i'(\state, \action) + \sum_{\states' \union \{\exit\}} \vect{z}'(\state) \cdot \gamma_i \geq \lambda_i
\end{align*}

In total, we can therefore conclude that $(\vect{x}, \vect{y}, \vect{z}) \in \mathcal{H}_{\mdp}^{\mathsf{MP}}$.

Proof of <ref>: Let $(\vect{g}', \vect{b}', \vect{z}') \in \mathcal{F}_{\mdp'}^{\mathsf{MP}}(\boldLambda)$. Then the following holds for all $(\state, \action) \in \SA'$:

\begin{align}
\vect{g}'(\state) &\leq \sum_{\state' \in \states' \union \{\exit\}} \transMat'(\state, \action, \state') \cdot \vect{g}'(\state')\\
\vect{g}'(\state) + \vect{b}'(\state) &\leq \sum_{\state' \in \states' \union \{\exit\}} \transMat'(\state, \action, \state') \cdot
\vect{b}'(\state') + \sum_{i=1}^k \vect{r}'_i(\state, \action) \cdot \vect{z}'(i) \label{eq:proof-monotonicity-forall-bias-gain}
\end{align}

and for all $\state \in \states' \union \{\exit\}$:

\begin{align*}
\vect{g}'(\state) \geq \sum_{i=1}^k \vect{z}'(i) \cdot {\vect{r}_{\min}}(i)
\end{align*}

and for all $i \in [k]$:

\begin{align}
\vect{g}'(\init) &\geq \sum_{i=1}^k \lambda_i \cdot \vect{z}'(i)
\end{align}

Let us define $\vect{z} = \vect{z}'$ and $\vect{g} \in \reals^\states$ as follows:

\[
\vect{g}(\state) =
\begin{cases}
\vect{g}'(\state),& \text{if } \state \in \states' \\
\sum_{i=1}^k \vect{z}'(i) \cdot {\vect{r}_{\min}}(i),              & \text{otherwise}
\end{cases}
\]

By construction we have $\supp{\vect{g} - {\vect{R}_{\min}}\vect{z}} \subseteq \supp{\vect{g}' - {{\vect{R}'}_{\min}}\vect{z}'}$. Analogously, we now need to show that there exists a $\vect{b} \in \reals^\states$ such that $(\vect{g}, \vect{b}, \vect{z}) \in \dqPoly{\mdp}{\geq}(\boldLambda)$.

For the sake of readability, let us define $\vect{c} \in \realsnn^\SA$ as $\vect{c}(\state, \action) = \sum_{i=1}^k \vect{r}_i(\state, \action) \cdot \vect{z}(i)$ for all $(\state, \action) \in \SA$ and $\vect{c}' \in \realsnn^{\SA'}$ as $\vect{c}'(\state, \action) = \sum_{i=1}^k {\vect{r}_i}'(\state, \action) \cdot \vect{z}(i)$ for all $(\state, \action) \in \SA'$.

We observe that we have $\vect{g}'(\exit) \geq \sum_{i=1}^k \vect{z}'(i) \cdot {\vect{r}_{\min}}'(i) = \sum_{i=1}^k \vect{z}(i) \cdot {\vect{r}_{\min}}(i)$. From (<ref>), we then have for all $\action \in \actions'(\exit)$ that

\[
\vect{g}'(\exit) + \vect{b}'(\exit) \leq \vect{b}'(\exit) + \sum_{i=1}^k \vect{c}'(\exit, \action) = \vect{b}'(\exit) + \sum_{i=1}^k \vect{z}(i) \cdot {\vect{r}_{\min}}(i)
\]

So in total we have $\vect{g}'(\exit) = \sum_{i=1}^k \vect{z}(i) \cdot {\vect{r}_{\min}}(i)$. Then, for all states $\state \in \states'$ and $\action \in \actions(\state)$ we get

\begin{align*}
\vect{g}(\state) = \vect{g}'(\state) &\leq \sum_{\state' \in \states' \union \{\exit\}} \transMat'(\state, \action, \state') \cdot \vect{g}'(\state')\\
&= \bigl(\sum_{\state' \in \states'} \transMat'(\state, \action, \state') \cdot \vect{g}'(\state') \bigr) + \transMat'(\state, \action, \exit) \cdot \vect{g}'(\exit)\\
&= \bigl(\sum_{\state' \in \states'} \transMat'(\state, \action, \state') \cdot \vect{g}'(\state') \bigr) + \transMat'(\state, \action, \exit) \cdot (\sum_{i=1}^k \vect{z}(i) \cdot {\vect{r}_{\min}}(i))\\
&= \bigl(\sum_{\state' \in \states'} \transMat'(\state, \action, \state') \cdot \vect{g}'(\state') \bigr) + \sum_{\state' \in \states \setminus \states'} \transMat(\state, \action, \state') \cdot \vect{g}(\state')\\
&= \sum_{\state' \in \states} \transMat(\state, \action, \state') \cdot \vect{g}(\state')
\end{align*}

Because $\vect{g}(\state) = \sum_{i=1}^k \vect{z}'(i) \cdot {\vect{r}_{\min}}'(i)$ for $\state \in \states \setminus \states'$ and the $\vect{g}(\state') \geq \sum_{i=1}^k \vect{z}'(i) \cdot {\vect{r}_{\min}}'(i)$ for all $\state' \in \states'$, we can conclude that $\vect{g}(\state) \leq \sum_{\state' \in \states} \transMat(\state, \action, \state') \cdot \vect{g}(\state')$ for all $(\state, \action) \in \SA$. Further, observe that because $\init \in \states'$ we have $\vect{g}(\init) = \vect{g}'(\init) \geq \sum_{i=1}^k \lambda_i \cdot \vect{z}(i)$.

Now it only remains to be shown that there exists a $\vect{b} \in \reals^\states$ such that for all $(\state, \action) \in \SA$ we have:

\begin{equation}
\vect{g}(\state) + \vect{b}(\state) \leq \sum_{\state' \in \states} \transMat(\state, \action, \state') \cdot \vect{b}(\state') + \vect{c}(\state, \action)
\label{eq:proof-monotonicity-gain-bias-original}
\end{equation}

For the sake of contradiction, suppose this was not the case. Then, by <Ref> <ref> there exists $\vect{x} \in \realsnn^\SA$ such that

\begin{align*}
\sum_{(\state' \action') \in \SA} \transMat(\state', \action', \state) \cdot \vect{x}(\state', \action') &= \sum_{\action \in \actions(\state)} \vect{x}(\state, \action) &\text{for all } \state \in \states\\
\sum_{(\state, \action) \in \SA} \vect{c}(\state, \action) \cdot \vect{x}(\state, \action) &< \sum_{(\state, \action) \in \SA} \vect{x}(\state, \action) \cdot \vect{g}(\state)&
\end{align*}

We note that the first equation describes a recurrent flow. In particular, $\vect{x}(\state, \action) = 0$ if $(\state, \action)$ is not contained in a MEC <cit.>. This allows us to write the second inequality as follows:

\begin{align*}
\sum_{\mec \in \MECS(\mdp)} \sum_{(\state, \action) \in \mec} \vect{c}(\state, \action) \cdot \vect{x}(\state, \action) &= \sum_{(\state, \action) \in \SA} \vect{c}(\state, \action) \cdot \vect{x}(\state, \action)\\
&< \sum_{(\state, \action) \in \SA} \vect{x}(\state, \action) \cdot \vect{g}(\state)\\
&= \sum_{\mec \in \MECS(\mdp)} \sum_{(\state, \action) \in \mec} \vect{x}(\state, \action) \cdot \vect{g}(\state)
\end{align*}

In particular, there exists a MEC $\mec \in \MECS(\mdp)$ such that

\[
\sum_{(\state, \action) \in \mec} \vect{c}(\state, \action) \cdot \vect{x}(\state, \action) < \sum_{(\state, \action) \in \mec} \vect{x}(\state, \action) \cdot \vect{g}(\state)
\]

From <cit.>, we know that $\vect{g}(\state) \leq \inf_{\scheduler \in \schedulers^{\mdp'}} \expectation[\mdp',\state]{\scheduler}{\lrSup{\vect{c}'}} \leq \inf_{\scheduler \in \schedulers^\mdp} \expectation[\mdp,\state]{\scheduler}{\lrSup{\vect{c}}}$ for all $\state \in \states'$.
We write $\scheduler^* \in \schedulers^\mdp$ to denote such optimal scheduler for $\mdp$. Further, observe that all states in a MEC have the same optimal expected mean-payoff. Let us denote this common value by $\nu$, i.e. $\nu = \expectation[\mdp,\state]{\scheduler^*}{\lrSup{\vect{c}}}$ for some $\state \in \states(\mec)$. Then we get:

\[
\sum_{(\state, \action) \in \mec} \vect{c}(\state, \action) \cdot \vect{x}(\state, \action) < \sum_{(\state, \action) \in \mec} \expectation[\mdp,\state]{\scheduler^*}{\lrSup{\vect{c}}} \cdot \vect{x}(\state, \action) = \nu \cdot \sum_{(\state, \action) \in \mec} \vect{x}(\state, \action)
\]

However, this implies that there exists a scheduler $\scheduler \in \mSchedulers^\mdp$ that achieves a strictly lower value inside $\mec$ than $\scheduler^*$. More precisely, inside $\mec$ the scheduler $\scheduler$ ensures that states $\state$ with $\vect{x}(\state, \action) > 0$ for some $(\state, \action) \in \mec$ are reached almost surely and then switches to the strategy $\scheduler_\mec \in \mSchedulers^\mdp$ with $\scheduler_\mec(\state, \action) = \vect{x}(\state, \action) / \sum_{\action \in \actions(\state)} \vect{x}(\state, \action)$ (cf. <cit.>). This contradicts the optimality of $\scheduler^*$ and we can conclude that such $\vect{x}$ cannot exist in the first place. Thus there exists $\vect{b} \in \reals^\states$ such that $(\vect{g}, \vect{b}, \vect{z}) \in \mathcal{F}_{\mdp}^{\mathsf{MP}}(\boldLambda)$.

The directions from left to right directly follow from <Ref>, <Ref> and <Ref>. Hence, we only need to show that if there exists a certificate for $\mdp$, then the corresponding support induces a subsystem that also satisfies the query. In the following, we write $\mdp' = \mdp_{\states'} = (\states' \union \{\exit\}, \actions, \init, \transMat')$ to denote the subsystem induced by $\states'$. Recall that $\SA' = \SA_{\mdp'} = \{(\state, \action) \in \SA \mid \state \in \states' \} \union \{(\exit, \action) \mid \action \in \actions \}$.

Proof of <ref>: Suppose there exists $(\vect{x}, \vect{y}, \vect{z}) \in \mathcal{H}_{\mdp}^{\mathsf{MP}}(\boldLambda)$ such that $\stateSupp{\vect{x}, \vect{y}} \subseteq \states'$. Then for all $\state \in \states' \subseteq \states$ we have:

\begin{align*}
\initDistr(\state) + \sum_{(\state', \action') \in \SA} \transMat(\state', \action', \state) \cdot \vect{y}(\state', \action') &= \sum_{\action \in \actions(\state)} \vect{y}(\state, \action) + \vect{x}(\state, \action) + \vect{z}(\state) \\
\sum_{(\state', \action') \in \SA} \transMat(\state', \action', \state) \cdot \vect{x}(\state', \action') &= \sum_{\action \in \actions(\state)} \vect{x}(\state, \action)
\end{align*}

and for all $i \in [k]$ we have:

\begin{align*}
\sum_{(\state, \action) \in \SA} \vect{x}(\state, \action) \cdot \vect{r}_i(\state,\action) + \sum_{\state \in \states} \vect{z}(\state) \cdot {\vect{r}_{\min}}(i) &\geq \lambda_i
\end{align*}

Let be an arbitrary $a' \in \actions(\exit)$ and let us define $\vect{x}', \vect{y}' \in \realsnn^{\SA'}$ as follows:

\begin{align*}
\vect{y}'(\state, \action) =
\begin{cases}
0,& \text{if } \state = \exit \\
\vect{y}(\state, \action),              & \text{otherwise}
\end{cases}
\\
\vect{x}'(\state, \action) =
\begin{cases}
\sum_{(\state', \action') \in \SA'} \transMat'(\state', \action', \exit) \cdot \vect{y}'(\state', \action') , & \text{if } \state = \exit \land a = a' \\
0 , & \text{if } \state = \exit \land a \neq a' \\
\vect{x}(\state, \action), & \text{otherwise}
\end{cases}
\end{align*}

Further, let $\vect{z}' \in \realsnn^{\states' \union \{\exit\}}$ with $\vect{z}'(\state) = \vect{z}(\state)$ for $\state \in \states'$ and $\vect{z}'(\exit) = 0$. We now show that the constructed vectors $(\vect{x}', \vect{y}', \vect{z}') \in \mathcal{H}_{\mdp'}^{\mathsf{MP}}(\boldLambda)$. We then get for all $\state \in \states'$:

\begin{align*}
\initDistr'(\state) + \sum_{(\state', \action') \in \SA'} \transMat'(\state', \action', \state) \cdot \vect{y}'(\state', \action') &= \initDistr(\state) + \sum_{(\state', \action') \in \SA'} \transMat(\state, \action, \state) \cdot \vect{y}(\state', \action')\\
&= \sum_{\action \in \actions(\state)} \vect{y}(\state, \action) + \vect{x}(\state, \action)+ \vect{z}(\state) \\
&= \sum_{\action \in \actions(\state)} \vect{y}'(\state, \action) + \vect{x}'(\state, \action) + \vect{z}'(\state)
\end{align*}

Further, we have $\initDistr'(\exit) + \sum_{(\state', \action') \in \SA'} \transMat'(\state', \action', \exit) \cdot \vect{y}'(\state', \action') = \sum_{\action \in \actions(\bot)} \vect{y}'(\exit, \action) + \vect{x}'(\exit, \action)$. Similarly, for all states $\state \in \states'$:

\begin{align*}
\sum_{(\state', \action') \in \SA'} \transMat'(\state', \action', \state) \cdot \vect{x}'(\state', \action') &= \sum_{(\state', \action') \in \SA} \transMat(\state', \action', \state) \cdot \vect{x}(\state', \action')\\
&= \sum_{\action \in \actions(\state)} \vect{x}(\state, \action)\\
&= \sum_{\action \in \actions(\state)} \vect{x}'(\state, \action)
\end{align*}

Again, we have $\sum_{(\state', \action') \in \SA'} \transMat'(\state', \action', \exit) \cdot \vect{x}'(\state', \action') = \sum_{\action \in \actions(\exit)}\vect{x}'(\exit, \action)$. Lastly, we have for all $i \in [k]$:

\begin{align*}
{}&\sum_{(\state, \action) \in \SA'} \vect{x}'(\state, \action) \cdot \vect{r}'_i(\state,\action) + \sum_{\state \in \states' \union \{\exit\}} \vect{z}'(\state) \cdot {\vect{r}_{\min}}'(i) \\
={}&\sum_{(\state, \action) \in \SA} \vect{x}(\state, \action) \cdot \vect{r}_i(\state,\action) + \sum_{\state \in \states} \vect{z}(\state) \cdot {\vect{r}_{\min}}(i)\\
\geq{}& \lambda_i
\end{align*}

Hence $(\vect{x}', \vect{y}') \in \cqPoly{\mdp'}{\geq}(\boldLambda)$ and by <Ref> the statement follows.

Proof of <ref>: Let $(\vect{g}, \vect{b}, \vect{z}) \in \dqPoly{\mdp}{\geq}(\boldLambda)$ such that $\supp{\vect{g} - {\vect{R}_{\min}} \vect{z}} \subseteq \states'$. Then we have:

\begin{align*}
\vect{g}(\state) &\leq \sum_{\state' \in \states} \transMat(\state, \action, \state') \cdot \vect{g}(\state') &\text{for all } (\state, \action) \in \SA\\
\vect{g}(\state) + \vect{b}(\state) &\leq \sum_{\state' \in \states} \transMat(\state, \action, \state') \cdot \vect{b}(\state') + \sum_{i=1}^k \vect{r}_i(\state, \action) \cdot \vect{z}(i) &\text{for all } (\state, \action) \in \SA\\
\vect{g}(\init) &\geq \sum_{i=1}^k \lambda_i \cdot \vect{z}(i) \qquad \sum_{i=1}^k \vect{z}(i) \geq 1 &\\
\vect{g}(\state) &\geq \sum_{i=1}^k \vect{z}(i) \cdot {\vect{r}_{\min}}(i) & \text{for all } \state \in \states
\end{align*}

We now construct corresponding $\vect{g}' \in \realsnn^{\states' \union \{\exit\}}$, $\vect{b}' \in \reals^{\states' \union \{\exit\}}$ and $\vect{z}' \in \realsnn^{[k]}$ and show that $(\vect{g}', \vect{b}', \vect{z}') \in \dqPoly{\mdp'}{\geq}(\boldLambda)$. We set $\vect{z}' = \vect{z}$ and define $\vect{g}'$ and $\vect{b}'$ as follows:

\[
\vect{g}'(\state) =
\begin{cases}
\sum_{i=1}^k \vect{z}(i) \cdot {\vect{r}_{\min}}(i), & \text{if } \state = \exit \\
\vect{g}(\state), & \text{otherwise}
\end{cases}
\qquad
\vect{b}'(\state) =
\begin{cases}
\max_{\state' \in \states} \vect{b}(\state'),& \text{if } \state = \exit \\
\vect{b}(\state),              & \text{otherwise}
\end{cases}
\]

We directly see that

\begin{align*}
\vect{g}'(\state) = \vect{g}(\state) &\leq \sum_{\state' \in \states} \transMat(\state, \action, \state') \cdot \vect{g}(\state')\\
&= \sum_{\state' \in \states'} \transMat(\state, \action, \state') \cdot \vect{g}(\state') + \sum_{\state' \in \states \setminus \states'}\transMat(\state, \action, \state') \cdot \vect{g}(\state')\\
&= \sum_{\state' \in \states'} \transMat(\state, \action, \state') \cdot \vect{g}(\state') + \sum_{\state' \in \states \setminus \states'}\transMat(\state, \action, \state') \cdot (\sum_{i=1}^k \vect{z}(i) \cdot {\vect{r}_{\min}}(i))\\
&= \sum_{\state' \in \states' \union \{\exit\}} \transMat'(\state, \action, \state') \cdot \vect{g}'(\state')
\end{align*}

for all $(\state, \action) \in \SA'$ with $\state \neq \exit$. Let us define $\vect{c}(\state, \action) = \sum_{i=1}^k \vect{r}_i(\state, \action) \cdot \vect{z}(i)$ for all $(\state, \action) \in \SA'$. Then, for all $(\state, \action) \in \SA'$ with $\state \neq \exit$ we have:

\begin{align*}
\vect{g}'(\state) + \vect{b}'(\state) &= \vect{g}(\state) + \vect{b}(\state)\\
&\leq \sum_{\state' \in \states} \transMat(\state, \action, \state') \cdot \vect{b}(\state') + \vect{c}(\state, \action)\\
&= \sum_{\state' \in \states'} \transMat(\state, \action, \state') \cdot \vect{b}(\state') + \sum_{\state' \in \states\setminus\states'} \transMat(\state, \action, \state') \cdot \vect{b}(\state') + \vect{c}(\state, \action)\\
&\leq \sum_{\state' \in \states'} \transMat(\state, \action, \state') \cdot \vect{b}(\state') + \sum_{\state' \in \states\setminus\states'} \transMat(\state, \action, \state') \cdot (\max_{\state'' \in \states} \vect{b}(\state''))+ \vect{c}(\state, \action)\\
&= \sum_{\state' \in \states'} \transMat(\state, \action, \state') \cdot \vect{b}'(\state') + \sum_{\state' \in \states\setminus\states'} \transMat(\state, \action, \state') \cdot \vect{b}'(\exit)+ \vect{c}(\state, \action)\\
&= \sum_{\state' \in \states' \union \{\exit\}} \transMat'(\state, \action, \state') \cdot \vect{b}'(\state') + \vect{c}(\state, \action)
\end{align*}

For $(\exit, \action) \in \SA'$ we have

\begin{align*}
\vect{g}'(\exit) + \vect{b}'(\exit)
&=\sum_{i=1}^k \vect{z}(i) \cdot {\vect{r}_{\min}}(i) + \transMat'(\exit, \action, \exit) \cdot \vect{b}'(\exit)\\
&\leq \sum_{i=1}^k \vect{z}'(i) \cdot \vect{r}'_i(\exit, \action) + \sum_{\state' \in \states' \union \{\exit\}} \transMat'(\exit, \action, \state') \cdot \vect{b}'(\state')
\end{align*}

Lastly, we have $\vect{g}'(\init) = \vect{g}(\init)$. With that, we can conclude $(\vect{g}', \vect{b}', \vect{z}') \in \dqPoly{\mdp'}{\geq}(\boldLambda)$ and with <Ref> the statement follows.

§ MILPS FOR FINDING WITNESSING SUBSYSTEMS

§.§ MILPs for Reachability

Recall the MILPs in <Ref>. We now touch upon the choice of $M$.

MILPs for -queries.
Firstly, we note that for the MILP of -queries, we can impose the additional constraint $\sum_{i \in [k]} \vect{z}(i) = 1$ if $\gtrsim \ = \ \geq$ and $\sum_{i \in [k]} \vect{z}(i) \leq 1$ if $\gtrsim \ = \ >$. For $\geq$, observe that given a certificate $(\vect{x}, \vect{z}) \in \dqPoly{\mdp}{\geq}(\pmb{\lambda})$, we can simply rescale with $\gamma = \frac{1}{\sum_{i \in [k]} \vect{z}(i)}$, i.e. $(\gamma \cdot \vect{x}, \gamma \cdot \vect{z}) \in \dqPoly{\mdp}{\gtrsim}(\pmb{\lambda})$, $\sum_{i \in [k]} \gamma \cdot \vect{z}(i) = 1$ and $\supp{\gamma \cdot \vect{x}} = \supp{\vect{x}}$. Analogously, we proceed for $>$. Imposing these additional constraints, ensures that $\vect{x}$ is bounded and an upper bound can be found via LP <cit.>. As a consequence of <cit.>, we can also simply choose $k$ as upper bound.

MILPs for -queries.
Unlike in the single-objective setting <cit.>, the set $\cqPoly{\mdp}{\gtrsim}(\boldLambda)$ is generally unbounded (see <cit.>). Note that if a minimal witnessing subsystem is given, its certificate can be easily determined and can serve as upper bound. Obviously, it is thus difficult to determine an upper bound $M$ a priori. Here, we resort to indicator constraints, i.e. constraints of the form $\gamma(\state) = 0 \implies \vect{y}(\state, \action) = 0$. These constraints are supported by Gurobi <cit.>.

§.§ MILPs for Mean-Payoff

To find minimal witnessing subsystem for mean-payoff queries, we can consider the MILPs shown in <Ref>. Like for reachability, we use the Big-$M$ encoding. Let us briefly discuss the choice of $M$. Like for reachability, we can impose the additional constraints on $\vect{z}$. Then $\vect{g}$ can again be bounded, e.g. by considering the absolute sum of the smallest and largest rewards (see e.g. <cit.>). It is well known that $\vect{x}$ is bounded from above by $\vect{1}$, see e.g. <cit.>. For the MILP for $\existsCQ$-queries, $\vect{y}$ is again generally unbounded. Here, we also resort to indicator constraints.

&\text{min } \sum_{\state \in \states} \boldGamma(\state) \text{  subject to:} \\
&\boldGamma \in \{0, 1\}^\states \text{ and } (\vect{x}, \vect{y}, \vect{z}) \in \mathcal{H}_{\mdp}^{\mathsf{MP}}(\boldLambda)\\
&\forall (\state, \action) \in \SA \centerdot \vect{x}(\state, \action) \leq \boldGamma(\state) \cdot M\\
&\forall (\state, \action) \in \SA \centerdot \vect{y}(\state, \action) \leq \boldGamma(\state) \cdot M
\end{aligned}$
MILP for $\existsCQ$-mean-payoff queries

&\text{min } \sum_{\state \in \state} \boldGamma(\state)\text{  subject to:}\\
&\boldGamma \in \{0, 1\}^\states \text{ and } (\vect{g}, \vect{b}, \vect{z}) \in \mathcal{F}_{\mdp}^{\mathsf{MP}}(\boldLambda)\\
&\forall \state \in \states \centerdot \vect{g}(\state) - \sum_{i=1}^k \vect{z}(i) \cdot \vect{r}_{\min}(i) \leq \boldGamma(\state) \cdot M
\end{aligned}$
MILP for $\universalDQ$-mean-payoff queries

MILPs for finding minimal witnessing subsystems for mean-payoff queries.

§ SUPPLEMENTARY MATERIAL FOR <REF>

Our implementation, experiments and results are made available on Zenodo <cit.>.

Storm results. The runtimes of Storm in seconds are shown in <Ref>. We remark that we verified -queries $\query$ by considering the dual -queries $\neg\query$. Note that for some queries, we encountered an error, denoted with err. Note that we were unable to verify the queries of  with Storm, as the queries were not supported. We refer to the log files in <cit.>. Lastly, we note that the Storm build time is faster than the build time of our implementation, because we have implemented the product construction in Python. The reason is that Storm's product construction is not available through its Python API.

Model      Type     $k$     #     Storm build time     Storm verification

[c]2*     $(\exists, \land)$     2     5     0.012     0.002

$(\forall, \lor)$     2     5     0.012     0.002

[c]2*     $(\exists, \land)$     2     5     0.013     0.004

$(\forall, \lor)$     2     5     0.012     0.003

[c]2*     $(\exists, \land)$     2     5     0.012     0.005

$(\forall, \lor)$     2     5     0.014     0.005

[c]2*     $(\exists, \land)$     3     1     0.014     0.042

$(\forall, \lor)$     3     1     0.015     err

[c]2*     $(\exists, \land)$     4     1     0.029     0.063

$(\forall, \lor)$     4     1     0.030     err

[c]2*     $(\exists, \land)$     5     1     0.121     0.242

$(\forall, \lor)$     5     1     0.115     err

[c]2*     $(\exists, \land)$     2     5     0.051     0.022

$(\forall, \lor)$     2     5     0.050     0.028

[c]2*     $(\exists, \land)$     2     5     0.094     0.042

$(\forall, \lor)$     2     5     0.093     0.052

[c]2*     $(\exists, \land)$     2     5     0.154     0.073

$(\forall, \lor)$     2     5     0.156     0.089

[c]2*     $(\exists, \land)$     3     2     0.013     0.037

$(\forall, \lor)$     3     2     0.013     0.037

[c]2*     $(\exists, \land)$     4     2     0.020     0.082

$(\forall, \lor)$     4     2     0.020     0.081

[c]2*     $(\exists, \land)$     5     2     0.063     0.321

$(\forall, \lor)$     5     2     0.067     0.318

[c]2*     $(\exists, \land)$     2     3     0.016     0.036

$(\forall, \lor)$     2     3     0.017     0.020

[c]2*     $(\exists, \land)$     2     3     0.069     0.773

$(\forall, \lor)$     2     3     0.070     0.224

[c]2*     $(\exists, \land)$     3     1     0.014     0.036

$(\forall, \lor)$     3     1     0.014     0.035

[c]2*     $(\exists, \land)$     3     1     0.070     0.437

$(\forall, \lor)$     3     1     0.068     0.368

Storm runtimes

Sizes of witnessing subsystems. Recall that in our experiments we have considered queries with $5$ different bounds for the consensus and firewire models. More specifically, for firewire we consider the labels and queries:

* $\exists \scheduler \in \schedulers \centerdot \prob^\scheduler(\eventually \texttt{"done1"}) \geq \lambda \land \prob^\scheduler(\eventually \texttt{"done2"}) \geq \lambda$

* $\forall \scheduler \in \schedulers \centerdot \prob^\scheduler(\eventually \texttt{"done1"}) \geq \lambda \lor \prob^\scheduler(\eventually \texttt{"done2"}) \geq \lambda$

where $\lambda \in \{0.01, 0.1325, 0.255, 0.3775, 0.5\}$. For consensus, we consider the labels and queries:

* $\exists \scheduler \in \schedulers \centerdot \prob^\scheduler(\eventually \texttt{"finish1"}) \geq \lambda \land \prob^\scheduler(\eventually \texttt{"finish2"}) \geq \lambda$

* $\forall \scheduler \in \schedulers \centerdot \prob^\scheduler(\eventually \texttt{"finish1"}) \geq \lambda \lor \prob^\scheduler(\eventually \texttt{"finish2"}) \geq \lambda$

where $\lambda \in \{0.05, 0.1125, 0.175, 0.2375, 0.3\}$.
Our implementation computes the witnessing subsystems for theses queries using our MILP approach and returns the best solution that has been found after the time limit. The sizes of the subsystems (relative to the original MDP) are shown in <Ref> and <Ref>. We observe that the subsystems for -queries are significantly larger than for -queries. Additionally, the bound $\lambda$ has a significant influence on the size, particularly for -queries.

Sizes of witnessing subsystems (relative to original MDP) for firewire.

Sizes of witnessing subsystems (relative to original MDP) for consensus.

Certification of dual queries. In our experiments, we consider queries that are satisfied and, thus, for which certificates exist. We also investigate the time it takes for the solver to determine that no certificate exists for the dual query, e.g. for a satisfied -query $\query$ we measure the time it takes for the tool to conclude that no certificates exist for the -query $\neg \query$. The results are shown in <Ref>. The column  describes the time for building the model for the dual. The column  describes the time for concluding that no certificate exists for the dual query. The column  describes the total time of  and . We observe that the time for determining that no certificate exists seems to be slightly faster than the time for computing the certificate.

Model     $\card{\states}$     $\card{\SA}$     Type     $k$     #     mean     mean     mean     mean     mean

[c]2*     [c]2*400     [c]2*592     $(\exists,\land)$     2     5     0.250     0.086     0.012     0.008     0.021

$(\forall,\lor)$     2     5     0.199     0.085     0.005     0.003     0.007

[c]2*     [c]2*528     [c]2*784     $(\exists,\land)$     2     5     0.347     0.112     0.024     0.015     0.039

$(\forall,\lor)$     2     5     0.264     0.112     0.019     0.005     0.025

[c]2*     [c]2*656     [c]2*976     $(\exists,\land)$     2     5     0.424     0.144     0.017     0.021     0.038

$(\forall,\lor)$     2     5     0.326     0.140     0.012     0.006     0.018

[c]2*     [c]2*410     [c]2*913     $(\exists,\land)$     3     1     0.229     0.094     0.024     0.003     0.026

$(\forall,\lor)$     3     1     0.158     0.092     0.024     0.002     0.026

[c]2*     [c]2*2115     [c]2*5749     $(\exists,\land)$     4     1     1.529     0.714     0.038     0.007     0.045

$(\forall,\lor)$     4     1     0.944     0.701     0.029     0.042     0.071

[c]2*     [c]2*10610     [c]2*33493     $(\exists,\land)$     5     1     13.544     7.866     0.063     0.057     0.120

$(\forall,\lor)$     5     1     8.859     7.793     0.058     0.078     0.137

[c]2*     [c]2*4093     [c]2*5519     $(\exists,\land)$     2     5     2.454     0.782     0.033     0.034     0.068

$(\forall,\lor)$     2     5     1.996     0.792     0.078     0.026     0.105

[c]2*     [c]2*8618     [c]2*12948     $(\exists,\land)$     2     5     6.045     1.724     0.044     0.061     0.105

$(\forall,\lor)$     2     5     4.463     1.723     0.218     0.068     0.287

[c]2*     [c]2*14727     [c]2*24229     $(\exists,\land)$     2     5     12.353     3.262     0.073     0.105     0.178

$(\forall,\lor)$     2     5     8.317     3.277     0.506     0.093     0.599

Runtimes for concluding non-existence of dual certificates.