We consider communication places in work ow nets, where the connected transitions lie in parallel threads. When a work ow Petri net is constructed structurally, by means of re nements, such places cannot be modeled structurally. They are added after the net is constructed. Work ow nets constructed in a structural manner are sound, but addition of such communication places can result in losing the desired soundness property. However, there is a method to avoid such misplacement of communication places. We should limit the pairs of connected transitions to the ones that lie in truly parallel threads and to avoid cycles introduced by communication places. Recovery transitions | special kind of transitions used as a powerful tool in dynamic work ow modeling | allow the manager to move tokens arbitrarily, when some unexpected situation happens. They were extensively studied and proved to be a useful tool in the work ow management [HA00]. They can be modeled as a kind of reset transitions with additional feature of depositing tokens taken from a speci ed region to particular places in this region, like it was proposed in [Ch06]. Moving tokens arbitrarily by the manager requires a lot of attention, since soundness of the net can easily be destroyed. In this paper we present a su cient and necessary condition of soundness for a marking in a structured net with communication places. Verifying the condition turns out to be fast. The cost is linear with respect to the total number of places and transitions.
Work ow management is an area, where work ow designers can prove correctness and exibility of their models. It has been studied in numerous papers, like [WS09], [BPS09]. One of the major problems is how to organize communication between parallel tasks performed by communicating agents [BPM05]. Making communication pattern wrongly can easily lead to deadlocks, mutual waiting or leaving messages as trash, when they are deposited somewhere, and not consumed by anyone. The danger of bad design increases, when we talk about management that lasts in time and needs rearrangement due to some unexpected situations.
Composing work ow nets in a structural way was proposed in [ChBHO03]. A number of basic node re nement rules has been introduced. These rules include sequential split, parallel split, choice and loop splits. They re ect typical programming constructs like sequence of actions, an invocation of parallel threads, instruction of choice and a loop statement. The control of the work ow runs can be hence guarded by these constructs. Restricting the nets to the nets obtained from a single node by these structural constructs was proven in to guarantee soundness, as de ned by [vdAtH00].
As it was already recognized in [ChBHO03], these constructs are not su cient for typical needs of a work ow designer. In the cited paper a number of nonstructural synchronization rules were proposed. By non-structural we mean here adding of new nodes and edges, which do not result as a re nement of existing nodes. Among them the most important was the synchronization of two parallel actions. When in two parallel threads A and B we want an action b from B to wait until an action a from A has been executed, we can model it by introducing a new communication place s with arcs leading from a to s and from s to b. Such construct we call a synchronization or communication, depending on whether we emphasize the fact that b must wait for a or that a has something important to communicate to b. Introducing such synchronization places can result in a possible deadlock or other unsound constructs, like trash tokens generation. In order to avoid misintroduction of such places, a criterion was proposed, which is a su cient condition for soundness. The condition was based on the idea of the re nement tree, re ecting the history of re nements. It has been proven that re nement trees are unique up to an isomorphism for a given structural WFnet. In other words, if a WF-net is constructed structurally, then all the histories creating this net di er only in unimportant details (like the order of re nements in disjoint areas), resulting in the same re nement tree.
p2 p4 t3 t1 t5 p3 p5 p9 p1 t4 t9 p6 p7 t2 t6 p8 t8 t7 p1
p9 t1 t5 t2
t9 p2 t3 p4 p3 t4 p5 p6 t6 p7 t7 p8 t8 Fig. 1. Example WF -net and an corresponding re nement tree
In dynamical work ows it is often desired that the control is being changed during the lifetime of the work ow execution. Such situations are quite normal, especially when work ows describe processes that last for a long time (months or even years). Sometimes the manager decides to detour from the anticipated control ow and would like to \correct" the ow manually moving tokens around. Situations of this kind can happen in particular, when for instance under some time pressure we decide to skip several actions or when we decide that some part of the work ow should be repeated due to unexpected failures, which were not foreseen during the design. In such cases we would like to support the work ow management by allowing the manager to perform only sound rearrangements of the ow. When no such restriction would be set, the manager, quite possibly without understanding side e ects, could make undesirable changes. This can lead to unwanted behavior, making the net unsound.
One of the main problems with such on-the- y changes of the markings is to determine the impact area, which is the least part of the net, called region, which is a ected by the rearrangement of tokens. The re nement tree gives us precise information | in order to de ne the impact area caused by any changes in the net, it su ces to nd the latest common predecessor of the nodes, where the changes were made. The nodes which are not descendants of this node are not a ected by these changes.
The changes we consider are of two kinds. First of them is the addition of places or transitions in an unstructured manner. An example of such useful addition is the introduction of a place joining two transitions, which are in (different) parallel threads. If such a place connects transition t with transition r, then the intention is to suspend the execution of r until t is executed. Clearly the introduction of such a place can result in a deadlock. In [ChBHO03] a strong sufcient condition was presented guaranteeing net soundness after such insertion of a communication place. It turns out that if an inserted place connects such two transittion-type leaves t and r in the re nement tree that no choice-split or loop-split node is found on the path from t to r and if no cycle can be detected in the net after such insertion, then the resulting net is sound.
The second kind of change is of dynamical matter. We allow the manager to modify the marking by arbitrary moving tokens around some region. A region is understood as the net unfolded from a single place-type node in the re nement tree. Inside a region we consider the so-called recovery transitions, which remove tokens from the whole area and restore them in arbitrarily chosen places. Our goal is to nd conditions, which would protect the manager from depositing tokens on such places, that the resulting marking would be unsound, hence not properly terminating. 2
This section is a short reminder of WF -nets re nement rules introduced in [ChBHO03]. The idea behind is that having de ned the re nement rules preserving certain network properties, we are able to analyse WF -networks that were p2 p4 t3 s t1 t5 p3 p5 p9 p1 t4 t9 p6 p7 t2 t6 p8 t8 t7 p1
p9 t1 t5 t2
t9 p2 t3 p4 p3 t4 p5 p6 t6 p7 t7 p8
t8 s constructed by using those rules. To construct such network one starts with a single place, and then repeatedly applies context-free rules on network elements. One of biggest advantages of using re nement rules approach is construction trace called re nement tree that contains much information about the network structure. An example of such tree and corresponding network can be found on gure 1. The rest of this section covers basic rules presented in [ChBHO03]. All described rules are depicted on gure 3.
The rst two rules are called sequential splits. They are used to create linear sequence of places and transitions, like p2 ! t3 ! p4 on gure 1. It's an example of splitting a single place. There are two kinds of sequential splits depending on the node type they are applied to. We call them sequential place split and sequential transition split respectively. Splits of this type introduce partial order of transitions in sound transition ring sequences. Splits replace the chosen node with three other nodes: the rst and the last are of the same type and have either the same inputs or outputs as the original node, respectively. The third node is the one in the middle that connects two other nodes, so is of opposite type.
The next two rules are equivalent to logical AN D and OR gates respectively. The rst of them applies to places and the second one to transitions and both are replacing node with two copies of it.
The rst split called parallel split introduces two parallel threads that will be executed simultaneously. In sound transition ring sequences transitions from di erent parallel paths can be safely swapped (if partial order de ned by other splits is preserved). Examples of such paths are p2 ! t3 ! p4 and p3 ! t4 ! p5 on gure 1.
The second split, called choice split, de nes two alternative paths that the process can follow. During a single process run, transitions of only one of the paths can be enabled. Examples of such paths are t1 ! : : : ! t5 and t2 ! : : : ! t9 on gure 1.
The last split type introduces loops and therefore is called a loop split. A loop example with nodes later splitted by sequential split rules can be found on gure 1. 3
In this section we'll present some de nitions and notation conventions that will be used in the rest of the article.
Siblings. For the node v that is a child of sequential split type node p, let right siblings be de ned as siblings that occur after v in p's children order. The de nition of left siblings of v is analogous. Prenodes. We de ne Prenodes (v) set as follows. Let pi be the i-th node on the path from root to v. Then for each pi of sequential split type, Prenodes (v) includes pi, left siblings of pi+1 and their subtrees.
This de nition corresponds to the original re nement tree, without using additional edges provided by synchronisations.
Existential marking function. Below we present notation and de nition for existential marking function which returns information if in a given set of nodes any places are marked.
M?(V ) = (0 if M (v) = 0 for each v 2 V
1 otherwise
Structured SWF -net (Synchronised WorkFlow network) is an extension of WF -net de ned as a 7-tuple hP; T; F; s; e; S; Ci, where 1. hP; T; F; s; ei is a standard structured WF -net with the set of places P , transitions T , ow function F the source place s, and the exit place e. 2. S | the set of synchronisation places (semaphores) 3. C | the set of edges joining semaphores and synchronised transitions. It is easy to see that C \ F = ;
When two transitions t1 and t2 are synchronised via place s, we denote t1 as in(s) and t2 as out(s). 4
The main goal of this chapter is to nd properties of marking M in SWF -net that guarantee soundness. Before introducing these properties we'll de ne two auxiliary sets Before and After, that will help us in those properties formulation and we'll explore some important properties of them. 4.1
Before and After sets Intuitively, Before (v) and After (v) sets include places and transitions, that are over or under vertex v in WF -net graph respectively. In the case of SWF -nets we consider only such nodes that are not synchronisation places during Before and After sets construction.
We de ne Before (v) set as follows. A leaf l is in Before (v) if and only if there exists a predecessor q of l being a left-sibling of some node lying on the path from the root to v inclusively. Similarly for Af ter(v) we consider right siblings instead. We ignore the synchronisation places.
An important feature of Before and After sets is that Before (v) and After (v) sets are not containing v itself, so immediate conclusion from Before and After sets de nitions is that Before (v) \ After (v) = ; for each node v.
It is worth to explore, how Before and After sets are constructed in the case of loops. We can distinguish two cases depending on whether loop contains the node for which these sets are constructed or not.
Let us consider loops from the rst case. Let l be the loop that was created by splitting place pl and transition tl. In this case Before and After sets will either contain leaves only from pl subtree or only from tl subtree.
In the second case the Before and After sets can either contain all the leaves of the given loop or none of its nodes.
In the forthcoming text it is important to have clarity about Before and After sets containment rules. Let v, vb, va be the vertices such that vb 2 Before (v) and va 2 After (v). Clearly, Before (vb) Before (v) and After (va) After (v). We also have v 2 After (vb) and v 2 Before (va). And so, nally, After (v) After (vb) and Before (v) Before (va).
The Before and After sets have some interesting properties in the context of sound marking, that we will formulate in the following proposition. We say that a node (place or transition) x in a Petri net is reachable from a given marking M if it is not dead in the case x is a transition or it can be marked by some marking reachable from M , in the case x is a place.
Proposition 1 Let M be a sound marking of WF-net with synchronisations. For each place or transition x we have: 1. M (x) 1 implies M (After (x)) = 0 2. M (Before (x)) > 0 implies M (After (x)) = 0 3. M (Before (x)) > 0 implies M (x) = 0 and x is reachable.
Proof. Let hP; T; F; s; e; S; Ci be a structured SWF -net and M a sound marking on this network.
We begin the proof with some observations. When constructing the Before and After sets, we take into account only subtrees related with nodes that are of sequential split type. The sequential split type nodes determine the partial order of transitions in possible transition sequences transforming any sound marking M (in particular Ms1) into Me1. Some transitions are incomparable in this order because of di erent types of nodes, for example AN D nodes that introduce concurrency in nets. This partial order results in important properties of Before and After sets.
For a transition t 2 T that is not a part of any loop, the set After (t) contains all transitions that can re after t occurs in a sequence transforming a sound marking M into Me1 and that this ring is directly dependent on t. If the transition t is in a loop, the same condition holds, except for some other transitions from this loop | not all of them are included in After (t) set. But still, all transitions from the loop that belong to the After (t) set in order to re, need transition t to re before them.
It is important to stress out here, that we only consider transition sequences that contain t when writing about ring dependences. In the case of transitions that come after AN D nodes, there are at least two independent paths which can lead to those transitions ring, so there are possible situations, when t won't occur in such sequences but the considered transitions will still re. Nevertheless, if t occurs in such a sequence, it determines the path that the process went through and we know that t ring is necessary in order to make the next transitions rings possible. We have a similar situation in the case when t results from loop main transition fragmentation (as t7 and t8 on gure 1).
With this observation, we can move to the main part of the proof. 1. The rst step is a direct result of our observation. If x = e then this point is obvious. If x 6= e then M (x) 1 means that x is a place and x is an input for some transitions Tx T .
Firstly, let's consider nets that contain no loops. Each transition in any sequence transforming Ms1 into M can occur only once. Since x isn't empty, we know that none of the Tx transitions will occur in possible transition sequences transforming Ms1 into M. Taking into account our observation this also means that none of the transitions from After sets of Tx transitions will occur in such sequences. It means that none of outputs of Tx transitions or outputs of transitions from their After sets is marked. We also know, that all the transitions from Tx, all their outputs and their After sets are in After (x). Moreover it is easy to nd that these are the only items in After (x). So we have M (After (x)) = 0.
The case of loops is very similar. The only problem is that x can be a loop element. It is possible in this case, that not all of Tx transitions will be in After (x) set | some of them can be transitions starting new loop iteration. However, it is easy to recognize that this makes no problem, and reasoning for transitions from Tx that are in After (x) is still valid.
2. This property is a simple consequence of 1. We know that for all places from Before (x) that marking M is greater than zero and their After sets markings is zero too. We also know that After (x) set is a subset of those After sets, so M (After (n)) = 0.
3. First part of this property is also a consequence of point 1. We know, that for all places from Before (x) for which the marking M is greater than zero, their After sets markings equal zero. We also know that x is an element of those places After sets, so M (x) = 0.
The fact that x is reachable is a result of our observation. Let ty be such a transition that is in After set of some place from Before (x) that the marking M is greater than zero, and for which this place in an input. We know that x is in ty's After set, so there exists a transition tx for which x is an output and either tx 2 After (ty) or simply tx = ty. Because marking M is sound, it is possible for ty to re. In the case when tx 6= ty, we know from the observation and from the fact that the marking M is sound [ChBHO03], that it is also possible for tx to re, so x is reachable. 4.2
Properties of sound SWF -net markings In this section we'll give a characterisation of SWF -net sound markings in the form of a short lemma. Before formulating the lemma, it is worth noticing, that as in the case of standard WF -nets, if M is a sound marking of WF -net with synchronisations, then M is 1-bounded (there can't be two tokens at a one place). Lemma 1 Let N = hP; T; F; f; ei be an WF-net and Ns = P; T; F; f; e; fsg; C be the same net with added synchronisation place s. Given Ns marking M is sound if and only if: 1. MjN is sound in N 2. Exactly one of following holds: (a) M (Before (in(s))) > 0 (b) s is marked (c) M (After (out(s))) > 0 (d) Synchronisation was skipped, so M (Before (in(s)) [ After (in(s))) = 0 and M (Before (out(s)) [ After (out(s))) = 0
Basically, the lemma describes intuitions about how synchronisation place should work. It says, that we have four di erent states, that our process can be in. First three cases are straightforward: it can be either before synchronisation, during synchronisation or after synchronisation. The last one is the case, when the synchronisation occurs in one of the branches that resulted from an choice split, and an active branch is not the synchronised one. An example of such situation is depicted below on gure 4.
p2 p4 t3 s t1 t5 p3 p5 p9 p1 t4 t9 p6 p7 t2 t6 p8 t8 t7
Therefore, for the sake of precision, we can describe the rst three states as: synchronisation place is active, process is during synchronisation and synchronisation is inactive, but either synchronisation has occurred, or the process branch without synchronisation is at the evaluation point, when marked places are in After (out(s)) set. The last one describes situation when process nished considered fragment with alternative). Nevertheless it is more convenient to use de nitions presented in the previous paragraph.
To show that the above intuitions are right, we will now prove our lemma. net.
Proof. It is important to remember that synchronization of items in loops is not allowed, so in every valid transition sequence in(s) and out(s) can occur only once.
Firstly let us assume that a marking M is sound in Ns = P; T; F; f; e; fsg; C What synchronisation point does, is prohibiting certain transition sequences that allow obtaining marking MjN from Ms1 in N , by enforcing rings of one transition group before another. It is important that synchronisation is not adding any new possible transition sequences. This means, that any transition sequence that leads to the marking M in Ns is also valid in N , leading to the marking MjN . This means that MjN is sound in N , so 1. holds.
For the case when there exists such OR place that allows to skip synchronisation, let pin be the place before such fork, and pout rst place after it. From the rules of synchronization we know that in this case pin is in Before (in(s)) and pout is in After (out(s)).
It is easy to see, that each of the conditions a), b) and c) exclude d) and vice versa. Now we'll show that a), b) and c) exclude each other. If M (Before (in(s))) > 0, then we know from the proven proposition, that there is no transition sequence that leads to a marking M containing in(s), so s will be empty for each valid subsequence of those transitions, which means that there was no possibility for out(s) to re, so again from the proposition, M (After (out(s))) = 0.
If s is marked, than in(s) has already red. We know that M jN is valid so, Before (in(s)) marking must be empty. Again from the proposition we have M (After (out(s))) = 0, because there was no possibility for out(s) to re.
If M (After (out(s))) > 0 then it means that transitions in(s) and out(s) have already red, so s is empty and from the validity of MjN , either M (Before (in(s))) is empty or the process was run following a path where no synchronisation occurs. In the second case we have M (pout [ After (pout)) > 0, we have that M (s) = 0 and M (Before (in(s))) = 0, because M (pin [ Before (pin)) = 0 according to the proposition.
If none of the conditions a), b) or c) holds, we have M (Before (in(s))) = 0, M (s) = 0 and M (After (out(s))) = 0. There are two possibilities. Firstly, we may consider situation when M (After (in(s))) > 0 and M (Before (out(s))) > 0, but in this case s can't be empty, because it would make impossible for out(s) to re and we know from the proposition that it has to re in order to clean up tokens from Before (out(s)).
The only valid option is M (After (in(s))) = 0 and M (Before (out(s))) = 0, which means that all tokens are in After (pin) \ Before (pout) on process path disjoint with the synchronisation. There are no other options because of the synchronisation rules, which allow to synchronize only these transitions, which are not separated by choice or loop split nodes in the re nement tree. So we know now that a), b), c) and d) exclude each other and in each case one of them must hold, so soundness of Ns means that 1. and 2. hold.
Now lets assume that 1. and 2. from the lemma hold.
MjN is sound, so let hxii be a sequence of events leading to Me1 in N . It's easy to see, that in case when one of b), c) or d) holds, the same sequence can be red in Ns. In the case when s is not empty, this sequence will clean s. A bit harder is the case when a) holds, but one can easily see, that it is possible to rearrange hxii so that in(s) will occur before out(s) and still all transitions from Before (in(s)) will be before in(s) and all transitions from After (out(s)) will be after out(s). Rules of synchronisation guarantee that such operations will lead to valid transition sequence, which will also be valid in Ns and will lead to the same result as the original sequence.
This proves that if 1. and 2. from the lemma hold for a given marking M that the marking is sound.
We have proved implications in both directions, so the lemma is valid. 5
The algorithm for checking the soundness of a marking will be a modi cation of the soundness checking algorithm (theorem) from presented in previous work [Ch06].
As a reminder, two functions w and W were de ned as follows: >81 if v = root > w(v) = <>>w(parent (v)) if v is a child of a node which is not a parallel split node >>>>: w0(parcent(v)) iwf ivthiscacchhilidldreonf a node of the parallel split node, >8M (v) w0(v) for each place-leaf v W (v) = <Py2Ch(v) W (y) for all internal nodes x >:0
for each transition-leaf t
The theorem stated that a marking is sound if and only if for each tree node x either W s(w)(x) = 0 or W s(w)(x) = w(s). We will now de ne new functions ws, W s and S such that W s and S will have the same signature as W and ws will have the same signature as w. Note that the values in W and S are determined only by leaves | for the internal nodes we take sum of the values of their children. For both in(s) and out(s), we will add additional weight to the path from the node to the root, and propagate this change downwards for the pre-nodes (nodes occurring to the left of it). Let cs be a constant such that for every node x the condition w(x) > cs is satis ed.
We will apply the following transformation two times to W presented in [Ch06] for both in(s), out(s), with c equal to cs, cs respectively.
For every node v on the path from t to root we add the weight c w0(v) = w(v) + c
For every node v 2 Prenode (in(s)) (nodes on the left of the path from in(s) to root) ws(v) = 8>1 if v = root > >><ws(parent (v)) if v is a child of a node which is not a parallel split node >>>:> ws(parcent(v)) infovdei,swaithchcildchoilfdraennode being a parallel split For the remaining nodes ws(v) = w(v). The function W remains unchanged, except for the fact that now it depends on ws.
S(M )(t) = 8 ><cs (M (s) + M?(After (out(s))))
cs (M?(After (out(s)))) >:0 if t = in(s) if t = out(s) for every other case
We will use this transformation two times to nodes in(s), out(s) with c being inverses of each other. Notice that this pair of transformations together changes nodes only inside the smallest subtree containing them.
p1 1 p1 1
Theorem 1 A marking M of the SWF-net N is sound if and only if for each node v in the re nement tree either W Ms (v) + S(v) = w(v) or W Ms (v) = 0 Proof. We will prove it by using the sound characterisation lemma.
Let M be a sound marking. By the above lemma, exactly one of following holds: 1. M (Before (in(s))) > 0 2. s is marked. 3. M (After (out(s))) > 0 4. Synchronisation was skipped, so M (After (in(s)) [ Before (in(s))) = 0 and M (Bef ore(out(s) = 0) [ After (out(s))) p1
p9 t1 t5 t2 t9 p2 t3 p4 p3 t4 p5 p6 t6 p7 t7 p8 t8 s
Lets reason case by case, we will prove that in each of these cases our algorithm will correctly verify the marking:
1. If M (Before (in(s))) > 0: Both in(s) and out(s) are inactive (which means S(in(s)) = S(out(s)) = 0). The marking M is sound, so M (After (out(s))) = 0 and M (After (in(s))) = 0. This means that all the marked nodes are in modi ed left sides (\Before") of trees, so the veri cation behaves just as in the W without synchronisation, because all the weights were just decreased by some amount.
2. If synchronization place s is marked: in(s) is active and out(s) is inactive. Since M(After (in(s)) [ Before (in(s))) > 0 and M (Before (in(s))) = 0, we have M (After (in(s))) > 0 and because the marking is sound, it meets S(in(s)) in some node in the path to root, and then S(in) modi es it to the correct amount 3. If M (After (out(s))) > 0: both in(s) and out(s) are active. Of course in this situation M(After (in(s)) [ Before (in(s))) > 0 and M (Before (in(s))) = 0, so we have M (After (in(s)))) > 0 The marking is sound, so it meets the S(in(s) in some node in the path to root, and then S(in(s)) modi es it to the correct amount. Similarly, since M (After (out(s))) > 0 and marking is sound, the veri cation succeeds until it meets at the path from in to root and here it is corrected by S from in(s)
4. If synchronisation was skipped, so M (After (in(s)) [ Before (in(s))) = 0 and M (Bef ore(out(s) = 0) [ After (out(s))): The modi cations to weights we made apply only to nodes in the path from in(s) to out(s) and they are all empty in this case.
This proves that in every case, our veri cation succeeds.
Let us prove the opposite implication now. Let M be such a marking that for each node v in the re nement tree either W Ms (v) + S(v) = w(v) or W Ms (v) = 0. We will show that the cases from the lemma are exclusive:
1: excludes (2: or 3:) Let's assume M (Before (in(s))) > 0. Then if 2: or 3: then in(s) is active, but since M (Before (in(s))) > 0, there is an active node that is on the left hand side from the path from in(s) to root, but it was already modi ed by c, so when S will meets, there will be c added two times. 2: and 3: Easy case, W (in(s)) = ws(in(s)) M (s) + M?(After (out(s))) = 2ws(in(s)) > ws(in(s))
It is easy to see that 4: is disjoint from the other cases too. We need only to distinguish 4: from 2:: If M (s) > 0 then W (in(s)) > 0, and since 4: holds, W (out(s)) = 0, so in the place where paths from in(s) to root and out(s) to root meet there will be an unbalance.
Hence the cases from the lemma are disjoint. We need to prove now that at least one of them holds. Let's assume none of them holds. Then in(s) and out(s) are not active. Assume that M (Before (out(s))) isn't empty. Because of 1:, M (Before (in(s))) = 0, so there are nodes enabled to the right from the path from out(s) to the root node, that are below least common ancestor of in(s) and out(s). When the weight of those active nodes gets passed to the path, they need S to have W Ms (v) + S(v) = w(v), but in(s) is inactive, so we came to a contradiction.
Similarly, assume M (After (in(s))) > 0. Because of 1:, M (After (out(s))) = 0, so there are enabled nodes to the left from path from out(s) to the root node, that are below least common ancestor of in(s) and out(s). When the weight of those enabled nodes get passed to the path, they need S to have W Ms (v)+S(v) = w(v), but in(s) is disabled, so we came to a contradiction.
These two arguments imply that 4:, M (After (in(s)) [ Before (in(s))) = 0 and M (Bef ore(out(s) = 0) [ After (out(s))), so at least one of the cases from the lemma holds.
Now we need to prove the rst part of the lemma, that MjN is sound in N . The proof of this fact is identical to rst part of this proof. We show that if one of 1:, 2: or 3: occurs, the rest of checking behaves identical to checking done in w. We have proven that the important construction of creating a channel between two transitions (like links in BPEL4WS) can be done in a semi-structured manner with the preservation of soundness. We have discovered a condition that is su cient and necessary for a marking to preserve soundness. The condition, based on the structure of the re nement tree is fast to verify; in fact it is linear with respect to the number of nodes of the net (so even better than the size of the net: the edges, with possible quadratic number of them, do not count). This condition allows us to determine soundness of an arbitrary marking and allow on-the y changes of markings during the execution of a work ow. Such changes are considered a powerful tool for a manager to change a marking in an arbitrary manner in case of an unexpected detour from the normal work ow run. Support by automatic veri cation, if such changes can cause an undesired behavior (like deadlock or creation of trash tokens) is an important improvement of the technology.