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