Reflections on Termination of Linear Loops

Abstract

This paper shows how techniques for linear dynamical systems can be used to reason about the behavior of general loops. We present two main results. First, we show that every loop that can be expressed as a transition formula in linear integer arithmetic has a best model as a deterministic affine transition system. Second, we show that for any linear dynamical system f with integer eigenvalues and any integer arithmetic formula G, there is a linear integer arithmetic formula that holds exactly for the states of f for which G is eventually invariant. Combining the two, we develop a monotone conditional termination analysis for general loops.

1 Introduction

Linear and affine dynamical systems are a model of computation that is easy to analyze (relative to non-linear systems), making them useful across a broad array of applications. In the context of program analysis, affine dynamical systems correspond to loops of the form

where G is a formula, A is a matrix, $\mathbf {x}$ is a vector of program variables, and $\mathbf {b}$ is a constant vector. The termination problem for such loops has been shown to be decidable for several variations of this model [4, 9, 12, 24, 29]. However, few loops in real programs take this form, and so this work has not yet made an impact on practical termination analysis tools. This paper bridges the gap between theory and practice, showing how techniques for linear and affine dynamical systems can be used to reason about general programs.

Example 1

We illustrate our methodology using the example program in Fig. 1 (left). First, observe that although the body of this loop is not of the form ($\dagger$), the value of the sum $x+y$ decreases by z each iteration, and z remains the same. Thus, we can approximate the loop by the linear dynamical system in Fig. 1 (right), where the nature of the approximation is given by the linear map in the center of Fig. 1 (i.e., the a coordinate corresponds to $x+y$, and the b coordinate to z). The linear map is a simulation, in the sense that it transforms the state space of the program into the state space of the linear dynamical system so that every step in the loop has a corresponding step in the linear dynamical system.

Next, we compute the image of the guard of the loop ($x \ge 0 \wedge y \ge 0$) under the simulation, which yields $a \ge 0$ (corresponding to the constraint $x + y \ge 0$ over the original program variables). We can compute a closed form for this constraint holding on the kth iteration of the loop by exponentiating the dynamics matrix of the linear dynamical system, multiplying on the left by the row vector corresponding to the constraint, and on the right by the simulation:

$$\underbrace{\begin{bmatrix}1&0\end{bmatrix}}_{\text {Constraint}}\underbrace{\begin{bmatrix} 1 &{} -1\\ 0 &{} 1 \end{bmatrix}^k}_{\text {Dynamics}}\underbrace{\begin{bmatrix} 0 &{} 1 &{} 1 &{} 0\\ 0 &{} 0 &{} 0 &{} 1\end{bmatrix}}_{\text {Simulation}}\begin{bmatrix}w\\ x\\ y\\ z\end{bmatrix} = (x+y) - kz. $$

We then analyze the asymptotic behavior of the closed form:

$$ \text {As } k \rightarrow \infty , (x+y) - kz \rightarrow {\left\{ \begin{array}{ll} -\infty &{} \text {if } z > 0\\ x+y &{} \text {if } z = 0\\ \infty &{} \text {if } z < 0 \end{array}\right. } $$

We conclude that $z > 0 \vee (x+y) < 0$ is a sufficient condition for the loop to terminate.    

Fig. 1.

Over-approximation of a loop by a linear dynamical system.

The paper is organized as follows. To serve as the class of “linear models” of loops, we introduce deterministic affine transition systems (DATS), a computational model that generalizes affine dynamical systems. Sect. 3 shows that any loop expressed as a linear integer arithmetic formula has a DATS-reflection, which is a best representation of the behavior of the loop as a DATS. Moreover, this holds for a restricted class of DATS with rational eigenvalues. Section 4 shows that for a linear map f with integer eigenvalues and a linear integer arithmetic formula G, there is a linear integer arithmetic formula that holds exactly for those states x such that $G(f^k(x))$ holds for all but finitely many $k \in \mathbb {N}$. Section 5 brings the results together, showing that the analysis of a DATS with rational eigenvalues can be reduced to the analysis of a linear dynamical system with integer eigenvalues. The fact that DATS-reflections are best implies monotonicity of the analysis. Finally, in Sect. 6, we demonstrate experimentally that the analysis can be successfully applied to general programs, using the framework of algebraic termination analysis [34] to lift our loop analysis to a whole-program conditional termination analysis. Some proofs are omitted for space, but may be found in the extended version of this paper [33].

2 Preliminaries

This paper assumes familiarity with linear algebra – see for example [19]. We recall some basic definitions below.

In the following, a linear space refers to a finite-dimensional linear space over the field of rational numbers $\mathbb {Q}$. For V a linear space and $U \subseteq V$, $\textit{span}(U)$ is the linear space generated by U; i.e., the smallest linear subspace of V that contains U. An affine subspace of a linear space V is the image of a linear subspace of V under a translation (i.e., a set of the form $\{ v + v_0 : v \in U \}$ for some linear subspace $U \subseteq V$ and some $v_0 \in V$). For any scalar $a \in \mathbb {Q}$, and any linear space V, we use $\underline{a}$ to denote the linear map $\underline{a} : V \rightarrow V$ that maps $v \mapsto av$ (in particular, $\underline{1}$ is the identity). A linear functional on a linear space V is a linear map $V \rightarrow \mathbb {Q}$; the set of all linear functionals on V forms a linear space called the dual space of V, denoted $V^\star$. A linear map $f : V_1 \rightarrow V_2$ induces a dual linear map $f^\star : V_2^\star \rightarrow V_1^\star$ where $f^\star (g) \triangleq g \circ f$. For any linear space V, V is naturally isomorphic to $V^\star {}^\star$, where the isomorphism maps $x \mapsto \lambda f : V^\star . f(x)$.

Let V be a linear space. A linear map $f : V \rightarrow V$ is associated with a characteristic polynomial $p_f(x)$, which is defined to be the determinant of $(xI - A_f)$, where $A_f$ is a matrix representation of f with respect to some basis (the choice of which is irrelevant). Define the spectrum (set of eigenvalues) of f to be the set of (possibly complex) roots of its characteristic polynomial, $\textit{spec}(f) \triangleq \{ \lambda \in \mathbb {C} : p_f(\lambda ) = 0 \}$. We say that f has rational spectrum if $\textit{spec}(f) \subseteq \mathbb {Q}$; equivalently (by the spectral theorem – see e.g. [19, Ch. 6, Theorem 7]):

• There is a basis $\{x_1,...,x_n\}$ for V consisting of generalized (right) eigenvectors, satisfying $(f - \underline{\lambda _i})^{r_i}(x_i) = 0$ for some $\lambda _i \in \textit{spec}(f)$ and some $r_i \ge 1$ ($r_i$ is called the rank of $x_i$)

• There is a basis $\{g_1,...,g_n\}$ for $V^\star$ consisting of generalized left eigenvectors, satisfying $g_i \circ (f - \underline{\lambda _i})^{r_i} = 0$ for some $\lambda _i \in \textit{spec}(f)$ and some $r_i \ge 1$

It is possible to determine whether a linear map has rational spectrum (and compute the basis of eigenvectors for V and $V^\star$) in polynomial time by computing its characteristic polynomial [15], factoring it [22], and checking whether each factor is linear.

The syntax of linear integer arithmetic (LIA) is given as follows:

$$\begin{aligned} x \in \textsf {Variable}\\ n \in \mathbb {Z}\\ t \in \textsf {Term}&{::=}\ x \mid n \mid n \cdot t \mid t_1 + t_2\\ F \in \textsf {Formula}&{::=}\ t_1 \le t_2 \mid (n\mid t) \mid F_1 \wedge F_2 \mid F_1 \vee F_2 \mid \lnot F \mid \exists x. F \mid \forall x. F \end{aligned}$$

Let $X \subseteq \textsf {Variable}$ be a set of variables. A valuation over X is a map $v : X \rightarrow \mathbb {Z}$. If F is a formula whose free variables range over X and v is a valuation over X, then we say that v satisfies F (written $v \models F$) if the formula F is true when interpreted over the standard model of the integers, using v to interpret the free variables. We write $F \models G$ if every valuation that satisfies F also satisfies G.

2.1 Transition Systems

A transition system T is a pair $T = \left\langle S_T, R_T \right\rangle$ where $S_T$ is a set of states and $R_T \subseteq S_T \times S_T$ is a transition relation. Within this paper, we shall assume that the state space of any transition system is a finite-dimensional linear space (over $\mathbb {Q}$). We write $x \rightarrow _{T} x'$ to denote that the pair $\left\langle x,x' \right\rangle$ belongs to $R_T$. We define the domain of a transition system T, $\text {dom}(T) \triangleq \{ x \in S_T : \exists x'. x \rightarrow _{T} x' \}$, to be the set of states that have a T-successor. We define the $\omega$-domain $\text {dom}^\omega (T)$ of T to be the set of states from which there exist infinite T-computations:

$$\begin{aligned} \text {dom}^\omega (T) \triangleq \left\{ x_0 \in S_T : \exists x_1,x_2,... \text { such that } x_0 \rightarrow _{T} x_1 \rightarrow _{T} x_2 \rightarrow _{T} \cdots \right\} \ . \end{aligned}$$

A transition formula $F(X,X')$ is an LIA formula whose free variables range over a designated finite set of variables X and a set of “primed copies” $X' = \{ x' : x \in X\}$. For example, a transition formula that represents the body of the loop in Fig. 1 is

$$\begin{aligned} \begin{array}{ll} &{}x \ge 0 \wedge y \ge 0 \wedge w' = 3w + x + 1 \wedge z' = z\\ \wedge &{} \left( \begin{array}{ll} &{}((2 \mid x-y) \wedge x' = x - z \wedge y' = y)\\ \vee &{}(\lnot (2 \mid x-y) \wedge y' = y - z \wedge x' = x) \end{array}\right) \end{array} \end{aligned}$$

(1)

We use $\mathbf{TF} {}$ to denote the set of transition formulas. A transition formula $F(X,X')$ defines a transition system where the state space is the set of functions $X \rightarrow \mathbb {Q}$, and where $v \rightarrow _F v'$ if and only if both (1) v and $v'$ map each $x \in X$ to an integer and (2) $[v,v'] \models F$, where $[v,v']$ denotes the valuation that maps each $x \in X$ to v(x) and each $x' \in S'$ to $v'(x)$. Defining the state space of F to be $X \rightarrow \mathbb {Q}$ rather than $X \rightarrow \mathbb {Z}$ is a technical convenience ($X \rightarrow \mathbb {Q} \cong \mathbb {Q}^{|X|}$ is a linear space), but does not materially affect the results of this paper since only (integral) valuations are involved in transitions.

Let $T = \left\langle S_T,R_T \right\rangle$ be a transition system. We say that T is:

• linear if $R_T$ is a linear subspace of $S_T \times S_T$,

• affine if $R_T$ is an affine subspace of $S_T \times S_T$,

• deterministic if $x \rightarrow _{T} x_1'$ and $x \rightarrow _{T} x_2'$ implies $x_1' = x_2'$

• total if for all $x \in S_T$ there exists some $x' \in S_T$ with $x \rightarrow _{T} x'$

For example, the transition system T with transition relation

$$ R_T \triangleq \left\{ \left\langle \begin{bmatrix}x\\ y\end{bmatrix},\begin{bmatrix}x'\\ y'\end{bmatrix} \right\rangle : \begin{bmatrix}1 &{} 0 \\ 0 &{} 1\\ 0 &{} 0\end{bmatrix}\begin{bmatrix}x'\\ y'\end{bmatrix} = \begin{bmatrix}2 &{} 1\\ 0 &{} 1 \\ 0 &{} 1\end{bmatrix}\begin{bmatrix}x\\ y\end{bmatrix} + \begin{bmatrix}0\\ 0\\ 1\end{bmatrix} \right\} $$

is deterministic and affine, but not linear or total. The transition system U with transition relation

$$ R_U \triangleq \left\{ \left\langle \begin{bmatrix}x\\ y\end{bmatrix},\begin{bmatrix}x'\\ y'\end{bmatrix} \right\rangle : \begin{bmatrix}1&1\end{bmatrix}\begin{bmatrix}x'\\ y'\end{bmatrix} = \begin{bmatrix}\frac{1}{2}&\frac{1}{2}\end{bmatrix}\begin{bmatrix}x\\ y\end{bmatrix} \right\} $$

is total, linear (and affine), but not deterministic. The classical notion of a linear dynamical system—a transition system where the state evolves according to a linear map—corresponds to a total, deterministic, linear transition system. Similarly, an affine dynamical system is a transition system that is total, deterministic, and affine.

For any map $s : X \rightarrow Y$, and any relation $R \subseteq X \times X$, define the image of R under s to be the relation $s[R] = \left\{ \left\langle s(x),s(x') \right\rangle : \left\langle x,x' \right\rangle \in R \right\}$. For any relation $R \subseteq Y \times Y$, define the inverse image of R under s to be the relation $s^{-1}[R] = \left\{ \left\langle x,x' \right\rangle : \left\langle s(x),s(x') \right\rangle \in R \right\}$. Let $T = \left\langle S_T,R_T \right\rangle$ and $U = \left\langle S_U,R_U \right\rangle$ be transition systems. We say that a linear map $s : S_T \rightarrow S_U$ is a linear simulation from T to U, and write $s : T \rightarrow U$, if for all $x \rightarrow _{T} x'$, we have $s(x) \rightarrow _{U} s(x')$. Observe that the following are equivalent: (1) s is a simulation, (2) $s[R_T] \subseteq R_U$, and (3) $R_T \subseteq s^{-1}[R_U]$.

An example of a simulation between a transition formula and a linear dynamical system is given in Fig. 1. In fact, there are many linear dynamical systems that over-approximate this loop; however, the simulation and linear dynamical system given in Fig. 1 is its best abstraction.

To formalize the meaning of best abstractions, it is convenient to use the language of category theory [17]. Any class of transition systems defines a category, where the objects are transitions systems of that class, and the arrows are linear simulations between them. We use boldface letters (Linear, Affine, Deterministic, Total) to denote categories of transition systems (e.g., $\mathbf {DATS}$ denotes the category of Deterministic Affine Transition Systems).

If T is a transition system and $\mathbf {C}$ is a category of transition systems, a $\mathbf {C}$-abstraction of T is a pair $\left\langle U,s \right\rangle$ consisting of a transition system U belonging to $\mathbf {C}$ and a linear simulation $s : T \rightarrow U$. A $\mathbf{C}$-reflection of T is a $\mathbf {C}$-abstraction that satisfies a universal property among $\mathbf{C}$-abstractions of T: for any $\mathbf {C}$-abstraction $\left\langle V,t \right\rangle$ of T there exists a unique simulation $\overline{t} : U \rightarrow V$ such that $\overline{t} \circ s = t$; i.e., the following diagram commutes:

If $\mathbf {D}$ is a category of transition systems and $\mathbf {C}$ is a subcategory such that every transition system in $\mathbf {D}$ has a $\mathbf {C}$-reflection, we say that $\mathbf {C}$ is a reflective subcategory of $\mathbf {D}$.

Our ultimate goal is to bring techniques from linear dynamical systems to bear on transition formulas. Fig. 1 gives an example of a program and its linear dynamical system reflection. Unfortunately, such reflections do not exist for all transition formulas, which motivates our investigation of alternative models.

Proposition 1

The transition formula $x' = x \wedge x = 0$ has no $\mathbf {TDATS}$-reflection.

Proof

Let F be the 1-dimensional transition formula $x' = x \wedge x = 0$. For a contradiction, suppose that $\left\langle A,s \right\rangle$ is a $\mathbf {TDATS}$-reflection of F. Since F contains the origin, then so must the transition relation of A, and so A is linear. Next, consider that for any $\lambda \in \mathbb {Q}$, we have the simulation $\textit{id} : F \rightarrow A_\lambda$, where $\textit{id}$ is the identity function and $A_\lambda = \left\langle \mathbb {Q},x \mapsto \lambda x \right\rangle$. Since $\left\langle A,s \right\rangle$ is a reflection of F, for any $\lambda$, there is some $t_\lambda$ such that $t_\lambda : A \rightarrow A_\lambda$ and $\textit{id} = t_\lambda \circ s$. Since $t_\lambda$ is a simulation, we have $\lambda t_\lambda = A_\lambda \circ t_\lambda = t_\lambda \circ A$. Since $\textit{id} = t_\lambda \circ s$, we must have $t_\lambda$ non-zero, and so $t_\lambda$ is a left eigenvector of A with eigenvalue $\lambda$. Since this holds for all $\lambda$, A must have infinitely many eigenvalues, a contradiction.

3 Linear Abstractions of Transition Formulas

Proposition 1 shows that not every transition formula has a total deterministic affine reflection. In the following we show that totality is the only barrier: every transition formula has a (computable) $\mathbf {DATS}{}$-reflection. Moreover, we show that every transition formula has a rational spectrum $\mathbf {DATS}{}$ ($\mathbb {Q}\text {-}\mathbf {DATS}$)-reflection, a restricted class of $\mathbf {DATS}{}$ that generalizes affine maps $x \mapsto A\mathbf {x} + \mathbf {b}$ where A has rational eigenvalues. The restriction on eigenvalues makes it easier to reason about the termination behavior of $\mathbb {Q}\text {-}\mathbf {DATS}$.

In the remainder of this section, we show that every transition formula has a $\mathbb {Q}\text {-}\mathbf {DATS}{}$-reflection by establishing a chain of reflective subcategories:

The fact that $\mathbb {Q}\text {-}\mathbf {DATS}{}$ is a reflective subcategory of $\mathbf {TF}$ then follows from the fact that a reflective subcategory of a reflective subcategory is reflective.

3.1 Affine Abstractions of Transition Formulas

Let $F(X,X')$ be a transition formula. The affine hull of F, denoted $\textit{aff}(F)$, is the smallest affine set $\textit{aff}(F) \subseteq (X \cup X') \rightarrow \mathbb {Q} \cong (X \rightarrow \mathbb {Q}) \times (X \rightarrow \mathbb {Q})$ that contains all of the models of F. Reps et al. give an algorithm that can be used to compute $\textit{aff}(F)$, by using an SMT solver to sample a set of generators [26].

Lemma 1

Let $F(X,X')$ be a transition formula. The affine hull of F (considered as a transition system) is the best affine abstraction of F (where the simulation from F to $\textit{aff}(F)$ is the identity).

Example 2

Consider the example program in Fig. 1. Letting F denote the transition formula corresponding to the program, $\textit{aff}(F)$ can be represented as the solutions to the constraints

$$\begin{aligned} \begin{bmatrix} 1 &{} 0 &{} 0 &{} 0\\ 0 &{} 1 &{} 1 &{} 0\\ 0 &{} 0 &{} 0 &{} 1 \end{bmatrix} \begin{bmatrix} w'\\ x'\\ y'\\ z'\\ \end{bmatrix} = \begin{bmatrix} 3 &{} 1 &{} 0 &{} 0\\ 0 &{} 1 &{} 1 &{} -1\\ 0 &{} 0 &{} 0 &{} 1 \end{bmatrix} \begin{bmatrix} w\\ x\\ y\\ z\\ \end{bmatrix} + \begin{bmatrix} 1\\ 0\\ 0\\ 0 \end{bmatrix} \end{aligned}$$

(2)

Notice that $\textit{aff}(F)$ is 4-dimensional and has a transition relation defined by 3 constraints, and thus is not deterministic. The next step is to find a suitable projection onto a lower-dimensional space so that the resulting transition system is deterministic.

3.2 Reflections via the Dual Space

This section presents a key technical tool that will be used in the next two subsections to prove the existence of reflections. For any transition system T, an abstraction $\left\langle U,s \right\rangle$ of T consisting of a transition system U and a simulation $s : S_T \rightarrow S_U$ induces a subspace of $S_T^\star$, which is the range of the dual map $s^\star$ (i.e., the set of all linear functionals on $S_T$ of the form $g \circ s$ where $g \in S_U^\star$). The essential idea is we can apply this in reverse: any subspace $\varLambda$ of $S_T^\star$ induces a transition system U and a simulation $s : T \rightarrow U$ that satisfies a universal property among all abstractions $\left\langle V,v \right\rangle$ of T where the range of $v^\star$ is contained in $\varLambda$. We will now formalize this idea.

Let T be a transition system, and let $\varLambda$ be a subspace of $S_T^\star$. Define $\alpha _\varLambda (T)$ to be the pair $\alpha _\varLambda (T) \triangleq \left\langle U,s \right\rangle$ consisting of a transition system U and a linear simulation $s : T \rightarrow U$ where

• $s : S_T \rightarrow \varLambda ^\star$ sends each $x \in S_T$ to $\lambda f : \varLambda . f(x)$

• $S_U \triangleq \varLambda ^\star$, and $R_U \triangleq s[R_T] = \left\{ \left\langle s(x),s(x') \right\rangle : \left\langle x,x' \right\rangle \in R_T \right\}$

Lemma 2

(Dual space simulation). Let T be a transition system, let $\varLambda$ be a subspace of $S_T^\star$, and let $\left\langle U,s \right\rangle = \alpha _\varLambda (T)$. Suppose that Z is a transition system and $z : T \rightarrow Z$ is a simulation such that the range of $z^\star$ is contained in $\varLambda$. Then there exists a unique simulation $\overline{z} : U \rightarrow Z$ such that $\overline{z} \circ s = z$.

Proof

The high-level intuition is that since the range of $z^\star$ is contained in $\varLambda$, we may consider it to be a map $z^\star : S_Z^\star \rightarrow \varLambda$; dualizing again, we get a map $z^\star {}^\star : \varLambda ^\star \rightarrow S_Z^{\star \star }$, whose domain is $S_U$ and codomain is (isomorphic to) $S_Z$.

More formally, let $j : S_Z \rightarrow S_Z^{\star \star }$ be the natural isomorphism between $S_Z$ and $S_Z^{\star \star }$ defined by $j(y) \triangleq \lambda g : S_Z^\star . g(y)$. Define $\overline{z} : \varLambda ^\star \rightarrow S_Z$ by

$$\begin{aligned} \overline{z}(h) \triangleq j^{-1}(\lambda g : S_Z^\star . h(g \circ z))\ . \end{aligned}$$

First we show that $\overline{z} \circ s = z$. Let $x \in S_Z$. Then we have

$$\begin{aligned} (\overline{z} \circ s)(x)&= \overline{z}(s(x))\\&= j^{-1}(\lambda g : S_Z^\star . (s(x))(g \circ z))\\&= j^{-1}(\lambda g : S_Z^\star . (\lambda f : \varLambda . f(x))(g \circ z))\\&= j^{-1}(\lambda g : S_Z^\star . g(z(x)))\\&= z(x)\ . \end{aligned}$$

Next we show that $\overline{z}$ is a simulation. Suppose $y \rightarrow _{U} y'$. Since $R_{U} = s[R_T]$, there is some $x,x' \in S_T$ such that $x \rightarrow _{T} x'$, $s(x) = y$, and $s(x') = y'$. Since $z : T \rightarrow Z$ is a simulation, we have that $z(x) \rightarrow _{Z} z(x)$, and so $\overline{z}(s(x)) \rightarrow _{Z} \overline{z}(s(x'))$, and we may conclude that $\overline{z}(y) \rightarrow _{Z} \overline{z}(y')$.

Finally, observe that s is surjective, and therefore the solution to the equation $\overline{z} \circ s = z$ is unique.

We conclude this section by illustrating how to compute the function $\alpha$ for affine transition systems. Suppose that T is an affine transition system of dimension n. We can represent states in $S_T$ by vectors in $\mathbb {Q}^n$, and the transition relation $R_T$ by a finite set of transitions $B \subseteq \mathbb {Q}^n \times \mathbb {Q}^n$ that generates $R_T$ (i.e., $R_T = \textit{aff}(B)$). Suppose that $\varLambda$ is an m-dimensional subspace of $S_T^\star$; elements of $S_T^\star$ can be represented by n-dimensional row vectors, and $\varLambda$ can be represented by a basis $\mathbf {f}^\intercal _1, \dots , \mathbf {f}^\intercal _m$. We can compute a representation of $\left\langle U,s \right\rangle = \alpha _\varLambda (T)$ as follows. The elements of $S_U = \varLambda ^\star$ can be represented by m-dimensional vectors (with respect to the basis $g_1, \dots , g_m$ such that $g_i$ is the linear map that sends $\mathbf {f}^\intercal _j$ to 1 if $i=j$ and to 0 otherwise). The simulation s can be represented by the $m \times n$ matrix where the ith row is $\mathbf {f}_i^\intercal$. Finally, the transition relation $R_U$ can be represented by a set of generators $\left\{ \left\langle s(\mathbf {x}), s(\mathbf {x}') \right\rangle : \left\langle \mathbf {x},\mathbf {x}' \right\rangle \in B \right\}$.

3.3 Determinization

In this section, we show that any transition system operating over a finite-dimensional vector space has a best deterministic abstraction, and give an algorithm for computing the best deterministic affine abstraction (or determinization) of an affine transition system.

Towards an application of Lemma 2, we seek to characterize the determinization of a transition system by a space of functionals on its state space. For any linear space V and space of functionals $\varLambda$ on V, define an equivalence relation $\equiv _\varLambda$ on V by $x \equiv _\varLambda y$ iff $f(x) = f(y)$ for all $f \in \varLambda$. If T is a transition system and $\varLambda ,\varLambda '$ are spaces of functionals on $S_T$, we say that T is $(\varLambda ,\varLambda ')$-deterministic if for all $x_1,x_2$ $x_1',x_2'$ such that $x_1 \equiv _\varLambda x_2$, $x_1 \rightarrow _{T} x_1'$, and $x_2 \rightarrow _{T} x_2'$, then we also have $x_1' \equiv _{\varLambda '} x_1'$. Observe that if D is a deterministic transition system and $d : T \rightarrow D$ is a simulation, then T must be $(\varLambda _d,\varLambda _d)$-deterministic, where $\varLambda _d$ is the range of the dual map $d^\star$.

For any T and $\varLambda$, define $\textsf {Det}(T,\varLambda ) \triangleq \left\{ f : T \text { is } (\varLambda ,\left\{ f \right\} )\text {-deterministic} \right\}$ to be the greatest set of functionals such that T is $(\varLambda ,\textsf {Det}(T,\varLambda ))$-deterministic. Observe that $\textsf {Det}(T, -)$ is a monotone operator on the complete lattice of linear subspaces of $S_T^\star$ (i.e., if $\varLambda _1 \subseteq \varLambda _2$ then $\textsf {Det}(T,\varLambda _1) \subseteq \textsf {Det}(T,\varLambda _2)$, since $\varLambda _1$ induces a coarser equivalence relation than $\varLambda _2$). By the Knaster-Tarski fixpoint theorem [28], $\textsf {Det}(T,-)$ has a greatest fixpoint, which we denote by $\textsf {Det}(T)$. Then we have that T is $(\textsf {Det}(T),\textsf {Det}(T))$-deterministic, and $\textsf {Det}(T)$ contains every space $\varLambda$ such that T is $(\varLambda ,\varLambda )$-deterministic.

Lemma 3

(Determinization). For any transition system T, $\alpha _{\textsf {Det}(T)}(T)$ is a deterministic reflection of T.

Proof

Let $\left\langle D,d \right\rangle \triangleq \alpha _{\textsf {Det}(T)}(T)$. First, we show that D is deterministic. Suppose that $y \rightarrow _{D} y_1'$ and $y \rightarrow _{D} y_2'$; we must show that $y_1' = y_2'$. Since $R_D$ is defined to be $d[R_T]$, there must be $x_1$, $x_2$, $x_1'$, and $x_2'$ in $S_T$ such that $x_1 \rightarrow _{T} x_1'$, $x_2 \rightarrow _{T} x_2'$, $d(x_1) = d(x_2) = y$, $d(x_1') = y_1'$, and $d(x_2') = y_2$. Since $d(x_1) = d(x_2)$, we have $(\lambda f : \textsf {Det}(T). f(x_1)) = (\lambda f : \textsf {Det}(T). f(x_2))$, and therefore $x_1 \equiv _{\textsf {Det}(T)} x_2$. We thus have $x_1' \equiv _{\textsf {Det}(T,\textsf {Det}(T))} x_2'$, and since $\textsf {Det}(T,\textsf {Det}(T)) = \textsf {Det}(T)$, we have $y_1' = d(x_1') = d(x_2') = y_2'$.

It remains to show that $\left\langle D,d \right\rangle$ is a deterministic reflection of T. Suppose that $\left\langle U,u \right\rangle$ is another deterministic abstraction of T. Define G to be the range of $u^\star$. Since U is deterministic, we must have $G \subseteq \textsf {Det}(T,G)$, and since $\textsf {Det}(T)$ is the greatest fixpoint of $\textsf {Det}(T,-)$ we have $G \subseteq \textsf {Det}(T)$. By Lemma 2, there is a unique linear simulation $\overline{u} : D \rightarrow U$ such that $\overline{u} \circ d = u$.

If a transition system T is affine, then its determinization can be computed in polynomial time. Fixing a basis for the state space $S_T$ (of some dimension n), we can represent the transition relation of T in the form $R_T = \{ \left\langle \mathbf {x},\mathbf {x}' \right\rangle : A\mathbf {x}' = B\mathbf {x} + \mathbf {c} \}$ where $A, B \in \mathbb {Q}^{m \times n}$ and $\mathbf {c} \in \mathbb {Q}^m$ (for some m). We can represent functionals on $S_T$ by n-dimensional vectors, where the vector $\mathbf {v} \in \mathbb {Q}^n$ corresponds to the functional that maps $\mathbf {u} \mapsto \mathbf {v}^\intercal \mathbf {u}$. A linear space of functionals $\varLambda$ can be represented by a system of linear equations $\varLambda = \left\{ \mathbf {x} : M\mathbf {x} = 0 \right\}$. The ith row $\mathbf {a}_i^\intercal \mathbf {v} = \mathbf {b}_i^\intercal \mathbf {u} + c_i$, of the system of equations $A\mathbf {x}' = B\mathbf {x} + \mathbf {c}$ can be read as “T is $(\left\{ \mathbf {b}_i^\intercal \right\} ,\left\{ \mathbf {a}_i^\intercal \right\} )$-deterministic.” Thus, the functionals $\mathbf {f}^\intercal$ such that T is $(\varLambda ,\left\{ \mathbf {f}^\intercal \right\} )$-deterministic are those that can be written as a linear combination of the rows of A such that the corresponding linear combination of the rows of B belongs to $\varLambda$; i.e.,

$$\begin{aligned} \textsf {Det}(\{ \left\langle \mathbf {x},\mathbf {x}' \right\rangle : A\mathbf {x}' = B\mathbf {x} + \mathbf {c} \} , \{ \mathbf {f} : M\mathbf {f} = 0 \}) = \left\{ \mathbf {d} : \exists \mathbf {y}. MB^\intercal \mathbf {y} = 0 \wedge A^\intercal \mathbf {y} = \mathbf {d} \right\} \ . \end{aligned}$$

A representation of $\textsf {Det}(T,\varLambda )$ can be computed in polynomial time using Gaussian elimination. Since the lattice of linear subspaces of $S_T^\star$ has height n, the greatest fixpoint of $\textsf {Det}(T,-)$ can be computed in polynomial time.

Example 3

Continuing the example from Fig. 1 and Example 2, we consider the determinization of the affine transition system in Eq. (2). The rows of the matrix on the left-hand side correspond to generators for $\textsf {Det}(\textit{aff}(F),{\mathbb {Q}^4}^\star )$:

$$\begin{aligned} \textsf {Det}(\textit{aff}(F),{\mathbb {Q}^4}^\star )&= \textit{span}(\{\begin{bmatrix} 1&0&0&0 \end{bmatrix}, \begin{bmatrix} 0&1&1&0 \end{bmatrix}, \begin{bmatrix} 0&0&0&1 \end{bmatrix}\})\\ \textsf {Det}(\textit{aff}(F),\textsf {Det}(\textit{aff}(F),{\mathbb {Q}^4}^\star ))&= \textit{span}(\{\begin{bmatrix} 0&1&1&0 \end{bmatrix}, \begin{bmatrix} 0&0&0&1 \end{bmatrix}\}) \end{aligned}$$

which is the greatest fixpoint $\textsf {Det}(\textit{aff}(F))$. Intuitively: after one step of $\textit{aff}(F)$, the values of w, $x+y$, and z are affine functions of the input; after two steps $x+y$ and z are affine functions of the input but w is not, since the value of w on the second step depends upon the value of x in the first, and x is not an affine function of the input.

This yields the deterministic reflection $\left\langle D,d \right\rangle$ (pictured in Fig. 1) where

3.4 Rational-Spectrum Reflections of DATS

In this section, we define rational-spectrum $\mathbf {DATS}{}$ and show that every $\mathbf {DATS}{}$ has a rational-spectrum-reflection.

In the following, it is convenient to work with transition systems that are linear rather than affine. We will prove that every deterministic linear transition system has a best abstraction with rational spectrum. The result extends to the affine case through the use of homogenization: i.e., we embed a (non-empty) affine transition system into a linear transition system with one additional dimension, such that if we fix that dimension to be 1 then we recover the affine transition system. If the transition relation of a $\mathbf {DATS}{}$ is represented in the form $A\mathbf {x}' = B\mathbf {x} + \mathbf {c}$, then its homogenization is simply

$$ \begin{bmatrix} A &{} 0\\ 0 &{} 1 \end{bmatrix} \begin{bmatrix} \mathbf {x}'\\ y \end{bmatrix} =\begin{bmatrix} B &{} \mathbf {c}\\ 0 &{} 1 \end{bmatrix} \begin{bmatrix} \mathbf {x}\\ y \end{bmatrix}\ . $$

For a $\mathbf {DATS}{}$ T, we use $\textsf {homog}(T)$ to denote the pair $\left\langle L, h \right\rangle$, consisting the $\mathbf {DLTS}$ L resulting from homogenization and the affine simulation $h : T \rightarrow L$ that maps each $\mathbf {x} \in S_T$ to $\begin{bmatrix} \mathbf {x} \\ 1 \end{bmatrix}$ (i.e., the affine simulation h formalizes the idea that if we fix the extra dimension y to be 1, we recover the original $\mathbf {DATS}$ T).

Let T be a deterministic linear transition system. Since our goal is to analyze the asymptotic behavior of T, and all long-running behaviors of T reside entirely within $\text {dom}^\omega (T)$, we are interested in the structure of $\text {dom}^\omega (T)$ and T’s behavior on this set. First, we observe that $\text {dom}^\omega (T)$ is a linear subspace of $S_T$ and is computable. For any k, let $T^k$ denote the linear transition system whose transition relation is the k-fold composition of the transition relation of R. Consider the descending sequence of linear spaces

$$\begin{aligned} \text {dom}(T) \supseteq \text {dom}(T^2) \supseteq \text {dom}(T^3) \supseteq \dots \end{aligned}$$

(i.e., the set of states from which there are T computations of length 1, length 2, length 3, ...). Since the space $S_T$ is finite dimensional, this sequence must stabilize at some k. Since the states in $\text {dom}(T^k)$ have T-computations of any length and T is deterministic, we have that $\text {dom}(T^k)$ is precisely $\text {dom}^\omega (T)$.

Since T is total on $\text {dom}^\omega (T)$ and the successor of a state in $\text {dom}^\omega (T)$ must also belong to $\text {dom}^\omega (T)$, T defines a linear map $T|_\omega : \text {dom}^\omega (T) \rightarrow \text {dom}^\omega (T)$. In this way, we can essentially reduce asymptotic analysis of $\mathbf {DATS}{}$ to asymptotic analysis of linear dynamical systems. The asymptotic analysis of linear dynamical systems developed in Sects. 4 and 5 requires rational eigenvalues; thus we are interested in $\mathbf {DATS}{}$ T such that $T|_\omega$ has rational eigenvalues. With this in mind, we define $\textit{spec}(T) = \textit{spec}(T|_\omega )$, and say that T has rational spectrum if $\textit{spec}(T) \subseteq \mathbb {Q}$. Define $\mathbb {Q}\text {-}\mathbf {DLTS}{}$ to be the subcategory of $\mathbf {DLTS}{}$ with rational spectrum, and $\mathbb {Q}\text {-}\mathbf {DATS}{}$ to be the subcategory of $\mathbf {DATS}{}$ whose homogenization lies in $\mathbb {Q}\text {-}\mathbf {DLTS}{}$.

Example 4

Consider the $\mathbf {DLTS}{}$ T with

$$ R_T \triangleq \left\{ \left\langle \begin{bmatrix}x\\ y\\ z\end{bmatrix},\begin{bmatrix}x'\\ y'\\ z'\end{bmatrix} \right\rangle : \begin{bmatrix} 1 &{} 0 &{} 0 \\ 0 &{} 1 &{} 0 \\ 0 &{} 0 &{} 1 \\ 0 &{} 0 &{} 0 \end{bmatrix} \begin{bmatrix}x'\\ y'\\ z'\end{bmatrix} = \begin{bmatrix} 2 &{} 0 &{} 1 \\ 0 &{} 2 &{} 2 \\ 0 &{} 0 &{} 3 \\ 1 &{} -1 &{} 0 \\ \end{bmatrix} \begin{bmatrix}x\\ y\\ z\end{bmatrix} \right\} $$

The bottom-most equation corresponds to a constraint that only vectors where the x and y coordinates are equal have successors, so we have:

$$\begin{aligned} \text {dom}(T) = \left\{ \begin{bmatrix}x&y&z\end{bmatrix}^\intercal : x = y \right\} \end{aligned}$$

Supposing that the x and y coordinates are equal in some pre-state, they are equal in the post-state exactly when $z=0$, so we have

$$\begin{aligned} \text {dom}(T^2) = \left\{ \begin{bmatrix}x&y&z\end{bmatrix}^\intercal : x = y \wedge z = 0 \right\} \end{aligned}$$

It is easy to check that $\text {dom}(T^3) = \text {dom}(T^2)$, and therefore $\text {dom}^\omega (T) = \text {dom}(T^2)$. The vector $\begin{bmatrix}1&1&0\end{bmatrix}^\intercal$ is a basis for $\text {dom}^\omega (T)$, and the matrix representation of $T|_\omega$ with respect to this basis is $\begin{bmatrix} 2 \end{bmatrix}$ (i.e., $\begin{bmatrix}1&1&0\end{bmatrix}^\intercal \rightarrow _T \begin{bmatrix}2&2&0\end{bmatrix}^\intercal$). Thus we can see $\textit{spec}(T) = \left\{ 2 \right\}$, and T is a $\mathbb {Q}\text {-}\mathbf {DLTS}{}$.

Towards an application of Lemma 2, define the generalized rational eigenspace of a DLTS T to be

$$ E_{\mathbb {Q}}(T) \triangleq \textit{span}\left( \left\{ f \in S_T^\star : \exists \lambda \in \mathbb {Q}, \exists r \in \mathbb {N}^+. f \circ (T|_\omega - \underline{\lambda })^r = 0 \right\} \right) . $$

Lemma 4

Let T be a DLTS, and define $\left\langle Q,q \right\rangle \triangleq \alpha _{E_\mathbb {Q}(T)}(T)$. Then for any $\mathbb {Q}\text {-}\mathbf {DLTS}{}$ U and any simulation $s : T \rightarrow U$, there is a unique simulation $\overline{s} : Q \rightarrow U$ such that $\overline{s} \circ q = s$.

While $\alpha _{E_\mathbb {Q}(T)}(T)$ satisfies a universal property for $\mathbb {Q}\text {-}\mathbf {DLTS}{}$, it does not necessary belong to $\mathbb {Q}\text {-}\mathbf {DLTS}{}$ itself because it need not be deterministic. However, by iterative interleaving of Lemma 4 and determinization as shown in Algorithm 1, we arrive at a $\mathbb {Q}\text {-}\mathbf {DLTS}{}$-reflection. Example 5 demonstrates how we calculate a $\mathbb {Q}\text {-}\mathbf {DLTS}{}$-reflection of a particular $\mathbf {DLTS}{}$.

Example 5

Consider the $\mathbf {DLTS}{}$ T with transition relation

$$ R_T \triangleq \left\{ \left\langle \begin{bmatrix}w\\ x\\ y\\ z\end{bmatrix},\begin{bmatrix}w'\\ x'\\ y'\\ z'\end{bmatrix} \right\rangle : \begin{bmatrix} 1 &{} 0 &{} 0 &{} 0\\ 0 &{} 1 &{} 0 &{} 0\\ 0 &{} 0 &{} 1 &{} 0\\ 0 &{} 0 &{} 0 &{} 1\\ 0 &{} 0 &{} 0 &{} 0 \end{bmatrix} \begin{bmatrix}w'\\ x'\\ y'\\ z'\end{bmatrix} = \begin{bmatrix} 1 &{} 1 &{} 0 &{} 0 \\ 1 &{} 1 &{} 0 &{} 0 \\ 0 &{} 0 &{} 0 &{} 1 \\ 0 &{} 0 &{} -1 &{} 0\\ 1 &{} -1 &{} 0 &{} 0 \end{bmatrix} \begin{bmatrix}w\\ x\\ y\\ z\end{bmatrix} \right\} $$

We can calculate the $\omega$-domain of T $\text {dom}^\omega (T) = \left\{ \begin{bmatrix}w&x&y&z\end{bmatrix}^\intercal : w = x \right\}$, which has a basis $B = \begin{bmatrix}1&1&0&0\end{bmatrix}^\intercal , \begin{bmatrix}0&0&1&0\end{bmatrix}^\intercal , \begin{bmatrix}0&0&0&1\end{bmatrix}^\intercal$. With respect to B, $T|_\omega$ corresponds to the matrix

$$ T|_\omega = \begin{bmatrix} 2 &{} 0 &{} 0\\ 0 &{} 0 &{} 1\\ 0 &{} -1 &{} 0 \end{bmatrix} $$

and so we have $\textit{spec}(T) = \left\{ 2,i,-i \right\}$. We may calculate $E_\mathbb {Q}(T)$ by finding (generalized) left eigenvectors with eigenvalue 2, the only rational number in $\textit{spec}(T)$:

$$\begin{aligned} E_\mathbb {Q}(T)&= \left\{ \mathbf {v}^\intercal : \mathbf {v}^\intercal \underbrace{\begin{bmatrix} 1 &{} 0 &{} 0\\ 1 &{} 0 &{} 0\\ 0 &{} 1 &{} 0\\ 0 &{} 0 &{} 1 \end{bmatrix}}_{B} \left( \underbrace{ \begin{bmatrix} 2 &{} 0 &{} 0\\ 0 &{} 0 &{} 1\\ 0 &{} -1 &{} 0 \end{bmatrix}}_{T|_\omega } - \underbrace{\begin{bmatrix} 2 &{} 0 &{} 0\\ 0 &{} 2 &{} 0\\ 0 &{} 0 &{} 2 \end{bmatrix}}_{2I}\right) = 0 \right\} \\&= \textit{span}(\begin{bmatrix}1&1&0&0\end{bmatrix}, \begin{bmatrix}1&-1&0&0\end{bmatrix}) \end{aligned}$$

Finally, we have $\left\langle Q,q \right\rangle = \alpha _{E_{\mathbb {Q}}(T)}(T)$, where

$$R_Q = \left\{ \left\langle \begin{bmatrix}a\\ b\end{bmatrix},\begin{bmatrix}a'\\ b'\end{bmatrix} \right\rangle : \begin{bmatrix}1 &{} 0\\ 0 &{} 1\\ 0&{}0\end{bmatrix}\begin{bmatrix}a'\\ b'\end{bmatrix} =\begin{bmatrix}2 &{} 0\\ 0 &{} 0\\ 0 &{} 1\end{bmatrix}\begin{bmatrix}a\\ b\end{bmatrix} \right\} q = \begin{bmatrix}1 &{} 1 &{} 0 &{} 0\\ 1 &{} -1 &{} 0 &{} 0\end{bmatrix} $$

Q is deterministic and has rational spectrum, so $\left\langle Q,q \right\rangle$ is a $\mathbb {Q}\text {-}\mathbf {DLTS}{}$-reflection of T.

Theorem 1

For any deterministic linear transition system, Algorithm 1 computes a $\mathbb {Q}\text {-}\mathbf {DLTS}{}$-reflection.

Finally, by homogenization and Theorem 1, we conclude with the desired result:

Corollary 1

$\mathbb {Q}\text {-}\mathbf {DATS}{}$ is a reflective subcategory of $\mathbf {DATS}{}$.

4 Asymptotic Analysis of Linear Dynamical Systems

This section is concerned with analyzing the behavior of loops of the form

$$\begin{aligned} \mathbf{while} (G(\mathbf {x})) \mathbf{do} \mathbf {x} := A\mathbf {x} \ , \end{aligned}$$

where the $G(\mathbf {x})$ is an LIA formula and A is a matrix with integer spectrum. Our goal is to capture the asymptotic behavior of iterating the map A on an initial state $\mathbf {x}_0$ with respect to the formula G. Specifically, we show that

Theorem 2

For any LIA formula G and any matrix A with integer spectrum, there is a periodic sequence of LIA formulas $H_0, H_1,H_2,\dots$ such that for any initial state $\mathbf {x}_0 \in \mathbb {Q}^n$, there exists K such that for any $k > K$, $G(A^k \mathbf {x}_0)$ holds if and only if $H_k(\mathbf {x}_0)$ does.

Recall that an infinite sequence $H_0, H_1, H_2, \ldots$ is periodic if it is of the form

$$\begin{aligned} (H_0, H_1, \dots , H_P)^\omega \triangleq H_0, H_1, \dots , H_P, H_0, H_1, \dots , H_P, \dots \end{aligned}$$

We call the periodic sequence $(H_0, H_1, \dots , H_P)^\omega$ the characteristic sequence of the guard formula G with respect to dynamics matrix A, and denote it by $\chi (G, A)$. Note that $G(A^k\mathbf {x}_0)$ holds for all but finitely many k exactly when $\bigwedge _{i=0}^P H_i(\mathbf {x}_0)$ holds.

In the remainder of this section, we show how to compute characteristic sequences. Let G be an LIA formula and let A be a matrix with integer spectrum. To begin, we compute a quantifier-formula $G'$ that is equivalent to G (using, for example, Cooper’s algorithm [7]). We define $\chi (G',A)$ by recursion on the structure of $G'$. For the logical connectives $\wedge$, $\vee$, and $\lnot$, characteristic sequences are defined pointwise:

$$\begin{aligned} \chi (\lnot H, A)&\triangleq (\lnot (\chi (H, A)_0), \lnot (\chi (H, A)_1), \ldots )\\ \chi (H_1 \wedge H_2, A)&\triangleq (\chi (H_1, A)_0 \wedge \chi (H_2, A)_0, \chi (H_1, A)_1 \wedge \chi (H_2, A)_1, \ldots )\\ \chi (H_1 \vee H_2, A)&\triangleq (\chi (H_1, A)_0 \vee \chi (H_2, A)_0, \chi (H_1, A)_1 \vee \chi (H_2, A)_1, \ldots ) \end{aligned}$$

It remains to show how $\chi$ acts on atomic formulas, which take the form of inequalities $t_1 \le t_2$ and divisibility constraints $n \mid t$. An important fact that we employ in both cases is that for any linear term $\mathbf {c}^\intercal \mathbf {x}$ over the variables $\mathbf {x}$, we can compute a closed form for $\mathbf {c}^\intercal A^k(\mathbf {x})$ by symbolically exponentiating A. Since (by assumption) A has integer eigenvalues, this closed form has the form $\frac{1}{Q}(p(\mathbf {x},k))$ where $Q \in \mathbb {N}$ and p is an integer exponential-polynomial term, which takes the form

$$\begin{aligned} \lambda _1^kk^{d_1}\mathbf {a}_1^\intercal \mathbf {x} + \cdots + \lambda _m^kk^{d_m}\mathbf {a}_m^\intercal \mathbf {x} \end{aligned}$$

(3)

where $\lambda _i \in \textit{spec}(A)$, $d_i \in \mathbb {N}$, and $\mathbf {a}_i \in \mathbb {Z}^n$.¹

Characteristic Sequences for Inequalities. Our method for computing characteristic sequences for inequalities is a variation of Tiwari’s method for deciding termination of linear loops with real eigenvalues [29].

First, suppose that $\mathbf {p}(\mathbf {x},k)$ is an integer exponential-polynomial of the form in Eq. (3) such that each $\lambda _i$ is a positive integer. Further suppose that the summands are ordered by asymptotic growth, with the dominant term appearing earliest in the list; i.e., for $i < j$ we have either $\lambda _i > \lambda _j$, or $\lambda _i = \lambda _j$ and $d_i > d_j$. If we imagine that the variables $\mathbf {x}$ are fixed to some $\mathbf {x}_0 \in \mathbb {Z}^n$, then we see that $p(\mathbf {x}_0,k)$ is either identically zero or has finitely many zeros, and therefore its sign is eventually stable. Furthermore, the sign of $p(\mathbf {x}_0,k)$ as k tends to $\infty$ is simply the sign of its dominant term – that is, the sign of $\mathbf {a}_i^\intercal \mathbf {x}_0$ for the least i such that $\mathbf {a}_i^\intercal \mathbf {x}_0$ is non-zero. Thus, we may define a function $\textsf {DTA}$ that maps any exponential-polynomial term $p(\mathbf {x},k)$ (with positive integral $\lambda _i$) to an LIA formula such that for any $\mathbf {x}_0 \in \mathbb {Z}^n$, $\mathbf {x}_0 \models \textsf {DTA}(p)$ holds if and only if $\mathbf {p}(\mathbf {x}_0,k)$ is eventually non-negative ($\mathbf {p}(\mathbf {x}_0,k) \ge 0$ for all but finitely many $k \in \mathbb {N}$). $\textsf {DTA}$ is defined as follows:

$$\begin{aligned} \textsf {DTA}(0)&\triangleq \textit{true}\\ \textsf {DTA}(\lambda ^kk^d\mathbf {a}^\intercal \mathbf {x} + p)&\triangleq \mathbf {a}^\intercal \mathbf {x} \ge 1 \vee \left( \mathbf {a}^\intercal \mathbf {x} = 0 \wedge \textsf {DTA}(p)\right) \end{aligned}$$

Finally, we define the characteristic sequence of an inequality atom as follows. An inequality $t_1 \le t_2$ over the variables $\mathbf {x}$ can be written as $\mathbf {c}^\intercal \mathbf {x} + d \ge 0$ for $\mathbf {c} \in \mathbb {Z}^n$ and $d \in \mathbb {Z}$. Let $\frac{1}{Q_{\textit{even}}}p_{\textit{even}}(\mathbf {x},k)$ and $\frac{1}{Q_{\textit{odd}}}p_{\textit{odd}}(\mathbf {x},k)$ be the closed forms of $\mathbf {c}^\intercal A^{2k}(\mathbf {x})$ and $\mathbf {c}^\intercal A^{2k + 1}(\mathbf {x})$, respectively; by splitting into “even” and “odd” cases, we ensure that the exponential-polynomial terms $p_{\textit{even}}(\mathbf {x},k)$ and $p_{\textit{odd}}(\mathbf {x},k)$ have only positive $\lambda _i$ and thus are amenable to the dominant term analysis $\textsf {DTA}$ described above. Then we define:

$$\begin{aligned} \chi \left( \mathbf {c}^\intercal \mathbf {x} + d \ge 0, A \right) \triangleq \left( \textsf {DTA}(p_{\textit{even}}(\mathbf {x},k) + dQ_{\textit{even}}), \textsf {DTA}( p_{\textit{odd}}(\mathbf {x},k)+ dQ_{\textit{odd}}) \right) ^\omega \end{aligned}$$

Example 6

Consider the matrix A and its exponential $A^k$ below:

$$ A\left( \begin{bmatrix} x \\ y \\ z \\ a \\ b \end{bmatrix}\right) = \begin{bmatrix} 1 &{} 1 &{} 0 &{} 0 &{} 0\\ 0 &{} 1 &{} 1 &{} 0 &{} 0\\ 0 &{} 0 &{} 1 &{} 0 &{} 0\\ 0 &{} 0 &{} 0 &{} -3 &{} 0 \\ 0 &{} 0 &{} 0 &{} 0 &{} 2 \\ \end{bmatrix} \begin{bmatrix} x \\ y \\ z \\ a \\ b \end{bmatrix} $$

$$ A^k\left( \begin{bmatrix}x\\ y\\ z\\ a\\ b\end{bmatrix}\right) = \begin{bmatrix} 1 &{} k &{} \frac{k(k-1)}{2} &{} 0 &{} 0 \\ 0 &{} 1 &{} k &{} 0 &{} 0\\ 0 &{} 0 &{} 1 &{} 0 &{} 0\\ 0 &{} 0 &{} 0 &{} (-3)^k &{} 0 \\ 0 &{} 0 &{} 0 &{} 0 &{} 2^k \end{bmatrix} \begin{bmatrix} x \\ y \\ z \\ a \\ b \end{bmatrix} = \begin{bmatrix} \frac{1}{2}(zk^2 + (2y - z)k + 2x)\\ zk + y\\ z \\ (-3)^k a\\ 2^k b \end{bmatrix} $$

First we compute the characteristic sequence $\chi (x \ge 0,A)$. Applying the dominant term analysis of the closed form of x yields

$$ \textsf {DTA}\left( z k^2 + \left( 2y - z\right) k + x \right) = \left( \begin{array}{ll}&{} z> 0 \\ \vee &{}(z = 0 \wedge 2y - z > 0) \\ \vee &{}(z = 0 \wedge 2y - z = 0 \wedge x \ge 0)\end{array} \right) \ , $$

Since the closed form involves only positive exponential terms, we need not split into an even and odd case, and we simply have:

$$ \chi (x \ge 0, A) = (z> 0 \vee (z = 0 \wedge 2y - z > 0) \vee (z = 0 \wedge 2y - z = 0 \wedge x \ge 0))^\omega $$

Next we compute the characteristic sequence $\chi (a-b \ge 0, A)$, which does require a case split. Applying dominant term analysis of the closed form of $(a-b)$ yields

$$\begin{aligned} \textsf {DTA}( a \cdot (-3)^{2k} - b \cdot 2^{2k})&= a> 0 \vee (a=0 \wedge -b \ge 0) \\ \textsf {DTA}( a \cdot (-3)^{2k+1} - b \cdot 2^{2k+1})&= -a > 0 \vee (-a=0 \wedge -b \ge 0) \ . \end{aligned}$$

and thus we have

$$ \chi (a - b \ge 0, A) = (a> 0 \vee (a=0 \wedge -b \ge 0), -a > 0 \vee (-a=0 \wedge -b \ge 0))^\omega \ . $$

   

Characteristic Sequences for Divisibility Atoms. Last we show how to define $\chi$ for divisibility atoms $n \mid t$. Write the term t as $\mathbf {c}^\intercal \mathbf {x}+d$ and let the closed form of $\mathbf {c}^\intercal A^k(\mathbf {x})$ be

$$\begin{aligned} \frac{1}{Q}(\lambda _1^kk^{d_1}\mathbf {a}_1^\intercal \mathbf {x} + \cdots + \lambda _m^kk^{d_m}\mathbf {a}_m^\intercal \mathbf {x})\ . \end{aligned}$$

The formula $n \mid \mathbf {c}^\intercal A^k(\mathbf {x})+d$ is equivalent to $Qn \mid \lambda _1^kk^{d_1} \mathbf {a}_1^\intercal \mathbf {x} + \cdots + \lambda _m^kk^{d_m}\mathbf {a}_m^\intercal \mathbf {x} + Qd$. For any i, the sequence $\langle \lambda _i^kk^{d_i} \bmod Qn\rangle _{k=0}^\infty$ is ultimately periodic, since (1) $\langle k \bmod Qn \rangle _{k=0}^\infty = (0, 1, \dots , Qn -1)^\omega$, (2) $\langle \lambda _i^k \mod Qn \rangle _{k=0}^\infty$ is ultimately periodic (with period and transient length bounded above by Qn)², and (3) ultimately periodic sequences are closed under pointwise product. It follows that for each i, there is a periodic sequence of integers $\left\langle z_{i,k} \right\rangle _{k=0}^\infty$ that agrees with $\langle \lambda _i^kk^{d_i} \bmod Qn\rangle _{k=0}^\infty$ on all but finitely many terms. Finally, we take

$$\begin{aligned} \chi (n \mid t,A) \triangleq \langle Qn \mid z_{1,k}\mathbf {a}_1^\intercal \mathbf {x} + \dots + z_{m,k}\mathbf {a}_m^\intercal \mathbf {x} + Qd \rangle _{k=0}^\infty \ . \end{aligned}$$

Example 7

Consider matrix A and the closed form of its exponents below

$$ A \left( \begin{bmatrix} x \\ y \\ z \end{bmatrix}\right) = \begin{bmatrix} 1 &{} 1 &{} 0 \\ 0 &{} 1 &{} 0 \\ 0 &{} 0 &{} 5 \\ \end{bmatrix} \begin{bmatrix} x \\ y \\ z \end{bmatrix} A^k\left( \begin{bmatrix} x \\ y \\ z \end{bmatrix} \right) = \begin{bmatrix} 1 &{} k &{} 0 \\ 0 &{} 1 &{} 0 \\ 0 &{} 0 &{} 5^k \\ \end{bmatrix} \begin{bmatrix} x \\ y \\ z \end{bmatrix} $$

We show the characteristic sequences for some divisibility atoms w.r.t A:

5 A Conditional Termination Analysis for Programs

This section demonstrates how the results from Sects. 3 and 4 can be combined to yield a conditional termination analysis that applies to general programs.

Integer-Spectrum Restriction for $\mathbb {Q}\text {-}\mathbf {DLTS}{}$. Section 3 gives a way to compute a $\mathbb {Q}\text {-}\mathbf {DATS}{}$-reflection of any transition formula. Yet the analysis we developed in Sect. 4 only applies to linear dynamical systems with integer spectrum. We now show how to bridge the gap. Let V be a $\mathbb {Q}\text {-}\mathbf {DATS}{}$. As discussed in Sect. 3.4, we may homogenize V to obtain a $\mathbb {Q}\text {-}\mathbf {DLTS}$ T. Define $\mathbb {Z}(T)$ to be the space spanned by the generalized (right) eigenvectors of $T|_\omega$ that correspond to integer eigenvalues:

$$ \mathbb {Z}(T) \triangleq \textit{span}(\{ x \in \text {dom}^\omega (T) : \exists r \in \mathbb {N}^+, \lambda \in \mathbb {Z}. (T|_\omega - \underline{\lambda })^r(x) = 0 \}) $$

Since $\mathbb {Z}(T)$ is invariant under $T|_\omega$ and thus T, T defines a linear map $T|_{\mathbb {Z}} : \mathbb {Z}(T) \rightarrow \mathbb {Z}(T)$, and by construction $T|_{\mathbb {Z}}$ has integer spectrum. The following lemma justifies the restriction of our attention to the subspace $\mathbb {Z}(T)$.

Lemma 5

Let F be a transition formula, let $\left\langle V, s \right\rangle$ be a $\mathbb {Q}\text {-}\mathbf {DATS}{}$-reflection of F, and let $\left\langle T,h \right\rangle = \textsf {homog}(V)$. For any state $v \in \text {dom}^\omega (F)$, we have $h(s(v)) \in \mathbb {Z}(T)$.

Example 8

The following loop computes the number of trailing 0’s in the binary representation of integer x and its corresponding transition formula:

The homogenization of the $\mathbb {Q}\text {-}\mathbf {DATS}{}$-reflection of F is the $\mathbb {Q}\text {-}\mathbf {DLTS}{}$ T, where:

$$ R_T \triangleq \left\{ \left\langle \begin{bmatrix}x\\ c\\ h\end{bmatrix}, \begin{bmatrix}x'\\ c'\\ h'\end{bmatrix} \right\rangle : \begin{bmatrix} x' \\ c' \\ h' \end{bmatrix} = \begin{bmatrix} \frac{1}{2} &{} 0 &{} 0 \\ 0 &{} 1 &{} 1\\ 0 &{} 0 &{} 1 \end{bmatrix} \begin{bmatrix} x \\ c \\ h \end{bmatrix} \right\} $$

The $\omega$-domain of T is the whole state space $\mathbb {Q}^3$. Since the eigenvector $\begin{bmatrix} 1&0&0 \end{bmatrix}^\intercal$ of the transition matrix corresponds to a non-integer eigenvalue $\frac{1}{2}$, the x-coordinate of states in $\mathbb {Z}(T)$ must be 0; i.e., $\mathbb {Z}(T) = \{ (x, c, y): x = 0 \}$. We conclude that $x \ne 0$ is a sufficient condition for the loop to terminate.

The Mortal Precondition Operator. Algorithm 2 shows how to compute a mortal precondition for an LIA transition formula $F(\mathbf {x},\mathbf {x}')$ (i.e., a sufficient condition for which F terminates). The algorithm operates as follows. First, we compute a $\mathbb {Q}\text {-}\mathbf {DATS}{}$-reflection of F, and homogenize to get a $\mathbb {Q}\text {-}\mathbf {DLTS}{}$ T and an affine simulation $t : F \rightarrow T$. Let p denote an (arbitrary) projection from $S_T$ onto $\mathbb {Z}(T)$ (so p is a simulation from T to $T|_{\mathbb {Z}}$). We then compute an LIA formula G which represents the states $\mathbf {w}$ of $T|_{\mathbb {Z}}$ such that there is some $v \in \text {dom}(F)$ such that $t(v) \in \mathbb {Z}(T)$ and $p(t(v)) = \mathbf {w}$. Letting $(H_0,...,H_P)^\omega$ be the characteristic sequence $\chi (G, T|_{\mathbb {Z}})$, we have that for any $v \in \text {dom}^\omega (F)$, t(v) must belong to $\mathbb {Z}(T)$ and p(t(v)) satisfies each $H_i$, so we define

$$\begin{aligned} \textit{mp}(F) \triangleq \{ v \in S_F : t(v) \notin \mathbb {Z}(T) \text { or } v \not \models \bigwedge _i H_i(p(t(\mathbf {x}))) . \end{aligned}$$

Within the context of the algorithm, we suppose that states of F are represented by n-dimensional vectors, states of T are represented as m-dimensional vectors, and state of $T|_{\mathbb {Z}}$ are represented as q-dimensional vectors. The affine simulation t is represented in the form $\mathbf {x} \mapsto A\mathbf {x} + \mathbf {b}$, where $A \in \mathbb {Z}^{m \times n}$ and $\mathbf {b} \in \mathbb {Z}^m$, the projection p as a $\mathbb {Z}^{q \times m}$ matrix, and the linear map $T|_{\mathbb {Z}}$ as a $\mathbb {Q}^{q \times q}$ matrix. The fact that p and t have all integer (rather than rational) entries is without loss of generality, since any simulation can be scaled by the least common denominator of its entries.

Theorem 3

(Soundness). For any transition formula F, for any state s such that , we have $s \notin \text {dom}^\omega (F)$.

Proof

Let T, t, p, C, G, and $H_0,\dots ,H_P$ be as in Algorithm 2. We prove the contrapositive: we assume $v \in \text {dom}^\omega (F)$ and prove $v \notin mp(F)$, or equivalently $v \models H_i(p (t( \mathbf {x})))$ for each i and $t(v) \in \mathbb {Z}(T)$. We have $t(v) \in \mathbb {Z}(T)$ by Lemma 5, so it remains only to show that $v \models H_i(p (t( \mathbf {x})))$ for each i.

Since $v \in \text {dom}^\omega (F)$, there exists an infinite trajectory of F starting from v: $v \rightarrow _F v_1 \rightarrow _F v_2 \rightarrow _F \ldots$. For any j, let $\mathbf {w}_j = T|_{\mathbb {Z}}^j(p(t(v)))$. Since $p \circ t$ is an (affine) simulation, we have $\mathbf {w}_j = p(t(v_j))$ for all j. It follows that for any j, we have $[v_j,v_{j+1}] \models F(\mathbf {x},\mathbf {x}') \wedge \mathbf {w}_j = p(t(\mathbf {x}_j)) \wedge Ct(\mathbf {x}_j) = 0$, and so $G(\mathbf {w}_j) = \exists \mathbf {x},\mathbf {x}'. F(\mathbf {x},\mathbf {x}') \wedge \mathbf {w}_j = p(t(\mathbf {x})) \wedge Ct(\mathbf {x}) = 0$ holds for all j. By Theorem 2, $H_i(p(t( \mathbf {x})))$ holds for all $H_i$.

The proof of soundness requires only that we can compute $\mathbb {Q}\text {-}\mathbf {DATS}{}$-abstractions of transition formulas. The following is the culmination of our development of $\mathbb {Q}\text {-}\mathbf {DATS}{}$-reflections:

Theorem 4

(Monotonicity). For any transition formulas $F_1$ and $F_2$ such that $F_1 \models F_2$, we have .

The desire for monotonicity is inspired by the principle that changes to a program should have a predictable impact on its analysis [34]. Monotonicity guarantees that more information into the analysis always leads to better results—for example, if a user annotates a procedure with pre-conditions or adds loop invariants into the program, our termination analysis can only produce weaker (that is, better) preconditions for termination. Moreover, in the context of this work, monotonicity also guarantees that if we cannot prove termination using the operator that we defined, then any linear abstraction of the loop has reachable non-terminating states.

6 Evaluation

Section 5 shows how to compute mortal preconditions for transition formulas. Using the framework of algebraic termination analysis [34], we can “lift” the analysis to compute mortal preconditions for whole programs. The essential idea is to compute summaries for loops and procedures in “bottom-up” fashion, apply the mortal precondition operator from Sect. 5 to each loop body summary, and then propagate the mortal preconditions for the loops back to the entry of the program (see [34] for more details). We can verify that a program terminates by using an SMT solver to check that its mortal precondition is valid.

We have implemented Algorithm 2 as a mortal precondition operator (“mortal precondition via Linear Reflections”) in ComPACT, a tool that implements the termination analysis framework presented in [34]. We compare the performance of our analysis against 2LS [5], Ultimate Automizer [10] and CPAchecker [23], the top three competitors in the termination category of Competition on Software Verification (SV-COMP) 2020.

Experiments are run on a virtual machine with Ubuntu 18.04, with a single-core Intel Core i7-9750H @ 2.60 GHz CPU and 8 GB of RAM. All tools were run with a time limit of 10 min.

Benchmarks. We tested on a suite of 263 programs divided into 4 categories. The termination and recursive suites contain small programs with challenging termination arguments, while the polybench suite contains larger real-world programs that have relatively simple termination arguments. The termination category consists of the non-recursive, terminating benchmarks from SV-COMP 2020 in the Termination-MainControlFlow suite. The recursive category consists of the recursive, terminating benchmarks from the recursive directory and Termination-MainControlFlow. Note that 2LS does not handle recursive programs, so we exclude it from the recursive category. Finally, we created a new test suite linear consisting of programs with terminating linear abstractions. This suite is designed to exercise the capabilities of the , and includes all examples from Ben-Amram and Genaim’s article [1] on multi-phase ranking functions, loops with disjunctive and/or modular arithmetic guards, and loops that model integer division and remainder calculation.

Table 1. Termination verification benchmarks; time in seconds.

Table 2. Comparing and ComPACT; time in seconds.

How Does Our Analysis Compare with the State-of-the-Art? The comparison of ComPACT using the operator against state-of-the-art termination analysis tools is shown in Table 1. ComPACT with is competitive with (but not dominating) leading tools in terms of number of tasks solved across the suite, and uses substantially less time. The analysis is least successful on the termination and recursive suites, which are designed to have difficult termination arguments. Most competitive tools use a portfolio of different termination techniques to approach such problems (e.g., Ultimate Automizer synthesizes linear, nested, multi-phase, lexicographic and piecewise ranking functions); we investigate the use of in a portfolio solver in the following.

ComPACT with solves all tasks in the polybench suite, which contains numerical programs that have simple termination arguments, but which are larger than the SV-COMP tasks. 2LS, Ultimate Automizer, and CPAChecker exhaust time or memory limits on all tasks. Nested loops are a problematic pattern that appears in these programs, e.g.,

For such loops, is guaranteed to synthesize a conditional termination argument that is at least as weak as (regardless of the contents of the inner loop) by monotonicity and the fact that the loop body formula entails . Ultimate Automizer, CPAChecker, and 2LS cannot make such theoretical guarantees.

The linear suite demonstrates that is capable of proving termination of programs that lie outside the boundaries of the other tools.

Can Our Analysis Improve a Portfolio Solver? We compare and ComPACT in Table 2. The columns correspond to running ComPACT with the following options: excluding the portfolio from [34] (), including the portfolio but excluding (ComPACT-), and including the portfolio and (ComPACT+). ComPACT+ can solve 11 additional tasks over ComPACT- while adding negligible runtime overhead. In fact, adding to the portfolio decreases the amount of time it takes for ComPACT to complete all benchmark suites. Note that the combined tool is successful on the most termination tasks among all the tools we tested, both overall and for each individual suite except the termination category.

7 Related Work

Termination Analysis of Linear Loops. The universal termination problem for linear loops (or total deterministic affine transition systems, in the terminology of Sect. 4) was posed by Tiwari [29]. The case of linear loops over the reals was resolved by Tiwari [29], over the rationals by Braverman [4], and finally over the integers by Hosseini et al. [14]. In principle, we can combine any of these techniques with our algorithm for computing $\mathbf {DATS}{}$-reflections of transition formulas to yield a sound (but incomplete) termination analysis. The significance of computing a $\mathbf {DATS}{}$-reflection (rather than just “some” abstraction) is that is provides an algorithmic completeness result: if it is possible to prove termination of a loop by exhibiting a terminating linear dynamical system that simulates it, the algorithm will prove termination.

The method introduced in Sect. 4 to compute characteristic sequences of inequalities is based on the method that Tiwari used to prove decidability of the universal termination problem for linear loops with (positive) real spectra [29]. Tiwari’s condition of having real spectra is strictly more general than the integer spectra used by our procedure; requiring that the spectrum be integer allows us express the $\mathbf {DTA}$ procedure in linear integer arithmetic rather than real arithmetic. Similar procedures appear also in [12, 18]. We note in particular that our results in Sects. 4 and 5 subsume Frohn and Giesl’s decision procedure for universal termination for upper-triangular linear loops [12]; since every rational upper-triangular linear loop has a rational spectrum (and is therefore a $\mathbb {Q}\text {-}\mathbf {DATS}{}$), the mortal precondition computed for any rational upper-triangular linear loop is valid iff the loop is universally terminating.

Linear Abstractions. The formulation of “best abstractions” using reflective subcategories is based on the framework developed in [17]. A variation of this method was used in the context of invariant generation, based on computing (weak) reflections of linear rational arithmetic formulas in the category of rational vector addition systems [27]. This paper is the first to apply the idea to termination analysis.

A method for extracting polynomial recurrence (in)equations that are entailed by a transition formula appears in [16]. The algorithm can also be applied to compute a $\mathbf {TDATS}$-abstraction of a transition formula. The procedure does not guarantee that the $\mathbf {TDATS}$-abstraction is a reflection (best abstraction); Proposition 1 demonstrates that no such procedure exists. In this paper, we generalize the model to allow non-total transition systems, and show that best abstractions do exist. The techniques from Sect. 3 can be used for invariant generation, improving upon the methods of [16].

Kincaid et al. show that the category of linear dynamical systems with periodic rational spectrum is a reflective subcategory of the category of linear dynamical systems [18]. A complex number n is periodic rational if $n^p$ is rational for some $p \in \mathbb {Z}^{>0}$. Combining this result with the technique from Sect. 3 yields the result that the category of $\mathbf {DATS}$ with periodic rational spectrum is a reflective subcategory of $\mathbf {TF}$. The decision procedure from Sect. 4 extends easily to the periodic rational case, which results in a strictly more powerful decision procedure.

Termination Analysis. Termination analysis, and in particular conditional termination analysis, has been widely studied. Work on the subject can be divided into practical termination analyses that work on real programs (but offer few theoretical guarantees) [2, 6, 8, 11, 13, 20, 30,31,32], and work on simplified model (such as linear, octagonal, and polyhedral loops) with strong guarantees (but cannot be applied directly to real programs) [1, 3, 4, 14, 21, 25, 29]. This paper aims to help bridge the gap between the two, by showing how to apply analyses for linear loops to general programs, while preserving some of their desirable theoretical properties, in particular monotonicity.