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

Disjoint-paths logic, denoted FO+DP, extends first-order logic (FO) with atomic predicates dp_k[(x_1, y_1),…,(x_k, y_k)], expressing the existence of internally vertex-disjoint paths between x_i and y_i, for 1 ≤ i ≤ k. In this talk, we first show how to prove (fixed-parameter) tractability of the model checking problem for FO+DP on graph classes excluding some fixed graph as a minor. Then, we sketch how to extend this tractability result to graph classes excluding some fixed graph as a *topological* minor. The latter settles the question of tractable model checking for this logic on subgraph-closed graph classes. Joint work with Petr A. Golovach and Dimitrios M. Thilikos and Nicole Schirrmacher, Sebastian Siebertz, Dimitrios M. Thilikos, and Alexandre Vigny.