Finding AND-OR Hierarchies in Workflow Nets Jacek Sroka Institute of Informatics 7 University of Warsaw, Poland 1 0 [email protected] 2 Jan Hidders n Vrije Universiteit Brussel, Belgium a J [email protected] 6 ] O Abstract L This paper presents the notion of AND-OR reduction, which reduces . a WF net to a smaller net by iteratively contracting certain well-formed s c subnets into single nodes until no more such contractions are possible. [ This reduction can reveal the hierarchical structure of a WF net, and since it preserves certain semantical properties such as soundness, it can 1 help with analysing and understanding why a WF net is sound or not. v The reduction can also be used to verify if a WF net is an AND-OR 9 net. This class of WF nets was introduced in earlier work, and arguably 9 1 describesnetsthatfollowgoodhierarchicaldesignprinciples. Itisshown 2 thattheAND-ORreductionisconfluentuptoisomorphism,whichmeans 0 that despite the inherent non-determinism that comes from the choice of . subnetsthatarecontracted,thefinalresultofthereductionisalwaysthe 1 sameuptothechoiceoftheidentityofthenodes. Basedonthisresult,a 0 7 polynomial-time algorithm is presented that computes this unique result 1 oftheAND-ORreduction. Finally,itisshownhowthisalgorithmcanbe : used to verify if a WF net is an AND-OR net. v i X 1 Introduction r a Petri nets [16] are one of the most popular and well studied formalisms for modeling processes. Their graphical notation is easy to understand, but at the same time concrete and formal, which allows for reasoning over the complex systems that are being modeled. Petri nets are especially useful for business processes and business workflows for which a specific class of Petri nets, called workflow nets,wasintroduced[24,25]. Eventhoughothernotationsareusedin mostindustrialprocessmodelingtoolslikeBusinessProcessModelingNotation (BPMN) [15], Business Process Execution Language (BPEL) or Event-driven Process Chain (EPC) [11], the control flow aspect of the models expressed in those notations can be translated to workflow nets. At the same time workflow 1 netsareconsideredtobethegotoformalismforworkflowanalysis,likedetecting possibleproblems, e.g., existenceofdeadlocksorlivelocks, andforinvestigating the principles of workflow modeling without focusing on a particular language. Workflow models that lack those problems are called sound, and the first definition of workflow-net soundness was proposed by van der Aalst in [24]. Quickly several alternative definitions of soundness, varying in strictness and verification difficulty, emerged. Examples of these are weak soundness [12, 13], relaxed soundness [6], lazy soundness [18], k-soundness and generalised sound- ness[29,28],up-to-k-soundness[27]andsubstitutionsoundness[20]. Informally, theoriginalnotionofsoundnessguaranteestwopropertiesofthenet. First,that if we initiate the workflow net correctly, then no matter how the execution pro- ceeds, we can always end up in a proper final state. Second, that every subtask canbepotentiallyexecutedinsomerunoftheworkflow. Anoverviewofthere- searchonthedifferenttypesofsoundnessofworkflownetsandtheirdecidability can be found in [26]. In earlier research [20] we have proposed a new notion of soundness, namely the substitution soundness or sub-soundness for short. It is similar to k- and *-soundness studied in [29], but captures exactly the conditions necessary for building complex workflow nets by following a structured approach where sub- systems with multiple inputs and outputs are used as building blocks of larger systems. As was shown in that research, it is not enough for such subsystems to be classically sound by themselves. It may be the case, for example, that if a sound WF net is used inside another sound WF net, that the nested WF net is used to execute several simultaneous computations which can interfere and cause the whole WF net to become unsound. Or it can be that partial results, represented by tokens in the output places of the nested WF net, are consumedprematurelybythecontainingWFnetbeforethenestedWFnethas finished properly. This is prevented by the notion of substitution soundness (or sub-soundness), which is informally defined as follows: a WF net is sub-sound iff after initiating it with k tokens in every input place and letting it execute it will always be able to finish by producing k tokens for every output place even if during the run the output tokens are removed by some external transitions. Although stronger soundness properties may be desirable, they are often also more difficult to verify. For this reason, a method is introduced in [20] for systematicallyconstructingworkflownetssothattheyareguaranteedtosatisfy the sub-soundness property. This method is in principle, and in effect, similar to methods employed in software engineering, where complexity is tackled by separationofconcernsandencapsulation,andsystemsaredividedintobuilding blockssuchasmodules,objectsandfunctions,whichinturncanbedecomposed further. We follow those good practices in the context of workflow nets where they, likeinsoftwareengineering,allowtoavoidcommonpitfalls. Similarlytogeneral programminglanguages,alsoforworkflownets,patternsandanti-patternshave been published [25, 22]. Also similarly to general programming, it is beneficial toorganisetheworkflowmodelsinastructuredway. Inprogrammingtheideas ofusingmacros,subroutines,procedures,functions,andlateron,classes,proved 2 that even extremely complex systems can be programmed and maintained in a practical and effective manner. Such structurisation was successfully applied to designing complex Petri nets [33, 21, 7, 1, 8, 17] and workflow nets [2, 23, 20]. As with general programming, the system is composed of small, separated fragments,whichareeasiertounderstandandmaintain. Fragmentscaninclude invocations of other fragments, which can include other nested fragments, and so on. The class of nets we introduced in [20] is called the class of AND-OR nets (seeSection3). Thisclassislargerandmoregeneralthanotherclassesofwork- flow nets generated with a similar type of structural approach, as presented for example in [29, 2]. Apart from studying conditions necessary for structured workflow systems to be *-sound, it was shown in [20] that all AND-OR nets indeed are sub-sound. In this paper we continue this line of research and intro- duce a method to determine the hierarchical structure of a WF net, or parts of it, that was not necessarily designed in such a structured way. In [20] the AND-OR nets were defined as all the nets that can be constructed with a top- downrefinementprocedure,byusingnetsofcertainbasicclassessimilartoS/T systems. In this paper we show that at the same time AND-OR nets that were notnecessarilyconstructedinsuchaway,canbeanalysedtodeterminearefine- ment hierarchy with a bottom-up reduction procedure that contracts subnets of the basic AND-OR classes. Moreover, it is shown that finding occurrences of such subnets can be done in polynomial time. A key result in this paper is that the procedure of contracting subnets of the basic AND-OR classes is confluent and therefore the reduction will always return the same result, independent of how the subnets where selected for con- traction. It is shown in this paper that this can be used to turn the procedure into a polynomial algorithm and therefore a tractable method for determining an AND-OR refinement tree. Next to that, it can also be determined if a net is anAND-ORbycheckingifthereductionprocedurereducesittoaone-nodeWF net. If a net is positively identified as an AND-OR net, it is consequently also guaranteed to be *-sound and sub-sound1, i.e., can be used as a building block of larger systems. A first example of an application of this result would be a scenario where a process modeller constructs a complex model from submodels published in some repository. He or she may want to make sure that the sub- modelsfollowgooddesignprinciplesandaresub-sound, whichmeansthatthey can be safely used as building blocks of a composite model. The repository can contain models for subunits in some organisational structure, e.g., models for facultiesofanuniversityordepartmentsofacompanyorevenmodelsfromsome global repository of socially shared workflows, which appear in e-science [5]. The reduction algorithm can not only be used for AND-OR nets, but also for the analysis of *-soundness and sub-soundness of general workflow nets. It can help the user with finding problems causing unsoundness. More concretely, if the result of AND-OR verification is negative, then the reduction algorithm 1It follows straightforwardly from the definitions of *-soundness and sub-soundness that thelatterimpliesthefirst. 3 stops without reaching a one-node WF net. This resulting net can serve as a condensed version of the original net and point the user to the source of the problem in the design. Note that a WF net may be not an AND-OR net, but still be *-sound or sub-sound. We conjecture, but have not proven, that to verify *-soundness or sub-soundness of an arbitrary net, it is enough to verify *-soundness or sub-soundness of the net resulting from AND-OR verification procedure. The contractions used in our algorithm would have to be proven to preserve *-soundness or sub-soundness, similarly as for example rules of [14] preserve liveness and boundedness. This would give a symmetric and probably similarlylaboriousresultto[20],whereitwasshownthatsubstitutionsofAND- OR nets into AND-OR nets preserve sub-soundness, from which it follows that they also preserve *-soundness. The reduced net, resulting from AND-OR net verification procedure, could then undergo a proper soundness verification with similar methods as in [31, 32]. Furthermore, limiting the size of the verified net withhierarchicalmethodscanbehelpfulforusersstrugglingwithunderstanding thereasonsforunsoundnessofworkflownets. Thatthisisoftenaproblem,even when using automated verification tools, is for example reported in [9]. Finally, as a byproduct of a successful reduction, a tree structure describing the nesting of the fragments of the net can be determined. As with similar methods [2, 4, 3], which deal with workflow net class which is a proper subclass ofAND-ORnets,suchatreestructurecanbeusedformodelingrecoveryregions or determining sound markings, or just for better understanding the structure of the workflow net and its properties. The latter can for example help with determining how parts of the workflow can best be distributed to independent organisational units or to different servers in case of workflows representing computations, e.g., as in scientific workflows. In related work [30] a set of heuristics was proposed to find appropriate decomposition boundaries, which results in a refinement tree for a given graph. Our approach, however concentrates specifically on workflow nets which are generalised to allow multiple inputs and outputs, and it is closely tied in a well understood manner to their semantics and soundness properties. The outline of the remainder of this paper is as follows. In Section 2 the basic terminology of WF nets and their semantics is introduced. In Section 3 the class of AND-OR nets is introduced, based on the notions of place and transition substitution, where a node is replaced with a WF net. In Section 4 the notion of AND-OR reduction is introduced, which is based on the notion of contraction, where certain well-formed subnets of WF nets are contracted into single nodes. It is discussed here how this reduction process is confluent in that it returns a unique result up to the choice of the identity of the nodes. This is based on the observation that the process is locally confluent, but since the proofofthisobservationisquiteinvolved,itispresentedseparatelyinSection5. In Section 6 a concrete polynomial algorithm for computing the result of the AND-OR reduction is presented, and it is shown how it can be used to verify if a WF net is an AND-OR net. Finally, in Section 7 a summary of the results is given, and potential future research directions are discussed. 4 2 Basic terminology and definitions Let S be a set. A bag (multiset) m over S is a function m : S → N. We use + and − for the sum and the difference of two bags and =, <, >, ≤, ≥ for comparisons of bags, which are defined in the standard way. We overload the set notation, writing ∅ for the empty bag and ∈ for the element inclusion. We list elements of bags between brackets, e.g. m = [p2,q] for a bag m with m(p) = 2, m(q) = 1, and m(x) = 0 for all x ∈/ {p,q}. The shorthand notation k.misusedtodenotethesumofkbagsm. ThesizeofabagmoverS isdefined as |m|=Σ m(s). s∈S Definition 1 (Petri net). A Petri net is a tuple N = (P,T,F) where P is a finite set of places, T is a finite set of transitions such that P ∩T = ∅ and F ⊆(T ×P)∪(P ×T) the set of flow edges. We will refer to the elements of P ∪T also as nodes in Petri net. We say that the type of a node is place or transition if it is in P or T, respectively. A path in a net is a non-empty sequence (n ,...,n ) of nodes where for all 1 m i such that 1 ≤ i ≤ n−1 it holds that (n ,n ) ∈ F. Markings are states i i+1 (configurations) of a net and the set of markings of N = (P,T,F) is the set of all bags over P and is denoted as M . Given a transition t ∈ T, the preset N •t and the postset t• of t are the sets {p | (p,t) ∈ F} and {p | (t,p) ∈ F}, respectively. In a similar fashion we write •p and p• for pre- and postsets of places,respectively. Toemphasisethefactthatthepreset(postset)isconsidered within some net N, we write • a, a• . We overload this notation by letting N N •a (a•) also denote the bags of nodes that (1) contain all nodes in the preset (postset) of a exactly once and (2) contains no other nodes. A transition t∈T is said to be enabled at marking m iff •t ≤ m. For a net N = (P,T,F) t with markings m and m and a transition t ∈ T we write m −→ m , if 1 2 1 N 2 t is enabled at m and m = m − •t + t•. For a sequence of transitions 1 2 1 σ =(t ,...,t ) we write m −σ→ m , if m −t→1 m −t→2 ...−t→n m , 1 n 1 N n+1 1 N 2 N N n+1 and we write m −∗→ m , if there exists such a sequence σ ∈ T∗. We will 1 N n+1 t σ ∗ write m −→ m , m −→ m and m −→ m , if N is clear from the 1 2 1 n+1 1 n+1 context. We now introduce the notion of Workflow net, which is a Petri net where certain places and transitions are marked as input and output nodes. Definition 2 (I/O net). An I/O net is a tuple N = (P,T,F,I,O) where (P,T,F) is a Petri net with a non-empty set I ⊆ P ∪T of input places and a non-empty set O ⊆P ∪T of output places. In our setting we will restrict ourselves to I/O nets where input and output nodes are either all places, or all transitions. Definition 3 (I/OconsistentI/Onet). AnI/OnetN =(P,T,F,I,O)iscalled I/O consistent if I∪O ⊆P or I∪O ⊆T. 5 As is usual for Petri nets that model workflows, we will also require that all nodes in the net can be reached from an input node, and from all nodes in the net an output node can be reached. Definition 4 (Well-connected I/O net). An I/O net N = (P,T,F,I,O) is called well-connected if (1) every node in P ∪T is reachable by a path from at least one node in I and (2) from every node in P ∪T we can reach at least one node in O. The formal definition of Workflow net is then as follows. Definition 5 (Workflow net). A workflow net (WF net) is a I/O net N = (P,T,F,I,O) that is I/O consistent and well-connected. IfI∪O ⊆P,thenwecallN aplaceworkflownet (pWFnet),andifI∪O ⊆T, thenatransitionworkflownet (tWFnet). TheI/Otype ofaWFnetisthetype of its input and output nodes, i.e., it is place if it is pWF net, and transition if it is a tWF net. Note that input places can have incoming edges in a workflow net, and that output places can have outgoing edges. We will refer to the nodes in I ∪O as theinterface nodes ofthenet. Wewillcallaworkflownetaone-input workflow net if I contains one element, and a one-output workflow net if O contains one element. Often, as in [24], workflow nets are restricted to one-input one-output place workflow nets. We generalise this in two ways: first by allowing also nets with input and output transitions rather than input and output places, and second by allowing multiple input and output places/transitions. For these generalised workflow nets we define the corresponding one-input one-output pWF net as follows. The place-completion of a tWF net N = (P,T,F,I,O) is denoted as pc(N) and is a one-input one-output pWF net that is constructed from N by adding places p and p such that p •=I and •p =O and setting i o i o theinputsetandoutputsetas{p }and{p },respectively. Thisisillustratedin i o Figure 1 (a). In such diagrams we will indicate nodes in I with an unconnected incoming arrow and nodes in O with an unconnected outgoing arrow. The transition-completion of a pWF net N = (P,T,F,I,O) is denoted as tc(N) and is a one-input one-output tWF net that is constructed from N by adding transitions t and t such that t • = I and •t = O and setting the input set i o i o andoutputsetas{t }and{t }, respectively. ThisisillustratedinFigure1(b). i o Inthispaperwediscussaparticularkindofsoundness,namelythesoundness thatguaranteesthereachabilityofaproperfinalstate[20]. Wegeneralisethisfor thecasewhere(1)therecanbemorethanoneinputplaceand(2)thesecontain one or more tokens in the initial marking. We also provide a generalisation of soundness for tWF nets, which intuitively states that after k firings of all input transitions the computation can end in an empty marking while firing each of the output transitions exactly k times. Definition 6 (k and *-soundness). A pWF net N = (P,T,F,I,O) is said to ∗ ∗ bek-sound ifforeachmarkingmsuchthatk.I −→mitholdsthatm−→k.O. 6 pc(N)ifN isatWFnet tc(N)ifN isapWFnet pi N po ti N to (a) (b) Figure1: Aplace-completedtWFnetandtransition-completionpWFnet(from [20]) We call N *-sound if it is k-sound for all k ≥ 1. We say that these properties hold for tWF net N if they hold for pc(N). By definition place-completion does not affect the *-soundness. However, as we observed in [20, 19], for transition-completion this is only true in one directionaseverypWFnetN is*-soundiftc(N)is*-soundbutnotviceversa. 3 Definition of AND-OR nets In thissection weintroduce theAND-OR netsand show thattheyare *-sound. For that we recall some definitions and a result from [20, 19] where we defined a method for constructing complex nets by substituting their nodes with other nets - places by pWF nets and transitions by tWF nets. Definition 7 (Place substitution, Transition substitution). Consider two dis- joint WFnetsN andM,i.e.,ifN =(P,T,F,I,O)andM =(P(cid:48),T(cid:48),F(cid:48),I(cid:48),O(cid:48)), then (P ∪T)∩(P(cid:48)∪T(cid:48))=∅. Place substitution: If p is a place in N and M is a pWF net, then we define theresultofsubstitutingpinN withM, denotedasN⊗ M, asthenetthatis p obtainedifin N weremovepandtheedgesin whichitparticipatesandreplace itwiththenetM andedgessuchthat•p(cid:48) =•pforeachinputplacep(cid:48) ∈I(cid:48) ofM and p(cid:48)•=p• for each output place p(cid:48) ∈O(cid:48) of M. If p∈I then p is replaced in the set of input nodes of the resulting net with I(cid:48), i.e., the input set of N⊗ M p is (I\{p})∪I(cid:48), and if p ∈ O then p is replaced in the set of output nodes of the resulting net with O(cid:48), i.e., the output set of N ⊗ M is (O\{p})∪O(cid:48). p Otherwise, the input and output sets of N⊗ M are the same as the respective p sets for N. Transition substitution: Likewise, if t is a transition in N and M is a tWF net,thenwedefinetheresultofsubstitutingtinN withM,denotedasN⊗ M, t as the net that is obtained if in N we remove t and the edges in which it participatesandreplaceitwiththenetM andedgessuchthat•t(cid:48) =•tforeach input transition t(cid:48) ∈ I(cid:48) of M and t(cid:48)• = t• for each output transition t(cid:48) ∈ O(cid:48) of M. If t∈I then t is replaced in the set of input nodes of the resulting net with 7 I(cid:48), i.e., the input set of N ⊗ M is (I\{t})∪I(cid:48), and if t∈O then t is replaced t in the set of output nodes of the resulting net with O(cid:48), i.e., the output set of N ⊗ M is (O\{t})∪O(cid:48). Otherwise, the input and output sets of N ⊗ M are t t the same as the respective sets for N. Theresultsofaplacesubstitutionandtransitionsubstitutionareillustrated in Figure 2 (a) and (b), respectively. It is not hard to see that for all WF nets N andM andnanodeinN suchthatN⊗ M isdefined,itisagainaWFnet. n ItalsoholdsforallWFnetsA,B andC that(A⊗ B)⊗ C =A⊗ (B⊗ C), n m n m and (A⊗ B)⊗ C =(A⊗ C)⊗ B if n and m are different nodes in A. n m n m N N p t M N⊗pM N⊗tM M M M (a) (b) Figure2: Illustrationofplacesubstitutionandtransitionsubstitution(adapted from [20]) Wewillgeneratenetsbystartingfromsomebasicclassesofnetsandallowing substitutions of places with pWF nets and transitions with tWF nets. Definition 8 (Substitution closure). Given a class C of nets we define the substitution closure of C, denoted as S(C), as the closure of C under transition substitution and place substitution, i.e., the smallest superclass S(C) of C that satisfies the following two rules for every two disjoints nets N and M in S(C): (1)ifM isapWFnetandpaplaceinN thenN⊗ M isanetinS(C)and p (2)if M isa tWFnet and t atransition in N then N⊗ M isa netin S(C). t The motivation for using the concept of substitution closure to define in- teresting classes of nets is that it makes it straightforward to show for such a class that its nets have a certain property, such as a certain kind of soundness, 8 by showing that (1) this property holds for the nets in the initial class and (2) this property is preserved by substitution. As was argued in earlier work [20], *-soundness is not preserved by substitution, but substitution does preserve a stronger property called substitution soundness. The intuition behind this no- tion of soundness is that the execution of a net, when started with the same number of tokens in all input places, should always be able to finish properly, even if the execution is interfered with by removing at some step an identical number of tokens from all output places. More precisely, if we start the net if k token in all its input places, and somewhere during the execution remove k(cid:48) tokens from all the output places, then the net should be able to finish with k−k(cid:48) tokens in its output places. Definition 9 (substitution soundness). A pWF net N =(P,T,F,I,O) is said to be substitution sound if for all 0 ≤ k(cid:48) ≤ k and every marking m(cid:48) of N such that k.I −∗→ m(cid:48)+k(cid:48).O it holds that m(cid:48) −∗→ (k−k(cid:48)).O. A tWF net is said to be substitution sound if its place-completion is substitution sound. Thechoicefortheinitialclassesismadesuchthattheseareindeedsubstitu- tion sound. Their intuition is based on that of acyclic marked graphs (T-nets) and state machines (S-nets), as considered in [29]. The basic idea of T-nets is that during executions no choices are made about who consumes a token and each transition will fire in the execution of a workflow. This is captured by a syntactic restriction that says that places have exactly one incoming edge and one outgoing edge. We will call this the AND-property of a WF net. Definition 10 (AND property). A WF net N =(P,T,F,I,O) is said to have the AND property if for every place p∈P it holds that (1) p∈I∧|•p|=0 or p∈/ I∧|•p|=1 and (2) p∈O∧|p•|=0 or p∈/ O∧|p•|=1. Note that in this definition being an input node is considered equivalent to having an extra incoming edge, and being an output node equivalent to having an extra outgoing edge. The basic idea of S-nets is that they represent a state machine, with the staterepresentedbyasingletokenthatisinoneoftheplaces. Thisiscaptured by a restriction that says that transitions have exactly one incoming edge and one outgoing edge. We will call this the OR-property of a net. Definition 11 (OR property). A WF net N = (P,T,F,I,O) is said to have the OR property if for every transition t∈T it holds that (1) t∈I ∧|•p|=0 or t∈/ I∧|•t|=1 and (2) t∈O∧|t•|=0 or t∈/ O∧|t•|=1. Although all WF nets with the OR property are substitution sound, it is unfortunately not the case that all WF nets with the AND property are substi- tution sound. Consider for example an AND net containing a transition t with a loop containing a place p. Note that because of the AND property place p can have no other edges except those of the loop. Therefore, the transition t can never fire, since that would require a token in p, but such a token can only be generated by firing t. To remedy this, we will define AND nets as WF nets 9 pANDnet tANDnet pORnet tORnet Figure 3: Examples of a pAND, tAND, pOR and tOR nets (adapted from [20]) that not only satisfy the AND property but are also acyclic, which leads to the following definitions of AND and OR nets. Definition 12 (ANDnet). AnAND net isanacyclicWFnetthatsatisfiesthe AND property. An AND net that is a pWF net is called a pAND net, and if it is a tWF net it is called a tAND net. Definition13(ORnet). AnORnet isaWFnetthatsatisfiestheORproperty. An OR net that is a pWF net is called a pOR net, and if it is a tWF net it is called a tOR net. For some examples of AND and OR nets see Figure 3. We will use names to identify the classes of nets we have just defined. The classes of pOR nets, pAND nets, tOR and tAND nets will be denoted as pOR, pAND, tOR and tAND. In addition we will prefix the name with 11 if the class contains only nets with one input node and one output node. So 11pOR is the class of one- input one-output pOR nets, and 11tAND is the class of one-input one-output tAND nets. Since our aim is to generate substitution sound nets, which as we will show arealso*-sound,wewillrestrictthetANDnetstoone-inputone-outputnets,so theclass11tAND. ThereasonisthatalthoughallpANDnetsaresubstitution sound, it is not true that all tAND nets are substitution sound, as is illustrated bythetANDnetinFigure3. RecallthatthesoundnessofatWFnetisdefined as the soundness of its place-completion which adds a single place before the input transitions and a single place after the output transitions. So if we put a singletokeninthefirstplaceinthisplace-completion, thenonlyoneofthefirst transitionscanfire, afterwhichthenetcannolongercorrectlyfinish. Asimilar problem occurs in the pOR net in Figure 3. If it starts with a token in each of its input places, then it cannot finish correctly if it moves the token of the upper input place to the place in the middle of the net. Both types of problems are solved if we only consider one-input one-output versions of tAND and pOR nets, which are all substitution sound nets. Hence we only consider the classes illustratedinFigure4, whichwewillrefertoasthebasic AND-OR classes, and theclassofnetsthatisobtainedbycombiningthembysubstitutionwewillcall the class of AND-OR nets. Definition 14 (AND-OR net). The class S(pAND∪11tAND∪11pOR∪ tOR) is called the class of AND-OR nets. 10