TY - GEN

T1 - Tight Continuous-Time Reachtubes for Lagrangian Reachability

AU - Cyranka, Jacek

AU - Islam, Md Ariful

AU - Smolka, Scott A.

AU - Gao, Sicun

AU - Grosu, Radu

N1 - Funding Information:
We thank the anonymous reviewers for their valuable comments. Research supported by: U.S. Air Force (AFRL) Contract No. FA9550-15-C-0030; NSF CPS-1446832; NSF IIS-1447549; NSF CNS-1445770; DARPA Assured Autonomy Program.
Publisher Copyright:
© 2018 IEEE.

PY - 2018/7/2

Y1 - 2018/7/2

N2 - 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.

AB - 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.

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

U2 - 10.1109/CDC.2018.8619647

DO - 10.1109/CDC.2018.8619647

M3 - Conference contribution

AN - SCOPUS:85062187168

T3 - Proceedings of the IEEE Conference on Decision and Control

SP - 6854

EP - 6861

BT - 2018 IEEE Conference on Decision and Control, CDC 2018

PB - Institute of Electrical and Electronics Engineers Inc.

Y2 - 17 December 2018 through 19 December 2018

ER -