182
H. Sibai et al.
Algorithm 1 symComputeReachtube
1: input: K v , T, tubecache
2: restube v ← /
0
3: storedtubes ← tubecache.getTube(K v )
4: for i ∈ [|storedtubes|] do
5:
if storedtubes[i].T < T then
6:
(K i , [τ i , T i ]) ← storedtubes[i].end
7:
tube i ← storedtubes[i] computeReachtube(K i , p v , [0, T − τ i ])
8:
tubecache.storeTube(tube i )
9:
else if storedtubes[i].T > T then
10:
tube i ← storedtubes[i].truncate(T )
11:
restube v ← restube v ∪ tube i
12: K
v ← K v \ ∪ i storedtubes[i].K
13: tube = computeReachtube(K
v , p v , [0, T ])
14: tubecache.storeTube(tube )
15: restube v ← restube v ∪ tube
16: return: restube v
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:
1. When the time bound T i of the stored reachtube storedtubes[i] is less than T ,
we need to extend storedtubes[i] until time T by concatenating the original tube
with computeReachtube(K i , p v , [0, T − τ i ]), where (K i , [τ i , T i ]) is the last pair in
storedtubes[i]. The result is a valid (storedtubes[i].K, p v , [0, T ])-reachtube.
2. When the time bound T i of the stored reachtube storedtubes[i] is more than T , the
truncated reachtube is also a valid (storedtubes[i].K, p v , [0, T ])-reachtube.
3. For K
v that is not contained in the union of the initial sets in storedtubes, the function
computeReachtube will return a valid (K
v , p v , [0, T ])-reachtube.
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.
5.3 Bounded time safety
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)
H. Sibai et al.
Algorithm 1 symComputeReachtube
1: input: K v , T, tubecache
2: restube v ← /
0
3: storedtubes ← tubecache.getTube(K v )
4: for i ∈ [|storedtubes|] do
5:
if storedtubes[i].T < T then
6:
(K i , [τ i , T i ]) ← storedtubes[i].end
7:
tube i ← storedtubes[i] computeReachtube(K i , p v , [0, T − τ i ])
8:
tubecache.storeTube(tube i )
9:
else if storedtubes[i].T > T then
10:
tube i ← storedtubes[i].truncate(T )
11:
restube v ← restube v ∪ tube i
12: K
v ← K v \ ∪ i storedtubes[i].K
13: tube = computeReachtube(K
v , p v , [0, T ])
14: tubecache.storeTube(tube )
15: restube v ← restube v ∪ tube
16: return: restube v
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:
1. When the time bound T i of the stored reachtube storedtubes[i] is less than T ,
we need to extend storedtubes[i] until time T by concatenating the original tube
with computeReachtube(K i , p v , [0, T − τ i ]), where (K i , [τ i , T i ]) is the last pair in
storedtubes[i]. The result is a valid (storedtubes[i].K, p v , [0, T ])-reachtube.
2. When the time bound T i of the stored reachtube storedtubes[i] is more than T , the
truncated reachtube is also a valid (storedtubes[i].K, p v , [0, T ])-reachtube.
3. For K
v that is not contained in the union of the initial sets in storedtubes, the function
computeReachtube will return a valid (K
v , p v , [0, T ])-reachtube.
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.
5.3 Bounded time safety
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)