A Holistic Approach for Soundness Verification of Decision-Aware Process Models (extended version)

TL;DR

This paper presents a comprehensive method for verifying the soundness of decision-aware process models by translating them into colored Petri nets, enabling effective analysis with existing tools.

Contribution

It introduces a holistic verification approach for integrated process models that considers data and decisions, extending previous local-focused methods.

Findings

The technique is proven correct and terminates reliably.

It can be applied to decision-aware soundness verification.

The approach leverages existing Petri net analysis tools.

Abstract

The last decade has witnessed an increasing transformation in the design, engineering, and mining of processes, moving from a pure control-flow perspective to more integrated models where also data and decisions are explicitly considered. This calls for methods and techniques able to ascertain the correctness of such integrated models. Differently from previous approaches, which mainly focused on the local interplay between decisions and their corresponding outgoing branches, we introduce a holistic approach to verify the end-to-end soundness of a Petri net-based process model, enriched with case data and decisions. In particular, we present an effective, implemented technique that verifies soundness by translating the input net into a colored Petri net with bounded color domains, which can then be analyzed using conventional tools. We prove correctness and termination of this technique. In addition, we relate our contribution to recent results on decision-aware soundness, showing that our approach can be readily applied there.