Translating Pi-Calculus into LOTOS NT

Radu Mateescu and Gwen Salaün

Proceedings of the 8th International Conference on Integrated Formal Methods IFM 2010 (Nancy, France)


Process calculi supporting mobile communication, such as the pi-calculus, are often seen as an evolution of classical value-passing 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 pi-calculus to LOTOS NT, a value-passing concurrent language with classical process algebra flavour. Our translation is succinct in the size of the pi-calculus specification and preserves the semantics of the language by ensuring a one-to-one 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 pi-calculus specifications using all the state-of-the-art simulation and verification functionalities provided by the CADP toolbox.

16 pages


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