A verification method of soundizability under protocol inheritance for acyclic free choice workflow nets

A workflow may be extended to adapt to market growth, legal reform, and so on. The extended workflow must be logically correct, and inherit the behavior of the existing workflow. Even if the extended workflow inherits the behavior, it may be not logically correct. Can we modify it so that it satisfies not only behavioral inheritance but also logical correctness? This is called soundizability problem. In this paper, we propose a Petri net based method to solve the problem. Limiting our analysis to acyclic free choice workflow nets, we gave a necessary and sufficient condition on the problem, which is the existence of a key structure of free choice workflow nets called TP-handles. Based on this condition, we also constructed a polynomial time procedure to solve the problem.