Types and Capabilities for Mobile Agents

Matthew Hennessy

(University of Sussex)

A language called Dpi is presented for describing ``mobile agents''. Both the syntax and reduction semantics is based on that of the picalculus in that communication is channel based, and these may be created dynamically and shared privately among agents. However in Dpi channels reside at explicit locations or sites and communication is local to sites. Moreover agents can migrate between sites to effect computations.

We describe a typing system for Dpi based on the novel notion of a location type. This associates with each location a set of capabilities, i.e. a set of permissions to perform certain behaviour. These capabilities include the ability to send or receive values, of specified types, on named channels.

We prove a Subject Reduction theorem and a Type Safety theorem. The latter is expressed formally in terms of the knowledge of an agent; well-typed agents can only perform actions which are consistent with their knowledge of their environment.
Tuesday 5th May 1998, 14:30
Seminar Room 322
Department of Computer Science