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 artificial intelligence. In this spectrum, Data Petri nets (DPNs) have gained growing popularity thanks to their ability to balance simplicity with expressiveness. To faithfully model real-world processes, the data perspective often requires arithmetic, which renders basic problems undecidable. Nonetheless, we show here that by appropriately restricting the constraint language or structure, a number of important tasks becomes decidable for practical classes of systems: This includes linear- and branching-time model checking, strategic reasoning, and verification of data-aware soundness.