?
Decidability of k-Soundness for Workflow Nets with an Unbounded Resource
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.