The aim of this course is to introduce the mathematical theory and algorithmic results about graph-games, to convey how graph-games form the foundation of formal-methods, and how they are used in AI.
Games on graphs are a useful mathematical model of many phenomena in computer science that involve interaction between players/agents/components. Solving a game means deciding if a given player has a winning strategy. There are a number of classes of games whose complexity are in the intersection of NP and co-NP, but are not known to be in P, i.e., parity games, mean-payoff games, discounted payoff games, simple stochastic games. This year, there was a breakthrough in the analysis of parity games, a deceptively simply class of games with tight connections to deep results in logic and automata theory. A team from New Zealand and Singapore [Calude et. al. 2017] gave a quasi-polynomial time algorithm for solving parity games --- previous algorithms were mildly subexponential.
I will chart a course through the theory of games on graphs, covering determinacy, memory required for winning, and the complexity of solving games. I will start with foundational work and end with very recent results.
- Ehrenfeucht and Mycielski (1979). Positional strategies for mean payoff games
- McNaughton (1993). Infinite games played on finite graphs.
- Zwick and Paterson (1995). The complexity of mean payoff games.
- Dziembowski, Jurdzinski, and Walukiewicz (1997). How much memory is needed to win infinite games?
- Zielonka (1998). Infinite games on finitely coloured graphs with applications to automata on infinite trees.
- Voge and Jurdzinski (2000). A discrete strategy improvement algorithm for solving parity games.
- Chatterjee, Henzinger, and Jurdzinski (2005). Mean-payoff parity games.
- Schewe (2007). Solving Parity Games in Big Steps.
- Jurdzinski, Paterson, and Zwick (2008). A deterministic subexponential algorithm for solving parity games.
- Friedmann (2009). An exponential lower bound for the parity game strategy improvement algorithm as we know it.
- Benerecetti, Dell'Erba and Mogavero (2016). Solving parity games via priority promotion
- Aminof and Rubin (2016). First Cycle Games.
- Calude, Jain, Khoussainov, Li, and Stephan (2017). Deciding parity games in quasipolynomial time.
- Jurdzinski and Lazic (2017). Succinct progress measures for solving parity games.
ECTS breakdown:
25h lectures
25h reading and discussing the papers covered by the lecturer
25h preparing and giving a presentation
Schedule: 8 x 2-hour lectures
The course is given in blocked form during 20.11.-1.12. The student presentations will be scheduled in the subsequent week (4.12.-8.12).
For credit, participants can give a talk on a classic or current paper. There are a variety of topics to choose from: the tight connection between graph-games and logic and automata-theory, the use of graph-games in formal-methods (modeling, verification, synthesis, testing, composition, simulation), the use of graph-games in AI (automated planning, verification in robotics, general-game playing), or extensions of the basic model (multiplayer games, partial-information games, stochastic games, pushdown games, timed games).
