Soundness Verification and Repair of Data-Aware Workflow Process Models: Experimental Data

This dataset includes synthetically generated data Petri nets (DPNs) of different sizes and the results of their soundness verification and repair.
The following setups are considered:
- Sound DPNs with n transitions, 0.9n places, 0.25n variables, 0.75n conditions.
- Bounded but unsound DPNs with n transitions (up to 25% of them can be dead), 0.9n places, 0.25n variables, 0.75n conditions.
- Unbounded DPNs with n transitions (up to 25% of them can be dead), 0.9n places, 0.25n variables, 0.75n conditions, and 0.2n additional arcs.
- DPNs with resources with n transitions, 0.9n workflow places, 0.2n resource places, 0.25n variables, 0.75n conditions.
As n, we consider the numbers in the range from 5 to 50.

In addition, the dataset includes cyclic and acyclic DPNs with different levels of concurrency (from 1 to 7) and the results of their soundness verification and repair.

We consider three types of operations over the DPNs:
- Classical soundness verification using the algorithms from Suvorov N. M., Lomazova I. A., Verification of data-aware process models: Checking soundness of data Petri nets, Journal of Logical and Algebraic Methods in Programming. 2024. Vol. 138. Article 100953.
- Relaxed lazy soundness verification using the algorithm from Suvorov N. M., Lomazova I. A., Relaxed Lazy Soundness Verification for Data Petri nets, Proceedings of the Institute for System Programming of the RAS. 2025. Vol. 37. No. 4. P. 69–84.
- Classical soundness repair using the algorithm from Suvorov N. M., Lomazova I. A., Soundness Correction of Data Petri Nets, IEEE Access. 2025. Vol. 13. P. 149142–149157.

Each directory has a name describing the considered setup. The directory includes the set of considered DPNs in the extended PNML format and the .csv-file showing the metainformation regarding the operation execution (DPN filename, DPN properties, execution time, abstract states constructed, etc.).

The results confirm the practical applicability of the previously introduced algorithms for small- and medium-sized models with a moderate level of concurrency. Verification algorithms take less than half of a minute for execution on each considered model. The soundness repair algorithm takes less than 3 minutes on almost all the bounded models considered, but on the unbounded models, it may require more than 15 minutes even for rather small models (with more than 13 transitions). The reason for the latter problem is the necessity to construct the whole abstract coverability graph, which is often large for unbounded DPNs. In the future, we plan to investigate whether we can fasten the algorithm execution for this type of models.