One-dimensional Resource Workow Nets
Workflow Petri nets with an additional (unbounded) resource place are studied. Resource tokens can be consumed and/or produced by transitions, hence a net can have an infinite number of different reachable states. A net with a certain initial resource is called sound if it properly terminates and, moreover, adding any extra initial resource does not violate its proper termination. An (unmarked) net is sound if it is sound for some initial resource. We prove the decidability of both marked and unmarked soundness for one-dimensional workow nets and present an algorithm of the minimal sound resource calculation.