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.
Type de document :
Communication dans un congrès
Roberto Bruni; Juergen Dingel. 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. Springer, Lecture Notes in Computer Science, LNCS-6722, pp.259-273, 2011, Formal Techniques for Distributed Systems. 〈10.1007/978-3-642-21461-5_17〉
Liste complète des métadonnées

Littérature citée [11 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01583317
Contributeur : Hal Ifip <>
Soumis le : jeudi 7 septembre 2017 - 11:10:15
Dernière modification le : vendredi 29 septembre 2017 - 14:36:04

Fichier

978-3-642-21461-5_17_Chapter.p...
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

María Martos-Salgado, Fernando Rosa-Velardo. Dynamic Soundness in Resource-Constrained Workflow Nets. Roberto Bruni; Juergen Dingel. 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. Springer, Lecture Notes in Computer Science, LNCS-6722, pp.259-273, 2011, Formal Techniques for Distributed Systems. 〈10.1007/978-3-642-21461-5_17〉. 〈hal-01583317〉

Partager

Métriques

Consultations de la notice

33

Téléchargements de fichiers

9