Institute of

Theoretical Computer Science


Technische Universität Braunschweig

Lecture: Games with Perfect Information

Summer term 2017 in Braunschweig


August 3
The following document contains information on the oral exam, in particular on which topics are relevant: Relevant material.
August 3
The lecture notes have been updated to cover the material of the last lecture.
August 3
A solution for Exercise Sheet 13 is now available below.
August 3
We offer oral exams on the following dates: August 31, September 1, and September 22. To get an appointment for the exam, please write a mail to Sebastian by August 18. It should contain your full name, your Matrikelnummer, the date, and your preferred time (e.g. in the morning or afternoon). All exams will take place in Prof. Meyers office (IZ 346).
July 7
The lecture notes now include the material on the complexity of mean payoff games that we covered in the exercise class as well as the proof of the existence of an undetermined game. I have added Exercise Sheet 13, which is a bonus exercise sheet. Its points will count towards your number of achieved points, but not towards the maximal points. I encourage you to take a look at the exercises!
June 30
The notes on mean payoff games are now complete, and the corresponding exercise sheet is available. For the sake of clarity, the proofs in the notes are much more detailed than the ones presented in the lecture.
June 23
The notes on payoff games and the corresponding exercise sheet are now online.
June 21
There was a bug in Line (3) of Exercise 3a) of exercise sheet 10. I have updated the sheet.
June 20
I have updated the lecture notes to include material on S2S.
June 15
Exercise sheet 10 and the updated lecture notes are now online. We will discuss S2S (monadic second order logic over infinite trees) in the exercise class session on June 20.
June 1
Exercise sheet 9 and the updated lecture notes are now online. Note that due to the excursion week, there are no classes in the week from June 5 to 9.
May 26
Exercise sheet 8 and the updated lecture notes are now online. Sorry for the delay!
May 11
The new exercise sheet and the updated lecture notes are only - hopefully bug-free this time!
May 7
In Exercise 1, the statement has to be proven for vertices owned by refuter. (The case of prover has already been considered in the lecture.) I updated the sheet and the notes - Sorry!
May 6
I just fixed several bugs in the fifth exercise sheet. Please download the updated version below. (1) Exercise 2: Added missing arc from 9 to 6. (2) Exercise 3: Added clarification that jobs have to be processed sequentially. (3) Exercise 3: Fixed small typo in Part a): Task tau3 generates a job after 6 steps, not tau6.
May 4
The new exercise sheet and updated lecture notes are online now. Sorry for the delay!
May 3
We will change the schedule for the exercise sheets to give you more time to work on them. I will release the exercise sheet on Wednesday or Thursday, and you have time until the Friday in the week afterwards to submit it. We will then talk about it in the week afterwards.
This in particular means that there are no exercise classes on May 9, since the new sheet has to be handed in on May 12 and will be discussed in the exercise classes on May 16.
April 26
Exercise sheet 4 is now online, and the lecture notes have been updated. Due to the public holiday on Monday, May 1, the exercise sheet can be submitted in the exercise classes on Tuesday, May 2. The exercise sheet contains only 2 exercises. We will discuss the applications of reachability games for scheduling problems in the exercise class.
April 19
The third exercise sheet is online. The lecture notes have been updated, too.
April 16
I fixed a bug on the second exercise sheet (the winning condition of Exercise 3 was missing a case). Please take a look at the updated version!
April 12
Due to the public holiday on Monday, April 17, the second exercise sheet can be submitted in the exercise classes on Tuesday, April 18.
April 5
The first exercise sheet and the first part of the lecture notes are now available! You can find them below, as well as more information on when and how submit your solutions.
April 3
The first lecture will take place on Wednesday, April 5, 11:30 - 13:00 in room IZ 358.


Lecture Notes

The full lecture notes are now available.

Lecture notes (last updated on September 20)

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


Exercises will be made available here each Wednesday after the lecture. Please hand in your solution in groups of 2 to 3 people in the box next to room 343 in the Institute for Theoretical Computer Science, Muehlenpfordtstr. 23. You can also submit your solution as a PDF-file via email to Sebastian. If you have questions or encounter problems with the exercises, please contact Sebastian.


Sucessfully 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-determinsm 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 untrollable ("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).

The lecture will be split into three parts.

In the first part, we will 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 visting 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.") For this part of the lecture, the theory naturally gives rise to algorithms that compute the winner of a game.

In the second part of the lecture, we turn to games on an infinite set of configurations. While the theory from the finite case still works, we cannot immediately obtain algorithms that compute the winner of games in finite time. Thus, we need to assume that the configuration space has some underlying structure. If the underlying structure is some automaton model with undecidable verification problems (e.g. Turing machines), then for any type of game, it will not be possible to compute the winner. We will see that, surprisingly, there are structures with decidable verification problems (e.g. Petri nets), for which games are undecidable.
This brings us to taking a step back and asking: Can we just not compute the winner, or is it even the case that no winner exists? We will see that there are non-determined games in which none of the players has a winning strategy, but that most games are determined.

In the third part, we return to studying algorithms for games. This time, we consider games whose infinite set of configurations is generated by a pushdown automaton respectively context-free grammar. We consider and compare three different algorithms for such games: Cachat's algorithm saturates a finite automaton that in the end describes the winning region, Walukiewicz's reduction allows us to reduce such a game to a game on a finite graph (that then can be solved using the techniques from the first part), and the summary algorithm computes formulas from which the winner and winning strategies can be read off.



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.