¹¹institutetext: Technische Universität Dresden^†^†thanks: This work was funded by DFG grant 389792660 as part of TRR 248, the Cluster of Excellence EXC 2050/1 (CeTI, project ID 390696704, as part of Germany’s Excellence Strategy), DFG-projects BA-1679/11-1 and BA-1679/12-1, and the Research Training Group QuantLA (GRK 1763).
¹¹email: {christel.baier, florian.funke, simon.jantsch,
jakob.piribauer, robin.ziemek}@tu-dresden.de

Probabilistic causes in Markov chains

Christel Baier Florian Funke Simon Jantsch
Jakob Piribauer Robin Ziemek

Abstract

The paper studies a probabilistic notion of causes in Markov chains that relies on the counterfactuality principle and the probability-raising property. This notion is motivated by the use of causes for monitoring purposes where the aim is to detect faulty or undesired behaviours before they actually occur. A cause is a set of finite executions of the system after which the probability of the effect exceeds a given threshold. We introduce multiple types of costs that capture the consump-tion of resources from different perspectives, and study the complexity of computing cost-minimal causes

1 Introduction

The study of cause-effect relationships in formal systems has received considerable attention over the past 25 years. Notions of causality have been proposed within various models, including structural equation models [37, 27, 26], temporal logics in Kripke structures [10, 3] and Markov chains [34, 35], and application areas have been identified in abundance, ranging from finance [32] to medicine [33] to aeronautics [30]. These approaches form an increasingly powerful toolkit aimed at explaining why an observable phenomenon (the effect) has happened, and which previous events (the causes) are logically linked to its occurrence. As such, causality plays a fundamental building block in determining moral responsibility [9, 5] or legal accountability [20], and ultimately fosters user acceptance through an increased level of transparency [36].

Despite the variety of models, application areas, and involved disciplines, all approaches essentially rely on (one of) two central paradigms that dictate how causes are linked to their effects: the counterfactuality principle and the probability-raising property. Counterfactual reasoning prescribes that an effect would not have happened if the cause had not occurred. Probability-raising states that the probability of the effect is higher whenever the cause has been observed.

The contribution of this paper is twofold: First, we define a novel notion of cause for $\omega$ -regular properties in stochastic operational models. Second, we study the complexity of computing optimal causes for cost mechanisms motivated by monitoring applications.

The causes presented in this paper combine the two prevailing causality paradigms mentioned above into a single concept. More specifically, a $p$ -cause for an $\omega$ -regular property $\mathcal{L}$ in a discrete-time Markov chain is a set of finite executions $\pi$ of the system such that the probability that $\mathcal{L}$ occurs after executing $\pi$ is at least $p$ , where $p$ is typically larger than the overall probability of $\mathcal{L}$ . The counterfactuality principle is invoked through the additional requirement that almost every execution exhibiting the event $\mathcal{L}$ contains a finite prefix which is a member of the $p$ -cause. This condition makes our approach amenable to the needs of monitoring a system at runtime.

Imagine a critical event that the system should avoid (e.g., a fully automated drone crashing onto the ground), and assume that a $p$ -cause for this event is known (e.g., physical specifications foreshadowing a crash). Typically, the probability threshold $p$ – which can be thought of as the sensitivity of the monitor – should be lower if the criticality of the event is higher. As the system is running, as soon as the execution seen so far is part of the $p$ -cause, the monitor can trigger an alarm and suitable countermeasures can be taken (e.g., manual control instead of automated behavior). As such, our approach can be preventive in nature.

The monitoring application outlined above suggests computing a $p$ -cause from the model before the system is put to use. However, multiple $p$ -causes may exist for the same property, which raises the question which one to choose. Cyber-physical systems consume time, energy and other resources, which are often subject to budget restrictions. Furthermore, the intended countermeasures may incur different costs depending on the system state. Such costs can be modelled using state weights in the Markov chain, which induce weight functions on the finite executions either in an accumulative (total resource consumption) or instantaneous (current consumption intensity) fashion. On top of this model, we present three cost mechanisms for causes: (1) The expected cost measures the expected resource consumption until the monitor triggers an alarm or reaches a safe state, (2) the partial expected cost measures the expected consumption where executions reaching a safe state do not incur any cost, and (3) the maximal cost measures the maximal consumption that can occur until an alarm is triggered.

	$\operatorname{expcost}$	$\operatorname{pexpcost}$	$\operatorname{maxcost}$
non-negative weights	in $\mathtt{P}$ (7)	pseudo-polyn. (4)	in $\mathtt{P}$ (9)
accumulated		$\mathtt{PP}$ -hard (6)
arbitrary weights	in $\mathtt{P}$ (7)	$\mathtt{PP}$ -hard (6)	pseudo-polyn. (9)
accumulated			in $\mathtt{NP}\cap\mathtt{coNP}$
arbitrary weights	in $\mathtt{P}$ (4.4)	in $\mathtt{P}$ (4.4)	in $\mathtt{P}$ (4.4)
instantaneous

Figure 1: Summary of complexity results for different kinds of cost.

Figure 1 summarizes our results regarding the complexity of computing cost-minimal $p$ -causes for the different combinations of weight type and cost mechanism. To obtain these results we utilize a web of connections to the rich landscape of computational problems for discrete-time Markovian models. More precisely, the results for the expected cost rely on connections to the stochastic shortest path problem (SSP) studied in [4]. The pseudo-polynomial algorithm for partial expected costs on non-negative, accumulated weights uses partial expectations in Markov decision processes [38]. The $\mathtt{PP}$ -hardness result is proved by reduction from the cost problem for acyclic Markov chains stated in [24]. The pseudo-polynomial algorithm for the maximal cost on arbitrary, accumulated weights applies insights from total-payoff games [6, 8].

Full proofs missing in the main document can be found in the appendix.

1.0.1 Related Work.

The structural model approach to actual causality [27] has sparked notions of causality in formal verification [10, 3]. The complexity of computing actual causes has been studied in [16, 17]. A probabilistic extension of this framework has been proposed in [21]. Recent work on checking and inferring actual causes is given in [29], and an application-oriented framework for it is presented in [30]. The work [34] builds a framework for actual causality in Markov chains and applies it to infer causal relationships in data sets. It was later extended to continuous time data [32] and to token causality [35] and has been refined using new measures for the significance of actual and token causes [28, 45].

A logic for probabilistic causal reasoning is given in [44] in combination with logical programming. The work [43] compares this approach to Pearl’s theory of causality involving Bayesian networks [37]. The CP-logic of [44] is close to the representation of causal mechanisms of [14]. The probability-raising principle goes back to Reichenbach [39]. It has been identified as a key ingredient to causality in various philosophical accounts, see e.g. [15].

Monitoring $\omega$ -regular properties in stochastic systems modeled as Hidden Markov Chains (HMCs) was studied in [40, 23] and has recently been revived [18]. The trade-off between accuracy and overhead in runtime verification has been studied in [2, 41, 31]. In particular [2] uses HMCs to estimate how likely each monitor instance is to violate a temporal property. Monitoring the evolution of finite executions has also been investigated in the context of statistical model checking of LTL properties [13]. How randomization can improve monitors for non-probabilistic systems has been examined in [7]. The safety level of [19] measures which portion of a language admits bad prefixes, in the sense classically used for safety languages.

2 Preliminaries

2.0.1 Markov chains.

A discrete-time Markov chain (DTMC) $M$ is a tuple $(S,s_{0},\mathbf{P})$ , where $S$ is a finite set of states, $s_{0}\in S$ is the initial state, and $\mathbf{P}\colon S\times S\to[0,1]$ is the transition probability function where we require $\sum_{s^{\prime}\in S}\mathbf{P}(s,s^{\prime})=1$ for all $s\in S$ . For algorithmic problems all transition probabilities are assumed to be rational. A finite path $\hat{\pi}$ in $M$ is a sequence $s_{0}s_{1}\ldots s_{n}$ of states such that $\mathbf{P}(s_{i},s_{i+1})>0$ for all $0\leq i\leq n-1$ . Let $\operatorname{last}(s_{0}\ldots s_{n})=s_{n}$ . Similarly one defines the notion of an infinite path $\pi$ . Let $\operatorname{Paths}_{\operatorname{fin}}(M)$ and $\operatorname{Paths}(M)$ be the set of finite and infinite paths. The set of prefixes of a path $\pi$ is denoted by $\operatorname{Pref}(\pi)$ . The cylinder set of a finite path $\hat{\pi}$ is $\operatorname{Cyl}(\hat{\pi})=\{\pi\in\ \operatorname{Paths}(M)\mid\hat{\pi}\in\operatorname{Pref}(\pi)\}$ . We consider $\operatorname{Paths}(M)$ as a probability space whose $\sigma$ -algebra is generated by such cylinder sets and whose probability measure is induced by $\mathrm{Pr}(\operatorname{Cyl}(s_{0}\ldots s_{n}))=\mathbf{P}(s_{0},s_{1})\cdot\ldots\cdot\mathbf{P}(s_{n-1},s_{n})$ (see [1, Chapter 10] for more details).

For an $\omega$ -regular language $\mathcal{L}\subseteq S^{\omega}$ let $\operatorname{Paths}_{M}(\mathcal{L})=\operatorname{Paths}(M)\cap\mathcal{L}$ . The probability of $\mathcal{L}$ in $M$ is defined as $\mathrm{Pr}_{M}(\mathcal{L})=\mathrm{Pr}(\operatorname{Paths}_{M}(\mathcal{L}))$ . Given a state $s\in S$ , let $\mathrm{Pr}_{M,s}(\mathcal{L})=\mathrm{Pr}_{M_{s}}(\mathcal{L})$ , where $M_{s}$ is the DTMC obtained from $M$ by replacing the initial state $s_{0}$ with $s$ . If $M$ is clear from the context, we omit the subscript. For a finite path $\hat{\pi}\in\operatorname{Paths}_{\operatorname{fin}}(M)$ , define the conditional probability

\mathrm{Pr}_{M}(\mathcal{L}\mid\hat{\pi})=\frac{\mathrm{Pr}_{M}\left(\operatorname{Paths}_{M}(\mathcal{L})\cap\operatorname{Cyl}(\hat{\pi})\right)}{\mathrm{Pr}_{M}(\operatorname{Cyl}(\hat{\pi}))}.

Given $E\subseteq S$ , let $\lozenge E=\{s_{0}s_{1}\ldots\in\operatorname{Paths}(M)\mid\exists i\geq 0.\;s_{i}\in E\}$ . For such reachability properties we have $\mathrm{Pr}_{M}(\lozenge E\mid s_{0}\ldots s_{n})=\mathrm{Pr}_{M,s_{n}}(\lozenge E)$ for any $s_{0}\ldots s_{n}\in\operatorname{Paths}_{\operatorname{fin}}(M)$ . We assume $\mathrm{Pr}_{s_{0}}(\lozenge s)>0$ all states $s\in S$ . Furthermore, define a weight function on $M$ as a map $c:S\to\mathbb{Q}$ . We typically use it to induce a weight function $c:\operatorname{Paths}_{\operatorname{fin}}(M)\to\mathbb{Q}$ (denoted by the same letter) by accumulation, i.e., $c(s_{0}\cdots s_{n})=\sum_{i=0}^{n}c(s_{i})$ . Finally, a set $\Pi\subseteq\operatorname{Paths}_{\operatorname{fin}}(M)$ is called prefix-free if for every $\hat{\pi}\in\Pi$ we have $\Pi\cap\operatorname{Pref}(\hat{\pi})=\{\hat{\pi}\}$ .

2.0.2 Markov decision processes.

A Markov decision process (MDP) $\mathcal{M}$ is a tuple $(S,\operatorname{Act},s_{0},\mathbf{P})$ , where $S$ is a finite set of states, $\operatorname{Act}$ is a finite set of actions, $s_{0}$ is the initial state, and $\mathbf{P}\colon S\times\operatorname{Act}\times S\to[0,1]$ is the transition probability function such that for all states $s\in S$ and actions $\alpha\in\operatorname{Act}$ we have $\sum_{s^{\prime}\in S}\mathbf{P}(s,\alpha,s^{\prime})\in\{0,1\}$ . An action $\alpha$ is enabled in state $s\in S$ if $\sum_{s^{\prime}\in S}\mathbf{P}(s,\alpha,s^{\prime})=1$ and we define $\operatorname{Act}(s)=\{\alpha\mid\alpha\text{ is enabled in }s\}$ . We require $\operatorname{Act}(s)\neq\emptyset$ for all states $s\in S$ .

An infinite path in $\mathcal{M}$ is an infinite sequence $\pi=s_{0}\alpha_{1}s_{1}\alpha_{2}s_{2}\dots\in(S\times\operatorname{Act})^{\omega}$ such that for all $i\geq 0$ we have $\mathbf{P}(s_{i},\alpha_{i+1},s_{i+1})>0$ . Any finite prefix of $\pi$ that ends in a state is a finite path. A scheduler $\mathfrak{S}$ is a function that maps a finite path $s_{0}\alpha_{1}s_{1}\dots s_{n}$ to an enabled action $\alpha\in\operatorname{Act}(s_{n})$ . Therefore it resolves the nondeterminism of the MDP and induces a (potentially infinite) Markov chain $\mathcal{M}_{\mathfrak{S}}$ . If the chosen action only depends on the last state of the path, i.e., $\mathfrak{S}(s_{0}\alpha_{1}s_{1}\dots s_{n})=\mathfrak{S}(s_{n})$ , then the scheduler is called memoryless and naturally induces a finite DTMC. For more details on DTMCs and MDPs we refer to [1].

3 Causes

This section introduces a notion of cause for $\omega$ -regular properties in Markov chains. For the rest of this section we fix a DTMC $M$ with state space $S$ , an $\omega$ -regular language $\mathcal{L}$ over the alphabet $S$ and a threshold $p\in(0,1]$ .

Definition 1 ( $p$ -critical prefix)

A finite path $\hat{\pi}$ is a $p$ -critical prefix for $\mathcal{L}$ if $\mathrm{Pr}(\mathcal{L}\mid\hat{\pi})\geq p$ .

Definition 2 ( $p$ -cause)

A $p$ -cause for $\mathcal{L}$ in $M$ is a prefix-free set of finite paths $\Pi\subseteq\operatorname{Paths}_{\operatorname{fin}}(M)$ such that

(1)

almost every $\pi\in\operatorname{Paths}_{M}(\mathcal{L})$ has a prefix $\hat{\pi}\in\Pi$ , and
(2)

every $\hat{\pi}\in\Pi$ is a $p$ -critical prefix for $\mathcal{L}$ .

Note that condition (1) and (2) are in the spirit of completeness and soundness as used in [11]. The first condition is our invocation of the counterfactuality principle: Almost every occurrence of the effect (for example, reaching a target set) is preceded by an element in the cause. If the threshold is chosen such that $p>\mathrm{Pr}_{s_{0}}(\mathcal{L})$ , then the second condition reflects the probability-raising principle in that seeing an element of $\Pi$ implies that the probability of the effect $\mathcal{L}$ has increased over the course of the execution. For monitoring purposes as described in the introduction it would be misleading to choose $p$ below $\mathrm{Pr}_{s_{0}}(\mathcal{L})$ as this could instantly trigger an alarm before the system is put to use. Also $p$ should not be too close to $1$ as this may result in an alarm being triggered too late.

If $\mathcal{L}$ coincides with a reachability property one could equivalently remove the almost from (1) of Definition 2. In general, however, ignoring paths with probability zero is necessary to guarantee the existence of $p$ -causes for all $p$ .

Example 1

Consider the DTMC $M$ depicted in Figure 3. For $p=3/4$ , a possible $p$ -cause for $\mathcal{L}=\lozenge\mathit{error}$ in $M$ is given by the set $\Pi_{1}=\{st,su\}$ since both $t$ and $u$ reach $\mathit{error}$ with probability greater or equal than $p$ . The sets $\Theta_{1}=\{st,su,stu\}$ and $\Theta_{2}=\{st\mathit{error},su\}$ are not $p$ -causes: $\Theta_{1}$ is not prefix-free and for $\Theta_{2}$ the path $stu\mathit{error}$ has no prefix in $\Theta_{2}$ . Another $p$ -cause is $\Pi_{2}=\{st\mathit{error},su,stu\}$ .

Example 2

It can happen that there does not exist any finite $p$ -cause. Consider Figure 3 and $p=1/2$ . Since $\mathrm{Pr}_{s}(\lozenge\mathit{error})<p$ , the singleton $\{s\}$ is not a $p$ -cause. Thus, for every $n\geq 0$ either $s^{n}t$ or $s^{n}t\mathit{error}$ is contained in any $p$ -cause, which must therefore be infinite. There may also exist non-regular $p$ -causes (as languages of finite words over $S$ ). For example, for $A=\{n\in\mathbb{N}\mid n\text{ prime}\}$ the $p$ -cause $\Pi_{A}=\{s_{0}^{n}t\mid n\in A\}\cup\{s_{0}^{m}t\mathit{error}\mid m\notin A\}$ is non-regular.

Figure 2: Example DTMC

M

Figure 3: Infinite and non-regular

1/2

-causes

Remark 1 (Reduction to reachability properties)

Let $\mathcal{A}$ be a deterministic Rabin automaton for $\mathcal{L}$ and consider the product Markov chain $M\otimes\mathcal{A}$ as in [1, Section 10.3]. For any finite path $\hat{\pi}=s_{0}\ldots s_{n}\in\operatorname{Paths}_{\operatorname{fin}}(M)$ there is a unique path $a(\hat{\pi})=(s_{0},q_{1})(s_{1},q_{2})\ldots(s_{n},q_{n+1})\in\operatorname{Paths}_{\operatorname{fin}}(M\otimes\mathcal{A})$ whose projection onto the first factor is $\hat{\pi}$ . Under this correspondence, a bottom strongly connected component (BSCC) of $M\otimes\mathcal{A}$ is either accepting or rejecting, meaning that for every finite path reaching this BSCC the corresponding path $\hat{\pi}$ in $M$ satisfies $\mathrm{Pr}_{M}(\mathcal{L}\mid\hat{\pi})=1$ , or respectively, $\mathrm{Pr}_{M}(\mathcal{L}\mid\hat{\pi})=0$ [1, Section 10.3]. This readily implies that almost every $\pi\in\operatorname{Paths}_{M}(\mathcal{L})$ has a $1$ -critical prefix and that, therefore, $p$ -causes exist for any $p$ .

Moreover, if $U$ is the union of all accepting BSCCs in $M\otimes\mathcal{A}$ , then

\mathrm{Pr}_{M}(\mathcal{L}\mid\hat{\pi})=\mathrm{Pr}_{M\otimes\mathcal{A}}\big{(}\lozenge U\mid a(\hat{\pi})\big{)}

(3.1)

holds for all finite paths $\hat{\pi}$ of $M$ [1, Theorem 10.56]. Hence every $p$ -cause $\Pi_{1}$ for $\mathcal{L}$ in $M$ induces a $p$ -cause $\Pi_{2}$ for $\lozenge U$ in $M\otimes\mathcal{A}$ by taking $\Pi_{2}=\{a(\hat{\pi})\mid\hat{\pi}\in\Pi_{1}\}$ . Vice versa, given a $p$ -cause $\Pi_{2}$ for $\lozenge U$ in $M\otimes\mathcal{A}$ , then the set of projections of paths in $\Pi_{2}$ onto their first component is a $p$ -cause for $\mathcal{L}$ in $M$ . In summary, the reduction of $\omega$ -regular properties on $M$ to reachability properties on the product $M\otimes\mathcal{A}$ also induces a reduction on the level of causes.

Remark 1 motivates us to focus on reachability properties henceforth. To apply the algorithms presented in Section 4 to specifications given in richer formalisms such as LTL, one would first have to apply the reduction to reachability given above, which increases the worst-case complexity exponentially.

In order to align the exposition with the monitoring application we are targeting, we will consider the target set as representing an erroneous behavior that is to be avoided. After collapsing the target set, we may assume that there is a unique state $\mathit{error}\in S$ , so $\mathcal{L}=\lozenge\mathit{error}$ is the language we are interested in. Further, we collapse all states from which $\mathit{error}$ is not reachable to a unique state $\mathit{safe}\in S$ with the property $\mathrm{Pr}_{\mathit{safe}}(\lozenge\mathit{error})=0$ . After this pre-processing, we have $\mathrm{Pr}_{s_{0}}(\lozenge\{\mathit{error},\mathit{safe}\})=1$ . Define the set

S_{p}:=\{s\in S\mid\mathrm{Pr}_{s}(\lozenge\mathit{error})\geq p\}

of all acceptable final states for $p$ -critical prefixes. This set is never empty as $\mathit{error}\in S_{p}$ for all $p\in(0,1]$ .

There is a partial order on the set of $p$ -causes defined as follows: $\Pi\preceq\Phi$ if and only if for all $\phi\in\Phi$ there exists $\pi\in\Pi$ such that $\pi\in\operatorname{Pref}(\phi)$ . The reflexivity and transitivity are straightforward, and the antisymmetry follows from the fact that $p$ -causes are prefix-free. However, this order itself has no influence on the probability. In fact for two $p$ -causes $\Pi,\Phi$ with $\Pi\preceq\Phi$ it can happen that for $\pi\in\Pi,\phi\in\Phi$ we have $\mathrm{Pr}(\lozenge\mathit{error}\mid\pi)\geq\mathrm{Pr}(\lozenge\mathit{error}\mid\phi)$ . This partial order admits a minimal element which is a regular language over $S$ and which plays a crucial role for finding optimal causes in Section 4.

{restatable}

[Canonical $p$ -cause]propositioncanonicalpath Let

\displaystyle\Theta=\left\{s_{0}\cdots s_{n}\in\operatorname{Paths}_{\operatorname{fin}}(M)\;\middle|\;s_{n}\in S_{p}\text{ and for all $i<n$: }\>s_{i}\notin S_{p}\right\}.

Then $\Theta$ is a regular $p$ -cause (henceforth called the canonical $p$ -cause) and for all $p$ -causes $\Pi$ we have $\Theta\preceq\Pi$ .

We now introduce an MDP associated with $M$ whose schedulers correspond to the $p$ -causes of $M$ . This is useful both to represent $p$ -causes and for algorithmic questions we consider later.

Definition 3 ( $p$ -causal MDP)

For the DTMC $M=(S,s_{0},\mathbf{P})$ define the $p$ -causal MDP $\mathcal{C}_{p}(M)=(S,\{continue,pick\},s_{0},\mathbf{P}^{\prime})$ associated with $M$ , where $\mathbf{P}^{\prime}$ is defined as follows:

	$\displaystyle\mathbf{P^{\prime}}(s,continue,s^{\prime})$	$\displaystyle=\mathbf{P}(s,s^{\prime})\text{ for all }s,s^{\prime}\in S$
	$\displaystyle\mathbf{P^{\prime}}(s,pick,\mathit{error})$	$\displaystyle=\begin{cases}1&\text{ if }s\in S_{p}\\ 0&\text{ otherwise}\end{cases}$

Given a weight function $c$ on $M$ , we consider $c$ also as weight function on $\mathcal{C}_{p}(M)$ .

Example 3

Figure 4 demonstrates the $p$ -causal MDP construction of $\mathcal{C}_{p}(M)$ . The black edges are transitions of $M$ , probabilities are omitted. Let us assume $S_{p}\backslash\{\mathit{error}\}=\{s_{1},s_{3},s_{4}\}$ . To construct $\mathcal{C}_{p}(M)$ one adds transitions for the action $pick$ , as shown by red edges.

Figure 4: Illustration of the

p

-causal MDP construction

Technically, schedulers are defined on all finite paths of an MDP $\mathcal{M}$ . However, under any scheduler, there are usually paths that cannot be obtained under the scheduler. Thus we define an equivalence relation $\equiv$ on the set of schedulers of $\mathcal{M}$ by setting $\mathfrak{S}\equiv\mathfrak{S}^{\prime}$ if $\operatorname{Paths}(\mathcal{M}_{\mathfrak{S}})=\operatorname{Paths}(\mathcal{M}_{\mathfrak{S}^{\prime}})$ . Note that two schedulers equivalent under $\equiv$ behave identically.

Lemma 1

There is a one-to-one correspondence between equivalence classes of schedulers in $\mathcal{C}_{p}(M)$ w.r.t. $\equiv$ and $p$ -causes in $M$ for $\lozenge\mathit{error}$ .

Proof

Given a $p$ -cause $\Pi$ for $\lozenge\mathit{error}$ in $M$ , we construct the equivalence class of scheduler $[\mathfrak{S}_{\Pi}]$ by defining $\mathfrak{S}_{\Pi}(\hat{\pi})=pick$ if $\hat{\pi}\in\Pi$ , and otherwise $\mathfrak{S}_{\Pi}(\hat{\pi})=continue$ . Vice versa, given an equivalence class $[\mathfrak{S}]$ of schedulers, we define the $p$ -cause

\displaystyle\Pi_{\mathfrak{S}}=\left\{\hat{\pi}\in\operatorname{Paths}_{\operatorname{fin}}(M)\;\middle|\;\begin{aligned} &\mathfrak{S}(\hat{\pi})=pick\text{ or $\hat{\pi}$ ends in $\mathit{error}$ and}\\ &\text{$\mathfrak{S}$ does not choose $pick$ on any prefix of $\hat{\pi}$}\end{aligned}\right\}

Since $pick$ can only be chosen once on every path in $\operatorname{Paths}(\mathcal{M}_{\mathfrak{S}})$ , it is easy to see that $\mathfrak{S}\equiv\mathfrak{S}^{\prime}$ implies $\Pi_{\mathfrak{S}}=\Pi_{\mathfrak{S}^{\prime}}$ . Note that every $\hat{\pi}\in\Pi_{\mathfrak{S}}$ is a $p$ -critical prefix since it ends in $S_{p}$ and every path in $\lozenge\mathit{error}$ is covered since either $pick$ is chosen or $\hat{\pi}$ ends in $\mathit{error}$ . Furthermore, the second condition makes $\Pi$ prefix-free. ∎

3.1 Types of $p$ -causes and induced monitors

We now introduce two classes of $p$ -causes which have a comparatively simple representation, and we explain what classes of schedulers they correspond to in the $p$ -causal MDP and how monitors can be derived for them.

Definition 4 (State-based $p$ -cause)

A $p$ -cause $\Pi$ is state-based if there exists a set of states $Q\subseteq S_{p}$ such that $\Pi=\{s_{0}\ldots s_{n}\in\operatorname{Paths}_{\operatorname{fin}}(M)\mid s_{n}\in Q\text{ and }\forall i<n:\;s_{i}\notin Q\}$ .

State-based $p$ -causes correspond to memoryless schedulers of $\mathcal{C}_{p}(M)$ which choose $pick$ exactly for paths ending in $Q$ . For DTMCs equipped with a weight function we introduce threshold-based $p$ -causes:

Definition 5 (Threshold-based $p$ -cause)

A $p$ -cause $\Pi$ is threshold-based if there exists a map $T:S_{p}\to\mathbb{Q}\cup\{\infty\}$ such that

\Pi=\left\{s_{0}\cdots s_{n}\in\operatorname{Paths}_{\operatorname{fin}}(M)\;\middle|\;\begin{aligned} &s_{0}\cdots s_{n}\in\operatorname{pick}(T)\text{ and}\\ &s_{0}\cdots s_{i}\notin\operatorname{pick}(T)\text{ for }i<n\end{aligned}\right\}

where $\operatorname{pick}(T)=\{s_{0}\ldots s_{n}\in\operatorname{Paths}_{\operatorname{fin}}(M)\mid s_{n}\in S_{p}\text{ and }c(s_{0}\ldots s_{n})<T(s_{n})\}$ .

Threshold-based $p$ -causes correspond to a simple class of weight-based schedulers of the $p$ -causal MDP, which base their decision in a state only on whether the current weight exceeds the threshold or not. Intuitively, threshold-based $p$ -causes are useful if triggering an alarm causes costs while reaching a safe state does not (see Section 4.2): The idea is that cheap paths (satisfying $c(s_{0}\ldots s_{n})<T(s_{n})$ ) are picked for the $p$ -cause, while expensive paths are continued in order to realize the chance (with probability $\leq 1{-}p$ ) that a safe state is reached and therefore the high cost that has already been accumulated is avoided.

The concept of $p$ -causes can be used as a basis for monitors that raise an alarm as soon as a state sequence in the $p$ -cause has been observed. State-based $p$ -causes have the advantage that they are realizable by “memoryless” monitors that only need the information on the current state of the Markov chain. Threshold-based monitors additonally need to track the weight that has been accumulated so far until the threshold value of the current state is exceeded. So, the memory requirements of monitors realizing a threshold-based $p$ -cause are given by the logarithmic length of the largest threshold value for $S_{p}$ -states. All algorithms proposed in Section 4 for computing cost-minimal $p$ -causes will return $p$ -causes that are either state-based or threshold-based with polynomially bounded memory requirements.

3.2 Comparison to prima facie causes

The work [34] presents the notion of prima facie causes in DTMCs where both causes and events are formalized as PCTL state formulae. In our setting we can equivalently consider a state $\mathit{error}\in S$ as the effect and a state subset $C\subseteq S$ constituting the cause. We then reformulate [34, Definition 4.1] to our setting.

Definition 6 (cf. [34])

A set $C\subseteq S$ is a $p$ -prima facie cause of $\lozenge\mathit{error}$ if the following three conditions hold:

(1)

The set $C$ is reachable from the initial state and $\mathit{error}\notin C$ .
(2)

$\forall s\in C:\;\mathrm{Pr}_{s}(\lozenge\mathit{error})\geq p$
(3)

$\mathrm{Pr}_{s_{0}}(\lozenge\mathit{error})<p$

The condition $p>\mathrm{Pr}_{s_{0}}(\lozenge\mathit{error})$ we discussed for $p$ -causes is hard-coded here as (3). In [34] the value $p$ is implicitly existentially quantified and thus conditions (2) and (3) can be combined to $\mathrm{Pr}_{s}(\lozenge\mathit{error})>\mathrm{Pr}_{s_{0}}(\lozenge\mathit{error})$ for all $s\in C$ . This encapsulates the probability-raising property. However, $\mathit{error}$ may be reached while avoiding the cause $C$ , so $p$ -prima facie causes do not entail the counterfactuality principle. Definition 2 can be seen as an extension of $p$ -prima facie causes by virtue of the following lemma:

Lemma 2

For $p>\mathrm{Pr}_{s_{0}}(\lozenge\mathit{error})$ every $p$ -prima facie cause induces a state-based $p$ -cause.

Proof

Let $C\subseteq S$ be a $p$ -prima facie cause. By condition (1) and (2) of Definition 6 we have $C\subseteq S_{p}\backslash\{\mathit{error}\}$ . Since every path reaching $\mathit{error}$ trivially visits a state in $Q:=C\cup\{\mathit{error}\}\subseteq S_{p}$ , the set $\Pi=\{s_{0}\ldots s_{n}\in\operatorname{Paths}_{\operatorname{fin}}(M)\mid s_{n}\in Q\text{ and }\forall i<n:\;s_{i}\notin Q\}$ is a state-based $p$ -cause. ∎

4 Costs of $p$ -causes

In this section we fix a DTMC $M$ with state space $S$ , unique initial state $s_{0}$ , unique target and safe state $\mathit{error},\mathit{safe}\in S$ and a threshold $p\in(0,1]$ . As motivated in the introduction, we equip the DTMC of our model with a weight function $c\colon S\to\mathbb{Q}$ on states and consider the induced accumulated weight function $c\colon\operatorname{Paths}_{\operatorname{fin}}(M)\to\mathbb{Q}$ . These weights typically represent resources spent, e.g., energy, time, material, etc.

4.1 Expected cost of a $p$ -cause

Definition 7 (Expected cost)

Given a $p$ -cause $\Pi$ for $\lozenge\mathit{error}$ in $M$ consider the random variable $\mathcal{X}:\operatorname{Paths}(M)\to\mathbb{Q}$ with

\mathcal{X}(\pi)=c(\hat{\pi})\text{ for }\begin{cases}\hat{\pi}\in\Pi\cap\operatorname{Pref}(\pi)&\text{ if such }\hat{\pi}\text{ exists}\\ \hat{\pi}\in\operatorname{Pref}(\pi)\text{ minimal with }\operatorname{last}(\hat{\pi})=\mathit{safe}&\text{ otherwise}.\end{cases}

Since $\mathrm{Pr}_{s_{0}}(\lozenge\{\mathit{error},\mathit{safe}\})=1$ , paths not falling under the two cases above have measure $0$ . Then the expected cost $\operatorname{expcost}(\Pi)$ of $\Pi$ is the expected value of $\mathcal{X}$ .

The expected cost is a means by which the efficiency of causes for monitoring purposes can be estimated. Assume a $p$ -cause $\Pi$ is used to monitor critical scenarios of a probabilistic system. This means that at some point either a critical scenario is predicted by the monitor (i.e., the execution seen so far lies in $\Pi$ ), or the monitor reports that no critical scenario will arise (i.e., $\mathit{safe}$ has been reached) and can therefore be turned off. If the weight function on the state space is chosen such that it models the cost of monitoring the respective states, then $\operatorname{expcost}(\Pi)$ estimates the average total resource consumption of the monitor.

We say that a $p$ -cause $\Pi$ is $\operatorname{expcost}$ -minimal if for all $p$ -causes $\Phi$ we have $\operatorname{expcost}(\Pi)\leq\operatorname{expcost}(\Phi)$ . By $\operatorname{expcost}^{\min}$ , we denote the value $\operatorname{expcost}(\Pi)$ of any $\operatorname{expcost}$ -minimal $p$ -cause $\Pi$ .

{restatable}

theoremexpcostComplexity

(1)

Given a non-negative weight function $c:S\to\mathbb{Q}_{\geq 0}$ , the canonical $p$ -cause $\Theta$ from Remark 1 is $\operatorname{expcost}$ -minimal.
(2)

For an arbitrary weight function $c:S\to\mathbb{Q}$ , an $\operatorname{expcost}$ -minimal and state-based $p$ -cause $\Pi$ and $\operatorname{expcost}^{\min}$ can be computed in polynomial time.

Proof

The statement (1) follows from the fact that if $\Pi\preceq\Phi$ holds for two $p$ -causes, then we have $\operatorname{expcost}(\Pi)\leq\operatorname{expcost}(\Phi)$ , which is shown in the appendix. The value $\operatorname{expcost}^{\min}=\operatorname{expcost}(\Theta)$ can then be computed in polynomial time using methods for expected rewards in Markov chains[1, Section 10.5].

To show (2), we reduce our problem to the stochastic shortest path problem (SSP)[4] from $s_{0}$ to $\{\mathit{error},\mathit{safe}\}$ . By Lemma 1 equivalence classes of schedulers in $\mathcal{C}_{p}(M)$ are in one-to-one correspondence with $p$ -causes in $M$ . Let $\Pi_{\mathfrak{S}}$ be a $p$ -cause associated with a representative scheduler $\mathfrak{S}$ . One can show that $\operatorname{expcost}(\Pi_{\mathfrak{S}})$ is equal to the expected accumulated weight of paths under scheduler $\mathfrak{S}$ in $\mathcal{C}_{p}(M)$ upon reaching $\{\mathit{error},\mathit{safe}\}$ . A scheduler $\mathfrak{S}^{*}$ minimizing this value can be computed in polynomial time by solving the SSP in $\mathcal{C}_{p}(M)$ [4], and the algorithm returns a memoryless such $\mathfrak{S}^{*}$ . It follows that $\Pi_{\mathfrak{S}^{*}}$ is an $\operatorname{expcost}$ -minimal and state-based $p$ -cause. ∎

4.2 Partial expected cost of a $p$ -cause

In this section we study a variant of the expected cost where paths with no prefix in the $p$ -cause are attributed zero costs. A use case for this cost mechanism arises if the costs are not incurred by monitoring the system, but by the countermeasures taken upon triggering the alarm. For example, an alarm might be followed by a downtime of the system, and the cost of this may depend on the current state and history of the execution. In such cases there are no costs incurred if no alarm is triggered.

Definition 8 (Partial expected cost)

For a $p$ -cause $\Pi$ for $\lozenge\mathit{error}$ in $M$ consider the random variable $\mathcal{X}:\operatorname{Paths}(M)\to\mathbb{Q}$ with

\displaystyle\mathcal{X}(\pi)=\begin{cases}c(\hat{\pi})&\text{for }\hat{\pi}\in\Pi\cap\operatorname{Pref}(\pi)\text{ if such }\hat{\pi}\text{ exists}\\ 0&\text{otherwise}.\end{cases}

The partial expected cost $\operatorname{pexpcost}(\Pi)$ of $\Pi$ is the expected value of $\mathcal{X}$ .

The analogous statement to Definition 7 (1) does not hold for partial expected costs, as the following example shows.

Example 4

Figure 5: An example showing that the partial expected cost is not monotonous on

p

-causes when

c

is non-negative.

Consider the Markov chain depicted in Figure 5. For $p=1/2$ and $\lozenge\mathit{error}$ we have $S_{p}=\{t,u,\mathit{error}\}$ . The canonical $p$ -cause is $\Theta=\{s_{0}^{k}t\mid k\geq 1\}$ with $\operatorname{pexpcost}(\Theta)=\sum_{k\geq 1}(1/4)^{k}\cdot k=4/9$ . Now let $\Pi$ be any $p$ -cause for $\lozenge\mathit{error}$ . If the path $s_{0}^{\ell}t$ belongs to $\Pi$ , then it contributes $(1/4)^{\ell}\cdot\ell$ to $\operatorname{pexpcost}(\Pi)$ . If instead the paths $s_{0}^{\ell}t\mathit{error}$ and $s_{0}^{\ell}tu\mathit{error}$ belong to $\Pi$ , they contribute $(1/4)^{\ell}\cdot 1/2\cdot\ell+(1/4)^{\ell}\cdot 1/2\cdot 3/4\cdot(\ell+w)$ . So, the latter case provides a smaller $\operatorname{pexpcost}$ if $l>3w$ , and the $\operatorname{pexpcost}$ -minimal $p$ -cause is therefore

\Pi=\{s_{0}^{k}t\mid 1\leq k\leq 3w\}\cup\{s_{0}^{k}t\mathit{error},s_{0}^{k}tu\mid 3w<k\}.

For $w=1$ , the expected cost of this $p$ -cause is $511/1152=4/9-1/1152$ . So, it is indeed smaller than $\operatorname{pexpcost}(\Theta)$ .

{restatable}

theorempexpcostPseudoP Given a non-negative weight function $c\colon S\to\mathbb{Q}_{\geq 0}$ , a $\operatorname{pexpcost}$ -minimal and threshold-based $p$ -cause $\Pi$ , and the value $\operatorname{pexpcost}^{\min}$ , can be computed in pseudo-polynomial time. $\Pi$ has a polynomially bounded representation.

Proof

For the pseudo-polynomial time bound we apply the techniques from [38] to optimize the partial expected cost in MDPs to the $p$ -causal MDP $\mathcal{C}_{p}(M)$ . It is shown in [38] that there is an optimal scheduler whose decision depends only on the current state and accumulated weight and that such a scheduler and its partial expectation can be computed in pseudo-polynomial time. It is further shown that a rational number $K$ can be computed in polynomial time such that for accumulated weights above $K$ , an optimal scheduler has to minimize the probability to reach $\mathit{error}$ . In our case, this means choosing the action $continue$ . Due to the special structure of $\mathcal{C}_{p}(M)$ , we can further show that there is indeed a threshold $T(s)$ for each state $s$ such that action $pick$ is optimal after a path $\hat{\pi}$ ending in $s$ if and only if $c(\hat{\pi})<T(s)$ . So, a threshold-based $\operatorname{pexpcost}$ -minimal $p$ -cause can be computed in pseudo-polynomial time. Furthermore, we have $T(s)<K$ for each state $s$ and as $K$ has a polynomially bounded representation the same applies to the values $T(s)$ for all states $s$ . ∎

Since the causal MDP $\mathcal{C}_{p}(M)$ has a comparatively simple form, one could expect that one can do better than the pseudo-polynomial algorithm obtained by reduction to [38]. Nevertheless, in the remainder of this section we argue that computing a $\operatorname{pexpcost}$ -minimal $p$ -cause is computationally hard, in contrast to $\operatorname{expcost}$ (cf. Definition 7). For this we recall that the complexity class $\mathtt{PP}$ [22] is characterized as the class of languages $\mathcal{L}$ that have a probabilistic polynomial-time bounded Turing machine $M_{\mathcal{L}}$ such that for all words $\tau$ one has $\tau\in\mathcal{L}$ if and only if $M_{\mathcal{L}}$ accepts $\tau$ with probability at least $1/2$ (cf. [25]). We will use polynomial Turing reductions, which, in contrast to many-one reductions, allow querying an oracle that solves the problem we reduce to a polynomial number of times. A polynomial time algorithm for a problem that is $\mathtt{PP}$ -hard under polynomial Turing reductions would imply that the polynomial hierarchy collapses [42]. We reduce the $\mathtt{PP}$ -complete cost-problem stated in [24, Theorem 3] to the problem of computing $\operatorname{pexpcost}^{\min}$ .

Figure 6: The DTMCs

N_{i}

for

i=0,1

{restatable}

theorempexpcostPP Given an acyclic DTMC $M$ , a weight function $c\colon S\to\mathbb{N}$ and a rational $\vartheta\in\mathbb{Q}$ , deciding whether $\operatorname{pexpcost}^{\min}\leq\vartheta$ is $\mathtt{PP}$ -hard under Turing reductions.

Proof

We sketch a Turing reduction from the following problem which is shown to be $\mathtt{PP}$ -hard in[24]: Given an acyclic DTMC $M$ over state space $S$ with initial state $s$ , absorbing state $t$ such that $\mathrm{Pr}_{s}(\lozenge t)=1$ , weight function $c:S\to\mathbb{N}$ and natural number $R\in\mathbb{N}$ , decide whether

\mathrm{Pr}_{M}(\{\pi\in\operatorname{Paths}(M)\mid c(\pi)\leq R\})\geq 1/2.

In an acyclic Markov chain $M$ the values of $\operatorname{pexpcost}$ have a polynomially bounded binary representation as shown in the appendix. This allows for a binary search to compute $\operatorname{pexpcost}^{\min}$ with polynomially many calls to the corresponding threshold problem. We use this procedure in a polynomial-time Turing reduction.

Let now $M$ be a Markov chain as in [24, Theorem 3] and let $R$ be a natural number. We construct two Markov chains $N_{0}$ and $N_{1}$ depicted in Figure 6. The $\operatorname{pexpcost}$ -minimal $p$ -cause in both Markov chains consists of all paths reaching $c$ with weight $\leq R$ and all paths reaching $\mathit{error}$ that do not have a prefix reaching $c$ with weight $\leq R$ . The difference between the values $\operatorname{pexpcost}^{\min}$ in the two Markov chains depends only on the probability of paths in the minimal $p$ -cause collecting the additional weight $+1$ in $N_{1}$ . This probability is $\frac{1}{6}\mathrm{Pr}_{M}(\{\pi\in\operatorname{Paths}(M)\mid c(\pi)\leq R\})$ . By repeatedly using the threshold problem to compute $\operatorname{pexpcost}^{\min}$ in $N_{0}$ and $N_{1}$ as described above, we can hence decide the problem from [24, Theorem 3]. More details can be found in the appendix. ∎

4.3 Maximal cost of a $p$ -cause

In practice, the weight function on the Markov chain potentially models resources for which the available consumption has a tight upper bound. For example, the amount of energy a drone can consume from its battery is naturally limited. Instead of just knowing that on average the consumption will lie below a given bound, it is therefore often desirable to find monitors whose costs are guaranteed to lie below this limit for (almost) any evolution of the system.

Definition 9 (Maximal cost)

Let $\Pi$ be a $p$ -cause for $\lozenge\mathit{error}$ in $M$ . We define the maximal cost of $\Pi$ to be

\displaystyle\operatorname{maxcost}(\Pi)

\displaystyle=\sup\{c(\hat{\pi})\mid\hat{\pi}\in\Pi\}.

The maximal cost of a $p$ -cause is a measure for the worst-case resource consumption among executions of the system. Therefore, by knowing the minimal value $\operatorname{maxcost}^{\min}$ for $p$ -causes one can ensure that there will be no critical scenario arising from resource management. {restatable}theoremmaxcostSummary

(1)

Given a non-negative weight function $c:S\to\mathbb{Q}_{\geq 0}$ , the canonical $p$ -cause $\Theta$ is $\operatorname{maxcost}$ -minimal and $\operatorname{maxcost}^{\min}$ can be computed in time polynomial in the size of $M$ .
(2)

For an arbitrary weight function $c:S\to\mathbb{Q}$ a $\operatorname{maxcost}$ -minimal and state-based $p$ -cause $\Pi$ and $\operatorname{maxcost}^{\min}$ can be computed in pseudo-polynomial time.
(3)

Given a rational $\vartheta\in\mathbb{Q}$ , deciding whether $\operatorname{maxcost}^{\min}\leq\vartheta$ is in $\mathtt{NP}\cap\mathtt{coNP}$ .

Proof

To show (1) it suffices to note that for non-negative weight functions $\operatorname{maxcost}$ is monotonous with respect to the partial order $\preceq$ on $p$ -causes. Therefore $\Theta$ is $\operatorname{maxcost}$ -minimal. For (2) we reduce the problem to a max-cost reachability game as defined in [6]. The algorithm from [6] computes the lowest maximal cost and has a pseudo-polynomial time bound. By virtue of the fact that the minimizing player has a memoryless strategy we can compute a set of states $Q\subseteq S_{p}$ on which a $\operatorname{maxcost}$ -minimal $p$ -cause $\Pi$ is based upon. In order to show (3) we reduce the max-cost reachability game from (2) further to mean-payoff games, as seen in [8]. Mean-payoff games are known to lie in $\mathtt{NP}\cap\mathtt{coNP}$ [8]. ∎

4.4 Instantaneous cost

The given weight function $c$ on states can also induce an instantaneous weight function $c_{\operatorname{inst}}:\operatorname{Paths}_{\operatorname{fin}}(M)\to\mathbb{Q}$ which just takes the weight of the state visited last, i.e., $c_{\operatorname{inst}}(s_{0}\cdots s_{n})=c(s_{n})$ . This yields an alternative cost mechanism intended to model the situation where the cost of repairing or rebooting only depends on the current state, e.g., the altitude an automated drone has reached.

We add the subscript ‘ ${\operatorname{inst}}$ ’ to the three cost variants, where the accumulative weight function $c$ has been replaced with the instantaneous weight function $c_{\operatorname{inst}}$ , the error state is replaced by an error set $E$ and the safe state is replaced by a set of terminal safe states $F$ . Thus we optimize $p$ -causes for $\lozenge E$ in $M$ .

{restatable}

theoreminstcost For $\operatorname{expcost}_{\operatorname{inst}}$ , $\operatorname{pexpcost}_{\operatorname{inst}}$ , and $\operatorname{maxcost}_{\operatorname{inst}}$ a cost-minimal $p$ -cause $\Pi$ and the value of the minimal cost can be computed in time polynomial in $M$ . In all cases $\Pi$ can be chosen to be a state-based $p$ -cause.

Proof

We first note that $\operatorname{pexpcost}_{\operatorname{inst}}$ can be reduced to $\operatorname{expcost}_{\operatorname{inst}}$ by setting the weight of all states in $F$ to $0$ . We then construct an MDP (different from $\mathcal{C}_{p}(M)$ ) which emulates the instantaneous weight function using an accumulating weight function. Thus, finding an $\operatorname{expcost}_{\operatorname{inst}}$ -minimal $p$ -cause $\Pi$ reduces to the SSP from [4], which can be solved in polynomial time. The solution admits a memoryless scheduler and thus $\Pi$ is state-based in this case.

For $\operatorname{maxcost}_{\operatorname{inst}}$ we order the states in $S_{p}$ by their cost and then start iteratively removing the states with lowest cost until $E$ is not reachable anymore. The set $Q$ of states which where removed induce a state-based $\operatorname{maxcost}_{\operatorname{inst}}$ -minimal $p$ -cause $\Pi$ . This gives us a polynomial time procedure to compute $\operatorname{maxcost}_{\operatorname{inst}}^{\min}$ and $\Pi$ . ∎

5 Conclusion

We combined the counterfactuality principle and the probability-raising property into the notion of $p$ -causes in DTMCs. In order to find suitable $p$ -causes we defined different cost models and gave algorithms to compute corresponding cost-minimal causes.

Cyber-physical systems are often not fully probabilistic, but involve a certain amount of control in form of decisions depending on the system state. Such systems can be modeled by MDPs, to which we intend to generalize the causality framework presented here. Our approach also assumes that the probabilistic system described by the Markov chain is fully observable. By observing execution traces instead of paths of the system, generalizing the notion of $p$ -causes to hidden Markov models is straightforward. However, the corresponding computational problems exhibit additional difficulties which we address in future work.

References

[1] Baier, C., Katoen, J.P.: Principles of Model Checking (Representation and Mind Series). The MIT Press, Cambridge, MA (2008)
[2] Bartocci, E., Grosu, R., Karmarkar, A., Smolka, S.A., Stoller, S.D., Zadok, E., Seyster, J.: Adaptive Runtime Verification. In: Runtime Verification. pp. 168–182. Springer Berlin Heidelberg (2013). https://doi.org/10.1007/978-3-642-35632-2_18
[3] Beer, I., Ben-David, S., Chockler, H., Orni, A., Trefler, R.: Explaining counterexamples using causality. In: Computer Aided Verification (CAV’09). pp. 94–108. Springer Berlin Heidelberg (2009). https://doi.org/10.1007/978-3-642-02658-4_11
[4] Bertsekas, D.P., Tsitsiklis, J.N.: An analysis of stochastic shortest path problems. Math. Oper. Res. 16(3), 580–595 (1991)
[5] Braham, M., van Hees, M.: An anatomy of moral responsibility. Mind 121 (483), 601–634 (2012)
[6] Brihaye, T., Geeraerts, G., Haddad, A., Monmege, B.: To Reach or not to Reach? Efficient Algorithms for Total-Payoff Games. In: Proceedings of the 26th International Conference on Concurrency Theory (CONCUR’15). LIPIcs, vol. 42, pp. 297–310 (2015). https://doi.org/10.4230/LIPIcs.CONCUR.2015.297
[7] Chadha, R., Sistla, A.P., Viswanathan, M.: On the expressiveness and complexity of randomization in finite state monitors. J. ACM 56(5) (2009). https://doi.org/10.1145/1552285.1552287
[8] Chatterjee, K., Doyen, L., Henzinger, T.A.: The Cost of Exactness in Quantitative Reachability. In: Models, Algorithms, Logics and Tools. pp. 367–381. Springer International Publishing, Cham (2017). https://doi.org/10.1007/978-3-319-63121-9_18
[9] Chockler, H., Halpern, J.Y.: Responsibility and Blame: A Structural-Model Approach. J. Artif. Int. Res. 22(1), 93–115 (Oct 2004)
[10] Chockler, H., Halpern, J.Y., Kupferman, O.: What causes a system to satisfy a specification? ACM Transactions on Computational Logic 9(3), 20:1–20:26 (2008)
[11] Cini, C., Francalanza, A.: An LTL Proof System for Runtime Verification. In: Baier, C., Tinelli, C. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 581–595. Springer Berlin Heidelberg (2015)
[12] Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, Third Edition. The MIT Press, 3rd edn. (2009)
[13] Daca, P., Henzinger, T.A., Křetínský, J., Petrov, T.: Faster Statistical Model Checking for Unbounded Temporal Properties. In: Tools and Algorithms for the Construction and Analysis of Systems. pp. 112–129. Springer Berlin Heidelberg (2016). https://doi.org/10.1007/978-3-662-49674-9_7
[14] Dash, D., Voortman, M., De Jongh, M.: Sequences of Mechanisms for Causal Reasoning in Artificial Intelligence. In: Proceedings of the 23rd International Joint Conference on Artificial Intelligence. p. 839–845. IJCAI ’13, AAAI Press (2013)
[15] Eells, E.: Probabilistic Causality. Cambridge Studies in Probability, Induction and Decision Theory, Cambridge University Press (1991)
[16] Eiter, T., Lukasiewicz, T.: Complexity results for explanations in the structural-model approach. Artificial Intelligence 154(1-2), 145–198 (2004)
[17] Eiter, T., Lukasiewicz, T.: Causes and explanations in the structural-model approach: Tractable cases. Artificial Intelligence 170(6-7), 542–580 (2006)
[18] Esparza, J., Kiefer, S., Kretinsky, J., Weininger, M.: Online monitoring $\omega$ -regular properties in unknown Markov chains. Arxiv preprint, 2010.08347 (2020)
[19] Faran, R., Kupferman, O.: Spanning the spectrum from safety to liveness. Acta Informatica 55(8), 703–732 (2018). https://doi.org/10.1007/s00236-017-0307-4
[20] Feigenbaum, J., Hendler, J.A., Jaggard, A.D., Weitzner, D.J., Wright, R.N.: Accountability and Deterrence in Online Life. In: Proceedings of WebSci ’11. ACM, New York, NY, USA (2011). https://doi.org/10.1145/2527031.2527043
[21] Fenton-Glynn, L.: A Proposed Probabilistic Extension of the Halpern and Pearl Definition of ‘Actual Cause’. The British Journal for the Philosophy of Science 68(4), 1061–1124 (2016)
[22] Gill, J.: Computational complexity of probabilistic Turing machines. SIAM Journal on Computing 6(4), 675–695 (1977). https://doi.org/10.1137/0206049
[23] Gondi, K., Patel, Y., Sistla, A.P.: Monitoring the Full Range of $\omega$ -Regular Properties of Stochastic Systems. In: Proceedings of VMCAI’09:. pp. 105–119. Springer Berlin Heidelberg (2009). https://doi.org/10.1007/978-3-540-93900-9_12
[24] Haase, C., Kiefer, S.: The Odds of Staying on Budget. In: Automata, Languages, and Programming. pp. 234–246. Springer Berlin Heidelberg (2015). https://doi.org/10.1007/978-3-662-47666-6_19
[25] Haase, C., Kiefer, S.: The Complexity of the Kth Largest Subset Problem and Related Problems. Inf. Process. Lett. 116(2), 111–115 (2016). https://doi.org/10.1016/j.ipl.2015.09.015
[26] Halpern, J.Y.: A Modification of the Halpern-Pearl Definition of Causality. In: Proceedings of IJCAI’15. p. 3022–3033. AAAI Press (2015)
[27] Halpern, J.Y., Pearl, J.: Causes and Explanations: A Structural-Model Approach: Part 1: Causes. In: Proceedings of the 17th Conference in Uncertainty in Artificial Intelligence (UAI). pp. 194–202 (2001)
[28] Huang, Y., Kleinberg, S.: Fast and Accurate Causal Inference from Time Series Data. In: Proceedings of FLAIRS 2015. pp. 49–54. AAAI Press (2015)
[29] Ibrahim, A., Pretschner, A.: From Checking to Inference: Actual Causality Computations as Optimization Problems. In: Proceedings of ATVA’20. pp. 343–359. Springer Internat. Publishing, Cham (2020). https://doi.org/10.1007/978-3-030-59152-6_19
[30] Ibrahim, A., Pretschner, A., Klesel, T., Zibaei, E., Kacianka, S., Pretschner, A.: Actual Causality Canvas: A General Framework for Explanation-Based Socio-Technical Constructs. In: Proceedings of ECAI’20. pp. 2978 – 2985. IOS Press Ebooks (2020). https://doi.org/10.3233/FAIA200472
[31] Kalajdzic, K., Bartocci, E., Smolka, S.A., Stoller, S.D., Grosu, R.: Runtime Verification with Particle Filtering. In: Runtime Verification. pp. 149–166. Springer Berlin Heidelberg (2013). https://doi.org/10.1007/978-3-642-40787-1_9
[32] Kleinberg, S.: A Logic for Causal Inference in Time Series with Discrete and Continuous Variables. In: Proceedings of IJCAI’11. pp. 943–950 (2011)
[33] Kleinberg, S., Hripcsak, G.: A review of causal inference for biomedical informatics. J Biomed Inform. 44(6), 1102–12 (2011). https://doi.org/10.1016/j.jbi.2011.07.001
[34] Kleinberg, S., Mishra, B.: The Temporal Logic of Causal Structures. In: Proceedings of the Twenty-Fifth Conference on Uncertainty in Artificial Intelligence (UAI). pp. 303–312 (2009)
[35] Kleinberg, S., Mishra, B.: The Temporal Logic of Token Causes. In: Proceedings of KR’10. p. 575–577. AAAI Press (2010)
[36] Miller, T.: Explanation in Artificial Intelligence: Insights from the Social Sciences. Artificial Intelligence 267 (06 2017). https://doi.org/10.1016/j.artint.2018.07.007
[37] Pearl, J.: Causality. Cambridge University Press, 2nd edn. (2009)
[38] Piribauer, J., Baier, C.: Partial and conditional expectations in Markov decision processes with integer weights. In: Proceedings of FoSSaCS’19. Lecture Notes in Computer Science, vol. 11425, pp. 436–452. Springer (2019)
[39] Reichenbach, H.: The Direction of Time. Dover Publications (1956)
[40] Sistla, A.P., Srinivas, A.R.: Monitoring Temporal Properties of Stochastic Systems. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) Verification, Model Checking, and Abstract Interpretation. pp. 294–308. Springer Berlin Heidelberg (2008)
[41] Stoller, S.D., Bartocci, E., Seyster, J., Grosu, R., Havelund, K., Smolka, S.A., Zadok, E.: Runtime Verification with State Estimation. In: Runtime Verification. pp. 193–207. Springer Berlin Heidelberg (2012). https://doi.org/10.1007/978-3-642-29860-8_15
[42] Toda, S.: PP is as Hard as the Polynomial-Time Hierarchy. SIAM Journal on Computing 20(5), 865–877 (1991). https://doi.org/10.1137/0220053
[43] Vennekens, J., Bruynooghe, M., Denecker, M.: Embracing Events in Causal Modelling: Interventions and Counterfactuals in CP-Logic. In: Logics in Artificial Intelligence. pp. 313–325. Springer Berlin Heidelberg (2010)
[44] Vennekens, J., Denecker, M., Bruynooghe, M.: CP-logic: A language of causal probabilistic events and its relation to logic programming. Theory and Practice of Logic Programming 9(3), 245–308 (2009). https://doi.org/10.1017/S1471068409003767
[45] Zheng, M., Kleinberg, S.: A Method for Automating Token Causal Explanation and Discovery. In: Proceedings of FLAIRS’17 (2017)

6 Appendix

We will denote nondeterministic finite automata as tuples $\mathcal{A}=(Q,\Sigma,Q_{0},T,F)$ , where $Q$ is the set of states, $\Sigma$ is the alphabet, $Q_{0}\subseteq Q$ is the initial state, $T\colon Q\times\Sigma\to 2^{Q}$ is the transition function, and $F\subseteq Q$ are the final states. A transition $q^{\prime}\in T(q,\alpha)$ is also denoted by $q\overset{\alpha}{\mapsto}q^{\prime}$ .

\canonicalpath

Proof

The first condition $s_{n}\in S_{p}=\{s\in S\mid\mathrm{Pr}_{s}(\lozenge\mathit{error})\geq p\}$ ensures that every path in $\Theta$ is a $p$ -critical prefix for $\lozenge\mathit{error}$ in $M$ . The second condition ensures that no proper prefix is a $p$ -critical prefix, and therefore $\Theta$ is prefix-free. Clearly, every path reaching $\mathit{error}$ passes through $S_{p}$ since $\mathit{error}$ is itself an element in $S_{p}$ . These properties together show that $\Theta$ is a $p$ -cause.

Let $\Pi$ be another $p$ -cause for $\lozenge\mathit{error}$ in $M$ and consider an arbitrary path $s_{0}\ldots s_{n}\in\Pi$ . This means $s_{n}\in S_{p}$ . If we have for all $i<n$ that $\mathrm{Pr}_{s_{i}}(\lozenge\mathit{error})<p$ , then $s_{0}\ldots s_{n}\in\Theta$ and there is nothing to prove. Therefore assume that there exists $i<n$ such that $s_{i}\in S_{p}$ . For minimal such $i$ we have $s_{0}\ldots s_{i}\in\Theta$ and thus $\Theta\preceq\Pi$ .

To prove that $\Theta$ is regular, consider the deterministic finite automaton $\mathcal{A}=(Q,\Sigma,q_{0},T,F)$ for $Q=S$ , $\Sigma=S\cup\{\iota\}$ , $q_{0}=\iota$ , and final states $F=S_{p}$ . The transition relation is given by

T=\{\iota\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny$s_{0}$}}}{\mapsto}}s_{0}\}\cup\{s\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny$s^{\prime}$}}}{\mapsto}}s^{\prime}\mid P(s,s^{\prime})>0\wedge s\notin S_{p}\}

i.e., all states in $S_{p}$ are terminal. We argue that this automaton describes the language $\Theta$ :

If $s_{0}\in S_{p}$ then there are no transitions possible and $\mathcal{L}_{\mathcal{A}}=\{s_{0}\}$ and $\Theta=\{s_{0}\}$ by definition.

Let $\mathcal{L}_{\mathcal{A}}\subseteq\Theta$ and let $s_{0}\ldots s_{n}$ be a word accepted by $\mathcal{A}$ . By definition we have $s_{n}\in S_{p}$ For any state $s\in S_{p}$ visited by $s_{0}\cdots s_{n}$ we know that $s=s_{n}$ since $S_{p}$ is terminal. This means $\forall i<n.\;\mathrm{Pr}_{s_{i}}(\lozenge\mathit{error})<p$ and thus $s_{0}\ldots s_{n}\in\Theta$ .

Now let $\mathcal{L}_{\mathcal{A}}\supseteq\Theta$ and $s_{0}\ldots s_{n}\in\Theta$ . A run for $s_{0}\ldots s_{n}$ in $\mathcal{A}$ is possible, since we have an edge for every transition in $M$ except for outgoing edges of $S_{p}$ . These exceptions are avoided, since for $i<n$ we have $\mathrm{Pr}_{s_{i}}(\lozenge\mathit{error})<p$ and thus no state but the last one is in $S_{p}$ . On the other hand $s_{n}$ is in $S_{p}$ by assumption and thus the word $s_{0}\ldots s_{n}$ is accepted by $\mathcal{A}$ . ∎

In the following proof, let $\operatorname{Cyl}(\Pi)=\bigcup_{\pi\in\Pi}\operatorname{Cyl}(\pi)$ for $\Pi\subseteq\operatorname{Paths}_{\operatorname{fin}}(M)$ .

\expcostComplexity

Proof

To show (1), we claim that for two $p$ -causes $\Pi$ and $\Phi$ with $\Pi\preceq\Phi$ we have $\operatorname{expcost}(\Pi)\leq\operatorname{expcost}(\Phi)$ . Let $\mathcal{X}_{\Pi}$ and $\mathcal{X}_{\Phi}$ be the corresponding random variables of $\operatorname{expcost}(\Pi)$ and $\operatorname{expcost}(\Phi)$ , respectively. We prove $\operatorname{expcost}(\Pi)\leq\operatorname{expcost}(\Phi)$ by showing for almost all $\pi\in\operatorname{Paths}(M)$ that $\mathcal{X}_{\Pi}(\pi)\leq\mathcal{X}_{\Phi}(\pi)$ . In the argument below we ignore cases that have measure $0$ .

From $\Pi\preceq\Phi$ it follows that $\operatorname{Cyl}(\Pi)\supseteq\operatorname{Cyl}(\Phi)$ . We now deal separately with the three cases obtained by the partition

\operatorname{Paths}(M)=\operatorname{Cyl}(\Phi)\ \dot{\cup}\ \operatorname{Cyl}(\Pi)\backslash\operatorname{Cyl}(\Phi)\ \dot{\cup}\ \operatorname{Paths}(M)\backslash\operatorname{Cyl}(\Pi).

For $s_{0}s_{1}\ldots\in\operatorname{Cyl}(\Phi)$ both random variables consider the unique prefix of $s_{0}s_{1}\ldots$ in the respective $p$ -cause. For any $s_{0}\ldots s_{n}\in\Phi$ we know by definition of $\preceq$ that there is $s_{0}\ldots s_{m}\in\Pi$ with $m\leq n$ . Therefore

\mathcal{X}_{\Pi}(s_{0}s_{1}\ldots)=c(s_{0}\ldots s_{m})\leq c(s_{0}\ldots s_{n})=\mathcal{X}_{\Phi}(s_{0}s_{1}\ldots).

For $s_{0}s_{1}\ldots\in\operatorname{Cyl}(\Pi)\backslash\operatorname{Cyl}(\Phi)$ the random variable $\mathcal{X}_{\Pi}$ takes the unique prefix $s_{0}\ldots s_{m}$ in $\Pi$ , whereas $\mathcal{X}_{\Phi}$ takes the path $s_{0}\ldots s_{n}$ such that $s_{n}=\mathit{safe}$ . Since $\mathrm{Pr}_{\mathit{safe}}(\lozenge\mathit{error})=0$ , we have almost surely that $m<n$ , and therefore

\mathcal{X}_{\Pi}(s_{0}s_{1}\ldots)=c(s_{0}\ldots s_{m})\leq c(s_{0}\ldots s_{n})=\mathcal{X}_{\Phi}(s_{0}s_{1}\ldots).

For $s_{0}s_{1}\ldots\in\operatorname{Paths}(M)\backslash\operatorname{Cyl}(\Pi)$ both random variables evaluate the same path and therefore $\mathcal{X}_{\Pi}(s_{0}s_{1}\ldots)=\mathcal{X}_{\Phi}(s_{0}s_{1}\ldots)$ . Therefore we have for any $\pi\in\operatorname{Paths}(M)$ that $\mathcal{X}_{\Pi}(\pi)\leq\mathcal{X}_{\Phi}(\pi)$ .

To compute $\operatorname{expcost}^{\min}=\operatorname{expcost}(\Theta)$ consider the DTMC $M$ but change the transitions such that every state in $S_{p}$ is terminal. The value $\operatorname{expcost}(\Theta)$ is then the expected reward $\operatorname{ExpRew}(s_{0}\models\lozenge S_{p}\cup\{\mathit{safe}\})$ defined in [1, Definition 10.71]. Expected rewards in DTMCs can be computed in polynomial time via a classical linear equation system [1, Section 10.5.1].

We show (2) by reducing the problem of finding an $\operatorname{expcost}$ -minimal $p$ -cause to the stochastic shortest path problem (SSP) [4] in $\mathcal{C}_{p}(M)$ . For a scheduler $\mathfrak{S}$ of of $\mathcal{C}_{p}(M)$ denote the corresponding $p$ -cause for $\lozenge\mathit{error}$ in $M$ by $\Pi_{\mathfrak{S}}$ (cf. Lemma 1). In [4] the authors define the value expected cost of a scheduler $\mathfrak{S}$ in an MDP. This value with respect to the target set $\{\mathit{error},\mathit{safe}\}$ coincides with $\operatorname{expcost}(\Pi_{\mathfrak{S}})$ .

The SSP asks to find a scheduler $\mathfrak{S}^{*}$ in $\mathcal{C}_{p}(M)$ minimizing the expected cost. It is shown in [4] that a memoryless such $\mathfrak{S}^{*}$ and the value $\operatorname{expcost}^{\min}$ can be computed in polynomial time. The scheduler $\mathfrak{S}^{*}$ corresponds to an $\operatorname{expcost}$ -minimal state-based $p$ -cause $\Pi$ . ∎

\pexpcostPseudoP

Proof

Consider a scheduler $\mathfrak{S}$ of $\mathcal{C}_{p}(M)$ with weight function $c$ and recall that $\mathcal{C}_{p}(M)_{\mathfrak{S}}$ denotes Markov chain induced by $\mathfrak{S}$ . Define the random variable $\oplus_{\mathfrak{S}}\mathit{error}:\operatorname{Paths}(\mathcal{C}_{p}(M)_{\mathfrak{S}})\to\mathbb{Q}$

\oplus_{\mathfrak{S}}\mathit{error}(\pi)=\begin{cases}c(\pi)&\text{if }\pi\in\lozenge\mathit{error}\\ 0&\text{otherwise.}\end{cases}

The partial expectation ${\mathbb{PE}}^{\mathfrak{S}}$ of a scheduler $\mathfrak{S}$ in $\mathcal{C}_{p}(M)$ is defined as the expected value of $\oplus_{\mathfrak{S}}\mathit{error}$ . The minimal partial expectation is ${\mathbb{PE}}^{\min}=\inf_{\mathfrak{S}}{\mathbb{PE}}^{\mathfrak{S}}$ . It is known that there is a scheduler obtaining the minimal partial expectation [38].

Then a $p$ -cause $\Pi$ and the corresponding scheduler $\mathfrak{S}_{\Pi}$ satisfy $\operatorname{pexpcost}(\Pi)=\mathbb{PE}^{\mathfrak{S}_{\Pi}}$ . A cost-minimal scheduler for the partial expectation in an MDP with non-negative weights can be computed in pseudo-polynomial time by [38]. In this process we also compute $\operatorname{pexpcost}^{\min}={\mathbb{PE}}^{\min}$ .

Furthermore, we can show that once the action $continue$ is optimal in a state $s$ with accumulated weight $w$ , it is also optimal for all weights $w^{\prime}>w$ : Suppose choosing $continue$ is optimal in some state $s$ if the accumulated weight is $w$ . Let $E$ be the partial expected accumulated weight that the optimal scheduler collects from then on and let $q=\mathrm{Pr}_{s}(\lozenge\mathit{error})$ . The optimality of $continue$ implies that $E+w\cdot q\leq w$ . For all $w^{\prime}>w$ , this implies $E+w^{\prime}\cdot q\leq w^{\prime}$ as well. We conclude the existence of $T:S\to\mathbb{Q}$ such that $continue$ is optimal if and only if the accumulated weight is at least $T(s)$ . If $pick$ is not enabled in a state $s$ , we have $T(s)=0$ . Therefore $\Pi$ is a threshold-based $p$ -cause defined by $T$ . As shown in [38], there is a saturation point $K$ such that schedulers minimizing the partial expectation can be chosen to behave memoryless as soon as the accumulated weight exceeds $K$ . This means that $T(s)$ can be chosen to be either at most $K$ or $\infty$ for each state $s$ . The saturation point $K$ and hence all thresholds $T(s)$ have a polynomial representation. ∎

\pexpcostPP

Proof

Figure 7: The DTMCs

N_{i}

for

i=0,1

We provide a Turing reduction from the following problem that is shown to be $\mathtt{PP}$ -hard in [24]: Given an acyclic DTMC $M$ over state space $S$ with initial state $s$ , absorbing state $t$ such that $\mathrm{Pr}_{s}(\lozenge t)=1$ , weight function $c:S\to\mathbb{N}$ and natural number $R\in\mathbb{N}$ , decide whether

\mathrm{Pr}_{M}(\{\varphi\in\operatorname{Paths}(M)\mid c(\pi)\leq R\})\geq\frac{1}{2}.

Given such an acyclic DTMC $M$ we construct the two DTMCs $N_{0}$ and $N_{1}$ depicted in Figure 7. We consider the $\operatorname{pexpcost}$ -minimal $p$ -causes for $p=1/2$ in $N_{i}$ for $\lozenge\mathit{error}$ and $i\in\{0,1\}$ . Suppose a path $\pi$ arrives at state $c_{i}$ with probability $\mathrm{Pr}_{s}(\pi)$ and accumulated weight $w$ . We have to decide whether the path $\pi$ or the extension $\pi^{\prime}=\pi b_{i}\mathit{error}$ should be included in the cost-minimal $p$ -cause. The path $\pi^{\prime}$ has weight $w+R+i$ and probability $\mathrm{Pr}_{s}(\pi)/2$ . We observe that $\pi$ is the optimal choice if

\mathrm{Pr}_{s}(\pi)\cdot w\leq\mathrm{Pr}_{s}(\pi)\cdot\frac{w+R+i}{2}.

This is the case if and only if $w\leq R+i$ . If $i=1$ , and $w=R+i$ , both choices are equally good and we decide to include the path $\pi$ in this case. Hence, the $\operatorname{pexpcost}$ -minimal $p$ -causes for $p=1/2$ in $N_{0}$ is

	$\displaystyle\Pi_{0}=$	$\displaystyle\{\hat{\pi}\in\operatorname{Paths}_{\operatorname{fin}}(N_{0})\mid\operatorname{last}(\hat{\pi})=c_{0}\text{ and }c(\hat{\pi})\leq R\}\cup$
		$\displaystyle\{\hat{\pi}\ \in\operatorname{Paths}_{\operatorname{fin}}(N_{0})\mid\operatorname{last}(\hat{\pi})=\mathit{error}\text{ and }c(\hat{\pi})>2R\}.$

Similarly in $N_{1}$ the following $p$ -cause is $\operatorname{pexpcost}$ -minimal:

	$\displaystyle\Pi_{1}=$	$\displaystyle\{\hat{\pi}\in\operatorname{Paths}_{\operatorname{fin}}(N_{1})\mid\operatorname{last}(\hat{\pi})=c_{1}\text{ and }c(\hat{\pi})\leq R\}\cup$
		$\displaystyle\{\hat{\pi}\ \in\operatorname{Paths}_{\operatorname{fin}}(N_{1})\mid\operatorname{last}(\hat{\pi})=\mathit{error}\text{ and }c(\hat{\pi})>2R+1\}.$

Therefore we have

	$\displaystyle 3\cdot\operatorname{pexpcost}_{N_{0}}(\Pi_{0})=$	$\displaystyle\sum_{\varphi\in\operatorname{Paths}_{\operatorname{fin}}(M),c(\varphi)\leq R}\mathrm{Pr}(\varphi)c(\varphi)$
		$\displaystyle+\sum_{\varphi\in\operatorname{Paths}_{\operatorname{fin}}(M),c(\varphi)>R}\mathrm{Pr}(\varphi)\frac{c(\varphi)+R}{2},$
	$\displaystyle 3\cdot\operatorname{pexpcost}_{N_{1}}(\Pi_{1})=$	$\displaystyle\sum_{\varphi\in\operatorname{Paths}_{\operatorname{fin}}(M),c(\varphi)\leq R}\mathrm{Pr}(\varphi)c(\varphi)$
		$\displaystyle+\sum_{\varphi\in\operatorname{Paths}_{\operatorname{fin}}(M),c(\varphi)>R}\mathrm{Pr}(\varphi)\frac{c(\varphi)+R+1}{2}.$

We conclude that

		$\displaystyle\operatorname{pexpcost}_{N_{0}}^{\min}-\operatorname{pexpcost}_{N_{1}}^{\min}$
	$\displaystyle=$	$\displaystyle\operatorname{pexpcost}_{N_{0}}(\Pi_{0})-\operatorname{pexpcost}_{N_{1}}(\Pi_{1})$
	$\displaystyle=$	$\displaystyle\frac{1}{6}\cdot\mathrm{Pr}_{M}(\{\varphi\in\operatorname{Paths}(M)\mid c(\varphi)>R\})$
	$\displaystyle=$	$\displaystyle\frac{1}{6}\cdot(1-\mathrm{Pr}_{M}(\{\varphi\in\operatorname{Paths}(M)\mid c(\varphi)\leq R\}))$

In the sequel we prove that we can use an oracle for the threshold problem for $\operatorname{pexpcost}^{\min}$ to compute the values

\operatorname{pexpcost}_{N_{0}}^{\min}\qquad\text{and}\qquad\operatorname{pexpcost}_{N_{1}}^{\min}.

This in turn allows us to compute $\frac{1}{6}\mathrm{Pr}_{M}(\{\hat{\pi}\in\operatorname{Paths}(M)\mid c(\hat{\pi})\leq R\})$ and thus to decide the problem from [24].

In any acyclic Markov chain $K$ , the following holds: We assume that the transition probabilities are encoded as fractions of coprime integers. Therefore we can compute the product of all denominators to get a number $L$ in polynomial time and with polynomially bounded encoding. The maximal weight $W$ of a path in $K$ can be computed in linear time and has a polynomially bounded encoding. Therefore the minimal $\operatorname{pexpcost}$ is an integer multiple of $1/L$ and there are at most $W\cdot L$ many different values for $\operatorname{pexpcost}$ . This in particular applies to the value of the $\operatorname{pexpcost}$ -optimal $p$ -cause.

Note that there are still exponentially many possible values for the minimal partial expected costs in both Markov chains $N_{i}$ . A binary search over all possible values with polynomially many applications of the threshold problem:

Is $\operatorname{pexpcost}^{\min}\leq\vartheta$ for a rational $\vartheta\in\mathbb{Q}$ ?

is possible, nevertheless. We therefore can apply this binary search to find the exact value $\operatorname{pexpcost}_{N_{i}}(\Pi)$ for both DTMCs $N_{i}(i=0,1)$ by solving polynomially many instances of the threshold problem. This gives us a polynomial Turing reduction to the problem stated in [24]. ∎

\maxcostSummary

Proof

We start with some preliminary considerations. If there exists a path $s_{0}\ldots s_{n}$ entirely contained in $S\backslash S_{p}$ containing a cycle with positive weight, then $\operatorname{maxcost}$ of any $p$ -cause is $\infty$ : Consider a such a positive cycle reachable in $S\backslash S_{p}$ . Then there are paths in $\lozenge\mathit{error}$ which contain this cycle arbitrarily often. For any $p$ -cause $\Pi$ almost all of these paths need a prefix in $\Pi$ . Since no state in the positive cycle nor in the path from $s_{0}$ to the cycle is in $S_{p}$ , such prefixes also contain the cycle arbitrarily often. This means these prefixes accumulate the positive weight of the cycle arbitrarily often. Therefore, all $p$ -causes contain paths with arbitrary high weight. Thus, before optimizing $\Pi$ we check whether there are positive cycles reachable in the induced graph of $M$ on $S\backslash S_{p}$ . This can be done in polynomial time with the Bellman-Ford algorithm [12]. Henceforth we assume there are no such positive cycles.

For (1) we show that for two $p$ -causes $\Pi,\Phi$ with $\Pi\preceq\Phi$ we have $\operatorname{maxcost}(\Pi)\leq\operatorname{maxcost}(\Phi)$ . Let $\hat{\pi}\in\Pi$ be arbitrary. Since $\hat{\pi}$ is a $p$ -critical prefix (and $p>0$ ), there is a path $\pi\in\operatorname{Paths}_{M}(\mathcal{L})$ with $\hat{\pi}\in\operatorname{Pref}(\pi)$ . Since $\Phi$ is a $p$ -cause, there exists $\hat{\varphi}\in\Phi\cap\operatorname{Pref}(\pi)$ . The assumption $\Pi\preceq\Phi$ and the fact that both $\Pi$ and $\Phi$ are prefix-free then force $\hat{\pi}$ to be a prefix of $\hat{\varphi}$ . Hence $c(\hat{\pi})\leq c(\hat{\varphi})$ , and since $\hat{\pi}$ was arbitrary, it follows that $\operatorname{maxcost}(\Pi)\leq\operatorname{maxcost}(\Phi)$ . This implies that $\Theta$ is $\operatorname{maxcost}$ -minimal.

Computing $\operatorname{maxcost}^{\min}=\operatorname{maxcost}(\Theta)$ for a non-negative weight function can be reduced to the computation of the longest path in a modified version of $M$ . There can be cycles with weight $0$ in $S\backslash S_{p}$ , but in such cycles every state in the cycle has weight $0$ . Therefore we collapse such cycles completely without changing the value $\operatorname{maxcost}(\Theta)$ . We further collapse the set $S_{p}$ into one absorbing state $f$ . Computing $\operatorname{maxcost}(\Theta)$ now amounts to searching for a longest path from $s_{0}$ to $f$ in this modified weighted directed acyclic graph. This can be done in linear time by finding a shortest path after multiplying all weights with $-1$ . Therefore the problem can be solved in overall polynomial time [12].

For (2) we reduce the problem of finding a $\operatorname{maxcost}$ -minimal $p$ -cause to the solution of a max-cost reachability game as defined in [6]. Define the game arena $\mathcal{A}=(V,V_{Max},V_{Min},E)$ with

\displaystyle V=S\>\dot{\cup}\>\dot{S}_{p},

\displaystyle V_{Max}=S,

\displaystyle V_{Min}=\dot{S}_{p},

where $\dot{S}_{p}$ is a copy of $S_{p}$ . The copy of state $s\in S_{p}$ in $\dot{S}_{p}$ will be written as $\dot{s}$ . There is an edge $(s,t)\in E$ between states $s$ and $t$ in $V$ if and only if one of the following conditions holds:

(1)

$s\in S,t\in S\backslash S_{p}$ , and $\mathbf{P}(s,t)>0$ ,
(2)

$s\in S,t\in\dot{S}_{p}$ , and for $u\in S_{p}$ with $t=\dot{u}$ we have $\mathbf{P}(s,u)>0$ ,
(3)

$s\in\dot{S}_{p},t\in S_{p}$ , and $s=\dot{t}$ , or
(4)

$s\in\dot{S}_{p}$ and $t=\mathit{error}$ .

We equip $\mathcal{A}$ with a weight function $w:V\to\mathbb{Q}$ by mirroring the weight function of $M$ in the following way:

(1)

$w(s)=c(s)$ for $s\in S\backslash S_{p}$ , and
(2)

$w(s)=0$ for $s\in S_{p}$ ,
(3)

$w(\dot{s})=c(s)$ for $s\in S_{p}$ ,

In [6] the authors define a min-cost reachability game. For our purposes we need the dual notion of a max-cost reachability game, which is obtained by just changing the total payoff of a play avoiding the target set to be $-\infty$ instead of $+\infty$ . The objective of player $Max$ with vertices $V_{Max}$ is then to maximize the total payoff of the play, while player $Min$ with vertices $V_{Min}$ wants to minimize the total payoff. By changing from min-cost to max-cost reachability games, the results of [6] concerning strategies for $Max$ and $Min$ are reversed.

We consider the max-cost reachability game on $\mathcal{A}$ with target $\mathit{error}$ . Define $Val(s)$ as the total payoff if both sides play optimally if the play starts in $s$ . We have $Val(s_{0})=\infty$ if there is a positive cycle reachable in $S\backslash S_{p}$ by the above argumentation. In contrast we always have $Val(s_{0})\neq-\infty$ since $\mathit{error}$ is reachable and $\mathit{safe}$ can be avoided by $Max$ . We proceed to show that our reduction is correct.

Claim

There is a $1$ - $1$ correspondence between strategies $\sigma$ of $Min$ and $p$ -causes in $M$ for $\lozenge\mathit{error}$ .

Proof (of the claim)

Let $\sigma$ be a strategy for $Min$ and consider the set of consistent plays starting in $s_{0}$ that we denote by $Plays_{s_{0}}(\mathcal{A},\sigma)$ . Every play $\pi\in Plays_{s_{0}}(\mathcal{A},\sigma)$ that reaches $\mathit{error}$ corresponds to a $p$ -critical prefix. To see this, omit all states contained in $\dot{S}_{p}$ from the play. If $\pi$ reaches $\mathit{error}$ and the last state before $\mathit{error}$ is in $\dot{S}_{p}$ then omit $\mathit{error}$ as well. The resulting path in $M$ is a $p$ -critical prefix. Let $\Pi\subseteq\operatorname{Paths}_{\operatorname{fin}}(M)$ be the set of $p$ -critical prefixes obtained in this way from plays in $Plays_{s_{0}}(\mathcal{A},\sigma)$ reaching $\mathit{error}$ .

To see that any path $\pi$ to $\mathit{error}$ in $M$ has a prefix in $\Pi$ , let $\tau$ be the strategy of player $Max$ that moves along the steps of $\pi$ . In the resulting play, either player $Min$ moves to $\mathit{error}$ from some state $s\in\dot{S}_{p}$ according to $\sigma$ and the corresponding prefix of $\pi$ is in $\Pi$ , or the play reaches $\mathit{error}$ from a state not in $\dot{S}_{p}$ and hence the path $\pi$ itself belongs to $\Pi$ . Since the strategy has to make decisions for every $s\in\dot{S}_{p}$ , every path $\pi\in\operatorname{Paths}_{M}(\lozenge\mathit{error})$ has a prefix in $\Pi$ . $\Pi$ is prefix-free since a violation of this property would correspond to a non-consistent play, since $Min$ can only choose the edge to $\mathit{error}$ once. Therefore $\Pi$ is a $p$ -cause in $M$ for $\lozenge\mathit{error}$ .

Since the reverse of this construction follows along completely analogous lines, we omit it here. $\blacksquare$

Claim

We have $\operatorname{maxcost}^{\min}=Val(s_{0})$ .

Proof (of the claim)

Recall that the value $Val(s_{0})$ is defined as the total payoff of the unique play $\pi\in Plays_{s_{0}}(\mathcal{A},\sigma)\cap Plays_{s_{0}}(\mathcal{A},\tau)$ , where $\sigma$ is the optimal strategy of $Min$ and $\tau$ is the optimal strategy of $Max$ . For each strategy $\sigma^{\prime}$ for $Min$ , let $\Pi_{\sigma^{\prime}}$ be the corresponding $p$ -cause as provided by the above claim. The optimal strategy $\tau^{\prime}$ for $Max$ against $\sigma^{\prime}$ has to avoid $\mathit{safe}$ and hence has to create a play that ends in $\mathit{error}$ . The total payoff of the induced play $\varphi$ is equal to the weight of the corresponding path $\hat{\varphi}\in\Pi_{\sigma^{\prime}}$ and the total payoff that $Max$ can achieve is precisely $\operatorname{maxcost}(\Pi_{\sigma^{\prime}})$ . The optimal strategy $\sigma$ for $Min$ hence corresponds to a $\operatorname{maxcost}$ -minimal $p$ -cause $\Pi_{\sigma}$ and $\operatorname{maxcost}(\Pi_{\sigma})=Val(s_{0})$ . $\blacksquare$

Now we apply the results for max-cost reachability games to $p$ -causes. This means we can use [6, Algorithm 1] to compute the value $Val(s)$ of the game for all states $s\in S$ in pseudo-polynomial time. This includes the value $Val(s_{0})=\operatorname{maxcost}^{\min}$ . From the values of the game starting at different states, an optimal memoryless strategy $\sigma$ for $Min$ can be derived by fixing a successor $s^{\prime}$ for each state $s\in V_{Min}$ with $(s,s^{\prime})\in E$ and

Val(s)=c(s^{\prime})+Val(s^{\prime}).

Since the strategy is memoryless, we get a set $Q\subseteq\dot{S}_{p}$ for which $Min$ chooses the edge to $\mathit{error}$ . By the construction from before the $\operatorname{maxcost}$ -minimal $p$ -cause $\Pi$ obtained in this way is state-based.

For (3) we note that the decision problem “Is $Val(s_{0})\leq 0$ ?” is in $\mathtt{NP}\cap\mathtt{coNP}$ by a reduction to mean-payoff games, as shown in [8]. The reduction introduces an edge from $\mathit{error}$ back to $s_{0}$ and removes the state $\mathit{safe}$ from the game. We have that $Val(s_{0})\leq 0$ in the original max-cost reachability game if and only if the value of the constructed mean-payoff game is at most $0$ . The reason is that the value of the mean-payoff game is at most $0$ if there is a strategy for $Min$ such that $Max$ can neither force a positive cycle in the original max-cost reachability game nor reach $\mathit{error}$ with positive weight in the original game. We adapt the construction to show that the decision problem “is $\operatorname{maxcost}^{\min}\leq\vartheta$ ?”, for $\vartheta\in\mathbb{Q}$ , is also in $\mathtt{NP}\cap\mathtt{coNP}$ . This can be achieved by adding an additional vertex $s$ with weight $-\vartheta$ to $V_{Max}$ , removing the edge between $\mathit{error}$ and $s_{0}$ and adding two new edges, one from $\mathit{error}$ to $s$ and one from $s$ to $s_{0}$ . The value of the resulting mean-payoff game is then at most $0$ if there is a strategy for $Min$ such that $Max$ can neither force a positive cycle in the original max-cost reachability game nor reach $\mathit{error}$ with weight above $\vartheta$ in the original game. ∎

\instcost

Proof

Recall that we now work with a set of error states $E$ instead of a single state $\mathit{error}$ and a set of terminal safe states $F$ such that $\mathrm{Pr}_{f}(\Diamond E)=0$ if and only if $f\in F$ . We first note that for an instantaneous weight function we reduce partial expected cost to expected cost and therefore only need to consider one case: Given a weight function $c\colon S\to\mathbb{Q}$ , consider the weight function $c^{\prime}$ obtained from $c$ by forcing $c^{\prime}(f)=0$ for all $f\in F$ . Then the partial expected cost with respect to $c_{\operatorname{inst}}$ equals the expected cost with respect to $c^{\prime}_{\operatorname{inst}}$ .

For $\operatorname{expcost}_{\operatorname{inst}}$ we construct an MDP $\mathcal{N}=(S\>\dot{\cup}\>\dot{S}_{p},\{pick,continue\},s_{0},\mathbf{P}^{\prime})$ , where $\dot{S}_{p},$ is a disjoint copy of $S_{p}$ in which all states are terminal. The copy of state $s\in S_{p}$ in $\dot{S}_{p}$ will be written as $\dot{s}$ . We define $\mathbf{P}^{\prime}(s,continue,s^{\prime})=\mathbf{P}(s,s^{\prime})$ for $s,s^{\prime}\in S$ , and $\mathbf{P}^{\prime}(s,pick,\dot{s})=1$ for $s\in S_{p}$ . The action $pick$ is not enabled states outside of $S_{p}$ , and the action $continue$ is not enabled in $\dot{S}_{p}$ . We define the weight function $c_{\mathcal{N}}:S\>\dot{\cup}\>\dot{S}_{p}\to\mathbb{Q}$ by

c_{\mathcal{N}}(s)=\begin{cases}c(s)&\text{if }s\in F\cup E\\ c(t)&\text{if $s\in\dot{S}_{p}$ and $\dot{t}=s$}\\ 0&\text{else.}\end{cases}

The construction is illustrated in Figures 9 and 9: Consider the DTMC $M^{\prime}$ depicted in Figure 9. The transition probabilities are omitted. It is enough to know $S_{p}^{\prime}=\{s_{0},s_{1}\}$ and $F^{\prime}=\{\mathit{safe}\}$ . The constructed MDP $\mathcal{N}^{\prime}$ can be seen in Figure 9, where the black edges are inherited from $M^{\prime}$ , and the red edges are added transitions belonging to the action $pick$ .

Figure 8: The DTMC

M^{\prime}

with instantaneous weight

Figure 9: The MDP

\mathcal{N}^{\prime}

emulating instantaneous weight

For the constructed MDP $\mathcal{N}$ we consider the accumulated weight function. This emulates an instantaneous weight function for the random variable $\mathcal{X}_{c}$ of $\operatorname{expcost}_{\operatorname{inst}}$ . A scheduler of this MDP corresponds to a $p$ -cause for $M$ in the same way as established in Lemma 1. Therefore the problem of finding an $\operatorname{expcost}$ -minimal $p$ -cause for instantaneous weight $c:S\to\mathbb{Q}$ in $M$ for $\lozenge E$ is equivalent to finding a cost-minimal scheduler in $\mathcal{N}$ for $\lozenge E\cup F\cup\dot{S}_{p}$ . This is again the stochastic shortest path problem for $\mathcal{N}$ , which can be solved in polynomial time by [4]. Since the SSP is solved by a memoryless scheduler, the $\operatorname{expcost}_{\operatorname{inst}}$ -minimal $p$ -cause is state-based.

For the computation of the minimal value of $\operatorname{maxcost}_{\operatorname{inst}}$ , we enumerate the set $S_{p}$ as $s^{0},\dots,s^{k}$ where $k=|S_{p}|-1$ such that $c(s^{i})\leq c(s^{j})$ for all $0\leq i<j\leq k$ . Now we iteratively remove states in increasing order starting with $s^{0}$ . After removing a state $s^{i}$ , we check whether $E$ is reachable in the resulting Markov chain. If this is the case, we continue by removing the next state. If $E$ is not reachable anymore, the set $S^{i}:=\{s^{0},\dots,s^{i}\}$ induces a state-based $p$ -cause $\Pi_{S^{i}}$ . This follows from the fact that each path from the initial state to $E$ contains a state in $S^{i}$ and that $S^{i}\subseteq S_{p}$ . Furthermore, $\operatorname{maxcost}_{\operatorname{inst}}(\Pi_{S^{i}})\leq c(s^{i})$ . Let $j$ be the largest number less than $i$ such that $c(s^{j})<c(s^{i})$ . There is no $p$ -cause in which all paths end in $\{s^{0},\dots,s^{j}\}$ as $E$ was still reachable after removing these states from $M$ . So, there is no $p$ -cause $\Pi$ with $\operatorname{maxcost}_{\operatorname{inst}}(\Pi)<c(s^{i})$ . Therefore, $\Pi_{S^{i}}$ is indeed a $\operatorname{maxcost}_{\operatorname{inst}}$ -minimal $p$ -cause. Since $E\subseteq S_{p}$ , the procedure terminates at the latest when the states in $E$ are removed. Hence the algorithm finds a state-based $\operatorname{maxcost}_{\operatorname{inst}}$ -minimal $p$ -cause in polynomial time. ∎

Probabilistic causes in Markov chains

Abstract

1 Introduction

1.0.1 Related Work.

2 Preliminaries

2.0.1 Markov chains.

2.0.2 Markov decision processes.

3 Causes

Definition 1 (pp-critical prefix)

Definition 2 (pp-cause)

Example 1

Example 2

Remark 1 (Reduction to reachability properties)

Definition 3 (pp-causal MDP)

Example 3

Lemma 1

Proof

3.1 Types of pp-causes and induced monitors

Definition 4 (State-based pp-cause)

Definition 5 (Threshold-based pp-cause)

3.2 Comparison to prima facie causes

Definition 6 (cf. [34])

Lemma 2

Proof

4 Costs of pp-causes

4.1 Expected cost of a pp-cause

Definition 7 (Expected cost)

Proof

4.2 Partial expected cost of a pp-cause

Definition 8 (Partial expected cost)

Example 4

Proof

Proof

4.3 Maximal cost of a pp-cause

Definition 9 (Maximal cost)

Proof

4.4 Instantaneous cost

Proof

5 Conclusion

References

6 Appendix

Proof

Proof

Proof

Proof

Proof

Claim

Proof (of the claim)

Claim

Proof (of the claim)

Proof

Definition 1 ( $p$ -critical prefix)

Definition 2 ( $p$ -cause)

Definition 3 ( $p$ -causal MDP)

3.1 Types of $p$ -causes and induced monitors

Definition 4 (State-based $p$ -cause)

Definition 5 (Threshold-based $p$ -cause)

4 Costs of $p$ -causes

4.1 Expected cost of a $p$ -cause

4.2 Partial expected cost of a $p$ -cause

4.3 Maximal cost of a $p$ -cause