Information Technology Reference
In-Depth Information
Ta b l e 1 .
The formulae making up the domain knowledge
Constraint Description
Formalization
⇒
(
b∈A\{a}
¬
To realize interleaving semantics, the formula
interleave
ensures that at most one action can be
true, i.e., one activity can be executed, at any state.
interleave
(
a
)=
a
b
))
=
a∈A
interleave
interleave
(
a
)
=
a∈A
The formula
progress
guarantees that at least one
action occurs at each state.
progress
a
)=
a,b∈S, a
=
b
¬
(
The mutual exclusion constraints given in
RE
are
enforced by the formula
mutex
, i.e., exclusive
results cannot be true at the same time.
mutex
(
S
a
∧
b
)
=
S∈RE
mutex
mutex
(
S
)
⇒
G
b∈CA
(
a
)
¬
Knowledge on contradicting actions or results is
taken into account by the formulae,
con
and
conRes
.
con
(
a
)=
a
b
⇒
G
s∈CR
(
r
)
¬
conRes
(
r
)=
a
s
=
a∈A∪R
contra
con
(
a
)
∧
conRes
(
a
)
⇒
r∈S
To implement the relation between actions and
results, formula
cau
1
states that for every entry
(
cau
1
(
a, S
)=
a
r
cau
2
(
r
)=
⇒
(
X
(
a,S
)
∈AM, {r,¬r}∩S
=
∅
AM
the action
a
must cause at least one
of the results in
S
.Formula
cau
2
states that for
every result
r
, that result can only be changed by
one of the actions which can cause it.
a, S
)
∈
r
a
)
B
¬
r
causality
=
(
a,S
)
∈AM
)
∧
r∈R∪R
cau
1
(
a, S
cau
2
(
r
)
The formula
once
enforces that all actions other
than
end
occur at most once, in order to avoid
infinite behavior. The formula
once
(
a
)=
a ⇒
XG
¬a
once
=
a∈A\{end}
once
(
a
)
enforces that
end
persists forever to represent the process end.
final
final
=
end
⇒
G
end
=
g∈G
The formula
goals
is used to require that
eventually the outcome of the process is
determined, while
inital
ensures correct initial
values for all objects.
goals
g
⇒
v∈IV
initial
=
start
v
correct initialization and successful termination of any trace. The combination of all
these formulae yields the formula
domain
, which represents the domain knowledge.
domain
=
start
∧
G
initial
∧
F
goals
∧
F
end
∧
G
interleave
∧
G
progress
∧
G
mutex
∧
G
causality
∧
G
once
∧
G
contra
∧
G
final
Example.
For our example, an expert first identifies the following actions and results.
Actions
=
{
ra, edd, og, od, bl
}
Results
=
{
ri, rh, rl, ei,
ef
,ep
}
ra
: conduct a risk assessment
ri
: risk assessment is initial
edd
: evaluate due-diligence
rh
: risk was assessed as high
og
: grant a request to open an account
rl
: risk was assessed as low
od
: deny a request to open an account
ei
: due-diligence evaluation is initial
bl
: blacklist a client.
ef
: due-diligence evaluation failed
ep
: due-diligence evaluation passed.
