skip to main content
research-article

On the linear ranking problem for integer linear-constraint loops

Published: 23 January 2013 Publication History

Abstract

In this paper we study the complexity of the Linear Ranking problem: given a loop, described by linear constraints over a finite set of integer variables, is there a linear ranking function for this loop? While existence of such a function implies termination, this problem is not equivalent to termination. When the variables range over the rationals or reals, the Linear Ranking problem is known to be PTIME decidable. However, when they range over the integers, whether for single-path or multipath loops, the complexity of the Linear Ranking problem has not yet been determined. We show that it is coNP-complete. However, we point out some special cases of importance of PTIME complexity. We also present complete algorithms for synthesizing linear ranking functions, both for the general case and the special PTIME cases.

Supplementary Material

JPG File (r2d1_talk2.jpg)
MP4 File (r2d1_talk2.mp4)

References

[1]
E. Albert, P. Arenas, S. Genaim, G. Puebla, and D. Zanardini. Costa: Design and implementation of a cost and termination analyzer for java bytecode. In F. S. de Boer, M. M. Bonsangue, S. Graf, and W. P. de Roever, editors, Formal Methods for Components and Objects, FMCO'07, volume 5382 of LNCS, pages 113--132. Springer, 2007.
[2]
E. Albert, P. Arenas, S. Genaim, and G. Puebla. Closed-form upper bounds in static cost analysis. J. Autom. Reasoning, 46 (2): 161--203, 2011.
[3]
C. Alias, A. Darte, P. Feautrier, and L. Gonnord. Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs. In R. Cousot and M. Martel, editors, Static Analysis Symposium, SAS'10, volume 6337 of LNCS, pages 117--133. Springer, 2010.
[4]
R. Bagnara, P. M. Hill, and E. Zaffanella. An improved tight closure algorithm for integer octagonal constraints. In F. Logozzo, D. Peled, and L. D. Zuck, editors, phVerification, Model Checking, and Abstract Interpretation, VMCAI'08, volume 4905 of LNCS, pages 8--21. Springer, 2008.
[5]
R. Bagnara, P. M. Hill, and E. Zaffanella. The parma polyhedra library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program., 72 (1--2): 3--21, 2008.
[6]
R. Bagnara, F. Mesnard, A. Pescetti, and E. Zaffanella. A new look at the automatic synthesis of linear ranking functions. Inf. Comput., 215: 47--67, 2012.
[7]
A. M. Ben-Amram. Size-change termination with difference constraints. ACM Trans. Program. Lang. Syst., 30 (3), 2008.
[8]
A. M. Ben-Amram and S. Genaim. On the linear ranking problem for integer linear-constraint loops. CoRR, abs/1208.4041, 2012.
[9]
A. M. Ben-Amram, S. Genaim, and A. N. Masud. On the termination of integer loops. In V. Kuncak and A. Rybalchenko, editors, Verification, Model Checking, and Abstract Interpretation, VMCAI'12, volume 7148 of LNCS, pages 72--87. Springer, 2012.
[10]
M. Bozga, R. Iosif, and F. Konecný. Deciding conditional termination. In C. Flanagan and B. König, editors, Tools and Algorithms for the Construction and Analysis of Systems, TACAS'12, volume 7214 of LNCS, pages 252--266. Springer, 2012.
[11]
L. Bozzelli and S. Pinchinat. Verification of gap-order constraint abstractions of counter systems. In V. Kuncak and A. Rybalchenko, editors, Verification, Model Checking, and Abstract Interpretation, VMCAI'12, volume 7148 of LNCS, pages 88--103. Springer, 2012.
[12]
A. R. Bradley, Z. Manna, and H. B. Sipma. Linear ranking with reachability. In K. Etessami and S. K. Rajamani, editors, Computer Aided Verification, CAV'05, volume 3576 of LNCS, pages 491--504. Springer, 2005.
[13]
A. R. Bradley, Z. Manna, and H. B. Sipma. Termination analysis of integer linear loops. In M. Abadi and L. de Alfaro, editors, Concurrency Theory, CONCUR 2005, volume 3653 of LNCS, pages 488--502. Springer, 2005.
[14]
A. R. Bradley, Z. Manna, and H. B. Sipma. The polyranking principle. In L. Caires, G. F. Italiano, L. Monteiro, C. Palamidessi, and M. Yung, editors, International Colloquium on Automata, Languages and Programming, ICALP'05, volume 3580 of LNCS, pages 1349--1361. Springer, 2005.
[15]
A. R. Bradley, Z. Manna, and H. B. Sipma. Termination of polynomial programs. In R. Cousot, editor, Verification, Model Checking, and Abstract Interpretation, VMCAI'05, volume 3385 of LNCS, pages 113--129. Springer, 2005.
[16]
M. Braverman. Termination of integer linear programs. In T. Ball and R. B. Jones, editors, Computer Aided Verification, CAV'06, volume 4144 of LNCS, pages 372--385. Springer, 2006.
[17]
M. Bruynooghe, M. Codish, J. P. Gallagher, S. Genaim, and W. Vanhoof. Termination analysis of logic programs through combination of type-based norms. ACM Trans. Program. Lang. Syst., 29 (2), 2007.
[18]
P. J. Charles, J. M. Howe, and A. King. Integer polyhedra for program analysis. In A. V. Goldberg and Y. Zhou, editors, Algorithmic Aspects in Information and Management, AAIM'09, volume 5564 of LNCS, pages 85--99. Springer, 2009.
[19]
M. Codish, V. Lagoon, and P. J. Stuckey. Testing for termination with monotonicity constraints. In M. Gabbrielli and G. Gupta, editors, International Conference on Logic Programming, ICLP'05, volume 3668 of LNCS, pages 326--340. Springer, 2005.
[20]
M. Colón and H. Sipma. Synthesis of linear ranking functions. In T. Margaria and W. Yi, editors, Tools and Algorithms for the Construction and Analysis of Systems, TACAS'01, volume 2031 of LNCS, pages 67--81. Springer, 2001.
[21]
B. Cook, A. Podelski, and A. Rybalchenko. Termination proofs for systems code. In M. I. Schwartzbach and T. Ball, editors, Programming Language Design and Implementation, PLDI'06, pages 415--426. ACM, 2006.
[22]
B. Cook, D. Kroening, P. Rümmer, and C. M. Wintersteiger. Ranking function synthesis for bit-vector relations. In J. Esparza and R. Majumdar, editors, Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, TACAS'10, volume 6015 of LNCS, pages 236--250. Springer, 2010.
[23]
P. Cousot. Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming. In R. Cousot, editor, Verification, Model Checking, and Abstract Interpretation, VMCAI'05, volume 3385 of LNCS, pages 1--24, 2005.
[24]
A. Darte. Understanding loops: The influence of the decomposition of Karp, Miller, and Winograd. In Formal Methods and Models for Codesign, MEMOCODE'10, pages 139--148. IEEE Computer Society, 2010.
[25]
P. Feautrier. Some efficient solutions to the affine scheduling problem. I. one-dimensional time. International Journal of Parallel Programming, 21 (5): 313--347, 1992.
[26]
M. R. Garey and D. S. Johnson. Computers and Intractability. W.H. Freeman and Co., New York, 1979.
[27]
J. Giesl, R. Thiemann, P. Schneider-Kamp, and S. Falke. Automated termination proofs with aprove. In V. van Oostrom, editor, Rewriting Techniques and Applications, RTA'04, volume 3091 of LNCS, pages 210--220. Springer, 2004.
[28]
M. E. Hartmann. Cutting Planes and the Complexity of the Integer Hull. PhD thesis, School of Operations Research and Industrial Engineering, Cornell University, 1988.
[29]
W. Harvey. Computing two-dimensional integer hulls. SIAM J. Comput., 28 (6): 2285--2299, 1999.
[30]
W. Harvey and P. J. Stuckey. A unit two variable per inequality integer constraint solver for constraint logic programming. In Australasian Computer Science Conference, ACSC'97, pages 102--111, 1997.
[31]
R. M. Karp. Reducibility among combinatorial problems. In R. E. Miller and J. W. Thatcher, editors, Complexity of Computer Computations, pages 85--103. Plenum Press, New York, 1972.
[32]
R. M. Karp and C. H. Papadimitriou. On linear characterizations of combinatorial optimization problems. In Symp. on Foundations of Computer Science, FOCS'80, pages 1--9. IEEE Computer Society, 1980.
[33]
J.-L. Lassez. Querying constraints. In Symposium on Principles of Database Systems, pages 288--298. ACM Press, 1990.
[34]
C. S. Lee, N. D. Jones, and A. M. Ben-Amram. The size-change principle for program termination. In C. Hankin and D. Schmidt, editors, Symposium on Principles of Programming Languages, POPL'01, pages 81--92, 2001.
[35]
N. Lindenstrauss and Y. Sagiv. Automatic termination analysis of Prolog programs. In L. Naish, editor, International Conference on Logic Programming, ICLP'97, pages 64--77. MIT Press, 1997.
[36]
F. Mesnard and A. Serebrenik. Recurrence with affine level mappings is p-time decidable for clp(r). TPLP, 8 (1): 111--119, 2008.
[37]
A. Miné. The octagon abstract domain. Higher-Order and Symbolic Computation, 19 (1): 31--100, Mar. 2006.
[38]
A. Podelski and A. Rybalchenko. A complete method for the synthesis of linear ranking functions. In B. Steffen and G. Levi, editors, Verification, Model Checking, and Abstract Interpretation, VMCAI'04, volume 2937 of phLNCS, pages 239--251. Springer, 2004.
[39]
P. Z. Revesz. Tightened transitive closure of integer addition constraints. In V. Bulitko and J. C. Beck, editors, phSymposium on Abstraction, Reformulation, and Approximation, SARA'09, 2009.
[40]
A. Rybalchenko. phTemporal Verification with Transition Invariants. PhD thesis, Universitat des Saarlandes, 2004.
[41]
A. Schrijver. Theory of Linear and Integer Programming. John Wiley and Sons, New York, 1986.
[42]
K. Sohn and A. V. Gelder. Termination detection in logic programs using argument sizes. In D. J. Rosenkrantz, editor, Symposium on Principles of Database Systems, pages 216--226. ACM Press, 1991.
[43]
F. Spoto, F. Mesnard, and É. Payet. A termination analyzer for java bytecode based on path-length. ACM Trans. Program. Lang. Syst., 32 (3), 2010.
[44]
Éva. Tardos. A strongly polynomial algorithm to solve combinatorial linear programs. Operations Research, 34: 250--256, 1986.
[45]
A. Tiwari. Termination of linear programs. In R. Alur and D. Peled, editors, Computer Aided Verification, CAV'04, volume 3114 of LNCS, pages 387--390. Springer, 2004.

Cited By

View all
  • (2022)Data-driven loop bound learning for termination analysisProceedings of the 44th International Conference on Software Engineering10.1145/3510003.3510220(499-510)Online publication date: 21-May-2022
  • (2022)What’s Decidable About Discrete Linear Dynamical Systems?Principles of Systems Design10.1007/978-3-031-22337-2_2(21-38)Online publication date: 29-Dec-2022
  • (2022)Algebraic Model Checking for Discrete Linear Dynamical SystemsFormal Modeling and Analysis of Timed Systems10.1007/978-3-031-15839-1_1(3-15)Online publication date: 29-Aug-2022
  • Show More Cited By

Index Terms

  1. On the linear ranking problem for integer linear-constraint loops

      Recommendations

      Comments

      Information & Contributors

      Information

      Published In

      cover image ACM SIGPLAN Notices
      ACM SIGPLAN Notices  Volume 48, Issue 1
      POPL '13
      January 2013
      561 pages
      ISSN:0362-1340
      EISSN:1558-1160
      DOI:10.1145/2480359
      Issue’s Table of Contents
      • cover image ACM Conferences
        POPL '13: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
        January 2013
        586 pages
        ISBN:9781450318327
        DOI:10.1145/2429069
      Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

      Publisher

      Association for Computing Machinery

      New York, NY, United States

      Publication History

      Published: 23 January 2013
      Published in SIGPLAN Volume 48, Issue 1

      Check for updates

      Author Tags

      1. linear constraints
      2. ranking functions
      3. termination

      Qualifiers

      • Research-article

      Contributors

      Other Metrics

      Bibliometrics & Citations

      Bibliometrics

      Article Metrics

      • Downloads (Last 12 months)9
      • Downloads (Last 6 weeks)0
      Reflects downloads up to 20 Feb 2025

      Other Metrics

      Citations

      Cited By

      View all
      • (2022)Data-driven loop bound learning for termination analysisProceedings of the 44th International Conference on Software Engineering10.1145/3510003.3510220(499-510)Online publication date: 21-May-2022
      • (2022)What’s Decidable About Discrete Linear Dynamical Systems?Principles of Systems Design10.1007/978-3-031-22337-2_2(21-38)Online publication date: 29-Dec-2022
      • (2022)Algebraic Model Checking for Discrete Linear Dynamical SystemsFormal Modeling and Analysis of Timed Systems10.1007/978-3-031-15839-1_1(3-15)Online publication date: 29-Aug-2022
      • (2022)Loopster++: Termination Analysis for Multi-path Linear LoopCollaborative Computing: Networking, Applications and Worksharing10.1007/978-3-030-92635-9_28(479-497)Online publication date: 1-Jan-2022
      • (2021)Termination Analysis of Programs with Multiphase Control-FlowElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.344.2344(13-21)Online publication date: 13-Sep-2021
      • (2021)How to find the convex hull of all integer points in a polyhedron?Optimization Letters10.1007/s11590-021-01729-w16:7(2177-2189)Online publication date: 15-Apr-2021
      • (2021)ComplexityParser: An Automatic Tool for Certifying Poly-Time Complexity of Java ProgramsTheoretical Aspects of Computing – ICTAC 202110.1007/978-3-030-85315-0_20(357-365)Online publication date: 20-Aug-2021
      • (2020)Termination analysis for evolving programs: an incremental approach by reusing certified modulesProceedings of the ACM on Programming Languages10.1145/34282674:OOPSLA(1-27)Online publication date: 13-Nov-2020
      • (2020)Proving termination by k-inductionProceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering10.1145/3324884.3418929(1239-1243)Online publication date: 21-Dec-2020
      • (2019)Learning Büchi Automata and Its ApplicationsEngineering Trustworthy Software Systems10.1007/978-3-030-17601-3_2(38-98)Online publication date: 14-Apr-2019
      • Show More Cited By

      View Options

      Login options

      View options

      PDF

      View or Download as a PDF file.

      PDF

      eReader

      View online with eReader.

      eReader

      Figures

      Tables

      Media

      Share

      Share

      Share this Publication link

      Share on social media