Affordable Access

Publisher Website

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

Electronic Notes in Theoretical Computer Science
Publication Date
DOI: 10.1016/j.entcs.2005.12.067
  • Business Process Modeling
  • Verification Of Process Model
  • Workflow Pattern
  • Property Transition Nets
  • Linguistics


Abstract 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.

There are no comments yet on this publication. Be the first to share your thoughts.