一句话：证明循环程序紧多项式界计算问题是 PSPACE 完全，并给出空间高效分析算法。
论文研究如何为循环程序计算变量在计算结束或任意程序点处相对于输入的紧渐近界，重点关注多项式有界变量和一个弱编程语言。此前已知该语言的多项式界可计算，但其复杂度未定。作者先给出单变量界的空间高效算法，并指出该子问题已是 PSPACE 难；随后利用表示多变量界的向量集合的几何性质，将多变量界的判定归约到单变量情形，并改造单变量算法使其生成多变量界。由此证明该程序分析问题是 PSPACE 完全的。该结果给出了问题的精确复杂度，并提供空间高效的分析方法。
We consider the following problem: given a program, find tight asymptotic bounds on the values of some variables at the end of the computation (or at any given program point) in terms of its input values. We focus on the case of polynomially-bounded variables, and on a weak programming language for which we have recently shown that tight bounds for polynomially-bounded variables are computable. These bounds are sets of multivariate polynomials. While their computability has been settled, the complexity of this program-analysis problem remained open. In this paper, we show the problem to be PSPACE-complete. The main contribution is a new, space-efficient analysis algorithm. This algorithm is obtained in a few steps. First, we develop an algorithm for univariate bounds, a sub-problem which is already PSPACE-hard. Then, a decision procedure for multivariate bounds is achieved by reducing this problem to the univariate case; this reduction is orthogonal to the solution of the univariate problem and uses observations on the geometry of a set of vectors that represent multivariate bounds. Finally, we transform the univariate-bound algorithm to produce multivariate bounds.
@article{paperbot1268,
title = {Tight Polynomial Bounds for Loop Programs in Polynomial Space},
author = {A. M. Ben-Amram and G. W. Hamilton},
journal = {Logical Methods in Computer Science},
volume = {Volume 17, Issue 4},
year = {2021},
doi = {10.46298/lmcs-17(4:7)2021}
}