Lagrangian reachabililty

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

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

4 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 - 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 Dive into the research topics of 'Lagrangian reachabililty'. Together they form a unique fingerprint.

Cite this