Reactive Synthesis Swen Jacobs, Martin Zimmermann

Reactive Synthesis

Advanced Lecture (6 CP), Winter Term 2017/18

Wednesdays 14:15-16:00, in HS 003, E1.3

Student Profile

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.

Syllabus

Many of todays 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.

Topics

• 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, incremental algorithms, SAT solving
• Implementation: BDD packages, SAT solvers, existing tools, Reactive Synthesis Competition

Grading

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.

Teaching Material

For background on infinite games, see the lecture notes from the course Infinite Games. Here, we will cover a subset of the topics of the first three chapters.