Autonomous robots used in infrastructure inspection, space exploration and other critical missions operate in highly dynamic environments. As such, they must continually verify their ability to complete the tasks associated with these missions safely and effectively. Here we present a Bayesian learning framework that enables this runtime verification of autonomous robots. The framework uses prior knowledge and observations of the verified robot to learn expected ranges for the occurrence rates of regular and singular (e.g., catastrophic failure) events. Interval continuous-time Markov models defined using these ranges are then analysed to obtain expected intervals of variation for system properties such as mission duration and success probability. We apply the framework to an autonomous robotic mission for underwater infrastructure inspection and repair. The formal proofs and experiments presented in the paper show that our framework produces results that reflect the uncertainty intrinsic to many real-world systems, enabling the robust verification of their quantitative properties under parametric uncertainty.

翻译：用于基础设施巡检、空间探测及其他关键任务的自主机器人运行在高度动态的环境中。因此，它们必须持续验证自身安全高效完成这些任务相关工作的能力。本文提出一种贝叶斯学习框架，使自主机器人能够实现运行时验证。该框架利用已验证机器人的先验知识与观测数据，学习常规事件与异常事件（如灾难性故障）发生率的预期范围。通过利用这些范围定义的区间连续时间马尔可夫模型，可分析获得任务持续时间、成功概率等系统属性的预期变化区间。我们将该框架应用于水下基础设施巡检与修复的自主机器人任务。论文中给出的形式化证明与实验表明，我们的框架能产出反映现实系统固有不确定性的结果，从而在参数不确定条件下实现其定量属性的鲁棒验证。