Lagrangian reachabililty

Jacek Cyranka; Md Ariful Islam; Greg Byrne; Paul Jones; Scott A. Smolka; Radu Grosu

doi:10.1007/978-3-319-63387-9_19

Lagrangian reachabililty

Jacek Cyranka
, Md Ariful Islam
, Greg Byrne
, Paul Jones
, Scott A. Smolka
, Radu Grosu

Computer Science

Rutgers - The State University of New Jersey, New Brunswick
Carnegie Mellon University
Metron, Inc.
United States Food and Drug Administration
TU Wien

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

12 Scopus citations

Abstract

We introduce LRT, a new Lagrangian-based ReachTube computation algorithm that conservatively approximates the set of reachable states of a nonlinear dynamical system. LRT makes use of the Cauchy-Green stretching factor (SF), which is derived from an over-approximation of the gradient of the solution-flows. The SF measures the discrepancy between two states propagated by the system solution from two initial states lying in a well-defined region, thereby allowing LRT to compute a reachtube with a ball-overestimate in a metric where the computed enclosure is as tight as possible. To evaluate its performance, we implemented a prototype of LRT in C++/Matlab, and ran it on a set of well-established benchmarks. Our results show that LRT compares very favorably with respect to the CAPD and Flow* tools.

Original language	English
Title of host publication	Computer Aided Verification - 29th International Conference, CAV 2017, Proceedings
Editors	Viktor Kuncak, Rupak Majumdar
Publisher	Springer Verlag
Pages	379-400
Number of pages	22
ISBN (Print)	9783319633862
DOIs	https://doi.org/10.1007/978-3-319-63387-9_19
State	Published - 2017
Event	29th International Conference on Computer Aided Verification, CAV 2017 - Heidelberg, Germany Duration: Jul 24 2017 → Jul 28 2017

Publication series

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

Conference

Conference	29th International Conference on Computer Aided Verification, CAV 2017
Country/Territory	Germany
City	Heidelberg
Period	07/24/17 → 07/28/17

Access to Document

10.1007/978-3-319-63387-9_19

Cite this

Cyranka, J., Islam, M. A., Byrne, G., Jones, P., Smolka, S. A., & Grosu, R. (2017). Lagrangian reachabililty. In V. Kuncak, & R. Majumdar (Eds.), Computer Aided Verification - 29th International Conference, CAV 2017, Proceedings (pp. 379-400). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10426 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-319-63387-9_19

Cyranka, Jacek ; Islam, Md Ariful ; Byrne, Greg et al. / Lagrangian reachabililty. Computer Aided Verification - 29th International Conference, CAV 2017, Proceedings. editor / Viktor Kuncak ; Rupak Majumdar. Springer Verlag, 2017. pp. 379-400 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{d85d5739d3514028a29ce5b6d96699c9,

title = "Lagrangian reachabililty",

abstract = "We introduce LRT, a new Lagrangian-based ReachTube computation algorithm that conservatively approximates the set of reachable states of a nonlinear dynamical system. LRT makes use of the Cauchy-Green stretching factor (SF), which is derived from an over-approximation of the gradient of the solution-flows. The SF measures the discrepancy between two states propagated by the system solution from two initial states lying in a well-defined region, thereby allowing LRT to compute a reachtube with a ball-overestimate in a metric where the computed enclosure is as tight as possible. To evaluate its performance, we implemented a prototype of LRT in C++/Matlab, and ran it on a set of well-established benchmarks. Our results show that LRT compares very favorably with respect to the CAPD and Flow* tools.",

author = "Jacek Cyranka and Islam, \{Md Ariful\} and Greg Byrne and Paul Jones and Smolka, \{Scott A.\} and Radu Grosu",

note = "Publisher Copyright: {\textcopyright} Springer International Publishing AG 2017.; 29th International Conference on Computer Aided Verification, CAV 2017 ; Conference date: 24-07-2017 Through 28-07-2017",

year = "2017",

doi = "10.1007/978-3-319-63387-9\_19",

language = "English",

isbn = "9783319633862",

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

publisher = "Springer Verlag",

pages = "379--400",

editor = "Viktor Kuncak and Rupak Majumdar",

booktitle = "Computer Aided Verification - 29th International Conference, CAV 2017, Proceedings",

}

Cyranka, J, Islam, MA, Byrne, G, Jones, P, Smolka, SA & Grosu, R 2017, Lagrangian reachabililty. in V Kuncak & R Majumdar (eds), Computer Aided Verification - 29th International Conference, CAV 2017, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10426 LNCS, Springer Verlag, pp. 379-400, 29th International Conference on Computer Aided Verification, CAV 2017, Heidelberg, Germany, 07/24/17. https://doi.org/10.1007/978-3-319-63387-9_19

Lagrangian reachabililty. / Cyranka, Jacek; Islam, Md Ariful; Byrne, Greg et al.
Computer Aided Verification - 29th International Conference, CAV 2017, Proceedings. ed. / Viktor Kuncak; Rupak Majumdar. Springer Verlag, 2017. p. 379-400 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10426 LNCS).

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

TY - GEN

T1 - Lagrangian reachabililty

AU - Cyranka, Jacek

AU - Islam, Md Ariful

AU - Byrne, Greg

AU - Jones, Paul

AU - Smolka, Scott A.

AU - Grosu, Radu

PY - 2017

Y1 - 2017

N2 - We introduce LRT, a new Lagrangian-based ReachTube computation algorithm that conservatively approximates the set of reachable states of a nonlinear dynamical system. LRT makes use of the Cauchy-Green stretching factor (SF), which is derived from an over-approximation of the gradient of the solution-flows. The SF measures the discrepancy between two states propagated by the system solution from two initial states lying in a well-defined region, thereby allowing LRT to compute a reachtube with a ball-overestimate in a metric where the computed enclosure is as tight as possible. To evaluate its performance, we implemented a prototype of LRT in C++/Matlab, and ran it on a set of well-established benchmarks. Our results show that LRT compares very favorably with respect to the CAPD and Flow* tools.

AB - We introduce LRT, a new Lagrangian-based ReachTube computation algorithm that conservatively approximates the set of reachable states of a nonlinear dynamical system. LRT makes use of the Cauchy-Green stretching factor (SF), which is derived from an over-approximation of the gradient of the solution-flows. The SF measures the discrepancy between two states propagated by the system solution from two initial states lying in a well-defined region, thereby allowing LRT to compute a reachtube with a ball-overestimate in a metric where the computed enclosure is as tight as possible. To evaluate its performance, we implemented a prototype of LRT in C++/Matlab, and ran it on a set of well-established benchmarks. Our results show that LRT compares very favorably with respect to the CAPD and Flow* tools.

UR - https://www.scopus.com/pages/publications/85026771715

U2 - 10.1007/978-3-319-63387-9_19

DO - 10.1007/978-3-319-63387-9_19

M3 - Conference contribution

AN - SCOPUS:85026771715

SN - 9783319633862

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

SP - 379

EP - 400

BT - Computer Aided Verification - 29th International Conference, CAV 2017, Proceedings

A2 - Kuncak, Viktor

A2 - Majumdar, Rupak

PB - Springer Verlag

T2 - 29th International Conference on Computer Aided Verification, CAV 2017

Y2 - 24 July 2017 through 28 July 2017

ER -

Cyranka J, Islam MA, Byrne G, Jones P, Smolka SA, Grosu R. Lagrangian reachabililty. In Kuncak V, Majumdar R, editors, Computer Aided Verification - 29th International Conference, CAV 2017, Proceedings. Springer Verlag. 2017. p. 379-400. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-63387-9_19

Lagrangian reachabililty

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this