Tight Continuous-Time Reachtubes for Lagrangian Reachability

Jacek Cyranka, Md Ariful Islam, Scott A. Smolka, Sicun Gao, Radu Grosu

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

4 Scopus citations


We introduce continuous Lagrangian reachability (CLRT), a new algorithm for the computation of a tight and continuous-time reachtube for the solution flows of a nonlinear, time-variant dynamical system. CLRT employs finite strain theory to determine the deformation of the solution set from time t- i to time t- i+1. We have developed simple explicit analytic formulas for the optimal metric for this deformation; this is superior to prior work, which used semi-definite programming. CLRT also uses infinitesimal strain theory to derive an optimal time increment h- i between t- i and t- i+1, nonlinear optimization to minimally bloat (i.e., using a minimal radius) the state set at time t- i such that it includes all the states of the solution flow in the interval [t- i, t- i+1]. We use delta -satisfiability to ensure the correctness of the bloating. Our results on a series of benchmarks show that CLRT performs favorably compared to state-of-the-art tools such as CAPD in terms of the continuous reachtube volumes they compute.

Original languageEnglish
Title of host publication2018 IEEE Conference on Decision and Control, CDC 2018
PublisherInstitute of Electrical and Electronics Engineers Inc.
Number of pages8
ISBN (Electronic)9781538613955
StatePublished - Jul 2 2018
Event57th IEEE Conference on Decision and Control, CDC 2018 - Miami, United States
Duration: Dec 17 2018Dec 19 2018

Publication series

NameProceedings of the IEEE Conference on Decision and Control
ISSN (Print)0743-1546
ISSN (Electronic)2576-2370


Conference57th IEEE Conference on Decision and Control, CDC 2018
Country/TerritoryUnited States


Dive into the research topics of 'Tight Continuous-Time Reachtubes for Lagrangian Reachability'. Together they form a unique fingerprint.

Cite this