University of Twente Student Theses
Symbolic LTL Reactive Synthesis
Abraham, R. (2021) Symbolic LTL Reactive Synthesis.
PDF
1MB |
Abstract: | Synthesis is a technique to arrive at provably correct systems by constructing them directly from their specification. We consider the synthesis of reactive systems, which are systems that continuously "react" to events in their environment (e.g. communication protocols, embedded controllers etc.). Unfortunately, reactive synthesis suffers from scalability issues due to the state space explosion problem. Symbolic techniques using binary decision diagrams can be used to improve this scalability. We investigate a symbolic approach based on the temporal logic hierarchy in a new prototypical tool Otus and compare it against the current state of the art. |
Item Type: | Essay (Master) |
Faculty: | EEMCS: Electrical Engineering, Mathematics and Computer Science |
Subject: | 54 computer science |
Programme: | Computer Science MSc (60300) |
Link to this item: | https://purl.utwente.nl/essays/87386 |
Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Repository Staff Only: item control page