Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

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

TL;DR

The paper proves that FO+dp model checking is fixed-parameter tractable on graph classes excluding a fixed graph as a topological minor, with running time $f(H,\varphi)\cdot |V(G)|^{3}$ and the ability to output a witnessing tuple when a formula is satisfied. The approach blends a decomposition into unbreakable parts, a collapse of FO+dp to FO on dense parts via a generic folio lemma, and a Feferman–Vaught-style dynamic programming over tree decompositions, supported by boundaried-graph representations and extended folios. Key technical contributions include a robust notion of annotated types, representative preservation under gluing, and a modular DP that handles both large clique-minor regions and minor-excluding parts. The results advance the frontier of tractable model checking for non-local logics on structured graph classes and open avenues for CMSO extensions and preprocessing-based query answering. Overall, the work tightly integrates graph-minor theory with logic-based decomposability to achieve uniform, constructive FPT algorithms for FO+dp in topological-minor-free classes, with further implications for related algorithmic meta-theorems.

Abstract

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).

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

TL;DR

The paper proves that FO+dp model checking is fixed-parameter tractable on graph classes excluding a fixed graph as a topological minor, with running time and the ability to output a witnessing tuple when a formula is satisfied. The approach blends a decomposition into unbreakable parts, a collapse of FO+dp to FO on dense parts via a generic folio lemma, and a Feferman–Vaught-style dynamic programming over tree decompositions, supported by boundaried-graph representations and extended folios. Key technical contributions include a robust notion of annotated types, representative preservation under gluing, and a modular DP that handles both large clique-minor regions and minor-excluding parts. The results advance the frontier of tractable model checking for non-local logics on structured graph classes and open avenues for CMSO extensions and preprocessing-based query answering. Overall, the work tightly integrates graph-minor theory with logic-based decomposability to achieve uniform, constructive FPT algorithms for FO+dp in topological-minor-free classes, with further implications for related algorithmic meta-theorems.

Abstract

Disjoint-paths logic, denoted +, extends first-order logic () with atomic predicates , expressing the existence of vertex-disjoint paths between and , for . We prove that for every graph class excluding some fixed graph as a topological minor, the model checking problem for + 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).
Paper Structure (44 sections, 20 theorems, 35 equations, 1 figure)

This paper contains 44 sections, 20 theorems, 35 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Our results
  3. Our techniques
  4. Follow-up work
  5. Organization
  6. Preliminaries
  7. Graphs
  8. Graphs
  9. Disjoint paths
  10. Trees and tree orders
  11. Minors and topological minors
  12. Tree decompositions
  13. Unbreakability
  14. Signatures and Logic
  15. Colored graph signatures
  16. ...and 29 more sections

Key Result

Theorem 1.1

There is an algorithm that, given a graph $G$ (with additional vertex colors) that excludes a graph $H$ as a topological minor, and an $\mathsf{FO}\space\raisebox{-0.3pt}{+}\space\mathsf{dp}\xspace$ formula $\varphi(\bar{x})$ (over the colored graph vocabulary), decides whether $G\models \exists \ba

Figures (1)

  • Figure 1: For a tight star decomposition of a graph $G$, we depict the concepts defined in \ref{['lem:combinatorial-collapse-unbreakable']}. Here, the partition is $\mathcal{C}:=\{\{x_1,x_7,y_3\},\{x_2\},\ldots,\{x_9,y_1,y_5\}\}$, and for each $C\in\mathcal{C}$ and a separation $(X_C,Y_C)$, we represent $S_C=X_{C}\cap Y_{C}$ with $X_C$ being the small part, we have $D_C$ as the union of the (small) connected components of $G\setminus S_C$ that contain a vertex of $C$.

Theorems & Definitions (33)

  • Theorem 1.1
  • Definition 2.1
  • Theorem 2.2: cygan2019minimum
  • Proposition 2.3: Lemma 2.2 and Theorem 3.1 of grohe2011finding
  • Proposition 3.1: Lemma 5.4 of robertson1995graph
  • Lemma 3.2
  • proof
  • Claim 1
  • Claim 2
  • Corollary 3.3
  • ...and 23 more