Scalable static hybridization methods for analysis of nonlinear systems Conference Paper

Author(s): Bak, Stanley; Bogomolov, Sergiy V; Henzinger, Thomas A; Johnson, Taylor T; Prakash, Pradyot
Title: Scalable static hybridization methods for analysis of nonlinear systems
Affiliation IST Austria
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 techniquesi.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. 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 timetriggered, 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.
Keywords: Dynamics; Hybrid systems; Abstracting; Nonlinear systems; Reachability analysis; Mathematical transformations; Nonlinear programming; Abstraction process; Exponential numbers; Hybridization methods; Model transformation; Non-linear optimization; Performance bottlenecks; Triggered transitions
Conference Title: HSCC: Hybrid Systems - Computation and Control
Conference Dates: April 12 - 14, 2016
Conference Location: Vienna, Austria
Publisher: Springer  
Date Published: 2016-04-11
Start Page: 155
End Page: 164
DOI: 10.1145/2883817.2883837
Notes: The material presented in this paper is based upon work supported by the Air Force Office of Scientific Research (AFOSR), in part under contract number FA9550-15-1-0258 and the Summer Faculty Fellowship Program (SFFP), by AFRL through contract number FA8750-15-1-0105, and by the National Science Foundation (NSF) under grant num- bers CNS 1464311 and CCF 1527398. Furthermore, this research was supported in part by the European Research Council (ERC) under grant 267989 (QUAREM) and by the Austrian Science Fund (FWF) under grant numbers S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award). Any opinions, findings, and conclusions or recommenda- tions expressed in this publication are those of the authors and do not necessarily reflect the views of AFRL, AFOSR, or NSF.
Open access: no
IST Austria Authors
  1. Thomas A. Henzinger
    415 Henzinger
Related IST Austria Work