Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2023
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2302.07033 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910023650639872 |
|---|---|
| author | Schirrmacher, Nicole Siebertz, Sebastian Stamoulis, Giannos Thilikos, Dimitrios M. Vigny, Alexandre |
| author_facet | Schirrmacher, Nicole Siebertz, Sebastian Stamoulis, Giannos Thilikos, Dimitrios M. Vigny, Alexandre |
| contents | Disjoint-paths logic, denoted $\mathsf{FO}$+$\mathsf{dp}$, extends first-order logic ($\mathsf{FO}$) with atomic predicates $\mathsf{dp}_r[(x_1,y_1),\ldots,(x_r,y_r)]$, expressing the existence of vertex-disjoint paths between $x_i$ and $y_i$, for $1\leq i\leq r$. We prove that for every graph class excluding some fixed graph as a topological minor, the model checking problem for $\mathsf{FO}$+$\mathsf{dp}$ is fixed-parameter tractable. This 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 of efficiency of encoding). |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2302_07033 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Model Checking Disjoint-Paths Logic on Topological-Minor-Free Graph Classes Schirrmacher, Nicole Siebertz, Sebastian Stamoulis, Giannos Thilikos, Dimitrios M. Vigny, Alexandre Logic in Computer Science Disjoint-paths logic, denoted $\mathsf{FO}$+$\mathsf{dp}$, extends first-order logic ($\mathsf{FO}$) with atomic predicates $\mathsf{dp}_r[(x_1,y_1),\ldots,(x_r,y_r)]$, expressing the existence of vertex-disjoint paths between $x_i$ and $y_i$, for $1\leq i\leq r$. We prove that for every graph class excluding some fixed graph as a topological minor, the model checking problem for $\mathsf{FO}$+$\mathsf{dp}$ is fixed-parameter tractable. This 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 of efficiency of encoding). |
| title | Model Checking Disjoint-Paths Logic on Topological-Minor-Free Graph Classes |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2302.07033 |