О разрешимости бездефектности для сетей потоков работ с неограниченным ресурсом

Рассматривается моделирование схем потоков работ (workflow) при помощи сетей Петри. Определяется класс сетей потоков работ с ресурсами (RWF- сетей) — обычных workflow-сетей, в которых дополнительно добавлено множество ресурсных позиций, содержащих какую-то начальную разметку (начальный ресурс). Ресурсы могут уничтожаться и производиться при срабатываниях переходов. Мы не накладываем ограничений ни на промежуточные, ни на финальные ресурсные разметки, поэтому сеть может порождать бесконечное множество различных достижимых состояний. RWF-сеть с данной начальной ресурсной разметкой называется бездефектной, если, во-первых, она всегда корректно завершает свою работу, и, во- вторых, любое увеличение начального ресурса не нарушает свойства корректного завершения. Неразмеченная RWF-сеть бездефектна, если она бездефектна при некоторой начальной ресурсной разметке. В данной работе доказана разрешимость обоих вариантов бездефектности для важного подкласса RWF- сетей — сетей с одномерным ресурсом (одной ресурсной позицией). Также представлен алгоритм вычисления наименьшего бездефектного ресурса.

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.