nach oben

Erschienen in:

2019 | OriginalPaper | Buchkapitel

Two-Level Reasoning About Graph Transformation Programs

verfasst von : Amani Makhlouf, Christian Percebois, Hanh Nhi Tran

Erschienen in: Graph Transformation

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

This paper presents a method for verifying graph transformation programs written in Small-t\(\mathcal ALC\), an imperative language which allows expressing graph properties and graph transformations in \(\mathcal ALCQI\) description logic. We aim at reasoning not only about the local effect when applying a transformation rule on a matched subgraph but also about the global impact on the whole input graph when applying a set of rules. Using \(\mathcal ALCQI\) assertional and terminological formulae to formalize directed labeled graphs, Small-t\(\mathcal ALC\) allows specifying local properties on individual nodes and edges as well as global properties on sets of nodes and edges. Our previous work focuses on verifying local properties of the graph. In this paper, we propose a static analyzer at terminological level that intertwines with a static analyzer at assertional level to infer global properties of the transformed graph.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren

Vorheriges Kapitel Unfolding Graph Grammars with Negative Application Conditions

Nächstes Kapitel Incremental (Unidirectional) Model Transformation with eMoflon::IBeX

https://www.irit.fr/~Martin.Strecker/CLIMT/Software/smalltalc.html.

Habel, A., Pennemann, K.-H.: Correctness of high-level transformation systems relative to nested conditions. Math. Struct. Comput. Sci. 19(2), 245–296 (2009). https://doi.org/10.1017/S0960129508007202MathSciNetCrossRefMATH

Rensink, A.: Representing first-order logic using graphs. In: Ehrig, H., Engels, G., Parisi-Presicce, F., Rozenberg, G. (eds.) ICGT 2004. LNCS, vol. 3256, pp. 319–335. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30203-2_23CrossRef

Orejas, F., Ehrig, H., Prange, U.: A logic of graph constraints. In: Fiadeiro, J.L., Inverardi, P. (eds.) FASE 2008. LNCS, vol. 4961, pp. 179–198. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78743-3_14CrossRef

Lambers, L., Orejas, F.: Tableau-based reasoning for graph properties. In: Giese, H., König, B. (eds.) Graph Transformation, pp. 17–32. Springer, Cham (2014)MATH

Poskitt, C.M., Plump, D.: Verifying monadic second-order properties of graph programs. In: Giese, H., König, B. (eds.) Graph Transformation, pp. 33–48. Springer, Cham (2014)MATH

Courcelle, B.: The expression of graph properties and graph transformations in monadic second-order logic. In: Handbook of Graph Grammars and Computing by Graph Transformations, Volume 1: Foundations, pp. 313–400 (1997)

Strecker, M.: Modeling and verifying graph transformations in proof assistants. Electron. Notes Theoret. Comput. Sci. 203(1), 135–148 (2008)MathSciNetCrossRef

Baklanova, N., et al.: Coding, executing and verifying graph transformations with small-t\(\cal{ ALCQ}\)e. In: 7th International Workshop on Graph Computation Models(GCM) (2016). http://gcm2016.inf.uni-due.de/

Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F. (eds.): The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press, New York (2003)MATH

10.

Makhlouf, A., Percebois, C., Tran, H.N.: An auto-active approach to develop correct logic-based graph transformations. Int. J. Adv. Softw. 11(1,2), 147–158 (2018) http://oatao.univ-toulouse.fr/22689/

11.

Sattler, U.: Reasoning in description logics: basics, extensions, and relatives. In: Antoniou, G., et al. (eds.) Reasoning Web 2007. LNCS, vol. 4636, pp. 154–182. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74615-7_2CrossRefMATH

12.

De Giacomo, G., Lenzerini, M., Poggi, A., Rosati, R.: On instance-level update and erasure in description logic ontologies. J. Logic Comput. 19(5), 745–770 (2009)MathSciNetCrossRef

13.

Dijkstra, E.W., Scholten, C.S.: Predicate Calculus and Program Semantics. Springer, New York (1990). https://doi.org/10.1007/978-1-4612-3228-5CrossRefMATH

14.

Cousot, P.: Abstract interpretation based formal methods and future challenges. In: Wilhelm, R. (ed.) Informatics. LNCS, vol. 2000, pp. 138–156. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-44577-3_10CrossRef

15.

Poskitt, C.M., Plump, D.: Hoare-style verification of graph programs. Fundam. Inform. 118, 135–175 (2012)MathSciNetMATH

16.

Navarro, M., Pino, E., Orejas, F., Lambers, L.: A logic of graph conditions extended with paths. In: Pre-proceedings 7th International Workshop on Graph Computation Models (2016 ). http://gcm2016.inf.uni-due.de/pre-proceedings.html

17.

Lambers, L., Navarro, M., Orejas, F., Pino, E.: Towards a navigational logic for graphical structures. In: Heckel, R., Taentzer, G. (eds.) Graph Transformation, Specifications, and Nets. LNCS, vol. 10800, pp. 124–141. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-75396-6_7CrossRef

18.

Ahmetaj, S., Calvanese, D., Ortiz, M., Simkus, M.: Managing change in graph-structured data using description logics. ACM Trans. Comput. Logic 18(4), 27:1–27:35 (2017). https://doi.org/10.1145/3143803MathSciNetCrossRefMATH

19.

Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. In: Gabbay, D.M., Guenthner, F. (eds.) Handbook of Philosophical Logic. Handbook of Philosophical Logic, vol. 4, pp. 99–217. Springer, Dordrecht (2002). https://doi.org/10.1007/978-94-017-0456-4_2CrossRefMATH

20.

Brenas, J.H., Echahed, R., Strecker, M.: C2PDLS: a combination of combinatory and converse PDL with substitutions. In: Gammarth, T., Mosbah, M., Rusinowitch, M. (eds.) 2017 the 8th International Symposium on Symbolic Computation in Software Science, SCSS 2017, 6–9 April 2017, pp. 29–41 (2017). https://easychair.org/publications/paper/dx4z

21.

Liu, H., Lutz, C., Miličić, M., Wolter, F.: Reasoning about actions using description logics with general TBoxes. In: Fisher, M., van der Hoek, W., Konev, B., Lisitsa, A. (eds.) JELIA 2006. LNCS (LNAI), vol. 4160, pp. 266–279. Springer, Heidelberg (2006). https://doi.org/10.1007/11853886_23CrossRefMATH

Titel: Two-Level Reasoning About Graph Transformation Programs
verfasst von: Amani Makhlouf
Christian Percebois
Hanh Nhi Tran
Verlag: Springer International Publishing
Buch: Graph Transformation
Print ISBN: 978-3-030-23610-6

Electronic ISBN: 978-3-030-23611-3

Copyright-Jahr: 2019
DOI: https://doi.org/10.1007/978-3-030-23611-3_7

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner