Multi-Agent Safety Verification using Symmetry Transformations
179
and γ p ( f (x, p)) = f (γ p (x), ρ p (p v )) = f (γ p (x), p v ). Consider the resulting ODE:
dξ
dt
(y, p v ,t) = f (ξ (y, p v ,t), p v ).
(5)
Following [27], we call (5) a virtual system. Correspondingly, we call (1), the real system
for the rest of the paper. The virtual system unifies the behavior of all modes of the real
system in one representative mode, the virtual one p v .
Example 3 (Fixed-wing aircraft virtual system). Consider the fixed-wing aircraft agent
described in Example 1 and the corresponding transformations described in Example 2.
Fix p ∈ P, we set goal in the transformation of Example 2 to [p[2], p[3]] and θ to
arctan 2 (p[0] − p[2], p[3] − p[1]) and let γ p and ρ p be the resulting transformations. Then,
for all p ∈ P, ρ p (p) = [0, 0, 0, 0]. Hence, p v = [0, 0, 0, 0] and the virtual system is that of
Example 1 with the parameter p = p v . For the aircraft, γ p would translate the origin of
the plane to the destination waypoint and rotate its axes so that the y-axis is aligned with
the segment between the source and destination waypoints. Hence, in the constructed
virtual system, the destination waypoint is the origin of the plane. The source waypoint
is the origin as well as it does not affect the dynamics.
The solutions of the virtual system can be transformed to get solutions of all other
modes in P using {γ −1
p } p∈P . This is shown in the following theorem.
Theorem 3. Given any initial state y 0 ∈ S, and any mode p ∈ P, γ −1
p (ξ (y 0 , p v , ·)) is a
solution of the real system (1) with mode p starting from γ −1
p (y 0 ). Similarly, given any
x 0 ∈ S, γ p (ξ (x 0 , p, ·)) is the solution of the virtual system (5) starting from γ p (x 0 ).
Proof. Lets start with the first part of the theorem. Fix p ∈ P and let x 0 = γ −1
p (y 0 ).
Using Theorem 1, γ p (ξ (x 0 , p, ·)) = ξ (γ p (x 0 ), ρ p (p), ·)) and is the solution of the real
system (1). Furthermore, ρ p (p) = p v , by definition, and γ p (x 0 ) = γ p (γ −1
p (y 0 )) = y 0 .
Hence, γ p (ξ (x 0 , p, ·)) = ξ (y 0 , p v , ·). Applying γ −1
p on both sides implies the first part of
the theorem. The second part is a direct application of Theorem 1.
The following corollary extends the result of Theorem 3 to reachtubes. It follows
from Theorem 2.
Corollary 1. Given a K v ⊆ S and a mode p ∈ P, γ −1
p (ReachTb(K v , p v , [t b ,t e ])) is a
reachtube of the real system (1) with mode p starting from γ −1
p (K v ). Similarly, given
any initial set K ⊂ S, γ p (ReachTb(K, p, [t b ,t e ])) is a reachtube of the virtual system (5)
starting from γ p (K).
Consequently, we get a solution or a reachtube for each mode p ∈ P of the real
system by simply transforming a single solution or a single reachtube of the virtual
system using the transformations {γ p } p∈P and their inverses. This will be the essential
idea behind the savings in computation time of the new symmetry-based reachtube
computation algorithm and symmetry-based safety verification algorithms presented
next. It will be also the essential idea behind proving safety in the case of unbounded
time and infinite number of modes.
179
and γ p ( f (x, p)) = f (γ p (x), ρ p (p v )) = f (γ p (x), p v ). Consider the resulting ODE:
dξ
dt
(y, p v ,t) = f (ξ (y, p v ,t), p v ).
(5)
Following [27], we call (5) a virtual system. Correspondingly, we call (1), the real system
for the rest of the paper. The virtual system unifies the behavior of all modes of the real
system in one representative mode, the virtual one p v .
Example 3 (Fixed-wing aircraft virtual system). Consider the fixed-wing aircraft agent
described in Example 1 and the corresponding transformations described in Example 2.
Fix p ∈ P, we set goal in the transformation of Example 2 to [p[2], p[3]] and θ to
arctan 2 (p[0] − p[2], p[3] − p[1]) and let γ p and ρ p be the resulting transformations. Then,
for all p ∈ P, ρ p (p) = [0, 0, 0, 0]. Hence, p v = [0, 0, 0, 0] and the virtual system is that of
Example 1 with the parameter p = p v . For the aircraft, γ p would translate the origin of
the plane to the destination waypoint and rotate its axes so that the y-axis is aligned with
the segment between the source and destination waypoints. Hence, in the constructed
virtual system, the destination waypoint is the origin of the plane. The source waypoint
is the origin as well as it does not affect the dynamics.
The solutions of the virtual system can be transformed to get solutions of all other
modes in P using {γ −1
p } p∈P . This is shown in the following theorem.
Theorem 3. Given any initial state y 0 ∈ S, and any mode p ∈ P, γ −1
p (ξ (y 0 , p v , ·)) is a
solution of the real system (1) with mode p starting from γ −1
p (y 0 ). Similarly, given any
x 0 ∈ S, γ p (ξ (x 0 , p, ·)) is the solution of the virtual system (5) starting from γ p (x 0 ).
Proof. Lets start with the first part of the theorem. Fix p ∈ P and let x 0 = γ −1
p (y 0 ).
Using Theorem 1, γ p (ξ (x 0 , p, ·)) = ξ (γ p (x 0 ), ρ p (p), ·)) and is the solution of the real
system (1). Furthermore, ρ p (p) = p v , by definition, and γ p (x 0 ) = γ p (γ −1
p (y 0 )) = y 0 .
Hence, γ p (ξ (x 0 , p, ·)) = ξ (y 0 , p v , ·). Applying γ −1
p on both sides implies the first part of
the theorem. The second part is a direct application of Theorem 1.
The following corollary extends the result of Theorem 3 to reachtubes. It follows
from Theorem 2.
Corollary 1. Given a K v ⊆ S and a mode p ∈ P, γ −1
p (ReachTb(K v , p v , [t b ,t e ])) is a
reachtube of the real system (1) with mode p starting from γ −1
p (K v ). Similarly, given
any initial set K ⊂ S, γ p (ReachTb(K, p, [t b ,t e ])) is a reachtube of the virtual system (5)
starting from γ p (K).
Consequently, we get a solution or a reachtube for each mode p ∈ P of the real
system by simply transforming a single solution or a single reachtube of the virtual
system using the transformations {γ p } p∈P and their inverses. This will be the essential
idea behind the savings in computation time of the new symmetry-based reachtube
computation algorithm and symmetry-based safety verification algorithms presented
next. It will be also the essential idea behind proving safety in the case of unbounded
time and infinite number of modes.