188
H. Sibai et al.
Fig. 1: Reachtubes for three fixed-wing aircrafts (left) and three linear models (right).
Real reachtubes (top) vs. the virtual ones saved in tubecache (bottom).
computed. In the experiments, we always compute the full tubes even if it was detected
to be unsafe earlier to have a fair comparison of running times. Moreover, the execution
time does not include dynamic safety checking as the four versions of the experiments are
doing the same computations for that purpose. We are using CacheReach in all scenarios
with other reachability computation tools to decrease the degrees of freedom and show
the benefits of transforming reachtubes over computing them. The Sym versions result
in decrease of running time up-to 64% in the linear case with three agents. The ratio of
transformed vs. computed tubes increases as the number of agents increase. This means
that different agents are sharing reachtubes with each other in the virtual system. The
total number of reachtubes is the same, whether tubecache is used or not. This means that
the quality of the tubes, i.e. how tight they are, is the same whether we are transforming
from tubecache or computing from scratch since the initial sets of modes are computed
from intersections of reachtubes with guards. The fatter the reachtube is, the larger the
initial set gets and the larger the number of reachtubes need to be computed.
7 Discussion and conclusions
In this paper, we investigated how symmetry transformations and caching can help
achieve scalable, and possibly unbounded, verification of multi-agent systems. We
developed a notion of virtual system which define symmetry transformations for a broad
class of hybrid and dynamical agent models visiting waypoint sequences. Using virtual
system, we present a prototype tool called CacheReach that builds a cache of reachtubes
for the transformed virtual system, in a way that is agnostic of the representation of the
reachsets and the reachability analysis subroutine used. Our experimental evaluation
show significant improvement in computation time on simple examples and increased
savings as number of agents increase.
H. Sibai et al.
Fig. 1: Reachtubes for three fixed-wing aircrafts (left) and three linear models (right).
Real reachtubes (top) vs. the virtual ones saved in tubecache (bottom).
computed. In the experiments, we always compute the full tubes even if it was detected
to be unsafe earlier to have a fair comparison of running times. Moreover, the execution
time does not include dynamic safety checking as the four versions of the experiments are
doing the same computations for that purpose. We are using CacheReach in all scenarios
with other reachability computation tools to decrease the degrees of freedom and show
the benefits of transforming reachtubes over computing them. The Sym versions result
in decrease of running time up-to 64% in the linear case with three agents. The ratio of
transformed vs. computed tubes increases as the number of agents increase. This means
that different agents are sharing reachtubes with each other in the virtual system. The
total number of reachtubes is the same, whether tubecache is used or not. This means that
the quality of the tubes, i.e. how tight they are, is the same whether we are transforming
from tubecache or computing from scratch since the initial sets of modes are computed
from intersections of reachtubes with guards. The fatter the reachtube is, the larger the
initial set gets and the larger the number of reachtubes need to be computed.
7 Discussion and conclusions
In this paper, we investigated how symmetry transformations and caching can help
achieve scalable, and possibly unbounded, verification of multi-agent systems. We
developed a notion of virtual system which define symmetry transformations for a broad
class of hybrid and dynamical agent models visiting waypoint sequences. Using virtual
system, we present a prototype tool called CacheReach that builds a cache of reachtubes
for the transformed virtual system, in a way that is agnostic of the representation of the
reachsets and the reachability analysis subroutine used. Our experimental evaluation
show significant improvement in computation time on simple examples and increased
savings as number of agents increase.