The following experiments are used to indicate what the performance that PAT
has in probabilistic model checking. The models we use include several
protocols:
model ME describes a probabilistic solution to N-process mutual exclusion
problem; model RC is a shared coin protocol of the randomized consensus
algorithm; Model DP is the probabilistic N-dining philosophers under fairness
and Model CS is the IEEE 802.3 CSMA/CD (Carrier Sense, Multiple Access with
Collision
Detection) protocol. Then we check the maximal probability(pmax) or minimal
probability(pmin) that the model could satisfy the desired properties and
compare the result with PRISM.
Table 1. Experiments on modeling
Table 2. Experiments on refinement checking

Table 3. Experiments on LTL checking
From Table 3, it is obvious that PAT has much good performance in probabilistic
model checking. Although the states and verification time increase quickly
when the parameter becomes larger and larger, PAT always has a comparable and
even better output compared with PRISM. Because our algorithm uses safety
recognition, the LTL which is safety or co-safety could be verified quite
fast. For example, in the RC(N=6, K=6) case, the co-safety(1) takes PAT 6s but
takes PRISM almost half an hour; and the co-safety(2) property cannot be
verified in PRISM within 10000 iteration but in PAT we could get the result in
several minutes. Even for liveness property, PAT could have a better
performance because our modeling language could guarantee smaller state space
in the same model compared with PRISM. However, PRISM could handle more states
per seconds, which could be indicated by the deadlock checking in the table,
so we are still improving our algorithm and data structure in this module, in
order to get better performance. The experiment data is available here.