Easy to Win, Hard to Master: Optimal Strategies in Finitary Parity Games

5^th September 2017, 16:00 ELEC-201 (in EEE)
Dr. Martin Zimmermann
Reactive Systems Group
Universität des Saarlandes
Saarland Informatics Campus, Building E 1.1, room 1.13

Abstract

Parity games are at the heart of a wide range of problems in verification, logics, synthesis, and automata theory. Furthermore, they have an intriguing complexity-theoretic status, being "almost in PTIME". Finally, both players have memoryless, i.e., very simple, winning strategies. However, the parity condition is a qualitative one and therefore not able to express quantitative specifications.

Here, we consider finitary parity games, a quantitative strengthening of parity games introduced by Chatterjee and Henzinger, by reformulating the parity condition as a boundedness property where the bound is existentially quantified. Finitary parity games retain most of the attractive properties of parity games, e.g., one player always has memoryless winning strategies and the winner can even be determined in polynomial time.

We show that the characteristics of finitary parity games are vastly different when asking for optimal strategies: the solution problem becomes PSPACE-complete and exponential memory is both necessary in general and always sufficient. Thus, playing finitary parity games optimally is harder than just winning them. Moreover, we show that the tradeoff between the memory size and the realised bound is gradual in general.

(Based on joint work with Alexander Weinert, published at CSL 2016.)