Recursive Abstractions for Parameterized Systems
Joxan Jaffar and Andrew Santosa
Abstract
We consider a language of recursively defined formulas about arrays of
variables, suitable for specifying safety properties of parameterized
systems. We then present an abstract interpretation framework which
translates a paramerized system as a symbolic transition system which
propagates such formulas as abstractions of underlying concrete
states. The main contribution is a proof method for implications
between the formulas, which then provides for an implementation of
this abstract interpreter.