Avoiding geometric intersection operations in reachability analysis of hybrid systems

Although a growing number of dynamical systems studied in various fields are hybrid in nature, the verification of properties, such as stability, safety, etc., is still a challenging problem. Reachability analysis is one of the promising methods for hybrid system verification, which together with all other verification techniques faces the challenge of making the analysis scale with respect to the number of continuous state variables. The bottleneck of many reachability analysis techniques for hybrid systems is the geometrically computed intersection with guard sets. In this work, we replace the intersection operation by a nonlinear mapping onto the guard, which is not only numerically stable, but also scalable, making it possible to verify systems which were previously out of reach. The approach can be applied to the fairly common class of hybrid systems with piecewise continuous solutions, guard sets modeled as halfspaces, and urgent semantics, i.e. discrete transitions are immediately taken when enabled by guard sets. We demonstrate the usefulness of the new approach by a mechanical system with backlash which has 101 continuous state variables.