IDEAS home Printed from https://ideas.repec.org/a/gam/jmathe/v11y2023i8p1798-d1119956.html
   My bibliography  Save this article

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

Author

Listed:
  • 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)

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.

Suggested Citation

  • Haoming Zhu & Ahmed M. El-Sherbeeny & Mohammed A. El-Meligy & Amir M. Fathollahi-Fard & Zhiwu Li, 2023. "Verification of Current-State Opacity in Discrete Event Systems by Using Basis Coverability Graphs," Mathematics, MDPI, vol. 11(8), pages 1-18, April.
    • Handle: RePEc:gam:jmathe:v:11:y:2023:i:8:p:1798-:d:1119956
    as

    Download full text from publisher

    File URL: https://www.mdpi.com/2227-7390/11/8/1798/pdf
    Download Restriction: no
    File URL: https://www.mdpi.com/2227-7390/11/8/1798/
    Download Restriction: no
    ---><---

    Citations

    Citations are extracted by the CitEc Project, subscribe to its RSS feed for this item.
    as


    Cited by:

    1. Haoming Zhu & Gaiyun Liu & Zhenhua Yu & Zhiwu Li, 2023. "Detectability in Discrete Event Systems Using Unbounded Petri Nets," Mathematics, MDPI, vol. 11(18), pages 1-28, September.

    Corrections

    All material on this site has been provided by the respective publishers and authors. You can help correct errors and omissions. When requesting a correction, please mention this item's handle: RePEc:gam:jmathe:v:11:y:2023:i:8:p:1798-:d:1119956. See general information about how to correct material in RePEc.

    If you have authored this item and are not yet registered with RePEc, we encourage you to do it here. This allows to link your profile to this item. It also allows you to accept potential citations to this item that we are uncertain about.

    We have no bibliographic references for this item. You can help adding them by using this form .

    If you know of missing items citing this one, you can help us creating those links by adding the relevant references in the same way as above, for each refering item. If you are a registered author of this item, you may also want to check the "citations" tab in your RePEc Author Service profile, as there may be some citations waiting for confirmation.

    For technical questions regarding this item, or to correct its authors, title, abstract, bibliographic or download information, contact: MDPI Indexing Manager (email available below). General contact details of provider: https://www.mdpi.com .

    Please note that corrections may take a couple of weeks to filter through the various RePEc services.

    IDEAS is a RePEc service. RePEc uses bibliographic data supplied by the respective publishers.