Sufficient Criteria for Applicability and
Non-Applicability of Rule Sequences
Leen Lambersa,1Hartmut Ehriga,2Gabi Taentzerb,3
aInstitut f¨ur Softwaretechnik und Theoretische Informatik
Technische Universit¨at Berlin, Germany
bFachbereich Mathematik und Informatik
Philipps-Universit¨at Marburg, Germany
Abstract
In several rule-based applications using graph transformation as underlying modeling technique the following
questions arise: How can one be sure that a specific sequence of rules is applicable (resp. not applicable)
on a given graph? Of course, it is possible to use a trial and error strategy to find out the answer to these
questions. In this paper however, we will formulate suitable sufficient criteria for applicability and other ones
for non-applicability. These criteria can be checked in a static way i.e. without trying to apply the whole rule
sequence explicitly. Moreover if a certain criterion is not satisfied, then this is an indication for reasons why
rule sequences may or may not be applicable. Consequently it is easier to rephrase critical rule sequences.
The results are formulated within the framework of double pushout (DPO) graph transformations with
negative application conditions (NACs).
Keywords: graph transformation, analysis, applicability of rules
1 Introduction
When analyzing integrated specifications of rules with control structures [4,7] for
consistency, a considerable amount of rule sequences is to be checked for applicabil-
ity (resp. non-applicability). Hence, it is not appropriate to check the applicability
or non-applicability of each rule sequence explicitly. Therefore static analysis tech-
niques are desirable. Statically means that it is not necessary to use a trial and error
strategy and therefore backtracking can be avoided. In the following, we present suf-
ficient criteria for the applicability and for the non-applicability of a rule sequence
to a graph. These criteria can be checked in a static way, since they are based
mainly on the dependency or independency of rules. Moreover the non-satisfaction
of one of the criteria gives a hint to the reason for a rule sequence to be applicable or
1Email: [email protected]
2Email: [email protected]
3Email: [email protected]
Lambers, Ehrig, Taentzer
inapplicable. Applicability criteria have been studied also in [9] for simple digraphs
using matrix graph grammars.
As example we consider a simple Mutual Exclusion Algorithm implemented by
graph transformation rules with a start graph Gand type graph presented in Fig. 1.
The algorithm enables two processes to access a resource according to the mutual
exclusion principle. The purpose of this algorithm is to control the usage of the
resource such that at most one process holds the resource at time (safety property).
Furthermore, if a process demonstrates a request for the resource it should be served
eventually (liveness property). In the following, we will check safety (resp. liveness)
by checking if certain rule sequences are not applicable (resp. applicable) on the
start graph.
The paper is structured as follows: Section 2 presents preliminaries. At first
we repeat the main definitions for rule-based transformations with means of dou-
ble pushout (DPO) graph transformations [1] with negative application conditions
(NACs) [3]. Then we define asymmetric dependency and independency on the level
of transformations. Therefrom we can deduce the concept of asymmetric indepen-
dency for rules. In Section 3 and 4 we define sufficient criteria for applicability and
non-applicability of rule sequences. Section 5 takes up the example again and shows
how to check the criteria presented in Section 3 and 4 with some support of the
graph transformation tool AGG [8].
2 Independency and Dependency of Rules
2.1 Graph Transformation with NACs
We repeat the basic definitions for double pushout graph transformation with neg-
ative application conditions (NACs). A graph rule holding a NAC ncan be applied
on a graph Gonly if the forbidden structure expressed by nis not present in G.
Definition 2.1 [graph, graph morphism, rule] A graph G= (GE, GV, s, t) consists
of a set GEof edges, a set GVof vertices and two mappings s, t :GE→GV,
assigning to each edge e∈GEa source q=s(e)∈GVand target z=t(e)∈GV.
Agraph morphism (short morphism)f:G1→G2between two graphs Gi=
(Gi,E, Gi,V , si, ti), (i= 1,2) is a pair f= (fE:GE,1→GE,2, fV:GV,1→GV,2) of
mappings, such that fV◦s1=s2◦fEand fV◦t1=t2◦fE. A morphism f:G1→G2
is injective (resp.surjective) if fVand fEare injective (resp. surjective) mappings.
A graph transformation rule p:Ll
←Kr
→Rconsists of a rule name pand a pair
of injective morphisms l:K→Land r:K→R. The graphs L, K and Rare
called the left-hand side (LHS), the interface, and the right-hand side (RHS) of p,
respectively.
Definition 2.2 [rule and transformation with NACs, applicability of rule with
NACs]
•Anegative application condition or NAC(n)on pfor a rule p:Ll
←Kr
→R(l,r
injective) is an arbitrary morphism n:L→N. A morphism g:L→Gsatisfies
NAC(n) on L, written g|=NAC(n), if and only if 6 ∃ q:N→Ginjective such
2
Lambers, Ehrig, Taentzer
Figure 1. Start graph G, graph H and type graph of Mutual Exclusion - Rules re-
questRes,takeRes,releaseRes,giveRes and nextProc - Dependency and Conflict Matrix in AGG
3
Lambers, Ehrig, Taentzer
that q◦n=g.
L
g
n//N
q
X
qq
G
A set of NACs on pis denoted by NACp={NAC(ni)|i∈I}. A morphism
g:L→Gsatisfies NACpif and only if gsatisfies all single NACs on pi.e.
g|=NAC(ni)∀i∈I.
•Arule (p, NACp)with NACs is a rule with a set of NACs on p.
•Adirect transformation Gp,g
⇒Hvia a rule p:L←K→Rwith NACpand a
match g:L→Gconsists of the double pushout [1] (DPO)
L
g
K//
ooR
h
G D //ooH
where gsatisfies NACp, written g|=NACp. Since pushouts along injective
morphisms always exist, the DPO can be constructed if the pushout complement
of K→L→Gexists. If so, we say that the match gsatisfies the gluing condition
of rule p. If there exists a morphism g:L→Gwhich satisfies the gluing condition
and g|=NACpwe say that rule pis applicable on Gvia the match g.
Example 2.3 Consider the graph transformation rules of the Mutual Exclusion
Algorithm presented in Fig. 1. Rule requestRes expresses a request of a process to
access the resource if this process has not requested the resource yet or is using the
resource already. Rule takeRes enables a process to start using the resource if this
process possesses a token. releaseRes can release the resource again and giveRes
passes the token to the other process after releasing. Finally rule nextProc can pass
a token from one process to the other one as long as the first one has not expressed
a request.
In [6] it is proven that to each rule pwith NACpthere exists an inverse rule
p−1with NACp−1such that each transformation can be inverted. The following
definition shows how to construct from NACpon rule pequivalent NACs NACp−1
on the inverse rule p−1[2]:
Definition 2.4 [construction of NACs on inverse rule] For each NAC(ni) with
ni:L→Nion p= (L←K→R), the equivalent NAC Rp(NAC(ni)) on p−1=
(R←K→L) is defined in the following way:
L
ni
K
oo//
(1) (2)
R
n0
i
NiZ
oo//N0
i
•If the pair (K→L, L →Ni) has a pushout complement, we construct (K→
Z, Z →Ni) as the pushout complement (1). Then we construct pushout (2) with
the morphism n0
i:R→N0
i. Now we define Rp(NAC(ni)) = NAC(n0
i).
4
Lambers, Ehrig, Taentzer
•If the pair (K→L, L →Ni) does not have a pushout complement, we define
Rp(NAC(ni)) = true.
For each set of NACs on p,NACp=∪i∈INAC(ni) we define the following set of
NACs on p−1:NACp−1=Rp(NACp) = ∪i∈I0Rp(NAC(ni)) with i∈I0if and only
if the pair (K→L, L →Ni) has a pushout complement.
With means of this construction we can formulate the following fact [2,6]:
Fact 2.5 (inverse direct transformation with NACs) For each direct trans-
formation with NACs G⇒Hvia a rule p:L←K→Rwith NACpa set of NACs
on p,H⇒Gis a direct transformation with NACs via the inverse rule p−1with
NACp−1.
Example 2.6 Consider rule requestRes. The inverse rule of requestRes deletes the
request edge between a process and the resource if there is no other request edge
nor a heldby edge between this process and the resource.
2.2 Independency and Dependency of Rules
The (non-)applicability of a rule sequence on a graph Gis affected by dependencies
and independencies between the rules in the rule sequence. In particular it is affected
by asymmetric dependencies as explained in this section.
Two direct transformations are in conflict if they are not parallel independent.
In [5] a Conflict Characterization is given in which different reasons for conflicting
transformations become clear. It is possible that one transformation deletes (resp.
produces) a structure which is used (resp. forbidden) by the other one and the
other way round. In particular we can deduce that two direct transformations are
in conflict if at least one transformation depends on the other one. This asymmet-
ric parallel dependency and on the contrary asymmetric parallel independency are
expressed by the following definition.
Definition 2.7 [asymmetrically parallel dependent and independent transforma-
tions] A direct transformation G(r2,m2)
=⇒H2with NACr2is asymmetrically parallel
dependent on G(r1,m1)
=⇒H1with NACr1if:
(i) @h21 :L2→D1:d1◦h21 =m2(delete-use-conflict)
OR
(ii) there exists a unique h21 :L2→D1:d1◦h21 =m2, but e1◦h21 6|=NACr2
(produce-forbid-conflict).
A direct transformation G(r2,m2)
=⇒H2with NACr2is asymmetrically parallel inde-
pendent on G(r1,m1)
=⇒H1with NACr1if G(r2,m2)
=⇒H2is not asymmetrically parallel
dependent on G(r1,m1)
=⇒H1. This means in particular that ∃h21 :L2→D1:
5
Lambers, Ehrig, Taentzer
d1◦h21 =m2such that e1◦h21 |=NACr2.
N1N2
R1
K1//oo
L1
n1
OO
m1
A
A
A
A
A
A
A
AL2
h21
ww
n2
OO
m2
~~}
}
}
}
}
}
}
}
K2
oo//
R2
H1D1d1//
e1
ooGD2
d2
ooe2//H2
If a sequence of two direct transformations is not sequentially independent this
is because either the second transformation depends on the first one or the other
way round. The case in which the second transformation depends (resp. is inde-
pendent) on the first one is described by asymmetric sequential dependency (resp.
independency) as in the following definition. This case occurs in particular when
the first transformation produces a structure which is used by the second one or
the first transformation deletes a structure forbidden by the second one. In other
words the first transformation triggers the second one.
Definition 2.8 [asymmetrically sequential dependent and independent transfor-
mations] A direct transformation H1
(r2,m2)
=⇒H2with NACr2is asymmetrically se-
quential dependent on G(r1,m1)
=⇒H1with NACr1if
(i) @h21 :L2→D1:e1◦h21 =m2(produce-use-dependency)
OR
(ii) there exists a unique h21 :L2→D1:e1◦h21 =m2, but d1◦h21 6|=NACr2
(delete-forbid-dependency).
A direct transformation H1
(r2,m2)
=⇒H2with NACr2is asymmetrically sequential
independent on G(r1,m1)
=⇒H1with NACr1if H1
(r2,m2)
=⇒H2with NACr2is not
asymmetrically sequential dependent on G(r1,m1)
=⇒H1with NACr1. This means in
particular that ∃h21 :L2→D1:e1◦h21 =m2such that d1◦h21 |=NACr2.
N1N2
L1
n1
OO
K1//oo
R1
m0
1!!
B
B
B
B
B
B
B
BL2
n2
OO
h21
ww
m2
}}|
|
|
|
|
|
|
|
K2
oo//
R2
GD1e1//
d1
ooH1D2
d2
ooe2//H2
Now we can define asymmetric parallel (resp. sequential) independency for rules
by demanding that the corresponding transformations are asymmetrically indepen-
dent. Analogously it is possible to define asymmetric parallel (resp. sequential)
dependency for rules.
Definition 2.9 [asymmetrically parallel independent rules] The rule r2is asym-
metrically parallel independent on r1if every transformation G(r2,m2)
=⇒H2via r2
6
Lambers, Ehrig, Taentzer
with NACr2is asymmetrically parallel independent on any other transformation
G(r1,m1)
=⇒H1via r1with NACr1.
Definition 2.10 [asymmetrically sequential independent rules] A rule r2is asym-
metrically sequential independent on r1if every transformation H1
(r2,m2)
=⇒H2via r2
with NACr2is asymmetrically sequential independent on any other transformation
G(r1,m1)
=⇒H1via r1with NACr1.
Example 2.11 Rule nextProc is asymmetric parallel dependent on requestRes,
since rule requestRes produces a request edge which is forbidden by rule nextProc.
On the contrary, rule requestRes is asymmetric parallel independent on nextProc,
since rule nextProc neither deletes anything what can be used by requestRes nor
produces anything forbidden by requestRes. Rule requestRes is asymmetric sequen-
tially dependent on rule releaseRes, since releaseRes deletes a heldby edge which is
forbidden by requestRes. On the contrary, rule releaseRes is asymmetric sequen-
tially independent on rule requestRes, since requestRes neither produces anything
what can be used by releaseRes nor deletes anything forbidden by requestRes.
For the criteria defined in the next section we need a special case of asymmetric
sequential dependency for the case without NACs. It is possible namely that a rule
r1produces everything which is needed by r2regardless of what is already present
in the corresponding transformations.
Definition 2.12 [purely sequential dependent rules] A rule r2:L2←K2→R2is
purely sequential dependent on r1:L1←K1→R1if r2is a rule without NACs and
there exists an injective morphism l21 :L2→R1.
Remark 2.13 r2is asymmetrically sequential dependent on r1, if r2is purely se-
quential dependent on r1and the following mild assumptions are satisfied: a mor-
phism k21 :L2→K1does not exist such that r1◦k21 =l21,r2is non-deleting on
nodes and id :R1→R1|=NACr−1
1.
Example 2.14 Rule releaseRes is purely sequential dependent on rule takeRes,
because its LHS can be embedded completely into the RHS of takeRes. Rule tak-
eRes is asymmetric sequentially, but not purely dependent on rule requestRes, since
requestRes does not produce a token edge.
We can analogously derive from the usual definition of sequential (resp. paral-
lel) independence of transformations with NACs [5] (Def. A.1 in Appendix A) the
definition for sequential (resp. parallel) independency on rules by demanding that
all existing transformations via these rules are sequentially (resp. parallel) indepen-
dent. Recall that for each pair of parallel independent transformations with NACs
H1
r1,m1
⇐Gr2,m2
⇒H2, there are an object G0and direct transformations H1
r2,m0
2
⇒G0
and H2
r1,m0
1
⇒G0such that Gr1,m1
⇒H1
r2,m0
2
⇒G0and Gr2,m2
⇒H2
r1,m0
1
⇒G0are sequen-
tially independent. The transformations can thus be performed in any order with
the same result (Theorem A.3 in Appendix A). Note that we have the following
relationship between parallel and sequential independency: Gr1
⇒H1
r2
⇒H2are se-
quentially independent iff Gr−1
1
⇐H1
r2
⇒H2are parallel independent. In the next
7
Lambers, Ehrig, Taentzer
section we need sequential independency of a rule pair in order to be able to switch
adjacent rules in a rule sequence.
Definition 2.15 [parallel and sequential independent rules] Rules r1and r2are
parallel independent if each pair of transformations G(r1,m1)
=⇒H1via r1with NACr1
and G(r2,m2)
=⇒H2via r2with NACr2is parallel independent. The pair of rules
(r1, r2) is sequentially independent if each sequence of transformations G(r1,m1)
=⇒H1
via r1with NACr1and H1
(r2,m2)
=⇒G0via r2with NACr2is sequentially independent.
Remark 2.16 Note that the following correspondences between asymmetric par-
allel (resp. sequential) independency and parallel (resp. sequential) independency
exists. Rules r1and r2are parallel independent if and only if r1is asymmetrically
parallel independent of r2and r2is asymmetrically parallel independent of r1. The
rule pair (r1, r2) is sequentially independent if and only if r2is asymmetrically se-
quential independent on r1and r−1
1is asymmetrically sequential independent on
r−1
2.
Example 2.17 The rule pair (requestRes,nextProc) is sequentially independent.
Note that the NAC of rule nextProc forbids a process to shift the token if this
process expressed a request. Thus whenever (requestRes,nextProc) can be applied
in this order the request is expressed by the process to which the token is shifted.
This is equivalent to first shifting the token to this process which then expresses a
request.
3 Applicability of Rule Sequences
3.1 Applicability Criteria
Let s:r1r2. . . rnbe a sequence of nrules and G0a graph on which this sequence
should be applied. The criteria defined in the following definition guarantee this
applicability. The initialization criterion is trivial, since it just requires the first rule
being applicable to graph G0. The no node-deleting rules criterion avoids dangling
edges. The third criterion ensures that the applicability of a rule riis not impeded by
one of the predecessor rules rjof ri. Criterion 4a will be satisfied if rule riis purely
sequential dependent from a rule rjoccurring somewhere before riin the sequence
s. In this case rjtriggers the applicability of riregardless of what is present already
in the start graph G0. As soon as the sequential dependencies are not pure though
this criterion is not satisfiable. Therefore we have also a more general criterion 4b.
It ensures the applicability of a rule rineeding some subgraph of a direct predecessor
rule together with parts of the start graph G0. This is expressed by the fact that a
concurrent rule rcof ri−1and riexists which is applicable on the start graph G0.
The construction of a concurrent rule with NACs is explained in [6]. The correctness
of the criteria is described in Theorem 3.2 which is proven in the Appendix B.
Definition 3.1 [applicability criteria] Given a sequence s:r1r2. . . rnof nrules
and a graph G0. Then we define the following applicability criteria for son G0:
(i) r1is applicable on G0via the injective match m1:L1→G0(initialization)
8
Lambers, Ehrig, Taentzer
(ii) each rule occurring in sis non-deleting on nodes (no node-deleting rules)
(iii) ∀ri, rjin swith 1 ≤j < i ≤n,riis asymmetrically parallel independent on rj
(no impeding predecessors)
(iv) ∀riin swith 1 < i ≤nwhich are not applicable on G0via an injective match
(a) there exists a rule rjin swhich is applicable via an injective match on
G0with 1 ≤j < i ≤nand riis purely sequential dependent on rj(pure
enabling predecessor), which especially means that rihas no NACs
OR
(b) there exists a concurrent rule rcof ri−1and risuch that rcis applicable
via an injective match on G0and rcis asymmetrically parallel independent
on rjfor all j < (i−1) and rjis asymmetrically parallel independent on
rcfor all i < j ≤n.(direct enabling predecessor)
Theorem 3.2 (correctness of applicability criteria) Given s:r1r2. . . rna
sequence of nrules and a graph G0. If the criteria in Def. 3.1 are satisfied for
rule sequence sand graph G0, then this rule sequence is applicable on G0with in-
jective matching i.e. there exists a graph transformation G0
r1
⇒G1. . . Gn−1
rn
⇒Gn
with injective matching.
3.2 Applicability of Summarized Rule Sequences
The 4th criterion in Def. 3.1 will be satisfied only, if the rule riis purely sequential
dependent from one single rule rjoccurring before riin the sequence or if it is
asymmetrically sequential dependent on the rule ri−1. In some transformations
though a rule needs not only a subgraph from one single predecessor, but from
several ones. For these cases the criteria could then be satisfied by a sequence
in which exactly these rules are summarized to a concurrent rule. Note that the
correctness of the following theorem is proven in the Appendix B.
Theorem 3.3 (summarized rule sequences) Given s:r1r2. . . rna sequence of
nrules and a graph G0. If the criteria in Def. 3.1 are satisfied for a rule sequence
s0:r0
1r0
2. . . r0
mwith m<nin which neighbored rules in scan be summarized by a
concurrent rule, then the original rule sequence sis applicable on G0with injective
matching i.e. there exists a graph transformation G0
r1
⇒G1. . . Gn−1
rn
⇒Gnwith
injective matching.
3.3 Applicability of Shift-Equivalent Rule Sequences
If it is not possible to satisfy criterion 4b in Def. 3.1 for a rule sequence s:r1r2. . . rn,
then it is still possible to exploit shift-equivalence. This is because criterion 4b could
be satisfiable for a rule sequence s0in which a normal predecessor is shifted to be a
direct one. Note that a rule rjin scan be switched with a rule rj+1 only if the pairs
of rules (rj, rj+1) and (rj+1, rj) is sequentially independent. If the criteria then hold
though for rule sequence s0in which some rules have been shifted, they hold also
for the original rule sequence s.
Definition 3.4 [shift-equivalent rule sequences] A rule sequence s0is shift-
equivalent with a rule sequence s:r1r2. . . rmif s0can be obtained by switching
9
Lambers, Ehrig, Taentzer
rules rjwith rj+1 and the switching is allowed only if (rj, rj+1) and (rj+1, rj) are
sequentially independent according to Def. 2.15.
Theorem 3.5 (checking shift-equivalent rule sequences) If the criteria in
Def. 3.1 are satisfied for a rule sequence s:r1r2. . . rnand a graph G0, then all
shift-equivalent rule sequences as defined in Def. 3.4 are applicable on G0with in-
jective matching as well with the same result.
Proof This follows directly from Def. 3.4, the Local Church-Rosser Theorem with
NACs [5] (Theorem A.3 in Appendix A), Def. 2.15 and Theorem 3.2.2
Remark 3.6 Note that a somewhat weaker version of this theorem holds as well.
Namely, suppose that we want to prove applicability of a rule sequence s:r1r2. . . rn
to a graph G0. Then it is sufficient to show the satisfaction of the criteria in Def. 3.1
for a rule sequence s0which can be deduced from sby switching forward rule ri+1
with rionly if rule pair (ri+1, ri) is sequentially independent.
4 Non-Applicability of Rule Sequences
Let s:r1r2. . . rnbe a sequence of nrules and G0a graph. The satisfaction of the
following criteria for sand G0guarantee that the sequence swill not be applicable
on G0. Criterion 1 is trivial, since it just requires the first rule being non-applicable
to graph G0. Criterion 2 checks if predecessors for a rule riwhich is not applicable
already on G0are present in the sequence such that they can trigger the applicability
of ri. If not, riwill not be applicable and therefore neither the rule sequence will be
applicable. Note that the correctness of the following criteria is proven in Appendix
B.
Definition 4.1 [non-applicability criteria] Given s:r1r2. . . rna sequence of nrules
and a graph G0. Then we define the following non-applicability criteria for son G0:
(i) r1is not applicable on G0(initialization error)
OR
(ii) ∃riin swith 1 < i ≤nsuch that riis not applicable on G0but for all rules rj
in swith 1 ≤j < i ≤n,riis asymmetrically sequential independent on rjno
enabling predecessor.
Theorem 4.2 (correctness of non-applicability criteria) Given a sequence
s:r1r2. . . rnof nrules and a graph G0. If the criteria in Def. 4.1 are satisfied
for rule sequence sand graph G0, then this rule sequence is not applicable on G0
i.e. there exists no graph transformation G0
r1
⇒G1. . . Gn−1
rn
⇒Gn.
Analogously to Theorem 3.5 we can formulate the following theorem expressing
that shift-equivalent-rule sequences are not applicable to a graph G0if one of the
sequences satisfies the non-applicability criteria.
Theorem 4.3 (checking shift-equivalent rule sequences) If the criteria in
Def. 4.1 are satisfied for a rule sequence s:r1r2. . . rnand a graph G0, then all
shift-equivalent rule sequences as defined in Def. 3.4 are not applicable on G0ei-
ther.
10
Lambers, Ehrig, Taentzer
Proof This follows directly from Def. 3.4, the Local Church-Rosser Theorem with
NACs [5] (Theorem A.3 in Appendix A), Def. 2.15 and Theorem 4.2.2
Remark 4.4 Note that a somewhat weaker version of this theorem holds as well.
Namely, suppose that we want to prove non-applicability of a rule sequence s:
r1r2. . . rnto a graph G0. Then it is sufficient to show the satisfaction of the criteria
in Def. 4.1 for a rule sequence s0which can be deduced from sby switching forward
rule ri+1 with rionly if rule pair (ri, ri+1) is sequentially independent.
5 Checking the Criteria
5.1 Checking for Sequential and Parallel Dependency of Rules in AGG
To check asymmetric sequential and parallel dependency of rules, we compute all
corresponding critical pairs by AGG [8]. A critical pair represents the parallel
(resp. sequential) dependency of rules in a minimal context. The minimal conflicts
(i.e. asymmetric parallel dependencies) are represented in a conflict matrix. The
minimal dependencies (i.e. asymmetric sequential dependencies) are represented in
a dependency matrix. The entry numbers within these matrices indicate how many
minimal conflicts and dependencies, resp. have been found. For the example they
are shown in Fig. 1.More precisely, entry (rj, ri) (row, column) in the conflict matrix
in AGG describes all G(ri,mi)
⇒Hiwhich are asymmetrically parallel dependent on
G(rj,mj)
⇒Hjin a minimal context. Entry (rj, ri) in the dependency matrix in
AGG describes all G(rj,mj)
⇒Hj
(ri,mi)
⇒G0such that the second transformation is
asymmetrically sequential dependent on the first one in a minimal context. Note
that it is not possible yet to check with AGG if a pair of rules (rj, ri) is sequentially
independent as defined in Def.2.15. It is part of current work though to enrich the
dependency matrix with more information and thus enable this possibility.
5.2 Checking Applicability Criteria on Mutual Exclusion
We check applicability (i.e. liveness) of the following rule sequences:
requestRes, takeRes, releaseRes should be applicable to the right process in
the graph Gshown in Figure 1. We thus check for this rule sequence and graph
Gthat the applicability criteria in Def. 3.1 are satisfied.
(i) Rule requestRes is applicable to G.
(ii) Rule takeRes is asymmetrically parallel independent of rule requestRes. Fur-
thermore, rule releaseRes is asymmetrically parallel independent of requestRes
as well as takeRes.
(iii) Rules takeRes, releaseRes, giveRes are not applicable to G. Thus, we have
to show that their application is enabled by the rule applications performed
before. Rule takeRes is asymmetrically sequential dependent on requestRes,
and the concurrent rule of takeRes and requestRes is applicable on G. It
expresses how a resource can be requested and taken in one step. requestRes
is thus a direct enabling predecessor for takeRes. Moreover rule releaseRes is
purely sequential dependent on rule takeRes and therefore takeRes is a pure
11
Lambers, Ehrig, Taentzer
enabling predecessor for releaseRes.
requestRes, takeRes, releaseRes, giveRes is a slightly longer sequence and
should still be applicable to G. It is not possible though to fulfill in particu-
lar criterion 4 in Def. 3.1 for this sequence. However, it is still possible to fulfill
the applicability criteria for a summarized sequence as proven in Theorem 3.3. In
this case, it is possible to satisfy the criteria for the summarized sequence only. It
consists of one concurrent rule requestTakeReleaseGiveRes which is equal to the
rule nextProc.nextProc is applicable on Gand therefore the original sequence is
applicable on Gas well. Thus sometimes an applicable rule sequence as given in
this example might be hard to detect. This is because giveRes needs some sub-
graph of the start graph Gwhich is not needed by the other rules and in addition
all rules (except for the first one) are asymmetrically sequential dependent of the
previous rule.
5.3 Checking Non-Applicability Criteria on Mutual Exclusion
We check non-applicability (i.e. safety) of the following rule sequences:
requestRes, requestRes, nextProc specifies a request of both processes and
then a token transfer. This sequence should not be applicable on the start graph
Gin Fig. 1, since before transferring a token one of the requests should be pro-
cessed. We check the non-applicability criteria in Def. 4.1 for this rule sequence
on G.
(i) requestRes is applicable on the start graph G.
(ii) nextProc is not applicable on the start graph Gand is sequentially indepen-
dent on requestRes. Therefore the second criterion is fulfilled and there is no
enabling predecessor.
requestRes, giveRes specifies a request and then a token shift because the re-
source has been released. This sequence should not be applicable to the start
graph Gin Fig. 1, since the resource is still unused. It is easy to verify that
the criteria in Def. 4.1 are fulfilled. Moreover rule pair (requestRes,giveRes) and
(giveRes,requestRes) are sequentially independent. Therefore due to Theorem 4.3
we can conclude directly that sequence giveRes,requestRes is not applicable either
on G.
takeRes, takeRes specifies a take of the resource by both processes simultane-
ously. This sequence should not be applicable on the graph Hin Figure 1in
which both processes request the resource. Thus we check the non-applicability
criteria in Def. 4.1 for this sequence and graph H.
(i) The first rule takeRes is applicable to graph Hon the right process.
(ii) The second rule is again takeRes and we just mentioned that it is applicable
on the right process in H. We want to check though for safety reasons that
it is impossible to apply the second takeRes on the other (i.e. left) process
simultaneously. A matching of takeRes on the left process into Hdoes not
exist. For this kind of matching criterion 2 holds since in addition rule tak-
eRes is asymmetrically sequentially independent from itself. This means in
particular that the application of the first takeRes on the right process does
not enable the application of the second takeRes on the left process and hence
12
Lambers, Ehrig, Taentzer
such a rule application on His not possible.
This example demonstrates that sometimes it is necessary to include information
about the matches for the rule sequence to be checked for safety. Note moreover
that if we would have taken a longer sequence consisting of requestRes, requestRes,
takeRes and takeRes, we could not have checked the non-applicability of that
sequence on the start graph Gby Def. 4.1, since rule takeRes is asymmetrically
sequentially dependent on rule requestRes. Thus it is crucial in this case to select
the kernel sequence where the problem is conjectured and in particular this shows
us that our criteria are sufficient but not necessary.
6 Conclusion and Future Work
In this paper sufficient criteria are formulated for the applicability (resp. non-
applicability) of a rule sequence on a graph G. These criteria can be used to check
in a static way applicability resp. non-applicability of rule sequences. Future work
is concerned with formulating criteria for rules with attributes, further optimization
of the criteria, efficiently checking the satisfaction of the criteria and implementing
applicability checks in AGG. Furthermore, we like to evaluate the criteria in larger
case studies such as [4,7].
References
[1] Corradini, A., U. Montanari, F. Rossi, H. Ehrig, R. Heckel and M. L¨owe, Algebraic Approaches to Graph
Transformation I: Basic Concepts and Double Pushout Approach, in: G. Rozenberg, editor, Handbook of
Graph Grammars and Computing by Graph Transformation, Volume 1: Foundations, World Scientific,
1997 pp. 163–245.
[2] Ehrig, H., K. Ehrig, A. Habel and K.-H. Pennemann, Constraints and application conditions: From
graphs to high-level structures, in: F. Parisi-Presicce, P. Bottoni and G. Engels, editors, Proc. 2nd Int.
Conference on Graph Transformation (ICGT’04), LNCS 3256 (2004), pp. 287–303.
[3] Habel, A., R. Heckel and G. Taentzer, Graph Grammars with Negative Application Conditions, Special
issue of Fundamenta Informaticae 26 (1996), pp. 287–313.
[4] Lambers, L., H. Ehrig, L. Mariani and M. Pezz`e, Iterative model-driven development of adaptable service-
based applications, in: proceedings of the International Conference on Automated Software Engineering,
2007.
[5] Lambers, L., H. Ehrig and F. Orejas, Conflict Detection for Graph Transformation with Negative
Application Conditions, in: Proc. Third International Conference on Graph Transformation (ICGT’06),
LNCS 4178 (2006), pp. 61–76.
[6] Lambers, L., H. Ehrig, F. Orejas and U. Prange, Parallelism and concurrency in adhesive high-level
replacement systems with negative application conditions, in: H. Ehrig, J. Pfalzgraf and U. Prange,
editors, Workshop on Applied and Computational Category Theory (ACCAT’07) (2007).
[7] Mehner, K., M. Monga and G. Taentzer, Interaction Analysis in Aspect-Oriented Models, in: Proc. 14th
IEEE International Requirements Engineering Conference (2006), pp. 66–75.
[8] Taentzer, G., AGG: A Graph Transformation Environment for Modeling and Validation of Software,
in: J. Pfaltz, M. Nagl and B. Boehlen, editors, Application of Graph Transformations with Industrial
Relevance (AGTIVE’03), LNCS 3062, Springer, 2004 pp. 446 – 456.
URL AGG-Homepage:http://tfs.cs.tu-berlin.de/agg
[9] Velasco, P. and J. de Lara, Using matrix graph grammars for the analysis of behavioural specifications:
Sequential and parallel independence, in: Jornadas de Programacion y Lenguajes (PROLE2007), 2007.
13
Lambers, Ehrig, Taentzer
A Independency of Transformations
We repeat the definition of parallel and sequential independency for transformations
and afterwards the Local Church-Rosser Theorem for independent transformations.
Definition A.1 [parallel independent and sequential independent transformations]
Two direct transformations G(r1,m1)
=⇒H1with NACr1and G(r2,m2)
=⇒H2with NACr2
are parallel independent if
∃h12 :L1→D2s.t. (d2◦h12 =m1and e2◦h12 |=NACr1)
and
∃h21 :L2→D1s.t. (d1◦h21 =m2and e1◦h21 |=NACr2)
as in the following diagram:
N1N2
R1
K1//oo
L1
n1
OO
h12
''
m1
A
A
A
A
A
A
A
AL2
n2
OO
h21
ww
m2
~~}
}
}
}
}
}
}
}
K2
oo//
R2
H1D1d1//
e1
ooGD2
d2
ooe2//H2
Two direct transformations G(r1,m1)
=⇒H1with NACr1and H1
(r2,m2)
=⇒H2with NACr2
are sequentially independent if
∃h12 :R1→D2s.t. (d2◦h12 =m0
1and e2◦h12 |=NACr−1
1)
and
∃h21 :L2→D1s.t. (e1◦h21 =m2and d1◦h21 |=NACr2)
as in the following diagram:
N1N0
1N2
L1
n1
OO
K1//oo
R1
n0
1
OO
h12
''
m0
1!!
C
C
C
C
C
C
C
CL2
n2
OO
h21
ww
m2
}}|
|
|
|
|
|
|
|
K2
oo//
R2
GD1e1//
d1
ooH1D2
d2
ooe2//H2
Note that for n1:L1→N1in NACr1we have the corresponding n0
1:R1→N0
1
from NACr−1
1according to Def. 2.4.
Remark A.2 Note that it follows directly from this definition that we have the
following relationship between parallel and sequential independency: Gr1
⇒H1
r2
⇒H2
are sequentially independent iff Gr−1
1
⇐H1
r2
⇒H2are parallel independent.
14
Lambers, Ehrig, Taentzer
The following fact is proven in [6] and describes that independent transforma-
tions can be performed in any order with the same result.
Fact A.3 (Local Church-Rosser Theorem with NACs) Given a graph
transformation system with NACs and two parallel independent direct trans-
formations with NACs H1
r1,m1
⇐Gr2,m2
⇒H2, there are an object G0and direct
transformations H1
r2,m0
2
⇒G0and H2
r1,m0
1
⇒G0such that Gr1,m1
⇒H1
r2,m0
2
⇒G0and
Gr2,m2
⇒H2
r1,m0
1
⇒G0are sequentially independent. Vice versa, given two sequentially
independent direct transformations with NACs Gr1,m1
⇒H1
r2,m0
2
⇒G0there are an
object H2and sequentially independent direct transformations Gr2,m2
⇒H2
r1,m0
1
⇒G0
such that H1
r1,m1
⇐Gr2,m2
⇒H2are parallel independent:
H1r2,m0
2
"*
M
M
M
M
M
M
M
M
M
M
M
M
G
r1,m14<
r
r
r
r
r
rr
r
r
r
r
r
r2,m2"*
L
L
L
L
L
L
L
L
L
L
L
LG0
H2
r1,m0
1
4<
q
q
q
q
q
qq
q
q
q
q
q
B Correctness of the Criteria
Theorem B.1 (no impeding predecessors and pure or direct enabling predecessor)
Given s:r1r2. . . rna sequence of nrules and a graph G0. If the criteria in Def. 3.1
are satisfied for rule sequence sand graph G0, then this rule sequence is ap-
plicable on G0with injective matching i.e. there exists a graph transformation
G0
r1
⇒G1. . . Gn−1
rn
⇒Gnwith injective matching.
Proof Note that because of criterion 2 and the fact that only injective matching is
allowed it is always possible to construct the pushout complement of Gm
←Ll
←K
with man injective match and lthe left-hand side rule morphism. The gluing
condition is thus fulfilled. This means in particular that as soon as a match m
is found for a rule rinto a graph G, this rule is applicable on Gif the NAC is
satisfied. Now we prove this theorem by induction over the number of rules in the
rule sequence s.
•(Basis. n= 1)Criterion 1 ensures that a match m1:L1→G0exists. The fact
that the gluing condition is always satisfied and m1satisfies NACr1allows us to
construct therefore the direct transformation G0
m1
⇒G1.
•(Induction Step.) Consider the transformation G0
r1
⇒G1. . . rn−1
⇒Gn−1. We are
now looking for a match mn:Ln→Gn−1such that also the direct transformation
Gn−1
rn
⇒Gnexists. We have the following two cases.
(i) Rule rnis applicable on G0via an injective match mn. We know because of
criterion 3 in Def. 3.1 that rnis asymmetrically parallel independent on each
rule rjin the sequence swith j < n. According to criterion 4b we know also
that rnis asymmetrically parallel independent on rj=rc. Therefore we have
the following diagram where j= 1 and there exists a morphism hn,1:Ln→D1
15
Lambers, Ehrig, Taentzer
with d1◦hn,1=mn(which implies that hn,1is injective) and e1◦hn,1|=NACrn:
N1Nn
R1
K1//oo
L1
n1
OO
m1
B
B
B
B
B
B
B
BLn
nn
OO
hn,1
ww
mn
~~|
|
|
|
|
|
|
|
Kn
oo//
Rn
G1D1d1//
e1
ooG0D0
n
oo//H0
n
Considering e1◦hn,1as an injective match of rninto G1satisfying NACrnwe
can construct the following diagram where j= 2 and there exists a morphism
hn,2:Ln→D2with d2◦hn,2=e1◦hn,1and e2◦hn,2|=NACrn.
N2Nn
R2
K2//oo
L2
n2
OO
m2!!
B
B
B
B
B
B
B
BLn
nn
OO
hn,2
wwe1◦hn,1
}}{
{
{
{
{
{
{
{
Kn
oo//
Rn
G2D2d2//
e2
ooG1D”n
oo//H”n
Iteratively we can construct analog diagrams such that in the end the following
diagram arises where j=n−1 and there exists a morphism hn,n−1:Ln→Dn−1
with dn−1◦hn,n−1=en−2◦hn,n−2and en−1◦hn,n−1|=NACrn.
Nn−1Nn
Rn−1
Kn−1//oo
Ln−1
nn−1
OO
mn−1$$
H
H
H
H
H
H
H
H
HLn
nn
OO
hn,n−1
uuen−2◦hn,n−2
||xxxxxxxxKn
oo//
Rn
Gn−1Dn−1dn−1//
en−1
ooGn−2D
oo//H
Considering en−1◦hn,n−1as an injective match of rninto Gn−1we can apply
now rule rnto Gnand have the direct transformation Gn
rn
⇒Gn+1.
(ii) There does not exist an injective match of rule rninto G0. Now we have two
cases.
·Criterion 4a in Def. 3.1 holds. Then there exists a rule rjin ssuch that
1≤j < n and rnis purely sequential dependent on rj. This means that rn
does not have any NACs and we have an injective morphism ln,j :Ln→Rj
according to Def. 2.12. Consider now the comatch m0
j:Rj→Gjof the direct
transformation Gj−1
rj
⇒Gj. We then have an injective match m0
j◦ln,j :Ln→
Gjfor the rule rninto Gj. Now analogously to the previous case we can use
16
Lambers, Ehrig, Taentzer
criterion 3 to construct the following diagram
Nj+1
Rj+1
Kj+1 //oo
Lj+1
j+1
OO
mj+1
2
2
2
2
2
2
2
2
2
2
2
2
2
2
2Ln
l0
n,j
hn,j+1
{{
m0
j◦ln,j
Kn
oo//
Rn
Rj
m0
j
~~}}}}}}}
Gj+1 Dj+1 dj+1 //
ej+1
ooGjD
oo//H
and in the end the requested injective match en−1◦hn,n−1:Ln→Gn−1and
thus the direct transformation Gn
rn
⇒Gn+1 exists.
·Criterion 4b in Def. 3.1 holds. Then there exists a concurrent rule rcof rn−1
and rnwith an injective match of rcinto G0satisfying NACrcand rcis asym-
metrically parallel independent on rjfor all j < (n−1). (direct enabling
predecessor) We now have a rule sequence s0:r1r2. . . rn−2rcfor which the
criteria in Def. 3.1 are fulfilled. This means that there exists a graph trans-
formation sequence along the sequence s0:r1r2. . . rcand therefore according
to the Concurrency Theorem with NACs in [6] also along the rule sequence
s:r1r2. . . rn−1rn.
2
Theorem B.2 (no impeding predecessors and pure or direct enabling predecessors)
3.3 Given a sequence s:r1r2. . . rnof nrules and a graph G0. If the criteria
in Def. 3.1 are satisfied for a rule sequence s0:r0
1r0
2. . . r0
mwith m < n in which
neighbored rules in scan be summarized by a concurrent rule, then the original
rule sequence sis applicable on G0with injective matching i.e. there exists a graph
transformation G0
r1
⇒G1. . . Gn−1
rn
⇒Gnwith injective matching.
Proof This follows directly from the Concurrency Theorem with NACs [6] and
Theorem 3.2.2
Theorem B.3 (no enabling predecessor) Given a sequence s:r1r2. . . rnof n
rules and a graph G0. If the criteria in Def. 4.1 are satisfied for rule sequence s
and graph G0, then this rule sequence is not applicable on G0i.e. there exists no
graph transformation G0
r1
⇒G1. . . Gn−1
rn
⇒Gn.
Proof
•If criterion 1 in Def. 4.1 is satisfied then it is obvious that a graph transformation
sequence can not exist.
•Suppose that criterion 2 in Def. 4.1 is satisfied. Then ∃riin swith 1 < i ≤n
such that there does not exist a match into G0satisfying NACribut for all rules
rjin swith 1 ≤j < i ≤n,riis asymmetrically sequential independent on rj.
Suppose that a graph transformation G0
r1
⇒G1. . . Gn−1
rn
⇒Gnexists. Then we
17
Lambers, Ehrig, Taentzer
have the following diagram:
Ni−1Ni
Li−1
ni−1
OO
Ki−1//oo
Ri−1
##
G
G
G
G
G
G
G
G
GLi
ni
OO
hi,i−1
uu
mi
||zzzzzzzzKi
oo//
Ri
Gi−2Di−1ei−1//
di−1
ooGi−1Di
di
ooei//Gi
Because of the assumption and Def. 2.10 we know that hi,i−1exists such that
ei−1◦hi,i−1=miand di−1◦hi,i−1|=NACri. Therefore we can now construct
the following diagram:
Ni−2Ni
Li−2
ni−2
OO
Ki−2//oo
Ri−2
##
F
F
F
F
F
F
F
F
FLi
ni
OO
hi,i−2
uudi−1◦hi,i−1
}}{{{{{{{{Ki
oo//
Ri
G0
i−3D0
i−2e0
i−2
//
d0
i−2
ooGi−2Di
di
ooei//Gi
Again because of the assumption and Def. 2.10 we know that hi,i−2exists such
that e0
i−2◦hi,i−2=di−1◦hi,i−1and d0
i−2◦hi,i−2|=NACri. Iteratively in the
end we will find a match m|=NACri:Li→G0and this is a contradiction.
Therefore a graph transformation G0
r1
⇒G1. . . Gn−1
rn
⇒Gncan not exist.
2
18
