Declarative Approaches for Compliance by Design

Abstract

The interest of scholars in devising automated methods to describe and analyse business processes has increased in the last decades due to the extreme interest of organisations in achieving their business objectives while remaining compliant with the relevant normative system. Adhering with norms and policies does not only help to avoid severe sanctions but also results in greater confidence by the consumers, and prestige for the organisation. Defining processes through the paradigm of declarative specifications is gaining momentum due to its intrinsic characteristic of being able to capture business as well as normative specifications within the same framework. We describe some of the state of the art techniques in the field of Business Process Compliance, focusing on pros and cons of such techniques, and advancing future lines of research.

A   Petri Nets

Petri nets (PN) are a popular modelling language used to formalise business processes [37]. Petri nets are mathematical models for the description of distributed systems [31]. Petri nets are directed bi-graphs with nodes consisting of places and transitions. Transitions within Petri nets represent events, while places represent conditions. Arcs form directed edges between place-transition pairs. Places may contain tokens. A distribution of tokens over the places is called a marking. A transition is enabled and can “fire” when all its input places contain at least one token. When a transition fires, one token is removed from each input place and one token is put into each output place. A Petri net is defined formally as follows [31]:

Definition 1

(Petri net). A tuple $(P,T,A,\lambda )$ is a labeled Petri net, where:

• P is a set of places

• T is a set of transitions, such that $P \cap T =\emptyset$

• $A \subseteq (P \times T) \cup (T \times P)$ is a set of arcs

• $\lambda : P \cup T \rightarrow \mathcal {L}$ is a labelling function.

The Petri net state, often referred to as the net marking, $M: P \rightarrow \mathbb {N}_0$ is a function that associates a place $p \in P$ with a natural number (viz., place tokens). A marked net $N = (P,T,A,\lambda ,M_0)$ is a Petri net $(P,T,A,\lambda )$ together with an initial marking $M_0$.

Places and transitions are referred to as nodes. The preset of a node is denoted by $\bullet {y} = \{x \in P\cup T \ | \ (x,y) \in A\}$, and the postset of a node is denoted by ${y}\bullet = \{z \in P\cup T \ | \ (y,z) \in A\}$.

If $\forall p \in \bullet {t} : M(p) > 0$, t is said to be enabled. The firing of t, denoted by $M\mathrel {\smash {{\mathop {\longrightarrow }\limits ^{t}}}}M^\prime$, leads to a new marking $M^\prime$, with $M^\prime (p) = M(p) - 1$ if $p \in \bullet {t} \setminus {t}\bullet$, $M^\prime (p) = M(p) + 1$ if $p \in {t}\bullet \setminus \bullet {t}$, and $M^\prime (p) = M(p)$ otherwise. The marking $M_n$ is said to be reachable from M if there exists a sequence of transition firings $\sigma =t_1 t_2 \dots t_n$ such that $M\mathrel {\smash {{\mathop {\longrightarrow }\limits ^{t_1}}}}M_1\mathrel {\smash {{\mathop {\longrightarrow }\limits ^{t_2}}}}\dots \mathrel {\smash {{\mathop {\longrightarrow }\limits ^{t_n}}}}M_n$.

A trace is a sequence $\lambda (t_{1}),\lambda (t_{2}),\dots$ such that $\sigma =t_{1},t_{2},\dots$ is a sequence of firing transitions. However, certain control-flow behaviour (like exclusive parallel branches) requires additional transitions that do not correspond to a task literal. These transitions are commonly referred to as silent or $\tau$ transitions [9]. For understandability purposes, we will add a label for each $\tau$ transition as well throughout the paper. As such, the set of transition labels $\mathcal {L}$ comprises both labels corresponding to task literals and labels corresponding to $\tau$ transitions. A visible trace is a trace where all $\tau$ transitions have been removed (maintaining the order of the transitions representing task literals). For the remainder of this work, we shall refer to visible traces as traces.