Linear Temporal Logic Satisfaction in Adversarial Environments Using Secure Control Barrier Certificates
Linear Temporal Logic Satisfaction in Adversarial Environments Using Secure Control Barrier Certificates
复制标题
DOI：
10.1007/978-3-030-32430-8_23
复制
发表时间：
2019-10
期刊：
影响因子：
--
通讯作者：
Bhaskar Ramasubramanian;Luyao Niu;Andrew Clark;L. Bushnell;R. Poovendran
中科院分区：
文献类型：
--
作者：
Bhaskar Ramasubramanian;Luyao Niu;Andrew Clark;L. Bushnell;R. Poovendran
本文研究了在离散时间动力学描述的环境中，在有限的时间范围内，在存在对手的情况下，网络物理系统（CPS）的一类时间属性的满足。时序逻辑规范中给出的，一个片段的线性时序逻辑的痕迹有限长度。CPS与对手的相互作用被建模为一个两人零和离散时间动态随机博弈的CPS作为防御者。我们制定了一个基于动态规划的方法来确定一个固定的防御者的政策，最大限度地满足aformula在有限的时间范围内的任何固定的对手的政策的概率。我们介绍了安全控制屏障证书（S-CBCs），概括的屏障证书和控制屏障证书，占对手的存在，并使用S-CBCs提供上述满意度概率的下限。当系统状态演化的动力学具有特定的底层结构时，我们提出了一种使用平方和优化将S-CBC确定为状态变量中的多项式的方法。一个示例说明了我们的方法。
This paper studies the satisfaction of a class of temporal properties for cyber-physical systems (CPSs) over a finite-time horizon in the presence of an adversary, in an environment described by discrete-time dynamics. The temporal logic specification is given in, a fragment of linear temporal logic over traces of finite length. The interaction of the CPS with the adversary is modeled as a two-player zero-sum discrete-time dynamic stochastic game with the CPS as defender. We formulate a dynamic programming based approach to determine a stationary defender policy that maximizes the probability of satisfaction of aformula over a finite time-horizon under any stationary adversary policy. We introducesecure control barrier certificates(S-CBCs), a generalization of barrier certificates and control barrier certificates that accounts for the presence of an adversary, and use S-CBCs to provide a lower bound on the above satisfaction probability. When the dynamics of the evolution of the system state has a specific underlying structure, we present a way to determine an S-CBC as a polynomial in the state variables using sum-of-squares optimization. An illustrative example demonstrates our approach.