Translating PiCalculus into LOTOS NT
Radu Mateescu and Gwen Salaün
Proceedings of the 8th International Conference on Integrated Formal Methods
IFM 2010 (Nancy, France)
Abstract:
Process calculi supporting mobile communication, such as the picalculus, are often seen as an evolution of classical valuepassing calculi, in which communication between processes takes place along a fixed network of static channels. In this paper, we attempt to bring these calculi closer by proposing a translation from the finite control fragment of the picalculus to LOTOS NT, a valuepassing concurrent language with classical process algebra flavour. Our translation is succinct in the size of the picalculus specification and preserves the semantics of the language by ensuring a onetoone correspondence between the states and transitions of the labeled transition systems corresponding to the input calculus and the output LOTOS NT specifications. We automated this translation by means of the Pic2Lnt tool, which makes it possible to analyze picalculus specifications using all the stateoftheart simulation and verification functionalities provided by the CADP toolbox.
16 pages 

PostScript 
Slides of G. Salaün's lecture IFM 2010: 
