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

• DOI: 10.1049/cth2.12546
• Publication Date: 2023-09-05T04:33:32Z
• Authors: Kun Peng; Yufeng Chen; Zhiwu Li
• Keywords: Basis (linear algebra); Opacity; Binary decision diagram

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