PostScript
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)
Abstract:
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 |
|
PostScript |
| Slides of G. Salaün's lecture IFM 2010: |
|