Forschungsberichte
der Fakultät IV – Elektrotechnik und Informatik
Low- and High-Level Petri Nets
with Individual Tokens
Tony Modica, Karsten Gabriel, Hartmut Ehrig,
Kathrin Hoffmann, Sarkaft Shareef, Claudia Ermel,
Ulrike Golas, Frank Hermann, Enrico Biermann
Bericht-Nr. 2009-13
ISSN 1436-9915
Low- and High-Level Petri Nets
with Individual Tokens
Tony Modica, Karsten Gabriel, Hartmut Ehrig,
Kathrin Hoffmann, Sarkaft Shareef, Claudia Ermel,
Ulrike Golas, Frank Hermann, Enrico Biermann
Bericht-Nr. 2009/13
ISSN 1436-9915
Technical Report 13/2009
Low- and High-Level Petri Nets
with Individual Tokens
∗
Tony Modica, Karsten Gabriel, Hartmut Ehrig,
Kathrin Homann, Sarkaft Shareef, Claudia Ermel,
Ulrike Golas, Frank Hermann, Enrico Biermann
E-Mail: {modica,kgabriel,ehrig,homann,sarkaft,
lieske,ugolas,frank,enricob}@cs.tu-berlin.de
July 8, 2010
TFS - Fakultät IV - Elektrotechnik und Informatik
Technische Universität Berlin
∗
This work has been supported by the Integrated Graduate Program on Human-Centric Communi-
cation at TU Berlin and by the research project
forMAlNET
(see
http://tfs.cs.tu-berlin.de/
formalnet/
) of the German Research Council.
1
2
Abstract
In this article, we present a new variant of Petri nets with markings called
Petri nets with individual tokens, together with rule-based transformation
following the double pushout approach. The most important change to former
Petri net transformation approaches is that the marking of a net is no longer
a collective set of tokens, but each each has an own identity leading to the
concept of Petri nets with individual tokens. This allows us to formulate
rules that can change the marking of a net arbitrarily without necessarily
manipulating the structure. As a rst main result that depends on nets with
individual markings we show the equivalence of transition ring steps and the
application of ring-simulating rules.
We dene categories of low-level and of algebraic high-level nets with indi-
vidual tokens, called PTI nets and AHLI nets, respectively, and relate them
with each other and their collective counterparts by functors.
To be able to use the properties and analysis results of
M
-adhesive HLR
systems (formerly know as weak adhesive high-level replacement systems) we
show in further main results that both categories of PTI nets and AHLI nets
are
M
-adhesive categories. By showing how to construct initial pushouts we
also give necessary and sucient conditions for the applicability of transfor-
mation rules in these categories, known as gluing condition in the literature.
CONTENTS
3
Contents
1. Introduction 4
1.1. The Notion of Individual Tokens . . . . . . . . . . . . . . . . . . . . . . . 5
2. Place/Transition Nets with Individual Tokens 6
2.1. Denition and Firing Behavior . . . . . . . . . . . . . . . . . . . . . . . . 6
2.2. Transformation of PTI Nets . . . . . . . . . . . . . . . . . . . . . . . . . . 9
2.3. Correspondence of Transition Firing and Rules . . . . . . . . . . . . . . . 13
3. Algebraic High-Level Nets with Individual Tokens 18
3.1. Denition and Firing Behavior . . . . . . . . . . . . . . . . . . . . . . . . 18
3.2. Transformation of AHLI Nets . . . . . . . . . . . . . . . . . . . . . . . . . 23
3.3. Correspondence of Transition Firing and Rules . . . . . . . . . . . . . . . 28
4. Functors for Individual Net Classes 35
5. Nets with Individual Tokens are
M
-adhesive Categories 41
6. Conclusion 43
7. Future Work 44
A. Appendix 49
A.1. Categorical Gluing Condition with Initial Pushouts . . . . . . . . . . . . . 49
A.2. Initial Pushouts in
Sets
............................ 56
A.3. Initial Pushouts in
PTNets
.......................... 61
B. Proofs 63
4
1. INTRODUCTION
1. Introduction
Petri nets are one of the main formalisms to describe and analyze concurrent processes
[Rei85a]. To be able to utilize them in modeling of additional complex aspects, a lot of
work has been done so far to extend the classical Petri nets or to integrate them with
other formal techniques.
One of those challenging extensions is the manipulation of running processes, which
has been formulated under the notion of adaptive workows [vdABV
+
99]. In the past,
several approaches have been proposed that tried to deal with this aspect of process
modeling by using Petri nets that can change their ring behavior, e.g. self-modifying
nets [Val78], mobile nets [AB09], recursive nets [HP00, HB08], and nets with dynamic
transition renement [KR07].
In this article, we concentrate on the approach to combine Petri nets with transforma-
tion rules based on graph transformation [EEPT06], which has been applied to adaptive
workows in [HME05, BDHM06]. This exploits the graph-like structure of Petri nets and
allows us to formulate rules to change the structure of a Petri net [EHP
+
08]. In general,
rule-based Petri net transformation can also be applied to Petri systems, i.e. Petri nets
with a marking, which is especially useful for manipulation of processes at runtime.
Petri nets have been shown in [EEPT06, EHP
+
08] to be dene a weak adhesive HLR
category for the class
M
of all injective net morphisms. This allows us to apply all the
results for adhesive HLR systems shown in [EEPT06] also for Petri net transformation
systems. In this paper, we use the short notion
M
-adhesive category for weak ad-
hesive HLR category. the concept of Petri systems leads to a category
PTSys
with
morphisms allowing to increase the number of tokens on corresponding places. Unfortu-
nately,
(PTSys,Minj)
with the class
Minj
of all injective morphisms is not
M
-adhesive
in contrast to
(PTSys,Mstrict)
, where
Mstrict
is the class of injective morphisms where
the number of tokens on corresponding places is equal. This, however, is an unpleas-
ant restriction for the usability of the transformation approach, especially the ring of
a transition cannot be simulated in a natural way by the application of a corresponding
transition rule.
To overcome this restriction we present a new Petri net formalism, called Petri nets
with individual tokens, together with a rule-based transformation approach that is al-
most equivalent to [EHP
+
08]
1
. The most important change is that a net's marking is no
longer a (collective) sum of a monoid but a set of individuals. This allows us to formu-
late rules that can change the marking of a net arbitrarily so that, as major advantage,
ring of nets can be modeled by rule applications.
As a main result we will show that Petri nets with individual tokens are
M
-adhesive
systems with all their nice properties.
With individual tokens, the category of Petri systems is even closer to typed attributed
graphs, which opens an elegant way to simulate Petri net transformations with graph
1
The approach in [EHP
+
08] follows the concept Petri nets are monoids [MM90] so that a net and its
marking are represented as sets and monoids over these sets, rather than e.g. with an explicit ow
relation. This makes it easier to handle categories of Petri nets and systems.
1.1. THE NOTION OF INDIVIDUAL TOKENS
5
transformation tools [Syl09].
In Sect. 2, we introduce
low-level
Petri nets with individual tokens and dene rule-
based transformation. As a main result we show the equivalence of transition ring steps
and the application of ring-simulating rules.
In Sect. 3, we lift the denitions and results of Sect. 2 to
high-level
nets that have
data elements of an algebra [EM85] as tokens rather than low-level black tokens. The
rst approach of inscripting Petri nets with algebraic terms was developed in [Rei91],
however, we use the approach of [EPR93], which allows us to use an arbitrary algebra,
as long as it complies to the given signature.
2
Section 4 relates the Petri net classes of Sect. 2 and 3 with each other and with their
collective counterparts by functors and we show a compatibility result for these functors.
We dene
M
-adhesive systems for both low and high-level Petri nets with individual
tokens in Sect. 5 and discuss the results and some nal remarks in the last sections.
1.1. The Notion of Individual Tokens
The term of
individual tokens
has been used in two senses for Petri nets so far:
1. It was mentioned rst in [Rei85b], where it was used to describe tokens that can
be identied as individual objects. The main contribution of this article was to dene
markings as multisets of distinguished elements rather than amounts of indistinguishable
black tokens. In the end,
individual tokens
in this context is a synonym for what by now
is called
high-level tokens
. This is not our intended meaning of individuality, moreover
we will consider both low-level and high-level Petri nets with individual tokens.
2. The other notion of token individuality has been coined in [vGP95]
3
as individual
token interpretation of ring steps, which entitles the denition of processes in [GR83].
In [vG05], the author investigates the collective-individual dichotomy of ring steps,
where under the individual approach ring sequences consider not only the number and
value of tokens (as in the collective approach) but also the history, i.e. the origin tran-
sition, of tokens. [BMMS99] introduces a category of Petri nets to be interpreted with a
functorial individual semantics.
Individual tokens in this article
The Petri net approach we present in this article is
related to 2., but in contrast, we will already introduce individual tokens in the (syntac-
tical) denition of the Petri nets (and their category) themselves, so that we can exploit
the individuality of tokens in the transformation approach, independently of the ring
rule. The individual ring rule of [vG05] is very close to the one presented in the next
sections, but it is still an interpretation of ring steps of a classic representation of Petri
nets.
2
Both articles consider algebraic specications with equations instead of signatures (which can be
understood as specications without equations). In this article we take into account signatures only.
3
Meanwhile, there is an updated version of this article: [vGP09].
6
2. PLACE/TRANSITION NETS WITH INDIVIDUAL TOKENS
The main purpose of our notion of nets with individual tokens is the possibility of
formulating marking-changing rules for this kind of nets. We have demonstrated the
practicability of such a transformation approach with modeling case studies on applica-
tions to Communication Spaces [BEE
+
09, Mod10, MEE
+
10].
2. Place/Transition Nets with Individual Tokens
In this section we treat low-level Petri nets and equip them with markings of individual
tokens. After describing their ring behavior and introducing rules for the transformation
of marked nets we show how special transformations correspond to transition ring steps.
2.1. Denition and Firing Behavior
With the denition of nets with individual tokens, we follow the concept Petri nets are
monoids from [MM90]:
Denition 2.1
(Place/Transition Nets with Individual Tokens (PTI))
.
We dene a marked P/T net with individual tokens, short PTI net, as
NI = (P, T, pre, post, I, m),
where
•N= (P, T, pre, post :T→P⊕)
is a classical P/T net, where
P⊕
is the free
commutative monoid over
P
,
•I
is the (possibly innite) set of individual tokens of
NI
, and
•m:I→P
is the marking function, assigning the individual tokens to the places.
Further, we introduce some additional notations:
•
the environment of a transition
t∈T
as
ENV (t) = P RE(t)∪POST(t)⊆P
with
PRE(t) = {p∈P|pre(t)(p)6= 0},
POST(t) = {p∈P|post(t)(p)6= 0},
Example.
Figure 1 on the facing page shows the graphical representation of a PTI net
with
I={x1, y1, x2, x3}
,
m(x1) = m(y1) = p1
,
m(x2) = p2
,
m(x3) = p3
.
Now that we have marked Petri nets, also called Petri systems, we have to dene
their behavior as ring steps. Because we have individual tokens, we have to consider a
possible ring step in the context of a selection of tokens.
Denition 2.2
(Firing of PTI Nets)
.
A transition
t∈T
in a PTI net
NI = (P, T, pre, post, I, m)
is
enabled
under a
token selection
(M, m, N, n)
, where
2.1. DEFINITION AND FIRING BEHAVIOR
7
t
p1
p2
p3
2
x1
y1
x2
x3
Figure 1: Example PTI net
•M⊆I
,
•m
is the token mapping of
NI
,
•N
is a set with
(I\M)∩N=∅
,
•n:N→P
is a function,
if it meets the following
token selection condition
:
"X
i∈M
m(i) = pre(t)#∧"X
i∈N
n(i) = post(t)#
If an enabled
t
res, the follower marking
(I0, m0)
is given by
I0= (I\M)∪N, m0:I0→P
with
m0(x) = (m(x), x ∈I\M
n(x), x ∈N
leading to
NI 0= (P, T, pre, post, I0, m0)
as the new PTI net in the
ring step
NI i
−
t
→NI 0
via
(M, m, N, n)
.
Remark
(Token Selection)
.
The purpose of the token selection is to specify exactly which
tokens should be consumed and produced in the ring step. Thus,
M⊆I
selects the
individual tokens to be consumed, and
N
contains the set of individual tokens to be
produced. Clearly,
(I\M)∩N=∅
must hold because it is impossible to add an
individual token to a net that already contains this token.
m
and
n
relate the tokens to
their carrying places. It would be sucient to consider only the restriction
m|M
here or
to infer it from the net but as a compromise on symmetry and readability we denote
m
in the token selection.
For the next subsection we need a category of Petri systems.
Denition 2.3
(PTI Net Morphisms and Category
PTINets
)
.
Given two PTI nets
NI i= (Pi, Ti, prei, posti, Ii, mi)
,
i∈ {1,2}
, a PTI net morphism is
a triple of functions
f= (fP:P1→P2, fT:T1→T2, fI:I1→I2) : NI 1→NI 2
, such
that the following diagrams commute (componentwise for
prei
and
posti
):
8
2. PLACE/TRANSITION NETS WITH INDIVIDUAL TOKENS
T1
fT
pre1//
=
post1
//P⊕
1
f⊕
P
I1
fI
m1//
=
P1
fP
T2
pre2//
post2
//P⊕
2I2
m2//P2
or, explicitly, that
f⊕
P◦pre1=pre2◦fT, f⊕
P◦post1=post2◦fT, fP◦m1=m2◦fI
.
The category
PTINets
consists of all PTI nets as objects with all PTI net morphisms.
Remark.
For a general PTI net morphism
f
we do not require that its token component
fI
is injective in order to have pushouts, pullbacks, and a
M
-adhesive category. But later
we may require injectivity of
fI
for rule and match morphisms and to have morphisms
preserving ring behavior.
Fact 2.4
(Construction of Pushouts in
PTINets
)
.
Pushouts in
PTINets
are constructed componentwise in
PTNets
and
Sets
. So,
(1)
is a PO in
PTINets
i
(2)
is a PO in
PTNets
and
(3)
is a PO in
Sets
with the
components of the
PTINets
morphisms, where
m3:I3→P3
is induced by PO object
I3
in the commuting cube below (whose front is the PO of place sets).
NI 0
f1//
f2
(1)
NI 1
g1
NI 2g2
//NI 3
N0
f0
1//
f0
2
(2)
N1
g0
1
N2g0
2
//N3
I0
f1I//
f2I
(3)
I1
g1I
I2g2I
//I3
I0
f1I//
f2I
m0
I1
g1I
m1
P0
f1P//
f2P
P1
g1P
I2g2I
//
m2
I3
m3
P2g2P
//P3
If
f1X
, for
X∈ {P, T, I}
, is injective then
g2X
is as well; analogously for components
of
f2
and
g1
.
Example.
Figure 2 on page 14 shows two pushouts in
PTINets
.
Fact 2.5
(Construction of Pullbacks in
PTINets
)
.
Pullbacks in
PTINets
along injective
PTINets
morphisms
4
are constructed compo-
nentwise in
PTNets
and
Sets
.
Consider a commutative square
(1)
in
PTINets
with
g1
having an injective net com-
ponent
g0
1
.
(1)
is a PB in
PTINets
i
(2)
is a PB in
PTNets
and
(3)
is a PB in
Sets
with the components of the
PTINets
morphisms, where
m0:I0→P0
is induced by PB
object
P0
in the commuting cube below (whose front is the PB of place sets).
4
We require morphisms that are injective in order to obtain componentwise pullbacks in
PTINets
.
See [EEPT06] for details.
2.2. TRANSFORMATION OF PTI NETS
9
NI 0
f1//
f2
(1)
NI 1
g1
NI 2g2
//NI 3
N0
f0
1//
f0
2
(2)
N1
g0
1
N2g0
2
//N3
I0
f1I//
f2I
(3)
I1
g1I
I2g2I
//I3
I0
f1I//
f2I
m0
I1
g1I
m1
P0
f1P//
f2P
P1
g1P
I2g2I
//
m2
I3
m3
P2g2P
//P3
Example.
The pushouts in Fig. 2 on page 14 are pullbacks, too.
2.2. Transformation of PTI Nets
This section is about rule-based transformation of PTI nets. We use the double pushout
approach, which has also been used in [EHP
+
08] and stems from [EEPT06]. We are
going to characterize the applicability of rules at some match by initial pushouts.
Denition 2.6
(PTI Transformation Rules)
.
A PTI transformation rule is a span of injective
PTINets
morphisms
%= (Ll
←Kr
→R).
Remark.
In contrast to [EHP
+
08], rule morphisms for PTI rules are not required to be
marking-strict in order to obtain an
M
-adhesive category (see Sect. 5 on page 41). This
allows to arbitrarily change the marking of a PTI net by applying rules with correspond-
ing places and individual tokens in
L
and
R
.
Denition 2.7
(PTI Transformation)
.
Given a PTI transformation rule
%= (Ll
←Kr
→R)
and a PTI net
NI 1
with a PTI net
morphism
f:L→NI 1
, called the match, a direct PTI net transformation
NI 1=
%,f
=⇒NI 2
from
NI 1
to the PTI net
NI 2
is given by the following double-pushout diagram (DPO)
diagram in the category
PTINets
:
L
f
(PO1)
K
(PO2)
l
oo
r//R
f∗
NI 1NI0
oo//NI 2
To be able to decide whether a rule is applicable at a certain match, we formulate a
gluing condition for PTI nets, such that there exists a pushout complement of the left
rule morphisms and the match if (and only if) they fulll the gluing condition. The
correctness of the gluing condition is shown via a proof on initial pushouts over matches,
according to [EEPT06].
10
2. PLACE/TRANSITION NETS WITH INDIVIDUAL TOKENS
Denition 2.8
(Gluing Condition in
PTINets
)
.
Given PTI nets
K, L
, and
NI
and PTI morphisms
l:K→L
and
f:L→NI
. We dene
the set of identication points
5
IP =IPP∪IPT∪IPI
with
•IPP={x∈PL| ∃x06=x:fP(x) = fP(x0)}
,
•IPT={x∈TL| ∃x06=x:fT(x) = fT(x0)}
,
•IPI={x∈IL| ∃x06=x:fI(x) = fI(x0)}
,
the set of dangling points
6
DP =DPT∪DPI
with
•DPT={p∈PL| ∃t∈TNI \fT(TL) : fP(p)∈ENV (t)}
,
•DPI={p∈PL| ∃i∈INI \fI(IL) : fP(p) = mNI (i)}
,
and the set of gluing points
7
GP =lP(PK)∪lT(TK)∪lI(IK)
We say that
l
and
f
satisfy the gluing condition if
IP ∪DP ⊆GP
. Given a PTI rule
%= (Ll
←Kr
→R)
, we say
%
and
f
satisfy the gluing condition i
l
and
f
satisfy the
gluing condition.
L
f
K
l
oor//R
NI
In order to construct the initial pushout for a match
f:L→NI
, we dene the
boundary
over the match
f
, which is the minimal subnet containing all places, transitions,
and individual tokens that must not be deleted by the application of a rule with left hand
side
L
such that there exists a pushout complement.
Denition 2.9
(Boundary in
PTINets
)
.
Given a morphism
f:L→NI
in
PTINets
. The boundary of
f
is a PTI net
B= (PB, TB, preB, postB, IB, mB)
with
5
That is, all elements in
L
that are mapped non-injectively by
f
.
6
That is, all places in
L
that would leave a dangling arc, if deleted.
7
That is, all elements in
L
that have a preimage in
K
.
2.2. TRANSFORMATION OF PTI NETS
11
•PB=DPT∪DPI∪IPP∪PIP T∪PIPI
•PIPT={p∈PL| ∃t∈IPT:p∈ENV (t)}
•PIPI={p∈PL| ∃i∈IPI:p=mL(i)}
•TB=IPT
•preB(t) = preL(t)
•postB(t) = postL(t)
•IB=IPI
•mB(i) = mL(i)
together with an inclusion
b:B→L
.
Well-denedness.
preB, postB:TB→P⊕
B
:
The well-denedness follows from the well-denedness of Denition A.9 and the
fact that
B
has the same set of transitions as the boundary in A.9 and the set of
places in Denition A.9 is a subset of
PB
.
mB:IB→PB
:
Let
i∈IB
. Then we have
i∈IPI
and hence
mB(i) = mL(i)∈PIPI⊆PB
b:B→L
:
We obtain an inclusion morphism
b:B→L
from the fact that
preB, postB
and
mB
are restrictions of the respective functions in
L
.
The following facts about the gluing condition and initial pushouts hold in all
M
-
adhesive categories
(PTINets,M)
whose morphism class
M
of monomorphisms con-
tains at least inclusions (for concrete instantiations see Sect. 5 on page 41). The next
fact completes the construction of initial pushouts for matches and shows that the con-
struction of the boundary in Def. 2.9 on the preceding page complies to the categorical
notion of boundaries in Def. A.1 on page 49.
Fact 2.10
(Initial Pushout in
PTINets
)
.
Given a morphism
f:L→NI
in
PTINets
, the boundary
B
of
f
and the PTI net
C= (PC, TC, preC, postC, IC, mC)
with
12
2. PLACE/TRANSITION NETS WITH INDIVIDUAL TOKENS
•PC= (PNI \fP(PL)) ∪fP(bP(PB))
•TC= (TNI \fT(TL)) ∪fT(bT(TB))
•IC= (INI \fI(IL)) ∪fI(bI(IB))
•preC(t) = preNI (t)
•postC(t) = postNI (t)
•mC(i) = mNI (i)
Then diagram (1) where
g:= f|B
is an initial pushout in
PTINets
.
Bb//
g
L
f
Cc//
(1)
NI
Proof.
See section B.1 on page 63.
The following two facts show the correspondence between the gluing condition in
PTINets
and the categorical gluing condition (see Def. A.2 on page 49), which is a
necessary and sucient condition for the (unique) existence of pushout complements in
all
M
-adhesive categories.
Fact 2.11
(Characterization of Gluing Condition in
PTINets
)
.
Let
l:K→L
and
f:L→NI
be morphisms in
PTINets
with
l∈ M
.
The morphisms
l
and
f
satisfy the gluing condition in
PTINets
if and only if they
satisfy the categorical gluing condition.
Proof.
See section B.2 on page 67.
Fact 2.12
(Gluing Condition for PTI Transformation)
.
Given a PTI rule
%= (Ll
←Kr
→R)
and a match
f:L→NI
into a PTI net
NI = (N, I, m :I→PNI )
. The rule
%
is applicable on match
f
, i.e. there exists a
(unique) pushout complement
NI 0
in the diagram below, i
%
and
f
satisfy the gluing
condition in
PTINets
.
L
f
(P O)
K
l
oo
f0
r//R
NI NI 0
oo
Proof.
By Fact 2.11
%
and
f
satisfy the gluing condition in
PTINets
if and only if
%
and
f
satisfy the categorical gluing condition, which by Fact A.3 is a necessary and sucient
condition for the (unique) existence of the pushout complement
NI 0
.
2.3. CORRESPONDENCE OF TRANSITION FIRING AND RULES
13
2.3. Correspondence of Transition Firing and Rules
Now that we can manipulate a net's marking with rules, we have a look at rules that
simulate ring steps for a certain transition under a token selection. We show that ring
of a transition corresponds to a canonical application of a special rule construction, called
transition rules. With this correspondence we can easily show that token-injective PTI
morphisms preserve ring steps.
Denition 2.13
(PTI Transition Rules)
.
We dene the
transition rule
for a transition
t∈T
enabled under a token selection
S= (M, m, N, n)
in a PTI net
NI = (P, T, pre, post, I, m)
as the rule
%(t, S)=(Lt
l
←Kt
r
→Rt),
with
•
the common xed net structure
PN t= (Pt,{t}, pret, postt)
, where
Pt=ENV (t)
,
pret(t) = pre(t)
and
postt(t) = post(t)
,
•Lt= (PN t, M, mt:M→Pt)
, with
mt(x) = m(x)
,
•Kt= (PN t,∅,∅:∅ → Pt)
,
•Rt= (PN t, N, nt:N→Pt)
, with
nt(x) = n(x)
,
•l, r
being the obvious inclusions on the rule nets.
mt
and
nt
are well-dened because
t
is enabled under
S
: The token selection condition
implies that
∀x∈M:m(x)∈PRE(t)
and due to the construction of
PN t
we have
PRE(t)⊆ENV (t) = Pt
. The argument for
nt
works analogously.
Note that
t
is enabled under
S
in
Lt
.
Example.
Figure 2 shows a PTI transition rule
%(t, S) = (Ll
←Kr
→R)
for transition
t
in
NI
.
Denition 2.14
(Canonical DPO Transformation of PTI Nets)
.
We call a direct transformation
NI 1=
%,f
=⇒NI 2
by rule
%= (Ll
←Kr
→R)
with
l, r
being
inclusions
canonical
if
•fI
is injective,
•
the morphisms in the span
(NI 1←NI0→NI 2)
of the DPO transformation
diagram below are inclusions, and
•I2=I0∪(IR\r(IK))
.
L
f
(PO1)
K
(PO2)
l
oo
r//R
f∗
NI 1NI0
oo//NI 2
14
2. PLACE/TRANSITION NETS WITH INDIVIDUAL TOKENS
Remark.
For each rule
%
being applied to some PTI net
NI
at a token-injective match
f
,
there exists a canonical transformation diagram, which is just the particular equivalent
DPO diagram with as less isomorphic changes as possible.
Because of the injectivity of the rule morphisms the lower span in the diagram is
already injective as well. To construct the canonical transformation diagram we rst
regard the last condition on
I2
, which demands that
(IR\r(IK)) ∩I0=∅
because of
pushout
PO2
. For this, it is sucient to replace the set of tokens in
R
that are created
by the rule, i.e.
IR\r(IK)
, such that is disjoint to the tokens preserved by the rule, i.e.
(I1\f(IL)) ∪f(l(IK))
.
8
With this we now can simply replace arbitrary
NI 0
and
NI 2
,
being some pushout complement object of
PO1
and pushout object of
PO2
, with nets
such that the lower span morphisms become inclusions.
Example.
The diagram in Fig. 2 shows the two pushouts in
PTINets
resulting from
applying the PTI transition rule
%(t, S)=(Ll
←Kr
→R)
to the net
NI
with identical
token morphism component. Moreover, this transformation is canonical.
t
p1p2
p3
2
x1y1x2
L
f
(PO1)
t
p1p2
p3
2
K
(PO2)
l
oo
r//
t
p1p2
p3
2
x3R
t
p1p2
p3
2
x1y1x2
z1y2
y3NI
t
p1p2
p3
2
z1y2
y3
oo//
t
p1p2
p3
2
x3
z1y2
y3
Figure 2: Canonical direct DPO-transformation in
PTINets
simulating a ring step
Theorem 2.1
(Equivalence of Canonical Transformations and Firing of PTI Nets)
.
1. Each ring step
NI i
−
t
→NI 0
via a token selection
S= (M, m, N, n)
corresponds to a
canonical direct transformation
NI =
%(t,S),f
====⇒NI 0
via the transition rule
%(t, S)
, matched
by the inclusion match
f:L%(t,S)→NI
.
8
This modication of the rule is passable since changing the tokens in
R
does not aect the ring
behavior of
NI2
(up to the token selections) nor the applicability of the rule.
2.3. CORRESPONDENCE OF TRANSITION FIRING AND RULES
15
2. Each canonical direct transformation
NI =
%(t,S),f
====⇒NI 1
, via some transition rule
%(t, S)=(Ll
←Kr
→R)
with
t∈TNI
and token selection
S= (M, m, N, n)
, and a
token-injective match
f:L→NI
, implies that the transition
fT(t)
is enabled in
NI
under
fI(M),fP◦m◦f−1
I, N, f∗
P◦m1◦f∗−1
I
with ring step
NI i
−
fT(t)
−−−→ NI 1
.
Proof.
1. Given the ring step
NI i
−
t
→NI 0
via
S= (M, m, N, n)
, the canonical direct transfor-
mation of the transition rule
%(t, S) = (Ll
←Kr
→R)
is
NI =
%(t,S),f
====⇒NI 1
as in the DPO
diagram in Fig. 3. The match
f
,
d
, and
d0
are inclusions.
L= (PN t, M, mt)
f
(PO1)
K= (PN t,∅,∅)
(PO2)
?_
l
oo
r//R= (PN t, N, nt)
f∗
NI = (PN , I, m)NI 0= (PN , I0, m0)
?_
d
oo
d0//NI 1= (PN , I1, m1)
Figure 3: DPO diagram for canonical direct transformation of
NI
with
%(t, S)
in
PTINets
According to Fact 2.4 on page 8, we have
I0=I\M
and
I1=I0∪(N\∅)
as in the DPO
diagram of the
Sets
components in Fig. 4. The ring step condition
(I\M)∩N=∅
grants us the last condition for canonical transformations
I0∪(N\r(∅)) = I1
.
M
fI
(PO1)
∅
(PO2)
?_
oo
//N
f∗
I
nt
''
I
m
++
I0= (I\M)
?_
dI
oo
d0
I
//
m0=m◦dI
&&
I1= (I\M)∪N
m1''
Pt
f∗
P=fP
PPN id PPN
Figure 4: DPO diagram in
Sets
for the token components of the transformation in Fig. 3
For
m1
as induced morphism for the pushout object
I1
follows that
m1(x) = (m0(x) = m(x)
for
x∈I\M
nt(x) = n(x)
for
x∈N
hence
I1=I0, m1=m0
and
NI 1=NI 0
, according to Def. 2.2 on page 6.
Remark.
fI
being injective is not only sucient for the existence of
(PO1)
, but also
necessary, because
IK=∅
(see Fact 2.12 on page 12).
2. Given a canonical direct transformation
NI =
%(t,S),f
====⇒NI 1
as in the DPO diagrams in
Figs. 3 and 4,
fT(t)∈TNI
is enabled under
fI(M),fP◦m◦f−1
I, N, f∗
P◦m1◦f∗−1
I
16
2. PLACE/TRANSITION NETS WITH INDIVIDUAL TOKENS
if
1.
fI(M)⊆I
,
2.
f∗
P◦m1◦f∗−1
I:N→PPN
,
3.
(I\fI(M)) ∩N=∅
,
4.
P
i∈fI(M)fP◦m◦f−1
I(i)=preNI (fT(t))
5.
P
i∈Nf∗
P◦m1◦f∗−1
I(i)=postNI (fT(t))
6. leading to the follower marking
I0= (I\M)∪N
with
m0(x) = (m0(x) = m(x)
for
x∈I\M
m1(x) = n(x)
for
x∈N
By construction of the transition rule
%(t, S)
and its application to
NI
we have 1., 2.,
and for 6. that
I0=I1, m0=m1
. The canonical transformation property grants us 3.
It remains to show 4. and 5., i.e. that
fI(M)
and
N
represent the correct numbers of
tokens in the environment of
fT(t)
to enable it:
X
i∈fI(M)
fP◦m◦f−1
I(i)
=X
i∈M
fP◦m(i) (fI
inj.
)
=f⊕
PX
i∈M
mt(i) (∀i∈M:mt(i) = m(i),
due to def.
%(t, S))
=f⊕
P◦prePN t(t) (t
enabled in
L)
=preNI ◦fT(t) (f
PTI morph.
)
and analogously,
X
i∈N
f∗
P◦m1◦f∗−1
I(i)
=X
i∈N
f∗
P◦m1(i) (f∗
I(N) = N)
=f∗⊕
PX
i∈N
nt(i) (∀i∈N:nt(i) = m1(i),
due to constr.
m1)
=f∗⊕
P◦prePN t(t) (t
enabled in
L)
=postNI ◦fT(t) (f
PTI morph.
)
2.3. CORRESPONDENCE OF TRANSITION FIRING AND RULES
17
The second item of the previous theorem covers all possible canonical direct transfor-
mations by any transition rule
%(t, S)
in an arbitrary net
NI
, without aasuming that
t∈NI
or
M⊆INI
. For the special case that a transition rule
%(t, S)
is applied on an
inclusion match, the second item reduces to the following corollary, which is more similar
to the theorem's rst item.
Corollary 2.2
(Equivalence of Canonical Transformations and Firing of PTI Nets)
.
Given a canonical transformation
NI =
%(t,S),f
====⇒NI 1
such that the match
f:L→NI
is an
inclusion, then
t
is enabled in
NI
under
S
with ring step
NI i
−
t
→NI 1
.
This follows directly from 2. of Theorem 2.1.
Theorem 2.3
(Token-injective PTI Net Morphisms preserve Firing Steps)
.
For each PTI net morphism
f:NI 1→NI 2
with injective
fI
component and each ring
step
NI 1i
−
t
→NI 0
1
there exists a ring step
NI 2i
−
fT(t)
−−−→ NI 0
2
and a PTI net morphism
f0:NI 0
1→NI 0
2
(depicted in diagram (1) below).
NI 1//t//
f
(1)
NI 0
1
f0
NI 2//fT(t)
//NI 0
2
Proof.
Given
f:NI 1→NI 2
and
NI 1i
−
t
→NI 0
1
via some
S
as above, we have by the
rst part of Theorem 2.1 on page 14 the canonical direct transformation given by the
pushouts
(1)
and
(2)
with
%(t, S)=(Ll
←Kr
→R)
in Fig. 5.
L
incL
(1)
K
(2)
l
oo
r//R
incR
NI 1
f
(3)
NI D1
l0
oor0//
(4)
NI 0
1
f0
NI 2NI D2
oo//NI 0
2
Figure 5: DPO diagrams for canonical direct transformation of
NI 1
and
NI 2
with
%(t, S)
Note that
f:NI 1→NI 2
satises the gluing condition w.r.t this rule and
f
, because
l0
P=idP1, l0
T=idT1
9
and none of the individuals of
NI 1
is an identication point
(
IPI=∅
) due to injectivity of
fI
. This allows to construct the canonical transformation
with extended rule
NI 1
l0
←NI D1
r0
→NI 0
1
along pushouts
(3)
and
(4)
. Hence, also
(1 + 3)
and
(2 + 4)
are pushouts of a canonical direct transformation via
%(t, S)
. The second
part of Theorem 2.1 on page 14 implies
NI 2i
−
fT(t)
−−−→ NI 0
2
.
9
This means that all places and transitions of
NI 1
are gluing points.
18
3. ALGEBRAIC HIGH-LEVEL NETS WITH INDIVIDUAL TOKENS
Remark
(Firing-preserving diagrams for
t
correspond to an extension diagram for
%(t, S)
)
.
The diagram in Fig. 5 on the previous page corresponds to an extension diagram for rule
%(t, S)
and
f
(as depicted below) because
(1) −(4)
are pushouts.
NI 1
%(t,S),inc +3
f
NI 0
1
f0
NI 2
%(t,S),f◦inc +3NI 0
2
3. Algebraic High-Level Nets with Individual Tokens
In this section, we lift the results of the previous section to high-level nets whose tokens
represent values of an algebra to a signature [EM85]. The rule-based transformation
of
collective
algebraic high-level nets from [PER95] is the foundation for the approach
presented in the following.
3.1. Denition and Firing Behavior
Denition 3.1
(Algebraic High-Level Nets with Individual Tokens)
.
We dene a marked AHL net with individual tokens, short AHLI net, as
ANI = (Σ, P, T, pre, post, cond, type, A, I, m),
where
•AN = (Σ, P, T, pre, post, cond, type, A)
is a classical AHL net with
signature
Σ=(S, OP, X)
of sorts
S
, operation symbols
OP
and variables
X= (Xs)s∈S
,
sets of places
P
and transitions
T
,
pre, post :T→(TOP (X)⊗P)⊕
10
, dening the transitions' pre- and postdo-
mains,
cond :T→ Pfin(Eqns(S, OP, X))
assigning a nite set of
Σ
-equations
(L, R, X)
as ring conditions to each transition,
type :P→S
typing the places of the signature's sorts,
a
Σ
-algebra
A
,
•I
is the (possibly innite) set of individual tokens of
ANI
, and
•m:I→A⊗P
is the marking function, assigning the individual tokens to the data
elements on the places.
m(I)
denes the actual set of data elements on the places
of
ANI
.
m
does not have to be injective.
Further, we introduce some additional notations:
10
TOP (X)⊗P={(t, p)∈TOP (X)×P|t∈TOP,type(p)(X)}
, i.e the pairs where term
t
is of sort
type(p)
.
3.1. DEFINITION AND FIRING BEHAVIOR
19
•V ar(t)⊆X
is the set of variables occurring in equations and on the environment
arcs of
t
,
•CP = (A⊗P) = {(a, p)∈A×P|a∈Atype(p)}
as the set of consistent value/place
pairs,
•CT ={(t, asg)∈T×(V ar(t)→A)|∀(L, R, X)∈cond(t) : asg(L) = asg(R)}
as the set of consistent transition assignments, i.e. all ring conditions of
t
are valid
when evaluated with the variable assignment
asg
11
,
•ENV (t) = PRE(t)∪POST(t)⊆(TOP (X)⊗P)
as the environment of a transition
t∈T
where
PRE(t) = {(term, p)∈(TOP (X)⊗P)|pre(t)(term, p)6= 0}
POST(t) = {(term, p)∈(TOP (X)⊗P)|post(t)(term, p)6= 0}
•ENV P(t) = πP(ENV (t)) ⊆P
the place environment of
t
,
•preA, postA:CT →CP⊕
, dened by
preA(t, asg)=(asg ⊗idP)⊕(pre(t)) ,
postA(t, asg)=(asg ⊗idP)⊕(post(t))
Similarly, we dene the sets
12
PREA(t, asg) = {(a, p)∈(A⊗P)|preA(t, asg)(a, p)6= 0}
POSTA(t, asg) = {(a, p)∈(A⊗P)|postA(t, asg)(a, p)6= 0}
We can express e.g. the concrete required
number
of a token
(a, p)
for
t
to re un-
der assignment
asg
with
preA(t, asg)(a, p)
by interpreting the monoid
preA(t, asg)
as a function
CP →N
. Similarly, we get the produced
number
of
(a, p)
with
postA(t, asg)(a, p)
.
Remark
(Individual tokens vs. classical algebraic data tokens)
.
Each AHLI net with
individual token marking
(I, m)
can be interpreted as an AHL net with marking
M=X
(a,p)∈A⊗P
|m−1(a, p)|(a, p) = X
i∈I
m(i)
where
|m−1(a, p)|
denotes the cardinality of individual tokens in
I
that
m
maps to
(a, p)
.
In AHL nets, the tokens are of the form
(a, p)
, s.t. they have already a kind of
identity, depending on their data values. The main dierence to AHLI nets is that we
can distinguish tokens of the same algebraic value on the same place. Moreover, the
individuals equip data tokens with identities. When ring a transition, we now can
relate the input and output tokens so that a token's history can be traced along the
ring steps.
11
where
asg :TOP (X)→A
is the evaluation of
Σ
-terms over variables in
X
to values in
A
. Technically,
asg =xeval(asg)A
results from a free construction over
asg
.
12
Obviously, these sets are the same as
(asg ⊗idP)◦PRE (t)
and
(asg ⊗idP)◦POST (t)
, respectively.
20
3. ALGEBRAIC HIGH-LEVEL NETS WITH INDIVIDUAL TOKENS
Example.
Figure 6 shows the graphical representation of an AHLI net with
•
signature
Σ=({s1, s2, s3},{t11 :→s1, t12 :→s1, t2:→s2, t3:→s3})
,
•
algebra carrier sets
As1={a1, b1, c1}, As2={a2, b2}, As3={a3, b3, c1}
•pre(t)=(t11, p1)⊕(t12, p1)⊕(t2, p2), post(t) = (t3, p3)
,
•type(p1) = s1, type(p2) = s2, type(p3) = s3
,
•cond(t) = ∅
,
•I={x1, y1, x2, x3}
,
m(x1) = m(y1)=(a1, p1), m(x2)=(a2, p2), m(x3)=(a3, p3)
,
Note that the algebraic value of an individual token is given next to the dashed arc to
its carrying place. In the following, if a transition has an empty set of conditions we just
denote the transition name without an explicit
∅
below.
t
∅
p1:
s1
p2:
s2
p3:
s3
t11⊕t12
t2
t3
x1
y1
x2
x3
a1
a2
a1
a3
Figure 6: Example AHLI net
Similar as for low-level PTI nets, we now dene ring steps for a transition and a token
selection. In addition, we have to take into account assignments evaluating the variables
on the arcs and in the transition conditions to algebra values.
Denition 3.2
(Firing of AHLI nets)
.
A consistent transition assignment
(t, asg)∈CT
for an AHLI net
ANI = (Σ, P, T, pre, post, cond, type, A, I, m)
is
enabled
under a
token selection
(M, m, N, n)
, where
•M⊆I
,
•m
is the token mapping of
ANI
,
•N
is a set with
(I\M)∩N=∅
,
•n:N→A⊗P
is a function,
3.1. DEFINITION AND FIRING BEHAVIOR
21
if it meets the following
token selection condition
:
X
i∈M
m(i) = preA(t, asg)∧X
i∈N
n(i) = postA(t, asg)
If such an
asg
-enabled
t
res, the follower marking
(I0, m0)
is given by
I0= (I\M)∪N, m0:I0→A⊗P
with
m0(x) = (m(x), x ∈I\M
n(x), x ∈N
leading to
ANI 0= (AN, I0, m0)
as the new AHLI net in the
ring step
ANI i
−
t,asg
−−−→ ANI 0
via
(M, m, N, n)
.
Remark
(Token Selection)
.
The purpose of the token selection is to specify exactly which
tokens should be consumed and produced in the ring step. Thus,
M⊆I
selects the
individual tokens to be consumed, and
N
contains the set of individual tokens to be
produced. Clearly,
(I\M)∩N=∅
must hold because it is impossible to add an
individual token to a net that already contains this token.
m
and
n
relate the tokens to
their place/value pairs. It would be sucient to consider only the restriction
m|M
here
or to infer it from the net but as a compromise on symmetry and readability we denote
m
in the token selection.
As a preparation for the transformation in the next subsection, we dene a category
of AHLI nets.
Denition 3.3
(AHLI Net Morphisms and Category
AHLINets
)
.
Given two AHLI nets
ANI i= (Σi, Pi, Ti, prei, posti, condi, typei, Ai, Ii, mi)
,
i∈ {1,2}
,
an AHLI net morphism
f:ANI 1→ANI 2
is a pentuple
f= (fΣ: Σ1→Σ2, fP:P1→P2, fT:T1→T2, fA:A1→VfΣ(A2), fI:I1→I2)
such that the following diagrams commute (componentwise for
prei
and
posti
)
13
:
13
VfΣ
is the forgetful functor induced by signature homomorphism
fΣ
, such that
fA:A1→VfΣ(A2)
is
a generalized
Σ1
-homomorphism.
f#
Σ
is the extension of
fΣ
to terms and equations.
22
3. ALGEBRAIC HIGH-LEVEL NETS WITH INDIVIDUAL TOKENS
Pfin(Eqns(Σ1))
Pfin(f#
Σ)
T1
cond1
oo
fT
pre1//
post1
//(TOP1(X1)⊗P1)⊕
(f#
Σ⊗fP)⊕
Pfin(Eqns(Σ2)) T2
cond2
oopre2//
post2
//(TOP2(X2)⊗P2)⊕
P1
type1//
fP
S1
fΣ
I1
fI
m1//A1⊗P1
fA⊗fP
P2type2
//S2I2
m2//A2⊗P2
For a transition assignment
(t, asg :X1→A1)
we call
asgf=fA◦asg ◦f−1
Σ|V ar(t):V ar(fT(t)) →A2
the
translation
of
asg
along
f
if
fΣ
is bijective on the variables in
V ar(t)
. Actually, for
all transitions
t∈T1
all
fΣ|V ar(t):V ar(t)→V ar(fT(t))
are already surjective because
of the commutativity of the diagrams above. So it is sucient to demand injectivity for
fΣ|V ar(t)
such that
asgf
is well-dened.
The category
AHLINets
consists of all AHLI nets as objects and all AHLI net mor-
phisms.
Remark
(Generalized algebra morphisms)
.
Because
VfΣ(A2)
just forgets some carrier
sets of
A2
if we considered them as a family of sets, we may use
fA
also with
A2
as
codomain omitting the postponed family of identities
(ιs: (VfΣ(A2))s→A2,fΣ(s))s∈S
.
Moreover, in the following constructions the algebra parts of the pushout cospan (and
the pullback span resp.) result from general constructions in the Grothendieck construct
with objects
(Σ, A ∈Alg(Σ))
and generalized algebra morphisms. See [EBO92, TBG91]
for amalgamation of algebras and limits/colimits in Grothendieck constructs and also
[EM85, EOP06] for details on the usage of free functors.
Fact 3.4
(Construction of Pushouts in
AHLINets
)
.
Pushouts in
AHLINets
are constructed componentwise in
AHLNets
and
Sets
. So,
(1)
is a PO in
AHLINets
i
(2)
is a PO in
AHLNets
and
(3)
is a PO in
Sets
with the
components of the
AHLINets
morphisms, where
m3:I3→A3⊗P3
is induced by PO
object
I3
in the commutating cube below (whose front's place components let the front
commutate because of the PO in the net structure).
3.2. TRANSFORMATION OF AHLI NETS
23
ANI 0
f1//
f2
(1)
ANI 1
g1
ANI 2g2
//ANI 3
AN0
f0
1//
f0
2
(2)
AN1
g0
1
AN2g0
2
//AN3
I0
f1I//
f2I
(3)
I1
g1I
I2g2I
//I3
I0
f1I//
f2I
m0
##
I1
g1I
m1
##
A0⊗P0
f1A⊗f1P//
f2A⊗f2P
A1⊗P1
g1A⊗g1P
I2g2I
//
m2##
I3
m3
##
A2⊗P2g2A⊗g2P
//A3⊗P3
If
f1X
, for
X∈ {P, T, I}
, is injective then
g2X
is as well and similar for components
of
f2
and
g1
and the other diagrams.
For the construction of pushouts in
AHLNets
we refer to [PER95].
Example.
Figure 7 on page 30 shows two pushouts in
AHLINets
.
Fact 3.5
(Construction of Pullbacks in
AHLINets
)
.
Pullbacks in
AHLINets
along injective
AHLNets
morphisms
14
are constructed com-
ponentwise in
AHLNets
and
Sets
.
Consider a commutative square
(1)
in
AHLINets
with
g0
1
being injective.
(1)
is a PB
in
AHLINets
i
(2)
is a PB in
AHLNets
and
(3)
is a PB in
Sets
with the components
of the
AHLINets
morphisms, where
m0:I0→A⊗P0
is induced by PB object
P0
in
the commutating cube below (whose front's place components let the front commutate
because of the PB in the net structure).
ANI 0
f1//
f2
(1)
ANI 1
g1
ANI 2g2
//ANI 3
AN0
f0
1//
f0
2
(2)
AN1
g0
1
AN2g0
2
//AN3
I0
f1I//
f2I
(3)
I1
g1I
I2g2I
//I3
I0
f1I//
f2I
m0
##
I1
g1I
m1
##
A0⊗P0
f1A⊗f1P//
f2A⊗f2P
A1⊗P1
g1A⊗g1P
I2g2I
//
m2##
I3
m3
##
A2⊗P2g2A⊗g2P
//A3⊗P3
Example.
The pushouts in Fig. 7 on page 30 are pullbacks, too.
3.2. Transformation of AHLI Nets
This section is about rule-based transformation of AHLI nets. For this, we use the
double pushout approach, which has also been used for
collective
AHL nets in [PER95]
14
We require morphisms that are injective on the net structure in order to obtain componentwise pull-
backs in
AHLNets
. See [EEPT06] for details.
24
3. ALGEBRAIC HIGH-LEVEL NETS WITH INDIVIDUAL TOKENS
and which has been investigated in the context of
M
-adhesive systems in [EEPT06]. We
are going to characterize the applicability of rules at some match by initial pushouts.
Denition 3.6
(AHLI Transformation Rules)
.
An AHLI transformation rule is a span of injective
AHLINets
morphisms
%= (Ll
←Kr
→R).
Remark.
AHLI Rule morphisms are not required to be marking-strict in order to obtain
an
M
-adhesive category (see Sect. 5 on page 41). This allows to arbitrarily change the
marking of an AHLI net by applying rules with corresponding places and individual
tokens in
L
and
R
.
Denition 3.7
(AHLI Transformation)
.
Given an AHLI transformation rule
%= (Ll
←Kr
→R)
and an AHLI net
ANI 1
with a
AHLI net morphism
m:L→ANI 1
, called the match, a direct AHLI net transformation
ANI 1=
%,m
==⇒ANI 2
from
ANI 1
to the AHLI net
ANI 2
is given by the following double-
pushout diagram (DPO) diagram in the category
AHLINets
:
L
m
(PO1)
K
(PO2)
l
oo
r//R
m∗
ANI 1ANI0
oo//ANI 2
To be able to decide whether a rule is applicable at a certain match, we formulate
a gluing condition for AHLI nets, such that there exists a pushout complement of the
left rule morphisms and the match if (and only if) they fulll the gluing condition. The
correctness of the gluing condition is shown via a proof on initial pushouts over matches,
according to [EEPT06].
Denition 3.8
(Gluing Condition in
AHLINets
)
.
Given AHLI nets
K, L
, and
ANI
and AHLI morphisms
l:K→L
and
f:L→ANI
.
We dene the set of identication points
15
IP =IPP∪IPT∪IPI
with
•IPP={x∈PL| ∃x06=x:fP(x) = fP(x0)}
,
•IPT={x∈TL| ∃x06=x:fT(x) = fT(x0)}
,
•IPI={x∈IL| ∃x06=x:fI(x) = fI(x0)}
,
the set of dangling points
16
DP =DPT∪DPI
with
15
That is, all elements in
L
that are mapped non-injectively by
f
.
16
That is, all places in
L
that would leave a dangling arc, if deleted.
3.2. TRANSFORMATION OF AHLI NETS
25
•DPT={p∈PL| ∃t∈TANI \fT(TL) : fP(p)∈ENVP(t)}
,
•DPI={p∈PL| ∃i∈IANI \fI(IL) : fP(p) = πP(mANI (i))}
,
and the set of gluing points
17
GP =lP(PK)∪lT(TK)∪lI(IK)
We say that
l
and
f
satisfy the gluing condition if
IP ∪DP ⊆GP
. Given an AHLI rule
%= (Ll
←Kr
→R)
, we say that
%
and
f
satisfy the gluing condition i
l
and
f
satisfy
the gluing condition.
L
f
K
l
oor//R
ANI
In order to construct the initial pushout for a match
f:L→ANI
, we dene the
boundary
over the match
f
, which is the minimal subnet containing all places, transitions,
and individual tokens that must not be deleted by the application of a rule with left hand
side
L
such that there exists a pushout complement.
Denition 3.9
(Boundary in
AHLINets
)
.
Given two AHLI nets
L= (ΣL, PL, TL, preL, postL, condL, typeL, AL, IL, mL),
ANI = (ΣANI , PANI , TANI , preANI , postANI , condANI , typeANI , AANI , IANI , mANI )
and an AHLI morphism
f:L→ANI
. The boundary of
f
is an AHLI net
B= (ΣB, PB, TB, preB, postB, condB, typeB, AB, IB, mB)
with
•ΣB= ΣL
,
•PB=DPT∪DPI∪IPP∪PIP T∪PIPI
•PIPT={p∈PL| ∃t∈IPT:p∈ENVP(t)}
•PIPI={p∈PL| ∃i∈IPI:p=πP(mL(i))}
•TB=IPT
•preB(t) = preL(t)
•postB(t) = postL(t)
17
That is, all elements in
L
that have a preimage in
K
.
26
3. ALGEBRAIC HIGH-LEVEL NETS WITH INDIVIDUAL TOKENS
•condB(t) = condL(t)
•typeB(p) = typeL(p)
•AB=AL
•IB=IPI
•mB(i) = mL(i)
together with
b:B→L= (bΣ, bP, bT, bA, bI)
where
bΣ=idΣB
,
bA=idAB
, and the
remaining parts are inclusions.
Well-denedness.
preB, postB:TB→(TOPB(XB)⊗PB)⊕
:
Let
t∈TB
and let
(term, p)≤preB(t)
. Then there is
(term, p)≤preL(t)
which
means that
term ∈TOPL(XL)
and
p∈PL
. Then from
ΣB= ΣL
follows that
term ∈TOPB(XB)
. Furthermore there is
t∈IPT
which by the fact that
p∈
ENVP(t)
means that
p∈PIPT⊆PB
.
So
preB
is well-dened. The proof for
postB
works completely analogously.
condB:TB→ Pfin(Eqns(ΣB))
:
Let
t∈TB
. Then we have
condB(t) = condL(t)∈ Pfin(Eqns(ΣL)) = Pfin(Eqns(ΣB))
typeB:PB→SB
:
Let
p∈PB
. Then we have
typeB(p) = typeL(p)∈SL=SB
mB:IB→AB⊗PB
:
Let
i∈IB
and let
(a, p) = mB(i)
. Then there is
(a, p) = mL(i)
which means that
a∈AtypeL(p)=AtypeB(p)
. The fact that
p∈PB
follows from the fact that
i∈IPI
and hence
p∈PIPI⊆PB
.
inclusion
b:B→L
:
We obtain an inclusion morphism
b:B→L
from the fact that
preB
,
postB
,
condB
,
typeB
,
and
mB
are restrictions of the respective functions in
L
.
The following facts about the gluing condition and initial pushouts hold in all
M
-
adhesive categories
(AHLINets,M)
whose morphism class
M
of monomorphisms con-
tains at least inclusions with identities for signature and algebra parts (for concrete
instantiations see Sect. 5 on page 41). The next fact completes the construction of initial
pushouts for matches and shows that the construction of the boundary in Def. 3.9 on the
previous page complies to the categorical notion of boundaries in Def. A.1 on page 49.
3.2. TRANSFORMATION OF AHLI NETS
27
Fact 3.10
(Initial Pushout in
AHLINets
)
.
Given a morphism
f:L→ANI
in
AHLINets
, the boundary
B
of
f
and the AHLI net
C= (ΣC, PC, TC, preC, postC, condC, typeC, AC, IC, mC)
with
•ΣC= ΣANI
•PC= (PANI \fP(PL)) ∪fP(bP(PB))
•TC= (TANI \fT(TL)) ∪fT(bT(TB))
•preC(t) = preANI (t)
•postC(t) = postANI (t)
•condC(t) = condANI (t)
•typeC(p) = typeANI (p)
•AC=AANI
•IC= (IANI \fI(IL)) ∪fI(bI(IB))
•mC(i) = mANI (i)
Then diagram (1) is an initial pushout in
AHLINets
, where
g:= f|B
and
c
is an
inclusion with
cΣ=idΣC
and
cA=idAC
.
Bb//
g
L
f
Cc//
(1)
ANI
Proof.
See section B.3.
The following two facts show the correspondence between the gluing condition in
AHLINets
and the categorical gluing condition (see Def. A.2 on page 49), which is
a necessary and sucient condition for the (unique) existence of pushout complements
in
M
-adhesive categories.
Fact 3.11
(Characterization of Gluing Condition in
AHLINets
)
.
Let
l:K→L
and
f:L→ANI
be morphisms in
AHLINets
with
l∈ M
.
The morphisms
l
and
f
satisfy the gluing condition in
AHLINets
if and only if they
satisfy the categorical gluing condition.
Proof.
See section B.4.
28
3. ALGEBRAIC HIGH-LEVEL NETS WITH INDIVIDUAL TOKENS
Fact 3.12
(Gluing Condition for AHLI Transformation)
.
Given an AHLI rule
%= (Ll
←Kr
→R)
and a match
f:L→ANI
into an AHLI net
ANI = (AN, I, m :I→PAN )
. The rule
%
is applicable on match
f
, i.e. there exists a
(unique) pushout complement
ANI 0
in the diagram below, i
%
and
f
satisfy the gluing
condition in
AHLINets
.
L
f
(P O)
K
l
oo
f0
r//R
ANI ANI 0
oo
Proof.
By Fact 3.11 the rule
%
and match
f
satisfy the gluing condition in
AHLINets
if and only if
%
and
f
satisfy the categorical gluing condition, which by Fact A.3 is a
sucient and necessary condition for the existence of a (unique) pushout complement
ANI 0
.
3.3. Correspondence of Transition Firing and Rules
Now that we can manipulate a net's marking with rules, we have a look at rules that
simulate ring steps for a certain transition under a token selection. We show that ring
of a transition corresponds to a canonical application of a special rule construction, called
transition rules. With this correspondence we can easily show that token-injective AHLI
morphisms preserve ring steps.
Denition 3.13
(AHLI Transition Rules)
.
Given an AHLI net
ANI = (Σ, P, T, pre, post, cond, type, A, I, m)
we dene the
transition rule
for a consistent transition assignment
(t, asg)∈CTANI
,
enabled under the token selection
S= (M, m, N, n)
, as the rule
%(t, S, asg)=(Lt
l
←Kt
r
→Rt)
with
•
the common xed AHL net part
AN t= (Σ, Pt,{t}, pret, postt, typet, A)
, where
Pt=ENV P(t), pret(t) = pre(t), postt(t) = post(t), typet(p) = type(p)
,
•Lt= (AN t, M, mt:M→A⊗Pt)
, with
mt(x) = m(x)
,
•Kt= (AN t,∅,∅:∅ → (A×Pt))
,
•Rt= (AN t, N, nt:N→A⊗Pt)
, with
nt(x) = n(x)
,
•l, r
being the obvious inclusions on the rule nets.
3.3. CORRESPONDENCE OF TRANSITION FIRING AND RULES
29
mt
and
nt
are well-dened because
t
is enabled under
S
: The token selection condition
implies that
∀x∈M:m(x)∈PREA(t, asg)
and due to the construction of
AN t
we have
PREA(t, asg)⊆(A⊗ENV P(t)) = (A⊗Pt)
. The argument for
nt
works analogously.
Note that
(t, asg)
is enabled under
S
in
Lt
.
Remark.
The structure of a transition rule depends only on the transition and the token
selection, for which there may exist several enabled transition assignments. Therefore
dierent consistent transition assignments may have the same correspondent transition
rule. Nevertheless, we denote an AHLI transition rule as
%(t, S, asg)
rather than
%(t, S)
to remember the concrete assignment this rule is intended to simulate.
Example.
Figure 7 shows an AHLI transition rule
%(t, S, asg) = (Ll
←Kr
→R)
.
Denition 3.14
(Canonical DPO Transformation of AHLI Nets)
.
We call a direct transformation
ANI 1=
%,f
=⇒ANI 2
by rule
%= (Ll
←Kr
→R)
with
l, r
being inclusions
canonical
if
•fI
is injective,
•fΣ
is injective on the set of variables of
ΣANI 1
18
•
the morphisms in the span
(ANI 1←ANI0→ANI 2)
of the DPO transformation
diagram below are inclusions, and
•I2=I0∪(IR\r(IK))
.
L
f
(PO1)
K
(PO2)
l
oo
r//R
f∗
ANI 1ANI0
oo//ANI 2
Remark.
For each rule
%
being applied to some AHLI net
ANI
at a token-injective match
f
, there exists a canonical transformation diagram, which is just the particular equivalent
DPO diagram with as less isomorphic changes as possible.
Because of the injectivity of the rule morphisms the lower span in the diagram is
already injective as well. To construct the canonical transformation diagram we rst
regard the last condition on
I2
, which demands that
(IR\r(IK)) ∩I0=∅
because of
pushout
PO2
. For this, it is sucient to replace the set of tokens in
R
that are created
by the rule, i.e.
IR\r(IK)
, such that it is disjoint to the tokens preserved by the rule,
i.e.
(I1\f(IL)) ∪f(l(IK))
.
19
With this we now can simply replace arbitrary
ANI 0
and
ANI 2
, being some pushout complement object of
PO1
and pushout object of
PO2
, with
nets such that the lower span morphisms become inclusions.
18
See the Context Condition in [EP97].
19
This modication of the rule is passable since changing the tokens in
R
does not aect the ring
behavior of
NI2
(up to the token selections) nor the applicability of the rule.
30
3. ALGEBRAIC HIGH-LEVEL NETS WITH INDIVIDUAL TOKENS
Example.
The following diagram shows the two pushouts in
AHLINets
resulting from
applying the AHL transition rule
%(t, S, asg)=(Ll
←Kr
→R)
for
asg ={t11 7→ a1, t12 7→ b1, t27→ a2, t37→ a3}
to the net
ANI
. All nets in this diagram have the same signature and algebra as the
example net in Fig. 6 on page 20. Moreover, this transformation is canonical.
L
t
p1:
s1
p2:
s2
p3:
s3
t11⊕t12 t2
t3
x1y1x2
b1a2
a1
(PO1)
K
t
p1:
s1
p2:
s2
p3:
s3
t11⊕t12 t2
t3
(PO2)
l
oo
r//
R
t
p1:
s1
p2:
s2
p3:
s3
t11⊕t12 t2
t3
x3a3
ANI
t
p1:
s1
p2:
s2
p3:
s3
t11⊕t12 t2
t3
x1y1x2
y3
b1a2
a1
b3
z1
c1
y2
b2
t
p1:
s1
p2:
s2
p3:
s3
t11⊕t12 t2
t3
y3
b3
z1
c1
y2
b2
oo//
t
p1:
s1
p2:
s2
p3:
s3
t11⊕t12 t2
t3
y3
b3
z1
c1
y2
x3a3
b2
Figure 7: Canonical direct DPO-transformation in
AHLINets
simulating a ring step
Theorem 3.1
(Equivalence of Canonical Transformations and Firing of AHLI Nets)
.
1. Each ring step
ANI i
−
t,asg
−−−→ ANI 0
via token selection
S= (M, m, N, n)
corresponds to
a canonical direct transformation
ANI =
%(t,S,asg),f
=======⇒ANI 0
via the transition rule
%(t, S, asg)
matched by the inclusion match
f:L→ANI
.
2. Each canonical direct transformation
ANI =
%(t,S,asg),f
=======⇒ANI 1
, via some transition rule
%(t, S, asg) = (Ll
←Kr
→R)
with
t∈TANI
and token selection
S= (M, m, N, n)
,
and token-injective match
f:L→ANI
, implies the consistent transition assignment
(fT(t), asgf)
being enabled in
ANI
under
fI(M),(fA⊗fP)◦m◦f−1
I, N, (f∗
A⊗f∗
P)◦m1◦f∗−1
I
3.3. CORRESPONDENCE OF TRANSITION FIRING AND RULES
31
with ring step
ANI i
−
fT(t),asgf
−−−−−−−→ ANI 1
. With
asgf
we denote the translation of
asg
along
f
, i.e.
asgf=fA◦asg ◦f−1
Σ|V ar(t)
.
Proof.
1. Given the ring step
ANI i
−
t,asg
−−−→ ANI 0
via
(M, m, N, n) = S
, the canonical direct
transformation of the transition rule
%(t, S, asg)
is
ANI =
%(t,asg),f
=====⇒ANI 1
as in the DPO
diagram in Fig. 8. The match
f
,
d
, and
d0
are inclusions.
L= (AN t, M, mt)
f
(PO1)
K= (AN t,∅,∅)
(PO2)
?_
l
oo
r//R= (AN t, N, nt)
f∗
ANI = (AN , I, m)ANI 0= (AN , I0, m0)
?_
d
oo
d0//ANI 1= (AN , I1, m1)
Figure 8: DPO diagram for canonical direct transformation of
ANI
with
%(t, S, asg)
in
AHLINets
According to Fact 3.4 on page 22, we have
I0=I\M
and
I1=I0∪(N\ ∅)
as in the
DPO diagram of the
Sets
components in Fig. 9. The ring step condition
(I\M)∩N=∅
grants us the last condition for canonical transformations
I0∪(N\r(∅)) = I1
.
M
fI
(PO1)
∅
(PO2)
?_
oo
//N
f∗
I
nt
))
I
m,,
I0= (I\M)
?_
dI
oo
d0
I
//
m0=m◦dI
((
I1= (I\M)∪N
m1))
At⊗Pt
f∗
A⊗f∗
P=fA⊗fP
AAN ⊗PAN id
+3AAN ⊗PAN
Figure 9: DPO diagram in
Sets
for the token components of the transformation in Fig. 8
For
m1
as induced morphism for the pushout object
I1
follows that
m1(x) = (m0(x) = m(x)
for
x∈I\M
nt(x) = n(x)
for
x∈N
hence
I1=I0, m1=m0
and
ANI 1=ANI 0
, according to Def. 3.2 on page 20.
Remark.
fI
being injective is not only sucient for the existence of
(PO1)
, but also
necessary, because
IK=∅
(see Fact 3.12 on page 28).
2. Consider a canonical direct transformation
ANI =
%(t,S,asg),f
=======⇒ANI 1
with
ANI = (Σ, P, T, pre, post, cond, type, A, I, m)
as in the DPO diagrams in Figs. 8 and 9.
(fT(t), asgf)∈CTANI
is enabled under
fI(M),(fA⊗fP)◦m◦f−1
I, N, (f∗
A⊗f∗
P)◦m1◦f∗−1
I
32
3. ALGEBRAIC HIGH-LEVEL NETS WITH INDIVIDUAL TOKENS
if
1.
fI(M)⊆I
,
2.
(fA⊗fP)◦m◦f−1
I:N→A⊗P
,
3.
(I\fI(M)) ∩N=∅
,
4.
P
i∈fI(M)(fA⊗fP)◦m◦f−1
I(i)=preA(fT(t), asgf)
5.
P
i∈N(f∗
A⊗f∗
P)◦m1◦f∗−1
I(i)=postA(fT(t), asgf)
6. leading to the follower marking
I0= (I\M)∪N
with
m0(x) = (m0(x) = m(x)
for
x∈I\M
m1(x) = n(x)
for
x∈N
By construction of the transition rule
%(t, S, asg)
and its application to
ANI
we have 1.,
2., and for 6. that
I0=I1, m0=m1
. The canonical transformation property grants us
3. It remains to show 4. and 5., i.e. that
fI(M)
and
N
represent the correct numbers of
value/place pairs in the environment of
fT(t)
to enable it when evaluated with
asgf
:
X
i∈fI(M)
(fA⊗fP)◦m◦f−1
I(i)
=X
i∈M
(fA⊗fP)◦m(i) (fI
inj.
)
= (fA⊗fP)⊕X
i∈M
mt(i) (∀i∈M:mt(i) = m(i),
due to def.
p(t, S, asg))
= (fA⊗fP)⊕◦(asg ×idP)⊕◦preAN t(t) ((t, asg)
enabled in
L)
= (asgf×idP)⊕◦(f#
Σ⊗fP)⊕◦preAN t(t) (
Lemma 3.2
)
= (asgf×idP)⊕◦pre ◦fT(t) (f
AHLI morph.
)
=preA(fT(t), asgf) (
def.
preA)
3.3. CORRESPONDENCE OF TRANSITION FIRING AND RULES
33
and analogously,
X
i∈N
(f∗
A⊗f∗
P)◦m1◦f∗−1
I(i)
=X
i∈N
(f∗
A⊗f∗
P)◦m1(i) (f∗
I(N) = N)
= (f∗
A⊗f∗
P)⊕X
i∈M
nt(i) (∀i∈N:nt(i) = m1(i),
due to constr.
m1)
= (f∗
A⊗f∗
P)⊕◦(asg ×idP)⊕◦preAN t(t) ((t, asg)
enabled in
L)
= (asgf×idP)⊕◦(f#
Σ⊗fP)⊕◦postAN t(t) (
Lemma 3.2
)
= (asgf×idP)⊕◦post ◦fT(t) (f
AHLI morph.
)
=postA(fT(t), asgf) (
def.
postA)
Lemma 3.2
(Translated Assignments)
.
Given two AHLI nets
ANI i= (Σi= (Si, OPi, Xi), Pi, Ti, prei, posti, condi, typei, Ai, Ii, mi), i ∈ {1,2}
a transition assignment
(t, asg :X1→A1)∈CT ANI1
, and an AHLI net morphism
f= (fΣ, fP, fT, fA, fI) : ANI 1→ANI 2
with
fΣ
injective on the variables of
V ar(t)
, it
holds for all terms
term ∈TOP1(V ar(t))
that
asgf◦f#
Σ(term) = fA◦asg(term),
where
asgf=fA◦asg◦f−1
Σ|V ar(t):V ar(fT(t)) →A2
Proof by structural induction over all
Σ1
terms over variables of
V ar(t)
.
20
First, note that
because
(fΣ, fA)
is a generalized algebra homomorphism we have for all constants
c
and
operations
op
in
OP1
fA(cA1)fA
homomorph.
=cVfΣ(A2)
def.
VfΣ
= (fΣ(c))A2
(1)
fA◦opA1
fA
homomorph.
=opVfΣ(A2)◦fA
def.
VfΣ
= (fΣ(op))A2◦fA
(2)
Case 1:
t=x∈V ar(t)
fA◦asg(x) = fA◦asg(x) = fA◦asg ◦f−1
Σ|V ar(t)◦f#
Σ(x)
because
fΣ|V ar(t):V ar(t)→V ar(fT(t))
is surjective due to
f
being a net morphism and
hence
fΣ
bijective on variables in
V ar(t)
.
Case 2:
t= (c:→s)∈TOP1
fA◦asg(c) = fA(cA1)(1)
= (fΣ(c))A2= (f#
Σ(c))A2=asgf◦f#
Σ(c)
The last equality holds because a constant
c
would be evaluated by the extension of just
any variable assignment to
cA2
.
20
A categorical proof using free constructions can be found in [EP97].
34
3. ALGEBRAIC HIGH-LEVEL NETS WITH INDIVIDUAL TOKENS
Case 3:
t=op(t1, . . . , tn)∈TOP1(V ar(t))
with
t1, . . . , tn
satisfying the property to be
proven.
fA◦asg(op(t1, . . . , tn)) = fA◦opA1(asg(t1), . . . , asg(tn))
(2)
=(fΣ(op))VfΣ(A2)(fA◦asg(t1), . . . , fA◦asg(tn))
ind.assumpt.
= (fΣ(op))VfΣ(A2)(asgf◦f#
Σ(t1), . . . , asgf◦f#
Σ(tn))
=asgf(fΣ(op)) (f#
Σ(t1), . . . , f#
Σ(tn))
=asgf◦f#
Σ(op(t1, . . . , tn))
The second item of the previous theorem covers all possible canonical direct transfor-
mations by any transition rule
%(t, S, asg)
in an arbitrary net
ANI
, without aasuming
that
t∈ANI
or
M⊆INI
. For the special case that a transition rule
%(t, S, asg)
is
applied on an inclusion match, the second item reduces to the following corollary, which
is more similar to the theorem's rst item.
Corollary 3.3
(Equivalence of Canonical Transformations and Firing of AHLI Nets)
.
Given a canonical transformation
ANI =
%(t,S,asg),f
=======⇒ANI 1
such that the match
f:L→ANI
is an inclusion, then the consistent token assignment
(t, asg)
is enabled in
ANI
under
S
with ring step
ANI i
−
t,asg
−−−→ ANI 1
.
This follows directly from 2. of Theorem 3.1.
Theorem 3.4
(Token-injective AHLI Net Morphisms preserve Firing Steps)
.
For each AHLI net morphism
f:ANI 1→ANI 2
, such that
fI
is injective and
fΣ
is
injective on all sets
V ar(t)
for all
t∈T1
21
, and each ring step
ANI 1i
−
t,asg
−−−→ ANI 0
1
there
exists a ring step
ANI 2i
−
fT(t),asgf
−−−−−−−→ ANI 0
2
and a AHLI net morphism
f0:ANI 0
1→ANI 0
2
(depicted in diagram (1) below).
ANI 1//t,asg //
f
(1)
ANI 0
1
f0
ANI 2//fT(t),asgf
//ANI 0
2
Proof.
Given
f:ANI 1→ANI 2
and
ANI 1i
−
t,asg
−−−→ ANI 0
1
via some
S
as above, we have
by the rst part of Theorem 3.1 on page 30 the canonical direct transformation with
%(t, S, asg)=(Ll
←Kr
→R)
given by the pushouts
(1)
and
(2)
in Fig. 10 on the facing
page.
Note that
f:ANI 1→ANI 2
satises the gluing condition w.r.t
l0
, because
l0
P=idP1, l0
T=idT1
and
IPI=∅
due to injectivity of
fI
. This allows to construct the
21
See the Context Condition in [EP97].
35
L
incL
(1)
K
(2)
l
oo
r//R
incR
ANI 1
f
(3)
ANI D1
l0
oor0//
(4)
ANI 0
1
f0
ANI 2ANI D2
oo//ANI 0
2
Figure 10: Double pushout diagrams for canonical direct transformation of
ANI 1
and
ANI 2
with
%(t, S, asg)
canonical transformation with extended rule
ANI 1
l0
←ANI D1
r0
→ANI 0
1
along pushouts
(3)
and
(4)
. Hence, also
(1 + 3)
and
(2 + 4)
are pushouts, dening a canonical direct
transformation via
%(t, S, asg)
. The second part of Theorem 3.1 on page 30 implies
ANI 2i
−
fT(t),asgf
−−−−−−−→ ANI 0
2
.
Remark
(Firing-preserving diagrams for
(t, asg)
correspond to an extension diagram for
%(t, asg)
)
.
The diagram in Fig. 10 corresponds to an extension diagram for rule
%(t, asg)
and
f
(as depicted below) because
(1) −(4)
are pushouts.
ANI 1
%(t,asg),inc +3
f
ANI 0
1
f0
ANI 2
%(t,asg),f◦inc+3ANI 0
2
4. Functors for Individual Net Classes
PTI and AHLI nets are still very close to their
collective
pendants. In this section, we
express this vicinity with functors. In addition we dene a attening functor from AHLI
to PTI nets, similar to the attening of AHL nets, that preserves enabling and ring and
nally show a compatibility result for these functors.
Denition and Fact 4.1
(
CollPT :PTINetsI→PTSys
)
.
The following construction attens a PTI net to a P/T net with collective marking and
forgets the individual token elements. We can translate nets with a nite number of
tokens on each place, only:
CollPT (P, T, pre, post, I, m) = P, T, pre, post, M =X
i∈I
m(i)∈P⊕!,
if
∀p∈P:|m−1(p)| ∈ N
.
Now, we extend the construction to a functor
CollPT :PTINetsI→PTSys
.
PTSys
is the category of P/T nets with a marking
M∈P⊕
, where
P⊕
is the commutative
36
4. FUNCTORS FOR INDIVIDUAL NET CLASSES
monoid over the set of places. Morphisms in
PTSys
are pairs
(fP:P1→P2, fT:T1→T2) : N1→N2
that are compatible to the nets'
pre
and
post
mappings (just as PTI morphisms) and
preserve markings placewise, i.e.
∀p∈P1:MN1(p)≤MN1(fP(p))
.
Because markings of nets in
PTSys
can only describe nitely many tokens on each
place of the net, we dene as domain of the functor the category
PTINetsI
of PTI
nets with nitely many tokens on each place (such that
∀p∈P:|m−1(p)| ∈ N
) and
token-injective PTI morphisms. For the morphisms, we just have to forget the individual
token component by dening
CollPT (f:NI 1→NI 2) = (fP, fT) : CollPT (NI 1)→CollPT (NI 2).
Proof.
Obviously,
CollPT (f)
is well-dened on the net structure parts of
CollPT (NI 1)
and
CollPT (NI 2)
. Furthermore, it holds that
∀p∈P1:M1(p) = |m−1
1(p)|≤|m−1
2(fP(p))|=M2(fP(p)).
The inequality is valid because each token
x
on place
p
implies a unique image
fI(x)
on
fP(p)
due to the PTI morphism properties and because
fI
being injective does not
merge token images in
I2
.
The compositionality follows directly from the componentwise composition of PTI net
morphisms.
Theorem 4.1
(
CollPT
preserves Enabling and Firing)
.
Given a PTI net
NI = (P, T, pre, post, I, m)∈PTINetsI,
each valid token selection
(M, m, N, n)
enabling a ring
NI i
−
t
→NI 0
implies the ring
CollPT (NI )i
−
t
→CollPT (NI 0)
.
Proof.
1.
t
is enabled in
CollPT (NI )
:
pre(t)t
enabled
=X
i∈M
m(i)M⊆I
≤X
i∈I
m(i)
def.
CollPT
=MCollPT (NI )
2. Firing of
t
results in
CollPT (NI 0)
: Obviously, for the ring step
CollPT (NI )i
−
t
→g
PN
the net structure parts of
g
PN
are the same as of
CollPT (NI 0)
. It remains to show the
equality of their markings. We have
INI 0= (I\M)]N, m0:INI 0→P
with
m0(x) = (m(x), x ∈I\M
n(x), x ∈N
37
which we use to show that
Mg
PN
=MCollPT (NI )pre(t)⊕post(t)
=X
i∈I
m(i)X
i∈M
m(i)⊕X
i∈N
n(i) (
def.
CollPT , t
enabled
)
=X
i∈I\M
m(i)⊕X
i∈N
n(i)
=X
i∈(I\M)]N
m0(i) (
def.
m0)
=MCollPT (NI 0)(
defs.
INI 0, CollPT )
Remark.
Because the only condition for
t
to be enabled in
CollPT (NI )
is that
∀p∈P:pre(t)(p)≤P
i∈I
m(i)(p)
, there are possibly many dierent valid token
selections corresponding to the same ring step of
t
in
CollPT (NI )
, depending only on
isomorphic
N
and
n
.
Denition and Fact 4.2
(
CollAHL :AHLINetsI→AHLSys
)
.
The following construction attens a AHLI net to a AHL net with collective marking
and forgets the individual token elements. We can translate nets with a nite number of
each value/place pairs, only:
CollAHL(AN , I, m) = AN , M =X
i∈I
m(i)∈(A⊗P)⊕!,
if
∀(a, p)∈A⊗P:|m−1(a, p)| ∈ N.
Now, we extend the construction to a functor
CollAHL :AHLINetsI→AHLSys
.
AHLSys
is the category of AHL nets with a marking
M∈(A⊗P)⊕
, where
(A⊗P)⊕
is
the commutative monoid over pairs of values from the net's algebra and the net's places
of compatible type. Morphisms in
AHLSys
are tuples
(fΣ: Σ1→Σ2, fP:P1→P2, fT:T1→T2, fA:A1→A2) : AN 1→AN 2
that comply to all compatibility properties of AHLI net morphisms (of course, ex-
cept the one regarding the individual token component) and that preserve markings
place/valuewise, i.e.
∀(a, p)∈A1⊗P1:MAN1(a, p)≤MAN2(fA⊗fP(a, p)).
Because markings of nets in
AHLSys
can only describe nitely many tokens on each
place of the net, we dene as domain of the functor the category
AHLINetsI
of AHLI
nets with nitely many occurrences of each value/place pair, i.e.
∀(a, p)∈A⊗P:|m−1(a, p)| ∈ N,
38
4. FUNCTORS FOR INDIVIDUAL NET CLASSES
and AHLI morphisms that are injective on tokens and variables
22
. For the morphisms,
we just have to forget the individual token component by dening
CollAHL(f:ANI 1→ANI 2) = (fΣ, fP, fT, fA) : CollAHL(ANI 1)→CollAHL(ANI 2).
Proof.
Obviously,
CollAHL(f)
is well-dened on the net structure parts of
CollAHL(ANI 1)
and
CollAHL(ANI 2)
. All properties for AHL net morphisms are already valid for the cor-
respondent components of AHLI net morphisms.
The compositionality follows directly from the componentwise composition of AHLI
net morphisms.
Theorem 4.2
(
CollAHL
preserves Enabling and Firing)
.
Given an AHLI net
ANI = (Σ, P, T, pre, post, cond, type, A, I, m)∈AHLINetsI,
each valid token selection
(M, m, N, n)
with ring step
ANI i
−
(t,asg)
−−−−→ ANI 0
implies the
ring
CollAHL(ANI )i
−
(t,asg)
−−−−→ CollAHL(ANI 0)
.
Proof.
1.
(t, asg)
is enabled in
CollAHL(ANI ) :
preA(t, asg)(t,asg)
enabled
=X
i∈M
m(i)M⊆I
≤X
i∈I
m(i)
def.
CollAHL
=MCollAHL(ANI )
2. Firing of
(t, asg)
results in
CollAHL(ANI 0)
: Obviously, for the ring step
CollAHL(ANI )i
−
(t,asg)
−−−−→ ]
ANI
the net structure parts of
]
ANI
are the same as of
CollAHL(ANI 0)
.
It remains to show the equality of their markings. We have
IANI 0= (I\M)]N, m0:IANI 0→A⊗P
with
m0(x) = (m(x), x ∈I\M
n(x), x ∈N
which we use to show that
M]
ANI
=MCollAHL(ANI )preA(t, asg)⊕postA(t, asg)
=X
i∈I
m(i)X
i∈M
m(i)⊕X
i∈N
n(i) (
def.
CollAHL, t
enabled
)
=X
i∈I\M
m(i)⊕X
i∈N
n(i)
=X
i∈(I\M)]N
m0(i) (
def.
m0)
=MCollAHL(ANI 0)(
defs.
IANI 0, CollAHL)
22
We need injectivity on variables of a signature for the attening of AHLI morphisms.
39
Denition and Fact 4.3
(
FlatI:AHLINetsI→PTINetsI
)
.
The following construction attens an AHLI net to a PTI net:
FlatI(AN , I, m)=(CP,CT , preA, postA, I, m)
Note that
(CP,CT , preA, postA) = Flat(AN )
and
m:I→(A⊗P) = CP
.
To extend the construction to a functor
FlatI:AHLINetsI→PTINetsI
, we dene
for each
f= (fΣ, fP, fT, fA, fI) : ANI 1→ANI 2
the attening
FlatI(f) = (fA⊗fP, fT×fA◦
_
◦f−1
Σ|V ar(t), fI) : FlatI(ANI 1)→F latI(ANI 2).
Proof.
To prove that
FlatI(f:ANI 1→ANI 2) : FlatI(ANI 1)→FlatI(ANI 2)
is a valid PTI net morphism, we have to show the following equalities:
fI◦m1=m2◦(fA⊗fP)
and
(fA⊗fP)⊕◦preA1=preA2◦fT×fA◦
_
◦f−1
Σ|V ar(t),
analogously for
postA
. The rst one follows directly from
f
being a AHLI morphism.
For the second one we have for all
(t, asg)∈CT1
that
preA2◦fT×fA◦
_
◦f−1
Σ|V ar(t)(t, asg)
=preA2fT(t), fA◦asg ◦f−1
Σ|V ar(t)
=preA2(fT(t), asgf)
abbrev.
asgf=fA◦asg ◦f−1
Σ|V ar(t)
= (asgf, idP2)⊕◦pre2◦fT(t) (
def.
preA2)
= (asgf, idP2)⊕◦(f#
Σ⊗fP)⊕◦pre1(t) (f
AHLI morph.
)
=
n
X
i=1 asgf◦f#
Σ(termi), fP(pi)
for
n
X
i=1
(termi, pi) = pre1(t)
=
n
X
i=1
(fA◦asg(termi), fP(pi)) (
Lemma 3.2
)
= (fA⊗fP)⊕◦(asg, idP1)⊕◦pre1(t)
= (fA⊗fP)⊕◦preA1(t, asg) (
def.
preA1)
and analogously for
postA
. The compositionality follows directly from the componentwise
composition of AHLI net morphisms.
40
4. FUNCTORS FOR INDIVIDUAL NET CLASSES
Theorem 4.3
(
FlatI
preserves and reects Enabling and Firing)
.
Given an AHLI net
ANI = (AN , I, m)
with
FlatI(AN , I, m)=(CN , I, m)
and a token
selection
S= (M, m, N, n)
, the following holds:
1.
(t, asg)∈CT
is enabled under
S
in
ANI
, i
(t, asg)
is enabled under
S
in
FlatI(ANI )
.
2.
ANI i
−
(t,asg)
−−−−→ (AN , I0, m0)
via
S⇔(CN , I, m)i
−
(t,asg)
−−−−→ (CN , I0, m0)
via
S
.
Proof.
1.
(t, asg)∈CT
is enabled under
S
in
(AN , I, m)
⇔P
i∈M
m(i) = preA(t, asg)∧P
i∈N
n(i) = postA(t, asg)
⇔(t, asg)∈CT
is enabled under
S
in
FlatI(AN , I, m) = (CP,CT , preA, postA, I, m)
2.
(AN , I, m)i
−
(t,asg)
−−−−→ (AN , I0, m0)
via
S
⇔(t, asg)
enabled under
S
in both
ANI
and
FlatI(ANI )
,
and
I0= (I\M)]N, m0(x) = (m(x), x ∈I\M
n(x), x ∈N
⇔FlatI(AN , I, m)=(CN , I, m)i
−
(t,asg)
−−−−→ (CN , I0, m0) = FlatI(AN , I0, m0)
via
S
Theorem 4.4
(Compatibility of Collection and Flattening Functors)
.
The previously dened functors are compatible, i.e.
CollPT ◦FlatI=F lat ◦CollAHL
.
AHLINetsI
F latI//
CollAHL
=
PTINetsI
CollPT
AHLSys F lat //PTSys
Proof.
Given an AHLI net
ANI = (Σ, P, T, pre, post, cond, type, A, I, m)∈AHLINetsI
,
we have
CollPT ◦FlatI(ANI )
=CollPT (CP,CT, preA, postA, I, m) (
def.
FlatI)
= CP,CT , preA, postA, M =X
i∈I
m(i)∈(A⊗P)⊕!(
def.
CollPT )
=Flat Σ, P, T, pre, post, cond, type, A, M =X
i∈I
m(i)!(
def.
Flat)
=Flat ◦CollAHL(ANI ) (
def.
CollAHL)
and for some AHL net morphism
f= (fΣ, fP, fT, fA, fI) : ANI 1→ANI 2
with injective
41
fI
we have
CollPT ◦FlatI(f)
=CollPT (fA⊗fP, fT×fA◦
_
◦f−1
Σ|V ar(t), fI) (
def.
FlatI)
= (fA⊗fP, fT×fA◦
_
◦f−1
Σ|V ar(t)) (
def.
CollPT )
=Flat(fΣ, fP, fT, fA) (
def.
Flat)
=Flat ◦CollAHL(f) (
def.
CollAHL)
5. Nets with Individual Tokens are
M
-adhesive Categories
[Pra08] shows how to construct a marking category for
collective
Petri nets, which can
be used to prove the properties of
M
-adhesive categories, i.e. weak adhesive high-level
replacement systems in the sense of [EEPT06], for marked Petri nets. In this section we
present a similar construction for individual markings and show some instantiations of
M
-adhesive categories for PTI and AHLI nets.
Denition 5.1
(Individual Petri Systems)
.
Given a category
Nets
of nets, an
individual system
IS = (N, I, m)
is given by a net
N∈Nets
, a set of individuals
I
, and a function
m:I→M(N)
, where
M:Nets →Sets
is a functor assigning a marking set to each net
N
.
For systems
IS1= (N1, I1, m1)
and
IS2= (N2, I2, m2)
, an individual system morphism
fIS = (fN, fI) : IS1→IS2
consists of a net morphisms
fN:N1→N2
and a function on
the individuals
fI:I1→I2
such that
M(fN)◦m1=m2◦fI
as depicted below.
I1
m1//
fI
=
M(N1)
M(fN)
I2
m2//M(N2)
All individual systems and system morphisms constitute the category
ISystems(Nets, M)
.
Theorem 5.1
(
ISystems(Nets, M)
is
M
-adhesive)
.
Given an
M
-adhesive category
(Nets,M)
of nets with a marking set functor
M:Nets →Sets
that preserves pullbacks along
M
-morphisms, then the category
(ISystems(Nets, M),M×Minj)
of individual systems over these nets is
M
-adhesive as well, where
Minj
is the class of
all injective functions.
Proof.
Consider the comma category
C=ComCat(IDSets, M, {m})
, with objects
(I, N, opm:I→M(N))
and morphisms
fC= (fI, fN)∈MorSets ×MorNets
.
Obviously,
C
is isomorphic to
ISystems(Nets, M)
.
42
5. NETS WITH INDIVIDUAL TOKENS ARE
M
-ADHESIVE CATEGORIES
By applying Thm. 1.4 (Construction of [Weak] Adhesive HLR Categories) from [PEL08],
we can conclude that
(C,M×Minj)
is
M
-adhesive because
•(Nets,M)
and
(Sets,Minj)
are
M
-adhesive categories,
•
the functor
IDSets
preserves pushouts along injective functions, and
•
the functor
M:Nets →Sets
preserves pullbacks along
M
-morphisms.
Hence,
(ISystems(Nets, M),M×Minj)
is
M
-adhesive as well.
Theorem 5.2
(
PTINets
is
M
-adhesive)
.
The category
(PTINets,Minj)
is an
M
-adhesive category where
Minj ={f∈MorPTINets|fP, fT, fI
injective
}
Proof.
We already know from [Pra08] that
(PTNets,M0)
is
M
-adhesive with
M0
being
the class of all injective Petri net morphisms. Given the functor
M:PTNets →Sets
with
M(P, T, pre, post) = P
, we have
PTINets ∼ISystems(PTNets, M)
.
M
preserves pullbacks along
M0
-morphisms because pullbacks along injective mor-
phisms are constructed componentwise in
PTNets
, hence Thm. 5.1 states that
(PTINets,Minj)
is
M
-adhesive.
For PTI net transformation systems we require rules with rule morphisms in
M
and
one of the following alternatives for matches:
1. general matches by PTI morphisms,
2. injective matches by
M
,
3. token-injective matches by
M0={f∈PTINets|fI
inj.
}
For all three cases we have a suitable theory by DPO transformations with general,
M
-matching resp.
M0
-matching in
M
-adhesive categories.
Theorem 5.3
(
AHLINets(Σ)
is
M
-adhesive)
.
For a xed signature
Σ
the category
(AHLINets(Σ),MI)
is an
M
-adhesive category
where
•AHLINets(Σ)
is the full subcategory of
AHLINets
containing all AHLI nets
with the signature
Σ
,
• MI={f∈MorAHLINets(Σ)|fΣ=idΣ, fA
isomorphic, and
fP, fT, fI
injective
}
.
Proof.
As shown in [Pra08], we already know that the category
(AHLNets(SP),M0)
of
AHL nets over a specication
SP
is
M
-adhesive with
M0={f∈MorAHLNets(SP)|fA
isomorphic, and
fP, fT
injective
}.
43
Given the functor
M:AHLNets(Σ,∅)→Sets
with
M(P, T, pre, post, cond, type, A) = A⊗P,
we have
AHLINets(Σ)∼ISystems(AHLNets(Σ,∅), M)
.
M
preserves pullbacks
along
M0
-morphisms because pullbacks along injective morphisms are constructed com-
ponentwise in
AHLNets(Σ,∅)
and we have only algebra isomorphisms in
M0
. Hence,
Thm. 5.1 states that
(AHLINets(Σ),MI)
is
M
-adhesive.
Theorem 5.4
(
AHLINets
is
M
-adhesive)
.
The category
(AHLINets,MI)
is a
M
-adhesive category where
MI={f∈MorAHLINets|fΣ
injective
, fA
isomorphic, and
fP, fT, fI
injective
}
Proof.
As shown in [Pra08], we already know that the category of generalized AHL nets
(AHLNets,M0)
is
M
-adhesive with
M0={f∈MorAHLNets|fSP
strict injective
, fA
isomorphic, and
fP, fT
injective
}.
We consider its full subcategory
(AHLNets∅,M0|AHLNets∅)
of generalized AHL nets
with empty sets of specication equations, which by Thm. 2.3(i) from [Pra08] is itself
M
-adhesive. Note that all injective morphisms between specications without equations
are strict.
Given the functor
M:AHLNets∅→Sets
with
M(SP, P, T, pre, post, cond, type, A) = A⊗P,
we have
AHLINets ∼ISystems(AHLNets∅, M)
.
M
preserves pullbacks along
M0|AHLNets∅
-morphisms because pullbacks along injective morphisms are constructed
componentwise in
AHLNets∅
and we have only algebra isomorphisms in
M0
. Hence,
Thm. 5.1 states that
(AHLINets,MI)
is
M
-adhesive.
6. Conclusion
In this article, we have introduced low- and high-level Petri nets with markings of indi-
vidual tokens. The Petri net approach we presented is related to [vGP95, BMMS99] but
in contrast the individual tokens in our framework are part of the syntactical denition
of the Petri nets.
With the individuals being part of a net's syntax, we can consider Petri nets with an
individual marking as objects of a category. Based on the double pushout transformation
approach, we are able to dene the rule based transformation for low- and high-level Petri
nets with individual tokens. Important results are a necessary and sucient condition
that we give for the applicability of rules and other results that follow from the properties
of
M
-adhesive categories, because we are able to show that our Petri net categories are
M
-adhesive, which is a short notion for weak adhesive HLR categories in [EEPT06].
44
7. FUTURE WORK
The main advantage of the presented Petri net transformation approach over previous
existing double pushout approaches (with collective markings) is that the marking of
a net with individual tokens can be manipulated with rules, which is not possible in an
adequate way with the collective token approach. So, ring steps of Petri nets with
individual tokens can be simulated with rules. Moreover, we proved a correspondence
between such transition productions and ring steps.
We related the newly presented and existing net classes with functors and showed that
they preserve enabling and ring.
7. Future Work
Although we have given some
M
-adhesive categories of Petri nets with individual tokens,
which allows us to use many interesting results for analysis of transformations, there
are several useful additional properties and recent developments that are worthwhile to
consider to examine if the presented categories comply to them.
Application Conditions
In [EHL10], the results of [EEPT06] concerning parallel and
concurrent rules have been lifted to transformation systems with rules with nested ap-
plication conditions (see also [HP09]). The only additional property for
M
-adhesive
categories that is needed for these results is an
E
-
M
factorization (and binary coprod-
ucts which we already have by cocompleteness).
Morphism pair factorization
There are several useful theorems as the Concurrency
Theorem and the Local Conuence Theorem, for which we need an
E0
-
M0
pair factor-
ization. Unfortunately, for the
M
-adhesive categories in this article we can not simply
apply the construction Thm. 4 from [PEL08] because for the individual marking functor
M
(cf. Def. 5.1 on page 41) establishing the constructed comma category does not in
general yield an isomorphism
M(f)
for a Petri net morphism
f
.
So for all these results, for transformation systems with or without application condi-
tions, it may be convenient to directly prove an epi-
M
factorization, which (with binary
coproducts) would directly constitute a
E0
-
M0
pair factorization with
E0
as the class of
jointly epimorphic morphisms.
Another possibility is to consider only nets with a nite structure, i.e. the nets with
nite sets of places, transitions, and individuals, which is the kind of nets mostly used in
practical cases. In an
M
-adhesive category as given above, nite objects are the objects
with a nite number of
M
-subobjects, which in the case of nets are exactly the nets with
nite structure. As shown in [BEGG10], the restriction of an
M
-adhesive category to
all its nite objects allows already to give a general construction for
E
-
M
factorizations
and for initial pushouts.
Rule amalgamation
Another powerful concept is the amalgamation of rules (with ap-
plication conditions) over a bundle of matches, which has been elaborated in [Gol10]. In
References
45
order to instantiate the results in this article to our Petri net categories we need to show
that they have so-called eective pushouts.
References
[AB09] Andrea Asperti and Nadia Busi. Mobile petri nets.
Mathematical Structures
in Computer Science
, 19(6):12651278, 2009.
[BDHM06] P. Bottoni, F. De Rosa, K. Homann, and M. Mecella. Applying Algebraic
Approaches for Modeling Workows and their Transformations in Mobile
Networks.
Journal of Mobile Information Systems
, 2(1):5176, 2006.
[BEE
+
09] Enrico Biermann, Hartmut Ehrig, Claudia Ermel, Kathrin Homann, and
Tony Modica. Modeling Multicasting in Dynamic Communication-based
Systems by Recongurable High-level Petri Nets. In
IEEE Symposium on
Visual Languages and Human-Centric Computing, VL/HCC 2009, Cor-
vallis, OR, USA, 20-24 September 2009, Proceedings
, pages 4750. IEEE,
2009.
[BEGG10] Benjamin Braatz, Hartmut Ehrig, Karsten Gabriel, and Ulrike Golas. Fini-
tary
M
-Adhesive Categories. In H. Ehrig, R. Heckel, G. Rozenberg, and
G. Taentzer, editors,
Proc. International Conference on Graph Transfor-
mation (ICGT'10)
, volume 5214 of
LNCS
, Heidelberg, 2010. Springer. to
appear.
[BMMS99] R. Bruni, J. Meseguer, U. Montanari, and V. Sassone. Functorial semantics
for petri nets under the individual token philosophy. In
Category Theory
and Computer Science, CTCS '99.
, volume 29 of
ENTCS
, page 18 pp.
Elsevier, 1999.
[EBO92] H. Ehrig, M. Baldamus, and F. Orejas. New concepts for amalgamation
and extension in the framework of specication logics. In
Proc. WADT-
COMPASS-Workshop Dourdan, 1991
, pages 199221. Springer LNCS 655,
1992.
[EEPT06] H. Ehrig, K. Ehrig, U. Prange, and G. Taentzer.
Fundamentals of Algebraic
Graph Transformation
. EATCS Monographs in Theoretical Computer Sci-
ence. Springer Verlag, 2006.
[EHL10] Hartmut Ehrig, Anngegret Habel, and Leen Lambers. Parallelism and Con-
currency Theorems for Rules with Nested Application Conditions.
Electr.
Communications of the EASST
, 26, 2010.
[EHP
+
08] H. Ehrig, K. Homann, J. Padberg, C. Ermel, U. Prange, E. Biermann,
and T. Modica. Petri Net Transformations. In
Petri Net Theory and
Applications
, pages 116. I-Tech Education and Publication, 2008.
46
References
[EM85] H. Ehrig and B. Mahr.
Fundamentals of Algebraic Specication 1: Equa-
tions and Initial Semantics
, volume 6 of
EATCS Monographs on Theoretical
Computer Science
. Springer, Berlin, 1985.
[EOP06] H. Ehrig, F. Orejas, and U. Prange. Categorical Foundations of Dis-
tributed Graph Transformation. In A. Corradini, H. Ehrig, U. Montanari,
L. Ribeiro, and G. Rozenberg, editors,
Proc. Third International Confer-
ence on Graph Transformation (ICGT'06)
, volume 4178 of
LNCS
, pages
215 229, Natal, Brazil, September 2006. Springer.
[EP97] C. Ermel and J. Padberg. Formalization of Variables in Algebraic High-
Level Nets. Technical Report 97-19, Technical University Berlin, 1997.
[EPR93] H. Ehrig, J. Padberg, and L. Ribeiro. Algebraic high-level nets: Petri
nets revisited. In
Proc. of the ADT-COMPASS Workshop'92 (Caldes de
Malavella, Spain)
, Berlin, 1993. Technical Report TUB93-06.
[Gol10] U. Golas. Multi-Amalgamation in
M
-Adhesive Categories. Technical Re-
port 2010/05, Technische Universität Berlin, 2010.
[GR83] Ursula Goltz and Wolfgang Reisig. The Non-sequential Behavior of Petri
Nets.
Information and Control
, 57(2/3):125147, 1983.
[HB08] Awatef Hicheur and Kamel Barkaoui. Modelling collaborative workows
using recursive ecatnets. In
NOTERE '08: Proceedings of the 8th interna-
tional conference on New technologies in distributed systems
, pages 111,
New York, NY, USA, 2008. ACM.
[HME05] K. Homann, T. Mossakowski, and H. Ehrig. High-Level Nets with Nets
and Rules as Tokens. In
Proc. of 26th Intern. Conf. on Application and
Theory of Petri Nets and other Models of Concurrency
, volume 3536 of
LNCS
, pages 268288. Springer, 2005.
[HP00] Serge Haddad and Denis Poitrenaud. Modelling and analyzing systems with
recursive petri nets. In
In Proc. of the Workshop on Discrete Event Systems
- Analysis and Control
, pages 449458. Kluwer Academics Publishers, 2000.
[HP09] Annegret Habel and Karl-Heinz Pennemann. Correctness of high-level
transformation systems relative to nested conditions.
Mathematical Struc-
tures in Computer Science
, 19:152, 2009.
[KR07] Michael Köhler and Heiko Rölke. Dynamic transition renement.
Electron.
Notes Theor. Comput. Sci.
, 175(2):119134, 2007.
[MEE
+
10] Tony Modica, Claudia Ermel, Hartmut Ehrig, Kathrin Homann, and En-
rico Biermann. Modeling communication spaces with higher-order petri
nets. In George E. Lasker and Jochen Pfalzgraf, editors,
Advances in Mul-
tiagent Systems, Robotics and Cybernetics: Theory and Practice
, volume
References
47
III, Tecumseh, Canada, 2010. The International Institute for Advanced
Studies in Systems Research and Cybernetics. to appear.
[MM90] J. Meseguer and U. Montanari. Petri Nets are Monoids.
Information and
Computation
, 88(2):105155, 1990.
[Mod10] Tony Modica. Towards formal algebraic modeling and analysis of com-
munication spaces. In Magne Haveraaen, Marina Lenisa, John Power,
and Monika Seisenberger, editors,
CALCO Young Researchers Workshop
(CALCO-jnr 2009) Selected Papers
, number 5-2010 in Technical Report,
pages 89103. Università di Udine Dipartimento di Matematica e Infor-
matica, 2010.
[PEL08] U. Prange, H. Ehrig, and L. Lambers. Construction and Properties of
Adhesive and Weak Adhesive High-Level Replacement Categories.
Applied
Categorical Structures
, 16(3):365388, 2008.
[PER95] J. Padberg, H. Ehrig, and L. Ribeiro. Algebraic high-level net transfor-
mation systems.
Mathematical Structures in Computer Science
, 5:217256,
1995.
[Pra08] U. Prange. Towards algebraic high-level systems as weak adhesive HLR
categories. In H. Ehrig, J. Pfalzgraf, and U. Prange, editors,
Proceedings of
the ACCAT workshop at ETAPS 2007
, volume 203 / 6 of
Electronic Notes
in Theoretical Computer Science
, pages 6788, Amsterdam, 2008. Elsevier.
[Rei85a] Wolfgang Reisig.
Petri Nets: An Introduction
, volume 4 of
EATCS Mono-
graphs on Theoretical Computer Science
. Springer, 1985.
[Rei85b] Wolfgang Reisig. Petri Nets with Individual Tokens.
Theoretical Computer
Science
, 41:185213, 1985.
[Rei91] Wolfgang Reisig. Petri nets and algebraic specications.
Theoretical Com-
puter Science
, 80(1):134, March 1991.
[Syl09] Peggy Sylopp. Konzeption und Implementierung von Analysetechniken
für rekongurierbare Objektnetze. Diplomarbeit, Technische Universität
Berlin, 2009.
[TBG91] Andrzej Tarlecki, Rod M. Burstall, and Joseph A. Goguen. Some funda-
mental algebraic tools for the semantics of computation: Part 3: Indexed
categories.
Theoretical Computer Science
, 91(2):239264, 1991.
[Val78] Rüdiger Valk. Self-modifying nets, a natural extension of petri nets. In
Giorgio Ausiello and Corrado Böhm, editors,
ICALP, Automata, Languages
and Programming, Fifth Colloquium, Udine, Italy
, volume 62 of
Lecture
Notes in Computer Science
, pages 464476. Springer, 1978.
48
References
[vdABV
+
99] W. M. P. van der Aalst, T. Basten, H. M. W. Verbeek, P. A. C. Verkoulen,
and M. Voorhoeve. Adaptive Workow-On the Interplay between Flexibil-
ity and Support. In
Proc. of the Int. Conference on Enterprise Information
Systems (ICEIS'99)
, pages 353360, 1999.
[vG05] Robert Jan van Glabbeek. The individual and collective token interpre-
tations of petri nets. In
Proceedings CONCUR 2005, 16 th International
Conference on Concurrency Theory
, pages 323337, London, UK, 2005.
Springer-Verlag.
[vGP95] R. J. van Glabbeek and G. D. Plotkin. Conguration structures. In
LICS
'95: Proceedings of the 10th Annual IEEE Symposium on Logic in Com-
puter Science
, page 199, Washington, DC, USA, 1995. IEEE Computer
Society.
[vGP09] R. J. van Glabbeek and G. D. Plotkin. Conguration structures, event
structures and petri nets.
Theoretical Computer Science
, 410(41):4111
4159, 2009.
49
A. Appendix
A.1. Categorical Gluing Condition with Initial Pushouts
The following denitions, that can also be found in [EEPT06], provide notions to formu-
late an abstract categorical condition, the so-called gluing condition, which is necessary
and sucient for the (unique) existence of pushout complements in
M
-adhesive cate-
gories. The gluing condition is used to show that the corresponding set-theoretical glu-
ing conditions in the categories
PTNets
(see Def. 2.8 on page 10) and
AHLINets
(see
Def. 3.8 on page 24) are necessary and sucient conditions for the application of trans-
formation rules
%= (Ll
←Kr
→R)
in suitable
M
-adhesive categories
(PTINets,M)
(see Fact 2.11 on page 12) and
(AHLINets,M)
(see Fact 3.11 on page 27), respectively.
Denition A.1
(Boundary, Initial Pushout)
.
Given a morphism
f:L→G
in an
M
-adhesive category, a morphism
b:B→L
with
b∈ M
is called the
boundary
over
f
if there is a pushout complement of
f
and
b
such
that (1) is a pushout which is
initial
over
f
. Initiality of (1) over
f
means, that for every
pushout (2) with
b0∈ M
there exist unique morphisms
b∗:B→D
and
c∗:C→E
with
b∗, c∗∈ M
such that
b0◦b∗=b, c0◦c∗=c
and (3) is a pushout.
B
is then called the
boundary object
and
c
the
context
with respect to
f
.
B
b//L
f
Cc//G
(1)
B
b∗//
b
))
D
b0//L
f
Cc∗//
c
55
E
(3)
c0//G
(2)
Denition A.2
(Categorical Gluing Condition)
.
Let
l:K→L∈ M
and
f:L→G
be morphisms in a given
M
-adhesive category
C
with initial pushouts.
We say that
l
and
f
satisfy the categorical gluing condition if for the initial pushout (1)
over
f
there exists a morphism
b∗:B→K
such that
l◦b∗=b
.
B
g
b
//
b∗
))
L
f
K
l
oor//R
Cc//G
(1)
Given a production
%= (Ll
←Kr
→R)
, we say
%
and
f
satisfy the categorical gluing
condition, i
l
and
f
satisfy the categorical gluing condition.
Fact A.3
(Categorical Gluing Condition)
.
Given an adhesive HLR category
C
with initial pushouts, a match
f:L→G
satises
the categorical gluing condition with respect to
l:K→L∈ M
(or a production
50
A. APPENDIX
%= (Ll
←Kr
→R)
, respectively) if and only if the context object
D
exists, i.e. there is
a pushout complement (2) of
l
and
m
:
B
g
b
//
b∗
))
L
f
K
l
oo
k
r//R
Cc//
c∗
55
G
(1)
D
d
oo
(2)
If it exists, the context object
D
is unique up to isomorphism.
Proof.
See Theorem 6.4 in [EEPT06].
In order to show initiality of a pushout (1) over a morphism
f:L→G
with cor-
responding opposite morphism
B→C
in an
M
-adhesive category
C
(cf. Def. A.1 on
the preceding page), one has to show for every pushout (2) over
f
with correspond-
ing opposite morphism
D→E
, that there exist unique morphisms
b∗:B→D
and
c∗:C→E
forming a pushout (cf. Def. A.1). The following Lemma states the fact, that
the existence of the required morphism
c∗
induces the remaining requirements.
Lemma A.1
(Morphism-Pushout-Lemma)
.
Given pushouts (1) and (2) in an
M
-adhesive category
C
where
b, d ∈ M
.
If there is a morphism
c∗:C→E
with
c=e◦c∗
then this
c∗
is unique and
c∗∈ M
and
there exists a unique
b∗:B→D∈ M
with
b=d◦b∗
such that (3) is pushout in
C
.
Bb//
g
L
f
D
d
oo
h
Cc//
c∗
55
(1)
G E
e
oo
(2)
B
b
))
g
b∗//
(3)
D
h
d
//L
f
C
c
55
c∗//Ee//
(2)
G
Proof.
We use in the following that also
c, e ∈ M
due to pushouts (1) and (2) and the
fact that
M
-morphisms are closed under pushouts.
uniqueness of
c∗
:
Let
¯c:C→E
with
c=e◦¯c
. Then there is
e◦¯c=c=e◦c∗
which by the fact that
e
is a monomorphism implies that
¯c=c∗
.
unique morphism
b∗
:
Since
d∈ M
the pushout (2) is also a pullback and since (1) is a pushout there is
f◦b=c◦g=e◦c∗◦g
A.1. CATEGORICAL GLUING CONDITION WITH INITIAL PUSHOUTS
51
from the pullback property follows that there is a unique morphism
b∗:B→D
with
c∗◦g=h◦b∗
and
b=d◦b∗
leading to commuting diagram (3).
B
b
))
g
b∗//
(3)
D
h
d
//L
f
C
c
55
c∗//Ee//
(2)
G
b∗, c∗∈ M
:
The morphisms
b
and
c
are
M
-morphisms. So the fact that
b=d◦b∗
and
c=e◦c∗
together with the fact that
M
-morphisms are closed under decomposition implies
that
b∗, c∗∈ M
.
(3) is pushout
:
Since
c
is an
M
-morphism and
M
-morphisms are closed under decomposition due
to the fact that
c◦idC=c∈ M
there is
idC∈ M
. Consider the following cube:
Cc∗//
idC
EidE//
idE
E
e
B
g
==
b∗//
idB
D
h
<<
idD//
idD
D
h
<<
d
Cc∗//Ee//G
B
g
==
b∗//D
h
<<
d//L
f
<<
•
The left face is a pullback,
•
the right face is pullback (2),
•
the front left and back left faces are pullbacks,
•
the front right and back right faces are pullbacks because
d, e ∈ M
,
•
the bottom is the pushout (1),
•
and the morphisms
idC, d
and
e
are
M
-morphisms.
So the cube is a weak Van Kampen cube implying that the top face (3) of the cube
is a pushout in
C
.
52
A. APPENDIX
In the following two lemmas we show, that the constructions
(
_
]⊗
_
)⊕
and
Pfin(
_
])
,
which are used in the pre and post conditions, and conditions of AHLI nets, respectively,
are compositional. We need these properties for the proofs of Fact 3.10 on page 27 and
Fact 3.11 on page 27.
Lemma A.2
(Compositionality of
(
_
]⊗
_
)⊕
)
.
Given three AHLI nets
ANi= (Σi, Pi, Ti, prei, posti, condi, typei, Ii, Ai)
where
(i∈ {1,2,3})
together with signature morphisms
fΣ: Σ1→Σ2
,
gΣ: Σ2→Σ3
and functions
fP:P1→P2
,
gP:P2→P3
with
type2◦fP=fS◦type1
Then for all
n
X
i=1
(termi, pi)∈(TOP1(X1)⊗P1)⊕
there is
(g]
Σ⊗gP)⊕((f]
Σ⊗fP)⊕(
n
X
i=1
(termi, pi))) = ((gΣ◦fΣ)]⊗(gP◦fP))⊕(
n
X
i=1
(termi, pi))
Proof.
Let
n
X
i=1
(termi, pi)∈(TOP1(X1)⊗P1)⊕
Due to the freeness of
TOP1(X1)
there is
VfΣ(g]
Σ)◦f]
Σ= (fΣ◦gΣ)]
A.1. CATEGORICAL GLUING CONDITION WITH INITIAL PUSHOUTS
53
So we have
(g]
Σ⊗gP)⊕((f]
Σ⊗fP)⊕(
n
X
i=1
(termi, pi)))
= (g]
Σ⊗gP)⊕(
n
X
i=1
((f]
Σ)type1(pi)(termi), fP(pi)))
=
n
X
i=1
((g]
Σ)type2(fP(pi))((f]
Σ)type1(pi)(termi)), gP(fP(pi)))
=
n
X
i=1
((g]
Σ)fS(type1(pi))((f]
Σ)type1(pi)(termi)), gP(fP(pi)))
=
n
X
i=1
(VfΣ(g]
Σ)type1(pi)((f]
Σ)type1(pi)(termi)), gP(fP(pi)))
=
n
X
i=1
((VfΣ(g]
Σ)◦f]
Σ)type1(pi)(termi), gP(fP(pi)))
=
n
X
i=1
((gΣ◦fΣ)]
type1(pi)(termi), gP◦fP(pi))
= ((gΣ◦fΣ)]⊗(gP◦fP))⊕(
n
X
i=1
(termi, pi))
Lemma A.3
(Compositionality of
Pfin(
_
])
)
.
Given three AHLI nets
ANi= (Σi, Pi, Ti, prei, posti, condi, typei, Ii, Ai)
where
(i∈ {1,2,3})
together with signature morphisms
fΣ: Σ1→Σ2
and
gΣ: Σ2→Σ3
.
Then for all
E∈ Pfin(Eqns(Σ1))
there is
Pfin(g]
Σ)(Pfin(f]
Σ)(E)) = Pfin((gΣ◦fΣ)])(E)
Proof.
Let
E∈ Pfin(Eqns(Σ1))
. For
e= (tl, tr)∈Eqns(Σ1)
the extension
f]
Σ
of a
signature morphism
fΣ: Σ1→Σ2
to equations of
Σ1
is dened by
f]
Σ(e) = ((f]
Σ)s(tl),(f]
Σ)s(tr))
where
s
is the sort of terms
tl
and
tr
, i.e.
tl, tr∈TOP1(X1)s
. The function
(f]
Σ)s
on the
right hand side of the equation is the extension of
fΣ
to terms of type
s
, i.e.
(f]
Σ)s:TOP1(X1)s→VfΣ(TOP2(X2))s
54
A. APPENDIX
Due to the denition of the forgetful functor
VfΣ
there is
VfΣ(TOP2(X2))s=TOP2(X2)fS(s)
and hence there is
(f]
Σ)s:TOP1(X1)s→TOP2(X2)fS(s)
So we have
Pfin(g]
Σ)(Pfin(f]
Σ)(E)) = Pfin(g]
Σ)(Pfin(f]
Σ)({e|e∈E}))
=Pfin(g]
Σ)({((f]
Σ)s(tl),(f]
Σ)s(tl)) |(tl, tr)∈E})
={((g]
Σ)fS(s)((f]
Σ)s(tl)),(g]
Σ)fS(s)((f]
Σ)s(tr))) |(tl, tr)∈E}
={(VfΣ(g]
Σ)s((f]
Σ)s(tl)), VfΣ(g]
Σ)s((f]
Σ)s(tr))) |(tl, tr)∈E}
={((VfΣ(g]
Σ)◦f]
Σ)s(tl),(VfΣ(g]
Σ)◦f]
Σ)s(tr)) |(tl, tr)∈E}
={((gΣ◦fΣ)]
s(tl),(gΣ◦fΣ)]
s(tr)) |(tl, tr)∈E}
=Pfin((gΣ◦fΣ)])(E)
In the following two lemmas we show, that the constructions _
⊗
_ and _
]
preserve
monomorphisms, which is used in the proofs of Fact 3.10 on page 27 and Fact 3.11 on
page 27.
Lemma A.4
(_
⊗
_ preserves Monomorphisms)
.
Given two AHLI nets
ANi= (Σi, Pi, Ti, prei, posti, condi, typei, Ii, Ai)
where
(i∈ {1,2})
and a monomorphism
f= (fP, fT, fΣ, fA, fI) : AN1→AN2
in
AHLINets
.
Then
fA⊗fP:A1⊗P1→A2⊗P2
is a monomorphism in
Sets
.
Proof.
Let
(a1, p1),(a2, p2)∈A1⊗P1
with
(fA⊗fP)(a1, p1)=(a, p)=(fA⊗fP)(a2, p2)
Then there is
(fA,type1(p1)(a1), fP(p1)) = (fA⊗fP)(a1, p1)
= (a, p)
= (fA⊗fP)(a2, p2)
= (fA,type1(p2)(a2), fP(p1))
which means that
fA,type1(p1)(a1) = a=fA,type1(p2)(a2)
A.1. CATEGORICAL GLUING CONDITION WITH INITIAL PUSHOUTS
55
and
fP(p1) = p=fP(p2)
Since
f
is a monomorphism in
AHLINets
the function
fP
is injective implying that
p1=p2
. This means that
fA,type1(p2)(a1) = fA,type1(p1)(a1) = a=fA,type1(p2)(a2)
and since
f
is a monomorphism in
AHLINets
there is
fA,type1(p2)
injective implying
that
a1=a2
. Hence there is
(a1, p1) = (a2, p2)
implying that
fA⊗fP
is injective, i.e. it
is a monomorphism in
Sets
.
Lemma A.5
(_
]
preserves Monomorphisms)
.
Given a signature morphism
f: Σ1→Σ2
.
If
f
is a monomorphism in
Sig
then
f]:TOP1(X1)→Vf(TOP2(X2))
is a monomorphism
in
Alg(Σ1)
.
Proof.
Since monomorphisms in
Alg(Σ1)
are exactly the injective homomorphisms it is
sucient to show that
f]
is injective. Let
t1, t2∈TOP1(X1)s
with
f]
s(t1) = t=f]
s(t2)
The recursive denition of terms allows us to prove this property by a structural induction
over
t∈Vf(TOP2(X2))s=TOP2(X2)fS(s)
.
Basis.
•t=x∈X2,fS(s)
This means that there are
x1, x2∈X1,s
with
f]
s(x1) = x=f]
s(x2)
⇔fX(x1) = x=fX(x2)
and since
fX
is injective this means
t1=x1=x2=t2
.
•t=c
with
c:→fS(s)∈OP2
This means that for
i= 1,2
there are
ci:→s∈OP1
with
f]
s(c1) = c=f]
s(c2)
⇔fOP (c1) = c=fOP (c2)
and since
fOP
is injective this means
t1=c1=c2=t2
.
Hypothesis.
For
ti∈Vf(TOP2(X2))si=TOP2(X2)fS(si)(i= 1, . . . , n)
there is
f]
si(t1) = ti=f]
si(t2)⇒t1=t2
56
A. APPENDIX
Step.
Let
t=op(t1, . . . , tn)
with
op :fS(s1). . . fS(sn)→fS(s)∈OP2
and
ti∈TOP2(X2)fS(si)(i= 1, . . . , n)
.
Then from
f]
s(t1) = t=f]
s(t2)
follows that there are
opi:s1. . . sn→s∈OP1
(i= 1,2)
such that
f]
s(t1) = t=f]
s(t2)
⇔f]
s(op1(t1
1, . . . , tn
1)) = op(t1, . . . , tn) = f]
s(op2(t1
2, . . . , tn
2))
⇔fOP (op1)(f]
s1(t1
1), . . . , f]
sn(tn
1)) = op(t1, . . . , tn) = fOP (op2)(f]
s1(t1
2), . . . , f]
sn(tn
2))
⇔fOP (op1) = op =fOP (op2)∧ ∀i∈ {1, . . . , n}:f]
si(ti
1) = ti=f]
si(ti
2)
Due to the injectivity of
fOP
there is
op1=op2
and by the induction hypothesis
there is
ti
1=ti
2
for all
i∈ {1, . . . , n}
. Hence we have
t1=t2
.
A.2. Initial Pushouts in
Sets
In this section we dene a gluing condition in the category
Sets
and show, that the
satisfaction of the condition for a suitable
M
-adhesive category
(Sets,M)
is equivalent to
the categorical gluing condition. This provides a necessary and sucient condition for the
existence of (unique) pushout complements in
Sets
, which is used in the corresponding
facts of the set-based categories
PTINets
and
AHLINets
.
Denition A.4
(Gluing Condition in
Sets
)
.
Let
l:K→L
and
f:L→G
be morphisms in
Sets
with
l∈ M
.
We dene the set of identication points
IP ={x∈L| ∃x06=x:f(x) = f(x0)}
and the set of gluing points
GP =l(K)
We say that
l
and
f
satisfy the gluing condition if
IP ⊆GP
.
The following lemma provides a set-theoretical construction of pushout complements
in
Sets
, whereas the category-theoretical construction of pushout complements is dened
via a pushout over the boundary (see Theorem 6.4 in [EEPT06]).
Lemma A.6
(Pushout Complement in
Sets
)
.
Let
l:K→L
and
f:L→G
be morphisms in
Sets
.
There is a pushout complement
C
of
l
and
f
, if
l
and
f
satisfy the gluing condition.
If a pushout complement exists it can be computed by
C= (G\f(L)) ∪f(l(K))
together with inclusion
c:C→G
and a morphism
g:K→C
with
g(x) = f(l(x))
for
every
x∈K
.
A.2. INITIAL PUSHOUTS IN
SETS
57
L
f
K
l
oo
g
G C
c
oo
(1)
Proof.
We dene
C
,
c
and
g
as above. We have to show that (1) is pushout in
Sets
.
commutativity of (1)
:
Let
x∈L
.
f(l(x)) = g(x) = c(g(x))
universal property
:
Let
H
be a set together with morphisms
c0:C→H
and
f0:L→H
with
c0◦g=f0◦l
We dene a morphism
h:G→H
with
h(x) = (c0(x)
, if
x∈C;
f0(x0)
, for
f(x0) = x
otherwise.
For the well-denedness of
h
we have to check if for every
x∈G
with
x /∈C
there
is a unique
x0∈L
such that
f(x0) = x
.
x /∈C
def.
C
⇔x /∈(G\f(L)) ∪f(l(K))
⇔ ¬x∈(G\f(L)) ∪f(l(K))
⇔ ¬(x∈G\f(L)∨x∈f(l(K)))
⇔x /∈G\f(L)∧x /∈f(l(K))
From the fact that
x∈G
and
x /∈G\f(L)
we have
x∈f(L)
which means that
there is
x0∈L
with
f(x0) = x
.
Let us assume that
x0
is not unique, i.e. there is
x00 ∈L
with
x06=x00
and
f(x00) = x
.
Then
x0
is an identication point which implies that
x0∈GP =f(l(K))
because
l
and
f
satisfy the gluing condition. This is a contradiction and hence
x0
is unique.
L
f
f0
K
l
oo
g
G
h
~~
(2)
(3)
C
c
oo
(1)
c0
nn
H
58
A. APPENDIX
Let
x∈C
. Then there is
h◦c(x) = h(x) = c0(x)
which means that diagram (2) commutes.
Let
x∈L
. Then we distinguish the following cases:
•
Case 1
:
x∈l(K)
Then there is
k∈K
with
l(k) = x
and
h(f(x)) = h(f(l(k))) = h(c(g(k))) = c0(g(k)) = f0(l(k)) = f0(x)
•
Case 2
:
x /∈l(K)
Then there is
f(x)/∈C
and therefore
h(f(x)) = f0(x)
Hence diagram (3) commutes.
For the uniqueness of
h
let
h0:G→H
with
h0◦c=c0
and
h0◦f=f0
.
Let
x∈G
.
•
Case 1
:
x∈C
h0(x) = h0(c(x)) = c0(x) = h(x)
•
Case 2
:
x /∈C
As we have shown above in this case there is a unique
x0∈L
with
f(x0) = x
and we obtain
h0(x) = h0(f(x0)) = f0(x0) = h(x)
So we have for all
x∈G
that
h0(x) = h(x)
and hence
h0=h
.
In the following denition and facts we dene the boundary and initial pushout over
a morphism
f:L→G
in
Sets
and show that the satisfaction of the gluing condition
in
Sets
is equivalent to the satisfaction of the categorical gluing condition in an
M
-
adhesive category
(Sets,M)
where the class of monomorphisms
M
contains inclusions.
A suitable class
M
is the class containing all monomorphisms in
Sets
, because
Sets
is
an adhesive category (see Theorem 4.6 in [EEPT06]).
Denition A.5
(Boundary in
Sets
)
.
Given a morphism
f:L→G
in
Sets
. The boundary
B
of
f
is the set
B=IP
of
identication points together with an inclusion
b:B→L
.
A.2. INITIAL PUSHOUTS IN
SETS
59
Fact A.6
(Initial Pushout in
Sets
)
.
Given a morphism
f:L→G
in
Sets
, the boundary
B
of
f
and the pushout complement
C
of
f
and
b
, dened as
C= (G\f(L)) ∪f(l(K))
together with inclusion
c:C→G
and a morphism
g:K→C
with
g(x) = f(l(x))
for
every
x∈K
.
Then diagram (1) is initial pushout in
Sets
.
Bb//
g
L
f
Cc//
(1)
G
Proof.
(1) is pushout
:
The fact that (1) is pushout follows from Lemma A.6 by the fact that
b
and
f
satisfy the gluing condition. It remains to show that (1) is initial.
Let (2) be a pushout in
Sets
with
d∈ M
.
Bb//
g
L
f
D
d
oo
h
Cc//
(1)
G E
e
oo
(2)
function
c∗
:
We dene a function
c∗:C→E
with
c∗(x) = y
with
e(y) = c(x)
well-denedness of
c∗
:
For the well-denedness of
c∗
we have to show that for every
x∈C
there is a
unique
y∈E
with
e(y) = c(x)
.
We distinguish the following cases for
x∈C
:
•
Case 1
:
x /∈f(L)
There is
c(x) = x∈G
. Since (2) is pushout in
Sets
the functions
f
and
e
are jointly surjective which by the fact that there is no
y∈L
with
f(y) = x
implies that there is
y∈E
with
e(y) = x=c(x)
.
•
Case 2
:
x∈f(b(B))
Then there is
z∈B
with
f(b(z)) = x
. From
z∈B=IP
and the fact that
E
is a pushout complement of
d
and
f
follows that
z∈d(D)
, i.e. there is
z0∈D
with
d(z0) = z
. Let
y=h(z0)
. Then we have
e(y) = e(h(z0)) = f(d(z0)) = f(z) = f(b(z)) = x=c(x)
60
A. APPENDIX
So for every
x∈C
there is a suitable element
y∈E
with
e(y) = c(x)
. Since
d∈ M
and pushouts in
Sets
are closed under
M
-morphisms there is also
e∈ M
, i.e.
e
is
injective which implies the uniqueness of
y
.
So
c∗
is well-dened. The fact that
e◦c∗=c
follows directly from the denition of
c∗
.
uniqueness of
c∗
, existence of
b∗
and pushout
:
By Lemma A.1 the morphism
c∗
is the unique morphism with
c=e◦c∗
and there
is a unique morphism
b∗:B→D
with
b=d◦b∗
such that (3) is a pushout in
Sets
.
B
b
))
g
b∗//
(3)
D
h
d
//L
f
C
c
55
c∗//Ee//
(2)
G
Hence diagram (1) is an initial pushout in
Sets
.
Fact A.7
(Characterization of Gluing Condition in
Sets
)
.
Let
l:K→L
and
f:L→G
be morphisms in
Sets
with
l∈ M
.
The morphisms
l
and
f
satisfy the gluing condition in
Sets
if and only if they satisfy
the categorical gluing condition.
Proof.
If.
Let
l
and
f
satisfy the categorical gluing condition, i.e. for initial pushout (1) there
is a function
b∗:B→K
with
l◦b∗=b
.
B
g
b
//
b∗
))
L
f
K
l
oo
Cc//G
(1)
Let
x∈IP
. Then there is
x∈B
and
y=b∗(x)∈K
with
l(y) = l(b∗(x)) = b(x) = x
which means that
x∈l(K) = GP
. Hence
l
and
f
satisfy the gluing condition in
Sets
.
Only If.
Let
l
and
f
satisfy the gluing condition in
Sets
, i.e. there is
IP ⊆GP =l(K)
.
We dene a function
b∗:B→K
with
b∗(x) = l−1(x)
A.3. INITIAL PUSHOUTS IN
PTNETS
61
For every
x∈B
there is
x∈IP
which by the fact that
l
and
f
satisfy the gluing
condition implies that
x∈GP =l(K)
, i.e. there is a preimage of
x
with respect to
l
. The preimage is unique since
l
is injective because
l∈ M
. Hence
b
is well-dened
and there is
l(b∗(x)) = l(l−1(x)) = x=b(x)
which means that
l
and
f
satisfy the categorical gluing condition.
A.3. Initial Pushouts in
PTNets
The construction and proof of the gluing condition for PTI nets (see Fact 2.12 on page 12)
allows to derive the corresponding result for P/T nets as a special case where the set of
individual tokens is empty.
Denition A.8
(Gluing Condition in
PTNets
)
.
Given P/T nets
K, L
and
G
and P/T morphisms
l:K→L
and
f:L→G
. We dene
the set of identication points
IP =IPP∪IPT
with
•IPP={x∈PL| ∃x06=x:fP(x) = fP(x0)}
,
•IPT={x∈TL| ∃x06=x:fT(x) = fT(x0)}
,
the set of dangling points
DP ={p∈PL| ∃t∈TG\fT(TL) : fP(p)∈ENV (t)}
and the set of gluing points
GP =lP(PK)∪lT(TK)
We say that
l
and
f
satisfy the gluing condition if
IP ∪DP ⊆GP
.
Denition A.9
(Boundary in
PTNets
)
.
Given a morphism
f:L→G
in
PTNets
. The boundary of
f
is a P/T net
B= (PB, TB, preB, postB)
with
•PB=DPT∪IPP∪PIP T
•PIPT={p∈PL| ∃t∈IPT:p∈ENV (t)}
•TB=IPT
62
A. APPENDIX
•preB(t) = preL(t)
•postB(t) = postL(t)
together with an inclusion
b:B→L
.
Well-denedness.
preB, postB:TB→P⊕
B
:
Let
t∈TB
and let
p≤preB(t)
. Then there is
p≤preL(t)
which means that
p∈PL
. Then there is
t∈IPT
which, by the fact that
p∈ENV (t)
, means that
p∈PIPT⊆PB
.
So
preB
is well-dened. The proof for
postB
works completely analogously.
inclusion
b:B→L
:
We obtain an inclusion morphism
b:B→L
from the fact that
preB
and
postB
are restrictions of the respective functions in
L
.
Fact A.10
(Initial Pushout in
PTNets
)
.
Given a morphism
f:L→G
in
PTNets
, the boundary
B
of
f
and the P/T net
C= (PC, TC, preC, postC)
with
•PC= (PG\fP(PL)) ∪fP(bP(PB))
•TC= (TG\fT(TL)) ∪fT(bT(TB))
•preC(t) = preG(t)
•postC(t) = postG(t)
Then diagram (1) where
g:= f|B
is initial pushout in
PTNets
.
Bb//
g
L
f
Cc//
(1)
G
Proof.
Analogously to Fact 2.10 with
I=∅
.
Fact A.11
(Characterization of Gluing Condition in
PTNets
)
.
Let
l:K→L
and
f:L→G
be morphisms in
PTNets
with
l∈ M
.
The morphisms
l
and
f
satisfy the gluing condition in
PTNets
if and only if they satisfy
the categorical gluing condition.
Proof.
Analogously to Fact 2.11 with
I=∅
.
B. PROOFS
63
B. Proofs
B.1. Proof of Fact 2.10
In this section we prove the well-denedness of the PTI net
C
dened in Fact 2.10 and
that the construction leads to an initial pushout in the category
PTINets
.
Proof.
well-denedness of
C
:
preC, postC:TC→P⊕
C
:
Follows from the well-denedness of
C
in Fact A.10 and the fact that we have
the same set of transitions, and the set of places in Fact A.10 is a subset of
PC
.
mC:IC→PC
:
Let
i∈IC
. Then there is
i∈(INI \fI(IL)) ∪fI(bI(IB))
.
Case 1
:
i /∈fI(IL)
Case 1.1
:
∃p∈PL:fP(p) = mNI (i)
This means that
p∈DP
and therefore
p∈PB
and
fP(p)∈PC
. So
we have
mC(i) = mNI (i) = fP(p)∈PC
Case 1.2
:
@p∈PL:fP(p) = mNI (i)
This means that
mNI (i)/∈fP(PL)
and hence
mC(i) = mNI (i)∈PC
.
Case 2
:
i∈fI(bI(IB))
Then there exists
j∈IB
with
fI(bI(j)) = i
and we have for
mC(i) = mNI (i)
that
mNI (i) = mNI (fI(bI(j))) = fP(mL(bI(j))) = fP(bP(mB(j)))
and since
fP(bP(PB)) ⊆PC
there is
mC(i)∈PC
.
well-denedness of
c
:
We obtain an inclusion morphism
c:C→NI
from the fact that
preC, postC
and
mC
are restrictions of the respective functions in
NI
.
well-denedness of
g
:
For
J={P, T, I}
we obtain well-dened functions
gJ:JB→JC
because for
j∈JB
there is
gJ(j) = fJ(j) = fJ(bJ(j)) ∈JC
The morphism
g
preserves pre and post domains and markings because it is a
restriction of
f
which is a well-dened PTI morphism.
64
B. PROOFS
(1) is pushout
:
Due to Lemma A.6 the diagrams (2)-(4) are pushouts in
Sets
which implies that
(1) is pushout in
PTINets
because the pushout in
PTINets
can be constructed
componentwise.
PB
bP//
gP
PL
fP
PCcP
//
(2)
PNI
TB
bT//
gT
TL
fT
TCcT
//
(3)
TNI
IB
bI//
gI
IL
fI
ICcI
//
(4)
INI
initiality of (1)
:
Given pushout (5) in
PTINets
with
d∈ M
.
Bb//
g
L
f
D
d
oo
h
Cc//
(1)
NI E
e
oo
(5)
The sets
TB
and
IB
are exactly the boundaries of
fT
and
fI
, respectively, in
Sets
.
So pushouts (3) and (4) are initial and since pushouts in
PTINets
can be con-
structed componentwise in
Sets
there are pushouts (6) and (7) in
Sets
leading to
unique suitable functions
b∗
T, c∗
T, b∗
I, c∗
I∈ MSets
such that (8) and (9) are pushouts
in
Sets
.
TB
bT
**
gT
b∗
T
//
(8)
TD
hT
dT
//TL
fT
TC
cT
44
c∗
T//TE
eT//
(6)
NI T
IB
bI
**
gI
b∗
I
//
(9)
ID
hI
dI
//IL
fI
IC
cI
44
c∗
I//IE
eI//
(7)
NI I
We dene a function
c∗
P:PC→PE
with
c∗
P(x) = y
with
eP(y) = cP(x)
well-denedness of
c∗
P
:
For the well-denedness of
c∗
P
we have to show that for every
x∈PC
there is
a unique
y∈PE
with
eP(y) = cP(x)
.
Let
x∈PC
. We use in the following the fact, that from pushout (5) in
PTINets
follows that (10) is a pushout in
Sets
.
PD
dP//
hP
PL
fP
PCeP
//
(10)
PNI
B. PROOFS
65
Case 1
:
x /∈fP(PL)
Since (10) is pushout in
Sets
the functions
fP
and
eP
are jointly surjec-
tive. So
x /∈fP(PL)
implies
x∈eP(PE)
and hence there exists
y∈PE
with
eP(y) = x
.
Case 2
:
x∈fP(bP(PB))
Then there exists
z∈PB
with
fP(bP(z)) = x
.
Case 2.1
:
z∈IPP
Then from the fact that (10) is pushout in
Sets
together with Fact
A.7 follows that
dP
and
fP
satisfy the gluing condition which means
that
z∈dP(PD)
, i.e. there exists
z0∈PD
with
dP(z0) = z
. Let
y=hP(z0)
. Then we have
eP(y) = eP(hP(z0)) = fP(dP(z0)) = fP(z) = x
which means that
y
is a suitable element.
Case 2.2
:
z∈DPT
This means that there is
t∈TG\fT(TL)
with
fP(z)∈ENVP(t)
. Since
(6) is pushout in
Sets
the functions
fT
and
eT
are jointly surjective
which by the fact that
t /∈fT(TL)
implies that
t∈eT(TE)
, i.e. there
exists
t0∈TE
with
eT(t0) = t
.
Then there is
y∈PE
with
y∈ENVP(t0)
and
eP(y) = fP(z) = x
because P/T morphisms preserve pre and post conditions.
Case 2.3
:
z∈DPI
Then there exists
i∈INI \fI(IL)
with
fP(z) = mNI (i)
. Since (7) is
pushout in
Sets
the functions
fI
and
eI
are jointly surjective which
due to the fact that
i /∈fI(IL)
implies that there is
i0∈IE
with
eI(i0) = i
. Hence we have
x=fP(z) = mNI (i) = mNI (eI(i0)) = eP(mE(i0))
which means that
y=mE(i0)
is a suitable place.
Case 2.4
:
z∈PIPT
This means that there is
t∈IPT
with
z∈ENVP(t)
. By Fact A.7
there is
t∈dT(TD)
because
TE
is a pushout complement of
dT
and
fT
. So there is
t0∈TD
with
t=dT(t0)
. Then we have
e⊕
P(preE(hT(t0))) = preG(eT(hT(t0)))
=preG(fT(dT(t0)))
=preG(fT(t))
=f⊕
P(preL(t))
and analogously
e⊕
P(postE(hT(t0))) = f⊕
P(postL(t))
66
B. PROOFS
which means that there is
y∈ENVP(hT(t0)) ⊆PE
with
eP(y) = fP(z) = x
Case 2.5
:
z∈PIPI
Then there exists
i∈IPI
with
z=mL(i)
which by Fact A.7 implies
that there is
i0∈ID
with
dI(i0) = i
because
IE
is a pushout comple-
ment of
dI
and
fI
.
Then we have
eP(mE(hI(i0))) = eP(hP(mD(i0))) = fP(dP(mD(i0)))
=fP(mL(dI(i0))) = fP(mL(i)) = fP(z) = x
and hence
y=mE(hI(i0))
is a suitable place.
So for every
x∈PC
there is a suitable
y∈PE
with
eP(y) = cP(x)
. Let us
assume that
y
is not unique, i.e. there is
y0∈PE
with
eP(y0) = cP(x)
. Since
d∈ M
and pushouts preserve
M
-morphisms we also have that
e∈ M
which
means that
eP
is injective implying that
y=y0
. Hence
cP
is well-dened.
morphism
c∗
:
We dene a PTI morphism
c∗= (c∗
P, c∗
T, c∗
I) : C→E
. In order to show that
c∗
is a well-dened PTI morphism we have to show that it preserves pre and
post domains and markings.
Let
t∈TC
and let
t0∈TE
with
eT(t0) = cT(t)
, i.e.
t0=c∗
T(t)
.
Then we have
c⊕
P(preC(t)) = preNI (cT(t)) = preNI (eT(t0)) = e⊕
P(preE(t0))
which means that for
preC(t) =
n
X
i=1
pi
and
preE(t0) =
m
X
i=1
p0
i
there is
n=m
because
cP
and
eP
are injective and therefore also
c⊕
P
and
e⊕
P
are injective.
So we have
n
X
i=1
cP(pi) = c⊕
P(preC(t)) = e⊕
P(preE(t0)) =
n
X
i=1
eP(p0
i)
which by the denition of
c∗
P
means that
c∗⊕
P(preC(t)) = c∗⊕
P(
n
X
i=1
pi) =
n
X
i=1
c∗
P(pi)
=
n
X
i=1
p0
i=preE(t0) = preE(c∗
T(t))
B. PROOFS
67
The proof that
c∗
preserves post domains works analogously.
Let
i∈IC
and let
i0∈IE
with
eI(i0) = cI(i)
, i.e.
i0=c∗
I(i)
.
Then we have
cP(mC(i)) = mNI (cI(i)) = mNI (eI(i0)) = eP(mE(i0))
which by denition of
c∗
P
means that
c∗
P(mC(i)) = mE(i0) = mE(c∗
I(i))
Hence
c∗
is a well-dened PTI morphism.
The fact that
e◦c∗=c
follows directly from the denition of
c∗
P
and the
initiality of (3) and (4).
uniqueness of
c∗
, existence of
b∗
and pushout
:
By Lemma A.1 the morphism
c∗
is the unique morphism with
c=e◦c∗
and
there is a unique morphism
b∗:B→D
with
b=d◦b∗
such that (11) is a
pushout in
PTINets
.
B
b
))
g
b∗//
(11)
D
h
d
//L
f
C
c
55
c∗//Ee//
(5)
NI
B.2. Proof of 2.11
In this section we prove the equivalence of the fact that PTI morphisms
l
and
f
satisfy
the gluing condition, and the fact that
l
and
f
satisfy the categorical gluing condition.
Proof.
If.
Let
l
and
f
satisfy the categorical gluing condition, i.e. for initial pushout (1) there
is a morphism
b∗:B→K
with
l◦b∗=b
.
B
g
b
//
b∗
))
L
f
K
l
oo
Cc//NI
(1)
Let
x∈IP ∪DP
. We have to show that
x∈GP =lP(PK)∪lT(TK)∪lI(IK)
.
Case 1
:
x∈IPP∪IPI∪DP
Then there is
x∈PB
and
y∈PK
with
b∗(x) = y
and
l(y) = l(b∗(x)) = b(x) = x
which means that
x∈lP(PK)⊆GP
.
68
B. PROOFS
Case 2
:
x∈IPT
Then there is
x∈TB
and
y∈TK
with
b∗(x) = y
and
l(y) = l(b∗(x)) = b(x) = x
which means that
x∈lT(TK)⊆GP
.
Case 3
:
x∈IPI
Analogously to Case 2.
Hence
l
and
f
satisfy the gluing condition in
PTINets
.
Only If.
Let
l
and
f
satisfy the gluing condition in
PTINets
, i.e. there is
IP ∪DP ⊆GP.
This means that there is
IPP⊆lP(PK)
,
IPT⊆lT(TK)
and
IPI⊆lI(IK)
implying
that
lP, fP
and
lT, fT
and
lI, fI
satisfy the gluing condition in
Sets
.
From Fact A.7 follows that there are functions
b∗
P:PB→PK
with
lP◦b∗
P=bP
,
b∗
T:TB→TK
with
lT◦b∗
T=bT
, and
lI:IB→IK
with
lI◦b∗
I=bI
.
We dene a PTI morphism
b∗= (b∗
P, b∗
T, b∗
I)
. For the well-denedness we have to
show that
b∗
preserves pre and post domains as well as markings.
Let
t∈TB
. Then there is
l⊕
P(b∗⊕
P(preB(t))) = (lP◦b∗
P)⊕(preB(t))
=b⊕
P(preB(t))
=preL(bT(t))
=preL(lT(b∗
T(t)))
=l⊕
P(preK(b∗
T(t)))
and since _
⊕
preserves monomorphisms in
Sets
because monomorphisms in
Sets
are exactly the coequalizers in
Sets
and _
⊕
is a free functor, the morphism
l⊕
P
is
a monomorphism implying that
b∗⊕
P(preB(t)) = preK(b∗
T(t))
The proof that
b∗
preserves post domains works analogously.
Let
i∈IB
. Then there is
lP(b∗
P(mB(i))) = bP(mB(i))
=mL(bI(i))
=mL(lI(b∗
I(i)))
=lP(mK(b∗
I(i)))
which by the fact that
lP
is a monomorphism implies that
b∗
P(mB(i)) = mK(b∗
I(i))
Hence
b∗
is a well-dened PTI morphism which means that
l
and
f
satisfy the
categorical gluing condition.
B. PROOFS
69
B.3. Proof of Fact 3.10
In this section we prove the well-denedness of the AHLI net
C
dened in Fact 3.10 and
that the construction leads to an initial pushout in the category
AHLINets
.
Proof.
well-denedness of
C
:
preC, postC:TC→(TOPC(XC)⊗PC)⊕
:
Let
t∈TC
and let
(term, p)≤preC(t)
. Then there is
term ∈TOPANI (XANI )typeANI (p)=TOPC(XC)typeC(p).
It remains to show that
p∈PC
.
Due to the fact that
t∈(TANI \fT(TL)) ∪fT(bT(TB))
we can distinguish the
following cases:
Case 1
:
t /∈fT(TL)
Case 1.1
:
∃p0∈PL:fP(p0) = p
Then due to the fact that there is
(term, p)≤preANI (t)
there is
p0∈DPT⊆PB
which means that
p=fP(bP(p0)) ∈PC
.
Case 1.2
:
@p0∈PL:fP(p0) = p
This means that
p∈PANI \fP(PL)⊆PC
.
Case 2
:
t∈fT(bT(TB))
Then there exists
t0∈TB
with
fT(bT(t0)) = t
and since AHL morphisms
preserve pre conditions there is
preANI (t) = preANI (fT(bT(t0)))
= (f]
Σ⊗fP)⊕(preL(bT(t0)))
= (f]
Σ⊗fP)⊕((b]
Σ⊗bP)⊕(preB(t0)))
By Lemma A.2 there is
preANI (t) = ((fΣ◦bΣ)]⊗(fP◦bP))⊕(preB(t0))
which for
(term, p)≤preANI (t)
means that
(term, p)≤((fΣ◦bΣ)]⊗(fP◦bP))⊕(preB(t0))
and hence
p∈fP(bP(PB)) ⊆PC
.
The proof for
postC
works analogously.
mC:IC→AC⊗PC
:
Let
i∈IC
and let
(a, p) = mC(i)
. Then there is
a∈AANI ,typeANI (p)=AC,typeC(p).
70
B. PROOFS
It remains to show that
p∈PC
. Due to the fact that
i∈(IANI \fI(IL)) ∪fI(bI(IB))
we can distinguish the following cases:
Case 1
:
i /∈fI(IL)
Case 1.1
:
∃p0∈PL:fP(p0) = p
This means that
p0∈DP
and thus
p0∈PB
and
p=fP(bP(p0)) ∈PC
.
Case 1.2
:
@p0∈PL:fP(p) = p
This means that
p /∈fP(PL)
, i.e.
p∈ANI \fP(PL)
and hence
p∈PC
.
Case 2
:
i∈fI(bI(IB))
Then there exists
j∈IB
with
fI(bI(j)) = i
and we have
mC(i) = mANI (i)
=mANI (fI(bI(j)))
= (fA⊗fP)(mL(bI(j)))
= (fA⊗fP)((bA⊗bP)(mB(j)))
which means that
p∈fP(bP(PB))
and hence
p∈PC
.
well-denedness of
c
:
We obtain an inclusion morphism
c:C→ANI
from the fact that
preC
,
postC
,
condC
,
typeC
and
mC
are restrictions of the respective functions in
ANI
. Fur-
thermore there is
cΣ=idΣC
and
cA=idAC
which are well-dened signature and
algebra morphisms, respectively.
well-denedness of
g
:
For
J={P, T, I}
we obtain well-dened functions
gJ:JB→JC
because for
j∈JB
there is
gJ(j) = fJ(j) = fJ(bJ(j)) ∈JC
The morphism
g
preserves pre and post domains, conditions, types and markings
because it is a restriction of
f
which is a well-dened AHLI morphism.
Furthermore there is
gΣ=fΣ
and
gA=fA
.
(1) is pushout
:
Due to Lemma A.6 the diagrams (2)-(4) are pushouts in
Sets
.
PB
bP//
gP
PL
fP
PCcP
//
(2)
PANI
TB
bT//
gT
TL
fT
TCcT
//
(3)
TANI
IB
bI//
gI
IL
fI
ICcI
//
(4)
IANI
B. PROOFS
71
Moreover diagram (5) is pushout in
Sig
and (6) is pushout in
Algs
.
ΣL
idΣL//
fΣ
ΣL
fΣ
ΣANI idΣANI
//
(5)
ΣANI
(ΣL, AL)id(ΣL,AL)//
(fΣ,fA)
(ΣL, AL)
(fΣ,fA)
(ΣANI , AANI )id(ΣANI ,AANI )
//
(6)
(ΣANI , AANI )
The pushouts (2)-(6) imply that (1) is pushout in
AHLINets
because the pushout
in
AHLINets
can be constructed componentwise.
initiality of (1)
:
Given pushout (7) in
AHLINets
with
d∈ M
.
Bb//
g
L
f
D
d
oo
h
Cc//
(1)
ANI E
e
oo
(7)
The sets
TB
and
IB
are exactly the boundaries of
fT
and
fI
, respectively, in
Sets
.
So pushouts (3) and (4) are initial and since pushouts in
AHLINets
can be con-
structed componentwise in
Sets
there are pushouts (8) and (9) in
Sets
leading
to unique suitable functions
b∗
T, c∗
T, b∗
I, c∗
I∈ MSets
such that (10) and (11) are
pushouts in
Sets
.
TB
bT
**
gT
b∗
T
//
(10)
TD
hT
dT
//TL
fT
TC
cT
33
c∗
T//TE
eT//
(8)
ANI T
IB
bI
**
gI
b∗
I
//
(11)
ID
hI
dI
//IL
fI
IC
cI
33
c∗
I//IE
eI//
(9)
ANI I
function
c∗
P
:
We dene a function
c∗
P:PC→PE
with
c∗
P(x) = y
with
eP(y) = cP(x)
For the well-denedness of
c∗
P
we have to show that for every
x∈PC
there is
a unique
y∈PE
with
eP(y) = cP(x)
.
Let
x∈PC
. We need in the following that pushout (7) in
AHLINets
implies
pushout (12) in
Sets
.
PD
dP//
hP
PL
fP
PEeP
//
(12)
PANI
72
B. PROOFS
Case 1
:
x /∈fP(PL)
Since (12) is pushout in
Sets
the functions
fP
and
eP
are jointly surjec-
tive. So
x /∈fP(PL)
implies
x∈eP(PE)
and hence there exists
y∈PE
with
eP(y) = x
.
Case 2
:
x∈fP(bP(PB))
Then there exists
z∈PB
with
fP(bP(z)) = x
.
Case 2.1
:
z∈IPP
Then from the fact that (12) is pushout in
Sets
together with Fact
A.7 follows that
d
and
f
satisfy the gluing condition which means
that
z∈dP(PD)
, i.e. there exists
z0∈PD
with
dP(z0) = z
. Let
y=hP(z0)
. Then we have
eP(y) = eP(hP(z0)) = fP(dP(z0)) = fP(z) = x
which means that
y
is a suitable element.
Case 2.2
:
z∈DPT
This means that there is
t∈TANI \fT(TL)
with
fP(z)∈ENVP(t)
.
Since (8) is pushout in
Sets
the functions
fT
and
eT
are jointly sur-
jective which by the fact that
t /∈fT(TL)
implies that
t∈eT(TE)
, i.e.
there exists
t0∈TE
with
eT(t0) = t
.
Then there is
y∈PE
with
y∈ENVP(t0)
and
eP(y) = fP(z) = x
because AHLI morphisms preserve pre and post conditions.
Case 2.3
:
z∈DPI
Then there exists
i∈IANI \fI(IL)
with
fP(z) = πP(mANI (i))
. Since
(9) is pushout in
Sets
the functions
fI
and
eI
are jointly surjective
which due to the fact that
i /∈fI(IL)
implies that there is
i0∈IE
with
eI(i0) = i
. Hence we have
x=fP(z) = πP(mANI (i))
=πP(mANI (eI(i0)))
=πP((eA⊗eP)(mE(i0)))
=eP(mE(i0))
which means that
y=mE(i0)
is a suitable place.
Case 2.4
:
z∈PIPT
This means that there is
t∈IPT
with
z∈ENVP(t)
. By Fact A.7
there is
t∈dT(TD)
because
TE
is a pushout complement of
dT
and
fT
. So there is
t0∈TD
with
t=dT(t0)
. Then we have
(e]
Σ⊗eP)⊕(preE(hT(t0))) = preANI (eT(hT(t0)))
=preANI (fT(dT(t0)))
=preANI (fT(t))
= (f]
Σ⊗fP)⊕(preL(t))
B. PROOFS
73
and analogously
(e]
Σ⊗eP)⊕(postE(hT(t0))) = (f]
Σ⊗fP)⊕(postL(t))
which means that there is
y∈ENVP(hT(t0)) ⊆PE
with
eP(y) = fP(z) = x
Case 2.5
:
z∈PIPI
Then there exists
i∈IPI
with
z=πP(mL(i))
which by Fact A.7
implies that there is
i0∈ID
with
dI(i0) = i
because
IE
is a pushout
complement of
dI
and
fI
.
Then we have
(eA⊗eP)(mE(hI(i0))) = mANI (eI(hI(i0)))
=mANI (fI(dI(i0)))
= (fA⊗fP)(mL(i))
which means that there is
y=πP(mE(hI(i0))) ⊆PE
with
eP(y) = fP(z) = x
So for every
x∈PC
there is a suitable
y∈PE
with
eP(y) = cP(x)
. Let us
assume that
y
is not unique, i.e. there is
y0∈PE
with
eP(y0) = cP(x)
. Since
d∈ M
and pushouts preserve
M
-morphisms there is also
e∈ M
which means
that
eP
is injective implying that
y=y0
. Hence
cP
is well-dened.
signature morphism
c∗
Σ
:
Due to the fact that
e∈ M
the signature morphism
eΣ
is an isomorphism.
We dene
c∗
Σ=e−1
Σ
Since
ΣC= ΣANI
the morphism
c∗
Σ
is well-dened.
algebra morphism
c∗
A
:
Also the algebra morphism
eA
is an isomorphism because
e∈ M
. So we dene
c∗
A=e−1
A
leading to a well-dened algebra morphism because
AC=AANI
.
morphism
c∗
:
We dene an AHLI morphism
c∗= (c∗
Σ, c∗
P, c∗
T, c∗
A, c∗
I) : C→E
. In order
to show that
c∗
is a well-dened AHLI morphism we have to show that it
preserves pre and post conditions, conditions, types and markings.
74
B. PROOFS
types
:
Let
p∈PC
and let
p0∈PE
with
cP(p) = eP(p0)
, i.e.
c∗
P(p) = p0
.
Furthermore let
c∗
Σ= (c∗
S, c∗
OP )
and
eΣ= (eS, eOP )
. Then we have
c∗
S(typeC(p)) = e−1
S(typeC(p))
=e−1
S(typeANI (p))
=e−1
S(typeANI (cP(p)))
=e−1
S(typeANI (eP(p0)))
=e−1
S(eS(typeE(p0)))
=typeE(p0)
=typeE(c∗
P(p))
pre and post conditions
:
Let
t∈TC
.
Due to the denition of
c∗
P
there is
cP=eP◦c∗
P
. So we have
(e]
Σ⊗eP)⊕((c∗]
Σ⊗c∗
P)⊕(preC(t)))
= (e]
Σ⊗eP)⊕((c∗]
Σ⊗c∗
P)⊕(preC(t)))
Lemma
A.2
= ((eΣ◦c∗
Σ)]⊗(eP◦c∗
P))⊕(preC(t))
= ((eΣ◦e−1
Σ)]⊗cP)⊕(preC(t))
= ((idΣANI )]⊗cP)⊕(preC(t))
= (c]
Σ⊗cP)⊕(preC(t))
=preANI (cT(t))
=preANI (eT◦c∗
T(t))
= (e]
Σ⊗eP)⊕(preE(c∗
T(t)))
Since
e∈ M
is a monomorphism and _
⊗
_
,
_
]
and _
⊕
preserve monomor-
phisms, there is also
(e]
Σ⊗eP)⊕
a monomorphism. So the above equation
implies
(c∗]
Σ⊗c∗
P)⊕(preC(t)) = preE(c∗
T(t))
The proof that
c∗
preserves post conditions works analogously.
conditions
:
Let
t∈TC
and let
t0∈TE
with
eT(t0) = cT(t)
, i.e.
t0=c∗
T(t)
.
Due to the fact that
cΣ=idΣC
there is
condC(t) = Pfin(c]
Σ)(condC(t))
=condANI (cT(t))
=condANI (eT(t0))
=Pfin(e]
Σ)(condE(t0))
B. PROOFS
75
which by the denition of
c∗
Σ
implies that
Pfin(c∗]
Σ)(condC(t)) = Pfin(c∗]
Σ)(Pfin(e]
Σ)(condE(t0)))
Lemma
A.3
=Pfin((c∗
Σ◦eΣ)])(condE(t0))
=Pfin((e−1
Σ◦eΣ)])(condE(t0))
=Pfin(id]
ΣE)(condE(t0))
=Pfin(idTOPE(XE))(condE(t0))
=condE(t0)
=condE(c∗
T(t))
markings
:
Let
i∈IC
and
mC(i)=(a, p)
.
Then we have
(eA⊗eP)((c∗
A⊗c∗
P)(mC(i))) = (eA⊗eP)((c∗
A⊗c∗
P)(a, p))
= (eA⊗eP)(c∗
A,typeC(p)(a), c∗
P(p))
= (eA,typeE(c∗
P(p))(c∗
A,typeC(p)(a)), eP(c∗
P(p)))
= (eA,c∗
S(typeC(p))(c∗
A,typeC(p)(a)), eP(c∗
P(p)))
= (Vc∗
Σ(eA)typeC(p)(c∗
A,typeC(p)(a)), eP(c∗
P(p)))
= (Vc∗
Σ(eA)typeC(p)(e−1
A,typeC(p)(a), cP(p)))
= ((Vc∗
Σ(eA)◦e−1
A)typeC(p)(a), cP(p))
= (a, cP(p))
= (cA(a), cP(p))
= (cA⊗cP)(a, p)
= (cA⊗cP)(mC(i))
=mANI (cI(i))
=mANI (eI◦c∗
I(i))
= (eA⊗eP)(mE(c∗
I(i)))
and since
e∈ M
is a monomorphism and _
⊗
_ preserves monomorphisms,
there is also
(eA⊗eP)
a monomorphism. So the equation above implies
(c∗
A⊗c∗
P)(mC(i)) = mE(c∗
I(i))
Hence
c∗
is a well-dened AHLI morphism.
The fact that
e◦c∗=c
follows directly from the denitions of
c∗
P
,
c∗
Σ
and
c∗
A
and the initiality of (3) and (4).
uniqueness of
c∗
, existence of
b∗
and pushout
:
By Lemma A.1 the morphism
c∗
is the unique morphism with
c=e◦c∗
and
there is a unique morphism
b∗:B→D
with
b=d◦b∗
such that (13) is a
pushout in
AHLINets
.
76
B. PROOFS
B
b
))
g
b∗//
(13)
D
h
d
//L
f
C
c
44
c∗//Ee//
(7)
ANI
B.4. Proof of Fact 3.11
In this section we prove that the fact that AHLI morphisms
f
and
l
satisfy the gluing
condition in
AHLINets
is equivalent to the fact that
f
and
l
satisfy the categorical
gluing condition.
Proof.
If.
Let
l
and
f
satisfy the categorical gluing condition, i.e. for initial pushout (1) there
is a morphism
b∗:B→K
with
l◦b∗=b
.
B
g
b
//
b∗
**
L
f
K
l
oo
Cc//ANI
(1)
Let
x∈IP ∪DP
. We have to show that
x∈GP =lP(PK)∪lT(TK)∪lI(IK)
.
The proof works completely analogously to the proof in Fact 2.11. Hence
l
and
f
satisfy the gluing condition in
AHLINets
.
Only If.
Let
l
and
f
satisfy the gluing condition in
AHLINets
, i.e. there is
IP ∪DP ⊆GP.
This means that there is
IPP⊆lP(PK)
,
IPT⊆lT(TK)
and
IPI⊆lI(IK)
implying
that
lP, fP
and
lT, fT
and
lI, fI
satisfy the gluing condition in
Sets
.
From Fact A.7 follows that there are functions
b∗
P:PB→PK
with
lP◦b∗
P=bP
,
b∗
T:TB→TK
with
lT◦b∗
T=bT
, and
lI:IB→IK
with
lI◦b∗
I=bI
.
We dene an AHLI morphism
b∗= (b∗
P, b∗
T, b∗
Σ, b∗
A, b∗
I)
with
b∗
Σ=l−1
Σ
and
b∗
A=l−1
A
.
The signature morphism
l−1
Σ
and algebra morphism
l−1
A
exist because
l∈ M
and
hence
lΣ
and
lA
are isomorphisms.
For the well-denedness of
b∗
it remains to show that
b∗
preserves pre and post
conditions, conditions, types, and markings.
types
:
Let
p∈PB
and let
p0∈PK
with
bP(p) = lP(p0)
, i.e.
b∗
P(p) = p0
.
B. PROOFS
77
Then we have
b∗
S(typeC(p)) = b∗
S(typeANI (p))
=b∗
S(typeANI (cP(p)))
=b∗
S(typeANI (eP(p0)))
=b∗
S(eS(typeE(p0)))
=e−1
S(eS(typeE(p0)))
=typeE(p0)
=typeE(c∗
P(p))
pre and post conditions
:
Let
t∈TB
. Then there is
(l]
Σ⊗lP)⊕((b∗]
Σ⊗b∗
P)⊕(preB(t)))
Lemma
A.2
= ((lΣ◦b∗
Σ)]⊗(lP◦b∗
P))⊕(preB(t))
= ((lΣ◦b∗
Σ)]⊗(lP◦b∗
P))⊕(preB(t))
= ((lΣ◦l−1
Σ)]⊗(lP◦b∗
P))⊕(preB(t))
= (id]
ΣL⊗bP)⊕(preB(t))
= (b]
Σ⊗bP)⊕(preB(t))
= (preANI (bT(t)))
= (preANI (lT◦b∗
T(t)))
= (l]
Σ⊗lP)⊕(preK(b∗
T(t)))
Since
l∈ M
is a monomorphism and _
⊗
_
,
_
]
and _
⊕
preserve monomor-
phisms, there is also
(l]
Σ⊗lP)⊕
a monomorphism. So the above equation
implies
(b∗]
Σ⊗b∗
P)⊕(preB(t)) = preK(b∗
T(t))
The proof for the post conditions works analogously.
conditions
:
78
B. PROOFS
Let
t∈TB
and let
t0∈TK
with
bT(t) = lT(t0)
, i.e.
t0=b∗
T(t)
. Then we have
Pfin(b∗]
Σ)(condB(t)) = Pfin(b∗]
Σ)(condL(t))
=Pfin(b∗]
Σ)(condL(bT(t)))
=Pfin(b∗]
Σ)(condL(lT(t0)))
=Pfin(b∗]
Σ)(Pfin(l]
Σ)(condK(t0)))
Lemma
A.3
=Pfin((b∗
Σ◦lΣ)])(condK(t0))
=Pfin((l−1
Σ◦lΣ)])(condK(t0))
=Pfin(idΣK)])(condK(t0))
=condK(t0)
=condK(b∗
T(t))
markings
:
Let
i∈IB
and
mB(i) = (a, p)
.
Then we have
(lA⊗lP)((b∗
A⊗b∗
P)(mB(i))) = (lA⊗lP)((b∗
A⊗b∗
P)(a, p))
= (lA⊗lP)(b∗
A,typeB(p)(a), b∗
P(p))
= (lA,typeK(b∗
P(p))(b∗
A,typeB(p)(a)), lP(b∗
P(p)))
= (lA,b∗
S(typeB(p))(b∗
A,typeB(p)(a)), lP(b∗
P(p)))
= (Vb∗
Σ(lA)typeB(p)(b∗
A,typeB(p)(a)), lP(b∗
P(p)))
= (Vb∗
Σ(lA)typeB(p)(l−1
A,typeB(p)(a), bP(p)))
= ((Vb∗
Σ(lA)◦l−1
A)typeB(p)(a), bP(p))
= (a, bP(p))
= (bA(a), bP(p))
= (bA⊗bP)(a, p)
= (bA⊗bP)(mB(i))
=mANI (bI(i))
=mANI (lI◦b∗
I(i))
= (lA⊗lP)(mK(b∗
I(i)))
and since
l∈ M
is a monomorphism and _
⊗
_ preserves monomorphisms,
there is also
(lA⊗lP)
a monomorphism. So the equation above implies
(b∗
A⊗b∗
P)(mB(i)) = mK(b∗
I(i))
Hence
b∗
is a well-dened AHLI morphism. The required commutativity follows
from the commutativity of its components. So
l
and
f
satisfy the categorical gluing
condition.
