Multi-Agent Safety Verification using Symmetry Transformations
177
3 Symmetry and Equivariant Dynamical Systems
Symmetry plays a fundamental role in the analysis of dynamical systems. It has been
used for studying stability of feedback systems [25], designing observers [5] and controllers [30], and analyzing neural networks [20]. In this section, we present definitions
of symmetries and their implications on systems that posses them.
3.1 Symmetry of systems with inputs
In the following, symmetry transformations are defined by the ability of computing new
solutions of (1) using already computed ones. First, let Γ be a group of smooth maps
acting on S.
Definition 4 (Definition 2 in [27]). We say that γ ∈ Γ is a symmetry of (1) if for any
solution ξ (x 0 , p, ·), γ(ξ (x 0 , p, ·)) is also a solution.
Using γ-symmetry, we can get a new trajectory without simulating the system but
instead by just transforming the entire old trajectory using γ.
In the following definition we characterize the conditions under which a transformation is a symmetry of (1).
Definition 5. The dynamic function f : S × P → S is said to be Γ -equivariant if for any
γ ∈ Γ , there exists ρ : P → P such that for all x ∈ S,
∂ γ
∂ x f (x, p) = f (γ(x), ρ(p)).
The following theorem shows that it is enough to check the condition in Definition 5
to prove that a transformation is a symmetry of (1).
Theorem 1 (part of Theorem 10 in [27]). If f is Γ -equivariant, then all maps in Γ
are symmetries of (1). Moreover, for any solution ξ (x 0 , p, ·) and γ ∈ Γ , γ(ξ (x 0 , p, ·)) =
ξ (γ(x 0 ), ρ(p), ·), where ρ is the transformation associated with γ in Definition 5.
Proof. Let y = γ(x), then ˙
y =
∂ γ
∂ x (˙ x) =
∂ γ
∂ x ( f (x, p)) = f (γ(x), ρ(p)) = f (y, ρ(p)). The
second equality is a result of the derivative chain rule. The 3 rd equality uses Definition 5.
Remark 1. If γ in Theorem 1 is linear, the condition in Definition 5 for a map γ to be a
symmetry becomes γ( f (x, p)) = f (γ(x), ρ(p)).
Example 2 (Fixed-wing aircraft coordinate transformation symmetry). Consider the
fixed-wing aircraft model of Example 1. Fix goal ∈ R 2 and θ ∈ R. Let γ : R 4 → R 4 and
ρ : R 4 → R 4 be defined as:
γ(x) = [x[0], x[1] + θ , (x[2] − goal[0]) cos(θ ) + (x[3] − goal[1]) sin(θ ),
− (x[2] − goal[0]) sin(θ ) + (x[3] − goal[1]) cos(θ )] and
(3)
ρ(p) = [0, 0, (p[2] − goal[0]) cos(θ ) + (p[3] − goal[1]) sin(θ ),
− (p[2] − goal[0]) sin(θ ) + (p[3] − goal[1]) cos(θ )].
(4)
Then, for all x ∈ S and p ∈ P, γ( f (x, p)) = f (γ(x), ρ(p)), where f is as in Section 2.1.
The transformation γ would change the origin of S from [0, 0, 0, 0] to [0, 0, goal[0], goal[1]].
177
3 Symmetry and Equivariant Dynamical Systems
Symmetry plays a fundamental role in the analysis of dynamical systems. It has been
used for studying stability of feedback systems [25], designing observers [5] and controllers [30], and analyzing neural networks [20]. In this section, we present definitions
of symmetries and their implications on systems that posses them.
3.1 Symmetry of systems with inputs
In the following, symmetry transformations are defined by the ability of computing new
solutions of (1) using already computed ones. First, let Γ be a group of smooth maps
acting on S.
Definition 4 (Definition 2 in [27]). We say that γ ∈ Γ is a symmetry of (1) if for any
solution ξ (x 0 , p, ·), γ(ξ (x 0 , p, ·)) is also a solution.
Using γ-symmetry, we can get a new trajectory without simulating the system but
instead by just transforming the entire old trajectory using γ.
In the following definition we characterize the conditions under which a transformation is a symmetry of (1).
Definition 5. The dynamic function f : S × P → S is said to be Γ -equivariant if for any
γ ∈ Γ , there exists ρ : P → P such that for all x ∈ S,
∂ γ
∂ x f (x, p) = f (γ(x), ρ(p)).
The following theorem shows that it is enough to check the condition in Definition 5
to prove that a transformation is a symmetry of (1).
Theorem 1 (part of Theorem 10 in [27]). If f is Γ -equivariant, then all maps in Γ
are symmetries of (1). Moreover, for any solution ξ (x 0 , p, ·) and γ ∈ Γ , γ(ξ (x 0 , p, ·)) =
ξ (γ(x 0 ), ρ(p), ·), where ρ is the transformation associated with γ in Definition 5.
Proof. Let y = γ(x), then ˙
y =
∂ γ
∂ x (˙ x) =
∂ γ
∂ x ( f (x, p)) = f (γ(x), ρ(p)) = f (y, ρ(p)). The
second equality is a result of the derivative chain rule. The 3 rd equality uses Definition 5.
Remark 1. If γ in Theorem 1 is linear, the condition in Definition 5 for a map γ to be a
symmetry becomes γ( f (x, p)) = f (γ(x), ρ(p)).
Example 2 (Fixed-wing aircraft coordinate transformation symmetry). Consider the
fixed-wing aircraft model of Example 1. Fix goal ∈ R 2 and θ ∈ R. Let γ : R 4 → R 4 and
ρ : R 4 → R 4 be defined as:
γ(x) = [x[0], x[1] + θ , (x[2] − goal[0]) cos(θ ) + (x[3] − goal[1]) sin(θ ),
− (x[2] − goal[0]) sin(θ ) + (x[3] − goal[1]) cos(θ )] and
(3)
ρ(p) = [0, 0, (p[2] − goal[0]) cos(θ ) + (p[3] − goal[1]) sin(θ ),
− (p[2] − goal[0]) sin(θ ) + (p[3] − goal[1]) cos(θ )].
(4)
Then, for all x ∈ S and p ∈ P, γ( f (x, p)) = f (γ(x), ρ(p)), where f is as in Section 2.1.
The transformation γ would change the origin of S from [0, 0, 0, 0] to [0, 0, goal[0], goal[1]].