Closed Forms for Numerical Loops
Zachary Kincaid, Jason Breck, John Cyphert, and Thomas Reps
This paper investigates the problem of reasoning about non-linear
behavior of simple numerical loops. Our approach builds on classical
techniques for analyzing the behavior of linear dynamical systems.
It is well-known that a closed-form representation of the behavior of
a linear dynamical system can always be expressed using algebraic
numbers, but this approach can create formulas that present an
obstacle for automated-reasoning tools.
This paper characterizes when linear loops have closed forms in
simpler theories that are more amenable to automated reasoning.
The algorithms for computing closed forms described in the paper
avoid the use of algebraic numbers, and produce closed forms
expressed using polynomials and exponentials over rational numbers.
We show that the logic for expressing closed forms is decidable,
yielding decision procedures for verifying safety and termination of
a class of numerical loops over rational numbers.
We also show that the procedure for computing closed forms for this
class of numerical loops can be used to over-approximate the behavior
of arbitrary numerical programs (with unrestricted control flow,
non-deterministic assignments, and recursive
procedures).
(Click here to access the paper:
PDF.)