2026-07-072026-07-07http://salesiana.dossiersoluciones.com/handle/123456789/171651In 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 (i.e. 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 the ideas by means of an example involving a family of interacting controllers for trains on a rail track.30 pagesLogic in Computer Sciencetext