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.