Lagrangian reachabililty

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

3 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 languageEnglish
Title of host publicationComputer Aided Verification - 29th International Conference, CAV 2017, Proceedings
EditorsViktor Kuncak, Rupak Majumdar
PublisherSpringer-Verlag
Pages379-400
Number of pages22
ISBN (Print)9783319633862
DOIs
StatePublished - Jan 1 2017
Event29th International Conference on Computer Aided Verification, CAV 2017 - Heidelberg, Germany
Duration: Jul 24 2017Jul 28 2017

Publication series

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

Conference

Conference29th International Conference on Computer Aided Verification, CAV 2017
CountryGermany
CityHeidelberg
Period07/24/1707/28/17

    Fingerprint

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