DROPS

Document

Track B: Automata, Logic, Semantics, and Theory of Programming

DOI: 10.4230/LIPIcs.ICALP.2024.140

The 2-Dimensional Constraint Loop Problem Is Decidable

Authors: Quentin Guilmant, Engel Lefaucheux, Joël Ouaknine, and James Worrell

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)

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 ℝ. 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.

Cite as

Quentin Guilmant, Engel Lefaucheux, Joël Ouaknine, and James Worrell. The 2-Dimensional Constraint Loop Problem Is Decidable. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 140:1-140:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{guilmant_et_al:LIPIcs.ICALP.2024.140,
  author =	{Guilmant, Quentin and Lefaucheux, Engel and Ouaknine, Jo\"{e}l and Worrell, James},
  title =	{{The 2-Dimensional Constraint Loop Problem Is Decidable}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{140:1--140:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.140},
  URN =		{urn:nbn:de:0030-drops-202831},
  doi =		{10.4230/LIPIcs.ICALP.2024.140},
  annote =	{Keywords: Linear Constraints Loops, Minkowski-Weyl, Convex Sets, Asymptotic Expansions}
}

Search Results

Documents authored by Guilmant, Quentin

The 2-Dimensional Constraint Loop Problem Is Decidable

Abstract

Cite as

Thanks for your feedback!

Could not send message