When: Thursday, March 31, 2022, 3pm (CEST).

Where: Zoom online, check the address in the Google Calendar Event.

Topic: Symbolic Reactive Synthesis from Extended Bounded Response LTL+P Specifications

Speaker: Dr. Luca Geatti, postdoc researcher in Computer Science at the Free University of Bozen/Bolzano.

Abstract

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, that limit their scalability.

In this talk, we introduce a new safety fragment of Linear Temporal Logic with Past (LTL+P), called Extended Bounded Response LTL with Past (LTLEBR+P), which allows one to combine bounded and universal unbounded temporal operators (thus covering a large set of practical cases).

First, we study the expressive power of LTLEBR+P, showing that it can express all and only the safety properties definable in LTL+P. Second, we show that reactive synthesis from LTLEBR+P specifications can be reduced to solving a safety game over a deterministic symbolic automaton built directly from the specification. Third, we study the theoretical complexity of the fragment showing that the proposed solution is optimal and we evaluate it on various benchmarks showing better performance with respect to other approaches for general LTL or larger safety fragments.

Short Bio

Luca Geatti is a postdoc researcher in Computer Science at the Free University of Bozen/Bolzano. His research interests span automata theory, temporal logics, automatic synthesis, reactive synthesis and formal verification.

Material