Model-Checking for First-Order Logic with Disjoint Paths Predicates in Proper Minor-Closed Graph Classes
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2022
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909120590774272 |
|---|---|
| author | Golovach, Petr A. Stamoulis, Giannos Thilikos, Dimitrios M. |
| author_facet | Golovach, Petr A. Stamoulis, Giannos Thilikos, Dimitrios M. |
| contents | The disjoint paths logic, FOL+DP, is an extension of First-Order Logic (FOL) with the extra atomic predicate $\mathsf{dp}_k(x_1,y_1,\ldots,x_k,y_k),$ expressing the existence of internally vertex-disjoint paths between $x_i$ and $y_i,$ for $i\in\{1,\ldots, 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{\sf -sdp}_k(x_1,y_1,\ldots,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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2211_01723 |
| institution | arXiv |
| publishDate | 2022 |
| record_format | arxiv |
| spellingShingle | Model-Checking for First-Order Logic with Disjoint Paths Predicates in Proper Minor-Closed Graph Classes Golovach, Petr A. Stamoulis, Giannos Thilikos, Dimitrios M. Logic in Computer Science Data Structures and Algorithms Combinatorics 05C83, 05C85, 68R10, 68W01, 68Q19, 03C13, 68Q25, 68Q27 F.2.2; G.2.2; F.4.1 The disjoint paths logic, FOL+DP, is an extension of First-Order Logic (FOL) with the extra atomic predicate $\mathsf{dp}_k(x_1,y_1,\ldots,x_k,y_k),$ expressing the existence of internally vertex-disjoint paths between $x_i$ and $y_i,$ for $i\in\{1,\ldots, 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{\sf -sdp}_k(x_1,y_1,\ldots,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. |
| title | Model-Checking for First-Order Logic with Disjoint Paths Predicates in Proper Minor-Closed Graph Classes |
| topic | Logic in Computer Science Data Structures and Algorithms Combinatorics 05C83, 05C85, 68R10, 68W01, 68Q19, 03C13, 68Q25, 68Q27 F.2.2; G.2.2; F.4.1 |
| url | https://arxiv.org/abs/2211.01723 |