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 in supporting the design of systems and predicting their behaviour. \changedtext{For this reason, different tools and techniques have been proposed to specify and verify the properties of space, mainly described as graphs. Therefore, the approaches generally use model spatial relations to describe 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 aspects of space by involving \emph{interactions among groups of entities. 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.

翻译：集体自适应系统通常由许多异质组件组成，这些组件往往以群体形式组织。这些实体通过调整自身行为来追求个体或集体目标，从而实现彼此交互。在此类系统中，实体的分布决定了空间属性，该空间可为物理空间或逻辑空间。前者通过组件间的物理关系定义，后者则取决于逻辑关系（如属于同一群体）。在此背景下，空间特性的规约与验证在支持系统设计及行为预测中具有根本性作用。为此，研究者已提出多种用于规约与验证空间特性的工具与技术，这些空间特性通常以图结构描述。因此，现有方法通常采用空间关系建模来描述实体对之间的邻近形式。然而，当需要描述涉及实体群体交互的空间特征时，这类基于图的模型无法处理涉及两个以上实体的关系。本文提出一种在单纯复形上解释的空间逻辑。单纯复形作为拓扑对象，能高效表征曲面与体积，并通过高阶边对图结构进行泛化。我们探讨了如何通过正确完备的模型检测算法验证逻辑公式的满足性，该算法的时间复杂度与单纯复形及逻辑公式的维度呈线性关系。通过在单纯复形上定义经典互模拟与分支互模拟关系的空间变体，我们研究了所提逻辑的表达能力。