×

zbMATH — the first resource for mathematics

Symbolic graphs for attributed graph constraints. (English) Zbl 1298.68121
Summary: In this paper we present a new class of graphs, called symbolic graphs, to define a new class of constraints on attributed graphs. In particular, in the first part of the paper, we study the category of symbolic graphs showing that it satisfies some properties, which are the basis for the work that we present in the second part of the paper, where we study how to reason with attributed graph constraints. More precisely, we define a set of inference rules, which are the instantiation of the inference rules defined in a previous paper, for reasoning about constraints on standard graphs, showing their soundness and (weak) completeness. Moreover, the proof of soundness and completeness is also an instantiation of the corresponding proof for standard graph constraints, using the categorical properties studied in the first part of the paper. Finally, we show that adding a new inference rule makes our system sound and strongly complete.

MSC:
68Q42 Grammars and rewriting systems
68Q65 Abstract data types; algebraic specification
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Berthold, M., Fischer, I., Koch, M., 2000. Attributed graph transformation with partial attribution. In: GRATRA 2000. Joint APPLIGRAPH and GETGRATS Workshop on Graph Transformation Systems. pp. 171-178.
[2] Courcelle, B., The expression of graph properties and graph transformations in monadic second-order logic, (), 313-400
[3] de Lara, J.; Guerra, E., Pattern-based model-to-model transformation, (), 426-441 · Zbl 1175.68114
[4] Ehrig, H., Attributed graphs and typing: relationship between different representations, Bull. eur. assoc. theor. comput. sci. EATCS, 82, 175-190, (2004) · Zbl 1169.68558
[5] Ehrig, H.; Ehrig, K.; Prange, U.; Taentzer, G., Fundamental theory of typed attributed graph transformation based on adhesive HLR-categories, Fund. inform., 74, 1, 31-61, (2006) · Zbl 1106.68055
[6] Ehrig, H.; Ehrig, K.; Prange, U.; Taentzer, G., ()
[7] Ehrig, H.; Habel, A., Graph grammars with application conditions, (), 87-100 · Zbl 0611.68045
[8] Habel, A.; Heckel, R.; Taentzer, G., Graph grammars with negative application conditions, Fund. inform., 26, 3/4, 287-313, (1996) · Zbl 0854.68055
[9] Habel, A.; Pennemann, K.-H., Correctness of high-level transformation systems relative to nested conditions, Math. structures comput. sci., 19, 245-296, (2009) · Zbl 1168.68022
[10] Heckel, R., Küster, J., Taentzer, G., 2002. Towards automatic translation of uml models into semantic domains. In: APPLIGRAPH Workshop on Applied Graph Transformation. pp. 11-22.
[11] Heckel, R.; Wagner, A., Ensuring consistency of conditional graph grammars — a constructive approach, Electron. notes theor. comput. sci., 2, 118-126, (1995)
[12] Koch, M.; Mancini, L.; Parisi-Presicce, F., Graph-based specification of access control policies, J. comput. system sci., 71, 1-33, (2005) · Zbl 1081.68072
[13] Lack, S.; Sobocinski, P., Adhesive and quasiadhesive categories, Theor. inform. appl., 39, 511-545, (2005) · Zbl 1078.18010
[14] Löwe, M.; Korff, M.; Wagner, A., An algebraic framework for the transformation of attributed graphs, (), 185-199
[15] Naeem, M.; Heckel, R.; Orejas, F.; Hermann, F., Incremental service composition based on partial matching of visual contracts, (), 123-138
[16] Orejas, F., Attributed graph constraints, (), 274-288 · Zbl 1175.68229
[17] Orejas, F.; Ehrig, H.; Prange, U., A logic of graph constraints, (), 179-198 · Zbl 1171.68516
[18] Orejas, F.; Ehrig, H.; Prange, U., Reasoning with graph constraints, Formal aspects of computing, (2009)
[19] Orejas, F., Lambers, L., 2010a. Delaying constraint solving in symbolic graph transformation. In: Graph Transformations, ICGT 2010. · Zbl 1306.68084
[20] Orejas, F., Lambers, L., 2010b. Symbolic attributed graphs for attributed graph transformation. In: Int. Coll. on Graph and Model Transformation. On the occasion of the 65th birthday of Hartmut Ehrig. · Zbl 1306.68084
[21] Pennemann, K.-H., Resolution-like theorem proving for high-level conditions, (), 289-304 · Zbl 1175.03008
[22] Rensink, A., Representing first-order logic using graphs, (), 319-335 · Zbl 1116.03303
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.