# Tight Polynomial Worst-Case Bounds for Loop Programs

## TL;DR

This paper presents a simple yet rigorous method for deriving tight polynomial upper bounds for the growth rates of non-deterministic imperative programs with bounded loops, extending previous decision results to quantitative bounds.

## Contribution

It introduces a complete algorithm for obtaining asymptotically-tight polynomial bounds for a class of programs, leveraging the forest factorization theorem for structural analysis.

## Key findings

- The algorithm reliably finds polynomial bounds when they exist.
- The method is simple despite relying on subtle reasoning.
- It extends previous decision procedures to quantitative bounds.

## Abstract

In 2008, Ben-Amram, Jones and Kristiansen showed that for a simple programming language - representing non-deterministic imperative programs with bounded loops, and arithmetics limited to addition and multiplication - it is possible to decide precisely whether a program has certain growth-rate properties, in particular whether a computed value, or the program's running time, has a polynomial growth rate. A natural and intriguing problem was to move from answering the decision problem to giving a quantitative result, namely, a tight polynomial upper bound. This paper shows how to obtain asymptotically-tight, multivariate, disjunctive polynomial bounds for this class of programs. This is a complete solution: whenever a polynomial bound exists it will be found. A pleasant surprise is that the algorithm is quite simple; but it relies on some subtle reasoning. An important ingredient in the proof is the forest factorization theorem, a strong structural result on homomorphisms into a finite monoid.