A Petri net system is said to be initial-state opaque if its initial state remains opaque to an external observer (called an intruder). In other words, the intruder is never able to ascertain that the initial state belongs to a given set of states (called a secret) based on its observation of the system's evolution. This paper addresses the problem of verifying initial-state opacity in discrete event systems (DES) modeled by labeled Petri nets. An efficient approach to verifying initial-state opacity is proposed based on the notion of basis reachability graph (BRG).

Verification of initial-state opacity in Petri nets

SEATZU, CARLA;GIUA, ALESSANDRO
2015

Abstract

A Petri net system is said to be initial-state opaque if its initial state remains opaque to an external observer (called an intruder). In other words, the intruder is never able to ascertain that the initial state belongs to a given set of states (called a secret) based on its observation of the system's evolution. This paper addresses the problem of verifying initial-state opacity in discrete event systems (DES) modeled by labeled Petri nets. An efficient approach to verifying initial-state opacity is proposed based on the notion of basis reachability graph (BRG).
Petri nets;discrete event systems;formal verification;observers;reachability analysis;BRG;DES;Petri net system;basis reachability graph;discrete event systems;external observer;initial-state opacity;initial-state opaque;intruder;labeled Petri nets;secret;system evolution;verification;Automata;Complexity theory;Explosions;Fault diagnosis;Observers;Petri nets;Yttrium
File in questo prodotto:
File Dimensione Formato  
15cdc_b_draft.pdf

Solo gestori archivio

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