Data-aware Soundness Verification and Repair of Data Petri-Nets

Business processes are one of organizations' core assets, impacting directly on the quality of products and services and on the revenue of corporations. A failure in such processes can negatively affect the core of the organization and its production chain. For such reasons, various tools, techniques, and methods have been gathered from different disciplines and collected in what is called Business Process Management (BPM). Petri Net, or Place/Transition (P/T) Net, is one such tool: it is a powerful modeling formalism combining a well-defined mathematical theory with a graphical representation of the dynamic behavior of systems. Given the endless heterogeneity of cases and the extensive combinations between the various resources that interact in a process, additional Petri Net extensions were designed through the years, each aiming to provide more expressive power to describe a broader range of systems. One is Data Petri Net (DPN). This Petri Net-based modeling formalism allows adding a data dimension to the traditional control flow, which permits both the description of how data evolve through the lifecycle of the process and the decisions based on such data. The presence of unreachable activities or steps without the possibility to proceed further falls under the concept of soundness, and its verification has been a central topic for different research activities. The following work hooks into soundness verification and provides an approach to repair Data Petri Nets concerning data and decision perspective. It provides an extensive and accurate description of unsound DPNs that helps the reader understand the base cases and their resolution. Due to the presence of false-positive cases within the existing soundness verification techniques in the literature, this work studies such issues and proposes a patch aimed at the correct identification of these unsound DPNs. The verification and repair techniques rely on the Constraint Graph structure, a finite symbolic abstraction of the possibly infinite traces of a DPN.The algorithms proposed assume that the underlying Petri Net is sound, thus focusing solely on the repair of data that determines the behavior of the net, aiming to restore its soundness. They seek to provide a solution with minimal changes from the original DPN, which helps the process designer verify its correctness and plan further developments and optimizations.