mdh.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
On the termination of integer loops
The Tel-Aviv Academic College.
Complutense University of Madrid.
Technical University of Madrid.ORCID iD: 0000-0002-4872-1208
2012 (English)In: Lecture Notes in Computer Science, vol. 7148, Springer, 2012, Vol. 7148, 72-87 p.Chapter in book (Refereed)
Abstract [en]

In this paper we study the decidability of termination of several variants of simple integer loops, without branching in the loop body and with affine constraints as the loop guard (and possibly a precondition). We show that termination of such loops is undecidable in some cases, in particular, when the body of the loop is expressed by a set of linear inequalities where the coefficients are from ℤ∪{r} with r an arbitrary irrational; or when the loop is a sequence of instructions, that compute either linear expressions or the step function. The undecidability result is proven by a reduction from counter programs, whose termination is known to be undecidable. For the common case of integer constraints loops with rational coefficients only we have not succeeded in proving decidability nor undecidability of termination, however, this attempt led to the result that a Petri net can be simulated with such a loop, which implies some interesting lower bounds. For example, termination for a given input is at least EXPSPACE-hard.

Place, publisher, year, edition, pages
Springer, 2012. Vol. 7148, 72-87 p.
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 7148
National Category
Engineering and Technology
Identifiers
URN: urn:nbn:se:mdh:diva-23900DOI: 10.1007/978-3-642-27940-9_6ISBN: 9783642279393 (print)OAI: oai:DiVA.org:mdh-23900DiVA: diva2:682330
Note

13th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2012; Philadelphia, PA; United States; 22 January 2012 through 24 January 2012

Available from: 2013-12-27 Created: 2013-12-20 Last updated: 2014-01-09Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full text

Search in DiVA

By author/editor
Masud, Abu Naser
Engineering and Technology

Search outside of DiVA

GoogleGoogle Scholar

Altmetric score

Total: 60 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf