Reference:

B König and J. Esparza. Verification of graph transformation systems with context-free specifications. In Proc. of the 5th International Conference on Graph Transformations, 2010.

Abstract:

We introduce an analysis method for graph transformation systems which checks that certain forbidden graphs are not reachable from the start graph. These forbidden graphs are specified by a context-free graph grammar. The technique is based on the approximation of graph transformation systems by Petri nets and on semilinear sets of markings. Especially we exploit Parikh's theorem which says that the Parikh image of a context-free grammar is semilinear. An important application is deadlock analysis for interaction nets and we specifically show how to apply the technique to an infinite-state dining philosopher's system.

Suggested BibTeX entry:

@inproceedings{KE10,
    author = {B K\"onig and J. Esparza},
    booktitle = {Proc. of the 5th International Conference on Graph Transformations},
    title = {Verification of Graph Transformation Systems with Context-Free Specifications},
    year = {2010}
}