Online Opacity Verification of Networked Discrete Event Systems Modeled With Labeled Petri Nets

This paper addresses the online verification of current-state and k-step opacity in networked discrete event systems modeled with labeled Petri nets. In networked transmissions, there are two main communication disruptions, namely, delays and losses, which may result in incomplete observation sequences, thus affecting the accuracy of traditional online opacity verification methods. To solve such an issue, the notions of current-state and k-step opacity of an observation are generalized by incorporating the effects of the two disruptions. As shown in the literature, a secret is described as a subset of markings for the generality of the approach. Under the assumptions that the unobservable subnet is acyclic and the system is bounded, integer linear programming problems (ILPPs) are formulated. Then, online algorithms are designed by solving ILPPs to respectively verify the current-state and k-step opacity of an observation that may be incomplete due to communication delays and losses. Furthermore, in the absence of communication disruption, fewer constraints and variables are considered in the proposed ILPPs compared with the existing approaches, which contributes to a lower computational overhead. Finally, the efficiency and efficacy of the proposed methods are illustrated through an example and a case study.