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 R. 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 R2 that is given as a conjunction of linear constraints is well-founded.
To appear at ICALP 24, LIPIcs ????, 2024. 25 pages.
PDF
© 2024 Quentin Guilmant, Engel Lefaucheux, Joël Ouaknine,
and James Worrell.