[NPPW07]
Gethin Norman, Catuscia Palamidessi, David Parker and Peng Wu.
Model Checking the Probabilistic Picalculus.
In Proc. 4th International Conference on Quantitative Evaluation of Systems (QEST'07), pages 169178, IEEE CS Press.
September 2007.
[ps.gz]
[pdf]
[bib]
[Presents model checking techniques for the probabilistic picalculus based on a translation to PRISM.]

Notes:
Further details are included in the technical report version of this paper [NPPW07b].

Abstract.
We present an implementation of model checking for the probabilistic picalculus, a process algebra which supports modelling of concurrency, mobility and discrete probabilistic behaviour.
Formal verification techniques for this calculus have clear applications in several domains, including mobile adhoc network protocols and random security protocols. Despite this, no implementation of automated verification exists. Building upon the (nonprobabilistic) picalculus model checker MMC, we first show an automated procedure for constructing the Markov decision process
representing a probabilistic picalculus process. This can then be verified using existing probabilistic model checkers such as PRISM.
Secondly, we demonstrate how for a large class of systems a more efficient, compositional approach can be applied, which uses our extension of MMC on each parallel component of the system and then translates the results into a highlevel model description for the PRISM tool. The feasibility of our techniques is demonstrated through three case studies from the picalculus literature.
