Document Open Access Logo

Termination of Linear Loops over the Integers (Track B: Automata, Logic, Semantics, and Theory of Programming)

Authors Mehran Hosseini, Joël Ouaknine, James Worrell

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2019.118.pdf
  • Filesize: 0.49 MB
  • 13 pages

Document Identifiers

Author Details

Mehran Hosseini
  • Department of Computer Science, University of Oxford, UK
Joël Ouaknine
  • Max Planck Institute for Software Systems, Germany
  • Department of Computer Science, University of Oxford, UK
James Worrell
  • Department of Computer Science, University of Oxford, UK

Funding

  • Hosseini, Mehran: Mehran Hosseini was supported by ERC grant AVS-ISS (648701).
  • Ouaknine, Joël: Joël Ouaknine was supported by ERC grant AVS-ISS (648701) and by DFG grant 389792660 as part of TRR 248 (see https://perspicuous-computing.science).
  • Worrell, James: James Worrell was supported by EPSRC Fellowship EP/N008197/1.

Cite As Get BibTex

Mehran Hosseini, Joël Ouaknine, and James Worrell. Termination of Linear Loops over the Integers (Track B: Automata, Logic, Semantics, and Theory of Programming). In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 118:1-118:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.ICALP.2019.118

Abstract

We consider the problem of deciding termination of single-path while loops with integer variables, affine updates, and affine guard conditions. The question is whether such a loop terminates on all integer initial values. This problem is known to be decidable for the subclass of loops whose update matrices are diagonalisable, but the general case has remained open since being conjectured decidable by Tiwari in 2004. In this paper we show decidability of determining termination for arbitrary update matrices, confirming Tiwari’s conjecture. For the class of loops considered in this paper, the question of deciding termination on a specific initial value is a longstanding open problem in number theory. The key to our decision procedure is in showing how to circumvent the difficulties inherent in deciding termination on a fixed initial value.

Subject Classification

ACM Subject Classification
  • Computing methodologies → Algebraic algorithms
  • Theory of computation → Logic and verification
Keywords
  • Program Verification
  • Loop Termination
  • Linear Integer Programs
  • Affine While Loops

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Shaull Almagor, Brynmor Chapman, Mehran Hosseini, Joël Ouaknine, and James Worrell. Effective Divergence Analysis for Linear Recurrence Sequences. In 29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China, pages 42:1-42:15, 2018. Google Scholar
  2. Alexander I. Barvinok. Lattice Points and Lattice Polytopes. In Handbook of Discrete and Computational Geometry, Second Edition., pages 153-176. Chapman and Hall/CRC, 2004. Google Scholar
  3. Amir M. Ben-Amram, Jesús Doménech, and Samir Genaim. Multiphase-Linear Ranking Functions and their Relation to Recurrent Sets. CoRR, abs/1811.07340, 2018. URL: http://arxiv.org/abs/1811.07340.
  4. Amir M. Ben-Amram and Samir Genaim. On the linear ranking problem for integer linear-constraint loops. In The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, Rome, Italy - January 23 - 25, 2013, pages 51-62, 2013. Google Scholar
  5. Amir M. Ben-Amram and Samir Genaim. Ranking Functions for Linear-Constraint Loops. J. ACM, 61(4):26:1-26:55, 2014. Google Scholar
  6. Amir M. Ben-Amram and Samir Genaim. On Multiphase-Linear Ranking Functions. In Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II, pages 601-620, 2017. Google Scholar
  7. Bernard Boigelot. On iterating linear transformations over recognizable sets of integers. Theor. Comput. Sci., 309(1-3):413-468, 2003. Google Scholar
  8. Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. Termination Analysis of Integer Linear Loops. In CONCUR 2005 - Concurrency Theory, 16th International Conference, CONCUR 2005, San Francisco, CA, USA, August 23-26, 2005, Proceedings, pages 488-502, 2005. Google Scholar
  9. Mark Braverman. Termination of Integer Linear Programs. In Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, pages 372-385, 2006. Google Scholar
  10. Hong Yi Chen, Shaked Flur, and Supratik Mukhopadhyay. Termination proofs for linear simple loops. STTT, 17(1):47-57, 2015. Google Scholar
  11. Michael Colón and Henny Sipma. Synthesis of Linear Ranking Functions. In Tools and Algorithms for the Construction and Analysis of Systems, 7th International Conference, TACAS 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2-6, 2001, Proceedings, pages 67-81, 2001. Google Scholar
  12. Byron Cook, Andreas Podelski, and Andrey Rybalchenko. Termination proofs for systems code. In Proceedings of the ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation, Ottawa, Ontario, Canada, June 11-14, 2006, pages 415-426, 2006. Google Scholar
  13. Graham Everest, Alfred J. van der Poorten, Igor E. Shparlinski, and Thomas Ward. Recurrence Sequences, volume 104 of Mathematical surveys and monographs. American Mathematical Society, 2003. Google Scholar
  14. Bertrand Jeannet, Peter Schrammel, and Sriram Sankaranarayanan. Abstract acceleration of general linear loops. In The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014, pages 529-540. ACM, 2014. Google Scholar
  15. Leonid Khachiyan and Lorant Porkolab. Computing Integral Points in Convex Semi-algebraic Sets. In 38th Annual Symposium on Foundations of Computer Science, FOCS '97, Miami Beach, Florida, USA, October 19-22, 1997, pages 162-171, 1997. Google Scholar
  16. Zachary Kincaid, Jason Breck, John Cyphert, and Thomas W. Reps. Closed forms for numerical loops. PACMPL, 3(POPL):55:1-55:29, 2019. Google Scholar
  17. David W Masser. Linear relations on algebraic groups. New Advances in Transcendence Theory, pages 248-262, 1988. Google Scholar
  18. Joël Ouaknine, João Sousa Pinto, and James Worrell. On Termination of Integer Linear Loops. In Proceedings of the Twenty-Sixth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2015, San Diego, CA, USA, January 4-6, 2015, pages 957-969, 2015. Google Scholar
  19. Joël Ouaknine and James Worrell. Positivity Problems for Low-Order Linear Recurrence Sequences. In Proceedings of the Twenty-Fifth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2014, Portland, Oregon, USA, January 5-7, 2014, pages 366-379, 2014. Google Scholar
  20. Andreas Podelski and Andrey Rybalchenko. A Complete Method for the Synthesis of Linear Ranking Functions. In Verification, Model Checking, and Abstract Interpretation, 5th International Conference, VMCAI 2004, Venice, Italy, January 11-13, 2004, Proceedings, pages 239-251, 2004. Google Scholar
  21. Andreas Podelski and Andrey Rybalchenko. Transition Invariants. In 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14-17 July 2004, Turku, Finland, Proceedings, pages 32-41, 2004. Google Scholar
  22. G. Rozenberg and A. Salomaa. Cornerstones of Undecidability. Prentice Hall, 1994. Google Scholar
  23. Arto Salomaa and Matti Soittola. Automata-Theoretic Aspects of Formal Power Series. Texts and Monographs in Computer Science. Springer, 1978. Google Scholar
  24. M. Soittola. On D0L Synthesis Problem. In A. Lindenmayer and G. Rozenberg, editors, Automata, Languages, Development. North-Holland, 1976. Google Scholar
  25. Ashish Tiwari. Termination of Linear Programs. In Computer Aided Verification, 16th International Conference, CAV 2004, Boston, MA, USA, July 13-17, 2004, Proceedings, pages 70-82, 2004. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact