{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:19:17Z","timestamp":1750220357198,"version":"3.41.0"},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2021,6,28]],"date-time":"2021-06-28T00:00:00Z","timestamp":1624838400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2021,7,30]]},"abstract":"<jats:p>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.<\/jats:p>","DOI":"10.1145\/3457214","type":"journal-article","created":{"date-parts":[[2021,6,28]],"date-time":"2021-06-28T13:07:55Z","timestamp":1624885675000},"page":"1-51","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Collapsible Pushdown Parity Games"],"prefix":"10.1145","volume":"22","author":[{"given":"Christopher H.","family":"Broadbent","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Oxford, UK"}]},{"given":"Arnaud","family":"Carayol","sequence":"additional","affiliation":[{"name":"CNRS, LIGM (Universit\u00e9 Paris Est &amp; CNRS), France"}]},{"given":"Matthew","family":"Hague","sequence":"additional","affiliation":[{"name":"Royal Holloway, University of London, UK"}]},{"given":"Andrzej S.","family":"Murawski","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Oxford, UK"}]},{"given":"C.-H. Luke","family":"Ong","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Oxford, UK"}]},{"given":"Olivier","family":"Serre","sequence":"additional","affiliation":[{"name":"Universit\u00e9 de Paris, IRIF, CNRS, France"}]}],"member":"320","published-online":{"date-parts":[[2021,6,28]]},"reference":[{"doi-asserted-by":"publisher","key":"e_1_2_1_1_1","DOI":"10.1007\/978-3-540-31982-5_31"},{"unstructured":"Andr\u00e9 Arnold and Damian Niwi\u0144ski. 2001. Rudiments of mu-Calculus(Studies in Logic and the Foundations of Mathematics Vol. 146). Elsevier.  Andr\u00e9 Arnold and Damian Niwi\u0144ski. 2001. Rudiments of mu-Calculus(Studies in Logic and the Foundations of Mathematics Vol. 146). Elsevier.","key":"e_1_2_1_2_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_3_1","DOI":"10.1007\/978-3-540-30538-5_12"},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of the 29th Symposium on Theoretical Aspects of Computer Science (STACS\u201912)","volume":"14","author":"Broadbent Christopher H.","year":"2012","unstructured":"Christopher H. Broadbent . 2012 . The limits of decidability for first order logic on CPDA graphs . In Proceedings of the 29th Symposium on Theoretical Aspects of Computer Science (STACS\u201912) (LIPIcs), Vol. 14 . Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 589\u2013600. Christopher H. Broadbent. 2012. The limits of decidability for first order logic on CPDA graphs. In Proceedings of the 29th Symposium on Theoretical Aspects of Computer Science (STACS\u201912) (LIPIcs), Vol. 14. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 589\u2013600."},{"doi-asserted-by":"publisher","key":"e_1_2_1_5_1","DOI":"10.1007\/978-3-642-31585-5_18"},{"doi-asserted-by":"publisher","key":"e_1_2_1_6_1","DOI":"10.1145\/2544174.2500589"},{"doi-asserted-by":"crossref","unstructured":"Christopher H. Broadbent Arnaud Carayol Matthew Hague and Olivier Serre. 2020. Higher-Order Recursion Schemes and Collapsible Pushdown Automata: Logical Properties. Retrieved from https:\/\/www.irif.fr\/ serre\/\/PublisMisc\/BCOS20.pdf .  Christopher H. Broadbent Arnaud Carayol Matthew Hague and Olivier Serre. 2020. Higher-Order Recursion Schemes and Collapsible Pushdown Automata: Logical Properties. Retrieved from https:\/\/www.irif.fr\/ serre\/\/PublisMisc\/BCOS20.pdf .","key":"e_1_2_1_7_1","DOI":"10.1145\/3452917"},{"doi-asserted-by":"publisher","key":"e_1_2_1_8_1","DOI":"10.1109\/LICS.2010.40"},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the 4th International Workshop on Verification of Infinite-State Systems, Infinity 2002 (Electronic Notes in Theoretical Computer Science)","volume":"68","author":"Cachat Thierry","year":"2002","unstructured":"Thierry Cachat . 2002 . Uniform solution of parity games on prefix-recognizable graphs . In Proceedings of the 4th International Workshop on Verification of Infinite-State Systems, Infinity 2002 (Electronic Notes in Theoretical Computer Science) , Vol. 68 . Elsevier Science Publishers. Thierry Cachat. 2002. Uniform solution of parity games on prefix-recognizable graphs. In Proceedings of the 4th International Workshop on Verification of Infinite-State Systems, Infinity 2002 (Electronic Notes in Theoretical Computer Science), Vol. 68. Elsevier Science Publishers."},{"doi-asserted-by":"publisher","key":"e_1_2_1_11_1","DOI":"10.5555\/1759210.1759266"},{"key":"e_1_2_1_12_1","volume-title":"The complexity of games on higher order pushdown automata. CoRR abs\/0705.0262","author":"Cachat Thierry","year":"2007","unstructured":"Thierry Cachat and Igor Walukiewicz . 2007. The complexity of games on higher order pushdown automata. CoRR abs\/0705.0262 ( 2007 ). Thierry Cachat and Igor Walukiewicz. 2007. The complexity of games on higher order pushdown automata. CoRR abs\/0705.0262 (2007)."},{"doi-asserted-by":"publisher","key":"e_1_2_1_13_1","DOI":"10.1007\/11549345_16"},{"doi-asserted-by":"publisher","key":"e_1_2_1_14_1","DOI":"10.1109\/LICS.2008.41"},{"doi-asserted-by":"publisher","key":"e_1_2_1_15_1","DOI":"10.1109\/LICS.2012.73"},{"doi-asserted-by":"publisher","key":"e_1_2_1_16_1","DOI":"10.1007\/978-3-540-85238-4_17"},{"doi-asserted-by":"publisher","key":"e_1_2_1_17_1","DOI":"10.5555\/645731.668334"},{"doi-asserted-by":"publisher","key":"e_1_2_1_18_1","DOI":"10.1016\/0304-3975(94)90268-2"},{"doi-asserted-by":"publisher","key":"e_1_2_1_19_1","DOI":"10.1109\/SFCS.1991.185392"},{"doi-asserted-by":"publisher","key":"e_1_2_1_20_1","DOI":"10.1016\/0890-5401(91)90015-T"},{"doi-asserted-by":"publisher","key":"e_1_2_1_21_1","DOI":"10.1145\/800070.802177"},{"doi-asserted-by":"publisher","key":"e_1_2_1_23_1","DOI":"10.1109\/LICS.2008.34"},{"doi-asserted-by":"publisher","key":"e_1_2_1_24_1","DOI":"10.1145\/3091122"},{"key":"e_1_2_1_25_1","volume-title":"Symbolic backwards-reachability analysis for higher-order pushdown systems. Log. Meth. Comput. Sci. 4, 4","author":"Hague Matthew","year":"2008","unstructured":"Matthew Hague and C.-H. Luke Ong . 2008. Symbolic backwards-reachability analysis for higher-order pushdown systems. Log. Meth. Comput. Sci. 4, 4 ( 2008 ). Matthew Hague and C.-H. Luke Ong. 2008. Symbolic backwards-reachability analysis for higher-order pushdown systems. Log. Meth. Comput. Sci. 4, 4 (2008)."},{"doi-asserted-by":"publisher","key":"e_1_2_1_26_1","DOI":"10.1016\/j.ic.2010.12.004"},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of the 27th Symposium on Theoretical Aspects of Computer Science (STACS\u201910)","volume":"5","author":"Kartzow Alexander","year":"2010","unstructured":"Alexander Kartzow . 2010 . Collapsible pushdown graphs of level 2 are tree-automatic . In Proceedings of the 27th Symposium on Theoretical Aspects of Computer Science (STACS\u201910) (LIPIcs), Vol. 5 . Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 501\u2013512. Alexander Kartzow. 2010. Collapsible pushdown graphs of level 2 are tree-automatic. In Proceedings of the 27th Symposium on Theoretical Aspects of Computer Science (STACS\u201910) (LIPIcs), Vol. 5. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 501\u2013512."},{"doi-asserted-by":"publisher","key":"e_1_2_1_28_1","DOI":"10.1007\/11523468_117"},{"doi-asserted-by":"publisher","key":"e_1_2_1_29_1","DOI":"10.2307\/1971035"},{"doi-asserted-by":"publisher","key":"e_1_2_1_30_1","DOI":"10.1016\/0304-3975(85)90087-8"},{"key":"e_1_2_1_31_1","first-page":"1","article-title":"Decidability of second-order theories and automata on infinite trees","volume":"141","author":"Rabin Michael O.","year":"1969","unstructured":"Michael O. Rabin . 1969 . Decidability of second-order theories and automata on infinite trees . Trans. Amer. Math. Soc. 141 (1969), 1 \u2013 35 . Michael O. Rabin. 1969. Decidability of second-order theories and automata on infinite trees. Trans. Amer. Math. Soc. 141 (1969), 1\u201335.","journal-title":"Trans. Amer. Math. Soc."},{"doi-asserted-by":"publisher","key":"e_1_2_1_32_1","DOI":"10.1016\/S0020-0190(02)00445-3"},{"doi-asserted-by":"publisher","key":"e_1_2_1_34_1","DOI":"10.1007\/978-3-642-00596-1_8"},{"doi-asserted-by":"publisher","key":"e_1_2_1_35_1","DOI":"10.5555\/267871.267878"},{"doi-asserted-by":"publisher","key":"e_1_2_1_36_1","DOI":"10.5555\/646252.685998"},{"doi-asserted-by":"publisher","key":"e_1_2_1_37_1","DOI":"10.5555\/647765.735846"},{"doi-asserted-by":"publisher","key":"e_1_2_1_38_1","DOI":"10.1006\/inco.2000.2894"},{"doi-asserted-by":"publisher","key":"e_1_2_1_39_1","DOI":"10.5555\/1018438.1021872"},{"doi-asserted-by":"publisher","key":"e_1_2_1_40_1","DOI":"10.36045\/bbms\/1102714178"},{"key":"e_1_2_1_41_1","volume-title":"Model checking synchronized products of infinite transition systems. Log. Meth. Comput. Sci. 3, 4","author":"W\u00f6hrle Stefan","year":"2007","unstructured":"Stefan W\u00f6hrle and Wolfgang Thomas . 2007. Model checking synchronized products of infinite transition systems. Log. Meth. Comput. Sci. 3, 4 ( 2007 ). Stefan W\u00f6hrle and Wolfgang Thomas. 2007. Model checking synchronized products of infinite transition systems. Log. Meth. Comput. Sci. 3, 4 (2007)."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3457214","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3457214","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:17:19Z","timestamp":1750191439000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3457214"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,6,28]]},"references-count":38,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2021,7,30]]}},"alternative-id":["10.1145\/3457214"],"URL":"https:\/\/doi.org\/10.1145\/3457214","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2021,6,28]]},"assertion":[{"value":"2020-10-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-03-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-06-28","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}