享受静默：含沉默变迁的随机 Petri 网分析

在业务和工作流程中捕捉随机行为，对于定量理解流程内决策时非确定性如何被消解至关重要。这在过程挖掘中尤为受关注，其中追踪流程实际执行的事件数据会与流程模型相关联，从而能提供关于频率和概率的洞察。随机 Petri 网的多种变体为此提供了自然的形式化基础。然而，在捕捉流程时，此类网需要用（可能重复的）活动进行标注，并配备沉默变迁以建模与流程编排相关的内部、未被记录的步骤。同时，它们必须在有限迹语义下进行分析，以契合每次流程执行由有限多个步骤组成这一事实。这两个方面阻碍了现有随机 Petri 网技术的直接应用，亟需一种在有限迹语义中纳入标注与沉默变迁的新刻画。本文从广义随机 Petri 网出发，得到标注随机流程（LSPs）框架，提供了这样一种刻画。在此框架之上，我们引入了关于 LSPs 的迹及其概率的若干关键分析任务。我们证明所有此类分析任务均可解析求解，具体将其归约为一种单一方法，该方法结合了基于自动机的技木以在 LSP 内甄别感兴趣的行为，以及基于吸收 Markov 链的技术以推理其概率。最后，我们展示了我们的方法在随机一致性检查背景下的意义，并通过概念验证实现及其在不同数据集上的应用说明了实际可行性。