Towards Spatial Bisimilarity for Closure Models: Logical and Coalgebraic\n Characterisations

The topological interpretation of modal logics provides descriptive languages\nand proof systems for reasoning about points of topological spaces. Recent work\nhas been devoted to model checking of spatial logics on discrete spatial\nstructures, such as finite graphs and digital images, with applications in\nvarious case studies including medical image analysis. These recent\ndevelopments required a generalisation step, from topological spaces to closure\nspaces. In this work we initiate the study of bisimilarity and minimisation\nalgorithms that are consistent with the closure spaces semantics. For this\npurpose we employ coalgebraic models. We present a coalgebraic definition of\nbisimilarity for quasi-discrete models, which is adequate with respect to a\nspatial logic with reachability operators, complemented by a free and\nopen-source minimisation tool for finite models. We also discuss the\nnon-quasi-discrete case, by providing a generalisation of the well-known\nset-theoretical notion of topo-bisimilarity, and a categorical definition, in\nthe same spirit as the coalgebraic rendition of neighbourhood frames, but\nemploying the covariant power set functor, instead of the contravariant one. We\nprove its adequacy with respect to infinitary modal logic.\n

Paper

Similar papers

© 2026 NYSGPT2525 LLC