论文标题
在离散事件系统中验证弱且强大的K-Step不透明度
Verifying Weak and Strong k-Step Opacity in Discrete-Event Systems
论文作者
论文摘要
不透明度是一个重要的系统理论属性，表达系统是否可以向了解系统结构但对其行为的观察有限的被动观察者（入侵者）揭示其秘密。文献中已经讨论了几种不透明度的概念，包括当前状态的不透明性，K-Step不透明度和无限步骤不透明度。我们研究了弱和强大的K-step不透明度，这些概念既概括了当前国家的不透明度和无限步骤不透明度，并询问入侵者在最后一个可观察的步骤中是否在系统中是否处于秘密状态时，在任何瞬间都无法决定。我们设计了一种新的算法，验证了弱k-step不透明度，其复杂性低于现有算法的复杂性，并且不依赖于参数k，并通过降低强大的k-step不透露性来验证强度k-step的不透明度来验证强度k-step nef k-step nef k-step obinity。所得算法的复杂性再次优于现有算法的复杂性，并且不依赖于参数k。
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.
