Click here to flash read.
Opacity is an important system-theoretic property expressing whether a system
may reveal its secret to a passive observer (an intruder) who knows the
structure of the system but has only limited observations of its behavior.
Several notions of opacity have been discussed in the literature, including
current-state opacity, k-step opacity, and infinite-step opacity. We
investigate weak and strong k-step opacity, the notions that generalize both
current-state opacity and infinite-step opacity, and ask whether the intruder
is not able to decide, at any instant, when respectively whether the system was
in a secret state during the last k observable steps. We design a new algorithm
verifying weak k-step opacity, the complexity of which is lower than the
complexity of existing algorithms and does not depend on the parameter k, and
show how to use it to verify strong k-step opacity by reducing strong k-step
opacity to weak k-step opacity. The complexity of the resulting algorithm is
again better than the complexity of existing algorithms and does not depend on
the parameter k.
