Top

Published in:

2021 | OriginalPaper | Chapter

Automated Checking and Completion of Backward Confluence for Hyperedge Replacement Grammars

Authors : Ira Fesefeldt, Christoph Matheja, Thomas Noll, Johannes Schulte

Published in: Graph Transformation

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

We present a tool that checks for a given context-free graph grammar whether the corresponding graph reduction system in which all rules are applied backward, is confluent—a question that arises when using graph grammars to guide state space abstractions for analyzing heap-manipulating programs; confluence of the graph reduction system then guarantees the abstraction’s uniqueness. If a graph reduction system is not confluent, our tool provides symbolic representations of counterexamples to confluence, i.e., non-joinable critical pairs, for manual inspection. Furthermore, it features a heuristics-based completion procedure that attempts to turn a graph reduction system into a confluent one without invalidating the properties mandated by the abstraction framework. We evaluate our implementation on various graph grammars for verifying data structure traversal algorithms from the literature.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter On the Complexity of Simulating Probabilistic Timed Graph Transformation Systems

next chapter GrapePress - A Computational Notebook for Graph Transformations

https://github.com/moves-rwth/attestor.

https://www.user.tu-berlin.de/o.runge/agg/.

https://github.com/moves-rwth/attestor-confluence.

That is, rules 2 and 3 were applied. To improve performance, Attestor generates specialized rules in which two or more external nodes are identical; the number after the dot indicates which case of a rule has been applied.

Arendt, T., Biermann, E., Jurack, S., Krause, C., Taentzer, G.: Henshin: advanced concepts and tools for in-place EMF model transformations. In: Petriu, D.C., Rouquette, N., Haugen, Ø. (eds.) MODELS 2010. LNCS, vol. 6394, pp. 121–135. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16145-2_9CrossRef

Arndt, H., Jansen, C., Katoen, J.-P., Matheja, C., Noll, T.: Let this graph be your witness!. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 3–11. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-96142-2_1CrossRef

Arndt, H., Jansen, C., Matheja, C., Noll, T.: Graph-based shape analysis beyond context-freeness. In: Johnsen, E.B., Schaefer, I. (eds.) SEFM 2018. LNCS, vol. 10886, pp. 271–286. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-92970-5_17CrossRef

Azzi, G.G., Bezerra, J.S., Ribeiro, L., Costa, A., Rodrigues, L.M., Machado, R.: The verigraph system for graph transformation. In: Heckel, R., Taentzer, G. (eds.) Graph Transformation, Specifications, and Nets. LNCS, vol. 10800, pp. 160–178. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-75396-6_9CrossRefMATH

Born, K., Arendt, T., Heß, F., Taentzer, G.: Analyzing conflicts and dependencies of rule-based transformations in Henshin. In: Egyed, A., Schaefer, I. (eds.) FASE 2015. LNCS, vol. 9033, pp. 165–168. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46675-9_11CrossRef

Campbell, G., Plump, D.: Confluence up to garbage. In: Gadducci, F., Kehrer, T. (eds.) ICGT 2020. LNCS, vol. 12150, pp. 20–37. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-51372-6_2CrossRef

Costa, A., et al.: Verigraph: a system for specification and analysis of graph grammars. In: Ribeiro, L., Lecomte, T. (eds.) SBMF 2016. LNCS, vol. 10090, pp. 78–94. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-49815-7_5CrossRef

Deckwerth, F.: Static Verification Techniques for Attributed Graph Transformations. Ph.D. thesis, Technische Universität, Darmstadt (2017)

Drewes, F., Kreowski, H.J., Habel, A.: Hyperedge replacement graph grammars. In: Handbook of Graph Grammars and Computing by Graph Transformation, vol. I: Foundations, pp. 95–162. World Scientific (1997)

10.

Fesefeldt, I.: moves-rwth/attestor-confluence. https://github.com/moves-rwth/attestor-confluence/blob/master/readme/HEURISTICS.md

11.

Heckel, R., Küster, J.M., Taentzer, G.: Confluence of typed attributed graph transformation systems. In: Corradini, A., Ehrig, H., Kreowski, H.-J., Rozenberg, G. (eds.) ICGT 2002. LNCS, vol. 2505, pp. 161–176. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45832-8_14CrossRefMATH

12.

Heinen, J., Jansen, C., Katoen, J.P., Noll, T.: Verifying pointer programs using graph grammars. Sci. Comput. Programm. 97(1), 157–162 (2015)CrossRef

13.

Hoffmann, B., Plump, D.: Implementing term rewriting by jungle evaluation. RAIRO Theor. Inform. Appl. 25, 445–472 (1991)MathSciNetCrossRef

14.

Hristakiev, I., Plump, D.: Checking graph programs for confluence. In: Seidl, M., Zschaler, S. (eds.) STAF 2017. LNCS, vol. 10748, pp. 92–108. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-74730-9_8CrossRef

15.

Jansen, C.: Static Analysis of Pointer Programs - Linking Graph Grammars and Separation Logic. Ph.D. thesis, RWTH Aachen University, Germany (2017)

16.

Jansen, C., Heinen, J., Katoen, J.-P., Noll, T.: A local greibach normal form for hyperedge replacement grammars. In: Dediu, A.-H., Inenaga, S., Martín-Vide, C. (eds.) LATA 2011. LNCS, vol. 6638, pp. 323–335. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21254-3_25CrossRef

17.

Knuth, D., Bendix, P.: Simple word problems in universal algebra. Computational Problems in Abstract Algebra, pp. 263–297 (1970)

18.

Lambers, L., Born, K., Kosiol, J., Strüber, D., Taentzer, G.: Granularity of conflicts and dependencies in graph transformation systems: a two-dimensional approach. J. Logic. Algebraic Meth. Program. 103, 105–129 (2019)MathSciNetCrossRef

19.

Lambers, L., Ehrig, H., Orejas, F.: Conflict detection for graph transformation with negative application conditions. In: Corradini, A., Ehrig, H., Montanari, U., Ribeiro, L., Rozenberg, G. (eds.) ICGT 2006. LNCS, vol. 4178, pp. 61–76. Springer, Heidelberg (2006). https://doi.org/10.1007/11841883_6CrossRefMATH

20.

Lambers, L., Ehrig, H., Orejas, F.: Efficient conflict detection in graph transformation systems by essential critical pairs. Electron. Notes Theor. Comput. Sci. 211, 17–26 (2008)CrossRef

21.

Matheja, C.: Automated reasoning and randomization in separation logic. Ph.D. thesis, RWTH Aachen University, Germany (2020)

22.

Matheja, C., Jansen, C., Noll, T.: Tree-like grammars and separation logic. In: Feng, X., Park, S. (eds.) APLAS 2015. LNCS, vol. 9458, pp. 90–108. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-26529-2_6CrossRefMATH

23.

Plump, D.: Confluence of graph transformation revisited. In: Middeldorp, A., van Oostrom, V., van Raamsdonk, F., de Vrijer, R. (eds.) Processes, Terms and Cycles: Steps on the Road to Infinity. LNCS, vol. 3838, pp. 280–308. Springer, Heidelberg (2005). https://doi.org/10.1007/11601548_16CrossRef

24.

Plump, D.: Checking graph-transformation systems for confluence. ECEASST 26 (2010)

25.

Runge, O., Ermel, C., Taentzer, G.: AGG 2.0 – new features for specifying and analyzing algebraic graph transformations. In: Schürr, A., Varró, D., Varró, G. (eds.) AGTIVE 2011. LNCS, vol. 7233, pp. 81–88. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-34176-2_8CrossRef

26.

Schulte, J.: Automated Detection and Completion of Confluence for Graph Grammars. Master thesis, RWTH Aachen University, Germany (2019). http://www-i2.informatik.rwth-aachen.de/pub/index.php?type=download&pub_id=1765

27.

Taentzer, G.: AGG: a graph transformation environment for modeling and validation of software. In: Pfaltz, J.L., Nagl, M., Böhlen, B. (eds.) AGTIVE 2003. LNCS, vol. 3062, pp. 446–453. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-25959-6_35CrossRef

Title: Automated Checking and Completion of Backward Confluence for Hyperedge Replacement Grammars
Authors: Ira Fesefeldt
Christoph Matheja
Thomas Noll
Johannes Schulte
Publisher: Springer International Publishing
Book: Graph Transformation
Print ISBN: 978-3-030-78945-9

Electronic ISBN: 978-3-030-78946-6

Copyright Year: 2021
DOI: https://doi.org/10.1007/978-3-030-78946-6_15

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner