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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

On Deciding Constant Runtime of Linear Loops

  • Florian Frohn,
  • Jürgen Giesl,
  • Peter Giesl,
  • Nils Lommen

摘要

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.