On Liveness of Non-sound Acyclic Free Choice Workflow Nets

Soundness is a criterion of correctness of workflow nets (WF-nets for short). For a subclass of WF-nets, called FC WF-nets, soundness can be decided in polynomial time. A WF-net is sound iff its short-circuited net is live and bounded. If a given WF-net is non-sound, we first must investigate the cause of non-soundness, i.e. Is the short-circuited net non-live and/or non-bounded? In this paper, we first proved that for the short-circuited nets of acyclic FC WF-nets, the liveness problem is co-NP-complete. The proof uses polynomial time reducing from 3-CNF-SAT. Next, we proposed a sufficient condition on the problem. The condition makes use of a structure, called PT-handle, and can be checked in polynomial time. Next, we illustrated the proposed condition with an example. Then, we proposed an algorithm deciding the condition in polynomial time. We also show an example that the proposed method contributes for modifying a given non-sound WF-nets.