中文

有界展开图类上后继不变一阶公式的模型检测

计算机科学中的逻辑 2023-08-15 v2

摘要

后继不变一阶公式是这样一种公式:它可访问结构论域上的辅助后继关系,但模型关系独立于该关系的特定解释。众所周知,在有限结构上,后继不变公式比无后继关系的普通一阶公式更具表达力。这自然引出一个问题:这种表达力的增强是否带来求解模型检测问题的额外代价,即判定给定结构连同某个(因而每个)后继关系是否为给定公式的模型的问题。早前研究表明,对底层Gaifman图是平面的[Engelmann et al., 2012]、排除固定minor [Eickmeyer et al., 2013]或固定拓扑minor [Eickmeyer and Kawarabayashi, 2016; Kreutzer et al., 2016]的有限结构类,为一阶逻辑增加后继不变性本质上不带来额外代价。本工作中,我们展示对于底层Gaifman图构成有界展开类的任意有限结构类,后继不变公式的模型检测问题是固定参数可处理的。我们的结果推广了所有早前结果,并接近于当前为普通一阶逻辑在无处稠密图类上所知的最佳可处理性结果。

关键词

引用

@article{arxiv.1701.08516,
  title  = {Model-Checking for Successor-Invariant First-Order Formulas on Graph Classes of Bounded Expansion},
  author = {Jan van den Heuvel and Stephan Kreutzer and Michał Pilipczuk and Daniel A. Quiroz and Roman Rabinovich and Sebastian Siebertz},
  journal= {arXiv preprint arXiv:1701.08516},
  year   = {2023}
}

备注

20 pages, submitted to LICS 2017