Proving distributed algorithms for mobile agents: Examples of spanning tree computation in dynamic networks

In a dynamic network topological events can occur at any time, and no stable periods can be assumed. To make designing distributed algorithms easier, we model these latter with a local computation model. The implementation of a local computation model using message passing communication model has given rise to various problems. Among these we can mention the use of a great amount of communication and computation resources. In order to solve these problems, we propose another implementation of rewriting systems using mobile agents. We present then, using local computations, a framework for describing distributed algorithms for mobile agents in a dynamic network. We make use of the high level encoding of these algorithms as transition rules. The main advantage of this uniform and formal approach is the proof correctness of distributed algorithms. We illustrate this approach by giving an example of distributed computation of a hierarchical spanning tree by mobile agents in a dynamic network.