Back to list of 2000/01 seminars

We describe a new flavor of modal logics for concurrency; the main novelty is the introduction of "spatial" connectives, in addition to standard and temporal connectives. Our logics 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 and checked by typechecking, by model checking, or by proof search (as in proof-carrying code).

A spatial logic was initially devised for the Ambient Calculus, where location structures give rise naturally to spatial connectives. But spatial connective make sense also for, e.g., the pi-calculus. We are now focusing on describing hidden and secret locations, i.e. on the logical interpretation of the pi-calculus restriction operations, and on the interactions between recursive formulas and logical notions of "freshness" previously studied by Gabbay and Pitts.