The 2-Dimensional Constraint Loop Problem Is Decidable

Authors Quentin Guilmant , Engel Lefaucheux , Joël Ouaknine , James Worrell



PDF
Thumbnail PDF

File

LIPIcs.ICALP.2024.140.pdf
  • Filesize: 0.92 MB
  • 21 pages

Document Identifiers

Author Details

Quentin Guilmant
  • Max Planck Institute for Software Systems, Saarland Informatics Campus, Saarbrücken, Germany
Engel Lefaucheux
  • Loria, Nancy, France
Joël Ouaknine
  • Max Planck Institute for Software Systems, Saarland Informatics Campus, Saarbrücken, Germany
James Worrell
  • Department of Computer Science, University of Oxford, UK

Cite AsGet BibTex

Quentin Guilmant, Engel Lefaucheux, Joël Ouaknine, and James Worrell. The 2-Dimensional Constraint Loop Problem Is Decidable. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 140:1-140:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ICALP.2024.140

Abstract

A linear constraint loop is specified by a system of linear inequalities that define the relation between the values of the program variables before and after a single execution of the loop body. In this paper we consider the problem of determining whether such a loop terminates, i.e., whether all maximal executions are finite, regardless of how the loop is initialised and how the non-determinism in the loop body is resolved. We focus on the variant of the termination problem in which the loop variables range over ℝ. Our main result is that the termination problem is decidable over the reals in dimension 2. A more abstract formulation of our main result is that it is decidable whether a binary relation on ℝ² that is given as a conjunction of linear constraints is well-founded.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program verification
Keywords
  • Linear Constraints Loops
  • Minkowski-Weyl
  • Convex Sets
  • Asymptotic Expansions

Metrics

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

References

  1. Amir M. Ben-Amram, Jesús J. Doménech, and Samir Genaim. Multiphase-linear ranking functions and their relation to recurrent sets. In Static Analysis - 26th International Symposium, SAS 2019, Proceedings, volume 11822 of Lecture Notes in Computer Science, pages 459-480. Springer, 2019. Google Scholar
  2. Amir M. Ben-Amram and Samir Genaim. Ranking functions for linear-constraint loops. Journal of the ACM, 61(4):1-55, 2014. URL: https://doi.org/10.1145/2629488.
  3. Amir M. Ben-Amram, Samir Genaim, and Abu Naser Masud. On the termination of integer loops. ACM Transactions on Programming Languages and Systems, 34(4):1-24, 2012. URL: https://doi.org/10.1145/2400676.2400679.
  4. Marius Bozga, Radu Iosif, and Filip Konecný. Deciding conditional termination. Log. Methods Comput. Sci., 10(3), 2014. URL: https://doi.org/10.2168/LMCS-10(3:8)2014.
  5. Mark Braverman. Termination of integer linear programs. In Computer Aided Verification 2006, volume 4144 of LNCS, pages 372-385. Springer Berlin Heidelberg, 2006. URL: https://doi.org/10.1007/11817963_34.
  6. Quentin Guilmant, Engel Lefaucheux, Joël Ouaknine, and James Worrell. The 2-dimensional constraint loop problem is decidable, 2024. URL: https://arxiv.org/abs/2405.12992.
  7. Mehran Hosseini, Joël Ouaknine, and James Worrell. Termination of linear loops over the integers. In ICALP 2019, volume 132 of LIPIcs, pages 118:1-118:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Wadern/Saarbruecken, Germany, 2019. URL: https://doi.org/10.4230/LIPICS.ICALP.2019.118.
  8. Jan Leike and Matthias Heizmann. Geometric nontermination arguments. In Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, volume 10806 of Lecture Notes in Computer Science, pages 266-283. Springer, 2018. Google Scholar
  9. Naomi Lindenstrauss and Yehoshua Sagiv. Automatic termination analysis of logic programs. In Lee Naish, editor, Logic Programming, Proceedings of the Fourteenth International Conference on Logic Programming, 1997, pages 63-77. MIT Press, 1997. Google Scholar
  10. Ashish Tiwari. Termination of linear programs. In Computer Aided Verification 2004, volume 3114 of LNCS, pages 70-82. Springer Berlin Heidelberg, 2004. URL: https://doi.org/10.1007/978-3-540-27813-9_6.