Hyperedge-Replacement grammars (HR) have been introduced by Courcelle in order to extend the notion of context-free sets from words and trees to graphs of bounded tree-width. While for words and trees the syntactic restrictions that guarantee that the associated languages of words resp. trees are regular - and hence, MSO-definable - are known, the situation is far more complicated for graphs. Here, Courcelle proposed the notion of regular graph grammars, a syntactic restriction of HR grammars that guarantees the definability of the associated languages of graphs in Counting Monadic Second Order Logic (CMSO). However, these grammars are not complete in the sense that not every CMSO-definable set of graphs of bounded tree-width can be generated by a regular graph grammar. In this paper, we introduce a new syntactic restriction of HR grammars, called tree-verifiable graph grammars, and a new notion of bounded tree-width, called embeddable bounded tree-width, where the later restricts the trees of a tree-decomposition to be a subgraph of the analyzed graph. The main property of tree-verifiable graph grammars is that their associated languages are CMSO-definable and that the have bounded embeddable tree-width. We show further that they strictly generalize the regular graph grammars of Courcelle. Finally, we establish a completeness result, showing that every language of graphs that is CMSO-definable and of bounded embeddable tree-width can be generated by a tree-verifiable graph grammar.

翻译：超边替换文法（HR）由Courcelle提出，旨在将上下文无关集的概念从词和树扩展到具有有界树宽的图。尽管对于词和树，已知保证对应的词语言或树语言是正则的（即MSO可定义）的句法限制，但图的情况则复杂得多。为此，Courcelle提出了正则图文法的概念，这种HR文法的句法限制保证了相关图语言在计数单子二阶逻辑（CMSO）中的可定义性。然而，这些文法并不完备——并非所有具有有界树宽的CMSO可定义图集都能由正则图文法生成。本文提出了一种新的HR文法的句法限制，称为树可验证图文法，以及一种新的有界树宽概念，称为可嵌入有界树宽，后者要求树分解中的树是待分析图的子图。树可验证图文法的主要性质是：其关联的图语言是CMSO可定义的，且具有有界可嵌入树宽。我们还进一步证明，它们严格推广了Courcelle的正则图文法。最后，我们建立了一个完备性结果：每个CMSO可定义且具有有界可嵌入树宽的图语言，都能由树可验证图文法生成。