Parameterized Verification of Graph Transformation Systems with Whole Neighbourhood Operations

  • Giorgio Delzanno
  • Jan Stückrath
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8762)

Abstract

We introduce a new class of graph transformation systems in which rewrite rules can be guarded by universally quantified conditions on the neighbourhood of nodes. These conditions are defined via special graph patterns which may be transformed by the rule as well. For the new class for graph rewrite rules, we provide a symbolic procedure working on minimal representations of upward closed sets of configurations. We prove correctness and effectiveness of the procedure by a categorical presentation of rewrite rules as well as the involved order, and using results for well-structured transition systems. We apply the resulting procedure to the analysis of the Distributed Dining Philosophers protocol on an arbitrary network structure.

Keywords

Graph Transformation Graph Transformation Rule Graph Transformation System Entire Neighbourhood Restricted Coverability 
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., Atig, M.F., Rezine, O.: Verification of directed acyclic ad hoc networks. In: Beyer, D., Boreale, M. (eds.) FORTE 2013 and FMOODS 2013. LNCS, vol. 7892, pp. 193–208. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  2. 2.
    Abdulla, P.A., Cederberg, J., Vojnar, T.: Monotonic abstraction for programs with multiply-linked structures. Int. J. Found. Comput. Sci. 24(2), 187–210 (2013)MathSciNetCrossRefMATHGoogle Scholar
  3. 3.
    Abdulla, P.A., Delzanno, G., Rezine, A.: Approximated parameterized verification of infinite-state processes with global conditions. Formal Methods in System Design 34(2), 126–156 (2009)CrossRefMATHGoogle Scholar
  4. 4.
    Abdulla, P.A., Delzanno, G., Rezine, A.: Automatic verification of directory-based consistency protocols with graph constraints. Int. J. Found. Comput. Sci. 22(4) (2011)Google Scholar
  5. 5.
    Abdulla, P.A., Ben Henda, N., Delzanno, G., Rezine, A.: Handling parameterized systems with non-atomic global conditions. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 22–36. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  6. 6.
    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
  7. 7.
    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: RTA 2012. LIPIcs, vol. 15, pp. 101–116. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2012)Google Scholar
  8. 8.
    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: RTA, pp. 101–116 (2012)Google Scholar
  9. 9.
    Boehm, P., Fonio, H., Habel, A.: Amalgamation of graph transformations: A synchronization mechanism. Journal of Computer and System Sciences 34, 377–408 (1987)MathSciNetCrossRefMATHGoogle Scholar
  10. 10.
    Delzanno, G., Di Giusto, C., Gabbrielli, M., Laneve, C., Zavattaro, G.: The κ-lattice: Decidability boundaries for qualitative analysis in biological languages. In: Degano, P., Gorrieri, R. (eds.) CMSB 2009. LNCS, vol. 5688, pp. 158–172. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  11. 11.
    Delzanno, G., Rezine, A.: A lightweight regular model checking approach for parameterized systems. STTT 14(2), 207–222 (2012)CrossRefGoogle Scholar
  12. 12.
    Delzanno, G., Sangnier, A., Traverso, R.: Parameterized verification of broadcast networks of register automata. In: Abdulla, P.A., Potapov, I. (eds.) RP 2013. LNCS, vol. 8169, pp. 109–121. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  13. 13.
    Delzanno, G., Sangnier, A., Traverso, R., Zavattaro, G.: On the complexity of parameterized reachability in reconfigurable broadcast networks. In: FSTTCS 2012. LIPIcs, vol. 18, pp. 289–300. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2012)Google Scholar
  14. 14.
    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
  15. 15.
    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
  16. 16.
    Delzanno, G., Sangnier, A., Zavattaro, G.: On the power of cliques in the parameterized verification of ad hoc networks. In: Hofmann, M. (ed.) FOSSACS 2011. LNCS, vol. 6604, pp. 441–455. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  17. 17.
    Delzanno, G., Stu whole neighbourhood operations, arXiv:1407.4394 (2014)̈ckrath, J.: Parameterized verification of graph transformation systems with whole neighbourhood operations, arXiv:1407.4394 (2014)Google Scholar
  18. 18.
    Delzanno, G., Traverso, R.: Decidability and complexity results for verification of asynchronous broadcast networks. In: Dediu, A.-H., Martín-Vide, C., Truthe, B. (eds.) LATA 2013. LNCS, vol. 7810, pp. 238–249. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  19. 19.
    Ding, G.: Subgraphs and well-quasi-ordering. Jornal of Graph Theory 16, 489–502 (1992)CrossRefMATHGoogle Scholar
  20. 20.
    Drewes, F., Hoffmann, B., Janssens, D., Minas, M., Van Eetvelde, N.: Adaptive star grammars. In: Corradini, A., Ehrig, H., Montanari, U., Ribeiro, L., Rozenberg, G. (eds.) ICGT 2006. LNCS, vol. 4178, pp. 77–91. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  21. 21.
    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. ch. 4, vol. 1. World Scientific (1997)Google Scholar
  22. 22.
    Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere? Theoretical Computer Science 256(1-2), 63–92 (2001)MathSciNetCrossRefMATHGoogle Scholar
  23. 23.
    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
  24. 24.
    König, B., Stückrath, J.: A general framework for well-structured graph transformation systems. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 467–481. Springer, Heidelberg (2014)CrossRefGoogle Scholar
  25. 25.
    Namjoshi, K.S., Trefler, R.J.: Uncovering symmetries in irregular process networks. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 496–514. Springer, Heidelberg (2013)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Giorgio Delzanno
    • 1
  • Jan Stückrath
    • 2
  1. 1.Università di GenovaItaly
  2. 2.Universität Duisburg-EssenGermany

Personalised recommendations