Coordination by Timers for Channel-Based Anonymous Communications

In this paper we present a new model for timed coordination of communicating distributed processes. The proposed model is an extension of the π-calculus with locations, types, and timers. Types are used to express restricted access to distributed resources. Timers define timeouts for both communication channels and resources. We define the syntax of the model and its operational semantics and provide a few results regarding the typing system and the timers. A timed barbed bisimulation relation is defined to compare the processes. Coordination is given in two stages: by strategically assigning values to timers, and then by employing a set of additional coordination rules. The timed coordination aspects are given through a coordinator pair. It consists of a timers assigning function which can be changed dynamically, and a set of coordination rules. As an illustrating example, we relate our model with the channels of the Reo coordination model.