Advertisement

On ranking functions for single-path linear-constraint loops

  • Yi LiEmail author
  • Wenyuan Wu
  • Yong Feng
STTT Regular Paper
  • 31 Downloads

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

Keywords

Software reliability Program termination Linear ranking functions Farkas’ lemma 

Notes

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

References

  1. 1.
    Alipranties, C., Border, K.: Infinite Dimensional Analysis: A Hitchhiker’s Guide. Springer, Berlin (2006)zbMATHGoogle Scholar
  2. 2.
    Bagnara, R., Mesnard, F.: Eventual linear ranking functions. In: PPDP’15, pp. 229–238. ACM, Madrid (2013)Google Scholar
  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)MathSciNetCrossRefGoogle 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)MathSciNetCrossRefGoogle 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)MathSciNetzbMATHGoogle Scholar
  7. 7.
    Boyd, S., Vandenberghe, L.: Convex Optimization. Cambridge University Press, New York (2004)CrossRefGoogle 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)Google Scholar
  11. 11.
    Colón, M., Sipma, H.: Synthesis of linear ranking functions. In: TACAS’01, vol. 2031, pp. 67–81. Springer (2001)Google Scholar
  12. 12.
    Cook, B., See, A., Zuleger, F.: Ramsey vs. lexicographic termination proving. In: TACAS’13, vol. 7795, pp. 47–61. Springer (2013)Google Scholar
  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)Google Scholar
  14. 14.
    Duistermaat, J., Kolk, J.: Multidimensional Real Analysis. Cambridge University Press, Cambridge (2004)CrossRefGoogle 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)MathSciNetCrossRefGoogle Scholar
  16. 16.
    Floudas, C., Pardalos, P.: Encyclopedia of Optimization. Springer, Berlin (2009)CrossRefGoogle 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)Google Scholar
  18. 18.
    Jing, R., Moreno Maza, M.: Computing the integer points of a polyhedron, I: algorithm. In: CASC2017, pp. 225–241. Springer (2017)Google Scholar
  19. 19.
    Korte, B., Vygen, J.: Combinatorial Optimization: Theory and Algorithms, 5th edn. Springer, Berlin (2012)CrossRefGoogle Scholar
  20. 20.
    Leike, J., Heizmann, M.: Ranking templates for linear loops. Log. Methods Comput. Sci. 11(1), 1–27 (2015)MathSciNetCrossRefGoogle Scholar
  21. 21.
    Leike, J., Heizmann, M.: Geometric nontermination arguments. In: TACAS’18, vol. 10806, pp. 266–283. Springer (2018)Google Scholar
  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)Google Scholar
  23. 23.
    Li, Y.: Witness to non-termination of linear programs. Theor. Comput. Sci. 681, 75–100 (2017)MathSciNetCrossRefGoogle 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)MathSciNetzbMATHGoogle Scholar
  25. 25.
    Ouaknine, J., Sousa Pinto, J., Worrell, J.: On termination of integer linear loops. In: SODA’15, pp. 957–69. SIAM (2015)Google Scholar
  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)Google Scholar
  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)Google Scholar
  28. 28.
    Schrijver, A.: Theory of Linear and Integer Programming. Wiley, New York (1986)zbMATHGoogle 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)Google Scholar

Copyright information

© Springer-Verlag GmbH Germany, part of Springer Nature 2019

Authors and Affiliations

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

Personalised recommendations