Winning regions of higher-order pushdown games

A. Carayol, M. Hague, A. Meyer, C. H.L. Ong, O. Serre

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

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.

Original languageEnglish
Title of host publicationProceedings - 23rd Annual IEEE Symposium on Logic in Computer Science, LICS 2008
Pages193-204
Number of pages12
DOIs
Publication statusPublished - 17 Sept 2008
Externally publishedYes
Event23rd Annual IEEE Symposium on Logic in Computer Science, LICS 2008 - Pittsburgh, PA, United States
Duration: 24 Jun 200827 Jun 2008

Publication series

NameProceedings - Symposium on Logic in Computer Science
ISSN (Print)1043-6871

Conference

Conference23rd Annual IEEE Symposium on Logic in Computer Science, LICS 2008
Country/TerritoryUnited States
CityPittsburgh, PA
Period24/06/0827/06/08

Fingerprint

Dive into the research topics of 'Winning regions of higher-order pushdown games'. Together they form a unique fingerprint.

Cite this