Paper detail

On Deciding Constant Runtime of Linear Loops

We consider linear single-path loops of the form \[ \textbf{while} \quad φ\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 $φ$ 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.