key: cord-0048956-3pkr4qow
authors: Sibai, Hussein; Mokhlesi, Navid; Fan, Chuchu; Mitra, Sayan
title: Multi-agent Safety Verification Using Symmetry Transformations
date: 2020-03-13
journal: Tools and Algorithms for the Construction and Analysis of Systems
DOI: 10.1007/978-3-030-45190-5_10
sha: ea96f47115c288e69f3df392115bd138632756fc
doc_id: 48956
cord_uid: 3pkr4qow

We show that symmetry transformations and caching can enable scalable, and possibly unbounded, verification of multi-agent systems. Symmetry transformations map any solution of the system to another solution. We show that this property can be used to transform cached reachsets to compute new reachsets, for hybrid and multi-agent models. We develop a notion of a virtual system which defines symmetry transformations for a broad class of agent models that visit waypoint sequences. Using this notion of a virtual system, we present a prototype tool CacheReach that builds a cache of reachsets, in a way that is agnostic of the representation of the reachsets and the reachability analysis method used. Our experimental evaluation of CacheReach shows up to 64% savings in safety verification computation time on multi-agent systems with 3-dimensional linear and 4-dimensional nonlinear fixed-wing aircraft models following sequences of waypoints. These savings and our theoretical results illustrate the potential benefits of using symmetry-based caching in the safety verification of multi-agent systems.

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.

Notations. We denote by N, R, and R ≥0 the sets of natural numbers, real numbers and non-negative reals. Given a finite set S, its cardinality is denoted by |S|. Given N ∈ N, we denote by [N] the set {1, . . . , N}. Given a vector v ∈ R n and a set L ⊆ [n], we denote the projection of v to the indices in L by v[L]. We define an n-dimensional hyper-rectangle by a 2d-array specifying its bottom-left and upper-right corners. We denote the projection of a hyper-rectangle H on the set of dimensions L by H[L]. Given a function γ : R k → R k and a set S ⊆ R k , we abuse notation and define γ(S) = {γ(x) | x ∈ S}. Moreover, given

In this section, we define the syntax and semantics of the model that determines the dynamics of an agent. We present the syntax first.

Definition 1 (syntax). The agent dynamics are defined by a tuple A = S, P, f , where S ⊆ R n is its state space, P ⊆ R m is its parameter or mode space, and the dynamic function f : S × P → S that is Lipschitz in the first argument.

The semantics of an agent dynamics is defined by trajectories, which describe the evolution of states over time.

Definition 2 (semantics). For a given agent A = S, P, f , we call a function ξ : S × P × R ≥0 → S a trajectory if ξ is differentiable in its third argument, and given an initial state x 0 ∈ S and a mode p ∈ P, ξ (x 0 , p, 0) = x 0 and for all t > 0,

We say that ξ (x 0 , p,t) is the state of A at time t when it starts from x 0 in mode p.

Given an initial state x 0 ∈ S and mode p ∈ P, the trajectory ξ (x 0 , p, ·) is the unique solution of the ordinary differential equation (ODE) (1) since f is Lipschitz continuous. Given a compact initial set K ⊆ S, a parameter p ∈ P, the set of reachable states of A over a time interval [ftime, etime] is defined as

We let Reach(K, p,t) denote the set of reachable states at time t. Unbounded reachset from K and p is Reach(K, p, [ftime, ∞)).

The bounded time safety verification problem requires one to check if any state reachable by A for a given initial set K and mode p is unsafe within a given time bound. That is, given a time bound T > 0, p ∈ P, and an unsafe set U ⊆ S, we want to check whether Reach(K, p, [0, T ]) ∩U = / 0.

Computing reachsets exactly is theoretically hard [22] . There are many reachability analysis tools [8, 1, 3] that can compute bounded-time over-approximations of the reachsets. Generally, given an initial set K for a set of ODEs, these tools can return a sequence of sets that contain the exact reachset over small time intervals. Motived by this, we define reachtubes as sequences of time-annotated over-approximations of exact reachsets:

Definition 3. For a given agent A = S, P, f , an initial set K ⊆ T , a mode p ∈ P, and a time interval

) ⊆ X i , and τ 0 = ftime < τ 1 < · · · < τ j = etime. Without loss of generality, we assume equal separation between the time points, i.e. ∃ τ

For a given (K, p, [ftime, etime])-reachtube rtube, we denote its parameters by rtube.K, rtube.p, rtube.ftime, and rtube.etime, respectively, and its cardinality by rtube.len.

We define union, truncation, concatenate, and time-shift operators on reachtubes. Fix

to be two reachtubes, where j 1 = rtube 1 .len and j 2 = rtube 2 .len. If τ i,1 = τ i,2 for all i ∈ [min( j 1 , j 2 )], we say they are time-aligned. Without loss of generality, assume that j 1 ≤ j 2 . The operators are defined as follows:

A simulation of system (1) is a reachtube with X 0 being a singleton state x 0 ∈ K. That is, a simulation is a representation of ξ (x 0 , p, ·). Several numerical solvers can compute such simulations as VNODE-LP 1 and CAPD Dyn-Sys library 2 .

Example 1 (Fixed-wing aircraft following a single waypoint). Consider an agent with state space S = R 4 , parameter space P = R 4 , and f : S × P → S defined as follows: for any x ∈ S and p ∈ P, [3] ), and k 1 , k 2 , m, g, c d1 , and v c are positive constants. The agent models a fixed-wing aircraft starting from a waypoint and following another in the 2D plane: x[0] is its speed, x[1] is its heading angle, (x[2], x [3] ) is its position in the plane, [p[0], p [1] ] is the position of the source waypoint, and (p [2] , p [3] ) is the position of the destination one. Note that the source waypoint does not affect the dynamics, but will be useful later in the paper.

Symmetry plays a fundamental role in the analysis of dynamical systems. It has been used for studying stability of feedback systems [25] , designing observers [5] and controllers [30] , and analyzing neural networks [20] . In this section, we present definitions of symmetries and their implications on systems that posses them.

In the following, symmetry transformations are defined by the ability of computing new solutions of (1) using already computed ones. First, let Γ be a group of smooth maps acting on S.

). We say that γ ∈ Γ is a symmetry of (1) if for any solution ξ (x 0 , p, ·), γ(ξ (x 0 , p, ·)) is also a solution.

Using γ-symmetry, we can get a new trajectory without simulating the system but instead by just transforming the entire old trajectory using γ.

In the following definition we characterize the conditions under which a transformation is a symmetry of (1).

The dynamic function f : S × P → S is said to be Γ -equivariant if for any

). The following theorem shows that it is enough to check the condition in Definition 5 to prove that a transformation is a symmetry of (1).

Theorem 1 (part of Theorem 10 in [27] ). If f is Γ -equivariant, then all maps in Γ are symmetries of (1). Moreover, for any solution ξ (x 0 , p, ·) and γ ∈ Γ , γ(ξ (x 0 , p, ·)) = ξ (γ(x 0 ), ρ(p), ·), where ρ is the transformation associated with γ in Definition 5.

, ρ(p)) = f (y, ρ(p)). The second equality is a result of the derivative chain rule. The 3 rd equality uses Definition 5.

Remark 1. If γ in Theorem 1 is linear, the condition in Definition 5 for a map γ to be a symmetry becomes γ( f (x, p)) = f (γ(x), ρ(p)).

Example 2 (Fixed-wing aircraft coordinate transformation symmetry). Consider the fixed-wing aircraft model of Example 1. Fix goal ∈ R 2 and θ ∈ R. Let γ : R 4 → R 4 and ρ : R 4 → R 4 be defined as:

Then, for all x ∈ S and p ∈ P, γ( f (x, p)) = f (γ(x), ρ(p)), where f is as in Section 2.1. The transformation γ would change the origin of S from [0, 0, 0, 0] to [0, 0, goal[0], goal [1] ].

Then, it would rotate the third and four axes counter-clockwise by θ . Moreover, ρ would set the first two coordinates of the parameters to zero as they do not affect the dynamics, translate the origin of the parameter space P to [0, 0, goal[0], goal [1] ], and rotate the third and fourth axes counter-clockwise by θ . For the aircraft, this means translating and rotating the plane where the aircraft and the waypoint positions reside.

Computing reachtubes is computationally expensive as it requires non-trivial optimization problems and integrating non-linear functions [13, 15, 16, 8, 6] . Compared with that, transforming reachtubes is much cheaper, especially if the transformation is linear.

In our previous work [29] , we showed how to get reachtubes of autonomous systems from previously computed ones using symmetry transformations. In this paper, we show how to do that for systems with parameters. This allows different modes of a hybrid system and different agents with similar dynamics to share reachtube computations. That was not possible when the theory was limited to non-parameterized systems.

Theorem 2. Let (1) be Γ -equivariant. Then for any γ ∈ Γ and its corresponding ρ, any

being an over-approximation of the exact reachset during the small time intervals

Theorem 2 says that we can transform a computed reachtube ReachTb(K, p, [t 1 ,

, which is an overapproximation of the reachsets starting from γ(K).

The results of this section subsume the results about transforming reachtubes of autonomous systems-dynamical systems without parameters as presented in [29] .

The challenge in safety verification of multi-agent systems is that the dimensionality of the problem grows rapidly with the number of agents. However, often agents share the same dynamics. For instance, several fixed-wing aircrafts of the type described in Example 1 share the same dynamics but may have different initial conditions and follow different waypoints. This commonality has been exploited in developing specialized proof techniques [23] . For reachability analysis, using symmetry transforms of the previous section, reachtubes of one agent in one mode can be used to get the reachtubes of other modes and even other agents.

Fix a particular value p v ∈ P and call it the virtual parameter. Assume that for all p ∈ P, there exists a pair of transformations (γ p , ρ p ) such that ρ p (p) = p v , γ p is invertible,

Following [27], we call (5) a virtual system. Correspondingly, we call (1), the real system for the rest of the paper. The virtual system unifies the behavior of all modes of the real system in one representative mode, the virtual one p v .

Example 3 (Fixed-wing aircraft virtual system). Consider the fixed-wing aircraft agent described in Example 1 and the corresponding transformations described in Example 2. Fix p ∈ P, we set goal in the transformation of Example 2 to [p [2] , p [3] ] and θ to [1] ) and let γ p and ρ p be the resulting transformations. Then, for all p ∈ P, ρ p (p) = [0, 0, 0, 0]. Hence, p v = [0, 0, 0, 0] and the virtual system is that of Example 1 with the parameter p = p v . For the aircraft, γ p would translate the origin of the plane to the destination waypoint and rotate its axes so that the y-axis is aligned with the segment between the source and destination waypoints. Hence, in the constructed virtual system, the destination waypoint is the origin of the plane. The source waypoint is the origin as well as it does not affect the dynamics.

The solutions of the virtual system can be transformed to get solutions of all other modes in P using {γ −1 p } p∈P . This is shown in the following theorem.

Theorem 3. Given any initial state y 0 ∈ S, and any mode p ∈ P, γ −1 p (ξ (y 0 , p v , ·)) is a solution of the real system (1) with mode p starting from γ −1 p (y 0 ). Similarly, given any x 0 ∈ S, γ p (ξ (x 0 , p, ·)) is the solution of the virtual system (5) starting from γ p (x 0 ).

Proof. Lets start with the first part of the theorem. Fix p ∈ P and let x 0 = γ −1 p (y 0 ). Using Theorem 1, γ p (ξ (x 0 , p, ·)) = ξ (γ p (x 0 ), ρ p (p), ·)) and is the solution of the real system (1). Furthermore, ρ p (p) = p v , by definition, and γ p (x 0 ) = γ p (γ −1 p (y 0 )) = y 0 . Hence, γ p (ξ (x 0 , p, ·)) = ξ (y 0 , p v , ·). Applying γ −1 p on both sides implies the first part of the theorem. The second part is a direct application of Theorem 1.

The following corollary extends the result of Theorem 3 to reachtubes. It follows from Theorem 2.

) is a reachtube of the real system (1) with mode p starting from γ −1

) is a reachtube of the virtual system (5) starting from γ p (K).

Consequently, we get a solution or a reachtube for each mode p ∈ P of the real system by simply transforming a single solution or a single reachtube of the virtual system using the transformations {γ p } p∈P and their inverses. This will be the essential idea behind the savings in computation time of the new symmetry-based reachtube computation algorithm and symmetry-based safety verification algorithms presented next. It will be also the essential idea behind proving safety in the case of unbounded time and infinite number of modes.

Example 4 (Fixed-wing aircraft infinite number of reachtubes resulting from transforming a single one). Consider the real system in Example 1 and the virtual one in Example 3. Fix the initial set, which is represented as a hyper-rectangle, K r = [[1, π 4 , 3, 1], [2, π 3 , 4, 2]], the real mode p r = [2.5, 0. 5, 13.3, 5] , and the time bound 20 seconds. Then, similar to Example 3, we fix θ = arctan 2 (2.5 − 13.3, 5 − 0.5) = −1.176 rad and goal = [13.3, 5] . We call the resulting transformations from Example 3, γ p r and ρ p r . Let K v = γ p r (K r ) and p v = ρ p r (p r ) = [0, 0, 0, 0]. Assume that we have the reachtube rtube r = ReachTb(K r , p r , T ). Then, using Corollary 1, we can get rtube v = ReachTb(K v , p v , T ) by transforming rtube r using γ p r . The benefit of the corollary appears in the following: for any p ∈ P = R 4 , we can get the corresponding reachtube ReachTb(γ −1 p (K v ), p, T ) by transforming rtube v using γ −1 p . The projection of K v on its last two coordinates K v In summary, the absolute positions of the aircraft and waypoints do not matter. What matters is their relative positions. The virtual system stores what matters and whenever a reachtube is needed for a new absolute position, we can transform it from the virtual one.

In this section, we introduce a novel safety verification algorithm, symSafetyVerif, which uses existing reachability subroutines, but exploits symmetry, unlike existing algorithms. In our earlier work [29] , we introduced reachtube transformations using symmetry for single mode dynamical systems. Here, we extend the method across modes, introduce the virtual system, and develop the corresponding verification algorithm.

In Section 5.1, we define tubecache-a data-structure for storing reachtubes; in 5.2, we present the symmetry-based reachtube computation algorithm symComputeReachtube that reuses reachtubes stored in tubecache; finally, in 5.3, we define the safetycache datastructure which stores previously computed safety verification results. These results would be used by the symSafetyVerif algorithm.

We show how we use the virtual system (5) to create a shared memory for the different modes of the real system (1) to reuse each others' computed reachtubes. We call this shared memory tubecache.

Definition 6. A tubecache is a data structure that stores a set of reachtubes of the virtual system (5) . It has two methods: getTube, for retrieving stored tubes and storeTube, for storing a newly computed one.

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,

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.

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). if storedtubes[i].T < T then 6:

tubecache.storeTube(tube i ) 9:

else if storedtubes[i].T > T then 10:

Proof. The function computeReachtube always returns over-approximations of the reachset from a given initial set and for a given time bound. The set restube contains reachtubes that were computed by computeReachtube at some point. There are three types of reachtubes in restube: The union of the initial sets of the tubes in storedtubes and K v contains K v , so the union of the reachtubes the algorithm returns a (K v , p v , [0, T ])-reachtube.

The importance of symComputeReachtube lies in that if a mode p required a computation of a reachtube and the result is saved in tubecache, another mode with a similar scenario with respect to the virtual system would reuse that tube instead of computing one from scratch. Moreover, reachtubes of the same mode might be reused as well if the scenario was repeated again.

In this section, we show how to use tubecache and symComputeReachtube of the previous section for bounded and unbounded time safety verification of the real system (1). We consider a scenario where the safety verification of multiple modes of the real system (1) 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).

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 =

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

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.

1: input: K, p, T,U, γ p , safetycache, tubecache 2: However, if symSafetyVerif returns unsafe, it might be that rtube in line 5 intersected the unsafe set because of an over-approximation error. There are two sources of such errors: first, the method computeReachtube used by symComputeReachtube can itself result in over-approximation errors. Actually, it will, most of the time [13, 8] . But it may be exact too [3] . Second, the tubecache.getTube method which would return a list of tubes with the union of their initial sets strictly over-approximating the needed initial set. The first problem can be solved by asking the method computeReachtube to compute tighter reachtubes. Existing methods provide this option at the expense of worse computational complexity [13, 8] . However, we can use symmetry in these tightening computations as well, as we did in [29] . We can also replace saved tubes in tubecache with newly computed tighter ones. The second problem can be solved by asking tubecache.getTube to return only the tubes with initial sets that are fully contained in the asked initial set. This would decrease the savings from transforming cached results, but it would reduce the false-positive error, saying unsafe while it is safe.

In this section, we show how infinite number of results of safety checks, i.e. results of intersections of reachtubes with unsafe sets, can be deduced from finite ones. The following corollary applies Lemma 1 to the transformations {γ p } p∈P that map the different modes of the real system (1) to the unique virtual one (5).

Corollary 2 (Infinite safety verification results from a single one). Fix U ⊆ R n and rtube = ReachTb(K v , p v , [0, T ]). If rtube∩U = / 0, then ∀p ∈ P, γ −1 p (rtube)∩γ −1 p (U) = / 0.

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. Assume that rtube v ∩U v = / 0 and the result is stored in safetycache. Then, for all p ∈ P,

. 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.

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] .

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 Definition 1 and two symmetry-related functions: symGamma and symGammaInv. Given a p ∈ P and a polytope 3 poly of dimension n representing a set of states of the agent, symGamma returns γ p (poly), where γ p is the symmetry map to the virtual system. Similarly, symGammaInv would return γ −1 p (poly). The list of modes that the i th agent transition between sequentially and their corresponding transitions conditions, denoted by guards, are specified as well and denoted by H i . The guard of the j th mode of the i th agent H i CacheReach would return unsafe if the reachtubes of the agents starting from their initial sets of states and following the sequence of modes intersect a static unsafe set, or when projected to O, intersect each other. It would return safe, otherwise. Currently, CacheReach assumes that all agents share the same dynamics but do not interact. Hence, it has a single tubecache that is shared by all.

CacheReach computes the reachtubes of individual agents iteratively. It would compute the reachtube mtube i of the j th mode of the i th agent using symComputeReachtube. Then, it intersects it with the guard using the function guardIntersect to get the initial set initset i for the next mode. In addition to initset i , guardIntersect computes the minimum and maximum times: mintime i and maxtime i , respectively, at which mtube i intersects the guard. The value mintime i is the time at which a trajectory of the next mode may start at and maxtime i is the maximum such time. These values are used to check safety against time-annotated unsafe sets such as collision between agents.

The computed tube mtube i gets appended to atube i storing the full reachtube of the i th agent. The benefit of this method is that now all modes of all agents can be mapped to a single virtual system. They can resuse each others reachtubes using tubecache that is getting updated at every call to symComputeReachtube. Moreover, the static safety is done in the usual way.

The collision between agents is done by the function checkDynamicSafety. It takes two full reachtubes of two agents atube 1 and atube 2 along with two arrays lookback 1 and lookback 2 . For agent i, the array lookback i consists of pairs of integers (ind j , timerange j ) specifying the index identifying the beginning of the j th mode tube in atube i and the uncertainty in the starting time of the trajectories from its initial set. checkDynamicSafety would use this information to time-align parts of atube 1 and atube 2 so that the intersection check happens only between two sets that may have been reached at the same time by the two agents.

We ran experiments using our tool CacheReach on two models: a 3-dimensional linear dynamical system example and the nonlinear aircraft model described in Example 1. The linear model is of the formẋ = A(x− p [3 : 5] 

x ∈ R 3 , and p ∈ R 6 . We considered scenarios with single, two, and three agents for each model following different sequences of waypoints. The sequences of waypoints for the linear model are translations and rotations of a digital-S shaped path. For the aircraft model, the paths are random crossing paths going north-east. In every scenario, all the agents have the same model. In the aircraft scenarios, the agent would switch to the next waypoint once its x, y position is within 0.5 units from the current waypoint in each dimension. The initial set of the aircraft was of size 1 in the position components, 0.1 in the speed, and 0.01 in the heading angle. We used Flow* [8] and DryVR [18] to compute reachtubes from scratch for the linear example. We only used DryVR for the aircraft model since our C++ Flow* wrapper does not handle a model having arctan 2 in the dynamics. We ran all scenarios in CacheReach with and without using tubecache. The symmetry used for the aircraft was the one we showed in Example 3. For the linear model, the symmetry transformation γ p that was used to map the state to the virtual system was a coordinate transformation where the new origin is at the next waypoint p [3 : 5] and rotating the xy-plane by the angle between the previous and the next waypoints p[0 : 2] and p [3 : 5] projected to the plane. We compared the computation time with and without symmetry and show the results in Table 1 . The reachtubes for three nonlinear and three linear agents are shown in Figure 1 . The different colors represent reachtubes of different agents, the black points represent the waypoints, the black segments connect consecutive waypoints, and the red rectangles represent the unsafe sets. The figures on the top represent the real reachtubes while those on the bottom represent the ones corresponding to the virtual system saved in tubecache. In Table 1 , we call CacheReach, when ran with DryVR while using tubecache, Sym-DryVR, for symmetric DryVR. We call it Sym-Flow* if we are using Flow* instead. If we are not using tubecache, we call them NoSym-DryVR and NoSym-Flow*, respectively. Remember in symComputeReachtube, some tubes may be cached but they have shorter time horizons than the needed tube. So, we compute the rest from scratch. Here, we report the fractions of tubes computed from scratch and tubes that were transformed from cached ones. Moreover, we report the execution time till the tubes are 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.

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.

An introduction to cora 2015

Online verification of automated road vehicles using reachability analysis

Hylaa: A tool for computing simulation-equivalent reachability for linear systems

Numerical verification of affine systems with up to a billion dimensions

Symmetry-preserving observers

Reachability analysis of non-linear hybrid systems using taylor models

Flow*: An analyzer for non-linear hybrid systems

Flow*: An analyzer for non-linear hybrid systems

Breach, a toolbox for verification and parameter synthesis of hybrid systems

Systematic simulation using sensitivity analysis

Meeting a powertrain verification challenge

Verification of annotated models from executions

Tools and Algorithms for the Construction and Analysis of Systems

Parsimonious, simulation based verification of linear systems

Locally optimal reach set over-approximation for nonlinear systems

Bounded verification with on-the-fly discrepancy computation

Data-driven formal reasoning and their applications in safety analysis of vehicle autonomy features

Data-driven verification and compositional reasoning for automotive systems

Automatic reachability analysis for nonlinear hybrid models with C2E2

Neuronal networks and controlled symmetries, a generic framework

What's decidable about hybrid automata?

A small model theorem for rectangular hybrid automata networks

Models, devices, properties, and verification of artificial pancreas systems

Symmetry and symmetry-breaking for a wave equation with feedback

Symmetries, stability, and control in nonlinear systems and networks

Cachereach: multi-agent safety verification using symmetry transformations software tool

Using symmetry transformations in equivariant dynamical systems for their safety verification

Controlled symmetries and passive walking

), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use