Providing guarantees on the safe operation of robots against edge cases is challenging as testing methods such as traditional Monte-Carlo require too many samples to provide reasonable statistics. Built upon recent advancements in rare-event sampling, we present a model-based method to verify if a robotic system satisfies a Signal Temporal Logic (STL) specification in the face of environment variations and sensor/actuator noises. Our method is efficient and applicable to both linear and nonlinear and even black-box systems with arbitrary, but known, uncertainty distributions. For linear systems with Gaussian uncertainties, we exploit a feature to find optimal parameters that minimize the probability of failure. We demonstrate illustrative examples on applying our approach to real-world autonomous robotic systems.

翻译：针对边缘情况下的机器人安全运行提供保障极具挑战性，因为传统蒙特卡洛等测试方法需要海量样本才能获得合理的统计结果。基于罕见事件采样的最新进展，我们提出了一种基于模型的方法，用于验证机器人系统在环境变化及传感器/执行器噪声影响下是否满足信号时序逻辑（STL）规范。该方法具有高效性，适用于线性和非线性系统，甚至可处理具有任意已知不确定性分布的黑箱系统。针对含高斯不确定性的线性系统，我们利用特征分析寻找最优参数以最小化故障概率。通过将本方法应用于真实自主机器人系统的实例，我们展示了其有效性。