Sequence-based Vs Observer-based Approaches to Verify Current-State Opacity: A Benchmark Case

Current-state opacity deals with the capability to hide a set of reachable states from a malicious intruder that can partially observe the system's dynamic. In bounded discrete event systems, the main approach adopted to verify opacity is the so-called observer-based one, where a (possibly reduced order) observer or estimator of the system's dynamic is used to verify whether the intruder can infer if the estimated current state is fully included in the set of secrets. On the other hand, sequence-based approaches to verify opacity consist of checking if, given a sequence leading to the secret state, there exists at least another one generating the same external observation but leading to a not-secret state, on a language with finite-cardinality, even in the case of live systems. This paper compares the performance of two different algorithms for current-state opacity verification: a sequence-based one that requires solving optimization problems and observer-based ones that use a modified version of the Basis Reachability Graph.