On the Formal Semantics of the Extended Compliance Rule Graph [original]

On the Formal Semantics of the Extended

Compliance Rule Graph ⋆

David Knuplesch1, Manfred Reichert1, Linh Thao Ly1, Akhil Kumar2, and

Stefanie Rinderle-Ma3

1Institute of Databases and Information Systems, Ulm University, Germany

david.knuplesch,manfred.reichert,[email protected]

2Smeal College of Business, Pennsylvania State University, PA, USA

[email protected]

3Faculty of Computer Science, University of Vienna, Austria

[email protected]

Abstract. A fundamental challenge for any process-aware information

system is to ensure compliance of modeled and executed business pro-

cesses with imposed compliance rules stemming from guidelines, stan-

dards and laws. Such compliance rules usually refer to multiple process

perspectives including control flow, data, time, and resources as well

as interactions with business partners. On one hand, compliance rules

should be comprehensible for domain experts who must define and ap-

ply them. On the other, compliance rules should have precise semantics

such that they can be automatically processed. In this context, providing

a visual compliance rule language, which hides formal details from rule

designers, is crucial in order to enable an intuitive way of modeling. So

far, visual compliance rule languages have focused on the control flow

perspective, but lack adequate support for the other perspectives. To

remedy this drawback, this report introduces the extended Compliance

Rule Graph language and its formal semantics.

Keywords: business process compliance, compliance rule graphs, busi-

ness process modeling, business intelligence, formal semantics

1 Introduction

During the last decade, numerous approaches for ensuring the correctness of

business processes have been discussed [2–5]. Most of them focus on syntac-

tical correctness and process model soundness (e.g., absence of deadlocks and

lifelocks). However, business processes must also comply with semantic rules

stemming from domain-specific requirements such as corporate standards, le-

gal regulations, guidelines or best practices [6, 7]. Summarized under the no-

tion of business process compliance, existing approaches have mostly considered

⋆This work was done within the research project C3Pro funded by the German Re-

search Foundation (DFG), Project number: RE 1402/2-1, and the Austrian Science

Fund (FWF) under project number: I743. Parts of this technical report will be pub-

lished in [1].

2 Knuplesch, Reichert, Ly, Kumar, Rinderle-Ma

compliance issues related to the control flow perspective of single processes. In

turn, only a few approaches consider the data, resource, and time perspectives

in this context, although they are crucial as well [8–11]. Furthermore, cross-

organizational scenarios characterized by interacting and collaborating business

processes of various parties have not been properly considered so far [12]. In this

context, compliance requirements need to be specified for both local and global

processes as well. Note that this requires to consider the data, resource, and time

perspectives as well as interactions between business partners (i.e. messages ex-

changed) as well. As examples consider the compliance rules in Table 1, which

are imposed on a cross-organizational process scenario involving the two business

partners reseller and manufacturer. In particular, as shown by the highlighted

terms in Table 1, compliance rules may refer to the data, time, and resource per-

spectives of business processes as well as to interactions with business partners.

Compliance rule c1refers to the interactions between a reseller and manufac-

turer (request and reply) after a particular point in time (3rd January, 2013) as

well as the maximum time distance between them (within three days). In turn,

the data perspective of compliance rules is emphasized by compliance rule c2

of the manufacturer. It forbids changing an order after having started the cor-

responding production task. Compliance rule c3combines the interaction, time,

and data perspectives. Finally, compliance rule c4introduces the resource per-

spective (member of the order processing department and another member of

the same department with supervisor status). In addition, c4considers the data

perspective (e.g. new customer and total amount greater than e5,000) and the

time perspective (at most three days). Particularly, c4shows that the different

perspectives might be relevant for the same rule and hence must not be consid-

ered in an isolated manner.

When comparing c4and c2with c1and c3, one can observe two different view-

points: c4and c2are expressed from the viewpoint of the manufacturer (i.e.,

local view), whereas c1and c3reflect a global view. Note that such distinction

Table 1: Examples of compliance rules for order-to-delivery processes

c1Any request sent from the reseller to the manufacturer after January 3rd, 2013

should be replied by the manufacturer within three days.

c2After starting the production related to a particular order, the latter must not

be changed anymore.

c3When the manufacturer sends a bill with an amount lower than e5,000 to the

reseller, the latter must make the payment within 7 days.

c4After receiving a production request message from the reseller, which refers to

anew customer and has a total amount greater than e5,000, the solvency of

this customer must be checked by a member of the order processing department.

Based on the result of this check, another member of the same department with

supervisor status must approve the request. Finally, the approval result must be

sent to the reseller at most three days after receiving the original request.

On the Formal Semantics of the Extended Compliance Rule Graph 3

between local and global views is common to cross-organizational collaboration

scenarios not only in the context of process compliance [12, 13]. For example,

BPMN 2.0 provides collaboration and choreography diagrams to express these

different viewpoints.

Several approaches for formally capturing compliance requirements at different

abstraction levels (e.g., temporal logics [14]) exist. In particular, they also enable

the automatic verification of the conformance of business processes with respec-

tive compliance rules. As the use of formal languages for specifying compliance

rules would be too intricate, rule patterns hiding formal detail from rule mod-

elers have been proposed [9, 11]. Furthermore, a few approaches also consider

more advanced issues like, for example, the use of data conditions in the context

of compliance requirements. However, existing approaches are usually restricted

to a specific subset of rule patterns. In turn, languages employing visual nota-

tions, like the compliance rule graph approach [15] or BPSL [16], combine an

intuitive notation with the advantages of a formal language. However, the meta-

analyses and case studies, we conducted in domains like higher education [17],

medicine [18–21] and automotive engineering [22, 23], have revealed that these

visual compliance rule languages still lack support for the time, data, and re-

source perspective of business processes and do not consider cross-organizational

scenarios with interacting partners [12]. Overall, the following fundamental re-

quirements for visual compliance rule languages need to be considered:

–In addition to the control flow perspective, the data, resource and time per-

spectives of compliance requirements must be properly captured.

–To not only consider process orchestrations, but cross-organizational scenar-

ios as well, it becomes necessary to integrate the interaction perspective with

compliance rule languages as well.

–To provide tool support for both the modeling and verification of compliance

rules, both their syntax and semantics must be formalized.

To cope with the discussed shortcomings, this report introduces the extended

Compliance Rule Graph (eCRG) and its formal semantics. The eCRG builds on

the Compliance Rule Graph (CRG) language developed in previous work [15, 24],

but additionally comprises elements enabling the visual modeling of compliance

rules with the support of the process, data, time, and resource perspectives. Fur-

thermore, we introduce concepts that allow defining compliance rules in respect

to message flows and partner interactions; i.e., the eCRG language is able to

specify compliance requirements for cross-organizational process scenarios (i.e.

processes choreographies). For defining the formal semantics of the eCRG, we

provide a transformation into FOL formula. Note that the latter can be evaluated

over process traces to a posteriori verify the compliance of business processes.

Altogether, the eCRG allows capturing compliance requirements at an abstract

level, while enabling the specification of verifiable compliance rules in the context

of cross-organizational scenarios, including the process, data, time, and resource

perspectives.

4 Knuplesch, Reichert, Ly, Kumar, Rinderle-Ma

The remainder of this report is structured as follows: Section 2 discusses re-

lated work. Section 3 introduces the extended Compliance Rule Graph (eCRG).

The formal semantics of the eCRG language is specified in Section 4, whereas

Section 5 provides a pattern-based evaluation. Finally, Section 6 concludes the

report and provides an outlook on future research.

2 Related Work

During the last years the interaction, time, resource, and data perspectives have

been considered in business process modeling in addition to the control flow

perspective (e.g., [25–33]).

The integration of business process compliance throughout the entire process

lifecycle has been discussed in [24, 34–36]; [37] examined compliance issues in

the context of cross-organizational processes developing a logic-based formalism

for describing the semantics of normative specifications as well as compliance

checking procedures. This approach allows modeling business obligations regu-

lating the execution of business processes. In turn, [38] introduced a semantic

layer that interprets process instances according to an independently designed

set of internal controls. Furthermore, there exist approaches using semantic an-

notations to ensure compliance [39]. An approach for checking the compliance of

process models against semantic constraints as well as for ensuring the validity

of process change operations based on Mixed-Integer Programming formulation

is proposed in [40]. It introduces the notions of degree of compliance,validity

of change operations, and compliance by compensation. Further, [9] uses align-

ments to detect compliance violations in process logs. To verify whether compli-

ance rules are fulfilled by process models at design time, many approaches apply

model checking techniques [14, 16, 41–44]; some of them address the data and

time perspectives as well. In order ensure compliability and global compliance

of cross-organizational processes, where partners only provide restricted views

on their local processes, [45, 46] apply model checking as well. Other approaches

for verifying compliance apply the notion of semantic congruence [47] or use

petri-nets [48] and consider the data and time perspectives as well.

The approach described in [41, 49] for visually modeling compliance considers the

control flow and data perspectives. It is based on linear temporal logic (LTL),

which allows modeling the control flow perspective based on operators like next,

eventually,always, and until. Other visual approaches for compliance rule mod-

eling [15, 16, 50] focus on control flow and partially the data perspective, but

ignore the other perspectives mentioned.

3 Extended Compliance Rule Graphs

This section introduces extended Compliance Rule Graphs (eCRG) – a visual

notation for compliance rule modeling covering the process, interaction, time,

resource, and data perspectives. Secion 3.1 introduces fundamentals of CRGs.

Its extensions are introduced stepwise in Sections 3.2–3.6.

On the Formal Semantics of the Extended Compliance Rule Graph 5

3.1 Fundamentals of Compliance Rule Graphs

The compliance rule graph (CRG) language [15, 24] allows visually modeling

compliance rules whose semantics is defined over event traces. More precisely, a

CRG is an acyclic graph consisting of an antecedence pattern as well as at least

one related consequence pattern. Both patterns are modeled using occurrence and

absence nodes, which indicate the occurrence or absence of events (e.g., related

of the execution of a particular task). Edges between such nodes indicate control

flow dependencies. As illustrated in Fig. 1, a trace is considered as compliant

with a CRG iff for each match of the antecedence pattern there is at least

one corresponding match of every consequence pattern. Furthermore, a trace is

considered as trivially compliant iff there is no match of the antecedence pattern.

For example, the CRG from Fig. 1 expresses that for each Bnot preceded by

an A, there must occur a D, which is not preceded by any Calso preceding the

corresponding B.

C D C D

Antecedence pattern Consequence pattern

only match < E, D, F, G, B >

only match < D, F, C, E, B >

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

only match < C, F, B, G, E >

1st match < B, C, D, E, B >

2nd match< B, C, D, E, B >

< E, D, F, G, B >

< D, F, C, E, B > (C is after D!)

no match (missing D)

< B, C, D, E, B >

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

A B A B A B

< E, D, F, G, B >

< D, F, C, E, B >

< A, B, C, E, D >

< C, F, B, G, E >

< B, C, D, E, B >

compliant

trivially compliant

violation

Antecedence

Occurrence

Antecedence

Absence

Consequence

Absence

Consequence

Occurrence

CRG

Fig. 1: CRG example and semantics over execution traces

In the following sections, we introduce the extended Compliance Rule Graph

(eCRG) language, which is based on CRGs. In addition to using nodes and

connectors (i.e., edges), eCRG allows for attachments. The latter represent con-

straints to the nodes or edges they are attached to. Furthermore, an eCRG may

contain instance nodes representing particular instances, which exist indepen-

dently from the respective rule (e.g. a particular employee Mr. Smith, date 3rd

January 2013, or role supervisor). Accordingly, instance nodes are neither part

of the antecedence nor the consequence pattern.

3.2 Process Perspective

We first consider the process (i.e., control flow) perspective. The eCRG elements

for modeling the process (i.e. control flow) perspective of compliance rules are in-

troduced in Fig. 2. Since the extensions are based on the CRG language, there ex-

ist four different task elements, i.e., antecedence occurrence,antecedence absence,

consequence occurrence, and consequence absence tasks. These allow expressing

whether or not particular tasks must be executed. In addition, two different

kinds of sequence flow connectors are provided that may be used to constrain

6 Knuplesch, Reichert, Ly, Kumar, Rinderle-Ma

Performer

Task

Performer

Task

Tasks Nodes – Local View

Antecedence Consequence

OccurenceAbsence

Task Task

Task

Tasks Nodes – Interaction View

Antecedence Consequence

OccurenceAbsence

Performer

Task

Performer

Sequence Exclusion

Antecedence Connectors

Sequence Exclusion

Consequence Connectors

Alternative

Fig. 2: eCRG elements of the process perspective

the execution sequence of tasks. Note that the absence of sequence flow indicates

a parallel flow. To clearly distinguish between start-start,start-end,end-start,

and end-end constraints on the execution sequence of tasks, sequence flow edges

are either connected to the right or left border of a task node. Furthermore,

exclusive connectors allow modeling mutual excluding tasks. Alternative con-

nectors, in turn, express that at least one of the connected tasks must occur.

Note that exclusive as well as alternative connectors may only connect nodes

that are either part of the antecedence or the consequence pattern.

Fig. 4A shows an example of a start-start constraint on the execution sequence

of tasks. It depicts the process perspective of compliance rule c2from Table 1

that disallows executing task change order after task production is started.

3.3 Interaction Perspective

The interaction perspective of business processes is crucial in cross-organizational

scenarios [51, 13]. It covers constraints on the messages exchanged between busi-

ness pratners and the interaction view of the eCRG meta-model. Message ex-

changes are expressed in terms of particular nodes that reflect the events of

sending and receiving a message. In turn, a message flow denotes the depen-

dency between the events representing the sending and receiving of a particular

message (cf. Fig. 3).

Antecedence Consequence Antecedence Consequence

Sender

Message

Receiver

Sender

Message

Receiver

Sender

Message

Receiver

Sender

Message

Receiver

Antecedence Consequence

OccurenceAbsence

Antecedence

Message Flow

Connector

Consequence

Message Flow

Connector

Interaction Nodes – Interaction ViewMessage Nodes – Local View

Sender

Receiver Message

Message

Sender

Message

Receiver

Message

Sender

Receiver Message

Message

Sender

Message

Receiver

Message

ReceiveSend

OccurenceAbsence

Fig. 3: eCRG elements of the interaction perspective

On the Formal Semantics of the Extended Compliance Rule Graph 7

Production

Change

Order

Reseller

Check

Solvency Approval

Request

A B

Fig. 4: Local view on c2and c4with process and interaction perspectives

Reseller

Request

Manufacturer

Reseller

Manufacturer

Billing

Information

Reseller

Payment

Reseller

Fig. 5: Interaction view on c1and c3with process and interaction perspectives

In Fig. 4B, the elements from Fig. 3 are used to model the process and inter-

action perspective of compliance rule c4. This rule requires that after receiving

message request from a reseller, a solvency check must be performed first. Then,

a decision about approval has to be made before replying the request. Although

the rule modeled in Fig. 4B considers the interaction perspective, using the two

message nodes request and reply, it still represents the view of a particular busi-

ness partner on its local business processes. We refer to this traditional point

of view as the local view of a compliance rule. However, when considering the

compliance rules c1and c3from Table 1, one can easily discover a global point

of view on cross-organizational processes and related interactions (i.e., the mes-

sages exchanged) that corresponds to the BPMN 2.0 choreography diagram. In

this interaction view, interaction nodes (cf. Fig. 3) are used to denote the ex-

change of a message between two business partners. Since the interaction view

spans multiple business partners, task nodes may be annotated with the the

business partner responsible (cf. Fig. 2).

Fig. 5A provides an interaction view on compliance rule c1from Table 1: After

the reseller sends a request to the manufacturer, eventually, the manufacturer

must reply. Furthermore, Fig. 5B provides an interaction view on compliance rule

c3from Table 1. This rule requires that the reseller must perform task payment

after having received billing information from the manufacturer.

3.4 Time Perspective

The time perspective of a business process deals with temporal constraints that

need to be obeyed by instances of the process [28, 29].

Having a closer look on the original definition of compliance rules c1and c3

from Table 1, it becomes clear that the eCRGs from Figs. 5A and 5B do not

fully specify them yet. In particular, the time distances between the interactions

and tasks have not been modeled. Fig. 6 provides elements for modeling points

in time and time conditions in compliance rules. The latter may be attached to

task nodes as well as sequence or message flow connectors to either constrain the

duration of a task or the time distance between tasks, messages or points in time.

Additionally, time distance connectors are introduced that must be attached

8 Knuplesch, Reichert, Ly, Kumar, Rinderle-Ma

Occurence

Anteced.

Points

in Time

Antecedence

Consequence

Time

Conditions

>2d

Anteced. Sequence

Distance Connector

Consequ. Sequence

Distance Connector

Absence

March 23th

2013

Particular

Point in TimeConsequ.

Fig. 6: eCRG elements of the time perspective

Reseller

Request

Manufacturer

Reseller

< 3 days

Jan 3rd

2013

Manufacturer

Billing

Information

Reseller

Payment

Reseller

< 7days

A B

Fig. 7: Interaction view on c1and c3with process, interaction and time perspec-

tives

with a time condition. Respective time distance connectors and related time

conditions then allow constraining the time distance between tasks, messages or

points in time without implying a particular sequence.

Fig. 7A combines the interaction and time perspectives of compliance rule c1.

This visual representation of c1covers exactly the semantics of the compliance

rule described in Table 1. In Fig. 7B, the interaction and time perspectives of

c3are provided. This compliance rule requires that at most seven days after the

manufacturer sends billing information to the reseller, the latter must perform

task payment.

3.5 Resource Perspective

The resource perspective covers the different kinds of human resources as well

as their inter-relations [25, 52]. Further, it allows constraining the assignment of

resources to tasks. In the context of our work, we consider resources like staff

member,role,group, and organizational unit as well as their relations to tasks.

Furthermore, we support resource conditions and relations among resources (cf.

Fig. 8). Similar to task nodes, resource nodes may be part of the antecedence

or consequence patterns. Alternatively, they may represent a particular resource

instance (e.g. staff member Mr. Smith, or role supervisor). In turn, resource

conditions may constrain resource nodes. Furthermore, the performing relation

indicates the performer of a task. Finally, resource relation connectors express

relations between resources. Note that the resource perspective can be easily

extended with other kinds of resources if required.

Fig. 9 combines the process, interaction, time, and resource perspectives of com-

pliance rule c4. This rule requires that at least three days after receiving a request

of the reseller, a replay must be sent to him. Before sending this reply, first of

all, task solvency check must be performed by a staff member assigned to the

particular organizational unit order processing department. Following this task,

another staff member of the same department with supervisor status (i.e., role)

must decide whether to grant approval before sending the reply.

On the Formal Semantics of the Extended Compliance Rule Graph 9

< value

> value

Antecedence

Consequence

Data/Resource Conditions

Data

Object

Data

Object

Data Nodes

AntecedenceConsequence

Antecedence

Data Flow Connector

Consequence

Data Flow Connector

Group Organizational

Unit

Staff

Member

Role

Group Organizational

Unit

Staff

Member

Role

Resource Nodes

Antecedence

Performing and

Relation Connector

Consequence

Performing and

Relation Connector

( )

Data Container

Requests

Request

from

Mrs Ly

Particular

Resources

Quality

Managers

Dept. Information

Systems

Mr Knup

Computer

Scientist

Fig. 8: eCRG elements of the resource and data perspectives

Supervisor

Reseller

Request

Reseller

Check

Solvency Approval

< 3 days

≠

Order

Processing

Department

assigned is

assigned

Fig. 9: Local view on c4with process, interaction, time, and resource perspectives

3.6 Data Perspective

The data perspective of business processes covers the data objects processed

as well as the data flow between the tasks of the process [32, 53, 33]. Fig. 8

introduces eCRG elements for modeling data containers and data objects as well

as connectors representing data flow. Thereby, data containers refer to process

data elements or global data stores. By contrast, data objects refer to particular

data values and object instances. Similar to resource nodes, data nodes may be

part of the antecedence or consequence pattern, or represent a particular data

container or data object (e.g., data container student credit points, document 1st

order from Mr. Smith). Furthermore, data flow defines which process tasks read

or write which data objects or data container. To constrain data container, data

objects, and data flow, data conditions may be attached. Finally, data relation

connectors may be used either to compare different data objects or to constrain

the value of data containers at particular points in time.

Figs. 10A-C show the visual modeling of compliance rules c2,c3, and c4covering

the data perspective as well as the other perspectives discussed. Note that each

of the depicted eCRG covers the informal semantics described in Table 1.

10 Knuplesch, Reichert, Ly, Kumar, Rinderle-Ma

Customer

data

Supervisor

Reseller

Request

Reseller

amount > 5000 €

Check

Solvency Approval

< 3 days

Request Approval

Result

new customer?

≠

Order

Processing

Department

assigned

Solvency

result

assigned

Production

Change

Order

Manufacturer

Billing

Information

Reseller

Payment

Reseller

< 7days

Bill

amount < 5000 €

Fig. 10: Local view on c2and interaction view on c3and c4, considering the

process, interaction, time, resource, and data perspectives

4 Formal Semantics of the eCRG

In the previous section, we have only informally described eCRG semantics. In

order to enable automated compliance checking of process logs against eCRG,

however, an unambiguous formal semantics is required. For this purpose, this sec-

tion provides a transformation from eCRG to first-order predicate logic (FOL),

which defines how to interpret and evaluate an eCRG over process logs.

How this transformation can be accomplished is described in the following. First,

Section 4.1 introduces sets representing fundamental business process concepts

(e.g., tasks types, resources, or data values). Second, process logs are formally

defined as set of predicates in Section 4.2. Third, Section 4.3 provides a set-based

formal description of an eCRG. Fourth, Section 4.4 defines the transformation

translating the eCRG into logic formula based on the defined predicates.

4.1 Environmental Sets and Concepts

The eCRG language relates to different perspectives of business processes, i.e.,

the process, time, data, resource, and interaction perspectives. The formalization

of the eCRG language requires a formal definition of theses fundamental concepts

defining the process environment in Def. 1 as follows:

Definition 1 (Process Environment).

The environment of a business process comprises the following sets:

–Tis the set of task types

–Mis set of message types

–Tis the discrete and ordered set of points in time

–R∶=RS∪RR∪RG∪RUis the set of resources, with RSbeing the set of staff members,

RRbeing the set of roles, RGbeing the set of groups, RUbeing the set of business units

and departments.

–Dset of data containers, Pset of activity and message parameters,

–Ωset of data values and objects (e.g. 5,1.345, color red, document-A, report-123, . . . ),

–ITset of task instance identifiers, and

–IMset of message instance identifier.

On the Formal Semantics of the Extended Compliance Rule Graph 11

Further, based on the definition of the environment, we introduce the following sets of conditions

and relations for time, data and resources:

–CT⊆{cont∣cont⊆T→B}is the set of time conditions,

–CD⊆{cond∣cond⊆Ω→B}is the set of data conditions,

–CR⊆{conr∣conr⊆R→B}is the set of resource conditions,

–RT⊆{relt∣relt⊆T2→B}is the set of time relations,

–RD⊆{reld∣reld⊆Ω2→B}is the set of data relations, and

–RR⊆{relr∣relr⊆R2→B}is the set of resource relations.

InStaff ∈RRis a resource relation and InStaff(r, s)indicates that staff member

sbelongs or is assigned to resource r. Furthermore, we do not explicitly distin-

guish between time conditions and time relations, since each time condition cont

constitutes a time relation relcontwith

relcont(t1, t2)∶⇔cont(∣t1−t2∣).

4.2 Process Logs

A common way to capture the execution of a business process is to store exe-

cution events in process logs and traces [2]. Usually, the latter contain multiple

information about the tasks executed, messages exchanged, or data objects ac-

cessed. However, not all logged information is of interest for evaluating whether

or not a particular process instance complies with a given compliance rule. In-

dependent from the concrete format of a process log, we introduce a set of

predicates describing its relevant information in Def. 2. Obviously, the values of

these predicates can be easily derived by processing a concrete process log:

Definition 2 (Execution Log Entries/Predicates).

Let T,M,T,R,D,IT,IMbe defined as in Def. 1. Then, predicate

–Start(t, i, tt)expresses that task i∈ITof type tt ∈Tis started at t∈T.

–End(t, i, tt)expresses that task i∈ITof type tt ∈Tis completed at t∈T.

–Perform(i, s)expresses that task i∈ITwas performed by the staff member s∈RS.

–Receive(t, i, mt, b)expresses that message i∈IMof type mt ∈Mis received from business

partner b∈Bat t∈T.

–Send(t, i, mt, b)expresses that message i∈IMof type mt ∈Mis sent to business partner

b∈Bat t∈T.

–Parameter(i, p, v)expresses that execution parameter p∈Pof task or message i∈IT∪IM

has parameter value v∈Ω.

–Write(t, i, p, v, d)expresses that task or message i∈IT∪IMwrites value v∈Ωto data

container d∈Dvia output parameter p∈Pat t∈T.

–Read(t, i, p, v, d)expresses that task or message i∈IT∪IMreads value v∈Ωto data

container d∈Dvia input parameter p∈Pat t∈T.

Based on predicate Write, we define predicate Value:

Value(t0, o, v)∶⇔∃t1∈T∶t1<t0∧Write(t1,⋅,⋅, v, o)∧∄t2∶t1<t2<t0∧Write(t2,⋅,⋅,⋅, o)

Note that we use dots (⋅) as wildcards, i.e.:

Write(t1,⋅,⋅,⋅, o)⇔∃x1, x2, x3∶Write(t1, x1, x2, x3, o)

12 Knuplesch, Reichert, Ly, Kumar, Rinderle-Ma

4.3 Formal Description of eCRG

We now introduce a set-based formal description of the eCRG. Since the latter

constitutes a graph, it consists of nodes (e.g. task nodes) and edges (e.g. sequence

flow edge). Furthermore, the eCRG nodes and edges may have attachments that

specify additional constraints. Thus, we can roughly define an eCRG as specified

in Def. 3:

Definition 3 (eCRG).

An eCRG Ψis a graph Ψ=(N, E, ◇), where

–Nis the set of nodes,

–Eis the set of edges, and

–◇is the set of attachments to nodes and edges.

As described in Section 3, each element of an eCRG (i.e., node, edge, or attach-

ment) can either be element of the antecedence pattern (A) or the consequence

pattern (C) or be a particular instance (I) (e.g., a particular employee Mr. Smith,

date 3rd January 2013, or role supervisor). In the cases of nodes, the antecedence

pattern is partitioned into the antecedence occurrence pattern (AO) and the an-

tecedence absence pattern (AA), while the consequence pattern is partitioned

into the consequence occurrence pattern (CO) and the consequence absence pat-

tern (CA). Before formally introducing these pattern classes in Def. 7, we first

define the various elements of an eCRG (i.e., nodes, edges and attachments) in

more detail.

Nodes. The most fundamental elements of the eCRG are nodes. According to

the different compliance perspectives the set of nodes Ncan be partitioned into

nodes corresponding to tasks, receiving and sending messages, points in time,

data containers, data objects, and resources as follows:

Definition 4 (Nodes of an eCRG).

Let Nbe the set of nodes of an eCRG Ψ=(N, E, ◇). Then, Ncan be partitioned as follows:

N∶=T∪MR∪MS∪P∪D∪O∪R, where

–Tis the set of task nodes,

–MR/MSis the set of receiving/sending message nodes,

–Pis the set of nodes representing points in time,

–Dis the set of data container nodes,

–Ois the set of data object nodes.

–R∶=RS∪RG∪RR∪RUare the sets of resource nodes for staff members, groups, roles, and

organizational units.

In the following, we use TS∪TEinstead of Tin order to distinguish whether

edges are connected to the left and right side of task nodes. Thereby, TSis

the left side, i.e. it corresponds to the start of a task, whereas TEis the right

side corresponding to completion end of a task. Furthermore, we introduce the

function s∶T→TS(e∶T→TE) to get the start (end) of a task node, and

function t∶TS∪TE→Tfor the opposite direction. Function type ∶(T→T)∪

(M→M)assigns to each task and message node the associated task or message

On the Formal Semantics of the Extended Compliance Rule Graph 13

type. bp ∶(MR∪MS)→Bdenotes the business partner that sends or receives a

message. Finally, T MP ∶=T∪MR∪MS∪P⊆Nis the set of a all task, message,

and points in time nodes, whereas DR ∶=D∪O∪R⊆Ncomprises all data

container, data object, and resource nodes.

We can partition the set of nodes and each of its subsets into distinct sets of

particular instance nodes, antecedence nodes, and absence nodes as well as into

particular instance nodes, antecedence occurrence nodes, antecedence absence

nodes, consequence occurrence nodes, and consequence absence nodes. We use

the exponents I,A,C,AO,AA,CO and CA to indicate the corresponding subset.

Further, the exponent −Idenotes that all nodes are considered except particular

instance ones.

Edges. The nodes of an eCRG can be connected through a wide range of edges

indicating relations and correlations between these nodes. In particular, the set

of edges can be partitioned into distinct subsets (cf. Def. 5). The latter contain

edges for sequence flow, message flow, and distance in time. Other edge subsets

refer to read/write data flow from/to data containers or data objects as well as

to the performers of tasks and relations among data objects or resources. Finally,

the two last subsets contain edges specifying correlations between conditions to

data containers and the particular points in time, when these conditions are

evaluated:

Definition 5 (Edges of an eCRG).

We consider Eas the set of edges of an eCRG Ψ=(N, E, ◇). Then, Ecan be partitioned as

follows:

E∶=# »

sf ∪# »

mf ∪# »

tde ∪# »

wdfc ∪# »

rdfc ∪# »

wdfo ∪# »

rdfo ∪# »

pfm ∪#»

rr ∪#»

dr ∪# »

dcec ∪# »

dceo, where

–# »

sf ⊆(TS∪TE∪MS∪MR∪P)2×RTis the set of sequence flow edges including a time

condition,

–# »

mf ⊆MS×MRis the set of message flow edges,

–# »

tde ⊆(T∪MR∪MS∪P)2×CTis the set of time distance edges including a time condition,

–# »

wdfc ⊆(T∪MR∪MS)×(P∪{⋅})×Dis the set of data flow edges writing to a data container,

–# »

rdfc ⊆D×(T∪MR∪MS)×(P∪{⋅}) is the set of data flow edges reading from a data

container,

–# »

wdfo ⊆(T∪MR∪MS)×(P∪{⋅})×Ois the set of data flow edges writing a data object,

–# »

rdfo ⊆O×(T∪MR∪MS)×(P∪{⋅}) is the set of data flow edges reading a data object,

–# »

pfm ⊆T×Ris the set of performing relation edges denoting the performer of a task,

–#»

rr ⊆R2×RRis the set of resource relation edges,

–#»

dr ⊆O×O×RDis the set of data relation edges,

–# »

dcec ⊆(TS∪TE∪MR∪MS∪P)×D×CDis the set of data condition edges constraining a

data container at a particular point in time by a data condition,

–# »

dceo ⊆(TS∪TE∪MR∪MS∪P)×D×Ois the set of data condition edges requiring a data

container to contain a data object at a particular point in time.

Further, src ∶E→N(tgt ∶E→N) is a function that maps each edge to its

source node (target node), whereas nd ∶E→N, e ↦nd(e)∶={src(e), tgt(e)} is

a function that maps each edge to the set containing its source and target node.

Edges are either part of the antecedence or the consequence pattern. Hence, we

can further partition the set of edges and each of its subsets into antecedence and

14 Knuplesch, Reichert, Ly, Kumar, Rinderle-Ma

consequence edges. We use exponents Aand Cto indicate when only considering

the particular subset.

According to the definition of

# »

sf, each sequence flow requires a time relation.

Thereby, if the graphical representation does not provide a time relation, we

just assume the time condition to be T2, i.e., true for each input. Further an

antecedence edge with a consequence time condition is interpreted as two edges:

an antecedence edge without a time condition and a consequence edge with the

respective time condition.

Attachments. Nodes and edges of an eCRG may be refined by attachments. In

turn, these attachments constitute additional conditions for the respective node

or edge. In particular, the set of attachments ◇can be partitioned into distinct

subsets. The latter refer to different data conditions constraining data flow or

parameters of tasks or messages. Other attachments express time conditions that

constrain the duration of tasks or resource conditions that constrain resources:

Definition 6 (Attachments of an eCRG).

We consider ◇as the set of attachments of an eCRG Ψ=(N, E, ◇). Then, ◇can be partitioned

as follows:

◇∶=◇dcp ∪◇doc ∪◇dfc ∪◇dfo ∪◇td ∪◇rc, where

–◇dcp ⊆(T∪M)×P×CDattaches a task or message node with a data condition on a particular

parameter,

–◇doc ⊆O×CDattaches data object nodes with a data condition,

–◇dfc ⊆(# »

wdfc ∪# »

rdfc ∪# »

wdfo ∪# »

rdfo)×CDattaches data flow edges with a data condition,

–◇dfo ⊆(# »

wdfc∪# »

rdfc)×Oattaches data flow edges from/to a data container with a data object

serving as placeholder for the value of the data flow,

–◇td ∶T×RTattaches task nodes with a time relation that constraints the duration of the

task, and

–◇rc ∶R×CRattaches resource nodes with a resource condition.

Further, at ∶◇→N∪Eis a function mapping each attachment to the node or

edge it corresponds to. Attachments are either part of the antecedence or the

consequence pattern. Consequently, we can partition the set of attachments and

each of its subsets into antecedence and consequence attachments. Again, we use

exponents Aand Cwhen solely referring to the respective subset.

Pattern Classes. As mentioned in Section 3, nodes, edges, and attachments can

be classified as elements of the instance, the antecedence, or the consequence

pattern. In the context of nodes, the antecedence and consequence pattern are

further partitioned into the antecedence occurrence and the antecedence absence

pattern as well as the consequence occurrence and the consequence absence pat-

tern. Def. 7 formally introduces the pattern classes and transfers the finer classi-

fication to edges and attachments (i.e., the classification into antecedence occur-

rence, antecedence absence, consequence occurrence, and consequence absence

patterns). For this purpose, we consider pattern classes of the nodes connected

by an edge as well as the pattern class of the element an attachment corresponds

to.

On the Formal Semantics of the Extended Compliance Rule Graph 15

Definition 7 (Classes of an eCRG).

Let Ψ=(N, E, ◇)be an eCRG. Then:

–I∶=NIis the instance pattern,

–A∶=NAO ∪NAA ∪EA∪◇Ais the antecedence pattern,

–C∶=NCO ∪NCA ∪EC∪◇Cis the consequence pattern,

–EAO ∶={e∈EA∣nd(e)⊆NAO}is the set of antecedence occurrence edges,

–EAA ∶={e∈EA∣nd(e)∩NAA ≠∅∧nd(e)∩NAO ≠∅}is the set of antecedence absence edges,

–ECO ∶={e∈EC∣nd(e)∩NC≠∅∧nd(e)⊆(NCO ∪NAO )} is the set of consequence occurrence

edges,

–ECA ∶={e∈EC∣nd(e)∩NCA ≠∅ ∧ nd(e)∩(NCO ∪NAO )≠∅}is the set of consequence

absence edges,

–◇AO ∶={a∈◇A∣at(a)∈NAO ∪EAO}is the set of antecedence occurrence attachments,

–◇AA ∶={a∈◇A∣at(a)∈NAA ∪EAA}is the set of antecedence absence attachments,

–◇CO ∶={a∈◇C∣at(a)∈NAO ∪EAO ∪NCO ∪ECO }is the set of consequence occurrence

attachments,

–◇CA ∶={a∈◇C∣at(a)∈NCA ∪ECA}is the set of consequence absence attachments,

–AO ∶=NAO ∪EAO ∪◇AO is the antecedence occurrence pattern,

–AA ∶=NAA ∪EAA ∪◇AA is the antecedence absence pattern,

–CO ∶=NCO ∪ECO ∪◇CO is the consequence occurrence pattern,

–CA ∶=NCA ∪ECA ∪◇CA is the consequence absence pattern, and

–C∶={I, AO, AA, CO, CA}is the set of pattern classes.

4.4 Transformation of eCRG

After having defined a formal representation of the process environment, process

logs and compliance rules, we are able to define the semantics of a particular

compliance rule. For this purpose, we transform the eCRG into a first-order pred-

icate logic formula in this subsection. Instead of nodes, edges and attachments,

the resulting logic formula comprises variables derived from the eCRG elements.

However, note that the set of variables is not isomorphic to the sets of nodes

and edges. Thus, Def. 8 introduces the variables required, before describing the

transformation in detail. In this context, we use relation ∈to indicate the set

of values a variable may take.

Definition 8 (Variables).

Let Ψ=(N, E, ◇)be an eCRG, then:

–νt

x∈Tcorresponds for each x∈TS∪TE∪MR∪MS∪Pto the variable for either the point in

time of the start (end) xof a task node, the point of receiving (sending) a message related

to message node x, the time related to a point in time node x, or the particular point in

time of xiff x∈PIis a particular point in time instance node.

–νi

x∈IT∪IMcorresponds for each x∈T∪MR∪MSto the the variable for the instance

identifier of a task or message node x.

–νp

x∈RScorresponds for each x∈Tto the variable for the performing staff member of a

task node x.

16 Knuplesch, Reichert, Ly, Kumar, Rinderle-Ma

–νr

x∈Rcorresponds for each x∈RS∪RG∪RR∪RUto the variable for the related resource

of a resource node xor to the particular resource of x, iff x∈RIrefers to a particular

resource instance.

–νdc

x∈Dcorresponds for each x∈Dto the variable for the associated data container of data

container node xor to the particular data container of x, iff x∈DIrefers to particular

data container instance.

–νdo

x∈Ωcorresponds for each x∈Oto the variable for the data object related to a data

object node xor to the particular data object x, iff x∈OIrefers to a particular data object

instance.

–νdv

x∈Ωcorresponds for each x∈# »

wdfo ∪# »

rdfo ∪# »

wdfa ∪# »

rdfa ∪◇dcp to the variable for the

value of a data flow edge xor the value of the parameter of an attached data condition x.

Furthermore, we define the following sets:

–Vt∶={νt

x∣x∈TS∪TE∪MR∪MS∪P}corresponds to the set of all variables for points in

time,

–Vi∶={νi

x∣x∈T∪MR∪MS}corresponds to the set of all variables for instance identifiers,

–Vp∶={νp

x∣x∈RS}corresponds to the set of all variables for performing staff members,

–Vr∶={νr

x∣x∈RS∪RG∪RR∪RU}corresponds to the set of all variables for resources,

–Vdc ∶={νdc

x∣x∈D}corresponds to the set of all variables for data containers,

–Vdo ∶={νdo

x∣x∈O}corresponds to the set of all variables for data objects,

–Vdv ∶={νdv

x∣x∈# »

wdfo ∪# »

rdfo ∪# »

wdfa ∪# »

rdfa ∪◇dcp}corresponds to the set of all variables for

data flow edges and parameters, and

–V∶=Vt∪Vi∪Vp∪Vr∪Vdc ∪Vdo ∪Vdv corresponds to the set of all variables.

Finally, for each set M⊂N∪E∪◇−NI, each y∈{t, ip, r, dc, do, dv}, and each x∈N∪E∪◇we

define:

–VM

y∶={νy

x∣νy

x∈Vy∧x∈M},

–VM∶=VM

t∩VM

i∩VM

p∩VM

r∩VM

dc ∩VM

do ∩VM

dv ,

–VM

T MP ∶=VM

t∩VM

i∩VM

–VM

RD ∶=VM

r∩VM

dc ∩VM

do ∩VM

dv , and

–VM

x∶={νy

x∣νy

x∈VM}.

Based on these variables, Table 2-4 introduce a set of transformation patterns

Γ, which map the elements of an eCRG to conditions over predicates. Further,

these tables comprise function φ, which defines the affiliation of each element;

i.e. the superordinated element.

For each pattern class c∈C(except I) and each node n∈N, Def. 9 summarizes

the conditions, which are derived by applying the transformation patterns Γto

the corresponding elements. Finally, the resulting terms are used to specify the

transformation in Def. 10.

Definition 9 (Pattern Conditions).

Let Ψ=(N, E, ◇)be an eCRG, let c∈C−{I}be a pattern class, and let n∈Nbe a node. Then

–ξc∶=⋀

x∈c

Γ(x)corresponds to the conjunction of all conditions of pattern c,

–ζc

n∶=⋀

x∈c

φ(x)=n

Γ(x)corresponds to the conjunction of all conditions of pattern cfor node n.

On the Formal Semantics of the Extended Compliance Rule Graph 17

Table 2: Transformation Pattern for Nodes

x Γ (x)φ(x)

α∈T Start(νt

s(α), νi

α, type(α)) ∧End(νt

e(α), νi

α, type(α)) ∧νt

s(α)≤νt

e(α)α

β∈MRReceive(νt

β, νi

β, type(β), bp(β)) β

β∈MSSend(νt

β, νi

β, type(β), bp(β)) β

τ∈Ptrue τ

γ∈Rtrue γ

ω∈Dtrue ω

δ∈Otrue δ

Table 3: Transformation Pattern for Edges

x Γ (x)φ(x)

e=(α, β, relt)∈

# »

sf νt

α≤νt

β∧relt(α, β)if α∈NAA ∪NCA then αelse β

e=(α, β)∈

# »

mf νi

α=νi

βif α∈NAA ∪NCA then αelse β

e=(α, β, cont)∈

# »

tde (νt

e(α)≥νt

s(β)∧cont(∣νt

e(α)−νt

s(β)∣)) if α∈NAA ∪NCA then αelse β

∨(νt

e(β)≥νt

s(α)∧cont(∣νt

e(β)−νt

s(α)∣))

∨(νt

s(α)<νt

e(β)∧νt

s(β)<νt

e(α)∧cont(0))

e=(α, p, ω)∈

# »

wdfc W rite(⋅, νi

α, p, νdv

e, νdc

ω)α

e=(ω, α, p)∈

# »

rdfc Read(⋅, νi

α, p, νdv

e, νdc

ω)α

e=(α, p, δ)∈

# »

wdfo W rite(⋅, νi

α, p, νdv

e,⋅)∧νdo

δ=νdv

eα

e=(δ, α, p)∈

# »

rdfo Read(⋅, νi

α, p, νdv

e,⋅)∧νdo

δ=νdv

eα

e=(α, γ)∈

# »

pfm P erform(νi

α, νr

e)∧InStaff(νr

γ, νr

e)α

e=(γ, η, relr)∈#»

rr relr(γ, η)γ

e=(δ, , reld)∈

#»

dr reld(δ, )δ

e=(α, ω, cond)∈

# »

dcec val(νt

α, ω, νdv

e)∧cond(νdv

e)α

e=(α, ω, δ)∈

# »

dceo val(νt

α, ω, νdo

δ)α

Table 4: Transformation Pattern for Attachments

x Γ (x)φ(x)

a=(α, p, cond)∈◇dcp P arameter(νi

α, p, vdv

a)∧cond(vdv

a)α

a=(o, cond)∈◇doc cond(νdo

o)φ(o)

a=(e, cond)∈◇dfc cond(vdv

e)φ(e)

a=(e, δ)∈◇dfo vdv

e=νdo

δφ(e)

a=(α, relt)∈◇td relt(νt

s(α), νt

e(α))α

a=(γ, conr)∈◇rc conr(νr

γ)γ

18 Knuplesch, Reichert, Ly, Kumar, Rinderle-Ma

Definition 10 (Transformation).

The semantic of an eCRG Ψ=(N, E, ◇)is expressed by the following FOL formula Λ(Ψ):

Λ(Ψ)∶=∀Θ(VAO

T MP )∶⎛

⎝(∃Θ(VAO

RD )∶ξAO)

∧(⋀

n∈T MP AA ∄Θ(VAA

n)∶∃Θ(VAO

RD ∪VAA

RD )∶ξAO ∧ζAA

n)⎞

⎠

⇒∃Θ(VCO

T MP )∶⎛

⎝(∃Θ(VAO

RD ∪VCO

RD )∶ξAO ∧ξCO )

∧(⋀

n∈T MP CA ∄Θ(VCA

n)∶∃Θ(VAO

RD ∪VCO

RD ∪VCA

RD )∶ξAO ∧ξCO ∧ζCA

n)⎞

⎠

Thereby, Θ(W)is replaced by the comma-separated concatenation of the vari-

ables contained by a set W⊆V. For example ’∃Θ({ν1, ν2, ν3})’ would be replaced

by ’∃ν1, ν2, ν3’. In case of the empty set (i.e., W=∅), Θ(W)is replaced by a

dummy variable.

Note that the transformation specified in Def. 3-10 is neither able to deal with

exclusive and alternative connectors nor with multiple consequence patterns.

Hence, we formally introduce exclusive and alternative connectors as well as

multiple consequences in Def. 11.

Definition 11 (eCRG with multiple consequences, exclusive & alternative connectors).

An eCRG with exclusive and alternative connectors is a tuple Ψ+=(N, E, ◇, ex, alt). Thereby

Ψ′∶=(N, E, ◇)is an eCRG and

–ex ⊆2T∪MS∪MR∪Pis the set of exclusive connectors between task nodes, sending message

nodes, receiving message nodes, and points in time and

–alt ⊆2T∪MS∪MR∪Pis the set of alternative connectors between task nodes, sending message

nodes, receiving message nodes, and points in time.

T, MS, MR, P ⊆Nare the distinct sets of task nodes, sending message nodes, receiving message

nodes, and points in time of Ψ′(cf. Def. 4). We define

–Nex ∶=⋃

χ∈ex

χas the set of nodes contained in the set of exclusive connectors,

–Nalt ∶=⋃

χ∈alt

χas the set of nodes contained in the set of alternative connectors, and

–Nex,alt ∶=Nex ∪Nalt as the union of these two sets.

As opposed to Def. 7,

–SC is the set of pairwise disjoint consequence patterns, and

–Ci∈SC with Ci⊆N∪E∪◇corresponds to a particular consequence pattern and COi(CAi)

is the corresponding consequence occurrence pattern (consequence absence pattern).

Exclusive and alternative connectors either connect elements of the antecedence

pattern solely or elements of the same consequence pattern. Consequently, we

can partition the set of exclusive and alternative connectors as well as the related

sets of nodes (Nex,Nalt,Nex,alt) into antecedence and consequence connectors.

We use exponents Aand Cito indicate the corresponding subset.

An exclusive connector is satisfied if the condition related to exactly one of its

nodes (and connected edges and attachments) is satisfied. In turn, the conditions

related to the other nodes of the exclusive connector must be violated. Thus, to

On the Formal Semantics of the Extended Compliance Rule Graph 19

solve an exclusive connector we can split it into different cases, whereby each

case corresponds to the selection of one node. In this context, the selected node

remains unchanged, while all other nodes of the exclusive connector are negated

(i.e. occurrence nodes become absence nodes and vice versa). Finally, the logic

disjunction of all cases expresses the semantics of the exclusive connector. An

alternative connector is satisfied, if the condition related to at least one of its

nodes (and connected edges and attachments) is satisfied. In turn, the conditions

of the remaining nodes are irrelevant. According to exclusive connectors, we can

solve an alternative connector by splitting it into its different cases, whereby each

case corresponds to the selection of one node. In this context, the selected node

remains unchanged, whereas the remaining nodes of the alternative connector

are removed. Again, the logic disjunction of all cases expresses the semantics of

the alternative connector. In Def. 12 formally introduce selections of nodes first,

which correspond to the cases mentioned above.

Definition 12 (Selections).

Let Ψ+=(N, E, ◇, ex, alt)be an eCRG with multiple consequences, exclusive and alternative

connectors. Then

–τ⊆NAis an antecedence selection choosing one node out of each exclusive and alternative

antecedence connector; i.e., ∀χ∈exA∪altA∶∣τ∩χ∣=1,

–τ−1∶=NA

ex,alt −τis the complement of τ,

–υ⊆NCiis a consequence selection choosing one node out of each exclusive and alternative

consequence connector of Ci; i.e., ∀χ∈exCi∪altCi∶∣τ∩χ∣=1,

–υ−1∶=NCi

ex,alt −υis the complement of υ,

–ΠA∶={τ⊆Nex,alt ∩(NAO ∪NAA)∣∀χ∈exA∪altA∶∣τ∩χ∣=1}is the set of all antecedence

selections, and

–ΠCi∶={υ⊆Nex,alt ∩(NCOi∪NCAi)∣∀χ∈exCi∪altCi∶∣υ∩χ∣=1}is the set of all consequence

selections of consequence pattern Ci.

As aforementioned, each selection configures the pattern class of nodes; i.e. se-

lected nodes remain in their class, while the non-selected ones change their pat-

tern class (exclusive connector) or are removed (alternative connector). Def. 13

specifies these node configurations in detail.

Definition 13 (Configuration of Nodes).

Let Ψ+=(N, E, ◇, ex, alt)be an eCRG with multiple consequences, exclusive and alternative

connectors, and let τ∈ΠAbe an antecedence selection and υ∈ΠCibe a consequence selection.

Then

–N(AO,τ)∶=(NAO −Nex,alt)∪(τ∩NAO

ex,alt)∪(τ−1∩NAA

ex )corresponds to the configuration of

antecedence occurrence nodes NAO based on τ,

–N(AA,τ)∶=(NAA −Nex,alt)∪(τ∩NAA

ex,alt)∪(τ−1∩NAO

ex )corresponds to the configuration of

antecedence absence nodes NAA based on τ,

–N(COi,υ)∶=(NCOi−Nex,alt)∪(υ∩NCOi

ex,alt)∪(υ−1∩NCAi

ex )corresponds to the configuration

of antecedence occurrence nodes NCOibased on τ,

–N(CAi,υ)∶=(NCAi−Nex,alt)∪(υ∩NCAi

ex,alt)∪(υ−1∩NCOi

ex )corresponds to the configuration

of antecedence absence nodes NCAibased on τ,

20 Knuplesch, Reichert, Ly, Kumar, Rinderle-Ma

Node configurations affect the corresponding edges and attachments as well.

Thus, Def. 14 (re-)configures the definition pattern classes from Def. 7:

Definition 14 (Configuration of Classes).

Let Ψ+=(N, E, ◇, ex, alt)be an eCRG with exclusive and alternative connectors, and let τ∈ΠA

be an antecedence selection and υ∈ΠCibe a consequence selection. Then:

–E(AO,τ)∶={e∈EA∣nd(e)⊆N(AO,τ)}is the configuration of antecedence occurrence edges

based on τ,

–E(AA,τ)∶={e∈EA∣nd(e)∩N(AA,τ)≠∅ ∧ nd(e)∩N(AO,τ)≠∅}is the configuration of

antecedence absence edges based on τ,

–E(COi,τ,υ)∶={e∈ECi∣nd(e)⊆(N(COi,υ)∪N(AO,τ))} is the configuration of consequence

occurrence edges based on τand υ,

–E(CAi,τ,υ)∶={e∈ECi∣nd(e)∩N(CAi,υ)≠∅ ∧ nd(e)∩(N(COi,υ)∪N(AO,τ ))≠∅}is the

configuration of consequence absence edges based on τand υ,

–◇(AO,τ)∶={a∈◇A∣at(a)∈N(AO,τ)∪E(AO,τ)}is the configuration of antecedence occur-

rence attachments based on τ,

–◇(AA,τ)∶={a∈◇A∣at(a)∈N(AA,τ)∪E(AA,τ )}is the configuration of antecedence absence

attachments based on τ,

–◇(COi,τ,υ)∶={a∈◇Ci∣at(a)∈N(AO,τ)∪E(AO,τ)∪N(COi,υ)∪E(COi,τ,υ)}is the configura-

tion of consequence occurrence attachments based on τand υ,

–◇(CAi,τ,υ)∶={a∈◇Ci∣at(a)∈N(CAi,υ)∪E(CAi,τ,υ)}is the configuration of consequence

absence attachments based on τand υ,

–AOτ∶=N(AO,τ )∪E(AO,τ)∪◇(AO,τ)is the configuration of the antecedence occurrence

pattern based on τ,

–AAτ∶=N(AA,τ)∪E(AA,τ)∪◇(AA,τ )is the configuration of the antecedence absence pattern

based on τ,

–CO(τ,υ)

i∶=N(COi,υ)∪E(COi,τ,υ)∪◇(COi,τ,υ)is the configuration of the consequence oc-

currence pattern based on τand υ,

–CA(τ,υ)

i∶=N(CAi,υ)∪E(CAi,τ,υ)∪◇(CAi,τ,υ)is the configuration of the consequence

absence pattern based on τand υ,

–Aτ∶=AOτ∪AAτis the configuration of the antecedence pattern based on τ, and

–C(τ,υ)

i=CO(τ,υ)

i∪CA(τ,υ)

iis the configuration of the consequence pattern based on τand υ,

–HAτ∶=A−Aτare the elements of the antecedence pattern that are masked during its

configuration based on τ,

–HC(τ,υ)

i∶=Ci−C(τ,υ)

iare the elements of consequence pattern Cithat are masked during

its configuration based on τand υ.

Based on Def. 14, we are able to enrich the transformation from Def. 10 with the

support for exclusive and alternative connectors as well as multiple consequences

in Def. 15.

On the Formal Semantics of the Extended Compliance Rule Graph 21

Definition 15 (Transformation).

The semantics of an eCRG Ψ+=(N, E, ◇, ex, alt)with multiple consequences, exclusive and

alternative connectors is expressed by the following FOL formula Λ+(Ψ+):

Λ+(Ψ+)∶=⋁

τ∈ΠA∀Θ(VAOτ

T MP )∶⎛

⎝((∃Θ(VAOτ

RD )∶ξAOτ)

∧(⋀

n∈T MP AAτ∄Θ(VAAτ

n)∶∃Θ(VAOτ

RD ∪VAAτ

RD )∶ξAOτ∧ζAAτ

n) )

⇒⋁

Ci∈SC

υ∈ΠCi

∃Θ(VCOτ,υ

T MP )∶((∃Θ(VAOτ

RD ∪VCOτ,υ

RD )∶ξAOτ∧ξCOτ,υ

∧(⋀

n∈T MP CAτ,υ

∄Θ(VCAτ,υ

n)∶∃Θ(VAOτ

RD ∪VCOτ,υ

RD ∪VCAτ,υ

RD )∶ξAOτ∧ξCOτ,υ

i∧ζCAτ,υ

n))⎞

⎠

For example, Def. 10 and Def. 15 translate eCRG c4from Fig. 10A into:

Λ(c4)=∀νt

PS, νt

PE, νi

P, νp

P∶⎛

⎝(∃νdo

O, νdv

(O,P )∶

Start(νt

PS, νi

P,Prod.)∧End(νt

PE, νi

P,Prod.)∧νt

PS≤νt

∧Read(⋅, νi

P,⋅, νdv

(O,P ),⋅)∧νdo

O=νdv

(O,P ))

⇒(∄νt

CS, νt

CE, νi

C, νp

C∶∃νdo

O, νdv

(O,P ), νdv

(O,C)∶

Start(νt

PS, νi

P,Prod.)∧End(νt

PE, νi

P,Prod.)∧νt

PS≤νt

∧Read(⋅, νi

P,⋅, νdv

(O,P ),⋅)∧νdo

O=νdv

(O,P )

∧Start(νt

CS, νi

C,Chg.)∧End(νt

CE, νi

C,Chg.)∧νt

CS≤νt

∧νt

PS≤νt

∧Read(⋅, νi

C,⋅, νdv

(O,C),⋅)∧νdo

O=νdv

(O,C))⎞

⎠

5 Pattern-based Evaluation

This section outlines a pattern-based evaluation of the eCRG language. In partic-

ular, we model the compliance patterns introduced in [9, 11, 29] with the eCRG

language. These patterns result from literature and case studies, and thus consti-

tute a suitable empirical basis for evaluating the appropriateness of our approach.

5.1 Business Process Control Pattern and Property Specification

Pattern

27 business process control patterns (BPCPs) for modeling compliance rules are

introduced in [11]. They include all property specification patterns from [54]. Out

of the 27 BPCPs, 15 BPCPs focus on the control flow (i.e., process) perspective,

7 BPCPs focus on the resource perspective, and 5 BPCPs focus on the time

perspective. In turn, the data perspective is implicitly supported by each BPCP,

since BPCPs do not distinguish between tasks and data conditions. Fig. 11

shows how to model the 15 control flow BPCPs with the eCRG language. In

turn, Fig. 12 provides eCRGs that model the 7 resource BPCPs and the 5 time

BPCPs.

22 Knuplesch, Reichert, Ly, Kumar, Rinderle-Ma

Q P

Q P = 0

Precedes

LeadsTo

XLeadsTo

PLeadsTo

Q S P T

S PQ T

ChainLeadsTo

ChainPrecedes

LeadsTo-Else

Exists

Absent

¬P

Universal

Q P

CoExists

CoAbsent

Exclusive

CoRequisite

Q P

P Q

Q P

QPMutexChoice

Fig. 11: control flow BPCPs

PerformedBy

SegregatedFrom

P Q

is is

≠

P Q

≠

USegregatedFrom

P Q

BondedWith

P Q

is is

≠

RBondedWith

P Q

≠

P Q

Multi-Segregated

Multi-Bonded

Q P < k

Within k

After k Q P > k

Q P = k

= k

ExactlyAt k

> k

Exists Max/Min k P

< k

Exists Every k Q

< k

every k

start

Fig. 12: Resource and time BPCPs

On the Formal Semantics of the Extended Compliance Rule Graph 23

Note that most BPCPs can easily be modeled using the eCRG language. How-

ever, from our subjective point of view the modeling of the XLeadsTo BPCP, the

Universal BPCP, the Exists Max/Min BPCP, and the Exists Every k BPCP was

a bit more complicated. In turn, Fig. 12 provides an eCRG for the special case of

the Multi-Segregated BPCP, which requires the numbers of performers and tasks

to be equal. Other cases of the Multi-Segregated BPCP can not be modeled us-

ing only one consequence pattern; e.g., in case that the Multi-Segregated BPCP

requires 4 tasks to be executed by 3 different performers (i.e., one performer

must execute two tasks), (4

2)=6 consequence patterns are required. Hence the

Multi-Segregated BPCP is the only BPCP that cannot always be appropriately

modeled using the eCRG language.

5.2 Compliance Rule Pattern

55 control flow compliance rule patterns (CRPs) are introduced in [9]. Further,

one example of the data perspective and another one of the resource perspective

are presented. The 55 control flow CRPs are partitioned into 15 categories. Note

that 7 categories and the respective CRPs fully coincide with the aforementioned

BPCPs (cf. Table 5). The remaining 8 categories and respective CRPs are mod-

eled with the eCRG language in Figs. 13-16. Fig. 17 contains both examples

illustrating the data and resource perspectives.

Table 5: Intersection between BPCPs and CRPs

Compliance rule pattern Business process control pattern

Existence - Event universality Exists

Existence - Event absence Absent

Exclusive Exclusive

Mutual Exclusive MutexChoice

Prequisite CoAbsent

Inclusive CoExists

Substitute LeadsTo-Else

CoRequisite CoRequisite

24 Knuplesch, Reichert, Ly, Kumar, Rinderle-Ma

Bounded Existence

Exactly k times A

Bounded Existence

At least k times

A A

Bounded Existence

At most k times A A A

Bounded Existence

Exactly k times in a row

Bounded Existence

At least k times in a row

Bounded Existence

At most k times in a row

A A

Between

After - Before C

Between

Simultaneously or after

Before

Between

After

Simultaneously or before

Between

Directly after

Directly before

A C B

Between

Simultaneously

Between

Simultaneously or after

Simultaneously or before

Between

At least one

other activity

A B

B A

Fig. 13: Bounded existence CRPs and between CRPs

A1 A2

Chain Precedence

Direct

B1 B2

Chain Precedence

Direct or indirect

A1 A2

B1 B2

A1 A2

B1 B2

Chain Precedence

Never direct

Chain Precedence

Never

A1 A2

B1 B2

A1 A2

Chain Response

Direct

B1 B2

Chain Response

Direct or indirect

A1 A2

B1 B2

A1 A2

B1 B2

Chain Response

Never direct

Chain Response

Never

A1 A2

B1 B2

Fig. 14: Chain precedence CRPs and chain response CRPs

On the Formal Semantics of the Extended Compliance Rule Graph 25

Bounded Sequence

One to one coexistence

Bounded Sequence

Coexistence

A B

B A

A B

B A

A B

B A

A B

B A

Bounded Sequence

Exactly k times

A B

B A

Bounded Sequence

At least k times

Bounded Sequence

At most k times

Parallel A

Fig. 15: Bounded sequence CRPs and parallel CRPs

26 Knuplesch, Reichert, Ly, Kumar, Rinderle-Ma

Precedence

Simultaneus or before

Precedence

Direct

Precedence

Direct or indirect

A B

Precedence

At least once A B

Precedence

Direct multiple events

Precedence

Direct or indirect

multiple events

A B

Precedence

Direct multiple

different events

Precedence

Direct or indirect multiple

different events

Precedence

Never direct B A

Precedence

Never

Response

Simultaneus or after

Response

Direct

Response

Direct or indirect

A B

Response

At least once A B

Response

Direct multiple events

Response

Direct or indirect

multiple events

A B

Response

Direct multiple

different events

Response

Direct or indirect multiple

different events

Response

Never direct B A

Response

Never

Fig. 16: Precedence CRPs and response CRPs

B A

≠

grant

customer

record

is silver

discout

= 5%

grant

customer

record

is gold

discout

= 10%

Data-flow Organizaitional

Fig. 17: Data flow CRPs and resource CRPs

On the Formal Semantics of the Extended Compliance Rule Graph 27

Note that most CRPs can easily be modeled using the eCRG language. However,

from our subjective point of view a thinking outside the box was required when

we modeled the Bounded Existence - Exactly k times in a row CRP, the Bounded

Existence - At most k times in a row CRP, the Between - Simultaneously, Si-

multaneously CRP, and all Bounded Sequence CRPs - especially in case of the

Bounded Sequence - One to one coexistence CRP.

5.3 Time Pattern

In [28, 29], a set of 10 time patterns (TPs) is introduced and formally specified.

In Fig. 18, the eCRG language is applied to model these TPs.

TP1

Time Lag between

two Activities

= 1d

TP2

Duration

< 3h

Sender

TP1

Time Lag between

Events

TP4

Fixed Data Elements

TP5

Schedule Restricted

Elements

TP6

Time-based

Restriction

TP7

Validity Period

TP 8

Time-dependent

Variability

TP9

Cyclic elements

TP10 Periodicity

12am

< 3h

A B

= 1d

iteration

9 April 2014

4:00 pm

< 2h A

start

schedule A

end

schedule

start

frame

end

frame

A A

start

validity

end

validity

Sender

9 April 2014

6:00 pm

9 April 2014

6:00 pm

start

period

end

period

Fig. 18: Time Patterns

Note that most TPs can be easily modeled using the eCRG language. However,

from our subjective point of view the modeling of TP6 Time-based Restrictions

and the modeling of TP8 Time-dependent Variability were a bit more compli-

cated.

Fig. 19 summarizes the results of the pattern-based evaluation. Overall, we were

able to model 26 out of the 27 business process control patterns (BPCPs) [11], in-

cluding 5 time BPCPs and 7 resource BPCPs as well. Only the multi-segregation

pattern cannot be properly modeled using the eCRG language in any case. Fur-

ther, the eCRG language supports the 15 categories of compliance rule patterns

28 Knuplesch, Reichert, Ly, Kumar, Rinderle-Ma

and respective rules as well as the data flow and the resource example from [9].

Finally, the eCRG language covers well-known time-patterns [29] as well.

Business process control patterns

Property specification patterns

Compliance rule

pattern categories

Time patterns

Precedes

USegregatedFrom

Existence

Time lags between activities

LeadsTo

BondedWith

Bounded existence

Durations

XLeadsTo

RBondedWith

Bounded sequence

Time lags between events

PLeadsTo

Multi-Segregated

Parallel

Fixed date elements

ChainLeadsTo

Multi-Bonded

Precedence

Schedule restricted elements

Chain Precedes

Within k

Chain precedence

Time-based restrictions

LeadsTo - Else

After k

Response

Validity period

Exists

ExactlyAt k

Chain response

Time-dependend variability

Absent

Exists Max/Min

Between

Cyclic elements

Universal

Exists Every k

Exclusive

Periodicity

CoExists

Mutual exclusive

CoAbsent

Inclusive

Exclusive

Prequisite

CoRequisite

Substitute

MutexChoice

Corequisite

PerformedBy

Data flow

SegregatedFrom

Organizational

++ full support, + inconvenient support, 0 partial support, - minor support, -- no support

Fig. 19: Support of compliance patterns

6 Summary and Outlook

While compliance rule modeling has been introduced by a plethora of approaches,

the data, time, resource and interaction perspectives of compliance rules have

not been sufficiently addressed yet [12, 8–11]. This report has introduced the

extended Compliance Rule Graph (eCRG) language, which is based on the com-

pliance rule graph (CRG) language [15, 24]. As opposed to existing visual com-

pliance rule notations, the eCRG supports multiple perspectives; i.e., beyond

the control flow perspective, data, time, resources, and interactions with busi-

ness partners are considered. To provide tool support for both the modeling and

verification of compliance rules, we have formalized the syntax and semantics of

the eCRG. Finally, we have conducted a pattern-based evaluation to prove the

proper expressiveness of the eCRG language.

In future work, we will conduct experiments to evaluate the usability and scala-

bility of the eCRG. Furthermore, we will develop techniques for verifying com-

pliance of business processes and process choreographies with such rules.

References

1. Knuplesch, D., Reichert, M., Ly, L.T., Kumar, A., Rinderle-Ma, S.: Visual model-

ing of business process compliance rules with the support of multiple perspectives.

In: ER’2013. Volume 8217 of LNCS., Springer (2013) 106–120

On the Formal Semantics of the Extended Compliance Rule Graph 29

2. Reichert, M., Weber, B.: Enabling Flexibility in Process-Aware Information Sys-

tems - Challenges, Methods, Technologies. Springer (2012)

3. van der Aalst, W.M.P.: Verification of workflow nets. In: ICATPN’97. Volume

1248 of LNCS., Springer (1997) 407–426

4. Reichert, M.: Dynamische ablauf¨anderungen in workflow-management-systemen,

university of ulm, germany (2000)

5. Rinderle, S., Reichert, M., Dadam, P.: Evaluation of correctness criteria for dy-

namic workflow changes. In: BPM ’03. Volume 2678 of LNCS., Springer (2003)

41–57

6. Sadiq, S., Governatori, G., Naimiri, K.: Modeling control objectives for business

process compliance. In: BPM’07. Volume 4717 of LNCS., Springer (2007) 149–164

7. Lenz, R., Reichert, M.: It support for healthcare processes - premises, challenges,

perspectives. Data and Knowledge Engineering 61(1) (2007) 39–58

8. Cabanillas, C., Resinas, M., Ruiz-Cort´es, A.: Hints on how to face business process

compliance. In: JISBD’10. (2010) 26–32

9. Ramezani, E., Fahland, D., van der Aalst, W.M.P.: Where did I misbehave? Di-

agnostic information in compliance checking. In: BPM’12. Volume 7481 of LNCS.,

Springer (2012) 262–278

10. Mangler, J., Rinderle-Ma, S.: IUPC: Identification and unification of process con-

straints. arXiv.org (2011)

11. Turetken, O., Elgammal, A., van den Heuvel, W.J., Papazoglou, M.: Capturing

compliance requirements: A pattern-based approach. IEEE Software 29(3) (2012)

29–36

12. Knuplesch, D., Reichert, M., Mangler, J., Rinderle-Ma, S., Fdhila, W.: Towards

compliance of cross-organizational processes and their changes. In: BPM’12 Work-

shops. Volume 132 of LNBIP., Springer (2013) 649–661

13. Fdhila, W., Rinderle-Ma, S., Reichert, M.: Change propagation in collaborative

processes scenarios. In: CollaborateCom’12, IEEE (2012) 452–461

14. Ghose, A.K., Koliadis, G.: Auditing business process compliance. In: ICSOC’07.

Volume 4749 of LNCS., Springer (2007) 169–180

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

pliance rule graphs in process-aware information systems. In: CAiSE’10. Volume

6051 of LNCS., Springer (2010) 9–23

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

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

17. Ly, L., Indiono, C., Mangler, J., Rinderle-Ma, S.: Data transformation and semantic

log purging for process mining. In: CAiSE’12. Volume 7328 of LNCS., Springer

(2012) 238–253

18. Schultheiß, B., Meyer, J., Mangold, R., Zemmler, T., Reichert, M., Dadam, P.,

Kreienberg, R.: Prozessentwurf am Beispiel eines Ablaufs aus dem OP-Bereich -

Ergebnisse einer Analyse an der Universit¨atsfrauenklinik Ulm. Technical Report

DBIS-6, University of Ulm (1996)

19. Schultheiß, B., Meyer, J., Mangold, R., Zemmler, T., Reichert, M., Dadam, P.,

Kreienberg, R.: Prozessentwurf f¨ur den Ablauf einer ambulanten Chemotherapie.

Technical Report DBIS-7, University of Ulm (1996)

20. Konyen, I., Schultheiß, B., Reichert, M.: Prozessentwurf f¨ur den Ablauf einer

radiologischen Untersuchung. Technical Report DBIS-15, University of Ulm (1996)

21. Konyen, I., Schultheiß, B., Reichert, M.: Prozessentwurf eines Ablaufs im Labor.

Technical Report DBIS-16, University of Ulm (1996)

30 Knuplesch, Reichert, Ly, Kumar, Rinderle-Ma

22. Bestfleisch, U., Herbst, J., Reichert, M.: Requirements for the workflow-based

support of release management processes in the automotive sector. In: ECEC’05.

(2005) 130–134

23. M¨uller, D., Herbst, J., Hammori, M., Reichert, M.: It support for release manage-

ment processes in the automotive industry. In: BPM’06. Volume 4102 of LNCS.,

Springer (September 2006) 368–377

24. Knuplesch, D., Reichert, M.: Ensuring business process compliance along the pro-

cess life cycle. Technical Report 2011-06, Ulm University (2011)

25. Russell, N., van der Aalst, W.M.P., ter Hofstede, A.H.M., Edmond, D.: Workflow

resource patterns: Identification, representation and tool support. In: CAiSE’05.

Volume 3520 of LNCS., Springer (2005) 216–232

26. Kumar, A., Wang, J.: A framework for document-driven workflow systems. In:

Handbook on Business Process Management 1. Volume 3649 of LNCS. Springer

(2010) 419–440

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

DEXA’08. Volume 5181 of LNCS., Springer (2008) 668–675

28. Lanz, A., Weber, B., Reichert, M.: Workflow time patterns for process-aware

information systems. In: BPMDS’10. Volume 50 of LNBIP., Springer (2010) 94–

107

29. Lanz, A., Weber, B., Reichert, M.: Time patterns for process-aware information

systems. Requirements Engineering 19(2) (2014) 113–141

30. Decker, G., Weske, M.: Interaction-centric modeling of process choreographies.

Information Systems 36(2) (2011) 292–312

31. Barros, A., Dumas, M., ter Hofstede, A.: Service interaction patterns. In: BPM’05.

Volume 3649 of LNCS., Springer (2005) 302–318

32. K¨unzle, V., Weber, B., Reichert, M.: Object-aware business processes: Fundamen-

tal requirements and their support in existing approaches. Journal of Information

System Modeling and Design 2(2) (2011) 19–46

33. Knuplesch, D., Pryss, R., Reichert, M.: Data-aware interaction in distributed and

collaborative workflows: Modeling, semantics, correctness. In: CollaborateCom’12,

IEEE (2012) 223–232

34. Ly, L.T., Rinderle, S., Dadam, P.: Integration and verification of semantic con-

straints in adaptive process management systems. Data & Knowledge Engineering

64(1) (2008) 3–23

35. Ly, L.T., Rinderle-Ma, S., G¨oser, K., Dadam, P.: On enabling integrated process

compliance with semantic constraints in process management systems. Information

Systems Frontiers 14(2) (2012) 195–219

36. Ramezani, E., Fahland, D., van der Werf, J.M., Mattheis, P.: Separating com-

pliance management and business process management. In: BPM’11 Workshops.

Volume 100 of LNBIP., Springer (2012) 459–464

37. Governatori, G., Sadiq, S.: The journey to business process compliance. In: Hand-

book of Research on BPM. IGI Global (2009) 426–454

38. Namiri, K., Stojanovic, N.: Pattern-Based design and validation of business process

compliance. In: OTM’07. Volume 4803 of LNCS., Springer (2007) 59–76

39. Governatori, G., Hoffmann, J., Sadiq, S., Weber, I.: Detecting regulatory com-

pliance for business process models through semantic annotations. In: BPM’08

Workshops. Volume 17 of LNBIP., Springer (2009) 5–17

40. Kumar, A., Yao, W., Chu, C.: Flexible process compliance with semantic con-

straints using mixed-integer programming. INFORMS Journal on Computing

25(3) (2013) 543–559

On the Formal Semantics of the Extended Compliance Rule Graph 31

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

violation for data aware compliance rules. In: ICSOC’09. Volume 5900 of LNCS.,

Springer (2009) 500–515

42. Knuplesch, D., Ly, L.T., Rinderle-Ma, S., Pfeifer, H., Dadam, P.: On enabling

data-aware compliance checking of business process models. In: ER’2010. Volume

6412 of LNCS., Springer (2010) 332–346

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

service models. In: SEFM’10, IEEE (2010) 125–134

44. Ly, L.T., 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: Information Systems Evolution. Volume 72 of LNBIP.

Springer (2011) 76–91

45. Knuplesch, D., Reichert, M., Fdhila, W., Rinderle-Ma, S.: On enabling compliance

of cross-organizational business processes. In: BPM’13. Volume 8094 of LNCS.

Springer (2013) 146–154

46. Knuplesch, D., Reichert, M., Pryss, R., Fdhila, W., Rinderle-Ma, S.: Ensuring

compliance of distributed and collaborative workflows. In: CollaborateCom’13,

IEEE (2013) 133–142

47. H¨ohn, S.: Model-based reasoning on the achievement of business goals. In: SAC’09,

ACM (2009) 1589–1593

48. Accorsi, R., Lowis, L., Sato, Y.: Automated certification for compliant cloud-based

business processes. Business & Information Systems Engineering 3(3) (2011) 145–

154

49. Awad, A., Weidlich, M., Weske, M.: Visually specifying compliance rules and

exp-laining their violations for business processes. Journal of Visual Languages &

Computing 22(1) (2011) 30–55

50. Feja, S., Speck, A., Witt, S., Schulz, M.: Checkable graphical business process

representation. In: ADBIS’11. Volume 6295 of LNCS., Springer (2011) 176–189

51. Rinderle, S., Wombacher, A., Reichert, M.: Evolution of process choreographies in

DYCHOR. In: OTM’06. Volume 4275 of LNCS., Springer (2006) 273–290

52. Cabanillas, C., Resinas, M., Cort´es, A.R.: Defining and analysing resource assign-

ments in business processes with RAL. In: ICSOC’11. Volume 7084 of LNCS.,

Springer (2011) 477–486

53. Reichert, M.: Process and data: Two sides of the same coin? In: OTM’12. Volume

7565 of LNCS., Springer (2012) 2–19

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

finite-state verification. In: FMSP’98, ACM (1998) 7–15