Abstract
Data Petri nets (DPNs) with arithmetic have gained popularity as a model for data-aware processes, thanks to their ability to balance simplicity with expressiveness and because they can be automatically discovered from event logs. While model checking techniques for DPNs have been studied, there are analysis tasks highly relevant for BPM that are beyond these methods. We focus here on process equivalence and process refinement with respect to language and configuration spaces; such comparisons are important in the context of process repair and discovery. To solve these tasks, we propose an approach for bounded DPNs based on constraint graphs, which are faithful abstractions of the reachable state space. Though the considered verification tasks are undecidable in general, we show that our method is a decision procedure for large classes of DPNs relevant in practice.