Model-Checking for First-Order Logic with Disjoint Paths Predicates in Proper Minor-Closed Graph Classes
share
The disjoint paths logic, FOL+DP, is an extension of First-Order Logic (FOL) with the extra atomic predicate 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 i∈{1,…, k}. This logic can express a wide variety of problems that escape the expressibility potential of FOL. We prove that for every proper 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 s -sdp_k(x_1,y_1,…,x_k,y_k), demanding that the disjoint paths are within distance bigger than some fixed value s. 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.
READ FULL TEXT