We consider linear single-path loops of the form \[ \textbf{while} \quad \varphi \quad \textbf{do} \quad \vec{x} \gets A \vec{x} + \vec{b} \quad \textbf{end} \] where $\vec{x}$ is a vector of variables, the loop guard $\varphi$ is a conjunction of linear inequations over the variables $\vec{x}$, and the update of the loop is represented by the matrix $A$ and the vector $\vec{b}$. It is already known that termination of such loops is decidable. In this work, we consider loops where $A$ has real eigenvalues, and prove that it is decidable whether the loop's runtime (for all inputs) is bounded by a constant if the variables range over $\mathbb R$ or $\mathbb Q$. This is an important problem in automatic program verification, since safety of linear while-programs is decidable if all loops have constant runtime, and it is closely connected to the existence of multiphase-linear ranking functions, which are often used for termination and complexity analysis. To evaluate its practical applicability, we also present an implementation of our decision procedure.

翻译：我们考虑形式为\[ \textbf{while} \quad \varphi \quad \textbf{do} \quad \vec{x} \gets A \vec{x} + \vec{b} \quad \textbf{end} \]的线性单路径循环，其中$\vec{x}$是变量向量，循环守卫$\varphi$是变量$\vec{x}$上线性不等式的合取，循环的更新由矩阵$A$和向量$\vec{b}$表示。已知此类循环的终止性是可判定的。在本工作中，我们考虑$A$具有实特征值的循环，并证明当变量取值范围为$\mathbb R$或$\mathbb Q$时，循环的运行时间（对所有输入）是否有常数上界是可判定的。这是自动程序验证中的一个重要问题，因为若所有循环均具有常数运行时间，则线性while程序的安全性是可判定的，且该问题与多相线性秩函数的存在性密切相关，后者常用于终止性和复杂性分析。为评估其实用性，我们还给出了判定过程的实现。