2014 | OriginalPaper | Buchkapitel
Decidability of \(k\)-Soundness for Workflow Nets with an Unbounded Resource
Autoren: Vladimir A. Bashkin, Irina A. Lomazova
Verlag: Springer Berlin Heidelberg
Abstract
A resource workflow net (RWF-net) is a workflow net, supplied with an additional set of initially marked resource places. Resources can be consumed and/or produced by transitions. Neither the intermediate nor final resource markings are constrained, hence a net can have an infinite number of different reachable states.
An RWF-net with \(k\) tokens in the initial place and a certain number of resource tokens in resource places is called \(k\)-sound if it properly terminates with \(k\) tokens in the final place and, moreover, adding any extra initial resource does not violate its proper termination. An unmarked RWF-net is \(k\)-sound if it is \(k\)-sound for some initial resource. In this paper we prove the decidability of both marked and unmarked \(k\)-soundness for a restricted class of RWF-nets with a single unbounded resource place (1-dim RWF-nets). We present an algorithm for computing the minimal \(k\)-sound resource for a given sound 1-dim RWF-net.
