Analysis of Option to Complete, Proper Completion and No Dead Tasks for Acyclic Free Choice Workflow Nets


IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences   Vol.E102-A   No.2   pp.336-342
Publication Date: 2019/02/01
Online ISSN: 1745-1337
DOI: 10.1587/transfun.E102.A.336
Type of Manuscript: Special Section PAPER (Special Section on Mathematical Systems Science and its Applications)
Petri net,  workflow net,  soundness,  liveness,  boundedness,  

Full Text: PDF(687.4KB)
>>Buy this Article

Workflow nets (WF-nets for short) are a subclass of Petri nets and are used for modeling and analysis of workflows. Soundness is a criterion of logical correctness defined for WF-nets. A WF-net is said to be sound if it satisfies three conditions: (i) option to complete, (ii) proper completion, and (iii) no dead tasks. In this paper, focusing our analysis on acyclic free choice WF-nets, we revealed that (1) Conditions (i) and (ii) of soundness are respectively equivalent to the liveness and the boundedness of its short-circuited net; (2) The decision problem for each condition of soundness is co-NP-complete; and (3) If the short-circuited net has no disjoint paths from a transition to a place (or no disjoint paths from a place to a transition), each condition can be checked in polynomial time.