ICGT 2008

4th International Conference on Graph Transformation
Leicester (United Kingdom), September 07 - 13, 2008

Main Page

Scope of the Conference


Program Committee


Important Dates

Submission details

Invited Speakers

Satellite Events



Travel Information

Conference Site

Monday, 8th

Tuesday, 9th

Wednesday, 10th

Thursday, 11th

Friday, 12th

Saturday, 13th















Main Conference
(including Doctoral Symposium)








Social Dinner

Main Conference Program


Reiko Heckel
Tutorial: Foundations and Applications of Graph Transformation
9.00 - 10.30 Tutorial, Session I: Foundations and Modelling
11.00 - 12.30 Tutorial, Session II: Model Transformation and Semantics

13.45 - 14.00 Opening

14.00 - 16.00
Hypergraph and Termgraph Rewriting

Steffen Mazanek, Sonja Maier and Mark Minas
An Algorithm for Hypergraph Completion according to Hyperedge Replacement Grammars

Abstract: The algorithm of Cocke, Younger and Kasami is a dynamic programming technique well-known from string parsing. It has been adopted to graphs successfully by Lautemann. Therewith, many practically relevant graph languages generated by hyperedge replacement can be parsed in an acceptable time. In this paper we propose an extension of this algorithm that allows for graph completion. If only a few graph components are missing, this algorithm is reasonably efficient and can be directly used, among other things, for auto-completion in the context of graph grammar based diagram editors.

Jérémie Chalopin, Antoni Mazurkiewicz and Yves Métivier
Labelled (Hyper)Graphs, Negotiations and the Naming Problem

Abstract: We consider four different models of process interactions that unify and generalise models introduced and studied by Angluin et al. and models introduced and studied by Mazurkiewicz.We encode these models by labelled (hyper)graphs and relabelling rules
on this labelled (hyper)graphs called negotiations. Then for these models, we give complete characterisations of labelled graphs
in which the naming problem can be solved. Our characterizations are expressedin terms of locally constrained homomorphisms that are generalisations of known graph homomorphisms.

Stefan Rieger and Thomas Noll
Abstracting Complex Data Structures by Hyperedge Replacement

Abstract: We present a novel application of hyperedge replacement grammars, showing that they can serve as an intuitive formalism for abstractly modeling dynamic data structures.
One aim of our framework is to extend finite-state verification techniques to handle pointer-manipulating programs operating on complex dynamic data structures that are potentially unbounded in their size.
The idea is to represent both abstraction mappings on user-defined dynamic data structures and the (abstract) semantics of pointer-manipulating operations using graph grammars, supporting a smooth integration of the two aspects. We demonstrate how our framework can be employed for analysis and verification purposes, e.g., to prove that it retains structural invariants of the heap.

Rachid Echahed
Inductively Sequential Term-graph Rewrite Systems

Abstract: Definitional trees have been introduced by Sergio Antoy in order to design an efficient term rewrite strategy which computes needed
outermost redexes. In this paper, we consider the use of definitional trees in the context of term-graph rewriting. We show that, unlike the
case of term rewrite systems, the strategies induced by definitional trees do not always compute needed redexes, in presence of term-graph
rewrite systems. We then define a new class called inductively sequential term-graph rewrite systems (istGRS) for which needed
redexes are still provided by definitional trees. Systems in this class are not confluent in general. We give additional syntactic
criteria over istGRS's which ensure the confluence property with respect to the set of admissible term-graphs.

16.30 - 18.30
Applications of Graph Transformation

Bilel Derbel, Mohamed Mosbah and Stefan Gruner
Mobile Agents For Implementing Local Computations in Graphs

Abstract: Mobile agents are a recent paradigm to facilitate the design and programming of distributed applications. However, whilst their popularity continues to grow, a uniform theory of mobile agent systems is not yet sufficiently elaborated, in comparison with classical models of distributed computation. In this paper we show how to use mobile agents as an alternative model for implementing distributed local computation rules. In doing so, we approach a general and unified framework for local computations which is consistent with the classical theory of distributed computations based on graph relabeling systems.

Fabio Gadducci and Giacoma Monreale
A decentralized implementation of mobile ambients

Abstract: We present a graphical implementation for finite processes of the mobile ambients calculus. Our encoding uses unstructured (i.e., non hierarchical) graphs and it is sound and complete with respect to the structural congruence of the calculus (that is, two processes are
equivalent iff they are mapped into isomorphic graphs). With respect to alternative proposals for the graphical implementation of mobile
ambients, our encoding distinguishes the syntactic structure of a process from the activation order of a process components.  Our
solution faithfully captures a basic feature of the calculus (ambients can be nested and reductions are propagated across ambient nesting)
and it allows to model the reduction semantics via a graph transformation system containing just three rules.

Pietro Cenciarelli, Daniele Gorla and Emilio Tuosto
Network Applications of Graph Bisimulation

Abstract: Synchronising Graphs is a system of parallel graph transformation designed for modeling process interaction in a network environment. We propose a theory of context-free synchronising graphs and a novel notion of bisimulation equivalence which is shown to be a congruence with respect to graph composition and node restriction. We use this notion of equivalence to study some sample network applications, and show that our bisimulation equivalence captures precisely notions like functional equivalence of logical switches, equivalence of channel implementations and level of fault tolerance of a network.

Mathieu Poudret, Agnès Arnould, Jean-Paul Comet and Pascale Le Gall
Graph Transformation for Topology Modelling

Abstract: In this paper we present a formalism of meta-rules of graph transformation to express an infinite class of semantically related graph transformation rules in the context of pure topological modelling with G-maps. This formalism has been motivated by specific operations to be done on topological representation of objects in computer graphics, especially for simulation of complex structured systems where rearrangements of compartments is subject to change. We also define application of such meta-rules and prove that meta-rules application preserves some necessary conditions for G-maps.


9.00 - 10.00 Invited talk

Perdita Stevens
Towards an algebraic theory of bidirectional transformations

10.30 - 12.30
Execution of Graph Transformations

Leen Lambers, Hartmut Ehrig, Ulrike Prange and Fernando Orejas
Embedding and Confluence of Graph Transformations with Negative Application Conditions

Abstract: The goal of this paper is the generalization of embedding and confluence results for graph transformation systems to transformation
systems with negative application conditions (NACs). These conditions restrict the application of a rule by expressing that a specific structure
must not be present before or after applying the rule to a certain context. Such a condition influences each rule application and transformation and therefore changes significantly the properties of the transformation system. This behavior modification is reflected by the generalization of the Embedding Theorem and the Critical Pair Lemma or Local Confluence Theorem, formulated already for graph transformation systems without negative application conditions. The results hold for adhesive high-level replacement systems with NACs and are formulated in this paper for the instantiation to double-pushout graph transformation systems with NACs. All constructions and results are explained on a running example.

Hartmut Ehrig and Ulrike Prange
Formal Analysis of Model Transformations Based on Triple Graph Rules with Kernels

Abstract: Triple graph transformation has become an important approach for model transformations. Triple graphs consist of a source, a target and a connection graph. The corresponding rules also contain these parts and describe the simultaneous construction of both the source and the target model. From these rules, forward rules can be derived which describe the model transformation from a given source model to a target model. The forward transformation must be source consistent in order to define a valid model transformation. Source consistency implies that the source and the target model correspond to each other according to a triple transformation.
In this paper, the relationship between the source consistency of forward transformations, and NAC consistency and termination used in other model transformation approaches is analysed from a formal point of view. We define the kernel of a forward rule and construct NACs based on this kernel. Then we give sufficient conditions such that source consistency implies NAC consistency and termination. Moreover, we analyse how to achieve local confluence independent of source consistency. Both results together provide sufficient conditions for functional behaviour of model transformations. Our results are illustrated by an example describing a model transformation from activity diagrams to CSP.

Frank Drewes, Berthold Hoffmann and Mark Minas
Adaptive Star Grammars for Graph Models

Abstract: Adaptive star grammars generalize well-known graph grammar formalisms based on hyperedge and node replacement while retaining parseability, and commutativity and associativity of rules. In this paper, we study how these grammars can be put to practical use for the definition of graph models. We define program graphs, which are models of object-oriented programs that have been devised for investigating refactoring operations. Using some notational enhancements and one proper extension (by application conditions), we develop an adaptive star grammar for program graphs in a systematic way. The grammar defines the shape of program graphs, comprising not only the nested composition of entities, but scope rules for their declarations as well. Such properties cannot easily be defined by meta-models like UML class diagrams. Vice versa, adaptive star grammars cover several aspects of class diagrams, and can be extended to capture the rest. Conformance of graphs to an adaptive star grammar can be checked by a parsing algorithm that is extended by the checking of predicates.

Karl Azab and Annegret Habel
High-level programs and program conditions

Abstract: High-level conditions are well-suited for expressing structural properties. They can describe the precondition and the postcondition for a high-level program, but they cannot describe the relationship between the input and the output of a program derivation. Therefore, we investigate program conditions, a generalized type of conditions expressing properties on program derivations. Program conditions look like nested rules with application conditions. We present a normal form result, a suitable graphical notation, and conditions under which a satisfying program can be constructed from a program condition. We define a sequential composition on program conditions and show that, for a suitable type of program conditions with a complete dependence relation we have that: Whenever the original programs satisfy the original program conditions, then the composed program satisfies the composed program condition.

12.30 - 14.00 Meeting of the ICGT Steering Committee

14.00 - 15.20 Doctorol Symposium, Applications I

Hong Qing Yu and Yi Hong
Graph Transformation for the Semantic Web: Queries and Inference rules

Pieter Van Gorp
Model-Driven Development of Model Transformations

Duc-Hanh Dang
Triple Graph Grammars and OCL for Validating System Behavior

Erhard Weinell
Transformation-based operationalization of Graph Languages

14.00 - 15.20 Doctorol Symposium, Foundations I

Dénes Bisztray
Verification of Architectural Refactorings: Rule Extraction and Tool Support

Tobias Heindel
Grammars Morphisms and Weakly Adhesive Categories

Karl-Heinz Pennemann
Development of Correct Graph Transformation Systems

Frank Hermann
Process Construction and Analysis for Workflows modelled by Adhesive HLR Systems with Application Conditions

15.40 - 17.00 Doctorol Symposium, Applications II

Carlos Matos
Service Extraction from Legacy Systems

Michael Striewe
Using a Triple Graph Grammar for State Machine implementations

Ákos Horváth
Towards a Two Layered Verification Approach for Compiled Graph Transformation

Ajab Khan
Model-based Analysis of Network Reconfigurations using Graph Transformation Systems

15.40 - 17.00 Doctorol Symposium, Foundations II

Filippo Bonchi
Abstract Semantics by Observable Contexts

Mohammad Hammoudeh
Modelling Clustering of Sensor Networks with Synchronised Hyperedge Replacement

Mike Dodds
From Separation Logic to Hyperedge Replacement and Back

Davide Grohmann
Security, cryptography and directed bigraphs

18.30 - 24.00 Excursion and Social Dinner

Busses leave at 18.30 from Stamford Hall.


9.00 - 10.00 Invited talk

Wil van der Aalst
Discovery Verification and Conformance of Workflows with Cancellation

10.30 - 12.30
Validation and Verification

Fernando Orejas
Attributed graph constraints

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, in a previous paper, we showed 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). Moreover, in that paper we present a sound and complete proof system for reasoning with this kind of constraints. Those results apply, in principle, to any category satisfying some given properties. However, the category of (typed) attributed graphs does not satisfy these properties. In particular, the proof rules introduced for reasoning with standard graph constraints  allow us to infer infinitary formulas, making the logic incomplete. In addition, using the straighforward generalization of standard graph constraints, there is no obvious way of stating properties about the attributes of the given graphs.
In this paper we introduce a new formulation for (typed) attributed graph constraints. More precisely, the idea is to see these constraints as standard graph constraints whose attributes are just variables, together with a logic formula that expresses properties that must be satisfied by these attributes. Then a proof system, which extends the one introduced in a previous paper, is presented and it is shown to be sound and complete

Karl-Heinz Pennemann
Resolution-like theorem proving for high-level conditions

Abstract: The tautology problem is the problem to prove the validity of statements. In this paper, we present a calculus for this undecidable problem on graphical conditions, prove its correctness, investigate the necessity of each deduction rule, and discuss practical aspects concerning an implementation. As we use the framework of weak adhesive HLR categories, the calculus is applicable to a number of replacement capable structures, such as Petri-Nets, graphs or hypergraphs.

Barbara König and Vitali Kozioura
Towards the Verification of Attributed Graph Transformation Systems

Abstract: In this paper we describe an approach for the verification of attributed graph transformation systems (AGTS). AGTSs are standard
graph transformation systems where graphs are labelled over an algebra. We base our verification procedure on so-called
approximated unfoldings combined with counterexample-based abstraction refinement. Both techniques were originally developed
for non-attributed systems. With respect to refinement we focus especially on detecting whether the spurious counterexample is
caused by structural over-approximation or by an abstraction of the attributes which is too coarse. The technique is implemented in the
verification tool Augur 2 and a leader election protocol has been successfully verified.

Jörg Bauer, Iovka Boneva, Marcos E. Kurbán and Arend Rensink
A Modal-Logic Based Graph Abstraction

Abstract: Infinite or very large state spaces often prohibit the successful verification of graph transformation systems. Abstract graph transformation is an approach that tackles this problem by abstracting graphs to abstract graphs of bounded size and by lifting application of productions to abstract graphs. In this work, we present a new framework of abstractions unifying and generalising existing takes on abstract graph transformation. The precision of the abstraction can be adjusted according to the properties to be verified facilitating abstraction
refinement. We present a modal logic defined on graphs, which is preserved and reflected by our abstractions.
Finally, we demonstrate the usability of the framework by verifying a graph transformation model of a firewall.

14.00 - 16.00
Graph Languages and Special Transformation Concepts

H.J. Sander Bruggink and Barbara König
On the Recognizability of Arrow and Graph Languages

Abstract: In this paper we give a category-based characterization of recognizability. A recognizable subset of arrows is defined via a
functor into the category of relations on sets, which can be seen as a straightforward generalization of a finite automaton. In the
second part of the paper we apply the theory to graphs, and we show that our approach is a generalization of Courcelle's recognizable
graph languages.

Hans-Jörg Kreowski and Sabine Kuske
Graph Multiset Transformation as a Framework for Massively Parallel Computation

Abstract: In this paper, graph multiset transformation is introduced and studied as a novel type of parallel graph transformation. The basic idea is that graph transformation rules may be applied to all or at least some members of a multiset of graphs simultaneously providing a computational step with the possibility of massive parallelism in this way. As a consequence, graph problems in the class NP can be solved by a single computation of polynomial length for each input graph.

Michel Bauderon, Rui Chen and Olivier Ly
Pullback grammars are context-free

Abstract: Following earlier works on pullback rewriting, we describe here the notion of graph grammar relevant to our formalism. We then show that pullback grammars are context-free and provide a surprising example, namely the context-free generation of square grids.

Eva Jelínková and Jan Kratochvíl
On Switching to H-Free Graphs

Abstract: In this paper we study the problem of deciding if, for a fixed graph $H$, a given graph is switching-equivalent to an $H$-free graph. Polynomial-time algorithms are known for $H$ having at most three vertices or isomorphic to $P_4$. We show that for $H$ isomorphic to a claw, the problem is polynomial, too. Further, we give a characterization of graphs switching-equivalent to a $K_{1,2}$-free graph by ten forbidden induced subgraphs, each having five vertices. We also give the forbidden induced subgraphs for graphs switching-equivalent to a forest of bounded vertex degrees.

16.30 - 18.00
Compositional Systems

Filippo Bonchi, Tobias Heindel and Fabio Gadducci
Parallel and Sequential Independence for Borrowed Contexts

Abstract: Parallel and sequential independence are central concepts in the concurrency theory of the double pushout (DPO) approach to graph
rewriting. However, so far those same notions were missing for DPO rewriting extended with borrowed contexts (DPOBC), a formalism used
for equipping DPO derivations with labels and introduced for modelling open systems that interact with the environment.
In this work we propose the definition of parallel and sequential independence for DPOBC rewriting, and we prove that these novel
notions allows for generalizing the local Church-Rosser and parallelism theorems holding for DPO rewriting. Most importantly, we
show that the DPOBC version of these theorems still guarantees the confluence and the parallel execution of independent DPOBC

Guilherme Rangel, Leen Lambers, Barbara König, Hartmut Ehrig and Paolo Baldan.
Behavior Preservation in Model Refactoring using DPO Transformations with Borrowed Contexts

Abstract: Behavior preservation, namely the fact that the behavior of a model is not altered along the transformations, is a crucial property in refactoring. The most common approaches to behavior preservation rely basically on checking given instances of a model class and their refactored versions. In this paper we introduce a more general technique for checking behavior preservation of refactorings defined by graph transformation rules. We use double pushout (DPO) rewriting with borrowed contexts, and, exploiting the fact that observational equivalence is a congruence, we show how to check refactoring rules for behavior preservation without the need of considering specific instances of the model. When rules are behavior-preserving, their application will never change behavior, i.e., every instance of the model class and its refactored version will have the same behavior. However, often there are refactoring rules describing intermediate steps of the transformation, which are not behavior-preserving, although the full refactoring does preserve the behavior. For these cases we present a procedure to combine refactoring rules to behavior-preserving concurrent productions in order to ensure behavior preservation. An example of refactoring for finite automata is given to illustrate the theory.

Paolo Baldan, Andrea Corradini, Hartmut Ehrig and Barbara König
Open Petri nets: Non-deterministic Processes and Compositionality

Abstract: We introduce ranked open nets, a reactive extension of Petri nets which generalises the open net model introduced in a previous work by allowing for a refined notion of interface. As for basic open nets, the interface towards the external environment of a ranked open net is given by a subset of places designated as open and used for composition. In this case, additionally, a bound on the number of connections which are allowed on an open place can be specified. We show that the non-deterministic process semantics is compositional with respect to the composition operation over ranked open nets, a result which did not hold for basic open nets.


9.00 - 10.00 Invited talk

Heiko Dörr
The AUTOSAR Way of Model-Based Engineering of Automotive Systems

10.30 - 12.30
Patterns and Model Transformations

István Ráth, Gábor Bergmann, Ákos Horváth and Dániel Varró
A Benchmark Evaluation of Incremental Pattern Matching in Graph Transformation

Abstract: In graph transformation, the most cost-intensive phase of a transformation execution is pattern matching, where subgraphs conforming to constraints encoded in graph patterns are extracted from a model graph.
Incremental pattern matching is a novel possible way of improving the efficiency of this critical pattern matching step. By this approach, the set of matches (i.e. the model elements conforming to a pattern) is calculated and incrementally maintained as the model changes, thus eliminating the need of graph traversal when a match is to be retrieved for transformation. Thus, in essence, this approach trades memory consumption for speed, which is, in some cases, a very advantageous trade-off.
In this paper, we compare RETE-based incremental graph pattern matching (as implemented in the VIATRA2 framework) and non-incremental graph pattern matching based on model-specific search plans. In order to carry out a detailed efficiency comparison, we extended the original Varro benchmarks.

Andy Schürr and Felix Klar
15 Years of Triple Graph Grammars

Abstract: Triple graph grammars (TGGs) have been invented 15 years ago as a formalism for the declarative specification of bidirectional graph-to-graph translations. In this paper we present a list of still open problems concerning the interpretation and the expressiveness of TGGs.
We will comment on extensions proposed to improve the original approach and the drawbacks that arise thereof.
Consequently a more precise formalization of compulsory properties of the translation of triple graph grammars into forward and backward graph translation functions is given. Regarding these properties an interpretation and implementation of negative application conditions is derived that does not destroy the benefits of the original approach. Additionally a new demand-driven forward/backward translation rule application strategy is proposed. It guarantees for the first time automatically a correct ordering of rule applications without imposing any additional requirements on the structure of the regarded graphs.

Juan de Lara and Esther Guerra
Pattern-based Model-to-Model Transformation

Abstract: We present a new, high-level approach for the specification of model-to-model transformations based on declarative patterns. These are (atomic or composite) constraints on triple graphs declaring the allowed or forbidden relationships between source and target models. In this way, a transformation is defined by specifying a set of triple graph constraints that should be satisfied by the result of the transformation. The description of the transformation is then compiled into lower-level operational mechanisms, to perform forward or backward transformations, as well as to establish mappings between two existent models. In this paper, we study one such mechanisms based on the generation of operational triple graph grammar rules. This technique exploits deduction techniques at the specification level to generate more specialized constraints (preserving the specification semantics) reflecting pattern dependencies, from which additional rules can be derived.

Claudia Ermel and Hartmut Ehrig
Semantical Correctness and Completeness of Model Transformations using Graph and Rule Transformation

Abstract: An important requirement of model transformations is the preservation of the behavior of the original model.
A model transformation is semantically correct if for each simulation run of the source system we find a corresponding simulation run in the target system. Analogously, we have semantical completeness, if for each simulation run of the target system we find a corresponding simulation run in the source system. In our framework of graph transformation, models are given by graphs, and graph transformation rules are used to define the operational behavior of visual models (called simulation rules).
In order to compare the semantics of source and target models, we assume that in both cases operational behavior can be defined by simulation rules. The model transformation from source to target models is given by another set of graph transformation rules.
These rules are also applied to the simulation rules of the source model. The main result in this paper states the conditions for model and rule transformations to be semantically correct and complete. The result is applied to analyze the behavior of a model transformation from a domain-specific visual language for production systems to Petri nets.