Table of Contents
Fetching ...

Validating Temporal Compliance Patterns: A Unified Approach with $MTL_f$ over various Data Models

Nesma M. Zaki, Iman M. A. Helal, Ehab E. Hassanein, Ahmed Awad

TL;DR

The paper addresses the need for explicit temporal constraints in process compliance checking by adopting Metric Temporal Logic over finite traces ($MTL_f$). It introduces a minimal set of $MTL_f$ formulas and templates that cover common compliance patterns, and provides systematic mappings to relational (SQL/Match_Recognize) and graph (Multi-Dimensional and UA) data models. An extensive empirical evaluation across four real-life event logs shows that graph-based UA encoding often delivers superior performance and scalability, validating the approach for large-scale conformance checking. The work advances a unified formalism for timing-aware compliance rules and demonstrates practical pathways to implement them in common data models, enabling more accurate and scalable process mining workflows.

Abstract

Process mining extracts valuable insights from event data to help organizations improve their business processes, which is essential for their growth and success. By leveraging process mining techniques, organizations gain a comprehensive understanding of their processes' execution, enabling the discovery of process models, detection of deviations, identification of bottlenecks, and assessment of performance. Compliance checking, a specific area within conformance checking, ensures that the organizational activities adhere to prescribed process models and regulations. Linear Temporal Logic over finite traces ($LTL_{f}$ ) is commonly used for conformance checking, but it may not capture all temporal aspects accurately. This paper proposes Metric Temporal Logic over finite traces ($MTL_{f}$ ) to define explicit time-related constraints effectively in addition to the implicit time-ordering covered by $LTL_f$. Therefore, it provides a universal formal approach to capture compliance rules. Moreover, we define a minimal set of generic $MTL_f$ formulas and show that they are capable of capturing all the common patterns for compliance rules. As compliance validation is largely driven by the data model used to represent the event logs, we provide a mapping from $MTL_f$ to the common data models we found in the literature to encode event logs, namely, the relational and the graph models. A comprehensive study comparing various data models and an empirical evaluation across real-life event logs demonstrates the effectiveness of the proposed approach.

Validating Temporal Compliance Patterns: A Unified Approach with $MTL_f$ over various Data Models

TL;DR

The paper addresses the need for explicit temporal constraints in process compliance checking by adopting Metric Temporal Logic over finite traces (). It introduces a minimal set of formulas and templates that cover common compliance patterns, and provides systematic mappings to relational (SQL/Match_Recognize) and graph (Multi-Dimensional and UA) data models. An extensive empirical evaluation across four real-life event logs shows that graph-based UA encoding often delivers superior performance and scalability, validating the approach for large-scale conformance checking. The work advances a unified formalism for timing-aware compliance rules and demonstrates practical pathways to implement them in common data models, enabling more accurate and scalable process mining workflows.

Abstract

Process mining extracts valuable insights from event data to help organizations improve their business processes, which is essential for their growth and success. By leveraging process mining techniques, organizations gain a comprehensive understanding of their processes' execution, enabling the discovery of process models, detection of deviations, identification of bottlenecks, and assessment of performance. Compliance checking, a specific area within conformance checking, ensures that the organizational activities adhere to prescribed process models and regulations. Linear Temporal Logic over finite traces ( ) is commonly used for conformance checking, but it may not capture all temporal aspects accurately. This paper proposes Metric Temporal Logic over finite traces ( ) to define explicit time-related constraints effectively in addition to the implicit time-ordering covered by . Therefore, it provides a universal formal approach to capture compliance rules. Moreover, we define a minimal set of generic formulas and show that they are capable of capturing all the common patterns for compliance rules. As compliance validation is largely driven by the data model used to represent the event logs, we provide a mapping from to the common data models we found in the literature to encode event logs, namely, the relational and the graph models. A comprehensive study comparing various data models and an empirical evaluation across real-life event logs demonstrates the effectiveness of the proposed approach.
Paper Structure (22 sections, 4 equations, 4 figures, 10 tables)

This paper contains 22 sections, 4 equations, 4 figures, 10 tables.

Figures (4)

  • Figure 1: Compliance Patterns
  • Figure 2: HR hiring process
  • Figure 3: Multi-Dimensional Encoding of Table \ref{['tbl:hiringeventlog']}
  • Figure 4: UA Encoding of Table \ref{['tbl:hiringeventlog']}

Theorems & Definitions (5)

  • Definition 1: Event
  • Definition 2: Trace
  • Definition 3: Event log
  • Definition 4: Linear-Time Temporal Logic (LTL)
  • Definition 5: Metric Temporal Logic on finite traces ($MTL_{f}$)