标题： 高效丰富的数据感知Declare规范的一致性检查（扩展版） 显示英文标题

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

摘要： 尽管对数据感知规范的过程分析和挖掘的兴趣不断增加，基于对齐的声明式过程模型的符合性检查主要集中在纯控制流规范上，或者仅限于数值数据和变量到常量比较的轻微数据感知扩展。 这并不令人意外：即使在存在数据依赖的情况下，找到对齐也是计算上困难的。 在本文中，我们针对参考模型使用具有通用数据类型和数据条件的数据感知Declare的情况来挑战这个问题。 我们表明，出人意料的是，在这种丰富的设置中可以计算出数据感知的最优对齐，同时享有效率和表达性。 这是通过仔细结合两种最著名的处理控制流和数据依赖性的方法来实现的，即A*搜索和SMT求解。 具体来说，我们引入了一种新的算法技术，该技术能够高效地探索搜索空间，通过应用旨在逐步解决约束违反的修复操作来生成后代状态。 我们证明了我们算法的正确性，并通过实验展示了其效率。 评估结果表明，我们的方法在性能上与最先进的方法相当或超越，同时支持显著更丰富的数据依赖性，展示了其支持实际应用的潜力。 显示英文摘要

摘要： 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.