This paper shows how techniques for linear dynamical systems can be used to reason about the behavior of general loops. We present two main results. First, we show that every loop that can be expressed as a transition formula in linear integer arithmetic has a best model as a deterministic affine transition system. Second, we show that for any linear dynamical system $f$ with integer eigenvalues and any integer arithmetic formula $G$, there is a linear integer arithmetic formula that holds exactly for the states of $f$ for which $G$ is eventually invariant. Combining the two, we develop a monotone conditional termination analysis for general loops.

翻译：本文展示了线性动态系统的技术如何用于解释一般循环的行为。 我们展示了两个主要结果。 首先, 我们展示了每个可以以线性整数算术的过渡公式表示的循环都有最佳模型作为确定性方形过渡系统。 其次, 我们展示了对于任何具有整数电子元值和任何整数算术公式的线性动态系统来说, 有一个线性整数算术公式, 正好维持在$f$的状态上, 而$G$最终是不可变的。 合并了这两个循环, 我们为一般循环开发了一个单一的有条件终止分析。