Alloy-Driven Verification of Object-Centric Event Data: From Temporal Logic to Knowledge Graphs

TL;DR

This paper introduces a formal framework using Alloy for verifying object-centric event data, ensuring data integrity and object relationships are preserved, which enhances knowledge graph creation and querying.

Contribution

It presents a novel Alloy-based verification framework for object-centric event data that maintains semantics and prevents data integrity issues, bridging formal methods and practical applications.

Findings

Effective verification of object dependencies in event logs.

Prevents data invisibility issues in knowledge graphs.

Provides accessible tools for industrial users.

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}