一句话：提出基于闭包空间的空间逻辑，并给出个体与集体片段的模型检测算法及原型工具。
针对传统形式验证忽视物理空间性质的问题，本文提出基于拓扑的空间验证方法。作者从模态逻辑的拓扑解释出发，将邻域模态提升到比拓扑更一般的闭包空间，以覆盖离散、图结构等情形；在逻辑中引入 surrounded、传播及集体算子，后者作用于空间点集而非单点。论文定义了个体与集体空间片段的模型检测过程，给出高效算法，并实现概念验证工具。
Spatial aspects of computation are becoming increasingly relevant in Computer Science, especially in the field of collective adaptive systems and when dealing with systems distributed in physical space. Traditional formal verification techniques are well suited to analyse the temporal evolution of programs; however, properties of space are typically not taken into account explicitly. We present a topology-based approach to formal verification of spatial properties depending upon physical space. We define an appropriate logic, stemming from the tradition of topological interpretations of modal logics, dating back to earlier logicians such as Tarski, where modalities describe neighbourhood. We lift the topological definitions to the more general setting of closure spaces, also encompassing discrete, graph-based structures. We extend the framework with a spatial surrounded operator, a propagation operator and with some collective operators. The latter are interpreted over arbitrary sets of points instead of individual points in space. We define efficient model checking procedures, both for the individual and the collective spatial fragments of the logic and provide a proof-of-concept tool.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{CianciaLLM16,
title = {Model Checking Spatial Logics for Closure Spaces},
author = {Vincenzo Ciancia and Diego Latella and Michele Loreti and Mieke Massink},
journal = {Logical Methods in Computer Science},
volume = {Volume 12, Issue 4},
year = {2017},
doi = {10.2168/lmcs-12(4:2)2016}
}