The typical approach to proving Courcelle's theorem involves the construction of a finite bottom-up tree automaton that acts on the tree decompositions of the given graph [REF].
A tree decomposition of a given graph G consists of a tree and, for each tree node, a subset of the vertices of G called a bag.