A Spatial Logic for Simplicial Models

TL;DR

This work introduces Spatial Logic for Simplicial Complexes (SLSC), enabling formal reasoning about spatial properties on higher-order interactions modeled by simplicial complexes instead of graphs. It defines a simplicial model, the syntax and semantics of the neighborhood and reachability operators, and adjacency-based semantics, along with a model-checking algorithm whose runtime scales linearly with the formula size and model size. The paper also develops two adjacency-aware notions of bisimulation, showing that fragments of SLSC correspond exactly to these equivalences under appropriate conditions. This framework broadens spatial verification to surfaces, volumes, and group interactions, with potential applications in engineering of collective adaptive systems and topology-inspired analysis.

Abstract

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. 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 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 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 bisimulation and branching bisimulation relations defined over simplicial complexes.

Figures (9)

• Figure 1: Representations of higher-order interactions. The set of interactions $[v_1, v_2, v_3]$, $[v_3,v_4]$, $[v_4,v_5]$, $[v_3,v_5]$ is represented using a simplicial complex (A). Simplicial complexes allow to discriminate between higher order interactions and sums of low-order ones (B). They require the presence of all possible subsimplices (C). Relaxing this condition effectively implies moving from simplices to hypergraphs (D), which are the most general and less constrained representation of higher-order interactions.
• Figure 2: A representation of some sensors in area to identify dangerous zones, where each $s_{i}$ represents a sensor while the blue cross identifies the victim.
• Figure 3: From left to right simplices of dimension zero, one, two and three are shown.
• Figure 4: In (A), a simplicial complex; in (B), a collection of simplices that is not a simplicial complex.
• Figure 5: An network of scientific collaborations.

Theorems & Definitions (39)

• Definition 2.1: Simplicial complex
• Example 2.2
• Example 2.3
• Definition 2.4: Lower adjacency
• Definition 2.5: Upper adjacency
• Definition 2.6: Spatial adjacency
• Proposition 2.7
• proof
• Proposition 2.8
• proof