Multi-Agent Safety Verification using Symmetry Transformations
185
The corollary means that from a single scenario safety check, i.e. an intersection operation between a reachtube ReachTb(K, p v , [0, T ]) and unsafe set U, we can deduce the
safety of any mode p ∈ P starting from γ −1
p (K) and running for T time units with respect
to the corresponding unsafe set γ −1
p (U). This would, for example, imply unbounded
time safety of a hybrid automaton under the assumption that the unsafe sets of the modes
are at the same relative position with respect to the reachtube. But, safetycache stores a
number of results of such operations. We can infer from each one of them the safety of
infinite scenarios. This is formalized in the following theorem which follows directly
from Corollary 2.
Theorem 6 (Infinite safety verification results from finite ones). For any mode p ∈ P,
initial set K ⊆ S, time bound T ≥ 0, and unsafe set U ⊂ S × R ≥0 , such that K ⊆ γ −1
p (K ),
U ⊆ γ −1
p (U ), and safetycache(K , T,U ) = 1, system (1) is safe.
As more results are added to safetycache, then we can deduce the safety of more
scenarios in all modes. If at a given point of time, we are sure that no new scenarios
would appear, we can deduce the safety for unbounded time and unbounded number of
agents with the same dynamics having scenarios already covered.
Example 5 (Fixed-wing aircraft infinite number of safety verification results from computing a single one). Consider the initial set K, mode p, time bound T , their corresponding virtual ones K v and p v , and the symmetry transformation γ p r considered in Example 4.
Let the unsafe set be U = [[0, −∞, 11.9, 5.1], [∞, ∞, 12.9, 6.1]] × R ≥0 and U v = γ p r (U).
Assume that rtube v ∩U v = /
0 and the result is stored in safetycache. Then, for all p ∈ P,
γ −1
p (rtube v ) ∩ γ −1
p (U v ) = /
0.
For the aircraft, U could represent a mountain. Crashing with the mountain at any
speed, heading angle, and time is unsafe. U v represents the relative position of the
mountain with respect to the segment of waypoints. Theorem 6 says that for any initial
set of states K of the aircraft and time bound T , if the relative positions of the aircraft,
unsafe set, and the segment of waypoints are the same or subsumed by those of K v , U v ,
and the origin, we can infer safety irrespective of their absolute positions.
6 Experimental evaluation
We implemented a software safety verification tool for multi-agent hybrid systems based
on symComputeReachtube using Python 3. We named it CacheReach. By hybrid, we
mean systems that transition between different modes under different conditions. We
tested it on a linear dynamical system and the aircraft model of Example 1, following
sequences of waypoints, using DryVR [18] and Flow* [8] as reachability subroutines.
Our code is available in a figshare repository [28] and has been tested on an Ubuntu
virtual machine available in another figshare repository [21].
6.1 CacheReach: multi-agent safety verification tool
Our tool CacheReach takes as input a JSON file specifying a list of N agents of dimension n. It also specifies the python file that contains the dynamics function f of
185
The corollary means that from a single scenario safety check, i.e. an intersection operation between a reachtube ReachTb(K, p v , [0, T ]) and unsafe set U, we can deduce the
safety of any mode p ∈ P starting from γ −1
p (K) and running for T time units with respect
to the corresponding unsafe set γ −1
p (U). This would, for example, imply unbounded
time safety of a hybrid automaton under the assumption that the unsafe sets of the modes
are at the same relative position with respect to the reachtube. But, safetycache stores a
number of results of such operations. We can infer from each one of them the safety of
infinite scenarios. This is formalized in the following theorem which follows directly
from Corollary 2.
Theorem 6 (Infinite safety verification results from finite ones). For any mode p ∈ P,
initial set K ⊆ S, time bound T ≥ 0, and unsafe set U ⊂ S × R ≥0 , such that K ⊆ γ −1
p (K ),
U ⊆ γ −1
p (U ), and safetycache(K , T,U ) = 1, system (1) is safe.
As more results are added to safetycache, then we can deduce the safety of more
scenarios in all modes. If at a given point of time, we are sure that no new scenarios
would appear, we can deduce the safety for unbounded time and unbounded number of
agents with the same dynamics having scenarios already covered.
Example 5 (Fixed-wing aircraft infinite number of safety verification results from computing a single one). Consider the initial set K, mode p, time bound T , their corresponding virtual ones K v and p v , and the symmetry transformation γ p r considered in Example 4.
Let the unsafe set be U = [[0, −∞, 11.9, 5.1], [∞, ∞, 12.9, 6.1]] × R ≥0 and U v = γ p r (U).
Assume that rtube v ∩U v = /
0 and the result is stored in safetycache. Then, for all p ∈ P,
γ −1
p (rtube v ) ∩ γ −1
p (U v ) = /
0.
For the aircraft, U could represent a mountain. Crashing with the mountain at any
speed, heading angle, and time is unsafe. U v represents the relative position of the
mountain with respect to the segment of waypoints. Theorem 6 says that for any initial
set of states K of the aircraft and time bound T , if the relative positions of the aircraft,
unsafe set, and the segment of waypoints are the same or subsumed by those of K v , U v ,
and the origin, we can infer safety irrespective of their absolute positions.
6 Experimental evaluation
We implemented a software safety verification tool for multi-agent hybrid systems based
on symComputeReachtube using Python 3. We named it CacheReach. By hybrid, we
mean systems that transition between different modes under different conditions. We
tested it on a linear dynamical system and the aircraft model of Example 1, following
sequences of waypoints, using DryVR [18] and Flow* [8] as reachability subroutines.
Our code is available in a figshare repository [28] and has been tested on an Ubuntu
virtual machine available in another figshare repository [21].
6.1 CacheReach: multi-agent safety verification tool
Our tool CacheReach takes as input a JSON file specifying a list of N agents of dimension n. It also specifies the python file that contains the dynamics function f of