Efficient Conformance Checking of Rich Data-Aware Declare Specifications (Extended)

TL;DR

This paper presents a novel, efficient method for conformance checking in data-aware declarative process models, combining A* search and SMT solving to handle complex data dependencies with high expressiveness.

Contribution

It introduces a new algorithm that efficiently computes optimal alignments in rich data-aware Declare models, surpassing previous methods in performance and expressiveness.

Findings

The approach matches or exceeds state-of-the-art performance.

Supports more expressive data dependencies.

Proven correctness and demonstrated efficiency through experiments.

Abstract

Despite growing interest in process analysis and mining for data-aware specifications, alignment-based conformance checking for declarative process models has focused on pure control-flow specifications, or mild data-aware extensions limited to numerical data and variable-to-constant comparisons. This is not surprising: finding alignments is computationally hard, even more so in the presence of data dependencies. In this paper, we challenge this problem in the case where the reference model is captured using data-aware Declare with general data types and data conditions. We show that, unexpectedly, it is possible to compute data-aware optimal alignments in this rich setting, enjoying at once efficiency and expressiveness. This is achieved by carefully combining the two best-known approaches to deal with control flow and data dependencies when computing alignments, namely A* search and SMT solving. Specifically, we introduce a novel algorithmic technique that efficiently explores the search space, generating descendant states through the application of repair actions aiming at incrementally resolving constraint violations. We prove the correctness of our algorithm and experimentally show its efficiency. The evaluation witnesses that our approach matches or surpasses the performance of the state of the art while also supporting significantly more expressive data dependencies, showcasing its potential to support real-world applications.