Symbolic LTL Reactive Synthesis

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.