Soundness in Object-centric Workflow Petri Nets
This work addresses formal verification challenges in workflow modeling for systems involving multiple interacting objects, but it is incremental as it builds on existing formalisms.
The paper tackles the problem of defining and analyzing soundness in object-centric workflow Petri nets, demonstrating that the soundness problem is decidable for nets with non-deterministic synchronization between case objects.
Recently introduced Petri net-based formalisms advocate the importance of proper representation and management of case objects as well as their co-evolution. In this work we build on top of one of such formalisms and introduce the notion of soundness for it. We demonstrate that for nets with non-deterministic synchronization between case objects, the soundness problem is decidable.