{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:57:32Z","timestamp":1776333452559,"version":"3.51.2"},"reference-count":78,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["101089343,101077902"],"award-info":[{"award-number":["101089343,101077902"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,1,2]]},"abstract":"<jats:p>We study Satisfiability Modulo Theories (SMT) enriched with the so-called Ramsey quantifiers, which assert the existence of cliques (complete graphs) in the graph induced by some formulas. The extended framework is known to have applications in proving program termination (in particular, whether a transitive binary predicate is well-founded), and monadic decomposability of SMT formulas. Our main result is a new algorithm for eliminating Ramsey quantifiers from three common SMT theories: Linear Integer Arithmetic (LIA), Linear Real Arithmetic (LRA), and Linear Integer Real Arithmetic (LIRA). In particular, if we work only with existentially quantified formulas, then our algorithm runs in polynomial time and produces a formula of linear size. One immediate consequence is that checking well-foundedness of a given formula in the aforementioned theory defining a transitive predicate can be straightforwardly handled by highly optimized SMT-solvers. We show also how this provides a uniform semi-algorithm for verifying termination and liveness with completeness guarantee (in fact, with an optimal computational complexity) for several well-known classes of infinite-state systems, which include succinct timed systems, one-counter systems, and monotonic counter systems. Another immediate consequence is a solution to an open problem on checking monadic decomposability of a given relation in quantifier-free fragments of LRA and LIRA, which is an important problem in automated reasoning and constraint databases. Our result immediately implies decidability of this problem with an optimal complexity (coNP-complete) and enables exploitation of SMT-solvers. It also provides a termination guarantee for the generic monadic decomposition algorithm of Veanes et al. for LIA, LRA, and LIRA. We report encouraging experimental results on a prototype implementation of our algorithms on micro-benchmarks.<\/jats:p>","DOI":"10.1145\/3632843","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"1-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Ramsey Quantifiers in Linear Arithmetics"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4681-2149","authenticated-orcid":false,"given":"Pascal","family":"Bergstr\u00e4\u00dfer","sequence":"first","affiliation":[{"name":"University of Kaiserslautern-Landau, Kaiserslautern, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0775-7781","authenticated-orcid":false,"given":"Moses","family":"Ganardi","sequence":"additional","affiliation":[{"name":"MPI-SWS, Kaiserslautern, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4715-5096","authenticated-orcid":false,"given":"Anthony W.","family":"Lin","sequence":"additional","affiliation":[{"name":"University of Kaiserslautern-Landau, Kaiserslautern, Germany"},{"name":"MPI-SWS, Kaiserslautern, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6421-4388","authenticated-orcid":false,"given":"Georg","family":"Zetzsche","sequence":"additional","affiliation":[{"name":"MPI-SWS, Kaiserslautern, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.15"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561359"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ICALP.2019.103"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-008-0064-3"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/11562948_35"},{"key":"e_1_3_1_8_1","volume-title":"Model-Theoretic Logics","author":"Barwise J.","year":"1985","unstructured":"J. Barwise and S. Feferman (Eds.). 1985. Model-Theoretic Logics. Perspectives in Logic, Vol. 8. Association for Symbolic Logic."},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876642"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","unstructured":"Pascal Bergstr\u00e4\u00dfer and Moses Ganardi. 2023a. Revisiting Membership Problems in Subclasses of Rational Relations. In 2023 38th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS). 1\u201314. https:\/\/doi.org\/10.1109\/LICS56636.2023.10175722 10.1109\/LICS56636.2023.10175722","DOI":"10.1109\/LICS56636.2023.10175722"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","unstructured":"Pascal Bergstr\u00e4\u00dfer and Moses Ganardi. 2023b. Revisiting Membership Problems in Subclasses of Rational Relations. CoRR abs\/2304.11034 (2023). https:\/\/doi.org\/10.48550\/arXiv.2304.11034 10.48550\/arXiv.2304.11034 arXiv:2304.11034","DOI":"10.48550\/arXiv.2304.11034"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","unstructured":"Pascal Bergstr\u00e4\u00dfer Moses Ganardi Anthony W. Lin and Georg Zetzsche. 2022. Ramsey Quantifiers over Automatic Structures: Complexity and Applications to Verification. In LICS \u201922: 37th Annual ACM\/IEEE Symposium on Logic in Computer Science Haifa Israel August 2 - 5 2022. 28:1\u201328:14. https:\/\/doi.org\/10.1145\/3531130.3533346 10.1145\/3531130.3533346","DOI":"10.1145\/3531130.3533346"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","unstructured":"Pascal Bergstr\u00e4\u00dfer Moses Ganardi Anthony W. Lin and Georg Zetzsche. 2023a. Ramsey Quantifiers in Linear Arithmetics. CoRR abs\/2311.04031 (2023). https:\/\/doi.org\/10.48550\/arXiv.2311.04031 10.48550\/arXiv.2311.04031 arXiv:2311.04031","DOI":"10.48550\/arXiv.2311.04031"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","unstructured":"Pascal Bergstr\u00e4\u00dfer Moses Ganardi Anthony W. Lin and Georg Zetzsche. 2023b. Ramsey Quantifiers in Linear Arithmetics -Artifact. https:\/\/doi.org\/10.5281\/zenodo.8422415 10.5281\/zenodo.8422415","DOI":"10.5281\/zenodo.8422415"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_61"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","unstructured":"Nikolaj S. Bj\u00f8rner Arie Gurfinkel Kenneth L. McMillan and Andrey Rybalchenko. 2015. Horn Clause Solvers for Program Verification. In Fields of Logic and Computation II - Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday (Lecture Notes in Computer Science Vol. 9300) Lev D. Beklemishev Andreas Blass Nachum Dershowitz Bernd Finkbeiner and Wolfram Schulte (Eds.). Springer 24\u201351. https:\/\/doi.org\/10.1007\/978-3-319-23534-9_2 10.1007\/978-3-319-23534-9_2","DOI":"10.1007\/978-3-319-23534-9_2"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.29007\/1l7f"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_28"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005068"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2000.855755"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_40"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_24"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9939-1976-0396605-3"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-011-0111-7"},{"key":"e_1_3_1_25_1","first-page":"64","volume-title":"Hybrid Systems II, Proceedings of the Third International Workshop on Hybrid Systems, Ithaca, NY, USA, October 1994 (Lecture Notes in Computer Science, Vol. 999)","author":"Bouajjani Ahmed","year":"1994","unstructured":"Ahmed Bouajjani, Rachid Echahed, and Riadh Robbana. 1994. On the Automatic Verification of Systems with Continuous Variables and Unbounded Discrete Data Structures. In Hybrid Systems II, Proceedings of the Third International Workshop on Hybrid Systems, Ithaca, NY, USA, October 1994 (Lecture Notes in Computer Science, Vol. 999), Panos J. Antsaklis, Wolf Kohn, Anil Nerode, and Shankar Sastry (Eds.). Springer, 64\u201385. https:\/\/doi.org\/10.1007\/3-540-60472-3_4"},{"key":"e_1_3_1_26_1","volume-title":"Model Theory","author":"Chang C.C.","year":"1990","unstructured":"C.C. Chang and H. J. Keisler. 1990. Model Theory. Elsevier."},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ICALP.2018.118"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48320-9_18"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1941487.1941509"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS52979.2021.00120"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44585-4_48"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00743-0"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054102001539"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_9"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44693-1_12"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSTTCS.2019.41"},{"key":"e_1_3_1_38_1","unstructured":"Alain Finkel and Ekanshdeep Gupta. 2019b. The Well Structured Problem for Presburger Counter Machines. CoRR abs\/1910.02736 (2019). arXiv:1910.02736"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00102-X"},{"key":"e_1_3_1_40_1","article-title":"Solution d\u2019une question particuliere du calcul des in\u00e9galit\u00e9s","volume":"99","author":"Joseph Fourier Jean Baptiste","year":"1826","unstructured":"Jean Baptiste Joseph Fourier. 1826. Solution d\u2019une question particuliere du calcul des in\u00e9galit\u00e9s. Nouveau Bulletin des Sciences par la Soci\u00e9t\u00e9 philomatique de Paris 99 (1826).","journal-title":"Nouveau Bulletin des Sciences par la Soci\u00e9t\u00e9 philomatique de Paris"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9939-1966-0201310-3"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","unstructured":"Mario Grobler Leif Sabellek and Sebastian Siebertz. 2023. Parikh Automata on Infinite Words. CoRR abs\/2301.08969 (2023). https:\/\/doi.org\/10.48550\/arXiv.2301.08969 10.48550\/arXiv.2301.08969 arXiv:2301.08969","DOI":"10.48550\/arXiv.2301.08969"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011464022461"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSTTCS.2022.40"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04081-8_25"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_60"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","unstructured":"Matthew Hague and Anthony Widjaja Lin. 2012. Synchronisation- and Reversal-Bounded Analysis of Multithreaded Programs with Counters. In Computer Aided Verification - 24th International Conference CAV 2012 Berkeley CA USA July 7-13 2012 Proceedings. 260\u2013276. https:\/\/doi.org\/10.1007\/978-3-642-31424-7_22 10.1007\/978-3-642-31424-7_22","DOI":"10.1007\/978-3-642-31424-7_22"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51074-9_8"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/322047.322058"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44612-5_38"},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/1592434.1592438"},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45061-0_54"},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-04031-7"},{"key":"e_1_3_1_54_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.STACS.2010.2483"},{"key":"e_1_3_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_52"},{"key":"e_1_3_1_56_1","unstructured":"K. Rustan M. Leino. 2023. Program Proofs. (2023)."},{"key":"e_1_3_1_57_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS52979.2021.00121"},{"key":"e_1_3_1_58_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785796"},{"key":"e_1_3_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-62822-2_6"},{"key":"e_1_3_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/937555.937557"},{"key":"e_1_3_1_61_1","article-title":"The reachability problem is exponential-space hard","volume":"62","author":"Lipton Richard","year":"1976","unstructured":"Richard Lipton. 1976. The reachability problem is exponential-space hard. Yale University, Department of Computer Science, Report 62 (1976).","journal-title":"Yale University, Department of Computer Science, Report"},{"key":"e_1_3_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/321592.321606"},{"key":"e_1_3_1_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_12"},{"key":"e_1_3_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/322186.322198"},{"key":"e_1_3_1_65_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2004.1319598"},{"key":"e_1_3_1_66_1","unstructured":"Mojzesz Presburger. 1929. \u00dcber die Vollst\u00e4ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen in welchem die Addition als einzige Operation hervortritt. Comptes Rendus du I congres de Mathematiciens de Pays Slaves (1929)."},{"key":"e_1_3_1_67_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_7"},{"key":"e_1_3_1_68_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005098"},{"key":"e_1_3_1_69_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(78)90036-1"},{"key":"e_1_3_1_70_1","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/s2-30.1.264"},{"key":"e_1_3_1_71_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273152"},{"key":"e_1_3_1_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/2422.322411"},{"key":"e_1_3_1_73_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(85)90076-6"},{"key":"e_1_3_1_74_1","doi-asserted-by":"publisher","unstructured":"Anthony Widjaja To. 2009. Model Checking FO(R) over One-Counter Processes and beyond. In Computer Science Logic 23rd international Workshop CSL 2009 18th Annual Conference of the EACSL Coimbra Portugal September 7-11 2009. Proceedings. 485\u2013499. https:\/\/doi.org\/10.1007\/978-3-642-04027-6_35 10.1007\/978-3-642-04027-6_35","DOI":"10.1007\/978-3-642-04027-6_35"},{"key":"e_1_3_1_75_1","doi-asserted-by":"publisher","unstructured":"Anthony Widjaja 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","DOI":"10.1007\/978-3-540-89439-1_15"},{"key":"e_1_3_1_76_1","doi-asserted-by":"publisher","DOI":"10.1145\/3040488"},{"key":"e_1_3_1_77_1","doi-asserted-by":"publisher","DOI":"10.1145\/258726.258746"},{"key":"e_1_3_1_78_1","doi-asserted-by":"publisher","DOI":"10.1145\/309831.309888"},{"key":"e_1_3_1_79_1","doi-asserted-by":"publisher","DOI":"10.2307\/2322281"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632843","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632843","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:06:05Z","timestamp":1751659565000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632843"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":78,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632843"],"URL":"https:\/\/doi.org\/10.1145\/3632843","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}