Resource-Constrained Workflow Nets

We study concurrent processes modelled as workflow Petri nets extended with resource constraints. We define a behavioural correctness criterion called soundness: given a sufficient initial number of resources, all cases in the net are guaranteed to terminate successfully, no matter which schedule is used. We give a necessary and sufficient condition for soundness and an algorithm that checks it.

• Type: Journal
• Year: 2006
• Where: FUIN
• Authors: Kees M. van Hee, Natalia Sidorova, Marc Voorhoeve
• Keywords: Behavioural Correctness Criterion, FUIN 2006, Sufficient Initial Number, Workflow Petri Nets