In: Gianfranco Ciardo, Philippe Darondeau (Eds.): Lecture Notes in Computer Science, Vol. 3536: Applications and Theory of Petri Nets 2005: 26th International Conference, ICATPN 2005, Miami, USA, June 20-25, 2005., pages 250-267. Springer Verlag, June 2005.
Abstract: 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.
Keywords: Petri nets; concurrency; workflow; resources; verification.