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
a best effort, and discuss how to algorithmically solve such
synthesis problems using graph algorithms.
This talk is based on joint works with Benjamin Aminof,
Giuseppe De Giacomo, Alessio Lomuscio, and Aniello Murano,
presented at IJCAI21 and KR21.
09/06/2022