Solving Queries for Boolean Fault Tree Logic via Quantified SAT

被引:1
|
作者
Saaltink, Caz [1 ]
Nicoletti, Stefano M. [1 ]
Volk, Matthias [1 ]
Hahn, Ernst Moritz [1 ]
Stoelinga, Marielle [1 ,2 ]
机构
[1] Univ Twente, Enschede, Netherlands
[2] Radboud Univ Nijmegen, Nijmegen, Netherlands
来源
PROCEEDINGS OF THE 9TH ACM SIGPLAN INTERNATIONAL WORKSHOP ON FORMAL TECHNIQUES FOR SAFETY-CRITICAL SYSTEMS, FTSCS 2023 | 2023年
关键词
fault trees; QSAT; quantified Boolean formulae; BOUNDED MODEL CHECKING;
D O I
10.1145/3623503.3623535
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
Fault trees (FTs) are hierarchical diagrams used to model the propagation of faults in a system. Fault tree analysis (FTA) is a widespread technique that allows to identify the key factors that contribute to system failure. In recent work [26] we introduced BFL, a Boolean Logic for Fault trees. BFL can be used to formally define simple yet expressive properties for FTA, e.g.: 1) we can set evidence to analyse what-if scenarios; 2) check whether two elements are independent or if they share a child that can influence their status; 3) and set upper/lower boundaries for failed elements. Furthermore, we provided algorithms based on binary decision diagrams (BDDs) to check BFL properties on FTs. In this work, we evaluate usability of a different approach by employing quantified Boolean formulae (QBFs) instead of BDDs. We present a translation from BFL to QBF and provide an implementation-making it the first tool for checking BFL properties-that builds on top of the Z3 solver. We further demonstrate its usability on a case study FT and investigate runtime, memory consumption and scalability on a number of benchmark FTs. Lastly, qualitative differences from a BDD-based approach are discussed.
引用
收藏
页码:48 / 59
页数:12
相关论文
共 50 条
  • [11] Quantified computation tree logic
    Patthak, AC
    Bhattacharya, I
    Dasgupta, A
    Dasgupta, P
    Chakrabarti, PP
    INFORMATION PROCESSING LETTERS, 2002, 82 (03) : 123 - 129
  • [12] Second-Order Quantified Boolean Logic
    Jiang, Jie-Hong R.
    THIRTY-SEVENTH AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE, VOL 37 NO 4, 2023, : 4007 - 4015
  • [13] Satisfiability in Boolean Logic (SAT problem) is polynomial
    Rybakov, Vladimir V.
    JOURNAL OF SIBERIAN FEDERAL UNIVERSITY-MATHEMATICS & PHYSICS, 2021, 14 (05): : 667 - 671
  • [14] SOLVING QUERIES BY TREE PROJECTIONS
    SAGIV, Y
    SHMUELI, O
    ACM TRANSACTIONS ON DATABASE SYSTEMS, 1993, 18 (03): : 487 - 511
  • [15] Solving Exist-Random Quantified Stochastic Boolean Satisfiability via Clause Selection
    Lee, Nian-Ze
    Wang, Yen-Shi
    Jiang, Jie-Hong R.
    PROCEEDINGS OF THE TWENTY-SEVENTH INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE, 2018, : 1339 - 1345
  • [16] FPGA logic synthesis using Quantified Boolean Satisfiability
    Ling, A
    Singh, DP
    Brown, SD
    THEORY AND APPLICATIONS OF SATISFIABILITY TESTING, PROCEEDINGS, 2005, 3569 : 444 - 450
  • [17] Epistemic Quantified Boolean Logic: Expressiveness and Completeness Results
    Belardinelli, Francesco
    van der Hoek, Wiebe
    PROCEEDINGS OF THE TWENTY-FOURTH INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE (IJCAI), 2015, : 2748 - 2754
  • [18] A Sharp Leap from Quantified Boolean Formula to Stochastic Boolean Satisfiability Solving
    Chen, Pei-Wei
    Huang, Yu-Ching
    Jiang, Jie-Hong R.
    THIRTY-FIFTH AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE, THIRTY-THIRD CONFERENCE ON INNOVATIVE APPLICATIONS OF ARTIFICIAL INTELLIGENCE AND THE ELEVENTH SYMPOSIUM ON EDUCATIONAL ADVANCES IN ARTIFICIAL INTELLIGENCE, 2021, 35 : 3697 - 3706
  • [19] Consistent Answers of Aggregation Queries via SAT
    Dixit, Akhil A.
    Kolaitis, Phokion G.
    2022 IEEE 38TH INTERNATIONAL CONFERENCE ON DATA ENGINEERING (ICDE 2022), 2022, : 924 - 937
  • [20] Solving dependency quantified Boolean formulas using quantifier localization
    Ge-Ernst, Aile
    Scholl, Christoph
    Sic, Juraj
    Wimmer, Ralf
    THEORETICAL COMPUTER SCIENCE, 2022, 925 : 1 - 24