University of Twente Student Theses


Solving BFL Queries: From BDDs to Quantified SAT

Saaltink, Caz (2023) Solving BFL Queries: From BDDs to Quantified SAT.

[img] PDF
Abstract:Fault trees are used to analyse the propagation of faults in a system. They also allow for fault tree analysis, which can be used to analyse the key factors that impact system failure. Recently, Nicoletti et al. introduced a new logic called BFL to reason about fault trees. BFL can be used to formally define properties of fault trees. The paper also provides algorithms for BFL, for example, to check whether properties written in BFL hold. All algorithms make use of BDDs, which can use exponential space and time in the number of basic events of the tree. To combat this problem, this work will aim to use quantified Boolean formulas (QBF) instead of BDDs. The algorithms provided by Nicoletti et al. will be replaced with an algorithm that translates BFL to QBF and then uses a QBF solver. This approach is implemented—also marking the first-ever BFL implementation—and it is demonstrated in a case study. Furthermore, qualitative differences from a BDD-based approach are discussed.
Item Type:Essay (Bachelor)
Faculty:EEMCS: Electrical Engineering, Mathematics and Computer Science
Subject:54 computer science
Programme:Computer Science BSc (56964)
Link to this item:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page