论文标题
在多项式空间中的循环程序的紧密多项式边界
Tight Polynomial Bounds for Loop Programs in Polynomial Space
论文作者
论文摘要
我们考虑以下问题：给定一个程序，在计算末尾（或任何给定程序点）的某些变量的值中找到紧密的渐近界限，以其输入值。我们专注于多项式结合变量的情况，以及一种弱编程语言，我们最近表明，多项式结合变量的紧密界限是可计算的。这些边界是多元多项式的集合。尽管它们的可计算性已经解决，但该程序分析问题的复杂性仍然开放。在本文中，我们表明问题是PSPACE完成的。主要贡献是一种新的，空间效率的分析算法。该算法以几个步骤获得。首先，我们开发了一种用于单变量界限的算法，该算法已经是Pspace-Hard。然后，通过将此问题减少到单变量案例来实现多变量界限的决策程序；这种还原与单变量问题的解决方案是正交的，并在代表多元边界的一组向量的几何形状上使用观察结果。最后，我们将单变量结合的算法转换为产生多元边界。
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.
