Verification of Current-State Opacity in Discrete Event Systems by Using Basis Coverability Graphs

Haoming Zhu, Ahmed M. El-Sherbeeny, Mohammed A. El-Meligy, Amir M. Fathollahi-Fard and Zhiwu Li ()
Additional contact information
Haoming Zhu: Institute of Systems Engineering, Macau University of Science and Technology, Taipa, Macao SAR, China
Ahmed M. El-Sherbeeny: Industrial Engineering Department, College of Engineering, King Saud University, P.O. Box 800, Riyadh 11421, Saudi Arabia
Mohammed A. El-Meligy: Industrial Engineering Department, College of Engineering, King Saud University, P.O. Box 800, Riyadh 11421, Saudi Arabia
Amir M. Fathollahi-Fard: Peter B. Gustavson School of Business, University of Victoria, P.O. Box 1700, Victoria, BC V8P 5C2, Canada
Zhiwu Li: Institute of Systems Engineering, Macau University of Science and Technology, Taipa, Macao SAR, China

Mathematics, 2023, vol. 11, issue 8, 1-18

Abstract: A new approach to the verification of current-state opacity for discrete event systems is proposed in this paper, which is modeled with unbounded Petri nets. The concept of opacity verification is first extended from bounded Petri nets to unbounded Petri nets. In this model, all transitions and partial places are assumed to be unobservable, i.e., only the number of tokens in the observable places can be measured. In this work, a novel basis coverability graph is constructed by using partial markings and quasi-observable transitions. By this graph, this research finds that an unbounded net system is current-state opaque if, for an arbitrary partial marking, there always exists at least one regular marking in the result of current-state estimation with respect to the partial marking not belonging to the given secret. Finally, a sufficient and necessary condition is proposed for the verification of current-state opacity. A manufacturing system example is presented to illustrate that the concept of current-state opacity can be verified for unbounded net systems.

Keywords: basis coverability graph; discrete event system; Petri net; current-state opacity (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: View citations in EconPapers (1)

Downloads: (external link)
https://www.mdpi.com/2227-7390/11/8/1798/pdf (application/pdf)
https://www.mdpi.com/2227-7390/11/8/1798/ (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:8:p:1798-:d:1119956

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 ().