NewsCurrently, no news are available
Advanced Lecture (6 CP), Winter Term 2019/20
Block course in semester break
This course is aimed at students that are interested in reactive synthesis in its full breadth, ranging from its theoretical formalization as an infinite game to efficient algorithms and data structures to solve the synthesis problem, and in the implementation of state-of-the-art algorithms for practically relevant and challenging problems.
Many of today's problems in computer science are no longer concerned with programs that transform data and then terminate, but with non-terminating systems that are in constant interaction with their (possibly antagonistic) environment. Over the course of the last fifty years it turned out to be very fruitful to model and analyze such reactive systems in a game-theoretic framework, which captures the antagonistic and strategic nature of the interaction between the system and its environment. Despite the prohibitive complexity of these problems in general, in recent years it has been shown that many benchmark problems can be solved automatically by efficient implementations of game-solving algorithms.
In this lecture, we will introduce different types of two-player games of infinite duration, and algorithms to solve them. To obtain efficient implementations, we will also cover automated reasoning methods that can be used as subprocedures in a synthesis algorithm, as well as data structures that can efficiently represent important aspects of infinite games.
During the course, students will implement a synthesis tool using their knowledge acquired during the lecture. At the end of the course, the resulting tools will be compared against each other and state-of-the-art tools on a set of benchmarks from the official Reactive Synthesis Competition.
- Theoretical Basics: reachability and safety games, Büchi and co-Büchi games, parity games
- Efficient Algorithms and Data Structures: fixpoint algorithms, strategy extraction, BDD representation and operations
- Implementation: BDD packages, existing tools, Reactive Synthesis Competition
The final grade will be composed of the project grade and the grade from an exam. For admission to the exam, students most solve a certain percentage of exercises during the course.