Sufficient Condition on Refactorizability of Acyclic Extended Free Choice Workflow Nets to Acyclic Well-Structured Workflow Nets

A workflow net (WF-net for short) is a Petri net which represents a workflow. There are two important subclasses of WF-nets: extended free choice (EFC for short) and well-structured (WS for short). It is known that most actual workflows can be modeled as EFC WF-nets, and a cyclic WS is a subclass of a cyclic EFC but has more analysis methods. A sound a cyclic EFC WF-net may be transformed to an a cyclic WS WF-net without changing the observable behavior of the net. Such a transformation is called refactoring. In this paper, we tackle a problem, named refactorizability problem, that decides whether a given sound a cyclic EFC WF-net is refactorable to an a cyclic WS WF-net. We give a sufficient condition on the problem, i.e. a sound a cyclic EFC WF-net is refactorable to an a cyclic WS WF-net if its short-circuited net has no PT-handle. Based on the condition, we construct a polynomial time procedure for solving the problem. This results in the enhancement of the analysis power of a cyclic EFC WF-nets.