# Geometric Model Checking of Continuous Space

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 10 of its 81 references that are in the map.
- First posted on arXiv 13 May 2021.

## Builds on (most cited first, 10 of 10)

- [The Simplex Tree: an Efficient Data Structure for General Simplicial Complexes](https://mlsanity.com/paper/2001.02581/) (2020)
- [A Novel Spatial-Temporal Specification-Based Monitoring System for Smart Cities](https://mlsanity.com/paper/2104.04904/) (2021)
- [Specifying and Verifying Properties of Space - Extended Version](https://mlsanity.com/paper/1406.6393/) (2014)
- [Model Checking Spatial Logics for Closure Spaces](https://mlsanity.com/paper/1609.06513/) (2016)
- [Qualitative and Quantitative Monitoring of Spatio-Temporal Properties with SSTL](https://mlsanity.com/paper/1706.09334/) (2017)
- [VoxLogicA: a Spatial Model Checker for Declarative Image Analysis (Extended Version)](https://mlsanity.com/paper/1811.05677/) (2018)
- [Spatial Logics and Model Checking for Medical Imaging (Extended Version)](https://mlsanity.com/paper/1811.06065/) (2018)
- [Towards Spatial Bisimilarity for Closure Models: Logical and Coalgebraic Characterisations](https://mlsanity.com/paper/2005.05578/) (2020)
- [Analysing Spatial Properties on Neighbourhood Spaces](https://mlsanity.com/paper/2007.01266/) (2020)
- [A spatial model checker in GPU (extended version)](https://mlsanity.com/paper/2010.07284/) (2020)

## Abstract (arXiv)

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.