On ranking functions for single-path linear-constraint loops

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, access via your institution.

References

  1. 1.

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

    Google Scholar 

  2. 2.

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

  3. 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)

    MathSciNet  MATH  Article  Google Scholar 

  4. 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. 5.

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

    MathSciNet  MATH  Article  Google Scholar 

  6. 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. 7.

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

    Google Scholar 

  8. 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. 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. 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. 11.

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

  12. 12.

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

  13. 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. 14.

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

    Google Scholar 

  15. 15.

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

    MathSciNet  MATH  Article  Google Scholar 

  16. 16.

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

    Google Scholar 

  17. 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. 18.

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

  19. 19.

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

    Google Scholar 

  20. 20.

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

    MathSciNet  MATH  Article  Google Scholar 

  21. 21.

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

  22. 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. 23.

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

    MathSciNet  MATH  Article  Google Scholar 

  24. 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. 25.

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

  26. 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. 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. 28.

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

    Google Scholar 

  29. 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. 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

Affiliations

Authors

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

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

Keywords

  • Software reliability
  • Program termination
  • Linear ranking functions
  • Farkas’ lemma