\textsf{PFL}: a probabilistic logic for fault trees

DOI10.1007/978-3-031-27481-7_13MaRDI QIDQ6174535zbMATH OpenOpenAlexFDO

Authors Stefano M. Nicoletti, Milan Lopuhaä-Zwakenberg, Ernst Moritz Hahn, Mariëlle I. A. Stoelinga

Publication date 17 August 2023

Published in Formal Methods (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2303.17314

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: 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 FT and analyzing these, e.g., when evaluating potential scenarios, and to give practitioners instruments to formulate queries on FTs in an understandable yet powerful way. In this paper, we aim to fill this gap by extending BFL [32], a logic that reasons about Boolean FTs. To do so, we introduce a Probabilistic Fault tree Logic (PFL). PFL is a simple, yet expressive logic that supports easier formulation of complex scenarios and specification of FT properties that comprise probabilities. Alongside PFL, we present LangPFL, a domain specific language to further ease property specification. We showcase PFL and 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).

Recommendations

• Formal fault tree analysis -- practical experiences
• Fault tree analysis: a survey of the state-of-the-art in modeling, analysis and tools
• Symbolic Fault Tree Analysis for Reactive Systems
• Sensitivity investigation of fault tree analysis with matrix-algebraic method

Cites work

• \texttt{SMT-RAT}: an open source \texttt{C++} toolbox for strategic and parallel SMT solving
• A Compositional Semantics for Dynamic Fault Trees in Terms of Interactive Markov Chains
• A logic for reasoning about time and reliability
• Accelerated model checking of parametric Markov chains
• Convex Optimization for Parameter Synthesis in MDPs
• Discrete Linear-time Probabilistic Logics: Completeness, Decidability and Complexity
• Fault tree analysis: a survey of the state-of-the-art in modeling, analysis and tools
• scientific article; zbMATH DE number 3870578 (Why is no real title available?)
• Mathematical Logic for Computer Science
• Model-checking in dense real-time
• The probabilistic model checking landscape

This page was built for publication: \textsf{PFL}: a probabilistic logic for fault trees

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6174535)