News
08.11.2017

Problem Set 3Problem Set 3 is now online. The deadline is on the 14th of November before the tutorial. 
08.11.2017

APPLY AlgorithmIt was pointed out to me that the APPLY algorithm, as presented in the lecture, did not properly reflect the fact that the current root nodes of the two BDDs could be labeled with different variables. In that case, the recursion only considers the successor nodes in... Read more It was pointed out to me that the APPLY algorithm, as presented in the lecture, did not properly reflect the fact that the current root nodes of the two BDDs could be labeled with different variables. In that case, the recursion only considers the successor nodes in the BDD that is rooted in the maximal variable (and reuses the current root node for the other BDD). I have already fixed this in the slides, thanks for pointing it out! 
25.10.2017

ExamsThe exam dates have been fixed. The first one takes place on January, 31st instead of the last lecture. The lecture has been moved to January, 30th. No exam relevant material will be presented during this last lecture. The reexam is scheduled for March, 20th, 14:15. 
23.10.2017

First TutorialAs determined in the first lecture, the tutorials will be on Tuesdays at 14:15. We will meet for the first time tomorrow in Seminar Room 15, E1.3. See you there! 
18.10.2017

Problem Set 1, Exercise 1.1(a)Try your best, but also be bold when you think it is impossible to solve! In any case, argue your claims. 
04.09.2017

Registration OpenIf 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 LectureThe 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:1516: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 stateoftheart 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 nonterminating 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 gametheoretic 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 gamesolving algorithms.
In this lecture, we will introduce different types of twoplayer 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 stateoftheart tools on a set of benchmarks from the official Reactive Synthesis Competition.
Topics
 Theoretical Basics: reachability and safety games, Büchi and coBü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.