Diagnosing Co ec ness o Seman ic Wo k low Models
Diana Bo egoa,∗, Rik Eshuisb, Ma ´ıa Te esa G´omez-L´opeza, Ra ael M.
Gascaa
aUni e si y o Se ille, Depa men o Compu e Languages and Sys ems, A Reina
Me cedes S/N, 41012 Se ille, Spain
bEindho en Uni e si y o Technology, School o Indus ial Enginee ing, P.O. Box 513,
5600 MB Eindho en, The Ne he lands
Abs ac
To model ope a ional business p ocesses in an accu a e way, wo k low models
need o e e ence bo h he con ol low and da a low pe spec i es. Checking
he co ec ness o such wo k low models and gi ing p ecise eedback in case
o e o s is challenging due o he in e play be ween hese di e en pe spec-
i es. In his pape , we p opose a ully au oma ed app oach o diagnosing
co ec ness o seman ic wo k low models in which he seman ics o ac i i ies
a e speci ied wi h p e and pos condi ions. The con ol low and da a low
pe spec i es o a seman ic wo k low a e modeled in an in eg a ed way us-
ing A i icial In elligence echniques (In ege P og amming and Cons ain
P og amming). The app oach has been implemen ed in he DiagFlow ool,
which eads and diagnoses anno a ed XPDL models, using a s a e-o - he-a
cons ain sol e as back end. Using his no el app oach, complex seman ic
wo k low models can be e i ied and diagnosed in an e icien way.
Keywo ds: wo k low, business p ocess managemen , diagnosis, cons ain
p og amming, in ege p og amming
1. In oduc ion
Nowadays, o ganiza ions au oma e hei business p ocesses wi h wo k low
models ha can be enac ed using wo k low managemen sys ems (WFMSs).
∗Co esponding au ho . Tel. +34 954 556 234. Fax. +34 954 557 139
Email add esses: [email p o ec ed] (Diana Bo ego), [email p o ec ed] (Rik Eshuis),
[email p o ec ed] (Ma ´ıa Te esa G´omez-L´opez), [email p o ec ed] (Ra ael M. Gasca)
P ep in submi ed o Da a and Knowledge Enginee ing Ma ch 1, 2013
Fo o ganiza ions i is essen ial o ensu e he co ec ope a ion o wo k low
models a design ime, be o e he wo k low models ge enac ed. An inco -
ec ope a ional wo k low can dissa is y cus ome s and ixing he e o s can
be e y cos ly, ce ainly compa ed o he cos s o ixing he wo k low model
be o e i is deployed. Co ec ness o a wo k low model can be e i ied by
exhaus i ely checking all possible execu ions. De ec ed e o s should be di-
agnosed, o ins ance by p o iding an e o pa h ha shows he cause o he
e o , such ha e o s can be epai ed in a quick and e ec i e way [1].
Wo k low models can e e ence di e en pe spec i es [2]. Mos wo k low
modeling and e i ica ion app oaches only conside he con ol low pe spec-
i e [1, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13], which is abou he o de in which
he indi idual ac i i ies o a business p ocess a e execu ed. Ano he ele an
pe spec i e is he da a low pe spec i e [14], which de ails he low o da a
among ac i i ies subjec o ce ain cons ain s. The da a low pe spec i e is
impo an because da a cons ain s in luence he possible execu ions o ac-
i i ies [14] and in u n, he execu ion o ac i i ies esul s in ce ain da a
cons ain s being en o ced.
An e ec i e means o exp ess da a cons ain s is o anno a e ac i i ies
in a wo k low model wi h p e and pos condi ions ha speci y he e ec on
he da a s a e o each ac i i y. Fo ins ance, in he Sa banes-Oxley Ac
o 2002, he in e nal audi depa men akes he lead and wo ks alongside
wo k low owne s o each p ocess ha has a di ec e ec on he da a o he
inancial epo ing. Anno a ing ac i i ies inside hese p ocesses wi h p e and
pos condi ions acili a es compliance checking o ensu e ha wo k lows a e
p ope ly designed.
Only ecen ly, app oaches o e i ying wo k low models wi h da a lows
ha e been p oposed [14, 15, 16, 17, 18]. Howe e , hese app oaches do no
conside diagnosis o da a low e o s. Diagnosing da a low e o s is complex
due o he in e play be ween con ol low and da a low dependencies, as we
explain in Sec ion 2 wi h an example.
The goal o his pape is o de elop an app oach o diagnosing he co -
ec ness o seman ic wo k low models, con aining ac i i ies whose e ec s a e
o mally speci ied using p e and pos condi ions. An ac i i y can s a i he
execu ion o he wo k low model has eached he ac i i y and i s p econdi-
ion is sa is ied. Upon comple ion, he ac i i y deli e s da a ha sa is ies
i s pos condi ion. An execu ion o he wo k low can each an ac i i y whose
p econdi ion is no sa is ied. In ha case he execu ion ge s s uck a he
ac i i y and ails.
2
We dis inguish be ween wo di e en no ions o co ec ness o diagnose
such da a low e o s:
•May-co ec ness. A wo k low model is may-co ec i e e y ac i i y can
be execu ed a leas once, so he e is an execu ion in which he ac i i y
is done.
•Mus -co ec ness. A wo k low model is mus -co ec i e e y possible
execu ion ha eaches an ac i i y sa is ies he p econdi ion o he ac-
i i y.
The diagnosis is pe o med a design- ime, using A i icial In elligence
echniques o compu e he execu ion ins ances allowed by a wo k low model.
Fo diagnosis, he wo k low model is ansla ed in o wo models: (1) an
In ege P og amming model (IP model), o de e mine he di e en ins ances
o execu ion o he wo k low, and (2) he p econdi ions and pos condi ions o
he ac i i ies a e modeled as cons ain s in a Cons ain Sa is ac ion P oblem
(CSP) [19], ollowing a BNF g amma in o de o a oid any ambigui y.
This pape makes se e al con ibu ions:
•Wo k low da a g aphs a e p oposed as a o malism o modeling se-
man ic wo k lows wi h p e and pos condi ions o he ac i i ies. These
condi ions a e modeled as cons ain s acco ding o a well-de ined g am-
ma in BNF.
•Two co ec ness no ions o wo k low da a g aphs, may and mus -
co ec ness, a e p oposed and no el diagnosis algo i hms a e de eloped
o e i ying may and mus -co ec ness. The algo i hms a e comple e:
nei he alse posi i es no alse nega i es a e gene a ed. Mo eo e , he
algo i hms o e p ecise diagnosis o he de ec ed e o s, indica ing he
execu ion causing he e o whe e he wo k low ge s s uck.
•The app oach has been implemen ed in he DiagFlow ool, p esen ed
in [1]. The ool eads XPDL models [20] in which he seman ics o
ac i i ies and he co esponding da a low a e speci ied using ex ended
a ibu es.
This pape is o ganized as ollows. Sec ion 2 p esen s a mo i a ing ex-
ample o illus a e he concep s o may and mus -co ec ness. Sec ion 3
3
in oduces wo k low da a g aphs as a o mal model o seman ic wo k lows
and de ines may and mus -co ec ness on wo k low da a g aphs. Sec ion 4
de ines he IP and CSP o mula ions o a wo k low da a g aph. The p ocess
o diagnosis is explained, and wo algo i hms a e p esen ed. The diagnosis
o he mo i a ing example is pe o med. Sec ion 5 gi es implemen a ion de-
ails. Sec ion 6 shows expe imen al esul s. Sec ion 7 p esen s an o e iew
o ela ed wo k ound in he li e a u e. And inally, conclusions a e d awn
and u u e wo k is p oposed in Sec ion 8.
2. A Mo i a ing Example
This sec ion in oduces an example o a seman ic wo k low model, shown
in Figu e 1. This example desc ibes he handling o a con e ence o an
o ganizing commi ee, and i is used o illus a e he concep s o may and
mus -co ec ness in seman ic wo k low models. We use BPMN 2.0 [21] o
isualize wo k low models.
Figu e 1: Mo i a ing Example
Figu e 1 shows a wo k low ha consis s o nine ac i i ies ( ec angles wi h
ounded co ne s) and eigh ga eways o con ol nodes (diamonds), and a s a
and end e en (ci cles). A ga eway wi h one incoming edge and mul iple
ou going edges is called a spli ; a ga eway wi h mul iple incoming edges
and one ou going edge is a join. Ga eways wi h he +-symbol a e AND: all
incoming edges a e equi ed o pass he ga eway, and he ga eway ac i a es
all ou going edges. The o he ga eways a e XOR: one incoming edge can
pass he ga eway and one o he ou going edges is ac i a ed as a esul . In
he igu e, he ac i i y labels a e abb e ia ions o ac i i y names ha a e
lis ed in Table 1. The wo k low pe o ms he ollowing s eps:
1. The wo k low s a s wi h he es ablishmen o he con e ence a e (ECR
ac i i y), in o de o begin he egis a ion pe iod.
4
Table 1: Ac i i ies o he example
Abb e ia ion Ac i i y
ECR Es ablishmen o Con e ence Ra e
SAP Selec ion o Accep ed Pape s
D Dinne
L Lunch
OS O he expenses + Social e en
O O he expenses
R Regis a ion
IGS In e na ional Gues Speake
NGS Na ional Gues Speake
2. In he ac i i y SAP, he p ocess o accep ance o pape s o he con e -
ence akes place. The numbe o inal pape s is de e mined.
3. The wo k low is spli in o wo b anches. In he uppe one, he cos
o he gala dinne (D) and he lunches (L) o se e du ing he con e -
ence a e calcula ed concu en ly. On he lowe b anch, he wo k low
is ou ed acco ding o he money spen in he social e en s du ing he
con e ence (O o OS ac i i ies).
4. Nex , he egis a ion o he a endees o he con e ence akes place
(R).
5. And inally, he wo k low is ou ed depending on he a ailable money
o spend in he in i a ion o na ional o in e na ional gues speake s
(NGS o IGS).
The ac i i ies in he example consume and p oduce da a du ing he ex-
ecu ion o he wo k low by eading and w i ing a iables. Those a iables
a e lis ed in Table 2 wi h hei co esponding domains and meanings. Ta-
ble 3 shows how hese a iables a e used by he ac i i ies o he example,
indica ing i hey a e ead ( d) o w i en (w ).
Each ac i i y in a wo k low uses wo ypes o condi ion o e he da a low
which mus be sa is ied. A p econdi ion mus be sa is ied p io o execu ion
o he ac i i y. I no , he wo k low ge s s uck a he ac i i y and ails. A
pos condi ion is sa is ied immedia ely a e he ac i i y has inished. The
p econdi ions and pos condi ions o he ac i i ies in he example in Figu e 1
5

Table 2: Da a inpu o he example in Figu e 1
Va iable Domain Meaning
egFee {200..390}Con e ence egis a ion ee
sponso ship {0..15000}Ex e nal con ibu ions o suppo he e en
numPape s {50..80}Numbe o accep ed pape s
dinne {60..100}Gala dinne cos
lunch {10..30}Cos o each lunch se ed du ing he con e ence
o he s {30..185}Money o o he expenses, like social e en s
con A {75..170}Numbe o con e ence a endees
gues Speake {0..10000}Money o spend in in i ing a gues speake
a e shown in Table 4. The no a ion is explained in he nex sec ion.
I is easy o check ha he wo k low is co ec om he con ol low
pe spec i e: each ac i i y can be pe o med and he e a e no deadlocks, so
he wo k low can always comple e. To assess he co ec ness o he example
om he da a low pe spec i e, he e a e wo impo an ypes o ques ions.
Bo h ques ions es whe he he p econdi ion o an ac i i y acan be sa is ied
by conside ing an a bi a y pa ial execu ion o he wo k low in which ais
o be execu ed nex . The pa ial execu ion o he wo k low esul s in a da a
s a e (assignmen o alues o a iables) ha has o sa is y he p econdi ion
o a.
One ques ion is whe he o each ac i i y a he e exis s a leas one pa ial
execu ion o he wo k low in which acan be done nex and he esul ing
da a s a e sa is ies he p econdi ion o a. In ha case, ac i i y acan become
enabled and execu ed. O he wise, he execu ion o he wo k low may ge
s uck a a, i he cu en da a s a e does no sa is y he p econdi ion o a. I
e e y ac i i y can be execu ed, he wo k low is may-co ec .
The o he ele an ques ion is whe he e e y possible pa ial execu ion
o he wo k low esul s in a da a s a e ha sa is ies he p econdi ion o he
ac i i y o be execu ed nex . Ph ased di e en ly, can e e y possible pa ial
execu ion always be con inued such ha e en ually he end s a e is eached?
I he answe is posi i e, he wo k low is mus -co ec .
No e ha mus -co ec ness is s onge han may-co ec ness. I is s aigh -
o wa d o check ha i a wo k low is mus -co ec , i is also may-co ec .
6
Table 3: Da a ead and w i en on each ac i i y
Ac i i ies
Va iables ECR SAP D L OS O R IGS NGS
egFee w - d d d d d d d
sponso ship w - d d d d - d d
numPape s - w d d d d d - -
dinne - - w - - - d d d
lunch - - - w - - d d d
o he s - - - - w w d d d
con A - - - - - - w d d
gues Speake - - - - - - - w w
May-co ec ness can be used as sani y check o each ac i i y o see whe he
i s p econdi ion is no oo s ic . Mus -co ec ness can be used o check he
co ec ness o he en i e wo k low wi h all he ac i i ies.
In he case o he example in Figu e 1, he wo k low is may-co ec since
e e y ac i i y is execu able. On he o he hand, i is no mus -co ec : o
example, i he pa ial execu ion con ains ac i i ies ECR,SAP,D,L, and OS
hen he esul ing da a s a e can assign he ollowing alues o he a iables:
egFee=200, dinne =100, lunch=30, o he s=30. Bu now he ac i i y o be
execu ed nex , R, has a p econdi ion ha is alse, since 3∗30+100+30 ≮200.
The e o e, wi h ha assignmen o he a iables, he wo k low ge s s uck a
ac i i y R.
No e ha all ac i i ies ha e co ec p e and pos condi ions, and ha he
wo k low model has a co ec con ol low de ini ion: no deadlock occu s i
he da a low (p e and pos condi ions) is abs ac ed om. The e o is caused
by he in e play be ween he con ol low, which speci ies ha ECR,SAP,
D,L, and OS a e pe o med be o e R, and he da a low as speci ied by he
p e and pos condi ion o each ac i i y, which de e mines he possible da a
s a es jus be o e R.
The e o can be epai ed in se e al ways, o ins ance by elaxing he
p econdi ion o R, by s eng hening he pos condi ions o D,Land OS, o
by ea anging he con ol low. So inding an e o a a p econdi ion does
no necessa ily imply he p econdi ion i sel is lawed.
7
Table 4: Ac i i ies wi h hei p e and pos condi ions
Ac i i y P econdi ion and Pos condi ion
ECR p e: ue
pos : ue
SAP p e: ue
pos : ue
Dp e: sponso ship > 0∨numP ape s > 60
pos : egFee ∗0.1≤dinne ∧dinne ≤ egFee ∗0.35
Lp e: sponso ship > 0∨numP ape s > 60
pos : egFee ∗0.1≤3∗lunch ∧3∗lunch ≤ egF ee ∗0.35
OS p e: sponso ship > 0∨numP ape s > 60
pos : o he s ≤0.2∗ egF ee + 0.05 ∗sponso ship ∧
o he s ≥0.05 ∗ egFee + 0.05 ∗sponso ship
Op e: sponso ship > 0∨numP ape s > 60
pos : o he s ≤0.25 ∗ egF ee ∧o he s ≥0.05 ∗ egFee
Rp e: 3∗lunch +dinne +o he s < egF ee
pos : numPape s ∗1.8≥con A
∧numPape s ∗0.5≤con A
NGS p e: con A ∗(3 ∗lunch +dinne +o he s)<
con A ∗ egF ee +sponso ship
pos : gues Speake ≥0.2∗sponso ship ∧
gues Speake ≤sponso ship + 0.1∗ egFee ∗con A
IGS p e: con A ∗(3 ∗lunch +dinne +o he s)<
con A ∗ egF ee +sponso ship
pos : gues Speake ≥0.4∗sponso ship ∧
gues Speake ≤sponso ship
3. Wo k low Da a G aphs
In o de o analyze may and mus -co ec ness o seman ic wo k lows,
we p opose an app oach based on g aph- heo y and A i icial In elligence
echniques.
In his sec ion, we de ine wo k low da a g aphs, including he s uc u al
cons ain s ha hey should sa is y. Nex , he no ions o da a ins ance sub-
g aph and co ec ness o wo k low da a g aphs a e in oduced. Finally, he
8
concep s o pa ial ins ance subg aph and bo de ac i i y a e p esen ed. The
de ini ions ex end ea lie p oposed de ini ions o he con ol low pe spec i e
o wo k low models [1, 22] by adding da a.
3.1. De ini ion
A wo k low da a g aph, such as he one shown in Figu e 1, is a se o
ac i i ies ha is o de ed o a se o p ocedu al ules. The e ec o each
ac i i y is speci ied wi h a p e and pos condi ion. The o de o execu ion o
he ac i i ies is speci ied by means o di ec ed edges, wi h a unique s a and
a unique end node.
De ini ion 1. A wo k low da a g aph is a uple P= (Ac , V, D, C, E, p e,
pos , w )whe e:
•Ac is a se o ac i i ies;
•Vis a se o yped a iables;
•Dis a se o ini e domains ( ypes), ha con ains o each a iable
∈Va ini e domain D ;
•Cis a se o con ol nodes (ga eways), pa i ioned in o disjoin s se s
o XOR spli s SXOR, AND spli s SAND, XOR joins JXOR, AND joins
JAND, and {s a , end}whe e s a is he unique s a node and end he
unique end node. Each spli in SXOR coun s on condi ion exp essions
o each ga e o he ga eway in o de o speci y he low depending on
he da a;
•E⊆Ac ×Ac is a se o edges which de e mine p ecedence ela ion;
•p e :Ac →Cs(V)assigns o each ac i i y i s p econdi ion (a con-
s ain c∈Cs on he se o a iables V);
•pos :Ac →Cs(V)assigns o each ac i i y i s pos condi ion (a con-
s ain c∈Cs on he se o a iables V);
•w :Ac →Vassigns o each ac i i y i s w i en a iables;
To simpli y he exposi ion, OR ga eways a e no conside ed. We plan o
conside OR ga eways in u u e wo k. Also, we do no conside gua d condi-
ions. O he wo k conside s e i ica ion o wo k low models wi h da a lows
9
ins ance subg aphs, ha can only ge s uck a ( aul y) AND o XOR joins.
Bu an ins ance subg aph ha igge s ais no comple e.
To gene a e a pa ial ins ance subg aph ha igge s a, we ake he exis -
ing IP o mula ion [1] bu eplace one cons ain . The exis ing IP o mula ion
uses o each a∈Ac he cons ain inedge1(a)−a= 0, which s a es ha i
he incoming edge o ais ac i a ed, so inedge1(a) = 1, hen ais ac i a ed as
well, so a= 1. To model ha he incoming edge o ais ac i a ed bu no a,
we eplace o e e y a∈Ac he cons ain inedge1(a)−a= 0 in he o iginal
IP o mula ion [1] wi h inedge1(a)>=a. This cons ain allows ha he
subg aph “s ops” a a(inedge1(a) = 1 and a= 0) bu disallows ha ais
spon aneously ac i a ed, so inedge1(a) = 0 and a= 1 is no allowed.
To gene a e pa ial ins ance subg aphs, as i was men ioned be o e, we use
a sligh ly modi ied e sion o he basic IP o mula ion [1]. All cons ain s
below, excep IP4, a e aken om he basic IP o mula ion [1]. Fo AND
joins we use he elaxed IP o mula ion (IP4) o allow o pa ial ins ance
subg aphs ha s op a an AND join. In ha case, one o he pa allel b anches
synch onised by he AND join has comple ed, bu he o he ones ha e o
comple e. This beha io is disallowed by he basic IP o mula ion.
De ini ion 8. Fo a wo k low da a g aph P= (Ac , V, D, C, E, p e, pos , w ),
he Relaxed IP o mula ion maximizes he alue a he end node subjec
o he ollowing cons ain s a each node in he wo k low g aph. Fo each
node and edge xo P, so x∈ {Ac ∪C∪E}, an IP a iable xis c ea ed.
The cons ain s, adap ed om [1], a e:
IP0 s a = 1
IP1 Fo n∈(SAND ∪SXOR ∪ {end}): inedge1(n) - n = 0
IP1a Fo n∈Ac :inedge1(n) >= n
IP2 Fo n∈(Ac ∪JAND ∪JXOR ∪ {s a }): ou edge1(n) - n = 0
IP3 Fo n∈SAND, being |ou edge(n)|=k:
k
X
i=1
ou edgei(n) - k·n = 0
IP4 Fo n∈JAND, being |inedge(n)|=k:
k
X
i=1
inedgei(n) - k·n≤1
∀i∈[1, k]: n≤inedgei(n)
16

IP5 Fo n∈SXOR, being |ou edge(n)|=k:
k
X
i=1
ou edgei(n) - n = 0
IP6 Fo n∈JXOR, being |inedge(n)|=k:
k
X
i=1
inedgei(n) - n = 0
CSP o mula ion. Cons ain p og amming is based on he algo i hmic es-
olu ion o Cons ain Sa is ac ion P oblems, and is an A i icial In elligence
echnique which p o ides us a way o model he seman ic in o ma ion o a
wo k low da a g aph. A CSP [19] consis s o he iple hV, D, Csi, whe e V
is a se o n a iables 1, 2, ..., nwhose alues a e aken om ini e domains
D 1, D 2, ..., D n espec i ely, and Cs is a se o cons ain s on hei alues.
The cons ain ck(xk1, . . . , xkn) is a p edica e ha is de ined on he Ca e-
sian p oduc Dk1×. . . ×Dkj. This p edica e is ue i he alue assignmen
o hese a iables sa is ies he cons ain ck.
The IP model encodes he con ol low o a da a ins ance subg aph. We
now explain how he da a low, so he p e and pos condi ions o he ac i i ies
con ained in he da a ins ance subg aph, a e ansla ed in o CSP cons ain s.
Fo each ac i i y a∈Ac , a cons ain o he o m a= 1 ⇒(p e(a)∧pos (a))
is de ined. Tha is, i ais pa o he pa ial ins ance subg aph, hen i s p e
and pos condi ion should be sa is ied. We need he conjunc ion s ipula ing
ha a= 1 o ensu e ha he p e and pos condi ion a e only en o ced i ais
ac i a ed, so ais in he ins ance subg aph.
No e ha he p e and pos condi ion cons ain s hold o each ac i i y in
he da a ins ance subg aph, no jus o bo de ac i i ies (c . De ini ion 3).
This way, he cons ain s can be easily encoded in a CSP model. Howe e ,
his encoding complica es inding a solu ion o he CSP model, since he
pos condi ion o a bo de ac i i y migh con lic wi h he pos condi ion o
an ea lie execu ed ac i i y, i bo h ac i i ies e e ence he same a iable.
Fo ins ance, a wo k low da a g aph can con ain wo ac i i ies Aand B ha
bo h w i e in ege a iable i, whe e he pos condi ion o Ais i < 10 and he
pos condi ion o Bis i > 10. A da a ins ance subg aph con aining Aand
Bcan assign only one alue o i, so ei he he pos condi ion o Ao o B
is iola ed. The e o e he pos condi ions o Aand Bcon lic . To esol e
con lic s, we pu he CSP model in SSA o m, explained nex .
SSA o m. In o de o esol e con lic s among pos condi ions, we will con e
he a iables and cons ain s o he CSP model in o S a ic Single Assignmen
17
(SSA) o m. The SSA o m is used in compile design as an in e media e ep-
esen a ion o a p og am [25, 26]. I he wo k low da a g aph is in SSA o m,
each a iable is assigned a alue by only one ac i i y. To u n a wo k low da a
g aph in o an SSA o m, each a iable is sepa a ed in o se e al a iables
i, each o which is assigned a alue by only one ac i i y.
A e iew o he li e a u e e eals a highly ci ed algo i hm o ge he a i-
ables in a p og am in SSA o m [26]. The algo i hm compu es he con ol
low p ope ies o p og ams, like condi ions (XOR) o loops. As an example
o a iables enaming, he wo k low in Figu e 3 uses 4 ac i i ies which ead
and/o w i e he a iables w,x,y, and z. Table 5 shows he p e and pos -
condi ions be o e and a e enaming. No e ha wo new cons ain s ha e
been added a ac i i y D. They a e known as Φ- unc ions in [26], and hey
indica e which assignmen o he a iable y eaches he join poin . Tha is,
he alue o a iable ydepends on he ac i i y which was execu ed (Bo
C).
Figu e 3: Wo k low Example
Howe e , he SSA o m and he enaming algo i hm is de ined o sequen-
ial p og ams while wo k low da a g aphs can con ain pa allelism. Due o
pa allelism, da a low e o s can a ise. Fo ins ance, wo pa allel ac i i ies
can assign he same a iable a alue (con lic ing da a, c . Sec ion 3). In ha
case, he assignmen o he a iable a a subsequen AND join may no be
possible due o con lic ing cons ain s in he CSP model. Fo ins ance, i in
Figu e 3 he XOR nodes a e eplaced wi h AND nodes, bo h Band Cw i e
a iable y. The cons ain s encoding he Φ- unc ion [26] o he subsequen
AND join a e now unsa is iable o y3.
Such da a low e o s a e a a mo e basic le el han iola ions o may and
mus -co ec ness, as explained in Sec ion 3. The e o e, hese da a low e o s
need o be de ec ed and esol ed be o e may and mus -co ec ness can be
diagnosed. The nex sec ion de ines an algo i hm o de ec ing basic da a low
18
Table 5: Va iables be o e and a e he enaming
Ac i i y Be o e SSA A e SSA
Ap e: ue p e: ue
pos : x > 20 pos : x1>20
Bp e: ue p e: ue
pos : y=x+ 10 pos : y1 = x1 + 10
z=x∗2z1 = x1∗2
Cp e: x < 100 p e: x1<100
pos : y=x+ 50 pos : y2 = x1 + 50
w=y∗2w1 = y2∗2
DB= 1 ⇒y3 = y1
C= 1 ⇒y3 = y2
p e: y > x p e: y3> x1
pos : x=x∗ypos : x2 = x1∗y3
e o s.
4.2. De ec ing basic da a low e o s
As explained in Sec ion 3, wo basic da a low e o s a e missing da a and
con lic ing da a. We nex discuss how each ype o da a low e o can be
de ec ed.
To iden i y missing da a, we use he ollowing cons ain . Fo each ac i i y
a∈Ac ha eads a a iable , i he e is a di ec ed pa h om he s a
node o awhe e none o he ac i i ies in he pa h w i es , hen missing da a
is iden i ied.
To iden i y con lic ing da a, we use he algo i hm p esen ed in Figu e 4.
Va iables in Va e p ocessed one by one in a while-loop. The cu en a iable
being p ocessed is cu en (line 6). The algo i hm i e a es o e all ac i i ies
ha w i e cu en in a nes ed o -loop. Fo each pai o dis inc ac i i ies a1
and a2, he algo i hm es s whe he he e exis s a pa ial ins ance subg aph
ha igge s bo h a1and a2. The p e and pos condi ions o he ac i i ies
a e no ele an o his check, so he CSP o mula ion is no used bu only
he IP o mula ion.
The nex heo em asse s he co ec ness o he algo i hm.
19
1: p ocedu e Da a low-No-Con lic -Check(Ac , V, D, C, E, p e, pos , w )
2: e o = alse
3: unma ked =V
4: IP = make IP o mula ion o (Ac ∪C, E)
5: while unma ked 6=∅∧e o = alse do
6: cu en = a a iable om unma ked
7: o a1∈Ac such ha ∈w (a1)do
8: o a2∈Ac such ha ∈w (a2) and a16=a2do
9: IP1=IP && (inedge1(a1)=1) && (a1=0) && (inedge(a2)=1)
&& (a2= 0)
10: sol = sol e IP1
11: i sol is no null hen // CSP 0is sa is iable, so con lic
12: P in ”Race be ween ac i i ies a1and a2 o a iable cu en ”
13: e o = ue
14: end i
15: end o
16: end o
17: unma ked =unma ked { cu en }
18: end while
19: i e o = alse hen
20: P in ”The wo k low da a g aph is da a low-co ec ”
21: end i
22: end p ocedu e
Figu e 4: Algo i hm o checking absence o con lic s
Theo em 1. Le (Ac , V, D, C, E, p e, pos , w )be a wo k low da a g aph.
Algo i hm Da a low-No-Con lic -Check inds no e o i and only i he e is
no con lic ing da a.
P oo 1. In he p oo , we use he ollowing lemma: wo ac i i ies a e ig-
ge ed by he same ins ance subg aph i and only i hey a e in pa allel. This
lemma ollows immedia ely om he de ini ion o ins ance subg aph and he
de ini ion o igge .
⇒: Since algo i hm Da a low-No-Con lic -Check inds no e o , o each
a iable he e is no pa ial ins ance subg aph igge ing wo ac i i ies ha
w i e he same a iable. The e o e, he e a e no wo pa allel ac i i ies w i ing
he same a iable. The e o e he e is no con lic ing da a.
⇐: Suppose he algo i hm inds an ins ance subg aph ha igge s wo
20
ac i i ies a1and a2 ha bo h w i e a iable ∈V. Then by de ini ion he e
is a da a con lic .
4.3. Algo i hm o May-co ec ness
To check may-co ec ness o a wo k low da a g aph and p o ide p ope
eedback in case o an inco ec ness, we de eloped an algo i hm (Figu e 5)
ha diagnoses whe he each ac i i y ais may-execu able (c . De . 4). Fo
each ac i i y a, he algo i hm ies o ind a da a ins ance subg aph ha
igge s aand whose alua ion sa is ies he p econdi ion o a. The da a
ins ance subg aph ha is sea ched o is a solu ion o he combined IP and
CSP model de ined in Sec ion 4.1 plus addi ional cons ain s ha encode
ha ais igge ed and ha he p econdi ion o ais sa is ied.
Looking a he algo i hm in mo e de ail, i begins wi h he IP o mula ion
o he wo k low da a g aph (line 4 in Figu e 5), which s a es he con ol low
cons ain s o da a ins ance subg aphs. This IP o mula ion is combined
wi h he CSP o mula ion o he wo k low (line 5), which s a es he p e and
pos condi ion cons ain s o he ac i i ies in da a ins ance subg aphs. This
combined IP and CSP model is used in he sequel o he algo i hm o e e y
da a ins ance subg aph. Nex , he algo i hm pe o ms a loop o check i
all he ac i i ies a e may-execu able (line 6). The ac i i y being p ocessed
in he loop is s o ed in a iable cu en (line 7). To es whe he ac i i y
cu en is may-execu able, he combined IP and CSP model is ex ended wi h
cons ain s ha a e ue i he da a ins ance subg aph igge s cu en and
sa is ies he p econdi ion o cu en (line 8). I no solu ion exis s, he e is no
such da a ins ance subg aph o cu en , so cu en is no may-execu able
(line 10). I all ac i i ies a e may-execu able, he wo k low da a g aph is
may-co ec (line 17).
The nex heo em asse s ha he algo i hm is co ec .
Theo em 2. Le (Ac , V, D, C, E, p e, pos , w )be a wo k low da a g aph.
Algo i hm May-Co ec ness-Check inds no e o i and only i (Ac , V, D, C,
E, p e, pos , w )is may-co ec .
P oo 2. ⇒:I algo i hm May-Co ec ness-Check inds no e o , o each
ac i i y a, a da a ins ance subg aph exis s, ep esen ed by he solu ion o he
CSP model (line 9), ha igge s a(line 8) and whose alua ion, ep esen ed
by he assignmen o a iables o he CSP a iables, sa is ies he p econdi ion
p e(a)o a(line 8). The e o e, each ac i i y is may-execu able, and he e o e
he wo k low da a g aph is may-co ec .
21

1: p ocedu e May-Co ec ness-Check(Ac , V, D, C, E, p e, pos , w )
2: e o = alse
3: unma ked =Ac
4: IP = make IP o mula ion o (Ac , E)
5: CSP =IP + CSP o mula ion o (Ac , p e, pos )
6: while unma ked 6=∅do
7: cu en = an ac i i y om unma ked
8: CSP 0=CSP && inedge1(cu en ) = 1 && cu en = 0 &&
p e(cu en )
9: sol = sol e CSP 0
10: i sol is null hen // CSP 0is unsa is iable
11: P in ”Ac i i y cu en is no may-execu able”
12: e o = ue
13: end i
14: unma ked =unma ked { cu en }
15: end while
16: i e o = alse hen
17: P in ”The wo k low g aph is may-co ec ”
18: end i
19: end p ocedu e
Figu e 5: Algo i hm o checking may-co ec ness
⇐:I (Ac , V, D, C, E, p e, pos , w )is no may-co ec , hen he e is an
ac i i y a ha is no may-execu able. By De ini ion 4, e e y da a ins ance
subg aph ha igge s acan only ha e a alua ion ha iola es he p econdi-
ion o a. The e o e, he CSP model (line 8) has no solu ion (line 10).
The pe o mance o he algo i hm is discussed in Sec ion 6.
4.4. Algo i hm o Mus -co ec ness
To e i y mus -co ec ness o a wo k low da a g aph, we de elop an algo-
i hm (Figu e 6) ha diagnoses whe he each ac i i y in he wo k low da a
g aph is mus -execu able (c . De . 5). I an ac i i y ais no mus -execu able,
he algo i hm p o ides a coun e example in he o m o a da a ins ance sub-
g aph ha igge s aand whose alua ion iola es he p econdi ion o a. I
e e y ac i i y is mus -execu able, he wo k low da a g aph is mus -co ec
by de ini ion.
Fi s , he combined IP and CSP model is c ea ed (line 4 and line 5) as
de ined in Sec ion 4.1. As in algo i hm May-Co ec ness-Check, each da a
22
1: p ocedu e Mus -Co ec ness-Check(Ac , V, D, C, E, p e, pos , w )
2: e o = alse
3: unma ked =Ac
4: IP = make IP o mula ion o (Ac , E)
5: CSP =IP + CSP o mula ion o (Ac , p e, pos )
6: while unma ked 6=∅do
7: cu en = an ac i i y om unma ked
8: CSP 0=CSP && inedge1(cu en ) = 1 && cu en = 0 &&
¬p e(cu en )
9: sol = sol e CSP 0
10: i sol is no null hen // CSP 0is sa is iable
11: P in ”Ac i i y cu en is no mus -execu able”
12: e o = ue
13: end i
14: unma ked =unma ked { cu en }
15: end while
16: i e o = alse hen
17: P in ”The wo k low g aph is mus -co ec ”
18: end i
19: end p ocedu e
Figu e 6: Algo i hm o checking mus -co ec ness
ins ance subg aph is a solu ion o his CSP model ex ended wi h addi ional
cons ain s. Nex , he algo i hm pe o ms a loop ha p ocesses each ac-
i i y o he inpu wo k low da a g aph (line 6). Va iable cu en s o es
he ac i i y p ocessed in he loop. The algo i hm ex ends o cu en he
combined IP and CSP model wi h cons ain s ha s a e ha he da a in-
s ance subg aph igge s cu en and ha he p econdi ion o cu en is
iola ed. I a solu ion o his ex ended CSP model exis s (line 10) hen
he e is a da a ins ance subg aph ha igge s cu en and whose p econ-
di ion iola es cu en . The e o e, cu en is no mus -execu able (line 11).
O he wise, cu en is mus -execu able and he nex ac i i y is p ocessed. I
e e y ac i i y is mus -execu able, he wo k low da a g aph is mus -co ec
(line 17).
We nex p o e ha he algo i hm is co ec .
Theo em 3. Le (Ac , V, D, C, E, p e, pos , w )be a wo k low da a g aph.
Algo i hm Mus -Co ec ness-Check inds no e o i and only i (Ac , V, D, C,
E, p e, pos , w )is mus -co ec .
23
P oo 3. ⇒:I algo i hm Mus -Co ec ness-Check inds no e o , o each
ac i i y ano da a ins ance subg aph exis s ha igge s a(line 8) and whose
alua ion, ep esen ed by he assignmen o a iables o he CSP a iables,
sa is ies he nega ion o he p econdi ion p e(a)o a(line 8). Equi alen ly,
each da a ins ance subg aph ha igge s ahas a alua ion ha sa is ies he
p econdi ion p e(a). The e o e, each ac i i y is mus -execu able, and he e-
o e he wo k low da a g aph is mus -co ec .
⇐:I (Ac , V, D, C, E, p e, pos , w )is no mus -co ec , hen he e is an
ac i i y a ha is no mus -execu able. By De ini ion 5, he e exis s a da a
ins ance subg aph ha igge s aand ha has a alua ion ha iola es he
p econdi ion p e(a)o a. The e o e, he CSP model (line 8) has a solu ion
and he ac i i y is no mus -execu able (line 11), so he algo i hm inds an
e o .
4.5. Co ec ing e o s
F om he eedback p o ided by he algo i hms, he wo k low designe
should op o a epai ac ion in o de o make he wo k low co ec . Among
he possible epai ac ions when he ac i i y ais non-execu able and is iden i-
ied as esponsible o he inco ec ness, he designe can decide, o example:
• o elax he cons ain ha de ines he p econdi ion o a. This op ion
should be aken when he p oblem is caused by he s ic ness o he
p econdi ion.
• o s eng hen he pos condi ion o some ac i i ies in he ins ance sub-
g aph which igge s a. This may be a solu ion when he p oblem is
caused by pos condi ions ha a e oo weak, allowing alua ions o he
a iables ha cause he iola ion o he p econdi ion o a.
• o modi y he domain o alues o some a iables in he da a low o
a oid he con lic ing alua ions.
4.6. Diagnosing he Mo i a ing Example
This sec ion p esen s he esul s o applying he algo i hms o diagnose
may and mus -co ec ness o he wo k low model in Figu e 1. The wo k low
model has no missing and no con lic ing da a. As explained in Sec ion 4.1,
he CSP model wi h he p e and pos condi ions o each ac i i y needs o
be in SSA o m. Table 6 shows he SSA o m o he p e and pos condi ions
o he ac i i ies wi h he new names o he a iables. No ice ha o he
24
ac i i y R wo new cons ain s a e in oduced because he a iable o he s
has wo new names (o he s1 and o he s2) assigned in wo di e en b anches
o a XOR spli . These wo new cons ain s uni y he name o he a iable o
o he s3 a e he join.
Table 6: Ac i i ies wi h hei p e and pos condi ions in SSA o m
Ac i i y P econdi ion and Pos condi ion
ECR p e: ue
pos : ue
SAP p e: ue
pos : ue
Dp e: sponso ship1>0∨numP ape s1>60
pos : egFee1∗0.1≤dinne 1∧dinne 1≤ egF ee1∗0.35
Lp e: sponso ship1>0∨numP ape s1>60
pos : egFee1∗0.1≤3∗lunch1∧3∗lunch1≤ egF ee1∗0.35
OS p e: sponso ship1>0∨numP ape s1>60
pos : o he s1≤0.2∗ egF ee1+0.05 ∗sponso ship1∧
o he s1≥0.05 ∗ egFee1+0.05 ∗sponso ship1
Op e: sponso ship1>0∨numP ape s1>60
pos : o he s2≤0.25 ∗ egF ee1∧o he s2≥0.05 ∗ egFee1
ROS = 1 ⇒o he s3 = o he s1
O= 1 ⇒o he s3 = o he s2
p e: 3∗lunch1 + dinne 1 + o he s3< egFee1
pos : numPape s1∗1.8≥con A 1
∧numPape s1∗0.5≤con A 1
NGS p e: con A 1∗(3 ∗lunch1 + dinne 1 + o he s3) <
con A 1∗ egF ee1 + sponso ship1
pos : gues Speake 1≥0.2∗sponso ship1∧
gues Speake 1≤sponso ship1+0.1∗ egF ee1∗con A 1
IGS p e: con A 1∗(3 ∗lunch1 + dinne 1 + o he s3) <
con A 1∗ egF ee1 + sponso ship1
pos : gues Speake 2≥0.4∗sponso ship1∧
gues Speake 2≤sponso ship1
Nex , we diagnose he wo k low model o may-co ec ness by applying
he algo i hm May-Co ec ness-Check o he wo k low model in Figu e 1 wi h
25
execu able. Howe e , he algo i hm does no conside he possible alua ions
o he da a o de e mine an inconsis ency. So, jus as Sido o a e al. [17], he
app oach by Webe e al. [16] would diagnose example in Figu e 1 as sound,
wi hou conside ing ha unde ce ain condi ions (i.e., some alua ions o
he a iables) he p ocess may ge s uck.
The e exis modeling languages like Colo ed Pe i ne s [33] ha combine
con ol low and da a. Howe e , hese modeling languages a e no a ge ed
owa ds a speci ic applica ion domain, while he app oach in his pape is
speci ic o wo k lows. Consequen ly, he no ion o mus and may co ec ness
p oposed in his pape is speci ic o wo k lows, bu no used o hese gene al
pu pose languages. Fo ins ance, using CPN Tools a s a e space g aph o
Colo ed Pe i ne can be cons uc ed, bu he esul ing epo only p o ides
gene al s a is ics.
To he bes o ou knowledge, his pape p esen s he i s e i ica ion
app oach o execu able wo k low models ha in eg a es bo h p ocess and
nume ical da a e i ica ion. The app oach can de ec e o s no de ec able
wi h o he app oaches. The app oach builds on esea ch done in he ield
o Cons ain P og amming and wo k low e i ica ion, combining he bes
o bo h wo lds o deli e ad anced ye e icien e i ica ion and diagnosis o
complex wo k low models wi h da a lows.
8. Conclusions
To enginee wo k low models wi h da a lows in a dependable way, diag-
nosis o co ec ness is o u mos impo ance. To ha end, we ha e p oposed
wo k low da a g aphs as o maliza ion o seman ic wo k low models oge he
wi h wo co ec ness no ions, may and mus -co ec ness, ha can be e i ied
o wo k low da a g aphs. Wo k low da a g aphs model seman ic wo k lows
by ex ending wo k low g aphs wi h p e and pos condi ions o he ac i i ies.
We also p oposed wo co ec ness no ions, may and mus -co ec ness, o
wo k low da a g aphs.
Nex , we ha e p esen ed a diagnosis app oach o check may and mus -
co ec ness, which consis s o se e al phases. Fi s , p ep ocessing is applied
o de ec basic da a anomalies. Then, he wo k low da a g aph is ansla ed
in o an IP o mula ion ha models he execu able ins ances, and in o a
CSP o mula ion ha models he da a s a es accep able acco ding o he p e
and pos condi ions o he ac i i ies. The combined IP and CSP model can
be e icien ly sol ed using Cons ain P og amming echniques. In case o
32

an e o , eedback is p o ided in he o m o an e o pa h showing whe e
he wo k low ge s s uck unde ce ain condi ions o e he da a low. Such
eedback p o ides alid in o ma ion o he wo k low designe o ix u u e
e o s be o e he wo k low is deployed. The app oach is comple e, so i always
gene a es accu a e eedback in case o an e o .
The app oach has been implemen ed by ex ending he DiagFlow ool [1].
The ool diagnoses wo k low models in an ex ended XPDL o ma . The
XPDL ex ension is needed o s o e he seman ic in o ma ion o each wo k-
low, adding he da a low wi h he p e and pos condi ions in he ac i i ies.
Pe o mance e alua ion o he ool shows ha he algo i hms scale well o
la ge wo k low models wi h da a lows, despi e he high wo s -case complexi y
o sol ing cons ain s sa is ac ion p og ams.
As u u e wo k, we plan o ex end he wo k low da a g aph model wi h
OR ga eways. Likewise, we would also like o o e addi ional eedback o he
end use in case o a iola ion, making easie he job o ixing he p oblem
which causes he abno mal beha io . Ano he in e es ing ex ension is o
conside s ochas ic beha io o iming beha io o ac i i ies, o imp o e he
accu acy o he analysis.
Re e ences
[1] R. Eshuis, A. Kuma , An in ege p og amming based app oach o
e i ica ion and diagnosis o wo k lows, Da a Knowl. Eng. 69 (2010)
816–835.
[2] S. Jablonski, C. Bussle , Wo k low managemen - modeling concep s,
a chi ec u e and implemen a ion, In e na ional Thomson, 1996.
[3] W. an de Aals , A. Hi nschhall, H. M. W. Ve beek, An al e na i e way
o analyze wo k low g aphs, in: P oceedings o he 14 h In e na ional
Con e ence on Ad anced In o ma ion Sys ems Enginee ing (CAiSE02),
olume 2348 o Lec u e No es in Compu e Science, Sp inge -Ve lag,
2002, pp. 535–552.
[4] H. H. Bi, J. L. Zhao, P ocess logic o e i ying he co ec ness o
business p ocess models, in: In e na ional Con e ence on In o ma ion
Sys ems ICIS, Associa ion o In o ma ion Sys ems, 2004, pp. 91–100.
33
[5] R. Eshuis, R. Wie inga, Ve i ica ion suppo o wo k low design wi h
uml ac i i y g aphs, in: P oceedings o he 24 h In e na ional Con e -
ence on So wa e Enginee ing, ACM, 2002, pp. 166–176.
[6] C. Ka amanolis, D. Giannakopoulou, J. Magee, S. M. Whea e , Model
checking o wo k low schemas, in: P oceedings o IEEE EDOC, 2000,
pp. 170–179.
[7] H. Lin, Z. Zhao, H. Li, Z. Chen, A no el g aph educ ion algo i hm o
iden i y s uc u al con lic s, in: P oceedings o he 35 h Annual Hawaii
In e na ional Con e ence on Sys em Sciences (HICSS’02) - Volume 9,
HICSS ’02, IEEE Compu e Socie y, Washing on, DC, USA, 2002.
[8] S. W. Sadiq, M. E. O lowska, W. Sadiq, C. Foulge , Da a low and
alida ion in wo k low modelling, in: ADC, olume 27 o CRPIT, Aus-
alian Compu e Socie y, 2004, pp. 207–214.
[9] F. Tou ´e, K. Ba¨ına, K. Benali, An e icien algo i hm o wo k low g aph
s uc u al e i ica ion, in: P oceedings o he OTM 2008 Con ede a ed
In e na ional Con e ences. Pa I on On he Mo e o Meaning ul In e ne
Sys ems, Sp inge -Ve lag, Be lin, Heidelbe g, 2008, pp. 392–408.
[10] W. M. P. an de Aals , K. M. an Hee, A. H. M. e Ho s ede,
N. Sido o a, H. M. W. Ve beek, M. Voo hoe e, M. T. Wynn, Sound-
ness o wo k low ne s wi h ese a cs, T. Pe i Ne s and O he Models
o Concu ency 3 (2009) 50–70.
[11] M. T. Wynn, H. M. W. Ve beek, W. M. P. . d. Aals , A. . Ho s ede,
D. Edmond, Business p ocess e i ica ion - inally a eali y!, Business
P ocess Managemen Jou nal 15 (2009) 74–92.
[12] W. Van De Aals , K. Van Hee, A. Te Ho s ede, N. Sido o a, H. Ve -
beek, M. Voo hoe e, M. Wynn, Soundness o wo k low ne s: Classi ica-
ion, decidabili y, and analysis, Fo mal Aspec s o Compu ing 23 (2011)
333–363. Ci ed By (since 1996) 20.
[13] S. Pa ig, M. S olz, A pa e n-based app oach o he e i ica ion o
business p ocess desc ip ions, In . So w. Technol. 55 (2013) 58–87.
34
[14] S. X. Sun, J. L. Zhao, J. F. Nunamake , O. R. L. Sheng, Fo mula ing
he da a- low pe spec i e o business p ocess managemen , In o ma ion
Sys ems Resea ch 17 (2006) pp. 374–391.
[15] N. T ˇcka, W. M. Aals , N. Sido o a, Da a- low an i-pa e ns: Disco -
e ing da a- low e o s in wo k lows, in: P oceedings o he 21s In-
e na ional Con e ence on Ad anced In o ma ion Sys ems Enginee ing,
CAiSE ’09, Sp inge -Ve lag, Be lin, Heidelbe g, 2009, pp. 425–439.
[16] I. Webe , J. Ho mann, J. Mendling, Beyond soundness: on he e i-
ica ion o seman ic business p ocess models, Dis ibu ed and Pa allel
Da abases 27 (2010) pp. 271–343.
[17] N. Sido o a, C. S ahl, N. T cka, Soundness e i ica ion o concep ual
wo k low ne s wi h da a: Ea ly de ec ion o e o s wi h he mos p eci-
sion possible, In o ma ion Sys ems 36 (2011) pp. 1026–1043.
[18] W. M. P. an de Aals , N. Lohmann, M. La Rosa, Ensu ing co ec ness
du ing p ocess con igu a ion ia pa ne syn hesis, In . Sys . 37 (2012)
574–592.
[19] F. Rossi, P. an Beek, T. Walsh (Eds.), Handbook o Cons ain P o-
g amming, Else ie , 2006.
[20] WFMC, Wo k low Managemen Coali ion Wo k low S anda d: P ocess
De ini ion In e ace – XML P ocess De ini ion Language, Technical Re-
po WFMC-TC-1025, Wo k low Managemen Coali ion, 2005.
[21] OMG, Objec Managemen G oup, Business P ocess Model and No a-
ion (BPMN), Ve sion 2.0, OMG S anda d, 2011.
[22] W. Sadiq, M. E. O lowska, Analyzing p ocess models using g aph e-
duc ion echniques, In o ma ion Sys ems 25 (2000) pp. 117–134.
[23] R. Eshuis, A. Kuma , An In ege P og amming based App oach o
Diagnosing Wo k lows, Technical Repo , Be a Wo king Pape Se ies,
WP 264, Eindho en Uni e si y o Technology, 2008.
[24] R. Eshuis, R. Wie inga, Tool suppo o e i ying uml ac i i y dia-
g ams, IEEE T ansac ions on So wa e Enginee ing 30 (2004) pp. 437–
447.
35
[25] B. Alpe n, M. N. Wegman, F. K. Zadeck, De ec ing equali y o a iables
in p og ams, in: P oceedings o he 15 h ACM SIGPLAN-SIGACT,
Symposium on P inciples o P og amming Languages, ACM, New Yo k,
NY, USA, 1988, pp. 1–11.
[26] R. Cy on, J. Fe an e, B. K. Rosen, M. N. Wegman, F. K. Zadeck,
E icien ly compu ing s a ic single assignmen o m and he con ol de-
pendence g aph, ACM T ansac ions on P og amming Languages and
Sys ems 13 (1991) pp. 451–490.
[27] Dynamic Decision Technologies, Dynadec web page,
h p://dynadec.com/, 2011.
[28] P. T axle , The ime complexi y o cons ain sa is ac ion, in: P o-
ceedings o he 3 d in e na ional con e ence on Pa ame e ized and exac
compu a ion, IWPEC’08, Sp inge -Ve lag, Be lin, Heidelbe g, 2008, pp.
190–201.
[29] R. Dech e , Cons ain ne wo ks, Encyclopedia o A i icial In elligence,
Second Edi ion (1992) pp. 276–285.
[30] V. Kuma , Algo i hms o cons ain sa is ac ion p oblems: A su ey,
AI Magazine 13 (1992) pp. 32–44.
[31] J. Ca doso, E alua ing he p ocess con ol- low complexi y measu e,
in: Web Se ices, ICWS 2005. P oceedings. 2005 IEEE In e na ional
Con e ence, olume 2, pp. 803–804.
[32] D. Bo ego, R. M. Gasca, M. T. G´omez-L´opez, L. Pa ody, Con ac -
based diagnosis o business p ocess ins ances using business compliance
ules, in: P oceedings o he 21s In e na ional Wo kshop on P inciples
o Diagnosis (DX-10), 2010, pp. 169–176.
[33] K. Jensen, L. M. K is ensen, L. Wells, Colou ed pe i ne s and cpn ools
o modelling and alida ion o concu en sys ems, STTT 9 (2007) 213–
254.
36