Dynamic Soundness in Resource-Constrained Workflow Nets - Formal Techniques for Distributed Systems
Conference Papers Year : 2011

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.
Fichier principal
Vignette du fichier
978-3-642-21461-5_17_Chapter.pdf (182.14 Ko) Télécharger le fichier
Origin Files produced by the author(s)
Loading...

Dates and versions

hal-01583317 , version 1 (07-09-2017)

Licence

Identifiers

Cite

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⟩
51 View
61 Download

Altmetric

Share

More