Multi-Agent Safety Verification using Symmetry Transformations
183
starting from different initial sets and for different time horizons is needed. We will
use the virtual system (5) and the transformations {γ p } p∈P to share safety computations
across modes, initial sets, time horizons, and unsafe sets.
We first introduce safetycache, a shared memory to store the results of intersecting
reachtubes of the virtual system (5) with different unsafe sets. It will prevent repeating
safety checking computations of different modes under similar scenarios and can be
used in finding unbounded time safety properties of the real system (1).
Definition 7. A safetycache is a data structure that stores the results of intersecting
reachtubes of the virtual system (5) with unsafe sets. It has two functions: getIntersect,
for retrieving stored results and storeIntersect, for storing a newly computed one.
Given an initial set K v , a time bound T , and an unsafe set U v , the reachtube rtube =
ReachTb(K v , p v , [0, T ]) is unsafe if there is another one rtube
= ReachTb(K
v , p v , [0, T ]),
is unsafe, and is an under-approximation of rtube. Similarly, if rtube
is an overapproximation of rtube and is safe, then rtube is safe. Formally, the getIntersect function of safetycache returns the truth value of the predicate ReachTb(K v , p v , [0, T ]) ∩U v =
/
0 if a subsuming computation is stored, and returns ⊥, otherwise.
Formally, safetycache.getIntersect(K v , T,U v ) =
⎧
⎪
⎨
⎪
⎩
0, if ∃ K
v , T ,U
v | K v ⊇ K
v , T ≥ T ,U v ⊇ U
v , safetycache(K
v , T ,U
v ) = 0,
1, if ∃ K
v , T ,U
v | K v ⊆ K
v , T ≤ T ,U v ⊆ U
v , safetycache(K
v , T ,U
v ) = 1, and
⊥, otherwise,
where 0 means unsafe and 1 means safe.
It is equivalent to check the intersection of a reachtube of the real system (1) with an
unsafe set U and to check the intersection of the corresponding reachtube and unsafe set
of the virtual one. This is formalized in the following lemma.
Lemma 1. Consider an unsafe set U ⊆ R n × R + and rtube = ReachTb(K, p, [t 1 ,t 2 ]).
Then, for any invertible γ : R n → R n , rtube ∩U = /
0 if and only if γ(rtube) ∩ γ(U) = /
0.
Now that we have established the equivalence of safety checking between the real
and virtual systems, we present Algorithm 2 denoted by symSafetyVerif. It uses
safetycache, tubecache, and symComputeReachtube in order to share safety verification computations across modes. The method symSafetyVerif would be called several
times to check safety of different scenarios and safetycache and tubecache would be
maintained across calls.
The function symSafetyVerif takes as input an initial set K, a mode p, a time
bound T , an unsafe set U, the transformation γ p , and safetycache and tubecache that
resulted from previous runs of the algorithm.
It starts by transforming the initial and unsafe sets K and U to a virtual system
initial and unsafe sets K v and U v using γ p in line 2. It then checks if a subsuming
result of the safety check for the tuple (K v , T,U v ) exists in safetycache using its method
getIntersect in line 3. If it does exist, it returns it directly in line 8. Otherwise,
the approximate reachtube is computed using symComputeReachtube in line 5. The
returned tube is intersected with U v in line 6 and the result of the intersection is stored in
safetycache in line 7 and returned in line 8.