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-decopositios of width at most k. Courcelle proves in (The Monadicsecond-order logicof 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 its is recognizable.
展开▼