A Spatial Logic for Concurrency (joint work with Luis Caires)

Luca Cardelli

(Microsoft Research, Cambridge)

We present the semantics and proof theory of a modal logic for describing the spatial organization and the behavior of distributed systems. In addition to standard logical and temporal operators, our logic includes spatial operations corresponding to process composition and name hiding, and a fresh name quantifier. Properties of concurrent systems can also be defined by second-order quantification and hence (through an encoding) by recursion. A central aim of our logic is the combination of a logical notion of freshness with inductive and coinductive definitions of properties.
Thursday 20th June 2002, 14:00
Robert Recorde Room
Department of Computer Science