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.

翻译：过程挖掘从事件数据中提取有价值的见解，帮助组织优化业务流程，这对组织的成长与成功至关重要。通过运用过程挖掘技术，组织能够全面理解其流程执行情况，从而发现过程模型、检测偏差、识别瓶颈并评估性能。合规性检查作为一致性检验中的特定领域，确保组织活动遵循既定的过程模型和规范。有限迹上的线性时序逻辑（$LTL_{f}$）常用于合规性检查，但可能无法准确捕获所有时间维度。本文提出有限迹上的度量时序逻辑（$MTL_{f}$），在$LTL_f$隐含的时间顺序约束基础上，有效定义显式时间相关约束，从而提供捕获合规规则的通用形式化方法。此外，我们定义了一组最小化的通用$MTL_f$公式，证明其能够覆盖所有常见合规规则模式。由于合规性验证很大程度上依赖于表示事件日志的数据模型，我们提供了从$MTL_f$到文献中常见的事件日志编码数据模型（关系模型与图模型）的映射方法。通过跨多种数据模型的综合比较及真实事件日志的实证评估，验证了所提出方法的有效性。