Lean reachability tree for Petri net analysis

Jun Li; Xiaolong Yu; Mengchu Zhou

doi:10.1109/ICNSC.2016.7478977

Lean reachability tree for Petri net analysis

Jun Li, Xiaolong Yu, Mengchu Zhou

Electrical and Computer Engineering

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

1 Scopus citations

Abstract

This work presents a non-Karp-Miller tree called a lean reachability tree (LRT). It does not try to equivalently represent but faithfully express in a finite manner the reachability set of an unbounded Petri net. First, we derive a sufficient and necessary condition of unbounded places and some incremental reachability properties to characterize unbounded nets. Then, we present a sufficiently enabling condition (SEC) and an LRT generation algorithm. No fake marking is produced and no legal marking is lost during the tree generation. We prove that LRT can represent faithfully the reachability set of an unbounded net in a finite manner. Also, we examine its properties and prove a sufficient condition for deadlock checking based on it. Our examples show that LRT outperforms the latest modified Karp-Miller trees in terms of size, expressiveness, and applicability.

Original language	English (US)
Title of host publication	ICNSC 2016 - 13th IEEE International Conference on Networking, Sensing and Control
Publisher	Institute of Electrical and Electronics Engineers Inc.
ISBN (Electronic)	9781467399753
DOIs	https://doi.org/10.1109/ICNSC.2016.7478977
State	Published - May 25 2016
Event	13th IEEE International Conference on Networking, Sensing and Control, ICNSC 2016 - Mexico City, Mexico Duration: Apr 28 2016 → Apr 30 2016

Other

Other	13th IEEE International Conference on Networking, Sensing and Control, ICNSC 2016
Country/Territory	Mexico
City	Mexico City
Period	4/28/16 → 4/30/16

All Science Journal Classification (ASJC) codes

Artificial Intelligence
Computer Networks and Communications
Control and Systems Engineering
Modeling and Simulation

Access to Document

10.1109/ICNSC.2016.7478977

Cite this

@inproceedings{e324b525721242f3bf019e353f53bd6c,

title = "Lean reachability tree for Petri net analysis",

abstract = "This work presents a non-Karp-Miller tree called a lean reachability tree (LRT). It does not try to equivalently represent but faithfully express in a finite manner the reachability set of an unbounded Petri net. First, we derive a sufficient and necessary condition of unbounded places and some incremental reachability properties to characterize unbounded nets. Then, we present a sufficiently enabling condition (SEC) and an LRT generation algorithm. No fake marking is produced and no legal marking is lost during the tree generation. We prove that LRT can represent faithfully the reachability set of an unbounded net in a finite manner. Also, we examine its properties and prove a sufficient condition for deadlock checking based on it. Our examples show that LRT outperforms the latest modified Karp-Miller trees in terms of size, expressiveness, and applicability.",

author = "Jun Li and Xiaolong Yu and Mengchu Zhou",

year = "2016",

month = may,

day = "25",

doi = "10.1109/ICNSC.2016.7478977",

language = "English (US)",

booktitle = "ICNSC 2016 - 13th IEEE International Conference on Networking, Sensing and Control",

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

address = "United States",

note = "13th IEEE International Conference on Networking, Sensing and Control, ICNSC 2016 ; Conference date: 28-04-2016 Through 30-04-2016",

}

Li, J, Yu, X & Zhou, M 2016, Lean reachability tree for Petri net analysis. in ICNSC 2016 - 13th IEEE International Conference on Networking, Sensing and Control., 7478977, Institute of Electrical and Electronics Engineers Inc., 13th IEEE International Conference on Networking, Sensing and Control, ICNSC 2016, Mexico City, Mexico, 4/28/16. https://doi.org/10.1109/ICNSC.2016.7478977

TY - GEN

T1 - Lean reachability tree for Petri net analysis

AU - Li, Jun

AU - Yu, Xiaolong

AU - Zhou, Mengchu

PY - 2016/5/25

Y1 - 2016/5/25

N2 - This work presents a non-Karp-Miller tree called a lean reachability tree (LRT). It does not try to equivalently represent but faithfully express in a finite manner the reachability set of an unbounded Petri net. First, we derive a sufficient and necessary condition of unbounded places and some incremental reachability properties to characterize unbounded nets. Then, we present a sufficiently enabling condition (SEC) and an LRT generation algorithm. No fake marking is produced and no legal marking is lost during the tree generation. We prove that LRT can represent faithfully the reachability set of an unbounded net in a finite manner. Also, we examine its properties and prove a sufficient condition for deadlock checking based on it. Our examples show that LRT outperforms the latest modified Karp-Miller trees in terms of size, expressiveness, and applicability.

AB - This work presents a non-Karp-Miller tree called a lean reachability tree (LRT). It does not try to equivalently represent but faithfully express in a finite manner the reachability set of an unbounded Petri net. First, we derive a sufficient and necessary condition of unbounded places and some incremental reachability properties to characterize unbounded nets. Then, we present a sufficiently enabling condition (SEC) and an LRT generation algorithm. No fake marking is produced and no legal marking is lost during the tree generation. We prove that LRT can represent faithfully the reachability set of an unbounded net in a finite manner. Also, we examine its properties and prove a sufficient condition for deadlock checking based on it. Our examples show that LRT outperforms the latest modified Karp-Miller trees in terms of size, expressiveness, and applicability.

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

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

U2 - 10.1109/ICNSC.2016.7478977

DO - 10.1109/ICNSC.2016.7478977

M3 - Conference contribution

AN - SCOPUS:84978173034

BT - ICNSC 2016 - 13th IEEE International Conference on Networking, Sensing and Control

PB - Institute of Electrical and Electronics Engineers Inc.

T2 - 13th IEEE International Conference on Networking, Sensing and Control, ICNSC 2016

Y2 - 28 April 2016 through 30 April 2016

ER -

Lean reachability tree for Petri net analysis

Abstract

Other

All Science Journal Classification (ASJC) codes

Access to Document

Other files and links

Fingerprint

Cite this