Solving Queries for Boolean Fault Tree Logic via Quantified SAT

Explore a 25-minute video presentation from the FTSCS 2023 conference that delves into solving queries for Boolean Fault Tree Logic using Quantified SAT. Learn about the introduction of BFL (Boolean Logic for Fault trees) and its applications in fault tree analysis, including what-if scenarios, independence checks, and setting boundaries for failed elements. Discover how the researchers evaluate the usability of quantified Boolean formulae (QBFs) as an alternative to binary decision diagrams (BDDs) for checking BFL properties. Gain insights into the translation process from BFL to QBF and the implementation of the first tool for checking BFL properties using the Z3 solver. Examine the practical application through a case study and analyze runtime, memory consumption, and scalability on benchmark fault trees. Compare the qualitative differences between QBF and BDD-based approaches in this informative presentation by researchers from the University of Twente and Radboud University Nijmegen.