Verification of K-step opacity and analysis of its complexity
Date
2009ISBN
978-1-4244-3871-6Source
Proceedings of the IEEE Conference on Decision and ControlProceedings of the IEEE Conference on Decision and Control
Pages
205-210Google Scholar check
Keyword(s):
Metadata
Show full item recordAbstract
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.