On the Decidability of Soundness of Workflow Nets with an Unbounded Resource
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 fin...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Yaroslavl State University
2013-01-01
|
| Series: | Моделирование и анализ информационных систем |
| Subjects: | |
| Online Access: | http://mais-journal.ru/jour/article/view/182 |
| _version_ | 1797966686676058112 |
|---|---|
| author | V. A. Bashkin I. A. Lomazova |
| author_facet | V. A. Bashkin I. A. Lomazova |
| author_sort | V. A. Bashkin |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-11T02:19:15Z |
| format | Article |
| id | doaj.art-49ca191044a046959003c0e64b595e69 |
| institution | Directory Open Access Journal |
| issn | 1818-1015 2313-5417 |
| language | English |
| last_indexed | 2024-04-11T02:19:15Z |
| publishDate | 2013-01-01 |
| publisher | Yaroslavl State University |
| record_format | Article |
| series | Моделирование и анализ информационных систем |
| spelling | doaj.art-49ca191044a046959003c0e64b595e692023-01-03T00:14:58ZengYaroslavl State UniversityМоделирование и анализ информационных систем1818-10152313-54172013-01-012042340176On the Decidability of Soundness of Workflow Nets with an Unbounded ResourceV. A. Bashkin0I. A. Lomazova1Ярославский государственный университет им. П. Г. ДемидоваНациональный исследовательский университет “Высшая школа экономики”; Институт программных систем РАН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.http://mais-journal.ru/jour/article/view/182сети Петрипотоки работресурсбездефектностьверификациямоделирование |
| spellingShingle | V. A. Bashkin I. A. Lomazova On the Decidability of Soundness of Workflow Nets with an Unbounded Resource Моделирование и анализ информационных систем сети Петри потоки работ ресурс бездефектность верификация моделирование |
| title | On the Decidability of Soundness of Workflow Nets with an Unbounded Resource |
| title_full | On the Decidability of Soundness of Workflow Nets with an Unbounded Resource |
| title_fullStr | On the Decidability of Soundness of Workflow Nets with an Unbounded Resource |
| title_full_unstemmed | On the Decidability of Soundness of Workflow Nets with an Unbounded Resource |
| title_short | On the Decidability of Soundness of Workflow Nets with an Unbounded Resource |
| title_sort | on the decidability of soundness of workflow nets with an unbounded resource |
| topic | сети Петри потоки работ ресурс бездефектность верификация моделирование |
| url | http://mais-journal.ru/jour/article/view/182 |
| work_keys_str_mv | AT vabashkin onthedecidabilityofsoundnessofworkflownetswithanunboundedresource AT ialomazova onthedecidabilityofsoundnessofworkflownetswithanunboundedresource |