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.
Technical University of Madrid.ORCID iD: 0000-0002-4872-1208
Complutense University of Madrid.
2012 (English)In: ACM Transactions on Programming Languages and Systems, ISSN 0164-0925, E-ISSN 1558-4593, Vol. 34, no 4, -Article number 16 p.Article in journal (Refereed) Published
Abstract [en]

In this article we study the decidability of termination of several variants of simple integer loops, without branching in the loop body and with affine constraints asthe 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 Z?{r} with r an arbitrary irrational; when the loop is a sequence of instructions, that compute either linear expressions or the step function; and when the loop body is a piecewise linear deterministic update with two pieces. The undecidability result is proven by a reduction from counter programs, whose termination is known to be undecidable. For the common case of integer linear-constraint loops with rational coefficients we have not succeeded in proving either decidability or undecidability of termination, but we show that a Petri net can be simulated with such a loop; this implies some interesting lower bounds. For example, termination for a partially specified input is at least EXPSPACE-hard.

Place, publisher, year, edition, pages
ACM Press, 2012. Vol. 34, no 4, -Article number 16 p.
National Category
Engineering and Technology
Identifiers
URN: urn:nbn:se:mdh:diva-23898DOI: 10.1145/2400676.2400679ISI: 000313658500002Scopus ID: 2-s2.0-84872372082OAI: oai:DiVA.org:mdh-23898DiVA: diva2:682329
Available from: 2013-12-27 Created: 2013-12-20 Last updated: 2014-06-17Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
Masud, Abu Naser
In the same journal
ACM Transactions on Programming Languages and Systems
Engineering and Technology

Search outside of DiVA

GoogleGoogle Scholar

Altmetric score

Total: 62 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