In: van der Aalst, W.M.P.; Desel, J.; Oberweis, A.: Lecture Notes in Computer Science, Vol. 1806: Business Process Managements - models, techniques and empirical studies, pages 184-200. Springer-Verlag, 2000.
Abstract: Workflow processes are represented as Petri nets with special entry and exit places and labeled transitions. The transition labels represent actions. We give a semantics for such nets in terms of transition systems. This allow us to describe and verify properties like termination: the guaranteed option to terminate successfully. We describe the composition of complex WF nets from simpler ones by means of certain operators.The simple operators preserve termination, giving correctness by design. Only the advanced communication operators are potentially dangerous. A strategy for verification of other properties is described.