Reactive Synthesis from Extended Bounded Response LTL Specifications

TL;DR

This paper introduces a new fragment of Linear Temporal Logic, extit{Extended Bounded Response LTL}, enabling more scalable reactive synthesis by reducing it to safety games over deterministic symbolic automata.

Contribution

It defines extit{Extended Bounded Response LTL} and demonstrates how synthesis from this fragment can be efficiently performed via safety games, improving scalability.

Findings

Successfully reduces synthesis to safety games over deterministic automata.

Proves correctness of the approach.

Evaluates effectively on various benchmarks.

Abstract

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.