PFL: A Probabilistic Logic for Fault Trees

Research output: Chapter in Book/Report/Conference proceedingChapterAcademicpeer-review

2 Citations (Scopus)
45 Downloads (Pure)


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).

Original languageEnglish
Title of host publicationFormal Methods
Subtitle of host publication25th International Symposium, FM 2023, Lübeck, Germany, March 6–10, 2023, Proceedings
EditorsMarsha Chechik, Joost-Pieter Katoen, Martin Leucker
Place of PublicationCham
PublisherSpringer Nature
Number of pages23
ISBN (Electronic)978-3-031-27481-7
ISBN (Print)978-3-031-27480-0
Publication statusPublished - 3 Mar 2023
Event25th International Symposium on Formal Methods, FM 2023 - Lübeck, Germany
Duration: 6 Mar 202310 Mar 2023
Conference number: 25

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference25th International Symposium on Formal Methods, FM 2023
Abbreviated titleFM


  • 2023 OA procedure


Dive into the research topics of 'PFL: A Probabilistic Logic for Fault Trees'. Together they form a unique fingerprint.

Cite this