Abstract

Matrix interpretations are widely used in automated complexity analysis. Certifying such analyses boils down to determining the growth rate of Aⁿ for a fixed non-negative rational matrix A. There exists a conceptually simple algorithm to determine the growth rate, but this algorithm has the disadvantage that it is based on algebraic number computations.
In this work we present an even simpler algorithm to compute the growth rate. Its soundness is based on a variant of a Perron–Frobenius theorem that has been conjectured in earlier work. So far it only has been proven for small matrices, and here we present a proof for the general case.
We further verify both the algorithm and the new Perron–Frobenius theorem in the proof assistant Isabelle/HOL, and integrate it into CeTA, a verified certifier for various properties, including complexity proofs. Because of the new results, CeTA no longer requires a verified implementation of algebraic numbers.

BibTeX

@article{Thi21,
  author    = {Ren\'e Thiemann},
  title     = {A {P}erron--{F}robenius theorem for deciding matrix growth},
  journal   = {J. Log. Algebraic Methods Program.},
  volume    = {123},
  year      = {2021},
  doi       = {10.1016/j.jlamp.2021.100699}
}