Sheaves and Geometric Logic and Applications to Modular Verification of Complex Systems
Viorica Sofronie-Stokkermans · Electronic Notes in Theoretical Computer Science · 2009
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 the ideas by means of an example involving a family of interacting controllers for trains on a rail track.