An Iterative Approach for Business Process Template Synthesis from Compliance Rules - Advanced Information Systems Engineering - page 408

consistency. This check guarantees that a template can be generated. Inconsistent traces
hint at issues in the specification, so that a new iteration of the synthesis may be started
with refined compliance rules or adapted domain knowledge. We focus on the analysis
of traces in Section 3.4. If the traces are consistent, we apply a process synthesis algo-
rithm to extract a process template. Details on this step are given in Section 3.5. The
synthesized template is then analyzed to identify discrepancies that stem, e.g., from un-
derspecification. Depending on the result of this analysis, again, a new iteration of the
synthesis may be started. We discuss the evaluation of process templates in Section 3.6.
Example. We illustrate our approach with an example from the financial domain. Anti
money laundering guidelines [8] address financial institutes, e.g., banks, and define a
set of checks to prevent money transfers with the purpose of financing criminal actions.
We focus on the following guidelines for opening new bank accounts:
R 1 : A risk assessment has to be conducted for each 'open account' request.

R 2 : A due diligence evaluation has to be conducted for each 'open account' request.

R 3 : Before opening an account the risk associated with that account must be low. Oth-

erwise, the account is not opened.

R 4 : If due diligence evaluation fails, the client has to be added to the bank's black list.

3.2 LTL Encoding
Once the compliance rules have been collected, a behavioral model that represents all
traces conforming to these rules is created. In order to arrive at such a model, we need to
collect extra domain-specific rules. Much of the domain-specific rules can be generated
automatically from a higher level description. Such a description needs to be defined by
a human expert in the first place and comprises the following information.

Actions and Goals. The set of all actions is denoted by A .Thesetof goal actions
G A comprises activities that indicate the completion of a trace. Moreover, we

capture contradicting actions that are not allowed to occur together in one trace in
a relation CA

⊂

× 2 A .
Results and Initial Values. The set of all results is denoted by R . The initial values
of data objects are defined by a set IV

: A

⊂ R . Further, we define the set of negated

results as R

= {¬ r | r ∈ R }

. Similar to contradicting actions, we capture contra-
dicting results in a relation CR × 2 R .

Relation between Actions and Results. The mapping from actions to sets of results is
given as a relation AM

: R

× 2 R ∪ R . Mutually exclusive sets of results are captured : A

.
Based on this information and two additional actions start and end that represent
the initial and final states of a trace (independent of any goal states), we derive LTL
rules to represent the domain knowledge according to Table 1. Common process de-
scription languages, e.g., BPMN or EPCs, assume interleaving semantics, which is
enforced by formula interleaving and progress . The information on exclusiveness
constraints and on contradicting actions and results yields the formulae mutex and
contra . The formula causality guarantees correct implementation of dependencies be-
tween actions and results. Finally, the formulae once , final , goals ,and initial ensure

in a relation RE = { S : ∃ a ∈ A. ( a, S ) ∈ AM ∧ S = ∅}