Syntax and Semantics of Workflows That Include Passbacks

The questions of how to represent passbacks (redoing) of work in a workflow and of what semantics to apply to passbacks comprise an important issue in workflow research. In this paper, cyclic workflows are regarded as workflows with passbacks, and the normal form of a workflow is defined from properties of workflows as graphs. For a normal workflow, semantics based on passbacks is defined as a transition system on subgraphs of the workflow. Based on the transition system, this paper defines total correctness of a workflow with passbacks. Furthermore, this paper proves that total correctness of workflows with passbacks, defined in this paper, is a natural extension of the conventional correctness of acyclic workflows. This paper also shows that the correctness of a normal workflow amounts to the correctness of the acyclic sub-workflows included in the normal workflow.