Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Maintaining $\mathsf{CMSO}_2$ properties on dynamic structures with bounded feedback vertex number

Konrad Majewski, Michał Pilipczuk, Marek Sokołowski

TL;DR

This work develops dynamic data-structure techniques to maintain satisfaction of CMSO$_2$ properties on graphs and relational structures with a bounded feedback vertex number. The core methodology combines fern decompositions, top-trees, and a Replacement Lemma to reduce global CMSO$_2$ satisfaction to finite, composable local types on boundaried substructures, enabling polylogarithmic update times under the fvs promise. Key contributions include the Contraction Lemma (dynamic fern-based contraction and ensemble contraction), the Downgrade Lemma (controlled reduction of the graph while preserving logical information), and an augmentation framework extending the results to relational structures and to Erdős–Pósa cycle packing. Collectively, these results advance fully dynamic maintenance of expressive graph properties expressible in CMSO$_2$, with concrete implications for parameterized dynamic problems on graphs of bounded feedback vertex number and related structural parameters.

Abstract

Let $\varphi$ be a sentence of $\mathsf{CMSO}_2$ (monadic second-order logic with quantification over edge subsets and counting modular predicates) over the signature of graphs. We present a dynamic data structure that for a given graph $G$ that is updated by edge insertions and edge deletions, maintains whether $\varphi$ is satisfied in $G$. The data structure is required to correctly report the outcome only when the feedback vertex number of $G$ does not exceed a fixed constant $k$, otherwise it reports that the feedback vertex number is too large. With this assumption, we guarantee amortized update time ${\cal O}_{\varphi,k}(\log n)$. If we additionally assume that the feedback vertex number of $G$ never exceeds $k$, this update time guarantee is worst-case. By combining this result with a classic theorem of Erdős and Pósa, we give a fully dynamic data structure that maintains whether a graph contains a packing of $k$ vertex-disjoint cycles with amortized update time ${\cal O}_{k}(\log n)$. Our data structure also works in a larger generality of relational structures over binary signatures.

Maintaining $\mathsf{CMSO}_2$ properties on dynamic structures with bounded feedback vertex number

TL;DR

This work develops dynamic data-structure techniques to maintain satisfaction of CMSO properties on graphs and relational structures with a bounded feedback vertex number. The core methodology combines fern decompositions, top-trees, and a Replacement Lemma to reduce global CMSO satisfaction to finite, composable local types on boundaried substructures, enabling polylogarithmic update times under the fvs promise. Key contributions include the Contraction Lemma (dynamic fern-based contraction and ensemble contraction), the Downgrade Lemma (controlled reduction of the graph while preserving logical information), and an augmentation framework extending the results to relational structures and to Erdős–Pósa cycle packing. Collectively, these results advance fully dynamic maintenance of expressive graph properties expressible in CMSO, with concrete implications for parameterized dynamic problems on graphs of bounded feedback vertex number and related structural parameters.

Abstract

Let be a sentence of (monadic second-order logic with quantification over edge subsets and counting modular predicates) over the signature of graphs. We present a dynamic data structure that for a given graph that is updated by edge insertions and edge deletions, maintains whether is satisfied in . The data structure is required to correctly report the outcome only when the feedback vertex number of does not exceed a fixed constant , otherwise it reports that the feedback vertex number is too large. With this assumption, we guarantee amortized update time . If we additionally assume that the feedback vertex number of never exceeds , this update time guarantee is worst-case. By combining this result with a classic theorem of Erdős and Pósa, we give a fully dynamic data structure that maintains whether a graph contains a packing of vertex-disjoint cycles with amortized update time . Our data structure also works in a larger generality of relational structures over binary signatures.

Paper Structure

This paper contains 19 sections, 44 theorems, 47 equations, 5 figures.

Table of Contents

  1. Introduction
  2. Overview
  3. Preliminaries
  4. Relational structures and logic
  5. Top trees
  6. Auxiliary information.
  7. Substructures of $\mathbb{A}$.
  8. Deducing information on almost induced substructures.
  9. Statement of the main result and proof strategy
  10. Proof strategy for Theorem \ref{['thm:efficient_augmented_structure']}.
  11. Reduction from Theorem \ref{['thm:main_theorem']} to Theorem \ref{['thm:efficient_augmented_structure']}.
  12. Contraction Lemma
  13. Fern decomposition
  14. Static variant of the Contraction Lemma
  15. Dynamic maintenance of fern decomposition
  16. ...and 4 more sections

Key Result

Theorem 1.1

Given an $\mathsf{MSO}_2$ sentence $\varphi$ over the signature of graphs and $d\in \mathbb{N}$, one can construct a dynamic data structure that maintains whether a given dynamic graph $G$ satisfies $\varphi$. The data structure is obliged to report a correct answer only when the treedepth of $G$ do

Figures (5)

  • Figure 1: Left: A graph $G$ together with its fern decomposition. Different ferns are depicted with different colors; these should not be confused with the coloring of edges of $G$ with colors from $\Sigma$. Right: The multigraph $\mathsf{Contract}(G)$ obtained by contracting each fern. Note that in the construction of $\mathsf{Contract}^p(G)$ described in the discussion of the Contraction Lemma, we would not have parallel edges or loops. Instead, each pack of parallel edges would be replaced by a single one, colored with the joint type of the whole pack. Similarly, loops on a vertex would be removed and their joint type would be stored in the color of the vertex.
  • Figure 2: An example top tree $\Delta_T$. Clusters correspond to light gray ovals. Boundary vertices in each cluster are marked dark gray. Note that in this example, $\Delta_T$ has two external boundary vertices. However, it may have fewer (zero or one) such vertices.
  • Figure 3: A cyclic fern $S$ with empty boundary and a boundaried tree $T$ representing $S$. Here, we have $\partial T = \{ x_1, x_1' \}$ and we set $\textsf{name}(x_i) = u_i$ and $\textsf{name}(x_1') = u_1$ (and the corresponding subtrees of $S$ and $T$ are mapped to each other). Note that, by definition, at least one of the vertices $x_1$ and $x_1'$ must be a leaf of $T$.
  • Figure 4: The effect of applying $\textsf{makeEssential}(x, y_1, y_2, y_3)$.
  • Figure 5: Adding a loop at a vertex $u$ to a fern $S_u$ which is: (a) a unicyclic graph of empty boundary, (b) a tree fern of boundary $\partial S_u = \{ v \}$, (c) a tree fern of boundary $\partial S_u = \{ v_1, v_2 \}$. Empty vertices denote essential vertices of $H$, and red elements: { , } denote vertices and edges of $H$ which become essential in $H^{\mathrm{add}}$.

Theorems & Definitions (119)

  • Theorem 1.1: DvorakKT14ChenCDFHNPPSWZ21
  • Theorem 1.2
  • Theorem 1.3
  • Theorem 1.4
  • proof
  • Theorem 1.5
  • proof
  • Theorem 1.6: DBLP:conf/focs/KorhonenMNP023
  • Theorem 2.1: folklore
  • Lemma 2.2: folklore
  • ...and 109 more