For Full-Text PDF, please login, if you are a member of IEICE,|
or go to Pay Per View on menu list, if you are a nonmember of IEICE.
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
Publication Date: 2019/02/01
Online ISSN: 1745-1337
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.