Sheaves and geometric logic in concurrency

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