Logic Based Approaches to Workflow Modeling and Verification

Saikat Mukherjee    Hasan Davulcu    Michael Kifer    Pinar Senkul    Guizhen Yang


A workflow is a collection of cooperating, coordinated activities designed to carry out a well-defined complex process, such as trip planning, graduate student registration, or a business process in a large enterprise. An activity in a workflow might be performed by a human, a device or a program. Workflow Management Systems (or WfMS) provide a framework for capturing the interaction among the activities in a workflow and are recognised as a new paradigm for integrating disparate systems, including legacy systems. A large workflow system might involve many disparate activities that are coordinated in complex ways and are subject to many constraints. Thus, modeling such systems and ensuring that they perform according to the specifications are not an easy task. To be able to analyze the properties of workflows, the latter must be specified using a formalism with a well-defined semantics. The popular formalisms in this area are the various logics, Petri Nets, Event-Condition-Action rules, and State Charts. In this paper we survey and compare a number of logic-based formalisms that were proposed in the literature.