In this paper, we propose a basis marking method- based semi-structural approach to verify nonblockingness of a Petri net. By solving a set of integer linear programming problems, the unobstructiveness of a basis reachability graph, which is a necessary condition for nonblockingness, is determined. We propose an algorithm to expand the basis reachability graph and show that a bounded Petri net is nonblocking if and only if its expanded basis reachability graph is unobstructed. The main advantages of this method are that it does not require to enumerate all the reachable markings and has wide applicability.

Verification of Nonblockingness in Bounded Petri Nets with a Semi-Structural Approach

Gu C.;Ma Z.;Li Z.;Giua A.
2019-01-01

Abstract

In this paper, we propose a basis marking method- based semi-structural approach to verify nonblockingness of a Petri net. By solving a set of integer linear programming problems, the unobstructiveness of a basis reachability graph, which is a necessary condition for nonblockingness, is determined. We propose an algorithm to expand the basis reachability graph and show that a bounded Petri net is nonblocking if and only if its expanded basis reachability graph is unobstructed. The main advantages of this method are that it does not require to enumerate all the reachable markings and has wide applicability.
2019
978-1-7281-1398-2
Petri nets; Basis marking; Nonblockingness
File in questo prodotto:
Non ci sono file associati a questo prodotto.

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