×

zbMATH — the first resource for mathematics

Reasoning with graph constraints. (English) Zbl 1209.68381
Summary: Graph constraints were introduced in the area of graph transformation, in connection with the notion of (negative) application conditions, as a form to limit the applicability of transformation rules. However, we believe that graph constraints may also play a significant role in the area of visual software modelling or in the specification and verification of semi-structured documents or websites (i.e. HTML or XML sets of documents). In this sense, after some discussion on these application areas, we concentrate on the problem of how to prove the consistency of specifications based on this kind of constraints. In particular, we present proof rules for two classes of graph constraints and show that our proof rules are sound and (refutationally) complete for each class. In addition, we study clause subsumption in this context as a form to speed up refutation.

MSC:
68R10 Graph theory (including graph drawing) in computer science
Software:
AGG
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Taentzer G (2004) AGG: a graph transformation environment for modeling and validation of software. In: Pfaltz J, Nagl M, Boehlen B (eds) Application of graph transformations with industrial relevance (AGTIVE903), LNCS 3062. Springer, Heidelberg, pp 446–456. URL: http://tfs.cs.tu-berlin.de/agg
[2] Alpuente M, Ballis D, Falaschi M (2006) Automated verification of web sites using partial rewriting. Softw Tools Technol Transf 8: 565–585 · Zbl 05075118 · doi:10.1007/s10009-006-0009-7
[3] Baldan P, Corradini A, Koenig B, Lluch-Lafuente A (2007) A temporal graph logic for verification of graph transformation systems. In: Recent trends in algebraic development techniques, 18th international workshop, WADT 2006. Springer Lecture Notes in Computer Science, vol 4409, pp 1–20 · Zbl 1196.68154
[4] Courcelle B (1997) The expression of graph properties and graph transformations in monadic second-order logic, in [Roz97], pp 313–400
[5] Ehrig H, Ehrig K, Prange U, Taentzer G (2006) Fundamentals of algebraic graph transformation. Springer, Heidelberg · Zbl 1095.68047
[6] Ehrig E, Ehrig K, Habel A, Pennemann KH (2004) Constraints and application conditions: from graphs to high-level structures. In: Ehrig H, Engels G, Parisi-Presicce F, Rozenberg G (eds) Graph transformations, second international conference, ICGT 2004. Springer Lecture Notes in Computer Science, vol 3256, pp 287–303 · Zbl 1116.68479
[7] Ehrig H, Habel A (1986) Graph grammars with application conditions. In: Rozenberg G, Salomaa A (eds) The book of L. Springer, Heidelberg, pp 87–100 · Zbl 0611.68045
[8] Ellmer E, Emmerich W, Finkelstein A, Nentwich C (2003) Flexible consistency checking. ACM Trans Softw Eng Method 12(1): 28–63 · Zbl 05459528 · doi:10.1145/839268.839271
[9] Habel A, Heckel R, Taentzer G (1996) Graph grammars with negative application conditions. Fundam Inform 26(3/4): 287–313 · Zbl 0854.68055
[10] Habel A, Pennemann KH (2005) Nested constraints and application conditions for high-level structures. In: Kreowski H-J, Montanari U, Orejas F, Rozenberg G, Taentzer G (eds) Formal methods in software and systems modeling. Essays dedicated to Hartmut Ehrig, on the occasion of his 60th birthday. Springer Lecture Notes in Computer Science, vol 3393, pp 293–308
[11] Habel A, Pennemann KH (2006) Satisfiability of high-level conditions. In: Corradini A, Ehrig H, Montanari U, Ribeiro L, Rozenberg G (eds) Graph transformations, third international conference, ICGT 2006. Springer Lecture Notes in Computer Science, vol 4178, pp 430–444 · Zbl 1156.68428
[12] Habel A, Pennemann KH (2008) Correctness of high-level transformation systems relative to nested conditions. Math Struct Comp Sci (accepted) · Zbl 1168.68022
[13] Heckel R, Wagner A (1995) Ensuring consistency of conditional graph grammars–a constructive approach. In: Proceedings SEGRAGRA 1995, Electr Notes Theor Comput Sci, vol 2, pp 118–126 · Zbl 0910.68154
[14] Jelliffe R (2000) Schematron. Internet document, May 2000. http://xml.ascc.net/resource/schematron/
[15] Lack S, Sobocinski P (2004) Adhesive categories. In: Walukiewicz I (ed) Foundations of software science and computation structures, 7th international conference, FOSSACS 2004, Lecture Notes in Computer Science, vol 2987. Springer, Heidelberg, pp 273–288 · Zbl 1126.68447
[16] Lambers L, Ehrig H, Orejas F (2006) Conflict detection for graph transformation with negative application conditions. In: Corradini A, Ehrig H, Montanari U, Ribeiro L, Rozenberg G (eds) Graph transformations, third international conference, ICGT 2006. Springer Lecture Notes in Computer Science, vol 4178, pp 61–76 · Zbl 1156.68431
[17] De Lara J, Guerra E (2008) Pattern-based model-to-model transformation. In: Ehrig H, Heckel R, Rozenberg G, Taentzer G (eds) Graph transformations, 4th international conference, ICGT 2008. Springer Lecture Notes in Computer Science, vol 5214, pp 426–441 · Zbl 1175.68114
[18] Lloyd JW (1987) Foundations of logic programming, 2nd edn. Springer, Heidelberg · Zbl 0668.68004
[19] Orejas F (2008) Attributed graph constraints. In: Ehrig H, Heckel R, Rozenberg G, Taentzer G (eds) Graph transformations, 4th international conference, ICGT 2008. Springer Lecture Notes in Computer Science, vol 5214, pp 274–288 · Zbl 1148.68002
[20] Orejas F, Ehrig H, Prange U (2008) A logic of graph constraints. In: Fiadeiro JL, Inverardi P (eds) Fundamental approaches to software engineering, 11th international conference, FASE 2008. Springer Lecture Notes in Computer Science, vol 4961, pp 179–198 · Zbl 1171.68516
[21] Koch M, Mancini LV, Parisi-Presicce F (2005) Graph-based specification of access control policies. J Comput Syst Sci 71(1): 1–33 · Zbl 1081.68072 · doi:10.1016/j.jcss.2004.11.002
[22] Pennemann KH (2008) Resolution-like theorem proving for high-level conditions. In: Ehrig H, Heckel R, Rozenberg G, Taentzer G (eds) Graph transformations, 4th international conference, ICGT 2008. Lecture Notes in Computer Science, vol 5214. Springer, Heidelberg, pp 289–304 · Zbl 1175.03008
[23] Rensink A (2004) Representing first-order logic using graphs. In: Ehrig H, Engels G, Parisi-Presicce F, Rozenberg G (eds) Graph transformations, second international conference, ICGT 2004. Springer Lecture Notes in Computer Science, vol 3256, pp 319–335
[24] Rozenberg, G (eds) (1997) Handbook of graph grammars and computing by graph transformation, vol 1 Foundations. World Scientific, Singapore · Zbl 0908.68095
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.