Advertisement

A General Framework for Well-Structured Graph Transformation Systems

  • Barbara König
  • Jan Stückrath
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8704)

Abstract

Graph transformation systems (GTSs) can be seen as well-structured transition systems (WSTSs), thus obtaining decidability results for certain classes of GTSs. In earlier work it was shown that well-structuredness can be obtained using the minor ordering as a well-quasi-order. In this paper we extend this idea to obtain a general framework in which several types of GTSs can be seen as (restricted) WSTSs. We instantiate this framework with the subgraph ordering and the induced subgraph ordering and apply it to analyse a simple access rights management system.

Keywords

Coverability Problem Graph Transformation Graph Grammar Graph Transformation Rule Error Graph 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Abdulla, P.A., Bouajjani, A., Cederberg, J., Haziza, F., Rezine, A.: Monotonic abstraction for programs with dynamic memory heaps. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 341–354. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  2. 2.
    Abdulla, P.A., Čerāns, K., Jonsson, B., Tsay, Y.: General decidability theorems for infinite-state systems. In: Proc. of LICS 1996, pp. 313–321. IEEE (1996)Google Scholar
  3. 3.
    Bansal, K., Koskinen, E., Wies, T., Zufferey, D.: Structural counter abstraction. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 62–77. Springer, Heidelberg (2013)Google Scholar
  4. 4.
    Bertrand, N., Delzanno, G., König, B., Sangnier, A., Stückrath, J.: On the decidability status of reachability and coverability in graph transformation systems. In: Proc. of RTA 2012. LIPIcs, vol. 15, pp. 101–116. Schloss Dagstuhl, Leibniz Center for Informatics (2012)Google Scholar
  5. 5.
    Delzanno, G., Sangnier, A., Zavattaro, G.: Parameterized verification of ad hoc networks. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 313–327. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  6. 6.
    Ding, G.: Subgraphs and well-quasi-ordering. Jornal of Graph Theory 16, 489–502 (1992)CrossRefzbMATHGoogle Scholar
  7. 7.
    Ehrig, H., Heckel, R., Korff, M., Löwe, M., Ribeiro, L., Wagner, A., Corradini, A.: Algebraic approaches to graph transformation—part II: Single pushout approach and comparison with double pushout approach. In: Rozenberg, G. (ed.) Handbook of Graph Grammars and Computing by Graph Transformation. Foundations, vol. 1, ch. 4. World Scientific (1997)Google Scholar
  8. 8.
    Fellows, M.R., Hermelin, D., Rosamond, F.A.: Well-quasi-orders in subclasses of bounded treewidth graphs. In: Chen, J., Fomin, F.V. (eds.) IWPEC 2009. LNCS, vol. 5917, pp. 149–160. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  9. 9.
    Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere? Theoretical Computer Science 256(1-2), 63–92 (2001)CrossRefzbMATHMathSciNetGoogle Scholar
  10. 10.
    Heumüller, M., Joshi, S., König, B., Stückrath, J.: Construction of pushout complements in the category of hypergraphs. In: Proc. of GCM 2010 (Workshop on Graph Computation Models) (2010)Google Scholar
  11. 11.
    Joshi, S., König, B.: Applying the graph minor theorem to the verification of graph transformation systems. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 214–226. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  12. 12.
    Joshi, S., König, B.: Applying the graph minor theorem to the verification of graph transformation systems. Technical Report 2012-01, Abteilung für Informatik und Angewandte Kognitionswissenschaft, Universität Duisburg-Essen (2012)Google Scholar
  13. 13.
    Koch, M., Mancini, L.V., Parisi-Presicce, F.: Decidability of safety in graph-based models for access control. In: Gollmann, D., Karjoth, G., Waidner, M. (eds.) ESORICS 2002. LNCS, vol. 2502, pp. 229–243. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  14. 14.
    König, B., Stückrath, J.: Well-structured graph transformation systems with negative application conditions. In: Ehrig, H., Engels, G., Kreowski, H.-J., Rozenberg, G. (eds.) ICGT 2012. LNCS, vol. 7562, pp. 81–95. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  15. 15.
    König, B., Stückrath, J.: A general framework for well-structured graph transformation systems, arXiv:1406.4782 (2014)Google Scholar
  16. 16.
    Meyer, R.: Structural Stationarity in the π-Calculus. PhD thesis, Carl-von-Ossietzky-Universität Oldenburg (2009)Google Scholar
  17. 17.
    Robertson, N., Seymour, P.: Graph minors. XX. Wagner’s conjecture. Journal of Combinatorial Theory, Series B 92(2), 325–357 (2004)CrossRefzbMATHMathSciNetGoogle Scholar
  18. 18.
    Robertson, N., Seymour, P.: Graph minors XXIII. Nash-Williams’ immersion conjecture. Journal of Combinatorial Theory Series B 100, 181–205 (2010)CrossRefzbMATHMathSciNetGoogle Scholar
  19. 19.
    Rozenberg, G. (ed.): Handbook of Graph Grammars and Computing by Graph Transformation. Foundations, vol. 1. World Scientific (1997)Google Scholar
  20. 20.
    Saksena, M., Wibling, O., Jonsson, B.: Graph grammar modeling and verification of ad hoc routing protocols. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 18–32. Springer, Heidelberg (2008)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • Barbara König
    • 1
  • Jan Stückrath
    • 1
  1. 1.Universität Duisburg-EssenGermany

Personalised recommendations