  Opacity is an information flow property that captures the notion of plausible
deniability in dynamic systems, that is whether an intruder can deduce that
"secret" behavior has occurred. In this paper we provide a general framework of
opacity to unify the many existing notions of opacity that exist for discrete
event systems. We use this framework to discuss language-based and state-based
notions of opacity over automata. We present several methods for language-based
opacity verification, and a general approach to transform state-based notions
into language-based ones. We demonstrate this approach for current-state and
initial-state opacity, unifying existing results. We then investigate the
notions of K-step opacity. We provide a language-based view of K-step opacity
encompassing two existing notions and two new ones. We then analyze the
corresponding language-based verification methods both formally and with
numerical examples. In each case, the proposed methods offer significant
reductions in runtime and space complexity.
