A Distributed Computational Model for Mobile Agents

In this paper, a novel formalized mobile agent distributed computation model based on transition systems is presented. In our model, the mobile agent actions (e.g. computations, communication and migration) are described using transitions. Thus, a mobile agent algorithm is viewed as a transition system and the underlying distributed system is modeled by a connected graph. We exploit the high-level encoding of agent actions by transitions to prove the correctness of agent algorithms. We illustrate this approach with the distributed computation of a spanning tree.