180
H. Sibai et al.
Example 4 (Fixed-wing aircraft infinite number of reachtubes resulting from transforming a single one). Consider the real system in Example 1 and the virtual one in Example 3.
Fix the initial set, which is represented as a hyper-rectangle, K r = [[1,
π
4 , 3, 1], [2,
π
3 , 4, 2]],
the real mode p r = [2.5, 0.5, 13.3, 5], and the time bound 20 seconds. Then, similar to Example 3, we fix θ = arctan 2 (2.5 − 13.3, 5 − 0.5) = −1.176 rad and goal = [13.3, 5]. We
call the resulting transformations from Example 3, γ p r and ρ p r . Let K v = γ p r (K r ) and p v =
ρ p r (p r ) = [0, 0, 0, 0]. Assume that we have the reachtube rtube r = ReachTb(K r , p r , T ).
Then, using Corollary 1, we can get rtube v = ReachTb(K v , p v , T ) by transforming rtube r
using γ p r . The benefit of the corollary appears in the following: for any p ∈ P = R 4 , we
can get the corresponding reachtube ReachTb(γ −1
p (K v ), p, T ) by transforming rtube v
using γ −1
p .
The projection of K v on its last two coordinates K v [2 : 3] represents the possible
initial position of the aircraft in the plane relative to the destination waypoint. It would
be a rotated square with angle θ . The distance from K v [2 : 3] center to the origin would
be equal to the distance from K[2 : 3] center to the destination waypoint. Moreover, the
angle between the y-axis and the line connecting the origin with the center of K v [2 : 3]
would be equal to the angle from the segment connecting the source and destination
waypoints to the line connecting the destination waypoint with the center of K[2 : 3]. On
the other hand, K v [0] = K[0] and K v [1] = K[1] + θ .
In summary, the absolute positions of the aircraft and waypoints do not matter. What
matters is their relative positions. The virtual system stores what matters and whenever a
reachtube is needed for a new absolute position, we can transform it from the virtual one.
5 Symmetry-based verification algorithm
In this section, we introduce a novel safety verification algorithm, symSafetyVerif,
which uses existing reachability subroutines, but exploits symmetry, unlike existing
algorithms. In our earlier work [29], we introduced reachtube transformations using
symmetry for single mode dynamical systems. Here, we extend the method across modes,
introduce the virtual system, and develop the corresponding verification algorithm.
In Section 5.1, we define tubecache—a data-structure for storing reachtubes; in 5.2,
we present the symmetry-based reachtube computation algorithm symComputeReachtube
that reuses reachtubes stored in tubecache; finally, in 5.3, we define the safetycache datastructure which stores previously computed safety verification results. These results
would be used by the symSafetyVerif algorithm.
5.1 tubecache: shared memory for reachtubes
We show how we use the virtual system (5) to create a shared memory for the different
modes of the real system (1) to reuse each others’ computed reachtubes. We call this
shared memory tubecache.
Definition 6. A tubecache is a data structure that stores a set of reachtubes of the virtual
system (5). It has two methods: getTube, for retrieving stored tubes and storeTube, for
storing a newly computed one.
H. Sibai et al.
Example 4 (Fixed-wing aircraft infinite number of reachtubes resulting from transforming a single one). Consider the real system in Example 1 and the virtual one in Example 3.
Fix the initial set, which is represented as a hyper-rectangle, K r = [[1,
π
4 , 3, 1], [2,
π
3 , 4, 2]],
the real mode p r = [2.5, 0.5, 13.3, 5], and the time bound 20 seconds. Then, similar to Example 3, we fix θ = arctan 2 (2.5 − 13.3, 5 − 0.5) = −1.176 rad and goal = [13.3, 5]. We
call the resulting transformations from Example 3, γ p r and ρ p r . Let K v = γ p r (K r ) and p v =
ρ p r (p r ) = [0, 0, 0, 0]. Assume that we have the reachtube rtube r = ReachTb(K r , p r , T ).
Then, using Corollary 1, we can get rtube v = ReachTb(K v , p v , T ) by transforming rtube r
using γ p r . The benefit of the corollary appears in the following: for any p ∈ P = R 4 , we
can get the corresponding reachtube ReachTb(γ −1
p (K v ), p, T ) by transforming rtube v
using γ −1
p .
The projection of K v on its last two coordinates K v [2 : 3] represents the possible
initial position of the aircraft in the plane relative to the destination waypoint. It would
be a rotated square with angle θ . The distance from K v [2 : 3] center to the origin would
be equal to the distance from K[2 : 3] center to the destination waypoint. Moreover, the
angle between the y-axis and the line connecting the origin with the center of K v [2 : 3]
would be equal to the angle from the segment connecting the source and destination
waypoints to the line connecting the destination waypoint with the center of K[2 : 3]. On
the other hand, K v [0] = K[0] and K v [1] = K[1] + θ .
In summary, the absolute positions of the aircraft and waypoints do not matter. What
matters is their relative positions. The virtual system stores what matters and whenever a
reachtube is needed for a new absolute position, we can transform it from the virtual one.
5 Symmetry-based verification algorithm
In this section, we introduce a novel safety verification algorithm, symSafetyVerif,
which uses existing reachability subroutines, but exploits symmetry, unlike existing
algorithms. In our earlier work [29], we introduced reachtube transformations using
symmetry for single mode dynamical systems. Here, we extend the method across modes,
introduce the virtual system, and develop the corresponding verification algorithm.
In Section 5.1, we define tubecache—a data-structure for storing reachtubes; in 5.2,
we present the symmetry-based reachtube computation algorithm symComputeReachtube
that reuses reachtubes stored in tubecache; finally, in 5.3, we define the safetycache datastructure which stores previously computed safety verification results. These results
would be used by the symSafetyVerif algorithm.
5.1 tubecache: shared memory for reachtubes
We show how we use the virtual system (5) to create a shared memory for the different
modes of the real system (1) to reuse each others’ computed reachtubes. We call this
shared memory tubecache.
Definition 6. A tubecache is a data structure that stores a set of reachtubes of the virtual
system (5). It has two methods: getTube, for retrieving stored tubes and storeTube, for
storing a newly computed one.