www.prismmodelchecker.org

Tandem Queueing Network

(Hermanns, Meyer-Kayser & Siegle)

Contents

Introduction

This case study is based on a simple tandem queueing network, taken from [HMKS99]. The model is represented as a CTMC which consists of a M/Cox2/1-queue sequentially composed with a M/M/1-queue. We use c to denote the capacity of the queues. The PRISM source code is given below.

// tandem queueing network [HKMKS99]
// gxn/dxp 25/01/00

ctmc

const int c; // queue capacity

const double lambda = 4*c;
const double mu1a = 0.1*2;
const double mu1b = 0.9*2;
const double mu2 = 2;
const double kappa = 4;

module serverC
	
	sc : [0..c];
	ph : [1..2];
	
	[] (sc<c) -> lambda: (sc'=sc+1); 
	[route] (sc>0) & (ph=1) -> mu1b: (sc'=sc-1);
	[] (sc>0) & (ph=1) -> mu1a: (ph'=2); 
	[route] (sc>0) & (ph=2) -> mu2: (ph'=1) & (sc'=sc-1);
	
endmodule  

module serverM
	
	sm : [0..c];
	
	[route]	(sm<c) -> 1: (sm'=sm+1);
	[] (sm>0) -> kappa: (sm'=sm-1);
	
endmodule

// reward - number of customers in network
rewards "customers"
	true : sc + sm;
endrewards
View: printable version          Download: tandem.sm

Model Statistics

The table below shows statistics for each model we have built. The first section gives information about the CTMC representing the model: the number of states and the number of non-zeros (transitions). The second part refers to the MTBDD which represents this CTMC: the total number of nodes, the number of leaves (terminal nodes), and the amount of memory needed to store it. The last column gives the amount of memory a sparse matrix would need to represent the same CTMC.

Kb:
c:   Model:   MTBDD:   Sparse:
States: NNZ: Nodes: Leaves: Kb:
5 66 189 10062.02.73
7 120 363 93 61.85.19
15 496 1,619 12362.422.8
31 2,016 6,819 15363.095.6
63 8,128 27,971 18363.6391
127 32,640 113,283 21364.21,582
255 130,816 455,939 24364.76,365
511 523,776 1,829,379 27365.325,530
1,0232,096,128 7,328,771 30365.9102,260
2,0478,386,560 29,337,603 33366.5409,320
4,09533,550,336117,395,45936367.11,637,840

Model Construction Times

The table below gives the times taken to construct the models. This process involves first building a CTMC (represented as an MTBDD) from the system description (in our module based language), and then computing the reachable states using a BDD based fixpoint algorithm. The total time required and the number of fixpoint iterations are given below.

c:   Construction:
Time (s): Iter.s:
5 0.03417
7 0.03523
15 0.04047
31 0.05895
63 0.128191
127 0.374383
255 1.409767
511 5.5651,535
1,02322.703,071
2,04799.646,143
4,095763.612,287

Model Checking

We now report on the model checking results obtained using PRISM when verifying the following CSL properties.

const double T;

// long run expected customers in the network
R=?[S]

// probability network becomes full in T time units
P=? [ true U<=T sc=c & sm=c & ph=2 ]

// probability first queue becomes full in T time units
P=? [ true U<=T sc=c ]

// the minimimum probability of leaving a situation where the second queue is entirely populated within T time units
P=? [ sm=c U<=T sm<c {sm=c}{min} ]

// expected number of customers in the network
R=?[I=T]
View: printable version          Download: tandem.csl

All experiments were carried out on a 2.80GHz PC with 1 Gb memory running Linux and in all iterative methods we stop iterating when the relative error between subsequent iteration vectors is less than 1e-6, that is:

relative error equation
  • Computing Steady State Probabilities: The table below gives the model checking statistics when computing these probabilities for both the Jacobi and Gauss-Seidel methods when using PRISM's different engines.

    c:   Jacobi: Gauss Seidel:
    Iters: Time per iter: (s)   Iters: Time per iter: (s)
    MTBDD Sparse Hybrid Sparse Hybrid
    5 189 0.001180< 0.00001< 0.0000134 < 0.00001< 0.00001
    7 207 0.001791< 0.000010.000010 54 < 0.000010.000037
    15 298 0.0068270.000013 0.000020 119 0.000034 0.000034
    31 555 0.0128060.000052 0.000074 218 0.000087 0.000188
    63 1,056 0.0517350.000227 0.000361 413 0.000363 0.000695
    127 2,093 0.1545520.003065 0.005955 816 0.004366 0.008109
    255 4,212 0.2246090.032259 0.041037 1,639 0.035350 0.045198
    511 8,498 0.6507460.166898 0.205874 3,303 0.176115 0.198061
    1,02316,3261.0925330.704615 0.789749 6,335 0.763633 0.817350
    2,04724,1411.9398702.877855 3.173416 9,394 3.085141 3.220208
    4,09537,931- - 13.14700 15,189- 14.38306

    In the graph below we have plotted the results we checking the expected number of customers in the network in the long run.

    plot: expected number of customers in the long run
  • The probability that, from the initial state, the tandem network becomes fully occupied within T time units. The table and graph below presents the statistics and results when verifying this property.

    c:   T=2:
    Iters: Time per iter: (s)
    MTBDD Sparse Hybrid
    5 225 0.001120< 0.00001< 0.00001
    7 241 0.0017800.000000 0.000008
    15 306 0.0089870.000016 0.000033
    31 437 0.0226590.000080 0.000135
    63 723 0.0425530.000372 0.000564
    127 1,325 0.0946580.002080 0.002654
    255 2,483 0.2560950.014267 0.027096
    511 4,733 0.7861300.045681 0.081702
    1,0239,137 2.5648980.119471 0.254866
    2,04717,8149.0979870.433326 0.899096
    4,09534,980- - 3.485094

    plot: probability that, from the initial state, the tandem network becomes fully occupied within T time units
  • The probability that, from the initial state, the first station of the tandem network becomes fully occupied within T time units. The table and graph below presents the statistics and results when verifying this property.

    c:   T=0.5:
    Iters: Time per iter: (s)
    MTBDD Sparse Hybrid
    5 30 0.000900< 0.00001< 0.00001
    7 30 0.001433< 0.00001< 0.00001
    15 35 0.0047430.000057 0.000057
    31 50 0.0086600.000260 0.000280
    63 82 0.0119880.001354 0.001476
    127 148 0.0171350.006176 0.006743
    255 281 0.0212810.027103 0.029299
    511 545 0.0335060.111947 0.123903
    1,0231,0730.0443200.410707 0.488582
    2,0472,1250.1123011.647587 1.972453
    4,0954,2250.149460- 8.087538

    plot: probability that, from the inital state, the first station of the tandem network becomes fully occupied within T time units
  • The minimum probability of leaving a situation where the second queue is fully occupied within T time units. The table and graph below presents the statistics and results when verifying this property.

    c:   T=0.5:
    Iters: Time per iter: (s)
    MTBDD Sparse Hybrid
    5 69 0.000058< 0.00001< 0.00001
    7 92 0.000098< 0.00001< 0.00001
    15 176 0.0001250.000011 < 0.00001
    31 237 0.0001390.000025 0.000030
    63 302 0.0001720.000086 0.000086
    127 433 0.0002190.000621 0.000672
    255 718 0.0002520.002249 0.002592
    511 1,3200.0003090.010255 0.009667
    1,0232,4790.0003360.025934 0.041160
    2,0474,7280.0003550.098713 0.160120
    4,0959,1330.0003840.371677 0.626650

    plot: minimum probability of leaving a situation where the second queue is fully occupied within T time units
  • The expected number of customers in the network at time T. The table and graph below presents the statistics and results when verifying this property.

    c:   T=1:
    Iters: Time per iter: (s)
    MTBDD Sparse Hybrid
    5 198 0.001131< 0.00001< 0.00001
    7 206 0.0018010.000000 0.000010
    15 239 0.0069710.000017 0.000033
    31 304 0.0331020.000066 0.000109
    63 435 0.0759930.000260 0.000444
    127 720 0.7276250.001549 0.002162
    255 1,3231.2126860.006620 0.009642
    511 2,48120.348830.026343 0.040297
    1,0231,063- 0.067043 0.149812
    2,0472,111- 0.267248 0.605698

    plot: expected number of customers in the network at time T

Case Studies