The reconstruction of a mobile agent computation and its validation

We propose a new representation to describe mobile agents computations, where the underlying control structures are diffusing computations. Usually, distributed computations are abstracted as sets of receiving, sending and internal events. Instead of using this representation, we consider a diffusing computation as a set of leaves of a control tree associated to the different threads of control generated by the computation. We introduce so-called "Visit tags" to capture such a representation. These tags exhibit several nice properties, in particular, the whole computation tree can be reconstructed from the knowledge of tags labeling termination events. This tree is useful to assess global properties or evaluate state predicates, as well as to replay the computation. We present a formal development of the reconstruction algorithm as a sequence of refinement steps.