Course Description
Objectives. This course introduces AI planning and program synthesis for tasks (goals) expressed over finite traces instead of states. Specifically, borrowing from Formal Methods, we will consider tasks and environment specifications expressed in LTL and in particular its finite trace variant LTLf. We will review the main results and algorithmic techniques to handle planning in nondeterministic domains. Then, we will draw connections with verification, and reactive synthesis, together with their game-theoretic solution techniques. The main catch is that working with these logics can be based on devising suitable 2-player games and finding strategies, i.e., plans, to win them. Specifically, we will cover the following topics: Planning in Nondeterministic Domains, Temporal Logics, LTL, LTLf, PPLTL, Game-theoretic Techniques, and Reactive Synthesis. This course is partially based on the work carried out in ERC Advanced Grant WhiteMech and EU ICT-48 TAILOR.
Schedule.
Thursday 02/05/2024: 15:00-19:00 CEST – Via Ariosto 25, A5 + online
Monday 06/05/2024: 17:00-19:00 CEST – Via Ariosto 25, A2 + online
Thursday 09/05/2024: 15:00-19:00 CEST – Via Ariosto 25, A5 + online
Monday 13/05/2024: 17:00-19:00 CEST – Via Ariosto 25, A2 + online
Thursday 16/05/2024: 15:00-18:00 CEST – Via Ariosto 25, A5 + online
Monday 20/05/2024: 17:00-19:00 CEST – Via Ariosto 25, A2 + online
Thursday 23/05/2024: 13:00-19:00 CEST – Via Ariosto 25, A5 + online
Monday 27/05/2024: 17:00-19:00 CEST – Via Ariosto 25, A2 + online
Thursday 30/05/2024: 13:00-19:00 CEST – Via Ariosto 25, A5 + online
Teaching material.
[1] Course slides 2023/2024 and additional readings which will be available on this page.