Model Checking Disjoint-Paths Logic on Topological-Minor-Free Graph Classes

Nicole Schirrmacher; Sebastian Siebertz; Giannos Stamoulis; Dimitrios M. Thilikos; Alexandre Vigny

doi:10.1145/3661814.3662089

Model Checking Disjoint-Paths Logic on Topological-Minor-Free Graph Classes

Nicole Schirrmacher, Sebastian Siebertz, Giannos Stamoulis, Dimitrios M. Thilikos, Alexandre Vigny

Computer Science

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

Abstract

Disjoint-paths logic, denoted FO+ DP, extends first-order logic (FO) with atomic predicates dp_k[(x₁, y₁), ..., (x_k, y_k)], expressing the existence of internally vertex-disjoint paths between x_i and y_i, for 1 ≤ i ≤ k. We prove that for every graph class excluding some fixed graph as a topological minor, the model checking problem for FO+ DP is fixed-parameter tractable. This extends the model checking algorithm of Golovach et al. [SODA 2023] for FO+ DP for minor-closed graph classes. It also essentially settles the question of tractable model checking for this logic on subgraph-closed classes, since the problem is hard on subgraph-closed classes not excluding a topological minor (assuming a further mild condition on efficiency of encoding).

Original language	English (US)
Title of host publication	Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science
Publisher	Institute of Electrical and Electronics Engineers Inc.
ISBN (Electronic)	9798400706608
DOIs	https://doi.org/10.1145/3661814.3662089
State	Published - Jul 8 2024
Event	39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2024 - Tallinn, Estonia Duration: Jul 8 2024 → Jul 11 2024

Publication series

Name	Proceedings - Symposium on Logic in Computer Science
ISSN (Print)	1043-6871

Conference

Conference	39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2024
Country/Territory	Estonia
City	Tallinn
Period	7/8/24 → 7/11/24

Keywords

disjoint paths
first-order logic
model checking
parameterized algorithms
topological-minor-free graphs

ASJC Scopus subject areas

Software
General Mathematics

Access to Document

10.1145/3661814.3662089

Cite this

Schirrmacher, N., Siebertz, S., Stamoulis, G., Thilikos, D. M., & Vigny, A. (2024). Model Checking Disjoint-Paths Logic on Topological-Minor-Free Graph Classes. In Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science Article 68 (Proceedings - Symposium on Logic in Computer Science). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1145/3661814.3662089

Model Checking Disjoint-Paths Logic on Topological-Minor-Free Graph Classes. / Schirrmacher, Nicole; Siebertz, Sebastian; Stamoulis, Giannos et al.
Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science. Institute of Electrical and Electronics Engineers Inc., 2024. 68 (Proceedings - Symposium on Logic in Computer Science).

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

Schirrmacher, N, Siebertz, S, Stamoulis, G, Thilikos, DM & Vigny, A 2024, Model Checking Disjoint-Paths Logic on Topological-Minor-Free Graph Classes. in Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science., 68, Proceedings - Symposium on Logic in Computer Science, Institute of Electrical and Electronics Engineers Inc., 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2024, Tallinn, Estonia, 7/8/24. https://doi.org/10.1145/3661814.3662089

Schirrmacher N, Siebertz S, Stamoulis G, Thilikos DM, Vigny A. Model Checking Disjoint-Paths Logic on Topological-Minor-Free Graph Classes. In Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science. Institute of Electrical and Electronics Engineers Inc. 2024. 68. (Proceedings - Symposium on Logic in Computer Science). doi: 10.1145/3661814.3662089

@inproceedings{d7cc0673a6b64eb6a7aee6b546035f54,

title = "Model Checking Disjoint-Paths Logic on Topological-Minor-Free Graph Classes",

abstract = "Disjoint-paths logic, denoted FO+ DP, extends first-order logic (FO) with atomic predicates dpk[(x1, y1), ..., (xk, yk)], expressing the existence of internally vertex-disjoint paths between xi and yi, for 1 ≤ i ≤ k. We prove that for every graph class excluding some fixed graph as a topological minor, the model checking problem for FO+ DP is fixed-parameter tractable. This extends the model checking algorithm of Golovach et al. [SODA 2023] for FO+ DP for minor-closed graph classes. It also essentially settles the question of tractable model checking for this logic on subgraph-closed classes, since the problem is hard on subgraph-closed classes not excluding a topological minor (assuming a further mild condition on efficiency of encoding).",

keywords = "disjoint paths, first-order logic, model checking, parameterized algorithms, topological-minor-free graphs",

author = "Nicole Schirrmacher and Sebastian Siebertz and Giannos Stamoulis and Thilikos, {Dimitrios M.} and Alexandre Vigny",

note = "Publisher Copyright: {\textcopyright} 2024 Institute of Electrical and Electronics Engineers Inc.. All rights reserved.; 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2024 ; Conference date: 08-07-2024 Through 11-07-2024",

year = "2024",

month = jul,

day = "8",

doi = "10.1145/3661814.3662089",

language = "English (US)",

series = "Proceedings - Symposium on Logic in Computer Science",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

booktitle = "Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science",

}

TY - GEN

T1 - Model Checking Disjoint-Paths Logic on Topological-Minor-Free Graph Classes

AU - Schirrmacher, Nicole

AU - Siebertz, Sebastian

AU - Stamoulis, Giannos

AU - Thilikos, Dimitrios M.

AU - Vigny, Alexandre

PY - 2024/7/8

Y1 - 2024/7/8

N2 - Disjoint-paths logic, denoted FO+ DP, extends first-order logic (FO) with atomic predicates dpk[(x1, y1), ..., (xk, yk)], expressing the existence of internally vertex-disjoint paths between xi and yi, for 1 ≤ i ≤ k. We prove that for every graph class excluding some fixed graph as a topological minor, the model checking problem for FO+ DP is fixed-parameter tractable. This extends the model checking algorithm of Golovach et al. [SODA 2023] for FO+ DP for minor-closed graph classes. It also essentially settles the question of tractable model checking for this logic on subgraph-closed classes, since the problem is hard on subgraph-closed classes not excluding a topological minor (assuming a further mild condition on efficiency of encoding).

AB - Disjoint-paths logic, denoted FO+ DP, extends first-order logic (FO) with atomic predicates dpk[(x1, y1), ..., (xk, yk)], expressing the existence of internally vertex-disjoint paths between xi and yi, for 1 ≤ i ≤ k. We prove that for every graph class excluding some fixed graph as a topological minor, the model checking problem for FO+ DP is fixed-parameter tractable. This extends the model checking algorithm of Golovach et al. [SODA 2023] for FO+ DP for minor-closed graph classes. It also essentially settles the question of tractable model checking for this logic on subgraph-closed classes, since the problem is hard on subgraph-closed classes not excluding a topological minor (assuming a further mild condition on efficiency of encoding).

KW - disjoint paths

KW - first-order logic

KW - model checking

KW - parameterized algorithms

KW - topological-minor-free graphs

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

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

U2 - 10.1145/3661814.3662089

DO - 10.1145/3661814.3662089

M3 - Conference contribution

AN - SCOPUS:85198153158

T3 - Proceedings - Symposium on Logic in Computer Science

BT - Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science

PB - Institute of Electrical and Electronics Engineers Inc.

T2 - 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2024

Y2 - 8 July 2024 through 11 July 2024

ER -

Model Checking Disjoint-Paths Logic on Topological-Minor-Free Graph Classes

Abstract

Publication series

Conference

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this