Cyranka/Islam/Smolka/Gao/Grosu.

Tight Continuous-Time Reachtubes for Lagrangian Reachability.*

J. Cyranka, M.A. Islam, S.A. Smolka, S. Gao, and R. Grosu.

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.