A Spatial Logic for a Simplicial Complex Model

Collective Adaptive Systems often consist of many heterogeneous components typically organised in groups. These entities interact with each other by adapting their behaviour to pursue individual or collective goals. In these systems, the distribution of these entities determines a space that can be either physical or logical. The former is defined in terms of a physical relation among components. The latter depends on logical relations, such as being part of the same group. In this context, specification and verification of spatial properties play a fundamental role to support the design of a system and predict its behaviour. For this reasons, different tools and techniques have been proposed to specify and verify the properties of space. However, these approaches are mainly based on graphs. These are used to model spatial relations, describing a form of proximity among pairs of entities. Unfortunately, these graph-based models do not permit considering relations among more than two entities that may arise when one is interested in describing \emph{multi-dimensional} aspects of space. In this work, we propose a spatial logic interpreted on \emph{simplicial complexes}. These are topological objects able to represent surfaces and volumes efficiently that generalise graphs with higher-order edges. We discuss how the satisfaction of logical formulas can be verified by a correct and complete model checking algorithm, which is linear to the dimension of the simplicial complex and logical formula. The expressiveness of the proposed logic is studied in terms of the spatial variants of classical \emph{bisimulation} and \emph{branching bisimulation} relations defined over simplicial complexes