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 - 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.
T2 - 57th IEEE Conference on Decision and Control, CDC 2018
Y2 - 17 December 2018 through 19 December 2018
ER -