Information Technology Reference
In-Depth Information
Note that the results are all descriptive statements, while the actions refer to activities.
Moreover, we introduce
positive
representations for the states 'high' and 'low' of the
risk object, even though both states are opposed. That is due to the three possible states
of the risk object: high, low, or initial. The same holds true for the the due-diligence
object.
Based on these actions and results, the compliance rules are encoded in LTL. As
a process to open a bank account is considered, the process is assumed to start by
receiving such a request. Therefore, rules 1 and 2 are interpreted as “A risk assessment
has to be conducted” and “A due diligence evaluation has to be conducted”, respectively.
The third rule is interpreted to mean that the risk associated with opening an account
must be low
at the time the request is granted
, rather than at some point in the past.
Similarly is the case when denying the open request, the risk has to be high.
R
1
:
A risk assessment has to be conducted.
F
ra
“Eventually
ra
must hold”
R
2
:
A due diligence evaluation has to be conducted.
F
edd
“Eventually
edd
must hold”
R
3
:
The risk associated with opening an account must be low when the request is
granted.
G
(
og
⇒
rl
)
∧
G
(
od
⇒
rh
)
“Alwa y s,
og
only if
rl
, and always,
od
only if
rh
”
R
4
:
If due diligence evaluation fails, the client has to be added to the bank's black list.
G
“Alwa y s,
edd
and
ef
imply eventually
bl
”
As a next step, the domain knowledge is defined in more detail. For instance, the action
mapping defines
ra
(
edd
∧
ef
⇒
F
bl
)
. The former says that action
ra
causes the risk object to take a concrete value of 'high' or 'low'. The latter means that
ra
causes the risk to stop being 'initial' by forcing
ri
to not hold. Excluding results
are defined, e.g.,
→{
rh, rl
}
and
ra
→{¬
ri
}
states that at most one of the propositions
ri, rh, rl
can
hold at a time. The goal of the process is defined as
{
ri, rl, rh
}
{
og, od
}
and the set of initial
values
signifies that initially, both risk and due-diligence objects, are put to
an initial, unknown, value. There are also contradicting actions,
{
ri, ei
}
{
og
→{
od
}
,od
→
{
, ensuring that we cannot grant and deny a request within the same trace. Based
on Table 1, this specification is converted into LTL. For example, this yields the formula
progress
og
}}
end
. The final set of LTL formulae is the
union of the
domain
formula with all four formulae representing the compliance rules.
=
ra
∨
edd
∨
og
∨
od
∨
bl
∨
start
∨
3.3
Extracting Traces
Given a set of LTL formulae, we apply the technique summarized in Section 2.3 to
determine whether the constraints are satisfiable. If so, we obtain a pseudomodel that
describes all traces that conform to the set of formulae. To create a process template,
these traces are extracted. Any sequence
σ
s
0
,...,s
n
of states, starting at the root
node of the pseudomodel can be extended into a trace. As we are modeling finite se-
quences with an end state, we consider a trace to be complete if
end
=
s
n
. Because of
the
once
constraint introduced in the previous section, there will be no loops in the pseu-
domodel between the start and the end. Hence, the finite set of paths in the pseudomodel
between the root state and a state labeled with
end
is the set of correct traces.
∈
