TY - GEN

T1 - Model-Checking for First-Order Logic with Disjoint Paths Predicates in Proper Minor-Closed Graph Classes

AU - Golovach, Petr A.

AU - Stamoulis, Giannos

AU - Thilikos, Dimitrios M.

N1 - Publisher Copyright:
Copyright © 2023 by SIAM.

PY - 2023

Y1 - 2023

N2 - The disjoint paths logic, FOL+DP, is an extension of First-Order Logic (FOL) with the extra atomic predicate dpk(x1, y1, ..., xk, yk), expressing the existence of internally vertex-disjoint paths between xi and yi, 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-sdpk(x1, y1, ..., xk, yk), 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.

AB - The disjoint paths logic, FOL+DP, is an extension of First-Order Logic (FOL) with the extra atomic predicate dpk(x1, y1, ..., xk, yk), expressing the existence of internally vertex-disjoint paths between xi and yi, 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-sdpk(x1, y1, ..., xk, yk), 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.

KW - Algorithmic meta-theorems

KW - Disjoint paths

KW - First-order logic

KW - Graph minors

KW - Hadwiger number

KW - Irrelevant vertex technique

KW - Model-checking

UR - http://www.scopus.com/inward/record.url?scp=85170058470&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85170058470&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:85170058470

T3 - Proceedings of the Annual ACM-SIAM Symposium on Discrete Algorithms

SP - 3684

EP - 3699

BT - 34th Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2023

PB - Association for Computing Machinery

T2 - 34th Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2023

Y2 - 22 January 2023 through 25 January 2023

ER -