Conformance checking of declarative data-aware processes

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 present an extension of Declare with general data types and expressive data conditions, which generalizes previous versions of data-aware Declare. 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 two established approaches to deal with control flow and data dependencies when computing alignments, namely uniform-cost 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 also show that our approach is expressive enough to capture the alignment problem for Timed Declare, which is a well-established extension of Declare with timed constraints, as well as its combination with general data types, which was not studied so far. 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, concerning both data-aware and Timed Declare, while supporting significantly more expressive data dependencies, showcasing its potential to support real-world applications.