Parameterized Verification of Graph Transformation Systems with Whole Neighbourhood Operations

Preprint English OPEN
Delzanno, Giorgio; Stückrath, Jan;
(2014)
  • Subject: Computer Science - Logic in Computer Science

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 t... View more
  • References (26)
    26 references, page 1 of 3

    1. P. A. Abdulla, M. F. Atig, and O. Rezine. Verification of directed acyclic ad hoc networks. In FMOODS/FORTE, pages 193-208, 2013.

    2. P. A. Abdulla, J. Cederberg, and T. Vojnar. Monotonic abstraction for programs with multiply-linked structures. Int. J. Found. Comput. Sci., 24(2):187-210, 2013.

    3. P. A. Abdulla, G. Delzanno, and A. Rezine. Approximated parameterized verification of infinite-state processes with global conditions. Formal Methods in System Design, 34(2):126-156, 2009.

    4. P. A. Abdulla, G. Delzanno, and A. Rezine. Automatic verification of directory-based consistency protocols with graph constraints. Int. J. Found. Comput. Sci., 22(4), 2011.

    5. P. A. Abdulla, N. Ben Henda, G. Delzanno, and A. Rezine. Handling parameterized systems with non-atomic global conditions. In VMCAI'08, volume 4905 of LNCS, pages 22-36. Springer, 2008.

    6. P. A. Abdulla, K. C˘ era¯ns, B. Jonsson, and Y. Tsay. General decidability theorems for infinitestate systems. In Proc. of LICS '96, pages 313-321. IEEE, 1996.

    7. N. Bertrand, G. Delzanno, B. Ko¨nig, A. Sangnier, and J. Stu¨ckrath. On the decidability status of reachability and coverability in graph transformation systems. In RTA'12, volume 15 of LIPIcs, pages 101-116. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2012.

    8. N. Bertrand, G. Delzanno, B. Ko¨nig, A. Sangnier, and J. Stu¨ckrath. On the decidability status of reachability and coverability in graph transformation systems. In RTA, pages 101-116, 2012.

    9. P. Boehm, H. Fonio, and A. Habel. Amalgamation of graph transformations: A synchronization mechanism. Journal of Computer and System Sciences, 34:377 - 408, 1987.

    10. G. Delzanno, C. Di Giusto, M. Gabbrielli, C. Laneve, and G. Zavattaro. The kappa-lattice: Decidability boundaries for qualitative analysis in biological languages. In CMSB, pages 158-172, 2009.

  • Metrics
Share - Bookmark