Mini course: Milestones in solving games on graphs

VCLA and WPI hosted a mini course by Sasha Rubin

Aim

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.

Lecturer

Sasha Rubin, University of Naples “Federico II”.

Dates and Venues

The course is given in a block format between November 20. and December 1, 2017.

Student presentations are scheduled for the subsequent week (4.12.–8.12).

Subject

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.

I will draw material from the following core papers:
– 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.

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

Literature

• Apt, Krzysztof R. and Erich Gradel (Eds.). 2011. Lectures in Game Theory for Computer Scientists. Cambridge University Press: Cambridge.
• Grädel, Erich, Wolfgang Thomas and Thomas Wilke (Eds.). 2002. Automata, Logics, and Infinite Games: A Guide to Current Research. Springer-Verlag New York: New York.

Sasha Rubin, University of Naples “Federico II”