The problem of workflow instance migration occurs during dynamic evolutionary changes in processes. The paper presents a catalogbased algorithm called the Yo-Yo Algorithm for consistent instance migration in Petri net workflow models. It uses a technique of folding and unfolding of nets. The algorithm is formulated in terms of Colored Derivation Trees, a novel representation of the runtime states of workflow nets. The approach solves the problem for certain types of changes on acyclic block-structured workflow nets built in terms of primitive patterns moving much of the computation to schema level on account of the use of two critical ideas, a catalog and the folding order. The approach is illustrated with the help of examples and comments on its correctness.
Organizational goals are realized by executing business processes that involve people, resources, schedules and technology. In order to cope up with changing environments, changing requirements or new internal challenges, business processes need to be changed. Traditional workflow management systems (WFMS) are well-suited for rigid processes. However, the volatile nature of business processes requires intricate facilities for changing the workflows at runtime in WFMS in a valid and consistent manner. In absence of this support the information system susceptible to changes needs to be tackled by slower porting processes, it not being immediately usable due to the not easily bridgeable gap between the pre-planned and the evolved actuality.
An evolutionary change includes process change at schema level and also
instance migration for all running cases. This paper describes the Yo-Yo
algorithm for Petri net models of acyclic block-structured workflows to carry out
consistent runtime instance migration in this context. At the schema level a
Yo-Yo compatibility property is specified to define the scope of the proposed
instance migration algorithm. A specialty of the algorithm is that it gives the
consistent token transportation based on pre-computed catalog solutions.
Secondly, from the two workflow net schemas, we are able to separate immediately
migratable and immediately not migratable markings. This work uses the Petri
net based workflow model called WF-net, which was introduced by Van der
Aalst [
The paper is organized as follows. After discussing the related work, we first present our pattern based block structured workflow specification approach in Section 3. Following this, the novel representation called Derivation Tree and its colored form are developed in Section 4. In Section 5, the intuition behind the algorithm is first outlined. The ingredients of the algorithm are then discussed developing the notions of the Yo-Yo compatibility property between two nets, instance level correctness of migration in the form of a valid and consistent catalog of token transportation and folding, unfolding operations on WF-net. Lastly, the algorithm, its working and its applicability are explained with the help of a practical example scenario. A proof of correctness of Yo-Yo algorithm is given in Section 6. The algorithm works on colored derivation tree representing the old net and produces colors in the derivation tree of the new net, i.e. colors corresponding to the marking in the new net. The catalog is used for color transfer at each iterative step in the algorithm. 2
In this section, we present a brief account of existing research on dynamic evolutionary changes in Petri net models of workflows to highlight the achievements so far and respective limitations. The literature in this field can be categorized into two kinds. Firstly, the change region based approaches are designed to work with arbitrary structural changes. The second category is of state based approaches. 2.1
An earlier among the change region based approaches is the approach of Ellis
et al. [
Aalst [
Sun and Jiang [
The work of Cicirelli et al. [
The difference between this category and the earlier one is that the state based approaches do not pre-compute the change regions. Instead, they directly provide state based mappings in the new net. If consistent mapping does not exist in a particular state, this approach can not make use of any possibility of delayed migration as in change region based approaches.
It has been noted [
The approach of Agostini and Michelis [
Van der Aalst and Basten [
The paper presents an algorithm for token transportation to ensure the
consistency criterion of history equivalence by applying catalog solutions without
replaying the history, unlike most of the existing approaches. For a practical
scenario of evolution, where thousands of instances need to be migrated, replaying
history for each of them or solving the state equation [
The Yo-Yo token transportation approach offloads some of the complexities
incurred by traditional change region based or state based approaches by means of
its block structured workflow specification. Confining the scope to block
structured workflows is in line with the philosophy of block structured executable
process models in BPEL [
The permissible change operations on workflow schemas have been referred
to as change patterns in the literature [
Block-structured workflows are composed by nesting the primitive patterns. This approach simplifies complex processes in terms of blocks. The block structures are directly folded in or out in the Yo-Yo algorithm. For the purpose of our work we assume that there is no repetition of transition-labels in a net.
Now, a compact string-based specification language called CWS is introduced for specifying block structured acyclic WF-nets. Unlike graphical and tuple based existing description methods for Petri net based workflows, in CWS, the places are dropped and only the labeled transitions are included. The reason for excluding the places is that the consistency criterion based on task execution traces does not require any role from the places. However, places shown in the pictorial models can be regenerated by parsing CWS specifications. The execution control transitions used in fork-join patterns are implicitly encoded into the delimiters, and only the application transitions are included in the specification. Start → SEQ; SEQ → SEQ t SEQ t SEQ | SEQ AN D SEQ | SEQ XOR SEQ | ; AN D → ( SEQ t SEQ ) ( SEQ t SEQ ) ; XOR → [ SEQ t SEQ ] [ SEQ t SEQ ] ; Workflow Net CWS Specification SEQ block in Fig. 1 txty AN D block in Fig. 1 (tx)(ty), (ty)(tx) XOR block in Fig. 1 [tx][ty], [ty][tx] The net in Fig. 8(a) t1(t2(t3)(t4))((t5)(t6)t7)t8 The net in Fig. 8(b) t1t2t3t4(t5)(t6)t7t8
The CWS grammar is shown in Fig. 2. A terminal symbol t represents a transition corresponding to a task in the workflow. Round and square bracket pairs are used to mark AN D and XOR fork-join patterns respectively. The top level pattern is always a Sequence that can generate either an empty string or a nesting of blocks. Example nets specified in CWS are given in Fig. 2. It can be seen that parallel or choice branches can be specified in any order, which creates multiple equivalent specifications. 4
Parsing of workflow models into hierarchical blocks has been implemented
earlier in the approach of Refined Process Structure Tree (RPST) [
For Yo-Yo algorithm, the nets are required to be parsed in a hierarchy of fixedsize ingredient blocks. This parsing obtains the Derivation Tree representation of a WF-net. The derivation tree is obtained after cleaning up the delimiters from the CWS parse tree. For the primitive nets shown in Fig. 1, their respective parse trees and derivation trees are shown in Fig. 3. Table 1 shows the correspondence between symbols in the derivation tree and WF-net.
The terminals in the parse tree are application transitions, delimiters and empty sequences; and the non-terminals represent block-structured configurations in the net. The derivation tree excludes delimiters and empty sequences resulting in leaf non-terminals (e.g. ni and n0x00 in Fig. 3f).
The child nodes of AN D and XOR non-terminals are organized into two triplets representing the two fork-join branches. Each triplet contains two places and a transition. The arcs in a triplet are ordered left to right, showing a transition sandwiched between pre- and post-places respectively.
A derivation tree can be viewed as a hierarchical composition of the derivation tree patterns, which are the derivation trees of the primitive patterns (Figs. 3b,d,f). An Example of derivation tree patterns in a bigger non-primitive net appears in Fig. 5, where the derivation tree patterns are marked as dotted ellipses. In a derivation tree pattern, the arcs coming out of a SEQ node are ordered from left to right. A SEQ node representing only a sequence of two transitions has five arcs, two for the transitions and three for the places. A SEQ node representing the grammatical reduction of an AN D or an XOR branching has three arcs to connect to the branching and the places before and after it. Yield of a non-terminal is a sequence obtained by depth-first traversal on the terminals in the entire subtree rooted at the non-terminal of a derivation tree, where elements of the sequence are terminals or sets of terminals which can be further nested. During the traversal, swapping the traversal order of triplets under an AN D or XOR node does not alter the yield. Hence, yield of an AN D or XOR node is formulated as a set of yields of the two triplets. Operator yield(n) generates this traversal for a non-terminal n. For example, yield(ns) = {tx, ty} in Fig. 3b, yield(ns) = txty and yield(n0s) = in Fig. 3d, yield of the root in Fig. 5a is a sequence with one element {t1t2t3, t4t5t6}, and the root of the derivation tree for the net given in Fig. 8a has yield t1{t2{t3, t4}, {t5, t6}t7}t8. 4.2
To recall, a pattern is any of the tree structures shown in Figs. 3(b,d,f). The notion of local terminal coverage (LTC) defined on patterns establishes pattern to pattern correspondence called peers in two nets. LTC of a pattern p, i.e. LT C(p), is a cross-product s × o of set s of terminals in the pattern and boolean value o indicating whether the set is ordered (i.e. SEQ block). The individual elements can be accessed through a dot operator as p.s and p.o.
Peer Patterns: Two LTCs can be compared by comparing their terminal sets and the ordering. The comparison operator (equality) called peer is defined as follows. Let =s be the set equality operator and =o be the ordered set equality operator. We can define the comparison operator peer(p, q) for two patterns p, q in terms of their respective LTCs, as an operator returning a boolean value: peer(p, q) = ((p.o ∧ q.o) ∧ (p.s =o q.s)) ∨ (¬(p.o ∧ q.o) ∧ (p.s =s q.s)). If both sets are ordered (first part of the disjunction), then the comparison operator checks for element ordering. This condition defines peer relation between sequences. For example, Sequence txty and tytx are not peers, their LTCs being ({tx, ty}, 1) and ({ty, tx}, 1). If one of the sets is unordered (second part of the disjunction), the comparison operator checks for set equality not considering the ordering of elements. This condition defines peer relation between two patterns when one of them is not a sequence. For example, Sequence txty and AND (ty)(tx) are peers, their LTCs being ({tx, ty}, 1) and ({ty, tx}, 0).
The peer operator is thus used to identify pattern to pattern correspondence between two nets, which contributes to the formulation of hand-in-hand folding and unfolding of the nets. For formulation of Yo-Yo compatible derivation trees of a given pair of nets, identification of peer pattern pairs is the very first requirement. The Yo-Yo algorithm carries out token transportation by transferring colors between the peer patterns. Examples of peer patterns can be seen in Fig. 4, where any two derivation trees satisfy the peer relation. 4.3
Coloring of a derivation tree represents a marking of the corresponding net. Nonterminals can be colored following Definitions 1 and 2. Fig. 4 shows examples of colorings of derivation trees and the corresponding net markings . Definition 1 Black Non-terminal : (i) A leaf non-terminal corresponds to a marked place in the net, and (ii) a non-leaf non-terminal abstracts a marked subnet in which no labeled-transition has been fired yet.
Definition 2 Red Non-terminal : It is a non-leaf non-terminal that abstracts a marked subnet where at least one labeled-transition is fired.
This section first develops an intuition to the Yo-Yo algorithm, and then discusses the ingredients of the algorithm, which are the consistency and validity notions, token transportation catalog, pattern hierarchy and folding order. The algorithm is discussed at the end of this section.
As discussed previously, a net is considered as a composition of primitive patterns, and the derivation tree of the net is a hierarchy of derivation trees of the component patterns. Due to the hierarchical structuring of patterns, the patterns in the upper level have places that are abstractions of patterns in the lower level. In other words, a pattern is folded into a place of a pattern which is at a higher level in the hierarchy. The Yo-Yo algorithm transports tokens from old net to new net by transporting tokens between peer patterns of two derivation trees starting from the top level. The tokens move into their places in the new net as they trickle down when the folded places unfold. Resemblance between the stretching and squeezing of the string of the Yo-Yo toy, and the nets being folded and unfolded caused the nomenclature of the algorithm. A token transportation catalog is constructed for the purpose of peer to peer token transportation. Transportation in a larger net is thus carried out by applying the cataloged solutions repetitively through the process of folding and unfolding of the patterns organized in the hierarchy. Given two pattern hierarchies the Folding Order is formulated, using which both of the nets are folded hand-in-hand. 5.1
Yo-Yo compatibility at schema level is a structural property, which is necessary for instance migration by the Yo-Yo algorithm. It ensures that the old and the new nets can be folded and unfolded hand-in-hand. During a workflow life-cycle, at the time of building the new net from the old net, if the changes are confined to only the allowed pattern alterations, the schema compatibility can be achieved.
A pattern in a derivation tree can be from any of AN D, XOR and SEQ blocks. A pattern occurring at any level in the derivation tree can be replaced by another pattern without changing the tasks involved in the pattern. Consequently, the tree of the old net is modified by replacing a derivation tree pattern by another. Two such replacements can be observed in the tree pair shown in Fig. 7. Syntactically, when a Sequence is changed into an AN D and XOR, triplets are formed by including additional nodes according to the grammar. The reverse happens in the case of a change from AN D or XOR to Sequence. These syntactic alterations among the primitive patterns can be observed in Figs. 3b,d,f.
The operator compatible(n1, n2) defines the Yo-Yo schema compatibility between two nets whose derivation trees are rooted at nodes n1 and n2 respectively: compatible(n1, n2)= (yield(n1) =y yield(n2)), where the yield equality operator =y compares two yields considering that swaps of triplets in a fork-join pattern are permissible. An example pair of compatible yields is t1{t2{t3, t4}, {t5, t6}t7}t8 and t1t2t3t4{t5, t6}t7t8 for the trees shown in Fig 8a,b. 5.2
In order to ensure the correctness of the applied dynamic change, validity and consistency of the resultant marking in the new net must be ensured. For Yo-Yo migratability, the following models of consistency and validity are adopted. Axiom 1 Consistency: The tasks which are already completed in the old net are also completed in the new net, and vice-versa.
Axiom 2 Validity: Resulting marking in the new net is reachable from its initial marking. 5.3
The process of abstracting a single primitive pattern into a place in a net is called folding. The reverse, i.e. expansion of a folded place into a pattern is referred to as unfolding. Folding operation simplifies the structure of a net consisting of multiple patterns converging into a single pattern at the top level. Folding operation can be applied multiple times, each one simplifying the net further until the whole net is folded into a single pattern at the top. The original net can be obtained by the reverse process of unfolding abstract places into patterns. (b) A WF-net (a) A Derivation Tree of Fig. 5b
(c) After folding of patterns P1 and P2
Pattern hierarchy of a derivation tree is a partial order capturing the nesting hierarchy of derivation tree patterns. In the corresponding net, it gives the hierarchy of folding of primitive patterns into places. For example, the derivation tree shown in Fig. 5a for the net in Fig. 5b shows the patterns in dotted ellipses for which the pattern hierarchy is given by bottom-up partial order ({P3 ← P2, P3 ← P1}). Each folding expression P ← C in the tree gives a pair of parent-child patterns, where child C is folded into a place in parent P . Expressions in round brackets represent sequences, and sets represent no ordering constraint among its folding expression elements.
Given two pattern hierarchies, a folding order is formulated for applying the Yo-Yo algorithm which is the order to fold the peer patterns hand-in-hand. All parent-child relations among the patterns for each of the two trees are covered (directly or transitively) in the folding order. The top-down folding order expression for the two bottom-up pattern hierarchy expressions ({P3 ← P2, P3 ← P1}) and (P10 ← P20, P30 ← P10) is a sequence (< P3-P30 >, < P1-P10 >, < P2-P20 >) consisting of folding expressions < Pi-Pi0 >, i ∈ {1, 2, 3}, where Pi, Pi0 are peer patterns. An expression in angular brackets is pair of peer patterns. 5.4
The catalog handles token transportation between two different patterns. Transfer between the same patterns are handled by the algorithm through a simpler generic step. Consistent migrations between valid markings of different peer patterns create the cases of the token transportation catalog given in Fig. 6. The counts of valid markings for the three patterns SEQ, AN D and XOR blocks are 3, 6 and 6 respectively. Each marking further generates variants based on (1) whether the influential places are folded and (2) if a marked place is folded, whether a token in it represents none, partial or full completion of the subnet abstracted in it. Some of the resultant markings that are not migratable due to the consistency criterion are omitted from the catalog. The catalog shown in Fig. 6 contains 37 entries all in all, and the transportation mappings among them. The entries are enlisted as colored derivation trees. A bidirectional arrow between migratable colorings of different patterns means that if one is the old pattern coloring the other can be the new coloring. For example, consider the mapping between case 28 and 26. Case 28 is a sequence, where the token is after tx and before ty. Case 26 is an AND pattern which has consistent mapping from case 28. It can be seen that there are two tokens in the two parallel branches of case 26, one after tx and another before ty. Thus, both the cases have completed task tx and hence they are defined to be consistent with each other.
In some cases, a SEQ coloring can be mapped to more than one AN D or XOR colorings. These ties are broken based on the conditions on non-empty yields noted in Table 2. A tag symbol is associated with each condition for use in Fig. 6. Also, if a node in the catalog is identified as a leaf or non-leaf or as a just completed folded place (i.e. holding a token just before the exit), the constraint has to be matched. In the table, node o is in the old SEQ pattern tree, and n1, n2 are in the new fork-join pattern tree. When o is the leftmost child, n1 is the leftmost child, and n2 is the node to the left of tx. When o is the middle child, n1 is the node to the right of tx, and n2 is the node to the left of ty. When o is the rightmost child, n1 is the node to the right of ty, and n2 is the rightmost child. Node n is in the subtree rooted at o s.t. yield(n) =y yield(n2). It can be noted that, since swapping of two tasks in a sequence is not included in the present catalog, the sequence tx, ty never becomes sequence ty, tx. The Yo-Yo algorithm formulates a consistent marking in the new net given the marked old net and a Yo-Yo compatible derivation tree pair of the two nets. The folding order for the derivation tree pair and the token transportation catalog are required for the computation. The algorithm is given in Algorithm 1.
At first, the marking of the old net is translated into a coloring in the derivation tree of the net. Then, the algorithm colors the new derivation tree pattern by pattern in top-down fashion given by the folding order. When all the color ripples reach the leaves, the algorithm successfully terminates.
Input: Old Marked Net N , Unmarked New Net N 0, Uncolored Old Derivation Tree D, Uncolored New Derivation Tree D0, Folding Order F , Token Transportation Catalog
Result: Marking in N 0 1 colorTree(D,N ) 2 Let < p-q > be the first folding expression ‘fetched’ from F , where p and q are peer patterns 3 if modularTransport(p,q) 6= true then return false 4 for every folding expression < p-q > ‘fetched’ from the remainder of F , not violating the partial order specified in F , where q has colored root do 5 if p is colored then 6 if modularTransport(p,q) 6= true then return false 7
else localPropagation(q) 8 Mark the places in N 0 corresponding to Black leaves in D0 9 return true Procedure colorTree(Uncolored Derivation Tree D, Marked Net N )
Result: Coloring in D 1 for each leaf non-terminal n in D corresponding to a marked place in N do 2 color n Black 3 S ← set of colored nodes in D having uncolored parent 4 while S is not φ do 5 n ← any element from S 6 p ← colorParent(n) 7 S ← S \ {n} 8 if p is not NULL then S ← S ∪ {p}
Fig. 7 shows the color propagation traces in the old and then in the new trees. Old Tree: Steps 1-4 depict the bottom-up coloring of the old tree performed by procedure colorTree. It starts by coloring the leaf nodes black corresponding to the marked places in the net of Fig. 8a. Then for each colored node, its parent is colored either red or black by procedure colorTree until the root is colored.
After transferring color between the top peers, the algorithm goes through the peer patterns < pi, qi > from the folding order confronting the following cases: (i) root of qi is uncolored, (ii) pi is colored, root of qi is colored, and (iii) pi is uncolored, root of qi is colored. In case (i) there is no color transfer. In case (ii), procedure modularTransport colors qi. When pi and qi are the same patterns, after replicating the color of pi to qi, a red color transferred to a leaf is turned black to preserve the validity of coloring. If pi and qi are different, cataloged transportations are applied. In case (iii), proc. localPropagation colors qi.
5 else color the leftmost child of r Black
Old Tree: Uncolored
Old Tree: Step 1
Old Tree: Step 2 Old Tree: Step 3
Old Tree: Step 4
New Tree: Uncolored New Tree: Step 1
New Tree: Step 2
New Tree: Step 3 Function modularTransport(Colored Pattern p, Uncolored Pattern q) Data: Token Transportation Catalog
Result: Coloring in q 1 if p and q are same patterns then 2 color q as p // same color transfer 3 change the Red leaves of q to Black // no leaf is left Red 4 return true 5 search catalog for colored p and its mapping to q 6 if no mapping found then 7 print instance not consistently migratable, return false 8 color q as per the search result, return true Function colorParent(non-terminal n) A realistic scenario of dynamic evolution in the reimbursement process in an academic institute is now illustrated where the Yo-Yo algorithm is used for token transportation. The old process schema is modeled by the net depicted in Fig. 8(a). The actual tasks corresponding to each labeled-transition are given in Table 3. As per this design, a student has to first fill the reimbursement form and submit it to initiate a reimbursement request. Next, two concurrent subprocesses begin, one of which is submission of the bills and then approval by guide and head of the department. In parallel, the verification of the funding history for the applicant and funding availability is performed by the awards’ committee, after a favorable result is confirmed by the committee approval. The reimbursement amount granted by these three approvals are lastly credited to the student’s scholarship account thereby completing the workflow.
This design is evolved into the new schema, depicted in Fig. 8(b) due to the following reasons: every time an application is approved by the head of the (a) An Instance of the Old Workflow (b) The New Workflow Schema department only after its approval by the student’s guide. In the new design, this dependency is reflected explicitly to prevent an applicant from making approval request to the HOD prior to his/her guide. Also, for some cases, though the funding background is verified by the awards’ committee, reimbursement is not granted due to rejection either from respective guide or the head. Therefore, to alleviate the unusable funding verification by the awards’ committee, the designed concurrency is now made sequential by moving the funding related activities in the later part of the process.
Dynamic migration of the reimbursement applications already in progress relieves the applicants from having to start fresh. Also, the process is too simple to maintain different versions. Therefore, consistent dynamic instance migration in response to the evolutionary changes are desired. The Yo-Yo algorithm carries out the consistent token transportation as shown in Fig. 8.
The visualization of the transportation in the given net pair is depicted in Fig. 9. The bottom-up coloring of the old derivation tree is equivalent to successive folding operations of the marked old net. Again, pattern by pattern top-down coloring of the new derivation tree is equivalent to unfolding a folded pattern in the new net and marking it each time. Movement of the color ripple into a leaf node is equivalent to reaching of a token into an actual place. In this case, the algorithm terminates when all the transported tokens are placed. Fig. 9 shows the nets being squeezed and released as they undergo token transportation. 6
This section provides a sketch of the proof of correctness and comments on the runtime complexity of the Yo-Yo algorithm. A top-down proof is given based on Old Net: Input Marking New Net: Unfolding Step 1 Old Net: Folding Step 1 Old Net: Folding Step 2 New Net: Unfolding Step 2 New Net: Unfolding Step 3 Old Net: Folding Step 3
New Net: Transported Final Marking a precondition, which is first outlined below.
Completeness of the Catalog A derivation tree of a arbitrary-sized net is composed of derivation trees of the primitive patterns. The folding operation enables us to abstract a bigger net into a single primitive pattern configuration. Given this folding, derivation trees of primitive patterns which are located at a lower level of a bigger derivation tree are abstracted as folded leaf non-terminals in the derivation tree of a pattern located at a higher level. Therefore, a derivation tree of a primitive pattern can have one or more of the following two types of leaf non-terminals based on where the pattern is located in the entire tree: (1) leaves which represent folded lower level patterns. These are tagged as non-leaf in the catalog, and (2) leaves which are actual places in the entire net. These are unfolded leaves which are tagged as leaf in the catalog.
Coloring of derivation trees is an encoding scheme under which all places fall into either of the three color based classes shown in the Table 4.
Every place in a pattern can belong to one of the three classes provided that the resultant marking is a valid marking. Every marked place in a valid pattern marking can be colored black or red. This leads to 6 possible colorings of SEQ pattern given that there are 3 valid markings of the primitive SEQ pattern. There are 6 valid markings of the primitive AND pattern which leads to 20 colorings. Similarly, for 6 valid marking of primitive XOR, there are 12 colorings. Out of these 38 cases, three cases of AND, and two cases of XOR are not migratable to any other consistent and valid making in any other pattern as per the correctness criteria. This gives a total of 33 unique migratable colorings of derivation trees of all primitive patterns. However, 4 more cases need to be considered as follows.
It can be seen that the six rows of the table have been colored using three colors. Using six different colors results in a much bigger catalog. It was found that clubbing the cases reduces the size of the catalog considerably, leaving out 4 extra cases that need to be handled separately. The clubbing is done based on whether the nodes are marked, and if marked, whether at least one task in the folded section is done. In the catalog these 4 extra cases are due to pairs 18 and 37, 4 and 36, 5 and 34, 6 and 35. One case in each pair is covered in the above 33 cases. In this way we obtain 37 valid and exhaustive entries in the catalog.
Mappings among this group are given as per the consistency criteria. For some cases among these 37 cases, there are multiple mappings possible. These are resolved by yield-based tie-breaker rules as explained previously. The Correctness Argument First, the algorithm colors the old derivation tree as per the old net marking, preserving the semantics of derivation tree coloring as given in Section 4.3. Next, it transports the color from the old top pattern to the new top pattern. If this step is not possible without violating consistency, the algorithm terminates. After the transfer, the colors are propagated further down through the descendant patterns in the new tree following the folding order. The color transfer iteratively continues until either no pattern can be colored thus, or till the algorithm terminates on finding the case not migratable. If a case is migratable, Lemma 1 proves that given the yield compatibility at the roots of a peer patterns guaranties that consistent color transfer between them leads to consistent color transfer in the immediate child patterns. To prove that this can be done repetitively for the entire tree Lemma 2 is used. Lemma 3 proves validity of each color transfer. As a result, the algorithm is guaranteed to terminate and produces correct token transportation.
Lemma 1 For a given pattern P 0 in the new tree having yield compatible root with peer pattern P in the old tree, consistent color transfer to P 0 guaranties to find consistent coloring of the immediate child patterns of P 0.
Proof: Coloring P 0 either by modularTransport or localPropagation leads to coloring of the roots of the child patterns visible to P 0. Given the yield compatibility between the roots of P and P 0, this color passing either by catalog cases or localTransport can result in the following variants coloring of a child root against the root of its peer in the old tree. Let Q0 be a direct child pattern of P 0. Let Q0 have peer Q in the old tree. (i) Roots of Q and Q0 have the same color (ii) Both have no color, and (iii) One of them is colored and the other is uncolored. (Note that, if P 0 and P are the same patterns, color transfer to P 0 follows either case (i) or case (ii)).
In case (i), either one of the catalog mappings or the same color replication mapping between Q and Q0 is guaranteed to be applicable. Since both of them are preserve consistency by construction, the lemma applies for this case. In case (ii), a pattern remains uncolored if either token has moved past it or has not reached in it yet. In case (iii), the colored root can be either black or red, which gives us four possibilities. If Q is uncolored and the root of Q0 is black, the token has not reached in Q, whereas in Q0 black color means that is in the source place indicating that no labeled-transition is fired yet. If the root of Q0 is red, the token is past Q, whereas in Q0 it is in the sink place just after firing the last transition in it. The other two possibilities in this case are reverse of the first two possibilities. Given the yield compatibility between the parent roots, i.e. the roots of P and P 0, it ensures the same relative positioning of Q and Q0 with their respective parent patterns, i.e. they are both either left, right or middle children. Therefore, when P and P 0 are consistently colored, a token before Q and after Q0 is a contradiction, which proves case (ii). Similar argument follows for case (iii) also. In this way consistent transportation for the direct children can be achieved. Case (i) is handled by modularTransport, case (ii) and the last two possibilities of case (iii) do not require any coloring action, and the first two possibilities of case (iii) are handled by localPropagation.
Lemma 2 Let two Yo-Yo compatible derivation trees have patterns P, Q in the old tree and their respective peer patterns P 0, Q0 in the new tree. Let Q be child of P and Q0 is child of P 0. Let the roots of P and P 0 satisfy yield compatibility. If P 0 and Q0 satisfy Lemma 1, then so do Q0 and all of its immediate children. Proof: The lemma is about a structural property achieved due to Yo-Yo compatibility and folding order that ensures yield compatibility between the roots of peer patterns extracted from the folding order for coloring at each step of iteration. We use notation SX to represent the yield sequence of the root of derivation sub-tree X. Let the transition terminals of peer patterns P and P 0 be denoted by tx (left) and ty (right). P and P 0 can be either of Sequence or fork-join patterns. We analysis the case where P is a Sequence and P 0 is a fork-join. The other three cases can be proved similarly. When P is a Sequence and P 0 is a fork-join, P 0 has at most six immediate child patterns rooted at its six leaf non-terminals. These are shown in Fig. 10a as Q011, Q012, Q021, Q022, Q031, and Q032. The term Q0 in the lemma refers to each one of them. Similarly, P being a Sequence has three child patterns Q1, Q2 and Q3 as shown in Fig. 10b. Since the roots of P and P 0 are yield compatible, SQ1 txSQ2 tySQ3 =y {SQ011 SQ012 txSQ021 , SQ022 tySQ031 SQ032 }. From this, at subtree level we can observe that SQi =y SQ0i1 SQ0i2 , i ∈ {1, 2, 3}. As each pattern has two transitions, to accommodate four transitions, each of Q1, Q2 and Q3 is a hierarchy of two patterns as shown in Fig. 10c or 10d.
Now there are two cases: Q0 can be either Q0i1 or Q0i2. For the first case, P has subtree as Fig. 10c, and for the second P has subtree as Fig. 10d. In the folding order corresponding to the first case, element < Qi1-Q0i1 > precedes element < Qi2-Q0i2 >, and for the second case they are swapped. As the coloring follows the folding order, after every step the visible parts of the nets are composed of the patterns from the already traversed. In this regard, for the extracted element < Qij -Q0ij >, the roots of Qij and Q0ij are yield compatible and hence, consistent color transfer to Q0ij guaranties consistent color transfer to the next level, thereby proving Lemma 1 for this case. The justification for other combinations of P and P 0 mentioned at the beginning of this argument is skipped due to lack of space. Lemma 3 Peer to peer color transfer preserves validity pattern of coloring. Proof: For catalog transfer cases validity is preserved by construction. For same color replication, validity of the newly produced color is preserved by the correctness of the old pattern coloring and the validity preserving step of the algorithm (line 3 of modularTransport). For local transportation, validity is preserved by following the definitions. Therefore, the lemma is proved.
Time Complexity and Brief Comparison As it can be observed from the algorithm, the asymptotic time complexity of the runtime token transportation in terms of number of patterns n is linear. This computation does not include parsing of the workflow specifications, finding out the compatible derivation tree pairs and the folding order. Therefore, the Yo-Yo approach improves the runtime migration cost by pushing much of the complexity into one-time schema level computations and design time catalog construction depending on the grammar. As compared to history-replay approach, Yo-Yo transportation does not compute or reproduce history. Transportation via pre-computed mappings among marked patterns achieves the desired migration. 7
The paper developed a novel catalog based dynamic token transportation
technique called Yo-Yo algorithm with the help of contributory concepts such as CWS
specification grammar for block structured WF-nets, derivation trees and their
colorings, peer patterns, Yo-Yo compatibility, catalog based transportation, and
folding and unfolding of hierarchically organized patterns. The algorithm uses
the ready-made consistent and valid migration solutions from the token
transportation catalog repetitively to achieve correct transportation for non-primitive
bigger nets. Also, immediately non-migratable markings are automatically
identified by the algorithm due to the non-existence of the corresponding entries in
the catalog. We supplemented the discussion on the algorithm with an example
realistic situation and also provided the sketch of the proof of correctness. We
plan to integrate an implementation of this algorithm in the workflow engine
described in [