The liveness of WS3PR: Complexity and decision

Guan Jun Liu, Chang Jun Jiang, Meng Chu Zhou, Atsushi Ohta

Research output: Contribution to journalArticlepeer-review

19 Scopus citations


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.

Original languageEnglish (US)
Pages (from-to)1783-1793
Number of pages11
JournalIEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences
Issue number8
StatePublished - Aug 2013

All Science Journal Classification (ASJC) codes

  • Signal Processing
  • Computer Graphics and Computer-Aided Design
  • Electrical and Electronic Engineering
  • Applied Mathematics


  • Concurrent systems
  • Deadlock
  • Liveness
  • Petri nets
  • Resource allocation


Dive into the research topics of 'The liveness of WS3PR: Complexity and decision'. Together they form a unique fingerprint.

Cite this