paperbot · PL 论文追踪

全部论文 待读 收藏

P2 First Order Logic on Pathwidth Revisited Again

有界路径宽度上的一阶逻辑再探
LMCS vol.Volume 22, Issue 22026匹配度 1/10 · 该论文属于纯理论逻辑与自动机/算法元定理研究,讨论有界路径宽度图上 FO 性质的可判定性与复杂度,与用户核心方向(LLM/Agent 与静态分析、形式化验证的交叉,浮点程序分析,贝叶斯程序分析)没有直接关联。虽然形式化验证可能涉及逻辑与图结构,但本文不涉及程序分析、LLM、Agent 或工业落地。引用 5 inbox
Michael Lampis
crossref: 2026-09-10

AI 速览

一句话:证明有界路径宽度图上的 FO 性质可在线性时间判定,且对公式依赖为初等,推广有界树深元定理。

Courcelle 定理指出有界树宽图上所有 MSO 可表达性质可线性时间判定,但其隐含常数是随量词交替增长的指数塔,且在树上判定 FO 性质时该非初等下界标准假设下不可改进。本文重新审视该问题,寻找可改进的自然特例。作者证明:当输入图具有有界路径宽度(而非树宽)时,所有 FO 可表达性质都可在对输入公式初等依赖下判定。该结果推广了 Gajarský 与 Hliněný 针对有界树深图的元定理,并显示树宽与路径宽度在复杂度行为上存在罕见差异;同时与有界路径宽度上 MSO 已知需非初等依赖形成鲜明对比。

问题
Courcelle 定理中 FO/MSO 判定的复杂度对公式的依赖能否在自然受限图类上从非初等改进为初等。
方法
在 Gajarský 与 Hliněný 的有界树深元定理基础上推广,对有界路径宽度图给出判定 FO 可表达性质的算法/元定理,并分析其对公式规模的依赖。
评估
以理论复杂度证明进行评估,与树上 FO 的非初等下界以及有界路径宽度上 MSO 的非初等结果对比。
原文摘要(Abstract)

Courcelle's celebrated theorem states that all MSO-expressible properties can be decided in linear time on graphs of bounded treewidth. Unfortunately, the hidden constant implied by this theorem is a tower of exponentials whose height increases with each quantifier alternation in the formula. More devastatingly, this cannot be improved, under standard assumptions, even if we consider the much more restricted problem of deciding FO-expressible properties on trees. In this paper we revisit this well-studied topic and identify a natural special case where the dependence of Courcelle's theorem can, in fact, be improved. Specifically, we show that all FO-expressible properties can be decided with an elementary dependence on the input formula, if the input graph has bounded pathwidth (rather than treewidth). This is a rare example of treewidth and pathwidth having different complexity behaviors. Our result is also in sharp contrast with MSO logic on graphs of bounded pathwidth, where it is known that the dependence has to be non-elementary, under standard assumptions. Our work builds upon, and generalizes, a corresponding meta-theorem by Gajarský and Hliněný for the more restricted class of graphs of bounded tree-depth.

链接与引用

DOI 原文 · arXiv · PDF(开放获取) · DBLP

BibTeX
@article{Lampis23,
  title = {First Order Logic on Pathwidth Revisited Again},
  author = {Michael Lampis},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 22, Issue 2},
  year = {2026},
  doi = {10.46298/lmcs-22(2:26)2026}
}