The monadic second-order logic of graphs. V: On closing the gap between definability and recognizability (Q1176232)

This is the fifth in an ambitious series of papers exploring the possibilities of monadic second-order logic (MSOL) as a language for expressing properties of finite labelled hypergraphs (called simply graphs). The central theme is the relationship between recognizability and MSO definability. The starting point is J. R. Büchi's classical theorem which states that a string language is recognizable iff it is MSO definable. This result extends to tree languages, but for graphs just one half of it holds: MSO definable sets of graphs are recognizable. The author focuses on the converse implication. He conjectures that it would hold for graphs with bounded tree-width. He also notes the lack of a suitable notion of an automaton that would serve as an intermediate between congruences, in terms of which recognizability is defined, and MSO-formulas. However, if the graphs are generated by a context-free graph grammar, the derivation trees serve as structures that can be read by an automaton in a meaningful way. The main result states that for graph languages generated by so-called MSO parsable CF graph grammars, recognizability implies MSO definability. The paper contains also several further related notions, results and conjectures. For Part IV see [\textit{B. Courcelle}, Ann. Pure Appl. Logic 49, No. 3, 193--255 (1990; Zbl 0731.03006)].