Recognizability equals monadic second-order definability for sets of graphs of bounded tree-width

Abstract

We prove that for each k, there exists a MSO-transduction that associates with every graph of tree-width at most k one of its tree-decompositions of width at most k. Courcelle proves in (The Monadic second-order logic of graphs, I: Recognizable sets of finite graphs) that every set of graphs is recognizable if it is definable in Counting Monadic Second-Order logic. It follows that every set of graphs of bounded tree-width is CMSO-definable if and only if it is recognizable. © 1998 Springer-Verlag.