Reachability Analysis of Multi-affine Systems

We present a computationally attractive technique to study the reachability of rectangular regions by trajectories of continuous multi-affine systems. The method is iterative. At each step, finer parti-tions and finite quotients that over-approximate the reachability properties of the initial system are produced. We exploit some convexity properties of multi-affine functions on rectangles to show that the construction of the quotient at each step requires only the evaluation of the vector field at the set of all vertices of all rectangles in the partition and finding the roots of a finite set of scalar affine functions. This methodology can be used for formal analysis of biochemical networks, aircraft and underwater vehicles, where multi-affine models are widely used.