A crucial task in process management is the validation of process re nements. A process re nement is a process description in a more ne-grained representation. The re nement is either with respect to an abstract model or with respect to component's principle behaviour model. We de ne process re nement based on the execution set semantics. Predecessor and successor relations of the activities are described in an ontology in which the re nement is represented and validated by concept satis ability checking.
The re nement of processes is a common task in process development. A generic process describes the core functionality of an application. A re nement is a transformation of a process into a more speci c process description which is developed for a more concrete application and based on more detailed process behaviour knowledge. A key question is whether a process re nement is valid, i.e. the re ned process refers to the intended behaviour of the abstract process.
We distinguish between horizontal and vertical re nement. A horizontal re nement is a transformation from an abstract to a more speci c model. A vertical re nement is a transformation from a principle behaviour model of a software component to a concrete process model of business. Once a re ned process model describes a concrete application process, the relationship to the original generic process is not always obvious due to a number of possibly complex re nement steps. A re nement step includes customisation, extensions and compositions of processes. Therefore it is quite di cult to validate the re nement of a process with respect to an abstract process model.
The validation of a process re nement consists of checking model constraints like execution order constraints. Modelling constraints for the re ned process has to cover the constraints of the generic process behaviour and also constraints which emerged during the re nement steps.
In this paper, we use execution set semantics to analyse process re nements. This set-based formalism accounts for a comparison of the process executions of di erent processes. The comparison of process execution sets is then reduced to the comparison of nite sets of predecessor and successor relations which is realized by subsumption checking. We further use ALC ontologies to model processes and process constraints, concerning the execution order conditions and binding of tasks. Finally the re nement checking is reduced to concept satis ability checking.
In Section 2 we de ne the problem of process re nement with its graphical syntax, semantics and mathematical foundation. The modelling of processes with the corresponding execution constraints is demonstrated in Section 3, followed by the re nement validation. 2 2.1
A process is a non-simple directed graph without multiple edges between two vertices. A vertex is either an activity, a gateway, a start, or an end event. As a graphical process syntax, we use the business process modelling notation (BPMN)1 due to its wide industry adoption. As an example, in Fig. 1, (a) shows a BPMN diagram of a simple ow which consists of two activities between the Start and End nodes; (b) shows the usage of exclusive gateway ( ) indicating that the ow can go through one and only one of its branches, and parallel gateway ( ) indicating that the ow should go through all of its branches; (c) shows the usage of a loop indicating that the ow can go back to previous gateways or activities. In block-based process modelling, gateways always appear in pairs. Thus in this work we consider only pairwise gateways to comply such convention. Also, we assume all the process models are valid by their own.
As a prerequisite to validating, we de ne the correctness of process re nement
based on the execution set semantics [
1 http://www.bpmn.org/
To facilitate horizontal validation, the process architect has to declare which activities of Fig. 1b implement which activity of Fig. 1a: hori(a1) = hori(a2) = hori(a3) = A, hori(b1) = B, hori(b2) = B. While for vertical validation, the process architect needs to link activities of Fig. 1b to service endpoints given in Fig. 1c and d: vert(a1) = E, vert(a2) = vert(a3) = D, vert(b1) = F, vert(b2) = C. In case such originality relations characterise the re nement, we assume they are always correct in this work.
Correct horizontal re nement. We say that a process Q is a correct horizontal re nement of a process P if ESQ ESP after the following transformations. 1. Renaming. Replace all activities in each execution of ESQ by their originators (function hori()). Renaming the execution set f[a1a2b1b2]; [a1b1b2a2]; [a1b1a2b2]; [a1a3]g of Fig. 1b yields f[AABB]; [ABBA]; [ABAB]; [AA]g. 2. Decomposition. Replace all pairs of duplicate activities by a single activity in each execution of ESQ. For Fig. 1b this yields f[AB]; [ABA]; [ABAB]; [A]g. As f[AB]g 6 f[AB]; [ABA]; [ABAB]; [A]g, Fig. 1b is a wrong horizontal re nement of Fig. 1a. The cause is the potentially inverted order of AB by b1a2 or b2a2 in Fig. 1b and that a3 can be the last activity in Fig. 1b, whereas A must always be followed by B in Fig. 1a.
Correct vertical re nement. We say that a process Q is a correct vertical re nement of a process P if ESQ ESP after the following transformations. 1. Renaming. Replace all activities in each execution of ESQ by their grounds (function vert()). Renaming the execution set f[a1a2b1b2]; [a1b1b2a2]; [a1b1a2b2]; [a1a3]g of Fig. 1b yields f[EDFC]; [EFCD]; [EFDC]; [ED]g. 2. Reduction. Remove all activities in each execution of ESQ that do not appear in P . For our example, reduction with respect to Component 1 yields f[DC]; [CD]; [D]g. Reduction with respect to Component 2 yields f[EF]; [E]g. As f[C]; [D]; [CC]; [CD]; [DC]; [DD]; : : :g f[DC]; [CD]; [D]g and f[EF]; [E]g f[EF]; [E]g, Fig. 1b is a correct vertical re nement of both Component 1 and 2.
As enumerating the execution sets for validation is infeasible, our solution works with descriptions in ontology instead of using the execution sets themselves. 3
In this section, we present our solution of validating process re nement with ontologies in detail. We accomplish the transformations from the last section by reductions on the process diagram and execution sets, represent the re nement with an ontology, and validate the re nement by concept satis ability checking. 3.1
Because the execution set may contain in nite number of executions, e.g. EScomponent1, it's di cult to directly compare them. Therefore we reduce the subsumption between in nitely large execution sets into subsumption between nite predecessor and successor sets that are also obtained from the process diagram and show that the transformations on the execution sets are equivalent to transformations on the process diagrams or the predecessor and successor sets.
As we can see from ESSpecific, the execution ordering relations between branches of a parallel gateway are implicit in the original process. In order to make them explicit, we rst reduce a process diagram by the following operation: A parallel gateway ([B1jP1]; : : : ; [BnjPn]) is reduced to an exclusive gateway B1 (P1; [B2jP2]; : : : ; [BnjPn]) ; : : : ; Bn ([B1jP1]; : : : ; [Bn 1jPn 1]; Pn) , where the notation [BjP ] represents a path with B the head and a subpath P the tail.
We repeatedly apply above operation until there's no parallel gateway in the diagram. Such an iteration will always terminate due to the nite size of the process. The resulting BPMN graph is called the Execution Diagram of P , denoted by EDP (see Fig. 2). An activity a 2 P may have multiple appearance in EDP . We use one more subscript j to di erentiate them, i.e. a21, a22 w.r.t. a2. This transformation may increase the size of the process model exponentially, e.g. a pair of parallel gateways containing n branches of one activity will be transformed into a pair of exclusive gateway containing n! branches of n activity.
Obviously, given a process P , its execution set ESP is the set of all routes between Start and End in its execution diagram EDP after replacing duplicated activities with their original names.
We further reduce EDP from a local perspective. For each activity appearance a in EDP , its Predecessor Set P SP (a) is the set of all the activities going to a through a direct link or a sequence containing only gateways. And its Successor Set SSP (a) is the set of all the activities going from a through a direct link or a sequence containing only gateways.
Obviously, according to the de nition, for each x; y such that x 2 P SP (aj ), y 2 SSP (aj ), [x; aj ; y] is a valid subpath of activities in EDP and thus [x; a; y] is a valid subpath of activities in P . Because the EDP is nite, P SP (aj ) and SSP (aj ) are also nite for any aj 2 P . Follow our example, P S(a31) = fa11g and SS(a31) = fEndg.
By obtaining these two sets for all the activities, the relation between two execution sets can be characterised by the following theorem:
SSP (a).
ESP i 8a 2 Q, P SQ(a)
P SP (a) and SSQ(a) Proof. (1) For the ! direction the lhs ESQ ESP holds. Given a 2 Q and b 2 P SQ(a), we demonstrate that b 2 P SP (a) holds: [b; a] is a subpath of some X 2 ESQ, from precondition it follows [b; a] is a subpath of X 2 ESP and the de nition of P S leads to b 2 P SP (a). Correspondingly for c 2 SSQ(a), it follows from de nition [a; c] is a subpath of some Y 2 ESQ and from precondition follows [a; c] is a subpath of Y 2 ESP . The de nition of SS leads to c 2 SSP (a). (2) For the direction the rhs holds and we demonstrate that ESQ ESP follows. Consider an execution s 2 ESQ, s = a1; : : : ; an. Activity ai 1 is predecessor of ai. For i = 2; : : : ; n the following implication holds: P SQ(ai) P SP (ai) ) [ai 1; ai] is a subpath of some X 2 ESP . For i = 1; : : : ; n 1 the following implication holds: SSQ(ai) SSP (ai) ) [ai; ai+1] is a subpath of some Y 2 ESP , therefore sequentially connect the subpathes [a1; : : : ; an] 2 ESP holds.
Therefore, we reduce the process re nement w.r.t. execution set semantics into the subsumption checking of nite predecessor and successor sets. We then show that the transformation operations of execution sets can be equivalently performed on the original process diagrams and the predecessor and successor sets obtained from them: { Reduction on the process diagrams has the same e ect on the execution sets. That means, given a component model P and a process model Q, if we reduce Q into Q0 by removing all the activities that do not appear in P , and link their predecessors and successors directly, the resulting ESQ0 will be the same as the reduction of ESQ with respect to P . { Renaming can also be directly performed on the process diagram, i.e.
ESP [a ! A] = ESP [a!A]. Thus, the renaming can be performed on the predecessor and successor sets as well, i.e. P SP (x)[a ! A] = P SP [a!A](x) (SSP (x)[a ! A] = SSP [a!A](x)). { Decomposition can be done on the predecessor and successor sets as well.
Particularly, ESQ0 ESP , where ESQ0 is ESQ after decomposition of all the sequential x grouped into a single x, i 8a 6= x, P SQ(a) P SP (a), SSQ(a) SSP (a) and 8x, P SQ(x) [ fxg P SP (x) and SSQ(x) [ fxg SSP (x). This interprets the decomposition as, any x that should be grouped, can go not only from predecessors of x, but also another appearance of x, and can go not only to successors of x, but also another appearance of x.
Thus, above analysis implies that: { For horizontal re nement, we can rst obtain the predecessor and successor sets of activities, and then perform the Renaming and Decomposition on these sets, and then check the validity. { For vertical re nement, we can rst perform the Reduction on processes, then obtain the predecessor and successor sets and perform the Renaming on these sets, and nally check the validity.
In this paper, we perform Reduction directly on the process diagram and obtain the predecessor and successor sets from its execution diagram, then perform Renaming and Decomposition with ontologies and check the validity with reasoning. 3.2
In this section we represent the predecessor and successor sets of activities with ontologies. In such ontologies, activities are represented by concepts. The predecessors and successors relations are described by two roles from and to, respectively. Composition of activities in horizontal re nement is described by role compose. Grounding of activities in vertical re nement is described by role groundedTo. The last two don't have essential logic di erence in the problem of process re nement but have di erent semantics in the process model, so that we distinguish between them. Then, for a set S containing predecessors or successors, we de ne four operators for translations as follows: De nition 1. :
Pre-re nement-from operator Prfrom(S) = 8f rom: Fx2S x Pre-re nement-to operator Prto(S) = 8to: Fy2S y Post-re nement-from operator Psfrom(S) = dx2S 9f rom:x Post-re nement-to operator Psto(S) = dy2S 9to:y
The e ect of the above operators in re nement checking can be characterised by the following theorem:
Disjoint(xjx 2 P [ Q) infers that Prfrom(P SP (a))uPsfrom(P SQ(a)) is satis able.
SSQ(a) SSP (a) i Disjoint(xjx 2 P [ Q) infers that Prto(SSP (a))uPsto(SSQ(a)) is satis able.
For sake of a shorter presentation, we only prove the rst part of the theorem. The proof for the second part is appropriate to the rst part.
Proof. (1) We demonstrate ! direction with a proof by contraposition. The disjointness of activities holds. Supposed the rhs is unsatis able, i.e. Prfrom(P SP (a))uPsfrom(P SQ(a)) is unsatis able. Obviously, both concept definitions on its own are satis able, since Prfrom(P SP (a)) is just a de nition with one all-quanti ed role followed by a union of (disjoint) concepts. The concept de nition behind this expression is 8f rom: Fx2P SP (a) x which restricts the range of f rom to all concepts (activities) of P SP (a). Psfrom(P SQ(a)) is a concept intersection which only consists of existential quanti ers and the same f rom role. This de nition is also satis able. Therefore the unsatis ability is caused by the intersection of both de nitions. In Psfrom(P SQ(a)) the same role f rom is used and the range is restricted by Prfrom(P SP (a)). Therefore the contradiction is caused by one activity b 2 P SQ(a) which is not in P SP (a), but this is a contradiction to the precondition P SQ(a) P SP (a). (2) For the direction we assume that the rhs Disjoint(xjx 2 P [ Q) infers that Prfrom(P SP (a))uPsfrom(P SQ(a)) is satis able. For each activity b 2 P SQ(a) we show that b is also in P SP (a): b 2 P SQ(a) and Psfrom(P SQ(a)) is satis able, the intersection contains the term 9f rom:b. Since Prfrom(P SP (a)) is satis able and is also the range restriction of f rom, it follows that b 2 P SP (a).
This theorem indicates that the re nement checking of processes can be reduced to the satis ability checking of concepts in an ontology. In the following, we present the representation of horizontal re nement and vertical re nement. Horizontal Re nement For conciseness of presentation, we always have a pre-re nement process and a post-re nement process and we re ne one activity in each step (this activity may have multiple appearance after conversion to the execution diagram). We assume P the pre-re nement process, Q the post-re nement process and z the activity being re ned. For each zj we de ne component zj 9compose:zj. The simultaneous re nement of multiple activities can be done in a similar manner of single re nement. Then we construct an ontology OP !Q with following axioms: 1. for each activity a 2 Q and hori(a) = zj, a v 9compose:zj
These axioms represent the composition of activities with concept subsumptions, which realise Renaming in horizontal re nement. For example, b11 v 9compose:B and a31 v 9compose:A. 2. for each a 2 Q and a is not re ned from any zj a vPrfrom(P SP (a))[zj ! component zj], a vPrto(SSP (a))[zj ! componennt zj], These axioms represent the predecessor and successor sets of all the unrened activities in the pre-re nement process. Because in the post-re nement process, any activity re ned from zj will be considered as a subconcept of component zj, we replace the appearance of each zj by corresponding component zj. For example, Start v 8to:component A. 3. for each zj 2 P , component zj vPrfrom(P SP (zj) [ fcomponent zjg)[zj ! componennt zj], component zj vPrto(SSP (zj) [ fcomponent zjg)[zj ! componennt zj], These axioms represent the predecessor and successor sets of all the re ned activities in the pre-re nement process. Due to the mechanism of Decomposing, we add the corresponding component zj to their predecessor and successor sets, and replace the zj with component zj for the same reason as before. For example, component A v 8f rom:(Start t component A), component A v 8to:(component B t component A), component B v 8f rom:(component A t component B) and component B v 8to:(End u component B). 4. for each a 2 Q, a vPsfrom(P SQ(a)) and a vPsto(SSQ(a)),
These axioms represent the predecessor and successor sets of all the activities in the post-re nement process. For example, a31 v 9to:End, b11 v 9to:a21 u 9to:b22 5. for each zj 2 P , Disjoint(aja 2 Q and Hori(a) = zj)
These axioms represent the uniqueness of all the sibling activities re ned from the same zj. For example, Disjoint(a11; a21; a22; a23; a31). 6. Disjoint( all the activity in P , and all the component zj).
This axiom represents the uniqueness of all the activities before re nement. For example, Disjoint(Start; End; A; B; component A; component B).
With above axioms, ontology OP !Q is a representation of the horizontal re nement from P to Q by describing the predecessor and successor sets of corresponding activities with axioms.
Vertical Re nement Similar as horizontal re nement, assume we have principle behaviour model P and a concrete process model Q, which is reduced w.r.t P to eliminate ungrounded activities. Any activity in Q can be grounded to some activity in P . Thus, after reduction, 8a 2 P; 9b 2 Q that b is grounded to a, and vice versa. Therefore for each xj 2 P , we de ne grounded xj 9groundedT o:xj.Then we construct an ontology OP !Q with following axioms: 1. for each activity a 2 Q and vert(a) = xj, a v 9groundedT o:xj These axioms represent the grounding of activities by concept subsumptions, which realise the Renaming in vertical re nement. For example, a11 v 9groundedT o:E, b11 v 9groundedT o:F . 2. for each a 2 P grounded a vPrfrom(P SP (a))[xj ! grounded xj], grounded a vPrto(SSP (a))[xj ! grounded xj], These axioms represent the predecessor and successor sets of all the activities in the pre-re nement process. Due the mechanism of Renaming we replace all the xj 2 P by grounded xj. Because Decomposition is not needed in vertical re nement, we stick to the original predecessor and successor sets. These axioms become the constraints on the activities in Q. For example, grounded E v 8f rom:Start, grounded E v 8to:(grounded F t End). 3. for each a 2 Q, a vPsfrom(P SQ(a)) and a vPsto(SSQ(a)),
These axioms represent the predecessor and successor sets of all the activities in the post-re nement process. For example, a11 v 9f rom:Start, a11 v 9to:b11 u 9to:End. Notice that the ungrounded activities such as a31 have been removed from the process so that End becomes a directed successor of a11 after reduction. 4. for each xj 2 P , Disjoint(aja 2 Q and vert(a) = xj)
These axioms represent the uniqueness of all the sibling activities re ned from the same xj. 5. Disjoint(all the grounded xj).
This axiom represents the uniqueness of all the activities before re nement. For example, Disjoint(Start; End; grounded E; grounded F ).
Both the horizontal and vertical re nement can be represented in DL in a linear complexity. The language is ALC. It's worth to mention that f rom and to do not need to be inverse roles because the unsatis ability of activities is caused by the contradiction of universal and existential restrictions.
With above axioms, ontology OP !Q is a representation of the re nement from P to Q by describing the predecessor and successor sets of corresponding activities with axioms. 3.3
Follow from the theorems and de nitions presented before, the relation between the ontology OP !Q and the validity of the re nement from P to Q is characterised by the following theorem: Theorem 3. The route contains activity a in Q is invalid in the re nement from P to Q, i OP !Q j= a v ?.
Proof. For each a in Q the ontology OP !Q contains the axioms a vPsfrom(P SQ(a)) and a vPsto(SSQ(a)). The axioms a vPrfrom(P SQ(a)) and a vPrto(SSQ(a)) are derived from the axioms (item 1,2). Depending on the re nement either the axioms a v 9groundedT o:xj and grounded xj 9groundedT o:xj or a v 9compose:zj and component zj 9compose:zj are in the ontology. (1) For the ! direction the lhs holds, we demonstrate that a is unsatis able. Since a is invalid either P SQ(a) 6 P SP (a) or SSQ(a) 6 SSP (a). From Theorem 3 it follows that either Prfrom(P SP (a))uPsfrom(P SQ(a)) or Prto(SSP (a))uPsto(SSQ(a)) is unsatis able and therefore a is unsatis able since a is subsumed. (2) The direction is proved by contraposition. Given a is unsatis able in OP !Q. Assumed a is valid in the re nement then P SQ(a) P SP (a) and SSQ(a) SSP (a) holds. From Theorem 3 the satis ability of Prto(SSP (a)), Prfrom(P SP (a)), Psfrom(P SQ(a)) and Psto(SSQ(a)) follows which leads to a contradiction to the satis ability of a.
This theorem has two implications: 1. The validity of a re nement can be checked by the satis ability of all the name concepts in an ontology; 2. The activities represented by unsatis able concepts in the ontology are the source of the invalid re nement.
The complexity of such concept satis ability checking is, according to the expressive power, ExpTime. we check the satis ability of the concepts to validate the process re nement. Every unsatis able concept is either an invalid re nement or relating to an invalid re nement.
For example, in the horizontal re nement ontology, a31 v 9compose:A, component A 9compose:A and component A v 8to:(component B t component A) implies that a31 v 8to:(component B t component A). However a31 v 9to:End, and Disjoint(End; component A; component B) indicates that a31 is unsatis able. Therefore the top route [a11; a31] in the speci c process model is invalid, so as the entire re nement.
While in the vertical re nement ontology, it's easy to infer that all the concepts are satis able. Therefore, the process model does comply to the principle behaviour models.
Helped by our analysis, the line of business manager and process architect remodel their processes (Fig. 3). Now, the execution set of Fig. 3a is f[AB]; [A]g. Renaming of Fig. 3b's execution set f[a1a2b1b2]; [a1a3]g yields f[AABB]; [AA]g. After decomposition, we conclude that Fig. 3b correctly re nes the process in Fig. 3a because f[AB]; [A]g f[AB]; [A]g. As for comparing with the component models, renaming yields f[EDFC]; [ED]g. After reduction with respect to C1 and C2, we conclude that Fig. 3b correctly grounds on C1 and C2 because f[C]; [D]; [CC]; [CD]; [DC]; [DD]; : : :g f[DC]; [D]g and f[EF]; [E]g f[EF]; [E]g. 4
Annotations to process models for service behaviour and interaction is described
in [
Other models use mathematical formalisms to describe and compare
concurrent system behaviour. In [
Calculus of communication systems and transition systems is used in other
works like in [
In [
The DL DLR is extended with temporal operators in [
In this paper, we have devised a method to checking process re nement w.r.t.
execution set semantics. We restricted our solution to a commonly used subset
of BPMN [
This work has been supported by the European Project Marrying Ontologies and Software Technologies (MOST ICT 2008-216691).