A. M. Ben-Amram ; G. W. Hamilton - Tight Polynomial Bounds for Loop Programs in Polynomial Space

lmcs:6832 - Logical Methods in Computer Science, November 11, 2021, Volume 17, Issue 4 - https://doi.org/10.46298/lmcs-17(4:7)2021
Tight Polynomial Bounds for Loop Programs in Polynomial SpaceArticle

Authors: A. M. Ben-Amram ; G. W. Hamilton

    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.


    Volume: Volume 17, Issue 4
    Published on: November 11, 2021
    Accepted on: September 17, 2021
    Submitted on: October 8, 2020
    Keywords: Computer Science - Logic in Computer Science,F.2.0,F.2.0

    Consultation statistics

    This page has been seen 1461 times.
    This article's PDF has been downloaded 300 times.