Towards Spatial Bisimilarity for Closure Models: Logical and Coalgebraic Characterisations

TL;DR

This paper develops coalgebraic models and algorithms for bisimilarity in closure spaces, extending topological modal logic reasoning to discrete spatial structures like digital images.

Contribution

It introduces a coalgebraic definition of bisimilarity for closure models and provides a minimisation tool, advancing reasoning about spatial logics in discrete structures.

Findings

Coalgebraic bisimilarity for quasi-discrete models established.

A minimisation tool for finite models developed.

Generalisation of topo-bisimilarity for non-quasi-discrete models discussed.

Abstract

The topological interpretation of modal logics provides descriptive languages and proof systems for reasoning about points of topological spaces. Recent work has been devoted to model checking of spatial logics on discrete spatial structures, such as finite graphs and digital images, with applications in various case studies including medical image analysis. These recent developments required a generalisation step, from topological spaces to closure spaces. In this work we initiate the study of bisimilarity and minimisation algorithms that are consistent with the closure spaces semantics. For this purpose we employ coalgebraic models. We present a coalgebraic definition of bisimilarity for quasi-discrete models, which is adequate with respect to a spatial logic with reachability operators, complemented by a free and open-source minimisation tool for finite models. We also discuss the non-quasi-discrete case, by providing a generalisation of the well-known set-theoretical notion of topo-bisimilarity, and a categorical definition, in the same spirit as the coalgebraic rendition of neighbourhood frames, but employing the covariant power set functor, instead of the contravariant one. We prove its adequacy with respect to infinitary modal logic.