Decidability of opacity verification problems in labeled Petri net systems
Tong, Y;Li, Z;SEATZU, CARLA;GIUA, ALESSANDRO
2017-01-01
Abstract
A system is said to be opaque if an intruder that observes its evolution through a mask cannot infer that the system's evolution belongs to a given secret behavior. Opacity verification is the problem of determining whether the system is opaque with respect to a given secret or not. In this paper we address the decidability of the opacity verification problem. Using reduction approaches, we show that verification of initial-state, current-state, and language opacity is undecidable in labeled Petri nets.File | Dimensione | Formato | |
---|---|---|---|
Giua et al_AUTOMATICA_80_2017.pdf Solo gestori archivio
Descrizione: articolo
Tipologia: versione editoriale
Dimensione 682.48 kB
Formato Adobe PDF
|
682.48 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
17aut_a_draft.pdf accesso aperto
Tipologia: versione post-print
Dimensione 411.28 kB
Formato Adobe PDF
|
411.28 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.