The aim of this course consists of providing the foundations of synthesis problems and how they are strongly connected to the winning strategies for games on graphs.
At the end of this course the student will be able to:
a) formalize and analyze real-world synthesis problems;
b) find the right techniques and tools for solving a synthesis problem;
c) know the basic results underlying graph games together with an idea of the main research directions in the field.
The course is divide into four main topics:
(i) first we will define the synthesis problem in its general form and we will establish a connection
to games on graph with single-objective;
(ii) in the second part we will analyze the algorithms, and the related complexity, for solving single-objective games on graphs;
(iii) then we will to analyze recent results, both positive and negative w.r.t. to decidability, on multi-objective games on graphs;
(iv) finally we consider how to solve stochastic games on graphs.
Program
1 The synthesis problem
2 Graph games with single objective
3 Graph games with multiple objectives
4 Stochastic games
References
[1] W. Zielonka : Infinite games on finitely coloured graphs with applications to automata on infinite tree,
TCS, 200(1-2):135-183, 1998
[2] E. Gradel, W. Thomas, T. Wilke (Eds.) : Automata, Logics, and Infinite Games, Springer LNCS 2500
(2003), ISBN 3-540-00388-6
[3] Krishnendu Chatterjee, Mickael Randour, and Jean-Francois Raskin, Strategy synthesis for multidimensional quantitative objectives, Acta Inf. 51 (2014), no. 3-4, 129{163.
[4] Marta Kwiatkowska, David Parker and Clemens Wiltsche. PRISM-games: Verification and Strategy
Synthesis for Stochastic Multi-player Games with Multiple Objectives. International Journal on Software
Tools for Technology Transfer, 20(2), pages 195-210, Springer. April 2018.
2
| Author | Title | Publisher | Year | ISBN | Note |
| E. Gradel, W. Thomas, T. Wilke (Eds.) | Automata, Logics, and Infinite Games (Edizione 1) | Springer | 2003 | 3-540-00388-6 |
The exam consists of giving a talk on a topic related
to the course. The topic of the talk must be
agreed upon with the teacher.
