Bounded Termination of Monotonicity-Constraint Transition Systems

Intuitively, if we can prove that a program terminates, we expect some conclusion re-garding its complexity. But the passage from termination proofs to complexity bounds is not always clear. In this work we consider Monotonicity Constraint Transition Systems, a program abstraction where termination is decidable (based on the size-change termination principle). We show that these programs also have a decidable complexity property: one can determine whether the length of all transition sequences can be bounded in terms of the initial state. This is the bounded termination problem. Interestingly, if a bound exists, it must be polynomial. We prove that the bounded termination problem is PSPACE-complete and, moreover, if a bound exists then a symbolic bound which is constant-factor tight (in the univariate case) can be computed in PSPACE. We present this computation in the form of computing a reachability bound, a bound on the number of visits to a given program location. This presentation is inspired by the practical usefulness of this problem formulation. We also discuss, theoretically, the use of bounds on the abstract program to infer conclu-sions on a concrete program that has been abstracted. The conclusion maybe a polynomial time bound, or in other cases polynomial space or exponential time. We argue that the monotonicity-constraint abstraction promises to be useful for practical complexity analysis of programs.