Supplementary Material: Scalable Static Hybridization Methods for Analysis of Nonlinear Systems

Stanley Bak, Sergiy Bogomolov, Thomas Henzinger, Taylor T. Johnson, and Pradyot Prakash

Abstract: Hybridization methods enable the analysis of hybrid automata with complex, nonlinear dynamics through a sound abstraction process. Complex dynamics are converted to simpler ones with added noise, and then analysis is done using a reachability method for the simpler dynamics. Several such recent approaches advocate that only dynamic hybridization techniques---i.e., those where the dynamics are abstracted on-the-fly during a reachability computation---are effective. In this paper, we demonstrate this is not the case, and create static hybridization methods which are more scalable than earlier approaches. The main insight in our approach is that quick, numeric simulations can be used to guide the process, eliminating the need for an exponential number of hybridization domains. Transitions between domains are generally time-triggered, avoiding accumulated error from geometric intersections. We enhance our static technique by combining time-triggered transitions with occasional space-triggered transitions, and demonstrate the benefits of the combined approach in what we call mixed-triggered hybridization. Finally, error modes are inserted to confirm that the reachable states stay within the hybridized regions. The developed techniques can scale to higher dimensions than previous static approaches, while enabling the parallelization of the main performance bottleneck for many dynamic hybridization approaches: the nonlinear optimization required for sound dynamics abstraction. We implement our method as a model transformation pass in the HYST tool, and perform reachability analysis and evaluation using an unmodified version of SpaceEx on nonlinear models with up to six dimensions.

Paper submission (PDF)
The supplementary materials, including all examples are available here. The latest release of HYST contains the hybridization method implemented as a transformation pass, and the archive above has everything necessary to reproduce all results. We are currently refactoring the prototype implementation into a transformation pass in Hyst.