Note on winning positions on pushdown games with omega-regular conditions
We consider infinite two-player games on pushdown graphs. For parity winning conditions, we show that the set of winning positions of each player is regular and we give an effective construction of an alternating automaton recognizing it. This provides a DEXPTIME procedure to decide whether 6 position is winning for a given player. Finally, using the same methods, we show, for any omega-regular winning condition, that the set of winning positions for a given player is regular and effective. (C) 2002 Elsevier Science B.V. All rights reserved.
games automata infinite graphs pushdown processes