Sheaves and geometric logic and applications to the modular verification of complex systems

TL;DR

This paper introduces a sheaf-theoretic framework for modeling concurrent systems and uses geometric logic to facilitate modular verification, demonstrated through a train controller example.

Contribution

It presents a novel approach linking sheaves and geometric logic to model and verify complex systems modularly, enhancing understanding of system interconnections.

Findings

Sheaves effectively model states and behaviors of concurrent systems.

Geometric logic helps identify properties preserved during system composition.

Application to train controllers demonstrates practical utility.

Abstract

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 (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.