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

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

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 

Randomized Consensus(RC) model describes the shared coin protocol of the randomized consensus algorithm 

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