Verification of Infinite-Step Opacity and Analysis of its Complexity*

In this paper, we formulate, analyze, and devise methodologies to verify the notion of infinite-step opacity in discrete event systems that are modeled as (possibly non-deterministic) finite automata with partial observation on their transitions. Specifically, a system is infinite-step opaque if the entrance of the system state at any particular instant to a set of secret states remains opaque (uncertain), for the length of the system operation, to an intruder who observes system activity through some projection map. In other words, based on observations through this map (and complete knowledge of the system model), the intruder can never be certain (and will never be certain) that the system state at any point in time evolves (or has evolved) to the set of secret states. We show that infinite-step opacity can be verified via the construction of a set of appropriate state estimators. We also establish that the verification of infinite-step opacity is a PSPACE-hard problem.