Solving Infinite Games with Bounds
Martin Zimmermann
We investigate the existence and the complexity of computing and implementing optimal winning strategies for graph games of infinite duration.
Parameterized linear temporal logics are extensions of Linear Temporal Logic (LTL) by temporal operators equipped with variables for time bounds. In model-checking, such specifications were introduced as PLTL by Alur et al. and as PROMPT-LTL by Kupferman et al. We show how to determine in doubly-exponential time, whether a player wins a game with PLTL winning condition with respect to some, infinitely many, or all variable valuations. Hence, these problems are not harder than solving LTL games. Furthermore, we present an algorithm with triply-exponential running time to determine optimal variable valuations that allow a player to win a game. Finally, we give doubly-exponential upper and lower bounds on the values of optimal variable valuations.
In Muller games, we measure the quality of a winning strategy using McNaughton’s scoring functions. We construct winning strategies that bound the losing player’s scores by two and show this to be optimal. This improves the previous best upper bound of n! in a game with n vertices, obtained by McNaughton. Using these strategies, we show how to transform a Muller game into a safety game whose solution allows to determine the winning regions of the Muller game and to compute a finite-state winning strategy for one player. This yields a novel antichain-based memory structure and the first definition of permissive strategies for Muller games. Moreover, we generalize our construction by presenting a new type of game reduction from infinite games to safety games and show its applicability to several other winning conditions.
PhD Thesis.