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

翻译：安全关键基础设施必须以安全可靠的方式运行。故障树分析是用于评估这些系统风险的广泛方法：例如，美国联邦航空管理局和核管理委员会要求使用故障树。尽管故障树广受欢迎，但在构建关于故障树的结构化查询并对其进行分析（例如，评估潜在场景）方面，以及为从业者提供易懂且强大的工具来对故障树进行查询方面，相关研究仍较少。本文旨在通过扩展BFL [32]（一种关于布尔故障树的逻辑）来填补这一空白。为此，我们提出了一种概率故障树逻辑（PFL）。PFL是一种简单而富有表现力的逻辑，支持更轻松地制定复杂场景以及指定包含概率的故障树属性。与PFL一同，我们介绍了LangPFL，一种领域特定语言，以进一步简化属性指定。我们通过将PFL和LangPFL应用于一个与新冠相关的故障树以及一个用于油气管道的故障树来展示其功能。最后，我们介绍了基于二元决策图（BDD）的理论和模型检测算法。