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.

• Type: Conference
• Year: 2010
• Where: GG
• Authors: Barbara König, Javier Esparza
• Keywords: Certain Forbidden Graphs, Forbidden Graphs, GG 2010, Graph Transformation Systems, Theoretical Computer Science