学习型状态估计系统鲁棒性与恢复力的形式化验证

本文提出一种形式化验证引导的方法，用于鲁棒且可恢复的学习使能系统的规范化设计与实现。我们聚焦于学习使能状态估计系统（LE-SESs），其已广泛应用于机器人应用中以确定复杂系统的当前状态（如位置、速度、方向等）。LE-SESs是网络化系统，由一组相连组件构成，包括用于状态估计的贝叶斯滤波器，以及用于处理感官输入的神经网络。我们从形式化验证的角度研究LE-SESs，即判定系统模型是否满足给定性质。针对LE-SESs，我们考察了两个关键性质——鲁棒性与恢复力——并给出其形式化定义。为支持形式化验证，我们将LE-SESs归约为一类新颖的标记转移系统，文中称为{PO}^2-LTS，并将性质形式化为约束优化目标。我们证明验证问题是NP完全的。基于{PO}^2-LTS与优化目标，开发了实用验证算法以检查LE-SESs上性质的满足性。作为一个主要案例研究，我们审视了一个真实动态跟踪系统，其使用单个卡尔曼滤波器（KF）——贝叶斯滤波器的特例——来定位并跟踪地面车辆。其感知系统基于卷积神经网络，处理高分辨率广域运动图像（WAMI）数据流。实验结果表明，我们的算法不仅能验证WAMI跟踪系统的性质，还能提供代表性示例，后者启发我们采用一种增强的LE-SESs设计，其中需要运行时监视器或联合KF。实验结果证实了增强设计在鲁棒性上的提升。