University of Cagliari
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.
Files in This Item:
| File | Size | Format | |
|---|---|---|---|
| Giua et al_AUTOMATICA_80_2017.pdf Solo gestori archivio
Description: articolo
Type: versione editoriale
Size 682.48 kB
Format Adobe PDF
|
682.48 kB | Adobe PDF | & nbsp; View / Open Request a copy |
| 17aut_a_draft.pdf open access
Type: versione post-print
Size 411.28 kB
Format Adobe PDF
|
411.28 kB | Adobe PDF | View/Open |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.