[Paper] 可解释的层次工作流验证：基于事件日志的挖掘与Shapley Values

Source: arXiv - 2512.09562v1

Overview

本文提出了一条新颖的流水线，将自动挖掘得到的层次化工作流转换为形式化逻辑规范，使用自动定理证明器进行检查，并利用 Shapley 值 解释 为何 工作流满足（或违反）安全性、活性或合规性等属性。通过将过程挖掘与博弈论归因相结合，作者为开发者提供了一种具体方法，以定位使过程“好”或“坏”的确切节点。

Key Contributions

• 形式化翻译：将从事件日志中提取的层次化过程树模型转换为适用于自动推理的逻辑公式。
• 属性验证（可满足性、活性、安全性）：使用现成的定理证明器，实现系统化的合规检查。
• Shapley 值归因：针对工作流元素进行适配，提供量化的“可解释性”层，说明每个节点对验证结果的贡献程度。
• 实证验证：在标准基准日志上展示该方法能够发现传统挖掘工具遗漏的关键瓶颈、冗余分支和有害模式。
• 原型工具链：集成过程挖掘、定理证明和博弈论分析，展示了在真实流水线中可行性。

Methodology

1. 挖掘层次化工作流 – 从事件日志出发，使用最先进的过程树挖掘器（如 Inductive Miner）生成一个嵌套树，内部节点表示控制流操作符（顺序、并行、选择、循环），叶子节点对应具体活动。
2. 逻辑编码 – 将每个操作符映射为时序/一阶逻辑的片段（例如顺序对应 “A → ◇B”）。整个树被转化为单一的逻辑规范。
3. 自动化验证 – 将规范输入 SMT 或 SAT‑based 定理证明器（Z3、CVC5），检查用户定义的属性（如 “每个订单最终都会到达 Ship”）是否成立。
4. Shapley 值计算 – 将工作流节点集合视为合作博弈：当仅保留某些节点时，若属性被满足则该联盟的“价值”为 1，否则为 0。通过枚举（或近似）边际贡献，为每个节点分配一个 Shapley 分数，量化其对最终验证结果的影响。
5. 解释与可视化 – 高正分数的节点是正确性的 “保护者”；高负分数的节点标记出风险或冗余构件。作者直接在过程树上可视化这些分数。

Results & Findings

• 在 BPI Challenge 日志上，该方法识别出 ≤5 % 的节点是导致安全属性违规的关键，结果与手工发现的缺陷一致，但所需工作量大幅降低。
• 冗余检测：在多个日志中，部分并行分支的 Shapley 值接近零，表明它们可以合并而不影响正确性。
• 性能：对最多 200 个节点的树，验证 + Shapley 分析的总耗时不足 30 秒，显示出对典型企业流程的可扩展性。
• 可解释性：开发者能够追溯到导致合规检查失败的单一循环构件，该构件引入了意外的死锁，这在原始事件日志统计中根本不可见。

Practical Implications

• 合规自动化 – 企业可以将该流水线嵌入业务流程的 CI/CD 环境，自动标记违反监管规则（如 GDPR 相关数据处理步骤）的情况。
• 流程优化 – 通过突出低影响或有害节点，工程师可以重构工作流，删除类似死代码的分支，从而降低执行时间和资源消耗。
• 复杂编排调试 – 微服务编排平台（BPMN、Camunda、Temporal）常生成大型执行图，基于 Shapley 的归因提供了一个 “热图”，显示哪些服务导致活性失败。
• 工具链集成 – 原型可包装为 REST 服务，允许现有过程挖掘平台（如 ProM、Celonis）调用形式化验证并获取可解释的分数。
• 教育与文档 – 新成员可以通过检查 Shapley 分数了解工作流为何安全，加速入职培训和知识转移。

Limitations & Future Work

• Shapley 计算的可扩展性 – 精确的联盟评估呈指数增长；当前实现依赖 Monte‑Carlo 抽样，对极大树可能引入方差。
• 属性表达能力 – 逻辑编码目前仅支持一部分时序属性；更丰富的规范（如定量时间界限）需要扩展编码。
• 事件日志噪声 – 挖掘错误（缺失或伪造事件）会传递到逻辑模型，可能导致 Shapley 分数偏差；鲁棒的预处理仍是待解问题。
• 用户定义属性选择 – 框架假设分析师能够自行构造合适的逻辑谓词；未来工作旨在基于领域本体自动推荐相关属性。

Bottom line: 通过将不透明的挖掘工作流转化为可验证、可解释的制品，该研究为开发者提供了一条实用路径，以 审计、调试和改进 过程驱动的软件系统，并达到与代码同等的严谨性。

Authors

• Radoslaw Klimek
• Jakub Blazowski

Paper Information

• arXiv ID: 2512.09562v1
• Categories: cs.SE, cs.IT
• Published: December 10, 2025
• PDF: Download PDF