Summer School on Reactive Synthesis + Workshop on Synthesis, Monitoring and Learning at University of Udine

*** 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

http://tcs.uniud.it/smile

-----------------------------------------------------------------------------


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