A Denotational Semantic Description for Safe Ambient Calculus

Since computation under network involves variants, complicated information and behaviors, it is difficult to give denotational semantic description for computing under network. As a kind of network computing model, Ambient calculus contributes to modeling mobility and distributed features of network computing. Researches on its semantics description are mostly based on reduction rules. These descriptions are brief, but based on them it is indeterminable and has disadvantage in system design and direct implementation. On the other hand, these works mostly focus on describing variants behaviors of Ambient calculus in one level, which makes it complicated to understand clearly how these variants behaviors work and how they work together. As a result, based on the unit ambient of Ambient calculus, a three-level semantics description framework is given for Ambient calculus. The three levels are: internal level of ambient, ambient level, and system level. For each of these three levels, the syntax and semantics of its behaviors is defined in detail, and the transformation relation functions between each two levels are given. In order to specify how the framework works, a practical example is given based on this framework in three levels. Finally, proof is shown to prove the correctness of this semantic framework. This layered semantics description may help users analyze behaviors of computing in Ambient calculus and understand the implementation of ambient practical systems.