{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,11]],"date-time":"2026-05-11T11:13:57Z","timestamp":1778498037575,"version":"3.51.4"},"reference-count":67,"publisher":"Springer Science and Business Media LLC","issue":"1-3","license":[{"start":{"date-parts":[[2023,12,4]],"date-time":"2023-12-04T00:00:00Z","timestamp":1701648000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,12,4]],"date-time":"2023-12-04T00:00:00Z","timestamp":1701648000000},"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"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"crossref","award":["235950644"],"award-info":[{"award-number":["235950644"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"crossref","award":["2236 (UnRAVeL)"],"award-info":[{"award-number":["2236 (UnRAVeL)"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100007210","name":"RWTH Aachen University","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100007210","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2025,4]]},"abstract":"Abstract<\/jats:title>\n We consider the problem of proving termination for triangular weakly non-linear loops (twn<\/jats:italic>-loops) over some ring \n \n $$\\mathcal {S}$$<\/jats:tex-math>\n \n S<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula> like \n \n $$\\mathbb {Z}$$<\/jats:tex-math>\n \n Z<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>, \n \n $$\\mathbb {Q}$$<\/jats:tex-math>\n \n Q<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>, or \n \n $$\\mathbb {R}$$<\/jats:tex-math>\n \n R<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>. The guard of such a loop is an arbitrary quantifier-free Boolean formula over (possibly non-linear) polynomial inequations, and the body is a single assignment of the form \n \n $$\\begin{bmatrix} x_1\\\\ \\ldots \\\\ x_d \\end{bmatrix} \\leftarrow \\begin{bmatrix} c_1 \\cdot x_1 + p_1\\\\ \\ldots \\\\ c_d \\cdot x_d + p_d \\end{bmatrix}$$<\/jats:tex-math>\n \n \n \n \n \n \n \n \n x<\/mml:mi>\n 1<\/mml:mn>\n <\/mml:msub>\n <\/mml:mtd>\n <\/mml:mtr>\n \n \n \n \n \u2026<\/mml:mo>\n <\/mml:mrow>\n <\/mml:mtd>\n <\/mml:mtr>\n \n \n \n \n \n x<\/mml:mi>\n d<\/mml:mi>\n <\/mml:msub>\n <\/mml:mrow>\n <\/mml:mtd>\n <\/mml:mtr>\n <\/mml:mtable>\n <\/mml:mrow>\n <\/mml:mfenced>\n \u2190<\/mml:mo>\n \n \n \n \n \n \n \n c<\/mml:mi>\n 1<\/mml:mn>\n <\/mml:msub>\n \u00b7<\/mml:mo>\n \n x<\/mml:mi>\n 1<\/mml:mn>\n <\/mml:msub>\n +<\/mml:mo>\n \n p<\/mml:mi>\n 1<\/mml:mn>\n <\/mml:msub>\n <\/mml:mrow>\n <\/mml:mtd>\n <\/mml:mtr>\n \n \n \n \n \u2026<\/mml:mo>\n <\/mml:mrow>\n <\/mml:mtd>\n <\/mml:mtr>\n \n \n \n \n \n c<\/mml:mi>\n d<\/mml:mi>\n <\/mml:msub>\n \u00b7<\/mml:mo>\n \n x<\/mml:mi>\n d<\/mml:mi>\n <\/mml:msub>\n +<\/mml:mo>\n \n p<\/mml:mi>\n d<\/mml:mi>\n <\/mml:msub>\n <\/mml:mrow>\n <\/mml:mtd>\n <\/mml:mtr>\n <\/mml:mtable>\n <\/mml:mrow>\n <\/mml:mfenced>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula> where each \n \n $$x_i$$<\/jats:tex-math>\n \n \n x<\/mml:mi>\n i<\/mml:mi>\n <\/mml:msub>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula> is a variable, \n \n $$c_i \\in \\mathcal {S}$$<\/jats:tex-math>\n \n \n \n c<\/mml:mi>\n i<\/mml:mi>\n <\/mml:msub>\n \u2208<\/mml:mo>\n S<\/mml:mi>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>, and each \n \n $$p_i$$<\/jats:tex-math>\n \n \n p<\/mml:mi>\n i<\/mml:mi>\n <\/mml:msub>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula> is a (possibly non-linear) polynomial over \n \n $$\\mathcal {S}$$<\/jats:tex-math>\n \n S<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula> and the variables \n \n $$x_{i+1},\\ldots ,x_{d}$$<\/jats:tex-math>\n \n \n \n x<\/mml:mi>\n \n i<\/mml:mi>\n +<\/mml:mo>\n 1<\/mml:mn>\n <\/mml:mrow>\n <\/mml:msub>\n ,<\/mml:mo>\n \u2026<\/mml:mo>\n ,<\/mml:mo>\n \n x<\/mml:mi>\n d<\/mml:mi>\n <\/mml:msub>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>. <\/jats:p>\n We show that the question of termination can be reduced to the existential fragment of the first-order theory of \n \n $$\\mathcal {S}$$<\/jats:tex-math>\n \n S<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>. For loops over \n \n $$\\mathbb {R}$$<\/jats:tex-math>\n \n R<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>, our reduction implies decidability of termination. For loops over \n \n $$\\mathbb {Z}$$<\/jats:tex-math>\n \n Z<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula> and \n \n $$\\mathbb {Q}$$<\/jats:tex-math>\n \n Q<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>, it proves semi-decidability of non-termination.<\/jats:p>\n Furthermore, we present a transformation to convert certain non-twn<\/jats:italic>-loops into twn<\/jats:italic>-form. Then the original loop terminates iff the transformed loop terminates over a specific subset of \n \n $$\\mathbb {R}$$<\/jats:tex-math>\n \n R<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>, which can also be checked via our reduction. Moreover, we formalize a technique to linearize<\/jats:italic> (the updates of) twn<\/jats:italic>-loops in our setting and analyze its complexity. Based on these results, we prove complexity bounds for the termination problem of twn<\/jats:italic>-loops as well as tight<\/jats:italic> bounds for two important classes of loops which can always<\/jats:italic> be transformed into twn<\/jats:italic>-loops.<\/jats:p>\n Finally, we show that there is an important class of linear loops. where our decision procedure results in an efficient<\/jats:italic> procedure for termination analysis, i.e., where the parameterized complexity of deciding termination is polynomial<\/jats:italic>.<\/jats:p>","DOI":"10.1007\/s10703-023-00440-z","type":"journal-article","created":{"date-parts":[[2023,12,4]],"date-time":"2023-12-04T16:02:07Z","timestamp":1701705727000},"page":"70-132","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Termination of triangular polynomial loops"],"prefix":"10.1007","volume":"65","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5111-3177","authenticated-orcid":false,"given":"Marcel","family":"Hark","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0902-1994","authenticated-orcid":false,"given":"Florian","family":"Frohn","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0283-8520","authenticated-orcid":false,"given":"J\u00fcrgen","family":"Giesl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,12,4]]},"reference":[{"key":"440_CR1","doi-asserted-by":"publisher","unstructured":"Alias C, Darte A, Feautrier P, Gonnord L (2010) Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs. In: Proceedings of the SAS, LNCS 6337, pp 117\u2013133, https:\/\/doi.org\/10.1007\/978-3-642-15769-1_8","DOI":"10.1007\/978-3-642-15769-1_8"},{"key":"440_CR2","doi-asserted-by":"publisher","unstructured":"Basu S, Pollack R, Roy MF (2006) Algorithms in real algebraic geometry. Algorithms and Comp. in Math. 10, Springer https:\/\/doi.org\/10.1007\/3-540-33099-2","DOI":"10.1007\/3-540-33099-2"},{"key":"440_CR3","first-page":"969","volume-title":"Handbook of discrete and computational geometry","author":"S Basu","year":"2017","unstructured":"Basu S, Mishra B (2017) Computational and quantitative real algebraic geometry. In: Goodman JE, O\u2019Rourke J, T\u00f3th CD (eds) Handbook of discrete and computational geometry, 3rd edn. CRC, Boca Raton, pp 969\u20131002","edition":"3"},{"key":"440_CR4","doi-asserted-by":"publisher","unstructured":"Ben-Amram AM, Genaim S, Masud AN (2012) On the termination of integer loops. ACM Trans Prog Lang Syst 34(4). https:\/\/doi.org\/10.1145\/2400676.2400679","DOI":"10.1145\/2400676.2400679"},{"key":"440_CR5","doi-asserted-by":"publisher","unstructured":"Ben-Amram AM, Genaim S (2014) Ranking functions for linear-constraint loops. J ACM 61(4). https:\/\/doi.org\/10.1145\/2629488","DOI":"10.1145\/2629488"},{"key":"440_CR6","doi-asserted-by":"publisher","unstructured":"Ben-Amram AM, Genaim S (2017) On multiphase-linear ranking functions. In: Proceedings of the CAV, LNCS 10427, pp 601\u2013620, https:\/\/doi.org\/10.1007\/978-3-319-63390-9_32","DOI":"10.1007\/978-3-319-63390-9_32"},{"key":"440_CR7","doi-asserted-by":"publisher","unstructured":"Ben-Amram AM, Dom\u00e9nech JJ, Genaim S (2019) Multiphase-linear ranking functions and their relation to recurrent sets. In: Proceedings of the SAS, LNCS 11822, pp 459\u2013480, https:\/\/doi.org\/10.1007\/978-3-030-32304-2_22","DOI":"10.1007\/978-3-030-32304-2_22"},{"key":"440_CR8","doi-asserted-by":"publisher","unstructured":"Bozga M, Iosif R, Konecn\u00fd F (2014) Deciding conditional termination. Log Methods Comput Sci 10(3). https:\/\/doi.org\/10.2168\/LMCS-10(3:8)2014","DOI":"10.2168\/LMCS-10(3:8)2014"},{"key":"440_CR9","doi-asserted-by":"publisher","unstructured":"Bradley AR, Manna Z, Sipma HB (2005) Linear ranking with reachability. In: Proceedings of the CAV, LNCS 3576, pp 491\u2013504, https:\/\/doi.org\/10.1007\/11513988_48","DOI":"10.1007\/11513988_48"},{"key":"440_CR10","doi-asserted-by":"publisher","unstructured":"Braverman M (2006) Termination of integer linear programs. In: Proceedings of the CAV, LNCS 4144, pp 372\u2013385, https:\/\/doi.org\/10.1007\/11817963_34","DOI":"10.1007\/11817963_34"},{"key":"440_CR11","doi-asserted-by":"publisher","unstructured":"Brockschmidt M, Cook B, Fuhs C (2013) Better termination proving through cooperation. In: Proceedings of the CAV, LNCS 8044, pp 413\u2013429, https:\/\/doi.org\/10.1007\/978-3-642-39799-8_28","DOI":"10.1007\/978-3-642-39799-8_28"},{"key":"440_CR12","doi-asserted-by":"publisher","unstructured":"Canny JF (1988) Some algebraic and geometric computations in PSPACE. In: Proceedings of the STOC, pp 460\u2013467, https:\/\/doi.org\/10.1145\/62212.62257","DOI":"10.1145\/62212.62257"},{"issue":"2","key":"440_CR13","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1002\/cpa.3160220202","volume":"22","author":"PJ Cohen","year":"1969","unstructured":"Cohen PJ (1969) Decision procedures for real and $$p$$-adic fields. Commun Pure Appl Math 22(2):131\u2013151. https:\/\/doi.org\/10.1002\/cpa.3160220202","journal-title":"Commun Pure Appl Math"},{"key":"440_CR14","doi-asserted-by":"publisher","unstructured":"Dai L, Xia B (2012) Non-termination sets of simple linear loops. In: Proceedings of the ICTAC, LNCS 7521, pp 61\u201373, https:\/\/doi.org\/10.1007\/978-3-642-32943-2_5","DOI":"10.1007\/978-3-642-32943-2_5"},{"key":"440_CR15","doi-asserted-by":"crossref","first-page":"73","DOI":"10.2307\/1905523","volume":"17","author":"GB Dantzig","year":"1949","unstructured":"Dantzig GB (1949) Programming in a linear structure. Econometrica 17:73\u201374 (Report of the September 9, 1948 meeting in Madison)","journal-title":"Econometrica"},{"key":"440_CR16","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0515-9","volume-title":"Parameterized complexity. Monographs in computer science","author":"RG Downey","year":"1999","unstructured":"Downey RG, Fellows MR (1999) Parameterized complexity. Monographs in computer science. Springer, Berlin. https:\/\/doi.org\/10.1007\/978-1-4612-0515-9"},{"key":"440_CR17","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1016\/0024-3795(95)00095-X","volume":"247","author":"A van den Essen","year":"1996","unstructured":"van den Essen A, Hubbers E (1996) Polynomial maps with strongly nilpotent Jacobian matrix and the Jacobian conjecture. Linear Algebra Appl 247:121\u2013132. https:\/\/doi.org\/10.1016\/0024-3795(95)00095-X","journal-title":"Linear Algebra Appl"},{"key":"440_CR18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-0348-8440-2","volume-title":"Polynomial automorphisms and the Jacobian conjecture","author":"A van den Essen","year":"2000","unstructured":"van den Essen A (2000) Polynomial automorphisms and the Jacobian conjecture. Springer, Berlin. https:\/\/doi.org\/10.1007\/978-3-0348-8440-2"},{"key":"440_CR19","doi-asserted-by":"publisher","unstructured":"Frohn F, Giesl J (2019) Termination of triangular integer loops is decidable. In: Proceedings of the CAV, LNCS 11562, pp 269\u2013286, https:\/\/doi.org\/10.1007\/978-3-030-25543-5_24","DOI":"10.1007\/978-3-030-25543-5_24"},{"key":"440_CR20","doi-asserted-by":"publisher","unstructured":"Frohn F, Hark M, Giesl J (2020) Termination of polynomial loops. In: Proceedings of the SAS, LNCS 12389, pp 89\u2013112, https:\/\/doi.org\/10.1007\/978-3-030-65474-0_5","DOI":"10.1007\/978-3-030-65474-0_5"},{"key":"440_CR21","doi-asserted-by":"publisher","unstructured":"Frohn F (2020) A calculus for modular loop acceleration. In: Proceedings of the TACAS, LNCS 12078, pp 58\u201376, https:\/\/doi.org\/10.1007\/978-3-030-45190-5_4","DOI":"10.1007\/978-3-030-45190-5_4"},{"key":"440_CR22","doi-asserted-by":"publisher","unstructured":"Frumkin MA (1977) Polynomial time algorithms in the theory of linear diophantine equations. In: Proceedings of the FCT, LNCS 56, pp 386\u2013392, https:\/\/doi.org\/10.1007\/3-540-08442-8_106","DOI":"10.1007\/3-540-08442-8_106"},{"issue":"5","key":"440_CR23","doi-asserted-by":"publisher","first-page":"948","DOI":"10.1137\/S0097539793252687","volume":"24","author":"M Giesbrecht","year":"1995","unstructured":"Giesbrecht M (1995) Nearly optimal algorithms for canonical matrix forms. SIAM J Comput 24(5):948\u2013969. https:\/\/doi.org\/10.1137\/S0097539793252687","journal-title":"SIAM J Comput"},{"issue":"1","key":"440_CR24","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10817-016-9388-y","volume":"58","author":"J Giesl","year":"2017","unstructured":"Giesl J, Aschermann C, Brockschmidt M, Emmes F, Frohn F, Fuhs C, Hensel J, Otto C, Pl\u00fccker M, Schneider-Kamp P, Str\u00f6der T, Swiderski S, Thiemann R (2017) Analyzing program termination and complexity automatically with AProVE. J Autom Reason 58(1):3\u201331. https:\/\/doi.org\/10.1007\/s10817-016-9388-y","journal-title":"J Autom Reason"},{"key":"440_CR25","doi-asserted-by":"publisher","unstructured":"Giesl J, Rubio A, Sternagel C, Waldmann J, Yamada A (2019) The termination and complexity competition. In: Proceedings of the TACAS, LNCS 11429, pp 156\u2013166, https:\/\/doi.org\/10.1007\/978-3-030-17502-3_10","DOI":"10.1007\/978-3-030-17502-3_10"},{"key":"440_CR26","unstructured":"Gomory R (1960) An algorithm for the mixed integer problem. Tech. Rep. RM-2597, The RAND Corporation, https:\/\/www.rand.org\/pubs\/research_memoranda\/RM2597.html"},{"key":"440_CR27","volume-title":"Concrete mathematics: a foundation for computer science","author":"RL Graham","year":"1994","unstructured":"Graham RL, Knuth DE, Patashnik O (1994) Concrete mathematics: a foundation for computer science, 2nd edn. Addison-Wesley, Boston","edition":"2"},{"key":"440_CR28","doi-asserted-by":"publisher","unstructured":"Hark M, Frohn F, Giesl J (2020) Polynomial loops: Beyond termination. In: Proceedings of the LPAR, EPiC 73, pp 279\u2013297, https:\/\/doi.org\/10.29007\/nxv1","DOI":"10.29007\/nxv1"},{"key":"440_CR29","doi-asserted-by":"publisher","unstructured":"Hark M (2021) Towards complete methods for automated complexity and termination analysis of (probabilistic) programs. PhD thesis, RWTH Aachen University, Germany, https:\/\/doi.org\/10.18154\/RWTH-2021-06073","DOI":"10.18154\/RWTH-2021-06073"},{"key":"440_CR30","doi-asserted-by":"publisher","unstructured":"Hark M, Frohn F, Giesl J (2022) Termination of triangular polynomial loops. CoRR abs\/1910.11588, https:\/\/doi.org\/10.48550\/arXiv.1910.11588","DOI":"10.48550\/arXiv.1910.11588"},{"key":"440_CR31","doi-asserted-by":"publisher","unstructured":"Hosseini M, Ouaknine J, Worrell J (2019) Termination of linear loops over the integers. In: Proceedings of the ICALP, LIPIcs 132, https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2019.118","DOI":"10.4230\/LIPIcs.ICALP.2019.118"},{"key":"440_CR32","doi-asserted-by":"publisher","unstructured":"Humenberger A, Kov\u00e1cs L (2021) Algebra-based synthesis of loops and their invariants (invited paper). In: Proceedings of the VMCAI, LNCS 12597, pp 17\u201328, https:\/\/doi.org\/10.1007\/978-3-030-67067-2_2","DOI":"10.1007\/978-3-030-67067-2_2"},{"issue":"4","key":"440_CR33","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1287\/mnsc.6.4.366","volume":"6","author":"LV Kantorovich","year":"1960","unstructured":"Kantorovich LV (1960) Mathematical methods of organizing and planning production. Manage Sci 6(4):366\u2013422. https:\/\/doi.org\/10.1287\/mnsc.6.4.366","journal-title":"Manage Sci"},{"key":"440_CR34","doi-asserted-by":"publisher","unstructured":"Kauers M, Paule P (2011) The concrete tetrahedron\u2014symbolic sums. Recurrence equations, generating functions, asymptotic estimates. Springer https:\/\/doi.org\/10.1007\/978-3-7091-0445-3","DOI":"10.1007\/978-3-7091-0445-3"},{"key":"440_CR35","doi-asserted-by":"publisher","unstructured":"Kincaid Z, Breck J, Cyphert J, Reps TW (2019) Closed forms for numerical loops. Proc ACM Progr Lang 3(POPL). https:\/\/doi.org\/10.1145\/3290368","DOI":"10.1145\/3290368"},{"key":"440_CR36","doi-asserted-by":"publisher","unstructured":"Kov\u00e1cs L (2008) Reasoning algebraically about $$p$$-solvable loops. In: Proceedings of the TACAS, LNCS 4963, pp 249\u2013264, https:\/\/doi.org\/10.1007\/978-3-540-78800-3_18","DOI":"10.1007\/978-3-540-78800-3_18"},{"issue":"3","key":"440_CR37","doi-asserted-by":"publisher","first-page":"497","DOI":"10.2307\/1910129","volume":"28","author":"AH Land","year":"1960","unstructured":"Land AH, Doig AG (1960) An automatic method of solving discrete programming problems. Econometrica 28(3):497\u2013520. https:\/\/doi.org\/10.2307\/1910129","journal-title":"Econometrica"},{"key":"440_CR38","unstructured":"Landau E (1909) Handbuch der Lehre von der Verteilung der Primzahlen. Teubner"},{"key":"440_CR39","doi-asserted-by":"publisher","unstructured":"Larraz D, Oliveras A, Rodr\u00edguez-Carbonell E, Rubio A (2013) Proving termination of imperative programs using Max-SMT. In: Proceedings of the FMCAD, pp 218\u2013225, https:\/\/doi.org\/10.1109\/FMCAD.2013.6679413","DOI":"10.1109\/FMCAD.2013.6679413"},{"key":"440_CR40","doi-asserted-by":"publisher","unstructured":"Leike J, Heizmann M (2015) Ranking templates for linear loops. Log Methods Comput Sci 11(1). https:\/\/doi.org\/10.2168\/LMCS-11(1:16)2015","DOI":"10.2168\/LMCS-11(1:16)2015"},{"issue":"4","key":"440_CR41","doi-asserted-by":"publisher","first-page":"538","DOI":"10.1287\/moor.8.4.538","volume":"8","author":"HW Lenstra Jr","year":"1983","unstructured":"Lenstra HW Jr (1983) Integer programming with a fixed number of variables. Math Oper Res 8(4):538\u2013548. https:\/\/doi.org\/10.1287\/moor.8.4.538","journal-title":"Math Oper Res"},{"key":"440_CR42","doi-asserted-by":"publisher","unstructured":"Li Y (2014) A recursive decision method for termination of linear programs. In: Proceedings of the SNC, pp 97\u2013106, https:\/\/doi.org\/10.1145\/2631948.2631966","DOI":"10.1145\/2631948.2631966"},{"key":"440_CR43","doi-asserted-by":"publisher","unstructured":"Li Y (2016) Termination of single-path polynomial loop programs. In: Proceedings of the ICTAC, LNCS 9965, pp 33\u201350, https:\/\/doi.org\/10.1007\/978-3-319-46750-4_3","DOI":"10.1007\/978-3-319-46750-4_3"},{"key":"440_CR44","doi-asserted-by":"publisher","unstructured":"Li Y (2017a) Termination of semi-algebraic loop programs. In: Proceedings of the SETTA, LNCS 10606, pp 131\u2013146, https:\/\/doi.org\/10.1007\/978-3-319-69483-2_8","DOI":"10.1007\/978-3-319-69483-2_8"},{"key":"440_CR45","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1016\/j.tcs.2017.03.036","volume":"681","author":"Y Li","year":"2017","unstructured":"Li Y (2017b) Witness to non-termination of linear programs. Theor Comput Sci 681:75\u2013100. https:\/\/doi.org\/10.1016\/j.tcs.2017.03.036","journal-title":"Theor Comput Sci"},{"key":"440_CR46","first-page":"279","volume":"191","author":"JV Matijasevi\u010d","year":"1970","unstructured":"Matijasevi\u010d JV (1970) The Diophantineness of enumerable sets. Dokl Akad Nauk SSSR 191:279\u2013282","journal-title":"Dokl Akad Nauk SSSR"},{"key":"440_CR47","doi-asserted-by":"publisher","unstructured":"Neumann E, Ouaknine J, Worrell J (2020) On ranking function synthesis and termination for polynomial programs. In: Proceedings of the CONCUR, LIPIcs 171, https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2020.15","DOI":"10.4230\/LIPIcs.CONCUR.2020.15"},{"key":"440_CR48","doi-asserted-by":"publisher","unstructured":"de\u00a0Oliveira S, Bensalem S, Prevosto V (2016) Polynomial invariants by linear algebra. In: Proceedings of the ATVA, LNCS 9938, pp 479\u2013494, https:\/\/doi.org\/10.1007\/978-3-319-46520-3_30","DOI":"10.1007\/978-3-319-46520-3_30"},{"key":"440_CR49","doi-asserted-by":"publisher","unstructured":"Ouaknine J, Pinto JS, Worrell J (2015) On termination of integer linear loops. In: Proceedings of the SODA, pp 957\u2013969, https:\/\/doi.org\/10.1137\/1.9781611973730.65","DOI":"10.1137\/1.9781611973730.65"},{"issue":"1\u20132","key":"440_CR50","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/s10107-016-1036-0","volume":"162","author":"AD Pia","year":"2017","unstructured":"Pia AD, Dey SS, Molinaro M (2017) Mixed-integer quadratic programming is in NP. Math Program 162(1\u20132):225\u2013240. https:\/\/doi.org\/10.1007\/s10107-016-1036-0","journal-title":"Math Program"},{"key":"440_CR51","doi-asserted-by":"publisher","unstructured":"Podelski A, Rybalchenko A (2004) A complete method for the synthesis of linear ranking functions. In: Proceedings of the VMCAI, LNCS 2937, pp 239\u2013251, https:\/\/doi.org\/10.1007\/978-3-540-24622-0_20","DOI":"10.1007\/978-3-540-24622-0_20"},{"issue":"3","key":"440_CR52","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1016\/S0747-7171(10)80003-3","volume":"13","author":"J Renegar","year":"1992","unstructured":"Renegar J (1992) On the computational complexity and geometry of the first-order theory of the reals, Part I: Introduction. Preliminaries. The geometry of semi-algebraic sets. The decision problem for the existential theory of the reals. J Symb Comput 13(3):255\u2013300. https:\/\/doi.org\/10.1016\/S0747-7171(10)80003-3","journal-title":"J Symb Comput"},{"issue":"2","key":"440_CR53","doi-asserted-by":"publisher","first-page":"98","DOI":"10.2307\/2266510","volume":"14","author":"J Robinson","year":"1949","unstructured":"Robinson J (1949) Definability and decision problems in arithmetic. J Symb Log 14(2):98\u2013114. https:\/\/doi.org\/10.2307\/2266510","journal-title":"J Symb Log"},{"issue":"02","key":"440_CR54","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1142\/S0129626496000200","volume":"06","author":"JL Roch","year":"1996","unstructured":"Roch JL, Villard G (1996) Fast parallel computation of the Jordan normal form of matrices. Parallel Process Lett 06(02):203\u2013212. https:\/\/doi.org\/10.1142\/S0129626496000200","journal-title":"Parallel Process Lett"},{"key":"440_CR55","doi-asserted-by":"publisher","unstructured":"Roche DS (2018) What can (and can\u2019t) we do with sparse polynomials? In: Proceedings of the ISSAC, pp 25\u201330, https:\/\/doi.org\/10.1145\/3208976.3209027","DOI":"10.1145\/3208976.3209027"},{"key":"440_CR56","doi-asserted-by":"publisher","unstructured":"Rodr\u00edguez-Carbonell E, Kapur D (2004) Automatic generation of polynomial loop invariants: Algebraic foundation. In: Proceedings of the ISSAC, pp 266\u2013273, https:\/\/doi.org\/10.1145\/1005285.1005324","DOI":"10.1145\/1005285.1005324"},{"key":"440_CR57","doi-asserted-by":"publisher","unstructured":"Schaefer M (2009) Complexity of some geometric and topological problems. In: Proceedings of the GD, LNCS 5849, pp 334\u2013344, https:\/\/doi.org\/10.1007\/978-3-642-11805-0_32","DOI":"10.1007\/978-3-642-11805-0_32"},{"issue":"2","key":"440_CR58","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/s00224-015-9662-0","volume":"60","author":"M Schaefer","year":"2017","unstructured":"Schaefer M, Stefankovic D (2017) Fixed points, Nash equilibria, and the existential theory of the reals. Theory Comput Syst 60(2):172\u2013193. https:\/\/doi.org\/10.1007\/s00224-015-9662-0","journal-title":"Theory Comput Syst"},{"issue":"5","key":"440_CR59","doi-asserted-by":"publisher","first-page":"756","DOI":"10.1134\/S0001434619050122","volume":"105","author":"SV Sidorov","year":"2019","unstructured":"Sidorov SV (2019) On the similarity of certain integer matrices with single eigenvalue over the ring of integers. Math Notes 105(5):756\u2013762. https:\/\/doi.org\/10.1134\/S0001434619050122","journal-title":"Math Notes"},{"key":"440_CR60","doi-asserted-by":"publisher","unstructured":"Storjohann A, Labahn G (1996) Asymptotically fast computation of Hermite normal forms of integer matrices. In: Proceedings of the ISSAC, pp 259\u2013266, https:\/\/doi.org\/10.1145\/236869.237083","DOI":"10.1145\/236869.237083"},{"key":"440_CR61","doi-asserted-by":"publisher","unstructured":"Tarski A (1998) A decision method for elementary algebra and geometry. In: Caviness BF, Johnson JR (eds) Quantifier elimination and cylindrical algebraic decomposition, Springer, pp 24\u201384, https:\/\/doi.org\/10.1007\/978-3-7091-9459-1 originally appeared in 1951, U California Press, Berkeley and Los Angeles","DOI":"10.1007\/978-3-7091-9459-1"},{"key":"440_CR62","doi-asserted-by":"publisher","unstructured":"Tiwari A (2004) Termination of linear programs. In: Proceedings of the CAV, LNCS 3114, pp 70\u201382 https:\/\/doi.org\/10.1007\/978-3-540-27813-9_6","DOI":"10.1007\/978-3-540-27813-9_6"},{"key":"440_CR63","unstructured":"TPDB (2003\u20132021) Termination Problems Data Base. http:\/\/www.termination-portal.org\/wiki\/TPDB"},{"key":"440_CR64","doi-asserted-by":"publisher","unstructured":"Wu B, Shen L, Bi Z, Zeng Z (2010) Termination of loop programs with polynomial guards. In: Proceedings of the ICCSA, LNCS 6019, pp 482\u2013496, https:\/\/doi.org\/10.1007\/978-3-642-12189-0_42","DOI":"10.1007\/978-3-642-12189-0_42"},{"issue":"11","key":"440_CR65","doi-asserted-by":"publisher","first-page":"1234","DOI":"10.1016\/j.jsc.2010.06.006","volume":"45","author":"B Xia","year":"2010","unstructured":"Xia B, Zhang Z (2010) Termination of linear programs with nonlinear constraints. J Symb Comput 45(11):1234\u20131249. https:\/\/doi.org\/10.1016\/j.jsc.2010.06.006","journal-title":"J Symb Comput"},{"issue":"2","key":"440_CR66","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/s00165-009-0144-5","volume":"23","author":"B Xia","year":"2011","unstructured":"Xia B, Yang L, Zhan N, Zhang Z (2011) Symbolic decision procedure for termination of linear programs. Formal Aspects Comput 23(2):171\u2013190. https:\/\/doi.org\/10.1007\/s00165-009-0144-5","journal-title":"Formal Aspects Comput"},{"key":"440_CR67","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1016\/j.jsc.2012.05.005","volume":"50","author":"M Xu","year":"2013","unstructured":"Xu M, Li ZB (2013) Symbolic termination analysis of solvable loops. J Symb Comput 50:28\u201349. https:\/\/doi.org\/10.1016\/j.jsc.2012.05.005","journal-title":"J Symb Comput"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-023-00440-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-023-00440-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-023-00440-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T13:57:57Z","timestamp":1746194277000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-023-00440-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,12,4]]},"references-count":67,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2025,4]]}},"alternative-id":["440"],"URL":"https:\/\/doi.org\/10.1007\/s10703-023-00440-z","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,12,4]]},"assertion":[{"value":"16 October 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 September 2023","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 December 2023","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}