[NPPW09]
Gethin Norman, Catuscia Palamidessi, David Parker and Peng Wu.
Model Checking Probabilistic and Stochastic Extensions of the PiCalculus.
IEEE Transactions on Software Engineering, 35(2), pages 209223, IEEE Computer Society.
March 2009.
[pdf]
[bib]
[Presents model checking techniques for the probabilistic/stochastic picalculus based on a translation to PRISM.]

Abstract.
We present an implementation of model checking for probabilistic and stochastic extensions of the
picalculus, a process algebra which supports modelling of concurrency and mobility. Formal verification
techniques for such extensions have clear applications in several domains, including mobile adhoc network
protocols, probabilistic security protocols and biological pathways. Despite this, no implementation of automated verification exists.
Building upon the picalculus model checker MMC, we first show an automated procedure for constructing
the underlying semantic model of a probabilistic or stochastic picalculus process.
This can then be verified using existing probabilistic model checkers such as PRISM. Secondly, we
demonstrate how for processes of a specific structure a more efficient, compositional approach is applicable,
which uses our extension of MMC on each parallel component of the system and then translates the results
into a highlevel modular description for the PRISM tool. The feasibility of our techniques is demonstrated
through a number of case studies from the picalculus literature.
