Termination of Linear Programs with Nonlinear Constraints

TL;DR

This paper investigates the decidability of termination for loops with polynomial conditions and linear updates, showing undecidability over integers and proposing an algorithm for a specific real case under certain assumptions.

Contribution

It extends previous work by analyzing polynomial conditions, proving undecidability over integers, and providing a decision algorithm for a restricted real case.

Findings

Termination over integers is undecidable.

A complete algorithm is provided for a class of real loops under an assumption.

Conjecture that general real case termination is undecidable.

Abstract

Tiwari proved that termination of linear programs (loops with linear loop conditions and updates) over the reals is decidable through Jordan forms and eigenvectors computation. Braverman proved that it is also decidable over the integers. In this paper, we consider the termination of loops with polynomial loop conditions and linear updates over the reals and integers. First, we prove that the termination of such loops over the integers is undecidable. Second, with an assumption, we provide an complete algorithm to decide the termination of a class of such programs over the reals. Our method is similar to that of Tiwari in spirit but uses different techniques. Finally, we conjecture that the termination of linear programs with polynomial loop conditions over the reals is undecidable in general by %constructing a loop and reducing the problem to another decision problem related to number theory and ergodic theory, which we guess undecidable.