We present 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 notion of freshness with inductive and coinductive definitions of properties.