In this paper we show that states, transitions and behavior of
concurrent systems can often be modeled as sheaves over a
suitable topological space.
In this context, geometric logic can be used to describe which
local properties, of individual systems, are preserved, at a
global level, when interconnecting the systems.
The main area of application is to modular verification
of complex systems. We illustrate our ideas by means of an
example involving a family of interacting controllers for
trains on a rail track.