From Verification to Causality-based Explications

Modern software systems are increasingly complex and even small changes to a system or its environment may lead to unforeseen and disastrous behaviors. As software controls more aspects of our lives everyday, it is desirable—and for widespread acceptance in societal decisions, eventually inevitable—to have comprehensive and powerful techniques available to understand what a system does.

The field of formal methods has developed a portfolio of tools that provide confidence in the working of complex software systems. In formal methods, one builds a formal model of a system and specifies its desired behavior in an appropriate (temporal) logical formalism. Algorithmic techniques such as model checking [12, 31] can answer the question whether the model satisfies the specification, or in other words, whether the system behaves as intended, often in a “push button” way. Moreover, an important aspect of these algorithms is that they can produce independently verifiable justifications of their outcome, such as counterexamples or certificates to justify the violation or correctness of a property, respectively. Since the earliest successes of model checking, the availability of counterexample traces was stated as a major advantage for the method over deductive verification [30]. As model checkers became more complex, concerns about their correct implementation led to research on producing certificates for correctness. Examples are inductive invariants or derivations in a deductive system [62, 64, 44, 70] that can be checked independently from the verification process.

While certificates and counterexample traces can provide a useful explication about the behavior of a system, they only provide rudimentary understanding of why a system works the way it does. In epistemic terms, the outcome of model checking applied to a system and a specification provides knowledge that a system satisfies a specification or not in terms of an assertion (whether the system satisfies the specification) and a justification (certificate or counterexample) to increase the belief in the result. However, model checking usually does not provide understanding on why a system behaves in a certain way. Such an understanding can be obtained by causal links between possible events and their observed outcome.¹¹1Epistemologists since Gettier [47] will recognize that justified true belief does not constitute a comprehensive theory of knowledge. For the same reason, a theory of understanding as knowledge of causes is a matter of vigorous debate, with Gettier-like counterexamples [52, 100, 101]. These subtle epistemic issues are orthogonal to our work.

The need to better understand why a system is correct or incorrect has led to a broad research program on models and reasoning methods that aim to provide such knowledge of causes (see, e.g., [97, 98]). The goal of this survey is to summarize research on causal reasoning in the field of verification and highlight the challenges that lie ahead.

The first step in understanding knowledge of causes is the mathematical formulation and study of causality. Grasping the intuitive concept of cause-effect relationships in a formal model has proved notoriously difficult. Centuries of philosophical reasoning on the subject have distilled the counterfactuality principle [67, 68, 88] as a central feature of what constitutes an actual cause: if the cause had not occurred, then the effect would not have happened. While the counterfactuality principle was generally agreed upon, a rigorous mathematical formulation was developed only recently, through the seminal work of Halpern and Pearl and their coworkers [95, 45, 46, 55]. In a nutshell, they model causal systems using structural equation models, and provide a set of axioms to characterize when an event is an actual cause of another. We provide a summary of the foundations of causality and some of their applications in verification in Section 2.

While causality is a qualitative concept, in that an event is an actual cause of another or is not, more recent work considers quantitative measures of responsibility. Responsibility measures the relative importance that an event had in causing another event. In other words, the responsibility of an acting agent gauges what fraction of an observable effect can be attributed to that agent’s behavior. Here, an agent could be, e.g., an individual, a coalition, a software component, or device in a computer network. Chockler and Halpern [23] define the degree of responsibility of an actual cause in the Halpern-Pearl sense based on the cardinality of the smallest witness change that makes an event a cause of another. A more recent strand for formalizing responsibility is based on the Shapley value [106]. In cooperative game theory, the Shapley value measures the influence of an agent on the outcome jointly brought about by the agents and is classically used to find a fair division of a cost or a surplus among them. The appeal of the Shapley value stems on the one hand from its uniqueness with respect to a relatively simple set of axioms, and on the other hand from its seemingly universal applicability. Research on employing Shapley-like values for the explication of machine-learning predictions [117, 35, 91, 1, 110] and the behavior of formal models [119, 11, 93, 10] is currently very active. A summary of applications of Shapley values in the verification context is provided in Section 3.

From a systematic viewpoint, causality and responsibility can be understood in either a backward or a forward manner [113]. In the backward or ex post setting, an effect has already transpired, and the goal is to describe its causes and determine their relative influence in producing the effect. The actual causation framework by Halpern and Pearl follows this paradigm, and therefore also most approaches presented in Section 2. In the forward or ex ante setting, a reasoning model includes possible contingencies and the goal is to characterize the global power of agents and events in affecting the outcome. The forward responsibility in game structures (see Section 3.1) and the importance value for temporal logics (see Section 3.2) pursue this pattern. There are also attempts to express forward-looking causality notions by structural equations in the context of accountability [73]. Seen from an operational angle, the distinction between backward and forward notions loosely relates to when the causal analysis is executed. Backward notions tend to be applicable at inspection time, e.g., to guide the debugging process in post mortem analyses. Forward notions are prone to be used at design time of the system, laying out general phenomena of its inner workings.

Finally, we consider causality in the setting of probabilistic models. Unlike the deterministic setting, mathematical notions of causality and responsibility are less understood. There is widespread agreement in the philosophy literature that a quintessential characteristic of causes in the probabilistic setting is the probability-raising property [111, 21, 107, 39]: an occurrence of the cause should increase the probability of subsequently observing the effect. Nevertheless, it has also been observed that simply taking probabilities often leads to counterintuitive phenomena owing to mutual dependencies and latent correlations with other events [104, 21, 107]. Section 4 discusses attempts to formulate probability-raising approaches to causation for operational probabilistic models. These approaches tend to produce forward notions since probabilities inherently refer to a collection of evolutions in which an event happened. There are numerous philosophical accounts on actual probabilistic causation [89, 84, 42]. In terms of formal models, Pearl’s early notion of actual causality in terms of causal beams [96, 97] entailed probabilistic flavor, and the causal probabilistic logic of [115, 14] describes a language for reasoning about probabilistic causation. Nonetheless, we are aware of only a few works that study a probabilistic version of causality in operational models (see, e.g., [75, 2, 37, 9]). Along these lines, we point out open directions for research that focus on the operational point of view.

An important starting point for the study of causality in formal methods is the influential work by Halpern and Pearl [58, 59, 60, 56, 57] on actual causality, henceforth abbreviated HP causality. We provide a brief and informal overview of their definition.

Halpern and Pearl use structural equation systems as a modeling language for causal models. A causal model relies on exogeneous variables $U$ and endogeneous variables $V$, representing external or independent factors and internal factors, respectively. The value of each endogeneous variable $x\in V$ is specified by a deterministic function $f_{x}$ that may depend on exogeneous variables and on endogeneous variables that are preceding $x$ with respect to a fixed order on $V$. Intuitively, a causal model can be thought of as an arithmetic circuit whose primary inputs are the exogeneous variables and where some of whose internal nodes are labeled by the endogeneous variables. The circuit then specifies the functions defining the endogeneous variables as well as the dependencies between the variables.

More formally, let $M=(U,V,{\{f_{x}\}}_{x\in V})$ be a causal model. Given a formula $\varphi$ over the exogeneous and endogeneous variables (in some appropriate logic), and a context $\vec{u}$ that assigns values to all variables in $U$, the goal of actual causality is to state whether an assignment of values $\vec{X}=\vec{x}$ to a subset $X\subseteq V$ is a cause of $\varphi$. Halpern and Pearl define $\vec{X}=\vec{x}$ to be a cause of a formula $\varphi$ in $(M,\vec{u})$ if the following three axioms hold.

1. AC1:

   both the cause and the effect are true: the model $(M,\vec{u})$ satisfies $\vec{X}=\vec{x}$ as well as $\varphi$,

2. AC2:

   the principle of counterfactual dependence (discussed below), and

3. AC3:

   causes are minimal: no partial assignment of $\vec{X}=\vec{x}$ satisfies AC1 and AC2.

The key to AC2 is captured by the notion of interventions, describing a direct assignment of values to some endogeneous variables while disregarding their defining functions. Formally, $[\vec{Y}\leftarrow\vec{y}]$ stands for the intervention on variables $Y\subseteq V$ by assigning them values $\vec{y}$ and leaving all other values for variables $V\setminus Y$ to follow from their defining functions. Then, $[\vec{Y}\leftarrow\vec{y}]\psi$ describes the impact of an intervention on a formula $\psi$. An intervention thus can represent a counterfactual: what if variables in $Y$ took values $\vec{y}$ instead of their actual values? Turning back to the definition of actual causes for $\varphi$, axiom AC2 now requires the existence of an intervention $[\vec{X}\leftarrow\vec{x}^{\prime}]$ on the variables in $X$ such that the effect $\varphi$ is not observable, i.e., $[\vec{X}\leftarrow\vec{x}^{\prime}]\neg\varphi$ holds in $(M,\vec{u})$. The precise definition of AC2 is, however, more involved and several variants exist for AC2 to account for different settings and applications.²²2Halpern and Pearl’s definition of causality underwent a considerable amount of development over the past 20 years, primarily varying AC2. One usually distinguishes the original version [58], the updated version [59, 60], and the modified version [56, 57] (alongside variations by other authors [54, 63]).

While the previous section defined and applied qualitative concepts of causation, this section shifts the focus towards quantitative approaches of responsibility. Loosely speaking, responsibility refers to a numerical value designed to measure how much weight an event had in producing an effect, relative to concurring or competing events linked to the same effect. There is widespread agreement that a necessary condition for assuming responsibility is causal relevance of the event in question to the effect [41, 18]. As a consequence, the term responsibility usually builds directly or indirectly on concepts of causality. While the specific numerical value in a notion of responsibility may not have a semantic content, it can order the events in terms of their causal relevance.

Chockler and Halpern [23] introduced the notion of degree of responsibility, which is attributed to actual causes in causal models of HP causality. This degree measures how many changes to the evolution of events are necessary until counterfactual values for the actual cause change the observable effect. In [24] this notion is combined with the study of mutant coverage to build a degree of responsibility in CTL model checking assigned to state-proposition pairs (see also Section 2.1).

The degree of responsibility measures the influence of an event by looking at how many further counterfactual changes are (minimally) required to swap the effect, but is does not take into account how many such minimal sets of changes exist. One can argue that a cause is individually more influential if it admits many such sets since this means less dependencies on other events. This rationale has generated an active strand in formalization of responsibility based on the Shapley value [106]. The Shapley value is a central solution concept from theoretical economics and was originally designed to find a fair distribution of a financial surplus that was brought about cooperatively by a number of producers.

Formally, a cooperative game with $n$ players is a mapping $g\colon 2^{[n]}\to\mathbb{R}$ such that $g(\emptyset)=0$, where $[n]=\{1,\ldots,n\}$. The value $g(C)$ is meant to represent the surplus (or, depending on the specific situation, the cost) that the coalition $C\subseteq[n]$ can ensure upon acting collaboratively. The Shapley value of player $i$ is then defined as

where $S_{n}$ denotes the set of self-bijections $[n]\to[n]$ and where $\pi_{\geq i}=\{j\in[n]\mid\pi(j)\geq\pi(i)\}$ for a given $\pi\in S_{n}$. Intuitively, $g(\pi_{\geq i})-g(\pi_{\geq i}\setminus\{i\})$ describes the marginal contribution of player $i$ to the coalition $\pi_{\geq i}$. The Shapley value takes the average of all such marginal contributions. Thus, ${\operatorname{Sh}}(i)$ is a measure for the overall influence of player $i$ in the game $g$.

The general setup of cooperative games as real-valued functions on the power set of $[n]$ makes the Shapley value amenable to measuring the influence of abstract players in formalized situations of collaborative interaction. This rationale has recently been invoked for the interpretation of machine learning models [117, 35, 91, 1, 110]. In this case, the players are the input parameters to a machine learning model, and the Shapley value has the goal to measure the influence of each parameter on the output of the model.

This section outlines three approaches that employ the Shapley value as a means to distribute an overall effect into individual responsibilities. In Section 3.1 the general setting of an extensive form game is chosen and responsibilities are attributed to its players with respect to producing a certain outcome. Section 3.2 discusses a notion of importance of states for the satisfaction of an LTL property in a Kripke structure. Section 3.3 finally presents an extension of the Shapley value that can be used to define responsibilities in a setting of continuously varying parameters.

As seen in the preceding sections, notions of causality and responsibility have been widely explored in the non-probabilistic setting. In contrast, there have been far less attempts at defining a suitable notion of causes for probabilistic operational systems such as Markov chains. However, probabilistic theories of causation have been considered in various philosophical accounts [111, 21, 107, 39]. One central idea behind these theories is the probability-raising principle, which goes back to Reichenbach [103, 104]. It states that causes should raise the probability of their effects. After observing a cause $C$, the probability of an effect $E$ is higher than after observing that the cause has not occurred. Formulated with conditional probabilities, this can be written as

For the conditional probabilities to be well-defined, it is necessary that ${\operatorname{Pr}}(C)>0$ and ${\operatorname{Pr}}(\neg C)>0$. Later on, we will make sure that the events conditioned on have positive probability. Note that if ${\operatorname{Pr}}(C)>0$ and ${\operatorname{Pr}}(E\mid C)>{\operatorname{Pr}}(E)$, it already follows that ${\operatorname{Pr}}(\neg C)>0$. Defining $p\stackrel{{\scriptstyle\text{\tiny def}}}{{=}}{\operatorname{Pr}}(C)$, the equivalence of the two inequalities follows from the equation ${\operatorname{Pr}}(E)=p\cdot{\operatorname{Pr}}(E\mid C)+(1-p)\cdot{\operatorname{Pr}}(E\mid\neg C)$, which implies

The probability-raising principle alone, however, cannot distinguish between cause and effect as it holds if and only if ${\operatorname{Pr}}(C\mid E)>{\operatorname{Pr}}(C\mid\neg E)$ as well. For this reason, additional conditions have to be imposed for causal reasoning. One key condition is temporal priority, which prescribes that a cause has to occur before the effect.

This section formalizes both the probability-raising principle as well as the requirement of temporal priority for probabilistic operational models. We draw connections between different ideas from the literature to provide an overview over basic probabilistic notions of causality in the context of formal verification. For this, we assume to have given a DTMC $\mathcal{M}$ with a probability distribution over initial states. This way, the sets $\Pi_{\varphi}$ of paths starting in initial states and fulfilling an LTL property $\varphi$ are measurable [114] and have a well-defined probability value ${\operatorname{Pr}}_{\mathcal{M}}(\Pi_{\varphi})$, which we also denote by ${\operatorname{Pr}}_{\mathcal{M}}(\varphi)$. Applying the probability-raising principle and expressing the temporal priority using LTL leads to the following first definition of causality in DTMCs for reachability properties.

Note that Equation 3 implies that ${\operatorname{Pr}}_{\mathcal{M}}\big{(}\neg(\neg E\;\mathcal{U}\,C)\big{)}>0$. This ensures that also ${\operatorname{Pr}}_{\mathcal{M}}\big{(}\Diamond E\mid\neg(\neg E\;\mathcal{U}\,C)\big{)}$ is well-defined and so Equation 3 is equivalent to ${\operatorname{Pr}}_{\mathcal{M}}(\Diamond E\mid\neg E\;\mathcal{U}\,C)>{\operatorname{Pr}}_{\mathcal{M}}\big{(}\Diamond E\mid\neg(\neg E\;\mathcal{U}\,C)\big{)}$. If there are no paths first reaching the effect $E$ and afterwards the cause $C$, e.g., because the states in the effect $E$ are absorbing, Equation 3 simplifies to ${\operatorname{Pr}}_{\mathcal{M}}(\Diamond E\mid\Diamond C)>{\operatorname{Pr}}_{\mathcal{M}}(\Diamond E)$.

In this treatment of reachability properties, a cause $C$ specifies the set of finite executions ending in $C$ that cause the subsequent extension to an infinite execution to satisfy $\Diamond E$. This idea can be lifted to the treatment of causes of arbitrary events in $\mathcal{M}$ specified by a measurable set of infinite paths $\mathcal{L}\subseteq S^{\omega}$. A cause is then a set of finite paths $\Gamma\subseteq S^{+}$. Besides the probability-raising property, the temporal priority condition needs to be included. For path properties this needs extra consideration. While for a cause $\Gamma\subseteq S^{+}$ it is clear that the cause is observed once a finite path in $\Gamma$ is generated in a DTMC, this is not the case for the effect $\mathcal{L}\subseteq S^{\omega}$ as it consists of infinite executions. However, it seems natural to say that the effect occurred on a finite path $\delta$ whenever ${\operatorname{Pr}}_{\mathcal{M}}(\mathcal{L}\mid\delta)=1$, i.e., if a generated finite path ensures that almost all infinite extensions belong to $\mathcal{L}$. Here, we used $\delta$ to also denote the event of all infinite paths having $\delta$ as a prefix. Analogously, for a set of finite paths $\Gamma$, we denote by $\Gamma$ also the event of all infinite paths with a prefix in $\Gamma$. Consequently, $\neg\Gamma$ denotes the event of all infinite paths that have no prefix in $\Gamma$. The discussed treatment of temporal priority is now used in the following definition of a cause in a DTMC.

As $\Gamma$ is a set of finite paths in $\mathcal{M}$, the cylinder set spanned by each $\gamma^{\prime}\in\Gamma$ has positive probability. So, the conditional probabilities ${\operatorname{Pr}}_{\mathcal{M}}(\mathcal{L}\ |\ \Gamma)$ and ${\operatorname{Pr}}_{\mathcal{M}}(\mathcal{L}\ |\ \gamma^{\prime})$ in Definition 4.2 are well-defined.

Axiom PAC1 expresses the probability-raising principle. It implies that ${\operatorname{Pr}}_{\mathcal{M}}(\neg\Gamma)>0$. As this ensures that all necessary conditional probabilities are well-defined, PAC1 is equivalent to the probability-raising condition ${\operatorname{Pr}}_{\mathcal{M}}(\mathcal{L}\mid\Gamma)>{\operatorname{Pr}}_{\mathcal{M}}(\mathcal{L}\mid\neg\Gamma)$. Axiom PAC2 captures that the effect must not occur before the cause.

The requirement on the cause in the provided definition is of global nature: the cause $\Gamma$ as a whole has to guarantee the probability-raising property with respect to the effect. Single elements $\gamma\in\Gamma$, however, do not necessarily guarantee that the probability of the effect has been raised. Furthermore, under mild assumptions, the definition subsumes the treatment of reachability properties above:

In the proposition above, ${\operatorname{Pr}}_{\mathcal{M},s}$ denotes the probability measure induced by $\mathcal{M}$ with assuming $s$ as the unique initial state. A related notion of causality based on probability-raising in DTMCs has been introduced by Kleinberg et al. in a series of papers [75, 76, 74, 66, 122]. Here, probabilistic CTL is used to describe the cause $C$ and the effect $E$ via state formulas. We can describe both events also directly as sets of states in the DTMC by considering exactly those states that fulfil the corresponding probabilistic CTL formula. For reachability properties, the set $C$ is then said to be a cause of $E$ if ${\operatorname{Pr}}_{\mathcal{M},c}(\Diamond E)>{\operatorname{Pr}}_{\mathcal{M}}(\Diamond E)$ for all $c\in C$. So, the requirement for this notion of causality is local: reaching any state $c\in C$ has to ensure that the probability of reaching $E$ afterwards is raised. In case $C=\{c\}$ is a singleton disjoint from $E$, this notion agrees with Definition 4.1.

Adapting PAC1 to sets of paths and including the temporal priority requirement that the effect does not occur before the cause (PAC2 as before), we obtain the following definition of causality:

Axiom PAC1^loc can be seen as the local version of PAC1. Clearly, PAC1^loc implies PAC1. Furthermore, PAC1^loc implies that ${\operatorname{Pr}}_{\mathcal{M}}(\neg\gamma)>0$ for all $\gamma\in\Gamma$. Hence, we could equivalently reformulate PAC1^loc as ${\operatorname{Pr}}_{\mathcal{M}}(\mathcal{L}\mid\gamma)>{\operatorname{Pr}}_{\mathcal{M}}(\mathcal{L}\mid\neg\gamma)$ for all $\gamma\in\Gamma$.

The work by Kleinberg et al. proceeds relative to an explicit probability value $p>{\operatorname{Pr}}_{\mathcal{M}}(\mathcal{L})$ such that ${\operatorname{Pr}}_{\mathcal{M}}(\mathcal{L}\mid\gamma)\geqslant p$ for all $\gamma$ in a cause $\Gamma$. The higher this value $p$ lies above ${\operatorname{Pr}}_{\mathcal{M}}(\mathcal{L})$, the greater is the amount by which all elements of $\Gamma$ are guaranteed to raise the probability of the effect $\mathcal{L}$.

Such a reference to a specific threshold value $p$ has also been incorporated into a notion of $p$-causes in [9]. Motivated by monitoring applications (see, e.g., [87]), the underlying idea is that notions of causality could be used to foresee undesirable behavior. If a cause for an erroneous execution is observed, countermeasures can be taken before the error actually occurs. Here it is particularly useful to specify a sensitivity $p$ that expresses how likely an error is after observing the cause. In addition, the occurrence of an erroneous execution should not stay undetected. Therefore, an additional condition is imposed on $p$-causes: almost all executions that exhibit the error should have a prefix in the cause. Together with the temporal priority of the cause (PAC2) as before, these requirements lead to the following definition:

Besides the practicality in monitoring applications, condition PAC3 also adds the counterfactual idea to the definition. Since almost all executions in $\mathcal{L}$ have a prefix in $\Gamma$, the effect occurs with probability $0$ if the cause was not observed. Condition PAC1^p is a third variant of the probability-raising requirement that compares the probability of the effect after observing an element of the cause to a specific threshold value $p$ rather than the overall probability ${\operatorname{Pr}}_{\mathcal{M}}(\mathcal{L})$. In case $p>{\operatorname{Pr}}_{\mathcal{M}}(\mathcal{L})$, this variant implies PAC1 and PAC1^loc.

For $\omega$-regular $\mathcal{L}$ there always exist $p$-causes for any $p\in(0,1]$. The reason is that then almost all paths in $\mathcal{L}$ have a prefix $\pi$ with ${\operatorname{Pr}}_{\mathcal{M}}(\mathcal{L}\mid\pi)=1$. Choosing the shortest of such prefixes in accordance with condition PAC2 yields a $1$-cause and hence a $p$-cause for any $p$. For $p<1$, there are multiple $p$-causes in general. In [9], the problem to find cost-optimal $p$-causes with respect to a variety of cost measures is addressed.

The relationship between the different notions of causes is summarized in the following proposition. It is a direct consequence of the implications between the axioms used in the definitions that have been discussed so far.

The probabilistic notions of causality discussed in this section naturally constitute forward-looking notions: the probability-raising principle inherently addresses the behavior of a system across multiple executions, and causes are prone to exhibiting a predictive character. These notions can be useful in inferring causal dependencies in data series [75, 74, 66] and predicting undesirable behavior of reactive systems through runtime monitoring [9]. Nevertheless, as far as formal probabilistic models are concerned, a comprehensive study of cause-effect relationships is still at the beginning.

This article gave an overview of recent trends in causality-based reasoning in the verification context. The focus of this article was on concepts that aim to explicate why a system exhibits a specific observable behavior and to which degree individual agents of a system can be held responsible for it. For non-probabilistic formal models, concepts of causation have been introduced in multiple facets and examined for manifold applications. To increase the power of causal inferences, a more systematic study relating forward and backward notions of causality would be highly beneficial.

Compared to the non-probabilistic setting, research on probabilistic causation in stochastic operational models is still in its infancy. While the techniques presented here are limited to purely probabilistic models (Markov chains), an examination of causality in probabilistic models with nondeterminism (Markov decision processes) is largely open. A first step in this direction is a formalization of action causes as a hyperproperty in Markov decision processes [37]. Another important future direction is to reason about cause-effect relationships in hidden Markovian models where states (and events) are not fully observable.

Another research strand not covered in this article are causality-based verification techniques (see, e.g., [82, 83]) that rely on the successive identification of cause-effect relationships between events to generate a causality-based proof for the satisfaction or violation of a system property. Along these lines, the work [8] presents a causality-based technique for solving symbolically expressed, infinite-state two-player reachability games. Applying this paradigm also in a probabilistic setting is a promising direction of study.