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 Tinvariant and Pinvariant of the workflow net(WFnet),the sets of transitions and places be covered by Tinvariants and Pinvariants respectively. A polynomial algorithm of workflow model decomposition based on Tinvariant 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.