# Reactive Synthesis from Extended Bounded Response LTL Specifications

arXiv: https://arxiv.org/abs/2008.05335 · HTML: https://mlsanity.com/paper/2008.05335/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 12 Aug 2020.

## Built on by (most cited first, 2 of 2)

- [LTLf+ and PPLTL+: Extending LTLf and PPLTL to Infinite Traces](https://mlsanity.com/paper/2411.09366/) (2024)
- [Planning for Temporally Extended Goals in Pure-Past Linear Temporal Logic: A Polynomial Reduction to Standard Planning](https://mlsanity.com/paper/2204.09960/) (2022)

## Abstract (arXiv)

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.