Solving Infinite Games with Bounds

Speaker(s)

Martin Zimmermann

Affiliation

Uniwersytet Warszawski

Date

Feb. 15, 2012, 2:15 p.m.

Room

room 5870

Seminar

Seminar Automata Theory

---

In this talk I will present results reported in my PhD thesis.

Parameterized linear temporal logic (PLTL) is an extension of Linear Temporal Logic (LTL) by temporal operators equipped with variables for time bounds. One can in 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, in triply-exponential running time an optimal variable valuation that allows a player to win a game can be determined.

Then, we introduce McNaughton's scoring functions for Muller games. 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 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.

---