Deadlock checking for one-place unbounded Petri nets based on modified reachability trees

Zhi Jun Ding, Chang Jun Jiang, Meng Chu Zhou

Research output: Contribution to journalArticlepeer-review

35 Scopus citations


A deadlock-checking approach for one-place unbounded Petri nets is presented based on modified reachability trees (MRTs). An MRT can provide some useful information that is lost in a finite reachability tree, owing to MRT's use of the expression a + bnirather than symbol ω to represent the value of the components of a marking. The information is helpful to property analysis of unbounded Petri nets. For the deadlock-checking purpose, this correspondence paper classifies full conditional nodes in MRT into two types: True and fake ones. Then, an algorithm is proposed to determine whether a full conditional node is true or not. Finally, a necessary and sufficient condition of deadlocks is presented. Examples are given to illustrate the method.

Original languageEnglish (US)
Pages (from-to)881-883
Number of pages3
JournalIEEE Transactions on Systems, Man, and Cybernetics, Part B: Cybernetics
Issue number3
StatePublished - Jun 2008

All Science Journal Classification (ASJC) codes

  • Control and Systems Engineering
  • Software
  • Information Systems
  • Human-Computer Interaction
  • Computer Science Applications
  • Electrical and Electronic Engineering


  • Automated manufacturing systems
  • Deadlock
  • Petri net
  • Reachability tree


Dive into the research topics of 'Deadlock checking for one-place unbounded Petri nets based on modified reachability trees'. Together they form a unique fingerprint.

Cite this