Infinite regular games in the higher-order pushdown and the parametrized setting
Michaela Slaats, Wolfgang H Thomas · RWTH Publications (RWTH Aachen) · 2011
Higher-order pushdown systems extend the idea of pushdown systems by using a "higher-order stack" (which is a nested stack). More precisely on level 1 this is a standard stack, on level 2 it is a stack of stacks, and so on. We study the higher-order pushdown systems in the context of infinite regular games. In the first part, we present a k-ExpTime algorithm to compute global positional winning strategies for parity games which are played on the configuration graph of a level-k higher-order pushdown system. To represent those winning strategies in a finite way we use a notion of regularity for sets of higher-order stacks that relies on certain ("symmetric") operations to build higher-order stacks. The construction of the strategies is based on automata theoretic techniques and uses the fact that the higher-order stacks constructed by symmetric operations can be arranged uniquely in a tree structure. In the second part, we study the solution of games in the sense of Gale and Stewart where the winning condition is specified by an MSO-formula phi(P) with a parameter P subset of N. This corresponds to a three player game where the i-th round between the two original players is extended by the choice of the bit 1 or 0 depending on whether i is in P or not. We consider the case that the parameter can be constructed by some deterministic machine, a "parameter generator". We solve the parametrized regular games for parameters P given by two kinds of such generators, namely: higher-order pushdown automata and collapsible pushdown automata. In the third part, we study higher-order pushdown systems and higher-order counter systems (where the stack alphabet contains only one symbol), by comparing the language classes accepted by corresponding automata. For example, we show that level-k pushdown languages are level-(k+1) counter languages.