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.
Shingo YAMAGUCHI
Yamaguchi University
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Copy
Shingo YAMAGUCHI, "Analysis of Option to Complete, Proper Completion and No Dead Tasks for Acyclic Free Choice Workflow Nets" in IEICE TRANSACTIONS on Fundamentals,
vol. E102-A, no. 2, pp. 336-342, February 2019, doi: 10.1587/transfun.E102.A.336.
Abstract: 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.
URL: https://global.ieice.org/en_transactions/fundamentals/10.1587/transfun.E102.A.336/_p
Copy
@ARTICLE{e102-a_2_336,
author={Shingo YAMAGUCHI, },
journal={IEICE TRANSACTIONS on Fundamentals},
title={Analysis of Option to Complete, Proper Completion and No Dead Tasks for Acyclic Free Choice Workflow Nets},
year={2019},
volume={E102-A},
number={2},
pages={336-342},
abstract={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.},
keywords={},
doi={10.1587/transfun.E102.A.336},
ISSN={1745-1337},
month={February},}
Copy
TY - JOUR
TI - Analysis of Option to Complete, Proper Completion and No Dead Tasks for Acyclic Free Choice Workflow Nets
T2 - IEICE TRANSACTIONS on Fundamentals
SP - 336
EP - 342
AU - Shingo YAMAGUCHI
PY - 2019
DO - 10.1587/transfun.E102.A.336
JO - IEICE TRANSACTIONS on Fundamentals
SN - 1745-1337
VL - E102-A
IS - 2
JA - IEICE TRANSACTIONS on Fundamentals
Y1 - February 2019
AB - 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.
ER -