Optimization-Based Assessment of Initial-State Opacity in Petri Nets

When dealing with security and safety problems, Discrete Events Systems (DESs) could be a convenient way to model the behavior of distributed dynamical systems. Among the different DES mathematical tools, Petri Nets (PNs), by benefiting from a twofold representation, i.e. a graphical and a mathematical one, can be exploited for effectively tackling some security problems in the DES context such as the opacity one. This latter property is related to the capability of hiding a secret to external observers. When the secret is modeled by the initial marking (state) of a PN, the problem is known in literature as Initial-State Opacity (ISO). A DES is said to be ISO if, for every trajectory originating from a secret state, there exists another trajectory originated from a non-secret state, such that both of them are equivalent from an external observer (potentially malicious) point of view. Therefore, in an opaque system, such intruder can never determine whether the system started from a secret state or from a non-secret one. In this paper, leveraging the mathematical representation of PNs, we present a sufficient condition which permit to assess if a system is not opaque, by solving a feasibility problem with integer optimization variables. Specifically, the proposed approach starts from the ISO definition and, then, characterizes the aforementioned non-opacity condition as a set of linear constraints that, if not satisfied, imply the system to be not ISO.