Paper Info
Title
Reactive Synthesis from Extended Bounded Response LTL Specifications
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 (LTL <sub xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">EBR</sub> ), 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 LTL <sub xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">EBR</sub> 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.
Year
DOI
Venue
2020
10.34727/2020/isbn.978-3-85448-042-6_15
2020 Formal Methods in Computer Aided Design (FMCAD)
Keywords
DocType
ISSN
extended bounded response LTL,EBR specifications,universal unbounded temporal operators,linear temporal logic,temporal logic specification,correct-by-construction systems,reactive synthesis
Conference
2641-8177
ISBN
Citations 
PageRank 
978-1-7281-5633-0
0
0.34
References 
Authors
15
5
Name
Order
Citations
PageRank
Alessandro Cimatti15064323.15
G. De Luca2136.55
Nicola Gigante342.12
Angelo Montanari41535135.04
Stefano Tonetta501.69