Graphical and logical formalisms for business process modeling and verification

Process models are an essential component of business process management and are found in various information systems such as workflow management systems, enterprise resource planning systems, and supply chain management systems. Process modeling and analysis are key steps in business process management. However, most existing activity-based process modeling paradigms found in process management tools lack a mathematical formalism, have limited expressive power, or have little analytical capability. Consequently, process modeling and analysis in the industry remain an art rather than a science.; In this dissertation, we first propose a logic-based workflow verification approach by applying propositional logic with constraints to verifying the correctness of both acyclic and cyclic workflow models. We demonstrate that this approach is capable of detecting process anomalies in workflow models.; We then propose process graphs as a graphical and mathematical tool for business process modeling and analysis. We formally define the syntax and semantics of process graphs and their constructs. We show that process graphs can not only model all types of execution order of activities, but also support of process models. We apply process graphs to defining and classifying process anomalies, and demonstrate that the proper use of process graphs can prevent certain process anomalies.; We also propose process logic as a logical formalism and mathematical method to represent process models for the purpose of process verification. We formally define the syntax and semantics of process logic to reflect the characteristics of process structures in a more precise way. We establish a formal relationship between process logic and graphical representations of process models, and transform the problem of verifying the correctness of process models into the problem of determining the validity of process argument forms in process logic. We demonstrate that process logic can be used to verify completely the correctness of activity-based process models.; Process graphs and process logic provide a theoretical foundation for the modeling, analysis, and verification of activity-based process models that are most widely used in the applications of business process management.