Tight polynomial worst-case bounds for loop programs
Ben-Amram, Amir M. and Hamilton, GeoffORCID: 0000-0001-5954-6444
(2020)
Tight polynomial worst-case bounds for loop programs.
Logical Methods in Computer Science, 16
(2).
4:1-4:39.
ISSN 1860-5974
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.
Item Type:
Article (Published)
Refereed:
Yes
Additional Information:
First published 5 Apr 2019 in International Conference on Foundations of Software Science and Computation Structures
FoSSaCS 2019: Foundations of Software Science and Computation Structures pp 80-97 as part of Lecture Notes in Computer Science, vol 11425. pp Springer, Cham. ISBN 978-3-030-17126-1
DOI: https://doi-org.dcu.idm.oclc.org/10.1007/978-3-030-17127-8_5