186
H. Sibai et al.
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 [ j].guard is a hyper-rectangle in the state space which when the agent reaches,
it transitions to the ( j + 1) st mode. The guard H i [ j] has time bound H i [ j].T on how long
the agent can stay in the mode. Moreover, it specifies the initial set of states for each
agent as a hyper-rectangle. Finally, it specifies the static unsafe set U and the subset of
dimensions O ⊆ [n] that is relevant for dynamic safety checking between agents. If the
reachtubes of two agents projected on O intersect each other, it would model a collision
between the agents. For example, O would be {2, 3} for the aircraft model in Example 1
as (x[2], x[3]) represents its position.
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.
3 https://github.com/tulip-control/polytope
H. Sibai et al.
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 [ j].guard is a hyper-rectangle in the state space which when the agent reaches,
it transitions to the ( j + 1) st mode. The guard H i [ j] has time bound H i [ j].T on how long
the agent can stay in the mode. Moreover, it specifies the initial set of states for each
agent as a hyper-rectangle. Finally, it specifies the static unsafe set U and the subset of
dimensions O ⊆ [n] that is relevant for dynamic safety checking between agents. If the
reachtubes of two agents projected on O intersect each other, it would model a collision
between the agents. For example, O would be {2, 3} for the aircraft model in Example 1
as (x[2], x[3]) represents its position.
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.
3 https://github.com/tulip-control/polytope