In: A. Banks Pidduck, J. Mylopoulos, C.C. Woo, M. Tamer Ozsu (Eds.): Advanced Information Systems Engineering, 14th International Conference, CAiSE 2002 Toronto, Canada, May 27-31, 2002, pages 1-535pp. Springer Verlag, LNCS 2348, May 2002.
Abstract: At the CAiSE conference in Heidelberg in 1999, Wasim Sadiq and Maria Orlowska presented an algorithm to verify workflow graphs [19]. The algorithm uses a set of reduction rules to detect structural conflicts. This paper shows that the set of reduction rules presented in [19] is not complete and proposes an alternative algorithm. The algorithm translates workflow graphs into so-called WF-nets. WF-nets are a class of Petri nets tailored towards workflow analysis. As a result, Petri-net theory and tools can be used to verify workflow graphs. In particular, our workflow verification tool Woflan can be used to detect design errors. It is shown that the absence of structural conflicts, i.e., deadlocks and lack of synchronization, conforms to soundness of the corresponding WF-net. In contrast to the algorithm presented in [19], the algorithm presented in this paper is complete. Moreover, the complexity of this alternative algorithm is given.