When: Thursday, March 11, 2021, 3pm (GMT+1).

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

Topic: Synthesis Problems for Prompt Linear Temporal Logic.

Speaker: Bastien Maubert, Postdoctoral Fellow at the Università degli Studi di Napoli Federico II

Abstract

In LTL, formula F p ensures that p will eventually be true at some point in the future, but it does not tell us anything about how far this moment may be. And formula G request -> F granted tells us that every request will eventually be granted, which is a classic requirement for a correct system (think of a printing server for instance); but the waiting time between the moment in which a request is made and the moment it is satisfied may grow arbitrarily large and still the formula would hold. There is no way in LTL to prevent this kind of behaviour. Prompt-LTL extends LTL with an operator of “bounded eventuality” that serves this purpose. In this talk I will present recent results concerning synthesis problems for Prompt LTL. In particular I will first focus on the problem of Assume-Guarantee Synthesis for Prompt-LTL, which remained open for a decade, and that we solved last year. Then I will move to logics for strategic reasoning, in particular Strategy Logic (SL), whose model-checking problem subsumes a number of synthesis problems. I will present extensions of SL with operators to bound the waiting time and operators to bound the number of “bad” executions, and give an idea of how we can model-check this logic. I will also briefly present cost functions and cost automata, which are a central tool to solve both problems.

Short Bio

Bastien Maubert obtained his PhD in 2014 at Université de Rennes 1. It was prepared in the team LogicA at IRISA, under the supervision of Sophie Pinchinat and Guillaume Aucher. He has then been a postdoctoral fellow at LORIA in Nancy, in Hans van Ditmarsch’ team CELLO (Computational Epistemic Logic in Lorraine), working on his ERC project Epistemic Protocol Synthesis. In 2016 he moved to Università degli Studi di Napoli “Federico II”, in Aniello Murano’s group, to work on the project LoGIcInMAS (Logics and Games for Imperfect Information in Multi-Agent Systems), for which he obtained a Marie-Curie Individual Fellowship. He is currently still working in Napoli as a postdoctoral fellow.

His research interests include logics dealing with knowledge and strategic abilities (epistemic, temporal, dynamic, alternating, strategic logics…), game theory, in particular games with imperfect information, automatic and rational structures, automata theory, and in general he is interested in problems dealing with the security of systems (program verification, program synthesis…).