A Spatial Logic for Simplicial Models

Collective Adaptive Systems often consist of many heterogeneous componentstypically organised in groups. These entities interact with each other byadapting their behaviour to pursue individual or collective goals. In thesesystems, the distribution of these entities determines a space that can beeither physical or logical. The former is defined in terms of a physicalrelation among components. The latter depends on logical relations, such asbeing part of the same group. In this context, specification and verificationof spatial properties play a fundamental role in supporting the design ofsystems and predicting their behaviour. For this reason, different tools andtechniques have been proposed to specify and verify the properties of space,mainly described as graphs. Therefore, the approaches generally use modelspatial relations to describe a form of proximity among pairs of entities.Unfortunately, these graph-based models do not permit considering relationsamong more than two entities that may arise when one is interested indescribing aspects of space by involving interactions among groups of entities.In this work, we propose a spatial logic interpreted on simplicial complexes.These are topological objects, able to represent surfaces and volumesefficiently that generalise graphs with higher-order edges. We discuss how thesatisfaction of logical formulas can be verified by a correct and completemodel checking algorithm, which is linear to the dimension of the simplicialcomplex and logical formula. The expressiveness of the proposed logic isstudied in terms of the spatial variants of classical bisimulation andbranching bisimulation relations defined over simplicial complexes