The Liveness of WS<SUP>3</SUP>PR: Complexity and Decision

GuanJun LIU; ChangJun JIANG; MengChu ZHOU; Atsushi OHTA

doi:10.1587/transfun.E96.A.1783

The Liveness of WS³PR: Complexity and Decision

GuanJun LIU, ChangJun JIANG, MengChu ZHOU, Atsushi OHTA

Full Text Views

0

Share
Cite this

Summary :

Petri nets are a kind of formal language that are widely applied in concurrent systems associated with resource allocation due to their abilities of the natural description on resource allocation and the precise characterization on deadlock. Weighted System of Simple Sequential Processes with Resources (WS³PR) is an important subclass of Petri nets that can model many resource allocation systems in which 1) multiple processes may run in parallel and 2) each execution step of each process may use multiple units from a single resource type but cannot use multiple resource types. We first prove that the liveness problem of WS³PR is co-NP-hard on the basis of the partition problem. Furthermore, we present a necessary and sufficient condition for the liveness of WS³PR based on two new concepts called Structurally Circular Wait (SCW) and Blocking Marking (BM), i.e., a WS³PR is live iff each SCW has no BM. A sufficient condition is also proposed to guarantee that an SCW has no BM. Additionally, we show some advantages of using SCW to analyze the deadlock problem compared to other siphon-based ones, and discuss the relation between SCW and siphon. These results are valuable to the further research on the deadlock prevention or avoidance for WS³PR.

Publication: IEICE TRANSACTIONS on Fundamentals Vol.E96-A No.8 pp.1783-1793

Publication Date: 2013/08/01

Publicized

Online ISSN: 1745-1337

DOI: 10.1587/transfun.E96.A.1783

Type of Manuscript: PAPER

Category: Concurrent Systems

Authors

GuanJun LIU
  Singapore University of Technology and Design
ChangJun JIANG
  Tongji University
MengChu ZHOU
  New Jersey Institute of Technology
Atsushi OHTA
  Aichi Prefectural University

Keyword

concurrent systems, Petri nets, liveness, deadlock, resource allocation

Cite this

Copy

GuanJun LIU, ChangJun JIANG, MengChu ZHOU, Atsushi OHTA, "The Liveness of WS3PR: Complexity and Decision" in IEICE TRANSACTIONS on Fundamentals, vol. E96-A, no. 8, pp. 1783-1793, August 2013, doi: 10.1587/transfun.E96.A.1783.
Abstract: Petri nets are a kind of formal language that are widely applied in concurrent systems associated with resource allocation due to their abilities of the natural description on resource allocation and the precise characterization on deadlock. Weighted System of Simple Sequential Processes with Resources (WS³PR) is an important subclass of Petri nets that can model many resource allocation systems in which 1) multiple processes may run in parallel and 2) each execution step of each process may use multiple units from a single resource type but cannot use multiple resource types. We first prove that the liveness problem of WS³PR is co-NP-hard on the basis of the partition problem. Furthermore, we present a necessary and sufficient condition for the liveness of WS³PR based on two new concepts called Structurally Circular Wait (SCW) and Blocking Marking (BM), i.e., a WS³PR is live iff each SCW has no BM. A sufficient condition is also proposed to guarantee that an SCW has no BM. Additionally, we show some advantages of using SCW to analyze the deadlock problem compared to other siphon-based ones, and discuss the relation between SCW and siphon. These results are valuable to the further research on the deadlock prevention or avoidance for WS³PR.
URL: https://globals.ieice.org/en_transactions/fundamentals/10.1587/transfun.E96.A.1783/_p

Copy

@ARTICLE{e96-a_8_1783,
author={GuanJun LIU, ChangJun JIANG, MengChu ZHOU, Atsushi OHTA, },
journal={IEICE TRANSACTIONS on Fundamentals},
title={The Liveness of WS3PR: Complexity and Decision},
year={2013},
volume={E96-A},
number={8},
pages={1783-1793},
abstract={Petri nets are a kind of formal language that are widely applied in concurrent systems associated with resource allocation due to their abilities of the natural description on resource allocation and the precise characterization on deadlock. Weighted System of Simple Sequential Processes with Resources (WS³PR) is an important subclass of Petri nets that can model many resource allocation systems in which 1) multiple processes may run in parallel and 2) each execution step of each process may use multiple units from a single resource type but cannot use multiple resource types. We first prove that the liveness problem of WS³PR is co-NP-hard on the basis of the partition problem. Furthermore, we present a necessary and sufficient condition for the liveness of WS³PR based on two new concepts called Structurally Circular Wait (SCW) and Blocking Marking (BM), i.e., a WS³PR is live iff each SCW has no BM. A sufficient condition is also proposed to guarantee that an SCW has no BM. Additionally, we show some advantages of using SCW to analyze the deadlock problem compared to other siphon-based ones, and discuss the relation between SCW and siphon. These results are valuable to the further research on the deadlock prevention or avoidance for WS³PR.},
keywords={},
doi={10.1587/transfun.E96.A.1783},
ISSN={1745-1337},
month={August},}

Copy

TY - JOUR
TI - The Liveness of WS3PR: Complexity and Decision
T2 - IEICE TRANSACTIONS on Fundamentals
SP - 1783
EP - 1793
AU - GuanJun LIU
AU - ChangJun JIANG
AU - MengChu ZHOU
AU - Atsushi OHTA
PY - 2013
DO - 10.1587/transfun.E96.A.1783
JO - IEICE TRANSACTIONS on Fundamentals
SN - 1745-1337
VL - E96-A
IS - 8
JA - IEICE TRANSACTIONS on Fundamentals
Y1 - August 2013
AB - Petri nets are a kind of formal language that are widely applied in concurrent systems associated with resource allocation due to their abilities of the natural description on resource allocation and the precise characterization on deadlock. Weighted System of Simple Sequential Processes with Resources (WS³PR) is an important subclass of Petri nets that can model many resource allocation systems in which 1) multiple processes may run in parallel and 2) each execution step of each process may use multiple units from a single resource type but cannot use multiple resource types. We first prove that the liveness problem of WS³PR is co-NP-hard on the basis of the partition problem. Furthermore, we present a necessary and sufficient condition for the liveness of WS³PR based on two new concepts called Structurally Circular Wait (SCW) and Blocking Marking (BM), i.e., a WS³PR is live iff each SCW has no BM. A sufficient condition is also proposed to guarantee that an SCW has no BM. Additionally, we show some advantages of using SCW to analyze the deadlock problem compared to other siphon-based ones, and discuss the relation between SCW and siphon. These results are valuable to the further research on the deadlock prevention or avoidance for WS³PR.
ER -