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.

翻译：闭包空间作为拓扑空间的一种推广，已被证明是空间模型检测中一个便利的理论框架。闭包空间和拟离散闭包空间的闭包算子导出了类似于基于开集的拓扑空间中的邻域概念。针对闭包模型和拟离散闭包模型，本文提出了三种双相似性概念，它们通过相应的含空间模态的模态逻辑进行逻辑刻画：(i) 闭包模型（CM）上的CM-双相似性被证明可推广拓扑模型上的Topo-双相似性。CM-双相似性对应于包含模态${\cal N}$（表示“邻近”）的无穷模态逻辑IML的等价关系。(ii) CMC-双相似性（其中CMC代表带逆关系的CM-双相似性）针对拟离散闭包空间（即拟离散闭包模型的载体）对CM-双相似性进行了细化。拟离散闭包模型配备了两个闭包算子：正向${\cal C}$和逆向${\cal C}$，它们源自闭包所基于的二元关系及其逆关系。包含两种模态（正向${\cal N}$和逆向${\cal N}$，分别对应两个闭包算子）的无穷模态逻辑IMLC刻画了CMC-双相似性。(iii) 基于相容路径概念的拟离散闭包模型上的CoPa-双相似性弱于CMC-双相似性。CoPa-双相似性的逻辑对应物是无穷模态逻辑ICRL，其包含模态正向$\zeta$和逆向$\zeta$，语义分别依赖于前向路径和后向路径。研究表明，拟离散闭包模型上的CoPa-双相似性与Kripke结构上的发散盲随机等价性相关联。