On Deciding Constant Runtime of Linear Loops

TL;DR

The paper studies whether a linear single-path loop with update $A x + b$ and a guard of linear inequalities has constant runtime across all inputs. It develops a decision procedure by deriving poly-exponential closed forms for the $n$-step update using the Jordan form when eigenvalues are non-negative real, and reduces constant-runtime to a first-order validity problem. Key steps include bounding the number of real roots of poly-exponential terms and applying a Fourier-Motzkin-type elimination to produce a univariate, algebraic-number decidable formula. The results establish decidability over the real numbers (and hence the rationals) for loops with real eigenvalues, extend to integers for eigenvalues in $oldsymbol{-1,0,1}$, and provide an implemented tool with practical evaluation. This work contributes to automated complexity and safety verification and lays groundwork toward multiphase-linear ranking functions, with future work on initial conditions and complex eigenvalues.

Abstract

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.