Monday
14:30 -> 16:00 & 16:30 -> 18:00
Wolfgang Thomas
3-hour course on “Synthesis of strategies in infinite two-player games”
Abstract:
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.
Tuesday
9:30 -> 11:00 & 11:30 -> 13:00
Swen Jacobs
3-hour course on “Reactive Synthesis: Towards Practice”
Abstract:
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.
14:30 -> 16:00 & 16:40 -> 18:00
Kim G. Larssen
3 hours course on “Synthesis and Optimization for Cyber Physical Systems”
Abstract:
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 maneuveurs, heating systems and traffic control).
Wednesday
9:30 -> 11:00 & 11:30 -> 13:00
Bernd Finkbeiner
3-hour course on “Synthesis of distributed systems”
Abstract:
The distributed synthesis problem asks to automatically generate a distributed finite-state system from a given specification in some suitable logic. In this lecture, we will study this challenging problem, encounter undecidability proofs for the general question as well as decidable special cases and a sufficient and necessary criterion for decidability.
14:30 -> 16:00 & 16:40 -> 18:00
Martin Zimmermann
3-hour course on “Synthesis from Hyperproperties”
Abstract:
Hyperproperties are system properties like partial observation, robustness, and information-flow security, that cannot be characterized as properties of individual computation traces, but rather relate multiple such traces. In this lecture, we will study hyperproperties expressed in the temporal logic HyperLTL and develop algorithms for the synthesis and repair of reactive systems from hyperproperties. We will discuss how many classic problems of reactive synthesis, such as synthesis under incomplete information, distributed synthesis, and symmetric synthesis, can be stated as hyperproperties, and how hyperproperties allow us to apply reactive synthesis in new domains, such as security-critical systems.
Thursday
9:30 -> 11:00 & 11:30 -> 13:00
Alessandro Cimatti
3-hour course on “Runtime verification and monitor synthesis”
Abstract:
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.