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.
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
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 derivations.
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.
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.
ICGT
2008
