Download Graph Transformation: 8th International Conference, ICGT 2015, Held as Part of STAF 2015, L'Aquila, Italy, July 21-23, 2015. Proceedings PDF

TitleGraph Transformation: 8th International Conference, ICGT 2015, Held as Part of STAF 2015, L'Aquila, Italy, July 21-23, 2015. Proceedings
File Size12.5 MB
Total Pages292
Table of Contents
From Software Modeling to System Modeling – Transforming the Change(Keynote)
	Polymorphic Sesqui-Pushout Graph Rewriting
		1 Introduction
		2 Sesqui-Pushout Rewriting Framework
		3 Sesqui-Pushout Rewriting Instances
			3.1 Sesqui-Pushout Rewriting of Graphs
			3.2 Sesqui-Pushout Rewriting of Typed Graphs
		4 Example: Version Management
		5 Related Work and Future Research
	Predictive Top-Down Parsing for Hyperedge Replacement Grammars
		1 Introduction
		2 Hyperedge Replacement Grammars
		3 Predictive Top-Down Parsing: From Strings to Graphs
		4 Predictive Top-Down Parsability
		5 Grammar Analysis
		6 Conclusions
	AGREE -- Algebraic Graph Rewriting with Controlled Embedding
		1 Introduction
		2 Preliminaries
			2.1 Examples of Partial Map Classifiers
		3 Algebraic Graph Rewriting with Controlled Embedding
		4 Example: Social Network Anonymization
		5 AGREE Subsumes SqPO and Polarized Node Cloning
			5.1 AGREE Subsumes SqPO Rewriting with Injective Matches
			5.2 AGREE Subsumes Polarized Node Cloning on Graphs
		6 Related Work and Discussion
	Proving Termination of Graph Transformation Systems Using Weighted Type Graphs over Semirings
		1 Introduction
		2 Preliminaries
			2.1 Graphs and Graph Transformation
			2.2 Matrix Interpretations for String Rewriting
			2.3 Ordered Semirings
		3 Weighted Type Graphs
		4 Using Strongly Ordered Semirings
		5 Examples
		6 Finding Weighted Type Graphs and Implementation
		7 Conclusion
	Towards Local Confluence Analysis for Amalgamated Graph Transformation
		1 Introduction
		2 Amalgamated Graph Transformation
		3 Parallel Independence of Rule Schemes
		4 Conflict Analysis for Rule Schemes
		5 Related Work and Conclusion
	Multi-amalgamated Triple Graph Grammars
		1 Introduction and Motivation
		2 Running Example and Preliminaries
			2.1 Consistency Specification with Triple Graph Grammars
		3 Multi-amalgamated Triple Graph Grammars
		4 Operationalizing Multi-amalgamated TGGs
		5 Model Transformation with Multi-amalgamated TGGs
		6 Related Work
		7 Conclusion and Future Work
	Reconfigurable Petri Nets with Transition Priorities and Inhibitor Arcs
		1 Introduction
		2 Reconfigurable Petri Nets
			2.1 Reconfigurable Place/Transition Nets
			2.2 Other Types of Reconfigurable Petri Nets
		3 Motivating Example
		4 Review of M-Adhesive Transformation Systems
		5 Transition Priorities
		6 Inhibitor Arcs
		7 Related Work
		8 Conclusion
	Reachability in Graph Transformation Systems and Slice Languages
		1 Introduction
		2 Graph Transformations
		3 Slices and Slice Languages
			3.1 Slice Languages
			3.2 Sub-Slices and Sub-Decompositions
		4 Elementary Slice Languages Operations
		5 Next Step Automaton
			5.1 Mapping Rules to Slice Decompositions
			5.2 Mapping Layers of Rewriting Rules into Unit Decompositions
			5.3 Applying Sliced Layers of Rules to Unit Decompositions
		6 Proofs of Our Main Results
		7 Conclusion
	Equational Reasoning with Context-Free Families of String Diagrams
		1 Introduction
		2 Preliminaries
			2.1 B-edNCE Grammars
			2.2 String Graphs and Rewriting
		3 Encoded String Graphs and B-ESG Grammars
		4 B-ESG Rewrite Patterns
		5 Transforming B-ESG Grammars
		6 Conclusion and Future Work
	Translating Essential OCL Invariants to Nested Graph Constraints Focusing on Set Operations
		1 Introduction
		2 Essential OCL Invariants
		3 Nested Graph Constraints
		4 Translation of Essential OCL Invariants
		5 Related Work
		6 Conclusion
	Characterizing Conflicts Between Rule Application and Rule Evolution in Graph Transformation Systems
		1 Introduction
		2 Background
		3 Evolution of Graph Transformation Systems
		4 Inter-level Conflicts
		5 Inter-level Confluence
		6 Inter-level Critical Pair Analysis
		7 Related Work
		8 Concluding Remarks
Applications: Technical Papers
	Graph Pattern Matching as an Embedded Clojure DSL
		1 Introduction
		2 Pattern Matching
		3 In-Place Transformations
		4 Related Work
			4.1 Embedded Model Transformation DSLs
			4.2 Graph Pattern Matching and Transformation Languages
		5 Conclusion
	Using Graph Transformations for Formalizing Prescriptions and Monitoring Adherence
		1 Introduction
		2 Medication Management Process
		3 Related Work
		4 A GT-Based Method to Formalize Prescriptions
			4.1 Interface Language
			4.2 Rx Graph Model
			4.3 Rx Graph Compilation
			4.4 Adherence Tracking
		5 Evaluation
		6 Conclusions and Future Work
	Towards Compliance Verification Between Global and Local Process Models
		1 Introduction
		2 Process Modelling in BPMN
			2.1 Global Behaviour
			2.2 Modelling Local Behaviour in BPMN
		3 Implementation in GROOVE
		4 A Case Study: The Settlement Process
			4.1 BPMN Collaboration Diagram of the Settlement Process
			4.2 Translation of the BPMN Collaboration Diagram into an LTL-Formula
			4.3 Example of a Correct Specification of Local Behaviour
			4.4 Example of an Incorrect Specification of Local Behaviour
			4.5 Test Results
		5 Related Work
		6 Discussion and Outlook
	Inductive Invariant Checking with Partial Negative Application Conditions
		1 Introduction
		2 Foundations
		3 Restrictions, Constructions, and Implication
			3.1 Constructions
			3.2 Implication
		4 Inductive Invariant Checking
			4.1 Step 2: Construction of Target Patterns
			4.2 Step 3: Construction of Source Patterns
			4.3 Step 4: Analysis of Source Patterns and Counterexamples
		5 Evaluation and Discussion
		6 Related Work
		7 Conclusion and Future Work
Applications: Tool Presentations
	Tool Support for Multi-amalgamated Triple Graph Grammars
		1 Introduction and Motivation
		2 Running Example
		3 Multi-amalgamated TGGs with eMoflon
		4 Related Work and Evaluation with Comparison
		5 Conclusion and Future Work
	Uncover: Using Coverability Analysis for Verifying Graph Transformation Systems
		1 Introduction
		2 Design and Usage
		3 Decidability Results
			3.1 Minor Ordering
			3.2 Subgraph Ordering
		4 Case Studies
		5 Future Development
	Local Search-Based Pattern Matching Features in EMF-IncQuery
		1 Introduction
		2 Model Queries with EMF-IncQuery
			2.1 Running Example: Anti-pattern Detection in Java Programs
			2.2 Graph Patterns
			2.3 The Query Development Environment of IncQuery
		3 Local-Search Pattern Matching in IncQuery
			3.1 Executing a Local Search Based Matching Strategy
			3.2 Local Search Support in IncQuery
		4 Debugging Model Queries with Local Search
		5 Related Work
		6 Conclusion and Future Work
Author Index
Document Text Contents
Page 1

Francesco Parisi-Presicce
Bernhard Westfechtel (Eds.)





8th International Conference, ICGT 2015
Held as Part of STAF 2015
L'Aquila, Italy, July 21–23, 2015, Proceedings


Page 2

Lecture Notes in Computer Science 9151

Commenced Publication in 1973
Founding and Former Series Editors:
Gerhard Goos, Juris Hartmanis, and Jan van Leeuwen

Editorial Board

David Hutchison
Lancaster University, Lancaster, UK

Takeo Kanade
Carnegie Mellon University, Pittsburgh, PA, USA

Josef Kittler
University of Surrey, Guildford, UK

Jon M. Kleinberg
Cornell University, Ithaca, NY, USA

Friedemann Mattern
ETH Zurich, Zürich, Switzerland

John C. Mitchell
Stanford University, Stanford, CA, USA

Moni Naor
Weizmann Institute of Science, Rehovot, Israel

C. Pandu Rangan
Indian Institute of Technology, Madras, India

Bernhard Steffen
TU Dortmund University, Dortmund, Germany

Demetri Terzopoulos
University of California, Los Angeles, CA, USA

Doug Tygar
University of California, Berkeley, CA, USA

Gerhard Weikum
Max Planck Institute for Informatics, Saarbrücken, Germany

Page 146

134 M. de Oliveira Oliveira

the application of one layer of transformation rules if and only if there exists
unit decompositions U1 ∈ L(A(R, ξ1, ..., ξc)) and U2 ∈ Δ(inv(U,αun)) such
that α(U1 ⊗ U2) is a unit decomposition of H.

The proof of Lemma 9, which is lengthy and technically involved, will be
available in the full version of this paper. Recall that if A is a slice automaton,
then N (A) denotes the slice automaton whose graph language consists of all
possible graphs that can be obtained from graphs in LG(A) by the application
of one layer of transformation rules (See Theorem 6). As a corollary of Lemma 9
we have that the slice automaton N (A) can be defined from A by the application
of a constant number of elementary slice language operations.

Corollary 10. Let R be a set of graph transformation rules, αun be the uncol-
oring projection defined in the beginning of this section, and α be the projection
of Lemma 9. Let N (A) be the slice automaton defined in Theorem 6. Then

N (A) = A ∪ α[A(R, ξ1, ...ξc) ⊗ Δ(inv(A,αun))] ∩ A(Σ(c · ‖R‖, Γ1, Γ2)).
Finally, by combining Corollary 10 with Lemma 5 we have that the automaton
N (A) can be constructed in time 2O(c·‖R‖ log ‖R‖) · |A|. This proves Theorem 6.


6 Proofs of Our Main Results

We start by proving Proposition 1 which says that it is NP-complete to determine
whether a given graph G of unbounded cutwidth can be transformed into a given
graph H in depth d = 5.

Proof of Proposition 1. We show that the problem of determining whether a
graph H can be derived from a graph G in depth d = 5 is NP-complete. The
proof is by reduction from the Hamiltonian path problem. It is well known that
determining whether a graph G has a Hamiltonian path is NP-complete even if
G has maximum degree 3. On the other hand, by Vising’s theorem, the edges of
any graph of degree 3 can be colored with 4 colors in such a way that no two
adjacent edges have the same color. Now let G have n vertices, and let H be the
graph consisting of a line with n vertices. Then we have that G has a Hamiltonian
path if and only if H is a subgraph of G. Our transformation system consists of
8 transformation rules r1, ..., r4 and r′1, ..., r

4. For each i ∈ {1, ..., 4}, ri takes an

edge e and colors it with the color i. In the opposite direction, each r′i takes an
edge e of color i, and deletes it, leaving only its endpoints in the graph. Then
the process of testing whether G has a Hamiltonian path can be determined in
the following way. Assume G has a Hamiltonian path p = First, we
color into a single transformation step all edges of G not belonging to p in such a
way that no two adjacent edges have the same color. Subsequently we apply four
parallel transformation steps. At step i, we erase all edges colored with i. Since
no two edges with the same color are adjacent, such operation is well defined.
At the end of this process, only the edges of the Hamiltonian path p remain in

Page 147

Reachability in Graph Transformation Systems and Slice Languages 135

the graph. Therefore, since H is isomorphic to p we have that H can be derived
from G in 5 parallel steps. ��
Before proceeding with the proofs of Theorems 2 and 3, we state a theorem
which says that for any connected graph H of cutwidth at most c, one can con-
struct in time 2O(c log c) · |H|O(c) a normalized saturated slice automaton A(H, c)
generating precisely the unit decompositions of H of width at most c.

Theorem 11. Let H be a connected (Γ1, Γ2)-labeled digraph of cutwidth at
most c. One can construct in time 2O(c log c) · |H|O(c) a normalized saturated
slice automaton A(H, c) over the slice alphabet Σ(c, Γ1, Γ2) such that

L(A(H, c)) = {U ∈ L(Σ(c, Γ1, Γ2)) |

U= H}.

Note that the graph language of A(H, c) has a unique graph, which is H itself.
In other words, LG(A(H, c)) = {H}. The importance of Theorem 11 for our
framework stems from the fact that that it allows us to verify in polynomial time
whether a graph H belongs to the graph language of an arbitrary normalized
slice automaton A. We observe that if A is not saturated, then some graphs in
the graph language LG(A) may correspond to few unit decompositions in the
slice language L(A). In this way to verify whether a graph H belongs to LG(A)
we have test for each unit decomposition U of H whether U ∈ L(A). If this
test is positive for one unit decomposition, then H is in the graph language
represented by A. However, enumerating all unit decompositions of a graph H
may take exponential time. Theorem 11 allows us to circumvent this problem.
Since A(H, c) is saturated, we have that H ∈ LG(A) if and only if the slice
language generated by A ∩ A(H, c) is non-empty. This non-emptiness test can
be performed in time |A| · |A(H, c)| = |A| · HO(c).
Proof of Theorem 2. Let G be a (Γ1, Γ2)-labeled graph of cutwidth at most
c. Using the results in [20] one can find, in time 2O(c) · |G|, an ordering ω =
(v1, v2, ..., vn) of the vertex of V such that maxi |E({v1, ..., vi}, {vi+1, ..., vn})| ≤
c. Now we can construct in time linear in |G| a unit decomposition U = S1S2...Sn
of G over the alphabet Σ(c, Γ1, Γ2) by letting vi be the center vertex of Si.

Now let A(U) be the slice automaton over Σ(c, Γ1, Γ2) which accepts a
unique unit decomposition, which is U itself. Then we have that |A| = O(|G|),
L(A(U)) = {U} and LG(A) = {G}. By Corollary 7 we can construct in time

d·log |R|) · |G| a slice automaton A(R, G, d) = N d(A) over the slice alpha-
bet Σ(c · ‖R‖d, Γ1, Γ2) whose graph language LG(A(R, G, d)) consists precisely
of the set of graphs that can be obtained from LG(A) by the application of one
layer of transformation rules.

Now let H be a another (Γ1, Γ2)-labeled graph, and let c′ = c · ‖R‖d If the
cutwidth of H is greater than c′, then H cannot be reached from G in depth
at most d, and thus in this case our algorithm returns No. On the other hand,
if the cut-width of H is at most c′, then by Theorem 11, one can construct
in time 2O(c

′ log c′) · |H|O(c′) a saturated slice automaton A(H, c′) over the slice
alphabet Σ(c′, Γ1, Γ1) such that the graph language LG(A(H, c)) = {H}. There-
fore, since A(H, c) is saturated, we have that H belongs to the graph language

Page 291

282 M. Búr et al.

6 Conclusion and Future Work

In this paper, we described a novel feature of the EMF-IncQuery framework,
the support of local search-based pattern matching in addition to the previously
available incremental evaluation. By reusing the existing pattern language and
query development environment, it is possible to select the most appropriate
strategy without modifications to already developed patterns. Furthermore, we
presented a prototype graphical debugger that helps understanding complex
patterns by visualizing the execution of the search process. Both contributions
are included in the EMF-IncQuery project.

In the future, we plan to improve the local search support by providing a
model-sensitive planner for local search [5], that is expected to enhance the per-
formance. Another promising idea is the support of hybrid pattern matching [11]:
by mixing incrementally evaluated and local search-based pattern matching, it
is possible to fine-tune the performance characteristics (memory footprint or
execution time), extending the range of problems that can be addressed.


1. Ujhelyi, Z., Szõke, G., Ákos Horvth, Csiszár, N.I., Vidács, L., Varró, D., Ferenc,
R.: Performance comparison of query-based techniques for anti-pattern detection.
Information and Software Technology (0) (2015) - Accepted

2. Ujhelyi, Z., Bergmann, G., Hegeds, Á., Horváth, Á., Izsó, B., Ráth, I., Szatmári, Z.,
Varró, D.: EMF-Incquery: an integrated development environment for live model
queries. Sci. Comput. Program. 98(1), 80–99 (2015)

3. Nickel, U., Niere, J., Zündorf, A.: Tool demonstration: The FUJABA environ-
ment. In: Proceedings of the 22nd International Conference on Software Engineer-
ing (ICSE 2000), pp. 742–745. ACM Press, Limerick, Ireland (2000)

4. Geiß, R., Batz, G.V., Grund, D., Hack, S., Szalkowski, A.: GrGen: a fast spo-
based graph rewriting tool. In: Corradini, A., Ehrig, H., Montanari, U., Ribeiro,
L., Rozenberg, G. (eds.) ICGT 2006. LNCS, vol. 4178, pp. 383–397. Springer,
Heidelberg (2006)

5. Varró, G., Deckwerth, F., Wieber, M., Schürr, A.: An algorithm for generating
model-sensitive search plans for emf models. In: Hu, Z., de Lara, J. (eds.) ICMT
2012. LNCS, vol. 7307, pp. 224–239. Springer, Heidelberg (2012)

6. Oracle: Enterprise Manager (2015).

7. Seifert, M., Katscher, S.: Debugging triple graph grammar-based model transfor-
mations. In: Fujaba Days, pp. 19–25 (2008)

8. Horn, T.: Model querying with funnyQT. In: Duddy, K., Kappel, G. (eds.) ICMB
2013. LNCS, vol. 7909, pp. 56–57. Springer, Heidelberg (2013)

9. Eclipse OCL Project: MDT-OCL website (2015).

10. IBM Software: InfoSphere Data Architect (2015).

11. Horváth, Á., Bergmann, G., Ráth, I., Varró, D.: Experimental assessment of com-
bining pattern matching strategies with VIATRA2. Int. J. Softw. Tools Technol.
Transfer 12(3–4), 211–230 (2010)

Page 292

Author Index

Anjorin, Anthony 87, 257
Arendt, Thorsten 155

Becker, Jan Steffen 155
Bruggink, H.J. Sander 52
Búr, Márton 275

Corradini, Andrea 35

de Oliveira Oliveira, Mateus 121
Diemert, Simon 205
Drewes, Frank 19
Duval, Dominique 35
Dyck, Johannes 237

Echahed, Rachid 35

Giese, Holger 237
Golas, Ulrike 69

Habel, Annegret 155
Heckel, Reiko 171
Hoffmann, Berthold 19
Horn, Tassilo 189
Horváth, Ákos 275

Kissinger, Aleks 138
Kleijn, Jetty 221
König, Barbara 52
Kwantes, Pieter M. 221

Leblebici, Erhan 87, 257
Löwe, Michael 3

Machado, Rodrigo 171
Minas, Mark 19

Nolte, Dennis 52

Padberg, Julia 104
Price, Morgan 205
Prost, Frederic 35

Radke, Hendrik 155
Rensink, Arend 221
Ribeiro, Leila 35, 171

Schürr, Andy 87, 257
Stückrath, Jan 266

Taentzer, Gabriele 69, 87, 155

Ujhelyi, Zoltán 275

Van Gorp, Pieter 221
Varró, Dániel 275

Weber, Jens H. 205

Zamdzhiev, Vladimir 138
Zantema, Hans 52

Similer Documents