Language-Based Opacity Verification in Partially Observed Petri Nets through Linear Constraints
Ikram Saadaoui,
Abdeldjalil Labed,
Zhiwu Li (),
Ahmed M. El-Sherbeeny and
Huiran Du
Additional contact information
Ikram Saadaoui: Institute of Systems Engineering, Macau University of Science and Technology, Taipa, Macau SAR 999078, China
Abdeldjalil Labed: Mediterranean Institute of Technology, South Mediterranean University, Tunis 99628, Tunisia
Zhiwu Li: Institute of Systems Engineering, Macau University of Science and Technology, Taipa, Macau SAR 999078, China
Ahmed M. El-Sherbeeny: Industrial Engineering Department, College of Engineering, King Saud University, P.O. Box 800, Riyadh 11421, Saudi Arabia
Huiran Du: Hitachi Building Technology (Guangzhou) Co., Ltd., Guangzhou 510700, China
Mathematics, 2023, vol. 11, issue 18, 1-23
Abstract:
Information security is an important area of concern in modern computer-integrated systems. It involves implementing preventative measures to protect confidential data from potential vulnerabilities, such as unauthorized access, secret disclosure, modification, or destruction. Considering such threats, we investigate a particular confidentiality property called opacity, which specifies a system’s ability to cover its ‘secret’ data from being interfered with by outside observers, termed as intruders. This paper discusses language-based opacity formulation and verification in the context of discrete event systems represented by partially observed Petri nets. In this context, we identify two opacity properties, called consistency and non-secrecy; then, we exploit the mathematical characterization of a net system, to separately check each property, by specifying two feasibility problems. The proposed method is carried out for two distinct settings of a system. The first setting is centralized, where an intruder is granted complete information about the system structure but a partial observation of its behavior. The second setting is decentralized, where a group of intruders cooperates to reveal the secret language, by using a coordinator. Finally, experimental findings are given, to demonstrate the proficiency of the proposed approach.
Keywords: discrete event system; opacity; Petri net; sensor configuration; linear constraints; integer linear programming (search for similar items in EconPapers)
JEL-codes: C (search for similar items in EconPapers)
Date: 2023
References: View complete reference list from CitEc
Citations:
Downloads: (external link)
https://www.mdpi.com/2227-7390/11/18/3880/pdf (application/pdf)
https://www.mdpi.com/2227-7390/11/18/3880/ (text/html)
Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.
Export reference: BibTeX
RIS (EndNote, ProCite, RefMan)
HTML/Text
Persistent link: https://EconPapers.repec.org/RePEc:gam:jmathe:v:11:y:2023:i:18:p:3880-:d:1237683
Access Statistics for this article
Mathematics is currently edited by Ms. Emma He
More articles in Mathematics from MDPI
Bibliographic data for series maintained by MDPI Indexing Manager ().