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.
|Title of host publication||Proceedings of Concurrency Specification and Programming (CS&P'2004, Caputh, Germany, September 24-26, 2004), Informatik-Bericht Nr.170|
|Place of Publication||Berlin, Germany|
|Publisher||Humboldt-Universität zu Berlin|
|Publication status||Published - 2004|