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.

翻译：本文工作建立在闭包空间空间逻辑(SLCS)的多面体语义与几何空间模型检测器PolyLogicA的基础上。多面体模型在利用网格处理的领域（如三维计算机图形学）中具有核心地位。多面体模型的离散表示由单元偏序集模型给出，该模型适用于使用逻辑语言SLCS$η$（SLCS的弱化版本）对多面体模型进行几何空间模型检测。本文证明了从多面体模型到单元偏序集模型的映射保持并反映SLCS$η$。我们进一步提出了多面体模型上的弱单纯双模拟与单元偏序集模型上的弱$\pm$-双模拟，其中“弱”意指相关等价关系比SLCS对应的等价关系更粗，从而能更大程度缩减模型规模，提升模型检测效率。我们证明了所提出的双模拟关系满足Hennessy-Milner性质，即两点弱单纯双模拟当且仅当它们在SLCS$η$下逻辑等价；类似地，两个单元弱$\pm$-双模拟当且仅当它们在SLCS$η$的偏序集模型解释下逻辑等价。此外，我们提出了一种模型最小化算法，并证明该算法能正确计算关于弱$\pm$-双模拟（即关于SLCS$η$逻辑等价）的最小模型。该算法通过将模型编码为LTS，进而利用这些LTS上的分支双模拟，并借助mCRL2工具集的最小化功能实现。多个实例验证了该方法的有效性。