An Equivalence Relation for Typed Ambient Calculus

摘要

Ambient calculus is a process algebra designed for describing mobile processes. The calculus has nesting construction of ambients that enables us to describe not only mobile processes but also the networks in which the processes move around. When we describe a network with ambients, however, malicious processes can destroy nodes of the network or alter the construction of the network. Thus, a type system was introduced to ambient calculus so that we can give each node a desirable character that prevent malicious processes from cracking the network. The designers of the calculus defined an equational relation for untyped ambient calculus. Our previous work pointed out there exist identified processes up to the relation that have different properties, and it refined the relation so that we can discriminate those processes. This paper shows the original and our former relations are no longer available for typed ambient calculus and it presents another rela-tion that is available for typed ambient calculus.