On the expressiveness of internal mobility in name-passing calculi

We consider pi I, a fragment of the pi-calculus where only exchange of private names among processes is permitted (internal mobility). The calculus pi I enjoys a simpler mathematical treatment, very close to that of CCS. In particular, pi I avoids the concept of substitution. We provide an encoding from the asynchronous pi-calculus to pi I and then prove that two processes are barbed-equivalent in pi-calculus if and only if their translations in pi I cannot be distinguished, under barbed bisimilarity, by any translated static context. The result shows that, in name-passing calculi, internal mobility is the essential ingredient as far as expressiveness is concerned. (C) 1998-Elsevier Science B.V. All rights reserved.