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.

 

·         Multi Lifts Experiments

·         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.

 


 

Multi Lifts Experiments

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

 


 

Experiments compared with PRISM model checker

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.


 

References

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