Forschungsberichte
der Fakultät IV – Elektrotechnik und Informatik
Process Denition
of Adhesive HLR Systems
(Long Version)
Frank Hermann
Bericht-Nr. 2008-09
ISSN 1436-9915
Process Definition
of Adhesive HLR Systems
(Long Version)
Frank Hermann
frank(at)cs.tu-berlin.de
Institut f¨ur Softwaretechnik und Theoretische Informatik
Technische Universit¨at Berlin, Germany
Bericht-Nr. 2008/09
ISSN 1436-9915
Process Definition of Adhesive HLR Systems
(Long Version)
Frank Hermann
frank(at)cs.tu-berlin.de
Institut f¨ur Softwaretechnik und Theoretische Informatik
Technische Universit¨at Berlin, Germany
Abstract
Process models of graph transformation systems are based on the concept of
occurrence grammars, which are a generalization of Petri net processes given by
occurrence nets. Recently, subobject transformation systems were proposed as an
abstract framework for occurrence grammars in adhesive categories, but they are
restricted to monomorphic matches for transformation steps. In this paper we review
the construction of STSs as processes for plain graph grammars and present an
extension to weak adhesive HLR categories with non-monomorphic matching, such
that e.g. attributed graph grammars are included.
Keywords: process definition, graph transformation, adhesive HLR systems
1 Introduction
Dynamic systems often show several possibilities for changing the order of their execution
steps while their observable behaviour remains equivalent, i.e. the same output is produced
for the same input and each execution step is performed in the same way. For this reason, a
process model of a specific system run does not only describe the given execution order but
also its equivalent ones. Formal models of processes build the basis for a formal analysis and
in this way for the verification of relevant properties. Furthermore, equivalent sequences
can be compared to find a suitable canonical one.
Graph transformation [12] is a universal modelling technique, which is applied e.g. for
the definition of visual languages [8] and for the specification of model transformations
[4]. Furthermore, it is especially appropriate to model concurrent and distributed systems,
where process analysis is highly relevant. Classical formal models in this context are Petri
nets [11], which can be characterized as restricted graph transformation systems (GTSs),
1
while general GTSs are more expressive. They provide an intuitive and object oriented
view on models and based on their formal categorical foundation they enable automated
and reliable checks.
Different graph transformation approaches were developed. In order to show results
for a variety of transformation approaches the concept of high level replacement systems
was introduced in [7, 6]. Adhesive transformation systems based on adhesive categories
[10] were presented to form a more compact framework. It covers a variety of important
transformation systems, e.g. typed graph transformation systems. Adhesive rewriting
systems were extended to the more general concept of adhesive high level replacement
systems [5], which covers approaches that also support attribution and inheritance. The
most important advantage of the abstract setting is that results are available for all concrete
instantiations.
As a main result the static analysis of conflicts between rules of a transformation
system can be based on the computation of critical pairs. Possible conflicts between rule
applications are detected. If there is no critical pair for a combination of two rules, it is
ensured that these rules will never be parallel dependent on each other in any derivation of
the transformation system. Furthermore, each dependency, which may arise, corresponds
to a critical pair, which can be embedded into the conflicting situation. The analysis of
critical pairs is complex in general, because all combination and all overlappings of the left
hand sides of the rules are checked.
Occurrence grammars [1] were proposed as a process definitions of GTSs in order to
provide a compact model for the analysis of dependencies between the derivation steps
of a given derivation in order to analyze the switch equivalence of derivations. They
correspond to the concept of occurrence nets for Petri nets. Occurrence grammars were
lifted to adhesive rewriting systems [2] and their properties were studied in more detail
leading to the notion of subobject transformation systems (STSs)[3].
In this paper we review the concept of STSs in Section 2 and show how to define an
STS corresponding to a derivation in a plain graph grammar, such that the STS can be
considered as the process corresponding to this derivation. The analysis techniques for
STSs (see [3]) - not reviewed in this paper - allow to analyze this process. In Sec. 3 we
show how the construction of an STS can be extended to weak adhesive HLR systems with
arbitrary matching, if suitable conditions are fulfilled by the concrete category. Exemplar-
ily we show that the conditions hold for attributed graph grammars with non-injective
matches. The main construction is based on E − M-factorization of the matches, where
Eand Mare subclasses of epi- and monomorphisms, respectively. We show that the con-
struction of the derived STS with its relations is well defined for adhesive HLR systems
with effective unions and E-M-factorizations of matches. The process construction creates
an STS, which allows us to analyze sequential and parallel independencies and dependen-
cies in a efficient way. This paper extends our previous work in [9] by the formal proves
and constructions.
2
2 STSs for Adhesive Transformation Systems
The definition of processes of graph grammars is given by occurrence grammars and was
extended to the more abstract setting of adhesive rewriting systems [2] based on subobjects.
In [3] we elaborated this technique and introduced the generalized concept of subobject
transformation systems (STSs). This included new basic relations on rule occurrences,
which are shown to compose to the previously defined compound relations for occurrence
grammars. The new basic relations separately define all occurring dependencies and con-
flicts between two derivation steps. The more detailed description of dependencies by the
basic relations shall improve the efficiency of an analysis when checking them in concrete
instantiations. In this section, we recall STSs and the process construction that builds
an STS to a given derivation in an adhesive rewriting system, i.e. within a transforma-
tion system over an adhesive category. At first, consider the following example of a graph
grammar GG0for which we will define the process S0later on.
TG0Object
Lnk
(a) Type Graph TG0
)
L R :Object
;
(b) Rule create
)
LR
:Object ;
(c) Rule delete
)
L R 1:Object
2:Object
:Lnk
1:Object
2:Object
(d) Rule addEdge
)
L R 1:Object
2:Object
:Lnk
1:Object
2:Object
(e) Rule removeEdge
Figure 1: Graph Grammar GG0
Example 1 (Graph grammar GG0).Fig. 1 shows the components of the graph gram-
mar GG0, where all elements are typed over T G0, which contains just one node “Object”
and one edge “Lnk”. Rules create and delete nodes and edges separately, e.g. the rule
“addEdge()” takes two nodes and creates a new edge in between. Consider the deriva-
tion d=DG0=
create
===⇒3G1=
addEdge
====⇒3G2=
removeEdge
=======⇒3G3=
delete
===⇒3G4E, where each of the pro-
ductions is applied three times. The intermediate graph G2is equal to T0in Fig. 2 and
G0=G4=∅. Now, an equivalent derivation d0for dcan be calculated with the help of a
corresponding STS S0as shown in Example 2. Many switchings of the derivation steps are
possible, which lead to equivalent derivations. For instance an edge may be added already
when the needed nodes are present and not as late as all nodes are created. This analy-
sis can be performed without checking the standard independence condition - existence of
mediating morphisms in the derivation diagram - but by checking the basic relations of the
STS S0.
In order to describe the process construction we review the notions needed for STSs.
Subobjects of an object Tare equivalence classes of monomorphisms a:A→Tin C, and
3
we write Afor short leaving the monomorphism and the equivalence class [a:A→T]
implicit. The category of subobjects of an object Tis called Sub(T). Its objects are the
subobjects of Tand its morphisms f:A→Bin Sub(T) are compatible with the implicit
monomorphisms, i.e. b◦f=a, implying that they are monomorphisms in Cas well and
we write A⊆Bfor short. Furthermore, all morphisms in Sub(T) are unique making all
diagrams commutative. For a graph Tin the category Grahps the morphisms in Sub(T)
are injective graph morphisms f= (fV, fE) : G1= (V1, E1, s1, t1)→G2= (V2, E2, s2, t2).
Definition 1 (Subobject transformation systems).ASubobject Transformation System
S= (T, P, π) over an adhesive category Cconsists of a super object T∈C, a set of
production names P, and a function π:P→Sub(T)·←·→·, which maps a production name
pto a production Lp⊇Kp⊆Rp, i.e., a span in Sub(T).
Direct derivations of an STS are defined by properties of union and intersection in
Sub(T). The intersection of two objects Aand Bwith morphisms a:A→Tand
b:B→Tis defined as the pullback of aand bin C. The union of Aand Bis given by
the pushout of Aand Bvia its intersection A∩Bin C. These constructions coincide with
the product of Aand Bin Sub(T) for the intersection and the coproduct of Aand Bin
Sub(T) for the union of both.
Definition 2 (Direct Derivations).Let S=hT, P, πibe a Subobject Transformation
System, π(q) = hL, K, Ribe a production, and let Gbe an object of Sub(T). Then there
is a direct derivation from Gto G0using q, written G=
q
⇒G0, if G0∈Sub(T) and if there
exists an object D∈Sub(T) such that:
(i)L∪D∼
=G; (iii)D∪R∼
=G0;
(ii)L∩D∼
=K; (iv)D∩R∼
=K.
If a production is applicable it is shown in [3] that STS transformations coincide with
DPO derivations in C. Note that the condition G0∈Sub(T) can be characterized by
the condition R∩G⊆L. Thus there is a special application condition in an STS, which
ensures that existing parts in Gare not added by a rule, otherwise the DPO step in C
would cause an additional creation an thus, the step would lead to a non-monomorphic
embedding of G0into Tmeaning that G0would not be a subobject of T.
In the following we explain how an STS Sis obtained from a given derivation dof an
adhesive grammar GG. This construction is called process of dand we denote the STS
Sby Prc(d). Based on the derived STS we can compute the dependency relations on the
rules of S. This leads to a partial order, which completely specifies the dependencies of
the steps of the derivation d. The super object Tis computed as colimit of the derivation
diagram. By composition of the existing monomorphisms all objects are automatically
embedded monomorphically into T.
4
Definition 3 (STS of a derivation).Let GG =hQ, πibe a graph transformation system,
and let d= (G0=
q1,m1
===⇒. . . =
qn,mn
===⇒Gn)be a derivation of GG. The STS generated from d
is defined as Prc(d) = hT, P, ˆπi, where Tis the colimit object of the diagram underlying the
derivation d,P={k|dk= (Gk−1=
qk,mk
===⇒Gk)is a step of d}, and ˆπ(k) = hLk, Kk, Rki,
where qk= (Lk←Kk→Rk).
T01:Object
2:Object 3:Object
1:Lnk 2:Lnk 3:Lnk
(a) Super object T0
)
L R 1:Object
;
(b) Rule create1
)
LR
1:Object ;
(c) Rule delete1
)
L R 1:Object
2:Object
1:Lnk
1:Object
2:Object
(d) Rule addEdge1
)
L R 1:Object
2:Object
1:Lnk
1:Object
2:Object
(e) Rule removeEdge1
Figure 2: STS S0
Example 2 (STS S0for GG0).The components of the STS S0= (T0, P0, π0)are shown in
Fig. 2. The super object T0shows three occurrences of nodes of the type “Object” and three
occurrences of edges of the type “Lnk”. It is the colimit of the derivation din Example
1. In this case it is equal to the intermediate graph G2of dbut it can be bigger than
any intermediate graph for other derivations. All rule occurrences in dare instantiated
as rules in S0. The set of production names Pcontains create[i], delete[i], addEdge[i]
and removeEdge[i]for i= (1,2,3), where the shown rules are for i= 1 and the rule
removeEdge[i]is inverse to addEdge[i]. Several dependencies can be calculated by relations
for STSs. For instance the rule addEdge1 is in “read causality”-relation to the rules create1
and create2. This means that addEdge1 needs elements, which are created by create1 and
create2. Therefore, a derivation sequence G=⇒. . . =
addEdge1
=====⇒Hwill always contain both
rules, create1 and create2 in the beginning or the nodes “1:Object” and “2:Object” are
present in the subobject Galready.
A sequence of rule names with each name occurring exactly once and where all depen-
dencies are respected according to the relations is called a linearization of the STS. Each
linearization corresponds to an equivalent derivation d0starting at G0=∅and ending at
G12 =∅as it is the case for d. For example the sequence s=c1; c2; a1; r1; c3; a2; a3; r2;
d2; r3; d3 with c=create, a =addEdge, r =removeEdge, d =delete defines a corre-
sponding derivation d0in GG0, which is switching equivalent to d. Each production of S0
corresponds to a step of the derivation dand hence, it occurs exactly once in a linearization
of the process.
5
Based on the construction of an STS to a given derivation by applying Prc it is possible
to automatically calculate all switch-equivalent derivations to a given one. The next section
shows how this construction can be extended to derivations with arbitrary matching in weak
adhesive HLR categories.
3 STSs for weak Adhesive HLR Systems
In this section we show how the process construction for derivations with monomorphic
matching in adhesvie rewriting systems as described in Section 2 can be extended to deriva-
tions with arbitrary matching in weak adhesive HLR systems [5]. Adhesive high level re-
placement (AHLR) systems [5] were introduced as a generalization of adhesive rewriting
systems in order to additionally cover some sophisticated transformation systems with con-
cepts like attribution and inheritance. In order to analyze the process of such systems the
construction of a corresponding STS has to be extended. First of all the construction has
to be performed along morphisms of the special class Mof an AHLR category instead of
general monomorphisms as before. Furthermore, since matches in AHLR systems cannot
be restricted to M-morphisms for practical reasons these morphisms have to be decom-
posed, such that the process will be build on the components with M-morphisms only. For
this purpose we require two conditions for the underlying categories, being the existence
of effective unions and E-M-factorization for the morphism class of the matches. We show
that these properties are fulfilled by the weak adhesive HLR category (AGraphsATG,M)
for attributed graphs.
In this section we explain the formal conditions which have to be shown for this chal-
lenge and provide the corresponding proofs. The suggested constructions and solutions are
explained by means of the following intuitive and compact example of an attributed graph
transformation system.
TG Object
size:int
val:int
(a) Type Graph TG
)
L R
;:Object
size=0
val=0
(b) Rule create()
)
L R ;
:Object
size=s
val=v
(c) Rule delete()
)
L R
:Object
size=s
val=v
:Object
size=s
val=x
(d) Rule setValue(x:int)
)
L R
:Object
size=s
val=v
:Object
size=x
val=v
(e) Rule setSize(x:int)
Figure 3: Graph Grammar GG
6
Example 3 (Graph Grammar GG).Rules in Fig. 3 define simple operations on objects
with two attributes, being “size” and “val”, both of type “int”. For keeping the example
compact the type graph T G of the graph grammar GG = (T G, S, R)contains only one
node “Object” containing these attributes. The start graph S=∅is empty and the set
of rules Rconsists of the four given rules in Fig. 3. The rule “create()” has an empty
left hand side meaning that there is no precondition for applying the rule, and the effect
is an insertion of a new node of type “Object” with both attributes set to 0. The opposite
behaviour is defined by “delete()”. Finally, the rule “setValue(x:int)” changes the attribute
“val” of a selected object and the analogous rule setSize(x:int) changes the attribute “size”
instead.
Weak adhesive HLR categories fulfill the following three conditions, which are less re-
strictive than the conditions for adhesive categories - mainly in the way that the conditions
have to hold only for a subclass Mof monomorphisms and furthermore, some of the con-
sidered morphisms in the conditions are additionally required to be M-morphisms. Weak
adhesive categories are a generalization of adhesive categories, for which the VK-property
in condition 3 is required with less preconditions.
Definition 4 (weak adhesive HLR category).A category Cwith a morphism class Mis
called a weak adhesive HLR category if:
1. Mis a class of monomorphisms closed under isomorphisms, composition (f:
A→B∈ M, g :B→C∈ M ⇒ g◦f∈ M), and decomposition
(g◦f∈ M, g ∈M⇒f∈ M).
2. Chas pushouts and pullbacks along M-morphisms, and M-morphisms are closed
under pushouts and pullbacks.
3. Pushouts in Calong M-morphisms are weak VK squares, i.e. the VK square property
holds for all commutative cubes with m∈ M and (f∈ M or b, c, d ∈ M)(see Fig. 4).
A
f
~~}
}
}
}m
A
A
A
A
(1)
C
n
A
A
A
AB
g
~~}
}
}
}
D
A0
f0
rreeeeeeeeeeeeeeeem0
))
S
S
S
S
S
S
S
a
C0
n0((
R
R
R
R
R
R
R
c
B0
g0ffffffffffff
rrf
f
f
b
D0
d
(2)
A
(1)
feeee
rreeeeeeeeeeeem
))
S
S
S
S
S
S
S
C
n))
S
S
S
S
S
S
SB
g
rreeeeeeeeeeeeeeeee
D
Figure 4: Pushout (1) and commutative cube (2) for VK property.
Based on the class Mof monomorphisms of a weak adhesive HLR category we define
the category of M-subobjects of a given object Tin order to extend the construction of
an STS to derivations in a weak adhesive HLR system.
7
Definition 5 (Category of M-Subobjects).Let Cbe a (weak) AHLR category with M
its subclass of monomorphisms and Tbe an object in C. The category of M-subobjects
of Cis called SubM(T). Its objects are the subobjects [a:A→T] of T, where ais
an M-morphism. A morphism f:A→Bin SubM(T) is compatible with the implicit
M-morphisms, i.e. b◦f=a, implying that fis an M-morphism in Cas well and we
write A⊆Bfor short.
Using the notion of M-subobjects we can now modify the constructions “intersection”
and “union” which were defined for subobjects in Sec. 2.
Definition 6 (Intersection and Union in SubM(T)).Let Cbe a (weak) AHLR category
with Mits subclass of monomorphisms and Tbe an object in C. Let SubM(T) be the
subcategory of M-subobjects of T. The intersection of two objects Aand Bin SubM(T)
is the product in SubM(T). The union of Aand Bin SubM(T) is the coproduct in
SubM(T).
We now characterize the constructions “intersection” and “union” for M-subobjects in
order to show the further properties - in particular the distributivity - which are needed
for the construction and analysis of an STS of a given derivation.
Lemma 1 (Intersection in SubM(T)).Let Cbe a (weak) AHLR category with Mits
subclass of monomorphisms and Tbe an object in C. Let SubM(T)be the subcategory
of M-subobjects of T. The intersection A∩Bof two objects Aand Bin SubM(T)
exists and is given by the pullback (1) in Cwith the M-morphism i:A∩B−
a◦pA
−−−−→ T.
A∩BpA//
pB(1)
A
a
Bb
//T
Proof. Let A, B be two objects in SubM(T) and (1) be a pullback in C. The pullback
exists, because a∈ M. The projections pA,pBare in M, because a, b ∈ M and Mis closed
under pullbacks. Furthermore, pA, pBare morphisms in SubM(T) by the commutativity
of the pullback construction and the definition of ab. Now, a comparison object X for the
product A∩Bin SubM(T) is also a comparison object for the pullback A∩Bin C, because
every diagram in SubM(T) commutes. Thus, there is a unique morphism hsatisfying the
universal property of both, the pullback in Cand the product in SubM(T). Furthermore,
h∈ M by decomposition of x1and his a morphism in SubM(T) by the commutativity
of the diagram beneath. X
x1
w
w
w
w
{{w
w
w
wh
x2
G
G
G
G
##
G
G
G
G
x
ss
A
a
G
G
G
G
##
G
G
G
G
A∩BpB//
pA
oo
i
B
bw
w
w
w
{{w
w
w
w
w
T
We now show that the union for the weak adhesive HLR category AGraphsATG exists
and can be constructed within AGraphsATG as the pushout in AGraphsATG over the
8
intersection in SubM(T). The main part here is to show that unions are effective, i.e. the
constructed object is again a subobject in SubM(T).
Theorem 2 (Union in SubM(T) for (AGraphsATG,M)).Let Tbe an object in
AGraphsATG and Mbe the class of monomorphisms, which are isomorphisms on the
data part. The union A∪Bof two objects Aand Bin SubM(T)exists and is given by
the pushout (1) over the intersection A∩Bwith the induced M-morphism u:A∪B→T
of the pushout (1).
AiA
%%
K
K
K
K
K
K
K
a
A∩B
pA99
s
s
s
s
s
s
s
pB%%
K
K
K
K
K
K
K(1) A∪Bu//T
BiB
99
s
s
s
s
s
s
s
b
??
Proof. The intersection exists by Lemma 1 and the pushout exists, because pA∈ M. The
induced morphism uis monomorphic using Thm. 4.7 in [10] and the existence of pullbacks
along M-morphisms. It remains to show that uis also an M-morphisms. This means that
uis additionally an isomorphism on the data part. Since aand iAare M-morphisms they
are isomorphisms on the data part and using the inverse isomorphism of iAon its data part
we have that uis an isomorphism on the data part by the composition of isomorphisms.
Theorem 3 (Distributivity).The union and intersection constructions in SubM(T)are
distributive, i.e. (i) : A∩(B∪C) = (A∩B)∪(A∩C)and (ii) : A∪(B∩C) = (A∪B)∩(A∪C).
Proof. We can perform the same steps as for the proof in Corollary 4.8 of [10], because all
Morphisms in the constructed cube are in Mand thus, the van Kampen property holds as
required using the general result for pullback decomposition. We derive (i) : A∩(B∪C) =
(A∩B)∪(A∩C). The direction A∪(B∩C)=(A∪B)∩(A∪C), which is not explicitly
shown in [10], follows directly:
(A∪B)∩(A∪C)
= ((A∪B)∩A)∪((A∪B)∩C) using (i)
=A∪((A∪B)∩C) using (A∪B)∩A=Agiven by A⊆A∪B
=A∪(A∩C)∪(B∩C) using (i)
=A∪(B∩C) using A∪(A∩C) = Agiven by A∩C⊆A.
The further constructions in [3] are based on the intersection and union constructions
together with the distributivity result and hence, they can be performed as well for weak
adhesive HLR categories with effective unions, like AGraphsATG.
We now want to consider derivations with arbitrary matching and therefore, we show
how they can be instantiated to derivations with M-matching, such that the previous
constructions can be performed again. Even though the rule applications of GG may
never identify structural nodes by their matches, because the left hand sides do not con-
tain more than one graph node, it is obvious that different attribute variables of a rule
9
may be matched to the same value of an instance graph. According to the definition of
attribution in the category AGraphsATG in [5] attribute values are nodes of E-graphs,
which implies that rule matches will identify E-graph nodes, meaning that the matches are
not monomorphic. For this reason a restriction to monomorphic matches will prohibit the
analysis of practical examples with attribution. Consider e.g. the presented example. The
rule setValue(x:int) shall be applicable for all possible values that can be assigned to an
object. This includes those cases in which the attribute size is equal to the same attribute
value as the one of the attribute val. Thus, matches cannot be restricted to monomorphic
ones in this situation. Therefore, the process construction using STSs is not applicable
directly.
Example 4 (Derivation).Derivation din Fig. 5 consists of four derivation steps
of the graph grammar GG:d=hd1;d2;d3;d4i=DG0=
create(),m1
======⇒G1=
create(),m2
======⇒G2
=
setAttribute(5),m3
==========⇒G3=
delete(),m4
======⇒G4E. Some steps are sequentially independent, while others
are not. For instance d3changes an attribute of node 1, such that it depends on d1, which
creates this node. Therefore, d3can only occur after d1in an equivalent derivation. The
following table shows all equivalent permutations for the derivation d.
πi\step d1d2d3d4
π11 2 3 4
π21 3 2 4
π32 1 3 4
π42 1 4 3
π52 4 1 3
;)
G1
G0G3
G2G4
) ) )
1:Object
size=0
val=0
d= d1; d2; d3 ; d4
1:Object
size=0
val=0
2:Object
size=0
val=0
1:Object
size=0
val=5
2:Object
size=0
val=0
1:Object
size=0
val=5
Figure 5: Derivation
In order to automatically derive a process of the derivation dthe process construction
Prc has to be extended to graph grammars with attribution and general matching. Since
rules may use terms to specify attribute values it is possible that two terms are matched
to the same value as in step d3, where rule variables sand vare both mapped to 0. This
implies that the match in this step is not injective. Therefore the process construction has
to be extended to non-injective matches in general. For this purpose we first instantiate
10
the derivation in the way that all identifications are performed to the rules itself and
thereafter we apply the existing process construction. This instantiation is based on E−M-
factorizations of the matches.
Definition 7 (E-Mfactorization). C has an E-Mfactorization for given
morphism classes Eand Mif for each fthere is a decompo-
sition, unique up to isomorphism, f=m◦ewith e∈ E and
m∈M.
Af//
e$$
J
J
J
J
JB
Cm
::
t
t
t
t
t
Usually Eis a subclass of epimorphisms and Mis a subclass of monomorphisms. In
the context of attributed graphs as in the category AGraphsATG the class Econtains all
epimorphisms and Mconsists of the monomorphisms f, which are injective on its graph
components fV, fEand isomorphic on the algebra component. We now show that the
category AGraphsATG has E-M-factorizations for a restricted class of morphisms, which
is enough in our case, because matches of derivations are included in this class.
Theorem 4 (E-M-factorization for (AGraphsATG,M)).Let Ebe the class of all epimor-
phisms in the weak adhesive HLR category AGraphsATG with Mthe class of monomor-
phism that are isomorphisms on the data part. Let f= (fG, fD) : AG →AH be a morphism
in AGraphsATG, where AG = (G, AG)and AH = (H, AH)are attributed graphs and the
algebra AG=TSigma(X)and AHis term generated. Then, there is an E-M-factorization
(e, m) = ((eG, eD),(mG, mD)) for f. The morphisms (eG, mG)are given by the epi-mono
factorization for typed graphs and the morphisms (eD, mD)are given by the the epi-mono
factorization for Alg(Σ).
Proof. By A.15 in [5] we know that GraphsTG and Alg(Σ) have epi-mono-factorizations.
Thus, eand muniquely exist. It remains to show that m∈ M. Since AHis term generated
we know that fD=xeval(ass) is surjective and by decomposition also mDis surjective.
By mDbeing mono according to the factorization we have that mDis an isomorphism.
Thus, m∈ M.
Remark 1. In the case that we consider derivations with algebras that are not term gen-
erated we can still perform a factorization AG −
e
→AG0−
m
−→ AH, but this time with ebeing
a general morphism and m∈ M. In this case AG0is obtained as before on the graph part,
but for the data part we use the A-quotient term algebra extended by a new variable for
each element not reached by xeval(ass) : TSigma(X)→AH. Based on this construction we
can also construct the STS, because we only use the lower part of the factorized derivation
diagrams, where only M-morphisms occur.
Based on the factorization of the matches we instantiate the derivation steps of a
derivation leading to a new derivation, where all matches are M-morphisms.
Definition 8 (Instantiation of a derivation).Let G=
p,m
==⇒Hbe a derivation step in a
weak adhesive HLR System with E-M-factorization for the morphism class of the matches.
The instantiated derivation step G=
p0,m0
==⇒His given by diagrams (5) and (6) below, which
11
d3
R:Object
size=s
val=x
:Object
size=s
val=
K
L:Object
size=s
val=v
L’1:Object
size=0
val=0
1:Object
size=0
val=
K’R’1:Object
size=0
val=5
G31:Object
size=0
val=5
2:Object
size=0
val=0
D21:Object
size=0
val=
2:Object
size=0
val=0
G21:Object
size=0
val=0
2:Object
size=0
val=0
(1)
(2)
(3)
(4)
Figure 6: Instantiated derivation step d3, Rule setAttribute(x:int)
are constructed as follows. The match mis factorized in the E-morphism m1and the M-
morphism m2. Diagram (5) is constructed as pullback, implying that k2∈ M, because Mis
closed under pullbacks. Morphism k1is obtained as the induced morphism from the pullback
(1) into K0and we have that (3) is a pullback by pullback decomposition and (5) is a pushout
by the pushou-pullback decomposition lemma for weak adhesive HLR categories. Diagram
(4) is obtained as a pushout and the morphism n2is derived as the induced morphism from
the pushout (4) into H. Thus, (6) is a pushout by pushout decomposition making ((4),(6))
a DPO diagram.
L
m
(1)
K
oooo////
k
(2)
R
n
G D
oooo////H
L
m1
m
(3)
K
oooo////
k1
k
(4)
R
n1
n
L0
m2
(5)
K0
oooo////
k2
(6)
R0
n2
G D
oooo////H
Let dbe a derivation in a weak adhesive HLR System with E-M-factorization for the
morphism class of the matches. The instantiated derivation d0is derived by instantiating
each derivation step as defined above.
Example 5 (Instantiation).We show the instantiation of the derivation dexemplarily at
step d3. Here, the attribute variables are identified by the match to the same value 0making
12
the match non-injective. If identifications of graph nodes occur, which is not the case in
the example, they are handled equivalently. Fig. 6 shows the step d3in the top most and
bottom line. The intermediate line contains the instantiated rule. All together squares (2)
and (4) are pushouts and applying this construction to the complete derivation dwe have
a new instantiated DPO derivation with matches in Monly.
Using the instantiation of a derivation we can again apply the process construction
Prc on a derivation diagram with M-morphisms only. The resulting STS of the example
derivation dis constructed by applying Prc to the instantiated derivation d0of d. The
results of an analysis of a derived STS concern the lower DPO diagrams of an instantiated
derivation dat first. But the computed equivalent derivations for the lower part lead to
equivalent derivations of dby composing the new DPO diagrams with the corresponding
but unchanged DPO diagrams of the upper line of the instantiation.
T1:Object
size=0
val=0
2:Object
size=0
val=0
val=5
(a) Super Object T
)
L R
1:Object
size=0
val=0
1:Object
size=0
val=5
(b) STS rule p3
p1
p2
p3
p4
(c) Dependencies
Figure 7: Parts of STS S
Example 6 (STS with Attribution).Applying Prc to the derivation din Example 4 we
derive an STS S= (T, P, π), with the super object Tas shown in Fig. 7(a) constructed as
the colimit of the lower line in the derivation diagram and in our example it is equal to
the pushout of G2←D2→G3in Fig. 6. The set of production names P={p1, p2, p3, p4}
contains four elements which are mapped by πto the rules, which are instantiations of
the rules in GG. For instance, the rule name p3is mapped to an instantiation of “se-
tAttribute(x:int)” as shown in Fig. 7(b). Now, STS relations presented in [3] can be used
to calculate a concrete dependency relation Dep and all conflicts Confl for all rules piin
P. In this example we have no conflicts and Dep ={(p1, p3),(p2, p4)}as visualized in
Fig. 7(c).
Remark 2 (Multiple Attribute Values).Attribute values in the category AGraphsATG are
defined as edges to actual value nodes. Therefore, a correctly typed node is allowed to have
zero or multiple attribute values by having zero or multiple edges of the same attribution
type. This loose typing is needed, e.g. to specify attribute changes by a rule, because an
attribute edge has to be deleted and recreated again to connect the node to a new data
value. Furthermore, multiple attribute values are of main interest in the context of process
construction. When applying Prc to construct an STS each occurrence of a node and an
edge is added to the super object Tseparately. This means that elements, which are deleted
and created again, appear as different elements in T. Thus, after changing an attribute
13
value as in rule setValue(x:int), the edge connecting the object node with its attribute is
deleted and created again to the new value. This leads to two separate edges in T, which is
the case in the example super object Twith value 0 and 5 for the node of type “Object”. If
this multiple structure would not be created, derivation steps, which depend on each other
at attributes, would be recognized misleadingly as independent.
The example has shown how processes of derivations with attributes and non-injective
matching are constructed. More complex processes can be calculated automatically and
the formal results justify the correctness of a process analysis based on the derived STS.
4 Conclusion
Process definitions for graph grammars [2, 1] have been studied in analogy to and as gen-
eralization of existing process constructions for Petri nets given by occurrence nets. These
constructions are limited to monomorphic matches and plain graph grammars without
attribution only.
Extension The extension to arbitrary matches and attribution is the main contribu-
tion of this paper. It was presented on behalf of an intuitive and compact example, but
the construction is highly scalable. A special condition for the new construction is the
existence of E-M-factorizations of matches in the regarded category of the transformation
system. Most categories for graphs, such as typed attributed graphs, as well as many
other categories have E-M-factorizations for all or a suitable subclass of morphisms, which
ensures that the condition is no restriction of the approach for practical cases. The formal
foundation and correctness were shown in this paper.
Further Extensions Practical applications of graph grammars often use negative ap-
plication conditions (NACs) for restricting the application situations of the rules. In order
to extend the presented process definition to handle also NACs we will instantiate NACs.
Furthermore, there are new conflict situations in a derivation with NACs. They will have
to be captured by new relations in the corresponding STS. Moreover, the notion of switch
equivalence has to be generalized, because there are derivations with NACs that shall be
seen to be equivalent, but they are not switch-equivalent using sequential independence
with NACs. The reason is that rule applications may be possible in an equivalent way at
several positions, which are not situated next to each other and these permutations cannot
be derived by switching independent steps.
The presented extension of process definitions of graph transformations opens new pos-
sibilities for the analysis of object oriented systems including the analysis of dependencies
caused by attribute changes. Case studies will benchmark the power of this approach and
may inspire further extensions.
14
References
[1] P. Baldan. Modelling Concurrent Computations: from Contextual Petri Nets to Graph
Grammars. PhD thesis, Computer Science Department - University of Pisa, 2000.
[2] P. Baldan, A. Corradini, T. Heindel, B. K¨onig, and P. Sobocinski. Processes for
adhesive rewriting systems. In L. Aceto and A. Ing´olfsd´ottir, editors, FoSSaCS, volume
3921 of Lecture Notes in Computer Science, pages 202–216. Springer, 2006.
[3] A. Corradini, F. Hermann, and P. Soboci´nski. Subobject Transformation Systems.
Applied Categorical Structures, February 2008.
[4] H. Ehrig, K. Ehrig, C. Ermel, F. Hermann, and G. Taentzer. Information preserving
bidirectional model transformations. In M. B. Dwyer and A. Lopes, editors, Fun-
damental Approaches to Software Engineering, volume 4422 of LNCS, pages 72–86.
Springer, 2007.
[5] H. Ehrig, K. Ehrig, U. Prange, and G. Taentzer. Fundamentals of Algebraic Graph
Transformation. EATCS Monographs in Theoretical Computer Science. Springer,
2006.
[6] H. Ehrig, A. Habel, H.-J. Kreowski, and F. Parisi-Presicce. Parallelism and concur-
rency in high level replacement systems. Technical Report 90-35, Technical University
of Berlin, 1990.
[7] H. Ehrig, A. Habel, H.-J. Kreowski, and F. Parisi-Presicce. From graph grammars to
high level replacement systems. In 4th Int. Workshop on Graph Grammars and their
Application to Computer Science, volume 532 of LNCS, pages 269–291. Springer, 1991.
[8] C. Ermel, K. Ehrig, G. Taentzer, and E. Weiss. Object Oriented and Rule-based
Design of Visual Languages using TIGER. In Proc. Third International Workshop
on Graph-Based Tools (GraBaTs’06), volume 1, Natal, Brazil, September 2006. Elec-
tronic Communications of the EASST.
[9] F. Hermann and H. Ehrig. Process Definition using Subobject Transformation Sys-
tems. EATCS Bulletin, 95:153–163, 2008.
[10] S. Lack and P. Soboci´nski. Adhesive Categories. In Proc. FOSSACS 2004, volume
2987 of LNCS, pages 273–288. Springer, 2004.
[11] W. Reisig. Petri Nets: An Introduction, volume 4 of EATCS Monographs on Theo-
retical Computer Science. Springer, 1985.
[12] G. Rozenberg, editor. Handbook of Graph Grammars and Computing by Graph Trans-
formations, Volume 1: Foundations. World Scientific, 1997.
15
