Termination of programs over the union of intervals
Lin Mu, Yi Li, Taige Jin, Jiawei Luo · 2010
For a generic loop: while (constraints) {updates} it is well known that the termination problem is undecidable in general, even for a simple class of polynomial programs. If the constraints or the updating function in the above loop is not linear, the loop is called nonlinear. In this paper, we investigate how to solve the termination of the above loop by deciding whether a fixed point exists, when the constraints are the union of intervals and the updating functions are polynomials. Furthermore, when all fixed points are on the boundaries of the union of intervals, we also establish a corresponding necessary and sufficient condition of nontermination.