Abstract
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.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
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
Alpuente M, Ballis D, Falaschi M (2006) Automated verification of web sites using partial rewriting. Softw Tools Technol Transf 8: 565–585
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
Courcelle B (1997) The expression of graph properties and graph transformations in monadic second-order logic, in [Roz97], pp 313–400
Ehrig H, Ehrig K, Prange U, Taentzer G (2006) Fundamentals of algebraic graph transformation. Springer, Heidelberg
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
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
Ellmer E, Emmerich W, Finkelstein A, Nentwich C (2003) Flexible consistency checking. ACM Trans Softw Eng Method 12(1): 28–63
Habel A, Heckel R, Taentzer G (1996) Graph grammars with negative application conditions. Fundam Inform 26(3/4): 287–313
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
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
Habel A, Pennemann KH (2008) Correctness of high-level transformation systems relative to nested conditions. Math Struct Comp Sci (accepted)
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
Jelliffe R (2000) Schematron. Internet document, May 2000. http://xml.ascc.net/resource/schematron/
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
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
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
Lloyd JW (1987) Foundations of logic programming, 2nd edn. Springer, Heidelberg
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
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
Koch M, Mancini LV, Parisi-Presicce F (2005) Graph-based specification of access control policies. J Comput Syst Sci 71(1): 1–33
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
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
Rozenberg, G (eds) (1997) Handbook of graph grammars and computing by graph transformation, vol 1 Foundations. World Scientific, Singapore
Author information
Authors and Affiliations
Corresponding author
Additional information
J.L. Fiadeiro, P. Inverardi and T.S.E. Maibaum
Rights and permissions
About this article
Cite this article
Orejas, F., Ehrig, H. & Prange, U. Reasoning with graph constraints. Form Asp Comp 22, 385–422 (2010). https://doi.org/10.1007/s00165-009-0116-9
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-009-0116-9