SMT Techniques for Data-Aware Process Mining

Alessandro Gianola

doi:10.1007/s13218-025-00890-z

2025-04-29

Alessandro Gianola

Marco Montali *

Sarah Winkler

DOI：10.1007/s13218-025-00890-z

原文链接

原文求助

摘要

En 中文

流程挖掘正经历从纯控制流过程模型向更丰富的、数据感知的过程模型的转变，其中可接受执行不仅由过程控制流表征，还由案例携带的数据以及它们如何与过程活动和决策动态交互来表征。即使在过程控制流有界的典型假设下，数据的引入也使得整体状态空间变为无限，这一困难转移到了流程分析和流程挖掘任务中。在本文中，我们回顾了如何通过基于自动推理的AI技术（特别是基于可满足性及理论优化（SMT/OMT））有效应对数据感知流程挖掘带来的挑战。为此，我们讨论了数据感知日志和带有有效载荷的轨迹合并。随后，我们回顾了数据Petri网作为符合这一多视角设置的表达式流程建模方法，以及逻辑data-LTLf\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\textsf {data-}{\textsf {LTL}_f}$$\end{document}，用于制定正确性属性和表示带有数据的声明式流程约束。接着，我们总结了关键流程分析和挖掘任务如何在该设置下通过SMT和OMT解决，特别关注正确性及符合性检查、模型修复和监控。我们概述了获得的结果，在集成视角下呈现它们，并提供相应的技术文献参考。在结论中，我们展望了开放挑战。

Keyword:

SOUNDNESS

VERIFIER

TOOL