Fundamentals of Algebraic Graph Transformation

by Ehrig, H.; Ehrig, K.; Prange, U.; Taentzer, G.

• ISBN13: 9783540311874
• ISBN10: 3540311874
• Format: Hardcover
• Copyright: 2006-04-15
• Publisher: Springer-Verlag New York Inc

Summary

Graphs are widely used to represent structural information in the form of objects and connections between them. Graph transformation is the rule-based manipulation of graphs, an increasingly important concept in computer science and related fields. This is the first textbook treatment of the algebraic approach to graph transformation, based on algebraic structures and category theory.Part I is an introduction to the classical case of graph and typed graph transformation. In Part II basic and advanced results are first shown for an abstract form of replacement systems, so-called adhesive high-level replacement systems based on category theory, and are then instantiated to several forms of graph and Petri net transformation systems. Part III develops typed attributed graph transformation, a technique of key relevance in the modeling of visual languages and in model transformation. Part IV contains a practical case study on model transformation and a presentation of the AGG (attributed graph grammar) tool environment. Finally the appendix covers the basics of category theory, signatures and algebras.The book addresses both research scientists and graduate students in computer science, mathematics and engineering.

Table of Contents

Part I Introduction to Graph Transformation Systems
1 General Introduction	5	(16)
1.1 General Overview of Graph Grammars and Graph Transformation	5	(5)
1.1.1 What Is Graph Transformation?	6	(1)
1.1.2 Aims and Paradigms of Graph Transformation	6	(3)
1.1.3 Overview of Various Approaches	9	(1)
1.2 The Main Ideas of the Algebraic Graph Transformation Approach	10	(5)
1.2.1 The DPO Approach	11	(1)
1.2.2 The Algebraic Roots	12	(1)
1.2.3 From the DPO to the SPO Approach	13	(1)
1.2.4 From Graphs to High-Level Structures	14	(1)
1.3 The Chapters of This Book and the Main Results	15	(2)
1.3.1 Part I: Introduction to Graph Transformation Systems	15	(1)
1.3.2 Part II: Adhesive HLR Categories and Systems	15	(1)
1.3.3 Part III: Typed Attributed Graph Transformation Systems	16	(1)
1.3.4 Part IV: Case Study and Tool Support	17	(1)
1.3.5 Appendices	17	(1)
1.3.6 Hints for Reading This Book	17	(1)
1.4 Bibliographic Notes and Further Topics	17	(4)
1.4.1 Concepts of Graph Grammars and Graph Transformation Systems	17	(2)
1.4.2 Application Areas of Graph Transformation Systems	19	(1)
1.4.3 Languages and Tools for Graph Transformation Systems	19	(1)
1.4.4 Future Work	20	(1)
2 Graphs, Typed Graphs, and the Gluing Construction	21	(16)
2.1 Graphs and Typed Graphs	21	(4)
2.2 Introduction to Categories	25	(4)
2.3 Pushouts as a Gluing Construction	29	(4)
2.4 Pullbacks as the Dual Construction of Pushouts	33	(4)
3 Graph Transformation Systems	37	(40)
3.1 Basic Definitions for GT Systems	37	(6)
3.2 Construction of Graph Transformations	43	(4)
3.3 Local Church—Rosser and Parallelism Theorems for GT Systems	47	(6)
3.4 Overview of Some Other Main Results for GT Systems	53	(11)
3.4.1 Concurrency Theorem	54	(2)
3.4.2 Embedding and Extension Theorems	56	(3)
3.4.3 Confluence, Local Confluence, Termination, and Critical Pairs	59	(3)
3.4.4 Functional Behavior of GT Systems and Termination Analysis	62	(2)
3.5 Graph Constraints and Application Conditions	64	(13)
Part II Adhesive High-Level Replacement Categories and Systems
4 Adhesive High-Level Replacement Categories	77	(24)
4.1 Van Kampen Squares and Adhesive Categories	77	(9)
4.2 Adhesive HLR Categories	86	(10)
4.3 HLR. Properties of Adhesive HLR Categories	96	(5)
5 Adhesive High-Level Replacement Systems	101	(24)
5.1 Basic Concepts of Adhesive HLR Systems	101	(4)
5.2 Instantiation of Adhesive HLR Systems	105	(4)
5.2.1 Graph and Typed Graph Transformation Systems	106	(1)
5.2.2 Hypergraph Transformation Systems	106	(1)
5.2.3 Petri Net Transformation Systems	107	(1)
5.2.4 Algebraic Specification Transformation Systems	108	(1)
5.2.5 Typed Attributed Graph Transformation Systems	108	(1)
5.3 The Local Church—Rosser and Parallelism Theorems	109	(8)
5.4 Concurrency Theorem and Pair Factorization	117	(8)
6 Embedding and Local Confluence	125	(26)
6.1 Initial Pushouts and the Gluing Condition	125	(5)
6.2 Embedding and Extension Theorems	130	(10)
6.3 Critical Pairs	140	(4)
6.4 Local Confluence Theorem	144	(7)
7 Constraints and Application Conditions	151	(20)
7.1 Definition of Constraints and Application Conditions	152	(4)
7.2 Construction of Application Conditions from Constraints	156	(4)
7.3 Construction of Left from Right Application Conditions	160	(4)
7.4 Guaranteeing and Preservation of Constraints	164	(7)
Part III Typed Attributed Graph Transformation Systems
8 Typed Attributed Graphs	171	(10)
8.1 Attributed Graphs and Typing	172	(5)
8.2 Pushouts as a Gluing Construction of Attributed Graphs	177	(1)
8.3 Pullbacks of Attributed Graphs	178	(3)
9 Typed Attributed Graph Transformation Systems	181	(26)
9.1 Basic Concepts for Typed AGT Systems	181	(7)
9.2 Construction of Typed Attributed Graph Transformations	188	(2)
9.3 Local Church—Rosser and Parallelism Theorem for Typed AGT Systems	190	(4)
9.4 Concurrency Theorem and Pair Factorization for Typed AGT Systems	194	(13)
9.4.1 Pair Factorizations	194	(7)
9.4.2 Concurrency Theorem	201	(6)
10 Embedding and Local Confluence for Typed AGT Systems	207	(14)
10.1 Embedding and Extension Theorems for Typed AGT Systems	207	(8)
10.2 Critical Pairs for Typed AGT Systems	215	(3)
10.3 Local Confluence Theorem for Typed AGT Systems	218	(3)
11 Adhesive HLR Categories for Typed Attributed Graphs	221	(16)
11.1 Attributed Graph Structure Signatures and Typed Attributed Graphs	222	(3)
11.2 Definition of Concrete Adhesive HLR Categories	225	(7)
11.3 Verification of the Main Results for Typed AGT Systems	232	(5)
12 Constraints, Application Conditions and Termination for TAGT Systems	237	(22)
12.1 Constraints and Application Conditions for Typed AGT Systems	237	(5)
12.2 Equivalence of Constraints and Application Conditions	242	(7)
12.3 Termination Criteria for Layered Typed Attributed Graph Grammars	249	(10)
13 Typed Attributed Graph Transformation with Inheritance.	259	(28)
13.1 Attributed Type Graphs with Inheritance	260	(5)
13.2 Attributed Clan Morphisms	265	(6)
13.3 Productions and Attributed Graph Transformation with Inheritance	271	(7)
13.4 Equivalence of Concepts with and without Inheritance	278	(9)
Part IV Case Study on Model Transformation, and Tool Support by AGG
14 Case Study on Model Transformation	287	(18)
14.1 Model Transformation by Typed Attributed Graph Transformation	287	(1)
14.2 Model Transformation from Statecharts to Petri Nets	288	(15)
14.2.1 Source Modeling Language: Simple Version of UML Statecharts	289	(1)
14.2.2 Target Modeling Language: Petri Nets	290	(3)
14.2.3 Model Transformation	293	(8)
14.2.4 Termination Analysis of the Model Transformation	301	(2)
14.3 Further Case Studies	303	(1)
14.3.1 From the General Resource Model to Petri Nets	303	(1)
14.3.2 From Process Interaction Diagrams to Timed Petri Nets	304	(1)
14.4 Conclusion	304	(1)
15 Implementation of Typed Attributed Graph Transformation by AGG	305	(24)
15.1 Language Concepts of AGG	305	(7)
15.1.1 Graphs	306	(1)
15.1.2 Typing Facilities	306	(1)
15.1.3 Node and Edge Attributes	307	(1)
15.1.4 Rules and Matches	308	(2)
15.1.5 Graph Transformations	310	(2)
15.1.6 Graph Grammars
15.2 Analysis Techniques Implemented iii AGG	312	(6)
15.2.1 Graph Constraints	312	(1)
15.2.2 Critical Pair Analysis	313	(4)
15.2.3 Graph Parsing	317	(1)
15.2.4 Termination	318	(1)
15.3 Tool Environment of AGG	318	(4)
15.3.1 Visual Environment
15.3.2 Graph Transformation Engine	321	(1)
15.3.3 Tool Integration	322	(1)
15.4 Conclusion	322	(7)
Appendices
A A Short Introduction to Category Theory	329	(24)
A.1 Categories	329	(1)
A.2 Construction of Categories, and Duality	330	(2)
A.3 Monomorphisms, Epimorphisms, and Isomorphisms	332	(2)
A.4 Pushouts and Pullbacks	334	(6)
A.5 Binary Coproducts and Initial Objects	340	(4)
A.6 Functors, Functor Categories, and Comma Categories	344	(6)
A.7 Isomorphism and Equivalence of Categories	350	(3)
B A Short Introduction to Signatures and Algebras	353	(6)
B.1 Algebraic Signatures	353	(2)
B.2 Algebras	355	(2)
B.3 Terms and Term Evaluation	357	(2)
C Detailed Proofs	359	(18)
C.1 Completion of Proof of Fact 4.24	359	(2)
C.2 Proof of Lemma 6.25	361	(1)
C.3 Completion of Proof of Theorem 11.3	362	(4)
C.3.1 Well-Definedness	362	(2)
C.3.2 Functors	364	(1)
C.3.3 Isomorphism	365	(1)
C.4 Proof of Lemma 11.17	366	(4)
C.4.1 Well-Definedness	366	(1)
C.4.2 Pushout Property	367	(1)
C.4.3 Initial Pushout	368	(2)
C.5 Proof of Theorem 13.12	370	(3)
C.6 Proof of Lemma 13.20	373	(4)
References	377	(8)
Index	385