Proving Regulatory Compliance: Business Processes, Logic, Complexity

The problem of proving regulatory compliance of a business process model is composed of two main elements. One of these elements is the business process model, which provides a formal compact description of the available executions capable of achieving a given business objective. The other element is the regulatory framework that the business process must follow, describing the compliance requirements given by the law or by a company’s own internal regulations. The problem consists of verifying whether a given business process model is compliant with the regulatory framework, which is carried out by verifying whether the executions of the model comply with the requirements of the regulatory framework.
Solutions to prove the regulatory compliance of business processes have been already proposed in the past. Some solutions disregard the computational complexity aspect of the problem, while other solutions either solve a simplified version of the problem efficiently or provide approximate solutions for the general one. However, none of these solutions have formally studied the computational complexity of the problem of proving regulatory compliance. This thesis addresses that issue, showing in addition why efficient solutions of the general problem are not possible. In particular I study the computational complexity of a problem of proving regulatory compliance whose regulatory framework is defined using conditional obligations. The approach I adopt to represent the compliance requirement is semantically similar to some of the existing solutions proposed by other researchers, such as van der Aalst and many others, who adopts linear temporal logic over finite traces, or different variants of such temporal logic, to define the compliance requirements. More precisely, the approach used in the present thesis adopts propositional logic as base logic, and defines the semantics of the regulatory framework in a similar way as Process Compliance Logic introduced by Governatori and Rotolo.
The study of the computational complexity of the problem is approached by dividing it in sub-classes and then combining their analysis to obtain the result for the target problem. The division is done according to three features of the regulatory framework. These features define whether the framework is composed of a single or a set of obligations, whether the obligations are conditional and whether violations can be compensated. These features can be omitted to identify simpler sub-classes of the problem. After having identified the different sub-classes of the problem, I study the computational complexity of some of these sub-classes and combine the results obtained to identify the computational complexity of the general problem tackled in the present thesis, where each of the three features identified are used to describe the compliance requirements.
The results of the computational complexity analysis show that proving the existence of an execution of a business process compliant with the regulatory framework is an NP-complete problem. Differently proving that for all of the executions of a business process model, they are either compliant or not with the regulatory framework, is a coNP-complete problem. The results show that combining the two elements composing the problem of proving regulatory compliance, the process model and the regulatory framework, which are tractable when considered individually, leads to an intractable problem. In addition to the computational complexity results, the analysis provided in the thesis has also shown that tractable sub-classes of the problem, where the computational complexity is at most polynomial with respect to the size of the input, can be obtained by trivialising the expressivity of either one of the elements composing the problem. However the expressivity of these sub-classes is limited. Thus I identify a different tractable sub-class of the problem by weakening the expressivity of both elements composing the problem, but where each element is not trivialised as for the other sub-classes. Whether the sub-class identified can be considered expressive is arguable, however it represents a first step towards identifying a sub-class of the problem being both tractable and expressive, taking into account the limitation of employing propositional logic as base logic.