2026-07-26T05:32:03Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:20283 2024-07-02T07:52:56Z ddc:004 open_access

The 2-Dimensional Constraint Loop Problem Is Decidable Guilmant, Quentin Lefaucheux, Engel Ouaknine, Joël Worrell, James Linear Constraints Loops Minkowski-Weyl Convex Sets Asymptotic Expansions 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Quentin Guilmant and Engel Lefaucheux and Joël Ouaknine and James Worrell 2024 Is Part Of LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ICALP.2024.140 urn:nbn:de:0030-drops-202831 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.140 eng https://creativecommons.org/licenses/by/4.0/legalcode