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

Zhi Jun Ding; Chang Jun Jiang; Meng Chu Zhou

doi:10.1109/TSMCB.2008.917177

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

Zhi Jun Ding, Chang Jun Jiang, Meng Chu Zhou

Electrical and Computer Engineering

Research output: Contribution to journal › Article › peer-review

36 Scopus citations

Abstract

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 + bn_irather 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 language	English (US)
Pages (from-to)	881-883
Number of pages	3
Journal	IEEE Transactions on Systems, Man, and Cybernetics, Part B: Cybernetics
Volume	38
Issue number	3
DOIs	https://doi.org/10.1109/TSMCB.2008.917177
State	Published - 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

Keywords

Automated manufacturing systems
Deadlock
Petri net
Reachability tree

Access to Document

10.1109/TSMCB.2008.917177

Cite this

@article{64982bd83c1d496e9c212bf7d1d28293,

title = "Deadlock checking for one-place unbounded Petri nets based on modified reachability trees",

abstract = "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.",

keywords = "Automated manufacturing systems, Deadlock, Petri net, Reachability tree",

author = "Ding, {Zhi Jun} and Jiang, {Chang Jun} and Zhou, {Meng Chu}",

note = "Funding Information: Manuscript received July 19, 2007. This work was supported in part by the National Basic Research Program of China (973 Program) (2003CB317002 and 2007CB316502), in part by the National Natural Science Funds (60534060, 90718012), and Chang Jiang Scholar Program, PRC Ministry of Education. This paper was recommended by Associate Editor Q. Zhang.",

year = "2008",

month = jun,

doi = "10.1109/TSMCB.2008.917177",

language = "English (US)",

volume = "38",

pages = "881--883",

journal = "IEEE Transactions on Systems, Man, and Cybernetics, Part B: Cybernetics",

issn = "1083-4419",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

number = "3",

}

TY - JOUR

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

AU - Ding, Zhi Jun

AU - Jiang, Chang Jun

AU - Zhou, Meng Chu

N1 - Funding Information: Manuscript received July 19, 2007. This work was supported in part by the National Basic Research Program of China (973 Program) (2003CB317002 and 2007CB316502), in part by the National Natural Science Funds (60534060, 90718012), and Chang Jiang Scholar Program, PRC Ministry of Education. This paper was recommended by Associate Editor Q. Zhang.

PY - 2008/6

Y1 - 2008/6

N2 - 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.

AB - 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.

KW - Automated manufacturing systems

KW - Deadlock

KW - Petri net

KW - Reachability tree

UR - http://www.scopus.com/inward/record.url?scp=44849128921&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=44849128921&partnerID=8YFLogxK

U2 - 10.1109/TSMCB.2008.917177

DO - 10.1109/TSMCB.2008.917177

M3 - Article

C2 - 18558549

AN - SCOPUS:44849128921

SN - 1083-4419

VL - 38

SP - 881

EP - 883

JO - IEEE Transactions on Systems, Man, and Cybernetics, Part B: Cybernetics

JF - IEEE Transactions on Systems, Man, and Cybernetics, Part B: Cybernetics

IS - 3

ER -

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

Abstract

All Science Journal Classification (ASJC) codes

Keywords

Access to Document

Other files and links

Fingerprint

Cite this