Probabilistic Model Checking of the CSMA/CD protocol using PRISM and APMC
Sat 4 Sep 2004 12:23 BST
This talk focussed on the first experimental validation of the APMC tool. The tool was used to compute results that were then compared with results computed by PRISM.
The summary was: PRISM and APMC are complementary tools; one might use APMC to gain a feel for the solution spaces, then switch to the slower PRISM for a precise calculation, switching back to APMC when the model grows to a size intractable to PRISM’s engine. APMC is faster than PRISM, although it does only give an approximate result.

PRISM models nondeterminism on average systems  state space explosion when the model grows

APMC models large systems deterministically  can only handle fully probabilistic systems (?)

This is the first real use of APMC  it is very new, developed in 2003.

it’s a distributed model checker! They used >80 workstations

similar kinds of questions to those that can be asked of prism

notions of confidence  error intervals in the answers it gives you! Statistical answers  cool!

they built a model with apmc and it has more than 10^{100} states! (try doing that in prism).

the results were good  apmc lined up with prism

I noticed that the error bars were all the same in the result graphs, so I asked a question at the end  the answer was that apmc has as an engine parameter to control the size of the required confidence interval, and that the algorithm is quadratic in the required error bound (which I’m unsure what that means exactly but the general idea is clear).