一句话：提出多面体模型上的弱单纯形互模拟与胞腔偏序模型上的弱±互模拟，并给出基于LTS编码和mCRL2的最小化方法。
该文研究多面体模型及其离散胞腔偏序模型上的空间逻辑 SLCSη 的模型检测。作者证明多面体到胞腔偏序模型的映射保持并反映 SLCSη，并定义多面体上的弱单纯形互模拟与胞腔偏序模型上的弱 ± 互模拟；弱等价比 SLCS 对应等价更粗，可显著缩小模型。论文证明二者具有 Hennessy-Milner 性质：互模拟等价当且仅当逻辑等价。还提出最小化过程，通过编码为 LTS 并利用 mCRL2 的分支互模拟最小化功能，正确计算弱 ± 互模拟意义下的最小模型；示例验证其有效性。
The work described in this paper builds on the polyhedral semantics of the Spatial Logic for Closure Spaces (SLCS) and the geometric spatial model checker PolyLogicA. Polyhedral models are central in domains that exploit mesh processing, such as 3D computer graphics. A discrete representation of polyhedral models is given by cell poset models, which are amenable to geometric spatial model checking on polyhedral models using the logical language SLCS$η$, a weaker version of SLCS. In this work we show that the mapping from polyhedral models to cell poset models preserves and reflects SLCS$η$. We also propose weak simplicial bisimilarity on polyhedral models and weak $\pm$-bisimilarity on cell poset models, where by ``weak'' we mean that the relevant equivalence is coarser than the corresponding one for SLCS, leading to a greater reduction of the size of models and thus to more efficient model checking. We show that the proposed bisimilarities enjoy the Hennessy-Milner property, i.e. two points are weakly simplicial bisimilar iff they are logically equivalent for SLCS$η$. Similarly, two cells are weakly $\pm$-bisimilar iff they are logically equivalent in the poset-model interpretation of SLCS$η$. Furthermore we present a model minimisation procedure and prove that it correctly computes the minimal model with respect to weak $\pm$-bisimilarity, i.e. with respect to logical equivalence of SLCS$η$. The procedure works via an encoding into LTSs and then exploits branching bisimilarity on those LTSs, exploiting the minimisation capabilities as included in the mCRL2 toolset. Various examples show the effectiveness of the approach.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2411-11428,
title = {Weak Simplicial Bisimilarity and Minimisation for Polyhedral Model Checking},
author = {Nick Bezhanishvili and Laura Bussi and Vincenzo Ciancia and David Gabelaia and Mamuka Jibladze and Diego Latella and Mieke Massink and Erik P. de Vink},
journal = {Logical Methods in Computer Science},
volume = {Volume 22, Issue 1},
year = {2026},
doi = {10.46298/lmcs-22(1:6)2026}
}