joint work with Martin Zimmermann

The starting point of this work is the following observation: although similar in flavor, parity games and finitary parity games are very different from an algorithmic perspective. Both are two-player games on graphs whose vertices are labeled by integers. The parity winning condition states that almost all odd labels are followed by a greater even label. Parity games have received a lot of attention since they are the model-checking games of the modal mu-calculus and determining the winner in a parity game is one of the few problems in NP and co-NP, but not known to be in PTIME. The finitary parity condition is obtained by additionally requiring a bound on the number of edges traversed between odd labels and the next greater even label. Quite surprisingly, deciding the winner in a finitary parity game can be carried out in polynomial time.

This work generalizes both parity games and finitary parity games by introducing cost-parity games. In these games traversing an edge comes with a cost and the condition requires a bound on the cost between odd labels and the next greater even label. We show that cost-parity games enjoy two nice properties of parity and finitary parity games: the first player has memoryless winning strategies, and determining the winner lies in NP and co-NP (as for parity games). Furthermore, we show that solving cost-parity games can be algorithmically reduced to solving parity games, which allows to solve cost-parity games almost as efficiently as parity games.