University of Twente Student Theses


Symbolic LTL Reactive Synthesis

Abraham, R. (2021) Symbolic LTL Reactive Synthesis.

[img] PDF
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:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page