Verification and synthesis for secrecy in discrete-event systems
Verification and synthesis for secrecy in discrete-event systems
复制标题
DOI：
10.1109/acc.2009.5160162
复制
发表时间：
2009-06
期刊：
影响因子：
--
通讯作者：
S. Takai;Ratnesh Kumar
中科院分区：
文献类型：
--
作者：
S. Takai;Ratnesh Kumar
对观察者保密系统行为的属性(观察者对任何执行的行为有部分观察)要求观察者不能知道任何满足属性或违反属性的行为的执行。当观察者不知道它观察到的系统的确切行为时，可以定义一个较弱的保密概念，我们在本文中介绍了这一概念。我们给出了一个验证保密性及其弱版本的算法。当给定的系统不具有保密性时，我们考虑通过监督控制来限制系统的行为，以确保被控系统满足期望的保密性。我们证明了最大允许监督者的存在，以确保保密性或其弱版本，并给出了它们的合成算法。
Keeping a property of system behaviors secret from an observer (who has a partial observation of any executed behavior) requires that the execution of any property-satisfying or property-violating behavior must not become known to the observer. When an observer does not know the exact behaviors of a system it observes, a weaker notion of secrecy can be defined, which we introduce in this paper. We present an algorithm for verifying the properties of secrecy as well as its weaker version. When a given system does not possess a secrecy property, we consider restricting the behaviors of the system by means of supervisory control so as to ensure that the controlled system satisfies the desired secrecy property. We show the existence of a maximally permissive supervisor to ensure secrecy or its weaker version, and present algorithms for their synthesis.