178
H. Sibai et al.
Then, it would rotate the third and four axes counter-clockwise by θ . Moreover, ρ would
set the first two coordinates of the parameters to zero as they do not affect the dynamics,
translate the origin of the parameter space P to [0, 0, goal[0], goal[1]], and rotate the third
and fourth axes counter-clockwise by θ . For the aircraft, this means translating and
rotating the plane where the aircraft and the waypoint positions reside.
3.2 Symmetry and reachtubes
Computing reachtubes is computationally expensive as it requires non-trivial optimization problems and integrating non-linear functions [13,15,16,8,6]. Compared with that,
transforming reachtubes is much cheaper, especially if the transformation is linear.
In our previous work [29], we showed how to get reachtubes of autonomous systems
from previously computed ones using symmetry transformations. In this paper, we show
how to do that for systems with parameters. This allows different modes of a hybrid
system and different agents with similar dynamics to share reachtube computations. That
was not possible when the theory was limited to non-parameterized systems.
Theorem 2. Let (1) be Γ -equivariant. Then for any γ ∈ Γ and its corresponding ρ, any
K, p, [ftime, etime] and {(X i , [τ i−1 , τ i ])}
j
i=1 as a (K, p, [ftime, etime])-reachtube,
∀i ∈ [ j], Reach(γ(K), ρ(p), [τ i−1 , τ i ]) = γ(Reach(K, p, [τ i−1 , τ i ])) ⊆ γ(X i ).
Proof. (Sketch) The first part Reach(γ(K), ρ(p), [τ i−1 , τ i ]) = γ(Reach(K, p, [τ i−1 , τ i ]))
follows directly from Theorem 1. The second part γ(Reach(K, p, [τ i−1 , τ i ])) ⊆ γ(X i )
follows from the reachtube ReachTb(K, p, [t b ,t e ]) being an over-approximation of the
exact reachset during the small time intervals [τ i−1 , τ i ].
Theorem 2 says that we can transform a computed reachtube ReachTb(K, p, [t 1 ,t 2 ]) =
{(X i , [τ i−1 , τ i ])}
j
i=1 to get another reachtube {(γ(X i ), [τ i−1 , τ i ])}
j
i=1 , which is an overapproximation of the reachsets starting from γ(K).
The results of this section subsume the results about transforming reachtubes of
autonomous systems-dynamical systems without parameters as presented in [29].
4 Virtual system
The challenge in safety verification of multi-agent systems is that the dimensionality
of the problem grows rapidly with the number of agents. However, often agents share
the same dynamics. For instance, several fixed-wing aircrafts of the type described in
Example 1 share the same dynamics but may have different initial conditions and follow
different waypoints. This commonality has been exploited in developing specialized
proof techniques [23]. For reachability analysis, using symmetry transforms of the
previous section, reachtubes of one agent in one mode can be used to get the reachtubes
of other modes and even other agents.
Fix a particular value p v ∈ P and call it the virtual parameter. Assume that for all
p ∈ P, there exists a pair of transformations (γ p , ρ p ) such that ρ p (p) = p v , γ p is invertible,
H. Sibai et al.
Then, it would rotate the third and four axes counter-clockwise by θ . Moreover, ρ would
set the first two coordinates of the parameters to zero as they do not affect the dynamics,
translate the origin of the parameter space P to [0, 0, goal[0], goal[1]], and rotate the third
and fourth axes counter-clockwise by θ . For the aircraft, this means translating and
rotating the plane where the aircraft and the waypoint positions reside.
3.2 Symmetry and reachtubes
Computing reachtubes is computationally expensive as it requires non-trivial optimization problems and integrating non-linear functions [13,15,16,8,6]. Compared with that,
transforming reachtubes is much cheaper, especially if the transformation is linear.
In our previous work [29], we showed how to get reachtubes of autonomous systems
from previously computed ones using symmetry transformations. In this paper, we show
how to do that for systems with parameters. This allows different modes of a hybrid
system and different agents with similar dynamics to share reachtube computations. That
was not possible when the theory was limited to non-parameterized systems.
Theorem 2. Let (1) be Γ -equivariant. Then for any γ ∈ Γ and its corresponding ρ, any
K, p, [ftime, etime] and {(X i , [τ i−1 , τ i ])}
j
i=1 as a (K, p, [ftime, etime])-reachtube,
∀i ∈ [ j], Reach(γ(K), ρ(p), [τ i−1 , τ i ]) = γ(Reach(K, p, [τ i−1 , τ i ])) ⊆ γ(X i ).
Proof. (Sketch) The first part Reach(γ(K), ρ(p), [τ i−1 , τ i ]) = γ(Reach(K, p, [τ i−1 , τ i ]))
follows directly from Theorem 1. The second part γ(Reach(K, p, [τ i−1 , τ i ])) ⊆ γ(X i )
follows from the reachtube ReachTb(K, p, [t b ,t e ]) being an over-approximation of the
exact reachset during the small time intervals [τ i−1 , τ i ].
Theorem 2 says that we can transform a computed reachtube ReachTb(K, p, [t 1 ,t 2 ]) =
{(X i , [τ i−1 , τ i ])}
j
i=1 to get another reachtube {(γ(X i ), [τ i−1 , τ i ])}
j
i=1 , which is an overapproximation of the reachsets starting from γ(K).
The results of this section subsume the results about transforming reachtubes of
autonomous systems-dynamical systems without parameters as presented in [29].
4 Virtual system
The challenge in safety verification of multi-agent systems is that the dimensionality
of the problem grows rapidly with the number of agents. However, often agents share
the same dynamics. For instance, several fixed-wing aircrafts of the type described in
Example 1 share the same dynamics but may have different initial conditions and follow
different waypoints. This commonality has been exploited in developing specialized
proof techniques [23]. For reachability analysis, using symmetry transforms of the
previous section, reachtubes of one agent in one mode can be used to get the reachtubes
of other modes and even other agents.
Fix a particular value p v ∈ P and call it the virtual parameter. Assume that for all
p ∈ P, there exists a pair of transformations (γ p , ρ p ) such that ρ p (p) = p v , γ p is invertible,