Skip to main content
SpringerLink
Log in

On ranking functions for single-path linear-constraint loops

  • General
  • Regular Paper
  • Published:
International Journal on Software Tools for Technology Transfer Aims and scope Submit manuscript

Abstract

Program termination is a fundamental research topic in program analysis. In this paper, we present a new complete polynomial-time method for the existence problem of linear ranking functions for single-path loops described by a conjunction of linear constraints, when variables range over the reals (or rationals). Unlike existing methods, our method does not depend on Farkas’ Lemma and provides us with counterexamples to existence of linear ranking functions, when no linear ranking function exists. In addition, we extend our results established over the rationals to the setting of the integers. This deduces an alternative approach to deciding whether or not a given SLC loop has a linear ranking function over the integers. Finally, we prove that the termination of bounded single-path linear-constraint loops is decidable over the reals (or rationals).

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Alipranties, C., Border, K.: Infinite Dimensional Analysis: A Hitchhiker’s Guide. Springer, Berlin (2006)

    MATH  Google Scholar 

  2. Bagnara, R., Mesnard, F.: Eventual linear ranking functions. In: PPDP’15, pp. 229–238. ACM, Madrid (2013)

  3. Bagnara, R., Mesnard, F., Pescetti, A., Zaffanella, E.: A new look at the automatic synthesis of linear ranking functions. Inf. Comput. 215, 47–67 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  4. Ben-Amram, A., Genaim, S.: On multiphase-linear ranking functions. In: Majumdar, R., Kunčak, V. (eds.) CAV’17, vol. 10427, pp. 601–620. Springer, Berlin (2017)

    Google Scholar 

  5. Ben-Amram, A., Genaim, S.: Ranking functions for linear-constraint loops. J. ACM 61(4), 1–55 (2014)

    Article  MathSciNet  MATH  Google Scholar 

  6. Borwein, J., Moors, W.: Stability of closedness of convex cones under linear mappings. J. Conv. Anal. 16(2–4), 699–705 (2009)

    MathSciNet  MATH  Google Scholar 

  7. Boyd, S., Vandenberghe, L.: Convex Optimization. Cambridge University Press, New York (2004)

    Book  MATH  Google Scholar 

  8. Bradley, A., Manna, Z., Sipma, H.: Linear ranking with reachability. In: Etessami, K., Rajamani, S. (eds.) CAV’05, vol. 3576, pp. 491–504. Springer, Berlin (2005)

    Google Scholar 

  9. Braverman, M.: Termination of integer linear programs. In: Ball, T., Jones, R. (eds.) CAV’06, vol. 4144, pp. 372–385. Springer, Berlin (2006)

    Google Scholar 

  10. Chen, Y., Xia, B., Yang, L., Zhan, N., Zhou, C.: Discovering non-linear ranking functions by solving semi-algebraic systems. In: ICTAC’07, vol. 4711, pp. 34–49. Springer (2007)

  11. Colón, M., Sipma, H.: Synthesis of linear ranking functions. In: TACAS’01, vol. 2031, pp. 67–81. Springer (2001)

  12. Cook, B., See, A., Zuleger, F.: Ramsey vs. lexicographic termination proving. In: TACAS’13, vol. 7795, pp. 47–61. Springer (2013)

  13. Cousot, P.: Proving program invariance and termination by parametric abstraction, In: Lagrangian Relaxation and Semidefinite Programming. VMCAI’05, vol. 3385, pp. 1–24. Springer (2005)

  14. Duistermaat, J., Kolk, J.: Multidimensional Real Analysis. Cambridge University Press, Cambridge (2004)

    Book  MATH  Google Scholar 

  15. Feautrier, P.: Some efficient solutions to the affine scheduling problem. I. One-dimensional timed. Int. J. Paral. Prog. 21(5), 313–347 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  16. Floudas, C., Pardalos, P.: Encyclopedia of Optimization. Springer, Berlin (2009)

    Book  MATH  Google Scholar 

  17. Heizmann, M., Hoenicke, J., Leike, J., Podelski, A.: Linear ranking for linear lasso programs. In: ATVA’13, vol. 8172, pp. 365–380. Springer (2013)

  18. Jing, R., Moreno Maza, M.: Computing the integer points of a polyhedron, I: algorithm. In: CASC2017, pp. 225–241. Springer (2017)

  19. Korte, B., Vygen, J.: Combinatorial Optimization: Theory and Algorithms, 5th edn. Springer, Berlin (2012)

    Book  MATH  Google Scholar 

  20. Leike, J., Heizmann, M.: Ranking templates for linear loops. Log. Methods Comput. Sci. 11(1), 1–27 (2015)

    Article  MathSciNet  MATH  Google Scholar 

  21. Leike, J., Heizmann, M.: Geometric nontermination arguments. In: TACAS’18, vol. 10806, pp. 266–283. Springer (2018)

  22. Li, Y., Zhu, G., Feng, Y.: The L-depth eventual linear ranking functions for single-path linear constraints loops. In: TASE’16, pp. 30–37. IEEE (2016)

  23. Li, Y.: Witness to non-termination of linear programs. Theor. Comput. Sci. 681, 75–100 (2017)

    Article  MathSciNet  MATH  Google Scholar 

  24. Liu, J., Xu, M., Zhan, N.J., Zhao, H.J.: Discovering non-terminating inputs for multi-path polynomial programs. J. Syst. Sci. Complex. 27, 1284–1304 (2014)

    MathSciNet  MATH  Google Scholar 

  25. Ouaknine, J., Sousa Pinto, J., Worrell, J.: On termination of integer linear loops. In: SODA’15, pp. 957–69. SIAM (2015)

  26. Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: VMCAI’04, vol. 2937, pp. 239–251. Springer (2004)

  27. Rebiha,R., Matringe, N., Moura,A.: Generating asymptotically non-terminant initial variable values for linear diagonalizable programs. In: Symbolic Computation in Software Science, SCSS’13, pp. 81–92 (2013)

  28. Schrijver, A.: Theory of Linear and Integer Programming. Wiley, New York (1986)

    MATH  Google Scholar 

  29. Sohn, K., Gelder, A.: Termination detection in logic programs using argument sizes. In: Rosenkrantz, D.J. (ed.) Proceedings of the Symposium on Principles of Database Systems, pp. 216–226. ACM, New York (1991)

    Google Scholar 

  30. Tiwari, A.: Termination of linear programs. In: CAV’04, pp. 70–82. Springer (2004)

Download references

Acknowledgements

The authors would like to thank the two anonymous reviewers for their helpful comments and suggestions. This research is partially supported by the National Natural Science Foundation of China NNSFC (61572024, 61103110) and the Natural Science Foundation of Chongqing (cstc2019jcyj-msxmX0638).

Author information

Authors and Affiliations

  1. Chongqing Institute of Green and Intelligent Technology, Chinese Academy of Sciences, Chongqing, China

    Yi Li, Wenyuan Wu & Yong Feng

Authors
  1. Yi Li
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Wenyuan Wu
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Yong Feng
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Yi Li.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Li, Y., Wu, W. & Feng, Y. On ranking functions for single-path linear-constraint loops. Int J Softw Tools Technol Transfer 22, 655–666 (2020). https://doi.org/10.1007/s10009-019-00549-9

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10009-019-00549-9

Keywords

Search

Navigation