=Paper=
{{Paper
|id=Vol-477/paper-35
|storemode=property
|title=Validating Process Refinement with Ontologies
|pdfUrl=https://ceur-ws.org/Vol-477/paper_59.pdf
|volume=Vol-477
|dblpUrl=https://dblp.org/rec/conf/dlog/RenGLRFZPS09
}}
==Validating Process Refinement with Ontologies==
https://ceur-ws.org/Vol-477/paper_59.pdf
Validating Process Refinement with Ontologies
Yuan Ren1 , Gerd Groener2 , Jens Lemcke3 , Tirdad Rahmani3 , Andreas Friesen3 ,
Yuting Zhao1 , Jeff Z. Pan1 and Steffen Staab2
1
University of Aberdeen, 2 University of Koblenz-Landau, 3 SAP AG
Abstract. A crucial task in process management is the validation of
process refinements. A process refinement is a process description in a
more fine-grained representation. The refinement is either with respect
to an abstract model or with respect to component’s principle behaviour
model. We define process refinement based on the execution set semantics.
Predecessor and successor relations of the activities are described in an
ontology in which the refinement is represented and validated by concept
satisfiability checking.
1 Introduction
The refinement of processes is a common task in process development. A generic
process describes the core functionality of an application. A refinement is a
transformation of a process into a more specific 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 refinement is valid, i.e.
the refined process refers to the intended behaviour of the abstract process.
We distinguish between horizontal and vertical refinement. A horizontal
refinement is a transformation from an abstract to a more specific model. A
vertical refinement is a transformation from a principle behaviour model of a
software component to a concrete process model of business. Once a refined
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 refinement steps. A refinement step includes customisation, extensions
and compositions of processes. Therefore it is quite difficult to validate the
refinement of a process with respect to an abstract process model.
The validation of a process refinement consists of checking model constraints
like execution order constraints. Modelling constraints for the refined process has
to cover the constraints of the generic process behaviour and also constraints
which emerged during the refinement steps.
In this paper, we use execution set semantics to analyse process refinements.
This set-based formalism accounts for a comparison of the process executions
of different processes. The comparison of process execution sets is then reduced
to the comparison of finite 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 refinement checking is reduced to concept
satisfiability checking.
In Section 2 we define the problem of process refinement 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 refinement validation.
2 Process Refinement
2.1 Execution Set Semantics
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 flow which consists of two activities between the Start
and End nodes; (b) shows the usage of exclusive gateway ( ) indicating that
the flow can go through one and only one of its branches, and parallel gateway
( ) indicating that the flow should go through all of its branches; (c) shows
the usage of a loop indicating that the flow 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 define the correctness of process refinement
based on the execution set semantics [14]. Briefly, the execution set of a process
P , denoted by ESP , is made up of all the valid paths between the Start and
the End in P . ESAbstract in Fig. 1a is {[AB]}: first A, then B. Any two branches
behind an exclusive gateway ( ) cannot occur together in the same path, thus
ESComponent2 is {[E], [EF]} (see Fig. 1d). When they are behind a parallel gateway
( ), any ordering between activities of the branches are valid, thus [a1 a2 b1 b2 ],
[a1 b1 a2 b2 ] and [a1 b1 b2 a2 ] ∈ ESSpecif ic (see Fig. 1b). The execution set of a process
containing a loop is infinite, e. g., ESComponent1 = {[C], [CDCD], . . .} (see Fig. 1c).
Consequently, enumerating the execution set is infeasible.
2.2 Process Refinement
Fig. 1 shows a refinement horizontally from abstract to specific 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 different components.
The challenge is to verify whether the refinement is consistent with the more
abstract horizontal and vertical processes.
1
http://www.bpmn.org/
Fig. 1. Wrong process refinement
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 refinement, we assume they are
always correct in this work.
Correct horizontal refinement. We say that a process Q is a correct horizontal
refinement of a process P if ESQ ⊆ ESP after the following transformations.
1. Renaming. Replace all activities in each execution of ESQ by their origi-
nators (function hori()). Renaming the execution set {[a1 a2 b1 b2 ], [a1 b1 b2 a2 ],
[a1 b1 a2 b2 ], [a1 a3 ]} of Fig. 1b yields {[AABB], [ABBA], [ABAB], [AA]}.
2. Decomposition. Replace all pairs of duplicate activities by a single activity
in each execution of ESQ . For Fig. 1b this yields {[AB], [ABA], [ABAB], [A]}.
As {[AB]} 6⊇ {[AB], [ABA], [ABAB], [A]}, Fig. 1b is a wrong horizontal refinement
of Fig. 1a. The cause is the potentially inverted order of AB by b1 a2 or b2 a2 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 refinement. We say that a process Q is a correct vertical
refinement 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 {[a1 a2 b1 b2 ], [a1 b1 b2 a2 ],
[a1 b1 a2 b2 ], [a1 a3 ]} of Fig. 1b yields {[EDFC], [EFCD], [EFDC], [ED]}.
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
{[DC], [CD], [D]}. Reduction with respect to Component 2 yields {[EF], [E]}.
As {[C], [D], [CC], [CD], [DC], [DD], . . .} ⊇ {[DC], [CD], [D]} and {[EF], [E]} ⊇ {[EF],
[E]}, Fig. 1b is a correct vertical refinement 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 Validation with Ontologies
In this section, we present our solution of validating process refinement with
ontologies in detail. We accomplish the transformations from the last section by
reductions on the process diagram and execution sets, represent the refinement
with an ontology, and validate the refinement by concept satisfiability checking.
3.1 Refinement reduction
Because the execution set may contain infinite number of executions, e.g.
EScomponent1 , it’s difficult to directly compare them. Therefore we reduce the
subsumption between infinitely large execution sets into subsumption between
finite 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 ESSpecif ic , the execution ordering relations between
branches of a parallel gateway are implicit in the original process. In order to
make them explicit, we first reduce a process diagram by the following operation:
A parallel gateway ([B1 |P1 ], . . . , [Bn |P n ]) is reduced to an exclusive gateway
B1 (P1 , [B2 |P2 ], . . . , [Bn |Pn ]) , . . . , Bn ([B1 |P1 ], . . . , [Bn−1 |Pn−1 ], Pn ) ,
where the notation [B|P ] 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 finite size of
the process. The resulting BPMN graph is called the Execution Diagram of P ,
denoted by EDP (see Fig. 2). An activity a ∈ P may have multiple appearance
in EDP . We use one more subscript j to differentiate them, i.e. a2 1, a2 2 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.
Fig. 2. Execution diagram for Fig. 1b
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 definition, for each x, y such that x ∈ P SP (aj ),
y ∈ 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 finite, P SP (aj ) and
SSP (aj ) are also finite for any aj ∈ P . Follow our example, P S(a31 ) = {a11 }
and SS(a31 ) = {End}.
By obtaining these two sets for all the activities, the relation between two
execution sets can be characterised by the following theorem:
Theorem 1. ESQ ⊆ ESP iff ∀a ∈ Q, P SQ (a) ⊆ P SP (a) and SSQ (a) ⊆
SSP (a).
Proof. (1) For the → direction the lhs ESQ ⊆ ESP holds. Given a ∈ Q and
b ∈ P SQ (a), we demonstrate that b ∈ P SP (a) holds: [b, a] is a subpath of some
X ∈ ESQ , from precondition it follows [b, a] is a subpath of X ∈ ESP and the
definition of P S leads to b ∈ P SP (a). Correspondingly for c ∈ SSQ (a), it follows
from definition [a, c] is a subpath of some Y ∈ ESQ and from precondition follows
[a, c] is a subpath of Y ∈ ESP . The definition of SS leads to c ∈ SSP (a).
(2) For the ← direction the rhs holds and we demonstrate that ESQ ⊆ ESP fol-
lows. Consider an execution s ∈ 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 ∈ ESP . For i = 1, . . . , n − 1 the following im-
plication holds: SSQ (ai ) ⊆ SSP (ai ) ⇒ [ai , ai+1 ] is a subpath of some Y ∈ ESP ,
therefore sequentially connect the subpathes [a1 , . . . , an ] ∈ ESP holds.
Therefore, we reduce the process refinement w.r.t. execution set semantics
into the subsumption checking of finite 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 effect 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, iff ∀a 6= x, P SQ (a) ⊆ P SP (a),
SSQ (a) ⊆ SSP (a) and ∀x, P SQ (x) ∪ {x} ⊆ P SP (x) and SSQ (x) ∪ {x} ⊆
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 refinement, we can first 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 refinement, we can first perform the Reduction on processes,
then obtain the predecessor and successor sets and perform the Renaming
on these sets, and finally 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 Refinement representation
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 refinement is described by
role compose. Grounding of activities in vertical refinement is described by role
groundedTo. The last two don’t have essential logic difference in the problem of
process refinement but have different semantics in the process model, so that we
distinguish between them. Then, for a set S containing predecessors or successors,
we define four operators for translations as follows:
Definition 1. : F
Pre-refinement-from operator Prf rom (S) =F∀f rom. x∈S x
Pre-refinement-to operator Prto (S) = ∀to. y∈S
d y
Post-refinement-from operator Psf rom (S)
d = x∈S ∃f rom.x
Post-refinement-to operator Psto (S) = y∈S ∃to.y
The effect of the above operators in refinement checking can be characterised
by the following theorem:
Theorem 2. P SQ (a) ⊆ P SP (a) iff
Disjoint(x|x ∈ P ∪ Q) infers that Prf rom (P SP (a))uPsf rom (P SQ (a)) is satisfi-
able.
SSQ (a) ⊆ SSP (a) iff
Disjoint(x|x ∈ P ∪ Q) infers that Prto (SSP (a))uPsto (SSQ (a)) is satisfiable.
For sake of a shorter presentation, we only prove the first part of the theorem.
The proof for the second part is appropriate to the first part.
Proof. (1) We demonstrate → direction with a proof by contraposition.
The disjointness of activities holds. Supposed the rhs is unsatisfiable, i.e.
Prf rom (P SP (a))uPsf rom (P SQ (a)) is unsatisfiable. Obviously, both concept def-
initions on its own are satisfiable, since Prf rom (P SP (a)) is just a definition with
one all-quantified role followed by a unionFof (disjoint) concepts. The concept
definition behind this expression is ∀f rom. x∈P SP (a) x which restricts the range
of f rom to all concepts (activities) of P SP (a). Psf rom (P SQ (a)) is a concept
intersection which only consists of existential quantifiers and the same f rom
role. This definition is also satisfiable. Therefore the unsatisfiability is caused by
the intersection of both definitions. In Psf rom (P SQ (a)) the same role f rom is
used and the range is restricted by Prf rom (P SP (a)). Therefore the contradiction
is caused by one activity b ∈ 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(x|x ∈ P ∪ Q) infers that Prf rom (P SP (a))uPsf rom (P SQ (a)) is satisfi-
able. For each activity b ∈ P SQ (a) we show that b is also in P SP (a): b ∈ P SQ (a)
and Psf rom (P SQ (a)) is satisfiable, the intersection contains the term ∃f rom.b.
Since Prf rom (P SP (a)) is satisfiable and is also the range restriction of f rom, it
follows that b ∈ P SP (a).
This theorem indicates that the refinement checking of processes can be
reduced to the satisfiability checking of concepts in an ontology. In the following,
we present the representation of horizontal refinement and vertical refinement.
Horizontal Refinement For conciseness of presentation, we always have a
pre-refinement process and a post-refinement process and we refine one activ-
ity in each step (this activity may have multiple appearance after conversion
to the execution diagram). We assume P the pre-refinement process, Q the
post-refinement process and z the activity being refined. For each zj we define
component zj ≡ ∃compose.zj . The simultaneous refinement of multiple activities
can be done in a similar manner of single refinement. Then we construct an
ontology OP →Q with following axioms:
1. for each activity a ∈ Q and hori(a) = zj , a v ∃compose.zj
These axioms represent the composition of activities with concept sub-
sumptions, which realise Renaming in horizontal refinement. For example,
b11 v ∃compose.B and a31 v ∃compose.A.
2. for each a ∈ Q and a is not refined from any zj
a vPrf rom (P SP (a))[zj → component zj ],
a vPrto (SSP (a))[zj → componennt zj ],
These axioms represent the predecessor and successor sets of all the unre-
fined activities in the pre-refinement process. Because in the post-refinement
process, any activity refined 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 ∀to.component A.
3. for each zj ∈ P ,
component zj vPrf rom (P SP (zj ) ∪ {component zj })[zj → componennt zj ],
component zj vPrto (SSP (zj ) ∪ {component zj })[zj → componennt zj ],
These axioms represent the predecessor and successor sets of all the refined
activities in the pre-refinement process. Due to the mechanism of Decom-
posing, 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 ∀f rom.(Start t component A),
component A v ∀to.(component B t component A), component B v
∀f rom.(component A t component B) and component B v ∀to.(End u
component B).
4. for each a ∈ Q, a vPsf rom (P SQ (a)) and a vPsto (SSQ (a)),
These axioms represent the predecessor and successor sets of all the activities
in the post-refinement process. For example, a31 v ∃to.End, b11 v ∃to.a21 u
∃to.b22
5. for each zj ∈ P , Disjoint(a|a ∈ Q and Hori(a) = zj )
These axioms represent the uniqueness of all the sibling activities refined
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 refinement.
For example, Disjoint(Start, End, A, B, component A, component B).
With above axioms, ontology OP →Q is a representation of the horizontal
refinement from P to Q by describing the predecessor and successor sets of
corresponding activities with axioms.
Vertical Refinement Similar as horizontal refinement, 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, ∀a ∈ P, ∃b ∈ Q that b is grounded
to a, and vice versa. Therefore for each xj ∈ P , we define grounded xj ≡
∃groundedT o.xj .Then we construct an ontology OP →Q with following axioms:
1. for each activity a ∈ Q and vert(a) = xj , a v ∃groundedT o.xj
These axioms represent the grounding of activities by concept subsumptions,
which realise the Renaming in vertical refinement. For example, a11 v
∃groundedT o.E, b11 v ∃groundedT o.F .
2. for each a ∈ P
grounded a vPrf rom (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-refinement process. Due the mechanism of Renaming we replace
all the xj ∈ P by grounded xj . Because Decomposition is not needed in
vertical refinement, we stick to the original predecessor and successor sets.
These axioms become the constraints on the activities in Q. For example,
grounded E v ∀f rom.Start, grounded E v ∀to.(grounded F t End).
3. for each a ∈ Q, a vPsf rom (P SQ (a)) and a vPsto (SSQ (a)),
These axioms represent the predecessor and successor sets of all the activities
in the post-refinement process. For example, a11 v ∃f rom.Start, a11 v
∃to.b11 u ∃to.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 ∈ P , Disjoint(a|a ∈ Q and vert(a) = xj )
These axioms represent the uniqueness of all the sibling activities refined
from the same xj .
5. Disjoint(all the grounded xj ).
This axiom represents the uniqueness of all the activities before refinement.
For example, Disjoint(Start, End, grounded E, grounded F ).
Both the horizontal and vertical refinement 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 unsatisfiability of activities is caused
by the contradiction of universal and existential restrictions.
With above axioms, ontology OP →Q is a representation of the refinement
from P to Q by describing the predecessor and successor sets of corresponding
activities with axioms.
3.3 Concept satisfiability checking
Follow from the theorems and definitions presented before, the relation between
the ontology OP →Q and the validity of the refinement from P to Q is characterised
by the following theorem:
Theorem 3. The route contains activity a in Q is invalid in the refinement
from P to Q, iff OP →Q |= a v ⊥.
Proof. For each a in Q the ontology OP →Q contains the axioms
a vPsf rom (P SQ (a)) and a vPsto (SSQ (a)). The axioms a vPrf rom (P SQ (a))
and a vPrto (SSQ (a)) are derived from the axioms (item 1,2). Depending on
the refinement either the axioms a v ∃groundedT o.xj and grounded xj ≡
∃groundedT o.xj or a v ∃compose.zj and component zj ≡ ∃compose.zj are in
the ontology. (1) For the → direction the lhs holds, we demonstrate that a is
unsatisfiable. 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 Prf rom (P SP (a))uPsf rom (P SQ (a)) or
Prto (SSP (a))uPsto (SSQ (a)) is unsatisfiable and therefore a is unsatisfiable since
a is subsumed. (2) The ← direction is proved by contraposition. Given a is unsat-
isfiable in OP →Q . Assumed a is valid in the refinement then P SQ (a) ⊆ P SP (a)
and SSQ (a) ⊆ SSP (a) holds. From Theorem 3 the satisfiability of Prto (SSP (a)),
Prf rom (P SP (a)), Psf rom (P SQ (a)) and Psto (SSQ (a)) follows which leads to a
contradiction to the satisfiability of a.
This theorem has two implications:
1. The validity of a refinement can be checked by the satisfiability of all the
name concepts in an ontology;
2. The activities represented by unsatisfiable concepts in the ontology are the
source of the invalid refinement.
The complexity of such concept satisfiability checking is, according to the
expressive power, ExpTime. we check the satisfiability of the concepts to validate
the process refinement. Every unsatisfiable concept is either an invalid refinement
or relating to an invalid refinement.
For example, in the horizontal refinement ontology, a31 v ∃compose.A,
component A ≡ ∃compose.A and component A v ∀to.(component B t
component A) implies that a31 v ∀to.(component B t component A). However
a31 v ∃to.End, and Disjoint(End, component A, component B) indicates that
a31 is unsatisfiable. Therefore the top route [a11, a31] in the specific process
model is invalid, so as the entire refinement.
While in the vertical refinement ontology, it’s easy to infer that all the
concepts are satisfiable. 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 {[AB], [A]}.
Renaming of Fig. 3b’s execution set {[a1 a2 b1 b2 ], [a1 a3 ]} yields {[AABB], [AA]}.
After decomposition, we conclude that Fig. 3b correctly refines the process in
Fig. 3a because {[AB], [A]} ⊇ {[AB], [A]}. As for comparing with the component
models, renaming yields {[EDFC], [ED]}. After reduction with respect to C1 and
C2 , we conclude that Fig. 3b correctly grounds on C1 and C2 because {[C], [D],
[CC], [CD], [DC], [DD], . . .} ⊇ {[DC], [D]} and {[EF], [E]} ⊇ {[EF], [E]}.
4 Related Works and Conclusion
Annotations to process models for service behaviour and interaction is described
in [4, 12, 11]. However, process refinement and model validation is not considered.
Fig. 3. Correct process refinement
Other models use mathematical formalisms to describe and compare concur-
rent system behaviour. In [3] a process algebra is described in order to analyse
equivalence. The analysed equivalence (trace equivalence) does not distinguish
between deterministic and non-deterministic choices. Semantics for BPMN mod-
els in process algebra and process refinements are outlined in [13]. The refinement
is validated with model checker.
Calculus of communication systems and transition systems is used in other
works like in [7, 8]. The π-calculus is a first order calculus for concurrent systems.
The bisimulation (equivalence relationship between transition systems) for the
π-calculus is described in [9] and in [10] higher-order process calculus is used
to analyse bisimulation. Some of these approaches also apply the execution set
semantics from [14], but without refinement validation.
In [5] actions and services are described in DL. Actions contain pre- and
post-conditions. As inference problems, the realizability of a service, subsumption
relation between services and service effect checking is analysed. Services are
also described with DL in [2]. The reasoning tasks are checking of pre- and
post-conditions. The focus of this work is the reasoning complexity.
The DL DLR is extended with temporal operators in [1]. Based on this
extension, query containment for specified (temporal) properties is analysed. In
[6] the DL ALC is extended with the temporal logics LTL and CTL. Still, neither
of them considers process modelling and refinements.
In this paper, we have devised a method to checking process refinement w.r.t.
execution set semantics. We restricted our solution to a commonly used subset
of BPMN [15], which we may extend in the future. We perform a topological
transformation of process models and translate them into ALC ontologies. The
refinement checking can be reduced to concept unsatisfiability checking. In the
future, we will implement and evaluate our approach, and extend it to deal with
more constraints.
Acknowledgements
This work has been supported by the European Project Marrying Ontologies
and Software Technologies (MOST ICT 2008-216691).
References
1. A. Artale, E. Franconi, F. Wolter, and M. Zakharyaschev. A Temporal Description
Logic for Reasoning over Conceptual Schemas and Queries. Lecture notes in
computer science, pages 98–110, 2002.
2. F. Baader, C. Lutz, M. Milicic, U. Sattler, and F. Wolter. A Description Logic
Based Approach to Reasoning about Web Services. In Proceedings of the WWW
2005 Workshop on Web Service Semantics (WSS2005), Chiba City, Japan, 2005.
3. A.J. Cowie. The Modelling of Temporal Properties in a Process Algebra Framework.
PhD thesis, University of South Australia, 1999.
4. Markus Fronk and Jens Lemcke. Expressing semantic Web service behavior with
description logics. In Semantics for Business Process Management Workshop at
ESWC, 2006.
5. C. Lutz and U. Sattler. A Proposal for Describing Services with DLs. In Proceedings
of the 2002 International Workshop on Description Logics, 2002.
6. C. Lutz, F. Wolter, and M. Zakharyaschev. Temporal description logics: A survey.
In Temporal Representation and Reasoning, 2008. TIME’08. 15th International
Symposium on, pages 3–14, 2008.
7. R. Milner. A Calculus of Communicating Systems. Springer LNCS, 1980.
8. R. Milner. Communication and Concurrency. Prentice Hall, 1989.
9. R. Milner, J. Parrow, and D. Walker. A Calculus of Mobile Processes. Information
and Computation, pages 41–77, 1992.
10. Davide Sangiorgi. Bisimulation for Higher-Order Process Calculi. Information and
Computation, 131:141–178, 1996.
11. I. Weber, J. Hoffmann, and J. Mendling. Semantic Business Process Validation. In
Proc. of International workshop on Semantic Business Process Management, 2008.
12. I. Weber, Joerg Hoffmann, and Jan Mendling. Beyond Soundness: On the Cor-
rectness of Executable Process Models. In Proc. of European Conference on Web
Services (ECOWS), 2008.
13. P.Y.H. Wong and J. Gibbons. A process-algebraic approach to workflow specification
and refinement. Lecture Notes in Computer Science, 4829:51, 2007.
14. George M. Wyner and Jintae Lee. Defining specialization for process models. In
Organizing Business Knowledge: The MIT Process Handbook, chapter 5, pages
131–174. MIT Press, 2003.
15. Michael zur Muehlen and Jan Recker. How much language is enough? Theoretical
and practical use of the Business Process Modeling Notation. In Zohra Bellahsene
and Michel Léonard, editors, CAiSE, volume 5074 of Lecture Notes in Computer
Science, pages 465–479. Springer, 2008.