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.

Non-Blockingness Verification of Bounded Petri Nets Using Basis Reachability Graphs

Gu C.
Primo
;
Ma Z.
Secondo
;
Li Z.
;
Giua A.
Ultimo
2022-01-01

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.
2022
Petri nets; reachability analysis; task analysis; postal services; automata; upper bound; system recovery; non-blockingness verification; basis reachability graph
File in questo prodotto:
File Dimensione Formato  
22lcss_b.pdf

Solo gestori archivio

Descrizione: articolo online
Tipologia: versione editoriale (VoR)
Dimensione 554.01 kB
Formato Adobe PDF
554.01 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11584/326394
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? 1
social impact