通过最小化模型和分支互模拟进行图像空间模型检验
计算机科学中的逻辑
2026-06-30 v1
摘要
空间模型在传统计算机科学领域及其他领域越来越受关注。空间最小化过程对于高效检验通常规模较大的此类模型至关重要。针对准离散闭包模型的空间互模拟的新概念，称为“兼容路径”（CoPa）互模拟，提出了一种有效的最小化方法，并证明了其正确性。对由准离散闭包模型表示的空间进行推理涉及两种不同的条件可达性模态：一种前向可达性，类似于时序逻辑中使用的；以及一种后向模态，表示在特定条件下可以从另一点到达某一点。我们最小化方法的核心是将闭包模型编码为标记转换系统，使分支互模拟的最小化算法能够计算CoPa等价类。提出了一个原型工具链VoxMinX来验证最小化方法。VoxMinX保留了等价类与原始图像中像素集之间的关系。通过基准示例对工具链进行的实验验证表明，在现实规模模型的空间属性模型检验中，速度有显著提升。
引用
@article{arxiv.2606.31344,
title = {Spatial Model Checking of Images via Minimised Models and Branching Bisimilarity},
author = {Vincenzo Ciancia and Jan Friso Groote and Diego Latella and Mieke Massink and Erik P. de Vink},
journal= {arXiv preprint arXiv:2606.31344},
year = {2026}
}