Ensuring Business Process Compliance Along the Process Life Cycle [original]

Ensuring Business Process Compliance

Along the Process Life Cycle

David Knuplesch and Manfred Reichert

Abstract

Business processes are subject to semantic constraints that stem from regu-

lations, laws and guidelines, and are also known as compliance rules. Hence,

process-aware information systems have to ensure compliance with those rules

in order to guarantee semantically correct and error-free executability as well

as changeability of their business processes. This report discusses how com-

pliance rules can be defined and how business process compliance can be

ensured for the different phases of the process lifecycle.

1 Motivation

In many past publications [1, 2] the correctness of a pre-specified process

model was directly related to its syntactical properties and behavioral sound-

ness (i.e., state consistency). However, these are not the only constraints, a

pre-specified process model has to obey. Typically, process models and corre-

sponding process instances are also subject to semantic constraints stemming

from a variety of sources like standards, regulations, guidelines, corporate

policies, and laws (e.g. Basel or Sarbanes-Oxley-Act). In the following these

semantic constraints are denoted as compliance rules, and techniques for en-

suring the compliance of a business process with these rules are covered under

the term business process compliance.

Compliance rules typically restrict the order in which process activities may

be executed. Hence, a compliance rule can be defined as a function that

recognizes whether or not a process instance – represented by its execution

trace – complies with the rule (cf. Definition 1). Generally, syntactically cor-

Institute of Databases and Information Systems

Ulm University, Germany

e-mail: {david.knuplesch,manfred.reichert}@uni-ulm.de

2 Knuplesch, Reichert

rect and sound process models still can violate compliance rules. When being

confronted with large process models or numerous compliance rules, however,

traditional approaches like manual auditing are not feasible. This, in turn,

raises the demand for techniques automatically ensuring business process

compliance in all phases of the process lifecycle.

Definition 1 (Compliance Rule). Let Σbe the set of all activities

and let Σ?be the set of all possible execution traces of processes based

on activities from Σ. Then: A compliance rule φdefines a function

φ:Σ?→Boolean that considers any trace σ=< e1, . . . , ek>∈Σ?

either to be true (i.e., to be compliant with φ) or false (i.e. to violate φ

or to be not compliant with it). We further denote σ|=φ:⇔φ(σ) and

say trace σsatisfies compliance rule φ.

Surgical Suite

discharge letter

for referring phys.

Outpatient DepartmentSurgical Ward

MTAPhysicianPhysicianNurse

Admit

patient

Perform

checkup Examine

patient Inform about

risks

Inform about

anesthesia Make

decision

Check

patient record

Admit

patient

Schedule

surgery

Write

discharge letter

Write

discharge letter

Make

lab test

Create

surgery report

Provide

postsurgical care

Discharge

patient

patient referral

to hospital

Transport

patient to ward

surgery

Perform

surgery

Prepare

patient

Send patient

to surgical suite

Fig. 1 Pre-Specified Process Model Smed

Ensuring Business Process Compliance Along the Process Life Cycle 3

Example 1 (Compliance Rules). Consider the process model Smed from

Figure 1. It shows a pre-specified process model for planning and per-

forming a keyhole surgery in a hospital. Further, consider the informal

compliance rules from Table 1, which must be satisfied by all medical

processes of the respective hospital. In particular, these compliance rules

have to be obeyed by the pre-specified process model from Figure 1 as

well. When analyzing the dynamic behavior of the process model, its

soundness [1, 2] can be easily verified. However, having a closer look

at the model and the compliance rules from Table 1, one can recognize

that the process model contains semantic errors; i.e., it violates some of

the given compliance rules. For example, according to the process model

the surgical ward may send the patient to the surgical suite before he is

prepared; the surgery could be even performed without having prepared

the patient at all. Obviously, this violates compliance rule c1. Further,

in the given process model the patient is either informed about anes-

thesia or risks, but not about both. However, according to compliance

rule c3the patient must be always informed about the risks after the

examination. Hence, c3is potentially violated.

Table 1 Examples of Compliance Rules for Medical Processes

c1Before a surgery may be performed the patient has to be prepared for it and be sent to

the surgical suite.

c2After examining the patient a decision has to be made. However, this must not be done

before the examination.

c3After the examination, the patient has to be informed about the risks of the (planned)

surgery.

c4Before scheduling the surgery the patient has to be informed about anesthesia.

c5If a surgery has not been scheduled it must not be performed.

c6After a patient is discharged a discharge letter has to be written.

c7After performing the surgery and before writing the discharge letter, a surgery report

must be created and a lab test be made.

Generally, ensuring business process compliance not only concerns the model-

ing phase of the process lifecycle [3], i.e., the definition of pre-specified process

models. Additionally, compliance has to be monitored for process instances

during their execution. This is crucial for process instances being defined or

adapted on-the-fly [4], i.e., for which there is no fully pre-specified process

model. Further, compliance monitoring at run-time is required if a priori

compliance checking is not feasible, e.g., if the process model is too large

or the compliance rules are too complex. Finally, for completed process in-

4 Knuplesch, Reichert

stances, a PAIS needs to be able to determine whether or not these instances

were executed in compliance with given regulations, laws and guidelines. For

this purpose, execution logs need to be analyzed accordingly.

Independent from the process lifecycle phase for which business process com-

pliance has to be ensured, compliance rules have to be specified in a machine-

readable way. Hence, this report first deals with issues related to the modeling

of compliance rules in Section 2. Following this, it will be shown how compli-

ance can be ensured during the different phases of the process lifecycle. More

precisely, Section 3 addresses a priori compliance checking in the process

modeling phase. Then, Section 4 shows how compliance rules can be moni-

tored during the execution of process instances, whereas Section 5 discusses

issues related to the compliance of completed process instances. Section 6

further illustrates how compliance can be ensured in the context of process

changes. We address the user perspective in Section 7 and present existing

approaches enabling business process compliance in Section 8. The report

closes with a summary in Section 9.

2 Modeling Compliance Rules

As prerequisite for verifying business process compliance of pre-specified pro-

cess models, process instances or process execution logs, corresponding com-

pliance rules need to be provided in a machine-readable way. In literature,

there exist different approaches for this. One way to define and represent

compliance rules is the usage of Linear Temporal Logic (LTL) [5]. LTL is

a modal temporal logic with modalities referring to time. It enhances ordi-

nary propositional logic with additional temporal operators as specified in

Definition 2.

Definition 2 (Syntax of Linear Temporal Logic). A formula <

LT L > is a syntactical correct LTL formula if it complies with the

following grammar (expressed in BNF):

<LT L>::= > | ⊥ | ¬ <LT L> |(<LT L>)

|X<LT L> |F<LT L> |G< LT L>

|<LT L> ∧< LT L> |<LT L> ⇒<LT L>

|<LT L> ∨< LT L> |<LT L> U<LT L>

|<LT L> W< LT L>

In Definition 2, X,F,G,U, and Wcorrespond to temporal operators: X

means next,Fmeans eventually,Gmeans global,Umeans until, and W

Ensuring Business Process Compliance Along the Process Life Cycle 5

means weakly until. Further, < LT L > may contain propositional variables.

In our context, these variables correspond to the execution of activities (e.g.

G(Discharge patient ⇒FWrite discharge letter)).

The temporal operators enable the navigation from point to point on a time

line. Definition 3 provides the formal semantics of these temporal operators

using recursive equitations.

Definition 3 (Semantics of Linear Temporal Logic). LTL is

defined on infinite traces. Hence, for any execution trace σ=<

e1, e2, e3, . . . , en>we first define its infinite extension σ:=<

e1, e2, e3, . . . , en,∅,∅,· · · >by adding empty events after event en. Fur-

ther let φand ψbe LTL formulas.

σ|=φ:⇔σ|=φ

σ=< e1, e2, e3,· · · >|=Xφ:⇔< e2, e3,· · · >|=φ

1. σ|=Fφ:⇔σ|=φ∨X F φ

2. σ|=Gφ:⇔σ|=φ∧X G φ

3. σ|=φUψ:⇔σ|=ψ∨(φ∧X(φUψ))

whereby ψhas to occur eventually (i.e., Fψholds).

4. σ|=φWψ:⇔σ|=ψ∨(φ∧X(φWψ))

whereby ψneed not occur eventually (i.e., G¬ψis allowed).

Example 2 illustrates how LTL can be used for modeling compliance rules.

Example 2 (Modeling Compliance Rules with LTL). Table 2 provides

examples illustrating the use of LTL. More precisely, the informal com-

pliance rules from Table 1 are now formally defined based on LTL.

Obviously, the formal definition of compliance rules by the use of LTL or other

temporal logics (e.g., Table 2) requires expert knowledge. In particular, LTL

expressions will be not understandable to domain experts. Hence, graphi-

cal notations like Compliance Rule Graphs (CRGs) have been suggested [6].

CRGs allow modeling compliance rules on a higher level of abstraction based

on graphs. CRGs further define a compliance rule by means of an antecedent

pattern complemented by a consequence pattern. Both, the antecedent and the

consequence pattern consist of occurrence and absence nodes. These nodes

are connected by directed edges that may also connect antecedent nodes with

consequence nodes. While nodes require the existence or absence of activities,

the edges connecting them describe respective activity sequences. Note that

edges must not connect two absence nodes.

6 Knuplesch, Reichert

Table 2 Representing the Compliance Rules from Table 1 in LTL

c1¬Perform surgery W(Prepare patient

∧(¬Perform surgery WSend patient to surgical suite))

c2(G(Examine patient ⇒FMake decision))

∧(¬Make decision UExamine patient)

c3G(Examine patient ⇒FInform about risks)

c4¬Schedule surgery WInform about anesthesia

c5(G¬Schedule surgery) ⇒(G¬Perform surgery)

c6G(Discharge patient ⇒FWrite discharge letter)

c7G(¬Perform surgery ⇒(FWrite discharge letter

⇒((¬Write discharge letter UCreate surgery report)

∧(¬Write discharge letter UMake lab test))))

The semantics of an CRG is as follows: Each trace will be compliant with

the CRG, if for any match of the antecedent pattern to the trace’s entries

the related consequence pattern has to find at least one suitable match as

well. Further, if there exists no match of the antecedent pattern the trace

will be compliant as well. The latter kind of compliance is denoted as trivial

compliance.

Any match of the antecedent pattern to a trace is a mapping from each an-

tecedent occurrence node to one of the entries of the trace. For sequenced

antecedent occurrence nodes, whose sequence is expressed by edges, the cor-

responding trace entries have to obey the same sequence. Further, for each

antecedent absence node, there must be no trace entry of the antecedent ab-

sence node’s activity that obeys the sequences with trace entries of adjacent

antecedent occurrence nodes denoted by appropriate edges. A suitable match

of the consequence pattern maps any consequence occurrence node to a cor-

responding trace entry as well. Further those trace entries have to consider

the sequence denoted by the edges as well. In addition, there must be no trace

entry of the consequence absence node’s activity that obeys sequences with

trace entries of adjacent antecedent and consequence occurrence nodes that

are denoted by appropriate edges. Examples 3 and 4 illustrate the semantics

of CRG-based constraints.

Example 3 (Compliance of Simple CRGs). We consider Figure 2 in or-

der to exemplarily describe the semantics of CRGs. More precisely, two

CRGs and related execution traces are provided in Figure 2A and Fig-

ure 2B respectively. Furthermore, for each trace we indicate whether

the corresponding process instance complies with the respective CRG

or violates it.

Ensuring Business Process Compliance Along the Process Life Cycle 7

A B

Antecedent

occurrence node

Consequence

occurrence node

σ = < E, D, F, G, B>

σ = < C, A, B, D, B>

σ = < A, F, A, D, B>

σ = < G, C, F, D, G >

σ = < G, C, B, A, D >

σ = < A, D, B, G, A>

BA C

Antecedent

absence node

Consequence

absence node

σ = < A, B, F, C, D >

σ = < B, F, D, B,A >

σ = < G, F, E, D, E >

σ = < G, D, B, F, D >

σ = < B, G, E, C, D >

σ = < B, A, B, F, C>

trivial compliant

compliant

trivial compliant

compliant

violation

trivial compliant

compliant

trivial compliant

violation

Antecedent pattern

Consequence pattern

BA C

no match

< C, A, B, D, B >

< A, F, A, D, B >

no match

< G, C, B, A, D >

< A, D, B, G, A >

< A, D, B, G, A>

Consequence pattern

< C, A, B, D, B >, < C, A, B, D, B>

< A, F, A, D, B>

no match

< A, D, B, G, A >,

no match

no match ( < B, A,B, F, C > )

< B, F, D, B, A >

no match

< G, D, B, F, D >

< B, G, E, C, D >

< B, A, B, F, C >

( not < B, A,B, F, C > )

< B, F, D, B, A >

< G, D, B, F, D >

no match ( < B, G, E, C, D > )

no match ( < B, A, B, F, C> )

Fig. 2 Simple Compliance Rule Graphs

Regarding the two CRGs from Figure 2, for example, trivial com-

pliance holds for σ1, σ4, and σ9. Obviously, for each of theses traces at

least one antecedent occurrence node can not be mapped to any trace

entry; e.g., Adoes not occur in σ1. Trace σ7constitutes another ex-

ample of trivial compliance although the antecedent occurrence node

Bcan be mapped to a trace entry; however, trace σ7also contains an

entry of activity A(preceding the entry of B) which corresponds to the

antecedent absence node (i.e., this entry prevents the antecedent pat-

tern from matching with σ7). To allow for a match of the antecedent

pattern in the given context there should not occur an Apreceding the

Bin σ7.

Consider now the non-trivial compliant traces: σ2, σ3, σ8, and σ10.

Concerning σ2, the antecedent pattern Amatches once, and there are

two suitable matches of the consequence pattern B. Regarding σ3,A

8 Knuplesch, Reichert

occurs twice. Since Bsucceeds both occurrences of A, there is a suitable

mapping of the consequence pattern in both cases. The same applies

to σ8and the CRG depicted in Figure 2B: There are two mappings

of the antecedent pattern in terms of the two Bthat do not have a

preceding A(but a succeeding one). Further, for both mappings there

is no Csucceeding the B. Hence, trace σ8is compliant with the CRG

depicted in Figure 2B. Finally, σ10 contains exactly one mapping of the

antecedent pattern B. Since no Cis following, the consequence pattern

maps as well.

Finally, let us consider the non-compliant traces σ5, σ6, σ11, and σ12.

σ5violates the CRG from Figure 2A since the antecedent pattern maps

on the A, but no suitable mapping of the consequence pattern with a

Bfollowing the Acan be found (the only occurring Bprecedes A). Re-

garding σ6, the antecedent pattern maps twice. However, while for the

first Athere exists a suitable mapping of the consequence pattern with

the B, the second Ais not followed by any B; i.e., trace σ6violates the

CRG depicted in Figure 2A. Regarding the CRG from Figure 2B and

σ11, the Ballows for the antecedent pattern to match, while the suc-

ceeding Cprohibits the consequence pattern to match. Finally, consider

the violation of the CRG from Figure 2B by σ12: Due to the presence

of the A, the antecedence pattern cannot map to the second occurrence

of B, but only to the first one. Due to the presence of the Cat the end

of the trace, however, no suitable match of the consequence pattern is

possible.

Example 4 (Compliance of Complex CRGs). Figure 3 provides two ad-

ditional CRGs and related execution traces. Again, for each trace it is

indicated whether the corresponding process instance complies with the

respective CRG or violates it.

Regarding Figure 3A, for example, trivial compliance holds for σ13

and σ16. Obviously, for each of theses traces at least one antecedent

occurrence node can not be mapped to any trace entry. Furthermore,

σ15, σ21, and σ22 also constitute examples of trivial compliance although

the antecedent occurrence nodes can be mapped to trace entries; how-

ever, the traces contain entries of the antecedent absence nodes’ ac-

tivities as well (i.e., those prevent the antecedent patterns from being

matched). Regarding σ15 there should be no Bbetween Aand Dto al-

low for a match of the antecedent pattern of the CRG from Figure 3A.

Regarding σ21 and σ22 no Ashould occur, in turn, to allow for a match

of the antecedent pattern of the CRG from Figure 3B.

Ensuring Business Process Compliance Along the Process Life Cycle 9

σ = < A, C, B, G, C >

σ = < E, A, E, C, D>

σ = < E, A, E, B, D>

σ = < G, B, E, G, D>

σ = < A, F, D, G, B>

σ = < A, F, D, C, D>

Antecedent pattern

Consequence pattern

no match

< E, A, E, C, D>

no match ( < E, A, E, B, D> )

no match

< A, F, D, G, B >

< A, F, D, C, D>

< A, F, D, C, D >

Consequence pattern

< E, A, E, C, D>

no match

< A, F, D, C, D>

no match

< E, D, F, G, B>

< D, F, C, E, B>

no match ( < A, B, C, E, D > )

no match ( < G, C, B, A, D > )

< C, F, B, G, E >

< C, F, D, E, B>

< E, D, F, G, B>

< D, F, C, E, B>

no match

no match ( < C, F, D, E, B> )

B A B A

trivial compliant

compliant

trivial compliant

violation

σ = < E, D, F, G, B>

σ = < D, F, C, E, B>

σ = < A, B, C, E, D>

σ = < G, C, B, A, D>

σ = < C, F, B, G, E >

σ = < C, F, D, E, B>

compliant

trivial compliant

violation

Fig. 3 More Complex Compliance Rule Graphs

Consider now the non-trivial compliant traces σ14, σ19, and σ20.σ14

contains an Asucceeded by a D; between these entries there is no B

such that the antecedent pattern of respective CRG (cf. Figure 3A)

matches. Furthermore, the consequence pattern also matches since σ14

contains an entry of the required Cbetween Aand D. With a Band

no Athe two traces σ19 and σ20 allow for mappings of the antecedent

pattern. Further, both traces contain a Dnot preceded by C(while

Cin σ20 succeeds the D,σ19 contains no Cat all); i.e., both traces

allow for a suitable mapping of the consequence pattern, and are thus

compliant with the CRG from Figure 3B.

Finally, let us consider the non-compliant traces σ17, σ18, σ23, and

σ24. Regarding Figure 3A and trace σ17, the antecedence pattern can

be mapped to the trace entries Aand D, since the Bis not in between;

however, the consequence pattern cannot match since σ17 contains no

10 Knuplesch, Reichert

C. Trace σ18 even enables two matches of the antecedent pattern of the

CRG from Figure 3A: the first one consists of the Aand the Din the

middle, while the second match consists of the same Aand the Dat the

end. Since the latter is preceded by C, the second match can be enriched

with a suitable mapping of the consequence pattern. Nevertheless, trace

σ18 violates the CRG from Figure 3A, since there is no Cbetween the

Aand the Dof the first mapping. Regarding trace σ23, the antecedent

pattern maps to the B, but the Dof the consequence pattern is missing

(i.e., the Cdoes not matter). Indeed, σ24 even contains a D, but this

is preceded by a C; i.e., the consequence pattern cannot map while

the antecedent pattern maps. Hence, σ24 violates the CRG depicted in

Figure 3B.

Example 5 (Modeling Compliance Rules by the Use of CRGs). In Fig-

ure 4, the compliance rules from Table 1 and Table 2 respectively are

re-modeled by means of CRGs.

Antecedent

occurrence

Antecedent

absence

Consequence

occurrence

Consequence

absence

Inform about

risks

Inform about

anesthesia

Send patient to

surgical suite

Discharge

patient Write discharge

letter

Perform

surgery Write discharge

letter

Create surgery

report

Make lab test

Schedule

surgery

Perform

surgery

Schedule

surgery

Perform

surgery

Make

decision

Examine

patient Make

decision

Prepare

patient

c c

Examine

patient

Fig. 4 Representing the Compliance Rules from Tables 1 and 2 as CRGs

3 A-priori Compliance Checking

Once the compliance rules have been modeled (e.g., by using CRGs), com-

pliance of pre-specified process models with those rules can be checked. This

is denoted as a-priori compliance checking since the compliance of processes

Ensuring Business Process Compliance Along the Process Life Cycle 11

with regulations is checked before their execution, i.e., before any process

instance is executed based on the pre-specified process model. According to

Definition 4, a pre-specified process model totally complies with a given com-

pliance rule, if and only if the model solely allows for traces being compliant

with the rule. Further, we define the notions of partial compliance and partial

violation as well as total violation.

Definition 4 (Compliance of Pre-specified Process Model). Let

Sbe a pre-specified process model and let φbe a compliance rule (cf.

Definition 1). Further, let QSS⊆Σ?be the set of all complete traces

producible on S; i.e., σ∈QSSrepresents a completed process instance.

Then:

•S(totally) complies with φ, if and only if all complete traces σbeing

producible on Scomply with φ; i.e., ∀σ∈QSS:φ(σ).

•Spartially complies with φ, if and only if there exists a complete trace

σbeing producible on Sand complying with φ; i.e., ∃σ∈QSS:φ(σ)

•Spartially violates φ, if and only if there exists a complete trace σ

being producible on Sand violating φ; i.e., ∃σ∈QSS:¬φ(σ).

•Sonly partially complies with φ, if and only if Spar-

tially complies with φas well as Spartially violates φ; i.e.,

∃σ1, σ2∈QSS:φ(σ1)∧ ¬φ(σ2)

•S(totally) violates φ, if and only if all complete traces σbeing pro-

ducible on Sviolate φ; i.e., ∀σ∈QSS:¬φ(σ).

In case Stotally complies with φ, for brevity we also use the phrase ”S

complies with φ”. The same applies if Stotally violates φ. In this case

we also say ”Sviolates φ”.

Example 6 illustrates the different notions.

Example 6 (Compliance of a Pre-specified Process Model). Reconsider

the pre-specified process model Smed from Figure 1 and the compliance

rules from Table 1 and Fig. 4 respectively. Process model Smed (to-

tally) complies with compliance rules c2, c5, c6, and c7. It only partially

complies with compliance rules c3and c4, while compliance rule c1is

(totally) violated.

12 Knuplesch, Reichert

One common way to perform a priori checking is the usage of model checking

techniques [5]. These allow for verifying models and systems against temporal

formulas. In this context tools exist that provide efficient implementations of

model checking algorithms. Generally, one can distinguish between explicit

model checking and symbolic model checking . In the context of LTL, explicit

model checking means to first create a state-based automaton that represents

the negated formula. Then, this automaton and the state space of the pro-

cess model are explored in combination. Symbolic model checking, in term,

transforms both the process model and the compliance rule into propositional

logic expressions and then applies a satisfiability check. When applying model

checking to the verification of compliance rules not being modeled in terms

of temporal logic (e.g., compliance rules that are modeled based on CRGs),

these rules first have to be transformed into temporal logic.

4 Compliance Monitoring

Checking business process compliance of a pre-specified process model a pri-

ori at build-time is not always feasible, e.g., if the process model is too large

or compliance rules are too complex or depend on run-time data. Besides,

loosely specified and dynamically evolving processes require support for en-

suring compliance during run-time as well. Hence, compliance monitoring

is required that allows process engineers to control and monitor compliance

rules during the execution of single process instances. However, at the process

instance level it is not sufficient to only consider one snapshot, i.e. to state

whether or not the process instance violates a particular compliance rule at a

certain point in time. On the one hand, the violation of a certain compliance

rule can often be cured later on when the process instance progresses. On the

other hand, there are violations for which no adequate continuation exists.

Hence, Definition 5 not only distinguishes between process instances being

compliant and those violating a compliance rule, but also between curable

and incurable violations of process instances regarding an imposed compli-

ance rule.

Definition 5 (Compliance and Curability of Process In-

stances). Let Ibe a process instance represented by its current trace

σI. Further, the process model based on which Ihas been executed may

not be known. Finally, let φbe a compliance rule. Then:

•Icomplies with φ, if and only if σIcomplies with φ; i.e., φ(σI).

•Iviolates φ, if and only if holds σIviolates φ; i.e., ¬φ(σI).

Ensuring Business Process Compliance Along the Process Life Cycle 13

•Icurably violates φ, if and only ifσIviolates φ, but the execution of

Ican be continued in such a way that the resulting trace complies

with φ; i.e., ¬φ(σI)∧ ∃τ∈Σ?:φ(σIτ).

•Iincurably violates φ, if and only if σIviolates φand any continua-

tion of Iviolates φas well; i.e., ¬φ(σI)∧ ∀τ∈Σ?:¬φ(σIτ).

Example 7 illustrates Definition 5.

Example 7 (Compliance and Curability of Process Instances). Consider

the compliance rules c2,c3and c4from Table 1 (see also Table 2 and

Figure 4). Further, consider the traces σI1and σI2of the running process

instances I1and I2respectively (cf. Figure 5). Obviously, I1violates

c2, while it complies with c3and c4. Further, c2is curably violated,

since σI1can be continued by executing activity Make decision. Finally,

I2complies with c2and c3. However, I2incurably violates c4since

no continuation of σI2contains the activity Inform about anesthesia

preceding Schedule surgery.

σσ

1 Admitpatient 1 Admitpatient

2 Performcheckup 2 Performcheckup

3 Examinepatient 3 Examinepatient

4 Informaboutrisks 4 Informaboutrisks

5 Makedecision

6 Schedulesurgery

I1I

Fig. 5 Snapshots of Instance Traces

In practice, it is not always feasible to only deploy process models being to-

tally compliant; i.e., there may be pre-specified process models that only par-

tially comply with imposed compliance rules. As will be shown in Example 8,

instances of respective pre-specified process model need to be monitored at

run-time to determine whether or not a compliance violation can be cured in

the following. According to this, Definition 6 distinguishes between different

levels of criticality of curable violations.

14 Knuplesch, Reichert

Definition 6 (Temporary and Permanent Compliance Viola-

tions). Let I= (S, σI) be a process instance running on a process

model S. Further, let QSSbe the set of all complete traces producible

on Sand φbe a compliance rule. Then:

•Itemporarily violates φ, if and only if Icurrently violates φ, but any

continuation on Swill comply with φat least at one future point in

time:

Icurably violates φ∧ ∀τ∈Σ?with σIτ∈QSS:

∃υ, ω ∈Σ?with υω =τ∧φ(σIυ).

•Ipotentially violates φtemporarily, if and only if Icurrently violates

φand it holds: On the one hand, Imay be continued in a way such

that it will comply with φat least at one future point in time. On

the other hand, Imay be also continued in a way such that it will

never comply with φagain; i.e.,

Icurably violates φ∧ ∃τ1, τ2∈Σ?: for σIτ1, σIτ2∈QSSit holds:

(∃υ1, ω1∈Σ?with υ1ω1=τ1:φ(σIυ1))∧

(∀υ2, ω2∈Σ?with υ2ω2=τ2:¬φ(σIυ2)).

•Ipermanently violates φ, if and only if Icurrently violates φand

any continuation on Salways violates φ; i.e.,

Icurably violates φ∧ ∀τ∈Σ?with σIτ∈QSS:

∀υ, ω ∈Σ?with υω =τ:¬φ(σIυ).

Example 8 applies Definition 6 to selected process instances.

Example 8 (Persistence of Compliance Violations). Reconsider the

compliance rules c2,c3and c4from Table 1 (see also Table 2 and

Figure 4). Further consider the traces σI3and σI4from Figure 6.

These correspond to the running process instances I3= (Smed, σI3)

and I4= (Smed, σI4), which are executed on the pre-specified process

model Smed from Figure 1.

•Obviously, I3violates c2and c3, while it complies with c4. Further, c2

is only temporarily violated by I3, since its continuation on Smed will

lead to the execution of Make decision (e.g., σI2and σI4). However, c3

is potentially temporarily violated, since Smed allows σI3continuing

with activity Inform about risks (e.g., σI1and σI2) or without activity

Inform about risks (e.g. σI4).

Ensuring Business Process Compliance Along the Process Life Cycle 15

•I4violates c3, but complies with c2and c4. Further, c3is permanently

violated by I4, since no continuation of I4on Smed will contain the

required activity Inform about risks.

σσ

1 Admitpatient 1 Admitpatient

2 Performcheckup 2 Performcheckup

3 Examinepatient 3 Examinepatient

4 Informaboutanesthesia

5 Makedecision

6 Schedulesurgery

I3I

Fig. 6 Additional Snapshots of Process Instance Traces

5 A-posteriori Compliance Checking

Instead of ensuring compliance a priori (i.e., by checking pre-specified process

models at build-time) or monitoring it during processes execution, compli-

ance may be also checked for completed process instances a-posteriori; e.g.,

to determine whether these completed instances comply with newly emerg-

ing regulations. Compliance of completed process instances can be directly

decided based on the definition of compliance rules (cf. Definition 1).

Example 9 illustrates a-posteriori compliance checking.

Example 9 (Compliance of Process Execution Logs). Consider the com-

pliance rules c1,c2,c3,c4,c5,c6, and c7from Table 1 (see also Table 2

and Figure 4). Further consider the execution traces σI5,σI6and σI7

from Figure 7, which correspond to the completed process instances I5,

I6and I7.I5violates c1and c4, and complies with c2,c5,c6, and c7.

Further, I6complies with ci,i= 1 . . . 7 and I7violates c1and c3, but

complies with c2,c4,c5,c6, and c7.

Similar to a-priori compliance checking, a-posteriori compliance checking can

be realized based on techniques that build on model checking. The approach

described in [7] transforms LTL-based compliance rules into state-based au-

tomata. Taking an execution log as input, these automata allow deciding

16 Knuplesch, Reichert

σσσ

1 Admitpatient 1 Admitpatient 1 Admitpatient

2 Performcheckup 2 Performcheckup 2 Performcheckup

3 Examinepatient 3 Examinepatient 3 Examinepatient

4 Informaboutrisks 4 Informaboutrisks 4 Informaboutanesthesia

I5I

5 Makedecision 5 Makedecision 5 Makedecision

6 Schedulesurgery 6 Writedischargeletter 6 Schedulesurgery

7 Checkpatientrecod 7 Checkpatientrecod

8 Admitpatient 8 Admitpatient

9 Sendpatienttosurgicasuite 9 Sendpatienttosurgicasuite

10 Performsurgery+ 10 Preparepatient

11 Preparepatient 11 Performsurgery+

12 Transportpatienttoward 12 Transportpatienttoward

13 Createsurgeryreport 13 Providepostsurgicalcare

14 Makelabtest 14 Makelabtest

15 Providepostsurgicalcare 15 Createsurgeryreport

16 Dischargepatient 16 Dischargepatient

17 Writedischargeletter 17 Writedischargeletter

Fig. 7 Execution Traces of Completed Process Instances

whether a completed process instance complies with the original rule or vio-

lates it.

6 Effects of Process Changes on Compliance

As discussed in [8, 9], pre-specified process models as well as process in-

stances running on them may have to be changed and adapted. Obviously,

such changes can affect compliance of the process models and process in-

stances, respectively, with the imposed compliance rules. Depending on the-

ses effects, we define compliance of changes with a given compliance rule (cf.

Definition 7).

Definition 7 (Compliance of Changes). Let Sbe a pre-specified

process model and let I= (S, σI) be a related process instance. Further,

let ∆be a change that correctly transforms the pre-specified process

model Sinto another pre-specified process model S0. Finally, let I=

(S, σI) be correctly migratable to S0, i.e., I= (S0, σI). Then:

•The application of ∆to Smeets compliance rule φ, if and only if the

application of ∆to Sdoes not weaken the compliance of Swith φ;

i.e.,

–Scomplies with φ⇒S0complies with φ.

–Spartially complies with φ⇒S0partially complies with φ.

Ensuring Business Process Compliance Along the Process Life Cycle 17

•The application of ∆to I= (S, σI) meets compliance rule φ, if and

only if the application of ∆to process instance Idoes not weaken

the compliance of Iwith φ; i.e.,

–I= (S, σI) complies with φ⇒(S0, σI) complies with φ.

–I= (S, σI) temporarily violates φ⇒

(S0, σI) temporarily violates φ∨(S0, σI) complies with φ.

–I= (S, σI) potentially violates φtemporarily ⇒

(S0, σI) potentially violates φtemporarily ∨(S0, σI) temporarily

violates φ∨(S0, σI) complies with φ.

Surgical Suite

discharge letter

for referring phys.

Outpatient DepartmentSurgical Ward

MTAPhysicianPhysicianNurse

Admit

patient

Perform

checkup

Examine

patient Inform about

risks

Inform about

anesthesia Make

decision

Check

patient record

Admit

patient

Schedule

surgery

Write

discharge letter

Write

discharge letter

Make

lab test

Create

surgery report

Provide

postsurgical care

Discharge

patient

patient referral

to hospital

Transport

patient to ward

surgery

Perform

surgery

Prepare

patient

Send patient

to surgical suite

Δ1:

delete (S, Schedule surgery)

Δ2:

delete (S, inform about risks)

Fig. 8 Changes Potentially Affecting the Compliance of Process Model Smed

σσ

1 Admitpatient 1 Admitpatient

2 Performcheckup 2 Performcheckup

3 Examinepatient 3 Examinepatient

4 Informaboutanesthesia

I8I

Fig. 9 Further Examples for Snapshots of Process Instance Traces

When applying Definition 7 in a straightforward manner, one would have

to re-check compliance of a process model with all defined compliance rules

whenever changing this model. This might become necessary in the context

of ad-hoc adaptations of single process instances or changes of a pre-specified

process models solely at the process type level (i.e., without propagating

the type change to already running process instances). However, re-checking

business compliance for large collections of running process instances might

be too expensive. More precisely, for each of these hundreds up to thousands

of process instances it has to be determined whether or not it still meets the

18 Knuplesch, Reichert

imposed compliance rules when migrating the process instance to the new

process model version. To cope with this challenge, changes and compliance

rules have to be analyzed (e.g., by considering the affected activities) in order

to restrict the set of compliance rules to be re-checked.

Example 10 (Effects of Changes on Process Model Compliance). Take

compliance rules c4and c5from Table 1 (see also Table 2 and Fig-

ure 4) and consider change ∆1of the pre-specified process model Smed

as depicted in Figure 8. Obviously, ∆1meets c4. While Sonly partially

complies with c4,S0totally complies with this rule. By contrast, ∆1vi-

olates c5since Stotally complies with c5, but S0only partially complies

with this rule.

Example 11 (Effects of Changes on Process Instance Compliance). Con-

sider now compliance rule c3from Table 1 (see also Table 2 and Figure 4)

and change ∆2from Figure 8 that transforms Smed into S0

med. Further,

consider the process instances I8= (Smed, σI8) and I9= (Smed, σI9)

from Figure 9 that both depend on the pre-specified process model Smed

from Figure 1. Regarding I8,∆2violates c3:I8= (Smed, σI8) potentially

violates c3temporarily, whereas (S0

med, σI8) permanently violates this

rule. However, regarding I9,∆2meets c3since I9= (Smed, σI9) perma-

nently violates c3which also applies to (S0

med, σI9) permanently.

7 User Perspective

This section gives an idea how compliance checking looks like from the per-

spective of the user. Currently, only few tools exist that allow ensuring busi-

ness process compliance at the process type or the process instance level. One

of them is the SeaFlows Toolset [10], which provides a comprehensive and ex-

tensible framework for checking business compliance of pre-specified process

models. For this purpose, the SeaFlows Toolset provides a user-friendly en-

vironment. For modeling compliance rules SeaFlows uses CRGs as presented

in Section 2.

The SeaFlows Toolset allows enriching process models with these rules and

checking for compliance with them. Furthermore, compliance checking con-

siders data as well as efficiency issues by applying a number of abstraction

strategies. Finally, violations of compliance rules are illustrated by means of a

Ensuring Business Process Compliance Along the Process Life Cycle 19

Fig. 10 Modeling Compliance Rules with the SeaFlows Graphical Editor

counter example (cf. Figure 11). At the technical level the applied compliance

checking approach uses the model checker SAL [11].

original

process graph

counterexample as

process graph

counterexample

as process log

data-aware

compliance rules

visualization of the

counterexample’s steps

Fig. 11 Compliance Checking with the SeaFlows Toolset

Additionally, a structural compliance checking approach is delivered. It first

derives structural criteria from compliance rules. Then it applies those cri-

20 Knuplesch, Reichert

teria to check business process compliance of cycle-free process models (cf.

Figure 12).

Fig. 12 Structural Compliance Checking with the SeaFlows Toolset

8 Existing Approaches Enabling Business Process

Compliance

Existing approaches enabling business process compliance follow different

paradigms to model compliance rules. In first position there are approaches

using temporal logic. For example, the work discussed in [12] applies LTL

and the one presented in [13] applies CTL for modeling compliance rules.

Further, these approaches apply model checking for enabling a priori com-

pliance checking. Other logic-based approaches consider the modalities of

compliance rules (e.g., obligations or permissions) and use deontic logic as

formal basis [14, 15]. As discussed in Section 2, however, logic expressions are

less comprehensible to end users. To improve this situation, a pattern-based

notation is suggested by Dwyer et al. in [16]. Finally, several approaches use

graphical notations (including CRGs) [6, 17, 12].

Model checking is the most common technique for verifying compliance rules

(e.g. [13, 17, 12, 18]). However, model checking depends on the exploration of

the state space of pre-specified process models. In particular, the state space

Ensuring Business Process Compliance Along the Process Life Cycle 21

explosion problem constitutes a big obstacle for the practical use of model

checking techniques. To tackle this challenge, techniques like graph reduction

and sequentialization of parallel flows as well as predicate abstraction are

applied [12, 17, 19]. Besides model checking, there exist other techniques

ensuring business process compliance a priori. For cycle-free process models,

for instance, [20] and [21] provide efficient algorithms.

Generally, compliance rules should not be restricted to the behavior perspec-

tive, but be applicable to other perspectives of a PAIS as well (e.g., the infor-

mation or time perspectives). Compliance checking of process models having

state-based data objects (i.e., enumerations), for instance, is suggested by

Awad et al. [22]. Further, [19] enables data-aware compliance checking for

larger data types (e.g., integers or reals). The verification of cycle-free pro-

cess models against temporal compliance rules is addressed by Eder et al.

[23], while [18] considers both the information and the time perspective.

9 Summary

This report dealt with issues related to business process compliance. Compli-

ance can be checked a-priori for pre-specified process models as well as for

running process instances or completed ones (i.e., execution logs). For each of

these artifacts it can be verified whether or not it complies with compliance

rules imposed from regulations, laws and guidelines. This report presented

two ways for modeling compliance rules: LTL and CRGs. It first discussed

how to apply a-priori compliance checking to pre-specified process models

and then gave insights into compliance monitoring and different kinds of

compliance violations including compliance checking. Following this, it dis-

cussed the potential impact of process changes (at both the type and the

instance level) on business process compliance. Finally, the report discussed

the user perspective as well as recent approaches enabling business process

compliance.

References

1. Weske, M.: Workflow management systems: Formal foundation, conceptual design, im-

plementation aspects. Habilitation Thesis, University of M¨unster, Germany. Springer

(2007)

2. van der Aalst, W.M.P.: The application of petri nets to workflow management. Journal

of Circuits, Systems, and Computers 8(1) (1998) 21–66

3. Weber, B., Reichert, M., Rinderle-Ma, S., Wild, W.: Providing integrated life cycle

support in process-aware information systems. Int. Journal of Cooperative Information

Systems (IJCIS) 18(1) (2009) 115–165

22 Knuplesch, Reichert

4. Reichert, M., Dadam, P.: ADEPTflex – supporting dynamic changes of workflows

without losing control. Journal of Intelligent Information Systems, Special Issue on

Workflow Management Systems 10(2) (1998) 93–129

5. Huth, M., Ryan, M.: Logic in Computer Science: Modelling and reasoning about

systems. Cambridge University Press (2004)

6. Ly, L.T., Rinderle-Ma, S., Dadam, P.: Design and verification of instantiable com-

pliance rule graphs in process-aware information systems. In: Proc. 22nd Int. Conf.

Advanced Systems Engineering (CAiSE’10), Springer (2010) 9–23

7. van der Aalst, W.M.P., de Beer, H., van Dongen, B.: Process mining and verification

of properties: An approach based on temporal logic. In: Proc. 13th Int. Conf. Coop.

Inf. Systems (CoopIS’05), Springer (2005) 130–147

8. Weber, B., Sadiq, S., Reichert, M.: Beyond rigidity – dynamic process lifecycle support.

Computer Science – Research and Development 23(2) (2009) 47–65

9. Reichert, M., Rinderle-Ma, S., Dadam, P.: Flexibility in process-aware information

systems. Transactions on Petri Nets and Other Models of Concurrency II 2(2009)

115–135

10. Ly, L., Knuplesch, D., Rinderle-Ma, S., G¨oser, K., Pfeifer, H., Reichert, M., Dadam,

P.: Seaflows toolset – compliance verification made easy for process-aware information

systems. In: Proc. CAISE’10 Forum - Information Systems Evolution. (2011) 76–91

11. Bensalem, S., et al.: An overview of SAL. In: Proc. of the 5th NASA Langley Formal

Methods Workshop, NASA Langley Research Center (2000) 187–196

12. Awad, A., Decker, G., Weske, M.: Efficient compliance checking using BPMN-Q and

temporal logic. In: Proc. 6th Int. Conf. Business Process Management (BPM’08),

Springer (2008) 326–341

13. Ghose, A.K., Koliadis, G.: Auditing business process compliance. In: Proc. 5th Int.

Conf. Service-Oriented Computing (ICSOC’07), Springer (2007) 169–180

14. Alberti, M., et al.: Expressing and verifying business contracts with abductive logic

programming. In: Proc. 2nd Int. Conf. Normative Multi-agent Systems (NorMAS’07).

Dagstuhl Seminar Proceedings (2007)

15. Goedertier, S., Vanthienen, J.: Designing compliant business processes with obligations

and permissions. In: Proc. BPM’06 Workshops, Springer (2006) 5–14

16. Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Property specification patterns for finite-

state verification. In: Proc. 2nd Workshop Formal Methods in Software Practice

(FMSP’98), ACM (1998)

17. Liu, Y., M¨uller, S., Xu, K.: A static compliance-checking framework for business

process models. IBM Systems Journal 46(2) (2007) 335–261

18. Kokash, N., Krause, C., de Vink, E.: Time and data aware analysis of graphical

service models. In: Proc. 8th Int. Conf. Software Engineering and Formal Methods

(SEFM’10), IEEE Computer Society (2010)

19. Knuplesch, D., Ly, L., Rinderle-Ma, S., Pfeifer, H., Dadam, P.: On enabling data-aware

compliance checking of business process models. In: Proc. 29th Int. Conf. Conceptual

Modeling (ER’2010), Springer (2010)

20. Governatori, G., Milosevic, Z., Sadiq, S.: Compliance checking between business pro-

cesses and business contracts. In: Proc. 10th Int. Enterprise Distributed Object Com-

puting Conf. (EDOC’06), IEEE Computer Society (2006) 221–232

21. Weber, I., Hoffmann, J., Mendling, J.: Semantic business process validation. In: Proc.

3rd Int. workshop on Semantic Business Process Management (SBPM’08). (2008)

22. Awad, A., Weidlich, M., Weske, M.: Specification, verification and explanation of

violation for dataaware compliance rules. In: Proc. of 7th Int. Conf. Service Oriented

Computing (ICSOC’09), Springer (2009) 500–515

23. Eder, J., Tahamtan, A.: Temporal conformance of federated choreographies. In: Proc.

19th Int. Conf. Database and Expert Sys. App. (DEXA’08), Springer (2008) 668–675