Workflow Properties

Wolfgang allows checking structural and soundness-related workflow properties:

Workflow-Net
A Workflow Net (WF-Net) is a Petri Net which has two structural properties (WF-
Structuredness):

  • A WF-net is a P/T-Net that has one input place (i) and one output place (o). A token in i corresponds to a case which needs to be handled, a token in o corresponds to a case which has been handled.
  • Every transition and place contributes to the processing of a case. Therefore, every transition t (place p) is located on a path from place i to place o (this corresponds to strongly connectedness if o is connected to i via an additional transition).

Based on the typical properties of a Petri Net and WF-structuredness, a WF-Net is
sound if and only if the following three requirements are satis ed:

  •  Option to complete: for each case it is always still possible to reach a state which marks end place (o).
  •  Proper completion: if o is marked all other places are empty for a given case.
  •  No dead transitions: it is possible to execute an arbitrary activity by following the appropriate route through the WF-Net.

Colored Workflow-Net
A ColoredWorkflow Net (CWN) is a bounded Colored Petri Net (CPN) which additionally satis es the structuredness properties of a WF-Net (where the token of a WF-Net is represented by the “black”-colored control flow token instead): The soundness of Colored Work ow Nets (CWN) is closely related to the soundness of WF-Nets. The formal de nitions of CWN-structuredness and -soundness may be found here.