Calculating the Order Relations of Workflow Net with Invariant Method

Workflow net is a popular formal notation for modeling workflow process. The order relation of the workflow net is the important information to describe the parallel relation, sequential relation and choice relation. From the state of the art of Petri net theory, there are two basic approaches for to analyze the order relations of the work-flow net: state space method and invariant method. State space method based on the reachability graph usually encounters the state space explosion problem. To avoid the state space explosion, we propose LMST-invariants according to the particularity of the workflow net, and calculate the order relations with invariant method.