Andy Gordon - Anytime, Anywhere: Modal Logics for Mobile Ambients

We describe a modal logic for mobile processes, based on the ambient calculus. The ambient calculus provides distinct locations where processes may reside. As a consequence, it makes sense to talk about properties that hold at particular locations, and it becomes natural to consider spatial modalities for formulas that hold at some location. In this talk, we describe techniques for reasoning about logical properties, both syntactically via a proof system, and semantically via properties of the model.

(Joint work with Luca Cardelli.)