Spatial logics are formalisms for expressing topological properties of structures based on geometrical entities and relations. In this paper we consider SLCS, the Spatial Logic for Closure Spaces, recently used for describing features of images and video frames. We equip the logic with temporal operators, and provide a linear-time semantics over finite traces. The resulting formalism allows one to state properties about geometrical entities whose attributes change over time. For the given extension, we prove the equivalence of its operational semantics with a denotational one. We then introduce a temporal extension of the tool VoxLogicA, a spatial model checker based on SLCS. The extension provides users with the possibility to analyse spatio-temporal properties of interest on image streams.

Spatial models are of increasing interest in traditional computer science domains and beyond. Spatial minimisation procedures are crucial for efficient model checking of such models that are often large in size. For the recent notion of spatial bisimilarity for quasi-discrete closure models, called `Compatible Paths' (CoPa) bisimilarity, an effective minimisation method is proposed, and shown to be correct. Reasoning about space represented by quasi-discrete closure models involves two different conditional reachability modalities: a forward reachability, similar to that used in temporal logic, and a backward modality, representing the fact that a point can be reached from another point, under certain conditions. The core of our minimisation method is the encoding of closure models as labelled transition systems, enabling minimisation algorithms for branching bisimilarity to compute CoPa equivalence classes. A prototype toolchain, VoxMinX, is proposed to validate the minimisation method. VoxMinX preserves the relationship between equivalence classes and sets of pixels in the original image. Experimental validation of the toolchain via benchmark examples demonstrates a promising speed-up in model checking of spatial properties for models of realistic size.

Model checking has traditionally focused on the analysis of the behaviour of concurrent systems. In this invited abstract, instead, we focus on spatial model checking. We briefly motivate its development and its application in the domain of medical imaging, providing a gentle guide to our recent work on that topic and future research lines.

The work described in this paper builds on the polyhedral semantics of the Spatial Logic for Closure Spaces (SLCS) and the geometric spatial model checker PolyLogicA. Polyhedral models are central in domains that exploit mesh processing, such as 3D computer graphics. A discrete representation of polyhedral models is given by cell poset models, which are amenable to geometric spatial model checking using SLCS eta, a weaker version of SLCS. In this work we show that the mapping from polyhedral models to cell poset models preserves and reflects SLCS eta. We also propose weak simplicial bisimilarity on polyhedral models and weak +/--bisimilarity on cell poset models, where by "weak" we mean that the relevant equivalence is coarser than the corresponding one for SLCS, leading to a greater reduction of the size of models and thus to more efficient model checking. We show that the proposed bisimilarities enjoy the Hennessy-Milner property, i.e. two points are weakly simplicial bisimilar iff they are logically equivalent for SLCS eta. Similarly, two cells are weakly +/--bisimilar iff they are logically equivalent in the poset-mo del interpretation of SLCS eta. Furthermore we present a model minimisation procedure and prove that it correctly computes the minimal model with respect to weak +/--bisimilarity, i.e. with respect to logical equivalence of SLCS eta. The procedure works via an encoding into LTSs and then exploits branching bisimilarity on those LTSs, exploiting the minimisation capabilities as included in the mCRL2 toolset. Various examples show the effectiveness of the approach.

This work explores the potential of spatial model checking of polyhedral models on a number of selected examples. In computer graphics polyhedral models can be found in the form of triangular surface meshes of tetrahedral volume meshes which are abundant. Spatial model checking is used to analyse spatial properties of interest of such models expressed in a suitable spatial logic. The original contributions of this paper are twofold. First we illustrate how a polyhedral model can be enriched by adding the outcome of one model checking session as an atomic proposition to the original model. This is useful as it provides a way to reduce the length of formulas to check on such models and to obtain more insightful results when these models are used for graphical visualisation. Second we show that this form of enrichment also enables practical model minimisation providing deeper insights in the basic spatial structure of the model in terms of the spatial logic properties it enjoys. This work is performed in the context of the geometric spatial model checker PolyLogicA, the visualizer PolyVisualizer and the polyhedral semantics of the Spatial Logic for Closure Spaces SLCS.

Closure spaces, a generalisation of topological spaces, have shown to be a convenient theoretical framework for spatial model checking. The closure operator of closure spaces and quasi-discrete closure spaces induces a notion of neighborhood akin to that of topological spaces that build on open sets. For closure models and quasi-discrete closure models, in this paper we present three notions of bisimilarity that are logically characterised by corresponding modal logics with spatial modalities: (i) CM-bisimilarity for closure models (CMs) is shown to generalise Topo-bisimilarity for topological models. CM-bisimilarity corresponds to equivalence with respect to the infinitary modal logic IML that includes the modality ${\cal N}$ for ``being near''. (ii) CMC-bisimilarity, with `CMC' standing for CM-bisimilarity with converse, refines CM-bisimilarity for quasi-discrete closure spaces, carriers of quasi-discrete closure models. Quasi-discrete closure models come equipped with two closure operators, Direct ${\cal C}$ and Converse ${\cal C}$, stemming from the binary relation underlying closure and its converse. CMC-bisimilarity, is captured by the infinitary modal logic IMLC including two modalities, Direct ${\cal N}$ and Converse ${\cal N}$, corresponding to the two closure operators. (iii) CoPa-bisimilarity on quasi-discrete closure models, which is weaker than CMC-bisimilarity, is based on the notion of compatible paths. The logical counterpart of CoPa-bisimilarity is the infinitary modal logic ICRL with modalities Direct $\zeta$ and Converse $\zeta$, whose semantics relies on forward and backward paths, respectively. It is shown that CoPa-bisimilarity for quasi-discrete closure models relates to divergence-blind stuttering equivalence for Kripke structures.

This paper presents preliminary results in the definition of a comprehensive benchmark framework designed to systematically evaluate spatial reasoning capabilities in neural networks, with a particular focus on morphological properties such as connectivity and distance relationships. The framework is currently being used to study the capabilities of nnU-Net, exploiting the spatial model checker VoxLogicA to generate two distinct categories of synthetic datasets: maze connectivity problems for topological analysis and spatial distance computation tasks for geometric understanding. Each category is evaluated across multiple resolutions to assess scalability and generalization properties. The automated pipeline encompasses a complete machine learning workflow including: synthetic dataset generation, standardized training with cross-validation, inference execution, and comprehensive evaluation using Dice coefficient and IoU (Intersection over Union) metrics. Preliminary experimental results demonstrate significant challenges in neural network spatial reasoning capabilities, revealing systematic failures in basic geometric and topological understanding tasks. The framework provides a reproducible experimental protocol, enabling researchers to identify specific limitations. Such limitations could be addressed through hybrid approaches combining neural networks with symbolic reasoning methods for improved spatial understanding in clinical applications, establishing a foundation for ongoing research into neural network spatial reasoning limitations and potential solutions.

Segmentation of 3D medical images, and brain segmentation in particular, is an important topic in neuroimaging and in radiotherapy. Overcoming the current, time consuming, practise of manual delineation of brain tumours and providing an accurate, explainable, and replicable method of segmentation of the tumour area and related tissues is therefore an open research challenge. In this paper, we first propose a novel symbolic approach to brain segmentation and delineation of brain lesions based on spatial model checking. This method has its foundations in the theory of closure spaces, a generalisation of topological spaces, and spatial logics. At its core is a high-level declarative logic language for image analysis, ImgQL, and an efficient spatial model checker, VoxLogicA, exploiting state-of-the-art image analysis libraries in its model checking algorithm. We then illustrate how this technique can be combined with Machine Learning techniques leading to a hybrid AI approach that provides accurate and explainable segmentation results. We show the results of the application of the symbolic approach on several public datasets with 3D magnetic resonance (MR) images. Three datasets are provided by the 2017, 2019 and 2020 international MICCAI BraTS Challenges with 210, 259 and 293 MR images, respectively, and the fourth is the BrainWeb dataset with 20 (synthetic) 3D patient images of the normal brain. We then apply the hybrid AI method to the BraTS 2020 training set. Our segmentation results are shown to be in line with the state-of-the-art with respect to other recent approaches, both from the accuracy point of view as well as from the view of computational efficiency, but with the advantage of them being explainable.

We present the design of a meta-programming system for hybrid AI, integrating spatial model checking and machine learning. The proposed system architecture blends together different programming languages and execution technologies using a simplified, declarative metalanguage. The design features a global-model-checking-alike execution model, backed up by a microservices architecture. The system is meant to be a follow up to the spatial model checker VoxLogicA currently used for research on declarative medical image analysis, aimed at explainable by construction artificial intelligence.

In the context of spatial logics and spatial model checking for polyhedral models - mathematical basis for visualisations in continuous space - we propose a weakening of simplicial bisimilarity. We additionally propose a corresponding weak notion of +/--bisimilarity on cell-poset models, discrete representation of polyhedral models. We show that two points are weakly simplicial bisimilar iff their representations are weakly +/--bisimilar. The advantage of this weaker notion is that it leads to a stronger reduction of models than its counterpart that was introduced in our previous work. This is important, since real-world polyhedral models, such as those found in domains exploiting mesh processing, typically consist of large numbers of cells. We also propose SLCS., a weaker version of the Spatial Logic for Closure Spaces (SLCS) on polyhedral models, and we show that the proposed bisimilarities enjoy the Hennessy-Milner property: two points are weakly simplicial bisimilar iff they are logically equivalent for SLCS.. Similarly, two cells are weakly +/--bisimilar iff they are logically equivalent in the poset-model interpretation of SLCS.. This work is performed in the context of the geometric spatial model checker PolyLogicA and the polyhedral semantics of SLCS.

In the context of spatial logics and spatial model checking for polyhedral models — mathematical basis for visualisations in continuous space — we propose a weakening of simplicial bisimilarity. We additionally propose a corresponding weak notion of ± -bisimilarity on cell-poset models, discrete representation of polyhedral models. We show that two points are weakly simplicial bisimilar iff their representations are weakly ± -bisimilar. The advantage of this weaker notion is that it leads to a stronger reduction of models than its counterpart that was introduced in our previous work. This is important, since real-world polyhedral models, such as those found in domains exploiting mesh processing, typically consist of large numbers of cells. We also propose SLCS _η , a weaker version of the Spatial Logic for Closure Spaces (SLCS) on polyhedral models, and we show that the proposed bisimilarities enjoy the Hennessy-Milner property: two points are weakly simplicial bisimilar iff they are logically equivalent for SLCS _η . Similarly, two cells are weakly ± -bisimilar iff they are logically equivalent in the poset-model interpretation of SLCS _η . This work is performed in the context of the geometric spatial model checker PolyLogicA and the polyhedral semantics of SLCS.

The notion of bisimilarity plays an important role in concurrency theory. It provides formal support to the idea of processes having “equivalent behaviour” and is a powerful tool for model reduction. Furthermore, bisimilarity typically coincides with logical equivalence of an appropriate modal logic enabling model checking to be applied on reduced models. Recently, notions of bisimilarity have been proposed also for models of space, including those based on polyhedra. The latter are central in many domains of application that exploit mesh processing and typically consist of millions of cells, the basic components of face-poset models, discrete representations of polyhedral models. This paper builds on the polyhedral semantics of the Spatial Logic for Closure Spaces (SLCS) for which the geometric spatial model checker PolyLogicA has been developed, that is based on face-poset models. We propose a novel notion of spatial bisimilarity for face-poset models, called ±-bisimilarity. We show that it coincides with logical equivalence induced by SLCS on such models. The latter corresponds to logical equivalence with respect to SLCS on polyhedra which, in turn, coincides with simplicial bisimilarity, a notion of bisimilarity for continuous spaces.

Spatial logic and spatial model checking have great potential for traditional computer science domains and beyond. Reasoning about space involves two different conditional reachability modalities: a forward reachability, similar to that used in temporal logic, and a backward modality representing that a point can be reached from another point, under certain conditions. Since spatial models can be huge, suitable model minimisation techniques are crucial for efficient model checking. An effective minimisation method for the recent notion of spatial Compatible Path (CoPa)-bisimilarity is proposed, and shown to be correct. The core of our method is the encoding of Closure Models as Labelled Transition Systems, enabling minimisation algorithms for branching bisimulation to compute CoPa equivalence classes. Initial validation via benchmark examples demonstrates a promising speed-up in model checking of spatial properties for models of realistic size.

Topological Spatial Model Checking is a recent paradigm where model checking techniques are developed for the topological interpretation of Modal Logic. The Spatial Logic of Closure Spaces, SLCS, extends Modal Logic with reachability connectives that, in turn, can be used for expressing interesting spatial properties, such as “being near to” or “being surrounded by”. SLCS constitutes the kernel of a solid logical framework for reasoning about discrete space, such as graphs and digital images, interpreted as quasi discrete closure spaces. Following a recently developed geometric semantics of Modal Logic, we propose an interpretation of SLCS in continuous space, admitting a geometric spatial model checking procedure, by resorting to models based on polyhedra. Such representations of space are increasingly relevant in many domains of application, due to recent developments of 3D scanning and visualisation techniques that exploit mesh processing. We introduce PolyLogicA, a geometric spatial model checker for SLCS formulas on polyhedra and demonstrate feasibility of our approach on two 3D polyhedral models of realistic size. Finally, we introduce a geometric definition of bisimilarity, proving that it characterises logical equivalence.

We present a feasibility study on the use of spatial logic model checking for real-time analysis of high-resolution video streams with the tool VoxLogicA. VoxLogicA is a voxel-based image analyser based on the Spatial Logic for Closure Spaces, a logic catered to deal with properties of spatial structures such as topological spaces, graphs and polyhedra. The underlying language includes operators to model proximity and reachability. We demonstrate, via the analysis of a series of video frames from a well-known video game, that it is possible to analyse high-resolution videos in real-time by exploiting the speed-up of VoxLogicA-GPU, a recently developed GPU-based version of the tool, which is 1–2 orders of magnitude faster than its previous iteration. Potential applications of real-time video analysis include medical imaging applications such as ultrasound exams, and other video-based diagnostic techniques. More broadly speaking, this work can be the first step towards novel information retrieval methods suitable to find information in a declarative way, in possibly large collections of video streams.

In medical imaging, (semi-)automatic image analysis techniques have been proposed to support the current time-consuming and cognitively demanding practice of manual segmentation of regions of interest (ROIs). The recently proposed image query language ImgQL, based on spatial logic and model checking, represents segmentation methods as concise, domain-oriented, human-readable procedures aimed at domain experts rather than technologists, and has been validated in several case studies. Such efforts are directed towards a human-centred Artificial Intelligence methodology. To this aim, we complemented the ongoing research line with a study of the Human-Computer Interaction aspects. In this work we investigate the design of a graphical user interface (GUI) prototype that supports the analysis procedure with minimal impact on the focus and the memory load of domain experts.

We adapt the standard notion of bisimilarity for topological models to closure models and refine it for quasi-discrete closure models. We also define an additional, weaker notion of bisimilarity that is based on paths in space and expresses a form of conditional reachability in a way that is reminiscent of Stuttering Equivalence on transition systems. For each bisimilarity we provide a characterisation with respect to a suitable spatial logic.