The Liveness of WS3PR: Complexity and Decision

GuanJun LIU  ChangJun JIANG  MengChu ZHOU  Atsushi OHTA  

IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences   Vol.E96-A    No.8    pp.1783-1793
Publication Date: 2013/08/01
Online ISSN: 1745-1337
DOI: 10.1587/transfun.E96.A.1783
Print ISSN: 0916-8508
Type of Manuscript: PAPER
Category: Concurrent Systems
concurrent systems,  Petri nets,  liveness,  deadlock,  resource allocation,  

Full Text: PDF>>
Buy this Article

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 (WS3PR) 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 WS3PR is co-NP-hard on the basis of the partition problem. Furthermore, we present a necessary and sufficient condition for the liveness of WS3PR based on two new concepts called Structurally Circular Wait (SCW) and Blocking Marking (BM), i.e., a WS3PR 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 WS3PR.