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/