Cyranka/Islam/Byrne/Jones/Smolka/Grosu.

Lagrangian Reachabililty.*

J. Cyranka, M.A. Islam, G. Byrne, P. Jones, S.A. Smolka, and R. Grosu.

We introduce LRT, a new Lagrangian-based Reach-Tube computation algorithm that conservatively approximates the set of reachable states of a nonlinear dynamical system. LRT makes use of the Cauchy-Green stretching factor (SF), which is derived from an overapproximation of the gradient of the solution-flows. The SF measures the discrepancy between two states propagated by the system solution from two initial states lying in a well-defined region, thereby allowing LRT to compute a reachtube with a ball-overestimate in a metric where the computed enclosure is as tight as possible. To evaluate its performance, we implemented a prototype of LRT in C++/Matlab, and ran it on a set of well-established benchmarks. Our results show that LRT compares very favorably with respect to the CAPD and Flow* tools.

In Proc. of CAV'17, the 29th International Conference on Computer-Aided Verification, Heidelberg, Germany, July, 2017, Springer, LNCS.

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