\operatorname{\mathit{recall}}_{\mathcal{M}}^{\mathfrak{T}}(\mathsf{Cause})&=&\frac{y}{y+q}&&\mathit{covrat}_{\mathcal{M}}^{\mathfrak{S}}(\mathsf{Cause})&=&\frac{y}{q}\end{array}$

where $x\geqslant y$ (and $q=\mathsf{fn}^{\mathfrak{S}}$). Considering
$\mathfrak{T}$ as a scheduler of $\mathcal{M}$ and of
$\mathcal{M}_{[\mathsf{Cause}]}$, we get:

$\begin{array}[]{rcccl}\operatorname{\mathit{recall}}_{\mathcal{M}}^{\mathfrak{S}}(\mathsf{Cause})&\geqslant&\operatorname{\mathit{recall}}_{\mathcal{M}}^{\mathfrak{T}}(\mathsf{Cause})&=&\operatorname{\mathit{recall}}_{\mathcal{M}_{[\mathsf{Cause}]}}^{\mathfrak{T}}(\mathsf{Cause})\\\
\mathit{covrat}_{\mathcal{M}}^{\mathfrak{S}}(\mathsf{Cause})&\geqslant&\mathit{covrat}_{\mathcal{M}}^{\mathfrak{T}}(\mathsf{Cause})&=&\mathit{covrat}_{\mathcal{M}_{[\mathsf{Cause}]}}^{\mathfrak{T}}(\mathsf{Cause})\end{array}$

This implies:

$\begin{array}[]{rcl}\operatorname{\mathit{recall}}_{\mathcal{M}}^{\mathfrak{S}}(\mathsf{Cause})&\
\geqslant&\operatorname{\mathit{recall}}_{\mathcal{M}_{[\mathsf{Cause}]}}(\mathsf{Cause})\\\
\mathit{covrat}_{\mathcal{M}}(\mathsf{Cause})&\geqslant&\mathit{covrat}_{\mathcal{M}_{[\mathsf{Cause}]}}(\mathsf{Cause})\end{array}$

With similar arguments we get:

$\begin{array}[]{rcccl}\operatorname{\mathit{precision}}_{\mathcal{M}}^{\mathfrak{S}}(\mathsf{Cause})&\geqslant&\operatorname{\mathit{precision}}_{\mathcal{M}}^{\mathfrak{T}}(\mathsf{Cause})&=&\operatorname{\mathit{precision}}_{\mathcal{M}_{[\mathsf{Cause}]}}^{\mathfrak{T}}(\mathsf{Cause})\end{array}$

As the harmonic mean viewed as a function
$f:\mathbb{R}_{>0}^{2}\to\mathbb{R}$, $f(x,y)=2\frac{xy}{x{+}y}$ is
monotonically increasing in both arguments (note that
$\frac{df}{dx}=\frac{y^{2}}{(x{+}y)^{2}}>0$ and
$\frac{df}{dy}=\frac{x^{2}}{(x{+}y)^{2}}>0$), we obtain:

$\mathit{fscore}_{\mathcal{M}}^{\mathfrak{S}}(\mathsf{Cause})\ \geqslant\
\mathit{fscore}_{\mathcal{M}}^{\mathfrak{T}}(\mathsf{Cause})\ =\
\mathit{fscore}_{\mathcal{M}_{[\mathsf{Cause}]}}^{\mathfrak{T}}(\mathsf{Cause})$

This yields
$\mathit{fscore}_{\mathcal{M}}(\mathsf{Cause})\geqslant\mathit{fscore}_{\mathcal{M}_{[\mathsf{Cause}]}}(\mathsf{Cause})$.

######  Lemma 29.

Let $\mathcal{N}$ be the MEC-quotient of $\mathcal{M}_{[\mathsf{Cause}]}$ for
some MDP $\mathcal{M}$ with a set of terminal states $\mathsf{Eff}$ and an SPR
or a GPR cause $\mathsf{Cause}$. Then:

$\operatorname{\mathit{recall}}_{\mathcal{M}_{[\mathsf{Cause}]}}(\mathsf{Cause})$ | = | $\operatorname{\mathit{recall}}_{\mathcal{N}}(\mathsf{Cause})$
---|---|---
$\mathit{covrat}_{\mathcal{M}_{[\mathsf{Cause}]}}(\mathsf{Cause})$ | = | $\mathit{covrat}_{\mathcal{N}}(\mathsf{Cause})$
$\mathit{fscore}_{\mathcal{M}_{[\mathsf{Cause}]}}(\mathsf{Cause})$ | = | $\mathit{fscore}_{\mathcal{N}}(\mathsf{Cause})$

######  Proof 5.2.

Analogously to the proof of Lemma 19.

This now allows us to work under assumptions (A1)-(A3) when addressing
problems concerning the quality measures for a fixed cause set.

As efficient computation methods for
$\operatorname{\mathit{recall}}(\mathsf{Cause})$ are known from literature
(see [BKKM14, Mär20] for poly-time algorithms to compute conditional
reachability probabilities), we can use the same methods to compute the
coverage ratio.

######  Corollary 30.

The value $\mathit{covrat}(\mathsf{Cause})$ and corresponding worst-case
schedulers are computable in polynomial time.

######  Proof 5.3.

For a given scheduler $\mathfrak{S}$ we have

$\displaystyle\mathit{covrat}^{\mathfrak{S}}(\mathsf{Cause})=\frac{\mathsf{tp}^{\mathfrak{S}}}{\mathsf{fn}^{\mathfrak{S}}}\
\ \text{and}\ \
\operatorname{\mathit{recall}}^{\mathfrak{S}}(\mathsf{Cause})=\frac{\mathsf{tp}^{\mathfrak{S}}}{\mathsf{tp}^{\mathfrak{S}}+\mathsf{fn}^{\mathfrak{S}}}$

We thus get the following

$\displaystyle\frac{1}{\frac{\mathsf{tp}^{\mathfrak{S}}}{\mathsf{tp}^{\mathfrak{S}}+\mathsf{fn}^{\mathfrak{S}}}}$
$\displaystyle=\frac{\mathsf{tp}^{\mathfrak{S}}+\mathsf{fn}^{\mathfrak{S}}}{\mathsf{tp}^{\mathfrak{S}}}=\frac{\mathsf{tp}^{\mathfrak{S}}}{\mathsf{tp}^{\mathfrak{S}}}+\frac{\mathsf{fn}^{\mathfrak{S}}}{\mathsf{tp}^{\mathfrak{S}}}=1+\frac{\mathsf{fn}^{\mathfrak{S}}}{\mathsf{tp}^{\mathfrak{S}}}=1+\frac{1}{\frac{\mathsf{tp}^{\mathfrak{S}}}{\mathsf{fn}^{\mathfrak{S}}}}.$

This implies

$\displaystyle\frac{1}{\operatorname{\mathit{recall}}^{\mathfrak{S}}(\mathsf{Cause})}=1+\frac{1}{\mathit{covrat}^{\mathfrak{S}}(\mathsf{Cause})}\
\ \text{and thus}\ \
\mathit{covrat}^{\mathfrak{S}}(\mathsf{Cause})=1/\left(\frac{1}{\operatorname{\mathit{recall}}^{\mathfrak{S}}(\mathsf{Cause})}-1\right)$

Computing $\mathit{covrat}(\mathsf{Cause})$ now implores us to take the
infimum of all sensible schedulers over
$1/\left(\frac{1}{\operatorname{\mathit{recall}}^{\mathfrak{S}}(\mathsf{Cause})}-1\right)$
which is the same as taking the infimum of all sensible schedulers over
$\operatorname{\mathit{recall}}^{\mathfrak{S}}(\mathsf{Cause})$. This amounts
to computing

$\displaystyle\inf_{\mathfrak{S}}\operatorname{\mathit{recall}}^{\mathfrak{S}}(\mathsf{Cause})=\mathrm{Pr}_{\mathcal{M}}^{\min}(\
\lozenge\mathsf{Cause}\mid\lozenge\mathsf{Eff}\ ),$

which can be computed in polynomial time by [BKKM14, Mär20].

In contrast to these results, we are not aware of known concepts that are
applicable for computing the f-score. Indeed, this quality measure is
efficiently computable:

######  Theorem 31.

The value $\mathit{fscore}(\mathsf{Cause})$ and corresponding worst-case
schedulers are computable in polynomial time.

The remainder of this subsection is devoted to the proof of Theorem 31. We can
express $\mathit{fscore}(\mathsf{Cause})$ in terms of the supremum of a
quotient of reachability probabilities for disjoint sets of terminal states.
More precisely, under assumptions (A1)-(A3) and assuming
$\mathit{fscore}(\mathsf{Cause})>0$, we have:

$\mathit{fscore}(\mathsf{Cause})=\frac{2}{X+2}\quad\text{where}\quad X\ =\
\sup_{\mathfrak{S}}\,\frac{\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{noeff}_{\mathsf{fp}})+\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{eff}_{\mathsf{unc}})}{\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{eff}_{\mathsf{cov}})}$

where $\mathfrak{S}$ ranges over all schedulers with
$\mathrm{Pr}_{\mathcal{M}}^{\mathfrak{S}}(\Diamond\mathsf{eff}_{\mathsf{cov}})>0$.
Moreover, we have

######  Lemma 32.

Let $\mathsf{Cause}$ be an SPR or a GPR cause. Then, the following three
statements are equivalent:

  1. (a)

$\operatorname{\mathit{recall}}(\mathsf{Cause})=0$

  2. (b)

$\mathit{fscore}(\mathsf{Cause})=0$

  3. (c)

There is a scheduler $\mathfrak{S}$ such that
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{Eff})>0$ and
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{Cause})=0$.

######  Proof 5.4.

Let $C=\mathsf{Cause}$. Using results of [BKKM14, Mär20], there exist
schedulers $\mathfrak{T}$ and $\mathfrak{U}$ with

  * •

$\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{M}}(\Diamond\mathsf{Eff})>0$ and
$\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{M}}(\ \Diamond C\ |\Diamond\mathsf{Eff}\
)=\inf_{\mathfrak{S}}\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\ \Diamond C\
|\Diamond\mathsf{Eff}\ )$ where $\mathfrak{S}$ ranges over all schedulers with
positive effect probability,

  * •

$\mathrm{Pr}^{\mathfrak{U}}_{\mathcal{M}}(\Diamond C)>0$ and
$\mathrm{Pr}^{\mathfrak{U}}_{\mathcal{M}}(\ \Diamond\mathsf{Eff}\ |\Diamond C\
)=\inf_{\mathfrak{S}}\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\
\Diamond\mathsf{Eff}\ |\Diamond C\ )$ where $\mathfrak{S}$ ranges over all
schedulers with $\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond C)>0$.

In particular,
$\operatorname{\mathit{recall}}(C)=\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{M}}(\
\Diamond C\ |\Diamond\mathsf{Eff}\ )$ and
$\operatorname{\mathit{precision}}(C)=\mathrm{Pr}^{\mathfrak{U}}_{\mathcal{M}}(\
\Diamond\mathsf{Eff}\ |\Diamond C\ )$. By (GPR) applied to $\mathfrak{U}$ and
$\mathfrak{T}$ (recall that each SPR cause is a GPR cause too, see Lemma 5),
we obtain the following statements (i) and (ii):

(i):

$p\ \stackrel{{\scriptstyle\text{\rm\tiny def}}}{{=}}\
\operatorname{\mathit{precision}}(C)\ >\ 0$

(ii):

If $\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{M}}(\Diamond C)>0$ then
$\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{M}}(\Diamond
C\wedge\Diamond\mathsf{Eff})>0$ and therefore
$\operatorname{\mathit{recall}}(C)>0$.

Obviously, if there is no scheduler $\mathfrak{S}$ as in statement (c) then
$\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{M}}(\Diamond C)>0$. Hence, as a
consequence of (ii) we obtain:

(iii):

If there is no scheduler $\mathfrak{S}$ as in statement (c) then
$\operatorname{\mathit{recall}}(C)>0$.

“(a) $\Longrightarrow$ (b)”: We prove $\mathit{fscore}(C)>0$ implies
$\operatorname{\mathit{recall}}(C)>0$. If $\mathit{fscore}(C)>0$ then, by
definition of the f-score, there is no scheduler $\mathfrak{S}$ as in
statement (c). But then $\operatorname{\mathit{recall}}(C)>0$ by statement
(iii).

“(b) $\Longrightarrow$ (c)”: Let $\mathit{fscore}(C)=0$. Suppose by
contradiction that there is no scheduler as in (c). Again by (iii) we obtain
$\operatorname{\mathit{recall}}(C)>0$. But then, for each scheduler
$\mathfrak{S}$ with $\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond C)>0$:

$\operatorname{\mathit{precision}}^{\mathfrak{S}}(C)\ \geqslant\ p\
\stackrel{{\scriptstyle\text{\tiny(i)}}}{{>}}\ 0$

and, with $r\stackrel{{\scriptstyle\text{\rm\tiny
def}}}{{=}}\operatorname{\mathit{recall}}(C)$:

$\operatorname{\mathit{recall}}^{\mathfrak{S}}(C)\ \geqslant\ r\ >\ 0$

The harmonic mean as a function $]0,1]^{2}\to\mathbb{R}$, $(x,y)\mapsto
2\frac{xy}{x+y}$ is monotonically increasing in both arguments. But then:

$\mathit{fscore}^{\mathfrak{S}}(C)\ \geqslant\ 2\frac{p\cdot r}{p{+}r}\ >\ 0$

Hence,
$\mathit{fscore}(C)=\inf_{\mathfrak{S}}\mathit{fscore}^{\mathfrak{S}}(C)\geqslant
2\frac{p\cdot r}{p{+}r}>0$. Contradiction.

“(c) $\Longrightarrow$ (a)”: Let $\mathfrak{S}$ be a scheduler as in statement
(c). Then,

$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\ \Diamond C\ |\Diamond\mathsf{Eff}\
)\ =\ 0.$

Hence: $\operatorname{\mathit{recall}}(C)\ =\
\mathrm{Pr}^{\min}_{\mathcal{M}}(\ \Diamond C\ |\Diamond\mathsf{Eff}\ )\ =\
0$.

The remaining task to prove Theorem 31 is a generally applicable technique for
computing extremal ratios of reachability probabilities in MDPs without ECs.

##### Max/min ratios of reachability probabilities for disjoint sets of
terminal states.

Suppose we are given an MDP $\mathcal{M}=(S,\mathit{Act},P,\mathsf{init})$
without ECs and disjoint subsets $U,V\subseteq S$ of terminal states. Given a
scheduler $\mathfrak{S}$ with
$\mathrm{Pr}_{\mathcal{M}}^{\mathfrak{S}}(\Diamond V)>0$ we define:

$\displaystyle\mathfrak{S}/\mathcal{M}{U,V}\ =\
\frac{\mathrm{Pr}_{\mathcal{M}}^{\mathfrak{S}}(\Diamond
U)}{\mathrm{Pr}_{\mathcal{M}}^{\mathfrak{S}}(\Diamond V)}$

The goal is an algorithm for computing the extremal values:

$\displaystyle\min/\mathcal{M}{U,V}=\inf_{\mathfrak{S}}\mathfrak{S}/\mathcal{M}{U,V}\quad\text{and}\quad\max/\mathcal{M}{U,V}=\sup_{\mathfrak{S}}\mathfrak{S}/\mathcal{M}{U,V}$

where $\mathfrak{S}$ ranges over all schedulers with
$\mathrm{Pr}_{\mathcal{M}}^{\mathfrak{S}}(\Diamond V)>0$. To compute these, we
rely on a polynomial reduction to the classical _stochastic shortest path
problem_ [BT91]. For this, consider the MDP $\mathcal{N}$ arising from
$\mathcal{M}$ by adding reset transitions from all terminal states $t\in
S\backslash V$ to $\mathsf{init}$. Thus, exactly the $V$-states are terminal
in $\mathcal{N}$. $\mathcal{N}$ might contain ECs, which, however, do not
intersect with $V$. We equip $\mathcal{N}$ with the weight function that
assigns $1$ to all states in $U$ and $0$ to all other states. For a scheduler
$\mathfrak{T}$ with $\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{N}}(\Diamond V)=1$,
let $\mathrm{E}^{\mathfrak{T}}_{\mathcal{N}}(\boxplus V)$ be the expected
accumulated weight until reaching $V$ under $\mathfrak{T}$. Let
$\mathrm{E}^{\min}_{\mathcal{N}}(\boxplus
V)=\inf_{\mathfrak{T}}\mathrm{E}^{\mathfrak{T}}_{\mathcal{N}}(\boxplus V)$ and
$\mathrm{E}^{\max}_{\mathcal{N}}(\boxplus
V)=\sup_{\mathfrak{T}}\mathrm{E}^{\mathfrak{T}}_{\mathcal{N}}(\boxplus V)$,
where $\mathfrak{T}$ ranges over all schedulers with
$\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{N}}(\Diamond V)=1$. We can rely on known
results [BT91, dA99, BBD+18] to obtain that both
$\mathrm{E}^{\min}_{\mathcal{N}}(\boxplus V)$ and
$\mathrm{E}^{\max}_{\mathcal{N}}(\boxplus V)$ are computable in polynomial
time. As $\mathcal{N}$ has only non-negative weights,
$\mathrm{E}^{\min}_{\mathcal{N}}(\boxplus V)$ is finite and a corresponding
MD-scheduler with minimal expectation exists. If $\mathcal{N}$ has an EC
containing at least one $U$-state, which is the case iff $\mathcal{M}$ has a
scheduler $\mathfrak{S}$ with
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond U)>0$ and
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond V)=0$, then
$\mathrm{E}^{\max}_{\mathcal{N}}(\boxplus V)=+\infty$. Otherwise,
$\mathrm{E}^{\max}_{\mathcal{N}}(\boxplus V)$ is finite and the maximum is
achieved by an MD-scheduler as well.

######  Theorem 33.

Let $\mathcal{M}$ be an MDP without ECs and $U,V$ disjoint sets of terminal
states in $\mathcal{M}$, and let $\mathcal{N}$ be as before. Then,
$\min/\mathcal{M}{U,V}=\mathrm{E}^{\min}_{\mathcal{N}}(\boxplus V)$ and
$\max/\mathcal{M}{U,V}=\mathrm{E}^{\max}_{\mathcal{N}}(\boxplus V)$. Thus,
both values are computable in polynomial time, and there is an MD-scheduler
minimizing $\mathfrak{S}/\mathcal{M}{U,V}$, and an MD-scheduler maximizing
$\mathfrak{S}/\mathcal{M}{U,V}$ if $\max/\mathcal{M}{U,V}$ is finite.

$\mathsf{init}$$\mathsf{eff}_{\mathsf{unc}}$$c$$\mathsf{noeff}$$\mathsf{eff}_{\mathsf{cov}}$$1/2$$1/2$$1/2$$1/2$$1/2$$\alpha$$\beta$$1/2$

Figure 8. MDP $\mathcal{M}$ from Example 5.2

$\mathsf{init}$$\mathsf{eff}_{\mathsf{unc}}$$c$$\mathsf{noeff}$$\mathsf{eff}_{\mathsf{cov}}$$1/2$$1/2$$1/2$$1/2$$1/2$$\alpha$$\beta$$1/2$

Figure 9. MDP $\mathcal{N}$ with reset transitions for
$\min/\mathcal{M}{\mathsf{eff}_{\mathsf{cov}},\mathsf{eff}_{\mathsf{unc}}}$

Consider the MDP $\mathcal{M}$ from Figure 9 with
$\mathsf{Eff}=\\{\mathsf{eff}_{\mathsf{unc}},\mathsf{eff}_{\mathsf{cov}}\\}$
and suppose the task is to compute
$\mathit{covrat}(c)=\min/\mathcal{M}{\mathsf{eff}_{\mathsf{cov}},\mathsf{eff}_{\mathsf{unc}}}$.
The construction for the algorithm is depicted in Figure 9 resulting in
$\mathcal{N}$, where reset transitions for $\mathsf{noeff}$ and
$\mathsf{eff}_{\mathsf{cov}}$ have been added (red edges) and
$\mathsf{eff}_{\mathsf{unc}}$ is the only terminal state. The weight function
now assigns $1$ to $\mathsf{eff}_{\mathsf{cov}}$ and $0$ to all others. By
Theorem 33 we have

$\displaystyle\mathit{covrat}(c)=\min/\mathcal{M}{\mathsf{eff}_{\mathsf{cov}},\mathsf{eff}_{\mathsf{unc}}}=\mathrm{E}^{\min}_{\mathcal{N}}(\boxplus\mathsf{eff}_{\mathsf{unc}}).$

######  Proof 5.5 (Proof of Theorem 33).

$\mathcal{M}$ has a scheduler $\mathfrak{S}$ with
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond U)>0$ and
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond V)=0$ if and only if the
transformed MDP $\mathcal{N}$ in Section 5.2 (Max/min ratios of reachability
probabilities for disjoint sets of terminal states) has an EC containing at
least one $U$-state. Therefore we then have
$\mathrm{E}^{\max}_{\mathcal{N}}(\boxplus V)=+\infty.$ Otherwise,
$\mathrm{E}^{\max}_{\mathcal{N}}(\boxplus
V)=1/\mathrm{E}^{\min}_{\mathcal{N}}(\boxplus V).$

For the following we only consider
$\min/\mathcal{M}{U,V}=\mathrm{E}^{\min}_{\mathcal{N}}(\boxplus V)$ since the
arguments for the maximum are similar. First we show
$\min/\mathcal{M}{U,V}\leqslant\mathrm{E}^{\min}_{\mathcal{N}}(\boxplus V)$.
For this, we consider an arbitrary scheduler $\mathfrak{S}$ for $\mathcal{M}$.
Let

$\displaystyle x$
$\displaystyle=\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond U)$
$\displaystyle p$
$\displaystyle=\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond V)$
$\displaystyle q$ $\displaystyle=1-x-p$

For $p>0$ we have

$\frac{\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond
U)}{\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond V)}\ \ =\ \ \frac{x}{p}$

Let $\mathfrak{T}$ be the scheduler that behaves as $\mathfrak{S}$ in the
first round and after each reset. Then:

$\displaystyle\mathrm{E}^{\mathfrak{T}}_{\mathcal{N}}(\boxplus V)\ \ =\ \
\sum_{n=0}^{\infty}\sum_{k=0}^{\infty}n\cdot
x^{n}\cdot\left(\\!\\!\\!\begin{array}[]{c}n{+}k\\\
k\end{array}\\!\\!\\!\right)q^{k}\cdot p\ \
\stackrel{{\scriptstyle\text{\eqref{second basic}}}}{{=}}\ \ \frac{x}{p}$ (10)

where (13) relies on some basic calculations (see Lemma 34). This yields:

$\mathfrak{S}/\mathcal{M}{U,V}\ =\ \frac{x}{p}\ =\
\mathrm{E}^{\mathfrak{T}}_{\mathcal{N}}(\boxplus V)\ \geqslant\
\mathrm{E}^{\min}_{\mathcal{N}}(\boxplus V)$

Hence, $\min/\mathcal{M}{U,V}\geqslant\mathrm{E}^{\min}_{\mathcal{N}}(\boxplus
V)$.

For the other direction $\mathrm{E}^{\min}_{\mathcal{N}}(\boxplus
V)\geqslant\min/\mathcal{M}{U,V}$, we use the fact that there is an MD-
scheduler $\mathfrak{T}$ for $\mathcal{N}$ such that
$\mathrm{E}^{\mathfrak{T}}_{\mathcal{N}}(\boxplus
V)=\mathrm{E}^{\min}_{\mathcal{N}}(\boxplus V)$. $\mathfrak{T}$ can be viewed
as an MD-scheduler for the original MDP $\mathcal{M}$. Again we can rely on
(10) to obtain that:

$\mathrm{E}^{\mathfrak{T}}_{\mathcal{N}}(\boxplus V)\ \ =\ \
\frac{\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{M}}\bigl{(}\Diamond
U\bigr{)}}{\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{M}}\bigl{(}\Diamond
V\bigr{)}}\ \ =\ \ \mathfrak{T}/\mathcal{M}{U,V}\ \ \geqslant\ \
\min/\mathcal{M}{U,V}$

But this yields $\mathrm{E}^{\min}_{\mathcal{N}}(\boxplus V)\ \geqslant\
\min/\mathcal{M}{U,V}$. we can now rely on known results [BT91, dA99, BBD+18]
to compute $\mathrm{E}^{\min}_{\mathcal{N}}(\boxplus V)$ and
$\mathrm{E}^{\max}_{\mathcal{N}}(\boxplus V)$ in polynomial time.

######  Lemma 34.

Let $x,p,q\in[0,1]$ such that $x{+}q{+}p=1$. Then:

$\displaystyle\sum_{n=0}^{\infty}\sum_{k=0}^{\infty}n\cdot
x^{n}\cdot\left(\\!\\!\\!\begin{array}[]{c}n{+}k\\\
k\end{array}\\!\\!\\!\right)q^{k}\cdot p\ \ =\ \ \frac{x}{p}$ (13)

######  Proof 5.6.

We first show for $0<q<1$, $n\in\mathbb{N}$ and

$\displaystyle a_{n}$ $\displaystyle\stackrel{{\scriptstyle\text{\rm\tiny
def}}}{{=}}$
$\displaystyle\sum_{k=0}^{\infty}\left(\\!\\!\\!\begin{array}[]{c}n{+}k\\\
k\end{array}\\!\\!\\!\right)q^{k},$

we have

$a_{n}=\frac{1}{(1{-}q)^{n+1}}$

This is done by induction on $n$. The claim is clear for $n{=}0$. For the step
of induction we use:

$\left(\\!\\!\\!\begin{array}[]{c}n{+}1{+}k\\\ k\end{array}\\!\\!\\!\right)\ \
=\ \ \left(\\!\\!\\!\begin{array}[]{c}n{+}k\\\ k\end{array}\\!\\!\\!\right)\
+\ \left(\\!\\!\\!\begin{array}[]{c}n{+}k\\\ k{-}1\end{array}\\!\\!\\!\right)\
\ =\ \ \left(\\!\\!\\!\begin{array}[]{c}n{+}k\\\ k\end{array}\\!\\!\\!\right)\
+\ \left(\\!\\!\\!\begin{array}[]{c}(n{+}1)+(k{-}1)\\\
k{-}1\end{array}\\!\\!\\!\right)$

But this yields $a_{n+1}=a_{n}+q\cdot a_{n+1}$. Hence:

$a_{n+1}\ =\ \frac{a_{n}}{1{-}q}$

The claim then follows directly from the induction hypothesis.

The statement of Lemma 34 now follows by some calculations and the preliminary
induction.

$\displaystyle\sum_{n=0}^{\infty}\sum_{k=0}^{\infty}n\cdot
x^{n}\cdot\left(\\!\\!\\!\begin{array}[]{c}n{+}k\\\
k\end{array}\\!\\!\\!\right)q^{k}\cdot p$ $\displaystyle=$
$\displaystyle\sum_{n=0}^{\infty}n\cdot x^{n}\cdot\frac{1}{(1{-}q)^{n+1}}\cdot
p$ $\displaystyle=$
$\displaystyle\frac{p}{1{-}q}\cdot\sum_{n=0}^{\infty}n\cdot\left(\frac{x}{1{-}q}\right)^{n}$
$\displaystyle=$
$\displaystyle\frac{p}{1{-}q}\cdot\frac{\displaystyle\frac{x}{1{-}q}}{\displaystyle\
\Bigl{(}1-\frac{x}{1{-}q}\Bigr{)}^{2}\ }$ $\displaystyle=$
$\displaystyle\frac{px}{(1{-}q{-}x)^{2}}\ \ \ =\ \ \ \frac{px}{p^{2}}\ \ \ =\
\ \ \frac{x}{p}$

where we use $p=1{-}q{-}x$.

Applying this framework for $\max/\mathcal{M}{U,V}$ to the f-score we now
proof Theorem 31.

######  Proof 5.7 (Proof of Theorem 31).

We use the simplifying assumptions (A1)-(A3) that can be made due to Lemmata
28 and 29. For $\mathit{fscore}(\mathsf{Cause})$ we have after some straight-
forward transformations

$\displaystyle\mathit{fscore}^{\mathfrak{S}}(\mathsf{Cause})$
$\displaystyle=\frac{2\mathsf{tp}^{\mathfrak{S}}}{2\mathsf{tp}^{\mathfrak{S}}+\mathsf{fn}^{\mathfrak{S}}+\mathsf{fp}^{\mathfrak{S}}}.$

Using this we get

$\displaystyle\frac{2}{\mathit{fscore}^{\mathfrak{S}}(\mathsf{Cause})}-2$
$\displaystyle=\frac{\mathsf{fp}^{\mathfrak{S}}+\mathsf{fn}^{\mathfrak{S}}}{\mathsf{tp}^{\mathfrak{S}}}=\frac{\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{noeff}_{\mathsf{fp}})+\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{eff}_{\mathsf{unc}})}{\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{eff}_{\mathsf{cov}})}$

Thus, the task is to compute

$X=\sup_{\mathfrak{S}}\frac{2}{\mathit{fscore}^{\mathfrak{S}}(\mathsf{Cause})}-2=\sup_{\mathfrak{S}}\frac{\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{noeff}_{\mathsf{fp}})+\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{eff}_{\mathsf{unc}})}{\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{eff}_{\mathsf{cov}})},$

where $\mathfrak{S}$ ranges over all schedulers with
$\mathrm{Pr}_{\mathcal{M}}^{\mathfrak{S}}(\Diamond\mathsf{eff}_{\mathsf{cov}})>0$.
We have

$\mathit{fscore}(\mathsf{Cause})=\frac{2}{X+2}.$

But $X$ can be expressed as a supremum in the form of Theorem 33. This yields
the claim that the optimal value is computable in polynomial time.

In case $\mathit{fscore}(\mathsf{Cause})=0$, we do not obtain an optimal
scheduler via Theorem 33. Lemma 32, however, shows that there is a scheduler
$\mathfrak{S}$ with
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{Eff})>0$ and
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{Cause})=0$. Such a
scheduler can be computed in polynomial time as any (memoryless) scheduler in
the largest sub-MDP of $\mathcal{M}$ that does not contain states in
$\mathsf{Cause}$. (This sub-MDP can be constructed by successively removing
states and state-action pairs.)

###  5.3. Quality-optimal probability-raising causes

For the computation there is no difference between GPR and SPR causes as only
the quality properties of the set are in question. However, when finding
optimal causes the distinction makes a difference. Here, we say an SPR cause
$\mathsf{Cause}$ is _recall-optimal_ if
$\operatorname{\mathit{recall}}(\mathsf{Cause})=\max_{C}\operatorname{\mathit{recall}}(C)$
where $C$ ranges over all SPR causes. Likewise, _ratio-optimality_ resp. _f-
score-optimality_ of $\mathsf{Cause}$ means maximality of
$\mathit{covrat}(\mathsf{Cause})$ resp. $\mathit{fscore}(\mathsf{Cause})$
among all SPR causes. Recall-, ratio- and f-score-optimality for GPR causes
are defined accordingly.

######  Lemma 35.

Let $\mathsf{Cause}$ be an SPR or a GPR cause. Then, $\mathsf{Cause}$ is
recall-optimal if and only if $\mathsf{Cause}$ is ratio-optimal.

######  Proof 5.8.

Essentially the proof uses the same connection between
$\operatorname{\mathit{recall}}$ and $\mathit{covrat}$ as Corollary 30. Here
we do not assume (A1)-(A3). However, for each scheduler $\mathfrak{S}$ and
each set $C$ of states we have:

$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{Eff})\ =\
\mathsf{fn}^{\mathfrak{S}}_{C}+\mathsf{tp}^{\mathfrak{S}}_{C}$

where
$\mathsf{fn}^{\mathfrak{S}}_{C}=\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}\bigl{(}(\neg\lozenge
C)\wedge\lozenge\mathsf{Eff}\bigr{)}$ and
$\mathsf{tp}^{\mathfrak{S}}_{C}=\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}\bigl{(}\Diamond(C\wedge\Diamond\mathsf{Eff})\bigr{)}$.
If $C$ is a cause where $\mathsf{fn}^{\mathfrak{S}}_{C}$ is positive then

$\mathit{covrat}^{\mathfrak{S}}(C)\ =\
\frac{\mathsf{tp}^{\mathfrak{S}}_{C}}{\mathsf{fn}^{\mathfrak{S}}_{C}}\quad\text{and}\quad\operatorname{\mathit{recall}}^{\mathfrak{S}}(C)\
=\
\frac{\mathsf{tp}^{\mathfrak{S}}_{C}}{\mathsf{fn}^{\mathfrak{S}}_{C}+\mathsf{tp}^{\mathfrak{S}}_{C}}$

For all non-negative reals $p,q,p^{\prime},q^{\prime}$ where $q,q^{\prime}>0$
we have:

$\frac{p}{q}<\frac{p^{\prime}}{q^{\prime}}\qquad\text{iff}\qquad\frac{p}{p+q}<\frac{p^{\prime}}{p^{\prime}+q^{\prime}}$

Hence, if $C$ is fixed and $\mathfrak{S}$ ranges over all schedulers with
$\mathsf{tp}_{C}^{\mathfrak{S}}>0$:

$\frac{\mathsf{tp}^{\mathfrak{S}}_{C}}{\mathsf{fn}^{\mathfrak{S}}_{C}}$ is
minimal iff
$\frac{\mathsf{tp}^{\mathfrak{S}}_{C}}{\mathsf{fn}^{\mathfrak{S}}_{C}+\mathsf{tp}^{\mathfrak{S}}_{C}}$
is minimal

Thus, if $C$ is fixed and $\mathfrak{S}=\mathfrak{S}_{C}$ is a scheduler
achieving the worst-case (i.e., minimal) coverage ratio for $C$ then
$\mathfrak{S}$ achieves the minimal recall for $C$, and vice versa.

Let now $\mathsf{fn}_{C}=\mathsf{fn}_{C}^{\mathfrak{S}_{C}}$,
$\mathsf{tp}_{C}=\mathsf{tp}_{C}^{\mathfrak{S}_{C}}$ where $\mathfrak{S}_{C}$
is a scheduler that minimizes the coverage ratio and minimizes the recall for
cause set $C$. Then:

$\mathit{covrat}(C)=\frac{\mathsf{tp}_{C}}{\mathsf{fn}_{C}}$ is maximal iff
$\frac{\mathsf{tp}_{C}}{\mathsf{fn}_{C}+\mathsf{tp}_{C}}$ is maximal iff
$\operatorname{\mathit{recall}}(C)$ is maximal

where the extrema range over all SPR resp. GPR causes $C$. This yields the
claim.

##### Recall- and ratio-optimal SPR causes.

The techniques of Section 4.1 yield an algorithm for generating a canonical
SPR cause with optimal recall and coverage ratio. To see this, let
$\mathcal{C}$ denote the set of all states which constitute a singleton SPR
cause. The canonical cause $\mathsf{CanCause}$ is defined as the set of states
$c\in\mathcal{C}$ such that there is a scheduler $\mathfrak{S}$ with
$\mathrm{Pr}_{\mathcal{M}}^{\mathfrak{S}}((\neg\mathcal{C})\,\mathrm{U}\,c)>0$.
So to speak $\mathsf{CanCause}$ is the “front” of $\mathcal{C}$. Obviously,
$\mathcal{C}$ and $\mathsf{CanCause}$ are computable in polynomial time.

######  Theorem 36.

If $\mathcal{C}\not=\varnothing$ then $\mathsf{CanCause}$ is a ratio- and
recall-optimal SPR cause.

######  Proof 5.9.

By definition of SPR causes any subset of $\mathcal{C}$ is a SPR cause and
thus also $\mathsf{CanCause}$. Optimality is a consequence as
$\mathsf{CanCause}$ even yields path-wise optimal coverage in the following
sense. If $C$ is any SPR cause then $C\subseteq\mathcal{C}$ by definition and
for each path $\pi$ in $\mathcal{M}$:

$\displaystyle\pi\models(\neg\lozenge\mathsf{CanCause})\wedge\lozenge\mathsf{Eff}$
$\displaystyle\implies\pi\models(\neg\lozenge
C)\wedge\lozenge\mathsf{Eff}\text{ and}$
$\displaystyle\pi\models\Diamond(C\wedge\Diamond\mathsf{Eff})$
$\displaystyle\implies\pi\models\Diamond(\mathsf{CanCause}\wedge\Diamond\mathsf{Eff}).$

But then

$\displaystyle\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond(C\wedge\Diamond\mathsf{Eff}))$
$\displaystyle\leqslant\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond(\mathsf{CanCause}\wedge\Diamond\mathsf{Eff})),$
$\displaystyle\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}((\neg\lozenge
C)\wedge\lozenge\mathsf{Eff}))$
$\displaystyle\geqslant\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}((\neg\lozenge\mathsf{CanCause})\wedge\mathsf{Eff})$

for every scheduler $\mathfrak{S}$,which yields the claim.

$\mathsf{init}$$\mathsf{eff}$$\mathsf{noeff}$$s_{1}$$s_{2}$$1/4$$1/4$$1/2$$1/4$$3/4$$1$

Figure 10. Markov chain from Remark 37

######  Remark 37.

It is not true that the canonical SPR cause $\mathsf{CanCause}$ is f-score-
optimal. To see this, Consider the Markov chain from Figure 10. There we have
$\mathsf{CanCause}=\\{s_{1}\\}$, which has
$\operatorname{\mathit{precision}}(\mathsf{CanCause})=\frac{3}{4}$ and
$\operatorname{\mathit{recall}}(\mathsf{CanCause})=\frac{3}{8}/(\frac{1}{4}+\frac{3}{8})=\frac{3}{5}.$
But the SPR cause $\\{s_{2}\\}$ has better f-score as its precision is $1$ and
it has the same recall as $\mathsf{CanCause}$. $\lhd$

##### F-score-optimal SPR cause.

From Section 5.2, we see that f-score-optimal SPR causes in MDPs can be
computed in polynomial space by computing the f-score for all potential SPR
causes one by one in polynomial time (Theorem 31). As the space can be reused
after each computation, this results in polynomial space. For Markov chains,
we can do better and compute an f-score-optimal SPR cause in polynomial time
via a polynomial reduction to the stochastic shortest path problem:

######  Theorem 38.

In Markov chains that have SPR causes, an f-score-optimal SPR cause can be
computed in polynomial time.

######  Proof 5.10.

We regard the given Markov chain $\mathcal{M}$ as an MDP with a singleton
action set $\mathit{Act}=\\{\alpha\\}$. As $\mathcal{M}$ has SPR causes, the
set $\mathcal{C}$ of states that constitute a singleton SPR cause is nonempty.
We may assume that $\mathcal{M}$ has no non-trivial (i.e., cyclic) bottom
strongly connected components as we may collapse them. Let $w_{c}$ $=$
$\mathrm{Pr}_{\mathcal{M},c}(\Diamond\mathsf{Eff})$. We switch from
$\mathcal{M}$ to a new MDP $\mathcal{K}$ with state space
$S_{\mathcal{K}}=S\cup\\{\mathsf{eff}_{\mathsf{cov}},\mathsf{noeff}_{\mathsf{fp}}\\}$
with fresh states $\mathsf{noeff}_{\mathsf{fp}}$ and
$\mathsf{eff}_{\mathsf{cov}}$ and the action set
$\mathit{Act}_{\mathcal{K}}=\\{\alpha,\gamma\\}$. The MDP $\mathcal{K}$ arises
from $\mathcal{M}$ by adding (i) for each state $c\in\mathcal{C}$ a fresh
state-action pair $(c,\gamma)$ with
$P_{\mathcal{K}}(c,\gamma,\mathsf{eff}_{\mathsf{cov}})=w_{c}$ and
$P_{\mathcal{K}}(c,\gamma,\mathsf{noeff}_{\mathsf{fp}})=1{-}w_{c}$ and (ii)
reset transitions to $\mathsf{init}$ with action label $\alpha$ from the new
state $\mathsf{noeff}_{\mathsf{fp}}$ and all terminal states of $\mathcal{M}$,
i.e., $P_{\mathcal{K}}(\mathsf{noeff}_{\mathsf{fp}},\alpha,\mathsf{init})=1$
and $P_{\mathcal{K}}(s,\alpha,\mathsf{init})=1$ for $s\in\mathsf{Eff}$ or if
$s$ is a terminal non-effect state of $\mathcal{M}$. So, exactly
$\mathsf{eff}_{\mathsf{cov}}$ is terminal in $\mathcal{K}$, and
$\mathit{Act}_{\mathcal{K}}(c)=\\{\alpha,\gamma\\}$ for $c\in\mathcal{C}$,
while $\mathit{Act}_{\mathcal{K}}(s)=\\{\alpha\\}$ for all other states $s$.
Intuitively, taking action $\gamma$ in state $c\in\mathcal{C}$ selects $c$ to
be a cause state. The states in $\mathsf{Eff}$ represent uncovered effects in
$\mathcal{K}$, while $\mathsf{eff}_{\mathsf{cov}}$ stands for covered effects.

We assign weight $1$ to all states in
$U=\mathsf{Eff}\cup\\{\mathsf{noeff}_{\mathsf{fp}}\\}$ and weight $0$ to all
other states of $\mathcal{K}$. Let $V=\\{\mathsf{eff}_{\mathsf{cov}}\\}$.
Then, $f=\mathrm{E}^{\min}_{\mathcal{K}}(\boxplus V)$ and an MD-scheduler
$\mathfrak{S}$ for $\mathcal{K}$ such that
$\mathrm{E}^{\mathfrak{S}}_{\mathcal{K}}(\boxplus V)=f$ are computable in
polynomial time. Let $\mathcal{C}_{\gamma}$ denote the set of states
$c\in\mathcal{C}$ where $\mathfrak{S}(c)=\gamma$ and let $\mathsf{Cause}$ be
the set of states $c\in\mathcal{C}_{\gamma}$ where $\mathcal{M}$ has a path
satisfying $(\neg\mathcal{C}_{\gamma})\,\mathrm{U}\,c$. Then, $\mathsf{Cause}$
is an SPR cause of $\mathcal{M}$. With arguments as in Section 5.2 we obtain
$\mathit{fscore}(\mathsf{Cause})=2/(f{+}2)$. It remains to show that
$\mathsf{Cause}$ is f-score-optimal. Let $C$ be an arbitrary SPR cause. Then,
$C\subseteq\mathcal{C}$. Let $\mathfrak{T}$ be the MD-scheduler for
$\mathcal{K}$ that schedules $\gamma$ in $C$ and $\alpha$ for all other states
of $\mathcal{K}$. Then, $\mathit{fscore}(C)=2/(f^{\mathfrak{T}}{+}2)$ where
$f^{\mathfrak{T}}=\mathrm{E}^{\mathfrak{T}}_{\mathcal{K}}(\boxplus V)$. Hence,
$f\leqslant f^{\mathfrak{T}}$, which yields
$\mathit{fscore}(\mathsf{Cause})\geqslant\mathit{fscore}(C)$.

The naïve adaption of the construction presented in the proof of Theorem 38
for MDPs would yield a stochastic game structure where the objective of one
player is to minimize the expected accumulated weight until reaching a target
state. Although algorithms for _stochastic shortest path (SSP) games_ are
known [PB99], they rely on assumptions on the game structure which would not
be satisfied here. However, for the threshold problem _SPR-f-score_ where
inputs are an MDP $\mathcal{M}$, $\mathsf{Eff}$ and
$\vartheta\in\mathbb{Q}_{\geq 0}$ and the task is to decide the existence of
an SPR cause whose f-score exceeds $\vartheta$, we can establish a polynomial
reduction to SSP games, which yields an $\mathrm{NP}\cap\mathrm{coNP}$ upper
bound:

######  Theorem 39.

The decision problem SPR-f-score is in $\mathrm{NP}\cap\mathrm{coNP}$.

Recall that for a given SPR cause $C$ and scheduler $\mathfrak{S}$ we have

$\mathit{fscore}^{\mathfrak{S}}(C)>\vartheta$ iff $\frac{\displaystyle
2\mathsf{tp}^{\mathfrak{S}}}{\displaystyle
2\mathsf{tp}^{\mathfrak{S}}+\mathsf{fp}^{\mathfrak{S}}+\mathsf{fn}^{\mathfrak{S}}}>\vartheta$.

In order to proof the upper bound of SPR-f-score we reformulate the condition
of SPR-f-score.

######  Lemma 40.

Let $\mathcal{M}=(S,\mathit{Act},P,\mathsf{init})$ be an MDP with a set of
terminal states $\mathsf{Eff}$, let $C$ be an SPR cause for $\mathsf{Eff}$ in
$\mathcal{M}$, and let $\vartheta$ be a rational. Then,
$\mathit{fscore}(C)>\vartheta$ iff

$\displaystyle
2(1{-}\vartheta)\mathsf{tp}^{\mathfrak{S}}-\vartheta\mathsf{fp}^{\mathfrak{S}}-\vartheta\mathsf{fn}^{\mathfrak{S}}>0$
(16)

for all schedulers $\mathfrak{S}$ for $\mathcal{M}$ with
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{Eff})>0$.

######  Proof 5.11.

Assume that $\mathit{fscore}(C)>\vartheta$ and let $\mathfrak{S}$ be a
scheduler with
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{Eff})>0$. If
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond C)=0$, then
$\mathit{fscore}(C)$ would be $0$. So,
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond C)>0$. Then,

$\mathit{fscore}^{\mathfrak{S}}(C)=\frac{\displaystyle
2\mathsf{tp}^{\mathfrak{S}}}{\displaystyle
2\mathsf{tp}^{\mathfrak{S}}+\mathsf{fp}^{\mathfrak{S}}+\mathsf{fn}^{\mathfrak{S}}}>\vartheta,\
\ \ $ which implies $\ \ \
2(1{-}\vartheta)\mathsf{tp}^{\mathfrak{S}}-\vartheta\mathsf{fp}^{\mathfrak{S}}-\vartheta\mathsf{fn}^{\mathfrak{S}}>0$

Now, suppose that (16) holds for a scheduler $\mathfrak{S}$ with
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{Eff})>0$. Let
$\mathfrak{S}$ be a scheduler that minimizes
$\mathit{fscore}^{\mathfrak{S}}(C)$. Such a scheduler exists by Theorem 31.
From (16), we conclude

$2(1{-}\vartheta)\mathsf{tp}^{\mathfrak{S}}-\vartheta\mathsf{fp}^{\mathfrak{S}}-\vartheta\mathsf{fn}^{\mathfrak{S}}>0$

and hence that $\mathit{fscore}^{\mathfrak{S}}(C)>\vartheta$ as above.

######  Proof 5.12 (Proof of Theorem 39).

Let $\mathcal{M}=(S,\mathit{Act},P,\mathsf{init})$ be an MDP,
$\mathsf{Eff}\subseteq S$ a set of terminal states, and $\vartheta$ a
rational. Consider $\mathcal{C}$, the set of states $c\in
S\setminus\mathsf{Eff}$ where $\\{c\\}$ is an SPR cause. If $\mathcal{C}$ is
empty then the threshold problem is trivial as there is no SPR cause at all.
Thus, we suppose that $\mathcal{C}$ is nonempty.

Note that $\mathrm{Pr}^{\min}_{\mathcal{M},c}(\Diamond\mathsf{Eff})>0$ for all
$c\in\mathcal{C}$. As the states in $\mathsf{Eff}$ are not part of any end
component of $\mathcal{M}$, no state $c\in\mathcal{C}$ is contained in an end
component of $\mathcal{M}$ either. Let
$\mathcal{N}=(S_{\mathcal{N}},\mathit{Act}_{\mathcal{N}},P_{\mathcal{N}},\mathsf{init}_{\mathcal{N}})$
be the MEC-quotient of $\mathcal{M}$ with the new additional terminal state
$\bot$. The MEC-quotient $\mathcal{N}$ contains the states from $\mathsf{Eff}$
and $\mathcal{C}$.

##### Claim 1:

There is an SPR cause $C$ for $\mathsf{Eff}$ in $\mathcal{M}$ with
$\mathit{fscore}(C)>\vartheta$ if and only if there is an SPR cause
$C^{\prime}$ for $\mathsf{Eff}$ in $\mathcal{N}$ with
$\mathit{fscore}(C^{\prime})>\vartheta$.

Proof of Claim 1. We first observe that all reachability probabilities
involved in the claim do not depend on the behavior during the traversal of
MECs. Furthermore, staying inside a MEC in $\mathcal{M}$ can be mimicked in
$\mathcal{N}$ by moving to $\bot$, and vice versa. More precisely, let
$C\subseteq\mathcal{C}$. Then, analogously to Lemma 19, for each scheduler
$\mathfrak{S}$ for $\mathcal{M}$, there is a scheduler $\mathfrak{T}$ for
$\mathcal{N}$, and vice versa, such that

  * •

$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{Eff}\mid(\neg
C)\,\mathrm{U}\,c)=\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{N}}(\Diamond\mathsf{Eff}\mid(\neg
C)\,\mathrm{U}\,c)$ for all $c\in C$ for which the values are defined,

  * •

$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{Eff})=\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{N}}(\Diamond\mathsf{Eff})$,

  * •

$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{Eff}\mid\Diamond
C)=\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{N}}(\Diamond\mathsf{Eff}\mid\Diamond
C)$ if the values are defined, and

  * •

$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond
C\mid\Diamond\mathsf{Eff})=\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{N}}(\Diamond
C\mid\Diamond\mathsf{Eff})$ if the values are defined.

Hence, $C$ is an SPR cause for $\mathsf{Eff}$ in $\mathcal{M}$ if and only if
it is in $\mathcal{N}$ and furthermore, if it is an SPR cause, the f-score of
$C$ in $\mathcal{M}$ and in $\mathcal{N}$ agree. This finishes the proof of
Claim 1.

##### Model transformation for ensuring positive effect probabilities.

Recall that the f-score is only defined for schedulers reaching $\mathsf{Eff}$
with positive probability. Now, we will provide a further model transformation
that will ensure that $\mathsf{Eff}$ is reached with positive probability
under all schedulers. If this is already the case, there is nothing to do. So,
we assume now that
$\mathrm{Pr}^{\min}_{\mathcal{N},\mathsf{init}_{\mathcal{N}}}(\Diamond\mathsf{Eff})=0$.

We define the subset $D\subseteq S_{\mathcal{N}}$ by

$D\stackrel{{\scriptstyle\text{\rm\tiny def}}}{{=}}\\{s\in
S_{\mathcal{N}}\mid\mathrm{Pr}^{\min}_{\mathcal{N},s}(\Diamond\mathsf{Eff})=0\\}.$

Note that $\mathsf{init}_{\mathcal{N}}\in D$. For each $s\in D$, we further
define

$\mathit{Act}^{\min}(s)=\\{\alpha\in\mathit{Act}_{\mathcal{N}}(s)\mid
P_{\mathcal{N}}(s,\alpha,D)=1\\}.$

Finally, let $E\subseteq D$ be the set of states that are reachable from
$\mathsf{init}_{\mathcal{N}}$ when only choosing actions from
$\mathit{Act}^{\min}(\cdot)$. Note that $E$ does not contain any states from
$\mathcal{C}$.

All schedulers that reach $\mathsf{Eff}$ with positive probability in
$\mathcal{N}$ have to leave the sub-MDP consisting of $E$ and the actions in
$\mathit{Act}^{\min}(\cdot)$ at some point. Let us call this sub-MDP
$\mathcal{N}^{\min}_{E}$. We define the set of state-action pairs $\Pi$ that
leave the sub-MDP $\mathcal{N}^{\min}_{E}$:

$\Pi\stackrel{{\scriptstyle\text{\rm\tiny def}}}{{=}}\\{(s,\alpha)\mid s\in
E\text{ and
}\alpha\in\mathit{Act}_{\mathcal{N}}(s)\setminus\mathit{Act}^{\min}(s)\\}.$

We now construct a further MDP $\mathcal{K}$. The idea is that $\mathcal{K}$
behaves like $\mathcal{N}$ after initially a scheduler is forced to choose a
probability distribution over state-action pairs from $\Pi$. In this way,
$\mathsf{Eff}$ is reached with positive probability under all schedulers.
Given an SPR cause, we will observe that for the f-score of this cause under a
scheduler, it is only important how large the probabilities with which state
action pairs from $\Pi$ are chosen are relative to each other while the
absolute values are not important. Due to this observation, for each SPR cause
$C$ and for each scheduler $\mathfrak{S}$ for $\mathcal{N}$ that reaches
$\mathsf{Eff}$ with positive probability, we can then construct a scheduler
for $\mathcal{K}$ that leads to the same recall and precision of $C$.

Formally, $\mathcal{K}$ is defined as follows: The state space is
$S_{\mathcal{N}}\cup\\{\mathsf{init}_{\mathcal{K}}\\}$ where
$\mathsf{init}_{\mathcal{K}}$ is a fresh initial state. For all states in
$S_{\mathcal{N}}$, the same actions as in $\mathcal{N}$ are available with the
same transition probabilities. I.e., for all $s,t\in S_{\mathcal{N}}$,

$\mathit{Act}_{\mathcal{K}}(s)\stackrel{{\scriptstyle\text{\rm\tiny
def}}}{{=}}\mathit{Act}_{\mathcal{N}}(s)\quad\text{and}\quad
P_{\mathcal{K}}(s,\alpha,t)\stackrel{{\scriptstyle\text{\rm\tiny
def}}}{{=}}P_{\mathcal{N}}(s,\alpha,t)\text{ for all
}\alpha\in\mathit{Act}_{\mathcal{K}}(s).$

For each state-action pair $(s,\alpha)$ from $\Pi$, we now add a new action
$\beta_{(s,\alpha)}$ that is enabled only in $\mathsf{init}_{\mathcal{K}}$.
These are all actions enabled in $\mathsf{init}_{\mathcal{K}}$, i.e.,

$\mathit{Act}_{\mathcal{K}}(\mathsf{init}_{\mathcal{K}})\stackrel{{\scriptstyle\text{\rm\tiny
def}}}{{=}}\\{\beta_{(s,\alpha)}\mid(s,\alpha)\in\Pi\\}.$

For each state $t\in S_{\mathcal{N}}$, we define the transition probabilities
under $\beta_{(s,\alpha)}$ by

$P_{\mathcal{K}}(\mathsf{init}_{\mathcal{K}},\beta_{(s,\alpha)},t)\stackrel{{\scriptstyle\text{\rm\tiny
def}}}{{=}}P_{\mathcal{N}}(s,\alpha,t).$

##### Claim 2:

A subset $C\subseteq\mathcal{C}$ such that for all $c\in
C:\mathrm{Pr}^{\max}_{\mathcal{N}}(\neg C\,\mathrm{U}\,c)>0$ is an SPR cause
for $\mathsf{Eff}$ in $\mathcal{N}$ with $\mathit{fscore}(C)>\vartheta$ if and
only if for all schedulers $\mathfrak{T}$ for $\mathcal{K}$, we have

$\displaystyle
2(1{-}\vartheta)\mathsf{tp}^{\mathfrak{T}}_{\mathcal{K}}-\vartheta\mathsf{fp}^{\mathfrak{T}}_{\mathcal{K}}-\vartheta\mathsf{fn}^{\mathfrak{T}}_{\mathcal{K}}>0.$
(17)

Proof of Claim 2. We first prove the direction “$\Rightarrow$”. So, let $C$ be
an SPR cause for $\mathsf{Eff}$ in $\mathcal{N}$ with
$\mathit{fscore}(C)>\vartheta$. As first observation we have that in order to
prove (17) for all schedulers $\mathfrak{T}$ for $\mathcal{K}$, it suffices to
consider schedulers $\mathfrak{T}$ that start with a deterministic choice for
state $\mathsf{init}_{\mathcal{K}}$ and then behave in an arbitrary way.

  * To see this, we consider the MDP $\mathcal{K}_{C}$ which consists of two copies of $\mathcal{K}$: “before $C$” and “after $C$”. When $\mathcal{K}_{C}$ enters a $C$-state in the first copy (“before $C$”), it switches to the second copy (“after $C$”) and stays there forever. Let us write $(s,1)$ for state $s$ in the first copy and $(s,2)$ for the copy of state $s$ in the second copy. Thus, in $\mathcal{K}_{C}$ the event $\Diamond C\wedge\Diamond\mathsf{Eff}$ is equivalent to reaching a state $(\mathsf{eff},2)$ where $\mathsf{eff}\in\mathsf{Eff}$, while $\Diamond C\wedge\neg\Diamond\mathsf{Eff}$ is equivalent to reaching a non-terminal state in the second copy, while $\neg\Diamond C\wedge\Diamond\mathsf{Eff}$ corresponds to the event reaching an effect state in the first copy.

Obviously, there is a one-to-one-correspondence of the schedulers of
$\mathcal{K}$ and $\mathcal{K}_{C}$. As $\mathcal{K}$ has no end components so
does $\mathcal{K}_{C}$. Therefore, a terminal state will be reached almost
surely under every scheduler. Furthermore, we equip $\mathcal{K}_{C}$ with a
weight function on states which assigns

    * –

weight $2(1{-}\vartheta)$ to the states $(\mathsf{eff},2)$ where
$\mathsf{eff}\in\mathsf{Eff}$,

    * –

weight $-\vartheta$ to the states $(\mathsf{eff},1)$ where
$\mathsf{eff}\in\mathsf{Eff}$ and to the states $(s,2)$ where $s$ is a
terminal non-effect state in $\mathcal{K}$ (and $\mathcal{K}_{C}$), and

    * –

weight 0 to all other states.

Let $V$ denote the set of all terminal states in $\mathcal{K}_{C}$. Then, the
expression on the left hand side of (17) equals
$\mathrm{E}^{\mathfrak{T}}_{\mathcal{K}_{C}}(\boxplus V)$, the expected
accumulated weight until reaching a terminal state under scheduler
$\mathfrak{T}$. Hence, (17) holds for all schedulers $\mathfrak{T}$ in
$\mathcal{K}$ if and only if $\mathrm{E}^{\min}_{\mathcal{K}_{C}}(\boxplus
V)>0$.

It is well-known that the minimal expected accumulated weight in EC-free MDPs
is achieved by an MD-scheduler [BK08]. Thus, there is an MD-scheduler
$\mathfrak{T}$ of $\mathcal{K}_{C}$ with
$\mathrm{E}^{\min}_{\mathcal{K}_{C}}(\boxplus
V)=\mathrm{E}^{\mathfrak{T}}_{\mathcal{K}_{C}}(\boxplus V)$. When viewed as a
scheduler of $\mathcal{K}$, $\mathfrak{T}$ behaves memoryless deterministic
before reaching $C$. In particular, $\mathfrak{T}$’s initial choice in
$\mathsf{init}_{\mathcal{K}}$ is deterministic.

Consider a scheduler $\mathfrak{T}$ for $\mathcal{K}$ with a deterministic
choice $\mathfrak{T}(\mathsf{init}_{\mathcal{K}})(\beta_{(s,\alpha)})=1$ where
$(s,\alpha)\in\Pi$. To construct an analogous scheduler $\mathfrak{S}$ of
$\mathcal{N}$, we pick an MD-scheduler $\mathfrak{U}$ of the sub-MDP
$\mathcal{N}^{\min}_{E}$ of $\mathcal{N}$ induced by the state-action pairs
$(u,\beta)$ where $u\in E$ and $\beta\in\mathit{Act}^{\min}(u)$ such that
there is a $\mathfrak{U}$-path from $\mathsf{init}_{\mathcal{N}}$ to state
$s$.

Scheduler $\mathfrak{S}$ of $\mathcal{N}$ operates with the mode
$\mathfrak{m}_{1}$ and the modes $\mathfrak{m}_{2,t}$ for $t\in
S_{\mathcal{N}}$. In its initial mode $\mathfrak{m}_{1}$, scheduler
$\mathfrak{S}$ behaves as $\mathfrak{U}$ as long as state $s$ has not been
visited. When having reached state $s$ in mode $\mathfrak{m}_{1}$, then
$\mathfrak{S}$ schedules the action $\alpha$ with probability 1. Let $t\in
S_{\mathcal{N}}$ be the state that $\mathfrak{S}$ reaches via the
$\alpha$-transition from $s$. Then, $\mathfrak{S}$ switches to mode
$\mathfrak{m}_{2,t}$ and behaves from then on as the residual scheduler
$\mathit{res}(\mathfrak{T},\varpi)$ of $\mathfrak{T}$ for the
$\mathfrak{T}$-path
$\varpi=\mathsf{init}_{\mathcal{K}}\,\beta_{(s,\alpha)}\,t$ in $\mathcal{K}$.
That is, after having scheduled the action $\beta_{(s,\alpha)}$, scheduler
$\mathfrak{S}$ behaves exactly as $\mathfrak{T}$.

Let $\lambda$ denote $\mathfrak{S}$’s probability to leave mode
$\mathfrak{m}_{1}$, which equals $\mathfrak{U}$’s probability to reach $s$
from $\mathsf{init}_{\mathcal{N}}$. Thus,
$\lambda=\mathrm{Pr}_{\mathcal{N}}^{\mathfrak{U}}(\Diamond s)$ when
$\mathfrak{U}$ is viewed as a scheduler of $\mathcal{N}$. As $E$ is disjoint
from $C$ and $\mathsf{Eff}$, scheduler $\mathfrak{S}$ stays forever in mode
$\mathfrak{m}_{1}$ and never reaches a state in $C\cup\mathsf{Eff}$ with
probability $1{-}\lambda$.

As $\mathfrak{S}$ and $\mathfrak{T}$ behave identically after choosing the
state-action pair $(s,\alpha)\in\Pi$ or the corresponding action
$\beta_{(s,\alpha)}$, respectively, which implies that

  * •

$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{N}}(\Diamond
C\land\Diamond\mathsf{Eff})=\lambda\cdot\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{K}}(\Diamond
C\land\Diamond\mathsf{Eff})$,

  * •

$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{N}}(\Diamond\mathsf{Eff})=\lambda\cdot\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{K}}(\Diamond\mathsf{Eff})$
and

  * •

$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{N}}(\Diamond
C\land\neg\Diamond\mathsf{Eff})=\lambda\cdot\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{K}}(\Diamond
C\land\neg\Diamond\mathsf{Eff})$.

As $\mathfrak{S}$ leaves the sub-MDP $\mathcal{N}^{\min}_{E}$ with probability
$\lambda>0$, we have
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{N}}(\Diamond\mathsf{Eff})>0$. By Lemma
40, we can conclude that

$2(1{-}\vartheta)\mathsf{tp}^{\mathfrak{S}}_{\mathcal{N}}-\vartheta\mathsf{fp}^{\mathfrak{S}}_{\mathcal{N}}-\vartheta\mathsf{fn}^{\mathfrak{S}}_{\mathcal{N}}>0$

By the equations above, this in turn implies that

$2(1{-}\vartheta)\mathsf{tp}^{\mathfrak{T}}_{\mathcal{K}}-\vartheta\mathsf{fp}^{\mathfrak{T}}_{\mathcal{K}}-\vartheta\mathsf{fn}^{\mathfrak{T}}_{\mathcal{K}}>0$

For the direction “$\Leftarrow$”, first recall that any subset of
$\mathcal{C}$ satisfying (M) is an SPR cause for $\mathsf{Eff}$ in
$\mathcal{N}$ by definition of $\mathcal{C}$. Now, let $\mathfrak{S}$ be a
scheduler for $\mathcal{N}$ with
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{N}}(\Diamond\mathsf{Eff})>0$. Let
$\Gamma$ be the set of finite $\mathfrak{S}$-paths $\gamma$ in the sub-MDP
$\mathcal{N}^{\min}_{E}$ such that $\mathfrak{S}$ chooses an action in
$\mathit{Act}_{\mathcal{N}}(\mathit{last}(\gamma))\setminus\mathit{Act}^{\min}(\mathit{last}(\gamma))$
with positive probability after $\gamma$ where $\mathit{last}(\gamma)$ denotes
the last state of $\gamma$. Let

$q\stackrel{{\scriptstyle\text{\rm\tiny
def}}}{{=}}\sum_{\gamma\in\Gamma}\sum_{\alpha\in\mathit{Act}_{\mathcal{N}}(\mathit{last}(\gamma))\setminus\mathit{Act}^{\min}(\mathit{last}(\gamma))}P_{\mathcal{N}}(\gamma)\cdot\mathfrak{S}(\gamma)(\alpha).$

So, $q$ is the overall probability that a state-action pair from $\Pi$ is
chosen under $\mathfrak{S}$. We now define a scheduler $\mathfrak{T}$ for
$\mathcal{K}$: For each $\gamma\in\Gamma$ ending in a state $s$ and each
$\alpha\in\mathit{Act}_{\mathcal{N}}(s)\setminus\mathit{Act}^{\min}(s)$, the
scheduler $\mathfrak{T}$ chooses action $\beta_{(s,\alpha)}$ in
$\mathsf{init}_{\mathcal{K}}$ with probability
$P_{\mathcal{N}}(\gamma)\cdot\mathfrak{S}(\gamma)(\alpha)/q$. When reaching a
state $t$ afterwards, $\mathfrak{T}$ behaves like
$\mathit{res}(\mathfrak{S},\gamma\,\alpha\,t)$ afterwards. Note that by
definition this indeed defines a probability distribution over the actions in
the initial state $\mathsf{init}_{\mathcal{K}}$.

By assumption, we know that now

$2(1{-}\vartheta)\mathsf{tp}^{\mathfrak{T}}_{\mathcal{K}}-\vartheta\mathsf{fp}^{\mathfrak{T}}_{\mathcal{K}}-\vartheta\mathsf{fn}^{\mathfrak{T}}_{\mathcal{K}}>0$

As the probability with which an action $\beta_{(s,\alpha)}$ is chosen by
$\mathfrak{T}$ for a $(s,\alpha)\in\Pi$ is $1/q$ times the probability that
$\alpha$ is chosen in $s$ to leave the sub-MDP $\mathcal{N}^{\min}_{E}$ under
$\mathfrak{S}$ in $\mathcal{N}$ and as the residual behavior is identical, we
conclude that

$\displaystyle
2(1{-}\vartheta)\mathsf{tp}^{\mathfrak{S}}_{\mathcal{N}}-\vartheta\mathsf{fp}^{\mathfrak{S}}_{\mathcal{N}}-\vartheta\mathsf{fn}^{\mathfrak{S}}_{\mathcal{N}}=\,\,q\cdot(2(1{-}\vartheta)\mathsf{tp}^{\mathfrak{T}}_{\mathcal{K}}-\vartheta\mathsf{fp}^{\mathfrak{T}}_{\mathcal{K}}-\vartheta\mathsf{fn}^{\mathfrak{T}}_{\mathcal{K}})>0.$

By Lemma 40, this shows that $\mathit{fscore}(C)>\vartheta$ in $\mathcal{N}$
and finishes the proof of Claim 2.

##### Construction of a game structure.

We now construct a _stochastic shortest path game_ (see [PB99]) to check
whether there is a subset $C\subseteq\mathcal{C}$ in $\mathcal{K}$ such that
(17) holds. Such a game is played on an MDP-like structure with the only
difference that the set of states is partitioned into two sets indicating
which player controls which states.

The game $\mathcal{G}$ has states
$(S_{\mathcal{K}}\times\\{\mathit{yes},\mathit{no}\\})\cup\mathcal{C}\times\\{\mathit{choice}\\}$.
On the subset $S_{\mathcal{K}}\times\\{\mathit{yes}\\}$, all available actions
and transition probabilities are just as in $\mathcal{K}$ and this copy of
$\mathcal{K}$ cannot be left. More formally, for all $s,t\in S_{\mathcal{K}}$
and $\alpha\in\mathit{Act}_{\mathcal{K}}(s)$, we have
$\mathit{Act}_{\mathcal{G}}((s,\mathit{yes}))=\mathit{Act}_{\mathcal{K}}(s)$
and
$P_{\mathcal{G}}((s,\mathit{yes}),\alpha,(t,\mathit{yes}))=P_{\mathcal{K}}(s,\alpha,t)$.

In the “$\mathit{no}$”-copy, the game also behaves like $\mathcal{G}$ but when
a state in $\mathcal{C}$ would be entered, the game moves to a state in
$\mathcal{C}\times\\{\mathit{choice}\\}$ instead. In a state of the form
$(c,\mathit{choice})$ with $c\in\mathcal{C}$, two actions $\alpha$ and $\beta$
are available. Choosing $\alpha$ leads to the state $(c,\mathit{yes})$ while
choosing $\beta$ leads to $(c,\mathit{no})$ with probability $1$.

Formally, this means that for all state $s\in S_{\mathcal{K}}$, we define
$\mathit{Act}_{\mathcal{G}}((s,\mathit{no}))=\mathit{Act}_{\mathcal{K}}(s)$
and for all actions $\alpha\in\mathit{Act}_{\mathcal{K}}(s)$:

  * •

$P_{\mathcal{G}}((s,\mathit{no}),\alpha,(t,\mathit{no}))=P_{\mathcal{K}}(s,\alpha,t)$
for all states $t\in S_{\mathcal{K}}\setminus\mathcal{C}$

  * •

$P_{\mathcal{G}}((s,\mathit{no}),\alpha,(c,\mathit{choice}))=P_{\mathcal{K}}(s,\alpha,c)$
for all states $c\in\mathcal{C}$

For states $s\in S_{\mathcal{K}}$, $c\in\mathcal{C}$, and
$\alpha\in\mathit{Act}_{\mathcal{K}}(s)$, we furthermore define:

$P_{\mathcal{G}}((c,\mathit{choice}),\alpha,(c,\mathit{yes}))=P_{\mathcal{G}}((c,\mathit{choice}),\beta,(c,\mathit{no}))=1$.

Intuitively speaking, whether a state $c\in\mathcal{C}$ should belong to the
cause set can be decided in the state $(c,\mathit{choice})$. The
“$\mathit{yes}$”-copy encodes that an effect state has been selected. More
concretely, the “$\mathit{yes}$-copy” is entered as soon as $\alpha$ has been
chosen in some state $(c,\mathit{choice})$ and will never be left from then
on. The “$\mathit{no}$”-copy of $\mathcal{K}$ then encodes that no state
$c\in\mathcal{C}$ which has been selected to become a cause state has been
visited so far. That is, if the current state of a play in $\mathcal{G}$
belongs to the $\mathit{no}$-copy then in all previous decisions in the states
$(c,\mathit{choice})$, action $\beta$ has been chosen.

Finally, we equip the game with a weight structure. All states in
$\mathsf{Eff}\times\\{\mathit{yes}\\}$ get weight $2(1-\vartheta)$. All
remaining terminal states in $S_{\mathcal{K}}\times\\{\mathit{yes}\\}$ get
weight $-\vartheta$. All states in $\mathsf{Eff}\times\\{\mathit{no}\\}$ get
weight $-\vartheta$. All remaining states have weight $0$.

The game is played between two players $0$ and $1$. Player $0$ controls all
states in $\mathcal{C}\times\\{\mathit{choice}\\}$ while player $1$ controls
the remaining states. The goal of player $0$ is to ensure that the expected
accumulated weight is $>0$.

##### Claim 3:

Player $0$ has a winning strategy ensuring that the expected accumulated
weight is $>0$ in the game $\mathcal{G}$ if and only if there is a subset
$C\subseteq\mathcal{C}$ in $\mathcal{K}$ which satisfies for all $c\in
C:\mathrm{Pr}^{\max}_{\mathcal{K}}(\neg C\,\mathrm{U}\,c)>0$ and for all
schedulers $\mathfrak{T}$ for $\mathcal{K}$ we have

$\displaystyle
2(1{-}\vartheta)\mathsf{tp}^{\mathfrak{T}}_{\mathcal{K}}-\vartheta\mathsf{fp}^{\mathfrak{T}}_{\mathcal{K}}-\vartheta\mathsf{fn}^{\mathfrak{T}}_{\mathcal{K}}>0.$
(18)

Proof of Claim 3. As $\mathcal{K}$ has no end components, also in the game
$\mathcal{G}$ a terminal state is reached almost surely under any pair of
strategies. Hence, we can rely on the results of [PB99] that state that both
players have an optimal memoryless deterministic strategy.

We start by proving direction “$\Rightarrow$” of Claim 3. Let $\zeta$ be a
memoryless deterministic winning strategy for player $0$. I.e., $\zeta$
assigns to each state in $\mathcal{C}\times\\{\mathit{choice}\\}$ an action
from $\\{\alpha,\beta\\}$. We define

$\mathcal{C}_{\alpha}\stackrel{{\scriptstyle\text{\rm\tiny
def}}}{{=}}\\{c\in\mathcal{C}\mid\zeta((c,\mathit{choice}))=\alpha\\}.$

Note that $\mathcal{C}_{\alpha}$ is not empty as otherwise a positive expected
accumulated weight in the game is not possible. (Here we use the fact that
only the effect states in the $\mathit{yes}$-copy have positive weight and
that the $\mathit{yes}$-copy can only be entered by taking $\alpha$ in one of
the states $(c,\mathit{choice})$.) To ensure for all $c\in
C:\mathrm{Pr}^{\max}_{\mathcal{K}}(\neg C\,\mathrm{U}\,c)>0$, we remove states
that cannot be visited as the first state of this set:

$C\stackrel{{\scriptstyle\text{\rm\tiny
def}}}{{=}}\\{c\in\mathcal{C}_{\alpha}\mid\mathcal{K},c\models\exists(\neg\mathcal{C}_{\alpha})\,\mathrm{U}\,c\\}.$

Note that the strategies for player $0$ in $\mathcal{G}$ which correspond to
the sets $\mathcal{C}_{\alpha}$ and $C$ lead to exactly the same plays.

Let $\mathfrak{T}$ be a scheduler for $\mathcal{K}$. This scheduler can be
used as a strategy for player $1$ in $\mathcal{G}$. Let us denote the expected
accumulated weight when player $0$ plays according to $\zeta$ and player $1$
plays according to $\mathfrak{T}$ by $w(\zeta,\mathfrak{T})$. As $\zeta$ is
winning for player 0 we have $w(\zeta,\mathfrak{T})>0.$ By the construction of
the game, it follows directly that

$w(\zeta,\mathfrak{T})=2(1{-}\vartheta)\mathsf{tp}^{\mathfrak{T}}_{\mathcal{K}}-\vartheta\mathsf{fp}^{\mathfrak{T}}_{\mathcal{K}}-\vartheta\mathsf{fn}^{\mathfrak{T}}_{\mathcal{K}}.$

Putting things together yields:

$\displaystyle
2(1{-}\vartheta)\mathsf{tp}^{\mathfrak{T}}_{\mathcal{K}}-\vartheta\mathsf{fp}^{\mathfrak{T}}_{\mathcal{K}}-\vartheta\mathsf{fn}^{\mathfrak{T}}_{\mathcal{K}}>0$
(19)

For the other direction, suppose there is a set $C\subseteq\mathcal{C}$ that
satisfies $\mathrm{Pr}^{\max}_{\mathcal{K}}(\neg C\,\mathrm{U}\,c)>0$ for all
$c\in C$ and (18) for all schedulers $\mathfrak{T}$ for $\mathcal{K}$. We
define the MD-strategy $\zeta$ from $C$ by letting
$\zeta((c,\mathit{choice}))=\alpha$ if and only if $c\in C$. For any strategy
$\mathfrak{T}$ for player $1$, we can again view $\mathfrak{T}$ also as a
scheduler for $\mathcal{K}$. Equation (19) holds again and shows that the
expected accumulated weight in $\mathcal{G}$ is positive if player $0$ plays
according to $\zeta$ against any strategy for player $1$. This finishes the
proof of Claim 3.

##### Putting together Claims 1-3.

We conclude that there is an SPR cause $C$ in the original MDP $\mathcal{M}$
with $\mathit{fscore}(C)>\vartheta$ if and only if player $1$ has a winning
strategy in the constructed game $\mathcal{G}$. As both players have optimal
MD-strategies in $\mathcal{G}$ [PB99], the decision problem is in
$\mathrm{NP}\cap\mathrm{coNP}$: We can guess the MD-strategy for player $0$
and solve the resulting stochastic shortest path problem in polynomial time
[BT91] to obtain an $\mathrm{NP}$-upper bound. Likewise, we can guess the MD-
strategy for player $1$ and solve the resulting stochastic shortest path
problem to obtain the $\mathrm{coNP}$-upper bound.

##### Optimality and threshold constraints for GPR causes.

Computing optimal GPR causes for either quality measure can be done in
polynomial space by considering all cause candidates, checking (G) in
$\mathrm{coNP}$ and computing the corresponding quality measure in polynomial
time (Section 5.2). As the space can be reused after each computation, this
results in polynomial space. However, we show that no polynomial-time
algorithms can be expected as the corresponding threshold problems are
$\mathrm{NP}$-hard. Let GPR-covratio (resp. GPR-recall, GPR-f-score) denote
the decision problems: Given $\mathcal{M},\mathsf{Eff}$ and
$\vartheta\in\mathbb{Q}$, decide whether there exists a GPR cause with
coverage ratio (resp. recall, f-score) at least $\vartheta$.

######  Theorem 41.

The problems GPR-covratio, GPR-recall and GPR-f-score are $\mathrm{NP}$-hard
and belong to $\Sigma^{P}_{2}$. For Markov chains, all three problems are
$\mathrm{NP}$-complete. $\mathrm{NP}$-hardness even holds for tree-like Markov
chains.

######  Proof 5.13.

$\Sigma^{P}_{2}$-membership. The algorithms for GPR-covratio, GPR-recall and
GPR-f-score rely on the guess-and-check principle: they start by non-
deterministically guessing a set $\mathsf{Cause}\subseteq S$, then check in
$\mathrm{coNP}$ whether $\mathsf{Cause}$ constitutes a GPR cause (see Section
4) and finally check
$\operatorname{\mathit{recall}}(\mathsf{Cause})\leq\vartheta$ (with standard
techniques), resp. $\mathit{covrat}(\mathsf{Cause})\leq\vartheta$, resp.
$\mathit{fscore}(\mathsf{Cause})\leq\vartheta$ (Theorem 31) in polynomial
time. The alternation between the existential quantification for guessing
$\mathsf{Cause}$ and the universal quantification for the $\mathrm{coNP}$
check of the GPR condition results in the complexity $\Sigma^{P}_{2}$ of the
polynomial-time hierarchy.

#####  $\mathrm{NP}$-membership for Markov chains.

$\mathrm{NP}$-membership for all three problems within Markov chains is
straightforward as we may non-deterministically guess a cause and check in
polynomial time whether it constitutes a GPR cause and satisfies the threshold
condition for the recall, coverage ratio or f-score.

#####  $\mathrm{NP}$-hardness of GPR-recall and GPR-covratio.

With arguments as in the proof of Lemma 35, the problems GPR-recall and GPR-
covratio are polynomially interreducible for Markov chains. Thus, it suffices
to prove NP-hardness of GPR-recall. For this, we provide a polynomial
reduction from the knapsack problem. The input of the latter are sequences
$A_{1},\ldots,A_{n},A$ and $B_{1},\ldots,B_{n},B$ of positive natural numbers
and the task is to decide whether there exists a subset $I$ of
$\\{1,\ldots,n\\}$ such that

$\displaystyle\sum_{i\in I}A_{i}\ <\ A\qquad\text{and}\qquad\sum_{i\in
I}B_{i}\ \geqslant\ B$ (20)

Let $K$ be the maximum of $A,A_{1},\ldots,A_{n},B,B_{1},\ldots,B_{n}$ and
$N=8(n{+}1)\cdot(K{+}1)$. We then define

$\displaystyle a_{i}$ $\displaystyle=\frac{A_{i}}{N},$ $\displaystyle a$
$\displaystyle=\frac{A}{N},$ $\displaystyle b_{i}$
$\displaystyle=\frac{B_{i}}{N},$ $\displaystyle b=$
$\displaystyle\frac{B}{N}.$

Then, $a,a_{1},\ldots,a_{n},b,b_{1},\ldots,b_{n}$ are positive rational
numbers strictly smaller than $\frac{1}{8(n{+}1)}$, and (20) can be rewritten
as:

$\displaystyle\sum_{i\in I}a_{i}\ <\ a\qquad\text{and}\qquad\sum_{i\in
I}b_{i}\ \geqslant\ b$ (21)

For $i\in\\{1,\ldots,n\\}$, let $p_{i}=2(a_{i}+b_{i})$ and
$w_{i}=\frac{b_{i}}{p_{i}}=\frac{1}{2}\cdot\frac{b_{i}}{a_{i}+b_{i}}$. Then,
$0<p_{i}<\frac{1}{2(n{+}1)}$ and $0<w_{i}<\frac{1}{2}$.
Moreover,$p_{i}\bigl{(}\frac{1}{2}-w_{i}\bigr{)}=a_{i}$ and $p_{i}\cdot
w_{i}=b_{i}$. Hence, (21) can be rewritten as:

$\displaystyle\sum\limits_{i\in I}p_{i}\bigl{(}\frac{1}{2}-w_{i}\bigr{)}\ <\
a\qquad\text{and}\qquad\sum\limits_{i\in I}p_{i}w_{i}\ \geqslant\ b$

which again is equivalent to:

$\displaystyle\frac{\sum\limits_{i\in I_{0}}p_{i}w_{i}}{\sum\limits_{i\in
I_{0}}p_{i}}\ >\ \frac{1}{2}\qquad\text{and}\qquad\sum\limits_{i\in
I_{0}}p_{i}w_{i}\ \geqslant\ \ p_{0}+b$ (22)

where $p_{0}=2a$, $w_{0}=1$ and $I_{0}=I\cup\\{0\\}$. Note that
$a<\frac{1}{8(n{+}1)}$ and hence $p_{0}<\frac{1}{4(n{+}1)}$.

Define a tree-shape Markov chain $\mathcal{M}$ with non-terminal states
$\mathsf{init}$, $s_{0},s_{1},\ldots,s_{n}$, and terminal states
$\mathsf{eff}_{0},\ldots,\mathsf{eff}_{n}$, $\mathsf{eff}_{\mathsf{unc}}$ and
$\mathsf{noeff},\mathsf{noeff}_{1},\ldots,\mathsf{noeff}_{n}$. Transition
probabilities are as follows:

  * •

$P(\mathsf{init},s_{i})=p_{i}$ for $i=0,\ldots,n$

  * •

$P(\mathsf{init},\mathsf{eff}_{\mathsf{unc}})\ =\
\frac{1}{2}-\sum\limits_{i=0}^{n}p_{i}w_{i}$

  * •

$P(\mathsf{init},\mathsf{noeff})=1-\sum\limits_{i=0}^{n}p_{i}-P(\mathsf{init},\mathsf{eff}_{\mathsf{unc}})$,

  * •

$P(s_{i},\mathsf{eff}_{i})=w_{i}$, $P(s_{i},\mathsf{noeff}_{i})=1{-}w_{i}$ for
$i=1,\ldots,n$

  * •

$P(s_{0},\mathsf{eff}_{0})=1=w_{0}$.

Note that $p_{0}+p_{1}+\ldots+p_{n}<\frac{1}{2}$ as all $p_{i}$’s are strictly
smaller than $\frac{1}{2(n{+}1)}$. As the $w_{i}$’s are bounded by 1, this
yields $0<P(\mathsf{init},\mathsf{eff}_{\mathsf{unc}})<\frac{1}{2}$ and
$0<P(\mathsf{init},\mathsf{noeff})<1$.

The graph structure of $\mathcal{M}$ is indeed a tree and $\mathcal{M}$ can be
constructed from the values $A,A_{1},\ldots,A_{n}$ and $B,B_{1},\ldots,B_{n}$
in polynomial time. Moreover, for
$\mathsf{Eff}=\\{\mathsf{eff}_{\mathsf{unc}}\\}\cup\\{\mathsf{eff}_{i}:i=0,1,\ldots,n\\}$
we have:

$\mathrm{Pr}_{\mathcal{M}}(\Diamond\mathsf{Eff})\ \ =\ \
\sum_{i=0}^{n}p_{i}w_{i}+P(\mathsf{init},\mathsf{eff}_{\mathsf{unc}})\ \ =\ \
\frac{1}{2}.$

As the values $w_{1},\ldots,w_{n}$ are strictly smaller than $\frac{1}{2}$, we
have $\mathrm{Pr}_{\mathcal{M}}(\ \Diamond\mathsf{Eff}\ |\ \Diamond C\
)<\frac{1}{2}$ for each nonempty subset $C$ of $\\{s_{1},\ldots,s_{n}\\}$.
Thus, the only candidates for GPR causes are the sets $C_{I}=\\{s_{i}:i\in
I_{0}\\}$ where $I\subseteq\\{1,\ldots,n\\}$ where as before
$I_{0}=I\cup\\{0\\}$. Note that for all states $s\in C_{I}$ there is a path
satisfying $(\neg C_{I})\,\mathrm{U}\,s$. Thus, $C_{I}$ is a GPR cause iff
$C_{I}$ satisfies (G). We have:

$\mathrm{Pr}_{\mathcal{M}}(\ \Diamond\mathsf{Eff}\ |\ \Diamond C_{I}\ )\ \ =\
\ \frac{\sum\limits_{i\in I_{0}}p_{i}w_{i}}{\sum\limits_{i\in I_{0}}p_{i}}$

and

$\operatorname{\mathit{recall}}(C_{I})\ \ =\ \ \mathrm{Pr}_{\mathcal{M}}(\
\Diamond(C_{I}\wedge\Diamond\mathsf{Eff})\ |\ \Diamond\mathsf{Eff}\ )\ \ =\ \
2\cdot\sum_{i\in I_{0}}p_{i}w_{i}.$

Thus, $C_{I}$ is a GPR cause with recall at least $2(p_{0}+b)$ if and only if
the two conditions in (22) hold, which again is equivalent to the satisfaction
of the conditions in (20). But this yields that $\mathcal{M}$ has a GPR cause
with recall at least $2(p_{0}+b)$ if and only if the knapsack problem is
solvable for the input $A,A_{1},\ldots,A_{n},B,B_{1},\ldots,B_{n}$.

#####  $\mathrm{NP}$-hardness of GPR-f-score.

Using similar ideas, we also provide a polynomial reduction from the knapsack
problem. Let $A,A_{1},\ldots,A_{n},B,B_{1},\ldots,B_{n}$ be an input for the
knapsack problem. We replace the $A$-sequence with $a,a_{1},\ldots,a_{n}$
where $a=\frac{A}{N}$ and $a_{i}=\frac{A_{i}}{N}$ where $N$ is as before. The
topological structure of the Markov chain that we are going to construct is
the same as in the NP-hardness proof for GPR-recall.

We will define polynomial-time computable values $p_{0},p_{1},\ldots,p_{n}\in\
]0,1[$ (where $p_{i}=P(\mathsf{init},s_{i})$), $w_{1},\ldots,w_{n}\in\ ]0,1[$
(where $w_{i}=P(s_{i},\mathsf{eff}_{i})$) and auxiliary variables $\delta\in\
]0,1[$ and $\lambda>1$ such that:

  1. (1)

$p_{0}+p_{1}+\ldots+p_{n}<\frac{1}{2}$

  2. (2)

$\lambda=\frac{p_{0}+\frac{1}{2}-\delta}{p_{0}}$

  3. (3)

for all $i\in\\{1,\ldots,n\\}$:

    1. (3.1)

$a_{i}\ =\ p_{i}\bigl{(}\frac{1}{2}-w_{i})$ (in particular
$w_{i}<\frac{1}{2}$)

    2. (3.2)

$B_{i}\ =\ \frac{1}{\delta}Bp_{i}\bigl{(}\lambda w_{i}-1)$ (in particular
$w_{i}>\frac{1}{\lambda}$)

Assuming such values have been defined, we obtain:

$\displaystyle\sum_{i\in I}B_{i}\ \geqslant\ B$ iff
$\displaystyle\frac{1}{\delta}B\sum_{i\in I}p_{i}(\lambda w_{i}-1)\ \geqslant\
B$ iff $\displaystyle\sum_{i\in I}p_{i}(\lambda w_{i}-1)\ \geqslant\ \delta$
iff $\displaystyle\lambda\sum_{i\in I}p_{i}w_{i}\ \geqslant\ \delta+\sum_{i\in
I}p_{i}$

Hence:

$\displaystyle\sum_{i\in I}B_{i}\ \geqslant\ B$ iff
$\displaystyle\frac{\displaystyle\sum\limits_{i\in
I}p_{i}w_{i}}{\displaystyle\delta+\sum\limits_{i\in I}p_{i}}\ \geqslant\
\frac{1}{\lambda}$

For all positive real numbers $x,y,u,v$ with $\frac{x}{y}=\frac{1}{\lambda}$
we have:

$\frac{x+u}{y+v}\geqslant\frac{1}{\lambda}\ \ \ \ \ \text{iff}\ \ \ \ \
\frac{u}{v}\geqslant\frac{1}{\lambda}$

By the constraints for $\lambda$ (see (2)), we have
$\frac{p_{0}}{p_{0}+\frac{1}{2}-\delta}=\frac{1}{\lambda}$. Therefore:

$\displaystyle\frac{\displaystyle\sum\limits_{i\in
I}p_{i}w_{i}}{\displaystyle\delta+\sum\limits_{i\in I}p_{i}}\ \geqslant\
\frac{1}{\lambda}$ iff $\displaystyle\frac{\displaystyle
p_{0}+\sum\limits_{i\in
I}p_{i}w_{i}}{\displaystyle(p_{0}+\frac{1}{2}-\delta)+\delta+\sum\limits_{i\in
I}p_{i}}\ \ =\ \ \frac{\displaystyle p_{0}+\sum\limits_{i\in
I}p_{i}w_{i}}{\displaystyle p_{0}+\frac{1}{2}+\sum\limits_{i\in I}p_{i}}\
\geqslant\ \frac{1}{\lambda}$

As before let $w_{0}=1$ and $I_{0}=I\cup\\{0\\}$. Then, the above yields:

$\displaystyle\sum_{i\in I}B_{i}\ \geqslant\ B$ iff
$\displaystyle\frac{\displaystyle\sum\limits_{i\in
I_{0}}p_{i}w_{i}}{\displaystyle\frac{1}{2}+\sum\limits_{i\in I_{0}}p_{i}}\
\geqslant\ \frac{1}{\lambda}$

As in the NP-hardness proof for GPR-recall and using (3.1):

$\mathrm{Pr}_{\mathcal{M}}(\Diamond\mathsf{Eff})\ =\ \frac{1}{2}\ >\
w_{i}\qquad\text{for $i=1,\ldots,n$}$

Thus, each GPR cause must have the form $C_{I}=\\{s_{i}:i\in I_{0}\\}$ for
some subset $I$ of $\\{1,\ldots,n\\}$. Moreover:

$\mathrm{Pr}_{\mathcal{M}}(\Diamond C_{I})\ =\ \sum_{i\in
I_{0}}p_{i}\qquad\text{and}\qquad\mathrm{Pr}_{\mathcal{M}}(\Diamond(C_{I}\wedge\Diamond\mathsf{Eff}))\
=\ \sum_{i\in I_{0}}p_{i}w_{i}$

So, the f-score of $C_{I}$ is:

$\mathit{fscore}(C_{I})\ \ =\ \
2\cdot\frac{\mathrm{Pr}_{\mathcal{M}}(\Diamond(C_{I}\wedge\Diamond\mathsf{Eff}))}{\mathrm{Pr}_{\mathcal{M}}(\Diamond\mathsf{Eff})+\mathrm{Pr}_{\mathcal{M}}(\Diamond
C_{I})}\ \ =\ \ 2\cdot\frac{\sum\limits_{i\in
I_{0}}p_{i}w_{i}}{\frac{1}{2}+\sum\limits_{i\in I_{0}}p_{i}}$

This implies:

$\displaystyle\sum_{i\in I}B_{i}\ \geqslant\ B$ iff
$\displaystyle\mathit{fscore}(C_{I})\ \geqslant\ \frac{2}{\lambda}$

With $p_{0}=2a$ and using (3.1) and arguments as in the NP-hardness proof for
GPR-recall, we obtain:

$\displaystyle\sum_{i\in I}A_{i}\ <\ A$ iff $C_{I}$ is a GPR cause

Thus, the constructed Markov chain has a GPR cause with f-score at least
$\frac{2}{\lambda}$ if and only if the knapsack problem is solvable for the
input $A,A_{1},\ldots,A_{n},B,B_{1},\ldots,B_{n}$.

It remains to define the values $p_{1},\ldots,p_{n},w_{1},\ldots,w_{n}$ and
$\delta$. (The value of $\lambda$ is then obtained by (2).) (3.1) and (3.2)
can be rephrased as equations for $w_{i}$:

(3.1’):

$w_{i}=\frac{1}{2}-\frac{a_{i}}{p_{i}}$

(3.2’):

$w_{i}=\frac{1}{\lambda}\bigl{(}\delta\frac{B_{i}}{Bp_{i}}+1\bigr{)}$

This yields an equation for $p_{i}$:

$\frac{1}{2}-\frac{a_{i}}{p_{i}}\ \ =\ \
\frac{1}{\lambda}\Bigl{(}\delta\frac{B_{i}}{Bp_{i}}+1\Bigr{)}$

and leads to:

$\displaystyle p_{i}\ \ =\ \ \frac{2\lambda}{\lambda-2}a_{i}\ +\
\frac{2\delta}{\lambda-2}\cdot\frac{B_{i}}{B}$ (23)

We now substitute $\lambda$ by (2) and arrive at

$p_{i}\ \ =\ \ \frac{p_{0}}{\frac{1}{2}-\delta}a_{i}\ +\ a_{i}+\ \frac{\delta
p_{0}}{\frac{1}{2}-\delta}\frac{B_{i}}{B}.$

By choice of $N$, all $a_{i}$’s and $a$ are smaller than $\frac{1}{8(n{+}1)}$.
Using this together with $p_{0}=2a$, we get:

$\displaystyle p_{i}\ <\
\frac{1}{4(n{+}1)(\frac{1}{2}-\delta)}\frac{1}{8(n{+}1)}\ +\
\frac{1}{8(n{+}1)}\ +\
\frac{\delta}{4(n{+}1)(\frac{1}{2}-\delta)}\frac{B_{i}}{B}$ (24)

Let now $\delta=\frac{1}{8K}$ (where $K$ is as above, i.e., the maximum of the
values $A,A_{1},\ldots,A_{n}$, $B$, $B_{1},\ldots,B_{n}$). Then,
$p_{1},\ldots,p_{n}$ are computable in polynomial time, and so are the values
$w_{1},\ldots,w_{n}$ (by (3.1’)). As $\frac{2\lambda}{\lambda-2}>2$ and using
(23), we obtain $p_{i}>2a_{i}$. So, by (3.1’) we get $0<w_{i}<\frac{1}{2}$.

It remains to prove (1). Using $\delta=\frac{1}{8K}$, we obtain from (24):

$p_{i}\ <\
\frac{1}{4(n{+}1)(\frac{1}{2}-\frac{1}{8K})}\frac{1}{8(n{+}1)}+\frac{1}{8(n{+}1)}+\frac{1}{32(n{+}1)(\frac{1}{2}-\frac{1}{8K})K}\frac{B_{i}}{B}\
\stackrel{{\scriptstyle\text{\rm\tiny def}}}{{=}}\ x$

As $\frac{1}{2}-\frac{1}{8K}\geq\frac{1}{4}$ and $\frac{B_{i}}{B}<K$, this
yields:

$p_{i}\ <\ x\ <\ \frac{1}{8(n{+}1)^{2}}+\frac{1}{8(n{+}1)}+\frac{1}{8(n{+}1)}\
<\ \frac{1}{2(n{+}1)}.$

But then condition (1) holds.

##### Arbitrary quality measures

Consider any algebraic function
$f(\mathsf{tp},\mathsf{tn},\mathsf{fp},\mathsf{fn})$. That is $f$ satisfies
some polynomial equation where the coefficients are polynomials in
$\mathsf{tp},\mathsf{tn},\mathsf{fp}$ and $\mathsf{fn}$. Almost every quality
measure for binary classifiers (see [Pow11]) is such a function. Taking the
worst case scheduler for such a function we define

$f(\mathsf{Cause})=\inf_{\mathfrak{S}}f^{\mathfrak{S}}(\mathsf{tp}_{\mathsf{Cause}}^{\mathfrak{S}},\mathsf{tn}_{\mathsf{Cause}}^{\mathfrak{S}},\mathsf{fp}_{\mathsf{Cause}}^{\mathfrak{S}},\mathsf{fn}_{\mathsf{Cause}}^{\mathfrak{S}}),$

where $\mathfrak{S}$ ranges over all schedulers such that $f^{\mathfrak{S}}$
is well defined. Given a PR cause $\mathsf{Cause}$ and a rational
$\vartheta\in\mathbb{Q}$, deciding whether $f(\mathsf{Cause})\leq\vartheta$
can be done in $\mathrm{PSPACE}$ as a satisfiability problem in the
existential theory of the reals [Can88].

As we can decide for a given cause candidate $\mathsf{Cause}$ whether it is a
SPR cause in $\mathrm{P}$ or a GPR cause in $\mathrm{coNP}$, this also yields
an algorithm for finding optimal causes for $f$. Given an MDP $\mathcal{M}$
with terminal effect set $\mathsf{Eff}$ and quality measure $f$ as algebraic
function we consider each cause candidate $\mathsf{Cause}$, check whether it
is a PR cause (SPR or GPR) and consider the decision problem
$f(\mathsf{Cause})\leq\vartheta$. As all of these steps have a complexity
upper bound of $\mathrm{PSPACE}$ and we only need to save the best cause
candidate so far with its value $f(\mathsf{Cause})$, this results in
polynomial space as well.

##  6\. $\omega$-regular effect scenarios

In this section, we turn to an extension of the previous definition of PR
causes. So far, we considered both the cause and the effect as sets of states
in an MDP $\mathcal{M}$ with state space $S$. We will refer to this setting as
the _state-based_ setting from now on. In a more general approach, we now
consider the effect to be an $\omega$-regular language $\mathsf{rEff}\subseteq
S^{\omega}$ over the state space $S$. Note that we denote regular events as
effects mainly by $\mathsf{rEff}$ to avoid confusion with effects as sets of
states.

In a first step, we still consider sets of states $\mathsf{Cause}\subseteq S$
as causes, which we call _reachability causes_ (Section 6.1). For reachability
GPR causes, the techniques from the previous section are mostly still
applicable. For reachability SPR causes, on the other hand, we observe that
they take on the flavor of state-based GPR causes as well. Afterwards, we
generalize the definition further to allow $\omega$-regular co-safety
properties over the state space $S$ as causes, which we call _co-safety
causes_ (Section 6.2). While this allows us to express much more involved
cause-effect relationships, we will see that attempts of checking co-safety
SPR causality or of finding good causes for a given effect encounter major new
difficulties.

###  6.1. Sets of states as causes

Throughout this section, let $\mathcal{M}=(S,\mathit{Act},P,\mathsf{init})$ be
an MDP. As long as we use sets of states as causes, the definition of GPR and
SPR causes can easily be adapted to $\omega$-regular effects: [Reachability
GPR/SPR causes] Let $\mathcal{M}$ be as above. Let $\mathsf{rEff}\subseteq
S^{\omega}$ be an $\omega$-regular language over $S$ and $\mathsf{Cause}$ a
nonempty subset of $S$ such that for each $c\in\mathsf{Cause}$, there is a
scheduler $\mathfrak{S}$ with
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}((\neg\mathsf{Cause})\,\mathrm{U}\,c)>0$.
Then, $\mathsf{Cause}$ is said to be a _reachability GPR cause_ for
$\mathsf{rEff}$ iff the following condition (rG) holds:

(rG):

For each scheduler $\mathfrak{S}$ where
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{Cause})>0$:

$\displaystyle\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\mathsf{rEff}\ |\
\Diamond\mathsf{Cause})\ >\
\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\mathsf{rEff}).$ (rGPR)

$\mathsf{Cause}$ is called a _reachability SPR cause_ for $\mathsf{rEff}$ iff
the following condition (rS) holds:

(rS):

For each state $c\in\mathsf{Cause}$ and each scheduler $\mathfrak{S}$ where
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}((\neg\mathsf{Cause})\,\mathrm{U}\,c)>0$:

$\displaystyle\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\mathsf{rEff}\mid(\neg\mathsf{Cause})\,\mathrm{U}\,c)\
>\ \mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\mathsf{rEff}).$ (rSPR)

There is one small caveat that we want to mention here: If the effect
$\mathsf{rEff}$ is a reachability property $\lozenge\mathsf{Eff}$ for a set of
states $\mathsf{Eff}\subseteq S$, then this new definition allows that a
GPR/SPR cause $\mathsf{Cause}$ is not disjoint from the set of states
$\mathsf{Eff}$. If two sets $\mathsf{Cause},\mathsf{Eff}\subseteq S$ are
disjoint, however, then $\mathsf{Cause}$ is a GPR/SPR cause for $\mathsf{Eff}$
according to Definition 3 iff $\mathsf{Cause}$ is a reachability GPR/SPR cause
for the $\omega$-regular event $\lozenge\mathsf{Eff}$ according to the new
definition. As we now view the effect as the $\omega$-regular property on
infinite executions, one can, nevertheless, argue that the _temporal priority_
(C2) is captured by the new definition because the cause will be reached after
finitely many steps if it is reached. We will address problems with this
interpretation and a stronger notion of temporal priority in Section 6.1.3.

A first simple observation that follows as in the state-based setting is that
a reachability SPR cause for $\mathsf{rEff}$ is also a reachability GPR cause
for $\mathsf{rEff}$

####  6.1.1. Checking causality and existence of reachability PR causes

To explore how this change of definition influences the previously established
results for GPR and SPR causes, we have to clarify how effects will be
represented. We use deterministic Rabin automata (DRAs) as they are expressive
enough to capture all $\omega$-regular languages and they are deterministic,
which will allow us to form well-behaved products of the automata with MDPs.
Let $\mathcal{M}$ be an MDP, $\mathsf{rEff}$ an effect given by the DRA
$\mathcal{A}_{\mathsf{rEff}}$ and $\mathsf{Cause}\subseteq S$ a cause
candidate. As a special case we again have Markov chains with no non-
deterministic choices. Then, the conditions (rG) and (rS) can easily be
checked by computing the corresponding probabilities in polynomial time (see
[BKKM14] for algorithms to compute conditional probabilities in MCs for path
properties.) We now consider the case where non-deterministic choices exist.
We will provide a model transformation of $\mathcal{M}$ using the DRA such
that the resulting MDP has no end components and the effect is a reachability
property again.

[Removing end components] Let $\mathcal{M}$ and $\mathcal{A}_{\mathsf{rEff}}$
be as above. Consider the product MDP
$\mathcal{N}\stackrel{{\scriptstyle\text{\rm\tiny
def}}}{{=}}\mathcal{M}\otimes\mathcal{A}_{\mathsf{rEff}}$. This product is an
MDP equipped with a Rabin acceptance condition found in the second component
of each state in the product.

We now take two copies of $\mathcal{N}$ representing a mode before
$\mathsf{Cause}$ has been reached and one mode after $\mathsf{Cause}$ has been
reached. So, each state $\mathfrak{s}$ is equipped with one extra bit $0$ or
$1$. Initially, the MDP starts in the copy labeled with $0$ and behaves like
$\mathcal{N}$ until a state with its first component in $\mathsf{Cause}$ is
reached. From there, the process moves to the corresponding successor states
in the second copy labeled with $1$. We call the resulting MDP
$\mathcal{N}^{\prime}$ and denote the set of states with their first component
in $\mathsf{Cause}$ in the first copy that are reachable in
$\mathcal{N}^{\prime}$ by $\mathsf{Cause}_{\mathcal{A}_{\mathsf{rEff}}}$, in
particular, to express that these states are enriched with states of the
automaton $\mathcal{A}_{\mathsf{rEff}}$.

Next, we consider the MECs $\mathcal{E}_{1},\dots,\mathcal{E}_{k}$ of
$\mathcal{N}^{\prime}$. Note that the states in
$\mathsf{Cause}_{\mathcal{A}_{\mathsf{rEff}}}$ are not contained in any MEC.
Furthermore, all MECs consist either only of states from the first copy
labeled $0$, or only of states from the second copy labeled with $1$. For each
MEC $\mathcal{E}_{i}$, we determine whether there is a scheduler for
$\mathcal{E}_{i}$ that ensures the event
$\mathit{Acc}(\mathcal{A}_{\mathsf{rEff}})$ that the acceptance condition of
$\mathcal{A}_{\mathsf{rEff}}$ is met with probability $1$ and whether there is
a scheduler that ensures this event with probability $0$. With the techniques
of [dA97] and [BGC09] this can be done in polynomial time. We then add four
new terminal states $\mathsf{eff}_{\mathsf{cov}}$,
$\mathsf{noeff}_{\mathsf{fp}}$, $\mathsf{eff}_{\mathsf{unc}}$, and
$\mathsf{noeff}_{\mathsf{tn}}$ and construct the MEC-quotient of
$\mathcal{N}^{\prime}$ while, for each $i\leq k$, enabling a new action in the
state $s_{\mathcal{E}_{i}}$ obtained from $\mathcal{E}_{i}$ leading to

  * •

$\mathsf{eff}_{\mathsf{unc}}$ if $\mathit{Acc}(\mathcal{A}_{\mathsf{rEff}})$
can be ensured with probability $1$ in $\mathcal{E}_{i}$ and $\mathcal{E}_{i}$
is contained in copy $0$, and

  * •

another new action leading to $\mathsf{noeff}_{\mathsf{tn}}$ if
$\mathit{Acc}(\mathcal{A}_{\mathsf{rEff}})$ can be ensured with probability
$0$ in $\mathcal{E}_{i}$ and $\mathcal{E}_{i}$ is contained in copy $0$;

  * •

$\mathsf{eff}_{\mathsf{cov}}$ if $\mathit{Acc}(\mathcal{A}_{\mathsf{rEff}})$
can be ensured with probability $1$ in $\mathcal{E}_{i}$ and $\mathcal{E}_{i}$
is contained in copy $1$, and

  * •

another new action leading to $\mathsf{noeff}_{\mathsf{fp}}$ if
$\mathit{Acc}(\mathcal{A}_{\mathsf{rEff}})$ can be ensured with probability
$0$ in $\mathcal{E}_{i}$ and $\mathcal{E}_{i}$ is contained in copy $1$.

Finally, we remove all states which are not reachable (from the initial
state). We call the resulting MDP
$\mathcal{M}_{[\mathsf{rEff},\mathsf{Cause}]}$ and emphasize that this MDP
contains all states in $\mathsf{Cause}_{\mathcal{A}_{\mathsf{rEff}}}$, has no
end components, and has the four terminal states
$\mathsf{eff}_{\mathsf{cov}}$, $\mathsf{noeff}_{\mathsf{fp}}$,
$\mathsf{eff}_{\mathsf{unc}}$, and $\mathsf{noeff}_{\mathsf{tn}}$.
Furthermore, for each $c\in\mathsf{Cause}$, we denote the subset of states in
$\mathsf{Cause}_{\mathcal{A}_{\mathsf{rEff}}}$ with $c$ in their first
component by $c_{\mathcal{A}_{\mathsf{rEff}}}$. $\lhd$

######  Lemma 42.

Let $\mathcal{M}$, $\mathsf{Cause}$, and $\mathcal{A}_{\mathsf{rEff}}$ be as
above and let $\mathcal{M}_{[\mathsf{rEff},\mathsf{Cause}]}$ be the
constructed MDP in Notation 6.1.1 which contains the set
$\mathsf{Cause}_{\mathcal{A}_{\mathsf{rEff}}}$. Then, $\mathsf{Cause}$ is a
reachability GPR cause for $\mathsf{rEff}$ in $\mathcal{M}$ if and only if
$\mathsf{Cause}_{\mathcal{A}_{\mathsf{rEff}}}$ is a GPR cause for
$\\{\mathsf{eff}_{\mathsf{cov}},\mathsf{eff}_{\mathsf{unc}}\\}$ in
$\mathcal{M}_{[\mathsf{rEff},\mathsf{Cause}]}$. Furthermore, $\mathsf{Cause}$
is a reachability SPR cause for $\mathsf{rEff}$ in $\mathcal{M}$ if and only
if, for each $c\in\mathsf{Cause}$, the set $c_{\mathcal{A}_{\mathsf{rEff}}}$
of states in $\mathsf{Cause}_{\mathcal{A}_{\mathsf{rEff}}}$ with $c$ in their
first component is a GPR cause for
$\\{\mathsf{eff}_{\mathsf{cov}},\mathsf{eff}_{\mathsf{unc}}\\}$ in
$\mathcal{M}_{[\mathsf{rEff},\mathsf{Cause}]}$.

######  Proof 6.1.

The set $\mathsf{Cause}_{\mathcal{A}_{\mathsf{rEff}}}$ in
$\mathcal{M}_{[\mathsf{rEff},\mathsf{rCause}]}$ satisfies
$\mathrm{Pr}^{\max}_{\mathcal{M}_{[\mathsf{rEff},\mathsf{rCause}]}}(\neg\mathsf{Cause}_{\mathcal{A}_{\mathsf{rEff}}}\,\mathrm{U}\,d)>0$
for each state $d\in\mathsf{Cause}_{\mathcal{A}_{\mathsf{rEff}}}$ by
construction, since all states in
$\mathsf{Cause}_{\mathcal{A}_{\mathsf{rEff}}}$ are reachable and a run cannot
reach two different states in $\mathsf{Cause}_{\mathcal{A}_{\mathsf{rEff}}}$.
So, this minimality condition is satisfied in any case and, of course,
$\\{\mathsf{eff}_{\mathsf{cov}},\mathsf{eff}_{\mathsf{unc}}\\}$ and
$\mathsf{Cause}_{\mathcal{A}_{\mathsf{rEff}}}$ are disjoint.

Now, let $\mathfrak{T}$ be a scheduler for
$\mathcal{M}_{[\mathsf{rEff},\mathsf{Cause}]}$. The scheduler $\mathfrak{T}$
can be mimicked by a scheduler $\mathfrak{S}$ for $\mathcal{M}$: As long as
$\mathfrak{T}$ moves through the MEC-quotient of $\mathcal{N}^{\prime}$, the
scheduler $\mathfrak{S}$ follows this behavior by leaving MECs through the
corresponding actions in $\mathcal{M}$. Whenever $\mathfrak{T}$ moves to one
of the states $\mathsf{eff}_{\mathsf{cov}}$ and $\mathsf{eff}_{\mathsf{unc}}$,
the last step begins in a state $s_{\mathcal{E}}$ obtained from a MEC
$\mathcal{E}$ of $\mathcal{M}$. In this case, $\mathfrak{S}$ will stay in
$\mathcal{E}$ while ensuring with probability $1$ that the resulting run is
accepted by $\mathcal{A}_{\mathsf{rEff}}$. Similarly, if $\mathfrak{T}$ moves
to $\mathsf{noeff}_{\mathsf{tn}}$ or $\mathsf{noeff}_{\mathsf{fp}}$, the
scheduler $\mathfrak{S}$ for $\mathcal{M}$ stays in the corresponding MEC and
realizes the acceptance condition of $\mathcal{A}_{\mathsf{rEff}}$ with
probability $0$. Vice versa, a scheduler $\mathfrak{S}$ for $\mathcal{M}$ can
be mimicked by a scheduler $\mathfrak{T}$ for
$\mathcal{M}_{[\mathsf{rEff},\mathsf{Cause}]}$ analogously. So in an end
component $\mathcal{E}$, if $\mathfrak{S}$ stays in $\mathcal{E}$ and ensures
that the resulting run is accepted by $\mathcal{A}_{\mathsf{rEff}}$ with
probability $p_{1}$, stays in $\mathcal{E}$ and ensures that the resulting run
is not accepted by $\mathcal{A}_{\mathsf{rEff}}$ with probability $p_{2}$, and
leaves $\mathcal{E}$ with probability $p_{3}$, $\mathfrak{T}$ will move to the
corresponding state $\mathsf{eff}_{\mathsf{cov}}$ or
$\mathsf{eff}_{\mathsf{unc}}$ with probability $p_{1}$, to
$\mathsf{noeff}_{\mathsf{tn}}$ or $\mathsf{noeff}_{\mathsf{fp}}$ with
probability $p_{2}$, and leave take actions leaving $s_{\mathcal{E}}$ to other
states with the same probability distribution with which $\mathfrak{S}$ takes
the leaving actions of $\mathcal{E}$.

For such a pair of schedulers $\mathfrak{S}$ and $\mathfrak{T}$, we observe
that

$\displaystyle\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\lozenge\mathsf{Cause})$
$\displaystyle=\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{M}_{[\mathsf{rEff},\mathsf{Cause}]}}(\lozenge\mathsf{Cause}_{\mathcal{A}_{\mathsf{rEff}}}),$
(25) $\displaystyle\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\mathsf{rEff})$
$\displaystyle=\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{M}_{[\mathsf{rEff},\mathsf{Cause}]}}(\lozenge
E),\text{ and}$ (26)
$\displaystyle\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\lozenge\mathsf{Cause}\wedge\mathsf{rEff})$
$\displaystyle=\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{M}_{[\mathsf{rEff},\mathsf{Cause}]}}(\lozenge\mathsf{eff}_{\mathsf{cov}})=\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{M}_{[\mathsf{rEff},\mathsf{Cause}]}}(\lozenge\mathsf{Cause}_{\mathcal{A}_{\mathsf{rEff}}}\wedge\lozenge
E).$ (27)

Hence, $\mathsf{Cause}^{\prime}$ is a GPR cause for
$\\{\mathsf{eff}_{\mathsf{cov}},\mathsf{eff}_{\mathsf{unc}}\\}$ in
$\mathcal{M}_{[\mathsf{rEff},\mathsf{Cause}]}$ if and only if $\mathsf{Cause}$
is a reachability GPR cause for $\mathsf{rEff}$ in $\mathcal{M}$.

Now consider each element $c\in\mathsf{Cause}$ individually. We can use the
same argumentation to see that a scheduler $\mathfrak{T}$ in
$\mathcal{M}_{[\mathsf{rEff},\mathsf{Cause}]}$ can be mimicked by a scheduler
$\mathfrak{S}$ for $\mathcal{M}$, and vice versa, such that

$\displaystyle\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\neg\mathsf{Cause}\,\mathrm{U}\,c)$
$\displaystyle=\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{M}_{[\mathsf{rEff},\mathsf{Cause}]}}(\lozenge
c_{\mathcal{A}_{\mathsf{rEff}}}),\text{ and}$
$\displaystyle\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\mathsf{rEff}\mid\neg\mathsf{Cause}\,\mathrm{U}\,c)$
$\displaystyle=\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{M}_{[\mathsf{rEff},\mathsf{Cause}]}}(\lozenge\mathsf{eff}_{\mathsf{cov}}\mid\lozenge
c_{\mathcal{A}_{\mathsf{rEff}}}).$

Thus, $\mathsf{Cause}$ is a reachability SPR cause for $\mathsf{rEff}$ in
$\mathcal{M}$ if and only if $c_{\mathcal{A}_{\mathsf{rEff}}}$ is a GPR cause
for $\\{\mathsf{eff}_{\mathsf{cov}},\mathsf{eff}_{\mathsf{unc}}\\}$ in
$\mathcal{M}_{[\mathsf{rEff},\mathsf{Cause}]}$ for all $c\in\mathsf{Cause}$.

This Lemma 42 shows that reachability SPR causality shares similarities with
GPR causality. As an immediate consequence we can check conditions (rG) and
(rS) in $\mathcal{M}_{[\mathsf{rEff},\mathsf{Cause}]}$ by using the already
established algorithms for GPR causes. This results in the following
complexity upper bounds.

######  Corollary 43.

Let $\mathcal{M}$ be an MDP and $\mathsf{rEff}\subseteq S^{\omega}$ an
$\omega$-regular language given as DRA $\mathcal{A}_{\mathsf{rEff}}$. Given a
set $\mathsf{Cause}\subseteq S$ we can decide whether $\mathsf{Cause}$ is a
reachability SPR/GPR cause for $\mathsf{rEff}$ in $\mathrm{coNP}$.

######  Proof 6.2.

By Lemma 42, we can use the construction of
$\mathcal{M}_{[\mathsf{rEff},\mathsf{Cause}]}$, which takes polynomial time.
Then, Theorem 17 allows us to check whether $\mathsf{Cause}$ is a reachability
GPR cause in $\mathrm{coNP}$ directly, while we can apply the GPR check to
each set $c_{\mathcal{A}_{\mathsf{rEff}}}$ and the effect
$\\{\mathsf{eff}_{\mathsf{cov}},\mathsf{eff}_{\mathsf{unc}}\\}$ in
$\mathcal{M}_{[\mathsf{rEff},\mathsf{Cause}]}$ for $c\in\mathsf{Cause}$ in
order to determine whether $\mathsf{Cause}$ is a reachability SPR
$\mathsf{Cause}$ for $\mathsf{rEff}$.

As in the state-based setting, we can argue that there is a reachability GPR
cause iff there is a reachability SPR cause iff there is a singleton
reachability SPR cause. Consequently, the existence of a reachability GPR/SPR
cause can be checked by checking for each state $c$ of the MDP whether
$\\{c\\}$ constitutes a reachability SPR cause. We conclude:

######  Corollary 44.

The existence of a reachability GPR/SPR cause can be decided in
$\mathrm{coNP}$.

####  6.1.2. Computing quality measures of reachability PR causes

As in Section 5.1, we can view reachability PR causes as binary classifiers.
This leads to the confusion matrix as before (Figure 7) with the difference
that this time the path does not “hit” the effect set, but rather
$\mathsf{rEff}$ holds on the path. Hence, we define the following entries of
the confusion matrix: Given $\mathsf{rEff}$, $\mathsf{Cause}$ and a scheduler
$\mathfrak{S}$, we let

$\begin{array}[]{rclrcl}\mathsf{tp}^{\mathfrak{S}}&\stackrel{{\scriptstyle\text{\rm\tiny
def}}}{{=}}&\mathrm{Pr}_{\mathcal{M}}^{\mathfrak{S}}(\lozenge\mathsf{Cause}\wedge\mathsf{rEff}),&\mathsf{tn}^{\mathfrak{S}}&\stackrel{{\scriptstyle\text{\rm\tiny
def}}}{{=}}&\mathrm{Pr}_{\mathcal{M}}^{\mathfrak{S}}(\neg\lozenge\mathsf{Cause}\wedge\neg\mathsf{rEff}),\\\\[4.30554pt]
\mathsf{fp}^{\mathfrak{S}}&\stackrel{{\scriptstyle\text{\rm\tiny
def}}}{{=}}&\mathrm{Pr}_{\mathcal{M}}^{\mathfrak{S}}(\lozenge\mathsf{Cause}\wedge\neg\mathsf{rEff}),&\mathsf{fn}^{\mathfrak{S}}&\stackrel{{\scriptstyle\text{\rm\tiny
def}}}{{=}}&\mathrm{Pr}_{\mathcal{M}}^{\mathfrak{S}}(\neg\lozenge\mathsf{Cause}\wedge\mathsf{rEff}).\end{array}$

######  Lemma 45.

Let $\mathcal{M}$ be as above, $\mathsf{rEff}$ an $\omega$-regular effect
given by the DRA $\mathcal{A}_{\mathsf{rEff}}$ and let
$\mathsf{Cause}\subseteq S$ be a reachability GPR/SPR cause. Further, let
$\mathcal{M}_{[\mathsf{rEff},\mathsf{Cause}]}$ be as constructed above with
the set of cause states $\mathsf{Cause}_{\mathcal{A}_{\mathsf{rEff}}}$ and the
set of effect states
$\\{\mathsf{eff}_{\mathsf{cov}},\mathsf{eff}_{\mathsf{unc}}\\}$. Then, for
each scheduler $\mathfrak{S}$ for $\mathcal{M}$, there is a scheduler
$\mathfrak{T}$ for $\mathcal{M}_{[\mathsf{rEff},\mathsf{Cause}]}$, and vice
versa, such that

$\mathsf{tp}^{\mathfrak{S}}=\mathsf{tp}^{\mathfrak{T}},\qquad\mathsf{tn}^{\mathfrak{S}}=\mathsf{tn}^{\mathfrak{T}},\qquad\mathsf{fp}^{\mathfrak{S}}=\mathsf{fp}^{\mathfrak{T}},\qquad\mathsf{fn}^{\mathfrak{S}}=\mathsf{fn}^{\mathfrak{T}},$

where the values for $\mathfrak{T}$ are defined in
$\mathcal{M}_{[\mathsf{rEff},\mathsf{Cause}]}$ as in Section 5.1.

######  Proof 6.3.

In the proof of Lemma 42, we have seen that for each scheduler $\mathfrak{S}$
for $\mathcal{M}$, we can find a scheduler $\mathfrak{T}$ for
$\mathcal{M}_{[\mathsf{rEff},\mathsf{Cause}]}$ and vice versa such that
Equations (25) - (27) hold. This implies the equalities claimed here.

Analogously to Section 5.1, we can now define
$\operatorname{\mathit{recall}}$, $\mathit{covrat}$, and $\mathit{fscore}$ of
a reachability PR cause as the infimum of these values in terms of
$\mathsf{tp}^{\mathfrak{S}}$, $\mathsf{fp}^{\mathfrak{S}}$,
$\mathsf{tn}^{\mathfrak{S}}$, and $\mathsf{fn}^{\mathfrak{S}}$ over all
schedulers $\mathfrak{S}$ for which the respective quality measures are
defined. The computation of these values can then be done with the methods
from the state-based setting:

######  Corollary 46.

Let $\mathcal{M}$ be an MDP and $\mathsf{rEff}\subseteq S^{\omega}$ an
$\omega$-regular language given as DRA $\mathcal{A}_{\mathsf{rEff}}$. Given a
reachability SPR/GPR cause $\mathsf{Cause}\subseteq S$ we can compute
$\operatorname{\mathit{recall}}(\mathsf{Cause}),\mathit{covrat}(\mathsf{Cause})$
and $\mathit{fscore}(\mathsf{Cause})$ in polynomial time.

######  Proof 6.4.

Use Lemma 45, Corollary 30 and Theorem 31.

####  6.1.3. Finding quality optimal reachability PR causes

When trying to find good causes for an $\omega$-regular effect
$\mathsf{rEff}$, we cannot say that effects and causes should be disjoint as
in the setting where effects and causes were sets of states. This leads to the
possibility that causes might exist that do not capture the intuition behind
temporal priority: E.g., if the effect $\mathsf{rEff}$ is a reachability
property $\lozenge E$ for a set of states $E$, the set of states $E$ itself
will be a reachability PR cause if for each state $c\in E$,
$\mathrm{Pr}^{\max}_{\mathcal{M}}(\neg E\,\mathrm{U}\,c)>0$ holds.
Furthermore, there might be causes $C$ that can only be reached after $E$ has
already been reached.

In order to account for the temporal priority of causes, we will include the
following condition when trying to find good causes: We require for a cause
$\mathsf{Cause}\subseteq S$ that

$\displaystyle\mathrm{Pr}^{\min}_{\mathcal{M}}(\mathsf{rEff}\mid\neg\mathsf{Cause}\,\mathrm{U}\,c)<1\text{
for all $c\in\mathsf{Cause}$.}$ (TempPrio)

Intuitively, this states that it is never already certain that the execution
will belong to $\mathsf{rEff}$ when the cause is reached. A variation of this
criteria has been proposed also in [BDF+21].

######  Remark 47.

The condition (TempPrio) could be added to the definition of reachability PR
causes. After the product construction in Notation 6.1.1, the condition can
easily be checked for a given cause candidate $\mathsf{Cause}\subseteq S$: For
each $c\in\mathsf{Cause}$, there must be at least one state with $c$ in the
first component in $\mathcal{M}_{[\mathsf{rEff},\mathsf{Cause}]}$ such that
$\mathsf{noeff}_{\mathsf{fp}}$ is reachable from this state.

Furthermore, this condition is stronger than the requirement that causes and
effects are disjoint in the state-based setting. In the state-based setting,
however, the analogue of condition (TempPrio) could also be included easily.
Instead of having to be disjoint from a set of effect states $\mathsf{Eff}$, a
cause $\mathsf{Cause}$ would then simply not be allowed to contain any state
$s$ with $\mathrm{Pr}^{\min}_{\mathcal{M},s}(\Diamond\mathsf{Eff})=1$. $\lhd$

Now, we want to find recall- and coverage ratio-optimal reachability SPR
causes. As in the state-based setting, we define the set $\mathcal{C}$ of all
possible singleton reachability SPR causes for $\mathsf{rEff}$ that in
addition satisfy (TempPrio) as explained in Remark 47. By Corollary 43, we can
check whether a state $c\in S$ is a singleton reachability SPR cause in
$\mathrm{coNP}$; whether there is at least one state with $c$ in the first
component in $\mathcal{M}_{[\mathsf{rEff},\mathsf{Cause}]}$ such that
$\mathsf{noeff}_{\mathsf{fp}}$ is reachable from this state is checkable in
polynomial time. As before, the canonical cause $\mathsf{CanCause}$ is now the
set of states $c\in\mathcal{C}$ for which there is a scheduler $\mathfrak{S}$
with $\mathrm{Pr}^{\mathfrak{S}}(\neg\mathcal{C}\,\mathrm{U}\,c)$.

For the complexity of the computation of the recall- and coverage ratio-
optimal canonical cause and its values, the observations above lead us to the
complexity class $\mathrm{PF}^{\mathrm{NP}}$ as defined in [Sel94]. It
consists of all functions that can be computed in polynomial time with access
to an $\mathrm{NP}$-oracle, or equivalently a $\mathrm{coNP}$-oracle.

######  Proposition 48.

If $\mathcal{C}\neq\emptyset$ then $\mathsf{CanCause}$ is a ratio- and recall
optimal reachability SPR cause for $\mathsf{rEff}$. The threshold problem for
the coverage ratio and the recall can be decided in $\mathrm{coNP}$. The
optimal values $\operatorname{\mathit{recall}}(\mathsf{CanCause})$ and
$\mathit{covrat}(\mathsf{CanCause})$ can be computed in
$\mathrm{PF}^{\mathrm{NP}}$.

######  Proof 6.5.

The optimality of $\mathsf{CanCause}$ follows by the arguments used for
Theorem 36. In order to compute $\mathsf{CanCause}$ we check for each state
$s$ whether (rS) does not hold in $\mathrm{NP}$ and then take the remaining
states $c\in S$ to define $\mathcal{C}$ by checking (TempPrio) for each $c$.
If (TempPrio) holds then $c\in\mathcal{C}$ and
$\mathsf{CanCause}=\\{c\in\mathcal{C}\mid\mathrm{Pr}^{\max}_{\mathcal{M}}(\neg\mathcal{C}\,\mathrm{U}\,c)>0\\}$.
This allows to compute the recall- and coverage ratio-optimal cause
$\mathsf{CanCause}$ in $\mathrm{PF}^{\mathrm{NP}}$.

For the threshold problem whether there is a reachability SPR cause with
recall at least a given $\vartheta\in\mathbb{Q}$, the $\mathrm{coNP}$ upper
bound can be shown as follows: For each state $c$ that does not belong to
$\mathcal{C}$, i.e., that is not a singleton reachability SPR cause, there is
a polynomial size certificate for this, as it can be checked in
$\mathrm{coNP}$. The collection of all states that do not belong to
$\mathcal{C}$ together with these certificates (they do not belong to
$\mathcal{C}$) can now serve as a certificate that the optimal recall is less
than $\vartheta$ in this the case. Given such a collection of certificates, we
can check in polynomial time that indeed all provided states do not belong to
$\mathcal{C}$. The complement of the provided states forms a super set
$\mathcal{D}$ of $\mathsf{CanCause}$. Computing the recall of the set
$\mathcal{D}$ can then be done in polynomial time as in Corollary 46. This
value is an upper bound for the recall of $\mathsf{CanCause}$. Note that if
all states that do not belong to $\mathcal{C}$ are given in the certificate,
the value even equals the recall of $\mathsf{CanCause}$.

So, if the optimal value is less than $\vartheta$, this is witnessed by the
described certificate containing all states not in $\mathcal{C}$. Vice versa,
if a certificate is given resulting in a super set $\mathcal{D}$ of
$\mathsf{CanCause}$ such that the recall of $\mathcal{D}$ is less than
$\vartheta$, then there is no reachability SPR cause with a recall of at least
$\vartheta$. So, the threshold problem lies in $\mathrm{coNP}$. For the
coverage ratio, the analogous argument works.

For the threshold problems for f-score-optimal reachability SPR causes and
reachability GPR causes optimal with respect to recall, coverage ration or
f-score that satisfy (TempPrio), we rely on the guess-and-check approach used
for optimal GPR causes in the state-based setting. We guess a subset
$\mathsf{Cause}$ of states of the MDP, check whether we found a reachability
SPR/GPR cause in $\mathrm{coNP}$, and compute the quality measure under
consideration in polynomial time as explained in the previous section. For the
computation of an optimal cause, we obtain a polynomial-space algorithm.

######  Corollary 49.

Let $\mathcal{M}$ be an MDP and $\mathsf{rEff}$ be an $\omega$-regular
language given by $\mathcal{A}_{\mathsf{rEff}}$. Given
$\vartheta\in\mathbb{Q}$, deciding whether there exists a reachability GPR
cause $\mathsf{Cause}$ with
$\operatorname{\mathit{recall}}(\mathsf{Cause})\geq\vartheta$ (resp.
$\mathit{covrat}(\mathsf{Cause})\geq\vartheta,\mathit{fscore}(\mathsf{Cause})\geq\vartheta$)
can be done in $\Sigma^{P}_{2}$ and is $\mathrm{NP}$-hard.
$\mathrm{NP}$-hardness even holds for Markov chains.

Deciding whether there is a reachability SPR cause $\mathsf{Cause}$ with
$\mathit{fscore}(\mathsf{Cause})\geq\vartheta$ can be done in
$\Sigma^{P}_{2}$. A recall-, covratio-, or f-score-optimal reachability GPR
cause as well as an f-score-optimal reachability SPR cause can be computed in
polynomial space.

######  Proof 6.6.

Obviously the lower bounds extend to this setting as we can interpret GPR
causes for $\mathsf{Eff}$ as reachability GPR causes for
$\lozenge\mathsf{Eff}$. The upper bounds extend to this setting by using the
construction from Notation 6.1.1. Since for Theorem 41 we relied on guess-and-
check algorithms to establish the upper bounds for the threshold problems, we
can use analogous algorithms in setting of $\omega$-regular effects. We guess
a set $\mathsf{Cause}\subseteq S$, check the reachability GPR causality in
$\mathrm{coNP}$ (Corollary 43) and compute the value of the quality measure in
polynomial time (Corollary 46). Again, the alternation between the existential
quantification for guessing $\mathsf{Cause}$ and the universal quantification
for the $\mathrm{coNP}$ check results in the complexity $\Sigma^{P}_{2}$ of
the polynomial-time hierarchy.

In order to show that the decision problem for
$\mathit{fscore}(\mathsf{Cause})\geq\vartheta$ for SPR causes $\mathsf{Cause}$
is in $\Sigma^{P}_{2}$ we resort to the constructed MDP
$\mathcal{M}_{[\mathsf{rEff},\mathsf{Cause}]}$. By Lemma 42 a reachability SPR
cause $\mathsf{Cause}$ in $\mathcal{M}$ corresponds to a set of GPR causes
$\\{c_{\mathcal{A}_{\mathsf{rEff}}}\mid c\in\mathsf{Cause}\\}$ in
$\mathcal{M}_{[\mathsf{rEff},\mathsf{Cause}]}$, which can be interpreted as
GPR cause $C=\bigcup_{c\in\mathsf{Cause}}c_{\mathcal{A}_{\mathsf{rEff}}}$.
This way we can encode the property
$\mathit{fscore}(\mathsf{Cause})\geq\vartheta$ in $\mathcal{M}$ by
$\mathit{fscore}(C)\geq\vartheta$ in
$\mathcal{M}_{[\mathsf{rEff},\mathsf{Cause}]}$. This results in a decision
problem GPR-f-score for GPR causes which is in $\Sigma^{P}_{2}$ by Theorem 41.

For computing optimal GPR causes as well as f-score-optimal SPR causes we can
try all cause candidates by computing the related value
($\operatorname{\mathit{recall}},\mathit{covrat}$ or $\mathit{fscore}$) and
always store the best one so far. As the space for the cause can be reused,
this results in a polynomial space algorithm.

###  6.2. $\omega$-regular co-safety properties as causes

We now want to discuss an extension of the previous framework when we also
consider causes to be regular sets of executions. However, in order to account
for the _temporal priority_ of causes, i.e., the fact that causes should occur
before their effects, it makes sense to restrict causes to $\omega$-regular
co-safety properties. The reason is that an $\omega$-regular co-safety
property $\mathcal{L}$ is uniquely determined by the regular set of minimal
_good_ prefixes of words in $\mathcal{L}$. Recall that a good prefix $\pi$ for
$\mathcal{L}$ is a finite word such that all infinite extensions of $\pi$
belong to $\mathcal{L}$ and that all infinite words in the co-safety language
$\mathcal{L}$ have a good prefix. Hence, we can say that a cause
$\mathsf{rCause}$ occurred as soon as a good prefix for $\mathsf{rCause}$ has
been produced. For this subsection we will denote regular effects and causes
mainly by $\mathsf{rEff}$ and $\mathsf{rCause}$ to avoid confusion with
effects and causes as sets of states. In the following formal definition, we
use finite words $\sigma\in S^{\ast}$ to denote the event $\sigma S^{\omega}$.
[co-safety GPR/SPR causes] Let $\mathcal{M}$ be an MDP with state space $S$
and let $\mathsf{rEff}\subseteq S^{\omega}$ be an $\omega$-regular language.
An $\omega$-regular co-safety language $\mathsf{rCause}\subseteq S^{\omega}$
is a _co-safety GPR cause_ for $\mathsf{rEff}$ if the following condition
(coG) holds:

(coG):

For each scheduler $\mathfrak{S}$ where
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\mathsf{rCause})>0$:

$\displaystyle\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\mathsf{rEff}\mid\mathsf{rCause})\
>\ \mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\mathsf{rEff}).$ (cosafeGPR)

The event $\mathsf{rCause}$ is called a _co-safety SPR cause_ for
$\mathsf{rEff}$ if the following condition (coS) hold:

(coS):

For each minimal good prefix $\sigma$ for $\mathsf{rCause}$ and each scheduler
$\mathfrak{S}$ where $\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\sigma)>0$:

$\displaystyle\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\mathsf{rEff}\mid\sigma)\
>\ \mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\mathsf{rEff}).$ (cosafeSPR)

As in the state-based setting it follows that co-safety SPR cause are also co-
safety GPR causes.

####  6.2.1. Checking co-safety causality

We will represent co-safety PR causes as DFAs which accept good prefixes of
the represented $\omega$-regular event. Note that, for any $\omega$-regular
co-safety property, there is a DFA accepting exactly the minimal good
prefixes. So, we will restrict to such DFAs that accept the minimal good
prefixes of an $\omega$-regular co-safety property. Such a DFA can never
accept a word $w$ as well as a proper prefix $v$ of $w$.

Let now $\mathcal{M}$ be an MDP, $\mathsf{rEff}$ an effect given by the DRA
$\mathcal{A}_{\mathsf{rEff}}$ and $\mathsf{rCause}$ a cause candidate given by
a DFA $\mathcal{A}_{\mathsf{rCause}}$ as above. So, in particular,
$\mathcal{A}_{\mathsf{rCause}}$ accepts exactly the minimal good prefixes for
$\mathsf{rCause}$. For the special case of Markov chains the check can be done
in polynomial time analogously to reachability PR causes by computing the
corresponding conditional probabilities. We can provide a model transformation
of $\mathcal{M}$ using both automata such that the resulting MDP has no end
components and the effect is a reachability property again similar to Notation
6.1.1.

For this consider the product
$\mathcal{N}\stackrel{{\scriptstyle\text{\rm\tiny
def}}}{{=}}\mathcal{M}\otimes\mathcal{A}_{\mathsf{rEff}}\otimes\mathcal{A}_{\mathsf{rCause}}$.
This product is an MDP equipped with two kinds of acceptance conditions. The
Rabin acceptance of $\mathcal{A}_{\mathsf{rEff}}$ in the second component of
each state and the acceptance condition of $\mathcal{A}_{\mathsf{rCause}}$ in
the third component. Now let $\mathsf{rCause}_{\mathcal{A}_{\mathsf{rEff}}}$
be the set of all states of $\mathcal{N}$ whose third component is accepting
in $\mathcal{A}_{\mathsf{rCause}}$ and which are reachable from the initial
state.

As in Notation 6.1.1, we construct an MDP $\mathcal{N}^{\prime}$ by
introducing a mode before $\mathsf{rCause}_{\mathcal{A}_{\mathsf{rEff}}}$ and
a mode after $\mathsf{rCause}_{\mathcal{A}_{\mathsf{rEff}}}$. We then take the
MEC-quotient with the four terminal states $\mathsf{eff}_{\mathsf{cov}}$,
$\mathsf{noeff}_{\mathsf{fp}}$, $\mathsf{eff}_{\mathsf{unc}}$, and
$\mathsf{noeff}_{\mathsf{tn}}$, which are reachable from states
$s_{\mathcal{E}}$ that result from collapsing the MEC $\mathcal{E}$ depending
on whether $\mathcal{E}$ is contained in the before- or
after-$\mathsf{rCause}_{\mathcal{A}_{\mathsf{rEff}}}$ mode and whether the
acceptance condition of $\mathcal{A}_{\mathsf{rEff}}$ can be realized with
probability $0$ and $1$, respectively in $\mathcal{E}$, analogously to
Notation 6.1.1. We call the resulting MDP
$\mathcal{M}_{[\mathsf{rEff},\mathsf{rCause}]}$ and emphasize that this MDP
still contains all states in $\mathsf{rCause}_{\mathcal{A}_{\mathsf{rEff}}}$
as they are not contained in any end component.

We start with the observation, that for co-safety GPR causes this reduction
characterizes the condition (coG) completely.

######  Lemma 50.

Let $\mathcal{M}$ be and MDP, $\mathcal{A}_{\mathsf{rEff}}$ an DRA, and
$\mathcal{A}_{\mathsf{rCause}}$ a DFA be as above and let
$\mathcal{M}_{[\mathsf{rEff},\mathsf{rCause}]}$ be the constructed MDP that
contains the set $\mathsf{rCause}_{\mathcal{A}_{\mathsf{rEff}}}$ of reachable
states that have an accepting $\mathcal{A}_{\mathsf{rCause}}$-component. Then,
$\mathsf{rCause}$ is a co-safety GPR cause for $\mathsf{rEff}$ in
$\mathcal{M}$ if and only if the set of states
$\mathsf{rCause}_{\mathcal{A}_{\mathsf{rEff}}}$ is a GPR cause for
$\\{\mathsf{eff}_{\mathsf{cov}},\mathsf{eff}_{\mathsf{unc}}\\}$ in
$\mathcal{M}_{[\mathsf{rEff},\mathsf{rCause}]}$.

######  Proof 6.7.

The set $\mathsf{rCause}_{\mathcal{A}_{\mathsf{rEff}}}$ in
$\mathcal{M}_{[\mathsf{rEff},\mathsf{rCause}]}$ satisfies
$\mathrm{Pr}^{\max}_{\mathcal{M}_{[\mathsf{rEff},\mathsf{rCause}]}}(\neg\mathsf{rCause}_{\mathcal{A}_{\mathsf{rEff}}}\,\mathrm{U}\,c)>0$
for each $c\in\mathsf{rCause}_{\mathcal{A}_{\mathsf{rEff}}}$ by construction,
since all states in $\mathsf{rCause}_{\mathcal{A}_{\mathsf{rEff}}}$ are
reachable and a run cannot reach two different states in
$\mathsf{rCause}_{\mathcal{A}_{\mathsf{rEff}}}$. Thus, the minimality
condition is satisfied in any case.

Now, let $\mathfrak{S}$ be a scheduler for
$\mathcal{M}_{[\mathsf{rEff},\mathsf{rCause}]}$. The scheduler $\mathfrak{S}$
can be mimicked by a scheduler $\mathfrak{T}$ for $\mathcal{M}$: As long as
$\mathfrak{S}$ moves through the MEC-quotient of $\mathcal{N}^{\prime}$, the
scheduler $\mathfrak{T}$ follows this behavior by leaving MECs through the
corresponding actions in $\mathcal{M}$. Whenever $\mathfrak{S}$ moves to one
of the states $\mathsf{eff}_{\mathsf{cov}}$ and $\mathsf{eff}_{\mathsf{unc}}$,
the last step begins in a state $s_{\mathcal{E}}$ obtained from a MEC
$\mathcal{E}$ of $\mathcal{M}$. In this case, $\mathfrak{T}$ will stay in
$\mathcal{E}$ while ensuring with probability $1$ that the resulting run is
accepted by $\mathcal{A}_{\mathsf{rEff}}$. Similarly, if $\mathfrak{S}$ moves
to $\mathsf{noeff}_{\mathsf{tn}}$ or $\mathsf{noeff}_{\mathsf{fp}}$, the
scheduler $\mathfrak{T}$ for $\mathcal{M}$ stays in the corresponding MEC and
realizes the acceptance condition of $\mathcal{A}_{\mathsf{rEff}}$ with
probability $0$. Vice versa, a scheduler $\mathfrak{T}$ for
$\mathcal{M}_{[\mathsf{rEff},\mathsf{rCause}]}$ can be mimicked by a scheduler
$\mathfrak{S}$ for $\mathcal{M}$ analogously (see also the proof of Lemma 42).

For such a pair of schedulers $\mathfrak{S}$ and $\mathfrak{T}$, we observe
that

$\displaystyle\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\mathsf{rCause})$
$\displaystyle=\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{M}_{[\mathsf{rEff},\mathsf{rCause}]}}(\lozenge\mathsf{rCause}_{\mathcal{A}_{\mathsf{rEff}}}),$
(28) $\displaystyle\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\mathsf{rEff})$
$\displaystyle=\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{M}_{[\mathsf{rEff},\mathsf{rCause}]}}(\lozenge
E),\text{ and}$ (29)
$\displaystyle\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\mathsf{rCause}\land\mathsf{rEff})$
$\displaystyle=\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{M}_{[\mathsf{rEff},\mathsf{rCause}]}}(\lozenge\mathsf{eff}_{\mathsf{cov}})=\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{M}_{[\mathsf{rEff},\mathsf{rCause}]}}(\lozenge\mathsf{rCause}_{\mathcal{A}_{\mathsf{rEff}}}\land\lozenge
E).$ (30)

Hence, $\mathsf{rCause}_{\mathcal{A}_{\mathsf{rEff}}}$ is a GPR cause for $E$
in $\mathcal{M}_{[\mathsf{rEff},\mathsf{rCause}]}$ if and only if
$\mathsf{rCause}$ is a regular GPR cause for $\mathsf{rEff}$ in $\mathcal{M}$.

For co-safety SPR causes this is not a full characterization but only holds in
one direction:

######  Lemma 51.

Let $\mathcal{M}$, $\mathcal{A}_{\mathsf{rEff}}$, and
$\mathcal{A}_{\mathsf{rCause}}$ be as above and let
$\mathcal{M}_{[\mathsf{rEff},\mathsf{rCause}]}$ be the constructed MDP that
contains the set $\mathsf{rCause}_{\mathcal{A}_{\mathsf{rEff}}}$ of reachable
states that have an accepting $\mathcal{A}_{\mathsf{rCause}}$-component. If
$\mathsf{rCause}$ is a co-safety SPR cause for $\mathsf{rEff}$ in
$\mathcal{M}$, then the set of states
$\mathsf{rCause}_{\mathcal{A}_{\mathsf{rEff}}}$ is an SPR cause for
$\\{\mathsf{eff}_{\mathsf{cov}},\mathsf{eff}_{\mathsf{unc}}\\}$ in
$\mathcal{M}_{[\mathsf{rEff},\mathsf{rCause}]}$.

######  Proof 6.8.

Suppose $\mathsf{rCause}$ is a regular SPR cause for $\mathsf{rEff}$ in
$\mathcal{M}$. Let $c\in\mathsf{rCause}_{\mathcal{A}_{\mathsf{rEff}}}$ and let
$\mathfrak{T}$ be a scheduler for
$\mathcal{M}_{[\mathsf{rEff},\mathsf{rCause}]}$ such that
$\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{M}_{[\mathsf{rEff},\mathsf{rCause}]}}(\neg\mathsf{rCause}_{\mathcal{A}_{\mathsf{rEff}}}\,\mathrm{U}\,c)>0$.
Let

$\Pi=\\{\pi\text{ a path in
$\mathcal{M}_{[\mathsf{rEff},\mathsf{rCause}]}$}\mid\pi\vDash\neg\mathsf{rCause}_{\mathcal{A}_{\mathsf{rEff}}}\,\mathrm{U}\,c\text{
and
$\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{M}_{[\mathsf{rEff},\mathsf{rCause}]}}(\pi)>0$}\\}.$

Let $\mathfrak{S}$ be a scheduler for $\mathcal{M}$ mimicking $\mathfrak{T}$
as described in the proof of Lemma 50. Let $\Sigma_{\pi}$ be the set of
$\mathfrak{T}$-paths in $\mathcal{M}$ that correspond to the path $\pi$ in
$\Pi$. I.e., a path $\sigma$ belongs to $\Sigma_{\pi}$ if it moves through the
MECs of $\mathcal{M}$ in the same way as the path $\pi$ moves through the MEC-
quotient until $\sigma$ and $\pi$ reach the state $c$ and if furthermore,
$\sigma$ has positive probability under $\mathfrak{S}$. Now,

$\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{M}_{[\mathsf{rEff},\mathsf{rCause}]}}(\lozenge
E\mid\neg\mathsf{rCause}_{\mathcal{A}_{\mathsf{rEff}}}\,\mathrm{U}\,c)=\frac{\sum_{\pi\in\Pi}\sum_{\sigma\in\Sigma_{\pi}}\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\mathsf{rEff}\mid\sigma)\cdot\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\sigma)}{\sum_{\pi\in\Pi}\sum_{\sigma\in\Sigma_{\pi}}\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\sigma)}.$

All the terms
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\mathsf{rEff}\mid\sigma)$ are
greater than
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\mathsf{rEff})=\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{M}_{[\mathsf{rEff},\mathsf{rCause}]}}(\lozenge
E)$. Hence, we conclude that

$\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{M}_{[\mathsf{rEff},\mathsf{rCause}]}}(\lozenge
E\mid\neg\mathsf{rCause}_{\mathcal{A}_{\mathsf{rEff}}}\,\mathrm{U}\,c)>\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{M}_{[\mathsf{rEff},\mathsf{rCause}]}}(\lozenge
E).$

For checking co-safety SPR causality this is not sufficient. The underlying
problem, in which co-safety SPR causes and SPR causes differ, can be seen in
the following example:

$\mathsf{init}$$b$$d$$c$$t$$\mathsf{noeff}$$\mathsf{eff}$$1/2$$1/4$$1/4$$3/4$$1/4$$\beta$$1/2$$1/2$$\alpha$

Figure 11. An MDP $\mathcal{M}$ for which the reduction from co-safety to
state-based PR causes fails

Consider the MDP $\mathcal{M}$ from Figure 11 with
$\mathsf{rEff}=\lozenge\mathsf{eff}$. For every scheduler $\mathfrak{S}$ with
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\lozenge c)>0$ we have

$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\lozenge\mathsf{eff}\mid\lozenge
c)>\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\lozenge\mathsf{eff})$

and thus $c$ is a state-based SPR cause for $\mathsf{eff}$. On the other hand
for the scheduler $\tau$, which chooses $\alpha$ after the path $\pi=a\;b\;c$
and $\beta$ otherwise ,we have

$\mathrm{Pr}^{\tau}_{\mathcal{M}}(\lozenge\mathsf{eff}\mid\pi)=\frac{1}{2}=\mathrm{Pr}^{\tau}_{\mathcal{M}}(\lozenge\mathsf{eff}).$

Therefore, the desired reduction as in Lemma 50 does not work for
$\mathcal{M}$. Note that the violation of the condition (coS) is only possible
in this example if the scheduler behaves differently depending on how state
$c$ is reached. This different behavior, however, does not have anything to do
with the effect, and potentially different residual properties that have to be
satisfied to achieve the effect; in the example, the effect is just a
reachability property. Furthermore, we want to emphasize that the concrete
probabilities of the individual paths leading to $c$ are important for the
violation. In general, this imposes a major challenge for checking the
condition (coS), for which we do not know a solution. Similar problems arise
when trying to check the existence of a co-safety SPR cause. A witness might
be just one individual path, potentially only together with a scheduler that
realizes this path with very low probability.

####  6.2.2. Computation of quality measures of co-safety causes

Analogously to Section 6.1.2, we can define recall, coverage ratio, and
f-score of co-safety PR causes. With the construction of
$\mathcal{M}_{[\mathsf{rEff},\mathsf{rCause}]}$ and the correspondence between
schedulers $\mathfrak{S}$ for $\mathcal{M}$ and $\mathfrak{T}$ for
$\mathcal{M}_{[\mathsf{rEff},\mathsf{rCause}]}$ satisfying Equations (28)-(30)
established in the proof of Lemma 50, we obtain analogously to the setting of
reachability PR causes:

######  Corollary 52.

Let $\mathcal{M}$ be an MDP and $\mathsf{rEff}\subseteq S^{\omega}$ an
$\omega$-regular language given as DRA $\mathcal{A}_{\mathsf{rEff}}$. Given a
co-safety SPR/GPR cause $\mathsf{rCause}\subseteq S^{\omega}$ by a DFA
$\mathcal{A}_{\mathsf{rCause}}$, we can compute
$\operatorname{\mathit{recall}}(\mathsf{Cause})$,
$\mathit{covrat}(\mathsf{Cause})$ and $\mathit{fscore}(\mathsf{Cause})$ in
polynomial time.

####  6.2.3. Finding optimal co-safety PR causes

Already for reachability PR causes, we have seen that without further
restrictions on the causes we allow, causes might be trivial and intuitively
violate the idea of temporal priority (cf. Section 6.1.3). Hence, also here,
we impose an additional condition, a variation of the condition (TempPrio)
used above: In line with the difference between the definitions of
reachability PR causes and co-safety PR causes, we require that after any good
prefix $\sigma$ of a co-safety cause $\mathsf{rCause}$, the probability that
effect $\mathsf{rEff}$ will occur is not guaranteed to be $1$, i.e., we
require that

$\displaystyle\mathrm{Pr}^{\min}_{\mathcal{M}}(\mathsf{rEff}\mid\sigma)<1\text{
for all good prefixes $\sigma$ of $\mathsf{rCause}$. }$ (TempPrio2)

Unfortunately, we will observe that there are some obstacles in the way when
trying to find optimal co-safety PR causes.

Following the observations from Theorem 36 we can define a canonical co-safety
PR cause which is an optimal co-safety SPR cause for both recall and coverage
ratio. In this fully path-based setting this canonical cause consists of all
minimal paths which are singleton co-safety SPR causes. However, as we are not
aware of a feasible way to check (coS), the computation of this cause is
unclear.

For co-safety GPR causes, the following example illustrates that there might
be no recall-optimal causes that respect (TempPrio2). Intuitively, the reason
is that causes can be pushed arbitrarily close towards a violation of the
probability raising condition while increasing the recall:

$\mathsf{init}$$a$$b$$c$$e$$f$$f$$1/3$$1/3$$1/3$$1/2$$1/2$$3/4$$1/4$$1/4$$3/4$

Figure 12. A Markov chain $\mathcal{M}$ in which the regular effect
$\mathsf{rEff}=\lozenge e$ has no recall-optimal regular PR-cause.

This example will show that there is a Markov chain $\mathcal{M}$ with a state
$e$ such that the effect $\mathsf{rEff}=\lozenge e$ has regular GPR causes
that respect the condition (TempPrio2), but no recall-optimal co-safety GPR
cause that respects (TempPrio2).

Consider the Markov chain $\mathcal{M}$ depicted in Figure 12 with states $S$
and the effect $\mathsf{rEff}=\lozenge e$. First of all, we have that
$\mathrm{Pr}_{\mathcal{M}}(\mathsf{rEff})=2/3$. Furthermore, clearly the cause
$\mathsf{init}\,b\,S^{\omega}$ with the unique minimal good prefix
$\mathsf{init}\,b$ is a regular GPR cause for example as
$\mathrm{Pr}_{\mathcal{M}}(\mathsf{rEff}\mid\mathsf{init}\,b)=3/4$.

Next, note that there cannot be a regular GPR cause $\mathsf{rCause}^{\prime}$
that does not have $\mathsf{init}\,b$ as a minimal good prefix. By (TempPrio2)
the minimal good prefixes are not allowed to end in $e$. Furthermore
$\mathsf{init}$ is clearly also no candidate for a minimal good prefix of
$\mathsf{rCause}^{\prime}$ as that would imply that $\mathsf{rCause}$ consists
of all paths of $\mathcal{M}$ and cannot satisfy the condition (rGPR). If
$\mathsf{init}\,b$ is not a minimal good prefix, hence all minimal good
prefixes have to end in $a$, $c$, or $f$. Afterwards, the probability to reach
$e$ is at most $1/4$ and hence also the probability
$\mathrm{Pr}_{\mathcal{M}}(\mathsf{rEff}\mid\mathsf{rCause}^{\prime})\leq 1/4$
because it is a weighted average of the probabilities
$\mathrm{Pr}_{\mathcal{M}}(\mathsf{rEff}\mid\sigma)\leq 1/4$ of the minimal
good prefixes $\sigma$ of $\mathsf{rCause}^{\prime}$.

So, all regular GPR causes have the minimal good prefix $\mathsf{init}\,b$
together with potentially further minimal good prefixes. Let now

$\mathsf{rCause}_{p}\stackrel{{\scriptstyle\text{\rm\tiny
def}}}{{=}}\mathsf{init}\,b\,S^{\omega}\cup A_{p}$

where $A_{p}$ is a regular subset of the paths $\\{\mathsf{init}\,a^{k}\,c\mid
k\geq 1\\}$ such that all the paths in $A_{p}$ together have probability mass
$\frac{1}{3}p$. Note that we can find such a set $A_{p}$ for a dense set of
values $p\in[0,1]$. We compute

$\mathrm{Pr}_{\mathcal{M}}(\mathsf{rCause}_{p})=\frac{1}{3}(1+p)$

and

$\mathrm{Pr}_{\mathcal{M}}(\mathsf{rCause}_{p}\land\mathsf{rEff})=\frac{1}{4}+\frac{1}{12}p.$

So, we obtain that $\mathsf{rCause}_{p}$ is a regular GPR cause if

$\mathrm{Pr}_{\mathcal{M}}(\mathsf{rEff}\mid\mathsf{rCause}_{p})=\frac{\frac{1}{4}+\frac{1}{12}p}{\frac{1}{3}(1+p)}>\frac{2}{3}=\mathrm{Pr}_{\mathcal{M}}(\mathsf{rEff}).$

After multiplying the inequality with $12(1+p)$, we see that this holds iff
$9+3p>8+8p$ iff $p<\frac{1}{5}$. The recall of $\mathsf{rCause}_{p}$ is now

$\mathrm{Pr}_{\mathcal{M}}(\mathsf{rCause}_{p}\mid\mathsf{rEff})=\frac{\frac{1}{4}+\frac{1}{12}p}{2/3}=\frac{3}{8}+\frac{1}{8}p.$

So, among the co-safety GPR causes of the form $\mathsf{rCause}_{p}$, there is
no recall-optimal one. For $p$ tending to $1/5$ from below, the recall always
increases. Note also that an $\varepsilon$-recall-optimal co-safety GPR cause
for $\varepsilon>0$ must take a very complicated form. It has to select paths
of the form $\mathsf{init}\,a^{k}\,c$ that have probability $\frac{1}{3\cdot
2^{k}}$ such that there probability adds up to a value less than, but close to
$\frac{1}{15}$. $\lhd$

We have seen that for recall-optimal (and hence coverage ratio-optimal) SPR
causes for an effect given by $\mathcal{A}_{\mathsf{rEff}}$, we can provide a
characterization of the canonical cause. How to compute this cause, however,
is unclear as we do not know how to check the co-safety SPR condition and as
there might be some paths ending in a given state in the product of
$\mathcal{M}$ and $\mathcal{A}_{\mathsf{rEff}}$ that belong to the canonical
cause while other paths ending in that state do not. For co-safety GPR causes,
we have even seen that there might be no (non-trivial) optimal causes and that
causes close to the optimum can be required to take a very complicated shape.
As the f-score is a more involved quality measure than the recall, we cannot
expect that the search for f-score optimal causes is simpler. It seems to be
likely that the situation is at least as bad as for recall-optimal causes if
not worse.

##  7\. Conclusion

In this work we formalized the probability-raising principle in MDPs and
studied several quality notions for probability-raising causes. We covered
fundamental algorithmic problems for both the strict (local) and global view,
where we considered a basic state-based setting in which cause and effect are
given as sets of states. We extended this setting to $\omega$-regular path
properties as effects in two ways. In a more simple setting we kept causes as
sets of states and in a more general approach considered co-safety path
properties as causes.

### Strict vs. Global probability raising

In our basic setting of state-based cause-effect relations, our results
indicate that GPR causes are more general overall by leaving more flexibility
to achieve better quality measures, while algorithmic reasoning on SPR causes
is simpler. This changed when extending the framework by considering
$\omega$-regular effects given by a deterministic Rabin automaton. Our results
mainly stem from a polynomial reduction from $\omega$-regular effects to
reachability effects (Lemma 42). The caveat here is that the strict PR
condition translates to a global PR condition after this transformation, which
increases the algorithmic complexity of reachability SPR causes to the level
of reachability GPR causes. Thus, the strict probability-raising loses its
advantage over the global perspective. Furthermore, when considering causes as
co-safety path properties we observe increasing difficulties to handle strict
probability-raising. This stems from an underlying problem in the approach of
strict probability-raising applied to path properties. As we consider cause-
effect relations between these properties, it is somewhat unnatural to require
each individual path to raise the probability of the effect property. Rather,
it is more natural to say a path property as a whole causes another one,
instead of saying all possible realizations of a path property cause another
one. This means that co-safety GPR causes also seem more natural than co-
safety SPR causes from a philosophical standpoint.

### Non-strict inequality in the PR conditions

The approach of probability-raising within this work is in line with the
classical notion in literature that uses a strict inequality in the PR
condition. As a consequence causes might not exist (see Example 2). However,
relaxing the PR condition by only requiring a non-strict inequality would
apparently be a minor change that broadens the choice of causes. Indeed, the
proposed algorithms for checking the SPR and GPR condition for reachability
effects (Section 4) can easily be modified for the relaxed definition. As the
algorithms of both extended settings discussed in Section 6 stem mainly from a
reduction to reachability effects this also holds for reachability and co-
safety causes of regular effects. However, a non-strict inequality in the PR
condition would lead to a questionable notion of causality, as e.g.
$\\{\mathsf{init}\\}$ would always be a recall- and ratio-optimal cause. Thus,
other side constraints are be needed in order to make use of the relaxed PR
condition. E.g., requiring the non-strict inequality for all schedulers that
reach a cause with positive probability and also requiring the existence of a
witnessing scheduler for the PR condition with strict inequality might be a
useful alternative definition which agrees with Def. 3 for Markov chains.

### Relaxing the minimality condition

As many causality notions in the literature include some minimality
constraint, we included the condition
$\mathrm{Pr}^{\max}_{\mathcal{M}}(\neg\mathsf{Cause}\,\mathrm{U}\,c)>0$ for
all states of $\mathsf{Cause}$ in the state-based setting and for reachability
PR causes of regular effects. However, this requirement could be dropped
without affecting the algorithmic results presented here. This can be useful
when the task is to identify components or agents which are responsible for
the occurrences of undesired effects. In these cases the cause candidates are
fixed (e.g., for each agent $i$, the set of states controlled by agent $i$),
but some of them might violate the minimality condition.

### Future directions

In this work we considered type-like causality where cause-effect relations
are defined within the model without needing an actual execution that shows
the effect. Hence, causes are considered in a forward-looking manner. Notions
of probabilistic backward causality that take a concrete execution of the
system into account and considerations on PR causality with external
interventions as in Pearl’s do-calculus [Pea09] are left for future work.

## Acknowledgments

We would like to thank Florian Funke, Simon Jantsch and Clemens Dubslaff for
their helpful comments and feedback on the topic of causality in MDPs. We
especially thank Simon Jantsch for pointing out improvements of prior results
(wrt. [BFPZ22]).

## References