*** apologies for cross-postings ***
===== Call for Attendance =====
----------------------------------------------------------------------------- Third edition of the UniVr/UniUd Summer School on Formal Methods for Cyber-Physical Systems - Udine, August 28-31
http://tcs.uniud.it/summer-school
+
Workshop on Synthesis, Monitoring and Learning - Udine, August 31-September 1
-----------------------------------------------------------------------------
Synthesis is a fundamental problem in computer science and mathematics, concerned with automatically generating programs that satisfy a given logical specification. Its applications span a range of domains, including model-based system design, software engineering, and automated theorem proving. For instance, designing a controller that guides the behavior of a reactive system, that is, a system that continually interacts with its environment, can be framed as a synthesis problem. Similarly, the design and verification of a distributed system often depend on distributed synthesis, which finds programs that enforce correct component interaction and satisfy desired specifications.
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.
### Lecturers
Wolfgang Thomas - RWTH Aachen University, Germany
3-hour lecture on “Synthesis of strategies in infinite two-player games”
We give an introduction to the synthesis of reactive systems in the finite-state setting, using the terminology of infinite two-player games and explaining the automatic construction of winning strategies in “regular games”. We also address the history of the subject, discuss extensions, and mention basic problems that are still open.
Martin Zimmermann - Aalborg University, Denmark
3-hour lecture on “Synthesis of infinite-state systems”
The reactive synthesis problem asks to compute, from a given specification of the input-output behavior of a reactive system, a system satisfying this specification (or to determine that no such system exists). In this lecture, we consider the synthesis of infinite-state systems with a focus on pushdown systems, which model simple recursive systems with finite data. On a technical level, we show how to solve infinite games on configuration graphs of pushdown automata and present recent work on generalizations to history-deterministic pushdown automata.
Kim G. Larsen - Aalborg University, Denmark
3-hour lecture on “Synthesis and Optimization for Cyber Physical Systems”
In these lectures we will present recent advances and applications of the tool UPPAAL Stratego (www.uppaal.org) supporting automatic synthesis of guaranteed safe and near-optimal control strategies for Cyber Physical Systems (CPS). UPPAAL Stratego combines symbolic methods from model checking, reinforcement learning methods from machine learning, as well as abstraction techniques for hybrid games. Trade-offs between efficiency of strategy representation and degree of optimality subject to safety constraints will be discussed, as well as successful applications (autonomous driving maneuvers, heating systems and traffic control).
Dana Fisman - Ben Gurion University of the Negev, Israel
3-hour lecture on “Automata learning of languages of finite and infinite words”
In these lectures we will get acquainted with the research area called grammatical inference or automata learning. We will start with the earliest results on the subject, and span different learning paradigms. We will describe several positive results, and efficient algorithms for learning regular languages. We will prove several negative results for learning different classes of languages in different learning paradigms. We will then discuss state-of-the-art results on learning regular languages of infinite words.
Swen Jacobs - CISPA Helmholtz-Center for Information Security, Germany
3-hour lecture on “Reactive synthesis: towards practice”
I will give an overview of different lines of research that try to make reactive synthesis (more) practical. This includes research into approaches to restrict the problem to more efficiently solvable fragments, into ways to split the problem into subproblems that can be solved independently or iteratively, and into efficient algorithms and data structures as well as heuristics that allow us to implement synthesis tools that can solve problems of significant size. I will report on progress observed in the reactive synthesis competition (SYNTCOMP), and on case studies and benchmark problems that demonstrate the capabilities of state-of-the-art synthesis tools.
Alessandro Cimatti - Fondazione Bruno Kessler, Italy
3-hour lecture on “Runtime verification and monitor synthesis”
Runtime Verification (RV) is a lightweight verification technique that aims at checking whether a run of a system under scrutiny (SUS) satisfies or violates a given correctness specification. The lecture will first overview the general framework of RV, and the techniques to synthesize run-time monitors that can be efficiently executed in combination with the SUS. Then, we will cover the relationship between RV and the field of Fault Detection and Isolation (FDI). In FDI, runtime monitors are built taking into account models of the SUS, in order to monitor the occurrence of internal (faulty) conditions that are not directly observable.
### Programme
Monday, August 28
13:30 - 14:00 Registration 14:00 - 14:30 Course Introduction 14:30 - 16:00 Wolfgang Thomas 16:00 - 16:30 Coffee break 16:30 - 18:00 Wolfgang Thomas
Tuesday, August 29
09:30 - 11:00 Martin Zimmermann 11:00 - 11:30 Coffee break 11:30 - 13:00 Martin Zimmermann 13:00 - 14:00 Lunch 14:30 - 16:00 Kim G. Larsen 16:00 - 16:30 Coffee break 16:30 - 18:00 Kim G. Larsen
Wednesday, August 30
09:30 - 11:00 Dana Fisman 11:00 - 11:30 Coffee break 11:30 - 13:00 Dana Fisman 13:00 - 14:00 Lunch 14:30 - 16:00 Swen Jacobs 16:00 - 16:30 Coffee break 16:30 - 18:00 Swen Jacobs 19:00 - 23:00 Social dinner
Thursday, August 31
09:30 - 11:00 Alessandro Cimatti 11:00 - 11:30 Coffee break 11:30 - 13:00 Alessandro Cimatti 13:00 - 14:00 Lunch 14:30 - 16:30 Workshop on Synthesis, Monitoring and Learning
Friday, September 1
09:30 - 14:00 Workshop on Synthesis, Monitoring and Learning
### Admission and accommodation
The course is offered in a hybrid format giving the possibility to remotely attend the course (on the Microsoft Teams platform).
On-site places are limited and assigned on first come first served basis.
The registration fees are: - On-site participation, 250.00 Euro + VAT 22% - Online participation, 120.00 Euro + VAT 22%
Deadline for online application is August 18, 2023. Participation application is available at https://www.cism.it/en/activities/courses/J2303/
### Contacts
CISM, Palazzo del Torso Piazza Garibaldi 18, 39100 Udine, Italy tel. +39 0432 248511 email: cism@cism.it | www.cism.it
### Organization Angelo Montanari - University of Udine, Italy Gabriele Puppis - University of Udine, Italy Tiziano Villa - University of Verona, Italy