Scalable Static Hybridization Methods for Analysis of Nonlinear Systems
Stanley Bak, Sergiy Bogomolov, Thomas A. Henzinger, Taylor Thomas Johnson, Pradyot Prakash · 2016
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 that are more scalable than earlier approaches.