Probabilistic causes in Markov chains

As cyber-physical systems grow ever more prevalent in our everyday lives, they also become increasingly complex. The need and desire to explain the behavior of such systems has sparked a branch of research, which tries to explain and explicate the substantial complexity of modern systems. One of the key principles which can lead to the understanding of formal systems are cause–effect relationships. The study of such relations in formal systems has received great interest over the past 25 years. Notions of causality have been proposed within a variety of models, such as structural equation models [30, 31, 43], Kripke structures [6, 14] and Markov chains [39, 40]. All of these investigations share a similar goal as they build a framework which tries to enable an explanation of why an observable phenomenon (the effect) has happened by logically linking previous events (the causes) to its occurrence. An understanding of such cause–effect relationships has been identified to be helpful in a variety of application areas ranging from finance [37] to medicine [38] and aeronautics [34], among others. Furthermore, in a societal context, causality plays a fundamental role in determining moral responsibility [8, 13] or legal accountability [24], and ultimately fosters user acceptance through an increased level of transparency [42].

Even though causality has been considered in various disciplines and within different application contexts, almost all approaches use at least one of the following two central paradigms to describe the logical link between causes and effect: The notion of causality introduced in this paper uses both of these paradigms: Given a probability threshold \(p\in (0,1]\), a p-cause for an \(\omega \)-regular effect \(\mathcal {L}\) in a discrete-time Markov chain is defined to be a set of finite executions \(\Pi \) such that

Condition (i) captures the probability-raising property if p is chosen to be greater than the overall probability that \(\mathcal {L}\) is observed, while (ii) is in line with counterfactual reasoning. Note that the effects are sets of infinite executions while causes are sets of finite executions preceding the effects. Nevertheless, it is of course possible that after some finite execution in a cause, it is already clear that the effect will (almost) surely be observed.

The precise meaning of execution depends on the setting. In the fully observable case, an observer has access to the system states themselves and thus an execution is a path in the Markov chain. In these settings we thus consider path-based p-causes (henceforth called p-causes). However, in settings without full introspection of the state space, only partial information about the current state can be observed. This can be modeled by labels on the states, where states with the same label are not distinguishable. In such a case an execution is represented by a trace (a sequence of labels) in the Markov chain and the corresponding p-causes are trace-based (henceforth called trace-p-cause).

By combining conditions (i) and (ii) the resulting notion is useful when causes are used for monitoring purposes. Imagine a critical event which the system should avoid (e.g., a fully automated drone crashing onto the ground). After a p-cause has been computed for this event, it can be used as a monitor that can trigger an alarm as soon as the execution so far is an element in the cause. Depending on the system and the threshold p the alarm is raised before the critical event occurs and thus suitable countermeasures can be taken (e.g., manual control instead of automated behavior). The probability threshold p can be thought of as the sensitivity of the monitor and can be adjusted depending on the criticality of the effect.

As multiple p-causes might exist for the same effect, the application described above motivates the question, which p-cause should be computed or used. Typically, one wants to minimize the resource consumption of the modeled system. Resources, such as time or energy, might be consumed by the system or the induced monitor, but also by the countermeasures taken upon triggering an alarm. The cost of countermeasures may depend on the state of the system or the execution until the alarm. Such costs can be modeled 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 resource consumption intensity) fashion. To be able to model the different types of costs one might be interested in, we consider three cost mechanisms for causes: Within a possible monitoring application the expected cost describes the expected resource consumption until the monitor triggers an alarm or reaches a safe state, whereas the partial expected cost can be used to model the costs of countermeasures that are only incurred if an execution in the cause is observed. In this context, the maximal cost measures the maximal possible resource consumption when an alarm is triggered.

In the setting of full observability of the state space where p-causes consist of finite paths, we obtain the complexity results presented in Table 1 for the computation of cost-minimal p-causes for different combinations of weight types and cost mechanisms if the effect \(\mathcal {L}\) is a reachability property. The case of arbitrary \(\omega \)-regular effects \(\mathcal {L}\) can be reduced to this case in polynomial time if \(\mathcal {L}\) is given by a deterministic Rabin automaton. In order to obtain the complexity results, we exploit connections to several computational problems for discrete-time Markovian models. For the expected cost we rely on reductions to the stochastic shortest path problem (SSP) studied in [7]. The exponential-time algorithm for partial expected costs on non-negative, accumulated weights uses results on partial expectations in Markov decision processes [44]. We obtain \(\mathtt {PP}\)-hardness for partial expected cost by a reduction from the cost problem for acyclic Markov chains stated in [28]. The pseudo-polynomial algorithm for the maximal cost on arbitrary, accumulated weights applies insights from total-payoff games [9, 12].

In the setting of partial observability, additional complications arise. For labeled Markov chains, we consider trace-p-causes, which consist of traces which incorporate the probability-raising principle for every underlying path. This approach is in line with notions of causality studied by Kleinberg et al. (see, e.g., [39]). In contrast to the full observable setting, trace-p-causes need not exist for arbitrary \(\omega \)-regular effects. We show that deciding the existence of a trace-p-cause is PSPACE-hard and can be done in exponential time. Furthermore, a few results about cost-minimal p-causes can be transferred with an exponential overhead in runtime: Namely, the results for the expected and maximal cost in case of non-negative weights and the algorithm for maximal cost for an instantaneous weight function. For the remaining combinations of weight types and cost mechanisms, analogous reductions to the results for p-causes lead to problem instances (mainly on partially observable MDPs) which are known to be undecidable in general or for which there are no known results in the literature. Whether the special form of these instances we obtain can be exploited to obtain further decidability results remains open.

Related Work Halpern and Pearl introduced a structural model approach to actual causality [31] which has sparked notions of causality in formal verification [6, 14]. The complexity of computing actual causes has been studied in [20, 21]. A probabilistic extension of this framework has been proposed in [25]. Recent work on checking and inferring actual causes is given in [33], and an application-oriented framework for it is presented in [34]. In another account, Kleinberg et al. [39] build a framework for actual causality in Markov chains and use it to infer causal relationships in data sets. This approach was later extended to continuous time data [37] and to token causality [40] and has been refined using new significance measures for actual and token causes [32, 52]. The survey article [1] introduces causes in probabilistic operational models by incorporating temporal priority and probability-raising in a state-based fashion. The extension of this approach to local and global probability-raising conditions as path properties is then compared to the PCTL approach of [39]. In [3] the probability-raising principle is incorporated in a causality notion for Markov decision processes and the coverage properties of causes are optimized by using quality measures.

In combination with logical programming, a logic for probabilistic causal reasoning is given in [51]. The subsequent work [50] compares this approach to Pearl’s theory of causality involving Bayesian networks [43]. The CP-logic of [51] is close to the representation of causal mechanisms of [18]. On the philosophical side, the probability-raising principle goes back to Reichenbach [45] and has been identified as a key ingredient to causality in various philosophical accounts, see e.g., [19, 48].

In stochastic systems modeled as Hidden Markov chains (HMCs) \(\omega \)-regular properties were studied in [27, 46] in a monitoring context. This approach to monitoring has recently been revived in [22]. In a similar context the trade-off between accuracy and overhead in runtime verification has been studied in [5, 35, 47]. In particular, [5] uses HMCs to estimate how likely the violation of a property is in the near future while monitoring a system. Monitoring the evolution of finite executions has also been investigated in the context of statistical model checking of LTL properties [17]. How randomization can improve monitors for non-probabilistic systems has been examined in [10]. The safety level of [23] measures which portion of a language admits bad prefixes, in the sense classically used for safety languages.

Contribution This paper contributes novel notions of causes for \(\omega \)-regular effects in stochastic operational models: In the setting of full introspection of the state space, p-causes are defined as sets of finite paths (Sect. 3). While the existence of such p-causes is always guaranteed, the paper considers various ways of assigning costs to a cause (Sect. 4). The cost mechanisms correspond to different kinds of resource consumption which may occur when applying p-causes, inspired by use-cases from the monitoring domain. The computational complexity of computing cost-minimal causes under these cost mechanisms is thoroughly developed. Finally, we extend the causality notion to partial observable models by introducing trace-p-causes (Sect. 5). While some of our methods for p-causes can be extended to trace-p-causes, we show that partial observability leads to additional computational difficulties in general.

This paper is an extended version of work published in the ATVA 2021 conference [2]. It extends the previous work by addressing partial observability in Sect. 5 and by providing the full proofs omitted in the conference version.

Markov chains A discrete-time Markov chain (DTMC) M is a tuple \((S, s_0, {\textbf {P}})\), where S is a finite set of states, \(s_0\in S\) is the initial state, and \({\textbf {P}} :S \times S \rightarrow [0,1]\) is the transition probability function where we require \(\sum _{s' \in S} {\textbf {P}}(s, s') = 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_0s_1\ldots s_n\) of states such that \({\textbf {P}}(s_i, s_{i+1}) > 0\) for all \(0 \le i \le n-1\). Let \({\text {last}}(s_0\ldots s_n) = s_n\). Similarly one defines the notion of an infinite path \(\pi \). Let \({\text {Paths}}_{{\text {fin}}}(M)\) and \({\text {Paths}}(M)\) be the set of finite and infinite paths. The set of prefixes of a path \(\pi \) is denoted by \({\text {Pref}}(\pi )\). The cylinder set of a finite path \({\hat{\pi }}\) is \({\text {Cyl}}({\hat{\pi }}) =\{\pi \in \ {\text {Paths}}(M)\mid {\hat{\pi }}\in {\text {Pref}}(\pi )\}.\) We consider \({\text {Paths}}(M)\) as a probability space whose \(\sigma \)-algebra is generated by such cylinder sets and whose probability measure is induced by \(\text {Pr}({\text {Cyl}}(s_0\ldots s_n)) = {\textbf {P}}(s_0, s_{1})\cdot \ldots \cdot {\textbf {P}}(s_{n-1}, s_n) \) (see [4, Chapter 10] for more details).

For an \(\omega \)-regular language \(\mathcal {L} \subseteq S^{\omega }\) let \({\text {Paths}}_M(\mathcal {L}) = {\text {Paths}}(M) \cap \mathcal {L}\). The probability of \(\mathcal {L}\) in M is defined as \(\text {Pr}_M(\mathcal {L}) = \text {Pr}({\text {Paths}}_M(\mathcal {L}))\). Given a state \(s\in S\), let \(\text {Pr}_{M,s}(\mathcal {L}) = \text {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 {\text {Paths}}_{{\text {fin}}}(M)\), define the conditional probabilityGiven \(E \subseteq S\), let \(\lozenge E = \{ s_0s_1\ldots \in {\text {Paths}}(M)\mid \exists i \ge 0. \; s_i\in E\}\). For such reachability properties we have \(\text {Pr}_{M}(\lozenge E \mid s_0\ldots s_n) = \text {Pr}_{M, s_n}(\lozenge E)\) for any \(s_0\ldots s_n\in {\text {Paths}}_{{\text {fin}}}(M)\). We assume \(\text {Pr}_{M,s_0}(\lozenge s) > 0\) for all states \(s \in S\). Furthermore, define a weight function on M as a map \(c: S \rightarrow \mathbb {Q}\). We typically use it to induce a weight function \(c: {\text {Paths}}_{{\text {fin}}}(M) \rightarrow \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 {\text {Paths}}_{{\text {fin}}}(M)\) is called prefix-free if for every \({\hat{\pi }}\in \Pi \) we have \(\Pi \cap {\text {Pref}}({\hat{\pi }}) = \{{\hat{\pi }}\}\).

A labeled DTMC \(\mathcal {M} = (S,s_0,{\textbf {P}},\Sigma ,L)\) is a DTMC equipped with a labeling function \(L: S \rightarrow \Sigma \) that assigns each state \(s \in S\) a label \(L(s) \in \Sigma \). A finite trace \({\hat{\tau }}\) in \(\mathcal {M}\) is a sequence \(L(s_0)L(s_1) \ldots L(s_n)\) of labels such that there exists a corresponding finite path \({\hat{\pi }} = s_0 s_1 \ldots s_n \in {\text {Paths}}_{{\text {fin}}}(\mathcal {M})\) The set of all corresponding paths to \({\hat{\tau }}\) in \(\mathcal {M}\) is denoted by \({\text {Paths}}_{\mathcal {M}}({\hat{\tau }})\). The notion of an infinite trace \(\tau \) is defined in a similar manner. \({\text {Traces}}(\mathcal {M})\) can be considered as a probability space whose \(\sigma \)-algebra is, analogously to the non-labeled case, induced by the cylinder sets of finite traces. The probability of an \(\omega \)-regular language \(\mathcal {L} \subseteq \Sigma ^\omega \) is given by \(\Pr _{\mathcal {M}}(\mathcal {L})=\Pr _{\mathcal {M}}(\mathcal {L} \cap {\text {Traces}}(\mathcal {M}))\). A weight function can also be defined over labels, i.e., \(c:\Sigma \rightarrow \mathbb {Q}\), which in turn induces a weight function on finite traces \(c: {\text {Traces}}_{{\text {fin}}}(\mathcal {M}) \rightarrow \mathbb {Q}\).

Markov decision processes A Markov decision process (MDP) \(\mathcal {M}\) is a tuple \((S, {\text {Act}}, s_0, {\textbf {P}})\), where S is a finite set of states, \({\text {Act}}\) is a finite set of actions, \(s_0\) is the initial state, and \({\textbf {P}} :S \times {\text {Act}} \times S \rightarrow [0,1]\) is the transition probability function such that for all states \(s \in S\) and actions \(\alpha \in {\text {Act}}\) we have \(\sum _{s' \in S} {\textbf {P}}(s, \alpha ,s') \in \{0,1 \}\). An action \(\alpha \) is enabled in state \(s \in S\) if \(\sum _{s' \in S} {\textbf {P}}(s, \alpha ,s')=1\) and we define \({\text {Act}}(s) = \{\alpha \mid \alpha \text { is enabled in } s\}\). We require \({\text {Act}}(s) \ne \emptyset \) for all states \(s \in S\).

An infinite path in \(\mathcal {M}\) is an infinite sequence \(\pi =s_0 \alpha _1s_1 \alpha _2s_2 \dots \in (S \times {\text {Act}})^\omega \) such that for all \(i \ge 0\) we have \({\textbf {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 _1s_1 \dots s_n\) to an enabled action \(\alpha \in {\text {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 _1s_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 [4].

Nondeterministic finite automata 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 set of initial states, \(T:Q\times \Sigma \rightarrow 2^Q\) is the transition function, and \(F\subseteq Q\) are the final states. A transition \(q'\in T(q,\alpha )\) is also denoted by \(q\overset{\alpha }{\mapsto } q'\).

Deterministic Rabin automata A deterministic Rabin automaton (DRA) is a tuple \(\mathcal {A} = (Q, \Sigma , q_0, \delta , \text {Acc})\) where Q is a finite set of states, \(\Sigma \) an alphabet, \(q_0\) the initial state, \(\delta : Q \times \Sigma \rightarrow Q\) the transition function and \(\text {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 \text {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.

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 = (S, s_0, {\textbf {P}})\), an \(\omega \)-regular language \(\mathcal {L}\) over the alphabet S and a threshold \(p \in (0,1]\).

Note that condition (1) and (2) are in the spirit of completeness and soundness as used, e.g., in [15]. The first condition is our invocation of the counterfactual reasoning principle: Almost every occurrence of the effect is preceded by an element in the cause. If the threshold is chosen such that \( p > \text {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 after the execution so far.

In particular, for monitoring purposes as described in the introduction it would be misleading to choose p below \(\text {Pr}_{s_0}(\mathcal {L})\) as this could instantly trigger an alarm before the system is put to use. On the other hand p should not be too close to 1 as this may result in an alarm being triggered too late. This can also lead to a non-classical cause–effect relation as \(\text {Pr}(\mathcal {L} \mid {\hat{\pi }}) = 1\) for a finite path \({\hat{\pi }}\) might also imply, that the effect has already occurred. Thus, a careful choice of the probability threshold p depending on the modeled system and application is crucial. Also note, that the probability might only be raised after the execution but not along the execution. For example, there might be paths \({\hat{\pi }} = s_0 s_1 \cdots s_n \in \Pi \) such that \(\text {Pr}_{s_i}(\mathcal {L}) \le \text {Pr}_{s_0}(\mathcal {L})\) for all \(i < n\) but \(\text {Pr}_{s_n}(\mathcal {L}) > p\).

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.

Remark 5 motivates us to focus on reachability properties henceforth. To apply the algorithms presented in Sect. 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.

In order to align the exposition with a possible monitoring application, we will consider the target set as representing an erroneous behavior that should be avoided. After collapsing the target set, we may assume that there is a unique state \( fail \in S\) such that \(\mathcal {L} = \lozenge fail \) is the language we are interested in. Further, we collapse all states from which \( fail \) is not reachable to a unique state \( safe \in S\) with the property \(\text {Pr}_{ safe }(\lozenge fail )=0\). After pre-processing, we then have \(\text {Pr}_{s_0}(\lozenge \{ fail , safe \}) = 1\). We define the setof acceptable final states for p-critical prefixes. This set is never empty as \( fail \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 {\text {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 threshold p. In fact, for two p-causes \(\Pi , \Phi \) with \(\Pi \preceq \Phi \) and \(\pi \in \Pi , \phi \in \Phi \) it might happen that \(\text {Pr}(\lozenge fail \mid \pi ) \ge \text {Pr}(\lozenge fail \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 Sect. 4.

We now introduce an MDP associated with M whose schedulers correspond to the p-causes of \(\lozenge fail \) in M. This MDP is useful both as a representation for p-causes and for algorithmic questions we consider later.

Technically, schedulers are defined on all finite paths of an MDP \(\mathcal {M}\). However, for given a scheduler \(\mathfrak {S}\), there might be paths which cannot be obtained under \(\mathfrak {S}\). Thus we define an equivalence relation \(\equiv \) on the set of schedulers of \(\mathcal {M}\) by setting two schedulers \(\mathfrak {S}\) and \(\mathfrak {S}'\) equivalent, i.e., \(\mathfrak {S} \equiv \mathfrak {S}'\), if \({\text {Paths}}(\mathcal {M}_{\mathfrak {S}})={\text {Paths}}(\mathcal {M}_{\mathfrak {S}'})\). Note that two schedulers equivalent under \(\equiv \) behave identically.

In this section we fix a DTMC M with state space S, unique initial state \(s_0\), unique target and safe state \( fail , 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:S \rightarrow \mathbb {Q}\) on states and consider the induced accumulated weight function on finite paths \(c:{\text {Paths}}_{{\text {fin}}}(M)\rightarrow \mathbb {Q}\). These weights typically represent resources spent, e.g., energy, time, material, etc. Naturally one would like to optimize resource consumption either by minimizing the expected resource consumption or by staying below a certain threshold. In this section we will introduce various measures for resource consumption applicable in different scenarios and analyze the complexity of computing optimal p-causes.

The definition of p-causes discussed so far works on the level of paths of a DTMC. Implicitly, it hence makes the assumption that the states of the DTMC themselves are observable. In this section, we want to discuss a generalization in which the system is not fully observable. This can be modeled by adding a labeling function which assigns to each state in the Markov chain a label from a finite alphabet \(\Sigma \). Instead of paths through the state space, only the traces of these paths, i.e., the sequences of labels encountered can be observed.

Such a consideration makes sense in applications where there is no full introspection into the system but there is only partial information about the system state that can be gathered. For example, in the discussed monitoring application for p-causes, a critical event should be avoided (e.g., a drone crashing), but full information on the system state might not be available, e.g., only sensor readings of the drone might be observable instead of a fully specified state. Then, a cause for such an event should also be expressed in terms of these possible observations, e.g., in terms of sensor readings foreshadowing the crash. For this section, we work with a labeled DTMC \(\mathcal {M}=(S,s_0,{\textbf {P}},\Sigma ,L)\), an \(\omega \)-regular language \(\mathcal {L} \subseteq \Sigma ^\omega \), and a probability threshold \(p \in (0,1]\).

With this definition of p-critical trace, we incorporated the probability-raising property in a strict sense, as we require that every underlying path raises the probability of \(\mathcal {L}\) above the specified value p. Such a strict interpretation of causes is in line with investigations of causality in operational models by Kleinberg et al. [32, 37, 39, 40, 52] where the probability-raising property is required for each element of a cause. For example, causes as defined in [39] are given by a set of states represented using a PCTL-formula, such that each included state raises the probability of the effect (see Sect. 3.2 for a more detailed comparison). A more detailed discussion of the correspondence between the notion of causality by Kleinberg et al. and trace- and path-based notions of causality can be found in [1].

In this paper we make a first step toward an understanding of trace-based causality by considering this strict view on the probability-raising principle. We show that some of the techniques developed for path-based p-causes can be applied in this setting of strict trace-p-causes. However, we also show that several new phenomena arise here. For example, strict trace-based p-causes may not exist at all (see Example 29). Another natural definition would be to take a global view and require that, for each trace in the cause, the conditional probability of the effect, given the finite prefix trace, is above p. For a treatment of this global definition, however, the techniques developed in this paper appear not to be applicable directly and additional difficulties have to be expected.

Note that these definitions generalize the notion of (path-)p-cause: If each state in the DTMC \(\mathcal {M}\) has a unique label, paths and traces can be identified with each other and the definitions agree with the definitions from Sect. 3.

First, let us briefly consider the case where \(\mathcal {L}\) constitutes a reachability property. So, assume there is a set of labels \(G \subseteq \Sigma \) such that \(\mathcal {L} = \mathcal {L}(\lozenge G)\). In this case, any finite trace in \((\Sigma \setminus G)^{*} G\) is clearly p-critical for any \(p \in (0,1]\). This readily implies that trace-p-causes always exist for reachability properties. In the sequel, we will see that an NFA-representation of the canonical trace-p-cause consisting of the minimal p-critical traces can be computed in exponential time in this case (see Proposition 35).

In contrast to the fully observable case, the investigation of causes of arbitrary \(\omega \)-regular effects, however, cannot be reduced to the simpler case of reachability properties. In fact, trace-p-causes might not exist in general as the following example shows.

This observation leads to the decision problem: Given a labeled DTMC \(\mathcal {M}\), an \(\omega \)-regular language \(\mathcal {L}\) and a probability threshold \(p \in (0,1]\) decide the existence of a trace-p-cause for \(\mathcal {L}\) in \(\mathcal {M}\). Addressing this problem we use the following construction:

Intuitively, the second component of states in the belief construction keeps track of the states in which the DTMC \(\mathcal {M}\) could have ended up if another path with the same trace had been taken.

We assume we are given a DRA \(\mathcal {A}\) over \(\Sigma \) specifying the \(\omega \)-regular effect \(\mathcal {L}\). We work with the product DTMC \(\text {Bel}(\mathcal {M}) \otimes \mathcal {A}\) of the belief construction with the automaton. The acceptance condition of \(\mathcal {A}\) allows us to distinguish accepting and rejecting BSCCs in this DTMC. In analogy to before, let \(S_p\) be the set of states in \(\text {Bel}(\mathcal {M}) \otimes \mathcal {A}\) from which an accepting BSCC is reached with probability \(\ge p\).

For a state (s, T) in \(\text {Bel}(\mathcal {M})\) and a state q of the automaton \(\mathcal {A}\), we call the state (s, T, q) in \(\text {Bel}(\mathcal {M})\otimes \mathcal {A}\) p-critical if \((t,T,q) \in S_p\) for all \(t\in T\). In words, a state is p-critical if it is in \(S_p\) and would still be in \(S_p\) if so far another run with the same trace as a run reaching (s, T, q) had been taken. Note that any other such run ends up in the same state q as \(\mathcal {A}\) is deterministic. Let us denote the set of p-critical states in \(\text {Bel}(\mathcal {M})\otimes \mathcal {A}\) by \(\text {Crit}_p\). With this notation, we get following result.

A non-labeled DTMC can be seen as a special case of a labeled DTMC where every state has a unique label. Lemma 31 hence subsumes the result that p-causes exist for any p in non-labeled DTMCs: Applying the belief construction to a DTMC \(\mathcal {M}\) with unique labels for each state, all reachable states of \(\text {Bel}(\mathcal {M})\) take the form \((s,\{s\})\) where s is a state of \(\mathcal {M}\). So, the sets \(S_p\) and \(\text {Crit}_p\) coincide in this case. The reachable part of \(\text {Bel}(\mathcal {M})\) is furthermore isomorphic to \(\mathcal {M}\). After taking the product with a DRA \(\mathcal {A}\), we observe that all accepting BSCCs with states B satisfy \(B\subseteq \text {Crit}_1\subseteq \text {Crit}_p\) in this case as argued in Remark 5. Thus, the first condition of Lemma 31 always holds. In labeled DTMCs, the situation is more complicated and in particular, it is possible that only some or no states of an accepting BSCC in the product of the belief construction and an automaton belong to \(\text {Crit}_p\) as illustrated by the following example.

We can now employ Lemma 31, to check the existence of a trace-p-cause. An accompanying hardness result is presented afterwards in Proposition 34.

Finally, if a trace-p-cause exists, the belief construction can be used to compute a NFA-representation of the canonical trace-p-cause consisting of the minimal p-critical traces. Recall that we defined the prefix-order \(\preceq \) on p-causes which can be applied analogously to trace-p-causes in Sect. 3.

A p-causal partially observable MDP The MDP construction described in Definition 7 does roughly work the same way for a labeled DTMC \(\mathcal {M}\), but leads to a partially observable MDP (POMDP). In a partially observable MDP, in each step an observation from a set \(\mathcal {O}\) is made. A scheduler does not have access to the current state of the process, but only to the history of observations and has to choose actions based only on the sequence of observations observed.

The construction of the p-causal POMDP \(\mathcal {C}_p(\mathcal {M})\), the analogue of the p-causal MDP from Definition 7, works as follows: Given a labeled DTMC \(\mathcal {M}\) and a DRA \(\mathcal {A}\), we start with the DTMC \(\text {Bel}(\mathcal {M})\otimes \mathcal {A}\). In each state, the action continue is enabled and leads to successors according to the transition probabilities of \(\text {Bel}(\mathcal {M})\otimes \mathcal {A}\). Furthermore, we add a fresh absorbing state \( cause \). In each state in \(\text {Crit}_p\), a further action pick is enabled that leads to \( cause \) with probability 1. Whenever entering a state (s, T, q) of \(\text {Bel}(\mathcal {M})\otimes \mathcal {A}\), the scheduler observes only the label L(s), but not the exact state.

If a run leads to \(\text {Crit}_p\), also all other runs with the same trace end in \(\text {Crit}_p\). So, after any sequence of observations either pick is enabled after all runs corresponding to the observations or after none of these runs. Note that based on the observed labels, the scheduler knows the second two components of the current state (s, T, q), i.e., the subset T of states of \(\mathcal {M}\) the original DTMC could currently be in and the current state q of the automaton. The scheduler can, however, not distinguish states (s, T, q) and (t, T, q) with \(s,t\in T\).

Let now R be the set of all states in rejecting BSCCs of \(\text {Bel}(\mathcal {M})\otimes \mathcal {A}\). There is now a 1-to-1-correspondence between schedulers for \(\mathcal {C}_p(\mathcal {M})\) that reach \(R\cup \{ cause \}\) with probability 1 and trace-p-causes for \(\mathcal {L}(\mathcal {A})\) in \(\mathcal {M}\): Given such a scheduler \(\mathfrak {S}\), the set of traces, i.e., sequences of observations, that are possible under \(\mathfrak {S}\) and after which \(\mathfrak {S}\) chooses pick constitute a trace-p-cause. We have seen before that traces of paths ending in \(\text {Crit}_p\) are p-critical and almost all infinite traces on which \(\mathfrak {S}\) never chooses pick are traces of paths ending in a rejecting BSCC and hence do not belong to \(\mathcal {L}(\mathcal {A})\). In the other direction, given a trace-p-cause C, the scheduler that chooses pick whenever the trace seen so far lies in C clearly reaches \( cause \) or R almost surely.

However, many verification problems concerning general POMDPs are undecidable [11, 41]. In particular, reductions analogous to the ones used in the fully observable setting to solve cost-problems lead to problems on POMDPs which are undecidable in general as discussed in the following section.

The proposed definition of p-causes in DTMCs combines the counterfactual definition of causes with the probability-raising property. Motivated by monitoring applications, we considered various cost mechanisms that are suitable for different interpretations of the costs incurred by monitoring or by taking countermeasures in case an alarm is triggered. We provided algorithms for and investigated the computational complexity of the computation of corresponding cost-minimal causes. By considering a notion of p-causes in labeled DTMCs we took a first step in addressing causality in partial observable probabilistic systems.

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. For this, incorporating the probability-raising principle is relatively straight-forward but poses a lot of algorithmic questions regarding the check of the probability-raising condition and the optimization of causes. These problems are addressed in [3]. On the other hand, fitting the non-probabilistic counterfactual reasoning idea into a suitable definition for MDPs is more challenging and should be addressed in future work.