# Item

ITEM ACTIONSEXPORT

Released

Paper

#### On the Decidability of Termination for Polynomial Loops

##### External Resource

No external resources are shared

##### Fulltext (restricted access)

There are currently no full texts shared for your IP range.

##### Fulltext (public)

arXiv:1910.11588.pdf

(Preprint), 455KB

##### Supplementary Material (public)

There is no public supplementary material available

##### Citation

Frohn, F., Hark, M., & Giesl, J. (2019). On the Decidability of Termination for Polynomial Loops. Retrieved from https://arxiv.org/abs/1910.11588.

Cite as: https://hdl.handle.net/21.11116/0000-0007-CEE8-C

##### Abstract

We consider the termination problem for triangular weakly non-linear loops

(twn-loops) over some ring $\mathcal{S}$ like $\mathbb{Z}$, $\mathbb{Q}$, or

$\mathbb{R}$. Essentially, the guard of such a loop is an arbitrary Boolean

formula over (possibly non-linear) polynomial inequations, and the body is a

single assignment $(x_1, \ldots, x_d) \longleftarrow (c_1 \cdot x_1 + p_1,

\ldots, c_d \cdot x_d + p_d)$ where each $x_i$ is a variable, $c_i \in

\mathcal{S}$, and each $p_i$ is a (possibly non-linear) polynomial over

$\mathcal{S}$ and the variables $x_{i+1},\ldots,x_{d}$. We present a reduction

from the question of termination to the existential fragment of the first-order

theory of $\mathcal{S}$ and $\mathbb{R}$. For loops over $\mathbb{R}$, our

reduction entails decidability of termination. For loops over $\mathbb{Z}$ and

$\mathbb{Q}$, it proves semi-decidability of non-termination.

Furthermore, we present a transformation to convert certain non-twn-loops

into twn-form. Then the original loop terminates iff the transformed loop

terminates over a specific subset of $\mathbb{R}$, which can also be checked

via our reduction. This transformation also allows us to prove tight complexity

bounds for the termination problem for two important classes of loops which can

always be transformed into twn-loops.

(twn-loops) over some ring $\mathcal{S}$ like $\mathbb{Z}$, $\mathbb{Q}$, or

$\mathbb{R}$. Essentially, the guard of such a loop is an arbitrary Boolean

formula over (possibly non-linear) polynomial inequations, and the body is a

single assignment $(x_1, \ldots, x_d) \longleftarrow (c_1 \cdot x_1 + p_1,

\ldots, c_d \cdot x_d + p_d)$ where each $x_i$ is a variable, $c_i \in

\mathcal{S}$, and each $p_i$ is a (possibly non-linear) polynomial over

$\mathcal{S}$ and the variables $x_{i+1},\ldots,x_{d}$. We present a reduction

from the question of termination to the existential fragment of the first-order

theory of $\mathcal{S}$ and $\mathbb{R}$. For loops over $\mathbb{R}$, our

reduction entails decidability of termination. For loops over $\mathbb{Z}$ and

$\mathbb{Q}$, it proves semi-decidability of non-termination.

Furthermore, we present a transformation to convert certain non-twn-loops

into twn-form. Then the original loop terminates iff the transformed loop

terminates over a specific subset of $\mathbb{R}$, which can also be checked

via our reduction. This transformation also allows us to prove tight complexity

bounds for the termination problem for two important classes of loops which can

always be transformed into twn-loops.