Seminar: Games in Verification and Synthesis

Instructors: Bernd Finkbeiner, Rayna Dimitrova, Klaus Dräger, Hans-Jörg Peter and Sven Schewe
Lecture Room: SR 014 Building E 1 3
Lecture Time: Thursdays 16:15 – 17:45

Topic Assignment and Seminar Schedule

Games provide a powerful framework for reasoning about the interaction between the components of reactive systems, such as communication protocols and control systems. In this seminar, we will study game-theoretic methods that derive implementations from formal specifications (synthesis) and that prove that a given implementation satisfies a logical property (verification). In both cases, we view the interaction between a software component and its environment as an infinite game; verification then amounts to checking that the strategy represented by the program is winning; synthesis amounts to deriving a winning strategy from a logical description of the winning condition.

Date Speaker Topic Slides Handout
May 15 Piotr Danilewski Algorithms for solving parity games pdf pdf
May 29 Walid Haddad Model checking games pdf pdf
June 12 Andreas Augustin Synthesis under incomplete information pdf pdf
June 12 Michael Maurer Simulation Games ppt pdf
June 19 Maël Hörz Module checking pdf pdf
June 19 Fabienne Eigner Alternating-time temporal logics pdf pdf
June 26 Jonathan Türpe Distributed synthesis pdf pdf
June 26 Steffen Metzger Bounded synthesis pdf pdf
July 3 Patrick Jungblut Timed games pdf pdf
July 3 Christine Rizkallah Synthesis of Asynchronous Systems pdf pdf
July 10 Stefan Stattelmann Timed interfaces pdf pdf
July 17 Daniel Dahrendorf Counterexample-guided control pdf pdf
July 17 Georg Neis Three-valued abstractions of games pdf pdf

Related Course: AG&V

The AG&V lecture (Automata, Games, and Verification) covers background and additional topics related to the seminar. We recommend (but do not require) attending AG&V in parallel.

Preliminary list of topics

Seminar (7 CP)

Sommersemester 2008