Verification of Joint Current-State Opacity Using Petri Nets
Zhao, Wenjie;Giua, Alessandro;Li, Zhiwu
2023-01-01
Abstract
A discrete event system (DES) is said to be opaque if a predefined secret can never be exposed to an intruder who can observe its evolution. In this paper we consider a problem of joint current-state opacity for a system modeled by a Petri net and monitored by multiple local intruders, each of which can partially observe the behavior of the system. The intruders can synchronously communicate to a coordinator the state estimate they have computed, but not their observations. We demonstrate that the verification of this property can be efficiently addressed by using a compact representation of the reachability graph, called basis reachability graph (BRG), as it avoids the need for exhaustive enumeration of the reachability space. A joint BRG-observer is constructed to analyze joint current- state opacity under such a coordinated decentralized architecture.File | Size | Format | |
---|---|---|---|
1-s2.0-S2405896323003646-main.pdf open access
Type: versione editoriale
Size 1.18 MB
Format Adobe PDF
|
1.18 MB | Adobe PDF | View/Open |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.