Matrix Approach for Verification of Opacity of Partially Observed Discrete Event Systems
- PDF / 520,808 Bytes
- 18 Pages / 439.37 x 666.142 pts Page_size
- 65 Downloads / 153 Views
Matrix Approach for Verification of Opacity of Partially Observed Discrete Event Systems Liujuan Mei1 · Rongjian Liu1 · Jianquan Lu2
· Jianlong Qiu3
Received: 22 November 2019 / Revised: 18 May 2020 / Accepted: 21 May 2020 © Springer Science+Business Media, LLC, part of Springer Nature 2020
Abstract Opacity is a confidential property characterizing whether the secret of a system can be inferred or not by an outside observer (also called an intruder). This paper focuses on presenting a matrix-based approach for verification of opacity of nondeterministic discrete event systems (DESs). Firstly, the given system is modeled as a finite-state automaton. Further, based on Boolean semi-tensor product (BSTP) of matrices, the algebraic expression of the observable dynamic of the system can be obtained. We, respectively, investigate current-state opacity and K -step opacity owing to the equivalence between a few opacity properties. Finally, necessary and sufficient conditions are presented to verify whether the secret is opaque for a given system, and the proposed methodology is tested effectively by examples. The matrix-based characterization of opacity proposed in this paper may provide a helpful angel for understanding the structure of this property. Keywords Discrete event systems (DESs) · Nondeterministic finite automata · Opacity · Boolean semi-tensor product (BSTP) of matrices
B B
Jianquan Lu [email protected] Jianlong Qiu [email protected] Liujuan Mei [email protected] Rongjian Liu [email protected]
1
School of Cyber Science and Engineering, Southeast University, Nanjing 210096, People’s Republic of China
2
School of Mathematics, Southeast University, Nanjing 210096, People’s Republic of China
3
Key Laboratory of Complex Systems and Intelligent Computing in Universities of Shandong (Linyi University), School of Automation and Electrical Engineering, Linyi University, Linyi 276005, People’s Republic of China
Circuits, Systems, and Signal Processing
1 Introduction In the past few decades, kinds of properties of discrete event systems (DESs) have been investigated, such as observability, detectability, controllability and diagnosability [36, 39,42]. DESs are event-driven systems with a discrete set of states, that is, their states evolve depending on the occurrence of asynchronous discrete events over time [3]. Nowadays DESs have been successfully applied to many man-made systems such as network systems, communication systems, manufacturing systems and automated traffic systems [3]. Opacity is an active topic in DESs recently owning to the increasing attention of security. It is a confidential property which was firstly introduced in the computer science community to analyze cryptographic protocols [24], and then extended to the framework of DESs [2]. A system is said to be opaque if its important information, namely secrets, cannot be revealed to the intruder. Otherwise, the system is said to be not opaque. The intruder is a malicious observer which has perfect knowledge of the structure of the syst
Data Loading...
