Alloy-Driven Verification of Object-Centric Event Data: From Temporal Logic to Knowledge Graphs
Saba Latif, Huma Latif, Touseef Ur Rehman, Muhammad Rameez Ur Rahman
TL;DR
The paper tackles data integrity and expressive limitations in object-centric process mining by formalizing OCED as FOCED and verifying it with Alloy. It then transforms verified FO C ED data into a Neo4j knowledge graph and demonstrates Cypher-based queries for path visualization, activity frequency, and event sequencing on BPIC 2013. The approach integrates formal verification with graph analytics and provides Python bindings to increase industrial adoption. Compared to OCEL and EKG, the work emphasizes formal guarantees of cross-object cardinality and time-aware consistency, reducing data invisibility during imports.
Abstract
Object-centric process mining addresses the limitations of traditional approaches, which often involve the lossy flattening of event data and obscure vital relationships among interacting objects. This paper presents a novel formal framework for Object-centric Event Data (OCED) that ensures the correctness of the meta-model and preserves native object-centric semantics prior to the system implementation. Our approach effectively leverages Alloy for precisely specifying temporal properties and structural relationships between objects and events. This guarantees thorough verification against predefined OCED constraints such as cross-object cardinality bounds and time-aware consistency rules, hence preventing common data integrity issues. We demonstrate the effectiveness of the proposed framework in discovering and validating implicit object dependencies in event logs, particularly when importing data into graph databases like Neo4j. This demonstrates how formal verification can avoid pitfalls that lead to data invisibility and improve knowledge graph creation, enrichment, and querying. To bridge theory and practice, our verified \emph{FOCED} is made accessible through automatically generated Python bindings, empowering industrial users without formal methods expertise. The code is available on GitHub \footnote{https://github.com/sabalati/FOCED}