License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ICALP.2019.118
URN: urn:nbn:de:0030-drops-106940
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/10694/
Go to the corresponding LIPIcs Volume Portal

Hosseini, Mehran ; Ouaknine, Joël ; Worrell, James

Termination of Linear Loops over the Integers

pdf-format:
LIPIcs-ICALP-2019-118.pdf (0.5 MB)

Abstract

We consider the problem of deciding termination of single-path while loops with integer variables, affine updates, and affine guard conditions. The question is whether such a loop terminates on all integer initial values. This problem is known to be decidable for the subclass of loops whose update matrices are diagonalisable, but the general case has remained open since being conjectured decidable by Tiwari in 2004. In this paper we show decidability of determining termination for arbitrary update matrices, confirming Tiwari's conjecture. For the class of loops considered in this paper, the question of deciding termination on a specific initial value is a longstanding open problem in number theory. The key to our decision procedure is in showing how to circumvent the difficulties inherent in deciding termination on a fixed initial value.

BibTeX - Entry

@InProceedings{hosseini_et_al:LIPIcs:2019:10694,
  author =	{Mehran Hosseini and Jo{\"e}l Ouaknine and James Worrell},
  title =	{{Termination of Linear Loops over the Integers}},
  booktitle =	{46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)},
  pages =	{118:1--118:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-109-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{132},
  editor =	{Christel Baier and Ioannis Chatzigiannakis and Paola Flocchini and Stefano Leonardi},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/10694},
  URN =		{urn:nbn:de:0030-drops-106940},
  doi =		{10.4230/LIPIcs.ICALP.2019.118},
  annote =	{Keywords: Program Verification, Loop Termination, Linear Integer Programs, Affine While Loops}
}

Keywords: Program Verification, Loop Termination, Linear Integer Programs, Affine While Loops
Collection: 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)
Issue Date: 2019
Date of publication: 04.07.2019

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI