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 with respect to either an abstract model or a 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 can be validated by concept satis ability checking.
can be performed within 1s, which is signi cantly faster than manually consistency checking and the correctness of the validation is guaranteed.
The rest of the paper is organised as follows: in Sec.2 we de ne the problem of process re nement with its graphical syntax, semantics and mathematical foundation. The representation and validation of processes with the corresponding execution constraints is demonstrated in Sec.3. In Sec.4 we present the evaluations and in Sec.5 we review related works and conclude the paper. 2
In this section, we introduce preliminary knowledge about process models, process re nement w.r.t. execution set semantics and DL-based ontologies. Syntax of Process Models A process model|or short: process|is a nonsimple directed graph P = hE; Vi without multiple edges between two vertices. As a graphical representation, we use the business process modelling notation (BPMN: http://www.bpmn.org/) due to its wide industry adoption. However, we consider a normal form of process models for the sake of this paper as opposed to the full set of partly redundant constructs in BPMN.
In our de nition, vertices (V) include activities, gateways (A; G V), and the speci c vertices start and end event (v0; vend 2 V). Fig. 1a shows a BPMN diagram which consists of two activities between the start and end events.
!!
A gateway is either opening or closing (GO; GC G), and either exclusive or parallel (G ; G G). The process models (c) and (d) in Fig. 1 contain exclusive and parallel gateways, respectively. We call a process normal if it does not contain parallel gateways (G = ;)|as, for example, process model (c).
The edge set (E) is a binary relation on V. We de ne the predecessor and the successor functions of each v1 2 V as follows: pre(v1) := fv2 2 V j (v2; v1) 2 Eg, suc(v1) := fv3 2 V j (v1; v3) 2 Eg. The start (end) event has no predecessor (successor): jpre(v0)j = jsuc(vend)j = 0 and exactly one successor (predecessor): jsuc(v0)j = jpre(vend)j = 1. Each open gateway o 2 GO (close gateway c 2 GC) has exactly one predecessor (successor): jpre(o)j = jsuc(c)j = 1. Each activity a 2 A has exactly one predecessor and successor: jpre(a)j = jsuc(a)j = 1. We can then construct gateway-free predecessor and successor sets as follows: P S(v1) := fv2 2 A j v2 2 pre(v1) or 9u 2 G s:t: u 2 pre(v1) and v2 2 P S(u)g SS(v1) := fv3 2 A j v3 2 suc(v1) or 9u 2 G s:t: u 2 suc(v1) and v3 2 SS(u)g
These two de nitions make gateways \transparent" to ordering relations. For
example in Fig.1b, SS(a1) = fb1; a2g, in Fig.1c, P S(C) = fC; Dg.
Execution Set Semantics of Process Models We de ne the semantics of a
process model using the execution set semantics [
For example, ES1a for process (a) in Fig. 1 is f[AB]g: rst A, then B (for brevity, we refer to an activity by its short name, which appears in the diagrams in parenthesis). Process (b) contains parallel gateways ( ) to express that some activities can be performed in any order: ES1b = f[a1a2b1b2b3]; [a1b1a2b2b3]; [a1b1b2a2b3]g. Exclusive gateways ( ) are used in process (c) both to choose from the two activities and to form a loop: ES1c = f[C]; [D]; [CC]; [CD]; [DC]; [DD]; : : :g. Process (d) shows that gateways can also occur in a non-block-wise manner: ES1d = f[EFGH]; [EFHG]; [FHEG]; [FEGH]; [FEHG]g.
Correct Process Re nement For re nement validation we have to distinguish between horizontal and vertical re nement. A horizontal re nement is a transformation from an abstract to a more speci c model which contains the decomposition of activities. A vertical re nement is a transformation from a principle behaviour model of a component to a concrete process model for an application. The validation have to account for both re nements.
Fig. 1 shows a re nement horizontally from abstract to speci c while vertically complying with the components' principle behaviour. In our example scenario, Fig. 1a is drawn by a line of business manager to sketch a new hiring process. Fig. 1b is drawn by a process architect who incrementally implements the sketched process. Fig. 1c and d are the principle behaviour models of di erent components.
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) = A, hori(b1) = hori(b2) = hori(b3) = B. 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) = F, vert(b1) = G, vert(b2) = H, vert(b3) = D. 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[a1a2b1b2b3]; [a1b1a2b2b3]; [a1b1b2a2b3]g of Fig. 1b yields f[AABBB]; [ABABB]; [ABBAB]g. 2. Decomposition. Replace all sequences of equal activities by a single activity in each execution of ESQ. For Fig. 1b this yields f[AB]; [ABAB]g. As f[AB]g 6 f[AB]; [ABAB]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. 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[a1a2b1b2b3]; [a1b1a2b2b3]; [a1b1b2a2b3]g of Fig. 1b yields f[EFGHD]; [EGFHD]; [EGHFD]g. 2. Reduction. Remove all activities in each execution of ESQ that do not appear in P . For our example, reduction with respect to Fig. 1c yields f[D]g.
Reduction with respect to Fig. 1d yields f[EFGH]; [EGFH]; [EGHF]g. Fig. 1b is a correct vertical re nement of Fig. 1c because f[C]; [D]; [CC]; [CD]; [DC]; [DD]; : : :g f[D]g and a wrong vertical re nement of Fig. 1d because f[EFGH]; [EFHG]; [FHEG]; [FEGH]; [FEHG]g 6 f[EFGH]; [EGFH]; [EGHF]g. The cause for the wrong re nement is the potentially inverted execution of FG by b1a2 in Fig. 1b.
As enumerating the execution sets for validation is infeasible, our solution works with descriptions in ontology instead of using the execution sets themselves. Description Logics and Ontologies DL-based ontologies have been widely applied as knowledge formalism for the semantic web. An ontology usually consists of a terminology box (TBox) and an assertion box (ABox). In TBox the domain is described by concepts and roles with DL constructs. In this paper, we use DL ALC. Its concepts are inductively de ned by following constructs: >; ?; A; :C; C u D; C t D; 9r:C; 8r:D where > is the super concept of all concepts; ? means nothing; A is an atomic concept; C and D are general concepts and r is an atomic role. In DL, the subsumption between two concepts C and D is depicted as C v D. If two concepts mutually subsume each other, they are equivalent, depicted by C D. When a concept can not be instantiated in any model, i.e., C v ?, it is unsatis able. Two concepts are disjoint if C v :D. In this paper we write Disjoint(C1; C2; : : : ; Cn) to denote that all these concepts disjoint with one another. 3
In this section, we present our solution of validating process re nement in detail. We rst eliminate all the parallel gateways in a process, then translate such a process into ontologies based on the predecessor and successor sets of activities, nally we show that the re nement checking can be reduced to concept unsatis ability checking 3.1
As we can see from ES1c, the execution ordering relations between successors of some g 2 GO are implicit in the original process. For example, b1 and a2 does not have any explicit edge, the semantics of parallel gateway still implies that b1a2 or a2b1 must appear in some execution. In order to make such relations explicit, we eliminate all the parallel gateways while retain the execution set. Our strategy is to generate exclusive gateways to represent the executions.
Given a process P , its normal n(P ) can be obtained as follows: 1. Repeatedly replace each penning-parallel gateway g by an opening-exclusive gateway e. For each v 2 suc(e), construct a new penning-parallel gateway g0 with pre(g0) = v, suc(g0) = suc(v) [ suc(e) n fvg and then make suc(v) = g0. 2. Remove all the edges from an opening- to a closing-parallel gateway. 3. If an opening-gateway has only one successor, remove the gateway 4. If an closing-gateway has only one predecessor, remove the gateway
In step 1 direct successors of parallel gateways are \pulled" out of the gateway. Here a loop block is considered as a single successor. In this procedure, a parallel gateway with n successors is transformed into n parallel gateways with n successors but one of the successive sequence is shortened by one successor. Due to the nite length of these sequences, this replacement always terminates. Step 2 then reduces the number of successors for these remaining parallel gateways by removing \empty" edges. Step 3 and 4 nally remove the gateways. When a gateway is removed, its predecessors and successors should be directly connected.
It's obvious that this normalisation will always result in a normal process. An example of normalisation of Fig.1b and Fig.1d can be seen in Fig.2.
The size of n(P ) can be exponentially large w.r.t. P in worst case: suppose P contains only a pair of parallel gateways with n sequences of one activity, then n(P ) will contains a pair of exclusive gateways with n! sequences of n activities.
In normalisation, some activities will be duplicated in the process. These duplications have di erent predecessors (successors). We distinguish them by an additional numerical subscript. We depict such a transformed process n(P ) with distinguished activities by P ?. Obviously, ESP ? is the same as ESn(P ) after replacing all the distinguished activities by their original names. Thus, relation between two execution sets can be characterised by the following theorem: Theorem 1. Given two processes P = hEP ; VP i and Q = hEQ; VQi, ESQ ESP i 8ai 2 AQ? , there exists some aj 2 AP ? such that P SQ? (ai) P SP ? (aj ) and SSQ? (ai) SSP ? (aj ).
Proof. (1) For the ! direction the lhs ESQ ESP holds. We demonstrate the subsumption for P S. For an arbitrary activity ai 2 AQ? , the activity ai0 is the corresponding activity before normalisation (i.e. without additional subscripts). The activity aj0 is the originator or ground activity of ai0 in P after renaming and aj 2 AP ? is the the corresponding activity after normalization of P . From the prerequisite it directly follows that the predecessors of ai 2 AQ? are predecessors of aj in Q?. The subsumption of the successor set is demonstrated likewise. (2) To prove the other direction we assume that the rhs holds. Consider an execution s 2 ESQ we demonstrate that s 2 ESP . For each activity ai0 of an arbitrary execution s 2 ESQ the corresponding activity ai 2 AQ? is received after normalization. From the rhs it follows that there exists an activity aj 2 AP ? so that each predecessor of ai is also a predecessor of aj in P ? and likewise for the successors of ai. After activity renaming and demonstrating for all activities of each execution of ESQ the inclusion of the lhs follows.
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 its process model and the predecessor and successor sets: { 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 connect their predecessors and successors directly, the resulting ESQ0 will be the same as the reduced 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.
Theorem 1 shows that the subsumption of execution sets can be reduced to subsumption of predecessor and successor sets. Decomposition means, an activity x can go from not only predecessors of x, but also another appearance of x, and can go to not only successors of x, but also another appearance of x. Any sequence of x in the execution will be decomposed.
Thus, 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 a process P and obtain the predecessor and successor sets from P ?, then encode Renaming and Decomposition into ontology 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/successors relations are described by two roles from and to, respectively. On instance level, these two roles should be inverse role of each other. However this is not necessary in our solution. Composition of activities in horizontal re nement is described by role compose. Grounding of activities in vertical re nement is described by role groundedTo. To facilitate the ontology construction, four operators are de ned for pre- and post- re nement process: De nition 1. : Given S a predecessors or successors set, we de ne four operators for translations as follows:
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: Theorem 2. P SQ(a) P SP (a) i Disjoint(xjx 2 AP [ AQ) infers that Prfrom(P SP (a))uPsfrom(P SQ(a)) is satis able.
SSQ(a) SSP (a) i Disjoint(xjx 2 AP [ AQ) 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 the ! 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) The direction can be proved similarly by contraposition.
Now we can represent horizontal and vertical re nements by ontologies: Horizontal Re nement For conciseness of presentation, we always have a pre-re nement process P and a post-re nement process Q and we re ne one activity z of P in this step. z may have multiple appearances zj in P ?. For each zj we de ne component zj 9compose:zj . 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:
With the 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, suppose we have principle behaviour model P and a concrete process model Q, which has already been 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 AP ; 9b 2 AQ that b is grounded to a, and vice versa. Therefore for each xj 2 AP ? , we de ne grounded xj 9groundedT o:xj.Then we construct an ontology OP !Q with following axioms: 1. for each activity ai 2 AQ? and vert(a) = x ai v F 9groundedT o:xj These axioms represent the grounding of activities by concept subsumption, which realise the Renaming in vertical re nement. For example, a11 v 9groundedT o:E, b11 v 9groundedT o:F . 2. for each ai 2 AP ? grounded ai vPrfrom(P SP ? (ai))[xj ! grounded xj], grounded ai 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 AP ? 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?. 3. for each ai 2 AQ? , ai vPsfrom(P SQ? (ai)), ai vPsto(SSQ? (ai)), These axioms represent the predecessor and successor sets of all the activities in the post-re nement process. Notice that the ungrounded activities have been removed from the process. 4. for each x 2 AP ,
Disjoint(aijai 2 Q? and vert(a) = x) These axioms represent the uniqueness of all the sibling activities re ned from the same x. 5. Disjoint(Start; End; all the grounded xj).
This axiom represents the uniqueness of all the activities before re nement. For example, Disjoint(Start; End; grounded C; grounded D).
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.
In both horizontal and vertical re nement, the number of axioms are linear w.r.t. the size of P ? and Q?. The language is ALC. 3.3
In ontology OP !Q, all the activities in Q? satisfy the ordering relations in P ? by satisfying the universal restrictions and satisfy the ordering relations in Q? by satisfying existential restrictions. Given the uniqueness of concepts, the inconsistency between P ? and Q? will lead to unsatis ability of particular concepts. The relation between the ontology OP !Q and the validity of the re nement from P to Q is characterised by the following theorems: Theorem 3. An execution path containing activity a in Q is invalid in the re nement from P to Q, i there is some ai 2 Q? such that OP !Q j= ai 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 2 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 2 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.
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.
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 related to an invalid re nement.
With the help of reasoning, we can easily see that Fig.1b is an invalid horizontal re nement w.r.t. Fig.1a: a22 v 9f rom:b12, also a22 v 9compose:A thus a22 v 8f rom:(Start t component A). However, b12 disjoints with both Start and component A therefore a22 is unsatis able. Similarly, we can detect that b12, b23 and a23 are unsatis able. This implies the invalid routes in Fig.2a and further the invalid re nement of Fig.1b. Also, the vertical re nement w.r.t. Fig.1d is wrong while the vertical re nement w.r.t. Fig.1c is correct.
According to the underlying logic, reasoning complexity is ExpTime.
Helped by our analysis, the process architect remodels their process (Fig. 3). Now, the execution set of Fig. 3 is f[a1a2b1b2b3]; [a1a2b2b1b3]; [a1a2b1b3b2]g. Renaming of Fig. 3's execution set with respect to Fig. 1a yields f[AABBB]g. After decomposition, we conclude that Fig. 3 correctly horizontally re nes the process in Fig. 1a because f[AB]g f[AB]g. As for validating vertical re nement with the component models, renaming yields f[EFGHD]; [EFHGD]; [EFGDH]g. After reduction with respect to Fig. 1c and Fig. 1d, we conclude that Fig. 3 correctly grounds on Fig. 1c and Fig. 1d because f[C]; [D]; [CC]; [CD]; [DC]; [DD]; : : :g f[D]g and f[EFGH]; [EFHG]; [FHEG]; [FEGH]; [FEHG]g f[EFGH]; [EFHG]g. 4
We have implemented the transformation of BPMN process models and re nement information to OWL-DL ontology. In addition to the transformation, we implemented a generator which creates random, arbitrarily complex re nement scenarios. Flow correctness is ensured by constructing the process models out of block-wise patterns that can be nested. The generator is parameterized by !! the maximum branching factor B, the maximum length L of a pattern instance, the maximum depth of nesting N , and by the probability for loops, parallel, or exclusive ow. Most realistic appearing process diagrams were created with B = 3, L = 6, N = 3, and with a mixture of loops, parallelism, and exclusive ow to the ratio of 2 : 1 : 2.
With the given parameters, we generated 1239 re nement scenarios (197 correct, 1042 wrong) with the average and maximum number of activities in the generic and re ned models printed on the left-hand side below.
The generated scenarios were used to evaluate the re nement analysis on a laptop with a 2 GHz dual core CPU, 2 GB of RAM using Java v1.6 and Pellet 2.0.0. Two factors contribute to the overall complexity of the analysis: 1. Transformation to OWL-DL. As we pointed out earlier, theoretically, the complexity of the transformation can be exponential in the worst case. However, our experiments show that in many practical cases, the size of the OWL-DL knowledge base|measured by the number of axioms|remains relatively small. In particular, for 80% (90%) of the scenarios, the number of axioms was below 220 (400) (see Fig. 4). Some unusual nesting of parallel ow causes the exceptions in the diagram that have a higher number of generated axioms. Remarkably, the appearance of such cases seems to uniquely distribute over the scenarios independently of the size of the original processes due to the arti cial nature of the generated scenarios. 2. OWL-DL Reasoning. The theoretical complexity of OWL-DL reasoning is exponential as well. However, our evaluation runs in Fig. 5 suggest that for the practical cases evaluated, reasoning time grows less than exponentially (less than a straight line on a logarithmic scale) compared to the number of axioms in the OWL-DL knowledge base. We separately plot the reasoning times of the correct and wrong re nements because classifying a consistent knowledge base is more expensive in general.
When comparing absolute times, reasoning consumes about two orders of magnitude more time than transformation as can be seen from the right-hand # of Tasks 50 60 70 side of the table above. This determines our future research to seek improvements in the reasoning rather than in the transformation.
As for the complete run time, the above table indicates that the re nement analysis of an average scenario|with a generic process of about 6 activities and a re ning process of about 17 activities|would take about 3 seconds. We consider this a simpler, yet realistic problem size.
In one of the larger evaluated scenarios, 15 generic activities were re ned to 48 speci c activities (for comparison: our running example contains 5 speci c activities). The 63 activities in total (= 15+48) were transformed to 402 activities due to many parallel ows in that scenario. Analysis of the 765 generated axioms was performed in 18 seconds.
In the most complicated scenario of our evaluation, where a large knowledge base had to be constructed due to the heavy use of parallel gateways, total analysis time remained below 4 minutes. Although this is de nitely too much for providing a real-time re nement check to process modelers, analysis took less than 1 second for 80% ( 220 axioms) and less than 10 seconds for 90% ( 400 axioms) of the examined practical cases. Compared to the manual e orts a human is required today, our approach provides a signi cant improvement. Furthermore, the check performed by our approach is|in contrast to the manual approach|guaranteed to be correct and thus helps to avoid costly follow-up process design errors. 5
There are many existing works related to our study. Some of them [
Researchers in system transition and communication systems [
Other models use mathematical formalisms to describe concurrent system
behaviour. [
Semantic web community contribute to this topic by providing rst semantic
annotations for process models such as service behaviour and interaction [
In [
The DL DLR is extended with temporal operators in [
Our contribution is this paper includes: 1. Devising a general approach to represent and reason with process models containing parallel and exclusive gateways; 2. Applying graph-based topological approach with DL reasoning to provide automatic solution of process re nement checking; 3. Implementing and evaluating a prototype that performs process transformation and re nement checking as proposed.
In the future, there are several potential extension of this work. We will continue our implementation and evaluation to support larger and more complex process models. We will also try to extend the process representation with more expressive power. Another interesting topic is whether the process transformation itself can be automatically inferred by reasoning. We also want to integrate our re nement representation with other business process modelling ontologies.