论文标题
对离散事件系统的强k-step不透明度验证
Verification of Strong K-Step Opacity for Discrete-Event Systems
论文作者
论文摘要
在本文中，我们重新审查了强k-step obyacity（K-SSO）的验证，以对以非确定性有限态自动机为模型的部分观察到的离散事件系统。作为标准K-Step不透明度的更强大版本，K-SSO要求入侵者无法确保在最后一个可观察的步骤中是否访问过秘密状态。为了有效验证K-SSO，我们提出了一种新的并发结构，这是我们先前提出的一种变体。基于这种新结构，我们设计了一种用于确定K-SSO的算法，并证明了所提出的算法不仅降低了现有算法的时间复杂性，而且还不取决于K.的价值。此外，在K-SSO中k中K的价值的新上限是k-SSO中的新上限，这还降低了现有范围内的K-SSO的界限。最后，我们通过一个简单的示例说明了所提出的算法。
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.
