Excommunication: Transforming Calculus Specifications to Remove Internal Communication

In this paper, we present a new automatic transformation algorithm called excommunication that transforms \$\$\backslashpi \$\$π-calculus processes to remove parallelism, and hence internal communication. We prove that the transformation is correct and that it always terminates for any specification in which the named processes are in a particular syntactic form we call serial form. We argue that this transformation facilitates the proving of properties of mobile processes, and demonstrate this by showing how it can be used to simplify a leakage analysis.