Soundness of Workflow Nets with an Unbounded Resource is Decidable
In this work we consider modeling of workﬂow systems with Petri nets. A resource workﬂow net (RWF-net) is a workﬂow net, supplied with an additional set of initially marked resource places. Resources can be consumed and/or produced by transitions. We do not constrain neither the intermediate nor ﬁnal resource markings, hence a net can have an inﬁnite number of diﬀerent reachable states.
An initially marked RWF-net is called sound if it properly terminates and, moreover, adding any extra initial resource does not violate itsproper termination. An (unmarked) RWF-net is sound if it is sound for some initial resource. In this paper we prove the decidability of both marked and unmarked 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 sound resource for a given sound 1-dim RWF-net.