184
H. Sibai et al.
Algorithm 2 symSafetyVerif
1: input: K, p, T,U, γ p , safetycache, tubecache
2: K v ← γ p (K), U v ← γ p (U)
3: result ← safetycache.getIntersect(K v , T,U v )
4: if result = ⊥ then
5:
rtube ← symComputeReachtube (K v , T, tubecache)
6:
result ← (tube ∩U v = /
0)
7:
safetycache.storeIntersect(K v , T,U v , result)
8: return: result
Theorem 5. If symSafetyVerif returns safe, then ReachTb(K, p, [0, T ]) ∩U = /
0.
Proof. From Theorem 4, if the result is not stored in safetycache, we know that rtube
in line 5 is an over-approximation of ReachTb(K v , p v , [0, T ]). Moreover, we know from
Corollary 1 that ReachTb(K, p, [0, T ]) ⊆ γ −1
p (rtube). But, from Lemma 1, we know that
the truth value of the predicate (rtube ∩U v = /
0) is equal to that of (γ −1
p (rtube) ∩U = /
0)
and hence result is safe if γ −1
p (rtube) ∩U = /
0 and thus it is safe if ReachTb(K, p, T ) ∩
U = /
0. Finally, the stored values in safetycache are results from previous runs, and hence
have the same property.
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.
5.4 Unbounded time safety
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.
H. Sibai et al.
Algorithm 2 symSafetyVerif
1: input: K, p, T,U, γ p , safetycache, tubecache
2: K v ← γ p (K), U v ← γ p (U)
3: result ← safetycache.getIntersect(K v , T,U v )
4: if result = ⊥ then
5:
rtube ← symComputeReachtube (K v , T, tubecache)
6:
result ← (tube ∩U v = /
0)
7:
safetycache.storeIntersect(K v , T,U v , result)
8: return: result
Theorem 5. If symSafetyVerif returns safe, then ReachTb(K, p, [0, T ]) ∩U = /
0.
Proof. From Theorem 4, if the result is not stored in safetycache, we know that rtube
in line 5 is an over-approximation of ReachTb(K v , p v , [0, T ]). Moreover, we know from
Corollary 1 that ReachTb(K, p, [0, T ]) ⊆ γ −1
p (rtube). But, from Lemma 1, we know that
the truth value of the predicate (rtube ∩U v = /
0) is equal to that of (γ −1
p (rtube) ∩U = /
0)
and hence result is safe if γ −1
p (rtube) ∩U = /
0 and thus it is safe if ReachTb(K, p, T ) ∩
U = /
0. Finally, the stored values in safetycache are results from previous runs, and hence
have the same property.
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.
5.4 Unbounded time safety
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.