M-Adhesive Transformation Systems with Nested Application Conditions. Part 2: Embedding, Critical Pairs and Local Confluence

• Autorzy: Ehrig H. , Golas U. , Habel A. , Lambers L. , Orejas F.
• Języki publikacji: EN

Abstrakty

EN

Graph transformation systems have been studied extensively and applied to several areas of computer science like formal language theory, the modeling of databases, concurrent or distributed systems, and visual, logical, and functional programming. In most kinds of applications it is necessary to have the possibility of restricting the applicability of rules. This is usually done by means of application conditions. In this paper, we continue the work of extending the fundamental theory of graph transformation to the case where rules may use arbitrary (nested) application conditions. More precisely, we generalize the Embedding theorem, and we study how local confluence can be checked in this context. In particular, we define a new notion of critical pair which allows us to formulate and prove a Local Confluence Theorem for the general case of rules with nested application conditions. All our results are presented, not for a specific class of graphs, but for any arbitraryM-adhesive category, which means that our results apply to most kinds of graphical structures. We demonstrate our theory on the modeling of an elevator control by a typed graph transformation system with positive and negative application conditions.

Słowa kluczowe

EN

M-adhesive transformation systems; M-adhesive categories; graph replacement categories; nested application conditions; embedding; critical pairs; local confluence

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2012
• Tom: Vol. 118, nr 1-2
• Strony: 35--63
• Opis fizyczny: Bibliogr. 30 poz., rys.

Twórcy

autor

Ehrig H.

autor

Golas U.

autor

Habel A.

autor

Lambers L.

autor

Orejas F.

• Fachgebiet Systemanalyse und Modellierung, Hasso-Plattner-Institut f¨ur Softwaresystemtechnik GmbH, Prof.-Dr.-Helmert-Str. 2-3, 14482 Potsdam,

Bibliografia

• [1] Baader, F., Nipkow, T.: Term Rewriting and All That, Cambridge University Press, Cambridge, 1998.
• [2] Baldan, P., Gadducci, F., Sobocinski, P.: Adhesivity Is Not Enough: Local Church-Rosser Revisited, Mathematical Foundations of Computer Science (MFCS 2011), 6907, 2011, 48-59.
• [3] Courcelle, B.: The Expression of Graph Properties and Graph Transformations in Monadic Second-Order Logic, in: Handbook of Graph Grammars and Computing by Graph Transformation, vol. 1,World Scientific, 1997, 313-400.
• [4] Ehrig, H., Ehrig, K., Habel, A., Pennemann, K.-H.: Theory of Constraints and Application Conditions: From Graphs to High-Level Structures, Fundamenta Informaticae, 74(1), 2006, 135-166.
• [5] Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamental Theory of Typed Attributed Graph Transformation based on Adhesive HLR-Categories, Fundamenta Informaticae, 74(1), 2006, 31-61.
• [6] Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic Graph Transformation, EATCS Monographs of Theoretical Computer Science, Springer, 2006.
• [7] Ehrig, H., Golas, U., Habel, A., Lambers, L., Orejas; F.: M-Adhesive Transformation Systems with Nested Application Conditions.Part 1: Parallelism, Concurrency and Amalgamation, Mathematical Structures in Computer Science, 2012. To appear.
• [8] Ehrig, H., Golas, U., Hermann, F.: Categorical Frameworks for Graph Transformation and HLR Systems based on the DPO Approach, Bulletin of the EATCS, 102, 2010, 111-121.
• [9] Ehrig, H., Habel, A., Kreowski, H.-J., Parisi-Presicce, F.: Parallelism and Concurrency in High Level Replacement Systems, Mathematical Structures in Computer Science, 1, 1991, 361-404.
• [10] Ehrig, H., Habel, A., Lambers, L., Orejas, F., Golas, U.: Local Confluence for Rules with Nested Application Conditions, Graph Transformations - 5th International Conference, ICGT 2010, 6372, Springer-Verlag, 2010, 330-345.
• [11] Ehrig, H., Habel, A., Parisi-Presicce, F.: Basic Results for Two Types of High-Level Replacement Systems, GETGRATS, 51, 2002.
• [12] Geiß, R., Batz, G. V., Grund, D., Hack, S., Szalkowski, A.: GrGen: A fast SPO-based graph rewriting tool, Graph Transformations (ICGT 2006), 4178, Springer, 2006, 383-397.
• [13] Golas, U.: Analysis and Correctness of Algebraic Graph and Model Transformations, Ph.D. Thesis, Technische Universität Berlin, Vieweg + Teubner, 2011.
• [14] Habel, A., Heckel, R., Taentzer, G.: Graph Grammars with Negative Application Conditions, Fundamenta Informaticae, 26, 1996, 287-313.
• [15] Habel, A., Müller, J., Plump, D.: Double-PushoutGraph Transformation Revisited, Mathematical Structures in Computer Science, 11(5), 2001, 637-688.
• [16] Habel, A., Pennemann, K.-H.: Nested Constraints and Application Conditions for High-Level Structures, Formal Methods in Software and System Modeling, 3393, Springer, 2005, 293-308.
• [17] Habel, A., Pennemann, K.-H.: Correctness of High-Level Transformation Systems Relative to Nested Conditions, Mathematical Structures in Computer Science, 19, 2009, 245-296.
• [18] Knuth, N. E., Bendix, P. B.: SimpleWord Problems in Universal Algebra, In J. Leech, editor, Computational Problems in Abstract Algebra, 1970, 263-297.
• [19] Koch,M., Mancini, L. V., Parisi-Presicce, F.: Graph-based Specification of Access Control Policies, Journal of Computer and System Sciences, 71, 2005, 1-33.
• [20] Lack, S., Soboci´nski, P.: Adhesive and Quasiadhesive Categories, Theoretical Informatics and Application, 39(2), 2005, 511-546.
• [21] Lambers, L.: Certifying Rule-Based Models using Graph Transformation, Ph.D. Thesis, Technische Universit ät Berlin, 2010.
• [22] Löwe, M.: Algebraic Approach to Single-Pushout Graph Transformation, Theoretical Computer Science, 109, 1993, 181-224.
• [23] Newman, M. H. A.: On theories with a combinatorial definition of "equivalence", Annals of Mathematics, 43(2), 1942, 223-243.
• [24] Orejas, F., Ehrig, H., Prange, U.: A Logic of Graph Constraints, Fundamental Approaches to Software Engineering (FASE 2008), 4961, 2008, 179-198.
• [25] Pennemann, K.-H.: Development of Correct Graph Transformation Systems, Ph.D. Thesis, Universität Oldenburg, 2009.
• [26] Plump, D.: Hypergraph Rewriting: Critical Pairs and Undecidability of Confluence, in: Term Graph Rewriting: Theory and Practice, John Wiley, 1993, 201-213.
• [27] Plump, D.: Confluence of Graph Transformation Revisited, Processes, Terms and Cycles: Steps on the Road to Infinity: Essays Dedicated to Jan Willem Klop on the Occasion of His 60th Birthday, 3838, Springer, 2005, 280-308.
• [28] Rensink, A.: Representing first-order logic by graphs, Graph Transformations (ICGT'04), 3256, Springer, 2004, 319-335.
• [29] Rozenberg, G., Ed.: Handbook of Graph Grammars and Computing by Graph Transformation, vol. 1: Foundations, World Scientific, 1997.
• [30] TFS-group, TU Berlin: AGG, http://tfs.cs.tu-berlin.de/agg.