We introduce continuous Lagrangian reachability (CLRT), a new algorithm for the computation of a tight, conservative 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 ti to time ti+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 hi between ti and ti+1, nonlinear optimization to minimally bloat (i.e., using a minimal radius) the state set at time ti such that it includes all the states of the solution flow in the interval [ti; ti+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.
In Proc. of CDC'18, the 57th IEEE Conference on Decision and Control, Miami Beach, FL, USA, December, 2018, IEEE.
*This work was partially supported by the NSF-Frontiers Cyber-Cardia
Award, the US-AFOSR Arrive Award, the EU-Artemis EMC2 Award, the
EU-Ecsel Semi40 Award, the EU-Ecsel Productive 4.0 Award, the
AT-FWF-NFN RiSE Award, the AT-FWF-LogicCS-DC Award, the AT-FFG
Harmonia Award, the AT-FFG Em2Apps Award, and the TUW-CPPS-DK Award.