Back to Search
Start Over
Non-Blockingness Verification of Bounded Petri Nets Using Basis Reachability Graphs
- Source :
- IEEE Control Systems Letters. 6:1220-1225
- Publication Year :
- 2022
- Publisher :
- Institute of Electrical and Electronics Engineers (IEEE), 2022.
-
Abstract
- In this letter, we study the problem of non-blockingness verification by tapping into the basis reachability graph (BRG). Non-blockingness is a property that ensures that all pre-specified tasks can be completed, which is a mandatory requirement during the system design stage. We develop a condition of transition partition of a given net such that the corresponding conflict-increase BRG contains sufficient information on verifying non-blockingness of its corresponding Petri net. Thanks to the compactness of the BRG, our approach possesses practical efficiency since the exhaustive enumeration of the state space can be avoided. In particular, our method does not require that the net is deadlock-free.
- Subjects :
- 0209 industrial biotechnology
Control and Optimization
Theoretical computer science
Basis (linear algebra)
Computer science
020208 electrical & electronic engineering
02 engineering and technology
Petri net
Net (mathematics)
Automaton
020901 industrial engineering & automation
Compact space
Control and Systems Engineering
Reachability
Bounded function
0202 electrical engineering, electronic engineering, information engineering
State space
Subjects
Details
- ISSN :
- 24751456
- Volume :
- 6
- Database :
- OpenAIRE
- Journal :
- IEEE Control Systems Letters
- Accession number :
- edsair.doi...........07528423c7fb346d9e2d1e172bb397c4