Priority Workflow Nets

This paper proposes priority (resource-constrained) workflow nets (WF nets) as Petri-net-based models of (resource-constrained) workflows with priorities between tasks. It is shown that the soundness problem (behavioral correctness criterion) is undecidable for priority (resource-constrained) WF nets. If supplementary conditions are imposed, soundness for priority (resource-constrained) WF nets can be reduced to soundness for their underlying (resource-constrained) WF nets. Two such conditions are proposed in this paper. One of them generalizes the well-known EQUAL-conflict condition for priority Petri nets, and the other one generalizes the conflict-freeness condition for Petri nets. Using the Petri net path logic, it is shown that both conditions are decidable. Finally, a generalization of the priority relation is proposed, which allows for a broader spectrum of workflow modeling. The results aforementioned also hold in this case.