@online{Frohn_arXiv1910.11588,
TITLE = {On the Decidability of Termination for Polynomial Loops},
AUTHOR = {Frohn, Florian and Hark, Marcel and Giesl, J{\"u}rgen},
LANGUAGE = {eng},
URL = {https://arxiv.org/abs/1910.11588},
EPRINT = {1910.11588},
EPRINTTYPE = {arXiv},
YEAR = {2019},
ABSTRACT = {We consider the termination problem for triangular weakly non-linear loops<br>(twn-loops) over some ring $\mathcal{S}$ like $\mathbb{Z}$, $\mathbb{Q}$, or<br>$\mathbb{R}$. Essentially, the guard of such a loop is an arbitrary Boolean<br>formula over (possibly non-linear) polynomial inequations, and the body is a<br>single assignment $(x_1, \ldots, x_d) \longleftarrow (c_1 \cdot x_1 + p_1,<br>\ldots, c_d \cdot x_d + p_d)$ where each $x_i$ is a variable, $c_i \in<br>\mathcal{S}$, and each $p_i$ is a (possibly non-linear) polynomial over<br>$\mathcal{S}$ and the variables $x_{i+1},\ldots,x_{d}$. We present a reduction<br>from the question of termination to the existential fragment of the first-order<br>theory of $\mathcal{S}$ and $\mathbb{R}$. For loops over $\mathbb{R}$, our<br>reduction entails decidability of termination. For loops over $\mathbb{Z}$ and<br>$\mathbb{Q}$, it proves semi-decidability of non-termination.<br> Furthermore, we present a transformation to convert certain non-twn-loops<br>into twn-form. Then the original loop terminates iff the transformed loop<br>terminates over a specific subset of $\mathbb{R}$, which can also be checked<br>via our reduction. This transformation also allows us to prove tight complexity<br>bounds for the termination problem for two important classes of loops which can<br>always be transformed into twn-loops.<br>},
}