Tight Continuous-Time Reachtubes for Lagrangian Reachability

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