Playing Pushdown Parity Games in a Hurry

TL;DR

This paper extends finite-duration game results to pushdown parity games, showing they can be solved via finite reachability games, thus enabling efficient winner determination.

Contribution

It establishes an equivalence between pushdown parity games and finite-duration variants, facilitating finite-tree reachability analysis for infinite-state games.

Findings

Pushdown parity games are equivalent to finite-duration variants.

Winner determination reduces to reachability in finite trees.

Results enable more efficient analysis of infinite-state games.

Abstract

We continue the investigation of finite-duration variants of infinite-duration games by extending known results for games played on finite graphs to those played on infinite ones. In particular, we establish an equivalence between pushdown parity games and a finite-duration variant. This allows us to determine the winner of a pushdown parity game by solving a reachability game on a finite tree.