Reachability Analysis of Nonlinear Systems Using Hybridization and Dynamics Scaling

Dongxu Li; Stanley Bak; Sergiy Bogomolov

doi:10.1007/978-3-030-57628-8_16

Reachability Analysis of Nonlinear Systems Using Hybridization and Dynamics Scaling

Dongxu Li, Stanley Bak, Sergiy Bogomolov^*

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

10 Citations (Scopus)

Abstract

Reachability analysis techniques aim to compute which states a dynamical system can enter. The analysis of systems described by nonlinear differential equations is known to be particularly challenging. Hybridization methods tackle this problem by abstracting nonlinear dynamics with piecewise linear dynamics around the reachable states, with additional inputs to ensure overapproximation. This reduces the analysis of a system with nonlinear dynamics to the one with piecewise affine dynamics, which have powerful analysis methods. In this paper, we present improvements to the hybridization approach based on a dynamics scaling model transformation. The transformation aims to reduce the sizes of the linearization domains, and therefore reduces overapproximation error. We showcase the efficiency of our approach on a number of nonlinear benchmark instances, and compare our approach with Flow*.

Original language	English
Title of host publication	Formal Modeling and Analysis of Timed Systems - 18th International Conference, FORMATS 2020, Proceedings
Editors	Nathalie Bertrand, Nils Jansen
Publisher	Springer
Pages	265-282
Number of pages	18
ISBN (Print)	9783030576271
DOIs	https://doi.org/10.1007/978-3-030-57628-8_16
Publication status	Published - 2020
Event	18th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2020 - Vienna, Austria Duration: 1 Sept 2020 → 3 Sept 2020

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	12288 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	18th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2020
Country/Territory	Austria
City	Vienna
Period	1/09/20 → 3/09/20

Access to Document

10.1007/978-3-030-57628-8_16

Cite this

Li, D., Bak, S., & Bogomolov, S. (2020). Reachability Analysis of Nonlinear Systems Using Hybridization and Dynamics Scaling. In N. Bertrand, & N. Jansen (Eds.), Formal Modeling and Analysis of Timed Systems - 18th International Conference, FORMATS 2020, Proceedings (pp. 265-282). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12288 LNCS). Springer. https://doi.org/10.1007/978-3-030-57628-8_16

Li, Dongxu ; Bak, Stanley ; Bogomolov, Sergiy. / Reachability Analysis of Nonlinear Systems Using Hybridization and Dynamics Scaling. Formal Modeling and Analysis of Timed Systems - 18th International Conference, FORMATS 2020, Proceedings. editor / Nathalie Bertrand ; Nils Jansen. Springer, 2020. pp. 265-282 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{4e8df6c51c254c70b55728b124834138,

title = "Reachability Analysis of Nonlinear Systems Using Hybridization and Dynamics Scaling",

abstract = "Reachability analysis techniques aim to compute which states a dynamical system can enter. The analysis of systems described by nonlinear differential equations is known to be particularly challenging. Hybridization methods tackle this problem by abstracting nonlinear dynamics with piecewise linear dynamics around the reachable states, with additional inputs to ensure overapproximation. This reduces the analysis of a system with nonlinear dynamics to the one with piecewise affine dynamics, which have powerful analysis methods. In this paper, we present improvements to the hybridization approach based on a dynamics scaling model transformation. The transformation aims to reduce the sizes of the linearization domains, and therefore reduces overapproximation error. We showcase the efficiency of our approach on a number of nonlinear benchmark instances, and compare our approach with Flow*.",

author = "Dongxu Li and Stanley Bak and Sergiy Bogomolov",

note = "Publisher Copyright: {\textcopyright} 2020, Springer Nature Switzerland AG.; 18th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2020 ; Conference date: 01-09-2020 Through 03-09-2020",

year = "2020",

doi = "10.1007/978-3-030-57628-8_16",

language = "English",

isbn = "9783030576271",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "265--282",

editor = "Nathalie Bertrand and Nils Jansen",

booktitle = "Formal Modeling and Analysis of Timed Systems - 18th International Conference, FORMATS 2020, Proceedings",

address = "Germany",

}

Li, D, Bak, S & Bogomolov, S 2020, Reachability Analysis of Nonlinear Systems Using Hybridization and Dynamics Scaling. in N Bertrand & N Jansen (eds), Formal Modeling and Analysis of Timed Systems - 18th International Conference, FORMATS 2020, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12288 LNCS, Springer, pp. 265-282, 18th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2020, Vienna, Austria, 1/09/20. https://doi.org/10.1007/978-3-030-57628-8_16

Reachability Analysis of Nonlinear Systems Using Hybridization and Dynamics Scaling. / Li, Dongxu; Bak, Stanley; Bogomolov, Sergiy.
Formal Modeling and Analysis of Timed Systems - 18th International Conference, FORMATS 2020, Proceedings. ed. / Nathalie Bertrand; Nils Jansen. Springer, 2020. p. 265-282 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12288 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Reachability Analysis of Nonlinear Systems Using Hybridization and Dynamics Scaling

AU - Li, Dongxu

AU - Bak, Stanley

AU - Bogomolov, Sergiy

PY - 2020

Y1 - 2020

N2 - Reachability analysis techniques aim to compute which states a dynamical system can enter. The analysis of systems described by nonlinear differential equations is known to be particularly challenging. Hybridization methods tackle this problem by abstracting nonlinear dynamics with piecewise linear dynamics around the reachable states, with additional inputs to ensure overapproximation. This reduces the analysis of a system with nonlinear dynamics to the one with piecewise affine dynamics, which have powerful analysis methods. In this paper, we present improvements to the hybridization approach based on a dynamics scaling model transformation. The transformation aims to reduce the sizes of the linearization domains, and therefore reduces overapproximation error. We showcase the efficiency of our approach on a number of nonlinear benchmark instances, and compare our approach with Flow*.

AB - Reachability analysis techniques aim to compute which states a dynamical system can enter. The analysis of systems described by nonlinear differential equations is known to be particularly challenging. Hybridization methods tackle this problem by abstracting nonlinear dynamics with piecewise linear dynamics around the reachable states, with additional inputs to ensure overapproximation. This reduces the analysis of a system with nonlinear dynamics to the one with piecewise affine dynamics, which have powerful analysis methods. In this paper, we present improvements to the hybridization approach based on a dynamics scaling model transformation. The transformation aims to reduce the sizes of the linearization domains, and therefore reduces overapproximation error. We showcase the efficiency of our approach on a number of nonlinear benchmark instances, and compare our approach with Flow*.

UR - http://www.scopus.com/inward/record.url?scp=85090170700&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-57628-8_16

DO - 10.1007/978-3-030-57628-8_16

M3 - Conference contribution

SN - 9783030576271

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 265

EP - 282

BT - Formal Modeling and Analysis of Timed Systems - 18th International Conference, FORMATS 2020, Proceedings

A2 - Bertrand, Nathalie

A2 - Jansen, Nils

PB - Springer

T2 - 18th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2020

Y2 - 1 September 2020 through 3 September 2020

ER -

Li D, Bak S, Bogomolov S. Reachability Analysis of Nonlinear Systems Using Hybridization and Dynamics Scaling. In Bertrand N, Jansen N, editors, Formal Modeling and Analysis of Timed Systems - 18th International Conference, FORMATS 2020, Proceedings. Springer. 2020. p. 265-282. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-57628-8_16

Reachability Analysis of Nonlinear Systems Using Hybridization and Dynamics Scaling

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this