When: Thursday, May 12, 2022, 9am (CEST).

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

Topic: Best-effort synthesis

Speaker: Prof. Sasha Rubin, Senior Lecturer, Leader of the Computational Logic for Artificial Intelligence (LOGIC-AI) group in the School of Computer Science, The University of Sydney.

Abstract

In the classic formulation (Pnueli and Rosner 1989), the synthesis problem concerns finding an agent strategy that guarantees that a specification formula expressed in linear-time temporal logic (LTL) is satisfied irrespective of the actions of the environment (this can be seen as an analogue of Planning with temporally extended goals in AI).

What should an agent do when it can’t achieve its task in all circumstances? In the classic formulation the agent ‘gives up’ (i.e., the synthesis procedure returns ‘unsynthesisable’). However, what if giving up is not acceptable? One idea might be to do as well as possible, i.e., do a ‘best effort’. In this talk I will offer a formalisation of what it means that an agent strategy does a best effort, and discuss how to algorithmically solve such synthesis problems using automata-theory.

This talk is based on joint works with Benjamin Aminof, Giuseppe De Giacomo, Alessio Lomuscio, and Aniello Murano.

Short Bio

Sasha Rubin is a Senior Lecturer and the Leader of the Computational Logic for Artificial Intelligence (LOGIC-AI) group in the School of Computer Science, The University of Sydney. His main interest is in Logic and Formal Methods for AI. In particular: Foundations of synthesis and planning for temporally extended goals, Logics for games and strategic reasoning, multiplayer games, imperfect information, incomplete information, Formal methods for multi-agent systems Automata theory, Finite and algorithmic model theory.