Interorganizational work°ows represent a new technique that o®ers companies a solution for managing business processes that involve more than one organization. In this paper, an interorganizational work°ow will be modelled using a special class of nested Petri nets, interorganizational work°ow nets (IWF-nets). This approach will allow the speci¯cation of the local work°ows in the organizations involved and of the communication structure between them, permitting a clear distinction between these components. The paper de¯nes a notion of behavioural correctness (soundness) and proves this property is decidable for IWFnets.
A work°ow is the automation of a business process that takes place inside one organization. Work°ow management deals with controlling, monitoring, optimizing and supporting work°ows.
Due to the rise of virtual organizations, electronic commerce and international companies, many existent business processes involve more than one organization. These work°ows , distributed over a number of di®erent organizations, are referred to as interorganizational work°ows.
A formal method which has been successfully used for work°ow modelling
is Petri nets. Petri nets are a graphical and mathematical tool for modelling
concurrent/distributed systems, which permit the explicit representation of the
states and transitions of a system. Petri nets are a suitable modelling technique
for work°ows (see [
Petri nets have also been proposed for modelling interorganizational
work°ows: in [
A common problem in these approaches is the mixture between the di®erent components of the interorganizational work°ow, which makes the model di±cult to understand and analyze. Also, the interoperability between the constituent work°ows either is not represented explicitly in the model, or it lacks clarity.
In order to tackle these problems, this paper presents a new approach on the
modelling of interorganizational work°ows, based on nested Petri nets. Nested
Petri nets ([
This approach o®ers a clear distinction between all the local work°ows and the communication structure, which is represented separately from the local work°ows. Thus, IWF-nets ensure a modular view over the components of an interorganizational work°ow. The proposed model provides a high degree of °exibility: any local work°ow can be modi¯ed without interfering with the other local work°ows and the communication structure can be changed without a®ecting the local work°ows. Also, our solution, based on nested Petri nets, preserves privacy and autonomy of the local work°ows: the work°ow inter-visibility is reduced, since the local work°ows make public only the labels (identi¯ers) of those tasks involved in cooperation. The paper introduces a notion of behavioural correctness for IWF-nets, soundness, and proves this property is decidable.
The rest of the paper is organized as follows: Section 2 introduces the basic terminology and notations related to Petri nets and work°ows, Section 3 presents an informal de¯nition of IWF-nets and a small introductory example of an IWFnet, Section 4 introduces the formal de¯nition of IWF-nets, Section 5 de¯nes and studies the soundness property for IWF-nets and Section 6 presents the concluding remarks.
This section introduces the terminology and notations related to Petri nets and
work°ows. For details, the reader is referred to [
The classical Petri net is a directed bipartite graph with two node types called places and transitions. The nodes are connected via directed arcs. Places are represented by circles and transitions by rectangles.
A Petri net is a triple P N = (P; T; F ), where P is a ¯nite set of places, T is a ¯nite set of transitions (P \ T = ;), F µ (P £ T ) [ (T £ P ) is a set of arcs (°ow relation).
For x 2 P [ T , the preset of x is ²x = fyj(y; x) 2 F g and the postset of x is x² = fyj(x; y) 2 F g. At any time a place contains zero or more tokens, drawn as black dots. The state (or the marking), is the distribution of tokens over places: M : P ! N (N denotes the set of natural numbers). We will represent a state as follows: if P = fp1; p2; p3g, then 10p1 + 20p2 is the state with one token in place p1, two tokens in p2 and no tokens in p3. Transitions change the state of the net according to the following ¯ring rule: a transition t is said to be enabled (in a marking M ) i® each place p in the preset of t contains at least one token in the marking M : M (p) ¸ 1; 8p 2 ²t. If an enabled transition t ¯res, it changes the marking M into M 0: M 0(p) = M (p) ¡ 1; 8p 2 ²t and M 0(p) = M (p) + 1; 8p 2 t². We write M [tiM 0.
We have the following notation: M1[¾iMn: the ¯ring sequence ¾ = t1t2 : : : tn 2 T ¤ leads from state M1 to Mn (i.e. there exist M2; : : : ; Mn¡1 such that M1[t1iM2[t2i : : : [tniMn). If ¾ = ¸, then M [¾iM . A state Mn is called reachable from M1 (M1[¤iMn) i® there is a ¯ring sequence ¾ such that M1[¾iMn. We denote by [M i the set of markings reachable from M . If N = (P; T; F ) is a Petri net and M0 is the initial marking of N , the set of reachable markings of N is denoted by [M0i.
Let N be a Petri net and M0 its initial marking. A transition t is not dead in (N; M0) if 9M 2 [M0i such that M [ti.
There are several extensions of Petri nets, which are obtained from the
classical model by adding expressions on arcs, tokens with a complex structure,
modi¯ed ¯ring rules, time concepts, etc. Nested Petri nets are an extension of
the Petri net model, in which tokens can be Petri nets themselves (see [
A work°ow can be seen as a collection of tasks organized in order to
accomplish some goal. The order of tasks is speci¯ed through di®erent constructors,
which permit the control of the °ow of execution, e.g. sequence, choice,
parallelism, and synchronization (see [
One of the most convenient ways of specifying work°ows is through the use of Petri nets: tasks can be modelled by transitions, the causal dependencies between tasks can be expressed using arcs and places. A place can model a pre or post-condition for a task. The state of the process can be explicitly modelled using the state of the Petri net.
In [
A Petri net PN=(P,T,F) is a WF-net i®: (1) PN has a source place i and a sink place o such that ²i = ; and o² = ; and (2) if we add a new transition t¤ to PN such that ²t¤ = fog and t¤² = fig, then the resulted Petri net is strongly connected. 3
In this section we will present an informal de¯nition of interorganizational work°ow nets and then we will apply their key features to a simple example of an interorganizational work°ow.
The interorganizational work°ows we are interested in are based on a special type of interoperability between processes : the global work°ow consists of loosely coupled work°ow processes which operate independently, but need to communicate and synchronize their activity at certain points in order to accomplish correctly the global work°ow process. There are two ways of interaction between processes: asynchronous communication (corresponding to the exchange of messages) and synchronous communication. Thus, the interorganizational work°ow consists of private work°ows and a communication structure.
In order to model interorganizational work°ows, we use an approach based on nested nets: interorganizational work°ow nets (IWF-nets) are nested Petri nets, extended with two special sets used for describing the communication structure between the local work°ows, SC and AC. AC represents the asynchronous communication relation: if (t; t0) 2 AC, then, the transition t must execute before the transition t0. SC represents the set of synchronous communication elements: if x 2 SC, then, all the transitions from x have to execute at the same time. Also, the IWF-net has two special sets of labels used for synchronizing the transitions involved in the elements of AC and SC: the labels in LabAC are used for the transitions which appear in the elements of AC and the labels from LabSC are used for the transitions which appear in the elements of SC. In an IWFnet, the system net SN comprises three places (I, p, O) and a transition (end). Tokens in SN can be atomic tokens (without inner structure) or net-tokens (object-nets). The arcs of SN are labelled with expressions: the arc (p; end) is labelled with the expression (x1; : : : ; xn; xn+1) (where x1; : : : ; xn; xn+1 are variables), while the rest of the arcs are labelled with the constant 1 (which is not represented explicitly on arcs). In an IWF-net, there are n + 1 object-nets: n object-nets (extended WF-nets) representing the local work°ows involved in the interorganizational work°ow and one object-net, C, which describes a part of the communication structure (the asynchronous communication). The structure of C results from AC: if ac = (t; t0) 2 AC, then, in C there is a place pac, a transition tc (corresponding to t), a transition t0c (corresponding to t0), one arc from tc to pac and one arc from pac to t0c. In an IWF-net there is a partial function, ¤, which labels transitions from the object-nets and the transition end from SN . If x 2 SC is a set of transitions which must ¯re synchronously, then all the transitions from x have the same label l 2 LabSC . For every transition t involved in an asynchronous communication element, there is a transition tc in the object-net C with the same label as t: ¤(t) = ¤(tc) = l; l 2 LabAC .
In our example, there are two local work°ow processes: the ¯rst process contains the tasks t1; t2; t3 and t4, while the second process contains the tasks t5; t6; t7 and t8. The two work°ow processes are modelled by two extended work°ow nets, W F10 and W F20 (see Fig. 1). These nets are work°ow nets, extended with transitions which empty the sink places of the work°ow nets (transition t01 in W F10 and t02 in W F20). The initial marking of W F10 is i1 and the initial marking of W F20 is i2.
In the interorganizational work°ow, the two work°ow processes interact as follows: task t1 in W F10 must ¯re before the tasks t5 and t6 in W F20, task t6 in W F20 must ¯re before task t3 in W F 0. We de¯ne, thus, a partial order on 1 tasks, describing the asynchronous communication between the two work°ow processes: AC = f(t1; t5); (t1; t6); (t6; t3)g. Also, task t4 in W F10 and task t8 in W F20 must ¯re synchronously (there is a synchronous communication between the two local work°ows, through these transitions). We will de¯ne the set of synchronous communication elements: SC = fft4; t8gg. The IWF-net used for modelling this interorganizational work°ow consists of the system net SN and of three object nets, W F10; W F20 and C. In the initial marking of the net (Fig. WF1’ p1 t2 p3
i1 1), there is an atomic token in place I and all the object-nets reside in place p. The initial marking of C is 0 (there are no tokens in the places of C). The arc (p; end) is assigned the expression (x1; x2; x3), while the rest of the arcs are assigned the constant expression 1.
The object-net C results from the asynchronous communication relation. The set of places is PC = fpac1 ; pac2 ; pac3 g, where ac1 = (t1; t5), ac2 = (t1; t6), ac3 = (t6; t3). The transitions in TC correspond to the transitions involved in asynchronous communication: TC = ft1c; t3c; t5c; t6cg. The arcs of C are obtained using the sets PC , TC and AC: for instance, since ac1 = (t1; t5) 2 AC; pac1 2 PC ; t1c; t5c 2 TC , then we will add the arcs (t1c; pac1 ) and (pac1 ; t5c).
Some of the transitions of the IWF-net are labelled. The sets of labels are: LabAC = fl1; l2; l3; l4g, LabSC = fl5g and a set fe; eg. The transitions involved in the asynchronous communication elements will be assigned asynchronous communication labels: in W F10, ¤(t1) = l1; ¤(t3) = l3 and in W F20, ¤(t5) = l2 and ¤(t6) = l4. The transitions from the synchronous communication element will be assigned the same synchronous communication label: ¤(t4) = ¤(t8) = l5. We also have ¤(t01) = e in W F10, ¤(t02) = e in W F20 and ¤(end) = e in SN . The labels for the transitions in C are assigned as follows: since (t1; t5) 2 AC, then ¤(t1c) = ¤(t1) = l1 and ¤(t5c) = ¤(t5) = l2. (t1; t6) 2 AC, then ¤(t6c) = ¤(t6) = l4. (t6; t3) 2 AC, then ¤(t3c) = ¤(t3) = l3.
The ¯ring rules in an IWF-net are the same as those from nested Petri nets.
The only di®erence is that we allow the horizontal synchronization of transitions
belonging to several object-nets (not just from two object-nets, as de¯ned in
[
In the example in Fig. 1, transition t1 is enabled in (W F10; i1) and the transitions t5 and t6 are enabled in (W F20; i2). But transition t5 should ¯re at the same time with transition t5c in the object-net C (because ¤(t5) = ¤(t5c)) and transition t6 should ¯re at the same time with transition t6c in the objectnet C (because ¤(t6) = ¤(t6c)). The transitions t5c and t6c are not enabled in (C; 0). So, transitions t5 and t6 cannot ¯re yet. This behaviour is consistent with the restrictions imposed by the asynchronous communication relation: (t1; t5); (t1; t6) 2 AC means that t1 should ¯re before t5 and t6. Since transition t1 is enabled in (W F10; i1), transition t1c is enabled in (C; 0), then the horizontal synchronization step (; t1; t1c) is enabled in marking M0. In the resulting marking, M1, place I contains an atomic token, place O contains no tokens, and place p contains three object-nets with their corresponding new markings: W F10 (with the marking m11 = 10p1 + 10p2, i.e. p1 and p2 have one token), W F20 (in its initial marking, i2) and C (with the marking mc1 = 10pac1 + 10pac2 ). We write: M1 = (1; ((W F 0; m11); (W F20; i2); (C; mc1)); 0). In (W F 0; m11) the unlabelled transi1 1 tion t2 is enabled. The ¯ring of this local transition is an object-autonomous step and the resulted marking is M2 = (1; ((W F10; m12); (W F20; i2); (C; mc1)); 0), where m12 = 10p2 + 10p3. One can notice that only the marking of the objectnet W F10 has changed. Transition t3 in W F10 can only ¯re synchronously with transition t3c in C, but transition t3c is not enabled in (C; mc1). The horizontal synchronization steps (; t5; t5c) and (; t6; t6c) are enabled in M2. If (; t6; t6c) ¯res, it produces the marking M3 = (1; ((W F 0; m12); (W F20; m21); (C; mc2)); 0), 1 where m21 = 10p6 and mc2 = 10pac1 + 10pac3 . If we assign to x1 the object-net (W F10; m14), to x2 the object-net (W F20; m22) and to x3 the object-net (C; mc3), then transition end is enabled in M5: place I contains an atomic token, place p contains three object-nets. Since t01 is enabled in (W F10; m14) and t02 is enabled in (W F20; m22), then the vertical synchronization step (end; t01; t02) is enabled in M5. The ¯ring of this step removes the atomic token from I, the object-nets from p and adds an atomic token to place O.
This section introduces the de¯nition of interorganizational work°ow nets, a model based on nested Petri nets, for loosely coupled interorganizational work°ows.
We will assume that there are n local work°ows belonging to n business partners. Each business partner has total control over his own work°ow process and the local work°ows interact at certain points, according to a communication structure. There are two types of communication: asynchronous communication (corresponding to the exchange of messages between work°ows) and synchronous communication (which forces the local work°ows to execute speci¯c tasks at the same time) .
We de¯ne, ¯rst, extended work°ow nets, an extension of the WF-nets de¯ned in Sect. 2.
De¯nition 1. Let W F = (P; T; F ) be a WF-net. The extended WF-net is W F 0 = (P; T 0; F 0), where T 0 = T [ ft0g and F 0 = F [ f(o; t0)g
W F is called the underlying net of W F 0. One can notice that the set of reachable markings of W F 0 includes the set of reachable markings of W F . The ¯nal marking of an extended work°ow net is the empty marking (the marking in which all the places are empty), denoted by 0. This marking is reachable only from the ¯nal marking of W F , o, by ¯ring the transition t0.
Extended WF-nets will be used for modelling the local work°ows from the interorganizational work°ow.
Interorganizational work°ow nets (IWF-nets) are de¯ned as a special class of nested Petri nets. IWF-nets are nested nets with a particular structure, extended with two sets (AC and SC), used for describing the communication between the local work°ows, and a special labelling system.
IW F = (V ar; Lab; (W F10; i1); : : : ; (W Fn0 ; in); AC; SC; (C; 0); SN; ¤) such that: 1. V ar = fx1; x2; : : : ; xn; xn+1g is a set of variables. 2. Lab = LabAC [ LabSC [ fe; eg is a set of labels.
tial markings i1; i2; : : : ; in. 4. AC is the asynchronous communication relation: AC µ T ± £ T ±, where T ± = [k2f1;:::;ngTk, Tk is the set of transitions from W Fk0 . If (t; t0) 2 AC; t 2 Ti; t0 2 Tj , then i 6= j. 5. SC is the set of synchronous communication elements: SC µ P (T ±) and: { 8x; y 2 SC : x \ y = ;.
{ if t 2 Ti; t0 2 Tj ; t; t0 2 x; x 2 SC, then i 6= j. 6. C = (PC ; TC ; FC ) is the communication object: { PC = fpacjac 2 ACg.
{ TC = ftcj9(t0; t) 2 AC _ (t; t0) 2 ACg. { FC = f(p; t) 2 PC £ T ±jp = (t0; t) 2 ACg [ f(t; p) 2 T ± £ PC jp = (t; t0) 2
ACg 7. SN = (N; W; M0) is the system net of IWF, such that: { N = (PN ; TN ; FN ) is a Petri net: ² PN = fI; p; Og, where O is a place such that O² = ; and I is a place such that ²I = ;. ² TN = fendg.
² FN = f(I; end); (p; end); (end; O)g. { W is the arc labelling function: W (I; end) = 1, W (p; end) = (x1; x2; : : : ; xn+1),
W (end; O) = 1. { M0 is the initial marking of the net: M0(I) = 1,
M0(p) = ((W F10; i1); : : : ; (W Fn0 ; in); (C; 0)) and M0(O) = 0.
{ 8x 2 SC; 8t; t0 2 x; ¤(t) = ¤(t0) = l; l 2 LabSC . { if t 2 T ± such that (t; t0) 2 AC or (t0; t) 2 AC, then there exists tc 2
TC : ¤(tc) = ¤(t) = l; l 2 LabAC . { ¤(t0i) = e; 8i 2 f1; : : : ng and ¤(end) = e.
{ 8t; t0 2 Ti(i 2 f1; : : : ; ng) : ¤(t) 6= ¤(t0).
In an IWF-net there are n object-nets (extended WF-nets) representing the local work°ows corresponding to the n business partners involved in the interorganizational work°ow.
V ar is the set of variables in the net. Variables xi, i 2 f1; : : : ; ng will take as value an object WF-net in a certain marking. Variable xn+1 will take as value the object-net C in a certain marking.
Lab is a set of labels: the labels in LabAC are used for asynchronous communication elements and the labels from LabSC are used for synchronous communication elements. LabAC and LabSC are not necessary disjoint. The label e is used for labelling the transition t0i from W Fi0, 8i 2 f1; : : : ; ng. The label e is used for the transition end from SN .
AC de¯nes a partial order on the transitions of the extended work°ow nets, representing the asynchronous communication: if (t; t0) 2 AC, t must execute before t0 (i.e. t0 waits for a message which is sent after the ¯ring of t). Also, t and t0 should not belong to the same set of transitions Ti (i 2 f1; : : : ng): if t and t0 belong to the same local work°ow, there exist other mechanisms for synchronizing these transitions and it is not necessary to specify an asynchronous communication relation between them.
SC represents the set of synchronous communication elements: if x 2 SC, then, all the transitions from x have to execute at the same time. x should not contain two transitions from the same set of transitions Ti: the local transitions from the same work°ow should not be synchronized using SC. All the sets in SC should be disjoint.
C is an object-net which describes the asynchronous communication between work°ows. C can be constructed automatically using the elements of AC: for every asynchronous communication element ac 2 AC, there is a corresponding place pac in PC . For every transition t 2 T ± involved in an asynchronous communication element, there is a transition tc 2 TC . Also, if ac = (t; t0) 2 AC, tc 2 TC is the transition which corresponds to t, t0c 2 TC is the transition which corresponds to t0, pac is the place which corresponds to ac, then there exist two arcs (tc; pac); (pac; t0c) 2 FC . The initial marking of C is the empty marking, denoted by 0.
W is a function that assigns to each arc in SN an expression. In IWF-nets, an expression can be either the pair (x1; : : : ; xn; xn+1) or the constant 1.
¤ is a partial function which assigns labels from Lab to certain transitions. All the transitions from a synchronous communication element x 2 SC have the same label l 2 LabSC . If t is a transition from an extended WF-net which appears in an asynchronous communication element ac 2 AC, then ¤(t) 2 LabAC . Since t belongs to an asynchronous communication element, there is a corresponding transition, tc, in the object-net C. t and tc have the same label: ¤(t) = ¤(tc) = l. In any extended WF-net, there are no transitions with the same label.
We denote by Anet the net tokens of the IWF-net: Anet = f(EN; m) / m is a marking of EN , EN 2 fW F10; : : : ; W Fn0 ; Cgg.
A marking of an IWF-net is a function such that: M (I) 2 N, M (O) 2 N and M (p) 2 Anne+t1. We write M as a vector M = (M (I); M (p); M (O)). De¯nition 3. A binding (of transition end) is a function b : V ar ! Anet. If expr is an expression, expr(b) denotes the evaluation of expr in binding b. expr(b) is obtained from expr by replacing every variable z 2 V ar from expr with b(z). If expr is a constant expression (an expression without variables), then expr(b) = expr.
in a marking M w.r.t. a binding b if and only if: 8q 2 ²end : W (q; end)(b) = M (q), where W (q; end)(b) is the arc expression of the arc (q; end) evaluated in binding b.
Transition end is enabled in a marking M w.r.t. the binding b if M (I) = 1 and the expression from the arc (p; end) evaluates to the same tuple of tokens from place p: W (p; end)(b) = M (p).
There are several types of steps, de¯ning the behaviour of nested Petri nets
(see [
tion t0i (¤(t0i) = e) is enabled in the object-net b(xi) = (W Fi0; mi); 8i 2 f1; : : : ; ng, then the simultaneous ¯ring of end and t01; : : : ; t0n is a vertical synchronization step.
produces the marking M 0 = (0; 0; 1).
This step removes the object-nets from p and the atomic token from I. In the resulting marking, M 0, there is only one atomic token in place O.
from p. Let ®i be one of the object-nets (i 2 f1; : : : ; ng) ®i = (W Fi0; m). Let t be a transition in ®i such that t is enabled in marking m, ¤(t) is unde¯ned and m[tim0 (i.e. the ¯ring of t, by the ¯ring rule from the classical Petri nets, produces a new marking m0 in ®i).
replacing, in the tuple (®1; ®2; : : : ; ®n+1) from M (p), the net token ®i with the net token ®i0, where ®i0 = (W Fi0; m0). We write: M [; tiM 0.
An object-autonomous step is the ¯ring of a local unlabelled transition in one of the local work°ows. None of the object-nets are moved from the place p.
Assume t1; : : : ts 2 T ± is the set of all the transitions with the same label l 6= e, ¤(t1) = ¤(t2) = : : : = ¤(ts) = l, such that: every transition tj (j 2 f1; : : : ; sg) is enabled in a net-token ®kj = (ENj ; mj ) (fk1; : : : ksg µ f1; : : : ; n + 1g, ENj 2 fW F10; : : : ; W Fn0 ; Cg ) and mj [tj im0j (by means of classical Petri nets). The synchronous ¯ring of t1; : : : ; ts is called a horizontal synchronization step.
from place p with the tuple (®10; ®20; : : : ; ®n0+1), where ®k0j = (ENj ; m0j ); 8j 2 f1; : : : ; sg and ®i0 = ®i; 8i 2 f1; : : : ; n + 1gnfk1; : : : ksg. We write: M [; t1; : : : ; tsiM 0.
If in a marking M of an IWF-net, all the transitions t1; : : : ; ts, with the same label l 6= e, are enabled in the object-nets ®k1 = (EN1; m1); : : : ; ®ks = (ENs; ms) from M (p), then the simultaneous ¯ring of these transitions is a horizontal synchronization step.
The de¯nitions of the vertical synchronization step and of the object-autonomous
step are the de¯nitions from [
In this section we will introduce a notion of soundness for IWF-nets.
A notion of soundness was de¯ned for WF-nets, expressing the minimal
conditions a correct work°ow should satisfy ([
sequence leading from m to the ¯nal marking o (termination condition): (8m)((i[¤im) =) (m[¤io)).
in place o: (8m)((i[¤im) ^ m ¸ o) =) (m = o)). 3. There are no dead transitions in WF: (8t 2 T )(9m; m0)(i[¤im[tim0).
It was proven (see [
In an interorganizational work°ow, although the local work°ows are sound, we can have synchronization errors and it is possible that communication elements introduce interlocking. In the interorganizational work°ow in Fig. 1, the two local work°ows are sound. But if we consider the execution sequence M0[Y1iM1[Y2iM2, where Y1 = (; t1; t1c), Y2 = (; t5; t5c), then, transition t3 will never ¯re in W F10, so the local work°ow W F10 does not terminate (transition t4 will never be enabled).
We will de¯ne a notion of soundness for interorganizational work°ows. We will consider the ¯nal state for an IWF-net, a marking Mf , in which there is only one atomic token in place O: Mf = (0; 0; 1). An IWF-net is sound if: (1) every extended WF-net W Fi0 (i 2 f1; : : : ; ng) is sound and (2) for any reachable marking of the IWF-net, M 2 [M0i, there is a ¯ring sequence that leads to Mf .
We can de¯ne formally the notion of soundness for an IWF-net as follows:
IW F = (V ar; Lab; (W F10; i1); : : : ; (W Fn0 ; in); AC;
1. (W Fj0; ij ) is a sound extended work°ow net, 8j 2 f1; : : : ; ng.
¯ring sequence leading from M to the ¯nal marking Mf : (8M )((M0[¤iM ) =) (M [¤iMf )).
First, we consider the interorganizational work°ow is sound if the extended WFnets describing the local work°ows are sound. The ¯nal marking of the IWF-net is reached if and only if the vertical synchronization step ¯res. This implies that all the transitions t0i are enabled in W Fi0 (i 2 f1; : : : ; ng), which happens if and only if the ¯nal markings in the extended WF-nets have been reached. Thus, the second condition from the soundness de¯nition basically states that the interorganizational work°ow is sound if the termination condition still holds for every WF-net, when the ¯ring of tasks is restricted by the communication structure.
The notion of soundness for IWF-nets is weaker than the notion of soundness
de¯ned in [
The notion of soundness for IWF-nets does not impose a condition similar to condition (2) from Def. 8, because such a condition always holds for sound IWF-nets:
reachable from M0 with at least one token in place O: (8M )((M0[¤iM ) ^ M ¸ Mf ) =) (M = Mf )) Proof. Assume M 2 [M0i and M ¸ Mf . If M ¸ Mf , then M (O) ¸ 1. But tokens can be added to place O only when transition end ¯res in IW F . This transition can only ¯re once and it empties place I and place p. No other steps can ¯re after this. So, the only reachable marking with M (O) ¸ 1 is Mf .
In order to decide whether the soundness property de¯ned is decidable, we
introduce a partial order on the markings of the IWF - net (see [
The marking M covers M 0 (w.r.t. the partial ordering ¹) if M 0 ¹ M . De¯nition 13. Given a set of markings Q = fq1; q2; : : : ; qng and an initial marking M , the inevitability problem is to decide whether all computations starting from M eventually visit a marking not covering (w.r.t. the partial ordering ¹) one of the markings from Q.
It was proven in [
Theorem 1. Let IW F be an IWF-net and M 2 [M0i. There is a ¯ring sequence M [¤iMf if and only if there is a ¯ring sequence M [¤iM 0 and M 0 does not cover (w.r.t. ¹) the marking (1; 0; 0).
(=)) Assume M [¤iMf in IW F . Since Mf does not cover the marking (1; 0; 0), we can consider M 0 = Mf . ((=) We assume there exists a ¯ring sequence from marking M to a marking M 0 which does not cover the marking (1; 0; 0). If M 0 does not cover (1; 0; 0), then M 0(I) = 0 (there are no tokens in place I). Marking M 0 is reachable from M0 (because M0[¤iM [¤iM 0). M 0(I) = 0 if and only if the vertical synchronization step Y = (end[b]; t01; : : : ; t0n) ¯res in IW F . The ¯ring of this step always leads to the marking Mf (so, M 0 = Mf ). This implies there is a ¯ring sequence such that M [¤iMf .
Proof: Let IW F be an IWF-net. Using the de¯nition of soundness and Theorem 1, IW F is sound if and only if: (1) W Fi0 are sound, 8i 2 f1; : : : ; ng and (2) for any reachable marking in IW F , M 2 [M0i, there exists a ¯ring sequence M [¤iM 0 such that M 0 does not cover (w.r.t. ¹) the marking (1; 0; 0). The soundness of the extended WF-nets is decidable (because the soundness for WF-net is decidable) and condition (2) is equivalent to the inevitability problem, if we consider the marking M and the set of markings Q = f(1; 0; 0)g. 6
In this paper we introduced a new approach on the modelling of interorganizational work°ows, based on nested Petri nets: the local work°ows and the communication structure are modelled as object-nets. The local work°ows have an independent behaviour and they can interact, according to the given communication structure, using the synchronization mechanisms o®ered by nested Petri nets. This approach has several advantages: one can have a modular view on the interorganizational work°ow, because the local work°ows and the communication structure are distinct elements in IWF-nets; steps in IWF- nets can easily express the synchronous and the asynchronous communication; IWF-nets represent a °exible model for interorganizational work°ows, because any component can be modi¯ed easily, with minimal changes to the other components. This is an important requirement for interorganizational work°ows, since the communication structure between the local work°ows can change in time. Also, our contribution preserves the privacy of the local work°ows: the local work°ows only share two sets of labels used for the synchronous and the asynchronous communication. A notion of soundness was introduced for IWF-nets: an IWF-net is sound if and only if all the extended work°ow nets which describe the local work°ows are sound and for any reachable marking of the IWF-net, there is a ¯ring sequence that leads to the ¯nal marking. We proved this property is decidable for IWF-nets. Future work aims at de¯ning IWF-nets which will model interorganizational work°ows in which every local work°ow processes batches of cases, instead of one case in isolation.