Description
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.