Talk "Reasoning about space: a logical framework based on Simplicial Complexes"

by Michele Loreti

Sat, 27 March 2021 at 02:40 pm in Luxembourg, Luxembourg

Joint work with: Michela Quadrini

Abstract: Collective Adaptive Systems consist of a large number of heterogeneous components. These entities are typically organised in groups where participants interact to adapt their behaviour to environmental settings pursuing an individual or collective goal. In this context, the concept of locality is strictly related to the spatial distribution of system entities. Therefore, the characterisation and verification of the spatial properties play a fundamental role in understanding CAS behaviour and its design. Recently, different tools and languages have been introduced to specify and verify properties of space. However, these formalisms do not handle surfaces and volumes and relationships among a large number of entities, the so-called higher-order relationships, that may characterise interactions and relations among entities of a CAS. In this work, we propose a methodology to verify spatial properties on surfaces and volumes and that considers higher-order relationships among entities. We define a spatial logic interpreted on simplicial complexes. These are topological objects able to represent surfaces and volumes efficiently and that generalise graphs with higher-order edges. In the paper we present a correct and complete model checking algorithm, that is linear to the dimension of the simplicial complex and the logical formula. Finally, the expressiveness of the proposed spatial logic is studied in terms of bisimulation and branching bisimulation relations defined over simplicial complexes.