The 2-Dimensional Constraint Loop Problem is Decidable
<|reference_start|>The 2-Dimensional Constraint Loop Problem is Decidable: 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.<|reference_end|>
@article{guilmant2024the,
    title={The 2-Dimensional Constraint Loop Problem is Decidable},
    author={Quentin Guilmant, Engel Lefaucheux, Jo"el Ouaknine, James Worrell},
    journal={arXiv preprint arXiv:2405.12992},
    year={2024},
    archivePrefix={arXiv},
    eprint={2405.12992},
    primaryClass={cs.LO}
}