In this paper we present an overview of results that show that
states, transitions and behavior of concurrent systems
can often be modeled as sheaves over a suitable topological space.
In such contexts, geometric logic can be used to test whether
(and describe which) local properties, of individual systems,
are preserved, at a global level, when interconnecting the systems.