一句话：提出连续空间上空间逻辑 SLCS 的几何语义与基于多面体的模型检测工具 PolyLogicA。
拓扑空间模型检测将模态逻辑的拓扑解释用于空间性质验证。SLCS 在模态逻辑上增加可达性连接词，可表达“接近”“被包围”等离散空间性质。本文借鉴模态逻辑的几何语义，把 SLCS 解释到连续空间，并以多面体作为模型表示，给出几何空间模型检测过程。作者实现 PolyLogicA，一个面向多面体上 SLCS 公式的几何空间模型检测器，并在两个真实规模的三维多面体模型上验证可行性。文章还定义几何互模拟，证明其恰好刻画逻辑等价。
Topological Spatial Model Checking is a recent paradigm where model checking techniques are developed for the topological interpretation of Modal Logic. The Spatial Logic of Closure Spaces, SLCS, extends Modal Logic with reachability connectives that, in turn, can be used for expressing interesting spatial properties, such as "being near to" or "being surrounded by". SLCS constitutes the kernel of a solid logical framework for reasoning about discrete space, such as graphs and digital images, interpreted as quasi discrete closure spaces. Following a recently developed geometric semantics of Modal Logic, we propose an interpretation of SLCS in continuous space, admitting a geometric spatial model checking procedure, by resorting to models based on polyhedra. Such representations of space are increasingly relevant in many domains of application, due to recent developments of 3D scanning and visualisation techniques that exploit mesh processing. We introduce PolyLogicA, a geometric spatial model checker for SLCS formulas on polyhedra and demonstrate feasibility of our approach on two 3D polyhedral models of realistic size. Finally, we introduce a geometric definition of bisimilarity, proving that it characterises logical equivalence.
@article{paperbot1642,
title = {Geometric Model Checking of Continuous Space},
author = {Nick Bezhanishvili and Vincenzo Ciancia and David Gabelaia and Gianluca Grilletti and Diego Latella and Mieke Massink},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 4},
year = {2022},
doi = {10.46298/lmcs-18(4:7)2022}
}