Successor-Invariant First-Order Logic on Graphs with Excluded Topological Subgraphs

TL;DR

This paper proves that model-checking for successor-invariant and order-invariant first-order logic is fixed-parameter tractable on certain classes of graphs and posets, extending previous results and narrowing the gap between FO and successor-invariant FO.

Contribution

It extends fixed-parameter tractability results for successor-invariant FO to graphs with excluded topological subgraphs and for order-invariant FO on bounded width posets.

Findings

Model-checking for successor-invariant FO is fixed-parameter tractable on graphs with excluded topological subgraphs.

Model-checking for order-invariant FO is tractable on coloured posets of bounded width.

The results extend previous work on planar graphs and graphs with excluded minors.

Abstract

We show that the model-checking problem for successor-invariant first-order logic is fixed-parameter tractable on graphs with excluded topological subgraphs when parameterised by both the size of the input formula and the size of the exluded topological subgraph. Furthermore, we show that model-checking for order-invariant first-order logic is tractable on coloured posets of bounded width, parameterised by both the size of the input formula and the width of the poset. Our result for successor-invariant FO extends previous results for this logic on planar graphs (Engelmann et al., LICS 2012) and graphs with excluded minors (Eickmeyer et al., LICS 2013), further narrowing the gap between what is known for FO and what is known for successor-invariant FO. The proof uses Grohe and Marx's structure theorem for graphs with excluded topological subgraphs. For order-invariant FO we show that Gajarsk\'y et al.'s recent result for FO carries over to order-invariant FO.