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

Disjoint-paths logic, denoted $\mathsf{F}\mathsf{O}$+$\mathsf{d}\mathsf{p}$, extends first-order logic ($\mathsf{F}\mathsf{O}$) with atomic predicates ${\mathsf{d}\mathsf{p}}_r[(x_1,y_1),\dots ,(x_r,y_r)]$, expressing the existence of vertex-disjoint paths between $x_i$ and $y_i$, for $1\le i\le r$. We prove that for every graph class excluding some fixed graph as a topological minor, the model checking problem for $\mathsf{F}\mathsf{O}$+$\mathsf{d}\mathsf{p}$ 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).