Soundness of Data-Aware Processes with Arithmetic Conditions
This addresses a crucial challenge in business process management and information systems engineering by enabling more realistic modeling with arithmetic, though it is incremental as it builds on existing DPN frameworks.
The paper tackles the problem of checking soundness in Data Petri nets with arithmetic data conditions, which previous approaches lacked, and provides a foundational framework with a proof-of-concept implementation using SMT technologies, validated on examples from the literature and synthetic variants.
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.