This is the extended version of the conference version at FoSSaCS 2022
[BFPZ22] [a] [a] [a]

# Foundations of probability-raising causality
in Markov decision processes

Christel Baier 0000-0002-5321-9343  ,  Jakob Piribauer 0000-0003-4829-0476
and  Robin Ziemek 0000-0002-8490-1433  Technische Universität Dresden
<EMAIL_ADDRESS><EMAIL_ADDRESS>robin.ziemek@tu-
dresden.de

###### Abstract.

This work introduces a novel cause-effect relation in Markov decision
processes using the probability-raising principle. Initially, sets of states
as causes and effects are considered, which is subsequently extended to
regular path properties as effects and then as causes. The paper lays the
mathematical foundations and analyzes the algorithmic properties of these
cause-effect relations. This includes algorithms for checking cause conditions
given an effect and deciding the existence of probability-raising causes. As
the definition allows for sub-optimal coverage properties, quality measures
for causes inspired by concepts of statistical analysis are studied. These
include recall, coverage ratio and f-score. The computational complexity for
finding optimal causes with respect to these measures is analyzed.

###### Key words and phrases:

Markov decision process, probabilistic causality, probability-raising, binary
classifier

This work was funded by DFG grant 389792660 as part of TRR 248 – CPEC (see
https://perspicuous-computing.science, 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.

##  1\. Introduction

In recent years, scientific and technological advancement in computer science
and engineering led to an ever increasing influence of computer systems on our
everyday lives. A lot of decisions which were historically done by humans are
now in the hands of intelligent systems. At the same time, these systems grow
more and more complex, and thus, harder to understand. This poses a huge
challenge in the development of reliable and trustworthy systems. Therefore,
an important task of computer science today is the broad development of
comprehensive and versatile ways to understand modern software and cyber
physical systems.

The area of formal verification aims to prove the correctness of a system with
respect to a specification. While the formal verification process can provide
guarantees on the behavior of a system, such a result alone does not tell much
about the inner workings of the system. To give some additional insight,
counterexamples, invariants or related certificates as a form of verifiable
justification that a system does or does not behave according to a
specification have been studied extensively (see e.g., [MP95, CGP99, Nam01]).
These kinds of certificates, however, do not allow us to understand the system
behavior to a full extend. This establishes a desideratum for a more
comprehensive understanding of _why_ a system satisfies or violates a
specification. Explications of the system are needed to assess _how_ different
components influence its behavior and performance. It is widely believed that
the analysis of causal relations between occurring events during the execution
of a system constitute a strong tool to form such an understanding.

The majority of prior work in this direction relies on causality notions based
on Lewis’ counterfactual principle [Lew73] which states that 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
[HP01] via structural equation models. This inspired formal definitions of
causality and related notions of blameworthiness and responsibility in Kripke
and game structures as well as reactive systems (see, e.g., [CHK08, BBC+12,
Cho16, YD16, FH19, YDJ+19, BFM21, CFF+22]).

A lot of systems are to a certain extend influenced by probabilistic events.
Thus, a branch of formal methods is studying probabilistic models such as
Markov chains (MCs) which are purely probabilistic or Markov decision
processes (MDPs) which combine non-determinism and probabilism. This gives
rise to another approach to the concept of causality in a probabilistic
setting, since the statement of counterfactual reasoning can be interpreted
more gently in a probabilistic setting: Instead of saying “the effect would
not have occurred, if the cause had not happened”, we can say “the probability
of the effect would have been lower if the cause would not have occurred”.
This interpretation leads to the widely accepted _probability-raising
principle_ which also has its roots in philosophy [Rei56, Sup70, Eel91, Hit16]
and has been refined by Pearl [Pea09] 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 causality in the context of
formal methods is comparably rare and has concentrated on the purely
probabilistic setting in Markov chains (see, e.g., [KM09, Kle12, ZPF+22] and
the discussion of related work below). To the best of our knowledge,
probabilistic causation for probabilistic operational models with
nondeterminism has not been studied before.

In this work, we formalize principles (C1) and (C2) for Markov decision
processes. We start in a basic setting by focusing on reachability properties
where both effect and cause are sets of states. Later, we naturally extend
this framework by considering the effect to be an $\omega$-regular path
property while causes can either still be state-based or $\omega$-regular co-
safety path properties.

As we like to to have probability-raising inherent in the MDP, we require (C1)
under every scheduler. Thus, the cause-effect relation holds for every
resolution of the non-deterministic choices. We consider two natural ways to
interpret condition (C1): On one hand, the probability-raising property can be
required locally for each element of the cause. This results in a strict
property which requires that after each execution leading to the cause the
probability of effect has been raised. 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 globally as a unit in (C1) leading to the notion of _global
probability-raising (GPR) cause_. This way, the causal relation can also be
formulated between properties instead of considering individual elements or
executions to be causal. Considering the cause as a whole is also better
suited when further constraints are imposed on the candidates for cause sets.
E.g. if the set of non-terminal states of the given MDP is partitioned into
sets of states $S_{i}$ under control of different agents $i$, $1\leq i\leq k$
and the task is to identify which agent’s decisions might 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.

Even with the distinction between strict and global probability-raising
causality, different causes might still vary substantially regarding how well
they predict the effect. Within Markov decision processes this intuitively
coincides with how well the executions exhibiting the cause cover executions
showing the effect. However, solely focusing on broader coverage might also
lead to more trivial causal relations. In order to take this trade off into
account, we take inspiration from measures for binary classifiers used in
statistical analysis (see, e.g., [Pow11]) to introduce quality measures for
causes. These allow us to compare different 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. The _f-score_ , a widely used quality
measure for binary classifiers, is the harmonic mean of recall and precision,
where the precision is the probability that the cause is followed by the
effect. Finally, we address the computation of arbitrary quality measures as
long as they can be represented as algebraic functions.

### Contributions.

In this work we build mathematical and algorithmic foundations for
probabilistic causation in Markov decision processes based on the principles
(C1) and (C2). In the setting where the effect is represented as a set of
terminal states, we introduce strict and global probability-raising cause sets
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 a cause set for a given effect set
(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 sets
(Section 5.2) and characterize the computational complexity of finding optimal
cause sets with respect to the different measures (Section 5.3). We then
extend the setting to $\omega$-regular effects (Section 6.1), and evaluate how
established properties transfer to this setting. We observe that in this
extension SPR causes can be viewed as a collection of GPR causes. Finally we
discuss the case where causes are also path properties, namely,
$\omega$-regular co-safety properties and investigate how this more general
perspective affects cause-effect relations (Section 6.2). Here, the class of
potential cause candidates is greatly increased, which especially affects
finding optimal causes. Table 1 summarizes our complexity results.

Table 1. Complexity results for MDPs and Markov chains (MC) with fixed
effects. The $\omega$-regular effects are given as deterministic Rabin
automata, $\omega$-regular co-safety properties as causes are given as
deterministic finite automata accepting good prefixes.

sets of states as causes and effects 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{coNP}$ and $\in\mathrm{P}$
for MC poly-time poly-space threshold problems $\in\Sigma^{P}_{2}$ and
$\mathrm{NP}$-hard and $\mathrm{NP}$-complete for MC sets of states as causes
and $\omega$-regular effects 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{coNP}$ and
$\in\mathrm{P}$ for MC poly-time $\mathrm{PF}^{\mathrm{NP}}$ (as def. in
[Sel94]) threshold problems $\in\mathrm{coNP}$ poly-space threshold problem
$\in\Sigma^{P}_{2}$ GPR $\in\mathrm{coNP}$ and $\in\mathrm{P}$ for MC poly-
time poly-space threshold problems $\in\Sigma^{P}_{2}$ $\mathrm{NP}$-hard
$\omega$-regular co-safety properties as causes and $\omega$-regular effects
for fixed cause property $\mathsf{rCause}$ find optimal cause compute quality
values check PR condition covratio-optimal = recall-optimal (recall, covratio,
f-score) f-score-optimal SPR difficulty illustrated in Example 6.2.1 poly-time
optimal cause known, computation unclear open GPR $\in\mathrm{coNP}$ and
$\in\mathrm{P}$ for MC poly-time in general, no optimal causes open

### Related work

Previous work in the direction of probabilistic causation in stochastic
operational models has mainly concentrated on Markov chains. Kleinberg [KM09,
Kle12] 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 [BDF+21]. Our notion of strict probability-raising causes
interpreted in Markov chains corresponds to Kleinberg’s prima facie causes
with the exception of a minimality condition forbidding redundant elements in
our definition. Ábrahám et al [ÁB18] 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 strict probability-raising causes up to minimality. Cause-effect
relations in Markov chains where effects are $\omega$-regular properties and
the causes are sets of paths has been introduced in [ZPF+22]. It relies on a
strict probability-raising condition, but uses a probability threshold $p$
instead of directly requiring probability-raising. Therefore, [ZPF+22] permits
a non-strict inequality in the PR condition with the consequence that causes
always exist, which is not the case for our notions. However, a minimal good
prefix of a co-safety strict probability-raising cause in a Markov chains
corresponds to a probability-raising path in [ZPF+22].

The survey article [BDF+21] introduces notions of global probability-raising
causes for Markov chains, where causes and effects can be path properties.
[BDF+21]’s notion of _reachability causes_ in Markov chains directly
corresponds to our notion GPR causes, the only difference being that [BDF+21]
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. On the other hand if we restrict [BDF+21]’s notion of global PR-
cause to $\omega$-regular effects and co-safety causes, this corresponds to
our notion co-safety GPR cause with the exception of the minimality condition.
The same can be said to the correspondence of local PR-causes from [BDF+21]
and co-safety SPR causes.

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 [DFT20] 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, 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 [KLL11, Lei15]. 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 [BFM21].

##  2\. Preliminaries

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

###  2.1. Markov decision processes

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

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)$. 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\in\mathit{Act}\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})^{*}\times
S\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. 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}\ldots\alpha_{n-1}\,s_{n}$ then
$\mathit{last}(\pi)=s_{n}$.

A _(randomized) scheduler_ $\mathfrak{S}$ is a function that maps each finite
non-maximal path $s_{0}\alpha_{0}\dots 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. A path $\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\\}$. Given 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$. Intuitively speaking,
$\mathit{res}(\mathfrak{S},\pi)$ behaves like $\mathfrak{S}$ after $\pi$ has
already been seen.

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.

###  2.2. MR-scheduler in MDPs without ECs

The following preliminary lemma is folklore (see, e.g., [Kal20, Theorem 9.16])
and used in the paper in the following form.

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

Consider an MDP $\mathcal{M}=(S,\mathit{Act},P,\mathsf{init})$ 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$.

As a consequence we also have the following.

######  Lemma 2 (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 2.1.

Thanks to Lemma 1 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 1 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)\ \ =\ \
\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$.

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

###  2.3. MEC-quotient

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

[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 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 (as we 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$. $\lhd$

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 Section
4.2, we use the notation $\mathsf{noeff}_{\mathsf{tn}}$ rather than $\bot$.

The original MDP and its MEC-quotient have been found to be connected by the
following lemma (see also [dA97, dA99]).

######  Lemma 3 (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}$ (1)

and vice versa. Moreover, if (1) 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 2.2.

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, 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 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}$ and 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 the probability under $\mathfrak{S}$ to
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}}$.

###  2.4. Automata and $\omega$-regular languages

In order to represent an $\omega$-regular language, we use _deterministic
Rabin automata_ (DRA). A DRA is a tuple
$\mathcal{A}=(Q,\Sigma,q_{0},\delta,\mathrm{Acc})$ where $Q$ is a finite set
of states, $\Sigma$ an alphabet, $q_{0}$ the initial state,
$\delta:Q\times\Sigma\to Q$ the transition function and $\mathrm{Acc}\subseteq
2^{Q}\times 2^{Q}$ the acceptance set. The _run_ of $\mathcal{A}$ on a word
$w=w_{0}w_{1}\dots\in\Sigma^{\omega}$ is the sequence $\tau=q_{0}q_{1}\ldots$
of states such that $\delta(q_{i},w_{i})=q_{i+1}$ for all $i$. It is
_accepting_ if there exists a pair $(L,K)\in\mathrm{Acc}$ such that $L$ is
only visited finitely often and $K$ is visited infinitely often by $\tau$. The
language $\mathcal{L}(\mathcal{A})$ is the set of all words
$w\in\Sigma^{\omega}$ on which the run of $\mathcal{A}$ is accepting.

A _good prefix_ $\pi$ for an $\omega$-regular language $\mathcal{L}$ is a
finite word such that all infinite extensions of $\pi$ belong to
$\mathcal{L}$. An $\omega$-regular language $\mathcal{L}$ is called a _co-
safety language_ if all words in $\mathcal{L}$ have a prefix that is a good
prefix for $\mathcal{L}$. A co-safety language $\mathcal{L}$ is uniquely
determined by the regular set of minimal good prefixes of words in
$\mathcal{L}$.

The regular language of minimal good prefixes of a co-safety $\mathcal{L}$
which uniquely determines $\mathcal{L}$ can be represented by a _deterministic
finite automaton_ (DFA). A DFA is a tuple
$\mathcal{A}=(Q,\Sigma,q_{0},\delta,\mathrm{Acc})$ where $Q$ is a finite set
of states, $\Sigma$ an alphabet, $q_{0}$ the initial state,
$\delta:Q\times\Sigma\to Q$ the transition function and $\mathrm{Acc}\subseteq
Q$ the acceptance set. The _run_ of $\mathcal{A}$ on a finite word
$w=w_{0}w_{1}\dots w_{n}$ is the sequence $\tau=q_{0}q_{1}\ldots q_{n}$ of
states such that $\delta(q_{i},w_{i})=q_{i+1}$ for all $i$. It is _accepting_
if $q_{n}\in\mathrm{Acc}$. The language $\mathcal{L}(\mathcal{A})$ is the set
of all words $w\in\Sigma^{*}$ on which the run of $\mathcal{A}$ is accepting.

Given an MDP $\mathcal{M}=(S,\mathit{Act},P,\mathsf{init})$ and a DFA
$\mathcal{A}=(Q,\Sigma,q_{0},\delta,\mathit{Acc})$ with $\Sigma\subseteq
S^{*}$ we define the _product MDP_ $\mathcal{M}\otimes\mathcal{A}=(S\times
Q,\mathit{Act},P^{\prime},\mathsf{init}^{\prime})$ with
$P^{\prime}(<s,q>,\alpha,<t,r>)=P(s,\alpha,t)$ if $r=\delta(q,s)$ and $0$
otherwise, and $\mathsf{init}^{\prime}=\delta(q_{0},\mathsf{init})$. The same
construction works for the product of an MDP with a DRA. The difference comes
from the acceptance condition encoded in the second components of states of
the product MDP.

##  3\. Strict and global probability-raising causes

Our contribution starts by providing novel 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. Here, 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. As the effect set is fixed, the assumption that all effect
states are terminal contributes to the temporal priority as stated by (C2). We
may also assume that every state $s\in S$ is reachable from $\mathsf{init}$.

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

[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}$ such that for each $c\in\mathsf{Cause}$ we
have
$\mathrm{Pr}^{\max}_{\mathcal{M}}((\neg\mathsf{Cause})\,\mathrm{U}\,c)>0$.
Then, $\mathsf{Cause}$ is said to be a _GPR cause_ for $\mathsf{Eff}$ iff the
following condition (G) holds:

(G):

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

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

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

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

$\displaystyle\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)

Note that we only consider sets $\mathsf{Cause}$ as PR cause when each state
in $c\in\mathsf{Cause}$ is accessible from $\mathsf{init}$ without traversing
other states in $\mathsf{Cause}$. This can be seen as a minimality condition
ensuring that a cause does not contain redundant elements. However, we could
omit this requirement without affecting the covered effects (events where an
effect state is reached after visiting a cause state) or uncovered effects
(events where an effect state is reached without visiting a cause state
before). More concretely, whenever a set $C\subseteq S\setminus\mathsf{Eff}$
satisfies conditions (G) or (S) then the set 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. On the other hand the set
$\mathsf{Cause}$ is disjoint of the effect $\mathsf{Eff}$ to ensure temporal
priority (C2).

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

We first observe that SPR and 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 4 (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}$.

The direction from SPR cause to GPR cause even holds in general as the event
$\Diamond\mathsf{Cause}$ can be expressed as a disjoint union of all events
$(\neg\mathsf{Cause})\,\mathrm{U}\,c$ where $c\in\mathsf{Cause}$. Therefore,
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}$, which
yields:

######  Lemma 5.

Every SPR cause for $\mathsf{Eff}$ is a GPR cause for $\mathsf{Eff}$.

######  Proof 3.1.

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\\}\quad\text{and}\quad
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}$.

[Non-strict GPR cause] Consider the Markov chain $\mathcal{M}$ depicted in
Figure 2 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\text{ 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})$.

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$

Figure 1. A MC allowing for non-strict GPR causes

$\mathsf{init}$$\mathsf{eff}$$1$

Figure 2. A MC in which no PR cause exists

[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 MC in Figure 2
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) forbids $\\{\mathsf{init}\\}$ to be a PR cause. The same
phenomenon occurs if all non-terminal states of a MC 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 6 (Memory needed for refuting PR condition).

Let $\mathcal{M}$ be the MDP in Figure 4, where the notation is similar to
Example 3.1 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 finite-memory 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 3. MDP $\mathcal{M}$ from Remark 6

$\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 4. MDP $\mathcal{M}$ from Remark 7

######  Remark 7 (Randomization needed for refuting PR condition).

Consider the MDP $\mathcal{M}$ in Figure 4. Let
$\mathsf{Eff}=\\{\mathsf{eff}_{\mathsf{unc}},\mathsf{eff}_{\mathsf{cov}}\\}$
and $\mathsf{Cause}=\\{c\\}$. Here the state $\mathsf{eff}_{\mathsf{unc}}$ is
not covered by the cause whereas $\mathsf{eff}_{\mathsf{cov}}$ is, hence their
names. The two MD-schedulers $\mathfrak{S}_{\alpha}$ and
$\mathfrak{S}_{\beta}$ which 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 PR
conditions. On the other hand $\mathfrak{S}_{\beta}$ satisfies (SPR) and (GPR)
since

$\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}$ also reaches $c$ with positive
probability but 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 8 (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 9 (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 copy of the
state $s$ in $\mathcal{M}_{0}$ constitutes an SPR cause for both copies of the
effect 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. Here, 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}$.

$\mathsf{init}$$s_{2}$$s_{1}$$\mathsf{eff}$$\mathsf{noeff}$$\beta$$1/100$$99/100$$\gamma$$\delta$$1/4$$3/4$$\alpha$

Figure 5. MDP $\mathcal{M}$ from Remark 9

$\mathsf{init}$$\mathsf{init}_{0}$$s_{0,2}$$s_{0,1}$$\mathsf{eff}_{0}$$\mathsf{noeff}_{0}$$1/2$$\beta$$1/100$$99/100$$\delta$$1/4$$3/4$$\alpha$$\mathsf{init}_{1}$$s_{1,2}$$s_{1,1}$$\mathsf{eff}_{1}$$\mathsf{noeff}_{1}$$1/2$$\beta$$1/100$$99/100$$\gamma$$1/4$$3/4$$\alpha$

Figure 6. $\mathcal{N}$ with the two copies $\mathcal{M}_{0}$ and
$\mathcal{M}_{1}$

To demonstrate this consider the MDP $\mathcal{M}$ from Figure 6. We are
interested in reaching the effect state $\mathsf{eff}$. For the action
$\delta$ in state $s_{1}$ the corresponding construction is depicted in Figure
6. The state $s_{1,0}$ as the copy of $s_{1}$ in $\mathcal{M}_{0}$ satisfies
(SPR), since for any scheduler $\mathfrak{S}$ reaching $s_{1,0}$ we have

$\mathrm{Pr}_{\mathcal{N},s_{1,0}}^{\mathfrak{S}}(\lozenge\\{\mathsf{eff}_{0},\mathsf{eff}_{1}\\})=1/4>107/800\geq\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{N}}(\lozenge\\{\mathsf{eff}_{0},\mathsf{eff}_{1}\\})$,

which means that the action $\delta$ does indeed raise the probability of
$\mathsf{eff}$ in $\mathcal{M}$. $\lhd$

##  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}$. Since the minimality condition (for
all
$c\in\mathsf{Cause}:\mathrm{Pr}^{\max}_{\mathcal{M}}(\neg\mathsf{Cause}\,\mathrm{U}\,c)>0$)
of PR causes is verifiable by standard model checking techniques in polynomial
time, we concentrate on checking the probability-raising conditions (S) and
(G). 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).

We start by stating that for (S) and (G), it suffices to consider schedulers
minimizing the probability to reach an effect state from every cause state.
For this we transform the MDP in question according to the cause candidate in
question.

[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. $\lhd$

######  Lemma 10.

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

Obviously, for all
$c\in\mathsf{Cause}:\mathrm{Pr}^{\max}_{\mathcal{M}}(\neg\mathsf{Cause}\,\mathrm{U}\,c)>0$
holds for $\mathsf{Cause}$ in $\mathcal{M}$ if and only if it holds for
$\mathsf{Cause}$ in $\mathcal{M}_{[\mathsf{Cause}]}$. Furthermore, it is clear
all SPR resp. GPR causes of $\mathcal{M}$ are also SPR resp. GPR causes in
$\mathcal{M}_{[\mathsf{Cause}]}$. So, it remains to prove the converse
direction. This will be done in Lemma 11 for SPR causes and in Lemma 12 for
GPR causes.

######  Lemma 11 (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 4.1.

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:

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

The task is to prove that (S) 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 (S) holds for $c$ and $\mathfrak{S}$ if and only if

$\displaystyle\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})$ (3)

Using

$\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 (3) 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})$
(4)

The remaining task is now to derive (4) from (2). Applying (2) 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, (4) holds for $c$ and $\mathfrak{S}$.

######  Lemma 12 (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 4.2.

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 (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}}\text{ 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}}<\\!\\!\\!\\!\\!\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})<\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}}.$ (5)

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 (5) holds for $\mathfrak{S}_{\mathfrak{T}}$ then (5) holds
for $\mathfrak{S}$. As (5) holds for $\mathfrak{S}_{\mathfrak{T}}$ by
assumption, this completes the proof.

###  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 (S) for a given cause candidate is the following polynomial time
algorithm to check whether (S) holds in a given state $c$ of $\mathcal{M}$ for
all schedulers $\mathfrak{S}$ with
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond c)>0$:

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

  1. 0.

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

  2. 1.

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

  3. 2.

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

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

######  Lemma 13.

Algorithm 4.1 is sound and runs in polynomial time.

######  Proof 4.3.

First, we show the soundness of Algorithm 4.1. By the virtue of Lemma 10 it
suffices to show that Algorithm 4.1 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.1 correctly answers “no” (case 2 or 3.1) if $w_{c}=0$. 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$.

  1. 1.

of Algorithm 4.1 (i.e., if $q<w_{c}$), the answer “yes” is sound as then
$\mathrm{Pr}^{\max}_{\mathcal{N}}(\Diamond\mathsf{Eff})=q<w_{c}$.

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

  3. 3.1

Pick an MD-scheduler $\mathfrak{S}$ of $\mathcal{M}^{\max}_{[c]}$ such that
$c$ is reachable from $\mathsf{init}$ via $\mathfrak{S}$ 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}$.

  4. 3.2

We have 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.1 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.

By applying Algorithm 4.1 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 14 (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 15 (Memory requirements for (S)).

As the soundness proof for Algorithm 4.1 shows: If $\mathsf{Cause}$ does not
satisfy (S), 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). $\lhd$

######  Lemma 16 (Criterion for the existence of PR causes).

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

  1. (a)

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

  2. (b)

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

  3. (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}$.

Thus, the existence of SPR and GPR causes can be checked with Algorithm 4.1 in
polynomial time.

######  Proof 4.4.

Obviously, statement (c) implies statements (a) and (b). The implication “(a)
$\Longrightarrow$ (b)” follows from Lemma 5. 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 10 it is now easy to see that
$\\{c_{0}\\}$ is both an SPR and a GPR cause for $\mathsf{Eff}$.

###  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 global probability-
raising cause for $\mathsf{Eff}$ in $\mathcal{M}$. As the minimality condition
(for all
$c\in\mathsf{Cause}:\mathrm{Pr}^{\max}_{\mathcal{M}}(\neg\mathsf{Cause}\,\mathrm{U}\,c)>0)$
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 17.

Given $\mathcal{M}$, $\mathsf{Cause}$ and $\mathsf{Eff}$, deciding whether
$\mathsf{Cause}$ is a GPR cause for $\mathsf{Eff}$ in $\mathcal{M}$ can be
done in $\mathrm{coNP}$.

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.

######  Theorem 18.

Let $\mathcal{M}$ be an MDP with effect set $\mathsf{Eff}$ as before and
$\mathsf{Cause}$ a set of non-effect states which satisfies for all
$c\in\mathsf{Cause}:\mathrm{Pr}^{\max}_{\mathcal{M}}(\neg\mathsf{Cause}\,\mathrm{U}\,c)>0$.
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 17 and
Theorem 18. We suppose that $\mathsf{Cause}$ satisfies for all
$c\in\mathsf{Cause}:\mathrm{Pr}^{\max}_{\mathcal{M}}(\neg\mathsf{Cause}\,\mathrm{U}\,c)>0$.

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

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

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.

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

##### Establishing 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 10,
we may suppose that $\mathcal{M}=\mathcal{M}_{[\mathsf{Cause}]}$ (see Notation
4) without changing the satisfaction of (G). 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 [dA97],
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.

In particular, consider the MEC-quotient $\mathcal{N}$ of
$\mathcal{M}_{[\mathsf{Cause}]}$ (see Definition 2.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.3.

######  Lemma 19.

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

By Lemma 3, 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 19 and Lemma 10, we conclude the following corollary that justifies
working under assumptions (A1)-(A3).

######  Corollary 20.

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

######  Proof 4.6.

By Lemma 19, 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 10, $\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}$.

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), (G) can be reformulated as follows:

######  Lemma 21.

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

$\displaystyle\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 (G) in terms of a quadratic constraint
system over variables for the expected frequencies of state-action pairs. 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}$}$ (S1) $\displaystyle x_{\mathsf{init}}$
$\displaystyle\ =\
1+\\!\\!\\!\\!\\!\sum_{(t,\alpha)\in\mathit{StAct}}\\!\\!\\!\\!\\!x_{t,\alpha}\cdot
P(t,\alpha,\mathsf{init})$ (S2) $\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}\\}$}$ (S3)

Using well-known results for MDPs without ECs (see, e.g., [Kal20, Theorem
9.16]), given a vector $x\in\mathbb{R}^{\mathit{StAct}}$, then $x$ is a
solution to (S1) and the balance equations (S2) and (S3) 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 21 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 0\ \ \geqslant\ \
\bigl{(}1-x_{\mathsf{Cause}}\bigl{)}\cdot\\!\\!\\!\\!\sum_{c\in\mathsf{Cause}}\\!\\!\\!\\!\\!\\!x_{c}\cdot
w_{c}\ -\ x_{\mathsf{Cause}}\cdot x_{\mathsf{eff}_{\mathsf{unc}}}$ (S4)

Finally, we can reformulate the condition
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{Cause})>0$ by
frequency variables:

$\displaystyle x_{\mathsf{Cause}}>0$ (S5)

######  Lemma 22.

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 (S1)-(S5) has a solution.

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

######  Proof 4.7 (Proof of Theorem 17).

The quadratic system of inequalities can be constructed from $\mathcal{M}$,
$\mathsf{Cause}$, and $\mathsf{Eff}$ in polynomial time. Except for the strict
inequality constraint in (S5), it has the form of a quadratic program, for
which the threshold problem can be decided in $\mathrm{NP}$ by [Vav90]. We
will prove that also with this strict inequality, it can be checked in
$\mathrm{NP}$ whether the system (S1)-(S5) has a solution. As the system of
inequalities is expressing the violation of (GPR), deciding whether a set
$\mathsf{Cause}$ is a GPR cause can then be done in $\mathrm{coNP}$.

To show that satisfiability of the system (S1)-(S5) is in $\mathrm{NP}$, we
will provide a non-deterministic algorithm that runs in polynomial time and
finds a solution if one exists. Some of the arguments are similar to the
arguments used in [Vav90]. Additionally, we will rely on the implicit function
theorem.

We begin by proving what a solution to (S1)-(S5) can be assumed to look like.
Thus assume that a solution to (S1)-(S5) exists. There are two possible cases:

Case 1:

All solutions to (S1)-(S3) and (S5) satisfy (S4). Then, in particular, the
frequency values of an MD-scheduler maximizing the probability to reach Cause
are a solution to (S1)-(S3) and (S5) and hence to (S4) in this case.

Case 2:

There are solutions to (S1)-(S3) and (S5) that violate (S4). The space of
feasible points for conditions (S1)-(S3) and (S5) is connected. Furthermore,
the right hand side of (S4)

$\bigl{(}1-x_{\mathsf{Cause}}\bigl{)}\cdot\\!\\!\\!\\!\sum_{c\in\mathsf{Cause}}\\!\\!\\!\\!\\!\\!x_{c}\cdot
w_{c}\ -\ x_{\mathsf{Cause}}\cdot x_{\mathsf{eff}_{\mathsf{unc}}}$

is continuous. Hence, as there are also solutions to (S1)-(S3) and (S5) that
satisfy (S4) by assumption, there is a solution to (S1)-(S3) and (S5) that
satisfies

$\bigl{(}1-x_{\mathsf{Cause}}\bigl{)}\cdot\\!\\!\\!\\!\sum_{c\in\mathsf{Cause}}\\!\\!\\!\\!\\!\\!x_{c}\cdot
w_{c}\ -\ x_{\mathsf{Cause}}\cdot x_{\mathsf{eff}_{\mathsf{unc}}}=0.$

Now, let us take a closer look at Case 2: First of all, we add the equation

$x_{\mathsf{Cause}}=\sum_{c\in\mathsf{Cause}}x_{c}$

to our system. Thus, the variables are $x_{\mathsf{Cause}}$ and $x_{s,\alpha}$
for each $(s,\alpha)\in\mathit{StAct}$. Obviously, this does not influence the
satisfiability. Equation (S4’) now contains the new variable
$x_{\mathsf{Cause}}$, which is not an abbreviation anymore. We write $x$ for
the vector of variables $x_{s,\alpha}$ with $(s,\alpha)\in\mathit{StAct}$.

In Case 2, there is a solution $(x^{\ast},x_{\mathsf{Cause}}^{\ast})$ such
that the maximal possible number of variables is $0$ and such that
$x_{\mathsf{Cause}}^{\ast}$ is maximal among all such solutions. Let
$X^{\prime}$ be the set of variables that are $0$ in
$(x^{\ast},x_{\mathsf{Cause}}^{\ast})$. We remove all variables from
$X^{\prime}$ from all constraints by setting them to $0$ and call the
resulting system (T1)-(T6) where (T4) is obtained from (S4’), while all other
equations (T$i$) are obtained from (S$i$), by removing the chosen variables.
We then collect the remaining variables in the vector
$v=(y,y_{\mathsf{Cause}})$. Let $(y^{\ast},y_{\mathsf{Cause}}^{\ast})$ be the
solution $(x^{\ast},x_{\mathsf{Cause}}^{\ast})$ after the variables in
$X^{\prime}$ have been removed. Thus, all values in this vector are positive.

Define the function $f$ as the right hand side of (T4):

$f(y,y_{\mathsf{Cause}})=\bigl{(}1-y_{\mathsf{Cause}}\bigl{)}\cdot\\!\\!\\!\\!\sum_{c\in\mathsf{Cause}}\\!\\!\\!\\!\\!\\!y_{c}\cdot
w_{c}\ -\ y_{\mathsf{Cause}}\cdot y_{\mathsf{eff}_{\mathsf{unc}}},$

where the variables $y$ are as the original variables $x$ after the variables
in $X^{\prime}$ have been removed. Now, we apply the implicit function
theorem: Observe that

$\frac{\partial f(y,y_{\mathsf{Cause}})}{\partial
y_{\mathsf{Cause}}}=-\sum_{c\in\mathsf{Cause}}y_{c}\cdot
w_{c}-y_{\mathsf{eff}_{\mathsf{unc}}}.$

Evaluated at $(y^{\ast},y_{\mathsf{Cause}}^{\ast})$, this value is non-zero as
all summands are negative and there are at least some of the variables in the
abbreviation $y_{c}$ with $c\in\mathsf{Cause}$ left, i.e., not removed because
they were not $0$ due to the original constraint (S5). So, we can apply the
implicit function theorem, which guarantees us the existence of a function
$g(y)$, such that $g(y^{\ast})=y_{\mathsf{Cause}}^{\ast}$ and, for all
$y^{\prime}$ in an open ball $B_{1}$ around $y^{\ast}$, we have

$f(y^{\prime},g(y^{\prime}))=0.$

By the implicit function theorem, we can explicitly compute the gradient

$\nabla g=\left(\frac{\partial g(y)}{\partial{y_{1}}},\dots,\frac{\partial
g(y)}{\partial{y_{k}}}\right)=-\left(\frac{\partial
f(y,y_{\mathsf{Cause}})}{\partial
y_{\mathsf{Cause}}}\right)^{-1}\cdot\left(\frac{\partial
f(y,y_{\mathsf{Cause}})}{\partial{y_{1}}},\dots,\frac{\partial
f(y,y_{\mathsf{Cause}})}{\partial{y_{k}}}\right)$

of the derivatives on $B_{1}$ for the appropriate $k$ from the derivatives of
$f$. Note that on $B_{1}$, the gradient $\nabla g$ is $0$ iff

$H(y,y_{\mathsf{Cause}})\stackrel{{\scriptstyle\text{\rm\tiny
def}}}{{=}}\left(\frac{\partial
f(y,y_{\mathsf{Cause}})}{\partial{y_{1}}},\dots,\frac{\partial
f(y,y_{\mathsf{Cause}})}{\partial{y_{k}}}\right)$

is $0$. Furthermore, all entries of $H(y,y_{\mathsf{Cause}})$ are linear in
the variables $v$ as the function $f$ is quadratic. As the function $g$ has a
local maximum in $y^{\ast}$, we know that $\nabla g$ evaluated at $y^{\ast}$
is $0$.

Equations (T2), (T3), and (T6) are linear equations in the remaining variables
$v$. We can rewrite these three equations with a matrix $M$ and a vector $b$
whose entries can easily be expressed in terms of the coefficients of the
original system (again, after the set of variables $X^{\prime}$ has been
removed) as

$Mv=b.$

The solutions to this equation form an $r$-dimensional affine space $W$. It
can be written as

$W=\\{\underbrace{c_{0}+c_{1}\cdot z_{1}+\dots+c_{r}\cdot
z_{r}}_{\stackrel{{\scriptstyle\text{\rm\tiny
def}}}{{=}}h(z_{1},\dots,z_{r})}\mid(z_{1},\dots,z_{r})\in\mathbb{R}^{r}\\}$

for some vectors $c_{0},c_{1},\dots,c_{r}$ which can be computed from $M$ and
$b$ in polynomial time.

Let $B_{2}$ be an open ball in $\mathbb{R}^{r}$ such that $h(B_{2})\subseteq
B_{1}$ and such that $h(B_{2})$ contains
$(y^{\ast},y_{\mathsf{Cause}}^{\ast})$. We claim that $g\circ h\colon
B_{2}\to\mathbb{R}$ has an isolated local maximum at
$z^{\ast}\stackrel{{\scriptstyle\text{\rm\tiny
def}}}{{=}}h^{-1}(y^{\ast},y_{\mathsf{Cause}}^{\ast})$. It is clear that
$g\circ h$ has local maximum since $g$ has a local maximum at
$(y^{\ast},y_{\mathsf{Cause}}^{\ast})$. Suppose now, that $g\circ h$ does not
have an isolated local maximum at
$h^{-1}(y^{\ast},y_{\mathsf{Cause}}^{\ast})$. As $h$ is an affine map and the
graph of $g$ is the solution to a quadratic equation, this is only possible if
there is a direction $d\in\mathbb{R}^{r}\setminus\\{0\\}$ such that

$\displaystyle g\circ h(z^{\ast})=g\circ h(z^{\ast}+t\cdot d)$ (6)

for all $t\in\mathbb{R}$. Due to the boundedness of the polyhedron described
by conditions (T1)-(T3), (T5), and (T6) and since $z^{\ast}$ lies in the
interior of this polyhedron, this means that there must be a value
$q\in\mathbb{R}$ such that $(h(z^{\ast}+q\cdot d),g\circ h(z^{\ast}+q\cdot
d))$ provides a solution $v$ to equations (T1)-(T3), (T5), and (T6) with an
additional $0$. By the definition of $g$, this solution furthermore satisfies
(T4) and, by equation (6), it still satisfies (T5). This contradicts the
choice of the original solution $(x^{\ast},x_{\mathsf{Cause}}^{\ast})$.

So, $g\circ h\colon B_{2}\to\mathbb{R}$ has an isolated local maximum at
$z^{\ast}$. This implies that on an open ball around $z^{\ast}$, the point
$z^{\ast}$ is the only solution to

$\nabla g(h(z))=0$

and consequently, the only solution to

$H(h(z))=0.$

Since $H(h(z))$ is a vector of linear expressions in $z$, this implies that
$z^{\ast}$ is the only solution on $\mathbb{R}^{r}$ to $H(h(z))=0$. This is
the key result that we need to provide a non-deterministic polynomial-time
algorithm to check the satisfiability of the original constraint system.

Let us now describe the algorithm: The algorithm begins by computing the
frequency values of an MD-scheduler as in Case 1 in polynomial time and checks
whether the resulting vector of frequency values satisfies (S1)-(S5). If this
is the case, the algorithm returns that the system is satisfiable.

If this is not the case, the algorithm tries to compute a solution to
(S1)-(S3), (S5), and (S4’) as in Case 2. The algorithm non-deterministically
guesses a subset of the variables and removes them from all constraints by
replacing them with $0$.

We will now suppose that the algorithm guesses the set $X^{\prime}$ as above
and show that in this case, it indeed computes a solution. After the variables
from $X^{\prime}$ have been removed, $H(y,y_{\mathsf{Cause}})$ can be computed
in polynomial time as all the derivatives of $f$ are simple linear expressions
in the variables which only require basic arithmetic and can be computed in
polynomial time. Likewise, $M$ and $b$ can be computed easily in polynomial
time from the original constraints after the guessed variables have been
removed. The vectors $c_{0},c_{1},\dots,c_{r}$ describing the solution space
to $Mv=b$ can then also be computed in polynomial time.

Thus, also the vector $H(h(z))$ of linear expressions in the variables $z$ can
be computed in polynomial time. The equation system $H(h(z))=0$ has a unique
solution if the guessed variables were indeed $X^{\prime}$. In this case, the
solution $z^{\ast}$ can be computed in polynomial time as well. If the guess
of variables was not $X^{\prime}$, then either there is no unique solution to
this equation system which can be detected in polynomial time, or the
solution, which is computed in the sequel in polynomial time, might not
satisfy the original constraints, which is checked in the end.

From $z^{\ast}$, we can compute $y^{\ast}=h(z^{\ast})$ using the vectors
$c_{0},c_{1},\dots,c_{r}$. The solution $x^{\ast}$ is then obtained by
plugging in $0$s for the removed variables. Checking whether the resulting
vector satisfies all constraints can also be done in polynomial time in the
end. If $X^{\prime}$ was guessed correctly, this vector $x^{\ast}$ indeed
forms a solution to the original constraints as we have seen.

In summary, the algorithm needs non-determinism to guess the set $X^{\prime}$
of variables which are $0$ in a solution to the original constraints with the
maximal number of zeroes. All other steps are deterministic polynomial-time
computations. Thus, the satisfiability of (S1)-(S5) can be checked in
$\mathrm{NP}$.

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

######  Corollary 23.

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
(GPR).

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

######  Lemma 24.

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 satisfies
$\mathrm{Pr}^{\mathfrak{T}}_{\mathcal{M}}(\Diamond\mathsf{Cause})>0$ and
violates (GPR) is computable in polynomial time.

######  Proof 4.8.

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. We regard the set $U$
of states $u$ which 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 (GPR) (or equivalently condition (GPR-1) from Lemma
21)

  * •

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

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

$\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
(GPR). For this, we suppose by contraction that this is not the case, which
means that (GPR) 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, $p_{x},p_{x,c},q_{x},v_{x}$ differ from
$p_{y},p_{y,c},q_{y},v_{y}$ only by the factor $\frac{x}{y}$. That is:

$p_{x}=p_{y}\frac{x}{y}$, $p_{x,c}=p_{y,c}\frac{x}{y}$,
$q_{x}=q_{y}\frac{x}{y}$ and $v_{x}=v_{y}\frac{x}{y}$.

Thus, $f(x)$ has the following form:

$\displaystyle f(x)$ $\displaystyle=$
$\displaystyle(p_{x}{+}p)(q_{x}{+}q)-\bigl{(}1{-}(p_{x}{+}p)\bigr{)}(v_{x}{+}v)$
$\displaystyle=$
$\displaystyle\underbrace{p_{x}q_{x}{+}p_{x}v_{x}}_{\mathfrak{a}x^{2}}+\underbrace{p_{x}(q+v)+q_{x}p-v_{x}}_{\mathfrak{b}x}+\underbrace{pq-v+pv}_{\mathfrak{c}}$
$\displaystyle=$ $\displaystyle\mathfrak{a}x^{2}+\mathfrak{b}x+\mathfrak{c}$

For the value $\mathfrak{a}$, we have
$\mathfrak{a}x^{2}=p_{x}q_{x}{+}p_{x}v_{x}$ and hence
$\mathfrak{a}=\frac{1}{y^{2}}(p_{y}q_{y}+p_{y}v_{y})>0$. But then the second
derivative $f^{\prime\prime}(x)=2\mathfrak{a}$ of $f$ is positive, which
yields that $f$ has a global minimum at some point $x_{0}$ and is strictly
decreasing for $x<x_{0}$ and strictly increasing for $x>x_{0}$. As $f(0)$ and
$f(1)$ are both negative, we obtain $f(x)<0$ for all $x$ in the interval
$[0,1]$. But this contradicts $f(y)\geqslant 0$.

This yields that at least one of the schedulers $\mathfrak{V}_{0}$ or
$\mathfrak{V}_{1}$ witnesses the violation of (GPR). Thus, we can define
$\mathfrak{T}_{i}\in\\{\mathfrak{V}_{0},\mathfrak{V}_{1}\\}$ accordingly.

The number of states $k$ in $U$ is bounded by the number of states in $S$. In
each iteration of the above construction, the function value $f(0)$ is
sufficient to determine one of the schedulers $\mathfrak{V}_{0}$ and
$\mathfrak{V}_{1}$ witnessing the violation of (GPR). So, the procedure has to
compute the values in condition (GPR-1) for $k$-many MR-schedulers and update
the scheduler afterwards. As the update can easily be carried out in
polynomial time, the run-time of all $k$ iterations is polynomial as well.

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.

######  Theorem 25.

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

Let $\mathfrak{S}$ be an MR-scheduler for $\mathit{MEC}(\mathcal{M})$ with
$\mathfrak{S}(s_{\mathcal{E}})(\tau)\in\\{0,1\\}$ for each MEC $\mathcal{E}$
of $\mathcal{M}$. We consider the following extension $\mathcal{M}^{\prime}$
of $\mathcal{M}$: The state space of $\mathcal{M}$ is extended by a new
terminal state $\bot$ and a fresh action $\tau$ is enabled in each state $s$
that belongs to a MEC of $\mathcal{M}$. Action $\tau$ leads to $\bot$ with
probability $1$. All remaining transition probabilities are as in
$\mathcal{M}$. So, $\mathcal{M}^{\prime}$ is obtained from $\mathcal{M}$ by
allowing a transition to a new terminal state $\bot$ from each state that
belongs to a MEC.

Now, we first provide a finite-memory scheduler $\mathfrak{T}$ for
$\mathcal{M}^{\prime}$ that leaves each MEC $\mathcal{E}$ for which
$\mathfrak{S}(s_{\mathcal{E}})(\tau)=0$ via the state action pair $(s,\alpha)$
with probability $\mathfrak{S}(s_{\mathcal{E}})(\alpha)$. Recall that we
assume that each action is enabled in at most one state and that the actions
enabled in the state $s_{\mathcal{E}}$ in $\mathit{MEC}(\mathcal{M})$ are
precisely the actions that are enabled in some state of $\mathcal{E}$ and that
do not belong to $\mathcal{E}$ (Section 2.3)

The scheduler $\mathfrak{T}$ is defined as follows: In all states that do not
belong to a MEC $\mathcal{E}$ of $\mathcal{M}$ with
$\mathfrak{S}(s_{\mathcal{E}})(\tau)=0$, the behavior of $\mathfrak{T}$ is
memoryless: For each state $s$ of $\mathcal{M}$ (and hence of
$\mathcal{M}^{\prime}$) that does not belong to a MEC,
$\mathfrak{T}(s)=\mathfrak{S}(s)$. For each state $s$ in an end component
$\mathcal{E}$ of $\mathcal{M}$ with $\mathfrak{S}(s_{\mathcal{E}})(\tau)=1$,
we define $\mathfrak{T}(s)(\tau)=1$. If a MEC $\mathcal{E}$ of $\mathcal{M}$
with $\mathfrak{S}(s_{\mathcal{E}})(\tau)=0$ is entered, $\mathfrak{T}$ makes
use of finitely many memory modes as follows: Enumerate the state action pairs
$(s,\alpha)$ where $s$ belongs to $\mathcal{E}$, but $\alpha$ does not belong
to $\mathcal{E}$, and for which $\mathfrak{S}(s_{\mathcal{E}})(\alpha)>0$ by
$(s_{1},\alpha_{1})$, …, $(s_{k},\alpha_{k})$ for some natural number $k$.
Further, let $p_{i}\stackrel{{\scriptstyle\text{\rm\tiny
def}}}{{=}}\mathfrak{S}(s_{\mathcal{E}})(\alpha_{i})>0$ for all $1\leq i\leq
k$. By assumption $\sum_{1\leq i\leq k}p_{i}=1$.

When entering $\mathcal{E}$, the scheduler works in $k$ memory modes $1$, …,
$k$ until an action $\alpha$ that does not belong to $\mathcal{E}$ is
scheduled starting in memory mode $1$. In each memory mode $i$, $\mathfrak{T}$
follows an MD-scheduler for $\mathcal{E}$ that reaches $s_{i}$ with
probability $1$ from all states of $\mathcal{E}$. Once, $s_{i}$ is reached,
$\mathfrak{T}$ chooses action $\alpha_{i}$ with probability

$q_{i}\stackrel{{\scriptstyle\text{\rm\tiny
def}}}{{=}}\frac{p_{i}}{1-\sum_{j<i}p_{j}}.$

Note that this means that $\mathfrak{T}$ leaves $\mathcal{E}$ via
$(s_{k},\alpha_{k})$ with probability $1$ if it reaches the last memory mode
$k$. As $\mathfrak{T}$ behaves in a memoryless deterministic way in each
memory mode, it leaves the end component $\mathcal{E}$ after finitely many
steps in expectation. Furthermore, for each $i\leq k$, it leaves $\mathcal{E}$
via $(s_{i},\alpha_{i})$ precisely with probability $(1-\sum_{j<i}p_{j})\cdot
q_{i}=p_{i}$. As the behavior of $\mathfrak{S}$ in $\mathit{MEC}(\mathcal{M})$
is hence mimicked by $\mathfrak{T}$ in $\mathcal{M}^{\prime}$, we conclude
that the expected frequency of all actions of $\mathcal{M}$ that do not belong
to an end component is the same in $\mathcal{M}^{\prime}$ under $\mathfrak{T}$
and in $\mathit{MEC}(\mathcal{M})$ under $\mathfrak{S}$.

As each end component of $\mathcal{M}^{\prime}$ is either left directly via
$\tau$ under $\mathfrak{T}$ or after finitely many steps in expectation as
just described, the expected frequency of each state-action pair of
$\mathcal{M}^{\prime}$ under $\mathfrak{T}$ is finite. In the terminology of
[Kal20], the scheduler $\mathfrak{T}$ is _transient_. By [Kal20, Theorem
9.16], this implies that there is a MR-scheduler $\mathfrak{U}$ for
$\mathcal{M}^{\prime}$ under which the expected frequency of all state-action
pairs is the same as under $\mathfrak{T}$. So, for this scheduler
$\mathfrak{U}$, the expected frequency in $\mathcal{M}^{\prime}$ of all
actions $\alpha$ of $\mathcal{M}$ that do not belong to an end component is
the same as under $\mathfrak{S}$ in $\mathit{MEC}(\mathcal{M})$.

Finally, we modify $\mathfrak{U}$ such that it becomes a scheduler for
$\mathcal{M}$: For each end component $\mathcal{E}$ of $\mathcal{M}$ with
$\mathfrak{S}(s_{\mathcal{E}})(\tau)=1$, we fix a memoryless scheduler
$\mathfrak{U}_{\mathcal{E}}$ that does not leave the end component. Now,
whenever a state $s$ in such an end component is visited, the modified
scheduler switches to the behavior of $\mathfrak{U}_{\mathcal{E}}$ instead of
choosing action $\tau$ with probability $1$. Clearly, this does not affect the
expected frequency of actions of $\mathcal{M}$ that do not belong to an end
component and hence the modified scheduler is as claimed in the theorem.

######  Remark 26.

The proof of Theorem 25 above provides an algorithm how to obtain the
scheduler $\mathfrak{T}$ from $\mathfrak{S}$. The number of memory modes of
the intermediately constructed finite-memory scheduler is bounded by the
number of state-action pairs of $\mathcal{M}$. Further, in each memory mode
during the traversal of a MEC, the scheduler behaves in a memoryless
deterministic way. Hence, the induced Markov chain is of size polynomial in
the size of the MDP $\mathcal{M}$ and the representation of the scheduler
$\mathfrak{S}$. Therefore, also the expected frequencies of all state-action
pairs under the intermediate finite-memory scheduler and hence under
$\mathfrak{T}$ can be computed in time polynomial in the size of the MDP
$\mathcal{M}$ and the representation of the scheduler $\mathfrak{S}$. So, also
the scheduler $\mathfrak{T}$ itself which can be derived from these expected
frequencies can be computed in polynomial time from $\mathfrak{S}$.

Together with Lemma 24, this means that $\mathfrak{T}$ and hence the scheduler
with two memory modes whose existence is stated in Theorem 18 can be computed
from a solution to the constraint system (S1)-(S5) from Section 4.2 in time
polynomial in the size of the original MDP and the size of the representation
of the solution to (S1)-(S5). $\lhd$

With these results we can now proof the second main result of this section,
Theorem 18.

######  Proof 4.10 (Proof of Theorem 18).

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 23 and Theorem 25, 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 15, $\mathfrak{S}$ can be extended to a
finite-memory randomized scheduler $\mathfrak{T}$ for $\mathcal{M}$ with two
memory cells.

######  Remark 27 (On lower bounds on GPR checking).

Solving systems of quadratic inequalities with linear side constraints is NP-
hard in general (see, e.g., [GJ79]). 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
[KTK80]. Unfortunately, the quadratic constraint system given by (S1)-(S5) 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 (S1)-(S3), i.e., by the structure of the MDP, the
inequality (S4) takes the form:

$\displaystyle x_{c}\cdot w_{c}-x_{c}^{2}\cdot(w_{c}+y)\leq 0$ (7)

Here, the $1\times 1$-matrix $({-}w_{c}{-}y)$ has a negative eigenvalue.
Although it is not ruled out that (S1)-(S5) belongs to another class of
efficiently solvable constraint systems, the NP-hardness result in [PV91] for
the solvability of quadratic inequalities of the form (7) 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.
[Pow11]). 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.

In this section, we assume as before an MDP
$\mathcal{M}=(S,\mathit{Act},P,\mathsf{init})$ and $\mathsf{Eff}\subseteq S$
are given where all effect states are terminal. Furthermore, we suppose all
states $s\in S$ are reachable from $\mathsf{init}$.

###  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, false
positives, true negatives and false negatives is as described in the confusion
matrix in Figure 7. The formal definition is

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

Path hits | $\mathsf{Eff}$ | $\neg\mathsf{Eff}$
---|---|---
$\mathsf{Cause}$ | True positive (tp) | False positive (fp)
|  $\mathsf{Cause}$ correctly predicted $\mathsf{Eff}$ |  $\mathsf{Cause}$ falsely predicted $\mathsf{Eff}$
$\neg\mathsf{Cause}$ | False negative (fn) | True negative (tn)
|  $\mathsf{Cause}$ falsely not predicted $\mathsf{Eff}$ |  $\mathsf{Cause}$ correctly not predicted $\mathsf{Eff}$
Figure 7. Confusion matrix for $\mathsf{Cause}$ as a binary classifier for
$\mathsf{Eff}$

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}$ are defined as follows:

$\begin{array}[]{rclcl}\operatorname{\mathit{precision}}^{\mathfrak{S}}(\mathsf{Cause})&\
=&\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\ \Diamond\mathsf{Eff}\ |\
\Diamond\mathsf{Cause}\
)&=&\frac{\displaystyle\mathsf{tp}^{\mathfrak{S}}}{\displaystyle\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{\displaystyle\mathsf{tp}^{\mathfrak{S}}}{\displaystyle\mathsf{tp}^{\mathfrak{S}}+\mathsf{fn}^{\mathfrak{S}}}\\\\[4.30554pt]
\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\lozenge\mathsf{Cause})\wedge\lozenge\mathsf{Eff}\bigr{)}}&=&\frac{\displaystyle\mathsf{tp}^{\mathfrak{S}}}{\displaystyle\mathsf{fn}^{\mathfrak{S}}}.\end{array}$

Note that for these definitions we make some respective assumptions on the
scheduler. We assume

  * •

$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{Cause})>0$ for
$\operatorname{\mathit{precision}}^{\mathfrak{S}}(\mathsf{Cause})$,

  * •

$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{Eff})>0$ for
$\operatorname{\mathit{recall}}^{\mathfrak{S}}(\mathsf{Cause})$ and

  * •

$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}\bigl{(}(\neg\lozenge\mathsf{Cause})\wedge\lozenge\mathsf{Eff}\bigr{)}>0$)
for $\mathit{covrat}^{\mathfrak{S}}(\mathsf{Cause})$.

If we have
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}\bigl{(}(\neg\lozenge\mathsf{Cause})\wedge\lozenge\mathsf{Eff}\bigr{)}=0$
and $\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{Cause})>0$ for
some scheduler $\mathfrak{S}$, we define
$\mathit{covrat}^{\mathfrak{S}}(\mathsf{Cause})=+\infty$. This makes sense
since we can converge to such a scheduler $\mathfrak{S}$ with a sequence of
schedulers $\mathfrak{S}_{0}\ldots$ for which
$\mathrm{Pr}^{\mathfrak{S}_{i}}_{\mathcal{M}}\bigl{(}(\neg\lozenge\mathsf{Cause})\wedge\lozenge\mathsf{Eff}\bigr{)}>0$
and $\mathrm{Pr}^{\mathfrak{S}_{i}}_{\mathcal{M}}(\Diamond\mathsf{Cause})>0$
for $i\in\mathbb{N}$. The coverage ratio of such a sequence converges to
$+\infty$.

Finally, the f-score of $\mathsf{Cause}$ _under a scheduler_ $\mathfrak{S}$ is
defined as the harmonic mean of the precision and recall. Here we assume
$\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{Cause})>0$, which
implies $\mathrm{Pr}^{\mathfrak{S}}_{\mathcal{M}}(\Diamond\mathsf{Eff})>0$:

$\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})}=\frac{2\cdot\mathsf{tp}^{\mathfrak{S}}}{2\cdot\mathsf{tp}^{\mathfrak{S}}+\mathsf{fp}^{\mathfrak{S}}+\mathsf{fn}^{\mathfrak{S}}}$

If, however,
$\mathrm{Pr}_{\mathcal{M}}^{\mathfrak{S}}(\Diamond\mathsf{Eff})>0$ and
$\mathrm{Pr}_{\mathcal{M}}^{\mathfrak{S}}(\Diamond\mathsf{Cause})=0$ for some
$\mathfrak{S}$, define $\mathit{fscore}^{\mathfrak{S}}(\mathsf{Cause})=0$.
This again makes sense as for a sequence of schedulers converging to
$\mathfrak{S}$ the f-score also converges to $0$ (also see Lemma 32).

To lift the definitions of the quality measures under a scheduler to the
quality measure of a cause, we consider the worst-case scheduler: [Quality
measures for causes] Let $\mathsf{Cause}$ be a PR cause. We define

$\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 – 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})$ $\lhd$

Besides the quality measures defined so far, which we will address in detail,
there is a vast landscape of further quality measures for binary classifiers
in the literature (for an overview, see, e.g., [Pow11]). One prominent example
which has been claimed to be superior to the f-score recently [CJ20] is
_Matthews correlation coefficient_ (MCC). In terms of the entries of a
confusion matrix (as in Figure 7), it is defined as

$\text{MCC}=\frac{tp\cdot tn-fp\cdot
fn}{\sqrt{(tp+fp)\cdot(tp+fn)\cdot(tn+fp)\cdot(tn+fn)}}$

In contrast to the f-score (as well as recall and coverage ratio), it makes
use of all four entries of the confusion matrix. In our setting, we could
assign the MCC to a $\mathsf{Cause}$ by again taking the infimum of the value
over all sensible schedulers.

Like the MCC, almost all (cf. [Pow11]) of the quality measures studied in the
literature are algebraic functions (intuitively speaking, build from
polynomials, fractions and root functions) in the entries of the confusion
matrix. At the end of this section, we will comment on the computational
properties of finding good causes when quality is measured by the infimum over
all sensible schedulers of an algebraic function in the entries of the
confusion matrix.

###  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. The first observation is,
that 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.

######  Lemma 28.

If $\mathsf{Cause}$ is an SPR or a GPR cause then:

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

######  Proof 5.1.

“$\leqslant$”: Each scheduler for $\mathcal{M}_{[\mathsf{Cause}]}$ can be
viewed as a scheduler $\mathfrak{S}$ for $\mathcal{M}$ that behaves as an MD-
scheduler minimizing the probability for reaching an effect state from every
state in $\mathsf{Cause}$ and we have:

$\operatorname{\mathit{recall}}_{\mathcal{M}}^{\mathfrak{S}}(\mathsf{Cause})$ |  = | $\operatorname{\mathit{recall}}^{\mathfrak{S}}_{\mathcal{M}_{[\mathsf{Cause}]}}(\mathsf{Cause})$
---|---|---
$\mathit{covrat}_{\mathcal{M}}^{\mathfrak{S}}(\mathsf{Cause})$ | = | $\mathit{covrat}^{\mathfrak{S}}_{\mathcal{M}_{[\mathsf{Cause}]}}(\mathsf{Cause})$
$\operatorname{\mathit{precision}}_{\mathcal{M}}^{\mathfrak{S}}(\mathsf{Cause})$ | = | $\operatorname{\mathit{precision}}^{\mathfrak{S}}_{\mathcal{M}_{[\mathsf{Cause}]}}(\mathsf{Cause})$

and therefore:

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

We obtain
$\operatorname{\mathit{recall}}_{\mathcal{M}}(\mathsf{Cause})\leqslant\operatorname{\mathit{recall}}_{\mathcal{M}_{[\mathsf{Cause}]}}(\mathsf{Cause})$
and the analogous statements for the coverage ratio and the f-score.

“$\geqslant$”: Let $\mathfrak{S}$ be a scheduler of $\mathcal{M}$. Let
$\mathfrak{T}=\mathfrak{T}_{\mathfrak{S}}$ be the scheduler of $\mathcal{M}$
that behaves as $\mathfrak{S}$ until the first visit to a state in
$\mathsf{Cause}$. As soon as $\mathfrak{T}$ has reached $\mathsf{Cause}$, it
behaves as an MD-scheduler minimizing the probability to reach $\mathsf{Eff}$.
Recall and coverage under $\mathfrak{T}$ and $\mathfrak{S}$ have the form:

$\begin{array}[]{rclcrcl}\operatorname{\mathit{recall}}_{\mathcal{M}}^{\mathfrak{S}}(\mathsf{Cause})&\
=&\frac{x}{x+q}&&\mathit{covrat}_{\mathcal{M}}^{\mathfrak{S}}(\mathsf{Cause})&\
=&\frac{x}{q}\\\