A symbolic approach to the verification and enforcement of current‐state opacity using labelled Petri nets

Abstract

Abstract This work proposes a symbolic method to verify and enforce the current‐state opacity of labelled Petri nets (LPNs). The notion of basis markings of partially observed Petri nets currently dominates the development of opacity verification and enforcement for discrete event systems. However, the related computational efficiency, to a great extent, depends on the number of basis markings in a system, which increases exponentially with respect to the size of its corresponding LPN model. Binary decision diagrams (BDDs) are capable of computing a set of basis markings in a compact shared structure. To mitigate the computational overheads, a BDD‐based method to efficiently model the structure and behaviour of an LPN is proposed. Then, the current‐state opacity of LPNs is verified and enforced in a symbolic manner. Finally, a number of examples are provided to demonstrate the effectiveness and efficiency of the proposed method.

Keywords

• discrete event systems
• Petri nets
• binary decision diagrams
• state‐based opacity