LIPIcs.ICALP.2024.140.pdf
- Filesize: 0.92 MB
- 21 pages
Document
The 2-Dimensional Constraint Loop Problem Is Decidable
Authors
Quentin Guilmant 
,
Engel Lefaucheux ,
Joël Ouaknine ,
James Worrell
-
Part of:
Volume:
51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Colloquium on Automata, Languages, and Programming (ICALP) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2024-07-02
File
Document Identifiers
Author Details
- Max Planck Institute for Software Systems, Saarland Informatics Campus, Saarbrücken, Germany
- Max Planck Institute for Software Systems, Saarland Informatics Campus, Saarbrücken, Germany
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
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)
0PDF Downloads
References
-
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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
-
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.
-
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.
- 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.