Verification of Joint Current-State Opacity Using Petri Nets

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.