Reference:
B König and J. Esparza. Verification of graph transformation systems with contextfree 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 contextfree 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 contextfree grammar is semilinear. An important application is deadlock analysis for interaction nets and we specifically show how to apply the technique to an infinitestate 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 ContextFree Specifications},
year = {2010}
}
