Reactive Synthesis Swen Jacobs, Martin Zimmermann

Registration for this course is open until Tuesday, 31.10.2017 23:59.

News

04.09.2017

Registration Open

If you plan to participate in this course, please register. It helps us in planning the course, and you will get future news and announcements by email.

31.08.2017

First Lecture

The first lecture is on Wednesday, October 18th, 2017. The tutorial slot will be determined during the first lecture.

 

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.



If you encounter technical problems, please contact the administrators