Stepwise structural verification of cyclic workflow models with acyclic decomposition and reduction of loops

Existence of cycles (or loops) is one of the main sources that make the analysis of workflow models difficult. Several approaches of structural verification exist in the literature, but how to verify cyclic workflow models efficiently in a comprehensible form remains an open research question. Thus, a novel structural verification approach for cyclic workflow models by means of acyclic decomposition and reduction of loops is introduced in this paper with the following contributions. First, acyclic decomposition of natural loops, further enhanced by reduction of nested loops, enables existing verification techniques, normally dealing with acyclic models, to handle workflow models with natural loops. Second, instantiation of an irreducible loop into natural loops, altogether with reduction of concurrent loop entries, enables the proposed approach to handle workflow models with irreducible loops. Last, diagnostic information, provided by the proposed approach, helps stakeholders correct and improve their workflow models. Two examples are provided to show that the proposed approach is systematic and practical. In addition, a prototype of the proposed approach is developed. Its execution result shows that, while providing diagnostic information, the proposed approach can handle workflow models with arbitrary cycles effectively.