Extended bounded response LTL: a new safety fragment for efficient reactive synthesis

Reactive synthesis is a key technique for the design of correct-by-construction systems, which has been thoroughly investigated in the last decades. It consists of 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 limits their scalability. In this paper, we introduce a new safety fragment of Linear Temporal Logic (LTL), called Extended Bounded Response LTL (LTLEBR), which allows one to combine bounded and universal unbounded temporal operators (thus covering a large set of practical cases). 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 approach and study the complexity of the fragment showing that the proposed solution is optimal. Finally, we evaluate it on various benchmarks showing better performance of other approaches for general LTL or larger safety fragments.