Deontic BPMN: a powerful extension of BPMN with a trusted model transformation

The Business Process Model and Notation (BPMN) is a widely-used standard for process modelling. A drawback of BPMN, however, is that modality is implicitly expressed through the structure of the process flow but not directly within the corresponding activity. Thus, an extension of BPMN with deontic logic has been proposed in previous work, called Deontic BPMN. Deontic BPMN reduces the structural complexity of the process flow and increases the readability by explicitly highlighting obligatory and permissible activities. In addition, an algebraic graph transformation from a subset of BPMN to Deontic BPMN, called Deontic BpmnGTS, has been defined. The goal of the current research is to show that DeonticBpmnGTS is terminating and confluent, resulting in a globally deterministic transformation. Moreover, the semantic equivalence of BPMN models and the respective Deontic BPMN models is proven based on Abstract State Machines (ASMs). Thus, DeonticBpmnGTS can be called a trusted model transformation.