%0 Conference Paper %1 nicoletti2023PFL %A Nicoletti, Stefano M. %A Lopuhaä-Zwakenberg, Milan %A Hahn, E. Moritz %A Stoelinga, Mariëlle %B Formal Methods. FM 2023 %C Cham %D 2023 %I Springer %K 03b70-logic-in-computer-science 68q60-specification-and-verification 90b25-reliability-availability-maintenance-inspection fault-tree-analysis %P 199--221 %R 10.1007/978-3-031-27481-7_13 %T PFL: a probabilistic logic for fault trees %U https://link.springer.com/chapter/10.1007/978-3-031-27481-7_13 %V 14000 %X 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 and analyzing these, e.g., when evaluating potential scenarios, and to give practitioners instruments to formulate queries on in an understandable yet powerful way. In this paper, we aim to fill this gap by extending 37, a logic that reasons about Boolean . To do so, we introduce a Probabilistic Fault tree Logic ( ). is a simple, yet expressive logic that supports easier formulation of complex scenarios and specification of FT properties that comprise probabilities. Alongside , we present , a domain specific language to further ease property specification. We showcase and 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). %@ 978-3-031-27480-0; 978-3-031-27481-7

@inproceedings{nicoletti2023PFL, 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 and analyzing these, e.g., when evaluating potential scenarios, and to give practitioners instruments to formulate queries on in an understandable yet powerful way. In this paper, we aim to fill this gap by extending [37], a logic that reasons about Boolean . To do so, we introduce a Probabilistic Fault tree Logic ( ). is a simple, yet expressive logic that supports easier formulation of complex scenarios and specification of FT properties that comprise probabilities. Alongside , we present , a domain specific language to further ease property specification. We showcase and 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).}, added-at = {2024-07-05T05:58:21.000+0200}, address = {Cham}, author = {Nicoletti, Stefano M. and Lopuhaä-Zwakenberg, Milan and Hahn, E. Moritz and Stoelinga, Mari{\"e}lle}, biburl = {https://www.bibsonomy.org/bibtex/22d63d1d65731b3c6409c1a5736297f5d/gdmcbain}, booktitle = {Formal Methods. FM 2023}, doi = {10.1007/978-3-031-27481-7_13}, eventdate = {March 6--10, 2023}, eventtitle = {Formal Methods}, interhash = {ed0848226d883cbad75f89446deff6bd}, intrahash = {2d63d1d65731b3c6409c1a5736297f5d}, isbn = {978-3-031-27480-0; 978-3-031-27481-7}, keywords = {03b70-logic-in-computer-science 68q60-specification-and-verification 90b25-reliability-availability-maintenance-inspection fault-tree-analysis}, language = {en}, pages = {199--221}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, timestamp = {2024-07-05T06:03:41.000+0200}, title = {{PFL}: a probabilistic logic for fault trees}, url = {https://link.springer.com/chapter/10.1007/978-3-031-27481-7_13}, venue = {Lübeck, Germany}, volume = 14000, year = 2023, zbl = {1529.68162}, zbmath = {7728844} }