Abstract

(Joint work with Andy Gordon, Microsoft Research)

The ambient calculus is a process calculus based on mobility instead of communication, where processes reside at the nodes of a dynamic hierarchy of locations. It becomes natural to discuss properties that hold at particular locations, and to discuss the dynamic evolution of the hierarchy of locations. We use a logic as a way of formalizing such discussions.

We describe a modal logic for the ambient calculus, whose main novelty is the introduction of spatial connectives (in addition to standard and temporal connectives). We obtain a logic where formulas denote sets of processes closed under structural congruence; we discuss some connections with linear, relevant, and bunched logics.

Our logic can be used for specifying mobility protocols, for expressing mobility policies, and as a playground for model checking of mobile computation, with potential applications to bytecode verification of mobile code. Mobility properties of varying degrees of difficultly can be established by proof search, by model checking, or by typechecking.