The 2-Dimensional Constraint Loop Problem is Decidable

TL;DR

This paper proves that the problem of determining whether a 2-dimensional linear constraint loop over real numbers terminates is decidable, providing a significant theoretical result in program analysis.

Contribution

It establishes the decidability of the termination problem for 2D linear constraint loops over the reals, a previously unresolved question.

Findings

Termination is decidable for 2D linear constraint loops over reals.

The problem reduces to checking well-foundedness of binary relations defined by linear constraints.

This advances understanding of program termination in higher dimensions.

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 $\mathbb{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 $\mathbb{R}^2$ that is given as a conjunction of linear constraints is well-founded.