{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T14:30:47Z","timestamp":1762353047521,"version":"3.41.0"},"reference-count":44,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T00:00:00Z","timestamp":1619740800000},"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,4,30]]},"abstract":"<jats:p>\n            This article studies the logical properties of a very general class of infinite ranked trees, namely, those generated by higher-order recursion schemes. We consider, for both monadic second-order logic and modal\n            <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>\n                  \n                <\/jats:tex-math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\n            -calculus, three main problems: model-checking, logical reflection (a.k.a. global model-checking, that asks for a finite description of the set of elements for which a formula holds), and selection (that asks, if exists, for some finite description of a set of elements for which an MSO formula with a second-order free variable holds). For each of these problems, we provide an effective solution. This is obtained, thanks to a known connection between higher-order recursion schemes and collapsible pushdown automata and on previous work regarding parity games played on transition graphs of collapsible pushdown automata.\n          <\/jats:p>","DOI":"10.1145\/3452917","type":"journal-article","created":{"date-parts":[[2021,5,15]],"date-time":"2021-05-15T19:27:02Z","timestamp":1621106822000},"page":"1-37","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Higher-order Recursion Schemes and Collapsible Pushdown Automata: Logical Properties"],"prefix":"10.1145","volume":"22","author":[{"given":"Christopher H.","family":"Broadbent","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Oxford, Oxford, UK"}]},{"given":"Arnaud","family":"Carayol","sequence":"additional","affiliation":[{"name":"LIGM, Univ Gustave Eiffel, CNRS, France"}]},{"given":"C.-H. Luke","family":"Ong","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Oxford, Oxford, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5936-240X","authenticated-orcid":false,"given":"Olivier","family":"Serre","sequence":"additional","affiliation":[{"name":"Universit\u00e9 de Paris, IRIF, CNRS, France"}]}],"member":"320","published-online":{"date-parts":[[2021,5,15]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/11874683_7"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31982-5_31"},{"key":"e_1_2_1_3_1","first-page":"439","article-title":"Translations on a context-free grammar","volume":"19","author":"Aho Alfred V.","year":"1971","unstructured":"Alfred V. Aho and Jeffrey D. Ullman . 1971 . Translations on a context-free grammar . Inf. Comput. 19 , 5 (1971), 439 \u2013 475 . Alfred V. Aho and Jeffrey D. Ullman. 1971. Translations on a context-free grammar. Inf. Comput. 19, 5 (1971), 439\u2013475.","journal-title":"Inf. Comput."},{"volume-title":"Rudiments of mu-Calculus. (Studies in Logic and the Foundations of Mathematics)","author":"Arnold Andr\u00e9","key":"e_1_2_1_4_1","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_5_1","unstructured":"Christopher H. Broadbent Arnaud Carayol Matthew Hague Andrzej S. Murawski C.-H. Luke Ong and Olivier Serre. 2020. Collapsible Pushdown Games. Retrieved from https:\/\/www.irif.fr\/ serre\/\/PublisMisc\/BCHMOS20.pdf.  Christopher H. Broadbent Arnaud Carayol Matthew Hague Andrzej S. Murawski C.-H. Luke Ong and Olivier Serre. 2020. Collapsible Pushdown Games. Retrieved from https:\/\/www.irif.fr\/ serre\/\/PublisMisc\/BCHMOS20.pdf."},{"key":"e_1_2_1_6_1","volume-title":"Proceedings of the 25th IEEE Symposium on Logic in Computer Science (LiCS\u201910)","author":"Broadbent Christopher H.","year":"2010","unstructured":"Christopher H. Broadbent , Arnaud Carayol , C.-H. Luke Ong , and Olivier Serre . 2010 . Recursion schemes and logical reflexion . In Proceedings of the 25th IEEE Symposium on Logic in Computer Science (LiCS\u201910) . IEEE Computer Society, 120\u2013129. Christopher H. Broadbent, Arnaud Carayol, C.-H. Luke Ong, and Olivier Serre. 2010. Recursion schemes and logical reflexion. In Proceedings of the 25th IEEE Symposium on Logic in Computer Science (LiCS\u201910). IEEE Computer Society, 120\u2013129."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00596-1_9"},{"key":"e_1_2_1_9_1","unstructured":"Arnaud Carayol. 2019. Habilitation. In Automata Logics and Games for Infinite Trees. Universit\u00e9 Paris Est.  Arnaud Carayol. 2019. Habilitation. In Automata Logics and Games for Infinite Trees. Universit\u00e9 Paris Est."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74915-8_15"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.41"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.73"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85238-4_17"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24597-1_10"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45687-2_13"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1936-1501858-0"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90268-2"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00049-3"},{"key":"e_1_2_1_19_1","first-page":"1","article-title":"An automata-theoretical characterization of the oi-hierarchy","volume":"71","author":"Damm Werner","year":"1986","unstructured":"Werner Damm and Andreas Goerdt . 1986 . An automata-theoretical characterization of the oi-hierarchy . Inf. Comput. 71 (1986), 1 \u2013 32 . Werner Damm and Andreas Goerdt. 1986. An automata-theoretical characterization of the oi-hierarchy. Inf. Comput. 71 (1986), 1\u201332.","journal-title":"Inf. Comput."},{"volume-title":"Mathematical Logic (2 ed.)","author":"Ebbinghaus Heinz-Dieter","key":"e_1_2_1_20_1","unstructured":"Heinz-Dieter Ebbinghaus , J\u00f6rg Flum , and Wolfgang Thomas . 1996. Mathematical Logic (2 ed.) . Springer-Verlag . Heinz-Dieter Ebbinghaus, J\u00f6rg Flum, and Wolfgang Thomas. 1996. Mathematical Logic (2 ed.). Springer-Verlag."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/310955.310961"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48057-1_20"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/800070.802177"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273673"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.77.4"},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of the 33rd International Conference on Foundations of Software Technology and Theoretical Computer Science (FST&TCS\u201913)","volume":"24","author":"Haddad Axel","year":"2013","unstructured":"Axel Haddad . 2013 . Model checking and functional program transformations . In Proceedings of the 33rd International Conference on Foundations of Software Technology and Theoretical Computer Science (FST&TCS\u201913) (LIPIcs), Vol. 24 . Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 115\u2013126. Axel Haddad. 2013. Model checking and functional program transformations. In Proceedings of the 33rd International Conference on Foundations of Software Technology and Theoretical Computer Science (FST&TCS\u201913) (LIPIcs), Vol. 24. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 115\u2013126."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.34"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3091122"},{"key":"e_1_2_1_31_1","first-page":"285","article-title":"On full abstraction for PCF: I. Models, observables and the full abstraction problem, II. Dialogue games and innocent strategies, III. A fully abstract and universal game model","volume":"163","author":"Martin J.","year":"2000","unstructured":"J. Martin , E. Hyland , and C.-H. Luke Ong . 2000 . On full abstraction for PCF: I. Models, observables and the full abstraction problem, II. Dialogue games and innocent strategies, III. A fully abstract and universal game model . Inf. Comput. 163 (2000), 285 \u2013 408 . J. Martin, E. Hyland, and C.-H. Luke Ong. 2000. On full abstraction for PCF: I. Models, observables and the full abstraction problem, II. Dialogue games and innocent strategies, III. A fully abstract and universal game model. Inf. Comput. 163 (2000), 285\u2013408.","journal-title":"Inf. Comput."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61604-7_60"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45413-6_21"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45931-6_15"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/11523468_117"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480933"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2009.29"},{"key":"e_1_2_1_38_1","volume-title":"Proceedings of the 21st IEEE Symposium on Logic in Computer Science (LiCS\u201906)","author":"Luke Ong C.-H.","year":"2006","unstructured":"C.-H. Luke Ong . 2006 . On model-checking trees generated by higher-order recursion schemes . In Proceedings of the 21st IEEE Symposium on Logic in Computer Science (LiCS\u201906) . IEEE Computer Society, 81\u201390. C.-H. Luke Ong. 2006. On model-checking trees generated by higher-order recursion schemes. In Proceedings of the 21st IEEE Symposium on Logic in Computer Science (LiCS\u201906). IEEE Computer Society, 81\u201390."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.62"},{"key":"e_1_2_1_40_1","volume-title":"Proceedings of the 35th Symposium on Theoretical Aspects of Computer Science (STACS\u201918)","volume":"96","author":"Parys Pawel","year":"2018","unstructured":"Pawel Parys . 2018 . Recursion schemes and the WMSO+U logic . In Proceedings of the 35th Symposium on Theoretical Aspects of Computer Science (STACS\u201918) (LIPIcs), Vol. 96 . Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 53:1\u201353:16. Pawel Parys. 2018. Recursion schemes and the WMSO+U logic. In Proceedings of the 35th Symposium on Theoretical Aspects of Computer Science (STACS\u201918) (LIPIcs), Vol. 96. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 53:1\u201353:16."},{"key":"e_1_2_1_41_1","volume-title":"Proceedings of the 16th International Conference on Computer-aided Verification (CAV\u201904)","volume":"3114","author":"Piterman Nir","unstructured":"Nir Piterman and Moshe Y. Vardi . 2004. Global model-checking of infinite-state systems . In Proceedings of the 16th International Conference on Computer-aided Verification (CAV\u201904) (Lecture Notes in Computer Science) , Vol. 3114 . Springer-Verlag, 387\u2013400. Nir Piterman and Moshe Y. Vardi. 2004. Global model-checking of infinite-state systems. In Proceedings of the 16th International Conference on Computer-aided Verification (CAV\u201904) (Lecture Notes in Computer Science), Vol. 3114. Springer-Verlag, 387\u2013400."},{"key":"e_1_2_1_42_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."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38946-7_15"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(89)90031-X"},{"volume-title":"Handbook of Formal Language Theory","author":"Thomas Wolfgang","key":"e_1_2_1_45_1","unstructured":"Wolfgang Thomas . 1997. Languages , automata, and logic . In Handbook of Formal Language Theory , G. Rozenberg and A. Salomaa (Eds.). Vol. III . Springer-Verlag , 389\u2013455. Wolfgang Thomas. 1997. Languages, automata, and logic. In Handbook of Formal Language Theory, G. Rozenberg and A. Salomaa (Eds.). Vol. III. Springer-Verlag, 389\u2013455."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.5555\/1018438.1021872"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.36045\/bbms\/1102714178"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3452917","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3452917","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:47:06Z","timestamp":1750193226000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3452917"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,4,30]]},"references-count":44,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2021,4,30]]}},"alternative-id":["10.1145\/3452917"],"URL":"https:\/\/doi.org\/10.1145\/3452917","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2021,4,30]]},"assertion":[{"value":"2020-10-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-02-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-05-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}