Encoding Mobile Ambients into the π-Calculus

摘要

We present an encoding of the mobile ambients without communication into a subset of the π-calculus, namely the localized sum-free synchronous π-calculus. We prove the operational correspondence between the two formalisms. A key idea of the encoding is the separation of the spatial structure of mobile ambients from their operational semantics. The operational semantics is given by a universal π-process Ruler which communicates with a π-calculus term Structure a simulating the spatial structure of a mobile ambient A by means of channels. We consider the presented encoding as a first step toward designing a fully abstract translation of the calculus of mobile ambients into the π-calculus and thus developing a uniform framework for the theory of mobile computations.