Merge-width and First-Order Model Checking
Jan Dreier, Szymon Toru\'nczyk

TL;DR
This paper introduces merge-width, a new graph parameter unifying several existing measures, and proves that first-order model checking is fixed-parameter tractable on classes of graphs with bounded merge-width.
Contribution
The paper defines merge-width, unifies multiple graph parameters, and establishes fixed-parameter tractability of first-order model checking for graphs with bounded merge-width.
Findings
Merge-width unifies treewidth, degeneracy, twin-width, clique-width, and coloring numbers.
Graph classes of bounded merge-width include those of bounded expansion and twin-width.
First-order model checking is fixed-parameter tractable on classes of bounded merge-width.
Abstract
We introduce merge-width, a family of graph parameters that unifies several structural graph measures, including treewidth, degeneracy, twin-width, clique-width, and generalized coloring numbers. Our parameters are based on new decompositions called construction sequences. These are sequences of ever coarser partitions of the vertex set, where each pair of parts has a specified default connection, and all vertex pairs of the graph that differ from the default are marked as resolved. The radius- merge-width is the maximum number of parts reached from a vertex by following a path of at most resolved edges. Graph classes of bounded merge-width -- for which the radius- merge-width parameter can be bounded by a constant, for each fixed -- include all classes of bounded expansion or of bounded twin-width, thus unifying two central notions from the Sparsity and…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Model-Driven Software Engineering Techniques
