{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:17:14Z","timestamp":1750220234386,"version":"3.41.0"},"reference-count":41,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2022,1,14]],"date-time":"2022-01-14T00:00:00Z","timestamp":1642118400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"ERC","award":["AVS-ISS (648701)"],"award-info":[{"award-number":["AVS-ISS (648701)"]}]},{"name":"DFG","award":["389792660"],"award-info":[{"award-number":["389792660"]}]},{"name":"EPSRC Fellowship","award":["EP\/N008197\/1"],"award-info":[{"award-number":["EP\/N008197\/1"]}]},{"name":"European Union\u2019s Horizon 2020 research and innovation programme","award":["837327"],"award-info":[{"award-number":["837327"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2022,4,30]]},"abstract":"<jats:p>\n            Termination analysis of linear loops plays a key r\u00f4le in several areas of computer science, including program verification and abstract interpretation. Already for the simplest variants of linear loops the question of termination relates to deep open problems in number theory, such as the decidability of the Skolem and Positivity Problems for linear recurrence sequences, or equivalently reachability questions for discrete-time linear dynamical systems. In this article, we introduce the class of\n            <jats:italic>o-minimal invariants<\/jats:italic>\n            , which is broader than any previously considered, and study the decidability of the existence and algorithmic synthesis of such invariants as certificates of non-termination for linear loops equipped with a large class of halting conditions. We establish two main decidability results, one of them conditional on Schanuel\u2019s conjecture is transcendental number theory.\n          <\/jats:p>","DOI":"10.1145\/3501299","type":"journal-article","created":{"date-parts":[[2022,1,14]],"date-time":"2022-01-14T12:02:07Z","timestamp":1642161727000},"page":"1-20","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["O-Minimal Invariants for Discrete-Time Dynamical Systems"],"prefix":"10.1145","volume":"23","author":[{"given":"Shaull","family":"Almagor","sequence":"first","affiliation":[{"name":"Computer Science Department, Technion, Haifa, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dmitry","family":"Chistikov","sequence":"additional","affiliation":[{"name":"Centre for Discrete Mathematics and its Applications (DIMAP) and Department of Computer Science, University of Warwick, Coventry, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jo\u00ebl","family":"Ouaknine","sequence":"additional","affiliation":[{"name":"Max Planck Institute for Software Systems, Saarbr\u00fccken, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"James","family":"Worrell","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Oxford University, Oxford, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,1,14]]},"reference":[{"issue":"3","key":"e_1_3_2_2_2","first-page":"19","article-title":"Logarithmic forms and group varieties","volume":"442","author":"Baker Alan","year":"1993","unstructured":"Alan Baker and Gisbert W\u00fcstholz. 1993. Logarithmic forms and group varieties. Journal f\u00fcr die reine und Angewandte Mathematik 442, 3 (1993), 19\u201362.","journal-title":"Journal f\u00fcr die reine und Angewandte Mathematik"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/2629488"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/2400676.2400679"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_34"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539794276853"},{"key":"e_1_3_2_7_2","volume-title":"An Introduction to Diophantine Approximation","author":"Cassels John W. S.","year":"1965","unstructured":"John W. S. Cassels. 1965. An Introduction to Diophantine Approximation. Cambridge University Press."},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/2488608.2488728"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.5555\/2722129.2722193"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/2857050"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_39"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_1"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511525919"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-32304-2_9"},{"key":"e_1_3_2_16_2","first-page":"29:1\u201329:13","volume-title":"Proceedings of the 34th Symposium on Theoretical Aspects of Computer Science","author":"Fijalkow Nathana\u00ebl","year":"2017","unstructured":"Nathana\u00ebl Fijalkow, Pierre Ohlmann, Jo\u00ebl Ouaknine, Amaury Pouly, and James Worrell. 2017. Semialgebraic invariant synthesis for the kannan-lipton orbit problem. In Proceedings of the 34th Symposium on Theoretical Aspects of Computer Science. 29:1\u201329:13."},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00224-019-09913-3"},{"key":"e_1_3_2_18_2","volume-title":"Proceedings of the 32nd International Symposium on Theoretical Aspects of Computer Science","author":"Galby Esther","year":"2015","unstructured":"Esther Galby, Jo\u00ebl Ouaknine, and James Worrell. 2015. On matrix powering in low dimensions. In Proceedings of the 32nd International Symposium on Theoretical Aspects of Computer Science."},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/1328897.1328459"},{"key":"e_1_3_2_20_2","first-page":"118:1\u2013118:13","volume-title":"Proceedings of the 46th International Colloquium on Automata, Languages, and Programming,","author":"Hosseini Mehran","year":"2019","unstructured":"Mehran Hosseini, Jo\u00ebl Ouaknine, and James Worrell. 2019. Termination of linear loops over the integers. In Proceedings of the 46th International Colloquium on Automata, Languages, and Programming,118:1\u2013118:13."},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/800141.804673"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/3506469.3506496"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158142"},{"key":"e_1_3_2_24_2","first-page":"441","volume-title":"Proceedings of the Kreiseliana. About and Around Georg Kreisel","author":"Macintyre Angus","year":"1996","unstructured":"Angus Macintyre and Alex J. Wilkie. 1996. On the decidability of the real exponential field. In Proceedings of the Kreiseliana. About and Around Georg Kreisel, Piergiorgio Odifreddi (Ed.), A K Peters, 441\u2013467."},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511897184.016"},{"key":"e_1_3_2_26_2","article-title":"The distance between terms of an algebraic recurrence sequence","volume":"1984","author":"Mignotte M.","year":"1984","unstructured":"M. Mignotte, T. Shorey, and R. Tijdeman. 1984. The distance between terms of an algebraic recurrence sequence. Journal f\u00fcr Die Reine und Angewandte Mathematik 1984, 349 (1984), 63\u201376.","journal-title":"Journal f\u00fcr Die Reine und Angewandte Mathematik"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.5555\/2722129.2722194"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43951-7_27"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.5555\/2634074.2634101"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43951-7_28"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/2766189.2766191"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(10)80003-3"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27864-1_21"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2007.01.002"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/982962.964028"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.5555\/2621980"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.5555\/1538776"},{"key":"e_1_3_2_38_2","article-title":"A Decision Method for Elementary Algebra and Geometry","author":"Tarski Alfred","year":"1951","unstructured":"Alfred Tarski. 1951. A Decision Method for Elementary Algebra and Geometry. RAND Corporation.","journal-title":"RAND Corporation"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27813-9_6"},{"issue":"2","key":"e_1_3_2_40_2","first-page":"609","article-title":"The problem of appearance of a zero in a linear recurrence sequence (in Russian)","volume":"38","author":"Vereshchagin N. K.","year":"1985","unstructured":"N. K. Vereshchagin. 1985. The problem of appearance of a zero in a linear recurrence sequence (in Russian). Matematicheskie Zametki 38, 2 (1985), 609\u2013615.","journal-title":"Matematicheskie Zametki"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1090\/S0894-0347-96-00216-0"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2010.06.006"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3501299","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3501299","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:19Z","timestamp":1750188619000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3501299"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,14]]},"references-count":41,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2022,4,30]]}},"alternative-id":["10.1145\/3501299"],"URL":"https:\/\/doi.org\/10.1145\/3501299","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2022,1,14]]},"assertion":[{"value":"2020-06-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-11-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-01-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}