Soundness of workflow nets with reset arcs is undecidable!

W.M.P. Aalst, van der; K.M. Hee, van; A.H.M. Hofstede, ter; N. Sidorova; H.M.W. Verbeek; M. Voorhoeve; M.T. Wynn

Soundness of workflow nets with reset arcs is undecidable!

W.M.P. Aalst, van der, K.M. Hee, van, A.H.M. Hofstede, ter, N. Sidorova, H.M.W. Verbeek, M. Voorhoeve, M.T. Wynn

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

1 Downloads (Pure)

Abstract

Petri nets are often used to model and analyze workflows. Many workflow languages have been mapped onto Petri nets in order to provide formal semantics or to verify correctness properties. Typically, the so-called Workflow nets are used to model and analyze workflows and variants of the classical soundness property are used as a correctness notion. Since many workflow languages have cancelation features, a map- ping to workflow nets is not always possible. Therefore, it is interesting to consider workflow nets with reset arcs. Unfortunately, soundness is undecidable for workflow nets with reset arcs. In this paper, we provide a proof and insights into the theoretical limits of workflow verification.

Original language	English
Title of host publication	Proceedings of the International Workshop on Concurrency Methods Issues and Applications (CHINA'08)
Editors	J. Kleijn, M. Koutny
Pages	57-72
Publication status	Published - 2008

Cite this

@inproceedings{93fd2b5b637045e798c8752b7c152163,

title = "Soundness of workflow nets with reset arcs is undecidable!",

abstract = "Petri nets are often used to model and analyze workflows. Many workflow languages have been mapped onto Petri nets in order to provide formal semantics or to verify correctness properties. Typically, the so-called Workflow nets are used to model and analyze workflows and variants of the classical soundness property are used as a correctness notion. Since many workflow languages have cancelation features, a map- ping to workflow nets is not always possible. Therefore, it is interesting to consider workflow nets with reset arcs. Unfortunately, soundness is undecidable for workflow nets with reset arcs. In this paper, we provide a proof and insights into the theoretical limits of workflow verification.",

author = "\{Aalst, van der\}, W.M.P. and \{Hee, van\}, K.M. and \{Hofstede, ter\}, A.H.M. and N. Sidorova and H.M.W. Verbeek and M. Voorhoeve and M.T. Wynn",

year = "2008",

language = "English",

pages = "57--72",

editor = "J. Kleijn and M. Koutny",

booktitle = "Proceedings of the International Workshop on Concurrency Methods Issues and Applications (CHINA'08)",

}

Soundness of workflow nets with reset arcs is undecidable! / Aalst, van der, W.M.P.; Hee, van, K.M.; Hofstede, ter, A.H.M. et al.
Proceedings of the International Workshop on Concurrency Methods Issues and Applications (CHINA'08). ed. / J. Kleijn; M. Koutny. 2008. p. 57-72.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Soundness of workflow nets with reset arcs is undecidable!

AU - Aalst, van der, W.M.P.

AU - Hee, van, K.M.

AU - Hofstede, ter, A.H.M.

AU - Sidorova, N.

AU - Verbeek, H.M.W.

AU - Voorhoeve, M.

AU - Wynn, M.T.

PY - 2008

Y1 - 2008

N2 - Petri nets are often used to model and analyze workflows. Many workflow languages have been mapped onto Petri nets in order to provide formal semantics or to verify correctness properties. Typically, the so-called Workflow nets are used to model and analyze workflows and variants of the classical soundness property are used as a correctness notion. Since many workflow languages have cancelation features, a map- ping to workflow nets is not always possible. Therefore, it is interesting to consider workflow nets with reset arcs. Unfortunately, soundness is undecidable for workflow nets with reset arcs. In this paper, we provide a proof and insights into the theoretical limits of workflow verification.

AB - Petri nets are often used to model and analyze workflows. Many workflow languages have been mapped onto Petri nets in order to provide formal semantics or to verify correctness properties. Typically, the so-called Workflow nets are used to model and analyze workflows and variants of the classical soundness property are used as a correctness notion. Since many workflow languages have cancelation features, a map- ping to workflow nets is not always possible. Therefore, it is interesting to consider workflow nets with reset arcs. Unfortunately, soundness is undecidable for workflow nets with reset arcs. In this paper, we provide a proof and insights into the theoretical limits of workflow verification.

M3 - Conference contribution

SP - 57

EP - 72

BT - Proceedings of the International Workshop on Concurrency Methods Issues and Applications (CHINA'08)

A2 - Kleijn, J.

A2 - Koutny, M.

ER -

Soundness of workflow nets with reset arcs is undecidable!

Abstract

Fingerprint

Cite this