{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,25]],"date-time":"2026-02-25T18:16:56Z","timestamp":1772043416955,"version":"3.50.1"},"reference-count":60,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2014,7,1]],"date-time":"2014-07-01T00:00:00Z","timestamp":1404172800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100003176","name":"Ministerio de Educaci\u00f3n, Cultura y Deporte","doi-asserted-by":"publisher","award":["TIN2008-05624, TIN2012-38137"],"award-info":[{"award-number":["TIN2008-05624, TIN2012-38137"]}],"id":[{"id":"10.13039\/501100003176","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004963","name":"Seventh Framework Programme","doi-asserted-by":"publisher","award":["FP7-ICT-610582 ENVISAGE"],"award-info":[{"award-number":["FP7-ICT-610582 ENVISAGE"]}],"id":[{"id":"10.13039\/501100004963","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2014,7]]},"abstract":"<jats:p>In this article, we study the complexity of the problems: given a loop, described by linear constraints over a finite set of variables, is there a linear or lexicographical-linear ranking function for this loop? While existence of such functions implies termination, these problems are not equivalent to termination. When the variables range over the rationals (or reals), it is known that both problems are PTIME decidable. However, when they range over the integers, whether for single-path or multipath loops, the complexity has not yet been determined. We show that both problems are coNP-complete. However, we point out some special cases of importance of PTIME complexity. We also present complete algorithms for synthesizing linear and lexicographical-linear ranking functions, both for the general case and the special PTIME cases. Moreover, in the rational setting, our algorithm for synthesizing lexicographical-linear ranking functions extends existing ones, because our definition for such functions is more general, yet it has PTIME complexity.<\/jats:p>","DOI":"10.1145\/2629488","type":"journal-article","created":{"date-parts":[[2014,8,12]],"date-time":"2014-08-12T13:53:48Z","timestamp":1407851628000},"page":"1-55","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":55,"title":["Ranking Functions for Linear-Constraint Loops"],"prefix":"10.1145","volume":"61","author":[{"given":"Amir M.","family":"Ben-Amram","sequence":"first","affiliation":[{"name":"The Academic College of Tel-Aviv Yaffo"}]},{"given":"Samir","family":"Genaim","sequence":"additional","affiliation":[{"name":"Complutense University of Madrid"}]}],"member":"320","published-online":{"date-parts":[[2014,7]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9174-1"},{"key":"e_1_2_1_2_1","volume-title":"Proceedings of the Symposium on Formal Methods for Components and Objects (FMCO\u201907)","volume":"5382","author":"Albert Elvira","year":"2007"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/1882094.1882102"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/1787526.1787532"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.08.001"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2505879.2505884"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2012.03.003"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1353445.1353450"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-7(3:4)2011"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429078"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2400676.2400679"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_18"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27940-9_7"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_48"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/11523468_109"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/11539452_37"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_8"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_34"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_28"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1216374.1216378"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02158-9_9"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/11562931_25"},{"key":"e_1_2_1_23_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201901). Tiziana Margaria and Wang Yi Eds.","author":"Col\u00f3n Michael"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/647771.734281"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_19"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134029"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_4"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_1"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2010.5558638"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01407835"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01407835"},{"key":"e_1_2_1_32_1","volume-title":"Lecture: Polyhedral Computation","author":"Fukuda Komei","year":"2013"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/2958031.2958105"},{"key":"e_1_2_1_34_1","unstructured":"Michael R. Garey and David S. Johnson. 1979. Computers and Intractability. W.H. Freeman and Co. New York.  Michael R. Garey and David S. Johnson. 1979. Computers and Intractability . W.H. Freeman and Co. New York."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-25979-4_15"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/1882094.1882113"},{"key":"e_1_2_1_37_1","unstructured":"Mark E. Hartmann. 1988. Cutting planes and the complexity of the integer hull. Ph.D. Dissertation. School of Operations Research and Industrial Engineering Cornell University.   Mark E. Hartmann. 1988. Cutting planes and the complexity of the integer hull. Ph.D. Dissertation. School of Operations Research and Industrial Engineering Cornell University."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1137\/S009753979528977X"},{"key":"e_1_2_1_39_1","volume-title":"Proceedings of the Australasian Computer Science Conference (ACSC\u201997)","author":"Harvey Warwick"},{"key":"e_1_2_1_40_1","volume-title":"Proceedings of the Automated Technology for Verification and Analysis","author":"Heizmann Matthias"},{"key":"e_1_2_1_41_1","volume-title":"Complexity of Computer Computations","author":"Karp R. M."},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1980.29"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_9"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679413"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/298514.298581"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360210"},{"key":"e_1_2_1_47_1","unstructured":"Jan Leike. 2013. Ranking function synthesis for linear lasso programs. Master\u2019s dissertation. University of Freiburg Department of Computer Science.  Jan Leike. 2013. Ranking function synthesis for linear lasso programs. Master\u2019s dissertation. University of Freiburg Department of Computer Science."},{"key":"e_1_2_1_48_1","volume-title":"Proceedings of the International Conference on Logic Programming (ICLP\u201997)","author":"Lindenstrauss Naomi","year":"1997"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706326"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068407003122"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-8609-1"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_20"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.5555\/1018438.1021840"},{"key":"e_1_2_1_54_1","volume-title":"Proceedings of the Symposium on Abstraction, Reformulation, and Approximation (SARA\u201909)","author":"Revesz Peter Z.","year":"2009"},{"key":"e_1_2_1_55_1","unstructured":"Andrey Rybalchenko. 2004. Temporal verification with transition invariants. Ph.D. Dissertation Universit\u00e4t des Saarlandes.  Andrey Rybalchenko. 2004. Temporal verification with transition invariants. Ph.D. Dissertation Universit\u00e4t des Saarlandes."},{"key":"e_1_2_1_56_1","unstructured":"Alexander Schrijver. 1986. Theory of Linear and Integer Programming. Wiley New York.   Alexander Schrijver. 1986. Theory of Linear and Integer Programming . Wiley New York."},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/113413.113433"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/1709093.1709095"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1287\/opre.34.2.250"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27813-9_6"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2629488","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2629488","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:01:17Z","timestamp":1750230077000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2629488"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,7]]},"references-count":60,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2014,7]]}},"alternative-id":["10.1145\/2629488"],"URL":"https:\/\/doi.org\/10.1145\/2629488","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,7]]},"assertion":[{"value":"2013-07-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-03-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-07-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}