拓扑小径自由图类上低单向度CMSO片段的模型检查
计算机科学中的逻辑
2026-05-04 v1 组合数学
摘要
算法元定理通过将逻辑可表达性与结构图属性关联，解释了大类计算问题的可解性。虽然如FO+dp等一阶逻辑扩展在排除固定拓扑小径的图类上允许高效模型检查，但针对更丰富CMSO片段的类似结果先前尚未知晓。我们进一步发展Sau、Stamoulis和Thilikos [SODA 2025]的框架，通过标注图参数对CMSO进行片段化处理，这些参数限制集合量化仅限于满足有限结构条件的顶点集合。遵循此方法，我们识别出一个CMSO片段，即仅允许量化具有我们称为低单向度（low monodimensionality）特性的集合，这一般化了若干先前已知的逻辑，我们证明该片段（增强后）加上disjoint-paths谓词的模型检查在拓扑小径自由图类上是固定参数可解。此类图基本上界定了该逻辑在子图封闭图类上的可解性。结果之所以如此，因而我们的结果将若干已知算法元定理超越一阶逻辑提升至拓扑小径自由设置。
引用
@article{arxiv.2605.00192,
title = {Model Checking for Low Monodimensionality Fragments of CMSO on Topological-Minor-Free Graph Classes},
author = {Ignasi Sau and Nicole Schirrmacher and Sebastian Siebertz and Giannos Stamoulis and Dimitrios M. Thilikos and Alexandre Vigny},
journal= {arXiv preprint arXiv:2605.00192},
year = {2026}
}
备注
An extended abstract of this paper has been accepted to LICS 2026