The 2-Dimensional Constraint Loop Problem is Decidable
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866910455035854848 |
|---|---|
| author | Guilmant, Quentin Lefaucheux, Engel Ouaknine, Joël Worrell, James |
| author_facet | Guilmant, Quentin Lefaucheux, Engel Ouaknine, Joël Worrell, James |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2405_12992 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | The 2-Dimensional Constraint Loop Problem is Decidable Guilmant, Quentin Lefaucheux, Engel Ouaknine, Joël Worrell, James Logic in Computer Science 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. |
| title | The 2-Dimensional Constraint Loop Problem is Decidable |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2405.12992 |