On the Termination of Linear and Affine Programs over the Integers

TL;DR

This paper proves that the termination problem for affine programs over integers is decidable for almost all cases, introduces the ANT set concept, and provides methods to compute and analyze termination conditions.

Contribution

It introduces the ANT set framework for analyzing termination of affine programs over integers and offers computational methods to determine termination behavior.

Findings

Termination is decidable for almost all affine programs over Z.

ANT sets are semi-linear and computable.

Provides a method for under-approximating terminating inputs.

Abstract

The termination problem for affine programs over the integers was left open in\cite{Braverman}. For more that a decade, it has been considered and cited as a challenging open problem. To the best of our knowledge, we present here the most complete response to this issue: we show that termination for affine programs over Z is decidable under an assumption holding for almost all affine programs, except for an extremely small class of zero Lesbegue measure. We use the notion of asymptotically non-terminating initial variable values} (ANT, for short) for linear loop programs over Z. Those values are directly associated to initial variable values for which the corresponding program does not terminate. We reduce the termination problem of linear affine programs over the integers to the emptiness check of a specific ANT set of initial variable values. For this class of linear or affine programs, we prove that the corresponding ANT set is a semi-linear space and we provide a powerful computational methods allowing the automatic generation of these $ANT$ sets. Moreover, we are able to address the conditional termination problem too. In other words, by taking ANT set complements, we obtain a precise under-approximation of the set of inputs for which the program does terminate.