Mobility control via passports

Samuel Hym (1, 2)

1 PPS - Preuves, Programmes et Systèmes
2 LIFL - Laboratoire d'Informatique Fondamentale de Lille

Dpi is a simple distributed extension of the pi-calculus in which agents are explicitly located, and may use an explicit migration construct to move between locations. In this paper we introduce passports to control those migrations; in order to gain access to a location agents are now expected to show some credentials, granted by the destination location. Passports are tied to specific locations, from which migration is permitted. We describe a type system for these passports, which includes a novel use of dependent types, and prove that well-typing enforces the desired behaviour in migrating processes. Passports allow locations to control incoming processes. This induces a major modification to the possible observations which can be made of agent-based systems. Using the type system we describe these observations, and use them to build a loyal notion of observational equivalence for this setting. Finally we provide a complete proof technique in the form of a bisimilarity for establishing equivalences between systems.

Mots clés: control of agent migrations; distributed computation; process calculus; typed observational equivalence

Domaines: Langage de programmation [cs.PL]; Calcul parallèle, distribué et partagé [cs.DC]

Samuel Hym. Mobility control via passports. Information and Computation, 2009, 207 (2), pp.171-193. ⟨10.1016/j.ic.2007.11.011⟩. ⟨hal-00140527⟩