{
  "annotation_id": "75109346-1476-44a0-9d72-815b56a0bbe4",
  "date_created": "2026-02-17T05:53:15.216000Z",
  "date_modified": "2026-02-17T05:53:15.216000Z",
  "file_hash": "8bcaff6cd789e82e48876ee83069bd86c3c2e1d609db2ab766720112605ef17b",
  "private": false,
  "record": {
    "abstract": "We consider linear single-path loops of the form \\[\n  \\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\u0027s 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.",
    "arxiv_id": "2601.08492",
    "authors": [
      "Florian Frohn",
      "J\u00fcrgen Giesl",
      "Peter Giesl",
      "Nils Lommen"
    ],
    "categories": [
      "cs.LO"
    ],
    "license": "http://arxiv.org/licenses/nonexclusive-distrib/1.0/",
    "title": "On Deciding Constant Runtime of Linear Loops",
    "url": "https://arxiv.org/abs/2601.08492",
    "version": "v1"
  },
  "schema_id": "dorsal/arxiv",
  "source": {
    "execution_id": "9f929ac7-b217-4840-ad14-da752cd30899",
    "id": "arXiv Dataset",
    "type": "Model",
    "variant": "snapshot-2026-01-17",
    "version": "0.1.0"
  },
  "user_id": 1000002
}