Property-Transition-Net-Based Workflow Process Modeling and Verification 1

The development of workflow management system requires satisfactory models and concepts. As mentioned in [W.M.P. van der Aalst and Arthur H.M.ter Hofstede, YAWL: Yet Another Workflow Language, QUT Technical report, FIT-TR-2002-06, Queensland University of Technology, Brisbane, 2002], classical Petri nets are not suitable to describe some advanced workflow patterns, thus this paper presents a Petri-net-based model characterized by places with new properties which are suitable to represent some advance workflow patterns. Many workflow models confuse the behaviors of workflow engine and external environment(tasks), and fail to describe the real semantics of workflow engine. In our model, through separating transitions from routings, the place will describe the behaviors of engine and the transition will describe the behavior of task. Because workflow engine is a reactive system, the token-game semantic behavior of a Petri net-based workflow model will differ from its behavior at run time. However, the semantics of property-transition-net-based model with ST firing rules is suitable enough to capture the behavior of workflow process. In this paper the formal definitions and semantics of this model are discussed in detail. This paper concludes with an introduction of a verification technique for structure-soundness detection based on some new reduction rules.