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 recursion. A central aim of our logic is the combination of a logical notion of freshness with inductive and coinductive definitions of properties.