1 Introduction↩︎

The visdeurbel (“fish doorbell”) is a citizen-science initiative designed to support migrating fish as they pass through the waterways of Utrecht, a major Dutch city [1], [2]. An underwater camera provides a live stream of fish in front of the lock. The lock operator can be alerted in two ways. Public observers may ring the virtual doorbell when they see fish, or the operator can watch the camera feed directly. The system aids fish migration and raises public awareness of ecology. This example illustrates how different components and failures (electric, public and operator failures) contribute to a system-level failure (the lock failing to open).

Fault trees (FTs) are a structured, hierarchical model to analyse failure propagation in complex systems [3], [4]. FTs enable a top-down, deductive approach to failure analysis, breaking down system failures into combinations of component failures using logical gates (e.g., AND, OR). In FT-terminology, the inputs of such a gate are often called the immediate causes of the higher-level cause labeled by the gate [5]. Widely used in safety-critical industries such as aerospace [6], nuclear energy [7], and cybersecurity [8], FTs enable structured reasoning about system reliability, risk assessment, and failure propagation. They serve as a powerful design tool, helping engineers identify weak points and prioritise mitigation strategies. An FT for the “fish doorbell” is given in Fig. 1.

As a risk model, FTs are primarily used to analyze potential failures: what can go wrong? This is done via minimal cut set (MCS) analysis: an MCS is a set of basic failure events that need to happen simultaneously in order for the system to fail. After finding a FT’s MCSs, these are then analyzed in terms of size, likelihood, and common causes to determine the system’s overall reliability.

Actual causality in the Halpern-Pearl framework. Causality, on the other hand, asks the question why has it gone wrong? after the fact. In computer science, the framework of actual causality (AC) by Halpern and Pearl [9] has been especially popular. In AC, a system is modeled as a causal model: a directed acyclic graph of variables, with functions describing each variable in terms of its input. The system’s context is given by values of the initial variables. Within such a system one can perform interventions using do-calculus [10] to forcibly set certain variables. This allows one to go beyond correlations and define causal relationships based on counterfactuals, describing what would have happened if some conditions were different. This has been applied successfully to problems such as fault localization [11], debugging [12], and failure reasoning [13].

Incident analysis and FTs. While FTs are mostly used to prevent failures through risk assessment, they are also an important tool in incident analysis or diagnostics: when a system fails, understand what has happened and why, to prevent its recurrence. A formal framework of causality would be an important asset towards systematic incident analysis. While the use of FTs in diagnoses has been well-studied with systematic methods [14]–[17], a systematic application of actual causality to fault trees is missing from the current literature. So far, the connection between AC and FTs has been limited to generating FTs from trace data [18], and translating attack trees (\(\approx\)FTs for cybersecurity) to causal models, without investigating their actual causes [19].

Contributions. Our main contribution is to apply the AC framework to FTs. We consider the most common type of FTs, namely static, coherent FTs. These can be phrased as directed acyclic graphs of Boolean variables, that are functions of their inputs via their role as AND/OR-gates. Thus FTs can directly be studied from an AC perspective. This by itself is not surprising, but the fact that all functions are Boolean and non-decreasing leads to a deeper understanding than would be possible in regular causal models.

First, it gives us concise classifications of AC. For the three main causality definitions in the AC literature [20] (original: AC-o, updated: AC-u, modified: AC-m), we classify the actual causes of event failure in FTs, given a context, allowing for a straightforward causal analysis of FTs (Thms. 5, 6 & 7). These classifications do not only take into account the Boolean nature of FTs, but also their graph structure. By contrast, FT analysis typically only considers the underlying Boolean functions. This leads to the surprising fact that equivalent FTs can behave differently as causal models. From an AC perspective, this is a feature rather than a bug: in AC, intermediate gates are not just dummy variables, but represent real-world events or subsystems that can be targets for interventions. For FTs, AC-o, AC-u, AC-m form a spectrum for defining causality, from a larger emphasis on the graph structure to a complete emphasis on the Boolean nature. As AC-m looks only at the Boolean nature of the FT, the relation between AC-m and MCSs is stronger. In fact, our results allow us to classify MCSs in terms of AC-m (Cor. 1).

Second, we look at the relation between minimal cut sets and AC-o and AC-u. As MCSs are potential pathways to failure, and AC are events that contributed to failure in a specific scenario, we cannot expect them to be the same. In fact, MCSs are typically large in robust systems to prevent a single-point-of-failure, but ACs are typically small: in fact, it is known for AC-o, and we show for AC-u, that actual causes are only singletons. Nevertheless, there is a clear relation between MCSs and AC. We show that if we take an MCSs as context, then all of its elements are ACs (Thm. 8). Furthermore, for AC-o and AC-u, in a given context, we show that every element of every MCS that has happened, is an AC (Thm. 9). If the FT is a (graph-theoretic) tree rather than a DAG, or if it is in disjunctive normal form, then the converse also holds.

Third, we determine the hardness of determining causes (Thm.10), showing that this is less complex than the general case for AC-u and AC-m, and leverage our classification of actual causality in fault trees to develop algorithms that find all causes for AC-o and AC-m (Sec. 9). Generalizing these algorithms to AC-u does not lead to an appreciable (theoretical) speedup over naïve algorithms; we leave the development of fast algorithms for AC-u to future work.

2 Fault trees↩︎

In a directed graph \((V,E)\), a root or sink is a vertex without outgoing edges; a leaf (source) is a vertex without ingoing edges. The inputs of a vertex \(v\) are its predecessors: \({\it Inp}(v) = \{w \in V \mid (w,v) \in E\}\).

A FT is a systematic, graphical tool for analyzing why systems fail. FT analysis proceeds by breaking down the system-level failure into its causes, and these causes into subcauses, until the root causes are found. These are called basic events (BEs), represented by the leaves of the tree; see Fig. 1. Higher-level failures are connected using an AND-gate when all subcauses must occur for the failure to propagate, or by an OR-gate when a single subcause is sufficient. Formally, a FT is a directed acyclic graph, whose non-leaf nodes are labeled with AND- and OR-gates.

The FT is called tree-shaped if the graph \((V,E)\) is a (directed) tree, i.e., no vertex has two successors. In other cases, we call it DAG-shaped. The nodes of a FT are usually called events: the root \({\it Root}_T\) of the tree is called the top level event, the leaves are the basic events and all other nodes are intermediate events. We write \(\operatorname{BE}_{T} = \{v \in V \mid \gamma(v) = \mathtt{BE}\}\) for the set of basic events. We omit the subscript if \(T\) is clear from the context.

The FT in Fig. 1 features three basic events electricity fails (\(\mathsf{EF}\)), public fails (\(\mathsf{PF}\)) and operator fails (\(\mathsf{OF}\)), one intermediate event alert fails (\(\mathsf{AF}\)), and the top event lock fails (\(\mathsf{LF}\)).

A status vector indicates for each basic event its status, i.e., whether that BE has failed. Write \(\mathbb{B}:= \{0,1\}\); a status vector for \(T\) is a \(\vec{u} \in \mathbb{B}^{\operatorname{BE}_{}}\), where \(u_v=1\) indicates that BE \(v\) has failed and \(u_v=0\) that \(v\) is operational. We often identify a status vector with its set of basic events: Given a set \(C\subseteq \operatorname{BE}_{}\), its status vector \({\vec{u}}^C\) is given by \(u^C_{v}=1\) for \(v\in C\) and \(u^C_v=0\) for \(v\not\in C\). Given a \(b \in \mathbb{B}\), we write \(\vec{u}[v\leftarrow b]\) for the vector that equals \(\vec{u}\), except that it sets \(v\) to \(b\): \((\vec{u}[v\leftarrow b])_v=b\) and \((\vec{u}[v\leftarrow b])_{v'}=(\vec{u})_{v'}\) for \(v\neq v'\).

The semantics of a FT is defined by its structure function. Given a status vector \(\vec{u}\) and a node \(v\), \({\Phi}_{T}(\vec{u},v)\) indicates whether the node \(v\) fails on status vector \(\vec{u}\).

The structure function of the FT in Fig.  1 is given by \(\Phi(\vec{u}) = u_{\mathsf{EF}} \vee (u_{\mathsf{PF}} \wedge u_{\mathsf{OF}})\). In particular, \({\Phi}_{}(0,1,0)=0\) and \({\Phi}_{}(1,1,0)=1\), also written as \({\Phi}_{}(\{\mathsf{PF}\})=0\) and \({\Phi}_{}(\{\mathsf{EF},\mathsf{PF}\})=1\).

A cut set is a set of basic events that causes the top event to fail; a cut set is minimal if no proper subset is a cut set. Minimal cut sets are a key tool in FT analysis, as they constitute a minimal cause for the FT to fail.

The following are cut sets of the FT in Fig. 1; The first two sets are MCSs. \[\{\sf EF\}~~~~ \{{\sf PF}, {\sf OF}\}~~~~ \{\sf EF, {\sf PF}\}~~~~\{\sf EF, {\sf OF}\}~~~~\{\sf EF, {\sf PF}, {\sf OF}\}\]

Since (standard) FTs do not contain any negations, they are coherent: a cut set remains a cut set if we add more elements, because a failed system remains failed if more failures occur. Formally, the structure function is monotonous: if \(C\subset C'\), then \({\Phi}_{}(C,v)\leq {\Phi}_{}(C',v)\) for all events \(v\).

A BE \(e\) is critical for a status vector if flipping its value from \(0\) to \(1\) causes the system to transition from non-failure to failure.

A basic event \(e\) is irrelevant iff the structure function is constant in \(u_{e}\) iff \(e\) is not an element of any MCS.

In FT analysis, each MCS is seen as a potential root cause. All elements of a given MCS are seen as causes, since we need each of them to occur for a top level failure.

3 Preliminaries on causal models↩︎

Halpern and Pearl [9] define actual causality (AC) in terms of Causal Models (CMs), composed of variables and their corresponding values. The dependencies between variables are expressed through structural equations encoding the system’s behavior. We first recap CMs and associated concepts as in [9].

3.1 Causal models and networks↩︎

A causal model is defined based on a signature \({S}\) consisting of a pair \(( {\mathsf{U}^{\textrm{c}}}, {\mathsf{U}^{{\textrm{i}} }})\), where \({\mathsf{U}^{\textrm{c}}}\) is a set of exogenous variables, \({\mathsf{U}^{{\textrm{i}} }}\) a set of endogenous variables. For notational convenience, we assume all variables to be Boolean.

Intuitively, exogenous variables represent a context (\(\mathsf{U}^{\textrm{c}}\)), or external factors: conditions outside the model’s control that influence the system, but are not explained by the model itself. Endogenous variables are the internal variables (\(\mathsf{U}^{{\textrm{i}} }\)) of the model. Take the fish doorbell example of the introduction. For instance, we let \({\sf B_{EF}}\in \mathsf{U}^{\textrm{c}}\) (“Electricity Failure”) denote an exogenous variable representing the external failure of supply of electrical power. Its value determines the endogenous variable \(\sf EF\in \mathsf{U}^{{\textrm{i}} }\), which captures the availability of electricity. Thus, \({\sf B_{EF}}\) serves as the contextual factor governing the state of \(\sf EF\), and may be thought of as reflecting the environment’s provision (or interruption) of power.

The values of endogenous variables \(X \in \mathsf{U}^{{\textrm{i}} }\) are determined by structural equations \(F_X\), based on the exogenous and other endogenous variables.

Each \(F_X\) captures how the value of \(X\) is determined by the other variables in \({\mathsf{U}^{\textrm{c}}} \cup {\mathsf{U}^{{\textrm{i}} }}\). The functions \(F_X\) define a so-called set of structural equations; causal models are also referred to as structural equation models (SEMs).

A CM induces a causal network: a directed edge from a variable \(Y \in \mathsf{U}^{{\textrm{i}} }\cup \mathsf{U}^{\textrm{c}}\) to a variable \(X \in \mathsf{U}^{{\textrm{i}} }\)

exists whenever the value of \(F_X\) depends on the value of \(Y\). Exogenous variables in \(\mathsf{U}^{\textrm{c}}\) have no incoming edges as they are the ‘inputs’ of the network. AC [9] is typically restricted to acyclic causal networks, ensuring that, for a given context, the structural equations have a unique solution.

Causal networks provide an intuitive and informative means of understanding the causal pathways within a CM. The causal network corresponding to Example 1 is provided in Fig. 3.

3.2 Reasoning in causal models↩︎

Given a signature \(S = ({\mathsf{U}^{\textrm{c}}}, {\mathsf{U}^{{\textrm{i}} }})\), an expression \(X = x\), where \(X \in {\mathsf{U}^{{\textrm{i}} }}\) and \(x \in \mathbb{B}\), is referred to as a primitive event. A basic causal formula has the structure \([Y_1 \leftarrow y_1, \ldots, Y_k \leftarrow y_k] \varphi\), where \(\varphi\) is a Boolean combination of primitive events, and each \(Y_i \in \mathsf{U}^{{\textrm{i}} }\) is a distinct endogenous variable. This formula is abbreviated as \([\vec{Y} \leftarrow \vec{y}] \varphi\) and, intuitively, it states that \(\varphi\) holds when \(Y_i\) is set to \(y_i\).

A context refers to an assignment \(\vec{u}\) of values to all exogenous variables in \({\mathsf{U}^{\textrm{c}}}\). We denote by \((M, \vec{u})\) the CM \(M\) under the specific assignment \(\vec{u}\) for \(\mathsf{U}^{\textrm{c}}\). An intervention modifies a CM \(M = ({S}, {F})\) by fixing an endogenous¹ variable \(X \in \mathsf{U}^{{\textrm{i}} }\) to a particular value \(x\). Interventions are considered as external effects on the system, not governed by the structural equations. The result is a new model, written \(M_{X \leftarrow x}\), which is identical to \(M\) except that the structural equation \(F_X\) is replaced with the constant assignment \(X = x\). When applying multiple interventions, such as \(X_1 \leftarrow x_1, \ldots, X_n \leftarrow x_n\), we write \(\vec{X} \leftarrow \vec{x}\) and denote the modified model by \(M_{\vec{X} \leftarrow \vec{x}}\).

We write \((M, \vec{u}) \models \varphi\) to indicate that the causal formula \(\varphi\) holds in the CM \(M\) under context \(\vec{u}\). The satisfaction relation \(\models\) is defined inductively. Specifically, \((M, \vec{u}) \models X = x\) iff the variable \(X\) takes the value \(x\) in the unique solution to the structural equations of \(M\) under context \(\vec{u}\). Uniqueness is guaranteed since [9] considers acyclic models. Conjunctions and negations are interpreted in the standard logical way. Furthermore, \((M, \vec{u}) \models [\vec{Y} \leftarrow \vec{y}] \varphi\) holds iff \((M_{\vec{Y} \leftarrow \vec{y}}, \vec{u}) \models \varphi\). Potential actual causes are of the form \(X_1 = x_1 \land \cdots \land X_k = x_k\), with \(X_i \in \mathsf{U}^{{\textrm{i}} }\), which can be abbreviated as \(\vec{X} = \vec{x}\).

4 Fault trees as causal models↩︎

Following the examples above, we embed FTs in CMs as follows.

As basic events appear twice in \(M_T\), we could have taken \(\mathsf{U}^{\textrm{c}}=\varnothing\). However, by considering basic events as endogenous variables, each context in \(M_T\) corresponds to a status vector in \(T\). Further, we note that FT analysts are merely interested in causal reasoning about failure of the top event, i.e., \(X_{{\it Root}} = 1\).

This construction guarantees that, given a FT status vector \(\vec{u}\), each variable in the CM gets assigned the correct value, i.e., the value given by the structure function applied to \(\vec{u}\). In other words, the structure function is the unique solution to the CM equations.

The following result phrases the coherency of FTs in terms of CMs. Intuitively, it states that setting a variable \(X \leftarrow 0\) can only decrease the value of other variables, and setting \(X \leftarrow 1\) can only increase the value of other variables. Its proof is straightforward induction.

5 Actual causality↩︎

Several notions of Halpern and Pearl’s actual causality (AC) have been defined over time. In what follows, we present the original AC-o definition from [9], followed by two refinements: the updated AC-u and the modified AC-m definitions. All three versions are included in Definition 2.2.1 of [20].

5.1 The original definition AC-o↩︎

Each definition of actual causality consists of three conditions, typically referred to as \({\boldsymbol{AC1}}\), \({\boldsymbol{AC2}}\), and \({\boldsymbol{AC3}}\) that must hold for a conjunction of primitive events \(\vec{X} = \vec{x}\) to be an actual cause for the effect \(\varphi\) in a causal model \(M\) under the context \(\vec{u}\). Intuitively, \({\boldsymbol{AC1}}\) states that both the cause \(\vec{X} = \vec{x}\) and the effect \(\varphi\) hold for \(M\) in context \(\vec{u}\). Note that \({\boldsymbol{AC2}}\) uses a partition \((\vec{Z}, \vec{W})\) of the endogenous variables \(\mathsf{U}^{{\textrm{i}} }\). \({\boldsymbol{AC2}}(a^o)\) represents the counterfactual test under contingency \(\vec{W}\): if the cause were absent, the effect should also disappear, assuming the interventions in \(\vec{W}\) that modify \(M\). Contingencies are particularly useful when causes are redundant, as they allow testing whether the counterfactual still holds after disabling one potential cause. This isolates the causal contribution of each factor: \(\vec{X} = \vec{x}\) becomes pivotal under \(\vec{W}\). The variables in \(\vec{Z}\) can be viewed as constituting the causal path to \(\varphi\) [20]: intuitively, intervening on some variable in \(\vec{X}\) propagates changes through variables in \(\vec{Z}\), ultimately altering the value of \(\varphi\). Interventions in \(\vec{W}\) may indirectly modify the values of variables in \(\vec{Z}\). According to \({\boldsymbol{AC2}}(b^0)\), these changes must leave \(\varphi\) unaffected, even when certain variables in \(\vec{Z}\) are held at their original values. \({\boldsymbol{AC2}}(b^0)\) corresponds to a sufficiency condition. Finally, \({\boldsymbol{AC3}}\) expresses minimality.

Without loss of generality, in our examples, the endogenous variables \((\in \mathsf{U}^{{\textrm{i}} })\) occurring in \(\varphi\) are excluded from \(Z\).

\({\boldsymbol{AC1}}\) requires that both the cause \(\vec{X} = \vec{x}\) and the effect \(\varphi\) hold in the actual world \(\vec{u}\). \({\boldsymbol{AC1}}\) is satisfied, as: \[\begin{align} \label{eq:ACO-AC1} (M^-_{\sf doorbell}, \vec{u}) &\models {\sf PF}= 1,\\ (M^-_{\sf doorbell}, \vec{u}) &\models \sf LF= 1. \nonumber \end{align}\tag{1}\]

\({\boldsymbol{AC2}}(a^o)\) corresponds to a necessity condition. Namely, setting the causal variables \(\vec{X}\) to different values \(\vec{x}'\) changes the satisfiability of \(\varphi\) from true to false. \({\boldsymbol{AC2}}(a^o)\) is sometimes referred to as the counterfactual test and \(W\) as the contingent variables.

In \((M^-_{\sf doorbell}, \vec{u})\), consider \(\vec{W} = \{\sf EF, {\sf OF}\}\) and the setting \(\{\sf EF\leftarrow 0\) and \({\sf OF}\leftarrow 1\}\) (i.e., \(\vec{w} = (0,1)\)). In this setting, the value of \({\sf PF}\) is pivotal: Let \(x'\) be the setting \({\sf PF}\leftarrow 0\) (i.e., \(\vec{x}' = (0)\)). Then \({{\boldsymbol{AC2}}(a^o)}\) and \({{\boldsymbol{AC2}}(b^o)}\) hold (note \(Z' = \varnothing\)): \[\label{eq:ACO-AC2a} (M^-_{\sf doorbell}, \vec{u}) \models [{\sf PF}\leftarrow 0, \sf EF\leftarrow 0, {\sf OF}\leftarrow 1] (\sf LF= 0)\tag{2}\] While \[\label{eq:ACO-AC2b} (M^-_{\sf doorbell}, \vec{u}) \models [{\sf PF}\leftarrow 1, \sf EF\leftarrow 0, {\sf OF}\leftarrow 1](\sf LF= 1)\tag{3}\]

\({\boldsymbol{AC2}}(b^o)\) corresponds to a sufficiency condition. It guarantees that it is \(\vec{X} \leftarrow \vec{x}\) (acting through the directed paths involving the variables in \(\vec{Z}\)) that is genuinely responsible for \(\varphi\).

\({\boldsymbol{AC3}}\) is a minimality condition that ensures the identified set of causal variables \(\vec{X}\) is the smallest set witnessing \(\varphi\) in \((M^-_{\sf doorbell}, \vec{u})\). \({\boldsymbol{AC3}}\) trivially holds in our example, as the singleton set \(\{{\sf PF}\}\) satisfies AC1-AC2. Hence, also based on (1 ), (2 ) and (3 ), it follows that \({\sf PF}= 1\) is an actual cause of \(\sf LF= 1\).

Now consider the CM \(M_{{\sf doorbell}}\) from Example 1, which includes the additional variable \({\sf AF}= {\sf PF}\land {\sf OF}\) (see Fig. 3). \(M_{{\sf doorbell}}\) and \(M^-_{{\sf doorbell}}\) are logically equivalent. However, in \(M_{{\sf doorbell}}\), \({\sf PF}= 1\) is not an actual cause of \(\sf LF= 1\) in the given context \(\vec{u} = (1,1,0)\). The reason is that changing \({\sf PF}\) from 0 to 1 in setting \(\vec{W}\) is no longer pivotal. There are two cases to consider: If \({{\sf AF}} \in \vec{W}\), then \(\sf LF\) will take the value of \({\sf AF}\), irrespective of \({\sf PF}\). (In fact, \({\sf AF}=0\) is an actual cause for \(\sf LF= 0\)). Otherwise, if \({\sf AF}\in \vec{Z}\), with \({\sf AF}= 0\) in the actual world, \({\boldsymbol{AC2}}(b)^0\) again fails. The choice of variables (what is treated as primitive and what is derived) crucially affects what qualifies as actual cause.

Interestingly, actual causes under AC-o are always singletons.

5.2 The updated definition AC-u↩︎

In the CM \(M^-_{\sf doorbell}\) of Example 4, \({\sf PF}\) is identified as a cause of \(\sf LF\). However, this may be regarded as a partial form of causality, since it results in a lock failure (\(\sf LF= 1\)) only in conjunction with an operator failure (\({\sf OF}= 1\)) that did not occur. To better capture such cases, a so-called updated actual causality AC-u was proposed in [20]. AC-u redefines \({\boldsymbol{AC2}}(b^o)\) in Definition 7 to:
\({\boldsymbol{AC2}}(b^u)\) For all subsets \(\vec{W}' \subseteq \vec{W}\) and \(\vec{Z}' \subseteq \vec{Z}-\vec{X}\), we have \[\label{eq:ACU} ({M}, \vec{u}) \models [ \vec{X} \leftarrow \vec{x}, \vec{W}' \leftarrow \vec{w}, \vec{Z}' \leftarrow \vec{z}^* ]\varphi\tag{4}\] where \(\vec{z}^*\) denotes the actual values of the variables in \(\vec{Z}'\).

Unlike AC-o, AC-u allows for multiple element causes [20]. It also subsumes AC-o:

5.3 The modified definition AC-m↩︎

To make the definition of causality more straightforward, a simplified form of AC2 was proposed [20]. The corresponding notion of causality is referred to as the modified actual causality AC-m. The core idea is to restrict attention to variable assignments that correspond to the actual situation we are analysing. Rather than considering hypothetical values for the contingency variables in \({\vec{W}}\), the modified definition only looks at the specific values these variables take in the considered context \(\vec{u}\). An important consequence of this simplification is that it makes \({\boldsymbol{AC2}}(b^o)\) and \({{\boldsymbol{AC2}}}(b^u)\) subsumed by the modified AC2\(^m\) below, whenever \(\vec{W}\) is held at its actual values. As a result, there is no longer a need for these additional conditions, since the only contingencies we need to consider are those that align with the actual context. Hence, in the modified definition AC-m, condition AC2 simply becomes:
AC2\(^m\) There is a set \(\vec{W} \subseteq \mathsf{U}^{{\textrm{i}} }\) and a setting \(\vec{x}'\) of the variables in \(\vec{X}\) such that \[\label{eq:ACM} ({M}, \vec{u}) \models [\vec{X} \leftarrow \vec{x}', \, \vec{W} \leftarrow \vec{w}^*] \lnot \varphi\tag{5}\] with \(\vec{w}^*\) the values of the variables in \(\vec{W}\) in the actual context.

Note that AC-m subsumes both AC-o and AC-u:

The complexity of computing ACs for each of the definitions AC-o, AC-u and AC-m is analysed in [20], [21]. The results show that computing AC is hard; e.g., AC-o is NP-complete in binary models (where all variables are binary). In binary models, SAT solving has been used to compute AC-m [22].

6 Actual causality in fault trees↩︎

Our main results are the classifications of AC-o, AC-u, and AC-m for FTs: Given a FT \(T\) and a context \(\vec{u}\) for its causal model \(M_T\) (so \(\vec{u}\) is a status vector), we give necessary and sufficient conditions for any \(\vec{X} = \vec{x}\) to be an actual cause for \(X_{{\it Root}} = 1\). We only consider \(X_{{\it Root}} = 1\) because our results transfer to any variable \(X_v = 1\) by considering the sub-FT rooted at \(v\); and we are more interested in what causes failure than in what causes non-failure. The results for \(X_{{\it Root}} = 0\) can be obtained by applying our results to the dual FT [23].

6.1 AC-o in FTs↩︎

The classification of AC-o for FTs is as follows:

Condition 1 requires that causes are singletons (by Theorem 2), and that only events \(X_v = 1\) can cause \(X_{{\it Root}} = 1\). The latter is a consequence of Theorem 1, by the lack of negation in FTs: an event \(X_v = 0\) will never cause a later variable to be equal to 1.

Example 6 points to an interesting property of causality in FTs. The two FTs of Fig. 6 have identical structure functions, hence identical minimal cut sets; thus in FT analysis they would be considered equivalent. However, under the context \(\vec{u} = (1,1,0)\) we see that \(X_{\mathsf{EF}}=1\) is a cause of system failure in one FT, but not in the other: Equivalent FTs may behave differently as causal models. From the causality perspective, this is a feature, not a bug: Endogenous variables in CMs are not simply functions of their inputs, but represent real-world events that can be interacted with independently of their inputs. For FTs, this may capture a form of the epistemic uncertainty that we might have modelled our system incorrectly: the possibility of an intervention setting an intermediate gate represents the possibility that an intermediate gate might fail despite its children not failing, because in modelling our system we missed a failure cause.

Theorem 5.2b is there to exclude some pathological cases.This condition does not hold, for excample, in \(T_1\) of Fig. 7: the path \(e_2 \rightarrow {\it Root}\) has two inputs that share the input \(e_1\), but have different labels. Therefore, \(X_{e_2} =1\) is not an actual cause (for AC-o) for \(X_{{\it Root}} = 1\). This is understood from the structure function \(X_{e_1} \vee (X_{e_1} \wedge X_{e_2}) \equiv X_{e_1}\). The BE \(e_2\) is irrelevant as it does not appear in the structure function; this is reflected by the fact that it cannot be an actual cause. Indeed, \(e_2\) does not satisfy Theorem 5.

Precisely because such a construction makes events irrelevant, one rarely sees paths in which AND-gates and OR-gates share children: Of the 54 real-world FTs in the benchmark of [24]–[26], only 10 have any such paths. Thus Theorem 5.2b is mathematically necessary, but plays a limited role in practice: Having a path \(v \rightarrow {\it Root}\) of only 1-valued nodes is often enough to imply AC-o. Note that it is also possible to construct FTs in which events that are irrelevant from the FT perspective can still be actual causes, such as in \(T_2\) of Fig. 7. The key here is again that changing the graph structure impacts how causality behaves, even if it leaves the structure function unchanged.

6.2 AC-u in FTs↩︎

The classification of AC-u for FTs is similar to that of AC-o. As before, we only consider causes of \(X_{{\it Root}} = 1\). Unlike in general causal models [20], the result below states that AC-u in FTs only admits singleton causes.

Unlike in general causal models [20], Theorem 6 states that AC-u in FTs only admits singleton causes. Once again, the culprit is the coherency of Theorem 1: the difference between AC-o and AC-u is that eq. 4 must hold for all subsets \(\vec{W}' \subseteq \vec{W}\), rather than just \(\vec{W}\) itself. However, due to coherency, in FTs it turns out that it just has to hold for the worst-case \(\vec{W}'\) consisting only of those variables that have value \(0\) in \(\vec{w}\). The fact that eq. 4 only has to hold for one \(\vec{W}'\) aligns the definition of AC-u closer to AC-o, and this turns out to be sufficient for the proof of Theorem 2 to also hold for AC-u in FTs. Other than that, the difference between AC-o and AC-u for FTs lies in condition 2c.

Example 7 illustrates how AC-u brings causality in FTs closer to the structure function: Under AC-u, this FT now behaves identically to the FT of Fig. 4 to which it is equivalent. However, it is still possible for two equivalent FTs to behave differently under AC-u: in \(T_1\) of Fig. 7 with \(\vec{u} = (1,1)\), the event \(X_{e_2} = 1\) is not a cause of \(X_{{\it Root}} = 1\), but it is a cause in the equivalent FT \(T_2\).

6.3 AC-m in FTs↩︎

For AC-m, we get the following classification. Interestingly, it looks completely different to those of AC-o and AC-u. The most striking difference is that it does not refer to the graphical structure of the FT; instead AC-m can be characterised purely in terms of the structure function.

We only consider causes that consist of BEs. This is for notational convenience; one can always consider non-BE causes by changing these nodes into BEs and removing their inputs.

The fact that AC-m so closely reflects the structure function also allows us to classify MCSs in terms of AC-m:

7 From minimal cut sets to actual causality↩︎

It may be striking that our classification of actual causality in FTs of Theorems 5, 6 & 7 has nothing to do with MCSs, as these are understood to be potential causes of system failures. In this section, we show that being part of an MCS is a necessary, but generally not sufficient, condition for being an actual cause.

7.1 Fault trees without given context↩︎

First, we consider FTs without a given context \(\vec{u}\). In this setting, the pertinent question is whether it is possible for a BE to ever be an actual cause. It turns out that being a relevant BE is a sufficient condition; for AC-m it is also necessary. Recall that a BE \(v\) is relevant if it is part of some MCS, or equivalently, if the structure function is non-constant in \(X_v\).

Theorem 8.2 does not hold for AC-o and AC-u: In \(T_2\) of Fig. 7 \(e_2\) is not relevant, but it satisfies AC-o and AC-u for \(\vec{u} = (1,1)\).

7.2 Fault trees with given context↩︎

Now we consider FTs with a given context \(\vec{u} = \vec{u}^D\). The question is now to what extent MCS \(C\) that have happened, i.e. that satisfy \(C \subseteq D\), give rise to actual causes. For AC-m, this does not have a neat description: in fact, Theorem 7.3 states that AC-m is best expressed in terms of maximal sets of events that still result in nonfailure, rather than minimal sets of events that result in failure. For AC-o and AC-u, however, we find that for every MCS \(C \subseteq D\), every \(v \in C\) is an actual cause of top event failure. This sufficient condition is not necessary: In \(T_2\) of Fig. 6, \(D = \{\mathsf{EF},\mathsf{OF}\}\), and \(\mathsf{OF}\) is not part of any MCS present in \(C\); however, \(X_{\mathsf{OF}} = 1\) still satisfies AC-o for \(X_{{\it Root}} = 1\). To state when the condition is necessary, we recap the definition of FTs in disjunctive normal form (DNF). A DNF FT consists of a top OR-gate, a second layer of AND-gates, and a third layer of BEs; the ANDs represent its MCSs.

We then get the following result:

8 Computational complexity↩︎

Determining whether something is a cause in binary models in general is NP-complete for AC-o/AC-m [20] and so-called \(\textrm{D}_2^{\textrm{P}}\)-complete (worse than NPC) for AC-u [21]. For FTs, we show that this is less complex for AC-u and AC-m:

A full computational study, where these complexity results are accompanied by algorithms that scale well in practice, is left for future work.

9 Algorithms↩︎

In previous sections we discussed how actual causes in FTs are characterized mathematically. In this section, we discuss how these characterizations can be used algorithmically: we describe algorithms for finding actual causes under AC-o, AC-u, and AC-m.

9.1 Algorithms for AC-o↩︎

Using Theorem 5, we can construct a naive algorithm that answer whether \(X_v =1\) satisfies AC-o for \(X_{{\it Root}} = 1\), by first checking whether \((M_T,\vec{u}) \models (X_v = 1) \wedge (X_{{\it Root}} = 1)\), and then considering all paths \(v \rightarrow {\it Root}\) and checking whether one of them satisfies properties (2a) and (2b). The fundamental issue with this approach is that the number of paths between two vertices in a DAG with \(n\) vertices is \(\mathcal{O}(2^n)\), hence this approach scales badly for large \(T\). Theorem 10 shows that deciding AC-o in FTs is NP-complete, hence worst-case exponential behaviour is likely to be unavoidable; nevertheless, we can improve on this naive approach.

More precisely, one may note that the impediment for a path to show AC-o is the presence of an AND-gate and an OR-gate on it with a shared child. As we discuss in Section 6.1, this typically leads to irrelevant BEs in the FT, and for this reason such pairs of gates rarely occur in real-world FTs. Therefore, it makes sense to find the set of such forbidden pairs, i.e., the set \[\mathcal{F}(T) = \left\{(h,l) \in V^2 \;\middle|\;\substack{\exists \text{ path } l \rightarrow h \textrm{ and } \gamma(l) \neq \gamma(h)\\ \textrm{and } {\it Inp}(h) \cap {\it Inp}(l) \neq \varnothing}\right\}.\] Note that each forbidden pair consists of a ‘high’ element \(h\) closer to \({\it Root}\), and a ‘low’ element \(l\) (see Fig. 10).

The set \(\mathcal{F}(T)\) can be used as follows. If one were just interested in nodes \(v\) that have a path \(v \rightarrow {\it Root}\) containing only 1s, a simple algorithm would suffice: starting from a set \(Q = \{{\it Root}\}\) of vertices from which \({\it Root}\) can be reached, we keep adding to \(Q\) vertices that evaluate to 1 under \(\vec{u}\) and that have an edge into \(Q\), until no more vertices can be added. This finds all relevant vertices in linear time.

For our problem, we only want such vertices whose paths to \({\it Root}\) do not contain two elements of a forbidden pair. That means that instead of storing binary information at each vertex (part of \(Q\) yes/no), we must store which ‘high’ elements we have encountered so far, to signal that we cannot add the corresponding ‘low’ elements. Since every node can have multiple paths to the root containing different high elements, we need to store a set of sets of high elements at each vertex.

This idea is the basis for Algorithm 9, which finds all vertices \(v\) such that \(X_v = 1\) satisfies AC-o for \(X_{{\it Root}} = 1\). Since we only care about nodes that evaluate to 1, we formalize this as the positive part of \(T\) (line 1 of Algorithm 9):

Of course, if \(X_{{\it Root}} = 0\), then \(X_{{\it Root}} = 1\) cannot have any cause as it is not true (line 3). Otherwise, we will define, for each node \(v\), a set of sets of high elements \(\mathcal{S}(v)\), where \(H \in \mathcal{S}(v)\) means that there is a path \(v \rightarrow {\it Root}\) which contains precisely the high elements in \(H\), and none of their corresponding low elements. Thus, we initialize \(\mathcal{S}({\it Root})\) as either \(\{\{{\it Root}\}\}\) or \(\{\varnothing\}\), depending on whether \({\it Root}\) is itself a high element in a forbidden pair or not (lines 5-9). Each other \(\mathcal{S}(v)\) is initialized as \(\varnothing\) (line 11), since we have not found a path to \({\it Root}\) yet.

Next, we address nodes one by one, starting at \({\it Root}\) and working our way down (line 10). At \(v\), we look at all \(H\) in all \(\mathcal{S}(w)\). If \(v\) is not the low element of any high element in \(H\) (line 14), then we add either \(H\) or \(H \cup \{v\}\) to \(\mathcal{S}(v)\), depending on whether \(v\) is a high element itself or not (lines 15-19).

At the end, we return the set of inputs of all vertices \(w\) with \(\mathcal{S}(w) \neq \varnothing\). This is because if \(v \in {\it Inp}(w)\) with \(\mathcal{S}(v) = \varnothing\) and \(\mathcal{S}(w) \neq \varnothing\), this means that \(v\) is a low element corresponding to a high element in every set in \(\mathcal{S}(w)\). However, by Theorem 5, the first element of a path is allowed to be part of a forbidden pair.

Essentially, this algorithm visits every edge once, so for fixed \(k = |\mathcal{F}(P_{T,\vec{u}})|\) the complexity is \(\mathcal{O}(|E|)\) (see Remark [rmk:ptu] for why we use \(\mathcal{F}(P_{T,\vec{u}})\) rather than \(\mathcal{F}(T)\) here and in Algorithm 9). The information transmitted over each edge is an element of \(\mathcal{S}(w) \in \mathcal{P}(\mathcal{P}(\mathcal{F}(P_{T,\vec{u}})))\), which has size \(\leq 2^k\) (\(\mathcal{P}\) stands for powerset).

To find all forbidden pairs, we have to look at each of the \(\mathcal{O}(|E|^2)\) pair of edges to see whether they have the same source and their targets have different gate types, and to see whether there is a path between one of the targets and the other (\(\mathcal{O}(|V|)\) steps per pair). As a result, we get the following theorem:

9.2 Algorithms for AC-u↩︎

Unfortunately, an approach such as Algorithm 9 appears not to work: by Theorem 6, we also need to be able to set the children of all OR-gates on the path to 0 without affecting \({\it Root}\). Thus, at every node we cannot just store a set of sets of high elements; instead, we need a set of sets of [high elements and OR-gates]. Thus the stored information is exponential in \(|V|\). At that rate, one might as well just check all paths, of which there are also \(\mathcal{O}(2^{|V|})\) many. Including some polynomial factors to account for the checks that need to be done at each path, this leads to the following, somewhat unsatisfying, conclusion:

Finding a more efficient algorithm to compute AC-u, that circumvents the need to enumerate all paths, is left for future work.

9.3 Algorithms for AC-m↩︎

As in Section 6.3, we only look at causes consisting of basic events, mostly for notational convenience. Theorem 10 was concerned with checking whether a given set of variables is a cause; now our task is to find all actual causes. this brings its own complications, since we are now looking for sets of events rather than just single events. At the same time, the fact that the problem is now purely about Boolean functions, rather than the graph structure, allows us to make use of existing methods for fault trees. In order to explain this, we first introduce the notion of minimal path sets, which are minimal sets of basic events whose nonfailure ensures continued system functioning:

MPS is the dual notion of MCS: the MPSs of \(T\) are precisely the MCSs of the dual FT \(\check{T}\) obtained by exchanging all AND-gates into OR-gates and vice versa (see Fig. 11). With this terminology and the notion of the positive part \(P_{T,\vec{u}}\), the following follows directly from Theorem 7:

Thus, finding all actual causes of \(X_{{\it Root}} = 1\) comes down to finding all MPS of \(P_{T,\vec{u}}\), which in turn comes down on finding all MCSs of \(\check{P}_{T,\vec{u}}\). Finding all MCSs is a core problem in FT analysis; an overview of existing approaches is given in [3]. These are typically worst-case exponential in the size of the FT, and differ in how well they perform on ‘typical’ FTs.

10 Related Work↩︎

Causal reasoning has gained significant traction in recent years, particularly in fields such as artificial intelligence, science, and engineering. Many approaches build on counterfactual notions of causality inspired by Lewis [27]. As in [27], determining whether \(A\) caused \(B\), involves evaluating a hypothetical scenario in which \(A\) did not occur and observing whether \(B\) would still take place. However, this counterfactual approach is often too weak to capture causality in robust systems where multiple failures are needed to cause system failure.

To address this issue, Halpern and Pearl introduced a more nuanced framework [9] based on structural models and Boolean equations. These, along with a set of formal conditions (commonly referred to as the AC conditions), characterise a cause of an outcome. This AC definition was later refined to account for richer causal scenarios [20]. These are particularly relevant to our investigation into the relationship between AC and causality in FTs.

Various other contributions build on AC to define liability frameworks for assessing responsibility, blame [28], and harm [29]. Frameworks such as [30], for instance, illustrate how AC can naturally be extended to address probabilistic causation as well. The work in [10] formalises interventions (and counterfactuals) based on the so-called do-operator. This captures interventions by modifying the structural model: it overrides specific functional dependencies with fixed values, while leaving the remainder of the model unaffected.

Beyond the philosophical community, AC has been connected in various ways to models of computation in more technical fields. In [31]–[33], for instance, the AC framework is applied to transition systems and trace-based models used to represent concurrent system behaviour. The work in [34] follows AC to define the causes responsible for the specification failure observed in counterexample traces. In [35], the authors propose an AC-inspired notion of causality in configurable systems, to determine those features (e.g., execution time) that cause a given undesired system behaviour. In [36], the do-operator [10] is used to define counterfactual-based tests for systems modeled as Bayesian Networks (BNs). This helped with speeding up the selection of the next diagnostic step in the root cause analysis of such systems. Moreover, BNs generalise FTs and can also be interpreted as structural causal models. However, computing conditional probabilities for formulas involving interventions, in the style of AC, presents significant challenges. Recent work, such as [37], explores a range of assumptions to enable the estimation of probabilities for interventional formulas in BNs.

In [19], causal models are extracted from attack trees [38] to support causal inference. While that work focuses on translating attack trees to CMs, we go beyond that by giving a full characterisation of AC as in [20] within FTs, and investigating the relation between AC and minimal cut sets, the main “causal” tool of FT analysis. An AC-based approach to extracting FTs encoding system failures was proposed in [18]. These trees are, in essence, a more compact way of encoding a set of counterexample traces witnessing the violation of a specification. In [18], such traces are considered causal based on an adoption of AC to the setting of state-based systems.

11 Conclusions↩︎

This paper offers a systematic study of fault trees from the perspective of the Halpern-Pearl framework of actual causality. We translate FTs to causal models, and classify actual causes in these models under the AC-o, AC-u and AC-m definitions. This shows how in FTs, causality arises as a combination of their Boolean nature and their graph structure. Using the different definitions, introduced in AC to capture multi-element causes (AC-u) and to simplify assessments (AC-m), gives us degrees to emphasize the role of the graph structure, and deepens our understanding of system failures.

We also study the relation between minimal cut sets and causality: MCSs are not causes, but being an element of an MCS is a sufficient condition for being a cause. Because of the role of the graph structure, it is only a necessary condition when the FT satisfies specific assumptions.

Our results lay the groundwork for integrating causal techniques like interventions and counterfactuals into FT analysis, enhancing diagnosis and explanation within a unified framework for reliability and failure analysis.

Our study opens several promising research directions. As an immediate next step, we will explore algorithmic methods for computing actual causes in FTs, focusing on the complexity of AC-o, AC-u and AC-m in practical cases. Second, a natural extension is to integrate probabilistic reasoning. Since Bayesian Networks generalise FTs and link closely to CMs, we aim to investigate how probabilistic fault analysis can benefit from our causality-based approach. Finally, our work paves the way for design-time causality analysis. Moving beyond post hoc diagnosis, we plan to explore how causality and responsibility can guide design decisions to reduce failures.

12 Proofs↩︎

In this appendix we prove the mathematical results of this paper. Before moving to the proofs proper, we reformulate causal models as graph causal models, the notation of which will be more suited for the mathematical proofs.

12.1 Graph causal models↩︎

For proving our results, it will be convenient to reformulate the definition of CM, as intricate mathematical reasoning can be tricky in the notation proposed in the main text. For example, for two variables \(X\) and \(Y\) the statement \(X=Y\) could mean that \(X\) and \(Y\) have the same value; that \(F_X(Y) = Y\); or that \(X\) and \(Y\) are the same element of the set \(\mathsf{U}^{{\textrm{i}} }\cup \mathsf{U}^{\textrm{c}}\). We therefore give a new definition which takes the underlying graph as the primordial object.

Each \(v \in \mathsf{V}\) is to be thought of as corresponding to a variable \(X_v\), which takes values in \(\mathcal{R}(v)\) (in the main text, we take \(\mathcal{R}(v) = \mathbb{B}\) throughout; we call such models binary graph causal models). The tuple of variables corresponding to a subset \(W \subseteq \mathsf{V}\) is denoted \(X_W\), which takes values of the form \(\mathcal{R}(W) := \prod_{w \in W} \mathcal{R}(w)\). Thus \(X_W = x_W\) denotes the fact that for each \(w \in W\), the variable \(X_w\) takes the value \(x_w\). Thus a context is an element \(\vec{u} \in \mathcal{R}(\mathsf{V}^{{\textrm{c}}})\) (for consistency with the main text, we keep contexts as \(\vec{u}\); its coefficients are written \(u_v\)).

To a graph causal model we associate a causal model as follows:

The transformation from graph causal models to causal models allows us to define the entire causality machinery on the level of graph causal models. For instance, if \(G = (\mathsf{V}^{{\textrm{c}}},\mathsf{V}^{{\textrm{i}}},\mathsf{E},\mathcal{R},F)\) is a graph causal model, \(W \subseteq \mathsf{V}^{{\textrm{i}}}\) is a set of internal nodes and \(x_W \in \mathcal{R}(W)\), then we define the intervention \(G_{X_W \leftarrow x_w}\) to be the graph causal model \(({\mathsf{V}^{{\textrm{i}}}}',{\mathsf{V}^{{\textrm{c}}}}',\mathsf{E}',\mathcal{R}',F')\) defined as \[\begin{align} {\mathsf{V}^{{\textrm{i}}}}' &= \mathsf{V}^{{\textrm{i}}},\\ {\mathsf{V}^{{\textrm{c}}}}' &= \mathsf{V}^{{\textrm{c}}},\\ \mathsf{E}' &= \mathsf{E}\setminus (\mathsf{V}\times W),\\ \mathcal{R}'(v) &= \mathcal{R}(v) \textrm{ for all v \in \mathsf{V}},\\ F'_v &\equiv x_v \textrm{ if v \in W,}\\ F'_v &= F_v \textrm{ otherwise.} \end{align}\] It is straightforward to check that this is the same as intervention on causal models:

Furthermore, it will be convenient to express \((M,\vec{u}) \models \varphi\) as a structure function, which we define as follows:

Because \((\mathsf{V},\mathsf{E})\) is a directed acyclic graph, this defines each \({\Phi}_{G}(\vec{u},v)\) uniquely. Intuitively, \({\Phi}_{G}(\vec{u},v)\) is the value \(X_v\) obtains in the causal model \(M_G\) under context \(\vec{u}\):

We write \({\Phi}_{G}(\vec{u},v)[X_W \leftarrow x_W]\) for \({\Phi}_{G[X_W \leftarrow x_w]}(\vec{u},v)\). By Lemmas 3 and 4, we have (in a somewhat confusing notation) \[(M_G,\vec{u}) \models [X_W \leftarrow x_w]\Big(X_v = {\Phi}_{G}(\vec{u},v)[X_W\leftarrow x_w]\Big).\]

12.2 Fault trees as graph causal models↩︎

If \(T = (V,E,\gamma)\) is a FT, then we define the associated graph causal model \(G_T = (\mathsf{V}^{{\textrm{c}}},\mathsf{V}^{{\textrm{i}}},\mathsf{E},\mathcal{R},F)\) as \[\begin{align} \mathsf{V}^{{\textrm{c}}}&= \{\tilde{v} \mid v \in \operatorname{BE}_{}\} \textrm{ is a disjoint copy of \operatorname{BE}_{}},\\ \mathsf{V}^{{\textrm{i}}}&= V,\\ \mathsf{E}&= E \cup \{(\tilde{v},v) \mid v \in \operatorname{BE}_{}\},\\ \mathcal{R}(v) &= \mathbb{B}\textrm{ for all v \in \mathsf{V}^{{\textrm{i}}}},\\ F_v &= \begin{cases} X_{\tilde{v}}, & \textrm{ if \gamma(v) = \mathtt{BE}},\\ \bigvee_{w \in {\it Inp}(v)} X_{w}, & \textrm{ if \gamma(v) = \mathtt{OR}},\\ \bigwedge_{w \in {\it Inp}(v)} X_{w}, & \textrm{ if \gamma(v) = \mathtt{AND}}. \end{cases} \end{align}\]

This is related to the causal model of a FT as follows:

In this notation, we get a more straightforward version of theorem 1:

12.3 Actual causality for graph causal models↩︎

We define AC-o, AC-u and AC-m for graph causal models; these are the exact counterparts of the definitions in Section 5.1.

It is straightforward to check that these are precisely the analoga of AC on causal models:

Likewise, the following result can be proven completely analogously to Theorem 2 (see [20]):

12.4 Proof of Theorem 5↩︎

Before we fully classify AC-o for FTs, we first prove an auxiliary lemma that simplifies Definition 14.1. It relies mainly on Theorem 14; in light of Proposition [prop:singleton], we only consider singleton causes. We also only consider causes for \(X_{{\it Root}} = 1\) in order to streamline our statements.

We use this lemma to prove the following analogon of Theorem 5 for graph causal models:

12.5 Proof of Theorem 6↩︎

Theorem 6 can be phrased in the language of graph causal models as follows:

The proof of Theorem 16 is to a large extent analogous to that of Theorem 15; we need two extra ingredients. The first is that AC-u only admits singleton causes:

The second ingredient is the following analogon to Lem 7. The proof is completely analogous, so we omit it.

Theorem 16 is now proven completely analogous to Theorem 15.

12.6 Proof of Theorem 7↩︎

In the graph causal model terminology, Theorem 7 becomes the following:

12.7 Proof of Theorem 8↩︎

In terms of graph causal models, Theorem 8 can be rephrased as follows:

12.8 Proof of Theorem 9↩︎

In terms of graph causal models, Theorem 9 can be rephrased as follows:

12.9 Proof of Theorem 10↩︎

We prove the statements for AC-o, AC-u and AC-m separately.

12.10 Proof of Theorem 11↩︎

We first prove correctness. In Remark [rmk:ptu], it is argued that a path of 1s that avoids all forbidden pairs of \(P := P_{T,\vec{u}}\) also avoids all forbidden pairs of \(T\). Therefore, \(X_v = 1\) is an actual cause (under AC-o) for \(X_{{\it Root}} = 1\) in \(T\) if and only if it is so in \(P_{T,\vec{u}}\). Now let \[\mathcal{H} = \{h \mid (h,l) \in \mathcal{F}(P)\}\] be the set of all high elements of forbidden pairs in \(P\). A straightforward induction from \({\it Root}\) downwards shows that for all \(H \subseteq \mathcal{H}\), we have \[\begin{align} H \in \mathcal{S}(v) \Leftrightarrow& \exists \textrm{ path } \pi\colon v \rightarrow {\it Root}\textrm{ s.t. } \pi \cap \mathcal{H} = \varnothing\\ & \textrm{and \pi contains no low elements corresponding to H.} \end{align}\] This means that a path \(v \rightarrow {\it Root}\) not containing both elements of a forbidden pair exists iff \(\mathcal{S}(v) \neq \varnothing\). It is precisely the inputs of such \(v\) that have a path as in Theorem 5, which shows that line 24 of Algorithm 9 returns the set of all \(v\) for which \(X_v = 1\) satisfies AC-o for \(X_{{\it Root}} = 1\).

Let us now consider its complexity. Computing \(P_{T,\vec{u}}\) requires computing \({\Phi}_{T}(\vec{u},v)\) for all \(v\), which takes \(\mathcal{O}(|E|)\) time. To find \(\mathcal{F}(P)\), we check every pair of edges to see whether they connect a forbidden pair to its shared child. There are \(|E|^2\) pairs to check, and each check takes \(\mathcal{O}(|V|)\) time since we need to see whether the high and low element are hierarchically related. Finally, to compute \(\mathcal{S}(v)\) for each \(v\), we pass along an element of \(\mathcal{P}(\mathcal{P}(\mathcal{F}(P)))\) along each edge, and this takes \(\mathcal{O}(2^{k}|E|)\) time. We conclude that this procedure as a whole has time complexity \(\mathcal{O}(|E|^2|V|+2^k|E|)\).

12.11 Proof of Theorem 12↩︎

We first compute \(P_{T,\vec{u}}\) (\(\mathcal{O}(|E|)\) time per Section 12.10), and we compute all its forbidden pairs (\(\mathcal{O}(|E|^2)\) time). To determine whether a given vertex \(v\) is an actual cause of \(X_{{\it Root}} = 1\) under AC-u, we first check whether \(v,{\it Root}\in P_{T,\vec{u}}\). Then, we enumerate all \(\mathcal{O}(2^{|V|})\) paths \(v \rightarrow {\it Root}\) in \(P_{T,\vec{u}}\). For each such path, we check whether setting all children of OR-gates to \(0\) changes the value of \(X_{{\it Root}}\) by recomputing \(P_{T,\vec{u}}\) (\(\mathcal{O}(|E|)\) time). Finally, we check if the path contains some forbidden pair (\(\mathcal{O}(|V|)\) time per pair for \(\mathcal{O}(|E|^2)\) pairs, so \(\mathcal{O}(|V||E|^2)\) time). Since we have to do this per path and per \(v\), the total computation time is

\[\mathcal{O}(|E|+|E|^2+2^{|V|}|V|(|E|+|V||E|^2|) = \mathcal{O}(2^{|V|}|V|^2|E|^2).\]

12.12 Proof of Theorem 13↩︎

By Lemma 2, it suffices to construct \(\check{P}_{T,\vec{u}}\) (\(\mathcal{O}(|E|)\) time per Section 12.10): if this does not contain \({\it Root}\), then \(X_{{\it Root}} = 1\) has no causes. If it does, we need to find all minimal cut sets of \(\check{P}_{T,\vec{u}}\). The MICSUP algorithm [5] computes all MCSs bottom-up, by storing a set of sets of BEs at each node (for details see [39]). Thus at every node we have \(\mathcal{O}(2^{|\operatorname{BE}_{T}|})\) sets that are communicated upwards once over each edge, at which point they are combined; this takes \(\mathcal{O}(2^{|\operatorname{BE}_{T}|}|E|)\) time. Thus the total time complexity is \(\mathcal{O}(|E|+2^{|\operatorname{BE}_{T}|}|E|) = \mathcal{O}(2^{|\operatorname{BE}_{T}|}|E|)\).

References↩︎

---

1. Interventions are often restricted to endogenous variables, as exogenous variables are considered given [20]. Mathematically, this restriction is not necessary.↩︎