一句话：为准离散闭包空间提出三种互模拟，并给出对应的空间模态逻辑刻画及与已知等价的联系。
闭包空间是拓扑空间的推广，已成为空间模型检测的理论框架。本文针对闭包模型与准离散闭包模型，研究其行为等价——互模拟。作者提出三种互模拟：面向闭包模型的 CM-互模拟，可推广拓扑模型上的 topo-互模拟，并视为邻域互模拟的实例，由含“接近”模态 N 的无穷模态逻辑 IML 刻画；面向准离散闭包空间的 CMC-互模拟，利用直接与逆向闭包算子，由含 Direct N 与 Converse N 的 IMLC 刻画；以及基于相容路径的 CoPa-互模拟，它弱于 CMC，由含正/反向路径模态的 ICRL 刻画，并与 Kripke 模型上忽略发散的 stuttering 等价相关。
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 and to be an instantiation of neighbourhood bisimilarity, when CMs are seen as (augmented) neighbourhood models. CM-bisimilarity corresponds to equivalence with respect to the infinitary modal logic IML that includes the modality ${\cal N}$ for ``being near to''. (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 $ζ$ and Converse $ζ$, 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 models.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{CianciaLMV25,
title = {On Bisimilarity for Quasi-discrete Closure Spaces},
author = {Vincenzo Ciancia and Diego Latella and Mieke Massink and Erik P. de Vink},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 3},
year = {2025},
doi = {10.46298/lmcs-21(3:21)2025}
}