English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Tools annual

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

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

Verification and Enforcement of Strong State-Based Opacity for Discrete-Event Systems