{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:57:33Z","timestamp":1776333453309,"version":"3.51.2"},"publisher-location":"New York, NY, USA","reference-count":36,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,8,2]],"date-time":"2022-08-02T00:00:00Z","timestamp":1659398400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"European Research Council","award":["759969"],"award-info":[{"award-number":["759969"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,8,2]]},"DOI":"10.1145\/3531130.3533346","type":"proceedings-article","created":{"date-parts":[[2022,8,4]],"date-time":"2022-08-04T20:23:38Z","timestamp":1659644618000},"page":"1-14","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Ramsey Quantifiers over Automatic Structures: Complexity and Applications to Verification"],"prefix":"10.1145","author":[{"given":"Pascal","family":"Bergstr\u00e4\u00dfer","sequence":"first","affiliation":[{"name":"Technische Universit\u00e4t Kaiserslautern, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Moses","family":"Ganardi","sequence":"additional","affiliation":[{"name":"Max Planck Institute for Software Systems (MPI-SWS), Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anthony","family":"W. Lin","sequence":"additional","affiliation":[{"name":"Technische Universit\u00e4t Kaiserslautern, Germany and Max Planck Institute for Software Systems (MPI-SWS), Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Georg","family":"Zetzsche","sequence":"additional","affiliation":[{"name":"Max Planck Institute for Software Systems (MPI-SWS), Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,8,4]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"14th International Conference, CAV 2002,Copenhagen, Denmark, July 27-31, 2002, Proceedings(Lecture Notes in Computer Science, Vol.\u00a02404)","author":"Abdulla Parosh\u00a0Aziz","year":"2002","unstructured":"Parosh\u00a0Aziz Abdulla , Bengt Jonsson , Pritha Mahata , and Julien d\u2019 Orso . 2002 . Regular Tree Model Checking. In Computer Aided Verification , 14th International Conference, CAV 2002,Copenhagen, Denmark, July 27-31, 2002, Proceedings(Lecture Notes in Computer Science, Vol.\u00a02404) , Ed\u00a0Brinksma and Kim\u00a0Guldstrand Larsen (Eds.). Springer, 555\u2013568. https:\/\/doi.org\/10.1007\/3-540-45657-0_47 10.1007\/3-540-45657-0_47 Parosh\u00a0Aziz Abdulla, Bengt Jonsson, Pritha Mahata, and Julien d\u2019Orso. 2002. Regular Tree Model Checking. In Computer Aided Verification, 14th International Conference, CAV 2002,Copenhagen, Denmark, July 27-31, 2002, Proceedings(Lecture Notes in Computer Science, Vol.\u00a02404), Ed\u00a0Brinksma and Kim\u00a0Guldstrand Larsen (Eds.). Springer, 555\u2013568. https:\/\/doi.org\/10.1007\/3-540-45657-0_47"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-28644-8_3"},{"key":"e_1_3_2_1_3_1","volume-title":"46th International Colloquium on Automata, Languages, and Programming, ICALP 2019","author":"Barcel\u00f3 Pablo","year":"2019","unstructured":"Pablo Barcel\u00f3 , Chih-Duo Hong , Xuan\u00a0Bach Le , Anthony\u00a0 W. Lin , and Reino Niskanen . 2019 . Monadic Decomposability of Regular Relations. In 46th International Colloquium on Automata, Languages, and Programming, ICALP 2019 , July 9-12, 2019, Patras, Greece(LIPIcs, Vol.\u00a0132), Christel Baier, Ioannis Chatzigiannakis, Paola Flocchini, and Stefano Leonardi (Eds.). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 103:1\u2013103:14. https:\/\/doi.org\/10.4230\/LIPIcs.ICALP. 2019.103 10.4230\/LIPIcs.ICALP.2019.103 Pablo Barcel\u00f3, Chih-Duo Hong, Xuan\u00a0Bach Le, Anthony\u00a0W. Lin, and Reino Niskanen. 2019. Monadic Decomposability of Regular Relations. In 46th International Colloquium on Automata, Languages, and Programming, ICALP 2019, July 9-12, 2019, Patras, Greece(LIPIcs, Vol.\u00a0132), Christel Baier, Ioannis Chatzigiannakis, Paola Flocchini, and Stefano Leonardi (Eds.). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 103:1\u2013103:14. https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2019.103"},{"key":"#cr-split#-e_1_3_2_1_4_1.1","unstructured":"Pascal Bergstr\u00e4\u00dfer Moses Ganardi Anthony\u00a0W. Lin and Georg Zetzsche. 2022. Ramsey Quantifiers over Automatic Structures: Complexity and Applications to Verification. CoRR abs\/2205.09015(2022). https:\/\/doi.org\/10.48550\/arXiv.2205.09015 arXiv:2205.09015 10.48550\/arXiv.2205.09015"},{"key":"#cr-split#-e_1_3_2_1_4_1.2","doi-asserted-by":"crossref","unstructured":"Pascal Bergstr\u00e4\u00dfer Moses Ganardi Anthony\u00a0W. Lin and Georg Zetzsche. 2022. Ramsey Quantifiers over Automatic Structures: Complexity and Applications to Verification. CoRR abs\/2205.09015(2022). https:\/\/doi.org\/10.48550\/arXiv.2205.09015 arXiv:2205.09015","DOI":"10.1145\/3531130.3533346"},{"key":"e_1_3_2_1_5_1","volume-title":"Automatic Structures. In 15th Annual IEEE Symposium on Logic in Computer Science","author":"Blumensath Achim","year":"2000","unstructured":"Achim Blumensath and Erich Gr\u00e4del . 2000 . Automatic Structures. In 15th Annual IEEE Symposium on Logic in Computer Science , Santa Barbara, California, USA , June 26-29, 2000. IEEE Computer Society, 51\u201362. https:\/\/doi.org\/10.1109\/LICS.2000.855755 10.1109\/LICS.2000.855755 Achim Blumensath and Erich Gr\u00e4del. 2000. Automatic Structures. In 15th Annual IEEE Symposium on Logic in Computer Science, Santa Barbara, California, USA, June 26-29, 2000. IEEE Computer Society, 51\u201362. https:\/\/doi.org\/10.1109\/LICS.2000.855755"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00224-004-1133-y"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1051\/ita:2006005"},{"key":"e_1_3_2_1_8_1","unstructured":"Hubert Comon Max Dauchet R\u00e9mi Gilleron Florent Jacquemard Denis Lugiez Christof L\u00f6ding Sophie Tison and Marc Tommasi. 1997. Tree Automata Techniques and Applications. (1997).  Hubert Comon Max Dauchet R\u00e9mi Gilleron Florent Jacquemard Denis Lugiez Christof L\u00f6ding Sophie Tison and Marc Tommasi. 1997. Tree Automata Techniques and Applications. (1997)."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1991.151654"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9939-1966-0201310-3"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1059513.1059520"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394734"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814288"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00153-017-0522-2"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.16"},{"key":"e_1_3_2_1_16_1","volume-title":"Automata and computability","author":"Kozen Dexter","unstructured":"Dexter Kozen . 1997. Automata and computability . Springer . Dexter Kozen. 1997. Automata and computability. Springer."},{"key":"e_1_3_2_1_17_1","volume-title":"27th International Symposium on Theoretical Aspects of Computer Science, STACS 2010","author":"Kuske Dietrich","year":"2010","unstructured":"Dietrich Kuske . 2010 . Is Ramsey\u2019s Theorem omega-automatic? . In 27th International Symposium on Theoretical Aspects of Computer Science, STACS 2010 , March 4-6, 2010, Nancy, France(LIPIcs, Vol.\u00a05), Jean-Yves Marion and Thomas Schwentick (Eds.). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 537\u2013548. https:\/\/doi.org\/10.4230\/LIPIcs.STACS. 2010.2483 10.4230\/LIPIcs.STACS.2010.2483 Dietrich Kuske. 2010. Is Ramsey\u2019s Theorem omega-automatic?. In 27th International Symposium on Theoretical Aspects of Computer Science, STACS 2010, March 4-6, 2010, Nancy, France(LIPIcs, Vol.\u00a05), Jean-Yves Marion and Thomas Schwentick (Eds.). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 537\u2013548. https:\/\/doi.org\/10.4230\/LIPIcs.STACS.2010.2483"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.2178\/jsl\/1268917499"},{"key":"e_1_3_2_1_19_1","first-page":"02","article-title":"Flat counter automata almost everywhere!","volume":"19","author":"Leroux J\u00e9r\u00f4me","year":"2006","unstructured":"J\u00e9r\u00f4me Leroux and Gr\u00e9goire Sutre . 2006 . Flat counter automata almost everywhere! . In Software Verification: Infinite-State Model Checking and Static Program Analysis , 19 . 02 . - 24.02.2006(Dagstuhl Seminar Proceedings, Vol.\u00a006081), Parosh\u00a0Aziz Abdulla, Ahmed Bouajjani, and Markus M\u00fcller-Olm (Eds.). Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany. http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2006\/729 J\u00e9r\u00f4me Leroux and Gr\u00e9goire Sutre. 2006. Flat counter automata almost everywhere!. In Software Verification: Infinite-State Model Checking and Static Program Analysis, 19.02. - 24.02.2006(Dagstuhl Seminar Proceedings, Vol.\u00a006081), Parosh\u00a0Aziz Abdulla, Ahmed Bouajjani, and Markus M\u00fcller-Olm (Eds.). Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany. http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2006\/729","journal-title":"Software Verification: Infinite-State Model Checking and Static Program Analysis"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/937555.937557"},{"key":"e_1_3_2_1_21_1","volume-title":"32nd International Colloquium, ICALP 2005, Lisbon, Portugal, July 11-15, 2005, Proceedings(Lecture Notes in Computer Science, Vol.\u00a03580)","author":"Libkin Leonid","year":"2005","unstructured":"Leonid Libkin . 2005 . Logics for Unranked Trees: An Overview. In Automata, Languages and Programming , 32nd International Colloquium, ICALP 2005, Lisbon, Portugal, July 11-15, 2005, Proceedings(Lecture Notes in Computer Science, Vol.\u00a03580) , Lu\u00eds Caires, Giuseppe\u00a0F. Italiano, Lu\u00eds Monteiro, Catuscia Palamidessi, and Moti Yung (Eds.). Springer, 35\u201350. https:\/\/doi.org\/10.1007\/11523468_4 10.1007\/11523468_4 Leonid Libkin. 2005. Logics for Unranked Trees: An Overview. In Automata, Languages and Programming, 32nd International Colloquium, ICALP 2005, Lisbon, Portugal, July 11-15, 2005, Proceedings(Lecture Notes in Computer Science, Vol.\u00a03580), Lu\u00eds Caires, Giuseppe\u00a0F. Italiano, Lu\u00eds Monteiro, Catuscia Palamidessi, and Moti Yung (Eds.). Springer, 35\u201350. https:\/\/doi.org\/10.1007\/11523468_4"},{"key":"e_1_3_2_1_22_1","volume-title":"IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2012","author":"Lin Anthony\u00a0Widjaja","year":"2012","unstructured":"Anthony\u00a0Widjaja Lin . 2012 . Accelerating tree-automatic relations . In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2012 , December 15-17, 2012, Hyderabad, India. 313\u2013324. https:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS. 2012.313 10.4230\/LIPIcs.FSTTCS.2012.313 Anthony\u00a0Widjaja Lin. 2012. Accelerating tree-automatic relations. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2012, December 15-17, 2012, Hyderabad, India. 313\u2013324. https:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS.2012.313"},{"key":"e_1_3_2_1_23_1","volume-title":"Lin and Philipp R\u00fcmmer","author":"W.","year":"2021","unstructured":"Anthony\u00a0 W. Lin and Philipp R\u00fcmmer . 2021 . Regular Model Checking Revisited. In Model Checking, Synthesis, and Learning - Essays Dedicated to Bengt Jonsson on The Occasion of His 60th Birthday . 97\u2013114. https:\/\/doi.org\/10.1007\/978-3-030-91384-7_6 10.1007\/978-3-030-91384-7_6 Anthony\u00a0W. Lin and Philipp R\u00fcmmer. 2021. Regular Model Checking Revisited. In Model Checking, Synthesis, and Learning - Essays Dedicated to Bengt Jonsson on The Occasion of His 60th Birthday. 97\u2013114. https:\/\/doi.org\/10.1007\/978-3-030-91384-7_6"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00224-004-1170-6"},{"key":"e_1_3_2_1_25_1","volume-title":"32nd International Symposium, MFCS 2007, Cesk\u00fd Krumlov, Czech Republic, August 26-31, 2007, Proceedings(Lecture Notes in Computer Science, Vol.\u00a04708)","author":"L\u00f6ding Christof","year":"2007","unstructured":"Christof L\u00f6ding and Alex Spelten . 2007 . Transition Graphs of Rewriting Systems over Unranked Trees. In Mathematical Foundations of Computer Science 2007 , 32nd International Symposium, MFCS 2007, Cesk\u00fd Krumlov, Czech Republic, August 26-31, 2007, Proceedings(Lecture Notes in Computer Science, Vol.\u00a04708) , Ludek Kucera and Anton\u00edn Kucera (Eds.). Springer, 67\u201377. https:\/\/doi.org\/10.1007\/978-3-540-74456-6_8 10.1007\/978-3-540-74456-6_8 Christof L\u00f6ding and Alex Spelten. 2007. Transition Graphs of Rewriting Systems over Unranked Trees. In Mathematical Foundations of Computer Science 2007, 32nd International Symposium, MFCS 2007, Cesk\u00fd Krumlov, Czech Republic, August 26-31, 2007, Proceedings(Lecture Notes in Computer Science, Vol.\u00a04708), Ludek Kucera and Anton\u00edn Kucera (Eds.). Springer, 67\u201377. https:\/\/doi.org\/10.1007\/978-3-540-74456-6_8"},{"key":"e_1_3_2_1_26_1","volume-title":"Decision Problems for Subclasses of Rational Relations over Finite and Infinite Words. Discret. Math. Theor. Comput. Sci. 21, 3","author":"L\u00f6ding Christof","year":"2019","unstructured":"Christof L\u00f6ding and Christopher Spinrath . 2019. Decision Problems for Subclasses of Rational Relations over Finite and Infinite Words. Discret. Math. Theor. Comput. Sci. 21, 3 ( 2019 ). http:\/\/dmtcs.episciences.org\/5141 Christof L\u00f6ding and Christopher Spinrath. 2019. Decision Problems for Subclasses of Rational Relations over Finite and Infinite Words. Discret. Math. Theor. Comput. Sci. 21, 3 (2019). http:\/\/dmtcs.episciences.org\/5141"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00214-4"},{"key":"e_1_3_2_1_28_1","volume-title":"16th International Workshop, CSL 2002, 11th Annual Conference of the EACSL, Edinburgh, Scotland, UK, September 22-25, 2002, Proceedings(Lecture Notes in Computer Science, Vol.\u00a02471)","author":"Neven Frank","year":"2002","unstructured":"Frank Neven . 2002 . Automata, Logic, and XML. In Computer Science Logic , 16th International Workshop, CSL 2002, 11th Annual Conference of the EACSL, Edinburgh, Scotland, UK, September 22-25, 2002, Proceedings(Lecture Notes in Computer Science, Vol.\u00a02471) , Julian\u00a0C. Bradfield (Ed.). Springer, 2\u201326. https:\/\/doi.org\/10.1007\/3-540-45793-3_2 10.1007\/3-540-45793-3_2 Frank Neven. 2002. Automata, Logic, and XML. In Computer Science Logic, 16th International Workshop, CSL 2002, 11th Annual Conference of the EACSL, Edinburgh, Scotland, UK, September 22-25, 2002, Proceedings(Lecture Notes in Computer Science, Vol.\u00a02471), Julian\u00a0C. Bradfield (Ed.). Springer, 2\u201326. https:\/\/doi.org\/10.1007\/3-540-45793-3_2"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.2178\/bsl\/1208442827"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(94)00130-8"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(67)90591-8"},{"key":"e_1_3_2_1_32_1","volume-title":"15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008. Proceedings. 198\u2013213","author":"To Anthony\u00a0Widjaja","year":"2008","unstructured":"Anthony\u00a0Widjaja To and Leonid Libkin . 2008 . Recurrent Reachability Analysis in Regular Model Checking. In Logic for Programming, Artificial Intelligence, and Reasoning , 15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008. Proceedings. 198\u2013213 . https:\/\/doi.org\/10.1007\/978-3-540-89439-1_15 10.1007\/978-3-540-89439-1_15 Anthony\u00a0Widjaja To and Leonid Libkin. 2008. Recurrent Reachability Analysis in Regular Model Checking. In Logic for Programming, Artificial Intelligence, and Reasoning, 15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008. Proceedings. 198\u2013213. https:\/\/doi.org\/10.1007\/978-3-540-89439-1_15"},{"key":"e_1_3_2_1_33_1","volume-title":"13th International Conference, FOSSACS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings. 221\u2013236","author":"To Anthony\u00a0Widjaja","year":"2010","unstructured":"Anthony\u00a0Widjaja To and Leonid Libkin . 2010 . Algorithmic Metatheorems for Decidable LTL Model Checking over Infinite Systems. In Foundations of Software Science and Computational Structures , 13th International Conference, FOSSACS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings. 221\u2013236 . https:\/\/doi.org\/10.1007\/978-3-642-12032-9_16 10.1007\/978-3-642-12032-9_16 Anthony\u00a0Widjaja To and Leonid Libkin. 2010. Algorithmic Metatheorems for Decidable LTL Model Checking over Infinite Systems. In Foundations of Software Science and Computational Structures, 13th International Conference, FOSSACS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings. 221\u2013236. https:\/\/doi.org\/10.1007\/978-3-642-12032-9_16"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/321864.321865"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3040488"}],"event":{"name":"LICS '22: 37th Annual ACM\/IEEE Symposium on Logic in Computer Science","location":"Haifa Israel","acronym":"LICS '22","sponsor":["SIGLOG ACM Special Interest Group on Logic and Computation"]},"container-title":["Proceedings of the 37th Annual ACM\/IEEE Symposium on Logic in Computer Science"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3531130.3533346","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3531130.3533346","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:02:09Z","timestamp":1750186929000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3531130.3533346"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8,2]]},"references-count":36,"alternative-id":["10.1145\/3531130.3533346","10.1145\/3531130"],"URL":"https:\/\/doi.org\/10.1145\/3531130.3533346","relation":{},"subject":[],"published":{"date-parts":[[2022,8,2]]},"assertion":[{"value":"2022-08-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}