Abstract
Liveness of Petri nets means all activities in a modeled system can potentially take place and thus implies deadlock freedom. The research on liveness analysis approaches is inadequate. This paper proposes a liveness judgment reachability graph (LJRG) approach to analyze the liveness of ω -independent Petri nets. Such nets can be loosely explained as a class of unbounded Petri nets in which the changes of tokens in unbounded places are not related to each other. This paper proposes several algorithms to transform a new modified reachability tree to a new modified reachability graph and then transform it to an LJRG. It then develops the application of LJRG into the liveness analysis of ω -independent unbounded Petri nets. The proposed method provides a new theoretical method and important tool for the liveness analysis of unbounded Petri nets. It is illustrated via some examples.
| Original language | English (US) |
|---|---|
| Article number | 7457700 |
| Pages (from-to) | 2601-2612 |
| Number of pages | 12 |
| Journal | IEEE Transactions on Systems, Man, and Cybernetics: Systems |
| Volume | 47 |
| Issue number | 9 |
| DOIs | |
| State | Published - Sep 2017 |
All Science Journal Classification (ASJC) codes
- Software
- Control and Systems Engineering
- Human-Computer Interaction
- Computer Science Applications
- Electrical and Electronic Engineering
Keywords
- Discrete event systems
- liveness
- reachability graph (RG)
- unbounded Petri net
- ω-independent Petri net