Infinite two player games
Alexis Julien-Bouquet
LaBRI, University of Bordeaux I, France.
28-01-04

---

Abstract

Infinite two player games are one of the central notions in verification and theory of automata on finite/infinite words and trees. Such a game is defined by a bipartite graph whose nodes are the positions for player 0 and 1. The winning condition (for player 0) is a set of infinite paths in the graph.

In general, the winning condition is a regular condition which can be defined by a parity condition. For this condition, an important result is that both players have memoryless winning strategies which depend only on the current position. Currently, solving finite state parity games is in UP intersection coUP, but it is not known if there exists a PTIME algorithm. (It is a famous open problem! A positive answer provides us a PTIME algorithm for famous model checking and synthesis of controllers problems. A negative solution will be a proof that P is not NP.)

We will focus on interesting subcases relative to a permissiveness notion defined by Bernet, Janin and Walukiewicz. The most permissive strategies are such that the player can stay in his winning region.

Next we look at infinite state games. The standard model is when the infinite game graph is defined by the configurations of a pushdown automaton. In this case, we can study winning conditions other than regular ones, such as the Unboundedness condition where player 0 wins if he can make the height of the stack higher and higher. We will show how to solve such a game by using finite parity game simulation.