First Order Logic on Pathwidth Revisited Again

TL;DR

This paper shows that first-order logic properties can be decided more efficiently on graphs with bounded pathwidth than on those with bounded treewidth, contrasting with known results for MSO logic.

Contribution

It identifies a special case where the complexity dependence for FO logic on graphs with bounded pathwidth is elementary, unlike the non-elementary dependence for MSO logic.

Findings

FO properties decidable with elementary dependence on formula on graphs of bounded pathwidth

Contrasts with non-elementary dependence for MSO logic on similar graphs

Highlights different complexity behaviors of treewidth and pathwidth

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{\'{y}} and Hlin{\v{e}}n{\'{y}} for the more restricted class of graphs of bounded tree-depth.