Necessary and Sufficient Condition to Assess Initial-State-Opacity in Live Bounded and Reversible Discrete Event Systems

Opacity is a property of discrete event systems (DES) that is related to the possibility of hiding a secret from external observers (the intruders). When the secret is the initial state of the system, the related opacity problem is referred to as Initial State Opacity (ISO). A necessary and sufficient condition to check ISO in DES modeled as Petri nets (PN) is given in this letter. By exploiting both the structural properties of PNs and the algebraic description of their dynamic, we propose to assess ISO by solving Integer Linear Programming problems.