Collapsible Pushdown Parity Games

Christopher H. Broadbent; Arnaud Carayol; Matthew Hague; Andrzej S. Murawski; C. H.Luke Ong; Olivier Serre

doi:10.1145/3457214

Collapsible Pushdown Parity Games

Christopher H. Broadbent
, Arnaud Carayol
, Matthew Hague
, Andrzej S. Murawski
, C. H.Luke Ong
, Olivier Serre

Research output: Contribution to journal › Article › peer-review

Abstract

This article studies a large class of two-player perfect-information turn-based parity games on infinite graphs, namely, those generated by collapsible pushdown automata. The main motivation for studying these games comes from the connections from collapsible pushdown automata and higher-order recursion schemes, both models being equi-expressive for generating infinite trees. Our main result is to establish the decidability of such games and to provide an effective representation of the winning region as well as of a winning strategy. Thus, the results obtained here provide all necessary tools for an in-depth study of logical properties of trees generated by collapsible pushdown automata/recursion schemes.

Original language	English
Article number	3457214
Journal	ACM Transactions on Computational Logic
Volume	22
Issue number	3
DOIs	https://doi.org/10.1145/3457214
Publication status	Published - 1 Jun 2021
Externally published	Yes

Keywords

Higher-order (collapsible) pushdown automata
logic
two-player perfect-information trun-based parity games

Access to Document

10.1145/3457214

Cite this

@article{83ec32e1ea944de48adc476f77bcf3d7,

title = "Collapsible Pushdown Parity Games",

abstract = "This article studies a large class of two-player perfect-information turn-based parity games on infinite graphs, namely, those generated by collapsible pushdown automata. The main motivation for studying these games comes from the connections from collapsible pushdown automata and higher-order recursion schemes, both models being equi-expressive for generating infinite trees. Our main result is to establish the decidability of such games and to provide an effective representation of the winning region as well as of a winning strategy. Thus, the results obtained here provide all necessary tools for an in-depth study of logical properties of trees generated by collapsible pushdown automata/recursion schemes.",

keywords = "Higher-order (collapsible) pushdown automata, logic, two-player perfect-information trun-based parity games",

author = "Broadbent, \{Christopher H.\} and Arnaud Carayol and Matthew Hague and Murawski, \{Andrzej S.\} and Ong, \{C. H.Luke\} and Olivier Serre",

note = "Publisher Copyright: {\textcopyright} 2021 Association for Computing Machinery.",

year = "2021",

month = jun,

day = "1",

doi = "10.1145/3457214",

language = "English",

volume = "22",

journal = "ACM Transactions on Computational Logic",

issn = "1529-3785",

number = "3",

}

TY - JOUR

T1 - Collapsible Pushdown Parity Games

AU - Broadbent, Christopher H.

AU - Carayol, Arnaud

AU - Hague, Matthew

AU - Murawski, Andrzej S.

AU - Ong, C. H.Luke

AU - Serre, Olivier

PY - 2021/6/1

Y1 - 2021/6/1

N2 - This article studies a large class of two-player perfect-information turn-based parity games on infinite graphs, namely, those generated by collapsible pushdown automata. The main motivation for studying these games comes from the connections from collapsible pushdown automata and higher-order recursion schemes, both models being equi-expressive for generating infinite trees. Our main result is to establish the decidability of such games and to provide an effective representation of the winning region as well as of a winning strategy. Thus, the results obtained here provide all necessary tools for an in-depth study of logical properties of trees generated by collapsible pushdown automata/recursion schemes.

AB - This article studies a large class of two-player perfect-information turn-based parity games on infinite graphs, namely, those generated by collapsible pushdown automata. The main motivation for studying these games comes from the connections from collapsible pushdown automata and higher-order recursion schemes, both models being equi-expressive for generating infinite trees. Our main result is to establish the decidability of such games and to provide an effective representation of the winning region as well as of a winning strategy. Thus, the results obtained here provide all necessary tools for an in-depth study of logical properties of trees generated by collapsible pushdown automata/recursion schemes.

KW - Higher-order (collapsible) pushdown automata

KW - logic

KW - two-player perfect-information trun-based parity games

U2 - 10.1145/3457214

DO - 10.1145/3457214

M3 - Article

AN - SCOPUS:85108943230

SN - 1529-3785

VL - 22

JO - ACM Transactions on Computational Logic

JF - ACM Transactions on Computational Logic

IS - 3

M1 - 3457214

ER -

Collapsible Pushdown Parity Games

Abstract

Keywords

Access to Document

Fingerprint

Cite this