Experiments of *Developing a Model Checker for
Probabilistic Real-time Hierarchical Systems*

This webpage
is used to give more details of the experiments in *Developing a Model Checker for Probabilistic Real-time Hierarchical
Systems.* All the examples are available here.

We use our model checker PAT to fulfill these
experiments on a PC with 2 Intel Xeon CPUs at 2.13GHz and 32GB RAM, and in the
following are two kinds of examples we use in our paper.

·
Experiments compared with
PRISM model checker

This page is maintained by Songzheng Song.

Please contact with us if you have any
question about this webpage or these experiments. We will reply your enquiries
as soon as possible.

As we have
described in our paper, this motivating example is based on an interesting
phenomena: sometimes a user has requested a service in multi-lift system, but a
lift traveling in the same direction passes by that user and the user must wait
for another lift to serve him. This is actually because of the request
assignment algorithm in the system and some other unpredictable reasons such as
a lift could be occupied by other users for a long time.

Therefore,
we have modeled such lifts system in order to check the probability that this
phenomena could happen. To make it more reasonable, we use two assignment
algorithms, and the results in the following table tell us that assigning
users’ requests to the “nearest” lift is much better than to a random one. OOM
means out of memory.

System |
Result-R
(pmax) |
Time-R
(s) |
Result-N
(pmax) |
Time-N
(s) |

lift=2;
floor=2; user=2 |
0.21875 |
3.262 |
0.13889 |
2.385 |

lift=2;
floor=2; user=3 |
0.47656 |
38.785 |
0.34722 |
18.061 |

lift=2;
floor=2; user=4 |
0.6792 |
224.708 |
0.53781 |
78.484 |

lift=2;
floor=2; user=∞ |
0.81372 |
945.853 |
0.68403 |
223.036 |

lift=2;
floor=3; user=2 |
0.2551 |
12.172 |
0.18 |
6.757 |

lift=2;
floor=3; user=3 |
0.54009 |
364.588 |
0.427 |
119.810 |

lift=2;
floor=3; user=4 |
0.74396 |
11479.966 |
0.6335 |
1956.041 |

lift=2;
floor=4; user=2 |
0.27 |
27.888 |
0.19898 |
13.693 |

lift=3;
floor=2; user=2 |
0.22917 |
208.481 |
0.10938 |
88.549 |

lift=3;
floor=2; user=3 |
OOM |
OOM |
0.27344 |
3093.969 |

PRISM is widely used in probabilistic model
checking; therefore we pick some examples PRISM has and rebuild them in PAT.
Since PRISM does not support systems having both real-time and probability, we
choose its MDP examples in order to test the probability verification in PAT.

·
Mutual Exclusion (ME) model describes a probabilistic solution to
N-process mutual exclusion [1]

·
Randomized Consensus(RC) model describes the shared coin protocol of the
randomized consensus algorithm [2]

·
CSMA/CD (CS) is the IEEE 802.3 Carrier Sense, Multiple Access with
Collision Detection protocol

We check some
Linear Temporal Logic (LTL) properties in these models and record the time
every verification consumes.

System |
Property |
Result |
PAT(s) |
PRISM(s) |

ME (N=5) |
System
|= <>all_high && <>all_low with pmax |
1 |
9.031 |
7.413 |

ME (N=8) |
System
|= <>all_high && <>all_low with pmax |
1 |
185.051 |
149.448 |

RC (N=4,K=4) |
System
|= <>all_coins_equal_0 && <>all_coins_equal_1 with pmax |
0.99935 |
4.287 |
33.091 |

RC (N=6,K=6) |
System
|= <>all_coins_equal_0 && <>all_coins_equal_1 with pmax |
1 |
146.089 |
2311.388 |

CS (N=2, K=4) |
System
|= !collision_max_backoff U all_delivered
with pmax |
0.99902 |
9.362 |
1.014 |

CS (N=3, K=2) |
System
|= !collision_max_backoff U all_delivered
with pmax |
0.85962 |
212.712 |
7.628 |

The results of the experiments indicate
that PAT has comparable performance with PRISM. The main reason that PRISM overperforms PAT in several cases is that PRISM is
based on symbolic model checking-BDD, which can handle large number
of states in these examples. Meanwhile, PRISM has much longer history than PAT
so that many optimizations have been implemented in it. It is our future work
to optimize the probabilistic model checking in PAT.

1. Pnueli and L. Zuck. Verification
of Multiprocess Probabilistic Protocols. *Distributed
Computing*, 1(1), pages 53--72. 1986.

2. J. Aspnes and M. Herlihy.
On
Fast Randomized Consensus Using Shared Memory. *Journal of Algorithms ,*
15(1), pages 441--460. 1990