Dipartimento di Informatica

Titolo: LTLf Synthesis under Environment Specifications

Abstract: Reactive Synthesis is one of the most appealing and challenging problem in computer science. It involves automatically building correct-by-design programs that exhibit desired behaviours given a set of formal specifications. Recent advances in the synthesis of Linear Temporal Logics on finite traces (LTLf) have pioneered the way for practical implementation and scalability of this approach, marking a significant step forward in the field. In this talk, I will show some recent progress in synthesis for agent goals specified in LTLf under environment specifications. In synthesis, environment specifications are constraints on the environments that rule out certain environment behaviour. To solve synthesis of LTLf goals under environment specifications, we could reduce the problem to LTL synthesis. Unfortunately, while synthesis in LTLf and in LTL have the same worst-case complexity (both are 2EXPTIME-complete), the algorithms available for LTL synthesis are much harder in practice than those for LTLf synthesis. I will show some results that avoid this detour while maintaining the simplicity of LTLf.

Bio: Antonio Di Stasio is a Lecturer in the Department of Computer Science at City, St George’s, University of London. Additionally, he is an Associate Member of the Department of Computer Science at the University of Oxford and member of the common room at Kellogg College, University of Oxford. His primary research interests include automated reasoning, computer-aided verification, knowledge representation, and temporal logic on finite and infinite traces (LTL and LTLf). Before joining City, Antonio was a Senior Research Associate in the Department of Computer Science at the University of Oxford, where he collaborated with Prof. Giuseppe De Giacomo on the Advanced ERC project WhiteMech. Antonio earned his Ph.D. in Mathematical and Computer Science from the University of Napoli "Federico II" (Italy), under the supervision of Prof. Aniello Murano. During his Ph.D., he was also a visiting research scholar at Rice University, working under the guidance of Prof. Moshe Vardi.