Statistical verification of learning-based cyber-physical systems
Statistical verification of learning-based cyber-physical systems
复制标题
DOI：
10.1145/3365365.3382209
复制
发表时间：
2020-04
期刊：
影响因子：
--
通讯作者：
Mojtaba Zarei;Yu Wang;Miroslav Pajic
中科院分区：
文献类型：
--
作者：
Mojtaba Zarei;Yu Wang;Miroslav Pajic
近年来，基于神经网络（NN）的控制器的使用引起了极大的关注。然而，由于这种基于神经网络的网络物理系统（CPS）的复杂性和非线性，采用穷举状态空间搜索的现有验证技术面临着重大的可扩展性挑战;这有效地限制了它们用于分析现实世界的CPS。在这项工作中，我们专注于使用统计模型检查（SMC）验证复杂的NN控制CPS。使用基于Clopper-Pearson置信水平的SMC方法，我们从信号时序逻辑（STL）公式捕获的样本规格进行验证。具体来说，我们考虑三个CPS基准与不同水平的工厂和控制器的复杂性，以及类型的STL属性-可达性属性的山地车，安全属性的双足机器人，和闭环磁悬浮系统的控制性能。在这些基准测试中，我们表明SMC方法可以成功地用于为基于学习的CPS提供高保证。
The use of Neural Network (NN)-based controllers has attracted significant attention in recent years. Yet, due to the complexity and non-linearity of such NN-based cyber-physical systems (CPS), existing verification techniques that employ exhaustive state-space search, face significant scalability challenges; this effectively limits their use for analysis of real-world CPS. In this work, we focus on the use of Statistical Model Checking (SMC) for verifying complex NN-controlled CPS. Using an SMC approach based on Clopper-Pearson confidence levels, we verify from samples specifications that are captured by Signal Temporal Logic (STL) formulas. Specifically, we consider three CPS benchmarks with varying levels of plant and controller complexity, as well as the type of considered STL properties - reachability property for a mountain car, safety property for a bipedal robot, and control performance of the closed-loop magnet levitation system. On these benchmarks, we show that SMC methods can be successfully used to provide high-assurance for learning-based CPS.