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

2008/10/16 by Viorica Sofronie-Stokkermans, Sofronie-Stokkermans, Viorica · 1 citation
Computer Science · #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #cs.LO

paper · pdf · doi:10.48550/arxiv.0810.2877

30 pages

arxiv created 2008/10/16 · arxiv updated 2009/12/01

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.

Cited by

• On verification and constraint generation for families of similar hybrid automata

Related

• Sheaf and duality methods for analyzing multi-model systems
• Dynamical Systems and Sheaves
• Geometric contexts and applications to logic
• Sheaf Representations and Duality in Logic
• Abstraction, Composition and Contracts: A Sheaf Theoretic Approach