Workflow modeling based on colored Petri nets and its soundness analysis

Due to the poor expression ability and difficulty to verify the soundness of workflow model, the paper maps the workflow notion defined by Workflow Management Coalition (WfMC) to WorkFlow net (WF-net). Through applying unified resource manager and the introduction of colored Petri net, the paper gets colored WF-net, which is simple and easy to computerize. Based on the definition of two adjustment mappings, which are proved not to destroy structure properties and system behaviors, the paper adjust the WF-net to a complete Extended Free Choice net (EFC-net). After adjustment, the soundness of all WF-net models can be verified in polynomial time.