www.prismmodelchecker.org

Cyclic Server Polling System

(Ibe and Trivedi)

Contents

Introduction:

This case study is based on a cyclic server polling system, taken from [IT90]. The model is represented as a CTMC. We use N to denote the number of stations handled by the polling server. By way of example, the PRISM source code for the case where N=5 is given below.

// polling example [IT90]
// gxn/dxp 26/01/00

ctmc

const int N=5;

const double mu= 1;
const double gamma= 200;
const double lambda= mu/N;

module server

	s : [1..5]; // station
	a : [0..1]; // action: 0=polling, 1=serving
	
	[loop1a] (s=1)&(a=0) -> gamma	: (s'=s+1);
	[loop1b] (s=1)&(a=0) -> gamma	: (a'=1);
	[serve1] (s=1)&(a=1) -> mu	: (s'=s+1)&(a'=0);
	
	[loop2a] (s=2)&(a=0) -> gamma	: (s'=s+1);
	[loop2b] (s=2)&(a=0) -> gamma	: (a'=1);
	[serve2] (s=2)&(a=1) -> mu	: (s'=s+1)&(a'=0);
	
	[loop3a] (s=3)&(a=0) -> gamma	: (s'=s+1);
	[loop3b] (s=3)&(a=0) -> gamma	: (a'=1);
	[serve3] (s=3)&(a=1) -> mu	: (s'=s+1)&(a'=0);
	
	[loop4a] (s=4)&(a=0) -> gamma	: (s'=s+1);
	[loop4b] (s=4)&(a=0) -> gamma	: (a'=1);
	[serve4] (s=4)&(a=1) -> mu	: (s'=s+1)&(a'=0);
	
	[loop5a] (s=5)&(a=0) -> gamma	: (s'=1);
	[loop5b] (s=5)&(a=0) -> gamma	: (a'=1);
	[serve5] (s=5)&(a=1) -> mu	: (s'=1)&(a'=0);
	
endmodule

module station1

	s1 : [0..1];
	
	[loop1a] (s1=0) -> 1 : (s1'=0);
	[]       (s1=0) -> lambda : (s1'=1);
	[loop1b] (s1=1) -> 1 : (s1'=1);
	[serve1] (s1=1) -> 1 : (s1'=0);
	
endmodule

// construct further stations through renaming
module station2 = station1 [s1=s2, loop1a=loop2a, loop1b=loop2b, serve1=serve2] endmodule
module station3 = station1 [s1=s3, loop1a=loop3a, loop1b=loop3b, serve1=serve3] endmodule
module station4 = station1 [s1=s4, loop1a=loop4a, loop1b=loop4b, serve1=serve4] endmodule
module station5 = station1 [s1=s5, loop1a=loop5a, loop1b=loop5b, serve1=serve5] endmodule

// cumulative rewards

rewards "waiting" // expected time the station 1 is waiting to be served
	s1=1 & !(s=1 & a=1) : 1;
endrewards

rewards "served" // expected number of times station1 is served
	[serve1] true : 1;
endrewards
View: printable version          Download: polling5.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.

N:   Model:   MTBDD:   Sparse:
States: NNZ: Nodes: Leaves: Kb: Kb:
4 96 272 178 43.484.3
5 240 800 271 45.2912.2
6 576 2,208 367 47.1732.6
7 1,344 5,824 482 414.984
8 3,072 14,848 608 411.9210
9 6,912 36,864 765 414.9513
1015,360 89,600 921 418.01,230
1133,792 214,016 1,096421.42,904
1273,728 503,808 1,282425.06,768
13159,744 1,171,456 1,491433.315,600
14344,064 2,695,168 1,707433.335,616
15737,280 6,144,000 1,942437.980,640
161,572,864 13,893,632 2,188442.7371,712
173,342,336 31,195,136 2,469448.2378,624
187,077,888 69,599,232 2,745453.6843,264
1914,942,208154,402,8163,040459.41,867,776
2031,457,280340,787,2003,346465.44,116,362

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.

N:   Construction:
Time (s): Iter.s:
4 0.0399
5 0.04311
6 0.05913
7 0.06315
8 0.06917
9 0.09 19
100.10721
110.11523
120.12625
130.14427
140.15629
150.19 31
160.20233
170.23935
180.27137
190.30239
200.34641

Model Checking

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

// time bound
const double T;

//Probability that in the long run station 1 is awaiting service 
S=? [ s1=1 & !(s=1 & a=1) ]

// Probability that in the long run station 1 is idle 
S=? [ s1=0 ] 

// once a station becomes full, the minimum probability it will eventually be polled is ...
P=? [ true U (s=1 & a=0) {s1=1}{min} ]

// probability that from the inital state station 1 is served before station 2 is ...
P=? [ !(s=2 & a=1) U (s=1 & a=1) ]

// once a station becomes full, probability it will be polled within T time units is ...
P=?[ true U<=T (s=1 & a=0) ]

// expected reward accumlated by time T
R{"waiting"}=?[C<=T] // time the station 1 is waiting to be served
R{"served"}=?[C<=T] // number of times station1 is served
View: printable version          Download: polling.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.

    N:   Jacobi: Gauss Seidel:
    Iters: Time per iter: (s)   Iters: Time per iter: (s)
    MTBDD Sparse Hybrid Sparse Hybrid
    4 1300.001100< 0.000010.00001518< 0.00001< 0.00001
    5 1730.0029310.000012 0.00001220< 0.00001< 0.00001
    6 2180.0074450.000014 0.00002822< 0.00001< 0.00001
    7 2640.0205720.000042 0.000068230.000087 0.000087
    8 3100.0591780.000100 0.000158250.000160 0.000320
    9 3580.2567040.000257 0.000377260.000462 0.000692
    10406- 0.000643 0.000958270.001037 0.001667
    11455- 0.001545 0.002455280.002393 0.003893
    12505- 0.003612 0.006646290.005207 0.009069
    13555- 0.008295 0.015944300.011733 0.020300
    14606- 0.019363 0.035465310.026161 0.045065
    15657- 0.044633 0.080626320.058656 0.104188
    16709- 0.106413 0.191898330.130212 0.231152
    17761- 0.235858 0.409599340.288147 0.537794
    18814- 0.567683 0.908693340.643882 1.187500
    19866- 1.325487 2.003745351.462714 2.633857
    20920- - 4.66472436- 5.759333
  • Probability that in the long run station 1 is awaiting service:

    plots probability that in the long run station 1 is awaiting service
  • Probability that in the long run station 1 is idle:

    plots probability that in the long run station 1 is idle
  • Once station 1 becomes full, the minimum probability it will eventually be polled: the table below presents statistics for the model checking process. Note that as this property holds with probability 1 the statistics correspond to a BDD precomputation algorithm.

    N: Iters: Time per iter: (s) Minimum probability:
    4 18<0.0000011
    5 22<0.0000011
    6 26 0.0003851
    7 30 0.0003331
    8 34 0.0002941
    9 38 0.0005261
    1042 0.0007141
    1146 0.0008701
    1250 0.0008001
    1354 0.0011111
    1458 0.0012071
    1562 0.0012901
    1666 0.0015151
    1770 0.0017141
    1874 0.0017571
    1978 0.0020731
    2082 0.0023081
  • The probability that, from the initial state, station 1 is polled before station 2: the table and below gives the model checking statistics when computing these probabilities for both the Jacobi and Gauss-Seidel methods when using PRISM's different engines.

    N:   Jacobi: Gauss Seidel:
    Iters: Time per iter: (s)   Iters: Time per iter: (s)
    MTBDD Sparse Hybrid Sparse Hybrid
    4 2,4800.0004630.0000020.0000021,8620.0000090.000011
    5 2,6640.0008480.0000050.0000062,2850.0000210.000024
    6 2,9650.0020410.0000130.0000162,4790.0000440.000045
    7 3,1240.0052060.0000300.0000412,8090.0000950.000102
    8 3,3740.0132860.0000760.0001012,9650.0002090.000233
    9 3,5160.0339810.0001800.0002323,2390.0004550.000516
    103,7320.0824600.0004570.0005603,3740.0009930.000956
    113,8630.1936700.0010760.0015103,6120.0022200.002256
    124,0540.4500050.0023930.0043573,7340.0048090.005239
    134,1761.0474510.0054840.0097193,9450.0103810.009450
    144,351- 0.0129990.0223784,0580.0230120.021251
    154,464- 0.0279700.0498144,2490.0491100.047892
    164,623- 0.0660750.1114544,3540.1068760.106191
    174,732- 0.1449110.2474694,5290.2338340.243856
    184,880- 0.3324250.5547294,6290.5399820.535855
    194,983- 0.7694291.2261364,7911.2620001.185987
    205,122- - 2.6664184,886- 2.657864

    The graph below we have plotted these probabilities as the number of stations varies.

    plot: probability that station 1 is served before station 2
  • The minimum probability that once station 1 is full it is polled within T time units: the table below presents statistics for the model checking process.

    N:   T=5: T=50:
    Iters: Time per iter: (s)   Iters: Time per iter: (s)
    MTBDD Sparse Hybrid MTBDD Sparse Hybrid
    4 1,2990.0001080.0000020.0000043,0290.0000970.0000020.000004
    5 1,2990.0003600.0000080.0000123,3900.0003250.0000060.000012
    6 1,2990.0008330.0000170.0000333,7350.0006380.0000160.000032
    7 1,2990.0015250.0000440.0000894,0680.0012760.0000400.000087
    8 1,2990.0029050.0001050.0002264,3930.0025990.0001000.000220
    9 1,2990.0059070.0002590.0005574,7090.0056400.0002450.000545
    101,2990.0131200.0006690.0014005,0190.0128210.0006120.001356
    111,2990.0312020.0015770.0035405,3240.0303400.0014830.003444
    121,2990.0730510.0036770.0090745,6250.0696250.0033990.008809
    131,2990.1752530.0084470.0211345,9210.1516770.0077900.020601
    141,2990.4474430.0195340.0488916,2130.3508960.0180840.049279
    151,2991.3329770.0451690.1117826,5030.8824480.0419780.109156
    161,2994.8235040.1091590.2556576,7892.4532820.1016690.249149
    171,299- 0.2362490.5746577,073- 0.2205430.559372
    181,299- 0.5720481.2885137,355- 0.5387521.253214
    191,299- 1.3768632.8535217,634- 1.2488192.778883
    201,299- - 6.3110277,911- - 6.146424

    In the graph below, we plot results of the above property for different numbers of stations (values of N):

    plot: minimum probability that once station 1 is full it is polled within T time units

  • Expected time station 1 spends awaiting service by time T: the table and graph below we present the model checking statistics as both the number of stations and time bound T varies.

    N:   T=5: T=50:
    Iters: Time per iter: (s)   Iters: Time per iter: (s)
    MTBDD Sparse Hybrid MTBDD Sparse Hybrid
    4 1,2990.0002700.0000030.0000063,856 0.0002660.0000040.000006
    5 1,2990.0006530.0000080.0000174,766 0.0006560.0000090.000017
    6 1,2990.0015320.0000220.0000405,677 0.0015340.0000250.000044
    7 1,2990.0038570.0000590.0001076,585 0.0038280.0000630.000112
    8 1,2990.0104980.0001420.0002667,489 0.0106050.0001500.000276
    9 1,2990.0277690.0003420.0006498,391 0.0285000.0003610.000676
    101,2990.0707940.0008410.0016019,290 0.0754880.0008650.001653
    111,2990.1753070.0019480.00403810,1870.2070290.0020150.004120
    121,2990.4736110.0044700.01004611,0820.9512480.0096200.010143
    131,2991.2646130.0102420.02328911,1113.6424360.0102850.023461
    141,299- 0.0232900.05309411,111- 0.0234220.053808
    151,299- 0.0527930.12083911,112- 0.0533460.121939
    161,299- 0.1240150.27363611,112- 0.1261520.276256
    171,299- 0.2699860.61194911,112- 0.2740050.616791
    181,299- 0.6397471.40010511,112- 0.6504631.371019
    191,299- - 3.01676811,112- - 3.030094
    201,299- - 6.62951511,112- - 6.676664

    plots expected time station 1 spends awaiting service by time T
  • Expected number of times station 1 is served by time T:

    plots expected number of times station 1 is served by time T

Case Studies