Depth-first Search Approach for Language-based Opacity Verification Using Petri Nets. Issue 4 (2020)

• Record Type: Journal Article
• Authors: Saadaoui, I.; Li, Z.; Wu, N.; Khalgui, M.
• Is Part Of: IFAC-PapersOnLine. Volume 53:Issue 4(2020)
• Page Start: 378
• Page End: 383
• Publication Date: 2020
• Subjects: Discrete-event system -- Petri net -- Opacity verification -- depth-first search; Automatic control -- Periodicals; 629.805
• DOI: 10.1016/j.ifacol.2021.04.037
• Languages: English
• ISSNs: 2405-8963

Abstract

Abstract: The rapidly growing use of modern computer-integrated systems involving critical assets underscores the need for developing measures to guarantee their security against malicious attacks. This paper deals with the problem of language-based opacity formulation and verification in the framework of discrete event systems modeled with partially observed Petri nets (POPNs). In this context, a secret behavior is defined as a sub-language that should be hidden from an intruder who partially observes the system's evolution. A Petri net system is qualified as language opaque if no observation leads to an event sequence estimation that is entirely contained in a secret. In this paper, we develop a depth-first search algorithm that verifies the language opacity of a POPN system. More specifically, the proposed algorithm checks the existence of a non-secret transition sequence that is observably equivalent to a secret one by performing a depth-first search on a portion of the system's execution. Complexity analysis and experimental results are presented to illustrate the efficiency of the proposed approach.