Symbolic Reachability Computation of A Class of Nonlinear Systems

Reachability is recognized as a key problem in designing physical control systems (most are nonlinear systems) in formal method community. Issues related to stability and controllability of physical systems are well studied in control theory. However there are not many results on reachability of those systems and fewer on nonlinear systems in computer science yet. In this paper we present the first known family of nonlinear systems with the decidable symbolic computation problem of their reachable state spaces at the best of our knowledge. This is approached by reducing reachability computation to semi-algebraic system solving. Furthermore we illustrate the application of our method by performing the Maple package DISCOVERER.