Multi-Agent Safety Verification using Symmetry Transformations
181
The function getTube returns a set of reachtubes {ReachTb(K i , p v , [0, T i ])} i∈[h] , for
some h ∈ N, that are already stored in tubecache. Moreover, the union of K i s is the
largest subset of K that can be covered by the initial sets of the reachtubes in tubecache.
Formally,
tubecache.getTube(K) =
argmax
{ReachTb(K i ,p v ,[0,T i ])∈tubecache} i
Vol(K ∩ ∪ i K i ),
(6)
where Vol(·) is the Lebesgue measure of the set. Note that for any K ⊂ R n , a maximizer
of (6) would be the set of all reachtubes in tubecache. However, this is very inefficient
and it would be too conservative to be useful for checking safety. Therefore, getTube
should return the minimum number of reachtubes that maximize (6). Note that the
reachtubes in tubecache may have different time bounds. We will truncate or extend
them when used.
5.2 symComputeReachtube: symmetry-based reachtube computation
Given an initial set K ⊂ S, a mode p ∈ P, and time bound T , there are dozens of tools that
can return a ReachTb(K, p, [0, T ]). See [13,8,9] for examples of such tools and [26] for a
comprehensive survey. We denote this procedure by computeReachtube(K, p, [0, T ]).
Whenever a reachtube is needed, instead of calling computeReachtube, we will
use symmetry to retrieve corresponding reachtubes that are already stored in tubecache
and only compute what is not stored. We introduce Algorithm 1 which implements this
idea and name it symComputeReachtube.
It takes as input the initial set of the virtual system K v , the time bound T , and
tubecache. It returns a reachtube of the virtual system starting from K v and running
for T time units. Hence, to get a reachtube of the real system starting from an initial
set K and having a mode p and time bound T , we transform K using γ p to get K v , call
symComputeReachtube, and transform the result using γ −1
p .
First, it initializes restube v as an empty tube of the virtual system (5) to store the
result in line 2. It then gets the reachtubes from tubecache that corresponds to K v using
the getTube method in line 3. Now that it has the relevant tubes in storedtubes, it adjusts
their lengths based on the time bound T . For a retrieved tube with a time bound less
than T in line 5, symComputeReachtube extends the tube for the remaining time using
computeReachtube in lines 6-7, store the resulting tube in tubecache instead of the
shorter one in line 8. If the retrieved tube is longer than T (line 9), it trims it in line 10.
However, we keep the long one in the tubecache to not lose a computation we already
did. Then, the tube with the adjusted length is added to the result tube restube v in line 11.
The union of the initial sets of the tubes retrieved storedtubes may not contain all of
the initial set K v . That uncovered part is called K
v in line 12. The reachtube starting from
K
v would be computed from scratch using computeReachtube in line 13, stored in
tubecache in line 14, and added to restube v in line 15. The resulting tube of the virtual
system (5) is returned in line 16. This tube would be transformed by the calling algorithm
using γ −1
p to get the corresponding tube of the real system (5).
Theorem 4. The output of Algorithm 1 is an over-approximation of the reachtube
ReachTb(K v , p v , [0, T ]).
181
The function getTube returns a set of reachtubes {ReachTb(K i , p v , [0, T i ])} i∈[h] , for
some h ∈ N, that are already stored in tubecache. Moreover, the union of K i s is the
largest subset of K that can be covered by the initial sets of the reachtubes in tubecache.
Formally,
tubecache.getTube(K) =
argmax
{ReachTb(K i ,p v ,[0,T i ])∈tubecache} i
Vol(K ∩ ∪ i K i ),
(6)
where Vol(·) is the Lebesgue measure of the set. Note that for any K ⊂ R n , a maximizer
of (6) would be the set of all reachtubes in tubecache. However, this is very inefficient
and it would be too conservative to be useful for checking safety. Therefore, getTube
should return the minimum number of reachtubes that maximize (6). Note that the
reachtubes in tubecache may have different time bounds. We will truncate or extend
them when used.
5.2 symComputeReachtube: symmetry-based reachtube computation
Given an initial set K ⊂ S, a mode p ∈ P, and time bound T , there are dozens of tools that
can return a ReachTb(K, p, [0, T ]). See [13,8,9] for examples of such tools and [26] for a
comprehensive survey. We denote this procedure by computeReachtube(K, p, [0, T ]).
Whenever a reachtube is needed, instead of calling computeReachtube, we will
use symmetry to retrieve corresponding reachtubes that are already stored in tubecache
and only compute what is not stored. We introduce Algorithm 1 which implements this
idea and name it symComputeReachtube.
It takes as input the initial set of the virtual system K v , the time bound T , and
tubecache. It returns a reachtube of the virtual system starting from K v and running
for T time units. Hence, to get a reachtube of the real system starting from an initial
set K and having a mode p and time bound T , we transform K using γ p to get K v , call
symComputeReachtube, and transform the result using γ −1
p .
First, it initializes restube v as an empty tube of the virtual system (5) to store the
result in line 2. It then gets the reachtubes from tubecache that corresponds to K v using
the getTube method in line 3. Now that it has the relevant tubes in storedtubes, it adjusts
their lengths based on the time bound T . For a retrieved tube with a time bound less
than T in line 5, symComputeReachtube extends the tube for the remaining time using
computeReachtube in lines 6-7, store the resulting tube in tubecache instead of the
shorter one in line 8. If the retrieved tube is longer than T (line 9), it trims it in line 10.
However, we keep the long one in the tubecache to not lose a computation we already
did. Then, the tube with the adjusted length is added to the result tube restube v in line 11.
The union of the initial sets of the tubes retrieved storedtubes may not contain all of
the initial set K v . That uncovered part is called K
v in line 12. The reachtube starting from
K
v would be computed from scratch using computeReachtube in line 13, stored in
tubecache in line 14, and added to restube v in line 15. The resulting tube of the virtual
system (5) is returned in line 16. This tube would be transformed by the calling algorithm
using γ −1
p to get the corresponding tube of the real system (5).
Theorem 4. The output of Algorithm 1 is an over-approximation of the reachtube
ReachTb(K v , p v , [0, T ]).