Multi-Agent Safety Verification using Symmetry Transformations
175
2 Model and problem statement
Notations. We denote by N, R, and R ≥0 the sets of natural numbers, real numbers and
non-negative reals. Given a finite set S, its cardinality is denoted by |S|. Given N ∈ N, we
denote by [N] the set {1,..., N}. Given a vector v ∈ R n and a set L ⊆ [n], we denote the
projection of v to the indices in L by v[L]. We define an n-dimensional hyper-rectangle by
a 2d-array specifying its bottom-left and upper-right corners. We denote the projection
of a hyper-rectangle H on the set of dimensions L by H[L]. Given a function γ : R k → R k
and a set S ⊆ R k , we abuse notation and define γ(S) = {γ(x) | x ∈ S}. Moreover, given
S ∈ 2 R k × R ≥0 , we define γ(S) = {(γ(X),t) | (X,t) ∈ S}.
2.1 Agent mode dynamics
In this section, we define the syntax and semantics of the model that determines the
dynamics of an agent. We present the syntax first.
Definition 1 (syntax). The agent dynamics are defined by a tuple A = S, P, f , where
S ⊆ R n is its state space, P ⊆ R m is its parameter or mode space, and the dynamic
function f : S × P → S that is Lipschitz in the first argument.
The semantics of an agent dynamics is defined by trajectories, which describe the
evolution of states over time.
Definition 2 (semantics). For a given agent A = S, P, f , we call a function ξ : S × P ×
R ≥0 → S a trajectory if ξ is differentiable in its third argument, and given an initial state
x 0 ∈ S and a mode p ∈ P, ξ (x 0 , p, 0) = x 0 and for all t > 0,
dξ
dt
(x 0 , p,t) = f (ξ (x 0 , p,t), p).
(1)
We say that ξ (x 0 , p,t) is the state of A at time t when it starts from x 0 in mode p.
Given an initial state x 0 ∈ S and mode p ∈ P, the trajectory ξ (x 0 , p, ·) is the unique
solution of the ordinary differential equation (ODE) (1) since f is Lipschitz continuous.
Given a compact initial set K ⊆ S, a parameter p ∈ P, the set of reachable states of
A over a time interval [ftime, etime] is defined as
Reach(K, p, [ftime, etime]) = {x ∈ S | ∃x 0 ∈ K,t ∈ [ftime, etime], x = ξ (x 0 , p,t)}. (2)
We let Reach(K, p,t) denote the set of reachable states at time t. Unbounded reachset
from K and p is Reach(K, p, [ftime, ∞)).
The bounded time safety verification problem requires one to check if any state
reachable by A for a given initial set K and mode p is unsafe within a given time bound.
That is, given a time bound T > 0, p ∈ P, and an unsafe set U ⊆ S, we want to check
whether Reach(K, p, [0, T ]) ∩U = /
0.
175
2 Model and problem statement
Notations. We denote by N, R, and R ≥0 the sets of natural numbers, real numbers and
non-negative reals. Given a finite set S, its cardinality is denoted by |S|. Given N ∈ N, we
denote by [N] the set {1,..., N}. Given a vector v ∈ R n and a set L ⊆ [n], we denote the
projection of v to the indices in L by v[L]. We define an n-dimensional hyper-rectangle by
a 2d-array specifying its bottom-left and upper-right corners. We denote the projection
of a hyper-rectangle H on the set of dimensions L by H[L]. Given a function γ : R k → R k
and a set S ⊆ R k , we abuse notation and define γ(S) = {γ(x) | x ∈ S}. Moreover, given
S ∈ 2 R k × R ≥0 , we define γ(S) = {(γ(X),t) | (X,t) ∈ S}.
2.1 Agent mode dynamics
In this section, we define the syntax and semantics of the model that determines the
dynamics of an agent. We present the syntax first.
Definition 1 (syntax). The agent dynamics are defined by a tuple A = S, P, f , where
S ⊆ R n is its state space, P ⊆ R m is its parameter or mode space, and the dynamic
function f : S × P → S that is Lipschitz in the first argument.
The semantics of an agent dynamics is defined by trajectories, which describe the
evolution of states over time.
Definition 2 (semantics). For a given agent A = S, P, f , we call a function ξ : S × P ×
R ≥0 → S a trajectory if ξ is differentiable in its third argument, and given an initial state
x 0 ∈ S and a mode p ∈ P, ξ (x 0 , p, 0) = x 0 and for all t > 0,
dξ
dt
(x 0 , p,t) = f (ξ (x 0 , p,t), p).
(1)
We say that ξ (x 0 , p,t) is the state of A at time t when it starts from x 0 in mode p.
Given an initial state x 0 ∈ S and mode p ∈ P, the trajectory ξ (x 0 , p, ·) is the unique
solution of the ordinary differential equation (ODE) (1) since f is Lipschitz continuous.
Given a compact initial set K ⊆ S, a parameter p ∈ P, the set of reachable states of
A over a time interval [ftime, etime] is defined as
Reach(K, p, [ftime, etime]) = {x ∈ S | ∃x 0 ∈ K,t ∈ [ftime, etime], x = ξ (x 0 , p,t)}. (2)
We let Reach(K, p,t) denote the set of reachable states at time t. Unbounded reachset
from K and p is Reach(K, p, [ftime, ∞)).
The bounded time safety verification problem requires one to check if any state
reachable by A for a given initial set K and mode p is unsafe within a given time bound.
That is, given a time bound T > 0, p ∈ P, and an unsafe set U ⊆ S, we want to check
whether Reach(K, p, [0, T ]) ∩U = /
0.