Name
Abstract | ||
|---|---|---|
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 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 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. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1145/2400676.2400679 | ACM Transactions on Programming Languages and Systems |
Keywords | DocType | Volume |
linear inequality,loop guard,linear expression,undecidability result,common case,integer constraints loop,integer linear-constraint loop,loop body,simple integer loop,affine constraint,integer loops,piecewise linear deterministic update,counter program | Conference | 34 |
Issue | ISSN | Citations |
4 | 0164-0925 | 15 |
PageRank | References | Authors |
0.82 | 27 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Amir M Ben-Amram | 1 | 327 | 30.52 |
| Samir Genaim | 2 | 891 | 44.31 |
| Abu Naser Masud | 3 | 47 | 4.30 |