Tight Continuous time Reachtubes for Lagrangian Reachability
Tight Continuous-Time Reachtubes for Lagrangian Reachability
Jacek Cyranka
1
, Md. Ariful Islam
2
, Scott A. Smolka
3
, Sicun Gao
1
, Radu Grosu
4
Abstract— 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 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.
I. I NTRODUCTION
Recent work introduced Lagrangian ReachTube algorithm
(LRT), a new approach for the reachability analysis of con-
tinuous, nonlinear, dynamical systems [4]. LRT constructs a
discrete reachtube (or flowpipe) that tightly overestimates at
each discrete time point the set of states reached at that time
point by a dynamical system.
The main idea of LRT was to construct a ball-overestimate
in a metric space that minimizes the Cauchy-Green stretching
factor at every discrete time instant. LRT was shown to
compare favorably to other reachability analysis tools, such
as CAPD [1], [17], [18] and Flow* [2], [3] in terms of the
discrete reachtube volumes they compute on a set of well-
known benchmarks.
This paper proposes a continuous-time-reachtube exten-
sion of LRT, the motivation for which is two-fold. First, LRT,
while being optimal in the discrete setting, is not sound in
the continuous setting: it is not obvious how to find a ball
tightly overestimating the dynamics between two discrete
points. Second, LRT is not directly applicable to the analysis
of hybrid systems, as the dynamics of a hybrid system may
change dramatically between two discrete time points due to
a mode switch.
The main goal of our algorithm, which we call continuous
Lagrangian ReachTube algorithm (CLRT), is to efficiently
construct an ellipsoidal continuous-reachtube overestimate
that is tighter than those constructed by available state-of-
the-art tools such as CAPD. CLRT combines a number of
techniques to achieve its goal, including infinitesimal strain
theory, analytic formulas for the tightest deformation metric,
Jacek Cyranka and Md. Ariful Islam contributted equally to this work.
1
University of California, San Diego, 9500 Gilman Dr, La Jolla, CA 92093,
2
Carnegie Mellon University,
3
Stony Brook University,
4
Vienna University
of Technology
nonconvex optimization, and δ -satisfiability. Computing an
as tight-as-possible continuous-reachtube overestimate helps
avoid false positives when checking if a set of unsafe states
can be reached from a set of initial states.
The class of continuous dynamical systems in which
we are interested is described by nonlinear, time-variant,
ordinary differential equations (ODEs):
x
0
(t) = f (t, x(t)), (1a)
x(t
0
) = x
0
, (1b)
where x : R → R
n
. We assume f is a smooth function, which
guarantees short-term existence of solutions. The class of
time-variant systems includes the class of time-invariant sys-
tems. Time-variant equations may contain additional terms,
e.g., excitation variables and periodic forcing terms.
Given an initial time t
0
, set of initial states X ⊂ R
n
, and
time bound T > t
0
, CLRT computes a conservative reachtube
of (1), that is, a sequence of time-stamped sets of states
(R
1
, t
1
), . . ., (R
k
, t
k
= T ) satisfying:
Reach ((t
0
, X ) , [t
i−1
, t
i
]) ⊂ R
i
for i = 1, . . . , k,
where Reach ((t
0
, X ) , [t
i−1
, t
i
]) denotes the set of all reach-
able states of ODE system (1) in the time interval [t
i−1
, t
i
].
The time steps are not necessarily uniformly spaced, and are
chosen using infinitesimal strain theory (IST).
In contrast to LRT [4], which only computes the set
of states reachable at discrete and uniformly spaced time
steps t
i
, for i ∈{1 , . . ., k } , CLRT computes a conserva-
tive overestimate for the set of states reachable in non-
uniformly spaced continuous time intervals [t
i−1
, t
i
]. Hence,
CLRT computes space-time cylinders overestimating the
continuous-time reachtube.
We also note that the LRT approach, as in prior work
on reachability [8], [13], employed semi-definite program-
ming to compute a tight deformation metric minimizing the
Cauchy-Green stretching factor. We show that this approach
is inferior and should be avoided, as it increases the total
running time of the algorithm significantly, and can result
in numerical instabilities (refer to the discussion in [4]). We
instead derive a very simple analytic formula for the tightest
deformation metric. Thus, there is no need to invoke an
optimization procedure to find a tight deformation metric,
as the formula for the tightest one is now available. Also,
we provide a very concise proof of this fact.
Let Reach ((t
0
, X ) , t
i−1
) ⊂ B
M
i−1
(x
i−1
, δ
i−1
), where
B
M
i−1
(x
i−1
, δ
i−1
) is the ball computed by LRT for time
t
i−1
. To construct a conservative continuous reachtube
overestimate for the interval [t
i−1
, t
i
], we bloat the
CONFIDENTIAL. Limited circulation. For review only.
Preprint submitted to 57th IEEE Conference on Decision and Control.
Received March 20, 2018.
Source: https://docslib.org/doc/7190578/tight-continuous-time-reachtubes-for-lagrangian-reachability
0 Response to "Tight Continuous time Reachtubes for Lagrangian Reachability"
Postar um comentário