[Back]

S. Grünbacher, J. Cyranka, M. Lechner, A. Islam, S. Smolka, R. Grosu:
"Lagrangian Reachtubes: The Next Generation";
ArXiv, . (2020).

We introduce LRT-NG, a set of techniques and
an associated toolset that computes a reachtube (an overapproximation
of the set of reachable states over a given time
horizon) of a nonlinear dynamical system. LRT-NG significantly
advances the state-of-the-art Langrangian Reachability and its
associated tool LRT. From a theoretical perspective, LRT-NG
is superior to LRT in three ways. First, it uses for the first
time an analytically computed metric for the propagated ball
which is proven to minimize the ball´s volume. We emphasize
that the metric computation is the centerpiece of all bloatingbased
techniques. Secondly, it computes the next reachset as the
intersection of two balls: one based on the Cartesian metric
and the other on the new metric. While the two metrics
were previously considered opposing approaches, their joint
use considerably tightens the reachtubes. Thirdly, it avoids
the "wrapping effect" associated with the validated integration
of the center of the reachset, by optimally absorbing the
interval approximation in the radius of the next ball. From
a tool-development perspective, LRT-NG is superior to LRT
in two ways. First, it is a standalone tool that no longer
relies on CAPD. This required the implementation of the
Lohner method and a Runge-Kutta time-propagation method.
Secondly, it has an improved interface, allowing the input
model and initial conditions to be provided as external input
files. Our experiments on a comprehensive set of benchmarks,
including two Neural ODEs, demonstrates LRT-NG´s superior
performance compared to LRT, CAPD, and Flow*.

https://publik.tuwien.ac.at/files/publik_293052.pdf