  In this paper, we investigate the verification and enforcement of strong
state-based opacity (SBO) in discrete-event systems modeled as
partially-observed (nondeterministic) finite-state automata, including strong
K-step opacity (K-SSO), strong current-state opacity (SCSO), strong
initial-state opacity (SISO), and strong infinite-step opacity (Inf-SSO). They
are stronger versions of four widely-studied standard opacity notions,
respectively. We firstly propose a new notion of K-SSO, and then we construct a
concurrent-composition structure that is a variant of our previously-proposed
one to verify it. Based on this structure, a verification algorithm for the
proposed notion of K-SSO is designed. Also, an upper bound on K in the proposed
K-SSO is derived. Secondly, we propose a distinctive opacity-enforcement
mechanism that has better scalability than the existing ones (such as
supervisory control). The basic philosophy of this new mechanism is choosing a
subset of controllable transitions to disable before an original system starts
to run in order to cut off all its runs that violate a notion of strong SBO of
interest. Accordingly, the algorithms for enforcing the above-mentioned four
notions of strong SBO are designed using the proposed two
concurrent-composition structures. In particular, the designed algorithm for
enforcing Inf-SSO has lower time complexity than the existing one in the
literature, and does not depend on any assumption. Finally, we illustrate the
applications of the designed algorithms using examples.
