  We formulate notions of opacity for cyberphysical systems modeled as
discrete-time linear time-invariant systems. A set of secret states is $k$-ISO
with respect to a set of nonsecret states if, starting from these sets at time
$0$, the outputs at time $k$ are indistinguishable to an adversarial observer.
Necessary and sufficient conditions to ensure that a secret specification is
$k$-ISO are established in terms of sets of reachable states. We also show how
to adapt techniques for computing under-approximations and over-approximations
of the set of reachable states of dynamical systems in order to soundly
approximate k-ISO. Further, we provide a condition for output controllability,
if $k$-ISO holds, and show that the converse holds under an additional
assumption.
  We extend the theory of opacity for single-adversary systems to the case of
multiple adversaries and develop several notions of decentralized opacity. We
study the following scenarios: i) the presence or lack of a centralized
coordinator, and ii) the presence or absence of collusion among adversaries. In
the case of colluding adversaries, we derive a condition for nonopacity that
depends on the structure of the directed graph representing the communication
between adversaries.
  Finally, we relax the condition that the outputs be indistinguishable and
define a notion of $\epsilon$-opacity, and also provide an extension to the
case of nonlinear systems.
