Mobile agents, i.e. pieces of programs that can be sent around networks of computers, are starting to appear on the Internet. Such programs may be seen as an enrichment of traditional distributed computing. Since mobile agents may carry communication links with them as they move across the network, they create very dynamic interconnection structures that can be extremely complex to analyse. In this paper we apply a non-interleaving semantics to analyse a system based on the mobile agent principle written in the Facile programming language. This example is a scaled down version of a system demonstrated at the European IT Conference Exhibition in Brussels, 1995.
This paper further develops a non-interleaving semantics for Facile, first presented in [4]. We develop a Structural Operational Semantics (SOS) for Facile, giving a proved transition system that records encodings of the derivation trees of transitions in their labels. This information allows us to easily recover non-interleaving semantics for Facile by looking only at the labels of transitions. This semantics may be instantiated to recover both causality and locality information.