Sound Recoveries of Structural Workflows with Synchronization Piotr Chrza̧stowski-Wachtel, Pawel Gola̧b, and Bartosz Lewiński Institute of Informatics, Warsaw University, Banacha 2, PL 02-097 Warszawa, Poland pch@mimuw.edu.pl, pawel.golab@mimuw.edu.pl, bartosz.lewinski@mimuw.edu.pl Abstract. We consider communication places in workflow nets, where the connected transitions lie in parallel threads. When a workflow Petri net is constructed structurally, by means of refinements, such places can- not be modeled structurally. They are added after the net is constructed. Workflow 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 com- munication 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 workflow modeling — allow the manager to move to- kens arbitrarily, when some unexpected situation happens. They were extensively studied and proved to be a useful tool in the workflow man- agement [HA00]. They can be modeled as a kind of reset transitions with additional feature of depositing tokens taken from a specified region to particular places in this region, like it was proposed in [Ch06]. Mov- ing 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 sufficient and necessary condition of soundness for a marking in a struc- tured 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. 1 Introduction Workflow management is an area, where workflow designers can prove correct- ness and flexibility of their models. It has been studied in numerous papers, like [WS09], [BPS09]. One of the major problems is how to organize commu- nication 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. 74 P. Chrza̧stowski-Wachtel, P. Gola̧b, B. Lewiński Composing workflow nets in a structural way was proposed in [ChBHO03]. A number of basic node refinement rules has been introduced. These rules include sequential split, parallel split, choice and loop splits. They reflect typical pro- gramming constructs like sequence of actions, an invocation of parallel threads, instruction of choice and a loop statement. The control of the workflow 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 defined by [vdAtH00]. As it was already recognized in [ChBHO03], these constructs are not sufficient for typical needs of a workflow designer. In the cited paper a number of non- structural synchronization rules were proposed. By non-structural we mean here adding of new nodes and edges, which do not result as a refinement 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 sufficient condition for soundness. The condition was based on the idea of the refinement tree, reflecting the history of refinements. It has been proven that refinement trees are unique up to an isomorphism for a given structural WF- net. In other words, if a WF-net is constructed structurally, then all the histories creating this net differ only in unimportant details (like the order of refinements in disjoint areas), resulting in the same refinement tree. p1 t1 t2 p1 p9 p2 p3 p6 t8 t3 t4 t6 p8 t1 t5 t2 t9 p4 p5 p7 t7 t5 t9 p9 p2 t3 p4 p3 t4 p5 p6 t6 p7 t7 p8 t8 Fig. 1. Example WF -net and an corresponding refinement tree Sound Recoveries of Structural Workflows with Synchronization 75 In dynamical workflows it is often desired that the control is being changed during the lifetime of the workflow execution. Such situations are quite normal, especially when workflows describe processes that last for a long time (months or even years). Sometimes the manager decides to detour from the anticipated control flow and would like to “correct” the flow 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 workflow should be repeated due to unexpected failures, which were not foreseen during the design. In such cases we would like to support the workflow management by allowing the manager to perform only sound rearrangements of the flow. When no such restriction would be set, the manager, quite possibly without understanding side effects, could make undesirable changes. This can lead to unwanted behavior, making the net unsound. One of the main problems with such on-the-fly changes of the markings is to determine the impact area, which is the least part of the net, called region, which is affected by the rearrangement of tokens. The refinement tree gives us precise information — in order to define the impact area caused by any changes in the net, it suffices to find the latest common predecessor of the nodes, where the changes were made. The nodes which are not descendants of this node are not affected 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 (dif- ferent) 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 suf- ficient 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 refinement 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 refinement 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 find conditions, which would protect the manager from depositing tokens on such places, that the resulting marking would be unsound, hence not properly terminating. 2 Refinement Rules This section is a short reminder of WF -nets refinement rules introduced in [ChBHO03]. The idea behind is that having defined the refinement rules preserv- ing certain network properties, we are able to analyse WF -networks that were 76 P. Chrza̧stowski-Wachtel, P. Gola̧b, B. Lewiński p1 t1 t2 p1 p9 p2 p3 p6 t8 t3 t4 t6 p8 s t1 t5 t2 t9 p4 p5 p7 t7 t5 t9 p2 t3 p4 p3 t4 p5 p6 t6 p7 t7 p8 t8 p9 s Fig. 2. Example of net synchronization with corresponding refinement tree 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 refinement rules approach is construction trace called refinement tree that contains much information about the network structure. An example of such tree and corresponding network can be found on figure 1. The rest of this section covers basic rules presented in [ChBHO03]. All described rules are depicted on figure 3. The first two rules are called sequential splits. They are used to create linear sequence of places and transitions, like p2 → t3 → p4 on figure 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 firing sequences. Splits replace the chosen node with three other nodes: the first 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 first of them applies to places and the second one to transitions and both are replacing node with two copies of it. The first split called parallel split introduces two parallel threads that will be executed simultaneously. In sound transition firing sequences transitions from different parallel paths can be safely swapped (if partial order defined by other splits is preserved). Examples of such paths are p2 → t3 → p4 and p3 → t4 → p5 on figure 1. The second split, called choice split, defines two alternative paths that the process can follow. During a single process run, transitions of only one of the Sound Recoveries of Structural Workflows with Synchronization 77 Fig. 3. Basic WF -nets refinement rules. Starting from top: sequential place split, se- quential transition split, parallel split, choice split and loop split. paths can be enabled. Examples of such paths are t1 → . . . → t5 and t2 → . . . → t9 on figure 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 figure 1. 3 Definitions In this section we’ll present some definitions 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 defined as siblings that occur after v in p’s children order. The definition of left siblings of v is analogous. 78 P. Chrza̧stowski-Wachtel, P. Gola̧b, B. Lewiński Prenodes. We define 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 definition corresponds to the original refinement tree, without using additional edges provided by synchronisations. Existential marking function. Below we present notation and definition for ex- istential marking function which returns information if in a given set of nodes any places are marked. ( ? 0 if M (v) = 0 for each v ∈ V M (V ) = 1 otherwise Structured SWF -net (Synchronised WorkFlow network) is an extension of WF -net defined 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 , flow 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 Soundness Characterisation The main goal of this chapter is to find properties of marking M in SWF -net that guarantee soundness. Before introducing these properties we’ll define 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 define 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 definitions is that Before (v) ∩ After (v) = ∅ for each node v. Sound Recoveries of Structural Workflows with Synchronization 79 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 first 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 ∈ Before (v) and va ∈ After (v). Clearly, Before (vb ) ⊂ Before (v) and After (va ) ⊂ After (v). We also have v ∈ After (vb ) and v ∈ Before (va ). And so, finally, 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 M1s ) into M1e . Some transitions are incomparable in this order because of different 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 ∈ T that is not a part of any loop, the set After (t) con- tains all transitions that can fire after t occurs in a sequence transforming a sound marking M into M1e and that this firing is directly dependent on t. If the transition t is in a loop, the same condition holds, except for some other transi- tions 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 fire, need transition t to fire before them. It is important to stress out here, that we only consider transition sequences that contain t when writing about firing 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 firing, so there are possible situations, when t won’t 80 P. Chrza̧stowski-Wachtel, P. Gola̧b, B. Lewiński occur in such sequences but the considered transitions will still fire. Neverthe- less, if t occurs in such a sequence, it determines the path that the process went through and we know that t firing is necessary in order to make the next transi- tions firings possible. We have a similar situation in the case when t results from loop main transition fragmentation (as t7 and t8 on figure 1). With this observation, we can move to the main part of the proof. 1. The first 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 se- quence transforming M1s 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 M1s 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 transi- tions 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 find 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 ∈ After (ty ) or simply tx = ty . Because marking M is sound, it is possible for ty to fire. 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 fire, 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). Sound Recoveries of Structural Workflows with Synchronization 81 Lemma 1 Let N = hP, T, F, f, ei be an WF-net and Ns = P, T, F, f, e, {s}, C be the same net with added synchronisation place s. Given Ns marking M is sound if and only if: 1. M|N 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 different 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 figure 4. p1 t1 t2 p2 p3 p6 t8 t3 t4 t6 p8 s p4 p5 p7 t7 t5 t9 p9 Fig. 4. Example of synchronisation skipping marking Therefore, for the sake of precision, we can describe the first three states as: synchronisation place is active, process is during synchronisation and syn- chronisation 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 finished considered fragment with alternative). Nevertheless it is more convenient to use definitions presented in the previous paragraph. 82 P. Chrza̧stowski-Wachtel, P. Gola̧b, B. Lewiński To show that the above intuitions are right, we will now prove our lemma. 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, {s}, C net. What synchronisation point does, is prohibiting certain transition sequences that allow obtaining marking M|N from M1s in N , by enforcing firings of one tran- sition 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 M|N . This means that M|N is sound in N , so 1. holds. For the case when there exists such OR place that allows to skip synchroni- sation, let pin be the place before such fork, and pout first 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 fire, so again from the proposition, M (After (out(s))) = 0. If s is marked, than in(s) has already fired. We know that M |N 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 fire. If M (After (out(s))) > 0 then it means that transitions in(s) and out(s) have already fired, so s is empty and from the validity of M|N , 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 fire and we know from the proposition that it has to fire 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 refinement 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. Sound Recoveries of Structural Workflows with Synchronization 83 M|N is sound, so let hxi i be a sequence of events leading to M1e in N . It’s easy to see, that in case when one of b), c) or d) holds, the same sequence can be fired 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 hxi i 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 Soundness Checking The algorithm for checking the soundness of a marking will be a modification of the soundness checking algorithm (theorem) from presented in previous work [Ch06]. As a reminder, two functions w and W were defined as follows:    1 if v = root  w(parent (v))  if v is a child of a node which is not a parallel w(v) = split node w0 (parent(v))      c if v is a child of a node of the parallel split node, with c children  M  (v) w0 (v) for each place-leaf v P W (v) = y∈Ch(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 define 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 satisfied. 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 84 P. Chrza̧stowski-Wachtel, P. Gola̧b, B. Lewiński For every node v ∈ Prenode (in(s)) (nodes on the left of the path from in(s) to root)  1   if v = root ws (parent (v)) if v is a child of a node which is not a parallel  ws (v) = split node  ws (parent(v)) if v is a child of a node being a parallel split     c node, with c children For the remaining nodes ws (v) = w(v). The function W remains unchanged, except for the fact that now it depends on ws .  ? cs · (M (s) + M (After (out(s))))  if t = in(s) S(M )(t) = −cs · (M? (After (out(s)))) if t = out(s)  0 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 t1 1 t2 1 t1 1 t2 1 p2 3/4 p3 1/4 p6 t8 1 p2 3/4 p3 1/4 p6 t8 1 1 1 +1/4 t3 t4 -1/4 t6 1 p8 1 +1/4 t3 t4 -1/4 t6 1 p8 1 s s 1/4 1/4 p4 1/2 p5 1/2 p7 t7 1 p4 1/2 p5 1/2 p7 t7 1 1 1 t5 1 t9 1 t5 1 t9 1 p9 1 p9 1 Fig. 5. Example of SWF -net with marked weights defined by functions from the the- orem. The marking on the left is sound, while the marking on the right isn’t, which results in weight explosion in t1. Theorem 1 A marking M of the SWF-net N is sound if and only if for each s s node v in the refinement tree either WM (v) + S(v) = w(v) or WM (v) = 0 Sound Recoveries of Structural Workflows with Synchronization 85 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 Fig. 6. Derivation Tree with paths highlighted Lets reason case by case, we will prove that in each of these cases our algo- rithm 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 modified left sides (“Before”) of trees, so the verification 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) modifies it to the correct amount 86 P. Chrza̧stowski-Wachtel, P. Gola̧b, B. Lewiński 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)) modifies it to the correct amount. Similarly, since M (After (out(s))) > 0 and marking is sound, the verification 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 modifications 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 verification succeeds. Let us prove the opposite implication now. Let M be such a marking that for s s each node v in the refinement tree either WM (v) + S(v) = w(v) or WM (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 modified 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 s need S to have WM (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 s enabled nodes get passed to the path, they need S to have WM (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 first part of the lemma, that M|N is sound in N . The proof of this fact is identical to first 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. Sound Recoveries of Structural Workflows with Synchronization 87 6 Conclusion 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 man- ner with the preservation of soundness. We have discovered a condition that is sufficient and necessary for a marking to preserve soundness. The condition, based on the structure of the refinement 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 fly changes of markings during the execution of a workflow. 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 workflow run. Support by automatic verification, if such changes can cause an undesired behavior (like deadlock or creation of trash tokens) is an important improvement of the technology. References [vdAtH00] W.M.P.van der Aalst, A.H.M. ter Hofstede, Verification of Workflow Task Structures: A Petri-net-based Approach, Information Systems, 25(1): 43-69, March 2000. [ChBHO03] Piotr Chrza̧stowski-Wachtel, Boualem Benatallah, Rachid Hamadi, Mil- ton O’Dell, Adi Susanto, Top-down Petri Net Based Approach to Dynamic Workflow Modelling, Lecture Note in Computer Science. v2678. 336-353., 2003. [Ch06] P.Chrza̧stowski-Wachtel, Determining Sound Markings in Structured Nets, Fundamenta Informaticae, 72, 2006. [BPM05] M. Laugna, J. Marklund. Business Process Modeling, Simulation, and De- sign. Prentice Hall, Upper Saddle River, New Jersey, 2005. [HA00] C.Hagen, G.Alonso, Exception Handling in Workflow Management Systems, IEEE Trans. of Soft. Eng. vol. 26 No 10, Oct 2000. [BPS09] W.M.P. van der Aalst, J. Nakatumba, A. Rozinat, and N. Russell. Business Process Simulation: How to get it right? In J. vom Brocke and M. Rosemann, editors, International Handbook on Business Process Management, Springer-Verlag, Berlin, 2009. [WS09] A. Rozinat, M. Wynn, W.M.P. van der Aalst, A.H.M. ter Hofstede, and C. Fidge., Workflow Simulation for Operational Decision Support., Data and Knowl- edge Engineering, 68(9):834-850, 2009.