University of Twente Student Theses
Solving BFL Queries: From BDDs to Quantified SAT
Saaltink, Caz (2023) Solving BFL Queries: From BDDs to Quantified SAT.
|
PDF
898kB |
| 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: | https://purl.utwente.nl/essays/95880 |
| Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Show download statistics for this publication
Show download statistics for this publicationRepository Staff Only: item control page