Verification of K-step opacity and analysis of its complexity
Hadjicostis, Christoforos N.
SourceProceedings of the IEEE Conference on Decision and Control
Proceedings of the IEEE Conference on Decision and Control
Google Scholar check
MetadataShow full item record
In this paper, we analyze the verification of K-step opacity in discrete event systems that are modeled as (possibly non-deterministic) finite automata with partial observation on their transitions. A system is K-step opaque if the entrance of the system state within the last K observations to a set of secret states remains opaque to an intruder who has complete knowledge of the system model and observes system activity through some projection map. We establish that the verification of K-step opacity is NP-hard. We also investigate the role of delay K in K-step opacity and show that there exists a delay K* such that K-step opacity and K'-step opacity become equivalent for K' > K ≥ K*. ©2009 IEEE.