Article Preview
Top1. Introduction
Process models are widely used to model how an organization conducts its activities to accomplish its goals. In that sense, process models are a widely used type of conceptual models. Process modeling is a complicated task and, hence, error-prone (e.g., Sadiq & Orlowska, 1997; Mendling, 2007). The syntax of process modeling languages specifies how to compose their constructs (which often have graphical notation) into process models. However, syntactically correct process models are not necessarily meaningful in terms of conveying the way the business conducts its activities. Moreover, a syntactically correct model might not even be feasible to execute, and even if it is, it cannot always be assured to reach its goal, namely, produce its required outcome. Some meaning can be represented in a process model via the semantics of the modeling language used. These semantics are believed to represent some real-world phenomena, and can be defined textually or mathematically. Either representation may have shortcomings. Textual definitions are typically semi-formal or informal (e.g., “An event is something that “happens” during the course of a business process” (Object Management Group, 2006)), and therefore do not provide representations that are sufficiently precise for formal analysis. In contrast, mathematically-based process representations (e.g., Petri nets (Petri, 1962), YAWL (van der Aalst & ter Hofstede, 2005), Pi Calculus (Milner, Parrow & Walker, 1992)), allow formal analysis and automated verification of models, but their semantics may not be readily associated with the problem domain.
Much effort has been devoted to the formal analysis and verification of process models, leading to methods and tools for analyzing structural properties of process models and for detecting logical problems in them. In particular, Workflow nets (WF-nets)—a special case of Petri nets—have been proposed as tools for modeling the dynamics of processes (van der Aalst, 1998). A Workflow net is a Petri net which (1) has one input place and one output place; and (2) does not contain dangling transitions or places (namely, transitions that might not fire or places that might not be populated). This is equivalent to the net being strongly connected if the output place is interlinked to the input place via an additional transition (van der Aalst, 1998). Workflow nets employ a small set of constructs, yet possess an impressive expressive power and can be used to represent precisely the entire set of workflow patterns (van der Aalst et. al, 2003, Russel et al., 2006).
An extensive body of work exists regarding the mathematical, structural, and behavioral properties of Petri nets, such as free choice, liveness, boundedness and strong connectedness (e.g., Esparza & Silva, 1990; Jensen, 1990; Desel & Esparza, 1995). These properties have been adapted for WF nets, and additional properties (such as soundness, relating to the process dynamics) have been defined (e.g., van der Aalst, 2000). Furthermore, these properties serve for formalizing and analyzing models in other process modeling languages (such as in EPC (van der Aalst, 1999) and in general workflow (van Hee et al., 2008).