Definability equals recognizability for graphs of bounded treewidth

TL;DR

This paper proves a conjecture by Courcelle, establishing an equivalence between definability in MSO logic with modular counting and recognizability via tree automata for graphs of bounded treewidth, thus completing a key theoretical link.

Contribution

It proves the long-standing conjecture that definability and recognizability are equivalent for properties of graphs with bounded treewidth, confirming a fundamental theoretical connection.

Findings

Proves the equivalence between MSO definability and recognizability for bounded treewidth graphs

Completes the proof of Courcelle's conjecture

Strengthens the theoretical foundation of graph property analysis

Abstract

We prove a conjecture of Courcelle, which states that a graph property is definable in MSO with modular counting predicates on graphs of constant treewidth if, and only if it is recognizable in the following sense: constant-width tree decompositions of graphs satisfying the property can be recognized by tree automata. While the forward implication is a classic fact known as Courcelle's theorem, the converse direction remained open