174
H. Sibai et al.
from a small neighborhood around the initial state of ξ . Thus, the computed neighboring
set of behaviors always contains ξ and its size is determined by the algorithms for
sensitivity analysis. In contrast, the type of generalization we pursue here uses symmetry
transforms on the state space. Given a group Γ of operators on the state space, and a single behavior ξ , we can generalize ξ to γ(ξ ), for each γ ∈ Γ . Symmetry transformations
can be applied to sets of behaviors symbolically. Not only can this type of generalization
work in conjunction with sensitivity analysis, it captures structural properties of the
system that make behaviors similar in a way that is not covered by sensitivity analysis.
In our recent work [29], we showed how symmetry transforms can be used to produce new reachsets from other previously computed reachsets for non-parameterized
dynamical systems. In this paper, we introduce the use of symmetry transforms of
parameterized dynamical systems for safety verification. We present an algorithm
symComputeReachtube (Algorithm 1) which caches and reuses reachsets, avoiding
repeating expensive computations. We show how an infinite number of reachsets can
be obtained by transforming a single one using symmetry transforms (Corollary 2).
Building on it, we provide unbounded time safety guarantees using finite cached safety
checking results (Theorem 6).
The key contributions of this paper are as follows.
First, we show how symmetry transformations for parameterized dynamical systems
can be used to compute reachable states (Theorem 2). Going well beyond the previous
theory [29], this enables cached reachtubes to be reused for verification across different
modes and across multiple agents.
We develop a notion of virtual system (Section 4) which automatically defines
symmetry transformations for a broad swathe of hybrid and dynamical systems modeling
agents visiting a sequence of waypoints (see Theorem 3 and Examples 3 and 4). That
is, reachability analysis of a multi-agent system, with possibly different dynamics and
different parameters, can be performed in a common transformed coordinate system, and
thus, increases the possibility of reuse. We show how this principle can make it possible
to verify systems over unbounded time and with infinite number of agents (Theorem 6),
provided that no new unproven scenarios appear for the virtual system.
We present a prototype implementation of a tool that uses symComputeReachtube.
We name it CacheReach. It builds a cache of reachtubes for the virtual system, from
different sets of initial states. In performing reachability analysis of a multi-agent hybrid
or dynamical system, for each agent and each mode, the algorithm proceeds as follows:
(1) transform the initial set X to an initial set of the virtual system to get γ(X). (2) If
the transformed set γ(X) has already been stored in the cache, then extract it and apply
γ −1 to get the actual reachset. (3) Otherwise, compute the reachset from γ(X) and cache
it. Our algorithm symComputeReachtube and its implementation in CacheReach are
agnostic of the representation of the reachsets and the reachability analysis subroutine,
and therefore, any of the ever-improving libraries can be plugged-in for step 3.
Our experimental evaluation of CacheReach shows safety verification computation
time savings of up to 64% on scenarios with multiple agents with 3-dimensional linear
and 4-dimensional nonlinear fixed-wing aircraft model following sequences of waypoints.
These savings illustrate the potential benefits of using symmetry transformations and
caching in the safety verification of multi-agent systems.
H. Sibai et al.
from a small neighborhood around the initial state of ξ . Thus, the computed neighboring
set of behaviors always contains ξ and its size is determined by the algorithms for
sensitivity analysis. In contrast, the type of generalization we pursue here uses symmetry
transforms on the state space. Given a group Γ of operators on the state space, and a single behavior ξ , we can generalize ξ to γ(ξ ), for each γ ∈ Γ . Symmetry transformations
can be applied to sets of behaviors symbolically. Not only can this type of generalization
work in conjunction with sensitivity analysis, it captures structural properties of the
system that make behaviors similar in a way that is not covered by sensitivity analysis.
In our recent work [29], we showed how symmetry transforms can be used to produce new reachsets from other previously computed reachsets for non-parameterized
dynamical systems. In this paper, we introduce the use of symmetry transforms of
parameterized dynamical systems for safety verification. We present an algorithm
symComputeReachtube (Algorithm 1) which caches and reuses reachsets, avoiding
repeating expensive computations. We show how an infinite number of reachsets can
be obtained by transforming a single one using symmetry transforms (Corollary 2).
Building on it, we provide unbounded time safety guarantees using finite cached safety
checking results (Theorem 6).
The key contributions of this paper are as follows.
First, we show how symmetry transformations for parameterized dynamical systems
can be used to compute reachable states (Theorem 2). Going well beyond the previous
theory [29], this enables cached reachtubes to be reused for verification across different
modes and across multiple agents.
We develop a notion of virtual system (Section 4) which automatically defines
symmetry transformations for a broad swathe of hybrid and dynamical systems modeling
agents visiting a sequence of waypoints (see Theorem 3 and Examples 3 and 4). That
is, reachability analysis of a multi-agent system, with possibly different dynamics and
different parameters, can be performed in a common transformed coordinate system, and
thus, increases the possibility of reuse. We show how this principle can make it possible
to verify systems over unbounded time and with infinite number of agents (Theorem 6),
provided that no new unproven scenarios appear for the virtual system.
We present a prototype implementation of a tool that uses symComputeReachtube.
We name it CacheReach. It builds a cache of reachtubes for the virtual system, from
different sets of initial states. In performing reachability analysis of a multi-agent hybrid
or dynamical system, for each agent and each mode, the algorithm proceeds as follows:
(1) transform the initial set X to an initial set of the virtual system to get γ(X). (2) If
the transformed set γ(X) has already been stored in the cache, then extract it and apply
γ −1 to get the actual reachset. (3) Otherwise, compute the reachset from γ(X) and cache
it. Our algorithm symComputeReachtube and its implementation in CacheReach are
agnostic of the representation of the reachsets and the reachability analysis subroutine,
and therefore, any of the ever-improving libraries can be plugged-in for step 3.
Our experimental evaluation of CacheReach shows safety verification computation
time savings of up to 64% on scenarios with multiple agents with 3-dimensional linear
and 4-dimensional nonlinear fixed-wing aircraft model following sequences of waypoints.
These savings illustrate the potential benefits of using symmetry transformations and
caching in the safety verification of multi-agent systems.