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.
Research supported by DFG project SANDS.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Baldan, P., Corradini, A., König, B.: A static analysis technique for graph transformation systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 381–395. Springer, Heidelberg (2001)
Baldan, P., König, B.: Approximating the behaviour of graph transformation systems. In: Corradini, A., Ehrig, H., Kreowski, H.-J., Rozenberg, G. (eds.) ICGT 2002. LNCS, vol. 2505, pp. 14–29. Springer, Heidelberg (2002)
Baldan, P., König, B., König, B.: A logic for analyzing abstractions of graph transformation systems. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 255–272. Springer, Heidelberg (2003)
Bauer, J., Wilhelm, R.: Static analysis of dynamic communication systems by partner abstraction. In: Riis Nielson, H., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 249–264. Springer, Heidelberg (2007)
Bouajjani, A., Esparza, J., Touili, T.: A generic approach to the static analysis of concurrent programs with procedures. In: Proc. of POPL 2003, pp. 62–73. ACM, New York (2003)
Chandy, K.M., Misra, J.: The drinking philosophers problem. ACM Transactions on Programming Languages and Systems 6(4), 632–646 (1984)
Courcelle, B.: The expression of graph properties and graph transformations in monadic second-order logic. In: Rozenberg, G. (ed.) Handbook of Graph Grammars and Computing by Graph Transformation, ch. 5. Foundations, vol. 1. World Scientific, Singapore (1997)
Deutsch, A.: Interprocedural may-alias analysis for pointers: Beyond k-limiting. In: Proc. of PLDI 1994. SIGPLAN Notices, vol. 29(6), pp. 230–241. ACM, New York (1994)
Distefano, D., O’Hearn, P.W., Yang, H.: A local shape analysis based on separation logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 287–302. Springer, Heidelberg (2006)
Dotti, F.L., Foss, L., Ribeiro, L., Marchi Santos, O.: Verification of distributed object-based systems. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol. 2884, pp. 261–275. Springer, Heidelberg (2003)
Esparza, J., Melzer, S.: Verification of safety properties using integer programming: Beyond the state equation. Formal Methods in System Design 16, 159–189 (2000)
Ginsburg, S., Spanier, E.H.: Semigroups, Presburger formulas, and languages. Pacific Journal of Mathematics 16(2), 285–296 (1966)
Habel, A.: Hyperedge Replacement: Grammars and Languages. In: Habel, A. (ed.) Hyperedge Replacement: Grammars and Languages. LNCS, vol. 643. Springer, Heidelberg (1992)
König, B.: Graph transformation systems, Petri nets and semilinear sets: Checking for the absence of forbidden paths in graphs. In: Proc. of PNGT 2006. Electronic Communications of the EASST, vol. 2 (2007)
König, B., Kozioura, V.: Counterexample-guided abstraction refinement for the analysis of graph transformation systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 197–211. Springer, Heidelberg (2006)
König, B., Kozioura, V.: Augur 2—a new version of a tool for the analysis of graph transformation systems. In: Proc. of GT-VMT 2006. ENTCS, vol. 211, pp. 201–210. Elsevier, Amsterdam (2006)
Lafont, Y.: Interaction nets. In: Proc. of POPL 1990, pp. 95–108. ACM Press, New York (1990)
Lammich, P., Müller-Olm, M., Wenner, A.: Predecessor sets of dynamic pushdown networks with tree-regular constraints. In: Bouajjani, A., Maler, O. (eds.) Computer Aided Verification. LNCS, vol. 5643, pp. 525–539. Springer, Heidelberg (2009)
Mayr, E.W.: An algorithm for the general Petri net reachability problem. SIAM J. Comput. 13(3), 441–460 (1984)
Meyer, R.: On boundedness in depth in the pi-calculus. In: Proc. of IFIP TCS 2008. IFIP, vol. 273, pp. 477–489. Springer, Heidelberg (2008)
Rensink, A., Distefano, D.: Abstract graph transformation. In: Proc. of SVV 2005. ENTCS, vol. 157.1, pp. 39–59 (2005)
Rieger, S., Noll, T.: Abstracting complex data structures by hyperedge replacement. In: Ehrig, H., Heckel, R., Rozenberg, G., Taentzer, G. (eds.) ICGT 2008. LNCS, vol. 5214, pp. 69–83. Springer, Heidelberg (2008)
Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. TOPLAS (ACM Transactions on Programming Languages and Systems) 24(3), 217–298 (2002)
Varró, D.: Towards symbolic analysis of visual modeling languages. In: Proc. of GT-VMT 2002. ENTCS, vol. 72. Elsevier, Amsterdam (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
König, B., Esparza, J. (2010). Verification of Graph Transformation Systems with Context-Free Specifications. In: Ehrig, H., Rensink, A., Rozenberg, G., Schürr, A. (eds) Graph Transformations. ICGT 2010. Lecture Notes in Computer Science, vol 6372. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15928-2_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-15928-2_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15927-5
Online ISBN: 978-3-642-15928-2
eBook Packages: Computer ScienceComputer Science (R0)