Generating Asymptotically Non-Terminating Initial Values for Linear Programs

TL;DR

This paper introduces a method to generate and analyze initial variable values that lead to non-termination in linear loop programs, providing tools for automatic analysis of program termination behavior.

Contribution

It presents a novel approach to compute semi-linear sets of asymptotically non-terminating initial values and extends the analysis to affine integer and rational programs.

Findings

Sets of non-terminating initial values can be symbolically represented.

The approach provides a precise under-approximation of terminating inputs.

Decidability results are extended to integer and rational programs.

Abstract

We present the notion of asymptotically non-terminating initial variable values for linear loop programs. Those values are directly associated to initial variable values for which the corresponding program does not terminate. Our theoretical contributions provide us with powerful computational methods for automatically generating sets of asymptotically non-terminating initial variable values. Such sets are represented symbolically and exactly by a semi-linear space, e.g., characterized by conjunctions and disjunctions of linear equalities and inequalities. Moreover, by taking their complements, we obtain a precise under-approximation of the set of inputs for which the program does terminate. We can then reduce the termination problem of linear programs to the emptiness check of a specific set of asymptotically non-terminating initial variable values. Our static input data analysis is not restricted only to programs where the variables are interpreted over the reals. We extend our approach and provide new decidability results for the termination problem of affine integer and rational programs.