# Spatial Logics and Model Checking for Medical Imaging (Extended Version)

arXiv: https://arxiv.org/abs/1811.06065 · HTML: https://mlsanity.com/paper/1811.06065/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 14 Nov 2018.

## Built on by (most cited first, 4 of 4)

- [Formalizing and Evaluating Requirements of Perception Systems for Automated Vehicles using Spatio-Temporal Perception Logic](https://mlsanity.com/paper/2206.14372/) (2022)
- [Geometric Model Checking of Continuous Space](https://mlsanity.com/paper/2105.06194/) (2021)
- [A Hybrid Deep Learning and Model-Checking Framework for Accurate Brain Tumor Detection and Validation](https://mlsanity.com/paper/2501.01991/) (2024)
- [Model Checking in Medical Imaging for Tumor Detection and Segmentation](https://mlsanity.com/paper/2501.02024/) (2025)

## Abstract (arXiv)

Recent research on spatial and spatio-temporal model checking provides novel image analysis methodologies, rooted in logical methods for topological spaces. Medical Imaging (MI) is a field where such methods show potential for ground-breaking innovation. Our starting point is SLCS, the Spatial Logic for Closure Spaces -- Closure Spaces being a generalisation of topological spaces, covering also discrete space structures -- and topochecker, a model-checker for SLCS (and extensions thereof). We introduce the logical language ImgQL ("Image Query Language"). ImgQL extends SLCS with logical operators describing distance and region similarity. The spatio-temporal model checker topochecker is correspondingly enhanced with state-of-the-art algorithms, borrowed from computational image processing, for efficient implementation of distancebased operators, namely distance transforms. Similarity between regions is defined by means of a statistical similarity operator, based on notions from statistical texture analysis. We illustrate our approach by means of two examples of analysis of Magnetic Resonance images: segmentation of glioblastoma and its oedema, and segmentation of rectal carcinoma.