Banach-Mazur Games on Graphs

Erich Grädel
RTWH Aachen
Friday, 14 December, 2012 - 14:00
NO Solvay (fifth floor)

Infnite games where two players take turns to move a token through a directed graph, thus tracing out an infinite path, have numerous applications in different branches of mathematics and computer science. In the classical format of such games, the possible moves of the players are given by the edges of the graph; in each move a player takes the token from its current position along an edge to a next position. In Banach-Mazur games the players instead select in each move a path of arbitrary finite length rather than just an edge. In both cases the outcome of a play is an infinite path and the objectives of the players are given by properties of infinite paths.

Banach-Mazur games have a long tradition in descriptive set theory and topology, and have recently been shown to have also interesting applications in computer science, such as for planning in nondeterministic domains, the study of fairness in concurrent systems and for timed automata.

We discuss several notions of ”simple” winning strategies for Banach-Mazur games on graphs, such as positional strategies, move-counting or length-counting strategies, and strategies with a memory based on finite appearance records (FAR). Banach-Mazur games often admit stronger determinacy results than classical graph games and more efficient algorithmic solutions. For instance, all Banach-Mazur games with omega-regular winning conditions are positionally determined. Beyond the omega-regular winning conditions, we focus here on Muller conditions with infinitely many colours. We investigate the infinitary Muller conditions that guarantee positional determinacy for Banach-Mazur games. Further, we determine classes of such conditions that require infinite memory but guarantee determinacy via move-counting strategies, length-counting strategies, and FAR-strategies. We also discuss the relationships between these different notions of determinacy.