loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
2008 23rd Annual IEEE Symposium on Logic in Computer Science
Winning Regions of Higher-Order Pushdown Games
June 24-June 27
ISBN: 978-0-7695-3183-0
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.A novelty 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.
Index Terms:
higher-order pushdown automata, higher-order recursion schemes, mu-calculus model-checking, parity games
Citation:
Arnaud Carayol, Matthew Hague, Antoine Meyer, C.-H. Luke Ong, Olivier Serre, "Winning Regions of Higher-Order Pushdown Games," lics, pp.193-204, 2008 23rd Annual IEEE Symposium on Logic in Computer Science, 2008
Usage of this product signifies your acceptance of the Terms of Use.