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

Shingo YAMAGUCHI  

Publication
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)
Category: 
Keyword: 
Petri net,  workflow net,  soundness,  liveness,  boundedness,  

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


Summary: 
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.