Object-Centric Conformance Checking with Synchronization of Interrelated Objects

This paper presents a new formalism called object-centric Petri nets with identifiers (OPIDs) that combines the ability to capture one-to-many relations between objects with the ability to compare and synchronize objects based on their identity. The authors define alignments and the conformance checking task for this setting, and propose a conformance checking approach based on an encoding in satisfiability modulo theories (SMT).