Efficient Process Analysis of Transformation Systems Based on Petri nets [original]

Forschungsberichte

der Fakultät IV – Elektrotechnik und Informatik

Efficient Process Analysis of

Transformation Systems

Based on Petri nets

Frank Hermann, Andrea Corradini, Hartmut Ehrig and

Barbara König

Bericht-Nr. 2010-03

ISSN 1436-9915

Efficient Process Analysis of

Transformation Systems Based on Petri Nets

Frank Hermann1, Andrea Corradini2, Hartmut Ehrig1and

Barbara K¨onig3

1{frank,ehrig}@cs.tu-berlin.de, Institut f¨ur Softwaretechnik und Theoretische

Informatik, Technische Universit¨at Berlin, Germany

2[email protected], Dipartimento di Informatica, Universit`a di Pisa, Italy

3barbara [email protected], Abteilung f¨ur Informatik und Angewandte

Kognitionswissenschaft, Universit¨at Duisburg-Essen, Germany

Abstract

In the framework of adhesive transformation systems with Negative Application

Conditions (NACs), we show how the problem of computing the set of equivalent

derivations to a given one can be reduced to the analysis of the reachability graph of a

generated Place/Transition Petri net. This net encodes the dependencies among rule

applications of the derivation, including the inhibiting effects of the NACs. We show

the effectiveness of this approach by comparing the cost of a brute force-approach

with the cost of the presented analysis applied to a derivation of a simple system,

showing a significant improvement in speed.

1 Introduction

Given a workflow of a system, it is often interesting to know whether the workflow can be

rearranged, by executing the tasks in a different order, which might be more convenient

for the user or preferable from an efficiency point of view. If the workflow is modelled by a

Petri net representing a deterministic process, these questions can be fairly easily answered:

processes incorporate a notion of concurrency that can be exploited to rearrange the tasks,

while still respecting causality. We are here considering workflow models with two further

dimensions, which considerably complicate the problem: first, we work in the general

setting of adhesive categories where we can model systems with an evolving topology, such

as graph transformation systems, in contrast to systems with a static structure like Petri

nets. The analysis can be further extended to the class of weak adhesive categories using the

results in [10]. Second, we take into account Negative Application Conditions (NACs) that

are used to ensure the “absence” of forbidden structures when executing a transformation

step: NACs significantly improve the specification formalisms based on transformation

rules leading to more compact and concise models as well as increased usability and as

a matter of fact they are widely used in non-trivial applications. The presence of NACs

leads to more complex interdependencies of tasks. Both dimensions are needed e.g. for the

analysis of workflows in mobile ad-hoc networks.

For this reason, we introduce a notion of permutation equivalence on derivations with

NACs, which is coarser and more adequate than the switch equivalence in the double-

pushout (DPO) approach including NACs. As defined in [9] two derivations are called

permutation-equivalent, if they respect the NACs and disregarding the NACs they are

switch-equivalent. Using the notion of switch equivalence with NACs directly does not

lead to all permutation-equivalent derivations of a given derivation in general. The main

remaining problem is how to derive the complete set of all permutation-equivalent deriva-

tions to a given one. For this purpose, we construct a subobject transformation system

(STS) via a standard colimit construction and from this STS we construct a dependency

net, given by a standard P/T Petri net, which includes a complete account of the inhibit-

ing effects of the NACs. The main result shows that complete firing sequences of this net

are one-to-one with derivations that are permutation-equivalent to the given derivation,

allowing us to derive the complete set of permutation-equivalent derivations.

Finally, for a given derivation of a simple example system with NACs, we perform a

detailed complexity analysis of the cost of identifying all permutation-equivalent derivations

using the reduction to a Petri net and its reachability graph, and compare it with a brute

force approach computing all shift-equivalent derivations first, and then filtering out the

ones which do not respect the NACs. We obtain a significant improvement in speed, which

shows that the proposed technique can be efficient for many applications which involve the

generation of permutation-equivalent derivations. Furthermore, the constructed P/T Petri

net can be used to derive specific permutations without generating the complete set first.

In the context of workflow analysis, both goals are of central interest for the modelling of

a system.

The structure of the paper is as follows. Sec. 2 reviews the main concepts of transfor-

mation systems over an adhesive category, permutation equivalence for derivations and the

process construction based on subobject transformation systems, elaborating on the results

of [9]. The construction of the process skeleton given by a Petri net is presented in Sec. 3

and it is shown to be sound and correct for computing the set of permutation-equivalent

derivations. Thereafter, Sec. 4 validates the efficiency of the analysis based on an extended

version of the running example. Finally, Sec. 5 sums up the main results, discusses related

work, and points out aspects of future work.

2 Transformation Systems and Permutation

Equivalence

Most definitions and results of the DPO approach, originally developed for graphs [7]

and similar structures, have been generalized to adhesive categories [13, 6]: these are

categories where pushouts along monos “behave well” with respect to pullbacks. Because

of this, it is quite natural to present our contribution at this level of generality, by referring

all definitions to an arbitrary but fixed adhesive category C; the reader unfamiliar with

adhesive categories can safely identify Cwith a standard category of graphs, like those

used in the examples.

Definition 1 (Adhesive categories).A category is called adhesive if (1) it has pullbacks;

(2) it has pushouts along monos; and (3) pushouts along monos are Van Kampen squares.

~~~

(1)

~~}

}

sshhhhhhhhhf0



g0%%



ttiiiiiiiii



(2)

(1)

hhhh

ssh

g&&

sshhhhhhhhhh

Referring to the diagram above, a Van Kampen square is a pushout (1) which satisfies the

following property: if we draw a commutative cube (2) which has (1) as its bottom face

and whose back faces are pullbacks then the front faces of the cube are pullbacks if and

only if its top face is a pushout.

For the rest of the section, let Cbe an arbitrary but fixed adhesive category: all

objects and arrows are assumed to belong to C. We recall some basic definitions of the

DPO approach with NACs.

Definition 2 (Transformation System with NACs).Arule is a pair of monos with the

same source in C,p= (Lp

←- Kp

,→Rp). A Negative Application Condition (NAC) for a

rule pis a mono n:Lp,→N, having the left-hand side of pas source. A rule with NACs

is a pair hp, Niwhere pis a rule and N={ni:Lp,→Ni}i∈Iis a finite set of NACs for

p. A match of a rule pin an object Gis a mono m:Lp,→G; match msatisfies the NAC

n:Lp,→Nfor p, written m|=n, if there is no arrow g:N→Gsuch that g◦n=m.1

We say that there is a direct derivation respecting NACs from an object Gto Husing a

rule with NACs hp, Niand a match m:Lp→G, if (a) there are two pushouts (1) and

(2) in C, as depicted; and (b) m|=nfor each NAC (n:Lp,→N)∈N. If condition

(a) above is satisfied (and (b) possibly not, thus NACs are ignored) we say that there is a

direct derivation from Gto H. In both cases we write G=

p,m

==⇒H.

1Intuitively, the image of Lpin Gcannot be extended to an image of the “forbidden context” N.



(1)



r//

(2)



G D //ooH

Atransformation system (TS) with NACs over Cis a pair G=hQ, πNiwhere Qis a set

of rule names, and πNmaps each name q∈Qto a rule with NACs πN(q) = hπ(q),Nqi.

Aderivation (respecting NACs) of Gis a sequence G0=

q1,m1

===⇒G1· · · =

qn,mn

===⇒Gn, where

q1, . . . , qn∈Qand di=Gi−1=

π(qi),mi

====⇒Giare direct derivations (respecting NACs) for

i∈1, . . . , n. Sometimes we denote a derivation as a sequence d=d1;. . . ;dnof direct

derivations.

continueTask

:worksOn

1:Person

3:started

1:Person

2:Task

NAC2

:worksOn

1:Person

2:Task

3:started

2:Task

3:started

2:Task

:worksOn

1:Person

2:Task

1:Person

2:Task

1:Person

2:Task

NAC1

:worksOn

:Person

2:Task

1:Person

stopTask

3:started

:worksOn

:started

Person

Task

Type Graph

Figure 1: Part of transformation system GS, modeling task assignment

w1:worksOn

1:Person

3:Task 4:started

2:Person

⇒ ⇒ ⇒

1:Person

3:Task 4:started

2:Person G2

1:Person

3:Task 4:started

2:Person G3

w2:worksOn

1:Person

3:Task 4:started

2:Person G4

1:Person

3:Task 4:started

2:Person

⇒

Figure 2: Derivation d(respecting NACs) of GS

Example 1 (Graph Transformation System with NACs).The adhesive category used in

the examples of this paper is (Graph↓TG), i.e., the slice category of directed graphs over

the graph TG of Fig. 1. Thus, objects are graphs with a typing morphism to TG, and

arrows are graph morphisms preserving the typing. Fig. 1 shows a part of GS, a TS with

NACs for specifying the assignment of tasks to persons, which is a little fragment of a

workflow modeling system. The type graph TG shows that nodes in the system represent

either persons or tasks: a task is active if it has a “:started” loop, and it can be assigned

to a person with a “:worksOn” edge. Rule “stopTask” cancels the assignment of a task to a

person; rule “continueTask” instead assigns the task, and it has two NACs to ensure that

the task is not assigned to a person already. Other rules are omitted, because they are not

used in the paper. Fig. 2 shows a derivation respecting NACs of GS. The only task is first

assigned to node “1:Person”, and then, after being stopped, to node “2:Person”.

The classical theory of the DPO approach (without NACs) introduces an equivalence

among derivations which relates derivations that differ only in the order in which indepen-

dent direct derivations are performed. The switch equivalence is based on the notion of

sequential independence and on the Local Church-Rosser theorem. This is briefly summa-

rized in the next definition.

Definition 3 (Switch Equivalence on Derivations).Let d1=G0=

p1,m1

===⇒G1and d2=

G1=

p2,m2

===⇒G2be two direct derivations. Then they are sequentially independent if there

exist arrows i:R1→D2and j:L2→D1such that l0

2◦i=m0

1and r0

1◦j=m2(see the

diagram on the right, which shows part of the derivation diagrams).



//R1



((









D1r0

1//G1D2

If d1and d2are sequentially independent, then according to the Local Church Rosser

Theorem (Thm. 5.12 in [6]) they can be “switched” obtaining direct derivations d0

G0=

p2,m2

===⇒G0

1and d0

1=G0

p1,m1

===⇒G2, which apply the two rules in the opposite order.

Now, let d= (d1;. . . ;dk;dk+1;. . . ;dn)be a derivation, where dkand dk+1 are two

sequentially independent direct derivations, and let d0be obtained from dby switching them

according to the Local Church Rosser Theorem. Then, d0is a switching of d, written

dsw

∼d0. The switch equivalence, denoted sw

≈, is the smallest equivalence on derivations

containing both sw

∼and the relation ∼

=for isomorphic derivations.2

Corresponding notions of parallel and sequential independence have been proposed

for graph transformation systems with NACs [8, 14]. However, the derived notion of

switch equivalence does not identify all intuitively equivalent derivations. The reason

is that, in presence of NACs, there might be an equivalent permutation of the direct

derivations that cannot be derived by switch equivalence. Looking at din Fig. 2 there

is no pair of consecutive direct derivations which is sequentially independent if NACs are

considered. However, the derivation d0should be considered as equivalent. There are

also examples in which even the switching of blocks of several steps would not lead to all

permutation-equivalent derivations. This brings us to the following, quite natural notion

of permutation equivalence of derivations respecting NACs, first proposed in [9]. Note

that for permutation-equivalent derivations dπ

≈d0the sequence of rules used in d0is a

permutation of those used in d.

Definition 4 (Permutation Equivalence of Derivations).Two derivations dand d0respect-

ing NACs are permutation equivalent, written dπ

≈d0if, disregarding the NACs, they are

switch equivalent as for Def. 3.

2Informally, d∼

=d0if they have the same length and there are isomorphisms between the corresponding

objects of dand d0compatible with the involved morphisms.

G’1

w1:worksOn

1:Person

3:Task 4:started

2:Person

⇒ ⇒ ⇒

1:Person

3:Task

4:started

2:Person G’2

1:Person

3:Task 4:started

2:Person G’3

w2:worksOn

1:Person

3:Task 4:started

2:Person G4

1:Person

3:Task 4:started

2:Person

⇒

Figure 3: Permutation-Equivalent Derivation d0(respecting NACs) of GS

In the theory of Petri nets [15], from a given firing sequence one can build a deterministic

process, which is a net which records all the transitions fired in the sequence, together with

their causal dependencies. Similar constructions have been proposed for graph transforma-

tion [5] and for transformation systems based on adhesive categories [2, 4]. In particular,

in [4] it is shown that starting with a derivation, with a suitable colimit construction in C

one can build a Subobject Transformation System (STS). An STS can be considered as a

double-pushout transformation system over the (distributive) lattice of subobjects Sub(T)

of a given object T∈C. Informally, a subobject of Tis an equivalence class of monos with

target T, and in this framework rewriting can be defined with a set-theoretical notation:

A⊆Bmeans that there is a mediating arrow from subobject Ato B, the meet A∩Bin

Sub(T) is obtained as a pullback in C, and the join A∪Bis a suitable pushout (thanks

to adhesivity of C[13]). We briefly recall the basic theory of STSs and then extend it to

systems with NACs.

Definition 5 (STS of a derivation).Asubobject transformation system S=hT, Q, πi

over an adhesive category Cconsists of a super object T∈C, a set of rule names Q, and

a function π, which maps a name q∈Qto a rule, i.e., to a triple π(q) = hLq, Kq, Rqiof

subobjects of Tsuch that Kq=Lq∩Rq.

Given objects G, H ∈Sub(T)and a rule π(q) = hLq, Kq, Rqi, there is a direct deriva-

tion G=

⇒Hif there exists an object D∈Sub(T)such that (a) G=Lq∪D, (b)

Kq=Lq∩D, (c) H=Rq∪D, and (d) Kq=Rq∩D.

Now, let G=hQ, πibe a transformation system over C, and let d= (G0=

q1,m1

===⇒

. . . =

qn,mn

===⇒Gn)be a derivation of G. The STS generated from dis defined as Prc(d) =

hT, P, ˆπi, where Tis the colimit object in Cof the diagram underlying the derivation d,P=

{dk|dk= (Gk−1=

pk,mk

===⇒Gk)is a step of d}, and ˆπ(dk) = h[inT(Lpk)],[inT(Kpk)],[inT(Rpk)]i,

where inT(X)is the injection of Xin the colimit T.

For the rest of the paper, we consider only derivations such that the colimit T is a finite

object, i.e. Sub(T) is a finite lattice. This is guaranteed if each rule of Ghas finite left- and

right-hand sides, and if the start object of the derivation is finite. In the STS generated

from a derivation dwe can identify all derivations which are switch equivalent to dsimply

checking how the rules overlap in Prc(d). We summarise some relevant facts presented in

[4].

Definition 6 (Switch Equivalence of Derivations in STS).Given an STS S= (T, Q, π),

two rules π(qi) = hLi, Ki, Rii,i∈ {1,2}, are called independent (written q1♦q2) if (L1∪

R1)∩(L2∪R2)⊆K1∩K2. Let dbe a derivation in Sand let s=hq1, . . . , qnibe its corre-

sponding sequence of rule names. If qk♦qk+1, then the sequence s0=hq1, . . . , qk+1, qk, . . . , qni

is switch equivalent to the sequence s, written ssw

∼Ss0. The switch equivalence sw

≈Son

sequences of rule names is the reflexive and transitive closure of sw

∼S.

Proposition 1 (Analysis of Switch Equivalence using Prc(d)).

Let d=d1;. . . ;dk;dk+1;. . . ;dnbe a derivation of a TS over C, and let Prc(d)be the

generated STS. Then dkand dk+1 are sequential independent if and only if dk♦dk+1 in

Prc(d). As a consequence, a derivation d0is shift equivalent to d(d0sw

≈d) if and only if

in Prc(d)the sequence of names of d,sd=hd1, . . . , dniis shift equivalent to the sequence

sd0(sd

≈Prc(d)sd0), which contains all the direct derivations of din the order they are

actually fired in d0.

We discuss now how to extend this result to TSs with NACs, and how Prc(d) can be

used to identify the derivations which are permutation equivalent to d.

Definition 7 (STS with NACs).Let p=hLp, Kp, Rpibe a rule in Sub(T), with T∈C.

Anegative application condition for pis an object N∈Sub(T)such that Lp⊆N. A

rule with NACs is a pair hp, Ni, where pis a rule and N=hN[1], N[2], . . . , N[k]iis an

ordered list of NACs for p(we denote by |N|the length of N). An STS with NACs is an

STS S=hT, Q, πNisuch that πN(q) = hπ(q),Nqiis a rule with NACs. A direct derivation

⇒Has in Def. 5 respects the NACs Nqif it holds: (e) for all 0< i ≤ |Nq|,N[i]6⊆ G.

The generation of an STS with NACs from a given derivation works as in Definition

5, but additionally each rule will be equipped with a list of NACs, i.e., those obtained as

“instances” of the original NACs in the colimit object T.

Definition 8 (Instantiated NACs).Let Gbe a TS with NACs and let d=d1;. . . ;dk;. . . ;dn

be a derivation respecting NACs. Let hp, Nibe the rule with NACs used in direct derivation

dk, let Tbe the colimit object of the derivation, and let inT(Lp)be the injection in Tof

the left-hand side of p. Let n:Lp,→Nbe a NAC of p; an instantiated NACs of nin Tis

a subobject [j:N ,→T]∈Sub(T)such that j◦n=inT(Lp). The set of all instantiated

NACs in Tof all NACs of a rule pis denoted by NACST(p).

Definition 9 (STS of a Derivation with NACs).Let Gbe a TS with NACs and let d

be a derivation of Grespecting NACs. The STS with NACs generated by dis given by

PrcN(d) = hT, P, ˆπNi, where Tand Pare as in Def. 5, ˆπN(dk) = hˆπ(dk),Nki,ˆπ(dk)is as

in Def. 5, and Nkis an arbitrary but fixed linearisation of NACST(pk), where pkis the

rule of Gused in dk.

Example 2 (Derived Process Prc(d)).For the derivation in Ex. 1 the process construction

leads to the STS as shown in Fig. 4. The derivation dinvolves the rules “continueTask”

and “stopTask” and thus, the derived STS contains the rule occurrences “cont1”, “cont2”,

“stop1” and “stop2”, where the NACs of the rule “continueTask” are instantiated.

w1:worksOn

1:Person 3:Task

4:started

2:Person

w2:worksOn

q1=cont1

w1:worksOn

1:Person

4:started

1:Person

3:Task

N1[2]

w2:worksOn

2:Person

3:Task

4:started

3:Task

4:started

3:Task

w2:worksOn

1:Person

3:Task

1:Person

3:Task

2:Person

3:Task

N1[1]

w1:worksOn

1:Person

3:Task

1:Person

q4=stop2

w1:worksOn

1:Person

3:Task

1:Person

3:Task

1:Person

3:Task

q2=stop1

q3=cont2

w2:worksOn

2:Person

4:started

2:Person

3:Task

4:started

3:Task

4:started

3:Task

4:started

N3[2]

w2:worksOn

2:Person

3:Task

N3[1]

w1:worksOn

1:Person

3:Task

2:Person

4:started

Figure 4: Derived Process Prc(d) as Subobject Transformation System

The following relations between the rules of an STS with NACs specify the possible

dependencies among them: the first four relations are discussed in [4], while the last two

are introduced in [9].

Definition 10 (Relations on Rules).Let q1and q2be two rules in an STS with NACs

S= (T, P, πN)with πN(qi)=(hLi, Ki, Rii,Ni)for i∈ {1,2}. The relations on rules are

defined on Pas follows:

Name Notation Condition

Read Causality q1<rc q2R1∩K2*K1

Write Causality q1<wc q2R1∩L2*K1∪K2

Deactivation q1<dq2K1∩L2*K2

Independence q1♦q2(L1∪R1)∩(L2∪R2)⊆K1∩K2

Weak NAC Enabling q1<wen[i]q20< i ≤ |N2| ∧ L1∩N2[i]*K1∪L2

Weak NAC Disabling q1<wdn[i]q20< i ≤ |N1| ∧ N1[i]∩R2*L1∪K2

In words, q1<wen[i]q2(read: “q1weakly enables q2at i”) if q1deletes a piece of the i-th

NAC of q2; instead q1<wdn[i]q2(“q2weakly disables q1at i”) if q2produces a piece of the

i-th NAC of q1. It is worth stressing that the relations introduced above are not transitive

in general.

Example 3 (Relations of an STS).The rules of Prc(d)in Fig. 4 are related by the following

dependencies. For write causality we have “cont1 <wc stop1” and “cont2 <wc stop2”. The

further dependencies are shown in in the table below.

Weak Enabling Weak Disabling

stop1<wen[1] cont1 stop2<wen[2] cont1 cont1<wdn[1] cont1 cont2<wdn[2] cont2

stop1<wen[1] cont2 stop2<wen[2] cont2 cont2<wdn[1] cont1 cont1<wdn[2] cont2

The following notion of legal sequences of rule names builds the basis for the analysis of

permutation equivalence of derivations with NACs within the constructed STS. It requires

that for every NAC N[i] of a rule qkof Prc(d), either there is a rule which deletes part of

N[i] and was fired before qk, or there is a rule which produces part of N[i] and is fired after

qk: In both cases N[i] cannot be present when firing qk, because the STS Prc(d) is a sort

of “unfolding” of the derivation, and every subobject is created at most once and deleted

at most once (see [4]).

Definition 11 (Legal Sequence).Let d= (d1;. . . ;dn)be a derivation respecting NACs in a

TS, and let Prc(d)=(T, P, πN)be its derived STS with NACs. A sequence s=hq1;. . . ;qni

of rule names of Pis locally legal at position k∈ {1, . . . , n}with respect to d, if each rule

name in Poccurs exactly once in sand the following conditions hold:

1. ssw

≈Prc(d)seq(d)

2. ∀NAC Nk[i]of qk:∃e∈ {1, . . . , k −1}:qe<wen[i]qkor

∃l∈ {k, . . . , n}:qk<wdn[i]ql.

A sequence sof rule names is legal with respect to d, if it is locally legal at all positions

k∈ {1, ..., n}with respect to d.

Theorem 1 (Analysis of Permutation Equivalence using Prc(d)).Let d=d1;. . . ;dnbe a

derivation respecting NACs of a TS with NACs over C, and let Prc(d)be the generated

STS with NACs. Then a derivation d0is permutation equivalent to d(d0π

≈d) if and only

if in Prc(d)the sequence of names sd0, which contains all the direct derivations of din the

order they are actually fired in d0, is legal with respect to d.

By Thm. 1 we can transfer the analysis of permutation equivalence from derivations

to sequences of rule names. Thus, given a derivation drespecting NACs we construct the

process model Prc(d) according to Def. 9, compute the relations for the STS, and then

generate the legal sequences w.r.t. daccording to Def. 11, which identify the derivations

permutation equivalent to d.

3 Construction of the Process Skeleton

Based on the process of a derivation given by an STS, we now present the construction

of its “process skeleton”, given by a P/T Petri net which specifies only the dependencies

between the derivation steps. All details about the internal structure of the objects and

the transformation rules are excluded, allowing us to further increase the efficiency of the

analysis of permutation equivalence.

Definition 12 (Process skeleton Prc of a derivation).Let dbe a derivation respecting

NACs of a TS with NACs over C, let Prc(d)be the generated STS with NACs and let

s=seq(d) = hq1, . . . , qnidenote the sequence of rule names in Prc(d)according to the

steps in d. The process skeleton of dis given by the marked Petri net Prc(d) = hN, Mi,

N=hPL,TR, pre, posti, defined as follows:

- TR ={qk|k∈ {1, . . . , n}}

- PL ={p(k)|qk∈TR} ∪{p(j <xk)|qj<xqk∧x∈ {rc, wc, d}

∪{p(k, N[i]) |Nk[i]is a NACof qkin Prc(d)∧qk≮wdn[i]qk}

-pre(qk) = p(k)⊕X

qj<xqk

x∈{rc,wc,d}

p(j <xk)⊕X

qj<wdn[i]qk

j6=k

p(j, N[i]) ⊕X

p(k,N[i])∈PL

p(k, N[i])

-post(qk) = X

qk<xql

x∈{rc,wc,d}

p(k <xl)⊕X

qk<wen[i]ql

p(l, N[i]) ⊕X

p(k,N[i])∈PL

p(k, N[i])

-M=X

qk∈TR

p(k)⊕X

qj<wdn[i]qk

p(j,N[i])∈PL

p(j, N[i])

3. For all i,qkwith qk≮wdn[i] qk

2. For all qk<xql, x ∈{rc,wc,d }

1. For each qk ∈P

Prc(d)= (S,T,P,¼)Prc(d)= ((PL,TR,pre,post),M)

a) N[i] of qk

b) For all qe<wen[i] qk

c) For all qk<wdn[i] ql

3. For all i,qkwith qk≮wdn[i] qk

2. For all qk<xql, x ∈{rc,wc,d }

1. For each qk ∈P

Prc(d)= (S,T,P,¼)Prc(d)= ((PL,TR,pre,post),M)

a) N[i] of qk

b) For all qe<wen[i] qk

c) For all qk<wdn[i] ql

p(j<xk)ql

qkp(j<xk)ql

p(k,N[i]) qk

p(k,N[i])qe

+p(k,N[i])qe

p(k,N[i]) ql

p(k,N[i])

p(k)qk

+++

p(k)qk

+++

Figure 5: Visualization of the Construction of the Petri net

Related document tools

Review similarity, sources and trust signals

Plag helps review text similarity and possible source overlap. Identific is designed for document-focused trust and verification tasks. They make it easier to notice issues early.

plag.ai

Fig. 5 presents an intuitive view of the construction in Def. 12. Gray line colour and

plus-signs mark the inserted elements. The tokens of the initial marking are represented

by bullets that are connected to their places by arcs. In the first step each rule is encoded

as a transition and it is connected to a marked place for ensuring that it cannot fire twice.

In step 2, between each pair of transitions in each of the relations <rc,<wc and <d, a

new place is created in order to enforce the corresponding dependency. The rest of the

construction is concerned with places which correspond to NACs and can contain several

tokens in general. Each token in such a place represents the absence of a piece of the

NAC; therefore if the place is empty, the NAC is complete. In this case, by step (3a)

the transition cannot fire. Consistently with this intuition, if q <wen[i]p, i.e. transition q

consumes part of the NAC N[i] of p, then by step (3b) qproduces a token in the place

corresponding to N[i]. Symmetrically, if q<wdn[i]p, i.e. pproduces part of NAC N[i] of q,

then by step (3c) pconsumes a token from the place corresponding to N[i]. Notice that if

a rule generates part of one of its NACs, say N[i] (qk<wdn[i]qk), then by the acyclicity of

Prc(d) the NAC N[i] cannot be completed before the firing of qk: therefore we ignore it in

the third step of the construction of the process skeleton.

Note that the constructed net is a true (bounded) P/T net, and not a safe one, because

the places for the NACs can contain several tokens. A bound is given by the maximum,

taken over places representing NACs, of the number of rules that either weakly disable or

weakly enable the specific NAC.

We now show that we can exploit the constructed Petri net Prc(d) to characterize

the derivations that are permutation equivalent to d, by analysing its firing behaviour.

Note that according to Def. 12 each sequence sof rule names in the STS Prc(d) can

be interpreted as a sequence of transitions in the derived marked Petri net Prc(d), and

vice versa. This correspondence allows us to transfer the results of the analysis back to

the STS. More precisely, we can generate the set of all permutation-equivalent sequences

by constructing the reachability graph of Prc(d), which therefore can be considered as a

compact representation of this equivalence class.

For the following theorem, recall that a transition complete firing sequence of a Petri

net is a firing sequence where each transition of the net occurs at least once; notice also

that in a process skeleton according to Def. 12, each transition can fire at most once by

construction.

Theorem 2 (Analysis based on Petri Nets).Let dbe a derivation respecting NACs of a

TS with NACs over C, then:

sπ

≈Prc(d)seq(d)iff sis a transition complete firing sequence of Prc(d),

i.e. sis a legal sequence with respect to diff sis a firing sequence of the skeleton process

of dgiven by the marked P/T Petri net Prc(d)and each transition occurs at least once in

In order to prove Thm. 2 we use Lemma 1 below, which we prove first. The lemma

states that switch equivalence without NACs of rule sequences in an STS respects the

partial order of the relations “<rc, <wc” and “<d”, and vice versa: if the order is respected

then the two sequences are switch equivalent.

Lemma 1 (Linearisation).Let dbe a derivation respecting NACs of a TS with NACs over

C, let Prc(d)be the generated STS with NACs, and let s=hq1, . . . , qnibe a permutation

of seq(d). Then,

ssw

≈Sseq(d)iff ∀i, j ∈ {1, . . . , n},x∈ {rc, wc, d}:qi<xqj⇒i<j.

Proof. Let (∗) : ∀i, j ∈ {1, . . . , n},x∈ {rc, wc, d}:qi<xqj⇒i<j.

Direction “⇒”

Let ssw

≈Sseq(d) and seq(d) = hq0

1, . . . , q0

ni.

We show that (∗) holds.

•We first show the property for s=seq(d), i.e.

(∗∗) : ∀i, j ∈ {1, . . . , n}, x ∈ {rc, wc, d}:q0

i<xq0

j⇒i<j.

⇔ ∀ i, j ∈ {1, . . . , n}, x ∈ {rc, wc, d}:i≥j⇒q0

i≮xq0

Let π(q0

i)=(hLi, Ki, Rii, Ni) and π(q0

j) = (hLj, Kj, Rji, Nj).

For i=jthe condition is fulfilled directly.

Now, consider i>j.

–Case x=rc:

By definition we have that q0

i≮rc q0

j⇔Ri∩Kj⊆Ki.

We can build up the colimit of the derivation dby stepwise pushouts. Let Ti−1

be the colimit of the steps d1, . . . , di−1. Then we have that (1) : Kj⊆Ti−1. Let

ibe the colimit of the single derivation step di, and therefore, T0

iis given by

the pushout (2) of Gi←Di→Gi+1. We perform a pushout (3) of Ti−1and T0

and obtain Ti. Now consider the category Sub(Ti). We compose the pushouts

(2) and (3) with the pushout (4) : Di←Ki→Ri→Gi+1 of the derivation

step di. This is also a pullback and thus, Ri∩Ti−1∼

=Ki. Using (1) this implies

Ri∩Kj⊆Ki.

–Case x=wc:

By definition we have that q0

i≮wc q0

j⇔Ri∩Lj⊆Ki∪Kj.

Considering the construction from before, we additionally derive Lj⊆Ti−1and

thus, the equation holds.

–Case x=d:

By definition we have that q0

i≮wc q0

j⇔Ki∩Lj⊆Kj.

Considering the construction from before, we can additionally compose the

pushout (5) : Dj←Kj→Lj→Gjof the derivation step djwith the pushouts

of the stepwise construction of Ti−1and finally derive Lj∩Ti−1∼

=Kj. Further-

more, we have Ki⊆Ti−1from (1) and thus, the above equation holds.

•We now show that the condition (∗) holds for every sequence sthat is switch-

equivalent to seq(d) without considering the NACs. By (∗∗) we know that the

condition holds for seq(d). Furthermore, each sequence sis derived from seq(d)

by switchings according to sw

≈S. It remains to show that each switching preserves

the condition (∗). Now, switch equivalence of sequences sw

≈Sis based on (qi♦qj),

which is equivalent to (qi≮rc qj∧qi≮wc qj∧qi≮dqj) according to Thm. 32.2 in [4].

Thus, the condition is not affected by any switching.

Direction “⇐”:

We have to show that the condition (∗) for the sequence simplies ssw

≈Sseq(d). This is

equivalent to ¬(ssw

≈Sseq(d)) ⇒ ¬(∗). Since sis a permutation of seq(d) the condition

¬(ssw

≈Sseq(d)) means that scan be derived by switching neighbouring steps of seq(d),

where at least on switching is performed on a pair (qi;qj) of steps that is dependent, i.e.

¬(qi♦qj), which is equivalent to (qi≮xqj) for one x∈ {rc, wc, d}according to Thm.

32.2 in [4]. Thus, this pair would violate the condition (∗) in the new order. Since sis

assumed to be not switching equivalent to seq(d) based on sw

≈Sthere is at least one such

pair, where the final position of qjis in front of qiin s.

Using Lemma 1 we now prove Thm. 2.

Proof of Thm. 2. Let seq(d) = hq1, . . . , qniand s=hˆq1,...,ˆqni.

Direction “⇒”:

Assume that sis a legal sequence with respect to din Prc(d). We have to show that sis

a transition complete firing sequence of Prc(d). First of all, each transition occurs exactly

once, because sis a permutation of seq(d) in Prc(d). Consider the rule name ˆqm=tr in

s, thus the claimed firing step Ma−

−→ Mbwith tr =qa. We check the activation of tr in

Ma, i.e. Ma≥pre(tr) according to Def. 12. Now, let pre(tr) = Ppl∈PL λpl ·pl. For each

pl we have:

1. case pl =p(k):

this implies that k=aand λpl = 1. By definition this place is initially marked

with one token and there is no other transition connected to this place. Since each

transition occurs exactly once in sthis token is available in Ma.

2. case pl =p(j <xk), x ∈ {rc, wc, d}:

this implies that a=kand λpl = 1, thus tr =qkand qj<xqk. By Def. 12 we

then have post(qj)≥pl and pl is not in the pre domain of any other transition than

tr =qk. By Lemma 1 we have that qjoccurs before qkin sand thus, Ma≥pl.

3. case pl =p(j, N[i]):

By Def. 12, the marking M≥m·pl with mbeing the amount of weak disabling

causes, i.e. m=|DC|, DC ={q0

k|qj<wdn[i]qk0}.

(a) case j6=a:

By Def. 12 we have that λpl = 1, qj<wdn[i]qkand a=k. The only transition tr0

in TR \DC with pre(tr0)≥pl is qjand qjconsumes and produces one token.

Each of the transitions in DC consumes exactly one token and in sum they

consume exactly mtokens. Therefore, Ma≥pl, because qkhas not fired at this

point.

(b) case j=a:Thus, λpl = 1. By Def. 11 there is one preceding rule occurrence

qin swith q <wen[i]ˆqjor there is one subsequent rule occurrence qin swith

ˆqj<wdn[i]q. This means that for the first case Ma≥m·pl + 1 −m·pl =pl and

for the second case: Ma≥mpl −(m−1)pl =pl.

Direction “⇐”:

Assume that sis a transition complete firing sequence of Prc(d). We have to show that

sis a legal sequence with respect to din Prc(d). First of all, sis a transition complete

firing and for each transition qkthe initial marking Mcontains exactly one token for the

corresponding place p(k)∈PL and qkis consuming exactly one token from p(k). Therefore,

each rule name qkin seq(d) occurs exactly once in s. Now, we consider an arbitrary rule

name qkin seq(d). We show that the two conditions in Def. 11 hold:

•condition 1: ssw

≈Sseq(d)

By Lemma 1 this condition is equivalent to

(∗) : ∀i, j ∈ {1, . . . , n},x∈ {rc, wc, d}:qi<xqj⇒i < j. According to

Def. 12 there is exactly one place with initially no token for each pair (qi, qj) with

qi<xqj, x ∈ {rc, wc, d}. The transition qiproduces exactly one token and qjcon-

sumes exactly one token from this place and there is no other transition connected

to this place. Therefore, the condition is ensured.

•condition 2: ∀NAC sNk[i] of qk:∃e∈ {1, . . . , k −1}:qe<wen[i]qkor

∃l∈ {k, . . . , n}:qk<wdn[i]ql.

Consider a NAC N[i] of qk.

1. case qk<wdn[i]qk: Thus, we have a l=kfor the above condition.

2. case qk≮wdn[i]qk:

Thus, there is the place p(k, N[i]), such that the transition qkconsumes exactly

one token from that place. Consider the firing step Mk−

−→ Mk+1 according

to s. Since qkhas fired there was a token on p(k, N[i]) in the marking Mk.

The initial marking contains mtokens for this place, where mis the amount of

weak disabling causes, i.e. m=|DC|, DC ={qk0|qk<wdn[i]qk0, k 6=k0}. Let

EC ={qe|qe<wen[i]qk}be the set of weak enabling causes of of qkfor Nk[i].

Assume that condition 2 of Def. 11 does not hold. We then have that all qk0

in DC occur before qkin sand there is no qein EC that occurs before qkin s.

This implies that each transition of DC has consumed a token from p(k, N[i])

and none of the transitions that precede qkhave produced a token on this place.

Therefore, there is no token left on p(k, N[i]), which is a contradiction to the

firing of qkand thus, condition 2 holds.

Coming back to the original challenge of computing the set of all permutation-equivalent

derivations for a given one, we can now state by the following corollary that the analysis

can be completely performed on the process skeleton Prc(d).

Corollary 1 (Analysis of Permutation Equivalence of Derivations).Let dbe a derivation

respecting NACs of a TS with NACs over C, and let Prc(d)be its process skeleton. Then a

derivation d0is permutation equivalent to d(d0π

≈d) if and only if the sequence of names

sd0, which contains all the direct derivations of din the order they are actually fired in d0,

is a transition complete firing sequence of the marked P/T Petri net Prc(d).

Proof. This is a direct consequence of Thms. 1 and 2.

Example 4 (Process Skeleton).Consider the derivation dfrom Ex. 1 and its derived STS

in Ex. 2. The marked Petri net shown in Fig. 6 is the process skeleton Prc(d)according

to Def. 12. As expected, there is a one-to-one correspondence between its firing sequences

and the set of permutation-equivalent derivations of d. At the beginning the transitions

cont1and cont2are enabled. The firing sequences according to the derivations dand d0of

Figures 2 and 3 can be executed, and are the only firing sequences of this net.

q1=cont1q3=cont2

q2=stop1q4=stop2

p(1<wc 2)

p(3)

p(1,N[2])

p(1) p(2)

p(3<wc 4)

p(3,N[1])

p(4)

Figure 6: Process Skeleton Prc(d) as Petri net

4 On the Cost of Analysis

Besides soundness and completeness of the analysis as presented before we now focus on its

efficiency. Therefore, we extend the previous example and compare the analysis efforts of

the new technique with those of a direct analysis of the derivation. This comparison shows

a significant advantage of the technique and the effect is not limited to specific examples.

The benefit is high for transformation sequences, where many steps overlap on matches

and include dependencies because of NACs.

q1=cont1', i ∈ {0,1,2,3,4}

w1:worksOn

1:Person

4:started

1:Person

3:Task

N1[2i+1]

w(2i+1):worksOn

1:Person

3:Task

4:started

3:Task

4:started

3:Task

N1[2i+2]

w(2i+2):worksOn

2:Person

3:Task

1:Person

4:started 4:started

T ’

w1:worksOn

1:Person

3:Task

4:started

2:Person

w2:worksOn

w3:worksOn

w5:worksOn

w7:worksOn

w9:worksOn

w4:worksOn

w6:worksOn

w8:worksOn

w10:worksOn

Figure 7: Part of the Dervied Process Prc(e

Example 5 (Extended Derivation).In order to evaluate the efficiency we extend the

derivation of Ex. 1 to a derivation e

d, which specifies that the two persons are working

on the same task, but they continue and stop their work five times, i.e. e

d= (d;d;d;d;d).

The construction of Prc(e

d)leads to an STS with 20 rule occurrences. Fig. 7 shows its

super object T0and the rule occurrence “cont1’ ” for the first step of e

d. This rule occur-

rence has 10 NACs, one for each possible edge of type “worksOn” in T0. These NACs are

visualised in the figure by two NACs with a parameter iranging from zero to four. The

derivation consists of 10 blocks of the form “contx; stopx”. Each permutation-equivalent

derivation of e

dhas to preserve these blocks, otherwise a NAC would not be fulfilled or the

causality relation would be violated. Thus there are 10! = 3.628.800 permutation-equivalent

derivations.

Let us consider to perform a direct analysis based on the definition of permutation

equivalence. We call this the brute force variant, where first all switch-equivalent deriva-

tions are generated without considering the NACs, and then those which do not respect

the NACs are filtered out. This means that we only have to respect the causality between

the first and the second step of each of the 10 blocks. Therefore, we can always switch

neighbouring steps of different blocks. For each permutation-equivalent sequence we can

move the rule occurrences of the rule “stop” forward, i.e. at later positions. Therefore, we

have F= 19×17×· · ·×1 = 654.729.075 switch-equivalent sequences for each permutation

in the order of the rule occurrences “contx”, i.e. for each single permutation-equivalent

sequence. This leads to a number of 20!/210 = 2.375.880.867.360.000 ≈2,4×1015 switch

equivalent sequences.

Fig. 8 shows how the different amounts of equivalent sequences develop for 2 up to 10

blocks of “continue;stop” steps. Since the complexity of a function, which is dominated by

a factorial expression, is super-exponential, the calculation of invalid sequences should be

avoided in general. In Fig. 9 we present the reachability graph of the dependency net for an

analogous transformation sequence with 10 steps, i.e. 5 “continue;stop” blocks. The graph

was generated using our implementation based on Mathematica. As presented before, the

reachability graph for the complete sequence contains 10! = 3.628.800 leaf nodes and would

be far to big for normal paper dimensions. The figure already shows the symmetric nature

2.375.880.850

2.375.880.860

Switch Equivalence

without NACs

Permutation

Equivalence

3,6

2.375.880.867,4

Amount of Equivalent Sequences for 20 Steps

In Millions

Amount of Equivalent Sequences

Logarithmic Scale

1,0E+00

1,0E+02

1,0E+04

1,0E+06

1,0E+08

1,0E+10

1,0E+12

1,0E+14

1,0E+16

4 6 8 10 12 14 16 18 20

Transformation Steps

Equivalent Sequences

Switch Equivalence

without NACs

Permutation

Equivalence

Figure 8: Comparison of the Amount of Equivalent Sequences

of the specific example and future work will encompass symmetry reduction techniques,

such that the size can be reduced for examples with symmetry.

Start

Amount of

permutation-

equivalent sequences:

5! = 120 permutations

Derivation with 10 Steps

Figure 9: Reachability Graph of the Dependency Net for 10 Steps

Obviously, the generation of the permutation-equivalent sequences involves several

computation steps. But let us compare the effort of generating the set of permutation-

equivalent derivations using the process skeleton Prc(d) with the effort of a brute force

generation directly based on Def. 4. The result is that a lower bound for the effort of the

brute force variant is 8 orders of magnitude higher than an upper bound for the analysis

based on the process skeleton.

Example 6 (Analysis Efforts).Based on the process skeleton Prc(e

d)we can construct

the reachability graph RG(Prc(e

d)) for this marked Petri net with 20 transitions and 120

places. Each path in this graph specifies a permutation equivalent derivation. An upper

bound for the effort eff of constructing RG(Prc(e

d)) is given by: eff ≤651.030.320 <

9·n, where nis n= 20 ·10! = 72.576.000, which is the number of derivation steps in

the set of all permutation-equivalent derivations. Considering the brute force variant we

will construct F= 654.729.075 times as many derivations as the number of permutation-

equivalent derivations. Thus, the lower bound for the brute force effort EFF is given by

F·n≤EFF. In comparison we have:

eff <1,4×10−8EFF.

Details for the Efficiency Results

•Size of the Petri net Prc(e

d)=(PN , M),PN = (PL,TR,pre,post):

|TR|= 20

|PL|= 20 + 10 + 10 ·9 = 120

Amount of arcs = 20 + 2 ·10 + (1 + 2 + 1) ·10 ·9 = 400

Amount of all elements: 540

•Size of RG(Prc(e

d)) = (V, E, s, t):

Branching number for the successors: root node: 10 (for each “contx”), then 1

(“stopx”), then 9 , . . . , then 1, then 1

|V|= 1 + 2 ·(Pi=0..10 10!/(10 −i)!) = 19.728.201

|E|=|V| − 1 = 19.728.200

•Effort for calculating RG(Prc(e

d)):

Store the transitions that have fired, since the maximum of one time firing is ensured

by definition

At each node: check each transition that has not fired for activation, i.e. for the

“contx” transitions 1 + 9 =10 pre arcs and for the “stopx” transitions 1+1 pre arcs.

If one place in the pre domain is found empty, the remaining ones do not have to

be checked. Then, continue and update the marking (1+9+1=11 for “contx” and

1+1+9=11 for “stopx”).

Effort eff measured in binary operations: eff ≤651.030.320 <33 · |V|<9·n

Of course, the effort for constructing the Petri net has also to be taken into account,

but it does not change the result. In general, the construction of the process Prc(d) with

its relations is shown to be of polynomial time complexity with respect to the length of

the derivation d[9]. Furthermore, the construction of the process skeleton is linear with

respect to Prc(d) with its dependency relations and in this this example there are only 120

places in the constructed Petri net. Note that still all steps in e

dare sequentially dependent

with the NACs and therefore, no direct switching is possible.

5 Conclusion

In the framework of adhesive high-level replacement (HLR) systems there are many in-

stantiations, such as graph transformation systems scaling up to typed attributed graph

transformation systems with node type inheritance, and Petri net transformation system -

in particular for the modelling of workflows of reconfigurable mobile adhoc networks. Each

of them has its specific features, which support the modelling of systems in the concrete

application domain. Negative Application Conditions (NACs) are an important control

structure for these techniques and they are widely used for applications. However, the

analysis of processes of such systems, i.e. the study of equivalence of derivations in the

presence of NACs, was introduced only recently in [9].

While switch-equivalence [2] for systems without NACs leads to the complete set of

equivalent derivations, this is not the case in the presence of NACs if the notion of equiv-

alence proposed in [8, 14] is considered. Similarly, the notion of shift equivalence [16, 12]

for derivations cannot be extended appropriately to the case with NACs, because it is also

based on sequential independence of neighbouring steps. The problem is that rule appli-

cations may be possible in an equivalent way at several positions of the derivation, which

are not situated next to each other, as shown with the presented example.

In order to provide a sound, complete and efficient analysis technique for permuta-

tion equivalence we have shown how the generated process given by an STS [4, 9] can

be transformed to a process skeleton given by a marked P/T Petri net. The construc-

tion is shown to be sound and complete with respect to the computation of the set of

permutation-equivalent derivations to a given one. Furthermore, the constructed Petri net

shows significant advantages with respect to efficiency. While the example in this paper

was kept compact, the overall approach can be applied to adhesive HLR systems in general,

if suitable side conditions are fulfilled [10].

The efficiency of the approach is based on two advantages. First of all, the constructed

Petri net only specifies the dependencies among the steps of the derivation, ignoring the

concrete structure of the involved objects: This advantage is independent of the presence

of NACs. The second advantage is that NACs are respected during the generation of the

permutation-equivalent sequences. Thus, the number of generated sequences during the

analysis is reduced significantly if NACs are involved, as shown by the presented example.

The construction of the Petri net can be performed in polynomial time with respect to the

size of the initial derivation [9], and thus it does not affect the efficiency of the analysis.

Some of the problems addressed in this paper are similar to those considered in the

process semantics [11] and unfolding [1, 3] of Petri nets with inhibitor arcs, and actually

we could have used some sort of inhibitor arcs to model the inhibiting effect of NACs in the

process skeleton of a derivation. However, we would have needed some kind of “generalised”

inhibitor nets, where a transition is connected to several (inhibiting) places and can fire if

at least one of them is unmarked. To avoid the burden of introducing yet another model of

nets, we preferred to stick to a direct encoding of the process of a derivation into a standard

marked P/T nets, leaving as a topic for future research the possible use of different models

of nets for our process skeletons.

Future work will also include the study of non-deterministic processes of transformation

systems with NACs, which will be based on incomplete firings of the constructed P/T Petri

net and suitable side conditions. Further improvements of efficiency could be obtained by

observing the occurring symmetries in the P/T Petri net, and applying symmetry reduction

techniques on it. Additionally, the space complexity of the analysis could be reduced by

unfolding the net and then representing all permutation-equivalent derivations in a more

compact, partially ordered structure. An implementation of the analysis is planned and

will be based on a recently developed graph transformation engine in Mathematica.

References

[1] P. Baldan. Modelling Concurrent Computations: from Contextual Petri Nets to Graph

Grammars. PhD thesis, Dipartimento di Informatica, Universit`a di Pisa, 2000. Avail-

able as technical report n. TD-1/00.

[2] P. Baldan, A. Corradini, T. Heindel, B. K¨onig, and P. Sobocinski. Processes for

Adhesive Rewriting Systems. In FoSSaCS’06, volume 3921 of LNCS, pages 202–216.

Springer, 2006.

[3] P. Baldan, B. K¨onig, and I. St¨urmer. Generating Test Cases for Code Generators

by Unfolding Graph Transformation Systems. In Proc. of ICGT ’04, volume 3256 of

LNCS, pages 194–209. Springer, 2004.

[4] A. Corradini, F. Hermann, and P. Soboci´nski. Subobject Transformation Systems.

Applied Categorical Structures, 16(3):389–419, June 2008.

[5] A. Corradini, U. Montanari, and F. Rossi. Graph processes. Fundamenta Informaticae,

26:241–265, 1996.

[6] H. Ehrig, K. Ehrig, U. Prange, and G. Taentzer. Fundamentals of Algebraic Graph

Transformation. EATCS Monographs in Theoretical Computer Science. Springer,

2006.

[7] H. Ehrig, M. Pfender, and H. Schneider. Graph-grammars: an algebraic approach.

In R. Book, editor, Switching and Automata Theory, pages 167–180. IEEE Computer

Society Press, 1973.

[8] A. Habel, R. Heckel, and G. Taentzer. Graph Grammars with Negative Application

Conditions. Special issue of Fundamenta Informaticae, 26(3,4):287–313, 1996.

[9] F. Hermann. Permutation Equivalence of DPO Derivations with Negative Application

Conditions based on Subobject Transformation Systems. Electronic Communications

of the EASST, 16, 2009.

[10] F. Hermann and H. Ehrig. Process Definition using Subobject Transformation Sys-

tems. EATCS Bulletin, 95:153–163, 2008.

[11] H. C. M. Kleijn and M. Koutny. Process semantics of general inhibitor nets. Infor-

mation and Computation, 190(1):18–69, 2004.

[12] H.-J. Kreowski. Is parallelism already concurrency? Part 1: Derivations in graph

grammars. In Graph-Grammars and Their Application to Computer Science, volume

291 of LNCS, pages 343–360. Springer, 1986.

[13] S. Lack and P. Soboci´nski. Adhesive and quasiadhesive categories. Theoretical Infor-

matics and Applications, 39(2):511–546, 2005.

[14] L. Lambers, H. Ehrig, and F. Orejas. Conflict Detection for Graph Transformation

with Negative Application Conditions. In ICGT’06, volume 4178 of LNCS, pages

61–76. Springer, 2006.

[15] W. Reisig. Petri Nets: An Introduction. EACTS Monographs on Theoretical Com-

puter Science. Springer Verlag, 1985.

[16] G. Rozenberg, editor. Handbook of Graph Grammars and Computing by Graph Trans-

formations, Volume 1: Foundations. World Scientific, 1997.