Abstract
A model of an information system describes its processes and how these processes manipulate data objects. Object-aware extensions of Petri nets focus on modeling the life-cycle of objects and their interactions. In this paper, we focus on Petri nets with identifiers, where identifiers are used to refer to objects. These objects should “behave” well in the system from inception to termination. We formalize this intuition in the notion of identifier soundness, and show that although this property is undecidable in general, useful subclasses exist that guarantee identifier soundness by construction.