Soundness Correction of Data Petri Nets

TL;DR

This paper introduces a new algorithm for repairing the soundness of data Petri nets by restricting transition guards, which does not require the original model to be sound, and demonstrates its effectiveness on moderate-sized models.

Contribution

It proposes a novel soundness repair algorithm for data Petri nets that operates without needing a sound control flow in the input model.

Findings

The algorithm effectively repairs soundness by restricting transition guards.

Implementation shows applicability to moderate-sized data Petri nets.

Preliminary evaluation confirms the method's feasibility.

Abstract

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 allows one to detect and eliminate 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). Specifically, we investigate the capabilities to repair soundness of DPNs by restricting the transition guards and propose a new repair algorithm that follows this approach. A distinctive feature of the algorithm is the absence of a requirement for an input DPN to have a sound control flow. The algorithm is implemented and results of the preliminary evaluation demonstrate its applicability to process models of moderate sizes.