Satisfiability of High-Level Conditions

  • Annegret Habel
  • Karl-Heinz Pennemann
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4178)


In this paper, we consider high-level structures like graphs, Petri nets, and algebraic specifications and investigate two kinds of satisfiability of conditions and two kinds of rule matching over these structures. We show that, for weak adhesive HLR categories with class \({\mathcal{A}}\) of all morphisms and a class \({\mathcal {M}}\) of monomorphisms, strictly closed under decompositions, \({\mathcal{A}}\)- and \({\mathcal{M}}\)-satisfiability and \({\mathcal{A}}\)- and \(P{\mathcal{M}}\)-matching are expressively equivalent. The results are applied to the category of graphs, where \({\mathcal{M}}\) is the class of all injective graph morphisms.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Corradini, A., Montanari, U., Rossi, F., Ehrig, H., Heckel, R., Löwe, M.: Algebraic approaches to graph transformation. Part I: Basic concepts and double pushout approach. In: Handbook of Graph Grammars and Computing by Graph Transformation, vol. 1, pp. 163–245. World Scientific, Singapore (1997)CrossRefGoogle Scholar
  2. 2.
    Ehrig, H.: Introduction to the algebraic theory of graph grammars. In: Ng, E.W., Ehrig, H., Rozenberg, G. (eds.) Graph Grammars 1978. LNCS, vol. 73, pp. 1–69. Springer, Heidelberg (1979)CrossRefGoogle Scholar
  3. 3.
    Ehrig, H., Ehrig, K., Habel, A., Pennemann, K.-H.: Theory of constraints and application conditions: From graphs to high-level structures. Fundamenta Informaticae 72 (2006)Google Scholar
  4. 4.
    Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic Graph Transformation. EATCS Monographs of Theoretical Computer Science. Springer, Heidelberg (2006)Google Scholar
  5. 5.
    Ehrig, H., Habel, A., Kreowski, H.-J., Parisi-Presicce, F.: Parallelism and concurrency in high level replacement systems. Mathematical Structures in Computer Science 1, 361–404 (1991)zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    Ehrig, H., Habel, A., Padberg, J., Prange, U.: Adhesive high-level replacement systems: A new categorical framework for graph transformation. Fundamenta Informaticae 72 (2006)Google Scholar
  7. 7.
    Habel, A., Müller, J., Plump, D.: Double-pushout graph transformation revisited. Mathematical Structures in Computer Science 11(5), 637–688 (2001)zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    Habel, A., Pennemann, K.-H.: 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. LNCS, vol. 3393, pp. 293–308. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  9. 9.
    Habel, A., Pennemann, K.-H., Rensink, A.: Weakest preconditions for high-level programs. In: Corradini, A., Ehrig, H., Montanari, U., Ribeiro, L., Rozenberg, G. (eds.) ICGT 2006. LNCS, vol. 4178, pp. 445–460. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  10. 10.
    Heckel, R., Wagner, A.: Ensuring consistency of conditional graph grammars — a constructive approach. In: SEGRAGRA 1995. Electronic Notes in Theoretical Computer Science, vol. 2, pp. 95–104 (1995)Google Scholar
  11. 11.
    Koch, M., Mancini, L.V., Parisi-Presicce, F.: Graph-based specification of access control policies. Journal of Computer and System Sciences 71, 1–33 (2005)zbMATHCrossRefMathSciNetGoogle Scholar
  12. 12.
    Lack, S., Sobociński, P.: Adhesive categories. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol. 2987, pp. 273–288. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  13. 13.
    Rensink, A.: Representing first-order logic by graphs. In: Ehrig, H., Engels, G., Parisi-Presicce, F., Rozenberg, G. (eds.) ICGT 2004. LNCS, vol. 3256, pp. 319–335. Springer, Heidelberg (2004)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • Annegret Habel
    • 1
  • Karl-Heinz Pennemann
    • 1
  1. 1.Carl v. Ossietzky Universität OldenburgGermany

Personalised recommendations