Sciweavers

Share
LICS
2008
IEEE

Winning Regions of Higher-Order Pushdown Games

11 years 7 months ago
Winning Regions of Higher-Order Pushdown Games
In this paper we consider parity games defined by higher-order pushdown automata. These automata generalise pushdown automata by the use of higher-order stacks, which are nested “stack of stacks” structures. Representing higher-order stacks as well-bracketed words in the usual way, we show that the winning regions of these games are regular sets of words. Moreover a finite automaton recognising this region can be effectively computed. y of our work are abstract pushdown processes which can be seen as (ordinary) pushdown automata but with an infinite stack alphabet. We use the device to give a uniform presentation of our results. From our main result on winning regions of parity games we derive a solution to the Modal Mu-Calculus Global Model-Checking Problem for higher-order pushdown graphs as well as for ranked trees generated by higher-order safe recursion schemes.
Arnaud Carayol, Matthew Hague, Antoine Meyer, C.-H
Added 31 May 2010
Updated 31 May 2010
Type Conference
Year 2008
Where LICS
Authors Arnaud Carayol, Matthew Hague, Antoine Meyer, C.-H. Luke Ong, Olivier Serre
Comments (0)
books