David Parker
Reader, Computer Science, University of Birmingham
[NPPW07] Gethin Norman, Catuscia Palamidessi, David Parker and Peng Wu. Model Checking the Probabilistic Pi-calculus. In Proc. 4th International Conference on Quantitative Evaluation of Systems (QEST'07), pages 169-178, IEEE CS Press. September 2007. [ps.gz] [pdf] [bib] [Presents model checking techniques for the probabilistic pi-calculus based on a translation to PRISM.]
Downloads:  ps.gz ps.gz (119 KB)  pdf pdf (231 KB)  bib bib
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 pi-calculus, 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 ad-hoc network protocols and random security protocols. Despite this, no implementation of automated verification exists. Building upon the (non-probabilistic) pi-calculus model checker MMC, we first show an automated procedure for constructing the Markov decision process representing a probabilistic pi-calculus 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 high-level model description for the PRISM tool. The feasibility of our techniques is demonstrated through three case studies from the pi-calculus literature.