Abstract
Game theory has been forged in the 1944 book of von Neumann (a mathematician) and Morgenstern (an economist) as a way to reason rigorously about economic behaviour, but its methodologies have since also illuminated many areas of social, political, and natural sciences. More recently, it has also enjoyed fruitful cross-fertilization with Computer Science, yielding the vibrant areas of Algorithmic Game Theory and Algorithmic Mechanism Design. Less broadly known, but relevant to the Theoretical Foundations of Computer Systems program at Simons, are the game theoretic models that originate from set theory, logic, and automata.
In this tutorial, we consider a very basic model of games on graphs. We then argue that this simple model is general enough to encompass a range of classic game-theoretic models, and that it can streamline or enable solutions of notable problems, for example:
- Gale-Stewart games in set theory and Martin’s Borel determinacy theorem;
- Church’s reactive synthesis problem and its solution by Buchi and Landweber;
- Rabin’s tree theorem and its proof using positional determinacy;
- Pnueli and Rosner’s temporal synthesis problem;
- evaluating nested Knaster-Tarski fixpoints;
- the complexity of pivoting rules in linear optimization and stochastic planning;
- star height problem.
The technical focus of this tutorial is on the algorithmic aspects of one relatively simple but influential graph game model called parity games. Building efficient parity game solvers is worthwhile because many model-checking, equivalence-checking, satisfiability, and synthesis problems boil down to solving a parity game. The problem has an intriguing computational complexity status: it is both in NP and in co-NP, and in PLS and PPAD, and hence unlikely to be complete for any of those complexity classes; no compelling evidence of hardness is known; and it is a long-standing open problem if it can be solved in polynomial time.
A key parameter that measures the descriptive complexity of a parity game graph is the number of distinct priorities; for example, in games arising from nested Knaster-Tarski fixpoint expressions, it reflects the number of alternations between least and greatest fixpoints. All known algorithms for several decades have been exponential in the number of priorities, until 2017 when Calude, Jain, Khoussainov, Li, and Stephan made a breakthrough by showing that the problem is FPT and that there is a quasi-polynomial algorithm.
In 2018, Lehtinen has proposed another parameter called the register number and has shown that parity games can be solved in time exponential in it. This refines the quasi-polynomial complexity obtained by Calude et al. because the register number of a finite game is at most logarithmic in its size. We argue that the register number coincides with another parameter called the Strahler number, which provides structural insights and allows to solve parity games efficiently using small Strahler-universal trees. We mention preliminary experimental evidence to support Lehtinen’s thesis that most parity games in the wild have very tiny register/Strahler numbers. This strengthens a popular belief that finding a polynomial-time algorithm is more vital in theory than in practice and it suggests practical ways of turning modern quasi-polynomial algorithms into competitive solvers.