maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2013-4-23-40mais-182Research ArticleОригинальные статьиArticlesО разрешимости бездефектности для сетей потоков работ с неограниченным ресурсомOn the Decidability of Soundness of Workflow Nets with an Unbounded ResourceБашкинВладимир АнатольевичBashkinV. A.

канд. физ.-мат. наук, доцент,

150000 Россия, г. Ярославль, ул. Советская, 14

канд. физ.-мат. наук, доцент,

Sovetskaya str., 14, Yaroslavl, 150000, Russia

v_bashkin@mail.ruЛомазоваИрина АлександровнаLomazovaI. A.

д-р физ.-мат. наук, профессор,

101000 Россия, г. Москва, ул. Мясницкая, д. 20;

зав. международной научно-учебной лабораторией процессно-ориентированных информационных систем, гл. науч. сотр.,

152021 Россия, Ярославская обл., Переславский р-н, с. Веськово, ул. Петра I, д. 4 «а»

д-р физ.-мат. наук, профессор,

ul. Myasnitskaya, 20, Moskva, 101000 Russia;

зав. международной научно-учебной лабораторией процессно-ориентированных информационных систем, гл. науч. сотр.,

Pereslavl-Zalessky, Yaroslavl Region, 152020 Russia

i_lomazova@mail.ruЯрославский государственный университет им. П. Г. ДемидоваРоссияP.G. Demidov Yaroslavl State UniversityRussian FederationНациональный исследовательский университет “Высшая школа экономики”; Институт программных систем РАНРоссияNational research university "Higher school of economics"; Program Systems Institute of RASRussian Federation2013200820132042340Copyright © Башкин В.А., Ломазова И.А., 20132013Башкин В.А., Ломазова И.А.Bashkin V.A., Lomazova I.A.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/182

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

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.

сети Петрипотоки работресурсбездефектностьверификациямоделированиеPetri netsworkflowresourcesoundnessverificationmodelingРФФИ, Программа "Научные и научно-педагогические кадры инновационной России”Referencesван дер Аалст В., ван Хей К. Управление потоками работ: модели, методы и системы. М.: Научный мир, 2007. (English: van der Aalst W. M. P., van Hee K. M. Workflow Management: Models, Methods and Systems. MIT Press, 2002.)ван дер Аалст В., ван Хей К. Управление потоками работ: модели, методы и системы. М.: Научный мир, 2007. (English: van der Aalst W. M. P., van Hee K. M. Workflow Management: Models, Methods and Systems. MIT Press, 2002.)Башкин В. А. Формализация семантики систем с ненадежными агентами // Программирование. 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.)Башкин В. А. Формализация семантики систем с ненадежными агентами // Программирование. 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.)Котов В. Е. Сети Петри. М.: Наука, 1984. (Kotov V. E. Seti Petri. Moskva: Nauka, 1984 [in Russian].)Котов В. Е. Сети Петри. М.: Наука, 1984. (Kotov V. E. Seti Petri. Moskva: Nauka, 1984 [in Russian].)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.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.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.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.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.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.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.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.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.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.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.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.Bashkin V. A., Lomazova I. A. Petri Nets and resource bisimulation // Fundamenta Informaticae. 2003. Vol. 55, No 2, P. 101–114.Bashkin V. A., Lomazova I. A. Petri Nets and resource bisimulation // Fundamenta Informaticae. 2003. Vol. 55, No 2, P. 101–114.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.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.Chrz¸astowski-Wachtel P. Sound Markings in Structured Nets // Proc. of Concurrency, Specification and Programming (CS&P’2005). Warsaw University, 2005. P. 71–85.Chrz¸astowski-Wachtel P. Sound Markings in Structured Nets // Proc. of Concurrency, Specification and Programming (CS&P’2005). Warsaw University, 2005. P. 71–85.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.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.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.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.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.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.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.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.Hopcroft J., Pansiot J.-J. On the reachability problem for 5-dimensional vector addition systems // Theoretical Computer Science. 1979. 8(2). P. 135–159.Hopcroft J., Pansiot J.-J. On the reachability problem for 5-dimensional vector addition systems // Theoretical Computer Science. 1979. 8(2). P. 135–159.Lomazova I.A. Nested Petri Nets for Adaptive Process Modeling // Lecture Notes in Computer Science. 2008. Vol. 4800. P. 460–474.Lomazova I.A. Nested Petri Nets for Adaptive Process Modeling // Lecture Notes in Computer Science. 2008. Vol. 4800. P. 460–474.Petri C. A. Kommunikation mit Automaten. Phd thesis. Bonn, Institute f¨ur Instrumentelle Mathematik. 1962.Petri C. A. Kommunikation mit Automaten. Phd thesis. Bonn, Institute f¨ur Instrumentelle Mathematik. 1962.Sidorova N., Stahl C. Soundness for Resource-Contrained Workflow Nets is Decidable // BPM Center Report BPM-12-09. BPMcenter.org. 2012.Sidorova N., Stahl C. Soundness for Resource-Contrained Workflow Nets is Decidable // BPM Center Report BPM-12-09. BPMcenter.org. 2012.Tiplea F. L., Marinescu D. C. Structural soundness of workflow nets is decidable // Information Processing Letters. 2005. Vol. 96. P. 54–58.Tiplea F. L., Marinescu D. C. Structural soundness of workflow nets is decidable // Information Processing Letters. 2005. Vol. 96. P. 54–58.

The authors declare that there are no conflicts of interest present.