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 | ||
| May 29 | Walid Haddad | Model checking games | ||
| June 12 | Andreas Augustin | Synthesis under incomplete information | ||
| June 12 | Michael Maurer | Simulation Games | ppt | |
| June 19 | Maël Hörz | Module checking | ||
| June 19 | Fabienne Eigner | Alternating-time temporal logics | ||
| June 26 | Jonathan Türpe | Distributed synthesis | ||
| June 26 | Steffen Metzger | Bounded synthesis | ||
| July 3 | Patrick Jungblut | Timed games | ||
| July 3 | Christine Rizkallah | Synthesis of Asynchronous Systems | ||
| July 10 | Stefan Stattelmann | Timed interfaces | ||
| July 17 | Daniel Dahrendorf | Counterexample-guided control | ||
| July 17 | Georg Neis | Three-valued abstractions of games |
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
- algorithms for solving parity games
- strategy improvement algorithms
- abstraction-based game solving
- games with incomplete information
- distributed games
- real-time games
- controller synthesis
- model checking games
- synthesis of distributed systems
Seminar (7 CP)
Sommersemester 2008