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. |
Year | DOI | Venue |
---|---|---|
2019 | 10.23638/LMCS-16(2:4)2020 | LOGICAL METHODS IN COMPUTER SCIENCE |
Keywords | DocType | Volume |
asymptotically-tight,multivariate,disjunctive,worst-case,polynomial bounds | Journal | 16 |
Issue | ISSN | Citations |
2 | 1860-5974 | 0 |
PageRank | References | Authors |
0.34 | 0 | 2 |
Name | Order | Citations | PageRank |
---|---|---|---|
Amir M Ben-Amram | 1 | 327 | 30.52 |
G. W. Hamilton | 2 | 52 | 6.64 |