# Termination of Triangular Integer Loops is Decidable

## Abstract

We consider the problem whether termination of affine integer loops is decidable. Since Tiwari conjectured decidability in 2004 [15], only special cases have been solved [3, 4, 14]. We complement this work by proving decidability for the case that the update matrix is triangular.

## 1 Introduction

^{1}over \(\overline{x}\) (i.e., \(\mathbb {A}\mathbbm {f}[\overline{x}] = \{\overline{c}^T\, \overline{x} + c \mid \overline{c} \in \mathbb {Q}^d, c \in \mathbb {Q}\}\)). So \(\varphi \) has the form \(B\,\overline{x} + \overline{b} > \overline{0}\) where \(\overline{0}\) is the vector containing

*k*zeros, \(B \in \mathbb {Q}^{k \times d}\), and \(\overline{b} \in \mathbb {Q}^k\) for some \(k \in \mathbb {N}\). Definition 1 formalizes the intuitive notion of termination for such loops.

### Definition 1

**(Termination).**Let \(f:\mathbb {Z}^d \rightarrow \mathbb {Z}^d\) with \(f(\overline{x}) = A\,\overline{x} + \overline{a}\). If

*non-terminating*and \(\overline{c}\) is a

*witness*for non-termination. Otherwise, (1)

*terminates*.

Here, \(f^n\) denotes the *n*-fold application of *f*, i.e., we have \(f^0(\overline{c}) = \overline{c}\) and \(f^{n+1}(\overline{c}) = f(f^n(\overline{c}))\). We call *f* the *update* of (1). Moreover, for any entity *s*, *s*[*x* / *t*] denotes the entity that results from *s* by replacing all occurrences of *x* by *t*. Similarly, if \(\overline{x} = \begin{bmatrix}x_1\\[-.15cm]\vdots \\x_m\end{bmatrix}\) and \(\overline{t} = \begin{bmatrix}t_1\\[-.15cm]\vdots \\t_m\end{bmatrix}\), then \(s[\overline{x} / \overline{t}]\) denotes the entity resulting from *s* by replacing all occurrences of \(x_i\) by \(t_i\) for each \(1 \le i \le m\).

### Example 2

While termination of affine loops is known to be decidable if the variables range over the real [15] or the rational numbers [4], the integer case is a well-known open problem [2, 3, 4, 14, 15].^{2} However, certain special cases have been solved: Braverman [4] showed that termination of *linear* loops is decidable (i.e., loops of the form (1) where \(\overline{a}\) is \(\overline{0}\) and \(\varphi \) is of the form \(B\,\overline{x} > \overline{0}\)). Bozga et al. [3] showed decidability for the case that the update matrix *A* in (1) has the *finite monoid property*, i.e., if there is an \(n > 0\) such that \(A^n\) is diagonalizable and all eigenvalues of \(A^n\) are in \(\{0,1\}.\) Ouaknine et al. [14] proved decidability for the case \(d \le 4\) and for the case that *A* is diagonalizable.

Ben-Amram et al. [2] showed undecidability of termination for certain extensions of affine integer loops, e.g., for loops where the body is of the form \(\mathbf {if}\ x > 0\ \mathbf {then}\ \overline{x} \leftarrow A\,\overline{x}\ \mathbf {else}\ \overline{x} \leftarrow A'\,\overline{x}\) where \(A,A' \in \mathbb {Z}^{d \times d}\) and \(x \in \overline{x}\).

In this paper, we present another substantial step towards the solution of the open problem whether termination of affine integer loops is decidable. We show that termination is decidable for *triangular* loops (1) where *A* is a triangular matrix (i.e., all entries of *A* below or above the main diagonal are zero). Clearly, the order of the variables is irrelevant, i.e., our results also cover the case that *A* can be transformed into a triangular matrix by reordering *A*, \(\overline{x}\), and \(\overline{a}\) accordingly.^{3} So essentially, triangularity means that the program variables \(x_1,\ldots ,x_d\) can be ordered such that in each loop iteration, the new value of \(x_i\) only depends on the previous values of \(x_1,\ldots ,x_{i-1},x_i\). Hence, this excludes programs with “cyclic dependencies” of variables (e.g., where the new values of *x* and *y* both depend on the old values of both *x* and *y*). While triangular loops are a very restricted subclass of general integer programs, integer programs often contain such loops. Hence, tools for termination analysis of such programs (e.g., [5, 6, 7, 8, 11, 12, 13]) could benefit from integrating our decision procedure and applying it whenever a sub-program is an affine triangular loop.

Note that triangularity and diagonalizability of matrices do not imply each other. As we consider loops with arbitrary dimension, this means that the class of loops considered in this paper is not covered by [3, 14]. Since we consider affine instead of linear loops, it is also orthogonal to [4].

*A*where \(c_1,\ldots ,c_k\) are the

*distinct*entries on the diagonal is diagonalizable iff \((A - c_1 I) \ldots (A- c_k I)\) is the zero matrix.

^{4}Here,

*I*is the identity matrix. So an easy example for a triangular loop where the update matrix is not diagonalizable is the following well-known program (see, e.g., [2]):

*y*eventually becomes negative and then

*x*decreases in each iteration. In matrix notation, the loop body is Open image in new window , i.e., the update matrix is triangular. Thus, this program is in our class of programs where we show that termination is decidable. However, the only entry on the diagonal of the update matrix

*A*is \(c = 1\) and Open image in new window is not the zero matrix. So

*A*(and in fact each \(A^n\) where \(n \in \mathbb {N}\)) is not diagonalizable. Hence, extensions of this example to a dimension greater than 4 where the loop is still triangular are not covered by any of the previous results.

^{5}

Our proof that termination is decidable for triangular loops proceeds in three steps. We first prove that termination of triangular loops is decidable iff termination of *non-negative triangular* loops (*nnt-loops*) is decidable, cf. Sect. 2. A loop is non-negative if the diagonal of *A* does not contain negative entries. Second, we show how to compute *closed forms* for nnt-loops, i.e., vectors \(\overline{q}\) of *d* expressions over the variables \(\overline{x}\) and *n* such that \(\overline{q}[n/c] = f^c(\overline{x})\) for all \(c\ge 0\), see Sect. 3. Here, triangularity of the matrix *A* allows us to treat the variables step by step. So for any \(1 \le i \le d\), we already know the closed forms for \(x_1,\ldots ,x_{i-1}\) when computing the closed form for \(x_i\). The idea of computing closed forms for the repeated updates of loops was inspired by our previous work on inferring lower bounds on the runtime of integer programs [10]. But in contrast to [10], here the computation of the closed form always succeeds due to the restricted shape of the programs. Finally, we explain how to decide termination of nnt-loops by reasoning about their closed forms in Sect. 4. While our technique does not yield witnesses for non-termination, we show that it yields witnesses for *eventual* non-termination, i.e., vectors \(\overline{c}\) such that \(f^n(\overline{c})\) witnesses non-termination for some \(n \in \mathbb {N}\). Detailed proofs for all lemmas and theorems can be found in [9].

## 2 From Triangular to Non-Negative Triangular Loops

To transform triangular loops into nnt-loops, we define how to *chain* loops. Intuitively, chaining yields a new loop where a single iteration is equivalent to two iterations of the original loop. Then we show that chaining a triangular loop always yields an nnt-loop and that chaining is equivalent w.r.t. termination.

### Definition 3

**(Chaining).**

*Chaining*the loop (1) yields:

### Example 4

Lemma 5 is needed to prove that (2) is an nnt-loop if (1) is triangular.

### Lemma 5

**(Squares of Triangular Matrices).** For every triangular matrix *A*, \(A^2\) is a triangular matrix whose diagonal entries are non-negative.

### Proof

### Theorem 8

**(Reducing Termination to nnt-Loops).** Termination of triangular loops is decidable iff termination of nnt-loops is decidable.

Thus, from now on we restrict our attention to nnt-loops.

## 3 Computing Closed Forms

The next step towards our decidability proof is to show that \(f^n(\overline{x})\) is equivalent to a vector of *poly-exponential expressions* for each nnt-loop, i.e., the closed form of each nnt-loop can be represented by such expressions. Here, *equivalence* means that two expressions evaluate to the same result for all variable assignments.

Poly-exponential expressions are sums of arithmetic terms where it is always clear which addend determines the asymptotic growth of the whole expression when increasing a designated variable *n*. This is crucial for our decidability proof in Sect. 4. Let \(\mathbb {N}_{\ge 1} = \{b \in \mathbb {N}\mid b \ge 1\}\) (and \(\mathbb {Q}_{>0}\), \(\mathbb {N}_{>1}\), etc. are defined analogously). Moreover, \(\mathbb {A}\mathbbm {f}[\overline{x}]\) is again the set of all affine expressions over \(\overline{x}\).

### Definition 9

**(Poly-Exponential Expressions).**Let \(\mathcal {C}\) be the set of all finite conjunctions over the literals \(n = c, n \ne c\) where

*n*is a designated variable and \(c \in \mathbb {N}\). Moreover for each formula \(\psi \) over

*n*, let Open image in new window be the characteristic function of \(\psi \), i.e., Open image in new window if \(\psi [n/c]\) is valid and Open image in new window , otherwise. The set of all

*poly-exponential expressions*over \(\overline{x}\) is

*n*ranges over \(\mathbb {N}\), we use Open image in new window as syntactic sugar for Open image in new window . So an example for a poly-exponential expression isMoreover, note that if \(\psi \) contains a

*positive*literal (i.e., a literal of the form “\(n = c\)” for some number \(c \in \mathbb {N}\)), then Open image in new window is equivalent to either 0 or Open image in new window .

The crux of the proof that poly-exponential expressions can represent closed forms is to show that certain sums over products of exponential and poly-exponential expressions can be represented by poly-exponential expressions, cf. Lemma 12. To construct these expressions, we use a variant of [1, Lemma 3.5]. As usual, \(\mathbb {Q}[\overline{x}]\) is the set of all polynomials over \(\overline{x}\) with rational coefficients.

### Lemma 10

**(Expressing Polynomials by Differences** [1]**).** If \(q \in \mathbb {Q}[n]\) and \(c \in \mathbb {Q}\), then there is an \(r \in \mathbb {Q}[n]\) such that \(q = r - c \cdot r[n/n-1]\) for all \(n \in \mathbb {N}\).

*q*via the difference of another polynomial

*r*at the positions

*n*and \(n-1\), where the additional factor

*c*can be chosen freely. The proof of Lemma 10 is by induction on the degree of

*q*and its structure resembles the structure of the following algorithm to compute

*r*. Using the Binomial Theorem, one can verify that \(q - s + c \cdot s[n/n-1]\) has a smaller degree than

*q*, which is crucial for the proof of Lemma 10 and termination of Algorithm 1.

### Example 11

As an example, consider \(q = 1\) (i.e., \(c_0 = 1\)) and \(c = 4\). Then we search for an *r* such that \(q = r - c \cdot r[n/n-1]\), i.e., \(1 = r - 4 \cdot r[n/n-1]\). According to Algorithm 1, the solution is \(r = \frac{c_0}{1-c} = -\frac{1}{3}\).

### Lemma 12

**(Closure of** \(\mathbb {PE}\) **under Sums of Products and Exponentials).** If \(m \in \mathbb {N}\) and \(p \in \mathbb {PE}[\overline{x}]\), then one can compute a \(q \in \mathbb {PE}[\overline{x}]\) which is equivalent to \(\sum _{i=1}^{n} m^{n - i} \cdot p[n/i-1]\).

### Proof

*c*be the maximal constant that occurs in \(\psi \) or \(-1\) if \(\psi \) is empty. We get:Again, the step marked with \((\dagger )\) holds since we have Open image in new window for all \(i \in \{1,\ldots ,n\}\). The last step holds as \(i \ge c+2\) implies Open image in new window . Similar to the case where \(\psi \) contains a positive literal, we can compute a poly-exponential expression which is equivalent to the first addend. We havewhich is a poly-exponential expression as \(\tfrac{1}{m^{i}}\cdot \alpha \cdot (i-1)^a \cdot b^{i-1} \in \mathbb {A}\mathbbm {f}[\overline{x}]\). For the second addend, we have:Lemma 10 ensures \(r \in \mathbb {Q}[n]\), i.e., we have \(r = \sum _{i=0}^{d_r} m_i \cdot n^i\) for some \(d_r \in \mathbb {N}\) and \(m_i \in \mathbb {Q}\). Thus, \(r[n/c+1] \cdot \left( \frac{b}{m}\right) ^{c+1} \cdot \frac{\alpha }{b} \in \mathbb {A}\mathbbm {f}[\overline{x}]\) which implies Open image in new window . It remains to show that the addend Open image in new window is equivalent to a poly-exponential expression. As \(\frac{\alpha }{b} \cdot m_i \in \mathbb {A}\mathbbm {f}[\overline{x}]\), we have \(\square \)

### Example 13

*w*is a variable. (It will later on be needed to compute a closed form for Example 4, see Example 18.) According to Algorithm 2 and (3), we getwith Open image in new window , Open image in new window , and \(p_3 = \sum _{i=1}^{n} 4^{n-i} \cdot (- 2)\). We search for \(q_1, q_2, q_3 \in \mathbb {PE}[w]\) that are equivalent to \(p_1, p_2, p_3\), i.e., \(q_1 + q_2 + q_3\) is equivalent to (12). We only show how to compute \(q_2\)(and omit the computation of Open image in new window ). Analogously to (8), we get:The next step is to rearrange the first sum as in (9). In our example, it directly simplifies to 0 and hence we obtainFinally, by applying the steps from (10) we get:The step marked with \((\dagger )\) holds by Lemma 10 with \(q = 1\) and \(c = 4\). Thus, we have \(r = -\tfrac{1}{3}\), cf. Example 11.

*n*-fold update function \(h(n,\overline{x}) = f^n(\overline{x})\) of (1) where

*f*is the update of (1), we consider a recursive update function for a single variable \(x \in \overline{x}\):

*g*can be represented by a poly-exponential expression.

### Lemma 14

**(Closed Form for Single Variables).**If \(x \in \overline{x}\), \(m \in \mathbb {N}\), and \(p \in \mathbb {PE}[\overline{x}]\), then one can compute a \(\,q \in \mathbb {PE}[\overline{x}]\) which satisfies

### Proof

### Example 15

*w*and

*x*from Example 4. We first consider the assignment \(w \leftarrow 2\), i.e., we want to compute a \(q_w \in \mathbb {PE}[w,x,y,z]\) with \(q_w [n/0] = w\) and \(q_w = (m_w \cdot q_w + p_w)\,[n/n-1]\) for \(n > 0\), where \(m_w = 0\) and \(p_w = 2\). According to (13) and (14), \(q_w\) isFor the assignment \(x \leftarrow x + 2\), we search for a \(q_x\) such that \(q_x[n/0] = x\) and \(q_x = (m_x \cdot q_x + p_x)\,[n/n-1]\) for \(n > 0\), where \(m_x = 1\) and \(p_x = 2\). By (13), \(q_x\) is

*A*, \(A_{i}\) is

*A*’s \(i^{th}\) row and \(A_{i_1,\ldots ,i_n;j_1,\ldots ,j_k}\) is the matrix with rows \((A_{i_1})_{j_1,\ldots ,j_k}, \ldots , (A_{i_n})_{j_1,\ldots ,j_k}\). So for \(A = \begin{bmatrix} a_{1,1}&a_{1,2}&a_{1,3}\\ a_{2,1}&a_{2,2}&a_{2,3}\\ a_{3,1}&a_{3,2}&a_{3,3} \end{bmatrix}\), we have \(A_{1,2;1,3} = \begin{bmatrix} a_{1,1}&a_{1,3}\\ a_{2,1}&a_{2,3} \end{bmatrix}\).

### Lemma 16

**(Closed Forms for Vectors of Variables).**If \(\overline{x}\) is a vector of at least \(d \ge 1\) pairwise different variables, \(A \in \mathbb {Z}^{d \times d}\) is triangular with \(A_{i;i} \ge 0\) for all \(1 \le i \le d\), and \(\overline{p} \in \mathbb {PE}[\overline{x}]^d\), then one can compute \(\overline{q} \in \mathbb {PE}[\overline{x}]^d\) such that:

### Proof

*A*is lower triangular (the case that

*A*is upper triangular works analogously). We use induction on

*d*. For any \(d \ge 1\) we have:

*A*is lower triangular. By Lemma 14, we can compute a \(\overline{q}_1 \in \mathbb {PE}[\overline{x}]\) that satisfies

*j*with \(1 < j \le d\). In the induction step (\(d > 1\)), it remains to show that we can compute \(\overline{q}_{2,\ldots ,d}\) such that

*A*, \(\overline{q}_1\), and the current value of \(\overline{p}\) as in the proof of Lemma 16, and then determines the closed form for \(\overline{x}_{2, \ldots , d}\) recursively.

We can now prove the main theorem of this section.

### Theorem 17

**(Closed Forms for nnt-Loops).** One can compute a closed form for every nnt-loop. In other words, if \(f:\mathbb {Z}^d \rightarrow \mathbb {Z}^d\) is the update function of an nnt-loop with the variables \(\overline{x}\), then one can compute a \(\overline{q} \in \mathbb {PE}[\overline{x}]^d\) such that \(\overline{q}[n/c] = f^c(\overline{x})\) for all \(c \in \mathbb {N}\).

### Proof

So invoking Algorithm 3 on \(\overline{x}, A\), and \(\overline{a}\) yields the closed form of an nnt-loop (1).

## 4 Deciding Non-Termination of nnt-Loops

Our proof uses the notion of *eventual non-termination* [4, 14]. Here, the idea is to disregard the condition of the loop during a finite prefix of the program run.

### Definition 19

Clearly, (1) is non-terminating iff (1) is eventually non-terminating [14]. Now Theorem 17 gives rise to an alternative characterization of eventual non-termination in terms of the closed form \(\overline{q}\) instead of \(f^{n}(\overline{c})\).

### Corollary 20

**(Expressing Non-Termination with**\(\mathbb {PE}\)

**).**If \(\overline{q}\) is the closed form of (1), then \(\overline{c} \in \mathbb {Z}^d\) witnesses eventual non-termination iff

### Proof

Immediate, as \(\overline{q}\) is equivalent to \(f^n(\overline{x})\). \(\square \)

So to prove that termination of nnt-loops is decidable, we will use Corollary 20 to show that the existence of a witness for eventual non-termination is decidable. To do so, we first eliminate the factors Open image in new window from the closed form \(\overline{q}\). Assume that \(\overline{q}\) has at least one factor Open image in new window where \(\psi \) is non-empty (otherwise, all factors Open image in new window are equivalent to 1) and let *c* be the maximal constant that occurs in such a factor. Then all addends Open image in new window where \(\psi \) contains a positive literal become 0 and all other addends become \(\alpha \cdot n^{a} \cdot b^n\) if \(n > c\). Thus, as we can assume \(n_0 > c\) in (18) without loss of generality, all factors Open image in new window can be eliminated when checking eventual non-termination.

### Corollary 21

**Removing**Open image in new window

**from**\(\mathbb {PE}\)

**s).**Let \(\overline{q}\) be the closed form of an nnt-loop (1). Let \(\overline{q}_{norm}\) result from \(\overline{q}\) by removing all addends Open image in new window where \(\psi \) contains a positive literal and by replacing all addends Open image in new window where \(\psi \) does not contain a positive literal by \(\alpha \cdot n^{a} \cdot b^n\). Then \(\overline{c} \in \mathbb {Z}^d\) is a witness for eventual non-termination iff

By removing the factors Open image in new window from the closed form \(\overline{q}\) of an nnt-loop, we obtain *normalized* poly-exponential expressions.

### Definition 22

**(Normalized**\(\mathbb {PE}\)

**s).**We call \(p \in \mathbb {PE}[\overline{x}]\)

*normalized*if it is inW.l.o.g., we always assume \((b_i,a_i) \ne (b_j,a_j)\) for all \(i,j \in \{1,\ldots ,\ell \}\) with \(i \ne j\). We define \(\mathbb {NPE}= \mathbb {NPE}[\varnothing ]\), i.e., we have \(p \in \mathbb {NPE}\) if \(\alpha _j \in \mathbb {Q}\) for all \(1 \le j \le \ell \).

### Example 23

Recall that the loop condition \(\varphi \) is a conjunction of inequalities of the form \(\alpha > 0\) where \(\alpha \in \mathbb {A}\mathbbm {f}[\overline{x}]\). Thus, \(\varphi [\overline{x} / \overline{q}_{norm}]\) is a conjunction of inequalities \(p > 0\) where \(p \in \mathbb {NPE}[\overline{x}]\) and we need to decide if there is an instantiation of these inequalities that is valid “for large enough *n*”. To do so, we order the coefficients \(\alpha _j\) of the addends \(\alpha _j \cdot n^{a_j} \cdot b_j^n\) of normalized poly-exponential expressions according to the addend’s asymptotic growth when increasing *n*. Lemma 24 shows that \(\alpha _2 \cdot n^{a_2} \cdot b_2^n\) grows faster than \(\alpha _1 \cdot n^{a_1} \cdot b_1^n\) iff \(b_2 > b_1\) or both \(b_2 = b_1\) and \(a_2 > a_1\).

### Lemma 24

**(Asymptotic Growth).** Let \(b_1,b_2 \in \mathbb {N}_{\ge 1}\) and \(a_1, a_2 \in \mathbb {N}\). If \((b_2, a_2) >_{lex} (b_1, a_1)\), then \(\mathcal {O}(n^{a_1} \cdot b_1^n) \subsetneq \mathcal {O}(n^{a_2} \cdot b_2^n)\). Here, \({>_{lex}}\) is the lexicographic order, i.e., \((b_2,a_2) >_{lex} (b_1,a_1)\) iff \(b_2 > b_1\) or \(b_2 = b_1 \wedge a_2 > a_1\).

### Proof

By considering the cases \(b_2 > b_1\) and \(b_2 = b_1\) separately, the claim can easily be deduced from the definition of \(\mathcal {O}\). \(\square \)

### Definition 25

**(Ordering Coefficients).**

*Marked coefficients*are of the form \(\alpha ^{(b,a)}\) where \(\alpha \in \mathbb {A}\mathbbm {f}[\overline{x}], b \in \mathbb {N}_{\ge 1}\), and \(a \in \mathbb {N}\). We define \(\mathrm{unmark}(\alpha ^{(b,a)}) = \alpha \) and \(\alpha _2^{(b_2,a_2)} \succ \alpha _1^{(b_1,a_1)}\) if \((b_2,a_2) >_{lex} (b_1,a_1)\). Let

*p*are

### Example 26

Now it is easy to see that the asymptotic growth of a normalized poly-exponential expression is solely determined by its \(\succ \)-maximal addend.

### Corollary 27

**(Maximal Addend Determines Asymptotic Growth).** Let \(p \in \mathbb {NPE}\) and let \(\max _{\succ }(\mathrm{coeffs}(p)) = c^{(b,a)}\). Then \(\mathcal {O}(p) = \mathcal {O}(c \cdot n^a \cdot b^n)\).

### Proof

Clear, as \(c \cdot n^a \cdot b^n\) is the asymptotically dominating addend of *p*. \(\square \)

Note that Corollary 27 would be incorrect for the case \(c = 0\) if we replaced \(\mathcal {O}(p) = \mathcal {O}(c \cdot n^a \cdot b^n)\) with \(\mathcal {O}(p) = \mathcal {O}(n^a \cdot b^n)\) as \(\mathcal {O}(0) \ne \mathcal {O}(1)\). Building upon Corollary 27, we now show that, for large *n*, the sign of a normalized poly-exponential expression is solely determined by its \(\succ \)-maximal coefficient. Here, we define \(\mathrm{sign}(c) = -1\) if \(c \in \mathbb {Q}_{<0} \cup \{-\infty \}\), \(\mathrm{sign}(0) = 0\), and \(\mathrm{sign}(c) = 1\) if \(c \in \mathbb {Q}_{>0} \cup \{\infty \}\).

### Lemma 28

**(Sign of**\(\mathbb {NPE}\)

**s).**Let \(p \in \mathbb {NPE}\). Then \(\lim _{n \mapsto \infty } p \in \mathbb {Q}\) iff \(p \in \mathbb {Q}\) and otherwise, \(\lim _{n \mapsto \infty } p \in \{ \infty , -\infty \}\). Moreover, we have

### Proof

If \(p \notin \mathbb {Q}\), then the limit of each addend of *p* is in \(\{-\infty , \infty \}\) by definition of \(\mathbb {NPE}\). As the asymptotically dominating addend determines \(\lim _{n \mapsto \infty } p\) and \(\mathrm{unmark}(\max _{\succ }(\mathrm{coeffs}(p)))\) determines the sign of the asymptotically dominating addend, the claim follows. \(\square \)

Lemma 29 shows the connection between the limit of a normalized poly-exponential expression *p* and the question whether *p* is positive for large enough *n*. The latter corresponds to the existence of a witness for eventual non-termination by Corollary 21 as \(\varphi [\overline{x} / \overline{q}_{norm}]\) is a conjunction of inequalities \(p > 0\) where \(p \in \mathbb {NPE}[\overline{x}]\).

### Lemma 29

**(Limits and Positivity of**\(\mathbb {NPE}\)

**s).**Let \(p \in \mathbb {NPE}\). Then

### Proof

By case analysis over \(\lim _{n \mapsto \infty } p\). \(\square \)

Now we show that Corollary 21 allows us to decide eventual non-termination by examining the coefficients of normalized poly-exponential expressions. As these coefficients are in \(\mathbb {A}\mathbbm {f}[\overline{x}]\), the required reasoning is decidable.

### Lemma 30

**(Deciding Eventual Positiveness of**\(\mathbb {NPE}\)

**s).**Validity of

### Proof

Note that (22) is valid iff \(\bigwedge _{i=1}^k \mathrm{max\_coeff\_pos}(p_i)\) is satisfiable. So to implement our decision procedure, one can use integer programming or SMT solvers to check satisfiability of \(\bigwedge _{i=1}^k \mathrm{max\_coeff\_pos}(p_i)\). Lemma 30 allows us to prove our main theorem.

### Theorem 31

Termination of triangular loops is decidable.

### Proof

### Example 32

is satisfiable. This formula is equivalent to \(6 \cdot y - 2 + 3 \cdot w = 0\) which does not have any integer solutions. Hence, the loop of Example 2 terminates.

Example 33 shows that our technique does not yield witnesses for non-termination, but it only proves the existence of a witness for *eventual* non-termination. While such a witness can be transformed into a witness for non-termination by applying the loop several times, it is unclear how often the loop needs to be applied.

### Example 33

*x*is Open image in new window . Replacing

*x*with \(q_{norm}\) in \(x > 0\) yields \(x + y + n - 1 > 0\). The maximal marked coefficient of \(x + y + n - 1\) is \(1^{(1,1)}\). So by Algorithm 4, (23) does not terminate if \(\exists x,y \in \mathbb {Z}.\ 1 > 0\) is valid. While \(1 > 0\) is a tautology, (23) terminates if \(x \le 0\) or \(x \le -y\).

However, the final formula constructed by Algorithm 4 precisely describes all witnesses for eventual non-termination.

### Lemma 34

**(Witnessing Eventual Non-Termination).**Let (1) be a triangular loop, let \(\overline{q}_{norm}\) be the normalized closed form of (2), and let

## 5 Conclusion

We presented a decision procedure for termination of affine integer loops with triangular update matrices. In this way, we contribute to the ongoing challenge of proving the 15 years old conjecture by Tiwari [15] that termination of affine integer loops is decidable. After linear loops [4], loops with at most 4 variables [14], and loops with diagonalizable update matrices [3, 14], triangular loops are the fourth important special case where decidability could be proven.

The key idea of our decision procedure is to compute *closed forms* for the values of the program variables after a symbolic number of iterations *n*. While these closed forms are rather complex, it turns out that reasoning about first-order formulas over the theory of linear integer arithmetic suffices to analyze their behavior for large *n*. This allows us to reduce (non-)termination of triangular loops to integer programming. In future work, we plan to investigate generalizations of our approach to other classes of integer loops.

## Footnotes

- 1.
Note that multiplying with the least common multiple of all denominators yields an equivalent constraint with integer coefficients, i.e., allowing rational instead of integer coefficients does not extend the considered class of loops.

- 2.
- 3.
Similarly, one could of course also use other termination-preserving pre-processings and try to transform a given program into a triangular loop.

- 4.
The reason is that in this case, \((x - c_1) \ldots (x- c_k)\) is the minimal polynomial of

*A*and diagonalizability is equivalent to the fact that the minimal polynomial is a product of distinct linear factors. - 5.
For instance, consider Open image in new window .

## References

- 1.Bagnara, R., Zaccagnini, A., Zolo, T.: The Automatic Solution of Recurrence Relations. I. Linear Recurrences of Finite Order with Constant Coefficients. Technical report. Quaderno 334. Dipartimento di Matematica, Università di Parma, Italy (2003). http://www.cs.unipr.it/Publications/
- 2.Ben-Amram, A.M., Genaim, S., Masud, A.N.: On the termination of integer loops. ACM Trans. Programm. Lang. Syst.
**34**(4), 16:1–16:24 (2012). https://doi.org/10.1145/2400676.2400679CrossRefzbMATHGoogle Scholar - 3.Bozga, M., Iosif, R., Konecný, F.: Deciding conditional termination. Logical Methods Comput. Sci.
**10**(3) (2014). https://doi.org/10.2168/LMCS-10(3:8)2014 - 4.Braverman, M.: Termination of integer linear programs. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 372–385. Springer, Heidelberg (2006). https://doi.org/10.1007/11817963_34CrossRefGoogle Scholar
- 5.Brockschmidt, M., Cook, B., Ishtiaq, S., Khlaaf, H., Piterman, N.: T2: temporal property verification. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 387–393. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49674-9_22CrossRefGoogle Scholar
- 6.Chen, Y.-F., et al.: Advanced automata-based algorithms for program termination checking. In: Foster, J.S., Grossman, D. (eds.) PLDI 2018, pp. 135–150 (2018). https://doi.org/10.1145/3192366.3192405
- 7.Chen, H.-Y., David, C., Kroening, D., Schrammel, P., Wachter, B.: Bit-precise procedure-modular termination analysis. ACM Trans. Programm. Lang. Syst.
**40**(1), 1:1–1:38 (2018). https://doi.org/10.1145/3121136CrossRefGoogle Scholar - 8.D’Silva, V., Urban, C.: Conflict-driven conditional termination. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 271–286. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21668-3_16CrossRefGoogle Scholar
- 9.Frohn, F., Giesl, J.: Termination of triangular integer loops is decidable. In: CoRR abs/1905.08664 (2019). https://arxiv.org/abs/1905.08664
- 10.Frohn, F., Naaf, M., Hensel, J., Brockschmidt, M., Giesl, J.: Lower runtime bounds for integer programs. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 550–567. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40229-1_37CrossRefGoogle Scholar
- 11.Giesl, J., et al.: Analyzing program termination and complexity automatically with AProVE. J. Autom. Reasoning
**58**(1), 3–31 (2017). https://doi.org/10.1007/s10817-016-9388-yMathSciNetCrossRefzbMATHGoogle Scholar - 12.Larraz, D., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A.: Proving termination of imperative programs using Max-SMT. In: Jobstmann, B., Ray, S. (eds.) FMCAD 2013, pp. 218–225 (2013). https://doi.org/10.1109/FMCAD.2013.6679413
- 13.Le, T.C., Qin, S., Chin, W.-N.: Termination and non-termination specification inference. In: Grove, D., Blackburn, S. (eds.) PLDI 2015, pp. 489–498 (2015). https://doi.org/10.1145/2737924.2737993
- 14.Ouaknine, J., Pinto, J.S., Worrell, J.: On termination of integer linear loops. In: Indyk, P. (ed.) SODA 2015, pp. 957–969 (2015). https://doi.org/10.1137/1.9781611973730.65
- 15.Tiwari, A.: Termination of linear programs. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 70–82. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-27813-9_6CrossRefGoogle Scholar

## Copyright information

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.