Material

Lecture Slides are available here (Note that parts 4 and 5 have not yet been updated to this years lecture)

Content

In the module students are introduced to the theory of games played on a (finite) graph (also: recursive games with finite state space). 
By means of different variants of reachability games (with/without chance, turn-based/concurrent moves) the students learn the basic definitions and algorithms in the field of mathematical game theory.
Building up on the reachability games more involved quantitative (e.g. Markov decision processes, discouted-payoff games, mean-payoff games, Shapely's stochastic games) and qualitative (e.g. Parity, Rabin, Muller, Streett) variants are discussed.
Further topics include e.g. techniques for reducing memory consumption (e.g. BDDs), tool presentations (e.g. PRISM), games with partial observations, games on pushdown graphs, relations to logics and set theory (e.g. Gale-Stewart games and Martin's determinacy result), or the synthesis of controllers.

Literature

• Filar, Vrieze: Competitive Markov Decision Processes, Springer, 1996
• Grädel, Thomas, Wilke: Automata, Logics, and Infinite Games, Springer 2002
• Perrin, Pin: Infinite Words – Automata, Semigroups, Logics and Games, Elsevier 2004