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

Petr A. Golovach; Giannos Stamoulis; Dimitrios M. Thilikos

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

Petr A. Golovach, Giannos Stamoulis, Dimitrios M. Thilikos

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

The disjoint paths logic, FOL+DP, is an extension of First-Order Logic (FOL) with the extra atomic predicate dp_k(x₁, y₁, ..., 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₁, y₁, ..., 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.

Original language	English (US)
Title of host publication	34th Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2023
Publisher	Association for Computing Machinery
Pages	3684-3699
Number of pages	16
ISBN (Electronic)	9781611977554
State	Published - 2023
Event	34th Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2023 - Florence, Italy Duration: Jan 22 2023 → Jan 25 2023

Publication series

Name	Proceedings of the Annual ACM-SIAM Symposium on Discrete Algorithms
Volume	2023-January

Conference

Conference	34th Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2023
Country/Territory	Italy
City	Florence
Period	1/22/23 → 1/25/23

Keywords

Algorithmic meta-theorems
Disjoint paths
First-order logic
Graph minors
Hadwiger number
Irrelevant vertex technique
Model-checking

ASJC Scopus subject areas

Software
General Mathematics

Cite this

Golovach, P. A., Stamoulis, G., & Thilikos, D. M. (2023). Model-Checking for First-Order Logic with Disjoint Paths Predicates in Proper Minor-Closed Graph Classes. In 34th Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2023 (pp. 3684-3699). (Proceedings of the Annual ACM-SIAM Symposium on Discrete Algorithms; Vol. 2023-January). Association for Computing Machinery.

Model-Checking for First-Order Logic with Disjoint Paths Predicates in Proper Minor-Closed Graph Classes. / Golovach, Petr A.; Stamoulis, Giannos; Thilikos, Dimitrios M.
34th Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2023. Association for Computing Machinery, 2023. p. 3684-3699 (Proceedings of the Annual ACM-SIAM Symposium on Discrete Algorithms; Vol. 2023-January).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Golovach, PA, Stamoulis, G & Thilikos, DM 2023, Model-Checking for First-Order Logic with Disjoint Paths Predicates in Proper Minor-Closed Graph Classes. in 34th Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2023. Proceedings of the Annual ACM-SIAM Symposium on Discrete Algorithms, vol. 2023-January, Association for Computing Machinery, pp. 3684-3699, 34th Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2023, Florence, Italy, 1/22/23.

@inproceedings{19e2e424a1704299a4068a97b821655b,

title = "Model-Checking for First-Order Logic with Disjoint Paths Predicates in Proper Minor-Closed Graph Classes",

abstract = "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.",

keywords = "Algorithmic meta-theorems, Disjoint paths, First-order logic, Graph minors, Hadwiger number, Irrelevant vertex technique, Model-checking",

author = "Golovach, {Petr A.} and Giannos Stamoulis and Thilikos, {Dimitrios M.}",

note = "Publisher Copyright: Copyright {\textcopyright} 2023 by SIAM.; 34th Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2023 ; Conference date: 22-01-2023 Through 25-01-2023",

year = "2023",

language = "English (US)",

series = "Proceedings of the Annual ACM-SIAM Symposium on Discrete Algorithms",

publisher = "Association for Computing Machinery",

pages = "3684--3699",

booktitle = "34th Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2023",

}

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.

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 -

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

Abstract

Publication series

Conference

Keywords

ASJC Scopus subject areas

Other files and links

Fingerprint

Cite this