再论路径宽度上的一阶逻辑
First Order Logic on Pathwidth Revisited Again
AI总结：
研究有界路径宽度图上一阶逻辑可表达性质的可判定性，证明其具有初等依赖，与树宽度情况形成对比。
摘要：
Courcelle 著名定理指出，所有 MSO 可表达的性质可以在有界树宽的图上在线性时间内判定。不幸的是，该定理隐含的常数是一个指数塔，其高度随公式中的量词交替次数增加。更糟糕的是，在标准假设下，即使考虑在树上判定 FO 可表达性质这个更受限的问题，也无法改进。本文重新审视这个被广泛研究的主题，并识别出一个自然特例，其中 Courcelle 定理的依赖关系实际上可以改进。具体来说，我们证明，如果输入图具有有界路径宽度（而非树宽度），则所有 FO 可表达的性质都可以用关于输入公式的初等依赖来判定。这是树宽度和路径宽度具有不同复杂度行为的一个罕见例子。我们的结果也与有界路径宽度图上的 MSO 逻辑形成鲜明对比，因为在标准假设下，已知后者的依赖必须是非初等的。我们的工作建立在 Gajarský 和 Hliněný 针对更受限的有界树深图类的相应元定理之上，并对其进行了推广。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
