Soundness Correction of Data Petri Nets

A process model is called sound if it always terminates properly and each model activity can occur in a process instance. Conducting soundness verification right after process design enables the detection and elimination of design errors in a process to be implemented. The process of eliminating such errors is called soundness repair. In many repair scenarios, the resulting model should retain only the correct behavior of the source model, especially if a model is created manually. In this paper, we consider this type of soundness repair applied to data-aware process models represented as data Petri nets (DPNs). We investigate the capabilities to repair soundness of DPNs by restricting the transition guards and disprove some earlier statements regarding it. We propose a new repair algorithm that follows this approach, with a key distinction that it does not require an input DPN to have a sound control flow. The algorithm is implemented, and the results of its preliminary evaluation justify its practical applicability in realistic application domains.