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