The 2-dimensional constraint loop problem is decidable

Conference item

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.

Authors: Guilmant, Q; Lefaucheux, E; Ouaknine, J; Worrell, J

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
• Host title: 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)
• Pages: 140:1-140:2
• Series: Leibniz International Proceedings in Informatics (LIPIcs)
• Series number: 297
• Publication date: 2024-07-02
• Acceptance date: 2024-04-14
• Event title: 51st EATCS International Colloquium on Automata, Languages, and Programming (ICALP 2024)
• Event location: Tallinn, Estonia
• Event website: https://compose.ioc.ee/icalp2024/
• Event start date: 2024-07-08
• Event end date: 2024-07-12
• DOI: 10.4230/LIPIcs.ICALP.2024.140
• EISSN: 1868-8969
• ISBN: 9783959773225
• Language: English
• Keywords: linear constraints loops; convex sets; Minkowski-Weyl; asymptotic expansions