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. © 2010 Springer-Verlag.
Cite
CITATION STYLE
König, B., & Esparza, J. (2010). Verification of graph transformation systems with context-free specifications. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6372 LNCS, pp. 107–122). https://doi.org/10.1007/978-3-642-15928-2_8
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
