is a compiler from a simple probabilistic pi-calculus to PRISM models. It is built on XSB, a tabled logic programming system, and generates the symbolic semantic representation of a probabilistic pi-calculus term in text. A separate Java program then translates this semantic representation into a probabilistic model for PRISM.MMCspThe tool was developed under the collaboration between teams Comete (Laboratoire d'Informatique de l'Ecole Polytechnique, LIX) and PRISM (Oxford University Computing Laboratory) under an INRIA/ARC Project ProNobis.

The source code is free to download.

Examples:

Dining Cryptographers Problem (under directories "Examples\probdcp2" and "Examples\probdcp3") Partial Secret Exchange algorithm (under directory "Examples\pse") To run these examples, type "make" under each of the above directories.

- Gethin Norman, Catuscia Palamidessi, David Parker and Peng Wu. Model Checking Probabilistic and Stochastic Extensions of the Pi-calculus. IEEE Transactions on Software Engineering, 2009, 35(2): 209 - 223 [full-text] A preminary version of this paper was presented at the 4th International Conference on the Quantitative Evaluation of SysTems (QEST 2007) [full-text]
- Gethin Norman, Catuscia Palamidessi, David Parker and Peng Wu. Translating the Probabilistic pi-Calculus to PRISM. Technical Report CSR-07-02, School of Computer Science, University of Birmingham. March 2007 [full-text]