An algebraic characterization of language-based opacity in labeled Petri nets

Opacity is a property of discrete event systems (DES) that is related to the possibility of hiding a secret to external observers (the intruders). The secret can be either a system state, or a sequence of events executed by the system itself. When the latter type of secrets is considered, the opacity property is referred to as language-based opacity (LBO). This paper deals with LBO when the DES is modeled by a labeled Petri net. One necessary and sufficient condition to check LBO by solving Integer Linear Programming problems is given; such a condition exploits the algebraic representation of Petri nets. A sufficient condition is then derived, which is less demanding from the computational point of view. The effectiveness of the proposed approach is shown by means of examples