Dynamic Soundness in Resource-Constrained Workflow Nets

Abstract : Workflow Petri nets (wf-nets) are an important formalism for the modeling of business processes. For them we are typically interested in the soundness problem, that intuitively consists in deciding whether several concurrent executions can always terminate properly. Resource-Constrained Workflow Nets (rcfw-nets) are wf-nets enriched with static places, that model global resources. In this paper we prove the undecidability of soundness for rcwf-nets when there may be several static places and in which instances are allowed to terminate having created or consumed resources. In order to have a clearer presentation of the proof, we define an asynchronous version of a class of Petri nets with dynamic name creation. Then, we prove that reachability is undecidable for them, and reduce it to dynamic soundness in rcwf-nets. Finally, we prove that if we restrict our class of rcwf-nets, assuming in particular that a single instance is sound when it is given infinitely many global resources, then dynamic soundness is decidable by reducing it to the home space problem in P/T nets for a linear set of markings.
Complete list of metadatas

Cited literature [11 references]  Display  Hide  Download

Contributor : Hal Ifip <>
Submitted on : Thursday, September 7, 2017 - 11:10:15 AM
Last modification on : Friday, September 29, 2017 - 2:36:04 PM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



María Martos-Salgado, Fernando Rosa-Velardo. Dynamic Soundness in Resource-Constrained Workflow Nets. 13th Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 31th International Conference on FORmal TEchniques for Networked and Distributed Systems (FORTE), Jun 2011, Reykjavik,, Iceland. pp.259-273, ⟨10.1007/978-3-642-21461-5_17⟩. ⟨hal-01583317⟩



Record views


Files downloads