176
H. Sibai et al.
2.2 Reachtubes
Computing reachsets exactly is theoretically hard [22]. There are many reachability analysis tools [8,1,3] that can compute bounded-time over-approximations of the reachsets.
Generally, given an initial set K for a set of ODEs, these tools can return a sequence of
sets that contain the exact reachset over small time intervals. Motived by this, we define
reachtubes as sequences of time-annotated over-approximations of exact reachsets:
Definition 3. For a given agent A = S, P, f , an initial set K ⊆ T , a mode p ∈ P, and
a time interval [ftime, etime], a (K, p, [ftime, etime])-reachtube ReachTb(K, p, [0, T ]) is
a sequence {(X i , [τ i−1 , τ i ])}
j
i=1 such that Reach(K, p, [τ i−1 , τ i ]) ⊆ X i , and τ 0 = ftime <
τ 1 < ··· < τ j = etime. Without loss of generality, we assume equal separation between
the time points, i.e. ∃ τ s > 0, ∀i ∈ [ j], τ i − τ i−1 = τ s .
For a given (K, p, [ftime, etime])-reachtube rtube, we denote its parameters by rtube.K,
rtube.p, rtube.ftime, and rtube.etime, respectively, and its cardinality by rtube.len.
We define union, truncation, concatenate, and time-shift operators on reachtubes. Fix
rtube 1 = {(X i,1 , [τ i−1,1 , τ i,1 ])}
j 1
i=1 and rtube 2 = {(X i,2 , [τ i−1,2 , τ i,2 ])}
j 2
i=1 to be two reachtubes, where j 1 = rtube 1 .len and j 2 = rtube 2 .len. If τ i,1 = τ i,2 for all i ∈ [min( j 1 , j 2 )], we
say they are time-aligned. Without loss of generality, assume that j 1 ≤ j 2 . The operators
are defined as follows:
– timeShift(rtube 1 ,t s ) = {(X i,1 , [t s + τ i−1,1 ,t s + τ i,1 ])}
j 1
i=1 ,
– union: rtube 1 ∪ rtube 2 = {(X i,1 ∪ X i,2 , [τ i−1,1 , τ i,1 ])}
j 1
i=1 ∪ {(X i,2 , [τ i−1,2 , τ i,2 ])}
j 2
i= j 1 +1 ,
– concatenation: rtube 1
rtube 2 = rtube 1 ∪ {(X i,2 , [τ j 1 ,1 + τ i−1,2 , τ j 1 ,1 + τ i,2 ))}
j 2
i=1 ,
– truncate(rtube 1 ,t c ) = {(X i,1 , [τ i−1,1 , τ i,1 ])} k
i=1 , where τ k,1 ≥ t c and τ k−1,1 < t c .
A simulation of system (1) is a reachtube with X 0 being a singleton state x 0 ∈ K. That
is, a simulation is a representation of ξ (x 0 , p, ·). Several numerical solvers can compute
such simulations as VNODE-LP 1 and CAPD Dyn-Sys library 2 .
Example 1 (Fixed-wing aircraft following a single waypoint). Consider an agent with
state space S = R 4 , parameter space P = R 4 , and f : S × P → S defined as follows: for
any x ∈ S and p ∈ P,
f (x, p) = [
T c − c d1 x[0] 2
m
,
g
x[0]
sin φ , x[0] cos x[1], x[0] sin x[1]],
where T c = k 1 m(v c − x[0]), φ = k 2
v c
g (ψ c − x[1]), ψ c = arctan 2 (
x[2]−p[2]
x[3]−p[3] ), and k 1 , k 2 , m, g,
c d1 , and v c are positive constants. The agent models a fixed-wing aircraft starting from
a waypoint and following another in the 2D plane: x[0] is its speed, x[1] is its heading
angle, (x[2], x[3]) is its position in the plane, [p[0], p[1]] is the position of the source
waypoint, and (p[2], p[3]) is the position of the destination one. Note that the source
waypoint does not affect the dynamics, but will be useful later in the paper.
1 http://www.cas.mcmaster.ca/~nedialk/vnodelp/
2 http://capd.sourceforge.net/capdDynSys/docs/html/odes_rigorous.html
H. Sibai et al.
2.2 Reachtubes
Computing reachsets exactly is theoretically hard [22]. There are many reachability analysis tools [8,1,3] that can compute bounded-time over-approximations of the reachsets.
Generally, given an initial set K for a set of ODEs, these tools can return a sequence of
sets that contain the exact reachset over small time intervals. Motived by this, we define
reachtubes as sequences of time-annotated over-approximations of exact reachsets:
Definition 3. For a given agent A = S, P, f , an initial set K ⊆ T , a mode p ∈ P, and
a time interval [ftime, etime], a (K, p, [ftime, etime])-reachtube ReachTb(K, p, [0, T ]) is
a sequence {(X i , [τ i−1 , τ i ])}
j
i=1 such that Reach(K, p, [τ i−1 , τ i ]) ⊆ X i , and τ 0 = ftime <
τ 1 < ··· < τ j = etime. Without loss of generality, we assume equal separation between
the time points, i.e. ∃ τ s > 0, ∀i ∈ [ j], τ i − τ i−1 = τ s .
For a given (K, p, [ftime, etime])-reachtube rtube, we denote its parameters by rtube.K,
rtube.p, rtube.ftime, and rtube.etime, respectively, and its cardinality by rtube.len.
We define union, truncation, concatenate, and time-shift operators on reachtubes. Fix
rtube 1 = {(X i,1 , [τ i−1,1 , τ i,1 ])}
j 1
i=1 and rtube 2 = {(X i,2 , [τ i−1,2 , τ i,2 ])}
j 2
i=1 to be two reachtubes, where j 1 = rtube 1 .len and j 2 = rtube 2 .len. If τ i,1 = τ i,2 for all i ∈ [min( j 1 , j 2 )], we
say they are time-aligned. Without loss of generality, assume that j 1 ≤ j 2 . The operators
are defined as follows:
– timeShift(rtube 1 ,t s ) = {(X i,1 , [t s + τ i−1,1 ,t s + τ i,1 ])}
j 1
i=1 ,
– union: rtube 1 ∪ rtube 2 = {(X i,1 ∪ X i,2 , [τ i−1,1 , τ i,1 ])}
j 1
i=1 ∪ {(X i,2 , [τ i−1,2 , τ i,2 ])}
j 2
i= j 1 +1 ,
– concatenation: rtube 1
rtube 2 = rtube 1 ∪ {(X i,2 , [τ j 1 ,1 + τ i−1,2 , τ j 1 ,1 + τ i,2 ))}
j 2
i=1 ,
– truncate(rtube 1 ,t c ) = {(X i,1 , [τ i−1,1 , τ i,1 ])} k
i=1 , where τ k,1 ≥ t c and τ k−1,1 < t c .
A simulation of system (1) is a reachtube with X 0 being a singleton state x 0 ∈ K. That
is, a simulation is a representation of ξ (x 0 , p, ·). Several numerical solvers can compute
such simulations as VNODE-LP 1 and CAPD Dyn-Sys library 2 .
Example 1 (Fixed-wing aircraft following a single waypoint). Consider an agent with
state space S = R 4 , parameter space P = R 4 , and f : S × P → S defined as follows: for
any x ∈ S and p ∈ P,
f (x, p) = [
T c − c d1 x[0] 2
m
,
g
x[0]
sin φ , x[0] cos x[1], x[0] sin x[1]],
where T c = k 1 m(v c − x[0]), φ = k 2
v c
g (ψ c − x[1]), ψ c = arctan 2 (
x[2]−p[2]
x[3]−p[3] ), and k 1 , k 2 , m, g,
c d1 , and v c are positive constants. The agent models a fixed-wing aircraft starting from
a waypoint and following another in the 2D plane: x[0] is its speed, x[1] is its heading
angle, (x[2], x[3]) is its position in the plane, [p[0], p[1]] is the position of the source
waypoint, and (p[2], p[3]) is the position of the destination one. Note that the source
waypoint does not affect the dynamics, but will be useful later in the paper.
1 http://www.cas.mcmaster.ca/~nedialk/vnodelp/
2 http://capd.sourceforge.net/capdDynSys/docs/html/odes_rigorous.html