Reactive Synthesis from Extended Bounded Response LTL Specifications
This work addresses the problem of scalable reactive synthesis for system designers, offering a practical solution for a large set of cases, though it is incremental as it builds on existing temporal logic and synthesis methods.
The paper tackles the scalability limitations of reactive synthesis for correct-by-construction systems by introducing Extended Bounded Response LTL (LTLEBR), a new fragment of Linear Temporal Logic that combines bounded and unbounded temporal operators, and shows that synthesis from LTLEBR specifications reduces to solving safety games over deterministic symbolic automata, with successful evaluation on benchmarks.
Reactive synthesis is a key technique for the design of correct-by-construction systems and has been thoroughly investigated in the last decades. It consists in the synthesis of a controller that reacts to environment's inputs satisfying a given temporal logic specification. Common approaches are based on the explicit construction of automata and on their determinization, which limit their scalability. In this paper, we introduce a new fragment of Linear Temporal Logic, called Extended Bounded Response LTL (\LTLEBR), that allows one to combine bounded and universal unbounded temporal operators (thus covering a large set of practical cases), and we show that reactive synthesis from \LTLEBR specifications can be reduced to solving a safety game over a deterministic symbolic automaton built directly from the specification. We prove the correctness of the proposed approach and we successfully evaluate it on various benchmarks.