Verification of Nonblockingness in Bounded Petri Nets With Minimax Basis Reachability Graphs
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2020
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866909369396887552 |
|---|---|
| author | Gu, Chao Ma, Ziyue Li, Zhiwu Giua, Alessandro |
| author_facet | Gu, Chao Ma, Ziyue Li, Zhiwu Giua, Alessandro |
| contents | This paper proposes a semi-structural approach to verify the nonblockingness of a Petri net. We construct a structure, called minimax basis reachability graph (minimax-BRG): it provides an abstract description of the reachability set of a net while preserving all information needed to test if the net is blocking. We prove that a bounded deadlock-free Petri net is nonblocking if and only if its minimax-BRG is unobstructed, which can be verified by solving a set of integer constraints and then examining the minimax-BRG. For Petri nets that are not deadlock-free, one needs to determine the set of deadlock markings. This can be done with an approach based on the computation of maximal implicit firing sequences enabled by the markings in the minimax-BRG. The approach we developed does not require the construction of the reachability graph and has wide applicability. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2003_14204 |
| institution | arXiv |
| publishDate | 2020 |
| record_format | arxiv |
| spellingShingle | Verification of Nonblockingness in Bounded Petri Nets With Minimax Basis Reachability Graphs Gu, Chao Ma, Ziyue Li, Zhiwu Giua, Alessandro Systems and Control Logic in Computer Science This paper proposes a semi-structural approach to verify the nonblockingness of a Petri net. We construct a structure, called minimax basis reachability graph (minimax-BRG): it provides an abstract description of the reachability set of a net while preserving all information needed to test if the net is blocking. We prove that a bounded deadlock-free Petri net is nonblocking if and only if its minimax-BRG is unobstructed, which can be verified by solving a set of integer constraints and then examining the minimax-BRG. For Petri nets that are not deadlock-free, one needs to determine the set of deadlock markings. This can be done with an approach based on the computation of maximal implicit firing sequences enabled by the markings in the minimax-BRG. The approach we developed does not require the construction of the reachability graph and has wide applicability. |
| title | Verification of Nonblockingness in Bounded Petri Nets With Minimax Basis Reachability Graphs |
| topic | Systems and Control Logic in Computer Science |
| url | https://arxiv.org/abs/2003.14204 |