Model Checking Workflow Net Based on Petri Net

The soundness is a very important criterion for the correctness of the workflow. Specifying the soundness with Computation Tree Logic (CTL) allows us to verify the soundness with symbolic model checkers. Therefore the state explosion problem in verifying soundness can be overcome efficiently. When the property is not satisfied by the system, model checking can give a counter-example, which can guide us to correct the workflow. In addition, relaxed soundness is another important criterion for the workflow. We also prove that Computation Tree Logic* (CTL*) can be used to character the relaxed soundness of the workflow.