Document Open Access Logo

The 2-Dimensional Constraint Loop Problem Is Decidable

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

PDF

File

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

Document Identifiers

Related Versions

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
    0
    Metadata Views

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.

Cite As Get 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

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

Funding

  • Lefaucheux, Engel: ANR BisoUS (ANR-22-CE48-0012).
  • Ouaknine, Joël: Also affiliated with Keble College, Oxford as https://emmy.network Fellow, and supported by DFG grant 389792660 as part of TRR 248 (see https://perspicuous-computing.science).
  • Worrell, James: Work supported by UKRI Frontier Research Grant EP/X033813/1.

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.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact