Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Tree-Verifiable Graph Grammars

Mark Chimes, Radu Iosif, Florian Zuleger

TL;DR

The paper addresses extending the connection between regular word/tree languages and logical definability to graphs by introducing tree-verifiable graph grammars. It establishes that languages generated by these grammars are definable in $CMSO$ and have bounded embeddable tree-width, and proves a completeness result: every $CMSO$-definable graph language with bounded embeddable tree-width can be generated by a tree-verifiable grammar. This new class strictly generalizes Courcelle's regular graph grammars, providing a more expressive yet still tractable framework for graph languages at the intersection of $CMSO$-definability and HR-context-freeness. The work thereby yields a robust tool for graph-grammar-based reasoning with potential applications in static analysis and verification of graph-structured systems.

Abstract

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.

Tree-Verifiable Graph Grammars

TL;DR

The paper addresses extending the connection between regular word/tree languages and logical definability to graphs by introducing tree-verifiable graph grammars. It establishes that languages generated by these grammars are definable in and have bounded embeddable tree-width, and proves a completeness result: every -definable graph language with bounded embeddable tree-width can be generated by a tree-verifiable grammar. This new class strictly generalizes Courcelle's regular graph grammars, providing a more expressive yet still tractable framework for graph languages at the intersection of -definability and HR-context-freeness. The work thereby yields a robust tool for graph-grammar-based reasoning with potential applications in static analysis and verification of graph-structured systems.

Abstract

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.
Paper Structure (14 sections, 2 theorems, 31 equations, 7 figures)

This paper contains 14 sections, 2 theorems, 31 equations, 7 figures.

Table of Contents

  1. Introduction
  2. Our contributions
  3. Related work
  4. Preliminaries
  5. Graphs
  6. Graph Operations and Grammars.
  7. Monadic Second Order Logic with Counting
  8. Recognizable Sets of Graphs.
  9. Trees.
  10. Tree Grammars
  11. Tree Verifiable Graph-Grammars
  12. Comparison with Regular Graph Grammars
  13. Conclusions
  14. Proofs

Key Result

Theorem 1

Let $\mathcal{L}$ be a language of trees. Then, $\mathcal{L}$ is $\mathsf{CMSO}$-definable iff $\mathcal{L}$ is recognizable.

Figures (7)

  • Figure 1: Graph operations: substitution (a) parallel composition (b)
  • Figure 2: Graph Grammar for Trees with Linked Leaves
  • Figure 3: Monadic Second Order Logic with Counting ($\mathsf{CMSO}$)
  • Figure 4: Tree operations: substitution (a) parallel composition (b)
  • Figure 5: Tree-Verifiable Grammar for Trees with Linked Leaves
  • ...and 2 more figures

Theorems & Definitions (13)

  • Definition 1
  • Definition 2: Substitution
  • Example 1
  • Definition 3
  • Theorem 1: journals/iandc/Courcelle90
  • Definition 4
  • Example 2
  • Definition 5
  • Definition 6
  • Definition 7
  • ...and 3 more