On Deciding Constant Runtime of Linear Loops

Florian Frohn, Jürgen Giesl, Peter Giesl +1

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 vecto…