Parametrized Regular Infinite Games and Higher-Order Pushdown Strategies
Paul Hänsch, Michaela Slaats, Wolfgang Thomas
Given a set $P$ of natural numbers, we consider infinite games where
the winning condition is a regular $\omega$-language parametrized
by $P$. In this context, an $\omega$-word, representing a play, has
letters consisting of three components: The first is a bit indicating
membership of the current position in $P$, and the other two components
are the letters contributed by the two players. Extending recent work of
Rabinovich we study here predicates $P$ where the structure $(\mathbb{N},
+1, P)$ belongs to the pushdown hierarchy (or ``Caucal hierarchy''). For
such a predicate $P$ where $(\mathbb{N}, +1, P)$ occurs in the $k$-th
level of the hierarchy, we provide an effective determinacy result and
show that winning strategies can be implemented by deterministic level-$k$
pushdown automata.