Abstract: To make easier of the verification of workflow model based on Petri nets, this paper presents a method of verification of workflow model based on reduction techniques of Petri nets. Based on a rigorous analysis of various verification techniques of workflow model, a analysis method is given aiming at non-free choice parts of Petri nets. A transformation from live and bounded non-free choice part to free choice part is given which preserves liveness and boundness. The verification of arbitrary Petri nets including non-free choice Petri nets could be transferred to the verification of free choice Petri nets. An example is introduced to illustrate how to apply the analysis method to verify a application model.

Key words: Petri nets, Workflow, Correctness of model, Reduction techniques

摘要： 为了更有效地对工作流模型进行分析验证，提出了一种基于Petri网化简技术的工作流模型正确性验证方法。在对各种工作流模型验证技术深入研究的基础上，通过对非自由选择网结构活性和有界性的分析，给出了针对Petri网中非自由选择部分的分析方法。在保持活性和有界性的前提下，给出了将活的且有界的非自由选择部分转化为自由选择部分的转化方法，从而将非自由选择的Petri网验证问题转化为自由选择Petri网的验证问题。通过一个例子说明了如何使用该文提出的方法来验证模型的正确性。

关键词: Petri网, 工作流, 模型正确性, 化简技术

CLC Number: 

• TP301