This article proposes a semi-structural approach to verify the nonblockingness of a Petri net. We construct a structure, called minimal-maximal basis reachability graph (min-max-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 min-max-BRG is unobstructed, which can be verified by solving a set of integer constraints and then examining the min-max-BRG. For Petri nets that are not deadlock-free, one needs to determine the set of dead markings. This can be done with an approach based on the computation of maximal implicit firing sequences enabled by the markings in the min-max-BRG. The approach we developed does not require the construction of the reachability graph and has wide applicability.

Verification of Nonblockingness in Bounded Petri Nets With Min-Max Basis Reachability Graphs

Gu, C
Primo
;
Giua, A
Ultimo
2022-01-01

Abstract

This article proposes a semi-structural approach to verify the nonblockingness of a Petri net. We construct a structure, called minimal-maximal basis reachability graph (min-max-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 min-max-BRG is unobstructed, which can be verified by solving a set of integer constraints and then examining the min-max-BRG. For Petri nets that are not deadlock-free, one needs to determine the set of dead markings. This can be done with an approach based on the computation of maximal implicit firing sequences enabled by the markings in the min-max-BRG. The approach we developed does not require the construction of the reachability graph and has wide applicability.
Petri nets; System recovery; Automata; Analytical models; Supervisory control; Computational modeling; Explosions; Basis reachability graph (BRG); Nonblockingness; Petri net
File in questo prodotto:
File Dimensione Formato  
22tsmc_sys.pdf

Solo gestori archivio

Tipologia: versione editoriale
Dimensione 903.92 kB
Formato Adobe PDF
903.92 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
22tsmc_sys_draft.pdf

accesso aperto

Tipologia: versione post-print
Dimensione 2.78 MB
Formato Adobe PDF
2.78 MB Adobe PDF Visualizza/Apri

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/345192
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? 0
social impact