Soundness for resource-constrained workflow nets is decidable

We investigate the verification of the soundness property for workflow nets extended with resources, thereby considering the most general instance of soundness, which requires that for any number of instances, the workflow net has always the possibility to terminate, for a certain initial (finite) number of resource items per resource type; moreover, adding additional resources to a sound net does not violate the result. We prove that this problem is decidable by reducing it to a home-space problem, and we show how soundness can be decided by using the procedure for deciding a home-space property.