Soundness in Object-centric Workflow Petri Nets

Abstract

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.

This is an ongoing work that introduces basic notions and theoretical results needed for establishing the theoretical framework for checking soundness of object-centric Petri nets