Study on soundness of workflow model based on Petri net

Due to the difficulty of constructing sound workflow model, this paper maps the workflow model defined by workflow management coalition (WFMC) to workflow net (WF-net). Based on the definition of two adjustment mappings proved not to destroy structure properties and system behaviors, this paper adjust the WF-net to a complete extended free choice net (EFC-net). Proved the equivalent deadlock properties of EFC-net and free choice net (FC-net), this paper introduces an algorithm to obtain minimum deadlock. Finally, combined with rank theorem, an algorithm is given to verify whether a WF-net is soundness.