Elementary first-order model checking for sparse graphs

TL;DR

This work characterizes when first-order model checking on monotone graph classes is elementarily fixed-parameter tractable by introducing and applying the notions of tree rank and elementary tree rank, based on r-subdivisions and shallow topological minors. The authors prove that classes with bounded elementary tree rank admit FO model checking with an elementary dependence on the formula size, and that excluding a fixed tree as a topological minor suffices to guarantee this tractability. They also establish a near-complete converse: if a monotone class admits elementarily-FPT FO model checking, it must have bounded tree rank; they further show that, on classes of bounded tree rank, every FO formula is equivalent to one with a bounded number of quantifier alternations (with the bound 3d), and, when elementary elementary-tree-rank is assumed, the equivalent formula size is elementary in the original size. The framework integrates a batched splitter game with Gaifman locality and interpretations to derive an elementary-FPT model-checking algorithm, while connecting to broader sparsity and transduction-based notions, and setting the stage for extensions to denser classes under a rank paradigm. Overall, the paper advances a structural/logic-parameterized frontier by linking tree-like decompositions, alternation hierarchies, and elementary growth bounds to FO model checking on restricted graph classes.

Abstract

It is known that for subgraph-closed graph classes the first-order model checking problem is fixed-parameter tractable if and only if the class is nowhere dense [Grohe, Kreutzer, Siebertz, STOC 2014]. However, the dependency on the formula size is non-elementary, and in fact, this is unavoidable even for the class of all trees [Frick and Grohe, LICS 2002]. On the other hand, it is known that the dependency is elementary for classes of bounded degree [Frick and Grohe, LICS 2002] as well as for classes of bounded pathwidth [Lampis, ICALP 2023]. In this paper we generalise these results and almost completely characterise subgraph-closed graph classes for which the model checking problem is fixed-parameter tractable with an elementary dependency on the formula size. Those are the graph classes for which there exists a number $d$ such that for every $r$, some tree of depth $d$ and size bounded by an elementary function of $r$ is avoided as an $({\leq} r)$-subdivision in all graphs in the class. In particular, this implies that if the class in question excludes a fixed tree as a topological minor, then first-order model checking for graphs in the class is fixed-parameter tractable with an elementary dependency on the formula size.

Figures (1)

• Figure 1: A forest of depth $3$ with two unary relations.

Theorems & Definitions (101)

• Definition 1
• Example 1
• Example 2
• Definition 2
• Theorem 3
• Corollary 4
• Theorem 5
• Theorem 6
• Theorem 7
• Example 3