On termination and divergence of linear programs

Thesis

The objective of this thesis is to shed some light on the boundaries of decidability by answering some of the central problems in the study of linear programs, and to provide an up-to-date survey of the latest results in this field.

In particular, we review some of the classical decision problems in the theory of linear recurrence sequences. Namely, we revisit the Skolem Problem, Positivity Problem, Ultimate Positivity Problem, and Absolute Divergence Problem. We then show that the Divergence Problem, the problem of deciding whether a given linear recurrence sequence diverges to infinity, is decidable for all linear recurrence sequences of order at most 5, and when the linear recurrence sequence is simple it is decidable up to order 8. Our results hold for both homogeneous and inhomogeneous linear recurrence sequences. As a by-product of our approach, we extend existing results on the Positivity Problem and Ultimate Positivity Problem for homogeneous linear recurrence sequences to inhomogeneous linear recurrence sequences. We further demonstrate why it is unlikely to improve these decidability boundaries to higher order linear recurrence sequences, by establishing reductions from long-lasting open problems in Diophantine Approximation.

Next, we answer a 15-year-old problem of Tiwari, which asks whether a given linear loop program with integer coefficients terminates over all its integer initial values. We use novel techniques to evade the obstacles in answering the Positivity and Ultimate Positivity Problems. In more detail, we exploit the freedom to choose the initial value to circumvent the need to solve “hard instances” of the Positivity Problem. Our algorithm decides, in double exponential space, whether a linear loop program with integer coefficients terminates over all integer initial values.

Finally, we summarise the state-of-the-art results in the field, and provide the reader with a landscape of some of the new and classical open problems in the field. We also discuss some of the shortcomings of the current approaches, and provide direction for further research.

Authors: Hosseini, M

• Type of award: DPhil
• Level of award: Doctoral
• Awarding institution: University of Oxford
• Language: English
• Keywords: algebraic numbers; Skolem problem; divergence; program verification; positivity; linear recurrence sequences; integer affine programs; integer linear programs; loop termination