hybridization domain construction using curvature estimation
This paper is concerned with the reachability computation for non-linear systems using hybridization. The main idea of hybridization is to approximate a non-linear vector field by a piecewise-affine one. The piecewise-affine vector field is defined by building around the set of current states of the system a simplicial domain and using linear interpolation over its vertices. To achieve a good time-efficiency and accuracy of the reachability computation on the approximate system, it is important to find a simplicial domain which, on one hand, is as large as possible and, on the other hand, guarantees a small interpolation error. In our previous work[8], we proposed a method for constructing hybridization domains based on the curvature of the dynamics and showed how the method can be applied to quadratic systems. In this paper we pursue this work further and present two main results. First, we prove an optimality property of the domain construction method for a class of quadratic systems. Second, we propose an algorithm of curvature estimation for more general non-linear systems with non-constant Hessian matrices. This estimation can then be used to determine efficient hybridization domains. We also describe some experimental results to illustrate the main ideas of the algorithm as well as its performance.
hybrid systems formal verification reachability analysis