Skip to main content
SpringerLink
Log in

Locality in Reasoning about Graph Transformations

  • Conference paper
Applications of Graph Transformations with Industrial Relevance (AGTIVE 2011)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 7233))

Abstract

This paper explores how to reason locally about global properties of graph transformations, in particular properties involving transitive closure of the edge relations of the graph. We show under which conditions we can soundly reduce reasoning about all nodes in the graph to reasoning about a finite set of nodes. We then give an effective procedure to turn this reduced problem into a Boolean satisfiability problem.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 54.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 72.00
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Asztalos, M., Lengyel, L., Levendovszky, T.: Towards automated, formal verification of model transformations. In: Proc. of the 3rd International Conference on Software Testing, Verification, and Validation, pp. 15–24. IEEE Computer Society, Los Alamitos (2010)

    Chapter  Google Scholar 

  2. Baldan, P., Corradini, A., Esparza, J., Heindel, T., König, B., Kozioura, V.: Verifying red-black trees. In: Proc. of Concurrent Systems with Dynamic Allocated Heaps, COSMICAH 2005 (2005); Proceedings available as report RR-05-04 (Queen Mary, University of London)

    Google Scholar 

  3. Baldan, P., Corradini, A., König, B.: A framework for the verification of infinite-state graph transformation systems. Information and Computation 206(7), 869–907 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  4. Berdine, J., Calcagno, C., O’Hearn, P.: A decidable fragment of separation logic. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 97–109. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  5. Caferra, R., Echahed, R., Peltier, N.: A term-graph clausal logic: Completeness and incompleteness results. Journal of Applied Non-classical Logics 18(4), 373–411 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  6. da Costa, S.A., Ribeiro, L.: Formal verification of graph grammars using mathematical induction. In: Proc. of the 11th Brazilian Symposium on Formal Methods (SBMF 2008). ENTCS, vol. 240, pp. 43–60. Elsevier (2009)

    Google Scholar 

  7. Dodds, M.: Graph Transformation and Pointer Structures. Ph.D. thesis, University of York (2008)

    Google Scholar 

  8. Ghamarian, A.H., de Mol, M.J., Rensink, A., Zambon, E., Zimakova, M.V.: Modelling and analysis using GROOVE. Tech. Rep. TR-CTIT-10-18, Centre for Telematics and Information Technology, University of Twente, Enschede (2010)

    Google Scholar 

  9. Habel, A., Pennemann, K.H.: Correctness of high-level transformation systems relative to nested conditions. Mathematical Structures in Computer Science 19(02), 245–296 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  10. Immerman, N., Rabinovich, A., Reps, T., Sagiv, M., Yorsh, G.: The Boundary Between Decidability and Undecidability for Transitive-Closure Logics. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, pp. 160–174. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  11. Kastenberg, H.: Graph-Based Software Specification and Verification. Ph.D. thesis, University of Twente (2008), http://eprints.eemcs.utwente.nl/13615/

  12. König, B., Kozioura, V.: Augur 2 – A new version of a tool for the analysis of graph transformation systems. In: Proc. of the 5th Int. Workshop on Graph Transformation and Visual Modeling Techniques. ENTCS, vol. 211, pp. 201–210. Elsevier (2008)

    Google Scholar 

  13. McPeak, S., Necula, G.C.: Data Structure Specifications via Local Equality Axioms. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 476–490. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  14. Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  15. Pennemann, K.H.: Resolution-Like Theorem Proving for High-Level Conditions. In: Ehrig, H., Heckel, R., Rozenberg, G., Taentzer, G. (eds.) ICGT 2008. LNCS, vol. 5214, pp. 289–304. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  16. Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proc. of the 17th Annual IEEE Symposium on Logic in Computer Science, pp. 55–74. IEEE Computer Society (2002)

    Google Scholar 

  17. Ribeiro, L., Dotti, F.L., da Costa, S.A., Dillenburg, F.C.: Towards theorem proving graph grammars using Event-B. In: Ermel, C., Ehrig, H., Orejas, F., Taentzer, G. (eds.) Proc. of the International Colloquium on Graph and Model Transformation 2010. ECEASST, vol. 30 (2010)

    Google Scholar 

  18. Strecker, M.: Modeling and verifying graph transformations in proof assistants. In: Mackie, I., Plump, D. (eds.) International Workshop on Computing with Terms and Graphs. ENTCS, vol. 203, pp. 135–148. Elsevier (2008)

    Google Scholar 

  19. Varró, D., Balogh, A.: The model transformation language of the VIATRA2 framework. Science of Computer Programming 68(3), 214–234 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  20. Yorsh, G., Rabinovich, A.M., Sagiv, M., Meyer, A., Bouajjani, A.: A logic of reachable patterns in linked data-structures. The Journal of Logic and Algebraic Programming 73(1-2), 111–142 (2007)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. IRIT (Institut de Recherche en Informatique de Toulouse), Université de Toulouse, France

    Martin Strecker

Authors
  1. Martin Strecker
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Real-Time Systems Lab, Technische Universität Darmstadt, Merckstraße 25, 64283, Darmstadt, Germany

    Andy Schürr  & Gergely Varró  & 

  2. Department of Measurement and Information Systems, Budapest University of Technology and Economics, Magyar tudósok krt. 2, 1117, Budapest, Hungary

    Dániel Varró

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Strecker, M. (2012). Locality in Reasoning about Graph Transformations. In: Schürr, A., Varró, D., Varró, G. (eds) Applications of Graph Transformations with Industrial Relevance. AGTIVE 2011. Lecture Notes in Computer Science, vol 7233. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-34176-2_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-34176-2_15

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-34175-5

  • Online ISBN: 978-3-642-34176-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation