永续自由选择网中的标识完全由其使能变迁刻画
计算机科学中的逻辑
2020-09-10 v3
摘要
一个带标识的Petri网若任意两个不同可达标识都不使能同一组变迁,即状态完全由其所使能的变迁刻画,则称其为lucent。本文探讨了lucent的带标识Petri网类,并证明永续带标识自由选择网是lucent。永续自由选择网是活的、有界的且拥有一个家簇的自由选择Petri网,即存在一个簇使得从任意可达状态出发都存在一个可达状态标记该簇的位置。永续网中的家簇充当过程的“再生点”,例如用于启动一个新的过程实例(案例、作业、周期等)。许多“良行为”过程模型属于此类。例如,短路健全工作流网类是永续的。此外,满足过程发现的 算法条件的过程类也属于此范畴。本文表明,永续带标识自由选择网中的状态完全由其所使能的变迁刻画,即这些过程模型是lucent。在状态与可发生动作之间具有一一对应,在多种应用领域中都具有价值。以使能变迁对标识的完全刻画使得永续自由选择网在工作流分析和过程挖掘中颇具意义。事实上,我们预期针对所识别的子类将出现新的验证、过程发现和一致性检验技术。
引用
@article{arxiv.1801.04315,
title = {Markings in Perpetual Free-Choice Nets Are Fully Characterized by Their Enabled Transitions},
author = {Wil M. P. van der Aalst},
journal= {arXiv preprint arXiv:1801.04315},
year = {2020}
}
备注
The proof of Theorem 3 has been changed. The original proof was incomplete. The original proof could be completed, but this complicates things and turns out to be rather indirect. Therefore, the new proof uses a more direct and self-contained approach