206
30 juin 2016 - 14h00
Scalable Static Hybridization Methods for Analysis of Nonlinear Systems
par Sergiy Bogomolov de 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 techniques—i.e., those where the dynamics are abstracted
on-the-fly during a reachability computation— are effective. In this
talk, 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 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.
Sergiy Bogomolov is a Postdoctoral Researcher in the Institute of
Science and Technology Austria. He is starting as a Lecturer
(Assistant Professor) at the Australian National University in Fall
2016. Sergiy is interested in verification and synthesis techniques
for cyber-physical systems and their applications in artificial
intelligence and systems biology. His Ph.D. and M.Sc. degrees are from
the University of Freiburg, Germany.
