Reachability Analysis for Polynomial Dynamical Systems Using the Bernstein Expansion

Abstract

This paper is concerned with the reachability computation problem for polynomial dynamical systems. Such computations constitute a crucial component in algorithmic verification tools for hybrid systems and embedded software with polynomial dynamics, which have found applications in many engineering domains. We describe two methods for overapproximating reachable sets of such systems; these methods are based a combination of the Bernstein expansion of polynomial functions and a representation of reachable sets by template polyhedra. Using a prototype implementation, the performance of the methods was demonstrated on a number of examples of control systems and biological systems. 1