A Neurosymbolic Approach to the Verification of Temporal Logic Properties of Learning enabled Control Systems

arxiv(2023)

引用 0|浏览21
暂无评分
摘要
Signal Temporal Logic (STL) has become a popular tool for expressing formal requirements of Cyber-Physical Systems (CPS). The problem of verifying STL properties of neural network-controlled CPS remains a largely unexplored problem. In this paper, we present a model for the verification of Neural Network (NN) controllers for general STL specifications using a custom neural architecture where we map an STL formula into a feed-forward neural network with ReLU activation. In the case where both our plant model and the controller are ReLU-activated neural networks, we reduce the STL verification problem to reachability in ReLU neural networks. We also propose a new approach for neural network controllers with general activation functions; this approach is a sound and complete verification approach based on computing the Lipschitz constant of the closed-loop control system. We demonstrate the practical efficacy of our techniques on a number of examples of learning-enabled control systems.
更多
查看译文
关键词
Signal Temporal Logic,Verification,Deep Neural Network,Lipstchitz constant,Reachability,Model,Controller,ReLU
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络