In this paper we propose an effective method based on basis marking analysis to verify the controllability of a given language specification in Petri nets. We compute the product, i.e., the concurrent composition, of the plant and of the specification nets and enumerate a subset of its reachable states, called basis markings. Each of these basis markings can be classified as controllable or uncontrollable by solving an integer programming problem. We show that the specification is controllable if and only if no basis marking is uncontrollable. The method can lead to practically efficient verification because it does not require an exhaustive enumeration of the state space.

A method to verify the controllability of language specifications in Petri nets based on basis marking analysis

GIUA, ALESSANDRO
2016

Abstract

In this paper we propose an effective method based on basis marking analysis to verify the controllability of a given language specification in Petri nets. We compute the product, i.e., the concurrent composition, of the plant and of the specification nets and enumerate a subset of its reachable states, called basis markings. Each of these basis markings can be classified as controllable or uncontrollable by solving an integer programming problem. We show that the specification is controllable if and only if no basis marking is uncontrollable. The method can lead to practically efficient verification because it does not require an exhaustive enumeration of the state space.
Petri nets; Controllability; Integer programming; State-space methods; Basis marking analysis; Integer programming problem; Language specification controllability; State space; Aerospace electronics; Electronic mail; Law; Supervisory control
File in questo prodotto:
File Dimensione Formato  
15cdc_a.pdf

Solo gestori archivio

Tipologia: versione post-print
Dimensione 384.13 kB
Formato Adobe PDF
384.13 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/178024
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? 4
social impact