Institute of

Theoretical Computer Science


Technische Universität Braunschweig

Lecture: Games with Perfect Information

Summer term 2018


July 26
We offer appointments for oral exams on the follwing dates:
  • Tuesday, July 17,
  • Monday, July 23,
  • Tuesday, September 11.
To book an appointment, please write a mail to Sebastian containing your full name and your student id ("Matrikelnummer").
July 11
An updated version of the lecture notes, containing all the material relevant for the exam, is now available. Please contact me if you spot any mistakes!
June 21
The lecture notes and the exercise sheet for the lecture that will be given on June 27 are available now.
June 20
There will be no exercise classes on June 27. Exercise sheet 10 (which you have submitted on June 20) will be discussed on July 4.
June 6
Exercise sheet 9 is available now! The lecture notes will be updated tomorrow, sorry for the delay. The lecture notes have been updated.
May 9
Due to organizational reasons, the lecture notes and exercise sheet for the lecture next week (on May 16) are already available. Exercise sheet 6 is the one corresponding to today's lecture.
May 4
The lecture notes have finally caught up to the lecture. Yay!
April 27
There was a bug in the winning condition in Exercise 2 of Exercise sheet 4. Please find an updated version below.
April 26
Exercise sheet 4 is available now. The lecture notes will be updated in a few days. (If you need the notes on online scheduling, you may consult last year's notes.) Sorry for the delay!
April 4
The lecture notes and the first exercise sheet are available. Please submit in groups of three persons.
March 20
The first lecture will take place on April 4. The first exercise session will take place on April 11.
Februrary 17
All information on this page is still tentative.


Lecture Notes

The lecture notes will be updated during the term.

Lecture notes (last updated on August 6).

If you have questions or spot a bug in the notes, please contact Sebastian.


The exercise sheets are made available here. Please hand in your solutions during the lecture (in the week after the sheet has been released). Please submit in groups of three people. If you have questions or encounter problems with the exercises, please contact Sebastian.


Successfully finishing the module consists of two parts:


When we consider non-deterministic systems (like NFAs), we usually either consider the non-determinism as controllable (Reachability problem: "Can we resolve the non-determinism such that we reach state q?"), or as uncontrollable (Safety problem: "Does the system avoid state q, no matter how non-determinism is resolved?"). It is a natural extensions to consider two types of non-determinism at once: a controllable ("angelic") non-determinism, and an uncontrollable ("demonic") one. This setting gives rise to a two-player game, in which each player represents one type of non-determinism. We are now able to ask questions like "Can one player enforce that state q is reached, no matter what the other player does?"
In this lecture, we will focus on games with perfect information, in which both players know the "rules" of the game (the possible states of the game and the moves), as well as the current state of the game whenever it is their turn. Many board games that you know from real life are of this type (e.g. Chess), while others use hidden/imperfect information (e.g. Battleships), randomness (e.g. Mensch ärgere dich nicht), or both (e.g. Poker).
Games with perfect information have numerous applications in automata theory, verification and synthesis that will be presented throughout the lecture (while games with imperfect information are usually studied e.g. in economy).

We will first consider games on finite graphs, where we have a finite set of configurations ("states"), transitions ("moves"), an ownership assignment of the configurations ("Who has the turn?") and a winning condition. We first consider simple winning conditions like reachability ("Reach a configuration in set W in finitely many moves") and safety ("Avoid visiting all configuration in set W for all time"). This is already sufficient to model the board games that you know from real life, but for the applications in verification, more complicated winning conditions are also of interest. Instead of considering all infinite plays as won (safety) or lost (reachability), the winning condition can consider infinite plays as won or lost depending on some property (e.g. "A play is winning if it has visited region W infinitely often.") In this part, the theory naturally gives rise to algorithms that compute the winner of a game.

If we find the time to do so, we will also consider games on infinite graph. We need to assume that the configuration space has some underlying structure. For example, we can study games played in the configuration graphs of pushdown automata. In this case, there are algorithms that use the finite representation to compute properties of the infinite game.



The lectures will be based upon the following books and articles. Most of them are available online, the remaining ones can be found in the library.