Go to: Lecturers – Programme – Venue – Admission and accommodation – Cancellation policy – Organization
Third edition of the UniVr/UniUd Summer School on Formal Methods for Cyber-Physical Systems
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 formal verification, 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.
The 3-hours lectures of Swen Jacobs have been canceled due to the sudden unavailability of the speaker. They will be replaced by invited talks by Kim Larsen, Martin Zimmermann and Dana Fisman. See below for details.
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 – 15:15 | Kim Larsen on “Monitoring Timed Properties” |
| 15:15 – 16:00 | Martin Zimmermann on “Logics for Hyperproperties” (part 1) |
| 16:00 – 16:30 | Coffee break |
| 16:30 – 17:15 | Martin Zimmermann on “Logics for Hyperproperties” (part 2) |
| 17:15 – 18:00 | Dana Fisman on “A normalized edit distance on finite and infinite words” |
| 20:00 – 23:00 | Social dinner (Pizzeria Concordia, Piazza I Maggio) |
| 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 | |
| 9:30 – 14:00 | Workshop on Synthesis, Monitoring and Learning |
Venue
The school will take place in Palazzo del Torso, the CISM headquarter, in Piazza Garibaldi, 18, 33100 Udine.
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*
This fee includes a complimentary bag, five fixed menu buffet lunches, coffee breaks, social dinner, downloadable lecture notes.
Deadline for on-site application is July 28, 2023. - Online participation, 120.00 Euro + VAT*
This fee includes downloadable lecture notes.
Deadline for online application is August 18, 2023.
Participation application is available at https://www.cism.it/en/activities/courses/J2303/
A message of confirmation will be sent to accepted participants.
Upon request a limited number of on-site participants can be accommodated at CISM Guest House at the price of 35 Euro per person/night (mail to: foresteria@cism.it).
* where applicable (bank charges are not included) Italian VAT is 22%.
Cancellation policy
Applicants may cancel their registration and receive a full refund by notifying CISM Secretariat in writing (by email) no later than:
- July 28, 2023 for on-site participants (no refund after the deadline);
- August 18, 2023 for online participants (no refund after the deadline).
Cancellation requests received before these deadlines will be charged a 50.00 Euro handling fee.
Incorrect payments are subject to Euro 50,00 handling fee.
For further information please contact:
Palazzo del Torso
CISM
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