---
_id: '1421'
abstract:
- lang: eng
text: '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.'
author:
- first_name: Stanley
full_name: Bak, Stanley
last_name: Bak
- first_name: Sergiy
full_name: Bogomolov, Sergiy
id: 369D9A44-F248-11E8-B48F-1D18A9856A87
last_name: Bogomolov
orcid: 0000-0002-0686-0365
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Taylor
full_name: Johnson, Taylor
last_name: Johnson
- first_name: Pradyot
full_name: Prakash, Pradyot
last_name: Prakash
citation:
ama: 'Bak S, Bogomolov S, Henzinger TA, Johnson T, Prakash P. Scalable static hybridization
methods for analysis of nonlinear systems. In: Springer; 2016:155-164. doi:10.1145/2883817.2883837'
apa: 'Bak, S., Bogomolov, S., Henzinger, T. A., Johnson, T., & Prakash, P. (2016).
Scalable static hybridization methods for analysis of nonlinear systems (pp. 155–164).
Presented at the HSCC 2016: International Conference on Hybrid Systems: Computation
and Control, Vienna, Austria: Springer. https://doi.org/10.1145/2883817.2883837'
chicago: Bak, Stanley, Sergiy Bogomolov, Thomas A Henzinger, Taylor Johnson, and
Pradyot Prakash. “Scalable Static Hybridization Methods for Analysis of Nonlinear
Systems,” 155–64. Springer, 2016. https://doi.org/10.1145/2883817.2883837.
ieee: 'S. Bak, S. Bogomolov, T. A. Henzinger, T. Johnson, and P. Prakash, “Scalable
static hybridization methods for analysis of nonlinear systems,” presented at
the HSCC 2016: International Conference on Hybrid Systems: Computation and Control,
Vienna, Austria, 2016, pp. 155–164.'
ista: 'Bak S, Bogomolov S, Henzinger TA, Johnson T, Prakash P. 2016. Scalable static
hybridization methods for analysis of nonlinear systems. HSCC 2016: International
Conference on Hybrid Systems: Computation and Control, 155–164.'
mla: Bak, Stanley, et al. Scalable Static Hybridization Methods for Analysis
of Nonlinear Systems. Springer, 2016, pp. 155–64, doi:10.1145/2883817.2883837.
short: S. Bak, S. Bogomolov, T.A. Henzinger, T. Johnson, P. Prakash, in:, Springer,
2016, pp. 155–164.
conference:
end_date: 2016-04-14
location: Vienna, Austria
name: 'HSCC 2016: International Conference on Hybrid Systems: Computation and Control'
start_date: 2016-04-12
date_created: 2018-12-11T11:51:55Z
date_published: 2016-04-11T00:00:00Z
date_updated: 2021-01-12T06:50:37Z
day: '11'
department:
- _id: ToHe
doi: 10.1145/2883817.2883837
ec_funded: 1
language:
- iso: eng
month: '04'
oa_version: None
page: 155 - 164
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication_status: published
publisher: Springer
publist_id: '5786'
quality_controlled: '1'
scopus_import: 1
status: public
title: Scalable static hybridization methods for analysis of nonlinear systems
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
year: '2016'
...