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.

翻译：本综述系统梳理了针对数值变量及线性约束定义转移关系的程序终止性分析技术。该程序分析子领域因存在不可判定问题而极具挑战性，本文系统探讨了缓解这一固有难度的研究方法，包括基础可判定性结论、排序函数方法以及析合良基转移不变式。综述同时讨论了用于证明程序不会终止的非终止见证方法。我们深入考察了这些方法的算法特性与计算复杂度，揭示了不同方法在表达能力和计算复杂度之间的权衡关系。本文不涉及现实编程语言的终止性分析技术，亦不讨论包含非线性算术、概率选择或项重写系统等更具表达能力的抽象模型。