The third edition of the Summer School on Formal Methods for Cyber-Physical
Systems offers an in-depth exploration of reactive synthesis, a topic that was
already introduced in the first edition of the school. The lecturers will
provide a systematic account of the main achievements and the current trends of
research in reactive synthesis, covering both theory and applications.
The course will begin with an overview of the classical synthesis problem in
the finite-state setting, as originally formulated by Church and solved by
Buechi and Landweber. This introductory part will introduce the terminology of
infinite two-player games, explain the automatic construction of winning
strategies in “regular games”, and address history of the subject, discussing
extensions and open problems. From there, the course will investigate
approaches for making reactive synthesis more efficient and practical,
including techniques for solving the synthesis problem in restricted settings,
for decomposing the problem into subproblems, and for employing algorithms,
data structures, and heuristics to manage complexity. Variants of the synthesis
problem will also be explored, such as control strategies for hybrid and
distributed systems, monitor synthesis, synthesis under incomplete information,
distributed synthesis, and symmetric synthesis. The implementation of synthesis
tools will also receive significant attention, with a focus on recent advances
and applications of UPPAAL Stratego and the SYNTCOMP reactive synthesis
competition.
The summer school will conclude with a workshop on emerging research trends in
synthesis, monitoring, and learning, which showcases some exciting interactions
between formal methods and machine learning. Distinguished invited speakers
will lead the workshop. Participants will also have the opportunity to engage
with peers from around the world and may propose to deliver short research
talks voluntarily.
