Abstract

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. The formulas of FO+DP can be expressed in monadic second-order logic (MSO) and can capture problems that are not definable in FO. We first 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, since the problem is hard on subgraph-closed classes not excluding a topological minor (assuming a further mild condition of efficiency of encoding).

Joint work with Petr A. Golovach and Dimitrios M. Thilikos and Nicole Schirrmacher, Sebastian Siebertz, Dimitrios M. Thilikos, and Alexandre Vigny.