Forschungsberichte
der Fakultät IV – Elektrotechnik und Informatik
Modelling Evolution of Communication
Platforms and Scenarios based on
Transformations of High-Level Nets and
Processes
(Extended Version)
Karsten Gabriel
Bericht-Nr. 2011 – 08
ISSN 1436-9915
Modelling Evolution
of Communication Platforms
and Scenarios based on
Transformations of
High-Level Nets and Processes
Extended Version
Karsten Gabriel
Institut f¨ur Softwaretechnik und Theoretische Informatik
Technische Universit¨at Berlin, Germany
[email protected]erlin.de
Bericht-Nr. 2011/08
ISSN 1436-9915
Modelling Evolution of Communication Platforms and Scenarios
based on Transformations of High-Level Nets and Processes
Extended Version
Karsten Gabriel
Integrated Graduate Program IGP H-C3, Technische Universit¨at Berlin, Germany
Abstract
Algebraic High-Level (AHL) nets are a well-known modelling technique based on Petri nets
with algebraic data types, which allows to model the communication structure and the data flow
within one modelling framework. Transformations of AHL-nets – inspired by the theory of graph
transformations – allow in addition to modify the communication structure. Moreover, high-level
processes of AHL-nets capture the concurrent semantics of AHL-nets in an adequate way. Altogether
we obtain a powerful integrated formal specification technique to model and analyse all kinds of
communication based systems, especially different kinds of communication platforms.
In this paper we show how to model the evolution of communication platforms and scenarios
based on transformations of Algebraic High-Level Nets and Processes. All constructions and results
are illustrated by a running example showing the evolution of Apache Wave platforms and scenarios.
The evolution of platforms is modelled by the transformation of AHL-nets and that of scenarios
by the transformation of AHL-net processes. The first main result shows under which conditions
AHL-net processes can be extended if the corresponding AHL-net is transformed. This result can
be applied to show the extension of scenarios for a given platform evolution. The second main result
shows how AHL-net processes can be transformed based on a special kind of transformation for
AHL-nets, corresponding to action evolution of platforms. Finally, we briefly discuss the case of
multiple action evolutions.
1 Introduction
High-level nets based on low-level Petri nets [Pet62, Roz87, Rei85] and data types in ML have been
studied as coloured Petri nets by Jensen [Jen91] and – using algebraic data types – as algebraic high-
level (AHL) nets in [Rei90, PER95, ER97].
Inspired by the theory of graph transformations [Ehr79, Roz97] transformations of AHL-nets were
first studied in [PER95] which – in addition to the token game – also allow to modify the net structure
by rule based transformations.
The concept of processes in Petri nets is essential to model not only sequential, but especially con-
current firing behaviour. A process of a low-level Petri net Nis given by an occurrence net Ktogether
with a net morphism p:K→N. Processes of high-level nets AN are often defined as processes
p:K→Flat(AN) of the corresponding low-level net Flat(AN), called flattening of AN. However,
this is not really adequate, because the flattening is in general an infinite net and the data type struc-
ture is lost. For this reason high-level processes for algebraic high-level nets have been introduced in
[EHP+02, Ehr05], which are high-level net morphisms p:K→AN based on a suitable concept of
high-level occurrence nets K.
The main aim of this paper is to give a comprehensive introduction to the integrated framework of
transformations of algebraic high-level nets and processes and to show how this can be applied to modern
communication platforms.
In previous papers it was shown already how to use this framework to model communication platforms
like Skype [HM10] and Google Wave [EG11]. In this paper we show how our integrated framework can
2 Evolution of Apache Wave Platforms and Scenarios
be used to model basic aspects of Apache Wave [Apa11b]. In Section 2 we introduce a small example of
an Apache Wave platform, which is also used as running example for the following sections.
In Section 3 we introduce AHL-nets together with high-level processes in the sense of [Ehr05]. Rule
based transformations in analogy to graph transformation systems [Roz97] are introduced in Section 4
for AHL-nets and AHL-processes and applied to the evolution of Apache Wave communication platforms
and waves. The first main result presented in Section 5 shows under which condition an AHL-process
can be extended if the corresponding AHL-net is transformed. This result can be applied to show the
extension of scenarios for a given platform evolution. The second main result presented in Section 6
shows how AHL-net processes can be transformed based on a special kind of transformation for AHL-
nets, corresponding to action evolution of platforms. Moreover, we briefly discuss the case of multiple
action evolutions.
Finally, the conclusion in Section 7 includes a summary of the paper.
2 Evolution of Apache Wave Platforms and Scenarios
In this section we introduce our main case study Apache Wave which is a communication platform that
was originally developed by the company Google [Goo11] as Google Wave. Google itself has stopped
the development of Google Wave, but the development is continued by the Apache Software Foundation
[Apa11a] as Apache Wave [Apa11b].
One of the most interesting aspects of Apache Wave is the possibility to make changes on previous
conributions. Therefore, in contrast to email, text chat or forums, due to possible changes the resulting
data of the communication does not necessarily give a comprehensive overview on all interactions of the
communication. For this reason, in Apache Wave for every communication there is a history allowing
the users to replay interactions of the communication step by step. So for the modelling of Apache Wave
it is necessary that we do not only model the systems and the communication but also the history of the
communication.
We have chosen Apache Wave as running example for this paper because it includes typical modern
features of many other communication systems, such as near-real-time communication. This means that
different users can simultaneously edit the same document, and changes of one user can be seen almost
immediately by the other users.
Note that we do not focus on the communication between servers and clients in this contribution but
on the communication between users. For details on the modeling of the more technical aspects of the
server-to-server and client-to-server communication we refer to [Yon10].
In Apache Wave users can communicate and collaborate via so-called waves. A wave is like a document
which can contain diverse types of data that can be edited by different invited users. The changes that
are made to a wave can be simultaneously recognized by the other participating users. In order to keep
track of the changes that have been made, every wave contains also a history of all the actions in that
wave.
Apache Wave supports different types of extensions which are divided into gadgets and robots. The
extensions are programs that can be used inside of a wave. The difference between gadgets and robots
is that gadgets are not able to interact with their environment while robots can be seen as automated
users that can independently create, read or change waves, invite users or other robots, and so on. This
allows robots for example to do real-time translation or highlighting of texts that are written by different
users of a wave. Clearly, it is intended to use different robots for different tasks and it is desired that
multiple robots interact without conflicts. This makes the modeling and analysis of Apache Wave very
important in order to predict possible conflicts or other undesired behavior of robots.
In [EG11] we have already shown that Google Wave (and thus also Apache Wave) can be adequately
modelled using algebraic high-level (AHL) nets, which is an integration of the modeling technique of
low-level Petri nets [Pet62, Roz87, Rei85] and algebraic data types [EM85].
Figure 1 shows a small example of the structure of an AHL-net Platform which has 3 places and 3
transitions with firing conditions, where the pre and post arcs are labelled with variables of an algebraic
signature. The AHL-net Platform models an Apache Wave platform with some basic features like the
creation of new waves, modifications to existing waves, and the invitation of users to a wave which are
modeled by the transitions new wavelet,modify text and invite user.
A wavelet is a part of a wave that contains a user ID, a list of XML documents and a set of users
2
w : wavelet
u : user
new wavelet
n = new(user,free)
next = next(free)
modify text
invited(o,user) = true
txt: text
rng: range
r = remText(o,rng)
n = insText(r,txt,start(rng))
id : nat
invite user
invited(o, user1) = true
n = addUser(o,user2)
user
user
user
user
user1 7 user2
user1 7 user2
n
n
o
o
n
free
next
Platform
Figure 1: AHL-net Platform for an Apache Wave platform
which are invited to modify the wavelet. For simplicity we model in our example only the simple case
that every wavelet contains only one single document and the documents contain only plain text. In
order to obtain a more realistic model one has to extend the used algebraic data part of the model given
by the signature Σ-Wave shown in Table 1 and the Σ-Wave-algebra Ain Table 2 in Section 3.
The transitions of the net contain firing conditions in the form of equations over the signature Σ-
Wave. In order to fire a transition there has to be an assignment vof the variables in the environment
of the transition such that the firing conditions are satisfied in the algebra A. The pair (t, v) is then
called a consistent transition assignment. Moreover, there have to be suitable data elements in the pre
domain of the transition. For example, in order to fire the transition modify text we need a wavelet on
the place wand a user on the place uthat can be assigned by the variables orespectively user such that
the user is invited to the selected wavelet. Furthermore, we need a text txt, a pair of natural numbers
rng and a new wavelet nsuch that nis the wavelet which is obtained by deleting all text in the range
specified by rng and by inserting the text txt on the starting position of rng into the original wavelet o.
The assignment vthen determines a follower marking which is computed by removing the assigned
data tokens in the pre domain of the transition and adding the assigned data tokens in the post domain.
In the case of the transition modify text this means that we remove the old wavelet from the place w
and replace it by a new wavelet which contains the modified text. For more details on the operational
semantics of AHL-nets we refer to [Ehr05].
As we have shown in [EG11] a suitable modelling technique for waves together with their histories are
AHL-processes with instantiations. Fig. 2 shows an example of an AHL-process Wave which abstractly
models a wave that contains two wavelets created by possibly different users.
Another interesting aspect of the modelling of Apache Wave are dynamic changes to the structure of
the platform. Using rule-based transformation of AHL-nets [PER95] in the sense of graph transformation
[Roz97], we can delete and add features, leading to a new platform. Figure 3 shows a net Platform0which
is an adaption of our example Platform where the modify text transition has been replaced. In the new
version we have a new transition modify and log which for every modification to a wave creates a log
entry with information about the user, the position and the text of the modification.
Since it is possible that the communication platform is modified at runtime there may already exist
some waves that correspond to the old version of the platform. In some cases that correspondence could
be violated by the modification of the platform.
An intuitive solution is to apply the modification of the platform also to the wave, replacing all
occurrences of the old feature with the new one. This leads to a new wave model Wave0depicted in
Fig. 4. The three transitions have been replaced by transitions that have the same firing conditions as
the transition modify and log and there are new log places in the post domain of the new transitions. In
Sections 5 and 6 we present general constructions to obtain a new correspondence between an existing
wave and a modified platform based on platform evolution under certain conditions.
3
2 Evolution of Apache Wave Platforms and Scenarios
modify2
: modify text
invite1
: invite user
new1
: new wavelet
modify1
: modify text
u1 : u
id1 : id
user
free
next
u2 : u
w1 : w
n
user user
o
u3 : u
w2 : w
user
n
u4 : u
user2
user1
o
u6 : uu5 : u
w3 : w
user2
user1
n
user
o
w4 : w
n
user
new2
: new wavelet
free
id3 : id
next
u8 : u
user
user
modify3
: modify text
user
u9 : u
w5 : w
n o
user
w6 : w
n
id2 : id
u7 : u
Wave
Figure 2: AHL-process W ave of a wave
w : wavelet
u : user
new wavelet
n = new(user,free)
next = next(free)
modify and log
invited(o,user) = true
txt: text
rng: range
r = remText(o,rng)
n = insText(r,txt,start(rng))
log = logEntry(user, rng, txt)
id : nat
invite user
invited(o, user1) = true
n = addUser(o,user2)
user
user
user
user
user1 7 user2
user1 7 user2
n
n
o
o
n
free
next
Platform'
log : mod
log
Figure 3: Modified AHL-net Platform0
modify'2
: modify and log
invite1
: invite user
new1
: new wavelet
modify'1
: modify and log
u1 : u
id1 : id
user
free
next
u2 : u
w1 : w
n
user user
o
u3 : u
w2 : w
user
n
u4 : u
user2
user1
o
u6 : uu5 : u
w3 : w
user2
user1
n
user
o
w4 : w
n
user
new2
: new wavelet
free
id3 : id
next
u8 : u
user
user
modify'3
: modify and log
user
u9 : u
w5 : w
n o
user
w6 : w
n
id2 : id
u7 : u
Wave'
l2 : log
log
l1 : log
log
log
l3 : log
Figure 4: Modified AHL-process Wave0
4
3 Modelling of Communication Platforms and Scenarios with
AHL-Nets and Processes
In the following we review the definition of AHL-nets and their processes from [Ehr05, EHP+02] based
on low-level nets in the sense of [MM90], where X⊕is the free commutative monoid over the set X.
Note that s∈X⊕is a formal sum s=Pn
i=1 λixiwith λi∈Nand xi∈Xmeaning that we have λi
copies of xiin sand for s0=Pn
i=1 λ0
ixiwe have s⊕s0=Pn
i=1 (λi+λ0
i)xi.
Definition 1 (Algebraic High-Level Net).An algebraic high-level (AHL-) net
AN = (Σ, P, T, pre, post, cond, type, A)
consists of
•a signature Σ = (S, OP;X) with additional variables X;
•a set of places Pand a set of transitions T;
•pre- and post domain functions pre, post :T→(TΣ(X)⊗P)⊕;
•firing conditions cond :T→ Pfin(Eqns(Σ; X));
•a type of places type :P→Sand
•a Σ-algebra A
where the signature Σ = (S, OP) consists of sorts Sand operation symbols OP,TΣ(X) is the set of
terms with variables over X,
(TΣ(X)⊗P) = {(term, p)|term ∈TΣ(X)type(p), p ∈P}
and Eqns(Σ; X) are all equations over the signature Σ with variables X.
An AHL-net morphism f:AN1→AN2is given by f= (fP, fT) with functions
fP:P1→P2and fT:T1→T2satisfying
(1) (id ⊗fP)⊕◦pre1=pre2◦fTand (id ⊗fP)⊕◦post1=post2◦fT,
(2) cond2◦fT=cond1and
(3) type2◦fP=type1.
The category defined by AHL-nets (with signature Σ and algebra A) and AHL-net morphisms is
denoted by AHLNets where the composition of AHL-net morphisms is defined componentwise for
places and transitions.
Note that it is also possible to define a category of AHL-nets with different signatures and algebras
which requires that the morphisms not only contain functions for places and transitions but also a
signature morphism together with a generalized algebra morphism (for details see [PER95]).
The firing behaviour of AHL-nets is defined analogously to the firing behaviour of low-level nets.
The difference is that in the high-level case all tokens are equipped with data values. Moreover, for the
activation of a transition t, we additionally need an assignment asg of the variables in the environment
of the transition, such that the assigned pre domain is part of the given marking and the firing conditions
of the transition are satisfied. This assignment is then used to compute the follower marking, obtained
by firing of transition twith assignment asg.
Definition 2 (Marking, Firing Behaviour).A marking M=Pn
i=1 λi(ai, pi)∈(A⊗P)⊕of an AHL-net
AN means that place picontains λi∈Ndata tokens ai∈Atype(pi).
Given an AHL-net AN with marking Ma transition t∈Tis enabled under Mand an assignment
asg :V ar(t)→A, if all firing conditions cond(t) are satisfied in Afor asg and we have enough token in
the pre domain of t, i.e. preA(t, asg)≤M, where
preA(t, asg) =
n
X
i=1
(asg(termi), pi) for pre(t) =
n
X
i=1
(termi, pi)
5
3 Modelling of Communication Platforms and Scenarios with AHL-Nets and Processes
with termi∈TOP (X) and asg(termi) is the evaluation of termiunder asg. In this case the follower
marking M0is given by
M0=MpreA(t, asg)⊕postA(t, asg).
Remark 1 (AHL-Nets with Individual Tokens).In contrast to the firing behaviour defined in Def. 2 it
is also possible to define a marking over a set Iof individuals and a marking function m:I→A⊗P
assigning each individual to a pair of a data element and a place. This makes it possible to distinguish
the single tokens of a marking.
In order to fire a transition under a given marking it is then necessary to specify a token selection
(M, m, N, n) where M⊆Iis the set of individuals which are consumed by the transition, Nis a set of
newly created individuals with (I\M)∩N=∅and m:M→A⊗P,n:N→A⊗Pare corresponding
marking functions. If a selection together with a consistent transition assignment (t, asg) meets the
token selection condition:
X
i∈M
m(i) = preA(t, asg) and X
i∈N
n(i) = postA(t, asg)
then tis asg-enabled and the follower marking (I0, m0) can be computed by
I0= (I\M)∪N, m0:I0→A⊗Pwith m0(x) = (m(x), if x∈I\M;
n(x), if x∈N.
Although this individual token approach is more complicated than the collective token approach in Def. 2
it has some benefits like the possibity to formulate transformation rules which can not only change the
net structure but also the marking of an AHL-net. For more details we refer to [MGE+10]. In this
paper we still use the collective approach but we will also research processes of AHL-nets with individual
tokens in the future.
Example 1 (Apache Wave Platform).The model of an Apache Wave platform in Fig. 1 is an AHL-net
Platform = (Σ-Wave, P, T, pre, post, cond, type, A)
where the signature Σ-Wave is shown in Table 1 and the Σ-W ave-algebra Ais shown in Table 2. This
signature and algebra is also used for all the following examples.
Let us consider the marking
M= (Alice, u)⊕(Bob, u)⊕(1,id)⊕((0,{Alice,Bob}, ), w)
of the AHL-net platform in Fig. 1 which means that we have two users Alice and Bob on the place u, a
free ID 1 and an empty wavelet with ID 0 on place wwhere Alice and Bob are invited. An assignment
asg :{user, txt, rng, o, n} → Awith asg(user) = Alice,asg(txt) = Hello Bob,asg(rng) = (0,0),
asg(o) = (0,{Alice,Bob}, ) and asg(n) = (0,{Alice,Bob},Hello Bob) satisfies the firing conditions of
the transition modify text. By firing the transition modify text with assignment asg we obtain the
follower marking
M0= (Alice, u)⊕(Bob, u)⊕,(1,id)⊕((0,{Alice,Bob},Hello Bob), w)
where the assigned text Hello Bob has been inserted at position 0 into the assigned wavelet.
Remark 2 (Morphisms Preserve Firing Behaviour).Given an AHL-net morphism f:AN1→AN2the
firing behaviour is preserved, i.e. for M0
1=M1pre1,A(t, asg)⊕post1,A(t, asg) in AN1we have M0
2=
M2pre2,A(fT(t), asg)⊕post2,A(fT(t), asg) in AN2with M2=Pn
i=1 (ai, fP(pi)) for M1=Pn
i=1(ai, pi)
and similar M0
2constructed from M0
1.
Now, we introduce AHL-process nets based on low-level occurrence nets (see [GR83]) and AHL-
processes according to [Ehr05, EHP+02]. The net structure of a high-level occurrence net has similar
properties like a low-level occurrence net, but it captures a set of different concurrent computations due
to different initial markings. In fact, high-level occurrence nets can be considered to have a set of initial
6
Table 1: Signature Σ-Wave
sorts: bool, nat, mod, range, text, user, wavelet
opns: true, false : →bool next : nat →nat
start, end : range →nat new : user nat →wavelet
addUser : user wavelet →wavelet invited : wavelet user →bool
len : text →nat sub : text range →text
insText : wavelet text nat →wavelet remText : wavelet range →wavelet
logEntry : user range text →mod
vars: free, next : nat log : mod
rng : range txt : text
user, user1, user2: user o, n, r : wavelet
Table 2: Σ-Wave-algebra A
Abool ={T, F}Anat =N
Auser ={a, . . . , z, A, . . . , Z}∗Atext ={a, . . . , z, A, . . . , Z, . . . }∗
Awavelet =Anat × P(Auser)×Atext Arange =Anat ×Anat
Amod =Auser ×Arange ×Atext
trueA=T∈Abool
falseA=F∈Abool
startA:Arange →Anat
(s, e)7→ s
endA:Arange →Anat
(s, e)7→ e
nextA:Anat →Anat
n7→ n+ 1
newA:Auser ×Anat →Awavelet
(u, id)7→ (id, {u}, )
addUserA:Auser ×Awavelet →Awavelet
(u, (id, uset, t)7→ (id, uset ∪ {u}, t)
invitedA:Awavelet ×Auser →Abool
(u, (id, uset, t)) 7→ (T, if u∈uset;
F, else.
lenA:Atext →Anat
t7→ (0 , if t=;
1 + lenA(t1. . . tn) , if t=t0. . . tn.
subA:Atext ×Arange →Atext
(t, (s, e)) 7→ (, if e<sor lenA(t)≤s;
ts. . . tn, if t=t0. . . tm, s ≤e, s < m and n=min(m, e).
insTextA:Awavelet ×Atext ×Anat →Awavelet
((id, uset, t), nt, pos)7→ (id, uset, subA(t, (0, pos −1)).nt.subA(t, (pos, lenA(t))))
remTextA:Awavelet ×Arange →Awavelet
((id, uset, t),(s, e)) 7→ (id, uset, subA(t, (0, s)).subA(t, (e, lenA(t))))
logEntryA:Auser ×Arange ×Atext →Amod
(u, r, t)7→ (u, r, t)
7
3 Modelling of Communication Platforms and Scenarios with AHL-Nets and Processes
markings for the input places, whereas there is only one implicit initial marking of the input places for
low-level occurrence nets.
Moreover, in a low-level occurrence net with an initial marking there is for any complete order of
transitions compatible with the causal relation a corresponding firing sequence once there is a token
on all input places. This is a consequence of the fact that in an occurrence net the cuasal relation is
finitary. In the case of high-level occurrence nets an initial marking additionally contains data values
and in general some of the firing conditions in a complete order of transitions are not satisfied. Hence,
even in the case that the causal relation is finitary, we cannot expect to have complete firing sequences.
In order to ensure a complete firing sequence in a high-level occurrence net there has to be an
“instantiation” of the occurrence net (see [Ehr05]). Instantiations, however, are not considered explicitely
in this paper. In the following definition of AHL-process nets, in contrast to occurrence nets, we omit
the requirement that the causal relation has to be finitary, because this is not a meaningful requirement
for our application domain.
Definition 3 (Algebraic High-Level Process Net).An AHL-process net Kis an AHL -net
K= (Σ, P, T, pre, post, cond, type, A)
such that for all t∈Twith pre(t) = Pn
i=1(termi, pi) and notation •t={p1, . . . , pn}and similarly t•we
have
1. (Unarity): •t, t•are sets rather than multisets for all t∈T, i.e. for •tthe places p1. . . pnare
pairwise distinct. Hence | • t|=nand the arc from pito thas a unary arc-inscription termi.
2. (No Forward Conflicts): •t∩ •t0=∅for all t, t0∈T, t 6=t0
3. (No Backward Conflicts): t• ∩t0•=∅for all t, t0∈T, t 6=t0
4. (Partial Order): the causal relation <K⊆(P×T)∪(T×P) defined by the transitive closure of
{(p, t)∈P×T|p∈ •t} ∪ {(t, p)∈T×P|p∈t•} is a strict partial order, i. e. the partial order is
irreflexive.
AHL-process nets (with signature Σ and algebra A) together with AHL-net morphisms between AHL-
process nets form the full subcategory AHLPNets ⊆AHLNets.
Note that an AHL-process net with a finitary causal relation is an AHL-occurrence net as defined in
[Ehr05].
We define the sets of input and output places of an AHL-process nets as the sets of places which are
not in the post respectively pre domain of a transition:
Definition 4 (Input and Output Places).Given an AHL-process net K. We define the set IN(K) of
input places of Kas
IN(K) = {p∈PK|@t∈TK:p∈t•}
and similar the set OUT(K) of output places of Kas
OUT(K) = {p∈PK|@t∈TK:p∈ •t}
Note that the properties of AHL-process nets are reflected by AHL-morphisms which is stated in the
following lemma.
Lemma 1 (AHL-Morphisms Reflect AHL-Process Nets).Given an AHL-morphism f:K1→K2. If
K2is an AHL-process net then also K1.
Proof Idea. The unarity of K2together with the fact that AHL-morphisms preserve pre and post con-
ditions imply that all non-injectively matched parts have equal structures. Thus, K1basically has the
same structural properties as K1which means that it does also satisfy the structural conditions to be
an AHL-process net. For a detailed proof see Appendix A.1.
8
An AHL-process of an AHL-net AN is defined as an AHL-morphism from an AHL-process net Kinto
the net AN. Note that from the preservation of firing behaviour by AHL-morphisms (see Remark 2) it
follows that a firing sequence in Kcorresponds to a firing sequence in AN. Thus, due to the conflict-free
and acyclic structure of AHL-process nets, an AHL-process mp of an AHL-net AN models a part of the
semantics of AN which – up to concurrency and possibly different data values – does not contain any
branches or iterations.
Definition 5 (AHL-Process).An AHL-process of an AHL-net AN is an AHL-net morphism mp :K→
AN where Kis an AHL-process net.
The category Proc(AN) of AHL-processes of an AHL-net AN is defined as the full subcategory
of the slice category AHLNets \AN such that the objects are AHL-processes. This means that the
objects of Proc(AN) are AHL-process morphisms mp :K→AN and the morphisms of the category
are AHL-net morphisms f:K1→K2such that diagram (1) below commutes.
The category AHLProcs of all AHL-processes is defined as full subcategory of the arrow category
AHLNets→such that the objects are AHL-processes, and the morphisms are pairs (f∗, f) of AHL-
process net morphisms and AHL-morphisms such that diagram (2) below commutes.
K1
f//
mp1""
E
E
E
E
EK2
mp2
||y
y
y
y
y
AN
(1)
K1
f∗
//
mp1
K2
mp2
AN1f//
(2)
AN2
Example 2 (Scenario).Figure 2 shows an AHL-process wave :Wave →Platform where the mappings
of the process are indicated with colons, e. g. u1:umeans that the place u1in the AHL-process net
Wave is mapped to the place uin the AHL-net Platform in Figure 1. The AHL-process describes an
abstract scenario in the Apache Wave platform in which two wavelets are created with consecutive IDs
by possibly two different users. Moreover, the creator of the first wavelet does a modification to the
wavelet, and it is open if this happens before or after the creation of the second wavelet. After that the
creator of the second wavelet is invited to the first one, and does modifications to the first and then to
the second wavelet.
4 Evolution of Communication Platforms and Transformation
of Scenario Nets
Due to the possibility to evolve the Apache Wave platforms by adding, removing or changing features
we need also techniques that make it possible to evolve the corresponding model of a platform. For this
reason we introduce rule-based AHL-net transformations [PER95] in the sense of graph transformations
[Roz97].
A production (or transformation rule) for AHL-nets specifies a local modification of an AHL-net. It
consists of a left-hand side, an interface which is the part of the left-hand side which is not deleted and
a right-hand side which additionally contains newly created net parts.
Definition 6 (Productions for AHL-Nets).Aproduction for AHL-nets is a span %:Ll
←Ir
→Rof
injective AHL-morphisms. We call Lthe left-hand side, Ithe interface, and Rthe right-hand side of the
production %. In most examples land rare inclusions.
L I
l
oor//R
Example 3 (Production for Platform Evolution).Figure 5 shows a production insertLog for AHL-nets
that can be used for the evolution of an Apache Wave platform. The production describes a local
modification that removes a transition modify text and inserts a new transition modify and log and a
new place log. Moreover, the newly created transition is connected to the former environment of the
removed transition.
In order to add the new parts as specified in the right-hand side of a production to an AHL-net we
define a gluing construction based on the gluing of its place and transition components in the category
of Sets in the following sense.
9
4 Evolution of Communication Platforms and Transformation of Scenario Nets
w1 : wavelet
u1 : user
modify and log
invited(o,user) = true
txt: text
rng: range
r = remText(o,rng)
n = insText(r,txt,start(rng))
log = logEntry(user, rng, txt)
user o
log : mod
log
w2 : waveletu2 : user
user n
w1 : waveletu1 : user
w2 : waveletu2 : user
w1 : wavelet
u1 : user
modify text
invited(o,user) = true
txt: text
rng: range
r = remText(o,rng)
n = insText(r,txt,start(rng))
user o
w2 : waveletu2 : user
user n
l r
LIR
Figure 5: AHL-net production insertLog for the evolution of platforms
Definition 7 (Gluing of Sets).Given sets A, B and C, and functions f1:A→B,f2:A→C. The
gluing Dof Band Calong A(or more precisely along f1and f2), written D=B+AC, is defined as
the quotient D= (B]C)/≡where ≡is the smallest equivalence relation containing the relation
∼={(f1(a), f2(a)) |a∈A}.
This means that we transitively identify all those elements in B]Cwhich are commonly mapped by the
same interface element. Moreover, we obtain functions g1:B→Dand g2:C→Dwith g1(b) = [b]≡
for all b∈B, and g2(c)=[c]≡for all c∈C.
Af1//
f2
B
g1
Cg2//D
(PO)
Fact 1 (Pushout of Sets).The diagram (PO) in Def. 7 is a pushout diagram in the category Sets, i. e.
(PO) commutes and has the following universal property: For all sets Xand functions h1:B→X,
h2:C→Xwith h1◦f1=h2◦f2there exists a unique h:D→Xwith h◦g1=h1and h◦g2=h2.
Proof. See Fact 2.17 in [EEPT06].
The gluing of AHL-nets over a given interface can be defined as the component-wise gluing in Sets.
Due to the fact that the gluing in Sets is also a pushout, we obtain also unique induced pre, post,
condition and type functions, leading to a well-defined AHL-net as shown in [Gab10].
Definition 8 (Gluing of AHL-Nets).Given two AHL-net morphisms f1:AN0→AN1and f2:AN0→
AN2the gluing AN3of AN1and AN2along f1and f2, written AN3=AN1+(AN0,f1,f2)AN2, with
ANx= (Σ, Px, Tx, prex, postx, condx, typex, A) for x= 0,1,2,3 is constructed as follows:
•T3=T1+T0T2with f0
1,T and f0
2,T as pushout (2) of f1,T and f2,T in Sets.
•P3=P1+P0P2with f0
1,P and f0
2,P as pushout (3) of f1,P and f2,P in Sets
•pre3(t) = (f0⊕
1,P ◦pre1(t1) , if f0
1,T (t1) = t;
f0⊕
2,P ◦pre2(t2) , if f0
2,T (t2) = t.
•post3(t) = (f0⊕
1,P ◦post1(t1) , if f0
1,T (t1) = t;
f0⊕
2,P ◦post2(t2) , if f0
2,T (t2) = t.
•cond3(t) = (cond1(t1) , if f0
1,T (t1) = t;
cond2(t2) , if f0
2,T (t2) = t.
10
•type3(p) = (type1(p1) , if f0
1,P (p1) = p;
type2(p2) , if f0
2,P (p2) = p.
•f0
1= (f0
1,P , f0
1,T ) and f0
2= (f0
2,P , f0
2,T ).
AN0
f2
f1//
(1)
AN1
f0
1
T0
f2,T
f1,T //
(2)
T1
f0
1,T
P0
f2,P
f1,P //
(3)
P1
f0
1,P
AN2f0
2
//AN3T2f0
2,T
//T3P2f0
2,P
//P3
Fact 2 (Pushout of AHL-Nets).The diagram (1) in Def. 8 is a pushout diagram in the category
AHLNets, i. e. (1) commutes and it has the following universal property: For all AHL-nets AN 0
3and
AHL-morphisms h1:AN 1→AN 0
3,h2:AN 2→AN 0
3with h1◦f1=h2◦f2there exists a unique
AHL-morphism h:AN 3→AN 0
3such that h◦f0
1=h1and h◦f0
2=h2.
Proof-Idea. The pushouts (2) and (3) provide unique functions hP:P3→P0
3,hT:T3→T0
3which
together form an AHL-morphism h= (hP, hT) : AN3→AN0
3satisfying the universal property. A
detailed proof can be found in [Gab10].
Example 4 (Evolution of Apache Wave Platform).With the gluing of AHL-nets we can use the pro-
duction insertLog in Fig. 5 to describe an evolution of Apache Wave platforms. Figure 6a shows a gluing
of the two AHL-nets Land Platform0over the interface Ileading to our example AHL-net P latform
from Section 2. Note that the morphism kmaps the places in Inon-injectively to the corresponding
places uand w. As a result the gluing does not only glue the transition modify text to the places that
are mapped by the same interface places but also the equally mapped places from Platform0are glued
together in the net Platform. On the other hand, the AHL-nets Land Platform0can be considered as
a decomposition of the AHL-net Platform.
Consider now the right-hand side of the production insertLog in Fig. 5. Using the morphisms r:I→
Rand k:I→Platform0we obtain the AHL-net Platform0in Fig. 3 as gluing of Rand Platform0over
the interface Ias shown in Fig. 6b.
The combination of both gluings describes a direct transformation of AHL-nets Platform ⇒Platform0
in the sense of Def. 9 below. The transformation uses the production insertLog at match m:L→
Platform, replacing the transition modify text by modify and log.
Definition 9 (Direct Transformation of AHL-Nets).Given a production %:Ll
←Ir
→Rand a (match)
morphism m:L→AN in AHLNets.
Then a direct transformation AN (p,m)
⇒AN0in AHLNets is given by pushouts (1) and (2) in AHLNets.
A transformation of AHL-nets is a sequence AN0
(p1,m1)
⇒AN1· · · (pn,mn)
⇒ANnof direct transformations,
written AN0⇒∗ANn.
L
m
(1)
I
l
oor//
c
(2)
R
n
AN C
d
ooe//AN0
Remark 3 (Modelling of Token-Game with Transformation).For AHL-nets with individual tokens (see
Remark 1) there is a similar definition for the rule-based direct transformation of AHL-nets with individ-
ual tokens (see [MGE+10]). It allows an alternative way to model the firing behaviour of AHL-nets by
rule-based transformation. For every consistent transition assignment (t, asg) (see Def. 2) of an AHL-net
with individual tokens ANI enabled under a token selection S= (M, m, N, n) (see Remark 1) there is a
corresponding transition rule %(t, S, asg) such that there is an equivalence between the firing of (t, asg)
via Sand the canonical direct transformation of ANI using the rule %(t, S, asg). For more details we
refer to [MGE+10].
11
4 Evolution of Communication Platforms and Transformation of Scenario Nets
w : wavelet
u : user
new wavelet
n = new(user,free)
next = next(free)
id : nat
invite user
invited(o, user1) = true
n = addUser(o,user2)
user user
user1 7 user2
user1 7 user2
n
on
free
next
Platform0
w : wavelet
u : user
new wavelet
n = new(user,free)
next = next(free)
modify text
invited(o,user) = true
txt: text
rng: range
r = remText(o,rng)
n = insText(r,txt,start(rng))
id : nat
invite user
invited(o, user1) = true
n = addUser(o,user2)
user
user
user
user
user1 7 user2
user1 7 user2
n
n
o
o
n
free
next
Platform
w1 : waveletu1 : user
w2 : waveletu2 : user
w1 : wavelet
u1 : user
modify text
invited(o,user) = true
txt: text
rng: range
r = remText(o,rng)
n = insText(r,txt,start(rng))
user o
w2 : waveletu2 : user
user n
l
LI
mk
(a) Gluing of AHL-nets Land Platform0
w : wavelet
u : user
new wavelet
n = new(user,free)
next = next(free)
id : nat
invite user
invited(o, user1) = true
n = addUser(o,user2)
user user
user1 7 user2
user1 7 user2
n
on
free
next
Platform0
w1 : waveletu1 : user
w2 : waveletu2 : user
I
n
k
w :
wavelet
u : user
new wavelet
n = new(user,free)
next = next(free)
modify and log
invited(o,user) = true
txt: text
rng: range
r = remText(o,rng)
n = insText(r,txt,start(rng))
log = logEntry(user, rng, txt)
id : nat
invite user
invited(o, user1) = true
n = addUser(o,user2)
user
user
user
user
user1 7 user2
user1 7 user2
n
n
o
o
n
free
next
Platform'
log : mod
log
w1 : wavelet
u1 : user
modify and log
invited(o,user) = true
txt: text
rng: range
r = remText(o,rng)
n = insText(r,txt,start(rng))
log = logEntry(user, rng, txt)
user o
log : mod
log
w2 : waveletu2 : user
user n
r
R
(b) Gluing of AHL-nets Rand Platform0
Figure 6: Direct transformation of AHL-nets Platform ⇒Platform0
12
The following gluing condition is a necessary and sufficient condition for the existence of a direct
transformation of AHL-nets. In order to satisfy the gluing condition by a production %under a match
msome of the places and transitions in the AHL-net AN in the codomain of mmust not be deleted by
application of the production. The preimages of these elements in the left-hand side of the production
are called identification points and dangling points.
The identification points are the preimages of places and transitions which are mapped non-injectively
by the match m. The dangling points are the preimages of places which occur in the pre or post conditions
of a transition which is matched, and therefore cannot be deleted by application of the production.
Definition 10 (Gluing Condition for AHL-Nets).Given a production %:Ll
←Ir
→Rfor AHL-nets and
an AHL-morphism m:L→AN. We define the set of identification points1
IP ={x∈PL| ∃x06=x:mP(x) = mP(x0)} ∪
{x∈TL| ∃x06=x:mT(x) = mT(x0)}
the set of dangling points2
DP ={p∈PL| ∃t∈TAN \mT(TL), term ∈TΣ(X)type(p):
(term, mP(p)) ≤preAN (t)⊕postAN (t)}
and the set of gluing points3
GP =lP(PI)∪lT(TI)
We say that %and msatisfy the gluing condition if IP ∪DP ⊆GP.
L
m
I
l
oor//R
AN
Fact 3 (Direct Transformation of AHL-Nets).Given a production for AHL-nets %= (Ll
←Ir
→R)
and a match m:L→AN . The production %is applicable on match m, i. e. there exists a context
AHL-net AN 0in the diagram below, such that (1) is pushout, iff %and msatisfy the gluing condition in
AHLNets. Then AN 0is called pushout complement of land m. Moreover, we obtain a unique AN0
as pushout object of the pushout (2) in AHLNets.
L
m(1)
I
l
oo
c
r//R
n
AN AN 0
d
oo_ _ _ _ //____ AN 0
(2)
Proof. See [PER95].
Example 5 (Evolution of Apache Wave Platform (revisited)).The gluings of AHL-nets depicted in
Fig. 6 describe a direct transformation of AHL-nets Platform ⇒Platform0using production insertLog
at match m. The diagram in Fig. 6a corresponds to the pushout (1) and the diagram in Fig. 6b
corresponds to pushout (2) in Fact 3.
Now, we extend our framework to the gluing and transformation of AHL-process nets. For this
purpose we define productions for AHL-process nets where the left hand and right hand side and the
interface of the production are AHL-process nets.
Definition 11 (Production for AHL-Process Nets).Aproduction for AHL-process nets %:Ll
←Ir
→R
is a span of injective AHLPNets-morphisms l:I→Land r:I→R.
L I
l
oor//R
1i. e. all elements in Lthat are mapped non-injectively by m
2i. e. all places in Lthat would leave a dangling arc, if deleted
3i. e. all elements in Lthat have a preimage in I
13
4 Evolution of Communication Platforms and Transformation of Scenario Nets
The following lemma states the fact that the gluing and the direct transformation of AHL-process
nets via pushout constructions can be computed in the category of AHL-nets because every pushout in
AHLPNets is also a pushout in AHLNets.
Lemma 2 (Pushout of AHL-Process Nets).Given AHL-process nets I,K1and K2and two AHL-net
morphisms f:I→K1and g:I→K2. If (1) is a pushout in AHLPNets then (1) is also pushout in
AHLNets.
K1
f0
A
A
A
A
A
I
f??
g
?
?
?
?
?
?
?(1)K
K2
g0
}
}
}
>>
}
}
}
Proof Idea. Constructing the pushout of the given span in the category AHLNets we obtain a pushout
object K0together with a unique induced morphism k:K0→K. Then by Lemma 1 the morphism k
implies that K0is an AHL-process net leading to a unique morphism k0:K→K0by universal property of
pushout (1). The morphisms kand k0can be shown to be inverse isomorphisms which by the uniqueness
of pushouts implies that (1) is pushout in AHLNets. For a detailed proof see Appendix A.2.
The gluing of AHL-nets may produce forward or backward conflicts as well as cycles in the causal
relation. So for the gluing of two AHL-process nets via pushout construction the AHL-process nets have
to be composable in order to obtain again an AHL-process net as a result of the gluing. Composability
of AHL-process nets with respect to an interface means that the result of the gluing does not violate the
process net properties in Def. 3.
A span of AHLPNets-morphisms i1:I→K1and i2:I→K2induces a causal relation between
the elements of the interface I. This relation consists of the causal relation between elements in K1and
K2and additionally between those elements in both of the AHL-process nets which is obtained by gluing
over the interface.
Definition 12 (Induced Causal Relation).Given three AHL-process nets I,K1and K2, and two AHL-
net morphisms i1:I→K1and i2:I→K2. The induced causal relation <(i1,i2)is defined as the
transitive closure of the relation ≺(i1,i2)defined by
≺(i1,i2)={(x, y)∈(PI]TI)×(PI]TI)|i1(x)<K1i1(y) or i2(x)<K2i2(y)}.
Definition 13 (Composability of AHL-Process Nets).Given three AHL-process nets I,K1and K2,
and two AHL-net morphisms i1:I→K1and i2:I→K2, where i1is injective. Then (K1, K2)are
composable w.r.t. (I, i1, i2) if
1. (No Cycles) the induced causal relation <(i1,i2)is a strict partial order,
2. (Non-Injective Gluing)
•for all p16=p2∈IN(I) with i2(p1) = i2(p2) there is
i1(p1)∈IN(K1) or i1(p2)∈IN(K1),
•for all p16=p2∈OUT(I) with i2(p1) = i2(p2): there is
i1(p1)∈OUT(K1) or i1(p2)∈OUT(K1), and
3. (No Conflicts)
•for all p∈IN(I) : i1(p)/∈IN(K1)⇒i2(p)∈IN(K2),
•for all p∈OUT(I) : i1(p)/∈OUT (K1)⇒i2(p)∈OUT(K2).
The composability of AHL-process nets is a sufficient and necessary condition for the existence of the
gluing of AHL-process nets as pushout in the category AHLPNets.
14
Fact 4 (Gluing of AHL-Process Nets).Given AHL-process nets I,K1,K2and AHL-net morphisms
i1:I→K1and i2:I→K2where i1is injective. Then there exists a pushout (PO) in the category
AHLPNets (see Def. 3) iff (K1, K2)are composable w.r.t. (I, i1, i2). The AHL-process net Kis then
called gluing of K1and K2along i1and i2, written K=K1+(I,i1,i2)K2.
Extension to Processes. In order to extend this gluing construction for AHL-processes in the
category Proc(AN)(see Def. 5) one additionally requires AHL-morphisms mp1:K1→AN and mp2:
K2→AN with mp1◦i1=mp2◦i2. The pushout (PO) in AHLPNets then provides a unique morphism
mp :K→AN such that (PO) is also a pushout in Proc(AN).
Ii1//
i2
(PO)
K1
i0
1
mp1
K2i0
2
//
mp2,,
K
mp
D
D
D
D
""
D
D
D
AN
Proof-Idea. In order to show that the diagram (PO) constructed as pushout in AHLNets is also a
pushout in the full subcategory AHLPNets ⊆AHLNets it suffices to show that the pushout object
Kis an AHL-process net. The fact that the gluing does not produce conflicts or cycles is ensured by the
corresponding items 1 and 3 of the required composability of K1and K2. Furthermore, item 2 ensures
that there are no conflicts or violations of the unarity condition created by non-injective gluing.
The other way around the pushout (PO) in AHLPNets means that the pushout object Kis an
AHL-process net and by Lemma 2 (PO) is also a pushout in AHLNets. Then, it can be shown that
the conditions of the composability can be derived from the fact that Ksatisfies the requirements of an
AHL-process net .
For a detailed proof see Appendix A.3.
We define a gluing relation for the transformation of AHL-process nets which is induced by a pro-
duction %for AHL-process nets and a match m. The gluing relation is a relation between the interface
elements of %which consists of the causal relation between elements in the codomain of mthat are
preserved by application of %and the causal relation of the right hand side of the production, and
additionally it consists of the causal relations that are obtained by gluing over the interface.
Definition 14 (Gluing Relation for Transformations).Given a production for AHL-process nets %:
Ll
←Ir
→Rand a match m:L→Kwe define the relations
≺(K,m)={(x, y)∈(PK×(TK\mT(TL))) ]((TK\mT(TL)) ×PK)|x∈ •y}
and <(K,m)as the transitive closure of ≺(K,m). Furthermore we define
≺(%,m)={(x, y)∈(PI×TI)](TI×PI)|m◦l(x)<(K,m)m◦l(y)∨r(x)<Rr(y)}
The transitive closure <(%,m)of ≺(%,m)is called gluing relation of production %under match m.
For the transformation of AHL-process nets we define a transformation condition which is a necessary
and sufficient condition that the direct transformation of an AHL-process nets exists. The satisfaction
of the transformation condition by a production %and a match mrequires that the gluing condition for
AHL-nets (see Def. 10) is satsfied. Moreover, it requires that the gluing condition is irreflexive and that
the application of the production does neither produce any conflicts nor violates the unarity condition
of AHL-process nets.
Definition 15 (Transformation Condition for AHL-Process Nets).Given a production for AHL-process
nets %:Ll
←Ir
→Rand an AHL-process net K. Then %satisfies the transformation condition under a
(match) morphism m:L→Kif
1. (Gluing Condition) the gluing condition is satisfied (see Def. 10),
2. (No Cycles) the gluing relation <(%,m)of %under mis a strict partial order,
15
4 Evolution of Communication Platforms and Transformation of Scenario Nets
3. (Non-Injective Gluing)
•for all p16=p2∈IN(I) with m◦l(p1) = m◦l(p2) we have
r(p1)∈IN(R) or r(p2)∈IN(R),
•for all p16=p2∈OUT(I) with m◦l(p1) = m◦l(p2) we have
r(p1)∈OUT(R) or r(p2)∈OUT(R),
4. (No Conflicts) for the sets of in and out places of the match
InP ={x∈IN(I)|l(x)∈IN(L) and m◦l(x)/∈IN(K)},and
OutP ={x∈OUT (I)|l(x)∈OUT(L) and m◦l(x)/∈OUT(K)}
there is
r(InP)⊆IN(R) and r(OutP)⊆OUT(R).
Theorem 1 (Direct Transformation of AHL-Process Nets).Given a production for AHL-process nets
%:Ll
←Ir
→Rand an AHL-process net Ktogether with a morphism m:L→K. Then the direct
transformation of AHL-process nets with pushouts (1) and (2) in AHLPNets exists iff %satisfies the
transformation condition for AHL-process nets under m.
Extension to processes. In order to extend this construction for AHL-processes in the category
Proc(AN)one additionally requires AHL-morphisms mp :K→AN and rp :R→AN with mp◦m◦l=
rp ◦r. Then by composition of AHL-morphisms we obtain an AHL-process cp =mp ◦d:C→AN and
the pushout (1) in AHLPNets is also a pushout of mp◦mand cp in Proc(AN). Moreover, the pushout
(2) in AHLPNets provides a unique morphism mp0:K0→AN such that mp0is pushout of cp and rp
in Proc(AN)according to Fact 4.
L
(1)
m
I
c
l
oor//R
n
(2)
K C
d
ooe//K0
Proof-Idea. Satisfaction of the transformation condition for AHL-process nets means that the gluing
condition for AHL-nets is satsfied which by Fact 3 implies that pushouts (1) and (2) can be constructed
in AHLNets. It can be shown that the process net properties in Def. 5 are reflected by AHL-morphisms,
implying that Cis an AHL-process net and (1) is also a pushout in AHLPNets. Finally, it can be
shown that the satisfaction of the transformation condition implies that Cand Rare composable w. r. t.
(I, c, r), i. e. the pushout (2) in AHLNets is also a pushout in AHLPNets.
Vice versa, given pushouts (1) and (2) in AHLPNets, we have also pushouts in AHLNets, implying
that the gluing condition for AHL-nets is satisfied. The satisfaction of the rest of the transformation
condition can be obtained by composability of Cand Rw. r. t. (I, c, r) by pushout (2) in AHLPNets,
and the construction of pushout complement C.
For a detailed proof see Appendix A.4.
Example 6 (Evolution of Scenario Net).The top row of Fig. 7 shows a production %:L←- I ,→Rfor
AHL-process nets that replaces two single invitations by one invitation of two users at a time. There
is a match m:L→Winto the AHL-process net Wat the left bottom of Fig. 7 where the transitions
are matched by inclusion and the places in the environments of the transitions are matched accordingly
to the environments of the images in W. The match msatisfies the transformation condition for AHL-
process nets. So the rule %can be applied with match m, leading to the context net W0where the two
invitations have been removed, and to the result net W0which is an AHL-process net containing the
new transition invite two.
Note that there are three other possible matches for the rule %into the AHL-process net W, but
these matches violate the gluing condition for AHL-nets because in the case of all three matches the
places w4and u7are identification points which are no gluing points (see Def. 10).
Moreover, consider a modified rule %0, containing places w4and u7in its interface and right-hand
side. Then %0and each of the possible matches satisfy the gluing condition for AHL-nets. But the
16
two matches m1and m2, matching both transitions of L0to invite1respectively invite2, violate the
transformation condition for AHL-process nets. The reason for the violation is the second condition, i. e.
for u6, u8∈IN(I) there is m1◦l(u6) = m1◦l(u8), but there is neither r(u6) nor r(u8) in IN(R). The
same holds for m2. Therefore, there exists no AHL-process net that is the result of a direct transformation
via %0and match m1respectively m2.
5 Extension of Scenarios based on Platform Evolutions
In the previous section we have presented the rule-based transformation of AHL-nets and processes and
we have shown how it can be used to evolve Apache Wave platforms and scenarios. As mentioned in
Section 2 it is possible that the communication platform is modified at runtime and there may already
exist some waves that correspond to the old version of the platform. So we have the case that there is an
AHL-process wave :Wave →Platform and a direct transformation of AHL-nets Platform ⇒Platform0.
In this section we show under which condition the scenario wave can be extended to a scenario wave0:
Wave →Platform0of the new platform. We regard wave0as an extension of wave if the two processes
“agree” in the context net of the direct transformation Platform ⇒Platform0in the following sense.
Definition 16 (Extension of AHL-Process based on AHL-Net Transformation).Given an AHL-net AN
and an AHL-process mp :K→AN. Let AN %,m
⇒AN0be a direct transformation with pushouts (1)
and (2) in AHLNets as depicted in Figure 8. Then we call mp0:K→AN0an extension of mp if there
exists mp0:K→AN0with f◦mp0=mp and g◦mp0=mp0.
L
(1)
m
I
k
l
oor//R
n
(2)
AN AN0
f
oog//AN0
K
mp
iiSSSSSSSSSSSSS
mp0
OO
mp0
55
k
k
k
k
k
k
k
k
k
k
k
k
k
Figure 8: Extension of AHL-Process
The following extension condition is a sufficient and necessary condition for the extension mp0of an
AHL-process mp based on an AHL-net transformation. In order to satisfy the extension condition, the
transformation must not delete any place or transition that have an occurrence in the AHL-process mp.
Definition 17 (Extension Condition).Given an AHL-net AN, an AHL-process mp :K→AN and a
direct transformation AN %,m
⇒AN0. We define the the set PP of process points as
PP ={x∈PL| ∃p∈PK:mpP(p) = mP(x)}∪{x∈TL| ∃t∈TK:mpT(t) = mT(x)}
We say that mp and %, m satisfy the extension condition if all process points are gluing points (see
Def. 10), i. e. P P ⊆GP .
Theorem 2 (Extension of AHL-Process based on AHL-Net Transformation).Given an AHL-net AN,
an AHL-process mp :K→AN and a direct transformation AN %,m
⇒AN0with pushouts (1) and (2) in
AHLNets as depicted in Figure 8. There exists an extension mp0:K→AN0of mp if and only if mp
and %, m satisfy the extension condition.
Proof-Idea. If the extension condition is satisfied, it can be explicitely shown that there exists a well-
defined morphism mp0:K→AN0defined by mp0=f−1◦mp. Then the extension mp0:K→AN0is
obtained by composition mp0=g◦mp0, satisfying the required properties.
Vice versa, the existence of an extension mp0:K→AN0implies the existence of a suitable morphism
mp0:K→AN0which can be used to show that all process points are gluing points.
For a detailed proof see Appendix A.5.
17
5 Extension of Scenarios based on Platform Evolutions
invite1
invited(o, user1) = true
n = addUser(o, user2)
new1
n = new(user,free)
next = next(free)
u1 : user
id1 : nat
user
free
next
u2 : user
w1 : wavelet
nuser u3 : user
user2
user1
o
u5 : user
u4 : user
w2 : wavelet
user1user2
n
id2 : nat
W
invite2
invited(o, user1) = true
n = addUser(o, user2)
user1
u6 : user
user2
o
w3 : wavelet
nu8 : user
u7 : user
user2
user1
new1
n = new(user,free)
next = next(free)
u1 : userid1 : nat
user
free
next
u2 : userw1 : wavelet
nuser
u3 : user
u4 : user
id2 : nat
u6 : user
w2 : wavelet
u8 : user
u5 : user
new1
n = new(user,free)
next = next(free)
u1 : user
id1 : nat
user
free
next
u2 : user
w1 : wavelet
nuser u3 : user
user2
user1
o
u4 : user
user2
id2 : nat
u6 : user
user3
w2 : wavelet
n
u8 : user
u5 : user user3
user1
invite1
invited(o, user1) = true
n = addUser(o, user2)
u1 : user
w1 : wavelet
u2 : user
user2
user1
o
u5 : user
u4 : user
w3 : wavelet
user1
user2
n
invite2
invited(o, user1) = true
n = addUser(o, user2)
user2
user1
o
u7 : user
u8 : user
w4 : wavelet
user1user2
n
u1 : user
w1 : wavelet
u2 : user
u3 : user
u8 : user
w2 : wavelet
u1 : user
w1 : wavelet
u2 : user
u3 : user
u8 : user
w2 : wavelet
u4 : user
u4 : user
invite two
invited(o, user1) = true
n0 = addUser(o, user2)
n = addUser(n0, user3)
user2
user1
o
user1
user2
n
u6 : user
u6 : user
user3
user3
invite two
invited(o, user1) = true
n0 = addUser(o, user2)
n = addUser(n0, user3)
W0W'
LIR
u6 : user
u3 : user
w2 : wavelet
u5 : user
w3 : wavelet
u5 : user
w3 : wavelet
Figure 7: Evolution W%,m
⇒W0of Scenario Nets
18
Example 7 (Extension of Scenario based on Platform Evolution).Consider again the AHL-process
net Win the left bottom of Fig. 7 together with an AHL-morphism mp :W→Platform matching
all elements in Wto the corresponding elements with similar names. Furthermore, consider the AHL-
net transformation Platform ⇒Platform0via production insertLog and match min Example 4. The
set of process points with this transformation and AHL-process is the set PP ={u1, u2, w1, w2}which
corresponds exactly to the set of gluing points and therefore PP ⊆GP. So the AHL-process mp
can be extended to a process mp0:W→Platform0that maps all elements in the same way as mp
and that corresponds to a scenario in the modified platform In contrast, for the AHL-process wave :
Wave →Platform in Example 2 the set of process points PP ={u1, u2, w1, w2,modify text}and we
have PP *GP because modify text is not a gluing point. Thus, there exists no extension of wave based
on the platform evolution Platform ⇒Platform0.
6 Evolution of Scenarios based on Platform Evolutions
As we have seen in Example 7 there are cases of scenarios and platform evolutions that do not sat-
isfy the extension condition. The reason in the discussed example is that the scenario wave contains
three occurrences of the action modify text, but there is no corresponding action in the new platform
Platform0. Nonetheless, the feature to modify some text in a wavelet has not been fully removed from the
communication platform, but it has been replaced by the new action modify and log which does more
or less the same as the old action with the only difference that it does additionally create a log entry.
So as discussed at the end of Section 2 an intuitive solution is to apply the modification of the platform
also to the scenario wave, leading to a scenario wave0as depicted in Fig. 4 where all occurrences of the
action modify text have been replaced by the new version modify and log of the action.
In this section we give a general construction for the modification of scenarios based on a special kind
of platform evolution, replacing one single action at a time. For this purpose, since scenarios are modeled
as AHL-processes, we need productions and the direct transformation of AHL-processes as defined in
the following.
Definition 18 (Production for AHL-Processes).Aproduction for AHL-processes is a span (%∗, %) :
mpL
(l∗,l)
←− mpI
(r∗,r)
−→ mpRof injective AHLProcs-morphisms as shown in Figure 9b.
Definition 19 (Direct Transformation of AHL-Processes).Given a production %:mpL
(l∗,l)
←− mpI
(r∗,r)
−→
mpRfor AHL-processes and a (match) morphism (m∗, m) : mpL→mp. Then a direct transformation
mp (%∗,%),(m∗,m)
=⇒mp0is given by the commuting cube in Figure 9b where the front and back faces are
pushouts in AHLNets and AHLPNets, respectively.
K
mp
%∗,m∗
+3K0
mp0
(%∗,%),(m∗,m)+3
AN %,m +3AN0
(a) Transformation of AHL-
process
L∗
m∗
mpL
""
D
D
D
DI∗
l∗
oor∗//
mpI
##
F
F
F
F
FR∗
mpR
""
F
F
F
F
L
m
I
l
oor//
R
K
mp
B
B
B
BK0
mp0""
D
D
D
D
oo//K0
mp0!!
C
C
C
C
AN AN0
oo//AN0
(b) Commuting Cube
Figure 9: Transformation of AHL-process
In the following we show how to construct productions for processes from a special type of production
for AHL-nets, called action evolution. An action evolution is a direct transformation of AHL-nets that
uses a special kind of production. The main aspect of such a production is that it contains exactly one
transition in its left-hand side.
Definition 20 (Action Evolution).A production %:Ll
←Ir
→Rfor AHL-process nets is called a
production for an action evolution if
19
6 Evolution of Scenarios based on Platform Evolutions
1. (Single Action) Lcontains only one transition and its environment, i. e. TL={t%}and for all
p∈PL:p∈ •t%∪t%•,
2. (Unique Arc Inscriptions) all arcs in one direction have different inscriptions, i. e. (term1, p1)⊕
(term2, p2)≤preL(t%) implies term16=term2and p16=p2, and the same holds for post arcs4,
3. (Preserved Environment) %is non-deleting on places, i. e. PL=lP(PI), and
4. (Preserved Input and Output) %preserves input and output places, i. e. for all p∈PI:
•l(p)∈IN(L)⇒r(p)∈IN(R) and
•l(p)∈OUT(L)⇒r(p)∈OUT (R).
Given an AHL-net AN and a match m:L→AN, a direct transformation AN %,m
=⇒AN0is called action
evolution.
Example 8 (Action Evolution).The production insertLog in Fig. 5 is a production for action evolution.
The left-hand side of insertLog consists of only one transition modify text and its environment. The
inscriptions of pre respectively post arcs of the left-hand side are unique. Note that the fact that there are
similar arc inscriptions user on pre and post arcs does not violate the single action condition. Moreover,
the production is non-deleting on places and all input respectively output places of the left-hand side
are also input respectively output places in the right-hand side of the production.
Hence, the direct transformation Platform ⇒Platform0via production insertLog and match mshown
in Fig. 6 is an action evolution.
Now, the following theorem states that for every process mp :K→AN and an action evolution
of the net AN there exists a corresponding transformation of AHL-processes mp ⇒mp0. As result we
obtain a process corresponding to the result of the action evolution, where all occurrences of the modified
part in AN have been modified in Kas well.
Theorem 3 (Process Evolution based on Action Evolution).Given an action evolution AN %,m
=⇒AN0
via production %:Ll
←Ir
→R, and a process mp :K→AN. Then there exists a production (%+, %)
for AHL-processes and a direct transformation mp (%+,%)
=⇒mp0as depicted in Figure 10a that realizes the
changes described by %on all occurrences in the process mp.
Construction: Let (mi:L→K)i∈I be the class of all matches mi:L→Kwith mp ◦mi=m.
1. The production for AHL-process nets %+:L+l+
←I+r+
→R+is defined as componentwise coproduct
in AHLPNets:
•X+=`i∈I Xwith injections ιX
i:X→X+for X∈ {L, I, R},
•x+=`i∈I xfor x∈ {l, r}
2. The processes mpX:X+→Xfor X∈ {L, I, R}are the unique induced morphisms with mpX◦ιX
i=
idXfor all i∈ I (see Figure 10b).
3. The match m+:L+→Kis the unique induced morphism with m+◦ιL
i=mifor all i∈ I.
4. K0and K0are constructed as direct AHL-process net transformation in the back of Figure 10a.
5. mp0:K0→AN0is defined as mp0=f−1◦mp ◦f0, and mp0:K0→AN0is induced by the right
pushout in the back of Figure 10a.
4This condition is necessary in order avoid that a match of the rule can correspond ambiguously to one occurrence in
a process of a matched AHL-net. For the modelling with AHL-nets equal term inscriptions in the environment of one
transition are not really necessary, since equality of two terms can also be expressed as a condition of the transition.
20
L+
m+
mpL
%%
K
K
K
K
K
KI+
l+
oor+//
mpI
%%
K
K
K
K
K
KR+
mpR
%%
L
L
L
L
L
L
L
mi
yyttttttm
I
l
oor//
k
R
n
K
mp $$
I
I
I
I
IK0
mp0%%
J
J
J
J
J
f0
oog0//K0
mp0%%
J
J
J
J
J
AN AN0
f
oog//AN0
(a) Process Evolution
X
ιX
i
idX
3
3
3
3
3
3
3
3
3
3
3
3
3
X+
mpX//X
(b) Induced Pro-
cess
Figure 10: Process evolution based on action evolution
Proof-Idea. The construction of %+by coproducts in AHLPNets as given above is well-defined, and the
universal property of coproducts can be used to show that (%+, m+) is a production for AHL-processes
(see Def. 18). Furthermore, the construction of L+induces a unique m+:L+→Kwith m+◦ιL
i=mi
for all i∈ I, and by compatibility of miwith mfor all i∈ I it can be concluded that (m+, m) is an
AHLProcs-morphism.
The existence of the direct transformation of AHL-process nets with pushouts in the back of Fig. 10a
can be shown using the properties required for action evolutions in Def. 20.
Finally, it can be shown that there exists a well-defined AHL-morphism mp0:K0→AN0defined
as mp0=f−1◦mp ◦f0, leading to a unique morphism mp0:K0→AN0induced by the pushout in the
right back of Fig. 10a such that all diagrams in the cube commute.
For a detailed proof see Appendix A.6.
Example 9 (Evolution of Scenario based on Platform Evolution).Now, consider again the platform
evolution Platform ⇒Platform0via production insertLog (see Fig. 5) and match min Example 4 and
the scenario wave :Wave →Platform (see Fig. 2) in Example 2. The platform evolution via production
insertLog is an action evolution and there are three possible matches mi:L→Wave consistent with m,
mapping modify text to the three occurrences of the transition in Wave. We can construct a production
insertLog+consisting of three copies of the left-hand side, interface and right-hand side of insertLog+as
depicted in Fig. 11. Moreover, we obtain processes mpL:L+→L,mpI:I+→Iand mpR:R+→R
mapping every copy to its original, and there is a match m+:L+→Wave that maps all copies according
to the matches mi:L→Wave. By application of insertLog+with match m+we obtain the scenario
wave0:Wave0→Platform0as depicted in Fig. 11 where all occurrences of the modify text action have
been replaced by a modfiy and log action.
In the future we will consider different types of multiple action evolutions, i. e. evolutions that modify
more than one transition at once. Two promising approaches are forward and backward multiple action
evolutions, which are evolutions where we have additional information about the relation between the left-
hand side Land right-hand side Rof the used production. These relations are expressed as morphisms
between the “skeletons” Skel(L) and Skel(R), that is only the low-level Petri net structure without any
high-level data part, of Lrespectively R.
A forward multiple action evolution consists of a morphism φ:Skel(L)→Skel(R). The morphism
describes that an element xis replaced by φ(x). This allows for example to express that one new action
modify text is the new version of multiple old actions insert text and remove text. The corresponding
process evolution should then replace all occurrences of insert text as well as of remove text by new
occurrences of modify text.
A backward multiple action evolution consists of a morphism ψ:Skel(R)→Skel(L), describing that
an element xreplaces ψ(x). This allows for example to express that a new action modify without invitation
is the new version of an old action modify text and an existing action invite user is removed without
any replacement. The corresponding process evolution should then replace all occurrences of modify text
while deleting all occurrences of invite user.
21
6 Evolution of Scenarios based on Platform Evolutions
l+r+
w1 : waveletu1 : user
w2 : waveletu2 : user
I
w1 : wavelet
u1 : user
modify and log
invited(o,user) = true
txt: text
rng: range
r = remText(o,rng)
n = insText(r,txt,start(rng))
log = logEntry(user, rng, txt)
user o
log : mod
log
w2 : waveletu2 : user
user n
R
w1 : wavelet
u1 : user
modify text
invited(o,user) = true
txt: text
rng: range
r = remText(o,rng)
n = insText(r,txt,start(rng))
user o
w2 : waveletu2 : user
user n
L
w1 : wavelet
u1 : user
modify text
invited(o,user) = true
txt: text
rng: range
r = remText(o,rng)
n = insText(r,txt,start(rng))
user o
w2 : waveletu2 : user
user n
L
w1 : wavelet
u1 : user
modify text
invited(o,user) = true
txt: text
rng: range
r = remText(o,rng)
n = insText(r,txt,start(rng))
user o
w2 : waveletu2 : user
user n
L+
w1 : waveletu1 : user
w2 : waveletu2 : user
I
w1 : waveletu1 : user
w2 : waveletu2 : user
I+
w1 : wavelet
u1 : user
modify and log
invited(o,user) = true
txt: text
rng: range
r = remText(o,rng)
n = insText(r,txt,start(rng))
log = logEntry(user, rng, txt)
user o
log : mod
log
w2 : waveletu2 : user
user n
R
w1 : wavelet
u1 : user
modify and log
invited(o,user) = true
txt: text
rng: range
r = remText(o,rng)
n = insText(r,txt,start(rng))
log = logEntry(user, rng, txt)
user o
log : mod
log
w2 : waveletu2 : user
user n
R+
modify2
: modify text
invite1
: invite user
new1
: new wavelet
modify1
: modify text
u1 : u
id1 : id
user
free
next
u2 : u
w1 : w
n
user user
o
u3 : u
w2 : w
user
n
u4 : u
user2
user1
o
u6 : uu5 : u
w3 : w
user2
user1
n
user
o
w4 : w
n
user
new2
: new wavelet
free
id3 : id
next
u8 : u
user
user
modify3
: modify text
user
u9 : u
w5 : w
n o
user
w6 : w
n
id2 : id
u7 : u
Wave
modify'2
: modify and log
invite1
: invite user
new1
: new wavelet
modify'1
: modify and log
u1 : u
id1 : id
user
free
next
u2 : u
w1 : w
n
user user
o
u3 : u
w2 : w
user
n
u4 : u
user2
user1
o
u6 : uu5 : u
w3 : w
user2
user1
n
user
o
w4 : w
n
user
new2
: new wavelet
free
id3 : id
next
u8 : u
user
user
modify'3
: modify and log
user
u9 : u
w5 : w
n o
user
w6 : w
n
id2 : id
u7 : u
Wave'
l2 : log
log
l1 : log
log
log
l3 : log
m+
n+
⇘
%+ ,m+
Figure 11: Process evolution based on action evolution
22
7 Conclusion
Algebraic high-level (AHL) nets are a well-known modelling technique based on Petri nets [Pet62, Rei85,
Roz87] with algebraic data types [EM85]. In this paper we have shown that AHL nets, AHL processes,
and AHL transformations can be considered as integrated framework for modelling the evolution of
communication platforms. In previous papers it was shown already how to use this framework to model
communication platforms like Skype [HM10] and Google Wave [EG11]. In this paper we have used the
evolution of Apache Wave platforms and scenarios as running example, where platforms are modelled
by AHL-nets and scenarios by AHL-processes. The evolution on both levels is defined by rule-based
modifications in the sense of graph transformation systems [EEPT06]. While transformations of AHL-
nets are introduced already in [PER95] the corresponding problem for AHL-processes is much more
difficult as shown in Section 4.
The first main result shows under which conditions AHL-net processes can be extended if the cor-
responding AHL-net is transformed. This result can be applied to show the extension of scenarios for
a given platform evolution. The second main result shows how AHL-net processes can be transformed
based on a special kind of transformation for AHL-nets, corresponding to action evolution of platforms.
In future work we will study the case of multiple action evolution, which is only briefly discussed in this
paper. Moreover we will analyse what kind of properties can be preserved by evolution of platforms and
scenarios.
A Detailed Proofs
A.1 Proof of Lemma 1 (AHL-Morphisms Reflect AHL-Process Nets)
Given an AHL-morphism f:K1→K2. If K2is an AHL-process net then also K1.
Proof. Given AHL-morphism f:K1→K2with AHL-process net K2. In order to show that K1is an
AHL-process net we have to show that it is unary, there are no forward or backward conflicts and the
causal relation <K1is a strict partial order.
Unarity. Let us assume that K1is not unary, i. e. there are p∈PK1,t∈TK1with
(term1, p)⊕(term2, p)≤preK1(t) or (term1, p)⊕(term2, p)≤postK1(t)
Let (term1, p)⊕(term2, p)≤preK1(t).
Since AHL-morphisms preserve pre conditions there is
(idTOP (X)⊗fP)⊕◦preK1(t) = preK2(fT(t))
and hence
(term1, fP(p)) ⊕(term2, fP(p)) = (idTOP (X)⊗fP)⊕((term1, p)⊕(term2, p))
≤preK2(fT(t))
This implies that K2is not unary, contradicting the fact that K2is an AHL-process net.
The case that (term1, p)⊕(term2, p)≤postK1(t) works analogously. Hence K1is unary.
No forward conflict. Let us assume that K1has a forward conflict, i. e. there is p∈PK1,t16=t2∈TK1
with p∈ •t1∩ •t2. This means that there are term1, term2∈TOP (X)type(p)such that
(term1, p)≤preK1(t1) and (term2, p)≤preK1(t2)
and since AHL-morphisms preserve pre and post conditions we obtain
(term1, fP(p)) = (idTOP (X)⊗fP)⊕(term1, p)
≤preK2(fT(t1))
and
(term2, fP(p)) = (idTOP (X)⊗fP)⊕(term2, p)
≤preK2(fT(t2))
23
A Detailed Proofs
In the case that fT(t1)6=fT(t2) the fact that fP(p)∈ •fT(t1)∩ •fT(t2) means that K2has a
forward conflict, contradicting the fact that K2is an AHL-process net. So let us consider the fact
that fT(t1) = t=fT(t2). Then we have
(term1, fP(p)) ⊕(term2, fP(p)) ≤t
which contradicts the fact that K2is unary. Hence K1has no forward conflict.
No backward conflict. The proof for this case works analogously to the one for forward conflicts
because AHL-morphisms preserve post as well as pre conditions and K2has no backward conflicts.
Strict partial order. We have to show that <K1is irreflexive. So, let us assume that <K1is not
irreflexive, i. e. there exists a cycle x <K1x. This implies f(x)<K2f(x) because AHL-morphisms
preserve pre and post conditions. This contradicts the fact that <K2is irreflexive because it is an
AHL-process net.
Hence, also <K1is irreflexive.
A.2 Proof of Lemma 2 (Pushout of AHL-Process Nets)
Given AHL-process nets I,K1and K2and two AHL-net morphisms f:I→K1and g:I→K2. If (1)
is a pushout in AHLPNets then (1) is also pushout in AHLNets.
K1
f0
A
A
A
A
A
I
f??
g
?
?
?
?
?
?
?(1)K
K2
g0
}
}
}
>>
}
}
}
Proof. Since the category AHLNets has pushouts we obtain pushout (2) in AHLNets. Then by the
fact that AHLPNets is a subcategory of AHLNets by the commutativity of (1) we obtain a unique
morphism k:K0→Kwith k◦f00 =f0and k◦g00 =g0.
K1
f00
B
B
B
!!
B
B
f0
##
I
f??
g
?
?
?
?
?
?
?(2)K0k//K
K2
g00
|
|
>>
|
|
|
g0
;;
K1
f0
A
A
A
A
A
f00
##
I
f??
g
?
?
?
?
?
?
?(1)Kk0//K0
K2
g0
}
}
}
>>
}
}
}
g00
<<
By Lemma 1 we have that K0is an AHL-process net and by the fact that AHLPNets is full subcategory
of AHLNets the morphisms f00 and g00 become AHLPNets-morphisms. So the commutativity of (2)
by the universal property of pushout (1) in AHLPNets implies a unique morphism k0:K→K0with
k0◦f0=f00 and k0◦g0=g00. Now we have
k◦k0◦f0=k◦f00 =f0and k◦k0◦g0=k◦g00 =g0
which by the universal property of pushout (1) implies that k◦k0=idK. Analogously we obtain by the
universal property of pushout (2) that k0◦k=idK0and, thus, kand k0become inverse isomorphisms.
Hence, by the uniqueness of pushouts up to isomorphism it follows that (1) is also pushout in AHLNets.
24
A.3 Proof of Fact 4 (Gluing of AHL-Process Nets)
A.3 Proof of Fact 4 (Gluing of AHL-Process Nets)
Given AHL-process nets I,K1,K2and AHL-net morphisms i1:I→K1and i2:I→K2where i1is
injective. Then there exists a pushout (PO) in the category AHLPNets (see Def. 3) iff (K1, K2) are
composable w. r. t. (I, i1, i2). The AHL-process net Kis then called gluing of K1and K2along i1and
i2, written K=K1+(I,i1,i2)K2.
Extension to Processes. In order to extend this gluing construction for AHL-processes in the
category Proc(AN) (see Def. 5) one additionally requires AHL-morphisms mp1:K1→AN and mp2:
K2→AN with mp1◦i1=mp2◦i2. The pushout (PO) in AHLPNets then provides a unique morphism
mp :K→AN such that (PO) is also a pushout in Proc(AN).
Ii1//
i2
(PO)
K1
i0
1
mp1
K2i0
2
//
mp2,,
K
mp
D
D
D
D
""
D
D
D
AN
Proof. We show the two directions of the proof seperately.
If. Given the AHL-process nets K1, K2and Iand morphisms i1,i2as above we construct the pushout
(PO) in the category AHLNets.
In order to show that (PO) is also a pushout in the full subcategory AHLPNets it suffices to show
that the AHL-net Kis an AHL-process net, i. e. Kis unary, it has no forward or backward conflicts,
and the causal relation <Kis a strict partial order.
Unarity. Let us assume that Kis not unary, i. e. there are p∈PK,t∈TKwith
(term1, p)⊕(term2, p)≤preK(t) or (term1, p)⊕(term2, p)≤postK(t)
Let us consider the case that (term1, p)⊕(term2, p)≤preK(t). Due to the universal property of
pushout (PO) there is a∈ {1,2}and t0∈TKawith i0
a,T (t0) = tand since AHL-morphisms preserve
pre and post conditions there is
preK(t)=(idTOP (X)⊗i0
a,P )⊕◦preKa(t0).
So the fact that (term1, p)⊕(term2, p)≤preK(t) implies
(term1, p1)⊕(term2, p2)≤preKa(t0)
with i0
a(p1) = p=i0
a(p2).
•Case 1. There is a= 1.
The fact that i0
1(p1) = p=i0
1(p2) by pushout (PO) implies that there are x1, x2∈PIwith
i1(x1) = p1,i1(x1) = p2and i2(x1) = i2(x2). Moreover, (term1, p1)⊕(term2, p2)≤preK1(t0)
means i1(x1), i1(x2)/∈OUT(K1).
– Case 1.1. There are x1, x2∈OUT(I).
Then by composability of K1and K2w. r. t. (I, i1, i2) we have that i1(x1)∈OUT (K1)
or i1(x2)∈OUT(K1), contradicting the fact that i1(x1), i1(x2)/∈OUT(K1).
– Case 1.2. There is x1/∈OUT (I).
This means that there is t0∈TIwith (term0, x1)≤preI(t0). By the fact that AHL-
morphisms preserve pre conditions, we obtain (term0, i1(x1)) ≤preK1(i1(t0)). This
implies that i1(t0) = t0because K1is an AHL-process net which does not have any
forward conflicts. Moreover, we have term0=term1. So, using again the fact that AHL-
morphisms preserve pre conditions, we obtain (term2, x2)∈preI(t0) and furthermore
(term1, i2(x1)) ⊕(term2, i2(x2)) ≤preK2(i2(t0)). Hence, by the fact that i2(x1) = i2(x2)
we have that K2is not unary. This is a contradiction because K2is an AHL-process net.
25
A Detailed Proofs
– Case 1.3. There is x2/∈OUT (I).
Analogously to Case 1.2 this case leads to a contradiction because AHL-morphisms pre-
serve post as well as pre conditions and AHL-process net K1does also have no backward
conflicts.
•Case 2. There is a= 2.
Since i1is injective, also i0
2is injective, because injective AHL-morphisms are closed under
pushouts. Thus, we have p1=p2, which means that K2is not unary. This is a contradiction
to the fact that K2is an AHL-process net.
The case (term1, p)⊕(term2, p)≤postK(t) works analogously. Hence, Kis unary.
No forward conflicts. Let us assume that Khas a forward conflict, i. e. there are p∈PKand
t16=t2∈TKwith p∈ •t1∩ •t2.
•Case 1: There is a∈ {1,2}such that t1, t2∈i0
a,T (TKa).
Then we have t0
16=t0
2∈TKawith
i0
a,T (t0
1) = t1and i0
a,T (t0
2) = t2
and there are p1, p2∈PKawith
i0
a,P (p1) = p=i0
a,P (p2) and p1∈ •t0
1, p2∈ •t0
2
because AHL-morphisms preserve pre conditions.
•Case 1.1 p1=p2.
This means that Kahas a forward conflict which contradicts the fact that Kais assumed to
be an AHL-process net.
•Case 1.2 p16=p2.
Since i0
2is injective, this implies that a= 1. Then, i0
1(p1) = p=i0
1(p2) implies x1, x2∈PI
with i1(x1) = p1,i1(x2) = p2and i2(x1) = i2(x2). Moreover, i1(x1) = p1∈ •t0
1means that
p1/∈OUT(K1), and i1(x2) = p2∈ •t0
2means that p2/∈OUT(K1).
Case 1.2.1. There is x1, x2∈OUT(I).
Then by composability of K1and K2w. r. t. (I, i1, i2) it follows that i1(x1)∈OUT(I) or
i1(x2)∈OUT(K1), contradicting the fact that i1(x1), i1(x2)/∈OUT(K1).
Case 1.2.2. There is x1/∈OUT(I), x2∈OUT(I).
By the fact that x2∈OUT(I) and i1(x2)/∈OUT (K1) the composability of K1and K2
w. r. t. (I, i1, i2) implies i2(x2)∈OUT(K2).
Furthermore, the fact that x1/∈OUT (I) means that there is some t0∈TIwith
(term0, x1)≤preI(t0). By the fact that AHL-morphisms preserve pre conditions, we
obtain (term0, i1(x1)) ≤preK1(i1(t0)). This implies that i1(t0) = t0
1because K1is
an AHL-process net which does not have any forward conflicts. Moreover, we have
term0=term1. Using again the fact that AHL-morphisms preserve pre conditions,
we obtain (term1, i2(x1)) ∈preK2(i2(t0)) which means that i2(x1) = i2(x2)/∈OUT (K2),
contradicting the fact that i2(x2)∈OUT(K2).
Case 1.2.3. There is x1∈OUT(I), x2/∈OUT(I).
This case is similar to Case 1.2.2.
Case 1.2.4. There is x1, x2/∈OUT(I). Then we have t0, t0
0∈TIwith (term0, x1)≤preI(t0)
and (term0
0, x2)≤preI(t0
0). Analogously to Case 1.2.2 we obtain that i1(t0) = t0
1and
i1(t0
0) = t0
2, and using the fact that AHL-morphisms preserve pre conditions, we have
i2(x1)≤preK2(i2(t0)) and i2(x1) = i2(x2)≤preK2(i2(t0
0)). Since K2is an AHL-process
net, it does not have any forward conflicts, implying that i2(t0) = i2(t0
0). Thus, we have
t1=i0
1(t0
1) = i0
1(i1(t0)) = i0
2(i2(t0)) = i0
2(i2(t0
0)) = i0
1(i1(t0
0)) = i0
1(t0
2) = t2
which contradicts the fact that t16=t2.
26
A.3 Proof of Fact 4 (Gluing of AHL-Process Nets)
•Case 2: There is t1∈i1(TK1) and t2∈i2(TK2).
Then we have t0
1∈TK1, t0
2∈TK2with
i0
1(t0
1) = t1and i0
2(t0
2) = t2
and since AHL-morphisms preserve pre conditions there are p1∈PK1,p2∈PK2with
i0
1(p1) = p, p1∈ •t0
1and i0
2(p2) = p, p2∈ •t0
2.
By the fact that Kis a pushout object of (PO) this implies a place p0∈PIwith
i1(p0) = p1and i2(p0) = p2.
•Case 2.1: There is p0∈OUT(I).
Due to the fact that p1∈ •t0
1, we have i1(p0)/∈OUT (K1), which by the composability of
(K1, K2) w. r. t. (I, i1, i2) implies that i2(p0)∈OUT (K2) contradicting the fact that i2(p0) =
p2∈ •t0
2.
•Case 2.2: There is p0/∈OUT(I).
This means that there is t0∈TIwith p0∈ •t0. By the fact that i1is an AHL-morphism
which preserves pre conditions we have p1∈ •i1(t0) which together with the fact that p1∈ •t0
1
means that i1(t0) = t0
1because K1has no forward conflicts. Analogously, due to the fact that
also K2has no forward conflict we obtain that i2(t0) = t0
2. Thus, by commutativity of (PO)
we have
t1=i0
1(t0
1) = i0
1(i1(t0)) = i0
2(i2(t0)) = i0
2(t0
2) = t2
which contradicts the assumption that t16=t2.
Hence, all cases lead to a contradiction which means that Khas no forward conflict.
No backward conflicts. The proof that Kdoes not have any backward conflicts works analogously
to the proof concerning the forward conflicts, because AHL-morphisms preserve post as well as pre
conditions, and the definition of the composability consists of corresponding conditions for input
as well as for output places.
Strict partial order. Since <Kis defined as a transitive closure, it suffices to show that e have to
show that <Kis irreflexive. Due to the fact that AHL-morphisms preserve pre and post conditions
we obtain the causal relation of <Kas the transitive closure of
[
a∈{1,2}
{(i0
a(x), i0
a(y)) |x, y ∈PKa]TKa, x <Kay}
This means that elements which are causally related in K1or K2are also causally related in K.
Additionally it is possible that elements in the net Kare related due to the gluing of one or more
elements.
Moreover, if for two interface elements x0, y0∈PI]TIthe images of these elements are causally
related in K, i. e. we have the following Statement (A):
∀x0, y0∈PI]TI:i0
1(i1(x0)) <Ki0
1(i1(y0)) ⇒x0<(i1,i2)y0
We prove this statement because we need it in the following:
Let x0, y0∈PI]TIwith i0
1(i1(x0)) <Ki0
1(i1(y0)). Then there is a∈ {1,2}such that either there is
ia(x0)<Kaia(y0) or there is z0∈PI]TIwith ia(x0)<Kaia(z0) and i0
1(i1(x0)) <Ki0
1(i1(z0)) <K
i0
1(i1(y0)). This recursively leads to the fact that x0<(i1,i2)y0because the induced causal relation
is transitive.
Let us now assume that <Kis not irreflexive, i. e. there exists x∈PK]TKs.t. x <Kx.
•Case 1. There is no element z∈PI]TIwith x <Ki0
1(i1(z)) <Kx.
Then there is a∈ {1,2}and y∈PKa]TKas.t. i0
a(y) = x. Since there are no images of
interface elements in the causal relation between xand x, the causal relation is completely
obtained from causal relations in Ka, i. e. we have y <Kay. This contradicts the fact that
<Kais irreflexive because Kais an AHL-process net.
27
A Detailed Proofs
•Case 2. There is an element z∈PI]TIwith x <Ki0
1(i1(z)) <Kx.
Due to the transitivity of <Kthere is i0
1(i1(z)) <Ki0
1(i1(z)) because
i0
1(i1(z)) <Kx <Ki0
1(i1(z)).
By statement (A) this implies z <(i1,i2)z, contradicting the fact that by the composability of
K1and K2w. r. t. (I, i1, i2) the induced causal relation <(i1,i2)is irreflexive.
Hence, <Kis irreflexive.
Only If. Given the pushout diagram (PO) in the category AHLPNets. By Lemma 2 (PO) is also a
pushout in the category AHLNets. We have to show that (K1, K2) are composable w. r. t. (I, i1, i2).
No cycles. Let x, y ∈PI]TIwith x≺(i1,i2)y.
Then by the definition of ≺(i1,i2)there is
i1(x)<K1i1(y) or i2(x)<K2i2(y)
and by the fact that i0
1◦i1=i0
2◦i2, we have
i0
1◦i1(x)<Ki0
1◦i1(y)
because AHL-morphisms preserve pre and post conditions.
Since <Kis transitive, we have also for the transitive closure <(i1,i2)of ≺(i1,i2), that x <(i1,i2)y
implies i0
1◦i1(x)<Ki0
1◦i1(y).
Now, let us assume that <Kis not irreflexive, i. e. there is x∈PI]TIwith x <(i1,i2)x. Then
there is
i0
1◦i1(x)<Ki0
1◦i1(x)
contradicting the fact that <Kis irreflexive. Hence, <(i1,i2)is irreflexive.
Non-injective gluing. We have to show that for all p16=p2∈IN(I) with i2(p1) = i2(p2) there is
i1(p1)∈IN(K1) or i1(p2)∈IN(K1).
So let p16=p2∈IN(I) with i2(p1) = i2(p2) and let us assume that i1(p1)/∈IN(K1) and
i1(p2)/∈IN(K2). This means that there are t1, t2∈TK1and terms term1, term2∈TΣ(X) with
(term1, i1(p1)) ≤postK1(t1) and (term2, i1(p2)) ≤postK1(t2).
From preservation of post conditions by AHL-morphisms it follows that (term1, i0
1(i1(p1))) ≤
postK(i0
1(t1)) and (term2, i0
1(i1(p2))) ≤postK(i0
1(t2)). Moreover, by commutativity of pushout
(PO) we have
i0
1(i1(p1)) = i0
2(i2(p1)) = i0
2(i2(p2)) = i0
1(i1(p2))
We distinguish the following two cases.
Case 1. There is i0
1(t1) = i0
1(t2).
Then we have (term1, i0
1(i1(p1))) ⊕(term2, i0
1(i1(p1))) ≤postK(i0
1(t1)), contradicting unarity
of AHL-process net K.
Case 2. There is i0
1(t1)6=i0
1(t2).
Then (term1, i0
1(i1(p1))) ≤postK(i0
1(t1)) and (term1, i0
1(i1(p1))) ≤postK(i0
1(t2)) means that
AHL-process net Khas a backward conflict, which is also a contradiction.
Thus, we have i1(p1)∈IN(K1) or i1(p2)∈IN(K1).
The fact that for all p16=p2∈OUT(I) with i2(p1) = i2(p2) there is i1(p1)∈OUT (K1) or i1(p2)∈
OUT(K1) follows analogously because AHL-morphisms preserve pre as well as post conditions and
AHL-process net Kalso does not have any forward conflicts.
28
A.3 Proof of Fact 4 (Gluing of AHL-Process Nets)
No conflicts. We have to show that ∀x∈IN(I) : i1(x)/∈IN(K1)⇒i2(x)∈IN(K2). Let x∈IN(I)
with i1(x)/∈IN(K1) and let us assume that there is i2(x)/∈IN(K2).
Then i1(x) and i2(x) both are in the post domain of transitions, i. e. there are t1∈TK1and
t2∈TK2such that i1(x)∈t1•and i2(x)∈t2•. Since AHL-morphisms preserve post conditions
there is
i0
1(i1(x)) ∈i0
1(t1)•and i0
2(i2(x)) ∈i0
1(t2)•
and due to the fact that (PO) commutes there is i0
1(i1(x)) = i0
2(i2(x)) which implies
i0
1(i1(x)) ∈i0
1(t1)• ∩i0
2(t2)•.
Since Kis an AHL-process net it has no backward conflict implying that i0
1(t1) = i0
2(t2). So due
to the pushout property there is t0∈TIwith
i1(t0) = t1and i2(t0) = t2
Then by the fact that i1(x)∈i1(t0)•together with the fact that i1is an AHL-morphism which
preserves post domains it follows that x∈t0•. This contradicts the fact that x∈IN(I). Hence,
there is i2(x)∈IN(K2).
Now, we show that ∀x∈OUT(I) : i1(x)/∈OUT (K1)⇒i2(x)∈OUT(K2). Let x∈OUT(I) with
i1(x)/∈OUT(K1) and let us assume that there is i2(x)/∈OUT(K2).
Then i1(x) and i2(x) both are in the pre domain of transitions, i. e. there are t1∈TK1and t2∈TK2
such that i1(x)∈ •t1and i2(x)∈ •t2. Since AHL-morphisms preserve pre conditions there is
i0
1(i1(x)) ∈ •i0
1(t1) and i0
2(i2(x)) ∈ •i0
1(t2)
and by commutativity of (PO) we have i0
1(i1(x)) = i0
2(i2(x)) which implies
i0
1(i1(x)) ∈ •i0
1(t1)∩ •i0
2(t2)
Since Kis an AHL-process net it has no forward conflict implying that i0
1(t1) = i0
2(t2). So due to
the pushout property there is t0∈TIwith
i1(t0) = t1and i2(t0) = t2
Then by the fact that i1(x)∈ •i1(t0) together with the fact that i1is an AHL-morphism which
preserves pre domains it follows that x∈ •t0. This contradicts the fact that x∈OUT(I). Hence,
there is i2(x)∈OUT(K2).
Extension to Processes.
Given the pushout (PO) and additional AHL-morphisms mp1:K1→AN and mp2:K2→AN with
mp1◦i1=mp2◦i2.
Ii1//
i2
(PO)
K1
i0
1
mp1
K2i0
2
//
mp2,,
K
mp
D
D
D
D
""
D
D
D
AN
Then we also have a morphism mp0:I→AN defined by mp0:= mp1◦i1=mp2◦i2. Moreover the
pushout property of (PO) implies a unique morphism mp :K→AN such that (PO) is also a pushout
in the slice category AHLNets \AN. As shown above the composability of K1and K2w. r. t. (I, i1, i2)
implies that Kis an AHL-process net. Hence, mp :K→AN is an AHL-process which implies that
(PO) is also pushout in the full subcategory Proc(AN)⊆AHLNets \AN of AHL-processes.
29
A Detailed Proofs
A.4 Proof of Theorem 1 (Direct Transformation of AHL-Process Nets)
Given a production for AHL-process nets %:Ll
←Ir
→Rand an AHL-process net Ktogether with a
morphism m:L→K. Then the direct transformation of AHL-process nets with pushouts (1) and (2)
in AHLPNets exists iff %satisfies the transformation condition for AHL-process nets under m.
Extension to processes. In order to extend this construction for AHL-processes in the category
Proc(AN) one additionally requires AHL-morphisms mp :K→AN and rp :R→AN with mp◦m◦l=
rp ◦r. Then by composition of AHL-morphisms we obtain an AHL-process cp =mp ◦d:C→AN
and the pushout (1) in AHLPNets is also a pushout of mp ◦mand cp in Proc(AN). Moreover, the
pushout (2) in AHLPNets provides a unique morphism mp0:K0→AN such that mp0is pushout of
cp and rp in Proc(AN) according to Fact 4.
L
(1)
m
I
c
l
oor//R
n
(2)
K C
d
ooe//K0
Proof. First, we prove the following lemma which states the equivalence of the gluing relation for a given
production and match and the induced causal relation of the right-hand side of the production and the
context net in AHLNets.
Lemma 3 (Gluing Relation Lemma).Given a production for AHL-process nets %:Ll
←Ir
→R, a match
m:L→Kwhere Kis an AHL-process net, and pushout (1) in AHLNets.
Then the gluing relation <(%,m)is exactly the induced causal relation of Cand Rw. r. t. (I, c, r), i. e.
<(%,m)=<(c,r).
L
m
(1)
I
l
oo
c
r//R
K C
d
oo
Proof. We define a relation ≺C⊆(PC×TC)](TC×PC) as follows:
≺C={(p, t)∈PC×TC|p∈ •t}∪{(t, p)∈TC×PC|p∈t•}
The relation ≺Cdescribes the direct causal relationship of the elements in C, i. e. the causal relation <C
is the transitive closure of ≺C. We show that for the relation ≺(K,m)in Def. 14 we have ≺(K,m)=≺C,
by showing that there is a subset relation in both directions.
Direction 1 (≺(K,m)⊆≺C). Let x, y ∈PK](TK\mT(TL)) with x≺(K,m)y. Due to the bipartite
structure of Petri nets there are two possible cases:
•Case 1. There is x∈PKand y∈TK\mT(TL).
Due to the construction of Cthere is y∈TC. Furthermore there is term ∈TOP (X)typeK(x)
such that
(term, x)≤preK(y)⇔(term, x)≤preK|TC(y)
⇔(term, x)≤preC(y)
and hence x≺Cy.
•Case 2. There is x∈TK\mT(TL) and y∈PK.
In this case we have x∈TCand there is term ∈TOP (X)typeK(x)such that
(term, y)≤postK(x)⇔(term, y)≤postK|TC(x)
⇔(term, y)≤postC(x)
and hence x≺Cy.
30
A.4 Proof of Theorem 1 (Direct Transformation of AHL-Process Nets)
Direction 2 (≺C⊆≺(K,m)). Let x, y ∈PC]TCwith x≺Cy. Again we distinguish the two possible
cases:
Case 1. There is x∈PCand y∈TC.
Then there is term ∈TOP (X)typeC(x)such that (term, x)≤preC(y). Since AHL-morphisms
preserve pre conditions and dis an inclusion we have
(term, x)≤preC(y)⇔(term, x)≤d⊕◦preC(y)
⇔(term, x)≤preK(d(y))
⇔(term, x)≤preK(y)
So the fact that TC=TK\mT(TL) implies x≺(K,m)y.
Case 2. There is x∈TCand y∈PC.
Then there is term ∈TOP (X)typeC(x)such that (term, x)≤postC(y). Since AHL-morphisms
preserve not only pre but also post conditions we obtain analogously to Case 1 that x≺(K,m)y.
So we have that ≺(K,m)=≺Cand since <(K,m)is the transitive closure of ≺(K,m)and <Cis the
transitive closure of ≺Cit follows that <(K,m)=<C.
Furthermore we can use the inclusion dto obtain from the commutativity of (1) that
m◦l(x) = d◦c(x) = c(x).
So let ≺(c,r)⊆(PI×TI)](TI×PI) be the relation defined by
≺(c,r)={(x, y)|c(x)<Cc(y)∨r(x)<Rr(y)}
then we have
≺(%,m)={(x, y)∈(PI×TI)](TI×PI)|m◦l(x)<(K,m)m◦l(y)∨r(x)<Rr(y)}
={(x, y)∈(PI×TI)](TI×PI)|c(x)<Cc(y)∨r(x)<Rr(y)}
={(x, y)∈(PI×TI)](TI×PI)|r(x)<Rr(y)∨c(x)<Cc(y)}
=≺(r,c)
and since <(%,m)is the transitive closure of ≺(%,m)and <(r,c)is the transitive closure of ≺(r,c)we
have <(%,m)=<(r,c).
Now we show that the pushouts (1) and (2) below exist in AHLPNets if and only if the production
punder msatisfies the transformation condition for AHL-process nets.
L
m
(1)
I
l
oor//
c
(2)
R
n
K C
d
ooe//K0
If. Given production %:Ll
←Ir
→Rsatisfying the transformation condition for AHL-processes under
match m. Since this implies that %satisfies the the gluing condition for AHL-nets by Theorem 3 there
exist pushouts (1) and (2) in AHLNets. We have to show that (1) and (2) are also pushouts in the
category AHLPNets of AHL-process nets.
Pushout (1). From AHL-process net Kand AHL-morphism d:C→Kit follows by Lemma 1
that also Cis an AHL-process net. So we have that all objects and morphisms in pushout (1)
are in the full subcategory AHLPNets ⊆AHLNets which means that (1) is also a pushout in
AHLPNets.
Pushout (2). We have to show that (R, C) are composable w. r. t. (I, r, c) (see Def. 13).
31
A Detailed Proofs
No cycles. The fact that the gluing relation <(%,m)of %und mis a strict partial order implies
that the induced causal relation <(r,c)is a strict partial order because by Lemma 3 there is
x <(%,m)y⇔x <(r,c)y.
Non-injective gluing. From pushout (1) in AHLPNets of morphisms land cit follows by
Fact 4 that (L, C) are composable w. r. t. (I, l, c).
Let p16=p2∈IN(I) with c(p1) = c(p2). Then we have
m◦l(p1) = d◦c(p1) = d◦c(p2) = m◦l(p2)
which by the fact that %and msatisfy the transformation condition implies that r(p1)∈
IN(R) or r(p2)∈IN(R).
Analogously, we obtain for p16=p2∈OUT (I) with c(p1) = c(p2) that there is r(p1)∈
OUT(R) or r(p2)∈OUT(R).
No conflicts. Let x∈IN(I) and c(x)/∈IN(C) then by the composability of (L, C) w. r. t. (I, l, c)
follows that l(x)∈IN(L). The fact that c(x)/∈IN(C) implies t∈TCwith c(x)∈t•and
d◦c(x)∈d(t)•because AHL-morphisms preserve post conditions. Due to the commutativity
of (1) there is m◦l(x) = d◦c(x) which means that m◦l(x)/∈IN(K) because m◦l(x)∈d(t)•.
So there is x∈InP and the fact that production %and match msatisfy the transformation
condition for AHL-processes implies that r(x)∈IN(R).
Now, let x∈OUT(I) and c(x)/∈OUT(C) then by the composability of (L, C) w. r. t. (I, l, c)
follows that l(x)∈OUT(L). The fact that c(x)/∈OUT(C) implies t∈TCwith c(x)∈ •tand
d◦c(x)∈ •d(t) because AHL-morphisms preserve pre conditions. Due to the commutativity of
(1) there is m◦l(x) = d◦c(x) which means that m◦l(x)/∈OUT(K) because m◦l(x)∈ •d(t).
So there is x∈OutP and the fact that production %and match msatisfy the transformation
condition for AHL-processes implies that r(x)∈OUT(R).
Thus, (R, C) are composable w. r. t. (I, r, c) leading to the existence of pushout (2) in AHLPNets.
Only If. Given pushouts (1) and (2) in AHLPNets. We have to show that the transformation condition
for AHL-process nets (see Def. 15) is satisfied by production %under match m.
Gluing condition. By Lemma 2 pushouts (1) and (2) in AHLPNets are also pushouts in AHLNets
which by Fact 3 implies that the gluing condition is satisfied.
No cycles. By Fact 4 pushout (2) in AHLPNets implies that (R, C) are composable w. r. t. (I, r, c)
which means that <(r,c)is a strict partial order. Due to Lemma 3 we know that there is <(r,c)=<(%,m)
which means that also <(%,m)is a strict partial order.
Non-injective gluing. Let p16=p2∈IN(I) with m◦l(p1) = m◦l(p2). Since lis injective,
p16=p2implies l(p1)6=l(p2). Then due to the fact that (1) is a pushout, there is p∈PCwith
c(p1) = p=c(p2). Thus, by composability of (R, C) w. r. t. (I, r, c) it follows that r(p1)∈IN(R)
or r(p2)∈IN(R).
Analogously, we obtain for p16=p2∈OUT(I) with m◦l(p1) = m◦l(p2) that r(p1)∈OUT(R) or
r(p2)∈OUT(R).
No conflicts. Let x∈InP which means that x∈IN(I) with l(x)∈IN(L) and m◦l(x)/∈IN(K).
The fact that m◦l(x)/∈IN(K) implies that there is t∈TKwith m◦l(x)∈t•.
Let us assume that there is t0∈TLwith mT(t0) = t. Then from the fact that mis an AHL-
morphism, it follows that l(x)∈t0•because AHL-morphisms preserve post conditions. This
contradicts the fact that l(x)∈IN(K) and thus t /∈mT(TL) which means that t∈TK\mT(TL).
Then by the construction of pushout complement TCin AHLNets it follows that t∈TC.
Moreover, we have c(x) = m◦l(x)∈t•which means that c(x)/∈IN(C). This implies that r(x)∈
IN(R) due to the composability of (R, C) w. r. t. (I, r, c) given by pushout (2) in AHLPNets and
Fact 4.
Now, let x∈OutP which means that x∈OUT (I) with l(x)∈OUT(L) and m◦l(x)/∈OUT (K).
Then m◦l(x)/∈OUT(K) implies that there is t∈TKwith m◦l(x)∈ •t. Again, the assumption
32
A.5 Proof of Theorem 2 (Extension of AHL-Process based on AHL-Net Transformation)
that t0∈TLwith mT(t0) = tleads to a contradiction which means that t∈TK\mT(TL). Then
by the construction of TCfollows that t∈TCand we have c(x) = m◦l(x)∈ •twhich means that
c(x)/∈OUT(C) and hence r(x)∈OUT(R) by composability of (R, C) w. r. t. (I, r, c).
Extension to Processes.
Given pushouts (1) and (2) in AHLPNets and additional morphisms mp :K→AN and rp :R→
AN with mp ◦m◦l=rp ◦r.
L
m(1)
I
l
oor//
c(2)
R
nrp
K
mp --
C
d
ooe//K0
AN
Since L,Cand Iare AHL-process nets we obtain AHL-processes by composition of AHL-morphisms
lp := mp ◦m:L→AN ,cp := mp ◦d:C→AN and ip := mp ◦m◦l=mp ◦d◦c:I→AN such that
(1) is a commuting diagram in Proc(AN).
By Lemma 2 pushout (1) in AHLPNets is also a pushout in AHLNets and thus by construction
of pushouts in slice categories it is also a pushout in AHLNets \AN . Hence, due to the fact that lp,
cp,ip and mp are AHL-processes we have that (1) is a pushout in the full subcategory Proc(AN)⊆
AHLNets \AN .
Finally, we have
cp ◦c=mp ◦d◦c=mp ◦m◦l=rp ◦r
which by Fact 4 implies a unique morphism mp0:K0→AN such that (2) is also a pushout in Proc(AN).
A.5 Proof of Theorem 2 (Extension of AHL-Process based on AHL-Net
Transformation)
Given an AHL-net AN, an AHL-process mp :K→AN and a direct transformation AN %,m
⇒AN0with
pushouts (1) and (2) in AHLNets as depicted in Figure 8. There exists an extension mp0:K→AN0
of mp if and only if mp and %, m satisfy the extension condition.
Proof. If. Let mp and p, m satisfy the extension condition. We define mp0:K→AN0as mp0=
f−1◦mp. Since fis injective, for the well-definedness of mp0it suffices to show that for all elements
xin in Kthere exists an element yin AN0with f(y) = mp(x). Let p∈PK.
Case 1. There exists x∈PLwith m(x) = mp(p).
Then there is x∈PP and since mp and %, m satisfy the extension condition, we have x0∈PI
with l(x0) = x. Thus, we have y=k(x0) with f(y) = f(k(x0)) = m(l(x0)) = m(x) = mp(p).
Case 2. There exists no x∈PLwith m(x) = mp(p).
Then by construction of pushout complements in AHLNets there exists y∈AN0with
f(y) = mp(p).
The proof for the existence of the transitions works analogously. Injectivitiy of fimplies that we
have a well-defined morphism mp0:K→AN0with f◦mp0=f◦f−1◦mp =mp, and we obtain
the required extension mp0:K→AN0by composition mp0=g◦mp0.
Only If. Let mp0:K→AN0be the extension of mp, i. e. there is mp0:K→AN0with f◦mp0=mp
and g◦mp0=mp0. We have to show that all process points are gluing points. So, let x∈PP and let
w. l. o. g. x∈PL. Then there is p∈PKwith mp(p) = m(x). Moreover, we have y=mp0(p)∈PAN0
with f(y) = f(mp0(p)) = mp(p) = m(x). Since (1) is pushout in AHLNets, this implies that
there is x0∈PIwith k(x0) = yand l(x0) = x. Hence, we have x∈GP.
33
A Detailed Proofs
A.6 Proof of Theorem 3 (Process Evolution based on Action Evolution)
Given an action evolution AN %,m
=⇒AN0via production %:Ll
←Ir
→R, and a process mp :K→AN.
Then there exists a production (%+, %) for AHL-processes and a direct transformation mp (%+,%)
=⇒mp0as
depicted in Figure 10a that realizes the changes described by %on all occurrences in the process mp.
Construction: Let (mi:L→K)i∈I be the class of all matches mi:L→Kwith mp ◦mi=m.
1. The production for AHL-process nets %+:L+l+
←I+r+
→R+is defined as componentwise coproduct
in AHLPNets:
•X+=`i∈I Xwith injections ιX
i:X→X+for X∈ {L, I, R},
•x+=`i∈I xfor x∈ {l, r}
2. The processes mpX:X+→Xfor X∈ {L, I, R}are the unique induced morphisms with mpX◦
ιX
i=idXfor all i∈ I (see Figure 10b).
3. The match m+:L+→Kis the unique induced morphism with m+◦ιL
i=mifor all i∈ I.
4. K0and K0are constructed as direct AHL-process net transformation in the back of Figure 10a.
5. mp0:K0→AN0is defined as mp0=f−1◦mp ◦f0, and mp0:K0→AN0is induced by the right
pushout in the back of Figure 10a.
L+
m+
mpL
%%
K
K
K
K
K
KI+
l+
oor+//
mpI
%%
K
K
K
K
K
KR+
mpR
%%
L
L
L
L
L
L
L
mi
yyttttttm
I
l
oor//
k
R
n
K
mp $$
I
I
I
I
IK0
mp0%%
J
J
J
J
J
f0
oog0//K0
mp0%%
J
J
J
J
J
AN AN0
f
oog//AN0
(a) Process Evolution
X
ιX
i
idX
3
3
3
3
3
3
3
3
3
3
3
3
3
X+
mpX//X
(b) Induced Pro-
cess
Figure 12: Process evolution based on action evolution
Proof. We have to show that the construction given above is well-defined.
1. Since by Lemma 4 below the category AHLPNets has coproducts, we can construct the coproducts
X+=`i∈I Xfor X∈ {L, I, R}and x+=`i∈I xfor x∈ {l, r}in AHLPNets, and obtain
coproduct injections ιX
i:X→X+for X∈ {L, I, R}and i∈ I. Then %+is a production for
AHL-process nets because L+,I+and R+are AHL-process nets.
2. The processes mpX:X+→Xfor X∈ {L, I, R}are obtained as unique morphisms with mpX◦
ιX
i=idXfor all i∈ I induced by the universal property of coproducts L+,I+and R+. Note
that mpXare retractions which in the case of AHL-morphisms means that mpX,P and mpX,T are
surjective.
It remains to show that (%+, %) is a production for AHL-processes, i. e. that the top faces in Fig. 12a
commute. By morphism l:I→Land coproduct I+of (I)i∈I there exists a unique morphism
u:I+→Lsuch that for all i∈ I there is u◦ιI
i=l. So from l◦mpI◦ιI
i=l◦idI=l(see Fig. 12b)
it follows that l◦mpI=uby uniqueness of u. Hence, by compatibility of l+and land Fig. 12b
we have
mpL◦l+◦ιI
i=mpL◦ιL
i◦l=idL◦l=l
By uniqueness of uthis implies mpL◦l+=u=l◦mpI. The commutativity mpR◦r+=r◦mpI
can be shown analogously. Hence, the top faces in Fig. 12a commute.
34
A.6 Proof of Theorem 3 (Process Evolution based on Action Evolution)
3. The match m+:L+→Kwith m+◦ιL
i=mifor all i∈ I is uniquely induced by coproduct L+.
Moreover, (m+, m) is a AHLProcs-morphism because mp ◦m+=mp ◦mi◦mpL=m◦mpL.
4. The existence of the direct transformation of AHL-process nets with pushouts (1) and (2) is shown
in Lemma 5 below.
L+
(1)
m+
I+
k+
l+
oor+//R+
n+
(2)
K K0
f0
oog0//K0
5. For the well-definedness of mp0as mp0=f−1◦mp ◦f0we have to show that for all elements
x∈K0there is a unique y∈AN0with mp ◦f0(x) = f(y). Since %is a production for action
evolution, there is PL=lP(PI) which means that lPis a bijection, i. e. an isomorphism in Sets.
This implies that also l+
Pis a bijection, and by the pushouts in the left front and back of the cube
in Fig. 12a also fPand f0
Pare bijections. Thus, mp0,P =f−1
P◦mpP◦f0
Pis well-defined. It remains
to show that also mp0,T is well-defined. Let t∈TK0. In order to show the existence of y∈TAN0
with mp ◦f0(t) = f(y), we distinguish the following two cases:
Case 1. There is f0(t)∈m+(TL+).
This means that there is t0∈TL+with f0(t) = m+(t0). By pushout (1) we obtain t0∈TI+
with l+(t0) = t0and k+(t0) = t. Then for k(mpI(t0)) we have
f(k(mpI(t0))) = m(l(mpI(t0))) = m(mpL(l+(t0)))
=mp(m+(l+(t0))) = mp(m+(t0))
=mp(f0(t))
Case 2. There is f0(t)/∈m+(TL+).
Let us assume that there is t0∈TLand i∈ I such that mi(t0) = f0(t). Then we have
m+(ιL
i(t0)) = mi(t0) = f0(t) which is a contradiction. Thus, there is also f0(t)/∈mi(TL) for
all i∈ I. Since (mi)i∈I are all matches mi:L→Kwith mp ◦mi=mit follows that
m(t%)6=mp(f0(t)) which means that mp(f0(t)) /∈m(TL). So by the pushout in the left front
of Fig. 12a there is y∈TAN0with f(y) = mp(f0(t)).
The required uniqueness follows from injectivity of fwhich is implied by injectivity of land the
pushout in the left front of Fig. 12a. Hence, mp0is well-defined and we have
f◦mp0=f◦f−1◦mp ◦f0=mp ◦f0
and
mp0◦k+=f−1◦mp ◦f0◦k+=f−1◦mp ◦m+◦l+
=f−1◦m◦mpL◦l+=f−1◦m◦l◦mpI
=f−1◦f◦k◦mpI=k◦mpI
which means that the left cube in Fig. 12a commutes.
Moreover, we have
g◦mp0◦k+=g◦k◦mpI=n◦r◦mpI
=n◦mpR◦r+
which by pushout (2) implies a unique morphism mp0:K0→AN0such that the right cube in
Fig. 12a commutes.
35
A Detailed Proofs
Lemma 4 (Coproduct of AHL-Process Nets).The categories AHLNets and AHLPNets have coprod-
ucts that can be constructed componentwise as disjoint unions in Sets. This means, given AHL-(process)
nets (Ki)i∈I, then there exists an AHL-(process) net Ktogether with injections ιi:Ki→Ksuch that
Kis the coproduct of (Ki)i∈I , written K=`i∈I Ki, satisfying the following universal property: For
all AHL-(process) nets K0and AHL-morphisms (fi:Ki→K0)i∈I there exists a unique morphism
f:K→K0such that f◦ιi=fifor all i∈ I.
Ki
ιi//
fi!!
B
B
B
B
B
B
BK
f
K0
Proof. Coproduct in AHLNets. First, we show that AHLNets has coproducts.
Let (Ki)i∈I be AHL-nets with Ki= (Σ, Pi, Ti, prei, posti, condi, typei, A). We construct the
coproducts P=`i∈I Piwith injections (ιP
i:Pi→P)i∈I and T=`i∈I Tiwith injections
(ιT
i:Ti→T)i∈I in Sets, given by the respective disjoint unions. Then, by the universal property
of coproducts in Sets we obtain unique functions cond :T→ Pfin(Eqns(Σ; X)), pre, post :T→
(TΣ(X)⊗P)⊕, and type :P→S, such that diagrams (1), (2) and (3) below commute for all i∈ I.
Ti
condi
ttiiiiiiiiiiiiiii
ιT
i
prei//
posti//(TΣ(X)⊗Pi)⊕
(id⊗ιP
i)⊕
Pi
ιP
i
typei
''
O
O
O
O
O
O
O
O
O
O
O
O
Pfin(Eqns(Σ; X)) (1) (2) (3)S
T
cond
jjUUUUUUUUUUUUUUUpre //
post //(TΣ(X)⊗P)⊕P
type
77
o
o
o
o
o
o
o
o
o
o
o
o
We define an AHL-net K= (Σ, P, T, pre, post, cond, type, A) and AHL-morphisms (ιi:Ki→K)i∈I
by ιi= (ιP
i, ιT
i). The well-definedness follows from commutativity of diagrams (1)-(3) above.
Now, in order to show the universal property for Kand (ιi)i∈I, let
K0= (Σ, P0, T0, pre0, post0, cond0, type0, A)
be an AHL-net and (fi:Ki→K0)i∈I AHL-morphisms. Using the universal property of Pand
Tin Sets, we obtain unique functions fP:P→P0and fT:T→T0, allowing us to define an
AHL-morphism f= (fP, fT) : K→K0. It remains to show that fis well-defined, i. e. we have to
show that the diagrams (4)-(6) below commute.
T
cond
ttiiiiiiiiiiiiiii
fT
pre //
post //(TΣ(X)⊗P)⊕
(id⊗fP)⊕
P
fP
type
''
O
O
O
O
O
O
O
O
O
O
O
O
Pfin(Eqns(Σ; X)) (4) (5) (6)S
T0
cond0
jjUUUUUUUUUUUUUUpre0
//
post0//(TΣ(X)⊗P0)⊕P0type0
77
o
o
o
o
o
o
o
o
o
o
o
o
Considering diagram (4) we have
cond0◦fT◦ιT
i=cond0◦fi,T =condi
which by uniqueness of cond implies that cond0◦fT=cond, i. e. diagram (4), and analogously
diagram (6), commutes.
Let us now consider the pre-component of (5). By coproduct Tof (Ti)i∈I there is a unique
morphism g:T→(TΣ(X)⊗P0)⊕such that g◦ιT
i= (id ⊗fP)⊕◦(id ⊗ιP
i)⊕◦preifor all i∈ I.
Then, by commutativity of (2) we have for all i∈ I:
(id ⊗fP)⊕◦pre ◦ιT
i= (id ⊗fP)⊕◦(id ⊗ιP
i)⊕ ◦prei
36
A.6 Proof of Theorem 3 (Process Evolution based on Action Evolution)
implying that g= (id ⊗fP)⊕◦pre by uniqueness of g. Moreover, we have for all i∈ I:
pre0◦fT◦ιT
i=pre0◦fi,T = (id ⊗fi,P )⊕◦prei
= (id ⊗(fP◦ιP
i))⊕◦prei= (id ⊗fP)⊕◦(id ⊗ιP
i)⊕◦prei
which by uniqueness of gimplies that pre0◦fT=g= (id ⊗fP)⊕◦pre. The proof for the
post-component works analogously.
Hence, fis a well-defined AHL-morphism. The uniqueness of ffollows from uniqueness of its
components fPand fT.
Coproduct in AHLPNets. Let now (Ki)i∈I be AHL-process nets. We show that the coproduct
K=`i∈I Kiin AHLNets is also coproduct in AHLPNets. Analogously as in Lemma 2 it can
be shown that coproducts in AHLPNets are also coproducts in AHLNets. Therefore, it suffices
to show that the coproduct Kin AHLNets is an AHL-process net. The conditions 1-4 in Def. 3 of
AHL-process nets correspond only to connections between places and transitions. Since Kconsists
only of disjoint copies of the AHL-process nets Kiwhich satisfy the conditions in Def. 3, also K
satisfies these conditions, because there are no new connections between places and transitions
which could violate the condition. Hence, Kis an AHL-process net.
Lemma 5 (Process Net Evolution based on Action Evolution).Given an action evolution AN %,m
=⇒AN0
via production %:Ll
←Ir
→R, and a process mp :K→AN. Then the production %+:L+l+
←I+r+
→R+
and match m+as defined in Theorem 3 are applicable, i. e. the direct transformation of AHL-process
nets with pushouts (1) and (2) below exist.
L+
(1)
m+
I+
k+
l+
oor+//R+
n+
(2)
K K0
f0
oog0//K0
Proof. For the existence of the direct transformation of AHL-process nets we have to show according to
Theorem 1 that %+and m+satisfy the transformation conditions 1-4 (see Def. 15):
1. (Gluing Condition) For satisfaction of the gluing condition we have to show that all identification
and dangling points are gluing points (see Def. 10). Let us first consider the places, i. e. let
p∈(IP ∩PL+)∪DP . There is mpL(p)∈PL, and since %is a production for action evolution,
there is p0∈PIwith l(p0) = mpL(p). By construction of L+as coproduct, there is some i∈ I such
that p=ιL
i(mpL(p)). Hence, we have ιI
i(p0)∈PI+with l+(ιI
i(p0)) = ιL
i(l(p0)) = ιL
i(mpL(p)) = p
which means p∈GP.
Considering the transitions, let us assume t∈IP ∩TL+. Then there is t0∈TL+with t6=t0and
m+(t) = m+(t0). Since %is a production for action evolution, we have mpL(t) = t%=mpL(t0) and
there are i, j ∈ I with ιL
i(t%) = tand ιL
j(t%) = t0. We show that mi=mj. First, we have
mi(t%) = m+(ιL
i(t%)) = m+(t) = m+(t0) = m+(ιL
j(t%)) = mj(t%)
which means that mi,T =mj,T .
Now, let p∈PL. By production %for action evolution, we have p∈ •t%∪t%•. W. l. o. g. let p∈ •t%
which means that there is term ∈TΣ(X) such that (term, p)≤preL(t%). Let us assume that
mi(p) = pi6=pj=mj(p). Since AHL-morphisms preserve pre conditions, we have (term, pi)⊕
(term, pj)≤preK(mi(t%)) and, moreover, there is p0∈PLwith mi(p0) = pjand (term, p0)≤
preL(t%). From pi6=pjit follows that p06=pwhich means that we have (term, p)⊕(term, p0)≤
preL(t%), contradicting the fact that %is a production for action evolution. Thus, we also have
mi,P =mj,P , implying that we have similar matches mi=mjand therefore i=j. So we have
t=ιL
i(t%) = ιL
j(t%) = t0, contradicting the assumption t6=t0by t∈IP ∩TL+. Hence, m+
Tis
injective which means that there are no transitions that are identification points.
37
A Detailed Proofs
2. (No Cycles) We have to show that the gluing relation <(%+,m+)defined as transitive closure of
{(x, y)∈(PI+×TI+)](TI+×PI+)|m+◦l+(x)<(K,m+)m+◦l+(y)∨r+(x)<Rr+(y)}
is irreflexive. In order to show this we first show in the following that for all x, y ∈PI+]TI+with
x <(%+,m+)yit follows that m+◦l+(x)<Km+◦l+(y).
So let us first consider the relation <(K,m+), defined as transitive closure of
{(x, y)∈(PK×(TK\m+
T(TL+))) ]((TK\m+
T(TL+)) ×PK)|x∈ •y}
Clearly, <(K,m+)is a subset of <K, containing only those relations between elements in Kwhich
are not or not only related via an occurrence mi(t%) for some i∈ I. So for p1, p2∈PI+we have
that m+◦l+(p1)<(K,m+)m+◦l+(p2) implies m+◦l+(p1)<Km+◦l+(p2).
It remains to show that for p1, p2∈PI+with r+(p1)<R+r+(p2) there is m+◦l+(p1)<Km+◦
l+(p2). For this purpose we first show that for places p1, p2∈PIwith r(p1)<Rr(p2) it follows
that l(p1)<Ll(p2).
So let p1, p2∈PIwith r(p1)<Rr(p2). Then there has to be at least one transition with r(p1)
in its pre domain as well as a transition with r(p2) in its post domain which means that we
have r(p1)/∈OUT(R) and r(p2)/∈IN(R). By contraposition of item 4 in Def. 20 we obtain
l(p1)/∈OUT(L) and l(p2)/∈IN(L), and due to the fact that all places in Lare in the environment
of one transition t%it follows that l(p1)<Ll(p2).
Since I+,R+and L+contain only disjoint copies of I,Rand L, respectively, we also have that
for p1, p2∈PI+with r+(p1)<R+r+(p2) it follows that l+(p1)<L+l+(p2).
Furthermore, by the fact that AHL-morphisms preserve pre and post conditions, for all t∈TI+
and p∈PI+it holds that r+(p)∈ •r+(t)∪r+(t)•implies p∈ •t∪t•which in turn implies
l+(p)∈ •l+(t)∪l+(t)•. Thus, by transitivity of <R+and <L+it follows for all x, y ∈PI+]TI+
that r+(x)<R+r+(y) implies l+(x)<L+l+(y). Moreover, due to the preservation of pre and post
conditions by AHL-morphisms, we obtain m+◦l+(x)<Km+◦l+(y).
Now, since x <(%+,m+)yimplies m+◦l+(x)<(K,m)m+◦l+(y) or r+(x)<R+r+(y), from the facts
that we have shown it follows that x <(%+,m+)yimplies m+◦l+(x)<Km+◦l+(y).
So let us now assume x∈PI+]TI+with x <(%+,m+)x. Then we have m+◦l+(x)<Km+◦l+(x),
contradicting the fact that <Kis irreflexive. Hence, <(%+,m+)is irreflexive which means that it is
a strict partial order.
3. (Non-Injective Gluing) Let p16=p2∈IN(I+) with m+◦l+(p1) = m+◦l+(p2). We have to show
that r+(p1)∈IN(R+) or r+(p2)∈IN(R+). We do this by showing that the negation leads to a
contradiction.
So let us assume that r+(p1), r+(p2)/∈IN(R+). Then there are transitions t1, t2∈TR+with
r+(p1)∈t1•and r+(p2)∈t2•, and it follows that mpR(r+(p1)) ∈mpR(t1)•and mpR(r+(p2)) ∈
mpR(t2)•because AHL-morphisms preserve post conditions.
So, by mpR◦r+=r◦mpIwe have r(mpI(p1)), r(mpI(p2)) /∈IN(R), and by contraposition of item
4 in Def. 20 we have l(mpI(p1)), l(mpI(p2)) /∈IN(L), and using mpL◦l+=l◦mpI(see Fig. 13)
we obtain mpL(l+(p1)), mpL(l+(p2)) /∈IN(L). Due to construction of L+as coproduct of Lthere
are i, j ∈ I such that l+(p1) = ιL
i(mpL(l+(p1))) and l+(p2) = ιL
j(mpL(l+(p2))). So, using again
the fact that AHL-morphisms preserve pre conditions, it follows that l+(p1), l+(p2)/∈IN(L+). We
distinguish the following two cases:
Case 1. There is t∈TL+with l+(p1), l+(p2)∈t•.
This means that there are term1, term2∈TΣ(X) with (term1, l+(p1)) ⊕(term2, l+(p2)) ≤
postL+(t) and since AHL-morphisms preserve pre and post conditions, we have
(term1, m+(l+(p1))) ⊕(term2, m+(l+(p2))) ≤postK(m+(t)),
contradicting the fact that AHL-process net Kis unary.
38
References
L+
m+
mpL
%%
K
K
K
K
K
KI+
l+
oor+//
mpI
%%
K
K
K
K
K
KR+
mpR
%%
L
L
L
L
L
L
L
mi
yyttttttm
I
l
oor//
k
R
n
K
mp $$
I
I
I
I
IK0
mp0%%
J
J
J
J
J
f0
oog0//K0
mp0%%
J
J
J
J
J
AN AN0
f
oog//AN0
Figure 13: Process evolution based on action evolution
Case 2. There are t16=t2∈TL+with l+(p1)∈t1•and l+(p2)∈t2•.
Then we have m+(l+(p1)) = m+(l+(p2)) ∈m+(t1)• ∩m+(t2)•and, by injectivity of m+
T
as shown item 1 (Gluing Condition) there is m+(t1)6=m+(t2), contradicting the fact that
AHL-process net Kdoes not have backward conflicts.
Hence, both cases lead to a contradiction, which means that there is r+(p1)∈IN(R+) or r+(p2)∈
IN(R+).
The proof for p16=p2∈OUT(I+) with m+◦l+(p1) = m+◦l+(p2) that r+(p1)∈OUT(R+) or
r+(p2)∈OUT(R+) works analogously.
4. (No Conflicts) Let x∈InP, we have to show that r+(x)∈IN(R+). Let us assume that
mpL(l+(x)) /∈IN(L) in order to show a contradiction. Then there is t∈TLwith mpL(l+(x)) ∈t•.
By construction of L+as coproduct there is some i∈ I such that ιL
i(mpL(l+(x))) = l+(x). Thus,
by the fact that AHL-morphisms preserve pre conditions, we obtain that l+(x)∈ιL
i(t)•, contra-
dicting the fact that l+(x)∈IN(L+) by definition of InP.
So we have mpL(l+(x)) ∈IN(L) and by l◦mpI=mpL◦l+we have l◦mpI(x)∈IN(L). By item
4 of Def. 20 we obtain r◦mpI(x)∈IN(R). By r◦mpI=mpR◦r+we have mpR◦r+(x)∈IN(R).
Let us now assume that r+(x)/∈IN(R+) in order to show a contradiction, i. e. that there is
t∈TR+with r+(x)∈t•. Then due to preservation of post conditions by AHL-morhpisms we have
mpR(r+(x)) ∈mpR(t)•, contradicting the fact that mpR◦r+(x)∈IN(R).
Thus, we have r+(x)∈IN(R+), and hence r+(InP)⊆IN(R+). The proof for r+(OutP )⊆
OUT(R+) works analogously.
References
[Apa11a] Apache Software Foundation. http://apache.org, August 2011.
[Apa11b] Apache Wave. http://incubator.apache.org/wave/, August 2011.
[EEPT06] H. Ehrig, K. Ehrig, U. Prange, and G. Taentzer. Fundamentals of Algebraic Graph Trans-
formation. EATCS Monographs in TCS. Springer, 2006.
[EG11] H. Ehrig and K. Gabriel. Transformation of algebraic high-level nets and amalgamation of
processes with applications to communication platforms. International Journal of Software
and Informatics, 5, Part1:207–229, 2011.
[EHP+02] H. Ehrig, K. Hoffmann, J. Padberg, P. Baldan, and R. Heckel. High-level net processes. In
Formal and Natural Computing, volume 2300 of LNCS, pages 191–219. Springer, 2002.
[Ehr79] H. Ehrig. Introduction to the algebraic theory of graph grammars (a survey). In V. Claus,
H. Ehrig, and G. Rozenberg, editors, Graph Grammars and Their Application to Computer
Science and Biology, Lecture Notes in Computer Science, No. 73, pages 1–69. Springer, 1979.
39
References
[Ehr05] H. Ehrig. Behaviour and Instantiation of High-Level Petri Net Processes. Fundamenta
Informaticae, 65(3):211–247, 2005.
[EM85] H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification 1. Springer, 1985.
[ER97] Hartmut Ehrig and Wolfgang Reisig. An Algebraic View on Petri Nets. Bulletin of the
EATCS, 61:52–58, February 1997.
[Gab10] K. Gabriel. Algebraic high-level nets and processes applied to communication platforms.
Technical Report 2010/14, Technische Universit¨at Berlin, 2010.
[Goo11] Google. http://google.com, August 2011.
[GR83] U. Goltz and W. Reisig. The Non-sequential Behavior of Petri Nets. Information and Control,
57(2/3):125–147, 1983.
[HM10] Kathrin Hoffmann and Tony Modica. Formal modeling of communication platforms using
reconfigurable algebraic high-level nets. ECEASST, 30:1–25, 2010.
[Jen91] K. Jensen. Coloured petri nets: A high-level language for system design and analysis. In
G. Rozenberg, editor, Advances in Petri Nets 1990, volume 483 of LNCS, pages 342–416.
Springer, 1991.
[MGE+10] Tony Modica, Karsten Gabriel, Hartmut Ehrig, Kathrin Hoffmann, Sarkaft Shareef, Claudia
Ermel, Ulrike Golas, Frank Hermann, and Enrico Biermann. Low- and High-Level Petri
Nets with Individual Tokens. Technical Report 2009/13, Technische Universit¨at Berlin,
2010. http://www.eecs.tu-berlin.de/menue/forschung/forschungsberichte/2009.
[MM90] J. Meseguer and U. Montanari. Petri Nets Are Monoids. Information and Computation,
88(2):105–155, 1990.
[PER95] J. Padberg, H. Ehrig, and L. Ribeiro. Algebraic high-level net transformation systems.
Mathematical Structures in Computer Science, 80:217–259, 1995.
[Pet62] C.A. Petri. Kommunikation mit Automaten. PhD thesis, Institut f¨ur instrumentelle Mathe-
matik, Universit¨at Bonn, 1962.
[Rei85] W. Reisig. Petrinetze, Eine Einf¨uhrung. Springer Verlag, Berlin, 1985.
[Rei90] W. Reisig. Petri nets and algebraic specifications. Technische Universit¨at M¨unchen, SFB-
Bericht 342/1/90 B, March, 1990.
[Roz87] G. Rozenberg. Behaviour of Elementary Net Systems. In Petri Nets: Central Models and
Their Properties, Advances in Petri Nets, volume 254 of LNCS, pages 60–94. Springer, 1987.
[Roz97] G. Rozenberg, editor. Handbook of Graph Grammars and Computing by Graph Transforma-
tion, Vol 1: Foundations. World Scientific, Singapore, 1997.
[Yon10] Tsvetelina Yonova. Formal description and analysis of distributed online collaboration plat-
forms. Bachelor thesis, Technische Universit¨at Berlin, 2010.
40
