On the Decidability of Soundness of Workflow Nets with an Unbounded Resource
https://doi.org/10.18255/1818-1015-2013-4-23-40
Abstract
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.
About the Authors
V. A. Bashkin
P.G. Demidov Yaroslavl State University
Russian Federation
Russian Federation
канд. физ.-мат. наук, доцент,
Sovetskaya str., 14, Yaroslavl, 150000, Russia
I. A. Lomazova
National research university "Higher school of economics";
Program Systems Institute of RAS
Russian Federation
Russian Federation
д-р физ.-мат. наук, профессор,
ul. Myasnitskaya, 20, Moskva, 101000 Russia;
зав. международной научно-учебной лабораторией процессно-ориентированных информационных систем, гл. науч. сотр.,
Pereslavl-Zalessky, Yaroslavl Region, 152020 Russia
References
1. ван дер Аалст В., ван Хей К. Управление потоками работ: модели, методы и системы. М.: Научный мир, 2007. (English: van der Aalst W. M. P., van Hee K. M. Workflow Management: Models, Methods and Systems. MIT Press, 2002.)
2. Башкин В. А. Формализация семантики систем с ненадежными агентами // Программирование. 2010. Т. 36. №4. C. 3–15. (English transl.: Bashkin V. A. Formalization of semantics of systems with unreliable agents by means of nets of active resources // Programming and Computer Software. 2010. 36(4). P. 187–196.)
3. Котов В. Е. Сети Петри. М.: Наука, 1984. (Kotov V. E. Seti Petri. Moskva: Nauka, 1984 [in Russian].)
4. van der Aalst W. M. P. The Application of Petri Nets to Workflow Management // The Journal of Circuits, Systems and Computers. 1998. 8(1). P. 21–66.
5. van der Aalst W. M. P., van Hee K. M., Hofstede A. H. M., Sidorova N., Verbeek H. M. W., Voorhoeve M., Wynn M. T. Soundness of workflow nets: classification, decidability, and analysis // Formal Aspects of Computing. 2011. 23(3). P. 333–363.
6. Abdulla P. A., Cerans K. ˇ Simulation is decidable for one-counter nets // Proc. of CONCUR’98. Lecture Notes in Computer Science. 1998. Vol. 1466. P. 253–268.
7. Barkaoui K., Petrucci L. Structural Analysis of Workflow Nets with Shared Resources // Proc. of Workflow Management: Net-based Concepts, Models, Techniques and Tools (WFM98). Computing Science Reports. Eindhoven University of Technology. 1998. Vol. 98/7. P. 82–95.
8. Barkaoui K., Ben Ayed R., Sba¨ı Z. Workflow Soundness Verification based on Structure Theory of Petri Nets // International Journal of Computing and Information Sciences. 2007. 5(1). P. 51–61.
9. Bashkin V. A., Lomazova I. A. Resource Similarities in Petri Net Models of Distributed Systems // Proc. of PaCT 2003. Lecture Notes in Computer Science. 2003. Vol. 2763. P. 35–48.
10. Bashkin V. A., Lomazova I. A. Petri Nets and resource bisimulation // Fundamenta Informaticae. 2003. Vol. 55, No 2, P. 101–114.
11. Bashkin V. A., Lomazova I. A. Resource equivalence in workflow nets // Proc. of Concurrency, Specification and Programming (CS&P’2006). Humboldt Universitat zu Berlin, 2006. Vol. 1. P. 80–91.
12. Chrz¸astowski-Wachtel P. Sound Markings in Structured Nets // Proc. of Concurrency, Specification and Programming (CS&P’2005). Warsaw University, 2005. P. 71–85.
13. Dickson L. E. Finiteness of the Odd Perfect and Primitive Abundant Numbers with n Distinct Prime Factors // American Journal of Mathematics. 1913. Vol. 35, No 4. P. 413–422.
14. van Hee K., Sidorova N., Voorhoeve M. Generalized Soundness of Workflow Nets is Decidable // Proc. of ICATPN 2004. Lecture Notes in Computer Science. 2004. Vol. 3099. P. 197–216.
15. van Hee K., Serebrenik A., Sidorova N., Voorhoeve M. Soundness of Resource-Constrained Workflow Nets // Proc. of ICATPN 2005. Lecture Notes in Computer Science. 2005. Vol. 3536. P. 250–267.
16. van Hee K., Oanea O., Serebrenik A., Sidorova N., Voorhoeve M., Lomazova I. A. Checking Properties of Adaptive Workflow Nets // Fundamenta Informaticae. 2007. Vol. 79, No 3. P. 347–362.
17. Hopcroft J., Pansiot J.-J. On the reachability problem for 5-dimensional vector addition systems // Theoretical Computer Science. 1979. 8(2). P. 135–159.
18. Lomazova I.A. Nested Petri Nets for Adaptive Process Modeling // Lecture Notes in Computer Science. 2008. Vol. 4800. P. 460–474.
19. Petri C. A. Kommunikation mit Automaten. Phd thesis. Bonn, Institute f¨ur Instrumentelle Mathematik. 1962.
20. Sidorova N., Stahl C. Soundness for Resource-Contrained Workflow Nets is Decidable // BPM Center Report BPM-12-09. BPMcenter.org. 2012.
21. Tiplea F. L., Marinescu D. C. Structural soundness of workflow nets is decidable // Information Processing Letters. 2005. Vol. 96. P. 54–58.
Review
For citations:
Bashkin V.A., Lomazova I.A. On the Decidability of Soundness of Workflow Nets with an Unbounded Resource. Modeling and Analysis of Information Systems. 2013;20(4):23-40. (In Russ.) https://doi.org/10.18255/1818-1015-2013-4-23-40
Views:
1008
Email this article 