Game-Theoretic Approach to Synthesis

16-20 June 2025

Instructor: Giuseppe Perelli, Antonio Di Stasio (Guest lecturer)
Course duration: 10 hours.
Course Type: Lecture/seminar series.
Location: Room G0, building G, viale Regina Elena 295 and Room S1, building E, viale Regina Elena 295
Schedule: From Monday 16th June to Friday 20th June from 10:00 to 12:00
Language: English/Italian (TBD)

Registration

All the students interested in attending the course are invited to register at the following link:

And join the classroom at:

https://classroom.google.com/c/MjMyOTA5MTcyNDZa?cjc=o2n2slqo

Abstract

This course introduces AI reactive synthesis for tasks (goals) expressed over finite traces instead of states. Drawing upon the methodologies of Formal Methods, we will consider tasks and environment specifications expressed in LTL and its finite trace variant LTLf. We will review the main results and algorithmic techniques for solving reactive synthesis. Then, we will draw connections 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. We will cover the following topics: Games on Graphs, Temporal Logics, LTL, LTLf , Game-theoretic techniques for LTLf objectives, and Reactive Synthesis. This course is a re-edition of the one taught at ESSAI-24 with fellow colleagues Antonio Di Stasio and Shufang Zhu. It is partially based on the work carried out in ERC Advanced Grant ERC Advanced Grant WhiteMech and EU ICT-48 TAILOR, and the PNRR MUR project PE0000013-FAIR.

Synopsis (Tentative)

Games on Graphs: Introduction to games on graphs. Classification of games based on: Turn types, observability, objectives. Solutions to games with Reachability, Safety, and more advanced objectives.

Linear Temporal Logic: Logic based language for the representation of programs. LTLf : linear-time temporal logic over finite traces.

Game-theoretic approach for LTLf objectives: Introduction to 2-player (turn-based) games on graphs and their relationship with Synthesis. Solutions to simple objective games: Reachability and Safety games, Safe-Reach, Buchi Games. Parity games: a more sophisticated game objective. Solution to parity games and their relationship with LTL synthesis.

Synthesis under environment specifications: The environment represented as an LTL specification. The synthesis under environment specifications solved as synthesis of an implication formula. Direct and more effective solutions to the synthesis under environment specifications for notable cases of LTLf formulas: Safety, Safety & Fairness, Safety & Stability, Safety & GR(1). Symbolic representation and techniques for Planning and Synthesis.