Alloy-Driven Verification of Object-Centric Event Data: From Temporal Logic to Knowledge Graphs
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909896517091328 |
|---|---|
| author | Latif, Saba Latif, Huma Rehman, Touseef Ur Rahman, Muhammad Rameez Ur |
| author_facet | Latif, Saba Latif, Huma Rehman, Touseef Ur Rahman, Muhammad Rameez Ur |
| contents | 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} |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2511_07263 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Alloy-Driven Verification of Object-Centric Event Data: From Temporal Logic to Knowledge Graphs Latif, Saba Latif, Huma Rehman, Touseef Ur Rahman, Muhammad Rameez Ur Formal Languages and Automata Theory 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} |
| title | Alloy-Driven Verification of Object-Centric Event Data: From Temporal Logic to Knowledge Graphs |
| topic | Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2511.07263 |