Spatial Logics for Distributed Systems

Luca Cardelli

Microsoft Research Cambridge

Wide-area distributed systems require new paradigms for computation and interaction. For example, such systems must be based on the asynchronous interaction of autonomous and loosely-connected entities, as opposed to the familiar synchronous interaction of closely-coupled objects. This is now very well understood: new computing paradigms are actively being developed, both practically and theoretically. Autonomy, security, and privacy, are now major concerns, in addition to the traditional concerns of correctness and efficiency.

We call "spatial logic" a logic where a property can describe a spatial component of a larger system. This idea may be quite general and applied in various ways. As a start, we have concretely investigated spatial logics for specific calculi of distributed systems. The spatial aspect is most obvious for calculi that have built-in notions of locations where processes reside. But, in retrospect, the idea can be usefully applied also to familiar calculi of concurrency. For example, the hiding operator of pi-calculus can be seen as restricting the location of a name (e.g. for privacy), and therefore has a spatial aspect that can be exploited by appropriate logical operators. More strikingly, the familiar parallel composition operator has an obvious flavor of spatial separation that can be exploited by logical operators that had so far been largely overlooked.

In this lecture we discuss the new view of computing arising from wide-area distributed systems, and the implications that have eventually led us to consider new logical properties. We hope that our point of view will be helpful in developing new forms of analysis and new tools for taming the needs of wide-area distributed computing.

(Reflecting work with Andy Gordon, Microsoft Research Cambridge, and Luis Caires, FCT/UNL Lisbon)