Assessment of Initial-State-Opacity in Live Bounded and Reversible Discrete Event Systems via Integer Linear Programming

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 sufficient condition to check ISO by solving Integer Linear Programming problems is given in this paper. Such a condition exploits the algebraic representation of Petri nets and a structural one of its behavior in terms of minimal support T-invariants. The effectiveness of the proposed approach is shown by means of examples.