Workshop on Synthesis, Monitoring and Learning - Invited talk

3-hour lectures 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.

3-hour lectures 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.

Workshop on Synthesis, Monitoring and Learning - Invited talk

Workshop on Synthesis, Monitoring and Learning - Invited talk

Planned presentation has been cancelled due to unforeseen circumstances
3-hour lectures 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.

3-hour lectures 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. 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).

Workshop on Synthesis, Monitoring and Learning - Invited talk

3-hour lectures 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.

3-hour lectures 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.