  In this paper, we revisit the verification of strong K-step opacity (K-SSO)
for partially-observed discrete-event systems modeled as nondeterministic
finite-state automata. As a stronger version of the standard K-step opacity,
K-SSO requires that an intruder cannot make sure whether or not a secret state
has been visited within the last K observable steps. To efficiently verify
K-SSO, we propose a new concurrent-composition structure, which is a variant of
our previously- proposed one. Based on this new structure, we design an
algorithm for deciding K-SSO and prove that the proposed algorithm not only
reduces the time complexity of the existing algorithms, but also does not
depend on the value of K. Furthermore, a new upper bound on the value of K in
K-SSO is derived, which also reduces the existing upper bound on K in the
literature. Finally, we illustrate the proposed algorithm by a simple example.
