On Deciding Constant Runtime of Linear Loops
摘要
We consider linear single-path loops of the form \( {\textbf {while}} \quad \varphi \quad {\textbf {do}} \quad \textbf{x}\leftarrow A \textbf{x}+ \textbf{b} \quad {\textbf {end}} \) where \(\textbf{x}\) is a vector of variables, the loop guard \(\varphi \) is a conjunction of linear inequations over the variables \(\textbf{x}\) , and the update of the loop is represented by the matrix A and the vector \(\textbf{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.