一句话：为带界循环的非确定性命令式程序提出算法，自动求出渐近紧的多变量析取多项式最坏情况界。
2008年 Ben-Amram、Jones 与 Kristiansen 已证明，对仅含加乘算术、带界循环的非确定性命令式程序，可精确判定某个计算值或运行时间是否具有多项式增长率。本文把该判定问题推进为定量问题：计算渐近紧的多变量析取多项式上界。作者给出完整解法——只要存在多项式界就一定能找到，并设计了相当简单但依赖精细论证的算法；证明关键构件是森林分解定理，即关于到有限幺半群同态的强结构结果。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{Ben-AmramH20,
title = {Tight Polynomial Worst-Case Bounds for Loop Programs},
author = {Amir M. Ben-Amram and Geoff Hamilton},
journal = {Logical Methods in Computer Science},
volume = {Volume 16, Issue 2},
year = {2020},
doi = {10.23638/lmcs-16(2:4)2020}
}