Soundness of Workflow Nets with an Unbounded Resource is Decidable

P. 61–75.

Vladimir A. Bashkin, Ломазова И. А.

In this work we consider 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 do not 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 and, moreover, adding any extra initial resource does not violate itsproper 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.

Ключевые слова: workflow modeling, Petri nets, soundness, resources, workflow nets

ПУБЛИКАЦИЯ ПОДГОТОВЛЕНА ПО РЕЗУЛЬТАТАМ ПРОЕКТА: Разработка и исследование многоуровневого ресурсно-ориентированного формализма для моделирования и анализа мультиагентных систем с динамической структурой (2012)

В книге

Joint Proceedings of the International Workshop on Petri Nets and Software Engineering (PNSE'13) and the International Workshop on Modeling and Business Environments (ModBE'13). Satellite events of the 34th International Conference on Application and Theory of Petri Nets and Concurrency. Milano, Italy, June, 2013

Vol. 989: CEUR Workshop Proceedings. , [б.и.], 2013.