Abstract: Workflow process modeling is a complicated and error-prone procedure. Thus, effective process verification in modeling phase is very essential. At present, the research on flexible workflow verification is very scarce. This paper explores in the field. This paper applies soundness verification and reduction verification to formal verification in flexible workflow process modeling based on interaction learning. Depiction of problems needed to be verified and their complexities are stated. This paper performs process soundness verification and reduction verification using Petri nets’ formal foundation characteristic. On the basis of reduction granularity, it applies atom level reduction and module level reduction to flexible workflow model based on interaction learning. The basic technologies of reduction are place fusion, transition fusion and subnet fusion. On the condition of characteristic retaining, the process model is reduced to appropriate size. The results show that formal verification methods in flexible workflow process modeling based on interaction learning are successful.

Key words: Workflow, Process modeling, Verification, Petri nets, Flexibility

摘要： 工作流过程建模是一个复杂且易错的过程，在建模阶段进行有效的过程验证是十分必要的。目前，柔性工作流验证领域的研究还比较欠缺，该文在这方面作了一些探索。把过程合理化验证和化简验证技术应用于基于交互学习的柔性工作流建模的形式化验证中，叙述了需要验证的问题和复杂度。利用Petri网的形式化基础特性对过程进行合理性验证和规约验证。根据规约粒度的不同，分别对基于交互学习的柔性工作流模型进行原子级和组件级规约。规约使用的基本技术有库所融合、变迁融合和子网融合。在特性保持的前提下，将过程模型缩小到适当规模。结果表明，基于交互学习的柔性工作流过程建模中的形式化验证方法具有一定的实用性和可操作性。

关键词: 工作流, 过程建模, 验证, Petri网, 柔性