The disjoint paths logic, FOL+DP, is an extension of First Order Logic (FOL) with the extra atomic predicate expressing the existence of internally vertex-disjoint paths between and for . This logic can express a wide variety of problems that escape the expressibility potential of FOL. We prove that for every minor-closed graph class, model-checking for FOL+DP can be done in quadratic time. We also introduce an extension of FOL+DP, namely the scattered disjoint paths logic, FOL+SDP, where we further consider the atomic predicate demanding that the disjoint paths are within distance bigger than some fixed value . Using the same technique we prove that model-checking for FOL+SDP can be done in quadratic time on classes of graphs with bounded Euler genus.
Joint work with Petr A. Golovach and Dimitrios M. Thilikos.