Verification of State-Based Opacity Using Petri Nets
Tong, YinFirst
;Li, ZhiwuSecond
;Seatzu, CarlaPenultimate
;Giua, AlessandroLast
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 | Size | Format | |
---|---|---|---|
17tac_d.pdf Solo gestori archivio
Description: articolo online
Type: versione editoriale
Size 1.44 MB
Format Adobe PDF
|
1.44 MB | Adobe PDF | & nbsp; View / Open Request a copy |
17tac_d_draft.pdf Open Access from 25/10/2018
Type: versione post-print
Size 1.32 MB
Format Adobe PDF
|
1.32 MB | Adobe PDF | View/Open |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.