Workflow Model Verification Based on Matrix Transformation

Synchronet is a workflow model which hasthree layers, i.e. workflow logic, case semantics and workflow management. Throughness is an important propertyin workflow logic layer. As a simple and widely used technique, graph reduction method can be employed to verifyworkflow logic via reduction rules. However, the graph reduction method is low effcient and space-consuming. Inthis paper, a workflow logic verification method based onmatrix transformation is proposed to solve above problems. Firstly, the incidence matrix of workflow logic isgenerated by its net representation. Then, matrix transformations can be conducted according to rows characteristic and columns characteristic of the incidence matrix.Related algorithms are implemented and experiments areconducted. Experiment results show that this method ismore effcient and space-saving than the graph reductionmethod. Moreover, a worked example is provided to illustrate the transformation process.