Spatial aspects of computation are prominent in Computer Science, especially when dealing with systems distributed in physical space or with image data acquired from various sources. However, formal verification techniques are usually concerned with temporal properties and do not explicitly handle spatial information. Our work stems from the topological interpretation of modal logics, the so-called Spatial Logics. We present a topology-based approach to model checking for spatial and spatio-temporal properties.

Our research was initiated with the definition of a modal logic enhanced with: 1) a reachability operator, in the general setting of Cech closure spaces, encompassing both topological spaces and graphs; 2) a collective extension, permitting global operators akin to region calculi. On top of this, applicability has been demonstrated via free and open source software tools, and case studies in the setting of smart transportation and image analysis.

In recent work, we explored the application domain of automatic contouring in Medical Imaging, introducing the tool VoxLogicA, which merges the state-of-the-art imaging library ITK with the unique combination of declarative specification and optimised execution provided by spatial model checking. The analysis of existing benchmarks of medical images, for segmentation of brain tumors, and for the automated contouring of nevi, shows that simple VoxLogicA specifications can reach state-of-the-art accuracy, competing with best-in-class algorithms based on machine learning, with the advantage of explainability and easy replicability.

More recently, we introduced a geometric interpretation on continuous space exploiting simplicial complexes, with applications to the analysis of 3D meshes, a GPU-based implementation, enabling a consistent efficiency speed-up, and a definition of bisimilarity, aimed at minimization up-to logical equivalence.