Soundness for Resource-Constrained Workflow Nets Is Decidable

We investigate the verification of the soundness property for workflow nets (WF-nets) extended with resources, thereby considering the most general instance of soundness, which requires that, for any number of instances, the WF-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.