基于安全控制障碍证书在对抗环境中满足线性时序逻辑
系统与控制
2019-10-29 v1 计算机科学与博弈论
计算机科学中的逻辑
系统与控制
摘要
本文研究了在离散时间动力学描述的环境中，存在对手时网络物理系统(CPSs)在有限时间范围内一类时序性质的满足问题。时序逻辑规范由safe-LTL_F给出，这是有限长度轨迹上线性时序逻辑的一个片段。CPS与对手的交互被建模为一个二人零和离散时间动态随机博弈，其中CPS为防御者。我们提出了一种基于动态规划的方法，以确定一个平稳防御者策略，该策略在任何平稳对手策略下最大化有限时间范围内safe-LTL_F公式的满足概率。我们引入了安全控制障碍证书(S-CBCs)，它是障碍证书和控制障碍证书的推广，考虑了对手的存在，并利用S-CBCs给出上述满足概率的下界。当系统状态演化的动力学具有特定的底层结构时，我们给出了一种使用平方和优化将S-CBC确定为状态变量多项式的方法。一个说明性示例展示了我们的方法。
引用
@article{arxiv.1910.12282,
title = {Linear Temporal Logic Satisfaction in Adversarial Environments using Secure Control Barrier Certificates},
author = {Bhaskar Ramasubramanian and Luyao Niu and Andrew Clark and Linda Bushnell and Radha Poovendran},
journal= {arXiv preprint arXiv:1910.12282},
year = {2019}
}
备注
Proc. of GameSec2019 (to appear). This version corrects a typo in the simulation, and clarifies some ambiguous material from the Proceedings version