Introduction

MMCsp 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. 

The 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.

Download/Build

The source code is free to download.

• To install MMCsp, please install XSB first. Then, unzip the source code and run "install.sh".
• 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.

Documentation

• 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]