DROPS

Document

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

DOI: 10.4230/LIPIcs.ICALP.2019.118

Termination of Linear Loops over the Integers (Track B: Automata, Logic, Semantics, and Theory of Programming)

Authors: Mehran Hosseini, Joël Ouaknine, and James Worrell

Published in: LIPIcs, Volume 132, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)

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.

Cite as

Mehran Hosseini, Joël Ouaknine, and James Worrell. Termination of Linear Loops over the Integers (Track B: Automata, Logic, Semantics, and Theory of Programming). In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 118:1-118:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{hosseini_et_al:LIPIcs.ICALP.2019.118,
  author =	{Hosseini, Mehran and Ouaknine, Jo\"{e}l and Worrell, James},
  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 =	{Baier, Christel and Chatzigiannakis, Ioannis and Flocchini, Paola and Leonardi, Stefano},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2019.118},
  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}
}

Document

DOI: 10.4230/LIPIcs.CONCUR.2018.42

Effective Divergence Analysis for Linear Recurrence Sequences

Authors: Shaull Almagor, Brynmor Chapman, Mehran Hosseini, Joël Ouaknine, and James Worrell

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

Abstract

We study the growth behaviour of rational linear recurrence sequences. We show that for low-order sequences, divergence is decidable in polynomial time. We also exhibit a polynomial-time algorithm which takes as input a divergent rational linear recurrence sequence and computes effective fine-grained lower bounds on the growth rate of the sequence.

Cite as

Shaull Almagor, Brynmor Chapman, Mehran Hosseini, Joël Ouaknine, and James Worrell. Effective Divergence Analysis for Linear Recurrence Sequences. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 42:1-42:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{almagor_et_al:LIPIcs.CONCUR.2018.42,
  author =	{Almagor, Shaull and Chapman, Brynmor and Hosseini, Mehran and Ouaknine, Jo\"{e}l and Worrell, James},
  title =	{{Effective Divergence Analysis for Linear Recurrence Sequences}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{42:1--42:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.42},
  URN =		{urn:nbn:de:0030-drops-95802},
  doi =		{10.4230/LIPIcs.CONCUR.2018.42},
  annote =	{Keywords: Linear recurrence sequences, Divergence, Algebraic numbers, Positivity}
}

Search Results

Documents authored by Hosseini, Mehran

Termination of Linear Loops over the Integers (Track B: Automata, Logic, Semantics, and Theory of Programming)

Abstract

Cite as

Effective Divergence Analysis for Linear Recurrence Sequences

Abstract

Cite as

Thanks for your feedback!

Could not send message