Termination of triangular polynomial loops

Formal Methods in System Design, vol. 65, pp. 70–132

Abstract

Abstract We consider the problem of proving termination for triangular weakly non-linear loops (twn-loops) over some ring $$\mathcal {S}$$ S like $$\mathbb {Z}$$ Z , $$\mathbb {Q}$$ Q , or $$\mathbb {R}$$ R . The guard of such a loop is an arbitrary quantifier-free Boolean formula over (possibly non-linear) polynomial inequations, and the body is a single assignment of the form $$\begin{bmatrix} x_1\\ \ldots \\ x_d \end{bmatrix} \leftarrow \begin{bmatrix} c_1 \cdot x_1 + p_1\\ \ldots \\ c_d \cdot x_d + p_d \end{bmatrix}$$ x 1 … x d ← c 1 · x 1 + p 1 … c d · x d + p d where each $$x_i$$ x i is a variable, $$c_i \in \mathcal {S}$$ c i ∈ S , and each $$p_i$$ p i is a (possibly non-linear) polynomial over $$\mathcal {S}$$ S and the variables $$x_{i+1},\ldots ,x_{d}$$ x i + 1 , … , x d . We show that the question of termination can be reduced to the existential fragment of the first-order theory of $$\mathcal {S}$$ S . For loops over $$\mathbb {R}$$ R , our reduction implies decidability of termination. For loops over $$\mathbb {Z}$$ Z and

Authors 3

1. Marcel Hark Aachen LuFG Informatik 2

   RWTH Aachen University

   Affiliation as printed

   LuFG Informatik 2, RWTH Aachen University, Aachen, Germany

2. Florian Frohn Aachen LuFG Informatik 2

   RWTH Aachen University · Max Planck Institute for Informatics

   Affiliation as printed

   LuFG Informatik 2, RWTH Aachen University, Aachen, Germany

   Max Planck Institute for Informatics, Saarland Informatics Campus, Saarbrücken, Germany

   Max Planck Institute for Informatics, Saarbrücken, Germany

3. Jürgen Giesl corresponding Aachen LuFG Informatik 2

   RWTH Aachen University

   Affiliation as printed

   LuFG Informatik 2, RWTH Aachen University, Aachen, Germany