Initial-state-opacity assessment in timed discrete event systems via optimization techniques

Opacity is a property of discrete event systems that allows to hide a secret from external observers. If the secret is the system initial state, then the related opacity problem is referred to as Initial State Opacity (ISO). The problem of ISO verification is usually approached at a logical level, by taking into account only the order of event occurrences. However, if the timing structure of the system is known, opacity analysis can be refined. This paper contributes to this line of research by proposing a result to assess opacity in a timed perspective. In such a framework, it is possible to establish how long the secret can be hidden from a malicious observer; indeed, by exploiting the timing information, the intruder may infer the secret, even if the system is logically opaque.