This section is dedicated to the proof of the following completeness result for deterministic linear loop programs.
To prove this completeness theorem, we need to construct a GNTA from a given infinite execution. The following lemma shows that we can restrict our construction to exclude all linear subspaces that have a bounded execution.
Proof
(of Theorem 11). The polyhedron corresponding to loop transition of the deterministic linear loop program
L is
Define
\(\mathcal {Y}\) to be the convex cone spanned by the rays of the guard polyhedron:
$$ \mathcal {Y} := \{ \varvec{y} \in \mathbb {R}^n \mid G\varvec{y} \le 0 \} $$
Let
\(\overline{\mathcal {Y}}\) be the smallest linear subspace of
\(\mathbb {R}^n\) that contains
\(\mathcal {Y}\), i.e.,
\(\overline{\mathcal {Y}} = \mathcal {Y} - \mathcal {Y}\) using pointwise subtraction, and let
\(\overline{\mathcal {Y}}^\bot \) be the linear subspace of
\(\mathbb {R}^n\) orthogonal to
\(\overline{\mathcal {Y}}\); hence
\(\mathbb {R}^n = \overline{\mathcal {Y}} \oplus \overline{\mathcal {Y}}^\bot \).
Let
\(P := \{ \varvec{x} \in \mathbb {R}^n \mid G\varvec{x} \le \varvec{g} \}\) denote the guard polyhedron. Its projection
\(P^{\overline{\mathcal {Y}}^\bot }\) to the subspace
\(\overline{\mathcal {Y}}^\bot \) is again a polyhedron. By the decomposition theorem for polyhedra [
36, Corollary 7.1b],
\(P^{\overline{\mathcal {Y}}^\bot } = Q + C\) for some polytope
Q and some convex cone
C. However, by definition of the subspace
\(\overline{\mathcal {Y}}^\bot \), the convex cone
C must be equal to
\(\{ \varvec{0} \}\): for any
\(\varvec{y} \in C \subseteq \overline{\mathcal {Y}}^\bot \), we have
\(G\varvec{y} \le \varvec{0}\), thus
\(\varvec{y} \in \mathcal {Y}\), and therefore
\(\varvec{y}\) is orthogonal to itself, i.e.,
\(\varvec{y} = \varvec{0}\). We conclude that
\(P^{\overline{\mathcal {Y}}^\bot }\) must be a polytope, and thus it is bounded. By assumption
L is nonterminating, so
\(L^{\overline{\mathcal {Y}}^\bot }\) is nonterminating, and since
\(P^{\overline{\mathcal {Y}}^\bot }\) is bounded, any infinite execution of
\(L^{\overline{\mathcal {Y}}^\bot }\) must be bounded.
Let
\(\mathcal {U}\) denote the direct sum of the generalized eigenspaces for the eigenvalues
\(0 \le \lambda < 1\). Any infinite execution is necessarily bounded on the subspace
\(\mathcal {U}\) since on this space the map
\(\varvec{x} \mapsto M\varvec{x} + \varvec{m}\) is a contraction. Let
\(\mathcal {U}^\bot \) denote the subspace of
\(\mathbb {R}^n\) orthogonal to
\(\mathcal {U}\). The space
\(\overline{\mathcal {Y}} \cap \mathcal {U}^\bot \) is a linear subspace of
\(\mathbb {R}^n\) and any infinite execution in its complement is bounded. Hence we can turn our analysis to the subspace
\(\overline{\mathcal {Y}} \cap \mathcal {U}^\bot + \varvec{x}\) for some
\(\varvec{x} \in \overline{\mathcal {Y}}^\bot \oplus \mathcal {U}\) for the rest of the proof according to Lemma
12. From now on, we implicitly assume that we are in this space without changing any of the notation.
Part 1. In this part we show that there is a basis
\(\varvec{y_1}, \ldots , \varvec{y_s} \in \mathcal {Y}\) such that
M turns into a matrix
U of the form given in (
1) with
\(\lambda _1, \ldots , \lambda _s, \mu _1, \ldots , \mu _{s-1} \ge 0\). Since we allow
\(\mu _k\) to be positive between different eigenvalues (Example
14 illustrates why), this is not necessarily a Jordan normal form and the vectors
\(\varvec{y_i}\) are not necessarily generalized eigenvectors.
We choose a basis \(\varvec{v_1}, \ldots , \varvec{v_s}\) such that M is in Jordan normal form with the eigenvalues ordered by size such that the largest eigenvalues come first. Define \(\mathcal {V}_1 := \overline{\mathcal {Y}} \cap \mathcal {U}^\bot \) and let \(\mathcal {V}_1 \supset \ldots \supset \mathcal {V}_s\) be a strictly descending chain of linear subspaces where \(\mathcal {V}_i\) is spanned by \(\varvec{v_k}, \ldots , \varvec{v_s}\).
We define a basis
\(\varvec{w_1}, \ldots , \varvec{w_s}\) by doing the following for each Jordan block of
M, starting with
\(k = 1\). Let
\(M^{(k)}\) be the projection of
M to the linear subspace
\(\mathcal {V}_k\) and let
\(\lambda \) be the largest eigenvalues of
\(M^{(k)}\). The
m-fold iteration of a Jordan block
\(J_\ell (\lambda )\) for
\(m \ge \ell \) is given by
$$\begin{aligned} J_\ell (\lambda )^m = \left( \begin{matrix} \lambda ^m &{} \genfrac(){0.0pt}1{m}{1}\lambda ^{m-1} &{} \dots &{} \genfrac(){0.0pt}1{m}{\ell }\lambda ^{m-\ell } \\ &{} \lambda ^m &{} \dots &{} \genfrac(){0.0pt}1{m}{\ell -1}\lambda ^{m-\ell +1} \\ &{} &{} \ddots &{} \vdots \\ 0 &{} &{} &{} \lambda ^m \end{matrix} \right) \in \mathbb {R}^{\ell \times \ell }. \end{aligned}$$
(7)
Let
\(\varvec{z_0}, \varvec{z_1}, \varvec{z_2}, \ldots \) be an infinite execution of the loop
L in the basis
\(\varvec{v_k}, \ldots , \varvec{v_s}\) projected to the space
\(\mathcal {V}_k\). Since by Lemma
12 we can assume that there are no fixed points on this space,
\(|\varvec{z_t}| \rightarrow \infty \) as
\(t \rightarrow \infty \) in each of the top
\(\ell \) components. Asymptotically, the largest eigenvalue
\(\lambda \) dominates and in each row of
\(J_k(\lambda _k)^m\) (
7), the entries
\(\genfrac(){0.0pt}1{m}{j}\lambda ^{m-j}\) in the rightmost column grow the fastest with an asymptotic rate of
\(\varTheta (m^j \exp (m))\). Therefore the sign of the component corresponding to basis vector
\(\varvec{v_{k+\ell }}\) determines whether the top
\(\ell \) entries tend to
\(+\infty \) or
\(-\infty \), but the top
\(\ell \) entries of
\(\varvec{z_t}\) corresponding to the top Jordan block will all have the same sign eventually. Because no state can violate the guard condition we have that the guard cannot constraint the infinite execution in the direction of
\(\varvec{v_j}\) or
\(-\varvec{v_j}\), i.e.,
\(G^{\mathcal {V}_k} \varvec{v_j} \le \varvec{0}\) for each
\(j\in \{k, \ldots , k+\ell \}\) or
\(G^{\mathcal {V}_k} \varvec{v_j} \ge \varvec{0}\) for each
\(j\in \{k, \ldots , k+\ell \}\), where
\(G^{\mathcal {V}_k}\) is the projection of
G to the subspace
\(\mathcal {V}_k\). So without loss of generality the former holds (otherwise we use
\(-\varvec{v_j}\) instead of
\(\varvec{v_j}\) for
\(j\in \{k, \ldots , k+\ell \}\)) and for
\(j\in \{k, \ldots , k+\ell \}\) we get
\(\varvec{v_j} \in \mathcal {Y} + \mathcal {V}_k^\bot \) where
\(\mathcal {V}_k^\bot \) is the space spanned by
\(\varvec{v_1}, \ldots , \varvec{v_{k-1}}\). Hence there is a
\(\varvec{u_j} \in \mathcal {V}_k^\bot \) such that
\(\varvec{w_j} := \varvec{v_j} + \varvec{u_j}\) is an element of
\(\mathcal {Y}\). Now we move on to the subspace
\(\mathcal {V}_{k+\ell +1}\), discarding the top Jordan block.
Let
T be the matrix
M written in the basis
\(\varvec{w_1}, \ldots , \varvec{w_k}\). Then
T is of upper triangular form: whenever we apply
\(M\varvec{w_k}\) we get
\(\lambda _k \varvec{w_k} + \varvec{u_k}\) (
\(\varvec{w_k}\) was an eigenvector in the space
\(\mathcal {V}_k\)) where
\(\varvec{u_k} \in \mathcal {V}_k^\bot \), the space spanned by
\(\varvec{v_1}, \ldots , \varvec{v_{k-1}}\) (which is identical with the space spanned by
\(\varvec{w_1}, \ldots , \varvec{w_{k-1}}\)). Moreover, since we processed every Jordan block entirely, we have that for
\(\varvec{w_k}\) and
\(\varvec{w_j}\) from the same generalized eigenspace (
\(T_{k,k} = T_{j,j}\)) that for
\(k > j\)$$\begin{aligned} T_{j,k} \in \{ 0, 1 \} \text { and } T_{j,k} = 1 \text { implies } k = j+1. \end{aligned}$$
(8)
In other words, when projected to any generalized eigenspace
T consists only of Jordan blocks.
Now we change basis again in order to get the upper triangular matrix
U defined in (
1) from
T. For this we define the vectors
$$ \varvec{y_k} := \varvec{\beta }_k \sum _{j=1}^k \alpha _{k,j} \varvec{w_j}. $$
with nonnegative real numbers
\(\alpha _{k,j} \ge 0\),
\(\alpha _{k,k} > 0\), and
\(\varvec{\beta }> 0\) to be determined later. Define the matrices
\(W := (\varvec{w_1} \ldots \varvec{w_s})\),
\(Y := (\varvec{y_1} \ldots \varvec{y_s})\), and
\(\alpha := (\alpha _{k,j})_{1 \le j \le k \le s}\). So
\(\alpha \) is a nonnegative lower triangular matrix with a positive diagonal and hence invertible. Since
\(\alpha \) and
W are invertible, the matrix
\(Y = \mathrm {diag}(\varvec{\beta }) \alpha W\) is invertible as well and thus the vectors
\(\varvec{y_1}, \ldots , \varvec{y_s}\) form a basis. Moreover, we have
\(\varvec{y_k} \in \mathcal {Y}\) for each
k since
\(\alpha \ge 0\),
\(\varvec{\beta }> 0\), and
\(\mathcal {Y}\) is a convex cone. Therefore we get
$$\begin{aligned} GY \le 0. \end{aligned}$$
(9)
We will first choose
\(\alpha \). Define
\(T =: D + N\) where
\(D = \mathrm {diag}(\lambda _1, \ldots , \lambda _s)\) is a diagonal matrix and
N is nilpotent. Since
\(\varvec{w_1}\) is an eigenvector of
M we have
\(M\varvec{y_1} = M \varvec{\beta }_1 \alpha _{1,1} \varvec{w_1} = \lambda _1 \varvec{\beta }_1 \alpha _{1,1} \varvec{w_1} = \lambda _1 \varvec{y_1}\). To get the form in (
1), we need for all
\(k > 1\)$$\begin{aligned} M\varvec{y_k} = \lambda _k \varvec{y_k} + \mu _{k-1} \varvec{y_{k-1}}. \end{aligned}$$
(10)
Written in the basis
\(\varvec{w_1}, \ldots , \varvec{w_s}\) (i.e., multiplied with
\(W^{-1}\)),
$$ (D + N) \varvec{\beta }_k \sum _{j \le k} \alpha _{k,j} \varvec{e_j} = \lambda _k \varvec{\beta }_k \sum _{j \le k} \alpha _{k,j} \varvec{e_j} + \mu _{k-1} \varvec{\beta }_{k-1} \sum _{j < k} \alpha _{k-1,j} \varvec{e_j}. $$
Hence we want to pick
\(\alpha \) such that
$$\begin{aligned} \sum _{j \le k} \alpha _{k,j} (\lambda _j - \lambda _k) \varvec{e_j} + N \sum _{j \le k} \alpha _{k,j} \varvec{e_j} - \mu _{k-1} \varvec{\beta }_{k-1} \sum _{j < k} \alpha _{k-1,j} \varvec{e_j} = \varvec{0}. \end{aligned}$$
(11)
First note that these constraints are independent of
\(\varvec{\beta }\) if we set
\(\mu _{k-1} := \varvec{\beta }_{k-1}^{-1} > 0\), so we can leave assigning a value to
\(\varvec{\beta }\) to a later part of the proof.
We distinguish two cases. First, if
\(\lambda _{k-1} \ne \lambda _k\), then
\(\lambda _j - \lambda _k\) is positive for all
\(j < k\) because larger eigenvalues come first. Since
N is nilpotent and upper triangular,
\(N \sum _{j \le k} \alpha _{k,j} \varvec{e_j}\) is a linear combination of
\(\varvec{e_1}, \ldots , \varvec{e_{k-1}}\) (i.e., only the first
\(k-1\) entries are nonzero). Whatever values this vector assumes, we can increase the parameters
\(\alpha _{k,j}\) for
\(j < k\) to make (
11) larger and increase the parameters
\(\alpha _{k-1,j}\) for
\(j < k\) to make (
11) smaller.
Second, let
\(\ell \) be minimal such that
\(\lambda _\ell = \lambda _k\) wkth
\(\ell \ne k\), then
\(\varvec{w_\ell }, \ldots , \varvec{w_j}\) are from the same generalized eigenspace. For the rows
\(1, \ldots , \ell -1\) we can proceed as we did in the first case and for the rows
\(\ell , \ldots , k-1\) we note that by (
8)
\(N \varvec{e_j} = T_{j-1,j} \varvec{e_{j-1}}\). Hence the remaining constraints (
11) are
$$ \sum _{\ell< j \le k} \alpha _{k,j} T_{j-1,j} \varvec{e_{j-1}} - \mu _{k-1} \sum _{\ell \le j < k} \alpha _{k-1,j} \varvec{e_j} = \varvec{0}, $$
which is solved by
\(\alpha _{k,j+1} T_{j,j+1} = \alpha _{k-1,j}\) for
\(\ell \le j < k\). This is only a problem if there is a
j such that
\(T_{j-1,j} = 0\), i.e., if there are multiple Jordan blocks for the same eigenvalue. In this case, we can reduce the dimension of the generalized eigenspace to the dimension of the largest Jordan block by combining all Jordan blocks: if
\(M\varvec{y_k} = \lambda \varvec{y_k} + \varvec{y_{k-1}}\), and
\(M\varvec{y_j} = \lambda \varvec{y_j} + \varvec{y_{j-1}}\), then
\(M(\varvec{y_k} + \varvec{y_j}) = \lambda (\varvec{y_k} + \varvec{y_j}) + (\varvec{y_{k-1}} + \varvec{y_{j-1}})\) and if
\(M\varvec{y_k} = \lambda \varvec{y_k} + \varvec{y_{k-1}}\), and
\(M\varvec{y_j} = \lambda \varvec{y_j}\), then
\(M(\varvec{y_k} + \varvec{y_j}) = \lambda (\varvec{y_k} + \varvec{y_j}) + \varvec{y_{k-1}}\). In both cases we can replace the basis vector
\(\varvec{y_k}\) with
\(\varvec{y_k} + \varvec{y_j}\) without reducing the expressiveness of the GNTA.
Importantly, there are no cyclic dependencies in the values of
\(\alpha \) because neither one of the coefficients
\(\alpha \) can be made too large. Therefore we can choose
\(\alpha \ge 0\) such that (
10) is satisfied for all
\(k > 1\) and hence the basis
\(\varvec{y_1}, \ldots , \varvec{y_s}\) brings
M into the desired form (
1).
Part 2. In this part we construct the geometric nontermination argument and check the constraints from Definition
5. Since
L has an infinite execution, there is a point
\(\varvec{x}\) that fulfills the guard, i.e.,
\(G\varvec{x} \le \varvec{g}\). We choose
\(\varvec{x_1} := \varvec{x} + Y\varvec{\gamma }\) with
\(\varvec{\gamma }\ge \varvec{0}\) to be determined later. Moreover, we choose
\(\lambda _1, \ldots , \lambda _s\) and
\(\mu _1, \ldots , \mu _{s-1}\) from the entries of
U given in (
1). The size of our GNTA is
s, the number of vectors
\(\varvec{y_1}, \ldots , \varvec{y_s}\). These vectors form a basis of
\(\overline{\mathcal {Y}} \cap \mathcal {U}^\bot \), which is a subspace of
\(\mathbb {R}^n\); thus
\(s \le n\), as required.
The constraint (domain) is satisfied by construction and the constraint (init) is vacuous since
L is a loop program. For (ray) note that from (
9) and (
10) we get
The remainder of this proof shows that we can choose
\(\varvec{\beta }\) and
\(\varvec{\gamma }\) such that (point) is satisfied, i.e., that
$$\begin{aligned} G\varvec{x_1} \le \varvec{g} \text { and } M \varvec{x_1} + \varvec{m} = \varvec{x_1} + Y\varvec{1}. \end{aligned}$$
(12)
The vector
\(\varvec{x_1}\) satisfies the guard since
\(G\varvec{x_1} = G\varvec{x} + G Y \varvec{\gamma }\le \varvec{g} + \varvec{0}\) according to (
9), which yields the first part of (
12). For the second part we observe the following.
with
\(\varvec{\tilde{x}} := Y^{-1}\varvec{x} = W^{-1} \alpha ^{-1} \mathrm {diag}(\varvec{\beta })^{-1} \varvec{x}\) and
\(\varvec{\tilde{m}} := Y^{-1} \varvec{m} = W^{-1} \alpha ^{-1} \mathrm {diag}(\varvec{\beta })^{-1} \varvec{m}\). Equation (
13) is now conveniently in the basis
\(\varvec{y_1}, \ldots , \varvec{y_s}\) and all that remains to show is that we can choose
\(\varvec{\gamma }\ge \varvec{0}\) and
\(\varvec{\beta }> 0\) such that (
13) is satisfied.
We proceed for each (not quite Jordan) block of U separately, i.e., we assume that we are looking at the subspace \(\varvec{y_j}, \ldots , \varvec{y_k}\) with \(\mu _k = \mu _{j-1} = 0\) and \(\mu _\ell > 0\) for all \(\ell \in \{j,\ldots ,k-1\}\). If this space only contains eigenvalues that are larger than 1, then \(U - I\) is invertible and has only nonnegative entries. By using large enough values for \(\varvec{\beta }\), we can make \(\varvec{\tilde{x}}\) and \(\varvec{\tilde{m}}\) small enough, such that \(\varvec{1} \ge (U - I)\varvec{\tilde{x}} + \varvec{\tilde{m}}\). Then we just need to pick \(\varvec{\gamma }\) appropriately.
If there is at least one eigenvalue 1, then
\(U - I\) is not invertible, so (
13) could be overconstraint. Notice that
\(\mu _\ell > 0\) for all
\(\ell \in \{j,\ldots ,k-1\}\), so only the bottom entry in the vector Eq. (
13) is not covered by
\(\varvec{\gamma }\). Moreover, since eigenvalues are ordered in decreasing order and all eigenvalues in our current subspace are
\(\ge 1\), we conclude that the eigenvalue for the bottom entry is 1. (Furthermore,
k is the highest index since each eigenvalue occurs only in one block). Thus we get the equation
\(\varvec{\tilde{m}}_k = 1\). If
\(\varvec{\tilde{m}}_k\) is positive, this equation has a solution since we can adjust
\(\varvec{\beta }_k\) accordingly. If it is zero, then the execution on the space spanned by
\(\varvec{y_k}\) is bounded, which we can rule out by Lemma
12.
It remains to rule out that
\(\varvec{\tilde{m}}_k\) is negative. Let
\(\mathcal {U}\) be the generalized eigenspace to the eigenvector 1 and use Lemma
13 below to conclude that
\(\varvec{o} := N^{s-1}\varvec{m} + \varvec{u} \in \mathcal {Y}\) for some
\(\varvec{u} \in \mathcal {U}^\bot \). We have that
\(M\varvec{o} = M(N^{s-1}\varvec{m} + \varvec{u}) = M\varvec{u} \in \mathcal {U}^\bot \), so
\(\varvec{o}\) is a candidate to pick for the vector
\(\varvec{w_k}\). Therefore without loss of generality we did so in part 1 of this proof and since
\(\varvec{y_k}\) is in the convex cone spanned by the basis
\(\varvec{w_1}, \ldots , \varvec{w_s}\) we get
\(\varvec{\tilde{m}}_k > 0\).
\(\square \)