Operational semantics of ambient calculus

Mobile ambients is a process calculus for modeling mobile agents in wide area networks. It has important theoretical and practical values in studying concurrent and mobile computation as well as the security of interactive systems. In this paper a frame structure is given for mobile ambients. First we introduce the concept of ambient calculus frame. Then we propose a construction method for translating an ambient definition into the frame definition, a transformation function is given based on the method. Next the movement and interaction of the code are discussed based on the frame structure. Finally an operating semantics is developed basing on the frame structure, an example of a frame and its execution are given. Introducing frame structure for ambient calculus is an attempt to provide languages support for asynchronous, distributed, and mobile programming. The ideas and methods in this paper can also be applied to other calculi with concurrency and mobility.