Model Checking Disjoint-Paths Logic on Topological-Minor-Free Graph Classes

TL;DR

This paper proves that model checking for disjoint-paths logic extended with vertex-disjoint path predicates is fixed-parameter tractable on graph classes excluding a fixed topological minor, advancing understanding of logical properties on such graph classes.

Contribution

It establishes fixed-parameter tractability of model checking for FO+dp on topological-minor-free graph classes, resolving a key open problem in the area.

Findings

Model checking is FPT on topological-minor-free classes.

Hardness results for classes not excluding a topological minor.

Extends tractability results to a richer logic with disjoint-path predicates.

Abstract

Disjoint-paths logic, denoted $\mathsf{FO}$+$\mathsf{dp}$, extends first-order logic ($\mathsf{FO}$) with atomic predicates $\mathsf{dp}_r[(x_1,y_1),\ldots,(x_r,y_r)]$, expressing the existence of vertex-disjoint paths between $x_i$ and $y_i$, for $1\leq i\leq r$. We prove that for every graph class excluding some fixed graph as a topological minor, the model checking problem for $\mathsf{FO}$+$\mathsf{dp}$ is fixed-parameter tractable. This essentially settles the question of tractable model checking for this logic on subgraph-closed classes, since the problem is hard on subgraph-closed classes not excluding a topological minor (assuming a further mild condition of efficiency of encoding).