Workflow Verification and Polynomial Algorithm of Model Decomposition

Abstract:

This paper presents a new necessary and sufficient condition for the soundness of workflow model based on the Petri nets modeling techniques.Some properties of workflow net were analyzed and verified,such as the existence of Tinvariant and Pinvariant of the workflow net(WFnet),the sets of transitions and places be covered by Tinvariants and Pinvariants respectively. A polynomial algorithm of workflow model decomposition based on Tinvariant is presented.Compared with other exponential algorithms, the algorithm is simple, easy to understand and operate,and can also effectively simplify decomposition and analysis of the workflow systems. The effect of the paper’s research results is verfied with an example.