Geodesic
On the Decidability of Soundness of Workflow Nets with an Unbounded Resource
Modelirovanie i analiz informacionnyh sistem, Tome 20 (2013) no. 4, pp. 23-40.

Voir la notice de l'article provenant de la source Math-Net.Ru

In this work, we consider the modeling of workflow systems with Petri nets. A resource workflow net (RWF-net) is a workflow net supplied with an additional set of initially marked resource places. Resources can be consumed and/or produced by transitions. We constrain neither the intermediate nor final resource markings, hence a net can have an infinite number of different reachable states. An initially marked RWF-net is called sound if it properly terminates its work and, moreover, an increase of the initial resource does not violate its proper termination. An unmarked RWF-net is sound if it is sound for some initial resource. In this paper, we prove the decidability of both marked and unmarked soundness for a restricted class of RWF-nets with a single unbounded resource place (1-dim RWF-nets). We present an algorithm for computing the minimal sound resource for a given sound 1-dim RWF-net.
Keywords: Petri nets, workflow, resource, soundness, verification, modeling. 
@article{MAIS_2013_20_4_a1,
     author = {V. A. Bashkin and I. A. Lomazova},
     title = {On the {Decidability} of {Soundness} of {Workflow} {Nets} with an {Unbounded} {Resource}},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {23--40},
     publisher = {mathdoc},
     volume = {20},
     number = {4},
     year = {2013},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2013_20_4_a1/}
}
TY  - JOUR
AU  - V. A. Bashkin
AU  - I. A. Lomazova
TI  - On the Decidability of Soundness of Workflow Nets with an Unbounded Resource
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2013
SP  - 23
EP  - 40
VL  - 20
IS  - 4
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2013_20_4_a1/
LA  - ru
ID  - MAIS_2013_20_4_a1
ER  - 
%0 Journal Article
%A V. A. Bashkin
%A I. A. Lomazova
%T On the Decidability of Soundness of Workflow Nets with an Unbounded Resource
%J Modelirovanie i analiz informacionnyh sistem
%D 2013
%P 23-40
%V 20
%N 4
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2013_20_4_a1/
%G ru
%F MAIS_2013_20_4_a1
V. A. Bashkin; I. A. Lomazova. On the Decidability of Soundness of Workflow Nets with an Unbounded Resource. Modelirovanie i analiz informacionnyh sistem, Tome 20 (2013) no. 4, pp. 23-40. http://geodesic.mathdoc.fr/item/MAIS_2013_20_4_a1/

[1] W. M. P. van der Aalst, K. M. van Hee Workflow, Management: Models, Methods and Systems, MIT Press, 2002 | Zbl

[2] V. A. Bashkin, “Formalization of semantics of systems with unreliable agents by means of nets of active resources”, Programming and Computer Software, 36:4 (2010), 187–196 | DOI | Zbl

[3] Kotov V. E., Seti Petri, Nauka, M., 1984 (in Russian)

[4] W. M. P. van der Aalst, “The Application of Petri Nets to Workflow Management”, The Journal of Circuits, Systems and Computers, 8:1 (1998), 21–66 | DOI

[5] W. M. P. van der Aalst, K. M. van Hee, A. H. M. Hofstede, N. Sidorova, H. M. W. Verbeek, M. Voorhoeve, M. T. Wynn, “Soundness of workflow nets: classification, decidability, and analysis”, Formal Aspects of Computing, 23:3 (2011), 333–363 | DOI | Zbl

[6] P. A. Abdulla, K. Čerans, “Simulation is decidable for one-counter nets”, Proc. of CONCUR'98, Lecture Notes in Computer Science, 1466, 1998, 253–268 | DOI | Zbl

[7] K. Barkaoui, L. Petrucci, “Structural Analysis of Workflow Nets with Shared Resources”, Proc. of Workflow Management: Net-based Concepts, Models, Techniques and Tools (WFM98); Computing Science Reports, No 98/7, Eindhoven University of Technology, 1998, 82–95

[8] K. Barkaoui, R. Ben Ayed, Z. Sbaï, “Workflow Soundness Verification based on Structure Theory of Petri Nets”, International Journal of Computing and Information Sciences, 5:1 (2007), 51–61

[9] V. A. Bashkin, I. A. Lomazova, “Resource Similarities in Petri Net Models of Distributed Systems”, Proc. of PaCT 2003, Lecture Notes in Computer Science, 2763, 2003, 35–48 | DOI

[10] V. A. Bashkin, I. A.Lomazova, “Petri Nets and resource bisimulation”, Fundamenta Informaticae, 55:2 (2003), 101–114 | Zbl

[11] V. A. Bashkin, I. A.Lomazova, “Resource equivalence in workflow nets”, Proc. of Concurrency, Specification and Programming, CS'2006, v. 1, Humboldt Universitat zu Berlin, 2006, 80–91

[12] P. Chrza̧stowski-Wachtel, “Sound Markings in Structured Nets”, Proc. of Concurrency, Specification and Programming, CS'2005, Warsaw University, 2005, 71–85

[13] L. E. Dickson, “Finiteness of the Odd Perfect and Primitive Abundant Numbers with n Distinct Prime Factors”, American Journal of Mathematics, 35:4 (1913), 413–422 | DOI | Zbl

[14] K. van Hee, N. Sidorova, M. Voorhoeve, “Generalized Soundness of Workflow Nets is Decidable”, Proc. of ICATPN 2004, Lecture Notes in Computer Science, 3099, 2004, 197–216 | DOI

[15] K. van Hee, A. Serebrenik, N. Sidorova, M. Voorhoeve, “Soundness of Resource-Constrained Workflow Nets”, Proc. of ICATPN 2005, Lecture Notes in Computer Science, 3536, 2005, 250–267 | DOI | Zbl

[16] K. van Hee, O. Oanea, A. Serebrenik, N. Sidorova, M. Voorhoeve, I. A. Lomazova, “Checking Properties of Adaptive Workflow Nets”, Fundamenta Informaticae, 79:3 (2007), 347–362 | Zbl

[17] J. Hopcroft, J.-J. Pansiot, “On the reachability problem for 5-dimensional vector addition systems”, Theoretical Computer Science, 8:2 (1979), 135–159 | DOI | Zbl

[18] I. A. Lomazova, “Nested Petri Nets for Adaptive Process Modeling”, Lecture Notes in Computer Science, 4800, 2008, 460–474 | DOI | Zbl

[19] C. A. Petri, Kommunikation mit Automaten, Phd thesis, Institute für Instrumentelle Mathematik, Bonn, 1962

[20] N. Sidorova, C. Stahl, Soundness for Resource-Contrained Workflow Nets is Decidable, BPM Center Report BPM-12-09, , 2012 http://BPMcenter.org

[21] F. L. Tiplea, D. C.Marinescu, “Structural soundness of workflow nets is decidable”, Information Processing Letters, 96 (2005), 54–58 | DOI | Zbl