Soundness of Data-Aware Processes with Arithmetic Conditions

TL;DR

This paper introduces a new framework for verifying the soundness of data-aware Petri nets that include arithmetic data conditions, using SMT technology for improved accuracy in real-world applications.

Contribution

It provides the first foundational and operational framework for assessing soundness of DPNs with arithmetic conditions, supported by an SMT-based implementation.

Findings

Framework successfully verifies soundness on literature examples.

Implementation demonstrates effectiveness with synthetic and real-world inspired models.

SMT technology enables handling of complex data conditions in process models.

Abstract

Data-aware processes represent and integrate structural and behavioural constraints in a single model, and are thus increasingly investigated in business process management and information systems engineering. In this spectrum, Data Petri nets (DPNs) have gained increasing popularity thanks to their ability to balance simplicity with expressiveness. The interplay of data and control-flow makes checking the correctness of such models, specifically the well-known property of soundness, crucial and challenging. A major shortcoming of previous approaches for checking soundness of DPNs is that they consider data conditions without arithmetic, an essential feature when dealing with real-world, concrete applications. In this paper, we attack this open problem by providing a foundational and operational framework for assessing soundness of DPNs enriched with arithmetic data conditions. The framework comes with a proof-of-concept implementation that, instead of relying on ad-hoc techniques, employs off-the-shelf established SMT technologies. The implementation is validated on a collection of examples from the literature, and on synthetic variants constructed from such examples.