eighty-twenty

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¹⁰⁰ 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).