Information Technology Reference
In-Depth Information
t
(s)
Reachability + Hoeffding
Reachability + SPRT
Termination
Gauss-Seidel
Jacobi
10
6
10
5
10
4
10
3
10
2
10
1
10
2
10
4
10
6
10
8
10
10
10
12
|
S
|
Fig. 3.
Verification time as a function of state-space size for modified polling system
5.2
Tandem Queuing Network
The second model is a tandem queuing network due to Hermanns et al. [14]. The
network consists of two serially connected queues, each with capacity
n
. Messages
arrive at the first queue, get routed to the second queue, and eventually leave
the system from the second queue. The inter-arrival time for messages at the
first queue is exponentially distributed with rate
λ
=4
n
. The processing time
at the second queue is exponentially distributed with rate
κ
=4.Thesizeofthe
state space for this model is
O
(
n
2
).
We verify that the probability is at most 0.03 that the second queue becomes
full before the first queue:
full
2
]. We use the same experimental
setup as for the first model, except for the choice of
p
T
. Instead of a fixed value,
we use
p
T
=
P
≤
0
.
03
[
¬
full
1
U
1
n
+2
for a model with queues of size
n
.Wedosobecausethe
subdominant eigenvalue for this model more quickly approaches 1 as
n
grows.
Figure 4 plots the verification time as a function of state-space size for the
t
(s)
10
5
Reachability + Hoeffding
Reachability + SPRT
Termination
Gauss-Seidel
Jacobi
10
3
10
1
10
−1
10
−3
10
1
10
3
10
5
10
7
10
9
|
S
|
Fig. 4.
Verification time as a function of state-space size for tandem queuing network
Search WWH ::
Custom Search