<figure><img src="image_1.png" /></figure>

HAL
open science

# Deciding Conditional Termination

Marius Bozga, Radu Iosif, Filip Konečny

► To cite this version:

Marius Bozga, Radu Iosif, Filip Konečny. Deciding Conditional Termination. 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012), Mar 2012, Tallinn, Estonia. pp.252-266, 10.1007/978-3-642-28756-5_18 . hal-01418906

HAL Id: hal-01418906

https://hal.science/hal-01418906

Submitted on 17 Dec 2016

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

Public Domain
# Deciding Conditional Termination*

Marius Bozga¹, Radu Iosif¹, and Filip Konečný¹,²

¹ VERIMAG, CNRS, 2 av. de Vignate, 38610 Gières, France
{bozga,iosif}@imag.fr

² FIT BUT, IT4Innovations Centre of Excellence, Czech Republic
ikonecny@fit.vutbr.cz

**Abstract.** This paper addresses the problem of conditional termination, which is that of defining the set of initial configurations from which a given program terminates. First we define the dual set, of initial configurations, from which a non-terminating execution exists, as the greatest fixpoint of the pre-image of the transition relation. This definition enables the representation of this set, whenever the closed form of the relation of the loop is definable in a logic that has quantifier elimination. This entails the decidability of the termination problem for such loops. Second, we present effective ways to compute the weakest precondition for non-termination for difference bounds and octagonal (non-deterministic) relations, by avoiding complex quantifier eliminations. We also investigate the existence of linear ranking functions for such loops. Finally, we study the class of linear affine relations and give a method of under-approximating the termination precondition for a non-trivial subclass of affine relations. We have performed preliminary experiments on transition systems modeling real-life systems, and have obtained encouraging results.

## 1 Introduction

The termination problem asks whether every computation of a given program ends in a halting state. The universal termination asks whether a given program stops for every possible input configuration. Both problems are among the first ever to be shown undecidable, by A. Turing [24]. In many cases however, programs will terminate when started in certain configurations, and may<fnref n="3" /> run forever, when started in other configurations. The problem of determining the set of configurations from which a program terminates on all paths is called *conditional termination*.

In program analysis, the presence of non-terminating runs has been traditionally considered faulty. However, more recently, with the advent of *reactive systems*, accidental termination can be an equally serious error. For instance, when designing a web

<footnote>* This work was supported by the French National Project ANR-09-SEGI-016 VERIDYC, by the Czech Science Foundation (projects P103/10/0306 and 102/09/H042), the Czech Ministry of Education (projects COST OC10009 and MSM 0021630528), the Barrande project MEB021023, and the EU/Czech IT4Innovations Centre of Excellence CZ.1.05/1.1.00/02.0070.</footnote>

<footnote n="3">³ If the program is non-deterministic, the existence of a single infinite run, among other finite runs, suffices to consider an initial configuration non-terminating.</footnote>
server, a developer would like to make sure that the main program loop will not exit unless a stopping request has been issued. These facts lead us to considering the *conditional non-termination* problem, which is determining the set of initial configurations which guarantee that the program will not exit.

In this paper we focus on programs that handle integer variables, performing linear arithmetic tests and (possibly non-deterministic) updates. A first observation is that the set of configurations guaranteeing non-termination is the greatest fixpoint of the pre-image of the program’s transition relation<fnref n="4" /> *R*. This set, called the *weakest recurrent set*, and denoted *wrs(*R*)* in our paper, can be defined in first-order arithmetic, provided that the closed form of the infinite sequence of relations {*R*<sup>*i*</sup>}<sub>*i*≥0</sub>, obtained by composing the transition relation with itself 0, 1, 2, ... times, can also be defined using first-order arithmetic. Moreover, if the fragment of arithmetic we use has quantifier elimination, the weakest recurrent set can be expressed in a quantifier-free decidable fragment of arithmetic. This also means that the problem *wrs(*R*)* ⇙ ∅ is decidable, yielding universal termination decidability proofs for free.

**Contributions of this paper** The main novelty in this paper is of rather theoretical na-
ture: we show that the non-termination preconditions for integer transition relations de-
fined as either *octagons* or *linear affine loops with finite monoid property* are definable
in quantifier-free Presburger arithmetic. Thus, the universal termination problem for
such program loops is decidable. However, since quantifier elimination in Presburger
arithmetic is a complex procedure, we have developed alternative ways of deriving the
preconditions for non-termination, and in particular:

- for *octagonal relations*, we use a result from [5], namely that the sequence {*R*<sup>*i*</sup>}<sub>*i*≥0</sub> is, in some sense, periodic. We give here a simple quantifier elimination method, targeted for the class of formulae defining weakest recursive sets. The algorithm suggested here runs in worst-case time complexity of *O*(n<sup>4</sup>) in the number of variables *n*. Moreover, we investigate the existence of linear ranking functions, and prove that, for each well-founded octagonal relations, there exists an effectively computable witness relation i.e., a well-founded relation that has a linear ranking function.

- for *linear affine relations*, weakest recurrent sets can be defined in Presburger arithmetic if we consider several restrictions concerning the transformation matrix. If the matrix *A* defining *R* has eigenvalues which are either zeros or roots of unity, all non-zero eigenvalues being of multiplicity one (these conditions are equivalent to the finite monoid property of [2, 13]), then *wrs(*R*)* is Presburger definable. Otherwise, if all non-zero eigenvalues of *A* are roots of unity, of multiplicities greater or equal to one, *wrs(*R*)* can be expressed using polynomial terms. In this case, we can systematically issue termination preconditions, which are of significant practical importance, as noted in [11].

For space reasons, all proofs are deferred to [7].

<footnote n="4">⁴ This definition is the dual of the *reachability set*, needed for checking safety properties: the reachability set is the least fixpoint of the post-image of the transition relation.</footnote>
**Practical applications** Unfortunately, in practice, the cases in which the closed form of the sequence {$R^i$}$_{i\ge 0}$ is definable in a logic that has quantifier elimination, are fairly rare. All relations considered so far are conjunctive, meaning that they can represent only simple program loops of the form while (condition) {body}, where the loop body contains no further conditional constructs. In order to deal with more complicated program loops, one can use the results from this paper in several ways:

- use the decision procedures as a back-end of a termination analyzer, in order to detect spurious non-termination counterexamples consisting of a finite prefix (stem) and a conjunctive loop body (lasso). The spurious counterexamples can be discarded by intersecting the program model with the complement of the weak deterministic Büchi automaton representing the counterexample, as in [17].

- abstract a disjunctive loop body $R_1 \lor \dots \lor R_n$ by a non-deterministic difference bounds or octagonal<fnref n="5" /> relation $R^\# \supseteq R_{1,...,n}$ and compute the weakest recurrent set of the latter. The complement of this set is a set of configurations from which the original loop terminates.

- attempt to compute a *transition invariant* i.e., an overapproximations of the transitive closure of the disjunctive loop body ($R_1 \vee \dots \vee R_n$)$^+$ (using e.g., the semi-algorithmic unfolding technique described in [6]) and overapproximate it by a disjunction $R_1^\# \vee \dots \vee R_m^\#$ of difference bounds or octagonal relations. Then compute the weakest recurrent set of each relation in the latter disjunction. If $wrs(R_1^\#) = \dots = wrs(R_m^\#) = \emptyset$, the original loop terminates on any input, following the principle of transition invariants [19].

## 1.1 Related Work

The literature on program termination is vast. Most work focuses however on universal termination, such as the techniques for synthesizing linear ranking functions of Sohn and Van Gelder [22] or Podelski and Rybalchenko [18], and the more sophisticated method of Bradley, Manna and Sipma [9], which synthesizes lexicographic polynomial ranking functions, suitable when dealing with disjunctive loops. However, not every terminating program (loop) has a linear (polynomial) ranking function. In this paper we show that, for an entire class of non-deterministic linear relations, defined using octagons, termination is always witnessed by a computable octagonal relation that has a linear ranking function.

Another line of work considers the decidability of termination for simple (conjunctive) linear loops. Initially Tiwari [23] shows decidability of termination for affine linear loops interpreted over *reals*, while Braverman [10] refines this result by showing decidability over *rationals* and over *integers*, for homogeneous relations of the form $C_1x > 0 \land C_2x \ge 0 \land x' = Ax$. The non-homogeneous integer case seems to be much more difficult as it is closely related to the open *Skolem's Problem* [16]: given a linear recurrence {$u_i$}$_{i\ge 0}$, determine whether $u_i = 0$ for some $i \ge 0$.

To our knowledge, the first work on proving non-termination of simple loops is reported in [15]. The notion of *recurrent sets* occurs in this work, however without

<footnote n="5">⁵ The linear affine relations considered in this paper are deterministic, which makes them unsuitable for abstraction.</footnote>
the connection with fixpoint theory, which is introduced in the present work. Finding
recurrent sets in [15] is complete with respect to a predefined set of templates, typically
linear systems of rational inequalities.

The work which is closest to ours is probably that of Cook et al. [11]. In this paper,
the authors develop an algorithm for deriving termination preconditions, by first guess-
ing a ranking function candidate (typically the linear term from the loop condition) and
then inferring a supporting assertion, which guarantees that the candidate function de-
creases with each iteration. The step of finding a supporting assertion requires a fixpoint
iteration, in order to find an invariant condition. Unlike our work, the authors of [11]
do not address issues related to completeness: the method is not guaranteed to find the
weakest precondition for termination, even in cases when this set can be computed. On
the other hand, it is applicable to a large range of programs, extracted from real-life soft-
ware. To compare our method with theirs, we tried all examples available in [11]. Since
most of them are linear affine relations, we used our under-approximation method and
have computed termination preconditions, which turn out to be slightly more general
than the ones reported in [11].

## 2 Preconditions for Non-termination

In the rest of this paper we denote by $\mathbf{x} = \{x_1, \dots, x_n\}$ the set of working variables, ranging over a domain of values denoted as $\mathcal{D}$. A state is a valuation $s : \mathbf{x} \to \mathcal{D}$, or equivalently, an $n$-tuple of values from $\mathcal{D}$. An execution step is a relation $R \subseteq \mathcal{D}^n \times \mathcal{D}^n$ defined by an arithmetic formula $\mathcal{R}(\mathbf{x}, \mathbf{x}')$, where the set $\mathbf{x}' = \{x'_1, \dots, x'_n\}$ denotes the values of the variables after executing $R$ once. If $s$ and $s'$ are valuations of the sets $\mathbf{x}$ and $\mathbf{x}'$, we denote by $\mathcal{R}(s, s')$ the fact that $(s, s') \in \mathcal{R}$. A relation $R$ is said to be consistent if there exist states $s, s'$ such that $\mathcal{R}(s, s')$.

Relational composition is defined as $R_1 \circ R_2 = \{(s, s') \in \mathcal{D}^n \times \mathcal{D}^n \mid \exists s'' \in \mathcal{D}^n . R_1(s, s'') \wedge R_2(s'', s')\}$. For any relation $R \in \mathcal{D}^n \times \mathcal{D}^n$, we consider $R^0$ to be the identity relation, and we define $R^{i+1} = R^i \circ R$, for all $i \ge 0$. The pre-image of a set $S \subseteq \mathcal{D}^n$ via $R$ is the set $\text{pre}_R(S) = \{s \in \mathcal{D}^n \mid \exists s' \in S . \mathcal{R}(s, s')\}$. It is easy to check that $\text{pre}_R^i(S) = \text{pre}_{R^i}(S)$, for any $S \subseteq \mathcal{D}^n$ and for all $i \ge 0$. For any $i \ge 0$, we write $\mathcal{R}^i$ for the formula defining the relation $R^i$ and $\mathcal{R}^{-i}(\top)$ for the formula defining the set $\text{pre}_{R^i}(\mathcal{D}^n)$.

**Definition 1.** A relation $R$ is said to be \*-consistent if and only if, for any $k > 0$, there exists a sequence of states $s_1, \dots, s_k$, such that $\mathcal{R}(s_i, s_{i+1})$, for all $i = 1, \dots, k-1$. $R$ is said to be well-founded if and only if there is no infinite sequence of states $\{s_i\}_{i>0}$, such that $\mathcal{R}(s_i, s_{i+1})$, for all $i > 0$.

Notice that if a relation is not \*-consistent, then it is also well-founded. However the
dual is not true. For instance, the relation $R = \{(n, n-1) \mid n > 0\}$ is both \*-consistent
and well-founded.

**Definition 2.** A set $S \subseteq \mathcal{D}^n$ is said to be a non-termination precondition for $R$ if, for each state $s \in S$ there exists an infinite sequence of states $s_0, s_1, s_2, \dots$ such that $s = s_0$ and $\mathcal{R}(s_i, s_{i+1})$, for all $i \ge 0$.
If $S_0, S_1, \dots$ are all non-termination preconditions for $R$, then the (possibly infinite) union $\bigcup_{i=0,1,\dots} S_i$ is a non-termination precondition for $R$ as well. The set $wnt(R) = \bigcup\{S \in \mathcal{D}^n \mid S$ is a non-termination precondition for $R\}$ is called the weakest non-termination precondition for $R$. A relation $R$ is well-founded if and only if $wnt(R) = \emptyset$. A set $S$ such that $S \cap wnt(R) = \emptyset$ is called a termination precondition.

**Definition 3.** A set $S \subseteq \mathcal{D}^n$ is said to be recurrent for a relation $R \in \mathcal{D}^n \times \mathcal{D}^n$ if and only if $S \subseteq \text{pre}_R(S)$.

**Proposition 1.** Let $S_0, S_1, \dots \in \mathcal{D}^n$ be a (possibly infinite) sequence of sets, all of which are recurrent for a relation $R \in \mathcal{D}^n \times \mathcal{D}^n$. Then their union $\bigcup_{i=0,1,\dots} S_i$ is recurrent for $R$ as well.

The set $wrs(R) = \bigcup\{S \in \mathcal{D}^n \mid S$ is a recurrent set for $R\}$ is called the weakest recurrent set for $R$. By Proposition 1, $wrs(R)$ is recurrent for $R$. Next we define the weakest recurrent set as the greatest fixpoint of the transition relation's pre-image.

**Lemma 1.** Given a relation $R \in \mathcal{D}^n \times \mathcal{D}^n$, the weakest recurrent set for $R$ is the greatest fixpoint of the function $X \mapsto \text{pre}_R(X)$.

As a consequence, we obtain $wrs(R) = \bigcap_{i>0} \text{pre}_R^i(\mathcal{D}^n)$, by the Kleene Fixpoint Theorem. Since $\text{pre}_R^i = \text{pre}_{R^i}$, we have $wrs(R) = \bigcap_{i>0} \text{pre}_{R^i}(\mathcal{D}^n)$. In other words, from any state in the weakest recurrent set for a relation, an iteration of any finite length of the given relation is possible. The following lemma shows that in fact, this is exactly the set of states from which an infinite iteration is also possible.

**Lemma 2.** Given a relation $R \in \mathcal{D}^n \times \mathcal{D}^n$, the weakest recurrent set for $R$ equals its weakest non-termination precondition.

The characterization of weakest recurrent sets as greatest fixpoints of the pre-image function suggests a method for computing such sets. In this section we show that, for certain classes of relations, these sets are definable in Presburger arithmetic, which gives a decision procedure for the well-foundedness problem for certain classes of relations, and consequently, for the termination problem for several classes of program loops.

**Definition 4.** Given a relation $R \in \mathcal{D}^n \times \mathcal{D}^n$ defined by an arithmetic formula $\mathcal{R}(\mathbf{x}, \mathbf{x}')$, the closed form of $R$ is a formula $\mathcal{R}^{(k)}(\mathbf{x}, \mathbf{x}')$, with free variables $\mathbf{x} \cup \mathbf{x}' \cup \{k\}$, such that for every integer valuation $i > 0$ of $k$, $\mathcal{R}^{(i)}(\mathbf{x}, \mathbf{x}')$ defines the relation $R^i$.

*Example* Consider for instance the relation $\mathcal{R}(x, x') \equiv x \ge 0 \land x' = x - 1$. Then we have $\mathcal{R}^{(k)}(x, x') \equiv x \ge k - 1 \land x' = x - k$. □

Since, by Lemma 1, we have $wrs(R) = \text{gfp}(\text{pre}_R) = \bigcap_{i>0} \text{pre}_{R^i}(\mathcal{D}^n)$, using the closed form of $R$, one can now define:

$$wrs(R) \equiv \forall k > 0 \exists \mathbf{x}' . \mathcal{R}^{(k)}(\mathbf{x}, \mathbf{x}') \quad (1)$$

Because Presburger arithmetic has quantifier elimination, $wrs(R)$ can be defined in Presburger arithmetic$^6$ whenever $\mathcal{R}^{(k)}$ can. In [5] we show two classes of relations

<footnote>$^6$Or, for that matter, in any theory that has quantifier elimination.</footnote>
for which $\mathcal{R}^{(k)}$ is Presburger definable: octagonal and finite-monoid affine relations (the formal definitions of these classes are given in the next section). For each of these classes of loops termination is decidable, by the above argument.

*Example* (ctd.) Consider again the relation with closed form $\mathcal{R}^{(k)}(x, x') \equiv x \ge k - 1 \land x' = x - k$. Quantifier elimination yields $wrs(R) \equiv \forall k > 0 \exists x' \cdot x \ge k - 1 \land x' = x - k \equiv \forall k > 0 \cdot x \ge k - 1 \equiv \text{false}$. Hence the relation $\mathcal{R}$ is well-founded. $\square$

# 3 Octagonal Relations

In this and the following sections, we assume that the variables $\mathbf{x} = \{x_1, \dots, x_n\}$ range over integers i.e., that $\mathcal{D} = \mathbb{Z}$.

**Definition 5.** A formula $\phi(\mathbf{x})$ is a difference bounds constraint if it is equivalent to a finite conjunction of atomic propositions of the form $x_i - x_j \le a_{ij}$, for $1 \le i, j \le n$, $i \ne j$, where $a_{ij} \in \mathbb{Z}$.

Given a difference bounds constraint $\phi$, a difference bounds matrix (DBM) representing $\phi$ is a matrix $m_{\phi} \in \mathbb{Z}_{\infty}^{n \times n}$ such that $(m_{\phi})_{ij} = a_{ij}$, if $x_i - x_j \le a_{ij}$ is an atomic proposition in $\phi$, and $\infty$, otherwise.

**Definition 6.** A consistent DBM $m \in \mathbb{Z}_{\infty}^{n \times n}$ is said to be closed if and only if $m_{ii} = 0$ and $m_{ij} \le m_{ik} + m_{kj}$, for all $1 \le i, j, k \le n$.

Given a consistent DBM $m$, we denote by $m^*$ the (unique) closed DBM equivalent with it. It is well-known that, if $m$ is consistent, then $m^*$ is unique, and can be computed from $m$ in time $O(n^3)$, by the classical Floyd-Warshall algorithm.

The octagonal relations are a generalization of difference bounds relations.

**Definition 7.** A formula $\phi(\mathbf{x})$ is an octagonal constraint if it is equivalent to a finite conjunction of terms of the form $\pm x_i \pm x_j \le a_{ij}$, where $a_{ij} \in \mathbb{Z}$ and $1 \le i, j \le n$.

We represent octagons as difference bounds constraints over the dual set of variables $y = \{y_1, y_2, \dots, y_{2n}\}$, with the convention that $y_{2i-1}$ stands for $x_i$ and $y_{2i}$ for $-x_i$, respectively. For example, the octagonal constraint $x_1 + x_2 = 3$ is represented as $y_1 - y_4 \le 3 \land y_2 - y_3 \le -3$. To handle the dual variables in the following, we define $\bar{i} = i - 1$, if $i$ is even, and $\bar{i} = i + 1$ if $i$ is odd. We say that a DBM $m \in \mathbb{Z}_{\infty}^{2n \times 2n}$ is coherent iff $m_{ij} = m_{\bar{j}\bar{i}}$ for all $1 \le i, j \le 2n$. The coherence property is needed because any atomic proposition $x_i - x_j \le a$, in $\phi$ can be represented as both $y_{2i-1} - y_{2j-1} \le a$ and $y_{2j} - y_{2i} \le a$, $1 \le i, j \le n$. We denote by $\bar{\phi}$ the difference bounds formula $\phi[y_1/x_1, y_2/ - x_1, \dots, y_{2n-1}/x_n, y_{2n}/ - x_n]$ with free variables $y$. The following equivalence relates $\phi$ and $\bar{\phi}$:

$$ \phi(\mathbf{x}) \Leftrightarrow (\exists y_2, y_4, \dots, y_{2n} \cdot \bar{\phi} \land \bigwedge_{i=1}^{n} y_{2i-1} + y_{2i} = 0)[x_1/y_1, \dots, x_n/y_{2n-1}] \quad (2) $$

Given a coherent DBM $m$ representing $\bar{\phi}$, we say that $m$ is octagonal-consistent if and only if $\phi$ is consistent. The following definition gives the canonical form of a DBM representing an octagonal-consistent constraint.
**Definition 8.** An octagonal-consistent coherent DBM $m \in \mathbb{Z}^{2n \times 2n}$ is said to be tightly closed if and only if the following hold:

$$1. \ m_{ii} = 0, \forall 1 \le i \le 2n$$

$$2. \ m_{i\bar{i}} \text{ is even}, \forall 1 \le i \le 2n$$

$$3. \ m_{ij} \le m_{ik} + m_{kj}, \forall 1 \le i, j, k \le 2n$$

$$4. \ m_{ij} \le \lfloor \frac{m_{i\bar{i}}}{2} \rfloor + \lfloor \frac{m_{j\bar{j}}}{2} \rfloor, \forall 1 \le i, j \le 2n$$

Given an octagonal-consistent DBM $m$, we denote by $m^t$ the equivalent tightly closed DBM. The tight closure of an octagonal-consistent DBM $m$ is unique and can be computed in time $O(n^3)$ as $m_{i,j}^t = \min \{m_{i,j}^*, \lfloor \frac{m_{i,\bar{i}}^*}{2} \rfloor + \lfloor \frac{m_{j,j}^*}{2} \rfloor \} [1]$. This generalizes to unbounded finite compositions of octagonal relations [4]:

$$\forall k \ge 0. (m_{R^k})_{i,j} = \min \left\{ (m_{\bar{R}^k})_{i,j}, \left\lfloor \frac{(m_{\bar{R}^k})_{i,\bar{i}}}{2} \right\rfloor + \left\lfloor \frac{(m_{\bar{R}^k})_{\bar{j},j}}{2} \right\rfloor \right\} \quad (3)$$

Notice that the above relates the entries of the tightly closed DBM representation of $R^k$ with the entries of the closed DBM representation of the relation defined by $\bar{R}^k$.

We are now ready to introduce a result [5] that defines the “shape” of the closed form $\mathcal{R}^{(k)}$ for an octagonal relation $R$. Intuitively, for each $i \ge 0$, $R^i$ is an octagon, whose bounds evolve in a periodic way. The following definition gives the precise meaning of periodicity for relations that have a matrix representation.

**Definition 9.** An infinite sequence of matrices $\{M_k\}_{k=1}^\infty \in \mathbb{Z}_\infty^{m \times m}$ is said to be ultimately periodic if and only if:

$$\exists b > 0 \exists c > 0 \exists \Lambda_0, \Lambda_1, \dots, \Lambda_{c-1} \in \mathbb{Z}_\infty^{m \times m} . M_{b+(k+1)c+i} = \Lambda_i + M_{b+kc+i}$$

for all $k \ge 0$ and $i = 0, 1, \dots, c-1$. The smallest $b, c$ for which the above holds are called prefix and period of the $\{M_k\}_{k=1}^\infty$ sequence, respectively.

A result reported in [5] is that the sequence $\{m_{R^i}^t\}_{i \ge 0}$ (3) of tightly closed matrices representing the sequence $\{R^i\}_{i \ge 0}$ of powers of a $*$-consistent octagonal relation $R$ is ultimately periodic, in the sense of the above definition. The constants $b$ and $c$ from Definition 9 will also be called the *prefix and period of the octagonal relation R*, throughout this section.

For a set $v$ of variables, let $U(v) = \{\pm v_1 \pm v_2 | v_1, v_2 \in v\}$ denote the set of octagonal terms over $v$. As a first remark, by the periodicity of the sequence $\{m_{R^i}^t\}_{i \ge 0}$, the closed form of the subsequence $\{R^{b+c\ell}\}_{\ell \ge 0}$ (of $\{R^i\}_{i \ge 0}$) can be defined as:

$$\mathcal{R}_{b,c}^{(\ell)} \equiv \bigwedge_{u \in U(v \cup x')} u \le a_u \ell + d_u, \forall \ell \ge 0 \quad (4)$$

where $a_u = (\Lambda_0)_{ij}$, $d_u = (m_{R^b})_{ij}$ for all octagonal terms $u = y_i - y_j$. This is indeed the case, since the matrix sequence $\{m_{R^{b+c\ell}}^t\}_{\ell \ge 0}$ is ultimately periodic i.e., $m_{R^{b+c\ell}}^t = m_{R^b}^t + \ell \Lambda_0$, for all $\ell \ge 0$.

Second, we notice that the greatest fixpoint of a monotonic$^7$ function can be computed by an infinite subsequence of the classical decreasing Kleene iteration. Concretely, we have that $wrs(R) = \bigcap_{k>0} pre_R^k(\mathbb{Z}^n) = \bigcap_{\ell \ge 0} pre_R^{b+\ell}(\mathbb{Z}^n)$. The latter

<footnote>$^7$ In our case, $pre_R^{k_1}(\mathbb{Z}^n) \supseteq pre_R^{k_2}(\mathbb{Z}^n)$, for $k_1 \le k_2$.</footnote>
set can now be defined using the closed form of the subsequence (4) i.e., wrs(R) ≡ ∀ℓ ≥ 0 ∃x' . R<sub>b,c</sub><sup>(ℓ)</sup>(x, x').

The proof of periodicity from [5] relies on the fact that the DBM encoding of the closed form of R is tightly closed for any unfolding of length k, see (3). Hence, the existential quantifier ∃x' can be eliminated by simply deleting all atomic propositions involving primed variables from (4). Thus, we obtain:

$$
\mathrm{wrs}(R) \equiv \forall \ell \ge 0 \ \bigwedge_{u \in U(\mathbf{x})} u \le a_u \ell + d_u \equiv \bigwedge_{u \in U(\mathbf{x})} u \le \inf \{a_u \ell + d_u \mid \ell \ge 0\}
$$

where, for a set S ⊆ Z, inf S denotes the minimal element of S, if one exists, or −∞,
otherwise. We have

$$
\inf \{a_u \ell + d_u \mid \ell \ge 0\} = \begin{cases} -\infty & \text{if } a_u < 0 \\ d_u & \text{otherwise} \end{cases}
$$

Hence wrs(R) is the empty set, if $a_u < 0$ for some $u \in U(\mathbf{x})$. Otherwise, we obtain
wrs(R) = $\bigwedge_{u \in U(\mathbf{x})} u \le d_u$. However, this is exactly the set defined by $\mathcal{R}^{-b}(\top) =$
$\exists \mathbf{x}' . \mathcal{R}^b(\mathbf{x}, \mathbf{x}')$, by (4).

**Lemma 3.** Let R be a \*-consistent octagonal relation with prefix b, period c and let $\mathcal{R}_{b,c}^{(\ell)}$ be the closed form of $\{R^{b+c\ell}\}_{\ell \ge 0}$ as defined in (4). Then, R is well-founded iff there exists $u \in U(\mathbf{x})$ s.t. $a_u < 0$. Moreover, if R is not well-founded, $wrs(R) = \mathcal{R}^{-b}(\top)$.

The following lemma can be applied as a decision procedure too, whenever the
prefix b of an octagon R is known.

**Lemma 4.** Let R be a \*-consistent octagonal relation with prefix b and let f ≥ b. Then, R is well-founded iff R<sup>-f</sup>(⊤) ≠ R<sup>-f-1</sup>(⊤). Moreover, if R is not well-founded, then wrs(R) = R<sup>-f</sup>(⊤).

**Lemma 5.** Let R be \*-consistent relation. If R is well-founded, then R<sup>-i-1</sup>(⊤) ⊂ R<sup>-i</sup>(⊤), for all i ≥ 0.

Proof. By contraposition. Suppose R<sup>-i-1</sup>(⊤) = R<sup>-i</sup>(⊤) for some i. If R<sup>-i</sup>(⊤) = ∅, then clearly R can't be \*-consistent. If R<sup>-i</sup>(⊤) ≠ ∅, then clearly R can't be well-founded. □

**Lemma 6.** Let R be \*-consistent relation. If R<sup>-i-1</sup>(⊤) = R<sup>-i</sup>(⊤), then wrs(R) = R<sup>-i</sup>(⊤) ≠ ∅, for all i ≥ 0.

Proof. By Lemma 1 and since R<sup>-i-1</sup>(⊤) = R<sup>-i</sup>(⊤), wrs(R) = R<sup>-i</sup>(⊤). \*-consistency implies that R<sup>-i</sup>(⊤) ≠ ∅. □

Proof of Lemma 4

*Proof.* Suppose that *R* is \*-consisten and well-founded. Then, by Lemma ?? *R*<sup>-f</sup>(*T*) ≠ *R*<sup>-f-1</sup>(*T*). Supposet that *R* is \*-consistent and *R*<sup>-f</sup>(*T*) = *R*<sup>-f-1</sup>(*T*). Then, by Lemma ??, *wrs*(*R*) ≠ ∅ andt thus *R* cannot be well-founded. □
<caption>**Algorithm 1** Weakest Recurrent Set for Octagons</caption>

1: **procedure** WEAKESTRECURRENTSET($R(\mathbf{x}, \mathbf{x}')$)
2: &nbsp;&nbsp;&nbsp;&nbsp;V $\leftarrow$ R
3: &nbsp;&nbsp;&nbsp;&nbsp;**for all** i $\in$ 1, 2, ..., 3n **do**
4: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;V $\leftarrow$ V $\circ$ V
5: &nbsp;&nbsp;&nbsp;&nbsp;W $\leftarrow$ V $\circ$ R
6: &nbsp;&nbsp;&nbsp;&nbsp;if $V^{-1}(\top) = W^{-1}(\top)$ **then** **return** $V^{-1}(\top)$
7: &nbsp;&nbsp;&nbsp;&nbsp;**else** **return** $\emptyset$

Next, we present an algorithm computing $wrs(R)$ for arbitrary octagonal relation.

Intuitively, the correctness for *-consistent input is based on existence of an upper bound $5^n$ on prefix $b$. Note that for all $B > 0$, $R^B$ can be computed in $\log_2 B$ time by iterating the line 4. Thus, the algorithm computes $U = R^{2^{3n}}$ and $V = R^{2^{3n}+1}$. Since $3n \ge \lceil \log_2(5^n) \rceil$, we can apply Lemma 4, which ensures correctness. Furthermore, since both octagonal composition (lines 4 and 5), inclusion (line 6) can be computed in $O(n^3)$ time and pre-image (line 6) is computed as a projection on a matrix, the algorithm runs in $O(n^4)$ time. We defer the discussion for *-inconsistent inputs to ??.

**Theorem 1.** Given an octagonal relation $R(\mathbf{x}, \mathbf{x}')$, where $\mathbf{x} = \{x_1, \dots, x_n\}$, the Algorithm 1 computes $wrs(R)$ in $O(n^4)$ time and $O(n^2)$ space.

**3.1 On the Existence of Linear Ranking Functions**

A ranking function for a given relation $R$ constitutes a proof of the fact that $R$ is well-founded. We distinguish here two cases. If $R$ is not *-consistent, then the well-foundedness of $R$ is witnessed simply by an integer constant $i > 0$ such that $R^i = \emptyset$. Otherwise, if $R$ is *-consistent, we need a better argument for well-foundedness. In this section we show that, for any *-consistent well-founded octagonal relation $R$ with prefix $b$, the (strenghtened) relation defined by $R^{-b}(\top) \wedge R$ is well-founded and has a linear ranking function, even when $R$ alone does not have one. For space reasons, we do not give here all the details of the construction of such a function. However, the existence proof suffices, as one can use *complete ranking function extraction tools* (such as e.g. RankFinder [18]) in order to find them.

**Definition 10.** Given a relation $R \subseteq \mathbb{Z}^n \times \mathbb{Z}^n$, a linear ranking function for $R$ is a term $f(\mathbf{x}) = \sum_{i=1}^n a_i x_i$ such that, for all states $s, s' : \mathbf{x} \to \mathbb{Z}$:

1. $f$ is decreasing: $\mathcal{R}(s, s') \to f(s) > f(s')$

2. $f$ is bounded: $\mathcal{R}(s, s') \to (f(s) > h \land f(s') > h)$, for some $h \in \mathbb{Z}$.

The main result of this section is the following:

**Theorem 2.** Let $R \subseteq \mathbb{Z}^n \times \mathbb{Z}^n$ be a *-consistent and well-founded octagonal relation, with prefix $b \ge 0$. Then, the relation defined by $R^{-b}(\top) \wedge R$ is well founded and has a linear ranking function.

The first part of the theorem is proved by the following lemma:
**Lemma 7.** Let $R \subseteq \mathbb{Z}^n \times \mathbb{Z}^n$ be a relation, and $m > 0$ be an integer. Then $wrs(R) = \emptyset$ if and only if $wrs(R_m) = \emptyset$, where $R_m$ is the relation defined by $R^{-m}(\top) \wedge R$.

It remains to prove that the witness relation defined by $\mathcal{R}^{-b}(\top) \wedge \mathcal{R}$ has a linear ranking function, provided that it is well-founded. The proof is organized as follows. First we show that well-foundedness of an octagonal relation $R$ is equivalent to the well-foundedness of its difference bounds representation $\bar{\mathcal{R}}$ (Lemma 8). Second, we use a result from [8], that the constraints in the sequence of iterated difference bounds relations $\{\bar{\mathcal{R}}^i\}_{i \ge 0}$ can be represented by a finite-state weighted automaton, called the zigzag automaton in the sequel. If the relation defined by $\bar{\mathcal{R}}$ is well-founded, then this weighted automaton must have a cycle of negative weight. The structure of this cycle, representing several of the constraints in $\bar{\mathcal{R}}$, is used to show the existence of the linear ranking function for the witness relation $\mathcal{R}^{-b}(\top) \wedge \mathcal{R}$.

**Lemma 8.** Let $R \subseteq \mathbb{Z}^n \times \mathbb{Z}^n$ be an octagonal relation and $R_{db}$ be the difference bounds relation defined by $\bar{\mathcal{R}}$. Then $R$ is well-founded if and only if $R_{db}$ is well-founded.

The above lemma reduces the problem of showing existence of a ranking function for an octagonal relation $\mathcal{R}(\mathbf{x}, \mathbf{x}')$ to showing existence of a ranking function for its difference bounds encoding $\bar{\mathcal{R}}(\mathbf{y}, \mathbf{y}')$. Assume that $f(\mathbf{y})$ is a ranking function for $\bar{\mathcal{R}}$. Then $f[x_i/y_{2i-1}, -x_i/y_{2i}]_{i=1}^n$ is a linear ranking function for $R$. Hence, in the rest of this section, we consider without loss of generality that $R$ is a difference bounds relation.

**Zigzag Automata** For the later developments, we need to introduce the zigzag automaton corresponding to a difference bounds relation $R$. Intuitively, for any $i > 0$, the relation $R^i$ can be represented by a constraint graph which is the $i$-times repetition of the constraint graph of $R$. The constraints induced by $R^i$ can be represented as shortest paths in this graph, and can be recognized (in the classical automata-theoretic sense) by a weighted automaton $\mathcal{A}_R$. The structure of this automaton is needed to show the existence of a linear ranking function.

For a difference bounds relation $R$, we define the directed graph $\mathcal{G}_R$, whose set of vertices is the set $\mathbf{x} \cup \mathbf{x}'$, and in which there is an edge from $x_i$ to $x_j$ labeled $a_{ij}$ if and only if the atomic proposition $x_i - x_j \le a_{ij}$ occurs in $R$. Clearly, $m_R$ is the incidence matrix of $\mathcal{G}_R$. We define the concatenation of $\mathcal{G}_R$ with itself as the disjoint union of two copies of $\mathcal{G}_R$, in which the $\mathbf{x}$ vertices of the second copy overlap with the $\mathbf{x}'$ vertices of the first copy. Then $R^m$ corresponds to the graph $\mathcal{G}_R^m$, obtained by concatenating the graph of $R$ to itself $m > 0$ times.

*Example* Let $\mathcal{R} \equiv x_2-x_1' \le -1 \wedge x_3-x_2' \le 0 \wedge x_1-x_3' \le 0 \wedge x_4-x_1' \le 0 \wedge x_3'-x_4 \le 0$. Figure 1 (b) shows $\mathcal{G}_R^8$, the 8-times unfolding of the graph $\mathcal{G}_R$ representing $R$. $\square$

Given a difference bounds relation $R$, the zigzag automaton $\mathcal{A}_R$ recognizes all paths from $x_i$ to $x_j$ in $\mathcal{G}_R^k$. Intuitively, a path $\pi$ between $x_i$ and $x_j$ in $\mathcal{G}_R^k$, is represented by a word $w$ of length $k$, as follows: the $w_l$ symbol represents simultaneously all edges of $\pi$ that involve only nodes from $\mathbf{x}^{(l)} \cup \mathbf{x}^{(l+1)}$, for all $0 \le l < k$. The alphabet of the zigzag automaton consists of subgraphs of $\mathcal{G}_R$, where the weight of a subgraph is the sum of the weights on its edges. The set of control states of the zigzag automaton is$^8$

<footnote>$^8$ The intuition behind the names $\{l, r, lr, rl, \perp\}$ of components of control states is that they capture the direction of incoming and outgoing edges (l for left, r for right).</footnote>
<figure><img src="image_2.png" /><figcaption>**Fig. 1.** (a) Unfolding of $\mathcal{G}_R$. Here $\mathbf{x}^{(i)} = \{x^{(i)} | x \in \mathbf{x}\}$. (b) A run of the zigzag automaton over a path in $\mathcal{G}_R^{\mathbf{s}}$.</figcaption></figure>

$\{l, r, lr, rl, \perp\}^n$. Clearly, the size of the zigzag automaton is at most $5^n$. For a complete definition, the interested reader may consult [8].

*Example* (ctd.) An example of a run of $\mathcal{A}_R$ recognizing a path of constraints in $\mathcal{G}_R^8$ is given in Figure 1 (b). The word accepted by $\pi$ is a subgraph of $\mathcal{G}_R^8$ shown in Figure 1 (a). The cycle $\pi: q_1 \xrightarrow{G_1} q_2 \xrightarrow{G_2} q_3 \xrightarrow{G_3} q_1$ is taken several times in this run. The weights of the symbols on the run are $w(G_1)=w(G_2)=w(G_4)=0$ and $w(G_3)=-1$. $\square$

The following lemma proves the existence of a negative weight cycle in the zigzag automata corresponding to well-founded difference bounds relation. The intuition behind this fact is that the rates of the DBM sequence $\{m_{R^i}\}_{i>0}$ are weights of optimal ratio (weight per length) cycles in the zigzag automaton. According to the previous section, if $R$ is well-founded, there exists a negative rate for $\{m_{R^i}\}_{i>0}$, which implies the existence of a negative cycle in the zigzag automaton.

**Lemma 9.** If $R$ is a $*$-consistent well-founded difference bounds relation of prefix $b \ge 0$, and $\mathcal{A}_R$ is its corresponding zigzag automaton, then there exists a cycle $\pi$ from a state $q$ to itself, such that $w(\pi) < 0$ and there exists paths $\pi_i$ from an initial state to $q$, and $\pi_f$ from $q$ to a final state, such that $|\pi_i| + |\pi_f| = b$.

Next we prove the existence of a linear decreasing function, based on the existence of a negative weight cycle in the zigzag automaton.

**Lemma 10.** If $R$ is a $*$-consistent well-founded difference bounds relation of prefix $b \ge 0$, then there exists a linear function $f(\mathbf{x})$ such that, for all states $s, s' : \mathbf{x} \to \mathbb{Z}$ we have $\mathcal{R}^{-b}(\top)(s) \wedge \mathcal{R}(s, s') \to f(s) > f(s')$.

*Example* (ctd.) We illustrate the construction of linear decreasing function. Summing the edges in $\pi$, we obtain $x_2-x'_1+x_1-x'_3+x_3-x'_2+x'_4-x_4+x'_4-x_4+x'_4-x_4 \le -1$, which simplifies to $x_1+x_2+x_3-3x_4-(x'_1+x'_2+x'_3-3x_4) \le -1$. Letting $f(\mathbf{x}) = -(x_1+x_2+x_3-3x_4)$, we have that $f(\mathbf{x}) > f(\mathbf{x}')$. $\square$

Last, we prove that the function $f$ of Lemma 10 is bounded, concluding that it is indeed a ranking function. Since each run in the zigzag automaton recognizes a path from some $x_i$ to some $x_j$, a run that repeats a cycle can be decomposed into a prefix, the cycle itself and a suffix. The recognized path may traverse the cycle several times, however each exit point from the cycle must match a subsequent entry point. These paths from
the exit to the corresponding entries give us the necessary lower bound. In fact, these paths appear already on graphs $G_R$, for $i \ge b$. Hence the need for a strengthened witness $\mathcal{R}^{-b}(\top) \wedge \mathcal{R}$, as $\mathcal{R}$ alone is not enough for proving boundedness of $f$.

**Lemma 11.** If $R$ is a $*$-consistent well-founded difference bounds relation of prefix $b$, and $f(\mathbf{x})$ is the linear decreasing function from Lemma 10, there exists an integer $h$ such that, for all states $s, s' : \mathbf{x} \to \mathbb{Z}$, $(\mathcal{R}^b(\top)(s) \wedge \mathcal{R}(s, s')) \to (f(s) \ge h \wedge f(s') \ge h)$.

*Example* (ctd.) We illustrate the boundedness of $f = -(x_1+x_2+x_3-3x_4)$ (see Figure 1b). Since there is a path $\mathbf{x}_2^{(6)} \rightsquigarrow \mathbf{x}_4^{(6)}$ in $G_3G_4$ (and hence in $G_R^2$), then $\mathcal{R}^2 \to (x_2-x_4 \le -1)$, and by Lemma 15, we obtain $\mathcal{R}^b \to (x_2-x_4 \le -1)$. Similarly, since there is a path $\mathbf{x}_3^{(5)} \rightsquigarrow \mathbf{x}_4^{(5)}$ in $G_2G_3G_4$ (and hence in $G_R^3$), we obtain $\mathcal{R}^b \to (x_3-x_4 \le -1)$. Similarly, since there is a path $\mathbf{x}_1^{(4)} \rightsquigarrow \mathbf{x}_4^{(4)}$ in $G_1G_2G_3G_4$ (and hence in $G_R^4$), we obtain $\mathcal{R}^b \to (x_1-x_4 \le -1)$. Summing up these inequalities, we obtain that $f(\mathbf{x}) = -(x_1+x_2+x_3-3x_4) \ge 3$ and, thus $\mathcal{R}^{-b}(\top) \wedge \mathcal{R} \to (f \ge 3)$.

As an experiment, we have tried the RANKFINDER [18] tool (complete for linear ranking functions), which failed to discover a ranking function on this example. This comes with no surprise, since no linear decreasing function that is bounded after the first iteration exists. However, RANKFINDER finds a ranking function for the witness relation $\mathcal{R}^{-b}(\top) \wedge \mathcal{R}$ instead. □

# 4 Linear Affine Relations

Let $\mathbf{x} = (x_1, \dots, x_n)^\top$ be a column vector of variables ranging over integers. A linear affine relation is a relation of the form $\mathcal{R}(\mathbf{x}, \mathbf{x}') \equiv C\mathbf{x} \ge \mathbf{d} \wedge \mathbf{x}' = A\mathbf{x} + \mathbf{b}$, where $A \in \mathbb{Z}^{n \times n}$, $C \in \mathbb{Z}^{p \times n}$ are matrices, and $\mathbf{b} \in \mathbb{Z}^n$, $\mathbf{d} \in \mathbb{Z}^p$ are column vectors of integer constants. Notice that we consider linear affine relations to be deterministic, unlike the octagonal relations considered in the previous. In the following, it is convenient to work with the equivalent homogeneous form:

$$ \mathcal{R}(\mathbf{x}, \mathbf{x}') \equiv C_h \mathbf{x}_h \ge \mathbf{0} \wedge \mathbf{x}'_h = A_h \mathbf{x}_h \quad (5) $$

$$ A_h = \begin{pmatrix} A & \mathbf{b} \\ 0 & 1 \end{pmatrix} \quad C_h = (C - \mathbf{d}) \quad \mathbf{x}_h = \begin{pmatrix} \mathbf{x} \\ x_{n+1} \end{pmatrix} \quad (5) $$

The closed form of a linear affine relation is defined by the following formula:

$$ \mathcal{R}^{(k)}(\mathbf{x}, \mathbf{x}') \equiv \exists x_{n+1}, x'_{n+1} \cdot \mathbf{x}'_h = A_h^k \mathbf{x}_h \wedge \forall 0 \le l < k \cdot C_h A_h^l \mathbf{x} \ge \mathbf{0} \wedge x_{n+1} = 1 \quad (6) $$

Intuitively, the first conjunct defines the (unique) outcome of iterating the relation $\mathbf{x}' = A\mathbf{x} + \mathbf{b}$ for $k$ steps, while the second (universally quantified) conjunct ensures that the condition $(C\mathbf{x} \ge \mathbf{d})$ has been always satisfied all along the way. The definition of the weakest recursive set of a linear affine relation is (after the elimination of the trailing existential quantifier):

$$ wrs(R)(\mathbf{x}) \equiv \exists x_{n+1} \forall k > 0 . C_h A_h^k \mathbf{x} \ge \mathbf{0} \wedge x_{n+1} = 1 \quad (7) $$
The main difficulty with the form (7) comes from the fact that the powers of a matrix A cannot usually be defined in a known decidable theory of arithmetic. In the following, we discuss the case of A having the finite monoid property [2, 25], which leads to wrs(R) being Presburger definable. Further, we relax the finite monoid condition and describe a method for generating sufficient termination conditions, i.e. sets S ∈ Zⁿ such that S ∩ wrs(R) = ∅.

Some basic notions of linear algebra are needed in the following. If A ∈ Zⁿ×ⁿ is a square matrix, and v ∈ Zⁿ is a column vector of integer constants, then any complex number λ ∈ C such that Av = λv, for some complex vector v ∈ Cⁿ, is called an eigenvalue of A. The vector v in this case is called an eigenvector of A. It is known that the eigenvalues of A are the roots of the characteristic polynomial det(A − λIₙ) = 0, which is an effectively computable univariate polynomial in λ. A complex number r is said to be a root of the unity if rⁿ = 1 for some integer d > 0.

In the previous work of Weber and Seidl [25], Boigelot [2], and Finkel and Leroux [13], a restriction of linear affine relations has been introduced, with the goal of defining the closed form of relations in Presburger arithmetic. A matrix A ∈ Zⁿ×ⁿ is said to have the finite monoid property if and only if its set of powers {Aᵢ | i ≥ 0} is finite. A linear affine relation has the finite monoid property if and only if the matrix A defining the update has the finite monoid property.

**Lemma 12 ([13,2]).** A matrix A ∈ Zⁿ×ⁿ has the finite monoid property iff:

1. all eigenvalues of A are either zero or roots of the unity, and

2. all non-zero eigenvalues are of multiplicity one.

Both conditions are decidable.

In the following, we drop the second requirement of Lemma 12, and consider only linear relations, such that all non-zero eigenvalues of A are roots of the unity. In this case, R⁽ᵏ⁾ cannot be defined in Presburger arithmetic any longer, thus we renounce defining wrs(R) precisely, and content ourselves with the discovery of sufficient conditions for termination. Basically given a linear affine relation R, we aim at finding a disjunction φ(x) of linear constraints on x, such that φ ∧ wrs(R) is inconsistent, without explicitly computing wrs(R).

**Lemma 13.** Given a square matrix A ∈ Zⁿ×ⁿ, whose non-zero eigenvalues are all roots of the unity. Then (A^m)_{i,j} ∈ Q[m], for all 1 ≤ i, j ≤ n, are effectively computable polynomials with rational coefficients.

We turn now back to the problem of defining wrs(R) for linear affine relations R of the form (7). First notice that, if all non-zero eigenvalues of A are roots of the unity, then the same holds for Aₕ (5). By Lemma 13, one can find rational polynomials pᵢⱼ(k) defining (Aₕᵏ)ᵢⱼ, for all 1 ≤ i, j ≤ n. The condition (7) resumes to a conjunction of the form:

$$wrs(R)(\mathbf{x}) \equiv \bigwedge_{i=1}^{n} \forall k > 0 . P_i(k, \mathbf{x}) \geq 0 \quad (8)$$

where each Pᵢ = aᵢⱼ(x) · kᵈ + ... + aᵢ,₁(x) · k + aᵢ,₀(x) is a polynomial in k whose coefficients are the linear combinations aᵢⱼ ∈ Q[x]. We are looking after a sufficient
condition for termination, which is, in this case, any set of valuations of x that would invalidate (8). The following proposition gives sufficient invalidating clauses for each conjunct above. By taking the disjunction of all these clauses we obtain a sufficient termination condition for R.

**Lemma 14.** Given a polynomial $P(k, \mathbf{x}) = a_d(\mathbf{x}) \cdot k^d + \dots + a_1(\mathbf{x}) \cdot k + a_0(\mathbf{x})$, there exists $n > 0$ such that $P(n, \mathbf{x}) < 0$ if, for some $i = 0, 1, \dots, d$, we have $a_{d-i}(\mathbf{x}) < 0$ and $a_d(\mathbf{x}) = a_{d-1}(\mathbf{x}) = \dots = a_{d-i+1}(\mathbf{x}) = 0$.

*Example* Consider the following program [11], and its linear transformation matrix A.

$$
\begin{array}{l@{\qquad}l@{\qquad}l}
\text{while } (x \ge 0) & A = \begin{pmatrix} 1 & 1 & 0 \\ 0 & 1 & 1 \\ 0 & 0 & 1 \end{pmatrix} & A^k = \begin{pmatrix} 1 & k & \frac{k(k-1)}{2} \\ 0 & 1 & k \\ 0 & 0 & 1 \end{pmatrix} \\
x' = x + y & & \\
y' = y + z & &
\end{array}
$$

The characteristic polynomial of A is $\det(A - \lambda I_3) = (1 - \lambda)^3$, hence the only eigenvalue is 1, with multiplicity 3. Then we compute $A^k$ (see above), and $x' = x + k \cdot y + \frac{k(k-1)}{2}z$ gives the value of x after k iterations of the loop. Hence the (precise) non-termination condition is: $\forall k > 0 \cdot \frac{\bar{z}}{2} \cdot k^2 + (y - \frac{\bar{z}}{2}) \cdot k + x \ge 0$. A sufficient condition for termination is: $(z < 0) \lor (z = 0 \land y < 0) \lor (z = 0 \land y = 0 \land x < 0)$ □

We can generalize this method further to the case where all eigenvalues of A are of the form $q \cdot r$, with $q \in \mathbb{R}$ and $r \in \mathbb{C}$ being a root of the unity. The main reason for not using this condition from the beginning is that we are, to this point, unaware of its decidability status. With this condition instead, it is sufficient to consider only the eigenvalues with the maximal absolute value, and the polynomials obtained as sums of the polynomial coefficients of these eigenvalues. The result of Lemma 13 and the sufficient condition of Lemma 14 carry over when using these polynomials instead.

# 5 Experimental Evaluation

We have validated the methods described in this paper by automatically verifying termination of all the octagonal running examples, and of several integer programs synthesized from (i) programs with lists [3] and (ii) VHDL models [21]. We have first computed automatically their strongest summary relation $\mathcal{T}$, by adapting the method for reachability analysis for integer programs, described in [6], and implemented in the FLATA tool [14]. Then we automatically proved that $\mathcal{T}$ is contained in a disjunction of octagonal relations, which are found to be well-founded by the procedure described in Section 3.

We have first verified the termination of the LISTCOUNTER and LISTREVERSAL programs, which were obtained using the translation scheme from [3], which generates an integer program from a program manipulating dynamically allocated single-selector linked lists. Using the same technique, we also verified the COUNTER and SYNLIFO programs, obtained by translating VHDL designs of hardware counter and synchronous LIFO [21]. These models have infinite runs for any input values, which is to be expected, as they encode the behavior of synchronous reactive circuits.
Second, we have compared (Table 1) our method for termination of linear affine loops with the examples given in [11], and found the same termination preconditions as they do, with one exception, in which we can prove universal termination in integer input values (row 3 of Table 1). The last example from [11] is the Euclidean Greatest Common Divisor algorithm, for which we infer automatically the correct termination preconditions using a disjunctively well-founded octagonal abstraction of the transition invariant.

<table><caption>**Table 1.** Termination preconditions for several program fragments from [11]</caption><thead><tr><th>PROGRAM</th><th>COOK ET. AL [11]</th><th>LINEAR AFFINE LOOPS</th></tr></thead><tbody><tr><td>if (lvar ≥ 0)<br>while (lvar &lt; 2<sup>30</sup>)<br>lvar = lvar &lt;&lt; 1;</td><td>lvar &gt; 0 ∨ lvar &lt; 0 ∨ lvar ≥ 2<sup>30</sup></td><td>¬(lvar=0) ∨ lvar ≥ 2<sup>30</sup></td></tr><tr><td>while (x ≤ N)<br>if (*) { x=2*x+y;<br>y=y+1; }<br>else x++;</td><td>x &gt; N ∨ x + y ≥ 0</td><td>x &gt; N ∨ x + y ≥ 0</td></tr><tr><td>while (x ≥ N)<br>x = -2*x + 10;</td><td>x &gt; 5 ∨ x + y ≥ 0</td><td>x ≠ <sup>10</sup>&frasl;<sub>3</sub> ⇐⇒ true</td></tr><tr><td>//@ requires n &gt; 200<br>x = 0;<br>while (1)<br>if (x &lt; n) { x=x+y;<br>if (x ≥ 200) break; }</td><td>y &gt; 0</td><td>y&gt;0</td></tr></tbody></table>

# 6 Conclusions

We have presented several methods for deciding conditional termination of several classes of program loops manipulating integer variables. The universal termination problem has been found to be decidable for octagonal relations and linear affine loops with the finite monoid property. In other cases of linear affine loops, we give sufficient termination conditions. We have implemented our method in the FLATA tool [14] and performed a number of preliminary experiments.

*Acknowledgements* The authors would like to thank Eugene Asarin, Alexandre Donze, Hang Zhou, Mihai Moraru and Barbara Jobstmann for the insightful discussions on the matters of this paper, as well as the anonymous reviewers, for their interesting suggestions that led to improvements of our work.

# References

1. R. Bagnara, P. M. Hill, and E. Zaffanella. An improved tight closure algorithm for integer octagonal constraints. In *VMCAI'08*, pages 8–21, 2008.

2. B. Boigelot. *Symbolic Methods for Exploring Infinite State Spaces*, volume PhD Thesis, Vol. 189. Collection des Publications de l'Université de Liège, 1999.
3. A. Bouajjani, M. Bozga, P. Habermehl, R. Iosif, P. Moro, and T. Vojnar. Programs with lists are counter automata. In CAV'06, pages 517-531, 2006.

4. M. Bozga, C. Gîrlea, and R. Iosif. Iterating octagons. In TACAS'09, pages 337-351, 2009.

5. M. Bozga, R. Iosif, and F. Konečný. Fast acceleration of ultimately periodic relations. In CAV'10, pages 227-242, 2010.

6. M. Bozga, R. Iosif, and F. Konečný. Relational Analysis of Integer Programs. Technical Report TR-2011-14, Verimag, Grenoble, France, 2011.

7. M. Bozga, R. Iosif, and F. Konečný. Deciding Conditional Termination. Technical Report TR-2012-1, Verimag, Grenoble, France, 2012.

8. M. Bozga, R. Iosif, and Y. Lakhnech. Flat parametric counter automata. Fundamenta Informaticae, 91:275-303, 2009.

9. A. R. Bradley, Z. Manna, and H. B. Sipma. Linear ranking with reachability. In CAV'05, pages 491-504, 2005.

10. M. Braverman. Termination of integer linear programs. In CAV'06, pages 372-385, 2006.

11. B. Cook, S. Gulwani, T. Lev-Ami, A. Rybalchenko, and M. Sagiv. Proving conditional termination. In CAV'08, pages 328-340, 2008.

12. G. Everest. Recurrence sequences. American Mathematical Soc., 2003.

13. A. Finkel and J. Leroux. How to compose presburger-accelerations: Applications to broadcast protocols. In FST TCS'02, pages 145-156, 2002.

14. http://www-verimag.imag.fr/FLATA.html.

15. Ashutosh Gupta, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko, and Ru-Gang Xu. Proving non-termination. SIGPLAN Not., 43:147-158, 2008.

16. V. Halava, T. Harju, M. Hirvensalo, and J. Karhumaki. Skolem's problem – on the border between decidability and undecidability, 2005.

17. R. Iosif and A. Rogalewicz. Automata-based termination proofs. In CIAA'09, pages 165-177, 2009.

18. A. Podelski and A. Rybalchenko. A complete method for the synthesis of linear ranking functions. In VMCAI'04, 2004.

19. A. Podelski and A. Rybalchenko. Transition invariants. In LICS'04, pages 32-41, 2004.

20. B. De Schutter. On the ultimate behavior of the sequence of consecutive powers of a matrix in the max-plus algebra. Linear Algebra and its Applications, 307:103-117, 2000.

21. A. Smrcka and T. Vojnar. Verifying parametrised hardware designs via counter automata. In HVC'07, pages 51-68, 2007.

22. K. Sohn and A. Van Gelder. Termination detection in logic programs using argument sizes. In PODS'91, 1991.

23. A. Tiwari. Termination of linear programs. In CAV'04, pages 70-82, 2004.

24. A. M. Turing. On computable numbers, with an application to the entscheidungsproblem. Proceedings of the London Mathematical Society, 42:230-265, 1936.

25. A. Weber and H. Seidl. On finitely generated monoids of matrices with entries in $\mathbb{N}$. ITA'91, pages 19-38, 1991.
## A Proofs from Section 2

*Proof of Proposition 1* For each $i$ we have $S_i \subseteq \text{pre}_R(S_i) \subseteq \text{pre}_R(\bigcup_{j=0,1,...} S_j)$. The last inclusion is by the monotonicity of $\text{pre}_R$. Hence $\bigcup_{j=0,1,...} S_j \subseteq \text{pre}_R(\bigcup_{j=0,1,...} S_j)$. $\square$

*Proof of Lemma 1* By the Knaster-Tarski Fixpoint Theorem, $\text{gfp}(\text{pre}_R) = \bigcup\{S \mid S \subseteq \text{pre}_R(S)\} = \text{wrs}(R)$. $\square$

*Proof of Lemma 2* “wrs(R) ⊆ wnt(R)” Let $s_0 \in \text{wrs}(R)$ be a state. Then there exists $s_1 \in \text{wrs}(R)$ such that $\mathcal{R}(s_0, s_1)$. Applying this argument infinitely many times, one can construct an infinite sequence $s_0, s_1, s_2, ...$ such that $\mathcal{R}(s_i, s_{i+1})$, for all $i \ge 0$. Hence $s_0 \in \text{wnt}(R)$.

“wnt(R) ⊆ wrs(R)” Let $s_0 \in \text{wnt}(R)$. Then there exists an infinite sequence $s_0, s_1, s_2, ...$ such that $\mathcal{R}(s_i, s_{i+1})$ for all $i \ge 0$. Then, for all $i \ge 0$, $s_0 \in \text{pre}_R^i(s_i) \subseteq \text{pre}_R^i(\mathcal{D}^n)$, by monotonicity of $\text{pre}_R$. Hence $s_0 \in \bigcap_{i \ge 0} \text{pre}_R^i(\mathcal{D}^n) = \text{gfp}(\text{pre}_R)$. By Lemma 1, $s_0 \in \text{wrs}(R)$. $\square$

## B Proofs from Section 3

*Proof of Lemma* **??** [TODO] $\square$

*Proof of Theorem 1* [TODO] $\square$

*Proof of Lemma 7* “⇒” By the fact that $\mathcal{R} \leftarrow \mathcal{R}^{-m}(\top) \wedge \mathcal{R}$ and the monotonicity of wrs. “⇔” We prove the dual. Assume that $\text{wrs}(R) \neq \emptyset$ i.e., there exists an infinite sequence $s_1, s_2, ...$ such that $\mathcal{R}(s_i, s_{i+1})$, for all $i > 0$. Then all $s_i$ belong to the set defined by $\mathcal{R}^{-m}(\top)$, hence $s_1, s_2, ...$ is an infinite sequence for the relation defined by $\mathcal{R}^{-m}(\top) \wedge \mathcal{R}$ as well. $\square$

**Proposition 2.** Let $\{a_n\}_{n=0}^{\infty}$ and $\{b_n\}_{n=0}^{\infty}$ be sequences. Then the following hold:

- if $\inf\{\lfloor \frac{a_n}{2} \rfloor\}_{n=0}^{\infty} = -\infty$ then $\inf\{a_n\}_{n=0}^{\infty} = -\infty$

- if $\inf\{a_n + n b_n\}_{n=0}^{\infty} = -\infty$ then $\inf\{a_n\}_{n=0}^{\infty} = -\infty$ or $\inf\{b_n\}_{n=0}^{\infty} = -\infty$

- if $\inf\{\min(a_n, b_n)\}_{n=0}^{\infty} = -\infty$ then $\inf\{a_n\}_{n=0}^{\infty} = -\infty$ or $\inf\{b_n\}_{n=0}^{\infty} = -\infty$

*Proof.* By contraposition. Suppose that $\inf S_1 \neq -\infty$ and $\inf S_2 \neq -\infty$. Then, $\exists k_1 \ge 1$. $\forall l_1 \ge k_1$. $a_{k_1} = a_{l_1}$ and $\exists k_2 \ge 1$. $\forall l_2 \ge k_2$. $b_{k_2} = b_{l_2}$. Let $k = \max\{k_1, k_2\}$. Then clearly, $\forall l \ge k$. $\lfloor \frac{a_k}{2} \rfloor = \lfloor \frac{a_l}{2} \rfloor \wedge a_k + b_k = a_l + b_l \wedge \min\{a_k, b_k\} = \min\{a_l, b_l\}$. Hence $\inf S_l \neq -\infty$, $\inf S_p \neq -\infty$, and $\inf S_m \neq -\infty$. $\square$
**Proof of Lemma 8** Let $b$ and $c$ be the prefix and period of $R$. In Section 3 we proved that a $*$-consistent octagon $R$ is well-founded if and only if the closed form of the sequence ${\mathcal{R}}^{b+c\ell}_{\ell\ge 0}$ contains an atomic proposition of the form $u \le a_u\ell + d_u$, where $u \in U(\mathbf{x})$ is an octagonal term, and $a_u < 0$. We will show that the same holds if we use the closed form of the sequence ${\overline{\mathcal{R}}}^{b+c\ell}_{\ell\ge 0}$ instead. Notice that for any $k \ge 0$, the difference bounds encoding of $\mathcal{R}^{-k}(\top)$ is the projection of $m_{\mathcal{R}^k}^t$ on the entries corresponding to unprimed variables i.e., $(m_{\mathcal{R}^k}^t)_{\downarrow y}$. By the monotonicity of $\mathrm{pre}_R$, the sequence ${\{(m_{\mathcal{R}^k}^t)_{\downarrow y}\}_{k\ge 0}}$ is decreasing. Since the elements of the sequence are defined by (3), we can apply Proposition 2 and observe that if for some $1 \le i, j \le 2n$, $\inf\{(m_{\mathcal{R}^k}^t)_{i,j}\}_{k\ge 0} = -\infty$, then also $\inf\{(m_{\overline{\mathcal{R}}^k}^*)_{i_2,j_2}\}_{k\ge 0} = -\infty$ for some $(i_2, j_2) \in \{(i, j), (i, \bar{i}), (\bar{j}, j)\}$. Hence $R$ is well-founded iff there exists a negative coefficient $a_u$ in the closed form of ${\overline{\mathcal{R}}}^{b+c\ell}_{\ell\ge 0}$ iff $R_{db}$ is well founded. $\square$

**Definition 11.** The sequence ${g_k}_{k=0}^{\infty}$ is ultimately geometric if there exist $b \in \mathbb{N}_0$, $c \in \mathbb{N}$, and $\lambda \in \mathbb{Q}_{\infty}$ such that

$$ \forall k \ge 0, \forall s \in \{0, \dots, c-1\} \cdot g_{b+s+(k+1)c} = \lambda + g_{b+s+kc} $$

**Definition 12.** The sequence ${g_k}_{k=0}^{\infty}$ is ultimately periodic if there exist $b \in \mathbb{N}_0$, $c \in \mathbb{N}$, and $\lambda_0, \dots, \lambda_{c-1} \in \mathbb{Q}_{\infty}$ such that

$$ \forall k \ge 0, \forall s \in \{0, \dots, c-1\} \cdot g_{b+s+(k+1)c} = \lambda_s + g_{b+s+kc} $$

For the sake of completeness, we present key results of [20]. Let $G = (V, E, \nu : E \to \mathbb{Z})$ be a weighted digraph and $M_G$ the associated incidence matrix. Let $\mathcal{G}(V')$, $V' \subseteq V$ be a subgraph induced by $V'$. We say that $\mathcal{G}(V')$ is strongly connected if for any two different vertices $v_1, v_2 \in V'$, $v_1 \ne v_2$ there exists a path from $v_1$ to $v_2$. $\mathcal{G}(V')$ is a strongly connected component of $G$ if there is no $V' \subset V'' \subseteq V$ such that $\mathcal{G}(V'')$ is strongly connected.

Given a path $\pi : v_0 \xrightarrow{c_1} v_1 \xrightarrow{c_2} v_2 \dots v_{p-1} \xrightarrow{c_p} v_p$, the length of $\pi$ is $|\pi| = p$, the weight of $\pi$ is $w(\pi) = \sum_{i=1}^p c_i$, average weight of $\pi$ is $\frac{w(\pi)}{|\pi|}$. A cycle is a path where $v_0 = v_p$. A cycle of a strongly connected graph $G$ is critical if it has maximum average weight among all cycles of $G$.

A cycle of a strongly connected graph $G$ is critical if it has minimum average weight and cyclicity of $G$ is the greatest common divisor of lengths of critical cycles in $G$.

**Theorem 3.** (Theorem 2.4 in [20]) Let $G$ be a strongly connected digraph, $c$ its cyclic-ity and $\lambda$ the minimum average weight of critical cycles in $G$. Then, $M_G$ is ultimately geometric with period $c$ and rate $\Lambda$, where $\Lambda_{i,j} = c\lambda$ for all $i, j$.

**Theorem 4.** (Immediate corollary of Theorem 3.3 in [20]) Let $G$ be a digraph and let $\{c_1, \dots, c_m\}$ and $\{\lambda_1, \dots, \lambda_m\}$ be cyclicities and minimum average weights of critical cycles of strongly connected components of $G$. Then, $M_G$ is ultimately periodic with period $c = \text{lcm}(c_1, \dots, c_m)$ and rates $\{\Lambda'_0, \dots, \Lambda'_{c-1}\}$, where $(\Lambda'_k)_{i,j} \in \{c\lambda_1, \dots, c\lambda_m\}$ for all $0 \le k < c$ and for all $i, j$.
**Corollary 1.** Let $c$ be the period of a graph $G$ and let $v_1, v_2 \in V$ s.t. $(\Lambda_0)_{v_1, v_2} \neq \infty$. Then, there exists a critical cycle $\pi: v \rightsquigarrow v$ of length $p$ and paths $\pi_i: v_1 \rightsquigarrow v$ and $\pi_f: v \rightsquigarrow v_2$ s.t. $|\pi_i \cdot \pi_f| = b$, $\frac{w(\pi)}{p} = \frac{(\Lambda_0)_{v_1, v_2}}{c}$, and

$$ \forall k \geq 0. \ (M_G^{b+pk})_{v_1, v_2} = w(\pi_i) + ck \cdot w(\pi) + w(\pi_f) $$

*Proof.* Let $v_1, v_2 \in V$ be any pair of nodes s.t. $(\Lambda_0)_{v_1, v_2} \neq \infty$. Clearly, there exist paths of the form $\rho: v_1 \rightsquigarrow v_2$ s.t. $w(\rho) = (M_G^b)_{v_1, v_2}$ and $|\rho| = b$. Since $(\Lambda_0)_{v_1, v_2} \neq \infty$, one of these paths must cross a critical cycle $\pi$ (let denote $p = |\pi|$) which has, by Theorem 4, minimum average weight $\frac{w(\pi)}{p} = \frac{(\Lambda_0)_{v_1, v_2}}{c}$. Let $v$ be the node where $\rho$ crosses $\pi$ and let split $\rho$ into $\rho = \pi_1 \cdot \pi_2$ s.t. $\pi_1: v_1 \rightsquigarrow v$, and $\pi_2: v \rightsquigarrow v_2$. We next infer that for all $k \geq 0$,

$$ \begin{aligned} w(\pi_1) + w(\pi_1) + ck \cdot w(\pi) &= (M_G^b)_{v_1, v_2} + ck \cdot \frac{p}{c}(\Lambda_0)_{v_1, v_2} \\ &= (M_G^b)_{v_1, v_2} + pk \cdot (\Lambda_0)_{v_1, v_2} \\ &= (M_G^{b+pk})_{v_1, v_2} \end{aligned} $$

thus proving $\forall k \geq 0. (M_G^{b+pk})_{v_1, v_2} = w(\pi_i) + ckw(\pi) + w(\pi_f)$. Notice that since $\rho = \pi_1 \cdot \pi_2$ and $|\rho| = b$, then $|\pi_i \cdot \pi_f| = b$. $\square$

Notice that zigzag automaton can be viewed as a digraph and hence Theorems 3 and 4 apply to them. This means that difference bounds relations are ultimately periodic. Let $b, c, \Lambda_0, \dots, \Lambda_{c-1}$ be the prefix, period, and rates of $R$. Then, $b+2, c, \Lambda_0, \dots, \Lambda_{c-1}$ are the prefix, period, and rates of $M_R$, the incidence matrix of a zigzag automaton $A_R$. Moreover, the closed form of $\{R^{b+c\ell}\}_{\ell \geq 0}$ is

$$ R_{b,c}^{(l)} \equiv \bigwedge_{i \neq j} x_i - x_j \leq (\Lambda_0)_{I_{i,j}, F_{i,j}} \ell + (M_{R^b})_{i,j} \quad (9) $$

or, equivalently

$$ R_{b,c}^{(l)} \equiv \bigwedge_{i \neq j} x_i - x_j \leq (\Lambda_0)_{I_{i,j}, F_{i,j}} \ell + (M_{R^b})_{I_{i,j}, F_{i,j}} \quad (10) $$

*Proof of Lemma 9* By Lemma 3, if $R$ is $*$-consistent and well-founded, then in the closed form $R_{b,c}^{(l)} \equiv \bigwedge_{u \in U(\mathbf{x} \cup \mathbf{x}')}$ $u \leq a_u \ell + d_u$, there exists $u \in U(\mathbf{x})$ s.t. $a_u < 0$. By the Equation (9), $a_u = (\Lambda_0)_{I_{i,j}, F_{i,j}}$. By Corollary 1, there exists a cycle $\pi$ s.t. $w(\pi) = \frac{p}{c}(\Lambda_0)_{I_{i,j}, F_{i,j}} = \frac{p}{c}a_u$. Since $a_u < 0$ and $p, c > 0$, we infer that $w(\pi) < 0$. Other properties stated in this lemma follow immediately from Corollary 1. $\square$

*Proof of Lemma 10* By Lemma 9, there is a negative critical cycle $\pi$ of length $p$ in the zigzag automaton: $q_1 \xrightarrow{G_1} q_2 \dots q_p \xrightarrow{G_p} q_1$. Let $G_j = (\mathbf{x} \cup \mathbf{x}', E_j)$ for all $1 \leq j \leq p$.

Consider the following sum of all constraints represented by edges appearing in the zigzag cycle (note that the sum of weights of these edges equals $w(\pi)$):

$$ \sum_{1 \leq j \leq p} \left( \sum_{(x_i \to x'_j) \in E_j} (x_i - x'_j) + \sum_{(x'_i \to x_j) \in E_j} (x'_i - x_j) \right) \leq w(\pi) \quad (11) $$
The left-hand side of (11) can be written equivalently as

$$ \sum_{1 \le j \le p} \left( \sum_{\substack{1 \le i \le n, \\ (q_j)_i = r}} (x_i - x'_i) + \sum_{\substack{1 \le i \le n, \\ (q_j)_i = l}} (-x_i + x'_i) + \sum_{\substack{1 \le i \le n, \\ (q_j)_i = lr}} (-x_i + x'_i) + \sum_{\substack{1 \le i \le n, \\ (q_j)_i = rl}} (-x'_i + x'_i) \right) \quad (12) $$

and thus, after simplifications ($-x_i+x_i = 0, -x'_i+x'_i = 0$), (11) can be written equivalently as

$$ \sum_{1 \le j \le p} \left( \sum_{\substack{1 \le i \le n, \\ (q_j)_i = r}} (x_i - x'_i) + \sum_{\substack{1 \le i \le n, \\ (q_j)_i = l}} (-x_i + x'_i) \right) \le w(\pi) \quad (13) $$

Let $f$ denote the negated sum of all unprimed terms in (12) and $f'$ denote the negated sum of all primed terms in (12). Then, clearly $f' = -f[x'/x]$. Thus, (13) can be written as

$$ f' - f \le w(\pi) \quad (14) $$

Notice that since $w(\pi) < 0$, we establish that $f' - f < 0$ hence $f$ is strictly decreasing. Since, for all states $s, s'$ we have $\mathcal{R}(s, s') \to f(s) > f'(s)$, we have that $\mathcal{R}^{-b}(\top)(s) \wedge \mathcal{R}(s, s') \to f(s) > f'(s)$. $\square$

**Lemma 15.** Let $R$ be a $*$-consistent octagonal relation with prefix $b$ and period $c$. Then, for any $1 \le i, j \le 2n$ and $k \ge 1$, we have $(m_{\mathcal{R}^{-k}(\top)})_{i,j} < \infty \to (m_{\mathcal{R}^{-b}(\top)})_{i,j} < \infty$.

*Proof.* (Case $1 \le k \le b$) By monotonicity of $pre_R$, $(m_{\mathcal{R}^{-k}(\top)})_{i,j} \ge (m_{\mathcal{R}^{-b}(\top)})_{i,j}$. Thus if $(m_{\mathcal{R}^{-k}(\top)})_{i,j} \ne \infty$, then clearly $(m_{\mathcal{R}^{-b}(\top)})_{i,j} < \infty$.

(Case $k > b$) Let $p = \lfloor \frac{k-b}{c} \rfloor$, and $k' = b + pc$. Note that $\mathcal{R}^{k'} = \mathcal{R}_{b,c}^{(\ell)}[p/\ell]$. Since $k' \ge k$, by the same argument as for case ($1 \le k \le b$), $(m_{\mathcal{R}^{-k'}(\top)})_{i,j} < \infty$. Since $\mathcal{R}_{b,c}^{(\ell)}$ is closed, $y_i - y_j \le a\ell + d$, where $a, d \in \mathbb{Z}$, is one of its conjuncts. Since $\mathcal{R}_{b,c}^{(\ell)}$ is closed, $(m_{\mathcal{R}^{-b}(\top)})_{i,j} = d \ne \infty$. $\square$

*Proof of Lemma 11* Let $f$ be a linear decreasing function from Lemma 10. Let $\pi : q_1 \xrightarrow{G_1} q_2 \dots q_p \xrightarrow{G_p} q_1$ be the negative cycle used to construct $f$, and $\pi_f$ be the suffix from Lemma 10. By construction of the zigzag automaton, for any $1 \le j \le p$,

$$ |\{i | (q_j)_i = r\}| = |\{i | (q_j)_i = l\}| $$

It follows from (13) that each $(q_j)_i = r$ contributes to $f$ with a term $-x_i$ and that each $(q_j)_i = l$ contributes to $f$ with a term $+x_i$ and that each $(q_j)_i \notin \{r, l\}$ doesn't contribute at all. We now demonstrate that for each $1 \le j \le p$, there exists a bijective matching $\beta_j : \{i | (q_j)_i = r\} \to \{i | (q_j)_i = l\}$ such that for any $1 \le i_1 \le n$ s.t. $\beta_j(i_1) = i_2$, the difference $x_{i_2} - x_{i_1}$ is bounded in $\mathcal{R}^{-b}(\top) \wedge \mathcal{R}$, formally $\mathcal{R}^{-b}(\top) \wedge \mathcal{R} \to (x_{i_2} - x_{i_1} \ge h)$ for some $h \in \mathbb{Z}$.

Let $j \in \{1, \dots, p\}$. By construction of the zigzag automaton, the concatenated graph $G_j G_{j+1} \dots G_p \pi_f$ connects each $(q_j)_{i_1}$ s.t. $(q_j)_{i_1} = r$ with a unique $(q_j)_{i_2}$ s.t. $(q_j)_{i_2} = l$. This induces the required bijection $\beta_j$. Since $G_j G_{j+1} \dots G_p \pi_f$ is a subgraph of $G_R^{p+|\pi_f|}$, it follows that there is a path $\mathbf{x}_{i_1}^{(0)} \rightsquigarrow \mathbf{x}_{i_2}^{(0)}$ in $G_R^{p+|\pi_f|}$, in other words,
$\mathbb{R}^{p+|\pi_f|} \to x_{i_1} - x_{i_2} \le h$ for some $h \in \mathbb{Z}$. By Lemma 15, $\mathbb{R}^b \to x_{i_1} - x_{i_2} \le h'$ for some $h' \in \mathbb{Z}$ too.

Clearly, $\mathbb{R}^{-b}(\mathbb{T}) \wedge \mathbb{R} \to x_{i_1} - x_{i_2} \le h'$ too. Since $x_{i_1} - x_{i_2} \le h'$ if and only if $x_{i_2} - x_{i_1} \ge -h'$, we obtain the required property.

Now since $f = \sum_{1 \le j \le p} \sum_{\substack{1 \le i_1, i_2 \le n \\ \beta_j(i_1)=i_2}} (x_{i_2} - x_{i_1})$ and since we proved that each of the differences $x_{i_2} - x_{i_1}$ in the sum is bounded in $\mathbb{R}^{-b}(\mathbb{T}) \wedge \mathbb{R}$, it follows that $f$ is bounded in $\mathbb{R}^{-b}(\mathbb{T}) \wedge \mathbb{R}$ too, formally $\mathbb{R}^{-b}(\mathbb{T}) \wedge \mathbb{R} \to (f \ge h)$ for some $h \in \mathbb{Z}$. $\square$

### C Proofs from Section 4

**Definition 13.** A function $f: \mathbb{N} \to \mathbb{C}$ is said to be a C-finite recurrence if and only if:

$$f(m+d) = a_{d-1}f(m+d-1) + \dots + a_1f(m+1) + a_0f(n), \forall m \ge 0$$

for some $d \in \mathbb{N}$ and $a_0, a_1, \dots, a_{d-1} \in \mathbb{C}$, with $a_{d-1} \neq 0$. The polynomial $x^d - a_{d-1}x^{d-1} - \dots a_1x - a_0$ is called the characteristic polynomial of $f$.

A C-finite recurrence always admits a closed form.

**Theorem 5 ([12].)** The closed form of a C-finite recurrence is:

$$f(m) = p_1(m)\lambda_1^m + \dots + p_s(m)\lambda_s^m$$

where $\lambda_1, \dots, \lambda_s \in \mathbb{C}$ are non-zero distinct roots of the characteristic polynomial of $f$, and $p_1, \dots, p_s \in \mathbb{C}[m]$ are polynomials of degree less than the multiplicities of $\lambda_1, \dots, \lambda_s$, respectively.

Next, we define the closed form for the sequence of powers of A.

**Corollary 2.** Given a square matrix $A \in \mathbb{Z}^{n \times n}$, we have:

$$(A^m)_{i,j} = p_{1,i,j}(m)\lambda_1^m + \dots + p_{s,i,j}(m)\lambda_s^m$$

where $\lambda_1, \dots, \lambda_s \in \mathbb{C}$ are non-zero distinct eigenvalues of $A$, and $p_{1,i,j}, \dots, p_{s,i,j} \in \mathbb{C}[m]$ are polynomials of degree less than the multiplicities of $\lambda_1, \dots, \lambda_s$, respectively.

*Proof.* If $\det(A-xI_n) = x^d - a_{d-1}x^{d-1} - \dots - a_1x - a_0$ is the characteristic polynomial of $A$, then we have

$$A^d - a_{d-1}A^{d-1} - \dots - a_1A - a_0 = 0$$

by the Cayley-Hamilton Theorem. If we define $f_{i,j}(m) = (A^m)_{i,j}$, then we have

$$x A^{m+d} = a_{d-1} A^{m+d-1} + \dots + a_1 A^{m+1} + a_0 A^m \\ f_{i,j}(m+d) = a_{d-1} f_{i,j}(m+d-1) + \dots + a_1 f_{i,j}(m+1) + a_0 f_{i,j}(m)$$

By Theorem 5, we have that

$$(A^m)_{i,j} = p_{1,i,j}(m)\lambda_1^m + \dots + p_{s,i,j}(m)\lambda_s^m$$

for some polynomials $p_{1,i,j}, \dots, p_{s,i,j} \in \mathbb{C}[m]$ of degrees less than the multiplicities of $\lambda_1, \dots, \lambda_s$, respectively. $\square$
**Proof of Lemma 13** Assume from now on that all non-zero eigenvalues $\lambda_1, \dots, \lambda_s$ of $A$ are such that $\lambda_1^{d_1} = \dots = \lambda_s^{d_s} = 1$, for some integers $d_1, \dots, d_s > 0$. The method given in [2] for testing the finite monoid condition for $A$ gives also bounds for $d_1, \dots, d_s$. Then we have $\lambda_1^L = \dots = \lambda_s^L = 1$, where $L = \text{lcm}(d_1, \dots, d_s)$. As $d_1, \dots, d_s$ are effectively bounded, so is $L$. By Corollary 2, we have that, if $m$ is a multiple of $L$, then $(A^m)_{i,j} = p_{i,j}(m)$ for some effectively computable polynomial $p_{i,j} \in \mathbb{C}[m]$ i.e., for $m$ multiple of $L$, $A^m$ is polynomially definable. But since $p_{i,j}(m)$ assumes real values in an infinity of points $m = kL, k > 0$, the it must be that its coefficients are all real numbers, i.e. $p_{i,j} \in \mathbb{R}[m]$. Moreover, these coefficients are the solutions of the integer system:

$$ \left\{ \begin{array}{l} p_{i,j}(L) = (A^L)_{i,j} \\ \dots \\ p_{i,j}((d+1)L) = (A^{(d+1)L})_{i,j} \end{array} \right. $$

Clearly, since $A \in \mathbb{Z}^{n \times n}$, $A^p \in \mathbb{Z}^{n \times n}$, for any $p \ge 0$. Hence $p_{i,j} \in \mathbb{Q}[m]$. $\square$

**Proof of Lemma 14** Assuming the condition $a_{d-i}(\mathbf{x}) < 0$ and $a_d(\mathbf{x}) = a_{d-1}(\mathbf{x}) = \dots = a_{d-i+1}(\mathbf{x}) = 0$, for some $0 \le i \le d$, we have $P(k, \mathbf{x}) = a_{d-i}(\mathbf{x}) \cdot k^d + \dots + a_1(\mathbf{x}) \cdot k + a_0(\mathbf{x})$. Since the dominant coefficient $a_{d-i}(\mathbf{x})$ is negative, the polynomial will assume only negative values, from some point on. $\square$