Sciweavers

Share
GG
2010
Springer

Verification of Graph Transformation Systems with Context-Free Specifications

11 years 10 months ago
Verification of Graph Transformation Systems with Context-Free Specifications
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 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.
Barbara König, Javier Esparza
Added 07 Dec 2010
Updated 07 Dec 2010
Type Conference
Year 2010
Where GG
Authors Barbara König, Javier Esparza
Comments (0)
books