An Optimization Approach to Current State Opacity Assessment

This paper provides a necessary and sufficient condition to assess Current State Opacity (CSO) in discrete event systems modeled as bounded Petri nets. The provided condition requires to check opacity on a finite number of sequences. By exploiting the algebraic representation of Petri nets, we show how to turn the required checks into the solution of an optimization problem. Therefore, the proposed approach enables to perform CSO assessment by using off-the-shelf commercial software, without the need to build any observer, neither complete nor reduced, hence being less affected by the curse of dimensionality.