Capturing stochastic behaviors in business and work processes is essential to quantitatively understand how nondeterminism is resolved when taking decisions within the process. This is of special interest in process mining, where event data tracking the actual execution of the process are related to process models, and can then provide insights on frequencies and probabilities. Variants of stochastic Petri nets provide a natural formal basis for this. However, when capturing processes, such nets need to be labelled with (possibly duplicated) activities, and equipped with silent transitions that model internal, non-logged steps related to the orchestration of the process. At the same time, they have to be analyzed in a finite-trace semantics, matching the fact that each process execution consists of finitely many steps. These two aspects impede the direct application of existing techniques for stochastic Petri nets, calling for a novel characterization that incorporates labels and silent transitions in a finite-trace semantics. In this article, we provide such a characterization starting from generalized stochastic Petri nets and obtaining the framework of labelled stochastic processes (LSPs). On top of this framework, we introduce different key analysis tasks on the traces of LSPs and their probabilities. We show that all such analysis tasks can be solved analytically, in particular reducing them to a single method that combines automata-based techniques to single out the behaviors of interest within a LSP, with techniques based on absorbing Markov chains to reason on their probabilities. Finally, we demonstrate the significance of how our approach in the context of stochastic conformance checking, illustrating practical feasibility through a proof-of-concept implementation and its application to different datasets.

翻译：捕捉业务流程中的随机行为对于定量理解在流程决策过程中非确定性的解决方式至关重要。这在过程挖掘中尤为关键——通过跟踪流程实际执行的事件数据与流程模型相关联，能够揭示频次与概率的深层洞察。随机Petri网的变体为此提供了自然的数学基础。然而，在建模流程时，这类网需要标注（可能重复的）活动，并配备用于模拟流程编排相关的内部非记录步骤的静默变迁。同时，必须基于有限迹语义进行分析，以匹配每次流程执行仅包含有限步骤的特性。这两个方面阻碍了现有随机Petri网技术的直接应用，亟需一种融入标签与静默变迁的有限迹语义新框架。本文从广义随机Petri网出发，构建了标签随机过程（LSP）分析框架。在此框架之上，我们提出了针对LSP迹及其概率的关键分析任务，并证明所有任务均可通过解析方法求解，特别是将其统一为融合自动机状态探索与吸收马尔可夫链概率推理的混合方法。最后，我们在随机符合性检查场景中验证了该方法的重要性，并通过概念验证实现及多数据集应用展示了其实用可行性。