11institutetext: Technische Universität Dresden
11email: {christel.baier, florian.funke, jakob.piribauer,robin.ziemek}@tu-
dresden.de

# On probability-raising causality
in Markov decision processes ††thanks: This work was funded by DFG grant
389792660 as part of TRR 248, the Cluster of Excellence EXC 2050/1 (CeTI,
project ID 390696704, as part of Germany’s Excellence Strategy), DFG-projects
BA-1679/11-1 and BA-1679/12-1,and the RTG QuantLA (GRK 1763).

Christel Baier(✉)  Florian Funke  Jakob Piribauer(✉)  Robin Ziemek(✉)

###### Abstract

The purpose of this paper is to introduce a notion of causality in Markov
decision processes based on the probability-raising principle and to analyze
its algorithmic properties. The latter includes algorithms for checking cause-
effect relationships and the existence of probability-raising causes for given
effect scenarios. Inspired by concepts of statistical analysis, we study
quality measures (recall, coverage ratio and f-score) for causes and develop
algorithms for their computation. Finally, the computational complexity for
finding optimal causes with respect to these measures is analyzed.

Related version: This is the extended version of the conference version
accepted for publication at FoSSaCS 2022.

##  1 Introduction

As modern software systems control more and more aspects of our everyday
lives, they grow increasingly complex. Even small changes to a system might
cause undesired or even disastrous behavior. Therefore, the goal of modern
computer science does not only lie in the development of powerful and
versatile systems, but also in providing comprehensive techniques to
understand these systems. In the area of formal verification, counterexamples,
invariants and related certificates are often used to provide a verifiable
justification that a system does or does not behave according to a
specification (see e.g., [29, 15, 31]). These, however, provide only
elementary insights on the system behavior. Thus, there is a growing demand
for a deeper understanding on _why_ a system satisfies or violates a
specification and _how_ different components influence the performance. The
analysis of causal relations between events occurring during the execution of
a system can lead to such understanding. The majority of prior work in this
direction relies on causality notions based on Lewis’ counterfactual principle
[28] stating the effect would not have occurred if the cause would not have
happened. A prominent formalization of the counterfactual principle is given
by Halpern and Pearl [20] via structural equation models. This inspired formal
definitions of causality and related notions of blameworthiness and
responsibility in Kripke and game structures (see, e.g., [14, 10, 13, 39, 18,
40, 7]).

In this work, we approach the concept of causality in a probabilistic setting,
where we focus on the widely accepted _probability-raising principle_ which
has its roots in philosophy [37, 38, 17, 21] and has been refined by Pearl
[34] for causal and probabilistic reasoning in intelligent systems. The
different notions of probability-raising cause-effect relations discussed in
the literature share the following two main principles:

(C1)

Causes raise the probabilities for their effects, informally expressed by the
requirement
“$\mathrm{Pr}(\,\text{effect}\,|\,\text{cause}\,)>\mathrm{Pr}(\,\text{effect}\,)$”.

(C2)

Causes must happen before their effects.

Despite the huge amount of work on probabilistic causation in other
disciplines, research on probability-raising causes in the context of formal
methods is comparably rare and has concentrated on Markov chains (see, e.g.,
[23, 24, 6] and the discussion of related work in Section 3.2). To the best of
our knowledge, probabilistic causation for probabilistic operational models
with nondeterminism has not been studied before.

We formalize the principles (C1) and (C2) for Markov decision processes
(MDPs), a standard operational model combining probabilistic and non-
deterministic behavior, and concentrate on reachability properties where both
cause and effect are given as sets of states. Condition (C1) can be
interpreted in two natural ways in this setting: On one hand, the probability-
raising property can be locally required for each element of the cause. Such
causes are called _strict probability-raising (SPR) causes_ in our framework.
This interpretation is especially suited when the task is to identify system
states that have to be avoided for lowering the effect probability. On the
other hand, one might want to treat the cause set globally as a unit in (C1)
leading to the notion of _global probability-raising (GPR) cause_. Considering
the cause set as a whole is better suited when further constraints are imposed
on the candidates for cause set. This might apply, e.g., when the set of non-
terminal states of the given MDP is partitioned into sets of states $S_{i}$
under the control of an agent $i$, $1\leq i\leq k$. For the task to identify
which agent’s decisions cause the effect only the subsets of
$S_{1},\ldots,S_{k}$ are candidates for causes. Furthermore, global causes are
more appropriate when causes are used for monitoring purposes under partial
observability constraints as then the cause candidates are sets of
indistinguishable states.

Table 1: Complexity results for MDPs and Markov chains (MC) with fixed effect
set

for fixed set $\mathsf{Cause}$ find optimal cause compute quality values check
PR condition covratio-optimal = recall-optimal (recall, covratio, f-score)
f-score-optimal SPR $\in\mathrm{P}$ poly-time poly-time poly-space poly-time
for MC threshold problem $\in\mathrm{NP}\cap\mathrm{coNP}$ GPR
$\in\mathrm{PSPACE}$ and $\in\mathrm{P}$ for MC poly-time poly-space threshold
problems $\in\mathrm{PSPACE}$ and $\mathrm{NP}$-hard and
$\mathrm{NP}$-complete for MC

Different causes for an effect according to our definition can differ
substantially regarding how well they predict the effect and how well the
executions exhibiting the cause cover the executions showing the effect.
Taking inspiration from measures used in statistical analysis (see, e.g.,
[35]), we introduce quality measures that allow us to compare causes and to
look for optimal causes: The _recall_ captures the probability that the effect
is indeed preceded by the cause. The _coverage-ratio_ quantifies the fraction
of the probability that cause and effect are observed and the probability that
the effect but not the cause is observed. Finally, the _f-score_ , a widely
used quality measure for binary classifiers, is the harmonic mean of recall
and precision, i.e., the probability that the cause is followed by the effect.

Contributions. The goal of this work are the mathematical and algorithmic
foundations of probabilistic causation in MDPs based on (C1) and (C2). We
introduce strict and global probability-raising causes in MDPs (Section 3).
Algorithms are provided to check whether given cause and effect sets satisfy
(one of) the probability-raising conditions (Section 4.1 and 4.2) and to check
the existence of causes for a given effect (Section 4.1). In order to evaluate
the coverage properties of a cause, we subsequently introduce the above-
mentioned quality measures (Section 5.1). We give algorithms for computing
these values for given cause-effect relations (Section 5.2) and characterize
the computational complexity of finding optimal causes wrt. to the different
measures (Section 5.3). Table 1 summarizes our complexity results. Omitted
proofs can be found in the appendix.

##  2 Preliminaries

Throughout the paper, we will assume some familiarity with basic concepts of
Markov decision processes. Here, we only present a brief summary of the
notations used in the paper. For more details, we refer to [36, 8, 22].

A _Markov decision process (MDP)_ is a tuple
$\mathcal{M}=(S,\mathit{Act},P,\mathsf{init})$ where $S$ is a finite set of
states, $\mathit{Act}$ a finite set of actions, $\mathsf{init}\in S$ the
initial state and $P:S\times\mathit{Act}\times S\to[0,1]$ the transition
probability function such that $\sum_{t\in S}P(s,\alpha,t)\in\\{0,1\\}$ for
all states $s\in S$ and actions $\alpha\in\mathit{Act}$. An action $\alpha$ is
_enabled_ in state $s\in S$ if $\sum_{t\in S}P(s,\alpha,t)=1$. We define
$\mathit{Act}(s)=\\{\alpha\mid\alpha\text{ is enabled in }s\\}$. A state $t$
is _terminal_ if $\mathit{Act}(t)=\emptyset$. A Markov chain (MC) is a special
case of an MDP where $\mathit{Act}$ is a singleton (we then write $P(s,u)$
rather than $P(s,\alpha,u)$). A _path_ in an MDP $\mathcal{M}$ is a (finite or
infinite) alternating sequence
$\pi=s_{0}\,\alpha_{0}\,s_{1}\,\alpha_{1}\,s_{2}\dots\in(S\times\mathit{Act})^{*}\cup(S\times\mathit{Act})^{\omega}$
such that $P(s_{i},\alpha_{i},s_{i+1})>0$ for all indices $i$. A path is
called maximal if it is infinite or finite and ends in a terminal state. An
MDP can be interpreted as a Kripke structure in which transitions go from
states to probability distributions over states.

A _(randomized) scheduler_ $\mathfrak{S}$ is a function that maps each finite
non-maximal path $s_{0}\alpha_{0}\dots\alpha_{n-1}s_{n}$ to a distribution
over $\mathit{Act}(s_{n})$. $\mathfrak{S}$ is called deterministic if
$\mathfrak{S}(\pi)$ is a Dirac distribution for all finite non-maximal paths
$\pi$. If the chosen action only depends on the last state of the path,
$\mathfrak{S}$ is called _memoryless_. We write MR for the class of memoryless
(randomized) and MD for the class of memoryless deterministic schedulers.
_Finite-memory_ schedulers are those that are representable by a finite-state
automaton.

The scheduler $\mathfrak{S}$ of $\mathcal{M}$ induces a (possibly infinite)
Markov chain. We write $\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M},s}$ for the
standard probability measure on measurable sets of maximal paths in the Markov
chain induced by $\mathfrak{S}$ with initial state $s$. If $\varphi$ is a
measurable set of maximal paths, then
$\mathrm{Pr}^{\max}_{\mathcal{M},s}(\varphi)$ and
$\mathrm{Pr}^{\min}_{\mathcal{M},s}(\varphi)$ denote the supremum resp.
infimum of the probabilities for $\varphi$ under all schedulers. We use the
abbreviation
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}=\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M},\mathsf{init}}$
and notations $\mathrm{Pr}^{\max}_{\mathcal{M}}$ and
$\mathrm{Pr}^{\min}_{\mathcal{M}}$ for extremal probabilities. Analogous
notations will be used for expectations. So, if $f$ is a random variable,
then, e.g., $\mathrm{E}^{\mathfrak{S}}_{\mathcal{M}}(f)$ denotes the
expectation of $f$ under $\mathfrak{S}$ and
$\mathrm{E}^{\max}_{\mathcal{M}}(f)$ its supremum over all schedulers. We use
LTL-like temporal modalities such as $\Diamond$ (eventually) and
$\,\mathrm{U}\,$ (until) to denote path properties. For $X,T\subseteq S$ the
formula $X\,\mathrm{U}\,T$ is satisfied by paths $\pi=s_{0}s_{1}\dots$ such
that there exists $j\geq 0$ such that for all $i<j:s_{i}\in X$ and $s_{j}\in
T$ and $\Diamond T=S\,\mathrm{U}\,T$. It is well-known that
$\mathrm{Pr}^{\min}_{\mathcal{M}}(X\,\mathrm{U}\,T)$ and
$\mathrm{Pr}^{\max}_{\mathcal{M}}(X\,\mathrm{U}\,T)$ and corresponding optimal
MD-schedulers are computable in polynomial time.

If $s\in S$ and $\alpha\in\mathit{Act}(s)$, then $(s,\alpha)$ is said to be a
state-action pair of $\mathcal{M}$. An _end component_ (EC) of an MDP
$\mathcal{M}$ is a strongly connected sub-MDP containing at least one state-
action pair. ECs will be often identified with the set of their state-action
pairs. An EC $\mathcal{E}$ is called maximal (abbreviated MEC) if there is no
proper superset $\mathcal{E}^{\prime}$ of (the set of state-action pairs of)
$\mathcal{E}$ which is an EC.

##  3 Strict and global probability-raising causes

We now provide formal definitions for cause-effect relations in MDPs which
rely on the probability-raising (PR) principle as stated by (C1) and (C2) in
the introduction. We focus on the case where both causes and effects are state
properties, i.e., sets of states.

In the sequel, let $\mathcal{M}=(S,\mathit{Act},P,\mathsf{init})$ be an MDP
and $\mathsf{Eff}\subseteq S\setminus\\{\mathsf{init}\\}$ a nonempty set of
terminal states. (Dealing with a fixed effect set, the assumption that all
effect states are terminal is justified by (C2).) Furthermore, we may assume
that every state $s\in S$ is reachable from $\mathsf{init}$. Proofs for the
results of this section are provided in Appendix 0.B.

We consider here two variants of the probability-raising condition: the global
setting treats the set $\mathsf{Cause}$ as a unit, while the strict view
requires the probability-raising condition for all states in $\mathsf{Cause}$
individually.

######  Definition 1 (Global and strict probability-raising cause (GPR/SPR
cause))

Let $\mathcal{M}$ and $\mathsf{Eff}$ be as above and $\mathsf{Cause}$ a
nonempty subset of $S\setminus\mathsf{Eff}$. Then, $\mathsf{Cause}$ is said to
be a _GPR cause_ for $\mathsf{Eff}$ iff the following two conditions (G) and
(M) hold:

  1. (G)

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

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

  2. (M)

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$.

$\mathsf{Cause}$ is called an _SPR cause_ for $\mathsf{Eff}$ iff (M) and the
following condition (S) hold:

  1. (S)

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$:

$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\ \Diamond\mathsf{Eff}\ |\
(\neg\mathsf{Cause})\,\mathrm{U}\,c\ )\ >\
\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{Eff}).$ (SPR)

Condition (M) can be seen as a minimality requirement as states
$c\in\mathsf{Cause}$ that are not accessible from $\mathsf{init}$ without
traversing other states in $\mathsf{Cause}$ could be omitted without affecting
the true positives (events where an effect state is reached after visiting a
cause state, “covered effects”) or false negatives (events where an effect
state is reached without visiting a cause state before, “uncovered effect”).
More concretely, whenever a set $C\subseteq S\setminus\mathsf{Eff}$ satisfies
conditions (G) or (S) then the set $\mathsf{Cause}$ of states $c\in C$ where
$\mathcal{M}$ has a path from $\mathsf{init}$ satisfying $(\neg
C)\,\mathrm{U}\,c$ is a GPR resp. an SPR cause.

###  3.1 Examples and simple properties of probability-raising causes

We first observe that SPR/GPR causes cannot contain the initial state
$\mathsf{init}$, since otherwise an equality instead of an inequality would
hold in (GPR) and (SPR). Furthermore as a direct consequence of the
definitions and using the equivalence of the LTL formulas
$\Diamond\mathsf{Cause}$ and
$(\neg\mathsf{Cause})\,\mathrm{U}\,\mathsf{Cause}$ we obtain:

######  Lemma 1 (Singleton PR causes)

If $\mathsf{Cause}$ is a singleton then $\mathsf{Cause}$ is a SPR cause for
$\mathsf{Eff}$ if and only if $\mathsf{Cause}$ is a GPR cause for
$\mathsf{Eff}$.

As the event $\Diamond\mathsf{Cause}$ is a disjoint union of all events
$(\neg\mathsf{Cause})\,\mathrm{U}\,c$ with $c\in\mathsf{Cause}$, the
probability for covered effects $\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\
\Diamond\mathsf{Eff}\ |\ \Diamond\mathsf{Cause}\ )$ is a weighted average of
the probabilities $\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\
\Diamond\mathsf{Eff}\ |\ (\neg\mathsf{Cause})\,\mathrm{U}\,c\ )$ for
$c\in\mathsf{Cause}$. This yields:

[Strict implies global]lemmastrictimpliesglobal Every SPR cause for
$\mathsf{Eff}$ is a GPR cause for $\mathsf{Eff}$.

######  Example 1 (Non-strict GPR cause)

Consider the Markov chain $\mathcal{M}$ depicted below where the nodes
represent states and the directed edges represent transitions labeled with
their respective probabilities. Let $\mathsf{Eff}=\\{\mathsf{eff}\\}$. Then,
$\mathrm{Pr}_{\mathcal{M}}(\Diamond\mathsf{Eff})=\frac{1}{3}\,+\,\frac{1}{3}\cdot\frac{1}{4}\,+\,\frac{1}{12}=\frac{1}{2}$,
$\mathrm{Pr}_{\mathcal{M}}(\Diamond\mathsf{Eff}|\Diamond
c_{1})=\mathrm{Pr}_{\mathcal{M},c_{1}}(\Diamond\mathsf{eff})=1$ and
$\mathrm{Pr}_{\mathcal{M}}(\Diamond\mathsf{Eff}|\Diamond
c_{2})=\mathrm{Pr}_{\mathcal{M},c_{2}}(\Diamond\mathsf{eff})=\frac{1}{4}$.
Thus, $\\{c_{1}\\}$ is both an SPR and a GPR cause for $\mathsf{Eff}$, while
$\\{c_{2}\\}$ is not. The set $\mathsf{Cause}=\\{c_{1},c_{2}\\}$ is a non-
strict GPR cause for $\mathsf{Eff}$ as:

$\mathrm{Pr}_{\mathcal{M}}(\ \Diamond\mathsf{Eff}\ |\ \Diamond\mathsf{Cause}\
)=(\frac{1}{3}+\frac{1}{3}\cdot\frac{1}{4})/(\frac{1}{3}+\frac{1}{3})=(\frac{5}{12})/(\frac{2}{3})=\frac{5}{8}>\frac{1}{2}=\mathrm{Pr}_{\mathcal{M}}(\Diamond\mathsf{Eff})$.

The second condition (M) is obviously fulfilled. Non-strictness follows from
the fact that the SPR condition does not hold for state $c_{2}$. $\lhd$

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

######  Example 2 (Probability-raising causes might not exist)

PR causes might not exist, even if $\mathcal{M}$ is a Markov chain. This
applies, e.g., to the Markov chain $\mathcal{M}$ with two states
$\mathsf{init}$ and $\mathsf{eff}$ where $P(\mathsf{init},\mathsf{eff})=1$ and
the effect set $\mathsf{Eff}=\\{\mathsf{eff}\\}$. The only cause candidate is
the singleton $\\{\mathsf{init}\\}$. However, the strict inequality in (GPR)
or (SPR) does not hold for $\mathsf{Cause}=\\{\mathsf{init}\\}$. The same
phenomenon occurs if all non-terminal states of a Markov chain reach the
effect states with the same probability. In such cases, however, the non-
existence of PR causes is well justified as the events $\Diamond\mathsf{Eff}$
and $\Diamond\mathsf{Cause}$ are stochastically independent for every set
$\mathsf{Cause}\subseteq S\setminus\mathsf{Eff}$. $\lhd$

######  Remark 1 (Memory needed for refuting PR condition)

Let $\mathcal{M}$ be the MDP in Figure 2, where the notation is similar to
Example 2 with the addition of actions $\alpha,\beta$ and $\gamma$. Let
$\mathsf{Cause}=\\{c\\}$ and $\mathsf{Eff}=\\{\mathsf{eff}\\}$. Only state $s$
has a nondeterministic choice. $\mathsf{Cause}$ is not an PR cause. To see
this, regard the deterministic scheduler $\mathfrak{T}$ that schedules $\beta$
only for the first visit of $s$ and $\alpha$ for the second visit of $s$.
Then:

$\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{M}}(\Diamond\mathsf{eff})\ =\
\frac{1}{2}\cdot\frac{1}{2}\,+\,\frac{1}{2}\cdot\frac{1}{2}\cdot
1\cdot\frac{1}{4}\ =\ \frac{5}{16}\ >\ \frac{1}{4}\ =\
\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{M}}(\Diamond\mathsf{eff}|\Diamond c)$

Denote the MR schedulers reaching $c$ with positive probability as
$\mathfrak{S}_{\lambda}$ with $\mathfrak{S}_{\lambda}(s)(\alpha)$ $=$
$\lambda$ and $\mathfrak{S}_{\lambda}(s)(\beta)=1{-}\lambda$ for some
$\lambda\in\,[0,1[$. Then,
$\mathrm{Pr}^{\mathfrak{S}_{\lambda}}_{\mathcal{M},s}(\Diamond\mathsf{eff})>0$
and:

$\mathrm{Pr}^{\mathfrak{S}_{\lambda}}_{\mathcal{M}}(\Diamond\mathsf{eff})\ =\
\frac{1}{2}\cdot\mathrm{Pr}^{\mathfrak{S}_{\lambda}}_{\mathcal{M},s}(\Diamond\mathsf{eff})\
<\ \mathrm{Pr}^{\mathfrak{S}_{\lambda}}_{\mathcal{M},s}(\Diamond\mathsf{eff})\
=\ \mathrm{Pr}^{\mathfrak{S}_{\lambda}}_{\mathcal{M},c}(\Diamond\mathsf{eff})\
=\
\mathrm{Pr}^{\mathfrak{S}_{\lambda}}_{\mathcal{M}}(\Diamond\mathsf{eff}|\Diamond
c)$

Thus, the SPR/GPR condition holds for $\mathsf{Cause}$ and $\mathsf{Eff}$
under all memoryless schedulers reaching $\mathsf{Cause}$ with positive
probability, although $\mathsf{Cause}$ is not an PR cause. $\lhd$

$\mathsf{init}$$\mathsf{noeff}$$s$$\mathsf{eff}$$c$$\gamma\mid 1/2$$\gamma\mid
1/2$$3/4$$1/4$$1/2$$1/2$$\gamma\mid 1$$\alpha$$\beta$

Figure 1: MDP $\mathcal{M}$ from Remark 1

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

Figure 2: MDP $\mathcal{M}$ from Remark 2

######  Remark 2 (Randomization needed for refuting PR condition)

Consider the MDP $\mathcal{M}$ of Figure 2. Let
$\mathsf{Eff}=\\{\mathsf{eff}_{\mathsf{unc}},\mathsf{eff}_{\mathsf{cov}}\\}$
and $\mathsf{Cause}=\\{c\\}$. The two MD-schedulers $\mathfrak{S}_{\alpha}$
and $\mathfrak{S}_{\beta}$ that select $\alpha$ resp. $\beta$ for the initial
state $\mathsf{init}$ are the only deterministic schedulers. As
$\mathfrak{S}_{\alpha}$ does not reach $c$, it is irrelevant for the SPR or
GPR condition. $\mathfrak{S}_{\beta}$ satisfies (SPR) and (GPR) as
$\mathrm{Pr}^{\mathfrak{S}_{\beta}}_{\mathcal{M}}(\Diamond\mathsf{Eff}|\Diamond
c)=\frac{1}{2}>\frac{1}{4}=\mathrm{Pr}^{\mathfrak{S}_{\beta}}_{\mathcal{M}}(\Diamond\mathsf{Eff})$.
The MR scheduler $\mathfrak{T}$ which selects $\alpha$ and $\beta$ with
probability $\frac{1}{2}$ in $\mathsf{init}$ reaches $c$ with positive
probability and violates (SPR) and (GPR) as
$\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{M}}(\Diamond\mathsf{Eff}|\Diamond
c)=\frac{1}{2}<\frac{5}{8}=\frac{1}{2}+\frac{1}{2}\cdot\frac{1}{2}\cdot\frac{1}{2}=\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{M}}(\Diamond\mathsf{Eff})$.
$\lhd$

######  Remark 3 (Cause-effect relations for regular classes of schedulers)

The definitions of PR causes in MDPs impose constraints for all schedulers
reaching a cause state. This condition is fairly strong and can often lead to
the phenomenon that no PR cause exists. Replacing $\mathcal{M}$ with an MDP
resulting from the synchronous parallel composition of $\mathcal{M}$ with a
deterministic finite automaton representing a regular constraint on the
scheduled state-action sequences (e.g., “alternate between actions $\alpha$
and $\beta$ in state $s$” or “take $\alpha$ on every third visit to state $s$
and actions $\beta$ or $\gamma$ otherwise”) leads to a weaker notion of PR
causality. This can be useful to obtain more detailed information on cause-
effect relationships in special scenarios, be it at design time where multiple
scenarios (regular classes of schedulers) are considered or for a post-hoc
analysis where one seeks for the causes of an occurred effect and where
information about the scheduled actions is extractable from log files or the
information gathered by a monitor. $\lhd$

######  Remark 4 (Action causality and other forms of PR causality)

Our notions of PR causes are purely state-based with PR conditions that
compare probabilities under the same scheduler. However, in combination with
model transformations, the proposed notions of PR causes are also applicable
for reasoning about other forms of PR causality.

Suppose, the task is to check whether taking action $\alpha$ in state $s$
raises the effect probabilities compared to never scheduling $\alpha$ in state
$s$. Let $\mathcal{M}_{0}$ and $\mathcal{M}_{1}$ be copies of $\mathcal{M}$
with the following modifications: In $\mathcal{M}_{0}$, the only enabled
action of state $s$ is $\alpha$, while in $\mathcal{M}_{1}$ the enabled
actions of state $s$ are the elements of
$\mathit{Act}_{\mathcal{M}}(s)\setminus\\{\alpha\\}$. Let now $\mathcal{N}$ be
the MDP whose initial state has a single enabled action and moves with
probability $1/2$ to $\mathcal{M}_{0}$ and $\mathcal{M}_{1}$. Then, action
$\alpha$ raises the effect probability in $\mathcal{M}$ iff the initial state
of $\mathcal{M}_{0}$ consitutes an SPR cause in $\mathcal{N}$. This idea can
be generalized to check whether scheduler classes satisfying a regular
constraint have higher effect probability compared to all other schedulers. In
this case, we can deal with an MDP $\mathcal{N}$ as above where
$\mathcal{M}_{0}$ and $\mathcal{M}_{1}$ are defined as the synchronous product
of deterministic finite automata and $\mathcal{M}$. $\lhd$

###  3.2 Related work

Previous work in the direction of probabilistic causation in stochastic
operational models has mainly concentrated on Markov chains. Kleinberg [23,
24] introduced _prima facie causes_ in finite Markov chains where both causes
and effects are formalized as PCTL state formulae, and thus they can be seen
as sets of states as in our approach. The correspondence of Kleinberg’s PCTL
constraints for prima facie causes and the strict probability-raising
condition formalized using conditional probabilities has been worked out in
the survey article [5]. Our notion of SPR causes corresponds to Kleinberg’s
prima facie causes, except for the minimality condition (M). Ábrahám et al [1]
introduces a hyperlogic for Markov chains and gives a formalization of
probabilistic causation in Markov chains as a hyperproperty, which is
consistent with Kleinberg’s prima facie causes, and with SPR causes up to
minimality. Cause-effect relations in Markov chains where effects are
$\omega$-regular properties has been introduced in [6]. It relies on strict
probability-raising condition, but requires completeness in the sense that
every path where the effect occurs has a prefix in the cause set. The paper
[6] permits a non-strict inequality in the SPR condition with the consequence
that causes always exist, which is not the case for our notions.

The survey article [5] introduces notions of global probability-raising causes
for Markov chains where causes and effects can be path properties. [5]’s
notion of _reachability causes_ in Markov chains directly corresponds to our
notion GPR causes, the only difference being that [5] deals with a relaxed
minimality condition and requires that the cause set is reachable without
visiting an effect state before. The latter is inherent in our approach as we
suppose that all states are reachable and the effect states are terminal.

To the best of our knowledge, probabilistic causation in MDPs has not been
studied before. The only work in this direction we are aware of is the recent
paper by Dimitrova et al [16] on a hyperlogic, called PHL, for MDPs. While the
paper focuses on the foundation of PHL, it contains an example illustrating
how action causality can be formalized as a PHL formula. Roughly, the
presented formula expresses that taking a specific action $\alpha$ increases
the probability for reaching effect states. Thus, it also relies on the
probability-raising principle, but compares the “effect probabilities” under
different schedulers (which either schedule $\alpha$ or not) rather than
comparing probabilities under the same scheduler as in our PR condition.
However, as Remark 4 argues, to some extent our notions of PR causes can
reason about action causality as well.

There has also been work on causality-based explanations of counterexamples in
probabilistic models [26, 27]. The underlying causality notion of this work,
however, relies on the non-probabilistic counterfactual principle rather than
the probability-raising condition. The same applies to the notions of forward
and backward responsibility in stochastic games in extensive form introduced
in the recent work [7].

##  4 Checking the existence of PR causes and the PR conditions

We now turn to algorithms for checking whether a given set $\mathsf{Cause}$ is
an SPR or GPR cause for $\mathsf{Eff}$. As condition (M) of SPR and GPR causes
is verifiable by standard model checking techniques in polynomial time, we
concentrate on checking the probability-raising conditions (SPR) and (GPR).
For Markov chains, both (SPR) and (GPR) can be checked in polynomial time by
computing the corresponding probabilities. So, the interesting case is
checking the PR conditions in MDPs. In case of SPR causality, this is closely
related to the existence of PR causes and solvable in polynomial time (Section
4.1), while checking the GPR condition is more complex and polynomially
reducible to (the non-solvability of) a quadratic constraint system (Section
4.2). All proofs and omitted details to this section can be found in Appendix
0.C.

We start by stating that for the SPR and GPR condition, it suffices to
consider schedulers minimizing the probability to reach an effect state from
every cause state.

######  Notation 4.1 (MDP with minimal effect probabilities from cause
candidates)

If $C\subseteq S$ then we write $\mathcal{M}_{[C]}$ for the MDP resulting from
$\mathcal{M}$ by removing all enabled actions of the states in $C$. Instead,
$\mathcal{M}_{[C]}$ has a new action $\gamma$ that is enabled exactly in the
states $s\in C$ with the transition probabilities
$P_{\mathcal{M}_{[C]}}(s,\gamma,\mathsf{eff})=\mathrm{Pr}^{\min}_{\mathcal{M},s}(\Diamond\mathsf{Eff})$
and
$P_{\mathcal{M}_{[C]}}(s,\gamma,\mathsf{noeff})=1{-}\mathrm{Pr}^{\min}_{\mathcal{M},s}(\Diamond\mathsf{Eff})$.
Here, $\mathsf{eff}$ is a fixed state in $\mathsf{Eff}$ and $\mathsf{noeff}$ a
(possibly fresh) terminal state not in $\mathsf{Eff}$. We write
$\mathcal{M}_{[c]}$ if $C=\\{c\\}$ is a singleton.

lemmawmincriterionPRcauses Let $\mathcal{M}=(S,\mathit{Act},P,\mathsf{init})$
be an MDP and $\mathsf{Eff}\subseteq S$ a set of terminal states. Let
$\mathsf{Cause}\subseteq S\setminus\mathsf{Eff}$. Then, $\mathsf{Cause}$ is an
SPR cause (resp. a GPR cause) for $\mathsf{Eff}$ in $\mathcal{M}$ if and only
if $\mathsf{Cause}$ is an SPR cause (resp. a GPR cause) for $\mathsf{Eff}$ in
$\mathcal{M}_{[\mathsf{Cause}]}$.

###  4.1 Checking the strict probability-raising condition and the existence
of causes

The basis of both checking the existence of PR causes or checking the SPR
condition for a given cause candidate is the following polynomial time
algorithm to check whether the SPR condition holds in a given state $c$ of
$\mathcal{M}$ for all schedulers $\mathfrak{S}$ with
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond c)>0$:

###### Algorithm 4.2

Input: state $c\in S$, set of terminal states $\mathsf{Eff}\subseteq S$; Task:
Decide whether (SPR) holds in $c$ for all schedulers $\mathfrak{S}$.

Compute $w_{c}=\mathrm{Pr}^{\min}_{\mathcal{M},c}(\Diamond\mathsf{Eff})$ and
$q_{s}=\mathrm{Pr}^{\max}_{\mathcal{M}_{[c]},s}(\Diamond\mathsf{Eff})$ for
each state $s$ in $\mathcal{M}_{[c]}$ .

  1. 1.

If $q_{\mathsf{init}}<w_{c}$, then return “yes, (SPR) holds for $c$”.

  2. 2.

If $q_{\mathsf{init}}>w_{c}$, then return “no, (SPR) does not hold for $c$”.

  3. 3.

Suppose $q_{\mathsf{init}}=w_{c}$. Let
$A(s)=\\{\alpha\in\mathit{Act}_{\mathcal{M}_{[c]}}(s)\mid q_{s}=\sum_{t\in
S_{[c]}}P_{\mathcal{M}_{[c]}}(s,\alpha,t)\cdot q_{t}\\}$ for each non-terminal
state $s$. Let $\mathcal{M}^{\max}_{[c]}$ denote the sub-MDP of
$\mathcal{M}_{[c]}$ induced by the state-action pairs $(s,\alpha)$ where
$\alpha\in A(s)$.

    1. 3.1

If $c$ is reachable from $\mathsf{init}$ in $\mathcal{M}^{\max}_{[c]}$, then
return “no, (SPR) does not hold for $c$”.

    2. 3.2

If $c$ is not reachable from $\mathsf{init}$ in $\mathcal{M}^{\max}_{[c]}$,
then return “yes, (SPR) holds for $c$”.

lemmasoundnessSPRalgo Algorithm 4.2 is sound and runs in polynomial time.

######  Proof (Soundness)

Let $\mathcal{N}=\mathcal{M}_{[c]}$. Soundness is obvious in case 1. For case
2, consider a real number $\lambda$ with
$1>\lambda>\frac{w_{c}}{q_{\mathsf{init}}}$ and MD-schedulers $\mathfrak{T}$
and $\mathfrak{S}$ realizing
$\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{N},s}(\Diamond\mathsf{Eff})=q_{s}$ and
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{N}}(\Diamond c)>0$ for all states $s$.
We can combine $\mathfrak{T}$ and $\mathfrak{S}$ to a new MR-scheduler
$\mathfrak{U}$ with the property that
$\mathrm{Pr}^{\mathfrak{U}}_{\mathcal{N}}(\Diamond
t)=\lambda\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{N}}(\Diamond
t)+(1{-}\lambda)\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{N}}(\Diamond t)$ for all
terminal states $t$ and for $t=c$. Then, $\mathfrak{U}$ witnesses a violation
of (SPR). For case 3.1 consider an MD-scheduler $\mathfrak{S}$ of
$\mathcal{M}^{\max}_{[c]}$ where $c$ is reachable from $\mathsf{init}$ via a
$\mathfrak{S}$-path and
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{N},s}(\Diamond\mathsf{Eff})=q_{s}$ for
all states $s$. Then, (SPR) does not hold for $c$ in the scheduler
$\mathfrak{S}$. In case 3.2 we have
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{N}}(\Diamond c)=0$ for all schedulers
$\mathfrak{S}$ for $\mathcal{N}$ with
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{N}}(\Diamond\mathsf{Eff})=q_{\mathsf{init}}=w_{c}$.
But then $\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{N}}(\Diamond c)>0$ implies
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{N}}(\Diamond\mathsf{Eff})<w_{c}$ as
required in (SPR). For more details on the soundness see Appendix 0.C.2. ∎

By applying Algorithm 4.2 to all states $c\in\mathsf{Cause}$ and standard
algorithms to check the existence of a path satisfying
$(\neg\mathsf{Cause})\,\mathrm{U}\,c$ for every state $c\in\mathsf{Cause}$, we
obtain:

######  Theorem 4.3 (Checking SPR causes)

The problem “given $\mathcal{M}$, $\mathsf{Cause}$ and $\mathsf{Eff}$, check
whether $\mathsf{Cause}$ is a SPR cause for $\mathsf{Eff}$ in $\mathcal{M}$”
is solvable in polynomial-time.

######  Remark 5 (Memory requirements for refuting the SPR property)

As the soundness proof for Algorithm 4.2 shows: If $\mathsf{Cause}$ does not
satisfy the SPR condition, then there is an MR-scheduler $\mathfrak{S}$ for
$\mathcal{M}_{[\mathsf{Cause}]}$ witnessing the violation of (SPR). Scheduler
$\mathfrak{S}$ corresponds to a finite-memory (randomized) scheduler
$\mathfrak{T}$ with two memory cells for $\mathcal{M}$: “before
$\mathsf{Cause}$” (where $\mathfrak{T}$ behaves as $\mathfrak{S}$) and “after
$\mathsf{Cause}$” (where $\mathfrak{T}$ behaves as an MD-scheduler minimizing
the effect probability form every state). $\lhd$

[Criterion for the existence of probability-raising
causes]lemmaexistencePRcauses Let $\mathcal{M}$ be an MDP and $\mathsf{Eff}$ a
nonempty set of states. Then $\mathsf{Eff}$ has an SPR cause in $\mathcal{M}$
iff $\mathsf{Eff}$ has a GPR cause in $\mathcal{M}$ iff there is a state
$c_{0}\in S\setminus\mathsf{Eff}$ such that the singleton $\\{c_{0}\\}$ is an
SPR cause (and therefore a GRP cause) for $\mathsf{Eff}$ in $\mathcal{M}$. In
particular, the existence of SPR/GPR causes can be checked with Algorithm 4.2
in polynomial time. The lemma can be derived from Lemmata 1, 1 and 4.1
together with the implication “(b) $\Longrightarrow$ (c)” shown in Appendix
0.C.2.

###  4.2 Checking the global probability-raising condition

Throughout this section, we suppose that both the effect set $\mathsf{Eff}$
and the cause candidate $\mathsf{Cause}$ are fixed disjoint subsets of the
state space of the MDP $\mathcal{M}=(S,\mathit{Act},P,\mathsf{init})$, and
address the task to check whether $\mathsf{Cause}$ is a strict resp. global
probability-raising cause for $\mathsf{Eff}$ in $\mathcal{M}$. As the
minimality condition (M) can be checked in polynomial time using a standard
graph algorithm, we will concentrate on an algorithm to check the probability-
raising condition (GPR). We start by stating the main results of this section.

###### Theorem 4.4

The problem “given $\mathcal{M}$, $\mathsf{Cause}$ and $\mathsf{Eff}$, check
whether $\mathsf{Cause}$ is a GPR cause for $\mathsf{Eff}$ in $\mathcal{M}$”
is solvable in polynomial space.

In order to provide an algorithm, we perform a model transformation after
which the violation of (GPR) by a scheduler $\mathfrak{S}$ can be expressed
solely in terms of the expected frequencies of the state-action pairs of the
transformed MDP under $\mathfrak{S}$. This allows us to express the existence
of a scheduler witnessing the non-causality of $\mathsf{Cause}$ in terms of
the satisfiability of a quadratic constraint system. Thus, we can restrict the
quantification in (G) to MR-schedulers in the transformed model. We trace back
the memory requirements to $\mathcal{M}_{[\mathsf{Cause}]}$ and to the
original MDP $\mathcal{M}$ yielding the second main result. Still, memory can
be necessary to witness non-causality (Remark 1).

###### Theorem 4.5

Let $\mathcal{M}$ be an MDP with effect set $\mathsf{Eff}$ as before and
$\mathsf{Cause}$ a set of non-effect states such that condition (M) holds. If
$\mathsf{Cause}$ is not a GPR cause for $\mathsf{Eff}$, then there is an MR-
scheduler for $\mathcal{M}_{[\mathsf{Cause}]}$ refuting the GPR condition for
$\mathsf{Cause}$ in $\mathcal{M}_{[\mathsf{Cause}]}$ and a finite-memory
scheduler for $\mathcal{M}$ with two memory cells refuting the GPR condition
for $\mathsf{Cause}$ in $\mathcal{M}$.

The remainder of this section is concerned with the proofs of Theorem 4.4 and
Theorem 4.5. We suppose that both the effect set $\mathsf{Eff}$ and the cause
candidate $\mathsf{Cause}$ are fixed disjoint subsets of the state space of
the MDP $\mathcal{M}$ and that $\mathsf{Cause}$ satisfies (M).

#### Checking the GPR condition (Proof of Theorem 4.4).

The first step is a polynomial-time model transformation which permits to make
the following assumptions when checking the GPR condition of $\mathsf{Cause}$
for $\mathsf{Eff}$.

(A1)

$\mathsf{Eff}=\\{\mathsf{eff}_{\mathsf{unc}},\mathsf{eff}_{\mathsf{cov}}\\}$
consists of two terminal states.

(A2)

For every state $c\in\mathsf{Cause}$, there is only a single enabled action,
say $\mathit{Act}(c)=\\{\gamma\\}$, and there exists
$w_{c}\in[0,1]\cap\mathbb{Q}$ such that
$P(c,\gamma,\mathsf{eff}_{\mathsf{cov}})=w_{c}$ and
$P(c,\gamma,\mathsf{noeff}_{\mathsf{fp}})=1{-}w_{c}$ where
$\mathsf{noeff}_{\mathsf{fp}}$ is a terminal non-effect state and
$\mathsf{noeff}_{\mathsf{fp}}$ and $\mathsf{eff}_{\mathsf{cov}}$ are only
accessible via the $\gamma$-transition from the states $c\in\mathsf{Cause}$.

(A3)

$\mathcal{M}$ has no end components and there is a further terminal state
$\mathsf{noeff}_{\mathsf{tn}}$ and an action $\tau$ such that
$\tau\in\mathit{Act}(s)$ implies $P(s,\tau,\mathsf{noeff}_{\mathsf{tn}})=1$.

Intuitively, $\mathsf{eff}_{\mathsf{cov}}$ stands for covered effects
(“$\mathsf{Eff}$ after $\mathsf{Cause}$”) and can be seen as a true positive,
while $\mathsf{eff}_{\mathsf{unc}}$ represents the uncovered effects
(“$\mathsf{Eff}$ without preceding $\mathsf{Cause}$”) and corresponds to a
false negative. Let $\mathfrak{S}$ be a scheduler in $\mathcal{M}$. Note that
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}((\neg\mathsf{Cause})\,\mathrm{U}\,\mathsf{Eff})=\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{eff}_{\mathsf{unc}})$
and
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond(\mathsf{Cause}\wedge\Diamond\mathsf{Eff}))=\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{eff}_{\mathsf{cov}})$.
As the cause states can not reach each other we also have
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}((\neg\mathsf{Cause})\,\mathrm{U}\,c)=\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond
c)$ for each $c\in\mathsf{Cause}$. The intuitive meaning of
$\mathsf{noeff}_{\mathsf{fp}}$ is a false positive (“no effect after
$\mathsf{Cause}$”), while $\mathsf{noeff}_{\mathsf{tn}}$ stands for true
negatives where neither the effect nor the cause is observed. Note that
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond(\mathsf{Cause}\wedge\neg\Diamond\mathsf{Eff}))=\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{noeff}_{\mathsf{fp}})$
and
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\neg\Diamond\mathsf{Cause}\wedge\neg\Diamond\mathsf{Eff}))=\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{noeff}_{\mathsf{tn}})$.

#### Justification of assumptions (A1)-(A3):

We justify the assumptions as we can transform $\mathcal{M}$ into a new MDP of
the same asymptotic size satisfying the above assumptions. Thanks to Lemma
4.1, we may suppose that $\mathcal{M}=\mathcal{M}_{[\mathsf{Cause}]}$ (see
Notation 4.1) without changing the satisfaction of the GPR condition. We then
may rename the effect state $\mathsf{eff}$ and the non-effect state
$\mathsf{noeff}$ reachable from $\mathsf{Cause}$ into
$\mathsf{eff}_{\mathsf{cov}}$ and $\mathsf{noeff}_{\mathsf{fp}}$,
respectively. Furthermore, we collapse all other effect states into a single
state $\mathsf{eff}_{\mathsf{unc}}$ and all true negative states into
$\mathsf{noeff}_{\mathsf{tn}}$. Similarly, by renaming and possibly
duplicating terminal states we also suppose that
$\mathsf{noeff}_{\mathsf{fp}}$ has no other incoming transitions than the
$\gamma$-transitions from the states in $\mathsf{Cause}$. This ensures (A1)
and (A2). For (A3) consider the set $T$ of terminal states in the MDP obtained
so far. We remove all end components by switching to the MEC-quotient [2],
i.e., we collapse all states that belong to the same MEC $\mathcal{E}$ into a
single state $s_{\mathcal{E}}$ while ignoring the actions inside
$\mathcal{E}$. Additionally, we add a fresh $\tau$-transition from the states
$s_{\mathcal{E}}$ to $\mathsf{noeff}_{\mathsf{tn}}$ (i.e.,
$P(s_{\mathcal{E}},\tau,\mathsf{noeff}_{\mathsf{tn}})=1$). The
$\tau$-transitions from states $s_{\mathcal{E}}$ to
$\mathsf{noeff}_{\mathsf{tn}}$ mimic cases where schedulers of the original
MDP eventually enter an end component and stay there forever with positive
probability. The soundness of the transition to the MEC-quotient is shown in
Lemma 10 and Corollary 2.

Note, however, that the transformation changes the memory-requirements of
schedulers witnessing that $\mathsf{Cause}$ is not a GPR cause for
$\mathsf{Eff}$. We will address the memory requirements in the original MDP
later.

With assumptions (A1)-(A3), the GPR condition can be reformulated as follows:

###### Lemma 2

Under assumptions (A1)-(A3), $\mathsf{Cause}$ satisfies the GPR condition if
and only if for each scheduler $\mathfrak{S}$ with
$\mathrm{Pr}_{\mathcal{M}}^{\mathfrak{S}}(\Diamond\mathsf{Cause})>0$ the
following condition holds:

$\mathrm{Pr}_{\mathcal{M}}^{\mathfrak{S}}(\Diamond\mathsf{Cause})\cdot\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{eff}_{\mathsf{unc}})\
<\
\bigl{(}1{-}\mathrm{Pr}_{\mathcal{M}}^{\mathfrak{S}}(\Diamond\mathsf{Cause})\bigr{)}\cdot\\!\\!\\!\\!\\!\\!\sum_{c\in\mathsf{Cause}}\\!\\!\\!\\!\\!\\!\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond
c)\cdot w_{c}$ (GPR-1)

With assumptions (A1)-(A3), a terminal state of $\mathcal{M}$ is reached
almost surely under any scheduler after finitely many steps in expectation.
Given a scheduler $\mathfrak{S}$ for $\mathcal{M}$, the expected frequencies
(i.e., expected number of occurrences in maximal paths) of state action-pairs
$(s,\alpha)$, states $s\in S$ and state-sets $T\subseteq S$ under
$\mathfrak{S}$ are defined by:

$\displaystyle\mathit{freq}_{\mathfrak{S}}(s,\alpha)$ $\displaystyle\ \
\stackrel{{\scriptstyle\text{\rm\tiny def}}}{{=}}\ \
\mathrm{E}^{\mathfrak{S}}_{\mathcal{M}}(\text{number of visits to $s$ in which
$\alpha$ is taken})$ $\displaystyle\mathit{freq}_{\mathfrak{S}}(s)$
$\displaystyle\ \ \stackrel{{\scriptstyle\text{\rm\tiny
def}}}{{=}}\sum\nolimits_{\alpha\in\mathit{Act}(s)}\mathit{freq}_{\mathfrak{S}}(s,\alpha),\qquad\mathit{freq}_{\mathfrak{S}}(T)\stackrel{{\scriptstyle\text{\rm\tiny
def}}}{{=}}\sum\nolimits_{s\in T}\mathit{freq}_{\mathfrak{S}}(s).$

Let $T$ be one of the sets $\\{\mathsf{eff}_{\mathsf{cov}}\\}$,
$\\{\mathsf{eff}_{\mathsf{unc}}\\}$, $\mathsf{Cause}$, or a singleton
$\\{c\\}$ with $c\in\mathsf{Cause}$. As $T$ is visited at most once during
each run of $\mathcal{M}$ (assumptions (A1) and (A2)), we have
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{N}}(\Diamond
T)=\mathit{freq}_{\mathfrak{S}}(T)$ for each scheduler $\mathfrak{S}$. This
allows us to express the violation of the GPR condition in terms of a
quadratic constraint system over variables for the expected frequencies of
state-action pairs in the following way:

Let $\mathit{StAct}$ denote the set of state-action pairs in $\mathcal{M}$. We
consider the following constraint system over the variables $x_{s,\alpha}$ for
each $(s,\alpha)\in\mathit{StAct}$ where we use the short form notation
$x_{s}=\sum_{\alpha\in\mathit{Act}(s)}x_{s,\alpha}$:

$\displaystyle x_{s,\alpha}$ $\displaystyle\ \geqslant 0\qquad\text{for all
$(s,\alpha)\in\mathit{StAct}$}$ (1) $\displaystyle x_{\mathsf{init}}$
$\displaystyle\ =\
1+\\!\\!\\!\\!\\!\sum_{(t,\alpha)\in\mathit{StAct}}\\!\\!\\!\\!\\!x_{t,\alpha}\cdot
P(t,\alpha,\mathsf{init})$ (2) $\displaystyle x_{s}$ $\displaystyle\
=\sum_{(t,\alpha)\in\mathit{StAct}}\\!\\!\\!\\!\\!x_{t,\alpha}\cdot
P(t,\alpha,s)\qquad\text{for all $s\in S\setminus\\{\mathsf{init}\\}$}$ (3)

Using well-known results for MDPs without ECs (see, e.g., [22, Theorem 9.16]),
given a vector $x\in\mathbb{R}^{\mathit{StAct}}$, then $x$ is a solution to
(1) and the balance equations (2) and (3) if and only if there is a (possibly
history-dependent) scheduler $\mathfrak{S}$ for $\mathcal{M}$ with
$x_{s,\alpha}=\mathit{freq}_{\mathfrak{S}}(s,\alpha)$ for all
$(s,\alpha)\in\mathit{StAct}$ if and only if there is an MR-scheduler
$\mathfrak{S}$ for $\mathcal{M}$ with
$x_{s,\alpha}=\mathit{freq}_{\mathfrak{S}}(s,\alpha)$ for all
$(s,\alpha)\in\mathit{StAct}$.

The violation of (GPR-1) in Lemma 2 and the condition
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{Cause})>0$ can be
reformulated in terms of the frequency-variables as follows where
$x_{\mathsf{Cause}}$ is an abbreviation for $\sum_{c\in\mathsf{Cause}}x_{c}$:

$\displaystyle x_{\mathsf{Cause}}\cdot x_{\mathsf{eff}_{\mathsf{unc}}}\ \
\geqslant\ \
\bigl{(}1-x_{\mathsf{Cause}}\bigl{)}\cdot\\!\\!\\!\sum_{c\in\mathsf{Cause}}\\!\\!\\!\\!\\!\\!x_{c}\cdot
w_{c}$ (4) $\displaystyle x_{\mathsf{Cause}}>0$ (5)

###### Lemma 3

Under assumptions (A1)-(A3), the set $\mathsf{Cause}$ is not a GPR cause for
$\mathsf{Eff}$ in $\mathcal{M}$ iff the constructed quadratic system of
inequalities (1)-(5) has a solution.

This now puts us in the position to prove Theorem 4.4.

######  Proof (Proof of Theorem 4.4)

The existence of a solution to the quadratic system of inequalities (Lemma 3)
can straight-forwardly be formulated as a sentence in the language of the
existential theory of the reals. The system of inequalities can be constructed
from $\mathcal{M}$, $\mathsf{Cause}$, and $\mathsf{Eff}$ in polynomial time.
Its solvability is decidable in polynomial space as the decision problem of
the existential theory of the reals is in PSPACE [12]. ∎

Memory requirements of schedulers in the original MDP (Proof of Theorem 4.5).
As stated above, every solution to the linear system of inequalities (1), (2),
and (3) corresponds to the expected frequencies of state-action pairs of an
MR-scheduler in the transformed model satisfying (A1)-(A3). Hence:

###### Corollary 1

Under assumptions (A1)-(A3), $\mathsf{Cause}$ is no GPR cause for
$\mathsf{Eff}$ iff there exists an MR-scheduler $\mathfrak{T}$ with
$\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{M}}(\Diamond\mathsf{Cause})>0$ violating
the GPR condition.

The model transformation we used for assumptions (A1)-(A3), however, does
affect the memory requirements of scheduler. We may further restrict the MR-
schedulers necessary to witness non-causality under assumptions (A1)-(A3). For
the following lemma, recall that $\tau$ is the action of the MEC quotient used
for the extra transition from states representing MECs to a new trap state
(see also assumption (A3)).

lemmaMRschedulersufficient Assume (A1)-(A3). Given an MR-scheduler
$\mathfrak{U}$ with
$\mathrm{Pr}^{\mathfrak{U}}_{\mathcal{M}}(\Diamond\mathsf{Cause})>0$ that
violates (GPR), an MR-scheduler $\mathfrak{T}$ with
$\mathfrak{T}(s)(\tau)\in\\{0,1\\}$ for each state $s$ with
$\tau\in\mathit{Act}(s)$ that satifies
$\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{M}}(\Diamond\mathsf{Cause})>0$ and
violates (GPR) is computable in polynomial time.

For the proof, see Appendix 0.C.4. The condition that $\tau$ only has to be
scheduled with probability $0$ or $1$ in each state is the key to transfer the
sufficiency of MR-schedulers to the MDP $\mathcal{M}_{[\mathsf{Cause}]}$. This
fact is of general interest as well and stated in the following theorem where
$\tau$ again is the action added to move from a state $s_{\mathcal{E}}$ to the
new trap state in the MEC-quotient.

theoremMRschedulerlift Let $\mathcal{M}$ be an MDP with pairwise disjoint
action sets for all states. Then, for each MR-scheduler $\mathfrak{S}$ for the
MEC-quotient of $\mathcal{M}$ with
$\mathfrak{S}(s_{\mathcal{E}})(\tau)\in\\{0,1\\}$ for each MEC $\mathcal{E}$
of $\mathcal{M}$ there is an MR-scheduler $\mathfrak{T}$ for $\mathcal{M}$
such that every action $\alpha$ of $\mathcal{M}$ that does not belong to an
MEC of $\mathcal{M}$, has the same expected frequency under $\mathfrak{S}$ and
$\mathfrak{T}$.

###### Proof

The crux are cases where $\mathfrak{S}(s_{\mathcal{E}})(\tau)=0$, which
requires to traverse the MEC $\mathcal{E}$ of $\mathcal{M}$ in a memoryless
way such that all actions leaving $\mathcal{E}$ have the same expected
frequency under $\mathfrak{T}$ and $\mathfrak{S}$. First, we construct a
finite-memory scheduler $\mathfrak{T}^{\prime}$ that always leaves each such
end component according to the distribution given by
$\mathfrak{S}(s_{\mathcal{E}})$. By [22, Theorem 9.16], we then conclude that
there is an MR-scheduler $\mathfrak{T}$ under which the expected frequencies
of all state-action pairs are the same as under $\mathfrak{T}^{\prime}$. ∎

######  Proof (Proof of Theorem 4.5)

The model transformation establishing assumptions (A1)-(A3) results in the
MEC-quotient of $\mathcal{M}_{[\mathsf{Cause}]}$ up to the renaming and
collapsing of terminal states. By Corollary 1 and Theorem 1, we conclude that
$\mathsf{Cause}$ is not a GPR cause for $\mathsf{Eff}$ in $\mathcal{M}$ if and
only if there is a MR-scheduler $\mathfrak{S}$ for
$\mathcal{M}_{[\mathsf{Cause}]}$ with
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}_{[\mathsf{Cause}]}}(\Diamond\mathsf{Cause})>0$
that violates (GPR). As in Remark 5, $\mathfrak{S}$ can be extended to a
finite-memory randomized scheduler $\mathfrak{T}$ for $\mathcal{M}$ with two
memory cells. ∎

######  Remark 6 (On lower bounds on GPR checking)

Solving systems of quadratic inequalities with linear side constraints is NP-
hard in general (see, e.g., [19]). For convex problems, in which the
associated symmetric matrix occurring in the quadratic inequality has only
non-negative eigenvalues, the problem is, however, solvable in polynomial time
[25]. Unfortunately, the quadratic constraint system given by (1)-(5) is not
of this form. We observe that even if $\mathsf{Cause}$ is a singleton
$\\{c\\}$ and the variable $x_{\mathsf{eff}_{\mathsf{unc}}}$ is forced to take
a constant value $y$ by (1)-(3), i.e., by the structure of the MDP, the
inequality (4) takes the form:

  1. $x_{c}\cdot w_{c}-x_{c}^{2}\cdot(w_{c}+y)\leq 0$ (*)

Here, the $1\times 1$-matrix $({-}w_{c}{-}y)$ has a negative eigenvalue.
Although it is not ruled out that (1)-(5) belongs to another class of
efficiently solvable constraint systems, the NP-hardness result in [32] for
the solvability of quadratic inequalities of the form (*) with linear side
constraints might be an indication for the computational difficulty. $\lhd$

##  5 Quality and optimality of causes

The goal of this section is to identify notions that measure how “good” causes
are and to present algorithms to determine good causes according to the
proposed quality measures. We have seen so far that small (singleton) causes
are easy to determine (see Section 4.1). Moreover, it is easy to see that the
proposed existence-checking algorithm can be formulated in such a way that the
algorithm returns a singleton (strict or global) probability-raising cause
$\\{c_{0}\\}$ with maximal _precision_ , i.e., a state $c_{0}$ where
$\inf_{\mathfrak{S}}\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{Eff}|\Diamond
c_{0})=\mathrm{Pr}^{\min}_{\mathcal{M},c_{0}}(\Diamond\mathsf{Eff})$ is
maximal. On the other hand, singleton or small cause sets might have poor
coverage in the sense that the probability for paths that reach an effect
state without visiting a cause state before (“uncovered effects”) can be
large. This motivates the consideration of quality notions for causes that
incorporate how well effect scenarios are covered. We take inspiration of
quality measures that are considered in statistical analysis (see e.g. [35]).
This includes the _recall_ as a measure for the relative coverage (proportion
of covered effects among all effect scenarios), the _coverage ratio_ (quotient
of covered and uncovered effects) as well as the _f-score_. The f-score is a
standard measure for classifiers defined by the harmonic mean of precision and
recall. It can be seen as a compromise to achieve both good precision and good
recall.

Throughout this section, we assume as before an MDP
$\mathcal{M}=(S,\mathit{Act},P,\mathsf{init})$ and a set
$\mathsf{Eff}\subseteq S$ are given where all effect states are terminal.
Furthermore, we suppose that all states $s\in S$ are reachable from
$\mathsf{init}$. Detailed proofs can be found in Appendix 0.D.

###  5.1 Quality measures for causes

In statistical analysis, the precision of a classifier with binary outcomes
(“positive” or “negative”) is defined as the ratio of all true positives among
all positively classified elements, while its recall is defined as the ratio
of all true positives among all actual positive elements. Translated to our
setting, we consider classifiers induced by a given cause set $\mathsf{Cause}$
that return “positive” for sample paths in case that a cause state is visited
and “negative” otherwise. The intuitive meaning of true positives and false
negatives is as explained after Definition 1. The meaning of true negatives
and false positives is analogous. We use $\mathsf{tp}^{\mathfrak{S}}$ for the
probability for true positives under $\mathfrak{S}$. The notations
$\mathsf{fp}^{\mathfrak{S}}$, $\mathsf{fn}^{\mathfrak{S}}$,
$\mathsf{tn}^{\mathfrak{S}}$ have analogous meanings.

With this interpretation of causes as binary classifiers in mind, the recall
and precision and coverage ratio of a cause set $\mathsf{Cause}$ _under a
scheduler_ $\mathfrak{S}$ is defined as follows (assuming
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{Eff})>0$ resp.
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{Cause})>0$ resp.
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}\bigl{(}(\neg\mathsf{Cause})\,\mathrm{U}\,\mathsf{Eff}\bigr{)}>0$):

$\begin{array}[]{rclcl}\operatorname{\mathit{precision}}^{\mathfrak{S}}(\mathsf{Cause})&\
=&\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\ \Diamond\mathsf{Eff}\ |\
\Diamond\mathsf{Cause}\
)&=&\frac{\mathsf{tp}^{\mathfrak{S}}}{\mathsf{tp}^{\mathfrak{S}}+\mathsf{fp}^{\mathfrak{S}}}\\\\[4.30554pt]
\operatorname{\mathit{recall}}^{\mathfrak{S}}(\mathsf{Cause})&=&\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\
\Diamond\mathsf{Cause}\ |\ \Diamond\mathsf{Eff}\
)&=&\frac{\mathsf{tp}^{\mathfrak{S}}}{\mathsf{tp}^{\mathfrak{S}}+\mathsf{fn}^{\mathfrak{S}}}\end{array}$
$\begin{array}[]{rclcl}\mathit{covrat}^{\mathfrak{S}}(\mathsf{Cause})&=&\frac{\displaystyle\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}\bigl{(}\Diamond(\mathsf{Cause}\wedge\Diamond\mathsf{Eff})\bigr{)}}{\displaystyle\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}\bigl{(}(\neg\mathsf{Cause})\,\mathrm{U}\,\mathsf{Eff}\bigr{)}}&=&\frac{\mathsf{tp}^{\mathfrak{S}}}{\mathsf{fn}^{\mathfrak{S}}}.\end{array}$

For the coverage ratio, if
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}\bigl{(}(\neg\mathsf{Cause})\,\mathrm{U}\,\mathsf{Eff}\bigr{)}=0$
and $\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{Cause})>0$ we
define $\mathit{covrat}^{\mathfrak{S}}(\mathsf{Cause})=+\infty$. Finally, the
f-score of $\mathsf{Cause}$ _under a scheduler_ $\mathfrak{S}$ is defined as
the harmonic mean of the precision and recall (assuming
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{Cause})>0$, which
implies $\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{Eff})>0$ as
$\mathsf{Cause}$ is a PR cause):

$\mathit{fscore}^{\mathfrak{S}}(\mathsf{Cause})\ \
\stackrel{{\scriptstyle\text{\rm\tiny def}}}{{=}}\ \
2\cdot\frac{\operatorname{\mathit{precision}}^{\mathfrak{S}}(\mathsf{Cause})\cdot\operatorname{\mathit{recall}}^{\mathfrak{S}}(\mathsf{Cause})}{\operatorname{\mathit{precision}}^{\mathfrak{S}}(\mathsf{Cause})+\operatorname{\mathit{recall}}^{\mathfrak{S}}(\mathsf{Cause})}$

If, however,
$\mathrm{Pr}_{\mathcal{M}}^{\mathfrak{S}}(\Diamond\mathsf{Eff})>0$ and
$\mathrm{Pr}_{\mathcal{M}}^{\mathfrak{S}}(\Diamond\mathsf{Cause})=0$ we define
$\mathit{fscore}^{\mathfrak{S}}(\mathsf{Cause})=0$.

#### Quality measures for cause sets.

Let $\mathsf{Cause}$ be a PR cause. The recall of $\mathsf{Cause}$ measures
the relative coverage in terms of the worst-case conditional probability for
covered effects (true positives) among all scenarios where the effect occurs.

$\operatorname{\mathit{recall}}(\mathsf{Cause})\ =\ \inf_{\mathfrak{S}}\
\operatorname{\mathit{recall}}^{\mathfrak{S}}(\mathsf{Cause})\ =\
\mathrm{Pr}^{\min}_{\mathcal{M}}(\ \Diamond\mathsf{Cause}\ |\
\Diamond\mathsf{Eff}\ )$

when ranging over all schedulers $\mathfrak{S}$ with
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{Eff})>0$. Likewise,
the coverage ratio and f-score of $\mathsf{Cause}$ are defined by the worst-
case coverage ratio resp. f-score (when ranging over schedulers for which
$\mathit{covrat}^{\mathfrak{S}}(\mathsf{Cause})$ resp.
$\mathit{fscore}^{\mathfrak{S}}(\mathsf{Cause})$ is defined):

$\mathit{covrat}(\mathsf{Cause})\ =\ \inf_{\mathfrak{S}}\
\mathit{covrat}^{\mathfrak{S}}(\mathsf{Cause}),\quad\mathit{fscore}(\mathsf{Cause})\
=\ \inf_{\mathfrak{S}}\ \mathit{fscore}^{\mathfrak{S}}(\mathsf{Cause})$

###  5.2 Computation schemes for the quality measures for fixed cause set

For this section, we assume a fixed PR cause $\mathsf{Cause}$ is given and
address the problem to compute its quality values. Since all quality measures
are preserved by the switch from $\mathcal{M}$ to
$\mathcal{M}_{[\mathsf{Cause}]}$ as well as the transformations of
$\mathcal{M}_{[\mathsf{Cause}]}$ to an MDP that satisfies conditions (A1)-(A3)
of Section 4.2, we may assume that $\mathcal{M}$ satisfies (A1)-(A3).

While efficient computation methods for
$\operatorname{\mathit{recall}}(\mathsf{Cause})$ are known from literature
(see [9, 30] for poly-time algorithms to compute conditional reachability
probabilities), we are not aware of known concepts that are applicable for
computing the coverage ratio or the f-score. Indeed, both are efficiently
computable:

theoremcomputecovratiofscore The values $\mathit{covrat}(\mathsf{Cause})$ and
$\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 5.2. By
definition, the value $\mathit{covrat}(\mathsf{Cause})$ is the infimum over a
quotient of reachability probabilities for disjoint sets of terminal states.
While this is not the case for the f-score, we can express
$\mathit{fscore}(\mathsf{Cause})$ in terms of the supremum of such a quotient.
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, $\mathit{fscore}(\mathsf{Cause})=0$ iff
$\operatorname{\mathit{recall}}(\mathsf{Cause})=0$ iff there exists a
scheduler $\mathfrak{S}$ satisfying
$\mathrm{Pr}_{\mathcal{M}}^{\mathfrak{S}}(\Diamond\mathsf{Eff})>0$ and
$\mathrm{Pr}_{\mathcal{M}}^{\mathfrak{S}}(\Diamond\mathsf{Cause})=0$.

So, the remaining task to prove Theorem 5.2 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:

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

The goal is to provide an algorithm for computing the extremal values:
$\min/\mathcal{M}{U,V}=\inf_{\mathfrak{S}}\mathfrak{S}/\mathcal{M}{U,V}$ and
$\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_ [11]. 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 [11, 3, 4] 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.

theoremcompQ 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.

######  Proof (Proof of Theorem 5.2)

Using assumptions (A1)-(A3), we obtain that
$\mathit{covrat}(\mathsf{Cause})=\min/\mathcal{M}{U,V}$ where
$U=\\{\mathsf{eff}_{\mathsf{cov}}\\}$, $V=\\{\mathsf{eff}_{\mathsf{unc}}\\}$.
Similarly, with
$U=\\{\mathsf{noeff}_{\mathsf{fp}},\mathsf{eff}_{\mathsf{unc}}\\}$,
$V=\\{\mathsf{eff}_{\mathsf{cov}}\\}$, we get
$\mathit{fscore}(\mathsf{Cause})=0$ if $\max/\mathcal{M}{U,V}=+\infty$ and
$\mathit{fscore}(\mathsf{Cause})=2/(\max/\mathcal{M}{U,V}+2)$ otherwise. Thus,
the claim follows from Theorem 5.2. ∎

###  5.3 Quality-optimal probability-raising causes

An SPR cause $\mathsf{Cause}$ is called _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.

lemmarecalloptimalityequalsratiooptimality 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.

#### 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 ratio. To see this, let $\mathcal{C}$ denote
the set of states that 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$.
Obviously, $\mathcal{C}$ and $\mathsf{CanCause}$ are computable in polynomial
time.

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

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

This is not true for the f-score. To see this, Consider the Markov chain on
the right hand side. 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}$.

#### 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 5.2). 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:

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

###### Proof

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 5.3
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 [33], 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:

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

###### Proof

Given an MDP $\mathcal{M}$, $\mathsf{Eff}$, and $\vartheta$, we construct an
SSP game [33] after a series of model transformations ensuring (i) that
terminal states are reached almost surely and (ii) that $\mathsf{Eff}$ is
reached with positive probability under all schedulers. Condition (i) is
established by a standard MEC-quotient construction. To establish condition
(ii), we provide a construction that forces schedulers to leave an initial
sub-MDP in which the minimal probability to reach $\mathsf{Eff}$ is $0$. This
construction – unlike the MEC-quotient – affects the possible combinations of
probability values with which terminal states and potential cause states can
be reached, but the existence of an SPR cause satisfying the f-score-threshold
condition is not affected.

The underlying idea of the construction of the game shares similarities with
the MDP constructed in the proof of Theorem 5.3: Player $0$ takes the role to
select potential cause states while player $1$ takes the role of a scheduler
in the transformed MDP. Using the observation that for each cause $C$,
$\mathit{fscore}(C)>\vartheta$ iff

$2(1{-}\vartheta)\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond
C\land\Diamond\mathsf{Eff})-\vartheta\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\neg\Diamond
C\land\Diamond\mathsf{Eff})-\vartheta\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond
C\land\neg\Diamond\mathsf{Eff})>0$ ($\times$)

for all schedulers $\mathfrak{S}$ for $\mathcal{M}$ with
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{Eff})>0$, weights
are assigned to $\mathsf{Eff}$-states and other terminal states depending on
whether player $0$ has chosen to include a state to the cause beforehand. In
the resulting SSP game, both players have optimal MD-strategies [33]. Given
such strategies $\zeta$ for player $0$ and $\mathfrak{S}$ for player $1$, the
resulting expected accumulated weight agrees with the left-hand side of
($\times$) when considering $\mathfrak{S}$ as a scheduler for the transformed
MDP and the cause $C$ induced by the states that $\zeta$ chooses to belong to
the cause. So, player $0$ wins the constructed game iff an SPR cause with
f-score above the threshold $\vartheta$ exists. The existence of optimal MD-
strategies for both players allows us to decide this threshold problem in NP
and coNP. ∎

#### 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 the GPR
condition in polynomial space (Theorem 4.4) and computing the corresponding
quality measure in polynomial time (Section 5.2). 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$.

theoremmeasureNPhardness The problems GPR-covratio, GPR-recall and GPR-f-score
are NP-hard and belong to PSPACE. For Markov chains, all three problems are
NP-complete. NP-hardness even holds for tree-like Markov chains.

###### Proof

NP-hardness is established via a polynomial reduction from the knapsack
problem. Membership to NP for Markov chains resp. to
$\mathrm{PSPACE}=\mathrm{NPSPACE}$ for MDPs is obvious as we can guess
nondeterministically a cause candidate and then check (i) the GPR condition in
polynomial time (Markov chains) resp. polynomial space (MDPs) and (ii) the
threshold condition in polynomial time (see Section 5.2). ∎

##  6 Conclusion

The goal of the paper was to formalize the PR principle in MDPs and related
quality notions for PR causes and to study fundamental algorithmic problems
for them. We considered the strict (local) and the global view. Our results
indicate that GPR causes are more general and leave more flexibility to
achieve better accuracy, while algorithmic reasoning about SPR causes is
simpler.

Existential definition of SPR/GPR causes. The proposed definition of PR causes
relies on a universal quantification over all relevant schedulers. However,
another approach could be via existential quantification, i.e. there is a
scheduler $\mathfrak{S}$ such that (GPR) or resp. (SPR) hold. The resulting
notion of causality yields fairly the same results (up to
$\mathrm{Pr}^{\max}_{\mathcal{M},c}(\Diamond\mathsf{Eff})$ instead of
$\mathrm{Pr}^{\min}_{\mathcal{M},c}(\Diamond\mathsf{Eff})$ etc). A canonical
existential SPR cause can be defined in analogy to the universal case and
shown to be recall- and ratio-optimal (cf. Theorem 5.3). The problem to find
an existential f-score-optimal SPR cause is even simpler and solvable in
polynomial time as the construction presented in the proof of Theorem 5.3 can
be adapted for MDPs (thanks to the simpler nature of
$\max_{C}\sup_{\mathfrak{S}}\mathit{fscore}^{\mathfrak{S}}(C)$ compared to
$\max_{C}\inf_{\mathfrak{S}}\mathit{fscore}^{\mathfrak{S}}(C)$). However, NP-
hardness for the existence of GPR causes with threshold constraints for the
quality carries over to the existential definition (as NP-hardness holds for
Markov chains, Theorem 5.3).

Non-strict inequality in the PR conditions. Our notions of PR causes are in
line with the classical approach of probability-raising causality in
literature with strict inequality in the PR condition, with the consequence
that causes might not exist (see Example 2). The switch to a relaxed
definition of PR causes with non-strict inequality seems to be a minor change
that identifies more sets as causes. Indeed, the proposed algorithms for
checking the SPR and GPR condition (Section 4) can easily be modified for the
relaxed definition. While the relaxed definition leads to a questionable
notion of causality (e.g., $\\{\mathsf{init}\\}$ would always be a recall- and
ratio-optimal SPR cause under the relaxed definition), it could be useful in
combination with other side constraints. E.g., requiring the relaxed PR
condition for all schedulers that reach a cause state with positive
probability and the existence of a scheduler where the PR condition with
strict inequality holds might be a useful alternative definition that agrees
with Def. 1 for Markov chains.

Relaxing the minimality condition (M). As many causality notions of the
literature include some minimality constraint, we included condition (M).
However, (M) could be dropped without affecting the algorithmic results
presented here. This can be useful when the task is to identify components or
agents that 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 (M).

Future directions include PR causality when causes and effects are path
properties and the investigation of other quality measures for PR causes
inspired by other indices for binary classifiers used in machine learning or
customized for applications of cause-effect reasoning in MDPs. More
sophisticated notions of probabilistic backward causality and considerations
on PR causality with external interventions as in Pearl’s do-calculus [34] are
left for future work.

Acknowledgments We would like to thank Simon Jantsch and Clemens Dubslaff for
their helpful comments and feedback on the topic of causality in MDPs.

## References

  * [1] Ábrahám, E., Bonakdarpour, B.: HyperPCTL: A temporal logic for probabilistic hyperproperties. In: McIver, A., Horváth, A. (eds.) 15th International Conference on Quantitative Evaluation of Systems (QEST). Lecture Notes in Computer Science, vol. 11024, pp. 20–35. Springer (2018), https://doi.org/10.1007/978-3-319-99154-2_2
  * [2] de Alfaro, L.: Formal Verification of Probabilistic Systems. Phd thesis, Stanford University, Stanford, USA (1997), https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/4375-deAlfaro(1997)-FormalVerificationofProbabilisticSystems.pdf
  * [3] de Alfaro, L.: Computing minimum and maximum reachability times in probabilistic systems. In: Baeten, J.C.M., Mauw, S. (eds.) 10th International Conference on Concurrency Theory (CONCUR). Lecture Notes in Computer Science, vol. 1664, pp. 66–81. Springer (1999), https://doi.org/10.1007/3-540-48320-9_7
  * [4] Baier, C., Bertrand, N., Dubslaff, C., Gburek, D., Sankur, O.: Stochastic shortest paths and weight-bounded properties in Markov decision processes. In: Dawar, A., Grädel, E. (eds.) 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018. pp. 86–94. ACM (2018), https://doi.org/10.1145/3209108.3209184
  * [5] Baier, C., Dubslaff, C., Funke, F., Jantsch, S., Majumdar, R., Piribauer, J., Ziemek, R.: From verification to causality-based explications (invited talk). In: Bansal, N., Merelli, E., Worrell, J. (eds.) 48th International Colloquium on Automata, Languages, and Programming, (ICALP). LIPIcs, vol. 198, pp. 1:1–1:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021), https://doi.org/10.4230/LIPIcs.ICALP.2021.1
  * [6] Baier, C., Funke, F., Jantsch, S., Piribauer, J., Ziemek, R.: Probabilistic causes in Markov chains. CoRR abs/2104.13604 (2021), https://arxiv.org/abs/2104.13604, accepted for publication at ATVA’21.
  * [7] Baier, C., Funke, F., Majumdar, R.: A game-theoretic account of responsibility allocation. In: Zhou, Z. (ed.) 30th International Joint Conference on Artificial Intelligence (IJCAI). pp. 1773–1779. ijcai.org (2021), https://doi.org/10.24963/ijcai.2021/244
  * [8] Baier, C., Katoen, J.P.: Principles of Model Checking (Representation and Mind Series). The MIT Press, Cambridge, MA (2008)
  * [9] Baier, C., Klein, J., Klüppelholz, S., Märcker, S.: Computing conditional probabilities in Markovian models efficiently. In: Ábrahám, E., Havelund, K. (eds.) 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, vol. 8413, pp. 515–530. Springer (2014), https://doi.org/10.1007/978-3-642-54862-8_43
  * [10] Beer, I., Ben-David, S., Chockler, H., Orni, A., Trefler, R.J.: Explaining counterexamples using causality. Formal Methods in System Design 40(1), 20–40 (2012), https://doi.org/10.1007/s10703-011-0132-2
  * [11] Bertsekas, D.P., Tsitsiklis, J.N.: An analysis of stochastic shortest path problems. Mathemathics of Operations Research 16(3), 580–595 (1991)
  * [12] Canny, J.F.: Some algebraic and geometric computations in PSPACE. In: 20th Annual ACM Symposium on Theory of Computing (STOC). pp. 460–467. ACM (1988)
  * [13] Chockler, H.: Causality and responsibility for formal verification and beyond. In: First Workshop on Causal Reasoning for Embedded and safety-critical Systems Technologies (CREST). EPTCS, vol. 224, pp. 1–8 (2016), https://doi.org/10.4204/EPTCS.224.1
  * [14] Chockler, H., Halpern, J.Y., Kupferman, O.: What causes a system to satisfy a specification? ACM Transactions on Computational Logic 9(3), 20:1–20:26 (2008)
  * [15] Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press (1999)
  * [16] Dimitrova, R., Finkbeiner, B., Torfah, H.: Probabilistic hyperproperties of Markov decision processes. In: Hung, D.V., Sokolsky, O. (eds.) 18th International Symposium on Automated Technology for Verification and Analysis (ATVA). Lecture Notes in Computer Science, vol. 12302, pp. 484–500. Springer (2020), https://doi.org/10.1007/978-3-030-59152-6_27
  * [17] Eells, E.: Probabilistic Causality. Cambridge Studies in Probability, Induction and Decision Theory, Cambridge University Press (1991)
  * [18] Friedenberg, M., Halpern, J.Y.: Blameworthiness in multi-agent settings. In: 33rd Conference on Artificial Intelligence (AAAI). pp. 525–532. AAAI Press (2019), https://doi.org/10.1609/aaai.v33i01.3301525
  * [19] Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman (1979)
  * [20] Halpern, J.Y., Pearl, J.: Causes and explanations: A structural-model approach: Part 1: Causes. In: 17th Conference in Uncertainty in Artificial Intelligence (UAI). pp. 194–202 (2001)
  * [21] Hitchcock, C.: Probabilistic causation. In: Hájek, A., Hitchcock, C. (eds.) The Oxford Handbook of Probability and Philosophy, pp. 815–832. Oxford University Press (2016)
  * [22] Kallenberg, L.: Lecture Notes Markov Decision Problems - version 2020 (02 2020)
  * [23] Kleinberg, S., Mishra, B.: The temporal logic of causal structures. In: 25th Conference on Uncertainty in Artificial Intelligence (UAI). pp. 303–312 (2009)
  * [24] Kleinberg, S.: Causality, Probability and Time. Cambridge University Press (2012)
  * [25] Kozlov, M.K., Tarasov, S.P., Khachiyan, L.G.: The polynomial solvability of convex quadratic programming. USSR Computational Mathematics and Mathematical Physics 20(5), 223–228 (1980)
  * [26] Kuntz, M., Leitner-Fischer, F., Leue, S.: From probabilistic counterexamples via causality to fault trees. In: Flammini, F., Bologna, S., Vittorini, V. (eds.) 30th International Conference on Computer Safety, Reliability, and Security (SAFECOMP). Lecture Notes in Computer Science, vol. 6894, pp. 71–84. Springer (2011), https://doi.org/10.1007/978-3-642-24270-0_6
  * [27] Leitner-Fischer, F.: Causality Checking of Safety-Critical Software and Systems. Ph.D. thesis, University of Konstanz, Germany (2015), http://kops.uni-konstanz.de/handle/123456789/30778
  * [28] Lewis, D.: Counterfactuals and comparative possibility. Journal of Philosophical Logic 2(4), 418–446 (1973)
  * [29] Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Safety. Springer-Verlag (1995)
  * [30] Märcker, S.: Model checking techniques for design and analysis of future hardware and software systems. Ph.D. thesis, TU Dresden, Germany (2020), https://d-nb.info/1232958204
  * [31] Namjoshi, K.S.: Certifying model checkers. In: 13th International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol. 2102, pp. 2–13. Springer (2001), https://doi.org/10.1007/3-540-44585-4_2
  * [32] Pardalos, P.M., Vavasis, S.A.: Quadratic programming with one negative eigenvalue is np-hard. Journal of Global optimization 1(1), 15–22 (1991)
  * [33] Patek, S.D., Bertsekas, D.P.: Stochastic shortest path games. SIAM Journal on Control and Optimization 37(3), 804–824 (1999)
  * [34] Pearl, J.: Causality. Cambridge University Press, 2nd edn. (2009)
  * [35] Powers, D.: Evaluation: From precision, recall and f-factor to ROC, informedness, markedness & correlation. Mach. Learn. Technol. 2 (01 2008)
  * [36] Puterman, M.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley & Sons, Inc., New York, NY (1994)
  * [37] Reichenbach, H.: The Direction of Time. Dover Publications (1956)
  * [38] Suppes, P.: A Probabilistic Theory of Causality. Amsterdam: North-Holland Pub. Co. (1970)
  * [39] Yazdanpanah, V., Dastani, M.: Distant group responsibility in multi-agent systems. In: Baldoni, M., Chopra, A.K., Son, T.C., Hirayama, K., Torroni, P. (eds.) 19th International Conference on Princiles and Practice of Multi-Agent Systems (PRIMA). Lecture Notes in Computer Science, vol. 9862, pp. 261–278. Springer (2016), https://doi.org/10.1007/978-3-319-44832-9_16
  * [40] Yazdanpanah, V., Dastani, M., Jamroga, W., Alechina, N., Logan, B.: Strategic responsibility under imperfect information. In: Elkind, E., Veloso, M., Agmon, N., Taylor, M.E. (eds.) 18th International Conference on Autonomous Agents and MultiAgent Systems (AAMAS). pp. 592–600. International Foundation for Autonomous Agents and Multiagent Systems (2019), http://dl.acm.org/citation.cfm?id=3331745

##  Appendix 0.A Notation and preliminary results used in the appendix

###  0.A.1 Basic notations

Let $\mathcal{M}=(S,\mathit{Act},P,\mathsf{init})$ be an MDP. For
$\alpha\in\mathit{Act}$ and $U\subseteq S$, $P(s,\alpha,U)$ is a shortform
notation for $\sum_{u\in U}P(s,\alpha,u)$. If $\pi$ is a finite path in
$\mathcal{M}$ then $\mathit{last}(\pi)$ denotes the last state of $\pi$. That
is, if $\pi=s_{0}\,\alpha_{0}\,s_{1}\,\alpha_{1}\ldots\alpha_{n-1}\,s_{n}$
then $\mathit{last}(\pi)=s_{n}$. If $\mathfrak{S}$ is a scheduler then $\pi$
is said to be a $\mathfrak{S}$-path if
$\mathfrak{S}(s_{0}\,\alpha_{0}\ldots\alpha_{i-1}\,s_{i})(\alpha_{i})>0$ for
each $i\in\\{0,\ldots,n{-}1\\}$.

When dealing with model transformations, we often attach the name of the MDP
as a subscript for the state space, action set, transition probability
function and the initial state. That is, we then write $S_{\mathcal{M}}$ for
$S$, $\mathit{Act}_{\mathcal{M}}$ for $\mathit{Act}$, $P_{\mathcal{M}}$ for
$P$ and $\mathsf{init}_{\mathcal{M}}$ for $\mathsf{init}$.

######  Notation 0.A.1 (Residual scheduler)

Given an MDP $\mathcal{M}=(S,\mathit{Act},P,\mathsf{init})$, a scheduler
$\mathfrak{S}$, and a path
$\pi=s_{0}\,\alpha_{0}\,\dots\,\alpha_{n-1}\,s_{n}$, the _residual scheduler_
$\mathit{res}(\mathfrak{S},\pi)$ of $\mathfrak{S}$ after $\pi$ is defined by

$\mathit{res}(\mathfrak{S},\pi)(\zeta)=\mathfrak{S}(\pi\circ\zeta)$

for all finite paths $\zeta$ starting in $s_{n}$. Here, $\pi\circ\zeta$
denotes the concatenation of the paths $\pi$ and $\zeta$. $\lhd$

Intuitively speaking, $\mathit{res}(\mathfrak{S},\pi)$ behaves like
$\mathfrak{S}$ after $\pi$ has already been seen.

###  0.A.2 MR-scheduler in MDPs without ECs

The following preliminary lemma is folklore (see, e.g., [22, Theorem 9.16])
and used in the proof of Lemma 1 in the following form.

######  Lemma 4 (From general schedulers to MR-schedulers in MDPs without ECs)

Let $\mathcal{M}=(S,\mathit{Act},P,\mathsf{init})$ be an MDP without end
components. Then, for each scheduler $\mathfrak{S}$ for $\mathcal{M}$, there
exists an MR-scheduler $\mathfrak{T}$ such that:

$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond t)\ =\
\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{M}}(\Diamond t)$ for each terminal state
$t$.

######  Lemma 5 (Convex combination of MR-schedulers)

Let $\mathcal{M}$ be an MDP without end components and let $\mathfrak{S}$ and
$\mathfrak{T}$ be schedulers for $\mathcal{M}$ and $\lambda$ a real number in
the open interval $]0,1[$. Then, there exists an MR-scheduler $\mathfrak{U}$
such that:

$\mathrm{Pr}^{\mathfrak{U}}_{\mathcal{M}}(\Diamond t)\ =\
\lambda\cdot\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond t)\ +\
(1{-}\lambda)\cdot\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{M}}(\Diamond t)$

for each terminal state $t$.

###### Proof

Thanks to Lemma 4 we may suppose that $\mathfrak{S}$ and $\mathfrak{T}$ are
MR-schedulers. Let

$f_{*}\ \ =\ \ \lambda\cdot\mathit{freq}_{\mathfrak{S}}(*)\ +\
(1{-}\lambda)\cdot\mathit{freq}_{\mathfrak{T}}(*)$

where $*$ stands for a state or a state-action pair in $\mathcal{M}$. Let
$\mathfrak{U}$ be an MR-scheduler defined by

$\mathfrak{U}(s)(\alpha)\ \ =\ \ \frac{f_{s,\alpha}}{f_{s}}$

for each non-terminal state $s$ where $f_{s}>0$ and each action
$\alpha\in\mathit{Act}(s)$. If $f_{s}=0$ then $\mathfrak{U}$ selects an
arbitrary distribution over $\mathit{Act}(s)$.

Using Lemma 4 we then obtain $f_{*}=\mathit{freq}_{\mathfrak{U}}(*)$ where $*$
ranges over all states and state-action pairs in $\mathcal{M}$. But this
yields:

$\displaystyle\mathrm{Pr}^{\mathfrak{U}}_{\mathcal{M}}(\Diamond t)$
$\displaystyle=$ $\displaystyle f_{t}\ \ =\ \
\lambda\cdot\mathit{freq}_{\mathfrak{S}}(t)\ +\
(1{-}\lambda)\cdot\mathit{freq}_{\mathfrak{T}}(t)$ $\displaystyle=$
$\displaystyle\lambda\cdot\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond
t)\ +\ (1{-}\lambda)\cdot\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{M}}(\Diamond t)$

for each terminal state $t$. ∎

######  Notation 0.A.2 (Convex combination of schedulers)

Let $\mathcal{M},\mathfrak{S},\mathfrak{T},\lambda$ be as in Lemma 5. Then,
the notation $\lambda\mathfrak{S}\oplus(1{-}\lambda)\mathfrak{T}$ will be used
to denote any MR-scheduler $\mathfrak{U}$ as in Lemma 5. $\lhd$

###  0.A.3 MEC-quotient

We now recall the definition of the MEC-quotient, which is a standard concept
for the analysis of MDPs [2]. More concretely, we use a modified version with
an additional trap state as in [4] that serves to mimic behaviors inside an
end component of the original MDP.

######  Definition 2 (MEC-quotient of an MDP)

Let $\mathcal{M}=(S,\mathit{Act},P,\mathsf{init})$ be an MDP with end
components. Let $\mathcal{E}_{1},\ldots,\mathcal{E}_{k}$ be the MECs of
$\mathcal{M}$. We may suppose without loss of generality that the enabled
actions of the states are pairwise disjoint, i.e., whenever $s_{1},s_{2}$ are
states in $\mathcal{M}$ with $s_{1}\not=s_{2}$ then
$\mathit{Act}_{\mathcal{M}}(s_{1})\cap\mathit{Act}_{\mathcal{M}}(s_{2})=\varnothing$.
This permits to consider $\mathcal{E}_{i}$ as a subset of $\mathit{Act}$. Let
$U_{i}$ denote the set of states that belong to $\mathcal{E}_{i}$ and let
$U=U_{1}\cup\ldots\cup U_{k}$.

The MEC-quotient of $\mathcal{M}$ is the MDP
$\mathcal{N}=(S^{\prime},\mathit{Act}^{\prime},P^{\prime},\mathsf{init}^{\prime})$
and the function $\iota:S\to S^{\prime}$ are defined as follows.

  * •

The state space $S^{\prime}$ is $S\setminus
U\cup\\{s_{\mathcal{E}_{1}},\ldots,s_{\mathcal{E}_{k}},\bot\\}$ where
$s_{\mathcal{E}_{1}},\ldots,s_{\mathcal{E}_{k}},\bot$ are pairwise distinct
fresh states.

  * •

The function $\iota$ is given by $\iota(s)=s$ if $s\in S\setminus U$ and
$\iota(u)=s_{\mathcal{E}_{i}}$ if $u\in U_{i}$.

  * •

The initial state of $\mathcal{N}$ is
$\mathsf{init}^{\prime}=\iota(\mathsf{init})$.

  * •

The action set $\mathit{Act}^{\prime}$ is $\mathit{Act}\cup\\{\tau\\}$ where
$\tau$ is a fresh action symbol.

  * •

The set of actions enabled in state $s\in S^{\prime}$ of $\mathcal{N}$ and the
transition probabilities are defined as follows:

    * –

If $s$ is a state of $\mathcal{M}$ that does not belong to an MEC of
$\mathcal{M}$ (i.e., $s\in S\cap S^{\prime}$) then then
$\mathit{Act}_{\mathcal{N}}(s)=\mathit{Act}_{\mathcal{M}}(s)$ and
$P^{\prime}(s,\alpha,s^{\prime})=P(s,\alpha,\iota^{-1}(s^{\prime}))$ for all
$s^{\prime}\in S^{\prime}$ and $\alpha\in\mathit{Act}_{\mathcal{M}}(s)$.

    * –

If $s=s_{\mathcal{E}_{i}}$ is a state representing MEC $\mathcal{E}_{i}$ of
$\mathcal{M}$ then (recall that we may view $\mathcal{E}_{i}$ as a set of
actions):

$\mathit{Act}_{\mathcal{N}}\bigl{(}s_{\mathcal{E}_{i}}\bigr{)}\ =\
\bigcup_{u\in
U_{i}}(\mathit{Act}_{\mathcal{M}}(u)\setminus\mathcal{E}_{i})\cup\\{\tau\\}$

The $\tau$-action stands for the deterministic transition to the fresh state
$\bot$, i.e.:

$P^{\prime}(s_{\mathcal{E}_{i}},\tau,\bot)=1$

Suppose now that $u\in U_{i}$ and
$\alpha\in\mathit{Act}_{\mathcal{M}}(u)\setminus\mathcal{E}_{i}$. Then, we set
$P^{\prime}(s_{\mathcal{E}_{i}},\alpha,s^{\prime})=P(u,\alpha,\iota^{-1}(s^{\prime}))$
for all $s^{\prime}\in S^{\prime}$.

    * –

The state $\bot$ is terminal, i.e.,
$\mathit{Act}_{\mathcal{N}}(\bot)=\varnothing$.

Thus, each terminal state of $\mathcal{M}$ is terminal in its MEC-quotient
$\mathcal{N}$ too. Vice versa, every terminal state of $\mathcal{N}$ is either
a terminal state of $\mathcal{M}$ or $\bot$. Moreover, $\mathcal{N}$ has no
end components, which implies that under every scheduler $\mathfrak{T}$ for
$\mathcal{N}$, a terminal state will be reached with probability 1.

In the main paper (Section 4.2), we use the notation
$\mathsf{noeff}_{\mathsf{tn}}$ rather than $\bot$.

######  Lemma 6 (Correspondence of an MDP and its MEC-quotient)

Let $\mathcal{M}$ be an MDP and $\mathcal{N}$ its MEC-quotient. Then, for each
scheduler $\mathfrak{S}$ for $\mathcal{M}$ there is a scheduler $\mathfrak{T}$
for $\mathcal{N}$ such that

$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond t)\ =\
\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{N}}(\Diamond t)$ for each terminal state
$t$ of $\mathcal{M}$ ($\dagger$)

and vice versa. Moreover, if ($\dagger$ ‣ 6) holds then
$\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{N}}(\Diamond\bot)$ equals the
probability for $\mathfrak{S}$ to generate an infinite path in $\mathcal{M}$
that eventually enters and stays forever in an end component.

###### Proof

Given a scheduler $\mathfrak{T}$ for $\mathcal{N}$, we pick an MD-scheduler
$\mathfrak{U}$ such that such that $\mathfrak{U}(u)\in\mathcal{E}_{i}$ for
each $u\in U_{i}$. Then, the corresponding scheduler $\mathfrak{S}$ for
$\mathcal{M}$ behaves as $\mathfrak{T}$ as long as $\mathfrak{T}$ does not
choose the $\tau$-transition to $\bot$. As soon as $\mathfrak{T}$ schedules
$\tau$ then $\mathfrak{S}$ behaves as $\mathfrak{U}$ from this moment on.

Vice versa, if we are given a scheduler $\mathfrak{S}$ for $\mathcal{M}$ then
a corresponding scheduler $\mathfrak{T}$ for $\mathcal{N}$ mimics
$\mathfrak{S}$ as long as $\mathfrak{S}$ has not visited a state belong to an
end component $\mathcal{E}_{i}$ of $\mathcal{M}$. Scheduler $\mathfrak{T}$
ignores $\mathfrak{S}$’s transitions inside an MEC $\mathcal{E}_{i}$ and takes
$\beta\in\bigcup_{u\in
U_{i}}(\mathit{Act}_{\mathcal{M}}(u)\setminus\mathcal{E}_{i})$ with the same
probability as $\mathfrak{S}$ leaves $\mathcal{E}_{i}$. With the remaining
probability mass, $\mathfrak{S}$ stays forever inside $\mathcal{E}_{i}$, which
is mimicked by $\mathfrak{T}$ by taking the $\tau$-transition to $\bot$.

For the formal definition of $\mathfrak{T}$, we use the following notation.
For simplicity, let us assume that $\mathsf{init}\notin U_{1}\cup\ldots\cup
U_{k}$. This yields $\mathsf{init}=\mathsf{init}^{\prime}$. Given a finite
path

$\pi=s_{0}\,\alpha_{0}\,s_{1}\,\alpha_{1}\ldots\alpha_{m-1}\,s_{m}$

in $\mathcal{M}$ with $s_{0}=\mathsf{init}$, let $\pi_{\mathcal{N}}$ the path
in $\mathcal{N}$ resulting from by replacing each maximal path fragment
$s_{h}\alpha_{h}\ldots\alpha_{j-1}s_{j}$ consisting of actions inside an
$\mathcal{E}_{i}$ with state $s_{\mathcal{E}_{i}}$. (Here, maximality means if
$h>0$ then $\alpha_{h-1}\notin\mathcal{E}_{i}$ and if $j<m$ then
$\alpha_{j+1}\notin\mathcal{E}_{i}$.) Furthermore, let
$p_{\pi}^{\mathfrak{S}}$ denote the probability for $\mathfrak{S}$ to generate
the path $\pi$ when starting in the first state of $\pi$.

Let $\rho$ be a finite path in $\mathcal{N}$ with first state $\mathsf{init}$
(recall that we suppose that $\mathcal{M}$’s initial state does not belong to
an MEC, which yields $\mathsf{init}=\mathsf{init}^{\prime}$) and
$\mathit{last}(\rho)\not=\bot$. Then, $\Pi_{\rho}$ denotes the set of finite
paths $\pi=s_{0}\,\alpha_{0}\,s_{1}\,\alpha_{1}\ldots\alpha_{m-1}\,s_{m}$ in
$\mathcal{M}$ such that (i) $\pi_{\mathcal{N}}=\rho$ and (ii) if $s_{m}\in
U_{i}$ then $\alpha_{m-1}\notin\mathcal{E}_{i}$. The formal definition of
scheduler $\mathfrak{T}$ is now as follows. Let $\rho$ be a finite path in
$\mathcal{N}$ where the last state $s$ of $\rho$ is non-terminal. If $s$ is a
state of $\mathcal{M}$ that does not belong to an MEC of $\mathcal{M}$ and
$\beta\in\mathit{Act}_{\mathcal{M}}(s)$ then:

$\mathfrak{T}(\rho)(\beta)\ \ =\ \
\sum_{\pi\in\Pi_{\rho}}p_{\pi}^{\mathfrak{S}}\cdot\mathfrak{S}(\pi)(\beta)$

If $s=s_{\mathcal{E}_{i}}$ and
$\beta\in\mathit{Act}_{\mathcal{N}}\bigl{(}s_{\mathcal{E}_{i}}\bigr{)}\setminus\\{\tau\\}$
then

$\mathfrak{T}(\rho)(\beta)\ \ =\ \
\sum_{\pi\in\Pi_{\rho}}p_{\pi}^{\mathfrak{S}}\cdot\mathrm{Pr}^{\mathit{res}(\mathfrak{S},\pi)}_{\mathcal{M},\mathit{last}(\pi)}\bigl{(}\
\text{``leave $\mathcal{E}_{i}$ via action $\beta$''}\ \bigr{)}$

where “leave $\mathcal{E}_{i}$ via action $\beta$” means the existence of a
prefix whose action sequence consists of actions inside $\mathcal{E}_{i}$
followed by action $\beta$. The last state of this prefix, however, could be a
state of $U_{i}$. (Note
$\beta\in\mathit{Act}_{\mathcal{N}}(s_{\mathcal{E}_{i}})$ means that $\beta$
could have reached a state outside $U_{i}$, but there might be states inside
$U_{i}$ that are accessible via $\beta$.) Similarly,

$\mathfrak{T}(\rho)(\tau)\ \ =\ \
\sum_{\pi\in\Pi_{\rho}}p_{\pi}^{\mathfrak{S}}\cdot\mathrm{Pr}^{\mathit{res}(\mathfrak{S},\pi)}_{\mathcal{M},\mathit{last}(\pi)}\bigl{(}\
\text{``stay forever in $\mathcal{E}_{i}$''}\ \bigr{)}$

where “stay forever in $\mathcal{E}_{i}$” means that only actions inside
$\mathcal{E}_{i}$ are performed. By induction on the length of $\rho$ we
obtain:

$p_{\rho}^{\mathfrak{T}}\ \ =\ \
\sum_{\pi\in\Pi_{\rho}}p_{\pi}^{\mathfrak{S}}$

But this yields $\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond t)$ =
$\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{N}}(\Diamond t)$ for each terminal state
$t$ of $\mathcal{M}$. Moreover,

$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\text{``eventually enter and stay
forever in $\mathcal{E}_{i}$''})$

equals the probability for $\mathfrak{T}$ to reach the terminal state $\bot$
via a path of the form $\rho\,\tau\,\bot$ where
$\mathit{last}(\rho)=s_{\mathcal{E}_{i}}$. ∎

##  Appendix 0.B Omitted Proofs and Details of Section 3

*

###### Proof

Assume that $\mathsf{Cause}$ is a SPR cause for $\mathsf{Eff}$ in
$\mathcal{M}$ and let $\mathfrak{S}$ be a scheduler that reaches
$\mathsf{Cause}$ with positive probability. Further, let

$C_{\mathfrak{S}}\stackrel{{\scriptstyle\text{\rm\tiny
def}}}{{=}}\\{c\in\mathsf{Cause}\ \mid\
\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}((\neg\mathsf{Cause})\,\mathrm{U}\,c)>0\\}$

and

$m\stackrel{{\scriptstyle\text{\rm\tiny def}}}{{=}}\min_{c\in
C_{\mathfrak{S}}}\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\
\Diamond\mathsf{Eff}\ |\ (\neg\mathsf{Cause})\,\mathrm{U}\,c\ ).$

As $\mathsf{Cause}$ is a SPR cause,
$m>\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{Eff})$. The set of
$\mathfrak{S}$-paths satisfying $\Diamond\mathsf{Cause}$ is the disjoint union
of the sets of $\mathfrak{S}$-paths satisfying
$(\neg\mathsf{Cause})\,\mathrm{U}\,c$ with $c\in C_{\mathfrak{S}}$. Hence,

$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{Eff}\mid\Diamond\mathsf{Cause})=\frac{\sum_{c\in
C_{\mathfrak{S}}}\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{Eff}\mid(\neg\mathsf{Cause})\,\mathrm{U}\,c)\cdot\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}((\neg\mathsf{Cause})\,\mathrm{U}\,c)}{\sum_{c\in
C_{\mathfrak{S}}}\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}((\neg\mathsf{Cause})\,\mathrm{U}\,c)}\geq
m.$

As $m>\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{Eff})$, the GPR
condition (GPR) is satisfied under $\mathfrak{S}$. ∎

##  Appendix 0.C Omitted Proofs and Details of Section 4

###  0.C.1 Switch to the MDP $\mathcal{M}_{[\mathsf{Cause}]}$

*

Obviously, condition (M) holds for $\mathsf{Cause}$ in $\mathcal{M}$ if and
only if condition (M) holds for $\mathsf{Cause}$ in
$\mathcal{M}_{[\mathsf{Cause}]}$. Furthermore, it is clear all SPR resp. GPR
causes of $\mathcal{M}$ are SPR resp. GPR causes in
$\mathcal{M}_{[\mathsf{Cause}]}$. So, it remains to prove the converse
direction. This will be done in Lemma 7 for SPR causes and in Lemma 8 for GPR
causes.

######  Lemma 7 (Criterion for strict probability-raising causes)

Suppose $\mathsf{Cause}$ is an SPR cause for $\mathsf{Eff}$ in
$\mathcal{M}_{[\mathsf{Cause}]}$. Then, $\mathsf{Cause}$ is an SPR cause for
$\mathsf{Eff}$ in $\mathcal{M}$.

###### Proof

We fix a state $c\in\mathsf{Cause}$. Recall also that we assume the states in
$\mathsf{Eff}$ to be terminal. Let
$\psi_{c}=(\neg\mathsf{Cause})\,\mathrm{U}\,c$,
$w_{c}=\mathrm{Pr}_{\mathcal{M},c}^{\min}(\Diamond\mathsf{Eff})$ and let
$\Upsilon_{c}$ denote the set of all schedulers $\mathfrak{U}$ for
$\mathcal{M}$ such that

  * •

$\mathrm{Pr}_{\mathcal{M}}^{\mathfrak{U}}(\psi_{c})>0$ and

  * •

$\mathrm{Pr}^{\mathit{res}(\mathfrak{U},\pi)}_{\mathcal{M},c}(\Diamond\mathsf{Eff})=w_{c}$
for each finite $\mathfrak{U}$-path $\pi$ from $\mathsf{init}$ to $c$.

Clearly, $\mathrm{Pr}^{\mathfrak{U}}_{\mathcal{M}}(\Diamond
c\wedge\Diamond\mathsf{Eff})=\mathrm{Pr}_{\mathcal{M}}^{\mathfrak{U}}(\Diamond
c)\cdot w_{c}$ for $\mathfrak{U}\in\Upsilon_{c}$.

As $\mathsf{Cause}$ is an SPR cause in $\mathcal{M}_{[\mathsf{Cause}]}$ we
have:

$w_{c}\ >\
\mathrm{Pr}^{\mathfrak{U}}_{\mathcal{M}}(\Diamond\mathsf{Eff})\quad\text{for
all schedulers $\mathfrak{U}\in\Upsilon_{c}$}$ (SPR-1)

The task is to prove that the SPR condition holds for $c$ and all schedulers
of $\mathcal{M}$ with $\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\psi_{c})>0$.

Suppose $\mathfrak{S}$ is a scheduler for $\mathcal{M}$ with
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\psi_{c})>0$. Then:

$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\psi_{c}\wedge\Diamond\mathsf{Eff})\
\ \geqslant\ \ \mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\psi_{c})\cdot w_{c}$

Moreover, there exists a scheduler
$\mathfrak{U}=\mathfrak{U}_{\mathfrak{S}}\in\Upsilon_{c}$ with

$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\psi_{c})=\mathrm{Pr}^{\mathfrak{U}}_{\mathcal{M}}(\psi_{c})$
and
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}((\neg\psi_{c})\wedge\Diamond\mathsf{Eff})=\mathrm{Pr}_{\mathcal{M}}^{\mathfrak{U}}((\neg\psi_{c})\wedge\Diamond\mathsf{Eff})$.

To see this, consider the scheduler $\mathfrak{U}$ that behaves as
$\mathfrak{S}$ as long as $c$ is not reached. As soon as $\mathfrak{U}$ has
reached $c$, scheduler $\mathfrak{U}$ switches mode and behaves as an MD-
scheduler minimizing the probability to reach an effect state.

The SPR condition holds for $c$ and $\mathfrak{S}$ if and only if

$\frac{\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\psi_{c}\wedge\Diamond\mathsf{Eff})}{\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\psi_{c})}\
\ >\ \ \mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{Eff})$
($\dagger$)

As

$\displaystyle\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{Eff})$
$\displaystyle=$
$\displaystyle\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\psi_{c}\wedge\Diamond\mathsf{Eff})\
+\
\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}((\neg\psi_{c})\wedge\Diamond\mathsf{Eff})$

we can equivalently convert condition ($\dagger$ ‣ 0.C.1) for $c$ and
$\mathfrak{S}$ to

$\displaystyle\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\psi_{c}\wedge\Diamond\mathsf{Eff})\cdot\frac{1-\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\psi_{c})}{\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\psi_{c})}\
\ >\ \
\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}((\neg\psi_{c})\wedge\Diamond\mathsf{Eff})$
($\ddagger$)

So, the remaining task is now to derive ($\ddagger$ ‣ 0.C.1) from (SPR-1).

(SPR-1) applied to scheduler $\mathfrak{U}=\mathfrak{U}_{\mathfrak{S}}$
yields:

$\begin{array}[]{lcl}w_{c}&\ \
>&\mathrm{Pr}^{\mathfrak{U}}_{\mathcal{M}}(\psi_{c}\wedge\Diamond\mathsf{Eff})\
+\
\mathrm{Pr}^{\mathfrak{U}}_{\mathcal{M}}((\neg\psi_{c})\wedge\Diamond\mathsf{Eff})\\\
\\\\[0.0pt] &=&\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\psi_{c})\cdot w_{c}\
+\
\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}((\neg\psi_{c})\wedge\Diamond\mathsf{Eff})\end{array}$

We conclude:

$\displaystyle\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\psi_{c}\wedge\Diamond\mathsf{Eff})\cdot\frac{1-\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\psi_{c})}{\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\psi_{c})}$
$\displaystyle\ \geqslant\ $
$\displaystyle\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\psi_{c})\cdot
w_{c}\cdot\frac{1-\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\psi_{c})}{\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\psi_{c})}$
$\displaystyle=$
$\displaystyle\bigl{(}1-\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\psi_{c})\bigr{)}\cdot
w_{c}$ $\displaystyle>$
$\displaystyle\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}((\neg\psi_{c})\wedge\Diamond\mathsf{Eff})$

Thus, ($\ddagger$ ‣ 0.C.1) holds for $c$ and $\mathfrak{S}$. ∎

######  Lemma 8 (Criterion for GPR causes)

Suppose $\mathsf{Cause}$ is an GPR cause for $\mathsf{Eff}$ in
$\mathcal{M}_{[\mathsf{Cause}]}$. Then, $\mathsf{Cause}$ is an GPR cause for
$\mathsf{Eff}$ in $\mathcal{M}$.

###### Proof

From the assumption that $\mathsf{Cause}$ is an GPR cause for $\mathsf{Eff}$
in $\mathcal{M}_{[\mathsf{Cause}]}$, we can conclude that the GPR condition
(GPR) holds for all schedulers $\mathfrak{S}$ that satisfy

$\mathrm{Pr}_{\mathcal{M}}^{\mathfrak{S}}(\Diamond\mathsf{Cause})>0$

and

$\mathrm{Pr}^{\mathit{res}(\mathfrak{S},\pi)}_{\mathcal{M},c}(\Diamond\mathsf{Eff})\
\ =\ \ \mathrm{Pr}^{\min}_{\mathcal{M},c}(\Diamond\mathsf{Eff})$

for each finite $\mathfrak{S}$-path from the initial state $\mathsf{init}$ to
a state $c\in\mathsf{Cause}$.

To prove that the GPR condition (GPR) holds for all schedulers $\mathfrak{S}$
that satisfy
$\mathrm{Pr}_{\mathcal{M}}^{\mathfrak{S}}(\Diamond\mathsf{Cause})>0$, we
introduce the following notation: We write

  * •

$\Sigma_{>0}$ for the set of all schedulers $\mathfrak{S}$ such that
$\mathrm{Pr}_{\mathcal{M}}^{\mathfrak{S}}(\Diamond\mathsf{Cause})>0$,

  * •

$\Sigma_{>0,\min}$ for the set of all schedulers with
$\mathrm{Pr}_{\mathcal{M}}^{\mathfrak{S}}(\Diamond\mathsf{Cause})>0$ such that

$\mathrm{Pr}^{\mathit{res}(\mathfrak{S},\pi)}_{\mathcal{M},c}(\Diamond\mathsf{Eff})\
\ =\ \ \mathrm{Pr}^{\min}_{\mathcal{M},c}(\Diamond\mathsf{Eff})$

for each finite $\mathfrak{S}$-path from the initial state $\mathsf{init}$ to
a state $c\in\mathsf{Cause}$.

It now suffices to show that for each scheduler $\mathfrak{S}\in\Sigma_{>0}$
there exists a scheduler $\mathfrak{S}^{\prime}\in\Sigma_{>0,\min}$ such that
if (GPR) holds $\mathfrak{S}^{\prime}$ then (GPR) holds for $\mathfrak{S}$.
So, let $\mathfrak{S}\in\Sigma_{>0}$.

For $c\in\mathsf{Cause}$, let $\Pi_{c}$ denote the set of finite paths
$\pi=s_{0}\,\alpha_{0}\,s_{1}\,\alpha_{1}\ldots\alpha_{n-1}\,s_{n}$ with
$s_{0}=\mathsf{init}$, $s_{n}=c$ and
$\\{s_{0},\ldots,s_{n-1}\\}\cap(\mathsf{Cause}\cup\mathsf{Eff})=\varnothing$.
Let

$w_{\pi}^{\mathfrak{S}}\ =\
\mathrm{Pr}^{\mathit{res}(\mathfrak{S},\pi)}_{\mathcal{M},c}(\Diamond\mathsf{Eff})$

Furthermore, let $p_{\pi}^{\mathfrak{S}}$ denote the probability for (the
cylinder set of) $\pi$ under scheduler $\mathfrak{S}$. Then

$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}((\neg\mathsf{Cause})\,\mathrm{U}\,c)\
=\ \sum_{\pi\in\Pi_{c}}p_{\pi}^{\mathfrak{S}}$

Moreover:

$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{Eff})\ \ =\ \
\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\neg\mathsf{Cause}\,\mathrm{U}\,\mathsf{Eff})\
+\sum_{c\in\mathsf{Cause}}\sum_{\pi\in\Pi_{c}}\\!\\!\\!p_{\pi}^{\mathfrak{S}}\cdot
w_{\pi}^{\mathfrak{S}}$

and,

$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\ \Diamond\mathsf{Eff}\ |\
\Diamond\mathsf{Cause}\ )\ \ =\ \
\frac{1}{\mathrm{Pr}_{\mathcal{M}}^{\mathfrak{S}}(\Diamond\mathsf{Cause})}\cdot\\!\\!\\!\sum_{c\in\mathsf{Cause}}\
\sum_{\pi\in\Pi_{c}}p_{\pi}^{\mathfrak{S}}\cdot w_{\pi}^{\mathfrak{S}}$

Thus, the condition (GPR) holds for the scheduler $\mathfrak{S}\in\Sigma_{>0}$
if and only if

$\displaystyle\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\neg\mathsf{Cause}\,\mathrm{U}\,\mathsf{Eff})+\sum_{c\in\mathsf{Cause}}\sum_{\pi\in\Pi_{c}}p_{\pi}^{\mathfrak{S}}\cdot
w_{\pi}^{\mathfrak{S}}$ $\displaystyle<$
$\displaystyle\frac{1}{\mathrm{Pr}_{\mathcal{M}}^{\mathfrak{S}}(\Diamond\mathsf{Cause})}\cdot\\!\\!\\!\sum_{c\in\mathsf{Cause}}\sum_{\pi\in\Pi_{c}}p_{\pi}^{\mathfrak{S}}\cdot
w_{\pi}^{\mathfrak{S}}$

The latter is equivalent to:

$\displaystyle\mathrm{Pr}_{\mathcal{M}}^{\mathfrak{S}}(\Diamond\mathsf{Cause})\cdot\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\neg\mathsf{Cause}\,\mathrm{U}\,\mathsf{Eff})\
\ +\ \
\mathrm{Pr}_{\mathcal{M}}^{\mathfrak{S}}(\Diamond\mathsf{Cause})\cdot\\!\\!\\!\sum_{c\in\mathsf{Cause}}\
\sum_{\pi\in\Pi_{c}}p_{\pi}^{\mathfrak{S}}\cdot w_{\pi}^{\mathfrak{S}}$
$\displaystyle<$ $\displaystyle\sum_{c\in\mathsf{Cause}}\
\sum_{\pi\in\Pi_{c}}p_{\pi}^{\mathfrak{S}}\cdot w_{\pi}^{\mathfrak{S}}$

which again is equivalent to:

$\displaystyle\mathrm{Pr}_{\mathcal{M}}^{\mathfrak{S}}(\Diamond\mathsf{Cause})\cdot\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\neg\mathsf{Cause}\,\mathrm{U}\,\mathsf{Eff})$
$\displaystyle<\ \ $
$\displaystyle\bigl{(}1-\mathrm{Pr}_{\mathcal{M}}^{\mathfrak{S}}(\Diamond\mathsf{Cause})\bigr{)}\cdot\\!\\!\\!\sum_{c\in\mathsf{Cause}}\
\sum_{\pi\in\Pi_{c}}p_{\pi}^{\mathfrak{S}}\cdot w_{\pi}^{\mathfrak{S}}$
(GPR-2)

Pick an MD-scheduler $\mathfrak{T}$ that minimizes the probability to reach
$\mathsf{Eff}$ from every state. In particular,
$w_{c}=w_{\pi}^{\mathfrak{T}}\leqslant w_{\pi}^{\mathfrak{S}}$ for every state
$c\in\mathsf{Cause}$ and every path $\pi\in\Pi_{c}$ (recall that
$w_{c}=\mathrm{Pr}^{\min}_{\mathcal{M},c}(\Diamond\mathsf{Eff})$). Moreover,
the scheduler $\mathfrak{S}$ can be transformed into a scheduler
$\mathfrak{S}_{\mathfrak{T}}\in\Sigma_{>0,\min}$ that is “equivalent” to
$\mathfrak{S}$ with respect to the global probability-raising condition. More
concretely, let $\mathfrak{S}_{\mathfrak{T}}$ denote the scheduler that
behaves as $\mathfrak{S}$ as long as $\mathfrak{S}$ has not yet visited a
state in $\mathsf{Cause}$ and behaves as $\mathfrak{T}$ as soon as a state in
$\mathsf{Cause}$ has been reached. Thus,
$p_{\pi}^{\mathfrak{S}}=p_{\pi}^{\mathfrak{S}_{\mathfrak{T}}}$ and
$\mathit{res}(\mathfrak{S}_{\mathfrak{T}},\pi)=\mathfrak{T}$ for each
$\pi\in\Pi_{c}$. This yields that the probability to reach
$c\in\mathsf{Cause}$ from $\mathsf{init}$ is the same under $\mathfrak{S}$ and
$\mathfrak{S}_{\mathfrak{T}}$, i.e.,
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond
c)=\mathrm{Pr}^{\mathfrak{S}_{\mathfrak{T}}}_{\mathcal{M}}(\Diamond c)$.
Therefore
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{Cause})=\mathrm{Pr}^{\mathfrak{S}_{\mathfrak{T}}}_{\mathcal{M}}(\Diamond\mathsf{Cause})$.
The latter implies that $\mathfrak{S}_{\mathfrak{T}}\in\Sigma_{>0}$, and hence
$\mathfrak{S}_{\mathfrak{T}}\in\Sigma_{>0,\min}$. Moreover, $\mathfrak{S}$ and
$\mathfrak{S}_{\mathfrak{T}}$ reach $\mathsf{Eff}$ without visiting
$\mathsf{Cause}$ with the same probability, i.e.,
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\neg\mathsf{Cause}\,\mathrm{U}\,\mathsf{Eff})=\mathrm{Pr}^{\mathfrak{S}_{\mathfrak{T}}}_{\mathcal{M}}(\neg\mathsf{Cause}\,\mathrm{U}\,\mathsf{Eff})$.

But this yields: if (0.C.1) holds for $\mathfrak{S}_{\mathfrak{T}}$ then
(0.C.1) holds for $\mathfrak{S}$. As (0.C.1) holds for
$\mathfrak{S}_{\mathfrak{T}}$ by assumption, this completes the proof. ∎

###  0.C.2 Proofs to Section 4.1

*

###### Proof

First, we show the soundness of Algorithm 4.2. By the virtue of Lemma 4.1 it
suffices to show that Algorithm 4.2 returns the correct answers “yes” or “no”
when the task is to check whether the singleton $\mathsf{Cause}=\\{c\\}$ is an
SPR cause in $\mathcal{N}=\mathcal{M}_{[c]}$. Recall the notation
$q_{s}=\mathrm{Pr}^{\max}_{\mathcal{M}_{[c]},s}(\Diamond\mathsf{Eff})$. We
abbreviate $q=q_{\mathsf{init}}$. Note that
$(\neg\mathsf{Cause})\,\mathrm{U}\,c$ is equivalent to $\Diamond c$.

For every scheduler $\mathfrak{S}$ of $\mathcal{N}$ we have
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{N},c}(\Diamond\mathsf{Eff})=w_{c}$.
Thus, $\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{N}}(\Diamond\mathsf{Eff}\ |\
\Diamond c)=w_{c}$ if $\mathfrak{S}$ is a scheduler of $\mathcal{N}$ with
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{N}}(\Diamond c)>0$.

Algorithm 4.2 correctly answers “no” (case 2 or 3.1) if $w_{c}=0$. Let us now
suppose that $w_{c}>0$. Thus, the SPR condition for $c$ reduces to
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{N}}(\Diamond\mathsf{Eff})<w_{c}$ for all
schedulers $\mathfrak{S}$ of $\mathcal{N}$ with
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{N}}(\Diamond c)>0$.

  * •

In case 1 of Algorithm 4.2 the answer “yes” is sound as then
$\mathrm{Pr}^{\max}_{\mathcal{N}}(\Diamond\mathsf{Eff})=q<w_{c}$.

  * •

For case 2 (i.e., if $q>w_{c}$), let $\mathfrak{T}$ be an MD-scheduler with
$\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{N},s}(\Diamond\mathsf{Eff})=q_{s}$ for
each state $s$ and pick an MD-scheduler $\mathfrak{S}$ with
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{N}}(\Diamond c)>0$. It is no restriction
to suppose that $\mathfrak{T}$ and $\mathfrak{S}$ realize the same end
components of $\mathcal{N}$. (Note that if state $s$ belongs to an end
component that is realized by $\mathfrak{T}$ then $s$ contained in a bottom
strongly connected component of the Markov chain induced by $\mathfrak{T}$.
But then $q_{s}=0$, i.e., no effect state is reachable from $s$ in
$\mathcal{N}$. Recall that all effect states are terminal and thus not
contained in end components. But then we can safely assume that $\mathfrak{T}$
and $\mathfrak{S}$ schedule the same action for state $s$.) Let $\lambda$ be
any real number with $1>\lambda>\frac{w_{c}}{q}$ and let $\mathcal{K}$ denote
the sub-MDP of $\mathcal{N}$ with state space $S$ where the enabled actions of
state $s$ are the actions scheduled for $s$ under one of the schedulers
$\mathfrak{T}$ or $\mathfrak{S}$. Let now $\mathfrak{U}$ be the MR-scheduler
$\lambda\mathfrak{T}\oplus(1{-}\lambda)\mathfrak{S}$ defined as in Notation
0.A.2 for the EC-free MDP resulting from $\mathcal{K}$ when collapsing
$\mathcal{K}$’s end components into a single terminal state. For the states
belonging to an end component of $\mathcal{K}$, $\mathfrak{U}$ schedules the
same action as $\mathfrak{T}$ and $\mathfrak{S}$. Then,
$\mathrm{Pr}^{\mathfrak{U}}_{\mathcal{N}}(\Diamond
t)=\lambda\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{N}}(\Diamond
t)+(1{-}\lambda)\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{N}}(\Diamond t)$ for all
terminal states $t$ of $\mathcal{N}$ and $t=c$. Hence:

$\mathrm{Pr}_{\mathcal{N}}^{\mathfrak{U}}(\Diamond c)\ \ \geqslant\ \
(1{-}\lambda)\cdot\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond c)\ \ >\ \
0$

and

$\mathrm{Pr}^{\mathfrak{U}}_{\mathcal{N}}(\Diamond\mathsf{Eff})\ \ \geqslant\
\ \lambda\cdot\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{M}}(\Diamond\mathsf{Eff})\
\ =\ \ \lambda\cdot q\ \ >\ \ w_{c}$

Thus, scheduler $\mathfrak{U}$ is a witness why (SPR) does not hold for $c$.

  * •

For case 3.1 pick an MD-scheduler $\mathfrak{S}$ of $\mathcal{M}^{\max}_{[c]}$
such that $c$ is reachable from $\mathsf{init}$ via a $\mathfrak{S}$-path and
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{N},s}(\Diamond\mathsf{Eff})=q_{s}$ for
all states $s$. Hence, (SPR) does not hold for $c$ and the scheduler
$\mathfrak{S}$.

  * •

The last case 3.2 has the property that
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{N}}(\Diamond c)=0$ for all schedulers
$\mathfrak{S}$ for $\mathcal{N}$ with
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{N}}(\Diamond\mathsf{Eff})=q=w_{c}$. But
then $\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{N}}(\Diamond c)>0$ implies
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{N}}(\Diamond\mathsf{Eff})<w_{c}$ as
required in (SPR).

The polynomial runtime of Algorithm 4.2 follows from the fact that minimal and
maximal reachability probabilities and hence also the MDPs
$\mathcal{N}=\mathcal{M}_{[c]}$ and its sub-MDP $\mathcal{M}^{\max}_{[c]}$ can
be computed in polynomial time. ∎

######  Lemma 9 (Criterion for the existence of PR causes (Lemma 5))

Let $\mathcal{M}$ be an MDP and $\mathsf{Eff}$ a nonempty set of states. The
following statements are equivalent:

  * (a)

$\mathsf{Eff}$ has an SPR cause in $\mathcal{M}$,

  * (b)

$\mathsf{Eff}$ has a GPR cause in $\mathcal{M}$,

  * (c)

there is a state $c_{0}\in S\setminus\mathsf{Eff}$ such that the singleton
$\\{c_{0}\\}$ is an SPR cause (and therefore a GRP cause) for $\mathsf{Eff}$
in $\mathcal{M}$.

In particular, the existence of SPR/GPR causes can be checked with Algorithm
4.2 in polynomial time.

###### Proof

Obviously, statement (c) implies statements (a) and (b). The implication “(a)
$\Longrightarrow$ (b)” follows from Lemma 1. We now turn to the proof of “(b)
$\Longrightarrow$ (c)”. For this, we assume that we are given a GPR cause
$\mathsf{Cause}$ for $\mathsf{Eff}$ in $\mathcal{M}$. For
$c\in\mathsf{Cause}$, let
$w_{c}=\mathrm{Pr}^{\min}_{\mathcal{M},c}(\Diamond\mathsf{Eff})$. Pick a state
$c_{0}\in\mathsf{Cause}$ such that
$w_{c_{0}}=\max\\{w_{c}:c\in\mathsf{Cause}\\}$. For every scheduler
$\mathfrak{S}$ for $\mathcal{M}$ that minimizes the effect probability
whenever it visits a state in $\mathsf{Cause}$, and visits $\mathsf{Cause}$
with positive probability, the conditional probability
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{Eff}|\Diamond\mathsf{Cause})$
is a weighted average of the values $w_{c}$, $c\in\mathsf{Cause}$, and thus
bounded by $w_{c_{0}}$. Using Lemma 4.1 it is now easy to see that
$\\{c_{0}\\}$ is both an SPR and a GPR cause for $\mathsf{Eff}$. ∎

###  0.C.3 Construction justifying assumptions (A1)-(A3)

In Section 4, we are given an MDP
$\mathcal{M}=(S,\mathit{Act},P,\mathsf{init})$ with two disjoint sets of
states $\mathsf{Cause}$ and $\mathsf{Eff}$. The states in $\mathsf{Eff}$ are
terminal.

Here, we provide the missing details of the transformation for the assumptions
(A1)-(A3) in Section 4 that are listed here again:

(A1)

$\mathsf{Eff}=\\{\mathsf{eff}_{\mathsf{unc}},\mathsf{eff}_{\mathsf{cov}}\\}$
consists of two terminal states.

(A2)

For every state $c\in\mathsf{Cause}$, there is only a single enabled action,
say $\mathit{Act}(c)=\\{\gamma\\}$, and there exists
$w_{c}\in[0,1]\cap\mathbb{Q}$ such that
$P(c,\tau,\mathsf{eff}_{\mathsf{cov}})=w_{c}$ and
$P(c,\tau,\mathsf{noeff}_{\mathsf{fp}})=1-w_{c}$. where
$\mathsf{noeff}_{\mathsf{fp}}$ is a terminal non-effect state and
$\mathsf{noeff}_{\mathsf{fp}}$ and $\mathsf{eff}_{\mathsf{cov}}$ are only
accessible via the $\gamma$-transition from the states $c\in\mathsf{Cause}$.

(A3)

$\mathcal{M}$ has no end components and there is a further terminal state
$\mathsf{noeff}_{\mathsf{tn}}$ and an action $\tau$ such that
$\tau\in\mathit{Act}(s)$ implies $P(s,\tau,\mathsf{noeff}_{\mathsf{tn}})=1$.

The terminal states $\mathsf{eff}_{\mathsf{unc}}$,
$\mathsf{eff}_{\mathsf{cov}}$, $\mathsf{noeff}_{\mathsf{fp}}$ and
$\mathsf{noeff}_{\mathsf{tn}}$ are supposed to be pairwise distinct.
$\mathcal{M}$ can have further terminal states representing true negatives.
These could be identified with $\mathsf{noeff}_{\mathsf{tn}}$, but this is
irrelevant for our purposes.

Assumptions (A1) and (A2) are established as described in the main body of the
paper (Section 4.2) by switching to the MDP $\mathcal{M}_{[\mathsf{Cause}]}$ –
which is justified by Lemma 4.1 – and by renaming and collapsing terminal
states resulting in an MDP $\mathcal{M}^{\prime}$.

Now, let $\mathcal{N}$ be the MEC-quotient of $\mathcal{M}^{\prime}$ (see
Appendix 0.A.3). Let $\mathsf{noeff}_{\mathsf{tn}}$ be the state to which we
add a $\tau$-transition with probability $1$ from each MEC that we collapse in
the MEC-quotient. That is, $\mathsf{noeff}_{\mathsf{tn}}=\bot$ with the
notations of Definition 2.

###### Lemma 10

For each scheduler $\mathfrak{S}$ for $\mathcal{M}_{[\mathsf{Cause}]}$, there
is a scheduler $\mathfrak{T}$ for $\mathcal{N}$, and vice versa, such that

  * •

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

  * •

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

  * •

$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}_{[\mathsf{Cause}]}}(\Diamond\mathsf{Cause}\land\Diamond\mathsf{Eff})=\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{N}}(\Diamond\mathsf{eff}_{\mathsf{cov}})$.

###### Proof

By Lemma 6, there is a scheduler $\mathfrak{T}$ for $\mathcal{N}$ for each
scheduler $\mathfrak{S}$ for $\mathcal{M}^{\prime}$ such that each terminal
state is reached with the same probability under $\mathfrak{T}$ in
$\mathcal{N}$ and under $\mathfrak{S}$ in $\mathcal{M}^{\prime}$. The state
$\mathsf{eff}_{\mathsf{cov}}$ is also present in
$\mathcal{M}_{[\mathsf{Cause}]}$ under the name $\mathsf{eff}$ and reached
with the same probability as in $\mathcal{M}^{\prime}$ when $\mathfrak{S}$ is
considered as a scheduler for $\mathcal{M}_{[\mathsf{Cause}]}$. The state
$\mathsf{eff}$ is furthermore reached in $\mathcal{M}_{[\mathsf{Cause}]}$ if
and only if $\Diamond\mathsf{Cause}\land\Diamond\mathsf{Eff}$ is satisfied
along a run. The set of terminal states in $\mathsf{Eff}$ is obtained from the
set $\mathsf{Eff}$ in $\mathcal{M}_{[\mathsf{Cause}]}$ by collapsing states.
As a scheduler $\mathfrak{S}$ can be viewed as a scheduler for both MDPs and
these MDPs agree except for the terminal states, the first equality follows as
well. As the probability to reach $\mathsf{Cause}$ is the sum of the
probabilities to reach the terminal states $\mathsf{eff}_{\mathsf{cov}}$ and
$\mathsf{noeff}_{\mathsf{fp}}$ in $\mathcal{N}$ and $\mathcal{M}^{\prime}$ and
as these states are only renamed in the transition from
$\mathcal{M}_{[\mathsf{Cause}]}$ to $\mathcal{M}^{\prime}$, the claim follows.
∎

From Lemma 10 and Lemma 4.1, we conclude the following corollary that
justifies working under assumptions (A1)-(A3) in Section 4.

###### Corollary 2

The set $\mathsf{Cause}$ is a SPR/GPR cause for $\mathsf{Eff}$ in
$\mathcal{M}$ if and only if $\mathsf{Cause}$ is a SPR/GPR cause for
$\mathsf{Eff}$ in $\mathcal{N}$.

###### Proof

By Lemma 10, for each scheduler $\mathfrak{S}$ for
$\mathcal{M}_{[\mathsf{Cause}]}$, there is a scheduler $\mathfrak{T}$ for
$\mathcal{N}$ such that all relevant probabilities agree, and vice versa. So,
$\mathsf{Cause}$ is a GPR cause for $\mathsf{Eff}$ in
$\mathcal{M}_{[\mathsf{Cause}]}$ if and only if it is a GPR cause in
$\mathcal{N}$. By Lemma 4.1, $\mathsf{Cause}$ is a GPR cause for
$\mathsf{Eff}$ in $\mathcal{M}_{[\mathsf{Cause}]}$ if and only if it is a GPR
cause in $\mathcal{M}$. ∎

###  0.C.4 Proofs to Section 4.2

*

###### Proof

Let $\mathfrak{U}$ be a scheduler with
$\mathrm{Pr}^{\mathfrak{U}}_{\mathcal{M}}(\Diamond\mathsf{Cause})>0$ violating
(GPR-1), i.e.:

$\mathrm{Pr}_{\mathcal{M}}^{\mathfrak{U}}(\Diamond\mathsf{Cause})\cdot\mathrm{Pr}^{\mathfrak{U}}_{\mathcal{M}}(\Diamond\mathsf{eff}_{\mathsf{unc}})\
<\
\bigl{(}1{-}\mathrm{Pr}_{\mathcal{M}}^{\mathfrak{U}}(\Diamond\mathsf{Cause})\bigr{)}\cdot\\!\\!\\!\\!\\!\sum_{c\in\mathsf{Cause}}\\!\\!\\!\\!\\!\mathrm{Pr}^{\mathfrak{U}}_{\mathcal{M}}(\Diamond
c)\cdot w_{c}.$

We will show how to transform $\mathfrak{U}$ into an MR-scheduler
$\mathfrak{T}$ that schedules the $\tau$-transitions to
$\mathsf{noeff}_{\mathsf{tn}}$ with probability 0 or 1. For this, we regard
the set $U$ of states $u$ that have a $\tau$-transition to
$\mathsf{noeff}_{\mathsf{tn}}$ (recall that then
$P(u,\tau,\mathsf{noeff}_{\mathsf{tn}})=1$) and where
$0<\mathfrak{U}(u)(\tau)<1$. We now process the $U$-states in an arbitrary
order, say $u_{1},\ldots,u_{k}$, and generate a sequence
$\mathfrak{T}_{0}=\mathfrak{U},\mathfrak{T}_{1},\ldots,\mathfrak{T}_{k}$ of
MR-schedulers such that for $i\in\\{1,\ldots,k\\}$:

  * •

$\mathfrak{T}_{i}$ refutes the GPR condition (or equivalently condition
(GPR-1) from Lemma 2)

  * •

$\mathfrak{T}_{i}$ agrees with $\mathfrak{T}_{i-1}$ for all states but
$u_{i}$,

  * •

$\mathfrak{T}_{i}(u_{i})(\tau)\in\\{0,1\\}$.

Thus, the final scheduler $\mathfrak{T}_{k}$ satisfies the desired properties.

We now explain how to derive $\mathfrak{T}_{i}$ from $\mathfrak{T}_{i-1}$. Let
$i\in\\{1,\ldots,k\\}$, $\mathfrak{V}=\mathfrak{T}_{i-1}$, $u=u_{i}$ and
$y=1{-}\mathfrak{V}(u)(\tau)$. Then, $0<y<1$ (as $u\in U$ and by definition of
$U$) and
$y=\sum_{\alpha\in\mathit{Act}(u)\setminus\\{\tau\\}}\mathfrak{V}(u)(\alpha)$.

For $x\in[0,1]$, let $\mathfrak{V}_{x}$ denote the MR-scheduler that agrees
with $\mathfrak{V}$ for all states but $u$, for which $\mathfrak{V}_{x}$’s
decision is as follows:

$\mathfrak{V}_{x}(u)(\tau)=1{-}x,\qquad\mathfrak{V}_{x}(u)(\alpha)=\mathfrak{V}(u)(\alpha)\cdot\frac{x}{y}\quad\text{for
$\alpha\in\mathit{Act}(u)\setminus\\{\tau\\}$}$

Obviously, $\mathfrak{V}_{y}=\mathfrak{V}$. We now show that at least one of
the two MR-schedulers $\mathfrak{V}_{0}$ or $\mathfrak{V}_{1}$ also refutes
the GPR condition. For this, we suppose by contraction that this is not the
case, which means that the GPR condition holds for both.

Let $f:[0,1]\to[0,1]$ be defined by

$f(x)\ =\
\mathrm{Pr}_{\mathcal{M}}^{\mathfrak{V}_{x}}(\Diamond\mathsf{Cause})\cdot\mathrm{Pr}^{\mathfrak{V}_{x}}_{\mathcal{M}}(\Diamond\mathsf{eff}_{\mathsf{unc}})-\bigl{(}1{-}\mathrm{Pr}_{\mathcal{M}}^{\mathfrak{V}_{x}}(\Diamond\mathsf{Cause})\bigr{)}\cdot\\!\\!\\!\\!\\!\sum_{c\in\mathsf{Cause}}\\!\\!\\!\\!\\!\\!\mathrm{Pr}^{\mathfrak{V}_{x}}_{\mathcal{M}}(\Diamond
c)\cdot w_{c}$

As $\mathfrak{V}=\mathfrak{V}_{y}$ violates (GPR-1), while $\mathfrak{V}_{0}$
and $\mathfrak{V}_{1}$ satisfy (GPR-1) we obtain:

$f(0),f(1)<0\qquad\text{and}\qquad f(y)\geqslant 0$

We now split $\mathsf{Cause}$ into the set $C$ of states $c\in\mathsf{Cause}$
such that there is a $\mathfrak{V}$-path from $\mathsf{init}$ to $c$ that
traverses $u$ and $D=\mathsf{Cause}\setminus C$. Thus,
$\mathrm{Pr}^{\mathfrak{V}_{x}}_{\mathcal{M}}(\Diamond\mathsf{Cause})=p_{x}+p$
where $p_{x}=\mathrm{Pr}^{\mathfrak{V}_{x}}(\Diamond C)$ and
$p=\mathrm{Pr}^{\mathfrak{V}}(\Diamond D)$. Similarly,
$\mathrm{Pr}^{\mathfrak{V}_{x}}_{\mathcal{M}}(\Diamond\mathsf{eff}_{\mathsf{unc}})$
has the form $q_{x}+q$ where
$q_{x}=\mathrm{Pr}^{\mathfrak{S}_{x}}_{\mathcal{M}}(\Diamond(u\wedge\Diamond\mathsf{eff}_{\mathsf{unc}}))$
and $q=\mathrm{Pr}^{\mathfrak{S}_{x}}_{\mathcal{M}}((\neg
u)\,\mathrm{U}\,\mathsf{eff}_{\mathsf{unc}})$. With
$p_{x,c}=\mathrm{Pr}^{\mathfrak{V}_{x}}_{\mathcal{M}}(\Diamond c)$ for $c\in
C$ and $p_{d}=\mathrm{Pr}^{\mathfrak{V}}_{\mathcal{M}}(\Diamond d)$ for $d\in
D$, let

$v_{x}=\sum_{c\in C}p_{x,c}\cdot w_{c}\qquad\text{and}\qquad v=\sum_{d\in
D}p_{d}\cdot w_{d}$

As $y$ is fixed, the values $p_{y},p_{y,c},q_{y},v_{y}$ can be seen as
constants. Moreover, the values $p_{x},p_{x,c},q_{x},v_{x}$ differ from