Reactive Synthesis

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

People: Swen Jacobs, Martin Zimmermann
Contact: reactivesynthesis@react.uni-saarland.de
Lecture Room: E1 3, HS 003
Lectures: Wednesdays, 14:15-16:00
Tutorials: Tuesdays, 14:00-16:00 or 16:00-18:00, E1 3, Room 015
Exams: End of Term: TBA
End of Semester: TBA
Exam room: TBA

News

  • Wed, Aug 23rd: The first lecture is on Wednesday, October 18th, 2017. The tutorial slot will be determined during the first lecture.

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

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.