Soundness Verification of Decision-Aware Process Models with Variable-to-Variable Conditions

In recent years, there has been an increasing interest in enriching the traditional control-flow perspective of processes with additional dimensions, the data perspective being the most prominent one. At the same time, variants of Petri nets with data have been extensively studied, giving raise to a plethora of formal models with different expressive power and computational guarantees. In this work, we focus on DPNs, a data-aware extension of P/T nets where the net is enriched with data variables of different types, and transitions are guarded by formulae that inspect and update such variables. Even though DPNs are less expressive than Petri nets where data are carried by tokens, they elegantly capture business processes operating over simple case data and taking complex decisions based on these data. Notably, various techniques have been implemented to discover DPNs from event data. However, such techniques do not guarantee that the discovered DPN is actually sound. In previous work, we have then studied how to check soundness of DPNs with simple data-based guards that can only compare variables with constants. In this paper, we generalize the study of soundness to DPNs to the fundamental case where the evolution of the process depends on the comparison between the values carried by different variables through linear inequations. Our main contribution is to show decidability of soundness for this sophisticated class of DPNs. This is done by constructing an abstract state space of the net relying on the manipulation of constraints, and by showing that such an abstract state space can be faithfully and effectively inspected for soundness. The construction lends itself to be directly implemented by combining standard state-space construction methods with constraint programming techniques.