Soundness Correction of Data Petri Nets

TL;DR

This work tackles repairing data-aware process models modeled as Data Petri Nets (DPNs) by restricting transition guards to eliminate executions that lead to improper termination, without introducing new behavior. It introduces a formal repair framework using labeled and colored reachability structures, including tau-refinement, to identify and forbid problematic executions while preserving as much of the original behavior as possible. The authors prove termination and non-additivity of behavior for the repair procedure, implement a prototype, and demonstrate practical applicability on small-to-medium DPNs with favorable performance compared to existing guard-restriction methods. The contribution advances soundness repair for DPNs with arbitrary data guards, offering a semi-decision procedure that complements domain knowledge in model repair and can be integrated into process-design workflows.

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.

Figures (18)

• Figure 1: DPN $\mathcal{N}$ representing a visit to a casino with a deadlock. $M_I = [i]$ and $M_F = [o]$. Variable age is of a real type and initialized to $\mathtt{0}$. Variable hasPass is of a boolean type and initialized to false.
• Figure 2: A fragment of the reachability graph for $\mathcal{N}$ from Figure \ref{['fig:casino']}. Arcs are labeled with the initials of the transition names. Square brackets denote markings. Curly brackets denote variable valuations. Double circles denote final nodes. Forbidden signs denote deadlocks.
• Figure 3: DPN $\mathcal{N}$ with an initial state $M_I = [i]$ and $\alpha_I(a) = 0$, and a final state $M_F = [o]$. The net has a sound control flow that cannot be repaired by restricting transition guards.
• Figure 4: Bounded DPN $\mathcal{N}$ with an unsound control flow that cannot be repaired by restricting transition guard. $M_I = [i]$ and $M_F = [o]$. For each transition, the guard is $\small{\texttt{true}}\xspace$.
• Figure 5: Unbounded DPN $\mathcal{N}$ that cannot be repaired by restricting transition guards. Here, $M_I = [i]$ and $\alpha_I(a) = 0$, and $M_F = [o]$.

Theorems & Definitions (26)

• Definition 2.1: Arithmetic constraint
• Definition 2.2: Satisfaction of an arithmetic constraint
• Definition 2.3: Data Petri net
• Definition 2.4: Transition firing
• Definition 2.5: Reachability set, reachability graph
• Example 2.1
• Definition 2.6: Data-aware soundness deLeoni18
• Example 2.2
• Definition 4.1: Labeled Transition System Induced by a DPN
• Example 4.1