Skip to Main content Skip to Navigation
Conference papers

Translating Pi-Calculus into LOTOS NT

Abstract : Process calculi supporting mobile communication, such as the π-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 π-calculus to Lotos NT, a value-passing concurrent language with classical process algebra flavour. Our translation is succinct in the size of the π-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 π-calculus specifications using all the state-of-the-art simulation and verification functionalities provided by the Cadp toolbox.
Complete list of metadata

Cited literature [31 references]  Display  Hide  Download
Contributor : Ist Inria Nancy Grand Est Connect in order to contact the contributor
Submitted on : Friday, October 8, 2010 - 11:23:49 AM
Last modification on : Sunday, June 26, 2022 - 9:33:35 AM
Long-term archiving on: : Monday, January 10, 2011 - 11:42:43 AM


Files produced by the author(s)


  • HAL Id : inria-00524586, version 1



Radu Mateescu, Gwen Salaün. Translating Pi-Calculus into LOTOS NT. Integrated Formal Methods - IFM 2010, INRIA Nancy Grand Est, Oct 2010, Nancy, France. pp.229-244. ⟨inria-00524586⟩



Record views


Files downloads