\(\textsf{PFL}\): A Probabilistic Logic for Fault Trees

Safety-critical infrastructures must operate in a safe and reliable way. Fault tree analysis is a widespread method used for risk assessment of these systems: fault trees (FTs) are required by, e.g., the Federal Aviation Administration and the Nuclear Regulatory Commission. In spite of their popularity, little work has been done on formulating structural queries about \(\textsc {ft} \textrm{s}\) and analyzing these, e.g., when evaluating potential scenarios, and to give practitioners instruments to formulate queries on \(\textsc {ft} \textrm{s}\) in an understandable yet powerful way. In this paper, we aim to fill this gap by extending \( BFL \) [37], a logic that reasons about Boolean \(\textsc {ft} \textrm{s}\). To do so, we introduce a Probabilistic Fault tree Logic (\(\textsf{PFL}\)). \(\textsf{PFL}\) is a simple, yet expressive logic that supports easier formulation of complex scenarios and specification of FT properties that comprise probabilities. Alongside \(\textsf{PFL}\), we present \(\textsf{LangPFL}\), a domain specific language to further ease property specification. We showcase \(\textsf{PFL}\) and \(\textsf{LangPFL}\) by applying them to a COVID-19 related FT and to a FT for an oil/gas pipeline. Finally, we present theory and model checking algorithms based on binary decision diagrams (BDDs).

1. 1.

   When considering conditional probabilities in layer-two and layer-three formulae, we disregard the case in which \(\varPhi ^*_\textit{T} (\mu _{\overline{\rho \,}}, \phi ') = 0\).

Authors and Affiliations

1. Formal Methods and Tools, University of Twente, Enschede, The Netherlands

   Stefano M. Nicoletti, Milan Lopuhaä-Zwakenberg, E. Moritz Hahn & Mariëlle Stoelinga

2. Department of Software Science, Radboud University, Nijmegen, The Netherlands

   Mariëlle Stoelinga

Corresponding author

Correspondence to Stefano M. Nicoletti .

Editors and Affiliations

1. University of Toronto, Toronto, ON, Canada

   Marsha Chechik

2. RWTH Aachen University, Aachen, Germany

   Joost-Pieter Katoen

3. University of Lübeck, Lübeck, Germany

   Martin Leucker

A Appendix: Algorithms and Additional Definitions for Layer One Formulae

Following, operations between \(\textsc {bdd} \textrm{s}\) are represented by bold operands e.g., \(\boldsymbol{\wedge }, \boldsymbol{\vee } \). Algorithms to conduct these operations on \(\textsc {bdd} \textrm{s}\) can be found in [2, 5]. Given a set of variables \(\texttt{V} = \{v_1, \ldots ,v_n\}\), existential quantification (needed to translate part of the semantics of \(\textrm{MCS}\) operator) can be defined as follows: \(\boldsymbol{\exists } v . \boldsymbol{\textrm{B}} = \textsc {Restrict}(\boldsymbol{\textrm{B}},v, 0) \boldsymbol{\vee } \textsc {Restrict}(\boldsymbol{\textrm{B}},v, 1)\); \(\boldsymbol{\exists } V . \boldsymbol{\textrm{B}} = \boldsymbol{\exists } v_1. \boldsymbol{\exists } v_2 . \,\ldots \, \boldsymbol{\exists } v_n . \boldsymbol{\textrm{B}} \).

1.1 A.1 Translating FTs to BDDs

\( \varPsi _{FT} \) is defined as follows:

Definition 7

The translation function of a FT T is a function \( \varPsi _{FT_{\textit{T}}} :\texttt{E} \rightarrow \texttt{BDD} \) that takes as input an element \(e\in \texttt{E} \). With \(e'\in ch (e)\), we can define \( \varPsi _{FT_{\textit{T}}} \):

where \(\overline{\boldsymbol{\textrm{B}}}(v)\) is a BDD with a single node in which \( Low (v)=\mathtt {{0}}\) and \( High (v)=\mathtt {{1}}\).

1.2 A.2 Algorithm 5: Translating FTs/Formulae to BDDs

Following, the recursion scheme taken from [37] to translate \(\textsc {ft} \textrm{s}\) and layer one formulae is presented.

where \(\underline{\boldsymbol{\textrm{B}}} _\textit{T} (\phi )[\texttt{V} \curvearrowright \mathtt {V'} ]\) indicates the \(\textsc {bdd}\) \(\underline{\boldsymbol{\textrm{B}}} _\textit{T} (\phi )\) in which every variable \(v_k\in \texttt{V} \) is renamed to its primed \(v'_k\in \mathtt {V'} \).

1.3 A.3 Algorithm 6: Model Checking \(\textsf{PFL}\) over a FT and a \(\overline{b\,}\)

Overview. As per [37], given a specific vector \(\overline{b}\), a \(\textsc {ft}\) \(\textit{T} \) and a layer one formula \(\phi \), this algorithm showcases how to check if \(\overline{b\,}, \textit{T} \models \phi \). To do so, we translate the given formula to a \(\textsc {bdd}\) and then we walk down the \(\textsc {bdd}\) from the root node following truth assignments given in the specific vector \(\overline{b\,}\).

Algorithm 6. Algorithm 6 shows an algorithm to check whether \(\overline{b\,},\textit{T} \models \phi \), given a status vector \(\overline{b\,}\), a \(\textsc {ft}\) \(\textit{T} \) and a formula \(\phi \). A \(\textsc {bdd}\) for the formula \(\phi \) is computed with regard to the structure function of the given \(\textsc {ft}\) \(\textit{T} \) i.e., we compute \(\underline{\boldsymbol{\textrm{B}}} _\textit{T} (\phi )\) as per Algorithm 5. Subsequently, the algorithm walks down the \(\textsc {bdd}\) following the Boolean assignments given in \(\overline{b\,}\): if the i-th element of \(\overline{b\,}\) is set to 0 then the next node in the path will be given by \( Low (w_i)\), if it is set to 1 then the next node will be \( High (w_i)\). When the algorithm reaches a terminal node it returns True if its value is one - i.e., if \(\overline{b\,},\textit{T} \models \phi \) - and False otherwise.

1.4 A.4 Algorithm 7: Computing all Satisfying Vectors

Overview. Given a \(\textsc {ft}\) \(\textit{T} \) and a formula \(\phi \), we now want to compute all vectors \(\overline{b}\) such that \(\overline{b\,}, \textit{T} \models \phi \). In this scenario no Boolean vector is given. Thus, we need to construct the \(\textsc {bdd}\) for the given formula and then collect every path that leads to the terminal \(\mathtt {{1}}\) to compute all satisfying vectors \({\llbracket {\overline{b\,}}\rrbracket }_\textit{T} \) for the given formula.

Algorithm 7. To achieve the desired outcome we will construct the \(\textsc {bdd}\) \(\underline{\boldsymbol{\textrm{B}}} _\textit{T} (\phi )\) for the given formula following Algorithm 5. Then, the algorithm will walk down the \(\textsc {bdd}\) and store all the paths that lead to the terminal node \(\mathtt {{1}}\). These paths represent all the status vectors that satisfy our formula \(\phi \). The value for the elements of each vector is set to 0 or 1 if the stored path follows respectively the low or high edge of the collected elements of the \(\textsc {bdd}\). After computing the \(\textsc {bdd}\) for a given \(\phi \), AllSat [2] will achieve the desired outcome. This algorithm returns exactly all the satisfying assignments for a given \(\textsc {bdd}\), i.e., in our case, all the Boolean vectors that satisfy our formula.

B Appendix: Proofs

1.1 B.1 Proof for Theorem 1

Proof

For a layer one formula \(\phi \) and \(\overline{\rho \,}\in B\), one can express

This is a polynomial in the n variables \(\rho _i\). Each summand has degree 1 in each \(\rho _i\), hence \(\varPhi ^*_\textit{T} (\mu _{\overline{\rho \,}},\phi )\) can be written as

for some constants \(c^h_w \in \mathbb {R}\). Now fix an i, and let \(\phi ,\phi '\) be two Boolean formulae; then we can write \(\frac{\varPhi ^*_\textit{T} (\mu _{\overline{\rho \,}},\phi \wedge \phi ')}{\varPhi ^*_\textit{T} (\mu _{\overline{\rho \,}},\phi ')} = \frac{A\rho _i + B}{C\rho _i + D}\) for some polynomials A, B, C, D in the variables \(\rho _1,\ldots ,\rho _{i-1},\rho _{i+1},\ldots ,\rho _n\). In particular, we have

The sign of this partial derivative does not depend on the value of \(\rho _i\). In particular, when all other \(\rho _{i'}\) are fixed, this expression is maximized on an interval when \(\rho _i\) is at one of the boundary points of that interval.

Now let us return to the setting of the Theorem; we will prove it for the maximum only as the minimum is proved analogously. Let Let \(B = \prod _i [l_i,u_i]\) and let \(\overline{\rho \,}\in \prod _i [l_i^{-1},l_i^{+}]\); our aim is to find a vertex \(\overline{\rho \,}'\) such that \(\frac{\varPhi ^*_\textit{T} (\mu _{\overline{\rho \,}},\phi \wedge \phi ')}{\varPhi ^*_\textit{T} (\mu _{\overline{\rho \,}},\phi ')} \le \frac{\varPhi ^*_\textit{T} (\mu _{\overline{\rho \,}'},\phi \wedge \phi ')}{\varPhi ^*_\textit{T} (\mu _{\overline{\rho \,}'},\phi ')}\). To do so, we construct a sequence \(\overline{\rho \,}_0,\overline{\rho \,}_1,\ldots ,\overline{\rho \,}_n\) with the following properties:

1. 1.

   \(\overline{\rho \,}_0 = \overline{\rho \,}\);

2. 2.

   \(\frac{\varPhi ^*_\textit{T} (\mu _{\overline{\rho \,}_i},\phi \wedge \phi ')}{\varPhi ^*_\textit{T} (\mu _{\overline{\rho \,}_i},\phi ')} \le \frac{\varPhi ^*_\textit{T} (\mu _{\overline{\rho \,}_{i+1}},\phi \wedge \phi ')}{\varPhi ^*_\textit{T} (\mu _{\overline{\rho \,}_{i+1}},\phi ')}\) for \(i < n\);

3. 3.

   \(\rho _{i,i'} \in \{l_{i'},u_{i'}\}\) for \(i' \le i \le n\).

This ensures that \(\overline{\rho \,}' := \overline{\rho \,}_n\) has the required property. We define each \(\overline{\rho \,}_{i}\) from \(\overline{\rho \,}_{i-1}\) as follows: define \(\overline{\rho \,}_{i}^-,\overline{\rho \,}_i^+ \in [l_i,u_i]\) by

By the discussion following (3), one has \(\frac{\varPhi ^*_\textit{T} (\mu _{\overline{\rho \,}_{i}},\phi \wedge \phi ')}{\varPhi ^*_\textit{T} (\mu _{\overline{\rho \,}_{i}},\phi ')} \le \max \left\{ \frac{\varPhi ^*_\textit{T} (\mu _{\overline{\rho \,}_{i+1}^-},\phi \wedge \phi ')}{\varPhi ^*_\textit{T} (\mu _{\overline{\rho \,}_{i+1}^-},\phi ')},\frac{\varPhi ^*_\textit{T} (\mu _{\overline{\rho \,}_{i+1}^+},\phi \wedge \phi ')}{\varPhi ^*_\textit{T} (\mu _{\overline{\rho \,}_{i+1}^+},\phi ')}\right\} \). Take \(\overline{\rho \,}_{i+1} \in \{\overline{\rho \,}^-_{i+1}\), \(\overline{\rho \,}^+_{i+1}\}\) to maximize \(\frac{\varPhi ^*_\textit{T} (\mu _{\overline{\rho \,}_{i+1}},\phi \wedge \phi ')}{\varPhi ^*_\textit{T} (\mu _{\overline{\rho \,}_{i+1}},\phi ')}\), then this satisfies conditions 1–3 above.

Reprints and permissions

© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG

Policies and ethics