Modular Verification of Opacity for Interconnected Control Systems via Barrier Certificates
Modular Verification of Opacity for Interconnected Control Systems via Barrier Certificates
复制标题
DOI：
10.1109/lcsys.2021.3087103
复制
发表时间：
2022
影响因子：
3
通讯作者：
Shadi Tasdighi Kalat;Siyuan Liu;Majid Zamani
中科院分区：
文献类型：
--
作者：
Shadi Tasdighi Kalat;Siyuan Liu;Majid Zamani
在这封信中，我们考虑的问题，验证初始状态不透明的离散时间控制系统的网络。我们制定的不透明性作为一个安全的适当构造的增强系统，并旨在通过找到合适的屏障证书来验证后一个属性。为了减少计算复杂性与计算屏障证书的大型网络，我们提出了一种组合的方法来构建这样的屏障证书的大型互联系统。这是通过在网络中的子系统引入本地屏障证书，并对这些本地屏障证书的增益施加一些小增益类型的条件来实现的。我们还提供了充分的条件，验证缺乏不透明性的大规模网络，通过构建屏障证书，确保一些可达性的增强系统。为了说明我们的研究结果的有效性，我们考虑的问题，跟踪一个目标，使用一组车辆，并验证其初始位置是否是秘密的可能的外部入侵者。
In this letter, we consider the problem of verifying initial-state opacity for networks of discrete-time control systems. We formulate the opacity property as a safety one over an appropriately constructed augmented system, and aim to verify this latter property by finding suitable barrier certificates. To reduce the computational complexity associated with computing barrier certificates for large networks, we propose a compositional approach to construct such barrier certificates for large-scale interconnected systems. This is achieved by introducing local barrier certificates for subsystems in the network and imposing some small-gain type conditions on the gains of those local barrier certificates. We also provide sufficient conditions for verifying the lack of opacity in large-scale networks by constructing barrier certificates ensuring some reachability properties over the augmented systems. To illustrate the effectiveness of our results, we consider the problem of tracking a target using a team of vehicles and verify if its initial position is secret from possible outside intruders.