{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,26]],"date-time":"2026-01-26T14:18:09Z","timestamp":1769437089561,"version":"3.49.0"},"reference-count":62,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T00:00:00Z","timestamp":1641945600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["389792660"],"award-info":[{"award-number":["389792660"]}],"id":[{"id":"10.13039\/501100001659","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":[[2022,1,16]]},"abstract":"<jats:p>\n            We consider the MSO model-checking problem for simple linear loops, or equivalently discrete-time linear dynamical systems, with semialgebraic predicates (i.e., Boolean combinations of polynomial inequalities on the variables). We place no restrictions on the number of program variables, or equivalently the ambient dimension. We establish decidability of the model-checking problem provided that each semialgebraic predicate\n            <jats:italic>either<\/jats:italic>\n            has intrinsic dimension at most 1,\n            <jats:italic>or<\/jats:italic>\n            is contained within some three-dimensional subspace. We also note that lifting either of these restrictions and retaining decidability would necessarily require major breakthroughs in number theory.\n          <\/jats:p>","DOI":"10.1145\/3498727","type":"journal-article","created":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T17:03:12Z","timestamp":1642006992000},"page":"1-25","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":17,"title":["What\u2019s decidable about linear loops?"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9405-2332","authenticated-orcid":false,"given":"Toghrul","family":"Karimov","sequence":"first","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0875-300X","authenticated-orcid":false,"given":"Engel","family":"Lefaucheux","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0031-9356","authenticated-orcid":false,"given":"Jo\u00ebl","family":"Ouaknine","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0394-1634","authenticated-orcid":false,"given":"David","family":"Purser","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5758-0657","authenticated-orcid":false,"given":"Anton","family":"Varonka","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6006-9902","authenticated-orcid":false,"given":"Markus A.","family":"Whiteland","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8151-2443","authenticated-orcid":false,"given":"James","family":"Worrell","sequence":"additional","affiliation":[{"name":"University of Oxford, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,1,12]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2629417"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ICALP.2018.114"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434329"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ICALP.2017.24"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.STACS.2019.6"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00224-020-09976-7"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2021.28"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-32304-2_22"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429078"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2629488"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_32"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-03718-8"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(03)00314-1"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/11539452_37"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_34"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539794276853"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-013-0288-8"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2488608.2488728"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1137\/1.9781611973730.64"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2857050"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_39"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45319-9_6"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134029"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_37"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_1"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"key":"e_1_2_2_27_1","unstructured":"Graham Everest Alfred J. van der Poorten Igor E. Shparlinski and Thomas Ward. 2003. Recurrence Sequences (Mathematical surveys and monographs Vol. 104). American Mathematical Society. isbn:978-0-8218-3387-2 http:\/\/www.ams.org\/bookstore?fn=20&arg1=survseries& item=SURV-104  Graham Everest Alfred J. van der Poorten Igor E. Shparlinski and Thomas Ward. 2003. Recurrence Sequences (Mathematical surveys and monographs Vol. 104). American Mathematical Society. isbn:978-0-8218-3387-2 http:\/\/www.ams.org\/bookstore?fn=20&arg1=survseries& item=SURV-104"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00224-019-09913-3"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63166-6_10"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328459"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.dam.2005.10.009"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0015749"},{"key":"e_1_2_2_33_1","volume-title":"Lectures on Linear Sequential Machines","author":"Harrison Michael A.","unstructured":"Michael A. Harrison . 1969. Lectures on Linear Sequential Machines . Academic Press , New York . Michael A. Harrison. 1969. Lectures on Linear Sequential Machines. Academic Press, New York."},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ICALP.2019.118"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535843"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_15"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/800141.804673"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/6490.6496"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.MFCS.2020.54"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-7091-0445-3"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290368"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158142"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.dam.2009.06.021"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_8"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2008.08.004"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45187-7_17"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511897184.016"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-7091-3406-1_16"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00847-2"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3049797.3049798"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43951-7_27"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1137\/1.9781611973402.27"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43951-7_28"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2766189.2766191"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_20"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2004.1319598"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27864-1_21"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2007.01.002"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1070\/IM1984v022n03ABEH001456"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20712-9_24"},{"key":"e_1_2_2_61_1","first-page":"63","article-title":"The distance between terms of an algebraic recurrence sequence","volume":"349","author":"Tijdeman Robert","year":"1984","unstructured":"Robert Tijdeman , Maurice Mignotte , and Tarlok Nath Shorey . 1984 . The distance between terms of an algebraic recurrence sequence .. Journal f\u00fcr die reine und angewandte Mathematik , 349 (1984), 63 \u2013 76 . http:\/\/eudml.org\/doc\/152622 Robert Tijdeman, Maurice Mignotte, and Tarlok Nath Shorey. 1984. The distance between terms of an algebraic recurrence sequence.. Journal f\u00fcr die reine und angewandte Mathematik, 349 (1984), 63\u201376. http:\/\/eudml.org\/doc\/152622","journal-title":"Journal f\u00fcr die reine und angewandte Mathematik"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27813-9_6"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498727","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498727","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:29Z","timestamp":1750188629000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498727"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,12]]},"references-count":62,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2022,1,16]]}},"alternative-id":["10.1145\/3498727"],"URL":"https:\/\/doi.org\/10.1145\/3498727","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,1,12]]},"assertion":[{"value":"2022-01-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}