Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Termination Analysis of Linear-Constraint Programs

Amir M. Ben-Amram, Samir Genaim, Joël Ouaknine, James Worrell

TL;DR

This survey addresses termination analysis for linear-constraint programs, where numerical variables evolve under linear transitions. It surveys three core approaches: ranking functions (LRFs/LLRFs and their variants), disjunctive well-founded invariants (DTIs) for decomposing proofs across multiple cycles, and non-termination witnesses (recurrent sets) to certify infinite behavior. It presents decidability landscapes across real, rational, and integer domains, highlighting complete algorithms for affine single-path loops, partial results for SLC/MLC, and undecidability for broader multi-path models. The work emphasizes algorithmic trade-offs between expressive power and complexity, covering polyhedral techniques, invariant synthesis, and various specialized loop classes (octagonal, gap/monotonicity constraints, etc.), while noting open problems and the limitations of current methods. Collectively, these insights underpin practical termination analysis tools and guide future theoretical advances in linear-constraint programming analysis.

Abstract

This Survey provides an overview of techniques in termination analysis for programs with numerical variables and transitions defined by linear constraints. This subarea of program analysis is challenging due to the existence of undecidable problems, and this Survey systematically explores approaches that mitigate this inherent difficulty. These include foundational decidability results, the use of ranking functions, and disjunctive well-founded transition invariants. The Survey also discusses non-termination witnesses, used to prove that a program will not halt. We examine the algorithmic and complexity aspects of these methods, showing how different approaches offer a trade-off between expressive power and computational complexity. The Survey does not discuss how termination analysis is performed on real-world programming languages, nor does it consider more expressive abstract models that include non-linear arithmetic, probabilistic choice, or term rewriting systems.

Termination Analysis of Linear-Constraint Programs

TL;DR

This survey addresses termination analysis for linear-constraint programs, where numerical variables evolve under linear transitions. It surveys three core approaches: ranking functions (LRFs/LLRFs and their variants), disjunctive well-founded invariants (DTIs) for decomposing proofs across multiple cycles, and non-termination witnesses (recurrent sets) to certify infinite behavior. It presents decidability landscapes across real, rational, and integer domains, highlighting complete algorithms for affine single-path loops, partial results for SLC/MLC, and undecidability for broader multi-path models. The work emphasizes algorithmic trade-offs between expressive power and complexity, covering polyhedral techniques, invariant synthesis, and various specialized loop classes (octagonal, gap/monotonicity constraints, etc.), while noting open problems and the limitations of current methods. Collectively, these insights underpin practical termination analysis tools and guide future theoretical advances in linear-constraint programming analysis.

Abstract

This Survey provides an overview of techniques in termination analysis for programs with numerical variables and transitions defined by linear constraints. This subarea of program analysis is challenging due to the existence of undecidable problems, and this Survey systematically explores approaches that mitigate this inherent difficulty. These include foundational decidability results, the use of ranking functions, and disjunctive well-founded transition invariants. The Survey also discusses non-termination witnesses, used to prove that a program will not halt. We examine the algorithmic and complexity aspects of these methods, showing how different approaches offer a trade-off between expressive power and computational complexity. The Survey does not discuss how termination analysis is performed on real-world programming languages, nor does it consider more expressive abstract models that include non-linear arithmetic, probabilistic choice, or term rewriting systems.

Paper Structure

This paper contains 82 sections, 52 theorems, 135 equations, 10 figures, 2 tables, 2 algorithms.

Table of Contents

  1. Introduction
  2. Organisation of this Survey.
  3. Preliminaries
  4. Mathematical Background
  5. Notations
  6. Eigenvectors and Eigenvalues
  7. Exponential Polynomials
  8. Convexity
  9. Lattices
  10. Multiplicative Relations
  11. Polyhedra and Linear Programming
  12. Polyhedra
  13. Integer Polyhedra
  14. Generator Representation
  15. Size of Polyhedra
  16. ...and 67 more sections

Key Result

Proposition 2.1

Let $S = \{\bm{a}_1,\ldots,\bm{a}_n\} \subseteq \mathbb R\xspace^n$. Then $\bm{u}$ lies in the relative interior of $\mathtt{conv}(S)$ if and only if there exist $\alpha_1,\ldots,\alpha_n > 0$ such that $\bm{u}=\sum_{i=1}^n \alpha_i \bm{a}_i$ and $\sum_{i=1}^n \alpha_i = 1$.

Figures (10)

  • Figure 1: A polyhedron ${\mathcal{P}}$ and its integer hull ${{\mathcal{P}}}_I$ (Figure from BG14).
  • Figure 2: A program, its corresponding CFG, and invariants.
  • Figure 3: Illustration (from BIK14) of various notions for a difference bounds relation $R$ defoned by $\{ x_2- x'_1\leq -1 ,\, x_3- x'_2\leq 0 ,\, x_1- x'_3\leq 0 ,\, x'_4- x_4\leq 0 ,\, x'_3- x_4\leq 0\}$.
  • Figure 4: The polyhedra associated with two of our examples, projected to two dimensions: (A) corresponds to Loop \ref{['eq:bg:loop1']} on Page \ref{['eq:bg:loop1']}; (B) corresponds to Loop \ref{['eq:bg:loop2']} on Page \ref{['eq:bg:loop2']}. Dashed lines are added when computing the integer hull; dotted areas represent the integer hull; Gray areas are rational points eliminated when computing the integer hull (Figure from BG14).
  • Figure 5: A program (taken from ADFG:2010), its corresponding CFG, and invariants when starting location $l_0$).
  • ...and 5 more figures

Theorems & Definitions (170)

  • Proposition 2.1
  • Theorem 2.1: Flatness Theorem
  • Theorem 2.2: DinZ10KP97
  • Theorem 2.3
  • Example 2.1
  • Example 2.2
  • Example 2.3
  • Example 2.4
  • Example 2.5
  • Remark 2.1
  • ...and 160 more