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 acyclic WS is a subclass of acyclic EFC but has more analysis methods. A sound acyclic EFC WF-net may be transformed to an acyclic 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 acyclic EFC WF-net is refactorable to an acyclic WS WF-net. We give a sufficient condition on the problem, i.e. a sound acyclic EFC WF-net is refactorable to an acyclic 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 acyclic EFC WF-nets.