کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
426233 | 686016 | 2009 | 23 صفحه PDF | دانلود رایگان |
Dπ is a simple distributed extension of the π-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 major modifications to the 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.
Journal: Information and Computation - Volume 207, Issue 2, February 2009, Pages 171-193