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.

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.
2017
Decidability problems; Discrete event systems; Opacity; Petri nets; Control and Systems Engineering; Electrical and Electronic Engineering
File in questo prodotto:
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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11584/212945
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 50
  • ???jsp.display-item.citation.isi??? 48
social impact