Alessandro Pisano
Verification of State-Based Opacity Using Petri Nets
Tong, YinPrimo
;Li, ZhiwuSecondo
;Seatzu, CarlaPenultimo
;Giua, AlessandroUltimo
2017-01-01
Abstract
A system is said to be opaque if a given secret behavior remains opaque (uncertain) to an intruder who can partially observe system activities. This work addresses the verification of state-based opacity in systems modeled with Petri nets. The secret behavior of a system is defined as a set of states. More precisely, two state-based opacity properties are considered: current-state opacity and initial-state opacity. We show that both current-state and initial-state opacity problems in bounded Petri nets can be efficiently solved by using a compact representation of the reachability graph, called basis reachability graph (BRG). This approach is practically efficient since the exhaustive enumeration of the reachability space can be avoided.File | Dimensione | Formato | |
---|---|---|---|
17tac_d.pdf Solo gestori archivio
Descrizione: articolo online
Tipologia: versione editoriale
Dimensione 1.44 MB
Formato Adobe PDF
|
1.44 MB | Adobe PDF | Visualizza/Apri Richiedi una copia |
17tac_d_draft.pdf Open Access dal 25/10/2018
Tipologia: versione post-print
Dimensione 1.32 MB
Formato Adobe PDF
|
1.32 MB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.