The monadic second-order logic of graphs V: on closing the gap between definability and recognizability

AbstractContext-free graph-grammars are considered such that, in every generated graph G, a derivation tree of G can be constructed by means of monadic second-order formulas that specify its nodes, its labels, the successors of a node etc. A subset of the set of graphs generated by such a grammar is recognizable iff it is definable in monadic second-order logic, whereas, in general, only the “if” direction holds